============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 3904 was started by mccune on cleo.thornwood, Wed Nov 22 11:25:05 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). restricted denial: (wt=7): 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]. 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. 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 (F,wt=11): 13 g(x,x) * x = f(x,x) * x. [hyper(2,a,xx,b,5,a),flip(a)]. given #9 (T,wt=7): 29 g(x,x) = f(x,x). [hyper(3,a,xx,b,13,a),flip(a)]. given #10 (T,wt=11): 20 b * b0 * x = a * a0 * x. [para(6(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=11): 23 d * b0 * x = c * a0 * x. [para(7(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. given #13 (F,wt=11): 26 b * d0 * x = a * c0 * x. [para(8(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. given #14 (T,wt=13): 21 a * a0 != x | b * y != x | b0 = y. [para(6(a,1),2(a,1))]. given #15 (T,wt=13): 22 a * a0 != x | y * b0 != x | b = y. [para(6(a,1),3(a,1))]. 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=13): 24 c * a0 != x | d * y != x | b0 = y. [para(7(a,1),2(a,1))]. given #18 (F,wt=13): 25 c * a0 != x | y * b0 != x | d = y. [para(7(a,1),3(a,1))]. given #19 (T,wt=13): 27 a * c0 != x | b * y != x | d0 = y. [para(8(a,1),2(a,1))]. given #20 (T,wt=13): 28 a * c0 != x | y * d0 != x | b = y. [para(8(a,1),3(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=13): 50 a * a0 != x | a * c0 != x | d0 = b0. [para(8(a,1),21(b,1)),flip(c)]. given #23 (F,wt=13): 54 a * a0 != x | c * a0 != x | d = b. [para(7(a,1),22(b,1)),flip(c)]. given #24 (T,wt=15): 76 g(x * x,x) * x = x * f(x * x,x). [hyper(11,a,12,a,b,1,a)]. given #25 (T,wt=17): 30 a * a0 * x != y | b * z != y | b0 * x = z. [para(20(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=15): 111 x * g(x,x * x) = f(x,x * x) * x. [hyper(11,a,14,a,b,1,a)]. given #28 (F,wt=17): 31 a * a0 * x != y | z * b0 * x != y | b = z. [para(20(a,1),3(a,1))]. given #29 (T,wt=17): 37 x * a * a0 != y | x * b * z != y | b0 = z. [para(6(a,1),10(a,1,2))]. given #30 (T,wt=17): 38 x * c * a0 != y | x * d * z != y | b0 = z. [para(7(a,1),10(a,1,2))]. 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=17): 39 x * a * c0 != y | x * b * z != y | d0 = z. [para(8(a,1),10(a,1,2))]. given #33 (F,wt=17): 41 c * a0 * x != y | d * z != y | b0 * x = z. [para(23(a,1),2(a,1))]. given #34 (T,wt=17): 42 c * a0 * x != y | z * b0 * x != y | d = z. [para(23(a,1),3(a,1))]. given #35 (T,wt=17): 45 a * c0 * x != y | b * z != y | d0 * x = z. [para(26(a,1),2(a,1))]. 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=17): 46 a * c0 * x != y | z * d0 * x != y | b = z. [para(26(a,1),3(a,1))]. given #38 (F,wt=17): 51 a * a0 != x | a * a0 * y != x | b0 * y = b0. [para(20(a,1),21(b,1)),flip(c)]. given #39 (T,wt=17): 52 a * a0 != x | a * c0 * y != x | d0 * y = b0. [para(26(a,1),21(b,1)),flip(c)]. given #40 (T,wt=17): 53 a * a0 != x | y * z * b0 != x | y * z = b. [para(1(a,1),22(b,1)),flip(c)]. 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=17): 60 x * a * a0 != y | z * b0 != y | x * b = z. [para(6(a,1),11(a,1,2))]. given #43 (F,wt=17): 61 x * c * a0 != y | z * b0 != y | x * d = z. [para(7(a,1),11(a,1,2))]. given #44 (T,wt=17): 62 x * y * b0 != z | c * a0 != z | x * y = d. [para(7(a,1),11(b,1))]. given #45 (T,wt=17): 63 x * a * c0 != y | z * d0 != y | x * b = z. [para(8(a,1),11(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=17): 64 x * y * d0 != z | a * c0 != z | x * y = b. [para(8(a,1),11(b,1))]. given #48 (F,wt=17): 72 c * a0 != x | c * a0 * y != x | b0 * y = b0. [para(23(a,1),24(b,1)),flip(c)]. given #49 (T,wt=17): 74 a * c0 != x | a * a0 * y != x | b0 * y = d0. [para(20(a,1),27(b,1)),flip(c)]. given #50 (T,wt=17): 75 a * c0 != x | a * c0 * y != x | d0 * y = d0. [para(26(a,1),27(b,1)),flip(c)]. 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=17): 157 a * a0 * x != y | c * a0 * x != y | d = b. [para(23(a,1),31(b,1)),flip(c)]. given #53 (F,wt=17): 163 x * a * a0 != y | x * a * c0 != y | d0 = b0. [para(8(a,1),37(b,1,2)),flip(c)]. given #54 (T,wt=17): 313 a * a0 != x | y * a * a0 != x | y * b = b. [para(6(a,1),53(b,1,2))]. given #55 (T,wt=17): 314 a * a0 != x | y * c * a0 != x | y * d = b. [para(7(a,1),53(b,1,2))]. given #56 (A,wt=19): 32 a * a0 * g(x,b0) * x = b * x * f(x,b0) * b0. [para(5(a,1),20(a,1,2)),flip(a)]. given #57 (F,wt=15): 383 a0 * g(d0,b0) * d0 = c0 * f(d0,b0) * b0. [hyper(2,a,26,a(flip),b,32,a),flip(a)]. given #58 (F,wt=17): 325 x * a * a0 != y | c * a0 != y | x * b = d. [para(7(a,1),60(b,1))]. given #59 (T,wt=17): 330 x * c * a0 != y | c * a0 != y | x * d = d. [para(7(a,1),61(b,1))]. given #60 (T,wt=17): 340 x * a * c0 != y | a * c0 != y | x * b = b. [para(8(a,1),63(b,1))]. given #61 (A,wt=21): 33 x * y * z * u != v | x * y * z * w != v | u = w. [para(1(a,1),10(a,1,2)),rewrite(1(6))]. given #62 (F,wt=19): 43 c * a0 * g(x,b0) * x = d * x * f(x,b0) * b0. [para(5(a,1),23(a,1,2)),flip(a)]. given #63 (F,wt=19): 47 a * c0 * g(x,d0) * x = b * x * f(x,d0) * d0. [para(5(a,1),26(a,1,2)),flip(a)]. given #64 (T,wt=15): 465 c0 * g(b0,d0) * b0 = a0 * f(b0,d0) * d0. [hyper(2,a,20,a(flip),b,47,a),flip(a)]. given #65 (T,wt=19): 82 g(a * a0,b) * a * a0 = b0 * f(a * a0,b) * b. [para(6(a,1),12(a,1,1,1)),rewrite(6(8),6(13))]. given #66 (A,wt=25): 34 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 #67 (F,wt=19): 83 g(c * a0,d) * c * a0 = b0 * f(c * a0,d) * d. [para(7(a,1),12(a,1,1,1)),rewrite(7(8),7(13))]. given #68 (F,wt=19): 84 g(a * c0,b) * a * c0 = d0 * f(a * c0,b) * b. [para(8(a,1),12(a,1,1,1)),rewrite(8(8),8(13))]. given #69 (T,wt=19): 94 g(x * x,x) * x * y = x * f(x * x,x) * y. [para(76(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. given #70 (T,wt=19): 106 b0 * g(b,a * a0) * b = f(b,a * a0) * a * a0. [hyper(30,a,1,a(flip),b,5,a(flip))]. given #71 (A,wt=21): 35 x * f(x,y) * y != z | y * g(x,y) * u != z | x = u. [para(5(a,1),10(a,1))]. given #72 (F,wt=19): 119 b0 * g(d,c * a0) * d = f(d,c * a0) * c * a0. [para(7(a,1),14(a,1,2,1,2)),rewrite(7(13),7(17))]. given #73 (F,wt=19): 120 d0 * g(b,a * c0) * b = f(b,a * c0) * a * c0. [para(8(a,1),14(a,1,2,1,2)),rewrite(8(13),8(17))]. given #74 (T,wt=19): 138 x * g(x,x * x) * y = f(x,x * x) * x * y. [para(111(a,1),1(a,1,1)),rewrite(1(4)),flip(a)]. given #75 (T,wt=19): 143 a * a0 * g(b0,b0 * b0) = b * f(b0,b0 * b0) * b0. [para(111(a,1),20(a,1,2)),flip(a)]. given #76 (A,wt=21): 36 x * g(y,x) * z != u | y * f(y,x) * x != u | z = y. [para(5(a,1),10(b,1))]. given #77 (F,wt=19): 145 c * a0 * g(b0,b0 * b0) = d * f(b0,b0 * b0) * b0. [para(111(a,1),23(a,1,2)),flip(a)]. given #78 (F,wt=19): 146 a * c0 * g(d0,d0 * d0) = b * f(d0,d0 * d0) * d0. [para(111(a,1),26(a,1,2)),flip(a)]. given #79 (T,wt=19): 185 x * g(b,x) * a * a0 = b * f(b,x) * x * b0. [para(6(a,1),15(a,1,2,2))]. given #80 (T,wt=19): 186 x * g(d,x) * c * a0 = d * f(d,x) * x * b0. [para(7(a,1),15(a,1,2,2))]. given #81 (A,wt=21): 40 x * a * a0 * y != z | x * b * u != z | b0 * y = u. [para(20(a,1),10(a,1,2))]. given #82 (F,wt=19): 187 x * g(b,x) * a * c0 = b * f(b,x) * x * d0. [para(8(a,1),15(a,1,2,2))]. given #83 (F,wt=19): 395 a0 * g(d0,b0) * d0 * x = c0 * f(d0,b0) * b0 * x. [para(383(a,1),1(a,1,1)),rewrite(1(8),1(7),1(15)),flip(a)]. given #84 (T,wt=19): 400 d * d0 * f(d0,b0) * b0 = c * c0 * f(d0,b0) * b0. [para(383(a,1),23(a,2,2)),rewrite(5(8))]. ============================== PROOF ================================= % Proof 1 at 0.18 (+ 0.00) seconds. % Length of proof is 18. % Level of proof is 6. % Maximum clause weight is 19. % Given clauses 84. 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]. 11 x * y * z != u | v * z != u | x * y = v. [para(1(a,1),3(a,1))]. 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)]. 32 a * a0 * g(x,b0) * x = b * x * f(x,b0) * b0. [para(5(a,1),20(a,1,2)),flip(a)]. 383 a0 * g(d0,b0) * d0 = c0 * f(d0,b0) * b0. [hyper(2,a,26,a(flip),b,32,a),flip(a)]. 400 d * d0 * f(d0,b0) * b0 = c * c0 * f(d0,b0) * b0. [para(383(a,1),23(a,2,2)),rewrite(5(8))]. 899 d * d0 = c * c0. [hyper(11,a,400,a,b,1,a)]. 900 $F. [resolve(899,a,9,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=84. Generated=2804. Kept=898. proofs=1. Usable=84. Sos=812. Demods=148. Limbo=0, Disabled=9. Hints=0. Weight_deleted=304. Literals_deleted=0. Forward_subsumed=1602. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=149 (0 lex), Back_demodulated=1. Back_unit_deleted=0. Demod_attempts=59095. Demod_rewrites=2604. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=17500. Nonunit_bsub_feature_tests=2351. Megabytes=1.33. User_CPU=0.18, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3904 exit (max_proofs) Wed Nov 22 11:25:05 2006