sIdx("2towers",1).
sCov("2towers",(A,B,C)) :- 
	on(A,B), on(B,table), on(C,table), A!=B, B!=C.

aCov("2t-mAC",move(A,C)) :- 
	sChoice("2towers"), sCov("2towers",(A,B,C)), move(A,C).
aCov("2t-mCA",move(C,A)) :- 
	sChoice("2towers"), sCov("2towers",(A,B,C)), move(C,A).
aCov("2t-mAt",move(A,table)) :- 
	sChoice("2towers"), sCov("2towers",(A,B,C)), move(A,table).

sIdx("3towers",2).
sCov("3towers",(A,B,C)) :- 
	on(A,table), on(B,table), on(C,table), A!=B, B!=C, A!=C.

aCov("3t-mAB",move(A,B)) :- 
	sChoice("3towers"), sCov("3towers",(A,B,C)), move(A,B).
aCov("3t-mBA",move(B,A)) :- 
	sChoice("3towers"), sCov("3towers",(A,B,C)), move(B,A).
aCov("3t-mAC",move(A,C)) :- 
	sChoice("3towers"), sCov("3towers",(A,B,C)), move(A,C).
aCov("3t-mCA",move(C,A)) :- 
	sChoice("3towers"), sCov("3towers",(A,B,C)), move(C,A).
aCov("3t-mBC",move(B,C)) :- 
	sChoice("3towers"), sCov("3towers",(A,B,C)), move(B,C).
aCov("3t-mCB",move(C,B)) :- 
	sChoice("3towers"), sCov("3towers",(A,B,C)), move(C,B).

sIdx("1tower",3).
sCov("1tower",(A,B,C)) :- 
	on(A,B), on(B,C), on(C,table), A!=B, B!=C, C!=table.

aCov("1t-mAt",move(A,table)) :- 
	sChoice("1tower"), sCov("1tower",(A,B,C)), move(A,table).

1 { sChoice(R) : sCov(R, _) } 1.
:- sChoice(R), sIdx(R,N), sIdx(R2,N2), sCov(R2, _), N2 < N.