twee-2.5: tests/lukasiewicz2.p
cnf(detachment, axiom, (p(X) & p(i(X,Y))) => p(Y)). cnf(lukasiewicz, axiom, p(i(i(i(P,Q),R),i(i(R,P),i(S,P))))). cnf(simp, axiom, p(i(P, i(Q, Q)))). cnf(peirce, axiom, p(i(i(i(P,Q),P),P))). cnf(syll, conjecture, p(i(i(a,b),i(i(b,c),i(a,c))))).