25.033/25.033 YES 25.033/25.033 25.033/25.033 Problem 1: 25.033/25.033 25.033/25.033 25.033/25.033 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.033/25.033 Confluence Problem: 25.033/25.033 (VAR vNonEmpty x) 25.033/25.033 (REPLACEMENT-MAP 25.033/25.033 (a) 25.033/25.033 (b) 25.033/25.033 (c) 25.033/25.033 (f 1) 25.033/25.033 (fSNonEmpty) 25.033/25.033 ) 25.033/25.033 (RULES 25.033/25.033 a -> b 25.033/25.033 b -> c 25.033/25.033 c -> b 25.033/25.033 f(x) -> x | x ->* a, b ->* x 25.033/25.033 ) 25.033/25.033 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.033/25.033 25.033/25.033 25.033/25.033 Problem 1: 25.033/25.033 25.033/25.033 Inlining of Conditions Processor [STERN17]: 25.033/25.033 25.033/25.033 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.033/25.033 Confluence Problem: 25.033/25.033 (VAR vNonEmpty x) 25.033/25.033 (REPLACEMENT-MAP 25.033/25.033 (a) 25.033/25.033 (b) 25.033/25.033 (c) 25.033/25.033 (f 1) 25.033/25.033 (fSNonEmpty) 25.033/25.033 ) 25.033/25.033 (RULES 25.033/25.033 a -> b 25.033/25.033 b -> c 25.033/25.033 c -> b 25.033/25.033 f(x) -> x | b ->* x, x ->* a 25.033/25.033 ) 25.033/25.033 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.033/25.033 25.033/25.033 25.033/25.033 Problem 1: 25.033/25.033 25.033/25.033 Clean CTRS Processor: 25.033/25.033 25.033/25.033 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.033/25.033 Confluence Problem: 25.033/25.033 (REPLACEMENT-MAP 25.033/25.033 (a) 25.033/25.033 (b) 25.033/25.033 (c) 25.033/25.033 (f 1) 25.033/25.033 (fSNonEmpty) 25.033/25.033 ) 25.033/25.033 (RULES 25.033/25.033 a -> b 25.033/25.033 b -> c 25.033/25.033 c -> b 25.033/25.033 ) 25.033/25.033 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.033/25.033 25.033/25.033 CRule InfChecker Info: 25.033/25.033 a -> b 25.033/25.033 Rule remains 25.033/25.033 Proof: 25.033/25.033 NO_CONDS 25.033/25.033 25.033/25.033 CRule InfChecker Info: 25.033/25.033 b -> c 25.033/25.033 Rule remains 25.033/25.033 Proof: 25.033/25.033 NO_CONDS 25.033/25.033 25.033/25.033 CRule InfChecker Info: 25.033/25.033 c -> b 25.033/25.033 Rule remains 25.033/25.033 Proof: 25.033/25.033 NO_CONDS 25.033/25.033 25.033/25.033 CRule InfChecker Info: 25.033/25.033 f(x) -> x | b ->* x, x ->* a 25.033/25.033 Rule deleted 25.033/25.033 Proof: 25.033/25.033 YES 25.033/25.033 25.033/25.033 Problem 1: 25.033/25.033 25.033/25.033 Infeasibility Problem: 25.033/25.033 [(VAR vNonEmpty x vNonEmpty x) 25.033/25.033 (STRATEGY CONTEXTSENSITIVE 25.033/25.033 (a) 25.033/25.033 (b) 25.033/25.033 (c) 25.033/25.033 (f 1) 25.033/25.033 (fSNonEmpty) 25.033/25.033 ) 25.033/25.033 (RULES 25.033/25.033 a -> b 25.033/25.033 b -> c 25.033/25.033 c -> b 25.033/25.033 f(x) -> x | b ->* x, x ->* a 25.033/25.033 )] 25.033/25.033 25.033/25.033 Infeasibility Conditions: 25.033/25.033 b ->* x, x ->* a 25.033/25.033 25.033/25.033 Problem 1: 25.033/25.033 25.033/25.033 Obtaining a model using Mace4: 25.033/25.033 25.033/25.033 -> Usable Rules: 25.033/25.033 a -> b 25.033/25.033 b -> c 25.033/25.033 c -> b 25.033/25.033 f(x) -> x | b ->* x, x ->* a 25.033/25.033 25.033/25.033 -> Mace4 Output: 25.033/25.033 ============================== Mace4 ================================= 25.033/25.033 Mace4 (64) version 2009-11A, November 2009. 25.033/25.033 Process 79023 was started by ubuntu on ubuntu, 25.033/25.033 Wed Mar 9 10:22:04 2022 25.033/25.033 The command was "./mace4 -c -f /tmp/mace479012-2.in". 25.033/25.033 ============================== end of head =========================== 25.033/25.033 25.033/25.033 ============================== INPUT ================================= 25.033/25.033 25.033/25.033 % Reading from file /tmp/mace479012-2.in 25.033/25.033 25.033/25.033 assign(max_seconds,20). 25.033/25.033 25.033/25.033 formulas(assumptions). 25.033/25.033 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence). 25.033/25.033 ->(a,b) # label(replacement). 25.033/25.033 ->(b,c) # label(replacement). 25.033/25.033 ->(c,b) # label(replacement). 25.033/25.033 ->*(b,x1) & ->*(x1,a) -> ->(f(x1),x1) # label(replacement). 25.033/25.033 ->*(x,x) # label(reflexivity). 25.033/25.033 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 25.033/25.033 end_of_list. 25.033/25.033 25.033/25.033 formulas(goals). 25.033/25.033 (exists x3 (->*(b,x3) & ->*(x3,a))) # label(goal). 25.033/25.033 end_of_list. 25.033/25.033 25.033/25.033 ============================== end of input ========================== 25.033/25.033 25.033/25.033 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 25.033/25.033 25.033/25.033 % Formulas that are not ordinary clauses: 25.033/25.033 1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 25.033/25.033 2 ->*(b,x1) & ->*(x1,a) -> ->(f(x1),x1) # label(replacement) # label(non_clause). [assumption]. 25.033/25.033 3 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 25.033/25.033 4 (exists x3 (->*(b,x3) & ->*(x3,a))) # label(goal) # label(non_clause) # label(goal). [goal]. 25.033/25.033 25.033/25.033 ============================== end of process non-clausal formulas === 25.033/25.033 25.033/25.033 ============================== CLAUSES FOR SEARCH ==================== 25.033/25.033 25.033/25.033 formulas(mace4_clauses). 25.033/25.033 -->(x,y) | ->(f(x),f(y)) # label(congruence). 25.033/25.033 ->(a,b) # label(replacement). 25.033/25.033 ->(b,c) # label(replacement). 25.033/25.033 ->(c,b) # label(replacement). 25.033/25.033 -->*(b,x) | -->*(x,a) | ->(f(x),x) # label(replacement). 25.033/25.033 ->*(x,x) # label(reflexivity). 25.033/25.033 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 25.033/25.033 -->*(b,x) | -->*(x,a) # label(goal). 25.033/25.033 end_of_list. 25.033/25.033 25.033/25.033 ============================== end of clauses for search ============= 25.033/25.033 25.033/25.033 % There are no natural numbers in the input. 25.033/25.033 25.033/25.033 ============================== DOMAIN SIZE 2 ========================= 25.033/25.033 25.033/25.033 ============================== MODEL ================================= 25.033/25.033 25.033/25.033 interpretation( 2, [number=1, seconds=0], [ 25.033/25.033 25.033/25.033 function(a, [ 0 ]), 25.033/25.033 25.033/25.033 function(b, [ 1 ]), 25.033/25.033 25.033/25.033 function(c, [ 1 ]), 25.033/25.033 25.033/25.033 function(f(_), [ 0, 1 ]), 25.033/25.033 25.033/25.033 relation(->*(_,_), [ 25.033/25.033 1, 1, 25.033/25.033 0, 1 ]), 25.033/25.033 25.033/25.033 relation(->(_,_), [ 25.033/25.033 0, 1, 25.033/25.033 0, 1 ]) 25.033/25.033 ]). 25.033/25.033 25.033/25.033 ============================== end of model ========================== 25.033/25.033 25.033/25.033 ============================== STATISTICS ============================ 25.033/25.033 25.033/25.033 For domain size 2. 25.033/25.033 25.033/25.033 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 25.033/25.033 Ground clauses: seen=21, kept=17. 25.033/25.033 Selections=3, assignments=3, propagations=10, current_models=1. 25.033/25.033 Rewrite_terms=24, rewrite_bools=27, indexes=6. 25.033/25.033 Rules_from_neg_clauses=3, cross_offs=3. 25.033/25.033 25.033/25.033 ============================== end of statistics ===================== 25.033/25.033 25.033/25.033 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 25.033/25.033 25.033/25.033 Exiting with 1 model. 25.033/25.033 25.033/25.033 Process 79023 exit (max_models) Wed Mar 9 10:22:04 2022 25.033/25.033 The process finished Wed Mar 9 10:22:04 2022 25.033/25.033 25.033/25.033 25.033/25.033 Mace4 cooked interpretation: 25.033/25.033 25.033/25.033 25.033/25.033 25.033/25.033 The problem is infeasible. 25.033/25.033 25.033/25.033 25.033/25.033 Problem 1: 25.033/25.033 25.033/25.033 Transform No Conds CTRS Processor: 25.033/25.033 25.033/25.033 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.033/25.033 Confluence Problem: 25.033/25.033 (REPLACEMENT-MAP 25.033/25.033 (a) 25.033/25.033 (b) 25.033/25.033 (c) 25.033/25.033 (f 1) 25.033/25.033 (fSNonEmpty) 25.033/25.033 ) 25.033/25.033 (RULES 25.033/25.033 a -> b 25.033/25.033 b -> c 25.033/25.033 c -> b 25.033/25.033 ) 25.033/25.033 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.033/25.033 Resulting R: 25.033/25.033 (STRATEGY CONTEXTSENSITIVE 25.033/25.033 (a) 25.033/25.033 (b) 25.033/25.033 (c) 25.033/25.033 (f 1) 25.033/25.033 (fSNonEmpty) 25.033/25.033 ) 25.033/25.033 (RULES 25.033/25.033 a -> b 25.033/25.033 b -> c 25.033/25.033 c -> b 25.033/25.033 ) 25.033/25.033 25.033/25.033 Problem 1: 25.033/25.033 25.033/25.033 CleanTRS Processor: 25.033/25.033 25.033/25.033 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.033/25.033 Confluence Problem: 25.033/25.033 (REPLACEMENT-MAP 25.033/25.033 (a) 25.033/25.033 (b) 25.033/25.033 (c) 25.033/25.033 (f 1) 25.033/25.033 (fSNonEmpty) 25.033/25.033 ) 25.033/25.033 (RULES 25.033/25.033 a -> b 25.033/25.033 b -> c 25.033/25.033 c -> b 25.033/25.033 ) 25.033/25.033 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.033/25.033 25.033/25.033 25.033/25.033 Problem 1: 25.033/25.033 25.033/25.033 Modular Confluence Combinations Decomposition Processor: 25.033/25.033 25.033/25.033 No usable combinations 25.033/25.033 25.033/25.033 Problem 1: 25.033/25.033 Linearity Processor: 25.033/25.033 Linear? 25.033/25.033 YES 25.033/25.033 Problem 1.1: 25.033/25.033 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.033/25.033 Confluence Problem: 25.033/25.033 (REPLACEMENT-MAP 25.033/25.033 (a) 25.033/25.033 (b) 25.033/25.033 (c) 25.033/25.033 (f 1) 25.033/25.033 (fSNonEmpty) 25.033/25.033 ) 25.033/25.033 (RULES 25.033/25.033 a -> b 25.033/25.033 b -> c 25.033/25.033 c -> b 25.033/25.033 ) 25.033/25.033 Linear:YES 25.033/25.033 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.033/25.033 25.033/25.033 Huet Levy Processor: 25.033/25.033 -> Rules: 25.033/25.033 a -> b 25.033/25.033 b -> c 25.033/25.033 c -> b 25.033/25.033 -> Vars: 25.033/25.033 25.033/25.033 25.033/25.033 -> Rlps: 25.033/25.033 (rule: a -> b, id: 1, possubterms: a->[]) 25.033/25.033 (rule: b -> c, id: 2, possubterms: b->[]) 25.033/25.033 (rule: c -> b, id: 3, possubterms: c->[]) 25.033/25.033 25.033/25.033 -> Unifications: 25.033/25.033 25.033/25.033 25.033/25.033 -> Critical pairs info: 25.033/25.033 25.033/25.033 25.033/25.033 -> Problem conclusions: 25.033/25.033 Left linear, Right linear, Linear 25.033/25.033 Weakly orthogonal, Almost orthogonal, Orthogonal 25.033/25.033 Huet-Levy confluent, Not Newman confluent 25.033/25.033 R is a TRS 25.033/25.033 25.033/25.033 25.033/25.033 The problem is joinable. 25.033/25.033 25.00user 0.54system 0:25.33elapsed 100%CPU (0avgtext+0avgdata 136112maxresident)k 25.033/25.033 8inputs+0outputs (0major+95254minor)pagefaults 0swaps