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