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