============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 12987 was started by mccune on cleo.thornwood, Mon Jun 19 16:39:41 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). clauses(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. clauses(goals). ((x * y) * z) * u = ((u * y) * z) * x. end_of_list. ============================== end of input ========================== ============================== PROCESS GOALS ========================= % Each goal clause was negated; the result (to be placed in sos): clauses(negated_goals). ((c4 * c2) * c3) * c1 != ((c1 * c2) * c3) * c4. end_of_list. ============================== end of process goals ================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 (x * e) * x = x. [input]. 2 x * (x * y) = y. [input]. 3 (x * y) * (z * u) = (x * z) * (y * u). [input]. 4 ((x * x) * x) * x = e. [input]. 5 ((c4 * c2) * c3) * c1 != ((c1 * c2) * c3) * c4. [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. *=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: clauses(usable). end_of_list. clauses(sos). 6 (x * e) * x = x. [input]. 7 x * (x * y) = y. [input]. 8 (x * y) * (z * u) = (x * z) * (y * u). [input]. 9 ((x * x) * x) * x = e. [input]. 10 ((c4 * c2) * c3) * c1 != ((c1 * c2) * c3) * c4. [clausify]. end_of_list. clauses(demodulators). 6 (x * e) * x = x. [input]. 7 x * (x * y) = y. [input]. 9 ((x * x) * x) * x = e. [input]. end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 6 (x * e) * x = x. [input]. given #2 (I,wt=7): 7 x * (x * y) = y. [input]. given #3 (I,wt=15): 8 (x * y) * (z * u) = (x * z) * (y * u). [input]. given #4 (I,wt=9): 9 ((x * x) * x) * x = e. [input]. given #5 (I,wt=15): 10 ((c4 * c2) * c3) * c1 != ((c1 * c2) * c3) * c4. [clausify]. given #6 (A,wt=5): 11 e * e = e. [para(6(a,1),6(a,1,1)),demod(7(5)),flip(a)]. given #7 (F,wt=9): 20 ((x * x) * x) * e = x. [para(9(a,1),7(a,1,2))]. given #8 (F,wt=13): 12 ((x * y) * x) * (e * y) = x * y. [para(8(a,1),6(a,1))]. given #9 (T,wt=13): 26 (e * x) * (e * y) = e * (x * y). [para(11(a,1),8(a,1,1)),flip(a)]. given #10 (T,wt=11): 44 (e * x) * e = e * (x * e). [para(11(a,1),26(a,1,2))]. given #11 (A,wt=15): 13 ((x * e) * y) * (x * z) = x * (y * z). [para(6(a,1),8(a,1,1)),flip(a)]. given #12 (F,wt=13): 27 (x * e) * (y * e) = (x * y) * e. [para(11(a,1),8(a,1,2)),flip(a)]. given #13 (F,wt=13): 28 x * ((x * x) * x) = (x * x) * x. [para(20(a,1),6(a,1,1))]. given #14 (T,wt=9): 83 x * ((x * e) * e) = x. [para(13(a,1),28(a,2)),demod(27(7),27(8),20(6),6(3)),flip(a)]. given #15 (T,wt=9): 84 (x * e) * e = x * x. [para(83(a,1),7(a,1,2)),flip(a)]. given #16 (A,wt=15): 14 (x * (y * e)) * (z * y) = (x * z) * y. [para(6(a,1),8(a,1,2)),flip(a)]. given #17 (F,wt=9): 91 (x * e) * (x * x) = e. [para(84(a,1),7(a,1,2))]. given #18 (F,wt=9): 144 (x * x) * (e * x) = e. [para(91(a,1),8(a,1)),flip(a)]. given #19 (T,wt=9): 150 (x * x) * e = e * x. [para(144(a,1),7(a,1,2))]. given #20 (T,wt=9): 151 (e * (x * x)) * x = e. [para(7(a,1),144(a,1,2)),demod(26(5))]. given #21 (A,wt=15): 16 (x * y) * ((x * z) * u) = z * (y * u). [para(7(a,1),8(a,1,1)),flip(a)]. given #22 (F,wt=9): 182 x * ((e * x) * x) = e. [back_demod(91),demod(176(4))]. given #23 (F,wt=9): 224 (e * x) * x = x * e. [para(182(a,1),7(a,1,2)),flip(a)]. given #24 (T,wt=11): 118 (x * y) * x = e * (y * x). [para(7(a,1),14(a,1,1)),flip(a)]. given #25 (T,wt=11): 156 ((x * e) * e) * (e * x) = e. [para(84(a,2),144(a,1,1))]. given #26 (A,wt=15): 17 (x * y) * (z * (y * u)) = (x * z) * u. [para(7(a,1),8(a,1,2)),flip(a)]. given #27 (F,wt=11): 168 e * (x * e) = x * (e * x). [para(150(a,1),84(a,1,1)),demod(118(4),101(7))]. given #28 (F,wt=11): 239 e * ((x * y) * x) = y * x. [para(118(a,2),7(a,1,2))]. given #29 (T,wt=13): 39 e * ((e * x) * y) = x * (e * y). [para(7(a,1),26(a,1,1)),flip(a)]. given #30 (T,wt=13): 40 e * (x * (e * y)) = (e * x) * y. [para(7(a,1),26(a,1,2)),flip(a)]. given #31 (A,wt=17): 23 (((x * y) * (x * y)) * x) * ((x * y) * y) = e. [para(9(a,1),8(a,1)),flip(a)]. given #32 (F,wt=13): 101 (x * x) * (x * y) = x * (e * y). [para(84(a,1),13(a,1,1))]. given #33 (F,wt=13): 104 ((x * x) * y) * e = x * (y * x). [para(84(a,2),13(a,1,2)),demod(66(8),27(6))]. given #34 (T,wt=11): 462 (x * x) * y = (y * y) * x. [para(104(a,1),83(a,1,2,1)),demod(455(7),297(6),297(5),7(6),239(5))]. given #35 (T,wt=11): 466 x * (y * x) = y * (x * y). [para(104(a,1),224(a,2)),demod(297(7),168(5,R),150(4),7(4))]. given #36 (A,wt=21): 35 (((x * y) * x) * z) * ((e * y) * u) = (x * y) * (z * u). [para(12(a,1),8(a,1,1)),flip(a)]. given #37 (F,wt=11): 468 (x * ((y * x) * x)) * y = e. [para(104(a,1),156(a,1,1,1)),demod(280(9),257(6))]. given #38 (F,wt=11): 483 ((x * (y * x)) * e) * x = y. [para(462(a,1),7(a,1)),demod(426(5),463(5))]. given #39 (T,wt=11): 505 x * (y * (x * y)) = y * x. [para(466(a,1),7(a,1,2))]. given #40 (T,wt=11): 596 (x * ((y * x) * x)) * e = y. [para(468(a,1),7(a,1,2))]. given #41 (A,wt=15): 49 x * (((x * e) * y) * z) = y * (x * z). [para(7(a,1),13(a,1,1)),flip(a)]. given #42 (F,wt=11): 635 (((x * y) * e) * x) * y = x. [para(7(a,1),483(a,1,1,1,2)),demod(133(6))]. given #43 (F,wt=11): 680 ((x * e) * y) * y = y * x. [para(505(a,1),13(a,2)),demod(7(5))]. given #44 (T,wt=11): 783 ((x * e) * y) * (y * x) = y. [para(7(a,1),635(a,1,1,1,1))]. given #45 (T,wt=13): 105 ((x * y) * x) * e = x * (y * y). [para(84(a,1),13(a,2,2)),demod(27(5),27(6))]. given #46 (A,wt=15): 50 ((x * e) * y) * z = x * (y * (x * z)). [para(7(a,1),13(a,1,2))]. given #47 (F,wt=13): 106 x * ((y * e) * e) = x * (y * y). [para(84(a,2),13(a,2,2)),demod(13(5)),flip(a)]. given #48 (F,wt=13): 140 ((x * e) * e) * y = (x * x) * y. [para(84(a,1),14(a,2,1)),demod(27(5),133(6))]. given #49 (T,wt=13): 146 x * ((x * x) * y) = e * (x * y). [para(91(a,1),13(a,1,1)),flip(a)]. given #50 (T,wt=13): 158 (x * (e * y)) * e = (x * y) * y. [back_demod(148),demod(150(3))]. given #51 (A,wt=25): 54 (((x * y) * e) * z) * ((x * u) * (y * v)) = (x * y) * (z * (u * v)). [para(8(a,1),13(a,1,2))]. given #52 (F,wt=13): 162 x * ((y * y) * x) = e * (x * y). [para(8(a,1),150(a,1,1)),demod(104(5))]. given #53 (F,wt=13): 164 (x * x) * (y * e) = (e * y) * x. [para(150(a,1),13(a,1,2)),demod(150(3),118(6),40(5)),flip(a)]. given #54 (T,wt=13): 165 (e * x) * (y * e) = x * (y * x). [para(150(a,1),27(a,1,1)),demod(104(9))]. given #55 (T,wt=13): 172 ((x * e) * y) * e = (e * y) * x. [back_demod(107),demod(164(9))]. given #56 (A,wt=19): 55 x * ((y * z) * (u * v)) = x * ((y * u) * (z * v)). [para(8(a,1),13(a,2,2)),demod(13(7))]. given #57 (F,wt=13): 177 (e * x) * (y * e) = y * (x * y). [back_demod(147),demod(172(7))]. given #58 (F,wt=13): 204 e * (x * (y * e)) = y * (x * e). [para(27(a,1),16(a,1,2)),demod(16(5)),flip(a)]. given #59 (T,wt=13): 208 (x * y) * (x * x) = e * (y * e). [para(84(a,1),16(a,1,2))]. given #60 (T,wt=13): 214 x * (y * (e * x)) = (x * y) * e. [para(144(a,1),16(a,1,2)),flip(a)]. given #61 (A,wt=21): 66 ((x * e) * y) * ((z * e) * u) = ((x * z) * e) * (y * u). [para(27(a,1),8(a,1,1)),flip(a)]. given #62 (F,wt=13): 216 (x * y) * (e * x) = x * (y * e). [para(150(a,1),16(a,1,2))]. given #63 (F,wt=13): 220 (x * x) * (y * x) = e * (y * e). [para(151(a,1),16(a,1,2)),demod(118(4)),flip(a)]. given #64 (T,wt=13): 227 x * (y * (x * e)) = (e * y) * x. [para(182(a,1),13(a,1,2)),demod(172(5),224(6)),flip(a)]. given #65 (T,wt=13): 229 (x * y) * (x * e) = (e * y) * x. [back_demod(135),demod(227(8))]. given #66 (A,wt=17): 74 ((x * y) * e) * (x * z) = x * ((y * e) * z). [para(27(a,1),13(a,1,1))]. given #67 (F,wt=13): 263 e * (x * (y * y)) = (y * x) * e. [back_demod(57),demod(242(4))]. given #68 (F,wt=13): 288 (x * (y * e)) * y = (x * y) * e. [para(83(a,1),17(a,1,2))]. given #69 (T,wt=13): 381 (x * (e * y)) * x = y * (e * x). [para(39(a,1),118(a,2))]. given #70 (T,wt=13): 425 x * (e * (x * y)) = (x * x) * y. [para(7(a,1),101(a,1,2)),flip(a)]. given #71 (A,wt=17): 92 ((x * e) * y) * (e * z) = (x * x) * (y * z). [para(84(a,1),8(a,1,1)),flip(a)]. given #72 (F,wt=13): 434 (x * (e * x)) * e = e * (x * x). [para(101(a,1),150(a,1,1))]. given #73 (F,wt=13): 444 (x * (y * y)) * y = (x * e) * e. [back_demod(363),demod(438(5))]. given #74 (T,wt=13): 446 x * ((y * x) * y) = (x * x) * y. [para(104(a,1),6(a,1,1)),demod(16(5))]. given #75 (T,wt=13): 492 ((x * e) * e) * y = (y * y) * x. [para(84(a,2),462(a,1,1))]. given #76 (A,wt=17): 94 ((x * e) * e) * (y * z) = (x * y) * (x * z). [para(84(a,2),8(a,1,1))]. given #77 (F,wt=13): 503 e * ((x * y) * e) = y * (x * x). [para(462(a,1),239(a,1,2,1)),demod(497(5))]. given #78 (F,wt=13): 506 (x * y) * y = x * ((x * y) * x). [para(7(a,1),466(a,1,2))]. given #79 (T,wt=13): 524 (x * y) * y = x * (e * (y * x)). [para(118(a,1),466(a,1,2)),demod(7(7)),flip(a)]. given #80 (T,wt=13): 532 (x * x) * x = y * ((x * y) * y). [para(466(a,1),466(a,1,2)),demod(17(4))]. given #81 (A,wt=17): 95 (x * y) * ((z * e) * e) = (x * z) * (y * z). [para(84(a,2),8(a,1,2))]. given #82 (F,wt=13): 662 ((x * ((y * e) * x)) * y) * x = e. [para(40(a,1),483(a,1,1,1,2)),demod(297(7),505(5),17(10))]. given #83 (F,wt=13): 671 e * (x * x) = y * ((x * y) * y). [para(468(a,1),483(a,1,1,1,2)),demod(173(5),26(5))]. given #84 (T,wt=13): 673 x * ((x * y) * y) = (x * y) * x. [para(7(a,1),505(a,1,2,2))]. given #85 (T,wt=13): 699 (x * y) * (y * x) = x * (e * y). [para(101(a,1),505(a,2)),demod(208(5),402(7),531(7))]. given #86 (A,wt=15): 96 ((x * y) * e) * e = (x * x) * (y * y). [para(84(a,2),8(a,1))]. given #87 (F,wt=13): 701 ((x * y) * y) * e = (y * e) * x. [para(505(a,1),104(a,2,2)),demod(297(5),297(4),7(5),637(4),297(8),374(8))]. given #88 (F,wt=13): 704 (x * y) * y = y * ((x * x) * x). [para(466(a,1),505(a,1,2,2)),demod(17(4)),flip(a)]. given #89 (T,wt=13): 744 x * ((e * y) * x) = y * (x * e). [para(27(a,1),49(a,1,2)),demod(172(5),204(9))]. given #90 (T,wt=13): 833 ((x * x) * y) * y = y * (x * e). [para(84(a,1),680(a,1,1,1))]. given #91 (A,wt=15): 108 (x * (y * e)) * e = (x * e) * (y * y). [para(84(a,1),27(a,1,2)),flip(a)]. given #92 (F,wt=13): 834 ((e * x) * y) * y = y * (x * x). [para(150(a,1),680(a,1,1,1))]. given #93 (F,wt=13): 860 (x * y) * y = y * (e * (x * x)). [para(635(a,1),680(a,1,1,1)),demod(173(7),26(7))]. given #94 (T,wt=13): 870 ((e * x) * y) * (y * (x * x)) = y. [para(150(a,1),783(a,1,1,1))]. given #95 (T,wt=13): 980 (x * e) * (y * x) = x * (y * e). [para(6(a,1),50(a,2,2,2)),demod(798(6)),flip(a)]. given #96 (A,wt=17): 119 (x * ((y * z) * e)) * z = (x * y) * (y * z). [para(7(a,1),14(a,1,2))]. given #97 (F,wt=13): 1009 x * ((x * y) * e) = y * (e * x). [para(224(a,1),50(a,2,2)),demod(301(6),118(4),848(6),11(3)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.96 (+ 0.00) seconds. % Length of proof is 46. % Level of proof is 19. % Maximum clause weight is 23. % Given clauses 97. 6 (x * e) * x = x. [input]. 7 x * (x * y) = y. [input]. 8 (x * y) * (z * u) = (x * z) * (y * u). [input]. 9 ((x * x) * x) * x = e. [input]. 10 ((c4 * c2) * c3) * c1 != ((c1 * c2) * c3) * c4. [clausify]. 11 e * e = e. [para(6(a,1),6(a,1,1)),demod(7(5)),flip(a)]. 13 ((x * e) * y) * (x * z) = x * (y * z). [para(6(a,1),8(a,1,1)),flip(a)]. 14 (x * (y * e)) * (z * y) = (x * z) * y. [para(6(a,1),8(a,1,2)),flip(a)]. 16 (x * y) * ((x * z) * u) = z * (y * u). [para(7(a,1),8(a,1,1)),flip(a)]. 17 (x * y) * (z * (y * u)) = (x * z) * u. [para(7(a,1),8(a,1,2)),flip(a)]. 20 ((x * x) * x) * e = x. [para(9(a,1),7(a,1,2))]. 26 (e * x) * (e * y) = e * (x * y). [para(11(a,1),8(a,1,1)),flip(a)]. 27 (x * e) * (y * e) = (x * y) * e. [para(11(a,1),8(a,1,2)),flip(a)]. 28 x * ((x * x) * x) = (x * x) * x. [para(20(a,1),6(a,1,1))]. 40 e * (x * (e * y)) = (e * x) * y. [para(7(a,1),26(a,1,2)),flip(a)]. 50 ((x * e) * y) * z = x * (y * (x * z)). [para(7(a,1),13(a,1,2))]. 66 ((x * e) * y) * ((z * e) * u) = ((x * z) * e) * (y * u). [para(27(a,1),8(a,1,1)),flip(a)]. 83 x * ((x * e) * e) = x. [para(13(a,1),28(a,2)),demod(27(7),27(8),20(6),6(3)),flip(a)]. 84 (x * e) * e = x * x. [para(83(a,1),7(a,1,2)),flip(a)]. 88 x * ((((x * e) * e) * e) * y) = (x * e) * (x * y). [para(83(a,1),13(a,1,1)),flip(a)]. 91 (x * e) * (x * x) = e. [para(84(a,1),7(a,1,2))]. 101 (x * x) * (x * y) = x * (e * y). [para(84(a,1),13(a,1,1))]. 104 ((x * x) * y) * e = x * (y * x). [para(84(a,2),13(a,1,2)),demod(66(8),27(6))]. 107 ((x * e) * y) * e = (x * x) * (y * e). [para(84(a,1),27(a,1,1)),flip(a)]. 118 (x * y) * x = e * (y * x). [para(7(a,1),14(a,1,1)),flip(a)]. 144 (x * x) * (e * x) = e. [para(91(a,1),8(a,1)),flip(a)]. 150 (x * x) * e = e * x. [para(144(a,1),7(a,1,2))]. 164 (x * x) * (y * e) = (e * y) * x. [para(150(a,1),13(a,1,2)),demod(150(3),118(6),40(5)),flip(a)]. 168 e * (x * e) = x * (e * x). [para(150(a,1),84(a,1,1)),demod(118(4),101(7))]. 172 ((x * e) * y) * e = (e * y) * x. [back_demod(107),demod(164(9))]. 176 (x * e) * (x * y) = x * ((e * x) * y). [back_demod(88),demod(172(6),11(3)),flip(a)]. 182 x * ((e * x) * x) = e. [back_demod(91),demod(176(4))]. 193 x * (y * ((z * x) * u)) = (z * y) * u. [para(7(a,1),16(a,1,2)),flip(a)]. 194 ((x * y) * z) * (((x * u) * v) * w) = (u * (y * v)) * (z * w). [para(16(a,1),8(a,1,1)),flip(a)]. 214 x * (y * (e * x)) = (x * y) * e. [para(144(a,1),16(a,1,2)),flip(a)]. 224 (e * x) * x = x * e. [para(182(a,1),7(a,1,2)),flip(a)]. 297 (x * (y * z)) * (u * v) = z * ((y * (x * u)) * v). [para(17(a,1),16(a,1,1)),demod(194(6))]. 301 (x * e) * (y * (x * z)) = ((e * x) * y) * z. [para(224(a,1),17(a,1,1))]. 466 x * (y * x) = y * (x * y). [para(104(a,1),224(a,2)),demod(297(7),168(5,R),150(4),7(4))]. 505 x * (y * (x * y)) = y * x. [para(466(a,1),7(a,1,2))]. 680 ((x * e) * y) * y = y * x. [para(505(a,1),13(a,2)),demod(7(5))]. 848 ((x * (y * x)) * z) * z = z * ((x * x) * y). [para(104(a,1),680(a,1,1,1))]. 1009 x * ((x * y) * e) = y * (e * x). [para(224(a,1),50(a,2,2)),demod(301(6),118(4),848(6),11(3)),flip(a)]. 1517 ((x * e) * y) * (z * e) = e * (z * ((e * y) * x)). [para(172(a,1),13(a,1,2)),demod(172(5),118(8)),flip(a)]. 3834 ((x * y) * z) * u = ((u * y) * z) * x. [para(1009(a,1),66(a,2,2)),demod(27(9),1517(8),297(7),214(5),193(7),17(10))]. 3835 $F. [resolve(3834,a,10,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=97. Generated=26039. Kept=3829. proofs=1. Usable=77. Sos=2519. Demods=1324. Denials=0. 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=570642. 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.89. User_CPU=0.96, System_CPU=0.00, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 12987 exit (max_proofs) Mon Jun 19 16:39:42 2006