twee-2.6.1: tests/rob2.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).
fof(winker, conjecture,
    ?[X,Y]: add(X,Y) = X).