============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11390 was started by mccune on cleo.thornwood, Sat Aug 12 21:00:08 2006 The command was "/home/mccune/bin/prover9 -f quot-comm.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file quot-comm.in 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: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ 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(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 3). % (nonunit Horn with equality) Auto_process settings: (no changes). % Operation * is commutative; C redundancy checks enabled. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 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]. 9 d * d0 != c * 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.00 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 (I,wt=0): 9 d * d0 != c * c0. [assumption]. 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 (A,wt=17): 10 x * y * z != u | x * y * v != u | z = v. [para(1(a,1),2(a,1)),rewrite(1(5))]. given #12 (F,wt=0): 27 d * d0 * x != x * c * c0. [ur(3,b,4,a,c,9,a),rewrite(1(4))]. given #13 (F,wt=0): 28 d * d0 * x != c * c0 * x. [ur(3,b,1,a,c,9,a),rewrite(1(4))]. given #14 (T,wt=11): 16 b0 * x * b = x * a * a0. [para(5(a,1),1(a,2,2)),rewrite(4(4))]. given #15 (T,wt=11): 19 b0 * d * x = a0 * c * x. [para(7(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. given #16 (A,wt=17): 11 x * y * z != u | v * z != u | x * y = v. [para(1(a,1),3(a,1))]. given #17 (F,wt=0): 29 c * c0 * x != x * d * d0. [ur(3,a,4,a,c,9,a),rewrite(1(4))]. given #18 (F,wt=0): 30 d * d0 * x * y != x * y * c * c0. [ur(2,b,1,a,c,9,a),rewrite(12(5),4(4))]. given #19 (T,wt=11): 20 d * x * b0 = x * a0 * c. [para(7(a,1),1(a,2,2)),rewrite(4(4))]. given #20 (T,wt=11): 23 b * d0 * x = a * c0 * x. [para(8(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.04 (+ 0.00) seconds. % Length of proof is 17. % Level of proof is 4. % Maximum clause weight is 17. % Given clauses 20. 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]. 10 x * y * z != u | x * y * v != u | z = v. [para(1(a,1),2(a,1)),rewrite(1(5))]. 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)]. 19 b0 * d * x = a0 * c * x. [para(7(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)]. 30 d * d0 * x * y != x * y * c * c0. [ur(2,b,1,a,c,9,a),rewrite(12(5),4(4))]. 166 a0 * b * c * d0 * x * y != a * a0 * x * y * c * c0. [ur(10,b,15,a,c,30,a),rewrite(19(8),12(9))]. 216 b * x * d0 * y = x * a * c0 * y. [para(23(a,1),12(a,1,2)),flip(a)]. 222 $F. [back_rewrite(166),rewrite(216(8),12(8),12(9)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=20. Generated=1359. Kept=220. proofs=1. Usable=18. Sos=176. Demods=25. Limbo=6, Disabled=28. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=1138. Back_subsumed=6. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=28 (10 lex), Back_demodulated=14. Back_unit_deleted=0. Demod_attempts=19703. Demod_rewrites=2503. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=1513. Nonunit_bsub_feature_tests=336. Megabytes=0.21. User_CPU=0.04, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11390 exit (max_proofs) Sat Aug 12 21:00:08 2006