============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13113 was started by mccune on cleo.thornwood, Mon Jun 19 16:41:24 2006 The command was "/home/mccune/bin/prover9 -f gt.in AE.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file gt.in op(450,infix,@). op(400,infix_right,*). assign(eq_defs,fold). assign(max_weight,25). clauses(sos). (x * y) * z = x * y * z. e * x = x. x ' * x = e. x @ y = x ' * y ' * x * y. end_of_list. % Reading from file AE.in clauses(sos). (x @ y) @ z = u @ (v @ w). end_of_list. clauses(sos). A * B * C * B * A != B * A * C * A * B # answer(E). end_of_list. ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 (x * y) * z = x * y * z. [input]. 2 e * x = x. [input]. 3 x ' * x = e. [input]. 4 x @ y = x ' * y ' * x * y. [input]. 5 (x @ y) @ z = u @ (v @ w). [input]. 6 A * B * C * B * A != B * A * C * A * B # answer(E). [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([ e, A, B, C, *, @, ' ]). After inverse_order: Function symbol precedence: lex([ e, A, B, C, *, ', @ ]). Folding symbols: @/2. After fold_eq: Function symbol precedence: lex([ e, A, B, C, @, *, ' ]). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). 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) * z = x * y * z. [input]. 8 e * x = x. [input]. 9 x ' * x = e. [input]. 10 x ' * y ' * x * y = x @ y. [copy(4),flip(a)]. 11 (x @ y) @ z = u @ (v @ w). [input]. 12 A * B * C * B * A != B * A * C * A * B # answer(E). [input]. end_of_list. clauses(demodulators). 7 (x * y) * z = x * y * z. [input]. 8 e * x = x. [input]. 9 x ' * x = e. [input]. 10 x ' * y ' * x * y = x @ y. [copy(4),flip(a)]. end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=11): 7 (x * y) * z = x * y * z. [input]. given #2 (I,wt=5): 8 e * x = x. [input]. given #3 (I,wt=6): 9 x ' * x = e. [input]. given #4 (I,wt=13): 10 x ' * y ' * x * y = x @ y. [copy(4),flip(a)]. given #5 (I,wt=11): 11 (x @ y) @ z = u @ (v @ w). [input]. given #6 (I,wt=19): 12 A * B * C * B * A != B * A * C * A * B # answer(E). [input]. given #7 (F,wt=5): 16 e @ x = e. [para(8(a,1),10(a,1,2,2)),demod(9(4),9(4)),flip(a)]. given #8 (F,wt=5): 24 x @ e = e. [back_demod(22),demod(23(2)),flip(a)]. given #9 (T,wt=6): 17 x ' @ x = e. [para(9(a,1),10(a,1,2,2)),demod(13(6)),flip(a)]. given #10 (T,wt=7): 21 x @ (y @ z) = e. [para(16(a,1),11(a,1,1)),demod(16(2)),flip(a)]. given #11 (A,wt=8): 13 x ' * x * y = y. [para(9(a,1),7(a,1,1)),demod(8(2)),flip(a)]. given #12 (F,wt=5): 29 x @ x = e. [para(13(a,1),10(a,1,2)),demod(9(2)),flip(a)]. given #13 (F,wt=5): 34 x * e = x. [back_demod(27),demod(31(4))]. given #14 (T,wt=4): 36 e ' = e. [para(34(a,1),9(a,1))]. given #15 (T,wt=7): 23 (x @ y) @ z = e. [para(16(a,1),11(a,2))]. given #16 (A,wt=17): 14 x ' * y ' * x * y * z = (x @ y) * z. [para(10(a,1),7(a,1,1)),demod(7(7),7(6)),flip(a)]. given #17 (F,wt=9): 31 x ' ' * y = x * y. [para(13(a,1),13(a,1,2))]. given #18 (F,wt=5): 60 x ' ' = x. [para(31(a,1),34(a,1)),demod(34(2)),flip(a)]. given #19 (T,wt=6): 55 x * x ' = e. [para(31(a,1),9(a,1))]. given #20 (T,wt=6): 63 x @ x ' = e. [para(60(a,1),17(a,1,1))]. given #21 (A,wt=19): 15 (x * y) ' * z ' * x * y * z = x * y @ z. [para(7(a,1),10(a,1,2,2))]. given #22 (F,wt=7): 79 x * x @ x = e. [para(15(a,1),15(a,1,2)),demod(9(2),36(2),8(4),9(4),16(5))]. given #23 (F,wt=8): 59 x * x ' * y = y. [para(31(a,1),13(a,1))]. given #24 (T,wt=10): 64 x * y * (x * y) ' = e. [para(55(a,1),7(a,1)),flip(a)]. given #25 (T,wt=9): 88 x * (y * x) ' = y '. [para(64(a,1),13(a,1,2)),demod(34(3)),flip(a)]. given #26 (A,wt=12): 32 x ' * y * x = y * (y @ x). [back_demod(30),demod(31(4)),flip(a)]. given #27 (F,wt=8): 99 (x @ y) ' = y @ x. [para(14(a,2),88(a,1,2,1)),demod(98(7),98(5),98(3),98(2),7(5),60(7),7(6),7(5),60(8),7(7),7(6),7(5),10(6),59(4)),flip(a)]. given #28 (F,wt=9): 105 (x @ y) * (y @ x) = e. [back_demod(90),demod(98(8),98(6),98(4),98(3),7(6),60(8),7(7),7(6),60(9),7(8),7(7),7(6),10(7),59(5))]. given #29 (T,wt=9): 109 x * y @ x = y @ x. [back_demod(73),demod(98(2),7(5),10(5)),flip(a)]. given #30 (T,wt=9): 144 x @ y * x = x @ y. [back_demod(128),demod(137(4)),flip(a)]. given #31 (A,wt=21): 37 x * y ' * z ' * y * z * u = x * (y @ z) * u. [para(14(a,1),7(a,2,2)),demod(7(7))]. given #32 (F,wt=8): 162 x ' @ y = y @ x. [back_demod(158),demod(161(3))]. given #33 (F,wt=8): 163 x @ y ' = y @ x. [back_demod(155),demod(161(2)),flip(a)]. given #34 (T,wt=9): 153 x @ x * y = x @ y. [para(109(a,1),99(a,1,1)),demod(99(2)),flip(a)]. given #35 (T,wt=9): 161 x * y @ y = x @ y. [para(144(a,1),99(a,1,1)),demod(99(2)),flip(a)]. given #36 (A,wt=13): 40 x ' * y * x = (x @ y ') * y. [para(9(a,1),14(a,1,2,2,2)),demod(34(5),31(4))]. given #37 (F,wt=9): 183 x ' @ y ' = x @ y. [para(162(a,2),162(a,1))]. given #38 (F,wt=9): 195 x ' @ y = x @ y '. [para(163(a,1),162(a,1)),flip(a)]. given #39 (T,wt=10): 98 (x * y) ' = y ' * x '. [para(88(a,1),13(a,1,2)),flip(a)]. given #40 (T,wt=10): 127 x * y @ y ' = y @ x. [back_demod(78),demod(109(5))]. given #41 (A,wt=22): 43 x ' * y * x * (y @ z) = (x @ y ') * z ' * y * z. [para(10(a,1),14(a,1,2,2,2)),demod(31(6))]. given #42 (F,wt=10): 131 x ' @ y * x = y @ x. [para(32(a,1),10(a,1,2,2)),demod(60(2),98(2),7(6),13(5),59(4)),flip(a)]. given #43 (F,wt=10): 150 x ' * y @ x = y @ x. [para(59(a,1),109(a,1,1)),flip(a)]. given #44 (T,wt=10): 152 x ' * y * x @ y = e. [para(32(a,2),109(a,1,1)),demod(23(6))]. given #45 (T,wt=10): 177 (x @ y) * (x @ y ') = e. [para(162(a,1),105(a,1,1))]. given #46 (A,wt=12): 45 (x ' @ y) * x = x * (y @ x). [para(10(a,1),14(a,1,2)),demod(31(4)),flip(a)]. given #47 (F,wt=10): 178 (x @ y ') * (x @ y) = e. [para(162(a,1),105(a,1,2))]. given #48 (F,wt=10): 179 (x ' @ y) * (x @ y) = e. [para(162(a,2),105(a,1,1))]. given #49 (T,wt=10): 180 (x @ y) * (x ' @ y) = e. [para(162(a,2),105(a,1,2))]. given #50 (T,wt=10): 200 x @ y ' * x * y = e. [para(32(a,2),153(a,1,2)),demod(21(6))]. given #51 (A,wt=16): 47 x ' * y * x * z = y * (y @ x) * z. [para(14(a,1),13(a,1,2)),demod(31(5)),flip(a)]. given #52 (F,wt=10): 290 x * y * x ' @ y = e. [para(60(a,1),152(a,1,1,1))]. given #53 (F,wt=10): 329 x @ y * x * y ' = e. [para(60(a,1),200(a,1,2,1))]. given #54 (T,wt=11): 116 x ' @ x * y = x ' @ y. [back_demod(33),demod(98(2),7(4),58(5)),flip(a)]. given #55 (T,wt=11): 126 x * y ' @ y = y ' @ x. [back_demod(80),demod(109(6))]. given #56 (A,wt=17): 49 x ' * y * x * z = (x @ y ') * y * z. [para(13(a,1),14(a,1,2,2,2)),demod(31(5))]. given #57 (F,wt=11): 134 (x @ y) * z * (y @ x) = z. [para(21(a,1),32(a,2,2)),demod(99(2),34(6))]. given #58 (F,wt=11): 135 x * y * (y @ x) = y * x. [para(32(a,1),13(a,1,2)),demod(60(2))]. given #59 (T,wt=11): 145 (x @ y) * (y @ x) * z = z. [para(99(a,1),13(a,1,1))]. given #60 (T,wt=11): 147 x ' * y * x @ y ' = e. [para(10(a,1),109(a,1,1)),demod(23(3)),flip(a)]. given #61 (A,wt=16): 52 (x ' @ y) * x * z = x * (y @ x) * z. [para(14(a,1),14(a,1,2)),demod(31(5)),flip(a)]. given #62 (F,wt=11): 148 x * y @ x ' = y @ x '. [para(13(a,1),109(a,1,1)),flip(a)]. given #63 (F,wt=11): 191 x @ x ' * y = y @ x '. [para(163(a,1),109(a,1))]. given #64 (T,wt=11): 197 x ' @ y ' * x * y = e. [para(10(a,1),153(a,1,2)),demod(21(3)),flip(a)]. given #65 (T,wt=11): 208 x @ y * x ' = y @ x '. [para(161(a,1),163(a,1)),flip(a)]. given #66 (A,wt=14): 57 x ' * y * x * y ' = x @ y '. [para(31(a,1),10(a,1,2))]. given #67 (F,wt=11): 229 (x @ y ') * (y @ x ') = e. [para(195(a,1),105(a,1,1))]. given #68 (F,wt=11): 230 (x ' @ y) * (y ' @ x) = e. [para(195(a,2),105(a,1,1))]. given #69 (T,wt=11): 234 x * y @ y ' * x ' = e. [para(98(a,1),63(a,1,2))]. given #70 (T,wt=11): 282 x * (x @ y) @ y = x @ y. [para(32(a,1),150(a,1,1)),demod(161(5))]. given #71 (A,wt=14): 58 x * y ' * x ' * y = x ' @ y. [para(31(a,1),10(a,1))]. given #72 (F,wt=11): 283 x ' * y ' * x @ y = e. [para(32(a,2),150(a,1,1)),demod(23(8))]. given #73 (F,wt=11): 293 x @ y ' * x ' * y = e. [para(152(a,1),163(a,1)),flip(a)]. given #74 (T,wt=11): 360 (x @ y) * z = z * (x @ y). [para(105(a,1),47(a,1,2,2)),demod(99(2),34(3),21(4),8(5))]. given #75 (T,wt=11): 415 x @ y * x ' * y ' = e. [para(290(a,1),163(a,1)),flip(a)]. given #76 (A,wt=18): 61 x ' * y * x * y ' * z = (x @ y ') * z. [para(31(a,1),14(a,1,2))]. given #77 (F,wt=11): 420 x * y * x ' @ y ' = e. [para(290(a,1),177(a,1,1)),demod(8(7))]. given #78 (F,wt=11): 421 x * y ' * x ' @ y = e. [para(290(a,1),177(a,1,2)),demod(34(7))]. given #79 (T,wt=11): 431 x @ y * (y @ x) = x @ y. [para(32(a,1),116(a,1,2)),demod(60(2),60(5),144(5))]. given #80 (T,wt=11): 443 (x @ y) * y * x = x * y. [para(9(a,1),49(a,1,2,2)),demod(60(2),34(2),183(4)),flip(a)]. given #81 (A,wt=18): 62 (x ' @ y) * z = x * y ' * x ' * y * z. [para(31(a,1),14(a,1)),flip(a)]. given #82 (F,wt=9): 786 x * y @ y * x = e. [para(443(a,1),144(a,1,2)),demod(21(6))]. given #83 (F,wt=11): 535 x @ (y @ x) * z = x @ z. [para(52(a,2),10(a,1,2,2)),demod(98(4),99(4),7(9),322(8),10(5)),flip(a)]. given #84 (T,wt=11): 622 x * y ' @ y * x ' = e. [para(60(a,1),234(a,1,2,1))]. given #85 (T,wt=11): 623 x ' * y @ y ' * x = e. [para(60(a,1),234(a,1,2,2))]. given #86 (A,wt=14): 65 x ' * y ' * x = (x @ y) * y '. [para(55(a,1),14(a,1,2,2,2)),demod(34(4))]. given #87 (F,wt=11): 626 x ' * y ' @ y * x = e. [para(234(a,1),99(a,1,1)),demod(36(2)),flip(a)]. given #88 (F,wt=11): 752 x ' * y ' @ x * y = e. [back_demod(111),demod(747(12))]. given #89 (T,wt=11): 791 x * y @ x ' * y ' = e. [para(443(a,1),127(a,1,1)),demod(98(3),21(8))]. given #90 (T,wt=11): 892 x @ (x @ y) * z = x @ z. [para(59(a,1),535(a,1,2)),demod(99(3)),flip(a)]. given #91 (A,wt=18): 71 x ' * y * z * x = y * z * (y * z @ x). [para(15(a,1),13(a,1,2)),demod(60(3),7(4)),flip(a)]. given #92 (F,wt=11): 893 (x @ y) * z @ y = z @ y. [para(535(a,1),99(a,1,1)),demod(99(2)),flip(a)]. given #93 (F,wt=11): 911 x @ y * (x @ z) = x @ y. [para(134(a,1),535(a,1,2)),flip(a)]. given #94 (T,wt=11): 912 x @ y * (z @ x) = x @ y. [para(135(a,1),535(a,1,2)),demod(21(5),34(5))]. given #95 (T,wt=11): 1012 x * y ' @ x ' * y = e. [para(60(a,1),752(a,1,1,1))]. given #96 (A,wt=21): 76 x ' * y ' * x * y * z @ u = (x @ y) * z @ u. [para(14(a,2),15(a,2,1)),demod(15(9)),flip(a)]. given #97 (F,wt=11): 1013 x ' * y @ x * y ' = e. [para(60(a,1),752(a,1,1,2))]. given #98 (F,wt=11): 1246 (x @ y) * z @ u = z @ u. [para(76(a,1),10(a,2)),demod(98(7),98(5),98(3),98(2),7(5),60(7),7(6),7(5),60(8),7(7),7(6),7(5),10(6),7(11),7(10),7(9),7(8),7(13),351(12),10(5)),flip(a)]. given #99 (T,wt=11): 1258 x @ (y @ z) * u = x @ u. [para(76(a,2),99(a,1,1)),demod(1251(7),13(3),99(2)),flip(a)]. given #100 (T,wt=11): 1260 x @ y * (z @ u) = x @ y. [para(76(a,2),144(a,1)),demod(1251(10),13(3),154(4),1246(6))]. given #101 (A,wt=18): 83 x ' * y ' * x * z = (x @ y) * y ' * z. [para(59(a,1),14(a,1,2,2,2))]. given #102 (F,wt=11): 1276 x * (y @ z) @ u = x @ u. [para(134(a,1),76(a,1,1,2,2,2)),demod(99(3),345(5),1246(3),21(3),8(5)),flip(a)]. given #103 (F,wt=11): 1365 x * y @ z = y * x @ z. [para(443(a,1),1246(a,1,1))]. given #104 (T,wt=11): 1372 x @ y * z = x @ z * y. [para(443(a,1),1258(a,1,2))]. given #105 (T,wt=12): 137 x ' * (y @ z) * x = y @ z. [para(23(a,1),32(a,2,2)),demod(34(7))]. given #106 (A,wt=24): 101 x ' * y ' * z * x * y * z ' = y * x @ x ' * z '. [para(88(a,1),15(a,1,2,2,2)),demod(98(2),98(5),98(7),60(5),60(5),7(7),7(8),98(11))]. given #107 (F,wt=12): 143 (x @ y) * x ' * y * x = y. [para(32(a,2),32(a,1,2)),demod(99(2),21(7),34(7))]. given #108 (F,wt=12): 189 x * (y @ x) = y * x * y '. [para(163(a,1),32(a,2,2)),demod(60(2)),flip(a)]. given #109 (T,wt=12): 213 x * (y @ x) = x * (x @ y '). [para(40(a,1),14(a,1,2,2)),demod(60(2),137(5),45(6)),flip(a)]. given #110 (T,wt=12): 299 (x @ y) * (x @ y ') * z = z. [para(177(a,1),7(a,1,1)),demod(8(2)),flip(a)]. given #111 (A,wt=15): 106 x ' * y ' = (x @ y) * y ' * x '. [back_demod(89),demod(98(3)),flip(a)]. given #112 (F,wt=12): 301 x * (y @ z ') = x * (z @ y). [para(177(a,1),37(a,1,2,2,2,2)),demod(99(3),34(4),137(4),21(4),8(6)),flip(a)]. given #113 (F,wt=12): 309 (x ' @ y) * x * y = y * x. [para(144(a,1),45(a,2,2)),demod(98(2),150(4),7(7),135(7))]. given #114 (T,wt=12): 316 (x @ y ') * (x @ y) * z = z. [para(178(a,1),7(a,1,1)),demod(8(2)),flip(a)]. given #115 (T,wt=12): 318 x * (y ' @ z) = x * (z @ y). [para(178(a,1),37(a,1,2,2,2,2)),demod(99(4),34(5),137(5),21(6),8(6))]. given #116 (A,wt=23): 107 x ' * y ' * z ' * x * y * z = y * x @ x ' * z. [back_demod(85),demod(98(2),98(6),60(6),7(7),7(8))]. given #117 (F,wt=12): 320 (x ' @ y) * (x @ y) * z = z. [para(179(a,1),7(a,1,1)),demod(8(2)),flip(a)]. given #118 (F,wt=12): 322 (x @ y) * (x ' @ y) * z = z. [para(180(a,1),7(a,1,1)),demod(8(2)),flip(a)]. given #119 (T,wt=12): 347 (x ' @ y) * z = (y @ x) * z. [para(47(a,1),14(a,1)),demod(345(6))]. given #120 (T,wt=12): 391 (x @ y) * z = z * (y @ x '). [para(177(a,1),47(a,1,2,2)),demod(99(2),34(3),21(4),8(6))]. given #121 (A,wt=21): 108 x ' * y ' * z * y * x * z ' = y * x @ z '. [back_demod(77),demod(98(2),7(8))]. given #122 (F,wt=12): 395 (x ' @ y) * z = z * (y @ x). [para(178(a,1),47(a,1,2,2)),demod(99(3),34(4),21(6),8(6))]. given #123 (F,wt=12): 397 (x @ y ') * z = z * (y @ x). [para(179(a,1),47(a,1,2,2)),demod(99(3),34(4),21(6),8(6))]. given #124 (T,wt=12): 398 (x @ y) * z = z * (y ' @ x). [para(180(a,1),47(a,1,2,2)),demod(99(2),34(3),21(4),8(6))]. given #125 (T,wt=12): 450 (x @ y ') * z = (y @ x) * z. [para(49(a,1),14(a,1,2)),demod(345(6))]. given #126 (A,wt=23): 110 x * y ' * z ' * x ' * y * z = y * x ' @ x * z. [back_demod(72),demod(98(3),60(2),98(4),7(7),7(8))]. given #127 (F,wt=12): 491 (x @ y) * z * (x @ y ') = z. [para(162(a,1),134(a,1,1))]. given #128 (F,wt=12): 492 (x @ y ') * z * (x @ y) = z. [para(162(a,1),134(a,1,2,2))]. given #129 (T,wt=12): 493 (x ' @ y) * z * (x @ y) = z. [para(162(a,2),134(a,1,1))]. given #130 (T,wt=12): 494 (x @ y) * z * (x ' @ y) = z. [para(162(a,2),134(a,1,2,2))]. given #131 (A,wt=24): 113 x ' * y ' * z ' * y * x * z * u = (y * x @ z) * u. [back_demod(39),demod(98(2),7(9))]. given #132 (F,wt=12): 506 x * y * (x ' @ y) = y * x. [para(162(a,2),135(a,1,2,2))]. given #133 (F,wt=12): 508 x * y * (x @ y ') = y * x. [para(163(a,2),135(a,1,2,2))]. given #134 (T,wt=12): 697 x * (y @ z) * x ' = y @ z. [para(360(a,2),59(a,1,2))]. given #135 (T,wt=12): 789 (x @ y ') * x * y = y * x. [para(163(a,2),443(a,1,1))]. given #136 (A,wt=24): 114 x ' * y ' * z ' * x * z * y * u = (x @ z * y) * u. [back_demod(38),demod(98(3),7(8))]. given #137 (F,wt=12): 1278 x ' * y * x @ z = y @ z. [para(135(a,1),76(a,1,1,2,2,2)),demod(1251(7),1246(9),1276(7))]. given #138 (F,wt=12): 1280 x * y * x ' @ z = y @ z. [para(57(a,1),76(a,1,1,2,2,2)),demod(60(3),1251(7),1276(4),1246(8)),flip(a)]. given #139 (T,wt=12): 1341 x @ y ' * z * y = x @ z. [back_demod(1077),demod(1260(7))]. given #140 (T,wt=12): 1465 x ' @ y * z = z * y @ x. [para(1365(a,1),162(a,2))]. given #141 (A,wt=20): 117 x ' * y ' * z ' * y * x * z = y * x @ z. [back_demod(15),demod(98(2),7(8))]. given #142 (F,wt=11): 2444 x * x @ y = x @ y * y. [back_demod(1792),demod(2417(4))]. given #143 (F,wt=12): 1466 x * y @ z ' = z @ y * x. [para(1365(a,1),163(a,1))]. given #144 (T,wt=12): 1496 x @ y * z * y ' = x @ z. [para(13(a,1),1372(a,1,2)),demod(7(4)),flip(a)]. given #145 (T,wt=12): 2466 x ' @ y * y = y @ x * x. [para(2444(a,1),162(a,2))]. given #146 (A,wt=16): 130 x * y ' * z * y = x * z * (z @ y). [para(32(a,1),7(a,2,2)),demod(7(4))]. given #147 (F,wt=12): 2468 x * x @ y ' = y * y @ x. [para(2444(a,2),163(a,2))]. given #148 (F,wt=13): 141 x * (x @ y ') = y * x * y '. [para(60(a,1),32(a,1,1)),flip(a)]. given #149 (T,wt=13): 154 x @ y * z * x = x @ y * z. [para(7(a,1),144(a,1,2))]. given #150 (T,wt=13): 176 x ' * y * x = y * (x ' @ y). [para(162(a,2),32(a,2,2))]. given #151 (A,wt=15): 136 x ' * (x ' @ y) = y ' * x ' * y. [para(13(a,1),32(a,1,2)),demod(98(2),7(4),116(8)),flip(a)]. given #152 (F,wt=13): 190 x ' * y * x = y * (x @ y '). [para(163(a,2),32(a,2,2))]. given #153 (F,wt=13): 203 x * y * z @ z = x * y @ z. [para(7(a,1),161(a,1,1))]. given #154 (T,wt=13): 221 x * y * x ' * y ' = x @ y. [para(183(a,1),10(a,2)),demod(60(2),60(2))]. given #155 (T,wt=13): 228 x * (x ' @ y) = y * x * y '. [para(195(a,2),32(a,2,2)),demod(60(2)),flip(a)]. given #156 (A,wt=21): 138 x ' * y * x * z * (z @ y) = (x @ y ') * z * y. [para(32(a,1),14(a,1,2,2,2)),demod(60(3))]. given #157 (F,wt=13): 236 x ' * y ' @ z = z @ y * x. [para(98(a,1),162(a,1,1))]. given #158 (F,wt=13): 237 x * y @ z = z @ y ' * x '. [para(98(a,1),163(a,1,2)),flip(a)]. given #159 (T,wt=13): 354 x ' * y = y * (y @ x) * x '. [para(55(a,1),47(a,1,2,2)),demod(34(3))]. given #160 (T,wt=13): 479 (x ' @ y) * z = (x @ y ') * z. [para(49(a,1),47(a,1,2)),demod(345(6),345(9)),flip(a)]. given #161 (A,wt=18): 140 x ' * y ' * z ' * y * z * x = y @ z. [para(14(a,2),32(a,1,2)),demod(23(11),34(11))]. given #162 (F,wt=13): 495 (x @ y ') * z * (y @ x ') = z. [para(195(a,1),134(a,1,1))]. given #163 (F,wt=13): 496 (x ' @ y) * z * (y ' @ x) = z. [para(195(a,2),134(a,1,1))]. given #164 (T,wt=13): 505 x * y ' * (x @ y) = y ' * x. [para(162(a,1),135(a,1,2,2))]. given #165 (T,wt=13): 507 x ' * y * (x @ y) = y * x '. [para(163(a,1),135(a,1,2,2))]. given #166 (A,wt=15): 146 x * y * z @ x * y = z @ x * y. [para(7(a,1),109(a,1,1))]. given #167 (F,wt=13): 524 (x @ y ') * (y @ x ') * z = z. [para(195(a,1),145(a,1,1))]. given #168 (F,wt=13): 525 (x ' @ y) * (y ' @ x) * z = z. [para(195(a,2),145(a,1,1))]. given #169 (T,wt=13): 609 x * (y ' @ z) = x * (y @ z '). [para(229(a,1),37(a,1,2,2,2,2)),demod(99(4),34(5),137(5),21(6),8(7))]. given #170 (T,wt=13): 612 (x ' @ y) * z = z * (x @ y '). [para(229(a,1),47(a,1,2,2)),demod(99(3),34(4),21(6),8(7))]. given #171 (A,wt=25): 164 x * y * z ' * u ' * z * u * v = x * y * (z @ u) * v. [para(37(a,1),7(a,1)),demod(7(4)),flip(a)]. given #172 (F,wt=13): 617 (x @ y ') * z = z * (x ' @ y). [para(230(a,1),47(a,1,2,2)),demod(99(3),34(4),21(6),8(7))]. given #173 (F,wt=13): 701 x ' * (y @ z) = (y @ z) * x '. [para(360(a,1),98(a,1,1)),demod(98(3),99(2),99(6)),flip(a)]. given #174 (T,wt=13): 787 x ' * y = (y @ x) * y * x '. [para(162(a,1),443(a,1,1)),flip(a)]. given #175 (T,wt=13): 788 (x @ y) * x ' * y = y * x '. [para(163(a,1),443(a,1,1))]. given #176 (A,wt=21): 166 x * y ' * z * y * u = x * (y @ z ') * z * u. [para(13(a,1),37(a,1,2,2,2,2)),demod(60(3))]. given #177 (F,wt=13): 851 x * y * z @ z * x * y = e. [para(7(a,1),786(a,1,1))]. given #178 (F,wt=13): 852 x * y * z @ y * z * x = e. [para(7(a,1),786(a,1,2))]. given #179 (T,wt=13): 1315 x * y @ y * (z @ u) * x = e. [back_demod(861),demod(1251(11),13(4))]. given #180 (T,wt=13): 1323 x * y * z @ y = x * z @ y. [back_demod(386),demod(1252(4)),flip(a)]. given #181 (A,wt=22): 168 x * (y ' @ z) * u = x * y * z ' * y ' * z * u. [para(60(a,1),37(a,1,2,1)),flip(a)]. given #182 (F,wt=13): 1460 (x * y @ z) * (z @ y * x) = e. [para(1365(a,1),105(a,1,1))]. given #183 (F,wt=13): 1461 (x @ y * z) * (z * y @ x) = e. [para(1365(a,1),105(a,1,2))]. given #184 (T,wt=13): 1467 x * y @ z = z @ x ' * y '. [para(1365(a,1),163(a,2)),demod(98(2)),flip(a)]. given #185 (T,wt=13): 1502 x ' * y ' @ z = z @ x * y. [para(1372(a,1),162(a,2)),demod(98(2))]. given #186 (A,wt=22): 169 x * y ' * z * y * z ' * u = x * (y @ z ') * u. [para(60(a,1),37(a,1,2,2,1))]. given #187 (F,wt=13): 1527 x @ y * x * z = x @ y * z. [back_demod(433),demod(1525(4)),flip(a)]. given #188 (F,wt=13): 2140 (x * y @ z) * (z @ y) = x @ z. [para(135(a,1),113(a,1,2,2,2,2)),demod(140(8)),flip(a)]. given #189 (T,wt=13): 2418 (x @ y) * (y @ x * z) = y @ z. [para(47(a,2),117(a,1,2,2,2)),demod(99(2),233(9),1276(7))]. given #190 (T,wt=13): 2429 (x @ y) * (y * z @ x) = z @ x. [para(143(a,1),117(a,1,2,2,2,2)),demod(99(2),98(6),98(4),60(7),7(6),7(8),7(7),117(9),1341(10),1276(7))]. given #191 (A,wt=18): 170 x * y ' * z ' * y = x * (y @ z) * z '. [para(55(a,1),37(a,1,2,2,2,2)),demod(34(4))]. given #192 (F,wt=13): 2446 (x @ y) * (z @ y) = x * z @ y. [back_demod(1600),demod(2420(6)),flip(a)]. given #193 (F,wt=13): 2465 x ' * x ' @ y = y * y @ x. [para(2444(a,2),162(a,1))]. given #194 (T,wt=13): 2467 x @ y ' * y ' = y @ x * x. [para(2444(a,1),163(a,1))]. given #195 (T,wt=13): 2605 x ' @ y * y = x * x @ y '. [para(2466(a,2),163(a,2)),flip(a)]. given #196 (A,wt=22): 171 x * y ' * z ' * y * u = x * (y @ z) * z ' * u. [para(59(a,1),37(a,1,2,2,2,2))]. given #197 (F,wt=13): 2814 x * x @ y * x = x @ y * y. [para(154(a,1),2444(a,2)),demod(7(5),1527(6))]. given #198 (F,wt=13): 3031 x * y ' @ z = z @ y * x '. [para(60(a,1),236(a,1,1,1))]. given #199 (T,wt=13): 3032 x ' * y @ z = z @ y ' * x. [para(60(a,1),236(a,1,1,2))]. given #200 (T,wt=13): 3174 x ' * y @ z = z @ x * y '. [para(354(a,1),236(a,2,2)),demod(60(3),1525(8))]. given #201 (A,wt=25): 172 x * y ' * z * y * u * (u @ z) = x * (y @ z ') * u * z. [para(32(a,1),37(a,1,2,2,2,2)),demod(60(3))]. given #202 (F,wt=13): 3175 x * y ' @ z = z @ x ' * y. [para(354(a,2),236(a,2,2)),demod(98(4),60(2),99(2),7(4),1252(5))]. given #203 (F,wt=13): 3222 (x @ y) * (z * y @ x) = z @ x. [para(135(a,1),140(a,1,2,2,2,2)),demod(98(3),99(2),7(10),117(9))]. given #204 (T,wt=13): 3377 x * y @ y * y = x @ y * y. [para(146(a,1),2444(a,1)),demod(7(2),1527(3),7(5),7(7),7(8),7(7),196(9),2796(7)),flip(a)]. given #205 (T,wt=13): 3708 x * y * z @ y * x * z = e. [para(135(a,1),851(a,1,1,2)),demod(7(6),1525(7))]. given #206 (A,wt=17): 173 (x @ y) * z = y * x ' * y ' * x * z. [para(162(a,1),14(a,2,1)),demod(60(2)),flip(a)]. given #207 (F,wt=13): 3845 x * y * z @ z * y * x = e. [para(443(a,1),1315(a,1,2,2)),demod(7(2))]. given #208 (F,wt=13): 4228 (x @ y * z) * (y @ x) = x @ z. [para(2140(a,1),13(a,1,2)),demod(99(3))]. given #209 (T,wt=13): 4238 (x @ y) * (y @ z * x) = y @ z. [para(2140(a,1),98(a,1,1)),demod(99(2),99(3),99(5)),flip(a)]. given #210 (T,wt=13): 4313 (x @ y) * (x @ z) = x @ y * z. [para(2418(a,1),13(a,1,2)),demod(99(2))]. given #211 (A,wt=18): 174 x ' * y ' * x * y * z = (y ' @ x) * z. [para(162(a,2),14(a,2,1))]. given #212 (F,wt=13): 4886 x * x @ y * x = x * x @ y. [para(2814(a,2),10(a,2)),demod(98(3),7(7),107(8),2428(4)),flip(a)]. given #213 (F,wt=13): 4891 x * y @ x * x = y @ x * x. [para(2814(a,2),161(a,1)),demod(7(5),7(4),203(9),1468(5))]. given #214 (T,wt=13): 5382 x * x @ x * y = x * x @ y. [para(3377(a,1),2418(a,1,1)),demod(7(5),2418(7))]. given #215 (T,wt=13): 5405 x * y * z @ x * z * y = e. [para(443(a,1),3708(a,1,1,2)),demod(1258(7))]. given #216 (A,wt=14): 175 x ' * (y @ x) = y ' * x ' * y. [para(162(a,1),32(a,2,2)),flip(a)]. given #217 (F,wt=14): 202 x ' * y ' * x * (y @ x) = y '. [back_demod(133),demod(197(6),34(3)),flip(a)]. given #218 (F,wt=14): 216 x ' * (y @ x) = x ' * (x @ y '). [para(40(a,1),32(a,1,2)),demod(98(2),7(7),137(6),131(8)),flip(a)]. given #219 (T,wt=14): 223 x ' * (x @ y) = y * x ' * y '. [para(183(a,1),32(a,2,2)),demod(60(2)),flip(a)]. given #220 (T,wt=14): 240 x ' * y ' @ z = y * x @ z '. [para(98(a,1),195(a,1,1))]. given #221 (A,wt=21): 181 x * (y @ z) * u = x * z * y ' * z ' * y * u. [para(162(a,1),37(a,2,2,1)),demod(60(2)),flip(a)]. given #222 (F,wt=14): 241 x ' @ y * z = x @ z ' * y '. [para(98(a,1),195(a,2,2))]. given #223 (F,wt=14): 242 x * y * z @ z ' = z @ x * y. [para(7(a,1),127(a,1,1))]. given #224 (T,wt=14): 274 x ' @ y * z * x = y * z @ x. [para(7(a,1),131(a,1,2))]. given #225 (T,wt=14): 444 (x @ y) * y ' * x ' * y = x '. [para(9(a,1),49(a,1,2)),demod(34(3),98(3),98(5),60(3),60(3),153(3),98(4),7(6)),flip(a)]. given #226 (A,wt=22): 182 x * y ' * z ' * y * z * u = x * (z ' @ y) * u. [para(162(a,2),37(a,2,2,1))]. given #227 (F,wt=14): 454 x ' * y = (x @ y ') * y * x '. [para(55(a,1),49(a,1,2,2)),demod(34(3))]. given #228 (F,wt=14): 511 x * y ' * (y @ x ') = y ' * x. [para(195(a,1),135(a,1,2,2))]. given #229 (T,wt=14): 512 x ' * y * (y ' @ x) = y * x '. [para(195(a,2),135(a,1,2,2))]. given #230 (T,wt=14): 790 (x ' @ y) * y ' * x = x * y '. [para(195(a,2),443(a,1,1))]. given #231 (A,wt=19): 185 (x @ y) * x * y * z = x * y * (x @ y) * z. [back_demod(51),demod(183(3))]. given #232 (F,wt=14): 970 (x @ y) * x ' = y * x ' * y '. [para(162(a,1),65(a,2,1)),demod(60(2)),flip(a)]. given #233 (F,wt=14): 1063 x * y * z @ y ' = y @ x * z. [para(49(a,2),892(a,1,2)),demod(191(5))]. given #234 (T,wt=14): 1410 x ' * (y @ z ') = (z @ y) * x '. [para(177(a,1),83(a,1,2,2)),demod(99(2),34(4),23(5),8(9)),flip(a)]. given #235 (T,wt=14): 1411 x ' * (y ' @ z) = (z @ y) * x '. [para(180(a,1),83(a,1,2,2)),demod(99(2),34(4),23(5),8(9)),flip(a)]. given #236 (A,wt=17): 187 x ' * y * x * y ' * z = (y @ x) * z. [para(163(a,1),14(a,2,1)),demod(60(3))]. given #237 (F,wt=14): 1469 x ' * y ' @ z ' = x * y @ z. [para(1365(a,1),183(a,2)),demod(98(2))]. given #238 (F,wt=14): 1470 x ' * y ' @ z = x * y @ z '. [para(1365(a,1),195(a,2)),demod(98(2))]. given #239 (T,wt=14): 1504 x ' @ y ' * z ' = x @ y * z. [para(1372(a,1),183(a,2)),demod(98(3))]. given #240 (T,wt=14): 1505 x ' @ y * z = x @ y ' * z '. [para(1372(a,1),195(a,1)),demod(98(5))]. given #241 (A,wt=18): 188 x ' * y ' * x * y * z = (y @ x ') * z. [para(163(a,2),14(a,2,1))]. given #242 (F,wt=14): 1578 (x @ y) * x * y ' * x ' = y '. [para(183(a,1),143(a,1,1)),demod(60(3))]. given #243 (F,wt=14): 1680 x * (x @ y) * y ' * x ' = y '. [para(106(a,1),13(a,1,2)),demod(60(2))]. given #244 (T,wt=12): 6864 x * (y @ x) * y * x ' = y. [para(163(a,1),1680(a,1,2,1)),demod(60(3),60(7))]. given #245 (T,wt=14): 1780 x * y ' @ y * y = x @ y * y. [para(32(a,1),107(a,1,2,2,2)),demod(60(2),1776(7),60(6)),flip(a)]. given #246 (A,wt=21): 193 x * y ' * z * y * z ' * u = x * (z @ y) * u. [para(163(a,1),37(a,2,2,1)),demod(60(3))]. given #247 (F,wt=14): 1791 (x @ y ') * (x * z @ y) = z @ y. [para(47(a,2),107(a,1,2,2)),demod(99(3),117(10),99(11),360(11),1260(12),1276(9))]. given #248 (F,wt=14): 1794 (x ' @ y) * (x @ y * z) = x @ z. [para(49(a,2),107(a,1,2,2,2)),demod(99(3),233(10),99(11),1258(12),1276(9))]. given #249 (T,wt=14): 1882 x ' * (y @ z) = (z ' @ y) * x '. [para(391(a,1),98(a,1,1)),demod(98(4),99(3),99(7)),flip(a)]. given #250 (T,wt=14): 2006 x ' * (y @ z) = (z @ y ') * x '. [para(398(a,1),98(a,1,1)),demod(98(4),99(3),99(7)),flip(a)]. given #251 (A,wt=22): 194 x * y ' * z ' * y * z * u = x * (z @ y ') * u. [para(163(a,2),37(a,2,2,1))]. given #252 (F,wt=14): 2067 x * y ' @ y * x = x @ y * y. [para(189(a,2),110(a,1,2,2,2)),demod(60(3),2054(8),60(8),1780(8))]. given #253 (F,wt=14): 2107 x * y ' * x ' * (x @ y) = y '. [para(493(a,1),83(a,2)),demod(60(2))]. given #254 (T,wt=14): 2186 x ' * y = y * (x @ y ') * x '. [para(391(a,2),506(a,1,2)),flip(a)]. given #255 (T,wt=14): 2417 (x ' @ y) * (z @ x) = y * z @ x. [para(47(a,1),117(a,1,2)),demod(2060(8))]. given #256 (A,wt=15): 196 x * y @ x * y * z = x * y @ z. [para(7(a,1),153(a,1,2))]. given #257 (F,wt=14): 2428 x * y @ y ' * x = y * y @ x. [para(71(a,1),117(a,1,2)),demod(161(8),131(6),360(5,R),1405(6),360(4),1549(7),7(6),1323(7))]. given #258 (F,wt=14): 2433 x * x @ x ' * y = x * x @ y. [para(117(a,1),107(a,1)),flip(a)]. given #259 (T,wt=14): 2476 x ' @ y * y = x ' * x ' @ y. [para(2444(a,2),116(a,2)),demod(116(4))]. given #260 (T,wt=14): 2753 (x @ y) * (y @ z ') = x * z @ y. [para(141(a,1),14(a,1,2,2,2)),demod(2447(8)),flip(a)]. given #261 (A,wt=17): 222 (x @ y) * z = x * y * x ' * y ' * z. [para(183(a,1),14(a,2,1)),demod(60(2),60(2)),flip(a)]. given #262 (F,wt=14): 2757 (x @ y ') * (y @ z) = y @ x * z. [para(141(a,1),61(a,1,2,2,2)),demod(1568(8),183(7)),flip(a)]. given #263 (F,wt=14): 2960 (x @ y) * (y ' @ z) = x * z @ y. [para(221(a,1),83(a,2,2)),demod(60(4),2447(8)),flip(a)]. given #264 (T,wt=14): 3028 x ' * y @ z = (y @ z) * (z @ x). [para(221(a,1),138(a,2,2)),demod(1496(10),63(7),34(7),7(7),7(6),2415(8),98(8),98(7),60(5),60(5),7(6),1496(7))]. given #265 (T,wt=14): 3235 (x @ y ') * (z * x @ y) = z @ y. [para(506(a,1),140(a,1,2,2,2,2)),demod(98(4),99(3),7(11),117(10))]. given #266 (A,wt=21): 224 x * (y @ z) * u = x * y * z * y ' * z ' * u. [para(183(a,1),37(a,2,2,1)),demod(60(2),60(2)),flip(a)]. given #267 (F,wt=14): 3864 x * y ' * z @ y = x * z @ y. [para(59(a,1),1323(a,1,1,2)),flip(a)]. given #268 (F,wt=14): 3919 x ' * y @ z ' = x * y ' @ z. [back_demod(2820),demod(3867(8)),flip(a)]. given #269 (T,wt=14): 3921 x ' * y @ z = x * y ' @ z '. [back_demod(2451),demod(3867(8))]. given #270 (T,wt=14): 4233 (x @ y) * (x ' @ z * y) = z @ x. [para(162(a,2),2140(a,1,1)),demod(360(5,R))]. given #271 (A,wt=18): 225 (x @ y ') * z = x * y ' * x ' * y * z. [para(195(a,1),14(a,2,1)),demod(60(2)),flip(a)]. given #272 (F,wt=14): 4265 x * y ' @ z = (z @ y) * (x @ z). [para(2140(a,1),491(a,1,2)),flip(a)]. given #273 (F,wt=14): 4314 (x ' @ y) * (y @ z) = y @ x * z. [para(13(a,1),2418(a,1,2,2))]. given #274 (T,wt=14): 4316 x @ y ' * z = (y @ x) * (x @ z). [para(59(a,1),2418(a,1,2,2)),flip(a)]. given #275 (T,wt=14): 4338 x @ y * z ' = (z @ x) * (x @ y). [para(189(a,2),2418(a,1,2,2)),demod(1260(4)),flip(a)]. given #276 (A,wt=18): 226 x ' * y * x * y ' * z = (x ' @ y) * z. [para(195(a,2),14(a,2,1)),demod(60(3))]. given #277 (F,wt=14): 4380 (x @ y ') * (z @ x) = y * z @ x. [para(13(a,1),2429(a,1,2,1))]. given #278 (F,wt=14): 4382 x ' * y @ z = (z @ x) * (y @ z). [para(59(a,1),2429(a,1,2,1)),flip(a)]. given #279 (T,wt=14): 4499 x * y ' @ z = (x @ z) * (z @ y). [para(162(a,1),2446(a,1,2)),flip(a)]. given #280 (T,wt=14): 4893 x ' * y @ x * y = y @ x * x. [para(2814(a,1),150(a,2)),demod(98(2),7(5),1251(7))]. given #281 (A,wt=15): 227 x ' * (x @ y ') = y ' * x ' * y. [para(195(a,1),32(a,2,2)),flip(a)]. given #282 (F,wt=14): 4916 x * y ' @ z ' = y * x ' @ z. [para(3031(a,2),10(a,2)),demod(98(4),60(3),7(7),1538(8))]. given #283 (F,wt=14): 4920 x ' @ y * z ' = x @ z * y '. [para(3031(a,1),162(a,2))]. given #284 (T,wt=14): 4960 x ' @ y ' * z = x @ y * z '. [para(3031(a,1),1465(a,2))]. given #285 (T,wt=14): 4963 x ' @ y * z ' = x @ y ' * z. [para(3031(a,1),1466(a,1))]. given #286 (A,wt=22): 231 x * (y @ z ') * u = x * y * z ' * y ' * z * u. [para(195(a,1),37(a,2,2,1)),demod(60(2)),flip(a)]. given #287 (F,wt=14): 5002 x ' * y @ z ' = y ' * x @ z. [para(3032(a,2),10(a,2)),demod(98(4),60(4),7(7),1773(8))]. given #288 (F,wt=14): 5005 x ' @ y ' * z = x @ z ' * y. [para(3032(a,1),162(a,2))]. given #289 (T,wt=14): 5368 x ' * y @ x * x = y @ x * x. [para(3377(a,1),150(a,2)),demod(98(2),7(5),2947(7))]. given #290 (T,wt=14): 5469 x @ y * z ' = (x @ y) * (z @ x). [para(213(a,1),173(a,2,2,2,2)),demod(4215(11)),flip(a)]. given #291 (A,wt=22): 232 x * y ' * z * y * z ' * u = x * (y ' @ z) * u. [para(195(a,2),37(a,2,2,1)),demod(60(3))]. given #292 (F,wt=14): 5583 x @ y ' * z = (x @ z) * (y @ x). [para(59(a,1),4228(a,1,1,2)),flip(a)]. given #293 (F,wt=14): 5584 (x @ y) * (z ' @ x) = x @ y * z. [para(32(a,1),4228(a,1,1,2)),demod(1260(3))]. given #294 (T,wt=14): 6035 x * x @ y * x ' = x * x @ y. [para(189(a,2),5382(a,1,2)),demod(1260(4)),flip(a)]. given #295 (T,wt=14): 6921 x * y ' @ x * y = x @ y * y. [para(1780(a,1),153(a,2)),demod(7(6),13(5))]. given #296 (A,wt=20): 233 x ' * y ' * z ' * x * z * y = x @ z * y. [para(98(a,1),10(a,1,2,1)),demod(7(7))]. given #297 (F,wt=14): 7002 x * y @ y * x ' = x * x @ y. [para(2067(a,1),99(a,1,1)),demod(99(3)),flip(a)]. given #298 (F,wt=14): 7010 x ' * y @ y * x = y @ x * x. [para(506(a,1),2067(a,1,2)),demod(7(5),360(4),135(5),1276(9))]. given #299 (T,wt=14): 7167 x * y @ x ' * y = x * x @ y. [para(135(a,1),2428(a,1,1)),demod(98(4),99(3),7(5),1258(6),7(9),3881(10),1442(8))]. given #300 (T,wt=14): 7169 x * y @ x * y ' = y * y @ x. [para(2428(a,1),1372(a,1)),flip(a)]. given #301 (A,wt=19): 235 x ' * y ' * z * y * x = z * (z @ y * x). [para(98(a,1),32(a,1,1)),demod(7(6))]. given #302 (F,wt=15): 342 (x @ y) * z * (y @ x) * u = z * u. [para(21(a,1),47(a,2,2,1)),demod(99(2),8(7))]. given #303 (F,wt=15): 343 x * y * (y @ x) * z = y * x * z. [para(47(a,1),13(a,1,2)),demod(60(2))]. given #304 (T,wt=15): 434 x * y * z ' @ z = z ' @ x * y. [para(7(a,1),126(a,1,1))]. given #305 (T,wt=15): 448 (x @ y) * y * x * z = x * y * z. [para(13(a,1),49(a,1,2,2)),demod(60(2),183(5)),flip(a)]. given #306 (A,wt=17): 247 x * y * z @ z ' * y ' = y * z @ x. [para(98(a,1),127(a,1,2))]. given #307 (F,wt=15): 487 (x @ y) * z * u * (y @ x) = z * u. [para(7(a,1),134(a,1,2))]. given #308 (F,wt=15): 490 x * (y @ z) * u = x * u * (y @ z). [para(134(a,1),37(a,1,2,2,2,2)),demod(99(3),345(5),21(5),8(7))]. given #309 (T,wt=15): 497 (x @ y) * z * u = z * u * (x @ y). [para(134(a,1),47(a,1,2,2)),demod(99(2),21(5),8(7))]. given #310 (T,wt=15): 510 x ' * y ' = y ' * x ' * (x @ y). [para(183(a,1),135(a,1,2,2)),flip(a)]. given #311 (A,wt=21): 255 (x @ y) * z ' * y * z = x * y * x ' * (y @ z). [para(60(a,1),43(a,1,1)),demod(183(8)),flip(a)]. given #312 (F,wt=15): 526 (x @ y) * z * u = z * (x @ y) * u. [para(145(a,1),47(a,1,2,2)),demod(99(2),21(5),8(7))]. given #313 (F,wt=15): 591 x @ y * z * x ' = y * z @ x '. [para(7(a,1),208(a,1,2))]. given #314 (T,wt=15): 601 (x @ y ') * y * x ' * y ' = x '. [para(57(a,1),32(a,1,2)),demod(98(4),98(3),60(2),7(4),360(7,R),414(13),34(10))]. given #315 (T,wt=15): 616 x ' * y ' * x = (y @ x ') * y '. [para(230(a,1),43(a,1,2,2)),demod(99(3),34(5),60(8),23(7),8(10)),flip(a)]. given #316 (A,wt=23): 269 x ' * y ' * x * (y @ z) = (x @ y) * z * y ' * z '. [para(183(a,1),43(a,1,2,2,2)),demod(60(8),60(9))]. given #317 (F,wt=15): 679 x ' @ y * x * z = x ' @ y * z. [back_demod(466),demod(672(6)),flip(a)]. given #318 (F,wt=15): 758 x ' * (y ' @ x) = y * x ' * y '. [para(421(a,1),32(a,2,2)),demod(7(6),7(5),58(6),34(10))]. given #319 (T,wt=15): 792 (x @ y) * z * y * x = z * x * y. [para(443(a,1),47(a,1,2,2)),demod(99(2),21(6),8(7))]. ============================== PROOF ================================= % Proof 1 at 4.45 (+ 0.06) seconds: E. % Length of proof is 42. % Level of proof is 15. % Maximum clause weight is 19. % Given clauses 319. 4 x @ y = x ' * y ' * x * y. [input]. 7 (x * y) * z = x * y * z. [input]. 8 e * x = x. [input]. 9 x ' * x = e. [input]. 10 x ' * y ' * x * y = x @ y. [copy(4),flip(a)]. 11 (x @ y) @ z = u @ (v @ w). [input]. 12 A * B * C * B * A != B * A * C * A * B # answer(E). [input]. 13 x ' * x * y = y. [para(9(a,1),7(a,1,1)),demod(8(2)),flip(a)]. 14 x ' * y ' * x * y * z = (x @ y) * z. [para(10(a,1),7(a,1,1)),demod(7(7),7(6)),flip(a)]. 15 (x * y) ' * z ' * x * y * z = x * y @ z. [para(7(a,1),10(a,1,2,2))]. 16 e @ x = e. [para(8(a,1),10(a,1,2,2)),demod(9(4),9(4)),flip(a)]. 21 x @ (y @ z) = e. [para(16(a,1),11(a,1,1)),demod(16(2)),flip(a)]. 23 (x @ y) @ z = e. [para(16(a,1),11(a,2))]. 27 x ' ' * e = x. [para(9(a,1),13(a,1,2))]. 30 x ' ' * (x @ y) = y ' * x * y. [para(10(a,1),13(a,1,2))]. 31 x ' ' * y = x * y. [para(13(a,1),13(a,1,2))]. 32 x ' * y * x = y * (y @ x). [back_demod(30),demod(31(4)),flip(a)]. 34 x * e = x. [back_demod(27),demod(31(4))]. 47 x ' * y * x * z = y * (y @ x) * z. [para(14(a,1),13(a,1,2)),demod(31(5)),flip(a)]. 49 x ' * y * x * z = (x @ y ') * y * z. [para(13(a,1),14(a,1,2,2,2)),demod(31(5))]. 55 x * x ' = e. [para(31(a,1),9(a,1))]. 59 x * x ' * y = y. [para(31(a,1),13(a,1))]. 60 x ' ' = x. [para(31(a,1),34(a,1)),demod(34(2)),flip(a)]. 64 x * y * (x * y) ' = e. [para(55(a,1),7(a,1)),flip(a)]. 73 (x * y) ' * y * x = x * y @ x. [para(13(a,1),15(a,1,2))]. 75 x ' * (y * x @ y) * x = x @ y * x. [para(14(a,1),15(a,1,2)),demod(13(3),13(8))]. 88 x * (y * x) ' = y '. [para(64(a,1),13(a,1,2)),demod(34(3)),flip(a)]. 98 (x * y) ' = y ' * x '. [para(88(a,1),13(a,1,2)),flip(a)]. 99 (x @ y) ' = y @ x. [para(14(a,2),88(a,1,2,1)),demod(98(7),98(5),98(3),98(2),7(5),60(7),7(6),7(5),60(8),7(7),7(6),7(5),10(6),59(4)),flip(a)]. 109 x * y @ x = y @ x. [back_demod(73),demod(98(2),7(5),10(5)),flip(a)]. 128 x ' * (x @ y) * x = x @ y * x. [back_demod(75),demod(109(3))]. 137 x ' * (y @ z) * x = y @ z. [para(23(a,1),32(a,2,2)),demod(34(7))]. 144 x @ y * x = x @ y. [back_demod(128),demod(137(4)),flip(a)]. 150 x ' * y @ x = y @ x. [para(59(a,1),109(a,1,1)),flip(a)]. 158 x ' * y @ y = y @ x. [para(59(a,1),144(a,1,2)),demod(150(6))]. 161 x * y @ y = x @ y. [para(144(a,1),99(a,1,1)),demod(99(2)),flip(a)]. 162 x ' @ y = y @ x. [back_demod(158),demod(161(3))]. 183 x ' @ y ' = x @ y. [para(162(a,2),162(a,1))]. 343 x * y * (y @ x) * z = y * x * z. [para(47(a,1),13(a,1,2)),demod(60(2))]. 443 (x @ y) * y * x = x * y. [para(9(a,1),49(a,1,2,2)),demod(60(2),34(2),183(4)),flip(a)]. 792 (x @ y) * z * y * x = z * x * y. [para(443(a,1),47(a,1,2,2)),demod(99(2),21(6),8(7))]. 9897 $F # answer(E). [para(792(a,2),12(a,1,2,2)),demod(343(13)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=319. Generated=154662. Kept=9890. proofs=1. Usable=270. Sos=6141. Demods=1953. Denials=0. Limbo=3, Disabled=3482. Hints=0. Weight_deleted=16406. Literals_deleted=0. Forward_subsumed=127215. Back_subsumed=564. Sos_limit_deleted=1150. Sos_displaced=0. Sos_removed=0. New_demodulators=4102 (5 lex), Back_demodulated=2912. Back_unit_deleted=0. Demod_attempts=2834281. Demod_rewrites=595547. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=6.47. User_CPU=4.45, System_CPU=0.06, Wall_clock=4. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13113 exit (max_proofs) Mon Jun 19 16:41:28 2006