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