============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13954 was started by mccune on cleo.thornwood, Mon Jun 19 17:18:28 2006 The command was "/home/mccune/bin/prover9 -f dist-short-long.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file dist-short-long.in assign(order,kbo). set(lex_order_vars). clauses(sos). f(x,x,y) = x # label(majority). f(x,y,z) = f(z,x,y) # label(2a). f(x,y,z) = f(x,z,y) # label(2b). f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). f(f(x,y,z),u,v) = f(x,f(y,u,v),f(z,u,v)) # label(dist_short). end_of_list. clauses(goals). f(f(x,y,z),u,E) = f(f(x,u,E),f(y,u,E),f(z,u,E)) # answer(dist_long). end_of_list. ============================== end of input ========================== ============================== PROCESS GOALS ========================= % Each goal clause was negated; the result (to be placed in sos): clauses(negated_goals). f(f(c1,c4,E),f(c2,c4,E),f(c3,c4,E)) != f(f(c1,c2,c3),c4,E) # answer(dist_long). end_of_list. ============================== end of process goals ================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 f(x,x,y) = x # label(majority). [input]. 2 f(x,y,z) = f(z,x,y) # label(2a). [input]. 3 f(x,y,z) = f(x,z,y) # label(2b). [input]. 4 f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). [input]. 5 f(f(x,y,z),u,v) = f(x,f(y,u,v),f(z,u,v)) # label(dist_short). [input]. 6 f(f(c1,c4,E),f(c2,c4,E),f(c3,c4,E)) != f(f(c1,c2,c3),c4,E) # answer(dist_long). [clausify]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). Auto_denials: no changes. Term ordering decisions: Function symbol KB weights: E=1. c1=1. c2=1. c3=1. c4=1. f=1. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ E, c1, c2, c3, c4, 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: clauses(usable). end_of_list. clauses(sos). 7 f(x,x,y) = x # label(majority). [input]. 8 f(x,y,z) = f(z,x,y) # label(2a). [input]. 9 f(x,y,z) = f(x,z,y) # label(2b). [input]. 10 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)) # label(associativity). [copy(4),demod(8(2),8(2),8(3,R),9(3))]. 11 f(x,f(y,z,u),f(v,z,u)) = f(z,u,f(x,y,v)) # label(dist_short). [copy(5),demod(8(2),8(2)),flip(a)]. 12 f(f(E,c1,c4),f(E,c2,c4),f(E,c3,c4)) != f(E,c4,f(c1,c2,c3)) # answer(dist_long). [copy(6),demod(8(4),8(8),8(12),8(20),9(20))]. end_of_list. clauses(demodulators). 7 f(x,x,y) = x # label(majority). [input]. 8 f(x,y,z) = f(z,x,y) # label(2a). [input]. % (lex-dep) 9 f(x,y,z) = f(x,z,y) # label(2b). [input]. % (lex-dep) 11 f(x,f(y,z,u),f(v,z,u)) = f(z,u,f(x,y,v)) # label(dist_short). [copy(5),demod(8(2),8(2)),flip(a)]. end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=6): 7 f(x,x,y) = x # label(majority). [input]. given #2 (I,wt=9): 8 f(x,y,z) = f(z,x,y) # label(2a). [input]. given #3 (I,wt=9): 9 f(x,y,z) = f(x,z,y) # label(2b). [input]. given #4 (I,wt=15): 10 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)) # label(associativity). [copy(4),demod(8(2),8(2),8(3,R),9(3))]. given #5 (I,wt=18): 11 f(x,f(y,z,u),f(v,z,u)) = f(z,u,f(x,y,v)) # label(dist_short). [copy(5),demod(8(2),8(2)),flip(a)]. given #6 (I,wt=21): 12 f(f(E,c1,c4),f(E,c2,c4),f(E,c3,c4)) != f(E,c4,f(c1,c2,c3)) # answer(dist_long). [copy(6),demod(8(4),8(8),8(12),8(20),9(20))]. given #7 (F,wt=6): 13 f(x,y,y) = y. [para(8(a,1),7(a,1))]. given #8 (F,wt=12): 20 f(x,y,f(x,z,y)) = f(x,z,y). [para(10(a,2),10(a,1)),demod(8(1,R),13(1),8(2),9(2)),flip(a)]. given #9 (T,wt=12): 44 f(x,y,f(x,y,z)) = f(x,y,z). [para(13(a,1),10(a,2,3)),demod(8(1),8(1),8(3),8(3))]. given #10 (T,wt=15): 14 f(x,y,f(x,z,u)) = f(x,z,f(x,y,u)). [para(10(a,2),8(a,1)),demod(8(1,R),9(1),9(3),8(4),9(4))]. given #11 (A,wt=15): 15 f(x,y,f(z,y,u)) = f(z,y,f(x,y,u)). [para(10(a,1),8(a,2)),demod(9(2),8(3))]. given #12 (F,wt=15): 16 f(x,y,f(x,z,u)) = f(x,u,f(x,z,y)). [para(10(a,2),8(a,2)),demod(9(2),8(3),8(3))]. given #13 (F,wt=15): 17 f(x,y,f(x,z,u)) = f(x,u,f(x,y,z)). [para(8(a,1),10(a,1,3)),demod(8(1),9(3),8(4,R),9(4))]. given #14 (T,wt=15): 23 f(x,y,f(z,u,f(x,y,z))) = f(x,y,z). [para(11(a,1),7(a,1)),demod(8(1),8(1),8(2),8(2),8(4),8(4))]. given #15 (T,wt=12): 98 f(x,y,f(z,x,y)) = f(z,x,y). [para(23(a,1),15(a,1)),demod(44(3),8(3,R),9(3)),flip(a)]. given #16 (A,wt=21): 18 f(x,y,f(z,u,f(x,u,v))) = f(x,u,f(x,y,f(z,u,v))). [para(10(a,1),10(a,1,3)),demod(8(1),9(5),8(6,R),9(6))]. given #17 (F,wt=15): 24 f(x,y,f(z,u,x)) = f(z,x,f(u,x,y)). [para(7(a,1),11(a,1,3)),demod(9(2)),flip(a)]. given #18 (F,wt=15): 46 f(x,y,f(z,x,u)) = f(z,x,f(x,y,u)). [back_demod(36),demod(44(2)),flip(a)]. given #19 (T,wt=15): 52 f(x,y,f(z,u,f(x,z,y))) = f(x,z,y). [back_demod(33),demod(8(1),8(2),48(4),7(2),8(2),20(2),8(2),8(4,R),9(4)),flip(a)]. given #20 (T,wt=15): 58 f(x,y,f(x,z,f(y,u,z))) = f(x,y,z). [para(14(a,1),11(a,1)),demod(8(1,R),9(1),9(2),8(4),7(4),8(4))]. given #21 (A,wt=21): 19 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,y,f(x,z,v))). [para(10(a,2),10(a,1,3)),demod(8(1,R),9(1),9(4),9(5),8(6,R),9(6))]. given #22 (F,wt=15): 60 f(x,y,f(z,y,f(x,z,u))) = f(x,z,y). [para(11(a,1),14(a,1)),demod(8(1),7(1),8(2),8(2),8(3),8(4,R),9(4)),flip(a)]. given #23 (F,wt=15): 78 f(x,y,f(x,z,f(y,z,u))) = f(x,y,z). [para(16(a,1),11(a,1)),demod(8(1),9(1),8(4),7(4),8(4),9(4))]. given #24 (T,wt=15): 80 f(x,y,f(z,y,f(z,x,u))) = f(z,x,y). [para(11(a,1),16(a,1)),demod(8(1),7(1),8(2),8(2),8(3,R),9(3),8(4,R),9(4)),flip(a)]. given #25 (T,wt=15): 88 f(x,y,f(z,u,f(z,x,y))) = f(z,x,y). [para(8(a,1),23(a,1)),demod(8(1),8(3),8(3),8(4))]. given #26 (A,wt=21): 22 f(x,f(y,z,u),f(x,y,v)) = f(x,v,f(y,u,f(x,y,z))). [para(10(a,2),10(a,2,3)),demod(8(2),8(2),8(6,R),9(6))]. given #27 (F,wt=15): 89 f(x,y,f(z,u,f(x,y,u))) = f(x,y,u). [para(8(a,2),23(a,1,3)),demod(9(2))]. given #28 (F,wt=15): 96 f(x,y,f(y,z,f(x,z,u))) = f(x,y,z). [para(11(a,1),23(a,1,3)),demod(8(1))]. given #29 (T,wt=15): 99 f(x,y,f(z,x,u)) = f(x,u,f(z,x,y)). [para(15(a,1),23(a,2)),demod(8(1,R),9(1),8(2,R),9(2),8(4,R),9(4),49(4),8(2),8(2),93(4),8(4,R),9(4))]. given #30 (T,wt=15): 111 f(x,y,f(z,x,f(z,y,u))) = f(z,x,y). [para(18(a,1),10(a,2)),demod(8(2,R),9(2),29(3),7(1),8(1),8(3,R),9(3)),flip(a)]. given #31 (A,wt=18): 26 f(x,f(y,z,u),f(y,z,v)) = f(y,z,f(x,u,v)). [para(11(a,1),8(a,1)),demod(8(3),8(3),8(4),8(4),8(5,R)),flip(a)]. given #32 (F,wt=15): 155 f(x,y,f(z,u,y)) = f(z,y,f(x,u,y)). [para(24(a,1),8(a,2)),demod(9(2),8(3))]. given #33 (F,wt=15): 181 f(x,y,f(y,z,f(x,u,z))) = f(x,y,z). [para(52(a,1),20(a,1,3)),demod(9(4),161(4),9(1),8(2,R),9(2),52(6))]. given #34 (T,wt=15): 191 f(x,y,f(x,z,f(z,y,u))) = f(x,z,y). [para(8(a,1),58(a,1)),demod(8(1),8(3),8(3),9(4))]. given #35 (T,wt=15): 376 f(x,f(y,z,u),f(y,x,z)) = f(y,x,z). [para(22(a,2),24(a,2)),demod(8(2),338(3),78(3),8(2),8(3)),flip(a)]. given #36 (A,wt=18): 27 f(x,f(y,z,u),f(z,u,v)) = f(z,u,f(y,v,x)). [para(11(a,1),8(a,2)),demod(8(2),8(2),8(3),8(4),8(4))]. given #37 (F,wt=15): 470 f(x,y,f(z,u,x)) = f(u,x,f(z,x,y)). [para(99(a,1),111(a,2)),demod(9(3),8(4,R),9(4),458(5),8(3)),flip(a)]. given #38 (F,wt=15): 530 f(x,y,f(x,z,f(u,z,y))) = f(x,z,y). [para(44(a,1),155(a,1,3)),demod(13(3),501(5),480(4)),flip(a)]. given #39 (T,wt=15): 551 f(x,y,f(x,z,f(z,u,y))) = f(x,z,y). [para(26(a,1),155(a,1)),demod(480(3),13(1),8(4,R),9(4),501(5),480(4)),flip(a)]. given #40 (T,wt=15): 588 f(x,y,f(z,u,y)) = f(u,y,f(x,z,y)). [para(13(a,1),27(a,1,3)),demod(9(2),8(3))]. given #41 (A,wt=18): 28 f(x,f(y,z,u),f(y,u,v)) = f(y,u,f(x,z,v)). [para(8(a,1),11(a,1,2)),demod(8(2),9(2),8(5,R),9(5))]. given #42 (F,wt=18): 29 f(x,f(y,z,u),f(v,y,z)) = f(y,z,f(v,x,u)). [para(8(a,1),11(a,1)),demod(8(2),8(2),8(3,R),8(4))]. given #43 (F,wt=18): 101 f(x,y,f(z,f(x,y,z),f(x,u,v))) = f(x,y,z). [para(23(a,1),23(a,1,3,3)),demod(8(4),8(4),48(4),8(2),8(2),23(7))]. given #44 (T,wt=18): 201 f(x,y,f(x,z,f(y,u,f(y,z,v)))) = f(x,y,z). [para(58(a,1),23(a,1,3,3)),demod(9(1),8(4),8(4),28(4),8(2,R),9(2),9(5),78(7))]. given #45 (T,wt=18): 279 f(x,y,f(y,z,f(x,u,f(x,z,v)))) = f(x,y,z). [para(10(a,1),60(a,1,3,3)),demod(9(1),8(2,R),9(2),8(3,R),9(3),9(5))]. given #46 (A,wt=21): 30 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,v,f(z,u,w))). [para(11(a,1),10(a,1,3)),demod(8(2,R),9(2),8(4,R),9(4),27(4),9(2),8(6),8(6),8(7),27(7),9(5),27(7),9(5))]. given #47 (F,wt=18): 280 f(x,y,f(y,z,f(z,u,f(x,z,v)))) = f(x,y,z). [para(10(a,2),60(a,1,3,3)),demod(8(3,R),9(3),9(5))]. given #48 (F,wt=18): 294 f(x,y,f(x,z,f(z,u,f(y,z,v)))) = f(x,y,z). [para(10(a,2),78(a,1,3,3))]. given #49 (T,wt=18): 479 f(x,y,f(z,u,f(x,v,y))) = f(x,y,f(z,v,u)). [para(20(a,1),26(a,1,2)),demod(28(3),9(4)),flip(a)]. given #50 (T,wt=18): 480 f(x,y,f(z,u,f(x,y,v))) = f(x,y,f(z,u,v)). [para(20(a,1),26(a,1,3)),demod(9(2),26(3),9(3)),flip(a)]. given #51 (A,wt=24): 32 f(x,f(y,z,u),f(x,v,f(z,u,w))) = f(x,v,f(z,u,f(x,y,w))). [para(11(a,1),10(a,2,3)),demod(8(2),8(2),8(3,R),9(3),9(5),8(7,R),9(7))]. given #52 (F,wt=15): 995 f(x,y,f(x,z,f(u,y,z))) = f(x,y,z). [para(60(a,1),32(a,1,3)),demod(924(3),564(7))]. given #53 (F,wt=18): 485 f(x,y,f(z,u,f(v,x,y))) = f(x,y,f(z,v,u)). [para(98(a,1),26(a,1,2)),demod(27(3),8(1),9(4)),flip(a)]. given #54 (T,wt=18): 564 f(x,y,f(z,y,f(x,u,f(x,z,v)))) = f(x,z,y). [para(60(a,1),191(a,2)),demod(9(5),495(6),8(3,R),9(3),59(5),9(2))]. given #55 (T,wt=18): 574 f(x,y,f(x,z,f(y,u,f(y,v,z)))) = f(x,y,z). [para(16(a,1),376(a,1,2)),demod(8(3,R),9(3),338(4),8(5,R),9(5))]. given #56 (A,wt=27): 35 f(x,f(y,z,f(u,v,w)),f(u,v,f(z,v,w))) = f(z,f(u,v,w),f(x,y,v)). [para(10(a,1),11(a,1,3)),demod(8(3))]. ============================== PROOF ================================= % Proof 1 at 1.10 (+ 0.02) seconds: dist_long. % Length of proof is 22. % Level of proof is 6. % Maximum clause weight is 27. % Given clauses 56. 4 f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). [input]. 5 f(f(x,y,z),u,v) = f(x,f(y,u,v),f(z,u,v)) # label(dist_short). [input]. 6 f(f(c1,c4,E),f(c2,c4,E),f(c3,c4,E)) != f(f(c1,c2,c3),c4,E) # answer(dist_long). [clausify]. 7 f(x,x,y) = x # label(majority). [input]. 8 f(x,y,z) = f(z,x,y) # label(2a). [input]. 9 f(x,y,z) = f(x,z,y) # label(2b). [input]. 10 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)) # label(associativity). [copy(4),demod(8(2),8(2),8(3,R),9(3))]. 11 f(x,f(y,z,u),f(v,z,u)) = f(z,u,f(x,y,v)) # label(dist_short). [copy(5),demod(8(2),8(2)),flip(a)]. 12 f(f(E,c1,c4),f(E,c2,c4),f(E,c3,c4)) != f(E,c4,f(c1,c2,c3)) # answer(dist_long). [copy(6),demod(8(4),8(8),8(12),8(20),9(20))]. 13 f(x,y,y) = y. [para(8(a,1),7(a,1))]. 20 f(x,y,f(x,z,y)) = f(x,z,y). [para(10(a,2),10(a,1)),demod(8(1,R),13(1),8(2),9(2)),flip(a)]. 26 f(x,f(y,z,u),f(y,z,v)) = f(y,z,f(x,u,v)). [para(11(a,1),8(a,1)),demod(8(3),8(3),8(4),8(4),8(5,R)),flip(a)]. 27 f(x,f(y,z,u),f(z,u,v)) = f(z,u,f(y,v,x)). [para(11(a,1),8(a,2)),demod(8(2),8(2),8(3),8(4),8(4))]. 28 f(x,f(y,z,u),f(y,u,v)) = f(y,u,f(x,z,v)). [para(8(a,1),11(a,1,2)),demod(8(2),9(2),8(5,R),9(5))]. 29 f(x,f(y,z,u),f(v,y,z)) = f(y,z,f(v,x,u)). [para(8(a,1),11(a,1)),demod(8(2),8(2),8(3,R),8(4))]. 32 f(x,f(y,z,u),f(x,v,f(z,u,w))) = f(x,v,f(z,u,f(x,y,w))). [para(11(a,1),10(a,2,3)),demod(8(2),8(2),8(3,R),9(3),9(5),8(7,R),9(7))]. 479 f(x,y,f(z,u,f(x,v,y))) = f(x,y,f(z,v,u)). [para(20(a,1),26(a,1,2)),demod(28(3),9(4)),flip(a)]. 684 f(x,f(y,z,f(x,u,v)),f(y,v,f(x,u,v))) = f(x,v,f(y,u,z)). [para(27(a,1),29(a,2)),demod(8(1),9(2),8(3),8(4,R),9(4),8(6),8(7,R),9(7))]. 962 f(x,f(y,z,f(x,u,v)),f(w,y,f(x,u,v))) = f(y,f(x,u,v),f(x,w,z)). [para(11(a,1),32(a,2)),demod(8(3,R),9(3),32(6),9(7))]. 1251 f(x,f(y,z,f(x,u,v)),f(y,w,f(x,u,v))) = f(y,f(x,u,v),f(x,z,w)). [back_demod(962),demod(8(4,R),9(4),9(7))]. 1256 f(x,f(y,z,u),f(y,v,u)) = f(y,u,f(x,v,z)). [back_demod(684),demod(1251(5),9(4))]. 1260 $F # answer(dist_long). [back_demod(12),demod(1256(13),8(9),9(9),479(10),8(6,R),9(6)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=56. Generated=13028. Kept=1253. proofs=1. Usable=49. Sos=897. Demods=640. Denials=0. Limbo=4, Disabled=309. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=11774. Back_subsumed=15. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=895 (2 lex), Back_demodulated=288. Back_unit_deleted=0. Demod_attempts=172920. Demod_rewrites=67163. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=1.30. User_CPU=1.10, System_CPU=0.02, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13954 exit (max_proofs) Mon Jun 19 17:18:29 2006