35.34/20.36	YES
35.34/20.36	
35.34/20.36	Problem 1: 
35.34/20.36	
35.34/20.36	Infeasibility Problem:
35.34/20.36	[(VAR vNonEmpty x y vNonEmpty x2 x1)
35.34/20.36	(STRATEGY CONTEXTSENSITIVE
35.34/20.36	(pin 1)
35.34/20.36	(tc 1)
35.34/20.36	(a)
35.34/20.36	(b)
35.34/20.36	(c)
35.34/20.36	(fSNonEmpty)
35.34/20.36	(pout 1)
35.34/20.36	(z)
35.34/20.36	)
35.34/20.36	(RULES
35.34/20.36	pin(a) -> pout(b)
35.34/20.36	pin(b) -> pout(c)
35.34/20.36	tc(x) -> x
35.34/20.36	tc(x) -> y | pin(x) ->* pout(z), tc(z) ->* y
35.34/20.36	)]
35.34/20.36	
35.34/20.36	Infeasibility Conditions:
35.34/20.36	pin(x1) ->* pout(z), tc(z) ->* x2
35.34/20.36	
35.34/20.36	Problem 1: 
35.34/20.36	
35.34/20.36	Obtaining a model using Mace4:
35.34/20.36	
35.34/20.36	 -> Usable Rules:
35.34/20.36	pin(a) -> pout(b)
35.34/20.36	pin(b) -> pout(c)
35.34/20.36	tc(x) -> x
35.34/20.36	tc(x) -> y | pin(x) ->* pout(z), tc(z) ->* y
35.34/20.36	
35.34/20.36	 -> Mace4 Output:
35.34/20.36	============================== Mace4 =================================
35.34/20.36	Mace4 (64) version 2009-11A, November 2009.
35.34/20.36	Process 49073 was started by sandbox on n086.star.cs.uiowa.edu,
35.34/20.36	Wed Jul 13 08:11:14 2022
35.34/20.36	The command was "./mace4 -c -f /tmp/mace449063.in".
35.34/20.36	============================== end of head ===========================
35.34/20.36	
35.34/20.36	============================== INPUT =================================
35.34/20.36	
35.34/20.36	% Reading from file /tmp/mace449063.in
35.34/20.36	
35.34/20.36	assign(max_seconds,100).
35.34/20.36	
35.34/20.36	formulas(assumptions).
35.34/20.36	->(x1,y) -> ->(pin(x1),pin(y)) # label(congruence).
35.34/20.36	->(x1,y) -> ->(tc(x1),tc(y)) # label(congruence).
35.34/20.36	->(x1,y) -> ->(pout(x1),pout(y)) # label(congruence).
35.34/20.36	->(pin(a),pout(b)) # label(replacement).
35.34/20.36	->(pin(b),pout(c)) # label(replacement).
35.34/20.36	->(tc(x1),x1) # label(replacement).
35.34/20.36	->*(pin(x1),pout(z)) & ->*(tc(z),x2) -> ->(tc(x1),x2) # label(replacement).
35.34/20.36	->*(x,x) # label(reflexivity).
35.34/20.36	->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity).
35.34/20.36	end_of_list.
35.34/20.36	
35.34/20.36	formulas(goals).
35.34/20.36	(exists x4 exists x5 (->*(pin(x5),pout(z)) & ->*(tc(z),x4))) # label(goal).
35.34/20.36	end_of_list.
35.34/20.36	
35.34/20.36	============================== end of input ==========================
35.34/20.36	
35.34/20.36	============================== PROCESS NON-CLAUSAL FORMULAS ==========
35.34/20.36	
35.34/20.36	% Formulas that are not ordinary clauses:
35.34/20.36	1 ->(x1,y) -> ->(pin(x1),pin(y)) # label(congruence) # label(non_clause).  [assumption].
35.34/20.36	2 ->(x1,y) -> ->(tc(x1),tc(y)) # label(congruence) # label(non_clause).  [assumption].
35.34/20.36	3 ->(x1,y) -> ->(pout(x1),pout(y)) # label(congruence) # label(non_clause).  [assumption].
35.34/20.36	4 ->*(pin(x1),pout(z)) & ->*(tc(z),x2) -> ->(tc(x1),x2) # label(replacement) # label(non_clause).  [assumption].
35.34/20.36	5 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause).  [assumption].
35.34/20.36	6 (exists x4 exists x5 (->*(pin(x5),pout(z)) & ->*(tc(z),x4))) # label(goal) # label(non_clause) # label(goal).  [goal].
35.34/20.36	
35.34/20.36	============================== end of process non-clausal formulas ===
35.34/20.36	
35.34/20.36	============================== CLAUSES FOR SEARCH ====================
35.34/20.36	
35.34/20.36	formulas(mace4_clauses).
35.34/20.36	-->(x,y) | ->(pin(x),pin(y)) # label(congruence).
35.34/20.36	-->(x,y) | ->(tc(x),tc(y)) # label(congruence).
35.34/20.36	-->(x,y) | ->(pout(x),pout(y)) # label(congruence).
35.34/20.36	->(pin(a),pout(b)) # label(replacement).
35.34/20.36	->(pin(b),pout(c)) # label(replacement).
35.34/20.36	->(tc(x),x) # label(replacement).
35.34/20.36	-->*(pin(x),pout(z)) | -->*(tc(z),y) | ->(tc(x),y) # label(replacement).
35.34/20.36	->*(x,x) # label(reflexivity).
35.34/20.36	-->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity).
35.34/20.36	-->*(pin(x),pout(z)) | -->*(tc(z),y) # label(goal).
35.34/20.36	end_of_list.
35.34/20.36	
35.34/20.36	============================== end of clauses for search =============
35.34/20.36	
35.34/20.36	% There are no natural numbers in the input.
35.34/20.36	
35.34/20.36	============================== DOMAIN SIZE 2 =========================
35.34/20.36	
35.34/20.36	============================== MODEL =================================
35.34/20.36	
35.34/20.36	interpretation( 2, [number=1, seconds=0], [
35.34/20.36	
35.34/20.36	        function(a, [ 0 ]),
35.34/20.36	
35.34/20.36	        function(b, [ 0 ]),
35.34/20.36	
35.34/20.36	        function(c, [ 0 ]),
35.34/20.36	
35.34/20.36	        function(z, [ 1 ]),
35.34/20.36	
35.34/20.36	        function(pin(_), [ 0, 0 ]),
35.34/20.36	
35.34/20.36	        function(tc(_), [ 0, 1 ]),
35.34/20.36	
35.34/20.36	        function(pout(_), [ 0, 1 ]),
35.34/20.36	
35.34/20.36	        relation(->*(_,_), [
35.34/20.36				   1, 0,
35.34/20.36				   0, 1 ]),
35.34/20.36	
35.34/20.36	        relation(->(_,_), [
35.34/20.36				   1, 0,
35.34/20.36				   0, 1 ])
35.34/20.36	]).
35.34/20.36	
35.34/20.36	============================== end of model ==========================
35.34/20.36	
35.34/20.36	============================== STATISTICS ============================
35.34/20.36	
35.34/20.36	For domain size 2.
35.34/20.36	
35.34/20.36	Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
35.34/20.36	Ground clauses: seen=34, kept=30.
35.34/20.36	Selections=13, assignments=18, propagations=30, current_models=1.
35.34/20.36	Rewrite_terms=241, rewrite_bools=139, indexes=109.
35.34/20.36	Rules_from_neg_clauses=6, cross_offs=6.
35.34/20.36	
35.34/20.36	============================== end of statistics =====================
35.41/20.36	
35.41/20.36	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
35.41/20.36	
35.41/20.36	Exiting with 1 model.
35.41/20.36	
35.41/20.36	Process 49073 exit (max_models) Wed Jul 13 08:11:14 2022
35.41/20.36	The process finished Wed Jul 13 08:11:14 2022
35.41/20.36	
35.41/20.36	
35.41/20.36	Mace4 cooked interpretation:
35.41/20.36	
35.41/20.36	% number = 1
35.41/20.36	% seconds = 0
35.41/20.36	
35.41/20.36	% Interpretation of size 2
35.41/20.36	
35.41/20.36	a = 0.
35.41/20.36	
35.41/20.36	b = 0.
35.41/20.36	
35.41/20.36	c = 0.
35.41/20.36	
35.41/20.36	z = 1.
35.41/20.36	
35.41/20.36	pin(0) = 0.
35.41/20.36	pin(1) = 0.
35.41/20.36	
35.41/20.36	tc(0) = 0.
35.41/20.36	tc(1) = 1.
35.41/20.36	
35.41/20.36	pout(0) = 0.
35.41/20.36	pout(1) = 1.
35.41/20.36	
35.41/20.36	  ->*(0,0).
35.41/20.36	- ->*(0,1).
35.41/20.36	- ->*(1,0).
35.41/20.36	  ->*(1,1).
35.41/20.36	
35.41/20.36	  ->(0,0).
35.41/20.36	- ->(0,1).
35.41/20.36	- ->(1,0).
35.41/20.36	  ->(1,1).
35.41/20.36	
35.41/20.36	
35.41/20.36	The problem is infeasible.
35.41/20.36	EOF