twee-0.1: tests/nicomachus.p

cnf(a, axiom, plus(X, Y) = plus(Y, X)).
cnf(a, axiom, plus(X, plus(Y, Z)) = plus(plus(X, Y), Z)).
cnf(a, axiom, times(X, Y) = times(Y, X)).
cnf(a, axiom, times(X, times(Y, Z)) = times(times(X, Y), Z)).
cnf(a, axiom, plus(X, zero) = X).
cnf(a, axiom, times(X, zero) = zero).
cnf(a, axiom, times(X, one) = X).
cnf(a, axiom, times(X, plus(Y, Z)) = plus(times(X, Y), times(X, Z))).
cnf(a, axiom, times(plus(X, Y), Z) = plus(times(X, Z), times(Y, Z))).
cnf(a, axiom, plus(s(X), Y) = s(plus(X, Y))).
cnf(a, axiom, times(s(X), Y) = plus(Y, times(X, Y))).
cnf(a, axiom, sum(zero) = zero).
cnf(a, axiom, sum(s(N)) = plus(s(N), sum(N))).
cnf(a, axiom, cubes(zero) = zero).
cnf(a, axiom, cubes(s(N)) = plus(times(s(N), times(s(N), s(N))), cubes(N))).
cnf(a, axiom, plus(sum(N), sum(N)) = times(N, s(N))).
cnf(a, axiom, times(sum(a), sum(a)) = cubes(a)).
cnf(a, axiom, times(sum(s(a)), sum(s(a))) != cubes(s(a))).