============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 3899 was started by mccune on cleo.thornwood, Wed Nov 22 11:24:28 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). restricted denial: (wt=7): 8 d * d0 != c * c0. [assumption]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 8 d * d0 != c * c0. [assumption]. 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]. 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 (F,wt=11): 21 b * b0 * x = a * a0 * x. [para(5(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. given #9 (T,wt=11): 25 d * b0 * x = c * a0 * x. [para(6(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. given #10 (T,wt=11): 29 b * d0 * x = a * c0 * x. [para(7(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=13): 22 a * a0 != x | b * y != x | b0 = y. [para(5(a,1),2(a,1))]. given #13 (F,wt=13): 23 a * a0 != x | y * b0 != x | b = y. [para(5(a,1),3(a,1))]. given #14 (T,wt=13): 26 c * a0 != x | d * y != x | b0 = y. [para(6(a,1),2(a,1))]. given #15 (T,wt=13): 27 c * a0 != x | y * b0 != x | d = y. [para(6(a,1),3(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=13): 30 a * c0 != x | b * y != x | d0 = y. [para(7(a,1),2(a,1))]. given #18 (F,wt=13): 31 a * c0 != x | y * d0 != x | b = y. [para(7(a,1),3(a,1))]. given #19 (T,wt=13): 61 a * a0 != x | a * c0 != x | d0 = b0. [para(7(a,1),22(b,1)),flip(c)]. given #20 (T,wt=13): 65 a * a0 != x | c * a0 != x | d = b. [para(6(a,1),23(b,1)),flip(c)]. 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=17): 33 a * a0 * x != y | b * z != y | b0 * x = z. [para(21(a,1),2(a,1))]. given #23 (F,wt=17): 34 a * a0 * x != y | z * b0 * x != y | b = z. [para(21(a,1),3(a,1))]. given #24 (T,wt=17): 39 c * a0 * x != y | d * z != y | b0 * x = z. [para(25(a,1),2(a,1))]. given #25 (T,wt=17): 40 c * a0 * x != y | z * b0 * x != y | d = z. [para(25(a,1),3(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=17): 45 a * c0 * x != y | b * z != y | d0 * x = z. [para(29(a,1),2(a,1))]. given #28 (F,wt=17): 46 a * c0 * x != y | z * d0 * x != y | b = z. [para(29(a,1),3(a,1))]. given #29 (T,wt=17): 54 x * a * a0 != y | x * b * z != y | b0 = z. [para(5(a,1),9(a,1,2))]. given #30 (T,wt=17): 55 x * c * a0 != y | x * d * z != y | b0 = z. [para(6(a,1),9(a,1,2))]. 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=17): 56 x * a * c0 != y | x * b * z != y | d0 = z. [para(7(a,1),9(a,1,2))]. given #33 (F,wt=17): 62 a * a0 != x | a * a0 * y != x | b0 * y = b0. [para(21(a,1),22(b,1)),flip(c)]. given #34 (T,wt=17): 63 a * a0 != x | a * c0 * y != x | d0 * y = b0. [para(29(a,1),22(b,1)),flip(c)]. given #35 (T,wt=17): 64 a * a0 != x | y * z * b0 != x | y * z = b. [para(1(a,1),23(b,1)),flip(c)]. 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=17): 67 c * a0 != x | c * a0 * y != x | b0 * y = b0. [para(25(a,1),26(b,1)),flip(c)]. given #38 (F,wt=17): 68 c * a0 != x | y * z * b0 != x | y * z = d. [para(1(a,1),27(b,1)),flip(c)]. given #39 (T,wt=17): 74 x * a * a0 != y | z * b0 != y | x * b = z. [para(5(a,1),10(a,1,2))]. given #40 (T,wt=17): 75 x * c * a0 != y | z * b0 != y | x * d = z. [para(6(a,1),10(a,1,2))]. 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=17): 76 x * a * c0 != y | z * d0 != y | x * b = z. [para(7(a,1),10(a,1,2))]. given #43 (F,wt=17): 77 x * y * d0 != z | a * c0 != z | x * y = b. [para(7(a,1),10(b,1))]. given #44 (T,wt=17): 85 a * c0 != x | a * a0 * y != x | b0 * y = d0. [para(21(a,1),30(b,1)),flip(c)]. given #45 (T,wt=17): 86 a * c0 != x | a * c0 * y != x | d0 * y = d0. [para(29(a,1),30(b,1)),flip(c)]. 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=17): 142 a * a0 * x != y | c * a0 * x != y | d = b. [para(25(a,1),34(b,1)),flip(c)]. given #48 (F,wt=17): 268 x * a * a0 != y | x * a * c0 != y | d0 = b0. [para(7(a,1),54(b,1,2)),flip(c)]. given #49 (T,wt=17): 338 a * a0 != x | y * a * a0 != x | y * b = b. [para(5(a,1),64(b,1,2))]. given #50 (T,wt=17): 339 a * a0 != x | y * c * a0 != x | y * d = b. [para(6(a,1),64(b,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=17): 419 c * a0 != x | y * a * a0 != x | y * b = d. [para(5(a,1),68(b,1,2))]. given #53 (F,wt=17): 420 c * a0 != x | y * c * a0 != x | y * d = d. [para(6(a,1),68(b,1,2))]. given #54 (T,wt=17): 442 x * a * c0 != y | a * c0 != y | x * b = b. [para(7(a,1),76(b,1))]. given #55 (T,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 #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=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 #58 (F,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 #59 (T,wt=19): 36 b0 * x * b * x * b0 = x * b0 * a * a0 * x. [para(21(a,1),4(a,1,2,2)),flip(a)]. given #60 (T,wt=19): 37 b * x * b0 * x * b = x * a * a0 * b * x. [para(21(a,1),4(a,1,2)),flip(a)]. 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=19): 42 b0 * x * d * x * b0 = x * b0 * c * a0 * x. [para(25(a,1),4(a,1,2,2)),flip(a)]. given #63 (F,wt=19): 43 d * x * b0 * x * d = x * c * a0 * d * x. [para(25(a,1),4(a,1,2)),flip(a)]. given #64 (T,wt=19): 48 d0 * x * b * x * d0 = x * d0 * a * c0 * x. [para(29(a,1),4(a,1,2,2)),flip(a)]. given #65 (T,wt=19): 49 b * x * d0 * x * b = x * a * c0 * b * x. [para(29(a,1),4(a,1,2)),flip(a)]. given #66 (A,wt=27): 35 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 #67 (F,wt=19): 283 d0 * a0 * x * a0 * c0 = b0 * c0 * x * c0 * a0. [hyper(45,a,14,a,b,21,a)]. given #68 (F,wt=19): 520 b0 * b * b * a * a0 = a * a0 * a * a0 * b. [para(21(a,1),24(a,1,2,2)),flip(a)]. given #69 (T,wt=19): 521 a * a0 * b0 * b0 * b = b0 * a * a0 * a * a0. [para(21(a,1),24(a,2,2))]. given #70 (T,wt=19): 523 b0 * b * d * a * a0 = a * a0 * c * a0 * b. [para(25(a,1),24(a,1,2,2)),flip(a)]. given #71 (A,wt=23): 38 a * a0 * x * y * x * b0 = b * x * b0 * y * b0 * x. [para(4(a,1),21(a,1,2)),flip(a)]. given #72 (F,wt=19): 524 a * a0 * d0 * b0 * b = b0 * a * c0 * a * a0. [para(29(a,1),24(a,2,2))]. given #73 (F,wt=19): 585 b0 * c * a0 * c * a0 = c * a0 * b0 * b0 * d. [para(25(a,1),28(a,1,2))]. given #74 (T,wt=19): 605 d0 * a * a0 * a * c0 = a * c0 * b0 * d0 * b. [para(21(a,1),32(a,1,2))]. given #75 (T,wt=19): 607 a * c0 * d0 * d0 * b = d0 * a * c0 * a * c0. [para(29(a,1),32(a,1,2)),flip(a)]. given #76 (A,wt=27): 41 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 #77 (F,wt=19): 608 d0 * b * b * a * c0 = a * c0 * a * c0 * b. [para(29(a,1),32(a,2,2,2))]. given #78 (F,wt=19): 648 b0 * d0 * a * c0 * b0 = d0 * b0 * a * a0 * d0. [para(29(a,1),36(a,1,2,2))]. given #79 (T,wt=19): 699 d * a * a0 * b * d = b * c * a0 * d * b. [para(25(a,1),37(a,1,2)),flip(a)]. given #80 (T,wt=19): 1085 a0 * d0 * x * d0 * b0 = c0 * b0 * x * b0 * d0. [hyper(2,a,29,a(flip),b,38,a),flip(a)]. given #81 (A,wt=23): 44 c * a0 * x * y * x * b0 = d * x * b0 * y * b0 * x. [para(4(a,1),25(a,1,2)),flip(a)]. given #82 (F,wt=19): 1278 a0 * d0 * a * c0 * b0 = c0 * b0 * a * a0 * d0. [para(21(a,1),1085(a,2,2,2)),rewrite(29(7))]. given #83 (F,wt=21): 51 x * y * z * u != v | x * y * z * w != v | u = w. [para(1(a,1),9(a,1,2)),rewrite(1(6))]. given #84 (T,wt=21): 57 x * a * a0 * y != z | x * b * u != z | b0 * y = u. [para(21(a,1),9(a,1,2))]. given #85 (T,wt=21): 58 x * c * a0 * y != z | x * d * u != z | b0 * y = u. [para(25(a,1),9(a,1,2))]. given #86 (A,wt=27): 47 d0 * x * b * y * a * c0 * x = a * c0 * x * y * d0 * x * b. [para(29(a,1),4(a,1,2,2,2)),rewrite(1(10),1(17),1(19),29(20))]. given #87 (F,wt=21): 59 x * a * c0 * y != z | x * b * u != z | d0 * y = u. [para(29(a,1),9(a,1,2))]. given #88 (F,wt=21): 69 x * y * z * u != v | w * u != v | x * y * z = w. [para(1(a,1),10(a,1,2))]. given #89 (T,wt=21): 70 x * y * z != u | v * w * z != u | x * y = v * w. [para(1(a,1),10(b,1))]. given #90 (T,wt=21): 78 x * a * a0 * y != z | u * b0 * y != z | x * b = u. [para(21(a,1),10(a,1,2))]. given #91 (A,wt=23): 50 a * c0 * x * y * x * d0 = b * x * d0 * y * d0 * x. [para(4(a,1),29(a,1,2)),flip(a)]. given #92 (F,wt=21): 79 x * y * b0 * z != u | a * a0 * z != u | x * y = b. [para(21(a,1),10(b,1))]. given #93 (F,wt=21): 80 x * c * a0 * y != z | u * b0 * y != z | x * d = u. [para(25(a,1),10(a,1,2))]. given #94 (T,wt=21): 81 x * y * b0 * z != u | c * a0 * z != u | x * y = d. [para(25(a,1),10(b,1))]. given #95 (T,wt=21): 82 x * a * c0 * y != z | u * d0 * y != z | x * b = u. [para(29(a,1),10(a,1,2))]. given #96 (A,wt=29): 52 x * y * z * u * z * y != v | x * z * w != v | y * u * y * z = w. [para(4(a,1),9(a,1,2))]. given #97 (F,wt=21): 83 x * y * d0 * z != u | a * c0 * z != u | x * y = b. [para(29(a,1),10(b,1))]. given #98 (F,wt=21): 133 a * a0 * x != y | a * a0 * z != y | b0 * x = b0 * z. [para(21(a,1),33(b,1))]. given #99 (T,wt=21): 134 a * a0 * x != y | a * c0 * z != y | d0 * z = b0 * x. [para(29(a,1),33(b,1)),flip(c)]. given #100 (T,wt=21): 152 c * a0 * x != y | c * a0 * z != y | b0 * x = b0 * z. [para(25(a,1),39(b,1))]. given #101 (A,wt=25): 53 x * y * z * y * x != u | y * x * v != u | z * x * y = v. [para(4(a,1),9(a,1))]. given #102 (F,wt=21): 247 a * c0 * x != y | a * c0 * z != y | d0 * x = d0 * z. [para(29(a,1),45(b,1))]. given #103 (F,wt=21): 265 x * y * a * a0 != z | x * y * b * u != z | b0 = u. [para(1(a,1),54(a,1)),rewrite(1(10))]. given #104 (T,wt=21): 269 x * a * a0 != y | x * a * a0 * z != y | b0 * z = b0. [para(21(a,1),54(b,1,2)),flip(c)]. given #105 (T,wt=21): 270 x * a * a0 != y | x * a * c0 * z != y | d0 * z = b0. [para(29(a,1),54(b,1,2)),flip(c)]. given #106 (A,wt=25): 60 a * a0 != x | y * b * z * b * y != x | y * z * y * b = b0. [para(4(a,1),22(b,1)),flip(c)]. given #107 (F,wt=21): 275 x * y * c * a0 != z | x * y * d * u != z | b0 = u. [para(1(a,1),55(a,1)),rewrite(1(10))]. given #108 (F,wt=21): 278 x * c * a0 != y | x * c * a0 * z != y | b0 * z = b0. [para(25(a,1),55(b,1,2)),flip(c)]. given #109 (T,wt=21): 313 x * y * a * c0 != z | x * y * b * u != z | d0 = u. [para(1(a,1),56(a,1)),rewrite(1(10))]. given #110 (T,wt=21): 316 x * a * c0 != y | x * a * a0 * z != y | b0 * z = d0. [para(21(a,1),56(b,1,2)),flip(c)]. given #111 (A,wt=25): 66 c * a0 != x | y * d * z * d * y != x | y * z * y * d = b0. [para(4(a,1),26(b,1)),flip(c)]. given #112 (F,wt=21): 317 x * a * c0 != y | x * a * c0 * z != y | d0 * z = d0. [para(29(a,1),56(b,1,2)),flip(c)]. given #113 (F,wt=21): 337 a * a0 != x | y * z * u * b0 != x | y * z * u = b. [para(1(a,1),64(b,1,2))]. given #114 (T,wt=21): 418 c * a0 != x | y * z * u * b0 != x | y * z * u = d. [para(1(a,1),68(b,1,2))]. given #115 (T,wt=21): 421 x * y * a * a0 != z | u * b0 != z | x * y * b = u. [para(1(a,1),74(a,1)),rewrite(1(12))]. given #116 (A,wt=29): 71 x * y * z * u * z * y != v | w * y * u * y * z != v | x * z = w. [para(4(a,1),10(a,1,2))]. given #117 (F,wt=21): 422 x * a * a0 != y | z * u * b0 != y | x * b = z * u. [para(1(a,1),74(b,1))]. given #118 (F,wt=21): 423 x * y * c * a0 != z | u * b0 != z | x * y * d = u. [para(1(a,1),75(a,1)),rewrite(1(12))]. given #119 (T,wt=21): 424 x * c * a0 != y | z * u * b0 != y | x * d = z * u. [para(1(a,1),75(b,1))]. given #120 (T,wt=21): 440 x * y * a * c0 != z | u * d0 != z | x * y * b = u. [para(1(a,1),76(a,1)),rewrite(1(12))]. given #121 (A,wt=25): 72 x * y * z * y * x != u | v * z * x * y != u | y * x = v. [para(4(a,1),10(a,1))]. given #122 (F,wt=21): 441 x * a * c0 != y | z * u * d0 != y | x * b = z * u. [para(1(a,1),76(b,1))]. given #123 (F,wt=21): 443 x * y * z * d0 != u | a * c0 != u | x * y * z = b. [para(1(a,1),77(a,1,2))]. given #124 (T,wt=21): 503 x * y * a * a0 != z | x * y * a * c0 != z | d0 = b0. [para(1(a,1),268(a,1)),rewrite(1(11))]. given #125 (T,wt=21): 504 a * a0 != x | y * z * a * a0 != x | y * z * b = b. [para(1(a,1),338(b,1)),rewrite(1(13))]. given #126 (A,wt=29): 73 x * y * z * u * z * v != w | z * v * u * v * z != w | x * y = v. [para(4(a,1),10(b,1))]. given #127 (F,wt=21): 505 a * a0 != x | y * z * c * a0 != x | y * z * d = b. [para(1(a,1),339(b,1)),rewrite(1(13))]. given #128 (F,wt=21): 510 c * a0 != x | y * z * a * a0 != x | y * z * b = d. [para(1(a,1),419(b,1)),rewrite(1(13))]. given #129 (T,wt=21): 511 c * a0 != x | y * z * c * a0 != x | y * z * d = d. [para(1(a,1),420(b,1)),rewrite(1(13))]. given #130 (T,wt=21): 512 x * y * a * c0 != z | a * c0 != z | x * y * b = b. [para(1(a,1),442(a,1)),rewrite(1(13))]. given #131 (A,wt=25): 84 a * c0 != x | y * b * z * b * y != x | y * z * y * b = d0. [para(4(a,1),30(b,1)),flip(c)]. given #132 (F,wt=21): 1826 x * a * a0 * y != z | a * a0 * y != z | x * b = b. [para(21(a,1),78(b,1))]. given #133 (F,wt=21): 1827 x * a * a0 * y != z | c * a0 * y != z | x * b = d. [para(25(a,1),78(b,1))]. given #134 (T,wt=21): 1910 x * c * a0 * y != z | a * a0 * y != z | x * d = b. [para(25(a,1),79(a,1,2))]. given #135 (T,wt=21): 1948 x * c * a0 * y != z | c * a0 * y != z | x * d = d. [para(25(a,1),80(b,1))]. given #136 (A,wt=31): 88 x * y * z * u * z * x * y * v = z * x * y * u * x * y * z * v. [para(12(a,1),1(a,1)),rewrite(1(4),1(6),1(9)),flip(a)]. given #137 (F,wt=21): 2023 x * a * c0 * y != z | a * c0 * y != z | x * b = b. [para(29(a,1),82(b,1))]. given #138 (F,wt=21): 2407 x * a * a0 != y | z * a * a0 != y | x * b = z * b. [para(5(a,1),422(b,1,2))]. given #139 (T,wt=21): 2408 x * a * a0 != y | z * c * a0 != y | z * d = x * b. [para(6(a,1),422(b,1,2)),flip(c)]. given #140 (T,wt=21): 2409 x * a * a0 != y | a * a0 * b0 != y | a * a0 = x * b. [para(21(a,1),422(b,1)),rewrite(5(16)),flip(c)]. given #141 (A,wt=27): 89 x * y * z * u * z * y * v = x * z * y * u * y * z * v. [para(12(a,1),1(a,2,2)),rewrite(1(6))]. given #142 (F,wt=21): 2410 x * a * a0 != y | c * a0 * b0 != y | c * a0 = x * b. [para(25(a,1),422(b,1)),rewrite(6(16)),flip(c)]. given #143 (F,wt=21): 2411 x * a * a0 != y | a * c0 * b0 != y | a * c0 = x * b. [para(29(a,1),422(b,1)),rewrite(7(16)),flip(c)]. given #144 (T,wt=21): 2415 x * c * a0 != y | z * c * a0 != y | x * d = z * d. [para(6(a,1),424(b,1,2))]. given #145 (T,wt=21): 2416 x * c * a0 != y | a * a0 * b0 != y | a * a0 = x * d. [para(21(a,1),424(b,1)),rewrite(5(16)),flip(c)]. given #146 (A,wt=27): 90 x * y * z * u * y * x * v = y * x * z * u * x * y * v. [para(1(a,1),12(a,1,2,2)),rewrite(1(10))]. given #147 (F,wt=21): 2417 x * c * a0 != y | c * a0 * b0 != y | c * a0 = x * d. [para(25(a,1),424(b,1)),rewrite(6(16)),flip(c)]. given #148 (F,wt=21): 2418 x * c * a0 != y | a * c0 * b0 != y | a * c0 = x * d. [para(29(a,1),424(b,1)),rewrite(7(16)),flip(c)]. given #149 (T,wt=21): 2459 x * a * c0 != y | z * a * c0 != y | x * b = z * b. [para(7(a,1),441(b,1,2))]. given #150 (T,wt=21): 2460 x * a * c0 != y | a * a0 * d0 != y | a * a0 = x * b. [para(21(a,1),441(b,1)),rewrite(5(16)),flip(c)]. given #151 (A,wt=29): 91 x * y * z * y * x * u != v | y * w != v | x * z * x * y * u = w. [para(12(a,1),2(a,1))]. given #152 (F,wt=21): 2461 x * a * c0 != y | c * a0 * d0 != y | c * a0 = x * b. [para(25(a,1),441(b,1)),rewrite(6(16)),flip(c)]. given #153 (F,wt=21): 2462 x * a * c0 != y | a * c0 * d0 != y | a * c0 = x * b. [para(29(a,1),441(b,1)),rewrite(7(16)),flip(c)]. given #154 (T,wt=23): 98 x * y * y * y * x * x = y * y * x * x * x * y. [para(4(a,1),12(a,1,2)),flip(a)]. given #155 (T,wt=23): 99 b * x * y * x * a * a0 = x * b * y * b * x * b0. [para(5(a,1),12(a,1,2,2,2,2))]. given #156 (A,wt=29): 92 x * y * z * y * x * u != v | w * x * z * x * y * u != v | y = w. [para(12(a,1),3(a,1))]. given #157 (F,wt=23): 100 d * x * y * x * c * a0 = x * d * y * d * x * b0. [para(6(a,1),12(a,1,2,2,2,2))]. given #158 (F,wt=23): 101 b * x * y * x * a * c0 = x * b * y * b * x * d0. [para(7(a,1),12(a,1,2,2,2,2))]. given #159 (T,wt=23): 103 a * a0 * x * b0 * b * y = b0 * b * x * a * a0 * y. [para(12(a,1),21(a,1)),rewrite(21(6)),flip(a)]. given #160 (T,wt=23): 105 b0 * x * b * x * b0 * y = x * b0 * a * a0 * x * y. [para(21(a,1),12(a,1,2,2)),flip(a)]. given #161 (A,wt=29): 93 x * y * z * y * u * v != w | y * u * z * u * y * v != w | x = u. [para(12(a,1),3(b,1))]. given #162 (F,wt=23): 106 b * x * b0 * x * b * y = x * a * a0 * b * x * y. [para(21(a,1),12(a,1,2)),flip(a)]. given #163 (F,wt=23): 108 c * a0 * x * b0 * d * y = b0 * d * x * c * a0 * y. [para(12(a,1),25(a,1)),rewrite(25(6)),flip(a)]. given #164 (T,wt=23): 110 b0 * x * d * x * b0 * y = x * b0 * c * a0 * x * y. [para(25(a,1),12(a,1,2,2)),flip(a)]. given #165 (T,wt=23): 111 d * x * b0 * x * d * y = x * c * a0 * d * x * y. [para(25(a,1),12(a,1,2)),flip(a)]. given #166 (A,wt=35): 94 x * y * z * x * y * y * y * x * z = y * x * y * z * x * x * y * z * y. [para(12(a,1),4(a,1,2)),rewrite(1(8),1(7),1(13),1(12),1(15),1(14))]. given #167 (F,wt=23): 113 d0 * b * x * a * c0 * y = a * c0 * x * d0 * b * y. [para(12(a,1),29(a,1)),rewrite(29(6))]. given #168 (F,wt=23): 115 d0 * x * b * x * d0 * y = x * d0 * a * c0 * x * y. [para(29(a,1),12(a,1,2,2)),flip(a)]. given #169 (T,wt=23): 116 b * x * d0 * x * b * y = x * a * c0 * b * x * y. [para(29(a,1),12(a,1,2)),flip(a)]. given #170 (T,wt=23): 129 b0 * b * x * b * a * a0 = a * a0 * x * a * a0 * b. [hyper(33,a,1,a(flip),b,4,a),rewrite(1(18),1(20))]. given #171 (A,wt=35): 95 x * y * z * y * u * x * v * x * u = y * x * z * x * y * u * v * u * x. [para(4(a,1),12(a,1,2,2,2,2))]. given #172 (F,wt=23): 169 d0 * b * x * b * a * c0 = a * c0 * x * a * c0 * b. [hyper(2,a,29,a,b,13,a(flip))]. given #173 (F,wt=23): 289 x * a * a0 * y * b0 * b = x * b0 * b * y * a * a0. [para(5(a,1),14(a,1,2,2,2,2)),rewrite(21(17)),flip(a)]. given #174 (T,wt=19): 5560 b0 * b * a * a * a0 = a * a0 * a * b0 * b. [hyper(91,a,12,a,b,289,a(flip)),flip(a)]. given #175 (T,wt=23): 290 x * d0 * b * y * a * c0 = x * a * c0 * y * d0 * b. [para(7(a,1),14(a,1,2,2,2,2)),rewrite(29(17))]. given #176 (A,wt=31): 96 x * y * z * y * x * u * y * x = y * x * z * y * x * u * x * y. [para(4(a,1),12(a,1,2,2,2)),flip(a)]. given #177 (F,wt=19): 5664 x * y * x * x * y = x * x * y * y * x. [hyper(51,a,90,a,b,96,a),flip(a)]. given #178 (F,wt=15): 5741 x * y * y * x = y * x * x * y. [hyper(2,a,xx,b,5664,a)]. given #179 (T,wt=15): 5742 d0 * b * a * c0 = a * c0 * d0 * b. [hyper(45,a,29,a(flip),b,5664,a(flip)),rewrite(7(5),29(14))]. given #180 (T,wt=15): 5743 b0 * d * c * a0 = c * a0 * b0 * d. [hyper(39,a,25,a(flip),b,5664,a(flip)),rewrite(6(5),25(14))]. given #181 (A,wt=27): 97 x * y * z * y * x * x * z = y * x * x * z * y * z * x. [para(4(a,1),12(a,1,2,2)),flip(a)]. given #182 (F,wt=15): 5744 b0 * b * a * a0 = a * a0 * b0 * b. [hyper(33,a,21,a(flip),b,5664,a(flip)),rewrite(5(5),21(14))]. given #183 (F,wt=19): 5757 b * a * a0 * b0 * b = a * a0 * b * a * a0. [para(5664(a,1),21(a,1)),rewrite(21(8),5(15))]. given #184 (T,wt=19): 5763 d * c * a0 * b0 * d = c * a0 * d * c * a0. [para(5664(a,1),25(a,1)),rewrite(25(8),6(15))]. given #185 (T,wt=19): 5768 b * a * c0 * d0 * b = a * c0 * b * a * c0. [para(5664(a,1),29(a,1)),rewrite(29(8),7(15))]. given #186 (A,wt=27): 102 a * a0 * x * y * x * b0 * z = b * x * b0 * y * b0 * x * z. [para(12(a,1),21(a,1,2)),flip(a)]. given #187 (F,wt=19): 6165 x * y * y * x * z = y * x * x * y * z. [para(5741(a,1),1(a,1,1)),rewrite(1(4),1(3),1(2),1(7),1(6))]. given #188 (F,wt=19): 6167 x * y * z * z * y = x * z * y * y * z. [para(5741(a,1),1(a,2,2)),rewrite(1(4))]. given #189 (T,wt=15): 7535 d0 * a0 * a0 * c0 = b0 * c0 * c0 * a0. [hyper(134,a,xx,b,6167,a)]. given #190 (T,wt=19): 6172 a * a0 * x * x * b0 = b * x * b0 * b0 * x. [para(5741(a,1),21(a,1,2)),flip(a)]. given #191 (A,wt=27): 104 b * x * y * x * a * a0 * z = x * b * y * b * x * b0 * z. [para(21(a,1),12(a,1,2,2,2,2))]. given #192 (F,wt=15): 7663 a0 * d0 * d0 * b0 = c0 * b0 * b0 * d0. [hyper(2,a,29,a(flip),b,6172,a),flip(a)]. given #193 (F,wt=19): 6174 c * a0 * x * x * b0 = d * x * b0 * b0 * x. [para(5741(a,1),25(a,1,2)),flip(a)]. given #194 (T,wt=19): 6176 a * c0 * x * x * d0 = b * x * d0 * d0 * x. [para(5741(a,1),29(a,1,2)),flip(a)]. given #195 (T,wt=19): 6427 d0 * b * a * c0 * x = a * c0 * d0 * b * x. [para(5742(a,1),1(a,1,1)),rewrite(1(8),1(7),1(6),1(15),1(14)),flip(a)]. given #196 (A,wt=27): 107 c * a0 * x * y * x * b0 * z = d * x * b0 * y * b0 * x * z. [para(12(a,1),25(a,1,2)),flip(a)]. given #197 (F,wt=19): 6498 b0 * d * c * a0 * x = c * a0 * b0 * d * x. [para(5743(a,1),1(a,1,1)),rewrite(1(8),1(7),1(6),1(15),1(14)),flip(a)]. given #198 (F,wt=19): 6502 a * a0 * d * c * a0 = b * c * a0 * b0 * d. [para(5743(a,1),21(a,1,2)),flip(a)]. given #199 (T,wt=19): 6718 b0 * b * a * a0 * x = a * a0 * b0 * b * x. [para(5744(a,1),1(a,1,1)),rewrite(1(8),1(7),1(6),1(15),1(14)),flip(a)]. given #200 (T,wt=19): 6722 d * a * a0 * b0 * b = c * a0 * b * a * a0. [para(5744(a,1),25(a,1,2))]. given #201 (A,wt=27): 109 d * x * y * x * c * a0 * z = x * d * y * d * x * b0 * z. [para(25(a,1),12(a,1,2,2,2,2))]. given #202 (F,wt=19): 7103 b * x * x * a * a0 = x * b * b * x * b0. [para(5(a,1),6165(a,1,2,2,2))]. given #203 (F,wt=19): 7104 d * x * x * c * a0 = x * d * d * x * b0. [para(6(a,1),6165(a,1,2,2,2))]. given #204 (T,wt=19): 7105 b * x * x * a * c0 = x * b * b * x * d0. [para(7(a,1),6165(a,1,2,2,2))]. given #205 (T,wt=19): 7613 d0 * a0 * a0 * c0 * x = b0 * c0 * c0 * a0 * x. [para(7535(a,1),1(a,1,1)),rewrite(1(8),1(7),1(6),1(15),1(14)),flip(a)]. given #206 (A,wt=27): 112 a * c0 * x * y * x * d0 * z = b * x * d0 * y * d0 * x * z. [para(12(a,1),29(a,1,2)),flip(a)]. given #207 (F,wt=19): 7953 a0 * d0 * d0 * b0 * x = c0 * b0 * b0 * d0 * x. [para(7663(a,1),1(a,1,1)),rewrite(1(8),1(7),1(6),1(15),1(14)),flip(a)]. given #208 (F,wt=19): 8170 d * d0 * b0 * b0 * d0 = c * c0 * b0 * b0 * d0. [para(7663(a,1),6174(a,1,2)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 5.11 (+ 0.04) seconds. % Length of proof is 26. % Level of proof is 9. % Maximum clause weight is 31. % Given clauses 208. 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]. 9 x * y * z != u | x * y * v != u | z = v. [para(1(a,1),2(a,1)),rewrite(1(5))]. 10 x * y * z != u | v * z != u | x * y = v. [para(1(a,1),3(a,1))]. 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))]. 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)]. 51 x * y * z * u != v | x * y * z * w != v | u = w. [para(1(a,1),9(a,1,2)),rewrite(1(6))]. 70 x * y * z != u | v * w * z != u | x * y = v * w. [para(1(a,1),10(b,1))]. 90 x * y * z * u * y * x * v = y * x * z * u * x * y * v. [para(1(a,1),12(a,1,2,2)),rewrite(1(10))]. 96 x * y * z * y * x * u * y * x = y * x * z * y * x * u * x * y. [para(4(a,1),12(a,1,2,2,2)),flip(a)]. 5664 x * y * x * x * y = x * x * y * y * x. [hyper(51,a,90,a,b,96,a),flip(a)]. 5741 x * y * y * x = y * x * x * y. [hyper(2,a,xx,b,5664,a)]. 6172 a * a0 * x * x * b0 = b * x * b0 * b0 * x. [para(5741(a,1),21(a,1,2)),flip(a)]. 6174 c * a0 * x * x * b0 = d * x * b0 * b0 * x. [para(5741(a,1),25(a,1,2)),flip(a)]. 7663 a0 * d0 * d0 * b0 = c0 * b0 * b0 * d0. [hyper(2,a,29,a(flip),b,6172,a),flip(a)]. 8170 d * d0 * b0 * b0 * d0 = c * c0 * b0 * b0 * d0. [para(7663(a,1),6174(a,1,2)),flip(a)]. 10288 d * d0 = c * c0. [hyper(70,a,xx,b,8170,a),flip(a)]. 10289 $F. [resolve(10288,a,8,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=208. Generated=60503. Kept=10288. proofs=1. Usable=208. Sos=9181. Demods=1341. Limbo=0, Disabled=906. Hints=0. Weight_deleted=26947. Literals_deleted=0. Forward_subsumed=23268. Back_subsumed=604. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1618 (0 lex), Back_demodulated=294. Back_unit_deleted=0. Demod_attempts=2101660. Demod_rewrites=202520. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=350913. Nonunit_bsub_feature_tests=213731. Megabytes=14.46. User_CPU=5.11, System_CPU=0.04, Wall_clock=6. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3899 exit (max_proofs) Wed Nov 22 11:24:34 2006