============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 5109 was started by mccune on cleo, Tue Nov 3 09:42:13 2009 The command was "/home/mccune/LADR/bin/prover9 -f cs.in NA.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file cs.in assign(max_seconds,30). op(450,infix,@). op(400,infix_right,*). assign(new_constants,1). assign(max_weight,25). formulas(sos). x * y != x * z | y = z. y * x != z * x | y = z. (x * y) * z = x * y * z. y * x * (x @ y) = x * y. end_of_list. % Reading from file NA.in formulas(sos). (x @ y) * z = z * (x @ y). end_of_list. formulas(sos). (A @ B) @ C != D @ (F @ G) # answer(A). 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 != x * z | y = z. [assumption]. x * y != z * y | x = z. [assumption]. (x * y) * z = x * y * z. [assumption]. x * y * (y @ x) = y * x. [assumption]. (x @ y) * z = z * (x @ y). [assumption]. (A @ B) @ C != D @ (F @ G) # answer(A). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ A, B, C, D, F, G, *, @ ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(hyper_resolution). % (nonunit Horn with equality) % set(hyper_resolution) -> set(pos_hyper_resolution). % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 2). % (nonunit Horn with equality) Auto_process settings: (no changes). kept: 1 x * y != x * z | y = z. [assumption]. kept: 2 x * y != z * y | x = z. [assumption]. kept: 3 (x * y) * z = x * y * z. [assumption]. kept: 4 x * y * (y @ x) = y * x. [assumption]. kept: 5 (x @ y) * z = z * (x @ y). [assumption]. kept: 6 (A @ B) @ C != D @ (F @ G) # answer(A). [assumption]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 x * y != x * z | y = z. [assumption]. 2 x * y != z * y | x = z. [assumption]. 3 (x * y) * z = x * y * z. [assumption]. 4 x * y * (y @ x) = y * x. [assumption]. 5 (x @ y) * z = z * (x @ y). [assumption]. 6 (A @ B) @ C != D @ (F @ G) # answer(A). [assumption]. end_of_list. formulas(demodulators). 3 (x * y) * z = x * y * z. [assumption]. 4 x * y * (y @ x) = y * x. [assumption]. 5 (x @ y) * z = z * (x @ y). [assumption]. % (lex-dep) end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=10): 1 x * y != x * z | y = z. [assumption]. given #2 (I,wt=10): 2 x * y != z * y | x = z. [assumption]. given #3 (I,wt=11): 3 (x * y) * z = x * y * z. [assumption]. given #4 (I,wt=11): 4 x * y * (y @ x) = y * x. [assumption]. given #5 (I,wt=11): 5 (x @ y) * z = z * (x @ y). [assumption]. given #6 (I,wt=11): 6 (A @ B) @ C != D @ (F @ G) # answer(A). [assumption]. given #7 (A,wt=14): 7 x * y * z != x * y * u | z = u. [para(3(a,1),1(a,1)),rewrite([3(4)])]. given #8 (F,wt=15): 23 ((A @ B) @ C) * x != (D @ (F @ G)) * x # answer(A). [ur(2,b,6,a)]. given #9 (F,wt=15): 24 x * ((A @ B) @ C) != x * (D @ (F @ G)) # answer(A). [ur(1,b,6,a)]. given #10 (F,wt=15): 38 (D @ (F @ G)) * x != x * ((A @ B) @ C) # answer(A). [para(5(a,1),23(a,1)),flip(a)]. given #11 (F,wt=15): 39 ((A @ B) @ C) * x != x * (D @ (F @ G)) # answer(A). [para(5(a,1),23(a,2))]. given #12 (T,wt=7): 9 x * (x @ x) = x. [hyper(1,a,4,a)]. given #13 (T,wt=10): 50 x * y != x | x @ x = y. [para(9(a,1),1(a,1)),flip(a)]. given #14 (T,wt=10): 51 x * (y @ y) != y | y = x. [para(9(a,1),2(a,1)),flip(a)]. given #15 (T,wt=10): 52 x * (y @ y) != y | x = y. [para(9(a,1),2(a,2))]. given #16 (A,wt=14): 8 x * y * z != u * z | x * y = u. [para(3(a,1),2(a,1))]. given #17 (F,wt=19): 25 x * y * ((A @ B) @ C) != x * y * (D @ (F @ G)) # answer(A). [ur(7,b,6,a)]. given #18 (F,wt=17): 77 C * (A @ B) * (D @ (F @ G)) != C * (A @ B) # answer(A). [para(4(a,1),25(a,1)),rewrite([5(5)]),flip(a)]. given #19 (F,wt=17): 78 (F @ G) * D * ((A @ B) @ C) != D * (F @ G) # answer(A). [para(4(a,1),25(a,2))]. given #20 (F,wt=19): 35 x * ((A @ B) @ C) * y != x * (D @ (F @ G)) * y # answer(A). [ur(1,b,23,a)]. given #21 (T,wt=10): 64 (x @ x) * y != x | x = y. [para(5(a,2),51(a,1))]. given #22 (T,wt=10): 65 (x @ x) * y != x | y = x. [para(5(a,2),52(a,1))]. given #23 (T,wt=11): 53 x * (x @ x) * y = x * y. [para(9(a,1),3(a,1,1)),flip(a)]. given #24 (T,wt=6): 98 x != y | y = x. [para(53(a,1),64(a,1)),rewrite([93(2),93(5)])]. given #25 (A,wt=14): 10 x * y != z * x | z * (z @ x) = y. [para(4(a,1),1(a,1)),flip(a)]. given #26 (F,wt=19): 42 (D @ (F @ G)) * x * y != x * ((A @ B) @ C) * y # answer(A). [ur(2,b,38,a),rewrite([3(7),3(14)])]. given #27 (F,wt=19): 43 x * (D @ (F @ G)) * y != x * y * ((A @ B) @ C) # answer(A). [ur(1,b,38,a)]. given #28 (F,wt=19): 44 (D @ (F @ G)) * x * y != x * y * ((A @ B) @ C) # answer(A). [para(3(a,1),38(a,2))]. given #29 (F,wt=19): 47 ((A @ B) @ C) * x * y != x * (D @ (F @ G)) * y # answer(A). [ur(2,b,39,a),rewrite([3(7),3(14)])]. given #30 (T,wt=7): 93 (x @ x) * y = y. [hyper(7,a,53,a)]. given #31 (T,wt=7): 131 x * (y @ y) = x. [hyper(10,a,93,a),rewrite([100(3)]),flip(a)]. NOTE: New constant: x @ x = c_0. [new_symbol(137)]. NOTE: New Function symbol precedence: function_order([ A, B, C, D, F, G, c_0, *, @ ]). given #32 (T,wt=5): 141 x @ x = c_0. [new_symbol(137)]. given #33 (T,wt=5): 149 x * c_0 = x. [back_rewrite(131),rewrite([141(1)])]. given #34 (A,wt=14): 11 x * y * (y @ z) != y * z | z = x. [para(4(a,1),2(a,1)),flip(a)]. given #35 (F,wt=19): 48 x * ((A @ B) @ C) * y != x * y * (D @ (F @ G)) # answer(A). [ur(1,b,39,a)]. given #36 (F,wt=19): 49 ((A @ B) @ C) * x * y != x * y * (D @ (F @ G)) # answer(A). [para(3(a,1),39(a,2))]. given #37 (F,wt=17): 161 D * (F @ G) * ((A @ B) @ C) != D * (F @ G) # answer(A). [para(4(a,1),49(a,2)),rewrite([5(10),5(11),3(11)])]. given #38 (F,wt=21): 81 C * (A @ B) * (D @ (F @ G)) * x != C * (A @ B) * x # answer(A). [ur(8,b,77,a),rewrite([3(11),3(18)])]. given #39 (T,wt=5): 150 c_0 * x = x. [back_rewrite(93),rewrite([141(1)])]. given #40 (T,wt=7): 147 x * (c_0 @ x) = x. [back_rewrite(133),rewrite([141(1)])]. given #41 (T,wt=7): 152 x * (x @ c_0) = x. [hyper(10,a,149,a(flip)),rewrite([150(2),150(2)])]. given #42 (T,wt=8): 144 x * y != x | c_0 = y. [back_rewrite(138),rewrite([141(3)])]. given #43 (A,wt=14): 12 x * y * (y @ z) != y * z | x = z. [para(4(a,1),2(a,2))]. given #44 (F,wt=21): 83 x * C * (A @ B) * (D @ (F @ G)) != x * C * (A @ B) # answer(A). [ur(1,b,77,a)]. given #45 (F,wt=21): 84 (F @ G) * D * ((A @ B) @ C) * x != D * (F @ G) * x # answer(A). [ur(8,b,78,a),rewrite([3(11),3(18)])]. given #46 (F,wt=21): 86 x * (F @ G) * D * ((A @ B) @ C) != x * D * (F @ G) # answer(A). [ur(1,b,78,a)]. given #47 (F,wt=21): 163 D * (F @ G) * ((A @ B) @ C) * x != D * (F @ G) * x # answer(A). [ur(8,b,161,a),rewrite([3(11),3(18)])]. given #48 (T,wt=5): 212 x @ c_0 = c_0. [hyper(144,a,152,a),flip(a)]. given #49 (T,wt=5): 213 c_0 @ x = c_0. [hyper(144,a,147,a),flip(a)]. given #50 (T,wt=8): 148 x * y != y | c_0 = x. [back_rewrite(132),rewrite([141(3)])]. given #51 (T,wt=9): 100 x * (x @ (y @ z)) = x. [hyper(10,a,5,a)]. ============================== PROOF ================================= % Proof 1 at 0.04 (+ 0.00) seconds: A. % Length of proof is 25. % Level of proof is 10. % Maximum clause weight is 19.000. % Given clauses 51. 1 x * y != x * z | y = z. [assumption]. 2 x * y != z * y | x = z. [assumption]. 3 (x * y) * z = x * y * z. [assumption]. 4 x * y * (y @ x) = y * x. [assumption]. 5 (x @ y) * z = z * (x @ y). [assumption]. 6 (A @ B) @ C != D @ (F @ G) # answer(A). [assumption]. 7 x * y * z != x * y * u | z = u. [para(3(a,1),1(a,1)),rewrite([3(4)])]. 9 x * (x @ x) = x. [hyper(1,a,4,a)]. 10 x * y != z * x | z * (z @ x) = y. [para(4(a,1),1(a,1)),flip(a)]. 23 ((A @ B) @ C) * x != (D @ (F @ G)) * x # answer(A). [ur(2,b,6,a)]. 35 x * ((A @ B) @ C) * y != x * (D @ (F @ G)) * y # answer(A). [ur(1,b,23,a)]. 50 x * y != x | x @ x = y. [para(9(a,1),1(a,1)),flip(a)]. 53 x * (x @ x) * y = x * y. [para(9(a,1),3(a,1,1)),flip(a)]. 93 (x @ x) * y = y. [hyper(7,a,53,a)]. 100 x * (x @ (y @ z)) = x. [hyper(10,a,5,a)]. 102 (x @ y) * ((x @ y) @ z) = x @ y. [hyper(10,a,5,a(flip))]. 131 x * (y @ y) = x. [hyper(10,a,93,a),rewrite([100(3)]),flip(a)]. 137 x @ x = y @ y. [hyper(50,a,131,a)]. 138 x * y != x | z @ z = y. [para(131(a,1),1(a,1)),flip(a)]. 141 x @ x = c_0. [new_symbol(137)]. 144 x * y != x | c_0 = y. [back_rewrite(138),rewrite([141(3)])]. 149 x * c_0 = x. [back_rewrite(131),rewrite([141(1)])]. 229 x @ (y @ z) = c_0. [hyper(144,a,100,a),flip(a)]. 233 x * ((A @ B) @ C) != x # answer(A). [para(100(a,1),35(a,1,2)),rewrite([229(11),229(14),149(9),149(8)])]. 234 $F # answer(A). [resolve(233,a,102,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=51. Generated=1227. Kept=233. proofs=1. Usable=40. Sos=105. Demods=16. Limbo=4, Disabled=89. Hints=0. Kept_by_rule=0, Deleted_by_rule=195. Forward_subsumed=799. Back_subsumed=9. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=34 (1 lex), Back_demodulated=74. Back_unit_deleted=0. Demod_attempts=19130. Demod_rewrites=1277. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=1177. Nonunit_bsub_feature_tests=1098. 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 5109 exit (max_proofs) Tue Nov 3 09:42:13 2009