twee-2.1.1: tests/veroff.p

cnf(majority, axiom,
    f(X,X,Y) = X).
cnf('2a', axiom,
    f(X,Y,Z) = f(Z,X,Y)).
cnf('2b', axiom,
    f(X,Y,Z) = f(X,Z,Y)).
cnf(associativity, axiom,
    f(f(X,W,Y),W,Z) = f(X,W,f(Y,W,Z))).

cnf(goal, axiom, f(f(a1,a2,a3),a4,a5) != f(f(a1,a4,a5),f(a2,a4,a5),f(a3,a4,a5))).