============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13112 was started by mccune on cleo.thornwood, Mon Jun 19 16:41:24 2006 The command was "/home/mccune/bin/prover9 -f cs.in AD.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file cs.in op(450,infix,@). op(400,infix_right,*). assign(new_constants,1). assign(max_weight,25). clauses(sos). x * y != x * z | y = z. x * y != z * y | x = z. (x * y) * z = x * y * z. x * y * (y @ x) = y * x. 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 != x * z | y = z. [input]. 2 x * y != z * y | x = z. [input]. 3 (x * y) * z = x * y * z. [input]. 4 x * y * (y @ x) = y * x. [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([ A, B, C, *, @ ]). After inverse_order: Function symbol precedence: lex([ A, B, C, *, @ ]). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 2). % (nonunit Horn with equality) 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 != x * z | y = z. [input]. 8 x * y != z * y | x = z. [input]. 9 (x * y) * z = x * y * z. [input]. 10 x * y * (y @ x) = y * x. [input]. 11 (x @ y) @ z = u @ (v @ w). [input]. 12 A * B @ C != (A @ C) * (B @ C) # answer(D). [copy(6),flip(a)]. end_of_list. clauses(demodulators). 9 (x * y) * z = x * y * z. [input]. 10 x * y * (y @ x) = y * x. [input]. end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=10): 7 x * y != x * z | y = z. [input]. given #2 (I,wt=10): 8 x * y != z * y | x = z. [input]. given #3 (I,wt=11): 9 (x * y) * z = x * y * z. [input]. given #4 (I,wt=11): 10 x * y * (y @ x) = y * x. [input]. given #5 (I,wt=11): 11 (x @ y) @ z = u @ (v @ w). [input]. given #6 (I,wt=13): 12 A * B @ C != (A @ C) * (B @ C) # answer(D). [copy(6),flip(a)]. given #7 (F,wt=17): 26 (A * B @ C) * x != (A @ C) * (B @ C) * x # answer(D). [ur(8,b,12,a),demod(9(14))]. given #8 (F,wt=17): 27 x * (A * B @ C) != x * (A @ C) * (B @ C) # answer(D). [ur(7,b,12,a)]. given #9 (T,wt=7): 15 x * (x @ x) = x. [hyper(7,a,10,a)]. given #10 (T,wt=10): 33 x * y != x | x @ x = y. [para(15(a,1),7(a,1)),flip(a)]. given #11 (A,wt=14): 13 x * y * z != x * y * u | z = u. [para(9(a,1),7(a,1)),demod(9(4))]. given #12 (F,wt=21): 28 x * (A * B @ C) * y != x * (A @ C) * (B @ C) * y # answer(D). [ur(7,b,26,a)]. given #13 (F,wt=17): 50 (A * B @ C) * x != x * (A @ C) * (B @ C) # answer(D). [para(10(a,1),28(a,1)),demod(39(19))]. given #14 (T,wt=10): 34 x * (y @ y) != y | y = x. [para(15(a,1),8(a,1)),flip(a)]. given #15 (T,wt=10): 35 x * (y @ y) != y | x = y. [para(15(a,1),8(a,2))]. given #16 (A,wt=14): 14 x * y * z != u * z | x * y = u. [para(9(a,1),8(a,1))]. given #17 (F,wt=21): 32 x * y * (A * B @ C) != x * y * (A @ C) * (B @ C) # answer(D). [ur(7,b,27,a)]. given #18 (F,wt=19): 64 C * A * B * (A @ C) * (B @ C) != A * B * C # answer(D). [para(10(a,1),32(a,1)),demod(9(5),9(17)),flip(a)]. given #19 (T,wt=11): 24 x @ (y @ z) = u @ (v @ w). [para(11(a,1),11(a,1))]. given #20 (T,wt=11): 25 (x @ y) @ z = (u @ v) @ w. [para(11(a,2),11(a,2))]. given #21 (A,wt=14): 16 x * y != z * x | z * (z @ x) = y. [para(10(a,1),7(a,1)),flip(a)]. given #22 (F,wt=21): 52 (A * B @ C) * x * y != x * (A @ C) * (B @ C) * y # answer(D). [ur(8,b,50,a),demod(9(7),9(16),9(15))]. given #23 (F,wt=21): 53 x * (A * B @ C) * y != x * y * (A @ C) * (B @ C) # answer(D). [ur(7,b,50,a)]. given #24 (T,wt=9): 68 x * (x @ x * x) = x. [hyper(16,a,9,a)]. given #25 (T,wt=9): 82 x @ x * x = x @ x. [hyper(33,a,68,a),flip(a)]. given #26 (A,wt=14): 17 x * y * (y @ z) != y * z | z = x. [para(10(a,1),8(a,1)),flip(a)]. given #27 (F,wt=21): 54 (A * B @ C) * x * y != x * y * (A @ C) * (B @ C) # answer(D). [para(9(a,1),50(a,2))]. given #28 (F,wt=21): 79 (A * B @ C) * x != x * (A @ C) * (B @ C) * (x @ x) # answer(D). [para(15(a,1),52(a,1,2))]. given #29 (T,wt=10): 89 x * y != y * y | y = x. [para(15(a,1),17(a,1,2))]. given #30 (T,wt=11): 36 x * (x @ x) * y = x * y. [para(15(a,1),9(a,1,1)),flip(a)]. given #31 (A,wt=14): 18 x * y * (y @ z) != y * z | x = z. [para(10(a,1),8(a,2))]. given #32 (F,wt=21): 101 x * (A * B @ C) * (x @ x) != x * (A @ C) * (B @ C) # answer(D). [para(36(a,1),53(a,2))]. given #33 (F,wt=23): 30 (A * B @ C) * x * (x @ (B @ C)) != (A @ C) * x * (B @ C) # answer(D). [para(10(a,1),26(a,2,2))]. given #34 (T,wt=7): 95 (x @ x) * y = y. [hyper(13,a,36,a)]. given #35 (T,wt=6): 127 x != y | y = x. [back_demod(103),demod(112(4),15(3))]. given #36 (A,wt=15): 19 x * y * (y @ x) * z = y * x * z. [para(10(a,1),9(a,1,1)),demod(9(2),9(5)),flip(a)]. given #37 (F,wt=17): 117 (A * B @ C) * (x @ x) != (A @ C) * (B @ C) # answer(D). [para(95(a,1),50(a,2))]. given #38 (F,wt=17): 138 (A * B @ C) * x != (B @ C) * (A @ C) * x # answer(D). [para(19(a,1),26(a,2)),demod(115(13))]. given #39 (T,wt=9): 114 x * ((y @ y) @ x) = x. [para(95(a,1),10(a,1,2)),demod(95(5))]. given #40 (T,wt=7): 177 x * (y @ y) = x. [back_demod(112),demod(165(3)),flip(a)]. NOTE: New constant: 0 x @ x = c_0. [new_symbol(181)]. NOTE: New Function symbol precedence: lex([ A, B, C, c_0, *, @ ]). given #41 (A,wt=17): 20 x * y * z * (z @ x * y) = z * x * y. [para(10(a,1),9(a,1)),flip(a)]. given #42 (F,wt=17): 150 C * A * (A * B @ C) != A * C * (B @ C) # answer(D). [para(19(a,1),32(a,2))]. given #43 (F,wt=17): 174 (A * B @ C) * x != (B @ C) * x * (A @ C) # answer(D). [back_demod(159),demod(165(10))]. given #44 (T,wt=5): 185 x @ x = c_0. [new_symbol(181)]. given #45 (T,wt=5): 189 x * c_0 = x. [back_demod(177),demod(185(1))]. given #46 (A,wt=17): 21 x * y * z * (y * z @ x) = y * z * x. [para(9(a,1),10(a,1,2)),demod(9(7))]. given #47 (F,wt=17): 175 (B @ C) * (A @ C) * x != x * (A * B @ C) # answer(D). [back_demod(158),demod(165(13))]. given #48 (F,wt=17): 178 (A * B @ C) * x != (A @ C) * x * (B @ C) # answer(D). [back_demod(110),demod(165(8))]. given #49 (T,wt=5): 193 c_0 @ x = c_0. [back_demod(162),demod(185(1),185(3))]. given #50 (T,wt=5): 198 c_0 * x = x. [back_demod(95),demod(185(1))]. given #51 (A,wt=11): 41 (x @ y) * z = z * (x @ y). [back_demod(22),demod(38(6))]. given #52 (F,wt=17): 180 (A @ C) * (B @ C) * x != x * (A * B @ C) # answer(D). [back_demod(29),demod(165(13))]. ============================== PROOF ================================= % Proof 1 at 0.04 (+ 0.00) seconds: D. % Length of proof is 24. % Level of proof is 7. % Maximum clause weight is 25. % Given clauses 52. 6 (A @ C) * (B @ C) != A * B @ C # answer(D). [input]. 7 x * y != x * z | y = z. [input]. 8 x * y != z * y | x = z. [input]. 9 (x * y) * z = x * y * z. [input]. 10 x * y * (y @ x) = y * x. [input]. 11 (x @ y) @ z = u @ (v @ w). [input]. 12 A * B @ C != (A @ C) * (B @ C) # answer(D). [copy(6),flip(a)]. 13 x * y * z != x * y * u | z = u. [para(9(a,1),7(a,1)),demod(9(4))]. 15 x * (x @ x) = x. [hyper(7,a,10,a)]. 16 x * y != z * x | z * (z @ x) = y. [para(10(a,1),7(a,1)),flip(a)]. 19 x * y * (y @ x) * z = y * x * z. [para(10(a,1),9(a,1,1)),demod(9(2),9(5)),flip(a)]. 22 (x @ y) * z = z * (x @ y) * (u @ (v @ w)). [para(11(a,1),10(a,1,2,2)),flip(a)]. 26 (A * B @ C) * x != (A @ C) * (B @ C) * x # answer(D). [ur(8,b,12,a),demod(9(14))]. 29 (A @ C) * (B @ C) * x * (x @ (A * B @ C)) != x * (A * B @ C) # answer(D). [para(10(a,1),26(a,1)),flip(a)]. 36 x * (x @ x) * y = x * y. [para(15(a,1),9(a,1,1)),flip(a)]. 38 (x @ y) * (z @ (u @ v)) = x @ y. [para(11(a,1),15(a,1,2))]. 41 (x @ y) * z = z * (x @ y). [back_demod(22),demod(38(6))]. 95 (x @ x) * y = y. [hyper(13,a,36,a)]. 114 x * ((y @ y) @ x) = x. [para(95(a,1),10(a,1,2)),demod(95(5))]. 116 ((x @ y) @ z) * u = u. [para(11(a,2),95(a,1,1))]. 155 x * (y @ x) * y * z = y * x * z. [para(19(a,1),19(a,1,2)),demod(116(7))]. 165 x * (y @ (z @ u)) = x. [para(11(a,1),114(a,1,2))]. 180 (A @ C) * (B @ C) * x != x * (A * B @ C) # answer(D). [back_demod(29),demod(165(13))]. 285 $F # answer(D). [ur(16,b,180,a(flip)),demod(41(11),9(11),155(13),10(8),9(10)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=52. Generated=1603. Kept=278. proofs=1. Usable=35. Sos=147. Demods=31. Denials=0. Limbo=1, Disabled=101. Hints=0. Weight_deleted=251. Literals_deleted=0. Forward_subsumed=1073. Back_subsumed=18. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=61 (1 lex), Back_demodulated=77. Back_unit_deleted=0. Demod_attempts=25093. Demod_rewrites=2013. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=1999. Nonunit_bsub_feature_tests=878. Megabytes=0.26. User_CPU=0.04, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13112 exit (max_proofs) Mon Jun 19 16:41:24 2006