============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13125 was started by mccune on cleo.thornwood, Mon Jun 19 16:41:35 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). clauses(sos). x * y != x * z | y = z. x * y != z * y | x = z. (x * y) * z = x * y * z. x * y * (y @ x) = y * x. end_of_list. % Reading from file EA.in clauses(sos). x * y * z * y * x = y * x * z * x * y. end_of_list. clauses(sos). (A @ B) @ C != D @ (F @ G) # answer(A). end_of_list. ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 x * y != x * z | y = z. [input]. 2 x * y != z * y | x = z. [input]. 3 (x * y) * z = x * y * z. [input]. 4 x * y * (y @ x) = y * x. [input]. 5 x * y * z * y * x = y * x * z * x * y. [input]. 6 (A @ B) @ C != D @ (F @ G) # answer(A). [input]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). Auto_denials: no changes. Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ A, B, C, D, F, G, *, @ ]). After inverse_order: Function symbol precedence: lex([ A, B, C, D, F, G, *, @ ]). 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: clauses(usable). end_of_list. clauses(sos). 7 x * y != x * z | y = z. [input]. 8 x * y != z * y | x = z. [input]. 9 (x * y) * z = x * y * z. [input]. 10 x * y * (y @ x) = y * x. [input]. 11 x * y * z * y * x = y * x * z * x * y. [input]. 12 (A @ B) @ C != D @ (F @ G) # answer(A). [input]. end_of_list. clauses(demodulators). 9 (x * y) * z = x * y * z. [input]. 10 x * y * (y @ x) = y * x. [input]. end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=10): 7 x * y != x * z | y = z. [input]. given #2 (I,wt=10): 8 x * y != z * y | x = z. [input]. given #3 (I,wt=11): 9 (x * y) * z = x * y * z. [input]. given #4 (I,wt=11): 10 x * y * (y @ x) = y * x. [input]. given #5 (I,wt=19): 11 x * y * z * y * x = y * x * z * x * y. [input]. given #6 (I,wt=11): 12 (A @ B) @ C != D @ (F @ G) # answer(A). [input]. given #7 (F,wt=15): 29 ((A @ B) @ C) * x != (D @ (F @ G)) * x # answer(A). [ur(8,b,12,a)]. given #8 (F,wt=15): 30 x * ((A @ B) @ C) != x * (D @ (F @ G)) # answer(A). [ur(7,b,12,a)]. given #9 (T,wt=7): 15 x * (x @ x) = x. [hyper(7,a,10,a)]. given #10 (T,wt=10): 35 x * y != x | x @ x = y. [para(15(a,1),7(a,1)),flip(a)]. given #11 (A,wt=14): 13 x * y * z != x * y * u | z = u. [para(9(a,1),7(a,1)),demod(9(4))]. given #12 (F,wt=19): 31 x * ((A @ B) @ C) * y != x * (D @ (F @ G)) * y # answer(A). [ur(7,b,29,a)]. given #13 (F,wt=19): 34 x * y * ((A @ B) @ C) != x * y * (D @ (F @ G)) # answer(A). [ur(7,b,30,a)]. given #14 (T,wt=10): 36 x * (y @ y) != y | y = x. [para(15(a,1),8(a,1)),flip(a)]. given #15 (T,wt=10): 37 x * (y @ y) != y | x = y. [para(15(a,1),8(a,2))]. given #16 (A,wt=14): 14 x * y * z != u * z | x * y = u. [para(9(a,1),8(a,1))]. given #17 (F,wt=17): 55 C * (A @ B) * (D @ (F @ G)) != (A @ B) * C # answer(A). [para(10(a,1),34(a,1)),flip(a)]. given #18 (F,wt=17): 56 (F @ G) * D * ((A @ B) @ C) != D * (F @ G) # answer(A). [para(10(a,1),34(a,2))]. given #19 (T,wt=11): 38 x * (x @ x) * y = x * y. [para(15(a,1),9(a,1,1)),flip(a)]. given #20 (T,wt=7): 71 (x @ x) * y = y. [hyper(13,a,38,a)]. given #21 (A,wt=14): 16 x * y != z * x | z * (z @ x) = y. [para(10(a,1),7(a,1)),flip(a)]. given #22 (F,wt=21): 65 C * (A @ B) * (D @ (F @ G)) * x != (A @ B) * C * x # answer(A). [ur(14,b,55,a),demod(9(11),9(18))]. given #23 (F,wt=21): 67 x * C * (A @ B) * (D @ (F @ G)) != x * (A @ B) * C # answer(A). [ur(7,b,55,a)]. given #24 (T,wt=6): 92 x != y | y = x. [para(15(a,1),16(a,2)),demod(71(2),81(4),15(3))]. given #25 (T,wt=9): 80 x * ((y @ y) @ x) = x. [para(71(a,1),10(a,1,2)),demod(71(5))]. given #26 (A,wt=14): 17 x * y * (y @ z) != y * z | z = x. [para(10(a,1),8(a,1)),flip(a)]. given #27 (F,wt=21): 68 (F @ G) * D * ((A @ B) @ C) * x != D * (F @ G) * x # answer(A). [ur(14,b,56,a),demod(9(11),9(18))]. given #28 (F,wt=21): 70 x * (F @ G) * D * ((A @ B) @ C) != x * D * (F @ G) # answer(A). [ur(7,b,56,a)]. given #29 (T,wt=9): 86 x * (x @ x * x) = x. [hyper(16,a,9,a)]. given #30 (T,wt=9): 98 (x @ x) @ y = y @ y. [hyper(35,a,80,a),flip(a)]. given #31 (A,wt=14): 18 x * y * (y @ z) != y * z | x = z. [para(10(a,1),8(a,2))]. given #32 (F,wt=21): 97 C * (A @ B) * (D @ (F @ G)) * (C @ C) != (A @ B) * C # answer(A). [para(15(a,1),65(a,2,2))]. given #33 (F,wt=21): 104 (D @ (F @ G)) * ((x @ x) @ ((A @ B) @ C)) != (A @ B) @ C # answer(A). [para(80(a,1),29(a,1)),flip(a)]. given #34 (T,wt=9): 125 x @ x * x = x @ x. [hyper(35,a,86,a),flip(a)]. given #35 (T,wt=9): 127 ((x @ x) @ y) * z = z. [para(98(a,2),71(a,1,1))]. given #36 (A,wt=15): 19 x * y * (y @ x) * z = y * x * z. [para(10(a,1),9(a,1,1)),demod(9(2),9(5)),flip(a)]. given #37 (F,wt=21): 105 ((A @ B) @ C) * ((x @ x) @ (D @ (F @ G))) != D @ (F @ G) # answer(A). [para(80(a,1),29(a,2))]. given #38 (F,wt=23): 32 (D @ (F @ G)) * x * (x @ ((A @ B) @ C)) != x * ((A @ B) @ C) # answer(A). [para(10(a,1),29(a,1)),flip(a)]. given #39 (T,wt=10): 79 x * y != y | z @ z = x. [para(71(a,1),8(a,1)),flip(a)]. NOTE: New constant: 0 x @ x = c_0. [new_symbol(173)]. NOTE: New Function symbol precedence: lex([ A, B, C, D, F, G, c_0, *, @ ]). given #40 (T,wt=5): 177 x @ x = c_0. [new_symbol(173)]. given #41 (A,wt=17): 20 x * y * z * (z @ x * y) = z * x * y. [para(10(a,1),9(a,1)),flip(a)]. given #42 (F,wt=23): 33 ((A @ B) @ C) * x * (x @ (D @ (F @ G))) != x * (D @ (F @ G)) # answer(A). [para(10(a,1),29(a,2))]. given #43 (F,wt=23): 46 x * y * z * ((A @ B) @ C) != x * y * z * (D @ (F @ G)) # answer(A). [ur(13,b,30,a)]. given #44 (T,wt=5): 181 c_0 @ x = c_0. [back_demod(172),demod(177(1),177(3))]. given #45 (T,wt=5): 187 c_0 * x = x. [back_demod(147),demod(177(1),181(2),181(2))]. given #46 (A,wt=17): 21 x * y * z * (y * z @ x) = y * z * x. [para(9(a,1),10(a,1,2)),demod(9(7))]. given #47 (F,wt=23): 47 x * y * ((A @ B) @ C) * z != x * y * (D @ (F @ G)) * z # answer(A). [ur(13,b,29,a)]. given #48 (F,wt=23): 53 x * (D @ (F @ G)) * (((A @ B) @ C) @ x) != ((A @ B) @ C) * x # answer(A). [para(10(a,1),31(a,1)),flip(a)]. given #49 (T,wt=5): 197 x * c_0 = x. [back_demod(128),demod(177(1),181(2),181(2))]. given #50 (T,wt=7): 198 x @ x * x = c_0. [back_demod(125),demod(177(3))]. given #51 (A,wt=22): 22 x * y * z * y * x != y * u | x * z * x * y = u. [para(11(a,1),7(a,1))]. given #52 (F,wt=19): 227 (D @ (F @ G)) * (((A @ B) @ C) @ c_0) != (A @ B) @ C # answer(A). [para(187(a,1),53(a,1)),demod(197(20))]. given #53 (F,wt=23): 54 x * ((A @ B) @ C) * ((D @ (F @ G)) @ x) != (D @ (F @ G)) * x # answer(A). [para(10(a,1),31(a,2))]. given #54 (T,wt=7): 202 x * (x @ c_0) = x. [back_demod(194),demod(197(5))]. given #55 (T,wt=8): 190 x * y != x | c_0 = y. [back_demod(143),demod(177(3),181(4),181(4))]. given #56 (A,wt=22): 23 x * y * z * y * u != y * u * z * u * y | u = x. [para(11(a,1),8(a,1)),flip(a)]. given #57 (F,wt=23): 96 C * (A @ B) * (D @ (F @ G)) * (C @ (A @ B)) != C * (A @ B) # answer(A). [para(10(a,1),65(a,2))]. given #58 (F,wt=23): 122 (F @ G) * D * ((A @ B) @ C) * ((F @ G) @ D) != (F @ G) * D # answer(A). [para(10(a,1),68(a,2))]. given #59 (T,wt=5): 252 x @ c_0 = c_0. [hyper(190,a,202,a),flip(a)]. given #60 (T,wt=8): 193 x * y != y | c_0 = x. [back_demod(138),demod(177(3),181(4))]. given #61 (A,wt=22): 24 x * y * z * y * u != y * u * z * u * y | x = u. [para(11(a,1),8(a,2))]. given #62 (F,wt=25): 66 x * y * C * (A @ B) * (D @ (F @ G)) != x * y * (A @ B) * C # answer(A). [ur(13,b,55,a)]. given #63 (F,wt=21): 264 B * A * C * (A @ B) * (D @ (F @ G)) != A * B * C # answer(A). [para(19(a,1),66(a,2))]. given #64 (T,wt=9): 216 x * (x * x @ x) = x. [hyper(13,a,21,a)]. given #65 (T,wt=7): 267 x * x @ x = c_0. [hyper(190,a,216,a),flip(a)]. given #66 (A,wt=23): 25 x * y * z * y * x * u = y * x * z * x * y * u. [para(11(a,1),9(a,1,1)),demod(9(5),9(4),9(3),9(2),9(9),9(8),9(7))]. given #67 (F,wt=25): 69 x * y * (F @ G) * D * ((A @ B) @ C) != x * y * D * (F @ G) # answer(A). [ur(13,b,56,a)]. given #68 (F,wt=21): 278 F * G * D * ((A @ B) @ C) != G * F * D * (F @ G) # answer(A). [para(19(a,1),69(a,1))]. given #69 (T,wt=10): 117 x * y != y * y | y = x. [para(15(a,1),17(a,1,2))]. given #70 (T,wt=12): 188 x * (x @ y) != x * y | c_0 = y. [back_demod(146),demod(177(5),181(6))]. given #71 (A,wt=23): 26 x * y * z * u * z * y = x * z * y * u * y * z. [para(11(a,1),9(a,2,2)),demod(9(5))]. given #72 (F,wt=25): 94 x * C * (A @ B) * (D @ (F @ G)) * y != x * (A @ B) * C * y # answer(A). [ur(7,b,65,a)]. given #73 (F,wt=25): 95 C * (A @ B) * (D @ (F @ G)) * x * (x @ C) != (A @ B) * x * C # answer(A). [para(10(a,1),65(a,2,2))]. given #74 (T,wt=12): 191 x * y * z != z | x * y = c_0. [back_demod(142),demod(177(4),181(5)),flip(b)]. given #75 (T,wt=12): 199 x * y != y | x * (x @ y) = c_0. [back_demod(112),demod(177(3),181(4)),flip(b)]. given #76 (A,wt=23): 27 x * y * z * u * y * x = y * x * z * u * x * y. [para(9(a,1),11(a,1,2,2)),demod(9(8))]. given #77 (F,wt=25): 120 x * (F @ G) * D * ((A @ B) @ C) * y != x * D * (F @ G) * y # answer(A). [ur(7,b,68,a)]. given #78 (F,wt=25): 121 D * (F @ G) * (((A @ B) @ C) @ D) != (F @ G) * ((A @ B) @ C) * D # answer(A). [para(10(a,1),68(a,1,2)),flip(a)]. given #79 (T,wt=12): 200 x * y * z != x * y | c_0 = z. [back_demod(106),demod(177(5),181(6))]. given #80 (T,wt=12): 287 x @ y != x * y | y * x = c_0. [para(10(a,1),191(a,1)),flip(a)]. given #81 (A,wt=23): 28 x * (x @ y) * y * (x @ y) * x = (x @ y) * x * x * y. [para(10(a,1),11(a,1,2,2)),flip(a)]. given #82 (F,wt=25): 215 (F @ G) * ((A @ B) @ C) * D * (D @ (D @ (F @ G))) != D * (F @ G) # answer(A). [ur(16,b,33,a(flip))]. given #83 (F,wt=25): 265 B * A * C * (A @ B) * (D @ (F @ G)) * x != A * B * C * x # answer(A). [ur(14,b,264,a),demod(9(15),9(14),9(13),9(22),9(21))]. given #84 (T,wt=12): 305 x * y != y * x | x @ y = c_0. [para(10(a,1),200(a,1)),flip(b)]. given #85 (T,wt=13): 87 x * y * (x * y @ x) = y * x. [hyper(16,a,9,a(flip)),demod(9(4))]. given #86 (A,wt=18): 48 x * y * z * u != x * y * z * v | u = v. [para(9(a,1),13(a,1,2)),demod(9(5))]. given #87 (F,wt=25): 266 x * B * A * C * (A @ B) * (D @ (F @ G)) != x * A * B * C # answer(A). [ur(7,b,264,a)]. given #88 (F,wt=25): 279 F * G * D * ((A @ B) @ C) * x != G * F * D * (F @ G) * x # answer(A). [ur(14,b,278,a),demod(9(11),9(10),9(22),9(21),9(20))]. given #89 (T,wt=13): 195 x * y @ x * y * x * y = c_0. [back_demod(135),demod(177(8))]. given #90 (T,wt=13): 203 x * y * (y @ y * x) = y * x. [hyper(7,a,20,a)]. given #91 (A,wt=18): 49 x * y * z != x * u * y | u * (u @ y) = z. [para(10(a,1),13(a,1,2)),flip(a)]. given #92 (F,wt=23): 355 F * G * D * ((A @ B) @ C) * ((F @ G) @ D) != F * G * D # answer(A). [para(10(a,1),279(a,2,2,2)),demod(19(26))]. given #93 (F,wt=25): 280 x * F * G * D * ((A @ B) @ C) != x * G * F * D * (F @ G) # answer(A). [ur(7,b,278,a)]. given #94 (T,wt=10): 378 x * y != x * z | z = y. [para(187(a,1),49(a,1,2)),demod(197(3),252(5),197(5))]. given #95 (T,wt=13): 269 x * y * x * y @ x * y = c_0. [para(9(a,1),267(a,1,1))]. given #96 (A,wt=14): 50 x * y * z != y * x | y @ x = z. [para(10(a,1),13(a,1)),flip(a)]. given #97 (F,wt=25): 323 B * A * C * (A @ B) * (D @ (F @ G)) * (C @ B) != A * C * B # answer(A). [para(10(a,1),265(a,2,2))]. given #98 (F,wt=25): 333 x * (D @ (F @ G)) * (x * ((A @ B) @ C) @ x) != ((A @ B) @ C) * x # answer(A). [para(87(a,1),31(a,1)),flip(a)]. given #99 (T,wt=12): 390 x * y != y * x | y @ x = c_0. [para(197(a,1),50(a,1,2))]. given #100 (T,wt=13): 328 x * (y * x @ y) = x * (x @ y). [hyper(16,a,87,a),flip(a)]. given #101 (A,wt=22): 51 x * y * z * y * x != y * x * u | z * x * y = u. [para(11(a,1),13(a,1))]. given #102 (F,wt=25): 363 C * (A @ B) * (D @ (F @ G)) * (C @ C * (A @ B)) != C * (A @ B) # answer(A). [para(203(a,1),65(a,2))]. given #103 (F,wt=9): 391 x * y @ x = y @ x. [hyper(378,a,328,a),flip(a)]. given #104 (T,wt=11): 402 (x @ y) * y * x = x * y. [hyper(51,a,19,a)]. given #105 (T,wt=9): 464 (x @ y) @ y * x = c_0. [para(402(a,1),305(a,1)),demod(9(4),10(4)),xx(a)]. given #106 (A,wt=18): 58 x * y * z * u != v * u | x * y * z = v. [para(9(a,1),14(a,1,2))]. given #107 (F,wt=17): 425 (D @ (F @ G)) * C * (A @ B) != (A @ B) * C # answer(A). [para(402(a,1),29(a,1)),flip(a)]. given #108 (F,wt=17): 426 ((A @ B) @ C) * (F @ G) * D != D * (F @ G) # answer(A). [para(402(a,1),29(a,2))]. given #109 (T,wt=9): 465 y * x @ (x @ y) = c_0. [para(402(a,1),305(a,2)),demod(9(3),10(3)),xx(a)]. given #110 (T,wt=9): 477 x * y @ (x @ y) = c_0. [para(402(a,1),391(a,1,1)),demod(465(6))]. given #111 (A,wt=18): 59 x * y * z != u * v * z | x * y = u * v. [para(9(a,1),14(a,2))]. given #112 (F,wt=21): 430 x * (D @ (F @ G)) * C * (A @ B) != x * (A @ B) * C # answer(A). [para(402(a,1),31(a,1,2)),flip(a)]. given #113 (F,wt=21): 432 x * ((A @ B) @ C) * (F @ G) * D != x * D * (F @ G) # answer(A). [para(402(a,1),31(a,2,2))]. given #114 (T,wt=9): 486 x * y @ y * x = c_0. [para(464(a,1),391(a,2)),demod(9(3),10(3))]. given #115 (T,wt=11): 479 (x * y @ y) @ x * y = c_0. [para(10(a,1),464(a,1,2)),demod(407(3))]. given #116 (A,wt=18): 60 x * y * (y @ z) != u * y * z | u * z = x. [para(10(a,1),14(a,1,2)),flip(a)]. given #117 (F,wt=21): 446 (F @ G) * D * ((A @ B) @ C) * G * F != D * F * G # answer(A). [para(402(a,1),68(a,2,2))]. given #118 (F,wt=21): 503 (D @ (F @ G)) * C * (A @ B) * x != (A @ B) * C * x # answer(A). [ur(58,b,425,a),demod(9(18))]. given #119 (T,wt=10): 582 x * y != z * y | z = x. [para(197(a,1),60(a,2,2)),demod(252(2),197(2),197(5))]. given #120 (T,wt=11): 487 (x @ y) @ y * y * x = c_0. [para(391(a,1),464(a,1,1))]. given #121 (A,wt=14): 61 x * (y @ z) != y * z | z * y = x. [para(10(a,1),14(a,1)),flip(a)]. given #122 (F,wt=21): 504 ((A @ B) @ C) * (F @ G) * D * x != D * (F @ G) * x # answer(A). [ur(58,b,426,a),demod(9(18))]. given #123 (F,wt=21): 592 (D @ (F @ G)) * C * A * B != (A @ B) * C * B * A # answer(A). [para(402(a,1),503(a,1,2,2))]. given #124 (T,wt=11): 506 x * y @ (x * y @ y) = c_0. [para(10(a,1),465(a,1,1)),demod(407(4))]. given #125 (T,wt=11): 513 x * x * y @ (y @ x) = c_0. [para(391(a,1),465(a,1,2))]. given #126 (A,wt=18): 62 x * y * z * (z @ u) != z * u | x * y = u. [para(10(a,1),14(a,2))]. given #127 (F,wt=21): 607 ((A @ B) @ C) * (F @ G) * D * G * F != D * F * G # answer(A). [para(402(a,1),504(a,2,2))]. given #128 (F,wt=21): 620 (D @ (F @ G)) * C * C * (A @ B) != C * (A @ B) * C # answer(A). [para(513(a,1),32(a,1,2,2)),demod(197(14),9(26),9(25),10(25))]. given #129 (T,wt=11): 531 x * y * x @ (y @ x) = c_0. [para(391(a,1),477(a,1,2)),demod(9(2))]. given #130 (T,wt=11): 648 x * y * y @ (x @ y) = c_0. [para(531(a,1),391(a,2)),demod(422(4))]. given #131 (A,wt=22): 63 x * y * z * y * x != u * z * x * y | y * x = u. [para(11(a,1),14(a,1))]. given #132 (F,wt=23): 431 (x @ ((A @ B) @ C)) * (D @ (F @ G)) * x != x * ((A @ B) @ C) # answer(A). [para(402(a,1),31(a,1)),flip(a)]. given #133 (F,wt=23): 433 (x @ (D @ (F @ G))) * ((A @ B) @ C) * x != x * (D @ (F @ G)) # answer(A). [para(402(a,1),31(a,2))]. given #134 (T,wt=12): 398 x * (x @ y) != x | x @ y = c_0. [para(328(a,1),190(a,1)),demod(391(6)),flip(b)]. given #135 (T,wt=12): 456 x * y != x | (x @ y) * y = c_0. [para(402(a,1),191(a,1))]. given #136 (A,wt=15): 75 x * y * y * x = y * x * x * y. [para(38(a,1),11(a,1,2)),demod(71(6))]. given #137 (F,wt=23): 434 (((A @ B) @ C) @ x) * x * (D @ (F @ G)) != ((A @ B) @ C) * x # answer(A). [para(402(a,1),34(a,1)),flip(a)]. given #138 (F,wt=23): 435 ((D @ (F @ G)) @ x) * x * ((A @ B) @ C) != (D @ (F @ G)) * x # answer(A). [para(402(a,1),34(a,2))]. given #139 (T,wt=12): 462 (x @ y) * y != x * y | c_0 = x. [para(402(a,1),200(a,1)),flip(a)]. given #140 (T,wt=13): 358 x * (x @ x * y) = x * (x @ y). [hyper(16,a,203,a),flip(a)]. given #141 (A,wt=20): 88 x * y * z != u * x * y | u * (u @ x * y) = z. [para(9(a,1),16(a,1))]. given #142 (F,wt=23): 441 (A @ B) * C * (F @ G) * D != C * (A @ B) * D * (F @ G) # answer(A). [para(402(a,1),65(a,1,2,2)),flip(a)]. given #143 (F,wt=23): 445 (F @ G) * D * (A @ B) * C != D * (F @ G) * C * (A @ B) # answer(A). [para(402(a,1),68(a,1,2,2))]. given #144 (T,wt=9): 722 x @ x * y = x @ y. [hyper(378,a,358,a),flip(a)]. given #145 (T,wt=9): 762 (x @ y) @ x * y = c_0. [para(402(a,1),722(a,1,2)),demod(464(6))]. given #146 (A,wt=20): 89 x * y * z != z * u | x * y * (x * y @ z) = u. [para(9(a,1),16(a,2)),demod(9(8)),flip(a)]. given #147 (F,wt=23): 521 (A @ B) * C * ((A @ B) @ C) != (D @ (F @ G)) * (A @ B) * C # answer(A). [para(477(a,1),32(a,1,2,2)),demod(197(12),9(22)),flip(a)]. given #148 (F,wt=23): 523 ((A @ B) @ C) * D * (F @ G) != D * (F @ G) * (D @ (F @ G)) # answer(A). [para(477(a,1),33(a,1,2,2)),demod(197(12),9(22))]. given #149 (T,wt=11): 763 (x @ y) @ x * y * x = c_0. [para(722(a,1),464(a,1,1)),demod(9(3))]. given #150 (T,wt=11): 764 x * y * x @ (x @ y) = c_0. [para(722(a,1),465(a,1,2)),demod(9(2))]. given #151 (A,wt=18): 90 x * y != z * y | z * (z @ y) = x * (x @ y). [para(10(a,1),16(a,1))]. given #152 (F,wt=21): 823 ((A @ B) @ C) * D * (F @ G) * D != D * D * (F @ G) # answer(A). [para(764(a,1),33(a,1,2,2)),demod(197(14),9(26),9(25),10(25))]. given #153 (F,wt=23): 532 (F @ G) * D * ((F @ G) @ D) * ((A @ B) @ C) != (F @ G) * D # answer(A). [back_demod(447),demod(519(17))]. given #154 (T,wt=11): 765 x * x * y @ (x @ y) = c_0. [para(722(a,1),477(a,1,2))]. given #155 (T,wt=11): 778 x * y @ (y @ x * y) = c_0. [back_demod(516),demod(751(4))]. given #156 (A,wt=20): 115 x * y * z * (y * z @ u) != y * z * u | u = x. [para(9(a,1),17(a,1,2)),demod(9(7))]. given #157 (F,wt=23): 533 C * (A @ B) * (C @ (A @ B)) * (D @ (F @ G)) != C * (A @ B) # answer(A). [back_demod(442),demod(519(17))]. given #158 (F,wt=23): 547 (C @ (A @ B)) * (D @ (F @ G)) * C * (A @ B) != C * (A @ B) # answer(A). [para(402(a,1),430(a,2))]. given #159 (T,wt=11): 788 (x @ y * x) @ y * x = c_0. [para(10(a,1),762(a,1,2)),demod(751(3))]. given #160 (T,wt=11): 796 (x @ y) @ y * x * y = c_0. [para(391(a,1),762(a,1,1)),demod(9(3))]. given #161 (A,wt=20): 132 x * y * z * (y * z @ u) != y * z * u | x = u. [para(9(a,1),18(a,1,2)),demod(9(7))]. given #162 (F,wt=21): 892 C * (A @ B) * C * (D @ (F @ G)) != (A @ B) * C * C # answer(A). [para(796(a,1),53(a,1,2,2)),demod(197(14),9(13),9(12),422(26))]. given #163 (F,wt=23): 549 ((F @ G) @ D) * ((A @ B) @ C) * (F @ G) * D != (F @ G) * D # answer(A). [para(402(a,1),432(a,2))]. given #164 (T,wt=11): 800 (x @ y) @ x * x * y = c_0. [para(722(a,1),762(a,1,1))]. given #165 (T,wt=11): 855 x * (y @ x) * y = y * x. [para(778(a,1),10(a,1,2,2)),demod(197(5),534(4),9(5),740(4)),flip(a)]. given #166 (A,wt=18): 149 x * y * z != y * u | x * (x @ y) * z = u. [para(19(a,1),7(a,1))]. given #167 (F,wt=17): 918 C * (D @ (F @ G)) * (A @ B) != (A @ B) * C # answer(A). [para(855(a,1),31(a,1)),flip(a)]. given #168 (F,wt=17): 919 (F @ G) * ((A @ B) @ C) * D != D * (F @ G) # answer(A). [para(855(a,1),31(a,2))]. given #169 (T,wt=11): 863 x * y @ (x @ y * x) = c_0. [para(778(a,1),391(a,2)),demod(534(4))]. given #170 (T,wt=11): 884 (x @ y * x) @ x * y = c_0. [para(788(a,1),722(a,2)),demod(534(6))]. given #171 (A,wt=18): 150 x * y * (y @ z) * u != y * z * u | z = x. [para(19(a,1),8(a,1)),flip(a)]. given #172 (F,wt=21): 925 x * C * (D @ (F @ G)) * (A @ B) != x * (A @ B) * C # answer(A). [para(855(a,1),47(a,1,2)),flip(a)]. given #173 (F,wt=21): 926 x * (F @ G) * ((A @ B) @ C) * D != x * D * (F @ G) # answer(A). [para(855(a,1),47(a,2,2))]. given #174 (T,wt=11): 898 (x @ y) @ x * y * y = c_0. [para(796(a,1),722(a,2)),demod(422(5))]. given #175 (T,wt=11): 914 (x @ y) * x = x * (x @ y). [hyper(16,a,855,a),flip(a)]. given #176 (A,wt=18): 151 x * y * (y @ z) * u != y * z * u | x = z. [para(19(a,1),8(a,2))]. given #177 (F,wt=15): 1045 ((A @ B) @ C) * D != D * (D @ (F @ G)) # answer(A). [para(914(a,1),29(a,2))]. given #178 (F,wt=19): 1044 (A @ B) * ((A @ B) @ C) != (D @ (F @ G)) * (A @ B) # answer(A). [para(914(a,1),29(a,1))]. given #179 (T,wt=7): 1038 x @ (x @ y) = c_0. [hyper(390,a,914,a)]. given #180 (T,wt=7): 1039 (x @ y) @ x = c_0. [hyper(305,a,914,a)]. given #181 (A,wt=21): 152 x * y * z * (z @ x * y) * u = z * x * y * u. [para(19(a,1),9(a,1)),demod(9(2)),flip(a)]. given #182 (F,wt=19): 1051 x * ((A @ B) @ C) * D != x * D * (D @ (F @ G)) # answer(A). [para(914(a,1),31(a,2,2))]. given #183 (F,wt=19): 1120 ((A @ B) @ C) * D * x != D * (D @ (F @ G)) * x # answer(A). [ur(582,b,1045,a),demod(9(8),9(16)),flip(a)]. given #184 (T,wt=11): 967 x * (x @ y) * (y @ x) = x. [hyper(149,a,10,a)]. given #185 (T,wt=9): 1154 (x @ y) * (y @ x) = c_0. [hyper(190,a,967,a),flip(a)]. given #186 (A,wt=21): 153 x * y * z * (y * z @ x) * u = y * z * x * u. [para(9(a,1),19(a,1,2)),demod(9(9))]. given #187 (F,wt=13): 1192 (D @ (F @ G)) * (C @ (A @ B)) != c_0 # answer(A). [para(1154(a,1),29(a,1)),flip(a)]. given #188 (F,wt=13): 1193 ((A @ B) @ C) * ((F @ G) @ D) != c_0 # answer(A). [para(1154(a,1),29(a,2))]. given #189 (T,wt=9): 1228 (x @ y) @ (y @ x) = c_0. [para(1154(a,1),305(a,1)),demod(1154(4)),xx(a)]. given #190 (T,wt=10): 1218 x @ y != c_0 | y @ x = c_0. [para(1154(a,1),190(a,1)),flip(a),flip(b)]. given #191 (A,wt=21): 154 x * y * z * (z @ (x @ y)) = y * x * z * (x @ y). [para(10(a,1),19(a,1,2,2)),flip(a)]. given #192 (F,wt=13): 1194 (C @ (A @ B)) * (D @ (F @ G)) != c_0 # answer(A). [para(1154(a,1),30(a,1)),flip(a)]. given #193 (F,wt=13): 1195 ((F @ G) @ D) * ((A @ B) @ C) != c_0 # answer(A). [para(1154(a,1),30(a,2))]. given #194 (T,wt=11): 1073 x * (x @ y) @ (x @ y) = c_0. [para(914(a,1),391(a,1,1)),demod(1038(6))]. given #195 (T,wt=11): 1081 (x @ y) @ x * (x @ y) = c_0. [para(914(a,1),722(a,1,2)),demod(1039(6))]. given #196 (A,wt=22): 159 x * y * z * u != x * z * v | y * (y @ z) * u = v. [para(19(a,1),13(a,1,2))]. given #197 (F,wt=15): 1188 ((A @ B) @ C) * D * ((F @ G) @ D) != D # answer(A). [para(967(a,1),1120(a,2))]. given #198 (F,wt=15): 1197 x * (D @ (F @ G)) * (C @ (A @ B)) != x # answer(A). [para(1154(a,1),31(a,1,2)),demod(197(2)),flip(a)]. given #199 (T,wt=11): 1191 (x @ y) * (y @ x) * z = z. [para(1154(a,1),9(a,1,1)),demod(187(2)),flip(a)]. given #200 (T,wt=9): 1410 ((x @ y) @ z) @ z = c_0. [para(1191(a,1),762(a,1,2)),demod(1409(4))]. given #201 (A,wt=18): 160 x * y * z != y * x * u | (x @ y) * z = u. [para(19(a,1),13(a,1))]. given #202 (F,wt=11): 1430 (F @ G) @ D != C @ (A @ B) # answer(A). [para(1191(a,1),1197(a,1)),flip(a)]. given #203 (F,wt=15): 1198 x * ((A @ B) @ C) * ((F @ G) @ D) != x # answer(A). [para(1154(a,1),31(a,2,2)),demod(197(14))]. given #204 (T,wt=9): 1436 x @ ((y @ z) @ x) = c_0. [back_demod(1391),demod(1409(4))]. given #205 (T,wt=11): 1254 (x @ y) * y * (y @ x) = y. [back_demod(1155),demod(1191(4)),flip(a)]. given #206 (A,wt=18): 161 x * y * z != y * x * u | (y @ x) * u = z. [para(19(a,1),13(a,2)),flip(b)]. given #207 (F,wt=15): 1199 x * (C @ (A @ B)) * (D @ (F @ G)) != x # answer(A). [para(1154(a,1),34(a,1,2)),demod(197(2)),flip(a)]. given #208 (F,wt=15): 1200 x * ((F @ G) @ D) * ((A @ B) @ C) != x # answer(A). [para(1154(a,1),34(a,2,2)),demod(197(14))]. given #209 (T,wt=7): 1532 x @ (y @ x) = c_0. [para(1254(a,1),391(a,1,1)),demod(1523(6))]. given #210 (T,wt=7): 1544 (x @ y) @ y = c_0. [para(1254(a,1),722(a,1,2)),demod(1522(6))]. given #211 (A,wt=22): 162 x * y * (y @ z) * u != v * y * z * u | v * z = x. [para(19(a,1),14(a,1,2)),flip(a)]. given #212 (F,wt=15): 1281 (D @ (F @ G)) * (C @ (A @ B)) * x != x # answer(A). [ur(582,b,1192,a),demod(187(2),9(12)),flip(a)]. given #213 (F,wt=15): 1284 ((A @ B) @ C) * ((F @ G) @ D) * x != x # answer(A). [ur(582,b,1193,a),demod(187(2),9(12)),flip(a)]. given #214 (T,wt=10): 1505 x * y != x | y @ x = y. [para(1254(a,1),17(a,1)),flip(a),flip(b)]. given #215 (T,wt=11): 1522 (y @ x) @ x * (x @ y) = c_0. [para(1254(a,1),305(a,1)),demod(9(4),1154(3),197(2)),xx(a)]. given #216 (A,wt=18): 163 x * (y @ z) * u != y * z * u | z * y = x. [para(19(a,1),14(a,1)),flip(a)]. given #217 (F,wt=15): 1310 (C @ (A @ B)) * (D @ (F @ G)) * x != x # answer(A). [ur(582,b,1194,a),demod(187(2),9(12)),flip(a)]. given #218 (F,wt=15): 1313 ((F @ G) @ D) * ((A @ B) @ C) * x != x # answer(A). [ur(582,b,1195,a),demod(187(2),9(12)),flip(a)]. given #219 (T,wt=11): 1523 x * (x @ y) @ (y @ x) = c_0. [para(1254(a,1),305(a,2)),demod(9(4),1154(3),197(2)),xx(a)]. given #220 (T,wt=11): 1558 (x @ y) * y = y * (x @ y). [para(1532(a,1),10(a,1,2,2)),demod(197(3))]. given #221 (A,wt=22): 164 x * y * z * (z @ u) * v != z * u * v | x * y = u. [para(19(a,1),14(a,2))]. given #222 (F,wt=15): 1427 (C @ (A @ B)) * D * (D @ (F @ G)) != D # answer(A). [para(1191(a,1),1051(a,1)),flip(a)]. given #223 (F,wt=15): 1475 ((F @ G) @ D) * x != (C @ (A @ B)) * x # answer(A). [ur(582,b,1430,a),flip(a)]. given #224 (T,wt=11): 1563 x * (y @ x) @ (y @ x) = c_0. [para(1532(a,1),391(a,2)),demod(1558(2))]. given #225 (T,wt=11): 1585 (x @ y) @ y * (x @ y) = c_0. [para(1544(a,1),722(a,2)),demod(1558(3))]. given #226 (A,wt=22): 166 x * y * z != u * y | u * (u @ y) = x * (x @ y) * z. [para(19(a,1),16(a,1))]. given #227 (F,wt=15): 1476 x * ((F @ G) @ D) != x * (C @ (A @ B)) # answer(A). [ur(378,b,1430,a),flip(a)]. given #228 (F,wt=15): 1484 C * ((A @ B) @ C) != (D @ (F @ G)) * C # answer(A). [para(1436(a,1),32(a,1,2,2)),demod(197(8)),flip(a)]. given #229 (T,wt=12): 933 x * y != x | y * (x @ y) = c_0. [para(855(a,1),191(a,1))]. given #230 (T,wt=12): 937 x * (y @ x) != y * x | c_0 = y. [para(855(a,1),200(a,1)),flip(a)]. given #231 (A,wt=25): 169 x * y * z * (z @ (x @ y)) * u = y * x * z * (x @ y) * u. [para(19(a,1),19(a,1,2,2)),flip(a)]. given #232 (F,wt=15): 1492 (D @ (F @ G)) * C * (C @ (A @ B)) != C # answer(A). [para(1254(a,1),29(a,1)),flip(a)]. given #233 (F,wt=15): 1666 ((F @ G) @ D) * C * ((A @ B) @ C) != C # answer(A). [para(1558(a,1),1313(a,1,2))]. given #234 (T,wt=12): 1189 (x @ y) * z != c_0 | y @ x = z. [para(1154(a,1),7(a,1)),flip(a)]. given #235 (T,wt=12): 1190 x * (y @ z) != c_0 | z @ y = x. [para(1154(a,1),8(a,1)),flip(a)]. given #236 (A,wt=16): 178 x * (x @ y) * z != x * y * z | c_0 = y. [back_demod(176),demod(177(7))]. given #237 (F,wt=15): 1686 ((F @ G) @ D) * C != C * (C @ (A @ B)) # answer(A). [para(914(a,1),1475(a,2))]. given #238 (F,wt=15): 1687 D * ((F @ G) @ D) != (C @ (A @ B)) * D # answer(A). [para(1558(a,1),1475(a,1))]. given #239 (T,wt=12): 1222 x @ y != z | z * (y @ x) = c_0. [para(1154(a,1),191(a,1,2)),demod(197(2)),flip(a)]. given #240 (T,wt=12): 1226 x * (y @ z) != x | z @ y = c_0. [para(1154(a,1),200(a,1,2)),demod(197(2)),flip(a),flip(b)]. given #241 (A,wt=20): 180 x * y * z * y * x != x * z * x * y | c_0 = y. [back_demod(174),demod(177(9))]. given #242 (F,wt=17): 1205 (A @ B) * C * ((F @ G) @ D) != C * (A @ B) # answer(A). [para(1154(a,1),65(a,1,2,2)),demod(197(6)),flip(a)]. given #243 (F,wt=17): 1207 D * (F @ G) * (C @ (A @ B)) != (F @ G) * D # answer(A). [para(1154(a,1),68(a,1,2,2)),demod(197(6)),flip(a)]. given #244 (T,wt=12): 1238 x * y != c_0 | y @ x = y * x. [para(1154(a,1),61(a,1)),flip(a),flip(b)]. given #245 (T,wt=12): 1361 x @ y != z | (y @ x) * z = c_0. [para(1191(a,1),190(a,1)),flip(a),flip(b)]. given #246 (A,wt=16): 185 x * y * z != y | x * (x @ y) * z = c_0. [back_demod(158),demod(177(4)),flip(b)]. given #247 (F,wt=17): 1208 (F @ G) * D * ((A @ B) @ C) * (G @ F) != D # answer(A). [para(1154(a,1),68(a,2,2)),demod(197(18))]. given #248 (F,wt=17): 1237 (D @ (F @ G)) * C != (A @ B) * C * (B @ A) # answer(A). [para(1154(a,1),503(a,1,2,2)),demod(197(8))]. given #249 (T,wt=12): 1362 (x @ y) * z != z | y @ x = c_0. [para(1191(a,1),193(a,1)),flip(a),flip(b)]. given #250 (T,wt=12): 1562 x * (y @ x) != x | y @ x = c_0. [para(1532(a,1),188(a,1,2)),demod(197(2)),flip(a),flip(b)]. given #251 (A,wt=20): 201 x * y * z * y * x != y | x * z * x * y = c_0. [back_demod(45),demod(177(6)),flip(b)]. given #252 (F,wt=17): 1239 ((A @ B) @ C) * (F @ G) * D * (G @ F) != D # answer(A). [para(1154(a,1),504(a,2,2)),demod(197(18))]. given #253 (F,wt=17): 1351 (B @ A) * C * (A @ B) * (D @ (F @ G)) != C # answer(A). [para(1191(a,1),67(a,2))]. given #254 (T,wt=12): 1725 c_0 != x | (y @ z) * x = y @ z. [para(1191(a,1),1189(a,1)),flip(a),flip(b)]. given #255 (T,wt=12): 1782 x * y * z != x | y * z = c_0. [para(19(a,1),185(a,1)),demod(1191(7))]. given #256 (A,wt=23): 207 x * y * z * u * (u @ x * y * z) = u * x * y * z. [para(20(a,1),9(a,1)),demod(9(2),9(5)),flip(a)]. given #257 (F,wt=17): 1356 D * ((A @ B) @ C) != (G @ F) * D * (F @ G) # answer(A). [para(1191(a,1),70(a,1))]. given #258 (F,wt=17): 1393 ((F @ G) @ D) * (A @ B) * C != C * (A @ B) # answer(A). [para(1191(a,1),430(a,1)),flip(a)]. given #259 (T,wt=12): 1805 (x @ y) * z != z | x @ y = c_0. [para(1191(a,1),1362(a,1)),flip(a)]. given #260 (T,wt=13): 407 x * (x @ y) @ y = x * y @ y. [para(10(a,1),391(a,1,1)),flip(a)]. given #261 (A,wt=23): 208 x * y * z * u * (z * u @ x * y) = z * u * x * y. [para(9(a,1),20(a,1,2,2)),demod(9(10))]. given #262 (F,wt=17): 1394 (B @ A) * (D @ (F @ G)) * C * (A @ B) != C # answer(A). [para(1191(a,1),430(a,2))]. given #263 (F,wt=17): 1395 (F @ G) * D != (C @ (A @ B)) * D * (F @ G) # answer(A). [para(1191(a,1),432(a,1))]. given #264 (T,wt=13): 478 (x @ y * z) @ y * z * x = c_0. [para(9(a,1),464(a,1,2))]. given #265 (T,wt=13): 505 x * y * z @ (z @ x * y) = c_0. [para(9(a,1),465(a,1,1))]. given #266 (A,wt=23): 213 x * y * z * (z @ x * (x @ y)) = y * z * x * (x @ y). [para(20(a,1),19(a,1,2)),flip(a)]. given #267 (F,wt=17): 1425 (B @ A) * C * (D @ (F @ G)) * (A @ B) != C # answer(A). [para(1191(a,1),925(a,2))]. given #268 (F,wt=17): 1426 ((A @ B) @ C) * D != (G @ F) * D * (F @ G) # answer(A). [para(1191(a,1),926(a,1))]. given #269 (T,wt=13): 514 x * y * z @ (x * y @ z) = c_0. [para(9(a,1),477(a,1,1))]. given #270 (T,wt=13): 530 x * y * (x @ y) @ (x @ y) = c_0. [para(477(a,1),391(a,2)),demod(515(3))]. given #271 (A,wt=23): 217 x * y * z * u * (y * z * u @ x) = y * z * u * x. [para(9(a,1),21(a,1,2,2,2,1)),demod(9(6),9(10))]. given #272 (F,wt=17): 1760 (A @ B) * ((F @ G) @ D) * C != C * (A @ B) # answer(A). [ur(16,b,1686,a(flip))]. given #273 (F,wt=19): 1152 ((A @ B) @ C) * D * D != D * D * (D @ (F @ G)) # answer(A). [para(914(a,1),1120(a,2,2))]. given #274 (T,wt=13): 550 x * y * z @ z * x * y = c_0. [para(9(a,1),486(a,1,1))]. given #275 (T,wt=13): 551 x * y * z @ y * z * x = c_0. [para(9(a,1),486(a,1,2))]. given #276 (A,wt=24): 218 x * y * z * u != x * u * v | y * z * (y * z @ u) = v. [para(21(a,1),13(a,1,2))]. given #277 (F,wt=19): 1211 x * y * (C @ (A @ B)) * (D @ (F @ G)) != x * y # answer(A). [para(1154(a,1),46(a,1,2,2)),demod(197(2)),flip(a)]. given #278 (F,wt=19): 1212 x * y * ((F @ G) @ D) * ((A @ B) @ C) != x * y # answer(A). [para(1154(a,1),46(a,2,2,2)),demod(197(15))]. given #279 (T,wt=13): 601 (x @ y) @ y * y * y * x = c_0. [para(391(a,1),487(a,1,1))]. given #280 (T,wt=13): 625 x * x * x * y @ (y @ x) = c_0. [para(391(a,1),513(a,1,2))]. given #281 (A,wt=20): 219 x * y * z != z * x * u | y * (x * y @ z) = u. [para(21(a,1),13(a,1))]. given #282 (F,wt=19): 1213 x * y * (D @ (F @ G)) * (C @ (A @ B)) != x * y # answer(A). [para(1154(a,1),47(a,1,2,2)),demod(197(2)),flip(a)]. given #283 (F,wt=19): 1214 x * y * ((A @ B) @ C) * ((F @ G) @ D) != x * y # answer(A). [para(1154(a,1),47(a,2,2,2)),demod(197(15))]. given #284 (T,wt=13): 649 x * x * y * x @ (y @ x) = c_0. [para(391(a,1),531(a,1,2)),demod(9(2))]. given #285 (T,wt=13): 659 x * y * x * x @ (y @ x) = c_0. [para(391(a,1),648(a,1,2)),demod(9(3))]. given #286 (A,wt=24): 220 x * y * z * (y * z @ u) != v * y * z * u | v * u = x. [para(21(a,1),14(a,1,2)),flip(a)]. given #287 (F,wt=19): 1332 ((A @ B) @ C) * D * ((F @ G) @ D) * x != D * x # answer(A). [ur(582,b,1188,a),demod(9(16),9(15)),flip(a)]. given #288 (F,wt=19): 1333 x * ((A @ B) @ C) * D * ((F @ G) @ D) != x * D # answer(A). [ur(378,b,1188,a),flip(a)]. given #289 (T,wt=13): 751 x @ y * (y @ x) = x @ y * x. [para(10(a,1),722(a,1,2)),flip(a)]. given #290 (T,wt=13): 787 (x * y @ z) @ x * y * z = c_0. [para(9(a,1),762(a,1,2))]. given #291 (A,wt=20): 221 x * y * (z * y @ u) != z * y * u | u * z = x. [para(21(a,1),14(a,1)),flip(a)]. given #292 (F,wt=19): 1336 x * (D @ (F @ G)) * (C @ (A @ B)) * y != x * y # answer(A). [ur(582,b,1197,a),demod(9(14),9(13)),flip(a)]. given #293 (F,wt=19): 1345 x * ((A @ B) @ C) * ((F @ G) @ D) * y != x * y # answer(A). [para(1191(a,1),31(a,2,2))]. given #294 (T,wt=13): 799 (x @ y) @ x * y * (x @ y) = c_0. [para(762(a,1),722(a,2)),demod(515(4))]. given #295 (T,wt=13): 815 (x @ y) @ x * x * y * x = c_0. [para(722(a,1),763(a,1,1)),demod(9(3))]. given #296 (A,wt=24): 222 x * y * z * u * (z * u @ v) != z * u * v | x * y = v. [para(21(a,1),14(a,2))]. given #297 (F,wt=19): 1358 x * (C @ (A @ B)) * (D @ (F @ G)) * y != x * y # answer(A). [para(1191(a,1),47(a,1,2)),flip(a)]. given #298 (F,wt=19): 1360 x * ((F @ G) @ D) * ((A @ B) @ C) * y != x * y # answer(A). [para(1191(a,1),47(a,2,2))]. given #299 (T,wt=13): 829 x * x * y * x @ (x @ y) = c_0. [para(722(a,1),764(a,1,2)),demod(9(2))]. given #300 (T,wt=13): 844 x * x * x * y @ (x @ y) = c_0. [para(722(a,1),765(a,1,2))]. given #301 (A,wt=24): 223 x * y * z != u * z | u * (u @ z) = x * y * (x * y @ z). [para(21(a,1),16(a,1))]. given #302 (F,wt=19): 1480 x * y * ((F @ G) @ D) != x * y * (C @ (A @ B)) # answer(A). [ur(13,b,1430,a)]. given #303 (F,wt=19): 1493 ((A @ B) @ C) * (F @ G) * ((F @ G) @ D) != F @ G # answer(A). [para(1254(a,1),29(a,2))]. given #304 (T,wt=13): 894 (x @ y) @ y * y * x * y = c_0. [para(391(a,1),796(a,1,1)),demod(9(3))]. given #305 (T,wt=13): 911 (x @ y) @ x * x * x * y = c_0. [para(722(a,1),800(a,1,1))]. given #306 (A,wt=23): 224 x * y * z * ((x @ y) * z @ x) = y * (x @ y) * z * x. [para(21(a,1),19(a,1,2)),flip(a)]. given #307 (F,wt=19): 1496 x * (D @ (F @ G)) * C * (C @ (A @ B)) != x * C # answer(A). [para(1254(a,1),31(a,1,2)),flip(a)]. given #308 (F,wt=19): 1561 ((A @ B) @ C) * (F @ G) != (F @ G) * (D @ (F @ G)) # answer(A). [para(1532(a,1),33(a,1,2,2)),demod(197(10))]. given #309 (T,wt=13): 959 x * (x @ y * x) = x * (x @ y). [back_demod(740),demod(914(5))]. given #310 (T,wt=9): 2304 x @ y * x = x @ y. [hyper(378,a,959,a),flip(a)]. given #311 (A,wt=25): 229 x * y * z * z * (z @ y * x * y * z) = z * x * z * y. [hyper(22,a,20,a(flip)),demod(9(11),9(10)),flip(a)]. given #312 (F,wt=11): 2523 D @ (G @ F) != C @ (A @ B) # answer(A). [back_demod(1430),demod(2366(5))]. given #313 (F,wt=11): 2644 D @ (F @ G) != C @ (B @ A) # answer(A). [back_demod(12),demod(2366(5)),flip(a)]. given #314 (T,wt=9): 2350 x * y @ y = x @ y. [para(10(a,1),2304(a,1,2)),demod(2346(4),407(4)),flip(a)]. given #315 (T,wt=11): 2340 x @ y * (y @ x) = x @ y. [back_demod(751),demod(2304(5))]. given #316 (A,wt=19): 230 x * (x @ y) * z * y * x = x * z * x * y. [hyper(22,a,19,a(flip)),flip(a)]. given #317 (F,wt=13): 2412 (C @ (B @ A)) * (D @ (G @ F)) != c_0 # answer(A). [back_demod(2262),demod(2366(5),2366(13),1558(17),1191(18))]. given #318 (F,wt=13): 2568 (D @ (G @ F)) * (C @ (B @ A)) != c_0 # answer(A). [back_demod(1195),demod(2366(5),2366(10))]. given #319 (T,wt=11): 2355 x * y * y @ (y @ x) = c_0. [para(2304(a,1),465(a,1,2)),demod(9(2))]. given #320 (T,wt=11): 2366 (x @ y) @ z = z @ (y @ x). [para(1191(a,1),2304(a,1,2)),demod(2350(3),1388(6))]. given #321 (A,wt=18): 231 x * y * y * x != y * z | x * x * y = z. [para(187(a,1),22(a,1,2,2)),demod(187(8))]. given #322 (F,wt=15): 2434 (C @ (B @ A)) * D * (D @ (G @ F)) != D # answer(A). [back_demod(1988),demod(2366(5),2366(15,R),2304(15),2366(11))]. given #323 (F,wt=15): 2480 D * (D @ (G @ F)) != (C @ (A @ B)) * D # answer(A). [back_demod(1687),demod(2366(6))]. given #324 (T,wt=11): 2402 x * (x @ y) @ y = x @ y. [back_demod(407),demod(2350(5))]. given #325 (T,wt=11): 2842 (x @ y) @ (z @ (y @ x)) = c_0. [para(2366(a,1),1038(a,1,2))]. given #326 (A,wt=18): 254 x * y * z != z | x * y * (x * y @ z) = c_0. [para(21(a,1),190(a,1)),flip(b)]. given #327 (F,wt=15): 2481 (D @ (G @ F)) * C != C * (C @ (A @ B)) # answer(A). [back_demod(1686),demod(2366(5))]. given #328 (F,wt=15): 2487 (D @ (G @ F)) * C * (C @ (B @ A)) != C # answer(A). [back_demod(1666),demod(2366(5),2366(11))]. given #329 (T,wt=11): 2850 (x @ y) @ ((y @ x) @ z) = c_0. [para(2366(a,2),1532(a,1,2))]. given #330 (T,wt=13): 1396 x @ (y @ z) * x * (z @ y) = c_0. [para(1191(a,1),486(a,1,1)),demod(9(4))]. given #331 (A,wt=22): 256 x * y * (x @ z) * y * x != x * z * x * y | y = z. [para(19(a,1),23(a,1)),flip(a)]. given #332 (F,wt=15): 2512 (D @ (F @ G)) * C != C * (C @ (B @ A)) # answer(A). [back_demod(1484),demod(2366(6)),flip(a)]. given #333 (F,wt=15): 2519 x * (D @ (G @ F)) != x * (C @ (A @ B)) # answer(A). [back_demod(1476),demod(2366(5))]. given #334 (T,wt=13): 1397 (x @ y) * z * (y @ x) @ z = c_0. [para(1191(a,1),486(a,1,2)),demod(9(4))]. given #335 (T,wt=13): 1945 x @ ((y @ z) @ x * (z @ y)) = c_0. [para(1154(a,1),505(a,1,1,2)),demod(197(2))]. given #336 (A,wt=18): 259 x * y * y * z != y * z * z * y | z = x. [para(187(a,1),23(a,1,2,2)),demod(187(6))]. given #337 (F,wt=15): 2520 (D @ (G @ F)) * x != (C @ (A @ B)) * x # answer(A). [back_demod(1475),demod(2366(5))]. given #338 (F,wt=15): 2546 (D @ (G @ F)) * (C @ (B @ A)) * x != x # answer(A). [back_demod(1313),demod(2366(5),2366(10))]. given #339 (T,wt=13): 2326 x * y @ x * (x @ y) = y @ x. [back_demod(2155),demod(2304(8),391(6))]. given #340 (T,wt=13): 2330 (x @ y) @ y * x * (y @ x) = c_0. [back_demod(2148),demod(2304(2))]. given #341 (A,wt=18): 261 x * y * (x * y @ z) != x * y * z | c_0 = z. [para(21(a,1),193(a,1)),flip(a)]. given #342 (F,wt=15): 2550 (C @ (B @ A)) * (D @ (G @ F)) * x != x # answer(A). [back_demod(1284),demod(2366(5),2366(10))]. given #343 (F,wt=15): 2566 x * (D @ (G @ F)) * (C @ (B @ A)) != x # answer(A). [back_demod(1200),demod(2366(5),2366(10))]. given #344 (T,wt=13): 2346 x * (x @ y) @ x * y = x @ y. [back_demod(1849),demod(2323(8))]. given #345 (T,wt=13): 2349 x @ y * z * x = x @ y * z. [para(9(a,1),2304(a,1,2))]. given #346 (A,wt=22): 262 x * y * (x @ z) * y * x != x * z * x * y | z = y. [para(19(a,1),24(a,1)),flip(a)]. given #347 (F,wt=15): 2567 x * (C @ (B @ A)) * (D @ (G @ F)) != x # answer(A). [back_demod(1198),demod(2366(5),2366(10))]. given #348 (F,wt=15): 2584 D * (D @ (F @ G)) != (C @ (B @ A)) * D # answer(A). [back_demod(1045),demod(2366(5)),flip(a)]. given #349 (T,wt=13): 2362 x * y * x * x @ (x @ y) = c_0. [para(2304(a,1),764(a,1,2)),demod(9(2))]. given #350 (T,wt=13): 2390 x * y @ y * (y @ x) = x @ y. [back_demod(2318),demod(2350(6))]. given #351 (A,wt=18): 263 x * y * y * z != y * z * z * y | x = z. [para(187(a,1),24(a,1,2,2)),demod(187(6))]. given #352 (F,wt=15): 2642 x * (D @ (F @ G)) != x * (C @ (B @ A)) # answer(A). [back_demod(30),demod(2366(5)),flip(a)]. given #353 (F,wt=15): 2643 (D @ (F @ G)) * x != (C @ (B @ A)) * x # answer(A). [back_demod(29),demod(2366(5)),flip(a)]. given #354 (T,wt=13): 2391 x * (x @ y) @ y * x = x @ y. [back_demod(2316),demod(2350(8),2304(6))]. given #355 (T,wt=13): 2672 x * y * z @ z = x * y @ z. [para(9(a,1),2350(a,1,1))]. given #356 (A,wt=23): 270 x * y * z * y * x * (y @ x) = y * x * z * y * x. [para(10(a,1),25(a,1,2,2,2)),flip(a)]. given #357 (F,wt=17): 2466 (A @ B) * (D @ (G @ F)) * C != C * (A @ B) # answer(A). [back_demod(1760),demod(2366(8))]. given #358 (F,wt=17): 2524 (G @ F) * D * (F @ G) != (C @ (B @ A)) * D # answer(A). [back_demod(1426),demod(2366(5)),flip(a)]. given #359 (T,wt=13): 2675 x * y * y * y @ (x @ y) = c_0. [para(2350(a,1),648(a,1,2)),demod(9(3))]. given #360 (T,wt=13): 2800 x * y * y * y @ (y @ x) = c_0. [para(2304(a,1),2355(a,1,2)),demod(9(3))]. given #361 (A,wt=23): 271 x * y * y * y * x * x = y * y * x * x * x * y. [para(11(a,1),25(a,1,2)),flip(a)]. given #362 (F,wt=17): 2526 (D @ (G @ F)) * (A @ B) * C != C * (A @ B) # answer(A). [back_demod(1393),demod(2366(5))]. given #363 (F,wt=17): 2537 (G @ F) * D * (F @ G) != D * (C @ (B @ A)) # answer(A). [back_demod(1356),demod(2366(6)),flip(a)]. given #364 (T,wt=13): 2801 (x @ (y @ z)) * (x @ (z @ y)) = c_0. [hyper(1361,a,2366,a)]. given #365 (T,wt=13): 2802 ((x @ y) @ z) * ((y @ x) @ z) = c_0. [hyper(1361,a,2366,a(flip))]. given #366 (A,wt=25): 273 x * y * z * y * x * (y @ z * x) = y * x * y * z * x. [para(20(a,1),25(a,1,2,2)),flip(a)]. given #367 (F,wt=17): 2557 (C @ (B @ A)) * (F @ G) * D * (G @ F) != D # answer(A). [back_demod(1239),demod(2366(5))]. given #368 (F,wt=17): 2564 (F @ G) * D * (C @ (B @ A)) * (G @ F) != D # answer(A). [back_demod(1208),demod(2366(9))]. given #369 (T,wt=13): 2815 x * (y @ z) @ (x @ (z @ y)) = c_0. [para(2366(a,1),465(a,1,2))]. given #370 (T,wt=13): 2816 (x @ y) * z @ ((y @ x) @ z) = c_0. [para(2366(a,2),465(a,1,2))]. given #371 (A,wt=19): 274 x * y * y * x * z = y * x * x * y * z. [para(187(a,1),25(a,1,2,2)),demod(187(8))]. given #372 (F,wt=17): 2565 (A @ B) * C * (D @ (G @ F)) != C * (A @ B) # answer(A). [back_demod(1205),demod(2366(9))]. given #373 (F,wt=17): 2599 (F @ G) * (C @ (B @ A)) * D != D * (F @ G) # answer(A). [back_demod(919),demod(2366(8))]. given #374 (T,wt=13): 2817 (x @ y) * z @ (z @ (y @ x)) = c_0. [para(2366(a,1),477(a,1,2))]. given #375 (T,wt=13): 2818 x * (y @ z) @ ((z @ y) @ x) = c_0. [para(2366(a,2),477(a,1,2))]. given #376 (A,wt=25): 275 x * y * z * y * x * (x * y @ z) = y * x * x * y * z. [para(21(a,1),25(a,1,2,2)),flip(a)]. given #377 (F,wt=17): 2624 (C @ (B @ A)) * (F @ G) * D != D * (F @ G) # answer(A). [back_demod(426),demod(2366(5))]. given #378 (F,wt=17): 2633 (F @ G) * D * (C @ (B @ A)) != D * (F @ G) # answer(A). [back_demod(56),demod(2366(9))]. given #379 (T,wt=13): 2843 (x @ (y @ z)) @ (x @ (z @ y)) = c_0. [para(2366(a,1),1228(a,1,1))]. given #380 (T,wt=13): 2844 ((x @ y) @ z) @ ((y @ x) @ z) = c_0. [para(2366(a,2),1228(a,1,1))]. given #381 (A,wt=24): 276 x * y * z * y * x * u != y | x * z * x * y * u = c_0. [para(25(a,1),190(a,1)),flip(b)]. given #382 (F,wt=17): 2670 (G @ F) * D * (C @ (A @ B)) != D * (G @ F) # answer(A). [ur(50,b,2523,a)]. given #383 (F,wt=17): 2671 (B @ A) * C * (D @ (F @ G)) != C * (B @ A) # answer(A). [ur(50,b,2644,a(flip))]. given #384 (T,wt=13): 2982 x * x * y @ y * x = x @ y. [para(2326(a,1),2326(a,1,2,2)),demod(9(4),10(3),9(5),10(5),2346(8))]. given #385 (T,wt=13): 3015 x * y @ y * y * x = x @ y. [para(2326(a,1),2346(a,1,1,2)),demod(9(3),10(3),9(5),10(4),2326(8))]. given #386 (A,wt=24): 277 x * y * z * y * x * u != x * z * x * y * u | c_0 = y. [para(25(a,1),193(a,1))]. given #387 (F,wt=17): 2796 C * (B @ A) * (D @ (G @ F)) != (B @ A) * C # answer(A). [ur(161,b,2412,a),demod(197(6)),flip(a)]. given #388 (F,wt=17): 2797 D * (G @ F) * (C @ (B @ A)) != (G @ F) * D # answer(A). [ur(161,b,2568,a),demod(197(6)),flip(a)]. given #389 (T,wt=13): 3314 (x @ (y @ z)) @ ((z @ y) @ x) = c_0. [para(2801(a,1),1396(a,1,2,2)),demod(197(6))]. given #390 (T,wt=13): 3316 ((x @ y) @ z) @ (z @ (y @ x)) = c_0. [para(2801(a,1),1397(a,1,1,2)),demod(197(4))]. given #391 (A,wt=19): 282 x * y * z * z * y = x * z * y * y * z. [para(187(a,1),26(a,1,2,2,2)),demod(187(7))]. given #392 (F,wt=17): 2902 (G @ F) * (C @ (A @ B)) * D != D * (G @ F) # answer(A). [ur(16,b,2480,a)]. given #393 (F,wt=17): 2944 (B @ A) * (D @ (F @ G)) * C != C * (B @ A) # answer(A). [ur(16,b,2512,a(flip))]. given #394 (T,wt=13): 3370 (x @ (y @ z)) @ x * (z @ y) = c_0. [hyper(1361,a,2815,a),demod(197(7))]. given #395 (T,wt=13): 3400 (x @ (y @ z)) @ (z @ y) * x = c_0. [para(2340(a,1),2816(a,1,2)),demod(2366(8,R),2349(8))]. given #396 (A,wt=24): 283 x * y * z * u * z * y != x | z * y * u * y * z = c_0. [para(26(a,1),190(a,1)),flip(b)]. given #397 (F,wt=19): 1662 (D @ (F @ G)) * (A @ B) * (C @ (A @ B)) != A @ B # answer(A). [para(1558(a,1),1281(a,1,2))]. given #398 (F,wt=19): 1665 (C @ (A @ B)) * (F @ G) * (D @ (F @ G)) != F @ G # answer(A). [para(1558(a,1),1310(a,1,2))]. given #399 (T,wt=13): 3544 x * y @ x * x * y * y = c_0. [para(2330(a,1),3015(a,2)),demod(1560(5),1043(4),1154(3),197(2),9(9),9(8),1154(7),197(6),9(6),9(5),1043(4),1558(3),642(5))]. given #400 (T,wt=13): 3635 x * x * y * y @ x * y = c_0. [hyper(1361,a,3544,a),demod(197(7))]. given #401 (A,wt=24): 284 x * y * z * u * z * y != z * y * u * y * z | c_0 = x. [para(26(a,1),193(a,1))]. given #402 (F,wt=19): 1677 (C @ (A @ B)) * D * (D @ (F @ G)) * x != D * x # answer(A). [ur(582,b,1427,a),demod(9(16),9(15)),flip(a)]. given #403 (F,wt=19): 1678 x * (C @ (A @ B)) * D * (D @ (F @ G)) != x * D # answer(A). [ur(378,b,1427,a),flip(a)]. given #404 (T,wt=14): 380 x * y * z != x * y * u | u = z. [para(9(a,1),378(a,1)),demod(9(4))]. given #405 (T,wt=14): 420 (x @ y) * z != x * y | y * x = z. [para(402(a,1),7(a,1)),flip(a)]. given #406 (A,wt=16): 285 x * y * z * u != u | x * y * z = c_0. [para(9(a,1),191(a,1,2))]. given #407 (F,wt=19): 1714 (D @ (F @ G)) * C * (C @ (A @ B)) * x != C * x # answer(A). [ur(582,b,1492,a),demod(9(16),9(15)),flip(a)]. given #408 (F,wt=19): 2425 (C @ (B @ A)) * D * D * (D @ (G @ F)) != D * D # answer(A). [back_demod(2142),demod(2366(5),2366(12))]. given #409 (T,wt=14): 421 x * y * z != z * y | z @ y = x. [para(402(a,1),8(a,1)),flip(a)]. given #410 (T,wt=14): 580 x * y * z != y * z | x * z = z. [para(10(a,1),60(a,1)),flip(a)]. given #411 (A,wt=16): 286 x * (x @ y) != z * x * y | z * y = c_0. [para(10(a,1),191(a,1,2)),flip(a)]. given #412 (F,wt=17): 3742 (C @ (A @ B)) * (G @ F) * D != D * (G @ F) # answer(A). [ur(421,b,2523,a)]. given #413 (F,wt=17): 3743 (D @ (F @ G)) * (B @ A) * C != C * (B @ A) # answer(A). [ur(421,b,2644,a(flip))]. given #414 (T,wt=12): 3764 c_0 != x | x * (y @ z) = y @ z. [para(1154(a,1),580(a,1,2)),demod(197(2),1154(3)),flip(a)]. given #415 (T,wt=14): 916 x * (y @ x) * z != y * x | y = z. [para(855(a,1),13(a,1)),flip(a)]. given #416 (A,wt=24): 288 x * y * z * u * z * y != y * u * y * z | x * z = c_0. [para(11(a,1),191(a,1,2))]. given #417 (F,wt=19): 2436 (C @ (B @ A)) * D * (D @ (G @ F)) * x != D * x # answer(A). [back_demod(1986),demod(2366(5),2366(15,R),2304(15),2366(11))]. given #418 (F,wt=19): 2464 x * D * (D @ (G @ F)) != x * (C @ (A @ B)) * D # answer(A). [back_demod(1762),demod(2366(6))]. given #419 (T,wt=10): 3822 x * y != y | y @ x = x. [para(1154(a,1),916(a,1,2)),demod(197(2)),flip(a),flip(b)]. given #420 (T,wt=14): 917 x * (y @ x) * z != y * x | z = y. [para(855(a,1),13(a,2))]. given #421 (A,wt=20): 289 x * y * z * y * x != z * x * y | y * x = c_0. [para(11(a,1),191(a,1))]. given #422 (F,wt=19): 2465 D * (D @ (G @ F)) * x != (C @ (A @ B)) * D * x # answer(A). [back_demod(1761),demod(2366(6))]. given #423 (F,wt=19): 2470 x * (D @ (G @ F)) * C != x * C * (C @ (A @ B)) # answer(A). [back_demod(1755),demod(2366(5))]. given #424 (T,wt=14): 922 x * y != z * x | y * (x @ y) = z. [para(855(a,1),14(a,1))]. given #425 (T,wt=14): 1040 (x @ y) * z != x * (x @ y) | x = z. [para(914(a,1),7(a,1)),flip(a)]. given #426 (A,wt=20): 290 x * (x @ y) * z != u * x * y * z | u * y = c_0. [para(19(a,1),191(a,1,2)),flip(a)]. given #427 (F,wt=19): 2471 (D @ (G @ F)) * C * x != C * (C @ (A @ B)) * x # answer(A). [back_demod(1754),demod(2366(5))]. given #428 (F,wt=19): 2475 x * (D @ (G @ F)) * C * (C @ (B @ A)) != x * C # answer(A). [back_demod(1717),demod(2366(5),2366(11))]. given #429 (T,wt=14): 1041 (x @ y) * z != x * (x @ y) | z = x. [para(914(a,1),7(a,2))]. given #430 (T,wt=14): 1042 x * (x @ y) != z * x | x @ y = z. [para(914(a,1),8(a,1))]. given #431 (A,wt=16): 291 (x @ y) * z != x * y * z | y * x = c_0. [para(19(a,1),191(a,1)),flip(a)]. given #432 (F,wt=19): 2476 (D @ (G @ F)) * C * (C @ (B @ A)) * x != C * x # answer(A). [back_demod(1716),demod(2366(5),2366(11))]. given #433 (F,wt=19): 2478 (D @ (F @ G)) * C * x != C * (C @ (B @ A)) * x # answer(A). [back_demod(1698),demod(2366(6)),flip(a)]. given #434 (T,wt=14): 1186 (x @ y) * z != x | x * (y @ x) = z. [para(967(a,1),149(a,1)),demod(1038(5),187(6)),flip(a)]. given #435 (T,wt=14): 1187 x * y * (z @ y) != y | y @ z = x. [para(967(a,1),150(a,2)),demod(1038(2),187(3))]. given #436 (A,wt=18): 293 x * (x @ y * z) != x * y * z | y * z = c_0. [para(20(a,1),191(a,1)),flip(a)]. given #437 (F,wt=19): 2479 (D @ (G @ F)) * (A @ B) != (A @ B) * (C @ (A @ B)) # answer(A). [back_demod(1688),demod(2366(5))]. given #438 (F,wt=19): 2482 (F @ G) * (D @ (G @ F)) != (C @ (A @ B)) * (F @ G) # answer(A). [back_demod(1685),demod(2366(8))]. given #439 (T,wt=14): 1196 x * (y @ z) * u != x | z @ y = u. [para(1154(a,1),13(a,1,2)),demod(197(2)),flip(a)]. given #440 (T,wt=14): 1201 x * (y @ z) != u | u * (z @ y) = x. [para(1154(a,1),14(a,1,2)),demod(197(2)),flip(a)]. given #441 (A,wt=22): 294 x * y * (x * y @ z) != u * x * y * z | u * z = c_0. [para(21(a,1),191(a,1,2)),flip(a)]. given #442 (F,wt=17): 4000 (D @ (F @ G)) * (B @ A) * C * (A @ B) != C # answer(A). [ur(1201,b,3743,a(flip)),demod(9(15),9(14))]. given #443 (F,wt=17): 4001 (C @ (A @ B)) * (G @ F) * D * (F @ G) != D # answer(A). [ur(1201,b,3742,a(flip)),demod(9(15),9(14))]. given #444 (T,wt=14): 1216 (x @ y) * z != u | (y @ x) * u = z. [para(1154(a,1),22(a,1,2,2,2)),demod(197(4),1191(4),1154(7),197(6)),flip(a)]. given #445 (T,wt=14): 1219 x * (y @ z) * u != u | z @ y = x. [para(1154(a,1),23(a,1,2,2,2)),demod(197(3),1154(8),197(7),1191(7))]. given #446 (A,wt=18): 295 x * (y * x @ z) != y * x * z | z * y = c_0. [para(21(a,1),191(a,1)),flip(a)]. given #447 (F,wt=17): 4002 (G @ F) * (C @ (A @ B)) * D * (F @ G) != D # answer(A). [ur(1201,b,2902,a(flip)),demod(9(15),9(14))]. given #448 (F,wt=17): 4003 (G @ F) * D * (C @ (A @ B)) * (F @ G) != D # answer(A). [ur(1201,b,2670,a(flip)),demod(9(15),9(14))]. given #449 (T,wt=14): 1253 x * y * (y @ z) != y | z @ y = x. [back_demod(1167),demod(1191(4)),flip(a)]. given #450 (T,wt=14): 1489 (x @ y) * z != y | y * (y @ x) = z. [para(1254(a,1),7(a,1)),flip(a)]. given #451 (A,wt=24): 296 x * y * z * y * x * u != z * x * y * u | y * x = c_0. [para(25(a,1),191(a,1))]. given #452 (F,wt=17): 4004 (F @ G) * (C @ (B @ A)) * D * (G @ F) != D # answer(A). [ur(1201,b,2599,a(flip)),demod(9(15),9(14))]. given #453 (F,wt=17): 4005 (A @ B) * C * (D @ (G @ F)) * (B @ A) != C # answer(A). [ur(1201,b,2565,a(flip)),demod(9(15),9(14))]. given #454 (T,wt=14): 1538 x * y * z != y | z @ y = x * z. [para(1254(a,1),60(a,1)),flip(a),flip(b)]. given #455 (T,wt=14): 1541 x * y != z * x | z * (y @ x) = y. [para(1254(a,1),62(a,1,2)),flip(a)]. given #456 (A,wt=23): 298 x * y * (x @ y) * z * y * x = x * y * z * x * y. [para(27(a,1),19(a,1))]. given #457 (F,wt=17): 4006 (G @ F) * D * (F @ G) * (C @ (A @ B)) != D # answer(A). [ur(1201,b,2537,a(flip)),demod(2366(14),9(15),9(14))]. given #458 (F,wt=17): 4007 (D @ (G @ F)) * (A @ B) * C * (B @ A) != C # answer(A). [ur(1201,b,2526,a(flip)),demod(9(15),9(14))]. given #459 (T,wt=14): 1559 x * (y @ x) != z * x | y @ x = z. [para(1532(a,1),17(a,1,2,2)),demod(197(2)),flip(a)]. given #460 (T,wt=14): 1613 x * y * z != z | y @ x = y * x. [para(1191(a,1),163(a,1)),flip(a),flip(b)]. given #461 (A,wt=23): 299 x * y * z * (z @ x) * y * x = y * z * x * x * y. [para(19(a,1),27(a,1,2)),flip(a)]. given #462 (F,wt=17): 4008 (A @ B) * (D @ (G @ F)) * C * (B @ A) != C # answer(A). [ur(1201,b,2466,a(flip)),demod(9(15),9(14))]. given #463 (F,wt=17): 4032 (D @ (G @ F)) * C != (B @ A) * C * (A @ B) # answer(A). [ur(1216,b,4000,a),demod(2366(5))]. given #464 (T,wt=14): 1619 (x @ y) * z != y * (x @ y) | y = z. [para(1558(a,1),7(a,1)),flip(a)]. given #465 (T,wt=14): 1620 (x @ y) * z != y * (x @ y) | z = y. [para(1558(a,1),7(a,2))]. given #466 (A,wt=24): 300 x * y * z * u * y * x != y | x * z * u * x * y = c_0. [para(27(a,1),190(a,1)),flip(b)]. given #467 (F,wt=17): 4033 (D @ (G @ F)) * C * (B @ A) != (B @ A) * C # answer(A). [ur(1216,b,3743,a),demod(2366(5))]. given #468 (F,wt=17): 4034 (G @ F) * D != (C @ (B @ A)) * D * (G @ F) # answer(A). [ur(1216,b,3742,a),demod(2366(5)),flip(a)]. given #469 (T,wt=14): 2399 x * y != y | x * (x @ y) = x @ y. [back_demod(1599),demod(2350(4)),flip(b)]. given #470 (T,wt=14): 2845 x @ (y @ z) != c_0 | x @ (z @ y) = c_0. [para(2366(a,1),1218(a,1))]. given #471 (A,wt=24): 301 x * y * z * u * y * x != x * z * u * x * y | c_0 = y. [para(27(a,1),193(a,1))]. given #472 (F,wt=17): 4035 (F @ G) * D * (G @ F) != (C @ (A @ B)) * D # answer(A). [ur(1216,b,2902,a)]. given #473 (F,wt=17): 4036 C * (D @ (F @ G)) != (A @ B) * C * (B @ A) # answer(A). [ur(1216,b,2671,a),flip(a)]. given #474 (T,wt=14): 2846 (x @ y) @ z != c_0 | (y @ x) @ z = c_0. [para(2366(a,2),1218(a,1))]. given #475 (T,wt=14): 3689 x * y != z | (y @ x) * z = y * x. [para(1191(a,1),420(a,1)),flip(a),flip(b)]. given #476 (A,wt=24): 302 x * y * z * u * y * x != z * u * x * y | y * x = c_0. [para(27(a,1),191(a,1))]. given #477 (F,wt=17): 4037 (F @ G) * D * (G @ F) != D * (C @ (A @ B)) # answer(A). [ur(1216,b,2670,a)]. given #478 (F,wt=17): 4038 C * (D @ (G @ F)) != (B @ A) * C * (A @ B) # answer(A). [ur(1216,b,2565,a),flip(a)]. given #479 (T,wt=14): 3823 x * y != z * x | (x @ z) * y = z. [para(1191(a,1),916(a,1,2)),flip(b)]. given #480 (T,wt=14): 3824 x * x * (y @ x) != y * x | y = x. [para(1558(a,1),916(a,1,2))]. given #481 (A,wt=16): 303 x * y * z * u != x * y * z | c_0 = u. [para(9(a,1),200(a,1,2))]. given #482 (F,wt=17): 4039 (G @ F) * D != D * (C @ (B @ A)) * (G @ F) # answer(A). [ur(1216,b,2564,a)]. given #483 (F,wt=17): 4045 (F @ G) * D * (G @ F) * (C @ (B @ A)) != D # answer(A). [ur(1216,b,2797,a(flip))]. given #484 (T,wt=14): 3851 x * x * (y @ x) != y * x | x = y. [para(1558(a,1),917(a,1,2))]. given #485 (T,wt=14): 3875 x * (x @ y) != z | (y @ x) * z = x. [para(1191(a,1),1040(a,1)),flip(a),flip(b)]. given #486 (A,wt=16): 304 x * y * z != x * z | y * (y @ z) = c_0. [para(10(a,1),200(a,1,2)),flip(b)]. given #487 (F,wt=17): 4046 (A @ B) * C * (B @ A) * (D @ (G @ F)) != C # answer(A). [ur(1216,b,2796,a(flip))]. given #488 (F,wt=17): 4097 (F @ G) * D != D * (C @ (A @ B)) * (F @ G) # answer(A). [ur(1216,b,4003,a)]. given #489 (T,wt=14): 3967 x != y | (z @ y) * x = y * (z @ y). [para(1191(a,1),1186(a,1)),flip(b)]. given #490 (T,wt=14): 3994 x * y * (y @ z) != x | z @ y = y. [para(914(a,1),1196(a,1,2))]. given #491 (A,wt=24): 306 x * y * z * u * z * y != x * z | y * u * y * z = c_0. [para(11(a,1),200(a,1,2)),flip(b)]. given #492 (F,wt=17): 4141 C * (D @ (G @ F)) * (B @ A) != (B @ A) * C # answer(A). [ur(1216,b,4005,a),flip(a)]. given #493 (F,wt=19): 2486 x * (D @ (G @ F)) * y != x * (C @ (A @ B)) * y # answer(A). [back_demod(1681),demod(2366(5))]. given #494 (T,wt=12): 4469 x * (y @ z) != x | y @ z = c_0. [para(1228(a,1),3994(a,1,2,2)),demod(197(3),1228(6)),flip(b)]. given #495 (T,wt=14): 3995 x * y != x | (z @ u) * y = z @ u. [para(1191(a,1),1196(a,1,2)),flip(b)]. given #496 (A,wt=20): 307 x * y * z * y * x != y * x | z * x * y = c_0. [para(11(a,1),200(a,1)),flip(b)]. given #497 (F,wt=19): 2498 x * (D @ (F @ G)) * C != x * C * (C @ (B @ A)) # answer(A). [back_demod(1625),demod(2366(6)),flip(a)]. given #498 (F,wt=19): 2499 (D @ (G @ F)) * (A @ B) * (C @ (B @ A)) != A @ B # answer(A). [back_demod(1615),demod(2366(5),2366(13))]. given #499 (T,wt=14): 3996 x * y * (z @ y) != x | y @ z = y. [para(1558(a,1),1196(a,1,2))]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 24 (0.00 of 1.94 sec). given #500 (T,wt=14): 4050 x != y | (z @ u) * y = (z @ u) * x. [para(1191(a,1),1216(a,1))]. given #501 (A,wt=24): 308 x * y * z * y * x * u != y * x * z * x * y | c_0 = u. [para(11(a,1),200(a,2)),demod(9(4),9(3),9(2))]. given #502 (F,wt=19): 2501 (F @ G) * (D @ (F @ G)) != (C @ (B @ A)) * (F @ G) # answer(A). [back_demod(1561),demod(2366(5)),flip(a)]. given #503 (F,wt=19): 2511 (C @ (B @ A)) * (F @ G) * (D @ (G @ F)) != F @ G # answer(A). [back_demod(1493),demod(2366(5),2366(13))]. given #504 (T,wt=14): 4051 x * (y @ x) != z | (x @ y) * z = x. [para(1558(a,1),1216(a,1))]. given #505 (T,wt=14): 4060 x @ (y @ z) != u | (z @ y) @ x = u. [para(2801(a,1),1219(a,1,2)),demod(197(2)),flip(a)]. given #506 (A,wt=20): 309 x * y * z * u != x * z | y * (y @ z) * u = c_0. [para(19(a,1),200(a,1,2)),flip(b)]. given #507 (F,wt=19): 2515 x * y * (D @ (G @ F)) != x * y * (C @ (A @ B)) # answer(A). [back_demod(1480),demod(2366(5))]. given #508 (F,wt=19): 2535 x * (D @ (G @ F)) * (C @ (B @ A)) * y != x * y # answer(A). [back_demod(1360),demod(2366(5),2366(10))]. given #509 (T,wt=14): 4061 (x @ y) @ z != u | z @ (y @ x) = u. [para(2802(a,1),1219(a,1,2)),demod(197(2)),flip(a)]. given #510 (T,wt=14): 4124 x != y | (y @ z) * x = y * (y @ z). [para(1191(a,1),1489(a,1)),flip(b)]. given #511 (A,wt=16): 310 x * y * z != y * x | (x @ y) * z = c_0. [para(19(a,1),200(a,1)),flip(b)]. given #512 (F,wt=19): 2540 x * (C @ (B @ A)) * (D @ (G @ F)) * y != x * y # answer(A). [back_demod(1345),demod(2366(5),2366(10))]. given #513 (F,wt=19): 2542 x * (C @ (B @ A)) * D * (D @ (G @ F)) != x * D # answer(A). [back_demod(1333),demod(2366(5),2366(11))]. given #514 (T,wt=14): 4468 x * y * z != x | z @ y = z * y. [para(391(a,1),3994(a,1,2,2)),demod(9(3),10(3),722(5))]. given #515 (T,wt=14): 4516 x * y != x | y * (y @ z) = y @ z. [para(2340(a,1),3996(a,1,2,2)),demod(9(4),1154(3),197(2),2402(5)),flip(b)]. given #516 (A,wt=22): 312 x * y * z * u != x * u | y * z * (y * z @ u) = c_0. [para(21(a,1),200(a,1,2)),flip(b)]. given #517 (F,wt=19): 2562 x * y * (C @ (B @ A)) * (D @ (G @ F)) != x * y # answer(A). [back_demod(1214),demod(2366(5),2366(10))]. given #518 (F,wt=19): 2563 x * y * (D @ (G @ F)) * (C @ (B @ A)) != x * y # answer(A). [back_demod(1212),demod(2366(5),2366(10))]. given #519 (T,wt=14): 4536 x != y | (x @ z) * y = x * (x @ z). [para(2340(a,1),4051(a,1,2)),demod(9(4),1154(3),197(2),2402(4))]. given #520 (T,wt=15): 403 (x @ y) * z * y * x = z * x * y. [hyper(51,a,19,a(flip)),flip(a)]. given #521 (A,wt=18): 313 x * y * z != z * x | y * (x * y @ z) = c_0. [para(21(a,1),200(a,1)),flip(b)]. given #522 (F,wt=17): 4711 (D @ (F @ G)) * C * A * B != C * A * B # answer(A). [para(403(a,1),503(a,2)),demod(1560(13),914(12),10(13))]. given #523 (F,wt=17): 5006 (D @ (G @ F)) * C * A * B != C * A * B # answer(A). [ur(1216,b,4711,a),demod(2366(5))]. given #524 (T,wt=11): 4674 (y @ z) @ x * z * y = c_0. [para(403(a,1),305(a,1)),demod(9(6),9(5),10(5)),xx(a)]. given #525 (T,wt=11): 4676 x * z * y @ (y @ z) = c_0. [para(403(a,1),305(a,2)),demod(9(4),9(3),10(3)),xx(a)]. given #526 (A,wt=24): 314 x * y * z * y * x * u != y * x | z * x * y * u = c_0. [para(25(a,1),200(a,1)),flip(b)]. given #527 (F,wt=17): 5019 (D @ (F @ G)) * A * B * C != A * B * C # answer(A). [ur(61,b,4711,a(flip)),demod(9(17),9(16),9(15),21(16),9(16))]. given #528 (F,wt=17): 5035 (D @ (G @ F)) * A * B * C != A * B * C # answer(A). [ur(61,b,5006,a(flip)),demod(9(17),9(16),9(15),21(16),9(16))]. given #529 (T,wt=11): 4696 x * y * z @ (y @ z) = c_0. [para(403(a,1),391(a,1,1)),demod(4676(8))]. given #530 (T,wt=11): 4721 (x @ y) @ z * x * y = c_0. [para(403(a,1),722(a,1,2)),demod(4674(8))]. given #531 (A,wt=24): 315 x * y * z * u * y * x != y * x | z * u * x * y = c_0. [para(27(a,1),200(a,1)),flip(b)]. given #532 (F,wt=17): 5178 (D @ (F @ G)) * B * C * A != B * C * A # answer(A). [ur(61,b,5019,a(flip)),demod(9(17),9(16),9(15),21(16),9(16))]. given #533 (F,wt=17): 5195 (D @ (G @ F)) * B * C * A != B * C * A # answer(A). [ur(61,b,5035,a(flip)),demod(9(17),9(16),9(15),21(16),9(16))]. given #534 (T,wt=11): 5060 ((x @ y) @ z) @ u * z = c_0. [para(1191(a,1),4674(a,1,2,2)),demod(2366(4,R),722(4))]. given #535 (T,wt=11): 5124 x * y @ ((z @ u) @ y) = c_0. [para(1191(a,1),4676(a,1,1,2)),demod(2366(5,R),722(5))]. given #536 (A,wt=18): 316 x * y @ z != x * y * z | z * x * y = c_0. [para(9(a,1),287(a,2))]. given #537 (F,wt=19): 2569 D * D * (D @ (F @ G)) != (C @ (B @ A)) * D * D # answer(A). [back_demod(1152),demod(2366(5)),flip(a)]. given #538 (F,wt=19): 2574 D * (D @ (F @ G)) * x != (C @ (B @ A)) * D * x # answer(A). [back_demod(1120),demod(2366(5)),flip(a)]. given #539 (T,wt=11): 5305 x * y @ (y @ (z @ u)) = c_0. [hyper(4061,a,5060,a)]. given #540 (T,wt=11): 5306 (x @ (y @ z)) @ u * x = c_0. [hyper(2846,a,5060,a)]. given #541 (A,wt=18): 324 x * y * z != z * x * y | x * y @ z = c_0. [para(9(a,1),305(a,1))]. given #542 (F,wt=19): 2582 x * D * (D @ (F @ G)) != x * (C @ (B @ A)) * D # answer(A). [back_demod(1051),demod(2366(5)),flip(a)]. given #543 (F,wt=19): 2585 (D @ (F @ G)) * (A @ B) != (A @ B) * (C @ (B @ A)) # answer(A). [back_demod(1044),demod(2366(8)),flip(a)]. given #544 (T,wt=13): 4819 x * y * z @ x * z * y = c_0. [para(403(a,1),2304(a,1,2)),demod(4676(9))]. given #545 (T,wt=13): 5041 (x @ y) @ z * u * y * x = c_0. [para(9(a,1),4674(a,1,2))]. given #546 (A,wt=18): 325 x * y * z != z * x * y | z @ x * y = c_0. [para(9(a,1),305(a,2)),flip(a)]. given #547 (F,wt=19): 2638 x * y * (D @ (F @ G)) != x * y * (C @ (B @ A)) # answer(A). [back_demod(34),demod(2366(5)),flip(a)]. given #548 (F,wt=19): 2641 x * (D @ (F @ G)) * y != x * (C @ (B @ A)) * y # answer(A). [back_demod(31),demod(2366(5)),flip(a)]. given #549 (T,wt=13): 5070 (x @ y) @ z * y * x * x = c_0. [para(2304(a,1),4674(a,1,1)),demod(9(3))]. given #550 (T,wt=13): 5101 x * y * z @ (x @ z * y) = c_0. [para(403(a,1),4674(a,1,2)),demod(2366(5))]. given #551 (A,wt=22): 345 x * y * z * u * v != x * y * z * u * w | v = w. [para(9(a,1),48(a,1,2,2)),demod(9(6))]. given #552 (F,wt=19): 2960 (G @ F) * (D @ (G @ F)) != (C @ (A @ B)) * (G @ F) # answer(A). [para(1558(a,1),2520(a,1))]. given #553 (F,wt=19): 2962 (D @ (G @ F)) * (B @ A) * (C @ (B @ A)) != B @ A # answer(A). [para(1558(a,1),2546(a,1,2))]. given #554 (T,wt=13): 5104 x * y * z * u @ (u @ z) = c_0. [para(9(a,1),4676(a,1,1))]. given #555 (T,wt=13): 5135 x * y * z * z @ (z @ y) = c_0. [para(2304(a,1),4676(a,1,2)),demod(9(2))]. given #556 (A,wt=22): 346 x * y * z * u != x * y * v * z | v * (v @ z) = u. [para(10(a,1),48(a,1,2,2)),flip(a)]. given #557 (F,wt=19): 3000 (C @ (B @ A)) * (G @ F) * (D @ (G @ F)) != G @ F # answer(A). [para(1558(a,1),2550(a,1,2))]. given #558 (F,wt=19): 3117 (D @ (F @ G)) * (B @ A) != (B @ A) * (C @ (B @ A)) # answer(A). [para(1558(a,1),2643(a,2))]. given #559 (T,wt=13): 5163 x * y * z @ (z * y @ x) = c_0. [para(403(a,1),4676(a,1,1))]. given #560 (T,wt=13): 5201 x * y * z * u @ (z @ u) = c_0. [para(9(a,1),4696(a,1,1))]. given #561 (A,wt=18): 347 x * y * z * u != x * z * y | z @ y = u. [para(10(a,1),48(a,1,2)),flip(a)]. given #562 (F,wt=19): 3652 (C @ (A @ B)) * D * D * (D @ (F @ G)) != D * D # answer(A). [para(914(a,1),1677(a,1,2,2))]. given #563 (F,wt=19): 3737 (D @ (F @ G)) * C * C * (C @ (A @ B)) != C * C # answer(A). [para(914(a,1),1714(a,1,2,2))]. given #564 (T,wt=13): 5217 x * y * z * z @ (y @ z) = c_0. [para(2350(a,1),4696(a,1,2)),demod(9(2))]. given #565 (T,wt=13): 5239 (x @ y) @ z * u * x * y = c_0. [para(9(a,1),4721(a,1,2))]. given #566 (A,wt=22): 348 x * y * z * y * x != y * x * z * u | x * y = u. [para(11(a,1),48(a,1))]. given #567 (F,wt=19): 3857 D * D * (D @ (G @ F)) != (C @ (A @ B)) * D * D # answer(A). [para(914(a,1),2465(a,1,2))]. given #568 (F,wt=19): 3905 (D @ (G @ F)) * C * C != C * C * (C @ (A @ B)) # answer(A). [para(914(a,1),2471(a,2,2))]. given #569 (T,wt=13): 5251 (x @ y) @ z * x * y * y = c_0. [para(2350(a,1),4721(a,1,1)),demod(9(3))]. given #570 (T,wt=13): 5307 ((x @ y) @ z) @ u * v * z = c_0. [para(9(a,1),5060(a,1,2))]. given #571 (A,wt=22): 349 x * y * z * u != x * z * y * v | (y @ z) * u = v. [para(19(a,1),48(a,1,2))]. given #572 (F,wt=19): 3942 (D @ (G @ F)) * C * C * (C @ (B @ A)) != C * C # answer(A). [para(914(a,1),2476(a,1,2,2))]. given #573 (F,wt=19): 3948 (D @ (F @ G)) * C * C != C * C * (C @ (B @ A)) # answer(A). [para(914(a,1),2478(a,2,2))]. given #574 (T,wt=11): 6064 ((x @ y) @ (z @ u)) @ v = c_0. [para(1154(a,1),5307(a,1,2,2)),demod(197(5))]. given #575 (T,wt=11): 6123 x @ ((y @ z) @ (u @ v)) = c_0. [hyper(4061,a,6064,a)]. given #576 (A,wt=22): 350 x * y * z * u != x * z * y * v | (z @ y) * v = u. [para(19(a,1),48(a,2,2)),flip(b)]. given #577 (F,wt=19): 3951 (D @ (G @ F)) * (F @ G) * (C @ (B @ A)) != F @ G # answer(A). [ur(1186,b,2642,a),demod(2366(5))]. given #578 (F,wt=19): 3952 (D @ (F @ G)) * (G @ F) * (C @ (A @ B)) != G @ F # answer(A). [ur(1186,b,2519,a),demod(2366(5))]. given #579 (T,wt=13): 5318 ((x @ y) @ z) @ z * (z @ u) = c_0. [para(914(a,1),5060(a,1,2))]. given #580 (T,wt=13): 5321 x @ ((y @ z) * x @ (u @ v)) = c_0. [para(1191(a,1),5060(a,1,2)),demod(2366(5))]. given #581 (A,wt=24): 351 x * y * z * u != x * v * y * z | v * (v @ y * z) = u. [para(20(a,1),48(a,1,2)),flip(a)]. given #582 (F,wt=19): 3953 (C @ (A @ B)) * (B @ A) * (D @ (F @ G)) != B @ A # answer(A). [ur(1186,b,2642,a(flip)),demod(2366(5))]. given #583 (F,wt=19): 3956 (C @ (B @ A)) * (A @ B) * (D @ (G @ F)) != A @ B # answer(A). [ur(1186,b,2519,a(flip)),demod(2366(5))]. given #584 (T,wt=13): 5322 ((x @ y) @ z) @ z * (u @ z) = c_0. [para(1558(a,1),5060(a,1,2))]. given #585 (T,wt=13): 5337 x * y * z @ ((u @ v) @ z) = c_0. [para(9(a,1),5124(a,1,1))]. given #586 (A,wt=20): 352 x * y * z * u != z * x * y | z @ x * y = u. [para(20(a,1),48(a,1)),flip(a)]. given #587 (F,wt=19): 4040 D @ (G @ F) != (G @ F) * (C @ (A @ B)) * (F @ G) # answer(A). [ur(1216,b,2482,a),flip(a)]. given #588 (F,wt=19): 4047 (B @ A) * (D @ (G @ F)) * (A @ B) != C @ (A @ B) # answer(A). [ur(1216,b,2479,a(flip))]. given #589 (T,wt=13): 5348 x * (x @ y) @ ((z @ u) @ x) = c_0. [para(914(a,1),5124(a,1,1))]. given #590 (T,wt=13): 5351 x @ ((y @ z) @ (u @ v) * x) = c_0. [para(1191(a,1),5124(a,1,1))]. given #591 (A,wt=24): 353 x * y * z * u != x * u * y * v | z * (y * z @ u) = v. [para(21(a,1),48(a,1,2))]. given #592 (F,wt=19): 4108 (C @ (A @ B)) * (G @ F) * (D @ (F @ G)) != G @ F # answer(A). [ur(1253,b,2523,a),demod(2366(13))]. given #593 (F,wt=19): 4109 (D @ (F @ G)) * (B @ A) * (C @ (A @ B)) != B @ A # answer(A). [ur(1253,b,2644,a(flip)),demod(2366(13))]. given #594 (T,wt=13): 5352 x * (y @ x) @ ((z @ u) @ x) = c_0. [para(1558(a,1),5124(a,1,1))]. given #595 (T,wt=13): 5377 x * y * z @ (z @ (u @ v)) = c_0. [para(9(a,1),5305(a,1,1))]. given #596 (A,wt=20): 354 x * y * z * u != y * z * x | y * z @ x = u. [para(21(a,1),48(a,1)),flip(a)]. given #597 (F,wt=19): 4437 (D @ (G @ F)) * (B @ A) != (B @ A) * (C @ (A @ B)) # answer(A). [ur(3875,b,2550,a),demod(2366(8)),flip(a)]. given #598 (F,wt=19): 4438 (G @ F) * (D @ (F @ G)) != (C @ (B @ A)) * (G @ F) # answer(A). [ur(3875,b,2546,a),demod(2366(8))]. given #599 (T,wt=13): 5383 x * (x @ y) @ (x @ (z @ u)) = c_0. [para(914(a,1),5305(a,1,1))]. given #600 (T,wt=13): 5385 x * (y @ x) @ (x @ (z @ u)) = c_0. [para(1558(a,1),5305(a,1,1))]. given #601 (A,wt=22): 373 x * y * z != x * u * z | u * (u @ z) = y * (y @ z). [para(10(a,1),49(a,1,2))]. given #602 (F,wt=19): 4526 (G @ F) * (C @ (B @ A)) * (F @ G) != D @ (F @ G) # answer(A). [ur(1216,b,2501,a)]. given #603 (F,wt=19): 5421 (B @ A) * (D @ (F @ G)) * (A @ B) != C @ (B @ A) # answer(A). [ur(1216,b,2585,a(flip))]. given #604 (T,wt=13): 5397 (x @ (y @ z)) @ u * v * x = c_0. [para(9(a,1),5306(a,1,2))]. given #605 (T,wt=13): 5401 (x @ (y @ z)) @ x * (x @ u) = c_0. [para(914(a,1),5306(a,1,2))]. given #606 (A,wt=18): 374 x * y * z != z * x | z @ x = y * (y @ z). [para(10(a,1),49(a,1)),flip(a),flip(b)]. given #607 (F,wt=19): 5674 D @ (G @ F) != (F @ G) * (C @ (A @ B)) * (G @ F) # answer(A). [ur(1216,b,2960,a),flip(a)]. given #608 (F,wt=19): 5813 (A @ B) * (D @ (F @ G)) * (B @ A) != C @ (B @ A) # answer(A). [ur(1216,b,3117,a(flip))]. given #609 (T,wt=13): 5402 (x @ (y @ z)) @ x * (u @ x) = c_0. [para(1558(a,1),5306(a,1,2))]. given #610 (T,wt=13): 5415 y * x @ x * x * y * y = c_0. [para(271(a,1),324(a,1)),demod(9(10),9(9),9(8)),xx(a)]. given #611 (A,wt=22): 376 x * y * z != z * x * u | (z @ x) * u = y * (y @ z). [para(19(a,1),49(a,1)),flip(a),flip(b)]. given #612 (F,wt=19): 6381 (A @ B) * (D @ (G @ F)) * (B @ A) != C @ (A @ B) # answer(A). [ur(1216,b,4437,a(flip))]. given #613 (F,wt=19): 6383 (F @ G) * (C @ (B @ A)) * (G @ F) != D @ (F @ G) # answer(A). [ur(1216,b,4438,a)]. given #614 (T,wt=13): 5567 x * x * y * y @ y * x = c_0. [para(271(a,1),325(a,1)),demod(9(10),9(9),9(8)),xx(a)]. given #615 (T,wt=13): 5833 x * y * z @ (y * x @ z) = c_0. [para(5163(a,1),391(a,2)),demod(1560(5),4734(4),3463(5))]. given #616 (A,wt=24): 377 x * y * z != u * x * z | u * (u @ x * z) = y * (y @ z). [para(20(a,1),49(a,1)),flip(a),flip(b)]. given #617 (F,wt=21): 969 B * A * (D @ (F @ G)) * C * (A @ B) != A * B * C # answer(A). [ur(149,b,430,a(flip)),flip(a)]. given #618 (F,wt=21): 977 C * (D @ (F @ G)) * (A @ B) * x != (A @ B) * C * x # answer(A). [ur(582,b,918,a),demod(9(6),9(18),9(17)),flip(a)]. given #619 (T,wt=13): 6167 x * y @ (y * x @ (z @ u)) = c_0. [para(391(a,1),5318(a,1,2,2)),demod(9(6),10(6),2366(5))]. given #620 (T,wt=13): 6184 x @ (x * (x @ y) @ (z @ u)) = c_0. [para(914(a,1),5321(a,1,2,1))]. given #621 (A,wt=24): 379 x * y * z != z * u * x | y * (x * y @ z) = u * (u @ x). [para(21(a,1),49(a,1)),flip(b)]. given #622 (F,wt=17): 6589 C * (D @ (F @ G)) * A * B != C * A * B # answer(A). [para(403(a,1),977(a,2)),demod(1560(13),914(12),10(13))]. given #623 (F,wt=21): 1026 B * A * C * (D @ (F @ G)) * (A @ B) != A * B * C # answer(A). [ur(149,b,925,a(flip)),flip(a)]. given #624 (T,wt=13): 6185 x @ (x * (y @ x) @ (z @ u)) = c_0. [para(1558(a,1),5321(a,1,2,1))]. given #625 (T,wt=13): 6294 x * y @ ((z @ u) @ y * x) = c_0. [para(391(a,1),5348(a,1,1,2)),demod(9(3),10(3))]. given #626 (A,wt=22): 383 x * y * z * y * x != x * y | x @ y = z * x * y. [para(11(a,1),50(a,1))]. given #627 (F,wt=21): 1056 C * (A @ B) * D * (D @ (F @ G)) != (A @ B) * C * D # answer(A). [para(914(a,1),65(a,1,2,2))]. given #628 (F,wt=21): 1077 (D @ (F @ G)) * C * A * (A @ B) != (A @ B) * C * A # answer(A). [para(914(a,1),503(a,1,2,2))]. given #629 (T,wt=13): 6308 x @ ((y @ z) @ x * (x @ u)) = c_0. [para(914(a,1),5351(a,1,2,2))]. given #630 (T,wt=13): 6309 x @ ((y @ z) @ x * (u @ x)) = c_0. [para(1558(a,1),5351(a,1,2,2))]. given #631 (A,wt=22): 384 x * y * z * u != z * x | z @ x = y * (y @ z) * u. [para(19(a,1),50(a,1,2))]. given #632 (F,wt=21): 1224 x * D * (F @ G) * (C @ (A @ B)) != x * (F @ G) * D # answer(A). [para(1154(a,1),120(a,1,2,2,2)),demod(197(6)),flip(a)]. given #633 (F,wt=21): 1230 G * F * D * (F @ G) * (C @ (A @ B)) != F * G * D # answer(A). [para(1154(a,1),279(a,1,2,2,2)),demod(197(5)),flip(a)]. given #634 (T,wt=13): 6527 x * y * z @ (z @ y * x) = c_0. [hyper(2845,a,5833,a)]. given #635 (T,wt=15): 406 x * y * z @ x * y = z @ x * y. [para(9(a,1),391(a,1,1))]. given #636 (A,wt=20): 387 x * y * z != z * y | z @ y = x * (x @ y * z). [para(20(a,1),50(a,1))]. given #637 (F,wt=21): 1354 D * (F @ G) * (C @ (A @ B)) * x != (F @ G) * D * x # answer(A). [para(1191(a,1),68(a,1,2,2)),flip(a)]. given #638 (F,wt=21): 1363 x * (B @ A) * C * (A @ B) * (D @ (F @ G)) != x * C # answer(A). [para(1191(a,1),66(a,2,2))]. given #639 (T,wt=15): 642 x * y * x * (y @ x) = y * x * x. [para(531(a,1),10(a,1,2,2)),demod(197(5),422(4),9(6),9(5)),flip(a)]. given #640 (T,wt=15): 653 x * y * z * z @ (x * y @ z) = c_0. [para(9(a,1),648(a,1,1))]. given #641 (A,wt=24): 388 x * y * z * u != u * x | u @ x = y * z * (y * z @ u). [para(21(a,1),50(a,1,2))]. given #642 (F,wt=21): 1367 (B @ A) * C * (A @ B) * (D @ (F @ G)) * x != C * x # answer(A). [para(1191(a,1),94(a,2))]. given #643 (F,wt=21): 1400 (D @ (F @ G)) * C * x != (A @ B) * C * (B @ A) * x # answer(A). [para(1191(a,1),503(a,1,2,2))]. given #644 (T,wt=15): 750 x * y @ x * y * z = x * y @ z. [para(9(a,1),722(a,1,2))]. given #645 (T,wt=15): 912 x * (y @ x) * (x * (y @ x) @ y) = x. [hyper(89,a,855,a)]. given #646 (A,wt=20): 389 x * y * z != x * z | y * (x * y @ z) = x @ z. [para(21(a,1),50(a,1)),flip(b)]. given #647 (F,wt=21): 1507 D * (F @ G) * C * (C @ (A @ B)) != (F @ G) * D * C # answer(A). [para(1254(a,1),68(a,1,2,2)),flip(a)]. given #648 (F,wt=21): 1539 (D @ (F @ G)) * C * B != (A @ B) * C * B * (B @ A) # answer(A). [para(1254(a,1),503(a,1,2,2))]. given #649 (T,wt=11): 7031 x * (y @ x) @ y = x @ y. [hyper(1196,a,912,a),flip(a)]. given #650 (T,wt=11): 7080 x @ y * (x @ y) = x @ y. [para(7031(a,1),2340(a,1,2,2)),demod(9(4),1154(3),197(2)),flip(a)]. given #651 (A,wt=18): 397 x * (x @ y) != z * x | x @ y = z * (z @ x). [para(328(a,1),16(a,1)),demod(391(8)),flip(b)]. given #652 (F,wt=21): 1648 (D @ (F @ G)) * C * B * (A @ B) != (A @ B) * C * B # answer(A). [para(1558(a,1),503(a,1,2,2))]. given #653 (F,wt=21): 1721 (x @ y) * (C @ (A @ B)) * (D @ (F @ G)) * (y @ x) != c_0 # answer(A). [ur(1189,b,1310,a(flip))]. given #654 (T,wt=13): 7067 x * y * y @ y * x = y @ x. [para(391(a,1),7031(a,1,1,2)),demod(6942(4),722(6))]. given #655 (T,wt=13): 7068 x * (y @ x) @ y * x = x @ y. [para(7031(a,1),722(a,2)),demod(9(5),914(4),10(5))]. given #656 (A,wt=22): 401 x * y * (y @ z) != x * u * y | y @ z = u * (u @ y). [para(328(a,1),49(a,1,2)),demod(391(10)),flip(b)]. given #657 (F,wt=21): 1723 (x @ y) * (D @ (F @ G)) * (C @ (A @ B)) * (y @ x) != c_0 # answer(A). [ur(1189,b,1281,a(flip))]. given #658 (F,wt=21): 1791 x * (D @ (F @ G)) * C != x * (A @ B) * C * (B @ A) # answer(A). [ur(378,b,1237,a),flip(a)]. given #659 (T,wt=13): 7097 x * (y @ x) @ x * y = x @ y. [back_demod(6942),demod(7067(8))]. given #660 (T,wt=13): 7103 x * y @ y * (x @ y) = x @ y. [para(7080(a,1),391(a,2)),demod(9(3),914(2),10(3))]. given #661 (A,wt=18): 404 x * y * y * x != y * x * z | x * y = z. [para(187(a,1),51(a,1,2,2)),demod(187(9))]. given #662 (F,wt=19): 7209 (C @ (B @ A)) * x * C != x * (D @ (F @ G)) * C # answer(A). [para(403(a,2),1791(a,2)),demod(3037(17),2366(13),9(22),1154(21),197(16)),flip(a)]. given #663 (F,wt=19): 7268 (C @ (A @ B)) * x * (D @ (F @ G)) * C != x * C # answer(A). [ur(1216,b,7209,a),demod(2366(5))]. given #664 (T,wt=13): 7104 x * y @ y * x * x = y @ x. [para(391(a,1),7080(a,1,2,2)),demod(7018(4),391(6))]. given #665 (T,wt=13): 7125 x * y @ x * (y @ x) = y @ x. [back_demod(7018),demod(7104(8))]. given #666 (A,wt=17): 409 x * (x @ y) * z @ y = x * y * z @ y. [para(19(a,1),391(a,1,1)),flip(a)]. given #667 (F,wt=21): 1797 B * A * (D @ (F @ G)) * C != A * B * C * (B @ A) # answer(A). [ur(161,b,1237,a(flip))]. given #668 (F,wt=21): 1889 (B @ A) * (D @ (F @ G)) * C * (A @ B) * x != C * x # answer(A). [ur(582,b,1394,a),demod(9(18),9(17),9(16)),flip(a)]. given #669 (T,wt=14): 7046 x * y * y != y | y @ x = x * y. [back_demod(6890),demod(7031(6))]. given #670 (T,wt=14): 7048 x * y * y != x * y | y @ x = y. [back_demod(6862),demod(7031(7))]. given #671 (A,wt=25): 412 x * y * z * y * x * u @ y = x * z * x * y * u @ y. [para(25(a,1),391(a,1,1))]. given #672 (F,wt=21): 1890 x * (B @ A) * (D @ (F @ G)) * C * (A @ B) != x * C # answer(A). [ur(378,b,1394,a),flip(a)]. given #673 (F,wt=21): 1894 (F @ G) * D * x != (C @ (A @ B)) * D * (F @ G) * x # answer(A). [ur(582,b,1395,a),demod(9(12),9(11),9(18)),flip(a)]. given #674 (T,wt=14): 7087 x != y | (z @ x) * y = x * (z @ x). [para(7031(a,1),3875(a,1,2)),demod(9(4),1154(3),197(2),7080(4))]. given #675 (T,wt=14): 7088 x * y != x | y * (z @ y) = z @ y. [para(7031(a,1),3994(a,1,2,2)),demod(9(4),1154(3),197(2),7080(5)),flip(b)]. given #676 (A,wt=23): 413 x * y * z * y * x @ u = y * x * z * x * y @ u. [para(26(a,1),391(a,1,1)),demod(391(6))]. given #677 (F,wt=17): 7384 (C @ (A @ B)) * D * F * G != D * F * G # answer(A). [para(403(a,1),1894(a,1)),demod(1560(18),914(17),10(18)),flip(a)]. given #678 (F,wt=17): 7392 (C @ (B @ A)) * D * F * G != D * F * G # answer(A). [ur(1216,b,7384,a),demod(2366(5))]. given #679 (T,wt=15): 1043 (x @ y) * x * z = x * (x @ y) * z. [para(914(a,1),9(a,1,1)),demod(9(3)),flip(a)]. given #680 (T,wt=13): 7507 (x @ y) @ y * (y @ z) * x = c_0. [para(1043(a,1),4674(a,1,2))]. given #681 (A,wt=18): 427 x * (y @ z) * u != x * y * z | z * y = u. [para(402(a,1),13(a,1,2)),flip(a)]. given #682 (F,wt=17): 7400 (C @ (A @ B)) * F * G * D != F * G * D # answer(A). [ur(61,b,7384,a(flip)),demod(9(17),9(16),9(15),21(16),9(16))]. given #683 (F,wt=17): 7412 (C @ (B @ A)) * F * G * D != F * G * D # answer(A). [ur(61,b,7392,a(flip)),demod(9(17),9(16),9(15),21(16),9(16))]. given #684 (T,wt=13): 7509 x * (x @ y) * z @ (z @ x) = c_0. [para(1043(a,1),4676(a,1,1))]. given #685 (T,wt=13): 7511 x * (x @ y) * z @ (x @ z) = c_0. [para(1043(a,1),4696(a,1,1))]. given #686 (A,wt=18): 436 x * y * z != u * z * y | x * (y @ z) = u. [para(402(a,1),14(a,1,2))]. given #687 (F,wt=17): 7625 (C @ (A @ B)) * G * D * F != G * D * F # answer(A). [ur(61,b,7400,a(flip)),demod(9(17),9(16),9(15),21(16),9(16))]. given #688 (F,wt=17): 7636 (C @ (B @ A)) * G * D * F != G * D * F # answer(A). [ur(61,b,7412,a(flip)),demod(9(17),9(16),9(15),21(16),9(16))]. given #689 (T,wt=13): 7513 (x @ y) @ x * (x @ z) * y = c_0. [para(1043(a,1),4721(a,1,2))]. given #690 (T,wt=13): 7566 x * y @ (x @ (z @ x) * y) = c_0. [para(1191(a,1),7507(a,1,2,2)),demod(2366(5))]. given #691 (A,wt=18): 438 x * y * z * u != u * z | u @ z = x * y. [para(402(a,1),14(a,2)),flip(b)]. given #692 (F,wt=21): 1895 x * (F @ G) * D != x * (C @ (A @ B)) * D * (F @ G) # answer(A). [ur(378,b,1395,a),flip(a)]. given #693 (F,wt=21): 1896 G * F * (C @ (A @ B)) * D * (F @ G) != F * G * D # answer(A). [ur(161,b,1395,a)]. given #694 (T,wt=13): 7586 x * y @ (x * (z @ x) @ y) = c_0. [para(7031(a,1),7507(a,1,2,2,1)),demod(9(8),1191(7),2366(5))]. given #695 (T,wt=13): 7651 x * y @ ((z @ x) * y @ x) = c_0. [para(1191(a,1),7509(a,1,1,2))]. given #696 (A,wt=20): 439 x * (y @ z) != y * z | x * (x @ (y @ z)) = z * y. [para(402(a,1),16(a,1)),flip(a)]. given #697 (F,wt=21): 1975 (B @ A) * C * (D @ (F @ G)) * (A @ B) * x != C * x # answer(A). [ur(582,b,1425,a),demod(9(18),9(17),9(16)),flip(a)]. given #698 (F,wt=21): 1976 x * (B @ A) * C * (D @ (F @ G)) * (A @ B) != x * C # answer(A). [ur(378,b,1425,a),flip(a)]. given #699 (T,wt=13): 7673 x * y @ (y @ x * (z @ x)) = c_0. [para(7031(a,1),7509(a,1,1,2,1)),demod(9(5),1191(4))]. given #700 (T,wt=14): 7473 x * y * z != x * y | x * z = x. [para(1043(a,1),916(a,1,2)),demod(19(4)),flip(b)]. given #701 (A,wt=25): 451 x * y * (D @ (F @ G)) * C * (A @ B) != x * y * (A @ B) * C # answer(A). [para(402(a,1),47(a,1,2,2)),flip(a)]. given #702 (F,wt=21): 2411 (G @ F) * (C @ (B @ A)) * (F @ G) * (D @ (G @ F)) != c_0 # answer(A). [back_demod(2263),demod(2366(8),2366(16))]. given #703 (F,wt=21): 2432 A * B * (D @ (G @ F)) * C != B * A * C * (A @ B) # answer(A). [back_demod(2034),demod(2366(7))]. given #704 (T,wt=15): 1059 x * y * y * (y @ x) = y * x * y. [para(914(a,1),19(a,1,2,2))]. given #705 (T,wt=15): 1409 (x @ y) @ (y @ x) * z = (x @ y) @ z. [para(1191(a,1),722(a,1,2)),flip(a)]. given #706 (A,wt=25): 453 x * y * (y * z @ x) * y * x * z = y * x * y * z * x. [para(402(a,1),25(a,1,2,2)),demod(9(2)),flip(a)]. given #707 (F,wt=21): 2433 (A @ B) * (D @ (G @ F)) * C * x != C * (A @ B) * x # answer(A). [back_demod(2033),demod(2366(8))]. given #708 (F,wt=21): 2440 x * (G @ F) * D * (F @ G) != x * (C @ (B @ A)) * D # answer(A). [back_demod(1981),demod(2366(5)),flip(a)]. given #709 (T,wt=15): 1560 (x @ y) * y * z = y * (x @ y) * z. [para(1532(a,1),19(a,1,2,2,1)),demod(187(3))]. given #710 (T,wt=13): 8139 (x @ y) @ y * (z @ y) * x = c_0. [para(1560(a,1),4674(a,1,2))]. given #711 (A,wt=16): 455 x * y * z != z * y | x * (y @ z) = c_0. [para(402(a,1),191(a,1,2))]. given #712 (F,wt=19): 8044 (D @ (F @ G)) * x * D != x * (C @ (B @ A)) * D # answer(A). [para(403(a,2),2440(a,1)),demod(2366(9),2350(9),9(14),1154(13),197(8))]. given #713 (F,wt=19): 8250 (D @ (G @ F)) * x * (C @ (B @ A)) * D != x * D # answer(A). [ur(1216,b,8044,a),demod(2366(5))]. given #714 (T,wt=13): 8141 x * (y @ x) * z @ (z @ x) = c_0. [para(1560(a,1),4676(a,1,1))]. given #715 (T,wt=13): 8143 x * (y @ x) * z @ (x @ z) = c_0. [para(1560(a,1),4696(a,1,1))]. given #716 (A,wt=16): 461 x * (y @ z) != x * y * z | z * y = c_0. [para(402(a,1),200(a,1,2)),flip(a),flip(b)]. given #717 (F,wt=21): 2441 (G @ F) * D * (F @ G) * x != (C @ (B @ A)) * D * x # answer(A). [back_demod(1980),demod(2366(5)),flip(a)]. given #718 (F,wt=21): 2442 C * ((A @ B) @ C * (D @ (F @ G))) != C * (D @ (F @ G)) # answer(A). [back_demod(1978),demod(2366(16,R),2349(16))]. given #719 (T,wt=13): 8145 (x @ y) @ x * (z @ x) * y = c_0. [para(1560(a,1),4721(a,1,2))]. given #720 (T,wt=13): 8212 x * y @ (x @ (x @ z) * y) = c_0. [para(1191(a,1),8139(a,1,2,2)),demod(2366(5))]. given #721 (A,wt=22): 466 x * y * (z @ u) * v != x * y * z * u | u * z = v. [para(402(a,1),48(a,1,2,2)),flip(a)]. given #722 (F,wt=21): 2443 C * ((A @ B) @ (D @ (F @ G)) * C) != (D @ (F @ G)) * C # answer(A). [back_demod(1892),demod(2366(16,R),2349(16))]. given #723 (F,wt=21): 2446 x * (D @ (G @ F)) * (A @ B) * C != x * C * (A @ B) # answer(A). [back_demod(1834),demod(2366(5))]. given #724 (T,wt=13): 8215 x * y @ (x * (x @ z) @ y) = c_0. [para(2340(a,1),8139(a,1,2,2,1)),demod(9(8),1191(7),2366(5))]. given #725 (T,wt=13): 8234 x * y * z @ (y @ x * z) = c_0. [para(1043(a,1),8139(a,1,2,2)),demod(19(6),2366(5))]. given #726 (A,wt=24): 472 x * y * (z @ u) != x * z * u | y * (y @ (z @ u)) = u * z. [para(402(a,1),49(a,1,2)),flip(a)]. given #727 (F,wt=21): 2447 (D @ (G @ F)) * (A @ B) * C * x != C * (A @ B) * x # answer(A). [back_demod(1833),demod(2366(5))]. given #728 (F,wt=21): 2448 (F @ G) * D * D * (C @ (B @ A)) != D * (F @ G) * D # answer(A). [back_demod(1832),demod(2366(10))]. given #729 (T,wt=13): 8277 x * y @ ((x @ z) * y @ x) = c_0. [para(1191(a,1),8141(a,1,1,2))]. given #730 (T,wt=13): 8282 x * y @ (y @ x * (x @ z)) = c_0. [para(2340(a,1),8141(a,1,1,2,1)),demod(9(5),1191(4))]. given #731 (A,wt=18): 473 (x @ y) * z * y != x * y | z * (z @ y) = x. [para(402(a,1),49(a,1)),flip(a)]. given #732 (F,wt=21): 2457 x * (C @ (B @ A)) * (F @ G) * D * (G @ F) != x * D # answer(A). [back_demod(1809),demod(2366(5))]. given #733 (F,wt=21): 2459 D * (D * (C @ (B @ A)) @ (F @ G)) != D * (C @ (B @ A)) # answer(A). [back_demod(1789),demod(2366(7),2366(16,R),2349(16),2366(12),2366(19))]. given #734 (T,wt=13): 8302 x * y * z @ (x * z @ y) = c_0. [para(1043(a,1),8141(a,1,1,2)),demod(19(4))]. given #735 (T,wt=14): 8539 x * y != y * y | x * (x @ y) = y. [para(177(a,1),473(a,1,1)),demod(187(3))]. given #736 (A,wt=20): 475 (x @ y) * z != z * x * y | (x @ y) @ z = y * x. [para(402(a,1),50(a,1,2)),flip(a)]. given #737 (F,wt=21): 2467 x * (A @ B) * (D @ (G @ F)) * C != x * C * (A @ B) # answer(A). [back_demod(1759),demod(2366(8))]. given #738 (F,wt=21): 2472 (x @ y) * (C @ (B @ A)) * (D @ (G @ F)) * (y @ x) != c_0 # answer(A). [back_demod(1722),demod(2366(6),2366(11))]. given #739 (T,wt=15): 2322 x * (x @ y) @ y * (y @ x) = x @ y. [back_demod(2176),demod(2304(9),391(7))]. given #740 (T,wt=15): 2382 x * y * y * x @ (x * x @ y) = c_0. [back_demod(798),demod(2349(3),2366(6))]. given #741 (A,wt=22): 489 x * y * z * u * v != w * v | x * y * z * u = w. [para(9(a,1),58(a,1,2,2))]. given #742 (F,wt=21): 2473 (x @ y) * (D @ (G @ F)) * (C @ (B @ A)) * (y @ x) != c_0 # answer(A). [back_demod(1720),demod(2366(6),2366(11))]. given #743 (F,wt=21): 2489 (C @ (B @ A)) * (F @ G) * D * G != D * G * (F @ G) # answer(A). [back_demod(1650),demod(2366(5))]. given #744 (T,wt=15): 2383 x @ y * x * x * y = x @ y * y. [back_demod(772),demod(2349(3)),flip(a)]. given #745 (T,wt=15): 2386 x * y * y * x @ (y @ x * x) = c_0. [back_demod(700),demod(2349(6))]. given #746 (A,wt=22): 490 x * y * z * u != v * w * u | x * y * z = v * w. [para(9(a,1),58(a,2))]. given #747 (F,wt=21): 2495 (F @ G) * D * (C @ (B @ A)) * G != D * G * (F @ G) # answer(A). [back_demod(1631),demod(2366(9))]. given #748 (F,wt=21): 2496 (F @ G) * D * C * (C @ (B @ A)) != D * (F @ G) * C # answer(A). [back_demod(1630),demod(2366(10))]. given #749 (T,wt=15): 2587 x * y * z * z @ (z @ x * y) = c_0. [back_demod(1032),demod(2366(6))]. given #750 (T,wt=15): 2691 x * y * y * x @ y = x * x @ y. [back_demod(693),demod(2672(7))]. given #751 (A,wt=22): 491 x * y * (y @ z) != u * v * y * z | u * v * z = x. [para(10(a,1),58(a,1,2,2)),flip(a)]. given #752 (F,wt=21): 2505 (C @ (B @ A)) * (F @ G) * D * G * (G @ F) != D * G # answer(A). [back_demod(1540),demod(2366(5))]. given #753 (F,wt=21): 2508 (F @ G) * D * (C @ (B @ A)) * G * (G @ F) != D * G # answer(A). [back_demod(1508),demod(2366(9))]. given #754 (T,wt=15): 2848 (x @ (y @ z)) * (x @ (z @ y)) * u = u. [para(2366(a,1),1191(a,1,1))]. given #755 (T,wt=15): 2849 ((x @ y) @ z) * ((y @ x) @ z) * u = u. [para(2366(a,2),1191(a,1,1))]. given #756 (A,wt=18): 492 x * (y @ z) != u * y * z | u * z * y = x. [para(10(a,1),58(a,1,2)),flip(a)]. given #757 (F,wt=17): 8842 (C @ (B @ A)) * G * F * D != G * F * D # answer(A). [ur(492,b,7636,a(flip)),demod(9(15),9(14),9(13),10(13))]. given #758 (F,wt=17): 8843 (C @ (A @ B)) * G * F * D != G * F * D # answer(A). [ur(492,b,7625,a(flip)),demod(9(15),9(14),9(13),10(13))]. given #759 (T,wt=15): 2897 (x @ (y @ z)) @ u = u @ (x @ (z @ y)). [para(2366(a,1),2366(a,1,1))]. given #760 (T,wt=15): 2898 ((x @ y) @ z) @ u = u @ ((y @ x) @ z). [para(2366(a,2),2366(a,1,1))]. given #761 (A,wt=22): 493 x * y * z * u * (u @ v) != u * v | x * y * z = v. [para(10(a,1),58(a,2))]. given #762 (F,wt=17): 8844 (C @ (B @ A)) * F * D * G != F * D * G # answer(A). [ur(492,b,7412,a(flip)),demod(9(15),9(14),9(13),10(13))]. given #763 (F,wt=17): 8845 (C @ (A @ B)) * F * D * G != F * D * G # answer(A). [ur(492,b,7400,a(flip)),demod(9(15),9(14),9(13),10(13))]. given #764 (T,wt=15): 2899 (x @ y) @ (z @ u) = (y @ x) @ (u @ z). [para(2366(a,2),2366(a,1))]. given #765 (T,wt=15): 2915 (x @ (y @ z)) @ (u @ (x @ (z @ y))) = c_0. [para(2366(a,1),2842(a,1,1))]. given #766 (A,wt=22): 494 x * y * z * y * x != u * x * y | y * x * z = u. [para(11(a,1),58(a,1))]. given #767 (F,wt=17): 8846 (C @ (B @ A)) * D * G * F != D * G * F # answer(A). [ur(492,b,7392,a(flip)),demod(9(15),9(14),9(13),10(13))]. given #768 (F,wt=17): 8847 (C @ (A @ B)) * D * G * F != D * G * F # answer(A). [ur(492,b,7384,a(flip)),demod(9(15),9(14),9(13),10(13))]. given #769 (T,wt=15): 2916 ((x @ y) @ z) @ (u @ ((y @ x) @ z)) = c_0. [para(2366(a,2),2842(a,1,1))]. given #770 (T,wt=15): 2928 (x @ (y @ z)) @ ((x @ (z @ y)) @ u) = c_0. [para(2366(a,1),2850(a,1,1))]. given #771 (A,wt=22): 495 x * (y @ z) * u != v * y * z * u | v * z * y = x. [para(19(a,1),58(a,1,2)),flip(a)]. given #772 (F,wt=17): 8848 C * (D @ (F @ G)) * B * A != C * B * A # answer(A). [ur(492,b,6589,a(flip)),demod(9(15),9(14),9(13),10(13))]. given #773 (F,wt=17): 8849 (D @ (G @ F)) * B * A * C != B * A * C # answer(A). [ur(492,b,5195,a(flip)),demod(9(15),9(14),9(13),10(13))]. given #774 (T,wt=15): 2929 ((x @ y) @ z) @ (((y @ x) @ z) @ u) = c_0. [para(2366(a,2),2850(a,1,1))]. given #775 (T,wt=15): 2977 x * y * x @ x * (x @ y) = y @ x. [para(2304(a,1),2326(a,1,2,2)),demod(2350(7))]. given #776 (A,wt=20): 496 x * (y @ z * u) != y * z * u | z * u * y = x. [para(20(a,1),58(a,1)),flip(a)]. given #777 (F,wt=17): 8850 (D @ (F @ G)) * B * A * C != B * A * C # answer(A). [ur(492,b,5178,a(flip)),demod(9(15),9(14),9(13),10(13))]. given #778 (F,wt=17): 8851 (D @ (G @ F)) * A * C * B != A * C * B # answer(A). [ur(492,b,5035,a(flip)),demod(9(15),9(14),9(13),10(13))]. given #779 (T,wt=15): 2989 (x @ y) @ y * x * x * (y @ x) = c_0. [para(2304(a,1),2330(a,1,1)),demod(2350(4),9(5))]. given #780 (T,wt=15): 3010 x * (x @ y) @ x * y * x = x @ y. [para(2304(a,1),2346(a,1,1,2)),demod(2304(7))]. given #781 (A,wt=24): 497 x * y * (z * y @ u) != v * z * y * u | v * u * z = x. [para(21(a,1),58(a,1,2)),flip(a)]. given #782 (F,wt=17): 8852 (D @ (F @ G)) * A * C * B != A * C * B # answer(A). [ur(492,b,5019,a(flip)),demod(9(15),9(14),9(13),10(13))]. given #783 (F,wt=17): 8853 (D @ (G @ F)) * C * B * A != C * B * A # answer(A). [ur(492,b,5006,a(flip)),demod(9(15),9(14),9(13),10(13))]. given #784 (T,wt=15): 3037 (x @ y) @ z * (y @ x) = (x @ y) @ z. [para(1154(a,1),2349(a,1,2,2)),demod(197(3)),flip(a)]. given #785 (T,wt=15): 3100 x * y * y @ y * (y @ x) = x @ y. [para(2304(a,1),2390(a,1,2,2)),demod(9(2),2350(7))]. given #786 (A,wt=20): 498 x * (y * z @ u) != y * z * u | u * y * z = x. [para(21(a,1),58(a,1)),flip(a)]. given #787 (F,wt=17): 8854 (D @ (F @ G)) * C * B * A != C * B * A # answer(A). [ur(492,b,4711,a(flip)),demod(9(15),9(14),9(13),10(13))]. given #788 (F,wt=19): 9364 (D @ (G @ F)) * x * D != x * (C @ (A @ B)) * D # answer(A). [ur(496,b,2464,a),demod(5306(16),197(10)),flip(a)]. given #789 (T,wt=15): 3128 x * (x @ y) @ y * x * x = x @ y. [para(2304(a,1),2391(a,1,1,2)),demod(9(4),2304(7))]. given #790 (T,wt=15): 3237 x * y * y * y * y @ (x @ y) = c_0. [para(2350(a,1),2675(a,1,2)),demod(9(4))]. given #791 (A,wt=22): 499 x * y * z * u != v * u * z | x * y * (z @ u) = v. [para(402(a,1),58(a,1,2,2))]. ============================== PROOF ================================= % Proof 1 at 4.79 (+ 0.05) seconds: A. % Length of proof is 103. % Level of proof is 31. % Maximum clause weight is 23. % Given clauses 791. 7 x * y != x * z | y = z. [input]. 8 x * y != z * y | x = z. [input]. 9 (x * y) * z = x * y * z. [input]. 10 x * y * (y @ x) = y * x. [input]. 11 x * y * z * y * x = y * x * z * x * y. [input]. 12 (A @ B) @ C != D @ (F @ G) # answer(A). [input]. 13 x * y * z != x * y * u | z = u. [para(9(a,1),7(a,1)),demod(9(4))]. 14 x * y * z != u * z | x * y = u. [para(9(a,1),8(a,1))]. 15 x * (x @ x) = x. [hyper(7,a,10,a)]. 16 x * y != z * x | z * (z @ x) = y. [para(10(a,1),7(a,1)),flip(a)]. 17 x * y * (y @ z) != y * z | z = x. [para(10(a,1),8(a,1)),flip(a)]. 19 x * y * (y @ x) * z = y * x * z. [para(10(a,1),9(a,1,1)),demod(9(2),9(5)),flip(a)]. 20 x * y * z * (z @ x * y) = z * x * y. [para(10(a,1),9(a,1)),flip(a)]. 29 ((A @ B) @ C) * x != (D @ (F @ G)) * x # answer(A). [ur(8,b,12,a)]. 35 x * y != x | x @ x = y. [para(15(a,1),7(a,1)),flip(a)]. 38 x * (x @ x) * y = x * y. [para(15(a,1),9(a,1,1)),flip(a)]. 49 x * y * z != x * u * y | u * (u @ y) = z. [para(10(a,1),13(a,1,2)),flip(a)]. 51 x * y * z * y * x != y * x * u | z * x * y = u. [para(11(a,1),13(a,1))]. 58 x * y * z * u != v * u | x * y * z = v. [para(9(a,1),14(a,1,2))]. 59 x * y * z != u * v * z | x * y = u * v. [para(9(a,1),14(a,2))]. 71 (x @ x) * y = y. [hyper(13,a,38,a)]. 79 x * y != y | z @ z = x. [para(71(a,1),8(a,1)),flip(a)]. 80 x * ((y @ y) @ x) = x. [para(71(a,1),10(a,1,2)),demod(71(5))]. 87 x * y * (x * y @ x) = y * x. [hyper(16,a,9,a(flip)),demod(9(4))]. 88 x * y * z != u * x * y | u * (u @ x * y) = z. [para(9(a,1),16(a,1))]. 98 (x @ x) @ y = y @ y. [hyper(35,a,80,a),flip(a)]. 106 x * y * z != x * y | (u @ u) @ y = z. [para(80(a,1),13(a,1,2)),flip(a)]. 127 ((x @ x) @ y) * z = z. [para(98(a,2),71(a,1,1))]. 128 x * (((y @ y) @ z) @ x) = x. [para(98(a,2),80(a,1,2,1))]. 137 x * (x @ ((y @ y) @ z)) = x * ((y @ y) @ z). [hyper(16,a,127,a)]. 143 x * y != x | ((z @ z) @ u) @ x = y. [para(127(a,1),16(a,2)),demod(127(8))]. 146 x * (x @ y) != x * y | (z @ z) @ u = y. [para(127(a,1),17(a,1)),flip(b)]. 147 (((x @ x) @ y) @ z) * u = u. [para(98(a,2),127(a,1,1,1))]. 149 x * y * z != y * u | x * (x @ y) * z = u. [para(19(a,1),7(a,1))]. 154 x * y * z * (z @ (x @ y)) = y * x * z * (x @ y). [para(10(a,1),19(a,1,2,2)),flip(a)]. 172 (x @ x) @ y = z @ z. [hyper(79,a,127,a),flip(a)]. 173 x @ x = y @ y. [hyper(79,a,71,a)]. 177 x @ x = c_0. [new_symbol(173)]. 181 c_0 @ x = c_0. [back_demod(172),demod(177(1),177(3))]. 187 c_0 * x = x. [back_demod(147),demod(177(1),181(2),181(2))]. 188 x * (x @ y) != x * y | c_0 = y. [back_demod(146),demod(177(5),181(6))]. 190 x * y != x | c_0 = y. [back_demod(143),demod(177(3),181(4),181(4))]. 194 x * (x @ c_0) = x * c_0. [back_demod(137),demod(177(1),181(2),177(4),181(5))]. 197 x * c_0 = x. [back_demod(128),demod(177(1),181(2),181(2))]. 200 x * y * z != x * y | c_0 = z. [back_demod(106),demod(177(5),181(6))]. 202 x * (x @ c_0) = x. [back_demod(194),demod(197(5))]. 203 x * y * (y @ y * x) = y * x. [hyper(7,a,20,a)]. 252 x @ c_0 = c_0. [hyper(190,a,202,a),flip(a)]. 305 x * y != y * x | x @ y = c_0. [para(10(a,1),200(a,1)),flip(b)]. 328 x * (y * x @ y) = x * (x @ y). [hyper(16,a,87,a),flip(a)]. 358 x * (x @ x * y) = x * (x @ y). [hyper(16,a,203,a),flip(a)]. 378 x * y != x * z | z = y. [para(187(a,1),49(a,1,2)),demod(197(3),252(5),197(5))]. 391 x * y @ x = y @ x. [hyper(378,a,328,a),flip(a)]. 402 (x @ y) * y * x = x * y. [hyper(51,a,19,a)]. 403 (x @ y) * z * y * x = z * x * y. [hyper(51,a,19,a(flip)),flip(a)]. 407 x * (x @ y) @ y = x * y @ y. [para(10(a,1),391(a,1,1)),flip(a)]. 426 ((A @ B) @ C) * (F @ G) * D != D * (F @ G) # answer(A). [para(402(a,1),29(a,2))]. 465 y * x @ (x @ y) = c_0. [para(402(a,1),305(a,2)),demod(9(3),10(3)),xx(a)]. 477 x * y @ (x @ y) = c_0. [para(402(a,1),391(a,1,1)),demod(465(6))]. 499 x * y * z * u != v * u * z | x * y * (z @ u) = v. [para(402(a,1),58(a,1,2,2))]. 504 ((A @ B) @ C) * (F @ G) * D * x != D * (F @ G) * x # answer(A). [ur(58,b,426,a),demod(9(18))]. 516 x * y @ (y @ x * (x @ y)) = c_0. [para(10(a,1),477(a,1,1))]. 534 (x @ y * x) * y * x = x * y. [hyper(59,a,402,a)]. 722 x @ x * y = x @ y. [hyper(378,a,358,a),flip(a)]. 740 x * (x @ y * x) = (x @ y) * x. [hyper(88,a,19,a)]. 751 x @ y * (y @ x) = x @ y * x. [para(10(a,1),722(a,1,2)),flip(a)]. 778 x * y @ (y @ x * y) = c_0. [back_demod(516),demod(751(4))]. 855 x * (y @ x) * y = y * x. [para(778(a,1),10(a,1,2,2)),demod(197(5),534(4),9(5),740(4)),flip(a)]. 914 (x @ y) * x = x * (x @ y). [hyper(16,a,855,a),flip(a)]. 959 x * (x @ y * x) = x * (x @ y). [back_demod(740),demod(914(5))]. 967 x * (x @ y) * (y @ x) = x. [hyper(149,a,10,a)]. 1154 (x @ y) * (y @ x) = c_0. [hyper(190,a,967,a),flip(a)]. 1155 (x @ y) * (y @ x) * x = (y @ x) * x * (x @ y). [para(967(a,1),11(a,1,2,2)),demod(914(3),1154(9),197(8)),flip(a)]. 1191 (x @ y) * (y @ x) * z = z. [para(1154(a,1),9(a,1,1)),demod(187(2)),flip(a)]. 1239 ((A @ B) @ C) * (F @ G) * D * (G @ F) != D # answer(A). [para(1154(a,1),504(a,2,2)),demod(197(18))]. 1254 (x @ y) * y * (y @ x) = y. [back_demod(1155),demod(1191(4)),flip(a)]. 1388 (x @ y) * z @ (y @ x) = z @ (y @ x). [para(1191(a,1),391(a,1,1)),flip(a)]. 1409 (x @ y) @ (y @ x) * z = (x @ y) @ z. [para(1191(a,1),722(a,1,2)),flip(a)]. 1523 x * (x @ y) @ (y @ x) = c_0. [para(1254(a,1),305(a,2)),demod(9(4),1154(3),197(2)),xx(a)]. 1532 x @ (y @ x) = c_0. [para(1254(a,1),391(a,1,1)),demod(1523(6))]. 1841 x * (x @ y) @ y * (y @ x) = y * x @ y * (y @ x). [para(10(a,1),407(a,2,1)),demod(751(3),959(3))]. 1849 x * (x @ y) @ x * y = x * x * y @ x * y. [para(722(a,1),407(a,1,1,2))]. 2155 x * y @ x * (x @ y) = x * y @ x * x * y. [para(722(a,1),751(a,1,2,2))]. 2175 x * x * y @ x * y = y * x @ y * y * x. [para(751(a,1),751(a,1,2,2)),demod(959(5),1841(5),2155(4),10(9),1849(8)),flip(a)]. 2304 x @ y * x = x @ y. [hyper(378,a,959,a),flip(a)]. 2323 x * x * y @ x * y = x @ y. [back_demod(2175),demod(2304(8),391(6))]. 2326 x * y @ x * (x @ y) = y @ x. [back_demod(2155),demod(2304(8),391(6))]. 2346 x * (x @ y) @ x * y = x @ y. [back_demod(1849),demod(2323(8))]. 2349 x @ y * z * x = x @ y * z. [para(9(a,1),2304(a,1,2))]. 2350 x * y @ y = x @ y. [para(10(a,1),2304(a,1,2)),demod(2346(4),407(4)),flip(a)]. 2366 (x @ y) @ z = z @ (y @ x). [para(1191(a,1),2304(a,1,2)),demod(2350(3),1388(6))]. 2557 (C @ (B @ A)) * (F @ G) * D * (G @ F) != D # answer(A). [back_demod(1239),demod(2366(5))]. 2850 (x @ y) @ ((y @ x) @ z) = c_0. [para(2366(a,2),1532(a,1,2))]. 2925 x * ((y @ z) @ x) = (y @ z) * x * (z @ y). [para(2850(a,1),154(a,1,2,2,2)),demod(197(4),1191(10)),flip(a)]. 3015 x * y @ y * y * x = x @ y. [para(2326(a,1),2346(a,1,1,2)),demod(9(3),10(3),9(5),10(4),2326(8))]. 3537 (x @ y) @ z = z @ (y @ x) * z * (y @ x) * z * (x @ y). [para(1191(a,1),3015(a,1,1)),demod(9(6),9(7),1409(12)),flip(a)]. 4676 x * z * y @ (y @ z) = c_0. [para(403(a,1),305(a,2)),demod(9(4),9(3),10(3)),xx(a)]. 5124 x * y @ ((z @ u) @ y) = c_0. [para(1191(a,1),4676(a,1,1,2)),demod(2366(5,R),722(5))]. 5343 x * (y @ z) * u * (z @ y) != x * u | (y @ z) @ u = c_0. [para(5124(a,1),188(a,1,2)),demod(197(3),9(5),2925(4)),flip(a),flip(b)]. 9571 (x @ y) * z * (y @ x) = z. [hyper(499,a,403,a)]. 9617 (z @ u) @ y = c_0. [back_demod(5343),demod(9571(4)),xx(a)]. 9657 x @ (y @ z) = c_0. [back_demod(3537),demod(9617(2),9571(6),2349(5),2304(4)),flip(a)]. 9660 $F # answer(A). [back_demod(2557),demod(9657(5),9571(10),187(3)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=791. Generated=157985. Kept=9653. proofs=1. Usable=600. Sos=6823. Demods=3113. Denials=0. 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=3503477. 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.96. User_CPU=4.79, System_CPU=0.05, Wall_clock=4. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13125 exit (max_proofs) Mon Jun 19 16:41:39 2006