25.072/25.072 NO 25.072/25.072 25.072/25.072 Problem 1: 25.072/25.072 25.072/25.072 25.072/25.072 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.072/25.072 Confluence Problem: 25.072/25.072 (VAR vNonEmpty:S x:S z:S) 25.072/25.072 (STRATEGY CONTEXTSENSITIVE 25.072/25.072 (c) 25.072/25.072 (f 1) 25.072/25.072 (g 1 2) 25.072/25.072 (s 1) 25.072/25.072 (a) 25.072/25.072 (b) 25.072/25.072 (fSNonEmpty) 25.072/25.072 (h 1 2) 25.072/25.072 (k) 25.072/25.072 (l) 25.072/25.072 (t 1) 25.072/25.072 ) 25.072/25.072 (RULES 25.072/25.072 c -> t(k) 25.072/25.072 c -> t(l) 25.072/25.072 f(x:S) -> z:S | s(x:S) ->* z:S 25.072/25.072 g(x:S,x:S) -> h(x:S,x:S) 25.072/25.072 s(a) -> c 25.072/25.072 s(b) -> c 25.072/25.072 ) 25.072/25.072 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.072/25.072 25.072/25.072 25.072/25.072 Problem 1: 25.072/25.072 25.072/25.072 Inlining of Conditions Processor [STERN17]: 25.072/25.072 25.072/25.072 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.072/25.072 Confluence Problem: 25.072/25.072 (VAR vNonEmpty:S x:S z:S) 25.072/25.072 (STRATEGY CONTEXTSENSITIVE 25.072/25.072 (c) 25.072/25.072 (f 1) 25.072/25.072 (g 1 2) 25.072/25.072 (s 1) 25.072/25.072 (a) 25.072/25.072 (b) 25.072/25.072 (fSNonEmpty) 25.072/25.072 (h 1 2) 25.072/25.072 (k) 25.072/25.072 (l) 25.072/25.072 (t 1) 25.072/25.072 ) 25.072/25.072 (RULES 25.072/25.072 c -> t(k) 25.072/25.072 c -> t(l) 25.072/25.072 f(x:S) -> s(x:S) 25.072/25.072 g(x:S,x:S) -> h(x:S,x:S) 25.072/25.072 s(a) -> c 25.072/25.072 s(b) -> c 25.072/25.072 ) 25.072/25.072 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.072/25.072 25.072/25.072 25.072/25.072 Problem 1: 25.072/25.072 25.072/25.072 Clean CTRS Processor: 25.072/25.072 25.072/25.072 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.072/25.072 Confluence Problem: 25.072/25.072 (VAR x:S) 25.072/25.072 (STRATEGY CONTEXTSENSITIVE 25.072/25.072 (c) 25.072/25.072 (f 1) 25.072/25.072 (g 1 2) 25.072/25.072 (s 1) 25.072/25.072 (a) 25.072/25.072 (b) 25.072/25.072 (fSNonEmpty) 25.072/25.072 (h 1 2) 25.072/25.072 (k) 25.072/25.072 (l) 25.072/25.072 (t 1) 25.072/25.072 ) 25.072/25.072 (RULES 25.072/25.072 c -> t(k) 25.072/25.072 c -> t(l) 25.072/25.072 f(x:S) -> s(x:S) 25.072/25.072 g(x:S,x:S) -> h(x:S,x:S) 25.072/25.072 s(a) -> c 25.072/25.072 s(b) -> c 25.072/25.072 ) 25.072/25.072 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.072/25.072 25.072/25.072 CRule InfChecker Info: 25.072/25.072 c -> t(k) 25.072/25.072 Rule remains 25.072/25.072 Proof: 25.072/25.072 NO_CONDS 25.072/25.072 25.072/25.072 CRule InfChecker Info: 25.072/25.072 c -> t(l) 25.072/25.072 Rule remains 25.072/25.072 Proof: 25.072/25.072 NO_CONDS 25.072/25.072 25.072/25.072 CRule InfChecker Info: 25.072/25.072 f(x:S) -> s(x:S) 25.072/25.072 Rule remains 25.072/25.072 Proof: 25.072/25.072 NO_CONDS 25.072/25.072 25.072/25.072 CRule InfChecker Info: 25.072/25.072 g(x:S,x:S) -> h(x:S,x:S) 25.072/25.072 Rule remains 25.072/25.072 Proof: 25.072/25.072 NO_CONDS 25.072/25.072 25.072/25.072 CRule InfChecker Info: 25.072/25.072 s(a) -> c 25.072/25.072 Rule remains 25.072/25.072 Proof: 25.072/25.072 NO_CONDS 25.072/25.072 25.072/25.072 CRule InfChecker Info: 25.072/25.072 s(b) -> c 25.072/25.072 Rule remains 25.072/25.072 Proof: 25.072/25.072 NO_CONDS 25.072/25.072 25.072/25.072 Problem 1: 25.072/25.072 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.072/25.072 Confluence Problem: 25.072/25.072 (VAR x:S) 25.072/25.072 (STRATEGY CONTEXTSENSITIVE 25.072/25.072 (c) 25.072/25.072 (f 1) 25.072/25.072 (g 1 2) 25.072/25.072 (s 1) 25.072/25.072 (a) 25.072/25.072 (b) 25.072/25.072 (fSNonEmpty) 25.072/25.072 (h 1 2) 25.072/25.072 (k) 25.072/25.072 (l) 25.072/25.072 (t 1) 25.072/25.072 ) 25.072/25.072 (RULES 25.072/25.072 c -> t(k) 25.072/25.072 c -> t(l) 25.072/25.072 f(x:S) -> s(x:S) 25.072/25.072 g(x:S,x:S) -> h(x:S,x:S) 25.072/25.072 s(a) -> c 25.072/25.072 s(b) -> c 25.072/25.072 ) 25.072/25.072 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.072/25.072 25.072/25.072 Critical Pairs Processor: 25.072/25.072 -> Rules: 25.072/25.072 c -> t(k) 25.072/25.072 c -> t(l) 25.072/25.072 f(x:S) -> s(x:S) 25.072/25.072 g(x:S,x:S) -> h(x:S,x:S) 25.072/25.072 s(a) -> c 25.072/25.072 s(b) -> c 25.072/25.072 -> Vars: 25.072/25.072 "x", "x" 25.072/25.072 -> FVars: 25.072/25.072 "x2", "x3" 25.072/25.072 -> PVars: 25.072/25.072 "x": ["x2", "x3"] 25.072/25.072 25.072/25.072 -> Rlps: 25.072/25.072 crule: c -> t(k), id: 1, possubterms: c-> [] 25.072/25.072 crule: c -> t(l), id: 2, possubterms: c-> [] 25.072/25.072 crule: f(x2:S) -> s(x2:S), id: 3, possubterms: f(x2:S)-> [] 25.072/25.072 crule: g(x3:S,x3:S) -> h(x3:S,x3:S), id: 4, possubterms: g(x3:S,x3:S)-> [] 25.072/25.072 crule: s(a) -> c, id: 5, possubterms: s(a)-> [], a-> [1] 25.072/25.072 crule: s(b) -> c, id: 6, possubterms: s(b)-> [], b-> [1] 25.072/25.072 25.072/25.072 -> Unifications: 25.072/25.072 R2 unifies with R1 at p: [], l: c, lp: c, conds: {}, sig: {}, l': c, r: t(l), r': t(k) 25.072/25.072 25.072/25.072 -> Critical pairs info: 25.072/25.072 => Not trivial, Overlay, N1 25.072/25.072 25.072/25.072 -> Problem conclusions: 25.072/25.072 Not left linear, Not right linear, Not linear 25.072/25.072 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 25.072/25.072 CTRS Type: 1 25.072/25.072 Deterministic, Strongly deterministic 25.072/25.072 Oriented CTRS, Properly oriented CTRS, Join CTRS 25.072/25.072 Maybe right-stable CTRS, Overlay CTRS 25.072/25.072 Normal CTRS, Almost normal CTRS 25.072/25.072 Maybe terminating CTRS, Maybe joinable CCPs 25.072/25.072 Maybe level confluent 25.072/25.072 Maybe confluent 25.072/25.072 25.072/25.072 Problem 1: 25.072/25.072 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.072/25.072 Confluence Problem: 25.072/25.072 (VAR x:S) 25.072/25.072 (STRATEGY CONTEXTSENSITIVE 25.072/25.072 (c) 25.072/25.072 (f 1) 25.072/25.072 (g 1 2) 25.072/25.072 (s 1) 25.072/25.072 (a) 25.072/25.072 (b) 25.072/25.072 (fSNonEmpty) 25.072/25.072 (h 1 2) 25.072/25.072 (k) 25.072/25.072 (l) 25.072/25.072 (t 1) 25.072/25.072 ) 25.072/25.072 (RULES 25.072/25.072 c -> t(k) 25.072/25.072 c -> t(l) 25.072/25.072 f(x:S) -> s(x:S) 25.072/25.072 g(x:S,x:S) -> h(x:S,x:S) 25.072/25.072 s(a) -> c 25.072/25.072 s(b) -> c 25.072/25.072 ) 25.072/25.072 Critical Pairs: 25.072/25.072 => Not trivial, Overlay, N1 25.072/25.072 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.072/25.072 25.072/25.072 Conditional Critical Pairs Distributor Processor 25.072/25.072 25.072/25.072 Problem 1: 25.072/25.072 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.072/25.072 Confluence Problem: 25.072/25.072 (VAR x:S) 25.072/25.072 (STRATEGY CONTEXTSENSITIVE 25.072/25.072 (c) 25.072/25.072 (f 1) 25.072/25.072 (g 1 2) 25.072/25.072 (s 1) 25.072/25.072 (a) 25.072/25.072 (b) 25.072/25.072 (fSNonEmpty) 25.072/25.072 (h 1 2) 25.072/25.072 (k) 25.072/25.072 (l) 25.072/25.072 (t 1) 25.072/25.072 ) 25.072/25.072 (RULES 25.072/25.072 c -> t(k) 25.072/25.072 c -> t(l) 25.072/25.072 f(x:S) -> s(x:S) 25.072/25.072 g(x:S,x:S) -> h(x:S,x:S) 25.072/25.072 s(a) -> c 25.072/25.072 s(b) -> c 25.072/25.072 ) 25.072/25.072 Critical Pairs: 25.072/25.072 => Not trivial, Overlay, N1 25.072/25.072 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.072/25.072 25.072/25.072 Infeasible Convergence No Conditions CCP Processor: 25.072/25.072 Infeasible convergence? 25.072/25.072 YES 25.072/25.072 25.072/25.072 Problem 1: 25.072/25.072 25.072/25.072 Infeasibility Problem: 25.072/25.072 [(VAR vNonEmpty:S x:S z:S) 25.072/25.072 (STRATEGY CONTEXTSENSITIVE 25.072/25.072 (c) 25.072/25.072 (f 1) 25.072/25.072 (g 1 2) 25.072/25.072 (s 1) 25.072/25.072 (a) 25.072/25.072 (b) 25.072/25.072 (fSNonEmpty) 25.072/25.072 (h 1 2) 25.072/25.072 (k) 25.072/25.072 (l) 25.072/25.072 (t 1) 25.072/25.072 ) 25.072/25.072 (RULES 25.072/25.072 c -> t(k) 25.072/25.072 c -> t(l) 25.072/25.072 f(x:S) -> s(x:S) 25.072/25.072 g(x:S,x:S) -> h(x:S,x:S) 25.072/25.072 s(a) -> c 25.072/25.072 s(b) -> c 25.072/25.072 )] 25.072/25.072 Infeasibility Conditions: 25.072/25.072 t(k) ->* z:S, t(l) ->* z:S 25.072/25.072 25.072/25.072 Problem 1: 25.072/25.072 25.072/25.072 Obtaining a model using Mace4: 25.072/25.072 25.072/25.072 -> Usable Rules: 25.072/25.072 Empty 25.072/25.072 25.072/25.072 -> Mace4 Output: 25.072/25.072 ============================== Mace4 ================================= 25.072/25.072 Mace4 (64) version 2009-11A, November 2009. 25.072/25.072 Process 50388 was started by ubuntu on ubuntu, 25.072/25.072 Wed Jul 14 10:54:59 2021 25.072/25.072 The command was "./mace4 -c -f /tmp/mace450365-2.in". 25.072/25.072 ============================== end of head =========================== 25.072/25.072 25.072/25.072 ============================== INPUT ================================= 25.072/25.072 25.072/25.072 % Reading from file /tmp/mace450365-2.in 25.072/25.072 25.072/25.072 assign(max_seconds,20). 25.072/25.072 25.072/25.072 formulas(assumptions). 25.072/25.072 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence). 25.072/25.072 ->(x1,y) -> ->(g(x1,x2),g(y,x2)) # label(congruence). 25.072/25.072 ->(x2,y) -> ->(g(x1,x2),g(x1,y)) # label(congruence). 25.072/25.072 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 25.072/25.072 ->(x1,y) -> ->(h(x1,x2),h(y,x2)) # label(congruence). 25.072/25.072 ->(x2,y) -> ->(h(x1,x2),h(x1,y)) # label(congruence). 25.072/25.072 ->(x1,y) -> ->(t(x1),t(y)) # label(congruence). 25.072/25.072 ->*(x,x) # label(reflexivity). 25.072/25.072 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 25.072/25.072 end_of_list. 25.072/25.072 25.072/25.072 formulas(goals). 25.072/25.072 (exists x2 (->*(t(k),x2) & ->*(t(l),x2))) # label(goal). 25.072/25.072 end_of_list. 25.072/25.072 25.072/25.072 ============================== end of input ========================== 25.072/25.072 25.072/25.072 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 25.072/25.072 25.072/25.072 % Formulas that are not ordinary clauses: 25.072/25.072 1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 25.072/25.072 2 ->(x1,y) -> ->(g(x1,x2),g(y,x2)) # label(congruence) # label(non_clause). [assumption]. 25.072/25.072 3 ->(x2,y) -> ->(g(x1,x2),g(x1,y)) # label(congruence) # label(non_clause). [assumption]. 25.072/25.072 4 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 25.072/25.072 5 ->(x1,y) -> ->(h(x1,x2),h(y,x2)) # label(congruence) # label(non_clause). [assumption]. 25.072/25.072 6 ->(x2,y) -> ->(h(x1,x2),h(x1,y)) # label(congruence) # label(non_clause). [assumption]. 25.072/25.072 7 ->(x1,y) -> ->(t(x1),t(y)) # label(congruence) # label(non_clause). [assumption]. 25.072/25.072 8 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 25.072/25.072 9 (exists x2 (->*(t(k),x2) & ->*(t(l),x2))) # label(goal) # label(non_clause) # label(goal). [goal]. 25.072/25.072 25.072/25.072 ============================== end of process non-clausal formulas === 25.072/25.072 25.072/25.072 ============================== CLAUSES FOR SEARCH ==================== 25.072/25.072 25.072/25.072 formulas(mace4_clauses). 25.072/25.072 -->(x,y) | ->(f(x),f(y)) # label(congruence). 25.072/25.072 -->(x,y) | ->(g(x,z),g(y,z)) # label(congruence). 25.072/25.072 -->(x,y) | ->(g(z,x),g(z,y)) # label(congruence). 25.072/25.072 -->(x,y) | ->(s(x),s(y)) # label(congruence). 25.072/25.072 -->(x,y) | ->(h(x,z),h(y,z)) # label(congruence). 25.072/25.072 -->(x,y) | ->(h(z,x),h(z,y)) # label(congruence). 25.072/25.072 -->(x,y) | ->(t(x),t(y)) # label(congruence). 25.072/25.072 ->*(x,x) # label(reflexivity). 25.072/25.072 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 25.072/25.072 -->*(t(k),x) | -->*(t(l),x) # label(goal). 25.072/25.072 end_of_list. 25.072/25.072 25.072/25.072 ============================== end of clauses for search ============= 25.072/25.072 25.072/25.072 % There are no natural numbers in the input. 25.072/25.072 25.072/25.072 ============================== DOMAIN SIZE 2 ========================= 25.072/25.072 25.072/25.072 ============================== MODEL ================================= 25.072/25.072 25.072/25.072 interpretation( 2, [number=1, seconds=0], [ 25.072/25.072 25.072/25.072 function(k, [ 0 ]), 25.072/25.072 25.072/25.072 function(l, [ 1 ]), 25.072/25.072 25.072/25.072 function(t(_), [ 0, 1 ]), 25.072/25.072 25.072/25.072 function(f(_), [ 0, 0 ]), 25.072/25.072 25.072/25.072 function(s(_), [ 0, 0 ]), 25.072/25.072 25.072/25.072 function(g(_,_), [ 25.072/25.072 0, 0, 25.072/25.072 0, 0 ]), 25.072/25.072 25.072/25.072 function(h(_,_), [ 25.072/25.072 0, 0, 25.072/25.072 0, 0 ]), 25.072/25.072 25.072/25.072 relation(->*(_,_), [ 25.072/25.072 1, 0, 25.072/25.072 0, 1 ]), 25.072/25.072 25.072/25.072 relation(->(_,_), [ 25.072/25.072 0, 0, 25.072/25.072 0, 0 ]) 25.072/25.072 ]). 25.072/25.072 25.072/25.072 ============================== end of model ========================== 25.072/25.072 25.072/25.072 ============================== STATISTICS ============================ 25.072/25.072 25.072/25.072 For domain size 2. 25.072/25.072 25.072/25.072 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 25.072/25.072 Ground clauses: seen=56, kept=52. 25.072/25.072 Selections=17, assignments=19, propagations=8, current_models=1. 25.072/25.072 Rewrite_terms=105, rewrite_bools=73, indexes=21. 25.072/25.072 Rules_from_neg_clauses=1, cross_offs=1. 25.072/25.072 25.072/25.072 ============================== end of statistics ===================== 25.072/25.072 25.072/25.072 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 25.072/25.072 25.072/25.072 Exiting with 1 model. 25.072/25.072 25.072/25.072 Process 50388 exit (max_models) Wed Jul 14 10:54:59 2021 25.072/25.072 The process finished Wed Jul 14 10:54:59 2021 25.072/25.072 25.072/25.072 25.072/25.072 Mace4 cooked interpretation: 25.072/25.072 25.072/25.072 25.072/25.072 25.072/25.072 The problem is infeasible. 25.072/25.072 25.072/25.072 25.072/25.072 The problem is not joinable. 25.072/25.072 48.45user 2.72system 0:25.72elapsed 198%CPU (0avgtext+0avgdata 1000144maxresident)k 25.072/25.072 0inputs+0outputs (0major+512149minor)pagefaults 0swaps