twee-2.6.1: tests/ROB007-1-b.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, inv(add(inv(add(X, Y)), inv(add(X, inv(Y)))))=X).
cnf(condition, hypothesis, inv(add(a, b))=inv(b)).
cnf(prove_huntingtons_axiom, negated_conjecture, add(inv(add(a, inv(b))), inv(add(inv(a), inv(b))))!=b).

cnf(sos04,axiom,(
    $hint(inv(add(A,inv(A)))) )).

%----Definition of h
cnf(sos05,axiom,(
    $hint(add(A,add(A,add(A,inv(add(A,inv(A))))))))).