packages feed

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).