twee-2.6.1: tests/nicomachus-tptp.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(plus_sum_step_1, axiom, plus(sum(zero), sum(zero)) = times(zero, s(zero)) => plus(sum(ih_a), sum(ih_a)) = times(ih_a, s(ih_a))).
cnf(plus_sum, axiom, (plus(sum(zero), sum(zero)) = times(zero, s(zero)) & plus(sum(s(ih_a)), sum(s(ih_a))) = times(s(ih_a), s(s(ih_a)))) => 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))).