packages feed

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