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

sIdx(r0,0).
sCov(r0,(Top,Next)) :- 
	incomplete(_,Top), clear(Top), goal(Next,Top), clear(Next).
aCov(move(next,top), move(Next,Top)) :- sChoice(r0), sCov(r0,(Top,Next)).
 
sIdx(r1,1).
sCov(r1,(Basis,Top,BadTop)) :- 
	incomplete(Basis,Top), not clear(Top),
	above(BadTop,Top), clear(BadTop).
aCov(move(badTop,table),move(BadTop,table)) :- 
	sChoice(r1), sCov(r1,(_,_,BadTop)).
aCov(move(badTop,other),move(BadTop,Other)) :- 
	sChoice(r1), sCov(r1,(Basis,Top,BadTop)),
	clear(Other), Other!=BadTop, Other!=table.

sIdx(r2,2).
sCov(r2,(Top,BadTop)) :- 	
	incomplete(Basis,Top), clear(Top), goal(Next,Top),
	not clear(Next), above(BadTop,Next), clear(BadTop).
aCov(move(badTop,table), move(BadTop,table)) :- 
	sChoice(r2), sCov(r2,(_,BadTop)).
aCov(move(badTop,otherTowerTop), move(BadTop,Other)) :- 
	sChoice(r2), sCov(r2,(Top,BadTop)),
	clear(Other), Other!=Top, Other!=BadTop, Other!=table.

sIdx(r3,3).
sCov(r3,(BadTop)) :- 
	not finalBasis(_), goal(_,Basis), not goal(Basis,_),
	not clear(Basis), above(BadTop,Basis), clear(BadTop).
aCov(move(badTop,table), move(BadTop,table)) :- 
	sChoice(r3), sCov(r3,(BadTop)).
aCov(move(badTop,otherTowerTop), move(BadTop,Other)) :- 
	sChoice(r3), sCov(r3,(BadTop)), clear(Other),
	Other!=BadTop, Other!=table.

sIdx(r4,4).
sCov(r4,(Basis)) :- 
	not finalBasis(_), goal(_,Basis),
	not goal(Basis,_), clear(Basis).
aCov(move(basis,table), move(Basis,table)) :- 
	sChoice(r4), sCov(r4,(Basis)).

sIdx(true,#sup).	
sCov(true,()).
aCov(others, move(X,Y)) :- 
	clear(X), clear(Y), X!=Y, X!=table, 
	not aCov(move(_,_),move(X,Y)), not on(X,Y).