============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 3851 was started by mccune on cleo.thornwood, Wed Nov 22 11:24:06 2006 The command was "/home/mccune/bin/prover9 -f gt.in AD.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 AD.in formulas(sos). (x @ y) @ z = u @ (v @ w). 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 = u @ (v @ w). [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 = u @ (v @ w). [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=11): 6 (x @ y) @ z = u @ (v @ w). [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=5): 19 x @ e = e. [back_rewrite(17),rewrite(18(2)),flip(a)]. given #9 (T,wt=6): 12 x' @ x = e. [para(3(a,1),5(a,1,2,2)),rewrite(8(6)),flip(a)]. given #10 (T,wt=7): 16 x @ (y @ z) = e. [para(11(a,1),6(a,1,1)),rewrite(11(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 = e. [para(8(a,1),5(a,1,2)),rewrite(3(2)),flip(a)]. given #13 (F,wt=5): 29 x * e = x. [back_rewrite(22),rewrite(26(4))]. given #14 (T,wt=4): 31 e' = e. [para(29(a,1),3(a,1))]. given #15 (T,wt=7): 18 (x @ y) @ z = e. [para(11(a,1),6(a,2))]. 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=19): 41 A' * C' * A * C * (B @ C) != A * B @ C # answer(D). [para(9(a,2),7(a,1))]. given #18 (F,wt=9): 26 x'' * y = x * y. [para(8(a,1),8(a,1,2))]. given #19 (T,wt=5): 56 x'' = x. [para(26(a,1),29(a,1)),rewrite(29(2)),flip(a)]. given #20 (T,wt=6): 51 x * x' = e. [para(26(a,1),3(a,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=6): 59 x @ x' = e. [para(56(a,1),12(a,1,1))]. given #23 (F,wt=7): 75 x * x @ x = e. [para(10(a,1),10(a,1,2)),rewrite(3(2),31(2),2(4),3(4),11(5))]. given #24 (T,wt=8): 55 x * x' * y = y. [para(26(a,1),8(a,1))]. given #25 (T,wt=10): 60 x * y * (x * y)' = e. [para(51(a,1),1(a,1)),flip(a)]. given #26 (A,wt=12): 20 (x * y)' * x * y * z = z. [para(1(a,1),8(a,1,2))]. given #27 (F,wt=7): 93 x @ x * x = e. [para(20(a,1),5(a,1,2)),rewrite(3(2)),flip(a)]. given #28 (F,wt=9): 84 x * (y * x)' = y'. [para(60(a,1),8(a,1,2)),rewrite(29(3)),flip(a)]. given #29 (T,wt=8): 114 (x @ y)' = y @ x. [para(9(a,2),84(a,1,2,1)),rewrite(113(7),113(5),113(3),113(2),1(5),56(7),1(6),1(5),56(8),1(7),1(6),1(5),5(6),55(4)),flip(a)]. given #30 (T,wt=9): 127 (x @ y) * (y @ x) = e. [back_rewrite(86),rewrite(113(8),113(6),113(4),113(3),1(6),56(8),1(7),1(6),56(9),1(8),1(7),1(6),5(7),55(5))]. given #31 (A,wt=12): 27 x' * y * x = y * (y @ x). [back_rewrite(25),rewrite(26(4)),flip(a)]. given #32 (F,wt=9): 131 x * y @ x = y @ x. [back_rewrite(69),rewrite(113(2),1(5),5(5)),flip(a)]. given #33 (F,wt=9): 155 x @ y * x = x @ y. [back_rewrite(148),rewrite(154(4)),flip(a)]. given #34 (T,wt=8): 184 x' @ y = y @ x. [back_rewrite(180),rewrite(181(3))]. given #35 (T,wt=8): 185 x @ y' = y @ x. [back_rewrite(177),rewrite(181(2)),flip(a)]. given #36 (A,wt=21): 32 x * y' * z' * y * z * u = x * (y @ z) * u. [para(9(a,1),1(a,2,2)),rewrite(1(7))]. given #37 (F,wt=14): 188 C' @ A * B != (A @ C) * (B @ C) # answer(D). [para(184(a,2),7(a,2)),flip(a)]. given #38 (F,wt=14): 204 (C @ A') * (B @ C) != A * B @ C # answer(D). [para(185(a,2),7(a,1,1))]. given #39 (T,wt=9): 173 x @ x * y = x @ y. [para(131(a,1),114(a,1,1)),rewrite(114(2)),flip(a)]. given #40 (T,wt=9): 181 x * y @ y = x @ y. [para(155(a,1),114(a,1,1)),rewrite(114(2)),flip(a)]. given #41 (A,wt=13): 35 x' * y * x = (x @ y') * y. [para(3(a,1),9(a,1,2,2,2)),rewrite(29(5),26(4))]. given #42 (F,wt=14): 205 (A @ C) * (C @ B') != A * B @ C # answer(D). [para(185(a,2),7(a,1,2))]. given #43 (F,wt=15): 206 C @ B' * A' != (A @ C) * (B @ C) # answer(D). [para(185(a,2),7(a,2)),rewrite(113(12)),flip(a)]. given #44 (T,wt=9): 199 x' @ y' = x @ y. [para(184(a,2),184(a,1))]. given #45 (T,wt=9): 215 x' @ y = x @ y'. [para(185(a,1),184(a,1)),flip(a)]. given #46 (A,wt=22): 38 x' * y * x * (y @ z) = (x @ y') * z' * y * z. [para(5(a,1),9(a,1,2,2,2)),rewrite(26(6))]. given #47 (F,wt=15): 231 C' @ A * B != (C @ A') * (B @ C) # answer(D). [para(184(a,2),188(a,2,1)),rewrite(215(10))]. given #48 (F,wt=15): 232 C' @ A * B != (A @ C) * (C @ B') # answer(D). [para(184(a,2),188(a,2,2)),rewrite(215(13))]. given #49 (T,wt=10): 113 (x * y)' = y' * x'. [para(84(a,1),8(a,1,2)),flip(a)]. given #50 (T,wt=10): 147 x * y @ y' = y @ x. [back_rewrite(74),rewrite(131(5))]. given #51 (A,wt=12): 40 (x' @ y) * x = x * (y @ x). [para(5(a,1),9(a,1,2)),rewrite(26(4)),flip(a)]. given #52 (F,wt=15): 234 (C @ A') * (C @ B') != A * B @ C # answer(D). [para(184(a,2),204(a,1,2)),rewrite(215(8))]. given #53 (F,wt=16): 230 B' * A' @ C' != (A @ C) * (B @ C) # answer(D). [para(184(a,2),188(a,1)),rewrite(113(4))]. given #54 (T,wt=10): 157 x' @ y * x = y @ x. [para(27(a,1),5(a,1,2,2)),rewrite(56(2),113(2),1(6),8(5),55(4)),flip(a)]. given #55 (T,wt=10): 172 x' * y @ x = y @ x. [para(55(a,1),131(a,1,1)),flip(a)]. given #56 (A,wt=16): 43 x' * y * x * z = y * (y @ x) * z. [para(9(a,1),8(a,1,2)),rewrite(26(5)),flip(a)]. given #57 (F,wt=14): 410 (B @ C) * (C @ A') != A * B @ C # answer(D). [back_rewrite(204),rewrite(367(8,R))]. given #58 (F,wt=15): 409 C' @ A * B != (B @ C) * (C @ A') # answer(D). [back_rewrite(231),rewrite(367(14,R))]. given #59 (T,wt=10): 175 x' * y * x @ y = e. [para(27(a,2),131(a,1,1)),rewrite(18(6))]. given #60 (T,wt=10): 193 (x @ y) * (x @ y') = e. [para(184(a,1),127(a,1,1))]. given #61 (A,wt=17): 45 x' * y * x * z = (x @ y') * y * z. [para(8(a,1),9(a,1,2,2,2)),rewrite(26(5))]. given #62 (F,wt=16): 261 C @ B' * A' != (A @ C) * (C @ B') # answer(D). [para(185(a,2),205(a,2)),rewrite(113(13)),flip(a)]. given #63 (F,wt=16): 301 C' @ A * B != (C @ A') * (C @ B') # answer(D). [para(184(a,2),231(a,2,2)),rewrite(215(14))]. given #64 (T,wt=10): 196 (x @ y) * (x' @ y) = e. [para(184(a,2),127(a,1,2))]. given #65 (T,wt=10): 240 x @ y' * x * y = e. [para(27(a,2),173(a,1,2)),rewrite(16(6))]. given #66 (A,wt=16): 48 (x' @ y) * x * z = x * (y @ x) * z. [para(9(a,1),9(a,1,2)),rewrite(26(5)),flip(a)]. given #67 (F,wt=16): 407 C @ B' * A' != (B @ C) * (C @ A') # answer(D). [back_rewrite(235),rewrite(367(15,R))]. given #68 (F,wt=17): 303 B' * A' @ C' != (A @ C) * (C @ B') # answer(D). [para(184(a,2),232(a,1)),rewrite(113(4))]. given #69 (T,wt=10): 418 x * y * x' @ y = e. [para(56(a,1),175(a,1,1,1))]. given #70 (T,wt=10): 487 x @ y * x * y' = e. [para(56(a,1),240(a,1,2,1))]. given #71 (A,wt=14): 53 x' * y * x * y' = x @ y'. [para(26(a,1),5(a,1,2))]. given #72 (F,wt=17): 335 C @ B' * A' != (C @ A') * (C @ B') # answer(D). [para(185(a,2),234(a,2)),rewrite(113(14)),flip(a)]. given #73 (F,wt=17): 404 B' * A' @ C' != (B @ C) * (C @ A') # answer(D). [back_rewrite(300),rewrite(367(16,R))]. given #74 (T,wt=11): 126 x * y * (y @ x) = y * x. [back_rewrite(95),rewrite(113(4),56(2),56(2),1(3))]. given #75 (T,wt=11): 138 x' @ x * y = x' @ y. [back_rewrite(28),rewrite(113(2),1(4),54(5)),flip(a)]. given #76 (A,wt=14): 54 x * y' * x' * y = x' @ y. [para(26(a,1),5(a,1))]. given #77 (F,wt=18): 476 B' * A' @ C' != (C @ A') * (C @ B') # answer(D). [para(184(a,2),301(a,1)),rewrite(113(4))]. given #78 (F,wt=19): 408 C' * A * C * (B @ C) * A' != A * B @ C # answer(D). [back_rewrite(233),rewrite(367(10,R))]. given #79 (T,wt=11): 146 x * y' @ y = y' @ x. [back_rewrite(76),rewrite(131(6))]. given #80 (T,wt=11): 153 (x @ y) * (y @ x) * z = z. [para(114(a,1),8(a,1,1))]. given #81 (A,wt=18): 57 x' * y * x * y' * z = (x @ y') * z. [para(26(a,1),9(a,1,2))]. given #82 (F,wt=18): 635 A * (A @ C) * (B @ C) * A' != A * B @ C # answer(D). [para(43(a,1),408(a,1))]. given #83 (F,wt=19): 636 (C @ A') * A * (B @ C) * A' != A * B @ C # answer(D). [para(45(a,1),408(a,1))]. given #84 (T,wt=11): 160 (x @ y) * z * (y @ x) = z. [para(16(a,1),27(a,2,2)),rewrite(114(2),29(6))]. given #85 (T,wt=11): 169 x' * y * x @ y' = e. [para(5(a,1),131(a,1,1)),rewrite(18(3)),flip(a)]. given #86 (A,wt=18): 58 (x' @ y) * z = x * y' * x' * y * z. [para(26(a,1),9(a,1)),flip(a)]. given #87 (F,wt=19): 684 A * (C @ A') * (B @ C) * A' != A * B @ C # answer(D). [para(184(a,2),635(a,1,2,1)),rewrite(215(5))]. given #88 (F,wt=19): 686 C' @ A * B != A * (A @ C) * (B @ C) * A' # answer(D). [para(184(a,2),635(a,2)),flip(a)]. given #89 (T,wt=11): 170 x * y @ x' = y @ x'. [para(8(a,1),131(a,1,1)),flip(a)]. given #90 (T,wt=11): 213 x @ x' * y = y @ x'. [para(185(a,1),131(a,1))]. given #91 (A,wt=14): 61 x' * y' * x = (x @ y) * y'. [para(51(a,1),9(a,1,2,2,2)),rewrite(29(4))]. given #92 (F,wt=20): 192 A' * C' * A * C * (B @ C) != C' @ A * B # answer(D). [para(184(a,2),41(a,2))]. given #93 (F,wt=20): 209 A' * C' * A * C * (C @ B') != A * B @ C # answer(D). [para(185(a,2),41(a,1,2,2,2,2))]. given #94 (T,wt=11): 248 x @ y * x' = y @ x'. [para(181(a,1),185(a,1)),flip(a)]. given #95 (T,wt=11): 268 (x @ y') * (y @ x') = e. [para(215(a,1),127(a,1,1))]. given #96 (A,wt=18): 67 x' * y * z * x = y * z * (y * z @ x). [para(10(a,1),8(a,1,2)),rewrite(56(3),1(4)),flip(a)]. given #97 (F,wt=20): 334 C' * A * C * A' * (C @ B') != A * B @ C # answer(D). [para(9(a,2),234(a,1)),rewrite(56(5))]. given #98 (F,wt=20): 405 C' * A * C * (B @ C) * A' != C' @ A * B # answer(D). [back_rewrite(299),rewrite(367(10,R))]. given #99 (T,wt=11): 269 (x' @ y) * (y' @ x) = e. [para(215(a,2),127(a,1,1))]. given #100 (T,wt=11): 305 x * y @ y' * x' = e. [para(113(a,1),59(a,1,2))]. given #101 (A,wt=21): 72 x' * y' * x * y * z @ u = (x @ y) * z @ u. [para(9(a,2),10(a,2,1)),rewrite(10(9)),flip(a)]. given #102 (F,wt=20): 412 B' * C' * B * C * (C @ A') != A * B @ C # answer(D). [para(9(a,2),410(a,1))]. given #103 (F,wt=19): 976 B' * C' * B * C * (A @ C) != A * B @ C # answer(D). [para(184(a,2),412(a,1,2,2,2,2)),rewrite(56(9))]. given #104 (T,wt=11): 367 (x @ y) * z = z * (x @ y). [para(127(a,1),43(a,1,2,2)),rewrite(114(2),29(3),16(4),2(5))]. given #105 (T,wt=11): 419 x @ y' * x' * y = e. [para(175(a,1),185(a,1)),flip(a)]. given #106 (A,wt=18): 79 x' * y' * x * z = (x @ y) * y' * z. [para(55(a,1),9(a,1,2,2,2))]. given #107 (F,wt=20): 687 C @ B' * A' != A * (A @ C) * (B @ C) * A' # answer(D). [para(185(a,2),635(a,2)),rewrite(113(17)),flip(a)]. given #108 (F,wt=20): 761 C' @ A * B != A * (C @ A') * (B @ C) * A' # answer(D). [para(184(a,2),684(a,2)),flip(a)]. given #109 (T,wt=11): 552 x @ y * x' * y' = e. [para(418(a,1),185(a,1)),flip(a)]. given #110 (T,wt=11): 814 x' * y' @ x * y = e. [back_rewrite(133),rewrite(813(12))]. given #111 (A,wt=24): 116 x' * y' * z * x * y * z' = y * x @ x' * z'. [para(84(a,1),10(a,1,2,2,2)),rewrite(113(2),113(5),113(7),56(5),56(5),1(7),1(8),113(11))]. given #112 (F,wt=16): 1110 C @ B' * C' * A' != A * B @ C # answer(D). [back_rewrite(975),rewrite(1081(14))]. ============================== PROOF ================================= % Proof 1 at 0.15 (+ 0.00) seconds: D. % Length of proof is 60. % Level of proof is 17. % Maximum clause weight is 25. % Given clauses 112. 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 = u @ (v @ w). [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))]. 11 e @ x = e. [para(2(a,1),5(a,1,2,2)),rewrite(3(4),3(4)),flip(a)]. 16 x @ (y @ z) = e. [para(11(a,1),6(a,1,1)),rewrite(11(2)),flip(a)]. 20 (x * y)' * x * y * z = z. [para(1(a,1),8(a,1,2))]. 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))]. 26 x'' * y = x * y. [para(8(a,1),8(a,1,2))]. 27 x' * y * x = y * (y @ x). [back_rewrite(25),rewrite(26(4)),flip(a)]. 29 x * e = x. [back_rewrite(22),rewrite(26(4))]. 43 x' * y * x * z = y * (y @ x) * z. [para(9(a,1),8(a,1,2)),rewrite(26(5)),flip(a)]. 51 x * x' = e. [para(26(a,1),3(a,1))]. 55 x * x' * y = y. [para(26(a,1),8(a,1))]. 56 x'' = x. [para(26(a,1),29(a,1)),rewrite(29(2)),flip(a)]. 60 x * y * (x * y)' = e. [para(51(a,1),1(a,1)),flip(a)]. 69 (x * y)' * y * x = x * y @ x. [para(8(a,1),10(a,1,2))]. 71 x' * (y * x @ y) * x = x @ y * x. [para(9(a,1),10(a,1,2)),rewrite(8(3),8(8))]. 72 x' * y' * x * y * z @ u = (x @ y) * z @ u. [para(9(a,2),10(a,2,1)),rewrite(10(9)),flip(a)]. 84 x * (y * x)' = y'. [para(60(a,1),8(a,1,2)),rewrite(29(3)),flip(a)]. 86 (x @ y) * z * (x' * y' * x * y * z)' = e. [para(9(a,2),60(a,1,2,2,1))]. 95 (x' * y')' * (x @ y) = x * y. [para(5(a,1),20(a,1,2))]. 113 (x * y)' = y' * x'. [para(84(a,1),8(a,1,2)),flip(a)]. 114 (x @ y)' = y @ x. [para(9(a,2),84(a,1,2,1)),rewrite(113(7),113(5),113(3),113(2),1(5),56(7),1(6),1(5),56(8),1(7),1(6),1(5),5(6),55(4)),flip(a)]. 116 x' * y' * z * x * y * z' = y * x @ x' * z'. [para(84(a,1),10(a,1,2,2,2)),rewrite(113(2),113(5),113(7),56(5),56(5),1(7),1(8),113(11))]. 126 x * y * (y @ x) = y * x. [back_rewrite(95),rewrite(113(4),56(2),56(2),1(3))]. 127 (x @ y) * (y @ x) = e. [back_rewrite(86),rewrite(113(8),113(6),113(4),113(3),1(6),56(8),1(7),1(6),56(9),1(8),1(7),1(6),5(7),55(5))]. 131 x * y @ x = y @ x. [back_rewrite(69),rewrite(113(2),1(5),5(5)),flip(a)]. 148 x' * (x @ y) * x = x @ y * x. [back_rewrite(71),rewrite(131(3))]. 154 x' * (y @ z) * x = y @ z. [para(127(a,1),9(a,1,2,2,2)),rewrite(114(3),29(4),16(6),2(7))]. 155 x @ y * x = x @ y. [back_rewrite(148),rewrite(154(4)),flip(a)]. 170 x * y @ x' = y @ x'. [para(8(a,1),131(a,1,1)),flip(a)]. 172 x' * y @ x = y @ x. [para(55(a,1),131(a,1,1)),flip(a)]. 177 x * y @ y = y @ x'. [para(8(a,1),155(a,1,2)),rewrite(170(5))]. 180 x' * y @ y = y @ x. [para(55(a,1),155(a,1,2)),rewrite(172(6))]. 181 x * y @ y = x @ y. [para(155(a,1),114(a,1,1)),rewrite(114(2)),flip(a)]. 184 x' @ y = y @ x. [back_rewrite(180),rewrite(181(3))]. 185 x @ y' = y @ x. [back_rewrite(177),rewrite(181(2)),flip(a)]. 204 (C @ A') * (B @ C) != A * B @ C # answer(D). [para(185(a,2),7(a,1,1))]. 362 (x @ y) * z * y' * x' * y * x * u = z * u. [para(9(a,2),43(a,1,2,2)),rewrite(114(2),16(11),2(11))]. 367 (x @ y) * z = z * (x @ y). [para(127(a,1),43(a,1,2,2)),rewrite(114(2),29(3),16(4),2(5))]. 399 x * (x @ y) * z @ y = x * y * z @ y. [para(43(a,1),172(a,1,1))]. 410 (B @ C) * (C @ A') != A * B @ C # answer(D). [back_rewrite(204),rewrite(367(8,R))]. 412 B' * C' * B * C * (C @ A') != A * B @ C # answer(D). [para(9(a,2),410(a,1))]. 902 (x @ y) * z @ u = z @ u. [para(72(a,1),5(a,2)),rewrite(113(7),113(5),113(3),113(2),1(5),56(7),1(6),1(5),56(8),1(7),1(6),1(5),5(6),1(11),1(10),1(9),1(8),1(13),362(12),5(5)),flip(a)]. 907 x' * y * x * z @ u = y * z @ u. [para(8(a,1),72(a,1,1,2,2,2)),rewrite(56(3),902(10))]. 908 x * (x @ y) * z @ u = x * z @ u. [para(9(a,1),72(a,1,1,2,2,2)),rewrite(56(3),907(7),902(12),907(9))]. 936 x * (y @ z) @ u = x @ u. [para(126(a,1),72(a,2,1)),rewrite(16(4),29(4),907(7),8(3)),flip(a)]. 952 x * y * z @ y = x * z @ y. [back_rewrite(399),rewrite(908(4)),flip(a)]. 975 B' * C' * B * A * C * A' != A * B @ C # answer(D). [para(27(a,2),412(a,1,2,2,2)),rewrite(56(8))]. 1081 x' * y' * x * z * y * z' = y @ x' * y' * z'. [para(27(a,1),116(a,2,1)),rewrite(113(2),56(5),1(8),55(7),1(8),113(12),1(15),936(16))]. 1110 C @ B' * C' * A' != A * B @ C # answer(D). [back_rewrite(975),rewrite(1081(14))]. 1113 $F # answer(D). [para(184(a,2),1110(a,1)),rewrite(113(9),113(6),56(3),56(4),56(6),1(5),952(7)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=112. Generated=6733. Kept=1111. proofs=1. Usable=91. Sos=587. Demods=324. Limbo=0, Disabled=439. Hints=0. Weight_deleted=469. Literals_deleted=0. Forward_subsumed=5152. Back_subsumed=39. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=630 (2 lex), Back_demodulated=394. Back_unit_deleted=0. Demod_attempts=100550. Demod_rewrites=20470. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.89. User_CPU=0.15, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3851 exit (max_proofs) Wed Nov 22 11:24:06 2006