twee-2.5: tests/p.p
cnf(a, axiom, p(X)!=true | p(s(X))!=true). cnf(a, axiom, p(X)!=false | p(s(X))!=false). cnf(a, axiom, p(a)=true). cnf(a, axiom, p(s(s(a)))!=true). cnf(a, axiom, true!=false). cnf(p, axiom, p(a)=true). cnf(p, axiom, p(s(a))=true). cnf(p, axiom, p(s(s(a)))=false). cnf(p, axiom, p(s(s(s(a))))=true). cnf(p, axiom, p(s(s(s(X))))=false => p(s(s(s(s(X)))))=true).