twee-0.1: tests/robbins-hard.p

cnf(a, axiom, '-+'(X, Y) = '-'('+'(X, Y))).
cnf(a, axiom, '+'(X, Y) = '+'(Y, X)).
cnf(a, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)).
cnf(a, axiom, '-'('+'('-'('+'(X, Y)), '-'('+'(X, '-'(Y))))) = X).
cnf(a, axiom, '+'('-'('+'('-'(a), b)), '-'('+'('-'(a), '-'(b)))) != a).