21.07/21.07 NO 21.07/21.07 21.07/21.07 Problem 1: 21.07/21.07 21.07/21.07 21.07/21.07 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 21.07/21.07 Confluence Problem: 21.07/21.07 (VAR vNonEmpty x) 21.07/21.07 (REPLACEMENT-MAP 21.07/21.07 (a) 21.07/21.07 (c) 21.07/21.07 (f 1) 21.07/21.07 (h 1) 21.07/21.07 (j 1) 21.07/21.07 (b) 21.07/21.07 (d) 21.07/21.07 (fSNonEmpty) 21.07/21.07 (g 1) 21.07/21.07 ) 21.07/21.07 (RULES 21.07/21.07 a -> b 21.07/21.07 c -> j(f(a)) 21.07/21.07 c -> d 21.07/21.07 f(x) -> g(x) | d ->*<- h(f(x)) 21.07/21.07 h(f(a)) -> c 21.07/21.07 h(x) -> j(x) 21.07/21.07 j(g(b)) -> d 21.07/21.07 ) 21.07/21.07 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 21.07/21.07 21.07/21.07 21.07/21.07 Problem 1: 21.07/21.07 21.07/21.07 Inlining of Conditions Processor [STERN17]: 21.07/21.07 21.07/21.07 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 21.07/21.07 Confluence Problem: 21.07/21.07 (VAR vNonEmpty x) 21.07/21.07 (REPLACEMENT-MAP 21.07/21.07 (a) 21.07/21.07 (c) 21.07/21.07 (f 1) 21.07/21.07 (h 1) 21.07/21.07 (j 1) 21.07/21.07 (b) 21.07/21.07 (d) 21.07/21.07 (fSNonEmpty) 21.07/21.07 (g 1) 21.07/21.07 ) 21.07/21.07 (RULES 21.07/21.07 a -> b 21.07/21.07 c -> j(f(a)) 21.07/21.07 c -> d 21.07/21.07 f(x) -> g(x) | d ->*<- h(f(x)) 21.07/21.07 h(f(a)) -> c 21.07/21.07 h(x) -> j(x) 21.07/21.07 j(g(b)) -> d 21.07/21.07 ) 21.07/21.07 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 21.07/21.07 21.07/21.07 21.07/21.07 Problem 1: 21.07/21.07 21.07/21.07 Clean CTRS Processor: 21.07/21.07 21.07/21.07 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 21.07/21.07 Confluence Problem: 21.07/21.07 (VAR x) 21.07/21.07 (REPLACEMENT-MAP 21.07/21.07 (a) 21.07/21.07 (c) 21.07/21.07 (f 1) 21.07/21.07 (h 1) 21.07/21.07 (j 1) 21.07/21.07 (b) 21.07/21.07 (d) 21.07/21.07 (fSNonEmpty) 21.07/21.07 (g 1) 21.07/21.07 ) 21.07/21.07 (RULES 21.07/21.07 a -> b 21.07/21.07 c -> j(f(a)) 21.07/21.07 c -> d 21.07/21.07 h(f(a)) -> c 21.07/21.07 h(x) -> j(x) 21.07/21.07 j(g(b)) -> d 21.07/21.07 ) 21.07/21.07 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 21.07/21.07 21.07/21.07 CRule InfChecker Info: 21.07/21.07 a -> b 21.07/21.07 Rule remains 21.07/21.07 Proof: 21.07/21.07 NO_CONDS 21.07/21.07 21.07/21.07 CRule InfChecker Info: 21.07/21.07 c -> j(f(a)) 21.07/21.07 Rule remains 21.07/21.07 Proof: 21.07/21.07 NO_CONDS 21.07/21.07 21.07/21.07 CRule InfChecker Info: 21.07/21.07 c -> d 21.07/21.07 Rule remains 21.07/21.07 Proof: 21.07/21.07 NO_CONDS 21.07/21.07 21.07/21.07 CRule InfChecker Info: 21.07/21.07 f(x) -> g(x) | d ->*<- h(f(x)) 21.07/21.07 Rule deleted 21.07/21.07 Proof: 21.07/21.07 YES 21.07/21.07 21.07/21.07 Problem 1: 21.07/21.07 21.07/21.07 Infeasibility Problem: 21.07/21.07 [(VAR vNonEmpty x vNonEmpty x) 21.07/21.07 (STRATEGY CONTEXTSENSITIVE 21.07/21.07 (a) 21.07/21.07 (c) 21.07/21.07 (f 1) 21.07/21.07 (h 1) 21.07/21.07 (j 1) 21.07/21.07 (b) 21.07/21.07 (d) 21.07/21.07 (fSNonEmpty) 21.07/21.07 (g 1) 21.07/21.07 ) 21.07/21.07 (RULES 21.07/21.07 a -> b 21.07/21.07 c -> j(f(a)) 21.07/21.07 c -> d 21.07/21.07 f(x) -> g(x) | d ->*<- h(f(x)) 21.07/21.07 h(f(a)) -> c 21.07/21.07 h(x) -> j(x) 21.07/21.07 j(g(b)) -> d 21.07/21.07 )] 21.07/21.07 21.07/21.07 Infeasibility Conditions: 21.07/21.07 d ->*<- h(f(x)) 21.07/21.07 21.07/21.07 Problem 1: 21.07/21.07 21.07/21.07 Obtaining a model using Mace4: 21.07/21.07 21.07/21.07 -> Usable Rules: 21.07/21.07 Empty 21.07/21.07 21.07/21.07 -> Mace4 Output: 21.07/21.07 ============================== Mace4 ================================= 21.07/21.07 Mace4 (64) version 2009-11A, November 2009. 21.07/21.07 Process 86444 was started by ubuntu on ubuntu, 21.07/21.07 Wed Mar 9 10:49:28 2022 21.07/21.07 The command was "./mace4 -c -f /tmp/mace486433-2.in". 21.07/21.07 ============================== end of head =========================== 21.07/21.07 21.07/21.07 ============================== INPUT ================================= 21.07/21.07 21.07/21.07 % Reading from file /tmp/mace486433-2.in 21.07/21.07 21.07/21.07 assign(max_seconds,20). 21.07/21.07 21.07/21.07 formulas(assumptions). 21.07/21.07 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence). 21.07/21.07 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence). 21.07/21.07 ->(x1,y) -> ->(j(x1),j(y)) # label(congruence). 21.07/21.07 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence). 21.07/21.07 ->*(x,x) # label(reflexivity). 21.07/21.07 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 21.07/21.07 ->*(x,y) & ->*(z,y) -> ->*<-(x,z) # label(joinability). 21.07/21.07 end_of_list. 21.07/21.07 21.07/21.07 formulas(goals). 21.07/21.07 (exists x3 ->*<-(d,h(f(x3)))) # label(goal). 21.07/21.07 end_of_list. 21.07/21.07 21.07/21.07 ============================== end of input ========================== 21.07/21.07 21.07/21.07 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 21.07/21.07 21.07/21.07 % Formulas that are not ordinary clauses: 21.07/21.07 1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 21.07/21.07 2 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 21.07/21.07 3 ->(x1,y) -> ->(j(x1),j(y)) # label(congruence) # label(non_clause). [assumption]. 21.07/21.07 4 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 21.07/21.07 5 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 21.07/21.07 6 ->*(x,y) & ->*(z,y) -> ->*<-(x,z) # label(joinability) # label(non_clause). [assumption]. 21.07/21.07 7 (exists x3 ->*<-(d,h(f(x3)))) # label(goal) # label(non_clause) # label(goal). [goal]. 21.07/21.07 21.07/21.07 ============================== end of process non-clausal formulas === 21.07/21.07 21.07/21.07 ============================== CLAUSES FOR SEARCH ==================== 21.07/21.07 21.07/21.07 formulas(mace4_clauses). 21.07/21.07 -->(x,y) | ->(f(x),f(y)) # label(congruence). 21.07/21.07 -->(x,y) | ->(h(x),h(y)) # label(congruence). 21.07/21.07 -->(x,y) | ->(j(x),j(y)) # label(congruence). 21.07/21.07 -->(x,y) | ->(g(x),g(y)) # label(congruence). 21.07/21.07 ->*(x,x) # label(reflexivity). 21.07/21.07 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 21.07/21.07 -->*(x,y) | -->*(z,y) | ->*<-(x,z) # label(joinability). 21.07/21.07 -->*<-(d,h(f(x))) # label(goal). 21.07/21.07 end_of_list. 21.07/21.07 21.07/21.07 ============================== end of clauses for search ============= 21.07/21.07 21.07/21.07 % There are no natural numbers in the input. 21.07/21.07 21.07/21.07 ============================== DOMAIN SIZE 2 ========================= 21.07/21.07 21.07/21.07 ============================== MODEL ================================= 21.07/21.07 21.07/21.07 interpretation( 2, [number=1, seconds=0], [ 21.07/21.07 21.07/21.07 function(d, [ 0 ]), 21.07/21.07 21.07/21.07 function(g(_), [ 0, 0 ]), 21.07/21.07 21.07/21.07 function(f(_), [ 0, 0 ]), 21.07/21.07 21.07/21.07 function(h(_), [ 1, 0 ]), 21.07/21.07 21.07/21.07 function(j(_), [ 0, 0 ]), 21.07/21.07 21.07/21.07 relation(->*(_,_), [ 21.07/21.07 1, 0, 21.07/21.07 0, 1 ]), 21.07/21.07 21.07/21.07 relation(->(_,_), [ 21.07/21.07 0, 0, 21.07/21.07 0, 0 ]), 21.07/21.07 21.07/21.07 relation(->*<-(_,_), [ 21.07/21.07 1, 0, 21.07/21.07 0, 1 ]) 21.07/21.07 ]). 21.07/21.07 21.07/21.07 ============================== end of model ========================== 21.07/21.07 21.07/21.07 ============================== STATISTICS ============================ 21.07/21.07 21.07/21.07 For domain size 2. 21.07/21.07 21.07/21.07 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 21.07/21.07 Ground clauses: seen=36, kept=31. 21.07/21.07 Selections=10, assignments=10, propagations=11, current_models=1. 21.07/21.07 Rewrite_terms=38, rewrite_bools=41, indexes=6. 21.07/21.07 Rules_from_neg_clauses=1, cross_offs=1. 21.07/21.07 21.07/21.07 ============================== end of statistics ===================== 21.07/21.07 21.07/21.07 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 21.07/21.07 21.07/21.07 Exiting with 1 model. 21.07/21.07 21.07/21.07 Process 86444 exit (max_models) Wed Mar 9 10:49:28 2022 21.07/21.07 The process finished Wed Mar 9 10:49:28 2022 21.07/21.07 21.07/21.07 21.07/21.07 Mace4 cooked interpretation: 21.07/21.07 21.07/21.07 21.07/21.07 21.07/21.07 The problem is infeasible. 21.07/21.07 21.07/21.07 21.07/21.07 CRule InfChecker Info: 21.07/21.07 h(f(a)) -> c 21.07/21.07 Rule remains 21.07/21.07 Proof: 21.07/21.07 NO_CONDS 21.07/21.07 21.07/21.07 CRule InfChecker Info: 21.07/21.07 h(x) -> j(x) 21.07/21.07 Rule remains 21.07/21.07 Proof: 21.07/21.07 NO_CONDS 21.07/21.07 21.07/21.07 CRule InfChecker Info: 21.07/21.07 j(g(b)) -> d 21.07/21.07 Rule remains 21.07/21.07 Proof: 21.07/21.07 NO_CONDS 21.07/21.07 21.07/21.07 Problem 1: 21.07/21.07 21.07/21.07 Transform No Conds CTRS Processor: 21.07/21.07 21.07/21.07 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 21.07/21.07 Confluence Problem: 21.07/21.07 (VAR x) 21.07/21.07 (REPLACEMENT-MAP 21.07/21.07 (a) 21.07/21.07 (c) 21.07/21.07 (f 1) 21.07/21.07 (h 1) 21.07/21.07 (j 1) 21.07/21.07 (b) 21.07/21.07 (d) 21.07/21.07 (fSNonEmpty) 21.07/21.07 (g 1) 21.07/21.07 ) 21.07/21.07 (RULES 21.07/21.07 a -> b 21.07/21.07 c -> j(f(a)) 21.07/21.07 c -> d 21.07/21.07 h(f(a)) -> c 21.07/21.07 h(x) -> j(x) 21.07/21.07 j(g(b)) -> d 21.07/21.07 ) 21.07/21.07 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 21.07/21.07 Resulting R: 21.07/21.07 (VAR x) 21.07/21.07 (STRATEGY CONTEXTSENSITIVE 21.07/21.07 (a) 21.07/21.07 (c) 21.07/21.07 (f 1) 21.07/21.07 (h 1) 21.07/21.07 (j 1) 21.07/21.07 (b) 21.07/21.07 (d) 21.07/21.07 (fSNonEmpty) 21.07/21.07 (g 1) 21.07/21.07 ) 21.07/21.07 (RULES 21.07/21.07 a -> b 21.07/21.07 c -> j(f(a)) 21.07/21.07 c -> d 21.07/21.07 h(f(a)) -> c 21.07/21.07 h(x) -> j(x) 21.07/21.07 j(g(b)) -> d 21.07/21.07 ) 21.07/21.07 21.07/21.07 Problem 1: 21.07/21.07 21.07/21.07 CleanTRS Processor: 21.07/21.07 21.07/21.07 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 21.07/21.07 Confluence Problem: 21.07/21.07 (VAR x) 21.07/21.07 (REPLACEMENT-MAP 21.07/21.07 (a) 21.07/21.07 (c) 21.07/21.07 (f 1) 21.07/21.07 (h 1) 21.07/21.07 (j 1) 21.07/21.07 (b) 21.07/21.07 (d) 21.07/21.07 (fSNonEmpty) 21.07/21.07 (g 1) 21.07/21.07 ) 21.07/21.07 (RULES 21.07/21.07 a -> b 21.07/21.07 c -> j(f(a)) 21.07/21.07 c -> d 21.07/21.07 h(f(a)) -> c 21.07/21.07 h(x) -> j(x) 21.07/21.07 j(g(b)) -> d 21.07/21.07 ) 21.07/21.07 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 21.07/21.07 21.07/21.07 21.07/21.07 Problem 1: 21.07/21.07 21.07/21.07 Modular Confluence Combinations Decomposition Processor: 21.07/21.07 21.07/21.07 No usable combinations 21.07/21.07 21.07/21.07 Problem 1: 21.07/21.07 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 21.07/21.07 Confluence Problem: 21.07/21.07 (VAR x) 21.07/21.07 (REPLACEMENT-MAP 21.07/21.07 (a) 21.07/21.07 (c) 21.07/21.07 (f 1) 21.07/21.07 (h 1) 21.07/21.07 (j 1) 21.07/21.07 (b) 21.07/21.07 (d) 21.07/21.07 (fSNonEmpty) 21.07/21.07 (g 1) 21.07/21.07 ) 21.07/21.07 (RULES 21.07/21.07 a -> b 21.07/21.07 c -> j(f(a)) 21.07/21.07 c -> d 21.07/21.07 h(f(a)) -> c 21.07/21.07 h(x) -> j(x) 21.07/21.07 j(g(b)) -> d 21.07/21.07 ) 21.07/21.07 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 21.07/21.07 21.07/21.07 Huet Levy Processor: 21.07/21.07 -> Rules: 21.07/21.07 a -> b 21.07/21.07 c -> j(f(a)) 21.07/21.07 c -> d 21.07/21.07 h(f(a)) -> c 21.07/21.07 h(x) -> j(x) 21.07/21.07 j(g(b)) -> d 21.07/21.07 -> Vars: 21.07/21.07 x 21.07/21.07 21.07/21.07 -> Rlps: 21.07/21.07 (rule: a -> b, id: 1, possubterms: a->[]) 21.07/21.07 (rule: c -> j(f(a)), id: 2, possubterms: c->[]) 21.07/21.07 (rule: c -> d, id: 3, possubterms: c->[]) 21.07/21.07 (rule: h(f(a)) -> c, id: 4, possubterms: h(f(a))->[], f(a)->[1], a->[1, 1]) 21.07/21.07 (rule: h(x) -> j(x), id: 5, possubterms: h(x)->[]) 21.07/21.07 (rule: j(g(b)) -> d, id: 6, possubterms: j(g(b))->[], g(b)->[1], b->[1, 1]) 21.07/21.07 21.07/21.07 -> Unifications: 21.07/21.07 (R3 unifies with R2 at p: [], l: c, lp: c, sig: {}, l': c, r: d, r': j(f(a))) 21.07/21.07 (R4 unifies with R1 at p: [1,1], l: h(f(a)), lp: a, sig: {}, l': a, r: c, r': b) 21.07/21.07 (R5 unifies with R4 at p: [], l: h(x), lp: h(x), sig: {x -> f(a)}, l': h(f(a)), r: j(x), r': c) 21.07/21.07 21.07/21.07 -> Critical pairs info: 21.07/21.07 => Not trivial, Not overlay, NW0, N1 21.07/21.07 => Not trivial, Overlay, NW0, N2 21.07/21.07 => Not trivial, Overlay, NW0, N3 21.07/21.07 21.07/21.07 -> Problem conclusions: 21.07/21.07 Left linear, Right linear, Linear 21.07/21.07 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 21.07/21.07 Not Huet-Levy confluent, Not Newman confluent 21.07/21.07 R is a TRS 21.07/21.07 21.07/21.07 21.07/21.07 Problem 1: 21.07/21.07 No Convergence Brute Force Processor: 21.07/21.07 -> Rewritings: 21.07/21.07 s: j(f(a)) 21.07/21.07 Nodes: [0,1] 21.07/21.07 Edges: [(0,1)] 21.07/21.07 ID: 0 => ('j(f(a))', D0) 21.07/21.07 ID: 1 => ('j(f(b))', D1, R1, P[1, 1], S{}), NR: 'b' 21.07/21.07 t: d 21.07/21.07 Nodes: [0] 21.07/21.07 Edges: [] 21.07/21.07 ID: 0 => ('d', D0) 21.07/21.07 j(f(a)) ->* no union *<- d 21.07/21.07 "Not joinable" 21.07/21.07 21.07/21.07 The problem is not joinable. 21.07/21.07 21.09user 0.63system 0:21.70elapsed 100%CPU (0avgtext+0avgdata 855860maxresident)k 21.07/21.07 8inputs+0outputs (0major+242720minor)pagefaults 0swaps