============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13015 was started by mccune on cleo.thornwood, Mon Jun 19 16:40:10 2006 The command was "/home/mccune/bin/prover9 -f identity2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file identity2.in clauses(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. clauses(goals). ((x * y) * z) * u = ((u * y) * z) * x. end_of_list. ============================== end of input ========================== ============================== PROCESS GOALS ========================= % Each goal clause was negated; the result (to be placed in sos): clauses(negated_goals). ((c4 * c2) * c3) * c1 != ((c1 * c2) * c3) * c4. end_of_list. ============================== end of process goals ================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 (x * e) * x = x. [input]. 2 x * (x * y) = y. [input]. 3 (x * y) * (z * u) = (x * z) * (y * u). [input]. 4 ((x * x) * x) * x = e. [input]. 5 x * (x \ y) = y. [input]. 6 x \ (x * y) = y. [input]. 7 (x / y) * y = x. [input]. 8 (x * y) / y = x. [input]. 9 ((c4 * c2) * c3) * c1 != ((c1 * c2) * c3) * c4. [clausify]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). Auto_denials: no changes. Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ e, c1, c2, c3, c4, *, /, \ ]). After inverse_order: Function symbol precedence: lex([ e, c1, c2, c3, c4, *, /, \ ]). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: no changes. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 10 (x * e) * x = x. [input]. 11 x * (x * y) = y. [input]. 12 (x * y) * (z * u) = (x * z) * (y * u). [input]. 13 ((x * x) * x) * x = e. [input]. 14 x * (x \ y) = y. [input]. 15 x \ (x * y) = y. [input]. 16 (x / y) * y = x. [input]. 17 (x * y) / y = x. [input]. 18 ((c4 * c2) * c3) * c1 != ((c1 * c2) * c3) * c4. [clausify]. end_of_list. clauses(demodulators). 10 (x * e) * x = x. [input]. 11 x * (x * y) = y. [input]. 13 ((x * x) * x) * x = e. [input]. 14 x * (x \ y) = y. [input]. 15 x \ (x * y) = y. [input]. 16 (x / y) * y = x. [input]. 17 (x * y) / y = x. [input]. end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 10 (x * e) * x = x. [input]. given #2 (I,wt=7): 11 x * (x * y) = y. [input]. given #3 (I,wt=15): 12 (x * y) * (z * u) = (x * z) * (y * u). [input]. given #4 (I,wt=9): 13 ((x * x) * x) * x = e. [input]. given #5 (I,wt=7): 14 x * (x \ y) = y. [input]. given #6 (I,wt=7): 16 (x / y) * y = x. [input]. given #7 (I,wt=7): 17 (x * y) / y = x. [input]. given #8 (I,wt=15): 18 ((c4 * c2) * c3) * c1 != ((c1 * c2) * c3) * c4. [clausify]. given #9 (T,wt=5): 19 e * e = e. [para(10(a,1),10(a,1,1)),demod(11(5)),flip(a)]. given #10 (T,wt=7): 34 x \ y = x * y. [para(14(a,1),11(a,1,2)),flip(a)]. given #11 (A,wt=13): 20 ((x * y) * x) * (e * y) = x * y. [para(12(a,1),10(a,1))]. given #12 (F,wt=7): 36 (x / y) * x = y. [para(16(a,1),11(a,1,2))]. % Operation / is commutative; redundancy checks enabled. given #13 (F,wt=7): 39 x / x = x * e. [para(10(a,1),17(a,1,1))]. given #14 (T,wt=7): 40 x / (y * x) = y. [para(11(a,1),17(a,1,1))]. given #15 (T,wt=7): 57 x / y = y / x. [para(36(a,1),17(a,1,1))]. given #16 (A,wt=15): 21 ((x * e) * y) * (x * z) = x * (y * z). [para(10(a,1),12(a,1,1)),flip(a)]. given #17 (F,wt=9): 28 ((x * x) * x) * e = x. [para(13(a,1),11(a,1,2))]. given #18 (F,wt=9): 42 e / x = (x * x) * x. [para(13(a,1),17(a,1,1))]. given #19 (T,wt=9): 60 x / e = (x * x) * x. [para(13(a,1),40(a,1,2))]. given #20 (T,wt=9): 84 x * ((x * e) * e) = x. [para(42(a,1),40(a,1)),demod(64(8),11(5))]. given #21 (A,wt=15): 22 (x * (y * e)) * (z * y) = (x * z) * y. [para(10(a,1),12(a,1,2)),flip(a)]. given #22 (F,wt=19): 109 ((c4 * (c3 * e)) * (c2 * c3)) * c1 != ((c1 * c2) * c3) * c4. [para(22(a,2),18(a,1,1))]. given #23 (F,wt=19): 110 ((c4 * c2) * (c1 * e)) * (c3 * c1) != ((c1 * c2) * c3) * c4. [para(22(a,2),18(a,1))]. given #24 (T,wt=9): 85 (x * e) * e = x * x. [para(84(a,1),11(a,1,2)),flip(a)]. given #25 (T,wt=9): 101 (e * (x * x)) * x = e. [para(22(a,2),13(a,1,1)),demod(11(3))]. given #26 (A,wt=15): 23 (x * y) * ((x * z) * (y * u)) = z * u. [para(12(a,1),11(a,1,2))]. given #27 (F,wt=19): 111 ((c4 * c2) * c3) * c1 != ((c1 * (c3 * e)) * (c2 * c3)) * c4. [para(22(a,2),18(a,2,1))]. given #28 (F,wt=19): 112 ((c4 * c2) * c3) * c1 != ((c1 * c2) * (c4 * e)) * (c3 * c4). [para(22(a,2),18(a,2))]. given #29 (T,wt=9): 122 e * ((x * x) * e) = x. [para(22(a,2),28(a,1,1)),demod(11(3),91(5))]. given #30 (T,wt=9): 143 x / e = e * (x * x). [back_demod(60),demod(91(4))]. given #31 (A,wt=15): 24 (x * y) * ((x * z) * u) = z * (y * u). [para(11(a,1),12(a,1,1)),flip(a)]. given #32 (F,wt=19): 158 ((c4 * c1) * (c2 * e)) * (c3 * c1) != ((c1 * c2) * c3) * c4. [para(12(a,1),110(a,1,1))]. given #33 (F,wt=19): 196 ((c4 * c2) * c3) * c1 != ((c1 * c4) * (c2 * e)) * (c3 * c4). [para(12(a,1),112(a,2,1))]. given #34 (T,wt=9): 151 e / x = e * (x * x). [back_demod(42),demod(91(4))]. given #35 (T,wt=9): 198 (x * x) * e = e * x. [para(122(a,1),11(a,1,2)),flip(a)]. given #36 (A,wt=15): 25 (x * y) * (z * (y * u)) = (x * z) * u. [para(11(a,1),12(a,1,2)),flip(a)]. given #37 (F,wt=19): 273 ((c4 * c1) * c3) * ((c2 * e) * c1) != ((c1 * c2) * c3) * c4. [para(12(a,1),158(a,1))]. given #38 (F,wt=19): 279 ((c4 * c2) * c3) * c1 != ((c1 * c4) * c3) * ((c2 * e) * c4). [para(12(a,1),196(a,2))]. given #39 (T,wt=11): 46 (x * y) * (e * (y * x)) = x. [para(11(a,1),20(a,1,1,1)),demod(11(7))]. given #40 (T,wt=11): 52 (x * (x / y)) * (e * y) = x. [para(16(a,1),20(a,1,1,1)),demod(16(7))]. given #41 (A,wt=23): 27 (x * (y * z)) * (u * (v * w)) = (x * u) * ((y * v) * (z * w)). [para(12(a,1),12(a,1,2)),flip(a)]. given #42 (F,wt=27): 631 c4 * (c3 * (e * ((c2 * c4) * (e * c1)))) != c1 * (c3 * (e * ((c2 * c1) * (e * c4)))). [back_demod(18),demod(461(7),461(20))]. given #43 (F,wt=27): 797 c1 * (c3 * (e * ((c2 * c1) * (e * c4)))) != c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))). [para(12(a,1),631(a,1,2,2,2)),flip(a)]. given #44 (T,wt=11): 58 (x * (y / x)) * (e * y) = x. [para(36(a,1),20(a,1,1,1)),demod(36(7))]. given #45 (T,wt=11): 91 (x * y) * x = e * (y * x). [para(11(a,1),22(a,1,1)),flip(a)]. given #46 (A,wt=15): 38 (x * (y / z)) * (u * z) = (x * u) * y. [para(16(a,1),12(a,1,2)),flip(a)]. given #47 (F,wt=27): 798 c4 * (c3 * (e * ((c2 * c4) * (e * c1)))) != c1 * (c3 * (e * ((c2 * e) * (c1 * c4)))). [para(12(a,1),631(a,2,2,2,2))]. given #48 (F,wt=27): 811 c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))) != c1 * (c3 * (e * ((c2 * e) * (c1 * c4)))). [para(12(a,1),797(a,1,2,2,2)),flip(a)]. given #49 (T,wt=11): 291 (x * e) * (x * e) = e * x. [para(198(a,1),22(a,2)),demod(19(3))]. given #50 (T,wt=11): 442 x / (e * (y * x)) = x * y. [para(46(a,1),40(a,1,2)),demod(57(4))]. given #51 (A,wt=15): 56 (x * (y / z)) * (u * y) = (x * u) * z. [para(36(a,1),12(a,1,2)),flip(a)]. given #52 (F,wt=29): 574 (x * c3) * ((x * ((c1 * c2) * (c4 * e))) * c4) != c4 * (c3 * (e * ((c2 * c4) * (e * c1)))). [back_demod(261),demod(461(7)),flip(a)]. given #53 (F,wt=29): 583 (x * c3) * ((x * ((c4 * c2) * (c1 * e))) * c1) != c1 * (c3 * (e * ((c2 * c1) * (e * c4)))). [back_demod(237),demod(461(20))]. given #54 (T,wt=9): 1119 x / (x * e) = e * x. [para(291(a,1),442(a,1,2,2)),demod(11(6),57(3),291(8))]. given #55 (T,wt=11): 824 (e * x) / y = y * (x / y). [para(58(a,1),40(a,1,2))]. given #56 (A,wt=23): 65 (x * (y * (x * z))) * ((x * u) * v) = (x * (y * u)) * (z * v). [para(21(a,1),12(a,1,1)),demod(64(8)),flip(a)]. given #57 (F,wt=29): 1247 (x * c3) * ((x * ((c1 * c2) * (c4 * e))) * c4) != c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))). [para(12(a,1),574(a,2,2,2,2))]. given #58 (F,wt=29): 1287 (x * c3) * ((x * ((c4 * c2) * (c1 * e))) * c1) != c1 * (c3 * (e * ((c2 * e) * (c1 * c4)))). [para(12(a,1),583(a,2,2,2,2))]. given #59 (T,wt=11): 902 x * (e * (x * e)) = e * x. [back_demod(198),demod(883(3))]. given #60 (T,wt=11): 1110 e * (x * e) = x * (e * x). [back_demod(603),demod(1095(7)),flip(a)]. given #61 (A,wt=23): 66 (x * ((y * e) * z)) * (u * (y * v)) = (x * u) * (y * (z * v)). [para(21(a,1),12(a,1,2)),flip(a)]. given #62 (F,wt=31): 487 c1 * (c3 * (e * ((c4 * c1) * (e * ((c2 * e) * c4))))) != c4 * (c3 * (e * ((c2 * c4) * (e * c1)))). [back_demod(428),demod(461(7),463(27),461(24)),flip(a)]. given #63 (F,wt=31): 500 c1 * (c3 * (e * ((c2 * c1) * (e * c4)))) != c4 * (c3 * (e * ((c1 * c4) * (e * ((c2 * e) * c1))))). [back_demod(415),demod(463(14),461(11),461(24)),flip(a)]. given #64 (T,wt=11): 1113 x / (e * y) = x * (x / y). [para(36(a,1),442(a,1,2,2))]. given #65 (T,wt=11): 1326 e * (x * (e * x)) = x * e. [para(1119(a,1),36(a,1,1)),demod(312(3))]. given #66 (A,wt=19): 68 x * ((y * z) * (u * v)) = x * ((y * u) * (z * v)). [para(12(a,1),21(a,2,2)),demod(64(7),11(4))]. given #67 (F,wt=31): 553 c4 * (c3 * (e * ((c2 * c4) * (e * c1)))) != c1 * (x * (e * ((c2 * c1) * (e * (c3 * (x * c4)))))). [back_demod(311),demod(461(7),461(22))]. given #68 (F,wt=27): 2290 c4 * (c3 * (e * ((c2 * c4) * (e * c1)))) != c1 * ((c2 * c1) * (e * (c3 * (e * c4)))). [para(11(a,1),553(a,2,2))]. given #69 (T,wt=13): 144 x * (e * (x * x)) = e * (x * x). [back_demod(54),demod(91(2),91(6))]. given #70 (T,wt=11): 3531 x * (y * x) = y * (x * y). [back_demod(2726),demod(3184(19),11(7),11(6))]. given #71 (A,wt=15): 313 x * (y * (z * u)) = z * (y * (x * u)). [para(36(a,1),25(a,1,1)),demod(306(6))]. given #72 (F,wt=47): 2436 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_demod(2291),demod(2355(10),11(18),11(25),2355(35),11(43),11(50))]. given #73 (F,wt=47): 3061 c4 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))). [back_demod(1067),demod(2355(10),11(23),11(25),2355(35),11(48),2355(50),11(55),2355(62),11(67),11(64),11(63),11(60),11(59),11(57),315(55),315(51))]. given #74 (T,wt=11): 3548 x * (y * (x * y)) = y * x. [para(3531(a,1),11(a,1,2))]. given #75 (T,wt=11): 3550 (x * y) / (x * (y * x)) = y. [para(3531(a,1),40(a,1,2))]. given #76 (A,wt=15): 315 x * (y * (z * (x * (y * u)))) = z * u. [para(36(a,1),25(a,2,1)),demod(306(5))]. given #77 (F,wt=47): 3071 c4 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c2 * (e * (c2 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))). [back_demod(1056),demod(2355(10),11(18),11(25),2355(35),11(48),2355(50),11(55),2355(62),11(67),11(64),11(63),11(60),11(59),11(57),315(55),315(51))]. given #78 (F,wt=47): 3225 c4 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [back_demod(819),demod(2355(12),11(25),2355(27),11(32),2355(39),11(44),11(41),11(40),11(37),11(36),11(34),315(32),315(28),2355(33),11(41),11(48))]. given #79 (T,wt=13): 440 x * (e * (y * (x / y))) = x / y. [para(16(a,1),46(a,1,1))]. given #80 (T,wt=13): 441 x * (e * (y * (y / x))) = y / x. [para(36(a,1),46(a,1,1))]. given #81 (A,wt=15): 400 x * (y * (z * (x * u))) = z * (y * u). [back_demod(217),demod(306(3))]. given #82 (F,wt=47): 3234 c4 * (c3 * (c2 * (e * (c2 * (e * (c4 * (e * (c2 * (e * (c2 * c1)))))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c1 * (e * (c2 * (e * (c2 * c4)))))))))). [back_demod(807),demod(2355(10),11(18),11(25),2355(35),11(43),2355(50),11(55),2355(62),11(67),11(64),11(63),11(60),11(59),11(57),315(55),315(51))]. given #83 (F,wt=47): 3573 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(313(a,1),2436(a,1,2,2,2,2,2,2))]. given #84 (T,wt=13): 842 e * (x * (y / x)) = y * (y / x). [para(16(a,1),91(a,1,1)),flip(a)]. given #85 (T,wt=13): 843 e * (x * (x / y)) = y * (x / y). [para(36(a,1),91(a,1,1)),flip(a)]. given #86 (A,wt=17): 403 e * (x * (e * (y * y))) = y * (x * (y * y)). [back_demod(200),demod(312(4))]. given #87 (F,wt=47): 3574 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(313(a,1),2436(a,1,2,2,2,2))]. given #88 (F,wt=47): 3575 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(313(a,1),2436(a,1,2))]. given #89 (T,wt=13): 1087 e * (x * (y * e)) = y * (x * e). [para(291(a,1),24(a,1,2)),demod(296(4)),flip(a)]. given #90 (T,wt=13): 1816 (x * e) / (x * x) = x * (e * x). [para(1110(a,1),1119(a,2)),demod(897(6),11(8),144(7),11(7))]. given #91 (A,wt=15): 455 e * (x * y) = z * (x * (e * (z * y))). [para(46(a,1),24(a,1,2)),demod(91(2))]. given #92 (F,wt=47): 3576 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(313(a,1),2436(a,1))]. given #93 (F,wt=47): 3577 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(313(a,1),2436(a,2,2,2,2,2,2,2,2,2))]. given #94 (T,wt=13): 3589 (x / y) * (y * x) = y * (x / y). [para(16(a,1),3548(a,1,2,2))]. given #95 (T,wt=13): 3590 (x / y) * (x * y) = x * (x / y). [para(36(a,1),3548(a,1,2,2))]. given #96 (A,wt=27): 473 x * (y * (e * (z * (x * (e * (x * u)))))) = x * (z * (x * (y * (x * u)))). [back_demod(77),demod(461(8),461(10),11(11),461(8),312(10),11(10),11(7),11(7),11(4))]. given #97 (F,wt=47): 3578 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(313(a,1),2436(a,2,2,2,2,2,2,2,2))]. given #98 (F,wt=47): 3579 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(313(a,1),2436(a,2,2,2,2,2))]. given #99 (T,wt=13): 3607 (x * y) / (x * (y / x)) = y / x. [para(16(a,1),3550(a,1,2,2)),demod(57(4))]. Demod_limit: 0 (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(315(a,1),3607(a,1,1)),demod(57(6),4377(7),2355(17),11(22),2355(23),11(28),2355(29),11(34),2355(35),11(40),11(47),11(48),11(49),2355(51),2355(61),11(66),2355(67),11(72),2355(73),11(78),11(85),11(86),11(87),11(88),2355(85),2355(95),11(100),2355(101),11(106),2355(107),11(112),11(119),11(120),11(121),1113(122),4377(122),2355(360),11(365),2355(366),11(374),11(372),11(370),2355(367),2355(377),11(382),2355(383),11(391),11(389),11(387),2355(384),2355(394),11(399),2355(400),11(408),11(406),11(404),2355(401),2355(411),11(416),2355(417),11(425),11(423),11(421),2355(418),2355(428),11(436),11(434),11(432),2355(429),2355(439),11(447),11(445),11(443),2355(440),2355(450),11(458),11(456),11(454),2355(451),2355(461),11(466),2355(467),11(475),11(473),11(471),2355(468),2355(478),11(483),2355(484),11(492),11(490),11(488),2355(485),2355(495),11(500),2355(501),11(509),11(507),11(505),2355(502),2355(512),11(520),11(518),11(516),2355(513),3184(522),11(507),2355(508),11(517),11(515),2355(513),11(518),11(515),11(514),2355(513),11(518),2355(519),11(527),11(525),11(523),2355(520),2355(530),11(535),2355(536),11(544),11(542),11(540),2355(537),2355(547),11(552),2355(553),11(561),11(559),11(557),2355(554),2355(564),11(572),11(570),11(568),2355(565),2355(575),11(583),11(581),11(579),2355(576),2355(586),11(594),11(592),11(590),2355(587),2355(597),11(602),2355(603),11(611),11(609),11(607),2355(604),2355(614),11(619),2355(620),11(628),11(626),11(624),2355(621),2355(631),11(636),2355(637),11(645),11(643),11(641),2355(638),2355(648),11(656),11(654),11(652),2355(649),2355(659),11(667),11(665),11(663),2355(660),2355(670),11(678),11(676),11(674),2355(671),2355(681),11(686),2355(687),11(695),11(693),11(691),2355(688),2355(698),11(703),2355(704),11(712),11(710),11(708),2355(705),2355(715),11(720),2355(721),11(729),11(727),11(725),2355(722),2355(732),11(740),11(738),11(736),2355(733),2355(743),11(751),11(749),11(747),2355(744),2355(754),11(762),11(760),11(758),2355(755),2355(765),11(770),2355(771),11(779),11(777),11(775),2355(772),2355(782),11(787),2355(788),11(796),11(794),11(792),2355(789),2355(799),11(804),2355(805),11(813),11(811),11(809),2355(806),11(822),11(820),11(818),2515(819),11(799),11(800),11(798),11(796),11(798),11(799),11(797),11(795),11(797),11(798),11(796),11(794),11(796),11(794),11(792),11(794),11(792),11(790),11(792),11(790),11(788),11(790),11(791),11(789),11(787),11(789),11(790),11(788),11(786),11(788),11(789),11(787),11(785),11(787),11(785),11(783),11(785),11(783),11(781),11(783),11(781),11(779),11(781),11(782),11(780),11(778),11(780),11(781),11(779),11(777),11(779),11(780),11(778),11(776),11(778),11(776),11(774),11(776),11(774),11(772),11(774),11(772),11(770),11(772),11(773),11(771),11(769),11(771),11(772),11(770),11(768),11(770),11(771),11(769),11(767),11(769),11(767),11(765),3184(766),11(751),11(753),11(751),11(749),11(746),11(745),11(744),11(745),11(743),11(741),11(743),11(744),11(742),11(740),11(742),11(743),11(741),11(739),11(741),11(739),11(737),11(739),11(737),11(735),11(737),11(735),11(733),11(735),11(736),11(734),11(732),11(734),11(735),11(733),11(731),11(733),11(734),11(732),11(730),2355(732),11(737),2355(744),11(749),2355(750),11(758),11(756),11(754),2355(751),2355(761),11(766),2355(767),11(775),11(773),11(771),2355(768),2355(778),11(783),2355(784),11(792),11(790),11(788),2355(785),2355(795),11(800),2355(801),11(809),11(807),11(805),2355(802),2355(812),11(820),11(818),11(816),2355(813),2355(823),11(831),11(829),11(827),2355(824),2355(834),11(842),11(840),11(838),2355(835),2355(845),11(850),2355(851),11(859),11(857),11(855),2355(852),2355(862),11(867),2355(868),11(876),11(874),11(872),2355(869),2355(879),11(884),2355(885),11(893),11(891),11(889),2355(886),2355(896),11(904),11(902),11(900),2355(897),3184(906),11(891),2355(892),11(901),11(899),2355(897),11(902),11(899),11(898),2355(897),11(902),2355(903),11(911),11(909),11(907),2355(904),2355(914),11(919),2355(920),11(928),11(926),11(924),2355(921),2355(931),11(936),2355(937),11(945),11(943),11(941),2355(938),2355(948),11(956),11(954),11(952),2355(949),2355(959),11(967),11(965),11(963),2355(960),2355(970),11(978),11(976),11(974),2355(971),2355(981),11(986),2355(987),11(995),11(993),11(991),2355(988),2355(998),11(1003),2355(1004),11(1012),11(1010),11(1008),2355(1005),2355(1015),11(1020),2355(1021),11(1029),11(1027),11(1025),2355(1022),2355(1032),11(1040),11(1038),11(1036),2355(1033),2355(1043),11(1051),11(1049),11(1047),2355(1044),2355(1054),11(1062),11(1060),11(1058),2355(1055),2355(1065),11(1070),2355(1071),11(1079),11(1077),11(1075),2355(1072))]. Demod_limit (steps=-1, size=1827). The most recent kept clause is 4381. From here on, a short message will be printed for each 100 times the limit is hit. given #100 (T,wt=13): 3615 x * (e * (y * (x * e))) = y * e. [para(19(a,1),315(a,1,2,2,2,2))]. given #101 (A,wt=17): 634 e * (x * (e * (y * (e * x)))) = x * (y * e). [para(52(a,1),22(a,1,1)),demod(143(5),144(7),312(7),91(11),461(10),19(11),198(10),11(10),312(7)),flip(a)]. given #102 (F,wt=47): 3580 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(313(a,1),2436(a,2,2,2))]. given #103 (F,wt=47): 3581 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(313(a,1),3061(a,1,2,2,2,2,2,2,2,2))]. given #104 (T,wt=15): 901 e * (x * e) = y * (e * (y * (x * y))). [back_demod(246),demod(883(3)),flip(a)]. given #105 (T,wt=15): 927 e * (x * (e * (x * (y * x)))) = y * e. [back_demod(179),demod(897(5),896(12),11(7))]. given #106 (A,wt=23): 637 x * (y * (e * (z * (e * (x * (y * u)))))) = e * (z * (e * u)). [para(52(a,1),23(a,1,2,1)),demod(461(6),36(3),312(12))]. given #107 (F,wt=47): 3582 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(313(a,1),3061(a,1,2))]. given #108 (F,wt=47): 3583 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(313(a,1),3061(a,1))]. given #109 (T,wt=15): 2721 x * (e * (y * e)) = x * (y * (e * y)). [back_demod(1776),demod(2355(6),2355(22),11(27),11(24),11(23),11(20),11(19),11(17),315(15),315(11))]. given #110 (T,wt=15): 3570 x * (y * (z * y)) = z * (x * (y * x)). [para(3531(a,1),313(a,1,2)),flip(a)]. given #111 (A,wt=23): 639 e * (x * (e * (y * z))) = u * (y * (e * (x * (e * (u * z))))). [para(52(a,1),24(a,1,2,1)),demod(461(5),36(3),312(12)),flip(a)]. given #112 (F,wt=41): 5001 c1 * (c3 * (c4 * (e * (c4 * (e * (c1 * (c2 * c2))))))) != c4 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * c1)))))))))). [back_demod(2816),demod(4957(32),11(17),11(14))]. given #113 (F,wt=41): 5002 c4 * (c3 * (c1 * (e * (c1 * (e * (c4 * (c2 * c2))))))) != c1 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c1 * c4)))))))))). [back_demod(2800),demod(4957(32),11(17),11(14))]. given #114 (T,wt=15): 3595 x * (y * (z * (y * x))) = z * (x * y). [para(3548(a,1),313(a,1,2)),flip(a)]. given #115 (T,wt=15): 3625 x * (y * (z * (y * (x * y)))) = z * x. [para(3531(a,1),315(a,1,2,2,2))]. given #116 (A,wt=29): 887 e * (x * (y * z)) = x * (y * (z * (e * (z * (e * (y * (e * (y * (e * x))))))))). [back_demod(738),demod(883(10),883(14))]. given #117 (F,wt=37): 5609 c1 * (c3 * (c4 * (e * (c4 * (e * (c1 * (c2 * c2))))))) != c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))). [para(3595(a,2),5001(a,1,2,2,2,2,2,2)),demod(11(15),5437(38))]. given #118 (F,wt=37): 5624 c4 * (c3 * (c1 * (e * (c1 * (e * (c4 * (c2 * c2))))))) != c1 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c1 * c4)))))))). [para(3595(a,2),5002(a,1,2,2,2,2,2,2)),demod(11(15),5437(38))]. given #119 (T,wt=15): 3715 x * (y * (e * (y * (e * (x * e))))) = y. [para(40(a,1),440(a,1,2,2,2)),demod(2355(3),3548(10),11(8),19(7),11(12),40(11))]. given #120 (T,wt=15): 3755 x * (y * (z * (x * z))) = y * (z * y). [para(400(a,2),3531(a,1))]. given #121 (A,wt=25): 922 e * (x * (e * (x * (e * (y * (e * (y * (z * x)))))))) = z * (e * y). [back_demod(297),demod(897(5),896(12),883(6))]. ============================== PROOF ================================= % Proof 1 at 8.84 (+ 0.03) seconds. % Length of proof is 90. % Level of proof is 16. % Maximum clause weight is 65. % Given clauses 121. 10 (x * e) * x = x. [input]. 11 x * (x * y) = y. [input]. 12 (x * y) * (z * u) = (x * z) * (y * u). [input]. 13 ((x * x) * x) * x = e. [input]. 16 (x / y) * y = x. [input]. 17 (x * y) / y = x. [input]. 18 ((c4 * c2) * c3) * c1 != ((c1 * c2) * c3) * c4. [clausify]. 19 e * e = e. [para(10(a,1),10(a,1,1)),demod(11(5)),flip(a)]. 20 ((x * y) * x) * (e * y) = x * y. [para(12(a,1),10(a,1))]. 21 ((x * e) * y) * (x * z) = x * (y * z). [para(10(a,1),12(a,1,1)),flip(a)]. 22 (x * (y * e)) * (z * y) = (x * z) * y. [para(10(a,1),12(a,1,2)),flip(a)]. 23 (x * y) * ((x * z) * (y * u)) = z * u. [para(12(a,1),11(a,1,2))]. 24 (x * y) * ((x * z) * u) = z * (y * u). [para(11(a,1),12(a,1,1)),flip(a)]. 25 (x * y) * (z * (y * u)) = (x * z) * u. [para(11(a,1),12(a,1,2)),flip(a)]. 28 ((x * x) * x) * e = x. [para(13(a,1),11(a,1,2))]. 36 (x / y) * x = y. [para(16(a,1),11(a,1,2))]. 40 x / (y * x) = y. [para(11(a,1),17(a,1,1))]. 42 e / x = (x * x) * x. [para(13(a,1),17(a,1,1))]. 46 (x * y) * (e * (y * x)) = x. [para(11(a,1),20(a,1,1,1)),demod(11(7))]. 52 (x * (x / y)) * (e * y) = x. [para(16(a,1),20(a,1,1,1)),demod(16(7))]. 54 x * ((x * x) * x) = (x * x) * x. [para(36(a,1),10(a,1,1)),demod(42(2),42(5))]. 60 x / e = (x * x) * x. [para(13(a,1),40(a,1,2))]. 64 ((x * e) * y) * z = x * (y * (x * z)). [para(11(a,1),21(a,1,2))]. 65 (x * (y * (x * z))) * ((x * u) * v) = (x * (y * u)) * (z * v). [para(21(a,1),12(a,1,1)),demod(64(8)),flip(a)]. 70 ((x * x) * x) * (y * x) = (x * y) * e. [para(13(a,1),21(a,1,2)),demod(28(4)),flip(a)]. 72 ((x * x) * x) * (y * z) = (x * y) * (((x * x) * x) * z). [para(16(a,1),21(a,1,1,1)),demod(60(3),60(7)),flip(a)]. 84 x * ((x * e) * e) = x. [para(42(a,1),40(a,1)),demod(64(8),11(5))]. 85 (x * e) * e = x * x. [para(84(a,1),11(a,1,2)),flip(a)]. 91 (x * y) * x = e * (y * x). [para(11(a,1),22(a,1,1)),flip(a)]. 101 (e * (x * x)) * x = e. [para(22(a,2),13(a,1,1)),demod(11(3))]. 112 ((c4 * c2) * c3) * c1 != ((c1 * c2) * (c4 * e)) * (c3 * c4). [para(22(a,2),18(a,2))]. 122 e * ((x * x) * e) = x. [para(22(a,2),28(a,1,1)),demod(11(3),91(5))]. 139 (e * (x * x)) * (y * z) = (x * y) * ((e * (x * x)) * z). [back_demod(72),demod(91(2),91(8))]. 141 (e * (x * x)) * (y * x) = (x * y) * e. [back_demod(70),demod(91(2))]. 144 x * (e * (x * x)) = e * (x * x). [back_demod(54),demod(91(2),91(6))]. 168 (x * x) * y = x * ((y * e) * (x * (e * y))). [para(85(a,1),22(a,2,1)),demod(64(8)),flip(a)]. 191 ((x * y) * (x * y)) * y = e * (x * e). [para(101(a,1),23(a,1,2)),demod(91(4)),flip(a)]. 198 (x * x) * e = e * x. [para(122(a,1),11(a,1,2)),flip(a)]. 217 x * (((y / x) * z) * u) = z * (y * u). [para(36(a,1),24(a,1,1))]. 246 (x * x) * (y * x) = e * (y * e). [para(101(a,1),24(a,1,2)),demod(91(4)),flip(a)]. 261 ((c4 * c2) * c3) * c1 != (x * c3) * ((x * ((c1 * c2) * (c4 * e))) * c4). [para(24(a,2),112(a,2))]. 291 (x * e) * (x * e) = e * x. [para(198(a,1),22(a,2)),demod(19(3))]. 296 (x * y) * (e * x) = x * (y * e). [para(198(a,1),24(a,1,2))]. 297 (x * (y * y)) * ((x * z) * e) = z * (e * y). [para(198(a,1),24(a,2,2))]. 306 ((x / y) * z) * u = x * (z * (y * u)). [para(16(a,1),25(a,1,1)),flip(a)]. 312 (e * x) * y = e * (x * (e * y)). [para(19(a,1),25(a,1,1)),flip(a)]. 313 x * (y * (z * u)) = z * (y * (x * u)). [para(36(a,1),25(a,1,1)),demod(306(6))]. 315 x * (y * (z * (x * (y * u)))) = z * u. [para(36(a,1),25(a,2,1)),demod(306(5))]. 400 x * (y * (z * (x * u))) = z * (y * u). [back_demod(217),demod(306(3))]. 406 (x * y) * e = e * ((x * x) * (e * (y * x))). [back_demod(141),demod(312(5)),flip(a)]. 408 (x * y) * (e * ((x * x) * (e * z))) = e * ((x * x) * (e * (y * z))). [back_demod(139),demod(312(5),312(12)),flip(a)]. 461 ((x * y) * z) * u = x * (z * (e * ((y * x) * (e * u)))). [para(46(a,1),25(a,1,1)),demod(312(4)),flip(a)]. 574 (x * c3) * ((x * ((c1 * c2) * (c4 * e))) * c4) != c4 * (c3 * (e * ((c2 * c4) * (e * c1)))). [back_demod(261),demod(461(7)),flip(a)]. 603 x * ((x * y) * (e * (y * (x * e)))) = e * (x * e). [back_demod(191),demod(461(4),296(6))]. 637 x * (y * (e * (z * (e * (x * (y * u)))))) = e * (z * (e * u)). [para(52(a,1),23(a,1,2,1)),demod(461(6),36(3),312(12))]. 862 (x * y) * (z * (y * x)) = e * (z * x). [para(91(a,1),25(a,2))]. 883 (x * x) * y = x * (e * (x * y)). [back_demod(168),demod(862(8))]. 896 (x * y) * (e * (x * (e * (x * (e * z))))) = e * (x * (e * (x * (e * (y * z))))). [back_demod(408),demod(883(6),883(16))]. 897 (x * y) * e = e * (x * (e * (x * (e * (y * x))))). [back_demod(406),demod(883(9))]. 901 e * (x * e) = y * (e * (y * (x * y))). [back_demod(246),demod(883(3)),flip(a)]. 922 e * (x * (e * (x * (e * (y * (e * (y * (z * x)))))))) = z * (e * y). [back_demod(297),demod(897(5),896(12),883(6))]. 1087 e * (x * (y * e)) = y * (x * e). [para(291(a,1),24(a,1,2)),demod(296(4)),flip(a)]. 1095 (x * y) * (e * (y * (x * e))) = e * x. [para(291(a,1),25(a,2))]. 1110 e * (x * e) = x * (e * x). [back_demod(603),demod(1095(7)),flip(a)]. 1247 (x * c3) * ((x * ((c1 * c2) * (c4 * e))) * c4) != c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))). [para(12(a,1),574(a,2,2,2,2))]. 1360 e * ((x * (e * y)) * z) = e * ((x * e) * (e * (y * z))). [para(19(a,1),65(a,1,2,1)),demod(312(8),11(8),312(12))]. 1620 c1 * (c3 * (e * ((c4 * c1) * (e * ((c2 * e) * c4))))) != c4 * (c3 * (e * ((c2 * e) * (c4 * c1)))). [para(23(a,1),1247(a,1,2,1)),demod(461(11))]. 1768 e * (x * (e * ((y * e) * (e * (y * (x * z)))))) = (y * e) * z. [para(1110(a,1),23(a,1,2,1)),demod(312(8),1360(8))]. 1771 (x * e) * (x * (e * (x * (e * (y * x))))) = y * (x * y). [para(1110(a,2),23(a,1,2)),demod(897(6),11(13))]. 2355 (x * y) * z = e * (x * (e * (x * (e * (y * (e * (x * (e * (x * (e * z)))))))))). [para(144(a,1),25(a,1,1)),demod(312(7),883(8),312(13),883(14)),flip(a)]. 2726 e * (x * (e * (x * (e * (x * (e * (x * (e * (x * (e * (x * (e * (y * x))))))))))))) = y * (x * y). [back_demod(1771),demod(2355(10),11(20))]. 2727 e * (x * (e * (x * (e * (x * (e * (x * (e * y)))))))) = e * (z * (x * (e * (x * (e * (x * (e * (z * y)))))))). [back_demod(1768),demod(2355(9),11(14),11(11),11(13),11(15),2355(16),11(26)),flip(a)]. 2816 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_demod(1620),demod(2355(12),11(25),11(27),2355(24),11(43),2355(51),11(64),11(66))]. 3184 e * (x * (e * (x * (e * (x * (e * (x * (e * (x * (e * y)))))))))) = x * (e * (x * y)). [back_demod(883),demod(2355(2))]. 3531 x * (y * x) = y * (x * y). [back_demod(2726),demod(3184(19),11(7),11(6))]. 3548 x * (y * (x * y)) = y * x. [para(3531(a,1),11(a,1,2))]. 3570 x * (y * (z * y)) = z * (x * (y * x)). [para(3531(a,1),313(a,1,2)),flip(a)]. 3595 x * (y * (z * (y * x))) = z * (x * y). [para(3548(a,1),313(a,1,2)),flip(a)]. 3615 x * (e * (y * (x * e))) = y * e. [para(19(a,1),315(a,1,2,2,2,2))]. 3627 x * (y * (z * (u * (v * (x * (u * w)))))) = z * (y * (v * w)). [para(315(a,1),313(a,1,2,2)),flip(a)]. 3806 x * (y * (z * (x * (z * y)))) = y * z. [para(400(a,2),3548(a,1))]. 4648 x * (e * (y * (e * (y * (x * y))))) = e. [para(901(a,1),3615(a,1,2,2)),demod(19(11))]. 4677 x * (y * (z * (e * (u * (e * (y * (x * v))))))) = z * (e * (u * (e * v))). [para(637(a,1),313(a,1,2)),flip(a)]. 4957 e * (x * (e * (y * (e * (y * (e * (y * (e * (y * (e * x)))))))))) = x * (e * (y * y)). [para(901(a,1),3570(a,1,2,2)),demod(2355(8),4648(14),19(8),11(9),3548(7),11(5),2355(8),11(18)),flip(a)]. 5001 c1 * (c3 * (c4 * (e * (c4 * (e * (c1 * (c2 * c2))))))) != c4 * (c3 * (c2 * (e * (c2 * (e * (c2 * (e * (c2 * (e * (c4 * c1)))))))))). [back_demod(2816),demod(4957(32),11(17),11(14))]. 5437 x * (e * (x * (e * (x * (e * (x * (e * y))))))) = e * (x * (e * (x * (e * (x * y))))). [para(1087(a,1),3595(a,1,2,2)),demod(2355(7),3806(13),11(9),11(8),2355(13),11(23),11(25)),flip(a)]. 5609 c1 * (c3 * (c4 * (e * (c4 * (e * (c1 * (c2 * c2))))))) != c4 * (c3 * (e * (c2 * (e * (c2 * (e * (c2 * (c4 * c1)))))))). [para(3595(a,2),5001(a,1,2,2,2,2,2,2)),demod(11(15),5437(38))]. 6028 e * (x * (y * (e * (y * (e * (y * (e * (x * z)))))))) = y * (e * (y * (e * (y * z)))). [back_demod(2727),demod(5437(13),11(11)),flip(a)]. 6706 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(922(a,2),5609(a,1,2,2,2,2)),demod(2355(21),2355(34),11(42),5437(47),11(38),11(40),11(42),2355(39),5437(50),4677(42),4677(36),11(31),2355(28),315(37),315(31),11(31),6028(29),11(24),11(25)),flip(a)]. 6707 $F. [resolve(6706,a,3627,a(flip))]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=121. Generated=14070. Kept=6697. proofs=1. Usable=36. Sos=2672. Demods=382. Denials=0. 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=1110211. 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.90. User_CPU=8.84, System_CPU=0.03, Wall_clock=9. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13015 exit (max_proofs) Mon Jun 19 16:40:19 2006