============================== Prover9 =============================== Prover9 (32) version 2009-02A, February 2009. Process 11618 was started by mccune on cleo, Wed Feb 25 09:33:12 2009 The command was "/home/mccune/bin/prover9 -f gt.in NE.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file gt.in assign(max_seconds,30). 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: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ e, A, B, C, *, @, ' ]). After inverse_order: Function symbol precedence: function_order([ e, A, B, C, *, ', @ ]). Folding symbols: @/2. After fold_eq: Function symbol precedence: function_order([ e, A, B, C, @, *, ' ]). Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). kept: 1 (x * y) * z = x * y * z. [assumption]. kept: 2 e * x = x. [assumption]. kept: 3 x' * x = e. [assumption]. 4 x @ y = x' * y' * x * y. [assumption]. kept: 5 x' * y' * x * y = x @ y. [copy(4),flip(a)]. kept: 6 (x @ y) * z = z * (x @ y). [assumption]. kept: 7 A * B * C * B * A != B * A * C * A * B # answer(E). [assumption]. ============================== 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.01 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 (A,wt=8): 8 x' * x * y = y. [para(3(a,1),1(a,1,1)),rewrite([2(2)]),flip(a)]. given #8 (T,wt=5): 11 e @ x = e. [para(2(a,1),5(a,1,2,2)),rewrite([3(4),3(4)]),flip(a)]. given #9 (T,wt=4): 33 e' = e. [para(11(a,1),5(a,2)),rewrite([2(5),3(4),31(4)])]. given #10 (T,wt=5): 24 x @ x = e. [para(8(a,1),5(a,1,2)),rewrite([3(2)]),flip(a)]. given #11 (T,wt=5): 31 x * e = x. [back_rewrite(22),rewrite([28(4)])]. given #12 (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 #13 (T,wt=5): 34 x @ e = e. [para(33(a,1),5(a,1,2,1)),rewrite([31(4),2(3),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=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 #16 (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 #17 (A,wt=19): 10 (x * y)' * z' * x * y * z = x * y @ z. [para(1(a,1),5(a,1,2,2))]. given #18 (T,wt=7): 72 x @ x * x = e. [para(10(a,1),10(a,1,2)),rewrite([3(2),33(2),70(3),2(4),3(4),11(5)])]. given #19 (T,wt=9): 28 x'' * y = x * y. [para(8(a,1),8(a,1,2))]. given #20 (T,wt=5): 82 x'' = x. [para(28(a,1),31(a,1)),rewrite([31(2)]),flip(a)]. given #21 (T,wt=6): 76 x * x' = e. [para(28(a,1),3(a,1))]. given #22 (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 #23 (T,wt=6): 86 x @ x' = e. [para(82(a,1),12(a,1,1))]. given #24 (T,wt=8): 81 x * x' * y = y. [para(28(a,1),8(a,1))]. given #25 (T,wt=10): 87 x * y * (x * y)' = e. [para(76(a,1),1(a,1)),flip(a)]. given #26 (T,wt=9): 122 x * (y * x)' = y'. [para(87(a,1),8(a,1,2)),rewrite([31(3)]),flip(a)]. given #27 (A,wt=15): 15 x * (y @ z) * u = x * u * (y @ z). [para(6(a,1),1(a,2,2)),rewrite([1(3)])]. given #28 (T,wt=8): 138 (x @ y)' = y @ x. [para(9(a,2),122(a,1,2,1)),rewrite([137(7),137(5),137(3),137(2),1(5),82(7),1(6),1(5),82(8),1(7),1(6),1(5),5(6),81(4)]),flip(a)]. given #29 (T,wt=9): 143 (x @ y) * (y @ x) = e. [back_rewrite(127),rewrite([137(5),137(4),138(4),1(6),81(7),109(5)])]. given #30 (T,wt=9): 153 x @ y * x = x @ y. [back_rewrite(74),rewrite([137(2),1(5),5(5)]),flip(a)]. given #31 (T,wt=9): 174 x * y @ x = y @ x. [back_rewrite(70),rewrite([153(4)])]. given #32 (A,wt=15): 16 (x @ y) * z * u = z * u * (x @ y). [para(6(a,1),1(a,2)),rewrite([1(3),1(6)])]. given #33 (T,wt=8): 216 x @ y' = y @ x. [para(8(a,1),174(a,1,1)),rewrite([214(5)])]. given #34 (T,wt=8): 218 x' @ y = y @ x. [para(81(a,1),174(a,1,1)),rewrite([213(4)]),flip(a)]. given #35 (T,wt=9): 212 x * y @ y = x @ y. [para(153(a,1),138(a,1,1)),rewrite([138(2)]),flip(a)]. given #36 (T,wt=9): 219 x @ x * y = x @ y. [para(174(a,1),138(a,1,1)),rewrite([138(2)]),flip(a)]. given #37 (A,wt=12): 27 x' * (y @ z) * x = y @ z. [para(6(a,2),8(a,1,2))]. given #38 (T,wt=9): 253 x' @ y' = x @ y. [para(216(a,1),216(a,2))]. given #39 (T,wt=9): 265 x' @ y = x @ y'. [para(218(a,1),216(a,1))]. given #40 (T,wt=10): 137 (x * y)' = y' * x'. [para(122(a,1),8(a,1,2)),flip(a)]. given #41 (T,wt=10): 172 x * y @ y' = y @ x. [back_rewrite(90),rewrite([153(5)])]. given #42 (A,wt=12): 29 x' * y * x = y * (y @ x). [back_rewrite(25),rewrite([28(4)]),flip(a)]. given #43 (T,wt=10): 214 x * y @ x' = x @ y. [back_rewrite(205),rewrite([212(5)])]. given #44 (T,wt=10): 247 (x @ y) * (x' @ y) = e. [para(216(a,1),143(a,1,1))]. given #45 (T,wt=10): 248 (x @ y) * (x @ y') = e. [para(216(a,2),143(a,1,1)),rewrite([6(4,R)])]. given #46 (T,wt=10): 272 x' @ y * x = y @ x. [para(212(a,1),218(a,2))]. given #47 (A,wt=21): 35 x * y' * z' * y * z * u = x * (y @ z) * u. [para(9(a,1),1(a,2,2)),rewrite([1(7)])]. given #48 (T,wt=10): 324 x' * y * x @ y = e. [para(29(a,2),174(a,1,1)),rewrite([18(6)])]. given #49 (T,wt=10): 332 x @ y' * x * y = e. [para(29(a,2),219(a,1,2)),rewrite([19(6)])]. given #50 (T,wt=10): 397 x * y * x' @ y = e. [para(82(a,1),324(a,1,1,1))]. given #51 (T,wt=10): 412 x @ y * x * y' = e. [para(82(a,1),332(a,1,2,1))]. given #52 (A,wt=13): 38 x' * y * x = y * (x @ y'). [para(3(a,1),9(a,1,2,2,2)),rewrite([31(5),28(4),6(6)])]. given #53 (T,wt=11): 129 x' * y' @ x * y = e. [back_rewrite(59),rewrite([123(8),3(8)]),flip(a)]. given #54 (T,wt=9): 471 x * y @ y * x = e. [para(129(a,1),216(a,2)),rewrite([137(5),82(3),82(3)])]. given #55 (T,wt=11): 163 x' @ x * y = x' @ y. [back_rewrite(30),rewrite([137(2),1(4),79(5)]),flip(a)]. given #56 (T,wt=11): 168 (x @ y) * z * (y @ x) = z. [back_rewrite(110),rewrite([138(3)])]. given #57 (A,wt=22): 41 x' * y * x * (y @ z) = (x @ y') * z' * y * z. [para(5(a,1),9(a,1,2,2,2)),rewrite([28(6)])]. given #58 (T,wt=11): 173 x * y' @ y = y' @ x. [back_rewrite(73),rewrite([153(7)])]. given #59 (T,wt=11): 190 x @ (y @ z) * u = x @ u. [back_rewrite(151),rewrite([187(8),5(5)]),flip(a)]. given #60 (T,wt=11): 191 (x @ y) * z @ u = z @ u. [back_rewrite(150),rewrite([187(9),5(5)]),flip(a)]. given #61 (T,wt=11): 197 x * (y @ z) @ u = x @ u. [back_rewrite(63),rewrite([191(3)]),flip(a)]. given #62 (A,wt=17): 44 x' * y' * x * y * z = z * (x @ y). [para(9(a,2),6(a,1))]. given #63 (T,wt=11): 198 x @ y * (z @ u) = x @ y. [back_rewrite(178),rewrite([197(3)]),flip(a)]. given #64 (T,wt=11): 201 (x @ y) * (y @ x) * z = z. [para(138(a,1),8(a,1,1))]. given #65 (T,wt=11): 213 x' * y @ x = x' @ y. [back_rewrite(210),rewrite([212(3)]),flip(a)]. given #66 (T,wt=11): 249 x @ x' * y = y @ x'. [para(216(a,1),174(a,1))]. given #67 (A,wt=21): 46 x' * y' * x * (z @ u) * y = (x @ y) * (z @ u). [para(6(a,2),9(a,1,2,2,2))]. given #68 (T,wt=11): 271 x @ y * x' = y @ x'. [para(212(a,1),216(a,1)),flip(a)]. given #69 (T,wt=11): 290 (x @ y') * (y @ x') = e. [para(265(a,1),143(a,1,1))]. given #70 (T,wt=11): 291 (x' @ y) * (y' @ x) = e. [para(265(a,2),143(a,1,1))]. given #71 (T,wt=11): 297 x * y @ y' * x' = e. [para(137(a,1),86(a,1,2))]. given #72 (A,wt=16): 47 x' * y * x * z = y * (y @ x) * z. [para(9(a,1),8(a,1,2)),rewrite([28(5)]),flip(a)]. given #73 (T,wt=11): 315 x * y * (y @ x) = y * x. [para(29(a,1),8(a,1,2)),rewrite([82(2)])]. given #74 (T,wt=11): 325 (x @ y) * y * x = x * y. [para(174(a,1),29(a,2,2)),rewrite([1(3),8(4),6(4,R)]),flip(a)]. given #75 (T,wt=11): 424 x @ y * x' * y' = e. [para(397(a,1),216(a,1)),flip(a)]. given #76 (T,wt=11): 431 x * y' * x' @ y = e. [para(397(a,1),247(a,1,1)),rewrite([137(5),137(4),82(3),1(5),2(7)])]. given #77 (A,wt=17): 49 x' * y * x * z = (x @ y') * y * z. [para(8(a,1),9(a,1,2,2,2)),rewrite([28(5)])]. given #78 (T,wt=11): 465 x * y' @ x' * y = e. [para(82(a,1),129(a,1,1,1))]. given #79 (T,wt=11): 466 x' * y @ x * y' = e. [para(82(a,1),129(a,1,1,2))]. given #80 (T,wt=11): 470 x * y @ x' * y' = e. [para(129(a,1),138(a,1,1)),rewrite([33(2)]),flip(a)]. given #81 (T,wt=11): 548 x' * y' @ y * x = e. [back_rewrite(355),rewrite([543(7)])]. given #82 (A,wt=18): 66 x' * y * z * x = y * z * (y * z @ x). [para(10(a,1),8(a,1,2)),rewrite([28(6),1(4)]),flip(a)]. given #83 (T,wt=11): 656 x * y' @ y * x' = e. [para(82(a,1),297(a,1,2,1))]. given #84 (T,wt=11): 657 x' * y @ y' * x = e. [para(82(a,1),297(a,1,2,2))]. given #85 (T,wt=11): 797 x @ y * z = x @ z * y. [para(325(a,1),190(a,1,2))]. given #86 (T,wt=11): 798 x * y @ z = y * x @ z. [para(325(a,1),191(a,1,1))]. given #87 (A,wt=14): 78 x' * y * x * y' = x @ y'. [para(28(a,1),5(a,1,2))]. given #88 (T,wt=12): 109 x * (y @ z) * x' = y @ z. [para(76(a,1),14(a,1,2)),rewrite([31(3)]),flip(a)]. given #89 (T,wt=12): 239 (x @ y) * z = z * (y @ x'). [para(216(a,1),6(a,1,1))]. given #90 (T,wt=12): 240 (x @ y') * z = z * (y @ x). [para(216(a,1),6(a,2,2))]. given #91 (T,wt=12): 254 x * (y @ x) = y * x * y'. [back_rewrite(159),rewrite([253(3)])]. given #92 (A,wt=14): 79 x * y' * x' * y = x' @ y. [para(28(a,1),5(a,1))]. given #93 (T,wt=12): 255 (x @ y) * z = z * (y' @ x). [para(218(a,1),6(a,1,1))]. given #94 (T,wt=12): 256 (x' @ y) * z = z * (y @ x). [para(218(a,1),6(a,2,2))]. given #95 (T,wt=12): 337 (x @ y) * x' * y * x = y. [para(29(a,2),29(a,1,2)),rewrite([138(2),19(7),31(7)])]. given #96 (T,wt=12): 340 (x @ y) * (x' @ y) * z = z. [para(247(a,1),1(a,1,1)),rewrite([2(2)]),flip(a)]. given #97 (A,wt=18): 83 x' * y * x * y' * z = (x @ y') * z. [para(28(a,1),9(a,1,2))]. given #98 (T,wt=12): 343 (x @ y) * z * (x' @ y) = z. [para(247(a,1),14(a,2,2)),rewrite([31(7)])]. given #99 (T,wt=12): 344 (x' @ y) * z * (x @ y) = z. [para(247(a,1),16(a,2,2)),rewrite([31(7)])]. given #100 (T,wt=12): 346 (x @ y) * (x @ y') * z = z. [para(248(a,1),1(a,1,1)),rewrite([2(2)]),flip(a)]. given #101 (T,wt=12): 349 (x @ y) * z * (x @ y') = z. [para(248(a,1),14(a,2,2)),rewrite([31(7)])]. given #102 (A,wt=18): 84 (x' @ y) * z = x * y' * x' * y * z. [para(28(a,1),9(a,1)),flip(a)]. given #103 (T,wt=12): 350 (x @ y') * z * (x @ y) = z. [para(248(a,1),16(a,2,2)),rewrite([31(7)])]. given #104 (T,wt=12): 390 x * (y' @ z) = x * (z @ y). [para(247(a,1),35(a,1,2,2,2,2)),rewrite([138(3),31(4),27(4),19(4),2(6)]),flip(a)]. given #105 (T,wt=12): 391 x * (y @ z') = x * (z @ y). [para(248(a,1),35(a,1,2,2,2,2)),rewrite([138(3),31(4),27(4),19(4),2(6)]),flip(a)]. given #106 (T,wt=12): 426 x * y * x' * y @ y = e. [para(397(a,1),212(a,2)),rewrite([1(4),1(3)])]. given #107 (A,wt=14): 88 x' * y' * x = (x @ y) * y'. [para(76(a,1),9(a,1,2,2,2)),rewrite([31(4)])]. given #108 (T,wt=12): 445 x * y * (x @ y') = y * x. [para(38(a,1),8(a,1,2)),rewrite([82(2)])]. given #109 (T,wt=12): 527 x' * y * x @ z = y @ z. [para(41(a,1),214(a,1,1)),rewrite([82(8),191(7),356(9)])]. given #110 (T,wt=12): 537 x @ y' * z * y = x @ z. [para(41(a,1),163(a,1,2)),rewrite([82(2),190(7),82(6),211(8)])]. given #111 (T,wt=12): 604 (x' @ y) * (x @ y) * z = z. [para(216(a,1),201(a,1,2,1))]. given #112 (A,wt=19): 91 x * (y @ z) * u * w = x * u * (y @ z) * w. [para(14(a,1),1(a,2,2)),rewrite([1(4)])]. given #113 (T,wt=12): 605 (x @ y') * (x @ y) * z = z. [para(216(a,2),201(a,1,1))]. given #114 (T,wt=12): 668 (x' @ y) * z = (y @ x) * z. [para(47(a,1),9(a,1)),rewrite([99(6)])]. given #115 (T,wt=12): 763 x * y * (x' @ y) = y * x. [para(218(a,2),315(a,1,2,2))]. given #116 (T,wt=12): 788 (x @ y') * x * y = y * x. [para(216(a,2),325(a,1,1))]. given #117 (A,wt=19): 92 (x @ y) * z * u * w = z * u * (x @ y) * w. [para(14(a,2),1(a,1)),rewrite([1(3)])]. given #118 (T,wt=12): 790 (x' @ y) * x * y = y * x. [para(218(a,2),325(a,1,1))]. given #119 (T,wt=12): 826 (x @ y') * z = (y @ x) * z. [para(49(a,1),9(a,1,2)),rewrite([99(6)])]. given #120 (T,wt=12): 967 x @ y * z * y' = x @ z. [para(8(a,1),797(a,1,2)),rewrite([1(4)]),flip(a)]. given #121 (T,wt=12): 975 x * y @ z' = z @ y * x. [para(797(a,1),216(a,2))]. given #122 (A,wt=21): 96 x' * (y @ z) * u' * x * u = (y @ z) * (x @ u). [para(5(a,1),14(a,1,2)),flip(a)]. given #123 (T,wt=12): 976 x' @ y * z = z * y @ x. [para(797(a,1),218(a,1))]. given #124 (T,wt=12): 1007 x * y * x' @ z = y @ z. [para(8(a,1),798(a,1,1)),rewrite([1(4)]),flip(a)]. given #125 (T,wt=12): 1131 x * (y @ x) = x * (x @ y'). [para(254(a,2),315(a,2)),rewrite([271(5),1(6),8(5)]),flip(a)]. given #126 (T,wt=13): 202 x @ y * z * x = x @ y * z. [para(1(a,1),153(a,1,2))]. given #127 (A,wt=19): 97 (x @ y) * (z @ u) * w = w * (x @ y) * (z @ u). [para(6(a,2),14(a,1,2))]. given #128 (T,wt=13): 266 x * y * z @ z = x * y @ z. [para(1(a,1),212(a,1,1))]. given #129 (T,wt=13): 280 x * y * x' * y' = x @ y. [para(253(a,1),5(a,2)),rewrite([82(2),82(2)])]. given #130 (T,wt=13): 282 (x @ y') * z = z * (x' @ y). [para(265(a,1),6(a,1,1))]. given #131 (T,wt=13): 283 (x' @ y) * z = z * (x @ y'). [para(265(a,1),6(a,2,2))]. given #132 (A,wt=16): 99 x' * (y @ z) * x * u = (y @ z) * u. [para(14(a,2),8(a,1,2))]. given #133 (T,wt=13): 295 x' * (y @ z) = (y @ z) * x'. [para(6(a,1),137(a,1,1)),rewrite([137(3),138(2),138(6)]),flip(a)]. given #134 (T,wt=13): 300 x * y @ z = z @ y' * x'. [para(137(a,1),216(a,1,2)),flip(a)]. given #135 (T,wt=13): 301 x' * y' @ z = z @ y * x. [para(137(a,1),218(a,1,1))]. given #136 (T,wt=13): 320 x * (x @ y') = y * x * y'. [para(82(a,1),29(a,1,1)),flip(a)]. given #137 (A,wt=21): 101 x' * y' * x * y * z * u = z * (x @ y) * u. [para(14(a,1),9(a,2))]. given #138 (T,wt=13): 330 x' * y * x = y * (x' @ y). [para(218(a,2),29(a,2,2))]. given #139 (T,wt=13): 335 x * (x' @ y) = y * x * y'. [para(265(a,2),29(a,2,2)),rewrite([82(2)]),flip(a)]. given #140 (T,wt=13): 457 (x' @ y) * y' * x * y = x. [para(38(a,2),29(a,1,2)),rewrite([138(3),19(9),31(8)])]. given #141 (T,wt=13): 475 x * y * z @ z * x * y = e. [para(1(a,1),471(a,1,1))]. given #142 (A,wt=25): 102 x' * y' * x * (z @ u) * y * w = (x @ y) * (z @ u) * w. [para(14(a,2),9(a,1,2,2,2))]. given #143 (T,wt=13): 476 x * y * z @ y * z * x = e. [para(1(a,1),471(a,1,2))]. given #144 (T,wt=13): 493 (x @ y') * z * (y @ x') = z. [para(265(a,1),168(a,1,1))]. given #145 (T,wt=13): 494 (x' @ y) * z * (y' @ x) = z. [para(265(a,2),168(a,1,1))]. given #146 (T,wt=13): 606 (x @ y') * (y @ x') * z = z. [para(265(a,1),201(a,1,1))]. given #147 (A,wt=25): 103 x' * (y @ z) * u' * x * u * w = (y @ z) * (x @ u) * w. [para(9(a,1),14(a,1,2)),flip(a)]. given #148 (T,wt=13): 607 (x' @ y) * (y' @ x) * z = z. [para(265(a,2),201(a,1,1))]. given #149 (T,wt=13): 649 x * (y' @ z) = x * (y @ z'). [para(290(a,1),35(a,1,2,2,2,2)),rewrite([138(4),31(5),27(5),19(6),2(7)])]. given #150 (T,wt=13): 675 x' * y = y * (y @ x) * x'. [para(76(a,1),47(a,1,2,2)),rewrite([31(3)])]. given #151 (T,wt=13): 728 x @ y * x * z = x @ y * z. [para(47(a,1),163(a,1,2)),rewrite([82(2),543(4),82(4)]),flip(a)]. given #152 (A,wt=25): 104 (x @ y) * z' * u' * z * u * w = (z @ u) * (x @ y) * w. [para(9(a,2),14(a,1,2))]. given #153 (T,wt=13): 740 x @ y * z = (x @ z) * (x @ y). [para(47(a,2),46(a,1,2,2)),rewrite([294(8)])]. given #154 (T,wt=13): 761 x' * y * (x @ y) = y * x'. [para(216(a,1),315(a,1,2,2))]. given #155 (T,wt=13): 762 x * y' * (x @ y) = y' * x. [para(218(a,1),315(a,1,2,2))]. given #156 (T,wt=13): 787 (x @ y) * x' * y = y * x'. [para(216(a,1),325(a,1,1))]. given #157 (A,wt=21): 105 (x @ y) * z * u = z * x' * y' * x * y * u. [para(9(a,2),14(a,2,2))]. given #158 (T,wt=13): 789 x' * y = (y @ x) * y * x'. [para(218(a,1),325(a,1,1)),flip(a)]. given #159 (T,wt=12): 3097 x * (y @ x) * y * x' = y. [para(789(a,1),8(a,1,2)),rewrite([82(2)])]. given #160 (T,wt=13): 865 (x' @ y) * z = (x @ y') * z. [para(49(a,1),47(a,1,2)),rewrite([99(6),99(9)]),flip(a)]. given #161 (T,wt=13): 972 (x * y @ z) * (z @ y * x) = e. [para(797(a,1),143(a,1,2))]. given #162 (A,wt=23): 111 (x @ y) * (z @ u) * w * v5 = w * (x @ y) * (z @ u) * v5. [para(14(a,2),14(a,1,2))]. given #163 (T,wt=13): 977 x' * y' @ z = z @ x * y. [para(797(a,1),218(a,2)),rewrite([137(2)])]. given #164 (T,wt=13): 1013 x * y @ z = z @ x' * y'. [para(798(a,1),216(a,2)),rewrite([137(2)]),flip(a)]. given #165 (T,wt=13): 1423 x * x * y * y @ x * y = e. [para(8(a,1),426(a,1,1,2,2)),rewrite([1(2)])]. given #166 (T,wt=13): 1884 (x @ y) * (z @ y) = x * z @ y. [para(49(a,2),96(a,1,2)),rewrite([164(8),82(4)]),flip(a)]. given #167 (A,wt=18): 113 x' * y' * x * z = (x @ y) * y' * z. [para(81(a,1),9(a,1,2,2,2))]. given #168 (T,wt=13): 2059 x * y * z @ y = x * z @ y. [para(315(a,1),266(a,1,1,2)),rewrite([198(5),198(7)])]. given #169 (T,wt=13): 2240 x * y' @ z = z @ y * x'. [para(82(a,1),300(a,2,2,1))]. given #170 (T,wt=13): 2241 x' * y @ z = z @ y' * x. [para(82(a,1),300(a,2,2,2))]. given #171 (T,wt=13): 2489 x * y * z @ y * x * z = e. [para(315(a,1),475(a,1,1,2)),rewrite([1(6),543(7)])]. given #172 (A,wt=16): 116 x * (y @ z) * x' * u = (y @ z) * u. [para(81(a,1),14(a,1,2)),flip(a)]. given #173 (T,wt=13): 2490 x * y * z @ z * y * x = e. [para(325(a,1),475(a,1,1,2)),rewrite([1(6),1723(7)])]. given #174 (T,wt=13): 2686 x * y' @ z = z @ x' * y. [para(675(a,1),300(a,1,1)),rewrite([195(5),82(6)])]. given #175 (T,wt=13): 2687 x' * y @ z = z @ x * y'. [para(675(a,2),300(a,1,1)),rewrite([137(7),82(5),138(5),1(7),543(8)])]. given #176 (T,wt=13): 2746 (x @ y) * (x @ z) = x @ y * z. [para(740(a,2),6(a,1)),flip(a)]. given #177 (A,wt=24): 139 x' * y' * z * x * y * z' = y * x @ x' * z'. [para(122(a,1),10(a,1,2,2,2)),rewrite([137(2),137(5),137(7),82(5),82(5),1(7),1(8),137(11)])]. given #178 (T,wt=11): 4143 x * x @ y = x @ y * y. [para(2746(a,1),1884(a,1)),flip(a)]. given #179 (T,wt=12): 4226 x * x @ y' = y * y @ x. [para(4143(a,2),216(a,2))]. given #180 (T,wt=12): 4227 x' @ y * y = y @ x * x. [para(4143(a,1),218(a,2))]. given #181 (T,wt=13): 2747 (x @ y) * (y @ z * x) = y @ z. [para(740(a,2),8(a,1,2)),rewrite([138(2)])]. given #182 (A,wt=15): 148 x' * y' = (x @ y) * y' * x'. [back_rewrite(123),rewrite([137(3)]),flip(a)]. given #183 (T,wt=13): 2768 (x @ y) * (y @ x * z) = y @ z. [para(740(a,2),27(a,1,2)),rewrite([138(2)])]. given #184 (T,wt=13): 3353 (x @ y) * (y * z @ x) = z @ x. [para(1884(a,1),8(a,1,2)),rewrite([138(2)])]. given #185 (T,wt=13): 3361 (x @ y) * (z * y @ x) = z @ x. [para(1884(a,1),27(a,1,2)),rewrite([138(2)])]. given #186 (T,wt=13): 3881 x * y * z @ x * z * y = e. [para(325(a,1),2489(a,1,1,2)),rewrite([190(7)])]. given #187 (A,wt=23): 149 x' * y' * z' * x * y * z = y * x @ x' * z. [back_rewrite(115),rewrite([137(2),137(6),82(6),1(7),1(8)])]. given #188 (T,wt=13): 4225 x @ y' * y' = y @ x * x. [para(4143(a,1),216(a,1))]. given #189 (T,wt=13): 4228 x' * x' @ y = y * y @ x. [para(4143(a,2),218(a,1))]. given #190 (T,wt=13): 4257 x * x @ y * x = x @ y * y. [para(4143(a,2),202(a,1)),rewrite([1(5),728(6)])]. given #191 (T,wt=13): 4258 x * y @ y * y = x * x @ y. [para(4143(a,1),266(a,1)),rewrite([1(5),2059(6)])]. given #192 (A,wt=21): 152 x' * y' * z * y * x * z' = y * x @ z'. [back_rewrite(85),rewrite([137(2),1(8)])]. given #193 (T,wt=13): 4295 x' @ y * y = x * x @ y'. [para(4226(a,2),218(a,2))]. given #194 (T,wt=13): 4641 x * x @ y * x = x * x @ y. [para(4257(a,2),5(a,2)),rewrite([137(3),1(7),149(8),4224(4)]),flip(a)]. given #195 (T,wt=13): 4645 x * y @ x * x = y @ x * x. [para(4257(a,2),212(a,1)),rewrite([1(5),1(4),266(9),1014(5)])]. given #196 (T,wt=13): 4684 x * x @ x * y = x * x @ y. [para(4258(a,2),153(a,1)),rewrite([1(8),1(7),202(9),973(5)])]. given #197 (A,wt=23): 154 x * y' * z' * x' * y * z = y * x' @ x * z. [back_rewrite(67),rewrite([137(3),82(2),137(4),1(7),1(8)])]. given #198 (T,wt=13): 4690 x * y @ y * y = x @ y * y. [para(4258(a,1),27(a,1,2,1)),rewrite([3352(4),279(6),2746(3)]),flip(a)]. given #199 (T,wt=14): 304 x' * y' @ z = y * x @ z'. [para(137(a,1),265(a,1,1))]. given #200 (T,wt=14): 305 x' @ y * z = x @ z' * y'. [para(137(a,1),265(a,2,2))]. given #201 (T,wt=14): 306 x * y * z @ z' = z @ x * y. [para(1(a,1),172(a,1,1))]. given #202 (A,wt=20): 164 x' * y' * z' * y * x * z = y * x @ z. [back_rewrite(10),rewrite([137(2),1(8)])]. given #203 (T,wt=14): 314 (x @ y) * y' * x' * y = x'. [para(5(a,1),29(a,1,2)),rewrite([137(4),137(2),82(5),1(4),6(6,R),267(12),31(9)])]. given #204 (T,wt=14): 329 x' * (y @ x) = y' * x' * y. [para(218(a,1),29(a,2,2)),flip(a)]. given #205 (T,wt=14): 333 x' * (x @ y) = y * x' * y'. [para(253(a,1),29(a,2,2)),rewrite([82(2)]),flip(a)]. given #206 (T,wt=14): 352 x' @ y * z * x = y * z @ x. [para(1(a,1),272(a,1,2))]. given #207 (A,wt=15): 166 (x @ y) * z * (y @ x) * u = z * u. [back_rewrite(117),rewrite([138(3)])]. given #208 (T,wt=14): 456 x' * (y @ x) = x' * (x @ y'). [para(38(a,1),29(a,1,2)),rewrite([137(2),1(7),8(6),272(8)]),flip(a)]. given #209 (T,wt=14): 662 x' * y' * x * (y @ x) = y'. [para(3(a,1),47(a,1,2)),rewrite([31(3),137(3),137(6),173(8),253(7),6(6),1(7)]),flip(a)]. given #210 (T,wt=14): 766 x * y' * (y @ x') = y' * x. [para(265(a,1),315(a,1,2,2))]. given #211 (T,wt=14): 767 x' * y * (y' @ x) = y * x'. [para(265(a,2),315(a,1,2,2))]. given #212 (A,wt=19): 175 x * y * (z @ u) * w = x * y * w * (z @ u). [para(15(a,1),1(a,1)),rewrite([1(4)]),flip(a)]. given #213 (T,wt=14): 791 x' * y = (x @ y') * y * x'. [para(265(a,1),325(a,1,1)),flip(a)]. given #214 (T,wt=14): 792 (x' @ y) * y' * x = x * y'. [para(265(a,2),325(a,1,1))]. given #215 (T,wt=14): 979 x' @ y' * z' = x @ y * z. [para(797(a,1),253(a,2)),rewrite([137(3)])]. given #216 (T,wt=14): 980 x' @ y * z = x @ y' * z'. [para(797(a,1),265(a,1)),rewrite([137(5)])]. given #217 (A,wt=19): 176 x * (y @ z) * u * w = x * u * w * (y @ z). [para(1(a,1),15(a,2,2))]. given #218 (T,wt=14): 1015 x' * y' @ z' = x * y @ z. [para(798(a,1),253(a,2)),rewrite([137(2)])]. given #219 (T,wt=14): 1016 x' * y' @ z = x * y @ z'. [para(798(a,1),265(a,2)),rewrite([137(2)])]. given #220 (T,wt=14): 1064 x' * (y @ z) = (z' @ y) * x'. [para(239(a,1),137(a,1,1)),rewrite([137(4),138(3),138(7)]),flip(a)]. given #221 (T,wt=14): 1093 x' * (y' @ z) = (z @ y) * x'. [para(240(a,1),137(a,1,1)),rewrite([137(3),138(2),138(7)]),flip(a)]. given #222 (A,wt=19): 180 (x @ y) * z * (u @ w) = (u @ w) * z * (x @ y). [para(15(a,1),6(a,1)),rewrite([1(8)])]. given #223 (T,wt=14): 1119 (x @ y) * x' = y * x' * y'. [para(254(a,1),137(a,1,1)),rewrite([137(4),137(3),82(2),1(4),138(6)]),flip(a)]. given #224 (T,wt=14): 1164 x' * (y @ z) = (z @ y') * x'. [para(255(a,1),137(a,1,1)),rewrite([137(4),138(3),138(7)]),flip(a)]. given #225 (T,wt=14): 1197 x' * (y @ z') = (z @ y) * x'. [para(256(a,1),137(a,1,1)),rewrite([137(3),138(2),138(7)]),flip(a)]. given #226 (T,wt=14): 1215 (x @ y) * x * y' * x' = y'. [para(253(a,1),337(a,1,1)),rewrite([82(3)])]. given #227 (A,wt=19): 181 (x @ y) * (z @ u) * w = w * (z @ u) * (x @ y). [para(15(a,2),6(a,1)),rewrite([1(8)])]. given #228 (T,wt=14): 1638 x' * y = y * (x @ y') * x'. [para(239(a,2),763(a,1,2)),flip(a)]. given #229 (T,wt=14): 1892 (x @ y) * (y @ z') = x * z @ y. [back_rewrite(1048),rewrite([1890(8)]),flip(a)]. given #230 (T,wt=14): 2430 x * y' @ z = (z @ y) * (x @ z). [back_rewrite(588),rewrite([2401(8)])]. given #231 (T,wt=14): 2432 x * y' @ z = (x @ z) * (z @ y). [back_rewrite(318),rewrite([2401(8)])]. given #232 (A,wt=25): 182 x' * y' * x * y * z * (u @ w) = (x @ y) * (u @ w) * z. [para(15(a,1),9(a,1,2,2,2))]. given #233 (T,wt=14): 2434 (x @ y) * (y' @ z) = x * z @ y. [para(335(a,1),9(a,1,2,2,2)),rewrite([1890(8)]),flip(a)]. given #234 (T,wt=14): 2640 x * (x @ y) * y' * x' = y'. [para(219(a,1),675(a,2,2,1)),rewrite([137(2),1(4),3(3),31(3),137(4)]),flip(a)]. given #235 (T,wt=14): 2696 x @ y * x' * z = x @ y * z. [para(81(a,1),728(a,1,2,2)),flip(a)]. given #236 (T,wt=14): 2759 x @ y * z' = (z @ x) * (x @ y). [para(216(a,1),740(a,2,1))]. given #237 (A,wt=25): 183 x' * y' * x * y * (z @ u) * w = (x @ y) * w * (z @ u). [para(15(a,1),9(a,2))]. given #238 (T,wt=14): 2760 x @ y' * z = (x @ z) * (y @ x). [para(216(a,1),740(a,2,2))]. given #239 (T,wt=14): 2808 (x @ y) * (z @ x') = x @ y * z. [para(740(a,2),239(a,1)),flip(a)]. given #240 (T,wt=14): 2809 x @ y' * z = (y @ x) * (x @ z). [para(740(a,2),239(a,2)),flip(a)]. given #241 (T,wt=14): 2810 x @ y * z' = (x @ y) * (z @ x). [para(740(a,2),240(a,1))]. given #242 (A,wt=21): 184 x * y' * z' * y * z * u = x * u * (y @ z). [para(9(a,2),15(a,1,2))]. given #243 (T,wt=14): 2812 (x @ y) * (z' @ x) = x @ y * z. [para(740(a,2),255(a,1)),flip(a)]. given #244 (T,wt=14): 2815 (x' @ y) * (y @ z) = y @ x * z. [para(740(a,2),256(a,2))]. given #245 (T,wt=14): 2822 (x' @ y) * (x @ y * z) = x @ z. [para(740(a,2),344(a,1,2))]. given #246 (T,wt=14): 2827 (x' @ y) * (x @ z * y) = x @ z. [para(740(a,2),604(a,1,2))]. given #247 (A,wt=23): 185 (x @ y) * z * u * (w @ v5) = z * (x @ y) * (w @ v5) * u. [para(15(a,1),14(a,1,2))]. given #248 (T,wt=14): 3358 (x @ y') * (z @ x) = y * z @ x. [para(216(a,2),1884(a,1,1))]. given #249 (T,wt=14): 3359 x' * y @ z = (z @ x) * (y @ z). [para(218(a,1),1884(a,1,1)),flip(a)]. given #250 (T,wt=14): 3388 x' * y @ z = (y @ z) * (z @ x). [para(1884(a,1),256(a,1))]. given #251 (T,wt=14): 3392 (x @ y') * (z * x @ y) = z @ y. [para(1884(a,1),350(a,1,2))]. given #252 (A,wt=23): 186 (x @ y) * z * (u @ w) * v5 = z * (x @ y) * v5 * (u @ w). [para(15(a,1),14(a,2,2))]. given #253 (T,wt=14): 3396 (x @ y') * (x * z @ y) = z @ y. [para(1884(a,1),605(a,1,2))]. given #254 (T,wt=14): 3603 x * y' * x' * (x @ y) = y'. [para(113(a,2),344(a,1)),rewrite([82(2)])]. given #255 (T,wt=14): 3714 x' @ y * z' = x @ z * y'. [para(2240(a,1),216(a,1))]. given #256 (T,wt=14): 3715 x * y' @ z' = y * x' @ z. [para(2240(a,2),216(a,2))]. given #257 (A,wt=23): 188 x * (y @ z) * u * (w @ v5) = x * (w @ v5) * u * (y @ z). [para(15(a,1),15(a,1,2)),rewrite([1(9)])]. given #258 (T,wt=14): 3746 x' @ y * z' = x @ y' * z. [para(2240(a,1),975(a,1))]. given #259 (T,wt=14): 3747 x' * y @ z' = x * y' @ z. [para(2240(a,2),975(a,2))]. given #260 (T,wt=14): 3748 x' @ y' * z = x @ y * z'. [para(2240(a,1),976(a,2))]. given #261 (T,wt=14): 3749 x' * y @ z = x * y' @ z'. [para(2240(a,2),976(a,1)),flip(a)]. given #262 (A,wt=23): 189 x * (y @ z) * (u @ w) * v5 = x * v5 * (u @ w) * (y @ z). [para(15(a,2),15(a,1,2)),rewrite([1(9)])]. given #263 (T,wt=14): 3791 x' @ y' * z = x @ z' * y. [para(2241(a,1),216(a,1))]. given #264 (T,wt=14): 3792 x' * y @ z' = y' * x @ z. [para(2241(a,2),216(a,2))]. given #265 (T,wt=14): 4224 x * y @ y' * x = y * y @ x. [para(4143(a,2),5(a,2)),rewrite([137(3),1(7),149(8)])]. given #266 (T,wt=14): 4233 x' @ y * y = x' * x' @ y. [para(4143(a,2),163(a,2)),rewrite([163(4)])]. given #267 (A,wt=15): 195 x * (y @ z) * u @ w = x * u @ w. [back_rewrite(106),rewrite([191(4)]),flip(a)]. given #268 (T,wt=14): 4328 x * y' @ y * x = x @ y * y. [para(4227(a,1),5(a,2)),rewrite([82(2),137(2),1(7),154(8)])]. given #269 (T,wt=14): 4565 x * y' @ y * y = x @ y * y. [para(29(a,1),149(a,1,2,2,2)),rewrite([82(2),4561(7),82(6)]),flip(a)]. given #270 (T,wt=14): 4568 x * x @ x' * y = x * x @ y. [para(47(a,1),149(a,1,2)),rewrite([847(6),149(8),4224(4)]),flip(a)]. given #271 (T,wt=14): 4781 x' * y @ x * x = y @ x * x. [para(81(a,1),4645(a,1,1)),flip(a)]. given #272 (A,wt=21): 199 (x @ y) * z' * u' * z * u * (y @ x) = z @ u. [back_rewrite(157),rewrite([197(12)])]. given #273 (T,wt=14): 4810 x * x @ y * x' = x * x @ y. [para(254(a,2),4684(a,1,2)),rewrite([198(4)]),flip(a)]. given #274 (T,wt=14): 7543 x' * y @ y * x = y @ x * x. [para(4224(a,1),138(a,1,1)),rewrite([138(3)]),flip(a)]. given #275 (T,wt=14): 7548 x * y @ x' * y = x * x @ y. [para(315(a,1),4224(a,1,1)),rewrite([137(4),138(3),1(5),190(6),1(9),1725(10),6(6),550(8)])]. given #276 (T,wt=14): 7549 x * y @ y * x' = x * x @ y. [para(315(a,1),4224(a,1,2)),rewrite([1(4),6(3),445(4),198(9)])]. given #277 (A,wt=15): 215 x * y * z @ x * y = z @ x * y. [para(1(a,1),174(a,1,1))]. given #278 (T,wt=14): 7551 x * y @ x * y' = y * y @ x. [para(4224(a,1),797(a,1)),flip(a)]. given #279 (T,wt=14): 7602 x * y' @ x * y = x @ y * y. [para(315(a,1),4328(a,1,2)),rewrite([1(4),195(6),197(8)])]. given #280 (T,wt=14): 7604 x' * y @ x * y = y @ x * x. [para(4328(a,1),798(a,1)),flip(a)]. given #281 (T,wt=15): 222 (x @ y) * z * u * (y @ x) = z * u. [para(16(a,1),8(a,1,2)),rewrite([138(2)])]. given #282 (A,wt=19): 221 (x @ y) * z * u * w = z * u * w * (x @ y). [para(16(a,2),1(a,1)),rewrite([1(3)])]. given #283 (T,wt=15): 274 x * y @ x * y * z = x * y @ z. [para(1(a,1),219(a,1,2))]. given #284 (T,wt=15): 316 x' * (x' @ y) = y' * x' * y. [para(8(a,1),29(a,1,2)),rewrite([137(2),1(4),163(8)]),flip(a)]. given #285 (T,wt=15): 334 x' * (x @ y') = y' * x' * y. [para(265(a,1),29(a,2,2)),flip(a)]. given #286 (T,wt=15): 539 x * y * z' @ z = z' @ x * y. [para(1(a,1),173(a,1,1))]. given #287 (A,wt=21): 223 x' * y' * x * y * z * u = z * u * (x @ y). [para(16(a,1),9(a,2))]. given #288 (T,wt=15): 543 x @ y * (z @ u) * w = x @ y * w. [para(14(a,1),190(a,1,2))]. given #289 (T,wt=15): 544 x @ y * z * (u @ w) = x @ y * z. [para(16(a,1),190(a,1,2))]. given #290 (T,wt=15): 550 x * y * (z @ u) @ w = x * y @ w. [para(16(a,1),191(a,1,1))]. given #291 (T,wt=15): 641 x @ y * z * x' = y * z @ x'. [para(1(a,1),271(a,1,2))]. given #292 (A,wt=25): 224 x' * y' * x * (z @ u) * y * w = (x @ y) * w * (z @ u). [para(16(a,2),9(a,1,2,2,2))]. given #293 (T,wt=15): 654 x' * y' * x = (y @ x') * y'. [para(291(a,1),41(a,1,2,2)),rewrite([138(3),31(5),82(8),18(7),2(10)]),flip(a)]. given #294 (T,wt=15): 665 x * y * (y @ x) * z = y * x * z. [para(47(a,1),8(a,1,2)),rewrite([82(2)])]. given #295 (T,wt=15): 687 x * y * z @ y' = x * z @ y'. [para(47(a,1),174(a,1,1)),rewrite([195(5)]),flip(a)]. given #296 (T,wt=15): 701 x' @ y * x * z = x' @ y * z. [para(47(a,1),219(a,1,2)),rewrite([543(5)]),flip(a)]. given #297 (A,wt=25): 226 x' * y' * x * y * z * (u @ w) = (u @ w) * (x @ y) * z. [para(16(a,2),9(a,2))]. given #298 (T,wt=15): 744 x' * y' * x * (x' @ y) = y'. [para(291(a,1),47(a,2,2)),rewrite([31(10)])]. given #299 (T,wt=15): 765 x' * y' = y' * x' * (x @ y). [para(253(a,1),315(a,1,2,2)),flip(a)]. given #300 (T,wt=15): 770 x * y * y * x = y * x * x * y. [para(471(a,1),315(a,1,2,2)),rewrite([31(4),1(3),1(6)])]. given #301 (T,wt=15): 777 (x @ y) * y * x * z = x * y * z. [para(325(a,1),1(a,1,1)),rewrite([1(2),1(5)]),flip(a)]. given #302 (A,wt=25): 227 (x @ y) * z' * u' * z * u * w = (z @ u) * w * (x @ y). [para(9(a,2),16(a,1,2))]. given #303 (T,wt=15): 783 (x @ y) * z * y * x = z * x * y. [para(325(a,1),14(a,2,2))]. ============================== PROOF ================================= % Proof 1 at 4.35 (+ 0.05) seconds: E. % Length of proof is 31. % Level of proof is 11. % Maximum clause weight is 19. % Given clauses 303. 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))]. 14 (x @ y) * z * u = z * (x @ y) * u. [para(6(a,1),1(a,1,1)),rewrite([1(3)]),flip(a)]. 22 x'' * e = x. [para(3(a,1),8(a,1,2))]. 25 x'' * (x @ y) = y' * x * y. [para(5(a,1),8(a,1,2))]. 28 x'' * y = x * y. [para(8(a,1),8(a,1,2))]. 29 x' * y * x = y * (y @ x). [back_rewrite(25),rewrite([28(4)]),flip(a)]. 31 x * e = x. [back_rewrite(22),rewrite([28(4)])]. 47 x' * y * x * z = y * (y @ x) * z. [para(9(a,1),8(a,1,2)),rewrite([28(5)]),flip(a)]. 68 (x * y)' * y * x = x * y @ x. [para(8(a,1),10(a,1,2))]. 70 x * y @ x = y @ x * y. [para(9(a,1),10(a,1,2)),rewrite([8(3),6(4),8(5),8(5)])]. 74 (x * y)' * y * x = y @ x * y. [back_rewrite(68),rewrite([70(6)])]. 76 x * x' = e. [para(28(a,1),3(a,1))]. 82 x'' = x. [para(28(a,1),31(a,1)),rewrite([31(2)]),flip(a)]. 87 x * y * (x * y)' = e. [para(76(a,1),1(a,1)),flip(a)]. 122 x * (y * x)' = y'. [para(87(a,1),8(a,1,2)),rewrite([31(3)]),flip(a)]. 137 (x * y)' = y' * x'. [para(122(a,1),8(a,1,2)),flip(a)]. 153 x @ y * x = x @ y. [back_rewrite(74),rewrite([137(2),1(5),5(5)]),flip(a)]. 174 x * y @ x = y @ x. [back_rewrite(70),rewrite([153(4)])]. 325 (x @ y) * y * x = x * y. [para(174(a,1),29(a,2,2)),rewrite([1(3),8(4),6(4,R)]),flip(a)]. 665 x * y * (y @ x) * z = y * x * z. [para(47(a,1),8(a,1,2)),rewrite([82(2)])]. 783 (x @ y) * z * y * x = z * x * y. [para(325(a,1),14(a,2,2))]. 8517 $F # answer(E). [para(783(a,2),7(a,1,2,2)),rewrite([665(13)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=303. Generated=143710. Kept=8515. proofs=1. Usable=275. Sos=6112. Demods=1753. Limbo=3, Disabled=2131. Hints=0. Kept_by_rule=0, Deleted_by_rule=19994. Forward_subsumed=115200. Back_subsumed=251. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=2932 (5 lex), Back_demodulated=1874. Back_unit_deleted=0. Demod_attempts=2618852. Demod_rewrites=525657. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=6.93. User_CPU=4.35, System_CPU=0.05, Wall_clock=5. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11618 exit (max_proofs) Wed Feb 25 09:33:17 2009