============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 10612 was started by mccune on cleo.thornwood, Sat Aug 12 20:57:19 2006 The command was "/home/mccune/bin/prover9 -f rp-ident.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file rp-ident.in assign(order,kbo). formulas(sos). (x * e) * x = x. x * (x * y) = y. (x * y) * (z * u) = (x * z) * (y * u). ((x * x) * x) * x = e. end_of_list. formulas(goals). ((x * y) * z) * u = ((u * y) * z) * x. end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 ((x * y) * z) * u = ((u * y) * z) * x. [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). (x * e) * x = x. [assumption]. x * (x * y) = y. [assumption]. (x * y) * (z * u) = (x * z) * (y * u). [assumption]. ((x * x) * x) * x = e. [assumption]. ((c4 * c2) * c3) * c1 != ((c1 * c2) * c3) * c4. [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: e=1. c1=1. c2=1. c3=1. c4=1. *=1. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ e, c1, c2, c3, c4, * ]). 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 (x * e) * x = x. [assumption]. 3 x * (x * y) = y. [assumption]. 4 (x * y) * (z * u) = (x * z) * (y * u). [assumption]. 5 ((x * x) * x) * x = e. [assumption]. 6 ((c4 * c2) * c3) * c1 != ((c1 * c2) * c3) * c4. [deny(1)]. end_of_list. formulas(demodulators). 2 (x * e) * x = x. [assumption]. 3 x * (x * y) = y. [assumption]. 5 ((x * x) * x) * x = e. [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 2 (x * e) * x = x. [assumption]. given #2 (I,wt=7): 3 x * (x * y) = y. [assumption]. given #3 (I,wt=15): 4 (x * y) * (z * u) = (x * z) * (y * u). [assumption]. given #4 (I,wt=9): 5 ((x * x) * x) * x = e. [assumption]. given #5 (I,wt=15): 6 ((c4 * c2) * c3) * c1 != ((c1 * c2) * c3) * c4. [deny(1)]. given #6 (A,wt=5): 7 e * e = e. [para(2(a,1),2(a,1,1)),rewrite(3(5)),flip(a)]. given #7 (F,wt=9): 16 ((x * x) * x) * e = x. [para(5(a,1),3(a,1,2))]. given #8 (F,wt=13): 8 ((x * y) * x) * (e * y) = x * y. [para(4(a,1),2(a,1))]. given #9 (T,wt=13): 22 (e * x) * (e * y) = e * (x * y). [para(7(a,1),4(a,1,1)),flip(a)]. given #10 (T,wt=11): 40 (e * x) * e = e * (x * e). [para(7(a,1),22(a,1,2))]. given #11 (A,wt=15): 9 ((x * e) * y) * (x * z) = x * (y * z). [para(2(a,1),4(a,1,1)),flip(a)]. given #12 (F,wt=13): 23 (x * e) * (y * e) = (x * y) * e. [para(7(a,1),4(a,1,2)),flip(a)]. given #13 (F,wt=13): 24 x * ((x * x) * x) = (x * x) * x. [para(16(a,1),2(a,1,1))]. given #14 (T,wt=9): 79 x * ((x * e) * e) = x. [para(9(a,1),24(a,2)),rewrite(23(7),23(8),16(6),2(3)),flip(a)]. given #15 (T,wt=9): 80 (x * e) * e = x * x. [para(79(a,1),3(a,1,2)),flip(a)]. given #16 (A,wt=15): 10 (x * (y * e)) * (z * y) = (x * z) * y. [para(2(a,1),4(a,1,2)),flip(a)]. given #17 (F,wt=9): 87 (x * e) * (x * x) = e. [para(80(a,1),3(a,1,2))]. given #18 (F,wt=9): 140 (x * x) * (e * x) = e. [para(87(a,1),4(a,1)),flip(a)]. given #19 (T,wt=9): 146 (x * x) * e = e * x. [para(140(a,1),3(a,1,2))]. given #20 (T,wt=9): 147 (e * (x * x)) * x = e. [para(3(a,1),140(a,1,2)),rewrite(22(5))]. given #21 (A,wt=15): 12 (x * y) * ((x * z) * u) = z * (y * u). [para(3(a,1),4(a,1,1)),flip(a)]. given #22 (F,wt=9): 178 x * ((e * x) * x) = e. [back_rewrite(87),rewrite(172(4))]. given #23 (F,wt=9): 220 (e * x) * x = x * e. [para(178(a,1),3(a,1,2)),flip(a)]. given #24 (T,wt=11): 114 (x * y) * x = e * (y * x). [para(3(a,1),10(a,1,1)),flip(a)]. given #25 (T,wt=11): 152 ((x * e) * e) * (e * x) = e. [para(80(a,2),140(a,1,1))]. given #26 (A,wt=15): 13 (x * y) * (z * (y * u)) = (x * z) * u. [para(3(a,1),4(a,1,2)),flip(a)]. given #27 (F,wt=11): 164 e * (x * e) = x * (e * x). [para(146(a,1),80(a,1,1)),rewrite(114(4),97(7))]. given #28 (F,wt=11): 235 e * ((x * y) * x) = y * x. [para(114(a,2),3(a,1,2))]. given #29 (T,wt=13): 35 e * ((e * x) * y) = x * (e * y). [para(3(a,1),22(a,1,1)),flip(a)]. given #30 (T,wt=13): 36 e * (x * (e * y)) = (e * x) * y. [para(3(a,1),22(a,1,2)),flip(a)]. given #31 (A,wt=17): 19 (((x * y) * (x * y)) * x) * ((x * y) * y) = e. [para(5(a,1),4(a,1)),flip(a)]. given #32 (F,wt=13): 97 (x * x) * (x * y) = x * (e * y). [para(80(a,1),9(a,1,1))]. given #33 (F,wt=13): 100 ((x * x) * y) * e = x * (y * x). [para(80(a,2),9(a,1,2)),rewrite(62(8),23(6))]. given #34 (T,wt=11): 458 (x * x) * y = (y * y) * x. [para(100(a,1),79(a,1,2,1)),rewrite(451(7),293(6),293(5),3(6),235(5))]. given #35 (T,wt=11): 462 x * (y * x) = y * (x * y). [para(100(a,1),220(a,2)),rewrite(293(7),164(5,R),146(4),3(4))]. given #36 (A,wt=21): 31 (((x * y) * x) * z) * ((e * y) * u) = (x * y) * (z * u). [para(8(a,1),4(a,1,1)),flip(a)]. given #37 (F,wt=11): 464 (x * ((y * x) * x)) * y = e. [para(100(a,1),152(a,1,1,1)),rewrite(276(9),253(6))]. given #38 (F,wt=11): 479 ((x * (y * x)) * e) * x = y. [para(458(a,1),3(a,1)),rewrite(422(5),459(5))]. given #39 (T,wt=11): 501 x * (y * (x * y)) = y * x. [para(462(a,1),3(a,1,2))]. given #40 (T,wt=11): 592 (x * ((y * x) * x)) * e = y. [para(464(a,1),3(a,1,2))]. given #41 (A,wt=15): 45 x * (((x * e) * y) * z) = y * (x * z). [para(3(a,1),9(a,1,1)),flip(a)]. given #42 (F,wt=11): 631 (((x * y) * e) * x) * y = x. [para(3(a,1),479(a,1,1,1,2)),rewrite(129(6))]. given #43 (F,wt=11): 676 ((x * e) * y) * y = y * x. [para(501(a,1),9(a,2)),rewrite(3(5))]. given #44 (T,wt=11): 779 ((x * e) * y) * (y * x) = y. [para(3(a,1),631(a,1,1,1,1))]. given #45 (T,wt=13): 101 ((x * y) * x) * e = x * (y * y). [para(80(a,1),9(a,2,2)),rewrite(23(5),23(6))]. given #46 (A,wt=15): 46 ((x * e) * y) * z = x * (y * (x * z)). [para(3(a,1),9(a,1,2))]. given #47 (F,wt=13): 102 x * ((y * e) * e) = x * (y * y). [para(80(a,2),9(a,2,2)),rewrite(9(5)),flip(a)]. given #48 (F,wt=13): 136 ((x * e) * e) * y = (x * x) * y. [para(80(a,1),10(a,2,1)),rewrite(23(5),129(6))]. given #49 (T,wt=13): 142 x * ((x * x) * y) = e * (x * y). [para(87(a,1),9(a,1,1)),flip(a)]. given #50 (T,wt=13): 154 (x * (e * y)) * e = (x * y) * y. [back_rewrite(144),rewrite(146(3))]. given #51 (A,wt=25): 50 (((x * y) * e) * z) * ((x * u) * (y * v)) = (x * y) * (z * (u * v)). [para(4(a,1),9(a,1,2))]. given #52 (F,wt=13): 158 x * ((y * y) * x) = e * (x * y). [para(4(a,1),146(a,1,1)),rewrite(100(5))]. given #53 (F,wt=13): 160 (x * x) * (y * e) = (e * y) * x. [para(146(a,1),9(a,1,2)),rewrite(146(3),114(6),36(5)),flip(a)]. given #54 (T,wt=13): 161 (e * x) * (y * e) = x * (y * x). [para(146(a,1),23(a,1,1)),rewrite(100(9))]. given #55 (T,wt=13): 168 ((x * e) * y) * e = (e * y) * x. [back_rewrite(103),rewrite(160(9))]. given #56 (A,wt=19): 51 x * ((y * z) * (u * v)) = x * ((y * u) * (z * v)). [para(4(a,1),9(a,2,2)),rewrite(9(7))]. given #57 (F,wt=13): 173 (e * x) * (y * e) = y * (x * y). [back_rewrite(143),rewrite(168(7))]. given #58 (F,wt=13): 200 e * (x * (y * e)) = y * (x * e). [para(23(a,1),12(a,1,2)),rewrite(12(5)),flip(a)]. given #59 (T,wt=13): 204 (x * y) * (x * x) = e * (y * e). [para(80(a,1),12(a,1,2))]. given #60 (T,wt=13): 210 x * (y * (e * x)) = (x * y) * e. [para(140(a,1),12(a,1,2)),flip(a)]. given #61 (A,wt=21): 62 ((x * e) * y) * ((z * e) * u) = ((x * z) * e) * (y * u). [para(23(a,1),4(a,1,1)),flip(a)]. given #62 (F,wt=13): 212 (x * y) * (e * x) = x * (y * e). [para(146(a,1),12(a,1,2))]. given #63 (F,wt=13): 216 (x * x) * (y * x) = e * (y * e). [para(147(a,1),12(a,1,2)),rewrite(114(4)),flip(a)]. given #64 (T,wt=13): 223 x * (y * (x * e)) = (e * y) * x. [para(178(a,1),9(a,1,2)),rewrite(168(5),220(6)),flip(a)]. given #65 (T,wt=13): 225 (x * y) * (x * e) = (e * y) * x. [back_rewrite(131),rewrite(223(8))]. given #66 (A,wt=17): 70 ((x * y) * e) * (x * z) = x * ((y * e) * z). [para(23(a,1),9(a,1,1))]. given #67 (F,wt=13): 259 e * (x * (y * y)) = (y * x) * e. [back_rewrite(53),rewrite(238(4))]. given #68 (F,wt=13): 284 (x * (y * e)) * y = (x * y) * e. [para(79(a,1),13(a,1,2))]. given #69 (T,wt=13): 377 (x * (e * y)) * x = y * (e * x). [para(35(a,1),114(a,2))]. given #70 (T,wt=13): 421 x * (e * (x * y)) = (x * x) * y. [para(3(a,1),97(a,1,2)),flip(a)]. given #71 (A,wt=17): 88 ((x * e) * y) * (e * z) = (x * x) * (y * z). [para(80(a,1),4(a,1,1)),flip(a)]. given #72 (F,wt=13): 430 (x * (e * x)) * e = e * (x * x). [para(97(a,1),146(a,1,1))]. given #73 (F,wt=13): 440 (x * (y * y)) * y = (x * e) * e. [back_rewrite(359),rewrite(434(5))]. given #74 (T,wt=13): 442 x * ((y * x) * y) = (x * x) * y. [para(100(a,1),2(a,1,1)),rewrite(12(5))]. given #75 (T,wt=13): 488 ((x * e) * e) * y = (y * y) * x. [para(80(a,2),458(a,1,1))]. given #76 (A,wt=17): 90 ((x * e) * e) * (y * z) = (x * y) * (x * z). [para(80(a,2),4(a,1,1))]. given #77 (F,wt=13): 499 e * ((x * y) * e) = y * (x * x). [para(458(a,1),235(a,1,2,1)),rewrite(493(5))]. given #78 (F,wt=13): 502 (x * y) * y = x * ((x * y) * x). [para(3(a,1),462(a,1,2))]. given #79 (T,wt=13): 520 (x * y) * y = x * (e * (y * x)). [para(114(a,1),462(a,1,2)),rewrite(3(7)),flip(a)]. given #80 (T,wt=13): 528 (x * x) * x = y * ((x * y) * y). [para(462(a,1),462(a,1,2)),rewrite(13(4))]. given #81 (A,wt=17): 91 (x * y) * ((z * e) * e) = (x * z) * (y * z). [para(80(a,2),4(a,1,2))]. given #82 (F,wt=13): 658 ((x * ((y * e) * x)) * y) * x = e. [para(36(a,1),479(a,1,1,1,2)),rewrite(293(7),501(5),13(10))]. given #83 (F,wt=13): 667 e * (x * x) = y * ((x * y) * y). [para(464(a,1),479(a,1,1,1,2)),rewrite(169(5),22(5))]. given #84 (T,wt=13): 669 x * ((x * y) * y) = (x * y) * x. [para(3(a,1),501(a,1,2,2))]. given #85 (T,wt=13): 695 (x * y) * (y * x) = x * (e * y). [para(97(a,1),501(a,2)),rewrite(204(5),398(7),527(7))]. given #86 (A,wt=15): 92 ((x * y) * e) * e = (x * x) * (y * y). [para(80(a,2),4(a,1))]. given #87 (F,wt=13): 697 ((x * y) * y) * e = (y * e) * x. [para(501(a,1),100(a,2,2)),rewrite(293(5),293(4),3(5),633(4),293(8),370(8))]. given #88 (F,wt=13): 700 (x * y) * y = y * ((x * x) * x). [para(462(a,1),501(a,1,2,2)),rewrite(13(4)),flip(a)]. given #89 (T,wt=13): 740 x * ((e * y) * x) = y * (x * e). [para(23(a,1),45(a,1,2)),rewrite(168(5),200(9))]. given #90 (T,wt=13): 829 ((x * x) * y) * y = y * (x * e). [para(80(a,1),676(a,1,1,1))]. given #91 (A,wt=15): 104 (x * (y * e)) * e = (x * e) * (y * y). [para(80(a,1),23(a,1,2)),flip(a)]. given #92 (F,wt=13): 830 ((e * x) * y) * y = y * (x * x). [para(146(a,1),676(a,1,1,1))]. given #93 (F,wt=13): 856 (x * y) * y = y * (e * (x * x)). [para(631(a,1),676(a,1,1,1)),rewrite(169(7),22(7))]. given #94 (T,wt=13): 866 ((e * x) * y) * (y * (x * x)) = y. [para(146(a,1),779(a,1,1,1))]. given #95 (T,wt=13): 976 (x * e) * (y * x) = x * (y * e). [para(2(a,1),46(a,2,2,2)),rewrite(794(6)),flip(a)]. given #96 (A,wt=17): 115 (x * ((y * z) * e)) * z = (x * y) * (y * z). [para(3(a,1),10(a,1,2))]. given #97 (F,wt=13): 1005 x * ((x * y) * e) = y * (e * x). [para(220(a,1),46(a,2,2)),rewrite(297(6),114(4),844(6),7(3)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.99 (+ 0.02) seconds. % Length of proof is 47. % Level of proof is 19. % Maximum clause weight is 23. % Given clauses 97. 1 ((x * y) * z) * u = ((u * y) * z) * x. [goal]. 2 (x * e) * x = x. [assumption]. 3 x * (x * y) = y. [assumption]. 4 (x * y) * (z * u) = (x * z) * (y * u). [assumption]. 5 ((x * x) * x) * x = e. [assumption]. 6 ((c4 * c2) * c3) * c1 != ((c1 * c2) * c3) * c4. [deny(1)]. 7 e * e = e. [para(2(a,1),2(a,1,1)),rewrite(3(5)),flip(a)]. 9 ((x * e) * y) * (x * z) = x * (y * z). [para(2(a,1),4(a,1,1)),flip(a)]. 10 (x * (y * e)) * (z * y) = (x * z) * y. [para(2(a,1),4(a,1,2)),flip(a)]. 12 (x * y) * ((x * z) * u) = z * (y * u). [para(3(a,1),4(a,1,1)),flip(a)]. 13 (x * y) * (z * (y * u)) = (x * z) * u. [para(3(a,1),4(a,1,2)),flip(a)]. 16 ((x * x) * x) * e = x. [para(5(a,1),3(a,1,2))]. 22 (e * x) * (e * y) = e * (x * y). [para(7(a,1),4(a,1,1)),flip(a)]. 23 (x * e) * (y * e) = (x * y) * e. [para(7(a,1),4(a,1,2)),flip(a)]. 24 x * ((x * x) * x) = (x * x) * x. [para(16(a,1),2(a,1,1))]. 36 e * (x * (e * y)) = (e * x) * y. [para(3(a,1),22(a,1,2)),flip(a)]. 46 ((x * e) * y) * z = x * (y * (x * z)). [para(3(a,1),9(a,1,2))]. 62 ((x * e) * y) * ((z * e) * u) = ((x * z) * e) * (y * u). [para(23(a,1),4(a,1,1)),flip(a)]. 79 x * ((x * e) * e) = x. [para(9(a,1),24(a,2)),rewrite(23(7),23(8),16(6),2(3)),flip(a)]. 80 (x * e) * e = x * x. [para(79(a,1),3(a,1,2)),flip(a)]. 84 x * ((((x * e) * e) * e) * y) = (x * e) * (x * y). [para(79(a,1),9(a,1,1)),flip(a)]. 87 (x * e) * (x * x) = e. [para(80(a,1),3(a,1,2))]. 97 (x * x) * (x * y) = x * (e * y). [para(80(a,1),9(a,1,1))]. 100 ((x * x) * y) * e = x * (y * x). [para(80(a,2),9(a,1,2)),rewrite(62(8),23(6))]. 103 ((x * e) * y) * e = (x * x) * (y * e). [para(80(a,1),23(a,1,1)),flip(a)]. 114 (x * y) * x = e * (y * x). [para(3(a,1),10(a,1,1)),flip(a)]. 140 (x * x) * (e * x) = e. [para(87(a,1),4(a,1)),flip(a)]. 146 (x * x) * e = e * x. [para(140(a,1),3(a,1,2))]. 160 (x * x) * (y * e) = (e * y) * x. [para(146(a,1),9(a,1,2)),rewrite(146(3),114(6),36(5)),flip(a)]. 164 e * (x * e) = x * (e * x). [para(146(a,1),80(a,1,1)),rewrite(114(4),97(7))]. 168 ((x * e) * y) * e = (e * y) * x. [back_rewrite(103),rewrite(160(9))]. 172 (x * e) * (x * y) = x * ((e * x) * y). [back_rewrite(84),rewrite(168(6),7(3)),flip(a)]. 178 x * ((e * x) * x) = e. [back_rewrite(87),rewrite(172(4))]. 189 x * (y * ((z * x) * u)) = (z * y) * u. [para(3(a,1),12(a,1,2)),flip(a)]. 190 ((x * y) * z) * (((x * u) * v) * w) = (u * (y * v)) * (z * w). [para(12(a,1),4(a,1,1)),flip(a)]. 210 x * (y * (e * x)) = (x * y) * e. [para(140(a,1),12(a,1,2)),flip(a)]. 220 (e * x) * x = x * e. [para(178(a,1),3(a,1,2)),flip(a)]. 293 (x * (y * z)) * (u * v) = z * ((y * (x * u)) * v). [para(13(a,1),12(a,1,1)),rewrite(190(6))]. 297 (x * e) * (y * (x * z)) = ((e * x) * y) * z. [para(220(a,1),13(a,1,1))]. 462 x * (y * x) = y * (x * y). [para(100(a,1),220(a,2)),rewrite(293(7),164(5,R),146(4),3(4))]. 501 x * (y * (x * y)) = y * x. [para(462(a,1),3(a,1,2))]. 676 ((x * e) * y) * y = y * x. [para(501(a,1),9(a,2)),rewrite(3(5))]. 844 ((x * (y * x)) * z) * z = z * ((x * x) * y). [para(100(a,1),676(a,1,1,1))]. 1005 x * ((x * y) * e) = y * (e * x). [para(220(a,1),46(a,2,2)),rewrite(297(6),114(4),844(6),7(3)),flip(a)]. 1513 ((x * e) * y) * (z * e) = e * (z * ((e * y) * x)). [para(168(a,1),9(a,1,2)),rewrite(168(5),114(8)),flip(a)]. 3830 ((x * y) * z) * u = ((u * y) * z) * x. [para(1005(a,1),62(a,2,2)),rewrite(23(9),1513(8),293(7),210(5),189(7),13(10))]. 3831 $F. [resolve(3830,a,6,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=97. Generated=26039. Kept=3829. proofs=1. Usable=77. Sos=2519. Demods=1324. Limbo=6, Disabled=1231. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=22210. Back_subsumed=135. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=2198 (5 lex), Back_demodulated=1091. Back_unit_deleted=0. Demod_attempts=570672. Demod_rewrites=87793. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=2.88. User_CPU=0.99, System_CPU=0.02, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 10612 exit (max_proofs) Sat Aug 12 20:57:20 2006