============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 3319 was started by mccune on cleo.thornwood, Wed Nov 22 11:22:01 2006 The command was "/home/mccune/bin/prover9 -f identity.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file identity.in 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 # label(goal). [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: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ e, c1, c2, c3, c4, * ]). After inverse_order: (no changes). 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=11): 30 (x * y) * (e * (y * x)) = x. [para(3(a,1),8(a,1,1,1)),rewrite(3(7))]. given #10 (T,wt=9): 42 e * ((x * x) * e) = x. [para(5(a,1),30(a,1,2,2)),rewrite(36(2),41(4),7(6),36(5))]. 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=9): 43 (x * x) * (e * x) = e. [para(16(a,1),30(a,1,2,2)),rewrite(36(3),3(5))]. given #13 (F,wt=9): 57 (e * (x * x)) * x = e. [back_rewrite(5),rewrite(36(2))]. given #14 (T,wt=9): 58 (x * x) * e = e * x. [para(42(a,1),3(a,1,2)),flip(a)]. given #15 (T,wt=9): 73 (x * e) * (x * x) = e. [para(43(a,1),4(a,1)),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=19): 98 ((c4 * (c3 * e)) * (c2 * c3)) * c1 != ((c1 * c2) * c3) * c4. [para(10(a,2),6(a,1,1))]. given #18 (F,wt=19): 99 ((c4 * c2) * (c1 * e)) * (c3 * c1) != ((c1 * c2) * c3) * c4. [para(10(a,2),6(a,1))]. given #19 (T,wt=9): 82 (x * e) * e = x * x. [para(73(a,1),3(a,1,2))]. given #20 (T,wt=11): 36 (x * y) * x = e * (y * x). [para(30(a,1),3(a,1,2))]. given #21 (A,wt=15): 11 (x * y) * ((x * z) * (y * u)) = z * u. [para(4(a,1),3(a,1,2))]. given #22 (F,wt=19): 100 ((c4 * c2) * c3) * c1 != ((c1 * (c3 * e)) * (c2 * c3)) * c4. [para(10(a,2),6(a,2,1))]. given #23 (F,wt=19): 101 ((c4 * c2) * c3) * c1 != ((c1 * c2) * (c4 * e)) * (c3 * c4). [para(10(a,2),6(a,2))]. given #24 (T,wt=11): 75 (e * x) * (x * x) = x * x. [para(43(a,1),30(a,1,1)),rewrite(3(8))]. given #25 (T,wt=11): 86 (x * x) * (x * e) = x * e. [para(73(a,1),30(a,1,1)),rewrite(3(8))]. given #26 (A,wt=15): 12 (x * y) * ((x * z) * u) = z * (y * u). [para(3(a,1),4(a,1,1)),flip(a)]. given #27 (F,wt=19): 129 ((c4 * c1) * (c2 * e)) * (c3 * c1) != ((c1 * c2) * c3) * c4. [para(4(a,1),99(a,1,1))]. given #28 (F,wt=19): 182 ((c4 * c2) * c3) * c1 != ((c1 * c4) * (c2 * e)) * (c3 * c4). [para(4(a,1),101(a,2,1))]. given #29 (T,wt=11): 312 x * (y * (x * y)) = y * x. [back_rewrite(51),rewrite(212(8),3(10),255(8))]. given #30 (T,wt=9): 368 x * ((e * x) * x) = e. [back_rewrite(314),rewrite(327(6))]. given #31 (A,wt=15): 13 (x * y) * (z * (y * u)) = (x * z) * u. [para(3(a,1),4(a,1,2)),flip(a)]. given #32 (F,wt=27): 624 c4 * (c3 * (e * ((c2 * c4) * (e * c1)))) != c1 * (c3 * (e * ((c2 * c1) * (e * c4)))). [back_rewrite(6),rewrite(403(7),403(20))]. given #33 (F,wt=27): 663 c1 * (c3 * (e * ((c2 * c1) * (e * c4)))) != c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))). [para(4(a,1),624(a,1,2,2,2)),flip(a)]. given #34 (T,wt=11): 327 x * (y * x) = y * (x * y). [para(312(a,1),3(a,1,2))]. given #35 (T,wt=13): 41 x * (e * (x * x)) = e * (x * x). [para(5(a,1),30(a,1,1)),rewrite(36(4),3(8),36(6))]. given #36 (A,wt=15): 207 e * (x * y) = z * (x * (e * (z * y))). [para(30(a,1),12(a,1,2)),rewrite(36(2))]. given #37 (F,wt=47): 784 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_rewrite(685),rewrite(738(12),3(25),738(27),3(32),738(39),3(44),3(41),3(40),3(37),3(36),3(34),655(32),655(28),738(33),3(41),3(48))]. given #38 (F,wt=47): 791 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_rewrite(677),rewrite(738(10),3(23),3(25),738(33),3(46),3(48))]. given #39 (T,wt=15): 406 e * (x * (y * z)) = y * (x * (e * z)). [para(57(a,1),13(a,1,1)),rewrite(397(8),397(11),78(12),397(10),397(13),3(13),3(12))]. given #40 (T,wt=13): 1140 e * (x * (y * e)) = y * (x * e). [para(7(a,1),406(a,2,2,2))]. given #41 (A,wt=19): 380 x * (y * (e * x)) = z * (y * (x * (z * (e * x)))). [para(368(a,1),12(a,1,2)),rewrite(212(3),372(9),212(7))]. given #42 (F,wt=47): 795 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_rewrite(673),rewrite(738(10),3(18),3(25),738(35),3(43),738(50),3(55),738(62),3(67),3(64),3(63),3(60),3(59),3(57),655(55),655(51))]. given #43 (F,wt=47): 803 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_rewrite(664),rewrite(738(10),3(18),3(25),738(33),3(46),3(48))]. given #44 (T,wt=13): 1173 x * (e * (y * (x * e))) = y * e. [para(1140(a,2),3(a,1,2))]. given #45 (T,wt=15): 408 x * (y * (e * (x * (y * z)))) = e * z. [para(57(a,1),13(a,2,1)),rewrite(397(4),397(9),78(10),397(8),397(11),3(11),3(10))]. given #46 (A,wt=17): 457 e * (x * (e * (y * (x * (y * y))))) = y * y. [para(13(a,2),75(a,1)),rewrite(397(6))]. given #47 (F,wt=47): 1166 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(406(a,2),784(a,1,2))]. given #48 (F,wt=47): 1167 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(406(a,2),784(a,2,2))]. given #49 (T,wt=15): 532 e * (x * (y * (e * z))) = y * (x * z). [back_rewrite(70),rewrite(397(10),403(11),3(12),403(9),397(11),3(11),3(8),3(8),3(5),3(4))]. given #50 (T,wt=15): 644 x * (e * (x * y)) = y * (e * (y * x)). [back_rewrite(486),rewrite(626(2))]. given #51 (A,wt=17): 513 e * (x * (e * (y * y))) = y * (x * (y * y)). [back_rewrite(275),rewrite(397(4))]. given #52 (F,wt=47): 1168 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(406(a,2),791(a,1,2))]. given #53 (F,wt=47): 1169 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(406(a,2),791(a,2,2))]. given #54 (T,wt=15): 651 x * (e * (y * (x * z))) = y * (e * z). [back_rewrite(248),rewrite(626(5),3(5))]. given #55 (T,wt=15): 652 e * (x * e) = y * (e * (y * (x * y))). [back_rewrite(216),rewrite(626(3)),flip(a)]. given #56 (A,wt=31): 524 e * (x * (y * (e * (y * (x * (y * (z * (x * u)))))))) = y * (x * (y * (z * (y * u)))). [back_rewrite(148),rewrite(397(9),403(10),3(11),403(8),397(10),3(10),3(9))]. given #57 (F,wt=47): 1235 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(406(a,2),795(a,1,2))]. given #58 (F,wt=47): 1236 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(406(a,2),795(a,2,2))]. given #59 (T,wt=15): 653 x * (e * (y * (x * (e * z)))) = y * z. [back_rewrite(171),rewrite(626(7),3(7))]. given #60 (T,wt=15): 712 e * (x * y) = x * (y * (e * (y * x))). [para(327(a,1),13(a,1)),rewrite(626(2),36(7)),flip(a)]. given #61 (A,wt=19): 577 x * (y * (e * (x * (z * (e * u))))) = z * (y * u). [back_rewrite(239),rewrite(403(8),403(10),3(11),397(8),3(11),403(13),444(15),3(7))]. given #62 (F,wt=39): 2127 c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))) != e * (c3 * (c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [back_rewrite(1325),rewrite(1950(21),1950(42),3(39))]. given #63 (F,wt=39): 2128 e * (c3 * (c4 * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [back_rewrite(1324),rewrite(1950(23),3(20),1950(40))]. given #64 (T,wt=15): 1104 e * x = x * (y * (x * (e * (y * e)))). [para(207(a,1),312(a,1,2)),flip(a)]. given #65 (T,wt=15): 1105 x * (y * (e * (x * (e * y)))) = y * e. [para(207(a,1),312(a,1))]. given #66 (A,wt=21): 643 e * (x * (e * (x * (e * (y * x))))) = x * (y * (e * x)). [back_rewrite(511),rewrite(626(8),3(8),3(7),626(6))]. given #67 (F,wt=39): 2202 c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [back_rewrite(791),rewrite(1950(21),1950(40))]. given #68 (F,wt=39): 2227 c4 * (c2 * (e * (c2 * (e * (c2 * (c4 * (c3 * (e * c1)))))))) != c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * (c3 * (e * c4)))))))). [back_rewrite(832),rewrite(2175(30),2175(49))]. given #69 (T,wt=15): 1113 x * (e * x) = y * (x * (e * (y * e))). [para(207(a,1),327(a,1)),flip(a)]. given #70 (T,wt=15): 1117 e * (x * e) = y * (x * (y * (e * y))). [para(327(a,1),207(a,2,2,2))]. given #71 (A,wt=29): 738 (x * y) * z = e * (x * (e * (x * (e * (y * (e * (x * (e * (x * (e * z)))))))))). [para(41(a,1),13(a,1,1)),rewrite(397(7),626(8),397(13),626(14)),flip(a)]. given #72 (F,wt=39): 2331 c4 * (c3 * (e * (c2 * (e * (c2 * (c4 * (c2 * (e * c1)))))))) != e * (c3 * (c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(577(a,2),2127(a,1,2,2,2,2,2,2,2)),rewrite(1932(19))]. given #73 (F,wt=39): 2333 c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))) != e * (c3 * (c1 * (c2 * (e * (c2 * (c1 * (c2 * (e * c4)))))))). [para(577(a,2),2127(a,2,2,2,2,2,2,2,2)),rewrite(1932(38))]. given #74 (T,wt=15): 1147 e * (x * (y * (x * e))) = y * (e * x). [para(312(a,1),406(a,2,2))]. given #75 (T,wt=15): 1151 e * (x * (y * x)) = x * (y * (e * y)). [para(327(a,1),406(a,1,2))]. given #76 (A,wt=53): 739 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(41(a,1),13(a,1,2,2)),rewrite(738(6),738(26),3(31))]. given #77 (F,wt=39): 2347 e * (c3 * (c4 * (c2 * (e * (c2 * (c4 * (c2 * (e * c1)))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(577(a,2),2128(a,1,2,2,2,2,2,2,2)),rewrite(1932(19))]. given #78 (F,wt=39): 2349 e * (c3 * (c4 * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (c1 * (c2 * (e * c4)))))))). [para(577(a,2),2128(a,2,2,2,2,2,2,2,2)),rewrite(1932(38))]. given #79 (T,wt=15): 1153 e * (x * (y * x)) = y * (e * (x * e)). [para(327(a,1),406(a,2,2))]. given #80 (T,wt=15): 1182 e * (x * (e * (y * e))) = x * (y * x). [back_rewrite(762),rewrite(1173(8))]. given #81 (A,wt=73): 741 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(41(a,1),13(a,2)),rewrite(738(5),3(21),738(20),738(39),3(55))]. given #82 (F,wt=39): 2540 c4 * (c3 * (e * (c2 * (e * (c2 * (c4 * (c2 * (e * c1)))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(577(a,2),2202(a,1,2,2,2,2,2,2,2)),rewrite(1932(19))]. given #83 (F,wt=39): 2541 c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (c1 * (c2 * (e * c4)))))))). [para(577(a,2),2202(a,2,2,2,2,2,2,2,2)),rewrite(1932(38))]. given #84 (T,wt=15): 1216 x * (e * (y * (x * (y * e)))) = e * y. [para(1140(a,1),380(a,1,2)),rewrite(7(5),738(5),312(11),3(9),3(8),41(6),3(6),3(3),738(11),3(21),1191(22)),flip(a)]. given #85 (T,wt=15): 1256 x * (y * (e * (y * (x * y)))) = e * x. [para(327(a,1),408(a,1,2,2,2))]. given #86 (A,wt=35): 744 e * (x * (e * (x * (e * (y * (e * (x * (e * (x * (e * (x * y))))))))))) = x * (e * (x * (y * y))). [back_rewrite(640),rewrite(738(10),3(15),3(12),3(11),3(8),41(8),3(8),3(9),738(8)),flip(a)]. given #87 (F,wt=39): 2555 c4 * (c2 * (e * (c2 * (c4 * (c2 * (e * (c3 * (e * c1)))))))) != c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * (c3 * (e * c4)))))))). [para(577(a,2),2227(a,1,2,2,2,2,2)),rewrite(1932(21))]. given #88 (F,wt=39): 2558 c4 * (c2 * (e * (c2 * (e * (c2 * (c4 * (c3 * (e * c1)))))))) != c1 * (c2 * (e * (c2 * (c1 * (c2 * (e * (c3 * (e * c4)))))))). [para(577(a,2),2227(a,2,2,2,2,2,2)),rewrite(1932(40))]. given #89 (T,wt=15): 1276 x * (e * (y * (x * y))) = e * (y * e). [para(457(a,1),380(a,1,2)),rewrite(41(5),3(5),738(3),41(9),3(9),3(6),312(7),3(5),7(4),41(10),3(10),41(12),3(12),738(11),816(26),655(12)),flip(a)]. given #90 (T,wt=15): 1309 x * (e * (x * (y * (e * y)))) = y * x. [para(532(a,2),312(a,1,2))]. given #91 (A,wt=29): 745 x * (y * (z * (e * (z * (e * (y * (e * (x * x)))))))) = z * (e * (z * (x * x))). [back_rewrite(564),rewrite(738(6),744(21),738(10),3(15),3(12),3(11),3(8),3(14),738(15),744(30))]. given #92 (F,wt=39): 2709 c4 * (c3 * (e * (c2 * (c4 * (c2 * (e * (c2 * (e * c1)))))))) != e * (c3 * (c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(577(a,2),2331(a,1,2,2,2,2,2)),rewrite(1932(21))]. ============================== PROOF ================================= % Proof 1 at 3.85 (+ 0.00) seconds. % Length of proof is 88. % Level of proof is 18. % Maximum clause weight is 51. % Given clauses 92. 1 ((x * y) * z) * u = ((u * y) * z) * x # label(goal). [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)]. 8 ((x * y) * x) * (e * y) = x * y. [para(4(a,1),2(a,1))]. 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)]. 11 (x * y) * ((x * z) * (y * u)) = z * u. [para(4(a,1),3(a,1,2))]. 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))]. 28 (((x * y) * x) * ((x * y) * y)) * e = x * y. [para(4(a,1),16(a,1,1))]. 30 (x * y) * (e * (y * x)) = x. [para(3(a,1),8(a,1,1,1)),rewrite(3(7))]. 36 (x * y) * x = e * (y * x). [para(30(a,1),3(a,1,2))]. 41 x * (e * (x * x)) = e * (x * x). [para(5(a,1),30(a,1,1)),rewrite(36(4),3(8),36(6))]. 42 e * ((x * x) * e) = x. [para(5(a,1),30(a,1,2,2)),rewrite(36(2),41(4),7(6),36(5))]. 43 (x * x) * (e * x) = e. [para(16(a,1),30(a,1,2,2)),rewrite(36(3),3(5))]. 51 ((e * (x * y)) * ((y * x) * x)) * e = y * x. [back_rewrite(28),rewrite(36(2))]. 57 (e * (x * x)) * x = e. [back_rewrite(5),rewrite(36(2))]. 58 (x * x) * e = e * x. [para(42(a,1),3(a,1,2)),flip(a)]. 61 ((x * e) * y) * z = x * (y * (x * z)). [para(3(a,1),9(a,1,2))]. 70 (e * ((x * (y * e)) * y)) * (y * (x * (y * z))) = y * (x * z). [para(9(a,1),9(a,2)),rewrite(61(5),36(5),61(10))]. 73 (x * e) * (x * x) = e. [para(43(a,1),4(a,1)),flip(a)]. 75 (e * x) * (x * x) = x * x. [para(43(a,1),30(a,1,1)),rewrite(3(8))]. 78 ((x * x) * y) * (e * z) = (e * x) * (y * z). [para(58(a,1),4(a,1,1)),flip(a)]. 82 (x * e) * e = x * x. [para(73(a,1),3(a,1,2))]. 108 (x * (e * (x * e))) * (x * (e * x)) = e. [para(10(a,2),43(a,1)),rewrite(36(4))]. 138 (x * x) * y = x * ((y * e) * (x * (e * y))). [para(82(a,1),10(a,2,1)),rewrite(61(8)),flip(a)]. 171 (x * x) * (x * (y * (x * (e * z)))) = y * z. [para(82(a,1),11(a,1,1)),rewrite(61(7))]. 185 (e * (x * y)) * ((x * x) * (y * y)) = (x * y) * (x * y). [para(4(a,1),75(a,1,2))]. 207 e * (x * y) = z * (x * (e * (z * y))). [para(30(a,1),12(a,1,2)),rewrite(36(2))]. 212 (x * y) * e = x * (y * (e * x)). [para(43(a,1),12(a,1,2))]. 239 ((x * y) * z) * (((x * (u * e)) * (y * u)) * v) = u * (z * v). [para(10(a,2),12(a,1,2,1))]. 255 (e * (x * y)) * (((y * x) * z) * u) = z * (y * u). [para(36(a,1),12(a,1,1))]. 271 ((x * y) * ((x * e) * z)) * ((y * z) * (y * z)) = (y * z) * (y * z). [para(12(a,2),75(a,1,1))]. 312 x * (y * (x * y)) = y * x. [back_rewrite(51),rewrite(212(8),3(10),255(8))]. 314 (e * x) * (x * (e * x)) = e. [back_rewrite(108),rewrite(312(5))]. 327 x * (y * x) = y * (x * y). [para(312(a,1),3(a,1,2))]. 368 x * ((e * x) * x) = e. [back_rewrite(314),rewrite(327(6))]. 372 (e * x) * x = x * e. [para(368(a,1),3(a,1,2)),flip(a)]. 380 x * (y * (e * x)) = z * (y * (x * (z * (e * x)))). [para(368(a,1),12(a,1,2)),rewrite(212(3),372(9),212(7))]. 397 (e * x) * y = e * (x * (e * y)). [para(7(a,1),13(a,1,1)),flip(a)]. 403 ((x * y) * z) * u = x * (z * (e * ((y * x) * (e * u)))). [para(30(a,1),13(a,1,1)),rewrite(397(4)),flip(a)]. 406 e * (x * (y * z)) = y * (x * (e * z)). [para(57(a,1),13(a,1,1)),rewrite(397(8),397(11),78(12),397(10),397(13),3(13),3(12))]. 434 (x * y) * (z * (y * x)) = e * (z * x). [para(13(a,2),36(a,1))]. 442 x * (y * (e * ((z * x) * (e * (x * ((z * (u * v)) * (e * ((u * x) * (e * (y * w)))))))))) = v * w. [para(13(a,2),11(a,1,2,1)),rewrite(403(8),403(14))]. 444 (x * y) * (z * (y * ((x * u) * (z * v)))) = u * v. [para(13(a,2),11(a,1))]. 516 e * ((x * y) * (e * (y * (z * (e * ((x * y) * (e * u))))))) = z * (y * u). [back_rewrite(255),rewrite(403(6),397(12))]. 521 e * ((x * y) * (e * ((x * x) * (y * y)))) = (x * y) * (x * y). [back_rewrite(185),rewrite(397(7))]. 532 e * (x * (y * (e * z))) = y * (x * z). [back_rewrite(70),rewrite(397(10),403(11),3(12),403(9),397(11),3(11),3(8),3(8),3(5),3(4))]. 564 x * (y * (e * ((z * y) * (e * ((z * x) * (z * x)))))) = (z * x) * (z * x). [back_rewrite(271),rewrite(403(9),403(13),3(14),397(11),3(14),3(13))]. 577 x * (y * (e * (x * (z * (e * u))))) = z * (y * u). [back_rewrite(239),rewrite(403(8),403(10),3(11),397(8),3(11),403(13),444(15),3(7))]. 624 c4 * (c3 * (e * ((c2 * c4) * (e * c1)))) != c1 * (c3 * (e * ((c2 * c1) * (e * c4)))). [back_rewrite(6),rewrite(403(7),403(20))]. 626 (x * x) * y = x * (e * (x * y)). [back_rewrite(138),rewrite(434(8))]. 627 x * (y * (e * ((z * u) * ((z * x) * (e * (y * v)))))) = u * v. [back_rewrite(442),rewrite(444(16))]. 640 e * ((x * y) * (e * (x * (e * (x * (y * y)))))) = (x * y) * (x * y). [back_rewrite(521),rewrite(626(6))]. 653 x * (e * (y * (x * (e * z)))) = y * z. [back_rewrite(171),rewrite(626(7),3(7))]. 663 c1 * (c3 * (e * ((c2 * c1) * (e * c4)))) != c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))). [para(4(a,1),624(a,1,2,2,2)),flip(a)]. 677 c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))) != c1 * (c3 * (e * ((c2 * e) * (c1 * c4)))). [para(4(a,1),663(a,1,2,2,2)),flip(a)]. 712 e * (x * y) = x * (y * (e * (y * x))). [para(327(a,1),13(a,1)),rewrite(626(2),36(7)),flip(a)]. 738 (x * y) * z = e * (x * (e * (x * (e * (y * (e * (x * (e * (x * (e * z)))))))))). [para(41(a,1),13(a,1,1)),rewrite(397(7),626(8),397(13),626(14)),flip(a)]. 744 e * (x * (e * (x * (e * (y * (e * (x * (e * (x * (e * (x * y))))))))))) = x * (e * (x * (y * y))). [back_rewrite(640),rewrite(738(10),3(15),3(12),3(11),3(8),41(8),3(8),3(9),738(8)),flip(a)]. 745 x * (y * (z * (e * (z * (e * (y * (e * (x * x)))))))) = z * (e * (z * (x * x))). [back_rewrite(564),rewrite(738(6),744(21),738(10),3(15),3(12),3(11),3(8),3(14),738(15),744(30))]. 791 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_rewrite(677),rewrite(738(10),3(23),3(25),738(33),3(46),3(48))]. 815 x * (y * (z * (e * (z * (e * (u * (x * (e * (z * (e * (z * (y * v)))))))))))) = u * v. [back_rewrite(627),rewrite(738(7),3(12),738(19),3(24),3(21),3(20),3(17),3(16),3(19))]. 896 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_rewrite(516),rewrite(738(8),3(13),3(20),738(20),3(25),3(32))]. 1140 e * (x * (y * e)) = y * (x * e). [para(7(a,1),406(a,2,2,2))]. 1151 e * (x * (y * x)) = x * (y * (e * y)). [para(327(a,1),406(a,1,2))]. 1161 e * (x * (y * z)) = u * (x * (y * (u * (e * z)))). [para(406(a,1),207(a,2,2,2))]. 1191 e * (x * (e * (x * (e * (x * (e * (x * (e * (y * (e * (x * e))))))))))) = x * (y * (x * e)). [para(312(a,1),380(a,2,2,2,2)),rewrite(738(8),3(18),738(24),3(29),41(28),3(28),3(26),3(23),312(24))]. 1216 x * (e * (y * (x * (y * e)))) = e * y. [para(1140(a,1),380(a,1,2)),rewrite(7(5),738(5),312(11),3(9),3(8),41(6),3(6),3(3),738(11),3(21),1191(22)),flip(a)]. 1310 e * (x * (y * (e * (y * x)))) = x * y. [para(532(a,2),312(a,1))]. 1321 e * (x * (y * (e * (z * (e * (x * u)))))) = y * (e * (z * u)). [para(207(a,2),532(a,2,2))]. 1325 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(532(a,2),791(a,2))]. 1905 e * (x * (y * (z * (x * (e * u))))) = y * (z * u). [para(653(a,1),406(a,2,2))]. 1924 x * (e * (x * (e * (y * (z * (e * (x * (e * (x * u))))))))) = y * (z * u). [back_rewrite(896),rewrite(1905(21),1905(17),3(12))]. 1932 x * (y * (z * (x * (y * u)))) = z * u. [back_rewrite(815),rewrite(1924(15))]. 1950 x * (e * (x * (e * (x * (e * (x * (e * y))))))) = e * (x * (e * (x * (e * (x * y))))). [para(1140(a,1),712(a,2,2,2)),rewrite(738(4),3(14),3(16),738(19),1216(25),3(21),3(20))]. 2127 c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))) != e * (c3 * (c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [back_rewrite(1325),rewrite(1950(21),1950(42),3(39))]. 2331 c4 * (c3 * (e * (c2 * (e * (c2 * (c4 * (c2 * (e * c1)))))))) != e * (c3 * (c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(577(a,2),2127(a,1,2,2,2,2,2,2,2)),rewrite(1932(19))]. 2709 c4 * (c3 * (e * (c2 * (c4 * (c2 * (e * (c2 * (e * c1)))))))) != e * (c3 * (c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(577(a,2),2331(a,1,2,2,2,2,2)),rewrite(1932(21))]. 2882 e * (x * (e * (x * (e * (x * (e * (x * y))))))) = x * (e * (x * (e * (x * (e * y))))). [para(1151(a,2),712(a,2,2,2,2)),rewrite(738(5),738(15),3(23),3(21),3(19),3(16),3(15),3(13),3(11),3(13),3(18),3(15),738(14),738(24),3(32),3(30),3(28),3(25),3(24),3(22),3(20)),flip(a)]. 3873 e * (x * (e * (x * (e * (x * (y * (e * (y * (e * x))))))))) = y * (e * (y * x)). [para(1151(a,2),745(a,1,2,2,2,2,2,2,2,2)),rewrite(3(14),738(13),3(18),41(17),3(17),738(14),3(23),3(21),41(19),3(19),3(17),3(15),41(13),3(13),3(10),3(10),738(14),1321(19),738(18),3(26),3(24),3(22),3(19),3(18),3(16),3(14),738(23),312(28),3(26),7(25),738(26),3(34),3(32),3(30),3(27),7(26),7(25),7(24),7(23),7(22),7(21),312(22),3(20))]. 3892 c4 * (c3 * (c1 * (c4 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))))) != e * (c3 * (c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(712(a,1),2709(a,1,2,2)),rewrite(738(28),738(41),3(49),738(50),3(58),3(56),3(54),738(51),3873(61),1310(49),738(42),3(51),3(49),3(49),3(47),3(45),1932(43),3(38),3(36),3(34),3(36),3(37),738(34),2882(46),738(43),738(56),3(64),3(62),3(60),738(57),1950(68),3(65),738(62),3(71),3(69),3(69),3(67),3(65),1932(63),1932(57),3(51),3(49),3(47),1932(45),3(40),1905(38),1905(32),3(25))]. 3893 $F. [resolve(3892,a,1161,a(flip))]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=92. Generated=12403. Kept=3891. proofs=1. Usable=48. Sos=2477. Demods=440. 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=948718. 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=8.85. User_CPU=3.85, System_CPU=0.00, Wall_clock=4. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3319 exit (max_proofs) Wed Nov 22 11:22:05 2006