============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 4313 was started by mccune on cleo, Tue Nov 3 09:38:31 2009 The command was "/home/mccune/LADR/bin/prover9 -f cg1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file cg1.in assign(max_seconds,30). formulas(sos). x * y = x * z -> y = z. y * x = z * x -> y = z. end_of_list. formulas(sos). (x * y) * (z * u) = (x * z) * (y * u). end_of_list. formulas(goals). (x * (y * z)) * ((u * v) * w) = (x * (u * z)) * ((y * v) * w). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x * y = x * z -> y = z # label(non_clause). [assumption]. 2 y * x = z * x -> y = z # label(non_clause). [assumption]. 3 (x * (y * z)) * ((u * v) * w) = (x * (u * z)) * ((y * v) * w) # label(non_clause) # label(goal). [goal]. ============================== 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. [clausify(1)]. x * y != z * y | x = z. [clausify(2)]. (x * y) * (z * u) = (x * z) * (y * u). [assumption]. (c1 * (c4 * c3)) * ((c2 * c5) * c6) != (c1 * (c2 * c3)) * ((c4 * c5) * c6). [deny(3)]. 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([ c1, c2, c3, c4, c5, c6, * ]). 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, 2). % (nonunit Horn with equality) Auto_process settings: (no changes). kept: 4 x * y != x * z | y = z. [clausify(1)]. kept: 5 x * y != z * y | x = z. [clausify(2)]. kept: 6 (x * y) * (z * u) = (x * z) * (y * u). [assumption]. 7 (c1 * (c4 * c3)) * ((c2 * c5) * c6) != (c1 * (c2 * c3)) * ((c4 * c5) * c6). [deny(3)]. kept: 8 (c1 * (c2 * c3)) * ((c4 * c5) * c6) != (c1 * (c4 * c3)) * ((c2 * c5) * c6). [copy(7),flip(a)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 4 x * y != x * z | y = z. [clausify(1)]. 5 x * y != z * y | x = z. [clausify(2)]. 6 (x * y) * (z * u) = (x * z) * (y * u). [assumption]. 8 (c1 * (c2 * c3)) * ((c4 * c5) * c6) != (c1 * (c4 * c3)) * ((c2 * c5) * c6). [copy(7),flip(a)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=10): 4 x * y != x * z | y = z. [clausify(1)]. given #2 (I,wt=10): 5 x * y != z * y | x = z. [clausify(2)]. given #3 (I,wt=15): 6 (x * y) * (z * u) = (x * z) * (y * u). [assumption]. given #4 (I,wt=23): 8 (c1 * (c2 * c3)) * ((c4 * c5) * c6) != (c1 * (c4 * c3)) * ((c2 * c5) * c6). [copy(7),flip(a)]. given #5 (A,wt=18): 9 (x * y) * (z * u) != (x * z) * w | y * u = w. [para(6(a,1),4(a,1))]. given #6 (F,wt=23): 15 (c1 * (c4 * c5)) * ((c2 * c3) * c6) != (c1 * (c4 * c3)) * ((c2 * c5) * c6). [para(6(a,1),8(a,1))]. given #7 (F,wt=23): 16 (c1 * (c2 * c3)) * ((c4 * c5) * c6) != (c1 * (c2 * c5)) * ((c4 * c3) * c6). [para(6(a,1),8(a,2))]. given #8 (F,wt=23): 27 (c1 * (c4 * c5)) * ((c2 * c3) * c6) != (c1 * (c2 * c5)) * ((c4 * c3) * c6). [para(6(a,1),15(a,2))]. given #9 (F,wt=27): 13 ((c1 * (c2 * c3)) * ((c4 * c5) * c6)) * x != ((c1 * (c4 * c3)) * ((c2 * c5) * c6)) * x. [ur(5,b,8,a)]. given #10 (T,wt=18): 10 (x * y) * (z * u) != w * (y * u) | x * z = w. [para(6(a,1),5(a,1))]. given #11 (T,wt=22): 22 (x * y) * (z * u) != (x * w) * (z * v5) | y * u = w * v5. [para(6(a,1),9(a,2))]. given #12 (T,wt=22): 52 (x * y) * (z * u) != (w * y) * (v5 * u) | x * z = w * v5. [para(6(a,1),10(a,2))]. given #13 (T,wt=22): 60 (x * y) * (z * u) != (x * w) * (y * v5) | z * u = w * v5. [para(6(a,1),22(a,1))]. given #14 (A,wt=23): 11 ((x * y) * (z * u)) * (w * v5) = ((x * z) * w) * ((y * u) * v5). [para(6(a,1),6(a,1,1))]. given #15 (F,wt=27): 14 x * ((c1 * (c2 * c3)) * ((c4 * c5) * c6)) != x * ((c1 * (c4 * c3)) * ((c2 * c5) * c6)). [ur(4,b,8,a)]. given #16 (F,wt=27): 24 ((c1 * (c4 * c5)) * ((c2 * c3) * c6)) * x != ((c1 * (c4 * c3)) * ((c2 * c5) * c6)) * x. [ur(5,b,15,a)]. given #17 (F,wt=27): 25 x * ((c1 * (c4 * c5)) * ((c2 * c3) * c6)) != x * ((c1 * (c4 * c3)) * ((c2 * c5) * c6)). [ur(4,b,15,a)]. given #18 (F,wt=27): 29 ((c1 * (c2 * c3)) * ((c4 * c5) * c6)) * x != ((c1 * (c2 * c5)) * ((c4 * c3) * c6)) * x. [ur(5,b,16,a)]. given #19 (T,wt=22): 61 (x * y) * (z * u) != (x * w) * (y * v5) | w * v5 = z * u. [para(6(a,1),22(a,2)),flip(a)]. given #20 (T,wt=22): 68 (x * y) * (z * u) != (w * v5) * (y * u) | w * v5 = x * z. [para(6(a,1),52(a,1)),flip(a)]. given #21 (T,wt=22): 169 (x * y) * (z * u) != (x * w) * (z * v5) | w * v5 = y * u. [para(6(a,1),61(a,1))]. given #22 (T,wt=22): 170 (x * y) * (z * u) != (x * y) * (w * v5) | w * v5 = z * u. [para(6(a,1),61(a,2))]. given #23 (A,wt=23): 12 (x * (y * z)) * (u * (w * v5)) = (x * u) * ((y * w) * (z * v5)). [para(6(a,1),6(a,1,2)),flip(a)]. given #24 (F,wt=27): 30 x * ((c1 * (c2 * c3)) * ((c4 * c5) * c6)) != x * ((c1 * (c2 * c5)) * ((c4 * c3) * c6)). [ur(4,b,16,a)]. given #25 (F,wt=27): 33 ((c1 * (c4 * c5)) * ((c2 * c3) * c6)) * x != ((c1 * (c2 * c5)) * ((c4 * c3) * c6)) * x. [ur(5,b,27,a)]. given #26 (F,wt=27): 34 x * ((c1 * (c4 * c5)) * ((c2 * c3) * c6)) != x * ((c1 * (c2 * c5)) * ((c4 * c3) * c6)). [ur(4,b,27,a)]. given #27 (F,wt=31): 17 (x * (c1 * (c2 * c3))) * (y * ((c4 * c5) * c6)) != (x * y) * ((c1 * (c4 * c3)) * ((c2 * c5) * c6)). [ur(9,b,8,a)]. given #28 (T,wt=22): 173 (x * y) * (z * u) != (w * v5) * (z * u) | w * v5 = x * y. [para(6(a,1),68(a,1))]. given #29 (T,wt=22): 175 (x * y) * (z * u) != (w * y) * (v5 * u) | w * v5 = x * z. [para(6(a,1),68(a,2))]. given #30 (T,wt=23): 74 ((x * y) * z) * ((u * w) * v5) = ((x * u) * z) * ((y * w) * v5). [para(11(a,1),6(a,1))]. ============================== PROOF ================================= % Proof 1 at 0.10 (+ 0.00) seconds. % Length of proof is 14. % Level of proof is 5. % Maximum clause weight is 39.000. % Given clauses 30. 1 x * y = x * z -> y = z # label(non_clause). [assumption]. 3 (x * (y * z)) * ((u * v) * w) = (x * (u * z)) * ((y * v) * w) # label(non_clause) # label(goal). [goal]. 4 x * y != x * z | y = z. [clausify(1)]. 6 (x * y) * (z * u) = (x * z) * (y * u). [assumption]. 7 (c1 * (c4 * c3)) * ((c2 * c5) * c6) != (c1 * (c2 * c3)) * ((c4 * c5) * c6). [deny(3)]. 8 (c1 * (c2 * c3)) * ((c4 * c5) * c6) != (c1 * (c4 * c3)) * ((c2 * c5) * c6). [copy(7),flip(a)]. 9 (x * y) * (z * u) != (x * z) * w | y * u = w. [para(6(a,1),4(a,1))]. 11 ((x * y) * (z * u)) * (w * v5) = ((x * z) * w) * ((y * u) * v5). [para(6(a,1),6(a,1,1))]. 12 (x * (y * z)) * (u * (w * v5)) = (x * u) * ((y * w) * (z * v5)). [para(6(a,1),6(a,1,2)),flip(a)]. 17 (x * (c1 * (c2 * c3))) * (y * ((c4 * c5) * c6)) != (x * y) * ((c1 * (c4 * c3)) * ((c2 * c5) * c6)). [ur(9,b,8,a)]. 74 ((x * y) * z) * ((u * w) * v5) = ((x * u) * z) * ((y * w) * v5). [para(11(a,1),6(a,1))]. 417 ((x * y) * ((z * u) * (w * v5))) * ((v6 * v7) * v8) = ((x * v6) * (y * (u * v5))) * (((z * w) * v7) * v8). [para(12(a,1),74(a,1,1))]. 429 (x * ((y * z) * u)) * ((c1 * (c4 * c3)) * ((c2 * c5) * c6)) != (x * (c1 * (c2 * c3))) * (((y * c4) * u) * ((z * c5) * c6)). [para(74(a,1),17(a,1,2)),flip(a)]. 430 $F. [resolve(429,a,417,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=30. Generated=1228. Kept=425. proofs=1. Usable=30. Sos=317. Demods=0. Limbo=63, Disabled=18. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=803. Back_subsumed=14. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=13020. Nonunit_bsub_feature_tests=2037. Megabytes=0.64. User_CPU=0.10, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 4313 exit (max_proofs) Tue Nov 3 09:38:31 2009