28.70/20.23 YES 28.70/20.23 28.70/20.23 Problem 1: 28.70/20.23 28.70/20.23 Infeasibility Problem: 28.70/20.23 (VAR vNonEmpty:S x:S) 28.70/20.23 (RULES 28.70/20.23 e(0) -> ttrue 28.70/20.23 e(s(x:S)) -> ffalse | e(x:S) ->* ttrue 28.70/20.23 e(s(x:S)) -> ttrue | o(x:S) ->* ttrue 28.70/20.23 o(0) -> ffalse 28.70/20.23 o(s(x:S)) -> ffalse | o(x:S) ->* ttrue 28.70/20.23 o(s(x:S)) -> ttrue | e(x:S) ->* ttrue 28.70/20.23 ) 28.70/20.23 28.70/20.23 Infeasibility Conditions: 28.70/20.23 e(x1:S) ->* ttrue 28.70/20.23 o(x1:S) ->* ttrue 28.70/20.23 28.70/20.23 Problem 1: 28.70/20.23 28.70/20.23 Obtaining a model using Mace4: 28.70/20.23 28.70/20.23 -> Usable Rules: 28.70/20.23 e(0) -> ttrue 28.70/20.23 e(s(x:S)) -> ffalse | e(x:S) ->* ttrue 28.70/20.23 e(s(x:S)) -> ttrue | o(x:S) ->* ttrue 28.70/20.23 o(0) -> ffalse 28.70/20.23 o(s(x:S)) -> ffalse | o(x:S) ->* ttrue 28.70/20.23 o(s(x:S)) -> ttrue | e(x:S) ->* ttrue 28.70/20.23 28.70/20.23 -> Mace4 Output: 28.70/20.23 ============================== Mace4 ================================= 28.70/20.23 Mace4 (64) version 2009-11A, November 2009. 28.70/20.23 Process 15806 was started by sandbox on n001.star.cs.uiowa.edu, 28.70/20.23 Mon Mar 25 12:14:27 2019 28.70/20.23 The command was "./mace4 -c -f /tmp/mace41957747793424238335.in". 28.70/20.23 ============================== end of head =========================== 28.70/20.23 28.70/20.23 ============================== INPUT ================================= 28.70/20.23 28.70/20.23 % Reading from file /tmp/mace41957747793424238335.in 28.70/20.23 28.70/20.23 assign(max_seconds,300). 28.70/20.23 28.70/20.23 formulas(assumptions). 28.70/20.23 arrowStar_s0(x,x) # label(reflexivity). 28.70/20.23 arrow_s0(x,y) & arrowStar_s0(y,z) -> arrowStar_s0(x,z) # label(transitivity). 28.70/20.23 arrow_s0(x1,y) -> arrow_s0(f2(x1),f2(y)) # label(congruence). 28.70/20.23 arrow_s0(x1,y) -> arrow_s0(f3(x1),f3(y)) # label(congruence). 28.70/20.23 arrow_s0(x1,y) -> arrow_s0(f7(x1),f7(y)) # label(congruence). 28.70/20.23 arrow_s0(f2(f4),f8) # label(repacement). 28.70/20.23 arrowStar_s0(f2(x1),f8) -> arrow_s0(f2(f7(x1)),f6) # label(repacement). 28.70/20.23 arrowStar_s0(f3(x1),f8) -> arrow_s0(f2(f7(x1)),f8) # label(repacement). 28.70/20.23 arrow_s0(f3(f4),f6) # label(repacement). 28.70/20.23 arrowStar_s0(f3(x1),f8) -> arrow_s0(f3(f7(x1)),f6) # label(repacement). 28.70/20.23 arrowStar_s0(f2(x1),f8) -> arrow_s0(f3(f7(x1)),f8) # label(repacement). 28.70/20.23 end_of_list. 28.70/20.23 28.70/20.23 formulas(goals). 28.70/20.23 (exists x3 (arrowStar_s0(f2(x3),f8) & arrowStar_s0(f3(x3),f8))) # label(goal). 28.70/20.23 end_of_list. 28.70/20.23 28.70/20.23 ============================== end of input ========================== 28.70/20.23 28.70/20.23 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 28.70/20.23 28.70/20.23 % Formulas that are not ordinary clauses: 28.70/20.23 1 arrow_s0(x,y) & arrowStar_s0(y,z) -> arrowStar_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 28.70/20.23 2 arrow_s0(x1,y) -> arrow_s0(f2(x1),f2(y)) # label(congruence) # label(non_clause). [assumption]. 28.70/20.23 3 arrow_s0(x1,y) -> arrow_s0(f3(x1),f3(y)) # label(congruence) # label(non_clause). [assumption]. 28.70/20.23 4 arrow_s0(x1,y) -> arrow_s0(f7(x1),f7(y)) # label(congruence) # label(non_clause). [assumption]. 28.70/20.23 5 arrowStar_s0(f2(x1),f8) -> arrow_s0(f2(f7(x1)),f6) # label(repacement) # label(non_clause). [assumption]. 28.70/20.23 6 arrowStar_s0(f3(x1),f8) -> arrow_s0(f2(f7(x1)),f8) # label(repacement) # label(non_clause). [assumption]. 28.70/20.23 7 arrowStar_s0(f3(x1),f8) -> arrow_s0(f3(f7(x1)),f6) # label(repacement) # label(non_clause). [assumption]. 28.70/20.23 8 arrowStar_s0(f2(x1),f8) -> arrow_s0(f3(f7(x1)),f8) # label(repacement) # label(non_clause). [assumption]. 28.70/20.23 9 (exists x3 (arrowStar_s0(f2(x3),f8) & arrowStar_s0(f3(x3),f8))) # label(goal) # label(non_clause) # label(goal). [goal]. 28.70/20.23 28.70/20.23 ============================== end of process non-clausal formulas === 28.70/20.23 28.70/20.23 ============================== CLAUSES FOR SEARCH ==================== 28.70/20.23 28.70/20.23 formulas(mace4_clauses). 28.70/20.23 arrowStar_s0(x,x) # label(reflexivity). 28.70/20.23 -arrow_s0(x,y) | -arrowStar_s0(y,z) | arrowStar_s0(x,z) # label(transitivity). 28.70/20.23 -arrow_s0(x,y) | arrow_s0(f2(x),f2(y)) # label(congruence). 28.70/20.23 -arrow_s0(x,y) | arrow_s0(f3(x),f3(y)) # label(congruence). 28.70/20.23 -arrow_s0(x,y) | arrow_s0(f7(x),f7(y)) # label(congruence). 28.70/20.23 arrow_s0(f2(f4),f8) # label(repacement). 28.70/20.23 -arrowStar_s0(f2(x),f8) | arrow_s0(f2(f7(x)),f6) # label(repacement). 28.70/20.23 -arrowStar_s0(f3(x),f8) | arrow_s0(f2(f7(x)),f8) # label(repacement). 28.70/20.23 arrow_s0(f3(f4),f6) # label(repacement). 28.70/20.23 -arrowStar_s0(f3(x),f8) | arrow_s0(f3(f7(x)),f6) # label(repacement). 28.70/20.23 -arrowStar_s0(f2(x),f8) | arrow_s0(f3(f7(x)),f8) # label(repacement). 28.70/20.23 -arrowStar_s0(f2(x),f8) | -arrowStar_s0(f3(x),f8) # label(goal). 28.70/20.23 end_of_list. 28.70/20.23 28.70/20.23 ============================== end of clauses for search ============= 28.70/20.23 28.70/20.23 % There are no natural numbers in the input. 28.70/20.23 28.70/20.23 ============================== DOMAIN SIZE 2 ========================= 28.70/20.23 28.70/20.23 ============================== MODEL ================================= 28.70/20.23 28.70/20.23 interpretation( 2, [number=1, seconds=0], [ 28.70/20.23 28.70/20.23 function(f4, [ 0 ]), 28.70/20.23 28.70/20.23 function(f6, [ 0 ]), 28.70/20.23 28.70/20.23 function(f8, [ 1 ]), 28.70/20.23 28.70/20.23 function(f2(_), [ 1, 0 ]), 28.70/20.23 28.70/20.23 function(f3(_), [ 0, 1 ]), 28.70/20.23 28.70/20.23 function(f7(_), [ 1, 0 ]), 28.70/20.23 28.70/20.23 relation(arrowStar_s0(_,_), [ 28.70/20.23 1, 0, 28.70/20.23 0, 1 ]), 28.70/20.23 28.70/20.23 relation(arrow_s0(_,_), [ 28.70/20.23 1, 0, 28.70/20.23 0, 1 ]) 28.70/20.23 ]). 28.70/20.23 28.70/20.23 ============================== end of model ========================== 28.70/20.23 28.70/20.23 ============================== STATISTICS ============================ 28.70/20.23 28.70/20.23 For domain size 2. 28.70/20.23 28.70/20.23 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 28.70/20.23 Ground clauses: seen=34, kept=30. 28.70/20.23 Selections=8, assignments=12, propagations=22, current_models=1. 28.70/20.23 Rewrite_terms=133, rewrite_bools=79, indexes=27. 28.70/20.23 Rules_from_neg_clauses=6, cross_offs=6. 28.70/20.23 28.70/20.23 ============================== end of statistics ===================== 28.70/20.23 28.70/20.23 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 28.70/20.23 28.70/20.23 Exiting with 1 model. 28.70/20.23 28.70/20.23 Process 15806 exit (max_models) Mon Mar 25 12:14:27 2019 28.70/20.23 The process finished Mon Mar 25 12:14:27 2019 28.70/20.23 28.70/20.23 28.70/20.23 Mace4 cooked interpretation: 28.70/20.23 28.70/20.23 % number = 1 28.70/20.23 % seconds = 0 28.70/20.23 28.70/20.23 % Interpretation of size 2 28.70/20.23 28.70/20.23 f4 = 0. 28.70/20.23 28.70/20.23 f6 = 0. 28.70/20.23 28.70/20.23 f8 = 1. 28.70/20.23 28.70/20.23 f2(0) = 1. 28.70/20.23 f2(1) = 0. 28.70/20.23 28.70/20.23 f3(0) = 0. 28.70/20.23 f3(1) = 1. 28.70/20.23 28.70/20.23 f7(0) = 1. 28.70/20.23 f7(1) = 0. 28.70/20.23 28.70/20.23 arrowStar_s0(0,0). 28.70/20.23 - arrowStar_s0(0,1). 28.70/20.23 - arrowStar_s0(1,0). 28.70/20.23 arrowStar_s0(1,1). 28.70/20.23 28.70/20.23 arrow_s0(0,0). 28.70/20.23 - arrow_s0(0,1). 28.70/20.23 - arrow_s0(1,0). 28.70/20.23 arrow_s0(1,1). 28.70/20.23 28.70/20.23 28.70/20.23 The problem is infeasible. 28.70/20.23 EOF