Problem:
 and3(x,y,F()) -> F()
 and3(T(),T(),T()) -> T()
 and3(x,y,z) -> and3(y,z,x)

Proof:
 Open