fof( mult_assoc, axiom, ![A,B,C] : mult(mult(A,B),C) = mult(A,mult(B,C)) ). fof( mult_comm, axiom, ![A,B] : mult(A,B) = mult(B,A) ). fof( mult_unit, axiom, ![A] : mult(A,one) = A ). fof( mult_recip, axiom, ![A] : (A!=zero => mult(A,recip(A))=one) ). fof( mult_zero, axiom, ![A] : mult(A,zero) = zero ). fof( succ_pred_id, axiom, ![A] : s(p(A)) = A ). fof( pred_succ_id, axiom, ![A] : p(s(A)) = A ). fof( succ_zero_one, axiom, s(zero) = one ). fof( succ_charn, axiom, ![A,B] : (A!=zero => s(mult(A,s(mult(B,recip(A))))) = mult(A,s(mult(s(B),recip(A))))) ). fof( add_def1, axiom, ![A,B] : (A!=zero => add(A,B) = mult(A,s(mult(B,recip(A))))) ). fof( add_def2, axiom, ![B] : add(zero,B) = B ). fof( add_assoc, conjecture, ![A,B,C] : add(add(A,B),C) = add(A,add(B,C)) ). % Out of Memory fof( add_comm, conjecture, ![A,B] : add(A,B) = add(B,A) ). fof( add_unit, conjecture, ![A] : add(A,zero) = A ). % OK fof( add_inv, conjecture, ![A] : ?[B] : add(A,B) = zero ). % OK fof( dist, conjecture, ![A,B,C] : mult(A,add(B,C)) = add(mult(A,B),mult(A,C)) ). % Failure: Resource limit exceeded (memory) % eprover -l 2 --tptp3-in AGS.tptp > out.pcl % checkproof out.pcl