============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11677 was started by mccune on cleo.thornwood, Sat Aug 12 21:22:12 2006 The command was "/home/mccune/bin/prover9 -f dep-2b.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file dep-2b.in assign(order,kbo). formulas(sos). f(x,x,y) = x # label(majority). f(x,y,z) = f(z,x,y) # label(2a). f(f(x,w,y),w,z) = f(x,w,f(y,w,z)) # label(associativity). end_of_list. formulas(goals). f(x,y,z) = f(x,z,y) # answer(2b). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 f(x,y,z) = f(x,z,y) # answer(2b). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). f(x,x,y) = x # label(majority). [assumption]. f(x,y,z) = f(z,x,y) # label(2a). [assumption]. f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). [assumption]. f(c1,c3,c2) != f(c1,c2,c3) # answer(2b). [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: Function symbol KB weights: c1=1. c2=1. c3=1. f=1. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, f ]). Skipping inverse_order, because term ordering is KBO. Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 2 f(x,x,y) = x # label(majority). [assumption]. 3 f(x,y,z) = f(z,x,y) # label(2a). [assumption]. 5 f(x,y,f(z,y,u)) = f(y,u,f(x,y,z)). [copy(4),rewrite(3(2,R)),flip(a)]. 6 f(c1,c3,c2) != f(c1,c2,c3) # answer(2b). [deny(1)]. end_of_list. formulas(demodulators). 2 f(x,x,y) = x # label(majority). [assumption]. 3 f(x,y,z) = f(z,x,y) # label(2a). [assumption]. % (lex-dep) end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=6): 2 f(x,x,y) = x # label(majority). [assumption]. given #2 (I,wt=9): 3 f(x,y,z) = f(z,x,y) # label(2a). [assumption]. given #3 (I,wt=15): 5 f(x,y,f(z,y,u)) = f(y,u,f(x,y,z)). [copy(4),rewrite(3(2,R)),flip(a)]. given #4 (I,wt=9): 6 f(c1,c3,c2) != f(c1,c2,c3) # answer(2b). [deny(1)]. given #5 (T,wt=6): 7 f(x,y,y) = y. [para(3(a,1),2(a,1))]. given #6 (A,wt=6): 8 f(x,y,x) = x. [para(3(a,2),2(a,1))]. given #7 (F,wt=12): 19 f(x,y,f(z,x,y)) = f(z,x,y). [para(8(a,1),5(a,1,3)),flip(a)]. given #8 (F,wt=12): 21 f(x,y,f(x,y,z)) = f(y,z,x). [para(8(a,1),5(a,2,3))]. given #9 (T,wt=12): 22 f(x,f(y,z,x),z) = f(y,z,x). [para(19(a,1),3(a,1)),rewrite(3(3)),flip(a)]. given #10 (T,wt=12): 23 f(x,y,f(y,z,x)) = f(z,x,y). [para(3(a,1),19(a,1,3))]. given #11 (A,wt=15): 9 f(x,f(y,x,z),u) = f(x,z,f(u,x,y)). [para(5(a,1),3(a,1)),rewrite(3(4)),flip(a)]. given #12 (F,wt=15): 10 f(x,f(y,z,u),z) = f(y,z,f(u,z,x)). [para(5(a,2),3(a,2))]. given #13 (F,wt=15): 11 f(x,y,f(z,u,y)) = f(y,z,f(x,y,u)). [para(3(a,1),5(a,1,3))]. given #14 (T,wt=15): 12 f(x,y,f(z,x,u)) = f(z,x,f(x,y,u)). [para(3(a,2),5(a,1,3)),flip(a)]. given #15 (T,wt=15): 13 f(x,y,f(z,u,x)) = f(u,x,f(z,x,y)). [para(3(a,1),5(a,2,3)),flip(a)]. given #16 (A,wt=15): 14 f(x,y,f(z,y,u)) = f(y,u,f(y,z,x)). [para(3(a,2),5(a,2,3))]. given #17 (F,wt=15): 18 f(x,y,f(z,y,f(x,y,z))) = f(x,y,z). [para(7(a,1),5(a,2))]. given #18 (F,wt=15): 29 f(x,y,f(z,x,u)) = f(x,y,f(x,u,z)). [para(5(a,1),21(a,1,3)),rewrite(28(3),9(4)),flip(a)]. given #19 (T,wt=15): 43 f(x,y,f(z,x,f(x,z,y))) = f(z,x,y). [para(23(a,1),21(a,2)),rewrite(3(3),34(3),3(3,R),9(3),3(2),9(2))]. given #20 (T,wt=12): 323 f(x,y,f(x,z,y)) = f(x,y,z). [back_rewrite(232),rewrite(293(3))]. given #21 (A,wt=21): 15 f(x,y,f(y,z,f(u,y,v))) = f(y,z,f(y,v,f(x,y,u))). [para(5(a,1),5(a,1,3)),rewrite(9(6),3(5,R))]. given #22 (F,wt=9): 335 f(x,y,z) = f(z,y,x). [para(323(a,1),3(a,1)),rewrite(3(3),44(3),326(3))]. ============================== PROOF ================================= % Proof 1 at 0.09 (+ 0.00) seconds: 2b. % Length of proof is 29. % Level of proof is 12. % Maximum clause weight is 18. % Given clauses 22. 1 f(x,y,z) = f(x,z,y) # answer(2b). [goal]. 2 f(x,x,y) = x # label(majority). [assumption]. 3 f(x,y,z) = f(z,x,y) # label(2a). [assumption]. 4 f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). [assumption]. 5 f(x,y,f(z,y,u)) = f(y,u,f(x,y,z)). [copy(4),rewrite(3(2,R)),flip(a)]. 6 f(c1,c3,c2) != f(c1,c2,c3) # answer(2b). [deny(1)]. 7 f(x,y,y) = y. [para(3(a,1),2(a,1))]. 8 f(x,y,x) = x. [para(3(a,2),2(a,1))]. 9 f(x,f(y,x,z),u) = f(x,z,f(u,x,y)). [para(5(a,1),3(a,1)),rewrite(3(4)),flip(a)]. 13 f(x,y,f(z,u,x)) = f(u,x,f(z,x,y)). [para(3(a,1),5(a,2,3)),flip(a)]. 18 f(x,y,f(z,y,f(x,y,z))) = f(x,y,z). [para(7(a,1),5(a,2))]. 19 f(x,y,f(z,x,y)) = f(z,x,y). [para(8(a,1),5(a,1,3)),flip(a)]. 21 f(x,y,f(x,y,z)) = f(y,z,x). [para(8(a,1),5(a,2,3))]. 22 f(x,f(y,z,x),z) = f(y,z,x). [para(19(a,1),3(a,1)),rewrite(3(3)),flip(a)]. 23 f(x,y,f(y,z,x)) = f(z,x,y). [para(3(a,1),19(a,1,3))]. 34 f(x,f(x,y,z),z) = f(y,z,x). [para(3(a,1),22(a,1,2))]. 43 f(x,y,f(z,x,f(x,z,y))) = f(z,x,y). [para(23(a,1),21(a,2)),rewrite(3(3),34(3),3(3,R),9(3),3(2),9(2))]. 44 f(x,f(y,z,x),u) = f(x,y,f(u,x,z)). [para(3(a,1),9(a,1,2))]. 45 f(x,f(x,y,z),u) = f(x,y,f(u,x,z)). [para(3(a,2),9(a,1,2))]. 147 f(x,y,f(z,y,f(z,x,y))) = f(z,x,y). [para(13(a,1),7(a,1))]. 232 f(x,y,f(z,y,f(x,z,f(x,y,z)))) = f(x,y,z). [para(18(a,1),21(a,2)),rewrite(3(5),9(5),7(5),3(4),3(4),45(4),3(3),45(3))]. 293 f(x,y,f(z,x,f(z,y,x))) = f(z,x,y). [para(3(a,2),43(a,1,3,3))]. 298 f(x,y,f(x,z,f(y,z,x))) = f(z,x,y). [para(5(a,2),43(a,1,3))]. 323 f(x,y,f(x,z,y)) = f(x,y,z). [back_rewrite(232),rewrite(293(3))]. 325 f(x,y,f(z,y,x)) = f(z,x,y). [back_rewrite(147),rewrite(323(2))]. 326 f(x,y,f(y,x,z)) = f(z,x,y). [back_rewrite(298),rewrite(325(2))]. 335 f(x,y,z) = f(z,y,x). [para(323(a,1),3(a,1)),rewrite(3(3),44(3),326(3))]. 449 f(x,y,z) = f(x,z,y). [para(335(a,1),3(a,1))]. 450 $F # answer(2b). [resolve(449,a,6,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=22. Generated=1788. Kept=447. proofs=1. Usable=19. Sos=358. Demods=101. Limbo=0, Disabled=73. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=1341. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=170 (3 lex), Back_demodulated=69. Back_unit_deleted=0. Demod_attempts=14280. Demod_rewrites=3778. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.38. User_CPU=0.09, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11677 exit (max_proofs) Sat Aug 12 21:22:12 2006