twee-2.5: tests/ROB007-1-a.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,(
    g(A) = inv(add(A,inv(A))) )).

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