20.011/20.011 NO 20.011/20.011 20.011/20.011 Problem 1: 20.011/20.011 20.011/20.011 20.011/20.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.011/20.011 Confluence Problem: 20.011/20.011 (VAR vNonEmpty x y) 20.011/20.011 (REPLACEMENT-MAP 20.011/20.011 (add 1, 2) 20.011/20.011 (gcd 1, 2) 20.011/20.011 (0) 20.011/20.011 (fSNonEmpty) 20.011/20.011 (false) 20.011/20.011 (leq 1, 2) 20.011/20.011 (s 1) 20.011/20.011 ) 20.011/20.011 (RULES 20.011/20.011 add(0,y) -> y 20.011/20.011 add(s(x),y) -> s(add(x,y)) 20.011/20.011 gcd(add(x,y),y) -> gcd(x,y) 20.011/20.011 gcd(0,x) -> x 20.011/20.011 gcd(x,0) -> x 20.011/20.011 gcd(x,y) -> gcd(y,x) | leq(y,x) ->* false 20.011/20.011 gcd(y,add(x,y)) -> gcd(x,y) 20.011/20.011 ) 20.011/20.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.011/20.011 20.011/20.011 20.011/20.011 Problem 1: 20.011/20.011 20.011/20.011 Inlining of Conditions Processor [STERN17]: 20.011/20.011 20.011/20.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.011/20.011 Confluence Problem: 20.011/20.011 (VAR vNonEmpty x y) 20.011/20.011 (REPLACEMENT-MAP 20.011/20.011 (add 1, 2) 20.011/20.011 (gcd 1, 2) 20.011/20.011 (0) 20.011/20.011 (fSNonEmpty) 20.011/20.011 (false) 20.011/20.011 (leq 1, 2) 20.011/20.011 (s 1) 20.011/20.011 ) 20.011/20.011 (RULES 20.011/20.011 add(0,y) -> y 20.011/20.011 add(s(x),y) -> s(add(x,y)) 20.011/20.011 gcd(add(x,y),y) -> gcd(x,y) 20.011/20.011 gcd(0,x) -> x 20.011/20.011 gcd(x,0) -> x 20.011/20.011 gcd(x,y) -> gcd(y,x) | leq(y,x) ->* false 20.011/20.011 gcd(y,add(x,y)) -> gcd(x,y) 20.011/20.011 ) 20.011/20.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.011/20.011 20.011/20.011 20.011/20.011 Problem 1: 20.011/20.011 20.011/20.011 Clean CTRS Processor: 20.011/20.011 20.011/20.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.011/20.011 Confluence Problem: 20.011/20.011 (VAR x y) 20.011/20.011 (REPLACEMENT-MAP 20.011/20.011 (add 1, 2) 20.011/20.011 (gcd 1, 2) 20.011/20.011 (0) 20.011/20.011 (fSNonEmpty) 20.011/20.011 (false) 20.011/20.011 (leq 1, 2) 20.011/20.011 (s 1) 20.011/20.011 ) 20.011/20.011 (RULES 20.011/20.011 add(0,y) -> y 20.011/20.011 add(s(x),y) -> s(add(x,y)) 20.011/20.011 gcd(add(x,y),y) -> gcd(x,y) 20.011/20.011 gcd(0,x) -> x 20.011/20.011 gcd(x,0) -> x 20.011/20.011 gcd(y,add(x,y)) -> gcd(x,y) 20.011/20.011 ) 20.011/20.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.011/20.011 20.011/20.011 CRule InfChecker Info: 20.011/20.011 add(0,y) -> y 20.011/20.011 Rule remains 20.011/20.011 Proof: 20.011/20.011 NO_CONDS 20.011/20.011 20.011/20.011 CRule InfChecker Info: 20.011/20.011 add(s(x),y) -> s(add(x,y)) 20.011/20.011 Rule remains 20.011/20.011 Proof: 20.011/20.011 NO_CONDS 20.011/20.011 20.011/20.011 CRule InfChecker Info: 20.011/20.011 gcd(add(x,y),y) -> gcd(x,y) 20.011/20.011 Rule remains 20.011/20.011 Proof: 20.011/20.011 NO_CONDS 20.011/20.011 20.011/20.011 CRule InfChecker Info: 20.011/20.011 gcd(0,x) -> x 20.011/20.011 Rule remains 20.011/20.011 Proof: 20.011/20.011 NO_CONDS 20.011/20.011 20.011/20.011 CRule InfChecker Info: 20.011/20.011 gcd(x,0) -> x 20.011/20.011 Rule remains 20.011/20.011 Proof: 20.011/20.011 NO_CONDS 20.011/20.011 20.011/20.011 CRule InfChecker Info: 20.011/20.011 gcd(x,y) -> gcd(y,x) | leq(y,x) ->* false 20.011/20.011 Rule deleted 20.011/20.011 Proof: 20.011/20.011 YES 20.011/20.011 20.011/20.011 Problem 1: 20.011/20.011 20.011/20.011 Infeasibility Problem: 20.011/20.011 [(VAR vNonEmpty x y vNonEmpty x y) 20.011/20.011 (STRATEGY CONTEXTSENSITIVE 20.011/20.011 (add 1 2) 20.011/20.011 (gcd 1 2) 20.011/20.011 (0) 20.011/20.011 (fSNonEmpty) 20.011/20.011 (false) 20.011/20.011 (leq 1 2) 20.011/20.011 (s 1) 20.011/20.011 ) 20.011/20.011 (RULES 20.011/20.011 add(0,y) -> y 20.011/20.011 add(s(x),y) -> s(add(x,y)) 20.011/20.011 gcd(add(x,y),y) -> gcd(x,y) 20.011/20.011 gcd(0,x) -> x 20.011/20.011 gcd(x,0) -> x 20.011/20.011 gcd(x,y) -> gcd(y,x) | leq(y,x) ->* false 20.011/20.011 gcd(y,add(x,y)) -> gcd(x,y) 20.011/20.011 )] 20.011/20.011 20.011/20.011 Infeasibility Conditions: 20.011/20.011 leq(y,x) ->* false 20.011/20.011 20.011/20.011 Problem 1: 20.011/20.011 20.011/20.011 Obtaining a model using Mace4: 20.011/20.011 20.011/20.011 -> Usable Rules: 20.011/20.011 add(0,y) -> y 20.011/20.011 add(s(x),y) -> s(add(x,y)) 20.011/20.011 gcd(add(x,y),y) -> gcd(x,y) 20.011/20.011 gcd(0,x) -> x 20.011/20.011 gcd(x,0) -> x 20.011/20.011 gcd(x,y) -> gcd(y,x) | leq(y,x) ->* false 20.011/20.011 gcd(y,add(x,y)) -> gcd(x,y) 20.011/20.011 20.011/20.011 -> Mace4 Output: 20.011/20.011 ============================== Mace4 ================================= 20.011/20.011 Mace4 (64) version 2009-11A, November 2009. 20.011/20.011 Process 10592 was started by ubuntu on ubuntu, 20.011/20.011 Wed Mar 9 09:13:56 2022 20.011/20.011 The command was "./mace4 -c -f /tmp/mace410581-2.in". 20.011/20.011 ============================== end of head =========================== 20.011/20.011 20.011/20.011 ============================== INPUT ================================= 20.011/20.011 20.011/20.011 % Reading from file /tmp/mace410581-2.in 20.011/20.011 20.011/20.011 assign(max_seconds,20). 20.011/20.011 20.011/20.011 formulas(assumptions). 20.011/20.011 ->(x1,y) -> ->(add(x1,x2),add(y,x2)) # label(congruence). 20.011/20.011 ->(x2,y) -> ->(add(x1,x2),add(x1,y)) # label(congruence). 20.011/20.011 ->(x1,y) -> ->(gcd(x1,x2),gcd(y,x2)) # label(congruence). 20.011/20.011 ->(x2,y) -> ->(gcd(x1,x2),gcd(x1,y)) # label(congruence). 20.011/20.011 ->(x1,y) -> ->(leq(x1,x2),leq(y,x2)) # label(congruence). 20.011/20.011 ->(x2,y) -> ->(leq(x1,x2),leq(x1,y)) # label(congruence). 20.011/20.011 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 20.011/20.011 ->(add(0,x2),x2) # label(replacement). 20.011/20.011 ->(add(s(x1),x2),s(add(x1,x2))) # label(replacement). 20.011/20.011 ->(gcd(add(x1,x2),x2),gcd(x1,x2)) # label(replacement). 20.011/20.011 ->(gcd(0,x1),x1) # label(replacement). 20.011/20.011 ->(gcd(x1,0),x1) # label(replacement). 20.011/20.011 ->*(leq(x2,x1),false) -> ->(gcd(x1,x2),gcd(x2,x1)) # label(replacement). 20.011/20.011 ->(gcd(x2,add(x1,x2)),gcd(x1,x2)) # label(replacement). 20.011/20.011 ->*(x,x) # label(reflexivity). 20.011/20.011 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 20.011/20.011 end_of_list. 20.011/20.011 20.011/20.011 formulas(goals). 20.011/20.011 (exists x4 exists x5 ->*(leq(x5,x4),false)) # label(goal). 20.011/20.011 end_of_list. 20.011/20.011 20.011/20.011 ============================== end of input ========================== 20.011/20.011 20.011/20.011 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 20.011/20.011 20.011/20.011 % Formulas that are not ordinary clauses: 20.011/20.011 1 ->(x1,y) -> ->(add(x1,x2),add(y,x2)) # label(congruence) # label(non_clause). [assumption]. 20.011/20.011 2 ->(x2,y) -> ->(add(x1,x2),add(x1,y)) # label(congruence) # label(non_clause). [assumption]. 20.011/20.011 3 ->(x1,y) -> ->(gcd(x1,x2),gcd(y,x2)) # label(congruence) # label(non_clause). [assumption]. 20.011/20.011 4 ->(x2,y) -> ->(gcd(x1,x2),gcd(x1,y)) # label(congruence) # label(non_clause). [assumption]. 20.011/20.011 5 ->(x1,y) -> ->(leq(x1,x2),leq(y,x2)) # label(congruence) # label(non_clause). [assumption]. 20.011/20.011 6 ->(x2,y) -> ->(leq(x1,x2),leq(x1,y)) # label(congruence) # label(non_clause). [assumption]. 20.011/20.011 7 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 20.011/20.011 8 ->*(leq(x2,x1),false) -> ->(gcd(x1,x2),gcd(x2,x1)) # label(replacement) # label(non_clause). [assumption]. 20.011/20.011 9 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 20.011/20.011 10 (exists x4 exists x5 ->*(leq(x5,x4),false)) # label(goal) # label(non_clause) # label(goal). [goal]. 20.011/20.011 20.011/20.011 ============================== end of process non-clausal formulas === 20.011/20.011 20.011/20.011 ============================== CLAUSES FOR SEARCH ==================== 20.011/20.011 20.011/20.011 formulas(mace4_clauses). 20.011/20.011 -->(x,y) | ->(add(x,z),add(y,z)) # label(congruence). 20.011/20.011 -->(x,y) | ->(add(z,x),add(z,y)) # label(congruence). 20.011/20.011 -->(x,y) | ->(gcd(x,z),gcd(y,z)) # label(congruence). 20.011/20.011 -->(x,y) | ->(gcd(z,x),gcd(z,y)) # label(congruence). 20.011/20.011 -->(x,y) | ->(leq(x,z),leq(y,z)) # label(congruence). 20.011/20.011 -->(x,y) | ->(leq(z,x),leq(z,y)) # label(congruence). 20.011/20.011 -->(x,y) | ->(s(x),s(y)) # label(congruence). 20.011/20.011 ->(add(0,x),x) # label(replacement). 20.011/20.011 ->(add(s(x),y),s(add(x,y))) # label(replacement). 20.011/20.011 ->(gcd(add(x,y),y),gcd(x,y)) # label(replacement). 20.011/20.011 ->(gcd(0,x),x) # label(replacement). 20.011/20.011 ->(gcd(x,0),x) # label(replacement). 20.011/20.011 -->*(leq(x,y),false) | ->(gcd(y,x),gcd(x,y)) # label(replacement). 20.011/20.011 ->(gcd(x,add(y,x)),gcd(y,x)) # label(replacement). 20.011/20.011 ->*(x,x) # label(reflexivity). 20.011/20.011 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 20.011/20.011 -->*(leq(x,y),false) # label(goal). 20.011/20.011 end_of_list. 20.011/20.011 20.011/20.011 ============================== end of clauses for search ============= 20.011/20.011 20.011/20.011 % There are no natural numbers in the input. 20.011/20.011 20.011/20.011 ============================== DOMAIN SIZE 2 ========================= 20.011/20.011 20.011/20.011 ============================== MODEL ================================= 20.011/20.011 20.011/20.011 interpretation( 2, [number=1, seconds=0], [ 20.011/20.011 20.011/20.011 function(0, [ 0 ]), 20.011/20.011 20.011/20.011 function(false, [ 0 ]), 20.011/20.011 20.011/20.011 function(s(_), [ 0, 0 ]), 20.011/20.011 20.011/20.011 function(add(_,_), [ 20.011/20.011 0, 0, 20.011/20.011 0, 0 ]), 20.011/20.011 20.011/20.011 function(gcd(_,_), [ 20.011/20.011 0, 0, 20.011/20.011 0, 0 ]), 20.011/20.011 20.011/20.011 function(leq(_,_), [ 20.011/20.011 1, 1, 20.011/20.011 1, 1 ]), 20.011/20.011 20.011/20.011 relation(->*(_,_), [ 20.011/20.011 1, 1, 20.011/20.011 0, 1 ]), 20.011/20.011 20.011/20.011 relation(->(_,_), [ 20.011/20.011 1, 1, 20.011/20.011 0, 1 ]) 20.011/20.011 ]). 20.011/20.011 20.011/20.011 ============================== end of model ========================== 20.011/20.011 20.011/20.011 ============================== STATISTICS ============================ 20.011/20.011 20.011/20.011 For domain size 2. 20.011/20.011 20.011/20.011 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 20.011/20.011 Ground clauses: seen=88, kept=84. 20.011/20.011 Selections=9, assignments=9, propagations=15, current_models=1. 20.011/20.011 Rewrite_terms=180, rewrite_bools=119, indexes=18. 20.011/20.011 Rules_from_neg_clauses=7, cross_offs=7. 20.011/20.011 20.011/20.011 ============================== end of statistics ===================== 20.011/20.011 20.011/20.011 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 20.011/20.011 20.011/20.011 Exiting with 1 model. 20.011/20.011 20.011/20.011 Process 10592 exit (max_models) Wed Mar 9 09:13:56 2022 20.011/20.011 The process finished Wed Mar 9 09:13:56 2022 20.011/20.011 20.011/20.011 20.011/20.011 Mace4 cooked interpretation: 20.011/20.011 20.011/20.011 20.011/20.011 20.011/20.011 The problem is infeasible. 20.011/20.011 20.011/20.011 20.011/20.011 CRule InfChecker Info: 20.011/20.011 gcd(y,add(x,y)) -> gcd(x,y) 20.011/20.011 Rule remains 20.011/20.011 Proof: 20.011/20.011 NO_CONDS 20.011/20.011 20.011/20.011 Problem 1: 20.011/20.011 20.011/20.011 Transform No Conds CTRS Processor: 20.011/20.011 20.011/20.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.011/20.011 Confluence Problem: 20.011/20.011 (VAR x y) 20.011/20.011 (REPLACEMENT-MAP 20.011/20.011 (add 1, 2) 20.011/20.011 (gcd 1, 2) 20.011/20.011 (0) 20.011/20.011 (fSNonEmpty) 20.011/20.011 (false) 20.011/20.011 (leq 1, 2) 20.011/20.011 (s 1) 20.011/20.011 ) 20.011/20.011 (RULES 20.011/20.011 add(0,y) -> y 20.011/20.011 add(s(x),y) -> s(add(x,y)) 20.011/20.011 gcd(add(x,y),y) -> gcd(x,y) 20.011/20.011 gcd(0,x) -> x 20.011/20.011 gcd(x,0) -> x 20.011/20.011 gcd(y,add(x,y)) -> gcd(x,y) 20.011/20.011 ) 20.011/20.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.011/20.011 Resulting R: 20.011/20.011 (VAR x y) 20.011/20.011 (STRATEGY CONTEXTSENSITIVE 20.011/20.011 (add 1 2) 20.011/20.011 (gcd 1 2) 20.011/20.011 (0) 20.011/20.011 (fSNonEmpty) 20.011/20.011 (false) 20.011/20.011 (leq 1 2) 20.011/20.011 (s 1) 20.011/20.011 ) 20.011/20.011 (RULES 20.011/20.011 add(0,y) -> y 20.011/20.011 add(s(x),y) -> s(add(x,y)) 20.011/20.011 gcd(add(x,y),y) -> gcd(x,y) 20.011/20.011 gcd(0,x) -> x 20.011/20.011 gcd(x,0) -> x 20.011/20.011 gcd(y,add(x,y)) -> gcd(x,y) 20.011/20.011 ) 20.011/20.011 20.011/20.011 Problem 1: 20.011/20.011 20.011/20.011 CleanTRS Processor: 20.011/20.011 20.011/20.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.011/20.011 Confluence Problem: 20.011/20.011 (VAR x y) 20.011/20.011 (REPLACEMENT-MAP 20.011/20.011 (add 1, 2) 20.011/20.011 (gcd 1, 2) 20.011/20.011 (0) 20.011/20.011 (fSNonEmpty) 20.011/20.011 (false) 20.011/20.011 (leq 1, 2) 20.011/20.011 (s 1) 20.011/20.011 ) 20.011/20.011 (RULES 20.011/20.011 add(0,y) -> y 20.011/20.011 add(s(x),y) -> s(add(x,y)) 20.011/20.011 gcd(add(x,y),y) -> gcd(x,y) 20.011/20.011 gcd(0,x) -> x 20.011/20.011 gcd(x,0) -> x 20.011/20.011 gcd(y,add(x,y)) -> gcd(x,y) 20.011/20.011 ) 20.011/20.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.011/20.011 20.011/20.011 20.011/20.011 Problem 1: 20.011/20.011 20.011/20.011 Modular Confluence Combinations Decomposition Processor: 20.011/20.011 20.011/20.011 No usable combinations 20.011/20.011 20.011/20.011 Problem 1: 20.011/20.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.011/20.011 Confluence Problem: 20.011/20.011 (VAR x y) 20.011/20.011 (REPLACEMENT-MAP 20.011/20.011 (add 1, 2) 20.011/20.011 (gcd 1, 2) 20.011/20.011 (0) 20.011/20.011 (fSNonEmpty) 20.011/20.011 (false) 20.011/20.011 (leq 1, 2) 20.011/20.011 (s 1) 20.011/20.011 ) 20.011/20.011 (RULES 20.011/20.011 add(0,y) -> y 20.011/20.011 add(s(x),y) -> s(add(x,y)) 20.011/20.011 gcd(add(x,y),y) -> gcd(x,y) 20.011/20.011 gcd(0,x) -> x 20.011/20.011 gcd(x,0) -> x 20.011/20.011 gcd(y,add(x,y)) -> gcd(x,y) 20.011/20.011 ) 20.011/20.011 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 20.011/20.011 20.011/20.011 Huet Levy Processor: 20.011/20.011 -> Rules: 20.011/20.011 add(0,y) -> y 20.011/20.011 add(s(x),y) -> s(add(x,y)) 20.011/20.011 gcd(add(x,y),y) -> gcd(x,y) 20.011/20.011 gcd(0,x) -> x 20.011/20.011 gcd(x,0) -> x 20.011/20.011 gcd(y,add(x,y)) -> gcd(x,y) 20.011/20.011 -> Vars: 20.011/20.011 y, x, y, x, y, x, x, x, y 20.011/20.011 20.011/20.011 -> Rlps: 20.011/20.011 (rule: add(0,y) -> y, id: 1, possubterms: add(0,y)->[], 0->[1]) 20.011/20.011 (rule: add(s(x),y) -> s(add(x,y)), id: 2, possubterms: add(s(x),y)->[], s(x)->[1]) 20.011/20.011 (rule: gcd(add(x,y),y) -> gcd(x,y), id: 3, possubterms: gcd(add(x,y),y)->[], add(x,y)->[1]) 20.011/20.011 (rule: gcd(0,x) -> x, id: 4, possubterms: gcd(0,x)->[], 0->[1]) 20.011/20.011 (rule: gcd(x,0) -> x, id: 5, possubterms: gcd(x,0)->[], 0->[2]) 20.011/20.011 (rule: gcd(y,add(x,y)) -> gcd(x,y), id: 6, possubterms: gcd(y,add(x,y))->[], add(x,y)->[2]) 20.011/20.011 20.011/20.011 -> Unifications: 20.011/20.011 (R3 unifies with R1 at p: [1], l: gcd(add(x,y),y), lp: add(x,y), sig: {x -> 0,y -> y'}, l': add(0,y'), r: gcd(x,y), r': y') 20.011/20.011 (R3 unifies with R2 at p: [1], l: gcd(add(x,y),y), lp: add(x,y), sig: {x -> s(x'),y -> y'}, l': add(s(x'),y'), r: gcd(x,y), r': s(add(x',y'))) 20.011/20.011 (R5 unifies with R3 at p: [], l: gcd(x,0), lp: gcd(x,0), sig: {x -> add(x',0),y -> 0}, l': gcd(add(x',y),y), r: x, r': gcd(x',y)) 20.011/20.011 (R5 unifies with R4 at p: [], l: gcd(x,0), lp: gcd(x,0), sig: {x -> 0,x' -> 0}, l': gcd(0,x'), r: x, r': x') 20.011/20.011 (R6 unifies with R4 at p: [], l: gcd(y,add(x,y)), lp: gcd(y,add(x,y)), sig: {y -> 0,x' -> add(x,0)}, l': gcd(0,x'), r: gcd(x,y), r': x') 20.011/20.011 (R6 unifies with R1 at p: [2], l: gcd(y,add(x,y)), lp: add(x,y), sig: {x -> 0,y -> y'}, l': add(0,y'), r: gcd(x,y), r': y') 20.011/20.011 (R6 unifies with R2 at p: [2], l: gcd(y,add(x,y)), lp: add(x,y), sig: {x -> s(x'),y -> y'}, l': add(s(x'),y'), r: gcd(x,y), r': s(add(x',y'))) 20.011/20.011 20.011/20.011 -> Critical pairs info: 20.011/20.011 => Not trivial, Not overlay, NW0, N1 20.011/20.011 => Not trivial, Overlay, NW0, N2 20.011/20.011 => Not trivial, Overlay, NW0, N3 20.011/20.011 <0,0> => Trivial, Overlay, NW0, N4 20.011/20.011 => Not trivial, Not overlay, NW0, N5 20.011/20.011 => Not trivial, Not overlay, NW0, N6 20.011/20.011 => Not trivial, Not overlay, NW0, N7 20.011/20.011 20.011/20.011 -> Problem conclusions: 20.011/20.011 Not left linear, Right linear, Not linear 20.011/20.011 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 20.011/20.011 Not Huet-Levy confluent, Not Newman confluent 20.011/20.011 R is a TRS 20.011/20.011 20.011/20.011 20.011/20.011 Problem 1: 20.011/20.011 Different Normal CP Terms Processor: 20.011/20.011 => Not trivial, Not overlay, NW0, N6, Normal and not trivial cp 20.011/20.011 20.011/20.011 The problem is not joinable. 20.011/20.011 17.98user 2.35system 0:20.11elapsed 101%CPU (0avgtext+0avgdata 35572maxresident)k 20.011/20.011 8inputs+0outputs (0major+20281minor)pagefaults 0swaps