25.006/25.006 YES 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 25.006/25.006 25.006/25.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.006/25.006 Confluence Problem: 25.006/25.006 (VAR vNonEmpty:S x:S) 25.006/25.006 (STRATEGY CONTEXTSENSITIVE 25.006/25.006 (f 1) 25.006/25.006 (g 1 2) 25.006/25.006 (a) 25.006/25.006 (b) 25.006/25.006 (c) 25.006/25.006 (fSNonEmpty) 25.006/25.006 ) 25.006/25.006 (RULES 25.006/25.006 f(x:S) -> c | a ->* b 25.006/25.006 g(x:S,x:S) -> g(f(a),f(b)) 25.006/25.006 ) 25.006/25.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.006/25.006 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 25.006/25.006 Inlining of Conditions Processor [STERN17]: 25.006/25.006 25.006/25.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.006/25.006 Confluence Problem: 25.006/25.006 (VAR vNonEmpty:S x:S) 25.006/25.006 (STRATEGY CONTEXTSENSITIVE 25.006/25.006 (f 1) 25.006/25.006 (g 1 2) 25.006/25.006 (a) 25.006/25.006 (b) 25.006/25.006 (c) 25.006/25.006 (fSNonEmpty) 25.006/25.006 ) 25.006/25.006 (RULES 25.006/25.006 f(x:S) -> c | a ->* b 25.006/25.006 g(x:S,x:S) -> g(f(a),f(b)) 25.006/25.006 ) 25.006/25.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.006/25.006 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 25.006/25.006 Clean CTRS Processor: 25.006/25.006 25.006/25.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.006/25.006 Confluence Problem: 25.006/25.006 (VAR x:S) 25.006/25.006 (STRATEGY CONTEXTSENSITIVE 25.006/25.006 (f 1) 25.006/25.006 (g 1 2) 25.006/25.006 (a) 25.006/25.006 (b) 25.006/25.006 (c) 25.006/25.006 (fSNonEmpty) 25.006/25.006 ) 25.006/25.006 (RULES 25.006/25.006 g(x:S,x:S) -> g(f(a),f(b)) 25.006/25.006 ) 25.006/25.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.006/25.006 25.006/25.006 CRule InfChecker Info: 25.006/25.006 f(x:S) -> c | a ->* b 25.006/25.006 Rule deleted 25.006/25.006 Proof: 25.006/25.006 YES 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 25.006/25.006 Infeasibility Problem: 25.006/25.006 [(VAR vNonEmpty:S vNonEmpty:S:S x:S:S) 25.006/25.006 (STRATEGY CONTEXTSENSITIVE 25.006/25.006 (f 1) 25.006/25.006 (g 1 2) 25.006/25.006 (a) 25.006/25.006 (b) 25.006/25.006 (c) 25.006/25.006 (fSNonEmpty) 25.006/25.006 ) 25.006/25.006 (RULES 25.006/25.006 f(x:S:S) -> c | a ->* b 25.006/25.006 g(x:S:S,x:S:S) -> g(f(a),f(b)) 25.006/25.006 )] 25.006/25.006 25.006/25.006 Infeasibility Conditions: 25.006/25.006 a ->* b 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 25.006/25.006 Obtaining a model using Mace4: 25.006/25.006 25.006/25.006 -> Usable Rules: 25.006/25.006 Empty 25.006/25.006 25.006/25.006 -> Mace4 Output: 25.006/25.006 ============================== Mace4 ================================= 25.006/25.006 Mace4 (64) version 2009-11A, November 2009. 25.006/25.006 Process 47568 was started by ubuntu on ubuntu, 25.006/25.006 Wed Jul 14 10:43:34 2021 25.006/25.006 The command was "./mace4 -c -f /tmp/mace447556-2.in". 25.006/25.006 ============================== end of head =========================== 25.006/25.006 25.006/25.006 ============================== INPUT ================================= 25.006/25.006 25.006/25.006 % Reading from file /tmp/mace447556-2.in 25.006/25.006 25.006/25.006 assign(max_seconds,20). 25.006/25.006 25.006/25.006 formulas(assumptions). 25.006/25.006 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence). 25.006/25.006 ->(x1,y) -> ->(g(x1,x2),g(y,x2)) # label(congruence). 25.006/25.006 ->(x2,y) -> ->(g(x1,x2),g(x1,y)) # label(congruence). 25.006/25.006 ->*(x,x) # label(reflexivity). 25.006/25.006 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 25.006/25.006 end_of_list. 25.006/25.006 25.006/25.006 formulas(goals). 25.006/25.006 ->*(a,b) # label(goal). 25.006/25.006 end_of_list. 25.006/25.006 25.006/25.006 ============================== end of input ========================== 25.006/25.006 25.006/25.006 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 25.006/25.006 25.006/25.006 % Formulas that are not ordinary clauses: 25.006/25.006 1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 25.006/25.006 2 ->(x1,y) -> ->(g(x1,x2),g(y,x2)) # label(congruence) # label(non_clause). [assumption]. 25.006/25.006 3 ->(x2,y) -> ->(g(x1,x2),g(x1,y)) # label(congruence) # label(non_clause). [assumption]. 25.006/25.006 4 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 25.006/25.006 5 ->*(a,b) # label(goal) # label(non_clause) # label(goal). [goal]. 25.006/25.006 25.006/25.006 ============================== end of process non-clausal formulas === 25.006/25.006 25.006/25.006 ============================== CLAUSES FOR SEARCH ==================== 25.006/25.006 25.006/25.006 formulas(mace4_clauses). 25.006/25.006 -->(x,y) | ->(f(x),f(y)) # label(congruence). 25.006/25.006 -->(x,y) | ->(g(x,z),g(y,z)) # label(congruence). 25.006/25.006 -->(x,y) | ->(g(z,x),g(z,y)) # label(congruence). 25.006/25.006 ->*(x,x) # label(reflexivity). 25.006/25.006 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 25.006/25.006 -->*(a,b) # label(goal). 25.006/25.006 end_of_list. 25.006/25.006 25.006/25.006 ============================== end of clauses for search ============= 25.006/25.006 25.006/25.006 % There are no natural numbers in the input. 25.006/25.006 25.006/25.006 ============================== DOMAIN SIZE 2 ========================= 25.006/25.006 25.006/25.006 ============================== MODEL ================================= 25.006/25.006 25.006/25.006 interpretation( 2, [number=1, seconds=0], [ 25.006/25.006 25.006/25.006 function(a, [ 0 ]), 25.006/25.006 25.006/25.006 function(b, [ 1 ]), 25.006/25.006 25.006/25.006 function(f(_), [ 0, 0 ]), 25.006/25.006 25.006/25.006 function(g(_,_), [ 25.006/25.006 0, 0, 25.006/25.006 0, 0 ]), 25.006/25.006 25.006/25.006 relation(->*(_,_), [ 25.006/25.006 1, 0, 25.006/25.006 0, 1 ]), 25.006/25.006 25.006/25.006 relation(->(_,_), [ 25.006/25.006 0, 0, 25.006/25.006 0, 0 ]) 25.006/25.006 ]). 25.006/25.006 25.006/25.006 ============================== end of model ========================== 25.006/25.006 25.006/25.006 ============================== STATISTICS ============================ 25.006/25.006 25.006/25.006 For domain size 2. 25.006/25.006 25.006/25.006 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 25.006/25.006 Ground clauses: seen=31, kept=27. 25.006/25.006 Selections=9, assignments=9, propagations=7, current_models=1. 25.006/25.006 Rewrite_terms=42, rewrite_bools=34, indexes=4. 25.006/25.006 Rules_from_neg_clauses=1, cross_offs=1. 25.006/25.006 25.006/25.006 ============================== end of statistics ===================== 25.006/25.006 25.006/25.006 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 25.006/25.006 25.006/25.006 Exiting with 1 model. 25.006/25.006 25.006/25.006 Process 47568 exit (max_models) Wed Jul 14 10:43:34 2021 25.006/25.006 The process finished Wed Jul 14 10:43:34 2021 25.006/25.006 25.006/25.006 25.006/25.006 Mace4 cooked interpretation: 25.006/25.006 25.006/25.006 25.006/25.006 25.006/25.006 The problem is infeasible. 25.006/25.006 25.006/25.006 25.006/25.006 CRule InfChecker Info: 25.006/25.006 g(x:S,x:S) -> g(f(a),f(b)) 25.006/25.006 Rule remains 25.006/25.006 Proof: 25.006/25.006 NO_CONDS 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.006/25.006 Confluence Problem: 25.006/25.006 (VAR x:S) 25.006/25.006 (STRATEGY CONTEXTSENSITIVE 25.006/25.006 (f 1) 25.006/25.006 (g 1 2) 25.006/25.006 (a) 25.006/25.006 (b) 25.006/25.006 (c) 25.006/25.006 (fSNonEmpty) 25.006/25.006 ) 25.006/25.006 (RULES 25.006/25.006 g(x:S,x:S) -> g(f(a),f(b)) 25.006/25.006 ) 25.006/25.006 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.006/25.006 25.006/25.006 Critical Pairs Processor: 25.006/25.006 -> Rules: 25.006/25.006 g(x:S,x:S) -> g(f(a),f(b)) 25.006/25.006 -> Vars: 25.006/25.006 "x" 25.006/25.006 -> FVars: 25.006/25.006 "x2" 25.006/25.006 -> PVars: 25.006/25.006 "x": ["x2"] 25.006/25.006 25.006/25.006 -> Rlps: 25.006/25.006 crule: g(x2:S,x2:S) -> g(f(a),f(b)), id: 1, possubterms: g(x2:S,x2:S)-> [] 25.006/25.006 25.006/25.006 -> Unifications: 25.006/25.006 25.006/25.006 25.006/25.006 -> Critical pairs info: 25.006/25.006 25.006/25.006 25.006/25.006 -> Problem conclusions: 25.006/25.006 Not left linear, Right linear, Not linear 25.006/25.006 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 25.006/25.006 CTRS Type: 1 25.006/25.006 Deterministic, Strongly deterministic 25.006/25.006 Oriented CTRS, Properly oriented CTRS, Join CTRS 25.006/25.006 Maybe right-stable CTRS, Overlay CTRS 25.006/25.006 Normal CTRS, Almost normal CTRS 25.006/25.006 Maybe terminating CTRS, Joinable CCPs 25.006/25.006 Maybe level confluent 25.006/25.006 Maybe confluent 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 Clean Infeasible CCPs Processor: 25.006/25.006 25.006/25.006 25.006/25.006 -> Problem conclusions: 25.006/25.006 Not left linear, Right linear, Not linear 25.006/25.006 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 25.006/25.006 CTRS Type: 1 25.006/25.006 Deterministic, Strongly deterministic 25.006/25.006 Oriented CTRS, Properly oriented CTRS, Join CTRS 25.006/25.006 Maybe right-stable CTRS, Overlay CTRS 25.006/25.006 Normal CTRS, Almost normal CTRS 25.006/25.006 Maybe terminating CTRS, Joinable CCPs 25.006/25.006 Maybe level confluent 25.006/25.006 Maybe confluent 25.006/25.006 25.006/25.006 Resulting CCPs: 25.006/25.006 No CCPs left 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 Underlying TRS Termination Processor: 25.006/25.006 25.006/25.006 Resulting Underlying TRS: 25.006/25.006 (VAR x:S) 25.006/25.006 (STRATEGY CONTEXTSENSITIVE 25.006/25.006 (g 1 2) 25.006/25.006 ) 25.006/25.006 (RULES 25.006/25.006 g(x:S,x:S) -> g(f(a),f(b)) 25.006/25.006 ) 25.006/25.006 Underlying TRS terminating? 25.006/25.006 YES 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 25.006/25.006 (VAR vu95NonEmpty:S xu58S:S) 25.006/25.006 (RULES 25.006/25.006 g(xu58S:S,xu58S:S) -> g(f(a),f(b)) 25.006/25.006 ) 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 25.006/25.006 Innermost Equivalent Processor: 25.006/25.006 -> Rules: 25.006/25.006 g(xu58S:S,xu58S:S) -> g(f(a),f(b)) 25.006/25.006 -> The term rewriting system is non-overlaping or locally confluent overlay system. Therefore, innermost termination implies termination. 25.006/25.006 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 25.006/25.006 Dependency Pairs Processor: 25.006/25.006 -> Pairs: 25.006/25.006 Empty 25.006/25.006 -> Rules: 25.006/25.006 g(xu58S:S,xu58S:S) -> g(f(a),f(b)) 25.006/25.006 25.006/25.006 Problem 1: 25.006/25.006 25.006/25.006 SCC Processor: 25.006/25.006 -> Pairs: 25.006/25.006 Empty 25.006/25.006 -> Rules: 25.006/25.006 g(xu58S:S,xu58S:S) -> g(f(a),f(b)) 25.006/25.006 ->Strongly Connected Components: 25.006/25.006 There is no strongly connected component 25.006/25.006 25.006/25.006 The problem is finite. 25.006/25.006 25.006/25.006 25.006/25.006 -> Problem conclusions: 25.006/25.006 Not left linear, Right linear, Not linear 25.006/25.006 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 25.006/25.006 CTRS Type: 1 25.006/25.006 Deterministic, Strongly deterministic 25.006/25.006 Oriented CTRS, Properly oriented CTRS, Join CTRS 25.006/25.006 Maybe right-stable CTRS, Overlay CTRS 25.006/25.006 Normal CTRS, Almost normal CTRS 25.006/25.006 Terminating CTRS, Joinable CCPs 25.006/25.006 Maybe level confluent 25.006/25.006 Confluent 25.006/25.006 25.006/25.006 The problem is joinable. 25.006/25.006 21.93user 0.16system 0:25.06elapsed 88%CPU (0avgtext+0avgdata 44784maxresident)k 25.006/25.006 0inputs+0outputs (0major+37023minor)pagefaults 0swaps