============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11397 was started by mccune on cleo.thornwood, Sat Aug 12 21:01:00 2006 The command was "/home/mccune/bin/prover9 -f quot-general.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file quot-general.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 * f(x,y) * y = y * g(x,y) * x # label(general_case). 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 * f(x,y) * y = y * g(x,y) * x # label(general_case). [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, *, f, g ]). 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). ============================== 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]. 5 x * g(y,x) * y = y * f(y,x) * x. [copy(4),flip(a)]. 6 b * b0 = a * a0. [assumption]. 7 d * b0 = c * a0. [assumption]. 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]. 5 x * g(y,x) * y = y * f(y,x) * x. [copy(4),flip(a)]. 6 b * b0 = a * a0. [assumption]. 7 d * b0 = c * a0. [assumption]. 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=15): 5 x * g(y,x) * y = y * f(y,x) * x. [copy(4),flip(a)]. given #5 (I,wt=7): 6 b * b0 = a * a0. [assumption]. given #6 (I,wt=7): 7 d * b0 = c * a0. [assumption]. 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): 13 g(x,x) * x = f(x,x) * x. [hyper(2,a,xx,b,5,a),flip(a)]. given #10 (T,wt=7): 34 g(x,x) = f(x,x). [hyper(3,a,xx,b,13,a),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): 29 d * d0 * g(x,c * c0) * x != x * f(x,c * c0) * c * c0. [ur(3,b,5,a,c,9,a),rewrite(1(9))]. given #13 (F,wt=0): 30 d * d0 * x != c * c0 * x. [ur(3,b,1,a,c,9,a),rewrite(1(4))]. given #14 (T,wt=11): 20 b * b0 * x = a * a0 * x. [para(6(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. given #15 (T,wt=11): 23 d * b0 * x = c * a0 * 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): 31 c * c0 * g(x,d * d0) * x != x * f(x,d * d0) * d * d0. [ur(3,a,5,a,c,9,a),rewrite(1(9))]. given #18 (F,wt=0): 32 x * y * d * d0 != x * y * c * c0. [ur(2,b,1,a,c,9,a),rewrite(1(5))]. given #19 (T,wt=11): 26 b * d0 * x = a * c0 * x. [para(8(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. given #20 (T,wt=13): 21 a * a0 != x | b * y != x | b0 = y. [para(6(a,1),2(a,1))]. given #21 (A,wt=19): 12 g(x * y,x) * x * y = y * f(x * y,x) * x. [hyper(2,a,1,a(flip),b,5,a),flip(a)]. given #22 (F,wt=0): 33 x * d * d0 != x * c * c0. [ur(2,b,1,a(flip),c,9,a),rewrite(1(8))]. given #23 (F,wt=0): 35 x * g(c * c0,x) * d * d0 != c * c0 * f(c * c0,x) * x. [ur(10,b,5,a,c,9,a),rewrite(1(18))]. given #24 (T,wt=13): 22 a * a0 != x | y * b0 != x | b = y. [para(6(a,1),3(a,1))]. given #25 (T,wt=13): 24 c * a0 != x | d * y != x | b0 = y. [para(7(a,1),2(a,1))]. given #26 (A,wt=19): 14 x * g(y,y * x) * y = f(y,y * x) * y * x. [hyper(2,a,1,a(flip),b,5,a(flip))]. given #27 (F,wt=0): 36 x * g(d * d0,x) * c * c0 != d * d0 * f(d * d0,x) * x. [ur(10,b,5,a,c,9,a(flip)),rewrite(1(18))]. given #28 (F,wt=0): 37 x * y * z * d * d0 != x * y * z * c * c0. [ur(10,b,1,a,c,9,a),rewrite(1(6))]. given #29 (T,wt=13): 25 c * a0 != x | y * b0 != x | d = y. [para(7(a,1),3(a,1))]. given #30 (T,wt=13): 27 a * c0 != x | b * y != x | d0 = y. [para(8(a,1),2(a,1))]. given #31 (A,wt=19): 15 x * g(y,x) * y * z = y * f(y,x) * x * z. [para(5(a,1),1(a,1,1)),rewrite(1(4),1(3),1(7)),flip(a)]. given #32 (F,wt=0): 45 x * g(y * f(y,c * c0) * c * c0,x) * d * d0 * g(y,c * c0) * y != y * f(y,c * c0) * c * c0 * f(y * f(y,c * c0) * c * c0,x) * x. [ur(10,b,5,a,c,29,a),rewrite(1(42),1(41),1(40))]. given #33 (F,wt=0): 46 x * y * z * d * d0 * g(u,c * c0) * u != x * y * z * u * f(u,c * c0) * c * c0. [ur(10,b,1,a,c,29,a),rewrite(1(12))]. given #34 (T,wt=13): 28 a * c0 != x | y * d0 != x | b = y. [para(8(a,1),3(a,1))]. given #35 (T,wt=13): 124 a * a0 != x | a * c0 != x | d0 = b0. [para(8(a,1),21(b,1)),flip(c)]. given #36 (A,wt=23): 16 x * y * g(z,x * y) * z = z * f(z,x * y) * x * y. [para(5(a,1),1(a,1)),flip(a)]. given #37 (F,wt=0): 48 x * y * d * d0 * g(z,c * c0) * z != x * y * z * f(z,c * c0) * c * c0. [ur(10,b,1,a(flip),c,29,a),rewrite(1(22))]. given #38 (F,wt=0): 49 x * g(d * d0 * g(y,c * c0) * y,x) * y * f(y,c * c0) * c * c0 != d * d0 * g(y,c * c0) * y * f(d * d0 * g(y,c * c0) * y,x) * x. [ur(10,a,5,a,c,29,a),rewrite(1(42),1(41),1(40))]. given #39 (T,wt=13): 205 a * a0 != x | c * a0 != x | d = b. [para(7(a,1),22(b,1)),flip(c)]. given #40 (T,wt=15): 127 g(x * x,x) * x = x * f(x * x,x). [hyper(11,a,12,a,b,1,a)]. given #41 (A,wt=21): 17 x * f(x,y) * y != z | y * u != z | g(x,y) * x = u. [para(5(a,1),2(a,1))]. given #42 (F,wt=0): 50 d * d0 * g(x,c * c0) * x * g(y,x * f(x,c * c0) * c * c0) * y != y * f(y,x * f(x,c * c0) * c * c0) * x * f(x,c * c0) * c * c0. [ur(3,b,5,a,c,29,a),rewrite(1(21),1(20),1(19))]. given #43 (F,wt=0): 51 d * d0 * g(x,c * c0) * x * y != x * f(x,c * c0) * c * c0 * y. [ur(3,b,1,a,c,29,a),rewrite(1(10),1(9),1(8),1(19),1(18))]. given #44 (T,wt=15): 208 x * g(x,x * x) = f(x,x * x) * x. [hyper(11,a,14,a,b,1,a)]. given #45 (T,wt=17): 42 x * a * a0 != y | x * b * z != y | b0 = z. [para(6(a,1),10(a,1,2))]. given #46 (A,wt=21): 18 x * f(x,y) * y != z | u * g(x,y) * x != z | y = u. [para(5(a,1),3(a,1))]. given #47 (F,wt=0): 52 x * f(x,c * c0) * c * c0 * g(y,d * d0 * g(x,c * c0) * x) * y != y * f(y,d * d0 * g(x,c * c0) * x) * d * d0 * g(x,c * c0) * x. [ur(3,a,5,a,c,29,a),rewrite(1(21),1(20),1(19))]. given #48 (F,wt=0): 53 x * d * d0 * g(y,c * c0) * y != x * y * f(y,c * c0) * c * c0. [ur(2,b,1,a(flip),c,29,a),rewrite(1(20))]. given #49 (T,wt=17): 43 x * c * a0 != y | x * d * z != y | b0 = z. [para(7(a,1),10(a,1,2))]. given #50 (T,wt=17): 44 x * a * c0 != y | x * b * z != y | d0 = z. [para(8(a,1),10(a,1,2))]. given #51 (A,wt=21): 19 x * g(y,z) * y != u | y * f(y,z) * z != u | x = z. [para(5(a,1),3(b,1))]. given #52 (F,wt=0): 54 x * g(c * c0 * y,x) * d * d0 * y != c * c0 * y * f(c * c0 * y,x) * x. [ur(10,b,5,a,c,30,a),rewrite(1(22),1(21))]. given #53 (F,wt=0): 55 x * y * z * d * d0 * u != x * y * z * c * c0 * u. [ur(10,b,1,a,c,30,a),rewrite(1(7))]. given #54 (T,wt=17): 63 a * a0 * x != y | b * z != y | b0 * x = z. [para(20(a,1),2(a,1))]. given #55 (T,wt=17): 64 a * a0 * x != y | z * b0 * x != y | b = z. [para(20(a,1),3(a,1))]. given #56 (A,wt=21): 38 x * y * z * u != v | x * y * z * w != v | u = w. [para(1(a,1),10(a,1,2)),rewrite(1(6))]. given #57 (F,wt=0): 57 x * y * d * d0 * z != x * y * c * c0 * z. [ur(10,b,1,a(flip),c,30,a),rewrite(1(12))]. given #58 (F,wt=0): 58 x * g(d * d0 * y,x) * c * c0 * y != d * d0 * y * f(d * d0 * y,x) * x. [ur(10,a,5,a,c,30,a),rewrite(1(22),1(21))]. given #59 (T,wt=17): 68 c * a0 * x != y | d * z != y | b0 * x = z. [para(23(a,1),2(a,1))]. given #60 (T,wt=17): 69 c * a0 * x != y | z * b0 * x != y | d = z. [para(23(a,1),3(a,1))]. given #61 (A,wt=25): 39 x * y * f(y,z) * z != u | x * z * v != u | g(y,z) * y = v. [para(5(a,1),10(a,1,2))]. given #62 (F,wt=0): 59 d * d0 * x * g(y,c * c0 * x) * y != y * f(y,c * c0 * x) * c * c0 * x. [ur(3,b,5,a,c,30,a),rewrite(1(11),1(10))]. given #63 (F,wt=0): 60 c * c0 * x * g(y,d * d0 * x) * y != y * f(y,d * d0 * x) * d * d0 * x. [ur(3,a,5,a,c,30,a),rewrite(1(11),1(10))]. given #64 (T,wt=17): 78 x * a * a0 != y | z * b0 != y | x * b = z. [para(6(a,1),11(a,1,2))]. given #65 (T,wt=17): 79 x * y * b0 != z | a * a0 != z | x * y = b. [para(6(a,1),11(b,1))]. given #66 (A,wt=21): 40 x * f(x,y) * y != z | y * g(x,y) * u != z | x = u. [para(5(a,1),10(a,1))]. given #67 (F,wt=0): 61 x * d * d0 * y != x * c * c0 * y. [ur(2,b,1,a(flip),c,30,a),rewrite(1(10))]. given #68 (F,wt=0): 62 b * d * d0 * g(b0,c * c0) * b0 != a * a0 * f(b0,c * c0) * c * c0. [ur(2,b,20,a,c,29,a)]. given #69 (T,wt=17): 80 x * c * a0 != y | z * b0 != y | x * d = z. [para(7(a,1),11(a,1,2))]. given #70 (T,wt=17): 81 x * y * b0 != z | c * a0 != z | x * y = d. [para(7(a,1),11(b,1))]. given #71 (A,wt=21): 41 x * g(y,x) * z != u | y * f(y,x) * x != u | z = y. [para(5(a,1),10(b,1))]. given #72 (F,wt=0): 67 d * d * d0 * g(b0,c * c0) * b0 != c * a0 * f(b0,c * c0) * c * c0. [ur(2,b,23,a,c,29,a)]. given #73 (F,wt=0): 72 d * d0 * g(x * y,c * c0) * x * y * z != x * y * f(x * y,c * c0) * c * c0 * z. [ur(11,a,1,a,c,29,a(flip)),rewrite(1(12),1(11),1(10),1(9),1(22),1(21))]. given #74 (T,wt=17): 82 x * a * c0 != y | z * d0 != y | x * b = z. [para(8(a,1),11(a,1,2))]. given #75 (T,wt=17): 83 x * y * d0 != z | a * c0 != z | x * y = b. [para(8(a,1),11(b,1))]. given #76 (A,wt=19): 65 a * a0 * g(x,b0) * x = b * x * f(x,b0) * b0. [para(5(a,1),20(a,1,2)),flip(a)]. given #77 (F,wt=0): 88 c * c0 * g(x,d * d0) * x * g(y,x * f(x,d * d0) * d * d0) * y != y * f(y,x * f(x,d * d0) * d * d0) * x * f(x,d * d0) * d * d0. [ur(11,b,5,a,c,31,a),rewrite(1(20),1(19))]. given #78 (F,wt=0): 89 c * c0 * g(x,d * d0) * x * y != x * f(x,d * d0) * d * d0 * y. [ur(11,b,1,a,c,31,a),rewrite(1(9),1(8),1(19),1(18))]. given #79 (T,wt=15): 2192 a0 * g(d0,b0) * d0 = c0 * f(d0,b0) * b0. [hyper(2,a,26,a(flip),b,65,a),flip(a)]. ============================== PROOF ================================= % Proof 1 at 1.19 (+ 0.01) seconds. % Length of proof is 17. % Level of proof is 5. % Maximum clause weight is 19. % Given clauses 79. 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 * f(x,y) * y = y * g(x,y) * x # label(general_case). [assumption]. 5 x * g(y,x) * y = y * f(y,x) * x. [copy(4),flip(a)]. 6 b * b0 = a * a0. [assumption]. 7 d * b0 = c * a0. [assumption]. 8 b * d0 = a * c0. [assumption]. 9 d * d0 != c * c0. [assumption]. 20 b * b0 * x = a * a0 * x. [para(6(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. 23 d * b0 * x = c * a0 * x. [para(7(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. 26 b * d0 * x = a * c0 * x. [para(8(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. 30 d * d0 * x != c * c0 * x. [ur(3,b,1,a,c,9,a),rewrite(1(4))]. 65 a * a0 * g(x,b0) * x = b * x * f(x,b0) * b0. [para(5(a,1),20(a,1,2)),flip(a)]. 2192 a0 * g(d0,b0) * d0 = c0 * f(d0,b0) * b0. [hyper(2,a,26,a(flip),b,65,a),flip(a)]. 2404 d * d0 * f(d0,b0) * b0 = c * c0 * f(d0,b0) * b0. [para(2192(a,1),23(a,2,2)),rewrite(5(8))]. 2405 $F. [resolve(2404,a,30,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=79. Generated=13154. Kept=2403. proofs=1. Usable=78. Sos=2046. Demods=77. Limbo=5, Disabled=281. Hints=0. Weight_deleted=109. Literals_deleted=0. Forward_subsumed=10642. Back_subsumed=258. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=78 (0 lex), Back_demodulated=15. Back_unit_deleted=0. Demod_attempts=728684. Demod_rewrites=62685. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=5155. Nonunit_bsub_feature_tests=906. Megabytes=10.31. User_CPU=1.19, System_CPU=0.01, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11397 exit (max_proofs) Sat Aug 12 21:01:01 2006