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