============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11359 was started by mccune on cleo.thornwood, Sat Aug 12 20:59:57 2006 The command was "/home/mccune/bin/prover9 -f cs.in EA.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file cs.in op(450,infix,@). op(400,infix_right,*). assign(new_constants,1). assign(max_weight,25). formulas(sos). x * y != x * z | y = z. y * x != z * x | y = z. (x * y) * z = x * y * z. y * x * (x @ y) = x * y. end_of_list. % Reading from file EA.in formulas(sos). x * y * z * y * x = y * x * z * x * y. end_of_list. formulas(sos). (A @ B) @ C != D @ (F @ G) # answer(A). 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 != x * z | y = z. [assumption]. x * y != z * y | x = z. [assumption]. (x * y) * z = x * y * z. [assumption]. x * y * (y @ x) = y * x. [assumption]. x * y * z * y * x = y * x * z * x * y. [assumption]. (A @ B) @ C != D @ (F @ G) # answer(A). [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, B, C, D, F, G, *, @ ]). 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, 2). % (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 != x * z | y = z. [assumption]. 2 x * y != z * y | x = z. [assumption]. 3 (x * y) * z = x * y * z. [assumption]. 4 x * y * (y @ x) = y * x. [assumption]. 5 x * y * z * y * x = y * x * z * x * y. [assumption]. 6 (A @ B) @ C != D @ (F @ G) # answer(A). [assumption]. end_of_list. formulas(demodulators). 3 (x * y) * z = x * y * z. [assumption]. 4 x * y * (y @ x) = y * x. [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=10): 1 x * y != x * z | y = z. [assumption]. given #2 (I,wt=10): 2 x * y != z * y | x = z. [assumption]. given #3 (I,wt=11): 3 (x * y) * z = x * y * z. [assumption]. given #4 (I,wt=11): 4 x * y * (y @ x) = y * x. [assumption]. given #5 (I,wt=19): 5 x * y * z * y * x = y * x * z * x * y. [assumption]. given #6 (I,wt=11): 6 (A @ B) @ C != D @ (F @ G) # answer(A). [assumption]. given #7 (F,wt=15): 23 ((A @ B) @ C) * x != (D @ (F @ G)) * x # answer(A). [ur(2,b,6,a)]. given #8 (F,wt=15): 24 x * ((A @ B) @ C) != x * (D @ (F @ G)) # answer(A). [ur(1,b,6,a)]. given #9 (T,wt=7): 9 x * (x @ x) = x. [hyper(1,a,4,a)]. given #10 (T,wt=10): 29 x * y != x | x @ x = y. [para(9(a,1),1(a,1)),flip(a)]. given #11 (A,wt=14): 7 x * y * z != x * y * u | z = u. [para(3(a,1),1(a,1)),rewrite(3(4))]. given #12 (F,wt=19): 25 x * ((A @ B) @ C) * y != x * (D @ (F @ G)) * y # answer(A). [ur(1,b,23,a)]. given #13 (F,wt=19): 28 x * y * ((A @ B) @ C) != x * y * (D @ (F @ G)) # answer(A). [ur(1,b,24,a)]. given #14 (T,wt=10): 30 x * (y @ y) != y | y = x. [para(9(a,1),2(a,1)),flip(a)]. given #15 (T,wt=10): 31 x * (y @ y) != y | x = y. [para(9(a,1),2(a,2))]. given #16 (A,wt=14): 8 x * y * z != u * z | x * y = u. [para(3(a,1),2(a,1))]. given #17 (F,wt=17): 49 C * (A @ B) * (D @ (F @ G)) != (A @ B) * C # answer(A). [para(4(a,1),28(a,1)),flip(a)]. given #18 (F,wt=17): 50 (F @ G) * D * ((A @ B) @ C) != D * (F @ G) # answer(A). [para(4(a,1),28(a,2))]. given #19 (T,wt=11): 32 x * (x @ x) * y = x * y. [para(9(a,1),3(a,1,1)),flip(a)]. given #20 (T,wt=7): 65 (x @ x) * y = y. [hyper(7,a,32,a)]. given #21 (A,wt=14): 10 x * y != z * x | z * (z @ x) = y. [para(4(a,1),1(a,1)),flip(a)]. given #22 (F,wt=21): 59 C * (A @ B) * (D @ (F @ G)) * x != (A @ B) * C * x # answer(A). [ur(8,b,49,a),rewrite(3(11),3(18))]. given #23 (F,wt=21): 61 x * C * (A @ B) * (D @ (F @ G)) != x * (A @ B) * C # answer(A). [ur(1,b,49,a)]. given #24 (T,wt=6): 86 x != y | y = x. [para(9(a,1),10(a,2)),rewrite(65(2),75(4),9(3))]. given #25 (T,wt=9): 74 x * ((y @ y) @ x) = x. [para(65(a,1),4(a,1,2)),rewrite(65(5))]. given #26 (A,wt=14): 11 x * y * (y @ z) != y * z | z = x. [para(4(a,1),2(a,1)),flip(a)]. given #27 (F,wt=21): 62 (F @ G) * D * ((A @ B) @ C) * x != D * (F @ G) * x # answer(A). [ur(8,b,50,a),rewrite(3(11),3(18))]. given #28 (F,wt=21): 64 x * (F @ G) * D * ((A @ B) @ C) != x * D * (F @ G) # answer(A). [ur(1,b,50,a)]. given #29 (T,wt=9): 80 x * (x @ x * x) = x. [hyper(10,a,3,a)]. given #30 (T,wt=9): 92 (x @ x) @ y = y @ y. [hyper(29,a,74,a),flip(a)]. given #31 (A,wt=14): 12 x * y * (y @ z) != y * z | x = z. [para(4(a,1),2(a,2))]. given #32 (F,wt=21): 91 C * (A @ B) * (D @ (F @ G)) * (C @ C) != (A @ B) * C # answer(A). [para(9(a,1),59(a,2,2))]. given #33 (F,wt=21): 98 (D @ (F @ G)) * ((x @ x) @ ((A @ B) @ C)) != (A @ B) @ C # answer(A). [para(74(a,1),23(a,1)),flip(a)]. given #34 (T,wt=9): 119 x @ x * x = x @ x. [hyper(29,a,80,a),flip(a)]. given #35 (T,wt=9): 121 ((x @ x) @ y) * z = z. [para(92(a,2),65(a,1,1))]. given #36 (A,wt=15): 13 x * y * (y @ x) * z = y * x * z. [para(4(a,1),3(a,1,1)),rewrite(3(2),3(5)),flip(a)]. given #37 (F,wt=21): 99 ((A @ B) @ C) * ((x @ x) @ (D @ (F @ G))) != D @ (F @ G) # answer(A). [para(74(a,1),23(a,2))]. given #38 (F,wt=23): 26 (D @ (F @ G)) * x * (x @ ((A @ B) @ C)) != x * ((A @ B) @ C) # answer(A). [para(4(a,1),23(a,1)),flip(a)]. given #39 (T,wt=10): 73 x * y != y | z @ z = x. [para(65(a,1),2(a,1)),flip(a)]. NOTE: New constant: x @ x = c_0. [new_symbol(167)]. NOTE: New Function symbol precedence: lex([ A, B, C, D, F, G, c_0, *, @ ]). given #40 (T,wt=5): 171 x @ x = c_0. [new_symbol(167)]. given #41 (A,wt=17): 14 x * y * z * (z @ x * y) = z * x * y. [para(4(a,1),3(a,1)),flip(a)]. given #42 (F,wt=23): 27 ((A @ B) @ C) * x * (x @ (D @ (F @ G))) != x * (D @ (F @ G)) # answer(A). [para(4(a,1),23(a,2))]. given #43 (F,wt=23): 40 x * y * z * ((A @ B) @ C) != x * y * z * (D @ (F @ G)) # answer(A). [ur(7,b,24,a)]. given #44 (T,wt=5): 175 c_0 @ x = c_0. [back_rewrite(166),rewrite(171(1),171(3))]. given #45 (T,wt=5): 181 c_0 * x = x. [back_rewrite(141),rewrite(171(1),175(2),175(2))]. given #46 (A,wt=17): 15 x * y * z * (y * z @ x) = y * z * x. [para(3(a,1),4(a,1,2)),rewrite(3(7))]. given #47 (F,wt=23): 41 x * y * ((A @ B) @ C) * z != x * y * (D @ (F @ G)) * z # answer(A). [ur(7,b,23,a)]. given #48 (F,wt=23): 47 x * (D @ (F @ G)) * (((A @ B) @ C) @ x) != ((A @ B) @ C) * x # answer(A). [para(4(a,1),25(a,1)),flip(a)]. given #49 (T,wt=5): 191 x * c_0 = x. [back_rewrite(122),rewrite(171(1),175(2),175(2))]. given #50 (T,wt=7): 192 x @ x * x = c_0. [back_rewrite(119),rewrite(171(3))]. given #51 (A,wt=22): 16 x * y * z * y * x != y * u | x * z * x * y = u. [para(5(a,1),1(a,1))]. given #52 (F,wt=19): 221 (D @ (F @ G)) * (((A @ B) @ C) @ c_0) != (A @ B) @ C # answer(A). [para(181(a,1),47(a,1)),rewrite(191(20))]. given #53 (F,wt=23): 48 x * ((A @ B) @ C) * ((D @ (F @ G)) @ x) != (D @ (F @ G)) * x # answer(A). [para(4(a,1),25(a,2))]. given #54 (T,wt=7): 196 x * (x @ c_0) = x. [back_rewrite(188),rewrite(191(5))]. given #55 (T,wt=8): 184 x * y != x | c_0 = y. [back_rewrite(137),rewrite(171(3),175(4),175(4))]. given #56 (A,wt=22): 17 x * y * z * y * u != y * u * z * u * y | u = x. [para(5(a,1),2(a,1)),flip(a)]. given #57 (F,wt=23): 90 C * (A @ B) * (D @ (F @ G)) * (C @ (A @ B)) != C * (A @ B) # answer(A). [para(4(a,1),59(a,2))]. given #58 (F,wt=23): 116 (F @ G) * D * ((A @ B) @ C) * ((F @ G) @ D) != (F @ G) * D # answer(A). [para(4(a,1),62(a,2))]. given #59 (T,wt=5): 246 x @ c_0 = c_0. [hyper(184,a,196,a),flip(a)]. given #60 (T,wt=8): 187 x * y != y | c_0 = x. [back_rewrite(132),rewrite(171(3),175(4))]. given #61 (A,wt=22): 18 x * y * z * y * u != y * u * z * u * y | x = u. [para(5(a,1),2(a,2))]. given #62 (F,wt=25): 60 x * y * C * (A @ B) * (D @ (F @ G)) != x * y * (A @ B) * C # answer(A). [ur(7,b,49,a)]. given #63 (F,wt=21): 258 B * A * C * (A @ B) * (D @ (F @ G)) != A * B * C # answer(A). [para(13(a,1),60(a,2))]. given #64 (T,wt=9): 210 x * (x * x @ x) = x. [hyper(7,a,15,a)]. given #65 (T,wt=7): 261 x * x @ x = c_0. [hyper(184,a,210,a),flip(a)]. given #66 (A,wt=23): 19 x * y * z * y * x * u = y * x * z * x * y * u. [para(5(a,1),3(a,1,1)),rewrite(3(5),3(4),3(3),3(2),3(9),3(8),3(7))]. given #67 (F,wt=25): 63 x * y * (F @ G) * D * ((A @ B) @ C) != x * y * D * (F @ G) # answer(A). [ur(7,b,50,a)]. given #68 (F,wt=21): 272 F * G * D * ((A @ B) @ C) != G * F * D * (F @ G) # answer(A). [para(13(a,1),63(a,1))]. given #69 (T,wt=10): 111 x * y != y * y | y = x. [para(9(a,1),11(a,1,2))]. given #70 (T,wt=12): 182 x * (x @ y) != x * y | c_0 = y. [back_rewrite(140),rewrite(171(5),175(6))]. given #71 (A,wt=23): 20 x * y * z * u * z * y = x * z * y * u * y * z. [para(5(a,1),3(a,2,2)),rewrite(3(5))]. given #72 (F,wt=25): 88 x * C * (A @ B) * (D @ (F @ G)) * y != x * (A @ B) * C * y # answer(A). [ur(1,b,59,a)]. given #73 (F,wt=25): 89 C * (A @ B) * (D @ (F @ G)) * x * (x @ C) != (A @ B) * x * C # answer(A). [para(4(a,1),59(a,2,2))]. given #74 (T,wt=12): 185 x * y * z != z | x * y = c_0. [back_rewrite(136),rewrite(171(4),175(5)),flip(b)]. given #75 (T,wt=12): 193 x * y != y | x * (x @ y) = c_0. [back_rewrite(106),rewrite(171(3),175(4)),flip(b)]. given #76 (A,wt=23): 21 x * y * z * u * y * x = y * x * z * u * x * y. [para(3(a,1),5(a,1,2,2)),rewrite(3(8))]. given #77 (F,wt=25): 114 x * (F @ G) * D * ((A @ B) @ C) * y != x * D * (F @ G) * y # answer(A). [ur(1,b,62,a)]. given #78 (F,wt=25): 115 D * (F @ G) * (((A @ B) @ C) @ D) != (F @ G) * ((A @ B) @ C) * D # answer(A). [para(4(a,1),62(a,1,2)),flip(a)]. given #79 (T,wt=12): 194 x * y * z != x * y | c_0 = z. [back_rewrite(100),rewrite(171(5),175(6))]. given #80 (T,wt=12): 281 x @ y != x * y | y * x = c_0. [para(4(a,1),185(a,1)),flip(a)]. given #81 (A,wt=23): 22 x * (x @ y) * y * (x @ y) * x = (x @ y) * x * x * y. [para(4(a,1),5(a,1,2,2)),flip(a)]. given #82 (F,wt=25): 209 (F @ G) * ((A @ B) @ C) * D * (D @ (D @ (F @ G))) != D * (F @ G) # answer(A). [ur(10,b,27,a(flip))]. given #83 (F,wt=25): 259 B * A * C * (A @ B) * (D @ (F @ G)) * x != A * B * C * x # answer(A). [ur(8,b,258,a),rewrite(3(15),3(14),3(13),3(22),3(21))]. given #84 (T,wt=12): 299 x * y != y * x | x @ y = c_0. [para(4(a,1),194(a,1)),flip(b)]. given #85 (T,wt=13): 81 x * y * (x * y @ x) = y * x. [hyper(10,a,3,a(flip)),rewrite(3(4))]. given #86 (A,wt=18): 42 x * y * z * u != x * y * z * v | u = v. [para(3(a,1),7(a,1,2)),rewrite(3(5))]. given #87 (F,wt=25): 260 x * B * A * C * (A @ B) * (D @ (F @ G)) != x * A * B * C # answer(A). [ur(1,b,258,a)]. given #88 (F,wt=25): 273 F * G * D * ((A @ B) @ C) * x != G * F * D * (F @ G) * x # answer(A). [ur(8,b,272,a),rewrite(3(11),3(10),3(22),3(21),3(20))]. given #89 (T,wt=13): 189 x * y @ x * y * x * y = c_0. [back_rewrite(129),rewrite(171(8))]. given #90 (T,wt=13): 197 x * y * (y @ y * x) = y * x. [hyper(1,a,14,a)]. given #91 (A,wt=18): 43 x * y * z != x * u * y | u * (u @ y) = z. [para(4(a,1),7(a,1,2)),flip(a)]. given #92 (F,wt=23): 349 F * G * D * ((A @ B) @ C) * ((F @ G) @ D) != F * G * D # answer(A). [para(4(a,1),273(a,2,2,2)),rewrite(13(26))]. given #93 (F,wt=25): 274 x * F * G * D * ((A @ B) @ C) != x * G * F * D * (F @ G) # answer(A). [ur(1,b,272,a)]. given #94 (T,wt=10): 372 x * y != x * z | z = y. [para(181(a,1),43(a,1,2)),rewrite(191(3),246(5),191(5))]. given #95 (T,wt=13): 263 x * y * x * y @ x * y = c_0. [para(3(a,1),261(a,1,1))]. given #96 (A,wt=14): 44 x * y * z != y * x | y @ x = z. [para(4(a,1),7(a,1)),flip(a)]. given #97 (F,wt=25): 317 B * A * C * (A @ B) * (D @ (F @ G)) * (C @ B) != A * C * B # answer(A). [para(4(a,1),259(a,2,2))]. given #98 (F,wt=25): 327 x * (D @ (F @ G)) * (x * ((A @ B) @ C) @ x) != ((A @ B) @ C) * x # answer(A). [para(81(a,1),25(a,1)),flip(a)]. given #99 (T,wt=12): 384 x * y != y * x | y @ x = c_0. [para(191(a,1),44(a,1,2))]. given #100 (T,wt=13): 322 x * (y * x @ y) = x * (x @ y). [hyper(10,a,81,a),flip(a)]. given #101 (A,wt=22): 45 x * y * z * y * x != y * x * u | z * x * y = u. [para(5(a,1),7(a,1))]. given #102 (F,wt=25): 357 C * (A @ B) * (D @ (F @ G)) * (C @ C * (A @ B)) != C * (A @ B) # answer(A). [para(197(a,1),59(a,2))]. given #103 (F,wt=9): 385 x * y @ x = y @ x. [hyper(372,a,322,a),flip(a)]. given #104 (T,wt=11): 396 (x @ y) * y * x = x * y. [hyper(45,a,13,a)]. given #105 (T,wt=9): 458 (x @ y) @ y * x = c_0. [para(396(a,1),299(a,1)),rewrite(3(4),4(4)),xx(a)]. given #106 (A,wt=18): 52 x * y * z * u != v * u | x * y * z = v. [para(3(a,1),8(a,1,2))]. given #107 (F,wt=17): 419 (D @ (F @ G)) * C * (A @ B) != (A @ B) * C # answer(A). [para(396(a,1),23(a,1)),flip(a)]. given #108 (F,wt=17): 420 ((A @ B) @ C) * (F @ G) * D != D * (F @ G) # answer(A). [para(396(a,1),23(a,2))]. given #109 (T,wt=9): 459 y * x @ (x @ y) = c_0. [para(396(a,1),299(a,2)),rewrite(3(3),4(3)),xx(a)]. given #110 (T,wt=9): 471 x * y @ (x @ y) = c_0. [para(396(a,1),385(a,1,1)),rewrite(459(6))]. given #111 (A,wt=18): 53 x * y * z != u * v * z | x * y = u * v. [para(3(a,1),8(a,2))]. given #112 (F,wt=21): 424 x * (D @ (F @ G)) * C * (A @ B) != x * (A @ B) * C # answer(A). [para(396(a,1),25(a,1,2)),flip(a)]. given #113 (F,wt=21): 426 x * ((A @ B) @ C) * (F @ G) * D != x * D * (F @ G) # answer(A). [para(396(a,1),25(a,2,2))]. given #114 (T,wt=9): 480 x * y @ y * x = c_0. [para(458(a,1),385(a,2)),rewrite(3(3),4(3))]. given #115 (T,wt=11): 473 (x * y @ y) @ x * y = c_0. [para(4(a,1),458(a,1,2)),rewrite(401(3))]. given #116 (A,wt=18): 54 x * y * (y @ z) != u * y * z | u * z = x. [para(4(a,1),8(a,1,2)),flip(a)]. given #117 (F,wt=21): 440 (F @ G) * D * ((A @ B) @ C) * G * F != D * F * G # answer(A). [para(396(a,1),62(a,2,2))]. given #118 (F,wt=21): 497 (D @ (F @ G)) * C * (A @ B) * x != (A @ B) * C * x # answer(A). [ur(52,b,419,a),rewrite(3(18))]. given #119 (T,wt=10): 576 x * y != z * y | z = x. [para(191(a,1),54(a,2,2)),rewrite(246(2),191(2),191(5))]. given #120 (T,wt=11): 481 (x @ y) @ y * y * x = c_0. [para(385(a,1),458(a,1,1))]. given #121 (A,wt=14): 55 x * (y @ z) != y * z | z * y = x. [para(4(a,1),8(a,1)),flip(a)]. given #122 (F,wt=21): 498 ((A @ B) @ C) * (F @ G) * D * x != D * (F @ G) * x # answer(A). [ur(52,b,420,a),rewrite(3(18))]. given #123 (F,wt=21): 586 (D @ (F @ G)) * C * A * B != (A @ B) * C * B * A # answer(A). [para(396(a,1),497(a,1,2,2))]. given #124 (T,wt=11): 500 x * y @ (x * y @ y) = c_0. [para(4(a,1),459(a,1,1)),rewrite(401(4))]. given #125 (T,wt=11): 507 x * x * y @ (y @ x) = c_0. [para(385(a,1),459(a,1,2))]. given #126 (A,wt=18): 56 x * y * z * (z @ u) != z * u | x * y = u. [para(4(a,1),8(a,2))]. given #127 (F,wt=21): 601 ((A @ B) @ C) * (F @ G) * D * G * F != D * F * G # answer(A). [para(396(a,1),498(a,2,2))]. given #128 (F,wt=21): 614 (D @ (F @ G)) * C * C * (A @ B) != C * (A @ B) * C # answer(A). [para(507(a,1),26(a,1,2,2)),rewrite(191(14),3(26),3(25),4(25))]. given #129 (T,wt=11): 525 x * y * x @ (y @ x) = c_0. [para(385(a,1),471(a,1,2)),rewrite(3(2))]. given #130 (T,wt=11): 642 x * y * y @ (x @ y) = c_0. [para(525(a,1),385(a,2)),rewrite(416(4))]. given #131 (A,wt=22): 57 x * y * z * y * x != u * z * x * y | y * x = u. [para(5(a,1),8(a,1))]. given #132 (F,wt=23): 425 (x @ ((A @ B) @ C)) * (D @ (F @ G)) * x != x * ((A @ B) @ C) # answer(A). [para(396(a,1),25(a,1)),flip(a)]. given #133 (F,wt=23): 427 (x @ (D @ (F @ G))) * ((A @ B) @ C) * x != x * (D @ (F @ G)) # answer(A). [para(396(a,1),25(a,2))]. given #134 (T,wt=12): 392 x * (x @ y) != x | x @ y = c_0. [para(322(a,1),184(a,1)),rewrite(385(6)),flip(b)]. given #135 (T,wt=12): 450 x * y != x | (x @ y) * y = c_0. [para(396(a,1),185(a,1))]. given #136 (A,wt=15): 69 x * y * y * x = y * x * x * y. [para(32(a,1),5(a,1,2)),rewrite(65(6))]. given #137 (F,wt=23): 428 (((A @ B) @ C) @ x) * x * (D @ (F @ G)) != ((A @ B) @ C) * x # answer(A). [para(396(a,1),28(a,1)),flip(a)]. given #138 (F,wt=23): 429 ((D @ (F @ G)) @ x) * x * ((A @ B) @ C) != (D @ (F @ G)) * x # answer(A). [para(396(a,1),28(a,2))]. given #139 (T,wt=12): 456 (x @ y) * y != x * y | c_0 = x. [para(396(a,1),194(a,1)),flip(a)]. given #140 (T,wt=13): 352 x * (x @ x * y) = x * (x @ y). [hyper(10,a,197,a),flip(a)]. given #141 (A,wt=20): 82 x * y * z != u * x * y | u * (u @ x * y) = z. [para(3(a,1),10(a,1))]. given #142 (F,wt=23): 435 (A @ B) * C * (F @ G) * D != C * (A @ B) * D * (F @ G) # answer(A). [para(396(a,1),59(a,1,2,2)),flip(a)]. given #143 (F,wt=23): 439 (F @ G) * D * (A @ B) * C != D * (F @ G) * C * (A @ B) # answer(A). [para(396(a,1),62(a,1,2,2))]. given #144 (T,wt=9): 716 x @ x * y = x @ y. [hyper(372,a,352,a),flip(a)]. given #145 (T,wt=9): 756 (x @ y) @ x * y = c_0. [para(396(a,1),716(a,1,2)),rewrite(458(6))]. given #146 (A,wt=20): 83 x * y * z != z * u | x * y * (x * y @ z) = u. [para(3(a,1),10(a,2)),rewrite(3(8)),flip(a)]. given #147 (F,wt=23): 515 (A @ B) * C * ((A @ B) @ C) != (D @ (F @ G)) * (A @ B) * C # answer(A). [para(471(a,1),26(a,1,2,2)),rewrite(191(12),3(22)),flip(a)]. given #148 (F,wt=23): 517 ((A @ B) @ C) * D * (F @ G) != D * (F @ G) * (D @ (F @ G)) # answer(A). [para(471(a,1),27(a,1,2,2)),rewrite(191(12),3(22))]. given #149 (T,wt=11): 757 (x @ y) @ x * y * x = c_0. [para(716(a,1),458(a,1,1)),rewrite(3(3))]. given #150 (T,wt=11): 758 x * y * x @ (x @ y) = c_0. [para(716(a,1),459(a,1,2)),rewrite(3(2))]. given #151 (A,wt=18): 84 x * y != z * y | z * (z @ y) = x * (x @ y). [para(4(a,1),10(a,1))]. given #152 (F,wt=21): 817 ((A @ B) @ C) * D * (F @ G) * D != D * D * (F @ G) # answer(A). [para(758(a,1),27(a,1,2,2)),rewrite(191(14),3(26),3(25),4(25))]. given #153 (F,wt=23): 526 (F @ G) * D * ((F @ G) @ D) * ((A @ B) @ C) != (F @ G) * D # answer(A). [back_rewrite(441),rewrite(513(17))]. given #154 (T,wt=11): 759 x * x * y @ (x @ y) = c_0. [para(716(a,1),471(a,1,2))]. given #155 (T,wt=11): 772 x * y @ (y @ x * y) = c_0. [back_rewrite(510),rewrite(745(4))]. given #156 (A,wt=20): 109 x * y * z * (y * z @ u) != y * z * u | u = x. [para(3(a,1),11(a,1,2)),rewrite(3(7))]. given #157 (F,wt=23): 527 C * (A @ B) * (C @ (A @ B)) * (D @ (F @ G)) != C * (A @ B) # answer(A). [back_rewrite(436),rewrite(513(17))]. given #158 (F,wt=23): 541 (C @ (A @ B)) * (D @ (F @ G)) * C * (A @ B) != C * (A @ B) # answer(A). [para(396(a,1),424(a,2))]. given #159 (T,wt=11): 782 (x @ y * x) @ y * x = c_0. [para(4(a,1),756(a,1,2)),rewrite(745(3))]. given #160 (T,wt=11): 790 (x @ y) @ y * x * y = c_0. [para(385(a,1),756(a,1,1)),rewrite(3(3))]. given #161 (A,wt=20): 126 x * y * z * (y * z @ u) != y * z * u | x = u. [para(3(a,1),12(a,1,2)),rewrite(3(7))]. given #162 (F,wt=21): 886 C * (A @ B) * C * (D @ (F @ G)) != (A @ B) * C * C # answer(A). [para(790(a,1),47(a,1,2,2)),rewrite(191(14),3(13),3(12),416(26))]. given #163 (F,wt=23): 543 ((F @ G) @ D) * ((A @ B) @ C) * (F @ G) * D != (F @ G) * D # answer(A). [para(396(a,1),426(a,2))]. given #164 (T,wt=11): 794 (x @ y) @ x * x * y = c_0. [para(716(a,1),756(a,1,1))]. given #165 (T,wt=11): 849 x * (y @ x) * y = y * x. [para(772(a,1),4(a,1,2,2)),rewrite(191(5),528(4),3(5),734(4)),flip(a)]. given #166 (A,wt=18): 143 x * y * z != y * u | x * (x @ y) * z = u. [para(13(a,1),1(a,1))]. given #167 (F,wt=17): 912 C * (D @ (F @ G)) * (A @ B) != (A @ B) * C # answer(A). [para(849(a,1),25(a,1)),flip(a)]. given #168 (F,wt=17): 913 (F @ G) * ((A @ B) @ C) * D != D * (F @ G) # answer(A). [para(849(a,1),25(a,2))]. given #169 (T,wt=11): 857 x * y @ (x @ y * x) = c_0. [para(772(a,1),385(a,2)),rewrite(528(4))]. given #170 (T,wt=11): 878 (x @ y * x) @ x * y = c_0. [para(782(a,1),716(a,2)),rewrite(528(6))]. given #171 (A,wt=18): 144 x * y * (y @ z) * u != y * z * u | z = x. [para(13(a,1),2(a,1)),flip(a)]. given #172 (F,wt=21): 919 x * C * (D @ (F @ G)) * (A @ B) != x * (A @ B) * C # answer(A). [para(849(a,1),41(a,1,2)),flip(a)]. given #173 (F,wt=21): 920 x * (F @ G) * ((A @ B) @ C) * D != x * D * (F @ G) # answer(A). [para(849(a,1),41(a,2,2))]. given #174 (T,wt=11): 892 (x @ y) @ x * y * y = c_0. [para(790(a,1),716(a,2)),rewrite(416(5))]. given #175 (T,wt=11): 908 (x @ y) * x = x * (x @ y). [hyper(10,a,849,a),flip(a)]. given #176 (A,wt=18): 145 x * y * (y @ z) * u != y * z * u | x = z. [para(13(a,1),2(a,2))]. given #177 (F,wt=15): 1039 ((A @ B) @ C) * D != D * (D @ (F @ G)) # answer(A). [para(908(a,1),23(a,2))]. given #178 (F,wt=19): 1038 (A @ B) * ((A @ B) @ C) != (D @ (F @ G)) * (A @ B) # answer(A). [para(908(a,1),23(a,1))]. given #179 (T,wt=7): 1032 x @ (x @ y) = c_0. [hyper(384,a,908,a)]. given #180 (T,wt=7): 1033 (x @ y) @ x = c_0. [hyper(299,a,908,a)]. given #181 (A,wt=21): 146 x * y * z * (z @ x * y) * u = z * x * y * u. [para(13(a,1),3(a,1)),rewrite(3(2)),flip(a)]. given #182 (F,wt=19): 1045 x * ((A @ B) @ C) * D != x * D * (D @ (F @ G)) # answer(A). [para(908(a,1),25(a,2,2))]. given #183 (F,wt=19): 1114 ((A @ B) @ C) * D * x != D * (D @ (F @ G)) * x # answer(A). [ur(576,b,1039,a),rewrite(3(8),3(16)),flip(a)]. given #184 (T,wt=11): 961 x * (x @ y) * (y @ x) = x. [hyper(143,a,4,a)]. given #185 (T,wt=9): 1148 (x @ y) * (y @ x) = c_0. [hyper(184,a,961,a),flip(a)]. given #186 (A,wt=21): 147 x * y * z * (y * z @ x) * u = y * z * x * u. [para(3(a,1),13(a,1,2)),rewrite(3(9))]. given #187 (F,wt=13): 1186 (D @ (F @ G)) * (C @ (A @ B)) != c_0 # answer(A). [para(1148(a,1),23(a,1)),flip(a)]. given #188 (F,wt=13): 1187 ((A @ B) @ C) * ((F @ G) @ D) != c_0 # answer(A). [para(1148(a,1),23(a,2))]. given #189 (T,wt=9): 1222 (x @ y) @ (y @ x) = c_0. [para(1148(a,1),299(a,1)),rewrite(1148(4)),xx(a)]. given #190 (T,wt=10): 1212 x @ y != c_0 | y @ x = c_0. [para(1148(a,1),184(a,1)),flip(a),flip(b)]. given #191 (A,wt=21): 148 x * y * z * (z @ (x @ y)) = y * x * z * (x @ y). [para(4(a,1),13(a,1,2,2)),flip(a)]. given #192 (F,wt=13): 1188 (C @ (A @ B)) * (D @ (F @ G)) != c_0 # answer(A). [para(1148(a,1),24(a,1)),flip(a)]. given #193 (F,wt=13): 1189 ((F @ G) @ D) * ((A @ B) @ C) != c_0 # answer(A). [para(1148(a,1),24(a,2))]. given #194 (T,wt=11): 1067 x * (x @ y) @ (x @ y) = c_0. [para(908(a,1),385(a,1,1)),rewrite(1032(6))]. given #195 (T,wt=11): 1075 (x @ y) @ x * (x @ y) = c_0. [para(908(a,1),716(a,1,2)),rewrite(1033(6))]. given #196 (A,wt=22): 153 x * y * z * u != x * z * v | y * (y @ z) * u = v. [para(13(a,1),7(a,1,2))]. given #197 (F,wt=15): 1182 ((A @ B) @ C) * D * ((F @ G) @ D) != D # answer(A). [para(961(a,1),1114(a,2))]. given #198 (F,wt=15): 1191 x * (D @ (F @ G)) * (C @ (A @ B)) != x # answer(A). [para(1148(a,1),25(a,1,2)),rewrite(191(2)),flip(a)]. given #199 (T,wt=11): 1185 (x @ y) * (y @ x) * z = z. [para(1148(a,1),3(a,1,1)),rewrite(181(2)),flip(a)]. given #200 (T,wt=9): 1404 ((x @ y) @ z) @ z = c_0. [para(1185(a,1),756(a,1,2)),rewrite(1403(4))]. given #201 (A,wt=18): 154 x * y * z != y * x * u | (x @ y) * z = u. [para(13(a,1),7(a,1))]. given #202 (F,wt=11): 1424 (F @ G) @ D != C @ (A @ B) # answer(A). [para(1185(a,1),1191(a,1)),flip(a)]. given #203 (F,wt=15): 1192 x * ((A @ B) @ C) * ((F @ G) @ D) != x # answer(A). [para(1148(a,1),25(a,2,2)),rewrite(191(14))]. given #204 (T,wt=9): 1430 x @ ((y @ z) @ x) = c_0. [back_rewrite(1385),rewrite(1403(4))]. given #205 (T,wt=11): 1248 (x @ y) * y * (y @ x) = y. [back_rewrite(1149),rewrite(1185(4)),flip(a)]. given #206 (A,wt=18): 155 x * y * z != y * x * u | (y @ x) * u = z. [para(13(a,1),7(a,2)),flip(b)]. given #207 (F,wt=15): 1193 x * (C @ (A @ B)) * (D @ (F @ G)) != x # answer(A). [para(1148(a,1),28(a,1,2)),rewrite(191(2)),flip(a)]. given #208 (F,wt=15): 1194 x * ((F @ G) @ D) * ((A @ B) @ C) != x # answer(A). [para(1148(a,1),28(a,2,2)),rewrite(191(14))]. given #209 (T,wt=7): 1526 x @ (y @ x) = c_0. [para(1248(a,1),385(a,1,1)),rewrite(1517(6))]. given #210 (T,wt=7): 1538 (x @ y) @ y = c_0. [para(1248(a,1),716(a,1,2)),rewrite(1516(6))]. given #211 (A,wt=22): 156 x * y * (y @ z) * u != v * y * z * u | v * z = x. [para(13(a,1),8(a,1,2)),flip(a)]. given #212 (F,wt=15): 1275 (D @ (F @ G)) * (C @ (A @ B)) * x != x # answer(A). [ur(576,b,1186,a),rewrite(181(2),3(12)),flip(a)]. given #213 (F,wt=15): 1278 ((A @ B) @ C) * ((F @ G) @ D) * x != x # answer(A). [ur(576,b,1187,a),rewrite(181(2),3(12)),flip(a)]. given #214 (T,wt=10): 1499 x * y != x | y @ x = y. [para(1248(a,1),11(a,1)),flip(a),flip(b)]. given #215 (T,wt=11): 1516 (y @ x) @ x * (x @ y) = c_0. [para(1248(a,1),299(a,1)),rewrite(3(4),1148(3),191(2)),xx(a)]. given #216 (A,wt=18): 157 x * (y @ z) * u != y * z * u | z * y = x. [para(13(a,1),8(a,1)),flip(a)]. given #217 (F,wt=15): 1304 (C @ (A @ B)) * (D @ (F @ G)) * x != x # answer(A). [ur(576,b,1188,a),rewrite(181(2),3(12)),flip(a)]. given #218 (F,wt=15): 1307 ((F @ G) @ D) * ((A @ B) @ C) * x != x # answer(A). [ur(576,b,1189,a),rewrite(181(2),3(12)),flip(a)]. given #219 (T,wt=11): 1517 x * (x @ y) @ (y @ x) = c_0. [para(1248(a,1),299(a,2)),rewrite(3(4),1148(3),191(2)),xx(a)]. given #220 (T,wt=11): 1552 (x @ y) * y = y * (x @ y). [para(1526(a,1),4(a,1,2,2)),rewrite(191(3))]. given #221 (A,wt=22): 158 x * y * z * (z @ u) * v != z * u * v | x * y = u. [para(13(a,1),8(a,2))]. given #222 (F,wt=15): 1421 (C @ (A @ B)) * D * (D @ (F @ G)) != D # answer(A). [para(1185(a,1),1045(a,1)),flip(a)]. given #223 (F,wt=15): 1469 ((F @ G) @ D) * x != (C @ (A @ B)) * x # answer(A). [ur(576,b,1424,a),flip(a)]. given #224 (T,wt=11): 1557 x * (y @ x) @ (y @ x) = c_0. [para(1526(a,1),385(a,2)),rewrite(1552(2))]. given #225 (T,wt=11): 1579 (x @ y) @ y * (x @ y) = c_0. [para(1538(a,1),716(a,2)),rewrite(1552(3))]. given #226 (A,wt=22): 160 x * y * z != u * y | u * (u @ y) = x * (x @ y) * z. [para(13(a,1),10(a,1))]. given #227 (F,wt=15): 1470 x * ((F @ G) @ D) != x * (C @ (A @ B)) # answer(A). [ur(372,b,1424,a),flip(a)]. given #228 (F,wt=15): 1478 C * ((A @ B) @ C) != (D @ (F @ G)) * C # answer(A). [para(1430(a,1),26(a,1,2,2)),rewrite(191(8)),flip(a)]. given #229 (T,wt=12): 927 x * y != x | y * (x @ y) = c_0. [para(849(a,1),185(a,1))]. given #230 (T,wt=12): 931 x * (y @ x) != y * x | c_0 = y. [para(849(a,1),194(a,1)),flip(a)]. given #231 (A,wt=25): 163 x * y * z * (z @ (x @ y)) * u = y * x * z * (x @ y) * u. [para(13(a,1),13(a,1,2,2)),flip(a)]. given #232 (F,wt=15): 1486 (D @ (F @ G)) * C * (C @ (A @ B)) != C # answer(A). [para(1248(a,1),23(a,1)),flip(a)]. given #233 (F,wt=15): 1660 ((F @ G) @ D) * C * ((A @ B) @ C) != C # answer(A). [para(1552(a,1),1307(a,1,2))]. given #234 (T,wt=12): 1183 (x @ y) * z != c_0 | y @ x = z. [para(1148(a,1),1(a,1)),flip(a)]. given #235 (T,wt=12): 1184 x * (y @ z) != c_0 | z @ y = x. [para(1148(a,1),2(a,1)),flip(a)]. given #236 (A,wt=16): 172 x * (x @ y) * z != x * y * z | c_0 = y. [back_rewrite(170),rewrite(171(7))]. given #237 (F,wt=15): 1680 ((F @ G) @ D) * C != C * (C @ (A @ B)) # answer(A). [para(908(a,1),1469(a,2))]. given #238 (F,wt=15): 1681 D * ((F @ G) @ D) != (C @ (A @ B)) * D # answer(A). [para(1552(a,1),1469(a,1))]. given #239 (T,wt=12): 1216 x @ y != z | z * (y @ x) = c_0. [para(1148(a,1),185(a,1,2)),rewrite(191(2)),flip(a)]. given #240 (T,wt=12): 1220 x * (y @ z) != x | z @ y = c_0. [para(1148(a,1),194(a,1,2)),rewrite(191(2)),flip(a),flip(b)]. given #241 (A,wt=20): 174 x * y * z * y * x != x * z * x * y | c_0 = y. [back_rewrite(168),rewrite(171(9))]. given #242 (F,wt=17): 1199 (A @ B) * C * ((F @ G) @ D) != C * (A @ B) # answer(A). [para(1148(a,1),59(a,1,2,2)),rewrite(191(6)),flip(a)]. given #243 (F,wt=17): 1201 D * (F @ G) * (C @ (A @ B)) != (F @ G) * D # answer(A). [para(1148(a,1),62(a,1,2,2)),rewrite(191(6)),flip(a)]. given #244 (T,wt=12): 1232 x * y != c_0 | y @ x = y * x. [para(1148(a,1),55(a,1)),flip(a),flip(b)]. given #245 (T,wt=12): 1355 x @ y != z | (y @ x) * z = c_0. [para(1185(a,1),184(a,1)),flip(a),flip(b)]. given #246 (A,wt=16): 179 x * y * z != y | x * (x @ y) * z = c_0. [back_rewrite(152),rewrite(171(4)),flip(b)]. given #247 (F,wt=17): 1202 (F @ G) * D * ((A @ B) @ C) * (G @ F) != D # answer(A). [para(1148(a,1),62(a,2,2)),rewrite(191(18))]. given #248 (F,wt=17): 1231 (D @ (F @ G)) * C != (A @ B) * C * (B @ A) # answer(A). [para(1148(a,1),497(a,1,2,2)),rewrite(191(8))]. given #249 (T,wt=12): 1356 (x @ y) * z != z | y @ x = c_0. [para(1185(a,1),187(a,1)),flip(a),flip(b)]. given #250 (T,wt=12): 1556 x * (y @ x) != x | y @ x = c_0. [para(1526(a,1),182(a,1,2)),rewrite(191(2)),flip(a),flip(b)]. given #251 (A,wt=20): 195 x * y * z * y * x != y | x * z * x * y = c_0. [back_rewrite(39),rewrite(171(6)),flip(b)]. given #252 (F,wt=17): 1233 ((A @ B) @ C) * (F @ G) * D * (G @ F) != D # answer(A). [para(1148(a,1),498(a,2,2)),rewrite(191(18))]. given #253 (F,wt=17): 1345 (B @ A) * C * (A @ B) * (D @ (F @ G)) != C # answer(A). [para(1185(a,1),61(a,2))]. given #254 (T,wt=12): 1719 c_0 != x | (y @ z) * x = y @ z. [para(1185(a,1),1183(a,1)),flip(a),flip(b)]. given #255 (T,wt=12): 1776 x * y * z != x | y * z = c_0. [para(13(a,1),179(a,1)),rewrite(1185(7))]. given #256 (A,wt=23): 201 x * y * z * u * (u @ x * y * z) = u * x * y * z. [para(14(a,1),3(a,1)),rewrite(3(2),3(5)),flip(a)]. given #257 (F,wt=17): 1350 D * ((A @ B) @ C) != (G @ F) * D * (F @ G) # answer(A). [para(1185(a,1),64(a,1))]. given #258 (F,wt=17): 1387 ((F @ G) @ D) * (A @ B) * C != C * (A @ B) # answer(A). [para(1185(a,1),424(a,1)),flip(a)]. given #259 (T,wt=12): 1799 (x @ y) * z != z | x @ y = c_0. [para(1185(a,1),1356(a,1)),flip(a)]. given #260 (T,wt=13): 401 x * (x @ y) @ y = x * y @ y. [para(4(a,1),385(a,1,1)),flip(a)]. given #261 (A,wt=23): 202 x * y * z * u * (z * u @ x * y) = z * u * x * y. [para(3(a,1),14(a,1,2,2)),rewrite(3(10))]. given #262 (F,wt=17): 1388 (B @ A) * (D @ (F @ G)) * C * (A @ B) != C # answer(A). [para(1185(a,1),424(a,2))]. given #263 (F,wt=17): 1389 (F @ G) * D != (C @ (A @ B)) * D * (F @ G) # answer(A). [para(1185(a,1),426(a,1))]. given #264 (T,wt=13): 472 (x @ y * z) @ y * z * x = c_0. [para(3(a,1),458(a,1,2))]. given #265 (T,wt=13): 499 x * y * z @ (z @ x * y) = c_0. [para(3(a,1),459(a,1,1))]. given #266 (A,wt=23): 207 x * y * z * (z @ x * (x @ y)) = y * z * x * (x @ y). [para(14(a,1),13(a,1,2)),flip(a)]. given #267 (F,wt=17): 1419 (B @ A) * C * (D @ (F @ G)) * (A @ B) != C # answer(A). [para(1185(a,1),919(a,2))]. given #268 (F,wt=17): 1420 ((A @ B) @ C) * D != (G @ F) * D * (F @ G) # answer(A). [para(1185(a,1),920(a,1))]. given #269 (T,wt=13): 508 x * y * z @ (x * y @ z) = c_0. [para(3(a,1),471(a,1,1))]. given #270 (T,wt=13): 524 x * y * (x @ y) @ (x @ y) = c_0. [para(471(a,1),385(a,2)),rewrite(509(3))]. given #271 (A,wt=23): 211 x * y * z * u * (y * z * u @ x) = y * z * u * x. [para(3(a,1),15(a,1,2,2,2,1)),rewrite(3(6),3(10))]. given #272 (F,wt=17): 1754 (A @ B) * ((F @ G) @ D) * C != C * (A @ B) # answer(A). [ur(10,b,1680,a(flip))]. given #273 (F,wt=19): 1146 ((A @ B) @ C) * D * D != D * D * (D @ (F @ G)) # answer(A). [para(908(a,1),1114(a,2,2))]. given #274 (T,wt=13): 544 x * y * z @ z * x * y = c_0. [para(3(a,1),480(a,1,1))]. given #275 (T,wt=13): 545 x * y * z @ y * z * x = c_0. [para(3(a,1),480(a,1,2))]. given #276 (A,wt=24): 212 x * y * z * u != x * u * v | y * z * (y * z @ u) = v. [para(15(a,1),7(a,1,2))]. given #277 (F,wt=19): 1205 x * y * (C @ (A @ B)) * (D @ (F @ G)) != x * y # answer(A). [para(1148(a,1),40(a,1,2,2)),rewrite(191(2)),flip(a)]. given #278 (F,wt=19): 1206 x * y * ((F @ G) @ D) * ((A @ B) @ C) != x * y # answer(A). [para(1148(a,1),40(a,2,2,2)),rewrite(191(15))]. given #279 (T,wt=13): 595 (x @ y) @ y * y * y * x = c_0. [para(385(a,1),481(a,1,1))]. given #280 (T,wt=13): 619 x * x * x * y @ (y @ x) = c_0. [para(385(a,1),507(a,1,2))]. given #281 (A,wt=20): 213 x * y * z != z * x * u | y * (x * y @ z) = u. [para(15(a,1),7(a,1))]. given #282 (F,wt=19): 1207 x * y * (D @ (F @ G)) * (C @ (A @ B)) != x * y # answer(A). [para(1148(a,1),41(a,1,2,2)),rewrite(191(2)),flip(a)]. given #283 (F,wt=19): 1208 x * y * ((A @ B) @ C) * ((F @ G) @ D) != x * y # answer(A). [para(1148(a,1),41(a,2,2,2)),rewrite(191(15))]. given #284 (T,wt=13): 643 x * x * y * x @ (y @ x) = c_0. [para(385(a,1),525(a,1,2)),rewrite(3(2))]. given #285 (T,wt=13): 653 x * y * x * x @ (y @ x) = c_0. [para(385(a,1),642(a,1,2)),rewrite(3(3))]. given #286 (A,wt=24): 214 x * y * z * (y * z @ u) != v * y * z * u | v * u = x. [para(15(a,1),8(a,1,2)),flip(a)]. given #287 (F,wt=19): 1326 ((A @ B) @ C) * D * ((F @ G) @ D) * x != D * x # answer(A). [ur(576,b,1182,a),rewrite(3(16),3(15)),flip(a)]. given #288 (F,wt=19): 1327 x * ((A @ B) @ C) * D * ((F @ G) @ D) != x * D # answer(A). [ur(372,b,1182,a),flip(a)]. given #289 (T,wt=13): 745 x @ y * (y @ x) = x @ y * x. [para(4(a,1),716(a,1,2)),flip(a)]. given #290 (T,wt=13): 781 (x * y @ z) @ x * y * z = c_0. [para(3(a,1),756(a,1,2))]. given #291 (A,wt=20): 215 x * y * (z * y @ u) != z * y * u | u * z = x. [para(15(a,1),8(a,1)),flip(a)]. given #292 (F,wt=19): 1330 x * (D @ (F @ G)) * (C @ (A @ B)) * y != x * y # answer(A). [ur(576,b,1191,a),rewrite(3(14),3(13)),flip(a)]. given #293 (F,wt=19): 1339 x * ((A @ B) @ C) * ((F @ G) @ D) * y != x * y # answer(A). [para(1185(a,1),25(a,2,2))]. given #294 (T,wt=13): 793 (x @ y) @ x * y * (x @ y) = c_0. [para(756(a,1),716(a,2)),rewrite(509(4))]. given #295 (T,wt=13): 809 (x @ y) @ x * x * y * x = c_0. [para(716(a,1),757(a,1,1)),rewrite(3(3))]. given #296 (A,wt=24): 216 x * y * z * u * (z * u @ v) != z * u * v | x * y = v. [para(15(a,1),8(a,2))]. given #297 (F,wt=19): 1352 x * (C @ (A @ B)) * (D @ (F @ G)) * y != x * y # answer(A). [para(1185(a,1),41(a,1,2)),flip(a)]. given #298 (F,wt=19): 1354 x * ((F @ G) @ D) * ((A @ B) @ C) * y != x * y # answer(A). [para(1185(a,1),41(a,2,2))]. given #299 (T,wt=13): 823 x * x * y * x @ (x @ y) = c_0. [para(716(a,1),758(a,1,2)),rewrite(3(2))]. given #300 (T,wt=13): 838 x * x * x * y @ (x @ y) = c_0. [para(716(a,1),759(a,1,2))]. given #301 (A,wt=24): 217 x * y * z != u * z | u * (u @ z) = x * y * (x * y @ z). [para(15(a,1),10(a,1))]. given #302 (F,wt=19): 1474 x * y * ((F @ G) @ D) != x * y * (C @ (A @ B)) # answer(A). [ur(7,b,1424,a)]. given #303 (F,wt=19): 1487 ((A @ B) @ C) * (F @ G) * ((F @ G) @ D) != F @ G # answer(A). [para(1248(a,1),23(a,2))]. given #304 (T,wt=13): 888 (x @ y) @ y * y * x * y = c_0. [para(385(a,1),790(a,1,1)),rewrite(3(3))]. given #305 (T,wt=13): 905 (x @ y) @ x * x * x * y = c_0. [para(716(a,1),794(a,1,1))]. given #306 (A,wt=23): 218 x * y * z * ((x @ y) * z @ x) = y * (x @ y) * z * x. [para(15(a,1),13(a,1,2)),flip(a)]. given #307 (F,wt=19): 1490 x * (D @ (F @ G)) * C * (C @ (A @ B)) != x * C # answer(A). [para(1248(a,1),25(a,1,2)),flip(a)]. given #308 (F,wt=19): 1555 ((A @ B) @ C) * (F @ G) != (F @ G) * (D @ (F @ G)) # answer(A). [para(1526(a,1),27(a,1,2,2)),rewrite(191(10))]. given #309 (T,wt=13): 953 x * (x @ y * x) = x * (x @ y). [back_rewrite(734),rewrite(908(5))]. given #310 (T,wt=9): 2298 x @ y * x = x @ y. [hyper(372,a,953,a),flip(a)]. given #311 (A,wt=25): 223 x * y * z * z * (z @ y * x * y * z) = z * x * z * y. [hyper(16,a,14,a(flip)),rewrite(3(11),3(10)),flip(a)]. given #312 (F,wt=11): 2517 D @ (G @ F) != C @ (A @ B) # answer(A). [back_rewrite(1424),rewrite(2360(5))]. given #313 (F,wt=11): 2638 D @ (F @ G) != C @ (B @ A) # answer(A). [back_rewrite(6),rewrite(2360(5)),flip(a)]. given #314 (T,wt=9): 2344 x * y @ y = x @ y. [para(4(a,1),2298(a,1,2)),rewrite(2340(4),401(4)),flip(a)]. given #315 (T,wt=11): 2334 x @ y * (y @ x) = x @ y. [back_rewrite(745),rewrite(2298(5))]. given #316 (A,wt=19): 224 x * (x @ y) * z * y * x = x * z * x * y. [hyper(16,a,13,a(flip)),flip(a)]. given #317 (F,wt=13): 2406 (C @ (B @ A)) * (D @ (G @ F)) != c_0 # answer(A). [back_rewrite(2256),rewrite(2360(5),2360(13),1552(17),1185(18))]. given #318 (F,wt=13): 2562 (D @ (G @ F)) * (C @ (B @ A)) != c_0 # answer(A). [back_rewrite(1189),rewrite(2360(5),2360(10))]. given #319 (T,wt=11): 2349 x * y * y @ (y @ x) = c_0. [para(2298(a,1),459(a,1,2)),rewrite(3(2))]. given #320 (T,wt=11): 2360 (x @ y) @ z = z @ (y @ x). [para(1185(a,1),2298(a,1,2)),rewrite(2344(3),1382(6))]. given #321 (A,wt=18): 225 x * y * y * x != y * z | x * x * y = z. [para(181(a,1),16(a,1,2,2)),rewrite(181(8))]. given #322 (F,wt=15): 2428 (C @ (B @ A)) * D * (D @ (G @ F)) != D # answer(A). [back_rewrite(1982),rewrite(2360(5),2360(15,R),2298(15),2360(11))]. given #323 (F,wt=15): 2474 D * (D @ (G @ F)) != (C @ (A @ B)) * D # answer(A). [back_rewrite(1681),rewrite(2360(6))]. given #324 (T,wt=11): 2396 x * (x @ y) @ y = x @ y. [back_rewrite(401),rewrite(2344(5))]. given #325 (T,wt=11): 2836 (x @ y) @ (z @ (y @ x)) = c_0. [para(2360(a,1),1032(a,1,2))]. given #326 (A,wt=18): 248 x * y * z != z | x * y * (x * y @ z) = c_0. [para(15(a,1),184(a,1)),flip(b)]. given #327 (F,wt=15): 2475 (D @ (G @ F)) * C != C * (C @ (A @ B)) # answer(A). [back_rewrite(1680),rewrite(2360(5))]. given #328 (F,wt=15): 2481 (D @ (G @ F)) * C * (C @ (B @ A)) != C # answer(A). [back_rewrite(1660),rewrite(2360(5),2360(11))]. given #329 (T,wt=11): 2844 (x @ y) @ ((y @ x) @ z) = c_0. [para(2360(a,2),1526(a,1,2))]. given #330 (T,wt=13): 1390 x @ (y @ z) * x * (z @ y) = c_0. [para(1185(a,1),480(a,1,1)),rewrite(3(4))]. given #331 (A,wt=22): 250 x * y * (x @ z) * y * x != x * z * x * y | y = z. [para(13(a,1),17(a,1)),flip(a)]. given #332 (F,wt=15): 2506 (D @ (F @ G)) * C != C * (C @ (B @ A)) # answer(A). [back_rewrite(1478),rewrite(2360(6)),flip(a)]. given #333 (F,wt=15): 2513 x * (D @ (G @ F)) != x * (C @ (A @ B)) # answer(A). [back_rewrite(1470),rewrite(2360(5))]. given #334 (T,wt=13): 1391 (x @ y) * z * (y @ x) @ z = c_0. [para(1185(a,1),480(a,1,2)),rewrite(3(4))]. given #335 (T,wt=13): 1939 x @ ((y @ z) @ x * (z @ y)) = c_0. [para(1148(a,1),499(a,1,1,2)),rewrite(191(2))]. given #336 (A,wt=18): 253 x * y * y * z != y * z * z * y | z = x. [para(181(a,1),17(a,1,2,2)),rewrite(181(6))]. given #337 (F,wt=15): 2514 (D @ (G @ F)) * x != (C @ (A @ B)) * x # answer(A). [back_rewrite(1469),rewrite(2360(5))]. given #338 (F,wt=15): 2540 (D @ (G @ F)) * (C @ (B @ A)) * x != x # answer(A). [back_rewrite(1307),rewrite(2360(5),2360(10))]. given #339 (T,wt=13): 2320 x * y @ x * (x @ y) = y @ x. [back_rewrite(2149),rewrite(2298(8),385(6))]. given #340 (T,wt=13): 2324 (x @ y) @ y * x * (y @ x) = c_0. [back_rewrite(2142),rewrite(2298(2))]. given #341 (A,wt=18): 255 x * y * (x * y @ z) != x * y * z | c_0 = z. [para(15(a,1),187(a,1)),flip(a)]. given #342 (F,wt=15): 2544 (C @ (B @ A)) * (D @ (G @ F)) * x != x # answer(A). [back_rewrite(1278),rewrite(2360(5),2360(10))]. given #343 (F,wt=15): 2560 x * (D @ (G @ F)) * (C @ (B @ A)) != x # answer(A). [back_rewrite(1194),rewrite(2360(5),2360(10))]. given #344 (T,wt=13): 2340 x * (x @ y) @ x * y = x @ y. [back_rewrite(1843),rewrite(2317(8))]. given #345 (T,wt=13): 2343 x @ y * z * x = x @ y * z. [para(3(a,1),2298(a,1,2))]. given #346 (A,wt=22): 256 x * y * (x @ z) * y * x != x * z * x * y | z = y. [para(13(a,1),18(a,1)),flip(a)]. given #347 (F,wt=15): 2561 x * (C @ (B @ A)) * (D @ (G @ F)) != x # answer(A). [back_rewrite(1192),rewrite(2360(5),2360(10))]. given #348 (F,wt=15): 2578 D * (D @ (F @ G)) != (C @ (B @ A)) * D # answer(A). [back_rewrite(1039),rewrite(2360(5)),flip(a)]. given #349 (T,wt=13): 2356 x * y * x * x @ (x @ y) = c_0. [para(2298(a,1),758(a,1,2)),rewrite(3(2))]. given #350 (T,wt=13): 2384 x * y @ y * (y @ x) = x @ y. [back_rewrite(2312),rewrite(2344(6))]. given #351 (A,wt=18): 257 x * y * y * z != y * z * z * y | x = z. [para(181(a,1),18(a,1,2,2)),rewrite(181(6))]. given #352 (F,wt=15): 2636 x * (D @ (F @ G)) != x * (C @ (B @ A)) # answer(A). [back_rewrite(24),rewrite(2360(5)),flip(a)]. given #353 (F,wt=15): 2637 (D @ (F @ G)) * x != (C @ (B @ A)) * x # answer(A). [back_rewrite(23),rewrite(2360(5)),flip(a)]. given #354 (T,wt=13): 2385 x * (x @ y) @ y * x = x @ y. [back_rewrite(2310),rewrite(2344(8),2298(6))]. given #355 (T,wt=13): 2666 x * y * z @ z = x * y @ z. [para(3(a,1),2344(a,1,1))]. given #356 (A,wt=23): 264 x * y * z * y * x * (y @ x) = y * x * z * y * x. [para(4(a,1),19(a,1,2,2,2)),flip(a)]. given #357 (F,wt=17): 2460 (A @ B) * (D @ (G @ F)) * C != C * (A @ B) # answer(A). [back_rewrite(1754),rewrite(2360(8))]. given #358 (F,wt=17): 2518 (G @ F) * D * (F @ G) != (C @ (B @ A)) * D # answer(A). [back_rewrite(1420),rewrite(2360(5)),flip(a)]. given #359 (T,wt=13): 2669 x * y * y * y @ (x @ y) = c_0. [para(2344(a,1),642(a,1,2)),rewrite(3(3))]. given #360 (T,wt=13): 2794 x * y * y * y @ (y @ x) = c_0. [para(2298(a,1),2349(a,1,2)),rewrite(3(3))]. given #361 (A,wt=23): 265 x * y * y * y * x * x = y * y * x * x * x * y. [para(5(a,1),19(a,1,2)),flip(a)]. given #362 (F,wt=17): 2520 (D @ (G @ F)) * (A @ B) * C != C * (A @ B) # answer(A). [back_rewrite(1387),rewrite(2360(5))]. given #363 (F,wt=17): 2531 (G @ F) * D * (F @ G) != D * (C @ (B @ A)) # answer(A). [back_rewrite(1350),rewrite(2360(6)),flip(a)]. given #364 (T,wt=13): 2795 (x @ (y @ z)) * (x @ (z @ y)) = c_0. [hyper(1355,a,2360,a)]. given #365 (T,wt=13): 2796 ((x @ y) @ z) * ((y @ x) @ z) = c_0. [hyper(1355,a,2360,a(flip))]. given #366 (A,wt=25): 267 x * y * z * y * x * (y @ z * x) = y * x * y * z * x. [para(14(a,1),19(a,1,2,2)),flip(a)]. given #367 (F,wt=17): 2551 (C @ (B @ A)) * (F @ G) * D * (G @ F) != D # answer(A). [back_rewrite(1233),rewrite(2360(5))]. given #368 (F,wt=17): 2558 (F @ G) * D * (C @ (B @ A)) * (G @ F) != D # answer(A). [back_rewrite(1202),rewrite(2360(9))]. given #369 (T,wt=13): 2809 x * (y @ z) @ (x @ (z @ y)) = c_0. [para(2360(a,1),459(a,1,2))]. given #370 (T,wt=13): 2810 (x @ y) * z @ ((y @ x) @ z) = c_0. [para(2360(a,2),459(a,1,2))]. given #371 (A,wt=19): 268 x * y * y * x * z = y * x * x * y * z. [para(181(a,1),19(a,1,2,2)),rewrite(181(8))]. given #372 (F,wt=17): 2559 (A @ B) * C * (D @ (G @ F)) != C * (A @ B) # answer(A). [back_rewrite(1199),rewrite(2360(9))]. given #373 (F,wt=17): 2593 (F @ G) * (C @ (B @ A)) * D != D * (F @ G) # answer(A). [back_rewrite(913),rewrite(2360(8))]. given #374 (T,wt=13): 2811 (x @ y) * z @ (z @ (y @ x)) = c_0. [para(2360(a,1),471(a,1,2))]. given #375 (T,wt=13): 2812 x * (y @ z) @ ((z @ y) @ x) = c_0. [para(2360(a,2),471(a,1,2))]. given #376 (A,wt=25): 269 x * y * z * y * x * (x * y @ z) = y * x * x * y * z. [para(15(a,1),19(a,1,2,2)),flip(a)]. given #377 (F,wt=17): 2618 (C @ (B @ A)) * (F @ G) * D != D * (F @ G) # answer(A). [back_rewrite(420),rewrite(2360(5))]. given #378 (F,wt=17): 2627 (F @ G) * D * (C @ (B @ A)) != D * (F @ G) # answer(A). [back_rewrite(50),rewrite(2360(9))]. given #379 (T,wt=13): 2837 (x @ (y @ z)) @ (x @ (z @ y)) = c_0. [para(2360(a,1),1222(a,1,1))]. given #380 (T,wt=13): 2838 ((x @ y) @ z) @ ((y @ x) @ z) = c_0. [para(2360(a,2),1222(a,1,1))]. given #381 (A,wt=24): 270 x * y * z * y * x * u != y | x * z * x * y * u = c_0. [para(19(a,1),184(a,1)),flip(b)]. given #382 (F,wt=17): 2664 (G @ F) * D * (C @ (A @ B)) != D * (G @ F) # answer(A). [ur(44,b,2517,a)]. given #383 (F,wt=17): 2665 (B @ A) * C * (D @ (F @ G)) != C * (B @ A) # answer(A). [ur(44,b,2638,a(flip))]. given #384 (T,wt=13): 2976 x * x * y @ y * x = x @ y. [para(2320(a,1),2320(a,1,2,2)),rewrite(3(4),4(3),3(5),4(5),2340(8))]. given #385 (T,wt=13): 3009 x * y @ y * y * x = x @ y. [para(2320(a,1),2340(a,1,1,2)),rewrite(3(3),4(3),3(5),4(4),2320(8))]. given #386 (A,wt=24): 271 x * y * z * y * x * u != x * z * x * y * u | c_0 = y. [para(19(a,1),187(a,1))]. given #387 (F,wt=17): 2790 C * (B @ A) * (D @ (G @ F)) != (B @ A) * C # answer(A). [ur(155,b,2406,a),rewrite(191(6)),flip(a)]. given #388 (F,wt=17): 2791 D * (G @ F) * (C @ (B @ A)) != (G @ F) * D # answer(A). [ur(155,b,2562,a),rewrite(191(6)),flip(a)]. given #389 (T,wt=13): 3308 (x @ (y @ z)) @ ((z @ y) @ x) = c_0. [para(2795(a,1),1390(a,1,2,2)),rewrite(191(6))]. given #390 (T,wt=13): 3310 ((x @ y) @ z) @ (z @ (y @ x)) = c_0. [para(2795(a,1),1391(a,1,1,2)),rewrite(191(4))]. given #391 (A,wt=19): 276 x * y * z * z * y = x * z * y * y * z. [para(181(a,1),20(a,1,2,2,2)),rewrite(181(7))]. given #392 (F,wt=17): 2896 (G @ F) * (C @ (A @ B)) * D != D * (G @ F) # answer(A). [ur(10,b,2474,a)]. given #393 (F,wt=17): 2938 (B @ A) * (D @ (F @ G)) * C != C * (B @ A) # answer(A). [ur(10,b,2506,a(flip))]. given #394 (T,wt=13): 3364 (x @ (y @ z)) @ x * (z @ y) = c_0. [hyper(1355,a,2809,a),rewrite(191(7))]. given #395 (T,wt=13): 3394 (x @ (y @ z)) @ (z @ y) * x = c_0. [para(2334(a,1),2810(a,1,2)),rewrite(2360(8,R),2343(8))]. given #396 (A,wt=24): 277 x * y * z * u * z * y != x | z * y * u * y * z = c_0. [para(20(a,1),184(a,1)),flip(b)]. given #397 (F,wt=19): 1656 (D @ (F @ G)) * (A @ B) * (C @ (A @ B)) != A @ B # answer(A). [para(1552(a,1),1275(a,1,2))]. given #398 (F,wt=19): 1659 (C @ (A @ B)) * (F @ G) * (D @ (F @ G)) != F @ G # answer(A). [para(1552(a,1),1304(a,1,2))]. given #399 (T,wt=13): 3538 x * y @ x * x * y * y = c_0. [para(2324(a,1),3009(a,2)),rewrite(1554(5),1037(4),1148(3),191(2),3(9),3(8),1148(7),191(6),3(6),3(5),1037(4),1552(3),636(5))]. given #400 (T,wt=13): 3629 x * x * y * y @ x * y = c_0. [hyper(1355,a,3538,a),rewrite(191(7))]. given #401 (A,wt=24): 278 x * y * z * u * z * y != z * y * u * y * z | c_0 = x. [para(20(a,1),187(a,1))]. given #402 (F,wt=19): 1671 (C @ (A @ B)) * D * (D @ (F @ G)) * x != D * x # answer(A). [ur(576,b,1421,a),rewrite(3(16),3(15)),flip(a)]. given #403 (F,wt=19): 1672 x * (C @ (A @ B)) * D * (D @ (F @ G)) != x * D # answer(A). [ur(372,b,1421,a),flip(a)]. given #404 (T,wt=14): 374 x * y * z != x * y * u | u = z. [para(3(a,1),372(a,1)),rewrite(3(4))]. given #405 (T,wt=14): 414 (x @ y) * z != x * y | y * x = z. [para(396(a,1),1(a,1)),flip(a)]. given #406 (A,wt=16): 279 x * y * z * u != u | x * y * z = c_0. [para(3(a,1),185(a,1,2))]. given #407 (F,wt=19): 1708 (D @ (F @ G)) * C * (C @ (A @ B)) * x != C * x # answer(A). [ur(576,b,1486,a),rewrite(3(16),3(15)),flip(a)]. given #408 (F,wt=19): 2419 (C @ (B @ A)) * D * D * (D @ (G @ F)) != D * D # answer(A). [back_rewrite(2136),rewrite(2360(5),2360(12))]. given #409 (T,wt=14): 415 x * y * z != z * y | z @ y = x. [para(396(a,1),2(a,1)),flip(a)]. given #410 (T,wt=14): 574 x * y * z != y * z | x * z = z. [para(4(a,1),54(a,1)),flip(a)]. given #411 (A,wt=16): 280 x * (x @ y) != z * x * y | z * y = c_0. [para(4(a,1),185(a,1,2)),flip(a)]. given #412 (F,wt=17): 3736 (C @ (A @ B)) * (G @ F) * D != D * (G @ F) # answer(A). [ur(415,b,2517,a)]. given #413 (F,wt=17): 3737 (D @ (F @ G)) * (B @ A) * C != C * (B @ A) # answer(A). [ur(415,b,2638,a(flip))]. given #414 (T,wt=12): 3758 c_0 != x | x * (y @ z) = y @ z. [para(1148(a,1),574(a,1,2)),rewrite(191(2),1148(3)),flip(a)]. given #415 (T,wt=14): 910 x * (y @ x) * z != y * x | y = z. [para(849(a,1),7(a,1)),flip(a)]. given #416 (A,wt=24): 282 x * y * z * u * z * y != y * u * y * z | x * z = c_0. [para(5(a,1),185(a,1,2))]. given #417 (F,wt=19): 2430 (C @ (B @ A)) * D * (D @ (G @ F)) * x != D * x # answer(A). [back_rewrite(1980),rewrite(2360(5),2360(15,R),2298(15),2360(11))]. given #418 (F,wt=19): 2458 x * D * (D @ (G @ F)) != x * (C @ (A @ B)) * D # answer(A). [back_rewrite(1756),rewrite(2360(6))]. given #419 (T,wt=10): 3816 x * y != y | y @ x = x. [para(1148(a,1),910(a,1,2)),rewrite(191(2)),flip(a),flip(b)]. given #420 (T,wt=14): 911 x * (y @ x) * z != y * x | z = y. [para(849(a,1),7(a,2))]. given #421 (A,wt=20): 283 x * y * z * y * x != z * x * y | y * x = c_0. [para(5(a,1),185(a,1))]. given #422 (F,wt=19): 2459 D * (D @ (G @ F)) * x != (C @ (A @ B)) * D * x # answer(A). [back_rewrite(1755),rewrite(2360(6))]. given #423 (F,wt=19): 2464 x * (D @ (G @ F)) * C != x * C * (C @ (A @ B)) # answer(A). [back_rewrite(1749),rewrite(2360(5))]. given #424 (T,wt=14): 916 x * y != z * x | y * (x @ y) = z. [para(849(a,1),8(a,1))]. given #425 (T,wt=14): 1034 (x @ y) * z != x * (x @ y) | x = z. [para(908(a,1),1(a,1)),flip(a)]. given #426 (A,wt=20): 284 x * (x @ y) * z != u * x * y * z | u * y = c_0. [para(13(a,1),185(a,1,2)),flip(a)]. given #427 (F,wt=19): 2465 (D @ (G @ F)) * C * x != C * (C @ (A @ B)) * x # answer(A). [back_rewrite(1748),rewrite(2360(5))]. given #428 (F,wt=19): 2469 x * (D @ (G @ F)) * C * (C @ (B @ A)) != x * C # answer(A). [back_rewrite(1711),rewrite(2360(5),2360(11))]. given #429 (T,wt=14): 1035 (x @ y) * z != x * (x @ y) | z = x. [para(908(a,1),1(a,2))]. given #430 (T,wt=14): 1036 x * (x @ y) != z * x | x @ y = z. [para(908(a,1),2(a,1))]. given #431 (A,wt=16): 285 (x @ y) * z != x * y * z | y * x = c_0. [para(13(a,1),185(a,1)),flip(a)]. given #432 (F,wt=19): 2470 (D @ (G @ F)) * C * (C @ (B @ A)) * x != C * x # answer(A). [back_rewrite(1710),rewrite(2360(5),2360(11))]. given #433 (F,wt=19): 2472 (D @ (F @ G)) * C * x != C * (C @ (B @ A)) * x # answer(A). [back_rewrite(1692),rewrite(2360(6)),flip(a)]. given #434 (T,wt=14): 1180 (x @ y) * z != x | x * (y @ x) = z. [para(961(a,1),143(a,1)),rewrite(1032(5),181(6)),flip(a)]. given #435 (T,wt=14): 1181 x * y * (z @ y) != y | y @ z = x. [para(961(a,1),144(a,2)),rewrite(1032(2),181(3))]. given #436 (A,wt=18): 287 x * (x @ y * z) != x * y * z | y * z = c_0. [para(14(a,1),185(a,1)),flip(a)]. given #437 (F,wt=19): 2473 (D @ (G @ F)) * (A @ B) != (A @ B) * (C @ (A @ B)) # answer(A). [back_rewrite(1682),rewrite(2360(5))]. given #438 (F,wt=19): 2476 (F @ G) * (D @ (G @ F)) != (C @ (A @ B)) * (F @ G) # answer(A). [back_rewrite(1679),rewrite(2360(8))]. given #439 (T,wt=14): 1190 x * (y @ z) * u != x | z @ y = u. [para(1148(a,1),7(a,1,2)),rewrite(191(2)),flip(a)]. given #440 (T,wt=14): 1195 x * (y @ z) != u | u * (z @ y) = x. [para(1148(a,1),8(a,1,2)),rewrite(191(2)),flip(a)]. given #441 (A,wt=22): 288 x * y * (x * y @ z) != u * x * y * z | u * z = c_0. [para(15(a,1),185(a,1,2)),flip(a)]. given #442 (F,wt=17): 3994 (D @ (F @ G)) * (B @ A) * C * (A @ B) != C # answer(A). [ur(1195,b,3737,a(flip)),rewrite(3(15),3(14))]. given #443 (F,wt=17): 3995 (C @ (A @ B)) * (G @ F) * D * (F @ G) != D # answer(A). [ur(1195,b,3736,a(flip)),rewrite(3(15),3(14))]. given #444 (T,wt=14): 1210 (x @ y) * z != u | (y @ x) * u = z. [para(1148(a,1),16(a,1,2,2,2)),rewrite(191(4),1185(4),1148(7),191(6)),flip(a)]. given #445 (T,wt=14): 1213 x * (y @ z) * u != u | z @ y = x. [para(1148(a,1),17(a,1,2,2,2)),rewrite(191(3),1148(8),191(7),1185(7))]. given #446 (A,wt=18): 289 x * (y * x @ z) != y * x * z | z * y = c_0. [para(15(a,1),185(a,1)),flip(a)]. given #447 (F,wt=17): 3996 (G @ F) * (C @ (A @ B)) * D * (F @ G) != D # answer(A). [ur(1195,b,2896,a(flip)),rewrite(3(15),3(14))]. given #448 (F,wt=17): 3997 (G @ F) * D * (C @ (A @ B)) * (F @ G) != D # answer(A). [ur(1195,b,2664,a(flip)),rewrite(3(15),3(14))]. given #449 (T,wt=14): 1247 x * y * (y @ z) != y | z @ y = x. [back_rewrite(1161),rewrite(1185(4)),flip(a)]. given #450 (T,wt=14): 1483 (x @ y) * z != y | y * (y @ x) = z. [para(1248(a,1),1(a,1)),flip(a)]. given #451 (A,wt=24): 290 x * y * z * y * x * u != z * x * y * u | y * x = c_0. [para(19(a,1),185(a,1))]. given #452 (F,wt=17): 3998 (F @ G) * (C @ (B @ A)) * D * (G @ F) != D # answer(A). [ur(1195,b,2593,a(flip)),rewrite(3(15),3(14))]. given #453 (F,wt=17): 3999 (A @ B) * C * (D @ (G @ F)) * (B @ A) != C # answer(A). [ur(1195,b,2559,a(flip)),rewrite(3(15),3(14))]. given #454 (T,wt=14): 1532 x * y * z != y | z @ y = x * z. [para(1248(a,1),54(a,1)),flip(a),flip(b)]. given #455 (T,wt=14): 1535 x * y != z * x | z * (y @ x) = y. [para(1248(a,1),56(a,1,2)),flip(a)]. given #456 (A,wt=23): 292 x * y * (x @ y) * z * y * x = x * y * z * x * y. [para(21(a,1),13(a,1))]. given #457 (F,wt=17): 4000 (G @ F) * D * (F @ G) * (C @ (A @ B)) != D # answer(A). [ur(1195,b,2531,a(flip)),rewrite(2360(14),3(15),3(14))]. given #458 (F,wt=17): 4001 (D @ (G @ F)) * (A @ B) * C * (B @ A) != C # answer(A). [ur(1195,b,2520,a(flip)),rewrite(3(15),3(14))]. given #459 (T,wt=14): 1553 x * (y @ x) != z * x | y @ x = z. [para(1526(a,1),11(a,1,2,2)),rewrite(191(2)),flip(a)]. given #460 (T,wt=14): 1607 x * y * z != z | y @ x = y * x. [para(1185(a,1),157(a,1)),flip(a),flip(b)]. given #461 (A,wt=23): 293 x * y * z * (z @ x) * y * x = y * z * x * x * y. [para(13(a,1),21(a,1,2)),flip(a)]. given #462 (F,wt=17): 4002 (A @ B) * (D @ (G @ F)) * C * (B @ A) != C # answer(A). [ur(1195,b,2460,a(flip)),rewrite(3(15),3(14))]. given #463 (F,wt=17): 4026 (D @ (G @ F)) * C != (B @ A) * C * (A @ B) # answer(A). [ur(1210,b,3994,a),rewrite(2360(5))]. given #464 (T,wt=14): 1613 (x @ y) * z != y * (x @ y) | y = z. [para(1552(a,1),1(a,1)),flip(a)]. given #465 (T,wt=14): 1614 (x @ y) * z != y * (x @ y) | z = y. [para(1552(a,1),1(a,2))]. given #466 (A,wt=24): 294 x * y * z * u * y * x != y | x * z * u * x * y = c_0. [para(21(a,1),184(a,1)),flip(b)]. given #467 (F,wt=17): 4027 (D @ (G @ F)) * C * (B @ A) != (B @ A) * C # answer(A). [ur(1210,b,3737,a),rewrite(2360(5))]. given #468 (F,wt=17): 4028 (G @ F) * D != (C @ (B @ A)) * D * (G @ F) # answer(A). [ur(1210,b,3736,a),rewrite(2360(5)),flip(a)]. given #469 (T,wt=14): 2393 x * y != y | x * (x @ y) = x @ y. [back_rewrite(1593),rewrite(2344(4)),flip(b)]. given #470 (T,wt=14): 2839 x @ (y @ z) != c_0 | x @ (z @ y) = c_0. [para(2360(a,1),1212(a,1))]. given #471 (A,wt=24): 295 x * y * z * u * y * x != x * z * u * x * y | c_0 = y. [para(21(a,1),187(a,1))]. given #472 (F,wt=17): 4029 (F @ G) * D * (G @ F) != (C @ (A @ B)) * D # answer(A). [ur(1210,b,2896,a)]. given #473 (F,wt=17): 4030 C * (D @ (F @ G)) != (A @ B) * C * (B @ A) # answer(A). [ur(1210,b,2665,a),flip(a)]. given #474 (T,wt=14): 2840 (x @ y) @ z != c_0 | (y @ x) @ z = c_0. [para(2360(a,2),1212(a,1))]. given #475 (T,wt=14): 3683 x * y != z | (y @ x) * z = y * x. [para(1185(a,1),414(a,1)),flip(a),flip(b)]. given #476 (A,wt=24): 296 x * y * z * u * y * x != z * u * x * y | y * x = c_0. [para(21(a,1),185(a,1))]. given #477 (F,wt=17): 4031 (F @ G) * D * (G @ F) != D * (C @ (A @ B)) # answer(A). [ur(1210,b,2664,a)]. given #478 (F,wt=17): 4032 C * (D @ (G @ F)) != (B @ A) * C * (A @ B) # answer(A). [ur(1210,b,2559,a),flip(a)]. given #479 (T,wt=14): 3817 x * y != z * x | (x @ z) * y = z. [para(1185(a,1),910(a,1,2)),flip(b)]. given #480 (T,wt=14): 3818 x * x * (y @ x) != y * x | y = x. [para(1552(a,1),910(a,1,2))]. given #481 (A,wt=16): 297 x * y * z * u != x * y * z | c_0 = u. [para(3(a,1),194(a,1,2))]. given #482 (F,wt=17): 4033 (G @ F) * D != D * (C @ (B @ A)) * (G @ F) # answer(A). [ur(1210,b,2558,a)]. given #483 (F,wt=17): 4039 (F @ G) * D * (G @ F) * (C @ (B @ A)) != D # answer(A). [ur(1210,b,2791,a(flip))]. given #484 (T,wt=14): 3845 x * x * (y @ x) != y * x | x = y. [para(1552(a,1),911(a,1,2))]. given #485 (T,wt=14): 3869 x * (x @ y) != z | (y @ x) * z = x. [para(1185(a,1),1034(a,1)),flip(a),flip(b)]. given #486 (A,wt=16): 298 x * y * z != x * z | y * (y @ z) = c_0. [para(4(a,1),194(a,1,2)),flip(b)]. given #487 (F,wt=17): 4040 (A @ B) * C * (B @ A) * (D @ (G @ F)) != C # answer(A). [ur(1210,b,2790,a(flip))]. given #488 (F,wt=17): 4091 (F @ G) * D != D * (C @ (A @ B)) * (F @ G) # answer(A). [ur(1210,b,3997,a)]. given #489 (T,wt=14): 3961 x != y | (z @ y) * x = y * (z @ y). [para(1185(a,1),1180(a,1)),flip(b)]. given #490 (T,wt=14): 3988 x * y * (y @ z) != x | z @ y = y. [para(908(a,1),1190(a,1,2))]. given #491 (A,wt=24): 300 x * y * z * u * z * y != x * z | y * u * y * z = c_0. [para(5(a,1),194(a,1,2)),flip(b)]. given #492 (F,wt=17): 4135 C * (D @ (G @ F)) * (B @ A) != (B @ A) * C # answer(A). [ur(1210,b,3999,a),flip(a)]. given #493 (F,wt=19): 2480 x * (D @ (G @ F)) * y != x * (C @ (A @ B)) * y # answer(A). [back_rewrite(1675),rewrite(2360(5))]. given #494 (T,wt=12): 4463 x * (y @ z) != x | y @ z = c_0. [para(1222(a,1),3988(a,1,2,2)),rewrite(191(3),1222(6)),flip(b)]. given #495 (T,wt=14): 3989 x * y != x | (z @ u) * y = z @ u. [para(1185(a,1),1190(a,1,2)),flip(b)]. given #496 (A,wt=20): 301 x * y * z * y * x != y * x | z * x * y = c_0. [para(5(a,1),194(a,1)),flip(b)]. given #497 (F,wt=19): 2492 x * (D @ (F @ G)) * C != x * C * (C @ (B @ A)) # answer(A). [back_rewrite(1619),rewrite(2360(6)),flip(a)]. given #498 (F,wt=19): 2493 (D @ (G @ F)) * (A @ B) * (C @ (B @ A)) != A @ B # answer(A). [back_rewrite(1609),rewrite(2360(5),2360(13))]. given #499 (T,wt=14): 3990 x * y * (z @ y) != x | y @ z = y. [para(1552(a,1),1190(a,1,2))]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 24 (0.00 of 1.96 sec). given #500 (T,wt=14): 4044 x != y | (z @ u) * y = (z @ u) * x. [para(1185(a,1),1210(a,1))]. given #501 (A,wt=24): 302 x * y * z * y * x * u != y * x * z * x * y | c_0 = u. [para(5(a,1),194(a,2)),rewrite(3(4),3(3),3(2))]. given #502 (F,wt=19): 2495 (F @ G) * (D @ (F @ G)) != (C @ (B @ A)) * (F @ G) # answer(A). [back_rewrite(1555),rewrite(2360(5)),flip(a)]. given #503 (F,wt=19): 2505 (C @ (B @ A)) * (F @ G) * (D @ (G @ F)) != F @ G # answer(A). [back_rewrite(1487),rewrite(2360(5),2360(13))]. given #504 (T,wt=14): 4045 x * (y @ x) != z | (x @ y) * z = x. [para(1552(a,1),1210(a,1))]. given #505 (T,wt=14): 4054 x @ (y @ z) != u | (z @ y) @ x = u. [para(2795(a,1),1213(a,1,2)),rewrite(191(2)),flip(a)]. given #506 (A,wt=20): 303 x * y * z * u != x * z | y * (y @ z) * u = c_0. [para(13(a,1),194(a,1,2)),flip(b)]. given #507 (F,wt=19): 2509 x * y * (D @ (G @ F)) != x * y * (C @ (A @ B)) # answer(A). [back_rewrite(1474),rewrite(2360(5))]. given #508 (F,wt=19): 2529 x * (D @ (G @ F)) * (C @ (B @ A)) * y != x * y # answer(A). [back_rewrite(1354),rewrite(2360(5),2360(10))]. given #509 (T,wt=14): 4055 (x @ y) @ z != u | z @ (y @ x) = u. [para(2796(a,1),1213(a,1,2)),rewrite(191(2)),flip(a)]. given #510 (T,wt=14): 4118 x != y | (y @ z) * x = y * (y @ z). [para(1185(a,1),1483(a,1)),flip(b)]. given #511 (A,wt=16): 304 x * y * z != y * x | (x @ y) * z = c_0. [para(13(a,1),194(a,1)),flip(b)]. given #512 (F,wt=19): 2534 x * (C @ (B @ A)) * (D @ (G @ F)) * y != x * y # answer(A). [back_rewrite(1339),rewrite(2360(5),2360(10))]. given #513 (F,wt=19): 2536 x * (C @ (B @ A)) * D * (D @ (G @ F)) != x * D # answer(A). [back_rewrite(1327),rewrite(2360(5),2360(11))]. given #514 (T,wt=14): 4462 x * y * z != x | z @ y = z * y. [para(385(a,1),3988(a,1,2,2)),rewrite(3(3),4(3),716(5))]. given #515 (T,wt=14): 4510 x * y != x | y * (y @ z) = y @ z. [para(2334(a,1),3990(a,1,2,2)),rewrite(3(4),1148(3),191(2),2396(5)),flip(b)]. given #516 (A,wt=22): 306 x * y * z * u != x * u | y * z * (y * z @ u) = c_0. [para(15(a,1),194(a,1,2)),flip(b)]. given #517 (F,wt=19): 2556 x * y * (C @ (B @ A)) * (D @ (G @ F)) != x * y # answer(A). [back_rewrite(1208),rewrite(2360(5),2360(10))]. given #518 (F,wt=19): 2557 x * y * (D @ (G @ F)) * (C @ (B @ A)) != x * y # answer(A). [back_rewrite(1206),rewrite(2360(5),2360(10))]. given #519 (T,wt=14): 4530 x != y | (x @ z) * y = x * (x @ z). [para(2334(a,1),4045(a,1,2)),rewrite(3(4),1148(3),191(2),2396(4))]. given #520 (T,wt=15): 397 (x @ y) * z * y * x = z * x * y. [hyper(45,a,13,a(flip)),flip(a)]. given #521 (A,wt=18): 307 x * y * z != z * x | y * (x * y @ z) = c_0. [para(15(a,1),194(a,1)),flip(b)]. given #522 (F,wt=17): 4705 (D @ (F @ G)) * C * A * B != C * A * B # answer(A). [para(397(a,1),497(a,2)),rewrite(1554(13),908(12),4(13))]. given #523 (F,wt=17): 5000 (D @ (G @ F)) * C * A * B != C * A * B # answer(A). [ur(1210,b,4705,a),rewrite(2360(5))]. given #524 (T,wt=11): 4668 (y @ z) @ x * z * y = c_0. [para(397(a,1),299(a,1)),rewrite(3(6),3(5),4(5)),xx(a)]. given #525 (T,wt=11): 4670 x * z * y @ (y @ z) = c_0. [para(397(a,1),299(a,2)),rewrite(3(4),3(3),4(3)),xx(a)]. given #526 (A,wt=24): 308 x * y * z * y * x * u != y * x | z * x * y * u = c_0. [para(19(a,1),194(a,1)),flip(b)]. given #527 (F,wt=17): 5013 (D @ (F @ G)) * A * B * C != A * B * C # answer(A). [ur(55,b,4705,a(flip)),rewrite(3(17),3(16),3(15),15(16),3(16))]. given #528 (F,wt=17): 5029 (D @ (G @ F)) * A * B * C != A * B * C # answer(A). [ur(55,b,5000,a(flip)),rewrite(3(17),3(16),3(15),15(16),3(16))]. given #529 (T,wt=11): 4690 x * y * z @ (y @ z) = c_0. [para(397(a,1),385(a,1,1)),rewrite(4670(8))]. given #530 (T,wt=11): 4715 (x @ y) @ z * x * y = c_0. [para(397(a,1),716(a,1,2)),rewrite(4668(8))]. given #531 (A,wt=24): 309 x * y * z * u * y * x != y * x | z * u * x * y = c_0. [para(21(a,1),194(a,1)),flip(b)]. given #532 (F,wt=17): 5172 (D @ (F @ G)) * B * C * A != B * C * A # answer(A). [ur(55,b,5013,a(flip)),rewrite(3(17),3(16),3(15),15(16),3(16))]. given #533 (F,wt=17): 5189 (D @ (G @ F)) * B * C * A != B * C * A # answer(A). [ur(55,b,5029,a(flip)),rewrite(3(17),3(16),3(15),15(16),3(16))]. given #534 (T,wt=11): 5054 ((x @ y) @ z) @ u * z = c_0. [para(1185(a,1),4668(a,1,2,2)),rewrite(2360(4,R),716(4))]. given #535 (T,wt=11): 5118 x * y @ ((z @ u) @ y) = c_0. [para(1185(a,1),4670(a,1,1,2)),rewrite(2360(5,R),716(5))]. given #536 (A,wt=18): 310 x * y @ z != x * y * z | z * x * y = c_0. [para(3(a,1),281(a,2))]. given #537 (F,wt=19): 2563 D * D * (D @ (F @ G)) != (C @ (B @ A)) * D * D # answer(A). [back_rewrite(1146),rewrite(2360(5)),flip(a)]. given #538 (F,wt=19): 2568 D * (D @ (F @ G)) * x != (C @ (B @ A)) * D * x # answer(A). [back_rewrite(1114),rewrite(2360(5)),flip(a)]. given #539 (T,wt=11): 5299 x * y @ (y @ (z @ u)) = c_0. [hyper(4055,a,5054,a)]. given #540 (T,wt=11): 5300 (x @ (y @ z)) @ u * x = c_0. [hyper(2840,a,5054,a)]. given #541 (A,wt=18): 318 x * y * z != z * x * y | x * y @ z = c_0. [para(3(a,1),299(a,1))]. given #542 (F,wt=19): 2576 x * D * (D @ (F @ G)) != x * (C @ (B @ A)) * D # answer(A). [back_rewrite(1045),rewrite(2360(5)),flip(a)]. given #543 (F,wt=19): 2579 (D @ (F @ G)) * (A @ B) != (A @ B) * (C @ (B @ A)) # answer(A). [back_rewrite(1038),rewrite(2360(8)),flip(a)]. given #544 (T,wt=13): 4813 x * y * z @ x * z * y = c_0. [para(397(a,1),2298(a,1,2)),rewrite(4670(9))]. given #545 (T,wt=13): 5035 (x @ y) @ z * u * y * x = c_0. [para(3(a,1),4668(a,1,2))]. given #546 (A,wt=18): 319 x * y * z != z * x * y | z @ x * y = c_0. [para(3(a,1),299(a,2)),flip(a)]. given #547 (F,wt=19): 2632 x * y * (D @ (F @ G)) != x * y * (C @ (B @ A)) # answer(A). [back_rewrite(28),rewrite(2360(5)),flip(a)]. given #548 (F,wt=19): 2635 x * (D @ (F @ G)) * y != x * (C @ (B @ A)) * y # answer(A). [back_rewrite(25),rewrite(2360(5)),flip(a)]. given #549 (T,wt=13): 5064 (x @ y) @ z * y * x * x = c_0. [para(2298(a,1),4668(a,1,1)),rewrite(3(3))]. given #550 (T,wt=13): 5095 x * y * z @ (x @ z * y) = c_0. [para(397(a,1),4668(a,1,2)),rewrite(2360(5))]. given #551 (A,wt=22): 339 x * y * z * u * v != x * y * z * u * w | v = w. [para(3(a,1),42(a,1,2,2)),rewrite(3(6))]. given #552 (F,wt=19): 2954 (G @ F) * (D @ (G @ F)) != (C @ (A @ B)) * (G @ F) # answer(A). [para(1552(a,1),2514(a,1))]. given #553 (F,wt=19): 2956 (D @ (G @ F)) * (B @ A) * (C @ (B @ A)) != B @ A # answer(A). [para(1552(a,1),2540(a,1,2))]. given #554 (T,wt=13): 5098 x * y * z * u @ (u @ z) = c_0. [para(3(a,1),4670(a,1,1))]. given #555 (T,wt=13): 5129 x * y * z * z @ (z @ y) = c_0. [para(2298(a,1),4670(a,1,2)),rewrite(3(2))]. given #556 (A,wt=22): 340 x * y * z * u != x * y * v * z | v * (v @ z) = u. [para(4(a,1),42(a,1,2,2)),flip(a)]. given #557 (F,wt=19): 2994 (C @ (B @ A)) * (G @ F) * (D @ (G @ F)) != G @ F # answer(A). [para(1552(a,1),2544(a,1,2))]. given #558 (F,wt=19): 3111 (D @ (F @ G)) * (B @ A) != (B @ A) * (C @ (B @ A)) # answer(A). [para(1552(a,1),2637(a,2))]. given #559 (T,wt=13): 5157 x * y * z @ (z * y @ x) = c_0. [para(397(a,1),4670(a,1,1))]. given #560 (T,wt=13): 5195 x * y * z * u @ (z @ u) = c_0. [para(3(a,1),4690(a,1,1))]. given #561 (A,wt=18): 341 x * y * z * u != x * z * y | z @ y = u. [para(4(a,1),42(a,1,2)),flip(a)]. given #562 (F,wt=19): 3646 (C @ (A @ B)) * D * D * (D @ (F @ G)) != D * D # answer(A). [para(908(a,1),1671(a,1,2,2))]. given #563 (F,wt=19): 3731 (D @ (F @ G)) * C * C * (C @ (A @ B)) != C * C # answer(A). [para(908(a,1),1708(a,1,2,2))]. given #564 (T,wt=13): 5211 x * y * z * z @ (y @ z) = c_0. [para(2344(a,1),4690(a,1,2)),rewrite(3(2))]. given #565 (T,wt=13): 5233 (x @ y) @ z * u * x * y = c_0. [para(3(a,1),4715(a,1,2))]. given #566 (A,wt=22): 342 x * y * z * y * x != y * x * z * u | x * y = u. [para(5(a,1),42(a,1))]. given #567 (F,wt=19): 3851 D * D * (D @ (G @ F)) != (C @ (A @ B)) * D * D # answer(A). [para(908(a,1),2459(a,1,2))]. given #568 (F,wt=19): 3899 (D @ (G @ F)) * C * C != C * C * (C @ (A @ B)) # answer(A). [para(908(a,1),2465(a,2,2))]. given #569 (T,wt=13): 5245 (x @ y) @ z * x * y * y = c_0. [para(2344(a,1),4715(a,1,1)),rewrite(3(3))]. given #570 (T,wt=13): 5301 ((x @ y) @ z) @ u * v * z = c_0. [para(3(a,1),5054(a,1,2))]. given #571 (A,wt=22): 343 x * y * z * u != x * z * y * v | (y @ z) * u = v. [para(13(a,1),42(a,1,2))]. given #572 (F,wt=19): 3936 (D @ (G @ F)) * C * C * (C @ (B @ A)) != C * C # answer(A). [para(908(a,1),2470(a,1,2,2))]. given #573 (F,wt=19): 3942 (D @ (F @ G)) * C * C != C * C * (C @ (B @ A)) # answer(A). [para(908(a,1),2472(a,2,2))]. given #574 (T,wt=11): 6058 ((x @ y) @ (z @ u)) @ v = c_0. [para(1148(a,1),5301(a,1,2,2)),rewrite(191(5))]. given #575 (T,wt=11): 6117 x @ ((y @ z) @ (u @ v)) = c_0. [hyper(4055,a,6058,a)]. given #576 (A,wt=22): 344 x * y * z * u != x * z * y * v | (z @ y) * v = u. [para(13(a,1),42(a,2,2)),flip(b)]. given #577 (F,wt=19): 3945 (D @ (G @ F)) * (F @ G) * (C @ (B @ A)) != F @ G # answer(A). [ur(1180,b,2636,a),rewrite(2360(5))]. given #578 (F,wt=19): 3946 (D @ (F @ G)) * (G @ F) * (C @ (A @ B)) != G @ F # answer(A). [ur(1180,b,2513,a),rewrite(2360(5))]. given #579 (T,wt=13): 5312 ((x @ y) @ z) @ z * (z @ u) = c_0. [para(908(a,1),5054(a,1,2))]. given #580 (T,wt=13): 5315 x @ ((y @ z) * x @ (u @ v)) = c_0. [para(1185(a,1),5054(a,1,2)),rewrite(2360(5))]. given #581 (A,wt=24): 345 x * y * z * u != x * v * y * z | v * (v @ y * z) = u. [para(14(a,1),42(a,1,2)),flip(a)]. given #582 (F,wt=19): 3947 (C @ (A @ B)) * (B @ A) * (D @ (F @ G)) != B @ A # answer(A). [ur(1180,b,2636,a(flip)),rewrite(2360(5))]. given #583 (F,wt=19): 3950 (C @ (B @ A)) * (A @ B) * (D @ (G @ F)) != A @ B # answer(A). [ur(1180,b,2513,a(flip)),rewrite(2360(5))]. given #584 (T,wt=13): 5316 ((x @ y) @ z) @ z * (u @ z) = c_0. [para(1552(a,1),5054(a,1,2))]. given #585 (T,wt=13): 5331 x * y * z @ ((u @ v) @ z) = c_0. [para(3(a,1),5118(a,1,1))]. given #586 (A,wt=20): 346 x * y * z * u != z * x * y | z @ x * y = u. [para(14(a,1),42(a,1)),flip(a)]. given #587 (F,wt=19): 4034 D @ (G @ F) != (G @ F) * (C @ (A @ B)) * (F @ G) # answer(A). [ur(1210,b,2476,a),flip(a)]. given #588 (F,wt=19): 4041 (B @ A) * (D @ (G @ F)) * (A @ B) != C @ (A @ B) # answer(A). [ur(1210,b,2473,a(flip))]. given #589 (T,wt=13): 5342 x * (x @ y) @ ((z @ u) @ x) = c_0. [para(908(a,1),5118(a,1,1))]. given #590 (T,wt=13): 5345 x @ ((y @ z) @ (u @ v) * x) = c_0. [para(1185(a,1),5118(a,1,1))]. given #591 (A,wt=24): 347 x * y * z * u != x * u * y * v | z * (y * z @ u) = v. [para(15(a,1),42(a,1,2))]. given #592 (F,wt=19): 4102 (C @ (A @ B)) * (G @ F) * (D @ (F @ G)) != G @ F # answer(A). [ur(1247,b,2517,a),rewrite(2360(13))]. given #593 (F,wt=19): 4103 (D @ (F @ G)) * (B @ A) * (C @ (A @ B)) != B @ A # answer(A). [ur(1247,b,2638,a(flip)),rewrite(2360(13))]. given #594 (T,wt=13): 5346 x * (y @ x) @ ((z @ u) @ x) = c_0. [para(1552(a,1),5118(a,1,1))]. given #595 (T,wt=13): 5371 x * y * z @ (z @ (u @ v)) = c_0. [para(3(a,1),5299(a,1,1))]. given #596 (A,wt=20): 348 x * y * z * u != y * z * x | y * z @ x = u. [para(15(a,1),42(a,1)),flip(a)]. given #597 (F,wt=19): 4431 (D @ (G @ F)) * (B @ A) != (B @ A) * (C @ (A @ B)) # answer(A). [ur(3869,b,2544,a),rewrite(2360(8)),flip(a)]. given #598 (F,wt=19): 4432 (G @ F) * (D @ (F @ G)) != (C @ (B @ A)) * (G @ F) # answer(A). [ur(3869,b,2540,a),rewrite(2360(8))]. given #599 (T,wt=13): 5377 x * (x @ y) @ (x @ (z @ u)) = c_0. [para(908(a,1),5299(a,1,1))]. given #600 (T,wt=13): 5379 x * (y @ x) @ (x @ (z @ u)) = c_0. [para(1552(a,1),5299(a,1,1))]. given #601 (A,wt=22): 367 x * y * z != x * u * z | u * (u @ z) = y * (y @ z). [para(4(a,1),43(a,1,2))]. given #602 (F,wt=19): 4520 (G @ F) * (C @ (B @ A)) * (F @ G) != D @ (F @ G) # answer(A). [ur(1210,b,2495,a)]. given #603 (F,wt=19): 5415 (B @ A) * (D @ (F @ G)) * (A @ B) != C @ (B @ A) # answer(A). [ur(1210,b,2579,a(flip))]. given #604 (T,wt=13): 5391 (x @ (y @ z)) @ u * v * x = c_0. [para(3(a,1),5300(a,1,2))]. given #605 (T,wt=13): 5395 (x @ (y @ z)) @ x * (x @ u) = c_0. [para(908(a,1),5300(a,1,2))]. given #606 (A,wt=18): 368 x * y * z != z * x | z @ x = y * (y @ z). [para(4(a,1),43(a,1)),flip(a),flip(b)]. given #607 (F,wt=19): 5668 D @ (G @ F) != (F @ G) * (C @ (A @ B)) * (G @ F) # answer(A). [ur(1210,b,2954,a),flip(a)]. given #608 (F,wt=19): 5807 (A @ B) * (D @ (F @ G)) * (B @ A) != C @ (B @ A) # answer(A). [ur(1210,b,3111,a(flip))]. given #609 (T,wt=13): 5396 (x @ (y @ z)) @ x * (u @ x) = c_0. [para(1552(a,1),5300(a,1,2))]. given #610 (T,wt=13): 5409 y * x @ x * x * y * y = c_0. [para(265(a,1),318(a,1)),rewrite(3(10),3(9),3(8)),xx(a)]. given #611 (A,wt=22): 370 x * y * z != z * x * u | (z @ x) * u = y * (y @ z). [para(13(a,1),43(a,1)),flip(a),flip(b)]. given #612 (F,wt=19): 6375 (A @ B) * (D @ (G @ F)) * (B @ A) != C @ (A @ B) # answer(A). [ur(1210,b,4431,a(flip))]. given #613 (F,wt=19): 6377 (F @ G) * (C @ (B @ A)) * (G @ F) != D @ (F @ G) # answer(A). [ur(1210,b,4432,a)]. given #614 (T,wt=13): 5561 x * x * y * y @ y * x = c_0. [para(265(a,1),319(a,1)),rewrite(3(10),3(9),3(8)),xx(a)]. given #615 (T,wt=13): 5827 x * y * z @ (y * x @ z) = c_0. [para(5157(a,1),385(a,2)),rewrite(1554(5),4728(4),3457(5))]. given #616 (A,wt=24): 371 x * y * z != u * x * z | u * (u @ x * z) = y * (y @ z). [para(14(a,1),43(a,1)),flip(a),flip(b)]. given #617 (F,wt=21): 963 B * A * (D @ (F @ G)) * C * (A @ B) != A * B * C # answer(A). [ur(143,b,424,a(flip)),flip(a)]. given #618 (F,wt=21): 971 C * (D @ (F @ G)) * (A @ B) * x != (A @ B) * C * x # answer(A). [ur(576,b,912,a),rewrite(3(6),3(18),3(17)),flip(a)]. given #619 (T,wt=13): 6161 x * y @ (y * x @ (z @ u)) = c_0. [para(385(a,1),5312(a,1,2,2)),rewrite(3(6),4(6),2360(5))]. given #620 (T,wt=13): 6178 x @ (x * (x @ y) @ (z @ u)) = c_0. [para(908(a,1),5315(a,1,2,1))]. given #621 (A,wt=24): 373 x * y * z != z * u * x | y * (x * y @ z) = u * (u @ x). [para(15(a,1),43(a,1)),flip(b)]. given #622 (F,wt=17): 6583 C * (D @ (F @ G)) * A * B != C * A * B # answer(A). [para(397(a,1),971(a,2)),rewrite(1554(13),908(12),4(13))]. given #623 (F,wt=21): 1020 B * A * C * (D @ (F @ G)) * (A @ B) != A * B * C # answer(A). [ur(143,b,919,a(flip)),flip(a)]. given #624 (T,wt=13): 6179 x @ (x * (y @ x) @ (z @ u)) = c_0. [para(1552(a,1),5315(a,1,2,1))]. given #625 (T,wt=13): 6288 x * y @ ((z @ u) @ y * x) = c_0. [para(385(a,1),5342(a,1,1,2)),rewrite(3(3),4(3))]. given #626 (A,wt=22): 377 x * y * z * y * x != x * y | x @ y = z * x * y. [para(5(a,1),44(a,1))]. given #627 (F,wt=21): 1050 C * (A @ B) * D * (D @ (F @ G)) != (A @ B) * C * D # answer(A). [para(908(a,1),59(a,1,2,2))]. given #628 (F,wt=21): 1071 (D @ (F @ G)) * C * A * (A @ B) != (A @ B) * C * A # answer(A). [para(908(a,1),497(a,1,2,2))]. given #629 (T,wt=13): 6302 x @ ((y @ z) @ x * (x @ u)) = c_0. [para(908(a,1),5345(a,1,2,2))]. given #630 (T,wt=13): 6303 x @ ((y @ z) @ x * (u @ x)) = c_0. [para(1552(a,1),5345(a,1,2,2))]. given #631 (A,wt=22): 378 x * y * z * u != z * x | z @ x = y * (y @ z) * u. [para(13(a,1),44(a,1,2))]. given #632 (F,wt=21): 1218 x * D * (F @ G) * (C @ (A @ B)) != x * (F @ G) * D # answer(A). [para(1148(a,1),114(a,1,2,2,2)),rewrite(191(6)),flip(a)]. given #633 (F,wt=21): 1224 G * F * D * (F @ G) * (C @ (A @ B)) != F * G * D # answer(A). [para(1148(a,1),273(a,1,2,2,2)),rewrite(191(5)),flip(a)]. given #634 (T,wt=13): 6521 x * y * z @ (z @ y * x) = c_0. [hyper(2839,a,5827,a)]. given #635 (T,wt=15): 400 x * y * z @ x * y = z @ x * y. [para(3(a,1),385(a,1,1))]. given #636 (A,wt=20): 381 x * y * z != z * y | z @ y = x * (x @ y * z). [para(14(a,1),44(a,1))]. given #637 (F,wt=21): 1348 D * (F @ G) * (C @ (A @ B)) * x != (F @ G) * D * x # answer(A). [para(1185(a,1),62(a,1,2,2)),flip(a)]. given #638 (F,wt=21): 1357 x * (B @ A) * C * (A @ B) * (D @ (F @ G)) != x * C # answer(A). [para(1185(a,1),60(a,2,2))]. given #639 (T,wt=15): 636 x * y * x * (y @ x) = y * x * x. [para(525(a,1),4(a,1,2,2)),rewrite(191(5),416(4),3(6),3(5)),flip(a)]. given #640 (T,wt=15): 647 x * y * z * z @ (x * y @ z) = c_0. [para(3(a,1),642(a,1,1))]. given #641 (A,wt=24): 382 x * y * z * u != u * x | u @ x = y * z * (y * z @ u). [para(15(a,1),44(a,1,2))]. given #642 (F,wt=21): 1361 (B @ A) * C * (A @ B) * (D @ (F @ G)) * x != C * x # answer(A). [para(1185(a,1),88(a,2))]. given #643 (F,wt=21): 1394 (D @ (F @ G)) * C * x != (A @ B) * C * (B @ A) * x # answer(A). [para(1185(a,1),497(a,1,2,2))]. given #644 (T,wt=15): 744 x * y @ x * y * z = x * y @ z. [para(3(a,1),716(a,1,2))]. given #645 (T,wt=15): 906 x * (y @ x) * (x * (y @ x) @ y) = x. [hyper(83,a,849,a)]. given #646 (A,wt=20): 383 x * y * z != x * z | y * (x * y @ z) = x @ z. [para(15(a,1),44(a,1)),flip(b)]. given #647 (F,wt=21): 1501 D * (F @ G) * C * (C @ (A @ B)) != (F @ G) * D * C # answer(A). [para(1248(a,1),62(a,1,2,2)),flip(a)]. given #648 (F,wt=21): 1533 (D @ (F @ G)) * C * B != (A @ B) * C * B * (B @ A) # answer(A). [para(1248(a,1),497(a,1,2,2))]. given #649 (T,wt=11): 7025 x * (y @ x) @ y = x @ y. [hyper(1190,a,906,a),flip(a)]. given #650 (T,wt=11): 7074 x @ y * (x @ y) = x @ y. [para(7025(a,1),2334(a,1,2,2)),rewrite(3(4),1148(3),191(2)),flip(a)]. given #651 (A,wt=18): 391 x * (x @ y) != z * x | x @ y = z * (z @ x). [para(322(a,1),10(a,1)),rewrite(385(8)),flip(b)]. given #652 (F,wt=21): 1642 (D @ (F @ G)) * C * B * (A @ B) != (A @ B) * C * B # answer(A). [para(1552(a,1),497(a,1,2,2))]. given #653 (F,wt=21): 1715 (x @ y) * (C @ (A @ B)) * (D @ (F @ G)) * (y @ x) != c_0 # answer(A). [ur(1183,b,1304,a(flip))]. given #654 (T,wt=13): 7061 x * y * y @ y * x = y @ x. [para(385(a,1),7025(a,1,1,2)),rewrite(6936(4),716(6))]. given #655 (T,wt=13): 7062 x * (y @ x) @ y * x = x @ y. [para(7025(a,1),716(a,2)),rewrite(3(5),908(4),4(5))]. given #656 (A,wt=22): 395 x * y * (y @ z) != x * u * y | y @ z = u * (u @ y). [para(322(a,1),43(a,1,2)),rewrite(385(10)),flip(b)]. given #657 (F,wt=21): 1717 (x @ y) * (D @ (F @ G)) * (C @ (A @ B)) * (y @ x) != c_0 # answer(A). [ur(1183,b,1275,a(flip))]. given #658 (F,wt=21): 1785 x * (D @ (F @ G)) * C != x * (A @ B) * C * (B @ A) # answer(A). [ur(372,b,1231,a),flip(a)]. given #659 (T,wt=13): 7091 x * (y @ x) @ x * y = x @ y. [back_rewrite(6936),rewrite(7061(8))]. given #660 (T,wt=13): 7097 x * y @ y * (x @ y) = x @ y. [para(7074(a,1),385(a,2)),rewrite(3(3),908(2),4(3))]. given #661 (A,wt=18): 398 x * y * y * x != y * x * z | x * y = z. [para(181(a,1),45(a,1,2,2)),rewrite(181(9))]. given #662 (F,wt=19): 7203 (C @ (B @ A)) * x * C != x * (D @ (F @ G)) * C # answer(A). [para(397(a,2),1785(a,2)),rewrite(3031(17),2360(13),3(22),1148(21),191(16)),flip(a)]. given #663 (F,wt=19): 7262 (C @ (A @ B)) * x * (D @ (F @ G)) * C != x * C # answer(A). [ur(1210,b,7203,a),rewrite(2360(5))]. given #664 (T,wt=13): 7098 x * y @ y * x * x = y @ x. [para(385(a,1),7074(a,1,2,2)),rewrite(7012(4),385(6))]. given #665 (T,wt=13): 7119 x * y @ x * (y @ x) = y @ x. [back_rewrite(7012),rewrite(7098(8))]. given #666 (A,wt=17): 403 x * (x @ y) * z @ y = x * y * z @ y. [para(13(a,1),385(a,1,1)),flip(a)]. given #667 (F,wt=21): 1791 B * A * (D @ (F @ G)) * C != A * B * C * (B @ A) # answer(A). [ur(155,b,1231,a(flip))]. given #668 (F,wt=21): 1883 (B @ A) * (D @ (F @ G)) * C * (A @ B) * x != C * x # answer(A). [ur(576,b,1388,a),rewrite(3(18),3(17),3(16)),flip(a)]. given #669 (T,wt=14): 7040 x * y * y != y | y @ x = x * y. [back_rewrite(6884),rewrite(7025(6))]. given #670 (T,wt=14): 7042 x * y * y != x * y | y @ x = y. [back_rewrite(6856),rewrite(7025(7))]. given #671 (A,wt=25): 406 x * y * z * y * x * u @ y = x * z * x * y * u @ y. [para(19(a,1),385(a,1,1))]. given #672 (F,wt=21): 1884 x * (B @ A) * (D @ (F @ G)) * C * (A @ B) != x * C # answer(A). [ur(372,b,1388,a),flip(a)]. given #673 (F,wt=21): 1888 (F @ G) * D * x != (C @ (A @ B)) * D * (F @ G) * x # answer(A). [ur(576,b,1389,a),rewrite(3(12),3(11),3(18)),flip(a)]. given #674 (T,wt=14): 7081 x != y | (z @ x) * y = x * (z @ x). [para(7025(a,1),3869(a,1,2)),rewrite(3(4),1148(3),191(2),7074(4))]. given #675 (T,wt=14): 7082 x * y != x | y * (z @ y) = z @ y. [para(7025(a,1),3988(a,1,2,2)),rewrite(3(4),1148(3),191(2),7074(5)),flip(b)]. given #676 (A,wt=23): 407 x * y * z * y * x @ u = y * x * z * x * y @ u. [para(20(a,1),385(a,1,1)),rewrite(385(6))]. given #677 (F,wt=17): 7378 (C @ (A @ B)) * D * F * G != D * F * G # answer(A). [para(397(a,1),1888(a,1)),rewrite(1554(18),908(17),4(18)),flip(a)]. given #678 (F,wt=17): 7386 (C @ (B @ A)) * D * F * G != D * F * G # answer(A). [ur(1210,b,7378,a),rewrite(2360(5))]. given #679 (T,wt=15): 1037 (x @ y) * x * z = x * (x @ y) * z. [para(908(a,1),3(a,1,1)),rewrite(3(3)),flip(a)]. given #680 (T,wt=13): 7501 (x @ y) @ y * (y @ z) * x = c_0. [para(1037(a,1),4668(a,1,2))]. given #681 (A,wt=18): 421 x * (y @ z) * u != x * y * z | z * y = u. [para(396(a,1),7(a,1,2)),flip(a)]. given #682 (F,wt=17): 7394 (C @ (A @ B)) * F * G * D != F * G * D # answer(A). [ur(55,b,7378,a(flip)),rewrite(3(17),3(16),3(15),15(16),3(16))]. given #683 (F,wt=17): 7406 (C @ (B @ A)) * F * G * D != F * G * D # answer(A). [ur(55,b,7386,a(flip)),rewrite(3(17),3(16),3(15),15(16),3(16))]. given #684 (T,wt=13): 7503 x * (x @ y) * z @ (z @ x) = c_0. [para(1037(a,1),4670(a,1,1))]. given #685 (T,wt=13): 7505 x * (x @ y) * z @ (x @ z) = c_0. [para(1037(a,1),4690(a,1,1))]. given #686 (A,wt=18): 430 x * y * z != u * z * y | x * (y @ z) = u. [para(396(a,1),8(a,1,2))]. given #687 (F,wt=17): 7619 (C @ (A @ B)) * G * D * F != G * D * F # answer(A). [ur(55,b,7394,a(flip)),rewrite(3(17),3(16),3(15),15(16),3(16))]. given #688 (F,wt=17): 7630 (C @ (B @ A)) * G * D * F != G * D * F # answer(A). [ur(55,b,7406,a(flip)),rewrite(3(17),3(16),3(15),15(16),3(16))]. given #689 (T,wt=13): 7507 (x @ y) @ x * (x @ z) * y = c_0. [para(1037(a,1),4715(a,1,2))]. given #690 (T,wt=13): 7560 x * y @ (x @ (z @ x) * y) = c_0. [para(1185(a,1),7501(a,1,2,2)),rewrite(2360(5))]. given #691 (A,wt=18): 432 x * y * z * u != u * z | u @ z = x * y. [para(396(a,1),8(a,2)),flip(b)]. given #692 (F,wt=21): 1889 x * (F @ G) * D != x * (C @ (A @ B)) * D * (F @ G) # answer(A). [ur(372,b,1389,a),flip(a)]. given #693 (F,wt=21): 1890 G * F * (C @ (A @ B)) * D * (F @ G) != F * G * D # answer(A). [ur(155,b,1389,a)]. given #694 (T,wt=13): 7580 x * y @ (x * (z @ x) @ y) = c_0. [para(7025(a,1),7501(a,1,2,2,1)),rewrite(3(8),1185(7),2360(5))]. given #695 (T,wt=13): 7645 x * y @ ((z @ x) * y @ x) = c_0. [para(1185(a,1),7503(a,1,1,2))]. given #696 (A,wt=20): 433 x * (y @ z) != y * z | x * (x @ (y @ z)) = z * y. [para(396(a,1),10(a,1)),flip(a)]. given #697 (F,wt=21): 1969 (B @ A) * C * (D @ (F @ G)) * (A @ B) * x != C * x # answer(A). [ur(576,b,1419,a),rewrite(3(18),3(17),3(16)),flip(a)]. given #698 (F,wt=21): 1970 x * (B @ A) * C * (D @ (F @ G)) * (A @ B) != x * C # answer(A). [ur(372,b,1419,a),flip(a)]. given #699 (T,wt=13): 7667 x * y @ (y @ x * (z @ x)) = c_0. [para(7025(a,1),7503(a,1,1,2,1)),rewrite(3(5),1185(4))]. given #700 (T,wt=14): 7467 x * y * z != x * y | x * z = x. [para(1037(a,1),910(a,1,2)),rewrite(13(4)),flip(b)]. given #701 (A,wt=25): 445 x * y * (D @ (F @ G)) * C * (A @ B) != x * y * (A @ B) * C # answer(A). [para(396(a,1),41(a,1,2,2)),flip(a)]. given #702 (F,wt=21): 2405 (G @ F) * (C @ (B @ A)) * (F @ G) * (D @ (G @ F)) != c_0 # answer(A). [back_rewrite(2257),rewrite(2360(8),2360(16))]. given #703 (F,wt=21): 2426 A * B * (D @ (G @ F)) * C != B * A * C * (A @ B) # answer(A). [back_rewrite(2028),rewrite(2360(7))]. given #704 (T,wt=15): 1053 x * y * y * (y @ x) = y * x * y. [para(908(a,1),13(a,1,2,2))]. given #705 (T,wt=15): 1403 (x @ y) @ (y @ x) * z = (x @ y) @ z. [para(1185(a,1),716(a,1,2)),flip(a)]. given #706 (A,wt=25): 447 x * y * (y * z @ x) * y * x * z = y * x * y * z * x. [para(396(a,1),19(a,1,2,2)),rewrite(3(2)),flip(a)]. given #707 (F,wt=21): 2427 (A @ B) * (D @ (G @ F)) * C * x != C * (A @ B) * x # answer(A). [back_rewrite(2027),rewrite(2360(8))]. given #708 (F,wt=21): 2434 x * (G @ F) * D * (F @ G) != x * (C @ (B @ A)) * D # answer(A). [back_rewrite(1975),rewrite(2360(5)),flip(a)]. given #709 (T,wt=15): 1554 (x @ y) * y * z = y * (x @ y) * z. [para(1526(a,1),13(a,1,2,2,1)),rewrite(181(3))]. given #710 (T,wt=13): 8133 (x @ y) @ y * (z @ y) * x = c_0. [para(1554(a,1),4668(a,1,2))]. given #711 (A,wt=16): 449 x * y * z != z * y | x * (y @ z) = c_0. [para(396(a,1),185(a,1,2))]. given #712 (F,wt=19): 8038 (D @ (F @ G)) * x * D != x * (C @ (B @ A)) * D # answer(A). [para(397(a,2),2434(a,1)),rewrite(2360(9),2344(9),3(14),1148(13),191(8))]. given #713 (F,wt=19): 8244 (D @ (G @ F)) * x * (C @ (B @ A)) * D != x * D # answer(A). [ur(1210,b,8038,a),rewrite(2360(5))]. given #714 (T,wt=13): 8135 x * (y @ x) * z @ (z @ x) = c_0. [para(1554(a,1),4670(a,1,1))]. given #715 (T,wt=13): 8137 x * (y @ x) * z @ (x @ z) = c_0. [para(1554(a,1),4690(a,1,1))]. given #716 (A,wt=16): 455 x * (y @ z) != x * y * z | z * y = c_0. [para(396(a,1),194(a,1,2)),flip(a),flip(b)]. given #717 (F,wt=21): 2435 (G @ F) * D * (F @ G) * x != (C @ (B @ A)) * D * x # answer(A). [back_rewrite(1974),rewrite(2360(5)),flip(a)]. given #718 (F,wt=21): 2436 C * ((A @ B) @ C * (D @ (F @ G))) != C * (D @ (F @ G)) # answer(A). [back_rewrite(1972),rewrite(2360(16,R),2343(16))]. given #719 (T,wt=13): 8139 (x @ y) @ x * (z @ x) * y = c_0. [para(1554(a,1),4715(a,1,2))]. given #720 (T,wt=13): 8206 x * y @ (x @ (x @ z) * y) = c_0. [para(1185(a,1),8133(a,1,2,2)),rewrite(2360(5))]. given #721 (A,wt=22): 460 x * y * (z @ u) * v != x * y * z * u | u * z = v. [para(396(a,1),42(a,1,2,2)),flip(a)]. given #722 (F,wt=21): 2437 C * ((A @ B) @ (D @ (F @ G)) * C) != (D @ (F @ G)) * C # answer(A). [back_rewrite(1886),rewrite(2360(16,R),2343(16))]. given #723 (F,wt=21): 2440 x * (D @ (G @ F)) * (A @ B) * C != x * C * (A @ B) # answer(A). [back_rewrite(1828),rewrite(2360(5))]. given #724 (T,wt=13): 8209 x * y @ (x * (x @ z) @ y) = c_0. [para(2334(a,1),8133(a,1,2,2,1)),rewrite(3(8),1185(7),2360(5))]. given #725 (T,wt=13): 8228 x * y * z @ (y @ x * z) = c_0. [para(1037(a,1),8133(a,1,2,2)),rewrite(13(6),2360(5))]. given #726 (A,wt=24): 466 x * y * (z @ u) != x * z * u | y * (y @ (z @ u)) = u * z. [para(396(a,1),43(a,1,2)),flip(a)]. given #727 (F,wt=21): 2441 (D @ (G @ F)) * (A @ B) * C * x != C * (A @ B) * x # answer(A). [back_rewrite(1827),rewrite(2360(5))]. given #728 (F,wt=21): 2442 (F @ G) * D * D * (C @ (B @ A)) != D * (F @ G) * D # answer(A). [back_rewrite(1826),rewrite(2360(10))]. given #729 (T,wt=13): 8271 x * y @ ((x @ z) * y @ x) = c_0. [para(1185(a,1),8135(a,1,1,2))]. given #730 (T,wt=13): 8276 x * y @ (y @ x * (x @ z)) = c_0. [para(2334(a,1),8135(a,1,1,2,1)),rewrite(3(5),1185(4))]. given #731 (A,wt=18): 467 (x @ y) * z * y != x * y | z * (z @ y) = x. [para(396(a,1),43(a,1)),flip(a)]. given #732 (F,wt=21): 2451 x * (C @ (B @ A)) * (F @ G) * D * (G @ F) != x * D # answer(A). [back_rewrite(1803),rewrite(2360(5))]. given #733 (F,wt=21): 2453 D * (D * (C @ (B @ A)) @ (F @ G)) != D * (C @ (B @ A)) # answer(A). [back_rewrite(1783),rewrite(2360(7),2360(16,R),2343(16),2360(12),2360(19))]. given #734 (T,wt=13): 8296 x * y * z @ (x * z @ y) = c_0. [para(1037(a,1),8135(a,1,1,2)),rewrite(13(4))]. given #735 (T,wt=14): 8533 x * y != y * y | x * (x @ y) = y. [para(171(a,1),467(a,1,1)),rewrite(181(3))]. given #736 (A,wt=20): 469 (x @ y) * z != z * x * y | (x @ y) @ z = y * x. [para(396(a,1),44(a,1,2)),flip(a)]. given #737 (F,wt=21): 2461 x * (A @ B) * (D @ (G @ F)) * C != x * C * (A @ B) # answer(A). [back_rewrite(1753),rewrite(2360(8))]. given #738 (F,wt=21): 2466 (x @ y) * (C @ (B @ A)) * (D @ (G @ F)) * (y @ x) != c_0 # answer(A). [back_rewrite(1716),rewrite(2360(6),2360(11))]. given #739 (T,wt=15): 2316 x * (x @ y) @ y * (y @ x) = x @ y. [back_rewrite(2170),rewrite(2298(9),385(7))]. given #740 (T,wt=15): 2376 x * y * y * x @ (x * x @ y) = c_0. [back_rewrite(792),rewrite(2343(3),2360(6))]. given #741 (A,wt=22): 483 x * y * z * u * v != w * v | x * y * z * u = w. [para(3(a,1),52(a,1,2,2))]. given #742 (F,wt=21): 2467 (x @ y) * (D @ (G @ F)) * (C @ (B @ A)) * (y @ x) != c_0 # answer(A). [back_rewrite(1714),rewrite(2360(6),2360(11))]. given #743 (F,wt=21): 2483 (C @ (B @ A)) * (F @ G) * D * G != D * G * (F @ G) # answer(A). [back_rewrite(1644),rewrite(2360(5))]. given #744 (T,wt=15): 2377 x @ y * x * x * y = x @ y * y. [back_rewrite(766),rewrite(2343(3)),flip(a)]. given #745 (T,wt=15): 2380 x * y * y * x @ (y @ x * x) = c_0. [back_rewrite(694),rewrite(2343(6))]. given #746 (A,wt=22): 484 x * y * z * u != v * w * u | x * y * z = v * w. [para(3(a,1),52(a,2))]. given #747 (F,wt=21): 2489 (F @ G) * D * (C @ (B @ A)) * G != D * G * (F @ G) # answer(A). [back_rewrite(1625),rewrite(2360(9))]. given #748 (F,wt=21): 2490 (F @ G) * D * C * (C @ (B @ A)) != D * (F @ G) * C # answer(A). [back_rewrite(1624),rewrite(2360(10))]. given #749 (T,wt=15): 2581 x * y * z * z @ (z @ x * y) = c_0. [back_rewrite(1026),rewrite(2360(6))]. given #750 (T,wt=15): 2685 x * y * y * x @ y = x * x @ y. [back_rewrite(687),rewrite(2666(7))]. given #751 (A,wt=22): 485 x * y * (y @ z) != u * v * y * z | u * v * z = x. [para(4(a,1),52(a,1,2,2)),flip(a)]. given #752 (F,wt=21): 2499 (C @ (B @ A)) * (F @ G) * D * G * (G @ F) != D * G # answer(A). [back_rewrite(1534),rewrite(2360(5))]. given #753 (F,wt=21): 2502 (F @ G) * D * (C @ (B @ A)) * G * (G @ F) != D * G # answer(A). [back_rewrite(1502),rewrite(2360(9))]. given #754 (T,wt=15): 2842 (x @ (y @ z)) * (x @ (z @ y)) * u = u. [para(2360(a,1),1185(a,1,1))]. given #755 (T,wt=15): 2843 ((x @ y) @ z) * ((y @ x) @ z) * u = u. [para(2360(a,2),1185(a,1,1))]. given #756 (A,wt=18): 486 x * (y @ z) != u * y * z | u * z * y = x. [para(4(a,1),52(a,1,2)),flip(a)]. given #757 (F,wt=17): 8836 (C @ (B @ A)) * G * F * D != G * F * D # answer(A). [ur(486,b,7630,a(flip)),rewrite(3(15),3(14),3(13),4(13))]. given #758 (F,wt=17): 8837 (C @ (A @ B)) * G * F * D != G * F * D # answer(A). [ur(486,b,7619,a(flip)),rewrite(3(15),3(14),3(13),4(13))]. given #759 (T,wt=15): 2891 (x @ (y @ z)) @ u = u @ (x @ (z @ y)). [para(2360(a,1),2360(a,1,1))]. given #760 (T,wt=15): 2892 ((x @ y) @ z) @ u = u @ ((y @ x) @ z). [para(2360(a,2),2360(a,1,1))]. given #761 (A,wt=22): 487 x * y * z * u * (u @ v) != u * v | x * y * z = v. [para(4(a,1),52(a,2))]. given #762 (F,wt=17): 8838 (C @ (B @ A)) * F * D * G != F * D * G # answer(A). [ur(486,b,7406,a(flip)),rewrite(3(15),3(14),3(13),4(13))]. given #763 (F,wt=17): 8839 (C @ (A @ B)) * F * D * G != F * D * G # answer(A). [ur(486,b,7394,a(flip)),rewrite(3(15),3(14),3(13),4(13))]. given #764 (T,wt=15): 2893 (x @ y) @ (z @ u) = (y @ x) @ (u @ z). [para(2360(a,2),2360(a,1))]. given #765 (T,wt=15): 2909 (x @ (y @ z)) @ (u @ (x @ (z @ y))) = c_0. [para(2360(a,1),2836(a,1,1))]. given #766 (A,wt=22): 488 x * y * z * y * x != u * x * y | y * x * z = u. [para(5(a,1),52(a,1))]. given #767 (F,wt=17): 8840 (C @ (B @ A)) * D * G * F != D * G * F # answer(A). [ur(486,b,7386,a(flip)),rewrite(3(15),3(14),3(13),4(13))]. given #768 (F,wt=17): 8841 (C @ (A @ B)) * D * G * F != D * G * F # answer(A). [ur(486,b,7378,a(flip)),rewrite(3(15),3(14),3(13),4(13))]. given #769 (T,wt=15): 2910 ((x @ y) @ z) @ (u @ ((y @ x) @ z)) = c_0. [para(2360(a,2),2836(a,1,1))]. given #770 (T,wt=15): 2922 (x @ (y @ z)) @ ((x @ (z @ y)) @ u) = c_0. [para(2360(a,1),2844(a,1,1))]. given #771 (A,wt=22): 489 x * (y @ z) * u != v * y * z * u | v * z * y = x. [para(13(a,1),52(a,1,2)),flip(a)]. given #772 (F,wt=17): 8842 C * (D @ (F @ G)) * B * A != C * B * A # answer(A). [ur(486,b,6583,a(flip)),rewrite(3(15),3(14),3(13),4(13))]. given #773 (F,wt=17): 8843 (D @ (G @ F)) * B * A * C != B * A * C # answer(A). [ur(486,b,5189,a(flip)),rewrite(3(15),3(14),3(13),4(13))]. given #774 (T,wt=15): 2923 ((x @ y) @ z) @ (((y @ x) @ z) @ u) = c_0. [para(2360(a,2),2844(a,1,1))]. given #775 (T,wt=15): 2971 x * y * x @ x * (x @ y) = y @ x. [para(2298(a,1),2320(a,1,2,2)),rewrite(2344(7))]. given #776 (A,wt=20): 490 x * (y @ z * u) != y * z * u | z * u * y = x. [para(14(a,1),52(a,1)),flip(a)]. given #777 (F,wt=17): 8844 (D @ (F @ G)) * B * A * C != B * A * C # answer(A). [ur(486,b,5172,a(flip)),rewrite(3(15),3(14),3(13),4(13))]. given #778 (F,wt=17): 8845 (D @ (G @ F)) * A * C * B != A * C * B # answer(A). [ur(486,b,5029,a(flip)),rewrite(3(15),3(14),3(13),4(13))]. given #779 (T,wt=15): 2983 (x @ y) @ y * x * x * (y @ x) = c_0. [para(2298(a,1),2324(a,1,1)),rewrite(2344(4),3(5))]. given #780 (T,wt=15): 3004 x * (x @ y) @ x * y * x = x @ y. [para(2298(a,1),2340(a,1,1,2)),rewrite(2298(7))]. given #781 (A,wt=24): 491 x * y * (z * y @ u) != v * z * y * u | v * u * z = x. [para(15(a,1),52(a,1,2)),flip(a)]. given #782 (F,wt=17): 8846 (D @ (F @ G)) * A * C * B != A * C * B # answer(A). [ur(486,b,5013,a(flip)),rewrite(3(15),3(14),3(13),4(13))]. given #783 (F,wt=17): 8847 (D @ (G @ F)) * C * B * A != C * B * A # answer(A). [ur(486,b,5000,a(flip)),rewrite(3(15),3(14),3(13),4(13))]. given #784 (T,wt=15): 3031 (x @ y) @ z * (y @ x) = (x @ y) @ z. [para(1148(a,1),2343(a,1,2,2)),rewrite(191(3)),flip(a)]. given #785 (T,wt=15): 3094 x * y * y @ y * (y @ x) = x @ y. [para(2298(a,1),2384(a,1,2,2)),rewrite(3(2),2344(7))]. given #786 (A,wt=20): 492 x * (y * z @ u) != y * z * u | u * y * z = x. [para(15(a,1),52(a,1)),flip(a)]. given #787 (F,wt=17): 8848 (D @ (F @ G)) * C * B * A != C * B * A # answer(A). [ur(486,b,4705,a(flip)),rewrite(3(15),3(14),3(13),4(13))]. given #788 (F,wt=19): 9358 (D @ (G @ F)) * x * D != x * (C @ (A @ B)) * D # answer(A). [ur(490,b,2458,a),rewrite(5300(16),191(10)),flip(a)]. given #789 (T,wt=15): 3122 x * (x @ y) @ y * x * x = x @ y. [para(2298(a,1),2385(a,1,1,2)),rewrite(3(4),2298(7))]. given #790 (T,wt=15): 3231 x * y * y * y * y @ (x @ y) = c_0. [para(2344(a,1),2669(a,1,2)),rewrite(3(4))]. given #791 (A,wt=22): 493 x * y * z * u != v * u * z | x * y * (z @ u) = v. [para(396(a,1),52(a,1,2,2))]. ============================== PROOF ================================= % Proof 1 at 4.85 (+ 0.07) seconds: A. % Length of proof is 103. % Level of proof is 31. % Maximum clause weight is 23. % Given clauses 791. 1 x * y != x * z | y = z. [assumption]. 2 x * y != z * y | x = z. [assumption]. 3 (x * y) * z = x * y * z. [assumption]. 4 x * y * (y @ x) = y * x. [assumption]. 5 x * y * z * y * x = y * x * z * x * y. [assumption]. 6 (A @ B) @ C != D @ (F @ G) # answer(A). [assumption]. 7 x * y * z != x * y * u | z = u. [para(3(a,1),1(a,1)),rewrite(3(4))]. 8 x * y * z != u * z | x * y = u. [para(3(a,1),2(a,1))]. 9 x * (x @ x) = x. [hyper(1,a,4,a)]. 10 x * y != z * x | z * (z @ x) = y. [para(4(a,1),1(a,1)),flip(a)]. 11 x * y * (y @ z) != y * z | z = x. [para(4(a,1),2(a,1)),flip(a)]. 13 x * y * (y @ x) * z = y * x * z. [para(4(a,1),3(a,1,1)),rewrite(3(2),3(5)),flip(a)]. 14 x * y * z * (z @ x * y) = z * x * y. [para(4(a,1),3(a,1)),flip(a)]. 23 ((A @ B) @ C) * x != (D @ (F @ G)) * x # answer(A). [ur(2,b,6,a)]. 29 x * y != x | x @ x = y. [para(9(a,1),1(a,1)),flip(a)]. 32 x * (x @ x) * y = x * y. [para(9(a,1),3(a,1,1)),flip(a)]. 43 x * y * z != x * u * y | u * (u @ y) = z. [para(4(a,1),7(a,1,2)),flip(a)]. 45 x * y * z * y * x != y * x * u | z * x * y = u. [para(5(a,1),7(a,1))]. 52 x * y * z * u != v * u | x * y * z = v. [para(3(a,1),8(a,1,2))]. 53 x * y * z != u * v * z | x * y = u * v. [para(3(a,1),8(a,2))]. 65 (x @ x) * y = y. [hyper(7,a,32,a)]. 73 x * y != y | z @ z = x. [para(65(a,1),2(a,1)),flip(a)]. 74 x * ((y @ y) @ x) = x. [para(65(a,1),4(a,1,2)),rewrite(65(5))]. 81 x * y * (x * y @ x) = y * x. [hyper(10,a,3,a(flip)),rewrite(3(4))]. 82 x * y * z != u * x * y | u * (u @ x * y) = z. [para(3(a,1),10(a,1))]. 92 (x @ x) @ y = y @ y. [hyper(29,a,74,a),flip(a)]. 100 x * y * z != x * y | (u @ u) @ y = z. [para(74(a,1),7(a,1,2)),flip(a)]. 121 ((x @ x) @ y) * z = z. [para(92(a,2),65(a,1,1))]. 122 x * (((y @ y) @ z) @ x) = x. [para(92(a,2),74(a,1,2,1))]. 131 x * (x @ ((y @ y) @ z)) = x * ((y @ y) @ z). [hyper(10,a,121,a)]. 137 x * y != x | ((z @ z) @ u) @ x = y. [para(121(a,1),10(a,2)),rewrite(121(8))]. 140 x * (x @ y) != x * y | (z @ z) @ u = y. [para(121(a,1),11(a,1)),flip(b)]. 141 (((x @ x) @ y) @ z) * u = u. [para(92(a,2),121(a,1,1,1))]. 143 x * y * z != y * u | x * (x @ y) * z = u. [para(13(a,1),1(a,1))]. 148 x * y * z * (z @ (x @ y)) = y * x * z * (x @ y). [para(4(a,1),13(a,1,2,2)),flip(a)]. 166 (x @ x) @ y = z @ z. [hyper(73,a,121,a),flip(a)]. 167 x @ x = y @ y. [hyper(73,a,65,a)]. 171 x @ x = c_0. [new_symbol(167)]. 175 c_0 @ x = c_0. [back_rewrite(166),rewrite(171(1),171(3))]. 181 c_0 * x = x. [back_rewrite(141),rewrite(171(1),175(2),175(2))]. 182 x * (x @ y) != x * y | c_0 = y. [back_rewrite(140),rewrite(171(5),175(6))]. 184 x * y != x | c_0 = y. [back_rewrite(137),rewrite(171(3),175(4),175(4))]. 188 x * (x @ c_0) = x * c_0. [back_rewrite(131),rewrite(171(1),175(2),171(4),175(5))]. 191 x * c_0 = x. [back_rewrite(122),rewrite(171(1),175(2),175(2))]. 194 x * y * z != x * y | c_0 = z. [back_rewrite(100),rewrite(171(5),175(6))]. 196 x * (x @ c_0) = x. [back_rewrite(188),rewrite(191(5))]. 197 x * y * (y @ y * x) = y * x. [hyper(1,a,14,a)]. 246 x @ c_0 = c_0. [hyper(184,a,196,a),flip(a)]. 299 x * y != y * x | x @ y = c_0. [para(4(a,1),194(a,1)),flip(b)]. 322 x * (y * x @ y) = x * (x @ y). [hyper(10,a,81,a),flip(a)]. 352 x * (x @ x * y) = x * (x @ y). [hyper(10,a,197,a),flip(a)]. 372 x * y != x * z | z = y. [para(181(a,1),43(a,1,2)),rewrite(191(3),246(5),191(5))]. 385 x * y @ x = y @ x. [hyper(372,a,322,a),flip(a)]. 396 (x @ y) * y * x = x * y. [hyper(45,a,13,a)]. 397 (x @ y) * z * y * x = z * x * y. [hyper(45,a,13,a(flip)),flip(a)]. 401 x * (x @ y) @ y = x * y @ y. [para(4(a,1),385(a,1,1)),flip(a)]. 420 ((A @ B) @ C) * (F @ G) * D != D * (F @ G) # answer(A). [para(396(a,1),23(a,2))]. 459 y * x @ (x @ y) = c_0. [para(396(a,1),299(a,2)),rewrite(3(3),4(3)),xx(a)]. 471 x * y @ (x @ y) = c_0. [para(396(a,1),385(a,1,1)),rewrite(459(6))]. 493 x * y * z * u != v * u * z | x * y * (z @ u) = v. [para(396(a,1),52(a,1,2,2))]. 498 ((A @ B) @ C) * (F @ G) * D * x != D * (F @ G) * x # answer(A). [ur(52,b,420,a),rewrite(3(18))]. 510 x * y @ (y @ x * (x @ y)) = c_0. [para(4(a,1),471(a,1,1))]. 528 (x @ y * x) * y * x = x * y. [hyper(53,a,396,a)]. 716 x @ x * y = x @ y. [hyper(372,a,352,a),flip(a)]. 734 x * (x @ y * x) = (x @ y) * x. [hyper(82,a,13,a)]. 745 x @ y * (y @ x) = x @ y * x. [para(4(a,1),716(a,1,2)),flip(a)]. 772 x * y @ (y @ x * y) = c_0. [back_rewrite(510),rewrite(745(4))]. 849 x * (y @ x) * y = y * x. [para(772(a,1),4(a,1,2,2)),rewrite(191(5),528(4),3(5),734(4)),flip(a)]. 908 (x @ y) * x = x * (x @ y). [hyper(10,a,849,a),flip(a)]. 953 x * (x @ y * x) = x * (x @ y). [back_rewrite(734),rewrite(908(5))]. 961 x * (x @ y) * (y @ x) = x. [hyper(143,a,4,a)]. 1148 (x @ y) * (y @ x) = c_0. [hyper(184,a,961,a),flip(a)]. 1149 (x @ y) * (y @ x) * x = (y @ x) * x * (x @ y). [para(961(a,1),5(a,1,2,2)),rewrite(908(3),1148(9),191(8)),flip(a)]. 1185 (x @ y) * (y @ x) * z = z. [para(1148(a,1),3(a,1,1)),rewrite(181(2)),flip(a)]. 1233 ((A @ B) @ C) * (F @ G) * D * (G @ F) != D # answer(A). [para(1148(a,1),498(a,2,2)),rewrite(191(18))]. 1248 (x @ y) * y * (y @ x) = y. [back_rewrite(1149),rewrite(1185(4)),flip(a)]. 1382 (x @ y) * z @ (y @ x) = z @ (y @ x). [para(1185(a,1),385(a,1,1)),flip(a)]. 1403 (x @ y) @ (y @ x) * z = (x @ y) @ z. [para(1185(a,1),716(a,1,2)),flip(a)]. 1517 x * (x @ y) @ (y @ x) = c_0. [para(1248(a,1),299(a,2)),rewrite(3(4),1148(3),191(2)),xx(a)]. 1526 x @ (y @ x) = c_0. [para(1248(a,1),385(a,1,1)),rewrite(1517(6))]. 1835 x * (x @ y) @ y * (y @ x) = y * x @ y * (y @ x). [para(4(a,1),401(a,2,1)),rewrite(745(3),953(3))]. 1843 x * (x @ y) @ x * y = x * x * y @ x * y. [para(716(a,1),401(a,1,1,2))]. 2149 x * y @ x * (x @ y) = x * y @ x * x * y. [para(716(a,1),745(a,1,2,2))]. 2169 x * x * y @ x * y = y * x @ y * y * x. [para(745(a,1),745(a,1,2,2)),rewrite(953(5),1835(5),2149(4),4(9),1843(8)),flip(a)]. 2298 x @ y * x = x @ y. [hyper(372,a,953,a),flip(a)]. 2317 x * x * y @ x * y = x @ y. [back_rewrite(2169),rewrite(2298(8),385(6))]. 2320 x * y @ x * (x @ y) = y @ x. [back_rewrite(2149),rewrite(2298(8),385(6))]. 2340 x * (x @ y) @ x * y = x @ y. [back_rewrite(1843),rewrite(2317(8))]. 2343 x @ y * z * x = x @ y * z. [para(3(a,1),2298(a,1,2))]. 2344 x * y @ y = x @ y. [para(4(a,1),2298(a,1,2)),rewrite(2340(4),401(4)),flip(a)]. 2360 (x @ y) @ z = z @ (y @ x). [para(1185(a,1),2298(a,1,2)),rewrite(2344(3),1382(6))]. 2551 (C @ (B @ A)) * (F @ G) * D * (G @ F) != D # answer(A). [back_rewrite(1233),rewrite(2360(5))]. 2844 (x @ y) @ ((y @ x) @ z) = c_0. [para(2360(a,2),1526(a,1,2))]. 2919 x * ((y @ z) @ x) = (y @ z) * x * (z @ y). [para(2844(a,1),148(a,1,2,2,2)),rewrite(191(4),1185(10)),flip(a)]. 3009 x * y @ y * y * x = x @ y. [para(2320(a,1),2340(a,1,1,2)),rewrite(3(3),4(3),3(5),4(4),2320(8))]. 3531 (x @ y) @ z = z @ (y @ x) * z * (y @ x) * z * (x @ y). [para(1185(a,1),3009(a,1,1)),rewrite(3(6),3(7),1403(12)),flip(a)]. 4670 x * z * y @ (y @ z) = c_0. [para(397(a,1),299(a,2)),rewrite(3(4),3(3),4(3)),xx(a)]. 5118 x * y @ ((z @ u) @ y) = c_0. [para(1185(a,1),4670(a,1,1,2)),rewrite(2360(5,R),716(5))]. 5337 x * (y @ z) * u * (z @ y) != x * u | (y @ z) @ u = c_0. [para(5118(a,1),182(a,1,2)),rewrite(191(3),3(5),2919(4)),flip(a),flip(b)]. 9565 (x @ y) * z * (y @ x) = z. [hyper(493,a,397,a)]. 9611 (z @ u) @ y = c_0. [back_rewrite(5337),rewrite(9565(4)),xx(a)]. 9651 x @ (y @ z) = c_0. [back_rewrite(3531),rewrite(9611(2),9565(6),2343(5),2298(4)),flip(a)]. 9654 $F # answer(A). [back_rewrite(2551),rewrite(9651(5),9565(10),181(3)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=791. Generated=157985. Kept=9653. proofs=1. Usable=600. Sos=6823. Demods=3113. Limbo=89, Disabled=2147. Hints=0. Weight_deleted=64549. Literals_deleted=0. Forward_subsumed=81830. Back_subsumed=187. Sos_limit_deleted=1952. Sos_displaced=0. Sos_removed=0. New_demodulators=4281 (1 lex), Back_demodulated=1954. Back_unit_deleted=0. Demod_attempts=3503502. Demod_rewrites=448237. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=646335. Nonunit_bsub_feature_tests=50496. Megabytes=7.95. User_CPU=4.85, System_CPU=0.07, Wall_clock=5. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11359 exit (max_proofs) Sat Aug 12 21:00:02 2006