============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13124 was started by mccune on cleo.thornwood, Mon Jun 19 16:41:34 2006 The command was "/home/mccune/bin/prover9 -f gt.in EA.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). clauses(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 EA.in clauses(sos). x * y * z * y * x = y * x * z * x * y. end_of_list. clauses(sos). (A @ B) @ C != D @ (F @ G) # answer(A). end_of_list. ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 (x * y) * z = x * y * z. [input]. 2 e * x = x. [input]. 3 x ' * x = e. [input]. 4 x @ y = x ' * y ' * x * y. [input]. 5 x * y * z * y * x = y * x * z * x * y. [input]. 6 (A @ B) @ C != D @ (F @ G) # answer(A). [input]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). 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: clauses(usable). end_of_list. clauses(sos). 7 (x * y) * z = x * y * z. [input]. 8 e * x = x. [input]. 9 x ' * x = e. [input]. 10 x ' * y ' * x * y = x @ y. [copy(4),flip(a)]. 11 x * y * z * y * x = y * x * z * x * y. [input]. 12 (A @ B) @ C != D @ (F @ G) # answer(A). [input]. end_of_list. clauses(demodulators). 7 (x * y) * z = x * y * z. [input]. 8 e * x = x. [input]. 9 x ' * x = e. [input]. 10 x ' * y ' * x * y = x @ y. [copy(4),flip(a)]. end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=11): 7 (x * y) * z = x * y * z. [input]. given #2 (I,wt=5): 8 e * x = x. [input]. given #3 (I,wt=6): 9 x ' * x = e. [input]. given #4 (I,wt=13): 10 x ' * y ' * x * y = x @ y. [copy(4),flip(a)]. given #5 (I,wt=19): 11 x * y * z * y * x = y * x * z * x * y. [input]. given #6 (I,wt=11): 12 (A @ B) @ C != D @ (F @ G) # answer(A). [input]. given #7 (F,wt=5): 16 e @ x = e. [para(8(a,1),10(a,1,2,2)),demod(9(4),9(4)),flip(a)]. given #8 (F,wt=6): 17 x ' @ x = e. [para(9(a,1),10(a,1,2,2)),demod(13(6)),flip(a)]. given #9 (T,wt=8): 13 x ' * x * y = y. [para(9(a,1),7(a,1,1)),demod(8(2)),flip(a)]. given #10 (T,wt=5): 31 x @ x = e. [para(13(a,1),10(a,1,2)),demod(9(2)),flip(a)]. given #11 (A,wt=17): 14 x ' * y ' * x * y * z = (x @ y) * z. [para(10(a,1),7(a,1,1)),demod(7(7),7(6)),flip(a)]. given #12 (F,wt=5): 40 x * e = x. [back_demod(29),demod(37(4))]. given #13 (F,wt=4): 61 e ' = e. [para(40(a,1),9(a,1))]. given #14 (T,wt=5): 62 x @ e = e. [para(40(a,1),10(a,1,2,2)),demod(61(3),8(3),9(2)),flip(a)]. given #15 (T,wt=9): 37 x ' ' * y = x * y. [para(13(a,1),13(a,1,2))]. given #16 (A,wt=19): 15 (x * y) ' * z ' * x * y * z = x * y @ z. [para(7(a,1),10(a,1,2,2))]. given #17 (F,wt=5): 72 x ' ' = x. [para(37(a,1),40(a,1)),demod(40(2)),flip(a)]. given #18 (F,wt=6): 63 x * x ' = e. [para(37(a,1),9(a,1))]. given #19 (T,wt=6): 86 x @ x ' = e. [para(72(a,1),17(a,1,1))]. given #20 (T,wt=7): 83 x * x @ x = e. [para(15(a,1),15(a,1,2)),demod(9(2),61(2),8(4),9(4),16(5))]. given #21 (A,wt=23): 19 x * y * z * y * x * u = y * x * z * x * y * u. [para(11(a,1),7(a,1,1)),demod(7(5),7(4),7(3),7(2),7(9),7(8),7(7))]. given #22 (F,wt=8): 68 x * x ' * y = y. [para(37(a,1),13(a,1))]. given #23 (F,wt=10): 88 x * y * (x * y) ' = e. [para(63(a,1),7(a,1)),flip(a)]. given #24 (T,wt=9): 122 x * (y * x) ' = y '. [para(88(a,1),13(a,1,2)),demod(40(3)),flip(a)]. given #25 (T,wt=8): 136 (x @ y) ' = y @ x. [para(14(a,2),122(a,1,2,1)),demod(135(7),135(5),135(3),135(2),7(5),72(7),7(6),7(5),72(8),7(7),7(6),7(5),10(6),68(4)),flip(a)]. given #26 (A,wt=23): 20 x * y * z * u * z * y = x * z * y * u * y * z. [para(11(a,1),7(a,2,2)),demod(7(5))]. given #27 (F,wt=9): 145 (x @ y) * (y @ x) = e. [back_demod(124),demod(135(8),135(6),135(4),135(3),7(6),72(8),7(7),7(6),72(9),7(8),7(7),7(6),10(7),68(5))]. given #28 (F,wt=9): 151 x * y @ x = y @ x. [back_demod(79),demod(135(2),7(5),10(5)),flip(a)]. given #29 (T,wt=9): 173 (x @ y) @ (y @ x) = e. [para(136(a,1),17(a,1,1))]. given #30 (T,wt=9): 191 x @ x * y = x @ y. [para(151(a,1),136(a,1,1)),demod(136(2)),flip(a)]. given #31 (A,wt=23): 21 x * y * z * u * y * x = y * x * z * u * x * y. [para(7(a,1),11(a,1,2,2)),demod(7(8))]. given #32 (F,wt=10): 135 (x * y) ' = y ' * x '. [para(122(a,1),13(a,1,2)),flip(a)]. given #33 (F,wt=10): 164 x * y @ y ' = y @ x. [back_demod(91),demod(151(5))]. given #34 (T,wt=10): 190 x ' * y @ x = y @ x. [para(68(a,1),151(a,1,1)),flip(a)]. given #35 (T,wt=10): 199 x @ x ' * y = x @ y. [para(68(a,1),191(a,1,2)),flip(a)]. given #36 (A,wt=15): 23 x * y * y * x = y * x * x * y. [para(8(a,1),11(a,1,2,2)),demod(8(6))]. given #37 (F,wt=10): 224 x ' @ y * x = y @ x. [para(164(a,1),136(a,1,1)),demod(136(2)),flip(a)]. given #38 (F,wt=11): 158 x ' @ x * y = x ' @ y. [back_demod(39),demod(135(2),7(4),66(5)),flip(a)]. given #39 (T,wt=11): 165 x * y * (y @ x) = y * x. [back_demod(85),demod(151(2))]. given #40 (T,wt=11): 166 x * y ' @ y = y ' @ x. [back_demod(84),demod(151(6))]. given #41 (A,wt=21): 33 x * y * x ' * z * y = y * z * x * y * x '. [para(13(a,1),11(a,1,2,2,2)),demod(7(5),7(10),7(12),13(13))]. given #42 (F,wt=11): 174 (x @ y) * (y @ x) * z = z. [para(136(a,1),13(a,1,1))]. given #43 (F,wt=11): 186 x * y @ x ' = y @ x '. [para(13(a,1),151(a,1,1)),flip(a)]. given #44 (T,wt=11): 219 x ' * y ' @ y * x = e. [para(135(a,1),17(a,1,1))]. given #45 (T,wt=11): 220 x * y @ y ' * x ' = e. [para(135(a,1),86(a,1,2))]. given #46 (A,wt=16): 34 x * y * x ' * y * x = y * x * y. [para(13(a,1),11(a,1,2,2)),flip(a)]. given #47 (F,wt=11): 245 (x @ y) * y * x = x * y. [para(23(a,1),14(a,1,2,2)),demod(13(6),13(4)),flip(a)]. given #48 (F,wt=9): 362 (x @ y) @ y * x = e. [para(245(a,1),10(a,1,2,2)),demod(136(2),135(3),7(6),10(6),145(3)),flip(a)]. given #49 (T,wt=7): 402 (x @ y) @ x = e. [para(68(a,1),362(a,1,2)),demod(190(3))]. given #50 (T,wt=7): 420 x @ (x @ y) = e. [para(402(a,1),136(a,1,1)),demod(61(2)),flip(a)]. given #51 (A,wt=18): 35 x ' * y * x * y * x ' = y * x ' * y. [para(13(a,1),11(a,1,2)),flip(a)]. given #52 (F,wt=8): 422 (x @ y) @ y ' = e. [para(224(a,1),402(a,1,1))]. given #53 (F,wt=8): 437 (x @ y) @ x ' = e. [para(420(a,1),164(a,2)),demod(423(2),186(4))]. given #54 (T,wt=7): 481 (x @ y) @ y = e. [para(224(a,1),437(a,1,1)),demod(72(3))]. given #55 (T,wt=7): 489 x @ (y @ x) = e. [para(481(a,1),136(a,1,1)),demod(61(2)),flip(a)]. given #56 (A,wt=20): 36 x ' * y * x * z * x * y = y * z * y * x. [para(11(a,1),13(a,1,2))]. given #57 (F,wt=8): 439 x ' @ (y @ x) = e. [para(224(a,1),420(a,1,2))]. given #58 (F,wt=8): 440 (x ' @ y) @ x = e. [para(420(a,1),166(a,2)),demod(423(4),190(5))]. given #59 (T,wt=8): 469 (x @ y ') @ y = e. [para(72(a,1),422(a,1,2))]. given #60 (T,wt=8): 476 x ' @ (x @ y) = e. [para(437(a,1),136(a,1,1)),demod(61(2)),flip(a)]. given #61 (A,wt=12): 38 x ' * y * x = y * (y @ x). [back_demod(32),demod(37(4)),flip(a)]. given #62 (F,wt=8): 484 x @ y ' = y @ x. [back_demod(364),demod(476(3),8(4))]. given #63 (F,wt=11): 582 D @ (F @ G) != C @ (B @ A) # answer(A). [para(484(a,2),12(a,1)),demod(136(5)),flip(a)]. given #64 (T,wt=8): 497 x @ (x ' @ y) = e. [para(166(a,1),489(a,1,2))]. given #65 (T,wt=8): 522 x @ (y @ x ') = e. [para(72(a,1),439(a,1,1))]. given #66 (A,wt=21): 44 x * y ' * z ' * y * z * u = x * (y @ z) * u. [para(14(a,1),7(a,2,2)),demod(7(7))]. given #67 (F,wt=12): 606 (F @ G) @ D ' != C @ (B @ A) # answer(A). [back_demod(584),demod(587(11))]. given #68 (F,wt=12): 607 D @ (G @ F ') != C @ (B @ A) # answer(A). [back_demod(583),demod(587(11))]. given #69 (T,wt=8): 579 x ' @ y = y @ x. [para(440(a,1),38(a,2,2)),demod(53(4),13(4),40(5)),flip(a)]. given #70 (T,wt=9): 374 (x @ y) @ x * y = e. [para(245(a,1),191(a,1,2)),demod(362(6))]. given #71 (A,wt=22): 51 x ' * y * x * (y @ z) = (x @ y ') * z ' * y * z. [para(10(a,1),14(a,1,2,2,2)),demod(37(6))]. given #72 (F,wt=12): 608 C @ (A ' @ B) != D @ (F @ G) # answer(A). [back_demod(581),demod(587(6))]. given #73 (F,wt=12): 619 (B @ A) @ C ' != D @ (F @ G) # answer(A). [para(484(a,2),582(a,2)),flip(a)]. given #74 (T,wt=9): 405 x * y @ y * x = e. [para(362(a,1),151(a,2)),demod(7(3),165(3))]. given #75 (T,wt=9): 430 x @ y * x = x @ y. [back_demod(167),demod(423(3),13(4)),flip(a)]. given #76 (A,wt=12): 53 (x ' @ y) * x = x * (y @ x). [para(10(a,1),14(a,1,2)),demod(37(4)),flip(a)]. given #77 (F,wt=13): 658 D ' @ (F ' @ G) != C @ (B @ A) # answer(A). [para(484(a,2),606(a,1,1)),demod(587(7))]. given #78 (F,wt=13): 659 (F @ G) @ D ' != C @ (A ' @ B) # answer(A). [para(484(a,2),606(a,2,2)),demod(598(11,R))]. given #79 (T,wt=9): 590 x ' @ y ' = x @ y. [para(484(a,2),151(a,1)),demod(135(2),258(4))]. given #80 (T,wt=9): 596 x * y @ y = x @ y. [para(484(a,2),224(a,1)),demod(72(3))]. given #81 (A,wt=15): 54 (x @ y) * z * y * x = z * x * y. [para(11(a,1),14(a,1,2,2)),demod(13(7),13(5)),flip(a)]. given #82 (F,wt=13): 660 (F @ G) @ D ' != (B @ A) @ C ' # answer(A). [para(484(a,2),606(a,2))]. given #83 (F,wt=13): 661 D @ (G @ F ') != C @ (A ' @ B) # answer(A). [para(484(a,2),607(a,2,2)),demod(598(11,R))]. given #84 (T,wt=9): 598 x ' @ y = x @ y '. [para(484(a,2),166(a,1)),demod(135(3),72(2),191(3)),flip(a)]. given #85 (T,wt=10): 415 x ' * y * x @ y = e. [back_demod(228),demod(402(6))]. given #86 (A,wt=13): 55 x ' * y = (y @ x) * y * x '. [para(11(a,1),14(a,1,2)),demod(13(6),13(5))]. given #87 (F,wt=13): 662 D @ (G @ F ') != (B @ A) @ C ' # answer(A). [para(484(a,2),607(a,2))]. given #88 (F,wt=13): 728 (A ' @ B) @ C ' != D @ (F @ G) # answer(A). [para(484(a,2),608(a,1))]. given #89 (T,wt=10): 421 (x @ y) @ y ' * x = e. [para(190(a,1),402(a,1,1))]. given #90 (T,wt=10): 424 (x @ y ') @ y * x = e. [para(186(a,1),402(a,1,1))]. given #91 (A,wt=16): 56 x ' * y * x * z = y * (y @ x) * z. [para(14(a,1),13(a,1,2)),demod(37(5)),flip(a)]. given #92 (F,wt=14): 811 D ' @ (F ' @ G) != C @ (A ' @ B) # answer(A). [para(484(a,2),658(a,2,2)),demod(598(12,R))]. given #93 (F,wt=14): 812 D ' @ (F ' @ G) != (B @ A) @ C ' # answer(A). [para(484(a,2),658(a,2))]. given #94 (T,wt=10): 425 x @ y ' * x * y = e. [back_demod(233),demod(420(6))]. given #95 (T,wt=10): 441 x * y @ (y @ x ') = e. [para(186(a,1),420(a,1,2))]. given #96 (A,wt=17): 58 x ' * y * x * z = (x @ y ') * y * z. [para(13(a,1),14(a,1,2,2,2)),demod(37(5))]. given #97 (F,wt=14): 813 (F @ G) @ D ' != (A ' @ B) @ C ' # answer(A). [para(484(a,2),659(a,2))]. given #98 (F,wt=14): 926 D @ (G @ F ') != (A ' @ B) @ C ' # answer(A). [para(484(a,2),661(a,2))]. given #99 (T,wt=10): 474 (x @ y) * (x @ y ') = e. [para(437(a,1),10(a,2)),demod(136(2),72(3),393(5))]. given #100 (T,wt=10): 480 (x @ y) @ x ' * y = e. [para(190(a,1),437(a,1,1)),demod(135(4),72(4))]. given #101 (A,wt=16): 60 (x ' @ y) * x * z = x * (y @ x) * z. [para(14(a,1),14(a,1,2)),demod(37(5)),flip(a)]. given #102 (F,wt=15): 1178 D ' @ (F ' @ G) != (A ' @ B) @ C ' # answer(A). [para(484(a,2),811(a,2))]. given #103 (F,wt=10): 490 (x ' @ y) @ x * y = e. [para(158(a,1),481(a,1,1))]. given #104 (T,wt=10): 496 x * y @ (x ' @ y) = e. [para(158(a,1),489(a,1,2))]. given #105 (T,wt=10): 526 (x @ y ') * (x @ y) = e. [para(440(a,1),10(a,2)),demod(136(3),53(6),13(6))]. given #106 (A,wt=14): 65 x ' * y * x * y ' = x @ y '. [para(37(a,1),10(a,1,2))]. given #107 (F,wt=10): 588 (x @ y) * (x ' @ y) = e. [para(484(a,1),145(a,1,1))]. given #108 (F,wt=10): 589 (x ' @ y) * (x @ y) = e. [para(484(a,1),145(a,1,2))]. given #109 (T,wt=10): 591 (x @ y) @ (x ' @ y) = e. [para(484(a,1),173(a,1,1))]. given #110 (T,wt=10): 592 (x @ y) @ (y @ x ') = e. [para(484(a,1),173(a,1,2)),demod(587(4))]. given #111 (A,wt=14): 66 x * y ' * x ' * y = x ' @ y. [para(37(a,1),10(a,1))]. given #112 (F,wt=10): 593 (x @ y) @ (y ' @ x) = e. [para(484(a,2),173(a,1,1)),demod(587(4))]. given #113 (F,wt=10): 594 (x @ y) @ (x @ y ') = e. [para(484(a,2),173(a,1,2))]. given #114 (T,wt=10): 605 (x @ y ') @ x * y = e. [para(484(a,2),362(a,1,1))]. given #115 (T,wt=10): 668 (x @ y) @ x * y ' = e. [para(579(a,1),362(a,1,1))]. given #116 (A,wt=18): 70 x ' * y * x * y ' * z = (x @ y ') * z. [para(37(a,1),14(a,1,2))]. given #117 (F,wt=10): 692 (x @ y) @ y * x ' = e. [para(484(a,1),374(a,1,1))]. given #118 (F,wt=10): 695 (x ' @ y) @ y * x = e. [para(579(a,2),374(a,1,1))]. given #119 (T,wt=10): 733 x @ y * x * y ' = e. [para(13(a,1),405(a,1,1)),demod(7(3))]. given #120 (T,wt=10): 734 x * y * x ' @ y = e. [para(13(a,1),405(a,1,2)),demod(7(3))]. given #121 (A,wt=18): 71 (x ' @ y) * z = x * y ' * x ' * y * z. [para(37(a,1),14(a,1)),flip(a)]. given #122 (F,wt=10): 1207 x * y @ (x @ y ') = e. [para(441(a,1),190(a,2)),demod(136(3),667(4))]. given #123 (F,wt=10): 1220 x * y @ (y ' @ x) = e. [para(598(a,2),441(a,1,2))]. given #124 (T,wt=11): 258 x @ y * x ' = y @ x '. [para(72(a,1),224(a,1,1))]. given #125 (T,wt=11): 326 x * y ' @ y * x ' = e. [para(72(a,1),219(a,1,1,1))]. given #126 (A,wt=18): 77 x ' * y * z * x = y * z * (y * z @ x). [para(15(a,1),11(a,1,2,2)),demod(7(7),7(6),68(5),7(13),7(12),63(11),40(11),9(11),40(9)),flip(a)]. given #127 (F,wt=11): 327 x ' * y @ y ' * x = e. [para(72(a,1),219(a,1,1,2))]. given #128 (F,wt=11): 381 x ' * y ' @ x * y = e. [para(245(a,1),224(a,1,2)),demod(135(2),362(8))]. given #129 (T,wt=11): 416 x * y @ x ' * y ' = e. [back_demod(378),demod(403(3)),flip(a)]. given #130 (T,wt=11): 423 (x @ y) * x = x * (x @ y). [para(402(a,1),165(a,1,2,2)),demod(40(3)),flip(a)]. given #131 (A,wt=21): 82 x ' * y ' * x * y * z @ u = (x @ y) * z @ u. [para(14(a,2),15(a,2,1)),demod(15(9)),flip(a)]. given #132 (F,wt=9): 2109 (x @ (y @ z)) * y = y. [para(423(a,1),14(a,1,2,2,2)),demod(136(3),900(6),13(3)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.33 (+ 0.00) seconds: A. % Length of proof is 69. % Level of proof is 19. % Maximum clause weight is 20. % Given clauses 132. 4 x @ y = x ' * y ' * x * y. [input]. 7 (x * y) * z = x * y * z. [input]. 8 e * x = x. [input]. 9 x ' * x = e. [input]. 10 x ' * y ' * x * y = x @ y. [copy(4),flip(a)]. 11 x * y * z * y * x = y * x * z * x * y. [input]. 12 (A @ B) @ C != D @ (F @ G) # answer(A). [input]. 13 x ' * x * y = y. [para(9(a,1),7(a,1,1)),demod(8(2)),flip(a)]. 14 x ' * y ' * x * y * z = (x @ y) * z. [para(10(a,1),7(a,1,1)),demod(7(7),7(6)),flip(a)]. 15 (x * y) ' * z ' * x * y * z = x * y @ z. [para(7(a,1),10(a,1,2,2))]. 17 x ' @ x = e. [para(9(a,1),10(a,1,2,2)),demod(13(6)),flip(a)]. 23 x * y * y * x = y * x * x * y. [para(8(a,1),11(a,1,2,2)),demod(8(6))]. 25 x * y * (x * y) ' * y * x = y * x * e. [para(9(a,1),11(a,1,2,2)),flip(a)]. 29 x ' ' * e = x. [para(9(a,1),13(a,1,2))]. 32 x ' ' * (x @ y) = y ' * x * y. [para(10(a,1),13(a,1,2))]. 37 x ' ' * y = x * y. [para(13(a,1),13(a,1,2))]. 38 x ' * y * x = y * (y @ x). [back_demod(32),demod(37(4)),flip(a)]. 40 x * e = x. [back_demod(29),demod(37(4))]. 42 x * y * (x * y) ' * y * x = y * x. [back_demod(25),demod(40(8))]. 54 (x @ y) * z * y * x = z * x * y. [para(11(a,1),14(a,1,2,2)),demod(13(7),13(5)),flip(a)]. 61 e ' = e. [para(40(a,1),9(a,1))]. 62 x @ e = e. [para(40(a,1),10(a,1,2,2)),demod(61(3),8(3),9(2)),flip(a)]. 63 x * x ' = e. [para(37(a,1),9(a,1))]. 65 x ' * y * x * y ' = x @ y '. [para(37(a,1),10(a,1,2))]. 68 x * x ' * y = y. [para(37(a,1),13(a,1))]. 72 x ' ' = x. [para(37(a,1),40(a,1)),demod(40(2)),flip(a)]. 74 (x * y ') ' * y ' * x = x * y ' @ y. [para(9(a,1),15(a,1,2,2,2)),demod(40(6))]. 79 (x * y) ' * y * x = x * y @ x. [para(13(a,1),15(a,1,2))]. 84 x * y ' @ y = x * y ' @ x. [back_demod(74),demod(79(6)),flip(a)]. 85 x * y * (x * y @ x) = y * x. [back_demod(42),demod(79(4))]. 86 x @ x ' = e. [para(72(a,1),17(a,1,1))]. 88 x * y * (x * y) ' = e. [para(63(a,1),7(a,1)),flip(a)]. 91 x * y @ y ' = x * y @ x. [para(63(a,1),15(a,1,2,2,2)),demod(72(4),40(4),79(4)),flip(a)]. 122 x * (y * x) ' = y '. [para(88(a,1),13(a,1,2)),demod(40(3)),flip(a)]. 124 (x @ y) * z * (x ' * y ' * x * y * z) ' = e. [para(14(a,2),88(a,1,2,2,1))]. 135 (x * y) ' = y ' * x '. [para(122(a,1),13(a,1,2)),flip(a)]. 136 (x @ y) ' = y @ x. [para(14(a,2),122(a,1,2,1)),demod(135(7),135(5),135(3),135(2),7(5),72(7),7(6),7(5),72(8),7(7),7(6),7(5),10(6),68(4)),flip(a)]. 145 (x @ y) * (y @ x) = e. [back_demod(124),demod(135(8),135(6),135(4),135(3),7(6),72(8),7(7),7(6),72(9),7(8),7(7),7(6),10(7),68(5))]. 151 x * y @ x = y @ x. [back_demod(79),demod(135(2),7(5),10(5)),flip(a)]. 164 x * y @ y ' = y @ x. [back_demod(91),demod(151(5))]. 165 x * y * (y @ x) = y * x. [back_demod(85),demod(151(2))]. 166 x * y ' @ y = y ' @ x. [back_demod(84),demod(151(6))]. 186 x * y @ x ' = y @ x '. [para(13(a,1),151(a,1,1)),flip(a)]. 190 x ' * y @ x = y @ x. [para(68(a,1),151(a,1,1)),flip(a)]. 191 x @ x * y = x @ y. [para(151(a,1),136(a,1,1)),demod(136(2)),flip(a)]. 194 x ' @ y ' * x * y = x ' @ (x @ y). [para(10(a,1),191(a,1,2)),flip(a)]. 224 x ' @ y * x = y @ x. [para(164(a,1),136(a,1,1)),demod(136(2)),flip(a)]. 245 (x @ y) * y * x = x * y. [para(23(a,1),14(a,1,2,2)),demod(13(6),13(4)),flip(a)]. 362 (x @ y) @ y * x = e. [para(245(a,1),10(a,1,2,2)),demod(136(2),135(3),7(6),10(6),145(3)),flip(a)]. 364 (x ' @ (x @ y)) * (y @ x ') = x @ y. [para(10(a,1),245(a,2)),demod(194(5),7(8),7(7),65(8))]. 402 (x @ y) @ x = e. [para(68(a,1),362(a,1,2)),demod(190(3))]. 420 x @ (x @ y) = e. [para(402(a,1),136(a,1,1)),demod(61(2)),flip(a)]. 423 (x @ y) * x = x * (x @ y). [para(402(a,1),165(a,1,2,2)),demod(40(3)),flip(a)]. 437 (x @ y) @ x ' = e. [para(420(a,1),164(a,2)),demod(423(2),186(4))]. 476 x ' @ (x @ y) = e. [para(437(a,1),136(a,1,1)),demod(61(2)),flip(a)]. 484 x @ y ' = y @ x. [back_demod(364),demod(476(3),8(4))]. 584 (F @ G) @ D ' != (A @ B) @ C # answer(A). [para(484(a,2),12(a,2)),flip(a)]. 587 (x @ y) @ z = z @ (y @ x). [para(136(a,1),484(a,1,2)),flip(a)]. 598 x ' @ y = x @ y '. [para(484(a,2),166(a,1)),demod(135(3),72(2),191(3)),flip(a)]. 606 (F @ G) @ D ' != C @ (B @ A) # answer(A). [back_demod(584),demod(587(11))]. 658 D ' @ (F ' @ G) != C @ (B @ A) # answer(A). [para(484(a,2),606(a,1,1)),demod(587(7))]. 811 D ' @ (F ' @ G) != C @ (A ' @ B) # answer(A). [para(484(a,2),658(a,2,2)),demod(598(12,R))]. 900 (x @ y) * z * y * (y @ x) = z * y. [para(38(a,1),54(a,1,2,2)),demod(164(3),7(8),63(7),40(7))]. 1178 D ' @ (F ' @ G) != (A ' @ B) @ C ' # answer(A). [para(484(a,2),811(a,2))]. 2109 (x @ (y @ z)) * y = y. [para(423(a,1),14(a,1,2,2,2)),demod(136(3),900(6),13(3)),flip(a)]. 2242 x @ ((x @ y) @ z) = (x @ y) @ z. [para(2109(a,1),10(a,1,2,2)),demod(136(3),9(4),40(4),587(5)),flip(a)]. 2252 (x @ y) @ z = e. [para(2109(a,1),224(a,1,2)),demod(598(2),86(2),587(4),2242(4)),flip(a)]. 2261 x @ (y @ z) = e. [para(2109(a,1),38(a,1,2)),demod(9(2),587(6),2252(5),62(5),40(5)),flip(a)]. 2289 $F # answer(A). [back_demod(1178),demod(2261(7),2252(8)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=132. Generated=13787. Kept=2282. proofs=1. Usable=100. Sos=1333. Demods=822. Denials=0. Limbo=37, Disabled=818. Hints=0. Weight_deleted=2878. Literals_deleted=0. Forward_subsumed=8626. Back_subsumed=359. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1481 (2 lex), Back_demodulated=453. Back_unit_deleted=0. Demod_attempts=217121. Demod_rewrites=40517. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=1.87. User_CPU=0.33, System_CPU=0.00, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13124 exit (max_proofs) Mon Jun 19 16:41:35 2006