============================== Prover9 =============================== Prover9 (32) version June-2007, June 2007. Process 4538 was started by zalta on mally, Sat Jul 14 15:08:32 2007 The command was "prove". ============================== end of head =========================== ============================== INPUT ================================= formulas(goals). (all x all y all z (x = y -> Sum(x,z) = Sum(y,z))). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all x all y all z (x = y -> Sum(x,z) = Sum(y,z))) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). c2 = c1. [deny(1)]. Sum(c2,c3) != Sum(c1,c3). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, c3, Sum ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 4. % Level of proof is 2. % Maximum clause weight is 3. % Given clauses 0. 1 (all x all y all z (x = y -> Sum(x,z) = Sum(y,z))) # label(non_clause) # label(goal). [goal]. 2 c2 = c1. [deny(1)]. 3 Sum(c2,c3) != Sum(c1,c3). [deny(1)]. 4 $F. [copy(3),rewrite([2(1)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=2. Kept=1. proofs=1. Usable=0. Sos=0. Demods=1. Limbo=1, Disabled=2. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=0. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=8. Demod_rewrites=1. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.01. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 4538 exit (max_proofs) Sat Jul 14 15:08:32 2007