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