============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11392 was started by mccune on cleo.thornwood, Sat Aug 12 21:00:11 2006 The command was "/home/mccune/bin/prover9 -f quot-xy3a.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file quot-xy3a.in op(400,infix_right,*). set(restrict_denials). assign(max_weight,35). formulas(sos). (x * y) * z = x * y * z # label(associativity). x * y != u | x * z != u | y = z # label(left_cancellation_extended). y * x != u | z * x != u | y = z # label(right_cancellation_extended). x * y * x * y * x * y = x * x * x * y * y * y # label("(xy)^3 = x^3y^3"). b * b0 = a * a0. d * b0 = c * a0. b * d0 = a * c0. d * d0 != c * c0. end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). (x * y) * z = x * y * z # label(associativity). [assumption]. x * y != z | x * u != z | y = u # label(left_cancellation_extended). [assumption]. x * y != z | u * y != z | x = u # label(right_cancellation_extended). [assumption]. x * y * x * y * x * y = x * x * x * y * y * y # label("(xy)^3 = x^3y^3"). [assumption]. b * b0 = a * a0. [assumption]. d * b0 = c * a0. [assumption]. b * d0 = a * c0. [assumption]. d * d0 != c * c0. [assumption]. 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([ a, a0, b, b0, c, c0, d, d0, * ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 3). % (nonunit Horn with equality) Auto_process settings: (no changes). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 (x * y) * z = x * y * z # label(associativity). [assumption]. 2 x * y != z | x * u != z | y = u # label(left_cancellation_extended). [assumption]. 3 x * y != z | u * y != z | x = u # label(right_cancellation_extended). [assumption]. 4 x * y * x * y * x * y = x * x * x * y * y * y # label("(xy)^3 = x^3y^3"). [assumption]. 5 b * b0 = a * a0. [assumption]. 6 d * b0 = c * a0. [assumption]. 7 b * d0 = a * c0. [assumption]. 8 d * d0 != c * c0. [assumption]. end_of_list. formulas(demodulators). 1 (x * y) * z = x * y * z # label(associativity). [assumption]. 5 b * b0 = a * a0. [assumption]. 6 d * b0 = c * a0. [assumption]. 7 b * d0 = a * c0. [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=11): 1 (x * y) * z = x * y * z # label(associativity). [assumption]. given #2 (I,wt=13): 2 x * y != z | x * u != z | y = u # label(left_cancellation_extended). [assumption]. given #3 (I,wt=13): 3 x * y != z | u * y != z | x = u # label(right_cancellation_extended). [assumption]. given #4 (I,wt=23): 4 x * y * x * y * x * y = x * x * x * y * y * y # label("(xy)^3 = x^3y^3"). [assumption]. given #5 (I,wt=7): 5 b * b0 = a * a0. [assumption]. given #6 (I,wt=7): 6 d * b0 = c * a0. [assumption]. given #7 (I,wt=7): 7 b * d0 = a * c0. [assumption]. given #8 (I,wt=0): 8 d * d0 != c * c0. [assumption]. given #9 (T,wt=11): 22 b * b0 * x = a * a0 * x. [para(5(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. given #10 (T,wt=11): 26 d * b0 * x = c * a0 * x. [para(6(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. given #11 (A,wt=17): 9 x * y * z != u | x * y * v != u | z = v. [para(1(a,1),2(a,1)),rewrite(1(5))]. given #12 (F,wt=0): 34 d * d0 * x * c * c0 * x * c * c0 * x != c * c0 * c * c0 * c * c0 * x * x * x. [ur(3,b,4,a,c,8,a),rewrite(1(10),1(12),1(14),1(26),1(27),1(28))]. given #13 (F,wt=0): 35 d * d0 * x != c * c0 * x. [ur(3,b,1,a,c,8,a),rewrite(1(4))]. given #14 (T,wt=11): 30 b * d0 * x = a * c0 * x. [para(7(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. given #15 (T,wt=13): 23 a * a0 != x | b * y != x | b0 = y. [para(5(a,1),2(a,1))]. given #16 (A,wt=17): 10 x * y * z != u | v * z != u | x * y = v. [para(1(a,1),3(a,1))]. given #17 (F,wt=0): 36 c * c0 * x * c * c0 * x * c * c0 * x != d * d0 * c * c0 * c * c0 * x * x * x. [ur(3,b,4,a(flip),c,8,a),rewrite(1(12),1(13),1(14),1(24),1(26),1(28)),flip(a)]. given #18 (F,wt=0): 37 c * c0 * x * d * d0 * x * d * d0 * x != d * d0 * d * d0 * d * d0 * x * x * x. [ur(3,a,4,a,c,8,a),rewrite(1(10),1(12),1(14),1(26),1(27),1(28))]. given #19 (T,wt=13): 24 a * a0 != x | y * b0 != x | b = y. [para(5(a,1),3(a,1))]. given #20 (T,wt=13): 27 c * a0 != x | d * y != x | b0 = y. [para(6(a,1),2(a,1))]. given #21 (A,wt=19): 11 x * y * x * y * x = y * y * x * x * x. [hyper(2,a,xx,b,4,a),flip(a)]. given #22 (F,wt=0): 38 c * c0 * d * d0 * d * d0 * x * x * x != d * d0 * x * d * d0 * x * d * d0 * x. [ur(3,a,4,a(flip),c,8,a),rewrite(1(12),1(13),1(14),1(24),1(26),1(28))]. given #23 (F,wt=0): 39 x * y * d * d0 != x * y * c * c0. [ur(2,b,1,a,c,8,a),rewrite(1(5))]. given #24 (T,wt=13): 28 c * a0 != x | y * b0 != x | d = y. [para(6(a,1),3(a,1))]. given #25 (T,wt=13): 31 a * c0 != x | b * y != x | d0 = y. [para(7(a,1),2(a,1))]. given #26 (A,wt=27): 12 x * y * x * y * x * y * z = x * x * x * y * y * y * z. [para(4(a,1),1(a,1,1)),rewrite(1(6),1(5),1(4),1(3),1(2),1(11),1(10),1(9),1(8)),flip(a)]. given #27 (F,wt=0): 40 x * d * d0 != x * c * c0. [ur(2,b,1,a(flip),c,8,a),rewrite(1(8))]. given #28 (F,wt=0): 54 x * y * z * d * d0 != x * y * z * c * c0. [ur(9,b,1,a,c,8,a),rewrite(1(6))]. given #29 (T,wt=13): 32 a * c0 != x | y * d0 != x | b = y. [para(7(a,1),3(a,1))]. given #30 (T,wt=13): 99 a * a0 != x | a * c0 != x | d0 = b0. [para(7(a,1),23(b,1)),flip(c)]. given #31 (A,wt=35): 13 x * y * z * x * y * z * x * y * z = x * y * x * y * x * y * z * z * z. [para(4(a,1),1(a,1)),rewrite(1(6),1(7),1(8),1(11),1(13)),flip(a)]. given #32 (F,wt=0): 67 x * y * z * d * d0 * u * c * c0 * u * c * c0 * u != x * y * z * c * c0 * c * c0 * c * c0 * u * u * u. [ur(9,b,1,a,c,34,a),rewrite(1(17))]. given #33 (F,wt=0): 68 x * y * d * d0 * z * c * c0 * z * c * c0 * z != x * y * c * c0 * c * c0 * c * c0 * z * z * z. [ur(9,b,1,a(flip),c,34,a),rewrite(1(32))]. given #34 (T,wt=13): 154 a * a0 != x | c * a0 != x | d = b. [para(6(a,1),24(b,1)),flip(c)]. given #35 (T,wt=17): 41 a * a0 * x != y | b * z != y | b0 * x = z. [para(22(a,1),2(a,1))]. given #36 (A,wt=27): 14 x * y * z * y * z * y * z = x * y * y * y * z * z * z. [para(4(a,1),1(a,2,2)),rewrite(1(6))]. given #37 (F,wt=0): 69 c * c0 * c * c0 * c * c0 * x * x * x * c * c0 * c * c0 * c * c0 * x * x * x * c * c0 * c * c0 * c * c0 * x * x * x * y * y * y != d * d0 * x * c * c0 * x * c * c0 * x * y * c * c0 * c * c0 * c * c0 * x * x * x * y * c * c0 * c * c0 * c * c0 * x * x * x * y. [ur(3,b,4,a,c,34,a),rewrite(1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(47),1(46),1(45),1(44),1(43),1(42),1(41),1(40),1(92),1(91),1(90),1(89),1(88),1(87),1(86),1(85),1(93),1(92),1(91),1(90),1(89),1(88),1(87),1(86),1(94),1(93),1(92),1(91),1(90),1(89),1(88),1(87)),flip(a)]. given #38 (F,wt=0): 70 d * d0 * x * c * c0 * x * c * c0 * x * y != c * c0 * c * c0 * c * c0 * x * x * x * y. [ur(3,b,1,a,c,34,a),rewrite(1(15),1(14),1(13),1(12),1(11),1(10),1(9),1(8),1(29),1(28),1(27),1(26),1(25),1(24),1(23))]. given #39 (T,wt=17): 42 a * a0 * x != y | z * b0 * x != y | b = z. [para(22(a,1),3(a,1))]. given #40 (T,wt=17): 47 c * a0 * x != y | d * z != y | b0 * x = z. [para(26(a,1),2(a,1))]. given #41 (A,wt=35): 15 x * y * z * x * y * z * x * y * z = x * x * x * y * z * y * z * y * z. [para(1(a,1),4(a,1,2,2,2)),rewrite(1(7),1(12),1(13))]. given #42 (F,wt=0): 71 c * c0 * c * c0 * c * c0 * x * x * x * y * c * c0 * c * c0 * c * c0 * x * x * x * y * c * c0 * c * c0 * c * c0 * x * x * x * y != d * d0 * x * c * c0 * x * c * c0 * x * c * c0 * c * c0 * c * c0 * x * x * x * c * c0 * c * c0 * c * c0 * x * x * x * y * y * y. [ur(3,b,4,a(flip),c,34,a),rewrite(1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(46),1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(47),1(46),1(45),1(44),1(43),1(42),1(41),1(40),1(90),1(89),1(88),1(87),1(86),1(85),1(84),1(83),1(92),1(91),1(90),1(89),1(88),1(87),1(86),1(85),1(94),1(93),1(92),1(91),1(90),1(89),1(88),1(87)),flip(a)]. given #43 (F,wt=0): 72 c * c0 * c * c0 * c * c0 * x * x * x * y * d * d0 * x * c * c0 * x * c * c0 * x * y * d * d0 * x * c * c0 * x * c * c0 * x * y != d * d0 * x * c * c0 * x * c * c0 * x * d * d0 * x * c * c0 * x * c * c0 * x * d * d0 * x * c * c0 * x * c * c0 * x * y * y * y. [ur(3,a,4,a,c,34,a),rewrite(1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(47),1(46),1(45),1(44),1(43),1(42),1(41),1(40),1(92),1(91),1(90),1(89),1(88),1(87),1(86),1(85),1(93),1(92),1(91),1(90),1(89),1(88),1(87),1(86),1(94),1(93),1(92),1(91),1(90),1(89),1(88),1(87))]. given #44 (T,wt=17): 48 c * a0 * x != y | z * b0 * x != y | d = z. [para(26(a,1),3(a,1))]. given #45 (T,wt=17): 60 x * a * a0 != y | x * b * z != y | b0 = z. [para(5(a,1),9(a,1,2))]. given #46 (A,wt=29): 16 x * x * x * y * y * y != z | x * u != z | y * x * y * x * y = u. [para(4(a,1),2(a,1))]. given #47 (F,wt=0): 73 c * c0 * c * c0 * c * c0 * x * x * x * d * d0 * x * c * c0 * x * c * c0 * x * d * d0 * x * c * c0 * x * c * c0 * x * y * y * y != d * d0 * x * c * c0 * x * c * c0 * x * y * d * d0 * x * c * c0 * x * c * c0 * x * y * d * d0 * x * c * c0 * x * c * c0 * x * y. [ur(3,a,4,a(flip),c,34,a),rewrite(1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(46),1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(47),1(46),1(45),1(44),1(43),1(42),1(41),1(40),1(90),1(89),1(88),1(87),1(86),1(85),1(84),1(83),1(92),1(91),1(90),1(89),1(88),1(87),1(86),1(85),1(94),1(93),1(92),1(91),1(90),1(89),1(88),1(87))]. given #48 (F,wt=0): 74 x * d * d0 * y * c * c0 * y * c * c0 * y != x * c * c0 * c * c0 * c * c0 * y * y * y. [ur(2,b,1,a(flip),c,34,a),rewrite(1(30))]. given #49 (T,wt=17): 61 x * c * a0 != y | x * d * z != y | b0 = z. [para(6(a,1),9(a,1,2))]. given #50 (T,wt=17): 62 x * a * c0 != y | x * b * z != y | d0 = z. [para(7(a,1),9(a,1,2))]. given #51 (A,wt=29): 17 x * y * x * y * x * y != z | x * u != z | x * x * y * y * y = u. [para(4(a,2),2(a,1))]. given #52 (F,wt=0): 77 c * c0 * d * d0 * c * c0 != c * c * c * c0 * c0 * c0. [ur(9,b,4,a,c,35,a)]. given #53 (F,wt=0): 78 x * y * z * d * d0 * u != x * y * z * c * c0 * u. [ur(9,b,1,a,c,35,a),rewrite(1(7))]. given #54 (T,wt=17): 90 a * c0 * x != y | b * z != y | d0 * x = z. [para(30(a,1),2(a,1))]. given #55 (T,wt=17): 91 a * c0 * x != y | z * d0 * x != y | b = z. [para(30(a,1),3(a,1))]. given #56 (A,wt=29): 18 x * x * x * y * y * y != z | u * y * x * y * x * y != z | x = u. [para(4(a,1),3(a,1))]. given #57 (F,wt=0): 79 c * c * d * d0 * c0 * c0 != c * c0 * c * c0 * c * c0. [ur(9,b,4,a(flip),c,35,a)]. given #58 (F,wt=0): 80 x * y * d * d0 * z != x * y * c * c0 * z. [ur(9,b,1,a(flip),c,35,a),rewrite(1(12))]. given #59 (T,wt=17): 100 a * a0 != x | a * a0 * y != x | b0 * y = b0. [para(22(a,1),23(b,1)),flip(c)]. given #60 (T,wt=17): 101 a * a0 != x | a * c0 * y != x | d0 * y = b0. [para(30(a,1),23(b,1)),flip(c)]. given #61 (A,wt=29): 19 x * y * x * y * x * y != z | u * x * x * y * y * y != z | x = u. [para(4(a,2),3(a,1))]. given #62 (F,wt=0): 81 d * d * d * d0 * d0 * d0 != d * d0 * c * c0 * d * d0. [ur(9,a,4,a,c,35,a),flip(a)]. given #63 (F,wt=0): 82 d * d0 * d * d0 * d * d0 != d * d * c * c0 * d0 * d0. [ur(9,a,4,a(flip),c,35,a),flip(a)]. given #64 (T,wt=17): 116 x * a * a0 != y | z * b0 != y | x * b = z. [para(5(a,1),10(a,1,2))]. given #65 (T,wt=17): 117 x * y * b0 != z | a * a0 != z | x * y = b. [para(5(a,1),10(b,1))]. given #66 (A,wt=29): 20 x * y * z * y * z * y != u | z * z * z * y * y * y != u | x = z. [para(4(a,1),3(b,1))]. given #67 (F,wt=0): 83 c * c0 * x * c * c0 * x * c * c0 * x * y * y * y != d * d0 * x * y * c * c0 * x * y * c * c0 * x * y. [ur(3,b,4,a,c,35,a),rewrite(1(13),1(12),1(15),1(14),1(17),1(16),1(32),1(31),1(33),1(32),1(34),1(33)),flip(a)]. given #68 (F,wt=0): 84 c * c0 * x * y * c * c0 * x * y * c * c0 * x * y != d * d0 * x * c * c0 * x * c * c0 * x * y * y * y. [ur(3,b,4,a(flip),c,35,a),rewrite(1(15),1(14),1(16),1(15),1(17),1(16),1(30),1(29),1(32),1(31),1(34),1(33)),flip(a)]. given #69 (T,wt=17): 118 x * c * a0 != y | z * b0 != y | x * d = z. [para(6(a,1),10(a,1,2))]. given #70 (T,wt=17): 119 x * y * b0 != z | c * a0 != z | x * y = d. [para(6(a,1),10(b,1))]. given #71 (A,wt=29): 21 x * y * y * z * z * z != u | y * z * y * z * y * z != u | x = y. [para(4(a,2),3(b,1))]. given #72 (F,wt=0): 85 c * c0 * x * y * d * d0 * x * y * d * d0 * x * y != d * d0 * x * d * d0 * x * d * d0 * x * y * y * y. [ur(3,a,4,a,c,35,a),rewrite(1(13),1(12),1(15),1(14),1(17),1(16),1(32),1(31),1(33),1(32),1(34),1(33))]. given #73 (F,wt=0): 86 c * c0 * x * d * d0 * x * d * d0 * x * y * y * y != d * d0 * x * y * d * d0 * x * y * d * d0 * x * y. [ur(3,a,4,a(flip),c,35,a),rewrite(1(15),1(14),1(16),1(15),1(17),1(16),1(30),1(29),1(32),1(31),1(34),1(33))]. given #74 (T,wt=17): 120 x * a * c0 != y | z * d0 != y | x * b = z. [para(7(a,1),10(a,1,2))]. given #75 (T,wt=17): 121 x * y * d0 != z | a * c0 != z | x * y = b. [para(7(a,1),10(b,1))]. given #76 (A,wt=23): 25 b * b * a * a0 * b0 * b0 = a * a0 * a * a0 * a * a0. [para(5(a,1),4(a,1,2,2,2,2)),rewrite(22(9),22(11),22(20)),flip(a)]. given #77 (F,wt=0): 87 c0 * d * d0 * c * c0 * c != c0 * c0 * c0 * c * c * c. [ur(2,b,4,a,c,35,a)]. given #78 (F,wt=0): 88 x * d * d0 * y != x * c * c0 * y. [ur(2,b,1,a(flip),c,35,a),rewrite(1(10))]. given #79 (T,wt=17): 157 c * a0 != x | c * a0 * y != x | b0 * y = b0. [para(26(a,1),27(b,1)),flip(c)]. given #80 (T,wt=17): 272 a * c0 != x | a * a0 * y != x | b0 * y = d0. [para(22(a,1),31(b,1)),flip(c)]. given #81 (A,wt=23): 33 b * b * a * c0 * d0 * d0 = a * c0 * a * c0 * a * c0. [para(7(a,1),4(a,1,2,2,2,2)),rewrite(30(9),30(11),30(20)),flip(a)]. given #82 (F,wt=0): 89 d0 * d0 * d0 * d * d * d != d0 * c * c0 * d * d0 * d. [ur(2,a,4,a,c,35,a),flip(a)]. given #83 (F,wt=0): 102 c * c0 * x * d * d0 * x * d * d0 * x != d * d * d * d0 * x * d0 * x * d0 * x. [ur(10,a,4,a,c,35,a),rewrite(1(12),1(14),1(13),1(24),1(25))]. given #84 (T,wt=17): 273 a * c0 != x | a * c0 * y != x | d0 * y = d0. [para(30(a,1),31(b,1)),flip(c)]. given #85 (T,wt=17): 718 a * a0 * x != y | c * a0 * x != y | d = b. [para(26(a,1),42(b,1)),flip(c)]. given #86 (A,wt=35): 43 b * b * a * a0 * x * b0 * x * b0 * x = a * a0 * x * a * a0 * x * a * a0 * x. [para(22(a,1),4(a,1,2,2,2,2)),rewrite(1(11),22(12),1(13),22(14),1(24),1(25),22(26)),flip(a)]. given #87 (F,wt=0): 103 c * c0 * c * c0 * c * c0 * x * x * x * d * d0 * x * c * c0 * x * c * c0 * x * d * d0 * x * c * c0 * x * c * c0 * x != d * d * d * d0 * x * c * c0 * x * c * c0 * x * d0 * x * c * c0 * x * c * c0 * x * d0 * x * c * c0 * x * c * c0 * x. [ur(10,a,4,a,c,34,a),rewrite(1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(84),1(83),1(82),1(81),1(80),1(79),1(78),1(85),1(84),1(83),1(82),1(81),1(80),1(79))]. given #88 (F,wt=0): 104 d * d * d * d0 * d0 * d0 != c * c0 * d * d0 * d * d0. [ur(10,a,4,a,c,8,a),rewrite(1(11)),flip(a)]. given #89 (T,wt=17): 941 x * a * a0 != y | x * a * c0 != y | d0 = b0. [para(7(a,1),60(b,1,2)),flip(c)]. given #90 (T,wt=17): 1385 x * a * a0 != y | a * a0 != y | x * b = b. [para(5(a,1),116(b,1))]. given #91 (A,wt=27): 45 a * a0 * b0 * b0 * x * x * x = a * a0 * x * b0 * x * b0 * x. [para(4(a,1),22(a,1,2)),rewrite(22(10))]. given #92 (F,wt=0): 105 d * d0 * x * c * c0 * x * c * c0 * x != c * c * c * c0 * x * c0 * x * c0 * x. [ur(10,a,4,a,c,35,a(flip)),rewrite(1(12),1(14),1(13),1(24),1(25))]. given #93 (F,wt=0): 106 d * d0 * x * c * c0 * x * c * c0 * x * c * c0 * c * c0 * c * c0 * x * x * x * c * c0 * c * c0 * c * c0 * x * x * x != c * c * c * c0 * c * c0 * c * c0 * x * x * x * c0 * c * c0 * c * c0 * x * x * x * c0 * c * c0 * c * c0 * x * x * x. [ur(10,a,4,a,c,34,a(flip)),rewrite(1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(84),1(83),1(82),1(81),1(80),1(79),1(78),1(85),1(84),1(83),1(82),1(81),1(80),1(79))]. given #94 (T,wt=17): 1386 x * a * a0 != y | c * a0 != y | x * b = d. [para(6(a,1),116(b,1))]. given #95 (T,wt=17): 1388 x * c * a0 != y | a * a0 != y | x * d = b. [para(6(a,1),117(a,1,2))]. given #96 (A,wt=27): 46 a * a0 * a0 * a0 * x * x * x = a * a0 * x * a0 * x * a0 * x. [para(4(a,1),22(a,2,2)),rewrite(22(10)),flip(a)]. given #97 (F,wt=0): 107 d * d0 * c * c0 * c * c0 != c * c * c * c0 * c0 * c0. [ur(10,a,4,a,c,8,a(flip)),rewrite(1(11))]. given #98 (F,wt=0): 128 c * c0 * x * c * c0 * x * c * c0 * x * y * d * d0 * c * c0 * c * c0 * x * x * x * y * d * d0 * c * c0 * c * c0 * x * x * x * y != d * d0 * c * c0 * c * c0 * x * x * x * d * d0 * c * c0 * c * c0 * x * x * x * d * d0 * c * c0 * c * c0 * x * x * x * y * y * y. [ur(10,b,4,a,c,36,a),rewrite(1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(35),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(46),1(45),1(44),1(43),1(42),1(41),1(40),1(92),1(91),1(90),1(89),1(88),1(87),1(86),1(85),1(93),1(92),1(91),1(90),1(89),1(88),1(87),1(86),1(94),1(93),1(92),1(91),1(90),1(89),1(88),1(87))]. given #99 (T,wt=17): 1472 x * c * a0 != y | c * a0 != y | x * d = d. [para(6(a,1),118(b,1))]. given #100 (T,wt=17): 1557 x * a * c0 != y | a * c0 != y | x * b = b. [para(7(a,1),120(b,1))]. given #101 (A,wt=35): 49 c * a0 * x * c * a0 * x * c * a0 * x = d * d * c * a0 * x * b0 * x * b0 * x. [para(26(a,1),4(a,1,2,2,2,2)),rewrite(1(11),26(12),1(13),26(14),1(24),1(25),26(26))]. given #102 (F,wt=0): 129 c * c0 * x * c * c0 * x * c * c0 * x * y != d * d0 * c * c0 * c * c0 * x * x * x * y. [ur(10,b,1,a,c,36,a),rewrite(1(14),1(13),1(12),1(11),1(10),1(9),1(8),1(29),1(28),1(27),1(26),1(25),1(24),1(23))]. given #103 (F,wt=0): 130 c * c0 * x * c * c0 * x * c * c0 * x * d * d0 * c * c0 * c * c0 * x * x * x * d * d0 * c * c0 * c * c0 * x * x * x * y * y * y != d * d0 * c * c0 * c * c0 * x * x * x * y * d * d0 * c * c0 * c * c0 * x * x * x * y * d * d0 * c * c0 * c * c0 * x * x * x * y. [ur(10,b,4,a(flip),c,36,a),rewrite(1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(46),1(45),1(44),1(43),1(42),1(41),1(40),1(90),1(89),1(88),1(87),1(86),1(85),1(84),1(83),1(92),1(91),1(90),1(89),1(88),1(87),1(86),1(85),1(94),1(93),1(92),1(91),1(90),1(89),1(88),1(87))]. given #104 (T,wt=19): 206 b0 * a * a0 * a * a0 = b * a * a0 * b0 * b0. [para(5(a,1),11(a,1,2,2,2)),rewrite(22(8),22(17))]. given #105 (T,wt=19): 207 d * c * a0 * b0 * b0 = b0 * c * a0 * c * a0. [para(6(a,1),11(a,1,2,2,2)),rewrite(26(8),26(17)),flip(a)]. given #106 (A,wt=27): 51 c * a0 * b0 * b0 * x * x * x = c * a0 * x * b0 * x * b0 * x. [para(4(a,1),26(a,1,2)),rewrite(26(10))]. given #107 (F,wt=0): 131 c * c * c * c0 * x * c * c0 * x * c * c0 * x * c0 * x * c * c0 * x * c * c0 * x * c0 * x * c * c0 * x * c * c0 * x != d * d0 * c * c0 * c * c0 * x * x * x * c * c0 * x * c * c0 * x * c * c0 * x * c * c0 * x * c * c0 * x * c * c0 * x. [ur(10,a,4,a,c,36,a),rewrite(1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(84),1(83),1(82),1(81),1(80),1(79),1(78),1(85),1(84),1(83),1(82),1(81),1(80),1(79)),flip(a)]. given #108 (F,wt=0): 135 x * y * z * c * c0 * u * c * c0 * u * c * c0 * u != x * y * z * d * d0 * c * c0 * c * c0 * u * u * u. [ur(9,b,1,a,c,36,a),rewrite(1(17))]. given #109 (T,wt=19): 208 d0 * a * c0 * a * c0 = b * a * c0 * d0 * d0. [para(7(a,1),11(a,1,2,2,2)),rewrite(30(8),30(17))]. given #110 (T,wt=19): 210 b0 * b0 * b * b * b = a * a0 * a * a0 * b. [para(11(a,1),22(a,1)),rewrite(22(16))]. given #111 (A,wt=27): 52 c * a0 * a0 * a0 * x * x * x = c * a0 * x * a0 * x * a0 * x. [para(4(a,1),26(a,2,2)),rewrite(26(10)),flip(a)]. given #112 (F,wt=0): 136 x * y * c * c0 * z * c * c0 * z * c * c0 * z != x * y * d * d0 * c * c0 * c * c0 * z * z * z. [ur(9,b,1,a(flip),c,36,a),rewrite(1(32))]. given #113 (F,wt=0): 137 c * c0 * x * c * c0 * x * c * c0 * x * c * c0 * x * c * c0 * x * c * c0 * x * c * c0 * x * c * c0 * x * c * c0 * x * y * y * y != d * d0 * c * c0 * c * c0 * x * x * x * y * c * c0 * x * c * c0 * x * c * c0 * x * y * c * c0 * x * c * c0 * x * c * c0 * x * y. [ur(3,a,4,a,c,36,a),rewrite(1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(47),1(46),1(45),1(44),1(43),1(42),1(41),1(40),1(92),1(91),1(90),1(89),1(88),1(87),1(86),1(85),1(93),1(92),1(91),1(90),1(89),1(88),1(87),1(86),1(94),1(93),1(92),1(91),1(90),1(89),1(88),1(87)),flip(a)]. given #114 (T,wt=19): 216 b0 * b0 * d * d * d = c * a0 * c * a0 * d. [para(11(a,1),26(a,1)),rewrite(26(16))]. given #115 (T,wt=19): 225 d0 * d0 * b * b * b = a * c0 * a * c0 * b. [para(11(a,1),30(a,1)),rewrite(30(16))]. given #116 (A,wt=21): 55 x * y * z * u != v | x * y * z * w != v | u = w. [para(1(a,1),9(a,1,2)),rewrite(1(6))]. given #117 (F,wt=0): 138 c * c0 * x * c * c0 * x * c * c0 * x * y * c * c0 * x * c * c0 * x * c * c0 * x * y * c * c0 * x * c * c0 * x * c * c0 * x * y != d * d0 * c * c0 * c * c0 * x * x * x * c * c0 * x * c * c0 * x * c * c0 * x * c * c0 * x * c * c0 * x * c * c0 * x * y * y * y. [ur(3,a,4,a(flip),c,36,a),rewrite(1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(46),1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(47),1(46),1(45),1(44),1(43),1(42),1(41),1(40),1(90),1(89),1(88),1(87),1(86),1(85),1(84),1(83),1(92),1(91),1(90),1(89),1(88),1(87),1(86),1(85),1(94),1(93),1(92),1(91),1(90),1(89),1(88),1(87)),flip(a)]. given #118 (F,wt=0): 139 x * c * c0 * y * c * c0 * y * c * c0 * y != x * d * d0 * c * c0 * c * c0 * y * y * y. [ur(2,b,1,a(flip),c,36,a),rewrite(1(30))]. given #119 (T,wt=19): 227 c0 * c0 * a * a * a = a * c0 * a * c0 * a. [para(11(a,1),30(a,2)),rewrite(30(9)),flip(a)]. given #120 (T,wt=19): 1057 c * c * a0 * a0 * a0 = a0 * c * a0 * c * a0. [hyper(17,a,26,a(flip),b,26,a(flip))]. given #121 (A,wt=33): 56 x * y * y * y * z * z * z != u | x * y * v != u | z * y * z * y * z = v. [para(4(a,1),9(a,1,2))]. given #122 (F,wt=0): 140 c * c0 * x * c * c0 * x * c * c0 * x * d * d0 * c * c0 * c * c0 * x * x * x * d * d0 * c * c0 * c * c0 * x * x * x != d * d * d * d0 * c * c0 * c * c0 * x * x * x * d0 * c * c0 * c * c0 * x * x * x * d0 * c * c0 * c * c0 * x * x * x. [ur(10,a,4,a,c,36,a(flip)),rewrite(1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(84),1(83),1(82),1(81),1(80),1(79),1(78),1(85),1(84),1(83),1(82),1(81),1(80),1(79))]. given #123 (F,wt=0): 141 c * c0 * x * d * d0 * x * d * d0 * x * y * d * d0 * d * d0 * d * d0 * x * x * x * y * d * d0 * d * d0 * d * d0 * x * x * x * y != d * d0 * d * d0 * d * d0 * x * x * x * d * d0 * d * d0 * d * d0 * x * x * x * d * d0 * d * d0 * d * d0 * x * x * x * y * y * y. [ur(10,b,4,a,c,37,a),rewrite(1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(35),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(46),1(45),1(44),1(43),1(42),1(41),1(40),1(92),1(91),1(90),1(89),1(88),1(87),1(86),1(85),1(93),1(92),1(91),1(90),1(89),1(88),1(87),1(86),1(94),1(93),1(92),1(91),1(90),1(89),1(88),1(87))]. given #124 (T,wt=19): 1833 b0 * b0 * x * x * x = x * b0 * x * b0 * x. [hyper(9,a,xx,b,45,a),flip(a)]. given #125 (T,wt=19): 1930 a0 * a0 * x * x * x = x * a0 * x * a0 * x. [hyper(9,a,xx,b,46,a),flip(a)]. given #126 (A,wt=33): 58 x * y * z * y * z * y * z != u | x * y * v != u | y * y * z * z * z = v. [para(4(a,2),9(a,1,2))]. given #127 (F,wt=0): 142 c * c0 * x * d * d0 * x * d * d0 * x * y != d * d0 * d * d0 * d * d0 * x * x * x * y. [ur(10,b,1,a,c,37,a),rewrite(1(14),1(13),1(12),1(11),1(10),1(9),1(8),1(29),1(28),1(27),1(26),1(25),1(24),1(23))]. given #128 (F,wt=0): 143 c * c0 * x * d * d0 * x * d * d0 * x * d * d0 * d * d0 * d * d0 * x * x * x * d * d0 * d * d0 * d * d0 * x * x * x * y * y * y != d * d0 * d * d0 * d * d0 * x * x * x * y * d * d0 * d * d0 * d * d0 * x * x * x * y * d * d0 * d * d0 * d * d0 * x * x * x * y. [ur(10,b,4,a(flip),c,37,a),rewrite(1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(46),1(45),1(44),1(43),1(42),1(41),1(40),1(90),1(89),1(88),1(87),1(86),1(85),1(84),1(83),1(92),1(91),1(90),1(89),1(88),1(87),1(86),1(85),1(94),1(93),1(92),1(91),1(90),1(89),1(88),1(87))]. given #129 (T,wt=19): 2708 d0 * d0 * x * x * x = x * d0 * x * d0 * x. [hyper(56,a,30,a,b,30,a),flip(a)]. given #130 (T,wt=19): 2709 c0 * c0 * x * x * x = x * c0 * x * c0 * x. [hyper(56,a,30,a(flip),b,30,a(flip)),flip(a)]. given #131 (A,wt=21): 63 x * a * a0 * y != z | x * b * u != z | b0 * y = u. [para(22(a,1),9(a,1,2))]. given #132 (F,wt=0): 144 c * c * c * c0 * x * d * d0 * x * d * d0 * x * c0 * x * d * d0 * x * d * d0 * x * c0 * x * d * d0 * x * d * d0 * x != d * d0 * d * d0 * d * d0 * x * x * x * c * c0 * x * d * d0 * x * d * d0 * x * c * c0 * x * d * d0 * x * d * d0 * x. [ur(10,a,4,a,c,37,a),rewrite(1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(84),1(83),1(82),1(81),1(80),1(79),1(78),1(85),1(84),1(83),1(82),1(81),1(80),1(79)),flip(a)]. given #133 (F,wt=0): 148 x * y * z * c * c0 * u * d * d0 * u * d * d0 * u != x * y * z * d * d0 * d * d0 * d * d0 * u * u * u. [ur(9,b,1,a,c,37,a),rewrite(1(17))]. given #134 (T,wt=21): 64 x * c * a0 * y != z | x * d * u != z | b0 * y = u. [para(26(a,1),9(a,1,2))]. given #135 (T,wt=21): 96 x * a * c0 * y != z | x * b * u != z | d0 * y = u. [para(30(a,1),9(a,1,2))]. given #136 (A,wt=35): 92 b * b * a * c0 * x * d0 * x * d0 * x = a * c0 * x * a * c0 * x * a * c0 * x. [para(30(a,1),4(a,1,2,2,2,2)),rewrite(1(11),30(12),1(13),30(14),1(24),1(25),30(26)),flip(a)]. given #137 (F,wt=0): 149 x * y * c * c0 * z * d * d0 * z * d * d0 * z != x * y * d * d0 * d * d0 * d * d0 * z * z * z. [ur(9,b,1,a(flip),c,37,a),rewrite(1(32))]. given #138 (F,wt=0): 150 c * c0 * x * d * d0 * x * d * d0 * x * c * c0 * x * d * d0 * x * d * d0 * x * c * c0 * x * d * d0 * x * d * d0 * x * y * y * y != d * d0 * d * d0 * d * d0 * x * x * x * y * c * c0 * x * d * d0 * x * d * d0 * x * y * c * c0 * x * d * d0 * x * d * d0 * x * y. [ur(3,a,4,a,c,37,a),rewrite(1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(47),1(46),1(45),1(44),1(43),1(42),1(41),1(40),1(92),1(91),1(90),1(89),1(88),1(87),1(86),1(85),1(93),1(92),1(91),1(90),1(89),1(88),1(87),1(86),1(94),1(93),1(92),1(91),1(90),1(89),1(88),1(87)),flip(a)]. given #139 (T,wt=21): 108 x * y * z * u != v | w * u != v | x * y * z = w. [para(1(a,1),10(a,1,2))]. given #140 (T,wt=21): 109 x * y * z != u | v * w * z != u | x * y = v * w. [para(1(a,1),10(b,1))]. given #141 (A,wt=27): 94 a * c0 * d0 * d0 * x * x * x = a * c0 * x * d0 * x * d0 * x. [para(4(a,1),30(a,1,2)),rewrite(30(10))]. given #142 (F,wt=0): 151 c * c0 * x * d * d0 * x * d * d0 * x * y * c * c0 * x * d * d0 * x * d * d0 * x * y * c * c0 * x * d * d0 * x * d * d0 * x * y != d * d0 * d * d0 * d * d0 * x * x * x * c * c0 * x * d * d0 * x * d * d0 * x * c * c0 * x * d * d0 * x * d * d0 * x * y * y * y. [ur(3,a,4,a(flip),c,37,a),rewrite(1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(46),1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(47),1(46),1(45),1(44),1(43),1(42),1(41),1(40),1(90),1(89),1(88),1(87),1(86),1(85),1(84),1(83),1(92),1(91),1(90),1(89),1(88),1(87),1(86),1(85),1(94),1(93),1(92),1(91),1(90),1(89),1(88),1(87)),flip(a)]. given #143 (F,wt=0): 152 x * c * c0 * y * d * d0 * y * d * d0 * y != x * d * d0 * d * d0 * d * d0 * y * y * y. [ur(2,b,1,a(flip),c,37,a),rewrite(1(30))]. given #144 (T,wt=21): 122 x * a * a0 * y != z | u * b0 * y != z | x * b = u. [para(22(a,1),10(a,1,2))]. given #145 (T,wt=21): 123 x * y * b0 * z != u | a * a0 * z != u | x * y = b. [para(22(a,1),10(b,1))]. given #146 (A,wt=27): 95 a * c0 * c0 * c0 * x * x * x = a * c0 * x * c0 * x * c0 * x. [para(4(a,1),30(a,2,2)),rewrite(30(10)),flip(a)]. given #147 (F,wt=0): 153 c * c0 * x * d * d0 * x * d * d0 * x * d * d0 * d * d0 * d * d0 * x * x * x * d * d0 * d * d0 * d * d0 * x * x * x != d * d * d * d0 * d * d0 * d * d0 * x * x * x * d0 * d * d0 * d * d0 * x * x * x * d0 * d * d0 * d * d0 * x * x * x. [ur(10,a,4,a,c,37,a(flip)),rewrite(1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(84),1(83),1(82),1(81),1(80),1(79),1(78),1(85),1(84),1(83),1(82),1(81),1(80),1(79))]. given #148 (F,wt=0): 160 c * c0 * x * d * d0 * x * d * d0 * x * y * d * d0 * d * d0 * d * d0 * x * x * x * y * d * d0 * d * d0 * d * d0 * x * x * x != y * y * d * d0 * d * d0 * d * d0 * x * x * x * d * d0 * d * d0 * d * d0 * x * x * x * d * d0 * d * d0 * d * d0 * x * x * x. [ur(10,b,11,a,c,37,a),rewrite(1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(89),1(88),1(87),1(86),1(85),1(84),1(83),1(82),1(90),1(89),1(88),1(87),1(86),1(85),1(84),1(83))]. given #149 (T,wt=21): 124 x * c * a0 * y != z | u * b0 * y != z | x * d = u. [para(26(a,1),10(a,1,2))]. given #150 (T,wt=21): 125 x * y * b0 * z != u | c * a0 * z != u | x * y = d. [para(26(a,1),10(b,1))]. given #151 (A,wt=29): 97 a * a0 != x | b * b * b * y * y * y != x | y * b * y * b * y = b0. [para(4(a,1),23(b,1)),flip(c)]. given #152 (F,wt=0): 161 c * c0 * x * c * c0 * x * c * c0 * x * y * d * d0 * c * c0 * c * c0 * x * x * x * y * d * d0 * c * c0 * c * c0 * x * x * x != y * y * d * d0 * c * c0 * c * c0 * x * x * x * d * d0 * c * c0 * c * c0 * x * x * x * d * d0 * c * c0 * c * c0 * x * x * x. [ur(10,b,11,a,c,36,a),rewrite(1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(89),1(88),1(87),1(86),1(85),1(84),1(83),1(82),1(90),1(89),1(88),1(87),1(86),1(85),1(84),1(83))]. given #153 (F,wt=0): 162 d * d0 * x * y * c * c0 * x * y * c * c0 * x != y * y * c * c0 * x * c * c0 * x * c * c0 * x. [ur(10,b,11,a,c,35,a),rewrite(1(13),1(12),1(15),1(29),1(28),1(30),1(29))]. given #154 (T,wt=21): 126 x * a * c0 * y != z | u * d0 * y != z | x * b = u. [para(30(a,1),10(a,1,2))]. given #155 (T,wt=21): 127 x * y * d0 * z != u | a * c0 * z != u | x * y = b. [para(30(a,1),10(b,1))]. given #156 (A,wt=29): 98 a * a0 != x | b * y * b * y * b * y != x | b * b * y * y * y = b0. [para(4(a,2),23(b,1)),flip(c)]. given #157 (F,wt=0): 163 d * d0 * x * c * c0 * x * c * c0 * x * y * c * c0 * c * c0 * c * c0 * x * x * x * y * c * c0 * c * c0 * c * c0 * x * x * x != y * y * c * c0 * c * c0 * c * c0 * x * x * x * c * c0 * c * c0 * c * c0 * x * x * x * c * c0 * c * c0 * c * c0 * x * x * x. [ur(10,b,11,a,c,34,a),rewrite(1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(89),1(88),1(87),1(86),1(85),1(84),1(83),1(82),1(90),1(89),1(88),1(87),1(86),1(85),1(84),1(83))]. given #158 (F,wt=0): 164 d * d0 * x * c * c0 * x * c * c0 != x * x * c * c0 * c * c0 * c * c0. [ur(10,b,11,a,c,8,a),rewrite(1(10),1(23),1(24))]. given #159 (T,wt=21): 566 a * a0 * x != y | a * a0 * z != y | b0 * x = b0 * z. [para(22(a,1),41(b,1))]. given #160 (T,wt=21): 567 a * a0 * x != y | a * c0 * z != y | d0 * z = b0 * x. [para(30(a,1),41(b,1)),flip(c)]. given #161 (A,wt=33): 110 x * y * y * y * z * z * z != u | v * z * y * z * y * z != u | x * y = v. [para(4(a,1),10(a,1,2))]. given #162 (F,wt=0): 165 d * d0 * d * d0 * d * d0 * x * x * x * y * c * c0 * x * d * d0 * x * d * d0 * x * y * c * c0 * x * d * d0 * x * d * d0 * x != y * y * c * c0 * x * d * d0 * x * d * d0 * x * c * c0 * x * d * d0 * x * d * d0 * x * c * c0 * x * d * d0 * x * d * d0 * x. [ur(10,b,11,a,c,37,a(flip)),rewrite(1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(89),1(88),1(87),1(86),1(85),1(84),1(83),1(82),1(90),1(89),1(88),1(87),1(86),1(85),1(84),1(83))]. given #163 (F,wt=0): 166 d * d0 * c * c0 * c * c0 * x * x * x * y * c * c0 * x * c * c0 * x * c * c0 * x * y * c * c0 * x * c * c0 * x * c * c0 * x != y * y * c * c0 * x * c * c0 * x * c * c0 * x * c * c0 * x * c * c0 * x * c * c0 * x * c * c0 * x * c * c0 * x * c * c0 * x. [ur(10,b,11,a,c,36,a(flip)),rewrite(1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(89),1(88),1(87),1(86),1(85),1(84),1(83),1(82),1(90),1(89),1(88),1(87),1(86),1(85),1(84),1(83))]. given #164 (T,wt=21): 736 c * a0 * x != y | c * a0 * z != y | b0 * x = b0 * z. [para(26(a,1),47(b,1))]. given #165 (T,wt=21): 940 x * y * a * a0 != z | x * y * b * u != z | b0 = u. [para(1(a,1),60(a,1)),rewrite(1(10))]. given #166 (A,wt=33): 112 x * y * z * y * z * y * z != u | v * y * y * z * z * z != u | x * y = v. [para(4(a,2),10(a,1,2))]. given #167 (F,wt=0): 167 c * c0 * x * y * d * d0 * x * y * d * d0 * x != y * y * d * d0 * x * d * d0 * x * d * d0 * x. [ur(10,b,11,a,c,35,a(flip)),rewrite(1(13),1(12),1(15),1(29),1(28),1(30),1(29))]. given #168 (F,wt=0): 168 c * c0 * c * c0 * c * c0 * x * x * x * y * d * d0 * x * c * c0 * x * c * c0 * x * y * d * d0 * x * c * c0 * x * c * c0 * x != y * y * d * d0 * x * c * c0 * x * c * c0 * x * d * d0 * x * c * c0 * x * c * c0 * x * d * d0 * x * c * c0 * x * c * c0 * x. [ur(10,b,11,a,c,34,a(flip)),rewrite(1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(89),1(88),1(87),1(86),1(85),1(84),1(83),1(82),1(90),1(89),1(88),1(87),1(86),1(85),1(84),1(83))]. given #169 (T,wt=21): 942 x * a * a0 != y | x * a * a0 * z != y | b0 * z = b0. [para(22(a,1),60(b,1,2)),flip(c)]. given #170 (T,wt=21): 943 x * a * a0 != y | x * a * c0 * z != y | d0 * z = b0. [para(30(a,1),60(b,1,2)),flip(c)]. given #171 (A,wt=33): 114 x * y * z * u * z * u * z != v | u * u * u * z * z * z != v | x * y = u. [para(4(a,1),10(b,1))]. given #172 (F,wt=0): 169 c * c0 * x * d * d0 * x * d * d0 != x * x * d * d0 * d * d0 * d * d0. [ur(10,b,11,a,c,8,a(flip)),rewrite(1(10),1(23),1(24))]. given #173 (F,wt=0): 170 c0 * x * d * d0 * x * d * d0 * x * c0 * x * d * d0 * x * d * d0 * x * c * c * c != d * d0 * d * d0 * d * d0 * x * x * x * c * c0 * x * d * d0 * x * d * d0 * x * c. [ur(10,a,11,a,c,37,a),rewrite(1(29),1(28),1(27),1(26),1(25),1(24),1(23),1(31),1(30),1(29),1(28),1(27),1(26),1(25),1(24),1(61),1(60),1(59),1(58),1(57),1(56),1(55),1(62),1(61),1(60),1(59),1(58),1(57),1(56)),flip(a)]. given #174 (T,wt=21): 1036 x * y * c * a0 != z | x * y * d * u != z | b0 = u. [para(1(a,1),61(a,1)),rewrite(1(10))]. given #175 (T,wt=21): 1037 x * c * a0 != y | x * c * a0 * z != y | b0 * z = b0. [para(26(a,1),61(b,1,2)),flip(c)]. given #176 (A,wt=33): 115 x * y * z * z * u * u * u != v | z * u * z * u * z * u != v | x * y = z. [para(4(a,2),10(b,1))]. given #177 (F,wt=0): 171 c0 * x * c * c0 * x * c * c0 * x * c0 * x * c * c0 * x * c * c0 * x * c * c * c != d * d0 * c * c0 * c * c0 * x * x * x * c * c0 * x * c * c0 * x * c * c0 * x * c. [ur(10,a,11,a,c,36,a),rewrite(1(29),1(28),1(27),1(26),1(25),1(24),1(23),1(31),1(30),1(29),1(28),1(27),1(26),1(25),1(24),1(61),1(60),1(59),1(58),1(57),1(56),1(55),1(62),1(61),1(60),1(59),1(58),1(57),1(56)),flip(a)]. given #178 (F,wt=0): 172 d0 * x * d0 * x * d * d * d != c * c0 * x * d * d0 * x * d. [ur(10,a,11,a,c,35,a),rewrite(1(9),1(11),1(10),1(21),1(22)),flip(a)]. given #179 (T,wt=21): 1046 x * y * a * c0 != z | x * y * b * u != z | d0 = u. [para(1(a,1),62(a,1)),rewrite(1(10))]. given #180 (T,wt=21): 1047 x * a * c0 != y | x * a * a0 * z != y | b0 * z = d0. [para(22(a,1),62(b,1,2)),flip(c)]. given #181 (A,wt=29): 155 c * a0 != x | d * d * d * y * y * y != x | y * d * y * d * y = b0. [para(4(a,1),27(b,1)),flip(c)]. given #182 (F,wt=0): 173 d0 * x * c * c0 * x * c * c0 * x * d0 * x * c * c0 * x * c * c0 * x * d * d * d != c * c0 * c * c0 * c * c0 * x * x * x * d * d0 * x * c * c0 * x * c * c0 * x * d. [ur(10,a,11,a,c,34,a),rewrite(1(29),1(28),1(27),1(26),1(25),1(24),1(23),1(31),1(30),1(29),1(28),1(27),1(26),1(25),1(24),1(61),1(60),1(59),1(58),1(57),1(56),1(55),1(62),1(61),1(60),1(59),1(58),1(57),1(56)),flip(a)]. given #183 (F,wt=0): 174 d0 * d0 * d * d * d != c * c0 * d * d0 * d. [ur(10,a,11,a,c,8,a),rewrite(1(9)),flip(a)]. given #184 (T,wt=21): 1048 x * a * c0 != y | x * a * c0 * z != y | d0 * z = d0. [para(30(a,1),62(b,1,2)),flip(c)]. given #185 (T,wt=21): 1182 a * c0 * x != y | a * c0 * z != y | d0 * x = d0 * z. [para(30(a,1),90(b,1))]. given #186 (A,wt=29): 156 c * a0 != x | d * y * d * y * d * y != x | d * d * y * y * y = b0. [para(4(a,2),27(b,1)),flip(c)]. given #187 (F,wt=0): 175 d0 * d * d0 * d * d0 * x * x * x * d0 * d * d0 * d * d0 * x * x * x * d * d * d != c * c0 * x * d * d0 * x * d * d0 * x * d * d0 * d * d0 * d * d0 * x * x * x * d. [ur(10,a,11,a,c,37,a(flip)),rewrite(1(29),1(28),1(27),1(26),1(25),1(24),1(23),1(31),1(30),1(29),1(28),1(27),1(26),1(25),1(24),1(61),1(60),1(59),1(58),1(57),1(56),1(55),1(62),1(61),1(60),1(59),1(58),1(57),1(56)),flip(a)]. given #188 (F,wt=0): 176 d0 * c * c0 * c * c0 * x * x * x * d0 * c * c0 * c * c0 * x * x * x * d * d * d != c * c0 * x * c * c0 * x * c * c0 * x * d * d0 * c * c0 * c * c0 * x * x * x * d. [ur(10,a,11,a,c,36,a(flip)),rewrite(1(29),1(28),1(27),1(26),1(25),1(24),1(23),1(31),1(30),1(29),1(28),1(27),1(26),1(25),1(24),1(61),1(60),1(59),1(58),1(57),1(56),1(55),1(62),1(61),1(60),1(59),1(58),1(57),1(56)),flip(a)]. given #189 (T,wt=21): 1383 x * y * a * a0 != z | u * b0 != z | x * y * b = u. [para(1(a,1),116(a,1)),rewrite(1(12))]. given #190 (T,wt=21): 1384 x * a * a0 != y | z * u * b0 != y | x * b = z * u. [para(1(a,1),116(b,1))]. given #191 (A,wt=23): 158 x * y * x * y * y * y = y * x * y * y * x * y. [hyper(2,a,1,a(flip),b,11,a),rewrite(1(4),1(8),1(10))]. given #192 (F,wt=0): 177 c0 * x * c0 * x * c * c * c != d * d0 * x * c * c0 * x * c. [ur(10,a,11,a,c,35,a(flip)),rewrite(1(9),1(11),1(10),1(21),1(22)),flip(a)]. given #193 (F,wt=0): 178 c0 * c * c0 * c * c0 * x * x * x * c0 * c * c0 * c * c0 * x * x * x * c * c * c != d * d0 * x * c * c0 * x * c * c0 * x * c * c0 * c * c0 * c * c0 * x * x * x * c. [ur(10,a,11,a,c,34,a(flip)),rewrite(1(29),1(28),1(27),1(26),1(25),1(24),1(23),1(31),1(30),1(29),1(28),1(27),1(26),1(25),1(24),1(61),1(60),1(59),1(58),1(57),1(56),1(55),1(62),1(61),1(60),1(59),1(58),1(57),1(56)),flip(a)]. given #194 (T,wt=21): 1387 x * y * z * b0 != u | a * a0 != u | x * y * z = b. [para(1(a,1),117(a,1,2))]. given #195 (T,wt=21): 1470 x * y * c * a0 != z | u * b0 != z | x * y * d = u. [para(1(a,1),118(a,1)),rewrite(1(12))]. given #196 (A,wt=27): 159 x * y * y * x * y * y * x = y * y * x * y * x * y * x. [hyper(2,a,1,a(flip),b,11,a(flip)),rewrite(1(4),1(10),1(11))]. given #197 (F,wt=0): 179 d * d0 * c * c0 * c != c0 * c0 * c * c * c. [ur(10,a,11,a,c,8,a(flip)),rewrite(1(9))]. given #198 (F,wt=0): 180 c * c0 * d * d0 * c != c0 * c0 * c * c * c. [ur(9,b,11,a,c,35,a)]. given #199 (T,wt=21): 1471 x * c * a0 != y | z * u * b0 != y | x * d = z * u. [para(1(a,1),118(b,1))]. given #200 (T,wt=21): 1473 x * y * z * b0 != u | c * a0 != u | x * y * z = d. [para(1(a,1),119(a,1,2))]. given #201 (A,wt=0): 181 d0 * d0 * d * d * d != d * d0 * c * c0 * d. [ur(9,b,11,a,c,35,a(flip)),flip(a)]. given #202 (F,wt=0): 182 c0 * d * d0 * c * c0 != c * c * c0 * c0 * c0. [ur(2,b,11,a,c,35,a)]. given #203 (F,wt=0): 183 d * d * d0 * d0 * d0 != d0 * c * c0 * d * d0. [ur(2,b,11,a,c,35,a(flip)),flip(a)]. given #204 (T,wt=21): 1555 x * y * a * c0 != z | u * d0 != z | x * y * b = u. [para(1(a,1),120(a,1)),rewrite(1(12))]. given #205 (T,wt=21): 1556 x * a * c0 != y | z * u * d0 != y | x * b = z * u. [para(1(a,1),120(b,1))]. given #206 (A,wt=0): 184 c * c0 * x * d * d0 * x * d * d0 * x * d * d0 * d * d0 * d * d0 * x * x * x * y * y * y != y * d * d0 * d * d0 * d * d0 * x * x * x * y * d * d0 * d * d0 * d * d0 * x * x * x * y. [ur(10,b,11,a(flip),c,37,a),rewrite(1(30),1(29),1(28),1(27),1(26),1(25),1(24),1(23),1(31),1(30),1(29),1(28),1(27),1(26),1(25),1(61),1(60),1(59),1(58),1(57),1(56),1(55),1(54),1(63),1(62),1(61),1(60),1(59),1(58),1(57),1(56))]. given #207 (F,wt=0): 185 c * c0 * x * c * c0 * x * c * c0 * x * d * d0 * c * c0 * c * c0 * x * x * x * y * y * y != y * d * d0 * c * c0 * c * c0 * x * x * x * y * d * d0 * c * c0 * c * c0 * x * x * x * y. [ur(10,b,11,a(flip),c,36,a),rewrite(1(30),1(29),1(28),1(27),1(26),1(25),1(24),1(23),1(31),1(30),1(29),1(28),1(27),1(26),1(25),1(61),1(60),1(59),1(58),1(57),1(56),1(55),1(54),1(63),1(62),1(61),1(60),1(59),1(58),1(57),1(56))]. given #208 (F,wt=0): 186 d * d0 * x * c * c0 * x * y * y * y != y * c * c0 * x * y * c * c0 * x * y. [ur(10,b,11,a(flip),c,35,a),rewrite(1(10),1(9),1(11),1(21),1(20),1(23),1(22))]. given #209 (T,wt=21): 1558 x * y * z * d0 != u | a * c0 != u | x * y * z = b. [para(1(a,1),121(a,1,2))]. given #210 (T,wt=21): 1831 x * y * a * a0 != z | x * y * a * c0 != z | d0 = b0. [para(1(a,1),941(a,1)),rewrite(1(11))]. given #211 (A,wt=0): 187 d * d0 * x * c * c0 * x * c * c0 * x * c * c0 * c * c0 * c * c0 * x * x * x * y * y * y != y * c * c0 * c * c0 * c * c0 * x * x * x * y * c * c0 * c * c0 * c * c0 * x * x * x * y. [ur(10,b,11,a(flip),c,34,a),rewrite(1(30),1(29),1(28),1(27),1(26),1(25),1(24),1(23),1(31),1(30),1(29),1(28),1(27),1(26),1(25),1(61),1(60),1(59),1(58),1(57),1(56),1(55),1(54),1(63),1(62),1(61),1(60),1(59),1(58),1(57),1(56))]. given #212 (F,wt=0): 188 d * d0 * c * c0 * x * x * x != x * c * c0 * x * c * c0 * x. [ur(10,b,11,a(flip),c,8,a),rewrite(1(8),1(17),1(19))]. given #213 (F,wt=0): 189 d * d0 * d * d0 * d * d0 * x * x * x * c * c0 * x * d * d0 * x * d * d0 * x * y * y * y != y * c * c0 * x * d * d0 * x * d * d0 * x * y * c * c0 * x * d * d0 * x * d * d0 * x * y. [ur(10,b,11,a(flip),c,37,a(flip)),rewrite(1(30),1(29),1(28),1(27),1(26),1(25),1(24),1(23),1(31),1(30),1(29),1(28),1(27),1(26),1(25),1(61),1(60),1(59),1(58),1(57),1(56),1(55),1(54),1(63),1(62),1(61),1(60),1(59),1(58),1(57),1(56))]. given #214 (T,wt=21): 1832 x * y * a * a0 != z | a * a0 != z | x * y * b = b. [para(1(a,1),1385(a,1)),rewrite(1(13))]. given #215 (T,wt=21): 1928 x * y * a * a0 != z | c * a0 != z | x * y * b = d. [para(1(a,1),1386(a,1)),rewrite(1(13))]. given #216 (A,wt=0): 190 d * d0 * c * c0 * c * c0 * x * x * x * c * c0 * x * c * c0 * x * c * c0 * x * y * y * y != y * c * c0 * x * c * c0 * x * c * c0 * x * y * c * c0 * x * c * c0 * x * c * c0 * x * y. [ur(10,b,11,a(flip),c,36,a(flip)),rewrite(1(30),1(29),1(28),1(27),1(26),1(25),1(24),1(23),1(31),1(30),1(29),1(28),1(27),1(26),1(25),1(61),1(60),1(59),1(58),1(57),1(56),1(55),1(54),1(63),1(62),1(61),1(60),1(59),1(58),1(57),1(56))]. given #217 (F,wt=0): 191 c * c0 * x * d * d0 * x * y * y * y != y * d * d0 * x * y * d * d0 * x * y. [ur(10,b,11,a(flip),c,35,a(flip)),rewrite(1(10),1(9),1(11),1(21),1(20),1(23),1(22))]. given #218 (F,wt=0): 192 c * c0 * c * c0 * c * c0 * x * x * x * d * d0 * x * c * c0 * x * c * c0 * x * y * y * y != y * d * d0 * x * c * c0 * x * c * c0 * x * y * d * d0 * x * c * c0 * x * c * c0 * x * y. [ur(10,b,11,a(flip),c,34,a(flip)),rewrite(1(30),1(29),1(28),1(27),1(26),1(25),1(24),1(23),1(31),1(30),1(29),1(28),1(27),1(26),1(25),1(61),1(60),1(59),1(58),1(57),1(56),1(55),1(54),1(63),1(62),1(61),1(60),1(59),1(58),1(57),1(56))]. given #219 (T,wt=21): 1929 x * y * c * a0 != z | a * a0 != z | x * y * d = b. [para(1(a,1),1388(a,1)),rewrite(1(13))]. given #220 (T,wt=21): 2009 x * y * c * a0 != z | c * a0 != z | x * y * d = d. [para(1(a,1),1472(a,1)),rewrite(1(13))]. given #221 (A,wt=0): 193 c * c0 * d * d0 * x * x * x != x * d * d0 * x * d * d0 * x. [ur(10,b,11,a(flip),c,8,a(flip)),rewrite(1(8),1(17),1(19))]. given #222 (F,wt=0): 194 c * d * d0 * c0 * c0 != c0 * c * c0 * c * c0. [ur(2,b,11,a(flip),c,35,a)]. given #223 (F,wt=0): 195 d0 * d * d0 * d * d0 != d * c * c0 * d0 * d0. [ur(2,b,11,a(flip),c,35,a(flip)),flip(a)]. given #224 (T,wt=21): 2010 x * y * a * c0 != z | a * c0 != z | x * y * b = b. [para(1(a,1),1557(a,1)),rewrite(1(13))]. given #225 (T,wt=21): 4654 x * a * a0 * y != z | a * a0 * y != z | x * b = b. [para(22(a,1),122(b,1))]. given #226 (A,wt=23): 196 x * y * x * y * x * z = y * y * x * x * x * z. [para(11(a,1),1(a,1,1)),rewrite(1(5),1(4),1(3),1(2),1(9),1(8),1(7)),flip(a)]. given #227 (F,wt=0): 240 c * c0 * d * d0 * d * d0 * x * x * x * y * d * d0 * x * d * d0 * x * d * d0 * x * y * d * d0 * x * d * d0 * x * d * d0 * x != y * y * d * d0 * x * d * d0 * x * d * d0 * x * d * d0 * x * d * d0 * x * d * d0 * x * d * d0 * x * d * d0 * x * d * d0 * x. [ur(10,b,11,a,c,38,a),rewrite(1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(89),1(88),1(87),1(86),1(85),1(84),1(83),1(82),1(90),1(89),1(88),1(87),1(86),1(85),1(84),1(83))]. given #228 (F,wt=0): 241 c * c0 * d * d0 * d * d0 * x * x * x * y != d * d0 * x * d * d0 * x * d * d0 * x * y. [ur(10,b,1,a,c,38,a),rewrite(1(14),1(13),1(12),1(11),1(10),1(9),1(8),1(29),1(28),1(27),1(26),1(25),1(24),1(23))]. given #229 (T,wt=21): 4655 x * a * a0 * y != z | c * a0 * y != z | x * b = d. [para(26(a,1),122(b,1))]. given #230 (T,wt=21): 4670 x * c * a0 * y != z | a * a0 * y != z | x * d = b. [para(26(a,1),123(a,1,2))]. given #231 (A,wt=31): 197 x * y * z * x * y * z * x * y = z * z * x * y * x * y * x * y. [para(11(a,1),1(a,1)),rewrite(1(4),1(5),1(11)),flip(a)]. given #232 (F,wt=0): 242 c * c0 * d * d0 * d * d0 * x * x * x * d * d0 * x * d * d0 * x * d * d0 * x * y * y * y != y * d * d0 * x * d * d0 * x * d * d0 * x * y * d * d0 * x * d * d0 * x * d * d0 * x * y. [ur(10,b,11,a(flip),c,38,a),rewrite(1(30),1(29),1(28),1(27),1(26),1(25),1(24),1(23),1(31),1(30),1(29),1(28),1(27),1(26),1(25),1(61),1(60),1(59),1(58),1(57),1(56),1(55),1(54),1(63),1(62),1(61),1(60),1(59),1(58),1(57),1(56))]. given #233 (F,wt=0): 243 c0 * d * d0 * d * d0 * x * x * x * c0 * d * d0 * d * d0 * x * x * x * c * c * c != d * d0 * x * d * d0 * x * d * d0 * x * c * c0 * d * d0 * d * d0 * x * x * x * c. [ur(10,a,11,a,c,38,a),rewrite(1(29),1(28),1(27),1(26),1(25),1(24),1(23),1(31),1(30),1(29),1(28),1(27),1(26),1(25),1(24),1(61),1(60),1(59),1(58),1(57),1(56),1(55),1(62),1(61),1(60),1(59),1(58),1(57),1(56)),flip(a)]. given #234 (T,wt=21): 4865 x * c * a0 * y != z | c * a0 * y != z | x * d = d. [para(26(a,1),124(b,1))]. given #235 (T,wt=21): 5074 x * a * c0 * y != z | a * c0 * y != z | x * b = b. [para(30(a,1),126(b,1))]. given #236 (A,wt=27): 198 x * y * z * x * y * z * x = y * z * y * z * x * x * x. [para(11(a,2),1(a,1)),rewrite(1(3),1(5),1(10))]. Demod_limit: c * c0 * d * d0 * d * d0 * v200 * v200 * v200 * v201 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * v201 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * v201 * v201 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * v201 * v201 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * v201 * v201 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * v201 * v201 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * v201 * v201 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * v201 * v201 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * v201 * v201 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * v201 * v201 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 != v201 * v201 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * v201 * v201 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * v201 * v201 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * v201 * v201 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * v201 * v201 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * v201 * v201 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * v201 * v201 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * v201 * v201 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * v201 * v201 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200 * d * d0 * v200. [ur(115,b,198,a(flip),c,240,a),rewrite(1(230),1(229),1(228),1(227),1(226),1(225),1(224),1(223),1(222),1(221),1(220),1(219),1(218),1(217),1(216),1(215),1(214),1(213),1(212),1(211),1(210),1(209),1(208),1(207),1(206),1(205),1(204),1(203),1(323),1(322),1(321),1(320),1(319),1(318),1(317),1(316),1(315),1(314),1(313),1(312),1(311),1(310),1(309),1(308),1(307),1(306),1(305),1(304),1(303),1(302),1(301),1(300),1(299),1(298),1(297),1(296),1(416),1(415),1(414),1(413),1(412),1(411),1(410),1(409),1(408),1(407),1(406),1(405),1(404),1(403),1(402),1(401),1(400),1(399),1(398),1(397),1(396),1(395),1(394),1(393),1(392),1(391),1(390),1(389),1(417),1(416),1(415),1(414),1(413),1(412),1(411),1(410),1(409),1(408),1(407),1(406),1(405),1(404),1(403),1(402),1(401),1(400),1(399),1(398),1(397),1(396),1(395),1(394),1(393),1(392),1(391),1(390),1(389),1(388),1(387),1(386),1(385),1(384),1(383),1(382),1(381),1(380),1(379),1(378),1(377),1(376),1(375),1(374),1(373),1(372),1(371),1(370),1(369),1(368),1(367),1(366),1(365),1(364),1(363),1(362),1(361),1(418),1(417),1(416),1(415),1(414),1(413),1(412),1(411),1(410),1(409),1(408),1(407),1(406),1(405),1(404),1(403),1(402),1(401),1(400),1(399),1(398),1(397),1(396),1(395),1(394),1(393),1(392),1(391),1(390),1(389),1(388),1(387),1(386),1(385),1(384),1(383),1(382),1(381),1(380),1(379),1(378),1(377),1(376),1(375),1(374),1(373),1(372),1(371),1(370),1(369),1(368),1(367),1(366),1(365),1(364),1(363),1(362),1(419),1(418),1(417),1(416),1(415),1(414),1(413),1(412),1(411),1(410),1(409),1(408),1(407),1(406),1(405),1(404),1(403),1(402),1(401),1(400),1(399),1(398),1(397),1(396),1(395),1(394),1(393),1(392),1(420),1(419),1(418),1(417),1(416),1(415),1(414),1(413),1(412),1(411),1(410),1(409),1(408),1(407),1(406),1(405),1(404),1(403),1(402),1(401),1(400),1(399),1(398),1(397),1(396),1(395),1(394),1(393),1(421),1(420),1(419),1(418),1(417),1(416),1(415),1(414),1(413),1(412),1(411),1(410),1(409),1(408),1(407),1(406),1(405),1(404),1(403),1(402),1(401),1(400),1(399),1(398),1(397),1(396),1(395),1(607),1(606),1(605),1(604),1(603),1(602),1(601),1(600),1(599),1(598),1(597),1(596),1(595),1(594),1(593),1(592),1(591),1(590),1(589),1(588),1(587),1(586),1(585),1(584),1(583),1(582),1(581),1(580),1(792),1(791),1(790),1(789),1(788),1(787),1(786),1(785),1(784),1(783),1(782),1(781),1(780),1(779),1(778),1(777),1(776),1(775),1(774),1(773),1(772),1(771),1(770),1(769),1(768),1(767),1(766),1(765),1(839),1(838),1(837),1(836),1(835),1(834),1(833),1(832),1(831),1(830),1(829),1(828),1(827),1(826),1(825),1(824),1(823),1(822),1(821),1(820),1(819),1(818),1(817),1(816),1(815),1(814),1(813),1(812),1(811),1(810),1(809),1(808),1(807),1(806),1(805),1(804),1(803),1(802),1(801),1(800),1(799),1(798),1(797),1(796),1(795),1(794),1(793),1(792),1(791),1(790),1(789),1(788),1(787),1(786),1(785),1(784),1(783),1(840),1(839),1(838),1(837),1(836),1(835),1(834),1(833),1(832),1(831),1(830),1(829),1(828),1(827),1(826),1(825),1(824),1(823),1(822),1(821),1(820),1(819),1(818),1(817),1(816),1(815),1(814),1(813),1(841),1(840),1(839),1(838),1(837),1(836),1(835),1(834),1(833),1(832),1(831),1(830),1(829),1(828),1(827),1(826),1(825),1(824),1(823),1(822),1(821),1(820),1(819),1(818),1(817),1(816),1(815),1(814),1(842),1(841),1(840),1(839),1(838),1(837),1(836),1(835),1(834),1(833),1(832),1(831),1(830),1(829),1(828),1(827),1(826),1(825),1(824),1(823),1(822),1(821),1(820),1(819),1(818),1(817),1(816),1(815),1(814),1(813),1(812),1(811),1(810),1(809),1(808),1(807),1(806),1(805),1(804),1(803),1(802),1(801),1(800),1(799),1(798),1(797),1(796),1(795),1(794),1(793),1(792),1(791),1(790),1(789),1(788),1(787),1(786),1(843),1(842),1(841),1(840),1(839),1(838),1(837),1(836),1(835),1(834),1(833),1(832),1(831),1(830),1(829),1(828),1(827),1(826),1(825),1(824),1(823),1(822),1(821),1(820),1(819),1(818),1(817),1(816),1(844),1(843),1(842),1(841),1(840),1(839),1(838),1(837),1(836),1(835),1(834),1(833),1(832),1(831),1(830),1(829),1(828),1(827),1(826),1(825),1(824),1(823),1(822),1(821),1(820),1(819),1(818),1(817))]. Demod_limit (steps=-1, size=1043). The most recent kept clause is 6267. From here on, a short message will be printed for each 100 times the limit is hit. Demod_limit hit 100 times. given #237 (F,wt=0): 247 x * y * z * c * c0 * d * d0 * d * d0 * u * u * u != x * y * z * d * d0 * u * d * d0 * u * d * d0 * u. [ur(9,b,1,a,c,38,a),rewrite(1(17))]. given #238 (F,wt=0): 248 x * y * c * c0 * d * d0 * d * d0 * z * z * z != x * y * d * d0 * z * d * d0 * z * d * d0 * z. [ur(9,b,1,a(flip),c,38,a),rewrite(1(32))]. given #239 (T,wt=21): 5630 x * a * a0 != y | z * a * a0 != y | x * b = z * b. [para(5(a,1),1384(b,1,2))]. given #240 (T,wt=21): 5631 x * a * a0 != y | z * c * a0 != y | z * d = x * b. [para(6(a,1),1384(b,1,2)),flip(c)]. given #241 (A,wt=23): 199 x * y * z * y * z * y = x * z * z * y * y * y. [para(11(a,1),1(a,2,2)),rewrite(1(5))]. given #242 (F,wt=0): 249 d * d0 * x * d * d0 * x * d * d0 * x * y * c * c0 * d * d0 * d * d0 * x * x * x * y * c * c0 * d * d0 * d * d0 * x * x * x != y * y * c * c0 * d * d0 * d * d0 * x * x * x * c * c0 * d * d0 * d * d0 * x * x * x * c * c0 * d * d0 * d * d0 * x * x * x. [ur(3,a,11,a,c,38,a),rewrite(1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(46),1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(89),1(88),1(87),1(86),1(85),1(84),1(83),1(82),1(90),1(89),1(88),1(87),1(86),1(85),1(84),1(83))]. given #243 (F,wt=0): 250 d * d0 * x * d * d0 * x * d * d0 * x * c * c0 * d * d0 * d * d0 * x * x * x * y * y * y != y * c * c0 * d * d0 * d * d0 * x * x * x * y * c * c0 * d * d0 * d * d0 * x * x * x * y. [ur(3,a,11,a(flip),c,38,a),rewrite(1(31),1(30),1(29),1(28),1(27),1(26),1(25),1(24),1(32),1(31),1(30),1(29),1(28),1(27),1(26),1(25),1(61),1(60),1(59),1(58),1(57),1(56),1(55),1(54),1(63),1(62),1(61),1(60),1(59),1(58),1(57),1(56))]. given #244 (T,wt=19): 6295 d0 * a0 * c0 * a0 * c0 = b0 * a0 * c0 * c0 * c0. [hyper(567,a,xx,b,199,a)]. given #245 (T,wt=19): 6296 d0 * c0 * a0 * a0 * a0 = b0 * c0 * a0 * c0 * a0. [hyper(567,a,199,a,b,xx)]. given #246 (A,wt=25): 200 x * x * y * y * y != z | y * u != z | x * y * x * y = u. [para(11(a,1),2(a,1))]. given #247 (F,wt=0): 251 x * c * c0 * d * d0 * d * d0 * y * y * y != x * d * d0 * y * d * d0 * y * d * d0 * y. [ur(2,b,1,a(flip),c,38,a),rewrite(1(30))]. given #248 (F,wt=0): 252 d0 * x * d * d0 * x * d * d0 * x * d0 * x * d * d0 * x * d * d0 * x * d * d * d != c * c0 * d * d0 * d * d0 * x * x * x * d * d0 * x * d * d0 * x * d * d0 * x * d. [ur(10,a,11,a,c,38,a(flip)),rewrite(1(29),1(28),1(27),1(26),1(25),1(24),1(23),1(31),1(30),1(29),1(28),1(27),1(26),1(25),1(24),1(61),1(60),1(59),1(58),1(57),1(56),1(55),1(62),1(61),1(60),1(59),1(58),1(57),1(56)),flip(a)]. given #249 (T,wt=21): 5632 x * a * a0 != y | a * a0 * b0 != y | a * a0 = x * b. [para(22(a,1),1384(b,1)),rewrite(5(16)),flip(c)]. given #250 (T,wt=21): 5633 x * a * a0 != y | c * a0 * b0 != y | c * a0 = x * b. [para(26(a,1),1384(b,1)),rewrite(6(16)),flip(c)]. given #251 (A,wt=25): 201 x * y * x * y * x != z | y * u != z | y * x * x * x = u. [para(11(a,2),2(a,1))]. given #252 (F,wt=0): 253 x * y * d * d0 * z * x * y * c * c0 * z * x * y * c * c0 != z * z * x * y * c * c0 * x * y * c * c0 * x * y * c * c0. [ur(10,b,11,a,c,39,a),rewrite(1(16),1(15),1(14),1(18),1(17),1(35),1(34),1(33),1(36),1(35),1(34))]. given #253 (F,wt=0): 254 x * y * d * d0 * x * y * c * c0 * z * z * z != z * x * y * c * c0 * z * x * y * c * c0 * z. [ur(10,b,11,a(flip),c,39,a),rewrite(1(12),1(11),1(10),1(13),1(12),1(25),1(24),1(23),1(27),1(26),1(25))]. given #254 (T,wt=21): 5634 x * a * a0 != y | a * c0 * b0 != y | a * c0 = x * b. [para(30(a,1),1384(b,1)),rewrite(7(16)),flip(c)]. given #255 (T,wt=21): 5936 x * c * a0 != y | z * c * a0 != y | x * d = z * d. [para(6(a,1),1471(b,1,2))]. given #256 (A,wt=25): 202 x * x * y * y * y != z | u * x * y * x * y != z | y = u. [para(11(a,1),3(a,1))]. given #257 (F,wt=0): 255 x * d * d0 * x * d * d0 * y * y * y != y * x * c * c0 * y * x * d * d0 * y. [ur(10,a,11,a,c,39,a),rewrite(1(10),1(9),1(12),1(11),1(10),1(23),1(22),1(24),1(23)),flip(a)]. given #258 (F,wt=0): 256 x * d * d0 * x * c * c0 * y * y * y != y * x * d * d0 * y * x * d * d0 * y. [ur(10,a,11,a(flip),c,39,a),rewrite(1(9),1(8),1(12),1(11),1(10),1(9),1(8),1(21),1(20),1(23),1(22))]. given #259 (T,wt=21): 5937 x * c * a0 != y | a * a0 * b0 != y | a * a0 = x * d. [para(22(a,1),1471(b,1)),rewrite(5(16)),flip(c)]. given #260 (T,wt=21): 5938 x * c * a0 != y | c * a0 * b0 != y | c * a0 = x * d. [para(26(a,1),1471(b,1)),rewrite(6(16)),flip(c)]. given #261 (A,wt=25): 203 x * y * x * y * x != z | u * y * x * x * x != z | y = u. [para(11(a,2),3(a,1))]. given #262 (F,wt=0): 260 c * c0 * x * c * c0 * x * d * d0 != x * x * c * c0 * c * c0 * c * c0. [ur(9,b,11,a,c,39,a),rewrite(1(11),1(13),1(23),1(24))]. given #263 (F,wt=0): 261 x * y * z * u * v * d * d0 != x * y * z * u * v * c * c0. [ur(9,b,1,a,c,39,a),rewrite(1(8))]. given #264 (T,wt=21): 5939 x * c * a0 != y | a * c0 * b0 != y | a * c0 = x * d. [para(30(a,1),1471(b,1)),rewrite(7(16)),flip(c)]. given #265 (T,wt=21): 5944 x * a * c0 != y | z * a * c0 != y | x * b = z * b. [para(7(a,1),1556(b,1,2))]. given #266 (A,wt=25): 204 x * y * z * y * z != u | y * y * z * z * z != u | x = z. [para(11(a,1),3(b,1))]. given #267 (F,wt=0): 262 c * c0 * x * c * c0 * x * c * c0 != x * x * c * c0 * c * c0 * d * d0. [ur(9,b,11,a(flip),c,39,a),rewrite(1(10),1(11),1(24),1(26)),flip(a)]. given #268 (F,wt=0): 263 x * y * z * u * d * d0 != x * y * z * u * c * c0. [ur(9,b,1,a(flip),c,39,a),rewrite(1(14))]. given #269 (T,wt=21): 5945 x * a * c0 != y | a * a0 * d0 != y | a * a0 = x * b. [para(22(a,1),1556(b,1)),rewrite(5(16)),flip(c)]. given #270 (T,wt=21): 5946 x * a * c0 != y | c * a0 * d0 != y | c * a0 = x * b. [para(26(a,1),1556(b,1)),rewrite(6(16)),flip(c)]. given #271 (A,wt=25): 205 x * y * z * z * z != u | z * y * z * y * z != u | x = y. [para(11(a,2),3(b,1))]. given #272 (F,wt=0): 264 d * d0 * x * d * d0 * x * c * c0 != x * x * d * d0 * d * d0 * d * d0. [ur(9,a,11,a,c,39,a),rewrite(1(11),1(13),1(23),1(24))]. given #273 (F,wt=0): 265 d * d0 * x * d * d0 * x * d * d0 != x * x * d * d0 * d * d0 * c * c0. [ur(9,a,11,a(flip),c,39,a),rewrite(1(10),1(11),1(24),1(26)),flip(a)]. given #274 (T,wt=21): 5947 x * a * c0 != y | a * c0 * d0 != y | a * c0 = x * b. [para(30(a,1),1556(b,1)),rewrite(7(16)),flip(c)]. given #275 (T,wt=23): 209 a * a0 * x * b0 * x * b0 = b * x * x * b0 * b0 * b0. [para(11(a,1),22(a,1,2)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 46.77 (+ 0.08) seconds. % Length of proof is 21. % Level of proof is 6. % Maximum clause weight is 33. % Given clauses 275. 1 (x * y) * z = x * y * z # label(associativity). [assumption]. 2 x * y != z | x * u != z | y = u # label(left_cancellation_extended). [assumption]. 3 x * y != z | u * y != z | x = u # label(right_cancellation_extended). [assumption]. 4 x * y * x * y * x * y = x * x * x * y * y * y # label("(xy)^3 = x^3y^3"). [assumption]. 5 b * b0 = a * a0. [assumption]. 6 d * b0 = c * a0. [assumption]. 7 b * d0 = a * c0. [assumption]. 8 d * d0 != c * c0. [assumption]. 9 x * y * z != u | x * y * v != u | z = v. [para(1(a,1),2(a,1)),rewrite(1(5))]. 11 x * y * x * y * x = y * y * x * x * x. [hyper(2,a,xx,b,4,a),flip(a)]. 22 b * b0 * x = a * a0 * x. [para(5(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. 26 d * b0 * x = c * a0 * x. [para(6(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. 30 b * d0 * x = a * c0 * x. [para(7(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. 35 d * d0 * x != c * c0 * x. [ur(3,b,1,a,c,8,a),rewrite(1(4))]. 56 x * y * y * y * z * z * z != u | x * y * v != u | z * y * z * y * z = v. [para(4(a,1),9(a,1,2))]. 209 a * a0 * x * b0 * x * b0 = b * x * x * b0 * b0 * b0. [para(11(a,1),22(a,1,2)),flip(a)]. 2708 d0 * d0 * x * x * x = x * d0 * x * d0 * x. [hyper(56,a,30,a,b,30,a),flip(a)]. 3222 d * d0 * d0 * b0 * b0 * b0 = c * a0 * d0 * b0 * d0 * b0. [para(2708(a,2),26(a,1,2))]. 6352 a0 * d0 * b0 * d0 * b0 = c0 * d0 * b0 * b0 * b0. [hyper(2,a,30,a(flip),b,209,a),flip(a)]. 6374 d * d0 * d0 * b0 * b0 * b0 = c * c0 * d0 * b0 * b0 * b0. [back_rewrite(3222),rewrite(6352(21))]. 6375 $F. [resolve(6374,a,35,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=275. Generated=115479. Kept=6374. proofs=1. Usable=260. Sos=5621. Demods=114. Limbo=22, Disabled=478. Hints=0. Weight_deleted=6898. Literals_deleted=0. Forward_subsumed=32731. Back_subsumed=439. Sos_limit_deleted=69476. Sos_displaced=0. Sos_removed=0. New_demodulators=151 (0 lex), Back_demodulated=31. Back_unit_deleted=0. Demod_attempts=24370666. Demod_rewrites=5756153. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=78104. Nonunit_bsub_feature_tests=19877. Megabytes=37.33. User_CPU=46.77, System_CPU=0.08, Wall_clock=47. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11392 exit (max_proofs) Sat Aug 12 21:00:58 2006