82.061/82.061 YES 82.061/82.061 82.061/82.061 Problem 1: 82.061/82.061 82.061/82.061 82.061/82.061 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.061/82.061 Confluence Problem: 82.061/82.061 (VAR vNonEmpty:S x:S y:S) 82.061/82.061 (STRATEGY CONTEXTSENSITIVE 82.061/82.061 (f 1 2) 82.061/82.061 (g 1) 82.061/82.061 (h 1) 82.061/82.061 (a) 82.061/82.061 (c 1) 82.061/82.061 (fSNonEmpty) 82.061/82.061 (s 1) 82.061/82.061 ) 82.061/82.061 (RULES 82.061/82.061 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.061/82.061 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.061/82.061 g(s(x:S)) -> x:S 82.061/82.061 h(s(x:S)) -> x:S 82.061/82.061 ) 82.061/82.061 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.061/82.061 82.061/82.061 82.061/82.061 Problem 1: 82.061/82.061 82.061/82.061 Inlining of Conditions Processor [STERN17]: 82.061/82.061 82.061/82.061 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.061/82.061 Confluence Problem: 82.061/82.061 (VAR vNonEmpty:S x:S y:S) 82.061/82.061 (STRATEGY CONTEXTSENSITIVE 82.061/82.061 (f 1 2) 82.061/82.061 (g 1) 82.061/82.061 (h 1) 82.061/82.061 (a) 82.061/82.061 (c 1) 82.061/82.061 (fSNonEmpty) 82.061/82.061 (s 1) 82.061/82.061 ) 82.061/82.061 (RULES 82.061/82.061 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.061/82.061 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.061/82.061 g(s(x:S)) -> x:S 82.061/82.061 h(s(x:S)) -> x:S 82.061/82.061 ) 82.061/82.061 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.061/82.061 82.061/82.061 82.061/82.061 Problem 1: 82.061/82.061 82.061/82.061 Clean CTRS Processor: 82.061/82.061 82.061/82.061 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.061/82.061 Confluence Problem: 82.061/82.061 (VAR x:S y:S) 82.061/82.061 (STRATEGY CONTEXTSENSITIVE 82.061/82.061 (f 1 2) 82.061/82.061 (g 1) 82.061/82.061 (h 1) 82.061/82.061 (a) 82.061/82.061 (c 1) 82.061/82.061 (fSNonEmpty) 82.061/82.061 (s 1) 82.061/82.061 ) 82.061/82.061 (RULES 82.061/82.061 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.061/82.061 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.061/82.061 g(s(x:S)) -> x:S 82.061/82.061 h(s(x:S)) -> x:S 82.061/82.061 ) 82.061/82.061 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.061/82.061 82.061/82.061 CRule InfChecker Info: 82.061/82.061 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.061/82.061 Rule remains 82.061/82.061 Proof: 82.061/82.061 NO 82.061/82.061 82.061/82.061 Problem 1: 82.061/82.061 82.061/82.061 Infeasibility Problem: 82.061/82.061 [(VAR vNonEmpty:S vNonEmpty:S:S x:S:S y:S:S) 82.061/82.061 (STRATEGY CONTEXTSENSITIVE 82.061/82.061 (f 1 2) 82.061/82.061 (g 1) 82.061/82.061 (h 1) 82.061/82.061 (a) 82.061/82.061 (c 1) 82.061/82.061 (fSNonEmpty) 82.061/82.061 (s 1) 82.061/82.061 ) 82.061/82.061 (RULES 82.061/82.061 f(x:S:S,y:S:S) -> g(s(x:S:S)) | c(g(x:S:S)) ->* c(a) 82.061/82.061 f(x:S:S,y:S:S) -> h(s(x:S:S)) | c(h(x:S:S)) ->* c(a) 82.061/82.061 g(s(x:S:S)) -> x:S:S 82.061/82.061 h(s(x:S:S)) -> x:S:S 82.061/82.061 )] 82.061/82.061 82.061/82.061 Infeasibility Conditions: 82.061/82.061 c(g(x:S:S)) ->* c(a) 82.061/82.061 82.061/82.061 Problem 1: 82.061/82.061 82.061/82.061 Obtaining a proof using Prover9: 82.061/82.061 82.061/82.061 -> Prover9 Output: 82.061/82.061 ============================== Prover9 =============================== 82.061/82.061 Prover9 (64) version 2009-11A, November 2009. 82.061/82.061 Process 54184 was started by ubuntu on ubuntu, 82.061/82.061 Wed Jul 14 11:11:25 2021 82.061/82.061 The command was "./prover9 -f /tmp/prover954175-0.in". 82.061/82.061 ============================== end of head =========================== 82.061/82.061 82.061/82.061 ============================== INPUT ================================= 82.061/82.061 82.061/82.061 % Reading from file /tmp/prover954175-0.in 82.061/82.061 82.061/82.061 assign(max_seconds,20). 82.061/82.061 82.061/82.061 formulas(assumptions). 82.061/82.061 ->*_s0(x,x) # label(reflexivity). 82.061/82.061 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 82.061/82.061 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence). 82.061/82.061 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence). 82.061/82.061 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence). 82.061/82.061 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence). 82.061/82.061 ->_s0(x1,y) -> ->_s0(c(x1),c(y)) # label(congruence). 82.061/82.061 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). 82.061/82.061 ->*_s0(c(g(x2)),c(a)) -> ->_s0(f(x2,x3),g(s(x2))) # label(replacement). 82.061/82.061 ->*_s0(c(h(x2)),c(a)) -> ->_s0(f(x2,x3),h(s(x2))) # label(replacement). 82.061/82.061 ->_s0(g(s(x2)),x2) # label(replacement). 82.061/82.061 ->_s0(h(s(x2)),x2) # label(replacement). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(goals). 82.061/82.061 (exists x2 ->*_s0(c(g(x2)),c(a))) # label(goal). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 ============================== end of input ========================== 82.061/82.061 82.061/82.061 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 82.061/82.061 82.061/82.061 % Formulas that are not ordinary clauses: 82.061/82.061 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 82.061/82.061 2 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 3 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 4 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 5 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 6 ->_s0(x1,y) -> ->_s0(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 7 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 8 ->*_s0(c(g(x2)),c(a)) -> ->_s0(f(x2,x3),g(s(x2))) # label(replacement) # label(non_clause). [assumption]. 82.061/82.061 9 ->*_s0(c(h(x2)),c(a)) -> ->_s0(f(x2,x3),h(s(x2))) # label(replacement) # label(non_clause). [assumption]. 82.061/82.061 10 (exists x2 ->*_s0(c(g(x2)),c(a))) # label(goal) # label(non_clause) # label(goal). [goal]. 82.061/82.061 82.061/82.061 ============================== end of process non-clausal formulas === 82.061/82.061 82.061/82.061 ============================== PROCESS INITIAL CLAUSES =============== 82.061/82.061 82.061/82.061 % Clauses before input processing: 82.061/82.061 82.061/82.061 formulas(usable). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(sos). 82.061/82.061 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.061/82.061 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.061/82.061 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.061/82.061 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.061/82.061 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.061/82.061 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.061/82.061 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.061/82.061 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.061/82.061 -->*_s0(c(g(x)),c(a)) | ->_s0(f(x,y),g(s(x))) # label(replacement). [clausify(8)]. 82.061/82.061 -->*_s0(c(h(x)),c(a)) | ->_s0(f(x,y),h(s(x))) # label(replacement). [clausify(9)]. 82.061/82.061 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 -->*_s0(c(g(x)),c(a)) # label(goal). [deny(10)]. 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(demodulators). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 ============================== PREDICATE ELIMINATION ================= 82.061/82.061 82.061/82.061 No predicates eliminated. 82.061/82.061 82.061/82.061 ============================== end predicate elimination ============= 82.061/82.061 82.061/82.061 Auto_denials: 82.061/82.061 % copying label goal to answer in negative clause 82.061/82.061 82.061/82.061 Term ordering decisions: 82.061/82.061 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 82.061/82.061 Function symbol precedence: function_order([ a, f, c, s, g, h ]). 82.061/82.061 After inverse_order: (no changes). 82.061/82.061 Unfolding symbols: (none). 82.061/82.061 82.061/82.061 Auto_inference settings: 82.061/82.061 % set(neg_binary_resolution). % (HNE depth_diff=-6) 82.061/82.061 % clear(ordered_res). % (HNE depth_diff=-6) 82.061/82.061 % set(ur_resolution). % (HNE depth_diff=-6) 82.061/82.061 % set(ur_resolution) -> set(pos_ur_resolution). 82.061/82.061 % set(ur_resolution) -> set(neg_ur_resolution). 82.061/82.061 82.061/82.061 Auto_process settings: (no changes). 82.061/82.061 82.061/82.061 kept: 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.061/82.061 kept: 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.061/82.061 kept: 13 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.061/82.061 kept: 14 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.061/82.061 kept: 15 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.061/82.061 kept: 16 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.061/82.061 kept: 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.061/82.061 kept: 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.061/82.061 kept: 19 -->*_s0(c(g(x)),c(a)) | ->_s0(f(x,y),g(s(x))) # label(replacement). [clausify(8)]. 82.061/82.061 kept: 20 -->*_s0(c(h(x)),c(a)) | ->_s0(f(x,y),h(s(x))) # label(replacement). [clausify(9)]. 82.061/82.061 kept: 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 kept: 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 kept: 23 -->*_s0(c(g(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.061/82.061 82.061/82.061 ============================== end of process initial clauses ======== 82.061/82.061 82.061/82.061 ============================== CLAUSES FOR SEARCH ==================== 82.061/82.061 82.061/82.061 % Clauses after input processing: 82.061/82.061 82.061/82.061 formulas(usable). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(sos). 82.061/82.061 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.061/82.061 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.061/82.061 13 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.061/82.061 14 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.061/82.061 15 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.061/82.061 16 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.061/82.061 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.061/82.061 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.061/82.061 20 -->*_s0(c(h(x)),c(a)) | ->_s0(f(x,y),h(s(x))) # label(replacement). [clausify(9)]. 82.061/82.061 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 23 -->*_s0(c(g(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(demodulators). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 ============================== end of clauses for search ============= 82.061/82.061 82.061/82.061 ============================== SEARCH ================================ 82.061/82.061 82.061/82.061 % Starting search at 0.00 seconds. 82.061/82.061 82.061/82.061 given #1 (I,wt=3): 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.061/82.061 82.061/82.061 given #2 (I,wt=9): 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.061/82.061 82.061/82.061 given #3 (I,wt=10): 13 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.061/82.061 82.061/82.061 given #4 (I,wt=10): 14 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.061/82.061 82.061/82.061 given #5 (I,wt=8): 15 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.061/82.061 82.061/82.061 given #6 (I,wt=8): 16 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.061/82.061 82.061/82.061 given #7 (I,wt=8): 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.061/82.061 82.061/82.061 given #8 (I,wt=8): 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.061/82.061 82.061/82.061 given #9 (I,wt=13): 20 -->*_s0(c(h(x)),c(a)) | ->_s0(f(x,y),h(s(x))) # label(replacement). [clausify(9)]. 82.061/82.061 82.061/82.061 given #10 (I,wt=5): 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 82.061/82.061 given #11 (I,wt=5): 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 82.061/82.061 given #12 (I,wt=6): 23 -->*_s0(c(g(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.061/82.061 82.061/82.061 ============================== PROOF ================================= 82.061/82.061 82.061/82.061 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 82.061/82.061 % Length of proof is 11. 82.061/82.061 % Level of proof is 3. 82.061/82.061 % Maximum clause weight is 9.000. 82.061/82.061 % Given clauses 12. 82.061/82.061 82.061/82.061 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 82.061/82.061 6 ->_s0(x1,y) -> ->_s0(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 10 (exists x2 ->*_s0(c(g(x2)),c(a))) # label(goal) # label(non_clause) # label(goal). [goal]. 82.061/82.061 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.061/82.061 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.061/82.061 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.061/82.061 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 23 -->*_s0(c(g(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.061/82.061 25 ->_s0(c(g(s(x))),c(x)). [ur(17,a,21,a)]. 82.061/82.061 39 -->_s0(c(g(x)),c(a)) # answer(goal). [ur(12,b,11,a,c,23,a)]. 82.061/82.061 40 $F # answer(goal). [resolve(39,a,25,a)]. 82.061/82.061 82.061/82.061 ============================== end of proof ========================== 82.061/82.061 82.061/82.061 ============================== STATISTICS ============================ 82.061/82.061 82.061/82.061 Given=12. Generated=29. Kept=29. proofs=1. 82.061/82.061 Usable=12. Sos=14. Demods=0. Limbo=1, Disabled=14. Hints=0. 82.061/82.061 Kept_by_rule=0, Deleted_by_rule=0. 82.061/82.061 Forward_subsumed=0. Back_subsumed=1. 82.061/82.061 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 82.061/82.061 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 82.061/82.061 Demod_attempts=0. Demod_rewrites=0. 82.061/82.061 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 82.061/82.061 Nonunit_fsub_feature_tests=1. Nonunit_bsub_feature_tests=15. 82.061/82.061 Megabytes=0.09. 82.061/82.061 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 82.061/82.061 82.061/82.061 ============================== end of statistics ===================== 82.061/82.061 82.061/82.061 ============================== end of search ========================= 82.061/82.061 82.061/82.061 THEOREM PROVED 82.061/82.061 82.061/82.061 Exiting with 1 proof. 82.061/82.061 82.061/82.061 Process 54184 exit (max_proofs) Wed Jul 14 11:11:25 2021 82.061/82.061 82.061/82.061 82.061/82.061 The problem is feasible. 82.061/82.061 82.061/82.061 82.061/82.061 CRule InfChecker Info: 82.061/82.061 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.061/82.061 Rule remains 82.061/82.061 Proof: 82.061/82.061 NO 82.061/82.061 82.061/82.061 Problem 1: 82.061/82.061 82.061/82.061 Infeasibility Problem: 82.061/82.061 [(VAR vNonEmpty:S vNonEmpty:S:S x:S:S y:S:S) 82.061/82.061 (STRATEGY CONTEXTSENSITIVE 82.061/82.061 (f 1 2) 82.061/82.061 (g 1) 82.061/82.061 (h 1) 82.061/82.061 (a) 82.061/82.061 (c 1) 82.061/82.061 (fSNonEmpty) 82.061/82.061 (s 1) 82.061/82.061 ) 82.061/82.061 (RULES 82.061/82.061 f(x:S:S,y:S:S) -> g(s(x:S:S)) | c(g(x:S:S)) ->* c(a) 82.061/82.061 f(x:S:S,y:S:S) -> h(s(x:S:S)) | c(h(x:S:S)) ->* c(a) 82.061/82.061 g(s(x:S:S)) -> x:S:S 82.061/82.061 h(s(x:S:S)) -> x:S:S 82.061/82.061 )] 82.061/82.061 82.061/82.061 Infeasibility Conditions: 82.061/82.061 c(h(x:S:S)) ->* c(a) 82.061/82.061 82.061/82.061 Problem 1: 82.061/82.061 82.061/82.061 Obtaining a proof using Prover9: 82.061/82.061 82.061/82.061 -> Prover9 Output: 82.061/82.061 ============================== Prover9 =============================== 82.061/82.061 Prover9 (64) version 2009-11A, November 2009. 82.061/82.061 Process 54207 was started by ubuntu on ubuntu, 82.061/82.061 Wed Jul 14 11:11:25 2021 82.061/82.061 The command was "./prover9 -f /tmp/prover954197-0.in". 82.061/82.061 ============================== end of head =========================== 82.061/82.061 82.061/82.061 ============================== INPUT ================================= 82.061/82.061 82.061/82.061 % Reading from file /tmp/prover954197-0.in 82.061/82.061 82.061/82.061 assign(max_seconds,20). 82.061/82.061 82.061/82.061 formulas(assumptions). 82.061/82.061 ->*_s0(x,x) # label(reflexivity). 82.061/82.061 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 82.061/82.061 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence). 82.061/82.061 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence). 82.061/82.061 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence). 82.061/82.061 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence). 82.061/82.061 ->_s0(x1,y) -> ->_s0(c(x1),c(y)) # label(congruence). 82.061/82.061 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). 82.061/82.061 ->*_s0(c(g(x2)),c(a)) -> ->_s0(f(x2,x3),g(s(x2))) # label(replacement). 82.061/82.061 ->*_s0(c(h(x2)),c(a)) -> ->_s0(f(x2,x3),h(s(x2))) # label(replacement). 82.061/82.061 ->_s0(g(s(x2)),x2) # label(replacement). 82.061/82.061 ->_s0(h(s(x2)),x2) # label(replacement). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(goals). 82.061/82.061 (exists x2 ->*_s0(c(h(x2)),c(a))) # label(goal). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 ============================== end of input ========================== 82.061/82.061 82.061/82.061 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 82.061/82.061 82.061/82.061 % Formulas that are not ordinary clauses: 82.061/82.061 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 82.061/82.061 2 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 3 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 4 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 5 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 6 ->_s0(x1,y) -> ->_s0(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 7 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 8 ->*_s0(c(g(x2)),c(a)) -> ->_s0(f(x2,x3),g(s(x2))) # label(replacement) # label(non_clause). [assumption]. 82.061/82.061 9 ->*_s0(c(h(x2)),c(a)) -> ->_s0(f(x2,x3),h(s(x2))) # label(replacement) # label(non_clause). [assumption]. 82.061/82.061 10 (exists x2 ->*_s0(c(h(x2)),c(a))) # label(goal) # label(non_clause) # label(goal). [goal]. 82.061/82.061 82.061/82.061 ============================== end of process non-clausal formulas === 82.061/82.061 82.061/82.061 ============================== PROCESS INITIAL CLAUSES =============== 82.061/82.061 82.061/82.061 % Clauses before input processing: 82.061/82.061 82.061/82.061 formulas(usable). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(sos). 82.061/82.061 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.061/82.061 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.061/82.061 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.061/82.061 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.061/82.061 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.061/82.061 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.061/82.061 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.061/82.061 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.061/82.061 -->*_s0(c(g(x)),c(a)) | ->_s0(f(x,y),g(s(x))) # label(replacement). [clausify(8)]. 82.061/82.061 -->*_s0(c(h(x)),c(a)) | ->_s0(f(x,y),h(s(x))) # label(replacement). [clausify(9)]. 82.061/82.061 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 -->*_s0(c(h(x)),c(a)) # label(goal). [deny(10)]. 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(demodulators). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 ============================== PREDICATE ELIMINATION ================= 82.061/82.061 82.061/82.061 No predicates eliminated. 82.061/82.061 82.061/82.061 ============================== end predicate elimination ============= 82.061/82.061 82.061/82.061 Auto_denials: 82.061/82.061 % copying label goal to answer in negative clause 82.061/82.061 82.061/82.061 Term ordering decisions: 82.061/82.061 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 82.061/82.061 Function symbol precedence: function_order([ a, f, c, s, g, h ]). 82.061/82.061 After inverse_order: (no changes). 82.061/82.061 Unfolding symbols: (none). 82.061/82.061 82.061/82.061 Auto_inference settings: 82.061/82.061 % set(neg_binary_resolution). % (HNE depth_diff=-6) 82.061/82.061 % clear(ordered_res). % (HNE depth_diff=-6) 82.061/82.061 % set(ur_resolution). % (HNE depth_diff=-6) 82.061/82.061 % set(ur_resolution) -> set(pos_ur_resolution). 82.061/82.061 % set(ur_resolution) -> set(neg_ur_resolution). 82.061/82.061 82.061/82.061 Auto_process settings: (no changes). 82.061/82.061 82.061/82.061 kept: 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.061/82.061 kept: 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.061/82.061 kept: 13 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.061/82.061 kept: 14 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.061/82.061 kept: 15 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.061/82.061 kept: 16 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.061/82.061 kept: 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.061/82.061 kept: 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.061/82.061 kept: 19 -->*_s0(c(g(x)),c(a)) | ->_s0(f(x,y),g(s(x))) # label(replacement). [clausify(8)]. 82.061/82.061 kept: 20 -->*_s0(c(h(x)),c(a)) | ->_s0(f(x,y),h(s(x))) # label(replacement). [clausify(9)]. 82.061/82.061 kept: 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 kept: 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 kept: 23 -->*_s0(c(h(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.061/82.061 82.061/82.061 ============================== end of process initial clauses ======== 82.061/82.061 82.061/82.061 ============================== CLAUSES FOR SEARCH ==================== 82.061/82.061 82.061/82.061 % Clauses after input processing: 82.061/82.061 82.061/82.061 formulas(usable). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(sos). 82.061/82.061 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.061/82.061 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.061/82.061 13 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.061/82.061 14 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.061/82.061 15 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.061/82.061 16 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.061/82.061 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.061/82.061 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.061/82.061 19 -->*_s0(c(g(x)),c(a)) | ->_s0(f(x,y),g(s(x))) # label(replacement). [clausify(8)]. 82.061/82.061 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 23 -->*_s0(c(h(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(demodulators). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 ============================== end of clauses for search ============= 82.061/82.061 82.061/82.061 ============================== SEARCH ================================ 82.061/82.061 82.061/82.061 % Starting search at 0.00 seconds. 82.061/82.061 82.061/82.061 given #1 (I,wt=3): 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.061/82.061 82.061/82.061 given #2 (I,wt=9): 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.061/82.061 82.061/82.061 given #3 (I,wt=10): 13 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.061/82.061 82.061/82.061 given #4 (I,wt=10): 14 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.061/82.061 82.061/82.061 given #5 (I,wt=8): 15 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.061/82.061 82.061/82.061 given #6 (I,wt=8): 16 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.061/82.061 82.061/82.061 given #7 (I,wt=8): 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.061/82.061 82.061/82.061 given #8 (I,wt=8): 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.061/82.061 82.061/82.061 given #9 (I,wt=13): 19 -->*_s0(c(g(x)),c(a)) | ->_s0(f(x,y),g(s(x))) # label(replacement). [clausify(8)]. 82.061/82.061 82.061/82.061 given #10 (I,wt=5): 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 82.061/82.061 given #11 (I,wt=5): 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 82.061/82.061 given #12 (I,wt=6): 23 -->*_s0(c(h(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.061/82.061 82.061/82.061 ============================== PROOF ================================= 82.061/82.061 82.061/82.061 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 82.061/82.061 % Length of proof is 11. 82.061/82.061 % Level of proof is 3. 82.061/82.061 % Maximum clause weight is 9.000. 82.061/82.061 % Given clauses 12. 82.061/82.061 82.061/82.061 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 82.061/82.061 6 ->_s0(x1,y) -> ->_s0(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 10 (exists x2 ->*_s0(c(h(x2)),c(a))) # label(goal) # label(non_clause) # label(goal). [goal]. 82.061/82.061 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.061/82.061 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.061/82.061 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.061/82.061 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 23 -->*_s0(c(h(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.061/82.061 32 ->_s0(c(h(s(x))),c(x)). [ur(17,a,22,a)]. 82.061/82.061 39 -->_s0(c(h(x)),c(a)) # answer(goal). [ur(12,b,11,a,c,23,a)]. 82.061/82.061 40 $F # answer(goal). [resolve(39,a,32,a)]. 82.061/82.061 82.061/82.061 ============================== end of proof ========================== 82.061/82.061 82.061/82.061 ============================== STATISTICS ============================ 82.061/82.061 82.061/82.061 Given=12. Generated=29. Kept=29. proofs=1. 82.061/82.061 Usable=12. Sos=14. Demods=0. Limbo=1, Disabled=14. Hints=0. 82.061/82.061 Kept_by_rule=0, Deleted_by_rule=0. 82.061/82.061 Forward_subsumed=0. Back_subsumed=1. 82.061/82.061 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 82.061/82.061 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 82.061/82.061 Demod_attempts=0. Demod_rewrites=0. 82.061/82.061 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 82.061/82.061 Nonunit_fsub_feature_tests=1. Nonunit_bsub_feature_tests=15. 82.061/82.061 Megabytes=0.09. 82.061/82.061 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 82.061/82.061 82.061/82.061 ============================== end of statistics ===================== 82.061/82.061 82.061/82.061 ============================== end of search ========================= 82.061/82.061 82.061/82.061 THEOREM PROVED 82.061/82.061 82.061/82.061 Exiting with 1 proof. 82.061/82.061 82.061/82.061 Process 54207 exit (max_proofs) Wed Jul 14 11:11:25 2021 82.061/82.061 82.061/82.061 82.061/82.061 The problem is feasible. 82.061/82.061 82.061/82.061 82.061/82.061 CRule InfChecker Info: 82.061/82.061 g(s(x:S)) -> x:S 82.061/82.061 Rule remains 82.061/82.061 Proof: 82.061/82.061 NO_CONDS 82.061/82.061 82.061/82.061 CRule InfChecker Info: 82.061/82.061 h(s(x:S)) -> x:S 82.061/82.061 Rule remains 82.061/82.061 Proof: 82.061/82.061 NO_CONDS 82.061/82.061 82.061/82.061 Problem 1: 82.061/82.061 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.061/82.061 Confluence Problem: 82.061/82.061 (VAR x:S y:S) 82.061/82.061 (STRATEGY CONTEXTSENSITIVE 82.061/82.061 (f 1 2) 82.061/82.061 (g 1) 82.061/82.061 (h 1) 82.061/82.061 (a) 82.061/82.061 (c 1) 82.061/82.061 (fSNonEmpty) 82.061/82.061 (s 1) 82.061/82.061 ) 82.061/82.061 (RULES 82.061/82.061 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.061/82.061 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.061/82.061 g(s(x:S)) -> x:S 82.061/82.061 h(s(x:S)) -> x:S 82.061/82.061 ) 82.061/82.061 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.061/82.061 82.061/82.061 Critical Pairs Processor: 82.061/82.061 -> Rules: 82.061/82.061 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.061/82.061 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.061/82.061 g(s(x:S)) -> x:S 82.061/82.061 h(s(x:S)) -> x:S 82.061/82.061 -> Vars: 82.061/82.061 "x", "y", "x", "y", "x", "x" 82.061/82.061 -> FVars: 82.061/82.061 "x3", "x4", "x5", "x6", "x7", "x8" 82.061/82.061 -> PVars: 82.061/82.061 "x": ["x3", "x5", "x7", "x8"], "y": ["x4", "x6"] 82.061/82.061 82.061/82.061 -> Rlps: 82.061/82.061 crule: f(x3:S,x4:S) -> g(s(x3:S)) | c(g(x3:S)) ->* c(a), id: 1, possubterms: f(x3:S,x4:S)-> [] 82.061/82.061 crule: f(x5:S,x6:S) -> h(s(x5:S)) | c(h(x5:S)) ->* c(a), id: 2, possubterms: f(x5:S,x6:S)-> [] 82.061/82.061 crule: g(s(x7:S)) -> x7:S, id: 3, possubterms: g(s(x7:S))-> [], s(x7:S)-> [1] 82.061/82.061 crule: h(s(x8:S)) -> x8:S, id: 4, possubterms: h(s(x8:S))-> [], s(x8:S)-> [1] 82.061/82.061 82.061/82.061 -> Unifications: 82.061/82.061 R2 unifies with R1 at p: [], l: f(x5:S,x6:S), lp: f(x5:S,x6:S), conds: {c(h(x5:S)) ->* c(a), c(g(x:S)) ->* c(a)}, sig: {x5:S -> x:S,x6:S -> y:S}, l': f(x:S,y:S), r: h(s(x5:S)), r': g(s(x:S)) 82.061/82.061 82.061/82.061 -> Critical pairs info: 82.061/82.061 | c(h(x:S)) ->* c(a), c(g(x:S)) ->* c(a) => Not trivial, Overlay, N1 82.061/82.061 82.061/82.061 -> Problem conclusions: 82.061/82.061 Left linear, Right linear, Linear 82.061/82.061 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 82.061/82.061 CTRS Type: 1 82.061/82.061 Deterministic, Strongly deterministic 82.061/82.061 Oriented CTRS, Properly oriented CTRS, Not join CTRS 82.061/82.061 Maybe right-stable CTRS, Overlay CTRS 82.061/82.061 Maybe normal CTRS, Maybe almost normal CTRS 82.061/82.061 Maybe terminating CTRS, Maybe joinable CCPs 82.061/82.061 Maybe level confluent 82.061/82.061 Maybe confluent 82.061/82.061 82.061/82.061 Problem 1: 82.061/82.061 Clean Infeasible CCPs Processor: 82.061/82.061 Num of CPIs: 1 82.061/82.061 Timeout: 60 82.061/82.061 Timeout for each infeasibility problem: 60 s 82.061/82.061 | c(h(x:S)) ->* c(a), c(g(x:S)) ->* c(a) => Not trivial, Overlay, Feasible conditions, N1 82.061/82.061 (PROBLEM INFEASIBILITY) 82.061/82.061 (VAR x y) 82.061/82.061 (RULES 82.061/82.061 f(x,y) -> g(s(x)) | c(g(x)) ->* c(a) 82.061/82.061 f(x,y) -> h(s(x)) | c(h(x)) ->* c(a) 82.061/82.061 g(s(x)) -> x 82.061/82.061 h(s(x)) -> x) 82.061/82.061 (VAR x5) 82.061/82.061 (CONDITION c(h(x5)) ->* c(a), c(g(x5)) ->* c(a)) 82.061/82.061 82.061/82.061 Proof: 82.061/82.061 NO 82.061/82.061 82.061/82.061 Problem 1: 82.061/82.061 82.061/82.061 Infeasibility Problem: 82.061/82.061 [(VAR vNonEmpty:S x:S y:S x5:S) 82.061/82.061 (STRATEGY CONTEXTSENSITIVE 82.061/82.061 (f 1 2) 82.061/82.061 (g 1) 82.061/82.061 (h 1) 82.061/82.061 (a) 82.061/82.061 (c 1) 82.061/82.061 (fSNonEmpty) 82.061/82.061 (s 1) 82.061/82.061 ) 82.061/82.061 (RULES 82.061/82.061 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.061/82.061 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.061/82.061 g(s(x:S)) -> x:S 82.061/82.061 h(s(x:S)) -> x:S 82.061/82.061 )] 82.061/82.061 82.061/82.061 Infeasibility Conditions: 82.061/82.061 c(h(x5:S)) ->* c(a), c(g(x5:S)) ->* c(a) 82.061/82.061 82.061/82.061 Problem 1: 82.061/82.061 82.061/82.061 Obtaining a proof using Prover9: 82.061/82.061 82.061/82.061 -> Prover9 Output: 82.061/82.061 ============================== Prover9 =============================== 82.061/82.061 Prover9 (64) version 2009-11A, November 2009. 82.061/82.061 Process 54234 was started by ubuntu on ubuntu, 82.061/82.061 Wed Jul 14 11:11:25 2021 82.061/82.061 The command was "./prover9 -f /tmp/prover954223-0.in". 82.061/82.061 ============================== end of head =========================== 82.061/82.061 82.061/82.061 ============================== INPUT ================================= 82.061/82.061 82.061/82.061 % Reading from file /tmp/prover954223-0.in 82.061/82.061 82.061/82.061 assign(max_seconds,20). 82.061/82.061 82.061/82.061 formulas(assumptions). 82.061/82.061 ->*_s0(x,x) # label(reflexivity). 82.061/82.061 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 82.061/82.061 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence). 82.061/82.061 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence). 82.061/82.061 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence). 82.061/82.061 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence). 82.061/82.061 ->_s0(x1,y) -> ->_s0(c(x1),c(y)) # label(congruence). 82.061/82.061 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). 82.061/82.061 ->*_s0(c(g(x1)),c(a)) -> ->_s0(f(x1,x2),g(s(x1))) # label(replacement). 82.061/82.061 ->*_s0(c(h(x1)),c(a)) -> ->_s0(f(x1,x2),h(s(x1))) # label(replacement). 82.061/82.061 ->_s0(g(s(x1)),x1) # label(replacement). 82.061/82.061 ->_s0(h(s(x1)),x1) # label(replacement). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(goals). 82.061/82.061 (exists x3 (->*_s0(c(h(x3)),c(a)) & ->*_s0(c(g(x3)),c(a)))) # label(goal). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 ============================== end of input ========================== 82.061/82.061 82.061/82.061 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 82.061/82.061 82.061/82.061 % Formulas that are not ordinary clauses: 82.061/82.061 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 82.061/82.061 2 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 3 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 4 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 5 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 6 ->_s0(x1,y) -> ->_s0(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 7 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 8 ->*_s0(c(g(x1)),c(a)) -> ->_s0(f(x1,x2),g(s(x1))) # label(replacement) # label(non_clause). [assumption]. 82.061/82.061 9 ->*_s0(c(h(x1)),c(a)) -> ->_s0(f(x1,x2),h(s(x1))) # label(replacement) # label(non_clause). [assumption]. 82.061/82.061 10 (exists x3 (->*_s0(c(h(x3)),c(a)) & ->*_s0(c(g(x3)),c(a)))) # label(goal) # label(non_clause) # label(goal). [goal]. 82.061/82.061 82.061/82.061 ============================== end of process non-clausal formulas === 82.061/82.061 82.061/82.061 ============================== PROCESS INITIAL CLAUSES =============== 82.061/82.061 82.061/82.061 % Clauses before input processing: 82.061/82.061 82.061/82.061 formulas(usable). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(sos). 82.061/82.061 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.061/82.061 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.061/82.061 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.061/82.061 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.061/82.061 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.061/82.061 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.061/82.061 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.061/82.061 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.061/82.061 -->*_s0(c(g(x)),c(a)) | ->_s0(f(x,y),g(s(x))) # label(replacement). [clausify(8)]. 82.061/82.061 -->*_s0(c(h(x)),c(a)) | ->_s0(f(x,y),h(s(x))) # label(replacement). [clausify(9)]. 82.061/82.061 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 -->*_s0(c(h(x)),c(a)) | -->*_s0(c(g(x)),c(a)) # label(goal). [deny(10)]. 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(demodulators). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 ============================== PREDICATE ELIMINATION ================= 82.061/82.061 82.061/82.061 No predicates eliminated. 82.061/82.061 82.061/82.061 ============================== end predicate elimination ============= 82.061/82.061 82.061/82.061 Auto_denials: 82.061/82.061 % copying label goal to answer in negative clause 82.061/82.061 82.061/82.061 Term ordering decisions: 82.061/82.061 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 82.061/82.061 Function symbol precedence: function_order([ a, f, c, s, g, h ]). 82.061/82.061 After inverse_order: (no changes). 82.061/82.061 Unfolding symbols: (none). 82.061/82.061 82.061/82.061 Auto_inference settings: 82.061/82.061 % set(neg_binary_resolution). % (HNE depth_diff=-6) 82.061/82.061 % clear(ordered_res). % (HNE depth_diff=-6) 82.061/82.061 % set(ur_resolution). % (HNE depth_diff=-6) 82.061/82.061 % set(ur_resolution) -> set(pos_ur_resolution). 82.061/82.061 % set(ur_resolution) -> set(neg_ur_resolution). 82.061/82.061 82.061/82.061 Auto_process settings: 82.061/82.061 % set(unit_deletion). % (Horn set with negative nonunits) 82.061/82.061 82.061/82.061 kept: 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.061/82.061 kept: 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.061/82.061 kept: 13 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.061/82.061 kept: 14 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.061/82.061 kept: 15 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.061/82.061 kept: 16 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.061/82.061 kept: 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.061/82.061 kept: 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.061/82.061 kept: 19 -->*_s0(c(g(x)),c(a)) | ->_s0(f(x,y),g(s(x))) # label(replacement). [clausify(8)]. 82.061/82.061 kept: 20 -->*_s0(c(h(x)),c(a)) | ->_s0(f(x,y),h(s(x))) # label(replacement). [clausify(9)]. 82.061/82.061 kept: 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 kept: 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 kept: 23 -->*_s0(c(h(x)),c(a)) | -->*_s0(c(g(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.061/82.061 82.061/82.061 ============================== end of process initial clauses ======== 82.061/82.061 82.061/82.061 ============================== CLAUSES FOR SEARCH ==================== 82.061/82.061 82.061/82.061 % Clauses after input processing: 82.061/82.061 82.061/82.061 formulas(usable). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(sos). 82.061/82.061 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.061/82.061 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.061/82.061 13 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.061/82.061 14 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.061/82.061 15 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.061/82.061 16 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.061/82.061 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.061/82.061 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.061/82.061 19 -->*_s0(c(g(x)),c(a)) | ->_s0(f(x,y),g(s(x))) # label(replacement). [clausify(8)]. 82.061/82.061 20 -->*_s0(c(h(x)),c(a)) | ->_s0(f(x,y),h(s(x))) # label(replacement). [clausify(9)]. 82.061/82.061 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 23 -->*_s0(c(h(x)),c(a)) | -->*_s0(c(g(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(demodulators). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 ============================== end of clauses for search ============= 82.061/82.061 82.061/82.061 ============================== SEARCH ================================ 82.061/82.061 82.061/82.061 % Starting search at 0.00 seconds. 82.061/82.061 82.061/82.061 given #1 (I,wt=3): 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.061/82.061 82.061/82.061 given #2 (I,wt=9): 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.061/82.061 82.061/82.061 given #3 (I,wt=10): 13 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 82.061/82.061 82.061/82.061 given #4 (I,wt=10): 14 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 82.061/82.061 82.061/82.061 given #5 (I,wt=8): 15 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 82.061/82.061 82.061/82.061 given #6 (I,wt=8): 16 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 82.061/82.061 82.061/82.061 given #7 (I,wt=8): 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.061/82.061 82.061/82.061 given #8 (I,wt=8): 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(7)]. 82.061/82.061 82.061/82.061 given #9 (I,wt=13): 19 -->*_s0(c(g(x)),c(a)) | ->_s0(f(x,y),g(s(x))) # label(replacement). [clausify(8)]. 82.061/82.061 82.061/82.061 given #10 (I,wt=13): 20 -->*_s0(c(h(x)),c(a)) | ->_s0(f(x,y),h(s(x))) # label(replacement). [clausify(9)]. 82.061/82.061 82.061/82.061 given #11 (I,wt=5): 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 82.061/82.061 given #12 (I,wt=5): 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 82.061/82.061 given #13 (I,wt=12): 23 -->*_s0(c(h(x)),c(a)) | -->*_s0(c(g(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.061/82.061 82.061/82.061 given #14 (A,wt=7): 24 ->_s0(s(g(s(x))),s(x)). [ur(18,a,21,a)]. 82.061/82.061 82.061/82.061 given #15 (F,wt=15): 38 -->*_s0(c(g(x)),c(a)) | -->_s0(c(h(x)),y) | -->*_s0(y,c(a)) # answer(goal). [resolve(23,a,12,c)]. 82.061/82.061 82.061/82.061 given #16 (F,wt=12): 49 -->*_s0(c(g(x)),c(a)) | -->_s0(c(h(x)),c(a)) # answer(goal). [resolve(38,c,11,a)]. 82.061/82.061 82.061/82.061 given #17 (F,wt=10): 51 -->*_s0(c(g(x)),c(a)) | -->_s0(h(x),a) # answer(goal). [resolve(49,b,17,b)]. 82.061/82.061 82.061/82.061 given #18 (F,wt=7): 53 -->*_s0(c(g(s(a))),c(a)) # answer(goal). [resolve(51,b,22,a)]. 82.061/82.061 82.061/82.061 ============================== PROOF ================================= 82.061/82.061 82.061/82.061 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 82.061/82.061 % Length of proof is 15. 82.061/82.061 % Level of proof is 6. 82.061/82.061 % Maximum clause weight is 15.000. 82.061/82.061 % Given clauses 18. 82.061/82.061 82.061/82.061 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 82.061/82.061 6 ->_s0(x1,y) -> ->_s0(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 10 (exists x3 (->*_s0(c(h(x3)),c(a)) & ->*_s0(c(g(x3)),c(a)))) # label(goal) # label(non_clause) # label(goal). [goal]. 82.061/82.061 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 82.061/82.061 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 82.061/82.061 17 -->_s0(x,y) | ->_s0(c(x),c(y)) # label(congruence). [clausify(6)]. 82.061/82.061 21 ->_s0(g(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 22 ->_s0(h(s(x)),x) # label(replacement). [assumption]. 82.061/82.061 23 -->*_s0(c(h(x)),c(a)) | -->*_s0(c(g(x)),c(a)) # label(goal) # answer(goal). [deny(10)]. 82.061/82.061 25 ->_s0(c(g(s(x))),c(x)). [ur(17,a,21,a)]. 82.061/82.061 38 -->*_s0(c(g(x)),c(a)) | -->_s0(c(h(x)),y) | -->*_s0(y,c(a)) # answer(goal). [resolve(23,a,12,c)]. 82.061/82.061 49 -->*_s0(c(g(x)),c(a)) | -->_s0(c(h(x)),c(a)) # answer(goal). [resolve(38,c,11,a)]. 82.061/82.061 51 -->*_s0(c(g(x)),c(a)) | -->_s0(h(x),a) # answer(goal). [resolve(49,b,17,b)]. 82.061/82.061 53 -->*_s0(c(g(s(a))),c(a)) # answer(goal). [resolve(51,b,22,a)]. 82.061/82.061 55 $F # answer(goal). [ur(12,b,11,a,c,53,a),unit_del(a,25)]. 82.061/82.061 82.061/82.061 ============================== end of proof ========================== 82.061/82.061 82.061/82.061 ============================== STATISTICS ============================ 82.061/82.061 82.061/82.061 Given=18. Generated=47. Kept=44. proofs=1. 82.061/82.061 Usable=18. Sos=25. Demods=0. Limbo=1, Disabled=13. Hints=0. 82.061/82.061 Kept_by_rule=0, Deleted_by_rule=0. 82.061/82.061 Forward_subsumed=2. Back_subsumed=0. 82.061/82.061 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 82.061/82.061 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 82.061/82.061 Demod_attempts=0. Demod_rewrites=0. 82.061/82.061 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 82.061/82.061 Nonunit_fsub_feature_tests=14. Nonunit_bsub_feature_tests=48. 82.061/82.061 Megabytes=0.12. 82.061/82.061 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 82.061/82.061 82.061/82.061 ============================== end of statistics ===================== 82.061/82.061 82.061/82.061 ============================== end of search ========================= 82.061/82.061 82.061/82.061 THEOREM PROVED 82.061/82.061 82.061/82.061 Exiting with 1 proof. 82.061/82.061 82.061/82.061 Process 54234 exit (max_proofs) Wed Jul 14 11:11:25 2021 82.061/82.061 82.061/82.061 82.061/82.061 The problem is feasible. 82.061/82.061 82.061/82.061 82.061/82.061 82.061/82.061 82.061/82.061 -> Problem conclusions: 82.061/82.061 Left linear, Right linear, Linear 82.061/82.061 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 82.061/82.061 CTRS Type: 1 82.061/82.061 Deterministic, Strongly deterministic 82.061/82.061 Oriented CTRS, Properly oriented CTRS, Not join CTRS 82.061/82.061 Maybe right-stable CTRS, Overlay CTRS 82.061/82.061 Maybe normal CTRS, Maybe almost normal CTRS 82.061/82.061 Maybe terminating CTRS, Maybe joinable CCPs 82.061/82.061 Maybe level confluent 82.061/82.061 Maybe confluent 82.061/82.061 82.061/82.061 Resulting CCPs: 82.061/82.061 | c(h(x:S)) ->* c(a), c(g(x:S)) ->* c(a) => Not trivial, Overlay, Feasible conditions, N1 82.061/82.061 82.061/82.061 Problem 1: 82.061/82.061 Underlying TRS Termination Processor: 82.061/82.061 82.061/82.061 Resulting Underlying TRS: 82.061/82.061 (VAR x:S y:S) 82.061/82.061 (STRATEGY CONTEXTSENSITIVE 82.061/82.061 (f 1 2) 82.061/82.061 (g 1) 82.061/82.061 (h 1) 82.061/82.061 ) 82.061/82.061 (RULES 82.061/82.061 f(x:S,y:S) -> g(s(x:S)) 82.061/82.061 f(x:S,y:S) -> h(s(x:S)) 82.061/82.061 g(s(x:S)) -> x:S 82.061/82.061 h(s(x:S)) -> x:S 82.061/82.061 ) 82.061/82.061 Underlying TRS terminating? 82.061/82.061 YES 82.061/82.061 82.061/82.061 Problem 1: 82.061/82.061 82.061/82.061 (VAR vu95NonEmpty:S xu58S:S yu58S:S) 82.061/82.061 (RULES 82.061/82.061 f(xu58S:S,yu58S:S) -> g(s(xu58S:S)) 82.061/82.061 f(xu58S:S,yu58S:S) -> h(s(xu58S:S)) 82.061/82.061 g(s(xu58S:S)) -> xu58S:S 82.061/82.061 h(s(xu58S:S)) -> xu58S:S 82.061/82.061 ) 82.061/82.061 82.061/82.061 Problem 1: 82.061/82.061 82.061/82.061 Dependency Pairs Processor: 82.061/82.061 -> Pairs: 82.061/82.061 F(xu58S:S,yu58S:S) -> G(s(xu58S:S)) 82.061/82.061 F(xu58S:S,yu58S:S) -> H(s(xu58S:S)) 82.061/82.061 -> Rules: 82.061/82.061 f(xu58S:S,yu58S:S) -> g(s(xu58S:S)) 82.061/82.061 f(xu58S:S,yu58S:S) -> h(s(xu58S:S)) 82.061/82.061 g(s(xu58S:S)) -> xu58S:S 82.061/82.061 h(s(xu58S:S)) -> xu58S:S 82.061/82.061 82.061/82.061 Problem 1: 82.061/82.061 82.061/82.061 SCC Processor: 82.061/82.061 -> Pairs: 82.061/82.061 F(xu58S:S,yu58S:S) -> G(s(xu58S:S)) 82.061/82.061 F(xu58S:S,yu58S:S) -> H(s(xu58S:S)) 82.061/82.061 -> Rules: 82.061/82.061 f(xu58S:S,yu58S:S) -> g(s(xu58S:S)) 82.061/82.061 f(xu58S:S,yu58S:S) -> h(s(xu58S:S)) 82.061/82.061 g(s(xu58S:S)) -> xu58S:S 82.061/82.061 h(s(xu58S:S)) -> xu58S:S 82.061/82.061 ->Strongly Connected Components: 82.061/82.061 There is no strongly connected component 82.061/82.061 82.061/82.061 The problem is finite. 82.061/82.061 82.061/82.061 82.061/82.061 -> Problem conclusions: 82.061/82.061 Left linear, Right linear, Linear 82.061/82.061 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 82.061/82.061 CTRS Type: 1 82.061/82.061 Deterministic, Strongly deterministic 82.061/82.061 Oriented CTRS, Properly oriented CTRS, Not join CTRS 82.061/82.061 Maybe right-stable CTRS, Overlay CTRS 82.061/82.061 Maybe normal CTRS, Maybe almost normal CTRS 82.061/82.061 Terminating CTRS, Maybe joinable CCPs 82.061/82.061 Maybe level confluent 82.061/82.061 Maybe confluent 82.061/82.061 82.061/82.061 Problem 1: 82.061/82.061 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.061/82.061 Confluence Problem: 82.061/82.061 (VAR x:S y:S) 82.061/82.061 (STRATEGY CONTEXTSENSITIVE 82.061/82.061 (f 1 2) 82.061/82.061 (g 1) 82.061/82.061 (h 1) 82.061/82.061 (a) 82.061/82.061 (c 1) 82.061/82.061 (fSNonEmpty) 82.061/82.061 (s 1) 82.061/82.061 ) 82.061/82.061 (RULES 82.061/82.061 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.061/82.061 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.061/82.061 g(s(x:S)) -> x:S 82.061/82.061 h(s(x:S)) -> x:S 82.061/82.061 ) 82.061/82.061 Critical Pairs: 82.061/82.061 | c(h(x:S)) ->* c(a), c(g(x:S)) ->* c(a) => Not trivial, Overlay, Feasible conditions, N1 82.061/82.061 Terminating:YES 82.061/82.061 82.061/82.061 -> Problem conclusions: 82.061/82.061 Left linear, Right linear, Linear 82.061/82.061 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 82.061/82.061 CTRS Type: 1 82.061/82.061 Deterministic, Strongly deterministic 82.061/82.061 Oriented CTRS, Properly oriented CTRS, Not join CTRS 82.061/82.061 Maybe right-stable CTRS, Overlay CTRS 82.061/82.061 Maybe normal CTRS, Maybe almost normal CTRS 82.061/82.061 Terminating CTRS, Maybe joinable CCPs 82.061/82.061 Maybe level confluent 82.061/82.061 Maybe confluent 82.061/82.061 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.061/82.061 82.061/82.061 Right Stable Processor: 82.061/82.061 Right-stable CTRS 82.061/82.061 Justification: 82.061/82.061 82.061/82.061 -> Term right-stability conditions: 82.061/82.061 Term: c(a) 82.061/82.061 Right-stable term 82.061/82.061 Linear constructor form 82.061/82.061 Don't know if term is a ground normal form (not needed) 82.061/82.061 Right-stability condition achieved 82.061/82.061 A call to InfChecker wasn't needed 82.061/82.061 82.061/82.061 82.061/82.061 -> Term right-stability conditions: 82.061/82.061 Term: c(a) 82.061/82.061 Right-stable term 82.061/82.061 Linear constructor form 82.061/82.061 Don't know if term is a ground normal form (not needed) 82.061/82.061 Right-stability condition achieved 82.061/82.061 A call to InfChecker wasn't needed 82.061/82.061 82.061/82.061 -> Problem conclusions: 82.061/82.061 Left linear, Right linear, Linear 82.061/82.061 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 82.061/82.061 CTRS Type: 1 82.061/82.061 Deterministic, Strongly deterministic 82.061/82.061 Oriented CTRS, Properly oriented CTRS, Not join CTRS 82.061/82.061 Right-stable CTRS, Overlay CTRS 82.061/82.061 Maybe normal CTRS, Almost normal CTRS 82.061/82.061 Terminating CTRS, Maybe joinable CCPs 82.061/82.061 Maybe level confluent 82.061/82.061 Maybe confluent 82.061/82.061 82.061/82.061 Problem 1: 82.061/82.061 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.061/82.061 Confluence Problem: 82.061/82.061 (VAR x:S y:S) 82.061/82.061 (STRATEGY CONTEXTSENSITIVE 82.061/82.061 (f 1 2) 82.061/82.061 (g 1) 82.061/82.061 (h 1) 82.061/82.061 (a) 82.061/82.061 (c 1) 82.061/82.061 (fSNonEmpty) 82.061/82.061 (s 1) 82.061/82.061 ) 82.061/82.061 (RULES 82.061/82.061 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.061/82.061 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.061/82.061 g(s(x:S)) -> x:S 82.061/82.061 h(s(x:S)) -> x:S 82.061/82.061 ) 82.061/82.061 Critical Pairs: 82.061/82.061 | c(h(x:S)) ->* c(a), c(g(x:S)) ->* c(a) => Not trivial, Overlay, Feasible conditions, N1 82.061/82.061 Terminating:YES 82.061/82.061 82.061/82.061 -> Problem conclusions: 82.061/82.061 Left linear, Right linear, Linear 82.061/82.061 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 82.061/82.061 CTRS Type: 1 82.061/82.061 Deterministic, Strongly deterministic 82.061/82.061 Oriented CTRS, Properly oriented CTRS, Not join CTRS 82.061/82.061 Right-stable CTRS, Overlay CTRS 82.061/82.061 Maybe normal CTRS, Almost normal CTRS 82.061/82.061 Terminating CTRS, Maybe joinable CCPs 82.061/82.061 Maybe level confluent 82.061/82.061 Maybe confluent 82.061/82.061 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.061/82.061 82.061/82.061 Normal RConds Processor: 82.061/82.061 YES 82.061/82.061 82.061/82.061 Problem 1: 82.061/82.061 82.061/82.061 Infeasibility Problem: 82.061/82.061 [(VAR vNonEmpty:S x:S y:S x1:S) 82.061/82.061 (STRATEGY CONTEXTSENSITIVE 82.061/82.061 (f 1 2) 82.061/82.061 (g 1) 82.061/82.061 (h 1) 82.061/82.061 (a) 82.061/82.061 (c 1) 82.061/82.061 (fSNonEmpty) 82.061/82.061 (s 1) 82.061/82.061 ) 82.061/82.061 (RULES 82.061/82.061 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.061/82.061 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.061/82.061 g(s(x:S)) -> x:S 82.061/82.061 h(s(x:S)) -> x:S 82.061/82.061 )] 82.061/82.061 82.061/82.061 Infeasibility Conditions: 82.061/82.061 c(a) -> x1:S 82.061/82.061 82.061/82.061 Problem 1: 82.061/82.061 82.061/82.061 Obtaining a model using Mace4: 82.061/82.061 82.061/82.061 -> Usable Rules: 82.061/82.061 Empty 82.061/82.061 82.061/82.061 -> Mace4 Output: 82.061/82.061 ============================== Mace4 ================================= 82.061/82.061 Mace4 (64) version 2009-11A, November 2009. 82.061/82.061 Process 54556 was started by ubuntu on ubuntu, 82.061/82.061 Wed Jul 14 11:12:19 2021 82.061/82.061 The command was "./mace4 -c -f /tmp/mace454544-2.in". 82.061/82.061 ============================== end of head =========================== 82.061/82.061 82.061/82.061 ============================== INPUT ================================= 82.061/82.061 82.061/82.061 % Reading from file /tmp/mace454544-2.in 82.061/82.061 82.061/82.061 assign(max_seconds,8). 82.061/82.061 82.061/82.061 formulas(assumptions). 82.061/82.061 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence). 82.061/82.061 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence). 82.061/82.061 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence). 82.061/82.061 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence). 82.061/82.061 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence). 82.061/82.061 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(goals). 82.061/82.061 (exists x3 ->(c(a),x3)) # label(goal). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 ============================== end of input ========================== 82.061/82.061 82.061/82.061 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 82.061/82.061 82.061/82.061 % Formulas that are not ordinary clauses: 82.061/82.061 1 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 2 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 3 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 4 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 5 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 6 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 82.061/82.061 7 (exists x3 ->(c(a),x3)) # label(goal) # label(non_clause) # label(goal). [goal]. 82.061/82.061 82.061/82.061 ============================== end of process non-clausal formulas === 82.061/82.061 82.061/82.061 ============================== CLAUSES FOR SEARCH ==================== 82.061/82.061 82.061/82.061 formulas(mace4_clauses). 82.061/82.061 -->(x,y) | ->(f(x,z),f(y,z)) # label(congruence). 82.061/82.061 -->(x,y) | ->(f(z,x),f(z,y)) # label(congruence). 82.061/82.061 -->(x,y) | ->(g(x),g(y)) # label(congruence). 82.061/82.061 -->(x,y) | ->(h(x),h(y)) # label(congruence). 82.061/82.061 -->(x,y) | ->(c(x),c(y)) # label(congruence). 82.061/82.061 -->(x,y) | ->(s(x),s(y)) # label(congruence). 82.061/82.061 -->(c(a),x) # label(goal). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 ============================== end of clauses for search ============= 82.061/82.061 82.061/82.061 % There are no natural numbers in the input. 82.061/82.061 82.061/82.061 ============================== DOMAIN SIZE 2 ========================= 82.061/82.061 82.061/82.061 ============================== MODEL ================================= 82.061/82.061 82.061/82.061 interpretation( 2, [number=1, seconds=0], [ 82.061/82.061 82.061/82.061 function(a, [ 0 ]), 82.061/82.061 82.061/82.061 function(g(_), [ 0, 0 ]), 82.061/82.061 82.061/82.061 function(h(_), [ 0, 0 ]), 82.061/82.061 82.061/82.061 function(c(_), [ 0, 0 ]), 82.061/82.061 82.061/82.061 function(s(_), [ 0, 0 ]), 82.061/82.061 82.061/82.061 function(f(_,_), [ 82.061/82.061 0, 0, 82.061/82.061 0, 0 ]), 82.061/82.061 82.061/82.061 relation(->(_,_), [ 82.061/82.061 0, 0, 82.061/82.061 0, 0 ]) 82.061/82.061 ]). 82.061/82.061 82.061/82.061 ============================== end of model ========================== 82.061/82.061 82.061/82.061 ============================== STATISTICS ============================ 82.061/82.061 82.061/82.061 For domain size 2. 82.061/82.061 82.061/82.061 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 82.061/82.061 Ground clauses: seen=34, kept=34. 82.061/82.061 Selections=13, assignments=13, propagations=4, current_models=1. 82.061/82.061 Rewrite_terms=68, rewrite_bools=39, indexes=6. 82.061/82.061 Rules_from_neg_clauses=0, cross_offs=0. 82.061/82.061 82.061/82.061 ============================== end of statistics ===================== 82.061/82.061 82.061/82.061 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 82.061/82.061 82.061/82.061 Exiting with 1 model. 82.061/82.061 82.061/82.061 Process 54556 exit (max_models) Wed Jul 14 11:12:19 2021 82.061/82.061 The process finished Wed Jul 14 11:12:19 2021 82.061/82.061 82.061/82.061 82.061/82.061 Mace4 cooked interpretation: 82.061/82.061 82.061/82.061 82.061/82.061 82.061/82.061 The problem is infeasible. 82.061/82.061 82.061/82.061 82.061/82.061 -> Problem conclusions: 82.061/82.061 Left linear, Right linear, Linear 82.061/82.061 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 82.061/82.061 CTRS Type: 1 82.061/82.061 Deterministic, Strongly deterministic 82.061/82.061 Oriented CTRS, Properly oriented CTRS, Not join CTRS 82.061/82.061 Right-stable CTRS, Overlay CTRS 82.061/82.061 Normal CTRS, Almost normal CTRS 82.061/82.061 Terminating CTRS, Maybe joinable CCPs 82.061/82.061 Maybe level confluent 82.061/82.061 Maybe confluent 82.061/82.061 82.061/82.061 Problem 1: 82.061/82.061 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.061/82.061 Confluence Problem: 82.061/82.061 (VAR x:S y:S) 82.061/82.061 (STRATEGY CONTEXTSENSITIVE 82.061/82.061 (f 1 2) 82.061/82.061 (g 1) 82.061/82.061 (h 1) 82.061/82.061 (a) 82.061/82.061 (c 1) 82.061/82.061 (fSNonEmpty) 82.061/82.061 (s 1) 82.061/82.061 ) 82.061/82.061 (RULES 82.061/82.061 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.061/82.061 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.061/82.061 g(s(x:S)) -> x:S 82.061/82.061 h(s(x:S)) -> x:S 82.061/82.061 ) 82.061/82.061 Critical Pairs: 82.061/82.061 | c(h(x:S)) ->* c(a), c(g(x:S)) ->* c(a) => Not trivial, Overlay, Feasible conditions, N1 82.061/82.061 Terminating:YES 82.061/82.061 82.061/82.061 -> Problem conclusions: 82.061/82.061 Left linear, Right linear, Linear 82.061/82.061 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 82.061/82.061 CTRS Type: 1 82.061/82.061 Deterministic, Strongly deterministic 82.061/82.061 Oriented CTRS, Properly oriented CTRS, Not join CTRS 82.061/82.061 Right-stable CTRS, Overlay CTRS 82.061/82.061 Normal CTRS, Almost normal CTRS 82.061/82.061 Terminating CTRS, Maybe joinable CCPs 82.061/82.061 Maybe level confluent 82.061/82.061 Maybe confluent 82.061/82.061 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.061/82.061 82.061/82.061 Conditional Critical Pairs Distributor Processor 82.061/82.061 Problem 1.1: 82.061/82.061 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.061/82.061 Confluence Problem: 82.061/82.061 (VAR x:S y:S) 82.061/82.061 (STRATEGY CONTEXTSENSITIVE 82.061/82.061 (f 1 2) 82.061/82.061 (g 1) 82.061/82.061 (h 1) 82.061/82.061 (a) 82.061/82.061 (c 1) 82.061/82.061 (fSNonEmpty) 82.061/82.061 (s 1) 82.061/82.061 ) 82.061/82.061 (RULES 82.061/82.061 f(x:S,y:S) -> g(s(x:S)) | c(g(x:S)) ->* c(a) 82.061/82.061 f(x:S,y:S) -> h(s(x:S)) | c(h(x:S)) ->* c(a) 82.061/82.061 g(s(x:S)) -> x:S 82.061/82.061 h(s(x:S)) -> x:S 82.061/82.061 ) 82.061/82.061 Critical Pairs: 82.061/82.061 | c(h(x:S)) ->* c(a), c(g(x:S)) ->* c(a) => Not trivial, Overlay, Feasible conditions, N1 82.061/82.061 Terminating:YES 82.061/82.061 82.061/82.061 -> Problem conclusions: 82.061/82.061 Left linear, Right linear, Linear 82.061/82.061 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 82.061/82.061 CTRS Type: 1 82.061/82.061 Deterministic, Strongly deterministic 82.061/82.061 Oriented CTRS, Properly oriented CTRS, Not join CTRS 82.061/82.061 Right-stable CTRS, Overlay CTRS 82.061/82.061 Normal CTRS, Almost normal CTRS 82.061/82.061 Terminating CTRS, Maybe joinable CCPs 82.061/82.061 Maybe level confluent 82.061/82.061 Maybe confluent 82.061/82.061 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 82.061/82.061 82.061/82.061 Prover9 CCP Convergence Checker Processor: 82.061/82.061 formulas(sos). 82.061/82.061 %Reflexivity 82.061/82.061 reds(x,x). 82.061/82.061 82.061/82.061 %Transitivity 82.061/82.061 (red(x,y) & reds(y,z)) -> reds(x,z). 82.061/82.061 82.061/82.061 %Congruence 82.061/82.061 red(x,y) -> red(f(x,z2),f(y,z2)). 82.061/82.061 red(x,y) -> red(f(z1,x),f(z1,y)). 82.061/82.061 red(x,y) -> red(g(x),g(y)). 82.061/82.061 red(x,y) -> red(h(x),h(y)). 82.061/82.061 82.061/82.061 red(x,y) -> red(c(x),c(y)). 82.061/82.061 82.061/82.061 red(x,y) -> red(s(x),s(y)). %Replacement 82.061/82.061 reds(c(g(x)),c(a)) -> red(f(x,y),g(s(x))). 82.061/82.061 reds(c(h(x)),c(a)) -> red(f(x,y),h(s(x))). 82.061/82.061 red(g(s(x)),x). 82.061/82.061 red(h(s(x)),x). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(goals). 82.061/82.061 exists z (reds(g(s(c_x)),z) & reds(h(s(c_x)),z)). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 Proof: 82.061/82.061 ============================== Prover9 =============================== 82.061/82.061 Prover9 (64) version 2009-11A, November 2009. 82.061/82.061 Process 54571 was started by ubuntu on ubuntu, 82.061/82.061 Wed Jul 14 11:12:43 2021 82.061/82.061 The command was "./prover9 -t 60 -f /tmp/prover954133-44.in". 82.061/82.061 ============================== end of head =========================== 82.061/82.061 82.061/82.061 ============================== INPUT ================================= 82.061/82.061 82.061/82.061 % Reading from file /tmp/prover954133-44.in 82.061/82.061 82.061/82.061 82.061/82.061 formulas(sos). 82.061/82.061 reds(x,x). 82.061/82.061 red(x,y) & reds(y,z) -> reds(x,z). 82.061/82.061 red(x,y) -> red(f(x,z2),f(y,z2)). 82.061/82.061 red(x,y) -> red(f(z1,x),f(z1,y)). 82.061/82.061 red(x,y) -> red(g(x),g(y)). 82.061/82.061 red(x,y) -> red(h(x),h(y)). 82.061/82.061 red(x,y) -> red(c(x),c(y)). 82.061/82.061 red(x,y) -> red(s(x),s(y)). 82.061/82.061 reds(c(g(x)),c(a)) -> red(f(x,y),g(s(x))). 82.061/82.061 reds(c(h(x)),c(a)) -> red(f(x,y),h(s(x))). 82.061/82.061 red(g(s(x)),x). 82.061/82.061 red(h(s(x)),x). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(goals). 82.061/82.061 (exists z (reds(g(s(c_x)),z) & reds(h(s(c_x)),z))). 82.061/82.061 end_of_list. 82.061/82.061 assign(max_megs,-1). 82.061/82.061 set(quiet). 82.061/82.061 82.061/82.061 ============================== end of input ========================== 82.061/82.061 82.061/82.061 % From the command line: assign(max_seconds, 60). 82.061/82.061 82.061/82.061 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 82.061/82.061 82.061/82.061 % Formulas that are not ordinary clauses: 82.061/82.061 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 82.061/82.061 2 red(x,y) -> red(f(x,z2),f(y,z2)) # label(non_clause). [assumption]. 82.061/82.061 3 red(x,y) -> red(f(z1,x),f(z1,y)) # label(non_clause). [assumption]. 82.061/82.061 4 red(x,y) -> red(g(x),g(y)) # label(non_clause). [assumption]. 82.061/82.061 5 red(x,y) -> red(h(x),h(y)) # label(non_clause). [assumption]. 82.061/82.061 6 red(x,y) -> red(c(x),c(y)) # label(non_clause). [assumption]. 82.061/82.061 7 red(x,y) -> red(s(x),s(y)) # label(non_clause). [assumption]. 82.061/82.061 8 reds(c(g(x)),c(a)) -> red(f(x,y),g(s(x))) # label(non_clause). [assumption]. 82.061/82.061 9 reds(c(h(x)),c(a)) -> red(f(x,y),h(s(x))) # label(non_clause). [assumption]. 82.061/82.061 10 (exists z (reds(g(s(c_x)),z) & reds(h(s(c_x)),z))) # label(non_clause) # label(goal). [goal]. 82.061/82.061 82.061/82.061 ============================== end of process non-clausal formulas === 82.061/82.061 82.061/82.061 ============================== PROCESS INITIAL CLAUSES =============== 82.061/82.061 82.061/82.061 % Clauses before input processing: 82.061/82.061 82.061/82.061 formulas(usable). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(sos). 82.061/82.061 reds(x,x). [assumption]. 82.061/82.061 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 82.061/82.061 -red(x,y) | red(f(x,z),f(y,z)). [clausify(2)]. 82.061/82.061 -red(x,y) | red(f(z,x),f(z,y)). [clausify(3)]. 82.061/82.061 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 82.061/82.061 -red(x,y) | red(h(x),h(y)). [clausify(5)]. 82.061/82.061 -red(x,y) | red(c(x),c(y)). [clausify(6)]. 82.061/82.061 -red(x,y) | red(s(x),s(y)). [clausify(7)]. 82.061/82.061 -reds(c(g(x)),c(a)) | red(f(x,y),g(s(x))). [clausify(8)]. 82.061/82.061 -reds(c(h(x)),c(a)) | red(f(x,y),h(s(x))). [clausify(9)]. 82.061/82.061 red(g(s(x)),x). [assumption]. 82.061/82.061 red(h(s(x)),x). [assumption]. 82.061/82.061 -reds(g(s(c_x)),x) | -reds(h(s(c_x)),x). [deny(10)]. 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(demodulators). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 ============================== PREDICATE ELIMINATION ================= 82.061/82.061 82.061/82.061 ============================== end predicate elimination ============= 82.061/82.061 82.061/82.061 Auto_denials: (no changes). 82.061/82.061 82.061/82.061 Term ordering decisions: 82.061/82.061 82.061/82.061 kept: 11 reds(x,x). [assumption]. 82.061/82.061 kept: 12 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 82.061/82.061 kept: 13 -red(x,y) | red(f(x,z),f(y,z)). [clausify(2)]. 82.061/82.061 kept: 14 -red(x,y) | red(f(z,x),f(z,y)). [clausify(3)]. 82.061/82.061 kept: 15 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 82.061/82.061 kept: 16 -red(x,y) | red(h(x),h(y)). [clausify(5)]. 82.061/82.061 kept: 17 -red(x,y) | red(c(x),c(y)). [clausify(6)]. 82.061/82.061 kept: 18 -red(x,y) | red(s(x),s(y)). [clausify(7)]. 82.061/82.061 kept: 19 -reds(c(g(x)),c(a)) | red(f(x,y),g(s(x))). [clausify(8)]. 82.061/82.061 kept: 20 -reds(c(h(x)),c(a)) | red(f(x,y),h(s(x))). [clausify(9)]. 82.061/82.061 kept: 21 red(g(s(x)),x). [assumption]. 82.061/82.061 kept: 22 red(h(s(x)),x). [assumption]. 82.061/82.061 kept: 23 -reds(g(s(c_x)),x) | -reds(h(s(c_x)),x). [deny(10)]. 82.061/82.061 82.061/82.061 ============================== end of process initial clauses ======== 82.061/82.061 82.061/82.061 ============================== CLAUSES FOR SEARCH ==================== 82.061/82.061 82.061/82.061 % Clauses after input processing: 82.061/82.061 82.061/82.061 formulas(usable). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(sos). 82.061/82.061 11 reds(x,x). [assumption]. 82.061/82.061 12 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 82.061/82.061 13 -red(x,y) | red(f(x,z),f(y,z)). [clausify(2)]. 82.061/82.061 14 -red(x,y) | red(f(z,x),f(z,y)). [clausify(3)]. 82.061/82.061 15 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 82.061/82.061 16 -red(x,y) | red(h(x),h(y)). [clausify(5)]. 82.061/82.061 17 -red(x,y) | red(c(x),c(y)). [clausify(6)]. 82.061/82.061 18 -red(x,y) | red(s(x),s(y)). [clausify(7)]. 82.061/82.061 19 -reds(c(g(x)),c(a)) | red(f(x,y),g(s(x))). [clausify(8)]. 82.061/82.061 20 -reds(c(h(x)),c(a)) | red(f(x,y),h(s(x))). [clausify(9)]. 82.061/82.061 21 red(g(s(x)),x). [assumption]. 82.061/82.061 22 red(h(s(x)),x). [assumption]. 82.061/82.061 23 -reds(g(s(c_x)),x) | -reds(h(s(c_x)),x). [deny(10)]. 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 formulas(demodulators). 82.061/82.061 end_of_list. 82.061/82.061 82.061/82.061 ============================== end of clauses for search ============= 82.061/82.061 82.061/82.061 ============================== SEARCH ================================ 82.061/82.061 82.061/82.061 % Starting search at 0.00 seconds. 82.061/82.061 82.061/82.061 given #1 (I,wt=3): 11 reds(x,x). [assumption]. 82.061/82.061 82.061/82.061 given #2 (I,wt=9): 12 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 82.061/82.061 82.061/82.061 given #3 (I,wt=10): 13 -red(x,y) | red(f(x,z),f(y,z)). [clausify(2)]. 82.061/82.061 82.061/82.061 given #4 (I,wt=10): 14 -red(x,y) | red(f(z,x),f(z,y)). [clausify(3)]. 82.061/82.061 82.061/82.061 given #5 (I,wt=8): 15 -red(x,y) | red(g(x),g(y)). [clausify(4)]. 82.061/82.061 82.061/82.061 given #6 (I,wt=8): 16 -red(x,y) | red(h(x),h(y)). [clausify(5)]. 82.061/82.061 82.061/82.061 given #7 (I,wt=8): 17 -red(x,y) | red(c(x),c(y)). [clausify(6)]. 82.061/82.061 82.061/82.061 given #8 (I,wt=8): 18 -red(x,y) | red(s(x),s(y)). [clausify(7)]. 82.061/82.061 82.061/82.061 given #9 (I,wt=13): 19 -reds(c(g(x)),c(a)) | red(f(x,y),g(s(x))). [clausify(8)]. 82.061/82.061 82.061/82.061 given #10 (I,wt=13): 20 -reds(c(h(x)),c(a)) | red(f(x,y),h(s(x))). [clausify(9)]. 82.061/82.061 82.061/82.061 given #11 (I,wt=5): 21 red(g(s(x)),x). [assumption]. 82.061/82.061 82.061/82.061 given #12 (I,wt=5): 22 red(h(s(x)),x). [assumption]. 82.061/82.061 82.061/82.061 given #13 (I,wt=10): 23 -reds(g(s(c_x)),x) | -reds(h(s(c_x)),x). [deny(10)]. 82.061/82.061 82.061/82.061 given #14 (A,wt=7): 24 red(s(g(s(x))),s(x)). [ur(18,a,21,a)]. 82.061/82.061 82.061/82.061 given #15 (F,wt=7): 39 -reds(h(s(c_x)),g(s(c_x))). [resolve(23,a,11,a)]. 82.061/82.061 82.061/82.061 given #16 (F,wt=5): 50 -reds(c_x,g(s(c_x))). [ur(12,a,22,a,c,39,a)]. 82.061/82.061 82.061/82.061 given #17 (F,wt=5): 52 -red(c_x,g(s(c_x))). [ur(12,b,11,a,c,50,a)]. 82.061/82.061 82.061/82.061 given #18 (F,wt=7): 41 -reds(g(s(c_x)),h(s(c_x))). [resolve(23,b,11,a)]. 82.061/82.061 82.061/82.061 given #19 (T,wt=5): 30 reds(g(s(x)),x). [ur(12,a,21,a,b,11,a)]. 82.061/82.061 82.061/82.061 ============================== PROOF ================================= 82.061/82.061 82.061/82.061 % Proof 1 at 0.00 (+ 0.00) seconds. 82.061/82.061 % Length of proof is 10. 82.061/82.061 % Level of proof is 3. 82.061/82.061 % Maximum clause weight is 10.000. 82.061/82.061 % Given clauses 19. 82.061/82.061 82.061/82.061 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 82.061/82.061 10 (exists z (reds(g(s(c_x)),z) & reds(h(s(c_x)),z))) # label(non_clause) # label(goal). [goal]. 82.061/82.061 11 reds(x,x). [assumption]. 82.061/82.061 12 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 82.061/82.061 21 red(g(s(x)),x). [assumption]. 82.061/82.061 22 red(h(s(x)),x). [assumption]. 82.061/82.061 23 -reds(g(s(c_x)),x) | -reds(h(s(c_x)),x). [deny(10)]. 82.061/82.061 30 reds(g(s(x)),x). [ur(12,a,21,a,b,11,a)]. 82.061/82.061 37 reds(h(s(x)),x). [ur(12,a,22,a,b,11,a)]. 82.061/82.061 56 $F. [resolve(30,a,23,a),unit_del(a,37)]. 82.061/82.061 82.061/82.061 ============================== end of proof ========================== 82.061/82.061 82.061/82.061 ============================== STATISTICS ============================ 82.061/82.061 82.061/82.061 Given=19. Generated=49. Kept=45. proofs=1. 82.061/82.061 Usable=19. Sos=26. Demods=0. Limbo=0, Disabled=13. Hints=0. 82.061/82.061 Kept_by_rule=0, Deleted_by_rule=0. 82.061/82.061 Forward_subsumed=3. Back_subsumed=0. 82.061/82.061 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 82.061/82.061 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 82.061/82.061 Demod_attempts=0. Demod_rewrites=0. 82.061/82.061 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 82.061/82.061 Nonunit_fsub_feature_tests=6. Nonunit_bsub_feature_tests=56. 82.061/82.061 Megabytes=0.12. 82.061/82.061 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 82.061/82.061 82.061/82.061 ============================== end of statistics ===================== 82.061/82.061 82.061/82.061 ============================== end of search ========================= 82.061/82.061 82.061/82.061 THEOREM PROVED 82.061/82.061 82.061/82.061 Exiting with 1 proof. 82.061/82.061 82.061/82.061 Process 54571 exit (max_proofs) Wed Jul 14 11:12:43 2021 82.061/82.061 82.061/82.061 82.061/82.061 The problem is joinable. 82.061/82.061 46.28user 3.19system 1:22.61elapsed 59%CPU (0avgtext+0avgdata 1960580maxresident)k 82.061/82.061 8inputs+0outputs (0major+669537minor)pagefaults 0swaps