============================== Prover9 =============================== Prover9 (32) version June-2007, June 2007. Process 4883 was started by zalta on mally, Sat Jul 14 17:15:21 2007 The command was "prove". ============================== end of head =========================== ============================== INPUT ================================= formulas(sos). (all x all y all z Sum(Sum(x,y),z) = Sum(x,Sum(y,z))). (all x all y (IsIn(x,y) <-> (exists z Sum(x,z) = y))). end_of_list. formulas(goals). (all x all y all z (IsIn(y,z) -> IsIn(Sum(x,y),Sum(x,z)))). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all x all y all z Sum(Sum(x,y),z) = Sum(x,Sum(y,z))) # label(non_clause). [assumption]. 2 (all x all y (IsIn(x,y) <-> (exists z Sum(x,z) = y))) # label(non_clause). [assumption]. 3 (all x all y all z (IsIn(y,z) -> IsIn(Sum(x,y),Sum(x,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). Sum(Sum(x,y),z) = Sum(x,Sum(y,z)). [clausify(1)]. -IsIn(x,y) | Sum(x,f1(x,y)) = y. [clausify(2)]. IsIn(x,y) | Sum(x,z) != y. [clausify(2)]. IsIn(c2,c3). [deny(3)]. -IsIn(Sum(c1,c2),Sum(c1,c3)). [deny(3)]. 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([ =, IsIn ]). Function symbol precedence: function_order([ c1, c2, c3, Sum, f1 ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(hyper_resolution) -> set(pos_hyper_resolution). % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 2). % (nonunit Horn with equality) Auto_process settings: (no changes). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 4 Sum(Sum(x,y),z) = Sum(x,Sum(y,z)). [clausify(1)]. 5 -IsIn(x,y) | Sum(x,f1(x,y)) = y. [clausify(2)]. 6 IsIn(x,y) | Sum(x,z) != y. [clausify(2)]. 7 IsIn(c2,c3). [deny(3)]. 8 -IsIn(Sum(c1,c2),Sum(c1,c3)). [deny(3)]. end_of_list. formulas(demodulators). 4 Sum(Sum(x,y),z) = Sum(x,Sum(y,z)). [clausify(1)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=11): 4 Sum(Sum(x,y),z) = Sum(x,Sum(y,z)). [clausify(1)]. given #2 (I,wt=10): 5 -IsIn(x,y) | Sum(x,f1(x,y)) = y. [clausify(2)]. given #3 (I,wt=8): 6 IsIn(x,y) | Sum(x,z) != y. [clausify(2)]. given #4 (I,wt=3): 7 IsIn(c2,c3). [deny(3)]. given #5 (I,wt=7): 8 -IsIn(Sum(c1,c2),Sum(c1,c3)). [deny(3)]. given #6 (A,wt=9): 9 IsIn(Sum(x,y),Sum(x,Sum(y,z))). [hyper(6,b,4,a)]. given #7 (F,wt=9): 14 Sum(c1,Sum(c2,x)) != Sum(c1,c3). [ur(6,a,8,a),rewrite([4(4)])]. given #8 (T,wt=5): 11 IsIn(x,Sum(x,y)). [hyper(6,b,xx)]. given #9 (T,wt=7): 13 Sum(c2,f1(c2,c3)) = c3. [hyper(5,a,7,a)]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 12. % Level of proof is 4. % Maximum clause weight is 11. % Given clauses 9. 1 (all x all y all z Sum(Sum(x,y),z) = Sum(x,Sum(y,z))) # label(non_clause). [assumption]. 2 (all x all y (IsIn(x,y) <-> (exists z Sum(x,z) = y))) # label(non_clause). [assumption]. 3 (all x all y all z (IsIn(y,z) -> IsIn(Sum(x,y),Sum(x,z)))) # label(non_clause) # label(goal). [goal]. 4 Sum(Sum(x,y),z) = Sum(x,Sum(y,z)). [clausify(1)]. 5 -IsIn(x,y) | Sum(x,f1(x,y)) = y. [clausify(2)]. 6 IsIn(x,y) | Sum(x,z) != y. [clausify(2)]. 7 IsIn(c2,c3). [deny(3)]. 8 -IsIn(Sum(c1,c2),Sum(c1,c3)). [deny(3)]. 9 IsIn(Sum(x,y),Sum(x,Sum(y,z))). [hyper(6,b,4,a)]. 13 Sum(c2,f1(c2,c3)) = c3. [hyper(5,a,7,a)]. 20 IsIn(Sum(x,c2),Sum(x,c3)). [para(13(a,1),9(a,2,2))]. 21 $F. [resolve(20,a,8,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=9. Generated=30. Kept=17. proofs=1. Usable=9. Sos=4. Demods=5. Limbo=2, Disabled=6. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=13. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=5 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=231. Demod_rewrites=24. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=1. Nonunit_bsub_feature_tests=4. Megabytes=0.04. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 4883 exit (max_proofs) Sat Jul 14 17:15:21 2007