============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 3866 was started by mccune on cleo.thornwood, Wed Nov 22 11:24:22 2006 The command was "/home/mccune/bin/prover9 -f gt.in ED.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 ED.in formulas(sos). x * y * z * y * x = y * x * z * x * y. end_of_list. formulas(sos). (A @ C) * (B @ C) != A * B @ C # answer(D). 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 * y * x = y * x * z * x * y. [assumption]. (A @ C) * (B @ C) != A * B @ C # answer(D). [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 * y * x = y * x * z * x * y. [assumption]. 7 (A @ C) * (B @ C) != A * B @ C # answer(D). [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)]. 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=19): 6 x * y * z * y * x = y * x * z * x * y. [assumption]. given #6 (I,wt=13): 7 (A @ C) * (B @ C) != A * B @ C # answer(D). [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=6): 12 x' @ x = e. [para(3(a,1),5(a,1,2,2)),rewrite(8(6)),flip(a)]. given #9 (T,wt=8): 8 x' * x * y = y. [para(3(a,1),1(a,1,1)),rewrite(2(2)),flip(a)]. given #10 (T,wt=5): 26 x @ x = e. [para(8(a,1),5(a,1,2)),rewrite(3(2)),flip(a)]. given #11 (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 #12 (F,wt=19): 51 A' * C' * A * C * (B @ C) != A * B @ C # answer(D). [para(9(a,2),7(a,1))]. given #13 (F,wt=5): 35 x * e = x. [back_rewrite(24),rewrite(32(4))]. given #14 (T,wt=4): 57 e' = e. [para(35(a,1),3(a,1))]. given #15 (T,wt=5): 58 x @ e = e. [para(35(a,1),5(a,1,2,2)),rewrite(57(3),2(3),3(2)),flip(a)]. given #16 (A,wt=19): 10 (x * y)' * z' * x * y * z = x * y @ z. [para(1(a,1),5(a,1,2,2))]. given #17 (F,wt=7): 69 x * x @ x = e. [para(10(a,1),10(a,1,2)),rewrite(3(2),57(2),2(4),3(4),11(5))]. given #18 (F,wt=9): 32 x'' * y = x * y. [para(8(a,1),8(a,1,2))]. given #19 (T,wt=5): 83 x'' = x. [para(32(a,1),35(a,1)),rewrite(35(2)),flip(a)]. given #20 (T,wt=6): 74 x * x' = e. [para(32(a,1),3(a,1))]. given #21 (A,wt=23): 14 x * y * z * y * x * u = y * x * z * x * y * u. [para(6(a,1),1(a,1,1)),rewrite(1(5),1(4),1(3),1(2),1(9),1(8),1(7))]. given #22 (F,wt=6): 85 x @ x' = e. [para(83(a,1),12(a,1,1))]. given #23 (F,wt=8): 79 x * x' * y = y. [para(32(a,1),8(a,1))]. given #24 (T,wt=10): 86 x * y * (x * y)' = e. [para(74(a,1),1(a,1)),flip(a)]. given #25 (T,wt=9): 118 x * (y * x)' = y'. [para(86(a,1),8(a,1,2)),rewrite(35(3)),flip(a)]. given #26 (A,wt=23): 15 x * y * z * u * z * y = x * z * y * u * y * z. [para(6(a,1),1(a,2,2)),rewrite(1(5))]. given #27 (F,wt=8): 132 (x @ y)' = y @ x. [para(9(a,2),118(a,1,2,1)),rewrite(131(7),131(5),131(3),131(2),1(5),83(7),1(6),1(5),83(8),1(7),1(6),1(5),5(6),79(4)),flip(a)]. given #28 (F,wt=9): 141 (x @ y) * (y @ x) = e. [back_rewrite(120),rewrite(131(8),131(6),131(4),131(3),1(6),83(8),1(7),1(6),83(9),1(8),1(7),1(6),5(7),79(5))]. given #29 (T,wt=9): 147 x * y @ x = y @ x. [back_rewrite(65),rewrite(131(2),1(5),5(5)),flip(a)]. given #30 (T,wt=9): 174 (x @ y) @ (y @ x) = e. [para(132(a,1),12(a,1,1))]. given #31 (A,wt=23): 16 x * y * z * u * y * x = y * x * z * u * x * y. [para(1(a,1),6(a,1,2,2)),rewrite(1(8))]. given #32 (F,wt=9): 188 x @ x * y = x @ y. [para(147(a,1),132(a,1,1)),rewrite(132(2)),flip(a)]. given #33 (F,wt=10): 131 (x * y)' = y' * x'. [para(118(a,1),8(a,1,2)),flip(a)]. given #34 (T,wt=10): 160 x * y @ y' = y @ x. [back_rewrite(89),rewrite(147(5))]. given #35 (T,wt=10): 186 x' * y @ x = y @ x. [para(79(a,1),147(a,1,1)),flip(a)]. given #36 (A,wt=15): 18 x * y * y * x = y * x * x * y. [para(2(a,1),6(a,1,2,2)),rewrite(2(6))]. given #37 (F,wt=10): 210 x @ x' * y = x @ y. [para(79(a,1),188(a,1,2)),flip(a)]. given #38 (F,wt=10): 221 x' @ y * x = y @ x. [para(160(a,1),132(a,1,1)),rewrite(132(2)),flip(a)]. given #39 (T,wt=11): 154 x' @ x * y = x' @ y. [back_rewrite(34),rewrite(131(2),1(4),77(5)),flip(a)]. given #40 (T,wt=11): 161 x * y * (y @ x) = y * x. [back_rewrite(71),rewrite(147(2))]. given #41 (A,wt=21): 28 x * y * x' * z * y = y * z * x * y * x'. [para(8(a,1),6(a,1,2,2,2)),rewrite(1(5),1(10),1(12),8(13))]. given #42 (F,wt=11): 162 x * y' @ y = y' @ x. [back_rewrite(70),rewrite(147(6))]. given #43 (F,wt=11): 175 (x @ y) * (y @ x) * z = z. [para(132(a,1),8(a,1,1))]. given #44 (T,wt=11): 182 x * y @ x' = y @ x'. [para(8(a,1),147(a,1,1)),flip(a)]. given #45 (T,wt=11): 216 x' * y' @ y * x = e. [para(131(a,1),12(a,1,1))]. given #46 (A,wt=16): 29 x * y * x' * y * x = y * x * y. [para(8(a,1),6(a,1,2,2)),flip(a)]. given #47 (F,wt=11): 217 x * y @ y' * x' = e. [para(131(a,1),85(a,1,2))]. given #48 (F,wt=11): 235 (x @ y) * y * x = x * y. [para(18(a,1),9(a,1,2,2)),rewrite(8(6),8(4)),flip(a)]. given #49 (T,wt=9): 359 (x @ y) @ y * x = e. [para(235(a,1),5(a,1,2,2)),rewrite(132(2),131(3),1(6),5(6),141(3)),flip(a)]. given #50 (T,wt=7): 399 (x @ y) @ x = e. [para(79(a,1),359(a,1,2)),rewrite(186(3))]. given #51 (A,wt=18): 30 x' * y * x * y * x' = y * x' * y. [para(8(a,1),6(a,1,2)),flip(a)]. given #52 (F,wt=7): 417 x @ (x @ y) = e. [para(399(a,1),132(a,1,1)),rewrite(57(2)),flip(a)]. given #53 (F,wt=8): 419 (x @ y) @ y' = e. [para(221(a,1),399(a,1,1))]. given #54 (T,wt=8): 457 (x @ y) @ x' = e. [para(417(a,1),160(a,2)),rewrite(420(2),182(4))]. given #55 (T,wt=7): 478 (x @ y) @ y = e. [para(221(a,1),457(a,1,1)),rewrite(83(3))]. given #56 (A,wt=20): 31 x' * y * x * z * x * y = y * z * y * x. [para(6(a,1),8(a,1,2))]. given #57 (F,wt=7): 486 x @ (y @ x) = e. [para(478(a,1),132(a,1,1)),rewrite(57(2)),flip(a)]. given #58 (F,wt=8): 459 x' @ (y @ x) = e. [para(221(a,1),417(a,1,2))]. given #59 (T,wt=8): 460 (x' @ y) @ x = e. [para(417(a,1),162(a,2)),rewrite(420(4),186(5))]. given #60 (T,wt=8): 466 (x @ y') @ y = e. [para(83(a,1),419(a,1,2))]. given #61 (A,wt=12): 33 x' * y * x = y * (y @ x). [back_rewrite(27),rewrite(32(4)),flip(a)]. given #62 (F,wt=8): 473 x' @ (x @ y) = e. [para(457(a,1),132(a,1,1)),rewrite(57(2)),flip(a)]. given #63 (F,wt=8): 481 x @ y' = y @ x. [back_rewrite(361),rewrite(473(3),2(4))]. given #64 (T,wt=8): 516 x @ (x' @ y) = e. [para(162(a,1),486(a,1,2))]. given #65 (T,wt=8): 519 x @ (y @ x') = e. [para(83(a,1),459(a,1,1))]. given #66 (A,wt=21): 39 x * y' * z' * y * z * u = x * (y @ z) * u. [para(9(a,1),1(a,2,2)),rewrite(1(7))]. given #67 (F,wt=14): 578 (C @ A') * (B @ C) != A * B @ C # answer(D). [para(481(a,2),7(a,1,1))]. given #68 (F,wt=14): 579 (A @ C) * (C @ B') != A * B @ C # answer(D). [para(481(a,2),7(a,1,2))]. given #69 (T,wt=8): 570 x' @ y = y @ x. [para(460(a,1),33(a,2,2)),rewrite(48(4),8(4),35(5)),flip(a)]. given #70 (T,wt=9): 373 (x @ y) @ x * y = e. [para(235(a,1),188(a,1,2)),rewrite(359(6))]. given #71 (A,wt=22): 46 x' * y * x * (y @ z) = (x @ y') * z' * y * z. [para(5(a,1),9(a,1,2,2,2)),rewrite(32(6))]. given #72 (F,wt=14): 656 C' @ A * B != (A @ C) * (B @ C) # answer(D). [para(570(a,2),7(a,2)),flip(a)]. given #73 (F,wt=15): 580 C @ B' * A' != (A @ C) * (B @ C) # answer(D). [para(481(a,2),7(a,2)),rewrite(131(12)),flip(a)]. given #74 (T,wt=9): 402 x * y @ y * x = e. [para(359(a,1),147(a,2)),rewrite(1(3),161(3))]. given #75 (T,wt=9): 427 x @ y * x = x @ y. [back_rewrite(163),rewrite(420(3),8(4)),flip(a)]. given #76 (A,wt=12): 48 (x' @ y) * x = x * (y @ x). [para(5(a,1),9(a,1,2)),rewrite(32(4)),flip(a)]. given #77 (F,wt=15): 653 (C @ A') * (C @ B') != A * B @ C # answer(D). [para(481(a,2),578(a,1,2))]. given #78 (F,wt=15): 668 C' @ A * B != (C @ A') * (B @ C) # answer(D). [para(570(a,2),578(a,2)),flip(a)]. given #79 (T,wt=9): 588 x' @ y' = x @ y. [para(481(a,2),147(a,1)),rewrite(131(2),255(4))]. given #80 (T,wt=9): 594 x * y @ y = x @ y. [para(481(a,2),221(a,1)),rewrite(83(3))]. given #81 (A,wt=15): 49 (x @ y) * z * y * x = z * x * y. [para(6(a,1),9(a,1,2,2)),rewrite(8(7),8(5)),flip(a)]. given #82 (F,wt=15): 669 C' @ A * B != (A @ C) * (C @ B') # answer(D). [para(570(a,2),579(a,2)),flip(a)]. given #83 (F,wt=16): 654 C @ B' * A' != (C @ A') * (B @ C) # answer(D). [para(481(a,2),578(a,2)),rewrite(131(13)),flip(a)]. given #84 (T,wt=9): 596 x' @ y = x @ y'. [para(481(a,2),162(a,1)),rewrite(131(3),83(2),188(3)),flip(a)]. given #85 (T,wt=10): 412 x' * y * x @ y = e. [back_rewrite(225),rewrite(399(6))]. given #86 (A,wt=13): 50 x' * y = (y @ x) * y * x'. [para(6(a,1),9(a,1,2)),rewrite(8(6),8(5))]. given #87 (F,wt=16): 655 C @ B' * A' != (A @ C) * (C @ B') # answer(D). [para(481(a,2),579(a,2)),rewrite(131(13)),flip(a)]. given #88 (F,wt=16): 725 B' * A' @ C' != (A @ C) * (B @ C) # answer(D). [para(570(a,2),656(a,1)),rewrite(131(4))]. given #89 (T,wt=10): 418 (x @ y) @ y' * x = e. [para(186(a,1),399(a,1,1))]. given #90 (T,wt=10): 421 (x @ y') @ y * x = e. [para(182(a,1),399(a,1,1))]. given #91 (A,wt=16): 52 x' * y * x * z = y * (y @ x) * z. [para(9(a,1),8(a,1,2)),rewrite(32(5)),flip(a)]. given #92 (F,wt=16): 810 C' @ A * B != (C @ A') * (C @ B') # answer(D). [para(570(a,2),653(a,2)),flip(a)]. given #93 (F,wt=17): 809 C @ B' * A' != (C @ A') * (C @ B') # answer(D). [para(481(a,2),653(a,2)),rewrite(131(14)),flip(a)]. given #94 (T,wt=10): 422 x @ y' * x * y = e. [back_rewrite(244),rewrite(417(6))]. given #95 (T,wt=10): 461 x * y @ (y @ x') = e. [para(182(a,1),417(a,1,2))]. given #96 (A,wt=17): 54 x' * y * x * z = (x @ y') * y * z. [para(8(a,1),9(a,1,2,2,2)),rewrite(32(5))]. given #97 (F,wt=17): 812 B' * A' @ C' != (C @ A') * (B @ C) # answer(D). [para(570(a,2),668(a,1)),rewrite(131(4))]. given #98 (F,wt=17): 927 B' * A' @ C' != (A @ C) * (C @ B') # answer(D). [para(570(a,2),669(a,1)),rewrite(131(4))]. given #99 (T,wt=10): 471 (x @ y) * (x @ y') = e. [para(457(a,1),5(a,2)),rewrite(132(2),83(3),390(5))]. given #100 (T,wt=10): 477 (x @ y) @ x' * y = e. [para(186(a,1),457(a,1,1)),rewrite(131(4),83(4))]. given #101 (A,wt=16): 56 (x' @ y) * x * z = x * (y @ x) * z. [para(9(a,1),9(a,1,2)),rewrite(32(5)),flip(a)]. given #102 (F,wt=18): 1189 B' * A' @ C' != (C @ A') * (C @ B') # answer(D). [para(570(a,2),810(a,1)),rewrite(131(4))]. given #103 (F,wt=19): 652 C' * A * C * A' * (B @ C) != A * B @ C # answer(D). [para(9(a,2),578(a,1)),rewrite(83(5))]. given #104 (T,wt=10): 487 (x' @ y) @ x * y = e. [para(154(a,1),478(a,1,1))]. given #105 (T,wt=10): 515 x * y @ (x' @ y) = e. [para(154(a,1),486(a,1,2))]. given #106 (A,wt=18): 63 x' * y * z * x = y * z * (y * z @ x). [para(10(a,1),8(a,1,2)),rewrite(32(6),1(4)),flip(a)]. given #107 (F,wt=18): 1532 (C @ A' * (B @ C)) * (B @ C) != A * B @ C # answer(D). [para(49(a,2),652(a,1,2)),rewrite(1(19),488(18),79(20),1427(16),8(17))]. given #108 (F,wt=17): 1644 ((C @ B) * A @ C) * (B @ C) != A * B @ C # answer(D). [para(570(a,2),1532(a,1,1)),rewrite(131(7),132(4),83(6))]. given #109 (T,wt=10): 523 (x @ y') * (x @ y) = e. [para(460(a,1),5(a,2)),rewrite(132(3),48(6),8(6))]. given #110 (T,wt=10): 586 (x @ y) * (x' @ y) = e. [para(481(a,1),141(a,1,1))]. given #111 (A,wt=21): 68 x' * y' * x * y * z @ u = (x @ y) * z @ u. [para(9(a,2),10(a,2,1)),rewrite(10(9)),flip(a)]. given #112 (F,wt=18): 1647 ((B' @ C) * A @ C) * (B @ C) != A * B @ C # answer(D). [para(481(a,2),1644(a,1,1,1,1)),rewrite(596(4,R))]. given #113 (F,wt=18): 1648 ((C @ B) * A @ C) * (C @ B') != A * B @ C # answer(D). [para(481(a,2),1644(a,1,2))]. given #114 (T,wt=10): 587 (x' @ y) * (x @ y) = e. [para(481(a,1),141(a,1,2))]. given #115 (T,wt=10): 589 (x @ y) @ (x' @ y) = e. [para(481(a,1),174(a,1,1))]. given #116 (A,wt=14): 76 x' * y * x * y' = x @ y'. [para(32(a,1),5(a,1,2))]. given #117 (F,wt=18): 1650 (C' @ (C @ B) * A) * (B @ C) != A * B @ C # answer(D). [para(570(a,2),1644(a,1,1))]. given #118 (F,wt=18): 1651 C' @ A * B != ((C @ B) * A @ C) * (B @ C) # answer(D). [para(570(a,2),1644(a,2)),flip(a)]. given #119 (T,wt=10): 590 (x @ y) @ (y @ x') = e. [para(481(a,1),174(a,1,2)),rewrite(585(4))]. given #120 (T,wt=10): 591 (x @ y) @ (y' @ x) = e. [para(481(a,2),174(a,1,1)),rewrite(585(4))]. given #121 (A,wt=14): 77 x * y' * x' * y = x' @ y. [para(32(a,1),5(a,1))]. given #122 (F,wt=19): 1248 A' * (C @ A') * A * (B @ C) != A * B @ C # answer(D). [para(54(a,1),51(a,1,2))]. given #123 (F,wt=19): 1640 (C @ A' * (C @ B')) * (B @ C) != A * B @ C # answer(D). [para(481(a,2),1532(a,1,1,2,2))]. given #124 (T,wt=10): 592 (x @ y) @ (x @ y') = e. [para(481(a,2),174(a,1,2))]. given #125 (T,wt=10): 603 (x @ y') @ x * y = e. [para(481(a,2),359(a,1,1))]. given #126 (A,wt=18): 81 x' * y * x * y' * z = (x @ y') * z. [para(32(a,1),9(a,1,2))]. given #127 (F,wt=19): 1641 (A' * (B @ C) @ C') * (B @ C) != A * B @ C # answer(D). [para(481(a,2),1532(a,1,1))]. given #128 (F,wt=19): 1642 (C @ A' * (B @ C)) * (C @ B') != A * B @ C # answer(D). [para(481(a,2),1532(a,1,2))]. given #129 (T,wt=10): 663 (x @ y) @ x * y' = e. [para(570(a,1),359(a,1,1))]. given #130 (T,wt=10): 689 (x @ y) @ y * x' = e. [para(481(a,1),373(a,1,1))]. given #131 (A,wt=18): 82 (x' @ y) * z = x * y' * x' * y * z. [para(32(a,1),9(a,1)),flip(a)]. given #132 (F,wt=19): 1645 C' @ A * B != (C @ A' * (B @ C)) * (B @ C) # answer(D). [para(570(a,2),1532(a,2)),flip(a)]. given #133 (F,wt=19): 1649 C @ B' * A' != ((C @ B) * A @ C) * (B @ C) # answer(D). [para(481(a,2),1644(a,2)),rewrite(131(16)),flip(a)]. given #134 (T,wt=10): 692 (x' @ y) @ y * x = e. [para(570(a,2),373(a,1,1))]. given #135 (T,wt=10): 730 x @ y * x * y' = e. [para(8(a,1),402(a,1,1)),rewrite(1(3))]. given #136 (A,wt=14): 87 x' * y' * x = (x @ y) * y'. [para(74(a,1),9(a,1,2,2,2)),rewrite(35(4))]. given #137 (F,wt=19): 1753 ((B' @ C) * A @ C) * (C @ B') != A * B @ C # answer(D). [para(481(a,2),1647(a,1,2))]. given #138 (F,wt=19): 1756 C' @ A * B != ((B' @ C) * A @ C) * (B @ C) # answer(D). [para(570(a,2),1647(a,2)),flip(a)]. given #139 (T,wt=10): 731 x * y * x' @ y = e. [para(8(a,1),402(a,1,2)),rewrite(1(3))]. given #140 (T,wt=10): 1220 x * y @ (x @ y') = e. [para(461(a,1),186(a,2)),rewrite(132(3),662(4))]. given #141 (A,wt=19): 90 x * y * y * x * z = y * x * x * y * z. [para(2(a,1),14(a,1,2,2)),rewrite(2(8))]. given #142 (F,wt=19): 1759 (C' @ (C @ B) * A) * (C @ B') != A * B @ C # answer(D). [para(570(a,2),1648(a,1,1))]. given #143 (F,wt=19): 1760 C' @ A * B != ((C @ B) * A @ C) * (C @ B') # answer(D). [para(570(a,2),1648(a,2)),flip(a)]. given #144 (T,wt=10): 1233 x * y @ (y' @ x) = e. [para(596(a,2),461(a,1,2))]. given #145 (T,wt=11): 255 x @ y * x' = y @ x'. [para(83(a,1),221(a,1,1))]. given #146 (A,wt=22): 91 x' * y * z * y = y * x' * z * x' * y * x. [para(3(a,1),14(a,1,2,2,2,2)),rewrite(35(3))]. given #147 (F,wt=19): 1796 C * A' * C' * A * (B @ C) != A * B @ C # answer(D). [para(9(a,2),1650(a,1)),rewrite(83(3),131(7),132(7),1(18),1(20),1133(19))]. given #148 (F,wt=19): 1798 (C' @ (C @ B) * A) * (B @ C) != C' @ A * B # answer(D). [para(570(a,2),1650(a,2))]. given #149 (T,wt=11): 323 x * y' @ y * x' = e. [para(83(a,1),216(a,1,1,1))]. given #150 (T,wt=11): 324 x' * y @ y' * x = e. [para(83(a,1),216(a,1,1,2))]. given #151 (A,wt=19): 94 x' * y' * z * (y @ x) = y' * x' * z. [para(5(a,1),14(a,1,2,2,2)),rewrite(8(12),3(10),35(10))]. given #152 (F,wt=14): 2531 (B @ C) * (C @ A') != A * B @ C # answer(D). [back_rewrite(1847),rewrite(2508(7),2407(12),2407(13),1(13),2(14),8(13))]. given #153 (F,wt=15): 2532 C' @ A * B != (B @ C) * (C @ A') # answer(D). [back_rewrite(1846),rewrite(2407(18),1(18),8(19))]. given #154 (T,wt=7): 2508 x @ (y @ z) = e. [back_rewrite(173),rewrite(2406(5),3(2)),flip(a)]. given #155 (T,wt=7): 2602 (x @ y) @ z = e. [back_rewrite(1465),rewrite(2508(3),2(5),471(4)),flip(a)]. given #156 (A,wt=13): 95 x * y' * (x @ y) = y' * x. [para(5(a,1),14(a,1,2,2)),rewrite(3(8),35(8),3(7),35(7))]. given #157 (F,wt=16): 2533 C @ B' * A' != (B @ C) * (C @ A') # answer(D). [back_rewrite(1845),rewrite(2407(19),1(19),8(20))]. given #158 (F,wt=17): 2520 B' * A' @ C' != (B @ C) * (C @ A') # answer(D). [back_rewrite(2062),rewrite(2407(15,R),1362(16),2407(16,R))]. given #159 (T,wt=11): 378 x' * y' @ x * y = e. [para(235(a,1),221(a,1,2)),rewrite(131(2),359(8))]. given #160 (T,wt=11): 413 x * y @ x' * y' = e. [back_rewrite(375),rewrite(401(3)),flip(a)]. given #161 (A,wt=23): 96 x * y * y * y * x * x = y * y * x * x * x * y. [para(6(a,1),14(a,1,2)),flip(a)]. given #162 (F,wt=17): 2557 (B @ C) * (A * (C @ B) @ C) != A * B @ C # answer(D). [back_rewrite(1644),rewrite(2407(5),2407(11,R))]. given #163 (F,wt=18): 2551 C' @ A * B != (B @ C) * (A * (C @ B) @ C) # answer(D). [back_rewrite(1651),rewrite(2407(11),2407(17,R))]. given #164 (T,wt=11): 431 x @ y * (y @ x) = x @ y. [back_rewrite(267),rewrite(427(5))]. given #165 (T,wt=11): 463 x' * y * x @ y' = e. [back_rewrite(180),rewrite(457(8))]. given #166 (A,wt=24): 97 x' * y * x * z * x * y * u = y * z * y * x * u. [para(14(a,1),8(a,1,2))]. given #167 (F,wt=18): 2552 (B @ C) * (C' @ A * (C @ B)) != A * B @ C # answer(D). [back_rewrite(1650),rewrite(2407(7),2407(12,R))]. given #168 (F,wt=18): 2554 (A * (C @ B) @ C) * (C @ B') != A * B @ C # answer(D). [back_rewrite(1648),rewrite(2407(5))]. given #169 (T,wt=11): 484 x' @ y' * x * y = e. [back_rewrite(205),rewrite(473(8))]. given #170 (T,wt=11): 613 x * (x @ y) @ y = x @ y. [back_rewrite(275),rewrite(594(5))]. given #171 (A,wt=20): 98 x * y * x' * y * x * z = y * x * y * z. [para(8(a,1),14(a,1,2,2)),flip(a)]. given #172 (F,wt=18): 2555 (B @ C) * (A * (B' @ C) @ C) != A * B @ C # answer(D). [back_rewrite(1647),rewrite(2407(6),2407(12,R))]. given #173 (F,wt=19): 2536 (B @ C) * (C' @ A * (C @ B)) != C' @ A * B # answer(D). [back_rewrite(1798),rewrite(2407(7),2407(12,R))]. given #174 (T,wt=11): 931 (x @ y') * (y @ x') = e. [para(596(a,1),141(a,1,1))]. given #175 (T,wt=11): 932 (x' @ y) * (y' @ x) = e. [para(596(a,2),141(a,1,1))]. given #176 (A,wt=22): 99 x' * y * x * y * x' * z = y * x' * y * z. [para(8(a,1),14(a,1,2)),flip(a)]. given #177 (F,wt=19): 2542 C' @ A * B != (A * (C @ B) @ C) * (C @ B') # answer(D). [back_rewrite(1760),rewrite(2407(11))]. given #178 (F,wt=19): 2543 (C @ B') * (C' @ A * (C @ B)) != A * B @ C # answer(D). [back_rewrite(1759),rewrite(2407(7),2407(13,R))]. given #179 (T,wt=11): 994 x' * y @ x * y' = e. [para(50(a,2),160(a,1,1)),rewrite(131(5),83(4),585(9,R),689(9))]. given #180 (T,wt=11): 999 x * y' @ x' * y = e. [para(50(a,2),221(a,1,2)),rewrite(131(3),83(2),663(9))]. given #181 (A,wt=19): 100 (x @ y) * z * y * x * u = z * x * y * u. [para(14(a,1),9(a,1,2,2)),rewrite(8(8),8(6)),flip(a)]. given #182 (F,wt=13): 3248 C @ A' * B' != A * B @ C # answer(D). [back_rewrite(653),rewrite(3238(9))]. given #183 (F,wt=11): 3250 B * A @ C != A * B @ C # answer(D). [para(570(a,2),3248(a,1)),rewrite(131(6),83(3),83(4))]. given #184 (T,wt=11): 1362 x @ (y @ x) * z = x @ z. [para(56(a,2),5(a,1,2,2)),rewrite(131(4),132(4),1(9),597(8),5(5)),flip(a)]. given #185 (T,wt=11): 2406 (x @ y) * z * (y @ x) = z. [para(94(a,1),9(a,1,2,2)),rewrite(83(2),83(2),79(5),79(3),588(3)),flip(a)]. given #186 (A,wt=23): 102 x' * y' * z * (y @ x) * u = y' * x' * z * u. [para(9(a,1),14(a,1,2,2,2)),rewrite(8(14),8(12))]. given #187 (F,wt=12): 3252 C' @ B * A != A * B @ C # answer(D). [para(570(a,2),3250(a,1))]. given #188 (F,wt=12): 3253 C' @ A * B != B * A @ C # answer(D). [para(570(a,2),3250(a,2)),flip(a)]. given #189 (T,wt=11): 2407 (x @ y) * z = z * (x @ y). [para(94(a,2),9(a,1,2,2)),rewrite(83(2),83(2),79(7),79(5),588(5)),flip(a)]. given #190 (T,wt=11): 2645 (x @ y) * y * x = x * y. [back_rewrite(881),rewrite(2614(7))]. given #191 (A,wt=17): 103 x * y' * (x @ y) * z = y' * x * z. [para(9(a,1),14(a,1,2,2)),rewrite(8(10),8(9))]. given #192 (F,wt=13): 3251 C @ B' * A' != B * A @ C # answer(D). [para(481(a,2),3250(a,2)),rewrite(131(10)),flip(a)]. given #193 (F,wt=13): 3420 C' @ B * A != C' @ A * B # answer(D). [para(570(a,2),3252(a,2))]. given #194 (T,wt=11): 3254 x @ (x @ y) * z = x @ z. [para(79(a,1),1362(a,1,2)),rewrite(132(3)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.68 (+ 0.01) seconds: D. % Length of proof is 89. % Level of proof is 22. % Maximum clause weight is 23. % Given clauses 194. 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 * y * x = y * x * z * x * y. [assumption]. 7 (A @ C) * (B @ C) != A * B @ C # answer(D). [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 * y * x * u = y * x * z * x * y * u. [para(6(a,1),1(a,1,1)),rewrite(1(5),1(4),1(3),1(2),1(9),1(8),1(7))]. 18 x * y * y * x = y * x * x * y. [para(2(a,1),6(a,1,2,2)),rewrite(2(6))]. 20 x * y * (x * y)' * y * x = y * x * e. [para(3(a,1),6(a,1,2,2)),flip(a)]. 24 x'' * e = x. [para(3(a,1),8(a,1,2))]. 27 x'' * (x @ y) = y' * x * y. [para(5(a,1),8(a,1,2))]. 32 x'' * y = x * y. [para(8(a,1),8(a,1,2))]. 33 x' * y * x = y * (y @ x). [back_rewrite(27),rewrite(32(4)),flip(a)]. 35 x * e = x. [back_rewrite(24),rewrite(32(4))]. 37 x * y * (x * y)' * y * x = y * x. [back_rewrite(20),rewrite(35(8))]. 46 x' * y * x * (y @ z) = (x @ y') * z' * y * z. [para(5(a,1),9(a,1,2,2,2)),rewrite(32(6))]. 48 (x' @ y) * x = x * (y @ x). [para(5(a,1),9(a,1,2)),rewrite(32(4)),flip(a)]. 49 (x @ y) * z * y * x = z * x * y. [para(6(a,1),9(a,1,2,2)),rewrite(8(7),8(5)),flip(a)]. 56 (x' @ y) * x * z = x * (y @ x) * z. [para(9(a,1),9(a,1,2)),rewrite(32(5)),flip(a)]. 57 e' = e. [para(35(a,1),3(a,1))]. 60 (x * y')' * y' * x = x * y' @ y. [para(3(a,1),10(a,1,2,2,2)),rewrite(35(6))]. 65 (x * y)' * y * x = x * y @ x. [para(8(a,1),10(a,1,2))]. 70 x * y' @ y = x * y' @ x. [back_rewrite(60),rewrite(65(6)),flip(a)]. 71 x * y * (x * y @ x) = y * x. [back_rewrite(37),rewrite(65(4))]. 74 x * x' = e. [para(32(a,1),3(a,1))]. 76 x' * y * x * y' = x @ y'. [para(32(a,1),5(a,1,2))]. 79 x * x' * y = y. [para(32(a,1),8(a,1))]. 83 x'' = x. [para(32(a,1),35(a,1)),rewrite(35(2)),flip(a)]. 86 x * y * (x * y)' = e. [para(74(a,1),1(a,1)),flip(a)]. 89 x * y @ y' = x * y @ x. [para(74(a,1),10(a,1,2,2,2)),rewrite(83(4),35(4),65(4)),flip(a)]. 94 x' * y' * z * (y @ x) = y' * x' * z. [para(5(a,1),14(a,1,2,2,2)),rewrite(8(12),3(10),35(10))]. 100 (x @ y) * z * y * x * u = z * x * y * u. [para(14(a,1),9(a,1,2,2)),rewrite(8(8),8(6)),flip(a)]. 118 x * (y * x)' = y'. [para(86(a,1),8(a,1,2)),rewrite(35(3)),flip(a)]. 120 (x @ y) * z * (x' * y' * x * y * z)' = e. [para(9(a,2),86(a,1,2,2,1))]. 131 (x * y)' = y' * x'. [para(118(a,1),8(a,1,2)),flip(a)]. 132 (x @ y)' = y @ x. [para(9(a,2),118(a,1,2,1)),rewrite(131(7),131(5),131(3),131(2),1(5),83(7),1(6),1(5),83(8),1(7),1(6),1(5),5(6),79(4)),flip(a)]. 141 (x @ y) * (y @ x) = e. [back_rewrite(120),rewrite(131(8),131(6),131(4),131(3),1(6),83(8),1(7),1(6),83(9),1(8),1(7),1(6),5(7),79(5))]. 147 x * y @ x = y @ x. [back_rewrite(65),rewrite(131(2),1(5),5(5)),flip(a)]. 160 x * y @ y' = y @ x. [back_rewrite(89),rewrite(147(5))]. 161 x * y * (y @ x) = y * x. [back_rewrite(71),rewrite(147(2))]. 162 x * y' @ y = y' @ x. [back_rewrite(70),rewrite(147(6))]. 175 (x @ y) * (y @ x) * z = z. [para(132(a,1),8(a,1,1))]. 182 x * y @ x' = y @ x'. [para(8(a,1),147(a,1,1)),flip(a)]. 186 x' * y @ x = y @ x. [para(79(a,1),147(a,1,1)),flip(a)]. 188 x @ x * y = x @ y. [para(147(a,1),132(a,1,1)),rewrite(132(2)),flip(a)]. 205 x' @ y' * x * y = x' @ (x @ y). [para(5(a,1),188(a,1,2)),flip(a)]. 221 x' @ y * x = y @ x. [para(160(a,1),132(a,1,1)),rewrite(132(2)),flip(a)]. 235 (x @ y) * y * x = x * y. [para(18(a,1),9(a,1,2,2)),rewrite(8(6),8(4)),flip(a)]. 255 x @ y * x' = y @ x'. [para(83(a,1),221(a,1,1))]. 359 (x @ y) @ y * x = e. [para(235(a,1),5(a,1,2,2)),rewrite(132(2),131(3),1(6),5(6),141(3)),flip(a)]. 361 (x' @ (x @ y)) * (y @ x') = x @ y. [para(5(a,1),235(a,2)),rewrite(205(5),1(8),1(7),76(8))]. 399 (x @ y) @ x = e. [para(79(a,1),359(a,1,2)),rewrite(186(3))]. 417 x @ (x @ y) = e. [para(399(a,1),132(a,1,1)),rewrite(57(2)),flip(a)]. 420 (x @ y) * x = x * (x @ y). [para(399(a,1),161(a,1,2,2)),rewrite(35(3)),flip(a)]. 457 (x @ y) @ x' = e. [para(417(a,1),160(a,2)),rewrite(420(2),182(4))]. 460 (x' @ y) @ x = e. [para(417(a,1),162(a,2)),rewrite(420(4),186(5))]. 473 x' @ (x @ y) = e. [para(457(a,1),132(a,1,1)),rewrite(57(2)),flip(a)]. 478 (x @ y) @ y = e. [para(221(a,1),457(a,1,1)),rewrite(83(3))]. 481 x @ y' = y @ x. [back_rewrite(361),rewrite(473(3),2(4))]. 488 (x @ y) * y = y * (x @ y). [para(478(a,1),161(a,1,2,2)),rewrite(35(3)),flip(a)]. 570 x' @ y = y @ x. [para(460(a,1),33(a,2,2)),rewrite(48(4),8(4),35(5)),flip(a)]. 578 (C @ A') * (B @ C) != A * B @ C # answer(D). [para(481(a,2),7(a,1,1))]. 588 x' @ y' = x @ y. [para(481(a,2),147(a,1)),rewrite(131(2),255(4))]. 593 x * y @ z = z @ y' * x'. [para(131(a,1),481(a,1,2)),flip(a)]. 597 (x @ y) * (x' @ y) * z = z. [para(481(a,1),175(a,1,1))]. 652 C' * A * C * A' * (B @ C) != A * B @ C # answer(D). [para(9(a,2),578(a,1)),rewrite(83(5))]. 696 x' * (y @ x') * z' * x * z = (x @ y) * (x @ z). [para(46(a,1),9(a,1,2))]. 719 x' * y * x * (y @ z) = (y @ x) * z' * y * z. [para(481(a,1),46(a,2,1))]. 1362 x @ (y @ x) * z = x @ z. [para(56(a,2),5(a,1,2,2)),rewrite(131(4),132(4),1(9),597(8),5(5)),flip(a)]. 1427 (x @ y) * x * z = x * (x @ y) * z. [para(570(a,1),56(a,2,2,1)),rewrite(588(3))]. 1532 (C @ A' * (B @ C)) * (B @ C) != A * B @ C # answer(D). [para(49(a,2),652(a,1,2)),rewrite(1(19),488(18),79(20),1427(16),8(17))]. 1640 (C @ A' * (C @ B')) * (B @ C) != A * B @ C # answer(D). [para(481(a,2),1532(a,1,1,2,2))]. 1850 (C @ A' * (C @ B')) * (C @ B') != A * B @ C # answer(D). [para(481(a,2),1640(a,1,2))]. 2407 (x @ y) * z = z * (x @ y). [para(94(a,2),9(a,1,2,2)),rewrite(83(2),83(2),79(7),79(5),588(5)),flip(a)]. 2529 (C @ B') * (C @ A' * (C @ B')) != A * B @ C # answer(D). [back_rewrite(1850),rewrite(2407(14,R))]. 3118 (x @ y) * z' * x * z = x * (x @ y * z). [para(100(a,2),33(a,1)),rewrite(131(3),1(7),8(6))]. 3204 x' * y * x * (y @ z) = y * (y @ x * z). [back_rewrite(719),rewrite(3118(10))]. 3221 (x @ y') * z' * y * z = y * (y @ x * z). [back_rewrite(46),rewrite(3204(5)),flip(a)]. 3238 (x @ y) * (x @ z) = x @ y * z. [back_rewrite(696),rewrite(3221(7),8(5)),flip(a)]. 3241 C @ B' * A' * (C @ B') != A * B @ C # answer(D). [back_rewrite(2529),rewrite(3238(14))]. 3254 x @ (x @ y) * z = x @ z. [para(79(a,1),1362(a,1,2)),rewrite(132(3)),flip(a)]. 3438 (x @ y) * (z @ u) * y * x = x * y * (z @ u). [para(2407(a,1),49(a,2)),rewrite(1(8))]. 3574 x @ y * z * (x @ u) = x @ y * z. [para(49(a,2),3254(a,1,2)),rewrite(3438(5))]. 3594 C @ B' * A' != A * B @ C # answer(D). [back_rewrite(3241),rewrite(3574(12))]. 3595 $F # answer(D). [resolve(3594,a,593,a(flip))]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=194. Generated=23157. Kept=3593. proofs=1. Usable=118. Sos=1771. Demods=974. Limbo=20, Disabled=1689. Hints=0. Weight_deleted=6348. Literals_deleted=0. Forward_subsumed=13216. Back_subsumed=652. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=2142 (3 lex), Back_demodulated=1031. Back_unit_deleted=0. Demod_attempts=407000. Demod_rewrites=70839. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=2.76. User_CPU=0.68, System_CPU=0.01, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3866 exit (max_proofs) Wed Nov 22 11:24:23 2006