0.004/0.004 YES 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 0.004/0.004 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 Confluence Problem: 0.004/0.004 (VAR vNonEmpty:S x:S) 0.004/0.004 (STRATEGY CONTEXTSENSITIVE 0.004/0.004 (f 1 2) 0.004/0.004 (a) 0.004/0.004 (b) 0.004/0.004 (fSNonEmpty) 0.004/0.004 (g 1) 0.004/0.004 ) 0.004/0.004 (RULES 0.004/0.004 f(x:S,x:S) -> a | g(x:S) ->* b 0.004/0.004 ) 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 0.004/0.004 Inlining of Conditions Processor [STERN17]: 0.004/0.004 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 Confluence Problem: 0.004/0.004 (VAR vNonEmpty:S x:S) 0.004/0.004 (STRATEGY CONTEXTSENSITIVE 0.004/0.004 (f 1 2) 0.004/0.004 (a) 0.004/0.004 (b) 0.004/0.004 (fSNonEmpty) 0.004/0.004 (g 1) 0.004/0.004 ) 0.004/0.004 (RULES 0.004/0.004 f(x:S,x:S) -> a | g(x:S) ->* b 0.004/0.004 ) 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 Confluence Problem: 0.004/0.004 (VAR vNonEmpty:S x:S) 0.004/0.004 (STRATEGY CONTEXTSENSITIVE 0.004/0.004 (f 1 2) 0.004/0.004 (a) 0.004/0.004 (b) 0.004/0.004 (fSNonEmpty) 0.004/0.004 (g 1) 0.004/0.004 ) 0.004/0.004 (RULES 0.004/0.004 f(x:S,x:S) -> a | g(x:S) ->* b 0.004/0.004 ) 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 0.004/0.004 Critical Pairs Processor: 0.004/0.004 -> Rules: 0.004/0.004 f(x:S,x:S) -> a | g(x:S) ->* b 0.004/0.004 -> Vars: 0.004/0.004 "x" 0.004/0.004 -> FVars: 0.004/0.004 "x2" 0.004/0.004 -> PVars: 0.004/0.004 "x": ["x2"] 0.004/0.004 0.004/0.004 -> Rlps: 0.004/0.004 crule: f(x2:S,x2:S) -> a | g(x2:S) ->* b, id: 1, possubterms: f(x2:S,x2:S)-> [] 0.004/0.004 0.004/0.004 -> Unifications: 0.004/0.004 0.004/0.004 0.004/0.004 -> Critical pairs info: 0.004/0.004 0.004/0.004 0.004/0.004 -> Problem conclusions: 0.004/0.004 Not left linear, Right linear, Not linear 0.004/0.004 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.004/0.004 CTRS Type: 1 0.004/0.004 Deterministic, Strongly deterministic 0.004/0.004 Oriented CTRS, Properly oriented CTRS, Not join CTRS 0.004/0.004 Maybe right-stable CTRS, Overlay CTRS 0.004/0.004 Maybe normal CTRS, Maybe almost normal CTRS 0.004/0.004 Maybe terminating CTRS, Joinable CCPs 0.004/0.004 Maybe level confluent 0.004/0.004 Maybe confluent 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 Underlying TRS Termination Processor: 0.004/0.004 0.004/0.004 Resulting Underlying TRS: 0.004/0.004 (VAR vNonEmpty:S x:S) 0.004/0.004 (STRATEGY CONTEXTSENSITIVE 0.004/0.004 (f 1 2) 0.004/0.004 (a) 0.004/0.004 ) 0.004/0.004 (RULES 0.004/0.004 f(x:S,x:S) -> a 0.004/0.004 ) 0.004/0.004 Underlying TRS terminating? 0.004/0.004 YES 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 0.004/0.004 (VAR vu95NonEmpty:S vNonEmptyu58S:S xu58S:S) 0.004/0.004 (RULES 0.004/0.004 f(xu58S:S,xu58S:S) -> a 0.004/0.004 ) 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 0.004/0.004 Innermost Equivalent Processor: 0.004/0.004 -> Rules: 0.004/0.004 f(xu58S:S,xu58S:S) -> a 0.004/0.004 -> The term rewriting system is non-overlaping or locally confluent overlay system. Therefore, innermost termination implies termination. 0.004/0.004 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 0.004/0.004 Dependency Pairs Processor: 0.004/0.004 -> Pairs: 0.004/0.004 Empty 0.004/0.004 -> Rules: 0.004/0.004 f(xu58S:S,xu58S:S) -> a 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 0.004/0.004 SCC Processor: 0.004/0.004 -> Pairs: 0.004/0.004 Empty 0.004/0.004 -> Rules: 0.004/0.004 f(xu58S:S,xu58S:S) -> a 0.004/0.004 ->Strongly Connected Components: 0.004/0.004 There is no strongly connected component 0.004/0.004 0.004/0.004 The problem is finite. 0.004/0.004 0.004/0.004 0.004/0.004 -> Problem conclusions: 0.004/0.004 Not left linear, Right linear, Not linear 0.004/0.004 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.004/0.004 CTRS Type: 1 0.004/0.004 Deterministic, Strongly deterministic 0.004/0.004 Oriented CTRS, Properly oriented CTRS, Not join CTRS 0.004/0.004 Maybe right-stable CTRS, Overlay CTRS 0.004/0.004 Maybe normal CTRS, Maybe almost normal CTRS 0.004/0.004 Terminating CTRS, Joinable CCPs 0.004/0.004 Maybe level confluent 0.004/0.004 Maybe confluent 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 Confluence Problem: 0.004/0.004 (VAR vNonEmpty:S x:S) 0.004/0.004 (STRATEGY CONTEXTSENSITIVE 0.004/0.004 (f 1 2) 0.004/0.004 (a) 0.004/0.004 (b) 0.004/0.004 (fSNonEmpty) 0.004/0.004 (g 1) 0.004/0.004 ) 0.004/0.004 (RULES 0.004/0.004 f(x:S,x:S) -> a | g(x:S) ->* b 0.004/0.004 ) 0.004/0.004 Critical Pairs: 0.004/0.004 0.004/0.004 Terminating:YES 0.004/0.004 0.004/0.004 -> Problem conclusions: 0.004/0.004 Not left linear, Right linear, Not linear 0.004/0.004 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.004/0.004 CTRS Type: 1 0.004/0.004 Deterministic, Strongly deterministic 0.004/0.004 Oriented CTRS, Properly oriented CTRS, Not join CTRS 0.004/0.004 Maybe right-stable CTRS, Overlay CTRS 0.004/0.004 Maybe normal CTRS, Maybe almost normal CTRS 0.004/0.004 Terminating CTRS, Joinable CCPs 0.004/0.004 Maybe level confluent 0.004/0.004 Maybe confluent 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 0.004/0.004 Right Stable Processor: 0.004/0.004 Right-stable CTRS 0.004/0.004 Justification: 0.004/0.004 0.004/0.004 -> Term right-stability conditions: 0.004/0.004 Term: b 0.004/0.004 Right-stable term 0.004/0.004 Linear constructor form 0.004/0.004 Don't know if term is a ground normal form (not needed) 0.004/0.004 Right-stability condition achieved 0.004/0.004 A call to InfChecker wasn't needed 0.004/0.004 0.004/0.004 -> Problem conclusions: 0.004/0.004 Not left linear, Right linear, Not linear 0.004/0.004 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.004/0.004 CTRS Type: 1 0.004/0.004 Deterministic, Strongly deterministic 0.004/0.004 Oriented CTRS, Properly oriented CTRS, Not join CTRS 0.004/0.004 Right-stable CTRS, Overlay CTRS 0.004/0.004 Maybe normal CTRS, Almost normal CTRS 0.004/0.004 Terminating CTRS, Joinable CCPs 0.004/0.004 Maybe level confluent 0.004/0.004 Maybe confluent 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 Confluence Problem: 0.004/0.004 (VAR vNonEmpty:S x:S) 0.004/0.004 (STRATEGY CONTEXTSENSITIVE 0.004/0.004 (f 1 2) 0.004/0.004 (a) 0.004/0.004 (b) 0.004/0.004 (fSNonEmpty) 0.004/0.004 (g 1) 0.004/0.004 ) 0.004/0.004 (RULES 0.004/0.004 f(x:S,x:S) -> a | g(x:S) ->* b 0.004/0.004 ) 0.004/0.004 Critical Pairs: 0.004/0.004 0.004/0.004 Terminating:YES 0.004/0.004 0.004/0.004 -> Problem conclusions: 0.004/0.004 Not left linear, Right linear, Not linear 0.004/0.004 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.004/0.004 CTRS Type: 1 0.004/0.004 Deterministic, Strongly deterministic 0.004/0.004 Oriented CTRS, Properly oriented CTRS, Not join CTRS 0.004/0.004 Right-stable CTRS, Overlay CTRS 0.004/0.004 Maybe normal CTRS, Almost normal CTRS 0.004/0.004 Terminating CTRS, Joinable CCPs 0.004/0.004 Maybe level confluent 0.004/0.004 Maybe confluent 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 0.004/0.004 Normal RConds Processor: 0.004/0.004 YES 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 0.004/0.004 Infeasibility Problem: 0.004/0.004 [(VAR vNonEmpty:S x:S x1:S) 0.004/0.004 (STRATEGY CONTEXTSENSITIVE 0.004/0.004 (f 1 2) 0.004/0.004 (a) 0.004/0.004 (b) 0.004/0.004 (fSNonEmpty) 0.004/0.004 (g 1) 0.004/0.004 ) 0.004/0.004 (RULES 0.004/0.004 f(x:S,x:S) -> a | g(x:S) ->* b 0.004/0.004 )] 0.004/0.004 0.004/0.004 Infeasibility Conditions: 0.004/0.004 b -> x1:S 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 0.004/0.004 Obtaining a model using Mace4: 0.004/0.004 0.004/0.004 -> Usable Rules: 0.004/0.004 Empty 0.004/0.004 0.004/0.004 -> Mace4 Output: 0.004/0.004 ============================== Mace4 ================================= 0.004/0.004 Mace4 (64) version 2009-11A, November 2009. 0.004/0.004 Process 34411 was started by ubuntu on ubuntu, 0.004/0.004 Wed Jul 14 09:52:58 2021 0.004/0.004 The command was "./mace4 -c -f /tmp/mace434398-2.in". 0.004/0.004 ============================== end of head =========================== 0.004/0.004 0.004/0.004 ============================== INPUT ================================= 0.004/0.004 0.004/0.004 % Reading from file /tmp/mace434398-2.in 0.004/0.004 0.004/0.004 assign(max_seconds,1). 0.004/0.004 0.004/0.004 formulas(assumptions). 0.004/0.004 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence). 0.004/0.004 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence). 0.004/0.004 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence). 0.004/0.004 end_of_list. 0.004/0.004 0.004/0.004 formulas(goals). 0.004/0.004 (exists x2 ->(b,x2)) # label(goal). 0.004/0.004 end_of_list. 0.004/0.004 0.004/0.004 ============================== end of input ========================== 0.004/0.004 0.004/0.004 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 0.004/0.004 0.004/0.004 % Formulas that are not ordinary clauses: 0.004/0.004 1 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 0.004/0.004 2 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 0.004/0.004 3 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 0.004/0.004 4 (exists x2 ->(b,x2)) # label(goal) # label(non_clause) # label(goal). [goal]. 0.004/0.004 0.004/0.004 ============================== end of process non-clausal formulas === 0.004/0.004 0.004/0.004 ============================== CLAUSES FOR SEARCH ==================== 0.004/0.004 0.004/0.004 formulas(mace4_clauses). 0.004/0.004 -->(x,y) | ->(f(x,z),f(y,z)) # label(congruence). 0.004/0.004 -->(x,y) | ->(f(z,x),f(z,y)) # label(congruence). 0.004/0.004 -->(x,y) | ->(g(x),g(y)) # label(congruence). 0.004/0.004 -->(b,x) # label(goal). 0.004/0.004 end_of_list. 0.004/0.004 0.004/0.004 ============================== end of clauses for search ============= 0.004/0.004 0.004/0.004 % There are no natural numbers in the input. 0.004/0.004 0.004/0.004 ============================== DOMAIN SIZE 2 ========================= 0.004/0.004 0.004/0.004 ============================== MODEL ================================= 0.004/0.004 0.004/0.004 interpretation( 2, [number=1, seconds=0], [ 0.004/0.004 0.004/0.004 function(b, [ 0 ]), 0.004/0.004 0.004/0.004 function(g(_), [ 0, 0 ]), 0.004/0.004 0.004/0.004 function(f(_,_), [ 0.004/0.004 0, 0, 0.004/0.004 0, 0 ]), 0.004/0.004 0.004/0.004 relation(->(_,_), [ 0.004/0.004 0, 0, 0.004/0.004 0, 0 ]) 0.004/0.004 ]). 0.004/0.004 0.004/0.004 ============================== end of model ========================== 0.004/0.004 0.004/0.004 ============================== STATISTICS ============================ 0.004/0.004 0.004/0.004 For domain size 2. 0.004/0.004 0.004/0.004 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 0.004/0.004 Ground clauses: seen=22, kept=22. 0.004/0.004 Selections=7, assignments=7, propagations=4, current_models=1. 0.004/0.004 Rewrite_terms=42, rewrite_bools=24, indexes=2. 0.004/0.004 Rules_from_neg_clauses=0, cross_offs=0. 0.004/0.004 0.004/0.004 ============================== end of statistics ===================== 0.004/0.004 0.004/0.004 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 0.004/0.004 0.004/0.004 Exiting with 1 model. 0.004/0.004 0.004/0.004 Process 34411 exit (max_models) Wed Jul 14 09:52:58 2021 0.004/0.004 The process finished Wed Jul 14 09:52:58 2021 0.004/0.004 0.004/0.004 0.004/0.004 Mace4 cooked interpretation: 0.004/0.004 0.004/0.004 0.004/0.004 0.004/0.004 The problem is infeasible. 0.004/0.004 0.004/0.004 0.004/0.004 -> Problem conclusions: 0.004/0.004 Not left linear, Right linear, Not linear 0.004/0.004 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.004/0.004 CTRS Type: 1 0.004/0.004 Deterministic, Strongly deterministic 0.004/0.004 Oriented CTRS, Properly oriented CTRS, Not join CTRS 0.004/0.004 Right-stable CTRS, Overlay CTRS 0.004/0.004 Normal CTRS, Almost normal CTRS 0.004/0.004 Terminating CTRS, Joinable CCPs 0.004/0.004 Maybe level confluent 0.004/0.004 Confluent 0.004/0.004 0.004/0.004 The problem is joinable. 0.004/0.004 0.02user 0.01system 0:00.04elapsed 85%CPU (0avgtext+0avgdata 9240maxresident)k 0.004/0.004 0inputs+0outputs (0major+3268minor)pagefaults 0swaps