twee-2.0: tests/nicomachus.p

cnf(plus_comm, axiom, plus(X, Y) = plus(Y, X)).
cnf(plus_assoc, axiom, plus(X, plus(Y, Z)) = plus(plus(X, Y), Z)).
cnf(times_comm, axiom, times(X, Y) = times(Y, X)).
cnf(times_assoc, axiom, times(X, times(Y, Z)) = times(times(X, Y), Z)).
cnf(plus_zero, axiom, plus(X, zero) = X).
cnf(times_zero, axiom, times(X, zero) = zero).
cnf(times_one, axiom, times(X, one) = X).
cnf(distr, axiom, times(X, plus(Y, Z)) = plus(times(X, Y), times(X, Z))).
cnf(distr, axiom, times(plus(X, Y), Z) = plus(times(X, Z), times(Y, Z))).
cnf(plus_s, axiom, plus(s(X), Y) = s(plus(X, Y))).
cnf(times_s, axiom, times(s(X), Y) = plus(Y, times(X, Y))).
cnf(sum_zero, axiom, sum(zero) = zero).
cnf(sum_s, axiom, sum(s(N)) = plus(s(N), sum(N))).
cnf(cubes_zero, axiom, cubes(zero) = zero).
cnf(cubes_s, axiom, cubes(s(N)) = plus(times(s(N), times(s(N), s(N))), cubes(N))).
cnf(plus_sum, axiom, plus(sum(N), sum(N)) = times(N, s(N))).
cnf(ih, axiom, times(sum(a), sum(a)) = cubes(a)).
cnf(conjecture, negated_conjecture, times(sum(s(a)), sum(s(a))) != cubes(s(a))).