============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13134 was started by mccune on cleo.thornwood, Mon Jun 19 16:41:41 2006 The command was "/home/mccune/bin/prover9 -f gt.in NE.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 NE.in clauses(sos). (x @ y) * z = z * (x @ y). 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 = z * (x @ y). [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 = z * (x @ y). [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)]. 11 (x @ y) * z = z * (x @ y). [input]. % (lex-dep) 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 = z * (x @ y). [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): 25 x * e = x. [para(16(a,1),11(a,1,1)),demod(8(2),16(2)),flip(a)]. given #9 (T,wt=4): 26 e ' = e. [para(25(a,1),9(a,1))]. given #10 (T,wt=5): 27 x @ e = e. [para(25(a,1),10(a,1,2,2)),demod(26(3),8(3),9(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. [para(9(a,1),13(a,1,2)),demod(25(4))]. given #13 (F,wt=5): 31 x @ x = e. [para(13(a,1),10(a,1,2)),demod(9(2)),flip(a)]. given #14 (T,wt=6): 17 x ' @ x = e. [para(9(a,1),10(a,1,2,2)),demod(13(6)),flip(a)]. given #15 (T,wt=6): 36 x * x ' = e. [para(29(a,1),9(a,1,1))]. 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=6): 40 x @ x ' = e. [para(29(a,1),17(a,1,1))]. given #18 (F,wt=7): 23 (x @ y) @ z = e. [para(11(a,1),10(a,1,2,2)),demod(13(6),11(4,R),22(4)),flip(a)]. given #19 (T,wt=7): 24 x @ (y @ z) = e. [para(11(a,2),10(a,1,2,2)),demod(13(6),9(2)),flip(a)]. given #20 (T,wt=8): 39 x * x ' * y = y. [para(29(a,1),13(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): 90 x @ x * x = e. [para(15(a,1),15(a,1,2)),demod(9(2),26(2),87(3),8(4),9(4),16(5))]. given #23 (F,wt=10): 41 x * y * (x * y) ' = e. [para(36(a,1),7(a,1)),flip(a)]. given #24 (T,wt=9): 99 x * (y * x) ' = y '. [para(41(a,1),13(a,1,2)),demod(25(3)),flip(a)]. given #25 (T,wt=8): 113 (x @ y) ' = y @ x. [para(14(a,2),99(a,1,2,1)),demod(112(7),112(5),112(3),112(2),7(5),29(7),7(6),7(5),29(8),7(7),7(6),7(5),10(6),39(4)),flip(a)]. given #26 (A,wt=15): 19 (x @ y) * z * u = z * (x @ y) * u. [para(11(a,1),7(a,1,1)),demod(7(3)),flip(a)]. given #27 (F,wt=9): 118 (x @ y) * (y @ x) = e. [back_demod(97),demod(112(4),113(3),68(5))]. given #28 (F,wt=9): 124 x @ y * x = x @ y. [back_demod(93),demod(112(2),7(5),10(5)),flip(a)]. given #29 (T,wt=9): 151 x * y @ x = y @ x. [back_demod(87),demod(124(4))]. given #30 (T,wt=8): 182 x @ y ' = y @ x. [para(13(a,1),151(a,1,1)),demod(180(5))]. given #31 (A,wt=15): 20 (x @ y) * z * u = z * u * (x @ y). [para(11(a,2),7(a,1))]. given #32 (F,wt=8): 184 x ' @ y = y @ x. [para(39(a,1),151(a,1,1)),demod(179(4)),flip(a)]. given #33 (F,wt=9): 176 x * y @ y = x @ y. [para(124(a,1),113(a,1,1)),demod(113(2)),flip(a)]. given #34 (T,wt=9): 185 x @ x * y = x @ y. [para(151(a,1),113(a,1,1)),demod(113(2)),flip(a)]. given #35 (T,wt=9): 197 x ' @ y ' = x @ y. [para(182(a,2),182(a,1))]. given #36 (A,wt=15): 21 x * (y @ z) * u = x * u * (y @ z). [para(11(a,1),7(a,2,2)),demod(7(3))]. given #37 (F,wt=9): 227 x ' @ y = x @ y '. [para(184(a,1),182(a,1))]. given #38 (F,wt=10): 112 (x * y) ' = y ' * x '. [para(99(a,1),13(a,1,2)),flip(a)]. given #39 (T,wt=10): 149 x * y @ y ' = y @ x. [back_demod(92),demod(124(5))]. given #40 (T,wt=10): 180 x * y @ x ' = x @ y. [back_demod(171),demod(176(5))]. given #41 (A,wt=12): 32 x ' * y * x = y * (y @ x). [para(10(a,1),13(a,1,2)),demod(29(2)),flip(a)]. given #42 (F,wt=10): 193 (x @ y) * (x ' @ y) = e. [para(182(a,1),118(a,1,1))]. given #43 (F,wt=10): 194 (x @ y) * (x @ y ') = e. [para(182(a,2),118(a,1,1)),demod(11(4,R))]. given #44 (T,wt=10): 237 x ' @ y * x = y @ x. [para(176(a,1),184(a,2))]. given #45 (T,wt=10): 312 x ' * y * x @ y = e. [para(32(a,2),151(a,1,1)),demod(23(6))]. given #46 (A,wt=12): 34 x ' * (y @ z) * x = y @ z. [para(11(a,2),13(a,1,2))]. given #47 (F,wt=10): 320 x @ y ' * x * y = e. [para(32(a,2),185(a,1,2)),demod(24(6))]. given #48 (F,wt=10): 351 x * y * x ' @ y = e. [para(29(a,1),312(a,1,1,1))]. given #49 (T,wt=10): 367 x @ y * x * y ' = e. [para(29(a,1),320(a,1,2,1))]. given #50 (T,wt=11): 104 x ' * y ' @ x * y = e. [back_demod(74),demod(100(8),9(8)),flip(a)]. given #51 (A,wt=14): 37 x * y ' * x ' * y = x ' @ y. [para(29(a,1),10(a,1,1))]. given #52 (F,wt=9): 408 x * y @ y * x = e. [para(104(a,1),182(a,2)),demod(112(5),29(3),29(3))]. given #53 (F,wt=11): 137 x ' @ x * y = x ' @ y. [back_demod(30),demod(112(2),7(4),37(5)),flip(a)]. given #54 (T,wt=11): 148 (x @ y) * z * (y @ x) = z. [back_demod(33),demod(113(2))]. given #55 (T,wt=11): 150 x * y ' @ y = y ' @ x. [back_demod(91),demod(124(7))]. given #56 (A,wt=14): 38 x ' * y * x * y ' = x @ y '. [para(29(a,1),10(a,1,2,1))]. given #57 (F,wt=11): 152 (x @ y) * (y @ x) * z = z. [para(113(a,1),13(a,1,1))]. given #58 (F,wt=11): 155 x @ (y @ z) * u = x @ u. [para(19(a,2),10(a,1,2,2)),demod(112(4),113(4),7(8),152(7),10(5)),flip(a)]. given #59 (T,wt=11): 169 x ' * y * x @ y ' = e. [para(10(a,1),124(a,1,2)),demod(24(5)),flip(a)]. given #60 (T,wt=11): 179 x ' * y @ x = x ' @ y. [back_demod(175),demod(176(3)),flip(a)]. given #61 (A,wt=21): 42 x * y ' * z ' * y * z * u = x * (y @ z) * u. [para(14(a,1),7(a,2,2)),demod(7(7))]. given #62 (F,wt=11): 195 x @ x ' * y = y @ x '. [para(182(a,1),151(a,1))]. given #63 (F,wt=11): 201 x @ y * (z @ u) = x @ y. [para(20(a,2),10(a,1,2,2)),demod(112(4),113(3),7(8),158(8),10(5)),flip(a)]. given #64 (T,wt=11): 235 (x @ y) * z @ u = z @ u. [para(19(a,2),176(a,1,1)),demod(155(6),230(4),155(6))]. given #65 (T,wt=11): 236 x @ y * x ' = y @ x '. [para(176(a,1),182(a,1)),flip(a)]. given #66 (A,wt=13): 45 x ' * y * x = y * (x @ y '). [para(9(a,1),14(a,1,2,2,2)),demod(29(3),25(3),11(6))]. given #67 (F,wt=11): 243 x * (y @ z) @ u = x @ u. [back_demod(80),demod(235(3)),flip(a)]. given #68 (F,wt=11): 274 (x @ y ') * (y @ x ') = e. [para(227(a,1),118(a,1,1))]. given #69 (T,wt=11): 275 (x ' @ y) * (y ' @ x) = e. [para(227(a,2),118(a,1,1))]. given #70 (T,wt=11): 282 x * y @ y ' * x ' = e. [para(112(a,1),40(a,1,2))]. given #71 (A,wt=22): 48 x ' * y * x * (y @ z) = (x @ y ') * z ' * y * z. [para(10(a,1),14(a,1,2,2,2)),demod(29(3))]. given #72 (F,wt=11): 303 x * y * (y @ x) = y * x. [para(32(a,1),13(a,1,2)),demod(29(2))]. given #73 (F,wt=11): 313 (x @ y) * y * x = x * y. [para(151(a,1),32(a,2,2)),demod(7(3),13(4),11(4,R)),flip(a)]. given #74 (T,wt=11): 380 x @ y * x ' * y ' = e. [para(351(a,1),182(a,1)),flip(a)]. given #75 (T,wt=11): 381 x ' @ y * x * y ' = e. [para(351(a,1),184(a,2))]. given #76 (A,wt=17): 51 x ' * y ' * x * y * z = z * (x @ y). [para(14(a,2),11(a,1))]. given #77 (F,wt=11): 387 x * y ' * x ' @ y = e. [para(351(a,1),193(a,1,1)),demod(112(5),112(4),29(3),7(5),8(7))]. given #78 (F,wt=11): 388 x * y * x ' @ y ' = e. [para(351(a,1),194(a,1,1)),demod(8(7))]. given #79 (T,wt=11): 402 x * y ' @ x ' * y = e. [para(29(a,1),104(a,1,1,1))]. given #80 (T,wt=11): 403 x ' * y @ x * y ' = e. [para(29(a,1),104(a,1,1,2))]. given #81 (A,wt=21): 53 x ' * y ' * x * (z @ u) * y = (x @ y) * (z @ u). [para(11(a,2),14(a,1,2,2,2))]. given #82 (F,wt=11): 406 x * y @ x ' * y ' = e. [para(104(a,1),113(a,1,1)),demod(26(2)),flip(a)]. given #83 (F,wt=11): 471 x ' * y ' @ y * x = e. [back_demod(343),demod(466(7))]. given #84 (T,wt=11): 570 x * y ' @ y * x ' = e. [para(29(a,1),282(a,1,2,1))]. given #85 (T,wt=11): 571 x ' * y @ y ' * x = e. [para(29(a,1),282(a,1,2,2))]. given #86 (A,wt=16): 54 x ' * y * x * z = y * (y @ x) * z. [para(14(a,1),13(a,1,2)),demod(29(2)),flip(a)]. given #87 (F,wt=11): 640 x @ y * z = x @ z * y. [para(313(a,1),155(a,1,2))]. given #88 (F,wt=11): 645 x * y @ z = y * x @ z. [para(313(a,1),235(a,1,1))]. given #89 (T,wt=12): 68 x * (y @ z) * x ' = y @ z. [para(11(a,2),39(a,1,2))]. given #90 (T,wt=12): 187 (x @ y) * z = z * (y @ x '). [para(182(a,1),11(a,1,1))]. given #91 (A,wt=17): 56 x ' * y * x * z = (x @ y ') * y * z. [para(13(a,1),14(a,1,2,2,2)),demod(29(3))]. given #92 (F,wt=12): 188 (x @ y ') * z = z * (y @ x). [para(182(a,2),11(a,1,1))]. given #93 (F,wt=12): 198 x * (y @ x) = y * x * y '. [back_demod(133),demod(197(3))]. given #94 (T,wt=12): 221 (x @ y) * z = z * (y ' @ x). [para(184(a,1),11(a,1,1))]. given #95 (T,wt=12): 222 (x ' @ y) * z = z * (y @ x). [para(184(a,2),11(a,1,1))]. given #96 (A,wt=18): 57 (x ' @ y) * z = x * y ' * x ' * y * z. [para(29(a,1),14(a,1,1)),flip(a)]. given #97 (F,wt=12): 327 (x @ y) * x ' * y * x = y. [para(32(a,2),32(a,1,2)),demod(113(2),24(7),25(7))]. given #98 (F,wt=12): 328 (x @ y) * (x ' @ y) * z = z. [para(193(a,1),7(a,1,1)),demod(8(2)),flip(a)]. given #99 (T,wt=12): 331 (x @ y) * z * (x ' @ y) = z. [para(193(a,1),19(a,2,2)),demod(25(7))]. given #100 (T,wt=12): 332 (x ' @ y) * z * (x @ y) = z. [para(193(a,1),20(a,2,2)),demod(25(7))]. given #101 (A,wt=18): 58 x ' * y * x * y ' * z = (x @ y ') * z. [para(29(a,1),14(a,1,2,1))]. given #102 (F,wt=12): 334 (x @ y) * (x @ y ') * z = z. [para(194(a,1),7(a,1,1)),demod(8(2)),flip(a)]. given #103 (F,wt=12): 337 (x @ y) * z * (x @ y ') = z. [para(194(a,1),19(a,2,2)),demod(25(7))]. given #104 (T,wt=12): 338 (x @ y ') * z * (x @ y) = z. [para(194(a,1),20(a,2,2)),demod(25(7))]. given #105 (T,wt=12): 382 x * y * x ' * y @ y = e. [para(351(a,1),176(a,2)),demod(7(4),7(3))]. given #106 (A,wt=14): 60 x ' * y ' * x = (x @ y) * y '. [para(36(a,1),14(a,1,2,2,2)),demod(25(4))]. given #107 (F,wt=12): 461 (x ' @ y) * (x @ y) * z = z. [para(182(a,1),152(a,1,2,1))]. given #108 (F,wt=12): 462 (x @ y ') * (x @ y) * z = z. [para(182(a,2),152(a,1,1))]. given #109 (T,wt=12): 506 x * (y ' @ z) = x * (z @ y). [para(193(a,1),42(a,1,2,2,2,2)),demod(113(3),25(4),34(4),24(4),8(6)),flip(a)]. given #110 (T,wt=12): 507 x * (y @ z ') = x * (z @ y). [para(194(a,1),42(a,1,2,2,2,2)),demod(113(3),25(4),34(4),24(4),8(6)),flip(a)]. given #111 (A,wt=18): 69 x ' * y ' * x * z = (x @ y) * y ' * z. [para(39(a,1),14(a,1,2,2,2))]. given #112 (F,wt=12): 522 x @ y ' * z * y = x @ z. [para(32(a,2),201(a,1,2))]. given #113 (F,wt=12): 538 x * y * (x @ y ') = y * x. [para(45(a,1),13(a,1,2)),demod(29(2))]. given #114 (T,wt=12): 556 x ' * y * x @ z = y @ z. [para(32(a,2),243(a,1,1))]. given #115 (T,wt=12): 614 x * y * (x ' @ y) = y * x. [para(184(a,2),303(a,1,2,2))]. given #116 (A,wt=18): 81 x ' * y * z * x = y * z * (y * z @ x). [para(15(a,1),13(a,1,2)),demod(29(3),7(4)),flip(a)]. given #117 (F,wt=12): 632 (x @ y ') * x * y = y * x. [para(182(a,2),313(a,1,1))]. given #118 (F,wt=12): 636 (x ' @ y) * x * y = y * x. [para(184(a,2),313(a,1,1))]. given #119 (T,wt=12): 782 (x ' @ y) * z = (y @ x) * z. [para(54(a,1),14(a,1)),demod(159(6))]. given #120 (T,wt=12): 891 x @ y * z * y ' = x @ z. [para(13(a,1),640(a,1,2)),demod(7(4)),flip(a)]. given #121 (A,wt=24): 115 x ' * y ' * z * x * y * z ' = y * x @ x ' * z '. [para(99(a,1),15(a,1,2,2,2)),demod(112(2),112(5),112(7),29(5),29(5),7(7),7(8),112(11))]. given #122 (F,wt=12): 898 x * y @ z ' = z @ y * x. [para(640(a,1),182(a,2))]. given #123 (F,wt=12): 900 x ' @ y * z = z * y @ x. [para(640(a,1),184(a,1))]. given #124 (T,wt=12): 932 x * y * x ' @ z = y @ z. [para(13(a,1),645(a,1,1)),demod(7(4)),flip(a)]. given #125 (T,wt=12): 967 (x @ y ') * z = (y @ x) * z. [para(187(a,2),11(a,2))]. given #126 (A,wt=18): 116 (x @ y * z) * x ' * y * z * x = y * z. [para(15(a,1),99(a,1,2,1)),demod(113(7),11(7,R),112(9),112(11),29(9),29(9))]. given #127 (F,wt=12): 1093 x * (y @ x) = x * (x @ y '). [para(198(a,2),303(a,2)),demod(236(5),7(6),13(5)),flip(a)]. given #128 (F,wt=13): 167 x @ y * z * x = x @ y * z. [para(7(a,1),124(a,1,2))]. given #129 (T,wt=13): 230 x * y * z @ z = x * y @ z. [para(7(a,1),176(a,1,1))]. given #130 (T,wt=13): 249 x * y * x ' * y ' = x @ y. [para(197(a,1),10(a,2)),demod(29(2),29(2))]. given #131 (A,wt=15): 123 x ' * y ' = (x @ y) * y ' * x '. [back_demod(100),demod(112(3)),flip(a)]. given #132 (F,wt=13): 268 (x @ y ') * z = z * (x ' @ y). [para(227(a,1),11(a,1,1))]. given #133 (F,wt=13): 269 (x ' @ y) * z = z * (x @ y '). [para(227(a,2),11(a,1,1))]. given #134 (T,wt=13): 281 x ' * (y @ z) = (y @ z) * x '. [para(11(a,1),112(a,1,1)),demod(112(3),113(2),113(6)),flip(a)]. given #135 (T,wt=13): 284 x * y @ z = z @ y ' * x '. [para(112(a,1),182(a,1,2)),flip(a)]. given #136 (A,wt=23): 125 x ' * y ' * z ' * x * y * z = y * x @ x ' * z. [back_demod(89),demod(112(2),112(6),29(6),7(7),7(8))]. given #137 (F,wt=13): 286 x ' * y ' @ z = z @ y * x. [para(112(a,1),184(a,1,1))]. given #138 (F,wt=13): 305 x * (x @ y ') = y * x * y '. [para(29(a,1),32(a,1,1)),flip(a)]. given #139 (T,wt=13): 318 x ' * y * x = y * (x ' @ y). [para(184(a,2),32(a,2,2))]. given #140 (T,wt=13): 324 x * (x ' @ y) = y * x * y '. [para(227(a,2),32(a,2,2)),demod(29(2)),flip(a)]. given #141 (A,wt=21): 126 x ' * y ' * z * y * x * z ' = y * x @ z '. [back_demod(84),demod(112(2),7(8))]. given #142 (F,wt=11): 2428 x * x @ y = x @ y * y. [back_demod(2231),demod(2420(4))]. given #143 (F,wt=12): 2442 x * x @ y ' = y * y @ x. [para(2428(a,2),182(a,2))]. given #144 (T,wt=12): 2446 x ' @ y * y = y @ x * x. [para(2428(a,1),184(a,2))]. given #145 (T,wt=13): 425 x * y * z @ z * x * y = e. [para(7(a,1),408(a,1,1))]. given #146 (A,wt=23): 127 x * y ' * z ' * x ' * y * z = y * x ' @ x * z. [back_demod(82),demod(112(3),29(2),112(4),7(7),7(8))]. given #147 (F,wt=13): 426 x * y * z @ y * z * x = e. [para(7(a,1),408(a,1,2))]. given #148 (F,wt=13): 443 (x @ y ') * z * (y @ x ') = z. [para(227(a,1),148(a,1,1))]. given #149 (T,wt=13): 444 (x ' @ y) * z * (y ' @ x) = z. [para(227(a,2),148(a,1,1))]. given #150 (T,wt=13): 463 (x @ y ') * (y @ x ') * z = z. [para(227(a,1),152(a,1,1))]. given #151 (A,wt=24): 134 x ' * y ' * z ' * y * x * z * u = (y * x @ z) * u. [back_demod(44),demod(112(2),7(9))]. given #152 (F,wt=13): 464 (x ' @ y) * (y ' @ x) * z = z. [para(227(a,2),152(a,1,1))]. given #153 (F,wt=13): 565 x * (y ' @ z) = x * (y @ z '). [para(274(a,1),42(a,1,2,2,2,2)),demod(113(4),25(5),34(5),24(6),8(7))]. given #154 (T,wt=13): 612 x ' * y * (x @ y) = y * x '. [para(182(a,1),303(a,1,2,2))]. given #155 (T,wt=13): 613 x * y ' * (x @ y) = y ' * x. [para(184(a,1),303(a,1,2,2))]. given #156 (A,wt=24): 135 x ' * y ' * z ' * x * z * y * u = (x @ z * y) * u. [back_demod(43),demod(112(3),7(8))]. given #157 (F,wt=13): 631 (x @ y) * x ' * y = y * x '. [para(182(a,1),313(a,1,1))]. given #158 (F,wt=13): 635 x ' * y = (y @ x) * y * x '. [para(184(a,1),313(a,1,1)),flip(a)]. given #159 (T,wt=12): 3085 x * (y @ x) * y * x ' = y. [para(635(a,1),13(a,1,2)),demod(29(2))]. given #160 (T,wt=13): 780 x ' * y = y * (y @ x) * x '. [para(36(a,1),54(a,1,2,2)),demod(25(3))]. given #161 (A,wt=20): 138 x ' * y ' * z ' * y * x * z = y * x @ z. [back_demod(15),demod(112(2),7(8))]. given #162 (F,wt=13): 836 x @ y * x * z = x @ y * z. [para(54(a,1),137(a,1,2)),demod(29(2),466(4),29(4)),flip(a)]. given #163 (F,wt=13): 895 (x @ y * z) * (z * y @ x) = e. [para(640(a,1),118(a,1,1))]. given #164 (T,wt=13): 896 (x * y @ z) * (z @ y * x) = e. [para(640(a,1),118(a,1,2))]. given #165 (T,wt=13): 901 x ' * y ' @ z = z @ x * y. [para(640(a,1),184(a,2)),demod(112(2))]. given #166 (A,wt=19): 153 (x @ y) * z * u * v = z * u * (x @ y) * v. [para(19(a,2),7(a,1)),demod(7(3))]. given #167 (F,wt=13): 937 x * y @ z = z @ x ' * y '. [para(645(a,1),182(a,2)),demod(112(2)),flip(a)]. given #168 (F,wt=13): 1046 (x ' @ y) * z = (x @ y ') * z. [para(56(a,1),54(a,1,2)),demod(159(6),159(9)),flip(a)]. given #169 (T,wt=13): 1343 x * x * y * y @ x * y = e. [para(13(a,1),382(a,1,1,2,2)),demod(7(2))]. given #170 (T,wt=13): 1971 x * y * z @ y = x * z @ y. [para(303(a,1),230(a,1,1,2)),demod(201(5),201(7))]. given #171 (A,wt=19): 154 x * (y @ z) * u * v = x * u * (y @ z) * v. [para(19(a,1),7(a,2,2)),demod(7(4))]. given #172 (F,wt=13): 2161 x * y ' @ z = z @ y * x '. [para(29(a,1),284(a,2,2,1))]. given #173 (F,wt=13): 2162 x ' * y @ z = z @ y ' * x. [para(29(a,1),284(a,2,2,2))]. given #174 (T,wt=13): 2400 (x @ y) * (z @ y) = x * z @ y. [para(69(a,1),126(a,1,2)),demod(29(5),156(7),29(6))]. given #175 (T,wt=13): 2441 x @ y ' * y ' = y @ x * x. [para(2428(a,1),182(a,1))]. given #176 (A,wt=21): 156 x ' * (y @ z) * u ' * x * u = (y @ z) * (x @ u). [para(10(a,1),19(a,1,2)),flip(a)]. given #177 (F,wt=13): 2445 x ' * x ' @ y = y * y @ x. [para(2428(a,2),184(a,1))]. given #178 (F,wt=13): 2525 x * x @ y * x = x @ y * y. [para(2428(a,2),167(a,1)),demod(7(5),836(6))]. given #179 (T,wt=13): 2526 x * y @ y * y = x * x @ y. [para(2428(a,1),230(a,1)),demod(7(5),1971(6))]. given #180 (T,wt=13): 2552 x ' @ y * y = x * x @ y '. [para(2442(a,2),184(a,2))]. given #181 (A,wt=19): 157 (x @ y) * (z @ u) * v = v * (x @ y) * (z @ u). [para(11(a,2),19(a,1,2))]. given #182 (F,wt=13): 2654 x * y * z @ y * x * z = e. [para(303(a,1),425(a,1,1,2)),demod(7(6),466(7))]. given #183 (F,wt=13): 2861 x ' * y @ z = z @ x * y '. [back_demod(2418),demod(2858(8))]. given #184 (T,wt=13): 2862 x * y ' @ z = z @ x ' * y. [back_demod(2417),demod(2858(8))]. given #185 (T,wt=13): 3012 (x @ y) * (x @ z) = x @ y * z. [para(48(a,1),135(a,1,2,2,2)),demod(29(2),156(9),2008(5),39(5),237(5)),flip(a)]. given #186 (A,wt=15): 158 (x @ y) * z * (y @ x) * u = z * u. [para(19(a,1),13(a,1,2)),demod(113(2))]. given #187 (F,wt=13): 3255 (x @ y) * (y @ x * z) = y @ z. [para(54(a,2),138(a,1,2,2,2)),demod(113(2),280(9),243(7))]. given #188 (F,wt=13): 3604 x * y * z @ z * y * x = e. [back_demod(2680),demod(3458(8))]. given #189 (T,wt=13): 4077 (x @ y) * (y * z @ x) = z @ x. [para(2400(a,1),13(a,1,2)),demod(113(2))]. given #190 (T,wt=13): 4096 (x @ y) * (z * y @ x) = z @ x. [para(2400(a,1),32(a,1,2)),demod(113(2),24(8),25(7))]. given #191 (A,wt=16): 159 x ' * (y @ z) * x * u = (y @ z) * u. [para(19(a,2),13(a,1,2))]. given #192 (F,wt=13): 4466 x * x @ y * x = x * x @ y. [para(2525(a,2),10(a,2)),demod(112(3),7(7),125(8),2429(4)),flip(a)]. given #193 (F,wt=13): 4471 x * y @ x * x = y @ x * x. [para(2525(a,2),176(a,1)),demod(7(5),7(4),230(9),939(5))]. given #194 (T,wt=13): 4506 x * x @ x * y = x * x @ y. [para(2526(a,2),124(a,1)),demod(7(8),7(7),167(9),897(5))]. given #195 (T,wt=13): 4517 x * y @ y * y = x @ y * y. [para(2526(a,1),34(a,1,2,1)),demod(4075(4),364(6),3012(3)),flip(a)]. given #196 (A,wt=25): 160 x ' * y ' * x * (z @ u) * y * v = (x @ y) * (z @ u) * v. [para(19(a,2),14(a,1,2,2,2))]. given #197 (F,wt=13): 4612 x * y * z @ x * z * y = e. [para(313(a,1),2654(a,1,1,2)),demod(155(7))]. given #198 (F,wt=13): 4857 (x @ y) * (y @ z * x) = y @ z. [para(3012(a,1),32(a,1,2)),demod(113(2),24(8),25(7))]. given #199 (T,wt=14): 290 x ' * y ' @ z = y * x @ z '. [para(112(a,1),227(a,1,1))]. given #200 (T,wt=14): 291 x ' @ y * z = x @ z ' * y '. [para(112(a,1),227(a,2,2))]. given #201 (A,wt=21): 161 x ' * y ' * x * y * z * u = z * (x @ y) * u. [para(19(a,1),14(a,2))]. given #202 (F,wt=14): 292 x * y * z @ z ' = z @ x * y. [para(7(a,1),149(a,1,1))]. given #203 (F,wt=14): 302 (x @ y) * y ' * x ' * y = x '. [para(10(a,1),32(a,1,2)),demod(112(4),112(2),29(5),7(4),11(6,R),231(12),25(9))]. given #204 (T,wt=14): 317 x ' * (y @ x) = y ' * x ' * y. [para(184(a,1),32(a,2,2)),flip(a)]. given #205 (T,wt=14): 321 x ' * (x @ y) = y * x ' * y '. [para(197(a,1),32(a,2,2)),demod(29(2)),flip(a)]. given #206 (A,wt=25): 162 x ' * (y @ z) * u ' * x * u * v = (y @ z) * (x @ u) * v. [para(14(a,1),19(a,1,2)),flip(a)]. given #207 (F,wt=14): 340 x ' @ y * z * x = y * z @ x. [para(7(a,1),237(a,1,2))]. given #208 (F,wt=14): 549 x ' * (y @ x) = x ' * (x @ y '). [para(45(a,1),32(a,1,2)),demod(112(2),7(7),13(6),237(8)),flip(a)]. given #209 (T,wt=14): 617 x * y ' * (y @ x ') = y ' * x. [para(227(a,1),303(a,1,2,2))]. given #210 (T,wt=14): 618 x ' * y * (y ' @ x) = y * x '. [para(227(a,2),303(a,1,2,2))]. given #211 (A,wt=25): 163 (x @ y) * z ' * u ' * z * u * v = (z @ u) * (x @ y) * v. [para(14(a,2),19(a,1,2))]. given #212 (F,wt=14): 638 x ' * y = (x @ y ') * y * x '. [para(227(a,1),313(a,1,1)),flip(a)]. given #213 (F,wt=14): 639 (x ' @ y) * y ' * x = x * y '. [para(227(a,2),313(a,1,1))]. given #214 (T,wt=14): 775 x ' * y ' * x * (y @ x) = y '. [para(9(a,1),54(a,1,2)),demod(25(3),112(3),112(6),150(8),197(7),11(6),7(7)),flip(a)]. given #215 (T,wt=14): 903 x ' @ y ' * z ' = x @ y * z. [para(640(a,1),197(a,2)),demod(112(3))]. given #216 (A,wt=21): 164 (x @ y) * z * u = z * x ' * y ' * x * y * u. [para(14(a,2),19(a,2,2))]. given #217 (F,wt=14): 905 x ' @ y * z = x @ y ' * z '. [para(640(a,1),227(a,1)),demod(112(5))]. given #218 (F,wt=14): 940 x ' * y ' @ z ' = x * y @ z. [para(645(a,1),197(a,2)),demod(112(2))]. given #219 (T,wt=14): 942 x ' * y ' @ z = x * y @ z '. [para(645(a,1),227(a,2)),demod(112(2))]. given #220 (T,wt=14): 978 x ' * (y @ z) = (z ' @ y) * x '. [para(187(a,1),112(a,1,1)),demod(112(4),113(3),113(7)),flip(a)]. given #221 (A,wt=16): 165 x * (y @ z) * x ' * u = (y @ z) * u. [para(19(a,2),39(a,1,2))]. given #222 (F,wt=14): 1062 x ' * (y ' @ z) = (z @ y) * x '. [para(188(a,1),112(a,1,1)),demod(112(3),113(2),113(7)),flip(a)]. given #223 (F,wt=14): 1086 (x @ y) * x ' = y * x ' * y '. [para(198(a,1),112(a,1,1)),demod(112(4),112(3),29(2),7(4),113(6)),flip(a)]. given #224 (T,wt=14): 1115 x ' * (y @ z) = (z @ y ') * x '. [para(221(a,1),112(a,1,1)),demod(112(4),113(3),113(7)),flip(a)]. given #225 (T,wt=14): 1145 x ' * (y @ z ') = (z @ y) * x '. [para(222(a,1),112(a,1,1)),demod(112(3),113(2),113(7)),flip(a)]. given #226 (A,wt=23): 166 (x @ y) * (z @ u) * v * w = v * (x @ y) * (z @ u) * w. [para(19(a,2),19(a,1,2))]. given #227 (F,wt=14): 1221 (x @ y) * x * y ' * x ' = y '. [para(197(a,1),327(a,1,1)),demod(29(3))]. given #228 (F,wt=14): 1495 x * y ' * x ' * (x @ y) = y '. [para(69(a,2),332(a,1)),demod(29(2))]. given #229 (T,wt=14): 1559 x ' * y = y * (x @ y ') * x '. [para(187(a,2),614(a,1,2)),flip(a)]. given #230 (T,wt=14): 2008 (x @ y ') * (y @ z) = y @ x * z. [para(249(a,1),56(a,2,2)),demod(1752(8)),flip(a)]. given #231 (A,wt=15): 181 x * y * z @ x * y = z @ x * y. [para(7(a,1),151(a,1,1))]. given #232 (F,wt=14): 2021 x * (x @ y) * y ' * x ' = y '. [para(123(a,1),13(a,1,2)),demod(29(2))]. given #233 (F,wt=14): 2215 x * y ' @ y * y = x @ y * y. [para(32(a,1),125(a,1,2,2,2)),demod(29(2),2209(7),29(6)),flip(a)]. given #234 (T,wt=14): 2222 (x ' @ y) * (x @ y * z) = x @ z. [para(45(a,2),125(a,2,1)),demod(113(3),675(10),2008(6),113(11),155(12),556(9))]. given #235 (T,wt=14): 2228 (x @ y ') * (x * z @ y) = z @ y. [para(54(a,2),125(a,1,2,2)),demod(113(3),138(10),113(11),11(11),201(12),243(9))]. given #236 (A,wt=17): 189 x ' * y * x * y ' * z = (y @ x) * z. [para(182(a,1),14(a,2,1)),demod(29(3))]. given #237 (F,wt=14): 2420 x * x @ x ' * y = x * x @ y. [back_demod(1754),demod(2400(7))]. given #238 (F,wt=14): 2426 (x @ y) * (y ' @ z) = x * z @ y. [back_demod(2011),demod(2419(6)),flip(a)]. given #239 (T,wt=14): 2429 x * y @ y ' * x = y * y @ x. [back_demod(2226),demod(2420(8))]. given #240 (T,wt=14): 2455 x ' @ y * y = x ' * x ' @ y. [para(2428(a,2),137(a,2)),demod(137(4))]. given #241 (A,wt=18): 190 x ' * y ' * x * y * z = (y @ x ') * z. [para(182(a,2),14(a,2,1))]. given #242 (F,wt=14): 2590 x * y ' @ y * x = x @ y * y. [para(2446(a,1),10(a,2)),demod(29(2),112(2),7(7),127(8))]. given #243 (F,wt=14): 2821 (x ' @ y) * (y @ z) = y @ x * z. [para(48(a,1),134(a,1,2,2,2)),demod(29(3),39(10),156(8),2008(4),179(5)),flip(a)]. given #244 (T,wt=14): 2858 x @ y * x ' * z = x @ y * z. [back_demod(2266),demod(2821(8))]. given #245 (T,wt=14): 2865 x @ y ' * z = (y @ x) * (x @ z). [back_demod(2264),demod(2858(5))]. given #246 (A,wt=16): 191 (x @ y) * z * u = z * (y @ x ') * u. [para(182(a,1),19(a,1,1))]. given #247 (F,wt=14): 2867 x @ y ' * z = (x @ z) * (y @ x). [back_demod(2262),demod(2858(5))]. given #248 (F,wt=14): 3254 (x ' @ y) * (z @ x) = y * z @ x. [para(54(a,1),138(a,1,2)),demod(675(8))]. given #249 (T,wt=14): 3880 x * y ' @ z ' = y * x ' @ z. [para(2161(a,2),10(a,2)),demod(112(4),29(3),7(7),1716(8))]. given #250 (T,wt=14): 3889 x ' @ y * z ' = x @ z * y '. [para(2161(a,1),182(a,1))]. given #251 (A,wt=16): 192 (x @ y ') * z * u = z * (y @ x) * u. [para(182(a,2),19(a,1,1))]. given #252 (F,wt=14): 3938 x ' @ y * z ' = x @ y ' * z. [para(2161(a,1),898(a,1))]. given #253 (F,wt=14): 3939 x ' * y @ z ' = x * y ' @ z. [para(2161(a,2),898(a,2))]. given #254 (T,wt=14): 3940 x ' * y @ z = x * y ' @ z '. [para(2161(a,2),900(a,1)),flip(a)]. given #255 (T,wt=14): 3941 x ' @ y ' * z = x @ y * z '. [para(2161(a,1),900(a,2))]. given #256 (A,wt=19): 199 (x @ y) * z * u * v = z * u * v * (x @ y). [para(20(a,2),7(a,1)),demod(7(3))]. given #257 (F,wt=14): 3976 x ' * y @ z ' = y ' * x @ z. [para(2162(a,2),10(a,2)),demod(112(4),29(4),7(7),2205(8))]. given #258 (F,wt=14): 3985 x ' @ y ' * z = x @ z ' * y. [para(2162(a,1),182(a,1))]. given #259 (T,wt=14): 4083 (x @ y ') * (z @ x) = y * z @ x. [para(182(a,2),2400(a,1,1))]. given #260 (T,wt=14): 4084 (x @ y) * (y @ z ') = x * z @ y. [para(182(a,2),2400(a,1,2))]. given #261 (A,wt=19): 200 x * (y @ z) * u * v = x * u * v * (y @ z). [para(20(a,1),7(a,2,2)),demod(7(4))]. given #262 (F,wt=14): 4087 x ' * y @ z = (z @ x) * (y @ z). [para(184(a,1),2400(a,1,1)),flip(a)]. given #263 (F,wt=14): 4088 x * y ' @ z = (x @ z) * (z @ y). [para(184(a,1),2400(a,1,2)),flip(a)]. given #264 (T,wt=14): 4114 x * y ' @ z = (z @ y) * (x @ z). [para(2400(a,1),221(a,2)),flip(a)]. given #265 (T,wt=14): 4115 x ' * y @ z = (y @ z) * (z @ x). [para(2400(a,1),222(a,1))]. given #266 (A,wt=19): 202 (x @ y) * z * (u @ v) = (u @ v) * z * (x @ y). [para(11(a,1),20(a,1,2))]. given #267 (F,wt=14): 4118 (x @ y ') * (z * x @ y) = z @ y. [para(2400(a,1),338(a,1,2))]. given #268 (F,wt=14): 4843 x @ y * z ' = (x @ y) * (z @ x). [para(182(a,1),3012(a,1,2)),flip(a)]. given #269 (T,wt=14): 4846 (x @ y) * (z ' @ x) = x @ y * z. [para(184(a,2),3012(a,1,2))]. given #270 (T,wt=14): 4870 x @ y * z ' = (z @ x) * (x @ y). [para(3012(a,1),187(a,2)),flip(a)]. given #271 (A,wt=19): 203 (x @ y) * (z @ u) * v = v * (z @ u) * (x @ y). [para(11(a,2),20(a,1,2))]. given #272 (F,wt=14): 4872 (x ' @ y) * (x @ z * y) = x @ z. [para(3012(a,1),332(a,1,2))]. given #273 (F,wt=14): 5327 x ' * y @ x * x = y @ x * x. [para(39(a,1),4471(a,1,1)),flip(a)]. given #274 (T,wt=14): 5348 x * x @ y * x ' = x * x @ y. [para(198(a,2),4506(a,1,2)),demod(201(4)),flip(a)]. given #275 (T,wt=14): 6390 x * y ' @ x * y = x @ y * y. [para(2215(a,1),185(a,2)),demod(7(6),13(5))]. given #276 (A,wt=15): 204 (x @ y) * z * u * (y @ x) = z * u. [para(20(a,1),13(a,1,2)),demod(113(2))]. given #277 (F,wt=14): 6516 x * y @ x ' * y = x * x @ y. [para(2420(a,1),176(a,2)),demod(7(4),39(3))]. given #278 (F,wt=14): 6580 x ' * y @ y * x = y @ x * x. [para(2429(a,1),113(a,1,1)),demod(113(3)),flip(a)]. given #279 (T,wt=14): 6584 x * y @ y * x ' = x * x @ y. [para(303(a,1),2429(a,1,2)),demod(7(4),11(3),538(4),201(9))]. given #280 (T,wt=14): 6586 x * y @ x * y ' = y * y @ x. [para(2429(a,1),640(a,1)),flip(a)]. given #281 (A,wt=25): 205 x ' * y ' * x * (z @ u) * y * v = (x @ y) * v * (z @ u). [para(20(a,2),14(a,1,2,2,2))]. given #282 (F,wt=14): 6681 x ' * y @ x * y = y @ x * x. [para(2590(a,1),645(a,1)),flip(a)]. given #283 (F,wt=15): 247 x * y @ x * y * z = x * y @ z. [para(7(a,1),185(a,1,2))]. given #284 (T,wt=15): 304 x ' * (x ' @ y) = y ' * x ' * y. [para(13(a,1),32(a,1,2)),demod(112(2),7(4),137(8)),flip(a)]. given #285 (T,wt=15): 323 x ' * (x @ y ') = y ' * x ' * y. [para(227(a,1),32(a,2,2)),flip(a)]. given #286 (A,wt=21): 207 x ' * y ' * x * y * z * u = z * u * (x @ y). [para(20(a,1),14(a,2))]. given #287 (F,wt=15): 445 x * y * z ' @ z = z ' @ x * y. [para(7(a,1),150(a,1,1))]. given #288 (F,wt=15): 458 (x @ y ') * y * x ' * y ' = x '. [para(38(a,1),32(a,1,2)),demod(112(4),112(3),29(2),7(4),11(7,R),381(13),25(10))]. given #289 (T,wt=15): 466 x @ y * (z @ u) * v = x @ y * v. [para(19(a,1),155(a,1,2))]. given #290 (T,wt=15): 467 x @ y * z * (u @ v) = x @ y * z. [para(20(a,1),155(a,1,2))]. given #291 (A,wt=25): 208 x ' * y ' * x * y * z * (u @ v) = (u @ v) * (x @ y) * z. [para(20(a,2),14(a,2))]. given #292 (F,wt=15): 526 x * (y @ z) * u @ v = x * u @ v. [para(19(a,1),235(a,1,1))]. given #293 (F,wt=15): 527 x * y * (z @ u) @ v = x * y @ v. [para(20(a,1),235(a,1,1))]. given #294 (T,wt=15): 531 x @ y * z * x ' = y * z @ x '. [para(7(a,1),236(a,1,2))]. given #295 (T,wt=15): 605 x ' * y ' * x = (y @ x ') * y '. [para(275(a,1),48(a,1,2,2)),demod(113(3),25(5),29(8),23(7),8(10)),flip(a)]. given #296 (A,wt=25): 209 (x @ y) * z ' * u ' * z * u * v = (z @ u) * v * (x @ y). [para(14(a,2),20(a,1,2))]. given #297 (F,wt=15): 606 x * y * (y @ x) * z = y * x * z. [para(303(a,1),7(a,1,1)),demod(7(2),7(5)),flip(a)]. given #298 (F,wt=15): 616 x ' * y ' = y ' * x ' * (x @ y). [para(197(a,1),303(a,1,2,2)),flip(a)]. given #299 (T,wt=15): 620 x * y * y * x = y * x * x * y. [para(408(a,1),303(a,1,2,2)),demod(25(4),7(3),7(6))]. given #300 (T,wt=15): 624 (x @ y) * y * x * z = x * y * z. [para(313(a,1),7(a,1,1)),demod(7(2),7(5)),flip(a)]. given #301 (A,wt=25): 210 (x @ y) * z * (u @ v) = z * u ' * v ' * u * v * (x @ y). [para(14(a,2),20(a,2,2))]. given #302 (F,wt=15): 630 (x @ y) * z * y * x = z * x * y. [para(313(a,1),19(a,2,2))]. ============================== PROOF ================================= % Proof 1 at 4.32 (+ 0.06) seconds: E. % Length of proof is 29. % Level of proof is 13. % Maximum clause weight is 19. % Given clauses 302. 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 = z * (x @ y). [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)]. 19 (x @ y) * z * u = z * (x @ y) * u. [para(11(a,1),7(a,1,1)),demod(7(3)),flip(a)]. 25 x * e = x. [para(16(a,1),11(a,1,1)),demod(8(2),16(2)),flip(a)]. 29 x ' ' = x. [para(9(a,1),13(a,1,2)),demod(25(4))]. 32 x ' * y * x = y * (y @ x). [para(10(a,1),13(a,1,2)),demod(29(2)),flip(a)]. 36 x * x ' = e. [para(29(a,1),9(a,1,1))]. 41 x * y * (x * y) ' = e. [para(36(a,1),7(a,1)),flip(a)]. 83 (x * y) ' * y * x = x * y @ x. [para(13(a,1),15(a,1,2))]. 87 x * y @ x = y @ x * y. [para(14(a,1),15(a,1,2)),demod(13(3),11(4),13(5),13(5))]. 93 (x * y) ' * y * x = y @ x * y. [back_demod(83),demod(87(6))]. 99 x * (y * x) ' = y '. [para(41(a,1),13(a,1,2)),demod(25(3)),flip(a)]. 112 (x * y) ' = y ' * x '. [para(99(a,1),13(a,1,2)),flip(a)]. 124 x @ y * x = x @ y. [back_demod(93),demod(112(2),7(5),10(5)),flip(a)]. 151 x * y @ x = y @ x. [back_demod(87),demod(124(4))]. 303 x * y * (y @ x) = y * x. [para(32(a,1),13(a,1,2)),demod(29(2))]. 313 (x @ y) * y * x = x * y. [para(151(a,1),32(a,2,2)),demod(7(3),13(4),11(4,R)),flip(a)]. 606 x * y * (y @ x) * z = y * x * z. [para(303(a,1),7(a,1,1)),demod(7(2),7(5)),flip(a)]. 630 (x @ y) * z * y * x = z * x * y. [para(313(a,1),19(a,2,2))]. 9096 $F # answer(E). [para(630(a,2),12(a,1,2,2)),demod(606(13)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=302. Generated=152618. Kept=9089. proofs=1. Usable=271. Sos=6129. Demods=1711. Denials=0. Limbo=2, Disabled=2693. Hints=0. Weight_deleted=17534. Literals_deleted=0. Forward_subsumed=124120. Back_subsumed=327. Sos_limit_deleted=1874. Sos_displaced=0. Sos_removed=0. New_demodulators=3254 (5 lex), Back_demodulated=2360. Back_unit_deleted=0. Demod_attempts=2673735. Demod_rewrites=539232. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=6.16. User_CPU=4.32, System_CPU=0.06, Wall_clock=5. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13134 exit (max_proofs) Mon Jun 19 16:41:46 2006