============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 3875 was started by mccune on cleo.thornwood, Wed Nov 22 11:24:24 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). formulas(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 formulas(sos). (x @ y) * z = z * (x @ y). end_of_list. formulas(sos). A * B * C * B * A != B * A * C * A * B # answer(E). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). (x * y) * z = x * y * z. [assumption]. e * x = x. [assumption]. x' * x = e. [assumption]. x @ y = x' * y' * x * y. [assumption]. (x @ y) * z = z * (x @ y). [assumption]. A * B * C * B * A != B * A * C * A * B # answer(E). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ 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: formulas(usable). end_of_list. formulas(sos). 1 (x * y) * z = x * y * z. [assumption]. 2 e * x = x. [assumption]. 3 x' * x = e. [assumption]. 5 x' * y' * x * y = x @ y. [copy(4),flip(a)]. 6 (x @ y) * z = z * (x @ y). [assumption]. 7 A * B * C * B * A != B * A * C * A * B # answer(E). [assumption]. end_of_list. formulas(demodulators). 1 (x * y) * z = x * y * z. [assumption]. 2 e * x = x. [assumption]. 3 x' * x = e. [assumption]. 5 x' * y' * x * y = x @ y. [copy(4),flip(a)]. 6 (x @ y) * z = z * (x @ y). [assumption]. % (lex-dep) end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=11): 1 (x * y) * z = x * y * z. [assumption]. given #2 (I,wt=5): 2 e * x = x. [assumption]. given #3 (I,wt=6): 3 x' * x = e. [assumption]. given #4 (I,wt=13): 5 x' * y' * x * y = x @ y. [copy(4),flip(a)]. given #5 (I,wt=11): 6 (x @ y) * z = z * (x @ y). [assumption]. given #6 (I,wt=19): 7 A * B * C * B * A != B * A * C * A * B # answer(E). [assumption]. given #7 (F,wt=5): 11 e @ x = e. [para(2(a,1),5(a,1,2,2)),rewrite(3(4),3(4)),flip(a)]. given #8 (F,wt=5): 20 x * e = x. [para(11(a,1),6(a,1,1)),rewrite(2(2),11(2)),flip(a)]. given #9 (T,wt=4): 21 e' = e. [para(20(a,1),3(a,1))]. given #10 (T,wt=5): 22 x @ e = e. [para(20(a,1),5(a,1,2,2)),rewrite(21(3),2(3),3(2)),flip(a)]. given #11 (A,wt=8): 8 x' * x * y = y. [para(3(a,1),1(a,1,1)),rewrite(2(2)),flip(a)]. given #12 (F,wt=5): 24 x'' = x. [para(3(a,1),8(a,1,2)),rewrite(20(4))]. given #13 (F,wt=5): 26 x @ x = e. [para(8(a,1),5(a,1,2)),rewrite(3(2)),flip(a)]. given #14 (T,wt=6): 12 x' @ x = e. [para(3(a,1),5(a,1,2,2)),rewrite(8(6)),flip(a)]. given #15 (T,wt=6): 31 x * x' = e. [para(24(a,1),3(a,1,1))]. given #16 (A,wt=17): 9 x' * y' * x * y * z = (x @ y) * z. [para(5(a,1),1(a,1,1)),rewrite(1(7),1(6)),flip(a)]. given #17 (F,wt=6): 35 x @ x' = e. [para(24(a,1),12(a,1,1))]. given #18 (F,wt=7): 18 (x @ y) @ z = e. [para(6(a,1),5(a,1,2,2)),rewrite(8(6),6(4,R),17(4)),flip(a)]. given #19 (T,wt=7): 19 x @ (y @ z) = e. [para(6(a,2),5(a,1,2,2)),rewrite(8(6),3(2)),flip(a)]. given #20 (T,wt=8): 34 x * x' * y = y. [para(24(a,1),8(a,1,1))]. given #21 (A,wt=19): 10 (x * y)' * z' * x * y * z = x * y @ z. [para(1(a,1),5(a,1,2,2))]. given #22 (F,wt=7): 85 x @ x * x = e. [para(10(a,1),10(a,1,2)),rewrite(3(2),21(2),82(3),2(4),3(4),11(5))]. given #23 (F,wt=10): 36 x * y * (x * y)' = e. [para(31(a,1),1(a,1)),flip(a)]. given #24 (T,wt=9): 94 x * (y * x)' = y'. [para(36(a,1),8(a,1,2)),rewrite(20(3)),flip(a)]. given #25 (T,wt=8): 108 (x @ y)' = y @ x. [para(9(a,2),94(a,1,2,1)),rewrite(107(7),107(5),107(3),107(2),1(5),24(7),1(6),1(5),24(8),1(7),1(6),1(5),5(6),34(4)),flip(a)]. given #26 (A,wt=15): 14 (x @ y) * z * u = z * (x @ y) * u. [para(6(a,1),1(a,1,1)),rewrite(1(3)),flip(a)]. given #27 (F,wt=9): 113 (x @ y) * (y @ x) = e. [back_rewrite(92),rewrite(107(4),108(3),63(5))]. given #28 (F,wt=9): 119 x @ y * x = x @ y. [back_rewrite(88),rewrite(107(2),1(5),5(5)),flip(a)]. given #29 (T,wt=9): 146 x * y @ x = y @ x. [back_rewrite(82),rewrite(119(4))]. given #30 (T,wt=8): 177 x @ y' = y @ x. [para(8(a,1),146(a,1,1)),rewrite(175(5))]. given #31 (A,wt=15): 15 (x @ y) * z * u = z * u * (x @ y). [para(6(a,2),1(a,1))]. given #32 (F,wt=8): 179 x' @ y = y @ x. [para(34(a,1),146(a,1,1)),rewrite(174(4)),flip(a)]. given #33 (F,wt=9): 171 x * y @ y = x @ y. [para(119(a,1),108(a,1,1)),rewrite(108(2)),flip(a)]. given #34 (T,wt=9): 180 x @ x * y = x @ y. [para(146(a,1),108(a,1,1)),rewrite(108(2)),flip(a)]. given #35 (T,wt=9): 192 x' @ y' = x @ y. [para(177(a,2),177(a,1))]. given #36 (A,wt=15): 16 x * (y @ z) * u = x * u * (y @ z). [para(6(a,1),1(a,2,2)),rewrite(1(3))]. given #37 (F,wt=9): 222 x' @ y = x @ y'. [para(179(a,1),177(a,1))]. given #38 (F,wt=10): 107 (x * y)' = y' * x'. [para(94(a,1),8(a,1,2)),flip(a)]. given #39 (T,wt=10): 144 x * y @ y' = y @ x. [back_rewrite(87),rewrite(119(5))]. given #40 (T,wt=10): 175 x * y @ x' = x @ y. [back_rewrite(166),rewrite(171(5))]. given #41 (A,wt=12): 27 x' * y * x = y * (y @ x). [para(5(a,1),8(a,1,2)),rewrite(24(2)),flip(a)]. given #42 (F,wt=10): 188 (x @ y) * (x' @ y) = e. [para(177(a,1),113(a,1,1))]. given #43 (F,wt=10): 189 (x @ y) * (x @ y') = e. [para(177(a,2),113(a,1,1)),rewrite(6(4,R))]. given #44 (T,wt=10): 232 x' @ y * x = y @ x. [para(171(a,1),179(a,2))]. given #45 (T,wt=10): 307 x' * y * x @ y = e. [para(27(a,2),146(a,1,1)),rewrite(18(6))]. given #46 (A,wt=12): 29 x' * (y @ z) * x = y @ z. [para(6(a,2),8(a,1,2))]. given #47 (F,wt=10): 315 x @ y' * x * y = e. [para(27(a,2),180(a,1,2)),rewrite(19(6))]. given #48 (F,wt=10): 346 x * y * x' @ y = e. [para(24(a,1),307(a,1,1,1))]. given #49 (T,wt=10): 362 x @ y * x * y' = e. [para(24(a,1),315(a,1,2,1))]. given #50 (T,wt=11): 99 x' * y' @ x * y = e. [back_rewrite(69),rewrite(95(8),3(8)),flip(a)]. given #51 (A,wt=14): 32 x * y' * x' * y = x' @ y. [para(24(a,1),5(a,1,1))]. given #52 (F,wt=9): 403 x * y @ y * x = e. [para(99(a,1),177(a,2)),rewrite(107(5),24(3),24(3))]. given #53 (F,wt=11): 132 x' @ x * y = x' @ y. [back_rewrite(25),rewrite(107(2),1(4),32(5)),flip(a)]. given #54 (T,wt=11): 143 (x @ y) * z * (y @ x) = z. [back_rewrite(28),rewrite(108(2))]. given #55 (T,wt=11): 145 x * y' @ y = y' @ x. [back_rewrite(86),rewrite(119(7))]. given #56 (A,wt=14): 33 x' * y * x * y' = x @ y'. [para(24(a,1),5(a,1,2,1))]. given #57 (F,wt=11): 147 (x @ y) * (y @ x) * z = z. [para(108(a,1),8(a,1,1))]. given #58 (F,wt=11): 150 x @ (y @ z) * u = x @ u. [para(14(a,2),5(a,1,2,2)),rewrite(107(4),108(4),1(8),147(7),5(5)),flip(a)]. given #59 (T,wt=11): 164 x' * y * x @ y' = e. [para(5(a,1),119(a,1,2)),rewrite(19(5)),flip(a)]. given #60 (T,wt=11): 174 x' * y @ x = x' @ y. [back_rewrite(170),rewrite(171(3)),flip(a)]. given #61 (A,wt=21): 37 x * y' * z' * y * z * u = x * (y @ z) * u. [para(9(a,1),1(a,2,2)),rewrite(1(7))]. given #62 (F,wt=11): 190 x @ x' * y = y @ x'. [para(177(a,1),146(a,1))]. given #63 (F,wt=11): 196 x @ y * (z @ u) = x @ y. [para(15(a,2),5(a,1,2,2)),rewrite(107(4),108(3),1(8),153(8),5(5)),flip(a)]. given #64 (T,wt=11): 230 (x @ y) * z @ u = z @ u. [para(14(a,2),171(a,1,1)),rewrite(150(6),225(4),150(6))]. given #65 (T,wt=11): 231 x @ y * x' = y @ x'. [para(171(a,1),177(a,1)),flip(a)]. given #66 (A,wt=13): 40 x' * y * x = y * (x @ y'). [para(3(a,1),9(a,1,2,2,2)),rewrite(24(3),20(3),6(6))]. given #67 (F,wt=11): 238 x * (y @ z) @ u = x @ u. [back_rewrite(75),rewrite(230(3)),flip(a)]. given #68 (F,wt=11): 269 (x @ y') * (y @ x') = e. [para(222(a,1),113(a,1,1))]. given #69 (T,wt=11): 270 (x' @ y) * (y' @ x) = e. [para(222(a,2),113(a,1,1))]. given #70 (T,wt=11): 277 x * y @ y' * x' = e. [para(107(a,1),35(a,1,2))]. given #71 (A,wt=22): 43 x' * y * x * (y @ z) = (x @ y') * z' * y * z. [para(5(a,1),9(a,1,2,2,2)),rewrite(24(3))]. given #72 (F,wt=11): 298 x * y * (y @ x) = y * x. [para(27(a,1),8(a,1,2)),rewrite(24(2))]. given #73 (F,wt=11): 308 (x @ y) * y * x = x * y. [para(146(a,1),27(a,2,2)),rewrite(1(3),8(4),6(4,R)),flip(a)]. given #74 (T,wt=11): 375 x @ y * x' * y' = e. [para(346(a,1),177(a,1)),flip(a)]. given #75 (T,wt=11): 376 x' @ y * x * y' = e. [para(346(a,1),179(a,2))]. given #76 (A,wt=17): 46 x' * y' * x * y * z = z * (x @ y). [para(9(a,2),6(a,1))]. given #77 (F,wt=11): 382 x * y' * x' @ y = e. [para(346(a,1),188(a,1,1)),rewrite(107(5),107(4),24(3),1(5),2(7))]. given #78 (F,wt=11): 383 x * y * x' @ y' = e. [para(346(a,1),189(a,1,1)),rewrite(2(7))]. given #79 (T,wt=11): 397 x * y' @ x' * y = e. [para(24(a,1),99(a,1,1,1))]. given #80 (T,wt=11): 398 x' * y @ x * y' = e. [para(24(a,1),99(a,1,1,2))]. given #81 (A,wt=21): 48 x' * y' * x * (z @ u) * y = (x @ y) * (z @ u). [para(6(a,2),9(a,1,2,2,2))]. given #82 (F,wt=11): 401 x * y @ x' * y' = e. [para(99(a,1),108(a,1,1)),rewrite(21(2)),flip(a)]. given #83 (F,wt=11): 466 x' * y' @ y * x = e. [back_rewrite(338),rewrite(461(7))]. given #84 (T,wt=11): 565 x * y' @ y * x' = e. [para(24(a,1),277(a,1,2,1))]. given #85 (T,wt=11): 566 x' * y @ y' * x = e. [para(24(a,1),277(a,1,2,2))]. given #86 (A,wt=16): 49 x' * y * x * z = y * (y @ x) * z. [para(9(a,1),8(a,1,2)),rewrite(24(2)),flip(a)]. given #87 (F,wt=11): 635 x @ y * z = x @ z * y. [para(308(a,1),150(a,1,2))]. given #88 (F,wt=11): 640 x * y @ z = y * x @ z. [para(308(a,1),230(a,1,1))]. given #89 (T,wt=12): 63 x * (y @ z) * x' = y @ z. [para(6(a,2),34(a,1,2))]. given #90 (T,wt=12): 182 (x @ y) * z = z * (y @ x'). [para(177(a,1),6(a,1,1))]. given #91 (A,wt=17): 51 x' * y * x * z = (x @ y') * y * z. [para(8(a,1),9(a,1,2,2,2)),rewrite(24(3))]. given #92 (F,wt=12): 183 (x @ y') * z = z * (y @ x). [para(177(a,2),6(a,1,1))]. given #93 (F,wt=12): 193 x * (y @ x) = y * x * y'. [back_rewrite(128),rewrite(192(3))]. given #94 (T,wt=12): 216 (x @ y) * z = z * (y' @ x). [para(179(a,1),6(a,1,1))]. given #95 (T,wt=12): 217 (x' @ y) * z = z * (y @ x). [para(179(a,2),6(a,1,1))]. given #96 (A,wt=18): 52 (x' @ y) * z = x * y' * x' * y * z. [para(24(a,1),9(a,1,1)),flip(a)]. given #97 (F,wt=12): 322 (x @ y) * x' * y * x = y. [para(27(a,2),27(a,1,2)),rewrite(108(2),19(7),20(7))]. given #98 (F,wt=12): 323 (x @ y) * (x' @ y) * z = z. [para(188(a,1),1(a,1,1)),rewrite(2(2)),flip(a)]. given #99 (T,wt=12): 326 (x @ y) * z * (x' @ y) = z. [para(188(a,1),14(a,2,2)),rewrite(20(7))]. given #100 (T,wt=12): 327 (x' @ y) * z * (x @ y) = z. [para(188(a,1),15(a,2,2)),rewrite(20(7))]. given #101 (A,wt=18): 53 x' * y * x * y' * z = (x @ y') * z. [para(24(a,1),9(a,1,2,1))]. given #102 (F,wt=12): 329 (x @ y) * (x @ y') * z = z. [para(189(a,1),1(a,1,1)),rewrite(2(2)),flip(a)]. given #103 (F,wt=12): 332 (x @ y) * z * (x @ y') = z. [para(189(a,1),14(a,2,2)),rewrite(20(7))]. given #104 (T,wt=12): 333 (x @ y') * z * (x @ y) = z. [para(189(a,1),15(a,2,2)),rewrite(20(7))]. given #105 (T,wt=12): 377 x * y * x' * y @ y = e. [para(346(a,1),171(a,2)),rewrite(1(4),1(3))]. given #106 (A,wt=14): 55 x' * y' * x = (x @ y) * y'. [para(31(a,1),9(a,1,2,2,2)),rewrite(20(4))]. given #107 (F,wt=12): 456 (x' @ y) * (x @ y) * z = z. [para(177(a,1),147(a,1,2,1))]. given #108 (F,wt=12): 457 (x @ y') * (x @ y) * z = z. [para(177(a,2),147(a,1,1))]. given #109 (T,wt=12): 501 x * (y' @ z) = x * (z @ y). [para(188(a,1),37(a,1,2,2,2,2)),rewrite(108(3),20(4),29(4),19(4),2(6)),flip(a)]. given #110 (T,wt=12): 502 x * (y @ z') = x * (z @ y). [para(189(a,1),37(a,1,2,2,2,2)),rewrite(108(3),20(4),29(4),19(4),2(6)),flip(a)]. given #111 (A,wt=18): 64 x' * y' * x * z = (x @ y) * y' * z. [para(34(a,1),9(a,1,2,2,2))]. given #112 (F,wt=12): 517 x @ y' * z * y = x @ z. [para(27(a,2),196(a,1,2))]. given #113 (F,wt=12): 533 x * y * (x @ y') = y * x. [para(40(a,1),8(a,1,2)),rewrite(24(2))]. given #114 (T,wt=12): 551 x' * y * x @ z = y @ z. [para(27(a,2),238(a,1,1))]. given #115 (T,wt=12): 609 x * y * (x' @ y) = y * x. [para(179(a,2),298(a,1,2,2))]. given #116 (A,wt=18): 76 x' * y * z * x = y * z * (y * z @ x). [para(10(a,1),8(a,1,2)),rewrite(24(3),1(4)),flip(a)]. given #117 (F,wt=12): 627 (x @ y') * x * y = y * x. [para(177(a,2),308(a,1,1))]. given #118 (F,wt=12): 631 (x' @ y) * x * y = y * x. [para(179(a,2),308(a,1,1))]. given #119 (T,wt=12): 777 (x' @ y) * z = (y @ x) * z. [para(49(a,1),9(a,1)),rewrite(154(6))]. given #120 (T,wt=12): 886 x @ y * z * y' = x @ z. [para(8(a,1),635(a,1,2)),rewrite(1(4)),flip(a)]. given #121 (A,wt=24): 110 x' * y' * z * x * y * z' = y * x @ x' * z'. [para(94(a,1),10(a,1,2,2,2)),rewrite(107(2),107(5),107(7),24(5),24(5),1(7),1(8),107(11))]. given #122 (F,wt=12): 893 x * y @ z' = z @ y * x. [para(635(a,1),177(a,2))]. given #123 (F,wt=12): 895 x' @ y * z = z * y @ x. [para(635(a,1),179(a,1))]. given #124 (T,wt=12): 927 x * y * x' @ z = y @ z. [para(8(a,1),640(a,1,1)),rewrite(1(4)),flip(a)]. given #125 (T,wt=12): 962 (x @ y') * z = (y @ x) * z. [para(182(a,2),6(a,2))]. given #126 (A,wt=18): 111 (x @ y * z) * x' * y * z * x = y * z. [para(10(a,1),94(a,1,2,1)),rewrite(108(7),6(7,R),107(9),107(11),24(9),24(9))]. given #127 (F,wt=12): 1088 x * (y @ x) = x * (x @ y'). [para(193(a,2),298(a,2)),rewrite(231(5),1(6),8(5)),flip(a)]. given #128 (F,wt=13): 162 x @ y * z * x = x @ y * z. [para(1(a,1),119(a,1,2))]. given #129 (T,wt=13): 225 x * y * z @ z = x * y @ z. [para(1(a,1),171(a,1,1))]. given #130 (T,wt=13): 244 x * y * x' * y' = x @ y. [para(192(a,1),5(a,2)),rewrite(24(2),24(2))]. given #131 (A,wt=15): 118 x' * y' = (x @ y) * y' * x'. [back_rewrite(95),rewrite(107(3)),flip(a)]. given #132 (F,wt=13): 263 (x @ y') * z = z * (x' @ y). [para(222(a,1),6(a,1,1))]. given #133 (F,wt=13): 264 (x' @ y) * z = z * (x @ y'). [para(222(a,2),6(a,1,1))]. given #134 (T,wt=13): 276 x' * (y @ z) = (y @ z) * x'. [para(6(a,1),107(a,1,1)),rewrite(107(3),108(2),108(6)),flip(a)]. given #135 (T,wt=13): 279 x * y @ z = z @ y' * x'. [para(107(a,1),177(a,1,2)),flip(a)]. given #136 (A,wt=23): 120 x' * y' * z' * x * y * z = y * x @ x' * z. [back_rewrite(84),rewrite(107(2),107(6),24(6),1(7),1(8))]. given #137 (F,wt=13): 281 x' * y' @ z = z @ y * x. [para(107(a,1),179(a,1,1))]. given #138 (F,wt=13): 300 x * (x @ y') = y * x * y'. [para(24(a,1),27(a,1,1)),flip(a)]. given #139 (T,wt=13): 313 x' * y * x = y * (x' @ y). [para(179(a,2),27(a,2,2))]. given #140 (T,wt=13): 319 x * (x' @ y) = y * x * y'. [para(222(a,2),27(a,2,2)),rewrite(24(2)),flip(a)]. given #141 (A,wt=21): 121 x' * y' * z * y * x * z' = y * x @ z'. [back_rewrite(79),rewrite(107(2),1(8))]. given #142 (F,wt=11): 2423 x * x @ y = x @ y * y. [back_rewrite(2226),rewrite(2415(4))]. given #143 (F,wt=12): 2437 x * x @ y' = y * y @ x. [para(2423(a,2),177(a,2))]. given #144 (T,wt=12): 2441 x' @ y * y = y @ x * x. [para(2423(a,1),179(a,2))]. given #145 (T,wt=13): 420 x * y * z @ z * x * y = e. [para(1(a,1),403(a,1,1))]. given #146 (A,wt=23): 122 x * y' * z' * x' * y * z = y * x' @ x * z. [back_rewrite(77),rewrite(107(3),24(2),107(4),1(7),1(8))]. given #147 (F,wt=13): 421 x * y * z @ y * z * x = e. [para(1(a,1),403(a,1,2))]. given #148 (F,wt=13): 438 (x @ y') * z * (y @ x') = z. [para(222(a,1),143(a,1,1))]. given #149 (T,wt=13): 439 (x' @ y) * z * (y' @ x) = z. [para(222(a,2),143(a,1,1))]. given #150 (T,wt=13): 458 (x @ y') * (y @ x') * z = z. [para(222(a,1),147(a,1,1))]. given #151 (A,wt=24): 129 x' * y' * z' * y * x * z * u = (y * x @ z) * u. [back_rewrite(39),rewrite(107(2),1(9))]. given #152 (F,wt=13): 459 (x' @ y) * (y' @ x) * z = z. [para(222(a,2),147(a,1,1))]. given #153 (F,wt=13): 560 x * (y' @ z) = x * (y @ z'). [para(269(a,1),37(a,1,2,2,2,2)),rewrite(108(4),20(5),29(5),19(6),2(7))]. given #154 (T,wt=13): 607 x' * y * (x @ y) = y * x'. [para(177(a,1),298(a,1,2,2))]. given #155 (T,wt=13): 608 x * y' * (x @ y) = y' * x. [para(179(a,1),298(a,1,2,2))]. given #156 (A,wt=24): 130 x' * y' * z' * x * z * y * u = (x @ z * y) * u. [back_rewrite(38),rewrite(107(3),1(8))]. given #157 (F,wt=13): 626 (x @ y) * x' * y = y * x'. [para(177(a,1),308(a,1,1))]. given #158 (F,wt=13): 630 x' * y = (y @ x) * y * x'. [para(179(a,1),308(a,1,1)),flip(a)]. given #159 (T,wt=12): 3080 x * (y @ x) * y * x' = y. [para(630(a,1),8(a,1,2)),rewrite(24(2))]. given #160 (T,wt=13): 775 x' * y = y * (y @ x) * x'. [para(31(a,1),49(a,1,2,2)),rewrite(20(3))]. given #161 (A,wt=20): 133 x' * y' * z' * y * x * z = y * x @ z. [back_rewrite(10),rewrite(107(2),1(8))]. given #162 (F,wt=13): 831 x @ y * x * z = x @ y * z. [para(49(a,1),132(a,1,2)),rewrite(24(2),461(4),24(4)),flip(a)]. given #163 (F,wt=13): 890 (x @ y * z) * (z * y @ x) = e. [para(635(a,1),113(a,1,1))]. given #164 (T,wt=13): 891 (x * y @ z) * (z @ y * x) = e. [para(635(a,1),113(a,1,2))]. given #165 (T,wt=13): 896 x' * y' @ z = z @ x * y. [para(635(a,1),179(a,2)),rewrite(107(2))]. given #166 (A,wt=19): 148 (x @ y) * z * u * v = z * u * (x @ y) * v. [para(14(a,2),1(a,1)),rewrite(1(3))]. given #167 (F,wt=13): 932 x * y @ z = z @ x' * y'. [para(640(a,1),177(a,2)),rewrite(107(2)),flip(a)]. given #168 (F,wt=13): 1041 (x' @ y) * z = (x @ y') * z. [para(51(a,1),49(a,1,2)),rewrite(154(6),154(9)),flip(a)]. given #169 (T,wt=13): 1338 x * x * y * y @ x * y = e. [para(8(a,1),377(a,1,1,2,2)),rewrite(1(2))]. given #170 (T,wt=13): 1966 x * y * z @ y = x * z @ y. [para(298(a,1),225(a,1,1,2)),rewrite(196(5),196(7))]. given #171 (A,wt=19): 149 x * (y @ z) * u * v = x * u * (y @ z) * v. [para(14(a,1),1(a,2,2)),rewrite(1(4))]. given #172 (F,wt=13): 2156 x * y' @ z = z @ y * x'. [para(24(a,1),279(a,2,2,1))]. given #173 (F,wt=13): 2157 x' * y @ z = z @ y' * x. [para(24(a,1),279(a,2,2,2))]. given #174 (T,wt=13): 2395 (x @ y) * (z @ y) = x * z @ y. [para(64(a,1),121(a,1,2)),rewrite(24(5),151(7),24(6))]. given #175 (T,wt=13): 2436 x @ y' * y' = y @ x * x. [para(2423(a,1),177(a,1))]. given #176 (A,wt=21): 151 x' * (y @ z) * u' * x * u = (y @ z) * (x @ u). [para(5(a,1),14(a,1,2)),flip(a)]. given #177 (F,wt=13): 2440 x' * x' @ y = y * y @ x. [para(2423(a,2),179(a,1))]. given #178 (F,wt=13): 2520 x * x @ y * x = x @ y * y. [para(2423(a,2),162(a,1)),rewrite(1(5),831(6))]. given #179 (T,wt=13): 2521 x * y @ y * y = x * x @ y. [para(2423(a,1),225(a,1)),rewrite(1(5),1966(6))]. given #180 (T,wt=13): 2547 x' @ y * y = x * x @ y'. [para(2437(a,2),179(a,2))]. given #181 (A,wt=19): 152 (x @ y) * (z @ u) * v = v * (x @ y) * (z @ u). [para(6(a,2),14(a,1,2))]. given #182 (F,wt=13): 2649 x * y * z @ y * x * z = e. [para(298(a,1),420(a,1,1,2)),rewrite(1(6),461(7))]. given #183 (F,wt=13): 2856 x' * y @ z = z @ x * y'. [back_rewrite(2413),rewrite(2853(8))]. given #184 (T,wt=13): 2857 x * y' @ z = z @ x' * y. [back_rewrite(2412),rewrite(2853(8))]. given #185 (T,wt=13): 3007 (x @ y) * (x @ z) = x @ y * z. [para(43(a,1),130(a,1,2,2,2)),rewrite(24(2),151(9),2003(5),34(5),232(5)),flip(a)]. given #186 (A,wt=15): 153 (x @ y) * z * (y @ x) * u = z * u. [para(14(a,1),8(a,1,2)),rewrite(108(2))]. given #187 (F,wt=13): 3250 (x @ y) * (y @ x * z) = y @ z. [para(49(a,2),133(a,1,2,2,2)),rewrite(108(2),275(9),238(7))]. given #188 (F,wt=13): 3599 x * y * z @ z * y * x = e. [back_rewrite(2675),rewrite(3453(8))]. given #189 (T,wt=13): 4072 (x @ y) * (y * z @ x) = z @ x. [para(2395(a,1),8(a,1,2)),rewrite(108(2))]. given #190 (T,wt=13): 4091 (x @ y) * (z * y @ x) = z @ x. [para(2395(a,1),27(a,1,2)),rewrite(108(2),19(8),20(7))]. given #191 (A,wt=16): 154 x' * (y @ z) * x * u = (y @ z) * u. [para(14(a,2),8(a,1,2))]. given #192 (F,wt=13): 4461 x * x @ y * x = x * x @ y. [para(2520(a,2),5(a,2)),rewrite(107(3),1(7),120(8),2424(4)),flip(a)]. given #193 (F,wt=13): 4466 x * y @ x * x = y @ x * x. [para(2520(a,2),171(a,1)),rewrite(1(5),1(4),225(9),934(5))]. given #194 (T,wt=13): 4501 x * x @ x * y = x * x @ y. [para(2521(a,2),119(a,1)),rewrite(1(8),1(7),162(9),892(5))]. given #195 (T,wt=13): 4512 x * y @ y * y = x @ y * y. [para(2521(a,1),29(a,1,2,1)),rewrite(4070(4),359(6),3007(3)),flip(a)]. given #196 (A,wt=25): 155 x' * y' * x * (z @ u) * y * v = (x @ y) * (z @ u) * v. [para(14(a,2),9(a,1,2,2,2))]. given #197 (F,wt=13): 4607 x * y * z @ x * z * y = e. [para(308(a,1),2649(a,1,1,2)),rewrite(150(7))]. given #198 (F,wt=13): 4852 (x @ y) * (y @ z * x) = y @ z. [para(3007(a,1),27(a,1,2)),rewrite(108(2),19(8),20(7))]. given #199 (T,wt=14): 285 x' * y' @ z = y * x @ z'. [para(107(a,1),222(a,1,1))]. given #200 (T,wt=14): 286 x' @ y * z = x @ z' * y'. [para(107(a,1),222(a,2,2))]. given #201 (A,wt=21): 156 x' * y' * x * y * z * u = z * (x @ y) * u. [para(14(a,1),9(a,2))]. given #202 (F,wt=14): 287 x * y * z @ z' = z @ x * y. [para(1(a,1),144(a,1,1))]. given #203 (F,wt=14): 297 (x @ y) * y' * x' * y = x'. [para(5(a,1),27(a,1,2)),rewrite(107(4),107(2),24(5),1(4),6(6,R),226(12),20(9))]. given #204 (T,wt=14): 312 x' * (y @ x) = y' * x' * y. [para(179(a,1),27(a,2,2)),flip(a)]. given #205 (T,wt=14): 316 x' * (x @ y) = y * x' * y'. [para(192(a,1),27(a,2,2)),rewrite(24(2)),flip(a)]. given #206 (A,wt=25): 157 x' * (y @ z) * u' * x * u * v = (y @ z) * (x @ u) * v. [para(9(a,1),14(a,1,2)),flip(a)]. given #207 (F,wt=14): 335 x' @ y * z * x = y * z @ x. [para(1(a,1),232(a,1,2))]. given #208 (F,wt=14): 544 x' * (y @ x) = x' * (x @ y'). [para(40(a,1),27(a,1,2)),rewrite(107(2),1(7),8(6),232(8)),flip(a)]. given #209 (T,wt=14): 612 x * y' * (y @ x') = y' * x. [para(222(a,1),298(a,1,2,2))]. given #210 (T,wt=14): 613 x' * y * (y' @ x) = y * x'. [para(222(a,2),298(a,1,2,2))]. given #211 (A,wt=25): 158 (x @ y) * z' * u' * z * u * v = (z @ u) * (x @ y) * v. [para(9(a,2),14(a,1,2))]. given #212 (F,wt=14): 633 x' * y = (x @ y') * y * x'. [para(222(a,1),308(a,1,1)),flip(a)]. given #213 (F,wt=14): 634 (x' @ y) * y' * x = x * y'. [para(222(a,2),308(a,1,1))]. given #214 (T,wt=14): 770 x' * y' * x * (y @ x) = y'. [para(3(a,1),49(a,1,2)),rewrite(20(3),107(3),107(6),145(8),192(7),6(6),1(7)),flip(a)]. given #215 (T,wt=14): 898 x' @ y' * z' = x @ y * z. [para(635(a,1),192(a,2)),rewrite(107(3))]. given #216 (A,wt=21): 159 (x @ y) * z * u = z * x' * y' * x * y * u. [para(9(a,2),14(a,2,2))]. given #217 (F,wt=14): 900 x' @ y * z = x @ y' * z'. [para(635(a,1),222(a,1)),rewrite(107(5))]. given #218 (F,wt=14): 935 x' * y' @ z' = x * y @ z. [para(640(a,1),192(a,2)),rewrite(107(2))]. given #219 (T,wt=14): 937 x' * y' @ z = x * y @ z'. [para(640(a,1),222(a,2)),rewrite(107(2))]. given #220 (T,wt=14): 973 x' * (y @ z) = (z' @ y) * x'. [para(182(a,1),107(a,1,1)),rewrite(107(4),108(3),108(7)),flip(a)]. given #221 (A,wt=16): 160 x * (y @ z) * x' * u = (y @ z) * u. [para(14(a,2),34(a,1,2))]. given #222 (F,wt=14): 1057 x' * (y' @ z) = (z @ y) * x'. [para(183(a,1),107(a,1,1)),rewrite(107(3),108(2),108(7)),flip(a)]. given #223 (F,wt=14): 1081 (x @ y) * x' = y * x' * y'. [para(193(a,1),107(a,1,1)),rewrite(107(4),107(3),24(2),1(4),108(6)),flip(a)]. given #224 (T,wt=14): 1110 x' * (y @ z) = (z @ y') * x'. [para(216(a,1),107(a,1,1)),rewrite(107(4),108(3),108(7)),flip(a)]. given #225 (T,wt=14): 1140 x' * (y @ z') = (z @ y) * x'. [para(217(a,1),107(a,1,1)),rewrite(107(3),108(2),108(7)),flip(a)]. given #226 (A,wt=23): 161 (x @ y) * (z @ u) * v * w = v * (x @ y) * (z @ u) * w. [para(14(a,2),14(a,1,2))]. given #227 (F,wt=14): 1216 (x @ y) * x * y' * x' = y'. [para(192(a,1),322(a,1,1)),rewrite(24(3))]. given #228 (F,wt=14): 1490 x * y' * x' * (x @ y) = y'. [para(64(a,2),327(a,1)),rewrite(24(2))]. given #229 (T,wt=14): 1554 x' * y = y * (x @ y') * x'. [para(182(a,2),609(a,1,2)),flip(a)]. given #230 (T,wt=14): 2003 (x @ y') * (y @ z) = y @ x * z. [para(244(a,1),51(a,2,2)),rewrite(1747(8)),flip(a)]. given #231 (A,wt=15): 176 x * y * z @ x * y = z @ x * y. [para(1(a,1),146(a,1,1))]. given #232 (F,wt=14): 2016 x * (x @ y) * y' * x' = y'. [para(118(a,1),8(a,1,2)),rewrite(24(2))]. given #233 (F,wt=14): 2210 x * y' @ y * y = x @ y * y. [para(27(a,1),120(a,1,2,2,2)),rewrite(24(2),2204(7),24(6)),flip(a)]. given #234 (T,wt=14): 2217 (x' @ y) * (x @ y * z) = x @ z. [para(40(a,2),120(a,2,1)),rewrite(108(3),670(10),2003(6),108(11),150(12),551(9))]. given #235 (T,wt=14): 2223 (x @ y') * (x * z @ y) = z @ y. [para(49(a,2),120(a,1,2,2)),rewrite(108(3),133(10),108(11),6(11),196(12),238(9))]. given #236 (A,wt=17): 184 x' * y * x * y' * z = (y @ x) * z. [para(177(a,1),9(a,2,1)),rewrite(24(3))]. given #237 (F,wt=14): 2415 x * x @ x' * y = x * x @ y. [back_rewrite(1749),rewrite(2395(7))]. given #238 (F,wt=14): 2421 (x @ y) * (y' @ z) = x * z @ y. [back_rewrite(2006),rewrite(2414(6)),flip(a)]. given #239 (T,wt=14): 2424 x * y @ y' * x = y * y @ x. [back_rewrite(2221),rewrite(2415(8))]. given #240 (T,wt=14): 2450 x' @ y * y = x' * x' @ y. [para(2423(a,2),132(a,2)),rewrite(132(4))]. given #241 (A,wt=18): 185 x' * y' * x * y * z = (y @ x') * z. [para(177(a,2),9(a,2,1))]. given #242 (F,wt=14): 2585 x * y' @ y * x = x @ y * y. [para(2441(a,1),5(a,2)),rewrite(24(2),107(2),1(7),122(8))]. given #243 (F,wt=14): 2816 (x' @ y) * (y @ z) = y @ x * z. [para(43(a,1),129(a,1,2,2,2)),rewrite(24(3),34(10),151(8),2003(4),174(5)),flip(a)]. given #244 (T,wt=14): 2853 x @ y * x' * z = x @ y * z. [back_rewrite(2261),rewrite(2816(8))]. given #245 (T,wt=14): 2860 x @ y' * z = (y @ x) * (x @ z). [back_rewrite(2259),rewrite(2853(5))]. given #246 (A,wt=16): 186 (x @ y) * z * u = z * (y @ x') * u. [para(177(a,1),14(a,1,1))]. given #247 (F,wt=14): 2862 x @ y' * z = (x @ z) * (y @ x). [back_rewrite(2257),rewrite(2853(5))]. given #248 (F,wt=14): 3249 (x' @ y) * (z @ x) = y * z @ x. [para(49(a,1),133(a,1,2)),rewrite(670(8))]. given #249 (T,wt=14): 3875 x * y' @ z' = y * x' @ z. [para(2156(a,2),5(a,2)),rewrite(107(4),24(3),1(7),1711(8))]. given #250 (T,wt=14): 3884 x' @ y * z' = x @ z * y'. [para(2156(a,1),177(a,1))]. given #251 (A,wt=16): 187 (x @ y') * z * u = z * (y @ x) * u. [para(177(a,2),14(a,1,1))]. given #252 (F,wt=14): 3933 x' @ y * z' = x @ y' * z. [para(2156(a,1),893(a,1))]. given #253 (F,wt=14): 3934 x' * y @ z' = x * y' @ z. [para(2156(a,2),893(a,2))]. given #254 (T,wt=14): 3935 x' * y @ z = x * y' @ z'. [para(2156(a,2),895(a,1)),flip(a)]. given #255 (T,wt=14): 3936 x' @ y' * z = x @ y * z'. [para(2156(a,1),895(a,2))]. given #256 (A,wt=19): 194 (x @ y) * z * u * v = z * u * v * (x @ y). [para(15(a,2),1(a,1)),rewrite(1(3))]. given #257 (F,wt=14): 3971 x' * y @ z' = y' * x @ z. [para(2157(a,2),5(a,2)),rewrite(107(4),24(4),1(7),2200(8))]. given #258 (F,wt=14): 3980 x' @ y' * z = x @ z' * y. [para(2157(a,1),177(a,1))]. given #259 (T,wt=14): 4078 (x @ y') * (z @ x) = y * z @ x. [para(177(a,2),2395(a,1,1))]. given #260 (T,wt=14): 4079 (x @ y) * (y @ z') = x * z @ y. [para(177(a,2),2395(a,1,2))]. given #261 (A,wt=19): 195 x * (y @ z) * u * v = x * u * v * (y @ z). [para(15(a,1),1(a,2,2)),rewrite(1(4))]. given #262 (F,wt=14): 4082 x' * y @ z = (z @ x) * (y @ z). [para(179(a,1),2395(a,1,1)),flip(a)]. given #263 (F,wt=14): 4083 x * y' @ z = (x @ z) * (z @ y). [para(179(a,1),2395(a,1,2)),flip(a)]. given #264 (T,wt=14): 4109 x * y' @ z = (z @ y) * (x @ z). [para(2395(a,1),216(a,2)),flip(a)]. given #265 (T,wt=14): 4110 x' * y @ z = (y @ z) * (z @ x). [para(2395(a,1),217(a,1))]. given #266 (A,wt=19): 197 (x @ y) * z * (u @ v) = (u @ v) * z * (x @ y). [para(6(a,1),15(a,1,2))]. given #267 (F,wt=14): 4113 (x @ y') * (z * x @ y) = z @ y. [para(2395(a,1),333(a,1,2))]. given #268 (F,wt=14): 4838 x @ y * z' = (x @ y) * (z @ x). [para(177(a,1),3007(a,1,2)),flip(a)]. given #269 (T,wt=14): 4841 (x @ y) * (z' @ x) = x @ y * z. [para(179(a,2),3007(a,1,2))]. given #270 (T,wt=14): 4865 x @ y * z' = (z @ x) * (x @ y). [para(3007(a,1),182(a,2)),flip(a)]. given #271 (A,wt=19): 198 (x @ y) * (z @ u) * v = v * (z @ u) * (x @ y). [para(6(a,2),15(a,1,2))]. given #272 (F,wt=14): 4867 (x' @ y) * (x @ z * y) = x @ z. [para(3007(a,1),327(a,1,2))]. given #273 (F,wt=14): 5322 x' * y @ x * x = y @ x * x. [para(34(a,1),4466(a,1,1)),flip(a)]. given #274 (T,wt=14): 5343 x * x @ y * x' = x * x @ y. [para(193(a,2),4501(a,1,2)),rewrite(196(4)),flip(a)]. given #275 (T,wt=14): 6385 x * y' @ x * y = x @ y * y. [para(2210(a,1),180(a,2)),rewrite(1(6),8(5))]. given #276 (A,wt=15): 199 (x @ y) * z * u * (y @ x) = z * u. [para(15(a,1),8(a,1,2)),rewrite(108(2))]. given #277 (F,wt=14): 6511 x * y @ x' * y = x * x @ y. [para(2415(a,1),171(a,2)),rewrite(1(4),34(3))]. given #278 (F,wt=14): 6575 x' * y @ y * x = y @ x * x. [para(2424(a,1),108(a,1,1)),rewrite(108(3)),flip(a)]. given #279 (T,wt=14): 6579 x * y @ y * x' = x * x @ y. [para(298(a,1),2424(a,1,2)),rewrite(1(4),6(3),533(4),196(9))]. given #280 (T,wt=14): 6581 x * y @ x * y' = y * y @ x. [para(2424(a,1),635(a,1)),flip(a)]. given #281 (A,wt=25): 200 x' * y' * x * (z @ u) * y * v = (x @ y) * v * (z @ u). [para(15(a,2),9(a,1,2,2,2))]. given #282 (F,wt=14): 6676 x' * y @ x * y = y @ x * x. [para(2585(a,1),640(a,1)),flip(a)]. given #283 (F,wt=15): 242 x * y @ x * y * z = x * y @ z. [para(1(a,1),180(a,1,2))]. given #284 (T,wt=15): 299 x' * (x' @ y) = y' * x' * y. [para(8(a,1),27(a,1,2)),rewrite(107(2),1(4),132(8)),flip(a)]. given #285 (T,wt=15): 318 x' * (x @ y') = y' * x' * y. [para(222(a,1),27(a,2,2)),flip(a)]. given #286 (A,wt=21): 202 x' * y' * x * y * z * u = z * u * (x @ y). [para(15(a,1),9(a,2))]. given #287 (F,wt=15): 440 x * y * z' @ z = z' @ x * y. [para(1(a,1),145(a,1,1))]. given #288 (F,wt=15): 453 (x @ y') * y * x' * y' = x'. [para(33(a,1),27(a,1,2)),rewrite(107(4),107(3),24(2),1(4),6(7,R),376(13),20(10))]. given #289 (T,wt=15): 461 x @ y * (z @ u) * v = x @ y * v. [para(14(a,1),150(a,1,2))]. given #290 (T,wt=15): 462 x @ y * z * (u @ v) = x @ y * z. [para(15(a,1),150(a,1,2))]. given #291 (A,wt=25): 203 x' * y' * x * y * z * (u @ v) = (u @ v) * (x @ y) * z. [para(15(a,2),9(a,2))]. given #292 (F,wt=15): 521 x * (y @ z) * u @ v = x * u @ v. [para(14(a,1),230(a,1,1))]. given #293 (F,wt=15): 522 x * y * (z @ u) @ v = x * y @ v. [para(15(a,1),230(a,1,1))]. given #294 (T,wt=15): 526 x @ y * z * x' = y * z @ x'. [para(1(a,1),231(a,1,2))]. given #295 (T,wt=15): 600 x' * y' * x = (y @ x') * y'. [para(270(a,1),43(a,1,2,2)),rewrite(108(3),20(5),24(8),18(7),2(10)),flip(a)]. given #296 (A,wt=25): 204 (x @ y) * z' * u' * z * u * v = (z @ u) * v * (x @ y). [para(9(a,2),15(a,1,2))]. given #297 (F,wt=15): 601 x * y * (y @ x) * z = y * x * z. [para(298(a,1),1(a,1,1)),rewrite(1(2),1(5)),flip(a)]. given #298 (F,wt=15): 611 x' * y' = y' * x' * (x @ y). [para(192(a,1),298(a,1,2,2)),flip(a)]. given #299 (T,wt=15): 615 x * y * y * x = y * x * x * y. [para(403(a,1),298(a,1,2,2)),rewrite(20(4),1(3),1(6))]. given #300 (T,wt=15): 619 (x @ y) * y * x * z = x * y * z. [para(308(a,1),1(a,1,1)),rewrite(1(2),1(5)),flip(a)]. given #301 (A,wt=25): 205 (x @ y) * z * (u @ v) = z * u' * v' * u * v * (x @ y). [para(9(a,2),15(a,2,2))]. given #302 (F,wt=15): 625 (x @ y) * z * y * x = z * x * y. [para(308(a,1),14(a,2,2))]. ============================== PROOF ================================= % Proof 1 at 4.25 (+ 0.05) seconds: E. % Length of proof is 29. % Level of proof is 13. % Maximum clause weight is 19. % Given clauses 302. 1 (x * y) * z = x * y * z. [assumption]. 2 e * x = x. [assumption]. 3 x' * x = e. [assumption]. 4 x @ y = x' * y' * x * y. [assumption]. 5 x' * y' * x * y = x @ y. [copy(4),flip(a)]. 6 (x @ y) * z = z * (x @ y). [assumption]. 7 A * B * C * B * A != B * A * C * A * B # answer(E). [assumption]. 8 x' * x * y = y. [para(3(a,1),1(a,1,1)),rewrite(2(2)),flip(a)]. 9 x' * y' * x * y * z = (x @ y) * z. [para(5(a,1),1(a,1,1)),rewrite(1(7),1(6)),flip(a)]. 10 (x * y)' * z' * x * y * z = x * y @ z. [para(1(a,1),5(a,1,2,2))]. 11 e @ x = e. [para(2(a,1),5(a,1,2,2)),rewrite(3(4),3(4)),flip(a)]. 14 (x @ y) * z * u = z * (x @ y) * u. [para(6(a,1),1(a,1,1)),rewrite(1(3)),flip(a)]. 20 x * e = x. [para(11(a,1),6(a,1,1)),rewrite(2(2),11(2)),flip(a)]. 24 x'' = x. [para(3(a,1),8(a,1,2)),rewrite(20(4))]. 27 x' * y * x = y * (y @ x). [para(5(a,1),8(a,1,2)),rewrite(24(2)),flip(a)]. 31 x * x' = e. [para(24(a,1),3(a,1,1))]. 36 x * y * (x * y)' = e. [para(31(a,1),1(a,1)),flip(a)]. 78 (x * y)' * y * x = x * y @ x. [para(8(a,1),10(a,1,2))]. 82 x * y @ x = y @ x * y. [para(9(a,1),10(a,1,2)),rewrite(8(3),6(4),8(5),8(5))]. 88 (x * y)' * y * x = y @ x * y. [back_rewrite(78),rewrite(82(6))]. 94 x * (y * x)' = y'. [para(36(a,1),8(a,1,2)),rewrite(20(3)),flip(a)]. 107 (x * y)' = y' * x'. [para(94(a,1),8(a,1,2)),flip(a)]. 119 x @ y * x = x @ y. [back_rewrite(88),rewrite(107(2),1(5),5(5)),flip(a)]. 146 x * y @ x = y @ x. [back_rewrite(82),rewrite(119(4))]. 298 x * y * (y @ x) = y * x. [para(27(a,1),8(a,1,2)),rewrite(24(2))]. 308 (x @ y) * y * x = x * y. [para(146(a,1),27(a,2,2)),rewrite(1(3),8(4),6(4,R)),flip(a)]. 601 x * y * (y @ x) * z = y * x * z. [para(298(a,1),1(a,1,1)),rewrite(1(2),1(5)),flip(a)]. 625 (x @ y) * z * y * x = z * x * y. [para(308(a,1),14(a,2,2))]. 9544 $F # answer(E). [para(625(a,2),7(a,1,2,2)),rewrite(601(13)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=302. Generated=152701. Kept=9542. proofs=1. Usable=271. Sos=6493. Demods=1784. Limbo=3, Disabled=2781. Hints=0. Weight_deleted=17529. Literals_deleted=0. Forward_subsumed=125629. Back_subsumed=332. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=3379 (5 lex), Back_demodulated=2443. Back_unit_deleted=0. Demod_attempts=2675637. Demod_rewrites=539420. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=7.34. User_CPU=4.25, System_CPU=0.05, Wall_clock=4. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3875 exit (max_proofs) Wed Nov 22 11:24:28 2006