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