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