32.78/20.29	YES
32.78/20.29	
32.78/20.29	Problem 1: 
32.78/20.29	
32.78/20.29	Infeasibility Problem:
32.78/20.29	[(VAR vNonEmpty x y z vNonEmpty y x1)
32.78/20.29	(STRATEGY CONTEXTSENSITIVE
32.78/20.29	(f 1 2)
32.78/20.29	(h 1)
32.78/20.29	(a 1)
32.78/20.29	(b)
32.78/20.29	(c 1)
32.78/20.29	(fSNonEmpty)
32.78/20.29	)
32.78/20.29	(RULES
32.78/20.29	f(c(c(c(x))),y) -> a(y) | c(f(c(x),c(c(y)))) ->* c(a(a(b)))
32.78/20.29	f(c(x),c(c(y))) -> a(a(x)) | c(f(x,y)) ->* c(a(b))
32.78/20.29	h(a(a(x))) -> a(b) | h(x) ->* b
32.78/20.29	h(b) -> b
32.78/20.29	)]
32.78/20.29	
32.78/20.29	Infeasibility Conditions:
32.78/20.29	c(f(c(c(x1)),y)) ->* c(a(b)), c(f(c(x1),c(c(c(c(y)))))) ->* c(a(a(b)))
32.78/20.29	
32.78/20.29	Problem 1: 
32.78/20.29	
32.78/20.29	Obtaining a model using Mace4:
32.78/20.29	
32.78/20.29	 -> Usable Rules:
32.78/20.29	f(c(c(c(x))),y) -> a(y) | c(f(c(x),c(c(y)))) ->* c(a(a(b)))
32.78/20.29	f(c(x),c(c(y))) -> a(a(x)) | c(f(x,y)) ->* c(a(b))
32.78/20.29	h(a(a(x))) -> a(b) | h(x) ->* b
32.78/20.29	h(b) -> b
32.78/20.29	
32.78/20.29	 -> Mace4 Output:
32.78/20.29	============================== Mace4 =================================
32.78/20.29	Mace4 (64) version 2009-11A, November 2009.
32.78/20.29	Process 30303 was started by sandbox on z022.star.cs.uiowa.edu,
32.78/20.29	Tue Aug  1 07:38:47 2023
32.78/20.29	The command was "./mace4 -c -f /tmp/mace430292.in".
32.78/20.29	============================== end of head ===========================
32.78/20.29	
32.78/20.29	============================== INPUT =================================
32.78/20.29	
32.78/20.29	% Reading from file /tmp/mace430292.in
32.78/20.29	
32.78/20.29	assign(max_seconds,100).
32.78/20.29	
32.78/20.29	formulas(assumptions).
32.78/20.29	->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence).
32.78/20.29	->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence).
32.78/20.29	->(x1,y) -> ->(h(x1),h(y)) # label(congruence).
32.78/20.29	->(x1,y) -> ->(a(x1),a(y)) # label(congruence).
32.78/20.29	->(x1,y) -> ->(c(x1),c(y)) # label(congruence).
32.78/20.29	->*(c(f(c(x1),c(c(x2)))),c(a(a(b)))) -> ->(f(c(c(c(x1))),x2),a(x2)) # label(replacement).
32.78/20.29	->*(c(f(x1,x2)),c(a(b))) -> ->(f(c(x1),c(c(x2))),a(a(x1))) # label(replacement).
32.78/20.29	->*(h(x1),b) -> ->(h(a(a(x1))),a(b)) # label(replacement).
32.78/20.29	->(h(b),b) # label(replacement).
32.78/20.29	->*(x,x) # label(reflexivity).
32.78/20.29	->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity).
32.78/20.29	end_of_list.
32.78/20.29	
32.78/20.29	formulas(goals).
32.78/20.29	(exists x5 exists x6 (->*(c(f(c(c(x6)),x5)),c(a(b))) & ->*(c(f(c(x6),c(c(c(c(x5)))))),c(a(a(b)))))) # label(goal).
32.78/20.29	end_of_list.
32.78/20.29	
32.78/20.29	============================== end of input ==========================
32.78/20.29	
32.78/20.29	============================== PROCESS NON-CLAUSAL FORMULAS ==========
32.78/20.29	
32.78/20.29	% Formulas that are not ordinary clauses:
32.78/20.29	1 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause).  [assumption].
32.78/20.29	2 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause).  [assumption].
32.78/20.29	3 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause).  [assumption].
32.78/20.29	4 ->(x1,y) -> ->(a(x1),a(y)) # label(congruence) # label(non_clause).  [assumption].
32.78/20.29	5 ->(x1,y) -> ->(c(x1),c(y)) # label(congruence) # label(non_clause).  [assumption].
32.78/20.29	6 ->*(c(f(c(x1),c(c(x2)))),c(a(a(b)))) -> ->(f(c(c(c(x1))),x2),a(x2)) # label(replacement) # label(non_clause).  [assumption].
32.78/20.29	7 ->*(c(f(x1,x2)),c(a(b))) -> ->(f(c(x1),c(c(x2))),a(a(x1))) # label(replacement) # label(non_clause).  [assumption].
32.78/20.29	8 ->*(h(x1),b) -> ->(h(a(a(x1))),a(b)) # label(replacement) # label(non_clause).  [assumption].
32.78/20.29	9 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause).  [assumption].
32.78/20.29	10 (exists x5 exists x6 (->*(c(f(c(c(x6)),x5)),c(a(b))) & ->*(c(f(c(x6),c(c(c(c(x5)))))),c(a(a(b)))))) # label(goal) # label(non_clause) # label(goal).  [goal].
32.78/20.29	
32.78/20.29	============================== end of process non-clausal formulas ===
32.78/20.29	
32.78/20.29	============================== CLAUSES FOR SEARCH ====================
32.78/20.29	
32.78/20.29	formulas(mace4_clauses).
32.78/20.29	-->(x,y) | ->(f(x,z),f(y,z)) # label(congruence).
32.78/20.29	-->(x,y) | ->(f(z,x),f(z,y)) # label(congruence).
32.78/20.29	-->(x,y) | ->(h(x),h(y)) # label(congruence).
32.78/20.29	-->(x,y) | ->(a(x),a(y)) # label(congruence).
32.78/20.29	-->(x,y) | ->(c(x),c(y)) # label(congruence).
32.78/20.29	-->*(c(f(c(x),c(c(y)))),c(a(a(b)))) | ->(f(c(c(c(x))),y),a(y)) # label(replacement).
32.78/20.29	-->*(c(f(x,y)),c(a(b))) | ->(f(c(x),c(c(y))),a(a(x))) # label(replacement).
32.78/20.29	-->*(h(x),b) | ->(h(a(a(x))),a(b)) # label(replacement).
32.78/20.29	->(h(b),b) # label(replacement).
32.78/20.29	->*(x,x) # label(reflexivity).
32.78/20.29	-->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity).
32.78/20.29	-->*(c(f(c(c(x)),y)),c(a(b))) | -->*(c(f(c(x),c(c(c(c(y)))))),c(a(a(b)))) # label(goal).
32.78/20.29	end_of_list.
32.78/20.29	
32.78/20.29	============================== end of clauses for search =============
32.78/20.29	
32.78/20.29	% There are no natural numbers in the input.
32.78/20.29	
32.78/20.29	============================== DOMAIN SIZE 2 =========================
32.78/20.29	
32.78/20.29	============================== MODEL =================================
32.78/20.29	
32.78/20.29	interpretation( 2, [number=1, seconds=0], [
32.78/20.29	
32.78/20.29	        function(b, [ 0 ]),
32.78/20.29	
32.78/20.29	        function(h(_), [ 0, 0 ]),
32.78/20.29	
32.78/20.29	        function(a(_), [ 0, 0 ]),
32.78/20.29	
32.78/20.29	        function(c(_), [ 0, 1 ]),
32.78/20.29	
32.78/20.29	        function(f(_,_), [
32.78/20.29				   1, 1,
32.78/20.29				   1, 1 ]),
32.78/20.29	
32.78/20.29	        relation(->*(_,_), [
32.78/20.29				   1, 0,
32.78/20.29				   0, 1 ]),
32.78/20.29	
32.78/20.29	        relation(->(_,_), [
32.78/20.29				   1, 0,
32.78/20.29				   0, 1 ])
32.78/20.29	]).
32.78/20.29	
32.78/20.29	============================== end of model ==========================
32.78/20.29	
32.78/20.29	============================== STATISTICS ============================
32.78/20.29	
32.78/20.29	For domain size 2.
32.78/20.29	
32.78/20.29	Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
32.78/20.29	Ground clauses: seen=53, kept=49.
32.78/20.29	Selections=13, assignments=18, propagations=7, current_models=1.
32.78/20.29	Rewrite_terms=280, rewrite_bools=95, indexes=87.
32.78/20.29	Rules_from_neg_clauses=0, cross_offs=0.
32.78/20.29	
32.78/20.29	============================== end of statistics =====================
32.78/20.29	
32.78/20.29	User_CPU=0.01, System_CPU=0.00, Wall_clock=0.
32.78/20.29	
32.78/20.29	Exiting with 1 model.
32.78/20.29	
32.78/20.29	Process 30303 exit (max_models) Tue Aug  1 07:38:47 2023
32.78/20.29	The process finished Tue Aug  1 07:38:47 2023
32.78/20.29	
32.78/20.29	
32.78/20.29	Mace4 cooked interpretation:
32.78/20.29	
32.78/20.29	% number = 1
32.78/20.29	% seconds = 0
32.78/20.29	
32.78/20.29	% Interpretation of size 2
32.78/20.29	
32.78/20.29	b = 0.
32.78/20.29	
32.78/20.29	h(0) = 0.
32.78/20.29	h(1) = 0.
32.78/20.29	
32.78/20.29	a(0) = 0.
32.78/20.29	a(1) = 0.
32.78/20.29	
32.78/20.29	c(0) = 0.
32.78/20.29	c(1) = 1.
32.78/20.29	
32.78/20.29	f(0,0) = 1.
32.78/20.29	f(0,1) = 1.
32.78/20.29	f(1,0) = 1.
32.78/20.29	f(1,1) = 1.
32.78/20.29	
32.78/20.29	  ->*(0,0).
32.78/20.29	- ->*(0,1).
32.78/20.29	- ->*(1,0).
32.78/20.29	  ->*(1,1).
32.78/20.29	
32.78/20.29	  ->(0,0).
32.78/20.29	- ->(0,1).
32.78/20.29	- ->(1,0).
32.78/20.29	  ->(1,1).
32.78/20.29	
32.78/20.29	
32.78/20.29	The problem is infeasible.
32.78/20.30	EOF