21.29/20.26 YES 21.29/20.26 21.29/20.26 Problem 1: 21.29/20.26 21.29/20.26 Infeasibility Problem: 21.29/20.26 (VAR vNonEmpty:S x:S y:S xs:S) 21.29/20.26 (RULES 21.29/20.26 le(0,s(y:S)) -> ttrue 21.29/20.26 le(s(x:S),s(y:S)) -> le(x:S,y:S) 21.29/20.26 le(x:S,0) -> ffalse 21.29/20.26 min(cons(x:S,nil)) -> x:S 21.29/20.26 min(cons(x:S,xs:S)) -> x:S | min(xs:S) ->* y:S, le(x:S,y:S) ->* ttrue 21.29/20.26 min(cons(x:S,xs:S)) -> y:S | min(xs:S) ->* y:S, le(x:S,y:S) ->* ffalse 21.29/20.26 ) 21.29/20.26 21.29/20.26 Infeasibility Conditions: 21.29/20.26 min(nil) ->* x3:S 21.29/20.26 le(x1:S,x3:S) ->* ffalse 21.29/20.26 21.29/20.26 Problem 1: 21.29/20.26 21.29/20.26 Obtaining a model using Mace4: 21.29/20.26 21.29/20.26 -> Usable Rules: 21.29/20.26 le(0,s(y:S)) -> ttrue 21.29/20.26 le(s(x:S),s(y:S)) -> le(x:S,y:S) 21.29/20.26 le(x:S,0) -> ffalse 21.29/20.26 min(cons(x:S,nil)) -> x:S 21.29/20.26 min(cons(x:S,xs:S)) -> x:S | min(xs:S) ->* y:S, le(x:S,y:S) ->* ttrue 21.29/20.26 min(cons(x:S,xs:S)) -> y:S | min(xs:S) ->* y:S, le(x:S,y:S) ->* ffalse 21.29/20.26 21.29/20.26 -> Mace4 Output: 21.29/20.26 ============================== Mace4 ================================= 21.29/20.26 Mace4 (64) version 2009-11A, November 2009. 21.29/20.26 Process 35597 was started by sandbox2 on n150.star.cs.uiowa.edu, 21.29/20.26 Tue Jul 6 11:01:04 2021 21.29/20.26 The command was "./mace4 -c -f /tmp/mace41957747793424238335.in". 21.29/20.26 ============================== end of head =========================== 21.29/20.26 21.29/20.26 ============================== INPUT ================================= 21.29/20.26 21.29/20.26 % Reading from file /tmp/mace41957747793424238335.in 21.29/20.26 21.29/20.26 assign(max_seconds,300). 21.29/20.26 21.29/20.26 formulas(assumptions). 21.29/20.26 arrowStar_s0(x,x) # label(reflexivity). 21.29/20.26 arrow_s0(x,y) & arrowStar_s0(y,z) -> arrowStar_s0(x,z) # label(transitivity). 21.29/20.26 arrow_s0(x1,y) -> arrow_s0(f2(x1,x2),f2(y,x2)) # label(congruence). 21.29/20.26 arrow_s0(x2,y) -> arrow_s0(f2(x1,x2),f2(x1,y)) # label(congruence). 21.29/20.26 arrow_s0(x1,y) -> arrow_s0(f3(x1),f3(y)) # label(congruence). 21.29/20.26 arrow_s0(x1,y) -> arrow_s0(f5(x1,x2),f5(y,x2)) # label(congruence). 21.29/20.26 arrow_s0(x2,y) -> arrow_s0(f5(x1,x2),f5(x1,y)) # label(congruence). 21.29/20.26 arrow_s0(x1,y) -> arrow_s0(f9(x1),f9(y)) # label(congruence). 21.29/20.26 arrow_s0(f2(f4,f9(x2)),f10) # label(repacement). 21.29/20.26 arrow_s0(f2(f9(x1),f9(x2)),f2(x1,x2)) # label(repacement). 21.29/20.26 arrow_s0(f2(x1,f4),f7) # label(repacement). 21.29/20.26 arrow_s0(f3(f5(x1,f8)),x1) # label(repacement). 21.29/20.26 arrowStar_s0(f3(x3),x2) & arrowStar_s0(f2(x1,x2),f10) -> arrow_s0(f3(f5(x1,x3)),x1) # label(repacement). 21.29/20.26 arrowStar_s0(f3(x3),x2) & arrowStar_s0(f2(x1,x2),f7) -> arrow_s0(f3(f5(x1,x3)),x2) # label(repacement). 21.29/20.26 end_of_list. 21.29/20.26 21.29/20.26 formulas(goals). 21.29/20.26 (exists x5 exists x6 (arrowStar_s0(f3(f8),x6) & arrowStar_s0(f2(x5,x6),f7))) # label(goal). 21.29/20.26 end_of_list. 21.29/20.26 21.29/20.26 ============================== end of input ========================== 21.29/20.26 21.29/20.26 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 21.29/20.26 21.29/20.26 % Formulas that are not ordinary clauses: 21.29/20.26 1 arrow_s0(x,y) & arrowStar_s0(y,z) -> arrowStar_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 21.29/20.26 2 arrow_s0(x1,y) -> arrow_s0(f2(x1,x2),f2(y,x2)) # label(congruence) # label(non_clause). [assumption]. 21.29/20.26 3 arrow_s0(x2,y) -> arrow_s0(f2(x1,x2),f2(x1,y)) # label(congruence) # label(non_clause). [assumption]. 21.29/20.26 4 arrow_s0(x1,y) -> arrow_s0(f3(x1),f3(y)) # label(congruence) # label(non_clause). [assumption]. 21.29/20.26 5 arrow_s0(x1,y) -> arrow_s0(f5(x1,x2),f5(y,x2)) # label(congruence) # label(non_clause). [assumption]. 21.29/20.26 6 arrow_s0(x2,y) -> arrow_s0(f5(x1,x2),f5(x1,y)) # label(congruence) # label(non_clause). [assumption]. 21.29/20.26 7 arrow_s0(x1,y) -> arrow_s0(f9(x1),f9(y)) # label(congruence) # label(non_clause). [assumption]. 21.29/20.26 8 arrowStar_s0(f3(x3),x2) & arrowStar_s0(f2(x1,x2),f10) -> arrow_s0(f3(f5(x1,x3)),x1) # label(repacement) # label(non_clause). [assumption]. 21.29/20.26 9 arrowStar_s0(f3(x3),x2) & arrowStar_s0(f2(x1,x2),f7) -> arrow_s0(f3(f5(x1,x3)),x2) # label(repacement) # label(non_clause). [assumption]. 21.29/20.26 10 (exists x5 exists x6 (arrowStar_s0(f3(f8),x6) & arrowStar_s0(f2(x5,x6),f7))) # label(goal) # label(non_clause) # label(goal). [goal]. 21.29/20.26 21.29/20.26 ============================== end of process non-clausal formulas === 21.29/20.26 21.29/20.26 ============================== CLAUSES FOR SEARCH ==================== 21.29/20.26 21.29/20.26 formulas(mace4_clauses). 21.29/20.26 arrowStar_s0(x,x) # label(reflexivity). 21.29/20.26 -arrow_s0(x,y) | -arrowStar_s0(y,z) | arrowStar_s0(x,z) # label(transitivity). 21.29/20.26 -arrow_s0(x,y) | arrow_s0(f2(x,z),f2(y,z)) # label(congruence). 21.29/20.26 -arrow_s0(x,y) | arrow_s0(f2(z,x),f2(z,y)) # label(congruence). 21.29/20.26 -arrow_s0(x,y) | arrow_s0(f3(x),f3(y)) # label(congruence). 21.29/20.26 -arrow_s0(x,y) | arrow_s0(f5(x,z),f5(y,z)) # label(congruence). 21.29/20.26 -arrow_s0(x,y) | arrow_s0(f5(z,x),f5(z,y)) # label(congruence). 21.29/20.26 -arrow_s0(x,y) | arrow_s0(f9(x),f9(y)) # label(congruence). 21.29/20.26 arrow_s0(f2(f4,f9(x)),f10) # label(repacement). 21.29/20.26 arrow_s0(f2(f9(x),f9(y)),f2(x,y)) # label(repacement). 21.29/20.26 arrow_s0(f2(x,f4),f7) # label(repacement). 21.29/20.26 arrow_s0(f3(f5(x,f8)),x) # label(repacement). 21.29/20.26 -arrowStar_s0(f3(x),y) | -arrowStar_s0(f2(z,y),f10) | arrow_s0(f3(f5(z,x)),z) # label(repacement). 21.29/20.26 -arrowStar_s0(f3(x),y) | -arrowStar_s0(f2(z,y),f7) | arrow_s0(f3(f5(z,x)),y) # label(repacement). 21.29/20.26 -arrowStar_s0(f3(f8),x) | -arrowStar_s0(f2(y,x),f7) # label(goal). 21.29/20.26 end_of_list. 21.29/20.26 21.29/20.26 ============================== end of clauses for search ============= 21.29/20.26 21.29/20.26 % There are no natural numbers in the input. 21.29/20.26 21.29/20.26 ============================== DOMAIN SIZE 2 ========================= 21.29/20.26 21.29/20.26 ============================== MODEL ================================= 21.29/20.26 21.29/20.26 interpretation( 2, [number=1, seconds=0], [ 21.29/20.26 21.29/20.26 function(f10, [ 0 ]), 21.29/20.26 21.29/20.26 function(f4, [ 0 ]), 21.29/20.26 21.29/20.26 function(f7, [ 0 ]), 21.29/20.26 21.29/20.26 function(f8, [ 1 ]), 21.29/20.26 21.29/20.26 function(f3(_), [ 0, 1 ]), 21.29/20.26 21.29/20.26 function(f9(_), [ 0, 0 ]), 21.29/20.26 21.29/20.26 function(f2(_,_), [ 21.29/20.26 0, 1, 21.29/20.26 0, 1 ]), 21.29/20.26 21.29/20.26 function(f5(_,_), [ 21.29/20.26 0, 0, 21.29/20.26 0, 0 ]), 21.29/20.26 21.29/20.26 relation(arrowStar_s0(_,_), [ 21.29/20.26 1, 1, 21.29/20.26 0, 1 ]), 21.29/20.26 21.29/20.26 relation(arrow_s0(_,_), [ 21.29/20.26 1, 1, 21.29/20.26 0, 1 ]) 21.29/20.26 ]). 21.29/20.26 21.29/20.26 ============================== end of model ========================== 21.29/20.26 21.29/20.26 ============================== STATISTICS ============================ 21.29/20.26 21.29/20.26 For domain size 2. 21.29/20.26 21.29/20.26 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 21.29/20.26 Ground clauses: seen=80, kept=76. 21.29/20.26 Selections=17, assignments=22, propagations=24, current_models=1. 21.29/20.26 Rewrite_terms=383, rewrite_bools=231, indexes=72. 21.29/20.26 Rules_from_neg_clauses=9, cross_offs=9. 21.29/20.26 21.29/20.26 ============================== end of statistics ===================== 21.29/20.26 21.29/20.26 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 21.29/20.26 21.29/20.26 Exiting with 1 model. 21.29/20.26 21.29/20.26 Process 35597 exit (max_models) Tue Jul 6 11:01:04 2021 21.29/20.26 The process finished Tue Jul 6 11:01:04 2021 21.29/20.26 21.29/20.26 21.29/20.26 Mace4 cooked interpretation: 21.29/20.26 21.29/20.26 % number = 1 21.29/20.26 % seconds = 0 21.29/20.26 21.29/20.26 % Interpretation of size 2 21.29/20.26 21.29/20.26 f10 = 0. 21.29/20.26 21.29/20.26 f4 = 0. 21.29/20.26 21.29/20.26 f7 = 0. 21.29/20.26 21.29/20.26 f8 = 1. 21.29/20.26 21.29/20.26 f3(0) = 0. 21.29/20.26 f3(1) = 1. 21.29/20.26 21.29/20.26 f9(0) = 0. 21.29/20.26 f9(1) = 0. 21.29/20.26 21.29/20.26 f2(0,0) = 0. 21.29/20.26 f2(0,1) = 1. 21.29/20.26 f2(1,0) = 0. 21.29/20.26 f2(1,1) = 1. 21.29/20.26 21.29/20.26 f5(0,0) = 0. 21.29/20.26 f5(0,1) = 0. 21.29/20.26 f5(1,0) = 0. 21.29/20.26 f5(1,1) = 0. 21.29/20.26 21.29/20.26 arrowStar_s0(0,0). 21.29/20.26 arrowStar_s0(0,1). 21.29/20.26 - arrowStar_s0(1,0). 21.29/20.26 arrowStar_s0(1,1). 21.29/20.26 21.29/20.26 arrow_s0(0,0). 21.29/20.26 arrow_s0(0,1). 21.29/20.26 - arrow_s0(1,0). 21.29/20.26 arrow_s0(1,1). 21.29/20.26 21.29/20.26 21.29/20.26 The problem is infeasible. 21.29/20.26 EOF