============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13111 was started by mccune on cleo.thornwood, Mon Jun 19 16:41:24 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). 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 AD.in clauses(sos). (x @ y) @ z = u @ (v @ w). 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 = u @ (v @ w). [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 = u @ (v @ w). [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=11): 11 (x @ y) @ z = u @ (v @ w). [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=5): 24 x @ e = e. [back_demod(22),demod(23(2)),flip(a)]. given #9 (T,wt=6): 17 x ' @ x = e. [para(9(a,1),10(a,1,2,2)),demod(13(6)),flip(a)]. given #10 (T,wt=7): 21 x @ (y @ z) = e. [para(16(a,1),11(a,1,1)),demod(16(2)),flip(a)]. given #11 (A,wt=8): 13 x ' * x * y = y. [para(9(a,1),7(a,1,1)),demod(8(2)),flip(a)]. given #12 (F,wt=5): 29 x @ x = e. [para(13(a,1),10(a,1,2)),demod(9(2)),flip(a)]. given #13 (F,wt=5): 34 x * e = x. [back_demod(27),demod(31(4))]. given #14 (T,wt=4): 36 e ' = e. [para(34(a,1),9(a,1))]. given #15 (T,wt=7): 23 (x @ y) @ z = e. [para(16(a,1),11(a,2))]. given #16 (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 #17 (F,wt=19): 46 A ' * C ' * A * C * (B @ C) != A * B @ C # answer(D). [para(14(a,2),12(a,1))]. given #18 (F,wt=9): 31 x ' ' * y = x * y. [para(13(a,1),13(a,1,2))]. given #19 (T,wt=5): 61 x ' ' = x. [para(31(a,1),34(a,1)),demod(34(2)),flip(a)]. given #20 (T,wt=6): 56 x * x ' = e. [para(31(a,1),9(a,1))]. given #21 (A,wt=19): 15 (x * y) ' * z ' * x * y * z = x * y @ z. [para(7(a,1),10(a,1,2,2))]. given #22 (F,wt=6): 64 x @ x ' = e. [para(61(a,1),17(a,1,1))]. given #23 (F,wt=7): 80 x * x @ x = e. [para(15(a,1),15(a,1,2)),demod(9(2),36(2),8(4),9(4),16(5))]. given #24 (T,wt=8): 60 x * x ' * y = y. [para(31(a,1),13(a,1))]. given #25 (T,wt=10): 65 x * y * (x * y) ' = e. [para(56(a,1),7(a,1)),flip(a)]. given #26 (A,wt=12): 25 (x * y) ' * x * y * z = z. [para(7(a,1),13(a,1,2))]. given #27 (F,wt=7): 98 x @ x * x = e. [para(25(a,1),10(a,1,2)),demod(9(2)),flip(a)]. given #28 (F,wt=9): 89 x * (y * x) ' = y '. [para(65(a,1),13(a,1,2)),demod(34(3)),flip(a)]. given #29 (T,wt=8): 119 (x @ y) ' = y @ x. [para(14(a,2),89(a,1,2,1)),demod(118(7),118(5),118(3),118(2),7(5),61(7),7(6),7(5),61(8),7(7),7(6),7(5),10(6),60(4)),flip(a)]. given #30 (T,wt=9): 132 (x @ y) * (y @ x) = e. [back_demod(91),demod(118(8),118(6),118(4),118(3),7(6),61(8),7(7),7(6),61(9),7(8),7(7),7(6),10(7),60(5))]. given #31 (A,wt=12): 32 x ' * y * x = y * (y @ x). [back_demod(30),demod(31(4)),flip(a)]. given #32 (F,wt=9): 136 x * y @ x = y @ x. [back_demod(74),demod(118(2),7(5),10(5)),flip(a)]. given #33 (F,wt=9): 160 x @ y * x = x @ y. [back_demod(153),demod(159(4)),flip(a)]. given #34 (T,wt=8): 189 x ' @ y = y @ x. [back_demod(185),demod(186(3))]. given #35 (T,wt=8): 190 x @ y ' = y @ x. [back_demod(182),demod(186(2)),flip(a)]. given #36 (A,wt=21): 37 x * y ' * z ' * y * z * u = x * (y @ z) * u. [para(14(a,1),7(a,2,2)),demod(7(7))]. given #37 (F,wt=14): 193 C ' @ A * B != (A @ C) * (B @ C) # answer(D). [para(189(a,2),12(a,2)),flip(a)]. given #38 (F,wt=14): 209 (C @ A ') * (B @ C) != A * B @ C # answer(D). [para(190(a,2),12(a,1,1))]. given #39 (T,wt=9): 178 x @ x * y = x @ y. [para(136(a,1),119(a,1,1)),demod(119(2)),flip(a)]. given #40 (T,wt=9): 186 x * y @ y = x @ y. [para(160(a,1),119(a,1,1)),demod(119(2)),flip(a)]. given #41 (A,wt=13): 40 x ' * y * x = (x @ y ') * y. [para(9(a,1),14(a,1,2,2,2)),demod(34(5),31(4))]. given #42 (F,wt=14): 210 (A @ C) * (C @ B ') != A * B @ C # answer(D). [para(190(a,2),12(a,1,2))]. given #43 (F,wt=15): 211 C @ B ' * A ' != (A @ C) * (B @ C) # answer(D). [para(190(a,2),12(a,2)),demod(118(12)),flip(a)]. given #44 (T,wt=9): 204 x ' @ y ' = x @ y. [para(189(a,2),189(a,1))]. given #45 (T,wt=9): 220 x ' @ y = x @ y '. [para(190(a,1),189(a,1)),flip(a)]. given #46 (A,wt=22): 43 x ' * y * x * (y @ z) = (x @ y ') * z ' * y * z. [para(10(a,1),14(a,1,2,2,2)),demod(31(6))]. given #47 (F,wt=15): 236 C ' @ A * B != (C @ A ') * (B @ C) # answer(D). [para(189(a,2),193(a,2,1)),demod(220(10))]. given #48 (F,wt=15): 237 C ' @ A * B != (A @ C) * (C @ B ') # answer(D). [para(189(a,2),193(a,2,2)),demod(220(13))]. given #49 (T,wt=10): 118 (x * y) ' = y ' * x '. [para(89(a,1),13(a,1,2)),flip(a)]. given #50 (T,wt=10): 152 x * y @ y ' = y @ x. [back_demod(79),demod(136(5))]. given #51 (A,wt=12): 45 (x ' @ y) * x = x * (y @ x). [para(10(a,1),14(a,1,2)),demod(31(4)),flip(a)]. given #52 (F,wt=15): 239 (C @ A ') * (C @ B ') != A * B @ C # answer(D). [para(189(a,2),209(a,1,2)),demod(220(8))]. given #53 (F,wt=16): 235 B ' * A ' @ C ' != (A @ C) * (B @ C) # answer(D). [para(189(a,2),193(a,1)),demod(118(4))]. given #54 (T,wt=10): 162 x ' @ y * x = y @ x. [para(32(a,1),10(a,1,2,2)),demod(61(2),118(2),7(6),13(5),60(4)),flip(a)]. given #55 (T,wt=10): 177 x ' * y @ x = y @ x. [para(60(a,1),136(a,1,1)),flip(a)]. given #56 (A,wt=16): 48 x ' * y * x * z = y * (y @ x) * z. [para(14(a,1),13(a,1,2)),demod(31(5)),flip(a)]. given #57 (F,wt=14): 415 (B @ C) * (C @ A ') != A * B @ C # answer(D). [back_demod(209),demod(372(8,R))]. given #58 (F,wt=15): 414 C ' @ A * B != (B @ C) * (C @ A ') # answer(D). [back_demod(236),demod(372(14,R))]. given #59 (T,wt=10): 180 x ' * y * x @ y = e. [para(32(a,2),136(a,1,1)),demod(23(6))]. given #60 (T,wt=10): 198 (x @ y) * (x @ y ') = e. [para(189(a,1),132(a,1,1))]. given #61 (A,wt=17): 50 x ' * y * x * z = (x @ y ') * y * z. [para(13(a,1),14(a,1,2,2,2)),demod(31(5))]. given #62 (F,wt=16): 266 C @ B ' * A ' != (A @ C) * (C @ B ') # answer(D). [para(190(a,2),210(a,2)),demod(118(13)),flip(a)]. given #63 (F,wt=16): 306 C ' @ A * B != (C @ A ') * (C @ B ') # answer(D). [para(189(a,2),236(a,2,2)),demod(220(14))]. given #64 (T,wt=10): 201 (x @ y) * (x ' @ y) = e. [para(189(a,2),132(a,1,2))]. given #65 (T,wt=10): 245 x @ y ' * x * y = e. [para(32(a,2),178(a,1,2)),demod(21(6))]. given #66 (A,wt=16): 53 (x ' @ y) * x * z = x * (y @ x) * z. [para(14(a,1),14(a,1,2)),demod(31(5)),flip(a)]. given #67 (F,wt=16): 412 C @ B ' * A ' != (B @ C) * (C @ A ') # answer(D). [back_demod(240),demod(372(15,R))]. given #68 (F,wt=17): 308 B ' * A ' @ C ' != (A @ C) * (C @ B ') # answer(D). [para(189(a,2),237(a,1)),demod(118(4))]. given #69 (T,wt=10): 423 x * y * x ' @ y = e. [para(61(a,1),180(a,1,1,1))]. given #70 (T,wt=10): 492 x @ y * x * y ' = e. [para(61(a,1),245(a,1,2,1))]. given #71 (A,wt=14): 58 x ' * y * x * y ' = x @ y '. [para(31(a,1),10(a,1,2))]. given #72 (F,wt=17): 340 C @ B ' * A ' != (C @ A ') * (C @ B ') # answer(D). [para(190(a,2),239(a,2)),demod(118(14)),flip(a)]. given #73 (F,wt=17): 409 B ' * A ' @ C ' != (B @ C) * (C @ A ') # answer(D). [back_demod(305),demod(372(16,R))]. given #74 (T,wt=11): 131 x * y * (y @ x) = y * x. [back_demod(100),demod(118(4),61(2),61(2),7(3))]. given #75 (T,wt=11): 143 x ' @ x * y = x ' @ y. [back_demod(33),demod(118(2),7(4),59(5)),flip(a)]. given #76 (A,wt=14): 59 x * y ' * x ' * y = x ' @ y. [para(31(a,1),10(a,1))]. given #77 (F,wt=18): 481 B ' * A ' @ C ' != (C @ A ') * (C @ B ') # answer(D). [para(189(a,2),306(a,1)),demod(118(4))]. given #78 (F,wt=19): 413 C ' * A * C * (B @ C) * A ' != A * B @ C # answer(D). [back_demod(238),demod(372(10,R))]. given #79 (T,wt=11): 151 x * y ' @ y = y ' @ x. [back_demod(81),demod(136(6))]. given #80 (T,wt=11): 158 (x @ y) * (y @ x) * z = z. [para(119(a,1),13(a,1,1))]. given #81 (A,wt=18): 62 x ' * y * x * y ' * z = (x @ y ') * z. [para(31(a,1),14(a,1,2))]. given #82 (F,wt=18): 640 A * (A @ C) * (B @ C) * A ' != A * B @ C # answer(D). [para(48(a,1),413(a,1))]. given #83 (F,wt=19): 641 (C @ A ') * A * (B @ C) * A ' != A * B @ C # answer(D). [para(50(a,1),413(a,1))]. given #84 (T,wt=11): 165 (x @ y) * z * (y @ x) = z. [para(21(a,1),32(a,2,2)),demod(119(2),34(6))]. given #85 (T,wt=11): 174 x ' * y * x @ y ' = e. [para(10(a,1),136(a,1,1)),demod(23(3)),flip(a)]. given #86 (A,wt=18): 63 (x ' @ y) * z = x * y ' * x ' * y * z. [para(31(a,1),14(a,1)),flip(a)]. given #87 (F,wt=19): 689 A * (C @ A ') * (B @ C) * A ' != A * B @ C # answer(D). [para(189(a,2),640(a,1,2,1)),demod(220(5))]. given #88 (F,wt=19): 691 C ' @ A * B != A * (A @ C) * (B @ C) * A ' # answer(D). [para(189(a,2),640(a,2)),flip(a)]. given #89 (T,wt=11): 175 x * y @ x ' = y @ x '. [para(13(a,1),136(a,1,1)),flip(a)]. given #90 (T,wt=11): 218 x @ x ' * y = y @ x '. [para(190(a,1),136(a,1))]. given #91 (A,wt=14): 66 x ' * y ' * x = (x @ y) * y '. [para(56(a,1),14(a,1,2,2,2)),demod(34(4))]. given #92 (F,wt=20): 197 A ' * C ' * A * C * (B @ C) != C ' @ A * B # answer(D). [para(189(a,2),46(a,2))]. given #93 (F,wt=20): 214 A ' * C ' * A * C * (C @ B ') != A * B @ C # answer(D). [para(190(a,2),46(a,1,2,2,2,2))]. given #94 (T,wt=11): 253 x @ y * x ' = y @ x '. [para(186(a,1),190(a,1)),flip(a)]. given #95 (T,wt=11): 273 (x @ y ') * (y @ x ') = e. [para(220(a,1),132(a,1,1))]. given #96 (A,wt=18): 72 x ' * y * z * x = y * z * (y * z @ x). [para(15(a,1),13(a,1,2)),demod(61(3),7(4)),flip(a)]. given #97 (F,wt=20): 339 C ' * A * C * A ' * (C @ B ') != A * B @ C # answer(D). [para(14(a,2),239(a,1)),demod(61(5))]. given #98 (F,wt=20): 410 C ' * A * C * (B @ C) * A ' != C ' @ A * B # answer(D). [back_demod(304),demod(372(10,R))]. given #99 (T,wt=11): 274 (x ' @ y) * (y ' @ x) = e. [para(220(a,2),132(a,1,1))]. given #100 (T,wt=11): 310 x * y @ y ' * x ' = e. [para(118(a,1),64(a,1,2))]. given #101 (A,wt=21): 77 x ' * y ' * x * y * z @ u = (x @ y) * z @ u. [para(14(a,2),15(a,2,1)),demod(15(9)),flip(a)]. given #102 (F,wt=20): 417 B ' * C ' * B * C * (C @ A ') != A * B @ C # answer(D). [para(14(a,2),415(a,1))]. given #103 (F,wt=19): 981 B ' * C ' * B * C * (A @ C) != A * B @ C # answer(D). [para(189(a,2),417(a,1,2,2,2,2)),demod(61(9))]. given #104 (T,wt=11): 372 (x @ y) * z = z * (x @ y). [para(132(a,1),48(a,1,2,2)),demod(119(2),34(3),21(4),8(5))]. given #105 (T,wt=11): 424 x @ y ' * x ' * y = e. [para(180(a,1),190(a,1)),flip(a)]. given #106 (A,wt=18): 84 x ' * y ' * x * z = (x @ y) * y ' * z. [para(60(a,1),14(a,1,2,2,2))]. given #107 (F,wt=20): 692 C @ B ' * A ' != A * (A @ C) * (B @ C) * A ' # answer(D). [para(190(a,2),640(a,2)),demod(118(17)),flip(a)]. given #108 (F,wt=20): 766 C ' @ A * B != A * (C @ A ') * (B @ C) * A ' # answer(D). [para(189(a,2),689(a,2)),flip(a)]. given #109 (T,wt=11): 557 x @ y * x ' * y ' = e. [para(423(a,1),190(a,1)),flip(a)]. given #110 (T,wt=11): 819 x ' * y ' @ x * y = e. [back_demod(138),demod(818(12))]. given #111 (A,wt=24): 121 x ' * y ' * z * x * y * z ' = y * x @ x ' * z '. [para(89(a,1),15(a,1,2,2,2)),demod(118(2),118(5),118(7),61(5),61(5),7(7),7(8),118(11))]. given #112 (F,wt=16): 1115 C @ B ' * C ' * A ' != A * B @ C # answer(D). [back_demod(980),demod(1086(14))]. ============================== PROOF ================================= % Proof 1 at 0.16 (+ 0.00) seconds: D. % Length of proof is 60. % Level of proof is 17. % Maximum clause weight is 25. % Given clauses 112. 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 = u @ (v @ w). [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))]. 16 e @ x = e. [para(8(a,1),10(a,1,2,2)),demod(9(4),9(4)),flip(a)]. 21 x @ (y @ z) = e. [para(16(a,1),11(a,1,1)),demod(16(2)),flip(a)]. 25 (x * y) ' * x * y * z = z. [para(7(a,1),13(a,1,2))]. 27 x ' ' * e = x. [para(9(a,1),13(a,1,2))]. 30 x ' ' * (x @ y) = y ' * x * y. [para(10(a,1),13(a,1,2))]. 31 x ' ' * y = x * y. [para(13(a,1),13(a,1,2))]. 32 x ' * y * x = y * (y @ x). [back_demod(30),demod(31(4)),flip(a)]. 34 x * e = x. [back_demod(27),demod(31(4))]. 48 x ' * y * x * z = y * (y @ x) * z. [para(14(a,1),13(a,1,2)),demod(31(5)),flip(a)]. 56 x * x ' = e. [para(31(a,1),9(a,1))]. 60 x * x ' * y = y. [para(31(a,1),13(a,1))]. 61 x ' ' = x. [para(31(a,1),34(a,1)),demod(34(2)),flip(a)]. 65 x * y * (x * y) ' = e. [para(56(a,1),7(a,1)),flip(a)]. 74 (x * y) ' * y * x = x * y @ x. [para(13(a,1),15(a,1,2))]. 76 x ' * (y * x @ y) * x = x @ y * x. [para(14(a,1),15(a,1,2)),demod(13(3),13(8))]. 77 x ' * y ' * x * y * z @ u = (x @ y) * z @ u. [para(14(a,2),15(a,2,1)),demod(15(9)),flip(a)]. 89 x * (y * x) ' = y '. [para(65(a,1),13(a,1,2)),demod(34(3)),flip(a)]. 91 (x @ y) * z * (x ' * y ' * x * y * z) ' = e. [para(14(a,2),65(a,1,2,2,1))]. 100 (x ' * y ') ' * (x @ y) = x * y. [para(10(a,1),25(a,1,2))]. 118 (x * y) ' = y ' * x '. [para(89(a,1),13(a,1,2)),flip(a)]. 119 (x @ y) ' = y @ x. [para(14(a,2),89(a,1,2,1)),demod(118(7),118(5),118(3),118(2),7(5),61(7),7(6),7(5),61(8),7(7),7(6),7(5),10(6),60(4)),flip(a)]. 121 x ' * y ' * z * x * y * z ' = y * x @ x ' * z '. [para(89(a,1),15(a,1,2,2,2)),demod(118(2),118(5),118(7),61(5),61(5),7(7),7(8),118(11))]. 131 x * y * (y @ x) = y * x. [back_demod(100),demod(118(4),61(2),61(2),7(3))]. 132 (x @ y) * (y @ x) = e. [back_demod(91),demod(118(8),118(6),118(4),118(3),7(6),61(8),7(7),7(6),61(9),7(8),7(7),7(6),10(7),60(5))]. 136 x * y @ x = y @ x. [back_demod(74),demod(118(2),7(5),10(5)),flip(a)]. 153 x ' * (x @ y) * x = x @ y * x. [back_demod(76),demod(136(3))]. 159 x ' * (y @ z) * x = y @ z. [para(132(a,1),14(a,1,2,2,2)),demod(119(3),34(4),21(6),8(7))]. 160 x @ y * x = x @ y. [back_demod(153),demod(159(4)),flip(a)]. 175 x * y @ x ' = y @ x '. [para(13(a,1),136(a,1,1)),flip(a)]. 177 x ' * y @ x = y @ x. [para(60(a,1),136(a,1,1)),flip(a)]. 182 x * y @ y = y @ x '. [para(13(a,1),160(a,1,2)),demod(175(5))]. 185 x ' * y @ y = y @ x. [para(60(a,1),160(a,1,2)),demod(177(6))]. 186 x * y @ y = x @ y. [para(160(a,1),119(a,1,1)),demod(119(2)),flip(a)]. 189 x ' @ y = y @ x. [back_demod(185),demod(186(3))]. 190 x @ y ' = y @ x. [back_demod(182),demod(186(2)),flip(a)]. 209 (C @ A ') * (B @ C) != A * B @ C # answer(D). [para(190(a,2),12(a,1,1))]. 367 (x @ y) * z * y ' * x ' * y * x * u = z * u. [para(14(a,2),48(a,1,2,2)),demod(119(2),21(11),8(11))]. 372 (x @ y) * z = z * (x @ y). [para(132(a,1),48(a,1,2,2)),demod(119(2),34(3),21(4),8(5))]. 404 x * (x @ y) * z @ y = x * y * z @ y. [para(48(a,1),177(a,1,1))]. 415 (B @ C) * (C @ A ') != A * B @ C # answer(D). [back_demod(209),demod(372(8,R))]. 417 B ' * C ' * B * C * (C @ A ') != A * B @ C # answer(D). [para(14(a,2),415(a,1))]. 907 (x @ y) * z @ u = z @ u. [para(77(a,1),10(a,2)),demod(118(7),118(5),118(3),118(2),7(5),61(7),7(6),7(5),61(8),7(7),7(6),7(5),10(6),7(11),7(10),7(9),7(8),7(13),367(12),10(5)),flip(a)]. 912 x ' * y * x * z @ u = y * z @ u. [para(13(a,1),77(a,1,1,2,2,2)),demod(61(3),907(10))]. 913 x * (x @ y) * z @ u = x * z @ u. [para(14(a,1),77(a,1,1,2,2,2)),demod(61(3),912(7),907(12),912(9))]. 941 x * (y @ z) @ u = x @ u. [para(131(a,1),77(a,2,1)),demod(21(4),34(4),912(7),13(3)),flip(a)]. 957 x * y * z @ y = x * z @ y. [back_demod(404),demod(913(4)),flip(a)]. 980 B ' * C ' * B * A * C * A ' != A * B @ C # answer(D). [para(32(a,2),417(a,1,2,2,2)),demod(61(8))]. 1086 x ' * y ' * x * z * y * z ' = y @ x ' * y ' * z '. [para(32(a,1),121(a,2,1)),demod(118(2),61(5),7(8),60(7),7(8),118(12),7(15),941(16))]. 1115 C @ B ' * C ' * A ' != A * B @ C # answer(D). [back_demod(980),demod(1086(14))]. 1118 $F # answer(D). [para(189(a,2),1115(a,1)),demod(118(9),118(6),61(3),61(4),61(6),7(5),957(7)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=112. Generated=6733. Kept=1111. proofs=1. Usable=91. Sos=587. Demods=324. Denials=0. 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=100518. 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.79. User_CPU=0.16, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13111 exit (max_proofs) Mon Jun 19 16:41:24 2006