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