2.007/2.007 YES 2.007/2.007 2.007/2.007 Problem 1: 2.007/2.007 2.007/2.007 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 Confluence Problem: 2.007/2.007 (VAR vNonEmpty x) 2.007/2.007 (REPLACEMENT-MAP 2.007/2.007 (a) 2.007/2.007 (c) 2.007/2.007 (f 1) 2.007/2.007 (h 1) 2.007/2.007 (b) 2.007/2.007 (fSNonEmpty) 2.007/2.007 (g 1) 2.007/2.007 (k 1) 2.007/2.007 ) 2.007/2.007 (RULES 2.007/2.007 a -> b 2.007/2.007 c -> k(f(a)) 2.007/2.007 c -> k(g(b)) 2.007/2.007 f(x) -> g(x) | h(f(x)) ->* k(g(b)) 2.007/2.007 h(f(a)) -> c 2.007/2.007 h(x) -> k(x) 2.007/2.007 ) 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 2.007/2.007 2.007/2.007 Problem 1: 2.007/2.007 2.007/2.007 Inlining of Conditions Processor [STERN17]: 2.007/2.007 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 Confluence Problem: 2.007/2.007 (VAR vNonEmpty x) 2.007/2.007 (REPLACEMENT-MAP 2.007/2.007 (a) 2.007/2.007 (c) 2.007/2.007 (f 1) 2.007/2.007 (h 1) 2.007/2.007 (b) 2.007/2.007 (fSNonEmpty) 2.007/2.007 (g 1) 2.007/2.007 (k 1) 2.007/2.007 ) 2.007/2.007 (RULES 2.007/2.007 a -> b 2.007/2.007 c -> k(f(a)) 2.007/2.007 c -> k(g(b)) 2.007/2.007 f(x) -> g(x) | h(f(x)) ->* k(g(b)) 2.007/2.007 h(f(a)) -> c 2.007/2.007 h(x) -> k(x) 2.007/2.007 ) 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 2.007/2.007 2.007/2.007 Problem 1: 2.007/2.007 2.007/2.007 Clean CTRS Processor: 2.007/2.007 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 Confluence Problem: 2.007/2.007 (VAR x) 2.007/2.007 (REPLACEMENT-MAP 2.007/2.007 (a) 2.007/2.007 (c) 2.007/2.007 (f 1) 2.007/2.007 (h 1) 2.007/2.007 (b) 2.007/2.007 (fSNonEmpty) 2.007/2.007 (g 1) 2.007/2.007 (k 1) 2.007/2.007 ) 2.007/2.007 (RULES 2.007/2.007 a -> b 2.007/2.007 c -> k(f(a)) 2.007/2.007 c -> k(g(b)) 2.007/2.007 f(x) -> g(x) | h(f(x)) ->* k(g(b)) 2.007/2.007 h(f(a)) -> c 2.007/2.007 h(x) -> k(x) 2.007/2.007 ) 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 2.007/2.007 CRule InfChecker Info: 2.007/2.007 a -> b 2.007/2.007 Rule remains 2.007/2.007 Proof: 2.007/2.007 NO_CONDS 2.007/2.007 2.007/2.007 CRule InfChecker Info: 2.007/2.007 c -> k(f(a)) 2.007/2.007 Rule remains 2.007/2.007 Proof: 2.007/2.007 NO_CONDS 2.007/2.007 2.007/2.007 CRule InfChecker Info: 2.007/2.007 c -> k(g(b)) 2.007/2.007 Rule remains 2.007/2.007 Proof: 2.007/2.007 NO_CONDS 2.007/2.007 2.007/2.007 CRule InfChecker Info: 2.007/2.007 f(x) -> g(x) | h(f(x)) ->* k(g(b)) 2.007/2.007 Rule remains 2.007/2.007 Proof: 2.007/2.007 NO 2.007/2.007 2.007/2.007 Problem 1: 2.007/2.007 2.007/2.007 Infeasibility Problem: 2.007/2.007 [(VAR vNonEmpty x vNonEmpty x) 2.007/2.007 (STRATEGY CONTEXTSENSITIVE 2.007/2.007 (a) 2.007/2.007 (c) 2.007/2.007 (f 1) 2.007/2.007 (h 1) 2.007/2.007 (b) 2.007/2.007 (fSNonEmpty) 2.007/2.007 (g 1) 2.007/2.007 (k 1) 2.007/2.007 ) 2.007/2.007 (RULES 2.007/2.007 a -> b 2.007/2.007 c -> k(f(a)) 2.007/2.007 c -> k(g(b)) 2.007/2.007 f(x) -> g(x) | h(f(x)) ->* k(g(b)) 2.007/2.007 h(f(a)) -> c 2.007/2.007 h(x) -> k(x) 2.007/2.007 )] 2.007/2.007 2.007/2.007 Infeasibility Conditions: 2.007/2.007 h(f(x)) ->* k(g(b)) 2.007/2.007 2.007/2.007 Problem 1: 2.007/2.007 2.007/2.007 Obtaining a proof using Prover9: 2.007/2.007 2.007/2.007 -> Prover9 Output: 2.007/2.007 ============================== Prover9 =============================== 2.007/2.007 Prover9 (64) version 2009-11A, November 2009. 2.007/2.007 Process 78146 was started by ubuntu on ubuntu, 2.007/2.007 Wed Mar 9 10:20:05 2022 2.007/2.007 The command was "./prover9 -f /tmp/prover978135-0.in". 2.007/2.007 ============================== end of head =========================== 2.007/2.007 2.007/2.007 ============================== INPUT ================================= 2.007/2.007 2.007/2.007 % Reading from file /tmp/prover978135-0.in 2.007/2.007 2.007/2.007 assign(max_seconds,20). 2.007/2.007 2.007/2.007 formulas(assumptions). 2.007/2.007 ->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence). 2.007/2.007 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence). 2.007/2.007 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence). 2.007/2.007 ->_s0(x1,y) -> ->_s0(k(x1),k(y)) # label(congruence). 2.007/2.007 ->_s0(a,b) # label(replacement). 2.007/2.007 ->_s0(c,k(f(a))) # label(replacement). 2.007/2.007 ->_s0(c,k(g(b))) # label(replacement). 2.007/2.007 ->*_s0(h(f(x1)),k(g(b))) -> ->_s0(f(x1),g(x1)) # label(replacement). 2.007/2.007 ->_s0(h(f(a)),c) # label(replacement). 2.007/2.007 ->_s0(h(x1),k(x1)) # label(replacement). 2.007/2.007 ->*_s0(x,x) # label(reflexivity). 2.007/2.007 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(goals). 2.007/2.007 (exists x3 ->*_s0(h(f(x3)),k(g(b)))) # label(goal). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 ============================== end of input ========================== 2.007/2.007 2.007/2.007 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 2.007/2.007 2.007/2.007 % Formulas that are not ordinary clauses: 2.007/2.007 1 ->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 2.007/2.007 2 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 2.007/2.007 3 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 2.007/2.007 4 ->_s0(x1,y) -> ->_s0(k(x1),k(y)) # label(congruence) # label(non_clause). [assumption]. 2.007/2.007 5 ->*_s0(h(f(x1)),k(g(b))) -> ->_s0(f(x1),g(x1)) # label(replacement) # label(non_clause). [assumption]. 2.007/2.007 6 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 2.007/2.007 7 (exists x3 ->*_s0(h(f(x3)),k(g(b)))) # label(goal) # label(non_clause) # label(goal). [goal]. 2.007/2.007 2.007/2.007 ============================== end of process non-clausal formulas === 2.007/2.007 2.007/2.007 ============================== PROCESS INITIAL CLAUSES =============== 2.007/2.007 2.007/2.007 % Clauses before input processing: 2.007/2.007 2.007/2.007 formulas(usable). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(sos). 2.007/2.007 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(1)]. 2.007/2.007 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(2)]. 2.007/2.007 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(3)]. 2.007/2.007 -->_s0(x,y) | ->_s0(k(x),k(y)) # label(congruence). [clausify(4)]. 2.007/2.007 ->_s0(a,b) # label(replacement). [assumption]. 2.007/2.007 ->_s0(c,k(f(a))) # label(replacement). [assumption]. 2.007/2.007 ->_s0(c,k(g(b))) # label(replacement). [assumption]. 2.007/2.007 -->*_s0(h(f(x)),k(g(b))) | ->_s0(f(x),g(x)) # label(replacement). [clausify(5)]. 2.007/2.007 ->_s0(h(f(a)),c) # label(replacement). [assumption]. 2.007/2.007 ->_s0(h(x),k(x)) # label(replacement). [assumption]. 2.007/2.007 ->*_s0(x,x) # label(reflexivity). [assumption]. 2.007/2.007 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(6)]. 2.007/2.007 -->*_s0(h(f(x)),k(g(b))) # label(goal). [deny(7)]. 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(demodulators). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 ============================== PREDICATE ELIMINATION ================= 2.007/2.007 2.007/2.007 No predicates eliminated. 2.007/2.007 2.007/2.007 ============================== end predicate elimination ============= 2.007/2.007 2.007/2.007 Auto_denials: 2.007/2.007 % copying label goal to answer in negative clause 2.007/2.007 2.007/2.007 Term ordering decisions: 2.007/2.007 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 2.007/2.007 Function symbol precedence: function_order([ a, c, b, f, k, h, g ]). 2.007/2.007 After inverse_order: (no changes). 2.007/2.007 Unfolding symbols: (none). 2.007/2.007 2.007/2.007 Auto_inference settings: 2.007/2.007 % set(neg_binary_resolution). % (HNE depth_diff=-3) 2.007/2.007 % clear(ordered_res). % (HNE depth_diff=-3) 2.007/2.007 % set(ur_resolution). % (HNE depth_diff=-3) 2.007/2.007 % set(ur_resolution) -> set(pos_ur_resolution). 2.007/2.007 % set(ur_resolution) -> set(neg_ur_resolution). 2.007/2.007 2.007/2.007 Auto_process settings: (no changes). 2.007/2.007 2.007/2.007 kept: 8 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(1)]. 2.007/2.007 kept: 9 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(2)]. 2.007/2.007 kept: 10 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(3)]. 2.007/2.007 kept: 11 -->_s0(x,y) | ->_s0(k(x),k(y)) # label(congruence). [clausify(4)]. 2.007/2.007 kept: 12 ->_s0(a,b) # label(replacement). [assumption]. 2.007/2.007 kept: 13 ->_s0(c,k(f(a))) # label(replacement). [assumption]. 2.007/2.007 kept: 14 ->_s0(c,k(g(b))) # label(replacement). [assumption]. 2.007/2.007 kept: 15 -->*_s0(h(f(x)),k(g(b))) | ->_s0(f(x),g(x)) # label(replacement). [clausify(5)]. 2.007/2.007 kept: 16 ->_s0(h(f(a)),c) # label(replacement). [assumption]. 2.007/2.007 kept: 17 ->_s0(h(x),k(x)) # label(replacement). [assumption]. 2.007/2.007 kept: 18 ->*_s0(x,x) # label(reflexivity). [assumption]. 2.007/2.007 kept: 19 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(6)]. 2.007/2.007 kept: 20 -->*_s0(h(f(x)),k(g(b))) # label(goal) # answer(goal). [deny(7)]. 2.007/2.007 2.007/2.007 ============================== end of process initial clauses ======== 2.007/2.007 2.007/2.007 ============================== CLAUSES FOR SEARCH ==================== 2.007/2.007 2.007/2.007 % Clauses after input processing: 2.007/2.007 2.007/2.007 formulas(usable). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(sos). 2.007/2.007 8 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(1)]. 2.007/2.007 9 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(2)]. 2.007/2.007 10 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(3)]. 2.007/2.007 11 -->_s0(x,y) | ->_s0(k(x),k(y)) # label(congruence). [clausify(4)]. 2.007/2.007 12 ->_s0(a,b) # label(replacement). [assumption]. 2.007/2.007 13 ->_s0(c,k(f(a))) # label(replacement). [assumption]. 2.007/2.007 14 ->_s0(c,k(g(b))) # label(replacement). [assumption]. 2.007/2.007 16 ->_s0(h(f(a)),c) # label(replacement). [assumption]. 2.007/2.007 17 ->_s0(h(x),k(x)) # label(replacement). [assumption]. 2.007/2.007 18 ->*_s0(x,x) # label(reflexivity). [assumption]. 2.007/2.007 19 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(6)]. 2.007/2.007 20 -->*_s0(h(f(x)),k(g(b))) # label(goal) # answer(goal). [deny(7)]. 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(demodulators). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 ============================== end of clauses for search ============= 2.007/2.007 2.007/2.007 ============================== SEARCH ================================ 2.007/2.007 2.007/2.007 % Starting search at 0.00 seconds. 2.007/2.007 2.007/2.007 given #1 (I,wt=8): 8 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(1)]. 2.007/2.007 2.007/2.007 given #2 (I,wt=8): 9 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(2)]. 2.007/2.007 2.007/2.007 given #3 (I,wt=8): 10 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(3)]. 2.007/2.007 2.007/2.007 given #4 (I,wt=8): 11 -->_s0(x,y) | ->_s0(k(x),k(y)) # label(congruence). [clausify(4)]. 2.007/2.007 2.007/2.007 given #5 (I,wt=3): 12 ->_s0(a,b) # label(replacement). [assumption]. 2.007/2.007 2.007/2.007 given #6 (I,wt=5): 13 ->_s0(c,k(f(a))) # label(replacement). [assumption]. 2.007/2.007 2.007/2.007 given #7 (I,wt=5): 14 ->_s0(c,k(g(b))) # label(replacement). [assumption]. 2.007/2.007 2.007/2.007 given #8 (I,wt=5): 16 ->_s0(h(f(a)),c) # label(replacement). [assumption]. 2.007/2.007 2.007/2.007 given #9 (I,wt=5): 17 ->_s0(h(x),k(x)) # label(replacement). [assumption]. 2.007/2.007 2.007/2.007 given #10 (I,wt=3): 18 ->*_s0(x,x) # label(reflexivity). [assumption]. 2.007/2.007 2.007/2.007 given #11 (I,wt=9): 19 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(6)]. 2.007/2.007 2.007/2.007 given #12 (I,wt=7): 20 -->*_s0(h(f(x)),k(g(b))) # label(goal) # answer(goal). [deny(7)]. 2.007/2.007 2.007/2.007 ============================== PROOF ================================= 2.007/2.007 2.007/2.007 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 2.007/2.007 % Length of proof is 10. 2.007/2.007 % Level of proof is 3. 2.007/2.007 % Maximum clause weight is 9.000. 2.007/2.007 % Given clauses 12. 2.007/2.007 2.007/2.007 6 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 2.007/2.007 7 (exists x3 ->*_s0(h(f(x3)),k(g(b)))) # label(goal) # label(non_clause) # label(goal). [goal]. 2.007/2.007 14 ->_s0(c,k(g(b))) # label(replacement). [assumption]. 2.007/2.007 16 ->_s0(h(f(a)),c) # label(replacement). [assumption]. 2.007/2.007 18 ->*_s0(x,x) # label(reflexivity). [assumption]. 2.007/2.007 19 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(6)]. 2.007/2.007 20 -->*_s0(h(f(x)),k(g(b))) # label(goal) # answer(goal). [deny(7)]. 2.007/2.007 43 ->*_s0(c,k(g(b))). [ur(19,a,14,a,b,18,a)]. 2.007/2.007 49 -->*_s0(c,k(g(b))) # answer(goal). [ur(19,a,16,a,c,20,a)]. 2.007/2.007 50 $F # answer(goal). [resolve(49,a,43,a)]. 2.007/2.007 2.007/2.007 ============================== end of proof ========================== 2.007/2.007 2.007/2.007 ============================== STATISTICS ============================ 2.007/2.007 2.007/2.007 Given=12. Generated=42. Kept=42. proofs=1. 2.007/2.007 Usable=12. Sos=25. Demods=0. Limbo=3, Disabled=14. Hints=0. 2.007/2.007 Kept_by_rule=0, Deleted_by_rule=0. 2.007/2.007 Forward_subsumed=0. Back_subsumed=1. 2.007/2.007 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 2.007/2.007 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 2.007/2.007 Demod_attempts=0. Demod_rewrites=0. 2.007/2.007 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 2.007/2.007 Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=8. 2.007/2.007 Megabytes=0.10. 2.007/2.007 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 2.007/2.007 2.007/2.007 ============================== end of statistics ===================== 2.007/2.007 2.007/2.007 ============================== end of search ========================= 2.007/2.007 2.007/2.007 THEOREM PROVED 2.007/2.007 2.007/2.007 Exiting with 1 proof. 2.007/2.007 2.007/2.007 Process 78146 exit (max_proofs) Wed Mar 9 10:20:05 2022 2.007/2.007 2.007/2.007 2.007/2.007 The problem is feasible. 2.007/2.007 2.007/2.007 2.007/2.007 CRule InfChecker Info: 2.007/2.007 h(f(a)) -> c 2.007/2.007 Rule remains 2.007/2.007 Proof: 2.007/2.007 NO_CONDS 2.007/2.007 2.007/2.007 CRule InfChecker Info: 2.007/2.007 h(x) -> k(x) 2.007/2.007 Rule remains 2.007/2.007 Proof: 2.007/2.007 NO_CONDS 2.007/2.007 2.007/2.007 Problem 1: 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 Confluence Problem: 2.007/2.007 (VAR x) 2.007/2.007 (REPLACEMENT-MAP 2.007/2.007 (a) 2.007/2.007 (c) 2.007/2.007 (f 1) 2.007/2.007 (h 1) 2.007/2.007 (b) 2.007/2.007 (fSNonEmpty) 2.007/2.007 (g 1) 2.007/2.007 (k 1) 2.007/2.007 ) 2.007/2.007 (RULES 2.007/2.007 a -> b 2.007/2.007 c -> k(f(a)) 2.007/2.007 c -> k(g(b)) 2.007/2.007 f(x) -> g(x) | h(f(x)) ->* k(g(b)) 2.007/2.007 h(f(a)) -> c 2.007/2.007 h(x) -> k(x) 2.007/2.007 ) 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 2.007/2.007 Critical Pairs Processor: 2.007/2.007 -> Rules: 2.007/2.007 a -> b 2.007/2.007 c -> k(f(a)) 2.007/2.007 c -> k(g(b)) 2.007/2.007 f(x) -> g(x) | h(f(x)) ->* k(g(b)) 2.007/2.007 h(f(a)) -> c 2.007/2.007 h(x) -> k(x) 2.007/2.007 -> Vars: 2.007/2.007 "x" 2.007/2.007 2.007/2.007 -> Rlps: 2.007/2.007 crule: a -> b, id: 1, possubterms: a-> [] 2.007/2.007 crule: c -> k(f(a)), id: 2, possubterms: c-> [] 2.007/2.007 crule: c -> k(g(b)), id: 3, possubterms: c-> [] 2.007/2.007 crule: f(x) -> g(x) | h(f(x)) ->* k(g(b)), id: 4, possubterms: f(x)-> [] 2.007/2.007 crule: h(f(a)) -> c, id: 5, possubterms: h(f(a))-> [], f(a)-> [1], a-> [1,1] 2.007/2.007 crule: h(x) -> k(x), id: 6, possubterms: h(x)-> [] 2.007/2.007 2.007/2.007 -> Unifications: 2.007/2.007 R3 unifies with R2 at p: [], l: c, lp: c, conds: {}, sig: {}, l': c, r: k(g(b)), r': k(f(a)) 2.007/2.007 R5 unifies with R4 at p: [1], l: h(f(a)), lp: f(a), conds: {h(f(x)) ->* k(g(b))}, sig: {x -> a}, l': f(x), r: c, r': g(x) 2.007/2.007 R5 unifies with R1 at p: [1,1], l: h(f(a)), lp: a, conds: {}, sig: {}, l': a, r: c, r': b 2.007/2.007 R6 unifies with R5 at p: [], l: h(x), lp: h(x), conds: {}, sig: {x -> f(a)}, l': h(f(a)), r: k(x), r': c 2.007/2.007 2.007/2.007 -> Critical pairs info: 2.007/2.007 => Not trivial, Overlay, NW1, N1 2.007/2.007 | h(f(a)) ->* k(g(b)) => Not trivial, Not overlay, NW0, N2 2.007/2.007 => Not trivial, Overlay, NW0, N3 2.007/2.007 => Not trivial, Not overlay, NW0, N4 2.007/2.007 2.007/2.007 -> Problem conclusions: 2.007/2.007 Left linear, Right linear, Linear 2.007/2.007 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 2.007/2.007 CTRS Type: 1 2.007/2.007 Deterministic, Strongly deterministic 2.007/2.007 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 2.007/2.007 Maybe right-stable CTRS, Not overlay CTRS 2.007/2.007 Maybe normal CTRS, Maybe almost normal CTRS 2.007/2.007 Maybe terminating CTRS, Maybe operational terminating CTRS, Maybe joinable CCPs 2.007/2.007 Maybe level confluent 2.007/2.007 Maybe confluent 2.007/2.007 2.007/2.007 Problem 1: 2.007/2.007 Clean Infeasible CCPs Processor: 2.007/2.007 Num of CPIs: 4 2.007/2.007 Timeout: 60 2.007/2.007 Timeout for each infeasibility problem: 60 s 2.007/2.007 => Not trivial, Overlay, NW1, N1 2.007/2.007 2.007/2.007 Proof: 2.007/2.007 NO_CONDS 2.007/2.007 2.007/2.007 2.007/2.007 2.007/2.007 | h(f(a)) ->* k(g(b)) => Not trivial, Not overlay, Feasible conditions, NW0, N2 2.007/2.007 (CONDITIONTYPE ORIENTED) 2.007/2.007 (VAR x) 2.007/2.007 (RULES 2.007/2.007 a -> b 2.007/2.007 c -> k(f(a)) 2.007/2.007 c -> k(g(b)) 2.007/2.007 f(x) -> g(x) | h(f(x)) ->* k(g(b)) 2.007/2.007 h(f(a)) -> c 2.007/2.007 h(x) -> k(x)) 2.007/2.007 (CONDITION h(f(a)) ->* k(g(b))) 2.007/2.007 2.007/2.007 Proof: 2.007/2.007 NO 2.007/2.007 2.007/2.007 Problem 1: 2.007/2.007 2.007/2.007 Infeasibility Problem: 2.007/2.007 [(VAR vNonEmpty x vNonEmpty) 2.007/2.007 (STRATEGY CONTEXTSENSITIVE 2.007/2.007 (a) 2.007/2.007 (c) 2.007/2.007 (f 1) 2.007/2.007 (h 1) 2.007/2.007 (b) 2.007/2.007 (fSNonEmpty) 2.007/2.007 (g 1) 2.007/2.007 (k 1) 2.007/2.007 ) 2.007/2.007 (RULES 2.007/2.007 a -> b 2.007/2.007 c -> k(f(a)) 2.007/2.007 c -> k(g(b)) 2.007/2.007 f(x) -> g(x) | h(f(x)) ->* k(g(b)) 2.007/2.007 h(f(a)) -> c 2.007/2.007 h(x) -> k(x) 2.007/2.007 )] 2.007/2.007 2.007/2.007 Infeasibility Conditions: 2.007/2.007 h(f(a)) ->* k(g(b)) 2.007/2.007 2.007/2.007 Problem 1: 2.007/2.007 2.007/2.007 Obtaining a proof using Prover9: 2.007/2.007 2.007/2.007 -> Prover9 Output: 2.007/2.007 ============================== Prover9 =============================== 2.007/2.007 Prover9 (64) version 2009-11A, November 2009. 2.007/2.007 Process 78377 was started by ubuntu on ubuntu, 2.007/2.007 Wed Mar 9 10:20:06 2022 2.007/2.007 The command was "./prover9 -f /tmp/prover978347-0.in". 2.007/2.007 ============================== end of head =========================== 2.007/2.007 2.007/2.007 ============================== INPUT ================================= 2.007/2.007 2.007/2.007 % Reading from file /tmp/prover978347-0.in 2.007/2.007 2.007/2.007 assign(max_seconds,20). 2.007/2.007 2.007/2.007 formulas(assumptions). 2.007/2.007 ->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence). 2.007/2.007 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence). 2.007/2.007 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence). 2.007/2.007 ->_s0(x1,y) -> ->_s0(k(x1),k(y)) # label(congruence). 2.007/2.007 ->_s0(a,b) # label(replacement). 2.007/2.007 ->_s0(c,k(f(a))) # label(replacement). 2.007/2.007 ->_s0(c,k(g(b))) # label(replacement). 2.007/2.007 ->*_s0(h(f(x1)),k(g(b))) -> ->_s0(f(x1),g(x1)) # label(replacement). 2.007/2.007 ->_s0(h(f(a)),c) # label(replacement). 2.007/2.007 ->_s0(h(x1),k(x1)) # label(replacement). 2.007/2.007 ->*_s0(x,x) # label(reflexivity). 2.007/2.007 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(goals). 2.007/2.007 ->*_s0(h(f(a)),k(g(b))) # label(goal). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 ============================== end of input ========================== 2.007/2.007 2.007/2.007 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 2.007/2.007 2.007/2.007 % Formulas that are not ordinary clauses: 2.007/2.007 1 ->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 2.007/2.007 2 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 2.007/2.007 3 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 2.007/2.007 4 ->_s0(x1,y) -> ->_s0(k(x1),k(y)) # label(congruence) # label(non_clause). [assumption]. 2.007/2.007 5 ->*_s0(h(f(x1)),k(g(b))) -> ->_s0(f(x1),g(x1)) # label(replacement) # label(non_clause). [assumption]. 2.007/2.007 6 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 2.007/2.007 7 ->*_s0(h(f(a)),k(g(b))) # label(goal) # label(non_clause) # label(goal). [goal]. 2.007/2.007 2.007/2.007 ============================== end of process non-clausal formulas === 2.007/2.007 2.007/2.007 ============================== PROCESS INITIAL CLAUSES =============== 2.007/2.007 2.007/2.007 % Clauses before input processing: 2.007/2.007 2.007/2.007 formulas(usable). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(sos). 2.007/2.007 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(1)]. 2.007/2.007 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(2)]. 2.007/2.007 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(3)]. 2.007/2.007 -->_s0(x,y) | ->_s0(k(x),k(y)) # label(congruence). [clausify(4)]. 2.007/2.007 ->_s0(a,b) # label(replacement). [assumption]. 2.007/2.007 ->_s0(c,k(f(a))) # label(replacement). [assumption]. 2.007/2.007 ->_s0(c,k(g(b))) # label(replacement). [assumption]. 2.007/2.007 -->*_s0(h(f(x)),k(g(b))) | ->_s0(f(x),g(x)) # label(replacement). [clausify(5)]. 2.007/2.007 ->_s0(h(f(a)),c) # label(replacement). [assumption]. 2.007/2.007 ->_s0(h(x),k(x)) # label(replacement). [assumption]. 2.007/2.007 ->*_s0(x,x) # label(reflexivity). [assumption]. 2.007/2.007 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(6)]. 2.007/2.007 -->*_s0(h(f(a)),k(g(b))) # label(goal). [deny(7)]. 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(demodulators). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 ============================== PREDICATE ELIMINATION ================= 2.007/2.007 2.007/2.007 No predicates eliminated. 2.007/2.007 2.007/2.007 ============================== end predicate elimination ============= 2.007/2.007 2.007/2.007 Auto_denials: 2.007/2.007 % copying label goal to answer in negative clause 2.007/2.007 2.007/2.007 Term ordering decisions: 2.007/2.007 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 2.007/2.007 Function symbol precedence: function_order([ a, c, b, f, k, h, g ]). 2.007/2.007 After inverse_order: (no changes). 2.007/2.007 Unfolding symbols: (none). 2.007/2.007 2.007/2.007 Auto_inference settings: 2.007/2.007 % set(neg_binary_resolution). % (HNE depth_diff=-3) 2.007/2.007 % clear(ordered_res). % (HNE depth_diff=-3) 2.007/2.007 % set(ur_resolution). % (HNE depth_diff=-3) 2.007/2.007 % set(ur_resolution) -> set(pos_ur_resolution). 2.007/2.007 % set(ur_resolution) -> set(neg_ur_resolution). 2.007/2.007 2.007/2.007 Auto_process settings: (no changes). 2.007/2.007 2.007/2.007 kept: 8 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(1)]. 2.007/2.007 kept: 9 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(2)]. 2.007/2.007 kept: 10 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(3)]. 2.007/2.007 kept: 11 -->_s0(x,y) | ->_s0(k(x),k(y)) # label(congruence). [clausify(4)]. 2.007/2.007 kept: 12 ->_s0(a,b) # label(replacement). [assumption]. 2.007/2.007 kept: 13 ->_s0(c,k(f(a))) # label(replacement). [assumption]. 2.007/2.007 kept: 14 ->_s0(c,k(g(b))) # label(replacement). [assumption]. 2.007/2.007 kept: 15 -->*_s0(h(f(x)),k(g(b))) | ->_s0(f(x),g(x)) # label(replacement). [clausify(5)]. 2.007/2.007 kept: 16 ->_s0(h(f(a)),c) # label(replacement). [assumption]. 2.007/2.007 kept: 17 ->_s0(h(x),k(x)) # label(replacement). [assumption]. 2.007/2.007 kept: 18 ->*_s0(x,x) # label(reflexivity). [assumption]. 2.007/2.007 kept: 19 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(6)]. 2.007/2.007 kept: 20 -->*_s0(h(f(a)),k(g(b))) # label(goal) # answer(goal). [deny(7)]. 2.007/2.007 2.007/2.007 ============================== end of process initial clauses ======== 2.007/2.007 2.007/2.007 ============================== CLAUSES FOR SEARCH ==================== 2.007/2.007 2.007/2.007 % Clauses after input processing: 2.007/2.007 2.007/2.007 formulas(usable). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(sos). 2.007/2.007 8 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(1)]. 2.007/2.007 9 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(2)]. 2.007/2.007 10 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(3)]. 2.007/2.007 11 -->_s0(x,y) | ->_s0(k(x),k(y)) # label(congruence). [clausify(4)]. 2.007/2.007 12 ->_s0(a,b) # label(replacement). [assumption]. 2.007/2.007 13 ->_s0(c,k(f(a))) # label(replacement). [assumption]. 2.007/2.007 14 ->_s0(c,k(g(b))) # label(replacement). [assumption]. 2.007/2.007 15 -->*_s0(h(f(x)),k(g(b))) | ->_s0(f(x),g(x)) # label(replacement). [clausify(5)]. 2.007/2.007 16 ->_s0(h(f(a)),c) # label(replacement). [assumption]. 2.007/2.007 17 ->_s0(h(x),k(x)) # label(replacement). [assumption]. 2.007/2.007 18 ->*_s0(x,x) # label(reflexivity). [assumption]. 2.007/2.007 19 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(6)]. 2.007/2.007 20 -->*_s0(h(f(a)),k(g(b))) # label(goal) # answer(goal). [deny(7)]. 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(demodulators). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 ============================== end of clauses for search ============= 2.007/2.007 2.007/2.007 ============================== SEARCH ================================ 2.007/2.007 2.007/2.007 % Starting search at 0.01 seconds. 2.007/2.007 2.007/2.007 given #1 (I,wt=8): 8 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(1)]. 2.007/2.007 2.007/2.007 given #2 (I,wt=8): 9 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(2)]. 2.007/2.007 2.007/2.007 given #3 (I,wt=8): 10 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(3)]. 2.007/2.007 2.007/2.007 given #4 (I,wt=8): 11 -->_s0(x,y) | ->_s0(k(x),k(y)) # label(congruence). [clausify(4)]. 2.007/2.007 2.007/2.007 given #5 (I,wt=3): 12 ->_s0(a,b) # label(replacement). [assumption]. 2.007/2.007 2.007/2.007 given #6 (I,wt=5): 13 ->_s0(c,k(f(a))) # label(replacement). [assumption]. 2.007/2.007 2.007/2.007 given #7 (I,wt=5): 14 ->_s0(c,k(g(b))) # label(replacement). [assumption]. 2.007/2.007 2.007/2.007 given #8 (I,wt=12): 15 -->*_s0(h(f(x)),k(g(b))) | ->_s0(f(x),g(x)) # label(replacement). [clausify(5)]. 2.007/2.007 2.007/2.007 given #9 (I,wt=5): 16 ->_s0(h(f(a)),c) # label(replacement). [assumption]. 2.007/2.007 2.007/2.007 given #10 (I,wt=5): 17 ->_s0(h(x),k(x)) # label(replacement). [assumption]. 2.007/2.007 2.007/2.007 given #11 (I,wt=3): 18 ->*_s0(x,x) # label(reflexivity). [assumption]. 2.007/2.007 2.007/2.007 given #12 (I,wt=9): 19 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(6)]. 2.007/2.007 2.007/2.007 given #13 (I,wt=7): 20 -->*_s0(h(f(a)),k(g(b))) # label(goal) # answer(goal). [deny(7)]. 2.007/2.007 2.007/2.007 ============================== PROOF ================================= 2.007/2.007 2.007/2.007 % Proof 1 at 0.01 (+ 0.00) seconds: goal. 2.007/2.007 % Length of proof is 10. 2.007/2.007 % Level of proof is 3. 2.007/2.007 % Maximum clause weight is 9.000. 2.007/2.007 % Given clauses 13. 2.007/2.007 2.007/2.007 6 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 2.007/2.007 7 ->*_s0(h(f(a)),k(g(b))) # label(goal) # label(non_clause) # label(goal). [goal]. 2.007/2.007 14 ->_s0(c,k(g(b))) # label(replacement). [assumption]. 2.007/2.007 16 ->_s0(h(f(a)),c) # label(replacement). [assumption]. 2.007/2.007 18 ->*_s0(x,x) # label(reflexivity). [assumption]. 2.007/2.007 19 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(6)]. 2.007/2.007 20 -->*_s0(h(f(a)),k(g(b))) # label(goal) # answer(goal). [deny(7)]. 2.007/2.007 43 ->*_s0(c,k(g(b))). [ur(19,a,14,a,b,18,a)]. 2.007/2.007 49 -->*_s0(c,k(g(b))) # answer(goal). [ur(19,a,16,a,c,20,a)]. 2.007/2.007 50 $F # answer(goal). [resolve(49,a,43,a)]. 2.007/2.007 2.007/2.007 ============================== end of proof ========================== 2.007/2.007 2.007/2.007 ============================== STATISTICS ============================ 2.007/2.007 2.007/2.007 Given=13. Generated=42. Kept=42. proofs=1. 2.007/2.007 Usable=13. Sos=25. Demods=0. Limbo=3, Disabled=13. Hints=0. 2.007/2.007 Kept_by_rule=0, Deleted_by_rule=0. 2.007/2.007 Forward_subsumed=0. Back_subsumed=0. 2.007/2.007 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 2.007/2.007 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 2.007/2.007 Demod_attempts=0. Demod_rewrites=0. 2.007/2.007 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 2.007/2.007 Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=7. 2.007/2.007 Megabytes=0.10. 2.007/2.007 User_CPU=0.01, System_CPU=0.00, Wall_clock=0. 2.007/2.007 2.007/2.007 ============================== end of statistics ===================== 2.007/2.007 2.007/2.007 ============================== end of search ========================= 2.007/2.007 2.007/2.007 THEOREM PROVED 2.007/2.007 2.007/2.007 Exiting with 1 proof. 2.007/2.007 2.007/2.007 Process 78377 exit (max_proofs) Wed Mar 9 10:20:06 2022 2.007/2.007 2.007/2.007 2.007/2.007 The problem is feasible. 2.007/2.007 2.007/2.007 2.007/2.007 2.007/2.007 2.007/2.007 => Not trivial, Overlay, NW0, N3 2.007/2.007 2.007/2.007 Proof: 2.007/2.007 NO_CONDS 2.007/2.007 2.007/2.007 2.007/2.007 2.007/2.007 => Not trivial, Not overlay, NW0, N4 2.007/2.007 2.007/2.007 Proof: 2.007/2.007 NO_CONDS 2.007/2.007 2.007/2.007 2.007/2.007 2.007/2.007 -> Problem conclusions: 2.007/2.007 Left linear, Right linear, Linear 2.007/2.007 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 2.007/2.007 CTRS Type: 1 2.007/2.007 Deterministic, Strongly deterministic 2.007/2.007 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 2.007/2.007 Maybe right-stable CTRS, Not overlay CTRS 2.007/2.007 Maybe normal CTRS, Maybe almost normal CTRS 2.007/2.007 Maybe terminating CTRS, Maybe operational terminating CTRS, Maybe joinable CCPs 2.007/2.007 Maybe level confluent 2.007/2.007 Maybe confluent 2.007/2.007 2.007/2.007 Resulting CCPs: 2.007/2.007 => Not trivial, Overlay, NW1, N1 2.007/2.007 | h(f(a)) ->* k(g(b)) => Not trivial, Not overlay, Feasible conditions, NW0, N2 2.007/2.007 => Not trivial, Overlay, NW0, N3 2.007/2.007 => Not trivial, Not overlay, NW0, N4 2.007/2.007 2.007/2.007 Problem 1: 2.007/2.007 Underlying TRS Termination Processor: 2.007/2.007 2.007/2.007 Resulting Underlying TRS: 2.007/2.007 (VAR x) 2.007/2.007 (STRATEGY CONTEXTSENSITIVE 2.007/2.007 (a) 2.007/2.007 (c) 2.007/2.007 (f 1) 2.007/2.007 (h 1) 2.007/2.007 (b) 2.007/2.007 (g 1) 2.007/2.007 (k 1) 2.007/2.007 ) 2.007/2.007 (RULES 2.007/2.007 a -> b 2.007/2.007 c -> k(f(a)) 2.007/2.007 c -> k(g(b)) 2.007/2.007 f(x) -> g(x) 2.007/2.007 h(f(a)) -> c 2.007/2.007 h(x) -> k(x) 2.007/2.007 ) 2.007/2.007 Underlying TRS terminating? 2.007/2.007 YES 2.007/2.007 2.007/2.007 Problem 1: 2.007/2.007 2.007/2.007 (VAR vu95NonEmpty x) 2.007/2.007 (RULES 2.007/2.007 a -> b 2.007/2.007 c -> k(f(a)) 2.007/2.007 c -> k(g(b)) 2.007/2.007 f(x) -> g(x) 2.007/2.007 h(f(a)) -> c 2.007/2.007 h(x) -> k(x) 2.007/2.007 ) 2.007/2.007 2.007/2.007 Problem 1: 2.007/2.007 2.007/2.007 Dependency Pairs Processor: 2.007/2.007 -> Pairs: 2.007/2.007 C -> A 2.007/2.007 C -> F(a) 2.007/2.007 H(f(a)) -> C 2.007/2.007 -> Rules: 2.007/2.007 a -> b 2.007/2.007 c -> k(f(a)) 2.007/2.007 c -> k(g(b)) 2.007/2.007 f(x) -> g(x) 2.007/2.007 h(f(a)) -> c 2.007/2.007 h(x) -> k(x) 2.007/2.007 2.007/2.007 Problem 1: 2.007/2.007 2.007/2.007 SCC Processor: 2.007/2.007 -> Pairs: 2.007/2.007 C -> A 2.007/2.007 C -> F(a) 2.007/2.007 H(f(a)) -> C 2.007/2.007 -> Rules: 2.007/2.007 a -> b 2.007/2.007 c -> k(f(a)) 2.007/2.007 c -> k(g(b)) 2.007/2.007 f(x) -> g(x) 2.007/2.007 h(f(a)) -> c 2.007/2.007 h(x) -> k(x) 2.007/2.007 ->Strongly Connected Components: 2.007/2.007 There is no strongly connected component 2.007/2.007 2.007/2.007 The problem is finite. 2.007/2.007 2.007/2.007 2.007/2.007 -> Problem conclusions: 2.007/2.007 Left linear, Right linear, Linear 2.007/2.007 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 2.007/2.007 CTRS Type: 1 2.007/2.007 Deterministic, Strongly deterministic 2.007/2.007 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 2.007/2.007 Maybe right-stable CTRS, Not overlay CTRS 2.007/2.007 Maybe normal CTRS, Maybe almost normal CTRS 2.007/2.007 Terminating CTRS, Maybe operational terminating CTRS, Maybe joinable CCPs 2.007/2.007 Maybe level confluent 2.007/2.007 Maybe confluent 2.007/2.007 2.007/2.007 Problem 1: 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 Confluence Problem: 2.007/2.007 (VAR x) 2.007/2.007 (REPLACEMENT-MAP 2.007/2.007 (a) 2.007/2.007 (c) 2.007/2.007 (f 1) 2.007/2.007 (h 1) 2.007/2.007 (b) 2.007/2.007 (fSNonEmpty) 2.007/2.007 (g 1) 2.007/2.007 (k 1) 2.007/2.007 ) 2.007/2.007 (RULES 2.007/2.007 a -> b 2.007/2.007 c -> k(f(a)) 2.007/2.007 c -> k(g(b)) 2.007/2.007 f(x) -> g(x) | h(f(x)) ->* k(g(b)) 2.007/2.007 h(f(a)) -> c 2.007/2.007 h(x) -> k(x) 2.007/2.007 ) 2.007/2.007 Critical Pairs: 2.007/2.007 => Not trivial, Overlay, NW1, N1 2.007/2.007 | h(f(a)) ->* k(g(b)) => Not trivial, Not overlay, Feasible conditions, NW0, N2 2.007/2.007 => Not trivial, Overlay, NW0, N3 2.007/2.007 => Not trivial, Not overlay, NW0, N4 2.007/2.007 Terminating:YES 2.007/2.007 2.007/2.007 -> Problem conclusions: 2.007/2.007 Left linear, Right linear, Linear 2.007/2.007 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 2.007/2.007 CTRS Type: 1 2.007/2.007 Deterministic, Strongly deterministic 2.007/2.007 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 2.007/2.007 Maybe right-stable CTRS, Not overlay CTRS 2.007/2.007 Maybe normal CTRS, Maybe almost normal CTRS 2.007/2.007 Terminating CTRS, Maybe operational terminating CTRS, Maybe joinable CCPs 2.007/2.007 Maybe level confluent 2.007/2.007 Maybe confluent 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 2.007/2.007 Right Stable Processor: 2.007/2.007 Right-stable CTRS 2.007/2.007 Justification: 2.007/2.007 2.007/2.007 -> Term right-stability conditions: 2.007/2.007 Term: k(g(b)) 2.007/2.007 Right-stable term 2.007/2.007 Linear constructor form 2.007/2.007 Don't know if term is a ground normal form (not needed) 2.007/2.007 Right-stability condition achieved 2.007/2.007 A call to InfChecker wasn't needed 2.007/2.007 2.007/2.007 -> Problem conclusions: 2.007/2.007 Left linear, Right linear, Linear 2.007/2.007 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 2.007/2.007 CTRS Type: 1 2.007/2.007 Deterministic, Strongly deterministic 2.007/2.007 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 2.007/2.007 Right-stable CTRS, Not overlay CTRS 2.007/2.007 Maybe normal CTRS, Almost normal CTRS 2.007/2.007 Terminating CTRS, Maybe operational terminating CTRS, Maybe joinable CCPs 2.007/2.007 Maybe level confluent 2.007/2.007 Maybe confluent 2.007/2.007 2.007/2.007 Problem 1: 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 Confluence Problem: 2.007/2.007 (VAR x) 2.007/2.007 (REPLACEMENT-MAP 2.007/2.007 (a) 2.007/2.007 (c) 2.007/2.007 (f 1) 2.007/2.007 (h 1) 2.007/2.007 (b) 2.007/2.007 (fSNonEmpty) 2.007/2.007 (g 1) 2.007/2.007 (k 1) 2.007/2.007 ) 2.007/2.007 (RULES 2.007/2.007 a -> b 2.007/2.007 c -> k(f(a)) 2.007/2.007 c -> k(g(b)) 2.007/2.007 f(x) -> g(x) | h(f(x)) ->* k(g(b)) 2.007/2.007 h(f(a)) -> c 2.007/2.007 h(x) -> k(x) 2.007/2.007 ) 2.007/2.007 Critical Pairs: 2.007/2.007 => Not trivial, Overlay, NW1, N1 2.007/2.007 | h(f(a)) ->* k(g(b)) => Not trivial, Not overlay, Feasible conditions, NW0, N2 2.007/2.007 => Not trivial, Overlay, NW0, N3 2.007/2.007 => Not trivial, Not overlay, NW0, N4 2.007/2.007 Terminating:YES 2.007/2.007 2.007/2.007 -> Problem conclusions: 2.007/2.007 Left linear, Right linear, Linear 2.007/2.007 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 2.007/2.007 CTRS Type: 1 2.007/2.007 Deterministic, Strongly deterministic 2.007/2.007 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 2.007/2.007 Right-stable CTRS, Not overlay CTRS 2.007/2.007 Maybe normal CTRS, Almost normal CTRS 2.007/2.007 Terminating CTRS, Maybe operational terminating CTRS, Maybe joinable CCPs 2.007/2.007 Maybe level confluent 2.007/2.007 Maybe confluent 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 2.007/2.007 Normal RConds Processor: 2.007/2.007 YES 2.007/2.007 2.007/2.007 Problem 1: 2.007/2.007 2.007/2.007 Infeasibility Problem: 2.007/2.007 [(VAR vNonEmpty x vNonEmpty z) 2.007/2.007 (STRATEGY CONTEXTSENSITIVE 2.007/2.007 (a) 2.007/2.007 (c) 2.007/2.007 (f 1) 2.007/2.007 (h 1) 2.007/2.007 (b) 2.007/2.007 (fSNonEmpty) 2.007/2.007 (g 1) 2.007/2.007 (k 1) 2.007/2.007 ) 2.007/2.007 (RULES 2.007/2.007 a -> b 2.007/2.007 c -> k(f(a)) 2.007/2.007 c -> k(g(b)) 2.007/2.007 f(x) -> g(x) | h(f(x)) ->* k(g(b)) 2.007/2.007 h(f(a)) -> c 2.007/2.007 h(x) -> k(x) 2.007/2.007 )] 2.007/2.007 2.007/2.007 Infeasibility Conditions: 2.007/2.007 k(g(b)) -> z 2.007/2.007 2.007/2.007 Problem 1: 2.007/2.007 2.007/2.007 Obtaining a model using Mace4: 2.007/2.007 2.007/2.007 -> Usable Rules: 2.007/2.007 Empty 2.007/2.007 2.007/2.007 -> Mace4 Output: 2.007/2.007 ============================== Mace4 ================================= 2.007/2.007 Mace4 (64) version 2009-11A, November 2009. 2.007/2.007 Process 78445 was started by ubuntu on ubuntu, 2.007/2.007 Wed Mar 9 10:20:07 2022 2.007/2.007 The command was "./mace4 -c -f /tmp/mace478429-2.in". 2.007/2.007 ============================== end of head =========================== 2.007/2.007 2.007/2.007 ============================== INPUT ================================= 2.007/2.007 2.007/2.007 % Reading from file /tmp/mace478429-2.in 2.007/2.007 2.007/2.007 assign(max_seconds,13). 2.007/2.007 2.007/2.007 formulas(assumptions). 2.007/2.007 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence). 2.007/2.007 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence). 2.007/2.007 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence). 2.007/2.007 ->(x1,y) -> ->(k(x1),k(y)) # label(congruence). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(goals). 2.007/2.007 (exists x3 ->(k(g(b)),x3)) # label(goal). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 ============================== end of input ========================== 2.007/2.007 2.007/2.007 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 2.007/2.007 2.007/2.007 % Formulas that are not ordinary clauses: 2.007/2.007 1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 2.007/2.007 2 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 2.007/2.007 3 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 2.007/2.007 4 ->(x1,y) -> ->(k(x1),k(y)) # label(congruence) # label(non_clause). [assumption]. 2.007/2.007 5 (exists x3 ->(k(g(b)),x3)) # label(goal) # label(non_clause) # label(goal). [goal]. 2.007/2.007 2.007/2.007 ============================== end of process non-clausal formulas === 2.007/2.007 2.007/2.007 ============================== CLAUSES FOR SEARCH ==================== 2.007/2.007 2.007/2.007 formulas(mace4_clauses). 2.007/2.007 -->(x,y) | ->(f(x),f(y)) # label(congruence). 2.007/2.007 -->(x,y) | ->(h(x),h(y)) # label(congruence). 2.007/2.007 -->(x,y) | ->(g(x),g(y)) # label(congruence). 2.007/2.007 -->(x,y) | ->(k(x),k(y)) # label(congruence). 2.007/2.007 -->(k(g(b)),x) # label(goal). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 ============================== end of clauses for search ============= 2.007/2.007 2.007/2.007 % There are no natural numbers in the input. 2.007/2.007 2.007/2.007 ============================== DOMAIN SIZE 2 ========================= 2.007/2.007 2.007/2.007 ============================== MODEL ================================= 2.007/2.007 2.007/2.007 interpretation( 2, [number=1, seconds=0], [ 2.007/2.007 2.007/2.007 function(b, [ 0 ]), 2.007/2.007 2.007/2.007 function(f(_), [ 0, 0 ]), 2.007/2.007 2.007/2.007 function(h(_), [ 0, 0 ]), 2.007/2.007 2.007/2.007 function(g(_), [ 0, 0 ]), 2.007/2.007 2.007/2.007 function(k(_), [ 0, 0 ]), 2.007/2.007 2.007/2.007 relation(->(_,_), [ 2.007/2.007 0, 0, 2.007/2.007 0, 0 ]) 2.007/2.007 ]). 2.007/2.007 2.007/2.007 ============================== end of model ========================== 2.007/2.007 2.007/2.007 ============================== STATISTICS ============================ 2.007/2.007 2.007/2.007 For domain size 2. 2.007/2.007 2.007/2.007 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 2.007/2.007 Ground clauses: seen=18, kept=18. 2.007/2.007 Selections=9, assignments=9, propagations=4, current_models=1. 2.007/2.007 Rewrite_terms=38, rewrite_bools=24, indexes=9. 2.007/2.007 Rules_from_neg_clauses=0, cross_offs=0. 2.007/2.007 2.007/2.007 ============================== end of statistics ===================== 2.007/2.007 2.007/2.007 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 2.007/2.007 2.007/2.007 Exiting with 1 model. 2.007/2.007 2.007/2.007 Process 78445 exit (max_models) Wed Mar 9 10:20:07 2022 2.007/2.007 The process finished Wed Mar 9 10:20:07 2022 2.007/2.007 2.007/2.007 2.007/2.007 Mace4 cooked interpretation: 2.007/2.007 2.007/2.007 2.007/2.007 2.007/2.007 The problem is infeasible. 2.007/2.007 2.007/2.007 2.007/2.007 -> Problem conclusions: 2.007/2.007 Left linear, Right linear, Linear 2.007/2.007 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 2.007/2.007 CTRS Type: 1 2.007/2.007 Deterministic, Strongly deterministic 2.007/2.007 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 2.007/2.007 Right-stable CTRS, Not overlay CTRS 2.007/2.007 Normal CTRS, Almost normal CTRS 2.007/2.007 Terminating CTRS, Maybe operational terminating CTRS, Maybe joinable CCPs 2.007/2.007 Maybe level confluent 2.007/2.007 Maybe confluent 2.007/2.007 2.007/2.007 Problem 1: 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 Confluence Problem: 2.007/2.007 (VAR x) 2.007/2.007 (REPLACEMENT-MAP 2.007/2.007 (a) 2.007/2.007 (c) 2.007/2.007 (f 1) 2.007/2.007 (h 1) 2.007/2.007 (b) 2.007/2.007 (fSNonEmpty) 2.007/2.007 (g 1) 2.007/2.007 (k 1) 2.007/2.007 ) 2.007/2.007 (RULES 2.007/2.007 a -> b 2.007/2.007 c -> k(f(a)) 2.007/2.007 c -> k(g(b)) 2.007/2.007 f(x) -> g(x) | h(f(x)) ->* k(g(b)) 2.007/2.007 h(f(a)) -> c 2.007/2.007 h(x) -> k(x) 2.007/2.007 ) 2.007/2.007 Critical Pairs: 2.007/2.007 => Not trivial, Overlay, NW1, N1 2.007/2.007 | h(f(a)) ->* k(g(b)) => Not trivial, Not overlay, Feasible conditions, NW0, N2 2.007/2.007 => Not trivial, Overlay, NW0, N3 2.007/2.007 => Not trivial, Not overlay, NW0, N4 2.007/2.007 Terminating:YES 2.007/2.007 2.007/2.007 -> Problem conclusions: 2.007/2.007 Left linear, Right linear, Linear 2.007/2.007 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 2.007/2.007 CTRS Type: 1 2.007/2.007 Deterministic, Strongly deterministic 2.007/2.007 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 2.007/2.007 Right-stable CTRS, Not overlay CTRS 2.007/2.007 Normal CTRS, Almost normal CTRS 2.007/2.007 Terminating CTRS, Maybe operational terminating CTRS, Maybe joinable CCPs 2.007/2.007 Maybe level confluent 2.007/2.007 Maybe confluent 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 2.007/2.007 Conditional Critical Pairs Distributor Processor 2.007/2.007 2.007/2.007 2.007/2.007 The problem is decomposed in 4 subproblems. 2.007/2.007 2.007/2.007 Problem 1.1: 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 Confluence Problem: 2.007/2.007 (VAR x) 2.007/2.007 (REPLACEMENT-MAP 2.007/2.007 (a) 2.007/2.007 (c) 2.007/2.007 (f 1) 2.007/2.007 (h 1) 2.007/2.007 (b) 2.007/2.007 (fSNonEmpty) 2.007/2.007 (g 1) 2.007/2.007 (k 1) 2.007/2.007 ) 2.007/2.007 (RULES 2.007/2.007 a -> b 2.007/2.007 c -> k(f(a)) 2.007/2.007 c -> k(g(b)) 2.007/2.007 f(x) -> g(x) | h(f(x)) ->* k(g(b)) 2.007/2.007 h(f(a)) -> c 2.007/2.007 h(x) -> k(x) 2.007/2.007 ) 2.007/2.007 Critical Pairs: 2.007/2.007 => Not trivial, Overlay, NW1, N1 2.007/2.007 Terminating:YES 2.007/2.007 2.007/2.007 -> Problem conclusions: 2.007/2.007 Left linear, Right linear, Linear 2.007/2.007 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 2.007/2.007 CTRS Type: 1 2.007/2.007 Deterministic, Strongly deterministic 2.007/2.007 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 2.007/2.007 Right-stable CTRS, Not overlay CTRS 2.007/2.007 Normal CTRS, Almost normal CTRS 2.007/2.007 Terminating CTRS, Maybe operational terminating CTRS, Maybe joinable CCPs 2.007/2.007 Maybe level confluent 2.007/2.007 Maybe confluent 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 2.007/2.007 Prover9 CCP Convergence Checker Processor: 2.007/2.007 Proof: 2.007/2.007 ============================== Prover9 =============================== 2.007/2.007 Prover9 (64) version 2009-11A, November 2009. 2.007/2.007 Process 78457 was started by ubuntu on ubuntu, 2.007/2.007 Wed Mar 9 10:20:07 2022 2.007/2.007 The command was "./prover9 -t 60 -f /tmp/prover978097-36.in". 2.007/2.007 ============================== end of head =========================== 2.007/2.007 2.007/2.007 ============================== INPUT ================================= 2.007/2.007 2.007/2.007 % Reading from file /tmp/prover978097-36.in 2.007/2.007 2.007/2.007 2.007/2.007 formulas(sos). 2.007/2.007 reds(x,x). 2.007/2.007 red(x,y) & reds(y,z) -> reds(x,z). 2.007/2.007 red(x,y) -> red(f(x),f(y)). 2.007/2.007 red(x,y) -> red(h(x),h(y)). 2.007/2.007 red(x,y) -> red(g(x),g(y)). 2.007/2.007 red(x,y) -> red(k(x),k(y)). 2.007/2.007 red(a,b). 2.007/2.007 red(c,k(f(a))). 2.007/2.007 red(c,k(g(b))). 2.007/2.007 (all x (reds(h(f(x)),k(g(b))) -> red(f(x),g(x)))). 2.007/2.007 red(h(f(a)),c). 2.007/2.007 (all x red(h(x),k(x))). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(goals). 2.007/2.007 (exists z (reds(k(f(a)),z) & reds(k(g(b)),z))). 2.007/2.007 end_of_list. 2.007/2.007 assign(max_megs,-1). 2.007/2.007 set(quiet). 2.007/2.007 2.007/2.007 ============================== end of input ========================== 2.007/2.007 2.007/2.007 % From the command line: assign(max_seconds, 60). 2.007/2.007 2.007/2.007 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 2.007/2.007 2.007/2.007 % Formulas that are not ordinary clauses: 2.007/2.007 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 2.007/2.007 2 red(x,y) -> red(f(x),f(y)) # label(non_clause). [assumption]. 2.007/2.007 3 red(x,y) -> red(h(x),h(y)) # label(non_clause). [assumption]. 2.007/2.007 4 red(x,y) -> red(g(x),g(y)) # label(non_clause). [assumption]. 2.007/2.007 5 red(x,y) -> red(k(x),k(y)) # label(non_clause). [assumption]. 2.007/2.007 6 (all x (reds(h(f(x)),k(g(b))) -> red(f(x),g(x)))) # label(non_clause). [assumption]. 2.007/2.007 7 (all x red(h(x),k(x))) # label(non_clause). [assumption]. 2.007/2.007 8 (exists z (reds(k(f(a)),z) & reds(k(g(b)),z))) # label(non_clause) # label(goal). [goal]. 2.007/2.007 2.007/2.007 ============================== end of process non-clausal formulas === 2.007/2.007 2.007/2.007 ============================== PROCESS INITIAL CLAUSES =============== 2.007/2.007 2.007/2.007 % Clauses before input processing: 2.007/2.007 2.007/2.007 formulas(usable). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(sos). 2.007/2.007 reds(x,x). [assumption]. 2.007/2.007 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 2.007/2.007 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 2.007/2.007 -red(x,y) | red(h(x),h(y)). [clausify(3)]. 2.007/2.007 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 2.007/2.007 -red(x,y) | red(k(x),k(y)). [clausify(5)]. 2.007/2.007 red(a,b). [assumption]. 2.007/2.007 red(c,k(f(a))). [assumption]. 2.007/2.007 red(c,k(g(b))). [assumption]. 2.007/2.007 -reds(h(f(x)),k(g(b))) | red(f(x),g(x)). [clausify(6)]. 2.007/2.007 red(h(f(a)),c). [assumption]. 2.007/2.007 red(h(x),k(x)). [clausify(7)]. 2.007/2.007 -reds(k(f(a)),x) | -reds(k(g(b)),x). [deny(8)]. 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(demodulators). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 ============================== PREDICATE ELIMINATION ================= 2.007/2.007 2.007/2.007 ============================== end predicate elimination ============= 2.007/2.007 2.007/2.007 Auto_denials: (no changes). 2.007/2.007 2.007/2.007 Term ordering decisions: 2.007/2.007 2.007/2.007 kept: 9 reds(x,x). [assumption]. 2.007/2.007 kept: 10 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 2.007/2.007 kept: 11 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 2.007/2.007 kept: 12 -red(x,y) | red(h(x),h(y)). [clausify(3)]. 2.007/2.007 kept: 13 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 2.007/2.007 kept: 14 -red(x,y) | red(k(x),k(y)). [clausify(5)]. 2.007/2.007 kept: 15 red(a,b). [assumption]. 2.007/2.007 kept: 16 red(c,k(f(a))). [assumption]. 2.007/2.007 kept: 17 red(c,k(g(b))). [assumption]. 2.007/2.007 kept: 18 -reds(h(f(x)),k(g(b))) | red(f(x),g(x)). [clausify(6)]. 2.007/2.007 kept: 19 red(h(f(a)),c). [assumption]. 2.007/2.007 kept: 20 red(h(x),k(x)). [clausify(7)]. 2.007/2.007 kept: 21 -reds(k(f(a)),x) | -reds(k(g(b)),x). [deny(8)]. 2.007/2.007 2.007/2.007 ============================== end of process initial clauses ======== 2.007/2.007 2.007/2.007 ============================== CLAUSES FOR SEARCH ==================== 2.007/2.007 2.007/2.007 % Clauses after input processing: 2.007/2.007 2.007/2.007 formulas(usable). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(sos). 2.007/2.007 9 reds(x,x). [assumption]. 2.007/2.007 10 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 2.007/2.007 11 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 2.007/2.007 12 -red(x,y) | red(h(x),h(y)). [clausify(3)]. 2.007/2.007 13 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 2.007/2.007 14 -red(x,y) | red(k(x),k(y)). [clausify(5)]. 2.007/2.007 15 red(a,b). [assumption]. 2.007/2.007 16 red(c,k(f(a))). [assumption]. 2.007/2.007 17 red(c,k(g(b))). [assumption]. 2.007/2.007 18 -reds(h(f(x)),k(g(b))) | red(f(x),g(x)). [clausify(6)]. 2.007/2.007 19 red(h(f(a)),c). [assumption]. 2.007/2.007 20 red(h(x),k(x)). [clausify(7)]. 2.007/2.007 21 -reds(k(f(a)),x) | -reds(k(g(b)),x). [deny(8)]. 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(demodulators). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 ============================== end of clauses for search ============= 2.007/2.007 2.007/2.007 ============================== SEARCH ================================ 2.007/2.007 2.007/2.007 % Starting search at 0.00 seconds. 2.007/2.007 2.007/2.007 given #1 (I,wt=3): 9 reds(x,x). [assumption]. 2.007/2.007 2.007/2.007 given #2 (I,wt=9): 10 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 2.007/2.007 2.007/2.007 given #3 (I,wt=8): 11 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 2.007/2.007 2.007/2.007 given #4 (I,wt=8): 12 -red(x,y) | red(h(x),h(y)). [clausify(3)]. 2.007/2.007 2.007/2.007 given #5 (I,wt=8): 13 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 2.007/2.007 2.007/2.007 given #6 (I,wt=8): 14 -red(x,y) | red(k(x),k(y)). [clausify(5)]. 2.007/2.007 2.007/2.007 given #7 (I,wt=3): 15 red(a,b). [assumption]. 2.007/2.007 2.007/2.007 given #8 (I,wt=5): 16 red(c,k(f(a))). [assumption]. 2.007/2.007 2.007/2.007 given #9 (I,wt=5): 17 red(c,k(g(b))). [assumption]. 2.007/2.007 2.007/2.007 given #10 (I,wt=12): 18 -reds(h(f(x)),k(g(b))) | red(f(x),g(x)). [clausify(6)]. 2.007/2.007 2.007/2.007 given #11 (I,wt=5): 19 red(h(f(a)),c). [assumption]. 2.007/2.007 2.007/2.007 given #12 (I,wt=5): 20 red(h(x),k(x)). [clausify(7)]. 2.007/2.007 2.007/2.007 given #13 (I,wt=10): 21 -reds(k(f(a)),x) | -reds(k(g(b)),x). [deny(8)]. 2.007/2.007 2.007/2.007 given #14 (A,wt=5): 22 red(k(a),k(b)). [ur(14,a,15,a)]. 2.007/2.007 2.007/2.007 given #15 (F,wt=7): 48 -reds(k(g(b)),k(f(a))). [resolve(21,a,9,a)]. 2.007/2.007 2.007/2.007 given #16 (F,wt=7): 50 -reds(k(f(a)),k(g(b))). [resolve(21,b,9,a)]. 2.007/2.007 2.007/2.007 given #17 (F,wt=7): 57 -red(k(g(b)),k(f(a))). [ur(10,b,9,a,c,48,a)]. 2.007/2.007 2.007/2.007 given #18 (F,wt=5): 60 -red(g(b),f(a)). [resolve(57,a,14,b)]. 2.007/2.007 2.007/2.007 given #19 (T,wt=3): 26 reds(a,b). [ur(10,a,15,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #20 (T,wt=5): 23 red(g(a),g(b)). [ur(13,a,15,a)]. 2.007/2.007 2.007/2.007 given #21 (T,wt=5): 24 red(h(a),h(b)). [ur(12,a,15,a)]. 2.007/2.007 2.007/2.007 given #22 (T,wt=5): 25 red(f(a),f(b)). [ur(11,a,15,a)]. 2.007/2.007 2.007/2.007 given #23 (A,wt=7): 27 red(k(c),k(k(f(a)))). [ur(14,a,16,a)]. 2.007/2.007 2.007/2.007 given #24 (F,wt=7): 59 -red(k(f(a)),k(g(b))). [ur(10,b,9,a,c,50,a)]. 2.007/2.007 2.007/2.007 given #25 (F,wt=5): 81 -red(f(a),g(b)). [resolve(59,a,14,b)]. 2.007/2.007 2.007/2.007 given #26 (F,wt=10): 56 -red(k(g(b)),x) | -reds(x,k(f(a))). [resolve(48,a,10,c)]. 2.007/2.007 2.007/2.007 given #27 (F,wt=10): 58 -red(k(f(a)),x) | -reds(x,k(g(b))). [resolve(50,a,10,c)]. 2.007/2.007 2.007/2.007 given #28 (T,wt=5): 31 reds(c,k(f(a))). [ur(10,a,16,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #29 (T,wt=5): 36 reds(c,k(g(b))). [ur(10,a,17,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #30 (T,wt=5): 41 reds(h(f(a)),c). [ur(10,a,19,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #31 (T,wt=5): 46 reds(h(x),k(x)). [ur(10,a,20,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #32 (A,wt=7): 28 red(g(c),g(k(f(a)))). [ur(13,a,16,a)]. 2.007/2.007 2.007/2.007 given #33 (F,wt=5): 86 -red(k(g(b)),c). [resolve(31,a,56,b)]. 2.007/2.007 2.007/2.007 given #34 (F,wt=5): 87 -red(k(f(a)),c). [resolve(36,a,58,b)]. 2.007/2.007 2.007/2.007 given #35 (F,wt=7): 89 -red(k(f(a)),h(g(b))). [resolve(46,a,58,b)]. 2.007/2.007 2.007/2.007 given #36 (F,wt=7): 90 -red(k(g(b)),h(f(a))). [resolve(46,a,56,b)]. 2.007/2.007 2.007/2.007 given #37 (T,wt=5): 55 reds(k(a),k(b)). [ur(10,a,22,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #38 (T,wt=5): 65 reds(g(a),g(b)). [ur(10,a,23,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #39 (T,wt=5): 70 reds(h(a),h(b)). [ur(10,a,24,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #40 (T,wt=5): 75 reds(f(a),f(b)). [ur(10,a,25,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #41 (A,wt=7): 29 red(h(c),h(k(f(a)))). [ur(12,a,16,a)]. 2.007/2.007 2.007/2.007 given #42 (F,wt=10): 82 -reds(k(x),k(f(a))) | -red(g(b),x). [resolve(56,a,14,b)]. 2.007/2.007 2.007/2.007 given #43 (F,wt=10): 84 -reds(k(x),k(g(b))) | -red(f(a),x). [resolve(58,a,14,b)]. 2.007/2.007 2.007/2.007 given #44 (F,wt=7): 106 -reds(k(f(b)),k(g(b))). [resolve(84,b,25,a)]. 2.007/2.007 2.007/2.007 given #45 (F,wt=5): 111 -red(k(f(b)),c). [ur(10,b,36,a,c,106,a)]. 2.007/2.007 2.007/2.007 given #46 (T,wt=5): 91 reds(h(a),k(b)). [ur(10,a,24,a,b,46,a)]. 2.007/2.007 2.007/2.007 given #47 (T,wt=7): 30 red(f(c),f(k(f(a)))). [ur(11,a,16,a)]. 2.007/2.007 2.007/2.007 given #48 (T,wt=7): 32 red(k(c),k(k(g(b)))). [ur(14,a,17,a)]. 2.007/2.007 2.007/2.007 given #49 (T,wt=7): 33 red(g(c),g(k(g(b)))). [ur(13,a,17,a)]. 2.007/2.007 2.007/2.007 given #50 (A,wt=7): 34 red(h(c),h(k(g(b)))). [ur(12,a,17,a)]. 2.007/2.007 2.007/2.007 given #51 (F,wt=7): 107 -reds(k(g(a)),k(g(b))). [resolve(84,b,18,b),unit_del(b,88)]. 2.007/2.007 2.007/2.007 ============================== PROOF ================================= 2.007/2.007 2.007/2.007 % Proof 1 at 0.01 (+ 0.00) seconds. 2.007/2.007 % Length of proof is 23. 2.007/2.007 % Level of proof is 6. 2.007/2.007 % Maximum clause weight is 12.000. 2.007/2.007 % Given clauses 51. 2.007/2.007 2.007/2.007 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 2.007/2.007 4 red(x,y) -> red(g(x),g(y)) # label(non_clause). [assumption]. 2.007/2.007 5 red(x,y) -> red(k(x),k(y)) # label(non_clause). [assumption]. 2.007/2.007 6 (all x (reds(h(f(x)),k(g(b))) -> red(f(x),g(x)))) # label(non_clause). [assumption]. 2.007/2.007 8 (exists z (reds(k(f(a)),z) & reds(k(g(b)),z))) # label(non_clause) # label(goal). [goal]. 2.007/2.007 9 reds(x,x). [assumption]. 2.007/2.007 10 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 2.007/2.007 13 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 2.007/2.007 14 -red(x,y) | red(k(x),k(y)). [clausify(5)]. 2.007/2.007 15 red(a,b). [assumption]. 2.007/2.007 17 red(c,k(g(b))). [assumption]. 2.007/2.007 18 -reds(h(f(x)),k(g(b))) | red(f(x),g(x)). [clausify(6)]. 2.007/2.007 19 red(h(f(a)),c). [assumption]. 2.007/2.007 21 -reds(k(f(a)),x) | -reds(k(g(b)),x). [deny(8)]. 2.007/2.007 23 red(g(a),g(b)). [ur(13,a,15,a)]. 2.007/2.007 36 reds(c,k(g(b))). [ur(10,a,17,a,b,9,a)]. 2.007/2.007 50 -reds(k(f(a)),k(g(b))). [resolve(21,b,9,a)]. 2.007/2.007 58 -red(k(f(a)),x) | -reds(x,k(g(b))). [resolve(50,a,10,c)]. 2.007/2.007 61 red(k(g(a)),k(g(b))). [ur(14,a,23,a)]. 2.007/2.007 84 -reds(k(x),k(g(b))) | -red(f(a),x). [resolve(58,a,14,b)]. 2.007/2.007 88 reds(h(f(a)),k(g(b))). [ur(10,a,19,a,b,36,a)]. 2.007/2.007 107 -reds(k(g(a)),k(g(b))). [resolve(84,b,18,b),unit_del(b,88)]. 2.007/2.007 137 $F. [ur(10,b,9,a,c,107,a),unit_del(a,61)]. 2.007/2.007 2.007/2.007 ============================== end of proof ========================== 2.007/2.007 2.007/2.007 ============================== STATISTICS ============================ 2.007/2.007 2.007/2.007 Given=51. Generated=152. Kept=128. proofs=1. 2.007/2.007 Usable=51. Sos=74. Demods=0. Limbo=3, Disabled=13. Hints=0. 2.007/2.007 Kept_by_rule=0, Deleted_by_rule=0. 2.007/2.007 Forward_subsumed=23. Back_subsumed=0. 2.007/2.007 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 2.007/2.007 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 2.007/2.007 Demod_attempts=0. Demod_rewrites=0. 2.007/2.007 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 2.007/2.007 Nonunit_fsub_feature_tests=14. Nonunit_bsub_feature_tests=78. 2.007/2.007 Megabytes=0.23. 2.007/2.007 User_CPU=0.01, System_CPU=0.00, Wall_clock=0. 2.007/2.007 2.007/2.007 ============================== end of statistics ===================== 2.007/2.007 2.007/2.007 ============================== end of search ========================= 2.007/2.007 2.007/2.007 THEOREM PROVED 2.007/2.007 2.007/2.007 Exiting with 1 proof. 2.007/2.007 2.007/2.007 Process 78457 exit (max_proofs) Wed Mar 9 10:20:07 2022 2.007/2.007 2.007/2.007 2.007/2.007 The problem is joinable. 2.007/2.007 2.007/2.007 Problem 1.2: 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 Confluence Problem: 2.007/2.007 (VAR x) 2.007/2.007 (REPLACEMENT-MAP 2.007/2.007 (a) 2.007/2.007 (c) 2.007/2.007 (f 1) 2.007/2.007 (h 1) 2.007/2.007 (b) 2.007/2.007 (fSNonEmpty) 2.007/2.007 (g 1) 2.007/2.007 (k 1) 2.007/2.007 ) 2.007/2.007 (RULES 2.007/2.007 a -> b 2.007/2.007 c -> k(f(a)) 2.007/2.007 c -> k(g(b)) 2.007/2.007 f(x) -> g(x) | h(f(x)) ->* k(g(b)) 2.007/2.007 h(f(a)) -> c 2.007/2.007 h(x) -> k(x) 2.007/2.007 ) 2.007/2.007 Critical Pairs: 2.007/2.007 | h(f(a)) ->* k(g(b)) => Not trivial, Not overlay, Feasible conditions, NW0, N2 2.007/2.007 Terminating:YES 2.007/2.007 2.007/2.007 -> Problem conclusions: 2.007/2.007 Left linear, Right linear, Linear 2.007/2.007 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 2.007/2.007 CTRS Type: 1 2.007/2.007 Deterministic, Strongly deterministic 2.007/2.007 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 2.007/2.007 Right-stable CTRS, Not overlay CTRS 2.007/2.007 Normal CTRS, Almost normal CTRS 2.007/2.007 Terminating CTRS, Maybe operational terminating CTRS, Maybe joinable CCPs 2.007/2.007 Maybe level confluent 2.007/2.007 Maybe confluent 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 2.007/2.007 Prover9 CCP Convergence Checker Processor: 2.007/2.007 Proof: 2.007/2.007 ============================== Prover9 =============================== 2.007/2.007 Prover9 (64) version 2009-11A, November 2009. 2.007/2.007 Process 78462 was started by ubuntu on ubuntu, 2.007/2.007 Wed Mar 9 10:20:07 2022 2.007/2.007 The command was "./prover9 -t 60 -f /tmp/prover978097-38.in". 2.007/2.007 ============================== end of head =========================== 2.007/2.007 2.007/2.007 ============================== INPUT ================================= 2.007/2.007 2.007/2.007 % Reading from file /tmp/prover978097-38.in 2.007/2.007 2.007/2.007 2.007/2.007 formulas(sos). 2.007/2.007 reds(x,x). 2.007/2.007 red(x,y) & reds(y,z) -> reds(x,z). 2.007/2.007 red(x,y) -> red(f(x),f(y)). 2.007/2.007 red(x,y) -> red(h(x),h(y)). 2.007/2.007 red(x,y) -> red(g(x),g(y)). 2.007/2.007 red(x,y) -> red(k(x),k(y)). 2.007/2.007 red(a,b). 2.007/2.007 red(c,k(f(a))). 2.007/2.007 red(c,k(g(b))). 2.007/2.007 (all x (reds(h(f(x)),k(g(b))) -> red(f(x),g(x)))). 2.007/2.007 red(h(f(a)),c). 2.007/2.007 (all x red(h(x),k(x))). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(goals). 2.007/2.007 (exists z exists z1 (reds(h(f(a)),k(g(b))) -> reds(h(g(a)),z) & reds(c,z))). 2.007/2.007 end_of_list. 2.007/2.007 assign(max_megs,-1). 2.007/2.007 set(quiet). 2.007/2.007 2.007/2.007 ============================== end of input ========================== 2.007/2.007 2.007/2.007 % From the command line: assign(max_seconds, 60). 2.007/2.007 2.007/2.007 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 2.007/2.007 2.007/2.007 % Formulas that are not ordinary clauses: 2.007/2.007 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 2.007/2.007 2 red(x,y) -> red(f(x),f(y)) # label(non_clause). [assumption]. 2.007/2.007 3 red(x,y) -> red(h(x),h(y)) # label(non_clause). [assumption]. 2.007/2.007 4 red(x,y) -> red(g(x),g(y)) # label(non_clause). [assumption]. 2.007/2.007 5 red(x,y) -> red(k(x),k(y)) # label(non_clause). [assumption]. 2.007/2.007 6 (all x (reds(h(f(x)),k(g(b))) -> red(f(x),g(x)))) # label(non_clause). [assumption]. 2.007/2.007 7 (all x red(h(x),k(x))) # label(non_clause). [assumption]. 2.007/2.007 8 (exists z exists z1 (reds(h(f(a)),k(g(b))) -> reds(h(g(a)),z) & reds(c,z))) # label(non_clause) # label(goal). [goal]. 2.007/2.007 2.007/2.007 ============================== end of process non-clausal formulas === 2.007/2.007 2.007/2.007 ============================== PROCESS INITIAL CLAUSES =============== 2.007/2.007 2.007/2.007 % Clauses before input processing: 2.007/2.007 2.007/2.007 formulas(usable). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(sos). 2.007/2.007 reds(x,x). [assumption]. 2.007/2.007 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 2.007/2.007 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 2.007/2.007 -red(x,y) | red(h(x),h(y)). [clausify(3)]. 2.007/2.007 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 2.007/2.007 -red(x,y) | red(k(x),k(y)). [clausify(5)]. 2.007/2.007 red(a,b). [assumption]. 2.007/2.007 red(c,k(f(a))). [assumption]. 2.007/2.007 red(c,k(g(b))). [assumption]. 2.007/2.007 -reds(h(f(x)),k(g(b))) | red(f(x),g(x)). [clausify(6)]. 2.007/2.007 red(h(f(a)),c). [assumption]. 2.007/2.007 red(h(x),k(x)). [clausify(7)]. 2.007/2.007 reds(h(f(a)),k(g(b))). [deny(8)]. 2.007/2.007 -reds(h(g(a)),x) | -reds(c,x). [deny(8)]. 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(demodulators). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 ============================== PREDICATE ELIMINATION ================= 2.007/2.007 2.007/2.007 ============================== end predicate elimination ============= 2.007/2.007 2.007/2.007 Auto_denials: (no changes). 2.007/2.007 2.007/2.007 Term ordering decisions: 2.007/2.007 2.007/2.007 kept: 9 reds(x,x). [assumption]. 2.007/2.007 kept: 10 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 2.007/2.007 kept: 11 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 2.007/2.007 kept: 12 -red(x,y) | red(h(x),h(y)). [clausify(3)]. 2.007/2.007 kept: 13 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 2.007/2.007 kept: 14 -red(x,y) | red(k(x),k(y)). [clausify(5)]. 2.007/2.007 kept: 15 red(a,b). [assumption]. 2.007/2.007 kept: 16 red(c,k(f(a))). [assumption]. 2.007/2.007 kept: 17 red(c,k(g(b))). [assumption]. 2.007/2.007 kept: 18 -reds(h(f(x)),k(g(b))) | red(f(x),g(x)). [clausify(6)]. 2.007/2.007 kept: 19 red(h(f(a)),c). [assumption]. 2.007/2.007 kept: 20 red(h(x),k(x)). [clausify(7)]. 2.007/2.007 kept: 21 reds(h(f(a)),k(g(b))). [deny(8)]. 2.007/2.007 kept: 22 -reds(h(g(a)),x) | -reds(c,x). [deny(8)]. 2.007/2.007 2.007/2.007 ============================== end of process initial clauses ======== 2.007/2.007 2.007/2.007 ============================== CLAUSES FOR SEARCH ==================== 2.007/2.007 2.007/2.007 % Clauses after input processing: 2.007/2.007 2.007/2.007 formulas(usable). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(sos). 2.007/2.007 9 reds(x,x). [assumption]. 2.007/2.007 10 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 2.007/2.007 11 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 2.007/2.007 12 -red(x,y) | red(h(x),h(y)). [clausify(3)]. 2.007/2.007 13 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 2.007/2.007 14 -red(x,y) | red(k(x),k(y)). [clausify(5)]. 2.007/2.007 15 red(a,b). [assumption]. 2.007/2.007 16 red(c,k(f(a))). [assumption]. 2.007/2.007 17 red(c,k(g(b))). [assumption]. 2.007/2.007 18 -reds(h(f(x)),k(g(b))) | red(f(x),g(x)). [clausify(6)]. 2.007/2.007 19 red(h(f(a)),c). [assumption]. 2.007/2.007 20 red(h(x),k(x)). [clausify(7)]. 2.007/2.007 21 reds(h(f(a)),k(g(b))). [deny(8)]. 2.007/2.007 22 -reds(h(g(a)),x) | -reds(c,x). [deny(8)]. 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(demodulators). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 ============================== end of clauses for search ============= 2.007/2.007 2.007/2.007 ============================== SEARCH ================================ 2.007/2.007 2.007/2.007 % Starting search at 0.00 seconds. 2.007/2.007 2.007/2.007 given #1 (I,wt=3): 9 reds(x,x). [assumption]. 2.007/2.007 2.007/2.007 given #2 (I,wt=9): 10 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 2.007/2.007 2.007/2.007 given #3 (I,wt=8): 11 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 2.007/2.007 2.007/2.007 given #4 (I,wt=8): 12 -red(x,y) | red(h(x),h(y)). [clausify(3)]. 2.007/2.007 2.007/2.007 given #5 (I,wt=8): 13 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 2.007/2.007 2.007/2.007 given #6 (I,wt=8): 14 -red(x,y) | red(k(x),k(y)). [clausify(5)]. 2.007/2.007 2.007/2.007 given #7 (I,wt=3): 15 red(a,b). [assumption]. 2.007/2.007 2.007/2.007 given #8 (I,wt=5): 16 red(c,k(f(a))). [assumption]. 2.007/2.007 2.007/2.007 given #9 (I,wt=5): 17 red(c,k(g(b))). [assumption]. 2.007/2.007 2.007/2.007 given #10 (I,wt=12): 18 -reds(h(f(x)),k(g(b))) | red(f(x),g(x)). [clausify(6)]. 2.007/2.007 2.007/2.007 given #11 (I,wt=5): 19 red(h(f(a)),c). [assumption]. 2.007/2.007 2.007/2.007 given #12 (I,wt=5): 20 red(h(x),k(x)). [clausify(7)]. 2.007/2.007 2.007/2.007 given #13 (I,wt=7): 21 reds(h(f(a)),k(g(b))). [deny(8)]. 2.007/2.007 2.007/2.007 given #14 (I,wt=8): 22 -reds(h(g(a)),x) | -reds(c,x). [deny(8)]. 2.007/2.007 2.007/2.007 given #15 (A,wt=5): 23 red(k(a),k(b)). [ur(14,a,15,a)]. 2.007/2.007 2.007/2.007 given #16 (F,wt=5): 50 -reds(c,h(g(a))). [resolve(22,a,9,a)]. 2.007/2.007 2.007/2.007 given #17 (F,wt=5): 52 -reds(h(g(a)),c). [resolve(22,b,9,a)]. 2.007/2.007 2.007/2.007 given #18 (F,wt=5): 59 -red(c,h(g(a))). [ur(10,b,9,a,c,50,a)]. 2.007/2.007 2.007/2.007 given #19 (F,wt=5): 63 -red(h(g(a)),c). [ur(10,b,9,a,c,52,a)]. 2.007/2.007 2.007/2.007 given #20 (T,wt=3): 27 reds(a,b). [ur(10,a,15,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #21 (T,wt=5): 24 red(g(a),g(b)). [ur(13,a,15,a)]. 2.007/2.007 2.007/2.007 given #22 (T,wt=5): 25 red(h(a),h(b)). [ur(12,a,15,a)]. 2.007/2.007 2.007/2.007 given #23 (T,wt=5): 26 red(f(a),f(b)). [ur(11,a,15,a)]. 2.007/2.007 2.007/2.007 given #24 (A,wt=7): 28 red(k(c),k(k(f(a)))). [ur(14,a,16,a)]. 2.007/2.007 2.007/2.007 given #25 (F,wt=5): 64 -reds(k(g(a)),c). [ur(10,a,20,a,c,52,a)]. 2.007/2.007 2.007/2.007 given #26 (F,wt=5): 86 -red(k(g(a)),c). [ur(10,b,9,a,c,64,a)]. 2.007/2.007 2.007/2.007 given #27 (F,wt=7): 60 -reds(k(g(b)),h(g(a))). [ur(10,a,17,a,c,50,a)]. 2.007/2.007 2.007/2.007 given #28 (F,wt=7): 61 -reds(k(f(a)),h(g(a))). [ur(10,a,16,a,c,50,a)]. 2.007/2.007 2.007/2.007 given #29 (T,wt=5): 32 reds(c,k(f(a))). [ur(10,a,16,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #30 (T,wt=5): 37 reds(c,k(g(b))). [ur(10,a,17,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #31 (T,wt=5): 42 reds(h(f(a)),c). [ur(10,a,19,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #32 (T,wt=5): 47 reds(h(x),k(x)). [ur(10,a,20,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #33 (A,wt=7): 29 red(g(c),g(k(f(a)))). [ur(13,a,16,a)]. 2.007/2.007 2.007/2.007 given #34 (F,wt=5): 95 -reds(c,k(g(a))). [resolve(47,a,22,a)]. 2.007/2.007 2.007/2.007 given #35 (F,wt=5): 103 -red(c,k(g(a))). [ur(10,b,9,a,c,95,a)]. 2.007/2.007 2.007/2.007 given #36 (F,wt=7): 88 -red(k(g(b)),h(g(a))). [ur(10,b,9,a,c,60,a)]. 2.007/2.007 2.007/2.007 given #37 (F,wt=7): 90 -red(k(f(a)),h(g(a))). [ur(10,b,9,a,c,61,a)]. 2.007/2.007 2.007/2.007 given #38 (T,wt=5): 48 red(f(a),g(a)). [ur(18,a,21,a)]. 2.007/2.007 2.007/2.007 given #39 (T,wt=5): 57 reds(k(a),k(b)). [ur(10,a,23,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #40 (T,wt=5): 69 reds(g(a),g(b)). [ur(10,a,24,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #41 (T,wt=5): 74 reds(h(a),h(b)). [ur(10,a,25,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #42 (A,wt=7): 30 red(h(c),h(k(f(a)))). [ur(12,a,16,a)]. 2.007/2.007 2.007/2.007 given #43 (F,wt=7): 91 -reds(h(g(a)),k(f(a))). [resolve(32,a,22,b)]. 2.007/2.007 2.007/2.007 given #44 (F,wt=7): 92 -reds(h(g(a)),k(g(b))). [resolve(37,a,22,b)]. 2.007/2.007 2.007/2.007 ============================== PROOF ================================= 2.007/2.007 2.007/2.007 % Proof 1 at 0.01 (+ 0.00) seconds. 2.007/2.007 % Length of proof is 19. 2.007/2.007 % Level of proof is 4. 2.007/2.007 % Maximum clause weight is 9.000. 2.007/2.007 % Given clauses 44. 2.007/2.007 2.007/2.007 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 2.007/2.007 3 red(x,y) -> red(h(x),h(y)) # label(non_clause). [assumption]. 2.007/2.007 4 red(x,y) -> red(g(x),g(y)) # label(non_clause). [assumption]. 2.007/2.007 7 (all x red(h(x),k(x))) # label(non_clause). [assumption]. 2.007/2.007 8 (exists z exists z1 (reds(h(f(a)),k(g(b))) -> reds(h(g(a)),z) & reds(c,z))) # label(non_clause) # label(goal). [goal]. 2.007/2.007 9 reds(x,x). [assumption]. 2.007/2.007 10 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 2.007/2.007 12 -red(x,y) | red(h(x),h(y)). [clausify(3)]. 2.007/2.007 13 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 2.007/2.007 15 red(a,b). [assumption]. 2.007/2.007 17 red(c,k(g(b))). [assumption]. 2.007/2.007 20 red(h(x),k(x)). [clausify(7)]. 2.007/2.007 22 -reds(h(g(a)),x) | -reds(c,x). [deny(8)]. 2.007/2.007 24 red(g(a),g(b)). [ur(13,a,15,a)]. 2.007/2.007 37 reds(c,k(g(b))). [ur(10,a,17,a,b,9,a)]. 2.007/2.007 47 reds(h(x),k(x)). [ur(10,a,20,a,b,9,a)]. 2.007/2.007 67 red(h(g(a)),h(g(b))). [ur(12,a,24,a)]. 2.007/2.007 92 -reds(h(g(a)),k(g(b))). [resolve(37,a,22,b)]. 2.007/2.007 122 $F. [ur(10,b,47,a,c,92,a),unit_del(a,67)]. 2.007/2.007 2.007/2.007 ============================== end of proof ========================== 2.007/2.007 2.007/2.007 ============================== STATISTICS ============================ 2.007/2.007 2.007/2.007 Given=44. Generated=125. Kept=113. proofs=1. 2.007/2.007 Usable=44. Sos=68. Demods=0. Limbo=1, Disabled=14. Hints=0. 2.007/2.007 Kept_by_rule=0, Deleted_by_rule=0. 2.007/2.007 Forward_subsumed=11. Back_subsumed=0. 2.007/2.007 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 2.007/2.007 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 2.007/2.007 Demod_attempts=0. Demod_rewrites=0. 2.007/2.007 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 2.007/2.007 Nonunit_fsub_feature_tests=7. Nonunit_bsub_feature_tests=50. 2.007/2.007 Megabytes=0.20. 2.007/2.007 User_CPU=0.01, System_CPU=0.00, Wall_clock=0. 2.007/2.007 2.007/2.007 ============================== end of statistics ===================== 2.007/2.007 2.007/2.007 ============================== end of search ========================= 2.007/2.007 2.007/2.007 THEOREM PROVED 2.007/2.007 2.007/2.007 Exiting with 1 proof. 2.007/2.007 2.007/2.007 Process 78462 exit (max_proofs) Wed Mar 9 10:20:07 2022 2.007/2.007 2.007/2.007 2.007/2.007 The problem is joinable. 2.007/2.007 2.007/2.007 Problem 1.3: 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 Confluence Problem: 2.007/2.007 (VAR x) 2.007/2.007 (REPLACEMENT-MAP 2.007/2.007 (a) 2.007/2.007 (c) 2.007/2.007 (f 1) 2.007/2.007 (h 1) 2.007/2.007 (b) 2.007/2.007 (fSNonEmpty) 2.007/2.007 (g 1) 2.007/2.007 (k 1) 2.007/2.007 ) 2.007/2.007 (RULES 2.007/2.007 a -> b 2.007/2.007 c -> k(f(a)) 2.007/2.007 c -> k(g(b)) 2.007/2.007 f(x) -> g(x) | h(f(x)) ->* k(g(b)) 2.007/2.007 h(f(a)) -> c 2.007/2.007 h(x) -> k(x) 2.007/2.007 ) 2.007/2.007 Critical Pairs: 2.007/2.007 => Not trivial, Overlay, NW0, N3 2.007/2.007 Terminating:YES 2.007/2.007 2.007/2.007 -> Problem conclusions: 2.007/2.007 Left linear, Right linear, Linear 2.007/2.007 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 2.007/2.007 CTRS Type: 1 2.007/2.007 Deterministic, Strongly deterministic 2.007/2.007 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 2.007/2.007 Right-stable CTRS, Not overlay CTRS 2.007/2.007 Normal CTRS, Almost normal CTRS 2.007/2.007 Terminating CTRS, Maybe operational terminating CTRS, Maybe joinable CCPs 2.007/2.007 Maybe level confluent 2.007/2.007 Maybe confluent 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 2.007/2.007 Prover9 CCP Convergence Checker Processor: 2.007/2.007 Proof: 2.007/2.007 ============================== Prover9 =============================== 2.007/2.007 Prover9 (64) version 2009-11A, November 2009. 2.007/2.007 Process 78466 was started by ubuntu on ubuntu, 2.007/2.007 Wed Mar 9 10:20:07 2022 2.007/2.007 The command was "./prover9 -t 60 -f /tmp/prover978097-40.in". 2.007/2.007 ============================== end of head =========================== 2.007/2.007 2.007/2.007 ============================== INPUT ================================= 2.007/2.007 2.007/2.007 % Reading from file /tmp/prover978097-40.in 2.007/2.007 2.007/2.007 2.007/2.007 formulas(sos). 2.007/2.007 reds(x,x). 2.007/2.007 red(x,y) & reds(y,z) -> reds(x,z). 2.007/2.007 red(x,y) -> red(f(x),f(y)). 2.007/2.007 red(x,y) -> red(h(x),h(y)). 2.007/2.007 red(x,y) -> red(g(x),g(y)). 2.007/2.007 red(x,y) -> red(k(x),k(y)). 2.007/2.007 red(a,b). 2.007/2.007 red(c,k(f(a))). 2.007/2.007 red(c,k(g(b))). 2.007/2.007 (all x (reds(h(f(x)),k(g(b))) -> red(f(x),g(x)))). 2.007/2.007 red(h(f(a)),c). 2.007/2.007 (all x red(h(x),k(x))). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(goals). 2.007/2.007 (exists z (reds(c,z) & reds(k(f(a)),z))). 2.007/2.007 end_of_list. 2.007/2.007 assign(max_megs,-1). 2.007/2.007 set(quiet). 2.007/2.007 2.007/2.007 ============================== end of input ========================== 2.007/2.007 2.007/2.007 % From the command line: assign(max_seconds, 60). 2.007/2.007 2.007/2.007 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 2.007/2.007 2.007/2.007 % Formulas that are not ordinary clauses: 2.007/2.007 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 2.007/2.007 2 red(x,y) -> red(f(x),f(y)) # label(non_clause). [assumption]. 2.007/2.007 3 red(x,y) -> red(h(x),h(y)) # label(non_clause). [assumption]. 2.007/2.007 4 red(x,y) -> red(g(x),g(y)) # label(non_clause). [assumption]. 2.007/2.007 5 red(x,y) -> red(k(x),k(y)) # label(non_clause). [assumption]. 2.007/2.007 6 (all x (reds(h(f(x)),k(g(b))) -> red(f(x),g(x)))) # label(non_clause). [assumption]. 2.007/2.007 7 (all x red(h(x),k(x))) # label(non_clause). [assumption]. 2.007/2.007 8 (exists z (reds(c,z) & reds(k(f(a)),z))) # label(non_clause) # label(goal). [goal]. 2.007/2.007 2.007/2.007 ============================== end of process non-clausal formulas === 2.007/2.007 2.007/2.007 ============================== PROCESS INITIAL CLAUSES =============== 2.007/2.007 2.007/2.007 % Clauses before input processing: 2.007/2.007 2.007/2.007 formulas(usable). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(sos). 2.007/2.007 reds(x,x). [assumption]. 2.007/2.007 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 2.007/2.007 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 2.007/2.007 -red(x,y) | red(h(x),h(y)). [clausify(3)]. 2.007/2.007 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 2.007/2.007 -red(x,y) | red(k(x),k(y)). [clausify(5)]. 2.007/2.007 red(a,b). [assumption]. 2.007/2.007 red(c,k(f(a))). [assumption]. 2.007/2.007 red(c,k(g(b))). [assumption]. 2.007/2.007 -reds(h(f(x)),k(g(b))) | red(f(x),g(x)). [clausify(6)]. 2.007/2.007 red(h(f(a)),c). [assumption]. 2.007/2.007 red(h(x),k(x)). [clausify(7)]. 2.007/2.007 -reds(c,x) | -reds(k(f(a)),x). [deny(8)]. 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(demodulators). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 ============================== PREDICATE ELIMINATION ================= 2.007/2.007 2.007/2.007 ============================== end predicate elimination ============= 2.007/2.007 2.007/2.007 Auto_denials: (no changes). 2.007/2.007 2.007/2.007 Term ordering decisions: 2.007/2.007 2.007/2.007 kept: 9 reds(x,x). [assumption]. 2.007/2.007 kept: 10 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 2.007/2.007 kept: 11 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 2.007/2.007 kept: 12 -red(x,y) | red(h(x),h(y)). [clausify(3)]. 2.007/2.007 kept: 13 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 2.007/2.007 kept: 14 -red(x,y) | red(k(x),k(y)). [clausify(5)]. 2.007/2.007 kept: 15 red(a,b). [assumption]. 2.007/2.007 kept: 16 red(c,k(f(a))). [assumption]. 2.007/2.007 kept: 17 red(c,k(g(b))). [assumption]. 2.007/2.007 kept: 18 -reds(h(f(x)),k(g(b))) | red(f(x),g(x)). [clausify(6)]. 2.007/2.007 kept: 19 red(h(f(a)),c). [assumption]. 2.007/2.007 kept: 20 red(h(x),k(x)). [clausify(7)]. 2.007/2.007 kept: 21 -reds(c,x) | -reds(k(f(a)),x). [deny(8)]. 2.007/2.007 2.007/2.007 ============================== end of process initial clauses ======== 2.007/2.007 2.007/2.007 ============================== CLAUSES FOR SEARCH ==================== 2.007/2.007 2.007/2.007 % Clauses after input processing: 2.007/2.007 2.007/2.007 formulas(usable). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(sos). 2.007/2.007 9 reds(x,x). [assumption]. 2.007/2.007 10 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 2.007/2.007 11 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 2.007/2.007 12 -red(x,y) | red(h(x),h(y)). [clausify(3)]. 2.007/2.007 13 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 2.007/2.007 14 -red(x,y) | red(k(x),k(y)). [clausify(5)]. 2.007/2.007 15 red(a,b). [assumption]. 2.007/2.007 16 red(c,k(f(a))). [assumption]. 2.007/2.007 17 red(c,k(g(b))). [assumption]. 2.007/2.007 18 -reds(h(f(x)),k(g(b))) | red(f(x),g(x)). [clausify(6)]. 2.007/2.007 19 red(h(f(a)),c). [assumption]. 2.007/2.007 20 red(h(x),k(x)). [clausify(7)]. 2.007/2.007 21 -reds(c,x) | -reds(k(f(a)),x). [deny(8)]. 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(demodulators). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 ============================== end of clauses for search ============= 2.007/2.007 2.007/2.007 ============================== SEARCH ================================ 2.007/2.007 2.007/2.007 % Starting search at 0.00 seconds. 2.007/2.007 2.007/2.007 given #1 (I,wt=3): 9 reds(x,x). [assumption]. 2.007/2.007 2.007/2.007 given #2 (I,wt=9): 10 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 2.007/2.007 2.007/2.007 given #3 (I,wt=8): 11 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 2.007/2.007 2.007/2.007 given #4 (I,wt=8): 12 -red(x,y) | red(h(x),h(y)). [clausify(3)]. 2.007/2.007 2.007/2.007 given #5 (I,wt=8): 13 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 2.007/2.007 2.007/2.007 given #6 (I,wt=8): 14 -red(x,y) | red(k(x),k(y)). [clausify(5)]. 2.007/2.007 2.007/2.007 given #7 (I,wt=3): 15 red(a,b). [assumption]. 2.007/2.007 2.007/2.007 given #8 (I,wt=5): 16 red(c,k(f(a))). [assumption]. 2.007/2.007 2.007/2.007 given #9 (I,wt=5): 17 red(c,k(g(b))). [assumption]. 2.007/2.007 2.007/2.007 given #10 (I,wt=12): 18 -reds(h(f(x)),k(g(b))) | red(f(x),g(x)). [clausify(6)]. 2.007/2.007 2.007/2.007 given #11 (I,wt=5): 19 red(h(f(a)),c). [assumption]. 2.007/2.007 2.007/2.007 given #12 (I,wt=5): 20 red(h(x),k(x)). [clausify(7)]. 2.007/2.007 2.007/2.007 given #13 (I,wt=8): 21 -reds(c,x) | -reds(k(f(a)),x). [deny(8)]. 2.007/2.007 2.007/2.007 ============================== PROOF ================================= 2.007/2.007 2.007/2.007 % Proof 1 at 0.01 (+ 0.00) seconds. 2.007/2.007 % Length of proof is 8. 2.007/2.007 % Level of proof is 3. 2.007/2.007 % Maximum clause weight is 9.000. 2.007/2.007 % Given clauses 13. 2.007/2.007 2.007/2.007 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 2.007/2.007 8 (exists z (reds(c,z) & reds(k(f(a)),z))) # label(non_clause) # label(goal). [goal]. 2.007/2.007 9 reds(x,x). [assumption]. 2.007/2.007 10 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 2.007/2.007 16 red(c,k(f(a))). [assumption]. 2.007/2.007 21 -reds(c,x) | -reds(k(f(a)),x). [deny(8)]. 2.007/2.007 31 reds(c,k(f(a))). [ur(10,a,16,a,b,9,a)]. 2.007/2.007 50 $F. [resolve(21,b,9,a),unit_del(a,31)]. 2.007/2.007 2.007/2.007 ============================== end of proof ========================== 2.007/2.007 2.007/2.007 ============================== STATISTICS ============================ 2.007/2.007 2.007/2.007 Given=13. Generated=42. Kept=41. proofs=1. 2.007/2.007 Usable=13. Sos=25. Demods=0. Limbo=3, Disabled=13. Hints=0. 2.007/2.007 Kept_by_rule=0, Deleted_by_rule=0. 2.007/2.007 Forward_subsumed=0. Back_subsumed=0. 2.007/2.007 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 2.007/2.007 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 2.007/2.007 Demod_attempts=0. Demod_rewrites=0. 2.007/2.007 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 2.007/2.007 Nonunit_fsub_feature_tests=3. Nonunit_bsub_feature_tests=8. 2.007/2.007 Megabytes=0.10. 2.007/2.007 User_CPU=0.01, System_CPU=0.00, Wall_clock=0. 2.007/2.007 2.007/2.007 ============================== end of statistics ===================== 2.007/2.007 2.007/2.007 ============================== end of search ========================= 2.007/2.007 2.007/2.007 THEOREM PROVED 2.007/2.007 2.007/2.007 Exiting with 1 proof. 2.007/2.007 2.007/2.007 Process 78466 exit (max_proofs) Wed Mar 9 10:20:07 2022 2.007/2.007 2.007/2.007 2.007/2.007 The problem is joinable. 2.007/2.007 2.007/2.007 Problem 1.4: 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 Confluence Problem: 2.007/2.007 (VAR x) 2.007/2.007 (REPLACEMENT-MAP 2.007/2.007 (a) 2.007/2.007 (c) 2.007/2.007 (f 1) 2.007/2.007 (h 1) 2.007/2.007 (b) 2.007/2.007 (fSNonEmpty) 2.007/2.007 (g 1) 2.007/2.007 (k 1) 2.007/2.007 ) 2.007/2.007 (RULES 2.007/2.007 a -> b 2.007/2.007 c -> k(f(a)) 2.007/2.007 c -> k(g(b)) 2.007/2.007 f(x) -> g(x) | h(f(x)) ->* k(g(b)) 2.007/2.007 h(f(a)) -> c 2.007/2.007 h(x) -> k(x) 2.007/2.007 ) 2.007/2.007 Critical Pairs: 2.007/2.007 => Not trivial, Not overlay, NW0, N4 2.007/2.007 Terminating:YES 2.007/2.007 2.007/2.007 -> Problem conclusions: 2.007/2.007 Left linear, Right linear, Linear 2.007/2.007 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 2.007/2.007 CTRS Type: 1 2.007/2.007 Deterministic, Strongly deterministic 2.007/2.007 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 2.007/2.007 Right-stable CTRS, Not overlay CTRS 2.007/2.007 Normal CTRS, Almost normal CTRS 2.007/2.007 Terminating CTRS, Maybe operational terminating CTRS, Maybe joinable CCPs 2.007/2.007 Maybe level confluent 2.007/2.007 Maybe confluent 2.007/2.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 2.007/2.007 2.007/2.007 Prover9 CCP Convergence Checker Processor: 2.007/2.007 Proof: 2.007/2.007 ============================== Prover9 =============================== 2.007/2.007 Prover9 (64) version 2009-11A, November 2009. 2.007/2.007 Process 78470 was started by ubuntu on ubuntu, 2.007/2.007 Wed Mar 9 10:20:07 2022 2.007/2.007 The command was "./prover9 -t 60 -f /tmp/prover978097-42.in". 2.007/2.007 ============================== end of head =========================== 2.007/2.007 2.007/2.007 ============================== INPUT ================================= 2.007/2.007 2.007/2.007 % Reading from file /tmp/prover978097-42.in 2.007/2.007 2.007/2.007 2.007/2.007 formulas(sos). 2.007/2.007 reds(x,x). 2.007/2.007 red(x,y) & reds(y,z) -> reds(x,z). 2.007/2.007 red(x,y) -> red(f(x),f(y)). 2.007/2.007 red(x,y) -> red(h(x),h(y)). 2.007/2.007 red(x,y) -> red(g(x),g(y)). 2.007/2.007 red(x,y) -> red(k(x),k(y)). 2.007/2.007 red(a,b). 2.007/2.007 red(c,k(f(a))). 2.007/2.007 red(c,k(g(b))). 2.007/2.007 (all x (reds(h(f(x)),k(g(b))) -> red(f(x),g(x)))). 2.007/2.007 red(h(f(a)),c). 2.007/2.007 (all x red(h(x),k(x))). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(goals). 2.007/2.007 (exists z (reds(h(f(b)),z) & reds(c,z))). 2.007/2.007 end_of_list. 2.007/2.007 assign(max_megs,-1). 2.007/2.007 set(quiet). 2.007/2.007 2.007/2.007 ============================== end of input ========================== 2.007/2.007 2.007/2.007 % From the command line: assign(max_seconds, 60). 2.007/2.007 2.007/2.007 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 2.007/2.007 2.007/2.007 % Formulas that are not ordinary clauses: 2.007/2.007 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 2.007/2.007 2 red(x,y) -> red(f(x),f(y)) # label(non_clause). [assumption]. 2.007/2.007 3 red(x,y) -> red(h(x),h(y)) # label(non_clause). [assumption]. 2.007/2.007 4 red(x,y) -> red(g(x),g(y)) # label(non_clause). [assumption]. 2.007/2.007 5 red(x,y) -> red(k(x),k(y)) # label(non_clause). [assumption]. 2.007/2.007 6 (all x (reds(h(f(x)),k(g(b))) -> red(f(x),g(x)))) # label(non_clause). [assumption]. 2.007/2.007 7 (all x red(h(x),k(x))) # label(non_clause). [assumption]. 2.007/2.007 8 (exists z (reds(h(f(b)),z) & reds(c,z))) # label(non_clause) # label(goal). [goal]. 2.007/2.007 2.007/2.007 ============================== end of process non-clausal formulas === 2.007/2.007 2.007/2.007 ============================== PROCESS INITIAL CLAUSES =============== 2.007/2.007 2.007/2.007 % Clauses before input processing: 2.007/2.007 2.007/2.007 formulas(usable). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(sos). 2.007/2.007 reds(x,x). [assumption]. 2.007/2.007 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 2.007/2.007 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 2.007/2.007 -red(x,y) | red(h(x),h(y)). [clausify(3)]. 2.007/2.007 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 2.007/2.007 -red(x,y) | red(k(x),k(y)). [clausify(5)]. 2.007/2.007 red(a,b). [assumption]. 2.007/2.007 red(c,k(f(a))). [assumption]. 2.007/2.007 red(c,k(g(b))). [assumption]. 2.007/2.007 -reds(h(f(x)),k(g(b))) | red(f(x),g(x)). [clausify(6)]. 2.007/2.007 red(h(f(a)),c). [assumption]. 2.007/2.007 red(h(x),k(x)). [clausify(7)]. 2.007/2.007 -reds(h(f(b)),x) | -reds(c,x). [deny(8)]. 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(demodulators). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 ============================== PREDICATE ELIMINATION ================= 2.007/2.007 2.007/2.007 ============================== end predicate elimination ============= 2.007/2.007 2.007/2.007 Auto_denials: (no changes). 2.007/2.007 2.007/2.007 Term ordering decisions: 2.007/2.007 2.007/2.007 kept: 9 reds(x,x). [assumption]. 2.007/2.007 kept: 10 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 2.007/2.007 kept: 11 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 2.007/2.007 kept: 12 -red(x,y) | red(h(x),h(y)). [clausify(3)]. 2.007/2.007 kept: 13 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 2.007/2.007 kept: 14 -red(x,y) | red(k(x),k(y)). [clausify(5)]. 2.007/2.007 kept: 15 red(a,b). [assumption]. 2.007/2.007 kept: 16 red(c,k(f(a))). [assumption]. 2.007/2.007 kept: 17 red(c,k(g(b))). [assumption]. 2.007/2.007 kept: 18 -reds(h(f(x)),k(g(b))) | red(f(x),g(x)). [clausify(6)]. 2.007/2.007 kept: 19 red(h(f(a)),c). [assumption]. 2.007/2.007 kept: 20 red(h(x),k(x)). [clausify(7)]. 2.007/2.007 kept: 21 -reds(h(f(b)),x) | -reds(c,x). [deny(8)]. 2.007/2.007 2.007/2.007 ============================== end of process initial clauses ======== 2.007/2.007 2.007/2.007 ============================== CLAUSES FOR SEARCH ==================== 2.007/2.007 2.007/2.007 % Clauses after input processing: 2.007/2.007 2.007/2.007 formulas(usable). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(sos). 2.007/2.007 9 reds(x,x). [assumption]. 2.007/2.007 10 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 2.007/2.007 11 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 2.007/2.007 12 -red(x,y) | red(h(x),h(y)). [clausify(3)]. 2.007/2.007 13 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 2.007/2.007 14 -red(x,y) | red(k(x),k(y)). [clausify(5)]. 2.007/2.007 15 red(a,b). [assumption]. 2.007/2.007 16 red(c,k(f(a))). [assumption]. 2.007/2.007 17 red(c,k(g(b))). [assumption]. 2.007/2.007 18 -reds(h(f(x)),k(g(b))) | red(f(x),g(x)). [clausify(6)]. 2.007/2.007 19 red(h(f(a)),c). [assumption]. 2.007/2.007 20 red(h(x),k(x)). [clausify(7)]. 2.007/2.007 21 -reds(h(f(b)),x) | -reds(c,x). [deny(8)]. 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 formulas(demodulators). 2.007/2.007 end_of_list. 2.007/2.007 2.007/2.007 ============================== end of clauses for search ============= 2.007/2.007 2.007/2.007 ============================== SEARCH ================================ 2.007/2.007 2.007/2.007 % Starting search at 0.01 seconds. 2.007/2.007 2.007/2.007 given #1 (I,wt=3): 9 reds(x,x). [assumption]. 2.007/2.007 2.007/2.007 given #2 (I,wt=9): 10 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 2.007/2.007 2.007/2.007 given #3 (I,wt=8): 11 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 2.007/2.007 2.007/2.007 given #4 (I,wt=8): 12 -red(x,y) | red(h(x),h(y)). [clausify(3)]. 2.007/2.007 2.007/2.007 given #5 (I,wt=8): 13 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 2.007/2.007 2.007/2.007 given #6 (I,wt=8): 14 -red(x,y) | red(k(x),k(y)). [clausify(5)]. 2.007/2.007 2.007/2.007 given #7 (I,wt=3): 15 red(a,b). [assumption]. 2.007/2.007 2.007/2.007 given #8 (I,wt=5): 16 red(c,k(f(a))). [assumption]. 2.007/2.007 2.007/2.007 given #9 (I,wt=5): 17 red(c,k(g(b))). [assumption]. 2.007/2.007 2.007/2.007 given #10 (I,wt=12): 18 -reds(h(f(x)),k(g(b))) | red(f(x),g(x)). [clausify(6)]. 2.007/2.007 2.007/2.007 given #11 (I,wt=5): 19 red(h(f(a)),c). [assumption]. 2.007/2.007 2.007/2.007 given #12 (I,wt=5): 20 red(h(x),k(x)). [clausify(7)]. 2.007/2.007 2.007/2.007 given #13 (I,wt=8): 21 -reds(h(f(b)),x) | -reds(c,x). [deny(8)]. 2.007/2.007 2.007/2.007 given #14 (A,wt=5): 22 red(k(a),k(b)). [ur(14,a,15,a)]. 2.007/2.007 2.007/2.007 given #15 (F,wt=5): 48 -reds(c,h(f(b))). [resolve(21,a,9,a)]. 2.007/2.007 2.007/2.007 given #16 (F,wt=5): 50 -reds(h(f(b)),c). [resolve(21,b,9,a)]. 2.007/2.007 2.007/2.007 given #17 (F,wt=5): 57 -red(c,h(f(b))). [ur(10,b,9,a,c,48,a)]. 2.007/2.007 2.007/2.007 given #18 (F,wt=5): 61 -red(h(f(b)),c). [ur(10,b,9,a,c,50,a)]. 2.007/2.007 2.007/2.007 given #19 (T,wt=3): 26 reds(a,b). [ur(10,a,15,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #20 (T,wt=5): 23 red(g(a),g(b)). [ur(13,a,15,a)]. 2.007/2.007 2.007/2.007 given #21 (T,wt=5): 24 red(h(a),h(b)). [ur(12,a,15,a)]. 2.007/2.007 2.007/2.007 given #22 (T,wt=5): 25 red(f(a),f(b)). [ur(11,a,15,a)]. 2.007/2.007 2.007/2.007 given #23 (A,wt=7): 27 red(k(c),k(k(f(a)))). [ur(14,a,16,a)]. 2.007/2.007 2.007/2.007 given #24 (F,wt=5): 62 -reds(k(f(b)),c). [ur(10,a,20,a,c,50,a)]. 2.007/2.007 2.007/2.007 given #25 (F,wt=5): 84 -red(k(f(b)),c). [ur(10,b,9,a,c,62,a)]. 2.007/2.007 2.007/2.007 given #26 (F,wt=7): 58 -reds(k(g(b)),h(f(b))). [ur(10,a,17,a,c,48,a)]. 2.007/2.007 2.007/2.007 given #27 (F,wt=7): 59 -reds(k(f(a)),h(f(b))). [ur(10,a,16,a,c,48,a)]. 2.007/2.007 2.007/2.007 given #28 (T,wt=5): 31 reds(c,k(f(a))). [ur(10,a,16,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #29 (T,wt=5): 36 reds(c,k(g(b))). [ur(10,a,17,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #30 (T,wt=5): 41 reds(h(f(a)),c). [ur(10,a,19,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #31 (T,wt=5): 46 reds(h(x),k(x)). [ur(10,a,20,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #32 (A,wt=7): 28 red(g(c),g(k(f(a)))). [ur(13,a,16,a)]. 2.007/2.007 2.007/2.007 given #33 (F,wt=5): 94 -reds(c,k(f(b))). [resolve(46,a,21,a)]. 2.007/2.007 2.007/2.007 given #34 (F,wt=5): 102 -red(c,k(f(b))). [ur(10,b,9,a,c,94,a)]. 2.007/2.007 2.007/2.007 given #35 (F,wt=7): 86 -red(k(g(b)),h(f(b))). [ur(10,b,9,a,c,58,a)]. 2.007/2.007 2.007/2.007 given #36 (F,wt=7): 88 -red(k(f(a)),h(f(b))). [ur(10,b,9,a,c,59,a)]. 2.007/2.007 2.007/2.007 given #37 (T,wt=5): 55 reds(k(a),k(b)). [ur(10,a,22,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #38 (T,wt=5): 67 reds(g(a),g(b)). [ur(10,a,23,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #39 (T,wt=5): 72 reds(h(a),h(b)). [ur(10,a,24,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #40 (T,wt=5): 77 reds(f(a),f(b)). [ur(10,a,25,a,b,9,a)]. 2.007/2.007 2.007/2.007 given #41 (A,wt=7): 29 red(h(c),h(k(f(a)))). [ur(12,a,16,a)]. 2.007/2.007 2.007/2.007 given #42 (F,wt=7): 89 -reds(h(f(b)),k(f(a))). [resolve(31,a,21,b)]. 2.007/2.007 2.007/2.007 given #43 (F,wt=7): 90 -reds(h(f(b)),k(g(b))). [resolve(36,a,21,b)]. 2.007/2.007 2.007/2.007 given #44 (F,wt=7): 92 -red(k(f(b)),h(f(a))). [ur(10,b,41,a,c,62,a)]. 2.007/2.007 2.007/2.007 given #45 (F,wt=7): 93 -red(h(f(b)),h(f(a))). [ur(10,b,41,a,c,50,a)]. 2.007/2.007 2.007/2.007 given #46 (T,wt=5): 95 reds(h(a),k(b)). [ur(10,a,24,a,b,46,a)]. 2.007/2.007 2.007/2.007 given #47 (T,wt=7): 30 red(f(c),f(k(f(a)))). [ur(11,a,16,a)]. 2.007/2.007 2.007/2.007 given #48 (T,wt=7): 32 red(k(c),k(k(g(b)))). [ur(14,a,17,a)]. 2.007/2.007 2.007/2.007 given #49 (T,wt=7): 33 red(g(c),g(k(g(b)))). [ur(13,a,17,a)]. 2.007/2.007 2.007/2.007 given #50 (A,wt=7): 34 red(h(c),h(k(g(b)))). [ur(12,a,17,a)]. 2.007/2.007 2.007/2.007 given #51 (F,wt=5): 118 -red(f(b),f(a)). [resolve(93,a,12,b)]. 2.007/2.007 2.007/2.007 given #52 (F,wt=3): 140 -red(b,a). [resolve(118,a,11,b)]. 2.007/2.007 2.007/2.007 given #53 (F,wt=7): 103 -reds(k(g(b)),k(f(b))). [ur(10,a,17,a,c,94,a)]. 2.007/2.007 2.007/2.007 given #54 (F,wt=7): 104 -reds(k(f(a)),k(f(b))). [ur(10,a,16,a,c,94,a)]. 2.007/2.007 2.007/2.007 ============================== PROOF ================================= 2.007/2.007 2.007/2.007 % Proof 1 at 0.01 (+ 0.00) seconds. 2.007/2.007 % Length of proof is 19. 2.007/2.007 % Level of proof is 5. 2.007/2.007 % Maximum clause weight is 9.000. 2.007/2.007 % Given clauses 54. 2.007/2.007 2.007/2.007 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 2.007/2.007 2 red(x,y) -> red(f(x),f(y)) # label(non_clause). [assumption]. 2.007/2.007 5 red(x,y) -> red(k(x),k(y)) # label(non_clause). [assumption]. 2.007/2.007 7 (all x red(h(x),k(x))) # label(non_clause). [assumption]. 2.007/2.007 8 (exists z (reds(h(f(b)),z) & reds(c,z))) # label(non_clause) # label(goal). [goal]. 2.007/2.007 9 reds(x,x). [assumption]. 2.007/2.007 10 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 2.007/2.007 11 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 2.007/2.007 14 -red(x,y) | red(k(x),k(y)). [clausify(5)]. 2.007/2.007 15 red(a,b). [assumption]. 2.007/2.007 16 red(c,k(f(a))). [assumption]. 2.007/2.007 20 red(h(x),k(x)). [clausify(7)]. 2.007/2.007 21 -reds(h(f(b)),x) | -reds(c,x). [deny(8)]. 2.007/2.007 25 red(f(a),f(b)). [ur(11,a,15,a)]. 2.007/2.007 46 reds(h(x),k(x)). [ur(10,a,20,a,b,9,a)]. 2.007/2.007 73 red(k(f(a)),k(f(b))). [ur(14,a,25,a)]. 2.007/2.007 94 -reds(c,k(f(b))). [resolve(46,a,21,a)]. 2.007/2.007 104 -reds(k(f(a)),k(f(b))). [ur(10,a,16,a,c,94,a)]. 2.007/2.007 144 $F. [ur(10,b,9,a,c,104,a),unit_del(a,73)]. 2.007/2.007 2.007/2.007 ============================== end of proof ========================== 2.007/2.007 2.007/2.007 ============================== STATISTICS ============================ 2.007/2.007 2.007/2.007 Given=54. Generated=151. Kept=135. proofs=1. 2.007/2.007 Usable=54. Sos=80. Demods=0. Limbo=1, Disabled=13. Hints=0. 2.007/2.007 Kept_by_rule=0, Deleted_by_rule=0. 2.007/2.007 Forward_subsumed=15. Back_subsumed=0. 2.007/2.007 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 2.007/2.007 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 2.007/2.007 Demod_attempts=0. Demod_rewrites=0. 2.007/2.007 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 2.007/2.007 Nonunit_fsub_feature_tests=7. Nonunit_bsub_feature_tests=60. 2.007/2.007 Megabytes=0.23. 2.007/2.007 User_CPU=0.01, System_CPU=0.00, Wall_clock=0. 2.007/2.007 2.007/2.007 ============================== end of statistics ===================== 2.007/2.007 2.007/2.007 ============================== end of search ========================= 2.007/2.007 2.007/2.007 THEOREM PROVED 2.007/2.007 2.007/2.007 Exiting with 1 proof. 2.007/2.007 2.007/2.007 Process 78470 exit (max_proofs) Wed Mar 9 10:20:07 2022 2.007/2.007 2.007/2.007 2.007/2.007 The problem is joinable. 2.007/2.007 0.50user 0.11system 0:02.07elapsed 29%CPU (0avgtext+0avgdata 22236maxresident)k 2.007/2.007 8inputs+0outputs (0major+31331minor)pagefaults 0swaps