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