============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13014 was started by mccune on cleo.thornwood, Mon Jun 19 16:40:06 2006 The command was "/home/mccune/bin/prover9 -f identity.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file identity.in 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: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ e, c1, c2, c3, c4, * ]). After inverse_order: Function symbol precedence: lex([ e, c1, c2, c3, c4, * ]). 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=11): 34 (x * y) * (e * (y * x)) = x. [para(7(a,1),12(a,1,1,1)),demod(7(7))]. given #10 (T,wt=9): 46 e * ((x * x) * e) = x. [para(9(a,1),34(a,1,2,2)),demod(40(2),45(4),11(6),40(5))]. 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=9): 47 (x * x) * (e * x) = e. [para(20(a,1),34(a,1,2,2)),demod(40(3),7(5))]. given #13 (F,wt=9): 61 (e * (x * x)) * x = e. [back_demod(9),demod(40(2))]. given #14 (T,wt=9): 62 (x * x) * e = e * x. [para(46(a,1),7(a,1,2)),flip(a)]. given #15 (T,wt=9): 77 (x * e) * (x * x) = e. [para(47(a,1),8(a,1)),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=19): 102 ((c4 * (c3 * e)) * (c2 * c3)) * c1 != ((c1 * c2) * c3) * c4. [para(14(a,2),10(a,1,1))]. given #18 (F,wt=19): 103 ((c4 * c2) * (c1 * e)) * (c3 * c1) != ((c1 * c2) * c3) * c4. [para(14(a,2),10(a,1))]. given #19 (T,wt=9): 86 (x * e) * e = x * x. [para(77(a,1),7(a,1,2))]. given #20 (T,wt=11): 40 (x * y) * x = e * (y * x). [para(34(a,1),7(a,1,2))]. given #21 (A,wt=15): 15 (x * y) * ((x * z) * (y * u)) = z * u. [para(8(a,1),7(a,1,2))]. given #22 (F,wt=19): 104 ((c4 * c2) * c3) * c1 != ((c1 * (c3 * e)) * (c2 * c3)) * c4. [para(14(a,2),10(a,2,1))]. given #23 (F,wt=19): 105 ((c4 * c2) * c3) * c1 != ((c1 * c2) * (c4 * e)) * (c3 * c4). [para(14(a,2),10(a,2))]. given #24 (T,wt=11): 79 (e * x) * (x * x) = x * x. [para(47(a,1),34(a,1,1)),demod(7(8))]. given #25 (T,wt=11): 90 (x * x) * (x * e) = x * e. [para(77(a,1),34(a,1,1)),demod(7(8))]. given #26 (A,wt=15): 16 (x * y) * ((x * z) * u) = z * (y * u). [para(7(a,1),8(a,1,1)),flip(a)]. given #27 (F,wt=19): 133 ((c4 * c1) * (c2 * e)) * (c3 * c1) != ((c1 * c2) * c3) * c4. [para(8(a,1),103(a,1,1))]. given #28 (F,wt=19): 186 ((c4 * c2) * c3) * c1 != ((c1 * c4) * (c2 * e)) * (c3 * c4). [para(8(a,1),105(a,2,1))]. given #29 (T,wt=11): 316 x * (y * (x * y)) = y * x. [back_demod(55),demod(216(8),7(10),259(8))]. given #30 (T,wt=9): 372 x * ((e * x) * x) = e. [back_demod(318),demod(331(6))]. given #31 (A,wt=15): 17 (x * y) * (z * (y * u)) = (x * z) * u. [para(7(a,1),8(a,1,2)),flip(a)]. given #32 (F,wt=27): 628 c4 * (c3 * (e * ((c2 * c4) * (e * c1)))) != c1 * (c3 * (e * ((c2 * c1) * (e * c4)))). [back_demod(10),demod(407(7),407(20))]. given #33 (F,wt=27): 667 c1 * (c3 * (e * ((c2 * c1) * (e * c4)))) != c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))). [para(8(a,1),628(a,1,2,2,2)),flip(a)]. given #34 (T,wt=11): 331 x * (y * x) = y * (x * y). [para(316(a,1),7(a,1,2))]. given #35 (T,wt=13): 45 x * (e * (x * x)) = e * (x * x). [para(9(a,1),34(a,1,1)),demod(40(4),7(8),40(6))]. given #36 (A,wt=15): 211 e * (x * y) = z * (x * (e * (z * y))). [para(34(a,1),16(a,1,2)),demod(40(2))]. given #37 (F,wt=47): 788 c4 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [back_demod(689),demod(742(12),7(25),742(27),7(32),742(39),7(44),7(41),7(40),7(37),7(36),7(34),659(32),659(28),742(33),7(41),7(48))]. given #38 (F,wt=47): 795 c4 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))). [back_demod(681),demod(742(10),7(23),7(25),742(33),7(46),7(48))]. given #39 (T,wt=15): 410 e * (x * (y * z)) = y * (x * (e * z)). [para(61(a,1),17(a,1,1)),demod(401(8),401(11),82(12),401(10),401(13),7(13),7(12))]. given #40 (T,wt=13): 1144 e * (x * (y * e)) = y * (x * e). [para(11(a,1),410(a,2,2,2))]. given #41 (A,wt=19): 384 x * (y * (e * x)) = z * (y * (x * (z * (e * x)))). [para(372(a,1),16(a,1,2)),demod(216(3),376(9),216(7))]. given #42 (F,wt=47): 799 c4 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c2 * (e * (c2 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [back_demod(677),demod(742(10),7(18),7(25),742(35),7(43),742(50),7(55),742(62),7(67),7(64),7(63),7(60),7(59),7(57),659(55),659(51))]. given #43 (F,wt=47): 807 c4 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c2 * (e * (c2 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))). [back_demod(668),demod(742(10),7(18),7(25),742(33),7(46),7(48))]. given #44 (T,wt=13): 1177 x * (e * (y * (x * e))) = y * e. [para(1144(a,2),7(a,1,2))]. given #45 (T,wt=15): 412 x * (y * (e * (x * (y * z)))) = e * z. [para(61(a,1),17(a,2,1)),demod(401(4),401(9),82(10),401(8),401(11),7(11),7(10))]. given #46 (A,wt=17): 461 e * (x * (e * (y * (x * (y * y))))) = y * y. [para(17(a,2),79(a,1)),demod(401(6))]. given #47 (F,wt=47): 1170 c4 * (e * (c2 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [para(410(a,2),788(a,1,2))]. given #48 (F,wt=47): 1171 c4 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * c1)))))))))) != c1 * (e * (c2 * (c3 * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [para(410(a,2),788(a,2,2))]. given #49 (T,wt=15): 536 e * (x * (y * (e * z))) = y * (x * z). [back_demod(74),demod(401(10),407(11),7(12),407(9),401(11),7(11),7(8),7(8),7(5),7(4))]. given #50 (T,wt=15): 648 x * (e * (x * y)) = y * (e * (y * x)). [back_demod(490),demod(630(2))]. given #51 (A,wt=17): 517 e * (x * (e * (y * y))) = y * (x * (y * y)). [back_demod(279),demod(401(4))]. given #52 (F,wt=47): 1172 c4 * (e * (c2 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))). [para(410(a,2),795(a,1,2))]. given #53 (F,wt=47): 1173 c4 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * c1)))))))))) != c1 * (e * (c2 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))). [para(410(a,2),795(a,2,2))]. given #54 (T,wt=15): 655 x * (e * (y * (x * z))) = y * (e * z). [back_demod(252),demod(630(5),7(5))]. given #55 (T,wt=15): 656 e * (x * e) = y * (e * (y * (x * y))). [back_demod(220),demod(630(3)),flip(a)]. given #56 (A,wt=31): 528 e * (x * (y * (e * (y * (x * (y * (z * (x * u)))))))) = y * (x * (y * (z * (y * u)))). [back_demod(152),demod(401(9),407(10),7(11),407(8),401(10),7(10),7(9))]. given #57 (F,wt=47): 1239 c4 * (e * (c2 * (c3 * (c2 * (e * (c4 * (e * (c2 * (e * (c2 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [para(410(a,2),799(a,1,2))]. given #58 (F,wt=47): 1240 c4 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c2 * (e * (c2 * c1)))))))))) != c1 * (e * (c2 * (c3 * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [para(410(a,2),799(a,2,2))]. given #59 (T,wt=15): 657 x * (e * (y * (x * (e * z)))) = y * z. [back_demod(175),demod(630(7),7(7))]. given #60 (T,wt=15): 716 e * (x * y) = x * (y * (e * (y * x))). [para(331(a,1),17(a,1)),demod(630(2),40(7)),flip(a)]. given #61 (A,wt=19): 581 x * (y * (e * (x * (z * (e * u))))) = z * (y * u). [back_demod(243),demod(407(8),407(10),7(11),401(8),7(11),407(13),448(15),7(7))]. given #62 (F,wt=39): 2131 c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))) != e * (c3 * (c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [back_demod(1329),demod(1954(21),1954(42),7(39))]. given #63 (F,wt=39): 2132 e * (c3 * (c4 * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [back_demod(1328),demod(1954(23),7(20),1954(40))]. given #64 (T,wt=15): 1108 e * x = x * (y * (x * (e * (y * e)))). [para(211(a,1),316(a,1,2)),flip(a)]. given #65 (T,wt=15): 1109 x * (y * (e * (x * (e * y)))) = y * e. [para(211(a,1),316(a,1))]. given #66 (A,wt=21): 647 e * (x * (e * (x * (e * (y * x))))) = x * (y * (e * x)). [back_demod(515),demod(630(8),7(8),7(7),630(6))]. given #67 (F,wt=39): 2206 c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [back_demod(795),demod(1954(21),1954(40))]. given #68 (F,wt=39): 2231 c4 * (c2 * (e * (c2 * (e * (c2 * (c4 * (c3 * (e * c1)))))))) != c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * (c3 * (e * c4)))))))). [back_demod(836),demod(2179(30),2179(49))]. given #69 (T,wt=15): 1117 x * (e * x) = y * (x * (e * (y * e))). [para(211(a,1),331(a,1)),flip(a)]. given #70 (T,wt=15): 1121 e * (x * e) = y * (x * (y * (e * y))). [para(331(a,1),211(a,2,2,2))]. given #71 (A,wt=29): 742 (x * y) * z = e * (x * (e * (x * (e * (y * (e * (x * (e * (x * (e * z)))))))))). [para(45(a,1),17(a,1,1)),demod(401(7),630(8),401(13),630(14)),flip(a)]. given #72 (F,wt=39): 2335 c4 * (c3 * (e * (c2 * (e * (c2 * (c4 * (c2 * (e * c1)))))))) != e * (c3 * (c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(581(a,2),2131(a,1,2,2,2,2,2,2,2)),demod(1936(19))]. given #73 (F,wt=39): 2337 c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))) != e * (c3 * (c1 * (c2 * (e * (c2 * (c1 * (c2 * (e * c4)))))))). [para(581(a,2),2131(a,2,2,2,2,2,2,2,2)),demod(1936(38))]. given #74 (T,wt=15): 1151 e * (x * (y * (x * e))) = y * (e * x). [para(316(a,1),410(a,2,2))]. given #75 (T,wt=15): 1155 e * (x * (y * x)) = x * (y * (e * y)). [para(331(a,1),410(a,1,2))]. given #76 (A,wt=53): 743 e * (x * (e * (x * (e * (y * (e * (x * (e * (x * (e * (z * (e * (y * y))))))))))))) = e * (x * (e * (x * (e * (z * (e * (x * (e * (x * (y * y)))))))))). [para(45(a,1),17(a,1,2,2)),demod(742(6),742(26),7(31))]. given #77 (F,wt=39): 2351 e * (c3 * (c4 * (c2 * (e * (c2 * (c4 * (c2 * (e * c1)))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(581(a,2),2132(a,1,2,2,2,2,2,2,2)),demod(1936(19))]. given #78 (F,wt=39): 2353 e * (c3 * (c4 * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (c1 * (c2 * (e * c4)))))))). [para(581(a,2),2132(a,2,2,2,2,2,2,2,2)),demod(1936(38))]. given #79 (T,wt=15): 1157 e * (x * (y * x)) = y * (e * (x * e)). [para(331(a,1),410(a,2,2))]. given #80 (T,wt=15): 1186 e * (x * (e * (y * e))) = x * (y * x). [back_demod(766),demod(1177(8))]. given #81 (A,wt=73): 745 e * (x * (e * (x * (e * (y * (e * (x * (e * (x * (e * (z * (y * (x * (e * (x * (e * (z * (e * (x * (e * (x * (e * (x * z))))))))))))))))))))))) = x * (e * (x * (e * (z * (e * (x * (e * (x * (e * (x * z)))))))))). [para(45(a,1),17(a,2)),demod(742(5),7(21),742(20),742(39),7(55))]. given #82 (F,wt=39): 2544 c4 * (c3 * (e * (c2 * (e * (c2 * (c4 * (c2 * (e * c1)))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(581(a,2),2206(a,1,2,2,2,2,2,2,2)),demod(1936(19))]. given #83 (F,wt=39): 2545 c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (c1 * (c2 * (e * c4)))))))). [para(581(a,2),2206(a,2,2,2,2,2,2,2,2)),demod(1936(38))]. given #84 (T,wt=15): 1220 x * (e * (y * (x * (y * e)))) = e * y. [para(1144(a,1),384(a,1,2)),demod(11(5),742(5),316(11),7(9),7(8),45(6),7(6),7(3),742(11),7(21),1195(22)),flip(a)]. given #85 (T,wt=15): 1260 x * (y * (e * (y * (x * y)))) = e * x. [para(331(a,1),412(a,1,2,2,2))]. given #86 (A,wt=35): 748 e * (x * (e * (x * (e * (y * (e * (x * (e * (x * (e * (x * y))))))))))) = x * (e * (x * (y * y))). [back_demod(644),demod(742(10),7(15),7(12),7(11),7(8),45(8),7(8),7(9),742(8)),flip(a)]. given #87 (F,wt=39): 2559 c4 * (c2 * (e * (c2 * (c4 * (c2 * (e * (c3 * (e * c1)))))))) != c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * (c3 * (e * c4)))))))). [para(581(a,2),2231(a,1,2,2,2,2,2)),demod(1936(21))]. given #88 (F,wt=39): 2562 c4 * (c2 * (e * (c2 * (e * (c2 * (c4 * (c3 * (e * c1)))))))) != c1 * (c2 * (e * (c2 * (c1 * (c2 * (e * (c3 * (e * c4)))))))). [para(581(a,2),2231(a,2,2,2,2,2,2)),demod(1936(40))]. given #89 (T,wt=15): 1280 x * (e * (y * (x * y))) = e * (y * e). [para(461(a,1),384(a,1,2)),demod(45(5),7(5),742(3),45(9),7(9),7(6),316(7),7(5),11(4),45(10),7(10),45(12),7(12),742(11),820(26),659(12)),flip(a)]. given #90 (T,wt=15): 1313 x * (e * (x * (y * (e * y)))) = y * x. [para(536(a,2),316(a,1,2))]. given #91 (A,wt=29): 749 x * (y * (z * (e * (z * (e * (y * (e * (x * x)))))))) = z * (e * (z * (x * x))). [back_demod(568),demod(742(6),748(21),742(10),7(15),7(12),7(11),7(8),7(14),742(15),748(30))]. given #92 (F,wt=39): 2713 c4 * (c3 * (e * (c2 * (c4 * (c2 * (e * (c2 * (e * c1)))))))) != e * (c3 * (c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(581(a,2),2335(a,1,2,2,2,2,2)),demod(1936(21))]. ============================== PROOF ================================= % Proof 1 at 3.92 (+ 0.02) seconds. % Length of proof is 87. % Level of proof is 18. % Maximum clause weight is 51. % Given clauses 92. 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)]. 12 ((x * y) * x) * (e * y) = x * y. [para(8(a,1),6(a,1))]. 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)]. 15 (x * y) * ((x * z) * (y * u)) = z * u. [para(8(a,1),7(a,1,2))]. 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))]. 32 (((x * y) * x) * ((x * y) * y)) * e = x * y. [para(8(a,1),20(a,1,1))]. 34 (x * y) * (e * (y * x)) = x. [para(7(a,1),12(a,1,1,1)),demod(7(7))]. 40 (x * y) * x = e * (y * x). [para(34(a,1),7(a,1,2))]. 45 x * (e * (x * x)) = e * (x * x). [para(9(a,1),34(a,1,1)),demod(40(4),7(8),40(6))]. 46 e * ((x * x) * e) = x. [para(9(a,1),34(a,1,2,2)),demod(40(2),45(4),11(6),40(5))]. 47 (x * x) * (e * x) = e. [para(20(a,1),34(a,1,2,2)),demod(40(3),7(5))]. 55 ((e * (x * y)) * ((y * x) * x)) * e = y * x. [back_demod(32),demod(40(2))]. 61 (e * (x * x)) * x = e. [back_demod(9),demod(40(2))]. 62 (x * x) * e = e * x. [para(46(a,1),7(a,1,2)),flip(a)]. 65 ((x * e) * y) * z = x * (y * (x * z)). [para(7(a,1),13(a,1,2))]. 74 (e * ((x * (y * e)) * y)) * (y * (x * (y * z))) = y * (x * z). [para(13(a,1),13(a,2)),demod(65(5),40(5),65(10))]. 77 (x * e) * (x * x) = e. [para(47(a,1),8(a,1)),flip(a)]. 79 (e * x) * (x * x) = x * x. [para(47(a,1),34(a,1,1)),demod(7(8))]. 82 ((x * x) * y) * (e * z) = (e * x) * (y * z). [para(62(a,1),8(a,1,1)),flip(a)]. 86 (x * e) * e = x * x. [para(77(a,1),7(a,1,2))]. 112 (x * (e * (x * e))) * (x * (e * x)) = e. [para(14(a,2),47(a,1)),demod(40(4))]. 142 (x * x) * y = x * ((y * e) * (x * (e * y))). [para(86(a,1),14(a,2,1)),demod(65(8)),flip(a)]. 175 (x * x) * (x * (y * (x * (e * z)))) = y * z. [para(86(a,1),15(a,1,1)),demod(65(7))]. 189 (e * (x * y)) * ((x * x) * (y * y)) = (x * y) * (x * y). [para(8(a,1),79(a,1,2))]. 211 e * (x * y) = z * (x * (e * (z * y))). [para(34(a,1),16(a,1,2)),demod(40(2))]. 216 (x * y) * e = x * (y * (e * x)). [para(47(a,1),16(a,1,2))]. 243 ((x * y) * z) * (((x * (u * e)) * (y * u)) * v) = u * (z * v). [para(14(a,2),16(a,1,2,1))]. 259 (e * (x * y)) * (((y * x) * z) * u) = z * (y * u). [para(40(a,1),16(a,1,1))]. 275 ((x * y) * ((x * e) * z)) * ((y * z) * (y * z)) = (y * z) * (y * z). [para(16(a,2),79(a,1,1))]. 316 x * (y * (x * y)) = y * x. [back_demod(55),demod(216(8),7(10),259(8))]. 318 (e * x) * (x * (e * x)) = e. [back_demod(112),demod(316(5))]. 331 x * (y * x) = y * (x * y). [para(316(a,1),7(a,1,2))]. 372 x * ((e * x) * x) = e. [back_demod(318),demod(331(6))]. 376 (e * x) * x = x * e. [para(372(a,1),7(a,1,2)),flip(a)]. 384 x * (y * (e * x)) = z * (y * (x * (z * (e * x)))). [para(372(a,1),16(a,1,2)),demod(216(3),376(9),216(7))]. 401 (e * x) * y = e * (x * (e * y)). [para(11(a,1),17(a,1,1)),flip(a)]. 407 ((x * y) * z) * u = x * (z * (e * ((y * x) * (e * u)))). [para(34(a,1),17(a,1,1)),demod(401(4)),flip(a)]. 410 e * (x * (y * z)) = y * (x * (e * z)). [para(61(a,1),17(a,1,1)),demod(401(8),401(11),82(12),401(10),401(13),7(13),7(12))]. 438 (x * y) * (z * (y * x)) = e * (z * x). [para(17(a,2),40(a,1))]. 446 x * (y * (e * ((z * x) * (e * (x * ((z * (u * v)) * (e * ((u * x) * (e * (y * w)))))))))) = v * w. [para(17(a,2),15(a,1,2,1)),demod(407(8),407(14))]. 448 (x * y) * (z * (y * ((x * u) * (z * v)))) = u * v. [para(17(a,2),15(a,1))]. 520 e * ((x * y) * (e * (y * (z * (e * ((x * y) * (e * u))))))) = z * (y * u). [back_demod(259),demod(407(6),401(12))]. 525 e * ((x * y) * (e * ((x * x) * (y * y)))) = (x * y) * (x * y). [back_demod(189),demod(401(7))]. 536 e * (x * (y * (e * z))) = y * (x * z). [back_demod(74),demod(401(10),407(11),7(12),407(9),401(11),7(11),7(8),7(8),7(5),7(4))]. 568 x * (y * (e * ((z * y) * (e * ((z * x) * (z * x)))))) = (z * x) * (z * x). [back_demod(275),demod(407(9),407(13),7(14),401(11),7(14),7(13))]. 581 x * (y * (e * (x * (z * (e * u))))) = z * (y * u). [back_demod(243),demod(407(8),407(10),7(11),401(8),7(11),407(13),448(15),7(7))]. 628 c4 * (c3 * (e * ((c2 * c4) * (e * c1)))) != c1 * (c3 * (e * ((c2 * c1) * (e * c4)))). [back_demod(10),demod(407(7),407(20))]. 630 (x * x) * y = x * (e * (x * y)). [back_demod(142),demod(438(8))]. 631 x * (y * (e * ((z * u) * ((z * x) * (e * (y * v)))))) = u * v. [back_demod(446),demod(448(16))]. 644 e * ((x * y) * (e * (x * (e * (x * (y * y)))))) = (x * y) * (x * y). [back_demod(525),demod(630(6))]. 657 x * (e * (y * (x * (e * z)))) = y * z. [back_demod(175),demod(630(7),7(7))]. 667 c1 * (c3 * (e * ((c2 * c1) * (e * c4)))) != c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))). [para(8(a,1),628(a,1,2,2,2)),flip(a)]. 681 c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))) != c1 * (c3 * (e * ((c2 * e) * (c1 * c4)))). [para(8(a,1),667(a,1,2,2,2)),flip(a)]. 716 e * (x * y) = x * (y * (e * (y * x))). [para(331(a,1),17(a,1)),demod(630(2),40(7)),flip(a)]. 742 (x * y) * z = e * (x * (e * (x * (e * (y * (e * (x * (e * (x * (e * z)))))))))). [para(45(a,1),17(a,1,1)),demod(401(7),630(8),401(13),630(14)),flip(a)]. 748 e * (x * (e * (x * (e * (y * (e * (x * (e * (x * (e * (x * y))))))))))) = x * (e * (x * (y * y))). [back_demod(644),demod(742(10),7(15),7(12),7(11),7(8),45(8),7(8),7(9),742(8)),flip(a)]. 749 x * (y * (z * (e * (z * (e * (y * (e * (x * x)))))))) = z * (e * (z * (x * x))). [back_demod(568),demod(742(6),748(21),742(10),7(15),7(12),7(11),7(8),7(14),742(15),748(30))]. 795 c4 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))). [back_demod(681),demod(742(10),7(23),7(25),742(33),7(46),7(48))]. 819 x * (y * (z * (e * (z * (e * (u * (x * (e * (z * (e * (z * (y * v)))))))))))) = u * v. [back_demod(631),demod(742(7),7(12),742(19),7(24),7(21),7(20),7(17),7(16),7(19))]. 900 x * (e * (x * (e * (y * (e * (x * (e * (x * (y * (z * (x * (e * (x * (e * (y * (e * (x * (e * (x * u))))))))))))))))))) = z * (y * u). [back_demod(520),demod(742(8),7(13),7(20),742(20),7(25),7(32))]. 1144 e * (x * (y * e)) = y * (x * e). [para(11(a,1),410(a,2,2,2))]. 1155 e * (x * (y * x)) = x * (y * (e * y)). [para(331(a,1),410(a,1,2))]. 1165 e * (x * (y * z)) = u * (x * (y * (u * (e * z)))). [para(410(a,1),211(a,2,2,2))]. 1195 e * (x * (e * (x * (e * (x * (e * (x * (e * (y * (e * (x * e))))))))))) = x * (y * (x * e)). [para(316(a,1),384(a,2,2,2,2)),demod(742(8),7(18),742(24),7(29),45(28),7(28),7(26),7(23),316(24))]. 1220 x * (e * (y * (x * (y * e)))) = e * y. [para(1144(a,1),384(a,1,2)),demod(11(5),742(5),316(11),7(9),7(8),45(6),7(6),7(3),742(11),7(21),1195(22)),flip(a)]. 1314 e * (x * (y * (e * (y * x)))) = x * y. [para(536(a,2),316(a,1))]. 1325 e * (x * (y * (e * (z * (e * (x * u)))))) = y * (e * (z * u)). [para(211(a,2),536(a,2,2))]. 1329 c4 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * c1)))))))))) != e * (c3 * (c1 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))))). [para(536(a,2),795(a,2))]. 1909 e * (x * (y * (z * (x * (e * u))))) = y * (z * u). [para(657(a,1),410(a,2,2))]. 1928 x * (e * (x * (e * (y * (z * (e * (x * (e * (x * u))))))))) = y * (z * u). [back_demod(900),demod(1909(21),1909(17),7(12))]. 1936 x * (y * (z * (x * (y * u)))) = z * u. [back_demod(819),demod(1928(15))]. 1954 x * (e * (x * (e * (x * (e * (x * (e * y))))))) = e * (x * (e * (x * (e * (x * y))))). [para(1144(a,1),716(a,2,2,2)),demod(742(4),7(14),7(16),742(19),1220(25),7(21),7(20))]. 2131 c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))) != e * (c3 * (c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [back_demod(1329),demod(1954(21),1954(42),7(39))]. 2335 c4 * (c3 * (e * (c2 * (e * (c2 * (c4 * (c2 * (e * c1)))))))) != e * (c3 * (c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(581(a,2),2131(a,1,2,2,2,2,2,2,2)),demod(1936(19))]. 2713 c4 * (c3 * (e * (c2 * (c4 * (c2 * (e * (c2 * (e * c1)))))))) != e * (c3 * (c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(581(a,2),2335(a,1,2,2,2,2,2)),demod(1936(21))]. 2886 e * (x * (e * (x * (e * (x * (e * (x * y))))))) = x * (e * (x * (e * (x * (e * y))))). [para(1155(a,2),716(a,2,2,2,2)),demod(742(5),742(15),7(23),7(21),7(19),7(16),7(15),7(13),7(11),7(13),7(18),7(15),742(14),742(24),7(32),7(30),7(28),7(25),7(24),7(22),7(20)),flip(a)]. 3877 e * (x * (e * (x * (e * (x * (y * (e * (y * (e * x))))))))) = y * (e * (y * x)). [para(1155(a,2),749(a,1,2,2,2,2,2,2,2,2)),demod(7(14),742(13),7(18),45(17),7(17),742(14),7(23),7(21),45(19),7(19),7(17),7(15),45(13),7(13),7(10),7(10),742(14),1325(19),742(18),7(26),7(24),7(22),7(19),7(18),7(16),7(14),742(23),316(28),7(26),11(25),742(26),7(34),7(32),7(30),7(27),11(26),11(25),11(24),11(23),11(22),11(21),316(22),7(20))]. 3896 c4 * (c3 * (c1 * (c4 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))))) != e * (c3 * (c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(716(a,1),2713(a,1,2,2)),demod(742(28),742(41),7(49),742(50),7(58),7(56),7(54),742(51),3877(61),1314(49),742(42),7(51),7(49),7(49),7(47),7(45),1936(43),7(38),7(36),7(34),7(36),7(37),742(34),2886(46),742(43),742(56),7(64),7(62),7(60),742(57),1954(68),7(65),742(62),7(71),7(69),7(69),7(67),7(65),1936(63),1936(57),7(51),7(49),7(47),1936(45),7(40),1909(38),1909(32),7(25))]. 3897 $F. [resolve(3896,a,1165,a(flip))]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=92. Generated=12403. Kept=3891. proofs=1. Usable=48. Sos=2477. Demods=440. Denials=0. Limbo=6, Disabled=1364. Hints=0. Weight_deleted=305. Literals_deleted=0. Forward_subsumed=8207. Back_subsumed=65. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=960 (1 lex), Back_demodulated=1294. Back_unit_deleted=0. Demod_attempts=948688. Demod_rewrites=169720. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=7.90. User_CPU=3.92, System_CPU=0.02, Wall_clock=4. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13014 exit (max_proofs) Mon Jun 19 16:40:10 2006