twee-2.6.1: tests/rob.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(winker_specialised, conjecture,
    add(add(x,x), negate(add(negate(add(x,add(x,x))),x))) = add(x,x)).