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