============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11391 was started by mccune on cleo.thornwood, Sat Aug 12 21:00:08 2006 The command was "/home/mccune/bin/prover9 -f quot-np2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file quot-np2.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 * z * y * x = y * x * z * x * y # label(nilpotent_class2). 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 * z * y * x = y * x * z * x * y # label(nilpotent_class2). [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 * z * y * x = y * x * z * x * y # label(nilpotent_class2). [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=19): 4 x * y * z * y * x = y * x * z * x * y # label(nilpotent_class2). [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): 21 b * b0 * x = a * a0 * x. [para(5(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. given #10 (T,wt=11): 25 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): 33 d * d0 * x * y * x * c * c0 != x * c * c0 * y * c * c0 * x. [ur(3,b,4,a,c,8,a),rewrite(1(10),1(17),1(19))]. given #13 (F,wt=0): 34 d * d0 * x != c * c0 * x. [ur(3,b,1,a,c,8,a),rewrite(1(4))]. given #14 (T,wt=11): 29 b * d0 * x = a * c0 * x. [para(7(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. given #15 (T,wt=13): 22 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): 35 c * c0 * x * y * x * d * d0 != x * d * d0 * y * d * d0 * x. [ur(3,a,4,a,c,8,a),rewrite(1(10),1(17),1(19))]. given #18 (F,wt=0): 36 x * y * d * d0 != x * y * c * c0. [ur(2,b,1,a,c,8,a),rewrite(1(5))]. given #19 (T,wt=13): 23 a * a0 != x | y * b0 != x | b = y. [para(5(a,1),3(a,1))]. given #20 (T,wt=13): 26 c * a0 != x | d * y != x | b0 = y. [para(6(a,1),2(a,1))]. given #21 (A,wt=23): 12 x * y * z * y * x * u = y * x * z * x * y * u. [para(4(a,1),1(a,1,1)),rewrite(1(5),1(4),1(3),1(2),1(9),1(8),1(7))]. given #22 (F,wt=0): 37 x * d * d0 != x * c * c0. [ur(2,b,1,a(flip),c,8,a),rewrite(1(8))]. given #23 (F,wt=0): 50 x * y * z * d * d0 != x * y * z * c * c0. [ur(9,b,1,a,c,8,a),rewrite(1(6))]. given #24 (T,wt=13): 27 c * a0 != x | y * b0 != x | d = y. [para(6(a,1),3(a,1))]. given #25 (T,wt=13): 30 a * c0 != x | b * y != x | d0 = y. [para(7(a,1),2(a,1))]. given #26 (A,wt=27): 13 x * y * z * u * z * x * y = z * x * y * u * x * y * z. [para(4(a,1),1(a,1)),rewrite(1(3),1(5)),flip(a)]. given #27 (F,wt=0): 61 c0 * x * c * c0 * y * c * d * d0 * y * x * y * c * c0 != c * c0 * x * c * c0 * y * y * c0 * x * c * c0 * y * c. [ur(9,b,4,a,c,33,a),rewrite(1(20),1(19),1(18),1(17),1(37),1(36),1(35),1(34),1(39),1(38),1(37),1(36))]. given #28 (F,wt=0): 62 x * y * z * d * d0 * u * v * u * c * c0 != x * y * z * u * c * c0 * v * c * c0 * u. [ur(9,b,1,a,c,33,a),rewrite(1(13))]. given #29 (T,wt=13): 31 a * c0 != x | y * d0 != x | b = y. [para(7(a,1),3(a,1))]. given #30 (T,wt=13): 95 a * a0 != x | a * c0 != x | d0 = b0. [para(7(a,1),22(b,1)),flip(c)]. given #31 (A,wt=23): 14 x * y * z * u * z * y = x * z * y * u * y * z. [para(4(a,1),1(a,2,2)),rewrite(1(5))]. given #32 (F,wt=0): 63 x * y * d * d0 * z * u * z * c * c0 != x * y * z * c * c0 * u * c * c0 * z. [ur(9,b,1,a(flip),c,33,a),rewrite(1(24))]. given #33 (F,wt=0): 64 d0 * x * y * x * c * c0 * d * x * y * x * c * c0 * d0 != x * y * x * c * c0 * d0 * x * c * c0 * y * c * c0 * x. [ur(9,a,4,a,c,33,a),rewrite(1(19),1(18),1(17),1(16),1(35),1(34),1(33),1(32),1(37),1(36),1(35),1(34)),flip(a)]. given #34 (T,wt=13): 157 a * a0 != x | c * a0 != x | d = b. [para(6(a,1),23(b,1)),flip(c)]. given #35 (T,wt=17): 38 a * a0 * x != y | b * z != y | b0 * x = z. [para(21(a,1),2(a,1))]. given #36 (A,wt=23): 15 x * y * z * u * y * x = y * x * z * u * x * y. [para(1(a,1),4(a,1,2,2)),rewrite(1(8))]. given #37 (F,wt=0): 65 d * d0 * x * y * x * c * c0 * z * u * z * x * c * c0 * y * c * c0 * x != z * x * c * c0 * y * c * c0 * x * u * x * c * c0 * y * c * c0 * x * z. [ur(3,b,4,a,c,33,a),rewrite(1(24),1(23),1(22),1(21),1(20),1(19),1(45),1(44),1(43),1(42),1(41),1(40),1(47),1(46),1(45),1(44),1(43),1(42))]. given #38 (F,wt=0): 66 d * d0 * x * y * x * c * c0 * z != x * c * c0 * y * c * c0 * x * z. [ur(3,b,1,a,c,33,a),rewrite(1(11),1(10),1(9),1(8),1(7),1(6),1(21),1(20),1(19),1(18),1(17))]. given #39 (T,wt=17): 39 a * a0 * x != y | z * b0 * x != y | b = z. [para(21(a,1),3(a,1))]. given #40 (T,wt=17): 44 c * a0 * x != y | d * z != y | b0 * x = z. [para(25(a,1),2(a,1))]. given #41 (A,wt=25): 16 x * y * z * y * x != u | y * v != u | x * z * x * y = v. [para(4(a,1),2(a,1))]. given #42 (F,wt=0): 67 x * c * c0 * y * c * c0 * x * z * u * z * d * d0 * x * y * x * c * c0 != z * d * d0 * x * y * x * c * c0 * u * d * d0 * x * y * x * c * c0 * z. [ur(3,a,4,a,c,33,a),rewrite(1(24),1(23),1(22),1(21),1(20),1(19),1(45),1(44),1(43),1(42),1(41),1(40),1(47),1(46),1(45),1(44),1(43),1(42))]. given #43 (F,wt=0): 68 c * a0 * c * c0 * x * c * c0 * b0 != d * d * d0 * b0 * x * b0 * c * c0. [ur(2,b,25,a,c,33,a),flip(a)]. given #44 (T,wt=17): 45 c * a0 * x != y | z * b0 * x != y | d = z. [para(25(a,1),3(a,1))]. given #45 (T,wt=17): 54 x * a * a0 != y | x * b * z != y | b0 = z. [para(5(a,1),9(a,1,2))]. given #46 (A,wt=25): 17 x * y * z * y * x != u | v * x * z * x * y != u | y = v. [para(4(a,1),3(a,1))]. given #47 (F,wt=0): 69 a * a0 * c * c0 * x * c * c0 * b0 != b * d * d0 * b0 * x * b0 * c * c0. [ur(2,b,21,a,c,33,a),flip(a)]. given #48 (F,wt=0): 70 c0 * x * c * c0 * c0 * c * x * c * c0 * c0 * c0 != x * c * c0 * c0 * d * d0 * c0 * x * c0 * c * c0. [ur(2,b,4,a,c,33,a),rewrite(1(19),1(18),1(17),1(35),1(34),1(33),1(37),1(36),1(35)),flip(a)]. given #49 (T,wt=17): 55 x * c * a0 != y | x * d * z != y | b0 = z. [para(6(a,1),9(a,1,2))]. given #50 (T,wt=17): 56 x * a * c0 != y | x * b * z != y | d0 = z. [para(7(a,1),9(a,1,2))]. given #51 (A,wt=25): 18 x * y * z * y * u != v | y * u * z * u * y != v | x = u. [para(4(a,1),3(b,1))]. given #52 (F,wt=0): 73 x * d * d0 * y * z * y * c * c0 != x * y * c * c0 * z * c * c0 * y. [ur(2,b,1,a(flip),c,33,a),rewrite(1(22))]. given #53 (F,wt=0): 74 d * x * d * c * c0 * d0 * x * d * c * c0 * d != x * d * c * c0 * d * c * c0 * x * c * c0 * d. [ur(2,a,4,a,c,33,a),rewrite(1(19),1(18),1(17),1(35),1(34),1(33),1(37),1(36),1(35)),flip(a)]. given #54 (T,wt=17): 87 a * c0 * x != y | b * z != y | d0 * x = z. [para(29(a,1),2(a,1))]. given #55 (T,wt=17): 88 a * c0 * x != y | z * d0 * x != y | b = z. [para(29(a,1),3(a,1))]. given #56 (A,wt=35): 19 x * y * z * y * y * z * x * z * y = y * x * y * z * z * x * y * z * y. [para(4(a,1),4(a,1,2,2)),rewrite(1(8),1(7),1(13),1(12),1(15),1(14))]. given #57 (F,wt=0): 77 c0 * x * c * x * c0 != x * c0 * d * d0 * x. [ur(9,b,4,a,c,34,a),flip(a)]. given #58 (F,wt=0): 78 x * y * z * d * d0 * u != x * y * z * c * c0 * u. [ur(9,b,1,a,c,34,a),rewrite(1(7))]. given #59 (T,wt=17): 96 a * a0 != x | a * a0 * y != x | b0 * y = b0. [para(21(a,1),22(b,1)),flip(c)]. given #60 (T,wt=17): 97 a * a0 != x | a * c0 * y != x | d0 * y = b0. [para(29(a,1),22(b,1)),flip(c)]. given #61 (A,wt=27): 20 x * y * x * y * y * y * x = y * x * y * x * x * y * y. [para(4(a,1),4(a,1,2)),rewrite(1(6),1(9),1(11))]. given #62 (F,wt=0): 79 x * y * d * d0 * z != x * y * c * c0 * z. [ur(9,b,1,a(flip),c,34,a),rewrite(1(12))]. given #63 (F,wt=0): 80 d0 * x * d * x * d0 != x * d0 * c * c0 * x. [ur(9,a,4,a,c,34,a),flip(a)]. given #64 (T,wt=17): 110 x * a * a0 != y | z * b0 != y | x * b = z. [para(5(a,1),10(a,1,2))]. given #65 (T,wt=17): 111 x * y * b0 != z | a * a0 != z | x * y = b. [para(5(a,1),10(b,1))]. given #66 (A,wt=19): 24 a * a0 * x * b0 * b = b0 * b * x * a * a0. [para(5(a,1),4(a,1,2,2,2)),rewrite(21(16)),flip(a)]. given #67 (F,wt=0): 81 d * d0 * x * y * z * y * c * c0 * x != y * c * c0 * x * z * c * c0 * x * y. [ur(3,b,4,a,c,34,a),rewrite(1(12),1(11),1(21),1(20),1(23),1(22))]. given #68 (F,wt=0): 82 c * c0 * x * y * z * y * d * d0 * x != y * d * d0 * x * z * d * d0 * x * y. [ur(3,a,4,a,c,34,a),rewrite(1(12),1(11),1(21),1(20),1(23),1(22))]. given #69 (T,wt=17): 112 x * c * a0 != y | z * b0 != y | x * d = z. [para(6(a,1),10(a,1,2))]. given #70 (T,wt=17): 113 x * y * b0 != z | c * a0 != z | x * y = d. [para(6(a,1),10(b,1))]. given #71 (A,wt=19): 28 b0 * d * x * c * a0 = c * a0 * x * b0 * d. [para(6(a,1),4(a,1,2,2,2)),rewrite(25(16))]. given #72 (F,wt=0): 83 c * x * c0 * x * c != x * d * d0 * c * x. [ur(2,b,4,a,c,34,a),flip(a)]. given #73 (F,wt=0): 84 x * d * d0 * y != x * c * c0 * y. [ur(2,b,1,a(flip),c,34,a),rewrite(1(10))]. given #74 (T,wt=17): 114 x * a * c0 != y | z * d0 != y | x * b = z. [para(7(a,1),10(a,1,2))]. given #75 (T,wt=17): 115 x * y * d0 != z | a * c0 != z | x * y = b. [para(7(a,1),10(b,1))]. given #76 (A,wt=19): 32 d0 * b * x * a * c0 = a * c0 * x * d0 * b. [para(7(a,1),4(a,1,2,2,2)),rewrite(29(16))]. given #77 (F,wt=0): 85 d * x * d0 * x * d != x * c * c0 * d * x. [ur(2,a,4,a,c,34,a),flip(a)]. given #78 (F,wt=0): 86 b * d * d0 * d0 * x * d0 * c * c0 != a * c0 * c * c0 * x * c * c0 * d0. [ur(2,b,29,a,c,33,a)]. given #79 (T,wt=17): 159 c * a0 != x | c * a0 * y != x | b0 * y = b0. [para(25(a,1),26(b,1)),flip(c)]. given #80 (T,wt=17): 254 a * c0 != x | a * a0 * y != x | b0 * y = d0. [para(21(a,1),30(b,1)),flip(c)]. given #81 (A,wt=27): 40 a * a0 * x * y * b0 * x * b = b0 * x * b * y * a * a0 * x. [para(21(a,1),4(a,1,2,2,2)),rewrite(1(10),1(17),1(19),21(20)),flip(a)]. given #82 (F,wt=0): 98 d0 * x * d * y * d * d0 * x != c * c0 * x * y * d0 * x * d. [ur(10,a,4,a,c,34,a),rewrite(1(8),1(10),1(9),1(20)),flip(a)]. given #83 (F,wt=0): 99 d0 * x * y * x * c * c0 * d * z * d * d0 * x * y * x * c * c0 != x * c * c0 * y * c * c0 * x * z * d0 * x * y * x * c * c0 * d. [ur(10,a,4,a,c,33,a),rewrite(1(20),1(19),1(18),1(17),1(16),1(22),1(21),1(20),1(19),1(18),1(17),1(44),1(43),1(42),1(41),1(40)),flip(a)]. given #84 (T,wt=17): 255 a * c0 != x | a * c0 * y != x | d0 * y = d0. [para(29(a,1),30(b,1)),flip(c)]. given #85 (T,wt=17): 797 a * a0 * x != y | c * a0 * x != y | d = b. [para(25(a,1),39(b,1)),flip(c)]. given #86 (A,wt=19): 41 b0 * x * b * x * b0 = x * b0 * a * a0 * x. [para(21(a,1),4(a,1,2,2)),flip(a)]. given #87 (F,wt=0): 100 d0 * d * x * d * d0 != c * c0 * x * d0 * d. [ur(10,a,4,a,c,8,a),rewrite(1(8)),flip(a)]. given #88 (F,wt=0): 101 c0 * x * c * y * c * c0 * x != d * d0 * x * y * c0 * x * c. [ur(10,a,4,a,c,34,a(flip)),rewrite(1(8),1(10),1(9),1(20)),flip(a)]. given #89 (T,wt=17): 1000 x * a * a0 != y | x * a * c0 != y | d0 = b0. [para(7(a,1),54(b,1,2)),flip(c)]. given #90 (T,wt=17): 1950 x * a * a0 != y | a * a0 != y | x * b = b. [para(5(a,1),110(b,1))]. given #91 (A,wt=19): 42 b * x * b0 * x * b = x * a * a0 * b * x. [para(21(a,1),4(a,1,2)),flip(a)]. given #92 (F,wt=0): 102 c * c0 * x * c * c0 * y * y * z * y * c * c0 * x * c * c0 * y != d * d0 * y * x * y * c * c0 * z * c * c0 * x * c * c0 * y * y. [ur(10,a,4,a,c,33,a(flip)),rewrite(1(20),1(19),1(18),1(17),1(16),1(22),1(21),1(20),1(19),1(18),1(17),1(44),1(43),1(42),1(41),1(40)),flip(a)]. given #93 (F,wt=0): 103 d * d0 * x * c0 * c != c0 * c * x * c * c0. [ur(10,a,4,a,c,8,a(flip)),rewrite(1(8))]. given #94 (T,wt=17): 1951 x * a * a0 != y | c * a0 != y | x * b = d. [para(6(a,1),110(b,1))]. given #95 (T,wt=17): 1953 x * c * a0 != y | a * a0 != y | x * d = b. [para(6(a,1),111(a,1,2))]. given #96 (A,wt=23): 43 a * a0 * x * y * x * b0 = b * x * b0 * y * b0 * x. [para(4(a,1),21(a,1,2)),flip(a)]. given #97 (F,wt=0): 104 d * d0 * x * y * z * x * y * c * c0 * u != x * y * c * c0 * z * c * c0 * x * y * u. [ur(10,a,1,a,c,33,a(flip)),rewrite(1(8),1(10),1(13),1(12),1(11),1(10),1(9),1(8),1(7),1(6),1(24),1(23),1(22),1(21),1(20),1(19))]. given #98 (F,wt=0): 122 c * c0 * x * y * x * d * d0 * z * u * z * x * d * d0 * y * d * d0 * x != z * x * d * d0 * y * d * d0 * x * u * x * d * d0 * y * d * d0 * x * z. [ur(10,b,4,a,c,35,a),rewrite(1(23),1(22),1(21),1(20),1(19),1(45),1(44),1(43),1(42),1(41),1(40),1(47),1(46),1(45),1(44),1(43),1(42))]. given #99 (T,wt=17): 2139 x * c * a0 != y | c * a0 != y | x * d = d. [para(6(a,1),112(b,1))]. given #100 (T,wt=17): 2285 x * a * c0 != y | a * c0 != y | x * b = b. [para(7(a,1),114(b,1))]. given #101 (A,wt=27): 46 c * a0 * x * y * b0 * x * d = b0 * x * d * y * c * a0 * x. [para(25(a,1),4(a,1,2,2,2)),rewrite(1(10),1(17),1(19),25(20)),flip(a)]. given #102 (F,wt=0): 123 c * c0 * x * y * x * d * d0 * z != x * d * d0 * y * d * d0 * x * z. [ur(10,b,1,a,c,35,a),rewrite(1(10),1(9),1(8),1(7),1(6),1(21),1(20),1(19),1(18),1(17))]. given #103 (F,wt=0): 124 c0 * x * y * x * d * d0 * c * z * c * c0 * x * y * x * d * d0 != x * d * d0 * y * d * d0 * x * z * c0 * x * y * x * d * d0 * c. [ur(10,a,4,a,c,35,a),rewrite(1(20),1(19),1(18),1(17),1(16),1(22),1(21),1(20),1(19),1(18),1(17),1(44),1(43),1(42),1(41),1(40)),flip(a)]. given #104 (T,wt=19): 47 b0 * x * d * x * b0 = x * b0 * c * a0 * x. [para(25(a,1),4(a,1,2,2)),flip(a)]. given #105 (T,wt=19): 48 d * x * b0 * x * d = x * c * a0 * d * x. [para(25(a,1),4(a,1,2)),flip(a)]. given #106 (A,wt=23): 49 c * a0 * x * y * x * b0 = d * x * b0 * y * b0 * x. [para(4(a,1),25(a,1,2)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 2.95 (+ 0.03) seconds. % Length of proof is 16. % Level of proof is 4. % Maximum clause weight is 23. % Given clauses 106. 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 * z * y * x = y * x * z * x * y # label(nilpotent_class2). [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]. 10 x * y * z != u | v * z != u | x * y = v. [para(1(a,1),3(a,1))]. 21 b * b0 * x = a * a0 * x. [para(5(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. 25 d * b0 * x = c * a0 * x. [para(6(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. 29 b * d0 * x = a * c0 * x. [para(7(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. 43 a * a0 * x * y * x * b0 = b * x * b0 * y * b0 * x. [para(4(a,1),21(a,1,2)),flip(a)]. 49 c * a0 * x * y * x * b0 = d * x * b0 * y * b0 * x. [para(4(a,1),25(a,1,2)),flip(a)]. 3248 a0 * d0 * x * d0 * b0 = c0 * b0 * x * b0 * d0. [hyper(2,a,29,a(flip),b,43,a),flip(a)]. 4128 $F. [ur(10,a,49,a(flip),c,8,a),rewrite(1(10),3248(19)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=106. Generated=20511. Kept=4127. proofs=1. Usable=106. Sos=3865. Demods=90. Limbo=17, Disabled=147. Hints=0. Weight_deleted=1709. Literals_deleted=0. Forward_subsumed=14674. Back_subsumed=133. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=94 (0 lex), Back_demodulated=6. Back_unit_deleted=0. Demod_attempts=1520521. Demod_rewrites=288728. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=15341. Nonunit_bsub_feature_tests=2065. Megabytes=14.77. User_CPU=2.95, System_CPU=0.03, Wall_clock=3. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11391 exit (max_proofs) Sat Aug 12 21:00:11 2006