20.021/20.021 NO 20.021/20.021 20.021/20.021 Problem 1: 20.021/20.021 20.021/20.021 20.021/20.021 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.021/20.021 Confluence Problem: 20.021/20.021 (VAR vNonEmpty x) 20.021/20.021 (REPLACEMENT-MAP 20.021/20.021 (a) 20.021/20.021 (f 1) 20.021/20.021 (s 1) 20.021/20.021 (b) 20.021/20.021 (fSNonEmpty) 20.021/20.021 (t 1) 20.021/20.021 ) 20.021/20.021 (RULES 20.021/20.021 a -> b 20.021/20.021 f(x) -> x | s(x) ->* t(x) 20.021/20.021 s(a) -> t(b) 20.021/20.021 ) 20.021/20.021 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.021/20.021 20.021/20.021 20.021/20.021 Problem 1: 20.021/20.021 20.021/20.021 Inlining of Conditions Processor [STERN17]: 20.021/20.021 20.021/20.021 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.021/20.021 Confluence Problem: 20.021/20.021 (VAR vNonEmpty x) 20.021/20.021 (REPLACEMENT-MAP 20.021/20.021 (a) 20.021/20.021 (f 1) 20.021/20.021 (s 1) 20.021/20.021 (b) 20.021/20.021 (fSNonEmpty) 20.021/20.021 (t 1) 20.021/20.021 ) 20.021/20.021 (RULES 20.021/20.021 a -> b 20.021/20.021 f(x) -> x | s(x) ->* t(x) 20.021/20.021 s(a) -> t(b) 20.021/20.021 ) 20.021/20.021 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.021/20.021 20.021/20.021 20.021/20.021 Problem 1: 20.021/20.021 20.021/20.021 Clean CTRS Processor: 20.021/20.021 20.021/20.021 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.021/20.021 Confluence Problem: 20.021/20.021 (REPLACEMENT-MAP 20.021/20.021 (a) 20.021/20.021 (f 1) 20.021/20.021 (s 1) 20.021/20.021 (b) 20.021/20.021 (fSNonEmpty) 20.021/20.021 (t 1) 20.021/20.021 ) 20.021/20.021 (RULES 20.021/20.021 a -> b 20.021/20.021 s(a) -> t(b) 20.021/20.021 ) 20.021/20.021 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.021/20.021 20.021/20.021 CRule InfChecker Info: 20.021/20.021 a -> b 20.021/20.021 Rule remains 20.021/20.021 Proof: 20.021/20.021 NO_CONDS 20.021/20.021 20.021/20.021 CRule InfChecker Info: 20.021/20.021 f(x) -> x | s(x) ->* t(x) 20.021/20.021 Rule deleted 20.021/20.021 Proof: 20.021/20.021 YES 20.021/20.021 20.021/20.021 Problem 1: 20.021/20.021 20.021/20.021 Infeasibility Problem: 20.021/20.021 [(VAR vNonEmpty x vNonEmpty x) 20.021/20.021 (STRATEGY CONTEXTSENSITIVE 20.021/20.021 (a) 20.021/20.021 (f 1) 20.021/20.021 (s 1) 20.021/20.021 (b) 20.021/20.021 (fSNonEmpty) 20.021/20.021 (t 1) 20.021/20.021 ) 20.021/20.021 (RULES 20.021/20.021 a -> b 20.021/20.021 f(x) -> x | s(x) ->* t(x) 20.021/20.021 s(a) -> t(b) 20.021/20.021 )] 20.021/20.021 20.021/20.021 Infeasibility Conditions: 20.021/20.021 s(x) ->* t(x) 20.021/20.021 20.021/20.021 Problem 1: 20.021/20.021 20.021/20.021 Obtaining a model using Mace4: 20.021/20.021 20.021/20.021 -> Usable Rules: 20.021/20.021 a -> b 20.021/20.021 f(x) -> x | s(x) ->* t(x) 20.021/20.021 s(a) -> t(b) 20.021/20.021 20.021/20.021 -> Mace4 Output: 20.021/20.021 ============================== Mace4 ================================= 20.021/20.021 Mace4 (64) version 2009-11A, November 2009. 20.021/20.021 Process 59716 was started by ubuntu on ubuntu, 20.021/20.021 Wed Mar 9 09:42:46 2022 20.021/20.021 The command was "./mace4 -c -f /tmp/mace459704-2.in". 20.021/20.021 ============================== end of head =========================== 20.021/20.021 20.021/20.021 ============================== INPUT ================================= 20.021/20.021 20.021/20.021 % Reading from file /tmp/mace459704-2.in 20.021/20.021 20.021/20.021 assign(max_seconds,20). 20.021/20.021 20.021/20.021 formulas(assumptions). 20.021/20.021 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence). 20.021/20.021 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 20.021/20.021 ->(x1,y) -> ->(t(x1),t(y)) # label(congruence). 20.021/20.021 ->(a,b) # label(replacement). 20.021/20.021 ->*(s(x1),t(x1)) -> ->(f(x1),x1) # label(replacement). 20.021/20.021 ->(s(a),t(b)) # label(replacement). 20.021/20.021 ->*(x,x) # label(reflexivity). 20.021/20.021 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 20.021/20.021 end_of_list. 20.021/20.021 20.021/20.021 formulas(goals). 20.021/20.021 (exists x3 ->*(s(x3),t(x3))) # label(goal). 20.021/20.021 end_of_list. 20.021/20.021 20.021/20.021 ============================== end of input ========================== 20.021/20.021 20.021/20.021 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 20.021/20.021 20.021/20.021 % Formulas that are not ordinary clauses: 20.021/20.021 1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 20.021/20.021 2 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 20.021/20.021 3 ->(x1,y) -> ->(t(x1),t(y)) # label(congruence) # label(non_clause). [assumption]. 20.021/20.021 4 ->*(s(x1),t(x1)) -> ->(f(x1),x1) # label(replacement) # label(non_clause). [assumption]. 20.021/20.021 5 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 20.021/20.021 6 (exists x3 ->*(s(x3),t(x3))) # label(goal) # label(non_clause) # label(goal). [goal]. 20.021/20.021 20.021/20.021 ============================== end of process non-clausal formulas === 20.021/20.021 20.021/20.021 ============================== CLAUSES FOR SEARCH ==================== 20.021/20.021 20.021/20.021 formulas(mace4_clauses). 20.021/20.021 -->(x,y) | ->(f(x),f(y)) # label(congruence). 20.021/20.021 -->(x,y) | ->(s(x),s(y)) # label(congruence). 20.021/20.021 -->(x,y) | ->(t(x),t(y)) # label(congruence). 20.021/20.021 ->(a,b) # label(replacement). 20.021/20.021 -->*(s(x),t(x)) | ->(f(x),x) # label(replacement). 20.021/20.021 ->(s(a),t(b)) # label(replacement). 20.021/20.021 ->*(x,x) # label(reflexivity). 20.021/20.021 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 20.021/20.021 -->*(s(x),t(x)) # label(goal). 20.021/20.021 end_of_list. 20.021/20.021 20.021/20.021 ============================== end of clauses for search ============= 20.021/20.021 20.021/20.021 % There are no natural numbers in the input. 20.021/20.021 20.021/20.021 ============================== DOMAIN SIZE 2 ========================= 20.021/20.021 20.021/20.021 ============================== STATISTICS ============================ 20.021/20.021 20.021/20.021 For domain size 2. 20.021/20.021 20.021/20.021 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 20.021/20.021 Ground clauses: seen=28, kept=24. 20.021/20.021 Selections=8, assignments=15, propagations=35, current_models=0. 20.021/20.021 Rewrite_terms=141, rewrite_bools=81, indexes=34. 20.021/20.021 Rules_from_neg_clauses=13, cross_offs=13. 20.021/20.021 20.021/20.021 ============================== end of statistics ===================== 20.021/20.021 20.021/20.021 ============================== DOMAIN SIZE 3 ========================= 20.021/20.021 20.021/20.021 ============================== MODEL ================================= 20.021/20.021 20.021/20.021 interpretation( 3, [number=1, seconds=0], [ 20.021/20.021 20.021/20.021 function(a, [ 0 ]), 20.021/20.021 20.021/20.021 function(b, [ 1 ]), 20.021/20.021 20.021/20.021 function(f(_), [ 0, 0, 0 ]), 20.021/20.021 20.021/20.021 function(s(_), [ 0, 1, 0 ]), 20.021/20.021 20.021/20.021 function(t(_), [ 2, 0, 2 ]), 20.021/20.021 20.021/20.021 relation(->*(_,_), [ 20.021/20.021 1, 1, 0, 20.021/20.021 0, 1, 0, 20.021/20.021 1, 1, 1 ]), 20.021/20.021 20.021/20.021 relation(->(_,_), [ 20.021/20.021 1, 1, 0, 20.021/20.021 0, 0, 0, 20.021/20.021 1, 0, 1 ]) 20.021/20.021 ]). 20.021/20.021 20.021/20.021 ============================== end of model ========================== 20.021/20.021 20.021/20.021 ============================== STATISTICS ============================ 20.021/20.021 20.021/20.021 For domain size 3. 20.021/20.021 20.021/20.021 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 20.021/20.021 Ground clauses: seen=65, kept=56. 20.021/20.021 Selections=17, assignments=32, propagations=47, current_models=1. 20.021/20.021 Rewrite_terms=235, rewrite_bools=195, indexes=43. 20.021/20.021 Rules_from_neg_clauses=5, cross_offs=17. 20.021/20.021 20.021/20.021 ============================== end of statistics ===================== 20.021/20.021 20.021/20.021 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 20.021/20.021 20.021/20.021 Exiting with 1 model. 20.021/20.021 20.021/20.021 Process 59716 exit (max_models) Wed Mar 9 09:42:46 2022 20.021/20.021 The process finished Wed Mar 9 09:42:46 2022 20.021/20.021 20.021/20.021 20.021/20.021 Mace4 cooked interpretation: 20.021/20.021 20.021/20.021 20.021/20.021 20.021/20.021 The problem is infeasible. 20.021/20.021 20.021/20.021 20.021/20.021 CRule InfChecker Info: 20.021/20.021 s(a) -> t(b) 20.021/20.021 Rule remains 20.021/20.021 Proof: 20.021/20.021 NO_CONDS 20.021/20.021 20.021/20.021 Problem 1: 20.021/20.021 20.021/20.021 Transform No Conds CTRS Processor: 20.021/20.021 20.021/20.021 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.021/20.021 Confluence Problem: 20.021/20.021 (REPLACEMENT-MAP 20.021/20.021 (a) 20.021/20.021 (f 1) 20.021/20.021 (s 1) 20.021/20.021 (b) 20.021/20.021 (fSNonEmpty) 20.021/20.021 (t 1) 20.021/20.021 ) 20.021/20.021 (RULES 20.021/20.021 a -> b 20.021/20.021 s(a) -> t(b) 20.021/20.021 ) 20.021/20.021 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.021/20.021 Resulting R: 20.021/20.021 (STRATEGY CONTEXTSENSITIVE 20.021/20.021 (a) 20.021/20.021 (f 1) 20.021/20.021 (s 1) 20.021/20.021 (b) 20.021/20.021 (fSNonEmpty) 20.021/20.021 (t 1) 20.021/20.021 ) 20.021/20.021 (RULES 20.021/20.021 a -> b 20.021/20.021 s(a) -> t(b) 20.021/20.021 ) 20.021/20.021 20.021/20.021 Problem 1: 20.021/20.021 20.021/20.021 CleanTRS Processor: 20.021/20.021 20.021/20.021 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.021/20.021 Confluence Problem: 20.021/20.021 (REPLACEMENT-MAP 20.021/20.021 (a) 20.021/20.021 (f 1) 20.021/20.021 (s 1) 20.021/20.021 (b) 20.021/20.021 (fSNonEmpty) 20.021/20.021 (t 1) 20.021/20.021 ) 20.021/20.021 (RULES 20.021/20.021 a -> b 20.021/20.021 s(a) -> t(b) 20.021/20.021 ) 20.021/20.021 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.021/20.021 20.021/20.021 20.021/20.021 Problem 1: 20.021/20.021 20.021/20.021 Modular Confluence Combinations Decomposition Processor: 20.021/20.021 20.021/20.021 No usable combinations 20.021/20.021 20.021/20.021 Problem 1: 20.021/20.021 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.021/20.021 Confluence Problem: 20.021/20.021 (REPLACEMENT-MAP 20.021/20.021 (a) 20.021/20.021 (f 1) 20.021/20.021 (s 1) 20.021/20.021 (b) 20.021/20.021 (fSNonEmpty) 20.021/20.021 (t 1) 20.021/20.021 ) 20.021/20.021 (RULES 20.021/20.021 a -> b 20.021/20.021 s(a) -> t(b) 20.021/20.021 ) 20.021/20.021 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.021/20.021 20.021/20.021 Huet Levy Processor: 20.021/20.021 -> Rules: 20.021/20.021 a -> b 20.021/20.021 s(a) -> t(b) 20.021/20.021 -> Vars: 20.021/20.021 20.021/20.021 20.021/20.021 -> Rlps: 20.021/20.021 (rule: a -> b, id: 1, possubterms: a->[]) 20.021/20.021 (rule: s(a) -> t(b), id: 2, possubterms: s(a)->[], a->[1]) 20.021/20.021 20.021/20.021 -> Unifications: 20.021/20.021 (R2 unifies with R1 at p: [1], l: s(a), lp: a, sig: {}, l': a, r: t(b), r': b) 20.021/20.021 20.021/20.021 -> Critical pairs info: 20.021/20.021 => Not trivial, Not overlay, NW0, N1 20.021/20.021 20.021/20.021 -> Problem conclusions: 20.021/20.021 Left linear, Right linear, Linear 20.021/20.021 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 20.021/20.021 Not Huet-Levy confluent, Not Newman confluent 20.021/20.021 R is a TRS 20.021/20.021 20.021/20.021 20.021/20.021 Problem 1: 20.021/20.021 Different Normal CP Terms Processor: 20.021/20.021 => Not trivial, Not overlay, NW0, N1, Normal and not trivial cp 20.021/20.021 20.021/20.021 The problem is not joinable. 20.021/20.021 32.46user 0.49system 0:20.21elapsed 163%CPU (0avgtext+0avgdata 95236maxresident)k 20.021/20.021 8inputs+0outputs (0major+53316minor)pagefaults 0swaps