============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 5115 was started by mccune on cleo, Tue Nov 3 09:42:18 2009 The command was "/home/mccune/LADR/bin/prover9 -f quot-comm.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file quot-comm.in assign(max_seconds,30). op(400,infix_right,*). set(restrict_denials). assign(max_weight,35). formulas(sos). (x * y) * z = x * y * z # label(associativity). x * y != u | x * z != u | y = z # label(left_cancellation_extended). y * x != u | z * x != u | y = z # label(right_cancellation_extended). x * y = y * x # label(commutativity). b * b0 = a * a0. d * b0 = c * a0. b * d0 = a * c0. d * d0 != c * c0. 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 # label(associativity). [assumption]. x * y != z | x * u != z | y = u # label(left_cancellation_extended). [assumption]. x * y != z | u * y != z | x = u # label(right_cancellation_extended). [assumption]. x * y = y * x # label(commutativity). [assumption]. b * b0 = a * a0. [assumption]. d * b0 = c * a0. [assumption]. b * d0 = a * c0. [assumption]. d * d0 != c * c0. [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, a0, b, b0, c, c0, d, d0, * ]). 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, 3). % (nonunit Horn with equality) Auto_process settings: (no changes). kept: 1 (x * y) * z = x * y * z # label(associativity). [assumption]. kept: 2 x * y != z | x * u != z | y = u # label(left_cancellation_extended). [assumption]. kept: 3 x * y != z | u * y != z | x = u # label(right_cancellation_extended). [assumption]. % Operation * is commutative; C redundancy checks enabled. kept: 4 x * y = y * x # label(commutativity). [assumption]. kept: 5 b * b0 = a * a0. [assumption]. 6 d * b0 = c * a0. [assumption]. kept: 7 b0 * d = a0 * c. [copy(6),rewrite([4(3),4(6)])]. kept: 8 b * d0 = a * c0. [assumption]. kept: 9 d * d0 != c * c0. [assumption]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 9 d * d0 != c * c0. [assumption]. end_of_list. formulas(sos). 1 (x * y) * z = x * y * z # label(associativity). [assumption]. 2 x * y != z | x * u != z | y = u # label(left_cancellation_extended). [assumption]. 3 x * y != z | u * y != z | x = u # label(right_cancellation_extended). [assumption]. 4 x * y = y * x # label(commutativity). [assumption]. 5 b * b0 = a * a0. [assumption]. 7 b0 * d = a0 * c. [copy(6),rewrite([4(3),4(6)])]. 8 b * d0 = a * c0. [assumption]. end_of_list. formulas(demodulators). 1 (x * y) * z = x * y * z # label(associativity). [assumption]. 4 x * y = y * x # label(commutativity). [assumption]. % (lex-dep) 5 b * b0 = a * a0. [assumption]. 7 b0 * d = a0 * c. [copy(6),rewrite([4(3),4(6)])]. 8 b * d0 = a * c0. [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=11): 1 (x * y) * z = x * y * z # label(associativity). [assumption]. given #2 (I,wt=13): 2 x * y != z | x * u != z | y = u # label(left_cancellation_extended). [assumption]. given #3 (I,wt=13): 3 x * y != z | u * y != z | x = u # label(right_cancellation_extended). [assumption]. given #4 (I,wt=7): 4 x * y = y * x # label(commutativity). [assumption]. % Operation * is associative-commutative; CAC redundancy checks enabled. given #5 (I,wt=7): 5 b * b0 = a * a0. [assumption]. given #6 (I,wt=7): 7 b0 * d = a0 * c. [copy(6),rewrite([4(3),4(6)])]. given #7 (I,wt=7): 8 b * d0 = a * c0. [assumption]. given #8 (A,wt=17): 10 x * y * z != u | x * y * w != u | z = w. [para(1(a,1),2(a,1)),rewrite([1(5)])]. given #9 (T,wt=11): 12 x * y * z = y * x * z. [para(4(a,1),1(a,1,1)),rewrite([1(2)])]. given #10 (T,wt=11): 15 b * b0 * x = a * a0 * x. [para(5(a,1),1(a,1,1)),rewrite([1(4)]),flip(a)]. given #11 (T,wt=11): 16 b0 * x * b = x * a * a0. [para(5(a,1),1(a,2,2)),rewrite([4(4)])]. given #12 (T,wt=11): 19 b0 * d * x = a0 * c * x. [para(7(a,1),1(a,1,1)),rewrite([1(4)]),flip(a)]. given #13 (A,wt=17): 11 x * y * z != u | w * z != u | x * y = w. [para(1(a,1),3(a,1))]. given #14 (T,wt=11): 20 d * x * b0 = x * a0 * c. [para(7(a,1),1(a,2,2)),rewrite([4(4)])]. given #15 (T,wt=11): 23 b * d0 * x = a * c0 * x. [para(8(a,1),1(a,1,1)),rewrite([1(4)]),flip(a)]. given #16 (T,wt=11): 24 d0 * x * b = x * a * c0. [para(8(a,1),1(a,2,2)),rewrite([4(4)])]. given #17 (T,wt=11): 39 b0 * x * d = x * a0 * c. [para(7(a,1),12(a,1,2)),flip(a)]. given #18 (A,wt=13): 13 x * y != z | y * u != z | x = u. [para(4(a,1),2(a,1))]. given #19 (T,wt=11): 40 b * x * d0 = x * a * c0. [para(8(a,1),12(a,1,2)),flip(a)]. given #20 (T,wt=11): 46 b * x * b0 = a * a0 * x. [para(4(a,1),15(a,1,2))]. given #21 (T,wt=7): 188 b0 * c0 = a0 * d0. [hyper(2,a,23,a(flip),b,46,a(flip)),rewrite([4(3)])]. given #22 (T,wt=11): 47 a0 * b * c = a * a0 * d. [para(7(a,1),15(a,1,2)),rewrite([12(5)])]. given #23 (A,wt=13): 14 x * y != z | u * x != z | y = u. [para(4(a,1),2(b,1))]. given #24 (T,wt=7): 209 b * c = a * d. [hyper(2,a,12,a,b,47,a),flip(a)]. given #25 (T,wt=11): 52 b0 * x * b = a0 * x * a. [para(16(a,2),1(a,2)),rewrite([4(4)]),flip(a)]. given #26 (T,wt=11): 90 d * x * b0 = c * x * a0. [para(20(a,2),1(a,2)),rewrite([4(4)]),flip(a)]. given #27 (T,wt=11): 116 d0 * x * b = c0 * x * a. [para(24(a,2),1(a,2)),rewrite([4(4)]),flip(a)]. given #28 (A,wt=13): 17 a * a0 != x | b * y != x | b0 = y. [para(5(a,1),2(a,1))]. given #29 (T,wt=11): 148 b0 * x * d = a0 * x * c. [para(39(a,2),12(a,1))]. given #30 (T,wt=11): 181 b * x * d0 = a * x * c0. [para(40(a,2),12(a,1))]. given #31 (T,wt=11): 199 a0 * d0 * x = b0 * c0 * x. [para(188(a,1),1(a,1,1)),rewrite([1(4)])]. ============================== PROOF ================================= % Proof 1 at 0.05 (+ 0.00) seconds. % Length of proof is 18. % Level of proof is 6. % Maximum clause weight is 13.000. % Given clauses 31. 1 (x * y) * z = x * y * z # label(associativity). [assumption]. 2 x * y != z | x * u != z | y = u # label(left_cancellation_extended). [assumption]. 4 x * y = y * x # label(commutativity). [assumption]. 5 b * b0 = a * a0. [assumption]. 6 d * b0 = c * a0. [assumption]. 7 b0 * d = a0 * c. [copy(6),rewrite([4(3),4(6)])]. 8 b * d0 = a * c0. [assumption]. 9 d * d0 != c * c0. [assumption]. 12 x * y * z = y * x * z. [para(4(a,1),1(a,1,1)),rewrite([1(2)])]. 15 b * b0 * x = a * a0 * x. [para(5(a,1),1(a,1,1)),rewrite([1(4)]),flip(a)]. 23 b * d0 * x = a * c0 * x. [para(8(a,1),1(a,1,1)),rewrite([1(4)]),flip(a)]. 39 b0 * x * d = x * a0 * c. [para(7(a,1),12(a,1,2)),flip(a)]. 46 b * x * b0 = a * a0 * x. [para(4(a,1),15(a,1,2))]. 148 b0 * x * d = a0 * x * c. [para(39(a,2),12(a,1))]. 188 b0 * c0 = a0 * d0. [hyper(2,a,23,a(flip),b,46,a(flip)),rewrite([4(3)])]. 199 a0 * d0 * x = b0 * c0 * x. [para(188(a,1),1(a,1,1)),rewrite([1(4)])]. 280 d * d0 = c * c0. [hyper(2,a,148,a(flip),b,199,a),rewrite([4(3),4(6)]),flip(a)]. 281 $F. [resolve(280,a,9,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=31. Generated=1433. Kept=279. proofs=1. Usable=26. Sos=212. Demods=35. Limbo=0, Disabled=48. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=1154. Back_subsumed=3. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=48 (16 lex), Back_demodulated=37. Back_unit_deleted=0. Demod_attempts=14008. Demod_rewrites=1228. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=5367. Nonunit_bsub_feature_tests=1128. Megabytes=0.25. User_CPU=0.05, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 5115 exit (max_proofs) Tue Nov 3 09:42:18 2009