============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11352 was started by mccune on cleo.thornwood, Sat Aug 12 20:59:51 2006 The command was "/home/mccune/bin/prover9 -f gt.in DA.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 DA.in formulas(sos). (x @ z) * (y @ z) = x * y @ z. end_of_list. formulas(sos). (A @ B) @ C != D @ (F @ G) # answer(A). 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 * z @ y. [assumption]. (A @ B) @ C != D @ (F @ G) # answer(A). [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, D, F, G, *, @, ' ]). After inverse_order: Function symbol precedence: lex([ e, A, B, C, D, F, G, *, ', @ ]). Folding symbols: @/2. After fold_eq: Function symbol precedence: lex([ e, A, B, C, D, F, G, @, *, ' ]). 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 * z @ y. [assumption]. 7 (A @ B) @ C != D @ (F @ G) # answer(A). [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 @ y) = x * z @ y. [assumption]. 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=13): 6 (x @ y) * (z @ y) = x * z @ y. [assumption]. given #6 (I,wt=11): 7 (A @ B) @ C != D @ (F @ G) # answer(A). [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): 23 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=5): 29 x * e = x. [back_rewrite(21),rewrite(26(4))]. given #13 (F,wt=4): 52 e' = e. [para(29(a,1),3(a,1))]. given #14 (T,wt=5): 53 x @ e = e. [para(29(a,1),5(a,1,2,2)),rewrite(52(3),2(3),3(2)),flip(a)]. given #15 (T,wt=9): 26 x'' * y = x * y. [para(8(a,1),8(a,1,2))]. 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=5): 62 x'' = x. [para(26(a,1),29(a,1)),rewrite(29(2)),flip(a)]. given #18 (F,wt=6): 54 x * x' = e. [para(26(a,1),3(a,1))]. given #19 (T,wt=6): 73 x @ x' = e. [para(62(a,1),12(a,1,1))]. given #20 (T,wt=8): 58 x * x' * y = y. [para(26(a,1),8(a,1))]. given #21 (A,wt=17): 14 (x * y @ z) * u = (x @ z) * (y @ z) * u. [para(6(a,1),1(a,1,1))]. given #22 (F,wt=8): 72 x' @ y = y @ x. [back_rewrite(64),rewrite(69(6))]. given #23 (F,wt=12): 98 (B' @ A) @ C != D @ (F @ G) # answer(A). [para(72(a,2),7(a,1,1))]. given #24 (T,wt=8): 80 x @ y' = y @ x. [para(73(a,1),6(a,1,2)),rewrite(29(4),78(5))]. given #25 (T,wt=9): 32 x * y @ x = y @ x. [para(23(a,1),6(a,1,1)),rewrite(2(3)),flip(a)]. given #26 (A,wt=23): 15 (x @ y)' * (z @ y)' * (x * z @ y) = (x @ y) @ (z @ y). [para(6(a,1),5(a,1,2,2))]. given #27 (F,wt=12): 99 C' @ (A @ B) != D @ (F @ G) # answer(A). [para(72(a,2),7(a,1))]. given #28 (F,wt=12): 121 (B @ A') @ C != D @ (F @ G) # answer(A). [para(80(a,2),7(a,1,1))]. given #29 (T,wt=9): 33 x * y @ y = x @ y. [para(23(a,1),6(a,1,2)),rewrite(29(3)),flip(a)]. given #30 (T,wt=9): 109 x' @ y' = x @ y. [para(72(a,2),72(a,1))]. given #31 (A,wt=10): 17 x' * y @ x = y @ x. [para(12(a,1),6(a,1,1)),rewrite(2(3)),flip(a)]. given #32 (F,wt=12): 123 D @ (G @ F') != (A @ B) @ C # answer(A). [para(80(a,2),7(a,2,2)),flip(a)]. given #33 (F,wt=12): 124 (F @ G) @ D' != (A @ B) @ C # answer(A). [para(80(a,2),7(a,2)),flip(a)]. given #34 (T,wt=7): 191 (x @ y) @ x = e. [para(5(a,1),17(a,1,1)),rewrite(139(6),3(4),11(4))]. given #35 (T,wt=7): 206 (x @ y) @ y = e. [para(80(a,1),191(a,1,1))]. given #36 (A,wt=12): 19 (x * y)' * x * y * z = z. [para(1(a,1),8(a,1,2))]. given #37 (F,wt=13): 132 C' @ (B @ A') != D @ (F @ G) # answer(A). [para(80(a,2),98(a,1)),rewrite(131(5),131(7,R))]. given #38 (F,wt=13): 133 D @ (G @ F') != (B @ A') @ C # answer(A). [para(80(a,2),98(a,2,2)),rewrite(131(4)),flip(a)]. given #39 (T,wt=8): 202 x' @ (x @ y) = e. [para(191(a,1),72(a,2))]. given #40 (T,wt=7): 247 x @ (y @ x) = e. [para(72(a,1),202(a,1,2)),rewrite(62(2))]. given #41 (A,wt=14): 25 (x @ y)' * (x * z @ y) = z @ y. [para(6(a,1),8(a,1,2))]. given #42 (F,wt=13): 134 (F @ G) @ D' != (B @ A') @ C # answer(A). [para(80(a,2),98(a,2)),rewrite(131(4)),flip(a)]. given #43 (F,wt=12): 305 (F @ G) @ D' != C @ (B @ A) # answer(A). [para(80(a,2),134(a,2)),rewrite(267(12),109(12))]. given #44 (T,wt=7): 250 x @ (x @ y) = e. [para(109(a,1),202(a,1,2)),rewrite(62(2))]. given #45 (T,wt=8): 203 (x @ y) @ y' = e. [para(72(a,1),191(a,1,1))]. given #46 (A,wt=12): 27 x' * y * x = y * (y @ x). [back_rewrite(24),rewrite(26(4)),flip(a)]. given #47 (F,wt=11): 307 D @ (F @ G) != C @ (B @ A) # answer(A). [para(72(a,2),305(a,1)),rewrite(62(3))]. given #48 (F,wt=12): 346 D @ (G @ F') != C @ (B @ A) # answer(A). [para(72(a,2),307(a,1,2)),rewrite(131(5))]. given #49 (T,wt=8): 205 x @ (x' @ y) = e. [para(191(a,1),80(a,1)),flip(a)]. given #50 (T,wt=8): 207 (x @ y') @ y = e. [para(80(a,2),191(a,1,1))]. given #51 (A,wt=10): 31 x * y' @ y = x @ y. [back_rewrite(18),rewrite(29(5))]. given #52 (F,wt=11): 350 (G @ F) @ D != C @ (B @ A) # answer(A). [para(72(a,2),346(a,1)),rewrite(267(5),109(5))]. given #53 (F,wt=12): 347 (F' @ G) @ D != C @ (B @ A) # answer(A). [para(72(a,2),307(a,1)),rewrite(267(4))]. given #54 (T,wt=8): 211 (x @ y) @ x' = e. [para(109(a,1),191(a,1,1))]. given #55 (T,wt=8): 218 x' @ (y @ x) = e. [para(206(a,1),72(a,2))]. given #56 (A,wt=21): 34 x * y' * z' * y * z * u = x * (y @ z) * u. [para(9(a,1),1(a,2,2)),rewrite(1(7))]. given #57 (F,wt=12): 348 C @ (A' @ B) != D @ (F @ G) # answer(A). [para(72(a,2),307(a,2,2)),flip(a)]. given #58 (F,wt=12): 349 (B @ A) @ C' != D @ (F @ G) # answer(A). [para(80(a,2),307(a,2)),flip(a)]. given #59 (T,wt=8): 219 (x' @ y) @ x = e. [para(72(a,2),206(a,1,1))]. given #60 (T,wt=8): 220 x @ (y @ x') = e. [para(206(a,1),80(a,1)),flip(a)]. given #61 (A,wt=23): 35 x' * (y * z)' * x * y * z * u = (x @ y * z) * u. [para(1(a,1),9(a,1,2,2,2))]. given #62 (F,wt=12): 372 D' @ (G @ F) != C @ (B @ A) # answer(A). [para(72(a,2),350(a,1))]. given #63 (F,wt=12): 373 C @ (A' @ B) != (G @ F) @ D # answer(A). [para(72(a,2),350(a,2,2)),flip(a)]. given #64 (T,wt=9): 131 x' @ y = x @ y'. [para(80(a,1),72(a,1)),flip(a)]. given #65 (T,wt=9): 177 x @ y * x = x @ y. [para(8(a,1),33(a,1,1)),rewrite(146(5))]. given #66 (A,wt=25): 36 (x * y)' * z' * x * y * z * u = (x @ z) * (y @ z) * u. [para(1(a,1),9(a,1,2,2)),rewrite(14(11))]. given #67 (F,wt=11): 453 (G @ F) @ D != (A @ B) @ C # answer(A). [para(72(a,2),373(a,1)),rewrite(267(5),62(3)),flip(a)]. given #68 (F,wt=12): 374 (B @ A') @ C != (G @ F) @ D # answer(A). [para(72(a,2),350(a,2)),rewrite(267(9),131(9)),flip(a)]. given #69 (T,wt=9): 208 (x @ y) @ y * x = e. [para(32(a,1),191(a,1,1))]. given #70 (T,wt=9): 210 (x @ y) @ x * y = e. [para(33(a,1),191(a,1,1))]. given #71 (A,wt=13): 38 x' * y * x = (x @ y') * y. [para(3(a,1),9(a,1,2,2,2)),rewrite(29(5),26(4))]. given #72 (F,wt=12): 375 (B @ A) @ C' != (G @ F) @ D # answer(A). [para(80(a,2),350(a,2)),flip(a)]. given #73 (F,wt=12): 466 (F' @ G) @ D != (A @ B) @ C # answer(A). [para(131(a,2),124(a,1)),rewrite(267(4))]. given #74 (T,wt=9): 237 (x * y)' * x = y'. [para(54(a,1),19(a,1,2,2)),rewrite(29(4))]. given #75 (T,wt=9): 267 (x @ y)' = x' @ y. [para(54(a,1),25(a,1,2,1)),rewrite(11(4),29(4))]. given #76 (A,wt=12): 43 (x' @ y) * x = x * (y @ x). [para(5(a,1),9(a,1,2)),rewrite(26(4)),flip(a)]. given #77 (F,wt=12): 504 D' @ (G @ F) != (A @ B) @ C # answer(A). [para(72(a,2),453(a,1))]. given #78 (F,wt=12): 505 C' @ (A @ B) != (G @ F) @ D # answer(A). [para(72(a,2),453(a,2)),flip(a)]. given #79 (T,wt=9): 268 (x @ y) * (y @ x) = e. [para(73(a,1),25(a,2)),rewrite(267(3),109(3),78(4))]. given #80 (T,wt=9): 293 (x @ y) @ (y @ x) = e. [back_rewrite(185),rewrite(267(2),267(4),97(5),3(2),11(2)),flip(a)]. given #81 (A,wt=19): 44 x' * y' * x * y * (z @ y) = x * z @ y. [para(9(a,2),6(a,1))]. given #82 (F,wt=13): 172 D @ (G @ F') != C' @ (A @ B) # answer(A). [para(72(a,2),99(a,2,2)),rewrite(131(11)),flip(a)]. given #83 (F,wt=13): 173 (F @ G) @ D' != C' @ (A @ B) # answer(A). [para(72(a,2),99(a,2)),rewrite(131(12)),flip(a)]. given #84 (T,wt=9): 518 x * y @ y * x = e. [para(208(a,1),32(a,2)),rewrite(1(3),325(3))]. given #85 (T,wt=9): 550 x @ x * y = x @ y. [back_rewrite(337),rewrite(533(4))]. given #86 (A,wt=21): 45 x' * y' * x * y * z @ u = (x @ y) * z @ u. [para(9(a,1),6(a,2,1)),rewrite(6(8))]. given #87 (F,wt=13): 199 (G @ F') @ D' != (A @ B) @ C # answer(A). [para(72(a,2),123(a,1)),rewrite(131(7))]. given #88 (F,wt=13): 306 (G @ F') @ D' != C @ (B @ A) # answer(A). [para(72(a,2),305(a,1,1)),rewrite(131(4))]. given #89 (T,wt=10): 78 x * y @ y' = y @ x. [para(54(a,1),10(a,1,2,2,2)),rewrite(62(4),29(4),69(4)),flip(a)]. given #90 (T,wt=10): 146 x' @ x * y = y @ x. [para(32(a,1),72(a,2))]. given #91 (A,wt=16): 47 x' * y * x * z = y * (y @ x) * z. [para(9(a,1),8(a,1,2)),rewrite(26(5)),flip(a)]. given #92 (F,wt=13): 308 (F @ G) @ D' != C @ (A' @ B) # answer(A). [para(72(a,2),305(a,2,2))]. given #93 (F,wt=13): 310 (F @ G) @ D' != (B @ A) @ C' # answer(A). [para(80(a,2),305(a,2))]. given #94 (T,wt=10): 180 x' @ y * x = y @ x. [para(33(a,1),72(a,2))]. given #95 (T,wt=10): 212 (x @ y) @ y' * x = e. [para(17(a,1),191(a,1,1))]. given #96 (A,wt=17): 49 x' * y * x * z = (x @ y') * y * z. [para(8(a,1),9(a,1,2,2,2)),rewrite(26(5))]. given #97 (F,wt=13): 351 D @ (G @ F') != C @ (A' @ B) # answer(A). [para(72(a,2),346(a,2,2))]. given #98 (F,wt=13): 352 D @ (G @ F') != (B @ A) @ C' # answer(A). [para(80(a,2),346(a,2))]. given #99 (T,wt=10): 280 (x @ y) @ (x' @ y) = e. [back_rewrite(153),rewrite(267(2),267(5),62(4),6(4),3(2),11(2)),flip(a)]. given #100 (T,wt=10): 281 (x' @ y) @ (x @ y) = e. [back_rewrite(150),rewrite(267(3),62(2),267(3),6(4),54(2),11(2)),flip(a)]. given #101 (A,wt=16): 51 (x' @ y) * x * z = x * (y @ x) * z. [para(9(a,1),9(a,1,2)),rewrite(26(5)),flip(a)]. given #102 (F,wt=13): 376 (F' @ G) @ D != C @ (A' @ B) # answer(A). [para(72(a,2),347(a,2,2))]. given #103 (F,wt=13): 377 (F' @ G) @ D != (B @ A') @ C # answer(A). [para(72(a,2),347(a,2)),rewrite(267(10),131(10))]. given #104 (T,wt=10): 359 (x @ y) @ (y' @ x) = e. [para(205(a,1),32(a,2)),rewrite(43(3),354(5))]. given #105 (T,wt=10): 366 (x @ y) * (x @ y') = e. [back_rewrite(361),rewrite(365(6))]. given #106 (A,wt=14): 56 x' * y * x * y' = x @ y'. [para(26(a,1),5(a,1,2))]. given #107 (F,wt=13): 378 (F' @ G) @ D != (B @ A) @ C' # answer(A). [para(80(a,2),347(a,2))]. given #108 (F,wt=13): 450 D' @ (G @ F) != C @ (A' @ B) # answer(A). [para(72(a,2),372(a,2,2))]. given #109 (T,wt=10): 370 (x @ y) @ x * y' = e. [para(31(a,1),191(a,1,1))]. given #110 (T,wt=10): 383 (x' @ y) @ y * x = e. [para(32(a,1),211(a,1,1)),rewrite(131(4,R),267(2))]. given #111 (A,wt=14): 57 x * y' * x' * y = x' @ y. [para(26(a,1),5(a,1))]. given #112 (F,wt=13): 451 D' @ (G @ F) != (B @ A') @ C # answer(A). [para(72(a,2),372(a,2)),rewrite(267(10),131(10))]. given #113 (F,wt=13): 452 D' @ (G @ F) != (B @ A) @ C' # answer(A). [para(80(a,2),372(a,2))]. given #114 (T,wt=10): 384 (x' @ y) @ x * y = e. [para(33(a,1),211(a,1,1)),rewrite(131(4,R),267(2))]. given #115 (T,wt=10): 422 (x @ y) @ (x @ y') = e. [para(220(a,1),17(a,2)),rewrite(267(3),109(3),418(5))]. given #116 (A,wt=18): 60 x' * y * x * y' * z = (x @ y') * z. [para(26(a,1),9(a,1,2))]. given #117 (F,wt=13): 506 C' @ (B @ A') != (G @ F) @ D # answer(A). [para(72(a,2),374(a,1))]. given #118 (F,wt=13): 588 (F' @ G) @ D != C' @ (A @ B) # answer(A). [para(72(a,2),466(a,2))]. given #119 (T,wt=10): 516 (x @ y) @ x' * y = e. [para(80(a,1),208(a,1,1))]. given #120 (T,wt=10): 517 (x @ y') @ x * y = e. [para(80(a,2),208(a,1,1))]. given #121 (A,wt=18): 61 (x' @ y) * z = x * y' * x' * y * z. [para(26(a,1),9(a,1)),flip(a)]. given #122 (F,wt=13): 681 D' @ (G @ F) != C' @ (A @ B) # answer(A). [para(72(a,2),504(a,2))]. given #123 (F,wt=14): 241 D @ (G @ F') != C' @ (B @ A') # answer(A). [para(72(a,2),132(a,2,2)),rewrite(131(12)),flip(a)]. given #124 (T,wt=10): 539 (x @ y) @ y * x' = e. [para(80(a,1),210(a,1,1))]. given #125 (T,wt=10): 540 (x @ y') @ y * x = e. [para(80(a,2),210(a,1,1))]. given #126 (A,wt=18): 67 x' * y * z * x = y * z * (y * z @ x). [para(10(a,1),8(a,1,2)),rewrite(62(3),1(4)),flip(a)]. given #127 (F,wt=14): 242 (F @ G) @ D' != C' @ (B @ A') # answer(A). [para(72(a,2),132(a,2)),rewrite(131(13)),flip(a)]. given #128 (F,wt=14): 243 (G @ F') @ D' != (B @ A') @ C # answer(A). [para(72(a,2),133(a,1)),rewrite(131(7))]. given #129 (T,wt=10): 577 x @ y' * x * y = e. [para(38(a,2),177(a,1,2)),rewrite(220(7))]. given #130 (T,wt=10): 590 (x * y)' = y' * x'. [para(8(a,1),237(a,1,1,1)),flip(a)]. given #131 (A,wt=14): 76 x' * y' * x = (x @ y) * y'. [para(54(a,1),9(a,1,2,2,2)),rewrite(29(4))]. given #132 (F,wt=14): 722 (G @ F') @ D' != C' @ (A @ B) # answer(A). [para(80(a,2),172(a,1))]. given #133 (F,wt=14): 825 (G @ F') @ D' != C @ (A' @ B) # answer(A). [para(80(a,2),199(a,2)),rewrite(267(12))]. given #134 (T,wt=10): 685 (x @ y') * (x @ y) = e. [para(72(a,1),268(a,1,2))]. given #135 (T,wt=10): 690 (x' @ y) @ (y @ x) = e. [para(293(a,1),72(a,2)),rewrite(267(2))]. given #136 (A,wt=11): 79 x * y @ x' = y @ x'. [para(73(a,1),6(a,1,1)),rewrite(2(4)),flip(a)]. given #137 (F,wt=14): 826 (G @ F') @ D' != (B @ A) @ C' # answer(A). [para(80(a,2),306(a,2))]. given #138 (F,wt=14): 1100 (F' @ G) @ D != C' @ (B @ A') # answer(A). [para(72(a,2),377(a,2))]. given #139 (T,wt=10): 691 (x @ y') @ (x @ y) = e. [para(72(a,1),293(a,1,2))]. given #140 (T,wt=10): 726 (x @ y) @ (y @ x') = e. [para(5(a,1),518(a,1,1)),rewrite(1(6),1(5),56(6))]. given #141 (A,wt=18): 82 x' * y' * x * z = (x @ y) * y' * z. [para(58(a,1),9(a,1,2,2,2))]. ============================== PROOF ================================= % Proof 1 at 0.20 (+ 0.00) seconds: A. % Length of proof is 63. % Level of proof is 17. % Maximum clause weight is 25. % Given clauses 141. 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 * z @ y. [assumption]. 7 (A @ B) @ C != D @ (F @ G) # answer(A). [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)]. 12 x' @ x = e. [para(3(a,1),5(a,1,2,2)),rewrite(8(6)),flip(a)]. 14 (x * y @ z) * u = (x @ z) * (y @ z) * u. [para(6(a,1),1(a,1,1))]. 16 (x @ y) * e = x * e @ y. [para(11(a,1),6(a,1,2))]. 17 x' * y @ x = y @ x. [para(12(a,1),6(a,1,1)),rewrite(2(3)),flip(a)]. 18 x * y' @ y = x * e @ y. [para(12(a,1),6(a,1,2)),rewrite(16(3)),flip(a)]. 19 (x * y)' * x * y * z = z. [para(1(a,1),8(a,1,2))]. 21 x'' * e = x. [para(3(a,1),8(a,1,2))]. 23 x @ x = e. [para(8(a,1),5(a,1,2)),rewrite(3(2)),flip(a)]. 24 x'' * (x @ y) = y' * x * y. [para(5(a,1),8(a,1,2))]. 25 (x @ y)' * (x * z @ y) = z @ y. [para(6(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(24),rewrite(26(4)),flip(a)]. 29 x * e = x. [back_rewrite(21),rewrite(26(4))]. 31 x * y' @ y = x @ y. [back_rewrite(18),rewrite(29(5))]. 32 x * y @ x = y @ x. [para(23(a,1),6(a,1,1)),rewrite(2(3)),flip(a)]. 54 x * x' = e. [para(26(a,1),3(a,1))]. 58 x * x' * y = y. [para(26(a,1),8(a,1))]. 62 x'' = x. [para(26(a,1),29(a,1)),rewrite(29(2)),flip(a)]. 64 (x * y')' * y' * x = x @ y. [para(3(a,1),10(a,1,2,2,2)),rewrite(29(6),31(9))]. 67 x' * y * z * x = y * z * (y * z @ x). [para(10(a,1),8(a,1,2)),rewrite(62(3),1(4)),flip(a)]. 69 (x * y)' * y * x = y @ x. [para(8(a,1),10(a,1,2)),rewrite(32(6))]. 72 x' @ y = y @ x. [back_rewrite(64),rewrite(69(6))]. 73 x @ x' = e. [para(62(a,1),12(a,1,1))]. 78 x * y @ y' = y @ x. [para(54(a,1),10(a,1,2,2,2)),rewrite(62(4),29(4),69(4)),flip(a)]. 80 x @ y' = y @ x. [para(73(a,1),6(a,1,2)),rewrite(29(4),78(5))]. 82 x' * y' * x * z = (x @ y) * y' * z. [para(58(a,1),9(a,1,2,2,2))]. 98 (B' @ A) @ C != D @ (F @ G) # answer(A). [para(72(a,2),7(a,1,1))]. 109 x' @ y' = x @ y. [para(72(a,2),72(a,1))]. 131 x' @ y = x @ y'. [para(80(a,1),72(a,1)),flip(a)]. 134 (F @ G) @ D' != (B @ A') @ C # answer(A). [para(80(a,2),98(a,2)),rewrite(131(4)),flip(a)]. 139 x * y * z @ y = x * z @ y. [para(32(a,1),6(a,1,2)),rewrite(6(3)),flip(a)]. 191 (x @ y) @ x = e. [para(5(a,1),17(a,1,1)),rewrite(139(6),3(4),11(4))]. 202 x' @ (x @ y) = e. [para(191(a,1),72(a,2))]. 237 (x * y)' * x = y'. [para(54(a,1),19(a,1,2,2)),rewrite(29(4))]. 250 x @ (x @ y) = e. [para(109(a,1),202(a,1,2)),rewrite(62(2))]. 267 (x @ y)' = x' @ y. [para(54(a,1),25(a,1,2,1)),rewrite(11(4),29(4))]. 305 (F @ G) @ D' != C @ (B @ A) # answer(A). [para(80(a,2),134(a,2)),rewrite(267(12),109(12))]. 307 D @ (F @ G) != C @ (B @ A) # answer(A). [para(72(a,2),305(a,1)),rewrite(62(3))]. 313 x * y @ (y @ z) = x @ (y @ z). [para(250(a,1),6(a,1,2)),rewrite(29(4)),flip(a)]. 331 (x * y)' * (y' @ z) * x * z' * y * z = x @ (y @ z). [para(27(a,2),10(a,1,2,2,2)),rewrite(267(4),313(13))]. 346 D @ (G @ F') != C @ (B @ A) # answer(A). [para(72(a,2),307(a,1,2)),rewrite(131(5))]. 350 (G @ F) @ D != C @ (B @ A) # answer(A). [para(72(a,2),346(a,1)),rewrite(267(5),109(5))]. 372 D' @ (G @ F) != C @ (B @ A) # answer(A). [para(72(a,2),350(a,1))]. 451 D' @ (G @ F) != (B @ A') @ C # answer(A). [para(72(a,2),372(a,2)),rewrite(267(10),131(10))]. 590 (x * y)' = y' * x'. [para(8(a,1),237(a,1,1,1)),flip(a)]. 630 x' * y' * (x' @ z) * y * z' * x * z = y @ (x @ z). [back_rewrite(331),rewrite(590(2),1(11))]. 1183 D' @ (G @ F) != C' @ (B @ A') # answer(A). [para(72(a,2),451(a,2))]. 1432 (x' @ y) * (z' @ y) * y' * z * x * y = z * x. [para(67(a,2),67(a,1,2)),rewrite(267(3),590(2),14(9),250(14),29(12))]. 1576 (x' @ y) * y' * x * z = x * y' * z. [para(8(a,1),82(a,1,2,2)),rewrite(62(2)),flip(a)]. 1636 (x' @ y) * z * y' * x * y = z * x. [back_rewrite(1432),rewrite(1576(9))]. 1638 x @ (y @ z) = e. [back_rewrite(630),rewrite(1636(9),8(4),3(2)),flip(a)]. 1665 $F # answer(A). [back_rewrite(1183),rewrite(1638(6),1638(8)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=141. Generated=9271. Kept=1663. proofs=1. Usable=115. Sos=991. Demods=687. Limbo=27, Disabled=536. Hints=0. Weight_deleted=1128. Literals_deleted=0. Forward_subsumed=6479. Back_subsumed=113. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1106 (2 lex), Back_demodulated=417. Back_unit_deleted=0. Demod_attempts=129460. Demod_rewrites=23070. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=1.27. User_CPU=0.20, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11352 exit (max_proofs) Sat Aug 12 20:59:51 2006