twee-0.1: tests/lukasiewicz.p

cnf(a, axiom, implies(true, X) = X).
cnf(a, axiom, implies(implies(X, Y), implies(implies(Y, Z), implies(X, Z))) = true).
cnf(a, axiom, implies(implies(not(X), not(Y)), implies(Y, X)) = true).
cnf(a, axiom, implies(implies(X, Y), Y) = implies(implies(Y, X), X)).
cnf(a, axiom, or(X, Y) = implies(not(X), Y)).
cnf(a, axiom, or(a,or(b,c)) != or(or(a,b),c)).