twee-2.3: tests/loop2.p

cnf('*-\\', axiom, X * (X \ Y) = Y).
cnf('\\-*', axiom, X \ (X * Y) = Y).
cnf('*-/', axiom, (X / Y) * Y = X).
cnf('/-*', axiom, (X * Y) / Y = X).
cnf(moufang, axiom, X * (Y * (X * Z)) = ((X * Y) * X) * Z).
cnf(conjecture, conjecture, a * (b / b) = a).