29.91/20.13 NO 29.91/20.13 29.91/20.13 Problem 1: 29.91/20.13 29.91/20.13 29.91/20.13 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 29.91/20.13 Confluence Problem: 29.91/20.13 (VAR vNonEmpty x y) 29.91/20.13 (REPLACEMENT-MAP 29.91/20.13 (add 1, 2) 29.91/20.13 (gcd 1, 2) 29.91/20.13 (0) 29.91/20.13 (fSNonEmpty) 29.91/20.13 (false) 29.91/20.13 (leq 1, 2) 29.91/20.13 (s 1) 29.91/20.13 ) 29.91/20.13 (RULES 29.91/20.13 add(0,y) -> y 29.91/20.13 add(s(x),y) -> s(add(x,y)) 29.91/20.13 gcd(add(x,y),y) -> gcd(x,y) 29.91/20.13 gcd(0,x) -> x 29.91/20.13 gcd(x,0) -> x 29.91/20.13 gcd(x,y) -> gcd(y,x) | leq(y,x) ->* false 29.91/20.13 gcd(y,add(x,y)) -> gcd(x,y) 29.91/20.13 ) 29.91/20.13 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 29.91/20.13 29.91/20.13 29.91/20.13 Problem 1: 29.91/20.13 29.91/20.13 Problem 1: 29.91/20.13 29.91/20.13 Clean CTRS Procedure: 29.91/20.13 29.91/20.13 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 29.91/20.13 Confluence Problem: 29.91/20.13 (VAR x y) 29.91/20.13 (REPLACEMENT-MAP 29.91/20.13 (add 1, 2) 29.91/20.13 (gcd 1, 2) 29.91/20.13 (0) 29.91/20.13 (fSNonEmpty) 29.91/20.13 (false) 29.91/20.13 (leq 1, 2) 29.91/20.13 (s 1) 29.91/20.13 ) 29.91/20.13 (RULES 29.91/20.13 add(0,y) -> y 29.91/20.13 add(s(x),y) -> s(add(x,y)) 29.91/20.13 gcd(add(x,y),y) -> gcd(x,y) 29.91/20.13 gcd(0,x) -> x 29.91/20.13 gcd(x,0) -> x 29.91/20.13 gcd(y,add(x,y)) -> gcd(x,y) 29.91/20.13 ) 29.91/20.13 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 29.91/20.13 29.91/20.13 CRule InfChecker Info: 29.91/20.13 add(0,y) -> y 29.91/20.13 Rule remains 29.91/20.13 Proof: 29.91/20.13 NO_CONDS 29.91/20.13 29.91/20.13 CRule InfChecker Info: 29.91/20.13 add(s(x),y) -> s(add(x,y)) 29.91/20.13 Rule remains 29.91/20.13 Proof: 29.91/20.13 NO_CONDS 29.91/20.13 29.91/20.13 CRule InfChecker Info: 29.91/20.13 gcd(add(x,y),y) -> gcd(x,y) 29.91/20.13 Rule remains 29.91/20.13 Proof: 29.91/20.13 NO_CONDS 29.91/20.13 29.91/20.13 CRule InfChecker Info: 29.91/20.13 gcd(0,x) -> x 29.91/20.13 Rule remains 29.91/20.13 Proof: 29.91/20.13 NO_CONDS 29.91/20.13 29.91/20.13 CRule InfChecker Info: 29.91/20.13 gcd(x,0) -> x 29.91/20.13 Rule remains 29.91/20.13 Proof: 29.91/20.13 NO_CONDS 29.91/20.13 29.91/20.13 CRule InfChecker Info: 29.91/20.13 gcd(x,y) -> gcd(y,x) | leq(y,x) ->* false 29.91/20.13 Rule deleted 29.91/20.13 Proof: 29.91/20.13 YES 29.91/20.13 29.91/20.13 Problem 1: 29.91/20.13 29.91/20.13 Infeasibility Problem: 29.91/20.13 [(VAR vNonEmpty x y vNonEmpty x y) 29.91/20.13 (STRATEGY CONTEXTSENSITIVE 29.91/20.13 (add 1 2) 29.91/20.13 (gcd 1 2) 29.91/20.13 (0) 29.91/20.13 (fSNonEmpty) 29.91/20.13 (false) 29.91/20.13 (leq 1 2) 29.91/20.13 (s 1) 29.91/20.13 ) 29.91/20.13 (RULES 29.91/20.13 add(0,y) -> y 29.91/20.13 add(s(x),y) -> s(add(x,y)) 29.91/20.13 gcd(add(x,y),y) -> gcd(x,y) 29.91/20.13 gcd(0,x) -> x 29.91/20.13 gcd(x,0) -> x 29.91/20.13 gcd(x,y) -> gcd(y,x) | leq(y,x) ->* false 29.91/20.13 gcd(y,add(x,y)) -> gcd(x,y) 29.91/20.13 )] 29.91/20.13 29.91/20.13 Infeasibility Conditions: 29.91/20.13 leq(y,x) ->* false 29.91/20.13 29.91/20.13 Problem 1: 29.91/20.13 29.91/20.13 Obtaining a model using Mace4: 29.91/20.13 29.91/20.13 -> Usable Rules: 29.91/20.13 add(0,y) -> y 29.91/20.13 add(s(x),y) -> s(add(x,y)) 29.91/20.13 gcd(add(x,y),y) -> gcd(x,y) 29.91/20.13 gcd(0,x) -> x 29.91/20.13 gcd(x,0) -> x 29.91/20.13 gcd(x,y) -> gcd(y,x) | leq(y,x) ->* false 29.91/20.13 gcd(y,add(x,y)) -> gcd(x,y) 29.91/20.13 29.91/20.13 -> Mace4 Output: 29.91/20.13 ============================== Mace4 ================================= 29.91/20.13 Mace4 (64) version 2009-11A, November 2009. 29.91/20.13 Process 45262 was started by sandbox on n122.star.cs.uiowa.edu, 29.91/20.13 Wed Jul 13 07:22:45 2022 29.91/20.13 The command was "./mace4 -c -f /tmp/mace445250.in". 29.91/20.13 ============================== end of head =========================== 29.91/20.13 29.91/20.13 ============================== INPUT ================================= 29.91/20.13 29.91/20.13 % Reading from file /tmp/mace445250.in 29.91/20.13 29.91/20.13 assign(max_seconds,10). 29.91/20.13 29.91/20.13 formulas(assumptions). 29.91/20.13 ->(x1,y) -> ->(add(x1,x2),add(y,x2)) # label(congruence). 29.91/20.13 ->(x2,y) -> ->(add(x1,x2),add(x1,y)) # label(congruence). 29.91/20.13 ->(x1,y) -> ->(gcd(x1,x2),gcd(y,x2)) # label(congruence). 29.91/20.13 ->(x2,y) -> ->(gcd(x1,x2),gcd(x1,y)) # label(congruence). 29.91/20.13 ->(x1,y) -> ->(leq(x1,x2),leq(y,x2)) # label(congruence). 29.91/20.13 ->(x2,y) -> ->(leq(x1,x2),leq(x1,y)) # label(congruence). 29.91/20.13 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 29.91/20.13 ->(add(0,x2),x2) # label(replacement). 29.91/20.13 ->(add(s(x1),x2),s(add(x1,x2))) # label(replacement). 29.91/20.13 ->(gcd(add(x1,x2),x2),gcd(x1,x2)) # label(replacement). 29.91/20.13 ->(gcd(0,x1),x1) # label(replacement). 29.91/20.13 ->(gcd(x1,0),x1) # label(replacement). 29.91/20.13 ->*(leq(x2,x1),false) -> ->(gcd(x1,x2),gcd(x2,x1)) # label(replacement). 29.91/20.13 ->(gcd(x2,add(x1,x2)),gcd(x1,x2)) # label(replacement). 29.91/20.13 ->*(x,x) # label(reflexivity). 29.91/20.13 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 29.91/20.13 end_of_list. 29.91/20.13 29.91/20.13 formulas(goals). 29.91/20.13 (exists x4 exists x5 ->*(leq(x5,x4),false)) # label(goal). 29.91/20.13 end_of_list. 29.91/20.13 29.91/20.13 ============================== end of input ========================== 29.91/20.13 29.91/20.13 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 29.91/20.13 29.91/20.13 % Formulas that are not ordinary clauses: 29.91/20.13 1 ->(x1,y) -> ->(add(x1,x2),add(y,x2)) # label(congruence) # label(non_clause). [assumption]. 29.91/20.13 2 ->(x2,y) -> ->(add(x1,x2),add(x1,y)) # label(congruence) # label(non_clause). [assumption]. 29.91/20.13 3 ->(x1,y) -> ->(gcd(x1,x2),gcd(y,x2)) # label(congruence) # label(non_clause). [assumption]. 29.91/20.13 4 ->(x2,y) -> ->(gcd(x1,x2),gcd(x1,y)) # label(congruence) # label(non_clause). [assumption]. 29.91/20.13 5 ->(x1,y) -> ->(leq(x1,x2),leq(y,x2)) # label(congruence) # label(non_clause). [assumption]. 29.91/20.13 6 ->(x2,y) -> ->(leq(x1,x2),leq(x1,y)) # label(congruence) # label(non_clause). [assumption]. 29.91/20.13 7 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 29.91/20.13 8 ->*(leq(x2,x1),false) -> ->(gcd(x1,x2),gcd(x2,x1)) # label(replacement) # label(non_clause). [assumption]. 29.91/20.13 9 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 29.91/20.13 10 (exists x4 exists x5 ->*(leq(x5,x4),false)) # label(goal) # label(non_clause) # label(goal). [goal]. 29.91/20.13 29.91/20.13 ============================== end of process non-clausal formulas === 29.91/20.13 29.91/20.13 ============================== CLAUSES FOR SEARCH ==================== 29.91/20.13 29.91/20.13 formulas(mace4_clauses). 29.91/20.13 -->(x,y) | ->(add(x,z),add(y,z)) # label(congruence). 29.91/20.13 -->(x,y) | ->(add(z,x),add(z,y)) # label(congruence). 29.91/20.13 -->(x,y) | ->(gcd(x,z),gcd(y,z)) # label(congruence). 29.91/20.13 -->(x,y) | ->(gcd(z,x),gcd(z,y)) # label(congruence). 29.91/20.13 -->(x,y) | ->(leq(x,z),leq(y,z)) # label(congruence). 29.91/20.13 -->(x,y) | ->(leq(z,x),leq(z,y)) # label(congruence). 29.91/20.13 -->(x,y) | ->(s(x),s(y)) # label(congruence). 29.91/20.13 ->(add(0,x),x) # label(replacement). 29.91/20.13 ->(add(s(x),y),s(add(x,y))) # label(replacement). 29.91/20.13 ->(gcd(add(x,y),y),gcd(x,y)) # label(replacement). 29.91/20.13 ->(gcd(0,x),x) # label(replacement). 29.91/20.13 ->(gcd(x,0),x) # label(replacement). 29.91/20.13 -->*(leq(x,y),false) | ->(gcd(y,x),gcd(x,y)) # label(replacement). 29.91/20.13 ->(gcd(x,add(y,x)),gcd(y,x)) # label(replacement). 29.91/20.13 ->*(x,x) # label(reflexivity). 29.91/20.13 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 29.91/20.13 -->*(leq(x,y),false) # label(goal). 29.91/20.13 end_of_list. 29.91/20.13 29.91/20.13 ============================== end of clauses for search ============= 29.91/20.13 29.91/20.13 % There are no natural numbers in the input. 29.91/20.13 29.91/20.13 ============================== DOMAIN SIZE 2 ========================= 29.91/20.13 29.91/20.13 ============================== MODEL ================================= 29.91/20.13 29.91/20.13 interpretation( 2, [number=1, seconds=0], [ 29.91/20.13 29.91/20.13 function(0, [ 0 ]), 29.91/20.13 29.91/20.13 function(false, [ 0 ]), 29.91/20.13 29.91/20.13 function(s(_), [ 0, 0 ]), 29.91/20.13 29.91/20.13 function(add(_,_), [ 29.91/20.13 0, 0, 29.91/20.13 0, 0 ]), 29.91/20.13 29.91/20.13 function(gcd(_,_), [ 29.91/20.13 0, 0, 29.91/20.13 0, 0 ]), 29.91/20.13 29.91/20.13 function(leq(_,_), [ 29.91/20.13 1, 1, 29.91/20.13 1, 1 ]), 29.91/20.13 29.91/20.13 relation(->*(_,_), [ 29.91/20.13 1, 1, 29.91/20.13 0, 1 ]), 29.91/20.13 29.91/20.13 relation(->(_,_), [ 29.91/20.13 1, 1, 29.91/20.13 0, 1 ]) 29.91/20.13 ]). 29.91/20.13 29.91/20.13 ============================== end of model ========================== 29.91/20.13 29.91/20.13 ============================== STATISTICS ============================ 29.91/20.13 29.91/20.13 For domain size 2. 29.91/20.13 29.91/20.13 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 29.91/20.13 Ground clauses: seen=88, kept=84. 29.91/20.13 Selections=9, assignments=9, propagations=15, current_models=1. 29.91/20.13 Rewrite_terms=180, rewrite_bools=119, indexes=18. 29.91/20.13 Rules_from_neg_clauses=7, cross_offs=7. 29.91/20.13 29.91/20.13 ============================== end of statistics ===================== 29.91/20.13 29.91/20.13 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 29.91/20.13 29.91/20.13 Exiting with 1 model. 29.91/20.13 29.91/20.13 Process 45262 exit (max_models) Wed Jul 13 07:22:45 2022 29.91/20.13 The process finished Wed Jul 13 07:22:45 2022 29.91/20.13 29.91/20.13 29.91/20.13 Mace4 cooked interpretation: 29.91/20.13 29.91/20.13 29.91/20.13 29.91/20.13 The problem is infeasible. 29.91/20.13 29.91/20.13 29.91/20.13 CRule InfChecker Info: 29.91/20.13 gcd(y,add(x,y)) -> gcd(x,y) 29.91/20.13 Rule remains 29.91/20.13 Proof: 29.91/20.13 NO_CONDS 29.91/20.13 29.91/20.13 Problem 1: 29.91/20.13 29.91/20.13 Transform No Conds CTRS Procedure: 29.91/20.13 29.91/20.13 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 29.91/20.13 Confluence Problem: 29.91/20.13 (VAR x y) 29.91/20.13 (REPLACEMENT-MAP 29.91/20.13 (add 1, 2) 29.91/20.13 (gcd 1, 2) 29.91/20.13 (0) 29.91/20.13 (fSNonEmpty) 29.91/20.13 (false) 29.91/20.13 (leq 1, 2) 29.91/20.13 (s 1) 29.91/20.13 ) 29.91/20.13 (RULES 29.91/20.13 add(0,y) -> y 29.91/20.13 add(s(x),y) -> s(add(x,y)) 29.91/20.13 gcd(add(x,y),y) -> gcd(x,y) 29.91/20.13 gcd(0,x) -> x 29.91/20.13 gcd(x,0) -> x 29.91/20.13 gcd(y,add(x,y)) -> gcd(x,y) 29.91/20.13 ) 29.91/20.13 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 29.91/20.13 29.91/20.13 29.91/20.13 Problem 1: 29.91/20.13 29.91/20.13 29.91/20.13 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 29.91/20.13 Confluence Problem: 29.91/20.13 (VAR x y) 29.91/20.13 (REPLACEMENT-MAP 29.91/20.13 (add 1, 2) 29.91/20.13 (gcd 1, 2) 29.91/20.13 (0) 29.91/20.13 (fSNonEmpty) 29.91/20.13 (false) 29.91/20.13 (leq 1, 2) 29.91/20.13 (s 1) 29.91/20.13 ) 29.91/20.13 (RULES 29.91/20.13 add(0,y) -> y 29.91/20.13 add(s(x),y) -> s(add(x,y)) 29.91/20.13 gcd(add(x,y),y) -> gcd(x,y) 29.91/20.13 gcd(0,x) -> x 29.91/20.13 gcd(x,0) -> x 29.91/20.13 gcd(y,add(x,y)) -> gcd(x,y) 29.91/20.13 ) 29.91/20.13 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 29.91/20.13 29.91/20.13 29.91/20.13 Problem 1: 29.91/20.13 29.91/20.13 Problem 1: 29.91/20.13 Not CS-TRS Procedure: 29.91/20.13 R is not a CS-TRS 29.91/20.13 29.91/20.13 Problem 1: 29.91/20.13 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 29.91/20.13 Confluence Problem: 29.91/20.13 (VAR x y) 29.91/20.13 (REPLACEMENT-MAP 29.91/20.13 (add 1, 2) 29.91/20.13 (gcd 1, 2) 29.91/20.13 (0) 29.91/20.13 (fSNonEmpty) 29.91/20.13 (false) 29.91/20.13 (leq 1, 2) 29.91/20.13 (s 1) 29.91/20.13 ) 29.91/20.13 (RULES 29.91/20.13 add(0,y) -> y 29.91/20.13 add(s(x),y) -> s(add(x,y)) 29.91/20.13 gcd(add(x,y),y) -> gcd(x,y) 29.91/20.13 gcd(0,x) -> x 29.91/20.13 gcd(x,0) -> x 29.91/20.13 gcd(y,add(x,y)) -> gcd(x,y) 29.91/20.13 ) 29.91/20.13 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 29.91/20.13 29.91/20.13 Huet Levy Procedure: 29.91/20.13 -> Rules: 29.91/20.13 add(0,y) -> y 29.91/20.13 add(s(x),y) -> s(add(x,y)) 29.91/20.13 gcd(add(x,y),y) -> gcd(x,y) 29.91/20.13 gcd(0,x) -> x 29.91/20.13 gcd(x,0) -> x 29.91/20.13 gcd(y,add(x,y)) -> gcd(x,y) 29.91/20.13 -> Vars: 29.91/20.13 y, x, y, x, y, x, x, x, y 29.91/20.13 29.91/20.13 -> Rlps: 29.91/20.13 (rule: add(0,y) -> y, id: 1, possubterms: add(0,y)->[], 0->[1]) 29.91/20.13 (rule: add(s(x),y) -> s(add(x,y)), id: 2, possubterms: add(s(x),y)->[], s(x)->[1]) 29.91/20.13 (rule: gcd(add(x,y),y) -> gcd(x,y), id: 3, possubterms: gcd(add(x,y),y)->[], add(x,y)->[1]) 29.91/20.13 (rule: gcd(0,x) -> x, id: 4, possubterms: gcd(0,x)->[], 0->[1]) 29.91/20.13 (rule: gcd(x,0) -> x, id: 5, possubterms: gcd(x,0)->[], 0->[2]) 29.91/20.13 (rule: gcd(y,add(x,y)) -> gcd(x,y), id: 6, possubterms: gcd(y,add(x,y))->[], add(x,y)->[2]) 29.91/20.13 29.91/20.13 -> Unifications: 29.91/20.13 (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') 29.91/20.13 (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'))) 29.91/20.13 (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)) 29.91/20.13 (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') 29.91/20.13 (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') 29.91/20.13 (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') 29.91/20.13 (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'))) 29.91/20.13 29.91/20.13 -> Critical pairs info: 29.91/20.13 => Not trivial, Overlay, Proper, NW0, N1 29.91/20.13 => Not trivial, Not overlay, Proper, NW0, N2 29.91/20.13 => Not trivial, Overlay, Proper, NW0, N3 29.91/20.13 => Not trivial, Not overlay, Proper, NW0, N4 29.91/20.13 => Not trivial, Not overlay, Proper, NW0, N5 29.91/20.13 <0,0> => Trivial, Overlay, Proper, NW0, N6 29.91/20.13 => Not trivial, Not overlay, Proper, NW0, N7 29.91/20.13 29.91/20.13 -> Problem conclusions: 29.91/20.13 Not left linear, Right linear, Not linear 29.91/20.13 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 29.91/20.13 Not Huet-Levy confluent, Not Newman confluent 29.91/20.13 R is a TRS 29.91/20.13 29.91/20.13 29.91/20.13 Problem 1: 29.91/20.13 No Convergence Brute Force Procedure: 29.91/20.13 -> Rewritings: 29.91/20.13 s: add(x,0) 29.91/20.13 Nodes: [0] 29.91/20.13 Edges: [] 29.91/20.13 ID: 0 => ('add(x,0)', D0) 29.91/20.13 t: gcd(x,0) 29.91/20.13 Nodes: [0,1] 29.91/20.13 Edges: [(0,1)] 29.91/20.13 ID: 0 => ('gcd(x,0)', D0) 29.91/20.13 ID: 1 => ('x', D1, R5, P[], S{x12 -> x}), NR: 'x' 29.91/20.13 add(x,0) ->* no union *<- gcd(x,0) 29.91/20.13 "Not joinable" 29.91/20.13 29.91/20.13 The problem is not confluent. 29.91/20.13 EOF