40.013/40.013 YES 40.013/40.013 40.013/40.013 Problem 1: 40.013/40.013 40.013/40.013 40.013/40.013 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.013/40.013 Confluence Problem: 40.013/40.013 (VAR vNonEmpty:S n:S r:S x:S xs:S y:S q:S) 40.013/40.013 (STRATEGY CONTEXTSENSITIVE 40.013/40.013 (filter 1 2 3) 40.013/40.013 (cons 1 2) 40.013/40.013 (div 1 2) 40.013/40.013 (eq 1 2) 40.013/40.013 (fSNonEmpty) 40.013/40.013 (false) 40.013/40.013 (mo) 40.013/40.013 (nil) 40.013/40.013 (pair 1 2) 40.013/40.013 (true) 40.013/40.013 (ys) 40.013/40.013 ) 40.013/40.013 (RULES 40.013/40.013 filter(n:S,r:S,cons(x:S,xs:S)) -> pair(x:S,xs:S) | eq(div(x:S,n:S),pair(q:S,r:S)) ->* true 40.013/40.013 filter(n:S,r:S,cons(x:S,xs:S)) -> pair(y:S,cons(x:S,ys)) | filter(n:S,r:S,xs:S) ->* pair(y:S,ys), eq(div(x:S,n:S),pair(q:S,r:S)) ->* false 40.013/40.013 filter(n:S,r:S,nil) -> pair(mo,nil) 40.013/40.013 ) 40.013/40.013 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.013/40.013 40.013/40.013 40.013/40.013 Problem 1: 40.013/40.013 40.013/40.013 Inlining of Conditions Processor [STERN17]: 40.013/40.013 40.013/40.013 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.013/40.013 Confluence Problem: 40.013/40.013 (VAR vNonEmpty:S n:S r:S x:S xs:S y:S q:S) 40.013/40.013 (STRATEGY CONTEXTSENSITIVE 40.013/40.013 (filter 1 2 3) 40.013/40.013 (cons 1 2) 40.013/40.013 (div 1 2) 40.013/40.013 (eq 1 2) 40.013/40.013 (fSNonEmpty) 40.013/40.013 (false) 40.013/40.013 (mo) 40.013/40.013 (nil) 40.013/40.013 (pair 1 2) 40.013/40.013 (true) 40.013/40.013 (ys) 40.013/40.013 ) 40.013/40.013 (RULES 40.013/40.013 filter(n:S,r:S,cons(x:S,xs:S)) -> pair(x:S,xs:S) | eq(div(x:S,n:S),pair(q:S,r:S)) ->* true 40.013/40.013 filter(n:S,r:S,cons(x:S,xs:S)) -> pair(y:S,cons(x:S,ys)) | filter(n:S,r:S,xs:S) ->* pair(y:S,ys), eq(div(x:S,n:S),pair(q:S,r:S)) ->* false 40.013/40.013 filter(n:S,r:S,nil) -> pair(mo,nil) 40.013/40.013 ) 40.013/40.013 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.013/40.013 40.013/40.013 40.013/40.013 Problem 1: 40.013/40.013 40.013/40.013 Clean CTRS Processor: 40.013/40.013 40.013/40.013 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.013/40.013 Confluence Problem: 40.013/40.013 (VAR n:S r:S) 40.013/40.013 (STRATEGY CONTEXTSENSITIVE 40.013/40.013 (filter 1 2 3) 40.013/40.013 (cons 1 2) 40.013/40.013 (div 1 2) 40.013/40.013 (eq 1 2) 40.013/40.013 (fSNonEmpty) 40.013/40.013 (false) 40.013/40.013 (mo) 40.013/40.013 (nil) 40.013/40.013 (pair 1 2) 40.013/40.013 (true) 40.013/40.013 (ys) 40.013/40.013 ) 40.013/40.013 (RULES 40.013/40.013 filter(n:S,r:S,nil) -> pair(mo,nil) 40.013/40.013 ) 40.013/40.013 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.013/40.013 40.013/40.013 CRule InfChecker Info: 40.013/40.013 filter(n:S,r:S,cons(x:S,xs:S)) -> pair(x:S,xs:S) | eq(div(x:S,n:S),pair(q:S,r:S)) ->* true 40.013/40.013 Rule deleted 40.013/40.013 Proof: 40.013/40.013 YES 40.013/40.013 40.013/40.013 Problem 1: 40.013/40.013 40.013/40.013 Infeasibility Problem: 40.013/40.013 [(VAR vNonEmpty:S vNonEmpty:S:S n:S:S r:S:S x:S:S xs:S:S y:S:S q:S:S) 40.013/40.013 (STRATEGY CONTEXTSENSITIVE 40.013/40.013 (filter 1 2 3) 40.013/40.013 (cons 1 2) 40.013/40.013 (div 1 2) 40.013/40.013 (eq 1 2) 40.013/40.013 (fSNonEmpty) 40.013/40.013 (false) 40.013/40.013 (mo) 40.013/40.013 (nil) 40.013/40.013 (pair 1 2) 40.013/40.013 (true) 40.013/40.013 (ys) 40.013/40.013 ) 40.013/40.013 (RULES 40.013/40.013 filter(n:S:S,r:S:S,cons(x:S:S,xs:S:S)) -> pair(x:S:S,xs:S:S) | eq(div(x:S:S,n:S:S),pair(q:S:S,r:S:S)) ->* true 40.013/40.013 filter(n:S:S,r:S:S,cons(x:S:S,xs:S:S)) -> pair(y:S:S,cons(x:S:S,ys)) | filter(n:S:S,r:S:S,xs:S:S) ->* pair(y:S:S,ys), eq(div(x:S:S,n:S:S),pair(q:S:S,r:S:S)) ->* false 40.013/40.013 filter(n:S:S,r:S:S,nil) -> pair(mo,nil) 40.013/40.013 )] 40.013/40.013 40.013/40.013 Infeasibility Conditions: 40.013/40.013 eq(div(x:S:S,n:S:S),pair(q:S:S,r:S:S)) ->* true 40.013/40.013 40.013/40.013 Problem 1: 40.013/40.013 40.013/40.013 Obtaining a model using Mace4: 40.013/40.013 40.013/40.013 -> Usable Rules: 40.013/40.013 filter(n:S:S,r:S:S,cons(x:S:S,xs:S:S)) -> pair(x:S:S,xs:S:S) | eq(div(x:S:S,n:S:S),pair(q:S:S,r:S:S)) ->* true 40.013/40.013 filter(n:S:S,r:S:S,cons(x:S:S,xs:S:S)) -> pair(y:S:S,cons(x:S:S,ys)) | filter(n:S:S,r:S:S,xs:S:S) ->* pair(y:S:S,ys), eq(div(x:S:S,n:S:S),pair(q:S:S,r:S:S)) ->* false 40.013/40.013 filter(n:S:S,r:S:S,nil) -> pair(mo,nil) 40.013/40.013 40.013/40.013 -> Mace4 Output: 40.013/40.013 ============================== Mace4 ================================= 40.013/40.013 Mace4 (64) version 2009-11A, November 2009. 40.013/40.013 Process 105881 was started by ubuntu on ubuntu, 40.013/40.013 Fri Jul 16 14:52:36 2021 40.013/40.013 The command was "./mace4 -c -f /tmp/mace4105868-2.in". 40.013/40.013 ============================== end of head =========================== 40.013/40.013 40.013/40.013 ============================== INPUT ================================= 40.013/40.013 40.013/40.013 % Reading from file /tmp/mace4105868-2.in 40.013/40.013 40.013/40.013 assign(max_seconds,10). 40.013/40.013 40.013/40.013 formulas(assumptions). 40.013/40.013 ->(x1,y) -> ->(filter(x1,x2,x3),filter(y,x2,x3)) # label(congruence). 40.013/40.013 ->(x2,y) -> ->(filter(x1,x2,x3),filter(x1,y,x3)) # label(congruence). 40.013/40.013 ->(x3,y) -> ->(filter(x1,x2,x3),filter(x1,x2,y)) # label(congruence). 40.013/40.013 ->(x1,y) -> ->(cons(x1,x2),cons(y,x2)) # label(congruence). 40.013/40.013 ->(x2,y) -> ->(cons(x1,x2),cons(x1,y)) # label(congruence). 40.013/40.013 ->(x1,y) -> ->(div(x1,x2),div(y,x2)) # label(congruence). 40.013/40.013 ->(x2,y) -> ->(div(x1,x2),div(x1,y)) # label(congruence). 40.013/40.013 ->(x1,y) -> ->(eq(x1,x2),eq(y,x2)) # label(congruence). 40.013/40.013 ->(x2,y) -> ->(eq(x1,x2),eq(x1,y)) # label(congruence). 40.013/40.013 ->(x1,y) -> ->(pair(x1,x2),pair(y,x2)) # label(congruence). 40.013/40.013 ->(x2,y) -> ->(pair(x1,x2),pair(x1,y)) # label(congruence). 40.013/40.013 ->*(eq(div(x4,x2),pair(x7,x3)),true) -> ->(filter(x2,x3,cons(x4,x5)),pair(x4,x5)) # label(replacement). 40.013/40.013 ->*(filter(x2,x3,x5),pair(x6,ys)) & ->*(eq(div(x4,x2),pair(x7,x3)),false) -> ->(filter(x2,x3,cons(x4,x5)),pair(x6,cons(x4,ys))) # label(replacement). 40.013/40.013 ->(filter(x2,x3,nil),pair(mo,nil)) # label(replacement). 40.013/40.013 ->*(x,x) # label(reflexivity). 40.013/40.013 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 40.013/40.013 end_of_list. 40.013/40.013 40.013/40.013 formulas(goals). 40.013/40.013 (exists x2 exists x3 exists x4 exists x7 ->*(eq(div(x4,x2),pair(x7,x3)),true)) # label(goal). 40.013/40.013 end_of_list. 40.013/40.013 40.013/40.013 ============================== end of input ========================== 40.013/40.013 40.013/40.013 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 40.013/40.013 40.013/40.013 % Formulas that are not ordinary clauses: 40.013/40.013 1 ->(x1,y) -> ->(filter(x1,x2,x3),filter(y,x2,x3)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 2 ->(x2,y) -> ->(filter(x1,x2,x3),filter(x1,y,x3)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 3 ->(x3,y) -> ->(filter(x1,x2,x3),filter(x1,x2,y)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 4 ->(x1,y) -> ->(cons(x1,x2),cons(y,x2)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 5 ->(x2,y) -> ->(cons(x1,x2),cons(x1,y)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 6 ->(x1,y) -> ->(div(x1,x2),div(y,x2)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 7 ->(x2,y) -> ->(div(x1,x2),div(x1,y)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 8 ->(x1,y) -> ->(eq(x1,x2),eq(y,x2)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 9 ->(x2,y) -> ->(eq(x1,x2),eq(x1,y)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 10 ->(x1,y) -> ->(pair(x1,x2),pair(y,x2)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 11 ->(x2,y) -> ->(pair(x1,x2),pair(x1,y)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 12 ->*(eq(div(x4,x2),pair(x7,x3)),true) -> ->(filter(x2,x3,cons(x4,x5)),pair(x4,x5)) # label(replacement) # label(non_clause). [assumption]. 40.013/40.013 13 ->*(filter(x2,x3,x5),pair(x6,ys)) & ->*(eq(div(x4,x2),pair(x7,x3)),false) -> ->(filter(x2,x3,cons(x4,x5)),pair(x6,cons(x4,ys))) # label(replacement) # label(non_clause). [assumption]. 40.013/40.013 14 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 40.013/40.013 15 (exists x2 exists x3 exists x4 exists x7 ->*(eq(div(x4,x2),pair(x7,x3)),true)) # label(goal) # label(non_clause) # label(goal). [goal]. 40.013/40.013 40.013/40.013 ============================== end of process non-clausal formulas === 40.013/40.013 40.013/40.013 ============================== CLAUSES FOR SEARCH ==================== 40.013/40.013 40.013/40.013 formulas(mace4_clauses). 40.013/40.013 -->(x,y) | ->(filter(x,z,u),filter(y,z,u)) # label(congruence). 40.013/40.013 -->(x,y) | ->(filter(z,x,u),filter(z,y,u)) # label(congruence). 40.013/40.013 -->(x,y) | ->(filter(z,u,x),filter(z,u,y)) # label(congruence). 40.013/40.013 -->(x,y) | ->(cons(x,z),cons(y,z)) # label(congruence). 40.013/40.013 -->(x,y) | ->(cons(z,x),cons(z,y)) # label(congruence). 40.013/40.013 -->(x,y) | ->(div(x,z),div(y,z)) # label(congruence). 40.013/40.013 -->(x,y) | ->(div(z,x),div(z,y)) # label(congruence). 40.013/40.013 -->(x,y) | ->(eq(x,z),eq(y,z)) # label(congruence). 40.013/40.013 -->(x,y) | ->(eq(z,x),eq(z,y)) # label(congruence). 40.013/40.013 -->(x,y) | ->(pair(x,z),pair(y,z)) # label(congruence). 40.013/40.013 -->(x,y) | ->(pair(z,x),pair(z,y)) # label(congruence). 40.013/40.013 -->*(eq(div(x,y),pair(z,u)),true) | ->(filter(y,u,cons(x,w)),pair(x,w)) # label(replacement). 40.013/40.013 -->*(filter(x,y,z),pair(u,ys)) | -->*(eq(div(w,x),pair(v5,y)),false) | ->(filter(x,y,cons(w,z)),pair(u,cons(w,ys))) # label(replacement). 40.013/40.013 ->(filter(x,y,nil),pair(mo,nil)) # label(replacement). 40.013/40.013 ->*(x,x) # label(reflexivity). 40.013/40.013 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 40.013/40.013 -->*(eq(div(x,y),pair(z,u)),true) # label(goal). 40.013/40.013 end_of_list. 40.013/40.013 40.013/40.013 ============================== end of clauses for search ============= 40.013/40.013 40.013/40.013 % There are no natural numbers in the input. 40.013/40.013 40.013/40.013 ============================== DOMAIN SIZE 2 ========================= 40.013/40.013 40.013/40.013 ============================== MODEL ================================= 40.013/40.013 40.013/40.013 interpretation( 2, [number=1, seconds=0], [ 40.013/40.013 40.013/40.013 function(true, [ 0 ]), 40.013/40.013 40.013/40.013 function(ys, [ 0 ]), 40.013/40.013 40.013/40.013 function(false, [ 0 ]), 40.013/40.013 40.013/40.013 function(mo, [ 0 ]), 40.013/40.013 40.013/40.013 function(nil, [ 0 ]), 40.013/40.013 40.013/40.013 function(pair(_,_), [ 40.013/40.013 0, 0, 40.013/40.013 0, 0 ]), 40.013/40.013 40.013/40.013 function(cons(_,_), [ 40.013/40.013 0, 0, 40.013/40.013 0, 0 ]), 40.013/40.013 40.013/40.013 function(div(_,_), [ 40.013/40.013 0, 0, 40.013/40.013 0, 0 ]), 40.013/40.013 40.013/40.013 function(eq(_,_), [ 40.013/40.013 1, 0, 40.013/40.013 0, 0 ]), 40.013/40.013 40.013/40.013 function(filter(_,_,_), [ 40.013/40.013 0, 0, 40.013/40.013 0, 0, 40.013/40.013 0, 0, 40.013/40.013 0, 0 ]), 40.013/40.013 40.013/40.013 relation(->*(_,_), [ 40.013/40.013 1, 0, 40.013/40.013 0, 1 ]), 40.013/40.013 40.013/40.013 relation(->(_,_), [ 40.013/40.013 1, 0, 40.013/40.013 0, 1 ]) 40.013/40.013 ]). 40.013/40.013 40.013/40.013 ============================== end of model ========================== 40.013/40.013 40.013/40.013 ============================== STATISTICS ============================ 40.013/40.013 40.013/40.013 For domain size 2. 40.013/40.013 40.013/40.013 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 40.013/40.013 Ground clauses: seen=238, kept=234. 40.013/40.013 Selections=25, assignments=25, propagations=12, current_models=1. 40.013/40.013 Rewrite_terms=1300, rewrite_bools=303, indexes=204. 40.013/40.013 Rules_from_neg_clauses=5, cross_offs=5. 40.013/40.013 40.013/40.013 ============================== end of statistics ===================== 40.013/40.013 40.013/40.013 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 40.013/40.013 40.013/40.013 Exiting with 1 model. 40.013/40.013 40.013/40.013 Process 105881 exit (max_models) Fri Jul 16 14:52:36 2021 40.013/40.013 The process finished Fri Jul 16 14:52:36 2021 40.013/40.013 40.013/40.013 40.013/40.013 Mace4 cooked interpretation: 40.013/40.013 40.013/40.013 40.013/40.013 40.013/40.013 The problem is infeasible. 40.013/40.013 40.013/40.013 40.013/40.013 CRule InfChecker Info: 40.013/40.013 filter(n:S,r:S,cons(x:S,xs:S)) -> pair(y:S,cons(x:S,ys)) | filter(n:S,r:S,xs:S) ->* pair(y:S,ys), eq(div(x:S,n:S),pair(q:S,r:S)) ->* false 40.013/40.013 Rule deleted 40.013/40.013 Proof: 40.013/40.013 YES 40.013/40.013 40.013/40.013 Problem 1: 40.013/40.013 40.013/40.013 Infeasibility Problem: 40.013/40.013 [(VAR vNonEmpty:S n:S:S r:S:S x:S:S xs:S:S y:S:S q:S:S) 40.013/40.013 (STRATEGY CONTEXTSENSITIVE 40.013/40.013 (filter 1 2 3) 40.013/40.013 (cons 1 2) 40.013/40.013 (div 1 2) 40.013/40.013 (eq 1 2) 40.013/40.013 (fSNonEmpty) 40.013/40.013 (false) 40.013/40.013 (mo) 40.013/40.013 (nil) 40.013/40.013 (pair 1 2) 40.013/40.013 (ys) 40.013/40.013 ) 40.013/40.013 (RULES 40.013/40.013 filter(n:S:S,r:S:S,cons(x:S:S,xs:S:S)) -> pair(y:S:S,cons(x:S:S,ys)) | filter(n:S:S,r:S:S,xs:S:S) ->* pair(y:S:S,ys), eq(div(x:S:S,n:S:S),pair(q:S:S,r:S:S)) ->* false 40.013/40.013 filter(n:S:S,r:S:S,nil) -> pair(mo,nil) 40.013/40.013 )] 40.013/40.013 40.013/40.013 Infeasibility Conditions: 40.013/40.013 filter(n:S:S,r:S:S,xs:S:S) ->* pair(y:S:S,ys), eq(div(x:S:S,n:S:S),pair(q:S:S,r:S:S)) ->* false 40.013/40.013 40.013/40.013 Problem 1: 40.013/40.013 40.013/40.013 Obtaining a model using Mace4: 40.013/40.013 40.013/40.013 -> Usable Rules: 40.013/40.013 filter(n:S:S,r:S:S,cons(x:S:S,xs:S:S)) -> pair(y:S:S,cons(x:S:S,ys)) | filter(n:S:S,r:S:S,xs:S:S) ->* pair(y:S:S,ys), eq(div(x:S:S,n:S:S),pair(q:S:S,r:S:S)) ->* false 40.013/40.013 filter(n:S:S,r:S:S,nil) -> pair(mo,nil) 40.013/40.013 40.013/40.013 -> Mace4 Output: 40.013/40.013 ============================== Mace4 ================================= 40.013/40.013 Mace4 (64) version 2009-11A, November 2009. 40.013/40.013 Process 105907 was started by ubuntu on ubuntu, 40.013/40.013 Fri Jul 16 14:52:56 2021 40.013/40.013 The command was "./mace4 -c -f /tmp/mace4105894-2.in". 40.013/40.013 ============================== end of head =========================== 40.013/40.013 40.013/40.013 ============================== INPUT ================================= 40.013/40.013 40.013/40.013 % Reading from file /tmp/mace4105894-2.in 40.013/40.013 40.013/40.013 assign(max_seconds,10). 40.013/40.013 40.013/40.013 formulas(assumptions). 40.013/40.013 ->(x1,y) -> ->(filter(x1,x2,x3),filter(y,x2,x3)) # label(congruence). 40.013/40.013 ->(x2,y) -> ->(filter(x1,x2,x3),filter(x1,y,x3)) # label(congruence). 40.013/40.013 ->(x3,y) -> ->(filter(x1,x2,x3),filter(x1,x2,y)) # label(congruence). 40.013/40.013 ->(x1,y) -> ->(cons(x1,x2),cons(y,x2)) # label(congruence). 40.013/40.013 ->(x2,y) -> ->(cons(x1,x2),cons(x1,y)) # label(congruence). 40.013/40.013 ->(x1,y) -> ->(div(x1,x2),div(y,x2)) # label(congruence). 40.013/40.013 ->(x2,y) -> ->(div(x1,x2),div(x1,y)) # label(congruence). 40.013/40.013 ->(x1,y) -> ->(eq(x1,x2),eq(y,x2)) # label(congruence). 40.013/40.013 ->(x2,y) -> ->(eq(x1,x2),eq(x1,y)) # label(congruence). 40.013/40.013 ->(x1,y) -> ->(pair(x1,x2),pair(y,x2)) # label(congruence). 40.013/40.013 ->(x2,y) -> ->(pair(x1,x2),pair(x1,y)) # label(congruence). 40.013/40.013 ->*(filter(x1,x2,x4),pair(x5,ys)) & ->*(eq(div(x3,x1),pair(x6,x2)),false) -> ->(filter(x1,x2,cons(x3,x4)),pair(x5,cons(x3,ys))) # label(replacement). 40.013/40.013 ->(filter(x1,x2,nil),pair(mo,nil)) # label(replacement). 40.013/40.013 ->*(x,x) # label(reflexivity). 40.013/40.013 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 40.013/40.013 end_of_list. 40.013/40.013 40.013/40.013 formulas(goals). 40.013/40.013 (exists x1 exists x2 exists x3 exists x4 exists x5 exists x6 (->*(filter(x1,x2,x4),pair(x5,ys)) & ->*(eq(div(x3,x1),pair(x6,x2)),false))) # label(goal). 40.013/40.013 end_of_list. 40.013/40.013 40.013/40.013 ============================== end of input ========================== 40.013/40.013 40.013/40.013 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 40.013/40.013 40.013/40.013 % Formulas that are not ordinary clauses: 40.013/40.013 1 ->(x1,y) -> ->(filter(x1,x2,x3),filter(y,x2,x3)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 2 ->(x2,y) -> ->(filter(x1,x2,x3),filter(x1,y,x3)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 3 ->(x3,y) -> ->(filter(x1,x2,x3),filter(x1,x2,y)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 4 ->(x1,y) -> ->(cons(x1,x2),cons(y,x2)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 5 ->(x2,y) -> ->(cons(x1,x2),cons(x1,y)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 6 ->(x1,y) -> ->(div(x1,x2),div(y,x2)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 7 ->(x2,y) -> ->(div(x1,x2),div(x1,y)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 8 ->(x1,y) -> ->(eq(x1,x2),eq(y,x2)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 9 ->(x2,y) -> ->(eq(x1,x2),eq(x1,y)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 10 ->(x1,y) -> ->(pair(x1,x2),pair(y,x2)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 11 ->(x2,y) -> ->(pair(x1,x2),pair(x1,y)) # label(congruence) # label(non_clause). [assumption]. 40.013/40.013 12 ->*(filter(x1,x2,x4),pair(x5,ys)) & ->*(eq(div(x3,x1),pair(x6,x2)),false) -> ->(filter(x1,x2,cons(x3,x4)),pair(x5,cons(x3,ys))) # label(replacement) # label(non_clause). [assumption]. 40.013/40.013 13 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 40.013/40.013 14 (exists x1 exists x2 exists x3 exists x4 exists x5 exists x6 (->*(filter(x1,x2,x4),pair(x5,ys)) & ->*(eq(div(x3,x1),pair(x6,x2)),false))) # label(goal) # label(non_clause) # label(goal). [goal]. 40.013/40.013 40.013/40.013 ============================== end of process non-clausal formulas === 40.013/40.013 40.013/40.013 ============================== CLAUSES FOR SEARCH ==================== 40.013/40.013 40.013/40.013 formulas(mace4_clauses). 40.013/40.013 -->(x,y) | ->(filter(x,z,u),filter(y,z,u)) # label(congruence). 40.013/40.013 -->(x,y) | ->(filter(z,x,u),filter(z,y,u)) # label(congruence). 40.013/40.013 -->(x,y) | ->(filter(z,u,x),filter(z,u,y)) # label(congruence). 40.013/40.013 -->(x,y) | ->(cons(x,z),cons(y,z)) # label(congruence). 40.013/40.013 -->(x,y) | ->(cons(z,x),cons(z,y)) # label(congruence). 40.013/40.013 -->(x,y) | ->(div(x,z),div(y,z)) # label(congruence). 40.013/40.013 -->(x,y) | ->(div(z,x),div(z,y)) # label(congruence). 40.013/40.013 -->(x,y) | ->(eq(x,z),eq(y,z)) # label(congruence). 40.013/40.013 -->(x,y) | ->(eq(z,x),eq(z,y)) # label(congruence). 40.013/40.013 -->(x,y) | ->(pair(x,z),pair(y,z)) # label(congruence). 40.013/40.013 -->(x,y) | ->(pair(z,x),pair(z,y)) # label(congruence). 40.013/40.013 -->*(filter(x,y,z),pair(u,ys)) | -->*(eq(div(w,x),pair(v5,y)),false) | ->(filter(x,y,cons(w,z)),pair(u,cons(w,ys))) # label(replacement). 40.013/40.013 ->(filter(x,y,nil),pair(mo,nil)) # label(replacement). 40.013/40.013 ->*(x,x) # label(reflexivity). 40.013/40.013 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 40.013/40.013 -->*(filter(x,y,z),pair(u,ys)) | -->*(eq(div(w,x),pair(v5,y)),false) # label(goal). 40.013/40.013 end_of_list. 40.013/40.013 40.013/40.013 ============================== end of clauses for search ============= 40.013/40.013 40.013/40.013 % There are no natural numbers in the input. 40.013/40.013 40.013/40.013 ============================== DOMAIN SIZE 2 ========================= 40.013/40.013 40.013/40.013 ============================== MODEL ================================= 40.013/40.013 40.013/40.013 interpretation( 2, [number=1, seconds=0], [ 40.013/40.013 40.013/40.013 function(ys, [ 0 ]), 40.013/40.013 40.013/40.013 function(false, [ 0 ]), 40.013/40.013 40.013/40.013 function(mo, [ 0 ]), 40.013/40.013 40.013/40.013 function(nil, [ 0 ]), 40.013/40.013 40.013/40.013 function(pair(_,_), [ 40.013/40.013 0, 0, 40.013/40.013 0, 0 ]), 40.013/40.013 40.013/40.013 function(cons(_,_), [ 40.013/40.013 0, 0, 40.013/40.013 0, 0 ]), 40.013/40.013 40.013/40.013 function(div(_,_), [ 40.013/40.013 0, 0, 40.013/40.013 0, 0 ]), 40.013/40.013 40.013/40.013 function(eq(_,_), [ 40.013/40.013 1, 0, 40.013/40.013 0, 0 ]), 40.013/40.013 40.013/40.013 function(filter(_,_,_), [ 40.013/40.013 0, 0, 40.013/40.013 0, 0, 40.013/40.013 0, 0, 40.013/40.013 0, 0 ]), 40.013/40.013 40.013/40.013 relation(->*(_,_), [ 40.013/40.013 1, 0, 40.013/40.013 0, 1 ]), 40.013/40.013 40.013/40.013 relation(->(_,_), [ 40.013/40.013 1, 0, 40.013/40.013 0, 1 ]) 40.013/40.013 ]). 40.013/40.013 40.013/40.013 ============================== end of model ========================== 40.013/40.013 40.013/40.013 ============================== STATISTICS ============================ 40.013/40.013 40.013/40.013 For domain size 2. 40.013/40.013 40.013/40.013 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 40.013/40.013 Ground clauses: seen=254, kept=250. 40.013/40.013 Selections=26, assignments=27, propagations=18, current_models=1. 40.013/40.013 Rewrite_terms=1517, rewrite_bools=393, indexes=272. 40.013/40.013 Rules_from_neg_clauses=8, cross_offs=8. 40.013/40.013 40.013/40.013 ============================== end of statistics ===================== 40.013/40.013 40.013/40.013 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 40.013/40.013 40.013/40.013 Exiting with 1 model. 40.013/40.013 40.013/40.013 Process 105907 exit (max_models) Fri Jul 16 14:52:56 2021 40.013/40.013 The process finished Fri Jul 16 14:52:56 2021 40.013/40.013 40.013/40.013 40.013/40.013 Mace4 cooked interpretation: 40.013/40.013 40.013/40.013 40.013/40.013 40.013/40.013 The problem is infeasible. 40.013/40.013 40.013/40.013 40.013/40.013 CRule InfChecker Info: 40.013/40.013 filter(n:S,r:S,nil) -> pair(mo,nil) 40.013/40.013 Rule remains 40.013/40.013 Proof: 40.013/40.013 NO_CONDS 40.013/40.013 40.013/40.013 Problem 1: 40.013/40.013 40.013/40.013 Transform No Conds CTRS Processor: 40.013/40.013 40.013/40.013 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.013/40.013 Confluence Problem: 40.013/40.013 (VAR n:S r:S) 40.013/40.013 (STRATEGY CONTEXTSENSITIVE 40.013/40.013 (filter 1 2 3) 40.013/40.013 (cons 1 2) 40.013/40.013 (div 1 2) 40.013/40.013 (eq 1 2) 40.013/40.013 (fSNonEmpty) 40.013/40.013 (false) 40.013/40.013 (mo) 40.013/40.013 (nil) 40.013/40.013 (pair 1 2) 40.013/40.013 (true) 40.013/40.013 (ys) 40.013/40.013 ) 40.013/40.013 (RULES 40.013/40.013 filter(n:S,r:S,nil) -> pair(mo,nil) 40.013/40.013 ) 40.013/40.013 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.013/40.013 Resulting R: 40.013/40.013 (VAR n:S r:S) 40.013/40.013 (STRATEGY CONTEXTSENSITIVE 40.013/40.013 (filter 1 2 3) 40.013/40.013 (cons 1 2) 40.013/40.013 (div 1 2) 40.013/40.013 (eq 1 2) 40.013/40.013 (fSNonEmpty) 40.013/40.013 (false) 40.013/40.013 (mo) 40.013/40.013 (nil) 40.013/40.013 (pair 1 2) 40.013/40.013 (true) 40.013/40.013 (ys) 40.013/40.013 ) 40.013/40.013 (RULES 40.013/40.013 filter(n:S,r:S,nil) -> pair(mo,nil) 40.013/40.013 ) 40.013/40.013 40.013/40.013 Problem 1: 40.013/40.013 40.013/40.013 CleanTRS Processor: 40.013/40.013 40.013/40.013 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.013/40.013 Confluence Problem: 40.013/40.013 (VAR n:S r:S) 40.013/40.013 (STRATEGY CONTEXTSENSITIVE 40.013/40.013 (filter 1 2 3) 40.013/40.013 (cons 1 2) 40.013/40.013 (div 1 2) 40.013/40.013 (eq 1 2) 40.013/40.013 (fSNonEmpty) 40.013/40.013 (false) 40.013/40.013 (mo) 40.013/40.013 (nil) 40.013/40.013 (pair 1 2) 40.013/40.013 (true) 40.013/40.013 (ys) 40.013/40.013 ) 40.013/40.013 (RULES 40.013/40.013 filter(n:S,r:S,nil) -> pair(mo,nil) 40.013/40.013 ) 40.013/40.013 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.013/40.013 40.013/40.013 40.013/40.013 Problem 1: 40.013/40.013 40.013/40.013 Modular Confluence Combinations Decomposition Processor: 40.013/40.013 40.013/40.013 No usable combinations 40.013/40.013 40.013/40.013 Problem 1: 40.013/40.013 Linearity Processor: 40.013/40.013 Linear? 40.013/40.013 YES 40.013/40.013 Problem 1.1: 40.013/40.013 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.013/40.013 Confluence Problem: 40.013/40.013 (VAR n:S r:S) 40.013/40.013 (STRATEGY CONTEXTSENSITIVE 40.013/40.013 (filter 1 2 3) 40.013/40.013 (cons 1 2) 40.013/40.013 (div 1 2) 40.013/40.013 (eq 1 2) 40.013/40.013 (fSNonEmpty) 40.013/40.013 (false) 40.013/40.013 (mo) 40.013/40.013 (nil) 40.013/40.013 (pair 1 2) 40.013/40.013 (true) 40.013/40.013 (ys) 40.013/40.013 ) 40.013/40.013 (RULES 40.013/40.013 filter(n:S,r:S,nil) -> pair(mo,nil) 40.013/40.013 ) 40.013/40.013 Linear:YES 40.013/40.013 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.013/40.013 40.013/40.013 Huet Levy Processor: 40.013/40.013 -> Rules: 40.013/40.013 filter(n:S,r:S,nil) -> pair(mo,nil) 40.013/40.013 -> Vars: 40.013/40.013 n, r 40.013/40.013 -> FVars: 40.013/40.013 x3, x4 40.013/40.013 -> PVars: 40.013/40.013 n: [x3], r: [x4] 40.013/40.013 40.013/40.013 -> Rlps: 40.013/40.013 (rule: filter(x3:S,x4:S,nil) -> pair(mo,nil), id: 1, possubterms: filter(x3:S,x4:S,nil)->[], nil->[3]) 40.013/40.013 40.013/40.013 -> Unifications: 40.013/40.013 40.013/40.013 40.013/40.013 -> Critical pairs info: 40.013/40.013 40.013/40.013 40.013/40.013 -> Problem conclusions: 40.013/40.013 Left linear, Right linear, Linear 40.013/40.013 Weakly orthogonal, Almost orthogonal, Orthogonal 40.013/40.013 Huet-Levy confluent, Not Newman confluent 40.013/40.013 R is a TRS 40.013/40.013 40.013/40.013 40.013/40.013 The problem is joinable. 40.013/40.013 39.87user 1.03system 0:40.13elapsed 101%CPU (0avgtext+0avgdata 55140maxresident)k 40.013/40.013 8inputs+0outputs (0major+39352minor)pagefaults 0swaps