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