twee-2.3.1: tests/group_plain.p

cnf(associativity, axiom,
    plus(X,plus(Y,Z))=plus(plus(X,Y),Z)).
cnf(plus_zero, axiom,
    plus(zero, X) = X).
cnf(plus_zero, axiom,
    plus(X, zero) = X).
cnf(minus_left, axiom,
    plus(neg(X),X) = zero).
cnf(minus_right, axiom,
    plus(X,neg(X)) = zero).
cnf(assumption, assumption,
    plus(a, b) = a).
cnf(goal, conjecture,
    b = zero).