============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13132 was started by mccune on cleo.thornwood, Mon Jun 19 16:41:41 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). 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 ND.in clauses(sos). (x @ y) * z = 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 = 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 = 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)]. 11 (x @ y) * z = z * (x @ y). [input]. % (lex-dep) 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 = 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=5): 25 x * e = x. [para(16(a,1),11(a,1,1)),demod(8(2),16(2)),flip(a)]. given #9 (T,wt=4): 26 e ' = e. [para(25(a,1),9(a,1))]. given #10 (T,wt=5): 27 x @ e = e. [para(25(a,1),10(a,1,2,2)),demod(26(3),8(3),9(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. [para(9(a,1),13(a,1,2)),demod(25(4))]. given #13 (F,wt=5): 31 x @ x = e. [para(13(a,1),10(a,1,2)),demod(9(2)),flip(a)]. given #14 (T,wt=6): 17 x ' @ x = e. [para(9(a,1),10(a,1,2,2)),demod(13(6)),flip(a)]. given #15 (T,wt=6): 36 x * x ' = e. [para(29(a,1),9(a,1,1))]. 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): 54 A ' * C ' * A * C * (B @ C) != A * B @ C # answer(D). [para(14(a,2),12(a,1))]. given #18 (F,wt=6): 40 x @ x ' = e. [para(29(a,1),17(a,1,1))]. given #19 (T,wt=7): 23 (x @ y) @ z = e. [para(11(a,1),10(a,1,2,2)),demod(13(6),11(4,R),22(4)),flip(a)]. given #20 (T,wt=7): 24 x @ (y @ z) = e. [para(11(a,2),10(a,1,2,2)),demod(13(6),9(2)),flip(a)]. 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=7): 86 x @ x * x = e. [para(15(a,1),15(a,1,2)),demod(9(2),26(2),84(3),8(4),9(4),16(5))]. given #23 (F,wt=8): 39 x * x ' * y = y. [para(29(a,1),13(a,1,1))]. given #24 (T,wt=10): 41 x * y * (x * y) ' = e. [para(36(a,1),7(a,1)),flip(a)]. given #25 (T,wt=9): 100 x * (y * x) ' = y '. [para(41(a,1),13(a,1,2)),demod(25(3)),flip(a)]. given #26 (A,wt=15): 19 (x @ y) * z * u = z * (x @ y) * u. [para(11(a,1),7(a,1,1)),demod(7(3)),flip(a)]. given #27 (F,wt=8): 114 (x @ y) ' = y @ x. [para(14(a,2),100(a,1,2,1)),demod(113(7),113(5),113(3),113(2),7(5),29(7),7(6),7(5),29(8),7(7),7(6),7(5),10(6),39(4)),flip(a)]. given #28 (F,wt=9): 119 (x @ y) * (y @ x) = e. [back_demod(98),demod(113(4),114(3),92(5))]. given #29 (T,wt=9): 126 x @ y * x = x @ y. [back_demod(89),demod(113(2),7(5),10(5)),flip(a)]. given #30 (T,wt=9): 152 x * y @ x = y @ x. [back_demod(84),demod(126(4))]. given #31 (A,wt=15): 20 (x @ y) * z * u = z * u * (x @ y). [para(11(a,2),7(a,1))]. given #32 (F,wt=19): 201 A ' * C ' * (B @ C) * A * C != A * B @ C # answer(D). [para(20(a,2),54(a,1,2,2))]. given #33 (F,wt=25): 210 A ' * C ' * B ' * C ' * B * C * A * C != A * B @ C # answer(D). [para(14(a,2),201(a,1,2,2))]. given #34 (T,wt=8): 184 x @ y ' = y @ x. [para(13(a,1),152(a,1,1)),demod(182(5))]. given #35 (T,wt=8): 186 x ' @ y = y @ x. [para(39(a,1),152(a,1,1)),demod(181(4)),flip(a)]. given #36 (A,wt=15): 21 x * (y @ z) * u = x * u * (y @ z). [para(11(a,1),7(a,2,2)),demod(7(3))]. given #37 (F,wt=14): 213 (B @ C) * (C @ A ') != A * B @ C # answer(D). [para(184(a,2),12(a,1,1)),demod(11(8,R))]. given #38 (F,wt=14): 214 (A @ C) * (C @ B ') != A * B @ C # answer(D). [para(184(a,2),12(a,1,2))]. given #39 (T,wt=9): 180 x * y @ y = x @ y. [para(126(a,1),114(a,1,1)),demod(114(2)),flip(a)]. given #40 (T,wt=9): 188 x @ x * y = x @ y. [para(152(a,1),114(a,1,1)),demod(114(2)),flip(a)]. given #41 (A,wt=12): 32 x ' * y * x = y * (y @ x). [para(10(a,1),13(a,1,2)),demod(29(2)),flip(a)]. given #42 (F,wt=14): 235 C ' @ A * B != (A @ C) * (B @ C) # answer(D). [para(186(a,2),12(a,2)),flip(a)]. given #43 (F,wt=15): 215 C @ B ' * A ' != (A @ C) * (B @ C) # answer(D). [para(184(a,2),12(a,2)),demod(113(12)),flip(a)]. given #44 (T,wt=9): 229 x ' @ y ' = x @ y. [para(184(a,2),184(a,1))]. given #45 (T,wt=9): 245 x ' @ y = x @ y '. [para(186(a,1),184(a,1))]. given #46 (A,wt=12): 34 x ' * (y @ z) * x = y @ z. [para(11(a,2),13(a,1,2))]. given #47 (F,wt=15): 273 (C @ A ') * (C @ B ') != A * B @ C # answer(D). [para(184(a,2),213(a,1,1)),demod(11(9,R))]. given #48 (F,wt=15): 275 C ' @ A * B != (B @ C) * (C @ A ') # answer(D). [para(186(a,2),213(a,2)),flip(a)]. given #49 (T,wt=10): 113 (x * y) ' = y ' * x '. [para(100(a,1),13(a,1,2)),flip(a)]. given #50 (T,wt=10): 150 x * y @ y ' = y @ x. [back_demod(88),demod(126(5))]. given #51 (A,wt=14): 37 x * y ' * x ' * y = x ' @ y. [para(29(a,1),10(a,1,1))]. given #52 (F,wt=15): 277 C ' @ A * B != (A @ C) * (C @ B ') # answer(D). [para(186(a,2),214(a,2)),flip(a)]. given #53 (F,wt=16): 274 C @ B ' * A ' != (B @ C) * (C @ A ') # answer(D). [para(184(a,2),213(a,2)),demod(113(13)),flip(a)]. given #54 (T,wt=10): 182 x * y @ x ' = x @ y. [back_demod(173),demod(180(5))]. given #55 (T,wt=10): 222 (x @ y) * (x ' @ y) = e. [para(184(a,1),119(a,1,1))]. given #56 (A,wt=14): 38 x ' * y * x * y ' = x @ y '. [para(29(a,1),10(a,1,2,1))]. given #57 (F,wt=16): 276 C @ B ' * A ' != (A @ C) * (C @ B ') # answer(D). [para(184(a,2),214(a,2)),demod(113(13)),flip(a)]. given #58 (F,wt=16): 312 B ' * A ' @ C ' != (A @ C) * (B @ C) # answer(D). [para(186(a,2),235(a,1)),demod(113(4))]. given #59 (T,wt=10): 223 (x @ y) * (x @ y ') = e. [para(184(a,2),119(a,1,1)),demod(11(4,R))]. given #60 (T,wt=10): 284 x ' @ y * x = y @ x. [para(180(a,1),186(a,2))]. given #61 (A,wt=21): 42 x * y ' * z ' * y * z * u = x * (y @ z) * u. [para(14(a,1),7(a,2,2)),demod(7(7))]. given #62 (F,wt=16): 334 C ' @ A * B != (C @ A ') * (C @ B ') # answer(D). [para(186(a,2),273(a,2)),flip(a)]. given #63 (F,wt=17): 333 C @ B ' * A ' != (C @ A ') * (C @ B ') # answer(D). [para(184(a,2),273(a,2)),demod(113(14)),flip(a)]. given #64 (T,wt=10): 301 x ' * y * x @ y = e. [para(32(a,2),152(a,1,1)),demod(23(6))]. given #65 (T,wt=10): 310 x @ y ' * x * y = e. [para(32(a,2),188(a,1,2)),demod(24(6))]. given #66 (A,wt=13): 45 x ' * y * x = y * (x @ y '). [para(9(a,1),14(a,1,2,2,2)),demod(29(3),25(3),11(6))]. given #67 (F,wt=17): 336 B ' * A ' @ C ' != (B @ C) * (C @ A ') # answer(D). [para(186(a,2),275(a,1)),demod(113(4))]. given #68 (F,wt=17): 372 B ' * A ' @ C ' != (A @ C) * (C @ B ') # answer(D). [para(186(a,2),277(a,1)),demod(113(4))]. given #69 (T,wt=10): 449 x * y * x ' @ y = e. [para(29(a,1),301(a,1,1,1))]. given #70 (T,wt=10): 463 x @ y * x * y ' = e. [para(29(a,1),310(a,1,2,1))]. given #71 (A,wt=22): 48 x ' * y * x * (y @ z) = (x @ y ') * z ' * y * z. [para(10(a,1),14(a,1,2,2,2)),demod(29(3))]. given #72 (F,wt=18): 445 B ' * A ' @ C ' != (C @ A ') * (C @ B ') # answer(D). [para(186(a,2),334(a,1)),demod(113(4))]. given #73 (F,wt=20): 218 A ' * C ' * A * C * (C @ B ') != A * B @ C # answer(D). [para(184(a,2),54(a,1,2,2,2,2))]. given #74 (T,wt=11): 105 x ' * y ' @ x * y = e. [back_demod(71),demod(101(8),9(8)),flip(a)]. given #75 (T,wt=9): 565 x * y @ y * x = e. [para(105(a,1),184(a,2)),demod(113(5),29(3),29(3))]. given #76 (A,wt=17): 51 x ' * y ' * x * y * z = z * (x @ y). [para(14(a,2),11(a,1))]. given #77 (F,wt=19): 596 B ' * C ' * B * C * (A @ C) != A * B @ C # answer(D). [para(51(a,2),12(a,1))]. given #78 (F,wt=19): 617 C ' * A * C * (B @ C) * A ' != A * B @ C # answer(D). [para(51(a,2),213(a,1)),demod(29(5),11(10,R))]. given #79 (T,wt=11): 138 x ' @ x * y = x ' @ y. [back_demod(30),demod(113(2),7(4),37(5)),flip(a)]. given #80 (T,wt=11): 149 (x @ y) * z * (y @ x) = z. [back_demod(33),demod(114(2))]. given #81 (A,wt=21): 53 x ' * y ' * x * (z @ u) * y = (x @ y) * (z @ u). [para(11(a,2),14(a,1,2,2,2))]. given #82 (F,wt=19): 618 C ' * B * C * (A @ C) * B ' != A * B @ C # answer(D). [para(51(a,2),214(a,1)),demod(29(5),11(10,R))]. given #83 (F,wt=19): 655 C ' * A * (B @ C) * C * A ' != A * B @ C # answer(D). [para(19(a,2),617(a,1,2,2))]. given #84 (T,wt=11): 151 x * y ' @ y = y ' @ x. [back_demod(87),demod(126(7))]. given #85 (T,wt=11): 160 (x @ y) * (y @ x) * z = z. [para(19(a,2),13(a,1)),demod(114(3))]. given #86 (A,wt=16): 55 x ' * y * x * z = y * (y @ x) * z. [para(14(a,1),13(a,1,2)),demod(29(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. 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 = 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))]. 16 e @ x = e. [para(8(a,1),10(a,1,2,2)),demod(9(4),9(4)),flip(a)]. 25 x * e = x. [para(16(a,1),11(a,1,1)),demod(8(2),16(2)),flip(a)]. 29 x ' ' = x. [para(9(a,1),13(a,1,2)),demod(25(4))]. 36 x * x ' = e. [para(29(a,1),9(a,1,1))]. 39 x * x ' * y = y. [para(29(a,1),13(a,1,1))]. 41 x * y * (x * y) ' = e. [para(36(a,1),7(a,1)),flip(a)]. 53 x ' * y ' * x * (z @ u) * y = (x @ y) * (z @ u). [para(11(a,2),14(a,1,2,2,2))]. 55 x ' * y * x * z = y * (y @ x) * z. [para(14(a,1),13(a,1,2)),demod(29(2)),flip(a)]. 80 (x * y) ' * y * x = x * y @ x. [para(13(a,1),15(a,1,2))]. 84 x * y @ x = y @ x * y. [para(14(a,1),15(a,1,2)),demod(13(3),11(4),13(5),13(5))]. 89 (x * y) ' * y * x = y @ x * y. [back_demod(80),demod(84(6))]. 100 x * (y * x) ' = y '. [para(41(a,1),13(a,1,2)),demod(25(3)),flip(a)]. 113 (x * y) ' = y ' * x '. [para(100(a,1),13(a,1,2)),flip(a)]. 114 (x @ y) ' = y @ x. [para(14(a,2),100(a,1,2,1)),demod(113(7),113(5),113(3),113(2),7(5),29(7),7(6),7(5),29(8),7(7),7(6),7(5),10(6),39(4)),flip(a)]. 126 x @ y * x = x @ y. [back_demod(89),demod(113(2),7(5),10(5)),flip(a)]. 152 x * y @ x = y @ x. [back_demod(84),demod(126(4))]. 173 x * y @ x ' = x * y @ y. [para(13(a,1),126(a,1,2)),flip(a)]. 180 x * y @ y = x @ y. [para(126(a,1),114(a,1,1)),demod(114(2)),flip(a)]. 182 x * y @ x ' = x @ y. [back_demod(173),demod(180(5))]. 184 x @ y ' = y @ x. [para(13(a,1),152(a,1,1)),demod(182(5))]. 213 (B @ C) * (C @ A ') != A * B @ C # answer(D). [para(184(a,2),12(a,1,1)),demod(11(8,R))]. 273 (C @ A ') * (C @ B ') != A * B @ C # answer(D). [para(184(a,2),213(a,1,1)),demod(11(9,R))]. 333 C @ B ' * A ' != (C @ A ') * (C @ B ') # answer(D). [para(184(a,2),273(a,2)),demod(113(14)),flip(a)]. 337 x ' * y ' * z ' * x * z * y = x @ z * y. [para(113(a,1),10(a,1,2,1)),demod(7(7))]. 786 x @ y * z = (x @ z) * (x @ y). [para(55(a,2),53(a,1,2,2)),demod(337(8))]. 787 $F # answer(D). [resolve(786,a,333,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=86. Generated=4693. Kept=780. proofs=1. Usable=78. Sos=466. Demods=269. Denials=0. 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=60763. 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.62. User_CPU=0.10, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13132 exit (max_proofs) Mon Jun 19 16:41:41 2006