============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 4309 was started by mccune on cleo, Tue Nov 3 09:37:44 2009 The command was "/home/mccune/LADR/bin/prover9 -f identity.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file identity.in assign(max_seconds,120). 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(non_clause) # 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: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ e, c1, c2, c3, c4, * ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). kept: 2 (x * e) * x = x. [assumption]. kept: 3 x * (x * y) = y. [assumption]. kept: 4 (x * y) * (z * u) = (x * z) * (y * u). [assumption]. kept: 5 ((x * x) * x) * x = e. [assumption]. kept: 6 ((c4 * c2) * c3) * c1 != ((c1 * c2) * c3) * c4. [deny(1)]. ============================== 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.01 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 (T,wt=9): 16 ((x * x) * x) * e = x. [para(5(a,1),3(a,1,2))]. given #8 (T,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 (T,wt=9): 43 (x * x) * (e * x) = e. [para(16(a,1),30(a,1,2,2)),rewrite([36(3),3(5)])]. given #13 (T,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 (F,wt=19): 100 ((c4 * c2) * c3) * c1 != ((c1 * (c3 * e)) * (c2 * c3)) * c4. [para(10(a,2),6(a,2,1))]. given #20 (F,wt=19): 101 ((c4 * c2) * c3) * c1 != ((c1 * c2) * (c4 * e)) * (c3 * c4). [para(10(a,2),6(a,2))]. given #21 (T,wt=9): 82 (x * e) * e = x * x. [para(73(a,1),3(a,1,2))]. given #22 (T,wt=11): 36 (x * y) * x = e * (y * x). [para(30(a,1),3(a,1,2))]. given #23 (T,wt=11): 75 (e * x) * (x * x) = x * x. [para(43(a,1),30(a,1,1)),rewrite([3(8)])]. given #24 (T,wt=11): 86 (x * x) * (x * e) = x * e. [para(73(a,1),30(a,1,1)),rewrite([3(8)])]. given #25 (A,wt=15): 11 (x * y) * ((x * z) * (y * u)) = z * u. [para(4(a,1),3(a,1,2))]. given #26 (F,wt=19): 129 ((c4 * c1) * (c2 * e)) * (c3 * c1) != ((c1 * c2) * c3) * c4. [para(4(a,1),99(a,1,1))]. given #27 (F,wt=19): 134 ((c4 * c2) * c3) * c1 != ((c1 * c4) * (c2 * e)) * (c3 * c4). [para(4(a,1),101(a,2,1))]. given #28 (F,wt=19): 192 ((c4 * c1) * c3) * ((c2 * e) * c1) != ((c1 * c2) * c3) * c4. [para(4(a,1),129(a,1))]. given #29 (F,wt=19): 196 ((c4 * c2) * c3) * c1 != ((c1 * c4) * c3) * ((c2 * e) * c4). [para(4(a,1),134(a,2))]. given #30 (T,wt=11): 112 (x * e) * (x * e) = e * x. [para(10(a,2),58(a,1)),rewrite([7(3)])]. given #31 (T,wt=9): 211 (e * x) * x = x * e. [para(112(a,1),30(a,1,1)),rewrite([112(8),3(6)])]. given #32 (T,wt=9): 218 (e * x) * (x * e) = x. [para(112(a,1),36(a,1,1)),rewrite([112(11),3(9)])]. given #33 (T,wt=11): 208 (x * e) * (e * x) = x * e. [para(112(a,1),3(a,1,2))]. given #34 (A,wt=15): 12 (x * y) * ((x * z) * u) = z * (y * u). [para(3(a,1),4(a,1,1)),flip(a)]. given #35 (F,wt=23): 126 ((c4 * (c3 * e)) * (c1 * e)) * ((c2 * c3) * c1) != ((c1 * c2) * c3) * c4. [para(10(a,2),98(a,1))]. given #36 (F,wt=21): 397 ((c4 * c1) * (c3 * c3)) * ((c2 * c3) * c1) != ((c1 * c2) * c3) * c4. [para(4(a,1),126(a,1,1)),rewrite([271(8),3(9)])]. given #37 (F,wt=21): 405 ((c4 * c3) * (c1 * c3)) * ((c2 * c3) * c1) != ((c1 * c2) * c3) * c4. [para(4(a,1),397(a,1,1))]. given #38 (F,wt=21): 406 ((c4 * c1) * (c2 * c3)) * ((c3 * c3) * c1) != ((c1 * c2) * c3) * c4. [para(4(a,1),397(a,1))]. given #39 (T,wt=11): 222 (e * x) * (x * (e * x)) = e. [back_rewrite(108),rewrite([215(5)])]. given #40 (T,wt=11): 223 e * (x * e) = x * (e * x). [para(3(a,1),211(a,1,1)),rewrite([36(7)]),flip(a)]. given #41 (T,wt=11): 239 (x * (y * y)) * y = x * x. [para(218(a,1),10(a,1,2)),rewrite([82(4),191(9),82(7)])]. given #42 (T,wt=11): 394 x * (y * (x * y)) = y * x. [back_rewrite(51),rewrite([271(8),3(10),313(8)])]. given #43 (A,wt=15): 13 (x * y) * (z * (y * u)) = (x * z) * u. [para(3(a,1),4(a,1,2)),flip(a)]. given #44 (F,wt=27): 889 c4 * (c3 * (e * ((c2 * c4) * (e * c1)))) != c1 * (c3 * (e * ((c2 * c1) * (e * c4)))). [back_rewrite(6),rewrite([554(7),554(20)])]. given #45 (F,wt=27): 968 c1 * (c3 * (e * ((c2 * c1) * (e * c4)))) != c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))). [para(4(a,1),889(a,1,2,2,2)),flip(a)]. given #46 (F,wt=27): 969 c4 * (c3 * (e * ((c2 * c4) * (e * c1)))) != c1 * (c3 * (e * ((c2 * e) * (c1 * c4)))). [para(4(a,1),889(a,2,2,2,2))]. given #47 (F,wt=27): 982 c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))) != c1 * (c3 * (e * ((c2 * e) * (c1 * c4)))). [para(4(a,1),968(a,1,2,2,2)),flip(a)]. given #48 (T,wt=11): 497 x * (y * x) = y * (x * y). [para(394(a,1),3(a,1,2))]. given #49 (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 #50 (T,wt=13): 343 e * (x * (y * e)) = y * (x * e). [para(112(a,1),12(a,1,2)),rewrite([274(4)]),flip(a)]. given #51 (T,wt=13): 1550 x * (e * (y * (x * e))) = y * e. [para(343(a,2),3(a,1,2))]. given #52 (A,wt=15): 267 e * (x * y) = z * (x * (e * (z * y))). [para(30(a,1),12(a,1,2)),rewrite([36(2)])]. given #53 (F,wt=47): 1093 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(1009),rewrite([1054(10),3(23),3(25),1054(35),3(48),1054(50),3(55),1054(62),3(67),3(64),3(63),3(60),3(59),3(57),956(55),956(51)])]. given #54 (F,wt=47): 1101 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(1000),rewrite([1054(10),3(18),3(25),1054(35),3(48),1054(50),3(55),1054(62),3(67),3(64),3(63),3(60),3(59),3(57),956(55),956(51)])]. given #55 (F,wt=47): 1110 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(990),rewrite([1054(12),3(25),1054(27),3(32),1054(39),3(44),3(41),3(40),3(37),3(36),3(34),956(32),956(28),1054(33),3(41),3(48)])]. given #56 (F,wt=47): 1120 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(978),rewrite([1054(10),3(18),3(25),1054(35),3(43),1054(50),3(55),1054(62),3(67),3(64),3(63),3(60),3(59),3(57),956(55),956(51)])]. given #57 (T,wt=15): 356 e * (x * (e * y)) = y * (x * (y * e)). [para(208(a,1),12(a,1,2)),rewrite([323(4)]),flip(a)]. given #58 (T,wt=15): 433 e * (x * e) = y * (x * (y * (e * y))). [para(222(a,1),12(a,1,2)),rewrite([36(4)])]. given #59 (T,wt=15): 625 e * (x * (e * (y * (x * y)))) = y * e. [para(13(a,2),211(a,1)),rewrite([548(5)])]. given #60 (T,wt=15): 630 e * (x * (e * (y * (x * (y * e))))) = y. [para(13(a,2),218(a,1)),rewrite([548(7)])]. given #61 (A,wt=17): 594 e * (x * (e * (y * (x * (y * y))))) = y * y. [para(13(a,2),75(a,1)),rewrite([548(6)])]. given #62 (F,wt=51): 1090 c4 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (x * (e * (c2 * (e * (c2 * (x * (c1 * c4)))))))))))). [back_rewrite(1012),rewrite([1054(10),3(23),3(25),1054(35),3(43),3(50)])]. given #63 (F,wt=51): 1091 c4 * (c3 * (c2 * (e * (c2 * (e * (x * (e * (c2 * (e * (c2 * (x * (c4 * c1)))))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))). [back_rewrite(1011),rewrite([1054(12),3(20),3(27),1054(35),3(48),3(50)])]. given #64 (F,wt=51): 1099 c4 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c2 * (e * (c2 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (x * (e * (c2 * (e * (c2 * (x * (c1 * c4)))))))))))). [back_rewrite(1002),rewrite([1054(10),3(18),3(25),1054(35),3(43),3(50)])]. given #65 (F,wt=51): 1108 c4 * (c3 * (c2 * (e * (c2 * (e * (x * (e * (c2 * (e * (c2 * (x * (c4 * c1)))))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [back_rewrite(992),rewrite([1054(12),3(20),3(27),1054(35),3(43),3(50)])]. given #66 (T,wt=15): 719 e * (x * (e * (y * e))) = y * (x * y). [back_rewrite(348),rewrite([548(5)])]. given #67 (T,wt=15): 733 e * (x * (e * (y * e))) = x * (y * x). [back_rewrite(238),rewrite([548(3),548(6),274(7),36(5)])]. given #68 (T,wt=15): 931 x * (e * (x * y)) = y * (e * (y * x)). [back_rewrite(679),rewrite([890(2)])]. given #69 (T,wt=15): 944 e * (x * e) = y * (e * (y * (x * y))). [back_rewrite(487),rewrite([890(3)]),flip(a)]. given #70 (A,wt=21): 714 e * (x * (e * (x * (e * (y * x))))) = x * (y * (e * x)). [back_rewrite(370),rewrite([632(4),548(7)])]. given #71 (F,wt=47): 1808 c4 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c1 * (e * (c1 * c2)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))). [para(931(a,1),1101(a,1,2,2,2,2,2,2,2,2))]. given #72 (F,wt=47): 1816 c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c4 * (e * (c4 * c2)))))))))) != c4 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * c1)))))))))). [para(931(a,1),1110(a,2,2,2,2,2,2,2,2,2)),flip(a)]. given #73 (F,wt=47): 1818 c4 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c1 * (e * (c1 * c2)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [para(931(a,1),1120(a,1,2,2,2,2,2,2,2,2))]. given #74 (F,wt=47): 1820 c4 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c2 * (e * (c2 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c4 * (e * (c4 * c2)))))))))). [para(931(a,1),1120(a,2,2,2,2,2,2,2,2,2))]. given #75 (T,wt=15): 953 x * (y * (e * (x * (y * z)))) = e * z. [back_rewrite(181),rewrite([890(3),3(6)])]. given #76 (T,wt=15): 954 x * (e * (y * (x * (e * z)))) = y * z. [back_rewrite(180),rewrite([890(7),3(7)])]. given #77 (T,wt=15): 956 e * (x * (y * (e * (x * z)))) = y * z. [back_rewrite(171),rewrite([890(3),3(6)])]. given #78 (T,wt=15): 963 x * (y * (z * (x * u))) = z * (y * u). [back_rewrite(923),rewrite([956(14),954(8)])]. given #79 (A,wt=21): 715 e * (x * (e * (x * (y * (e * x))))) = x * (e * (y * x)). [back_rewrite(369),rewrite([548(7),632(11)])]. given #80 (F,wt=47): 1970 c4 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c1 * (e * (c1 * c2)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c4 * (e * (c4 * c2)))))))))). [para(931(a,1),1818(a,2,2,2,2,2,2,2,2,2))]. given #81 (F,wt=47): 2087 c4 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c2 * (e * (c2 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c4 * (e * (c1 * c2)))))))))). [back_rewrite(1982),rewrite([2071(24),3(17)]),flip(a)]. given #82 (F,wt=47): 2088 c4 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c1 * (e * (c4 * c2)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [back_rewrite(1965),rewrite([2071(24),3(17)])]. given #83 (F,wt=47): 2089 c1 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c4 * (e * (c1 * c2)))))))))) != c4 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * c1)))))))))). [back_rewrite(1949),rewrite([2071(24),3(17)])]. given #84 (T,wt=15): 1034 e * (x * y) = x * (y * (e * (y * x))). [para(497(a,1),13(a,1)),rewrite([890(2),36(7)]),flip(a)]. given #85 (T,wt=15): 1465 e * (x * (e * (x * (y * x)))) = y * e. [back_rewrite(375),rewrite([1054(7),715(14),3(10),3(9),3(7)])]. given #86 (T,wt=15): 1563 e * x = x * (y * (x * (e * (y * e)))). [para(267(a,1),394(a,1,2)),flip(a)]. given #87 (T,wt=15): 1571 x * (e * x) = y * (x * (e * (y * e))). [para(267(a,1),497(a,1)),flip(a)]. given #88 (A,wt=17): 721 e * (x * (e * (y * y))) = y * (x * (y * y)). [back_rewrite(319),rewrite([548(4)])]. given #89 (F,wt=39): 2875 c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [back_rewrite(1093),rewrite([2488(21),2488(40)])]. given #90 (F,wt=43): 2503 c4 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c1 * (e * (c1 * c2)))))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(1034(a,1),1101(a,1,2,2,2,2,2,2,2,2,2)),rewrite([3(19),2488(44)])]. given #91 (F,wt=43): 2504 c4 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c2 * (e * (c2 * c1)))))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(1034(a,1),1101(a,1,2,2,2,2,2,2,2)),rewrite([1054(21),3(30),3(28),1054(26),3(34),41(33),3(32),1497(34),3(26),3(24),3(22),1054(19),3(28),3(26),1054(24),3(32),3(29),1742(29),3(27),3(25),3(23),3(20),2488(44)])]. given #92 (F,wt=43): 2513 c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c4 * (e * (c4 * c2)))))))))) != c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))). [para(1034(a,1),1110(a,2,2,2,2,2,2,2,2,2,2)),rewrite([2488(21),3(38)]),flip(a)]. given #93 (T,wt=15): 1619 e * (x * (y * (x * e))) = y * (e * x). [para(356(a,1),3(a,1,2))]. given #94 (T,wt=15): 1620 x * (e * (y * (e * x))) = y * (x * e). [para(356(a,2),3(a,1,2))]. given #95 (T,wt=15): 1657 e * (x * (y * (x * (e * x)))) = y * e. [para(433(a,1),3(a,1,2))]. given #96 (T,wt=15): 1658 x * (e * (y * e)) = y * (x * (e * x)). [para(433(a,2),3(a,1,2))]. given #97 (A,wt=17): 739 e * (x * (e * (y * x))) = x * (y * (x * x)). [back_rewrite(212),rewrite([548(4)])]. given #98 (F,wt=41): 3242 c4 * (c3 * (c1 * (e * (c1 * (e * (c4 * (c2 * c2))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [back_rewrite(2844),rewrite([3225(25),3(14)])]. given #99 (F,wt=37): 3350 c4 * (c3 * (c1 * (e * (c1 * (e * (c4 * (c2 * c2))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(1619(a,2),3242(a,2,2,2,2,2,2,2)),rewrite([1054(41),7(49),394(50),3(47),1054(44),3(53),3(51),1054(49),3(57),41(56),3(55),1497(57),3(49),3(47),3(45),3(42),1054(43),1054(56),3(64),3(62),3(60),1054(57),2488(68),2092(60),3(57),2092(56),2071(49),3(42),3(40),3(38),3(36),3(38),2488(38)])]. given #100 (F,wt=41): 3243 c4 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c2 * (e * (c2 * c1)))))))))) != c1 * (c3 * (c4 * (e * (c4 * (e * (c1 * (c2 * c2))))))). [back_rewrite(2841),rewrite([3225(25),3(14)]),flip(a)]. given #101 (F,wt=37): 3405 c1 * (c3 * (c4 * (e * (c4 * (e * (c1 * (c2 * c2))))))) != c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))). [para(1619(a,2),3243(a,1,2,2,2,2,2,2)),rewrite([1054(24),7(32),394(33),3(30),1054(27),3(36),3(34),1054(32),3(40),41(39),3(38),1497(40),3(32),3(30),3(28),3(25),1054(26),1054(39),3(47),3(45),3(43),1054(40),2488(51),2092(43),3(40),2092(39),2071(32),3(25),3(23),3(21),3(19),3(21),2488(21)]),flip(a)]. given #102 (T,wt=15): 1659 e * x = x * (y * (x * (y * (e * y)))). [para(433(a,1),394(a,1,2)),flip(a)]. given #103 (T,wt=15): 1662 x * (e * x) = y * (x * (y * (e * y))). [para(433(a,1),497(a,1)),flip(a)]. given #104 (T,wt=15): 1690 e * (x * (y * (x * (e * (y * e))))) = x. [para(267(a,1),630(a,1,2,2,2,2)),rewrite([3(12)])]. given #105 (T,wt=15): 1693 e * (x * (y * (x * (y * (e * y))))) = x. [para(433(a,1),630(a,1,2,2,2,2)),rewrite([3(11)])]. given #106 (A,wt=31): 744 e * (x * (y * (e * (y * (x * (y * (z * (x * u)))))))) = y * (x * (y * (z * (y * u)))). [back_rewrite(151),rewrite([548(9),554(10),3(11),554(8),548(10),3(10),3(9)])]. given #107 (F,wt=41): 3343 c4 * (c3 * (c1 * (e * (c1 * (e * (c4 * (c2 * c2))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c4 * (e * (c4 * c2)))))))))). [para(1034(a,1),3242(a,2,2,2,2,2,2,2,2,2,2)),rewrite([3(36)])]. given #108 (F,wt=41): 3353 c4 * (c3 * (c1 * (e * (c1 * (x * (c4 * (e * (x * (c2 * c2))))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(267(a,1),3350(a,1,2,2,2,2,2))]. given #109 (F,wt=37): 3761 c4 * (c3 * (c1 * (e * (c1 * (c2 * (c4 * (e * c2))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(3(a,1),3353(a,1,2,2,2,2,2,2,2,2))]. given #110 (F,wt=37): 3762 c4 * (c3 * (c1 * (e * (c4 * (e * (c1 * (c2 * c2))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(3(a,1),3353(a,1,2,2,2,2))]. given #111 (T,wt=15): 1741 e * (x * (y * x)) = y * (e * (x * e)). [para(719(a,1),3(a,1,2))]. given #112 (T,wt=15): 1742 x * (e * (y * (e * (x * e)))) = y * x. [para(719(a,2),3(a,1,2))]. given #113 (T,wt=15): 1745 x * (e * (x * (e * (y * e)))) = y * x. [para(719(a,2),394(a,1,2))]. given #114 (T,wt=15): 1767 e * (x * (y * x)) = x * (e * (y * e)). [para(733(a,1),3(a,1,2))]. given #115 (A,wt=23): 933 x * (e * (x * (y * (z * u)))) = x * (y * (z * (e * (x * u)))). [back_rewrite(674),rewrite([890(4)])]. given #116 (F,wt=37): 4062 c1 * (c3 * (e * (c2 * (c4 * (c2 * (c4 * (c2 * (c1 * e)))))))) != c4 * (c3 * (c1 * (e * (c1 * (e * (c4 * (c2 * c2))))))). [para(1745(a,2),3242(a,2,2,2,2,2,2,2)),rewrite([1054(48),3(56),3(54),3(52),1054(49),1054(62),3(70),3(68),3(66),1054(63),2488(74),3(71),2092(70),2092(64),3(58),3(56),3(54),3(56),3(54),3(52),1054(50),3(58),3(56),3(54),1054(51),2488(62),3(59),1054(56),3(65),3(63),1054(61),3(69),3(66),3(63),3(60),3(57),3(60),3(58),3(56),2488(56),3(53),3(51),3(49),3(47),3(44),3(41),3(38)]),flip(a)]. given #117 (F,wt=37): 4081 c1 * (c3 * (c4 * (e * (c4 * (e * (c1 * (c2 * c2))))))) != c4 * (c3 * (e * (c2 * (c1 * (c2 * (c1 * (c2 * (c4 * e)))))))). [para(1745(a,2),3243(a,1,2,2,2,2,2,2)),rewrite([1054(31),3(39),3(37),3(35),1054(32),1054(45),3(53),3(51),3(49),1054(46),2488(57),3(54),2092(53),2092(47),3(41),3(39),3(37),3(39),3(37),3(35),1054(33),3(41),3(39),3(37),1054(34),2488(45),3(42),1054(39),3(48),3(46),1054(44),3(52),3(49),3(46),3(43),3(40),3(43),3(41),3(39),2488(39),3(36),3(34),3(32),3(30),3(27),3(24),3(21)]),flip(a)]. given #118 (F,wt=37): 4374 c1 * (c3 * (c4 * (e * (c1 * (e * (c4 * (c2 * c2))))))) != c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))). [para(933(a,1),3405(a,1,2,2))]. given #119 (F,wt=37): 4418 c4 * (c3 * (c1 * (c2 * (c4 * (e * (c1 * (e * c2))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(933(a,1),3761(a,1,2,2))]. given #120 (T,wt=15): 1847 x * (y * (e * (y * (x * y)))) = e * x. [para(944(a,1),394(a,1,2))]. given #121 (T,wt=15): 1854 x * (e * (y * (e * (y * (x * y))))) = e. [para(944(a,1),1550(a,1,2,2)),rewrite([7(11)])]. given #122 (T,wt=15): 2032 x * (e * (y * e)) = x * (y * (e * y)). [para(719(a,1),954(a,1,2,2,2)),rewrite([3(8)]),flip(a)]. given #123 (T,wt=15): 2091 x * (y * (z * u)) = z * (y * (x * u)). [para(963(a,1),3(a,1,2))]. given #124 (A,wt=17): 945 e * (x * (y * (x * x))) = y * (e * (x * x)). [back_rewrite(483),rewrite([890(4),3(4)]),flip(a)]. given #125 (F,wt=37): 4419 c4 * (e * (c4 * (c3 * (c1 * (e * (c1 * (c2 * c2))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(933(a,2),3762(a,1))]. given #126 (F,wt=37): 4642 c1 * (c3 * (c4 * (c2 * (e * (c2 * (c4 * (c2 * (c1 * e)))))))) != c4 * (c3 * (c1 * (e * (c1 * (e * (c4 * (c2 * c2))))))). [para(744(a,2),4062(a,1,2,2,2)),rewrite([3(17),3(21)])]. given #127 (F,wt=37): 4650 c1 * (c3 * (e * (c2 * (c4 * (c2 * (c4 * (c2 * (c1 * e)))))))) != c4 * (c3 * (c1 * (e * (c4 * (e * (c1 * (c2 * c2))))))). [para(933(a,1),4062(a,2,2,2))]. given #128 (F,wt=37): 4674 c1 * (c3 * (c4 * (e * (c4 * (e * (c1 * (c2 * c2))))))) != c4 * (c3 * (c1 * (c2 * (e * (c2 * (c1 * (c2 * (c4 * e)))))))). [para(744(a,2),4081(a,2,2,2,2)),rewrite([3(34),3(38)])]. given #129 (T,wt=15): 2092 x * (y * (z * (x * (y * u)))) = z * u. [para(963(a,2),3(a,1,2))]. given #130 (T,wt=15): 2094 x * (y * (x * (z * (y * z)))) = z * x. [para(963(a,2),394(a,1,2))]. given #131 (T,wt=15): 2095 x * (y * (z * (x * (z * y)))) = y * z. [para(963(a,2),394(a,1))]. given #132 (T,wt=15): 2098 x * (y * (x * z)) = z * (y * (z * x)). [para(394(a,1),963(a,1,2,2))]. given #133 (A,wt=23): 1053 e * (x * (e * (x * (y * y)))) = e * (x * (y * (x * (e * y)))). [para(12(a,2),41(a,2,2)),rewrite([1042(6),1041(9),1042(5),899(13)])]. given #134 (F,wt=37): 4682 c1 * (c3 * (c4 * (e * (c1 * (e * (c4 * (c2 * c2))))))) != c4 * (c3 * (e * (c2 * (c1 * (c2 * (c1 * (c2 * (c4 * e)))))))). [para(933(a,1),4081(a,1,2,2))]. given #135 (F,wt=37): 4722 c1 * (e * (c1 * (c3 * (c4 * (e * (c4 * (c2 * c2))))))) != c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))). [para(933(a,2),4374(a,1))]. given #136 (F,wt=37): 4744 c4 * (c3 * (c1 * (c2 * (c4 * (c2 * (c1 * (c2 * e))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(1619(a,2),4418(a,1,2,2,2,2,2,2)),rewrite([3(16)])]. given #137 (F,wt=37): 4955 c4 * (e * (c1 * (c3 * (c1 * (e * (c4 * (c2 * c2))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(2091(a,1),3350(a,1,2))]. given #138 (T,wt=15): 2101 x * (y * (z * (x * z))) = y * (z * y). [para(963(a,2),497(a,1))]. given #139 (T,wt=15): 2103 x * (y * (x * (z * x))) = z * (y * z). [para(497(a,1),963(a,1,2,2))]. given #140 (T,wt=15): 3255 x * (y * (e * y)) = y * (x * (e * x)). [para(497(a,1),1658(a,1,2))]. given #141 (T,wt=15): 3872 e * (x * (y * x)) = x * (y * (e * y)). [para(1741(a,2),1658(a,1))]. given #142 (A,wt=29): 1054 (x * y) * z = e * (x * (e * (x * (e * (y * (e * (x * (e * (x * (e * z)))))))))). [para(41(a,1),13(a,1,1)),rewrite([548(7),890(8),548(13),890(14)]),flip(a)]. given #143 (F,wt=37): 4956 c1 * (c3 * (c4 * (e * (c1 * (e * (c4 * (c2 * c2))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(2091(a,1),3350(a,1))]. given #144 (F,wt=37): 4957 c4 * (c3 * (c1 * (e * (c1 * (e * (c4 * (c2 * c2))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (c1 * (c2 * (e * c4)))))))). [para(2091(a,1),3350(a,2,2,2,2,2,2,2))]. given #145 (F,wt=37): 4958 c4 * (c3 * (c1 * (e * (c1 * (e * (c4 * (c2 * c2))))))) != c1 * (c2 * (e * (c3 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(2091(a,1),3350(a,2,2))]. given #146 (F,wt=37): 4959 c4 * (c3 * (c1 * (e * (c1 * (e * (c4 * (c2 * c2))))))) != e * (c3 * (c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(2091(a,1),3350(a,2))]. given #147 (T,wt=15): 3897 x * (y * (e * (y * (e * (x * e))))) = y. [para(1745(a,2),3(a,1,2))]. given #148 (T,wt=15): 4179 e * (x * (y * x)) = e * (y * (x * y)). [para(1767(a,2),1741(a,2))]. given #149 (T,wt=15): 4835 x * (y * (z * (y * x))) = z * (x * y). [para(394(a,1),2091(a,1,2)),flip(a)]. given #150 (T,wt=15): 4838 x * (y * (z * y)) = z * (x * (y * x)). [para(497(a,1),2091(a,1,2)),flip(a)]. given #151 (A,wt=53): 1055 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([1054(6),1054(26),3(31)])]. given #152 (F,wt=37): 4965 c1 * (c3 * (c4 * (e * (c4 * (c2 * (c1 * (e * c2))))))) != c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))). [para(2091(a,1),3405(a,1,2,2,2,2,2))]. given #153 (F,wt=37): 4966 c1 * (e * (c4 * (c3 * (c4 * (e * (c1 * (c2 * c2))))))) != c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))). [para(2091(a,1),3405(a,1,2))]. given #154 (F,wt=37): 4967 c4 * (c3 * (c1 * (e * (c4 * (e * (c1 * (c2 * c2))))))) != c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))). [para(2091(a,1),3405(a,1))]. given #155 (F,wt=37): 4968 c4 * (c3 * (e * (c2 * (e * (c2 * (c4 * (c2 * (e * c1)))))))) != c1 * (c3 * (c4 * (e * (c4 * (e * (c1 * (c2 * c2))))))). [para(2091(a,1),3405(a,2,2,2,2,2,2,2)),flip(a)]. given #156 (T,wt=15): 5244 x * (y * (z * (y * (x * y)))) = z * x. [para(497(a,1),2092(a,1,2,2,2))]. given #157 (T,wt=15): 5376 x * (y * (z * (y * (x * (z * x))))) = y. [para(2094(a,2),3(a,1,2))]. given #158 (T,wt=15): 5386 x * (y * (x * (y * (z * y)))) = z * x. [para(497(a,1),2094(a,1,2,2,2))]. given #159 (T,wt=15): 6144 x * (y * (x * (z * x))) = y * (z * y). [para(497(a,1),2101(a,1,2,2))]. given #160 (A,wt=73): 1057 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([1054(5),3(21),1054(20),1054(39),3(55)])]. given #161 (F,wt=37): 4969 c1 * (c3 * (c4 * (e * (c4 * (e * (c1 * (c2 * c2))))))) != c4 * (c2 * (e * (c3 * (e * (c2 * (e * (c2 * (c4 * c1)))))))). [para(2091(a,1),3405(a,2,2))]. given #162 (F,wt=37): 4970 c1 * (c3 * (c4 * (e * (c4 * (e * (c1 * (c2 * c2))))))) != e * (c3 * (c4 * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))). [para(2091(a,1),3405(a,2))]. given #163 (F,wt=37): 4994 c4 * (c3 * (c1 * (e * (c4 * (c2 * (c1 * (e * c2))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(2091(a,1),3761(a,1,2,2,2,2))]. given #164 (F,wt=37): 4995 c4 * (c3 * (c1 * (c2 * (c1 * (e * (c4 * (e * c2))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(2091(a,1),3761(a,1,2,2,2))]. given #165 (T,wt=15): 6763 x * (y * (z * y)) = x * (z * (y * z)). [para(4179(a,1),2092(a,1,2,2,2,2)),rewrite([2092(9)])]. given #166 (T,wt=15): 7040 x * (y * (z * (y * (z * (x * z))))) = y. [para(2103(a,2),4835(a,1,2,2)),rewrite([3(8)])]. given #167 (T,wt=15): 7127 x * (y * (z * y)) = y * (x * (z * x)). [para(497(a,1),4838(a,1,2))]. given #168 (T,wt=17): 1577 x * (y * (e * (x * (z * e)))) = z * (y * e). [para(267(a,1),343(a,1))]. given #169 (A,wt=29): 1061 x * (y * (z * (e * (z * (e * (y * (e * (x * x)))))))) = z * (e * (z * (x * x))). [back_rewrite(816),rewrite([1054(6),1060(21),1054(10),3(15),3(12),3(11),3(8),3(14),1054(15),1060(30)])]. given #170 (F,wt=37): 4996 c4 * (e * (c1 * (c3 * (c1 * (c2 * (c4 * (e * c2))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(2091(a,1),3761(a,1,2))]. given #171 (F,wt=37): 4997 c1 * (c3 * (c4 * (e * (c1 * (c2 * (c4 * (e * c2))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(2091(a,1),3761(a,1))]. given #172 (F,wt=37): 4998 c4 * (c3 * (c1 * (e * (c1 * (c2 * (c4 * (e * c2))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (c1 * (c2 * (e * c4)))))))). [para(2091(a,1),3761(a,2,2,2,2,2,2,2))]. given #173 (F,wt=37): 4999 c4 * (c3 * (c1 * (e * (c1 * (c2 * (c4 * (e * c2))))))) != c1 * (c2 * (e * (c3 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(2091(a,1),3761(a,2,2))]. given #174 (T,wt=17): 1579 e * (x * (y * e)) = z * (x * (y * (z * e))). [para(343(a,1),267(a,2,2,2))]. given #175 (T,wt=17): 1629 e * (x * (e * y)) = y * (e * (y * (x * e))). [para(343(a,2),356(a,2,2))]. given #176 (T,wt=17): 1694 x * (e * (y * (x * (y * y)))) = e * (y * y). [para(594(a,1),3(a,1,2)),flip(a)]. given #177 (T,wt=17): 2018 x * (e * (y * (e * (x * x)))) = y * (x * x). [para(41(a,1),954(a,1,2,2,2))]. given #178 (A,wt=57): 1070 e * (x * (e * (x * (e * (y * (e * (x * (e * (x * (e * (z * (y * (u * (x * z)))))))))))))) = u * (e * (x * (e * (x * (e * (z * (e * (x * (e * (x * (e * u))))))))))). [back_rewrite(1035),rewrite([1054(6),1054(23)])]. given #179 (F,wt=37): 5000 c4 * (c3 * (c1 * (e * (c1 * (c2 * (c4 * (e * c2))))))) != e * (c3 * (c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(2091(a,1),3761(a,2))]. given #180 (F,wt=37): 5001 c4 * (c3 * (c4 * (e * (c1 * (e * (c1 * (c2 * c2))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(2091(a,1),3762(a,1,2,2))]. given #181 (F,wt=37): 5002 c4 * (e * (c1 * (c3 * (c4 * (e * (c1 * (c2 * c2))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(2091(a,1),3762(a,1,2))]. given #182 (F,wt=37): 5003 c1 * (c3 * (c4 * (e * (c4 * (e * (c1 * (c2 * c2))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(2091(a,1),3762(a,1))]. given #183 (T,wt=17): 2020 x * (e * (y * (z * e))) = y * (z * (x * e)). [para(1550(a,1),954(a,1,2,2,2))]. given #184 (T,wt=17): 2047 x * (y * (e * (y * (e * (x * y))))) = y * y. [para(714(a,2),954(a,1,2,2)),rewrite([3(11)])]. given #185 (T,wt=17): 2058 x * (e * (y * (z * e))) = x * (z * (y * e)). [para(343(a,1),956(a,1,2,2,2,2)),rewrite([3(10)])]. given #186 (T,wt=17): 2059 e * (x * (y * (z * (x * e)))) = y * (z * e). [para(343(a,1),956(a,1,2,2,2))]. given #187 (A,wt=35): 1071 e * (x * (e * (x * (e * (y * (e * (x * (e * (x * (e * (y * (z * y)))))))))))) = x * (e * (z * x)). [back_rewrite(1033),rewrite([1054(4)])]. given #188 (F,wt=37): 5004 c4 * (c3 * (c1 * (e * (c4 * (e * (c1 * (c2 * c2))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (c1 * (c2 * (e * c4)))))))). [para(2091(a,1),3762(a,2,2,2,2,2,2,2))]. given #189 (F,wt=37): 5005 c4 * (c3 * (c1 * (e * (c4 * (e * (c1 * (c2 * c2))))))) != c1 * (c2 * (e * (c3 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(2091(a,1),3762(a,2,2))]. given #190 (F,wt=37): 5006 c4 * (c3 * (c1 * (e * (c4 * (e * (c1 * (c2 * c2))))))) != e * (c3 * (c1 * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(2091(a,1),3762(a,2))]. given #191 (F,wt=37): 5027 c4 * (c3 * (c1 * (e * (c1 * (e * (c4 * (c2 * c2))))))) != c1 * (c3 * (e * (c2 * (c4 * (c2 * (c1 * (c2 * (c4 * e)))))))). [para(2091(a,1),4062(a,1,2,2,2,2,2,2)),flip(a)]. given #192 (T,wt=17): 2282 x * (e * (x * (e * (y * x)))) = y * (x * x). [para(714(a,2),963(a,1,2)),rewrite([3(11)])]. given #193 (T,wt=17): 2397 e * (x * (y * (x * x))) = x * (e * (y * x)). [para(963(a,1),715(a,1,2,2))]. given #194 (T,wt=17): 3103 e * (x * (y * e)) = x * (e * (y * (e * x))). [para(1619(a,2),497(a,1,2)),rewrite([1054(9),3(17),3(15),3(13),3(10),3(10),3(8),1054(8),3(17),3(15),3(15),3(13)])]. given #195 (T,wt=17): 3105 e * (x * (e * (x * (y * e)))) = y * (e * x). [para(343(a,2),1619(a,1,2,2))]. given #196 (A,wt=71): 1075 e * (x * (e * (x * (e * (y * (e * (x * (e * (x * (e * (x * (z * (u * (e * (u * (e * (x * (e * (u * (e * (u * (x * y)))))))))))))))))))))) = x * (z * (u * (e * (u * (e * (x * (e * (u * (e * (y * z)))))))))). [back_rewrite(1028),rewrite([1054(7),3(12),3(19),1054(18),1054(40),3(45),3(42),3(50)])]. given #197 (F,wt=37): 5028 c1 * (c2 * (e * (c3 * (c4 * (c2 * (c4 * (c2 * (c1 * e)))))))) != c4 * (c3 * (c1 * (e * (c1 * (e * (c4 * (c2 * c2))))))). [para(2091(a,1),4062(a,1,2))]. given #198 (F,wt=37): 5029 e * (c3 * (c1 * (c2 * (c4 * (c2 * (c4 * (c2 * (c1 * e)))))))) != c4 * (c3 * (c1 * (e * (c1 * (e * (c4 * (c2 * c2))))))). [para(2091(a,1),4062(a,1))]. given #199 (F,wt=37): 5030 c1 * (c3 * (e * (c2 * (c4 * (c2 * (c4 * (c2 * (c1 * e)))))))) != c4 * (c3 * (c1 * (e * (c1 * (c2 * (c4 * (e * c2))))))). [para(2091(a,1),4062(a,2,2,2,2,2,2))]. ============================== PROOF ================================= % Proof 1 at 32.39 (+ 0.06) seconds. % Length of proof is 134. % Level of proof is 24. % Maximum clause weight is 67.000. % Given clauses 199. 1 ((x * y) * z) * u = ((u * y) * z) * x # label(non_clause) # 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)])]. 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))]. 66 (x * (y * z)) * (e * ((x * z) * ((x * e) * y))) = (x * e) * y. [para(9(a,1),30(a,1,1))]. 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))]. 99 ((c4 * c2) * (c1 * e)) * (c3 * c1) != ((c1 * c2) * c3) * c4. [para(10(a,2),6(a,1))]. 108 (x * (e * (x * e))) * (x * (e * x)) = e. [para(10(a,2),43(a,1)),rewrite([36(4)])]. 112 (x * e) * (x * e) = e * x. [para(10(a,2),58(a,1)),rewrite([7(3)])]. 129 ((c4 * c1) * (c2 * e)) * (c3 * c1) != ((c1 * c2) * c3) * c4. [para(4(a,1),99(a,1,1))]. 141 (x * x) * y = x * ((y * e) * (x * (e * y))). [para(82(a,1),10(a,2,1)),rewrite([61(8)]),flip(a)]. 153 ((e * x) * y) * ((x * x) * z) = (x * x) * (y * z). [para(75(a,1),4(a,1,1)),flip(a)]. 159 x * ((y * z) * ((y * x) * u)) = z * u. [para(3(a,1),11(a,1,1))]. 171 e * (x * (y * (x * ((x * x) * z)))) = y * z. [para(73(a,1),11(a,1,1)),rewrite([61(7)])]. 180 (x * x) * (x * (y * (x * (e * z)))) = y * z. [para(82(a,1),11(a,1,1)),rewrite([61(7)])]. 191 (x * (y * z)) * (z * y) = (x * e) * y. [back_rewrite(66),rewrite([159(9)])]. 192 ((c4 * c1) * c3) * ((c2 * e) * c1) != ((c1 * c2) * c3) * c4. [para(4(a,1),129(a,1))]. 211 (e * x) * x = x * e. [para(112(a,1),30(a,1,1)),rewrite([112(8),3(6)])]. 215 x * (e * (x * e)) = e * x. [para(112(a,1),10(a,2)),rewrite([82(4),3(2)])]. 218 (e * x) * (x * e) = x. [para(112(a,1),36(a,1,1)),rewrite([112(11),3(9)])]. 222 (e * x) * (x * (e * x)) = e. [back_rewrite(108),rewrite([215(5)])]. 226 (e * x) * ((x * y) * y) = (x * y) * e. [para(211(a,1),4(a,1)),flip(a)]. 234 (x * (e * y)) * ((x * z) * (y * e)) = z * y. [para(211(a,1),11(a,1,2,2))]. 235 (e * x) * ((x * y) * e) = (x * y) * y. [para(211(a,1),11(a,1,2))]. 238 ((e * x) * y) * x = x * (y * x). [para(218(a,1),10(a,1,1)),flip(a)]. 239 (x * (y * y)) * y = x * x. [para(218(a,1),10(a,1,2)),rewrite([82(4),191(9),82(7)])]. 267 e * (x * y) = z * (x * (e * (z * y))). [para(30(a,1),12(a,1,2)),rewrite([36(2)])]. 271 (x * y) * e = x * (y * (e * x)). [para(43(a,1),12(a,1,2))]. 274 (x * y) * (e * x) = x * (y * e). [para(58(a,1),12(a,1,2))]. 307 (x * y) * (x * x) = e * (y * e). [para(82(a,1),12(a,1,2))]. 313 (e * (x * y)) * (((y * x) * z) * u) = z * (y * u). [para(36(a,1),12(a,1,1))]. 343 e * (x * (y * e)) = y * (x * e). [para(112(a,1),12(a,1,2)),rewrite([274(4)]),flip(a)]. 348 (e * x) * (y * e) = y * (x * y). [para(211(a,1),12(a,1,2))]. 369 (e * x) * (x * (y * (e * x))) = (x * y) * y. [back_rewrite(235),rewrite([271(5)])]. 370 (e * x) * ((x * y) * y) = x * (y * (e * x)). [back_rewrite(226),rewrite([271(8)])]. 394 x * (y * (x * y)) = y * x. [back_rewrite(51),rewrite([271(8),3(10),313(8)])]. 433 e * (x * e) = y * (x * (y * (e * y))). [para(222(a,1),12(a,1,2)),rewrite([36(4)])]. 489 ((x * (y * y)) * z) * ((x * x) * u) = y * (z * u). [para(239(a,1),12(a,1,2,1))]. 495 (x * (e * (y * e))) * (x * (e * (y * e))) = (x * x) * y. [para(239(a,1),239(a,1,1)),rewrite([307(5),307(10)]),flip(a)]. 497 x * (y * x) = y * (x * y). [para(394(a,1),3(a,1,2))]. 548 (e * x) * y = e * (x * (e * y)). [para(7(a,1),13(a,1,1)),flip(a)]. 554 ((x * y) * z) * u = x * (z * (e * ((y * x) * (e * u)))). [para(30(a,1),13(a,1,1)),rewrite([548(4)]),flip(a)]. 589 (x * y) * (z * (y * x)) = e * (z * x). [para(13(a,2),36(a,1))]. 594 e * (x * (e * (y * (x * (y * y))))) = y * y. [para(13(a,2),75(a,1)),rewrite([548(6)])]. 627 e * ((x * (e * y)) * (e * z)) = (x * e) * (y * (x * z)). [para(211(a,1),13(a,1,1)),rewrite([548(8),548(11)]),flip(a)]. 632 (x * y) * y = x * (e * (y * x)). [para(218(a,1),13(a,1,2)),rewrite([271(7),548(7),3(7)])]. 674 (x * x) * (y * (z * u)) = x * (y * (z * (e * (x * u)))). [para(239(a,1),13(a,1,1)),rewrite([554(8),78(10),548(9),3(12)])]. 714 e * (x * (e * (x * (e * (y * x))))) = x * (y * (e * x)). [back_rewrite(370),rewrite([632(4),548(7)])]. 715 e * (x * (e * (x * (y * (e * x))))) = x * (e * (y * x)). [back_rewrite(369),rewrite([548(7),632(11)])]. 719 e * (x * (e * (y * e))) = y * (x * y). [back_rewrite(348),rewrite([548(5)])]. 733 e * (x * (e * (y * e))) = x * (y * x). [back_rewrite(238),rewrite([548(3),548(6),274(7),36(5)])]. 742 (x * e) * (y * (x * ((x * x) * z))) = (x * x) * (y * z). [back_rewrite(153),rewrite([548(3),548(8),627(10)])]. 763 x * (y * (e * (z * (x * (e * ((z * z) * ((x * x) * u))))))) = z * (y * u). [back_rewrite(489),rewrite([554(6),554(8),3(9)])]. 853 c1 * (c3 * (e * ((c2 * c1) * (e * c4)))) != c4 * (c3 * (e * ((c1 * c4) * (e * ((c2 * e) * c1))))). [back_rewrite(192),rewrite([554(11),554(24)]),flip(a)]. 890 (x * x) * y = x * (e * (x * y)). [back_rewrite(141),rewrite([589(8)])]. 923 x * (y * (e * (z * (x * (e * (z * (e * (z * (x * (e * (x * u))))))))))) = z * (y * u). [back_rewrite(763),rewrite([890(5),890(8)])]. 925 (x * e) * (y * (e * (x * z))) = x * (e * (x * (y * z))). [back_rewrite(742),rewrite([890(4),3(7),890(10)])]. 933 x * (e * (x * (y * (z * u)))) = x * (y * (z * (e * (x * u)))). [back_rewrite(674),rewrite([890(4)])]. 943 (x * (e * (y * e))) * (x * (e * (y * e))) = x * (e * (x * y)). [back_rewrite(495),rewrite([890(13)])]. 954 x * (e * (y * (x * (e * z)))) = y * z. [back_rewrite(180),rewrite([890(7),3(7)])]. 956 e * (x * (y * (e * (x * z)))) = y * z. [back_rewrite(171),rewrite([890(3),3(6)])]. 963 x * (y * (z * (x * u))) = z * (y * u). [back_rewrite(923),rewrite([956(14),954(8)])]. 1034 e * (x * y) = x * (y * (e * (y * x))). [para(497(a,1),13(a,1)),rewrite([890(2),36(7)]),flip(a)]. 1054 (x * y) * z = e * (x * (e * (x * (e * (y * (e * (x * (e * (x * (e * z)))))))))). [para(41(a,1),13(a,1,1)),rewrite([548(7),890(8),548(13),890(14)]),flip(a)]. 1141 e * (x * (e * (x * (e * (y * (e * (y * (e * (y * (e * (y * (e * (x * (e * (x * (e * (x * (e * (y * e))))))))))))))))))) = x * (e * (x * y)). [back_rewrite(943),rewrite([1054(11),1054(21),3(29),3(27),3(25),1054(22),3(32),3(34),3(32),3(30)])]. 1151 e * (x * (e * (x * (e * (x * (e * (x * (e * (y * (e * (x * z))))))))))) = x * (e * (x * (y * z))). [back_rewrite(925),rewrite([1054(7),3(17)])]. 1171 e * (x * (e * (x * (e * (x * (e * (x * (e * (x * (e * y)))))))))) = x * (e * (x * y)). [back_rewrite(890),rewrite([1054(2)])]. 1201 c4 * (c3 * (c1 * (e * (c1 * (e * (c4 * (e * (c1 * (e * (c1 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * c1))))))))))))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [back_rewrite(853),rewrite([1054(10),3(18),3(25),1054(35),3(48),3(50),1054(47),3(66)]),flip(a)]. 1488 e * (x * (e * (x * (e * (y * (e * x)))))) = e * (y * e). [back_rewrite(307),rewrite([1054(3),41(9),3(9),3(6)])]. 1509 e * (x * (e * (x * (y * (e * (z * (e * (x * (e * (x * (e * (y * e)))))))))))) = z * y. [back_rewrite(234),rewrite([1054(7),1054(23),3(28),3(25),3(24),3(21),3(20),1054(17),3(26),3(24),3(24),3(22),3(20)])]. 1563 e * x = x * (y * (x * (e * (y * e)))). [para(267(a,1),394(a,1,2)),flip(a)]. 1571 x * (e * x) = y * (x * (e * (y * e))). [para(267(a,1),497(a,1)),flip(a)]. 1657 e * (x * (y * (x * (e * x)))) = y * e. [para(433(a,1),3(a,1,2))]. 1660 e * (x * (e * (x * (y * (e * (y * (e * (y * (x * (e * (x * (e * y)))))))))))) = y * (e * (x * (e * (x * (y * (e * (y * (e * (y * (x * e)))))))))). [para(433(a,2),394(a,1,2,2)),rewrite([1054(9),3(14),3(11),7(10),1054(11),3(16),1054(17),3(25),3(23),3(21),3(18),3(17),3(15),3(13),3(15),1054(21),1054(31),3(36),1054(37),3(45),3(43),3(41),3(38),3(37),3(35),3(33),3(35)]),flip(a)]. 1695 e * (x * (y * (e * (y * (e * (x * e)))))) = e * y. [para(343(a,2),594(a,1,2,2,2,2,2)),rewrite([1054(9),7(14),394(15),3(13),3(11),41(10),3(10),3(7),1054(8),1488(17),3(11),3(13),1054(16),394(22),3(20),3(19),41(17),3(17),3(14)])]. 1742 x * (e * (y * (e * (x * e)))) = y * x. [para(719(a,2),3(a,1,2))]. 1745 x * (e * (x * (e * (y * e)))) = y * x. [para(719(a,2),394(a,1,2))]. 1910 e * (x * (e * (x * (e * (y * (e * (x * (e * (x * (e * (y * (e * (x * y))))))))))))) = x * (e * (x * (e * (y * y)))). [para(719(a,2),714(a,1,2,2,2,2,2)),rewrite([3(13),1054(10),3(26),1054(23),1151(32),956(18),1742(12),3(6),3(11),1054(13)]),flip(a)]. 2017 x * (e * (x * (e * (y * (e * x))))) = y * e. [para(497(a,1),954(a,1,2,2)),rewrite([1054(4),3(13),3(11),3(11),3(9),1054(12),3(21),3(19),394(18),3(17),3(15)])]. 2058 x * (e * (y * (z * e))) = x * (z * (y * e)). [para(343(a,1),956(a,1,2,2,2,2)),rewrite([3(10)])]. 2091 x * (y * (z * u)) = z * (y * (x * u)). [para(963(a,1),3(a,1,2))]. 2092 x * (y * (z * (x * (y * u)))) = z * u. [para(963(a,2),3(a,1,2))]. 2094 x * (y * (x * (z * (y * z)))) = z * x. [para(963(a,2),394(a,1,2))]. 2095 x * (y * (z * (x * (z * y)))) = y * z. [para(963(a,2),394(a,1))]. 2101 x * (y * (z * (x * z))) = y * (z * y). [para(963(a,2),497(a,1))]. 2103 x * (y * (x * (z * x))) = z * (y * z). [para(497(a,1),963(a,1,2,2))]. 2346 x * (y * (z * (u * (w * v5)))) = w * (y * (x * (u * (z * v5)))). [para(963(a,1),963(a,1,2,2,2)),flip(a)]. 2351 x * (y * (z * (u * (y * (x * w))))) = z * (u * w). [para(963(a,2),963(a,1,2))]. 2376 e * (x * (e * (x * (e * (y * (e * (x * (e * (y * x))))))))) = x * (e * (x * (e * y))). [para(497(a,1),715(a,2,2,2)),rewrite([1054(9),1910(24),1054(12),3(17),3(14),3(13),3(10),3(9),3(6),3(10),1054(12),3(17),3(14)]),flip(a)]. 2389 e * (x * (e * (x * (y * (e * (y * (x * x))))))) = x * (e * (x * y)). [para(733(a,1),715(a,2,2,2)),rewrite([3(21),1054(18),1054(28),3(36),3(34),3(32),1054(29),3(39),3(41),3(39),3(37),1141(38),1054(13),3(18),3(15),3(14),3(11),1054(11),3(19),3(17),3(15),1054(12),394(19),3(17),7(16),7(15),7(14),394(15),3(13),3(11),3(9),3(7),3(8),1054(14),3(19),3(16),1054(18),3(26),3(24),3(22),1054(19),3(29),1151(30),3(19),3(17),3(15)]),flip(a)]. 2392 e * (x * (e * (x * (e * (x * (e * (x * (y * (e * (y * (e * x))))))))))) = x * (e * (x * (e * (x * (e * (x * (e * (y * (e * (y * (x * x))))))))))). [para(714(a,1),715(a,2,2,2)),rewrite([3(27),1054(24),1054(34),3(42),3(40),3(38),1054(35),1171(42),3(30),3(29),1054(26),3(35),3(33),1054(31),3(36),394(33),2376(40),3(33),3(31),3(29),3(30),3(28),3(26),3(28),1054(25),1171(34),3(19),1054(20),3(29),3(27),1054(25),3(30),3(27),3(26),1054(25),3(33),3(31),3(29),1054(26),2092(32),2092(28),41(24),3(24),3(25),3(23),3(21),3(23),3(21),3(19),3(21),1054(31),3(36),3(33),1054(35),3(43),3(41),3(39),1054(36),2017(42),1054(39),3(47),3(45),3(43),1054(40),1742(46),2376(48),3(41),3(39),3(37),3(38),3(36),3(34)]),flip(a)]. 2488 x * (e * (x * (e * (x * (e * (x * (e * y))))))) = e * (x * (e * (x * (e * (x * y))))). [para(343(a,1),1034(a,2,2,2)),rewrite([1054(4),3(14),3(16),1054(19),2095(25),3(21),3(20)])]. 2538 e * (x * (e * (x * (e * (x * (e * (x * y))))))) = x * (e * (x * (e * (x * (e * y))))). [para(733(a,1),1034(a,2,2,2)),rewrite([1054(6),3(15),3(13),1054(11),3(16),3(17),3(19),3(17),3(15),3(19),1054(18),3(27),3(25),1054(23),3(28),3(25),3(27),3(29),3(27),3(25)])]. 2618 x * (e * (x * (e * (x * (e * (y * (e * (y * (e * x))))))))) = x * y. [back_rewrite(2392),rewrite([2538(18),2488(32),2389(27),3(21),3(20)])]. 2844 c4 * (c3 * (c1 * (e * (c1 * (e * (c4 * (e * (c1 * (e * (c1 * (c2 * (e * (c2 * (e * (c2 * c1))))))))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [back_rewrite(1201),rewrite([2488(29),3(26)])]. 2933 e * (x * (e * (x * (y * (e * (y * (x * (e * (x * (e * (x * (y * (e * (y * (x * (e * (x * (e * y)))))))))))))))))) = y * (e * y). [para(1563(a,2),394(a,1,2,2)),rewrite([1054(9),3(14),1054(15),3(20),2095(18),3(13),1054(13),3(21),3(19),3(17),1054(14),394(21),3(19),7(18),7(17),7(16),394(17),3(15),3(13),3(11),3(9),3(10),2095(8),3(3),1054(10),1054(20),3(25),1054(26),3(34),3(32),3(30),1054(27),3(37),2488(37),3(35),3(33),3(31),3(29),3(30)]),flip(a)]. 2953 e * (x * (e * (x * (y * (e * (y * (e * (x * (e * (x * y)))))))))) = e * (y * y). [para(1563(a,2),714(a,1,2,2,2,2,2)),rewrite([3(18),1054(15),1054(25),3(30),1054(31),3(39),3(37),3(35),1054(32),3(42),2488(42),3(40),3(38),3(36),3(34),3(35),2933(35),394(12),1054(10),1054(20),3(25),1695(23),1054(17),3(25),3(23),3(21),1054(18),2017(26),3(21),3(23),3(21),3(19),3(21),1509(21),2092(17),3(12),1054(11),7(16),394(17),3(15),1054(12),1054(22),3(30),3(28),3(26),1054(23),3(33),2618(31),3(21),3(19),3(17),3(19)]),flip(a)]. 2975 x * (e * (y * (e * (y * (x * (e * (x * (e * (x * (y * e)))))))))) = e * (y * (e * (y * (e * (x * (e * (x * y))))))). [para(1571(a,2),394(a,1,2,2)),rewrite([1054(9),394(14),3(12),7(11),1054(12),3(20),3(18),3(16),1054(13),3(23),2488(23),3(21),3(19),3(17),3(15),1054(22),1054(32),3(40),3(38),3(36),1054(33),3(43),2618(41),3(31),3(29),3(27)])]. 3000 e * (x * (e * (x * (y * (e * (y * (e * (y * (x * (e * (x * (e * y)))))))))))) = e * (x * (e * (x * (e * (y * (e * (y * x))))))). [back_rewrite(1660),rewrite([2975(35)])]. 3225 x * (e * (x * (y * (e * (y * (e * (y * x))))))) = e * (y * y). [para(1657(a,1),394(a,1,2,2)),rewrite([1054(9),1054(19),3(24),1695(22),1054(16),3(21),715(21),1054(17),3(26),3(24),3(24),3(22),3(20),3(17),3(16),3(13),3(12),3(14),3(15),1054(18),7(23),394(24),3(22),1054(19),1054(29),3(34),1054(35),3(43),3(41),3(39),3(36),3(35),3(33),3(31),3(33),3000(33),3(27),2953(27)])]. 3242 c4 * (c3 * (c1 * (e * (c1 * (e * (c4 * (c2 * c2))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [back_rewrite(2844),rewrite([3225(25),3(14)])]. 4062 c1 * (c3 * (e * (c2 * (c4 * (c2 * (c4 * (c2 * (c1 * e)))))))) != c4 * (c3 * (c1 * (e * (c1 * (e * (c4 * (c2 * c2))))))). [para(1745(a,2),3242(a,2,2,2,2,2,2,2)),rewrite([1054(48),3(56),3(54),3(52),1054(49),1054(62),3(70),3(68),3(66),1054(63),2488(74),3(71),2092(70),2092(64),3(58),3(56),3(54),3(56),3(54),3(52),1054(50),3(58),3(56),3(54),1054(51),2488(62),3(59),1054(56),3(65),3(63),1054(61),3(69),3(66),3(63),3(60),3(57),3(60),3(58),3(56),2488(56),3(53),3(51),3(49),3(47),3(44),3(41),3(38)]),flip(a)]. 4217 x * (e * (x * (y * (z * (u * (e * (x * w))))))) = x * (y * (z * (u * w))). [para(267(a,2),933(a,2,2,2,2,2)),rewrite([3(15)])]. 4835 x * (y * (z * (y * x))) = z * (x * y). [para(394(a,1),2091(a,1,2)),flip(a)]. 5030 c1 * (c3 * (e * (c2 * (c4 * (c2 * (c4 * (c2 * (c1 * e)))))))) != c4 * (c3 * (c1 * (e * (c1 * (c2 * (c4 * (e * c2))))))). [para(2091(a,1),4062(a,2,2,2,2,2,2))]. 5282 x * (y * (z * (e * (z * (x * (y * u)))))) = z * (e * (z * u)). [para(933(a,2),2092(a,1,2,2))]. 6472 e * (x * (e * (x * (e * (x * (e * (y * (e * (y * (e * (y * (e * (x * (e * (x * (e * z)))))))))))))))) = e * (x * (e * (x * (y * (e * (y * (x * (y * (e * (y * (x * (e * (x * (e * z)))))))))))))). [para(714(a,1),1054(a,1,1)),rewrite([1054(5),1054(15),3(20),1054(21),3(29),3(27),3(25),3(24),3(22),3(20),3(21),3(40),3(38),1054(36),3(41),1054(42),3(50),3(48),3(46),1054(43),2538(52),1054(50),3(59),3(57),1054(55),3(60),5282(61),2538(60),3(59),3(57),3(55),3(56),3(54),3(52),2538(53),3(52),3(50)]),flip(a)]. 7036 x * (e * (x * (e * (x * (e * (y * (e * (y * (e * (y * (e * (x * (e * z))))))))))))) = e * (x * (e * (x * (y * (e * (y * (e * (y * (x * z))))))))). [para(2103(a,1),4835(a,1,2,2)),rewrite([394(5),1054(4),1054(14),3(19),5282(17),2092(14),3(14),1054(17),1054(27),3(32),5282(33),2538(32)]),flip(a)]. 7089 e * (x * (e * (x * (y * (e * (y * (x * (y * (e * (y * (x * (e * (x * (e * z)))))))))))))) = x * (e * (x * (y * (e * (y * (e * (y * (e * z)))))))). [back_rewrite(6472),rewrite([7036(25),3(9),3(17)]),flip(a)]. 10027 x * (e * (y * (e * (z * (y * z))))) = x * (z * e). [para(2101(a,2),2058(a,1,2,2)),rewrite([7(11)])]. 11356 c4 * (c3 * (c1 * (c2 * (e * (c2 * (c4 * (c2 * (c1 * e)))))))) != c1 * (c3 * (e * (c2 * (c4 * (c2 * (c4 * (c2 * (c1 * e)))))))). [para(2094(a,2),5030(a,2,2,2,2,2)),rewrite([1054(42),1054(55),3(63),1054(64),3(72),3(70),3(68),3(67),3(65),3(63),3(64),7089(64),1054(54),2092(63),1054(59),3(67),2351(64),3(57),2092(55),1054(48),3(57),3(55),3(55),3(53),3(51),4217(50),10027(41),3(38),3(39)]),flip(a)]. 11357 $F. [resolve(11356,a,2346,a(flip))]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=199. Generated=41708. Kept=11355. proofs=1. Usable=113. Sos=7978. Demods=1057. Limbo=24, Disabled=3244. Hints=0. Kept_by_rule=0, Deleted_by_rule=2784. Forward_subsumed=27569. Back_subsumed=578. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=2152 (2 lex), Back_demodulated=2661. Back_unit_deleted=0. Demod_attempts=4207510. Demod_rewrites=726218. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=26.23. User_CPU=32.39, System_CPU=0.06, Wall_clock=33. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 4309 exit (max_proofs) Tue Nov 3 09:38:17 2009