twee-2.3: tests/blah.p

cnf(plus_comm, axiom, '+'(X, Y) = '+'(Y, X)).
cnf(plus_assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)).
cnf(plus_zero, axiom, '+'('0', X) = X).
cnf(plus_inv, axiom, '+'(X, '-'(X)) = '0').
cnf(conjecture, negated_conjecture, '*'(a, b) != '*'(b, a)).