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