============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 3852 was started by mccune on cleo.thornwood, Wed Nov 22 11:24:06 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). 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 AD.in formulas(sos). (x @ y) @ z = u @ (v @ w). 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 != 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 = u @ (v @ w). [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([ A, B, C, *, @ ]). After inverse_order: (no changes). 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: 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 = u @ (v @ w). [assumption]. 7 A * B @ C != (A @ C) * (B @ C) # answer(D). [copy(6),flip(a)]. end_of_list. formulas(demodulators). 3 (x * y) * z = x * y * z. [assumption]. 4 x * y * (y @ x) = y * x. [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 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 = u @ (v @ w). [assumption]. given #6 (I,wt=13): 7 A * B @ C != (A @ C) * (B @ C) # answer(D). [copy(6),flip(a)]. given #7 (F,wt=17): 21 (A * B @ C) * x != (A @ C) * (B @ C) * x # answer(D). [ur(2,b,7,a),rewrite(3(14))]. given #8 (F,wt=17): 22 x * (A * B @ C) != x * (A @ C) * (B @ C) # answer(D). [ur(1,b,7,a)]. given #9 (T,wt=7): 10 x * (x @ x) = x. [hyper(1,a,4,a)]. given #10 (T,wt=10): 28 x * y != x | x @ x = y. [para(10(a,1),1(a,1)),flip(a)]. given #11 (A,wt=14): 8 x * y * z != x * y * u | z = u. [para(3(a,1),1(a,1)),rewrite(3(4))]. given #12 (F,wt=21): 23 x * (A * B @ C) * y != x * (A @ C) * (B @ C) * y # answer(D). [ur(1,b,21,a)]. given #13 (F,wt=17): 45 (A * B @ C) * x != x * (A @ C) * (B @ C) # answer(D). [para(4(a,1),23(a,1)),rewrite(34(19))]. given #14 (T,wt=10): 29 x * (y @ y) != y | y = x. [para(10(a,1),2(a,1)),flip(a)]. given #15 (T,wt=10): 30 x * (y @ y) != y | x = y. [para(10(a,1),2(a,2))]. given #16 (A,wt=14): 9 x * y * z != u * z | x * y = u. [para(3(a,1),2(a,1))]. given #17 (F,wt=21): 27 x * y * (A * B @ C) != x * y * (A @ C) * (B @ C) # answer(D). [ur(1,b,22,a)]. given #18 (F,wt=19): 59 C * A * B * (A @ C) * (B @ C) != A * B * C # answer(D). [para(4(a,1),27(a,1)),rewrite(3(5),3(17)),flip(a)]. given #19 (T,wt=11): 19 x @ (y @ z) = u @ (v @ w). [para(5(a,1),5(a,1))]. given #20 (T,wt=11): 20 (x @ y) @ z = (u @ v) @ w. [para(5(a,2),5(a,2))]. given #21 (A,wt=14): 11 x * y != z * x | z * (z @ x) = y. [para(4(a,1),1(a,1)),flip(a)]. given #22 (F,wt=21): 47 (A * B @ C) * x * y != x * (A @ C) * (B @ C) * y # answer(D). [ur(2,b,45,a),rewrite(3(7),3(16),3(15))]. given #23 (F,wt=21): 48 x * (A * B @ C) * y != x * y * (A @ C) * (B @ C) # answer(D). [ur(1,b,45,a)]. given #24 (T,wt=9): 63 x * (x @ x * x) = x. [hyper(11,a,3,a)]. given #25 (T,wt=9): 77 x @ x * x = x @ x. [hyper(28,a,63,a),flip(a)]. given #26 (A,wt=14): 12 x * y * (y @ z) != y * z | z = x. [para(4(a,1),2(a,1)),flip(a)]. given #27 (F,wt=21): 49 (A * B @ C) * x * y != x * y * (A @ C) * (B @ C) # answer(D). [para(3(a,1),45(a,2))]. given #28 (F,wt=21): 74 (A * B @ C) * x != x * (A @ C) * (B @ C) * (x @ x) # answer(D). [para(10(a,1),47(a,1,2))]. given #29 (T,wt=10): 84 x * y != y * y | y = x. [para(10(a,1),12(a,1,2))]. given #30 (T,wt=11): 31 x * (x @ x) * y = x * y. [para(10(a,1),3(a,1,1)),flip(a)]. given #31 (A,wt=14): 13 x * y * (y @ z) != y * z | x = z. [para(4(a,1),2(a,2))]. given #32 (F,wt=21): 96 x * (A * B @ C) * (x @ x) != x * (A @ C) * (B @ C) # answer(D). [para(31(a,1),48(a,2))]. given #33 (F,wt=23): 25 (A * B @ C) * x * (x @ (B @ C)) != (A @ C) * x * (B @ C) # answer(D). [para(4(a,1),21(a,2,2))]. given #34 (T,wt=7): 90 (x @ x) * y = y. [hyper(8,a,31,a)]. given #35 (T,wt=6): 122 x != y | y = x. [back_rewrite(98),rewrite(107(4),10(3))]. given #36 (A,wt=15): 14 x * y * (y @ x) * z = y * x * z. [para(4(a,1),3(a,1,1)),rewrite(3(2),3(5)),flip(a)]. given #37 (F,wt=17): 112 (A * B @ C) * (x @ x) != (A @ C) * (B @ C) # answer(D). [para(90(a,1),45(a,2))]. given #38 (F,wt=17): 133 (A * B @ C) * x != (B @ C) * (A @ C) * x # answer(D). [para(14(a,1),21(a,2)),rewrite(110(13))]. given #39 (T,wt=9): 109 x * ((y @ y) @ x) = x. [para(90(a,1),4(a,1,2)),rewrite(90(5))]. given #40 (T,wt=7): 172 x * (y @ y) = x. [back_rewrite(107),rewrite(160(3)),flip(a)]. NOTE: New constant: x @ x = c_0. [new_symbol(176)]. NOTE: New Function symbol precedence: lex([ A, B, C, c_0, *, @ ]). given #41 (A,wt=17): 15 x * y * z * (z @ x * y) = z * x * y. [para(4(a,1),3(a,1)),flip(a)]. given #42 (F,wt=17): 145 C * A * (A * B @ C) != A * C * (B @ C) # answer(D). [para(14(a,1),27(a,2))]. given #43 (F,wt=17): 169 (A * B @ C) * x != (B @ C) * x * (A @ C) # answer(D). [back_rewrite(154),rewrite(160(10))]. given #44 (T,wt=5): 180 x @ x = c_0. [new_symbol(176)]. given #45 (T,wt=5): 184 x * c_0 = x. [back_rewrite(172),rewrite(180(1))]. given #46 (A,wt=17): 16 x * y * z * (y * z @ x) = y * z * x. [para(3(a,1),4(a,1,2)),rewrite(3(7))]. given #47 (F,wt=17): 170 (B @ C) * (A @ C) * x != x * (A * B @ C) # answer(D). [back_rewrite(153),rewrite(160(13))]. given #48 (F,wt=17): 173 (A * B @ C) * x != (A @ C) * x * (B @ C) # answer(D). [back_rewrite(105),rewrite(160(8))]. given #49 (T,wt=5): 188 c_0 @ x = c_0. [back_rewrite(157),rewrite(180(1),180(3))]. given #50 (T,wt=5): 193 c_0 * x = x. [back_rewrite(90),rewrite(180(1))]. given #51 (A,wt=11): 36 (x @ y) * z = z * (x @ y). [back_rewrite(17),rewrite(33(6))]. given #52 (F,wt=17): 175 (A @ C) * (B @ C) * x != x * (A * B @ C) # answer(D). [back_rewrite(24),rewrite(160(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. 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 = u @ (v @ w). [assumption]. 6 (A @ C) * (B @ C) != A * B @ C # answer(D). [assumption]. 7 A * B @ C != (A @ C) * (B @ C) # answer(D). [copy(6),flip(a)]. 8 x * y * z != x * y * u | z = u. [para(3(a,1),1(a,1)),rewrite(3(4))]. 10 x * (x @ x) = x. [hyper(1,a,4,a)]. 11 x * y != z * x | z * (z @ x) = y. [para(4(a,1),1(a,1)),flip(a)]. 14 x * y * (y @ x) * z = y * x * z. [para(4(a,1),3(a,1,1)),rewrite(3(2),3(5)),flip(a)]. 17 (x @ y) * z = z * (x @ y) * (u @ (v @ w)). [para(5(a,1),4(a,1,2,2)),flip(a)]. 21 (A * B @ C) * x != (A @ C) * (B @ C) * x # answer(D). [ur(2,b,7,a),rewrite(3(14))]. 24 (A @ C) * (B @ C) * x * (x @ (A * B @ C)) != x * (A * B @ C) # answer(D). [para(4(a,1),21(a,1)),flip(a)]. 31 x * (x @ x) * y = x * y. [para(10(a,1),3(a,1,1)),flip(a)]. 33 (x @ y) * (z @ (u @ v)) = x @ y. [para(5(a,1),10(a,1,2))]. 36 (x @ y) * z = z * (x @ y). [back_rewrite(17),rewrite(33(6))]. 90 (x @ x) * y = y. [hyper(8,a,31,a)]. 109 x * ((y @ y) @ x) = x. [para(90(a,1),4(a,1,2)),rewrite(90(5))]. 111 ((x @ y) @ z) * u = u. [para(5(a,2),90(a,1,1))]. 150 x * (y @ x) * y * z = y * x * z. [para(14(a,1),14(a,1,2)),rewrite(111(7))]. 160 x * (y @ (z @ u)) = x. [para(5(a,1),109(a,1,2))]. 175 (A @ C) * (B @ C) * x != x * (A * B @ C) # answer(D). [back_rewrite(24),rewrite(160(13))]. 280 $F # answer(D). [ur(11,b,175,a(flip)),rewrite(36(11),3(11),150(13),4(8),3(10)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=52. Generated=1603. Kept=278. proofs=1. Usable=35. Sos=147. Demods=31. 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=25116. 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.28. User_CPU=0.04, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3852 exit (max_proofs) Wed Nov 22 11:24:06 2006