25.037/25.037 YES 25.037/25.037 25.037/25.037 Problem 1: 25.037/25.037 25.037/25.037 25.037/25.037 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.037/25.037 Confluence Problem: 25.037/25.037 (VAR vNonEmpty:S x:S) 25.037/25.037 (STRATEGY CONTEXTSENSITIVE 25.037/25.037 (a) 25.037/25.037 (b) 25.037/25.037 (c) 25.037/25.037 (f 1) 25.037/25.037 (fSNonEmpty) 25.037/25.037 ) 25.037/25.037 (RULES 25.037/25.037 a -> b 25.037/25.037 b -> c 25.037/25.037 c -> b 25.037/25.037 f(x:S) -> x:S | x:S ->* a, b ->* x:S 25.037/25.037 ) 25.037/25.037 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.037/25.037 25.037/25.037 25.037/25.037 Problem 1: 25.037/25.037 25.037/25.037 Inlining of Conditions Processor [STERN17]: 25.037/25.037 25.037/25.037 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.037/25.037 Confluence Problem: 25.037/25.037 (VAR vNonEmpty:S x:S) 25.037/25.037 (STRATEGY CONTEXTSENSITIVE 25.037/25.037 (a) 25.037/25.037 (b) 25.037/25.037 (c) 25.037/25.037 (f 1) 25.037/25.037 (fSNonEmpty) 25.037/25.037 ) 25.037/25.037 (RULES 25.037/25.037 a -> b 25.037/25.037 b -> c 25.037/25.037 c -> b 25.037/25.037 f(x:S) -> x:S | b ->* x:S, x:S ->* a 25.037/25.037 ) 25.037/25.037 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.037/25.037 25.037/25.037 25.037/25.037 Problem 1: 25.037/25.037 25.037/25.037 Clean CTRS Processor: 25.037/25.037 25.037/25.037 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.037/25.037 Confluence Problem: 25.037/25.037 (STRATEGY CONTEXTSENSITIVE 25.037/25.037 (a) 25.037/25.037 (b) 25.037/25.037 (c) 25.037/25.037 (f 1) 25.037/25.037 (fSNonEmpty) 25.037/25.037 ) 25.037/25.037 (RULES 25.037/25.037 a -> b 25.037/25.037 b -> c 25.037/25.037 c -> b 25.037/25.037 ) 25.037/25.037 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.037/25.037 25.037/25.037 CRule InfChecker Info: 25.037/25.037 a -> b 25.037/25.037 Rule remains 25.037/25.037 Proof: 25.037/25.037 NO_CONDS 25.037/25.037 25.037/25.037 CRule InfChecker Info: 25.037/25.037 b -> c 25.037/25.037 Rule remains 25.037/25.037 Proof: 25.037/25.037 NO_CONDS 25.037/25.037 25.037/25.037 CRule InfChecker Info: 25.037/25.037 c -> b 25.037/25.037 Rule remains 25.037/25.037 Proof: 25.037/25.037 NO_CONDS 25.037/25.037 25.037/25.037 CRule InfChecker Info: 25.037/25.037 f(x:S) -> x:S | b ->* x:S, x:S ->* a 25.037/25.037 Rule deleted 25.037/25.037 Proof: 25.037/25.037 YES 25.037/25.037 25.037/25.037 Problem 1: 25.037/25.037 25.037/25.037 Infeasibility Problem: 25.037/25.037 [(VAR vNonEmpty:S vNonEmpty:S:S x:S:S) 25.037/25.037 (STRATEGY CONTEXTSENSITIVE 25.037/25.037 (a) 25.037/25.037 (b) 25.037/25.037 (c) 25.037/25.037 (f 1) 25.037/25.037 (fSNonEmpty) 25.037/25.037 ) 25.037/25.037 (RULES 25.037/25.037 a -> b 25.037/25.037 b -> c 25.037/25.037 c -> b 25.037/25.037 f(x:S:S) -> x:S:S | b ->* x:S:S, x:S:S ->* a 25.037/25.037 )] 25.037/25.037 25.037/25.037 Infeasibility Conditions: 25.037/25.037 b ->* x:S:S, x:S:S ->* a 25.037/25.037 25.037/25.037 Problem 1: 25.037/25.037 25.037/25.037 Obtaining a model using Mace4: 25.037/25.037 25.037/25.037 -> Usable Rules: 25.037/25.037 a -> b 25.037/25.037 b -> c 25.037/25.037 c -> b 25.037/25.037 f(x:S:S) -> x:S:S | b ->* x:S:S, x:S:S ->* a 25.037/25.037 25.037/25.037 -> Mace4 Output: 25.037/25.037 ============================== Mace4 ================================= 25.037/25.037 Mace4 (64) version 2009-11A, November 2009. 25.037/25.037 Process 62968 was started by ubuntu on ubuntu, 25.037/25.037 Wed Jul 14 11:41:17 2021 25.037/25.037 The command was "./mace4 -c -f /tmp/mace462955-2.in". 25.037/25.037 ============================== end of head =========================== 25.037/25.037 25.037/25.037 ============================== INPUT ================================= 25.037/25.037 25.037/25.037 % Reading from file /tmp/mace462955-2.in 25.037/25.037 25.037/25.037 assign(max_seconds,20). 25.037/25.037 25.037/25.037 formulas(assumptions). 25.037/25.037 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence). 25.037/25.037 ->(a,b) # label(replacement). 25.037/25.037 ->(b,c) # label(replacement). 25.037/25.037 ->(c,b) # label(replacement). 25.037/25.037 ->*(b,x2) & ->*(x2,a) -> ->(f(x2),x2) # label(replacement). 25.037/25.037 ->*(x,x) # label(reflexivity). 25.037/25.037 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 25.037/25.037 end_of_list. 25.037/25.037 25.037/25.037 formulas(goals). 25.037/25.037 (exists x2 (->*(b,x2) & ->*(x2,a))) # label(goal). 25.037/25.037 end_of_list. 25.037/25.037 25.037/25.037 ============================== end of input ========================== 25.037/25.037 25.037/25.037 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 25.037/25.037 25.037/25.037 % Formulas that are not ordinary clauses: 25.037/25.037 1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 25.037/25.037 2 ->*(b,x2) & ->*(x2,a) -> ->(f(x2),x2) # label(replacement) # label(non_clause). [assumption]. 25.037/25.037 3 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 25.037/25.037 4 (exists x2 (->*(b,x2) & ->*(x2,a))) # label(goal) # label(non_clause) # label(goal). [goal]. 25.037/25.037 25.037/25.037 ============================== end of process non-clausal formulas === 25.037/25.037 25.037/25.037 ============================== CLAUSES FOR SEARCH ==================== 25.037/25.037 25.037/25.037 formulas(mace4_clauses). 25.037/25.037 -->(x,y) | ->(f(x),f(y)) # label(congruence). 25.037/25.037 ->(a,b) # label(replacement). 25.037/25.037 ->(b,c) # label(replacement). 25.037/25.037 ->(c,b) # label(replacement). 25.037/25.037 -->*(b,x) | -->*(x,a) | ->(f(x),x) # label(replacement). 25.037/25.037 ->*(x,x) # label(reflexivity). 25.037/25.037 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 25.037/25.037 -->*(b,x) | -->*(x,a) # label(goal). 25.037/25.037 end_of_list. 25.037/25.037 25.037/25.037 ============================== end of clauses for search ============= 25.037/25.037 25.037/25.037 % There are no natural numbers in the input. 25.037/25.037 25.037/25.037 ============================== DOMAIN SIZE 2 ========================= 25.037/25.037 25.037/25.037 ============================== MODEL ================================= 25.037/25.037 25.037/25.037 interpretation( 2, [number=1, seconds=0], [ 25.037/25.037 25.037/25.037 function(a, [ 0 ]), 25.037/25.037 25.037/25.037 function(b, [ 1 ]), 25.037/25.037 25.037/25.037 function(c, [ 1 ]), 25.037/25.037 25.037/25.037 function(f(_), [ 0, 1 ]), 25.037/25.037 25.037/25.037 relation(->*(_,_), [ 25.037/25.037 1, 1, 25.037/25.037 0, 1 ]), 25.037/25.037 25.037/25.037 relation(->(_,_), [ 25.037/25.037 0, 1, 25.037/25.037 0, 1 ]) 25.037/25.037 ]). 25.037/25.037 25.037/25.037 ============================== end of model ========================== 25.037/25.037 25.037/25.037 ============================== STATISTICS ============================ 25.037/25.037 25.037/25.037 For domain size 2. 25.037/25.037 25.037/25.037 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 25.037/25.037 Ground clauses: seen=21, kept=17. 25.037/25.037 Selections=3, assignments=3, propagations=10, current_models=1. 25.037/25.037 Rewrite_terms=24, rewrite_bools=27, indexes=6. 25.037/25.037 Rules_from_neg_clauses=3, cross_offs=3. 25.037/25.037 25.037/25.037 ============================== end of statistics ===================== 25.037/25.037 25.037/25.037 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 25.037/25.037 25.037/25.037 Exiting with 1 model. 25.037/25.037 25.037/25.037 Process 62968 exit (max_models) Wed Jul 14 11:41:17 2021 25.037/25.037 The process finished Wed Jul 14 11:41:17 2021 25.037/25.037 25.037/25.037 25.037/25.037 Mace4 cooked interpretation: 25.037/25.037 25.037/25.037 25.037/25.037 25.037/25.037 The problem is infeasible. 25.037/25.037 25.037/25.037 25.037/25.037 Problem 1: 25.037/25.037 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.037/25.037 Confluence Problem: 25.037/25.037 (STRATEGY CONTEXTSENSITIVE 25.037/25.037 (a) 25.037/25.037 (b) 25.037/25.037 (c) 25.037/25.037 (f 1) 25.037/25.037 (fSNonEmpty) 25.037/25.037 ) 25.037/25.037 (RULES 25.037/25.037 a -> b 25.037/25.037 b -> c 25.037/25.037 c -> b 25.037/25.037 ) 25.037/25.037 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.037/25.037 25.037/25.037 Critical Pairs Processor: 25.037/25.037 -> Rules: 25.037/25.037 a -> b 25.037/25.037 b -> c 25.037/25.037 c -> b 25.037/25.037 -> Vars: 25.037/25.037 25.037/25.037 -> FVars: 25.037/25.037 25.037/25.037 -> PVars: 25.037/25.037 25.037/25.037 25.037/25.037 -> Rlps: 25.037/25.037 crule: a -> b, id: 1, possubterms: a-> [] 25.037/25.037 crule: b -> c, id: 2, possubterms: b-> [] 25.037/25.037 crule: c -> b, id: 3, possubterms: c-> [] 25.037/25.037 25.037/25.037 -> Unifications: 25.037/25.037 25.037/25.037 25.037/25.037 -> Critical pairs info: 25.037/25.037 25.037/25.037 25.037/25.037 -> Problem conclusions: 25.037/25.037 Left linear, Right linear, Linear 25.037/25.037 Weakly orthogonal, Almost orthogonal, Orthogonal 25.037/25.037 CTRS Type: 1 25.037/25.037 Deterministic, Strongly deterministic 25.037/25.037 Oriented CTRS, Properly oriented CTRS, Join CTRS 25.037/25.037 Maybe right-stable CTRS, Overlay CTRS 25.037/25.037 Normal CTRS, Almost normal CTRS 25.037/25.037 Maybe terminating CTRS, Joinable CCPs 25.037/25.037 Level confluent 25.037/25.037 Confluent 25.037/25.037 25.037/25.037 The problem is joinable. 25.037/25.037 24.70user 0.52system 0:25.37elapsed 99%CPU (0avgtext+0avgdata 135872maxresident)k 25.037/25.037 8inputs+0outputs (0major+96150minor)pagefaults 0swaps