============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 3873 was started by mccune on cleo.thornwood, Wed Nov 22 11:24:24 2006 The command was "/home/mccune/bin/prover9 -f gt.in ND.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 ND.in formulas(sos). (x @ y) * z = z * (x @ y). 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 = z * (x @ y). [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 = z * (x @ y). [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)]. 6 (x @ y) * z = z * (x @ y). [assumption]. % (lex-dep) 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 = z * (x @ y). [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): 20 x * e = x. [para(11(a,1),6(a,1,1)),rewrite(2(2),11(2)),flip(a)]. given #9 (T,wt=4): 21 e' = e. [para(20(a,1),3(a,1))]. given #10 (T,wt=5): 22 x @ e = e. [para(20(a,1),5(a,1,2,2)),rewrite(21(3),2(3),3(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. [para(3(a,1),8(a,1,2)),rewrite(20(4))]. given #13 (F,wt=5): 26 x @ x = e. [para(8(a,1),5(a,1,2)),rewrite(3(2)),flip(a)]. given #14 (T,wt=6): 12 x' @ x = e. [para(3(a,1),5(a,1,2,2)),rewrite(8(6)),flip(a)]. given #15 (T,wt=6): 31 x * x' = e. [para(24(a,1),3(a,1,1))]. 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): 49 A' * C' * A * C * (B @ C) != A * B @ C # answer(D). [para(9(a,2),7(a,1))]. given #18 (F,wt=6): 35 x @ x' = e. [para(24(a,1),12(a,1,1))]. given #19 (T,wt=7): 18 (x @ y) @ z = e. [para(6(a,1),5(a,1,2,2)),rewrite(8(6),6(4,R),17(4)),flip(a)]. given #20 (T,wt=7): 19 x @ (y @ z) = e. [para(6(a,2),5(a,1,2,2)),rewrite(8(6),3(2)),flip(a)]. 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=7): 81 x @ x * x = e. [para(10(a,1),10(a,1,2)),rewrite(3(2),21(2),79(3),2(4),3(4),11(5))]. given #23 (F,wt=8): 34 x * x' * y = y. [para(24(a,1),8(a,1,1))]. given #24 (T,wt=10): 36 x * y * (x * y)' = e. [para(31(a,1),1(a,1)),flip(a)]. given #25 (T,wt=9): 95 x * (y * x)' = y'. [para(36(a,1),8(a,1,2)),rewrite(20(3)),flip(a)]. given #26 (A,wt=15): 14 (x @ y) * z * u = z * (x @ y) * u. [para(6(a,1),1(a,1,1)),rewrite(1(3)),flip(a)]. given #27 (F,wt=8): 109 (x @ y)' = y @ x. [para(9(a,2),95(a,1,2,1)),rewrite(108(7),108(5),108(3),108(2),1(5),24(7),1(6),1(5),24(8),1(7),1(6),1(5),5(6),34(4)),flip(a)]. given #28 (F,wt=9): 114 (x @ y) * (y @ x) = e. [back_rewrite(93),rewrite(108(4),109(3),87(5))]. given #29 (T,wt=9): 121 x @ y * x = x @ y. [back_rewrite(84),rewrite(108(2),1(5),5(5)),flip(a)]. given #30 (T,wt=9): 147 x * y @ x = y @ x. [back_rewrite(79),rewrite(121(4))]. given #31 (A,wt=15): 15 (x @ y) * z * u = z * u * (x @ y). [para(6(a,2),1(a,1))]. given #32 (F,wt=19): 196 A' * C' * (B @ C) * A * C != A * B @ C # answer(D). [para(15(a,2),49(a,1,2,2))]. given #33 (F,wt=25): 205 A' * C' * B' * C' * B * C * A * C != A * B @ C # answer(D). [para(9(a,2),196(a,1,2,2))]. given #34 (T,wt=8): 179 x @ y' = y @ x. [para(8(a,1),147(a,1,1)),rewrite(177(5))]. given #35 (T,wt=8): 181 x' @ y = y @ x. [para(34(a,1),147(a,1,1)),rewrite(176(4)),flip(a)]. given #36 (A,wt=15): 16 x * (y @ z) * u = x * u * (y @ z). [para(6(a,1),1(a,2,2)),rewrite(1(3))]. given #37 (F,wt=14): 208 (B @ C) * (C @ A') != A * B @ C # answer(D). [para(179(a,2),7(a,1,1)),rewrite(6(8,R))]. given #38 (F,wt=14): 209 (A @ C) * (C @ B') != A * B @ C # answer(D). [para(179(a,2),7(a,1,2))]. given #39 (T,wt=9): 175 x * y @ y = x @ y. [para(121(a,1),109(a,1,1)),rewrite(109(2)),flip(a)]. given #40 (T,wt=9): 183 x @ x * y = x @ y. [para(147(a,1),109(a,1,1)),rewrite(109(2)),flip(a)]. given #41 (A,wt=12): 27 x' * y * x = y * (y @ x). [para(5(a,1),8(a,1,2)),rewrite(24(2)),flip(a)]. given #42 (F,wt=14): 230 C' @ A * B != (A @ C) * (B @ C) # answer(D). [para(181(a,2),7(a,2)),flip(a)]. given #43 (F,wt=15): 210 C @ B' * A' != (A @ C) * (B @ C) # answer(D). [para(179(a,2),7(a,2)),rewrite(108(12)),flip(a)]. given #44 (T,wt=9): 224 x' @ y' = x @ y. [para(179(a,2),179(a,1))]. given #45 (T,wt=9): 240 x' @ y = x @ y'. [para(181(a,1),179(a,1))]. given #46 (A,wt=12): 29 x' * (y @ z) * x = y @ z. [para(6(a,2),8(a,1,2))]. given #47 (F,wt=15): 268 (C @ A') * (C @ B') != A * B @ C # answer(D). [para(179(a,2),208(a,1,1)),rewrite(6(9,R))]. given #48 (F,wt=15): 270 C' @ A * B != (B @ C) * (C @ A') # answer(D). [para(181(a,2),208(a,2)),flip(a)]. given #49 (T,wt=10): 108 (x * y)' = y' * x'. [para(95(a,1),8(a,1,2)),flip(a)]. given #50 (T,wt=10): 145 x * y @ y' = y @ x. [back_rewrite(83),rewrite(121(5))]. given #51 (A,wt=14): 32 x * y' * x' * y = x' @ y. [para(24(a,1),5(a,1,1))]. given #52 (F,wt=15): 272 C' @ A * B != (A @ C) * (C @ B') # answer(D). [para(181(a,2),209(a,2)),flip(a)]. given #53 (F,wt=16): 269 C @ B' * A' != (B @ C) * (C @ A') # answer(D). [para(179(a,2),208(a,2)),rewrite(108(13)),flip(a)]. given #54 (T,wt=10): 177 x * y @ x' = x @ y. [back_rewrite(168),rewrite(175(5))]. given #55 (T,wt=10): 217 (x @ y) * (x' @ y) = e. [para(179(a,1),114(a,1,1))]. given #56 (A,wt=14): 33 x' * y * x * y' = x @ y'. [para(24(a,1),5(a,1,2,1))]. given #57 (F,wt=16): 271 C @ B' * A' != (A @ C) * (C @ B') # answer(D). [para(179(a,2),209(a,2)),rewrite(108(13)),flip(a)]. given #58 (F,wt=16): 307 B' * A' @ C' != (A @ C) * (B @ C) # answer(D). [para(181(a,2),230(a,1)),rewrite(108(4))]. given #59 (T,wt=10): 218 (x @ y) * (x @ y') = e. [para(179(a,2),114(a,1,1)),rewrite(6(4,R))]. given #60 (T,wt=10): 279 x' @ y * x = y @ x. [para(175(a,1),181(a,2))]. given #61 (A,wt=21): 37 x * y' * z' * y * z * u = x * (y @ z) * u. [para(9(a,1),1(a,2,2)),rewrite(1(7))]. given #62 (F,wt=16): 329 C' @ A * B != (C @ A') * (C @ B') # answer(D). [para(181(a,2),268(a,2)),flip(a)]. given #63 (F,wt=17): 328 C @ B' * A' != (C @ A') * (C @ B') # answer(D). [para(179(a,2),268(a,2)),rewrite(108(14)),flip(a)]. given #64 (T,wt=10): 296 x' * y * x @ y = e. [para(27(a,2),147(a,1,1)),rewrite(18(6))]. given #65 (T,wt=10): 305 x @ y' * x * y = e. [para(27(a,2),183(a,1,2)),rewrite(19(6))]. given #66 (A,wt=13): 40 x' * y * x = y * (x @ y'). [para(3(a,1),9(a,1,2,2,2)),rewrite(24(3),20(3),6(6))]. given #67 (F,wt=17): 331 B' * A' @ C' != (B @ C) * (C @ A') # answer(D). [para(181(a,2),270(a,1)),rewrite(108(4))]. given #68 (F,wt=17): 367 B' * A' @ C' != (A @ C) * (C @ B') # answer(D). [para(181(a,2),272(a,1)),rewrite(108(4))]. given #69 (T,wt=10): 444 x * y * x' @ y = e. [para(24(a,1),296(a,1,1,1))]. given #70 (T,wt=10): 458 x @ y * x * y' = e. [para(24(a,1),305(a,1,2,1))]. given #71 (A,wt=22): 43 x' * y * x * (y @ z) = (x @ y') * z' * y * z. [para(5(a,1),9(a,1,2,2,2)),rewrite(24(3))]. given #72 (F,wt=18): 440 B' * A' @ C' != (C @ A') * (C @ B') # answer(D). [para(181(a,2),329(a,1)),rewrite(108(4))]. given #73 (F,wt=20): 213 A' * C' * A * C * (C @ B') != A * B @ C # answer(D). [para(179(a,2),49(a,1,2,2,2,2))]. given #74 (T,wt=11): 100 x' * y' @ x * y = e. [back_rewrite(66),rewrite(96(8),3(8)),flip(a)]. given #75 (T,wt=9): 560 x * y @ y * x = e. [para(100(a,1),179(a,2)),rewrite(108(5),24(3),24(3))]. given #76 (A,wt=17): 46 x' * y' * x * y * z = z * (x @ y). [para(9(a,2),6(a,1))]. given #77 (F,wt=19): 591 B' * C' * B * C * (A @ C) != A * B @ C # answer(D). [para(46(a,2),7(a,1))]. given #78 (F,wt=19): 612 C' * A * C * (B @ C) * A' != A * B @ C # answer(D). [para(46(a,2),208(a,1)),rewrite(24(5),6(10,R))]. given #79 (T,wt=11): 133 x' @ x * y = x' @ y. [back_rewrite(25),rewrite(108(2),1(4),32(5)),flip(a)]. given #80 (T,wt=11): 144 (x @ y) * z * (y @ x) = z. [back_rewrite(28),rewrite(109(2))]. given #81 (A,wt=21): 48 x' * y' * x * (z @ u) * y = (x @ y) * (z @ u). [para(6(a,2),9(a,1,2,2,2))]. given #82 (F,wt=19): 613 C' * B * C * (A @ C) * B' != A * B @ C # answer(D). [para(46(a,2),209(a,1)),rewrite(24(5),6(10,R))]. given #83 (F,wt=19): 650 C' * A * (B @ C) * C * A' != A * B @ C # answer(D). [para(14(a,2),612(a,1,2,2))]. given #84 (T,wt=11): 146 x * y' @ y = y' @ x. [back_rewrite(82),rewrite(121(7))]. given #85 (T,wt=11): 155 (x @ y) * (y @ x) * z = z. [para(14(a,2),8(a,1)),rewrite(109(3))]. given #86 (A,wt=16): 50 x' * y * x * z = y * (y @ x) * z. [para(9(a,1),8(a,1,2)),rewrite(24(2)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.10 (+ 0.00) seconds: D. % Length of proof is 36. % Level of proof is 16. % Maximum clause weight is 21. % Given clauses 86. 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 = z * (x @ y). [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)]. 20 x * e = x. [para(11(a,1),6(a,1,1)),rewrite(2(2),11(2)),flip(a)]. 24 x'' = x. [para(3(a,1),8(a,1,2)),rewrite(20(4))]. 31 x * x' = e. [para(24(a,1),3(a,1,1))]. 34 x * x' * y = y. [para(24(a,1),8(a,1,1))]. 36 x * y * (x * y)' = e. [para(31(a,1),1(a,1)),flip(a)]. 48 x' * y' * x * (z @ u) * y = (x @ y) * (z @ u). [para(6(a,2),9(a,1,2,2,2))]. 50 x' * y * x * z = y * (y @ x) * z. [para(9(a,1),8(a,1,2)),rewrite(24(2)),flip(a)]. 75 (x * y)' * y * x = x * y @ x. [para(8(a,1),10(a,1,2))]. 79 x * y @ x = y @ x * y. [para(9(a,1),10(a,1,2)),rewrite(8(3),6(4),8(5),8(5))]. 84 (x * y)' * y * x = y @ x * y. [back_rewrite(75),rewrite(79(6))]. 95 x * (y * x)' = y'. [para(36(a,1),8(a,1,2)),rewrite(20(3)),flip(a)]. 108 (x * y)' = y' * x'. [para(95(a,1),8(a,1,2)),flip(a)]. 109 (x @ y)' = y @ x. [para(9(a,2),95(a,1,2,1)),rewrite(108(7),108(5),108(3),108(2),1(5),24(7),1(6),1(5),24(8),1(7),1(6),1(5),5(6),34(4)),flip(a)]. 121 x @ y * x = x @ y. [back_rewrite(84),rewrite(108(2),1(5),5(5)),flip(a)]. 147 x * y @ x = y @ x. [back_rewrite(79),rewrite(121(4))]. 168 x * y @ x' = x * y @ y. [para(8(a,1),121(a,1,2)),flip(a)]. 175 x * y @ y = x @ y. [para(121(a,1),109(a,1,1)),rewrite(109(2)),flip(a)]. 177 x * y @ x' = x @ y. [back_rewrite(168),rewrite(175(5))]. 179 x @ y' = y @ x. [para(8(a,1),147(a,1,1)),rewrite(177(5))]. 208 (B @ C) * (C @ A') != A * B @ C # answer(D). [para(179(a,2),7(a,1,1)),rewrite(6(8,R))]. 268 (C @ A') * (C @ B') != A * B @ C # answer(D). [para(179(a,2),208(a,1,1)),rewrite(6(9,R))]. 328 C @ B' * A' != (C @ A') * (C @ B') # answer(D). [para(179(a,2),268(a,2)),rewrite(108(14)),flip(a)]. 332 x' * y' * z' * x * z * y = x @ z * y. [para(108(a,1),5(a,1,2,1)),rewrite(1(7))]. 781 x @ y * z = (x @ z) * (x @ y). [para(50(a,2),48(a,1,2,2)),rewrite(332(8))]. 782 $F # answer(D). [resolve(781,a,328,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=86. Generated=4693. Kept=780. proofs=1. Usable=78. Sos=466. Demods=269. Limbo=80, Disabled=161. Hints=0. Weight_deleted=180. Literals_deleted=0. Forward_subsumed=3733. Back_subsumed=12. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=395 (2 lex), Back_demodulated=143. Back_unit_deleted=0. Demod_attempts=60795. Demod_rewrites=11737. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.66. User_CPU=0.10, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3873 exit (max_proofs) Wed Nov 22 11:24:24 2006