============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 4310 was started by mccune on cleo, Tue Nov 3 09:38:17 2009 The command was "/home/mccune/LADR/bin/prover9 -f identity2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file identity2.in assign(max_seconds,30). formulas(sos). (x * e) * x = x. x * (x * y) = y. (x * y) * (z * u) = (x * z) * (y * u). ((x * x) * x) * x = e. x * (x \ y) = y. x \ (x * y) = y. (x / y) * y = x. (x * y) / y = x. 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]. x * (x \ y) = y. [assumption]. x \ (x * y) = y. [assumption]. (x / y) * y = x. [assumption]. (x * y) / y = x. [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 x * (x \ y) = y. [assumption]. kept: 7 x \ (x * y) = y. [assumption]. kept: 8 (x / y) * y = x. [assumption]. kept: 9 (x * y) / y = x. [assumption]. kept: 10 ((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 x * (x \ y) = y. [assumption]. 7 x \ (x * y) = y. [assumption]. 8 (x / y) * y = x. [assumption]. 9 (x * y) / y = x. [assumption]. 10 ((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]. 6 x * (x \ y) = y. [assumption]. 7 x \ (x * y) = y. [assumption]. 8 (x / y) * y = x. [assumption]. 9 (x * y) / y = x. [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=7): 6 x * (x \ y) = y. [assumption]. given #6 (I,wt=7): 8 (x / y) * y = x. [assumption]. given #7 (I,wt=7): 9 (x * y) / y = x. [assumption]. given #8 (I,wt=15): 10 ((c4 * c2) * c3) * c1 != ((c1 * c2) * c3) * c4. [deny(1)]. given #9 (A,wt=5): 11 e * e = e. [para(2(a,1),2(a,1,1)),rewrite([3(5)]),flip(a)]. given #10 (T,wt=7): 26 x \ y = x * y. [para(6(a,1),3(a,1,2)),flip(a)]. given #11 (T,wt=7): 28 (x / y) * x = y. [para(8(a,1),3(a,1,2))]. % Operation / is commutative; C redundancy checks enabled. given #12 (T,wt=7): 31 x / x = x * e. [para(2(a,1),9(a,1,1))]. given #13 (T,wt=7): 32 x / (y * x) = y. [para(3(a,1),9(a,1,1))]. given #14 (A,wt=13): 12 ((x * y) * x) * (e * y) = x * y. [para(4(a,1),2(a,1))]. given #15 (T,wt=7): 40 x / y = y / x. [para(28(a,1),9(a,1,1))]. given #16 (T,wt=9): 20 ((x * x) * x) * e = x. [para(5(a,1),3(a,1,2))]. given #17 (T,wt=9): 34 e / x = (x * x) * x. [para(5(a,1),9(a,1,1))]. given #18 (T,wt=9): 42 x / e = (x * x) * x. [para(5(a,1),32(a,1,2))]. given #19 (A,wt=15): 13 ((x * e) * y) * (x * z) = x * (y * z). [para(2(a,1),4(a,1,1)),flip(a)]. given #20 (T,wt=9): 58 x * ((x * e) * e) = x. [para(34(a,1),32(a,1)),rewrite([13(8)])]. given #21 (T,wt=9): 76 (x * e) * e = x * x. [para(58(a,1),3(a,1,2)),flip(a)]. given #22 (T,wt=9): 79 (x * e) * (x * x) = e. [para(76(a,1),3(a,1,2))]. given #23 (T,wt=9): 86 (x * x) * (e * x) = e. [para(79(a,1),4(a,1)),flip(a)]. given #24 (A,wt=15): 14 (x * (y * e)) * (z * y) = (x * z) * y. [para(2(a,1),4(a,1,2)),flip(a)]. given #25 (F,wt=19): 113 ((c4 * (c3 * e)) * (c2 * c3)) * c1 != ((c1 * c2) * c3) * c4. [para(14(a,2),10(a,1,1))]. given #26 (F,wt=19): 114 ((c4 * c2) * (c1 * e)) * (c3 * c1) != ((c1 * c2) * c3) * c4. [para(14(a,2),10(a,1))]. given #27 (F,wt=19): 115 ((c4 * c2) * c3) * c1 != ((c1 * (c3 * e)) * (c2 * c3)) * c4. [para(14(a,2),10(a,2,1))]. given #28 (F,wt=19): 116 ((c4 * c2) * c3) * c1 != ((c1 * c2) * (c4 * e)) * (c3 * c4). [para(14(a,2),10(a,2))]. given #29 (T,wt=9): 88 (x * x) * e = e * x. [para(86(a,1),3(a,1,2))]. given #30 (T,wt=9): 89 (e * (x * x)) * x = e. [para(3(a,1),86(a,1,2)),rewrite([35(5)])]. given #31 (T,wt=9): 126 (e * x) * (x * e) = x. [para(14(a,2),20(a,1)),rewrite([11(4),88(3)])]. given #32 (T,wt=9): 162 x / e = e * (x * x). [back_rewrite(42),rewrite([97(4)])]. given #33 (A,wt=15): 15 (x * y) * ((x * z) * (y * u)) = z * u. [para(4(a,1),3(a,1,2))]. given #34 (F,wt=19): 172 ((c4 * c1) * (c2 * e)) * (c3 * c1) != ((c1 * c2) * c3) * c4. [para(4(a,1),114(a,1,1))]. given #35 (F,wt=19): 177 ((c4 * c2) * c3) * c1 != ((c1 * c4) * (c2 * e)) * (c3 * c4). [para(4(a,1),116(a,2,1))]. given #36 (F,wt=19): 229 ((c4 * c1) * c3) * ((c2 * e) * c1) != ((c1 * c2) * c3) * c4. [para(4(a,1),172(a,1))]. given #37 (F,wt=19): 233 ((c4 * c2) * c3) * c1 != ((c1 * c4) * c3) * ((c2 * e) * c4). [para(4(a,1),177(a,2))]. given #38 (T,wt=9): 164 e / x = e * (x * x). [back_rewrite(34),rewrite([97(4)])]. given #39 (T,wt=9): 189 (e * x) * x = x * e. [para(126(a,1),3(a,1,2))]. given #40 (T,wt=9): 193 x / (x * e) = e * x. [para(126(a,1),32(a,1,2)),rewrite([40(3)])]. given #41 (T,wt=11): 44 (x * y) * (e * (y * x)) = x. [para(3(a,1),12(a,1,1,1)),rewrite([3(7)])]. given #42 (A,wt=15): 16 (x * y) * ((x * z) * u) = z * (y * u). [para(3(a,1),4(a,1,1)),flip(a)]. given #43 (F,wt=23): 169 ((c4 * (c3 * e)) * (c1 * e)) * ((c2 * c3) * c1) != ((c1 * c2) * c3) * c4. [para(14(a,2),113(a,1))]. given #44 (F,wt=21): 426 ((c4 * c1) * (c3 * c3)) * ((c2 * c3) * c1) != ((c1 * c2) * c3) * c4. [para(4(a,1),169(a,1,1)),rewrite([395(8),163(11),3(10)])]. given #45 (F,wt=21): 434 ((c4 * c3) * (c1 * c3)) * ((c2 * c3) * c1) != ((c1 * c2) * c3) * c4. [para(4(a,1),426(a,1,1))]. given #46 (F,wt=21): 435 ((c4 * c1) * (c2 * c3)) * ((c3 * c3) * c1) != ((c1 * c2) * c3) * c4. [para(4(a,1),426(a,1))]. given #47 (T,wt=11): 50 (x * (x / y)) * (e * y) = x. [para(8(a,1),12(a,1,1,1)),rewrite([8(7)])]. given #48 (T,wt=11): 51 (x * (y / x)) * (e * y) = x. [para(28(a,1),12(a,1,1,1)),rewrite([28(7)])]. given #49 (T,wt=11): 78 (x * x) * (x * e) = x * e. [para(76(a,1),2(a,1,1))]. given #50 (T,wt=11): 97 (x * y) * x = e * (y * x). [para(3(a,1),14(a,1,1)),flip(a)]. given #51 (A,wt=15): 17 (x * y) * (z * (y * u)) = (x * z) * u. [para(3(a,1),4(a,1,2)),flip(a)]. given #52 (F,wt=27): 863 c4 * (c3 * (e * ((c2 * c4) * (e * c1)))) != c1 * (c3 * (e * ((c2 * c1) * (e * c4)))). [back_rewrite(10),rewrite([596(7),596(20)])]. given #53 (F,wt=27): 910 c1 * (c3 * (e * ((c2 * c1) * (e * c4)))) != c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))). [para(4(a,1),863(a,1,2,2,2)),flip(a)]. given #54 (F,wt=27): 911 c4 * (c3 * (e * ((c2 * c4) * (e * c1)))) != c1 * (c3 * (e * ((c2 * e) * (c1 * c4)))). [para(4(a,1),863(a,2,2,2,2))]. given #55 (F,wt=27): 924 c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))) != c1 * (c3 * (e * ((c2 * e) * (c1 * c4)))). [para(4(a,1),910(a,1,2,2,2)),flip(a)]. given #56 (T,wt=11): 190 x * (e * (x * e)) = e * x. [para(3(a,1),126(a,1,1)),rewrite([97(4)])]. given #57 (T,wt=11): 247 e * (x * e) = x * (e * x). [para(3(a,1),189(a,1,1)),rewrite([97(7)]),flip(a)]. given #58 (T,wt=11): 266 x / (e * (y * x)) = x * y. [para(44(a,1),32(a,1,2)),rewrite([40(4)])]. given #59 (T,wt=11): 471 (e * x) / y = y * (x / y). [para(51(a,1),32(a,1,2))]. given #60 (A,wt=23): 19 (x * (y * z)) * (u * (w * v5)) = (x * u) * ((y * w) * (z * v5)). [para(4(a,1),4(a,1,2)),flip(a)]. given #61 (F,wt=29): 761 c4 * ((c2 * c3) * (e * ((c3 * c4) * (c3 * c1)))) != c1 * (c3 * (e * ((c2 * c1) * (e * c4)))). [back_rewrite(442),rewrite([596(13),3(15),596(22)])]. given #62 (F,wt=29): 796 (x * c3) * ((x * ((c1 * c2) * (c4 * e))) * c4) != c4 * (c3 * (e * ((c2 * c4) * (e * c1)))). [back_rewrite(332),rewrite([596(7)]),flip(a)]. given #63 (F,wt=29): 800 (x * c3) * ((x * ((c4 * c2) * (c1 * e))) * c1) != c1 * (c3 * (e * ((c2 * c1) * (e * c4)))). [back_rewrite(328),rewrite([596(20)])]. given #64 (F,wt=29): 1193 c4 * ((c2 * e) * (c3 * ((c3 * c4) * (c3 * c1)))) != c1 * (c3 * (e * ((c2 * c1) * (e * c4)))). [para(4(a,1),761(a,1,2))]. given #65 (T,wt=11): 864 (x * (y * y)) * y = x * x. [back_rewrite(196),rewrite([597(6),395(4),163(5),3(5)]),flip(a)]. given #66 (T,wt=11): 975 e * (x * (e * x)) = x * e. [para(247(a,1),3(a,1,2))]. given #67 (T,wt=11): 979 (x * e) / (x * (e * x)) = e. [para(247(a,1),32(a,1,2))]. given #68 (T,wt=11): 1011 x / (e * y) = x * (x / y). [para(28(a,1),266(a,1,2,2))]. given #69 (A,wt=15): 30 (x * (y / z)) * (u * z) = (x * u) * y. [para(8(a,1),4(a,1,2)),flip(a)]. given #70 (F,wt=27): 1262 c1 * (c3 * (e * ((c2 * c1) * (e * c4)))) != c4 * ((c2 * e) * (e * (c3 * (c4 * c1)))). [para(4(a,1),1193(a,1,2,2,2)),rewrite([865(12),3(15)]),flip(a)]. given #71 (F,wt=27): 1524 c4 * ((c2 * e) * (e * (c3 * (c4 * c1)))) != c1 * (c3 * (e * ((c2 * e) * (c1 * c4)))). [para(4(a,1),1262(a,1,2,2,2)),flip(a)]. given #72 (F,wt=29): 1194 c4 * ((c2 * c3) * (e * ((c3 * c4) * (c3 * c1)))) != c1 * (c3 * (e * ((c2 * e) * (c1 * c4)))). [para(4(a,1),761(a,2,2,2,2))]. given #73 (F,wt=29): 1209 (x * c3) * ((x * ((c1 * c2) * (c4 * e))) * c4) != c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))). [para(4(a,1),796(a,2,2,2,2))]. given #74 (T,wt=11): 1285 x / (y * y) = y * (x * x). [para(864(a,1),32(a,1,2))]. given #75 (T,wt=11): 1606 (x * x) / y = x * (y * y). [para(1285(a,1),40(a,1)),flip(a)]. given #76 (T,wt=13): 135 (x * (e * x)) * (e * (x * x)) = e. [para(14(a,2),79(a,1)),rewrite([88(3)])]. given #77 (T,wt=13): 163 x * (e * (x * x)) = e * (x * x). [back_rewrite(37),rewrite([97(2),97(6)])]. given #78 (A,wt=13): 264 x * (e * (y * (x / y))) = x / y. [para(8(a,1),44(a,1,1))]. given #79 (F,wt=47): 1770 c4 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (c3 * (c4 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))). [back_rewrite(1545),rewrite([1671(12),3(20),3(21),1671(35),3(48),1671(50),3(55),1671(62),3(67),3(64),3(63),3(60),3(59),3(57),522(55),522(51)])]. given #80 (F,wt=47): 1781 c4 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (c3 * (c4 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [back_rewrite(1532),rewrite([1671(12),3(22),1671(24),3(29),3(26),3(25),3(22),3(21),522(20),522(16),1671(12),3(20),3(21),1671(33),3(41),3(48)])]. given #81 (F,wt=47): 2130 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(951),rewrite([1671(10),3(23),3(25),1671(35),3(48),1671(50),3(55),1671(62),3(67),3(64),3(63),3(60),3(59),3(57),522(55),522(51)])]. given #82 (F,wt=47): 2138 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(942),rewrite([1671(10),3(18),3(25),1671(35),3(48),1671(50),3(55),1671(62),3(67),3(64),3(63),3(60),3(59),3(57),522(55),522(51)])]. given #83 (T,wt=13): 265 x * (e * (y * (y / x))) = y / x. [para(28(a,1),44(a,1,1))]. given #84 (T,wt=13): 459 e * (x * (y * e)) = y * (x * e). [para(50(a,1),14(a,1,1)),rewrite([162(5),163(7),302(9),420(11),395(7),11(9),3(10)]),flip(a)]. Demod_increase_limit: e * (x * (e * (x * (y * (e * (y * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (u * (e * (u * (e * (e * (e * (e * (e * (e * (e * (u * (e * (u * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (w * (e * (w * (e * (e * (e * (e * (e * (e * (e * (w * (e * (w * (e * (e * (e * (e * (e * (e * (e * (v5 * (e * (v5 * (e * (e * (e * (e * (e * (e * (e * (w * (e * (w * (e * (e * (e * (e * (e * (e * (e * (w * (e * (w * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (u * (e * (u * (e * (e * (e * (e * (e * (e * (e * (u * (e * (u * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (u * (e * (u * (e * (e * (e * (e * (e * (e * (e * (u * (e * (u * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (w * (e * (w * (e * (e * (e * (e * (e * (e * (e * (w * (e * (w * (e * (e * (e * (e * (e * (e * (e * (v5 * (e * (v5 * (e * (e * (e * (e * (e * (e * (e * (w * (e * (w * (e * (e * (e * (e * (e * (e * (e * (w * (e * (w * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (u * (e * (u * (e * (e * (e * (e * (e * (e * (e * (u * (e * (u * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * ((u * (e * (u * (e * (z * (e * (z * (e * (z * (e * (z * (e * (w * (e * (w * (e * (v5 * (e * (w * (e * (w * (e * (z * (e * (z * (e * (z * (e * (z * (e * (u * (e * (u * (e * (z * (e * (z * (e * (z * (e * (z * (y * y)))))))))))))))))))))))))))))))))))))))))) * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (u * (e * (u * (e * (u * (e * (u * (e * (z * (e * (w * (e * (w * (e * (w * (e * (w * (e * (v5 * (e * (v5 * (e * (w * (e * (w * (e * (w * (e * (w * (e * (z * (e * (z * (e * (z * (e * (u * (e * (z * (e * (w * (e * (w * (e * (w * (e * (w * (e * (v5 * (e * (v5 * (e * (w * (e * (w * (e * (w * (e * (w * (e * (z * (e * (z * (u * (e * (u * (e * (u * (e * (y * (e * (y * (x * (e * (x * (e * (u * v5))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) = e * (x * (e * (x * (z * (e * (z * (e * (w * (e * (z * (e * (z * (x * (e * (x * (e * y)))))))))))))))). [back_rewrite(1881),rewrite([2559(21),1671(59),3(64),1671(65),3(73),3(71),3(69),1671(66),1671(76),3(84),3(82),3(80),1671(77),1671(87),3(95),3(93),3(91),1671(88),1671(98),3(106),3(104),3(102),1671(99),1671(109),3(117),3(115),3(113),1671(110),3(126),3(124),3(122),3(124),3(122),3(120),3(122),3(120),3(118),3(120),3(118),3(116),3(118),3(116),3(114),3(116),1671(113),1713(120),3(110),3(111),3(108),3(107),1671(104),3(113),3(111),1671(109),3(114),3(111),1671(113),3(121),3(119),3(117),1671(114),1671(124),3(132),3(130),3(128),1671(125),1671(135),3(143),3(141),3(139),1671(136),1671(146),3(154),3(152),3(150),1671(147),3(163),3(161),3(159),3(161),3(159),3(157),3(159),3(157),3(155),3(157),3(155),3(153),3(155),3(153),3(151),3(153),1671(150),1713(157),3(147),3(148),3(145),3(144),1671(141),3(150),3(148),1671(146),3(151),3(148),1671(150),3(158),3(156),3(154),1671(151),1671(161),3(169),3(167),3(165),1671(162),1671(172),3(180),3(178),3(176),1671(173),1671(183),3(191),3(189),3(187),1671(184),3(200),3(198),3(196),3(198),3(196),3(194),3(196),3(194),3(192),3(194),3(192),3(190),3(192),3(190),3(188),3(190),1671(200),3(205),1671(206),3(214),3(212),3(210),1671(207),1671(217),3(225),3(223),3(221),1671(218),1713(225),3(220),3(217),3(216),1671(213),3(222),3(220),1671(218),3(223),3(220),3(219),1671(218),3(226),3(224),3(222),1671(219),1671(229),3(237),3(235),3(233),1671(230),1671(240),3(248),3(246),3(244),1671(241),1671(251),3(259),3(257),3(255),1671(252),1671(262),3(270),3(268),3(266),1671(263),1713(270),3(260),2094(258),3(256),3(253),3(252),1671(249),3(258),3(256),1671(254),3(259),1671(260),3(268),3(266),3(264),1671(261),1671(271),3(279),3(277),3(275),1671(272),1671(282),3(290),3(288),3(286),1671(283),1671(293),3(301),3(299),3(297),1671(294),1671(304),3(312),3(310),3(308),1671(305),1671(315),3(323),3(321),3(319),1671(316),1671(326),3(334),3(332),3(330),1671(327),1671(337),3(345),3(343),3(341),1671(338),1713(345),3(335),3(336),3(333),3(332),1671(329),3(338),3(336),1671(334),3(339),3(336),1671(338),3(346),3(344),3(342),1671(339),1671(349),3(357),3(355),3(353),1671(350),1671(360),3(368),3(366),3(364),1671(361),1671(371),3(379),3(377),3(375),1671(372),1671(382),3(390),3(388),3(386),1671(383),1671(393),3(401),3(399),3(397),1671(394),1671(404),3(412),3(410),3(408),1671(405),1671(415),3(423),3(421),3(419),1671(416),1713(423),3(413),2094(411),3(400),522(398),522(394),522(390),3(385),3(384),1671(384),3(392),3(390),3(388),1671(385),1671(395),3(403),3(401),3(399),1671(396),1671(406),3(414),3(412),3(410),1671(407),1671(417),3(425),3(423),3(421),1671(418),1671(428),3(436),3(434),3(432),1671(429),1671(439),3(447),3(445),3(443),1671(440),1671(450),3(458),3(456),3(454),1671(451),1671(461),3(469),3(467),3(465),1671(462),1671(472),3(480),3(478),3(476),1671(473),1713(480),3(470),3(471),3(468),3(467),1671(464),3(473),3(471),1671(469),3(474),3(471),1671(473),3(481),3(479),3(477),1671(474),1671(484),3(492),3(490),3(488),1671(485),1671(495),3(503),3(501),3(499),1671(496),1671(506)])]. Demod_increase_limit (steps=371, size=1113). The most recent kept clause is 2621. From here on, a short message will be printed for each 100 times the limit is hit. given #85 (T,wt=13): 2543 x * (e * (y * (x * e))) = y * e. [para(459(a,2),3(a,1,2))]. given #86 (T,wt=15): 378 e * (x * y) = z * (x * (e * (z * y))). [para(44(a,1),16(a,1,2)),rewrite([97(2)])]. given #87 (A,wt=15): 520 x * (y * (z * u)) = z * (y * (x * u)). [para(28(a,1),17(a,1,1)),rewrite([513(6)])]. given #88 (F,wt=47): 2147 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(932),rewrite([1671(12),3(25),1671(27),3(32),1671(39),3(44),3(41),3(40),3(37),3(36),3(34),522(32),522(28),1671(33),3(41),3(48)])]. given #89 (F,wt=47): 2156 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(920),rewrite([1671(10),3(18),3(25),1671(35),3(43),1671(50),3(55),1671(62),3(67),3(64),3(63),3(60),3(59),3(57),522(55),522(51)])]. given #90 (F,wt=47): 2759 c4 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * (c3 * (c2 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))). [para(520(a,1),1770(a,1,2,2,2,2,2,2,2,2))]. given #91 (F,wt=47): 2760 c4 * (e * (c2 * (e * (c2 * (e * (c2 * (c3 * (c2 * (e * (c4 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))). [para(520(a,1),1770(a,1,2,2,2,2,2,2,2))]. given #92 (T,wt=15): 522 x * (y * (z * (x * (y * u)))) = z * u. [para(28(a,1),17(a,2,1)),rewrite([513(5)])]. given #93 (T,wt=15): 561 e * (x * (e * (y * (x * (y * e))))) = y. [para(17(a,2),126(a,1)),rewrite([519(7)])]. given #94 (T,wt=15): 659 x * (y * (z * (x * u))) = z * (y * u). [back_rewrite(295),rewrite([513(3)])]. given #95 (T,wt=15): 674 e * (x * (e * (y * e))) = y * (x * y). [back_rewrite(368),rewrite([519(5)])]. given #96 (A,wt=17): 563 e * (x * (y * (x * x))) = y * (e * (x * x)). [para(126(a,1),17(a,1,2)),rewrite([395(2),302(10),519(10),3(13)])]. given #97 (F,wt=47): 2761 c2 * (e * (c4 * (e * (c2 * (e * (c2 * (e * (c2 * (c3 * (c4 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))). [para(520(a,1),1770(a,1))]. given #98 (F,wt=47): 2762 c4 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (c3 * (c4 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * c4)))))))))). [para(520(a,1),1770(a,2,2,2,2,2,2,2,2,2))]. given #99 (F,wt=47): 2763 c4 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (c3 * (c4 * c1)))))))))) != c1 * (e * (c2 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))). [para(520(a,1),1770(a,2,2))]. given #100 (F,wt=47): 2764 c4 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (c3 * (c4 * c1)))))))))) != c2 * (c3 * (c1 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))). [para(520(a,1),1770(a,2))]. given #101 (T,wt=15): 675 e * (x * (e * y)) = y * (x * (y * e)). [back_rewrite(346),rewrite([519(3)])]. given #102 (T,wt=15): 682 e * (x * (e * (y * e))) = x * (y * x). [back_rewrite(195),rewrite([519(3),519(6),335(7),97(5)])]. given #103 (T,wt=11): 3239 x * (y * x) = y * (x * y). [para(682(a,1),190(a,2)),rewrite([1671(13),11(18),190(19),3(17),1671(14),3(23),3(21),1671(19),3(24),3(25),3(27),3(25),3(23),3(25),1671(22),1671(32),3(40),3(38),3(36),1671(33),3(43),3(45),3(43),3(41),2998(42)])]. given #104 (T,wt=11): 3284 x * (y * (x * y)) = y * x. [para(3239(a,1),3(a,1,2))]. given #105 (A,wt=31): 669 e * (x * (y * (e * (y * (x * (y * (z * (x * u)))))))) = y * (x * (y * (z * (y * u)))). [back_rewrite(421),rewrite([519(9),596(10),3(11),596(8),519(10),3(10),3(9)])]. given #106 (F,wt=47): 2765 c4 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * (c3 * (c2 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [para(520(a,1),1781(a,1,2,2,2,2,2,2,2,2))]. given #107 (F,wt=47): 2766 c4 * (e * (c2 * (e * (c2 * (e * (c2 * (c3 * (c2 * (e * (c4 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [para(520(a,1),1781(a,1,2,2,2,2,2,2,2))]. given #108 (F,wt=47): 2767 c2 * (e * (c4 * (e * (c2 * (e * (c2 * (e * (c2 * (c3 * (c4 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [para(520(a,1),1781(a,1))]. given #109 (F,wt=47): 2768 c4 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (c3 * (c4 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * (e * (c2 * c4)))))))))). [para(520(a,1),1781(a,2,2,2,2,2))]. given #110 (T,wt=15): 906 e * (x * e) = y * (e * (y * (x * y))). [back_rewrite(341),rewrite([865(3)]),flip(a)]. given #111 (T,wt=15): 1625 x * (y * (e * (y * (x * (e * x))))) = y. [para(1606(a,1),32(a,1)),rewrite([1282(5),865(4),3(4)])]. given #112 (T,wt=15): 1629 x * (y * (e * y)) = y * (x * (e * x)). [para(1606(a,1),1285(a,1)),rewrite([865(3),3(3),865(7),3(7)])]. given #113 (T,wt=15): 2101 x * (e * (y * e)) = x * (y * (e * y)). [back_rewrite(994),rewrite([1671(6),1671(22),3(27),3(24),3(23),3(20),3(19),3(17),522(15),522(11)])]. given #114 (A,wt=19): 890 e * (x * (e * (x * (e * (y * e))))) = e * (y * x). [back_rewrite(688),rewrite([865(7)])]. given #115 (F,wt=43): 3692 c1 * (c3 * (e * (c2 * (c4 * (c2 * (c4 * (c2 * (c1 * e)))))))) != c4 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (c3 * (c4 * c1)))))))))). [para(890(a,2),1781(a,2,2,2,2,2,2)),rewrite([1671(54),3(62),3(60),3(58),1671(55),1671(68),3(76),3(74),3(72),1671(69),3669(81),522(76),522(70),3(64),3(62),3(60),3(62),3(60),3(58),1671(56),3(64),3(62),3(60),1671(57),1671(70),3(78),3(76),3(74),1671(71),1713(81),3(68),3(69),3(66),3(63),3(66),3(64),3(62),3(64),3(62),3(60),1713(59),3(46),3(47),3(44)]),flip(a)]. given #116 (F,wt=43): 3701 c4 * (c3 * (e * (c2 * (c1 * (c2 * (c1 * (c2 * (c4 * e)))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))). [para(890(a,2),2138(a,1,2,2,2,2,2)),rewrite([1671(31),3(39),3(37),3(35),1671(32),1671(45),3(53),3(51),3(49),1671(46),3669(58),522(53),522(47),3(41),3(39),3(37),3(39),3(37),3(35),1671(33),3(41),3(39),3(37),1671(34),1671(47),3(55),3(53),3(51),1671(48),1713(58),3(45),3(46),3(43),3(40),3(43),3(41),3(39),3(41),3(39),3(37),1713(36),3(23),3(24),3(21)])]. given #117 (F,wt=43): 3722 c1 * (c3 * (e * (c2 * (c4 * (c2 * (c4 * (c2 * (c1 * e)))))))) != c4 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * c1)))))))))). [para(890(a,2),2147(a,2,2,2,2,2,2)),rewrite([1671(54),3(62),3(60),3(58),1671(55),1671(68),3(76),3(74),3(72),1671(69),3669(81),522(76),522(70),3(64),3(62),3(60),3(62),3(60),3(58),1671(56),3(64),3(62),3(60),1671(57),1671(70),3(78),3(76),3(74),1671(71),1713(81),3(68),3(69),3(66),3(63),3(66),3(64),3(62),3(64),3(62),3(60),1713(59),3(46),3(47),3(44)]),flip(a)]. given #118 (F,wt=43): 3725 c4 * (c3 * (e * (c2 * (c1 * (c2 * (c1 * (c2 * (c4 * e)))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [para(890(a,2),2156(a,1,2,2,2,2,2)),rewrite([1671(31),3(39),3(37),3(35),1671(32),1671(45),3(53),3(51),3(49),1671(46),3669(58),522(53),522(47),3(41),3(39),3(37),3(39),3(37),3(35),1671(33),3(41),3(39),3(37),1671(34),1671(47),3(55),3(53),3(51),1671(48),1713(58),3(45),3(46),3(43),3(40),3(43),3(41),3(39),3(41),3(39),3(37),1713(36),3(23),3(24),3(21)])]. given #119 (T,wt=15): 2535 x * (e * (x * (e * (y * e)))) = y * x. [back_rewrite(2247),rewrite([2335(19),975(8),3(6),11(5)])]. given #120 (T,wt=15): 2539 x * (y * (e * (y * (e * (x * e))))) = y. [para(32(a,1),264(a,1,2,2,2)),rewrite([1671(3),975(10),3(8),11(7),3(12),32(11)])]. given #121 (T,wt=15): 2695 e * x = x * (y * (x * (e * (y * e)))). [para(378(a,1),190(a,1,2)),flip(a)]. given #122 (T,wt=15): 2699 x * (e * x) = y * (x * (e * (y * e))). [para(378(a,1),247(a,1)),flip(a)]. given #123 (A,wt=21): 1191 e * (x * (y * y)) = y * (e * (y * (e * (y * (x * e))))). [back_rewrite(746),rewrite([1151(13),486(6),3(7)]),flip(a)]. given #124 (F,wt=39): 4078 c1 * (c3 * (e * (c2 * (c4 * (c2 * (c4 * (c2 * (c1 * e)))))))) != c4 * (c3 * (e * (c2 * (c1 * (c2 * (c1 * (c2 * (c4 * e)))))))). [para(2535(a,2),3725(a,2,2,2,2,2,2,2)),rewrite([1671(50),3(58),3(56),3(54),1671(51),1671(64),3(72),3(70),3(68),1671(65),3669(77),522(72),522(66),3(60),3(58),3(56),3(58),3(56),3(54),1671(52),3(60),3(58),3(56),1671(53),1671(66),3(74),3(72),3(70),1671(67),1713(77),3(64),3(65),3(62),3(59),3(62),3(60),3(58),3(60),3(58),3(56),1713(55),3(42),3(43),3(40)]),flip(a)]. given #125 (F,wt=39): 4284 c4 * (c3 * (e * (c2 * (c1 * (c2 * (c1 * (c2 * (c4 * e)))))))) != c1 * (c3 * (e * (c2 * (c4 * (c2 * (c1 * (c2 * (c4 * e)))))))). [para(520(a,1),4078(a,1,2,2,2,2,2,2)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 3.52 (+ 0.01) seconds. % Length of proof is 86. % Level of proof is 19. % Maximum clause weight is 63.000. % Given clauses 125. 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]. 8 (x / y) * y = x. [assumption]. 9 (x * y) / y = x. [assumption]. 10 ((c4 * c2) * c3) * c1 != ((c1 * c2) * c3) * c4. [deny(1)]. 11 e * e = e. [para(2(a,1),2(a,1,1)),rewrite([3(5)]),flip(a)]. 12 ((x * y) * x) * (e * y) = x * y. [para(4(a,1),2(a,1))]. 13 ((x * e) * y) * (x * z) = x * (y * z). [para(2(a,1),4(a,1,1)),flip(a)]. 14 (x * (y * e)) * (z * y) = (x * z) * y. [para(2(a,1),4(a,1,2)),flip(a)]. 15 (x * y) * ((x * z) * (y * u)) = z * u. [para(4(a,1),3(a,1,2))]. 16 (x * y) * ((x * z) * u) = z * (y * u). [para(3(a,1),4(a,1,1)),flip(a)]. 17 (x * y) * (z * (y * u)) = (x * z) * u. [para(3(a,1),4(a,1,2)),flip(a)]. 20 ((x * x) * x) * e = x. [para(5(a,1),3(a,1,2))]. 28 (x / y) * x = y. [para(8(a,1),3(a,1,2))]. 32 x / (y * x) = y. [para(3(a,1),9(a,1,1))]. 34 e / x = (x * x) * x. [para(5(a,1),9(a,1,1))]. 35 (e * x) * (e * y) = e * (x * y). [para(11(a,1),4(a,1,1)),flip(a)]. 37 x * ((x * x) * x) = (x * x) * x. [para(28(a,1),2(a,1,1)),rewrite([34(2),34(5)])]. 44 (x * y) * (e * (y * x)) = x. [para(3(a,1),12(a,1,1,1)),rewrite([3(7)])]. 58 x * ((x * e) * e) = x. [para(34(a,1),32(a,1)),rewrite([13(8)])]. 61 ((x * e) * y) * z = x * (y * (x * z)). [para(3(a,1),13(a,1,2))]. 72 ((x * x) * x) * (y * e) = (x * y) * x. [para(20(a,1),13(a,1,2)),rewrite([20(4)]),flip(a)]. 76 (x * e) * e = x * x. [para(58(a,1),3(a,1,2)),flip(a)]. 79 (x * e) * (x * x) = e. [para(76(a,1),3(a,1,2))]. 86 (x * x) * (e * x) = e. [para(79(a,1),4(a,1)),flip(a)]. 88 (x * x) * e = e * x. [para(86(a,1),3(a,1,2))]. 97 (x * y) * x = e * (y * x). [para(3(a,1),14(a,1,1)),flip(a)]. 126 (e * x) * (x * e) = x. [para(14(a,2),20(a,1)),rewrite([11(4),88(3)])]. 133 (x * x) * y = x * ((y * e) * (x * (e * y))). [para(76(a,1),14(a,2,1)),rewrite([61(8)]),flip(a)]. 135 (x * (e * x)) * (e * (x * x)) = e. [para(14(a,2),79(a,1)),rewrite([88(3)])]. 149 (e * (x * x)) * (y * e) = e * (y * x). [back_rewrite(72),rewrite([97(2),97(8)])]. 163 x * (e * (x * x)) = e * (x * x). [back_rewrite(37),rewrite([97(2),97(6)])]. 189 (e * x) * x = x * e. [para(126(a,1),3(a,1,2))]. 190 x * (e * (x * e)) = e * x. [para(3(a,1),126(a,1,1)),rewrite([97(4)])]. 195 ((e * x) * y) * x = x * (y * x). [para(126(a,1),14(a,1,1)),flip(a)]. 196 (x * (e * y)) * (y * e) = (x * (y * y)) * y. [para(126(a,1),14(a,1,2)),rewrite([76(4)]),flip(a)]. 247 e * (x * e) = x * (e * x). [para(3(a,1),189(a,1,1)),rewrite([97(7)]),flip(a)]. 254 (e * x) * ((x * y) * e) = (x * y) * y. [para(189(a,1),15(a,1,2))]. 302 (x * y) * e = e * (y * (x * x)). [para(79(a,1),16(a,1,2))]. 335 (x * y) * (e * x) = x * (y * e). [para(88(a,1),16(a,1,2))]. 368 (e * x) * (y * e) = y * (x * y). [para(189(a,1),16(a,1,2))]. 373 ((x * y) * z) * (e * ((u * x) * ((u * z) * y))) = x * y. [para(16(a,2),44(a,1,2,2))]. 395 (x * y) * y = e * (x * (y * (x * x))). [back_rewrite(254),rewrite([302(5),35(7)]),flip(a)]. 513 ((x / y) * z) * u = x * (z * (y * u)). [para(8(a,1),17(a,1,1)),flip(a)]. 519 (e * x) * y = e * (x * (e * y)). [para(11(a,1),17(a,1,1)),flip(a)]. 520 x * (y * (z * u)) = z * (y * (x * u)). [para(28(a,1),17(a,1,1)),rewrite([513(6)])]. 522 x * (y * (z * (x * (y * u)))) = z * u. [para(28(a,1),17(a,2,1)),rewrite([513(5)])]. 562 e * ((x * (e * y)) * (e * z)) = x * (y * ((x * e) * z)). [para(126(a,1),17(a,1,1)),rewrite([519(8),519(11)]),flip(a)]. 596 ((x * y) * z) * u = x * (z * (e * ((y * x) * (e * u)))). [para(44(a,1),17(a,1,1)),rewrite([519(4)]),flip(a)]. 597 (x * (y * z)) * (z * y) = (x * e) * y. [para(44(a,1),17(a,1,2)),flip(a)]. 646 (x * y) * (z * (y * x)) = e * (z * x). [para(17(a,2),97(a,1))]. 649 x * (y * (e * ((z * x) * (e * (x * (y * u)))))) = e * ((z * x) * (e * u)). [para(97(a,1),17(a,2,1)),rewrite([596(5),519(14)])]. 674 e * (x * (e * (y * e))) = y * (x * y). [back_rewrite(368),rewrite([519(5)])]. 682 e * (x * (e * (y * e))) = x * (y * x). [back_rewrite(195),rewrite([519(3),519(6),335(7),97(5)])]. 688 e * ((x * x) * (e * (y * e))) = e * (y * x). [back_rewrite(149),rewrite([519(6)])]. 782 x * (y * (e * ((z * x) * ((u * x) * ((u * y) * z))))) = x * z. [back_rewrite(373),rewrite([596(9),3(10)])]. 863 c4 * (c3 * (e * ((c2 * c4) * (e * c1)))) != c1 * (c3 * (e * ((c2 * c1) * (e * c4)))). [back_rewrite(10),rewrite([596(7),596(20)])]. 864 (x * (y * y)) * y = x * x. [back_rewrite(196),rewrite([597(6),395(4),163(5),3(5)]),flip(a)]. 865 (x * x) * y = x * (e * (x * y)). [back_rewrite(133),rewrite([646(8)])]. 890 e * (x * (e * (x * (e * (y * e))))) = e * (y * x). [back_rewrite(688),rewrite([865(7)])]. 920 c4 * (c3 * (e * ((c2 * c4) * (e * c1)))) != c1 * ((x * e) * ((x * c3) * ((c2 * c1) * (e * c4)))). [para(16(a,2),863(a,2,2))]. 975 e * (x * (e * x)) = x * e. [para(247(a,1),3(a,1,2))]. 994 (x * e) * ((x * y) * (z * e)) = y * (z * (e * z)). [para(247(a,1),16(a,2,2))]. 1295 x * (e * (y * (z * ((z * x) * ((z * e) * u))))) = y * (z * u). [para(864(a,1),16(a,1,1)),rewrite([596(5),865(4),562(10),865(10),3(10)])]. 1638 e * (x * (y * (e * ((x * e) * (e * z))))) = y * (e * (x * (e * (x * (e * z))))). [para(135(a,1),16(a,1,1)),rewrite([596(6),395(5),11(7),3(8),519(15),865(16)])]. 1671 (x * y) * z = e * (x * (e * (x * (e * (y * (e * (x * (e * (x * (e * z)))))))))). [para(163(a,1),17(a,1,1)),rewrite([519(7),865(8),519(13),865(14)]),flip(a)]. 1713 e * (x * (y * (x * (e * (x * (e * (x * (e * (x * z))))))))) = y * (e * (x * (e * (x * (e * z))))). [back_rewrite(1638),rewrite([1671(7),3(12),3(13),3(15)])]. 1954 x * (e * (y * (z * (e * (x * u))))) = y * (z * u). [back_rewrite(1295),rewrite([1671(5),3(15),1671(17),3(22),3(19),3(18),3(15),3(14),522(13),522(9)])]. 2101 x * (e * (y * e)) = x * (y * (e * y)). [back_rewrite(994),rewrite([1671(6),1671(22),3(27),3(24),3(23),3(20),3(19),3(17),522(15),522(11)])]. 2156 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(920),rewrite([1671(10),3(18),3(25),1671(35),3(43),1671(50),3(55),1671(62),3(67),3(64),3(63),3(60),3(59),3(57),522(55),522(51)])]. 2247 x * (y * (z * (e * (z * (e * (x * (e * (z * (e * (z * (x * (y * (e * z))))))))))))) = x * z. [back_rewrite(782),rewrite([1671(5),1671(21),3(26),3(23),3(22),3(19),3(18),1954(17),1954(13),1671(9),3(14),3(21)])]. 2335 x * (y * (z * (e * (z * (e * (x * (e * (z * (e * (z * (x * (y * u)))))))))))) = z * (e * (z * (e * (x * (e * (z * (e * (z * u)))))))). [back_rewrite(649),rewrite([1671(7),3(12),3(19),1671(22),3(27),3(34)])]. 2535 x * (e * (x * (e * (y * e)))) = y * x. [back_rewrite(2247),rewrite([2335(19),975(8),3(6),11(5)])]. 2795 x * (y * (z * (u * (w * v5)))) = w * (y * (x * (u * (z * v5)))). [para(520(a,1),520(a,1,2,2))]. 2998 e * (x * (e * (x * (e * (y * (e * (y * (e * (y * (e * (y * (e * (x * (e * (x * (e * (x * (e * (x * (e * (y * (e * (y * (e * (y * (e * (y * x))))))))))))))))))))))))))) = y * (x * y). [para(674(a,1),190(a,2)),rewrite([1671(13),11(18),190(19),3(17),1671(14),3(23),3(21),1671(19),3(24),3(25),3(27),3(25),3(23),3(25),1671(22),1671(32),3(40),3(38),3(36),1671(33),3(43),3(45),3(43),3(41)])]. 3239 x * (y * x) = y * (x * y). [para(682(a,1),190(a,2)),rewrite([1671(13),11(18),190(19),3(17),1671(14),3(23),3(21),1671(19),3(24),3(25),3(27),3(25),3(23),3(25),1671(22),1671(32),3(40),3(38),3(36),1671(33),3(43),3(45),3(43),3(41),2998(42)])]. 3296 x * (y * (z * (y * (x * y)))) = z * x. [para(3239(a,1),522(a,1,2,2,2))]. 3669 e * (x * (e * (x * (e * (x * (e * (x * (e * (y * e))))))))) = x * (e * (x * (e * (x * (y * e))))). [para(2101(a,1),682(a,2,2)),rewrite([1671(10),3(18),3(16),3(14),1671(11),3(21),3(23),3(21),3(19),1671(25),3(34),3(32),1671(30),3(35),3296(33),3(31),3(33),3(31),3(29)])]. 3725 c4 * (c3 * (e * (c2 * (c1 * (c2 * (c1 * (c2 * (c4 * e)))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [para(890(a,2),2156(a,1,2,2,2,2,2)),rewrite([1671(31),3(39),3(37),3(35),1671(32),1671(45),3(53),3(51),3(49),1671(46),3669(58),522(53),522(47),3(41),3(39),3(37),3(39),3(37),3(35),1671(33),3(41),3(39),3(37),1671(34),1671(47),3(55),3(53),3(51),1671(48),1713(58),3(45),3(46),3(43),3(40),3(43),3(41),3(39),3(41),3(39),3(37),1713(36),3(23),3(24),3(21)])]. 4078 c1 * (c3 * (e * (c2 * (c4 * (c2 * (c4 * (c2 * (c1 * e)))))))) != c4 * (c3 * (e * (c2 * (c1 * (c2 * (c1 * (c2 * (c4 * e)))))))). [para(2535(a,2),3725(a,2,2,2,2,2,2,2)),rewrite([1671(50),3(58),3(56),3(54),1671(51),1671(64),3(72),3(70),3(68),1671(65),3669(77),522(72),522(66),3(60),3(58),3(56),3(58),3(56),3(54),1671(52),3(60),3(58),3(56),1671(53),1671(66),3(74),3(72),3(70),1671(67),1713(77),3(64),3(65),3(62),3(59),3(62),3(60),3(58),3(60),3(58),3(56),1713(55),3(42),3(43),3(40)]),flip(a)]. 4284 c4 * (c3 * (e * (c2 * (c1 * (c2 * (c1 * (c2 * (c4 * e)))))))) != c1 * (c3 * (e * (c2 * (c4 * (c2 * (c1 * (c2 * (c4 * e)))))))). [para(520(a,1),4078(a,1,2,2,2,2,2,2)),flip(a)]. 4313 c4 * (c3 * (c1 * (c2 * (e * (c2 * (c1 * (c2 * (c4 * e)))))))) != c1 * (c3 * (e * (c2 * (c4 * (c2 * (c1 * (c2 * (c4 * e)))))))). [para(520(a,1),4284(a,1,2,2))]. 4314 $F. [resolve(4313,a,2795,a(flip))]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=125. Generated=10013. Kept=4312. proofs=1. Usable=46. Sos=2144. Demods=251. Limbo=5, Disabled=2125. Hints=0. Kept_by_rule=0, Deleted_by_rule=649. Forward_subsumed=5052. Back_subsumed=169. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=899 (5 lex), Back_demodulated=1947. Back_unit_deleted=0. Demod_attempts=634042. Demod_rewrites=96523. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=8.62. User_CPU=3.52, System_CPU=0.01, Wall_clock=4. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 4310 exit (max_proofs) Tue Nov 3 09:38:21 2009