~Equals(A,B)
~Equals(A,C)
~Equals(B,A)
~Equals(B,C)
~Equals(C,A)
~Equals(C,B)
~Equals(A,Table)
~Equals(B,Table)
~Equals(C,Table)	
Block(A)
Block(B)
Block(C)
~Block(Table)

all x all y all z all s On(x,y,s) ^ On(x,z,s) -> Equals(y,z)
all x all y all z all s On(x,z,s) ^ On(y,z,s) -> Equals(x,y) v Equals(z,Table)

all s all x Clear(x,s) <-> (~ exists y Block(y) ^ On(y,x,s)) v Equals(x,Table)

all s all x all y all z Clear(x,s) ^ Clear(y,s) ^ On(x,z,s) -> On(x,y,result(move(x,y),s)) ^ Clear(z,result(move(x,y),s))

all s all x all y all z all w On(x,y,s) ^ ~Equals(x,z) -> On(x,y,result(move(z,w),s))

all s all x all y all z Clear(x,s) ^ ~Equals(x,z) -> Clear(x,result(move(y,z),s))

On(A,Table,S0)
On(C,B,S0)
On(B,Table,S0)
Clear(C,S0)
Clear(A,S0)
all s Clear(Table,s)

~exists s On(A,B,s) ^ ~Answer(s)