twee-2.5: tests/ROB007-1.p

cnf(commutativity_of_add, axiom, add(X, Y)=add(Y, X)).
cnf(associativity_of_add, axiom, add(add(X, Y), Z)=add(X, add(Y, Z))).
cnf(robbins_axiom, axiom, negate(add(negate(add(X, Y)), negate(add(X, negate(Y)))))=X).
cnf(condition, hypothesis, negate(add(a, b))=negate(b)).
cnf(prove_huntingtons_axiom, negated_conjecture, add(negate(add(a, negate(b))), negate(add(negate(a), negate(b))))!=b).