============================== Prover9 =============================== Prover9 (32) version June-2007, June 2007. Process 4990 was started by zalta on mally, Sat Jul 14 17:42:19 2007 The command was "prove". ============================== end of head =========================== ============================== INPUT ================================= formulas(sos). (all x all y Sum(x,y) = Sum(y,x)). (all x Sum(x,x) = x). (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(x,z) & IsIn(y,z) -> IsIn(Sum(x,y),z))). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all x all y Sum(x,y) = Sum(y,x)) # label(non_clause). [assumption]. 2 (all x Sum(x,x) = x) # label(non_clause). [assumption]. 3 (all x all y all z Sum(Sum(x,y),z) = Sum(x,Sum(y,z))) # label(non_clause). [assumption]. 4 (all x all y (IsIn(x,y) <-> (exists z Sum(x,z) = y))) # label(non_clause). [assumption]. 5 (all x all y all z (IsIn(x,z) & IsIn(y,z) -> IsIn(Sum(x,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). Sum(x,y) = Sum(y,x). [clausify(1)]. Sum(x,x) = x. [clausify(2)]. Sum(Sum(x,y),z) = Sum(x,Sum(y,z)). [clausify(3)]. -IsIn(x,y) | Sum(x,f1(x,y)) = y. [clausify(4)]. IsIn(x,y) | Sum(x,z) != y. [clausify(4)]. IsIn(c1,c3). [deny(5)]. IsIn(c2,c3). [deny(5)]. -IsIn(Sum(c1,c2),c3). [deny(5)]. 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). % Operation Sum is commutative; C redundancy checks enabled. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 6 Sum(x,y) = Sum(y,x). [clausify(1)]. 7 Sum(x,x) = x. [clausify(2)]. 8 Sum(Sum(x,y),z) = Sum(x,Sum(y,z)). [clausify(3)]. 9 -IsIn(x,y) | Sum(x,f1(x,y)) = y. [clausify(4)]. 10 IsIn(x,y) | Sum(x,z) != y. [clausify(4)]. 11 IsIn(c1,c3). [deny(5)]. 12 IsIn(c2,c3). [deny(5)]. 13 -IsIn(Sum(c1,c2),c3). [deny(5)]. end_of_list. formulas(demodulators). 6 Sum(x,y) = Sum(y,x). [clausify(1)]. % (lex-dep) 7 Sum(x,x) = x. [clausify(2)]. 8 Sum(Sum(x,y),z) = Sum(x,Sum(y,z)). [clausify(3)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 6 Sum(x,y) = Sum(y,x). [clausify(1)]. given #2 (I,wt=5): 7 Sum(x,x) = x. [clausify(2)]. given #3 (I,wt=11): 8 Sum(Sum(x,y),z) = Sum(x,Sum(y,z)). [clausify(3)]. % Operation Sum is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 14 Sum(x,Sum(y,z)) = Sum(z,Sum(x,y)). [para(8(a,1),6(a,1))]. given #4 (I,wt=10): 9 -IsIn(x,y) | Sum(x,f1(x,y)) = y. [clausify(4)]. given #5 (I,wt=8): 10 IsIn(x,y) | Sum(x,z) != y. [clausify(4)]. given #6 (I,wt=3): 11 IsIn(c1,c3). [deny(5)]. given #7 (I,wt=3): 12 IsIn(c2,c3). [deny(5)]. given #8 (I,wt=5): 13 -IsIn(Sum(c1,c2),c3). [deny(5)]. given #9 (A,wt=11): 15 Sum(x,Sum(y,z)) = Sum(y,Sum(x,z)). [para(6(a,1),8(a,1,1)),rewrite([8(2)])]. given #10 (F,wt=7): 29 Sum(c1,Sum(c2,x)) != c3. [ur(10,a,13,a),rewrite([8(4)])]. given #11 (F,wt=5): 33 Sum(c1,c2) != c3. [para(7(a,1),29(a,1,2))]. given #12 (F,wt=7): 32 Sum(c1,Sum(x,c2)) != c3. [para(6(a,1),29(a,1,2))]. given #13 (F,wt=7): 36 Sum(x,Sum(c1,c2)) != c3. [para(15(a,1),32(a,1))]. given #14 (T,wt=3): 20 IsIn(x,x). [hyper(10,b,7,a)]. given #15 (T,wt=5): 21 IsIn(x,Sum(y,x)). [hyper(10,b,6,a)]. given #16 (T,wt=5): 23 IsIn(x,Sum(x,y)). [hyper(10,b,7,a(flip)),rewrite([7(3)])]. given #17 (T,wt=6): 25 IsIn(x,y) | x != y. [para(7(a,1),10(b,1))]. given #18 (A,wt=9): 17 Sum(x,Sum(x,y)) = Sum(x,y). [para(7(a,1),8(a,1,1)),flip(a)]. given #19 (F,wt=9): 34 Sum(c1,Sum(x,Sum(c2,y))) != c3. [para(15(a,1),29(a,1,2))]. given #20 (F,wt=9): 35 Sum(c1,Sum(x,Sum(y,c2))) != c3. [para(8(a,1),32(a,1,2))]. given #21 (F,wt=9): 37 Sum(x,Sum(y,Sum(c1,c2))) != c3. [para(8(a,1),36(a,1))]. given #22 (F,wt=9): 48 Sum(x,Sum(c1,Sum(c2,y))) != c3. [para(15(a,1),34(a,1))]. given #23 (T,wt=7): 27 Sum(c1,f1(c1,c3)) = c3. [hyper(9,a,11,a)]. given #24 (T,wt=5): 57 IsIn(f1(c1,c3),c3). [para(27(a,1),21(a,2))]. given #25 (T,wt=5): 58 Sum(c1,c3) = c3. [para(27(a,1),17(a,1,2)),rewrite([27(8)])]. given #26 (T,wt=6): 55 IsIn(c1,x) | c3 != x. [para(27(a,1),10(b,1))]. given #27 (A,wt=9): 18 Sum(x,Sum(y,x)) = Sum(y,x). [para(7(a,1),8(a,2,2)),rewrite([6(2)])]. given #28 (F,wt=9): 50 Sum(x,Sum(c1,Sum(y,c2))) != c3. [para(15(a,1),35(a,1))]. given #29 (F,wt=11): 47 Sum(c1,Sum(x,Sum(y,Sum(c2,z)))) != c3. [para(8(a,1),34(a,1,2))]. given #30 (F,wt=11): 49 Sum(c1,Sum(x,Sum(y,Sum(z,c2)))) != c3. [para(8(a,1),35(a,1,2,2))]. given #31 (F,wt=11): 51 Sum(x,Sum(y,Sum(z,Sum(c1,c2)))) != c3. [para(8(a,1),37(a,1,2))]. given #32 (T,wt=7): 28 Sum(c2,f1(c2,c3)) = c3. [hyper(9,a,12,a)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 17. % Level of proof is 4. % Maximum clause weight is 11. % Given clauses 32. 2 (all x Sum(x,x) = x) # label(non_clause). [assumption]. 3 (all x all y all z Sum(Sum(x,y),z) = Sum(x,Sum(y,z))) # label(non_clause). [assumption]. 4 (all x all y (IsIn(x,y) <-> (exists z Sum(x,z) = y))) # label(non_clause). [assumption]. 5 (all x all y all z (IsIn(x,z) & IsIn(y,z) -> IsIn(Sum(x,y),z))) # label(non_clause) # label(goal). [goal]. 7 Sum(x,x) = x. [clausify(2)]. 8 Sum(Sum(x,y),z) = Sum(x,Sum(y,z)). [clausify(3)]. 9 -IsIn(x,y) | Sum(x,f1(x,y)) = y. [clausify(4)]. 10 IsIn(x,y) | Sum(x,z) != y. [clausify(4)]. 11 IsIn(c1,c3). [deny(5)]. 12 IsIn(c2,c3). [deny(5)]. 13 -IsIn(Sum(c1,c2),c3). [deny(5)]. 17 Sum(x,Sum(x,y)) = Sum(x,y). [para(7(a,1),8(a,1,1)),flip(a)]. 27 Sum(c1,f1(c1,c3)) = c3. [hyper(9,a,11,a)]. 28 Sum(c2,f1(c2,c3)) = c3. [hyper(9,a,12,a)]. 29 Sum(c1,Sum(c2,x)) != c3. [ur(10,a,13,a),rewrite([8(4)])]. 58 Sum(c1,c3) = c3. [para(27(a,1),17(a,1,2)),rewrite([27(8)])]. 74 $F. [para(28(a,1),29(a,1,2)),rewrite([58(3)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=32. Generated=354. Kept=68. proofs=1. Usable=32. Sos=28. Demods=22. Limbo=3, Disabled=13. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=285. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=26 (3 lex), Back_demodulated=3. Back_unit_deleted=0. Demod_attempts=2385. Demod_rewrites=243. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=16. Nonunit_bsub_feature_tests=21. Megabytes=0.07. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 4990 exit (max_proofs) Sat Jul 14 17:42:19 2007