twee-0.1: tests/plus-combinator.p

cnf(a, axiom, app(app('+', X), Y) = app(app('+', Y), X)).
cnf(a, axiom, app(app('+', X), app(app('+', Y), Z)) = app(app('+', app(app('+', X), Y)), Z)).