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