45.027/45.027 NO 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 45.027/45.027 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 Confluence Problem: 45.027/45.027 (VAR vNonEmpty:S x:S y:S) 45.027/45.027 (STRATEGY CONTEXTSENSITIVE 45.027/45.027 (add 1 2) 45.027/45.027 (gcd 1 2) 45.027/45.027 (0) 45.027/45.027 (fSNonEmpty) 45.027/45.027 (false) 45.027/45.027 (leq 1 2) 45.027/45.027 (s 1) 45.027/45.027 ) 45.027/45.027 (RULES 45.027/45.027 add(0,y:S) -> y:S 45.027/45.027 add(s(x:S),y:S) -> s(add(x:S,y:S)) 45.027/45.027 gcd(add(x:S,y:S),y:S) -> gcd(x:S,y:S) 45.027/45.027 gcd(0,x:S) -> x:S 45.027/45.027 gcd(x:S,0) -> x:S 45.027/45.027 gcd(x:S,y:S) -> gcd(y:S,x:S) | leq(y:S,x:S) ->* false 45.027/45.027 gcd(y:S,add(x:S,y:S)) -> gcd(x:S,y:S) 45.027/45.027 ) 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 45.027/45.027 Inlining of Conditions Processor [STERN17]: 45.027/45.027 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 Confluence Problem: 45.027/45.027 (VAR vNonEmpty:S x:S y:S) 45.027/45.027 (STRATEGY CONTEXTSENSITIVE 45.027/45.027 (add 1 2) 45.027/45.027 (gcd 1 2) 45.027/45.027 (0) 45.027/45.027 (fSNonEmpty) 45.027/45.027 (false) 45.027/45.027 (leq 1 2) 45.027/45.027 (s 1) 45.027/45.027 ) 45.027/45.027 (RULES 45.027/45.027 add(0,y:S) -> y:S 45.027/45.027 add(s(x:S),y:S) -> s(add(x:S,y:S)) 45.027/45.027 gcd(add(x:S,y:S),y:S) -> gcd(x:S,y:S) 45.027/45.027 gcd(0,x:S) -> x:S 45.027/45.027 gcd(x:S,0) -> x:S 45.027/45.027 gcd(x:S,y:S) -> gcd(y:S,x:S) | leq(y:S,x:S) ->* false 45.027/45.027 gcd(y:S,add(x:S,y:S)) -> gcd(x:S,y:S) 45.027/45.027 ) 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 45.027/45.027 Clean CTRS Processor: 45.027/45.027 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 Confluence Problem: 45.027/45.027 (VAR x:S y:S) 45.027/45.027 (STRATEGY CONTEXTSENSITIVE 45.027/45.027 (add 1 2) 45.027/45.027 (gcd 1 2) 45.027/45.027 (0) 45.027/45.027 (fSNonEmpty) 45.027/45.027 (false) 45.027/45.027 (leq 1 2) 45.027/45.027 (s 1) 45.027/45.027 ) 45.027/45.027 (RULES 45.027/45.027 add(0,y:S) -> y:S 45.027/45.027 add(s(x:S),y:S) -> s(add(x:S,y:S)) 45.027/45.027 gcd(add(x:S,y:S),y:S) -> gcd(x:S,y:S) 45.027/45.027 gcd(0,x:S) -> x:S 45.027/45.027 gcd(x:S,0) -> x:S 45.027/45.027 gcd(y:S,add(x:S,y:S)) -> gcd(x:S,y:S) 45.027/45.027 ) 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 45.027/45.027 CRule InfChecker Info: 45.027/45.027 add(0,y:S) -> y:S 45.027/45.027 Rule remains 45.027/45.027 Proof: 45.027/45.027 NO_CONDS 45.027/45.027 45.027/45.027 CRule InfChecker Info: 45.027/45.027 add(s(x:S),y:S) -> s(add(x:S,y:S)) 45.027/45.027 Rule remains 45.027/45.027 Proof: 45.027/45.027 NO_CONDS 45.027/45.027 45.027/45.027 CRule InfChecker Info: 45.027/45.027 gcd(add(x:S,y:S),y:S) -> gcd(x:S,y:S) 45.027/45.027 Rule remains 45.027/45.027 Proof: 45.027/45.027 NO_CONDS 45.027/45.027 45.027/45.027 CRule InfChecker Info: 45.027/45.027 gcd(0,x:S) -> x:S 45.027/45.027 Rule remains 45.027/45.027 Proof: 45.027/45.027 NO_CONDS 45.027/45.027 45.027/45.027 CRule InfChecker Info: 45.027/45.027 gcd(x:S,0) -> x:S 45.027/45.027 Rule remains 45.027/45.027 Proof: 45.027/45.027 NO_CONDS 45.027/45.027 45.027/45.027 CRule InfChecker Info: 45.027/45.027 gcd(x:S,y:S) -> gcd(y:S,x:S) | leq(y:S,x:S) ->* false 45.027/45.027 Rule deleted 45.027/45.027 Proof: 45.027/45.027 YES 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 45.027/45.027 Infeasibility Problem: 45.027/45.027 [(VAR vNonEmpty:S vNonEmpty:S:S x:S:S y:S:S) 45.027/45.027 (STRATEGY CONTEXTSENSITIVE 45.027/45.027 (add 1 2) 45.027/45.027 (gcd 1 2) 45.027/45.027 (0) 45.027/45.027 (fSNonEmpty) 45.027/45.027 (false) 45.027/45.027 (leq 1 2) 45.027/45.027 (s 1) 45.027/45.027 ) 45.027/45.027 (RULES 45.027/45.027 add(0,y:S:S) -> y:S:S 45.027/45.027 add(s(x:S:S),y:S:S) -> s(add(x:S:S,y:S:S)) 45.027/45.027 gcd(add(x:S:S,y:S:S),y:S:S) -> gcd(x:S:S,y:S:S) 45.027/45.027 gcd(0,x:S:S) -> x:S:S 45.027/45.027 gcd(x:S:S,0) -> x:S:S 45.027/45.027 gcd(x:S:S,y:S:S) -> gcd(y:S:S,x:S:S) | leq(y:S:S,x:S:S) ->* false 45.027/45.027 gcd(y:S:S,add(x:S:S,y:S:S)) -> gcd(x:S:S,y:S:S) 45.027/45.027 )] 45.027/45.027 45.027/45.027 Infeasibility Conditions: 45.027/45.027 leq(y:S:S,x:S:S) ->* false 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 45.027/45.027 Obtaining a model using Mace4: 45.027/45.027 45.027/45.027 -> Usable Rules: 45.027/45.027 add(0,y:S:S) -> y:S:S 45.027/45.027 add(s(x:S:S),y:S:S) -> s(add(x:S:S,y:S:S)) 45.027/45.027 gcd(add(x:S:S,y:S:S),y:S:S) -> gcd(x:S:S,y:S:S) 45.027/45.027 gcd(0,x:S:S) -> x:S:S 45.027/45.027 gcd(x:S:S,0) -> x:S:S 45.027/45.027 gcd(x:S:S,y:S:S) -> gcd(y:S:S,x:S:S) | leq(y:S:S,x:S:S) ->* false 45.027/45.027 gcd(y:S:S,add(x:S:S,y:S:S)) -> gcd(x:S:S,y:S:S) 45.027/45.027 45.027/45.027 -> Mace4 Output: 45.027/45.027 ============================== Mace4 ================================= 45.027/45.027 Mace4 (64) version 2009-11A, November 2009. 45.027/45.027 Process 39078 was started by ubuntu on ubuntu, 45.027/45.027 Wed Jul 14 10:10:20 2021 45.027/45.027 The command was "./mace4 -c -f /tmp/mace439065-2.in". 45.027/45.027 ============================== end of head =========================== 45.027/45.027 45.027/45.027 ============================== INPUT ================================= 45.027/45.027 45.027/45.027 % Reading from file /tmp/mace439065-2.in 45.027/45.027 45.027/45.027 assign(max_seconds,20). 45.027/45.027 45.027/45.027 formulas(assumptions). 45.027/45.027 ->(x1,y) -> ->(add(x1,x2),add(y,x2)) # label(congruence). 45.027/45.027 ->(x2,y) -> ->(add(x1,x2),add(x1,y)) # label(congruence). 45.027/45.027 ->(x1,y) -> ->(gcd(x1,x2),gcd(y,x2)) # label(congruence). 45.027/45.027 ->(x2,y) -> ->(gcd(x1,x2),gcd(x1,y)) # label(congruence). 45.027/45.027 ->(x1,y) -> ->(leq(x1,x2),leq(y,x2)) # label(congruence). 45.027/45.027 ->(x2,y) -> ->(leq(x1,x2),leq(x1,y)) # label(congruence). 45.027/45.027 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 45.027/45.027 ->(add(0,x3),x3) # label(replacement). 45.027/45.027 ->(add(s(x2),x3),s(add(x2,x3))) # label(replacement). 45.027/45.027 ->(gcd(add(x2,x3),x3),gcd(x2,x3)) # label(replacement). 45.027/45.027 ->(gcd(0,x2),x2) # label(replacement). 45.027/45.027 ->(gcd(x2,0),x2) # label(replacement). 45.027/45.027 ->*(leq(x3,x2),false) -> ->(gcd(x2,x3),gcd(x3,x2)) # label(replacement). 45.027/45.027 ->(gcd(x3,add(x2,x3)),gcd(x2,x3)) # label(replacement). 45.027/45.027 ->*(x,x) # label(reflexivity). 45.027/45.027 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 45.027/45.027 end_of_list. 45.027/45.027 45.027/45.027 formulas(goals). 45.027/45.027 (exists x2 exists x3 ->*(leq(x3,x2),false)) # label(goal). 45.027/45.027 end_of_list. 45.027/45.027 45.027/45.027 ============================== end of input ========================== 45.027/45.027 45.027/45.027 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 45.027/45.027 45.027/45.027 % Formulas that are not ordinary clauses: 45.027/45.027 1 ->(x1,y) -> ->(add(x1,x2),add(y,x2)) # label(congruence) # label(non_clause). [assumption]. 45.027/45.027 2 ->(x2,y) -> ->(add(x1,x2),add(x1,y)) # label(congruence) # label(non_clause). [assumption]. 45.027/45.027 3 ->(x1,y) -> ->(gcd(x1,x2),gcd(y,x2)) # label(congruence) # label(non_clause). [assumption]. 45.027/45.027 4 ->(x2,y) -> ->(gcd(x1,x2),gcd(x1,y)) # label(congruence) # label(non_clause). [assumption]. 45.027/45.027 5 ->(x1,y) -> ->(leq(x1,x2),leq(y,x2)) # label(congruence) # label(non_clause). [assumption]. 45.027/45.027 6 ->(x2,y) -> ->(leq(x1,x2),leq(x1,y)) # label(congruence) # label(non_clause). [assumption]. 45.027/45.027 7 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 45.027/45.027 8 ->*(leq(x3,x2),false) -> ->(gcd(x2,x3),gcd(x3,x2)) # label(replacement) # label(non_clause). [assumption]. 45.027/45.027 9 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 45.027/45.027 10 (exists x2 exists x3 ->*(leq(x3,x2),false)) # label(goal) # label(non_clause) # label(goal). [goal]. 45.027/45.027 45.027/45.027 ============================== end of process non-clausal formulas === 45.027/45.027 45.027/45.027 ============================== CLAUSES FOR SEARCH ==================== 45.027/45.027 45.027/45.027 formulas(mace4_clauses). 45.027/45.027 -->(x,y) | ->(add(x,z),add(y,z)) # label(congruence). 45.027/45.027 -->(x,y) | ->(add(z,x),add(z,y)) # label(congruence). 45.027/45.027 -->(x,y) | ->(gcd(x,z),gcd(y,z)) # label(congruence). 45.027/45.027 -->(x,y) | ->(gcd(z,x),gcd(z,y)) # label(congruence). 45.027/45.027 -->(x,y) | ->(leq(x,z),leq(y,z)) # label(congruence). 45.027/45.027 -->(x,y) | ->(leq(z,x),leq(z,y)) # label(congruence). 45.027/45.027 -->(x,y) | ->(s(x),s(y)) # label(congruence). 45.027/45.027 ->(add(0,x),x) # label(replacement). 45.027/45.027 ->(add(s(x),y),s(add(x,y))) # label(replacement). 45.027/45.027 ->(gcd(add(x,y),y),gcd(x,y)) # label(replacement). 45.027/45.027 ->(gcd(0,x),x) # label(replacement). 45.027/45.027 ->(gcd(x,0),x) # label(replacement). 45.027/45.027 -->*(leq(x,y),false) | ->(gcd(y,x),gcd(x,y)) # label(replacement). 45.027/45.027 ->(gcd(x,add(y,x)),gcd(y,x)) # label(replacement). 45.027/45.027 ->*(x,x) # label(reflexivity). 45.027/45.027 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 45.027/45.027 -->*(leq(x,y),false) # label(goal). 45.027/45.027 end_of_list. 45.027/45.027 45.027/45.027 ============================== end of clauses for search ============= 45.027/45.027 45.027/45.027 % There are no natural numbers in the input. 45.027/45.027 45.027/45.027 ============================== DOMAIN SIZE 2 ========================= 45.027/45.027 45.027/45.027 ============================== MODEL ================================= 45.027/45.027 45.027/45.027 interpretation( 2, [number=1, seconds=0], [ 45.027/45.027 45.027/45.027 function(0, [ 0 ]), 45.027/45.027 45.027/45.027 function(false, [ 0 ]), 45.027/45.027 45.027/45.027 function(s(_), [ 0, 0 ]), 45.027/45.027 45.027/45.027 function(add(_,_), [ 45.027/45.027 0, 0, 45.027/45.027 0, 0 ]), 45.027/45.027 45.027/45.027 function(gcd(_,_), [ 45.027/45.027 0, 0, 45.027/45.027 0, 0 ]), 45.027/45.027 45.027/45.027 function(leq(_,_), [ 45.027/45.027 1, 1, 45.027/45.027 1, 1 ]), 45.027/45.027 45.027/45.027 relation(->*(_,_), [ 45.027/45.027 1, 1, 45.027/45.027 0, 1 ]), 45.027/45.027 45.027/45.027 relation(->(_,_), [ 45.027/45.027 1, 1, 45.027/45.027 0, 1 ]) 45.027/45.027 ]). 45.027/45.027 45.027/45.027 ============================== end of model ========================== 45.027/45.027 45.027/45.027 ============================== STATISTICS ============================ 45.027/45.027 45.027/45.027 For domain size 2. 45.027/45.027 45.027/45.027 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 45.027/45.027 Ground clauses: seen=88, kept=84. 45.027/45.027 Selections=9, assignments=9, propagations=15, current_models=1. 45.027/45.027 Rewrite_terms=180, rewrite_bools=119, indexes=18. 45.027/45.027 Rules_from_neg_clauses=7, cross_offs=7. 45.027/45.027 45.027/45.027 ============================== end of statistics ===================== 45.027/45.027 45.027/45.027 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 45.027/45.027 45.027/45.027 Exiting with 1 model. 45.027/45.027 45.027/45.027 Process 39078 exit (max_models) Wed Jul 14 10:10:20 2021 45.027/45.027 The process finished Wed Jul 14 10:10:20 2021 45.027/45.027 45.027/45.027 45.027/45.027 Mace4 cooked interpretation: 45.027/45.027 45.027/45.027 45.027/45.027 45.027/45.027 The problem is infeasible. 45.027/45.027 45.027/45.027 45.027/45.027 CRule InfChecker Info: 45.027/45.027 gcd(y:S,add(x:S,y:S)) -> gcd(x:S,y:S) 45.027/45.027 Rule remains 45.027/45.027 Proof: 45.027/45.027 NO_CONDS 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 Confluence Problem: 45.027/45.027 (VAR x:S y:S) 45.027/45.027 (STRATEGY CONTEXTSENSITIVE 45.027/45.027 (add 1 2) 45.027/45.027 (gcd 1 2) 45.027/45.027 (0) 45.027/45.027 (fSNonEmpty) 45.027/45.027 (false) 45.027/45.027 (leq 1 2) 45.027/45.027 (s 1) 45.027/45.027 ) 45.027/45.027 (RULES 45.027/45.027 add(0,y:S) -> y:S 45.027/45.027 add(s(x:S),y:S) -> s(add(x:S,y:S)) 45.027/45.027 gcd(add(x:S,y:S),y:S) -> gcd(x:S,y:S) 45.027/45.027 gcd(0,x:S) -> x:S 45.027/45.027 gcd(x:S,0) -> x:S 45.027/45.027 gcd(y:S,add(x:S,y:S)) -> gcd(x:S,y:S) 45.027/45.027 ) 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 45.027/45.027 Critical Pairs Processor: 45.027/45.027 -> Rules: 45.027/45.027 add(0,y:S) -> y:S 45.027/45.027 add(s(x:S),y:S) -> s(add(x:S,y:S)) 45.027/45.027 gcd(add(x:S,y:S),y:S) -> gcd(x:S,y:S) 45.027/45.027 gcd(0,x:S) -> x:S 45.027/45.027 gcd(x:S,0) -> x:S 45.027/45.027 gcd(y:S,add(x:S,y:S)) -> gcd(x:S,y:S) 45.027/45.027 -> Vars: 45.027/45.027 "y", "x", "y", "x", "y", "x", "x", "x", "y" 45.027/45.027 -> FVars: 45.027/45.027 "x3", "x4", "x5", "x6", "x7", "x8", "x9", "x10", "x11" 45.027/45.027 -> PVars: 45.027/45.027 "y": ["x3", "x5", "x7", "x11"], "x": ["x4", "x6", "x8", "x9", "x10"] 45.027/45.027 45.027/45.027 -> Rlps: 45.027/45.027 crule: add(0,x3:S) -> x3:S, id: 1, possubterms: add(0,x3:S)-> [], 0-> [1] 45.027/45.027 crule: 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] 45.027/45.027 crule: 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] 45.027/45.027 crule: gcd(0,x8:S) -> x8:S, id: 4, possubterms: gcd(0,x8:S)-> [], 0-> [1] 45.027/45.027 crule: gcd(x9:S,0) -> x9:S, id: 5, possubterms: gcd(x9:S,0)-> [], 0-> [2] 45.027/45.027 crule: 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] 45.027/45.027 45.027/45.027 -> Unifications: 45.027/45.027 R3 unifies with R1 at p: [1], l: gcd(add(x6:S,x7:S),x7:S), lp: add(x6:S,x7:S), conds: {}, sig: {x6:S -> 0,x7:S -> y:S}, l': add(0,y:S), r: gcd(x6:S,x7:S), r': y:S 45.027/45.027 R3 unifies with R2 at p: [1], l: gcd(add(x6:S,x7:S),x7:S), lp: add(x6:S,x7:S), conds: {}, 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)) 45.027/45.027 R5 unifies with R3 at p: [], l: gcd(x9:S,0), lp: gcd(x9:S,0), conds: {}, 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) 45.027/45.027 R5 unifies with R4 at p: [], l: gcd(x9:S,0), lp: gcd(x9:S,0), conds: {}, sig: {x:S -> 0,x9:S -> 0}, l': gcd(0,x:S), r: x9:S, r': x:S 45.027/45.027 R6 unifies with R4 at p: [], l: gcd(x11:S,add(x10:S,x11:S)), lp: gcd(x11:S,add(x10:S,x11:S)), conds: {}, sig: {x:S -> add(x10:S,0),x11:S -> 0}, l': gcd(0,x:S), r: gcd(x10:S,x11:S), r': x:S 45.027/45.027 R6 unifies with R1 at p: [2], l: gcd(x11:S,add(x10:S,x11:S)), lp: add(x10:S,x11:S), conds: {}, sig: {x10:S -> 0,x11:S -> y:S}, l': add(0,y:S), r: gcd(x10:S,x11:S), r': y:S 45.027/45.027 R6 unifies with R2 at p: [2], l: gcd(x11:S,add(x10:S,x11:S)), lp: add(x10:S,x11:S), conds: {}, 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)) 45.027/45.027 45.027/45.027 -> Critical pairs info: 45.027/45.027 <0,0> => Trivial, Overlay, N1 45.027/45.027 => Not trivial, Not overlay, N2 45.027/45.027 => Not trivial, Overlay, N3 45.027/45.027 => Not trivial, Overlay, N4 45.027/45.027 => Not trivial, Not overlay, N5 45.027/45.027 => Not trivial, Not overlay, N6 45.027/45.027 45.027/45.027 -> Problem conclusions: 45.027/45.027 Not left linear, Right linear, Not linear 45.027/45.027 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 45.027/45.027 CTRS Type: 1 45.027/45.027 Deterministic, Strongly deterministic 45.027/45.027 Oriented CTRS, Properly oriented CTRS, Join CTRS 45.027/45.027 Maybe right-stable CTRS, Not overlay CTRS 45.027/45.027 Normal CTRS, Almost normal CTRS 45.027/45.027 Maybe terminating CTRS, Maybe joinable CCPs 45.027/45.027 Maybe level confluent 45.027/45.027 Maybe confluent 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 Confluence Problem: 45.027/45.027 (VAR x:S y:S) 45.027/45.027 (STRATEGY CONTEXTSENSITIVE 45.027/45.027 (add 1 2) 45.027/45.027 (gcd 1 2) 45.027/45.027 (0) 45.027/45.027 (fSNonEmpty) 45.027/45.027 (false) 45.027/45.027 (leq 1 2) 45.027/45.027 (s 1) 45.027/45.027 ) 45.027/45.027 (RULES 45.027/45.027 add(0,y:S) -> y:S 45.027/45.027 add(s(x:S),y:S) -> s(add(x:S,y:S)) 45.027/45.027 gcd(add(x:S,y:S),y:S) -> gcd(x:S,y:S) 45.027/45.027 gcd(0,x:S) -> x:S 45.027/45.027 gcd(x:S,0) -> x:S 45.027/45.027 gcd(y:S,add(x:S,y:S)) -> gcd(x:S,y:S) 45.027/45.027 ) 45.027/45.027 Critical Pairs: 45.027/45.027 => Not trivial, Not overlay, N2 45.027/45.027 => Not trivial, Overlay, N3 45.027/45.027 => Not trivial, Overlay, N4 45.027/45.027 => Not trivial, Not overlay, N5 45.027/45.027 => Not trivial, Not overlay, N6 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 45.027/45.027 Conditional Critical Pairs Distributor Processor 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 Confluence Problem: 45.027/45.027 (VAR x:S y:S) 45.027/45.027 (STRATEGY CONTEXTSENSITIVE 45.027/45.027 (add 1 2) 45.027/45.027 (gcd 1 2) 45.027/45.027 (0) 45.027/45.027 (fSNonEmpty) 45.027/45.027 (false) 45.027/45.027 (leq 1 2) 45.027/45.027 (s 1) 45.027/45.027 ) 45.027/45.027 (RULES 45.027/45.027 add(0,y:S) -> y:S 45.027/45.027 add(s(x:S),y:S) -> s(add(x:S,y:S)) 45.027/45.027 gcd(add(x:S,y:S),y:S) -> gcd(x:S,y:S) 45.027/45.027 gcd(0,x:S) -> x:S 45.027/45.027 gcd(x:S,0) -> x:S 45.027/45.027 gcd(y:S,add(x:S,y:S)) -> gcd(x:S,y:S) 45.027/45.027 ) 45.027/45.027 Critical Pairs: 45.027/45.027 => Not trivial, Not overlay, N2 45.027/45.027 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 45.027/45.027 45.027/45.027 Infeasible Convergence No Conditions CCP Processor: 45.027/45.027 Infeasible convergence? 45.027/45.027 YES 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 45.027/45.027 Infeasibility Problem: 45.027/45.027 [(VAR vNonEmpty:S x:S y:S z:S) 45.027/45.027 (STRATEGY CONTEXTSENSITIVE 45.027/45.027 (add 1 2) 45.027/45.027 (gcd 1 2) 45.027/45.027 (0) 45.027/45.027 (cy) 45.027/45.027 (fSNonEmpty) 45.027/45.027 (s 1) 45.027/45.027 ) 45.027/45.027 (RULES 45.027/45.027 add(0,y:S) -> y:S 45.027/45.027 add(s(x:S),y:S) -> s(add(x:S,y:S)) 45.027/45.027 gcd(add(x:S,y:S),y:S) -> gcd(x:S,y:S) 45.027/45.027 gcd(0,x:S) -> x:S 45.027/45.027 gcd(x:S,0) -> x:S 45.027/45.027 gcd(y:S,add(x:S,y:S)) -> gcd(x:S,y:S) 45.027/45.027 )] 45.027/45.027 Infeasibility Conditions: 45.027/45.027 gcd(cy,cy) ->* z:S, gcd(0,cy) ->* z:S 45.027/45.027 45.027/45.027 Problem 1: 45.027/45.027 45.027/45.027 Obtaining a model using Mace4: 45.027/45.027 45.027/45.027 -> Usable Rules: 45.027/45.027 gcd(add(x:S,y:S),y:S) -> gcd(x:S,y:S) 45.027/45.027 gcd(0,x:S) -> x:S 45.027/45.027 gcd(x:S,0) -> x:S 45.027/45.027 gcd(y:S,add(x:S,y:S)) -> gcd(x:S,y:S) 45.027/45.027 45.027/45.027 -> Mace4 Output: 45.027/45.027 ============================== Mace4 ================================= 45.027/45.027 Mace4 (64) version 2009-11A, November 2009. 45.027/45.027 Process 39112 was started by ubuntu on ubuntu, 45.027/45.027 Wed Jul 14 10:10:40 2021 45.027/45.027 The command was "./mace4 -c -f /tmp/mace439099-2.in". 45.027/45.027 ============================== end of head =========================== 45.027/45.027 45.027/45.027 ============================== INPUT ================================= 45.027/45.027 45.027/45.027 % Reading from file /tmp/mace439099-2.in 45.027/45.027 45.027/45.027 assign(max_seconds,20). 45.027/45.027 45.027/45.027 formulas(assumptions). 45.027/45.027 ->(x1,y) -> ->(add(x1,x2),add(y,x2)) # label(congruence). 45.027/45.027 ->(x2,y) -> ->(add(x1,x2),add(x1,y)) # label(congruence). 45.027/45.027 ->(x1,y) -> ->(gcd(x1,x2),gcd(y,x2)) # label(congruence). 45.027/45.027 ->(x2,y) -> ->(gcd(x1,x2),gcd(x1,y)) # label(congruence). 45.027/45.027 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 45.027/45.027 ->(gcd(add(x1,x2),x2),gcd(x1,x2)) # label(replacement). 45.027/45.027 ->(gcd(0,x1),x1) # label(replacement). 45.027/45.027 ->(gcd(x1,0),x1) # label(replacement). 45.027/45.027 ->(gcd(x2,add(x1,x2)),gcd(x1,x2)) # label(replacement). 45.027/45.027 ->*(x,x) # label(reflexivity). 45.027/45.027 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 45.027/45.027 end_of_list. 45.027/45.027 45.027/45.027 formulas(goals). 45.027/45.027 (exists x3 (->*(gcd(cy,cy),x3) & ->*(gcd(0,cy),x3))) # label(goal). 45.027/45.027 end_of_list. 45.027/45.027 45.027/45.027 ============================== end of input ========================== 45.027/45.027 45.027/45.027 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 45.027/45.027 45.027/45.027 % Formulas that are not ordinary clauses: 45.027/45.027 1 ->(x1,y) -> ->(add(x1,x2),add(y,x2)) # label(congruence) # label(non_clause). [assumption]. 45.027/45.027 2 ->(x2,y) -> ->(add(x1,x2),add(x1,y)) # label(congruence) # label(non_clause). [assumption]. 45.027/45.027 3 ->(x1,y) -> ->(gcd(x1,x2),gcd(y,x2)) # label(congruence) # label(non_clause). [assumption]. 45.027/45.027 4 ->(x2,y) -> ->(gcd(x1,x2),gcd(x1,y)) # label(congruence) # label(non_clause). [assumption]. 45.027/45.027 5 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 45.027/45.027 6 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 45.027/45.027 7 (exists x3 (->*(gcd(cy,cy),x3) & ->*(gcd(0,cy),x3))) # label(goal) # label(non_clause) # label(goal). [goal]. 45.027/45.027 45.027/45.027 ============================== end of process non-clausal formulas === 45.027/45.027 45.027/45.027 ============================== CLAUSES FOR SEARCH ==================== 45.027/45.027 45.027/45.027 formulas(mace4_clauses). 45.027/45.027 -->(x,y) | ->(add(x,z),add(y,z)) # label(congruence). 45.027/45.027 -->(x,y) | ->(add(z,x),add(z,y)) # label(congruence). 45.027/45.027 -->(x,y) | ->(gcd(x,z),gcd(y,z)) # label(congruence). 45.027/45.027 -->(x,y) | ->(gcd(z,x),gcd(z,y)) # label(congruence). 45.027/45.027 -->(x,y) | ->(s(x),s(y)) # label(congruence). 45.027/45.027 ->(gcd(add(x,y),y),gcd(x,y)) # label(replacement). 45.027/45.027 ->(gcd(0,x),x) # label(replacement). 45.027/45.027 ->(gcd(x,0),x) # label(replacement). 45.027/45.027 ->(gcd(x,add(y,x)),gcd(y,x)) # label(replacement). 45.027/45.027 ->*(x,x) # label(reflexivity). 45.027/45.027 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 45.027/45.027 -->*(gcd(cy,cy),x) | -->*(gcd(0,cy),x) # label(goal). 45.027/45.027 end_of_list. 45.027/45.027 45.027/45.027 ============================== end of clauses for search ============= 45.027/45.027 45.027/45.027 % There are no natural numbers in the input. 45.027/45.027 45.027/45.027 ============================== DOMAIN SIZE 2 ========================= 45.027/45.027 45.027/45.027 ============================== MODEL ================================= 45.027/45.027 45.027/45.027 interpretation( 2, [number=1, seconds=0], [ 45.027/45.027 45.027/45.027 function(0, [ 0 ]), 45.027/45.027 45.027/45.027 function(cy, [ 1 ]), 45.027/45.027 45.027/45.027 function(s(_), [ 0, 0 ]), 45.027/45.027 45.027/45.027 function(add(_,_), [ 45.027/45.027 0, 0, 45.027/45.027 1, 1 ]), 45.027/45.027 45.027/45.027 function(gcd(_,_), [ 45.027/45.027 0, 1, 45.027/45.027 1, 0 ]), 45.027/45.027 45.027/45.027 relation(->*(_,_), [ 45.027/45.027 1, 0, 45.027/45.027 0, 1 ]), 45.027/45.027 45.027/45.027 relation(->(_,_), [ 45.027/45.027 1, 0, 45.027/45.027 0, 1 ]) 45.027/45.027 ]). 45.027/45.027 45.027/45.027 ============================== end of model ========================== 45.027/45.027 45.027/45.027 ============================== STATISTICS ============================ 45.027/45.027 45.027/45.027 For domain size 2. 45.027/45.027 45.027/45.027 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 45.027/45.027 Ground clauses: seen=60, kept=56. 45.027/45.027 Selections=21, assignments=36, propagations=43, current_models=1. 45.027/45.027 Rewrite_terms=398, rewrite_bools=245, indexes=106. 45.027/45.027 Rules_from_neg_clauses=10, cross_offs=10. 45.027/45.027 45.027/45.027 ============================== end of statistics ===================== 45.027/45.027 45.027/45.027 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 45.027/45.027 45.027/45.027 Exiting with 1 model. 45.027/45.027 45.027/45.027 Process 39112 exit (max_models) Wed Jul 14 10:10:40 2021 45.027/45.027 The process finished Wed Jul 14 10:10:40 2021 45.027/45.027 45.027/45.027 45.027/45.027 Mace4 cooked interpretation: 45.027/45.027 45.027/45.027 45.027/45.027 45.027/45.027 The problem is infeasible. 45.027/45.027 45.027/45.027 45.027/45.027 The problem is not joinable. 45.027/45.027 38.06user 3.20system 0:45.27elapsed 91%CPU (0avgtext+0avgdata 62468maxresident)k 45.027/45.027 0inputs+0outputs (0major+60806minor)pagefaults 0swaps