twee-0.1: tests/y.p
cnf(a, axiom, '@'('@'('@'(c, X), Y), Z) = '@'(X, '@'(Y, Z))).
cnf(a, axiom, '@'('@'('@'(f, X), Y), Z) = '@'('@'(X, Z), Y)).
cnf(a, axiom, '@'(w, X) = '@'(X, X)).
cnf(a, axiom, '@'(X, a) != '@'(a, '@'(X, a))).
cnf(a, axiom, '@'('@'('@'(c, X), Y), Z) = '@'(X, '@'(Y, Z))).
cnf(a, axiom, '@'('@'('@'(f, X), Y), Z) = '@'('@'(X, Z), Y)).
cnf(a, axiom, '@'(w, X) = '@'(X, X)).
cnf(a, axiom, '@'(X, a) != '@'(a, '@'(X, a))).