============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13126 was started by mccune on cleo.thornwood, Mon Jun 19 16:41:39 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). 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 ED.in clauses(sos). x * y * z * y * x = y * x * z * x * y. end_of_list. clauses(sos). (A @ C) * (B @ C) != A * B @ C # answer(D). 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 @ C) * (B @ C) != A * B @ C # answer(D). [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, *, @, ' ]). 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: 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 @ C) * (B @ C) != A * B @ C # answer(D). [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=13): 12 (A @ C) * (B @ C) != A * B @ C # answer(D). [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=19): 56 A ' * C ' * A * C * (B @ C) != A * B @ C # answer(D). [para(14(a,2),12(a,1))]. given #13 (F,wt=5): 40 x * e = x. [back_demod(29),demod(37(4))]. given #14 (T,wt=4): 62 e ' = e. [para(40(a,1),9(a,1))]. given #15 (T,wt=5): 63 x @ e = e. [para(40(a,1),10(a,1,2,2)),demod(62(3),8(3),9(2)),flip(a)]. 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=7): 74 x * x @ x = e. [para(15(a,1),15(a,1,2)),demod(9(2),62(2),8(4),9(4),16(5))]. given #18 (F,wt=9): 37 x ' ' * y = x * y. [para(13(a,1),13(a,1,2))]. given #19 (T,wt=5): 88 x ' ' = x. [para(37(a,1),40(a,1)),demod(40(2)),flip(a)]. given #20 (T,wt=6): 79 x * x ' = e. [para(37(a,1),9(a,1))]. 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=6): 90 x @ x ' = e. [para(88(a,1),17(a,1,1))]. given #23 (F,wt=8): 84 x * x ' * y = y. [para(37(a,1),13(a,1))]. given #24 (T,wt=10): 91 x * y * (x * y) ' = e. [para(79(a,1),7(a,1)),flip(a)]. given #25 (T,wt=9): 123 x * (y * x) ' = y '. [para(91(a,1),13(a,1,2)),demod(40(3)),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=8): 137 (x @ y) ' = y @ x. [para(14(a,2),123(a,1,2,1)),demod(136(7),136(5),136(3),136(2),7(5),88(7),7(6),7(5),88(8),7(7),7(6),7(5),10(6),84(4)),flip(a)]. given #28 (F,wt=9): 146 (x @ y) * (y @ x) = e. [back_demod(125),demod(136(8),136(6),136(4),136(3),7(6),88(8),7(7),7(6),88(9),7(8),7(7),7(6),10(7),84(5))]. given #29 (T,wt=9): 152 x * y @ x = y @ x. [back_demod(70),demod(136(2),7(5),10(5)),flip(a)]. given #30 (T,wt=9): 179 (x @ y) @ (y @ x) = e. [para(137(a,1),17(a,1,1))]. 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=9): 193 x @ x * y = x @ y. [para(152(a,1),137(a,1,1)),demod(137(2)),flip(a)]. given #33 (F,wt=10): 136 (x * y) ' = y ' * x '. [para(123(a,1),13(a,1,2)),flip(a)]. given #34 (T,wt=10): 165 x * y @ y ' = y @ x. [back_demod(94),demod(152(5))]. given #35 (T,wt=10): 191 x ' * y @ x = y @ x. [para(84(a,1),152(a,1,1)),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): 215 x @ x ' * y = x @ y. [para(84(a,1),193(a,1,2)),flip(a)]. given #38 (F,wt=10): 226 x ' @ y * x = y @ x. [para(165(a,1),137(a,1,1)),demod(137(2)),flip(a)]. given #39 (T,wt=11): 159 x ' @ x * y = x ' @ y. [back_demod(39),demod(136(2),7(4),82(5)),flip(a)]. given #40 (T,wt=11): 166 x * y * (y @ x) = y * x. [back_demod(76),demod(152(2))]. 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): 167 x * y ' @ y = y ' @ x. [back_demod(75),demod(152(6))]. given #43 (F,wt=11): 180 (x @ y) * (y @ x) * z = z. [para(137(a,1),13(a,1,1))]. given #44 (T,wt=11): 187 x * y @ x ' = y @ x '. [para(13(a,1),152(a,1,1)),flip(a)]. given #45 (T,wt=11): 221 x ' * y ' @ y * x = e. [para(136(a,1),17(a,1,1))]. 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): 222 x * y @ y ' * x ' = e. [para(136(a,1),90(a,1,2))]. given #48 (F,wt=11): 240 (x @ y) * y * x = x * y. [para(23(a,1),14(a,1,2,2)),demod(13(6),13(4)),flip(a)]. given #49 (T,wt=9): 364 (x @ y) @ y * x = e. [para(240(a,1),10(a,1,2,2)),demod(137(2),136(3),7(6),10(6),146(3)),flip(a)]. given #50 (T,wt=7): 404 (x @ y) @ x = e. [para(84(a,1),364(a,1,2)),demod(191(3))]. 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=7): 422 x @ (x @ y) = e. [para(404(a,1),137(a,1,1)),demod(62(2)),flip(a)]. given #53 (F,wt=8): 424 (x @ y) @ y ' = e. [para(226(a,1),404(a,1,1))]. given #54 (T,wt=8): 462 (x @ y) @ x ' = e. [para(422(a,1),165(a,2)),demod(425(2),187(4))]. given #55 (T,wt=7): 483 (x @ y) @ y = e. [para(226(a,1),462(a,1,1)),demod(88(3))]. 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=7): 491 x @ (y @ x) = e. [para(483(a,1),137(a,1,1)),demod(62(2)),flip(a)]. given #58 (F,wt=8): 464 x ' @ (y @ x) = e. [para(226(a,1),422(a,1,2))]. given #59 (T,wt=8): 465 (x ' @ y) @ x = e. [para(422(a,1),167(a,2)),demod(425(4),191(5))]. given #60 (T,wt=8): 471 (x @ y ') @ y = e. [para(88(a,1),424(a,1,2))]. 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): 478 x ' @ (x @ y) = e. [para(462(a,1),137(a,1,1)),demod(62(2)),flip(a)]. given #63 (F,wt=8): 486 x @ y ' = y @ x. [back_demod(366),demod(478(3),8(4))]. given #64 (T,wt=8): 521 x @ (x ' @ y) = e. [para(167(a,1),491(a,1,2))]. given #65 (T,wt=8): 524 x @ (y @ x ') = e. [para(88(a,1),464(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=14): 583 (C @ A ') * (B @ C) != A * B @ C # answer(D). [para(486(a,2),12(a,1,1))]. given #68 (F,wt=14): 584 (A @ C) * (C @ B ') != A * B @ C # answer(D). [para(486(a,2),12(a,1,2))]. given #69 (T,wt=8): 575 x ' @ y = y @ x. [para(465(a,1),38(a,2,2)),demod(53(4),13(4),40(5)),flip(a)]. given #70 (T,wt=9): 378 (x @ y) @ x * y = e. [para(240(a,1),193(a,1,2)),demod(364(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=14): 661 C ' @ A * B != (A @ C) * (B @ C) # answer(D). [para(575(a,2),12(a,2)),flip(a)]. given #73 (F,wt=15): 585 C @ B ' * A ' != (A @ C) * (B @ C) # answer(D). [para(486(a,2),12(a,2)),demod(136(12)),flip(a)]. given #74 (T,wt=9): 407 x * y @ y * x = e. [para(364(a,1),152(a,2)),demod(7(3),166(3))]. given #75 (T,wt=9): 432 x @ y * x = x @ y. [back_demod(168),demod(425(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=15): 658 (C @ A ') * (C @ B ') != A * B @ C # answer(D). [para(486(a,2),583(a,1,2))]. given #78 (F,wt=15): 673 C ' @ A * B != (C @ A ') * (B @ C) # answer(D). [para(575(a,2),583(a,2)),flip(a)]. given #79 (T,wt=9): 593 x ' @ y ' = x @ y. [para(486(a,2),152(a,1)),demod(136(2),260(4))]. given #80 (T,wt=9): 599 x * y @ y = x @ y. [para(486(a,2),226(a,1)),demod(88(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=15): 674 C ' @ A * B != (A @ C) * (C @ B ') # answer(D). [para(575(a,2),584(a,2)),flip(a)]. given #83 (F,wt=16): 659 C @ B ' * A ' != (C @ A ') * (B @ C) # answer(D). [para(486(a,2),583(a,2)),demod(136(13)),flip(a)]. given #84 (T,wt=9): 601 x ' @ y = x @ y '. [para(486(a,2),167(a,1)),demod(136(3),88(2),193(3)),flip(a)]. given #85 (T,wt=10): 417 x ' * y * x @ y = e. [back_demod(230),demod(404(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=16): 660 C @ B ' * A ' != (A @ C) * (C @ B ') # answer(D). [para(486(a,2),584(a,2)),demod(136(13)),flip(a)]. given #88 (F,wt=16): 730 B ' * A ' @ C ' != (A @ C) * (B @ C) # answer(D). [para(575(a,2),661(a,1)),demod(136(4))]. given #89 (T,wt=10): 423 (x @ y) @ y ' * x = e. [para(191(a,1),404(a,1,1))]. given #90 (T,wt=10): 426 (x @ y ') @ y * x = e. [para(187(a,1),404(a,1,1))]. given #91 (A,wt=16): 57 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=16): 815 C ' @ A * B != (C @ A ') * (C @ B ') # answer(D). [para(575(a,2),658(a,2)),flip(a)]. given #93 (F,wt=17): 814 C @ B ' * A ' != (C @ A ') * (C @ B ') # answer(D). [para(486(a,2),658(a,2)),demod(136(14)),flip(a)]. given #94 (T,wt=10): 427 x @ y ' * x * y = e. [back_demod(249),demod(422(6))]. given #95 (T,wt=10): 466 x * y @ (y @ x ') = e. [para(187(a,1),422(a,1,2))]. given #96 (A,wt=17): 59 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=17): 817 B ' * A ' @ C ' != (C @ A ') * (B @ C) # answer(D). [para(575(a,2),673(a,1)),demod(136(4))]. given #98 (F,wt=17): 932 B ' * A ' @ C ' != (A @ C) * (C @ B ') # answer(D). [para(575(a,2),674(a,1)),demod(136(4))]. given #99 (T,wt=10): 476 (x @ y) * (x @ y ') = e. [para(462(a,1),10(a,2)),demod(137(2),88(3),395(5))]. given #100 (T,wt=10): 482 (x @ y) @ x ' * y = e. [para(191(a,1),462(a,1,1)),demod(136(4),88(4))]. given #101 (A,wt=16): 61 (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=18): 1194 B ' * A ' @ C ' != (C @ A ') * (C @ B ') # answer(D). [para(575(a,2),815(a,1)),demod(136(4))]. given #103 (F,wt=19): 657 C ' * A * C * A ' * (B @ C) != A * B @ C # answer(D). [para(14(a,2),583(a,1)),demod(88(5))]. given #104 (T,wt=10): 492 (x ' @ y) @ x * y = e. [para(159(a,1),483(a,1,1))]. given #105 (T,wt=10): 520 x * y @ (x ' @ y) = e. [para(159(a,1),491(a,1,2))]. given #106 (A,wt=18): 68 x ' * y * z * x = y * z * (y * z @ x). [para(15(a,1),13(a,1,2)),demod(37(6),7(4)),flip(a)]. given #107 (F,wt=18): 1537 (C @ A ' * (B @ C)) * (B @ C) != A * B @ C # answer(D). [para(54(a,2),657(a,1,2)),demod(7(19),493(18),84(20),1432(16),13(17))]. given #108 (F,wt=17): 1649 ((C @ B) * A @ C) * (B @ C) != A * B @ C # answer(D). [para(575(a,2),1537(a,1,1)),demod(136(7),137(4),88(6))]. given #109 (T,wt=10): 528 (x @ y ') * (x @ y) = e. [para(465(a,1),10(a,2)),demod(137(3),53(6),13(6))]. given #110 (T,wt=10): 591 (x @ y) * (x ' @ y) = e. [para(486(a,1),146(a,1,1))]. given #111 (A,wt=21): 73 x ' * y ' * x * y * z @ u = (x @ y) * z @ u. [para(14(a,2),15(a,2,1)),demod(15(9)),flip(a)]. given #112 (F,wt=18): 1652 ((B ' @ C) * A @ C) * (B @ C) != A * B @ C # answer(D). [para(486(a,2),1649(a,1,1,1,1)),demod(601(4,R))]. given #113 (F,wt=18): 1653 ((C @ B) * A @ C) * (C @ B ') != A * B @ C # answer(D). [para(486(a,2),1649(a,1,2))]. given #114 (T,wt=10): 592 (x ' @ y) * (x @ y) = e. [para(486(a,1),146(a,1,2))]. given #115 (T,wt=10): 594 (x @ y) @ (x ' @ y) = e. [para(486(a,1),179(a,1,1))]. given #116 (A,wt=14): 81 x ' * y * x * y ' = x @ y '. [para(37(a,1),10(a,1,2))]. given #117 (F,wt=18): 1655 (C ' @ (C @ B) * A) * (B @ C) != A * B @ C # answer(D). [para(575(a,2),1649(a,1,1))]. given #118 (F,wt=18): 1656 C ' @ A * B != ((C @ B) * A @ C) * (B @ C) # answer(D). [para(575(a,2),1649(a,2)),flip(a)]. given #119 (T,wt=10): 595 (x @ y) @ (y @ x ') = e. [para(486(a,1),179(a,1,2)),demod(590(4))]. given #120 (T,wt=10): 596 (x @ y) @ (y ' @ x) = e. [para(486(a,2),179(a,1,1)),demod(590(4))]. given #121 (A,wt=14): 82 x * y ' * x ' * y = x ' @ y. [para(37(a,1),10(a,1))]. given #122 (F,wt=19): 1253 A ' * (C @ A ') * A * (B @ C) != A * B @ C # answer(D). [para(59(a,1),56(a,1,2))]. given #123 (F,wt=19): 1645 (C @ A ' * (C @ B ')) * (B @ C) != A * B @ C # answer(D). [para(486(a,2),1537(a,1,1,2,2))]. given #124 (T,wt=10): 597 (x @ y) @ (x @ y ') = e. [para(486(a,2),179(a,1,2))]. given #125 (T,wt=10): 608 (x @ y ') @ x * y = e. [para(486(a,2),364(a,1,1))]. given #126 (A,wt=18): 86 x ' * y * x * y ' * z = (x @ y ') * z. [para(37(a,1),14(a,1,2))]. given #127 (F,wt=19): 1646 (A ' * (B @ C) @ C ') * (B @ C) != A * B @ C # answer(D). [para(486(a,2),1537(a,1,1))]. given #128 (F,wt=19): 1647 (C @ A ' * (B @ C)) * (C @ B ') != A * B @ C # answer(D). [para(486(a,2),1537(a,1,2))]. given #129 (T,wt=10): 668 (x @ y) @ x * y ' = e. [para(575(a,1),364(a,1,1))]. given #130 (T,wt=10): 694 (x @ y) @ y * x ' = e. [para(486(a,1),378(a,1,1))]. given #131 (A,wt=18): 87 (x ' @ y) * z = x * y ' * x ' * y * z. [para(37(a,1),14(a,1)),flip(a)]. given #132 (F,wt=19): 1650 C ' @ A * B != (C @ A ' * (B @ C)) * (B @ C) # answer(D). [para(575(a,2),1537(a,2)),flip(a)]. given #133 (F,wt=19): 1654 C @ B ' * A ' != ((C @ B) * A @ C) * (B @ C) # answer(D). [para(486(a,2),1649(a,2)),demod(136(16)),flip(a)]. given #134 (T,wt=10): 697 (x ' @ y) @ y * x = e. [para(575(a,2),378(a,1,1))]. given #135 (T,wt=10): 735 x @ y * x * y ' = e. [para(13(a,1),407(a,1,1)),demod(7(3))]. given #136 (A,wt=14): 92 x ' * y ' * x = (x @ y) * y '. [para(79(a,1),14(a,1,2,2,2)),demod(40(4))]. given #137 (F,wt=19): 1758 ((B ' @ C) * A @ C) * (C @ B ') != A * B @ C # answer(D). [para(486(a,2),1652(a,1,2))]. given #138 (F,wt=19): 1761 C ' @ A * B != ((B ' @ C) * A @ C) * (B @ C) # answer(D). [para(575(a,2),1652(a,2)),flip(a)]. given #139 (T,wt=10): 736 x * y * x ' @ y = e. [para(13(a,1),407(a,1,2)),demod(7(3))]. given #140 (T,wt=10): 1225 x * y @ (x @ y ') = e. [para(466(a,1),191(a,2)),demod(137(3),667(4))]. given #141 (A,wt=19): 95 x * y * y * x * z = y * x * x * y * z. [para(8(a,1),19(a,1,2,2)),demod(8(8))]. given #142 (F,wt=19): 1764 (C ' @ (C @ B) * A) * (C @ B ') != A * B @ C # answer(D). [para(575(a,2),1653(a,1,1))]. given #143 (F,wt=19): 1765 C ' @ A * B != ((C @ B) * A @ C) * (C @ B ') # answer(D). [para(575(a,2),1653(a,2)),flip(a)]. given #144 (T,wt=10): 1238 x * y @ (y ' @ x) = e. [para(601(a,2),466(a,1,2))]. given #145 (T,wt=11): 260 x @ y * x ' = y @ x '. [para(88(a,1),226(a,1,1))]. given #146 (A,wt=22): 96 x ' * y * z * y = y * x ' * z * x ' * y * x. [para(9(a,1),19(a,1,2,2,2,2)),demod(40(3))]. given #147 (F,wt=19): 1801 C * A ' * C ' * A * (B @ C) != A * B @ C # answer(D). [para(14(a,2),1655(a,1)),demod(88(3),136(7),137(7),7(18),7(20),1138(19))]. given #148 (F,wt=19): 1803 (C ' @ (C @ B) * A) * (B @ C) != C ' @ A * B # answer(D). [para(575(a,2),1655(a,2))]. given #149 (T,wt=11): 328 x * y ' @ y * x ' = e. [para(88(a,1),221(a,1,1,1))]. given #150 (T,wt=11): 329 x ' * y @ y ' * x = e. [para(88(a,1),221(a,1,1,2))]. given #151 (A,wt=19): 99 x ' * y ' * z * (y @ x) = y ' * x ' * z. [para(10(a,1),19(a,1,2,2,2)),demod(13(12),9(10),40(10))]. given #152 (F,wt=14): 2536 (B @ C) * (C @ A ') != A * B @ C # answer(D). [back_demod(1852),demod(2513(7),2412(12),2412(13),7(13),8(14),13(13))]. given #153 (F,wt=15): 2537 C ' @ A * B != (B @ C) * (C @ A ') # answer(D). [back_demod(1851),demod(2412(18),7(18),13(19))]. given #154 (T,wt=7): 2513 x @ (y @ z) = e. [back_demod(178),demod(2411(5),9(2)),flip(a)]. given #155 (T,wt=7): 2607 (x @ y) @ z = e. [back_demod(1470),demod(2513(3),8(5),476(4)),flip(a)]. given #156 (A,wt=13): 100 x * y ' * (x @ y) = y ' * x. [para(10(a,1),19(a,1,2,2)),demod(9(8),40(8),9(7),40(7))]. given #157 (F,wt=16): 2538 C @ B ' * A ' != (B @ C) * (C @ A ') # answer(D). [back_demod(1850),demod(2412(19),7(19),13(20))]. given #158 (F,wt=17): 2525 B ' * A ' @ C ' != (B @ C) * (C @ A ') # answer(D). [back_demod(2067),demod(2412(15,R),1367(16),2412(16,R))]. given #159 (T,wt=11): 383 x ' * y ' @ x * y = e. [para(240(a,1),226(a,1,2)),demod(136(2),364(8))]. given #160 (T,wt=11): 418 x * y @ x ' * y ' = e. [back_demod(380),demod(406(3)),flip(a)]. given #161 (A,wt=23): 101 x * y * y * y * x * x = y * y * x * x * x * y. [para(11(a,1),19(a,1,2)),flip(a)]. given #162 (F,wt=17): 2562 (B @ C) * (A * (C @ B) @ C) != A * B @ C # answer(D). [back_demod(1649),demod(2412(5),2412(11,R))]. given #163 (F,wt=18): 2556 C ' @ A * B != (B @ C) * (A * (C @ B) @ C) # answer(D). [back_demod(1656),demod(2412(11),2412(17,R))]. given #164 (T,wt=11): 436 x @ y * (y @ x) = x @ y. [back_demod(272),demod(432(5))]. given #165 (T,wt=11): 468 x ' * y * x @ y ' = e. [back_demod(185),demod(462(8))]. given #166 (A,wt=24): 102 x ' * y * x * z * x * y * u = y * z * y * x * u. [para(19(a,1),13(a,1,2))]. given #167 (F,wt=18): 2557 (B @ C) * (C ' @ A * (C @ B)) != A * B @ C # answer(D). [back_demod(1655),demod(2412(7),2412(12,R))]. given #168 (F,wt=18): 2559 (A * (C @ B) @ C) * (C @ B ') != A * B @ C # answer(D). [back_demod(1653),demod(2412(5))]. given #169 (T,wt=11): 489 x ' @ y ' * x * y = e. [back_demod(210),demod(478(8))]. given #170 (T,wt=11): 618 x * (x @ y) @ y = x @ y. [back_demod(280),demod(599(5))]. given #171 (A,wt=20): 103 x * y * x ' * y * x * z = y * x * y * z. [para(13(a,1),19(a,1,2,2)),flip(a)]. given #172 (F,wt=18): 2560 (B @ C) * (A * (B ' @ C) @ C) != A * B @ C # answer(D). [back_demod(1652),demod(2412(6),2412(12,R))]. given #173 (F,wt=19): 2541 (B @ C) * (C ' @ A * (C @ B)) != C ' @ A * B # answer(D). [back_demod(1803),demod(2412(7),2412(12,R))]. given #174 (T,wt=11): 936 (x @ y ') * (y @ x ') = e. [para(601(a,1),146(a,1,1))]. given #175 (T,wt=11): 937 (x ' @ y) * (y ' @ x) = e. [para(601(a,2),146(a,1,1))]. given #176 (A,wt=22): 104 x ' * y * x * y * x ' * z = y * x ' * y * z. [para(13(a,1),19(a,1,2)),flip(a)]. given #177 (F,wt=19): 2547 C ' @ A * B != (A * (C @ B) @ C) * (C @ B ') # answer(D). [back_demod(1765),demod(2412(11))]. given #178 (F,wt=19): 2548 (C @ B ') * (C ' @ A * (C @ B)) != A * B @ C # answer(D). [back_demod(1764),demod(2412(7),2412(13,R))]. given #179 (T,wt=11): 999 x ' * y @ x * y ' = e. [para(55(a,2),165(a,1,1)),demod(136(5),88(4),590(9,R),694(9))]. given #180 (T,wt=11): 1004 x * y ' @ x ' * y = e. [para(55(a,2),226(a,1,2)),demod(136(3),88(2),668(9))]. given #181 (A,wt=19): 105 (x @ y) * z * y * x * u = z * x * y * u. [para(19(a,1),14(a,1,2,2)),demod(13(8),13(6)),flip(a)]. given #182 (F,wt=13): 3253 C @ A ' * B ' != A * B @ C # answer(D). [back_demod(658),demod(3243(9))]. given #183 (F,wt=11): 3255 B * A @ C != A * B @ C # answer(D). [para(575(a,2),3253(a,1)),demod(136(6),88(3),88(4))]. given #184 (T,wt=11): 1367 x @ (y @ x) * z = x @ z. [para(61(a,2),10(a,1,2,2)),demod(136(4),137(4),7(9),602(8),10(5)),flip(a)]. given #185 (T,wt=11): 2411 (x @ y) * z * (y @ x) = z. [para(99(a,1),14(a,1,2,2)),demod(88(2),88(2),84(5),84(3),593(3)),flip(a)]. given #186 (A,wt=23): 107 x ' * y ' * z * (y @ x) * u = y ' * x ' * z * u. [para(14(a,1),19(a,1,2,2,2)),demod(13(14),13(12))]. given #187 (F,wt=12): 3257 C ' @ B * A != A * B @ C # answer(D). [para(575(a,2),3255(a,1))]. given #188 (F,wt=12): 3258 C ' @ A * B != B * A @ C # answer(D). [para(575(a,2),3255(a,2)),flip(a)]. given #189 (T,wt=11): 2412 (x @ y) * z = z * (x @ y). [para(99(a,2),14(a,1,2,2)),demod(88(2),88(2),84(7),84(5),593(5)),flip(a)]. given #190 (T,wt=11): 2650 (x @ y) * y * x = x * y. [back_demod(886),demod(2619(7))]. given #191 (A,wt=17): 108 x * y ' * (x @ y) * z = y ' * x * z. [para(14(a,1),19(a,1,2,2)),demod(13(10),13(9))]. given #192 (F,wt=13): 3256 C @ B ' * A ' != B * A @ C # answer(D). [para(486(a,2),3255(a,2)),demod(136(10)),flip(a)]. given #193 (F,wt=13): 3425 C ' @ B * A != C ' @ A * B # answer(D). [para(575(a,2),3257(a,2))]. given #194 (T,wt=11): 3259 x @ (x @ y) * z = x @ z. [para(84(a,1),1367(a,1,2)),demod(137(3)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.69 (+ 0.01) seconds: D. % Length of proof is 89. % Level of proof is 22. % Maximum clause weight is 23. % Given clauses 194. 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 @ C) * (B @ C) != A * B @ C # answer(D). [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))]. 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))]. 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))]. 51 x ' * y * x * (y @ z) = (x @ y ') * z ' * y * z. [para(10(a,1),14(a,1,2,2,2)),demod(37(6))]. 53 (x ' @ y) * x = x * (y @ x). [para(10(a,1),14(a,1,2)),demod(37(4)),flip(a)]. 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 (x ' @ y) * x * z = x * (y @ x) * z. [para(14(a,1),14(a,1,2)),demod(37(5)),flip(a)]. 62 e ' = e. [para(40(a,1),9(a,1))]. 65 (x * y ') ' * y ' * x = x * y ' @ y. [para(9(a,1),15(a,1,2,2,2)),demod(40(6))]. 70 (x * y) ' * y * x = x * y @ x. [para(13(a,1),15(a,1,2))]. 75 x * y ' @ y = x * y ' @ x. [back_demod(65),demod(70(6)),flip(a)]. 76 x * y * (x * y @ x) = y * x. [back_demod(42),demod(70(4))]. 79 x * x ' = e. [para(37(a,1),9(a,1))]. 81 x ' * y * x * y ' = x @ y '. [para(37(a,1),10(a,1,2))]. 84 x * x ' * y = y. [para(37(a,1),13(a,1))]. 88 x ' ' = x. [para(37(a,1),40(a,1)),demod(40(2)),flip(a)]. 91 x * y * (x * y) ' = e. [para(79(a,1),7(a,1)),flip(a)]. 94 x * y @ y ' = x * y @ x. [para(79(a,1),15(a,1,2,2,2)),demod(88(4),40(4),70(4)),flip(a)]. 99 x ' * y ' * z * (y @ x) = y ' * x ' * z. [para(10(a,1),19(a,1,2,2,2)),demod(13(12),9(10),40(10))]. 105 (x @ y) * z * y * x * u = z * x * y * u. [para(19(a,1),14(a,1,2,2)),demod(13(8),13(6)),flip(a)]. 123 x * (y * x) ' = y '. [para(91(a,1),13(a,1,2)),demod(40(3)),flip(a)]. 125 (x @ y) * z * (x ' * y ' * x * y * z) ' = e. [para(14(a,2),91(a,1,2,2,1))]. 136 (x * y) ' = y ' * x '. [para(123(a,1),13(a,1,2)),flip(a)]. 137 (x @ y) ' = y @ x. [para(14(a,2),123(a,1,2,1)),demod(136(7),136(5),136(3),136(2),7(5),88(7),7(6),7(5),88(8),7(7),7(6),7(5),10(6),84(4)),flip(a)]. 146 (x @ y) * (y @ x) = e. [back_demod(125),demod(136(8),136(6),136(4),136(3),7(6),88(8),7(7),7(6),88(9),7(8),7(7),7(6),10(7),84(5))]. 152 x * y @ x = y @ x. [back_demod(70),demod(136(2),7(5),10(5)),flip(a)]. 165 x * y @ y ' = y @ x. [back_demod(94),demod(152(5))]. 166 x * y * (y @ x) = y * x. [back_demod(76),demod(152(2))]. 167 x * y ' @ y = y ' @ x. [back_demod(75),demod(152(6))]. 180 (x @ y) * (y @ x) * z = z. [para(137(a,1),13(a,1,1))]. 187 x * y @ x ' = y @ x '. [para(13(a,1),152(a,1,1)),flip(a)]. 191 x ' * y @ x = y @ x. [para(84(a,1),152(a,1,1)),flip(a)]. 193 x @ x * y = x @ y. [para(152(a,1),137(a,1,1)),demod(137(2)),flip(a)]. 210 x ' @ y ' * x * y = x ' @ (x @ y). [para(10(a,1),193(a,1,2)),flip(a)]. 226 x ' @ y * x = y @ x. [para(165(a,1),137(a,1,1)),demod(137(2)),flip(a)]. 240 (x @ y) * y * x = x * y. [para(23(a,1),14(a,1,2,2)),demod(13(6),13(4)),flip(a)]. 260 x @ y * x ' = y @ x '. [para(88(a,1),226(a,1,1))]. 364 (x @ y) @ y * x = e. [para(240(a,1),10(a,1,2,2)),demod(137(2),136(3),7(6),10(6),146(3)),flip(a)]. 366 (x ' @ (x @ y)) * (y @ x ') = x @ y. [para(10(a,1),240(a,2)),demod(210(5),7(8),7(7),81(8))]. 404 (x @ y) @ x = e. [para(84(a,1),364(a,1,2)),demod(191(3))]. 422 x @ (x @ y) = e. [para(404(a,1),137(a,1,1)),demod(62(2)),flip(a)]. 425 (x @ y) * x = x * (x @ y). [para(404(a,1),166(a,1,2,2)),demod(40(3)),flip(a)]. 462 (x @ y) @ x ' = e. [para(422(a,1),165(a,2)),demod(425(2),187(4))]. 465 (x ' @ y) @ x = e. [para(422(a,1),167(a,2)),demod(425(4),191(5))]. 478 x ' @ (x @ y) = e. [para(462(a,1),137(a,1,1)),demod(62(2)),flip(a)]. 483 (x @ y) @ y = e. [para(226(a,1),462(a,1,1)),demod(88(3))]. 486 x @ y ' = y @ x. [back_demod(366),demod(478(3),8(4))]. 493 (x @ y) * y = y * (x @ y). [para(483(a,1),166(a,1,2,2)),demod(40(3)),flip(a)]. 575 x ' @ y = y @ x. [para(465(a,1),38(a,2,2)),demod(53(4),13(4),40(5)),flip(a)]. 583 (C @ A ') * (B @ C) != A * B @ C # answer(D). [para(486(a,2),12(a,1,1))]. 593 x ' @ y ' = x @ y. [para(486(a,2),152(a,1)),demod(136(2),260(4))]. 598 x * y @ z = z @ y ' * x '. [para(136(a,1),486(a,1,2)),flip(a)]. 602 (x @ y) * (x ' @ y) * z = z. [para(486(a,1),180(a,1,1))]. 657 C ' * A * C * A ' * (B @ C) != A * B @ C # answer(D). [para(14(a,2),583(a,1)),demod(88(5))]. 701 x ' * (y @ x ') * z ' * x * z = (x @ y) * (x @ z). [para(51(a,1),14(a,1,2))]. 724 x ' * y * x * (y @ z) = (y @ x) * z ' * y * z. [para(486(a,1),51(a,2,1))]. 1367 x @ (y @ x) * z = x @ z. [para(61(a,2),10(a,1,2,2)),demod(136(4),137(4),7(9),602(8),10(5)),flip(a)]. 1432 (x @ y) * x * z = x * (x @ y) * z. [para(575(a,1),61(a,2,2,1)),demod(593(3))]. 1537 (C @ A ' * (B @ C)) * (B @ C) != A * B @ C # answer(D). [para(54(a,2),657(a,1,2)),demod(7(19),493(18),84(20),1432(16),13(17))]. 1645 (C @ A ' * (C @ B ')) * (B @ C) != A * B @ C # answer(D). [para(486(a,2),1537(a,1,1,2,2))]. 1855 (C @ A ' * (C @ B ')) * (C @ B ') != A * B @ C # answer(D). [para(486(a,2),1645(a,1,2))]. 2412 (x @ y) * z = z * (x @ y). [para(99(a,2),14(a,1,2,2)),demod(88(2),88(2),84(7),84(5),593(5)),flip(a)]. 2534 (C @ B ') * (C @ A ' * (C @ B ')) != A * B @ C # answer(D). [back_demod(1855),demod(2412(14,R))]. 3123 (x @ y) * z ' * x * z = x * (x @ y * z). [para(105(a,2),38(a,1)),demod(136(3),7(7),13(6))]. 3209 x ' * y * x * (y @ z) = y * (y @ x * z). [back_demod(724),demod(3123(10))]. 3226 (x @ y ') * z ' * y * z = y * (y @ x * z). [back_demod(51),demod(3209(5)),flip(a)]. 3243 (x @ y) * (x @ z) = x @ y * z. [back_demod(701),demod(3226(7),13(5)),flip(a)]. 3246 C @ B ' * A ' * (C @ B ') != A * B @ C # answer(D). [back_demod(2534),demod(3243(14))]. 3259 x @ (x @ y) * z = x @ z. [para(84(a,1),1367(a,1,2)),demod(137(3)),flip(a)]. 3443 (x @ y) * (z @ u) * y * x = x * y * (z @ u). [para(2412(a,1),54(a,2)),demod(7(8))]. 3579 x @ y * z * (x @ u) = x @ y * z. [para(54(a,2),3259(a,1,2)),demod(3443(5))]. 3599 C @ B ' * A ' != A * B @ C # answer(D). [back_demod(3246),demod(3579(12))]. 3600 $F # answer(D). [resolve(3599,a,598,a(flip))]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=194. Generated=23157. Kept=3593. proofs=1. Usable=118. Sos=1771. Demods=974. Denials=0. 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=406964. 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.30. User_CPU=0.69, System_CPU=0.01, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13126 exit (max_proofs) Mon Jun 19 16:41:40 2006