============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 10670 was started by mccune on cleo.thornwood, Sat Aug 12 20:57:50 2006 The command was "/home/mccune/bin/prover9 -f identity2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file identity2.in 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. [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: 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 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.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=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 (T,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 (A,wt=13): 12 ((x * y) * x) * (e * y) = x * y. [para(4(a,1),2(a,1))]. given #12 (F,wt=7): 28 (x / y) * x = y. [para(8(a,1),3(a,1,2))]. % Operation / is commutative; C redundancy checks enabled. given #13 (F,wt=7): 31 x / x = x * e. [para(2(a,1),9(a,1,1))]. given #14 (T,wt=7): 32 x / (y * x) = y. [para(3(a,1),9(a,1,1))]. given #15 (T,wt=7): 49 x / y = y / x. [para(28(a,1),9(a,1,1))]. given #16 (A,wt=15): 13 ((x * e) * y) * (x * z) = x * (y * z). [para(2(a,1),4(a,1,1)),flip(a)]. given #17 (F,wt=9): 20 ((x * x) * x) * e = x. [para(5(a,1),3(a,1,2))]. given #18 (F,wt=9): 34 e / x = (x * x) * x. [para(5(a,1),9(a,1,1))]. given #19 (T,wt=9): 52 x / e = (x * x) * x. [para(5(a,1),32(a,1,2))]. given #20 (T,wt=9): 76 x * ((x * e) * e) = x. [para(34(a,1),32(a,1)),rewrite(56(8),3(5))]. given #21 (A,wt=15): 14 (x * (y * e)) * (z * y) = (x * z) * y. [para(2(a,1),4(a,1,2)),flip(a)]. given #22 (F,wt=19): 101 ((c4 * (c3 * e)) * (c2 * c3)) * c1 != ((c1 * c2) * c3) * c4. [para(14(a,2),10(a,1,1))]. given #23 (F,wt=19): 102 ((c4 * c2) * (c1 * e)) * (c3 * c1) != ((c1 * c2) * c3) * c4. [para(14(a,2),10(a,1))]. given #24 (T,wt=9): 77 (x * e) * e = x * x. [para(76(a,1),3(a,1,2)),flip(a)]. given #25 (T,wt=9): 93 (e * (x * x)) * x = e. [para(14(a,2),5(a,1,1)),rewrite(3(3))]. given #26 (A,wt=15): 15 (x * y) * ((x * z) * (y * u)) = z * u. [para(4(a,1),3(a,1,2))]. given #27 (F,wt=19): 103 ((c4 * c2) * c3) * c1 != ((c1 * (c3 * e)) * (c2 * c3)) * c4. [para(14(a,2),10(a,2,1))]. given #28 (F,wt=19): 104 ((c4 * c2) * c3) * c1 != ((c1 * c2) * (c4 * e)) * (c3 * c4). [para(14(a,2),10(a,2))]. given #29 (T,wt=9): 114 e * ((x * x) * e) = x. [para(14(a,2),20(a,1,1)),rewrite(3(3),83(5))]. given #30 (T,wt=9): 135 x / e = e * (x * x). [back_rewrite(52),rewrite(83(4))]. given #31 (A,wt=15): 16 (x * y) * ((x * z) * u) = z * (y * u). [para(3(a,1),4(a,1,1)),flip(a)]. given #32 (F,wt=19): 150 ((c4 * c1) * (c2 * e)) * (c3 * c1) != ((c1 * c2) * c3) * c4. [para(4(a,1),102(a,1,1))]. given #33 (F,wt=19): 188 ((c4 * c2) * c3) * c1 != ((c1 * c4) * (c2 * e)) * (c3 * c4). [para(4(a,1),104(a,2,1))]. given #34 (T,wt=9): 143 e / x = e * (x * x). [back_rewrite(34),rewrite(83(4))]. given #35 (T,wt=9): 190 (x * x) * e = e * x. [para(114(a,1),3(a,1,2)),flip(a)]. given #36 (A,wt=15): 17 (x * y) * (z * (y * u)) = (x * z) * u. [para(3(a,1),4(a,1,2)),flip(a)]. given #37 (F,wt=19): 265 ((c4 * c1) * c3) * ((c2 * e) * c1) != ((c1 * c2) * c3) * c4. [para(4(a,1),150(a,1))]. given #38 (F,wt=19): 271 ((c4 * c2) * c3) * c1 != ((c1 * c4) * c3) * ((c2 * e) * c4). [para(4(a,1),188(a,2))]. given #39 (T,wt=11): 38 (x * y) * (e * (y * x)) = x. [para(3(a,1),12(a,1,1,1)),rewrite(3(7))]. given #40 (T,wt=11): 44 (x * (x / y)) * (e * y) = x. [para(8(a,1),12(a,1,1,1)),rewrite(8(7))]. given #41 (A,wt=23): 19 (x * (y * z)) * (u * (v * w)) = (x * u) * ((y * v) * (z * w)). [para(4(a,1),4(a,1,2)),flip(a)]. given #42 (F,wt=27): 623 c4 * (c3 * (e * ((c2 * c4) * (e * c1)))) != c1 * (c3 * (e * ((c2 * c1) * (e * c4)))). [back_rewrite(10),rewrite(453(7),453(20))]. given #43 (F,wt=27): 789 c1 * (c3 * (e * ((c2 * c1) * (e * c4)))) != c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))). [para(4(a,1),623(a,1,2,2,2)),flip(a)]. given #44 (T,wt=11): 50 (x * (y / x)) * (e * y) = x. [para(28(a,1),12(a,1,1,1)),rewrite(28(7))]. given #45 (T,wt=11): 83 (x * y) * x = e * (y * x). [para(3(a,1),14(a,1,1)),flip(a)]. given #46 (A,wt=15): 30 (x * (y / z)) * (u * z) = (x * u) * y. [para(8(a,1),4(a,1,2)),flip(a)]. given #47 (F,wt=27): 790 c4 * (c3 * (e * ((c2 * c4) * (e * c1)))) != c1 * (c3 * (e * ((c2 * e) * (c1 * c4)))). [para(4(a,1),623(a,2,2,2,2))]. given #48 (F,wt=27): 803 c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))) != c1 * (c3 * (e * ((c2 * e) * (c1 * c4)))). [para(4(a,1),789(a,1,2,2,2)),flip(a)]. given #49 (T,wt=11): 283 (x * e) * (x * e) = e * x. [para(190(a,1),14(a,2)),rewrite(11(3))]. given #50 (T,wt=11): 434 x / (e * (y * x)) = x * y. [para(38(a,1),32(a,1,2)),rewrite(49(4))]. given #51 (A,wt=15): 48 (x * (y / z)) * (u * y) = (x * u) * z. [para(28(a,1),4(a,1,2)),flip(a)]. given #52 (F,wt=29): 566 (x * c3) * ((x * ((c1 * c2) * (c4 * e))) * c4) != c4 * (c3 * (e * ((c2 * c4) * (e * c1)))). [back_rewrite(253),rewrite(453(7)),flip(a)]. given #53 (F,wt=29): 575 (x * c3) * ((x * ((c4 * c2) * (c1 * e))) * c1) != c1 * (c3 * (e * ((c2 * c1) * (e * c4)))). [back_rewrite(229),rewrite(453(20))]. given #54 (T,wt=9): 1111 x / (x * e) = e * x. [para(283(a,1),434(a,1,2,2)),rewrite(3(6),49(3),283(8))]. given #55 (T,wt=11): 816 (e * x) / y = y * (x / y). [para(50(a,1),32(a,1,2))]. given #56 (A,wt=23): 57 (x * (y * (x * z))) * ((x * u) * v) = (x * (y * u)) * (z * v). [para(13(a,1),4(a,1,1)),rewrite(56(8)),flip(a)]. given #57 (F,wt=29): 1239 (x * c3) * ((x * ((c1 * c2) * (c4 * e))) * c4) != c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))). [para(4(a,1),566(a,2,2,2,2))]. given #58 (F,wt=29): 1279 (x * c3) * ((x * ((c4 * c2) * (c1 * e))) * c1) != c1 * (c3 * (e * ((c2 * e) * (c1 * c4)))). [para(4(a,1),575(a,2,2,2,2))]. given #59 (T,wt=11): 894 x * (e * (x * e)) = e * x. [back_rewrite(190),rewrite(875(3))]. given #60 (T,wt=11): 1102 e * (x * e) = x * (e * x). [back_rewrite(595),rewrite(1087(7)),flip(a)]. given #61 (A,wt=23): 58 (x * ((y * e) * z)) * (u * (y * v)) = (x * u) * (y * (z * v)). [para(13(a,1),4(a,1,2)),flip(a)]. given #62 (F,wt=31): 479 c1 * (c3 * (e * ((c4 * c1) * (e * ((c2 * e) * c4))))) != c4 * (c3 * (e * ((c2 * c4) * (e * c1)))). [back_rewrite(420),rewrite(453(7),455(27),453(24)),flip(a)]. given #63 (F,wt=31): 492 c1 * (c3 * (e * ((c2 * c1) * (e * c4)))) != c4 * (c3 * (e * ((c1 * c4) * (e * ((c2 * e) * c1))))). [back_rewrite(407),rewrite(455(14),453(11),453(24)),flip(a)]. given #64 (T,wt=11): 1105 x / (e * y) = x * (x / y). [para(28(a,1),434(a,1,2,2))]. given #65 (T,wt=11): 1318 e * (x * (e * x)) = x * e. [para(1111(a,1),28(a,1,1)),rewrite(304(3))]. given #66 (A,wt=19): 60 x * ((y * z) * (u * v)) = x * ((y * u) * (z * v)). [para(4(a,1),13(a,2,2)),rewrite(56(7),3(4))]. given #67 (F,wt=31): 545 c4 * (c3 * (e * ((c2 * c4) * (e * c1)))) != c1 * (x * (e * ((c2 * c1) * (e * (c3 * (x * c4)))))). [back_rewrite(303),rewrite(453(7),453(22))]. given #68 (F,wt=27): 2282 c4 * (c3 * (e * ((c2 * c4) * (e * c1)))) != c1 * ((c2 * c1) * (e * (c3 * (e * c4)))). [para(3(a,1),545(a,2,2))]. given #69 (T,wt=13): 136 x * (e * (x * x)) = e * (x * x). [back_rewrite(46),rewrite(83(2),83(6))]. given #70 (T,wt=11): 3523 x * (y * x) = y * (x * y). [back_rewrite(2718),rewrite(3176(19),3(7),3(6))]. given #71 (A,wt=15): 305 x * (y * (z * u)) = z * (y * (x * u)). [para(28(a,1),17(a,1,1)),rewrite(298(6))]. given #72 (F,wt=47): 2428 c4 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c2 * (e * (c2 * c1)))))))))) != c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * (c3 * (c1 * c4)))))))))). [back_rewrite(2283),rewrite(2347(10),3(18),3(25),2347(35),3(43),3(50))]. given #73 (F,wt=47): 3053 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(1059),rewrite(2347(10),3(23),3(25),2347(35),3(48),2347(50),3(55),2347(62),3(67),3(64),3(63),3(60),3(59),3(57),307(55),307(51))]. given #74 (T,wt=11): 3540 x * (y * (x * y)) = y * x. [para(3523(a,1),3(a,1,2))]. given #75 (T,wt=11): 3542 (x * y) / (x * (y * x)) = y. [para(3523(a,1),32(a,1,2))]. given #76 (A,wt=15): 307 x * (y * (z * (x * (y * u)))) = z * u. [para(28(a,1),17(a,2,1)),rewrite(298(5))]. given #77 (F,wt=47): 3063 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(1048),rewrite(2347(10),3(18),3(25),2347(35),3(48),2347(50),3(55),2347(62),3(67),3(64),3(63),3(60),3(59),3(57),307(55),307(51))]. given #78 (F,wt=47): 3217 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(811),rewrite(2347(12),3(25),2347(27),3(32),2347(39),3(44),3(41),3(40),3(37),3(36),3(34),307(32),307(28),2347(33),3(41),3(48))]. given #79 (T,wt=13): 432 x * (e * (y * (x / y))) = x / y. [para(8(a,1),38(a,1,1))]. given #80 (T,wt=13): 433 x * (e * (y * (y / x))) = y / x. [para(28(a,1),38(a,1,1))]. given #81 (A,wt=15): 392 x * (y * (z * (x * u))) = z * (y * u). [back_rewrite(209),rewrite(298(3))]. given #82 (F,wt=47): 3226 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(799),rewrite(2347(10),3(18),3(25),2347(35),3(43),2347(50),3(55),2347(62),3(67),3(64),3(63),3(60),3(59),3(57),307(55),307(51))]. given #83 (F,wt=47): 3565 c4 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * (e * (c2 * c1)))))))))) != c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * (c3 * (c1 * c4)))))))))). [para(305(a,1),2428(a,1,2,2,2,2,2,2))]. given #84 (T,wt=13): 834 e * (x * (y / x)) = y * (y / x). [para(8(a,1),83(a,1,1)),flip(a)]. given #85 (T,wt=13): 835 e * (x * (x / y)) = y * (x / y). [para(28(a,1),83(a,1,1)),flip(a)]. given #86 (A,wt=17): 395 e * (x * (e * (y * y))) = y * (x * (y * y)). [back_rewrite(192),rewrite(304(4))]. given #87 (F,wt=47): 3566 c4 * (c3 * (c2 * (e * (c4 * (e * (c2 * (e * (c2 * (e * (c2 * c1)))))))))) != c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * (c3 * (c1 * c4)))))))))). [para(305(a,1),2428(a,1,2,2,2,2))]. given #88 (F,wt=47): 3567 c4 * (e * (c2 * (c3 * (c2 * (e * (c4 * (e * (c2 * (e * (c2 * c1)))))))))) != c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * (c3 * (c1 * c4)))))))))). [para(305(a,1),2428(a,1,2))]. given #89 (T,wt=13): 1079 e * (x * (y * e)) = y * (x * e). [para(283(a,1),16(a,1,2)),rewrite(288(4)),flip(a)]. given #90 (T,wt=13): 1808 (x * e) / (x * x) = x * (e * x). [para(1102(a,1),1111(a,2)),rewrite(889(6),3(8),136(7),3(7))]. given #91 (A,wt=15): 447 e * (x * y) = z * (x * (e * (z * y))). [para(38(a,1),16(a,1,2)),rewrite(83(2))]. given #92 (F,wt=47): 3568 c2 * (c3 * (c4 * (e * (c2 * (e * (c4 * (e * (c2 * (e * (c2 * c1)))))))))) != c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * (c3 * (c1 * c4)))))))))). [para(305(a,1),2428(a,1))]. given #93 (F,wt=47): 3569 c4 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c2 * (e * (c2 * c1)))))))))) != c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c1 * (c3 * (c2 * c4)))))))))). [para(305(a,1),2428(a,2,2,2,2,2,2,2,2,2))]. given #94 (T,wt=13): 3581 (x / y) * (y * x) = y * (x / y). [para(8(a,1),3540(a,1,2,2))]. given #95 (T,wt=13): 3582 (x / y) * (x * y) = x * (x / y). [para(28(a,1),3540(a,1,2,2))]. given #96 (A,wt=27): 465 x * (y * (e * (z * (x * (e * (x * u)))))) = x * (z * (x * (y * (x * u)))). [back_rewrite(69),rewrite(453(8),453(10),3(11),453(8),304(10),3(10),3(7),3(7),3(4))]. given #97 (F,wt=47): 3570 c4 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c2 * (e * (c2 * c1)))))))))) != c2 * (e * (c2 * (e * (c1 * (e * (c2 * (c3 * (c2 * (e * (c1 * c4)))))))))). [para(305(a,1),2428(a,2,2,2,2,2,2,2,2))]. given #98 (F,wt=47): 3571 c4 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c2 * (e * (c2 * c1)))))))))) != c2 * (e * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * (c3 * (c1 * c4)))))))))). [para(305(a,1),2428(a,2,2,2,2,2))]. given #99 (T,wt=13): 3599 (x * y) / (x * (y / x)) = y / x. [para(8(a,1),3542(a,1,2,2)),rewrite(49(4))]. Demod_limit: (y * (e * (y * (z * (e * (z * (v100 * (e * (v100 * (y * (e * (y * (e * (u * (e * (y * (e * (y * (v100 * (e * (v100 * (z * (e * (z * (y * (e * (y * (e * (y * (e * (y * (z * (e * (z * (v100 * (e * (v100 * (y * (e * (y * (e * (u * (e * (y * (e * (y * (v100 * (e * (v100 * (z * (e * (z * (y * (e * (y * (e * (v100 * (e * (y * (e * (y * (z * (e * (z * (v100 * (e * (v100 * (y * (e * (y * (e * (u * (e * (y * (e * (y * (v100 * (e * (v100 * (z * (e * (z * (y * (e * (y * v100))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) * (e * (e * (y * (e * (y * (e * (e * (e * (e * (e * (e * (e * (y * (e * (y * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (v100 * (e * (v100 * (e * (e * (e * (e * (e * (e * (e * (v100 * (e * (v100 * (e * (e * (y * (e * (y * (e * (e * (e * (e * (e * (e * (e * (y * (e * (y * (e * (e * (e * (e * (e * (e * (e * (u * (e * (u * (e * (e * (e * (e * (e * (e * (e * (y * (e * (y * (e * (e * (e * (e * (e * (e * (e * (y * (e * (y * (e * (e * (v100 * (e * (v100 * (e * (e * (e * (e * (e * (e * (e * (v100 * (e * (v100 * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (y * (e * (y * (e * (e * (e * (e * (e * (e * (e * (y * (e * (y * (e * (e * (e * (e * (e * (e * (e * (y * (e * (y * (e * (e * (e * (e * (e * (e * (e * (y * (e * (y * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (v100 * (e * (v100 * (e * (e * (e * (e * (e * (e * (e * (v100 * (e * (v100 * (e * (e * (y * (e * (y * (e * (e * (e * (e * (e * (e * (e * (y * (e * (y * (e * (e * (e * (e * (e * (e * (e * (u * (e * (u * (e * (e * (e * (e * (e * (e * (e * (y * (e * (y * (e * (e * (e * (e * (e * (e * (e * (y * (e * (y * (e * (e * (v100 * (e * (v100 * (e * (e * (e * (e * (e * (e * (e * (v100 * (e * (v100 * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * (e * (y * (e * (y * (e * (e * (e * (e * (e * (e * (e * (y * (e * (y * (e * (e * (e * (e * (e * (e * (e * (v100 * (e * (v100 * (e * (e * (e * (e * (e * (e * (e * (y * (e * (y * (e * (e * (e * (e * (e * (e * (e * (y * (e * (y * (e * (e * (z * (e * (z * (e * (e * (e * (e * (e * (e * (e * (z * (e * (z * (e * ((v100 * (e * (v100 * (y * (e * (y * (e * (u * (e * (y * (e * (y * (v100 * (e * (v100 * (z * (e * (z * (y * (e * (y * v100))))))))))))))))))))) * (e * (z * (e * (z * (e * (z * (e * (z * (y * (e * (y * (e * (y * (e * (y * (e * (v100 * (e * (v100 * (e * (y * (e * (y * (e * (y * (e * (y * (z * (e * (z * (e * (z * (e * (z * (v100 * (e * (v100 * (e * (v100 * (e * (v100 * (y * (e * (y * (e * (y * (e * (y * (e * (u * (e * (u * (e * (y * (e * (y * (e * (y * (e * (y * (v100 * (e * (v100 * (e * (v100 * (e * (v100 * (z * (e * (z * (e * (z * (e * (z * (y * (z * (e * (z * (e * (z * (e * (z * (v100 * (e * (v100 * (e * (v100 * (e * (v100 * (y * (e * (y * (e * (y * (e * (y * (e * (u * (e * (u * (e * (y * (e * (y * (e * (y * (e * (y * (v100 * (e * (v100 * (e * (v100 * (e * (v100 * (z * (e * (z * (e * (z * (e * (z * (y * (e * (y * (e * (y * (e * (y * (z * (e * (z * (e * (u * (e * (z * (e * (z * (y * (e * (y * (e * (y * (e * (y * (z * (e * (z * (e * (z * (e * (z * (v100 * (e * (v100 * (e * (v100 * (e * (v100 * (y * (e * (y * (e * (y * (e * (y * (e * (u * (e * (u * (e * (y * (e * (y * (e * (y * (e * (y * (v100 * (e * (v100 * (e * (v100 * (e * (v100 * (z * (e * (z * (e * (z * (e * (z * (y * (z * (e * (z * (e * (z * (e * (z * (v100 * (e * (v100 * (e * (v100 * (e * (v100 * (y * (e * (y * (e * (y * (e * (y * (e * (u * (e * (u * (e * (y * (e * (y * (e * (y * (e * (y * (v100 * (e * (v100 * (e * (v100 * (e * (v100 * (z * (e * (z * (e * (z * (e * (z * (y * (e * (y * (e * (y * (e * (y * (e * (v100 * (e * (v100 * (e * (y * (e * (y * (e * (y * (e * (y * (z * (e * (z * (e * (z * (e * (z * (v100 * (e * (v100 * (e * (v100 * (e * (v100 * (y * (e * (y * (e * (y * (e * (y * (e * (u * (e * (u * (e * (y * (e * (y * (e * (y * (e * (y * (v100 * (e * (v100 * (e * (v100 * (e * (v100 * (z * (e * (z * (e * (z * (e * (z * (v100 * (e * (y * (z * (e * (z * (e * (z * (e * (z * (v100 * (e * (v100 * (e * (v100 * (e * (v100 * (y * (e * (y * (e * (y * (e * (y * (e * (u * (e * (u * (e * (y * (e * (y * (e * (y * (e * (y * (v100 * (e * (v100 * (e * (v100 * (e * (v100 * (z * (e * (z * (e * (z * (e * (z * (y * (e * (y * (e * (y * (e * (y * (e * (v100 * (e * (v100 * (e * (y * (e * (y * (e * (y * (e * (y * (z * (e * (z * (e * (z * (e * (z * (v100 * (e * (v100 * (e * (v100 * (e * (v100 * (y * (e * (y * (e * (y * (e * (y * (e * (u * (e * (u * (e * (y * (e * (y * (e * (y * (e * (y * (v100 * (e * (v100 * (e * (v100 * (e * (v100 * (z * (e * (z * (e * (z * (e * (z * (y * (z * (e * (z * (e * (z * (e * (z * (v100 * (e * (v100 * (e * (v100 * (e * (v100 * (y * (e * (y * (e * (y * (e * (y * (e * (u * (e * (u * (e * (y * (e * (y * (e * (y * (e * (y * (v100 * (e * (v100 * (e * (v100 * (e * (v100 * (z * (e * (z * (e * (z * (e * (z * (y * (e * (y * (e * (y * (e * (y * (z * u)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) = (y * (z * (v100 * (y * u)))) / v100. [para(307(a,1),3599(a,1,1)),rewrite(49(6),4369(7),2347(17),3(22),2347(23),3(28),2347(29),3(34),2347(35),3(40),3(47),3(48),3(49),2347(51),2347(61),3(66),2347(67),3(72),2347(73),3(78),3(85),3(86),3(87),3(88),2347(85),2347(95),3(100),2347(101),3(106),2347(107),3(112),3(119),3(120),3(121),1105(122),4369(122),2347(360),3(365),2347(366),3(374),3(372),3(370),2347(367),2347(377),3(382),2347(383),3(391),3(389),3(387),2347(384),2347(394),3(399),2347(400),3(408),3(406),3(404),2347(401),2347(411),3(416),2347(417),3(425),3(423),3(421),2347(418),2347(428),3(436),3(434),3(432),2347(429),2347(439),3(447),3(445),3(443),2347(440),2347(450),3(458),3(456),3(454),2347(451),2347(461),3(466),2347(467),3(475),3(473),3(471),2347(468),2347(478),3(483),2347(484),3(492),3(490),3(488),2347(485),2347(495),3(500),2347(501),3(509),3(507),3(505),2347(502),2347(512),3(520),3(518),3(516),2347(513),3176(522),3(507),2347(508),3(517),3(515),2347(513),3(518),3(515),3(514),2347(513),3(518),2347(519),3(527),3(525),3(523),2347(520),2347(530),3(535),2347(536),3(544),3(542),3(540),2347(537),2347(547),3(552),2347(553),3(561),3(559),3(557),2347(554),2347(564),3(572),3(570),3(568),2347(565),2347(575),3(583),3(581),3(579),2347(576),2347(586),3(594),3(592),3(590),2347(587),2347(597),3(602),2347(603),3(611),3(609),3(607),2347(604),2347(614),3(619),2347(620),3(628),3(626),3(624),2347(621),2347(631),3(636),2347(637),3(645),3(643),3(641),2347(638),2347(648),3(656),3(654),3(652),2347(649),2347(659),3(667),3(665),3(663),2347(660),2347(670),3(678),3(676),3(674),2347(671),2347(681),3(686),2347(687),3(695),3(693),3(691),2347(688),2347(698),3(703),2347(704),3(712),3(710),3(708),2347(705),2347(715),3(720),2347(721),3(729),3(727),3(725),2347(722),2347(732),3(740),3(738),3(736),2347(733),2347(743),3(751),3(749),3(747),2347(744),2347(754),3(762),3(760),3(758),2347(755),2347(765),3(770),2347(771),3(779),3(777),3(775),2347(772),2347(782),3(787),2347(788),3(796),3(794),3(792),2347(789),2347(799),3(804),2347(805),3(813),3(811),3(809),2347(806),3(822),3(820),3(818),2507(819),3(799),3(800),3(798),3(796),3(798),3(799),3(797),3(795),3(797),3(798),3(796),3(794),3(796),3(794),3(792),3(794),3(792),3(790),3(792),3(790),3(788),3(790),3(791),3(789),3(787),3(789),3(790),3(788),3(786),3(788),3(789),3(787),3(785),3(787),3(785),3(783),3(785),3(783),3(781),3(783),3(781),3(779),3(781),3(782),3(780),3(778),3(780),3(781),3(779),3(777),3(779),3(780),3(778),3(776),3(778),3(776),3(774),3(776),3(774),3(772),3(774),3(772),3(770),3(772),3(773),3(771),3(769),3(771),3(772),3(770),3(768),3(770),3(771),3(769),3(767),3(769),3(767),3(765),3176(766),3(751),3(753),3(751),3(749),3(746),3(745),3(744),3(745),3(743),3(741),3(743),3(744),3(742),3(740),3(742),3(743),3(741),3(739),3(741),3(739),3(737),3(739),3(737),3(735),3(737),3(735),3(733),3(735),3(736),3(734),3(732),3(734),3(735),3(733),3(731),3(733),3(734),3(732),3(730),2347(732),3(737),2347(744),3(749),2347(750),3(758),3(756),3(754),2347(751),2347(761),3(766),2347(767),3(775),3(773),3(771),2347(768),2347(778),3(783),2347(784),3(792),3(790),3(788),2347(785),2347(795),3(800),2347(801),3(809),3(807),3(805),2347(802),2347(812),3(820),3(818),3(816),2347(813),2347(823),3(831),3(829),3(827),2347(824),2347(834),3(842),3(840),3(838),2347(835),2347(845),3(850),2347(851),3(859),3(857),3(855),2347(852),2347(862),3(867),2347(868),3(876),3(874),3(872),2347(869),2347(879),3(884),2347(885),3(893),3(891),3(889),2347(886),2347(896),3(904),3(902),3(900),2347(897),3176(906),3(891),2347(892),3(901),3(899),2347(897),3(902),3(899),3(898),2347(897),3(902),2347(903),3(911),3(909),3(907),2347(904),2347(914),3(919),2347(920),3(928),3(926),3(924),2347(921),2347(931),3(936),2347(937),3(945),3(943),3(941),2347(938),2347(948),3(956),3(954),3(952),2347(949),2347(959),3(967),3(965),3(963),2347(960),2347(970),3(978),3(976),3(974),2347(971),2347(981),3(986),2347(987),3(995),3(993),3(991),2347(988),2347(998),3(1003),2347(1004),3(1012),3(1010),3(1008),2347(1005),2347(1015),3(1020),2347(1021),3(1029),3(1027),3(1025),2347(1022),2347(1032),3(1040),3(1038),3(1036),2347(1033),2347(1043),3(1051),3(1049),3(1047),2347(1044),2347(1054),3(1062),3(1060),3(1058),2347(1055),2347(1065),3(1070),2347(1071),3(1079),3(1077),3(1075),2347(1072))]. Demod_limit (steps=-1, size=1827). The most recent kept clause is 4373. From here on, a short message will be printed for each 100 times the limit is hit. given #100 (T,wt=13): 3607 x * (e * (y * (x * e))) = y * e. [para(11(a,1),307(a,1,2,2,2,2))]. given #101 (A,wt=17): 626 e * (x * (e * (y * (e * x)))) = x * (y * e). [para(44(a,1),14(a,1,1)),rewrite(135(5),136(7),304(7),83(11),453(10),11(11),190(10),3(10),304(7)),flip(a)]. given #102 (F,wt=47): 3572 c4 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c2 * (e * (c2 * c1)))))))))) != c2 * (e * (c1 * (e * (c2 * (e * (c2 * (e * (c2 * (c3 * (c1 * c4)))))))))). [para(305(a,1),2428(a,2,2,2))]. given #103 (F,wt=47): 3573 c4 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * (e * (c2 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))). [para(305(a,1),3053(a,1,2,2,2,2,2,2,2,2))]. given #104 (T,wt=15): 893 e * (x * e) = y * (e * (y * (x * y))). [back_rewrite(238),rewrite(875(3)),flip(a)]. given #105 (T,wt=15): 919 e * (x * (e * (x * (y * x)))) = y * e. [back_rewrite(171),rewrite(889(5),888(12),3(7))]. given #106 (A,wt=23): 629 x * (y * (e * (z * (e * (x * (y * u)))))) = e * (z * (e * u)). [para(44(a,1),15(a,1,2,1)),rewrite(453(6),28(3),304(12))]. given #107 (F,wt=47): 3574 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(305(a,1),3053(a,1,2))]. given #108 (F,wt=47): 3575 c2 * (c3 * (c4 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))). [para(305(a,1),3053(a,1))]. given #109 (T,wt=15): 2713 x * (e * (y * e)) = x * (y * (e * y)). [back_rewrite(1768),rewrite(2347(6),2347(22),3(27),3(24),3(23),3(20),3(19),3(17),307(15),307(11))]. given #110 (T,wt=15): 3562 x * (y * (z * y)) = z * (x * (y * x)). [para(3523(a,1),305(a,1,2)),flip(a)]. given #111 (A,wt=23): 631 e * (x * (e * (y * z))) = u * (y * (e * (x * (e * (u * z))))). [para(44(a,1),16(a,1,2,1)),rewrite(453(5),28(3),304(12)),flip(a)]. given #112 (F,wt=41): 4993 c1 * (c3 * (c4 * (e * (c4 * (e * (c1 * (c2 * c2))))))) != c4 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * c1)))))))))). [back_rewrite(2808),rewrite(4949(32),3(17),3(14))]. given #113 (F,wt=41): 4994 c4 * (c3 * (c1 * (e * (c1 * (e * (c4 * (c2 * c2))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))). [back_rewrite(2792),rewrite(4949(32),3(17),3(14))]. given #114 (T,wt=15): 3587 x * (y * (z * (y * x))) = z * (x * y). [para(3540(a,1),305(a,1,2)),flip(a)]. given #115 (T,wt=15): 3617 x * (y * (z * (y * (x * y)))) = z * x. [para(3523(a,1),307(a,1,2,2,2))]. given #116 (A,wt=29): 879 e * (x * (y * z)) = x * (y * (z * (e * (z * (e * (y * (e * (y * (e * x))))))))). [back_rewrite(730),rewrite(875(10),875(14))]. given #117 (F,wt=37): 5601 c1 * (c3 * (c4 * (e * (c4 * (e * (c1 * (c2 * c2))))))) != c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))). [para(3587(a,2),4993(a,1,2,2,2,2,2,2)),rewrite(3(15),5429(38))]. given #118 (F,wt=37): 5616 c4 * (c3 * (c1 * (e * (c1 * (e * (c4 * (c2 * c2))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(3587(a,2),4994(a,1,2,2,2,2,2,2)),rewrite(3(15),5429(38))]. given #119 (T,wt=15): 3707 x * (y * (e * (y * (e * (x * e))))) = y. [para(32(a,1),432(a,1,2,2,2)),rewrite(2347(3),3540(10),3(8),11(7),3(12),32(11))]. given #120 (T,wt=15): 3747 x * (y * (z * (x * z))) = y * (z * y). [para(392(a,2),3523(a,1))]. given #121 (A,wt=25): 914 e * (x * (e * (x * (e * (y * (e * (y * (z * x)))))))) = z * (e * y). [back_rewrite(289),rewrite(889(5),888(12),875(6))]. ============================== PROOF ================================= % Proof 1 at 9.22 (+ 0.02) seconds. % Length of proof is 91. % Level of proof is 16. % Maximum clause weight is 65. % Given clauses 121. 1 ((x * y) * z) * u = ((u * y) * z) * x. [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))]. 38 (x * y) * (e * (y * x)) = x. [para(3(a,1),12(a,1,1,1)),rewrite(3(7))]. 44 (x * (x / y)) * (e * y) = x. [para(8(a,1),12(a,1,1,1)),rewrite(8(7))]. 46 x * ((x * x) * x) = (x * x) * x. [para(28(a,1),2(a,1,1)),rewrite(34(2),34(5))]. 52 x / e = (x * x) * x. [para(5(a,1),32(a,1,2))]. 56 ((x * e) * y) * z = x * (y * (x * z)). [para(3(a,1),13(a,1,2))]. 57 (x * (y * (x * z))) * ((x * u) * v) = (x * (y * u)) * (z * v). [para(13(a,1),4(a,1,1)),rewrite(56(8)),flip(a)]. 62 ((x * x) * x) * (y * x) = (x * y) * e. [para(5(a,1),13(a,1,2)),rewrite(20(4)),flip(a)]. 64 ((x * x) * x) * (y * z) = (x * y) * (((x * x) * x) * z). [para(8(a,1),13(a,1,1,1)),rewrite(52(3),52(7)),flip(a)]. 76 x * ((x * e) * e) = x. [para(34(a,1),32(a,1)),rewrite(56(8),3(5))]. 77 (x * e) * e = x * x. [para(76(a,1),3(a,1,2)),flip(a)]. 83 (x * y) * x = e * (y * x). [para(3(a,1),14(a,1,1)),flip(a)]. 93 (e * (x * x)) * x = e. [para(14(a,2),5(a,1,1)),rewrite(3(3))]. 104 ((c4 * c2) * c3) * c1 != ((c1 * c2) * (c4 * e)) * (c3 * c4). [para(14(a,2),10(a,2))]. 114 e * ((x * x) * e) = x. [para(14(a,2),20(a,1,1)),rewrite(3(3),83(5))]. 131 (e * (x * x)) * (y * z) = (x * y) * ((e * (x * x)) * z). [back_rewrite(64),rewrite(83(2),83(8))]. 133 (e * (x * x)) * (y * x) = (x * y) * e. [back_rewrite(62),rewrite(83(2))]. 136 x * (e * (x * x)) = e * (x * x). [back_rewrite(46),rewrite(83(2),83(6))]. 160 (x * x) * y = x * ((y * e) * (x * (e * y))). [para(77(a,1),14(a,2,1)),rewrite(56(8)),flip(a)]. 183 ((x * y) * (x * y)) * y = e * (x * e). [para(93(a,1),15(a,1,2)),rewrite(83(4)),flip(a)]. 190 (x * x) * e = e * x. [para(114(a,1),3(a,1,2)),flip(a)]. 209 x * (((y / x) * z) * u) = z * (y * u). [para(28(a,1),16(a,1,1))]. 238 (x * x) * (y * x) = e * (y * e). [para(93(a,1),16(a,1,2)),rewrite(83(4)),flip(a)]. 253 ((c4 * c2) * c3) * c1 != (x * c3) * ((x * ((c1 * c2) * (c4 * e))) * c4). [para(16(a,2),104(a,2))]. 283 (x * e) * (x * e) = e * x. [para(190(a,1),14(a,2)),rewrite(11(3))]. 288 (x * y) * (e * x) = x * (y * e). [para(190(a,1),16(a,1,2))]. 289 (x * (y * y)) * ((x * z) * e) = z * (e * y). [para(190(a,1),16(a,2,2))]. 298 ((x / y) * z) * u = x * (z * (y * u)). [para(8(a,1),17(a,1,1)),flip(a)]. 304 (e * x) * y = e * (x * (e * y)). [para(11(a,1),17(a,1,1)),flip(a)]. 305 x * (y * (z * u)) = z * (y * (x * u)). [para(28(a,1),17(a,1,1)),rewrite(298(6))]. 307 x * (y * (z * (x * (y * u)))) = z * u. [para(28(a,1),17(a,2,1)),rewrite(298(5))]. 392 x * (y * (z * (x * u))) = z * (y * u). [back_rewrite(209),rewrite(298(3))]. 398 (x * y) * e = e * ((x * x) * (e * (y * x))). [back_rewrite(133),rewrite(304(5)),flip(a)]. 400 (x * y) * (e * ((x * x) * (e * z))) = e * ((x * x) * (e * (y * z))). [back_rewrite(131),rewrite(304(5),304(12)),flip(a)]. 453 ((x * y) * z) * u = x * (z * (e * ((y * x) * (e * u)))). [para(38(a,1),17(a,1,1)),rewrite(304(4)),flip(a)]. 566 (x * c3) * ((x * ((c1 * c2) * (c4 * e))) * c4) != c4 * (c3 * (e * ((c2 * c4) * (e * c1)))). [back_rewrite(253),rewrite(453(7)),flip(a)]. 595 x * ((x * y) * (e * (y * (x * e)))) = e * (x * e). [back_rewrite(183),rewrite(453(4),288(6))]. 629 x * (y * (e * (z * (e * (x * (y * u)))))) = e * (z * (e * u)). [para(44(a,1),15(a,1,2,1)),rewrite(453(6),28(3),304(12))]. 854 (x * y) * (z * (y * x)) = e * (z * x). [para(83(a,1),17(a,2))]. 875 (x * x) * y = x * (e * (x * y)). [back_rewrite(160),rewrite(854(8))]. 888 (x * y) * (e * (x * (e * (x * (e * z))))) = e * (x * (e * (x * (e * (y * z))))). [back_rewrite(400),rewrite(875(6),875(16))]. 889 (x * y) * e = e * (x * (e * (x * (e * (y * x))))). [back_rewrite(398),rewrite(875(9))]. 893 e * (x * e) = y * (e * (y * (x * y))). [back_rewrite(238),rewrite(875(3)),flip(a)]. 914 e * (x * (e * (x * (e * (y * (e * (y * (z * x)))))))) = z * (e * y). [back_rewrite(289),rewrite(889(5),888(12),875(6))]. 1079 e * (x * (y * e)) = y * (x * e). [para(283(a,1),16(a,1,2)),rewrite(288(4)),flip(a)]. 1087 (x * y) * (e * (y * (x * e))) = e * x. [para(283(a,1),17(a,2))]. 1102 e * (x * e) = x * (e * x). [back_rewrite(595),rewrite(1087(7)),flip(a)]. 1239 (x * c3) * ((x * ((c1 * c2) * (c4 * e))) * c4) != c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))). [para(4(a,1),566(a,2,2,2,2))]. 1352 e * ((x * (e * y)) * z) = e * ((x * e) * (e * (y * z))). [para(11(a,1),57(a,1,2,1)),rewrite(304(8),3(8),304(12))]. 1612 c1 * (c3 * (e * ((c4 * c1) * (e * ((c2 * e) * c4))))) != c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))). [para(15(a,1),1239(a,1,2,1)),rewrite(453(11))]. 1760 e * (x * (e * ((y * e) * (e * (y * (x * z)))))) = (y * e) * z. [para(1102(a,1),15(a,1,2,1)),rewrite(304(8),1352(8))]. 1763 (x * e) * (x * (e * (x * (e * (y * x))))) = y * (x * y). [para(1102(a,2),15(a,1,2)),rewrite(889(6),3(13))]. 2347 (x * y) * z = e * (x * (e * (x * (e * (y * (e * (x * (e * (x * (e * z)))))))))). [para(136(a,1),17(a,1,1)),rewrite(304(7),875(8),304(13),875(14)),flip(a)]. 2718 e * (x * (e * (x * (e * (x * (e * (x * (e * (x * (e * (x * (e * (y * x))))))))))))) = y * (x * y). [back_rewrite(1763),rewrite(2347(10),3(20))]. 2719 e * (x * (e * (x * (e * (x * (e * (x * (e * y)))))))) = e * (z * (x * (e * (x * (e * (x * (e * (z * y)))))))). [back_rewrite(1760),rewrite(2347(9),3(14),3(11),3(13),3(15),2347(16),3(26)),flip(a)]. 2808 c1 * (c3 * (c4 * (e * (c4 * (e * (c1 * (e * (c4 * (e * (c4 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * c4))))))))))))))))))) != c4 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * c1)))))))))). [back_rewrite(1612),rewrite(2347(12),3(25),3(27),2347(24),3(43),2347(51),3(64),3(66))]. 3176 e * (x * (e * (x * (e * (x * (e * (x * (e * (x * (e * y)))))))))) = x * (e * (x * y)). [back_rewrite(875),rewrite(2347(2))]. 3523 x * (y * x) = y * (x * y). [back_rewrite(2718),rewrite(3176(19),3(7),3(6))]. 3540 x * (y * (x * y)) = y * x. [para(3523(a,1),3(a,1,2))]. 3562 x * (y * (z * y)) = z * (x * (y * x)). [para(3523(a,1),305(a,1,2)),flip(a)]. 3587 x * (y * (z * (y * x))) = z * (x * y). [para(3540(a,1),305(a,1,2)),flip(a)]. 3607 x * (e * (y * (x * e))) = y * e. [para(11(a,1),307(a,1,2,2,2,2))]. 3619 x * (y * (z * (u * (v * (x * (u * w)))))) = z * (y * (v * w)). [para(307(a,1),305(a,1,2,2)),flip(a)]. 3798 x * (y * (z * (x * (z * y)))) = y * z. [para(392(a,2),3540(a,1))]. 4640 x * (e * (y * (e * (y * (x * y))))) = e. [para(893(a,1),3607(a,1,2,2)),rewrite(11(11))]. 4669 x * (y * (z * (e * (u * (e * (y * (x * v))))))) = z * (e * (u * (e * v))). [para(629(a,1),305(a,1,2)),flip(a)]. 4949 e * (x * (e * (y * (e * (y * (e * (y * (e * (y * (e * x)))))))))) = x * (e * (y * y)). [para(893(a,1),3562(a,1,2,2)),rewrite(2347(8),4640(14),11(8),3(9),3540(7),3(5),2347(8),3(18)),flip(a)]. 4993 c1 * (c3 * (c4 * (e * (c4 * (e * (c1 * (c2 * c2))))))) != c4 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * c1)))))))))). [back_rewrite(2808),rewrite(4949(32),3(17),3(14))]. 5429 x * (e * (x * (e * (x * (e * (x * (e * y))))))) = e * (x * (e * (x * (e * (x * y))))). [para(1079(a,1),3587(a,1,2,2)),rewrite(2347(7),3798(13),3(9),3(8),2347(13),3(23),3(25)),flip(a)]. 5601 c1 * (c3 * (c4 * (e * (c4 * (e * (c1 * (c2 * c2))))))) != c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))). [para(3587(a,2),4993(a,1,2,2,2,2,2,2)),rewrite(3(15),5429(38))]. 6020 e * (x * (y * (e * (y * (e * (y * (e * (x * z)))))))) = y * (e * (y * (e * (y * z)))). [back_rewrite(2719),rewrite(5429(13),3(11)),flip(a)]. 6698 c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))) != c1 * (c3 * (c4 * (x * (e * (x * (c1 * (c2 * (e * (c2 * (e * (c2 * (c4 * x)))))))))))). [para(914(a,2),5601(a,1,2,2,2,2)),rewrite(2347(21),2347(34),3(42),5429(47),3(38),3(40),3(42),2347(39),5429(50),4669(42),4669(36),3(31),2347(28),307(37),307(31),3(31),6020(29),3(24),3(25)),flip(a)]. 6699 $F. [resolve(6698,a,3619,a(flip))]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=121. Generated=14070. Kept=6697. proofs=1. Usable=36. Sos=2672. Demods=382. Limbo=197, Disabled=3800. Hints=0. Weight_deleted=1297. Literals_deleted=0. Forward_subsumed=6076. Back_subsumed=117. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1285 (5 lex), Back_demodulated=3674. Back_unit_deleted=0. Demod_attempts=1110253. Demod_rewrites=176297. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=9.78. User_CPU=9.22, System_CPU=0.02, Wall_clock=10. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 10670 exit (max_proofs) Sat Aug 12 20:58:00 2006