twee-2.3: tests/loop-ascii.p

cnf(mult_ld, axiom, mult(X, back(X, Y)) = Y).
cnf(ld_mult, axiom, back(X, mult(X, Y)) = Y).
cnf(mult_rd, axiom, mult(slash(X, Y), Y) = X).
cnf(rd_mult, axiom, slash(mult(X, Y), Y) = X).
cnf(moufang, axiom, mult(X, mult(Y, mult(X, Z))) = mult(mult(mult(X, Y), X), Z)).
cnf(conjecture, conjecture, back(a, a) = slash(a, a)).