40.017/40.017 YES 40.017/40.017 40.017/40.017 Problem 1: 40.017/40.017 40.017/40.017 40.017/40.017 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.017/40.017 Confluence Problem: 40.017/40.017 (VAR vNonEmpty:S n:S r:S x:S xs:S y:S q:S) 40.017/40.017 (STRATEGY CONTEXTSENSITIVE 40.017/40.017 (filter 1 2 3) 40.017/40.017 (cons 1 2) 40.017/40.017 (div 1 2) 40.017/40.017 (eq 1 2) 40.017/40.017 (fSNonEmpty) 40.017/40.017 (false) 40.017/40.017 (mo) 40.017/40.017 (nil) 40.017/40.017 (pair 1 2) 40.017/40.017 (true) 40.017/40.017 (ys) 40.017/40.017 ) 40.017/40.017 (RULES 40.017/40.017 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.017/40.017 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.017/40.017 filter(n:S,r:S,nil) -> pair(mo,nil) 40.017/40.017 ) 40.017/40.017 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.017/40.017 40.017/40.017 40.017/40.017 Problem 1: 40.017/40.017 40.017/40.017 Inlining of Conditions Processor [STERN17]: 40.017/40.017 40.017/40.017 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.017/40.017 Confluence Problem: 40.017/40.017 (VAR vNonEmpty:S n:S r:S x:S xs:S y:S q:S) 40.017/40.017 (STRATEGY CONTEXTSENSITIVE 40.017/40.017 (filter 1 2 3) 40.017/40.017 (cons 1 2) 40.017/40.017 (div 1 2) 40.017/40.017 (eq 1 2) 40.017/40.017 (fSNonEmpty) 40.017/40.017 (false) 40.017/40.017 (mo) 40.017/40.017 (nil) 40.017/40.017 (pair 1 2) 40.017/40.017 (true) 40.017/40.017 (ys) 40.017/40.017 ) 40.017/40.017 (RULES 40.017/40.017 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.017/40.017 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.017/40.017 filter(n:S,r:S,nil) -> pair(mo,nil) 40.017/40.017 ) 40.017/40.017 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.017/40.017 40.017/40.017 40.017/40.017 Problem 1: 40.017/40.017 40.017/40.017 Clean CTRS Processor: 40.017/40.017 40.017/40.017 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.017/40.017 Confluence Problem: 40.017/40.017 (VAR n:S r:S) 40.017/40.017 (STRATEGY CONTEXTSENSITIVE 40.017/40.017 (filter 1 2 3) 40.017/40.017 (cons 1 2) 40.017/40.017 (div 1 2) 40.017/40.017 (eq 1 2) 40.017/40.017 (fSNonEmpty) 40.017/40.017 (false) 40.017/40.017 (mo) 40.017/40.017 (nil) 40.017/40.017 (pair 1 2) 40.017/40.017 (true) 40.017/40.017 (ys) 40.017/40.017 ) 40.017/40.017 (RULES 40.017/40.017 filter(n:S,r:S,nil) -> pair(mo,nil) 40.017/40.017 ) 40.017/40.017 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.017/40.017 40.017/40.017 CRule InfChecker Info: 40.017/40.017 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.017/40.017 Rule deleted 40.017/40.017 Proof: 40.017/40.017 YES 40.017/40.017 40.017/40.017 Problem 1: 40.017/40.017 40.017/40.017 Infeasibility Problem: 40.017/40.017 [(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.017/40.017 (STRATEGY CONTEXTSENSITIVE 40.017/40.017 (filter 1 2 3) 40.017/40.017 (cons 1 2) 40.017/40.017 (div 1 2) 40.017/40.017 (eq 1 2) 40.017/40.017 (fSNonEmpty) 40.017/40.017 (false) 40.017/40.017 (mo) 40.017/40.017 (nil) 40.017/40.017 (pair 1 2) 40.017/40.017 (true) 40.017/40.017 (ys) 40.017/40.017 ) 40.017/40.017 (RULES 40.017/40.017 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.017/40.017 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.017/40.017 filter(n:S:S,r:S:S,nil) -> pair(mo,nil) 40.017/40.017 )] 40.017/40.017 40.017/40.017 Infeasibility Conditions: 40.017/40.017 eq(div(x:S:S,n:S:S),pair(q:S:S,r:S:S)) ->* true 40.017/40.017 40.017/40.017 Problem 1: 40.017/40.017 40.017/40.017 Obtaining a model using Mace4: 40.017/40.017 40.017/40.017 -> Usable Rules: 40.017/40.017 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.017/40.017 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.017/40.017 filter(n:S:S,r:S:S,nil) -> pair(mo,nil) 40.017/40.017 40.017/40.017 -> Mace4 Output: 40.017/40.017 ============================== Mace4 ================================= 40.017/40.017 Mace4 (64) version 2009-11A, November 2009. 40.017/40.017 Process 44081 was started by ubuntu on ubuntu, 40.017/40.017 Wed Jul 14 10:29:39 2021 40.017/40.017 The command was "./mace4 -c -f /tmp/mace444070-2.in". 40.017/40.017 ============================== end of head =========================== 40.017/40.017 40.017/40.017 ============================== INPUT ================================= 40.017/40.017 40.017/40.017 % Reading from file /tmp/mace444070-2.in 40.017/40.017 40.017/40.017 assign(max_seconds,20). 40.017/40.017 40.017/40.017 formulas(assumptions). 40.017/40.017 ->(x1,y) -> ->(filter(x1,x2,x3),filter(y,x2,x3)) # label(congruence). 40.017/40.017 ->(x2,y) -> ->(filter(x1,x2,x3),filter(x1,y,x3)) # label(congruence). 40.017/40.017 ->(x3,y) -> ->(filter(x1,x2,x3),filter(x1,x2,y)) # label(congruence). 40.017/40.017 ->(x1,y) -> ->(cons(x1,x2),cons(y,x2)) # label(congruence). 40.017/40.017 ->(x2,y) -> ->(cons(x1,x2),cons(x1,y)) # label(congruence). 40.017/40.017 ->(x1,y) -> ->(div(x1,x2),div(y,x2)) # label(congruence). 40.017/40.017 ->(x2,y) -> ->(div(x1,x2),div(x1,y)) # label(congruence). 40.017/40.017 ->(x1,y) -> ->(eq(x1,x2),eq(y,x2)) # label(congruence). 40.017/40.017 ->(x2,y) -> ->(eq(x1,x2),eq(x1,y)) # label(congruence). 40.017/40.017 ->(x1,y) -> ->(pair(x1,x2),pair(y,x2)) # label(congruence). 40.017/40.017 ->(x2,y) -> ->(pair(x1,x2),pair(x1,y)) # label(congruence). 40.017/40.017 ->*(eq(div(x4,x2),pair(x7,x3)),true) -> ->(filter(x2,x3,cons(x4,x5)),pair(x4,x5)) # label(replacement). 40.017/40.017 ->*(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.017/40.017 ->(filter(x2,x3,nil),pair(mo,nil)) # label(replacement). 40.017/40.017 ->*(x,x) # label(reflexivity). 40.017/40.017 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 40.017/40.017 end_of_list. 40.017/40.017 40.017/40.017 formulas(goals). 40.017/40.017 (exists x2 exists x3 exists x4 exists x7 ->*(eq(div(x4,x2),pair(x7,x3)),true)) # label(goal). 40.017/40.017 end_of_list. 40.017/40.017 40.017/40.017 ============================== end of input ========================== 40.017/40.017 40.017/40.017 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 40.017/40.017 40.017/40.017 % Formulas that are not ordinary clauses: 40.017/40.017 1 ->(x1,y) -> ->(filter(x1,x2,x3),filter(y,x2,x3)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 2 ->(x2,y) -> ->(filter(x1,x2,x3),filter(x1,y,x3)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 3 ->(x3,y) -> ->(filter(x1,x2,x3),filter(x1,x2,y)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 4 ->(x1,y) -> ->(cons(x1,x2),cons(y,x2)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 5 ->(x2,y) -> ->(cons(x1,x2),cons(x1,y)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 6 ->(x1,y) -> ->(div(x1,x2),div(y,x2)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 7 ->(x2,y) -> ->(div(x1,x2),div(x1,y)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 8 ->(x1,y) -> ->(eq(x1,x2),eq(y,x2)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 9 ->(x2,y) -> ->(eq(x1,x2),eq(x1,y)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 10 ->(x1,y) -> ->(pair(x1,x2),pair(y,x2)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 11 ->(x2,y) -> ->(pair(x1,x2),pair(x1,y)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 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.017/40.017 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.017/40.017 14 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 40.017/40.017 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.017/40.017 40.017/40.017 ============================== end of process non-clausal formulas === 40.017/40.017 40.017/40.017 ============================== CLAUSES FOR SEARCH ==================== 40.017/40.017 40.017/40.017 formulas(mace4_clauses). 40.017/40.017 -->(x,y) | ->(filter(x,z,u),filter(y,z,u)) # label(congruence). 40.017/40.017 -->(x,y) | ->(filter(z,x,u),filter(z,y,u)) # label(congruence). 40.017/40.017 -->(x,y) | ->(filter(z,u,x),filter(z,u,y)) # label(congruence). 40.017/40.017 -->(x,y) | ->(cons(x,z),cons(y,z)) # label(congruence). 40.017/40.017 -->(x,y) | ->(cons(z,x),cons(z,y)) # label(congruence). 40.017/40.017 -->(x,y) | ->(div(x,z),div(y,z)) # label(congruence). 40.017/40.017 -->(x,y) | ->(div(z,x),div(z,y)) # label(congruence). 40.017/40.017 -->(x,y) | ->(eq(x,z),eq(y,z)) # label(congruence). 40.017/40.017 -->(x,y) | ->(eq(z,x),eq(z,y)) # label(congruence). 40.017/40.017 -->(x,y) | ->(pair(x,z),pair(y,z)) # label(congruence). 40.017/40.017 -->(x,y) | ->(pair(z,x),pair(z,y)) # label(congruence). 40.017/40.017 -->*(eq(div(x,y),pair(z,u)),true) | ->(filter(y,u,cons(x,w)),pair(x,w)) # label(replacement). 40.017/40.017 -->*(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.017/40.017 ->(filter(x,y,nil),pair(mo,nil)) # label(replacement). 40.017/40.017 ->*(x,x) # label(reflexivity). 40.017/40.017 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 40.017/40.017 -->*(eq(div(x,y),pair(z,u)),true) # label(goal). 40.017/40.017 end_of_list. 40.017/40.017 40.017/40.017 ============================== end of clauses for search ============= 40.017/40.017 40.017/40.017 % There are no natural numbers in the input. 40.017/40.017 40.017/40.017 ============================== DOMAIN SIZE 2 ========================= 40.017/40.017 40.017/40.017 ============================== MODEL ================================= 40.017/40.017 40.017/40.017 interpretation( 2, [number=1, seconds=0], [ 40.017/40.017 40.017/40.017 function(true, [ 0 ]), 40.017/40.017 40.017/40.017 function(ys, [ 0 ]), 40.017/40.017 40.017/40.017 function(false, [ 0 ]), 40.017/40.017 40.017/40.017 function(mo, [ 0 ]), 40.017/40.017 40.017/40.017 function(nil, [ 0 ]), 40.017/40.017 40.017/40.017 function(pair(_,_), [ 40.017/40.017 0, 0, 40.017/40.017 0, 0 ]), 40.017/40.017 40.017/40.017 function(cons(_,_), [ 40.017/40.017 0, 0, 40.017/40.017 0, 0 ]), 40.017/40.017 40.017/40.017 function(div(_,_), [ 40.017/40.017 0, 0, 40.017/40.017 0, 0 ]), 40.017/40.017 40.017/40.017 function(eq(_,_), [ 40.017/40.017 1, 0, 40.017/40.017 0, 0 ]), 40.017/40.017 40.017/40.017 function(filter(_,_,_), [ 40.017/40.017 0, 0, 40.017/40.017 0, 0, 40.017/40.017 0, 0, 40.017/40.017 0, 0 ]), 40.017/40.017 40.017/40.017 relation(->*(_,_), [ 40.017/40.017 1, 0, 40.017/40.017 0, 1 ]), 40.017/40.017 40.017/40.017 relation(->(_,_), [ 40.017/40.017 1, 0, 40.017/40.017 0, 1 ]) 40.017/40.017 ]). 40.017/40.017 40.017/40.017 ============================== end of model ========================== 40.017/40.017 40.017/40.017 ============================== STATISTICS ============================ 40.017/40.017 40.017/40.017 For domain size 2. 40.017/40.017 40.017/40.017 Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). 40.017/40.017 Ground clauses: seen=238, kept=234. 40.017/40.017 Selections=25, assignments=25, propagations=12, current_models=1. 40.017/40.017 Rewrite_terms=1300, rewrite_bools=303, indexes=204. 40.017/40.017 Rules_from_neg_clauses=5, cross_offs=5. 40.017/40.017 40.017/40.017 ============================== end of statistics ===================== 40.017/40.017 40.017/40.017 User_CPU=0.01, System_CPU=0.00, Wall_clock=0. 40.017/40.017 40.017/40.017 Exiting with 1 model. 40.017/40.017 40.017/40.017 Process 44081 exit (max_models) Wed Jul 14 10:29:39 2021 40.017/40.017 The process finished Wed Jul 14 10:29:39 2021 40.017/40.017 40.017/40.017 40.017/40.017 Mace4 cooked interpretation: 40.017/40.017 40.017/40.017 40.017/40.017 40.017/40.017 The problem is infeasible. 40.017/40.017 40.017/40.017 40.017/40.017 CRule InfChecker Info: 40.017/40.017 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.017/40.017 Rule deleted 40.017/40.017 Proof: 40.017/40.017 YES 40.017/40.017 40.017/40.017 Problem 1: 40.017/40.017 40.017/40.017 Infeasibility Problem: 40.017/40.017 [(VAR vNonEmpty:S n:S:S r:S:S x:S:S xs:S:S y:S:S q:S:S) 40.017/40.017 (STRATEGY CONTEXTSENSITIVE 40.017/40.017 (filter 1 2 3) 40.017/40.017 (cons 1 2) 40.017/40.017 (div 1 2) 40.017/40.017 (eq 1 2) 40.017/40.017 (fSNonEmpty) 40.017/40.017 (false) 40.017/40.017 (mo) 40.017/40.017 (nil) 40.017/40.017 (pair 1 2) 40.017/40.017 (ys) 40.017/40.017 ) 40.017/40.017 (RULES 40.017/40.017 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.017/40.017 filter(n:S:S,r:S:S,nil) -> pair(mo,nil) 40.017/40.017 )] 40.017/40.017 40.017/40.017 Infeasibility Conditions: 40.017/40.017 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.017/40.017 40.017/40.017 Problem 1: 40.017/40.017 40.017/40.017 Obtaining a model using Mace4: 40.017/40.017 40.017/40.017 -> Usable Rules: 40.017/40.017 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.017/40.017 filter(n:S:S,r:S:S,nil) -> pair(mo,nil) 40.017/40.017 40.017/40.017 -> Mace4 Output: 40.017/40.017 ============================== Mace4 ================================= 40.017/40.017 Mace4 (64) version 2009-11A, November 2009. 40.017/40.017 Process 44121 was started by ubuntu on ubuntu, 40.017/40.017 Wed Jul 14 10:29:59 2021 40.017/40.017 The command was "./mace4 -c -f /tmp/mace444108-2.in". 40.017/40.017 ============================== end of head =========================== 40.017/40.017 40.017/40.017 ============================== INPUT ================================= 40.017/40.017 40.017/40.017 % Reading from file /tmp/mace444108-2.in 40.017/40.017 40.017/40.017 assign(max_seconds,20). 40.017/40.017 40.017/40.017 formulas(assumptions). 40.017/40.017 ->(x1,y) -> ->(filter(x1,x2,x3),filter(y,x2,x3)) # label(congruence). 40.017/40.017 ->(x2,y) -> ->(filter(x1,x2,x3),filter(x1,y,x3)) # label(congruence). 40.017/40.017 ->(x3,y) -> ->(filter(x1,x2,x3),filter(x1,x2,y)) # label(congruence). 40.017/40.017 ->(x1,y) -> ->(cons(x1,x2),cons(y,x2)) # label(congruence). 40.017/40.017 ->(x2,y) -> ->(cons(x1,x2),cons(x1,y)) # label(congruence). 40.017/40.017 ->(x1,y) -> ->(div(x1,x2),div(y,x2)) # label(congruence). 40.017/40.017 ->(x2,y) -> ->(div(x1,x2),div(x1,y)) # label(congruence). 40.017/40.017 ->(x1,y) -> ->(eq(x1,x2),eq(y,x2)) # label(congruence). 40.017/40.017 ->(x2,y) -> ->(eq(x1,x2),eq(x1,y)) # label(congruence). 40.017/40.017 ->(x1,y) -> ->(pair(x1,x2),pair(y,x2)) # label(congruence). 40.017/40.017 ->(x2,y) -> ->(pair(x1,x2),pair(x1,y)) # label(congruence). 40.017/40.017 ->*(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.017/40.017 ->(filter(x1,x2,nil),pair(mo,nil)) # label(replacement). 40.017/40.017 ->*(x,x) # label(reflexivity). 40.017/40.017 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 40.017/40.017 end_of_list. 40.017/40.017 40.017/40.017 formulas(goals). 40.017/40.017 (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.017/40.017 end_of_list. 40.017/40.017 40.017/40.017 ============================== end of input ========================== 40.017/40.017 40.017/40.017 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 40.017/40.017 40.017/40.017 % Formulas that are not ordinary clauses: 40.017/40.017 1 ->(x1,y) -> ->(filter(x1,x2,x3),filter(y,x2,x3)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 2 ->(x2,y) -> ->(filter(x1,x2,x3),filter(x1,y,x3)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 3 ->(x3,y) -> ->(filter(x1,x2,x3),filter(x1,x2,y)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 4 ->(x1,y) -> ->(cons(x1,x2),cons(y,x2)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 5 ->(x2,y) -> ->(cons(x1,x2),cons(x1,y)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 6 ->(x1,y) -> ->(div(x1,x2),div(y,x2)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 7 ->(x2,y) -> ->(div(x1,x2),div(x1,y)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 8 ->(x1,y) -> ->(eq(x1,x2),eq(y,x2)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 9 ->(x2,y) -> ->(eq(x1,x2),eq(x1,y)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 10 ->(x1,y) -> ->(pair(x1,x2),pair(y,x2)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 11 ->(x2,y) -> ->(pair(x1,x2),pair(x1,y)) # label(congruence) # label(non_clause). [assumption]. 40.017/40.017 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.017/40.017 13 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 40.017/40.017 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.017/40.017 40.017/40.017 ============================== end of process non-clausal formulas === 40.017/40.017 40.017/40.017 ============================== CLAUSES FOR SEARCH ==================== 40.017/40.017 40.017/40.017 formulas(mace4_clauses). 40.017/40.017 -->(x,y) | ->(filter(x,z,u),filter(y,z,u)) # label(congruence). 40.017/40.017 -->(x,y) | ->(filter(z,x,u),filter(z,y,u)) # label(congruence). 40.017/40.017 -->(x,y) | ->(filter(z,u,x),filter(z,u,y)) # label(congruence). 40.017/40.017 -->(x,y) | ->(cons(x,z),cons(y,z)) # label(congruence). 40.017/40.017 -->(x,y) | ->(cons(z,x),cons(z,y)) # label(congruence). 40.017/40.017 -->(x,y) | ->(div(x,z),div(y,z)) # label(congruence). 40.017/40.017 -->(x,y) | ->(div(z,x),div(z,y)) # label(congruence). 40.017/40.017 -->(x,y) | ->(eq(x,z),eq(y,z)) # label(congruence). 40.017/40.017 -->(x,y) | ->(eq(z,x),eq(z,y)) # label(congruence). 40.017/40.017 -->(x,y) | ->(pair(x,z),pair(y,z)) # label(congruence). 40.017/40.017 -->(x,y) | ->(pair(z,x),pair(z,y)) # label(congruence). 40.017/40.017 -->*(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.017/40.017 ->(filter(x,y,nil),pair(mo,nil)) # label(replacement). 40.017/40.017 ->*(x,x) # label(reflexivity). 40.017/40.017 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 40.017/40.017 -->*(filter(x,y,z),pair(u,ys)) | -->*(eq(div(w,x),pair(v5,y)),false) # label(goal). 40.017/40.017 end_of_list. 40.017/40.017 40.017/40.017 ============================== end of clauses for search ============= 40.017/40.017 40.017/40.017 % There are no natural numbers in the input. 40.017/40.017 40.017/40.017 ============================== DOMAIN SIZE 2 ========================= 40.017/40.017 40.017/40.017 ============================== MODEL ================================= 40.017/40.017 40.017/40.017 interpretation( 2, [number=1, seconds=0], [ 40.017/40.017 40.017/40.017 function(ys, [ 0 ]), 40.017/40.017 40.017/40.017 function(false, [ 0 ]), 40.017/40.017 40.017/40.017 function(mo, [ 0 ]), 40.017/40.017 40.017/40.017 function(nil, [ 0 ]), 40.017/40.017 40.017/40.017 function(pair(_,_), [ 40.017/40.017 0, 0, 40.017/40.017 0, 0 ]), 40.017/40.017 40.017/40.017 function(cons(_,_), [ 40.017/40.017 0, 0, 40.017/40.017 0, 0 ]), 40.017/40.017 40.017/40.017 function(div(_,_), [ 40.017/40.017 0, 0, 40.017/40.017 0, 0 ]), 40.017/40.017 40.017/40.017 function(eq(_,_), [ 40.017/40.017 1, 0, 40.017/40.017 0, 0 ]), 40.017/40.017 40.017/40.017 function(filter(_,_,_), [ 40.017/40.017 0, 0, 40.017/40.017 0, 0, 40.017/40.017 0, 0, 40.017/40.017 0, 0 ]), 40.017/40.017 40.017/40.017 relation(->*(_,_), [ 40.017/40.017 1, 0, 40.017/40.017 0, 1 ]), 40.017/40.017 40.017/40.017 relation(->(_,_), [ 40.017/40.017 1, 0, 40.017/40.017 0, 1 ]) 40.017/40.017 ]). 40.017/40.017 40.017/40.017 ============================== end of model ========================== 40.017/40.017 40.017/40.017 ============================== STATISTICS ============================ 40.017/40.017 40.017/40.017 For domain size 2. 40.017/40.017 40.017/40.017 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 40.017/40.017 Ground clauses: seen=254, kept=250. 40.017/40.017 Selections=26, assignments=27, propagations=18, current_models=1. 40.017/40.017 Rewrite_terms=1517, rewrite_bools=393, indexes=272. 40.017/40.017 Rules_from_neg_clauses=8, cross_offs=8. 40.017/40.017 40.017/40.017 ============================== end of statistics ===================== 40.017/40.017 40.017/40.017 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 40.017/40.017 40.017/40.017 Exiting with 1 model. 40.017/40.017 40.017/40.017 Process 44121 exit (max_models) Wed Jul 14 10:29:59 2021 40.017/40.017 The process finished Wed Jul 14 10:29:59 2021 40.017/40.017 40.017/40.017 40.017/40.017 Mace4 cooked interpretation: 40.017/40.017 40.017/40.017 40.017/40.017 40.017/40.017 The problem is infeasible. 40.017/40.017 40.017/40.017 40.017/40.017 CRule InfChecker Info: 40.017/40.017 filter(n:S,r:S,nil) -> pair(mo,nil) 40.017/40.017 Rule remains 40.017/40.017 Proof: 40.017/40.017 NO_CONDS 40.017/40.017 40.017/40.017 Problem 1: 40.017/40.017 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.017/40.017 Confluence Problem: 40.017/40.017 (VAR n:S r:S) 40.017/40.017 (STRATEGY CONTEXTSENSITIVE 40.017/40.017 (filter 1 2 3) 40.017/40.017 (cons 1 2) 40.017/40.017 (div 1 2) 40.017/40.017 (eq 1 2) 40.017/40.017 (fSNonEmpty) 40.017/40.017 (false) 40.017/40.017 (mo) 40.017/40.017 (nil) 40.017/40.017 (pair 1 2) 40.017/40.017 (true) 40.017/40.017 (ys) 40.017/40.017 ) 40.017/40.017 (RULES 40.017/40.017 filter(n:S,r:S,nil) -> pair(mo,nil) 40.017/40.017 ) 40.017/40.017 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 40.017/40.017 40.017/40.017 Critical Pairs Processor: 40.017/40.017 -> Rules: 40.017/40.017 filter(n:S,r:S,nil) -> pair(mo,nil) 40.017/40.017 -> Vars: 40.017/40.017 "n", "r" 40.017/40.017 -> FVars: 40.017/40.017 "x3", "x4" 40.017/40.017 -> PVars: 40.017/40.017 "n": ["x3"], "r": ["x4"] 40.017/40.017 40.017/40.017 -> Rlps: 40.017/40.017 crule: filter(x3:S,x4:S,nil) -> pair(mo,nil), id: 1, possubterms: filter(x3:S,x4:S,nil)-> [], nil-> [3] 40.017/40.017 40.017/40.017 -> Unifications: 40.017/40.017 40.017/40.017 40.017/40.017 -> Critical pairs info: 40.017/40.017 40.017/40.017 40.017/40.017 -> Problem conclusions: 40.017/40.017 Left linear, Right linear, Linear 40.017/40.017 Weakly orthogonal, Almost orthogonal, Orthogonal 40.017/40.017 CTRS Type: 1 40.017/40.017 Deterministic, Strongly deterministic 40.017/40.017 Oriented CTRS, Properly oriented CTRS, Join CTRS 40.017/40.017 Maybe right-stable CTRS, Overlay CTRS 40.017/40.017 Normal CTRS, Almost normal CTRS 40.017/40.017 Maybe terminating CTRS, Joinable CCPs 40.017/40.017 Level confluent 40.017/40.017 Confluent 40.017/40.017 40.017/40.017 The problem is joinable. 40.017/40.017 40.68user 0.98system 0:40.17elapsed 103%CPU (0avgtext+0avgdata 55276maxresident)k 40.017/40.017 0inputs+0outputs (0major+38739minor)pagefaults 0swaps