71.19/50.60	NO
71.19/50.60	
71.19/50.60	Problem 1: 
71.19/50.60	
71.19/50.60	
71.19/50.60	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
71.19/50.60	Confluence Problem:
71.19/50.60	(VAR x)
71.19/50.60	(REPLACEMENT-MAP
71.19/50.60	(p 1)
71.19/50.60	(q 1)
71.19/50.60	(r 1)
71.19/50.60	(s 1)
71.19/50.60	(0)
71.19/50.60	(1)
71.19/50.60	(h 1)
71.19/50.60	)
71.19/50.60	(RULES
71.19/50.60	p(q(x)) -> p(r(x))
71.19/50.60	q(h(x)) -> r(x)
71.19/50.60	r(x) -> r(h(x)) | s(x) ->* 0
71.19/50.60	s(x) -> 1
71.19/50.60	)
71.19/50.60	
71.19/50.60	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
71.19/50.60	
71.19/50.60	
71.19/50.60	Problem 1: 
71.19/50.60	
71.19/50.60	Problem 1: 
71.19/50.60	
71.19/50.60	Clean CTRS Procedure:
71.19/50.60	
71.19/50.60	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
71.19/50.60	Confluence Problem:
71.19/50.60	(VAR x)
71.19/50.60	(REPLACEMENT-MAP
71.19/50.60	(p 1)
71.19/50.60	(q 1)
71.19/50.60	(r 1)
71.19/50.60	(s 1)
71.19/50.60	(0)
71.19/50.60	(1)
71.19/50.60	(h 1)
71.19/50.60	)
71.19/50.60	(RULES
71.19/50.60	p(q(x)) -> p(r(x))
71.19/50.60	q(h(x)) -> r(x)
71.19/50.60	r(x) -> r(h(x)) | s(x) ->* 0
71.19/50.60	s(x) -> 1
71.19/50.60	)
71.19/50.60	
71.19/50.60	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
71.19/50.60	
71.19/50.60	CRule InfChecker Info:
71.19/50.60	p(q(x)) -> p(r(x))
71.19/50.60	Rule remains
71.19/50.60	Proof:
71.19/50.60	NO_CONDS
71.19/50.60	
71.19/50.60	CRule InfChecker Info:
71.19/50.60	q(h(x)) -> r(x)
71.19/50.60	Rule remains
71.19/50.60	Proof:
71.19/50.60	NO_CONDS
71.19/50.60	
71.19/50.60	CRule InfChecker Info:
71.19/50.60	r(x) -> r(h(x)) | s(x) ->* 0
71.19/50.60	Rule remains
71.19/50.60	Proof:
71.19/50.60	HAS_EQUATIONAL_CONDS
71.19/50.60	
71.19/50.60	CRule InfChecker Info:
71.19/50.60	s(x) -> 1
71.19/50.60	Rule remains
71.19/50.60	Proof:
71.19/50.60	NO_CONDS
71.19/50.60	
71.19/50.60	Problem 1: 
71.19/50.60	
71.19/50.60	Problem 1: 
71.19/50.60	
71.19/50.60	Problem 1: 
71.19/50.60	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
71.19/50.60	Confluence Problem:
71.19/50.60	(VAR x)
71.19/50.60	(REPLACEMENT-MAP
71.19/50.60	(p 1)
71.19/50.60	(q 1)
71.19/50.60	(r 1)
71.19/50.60	(s 1)
71.19/50.60	(0)
71.19/50.60	(1)
71.19/50.60	(h 1)
71.19/50.60	)
71.19/50.60	(RULES
71.19/50.60	p(q(x)) -> p(r(x))
71.19/50.60	q(h(x)) -> r(x)
71.19/50.60	r(x) -> r(h(x)) | s(x) ->* 0
71.19/50.60	s(x) -> 1
71.19/50.60	)
71.19/50.60	
71.19/50.60	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
71.19/50.60	
71.19/50.60	Critical Pairs CProcedure:
71.19/50.60	-> Rules:
71.19/50.60	p(q(x)) -> p(r(x))
71.19/50.60	q(h(x)) -> r(x)
71.19/50.60	r(x) -> r(h(x)) | s(x) ->* 0
71.19/50.60	s(x) -> 1
71.19/50.60	-> Vars:
71.19/50.60	"x"
71.19/50.60	
71.19/50.60	-> Rlps:
71.19/50.60	crule: p(q(x)) -> p(r(x)), id: 1, possubterms: p(q(x))-> [], q(x)-> [1]
71.19/50.60	crule: q(h(x)) -> r(x), id: 2, possubterms: q(h(x))-> [], h(x)-> [1]
71.19/50.60	crule: r(x) -> r(h(x)) | s(x) ->* 0, id: 3, possubterms: r(x)-> []
71.19/50.60	crule: s(x) -> 1, id: 4, possubterms: s(x)-> []
71.19/50.60	
71.19/50.60	-> Unifications:
71.19/50.60	R1 unifies with  R2 at  p: [1], l: p(q(x)), lp: q(x), conds: {}, sig: {x -> h(x')}, l': q(h(x')), r: p(r(x)), r': r(x')
71.19/50.60	
71.19/50.60	-> Critical pairs info:
71.19/50.60	<p(r(x')),p(r(h(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N1
71.19/50.60	
71.19/50.60	-> Problem conclusions:
71.19/50.60	 Left linear, Right linear, Linear, Weakly left-Linear
71.19/50.60	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal, Not strongly orthogonal
71.19/50.60	 CTRS Type: 1
71.19/50.60	 Deterministic, Strongly deterministic
71.19/50.60	 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS
71.19/50.60	 Maybe right-stable CTRS, Not overlay CTRS
71.19/50.60	 Maybe normal CTRS, Maybe almost normal CTRS
71.19/50.60	 ECCPs not considered
71.19/50.60	 Maybe terminating CTRS, Maybe operational terminating CTRS
71.19/50.60	 Maybe joinable CCPs
71.19/50.60	 Maybe level confluent, Maybe confluent
71.19/50.60	
71.19/50.60	Problem 1: 
71.19/50.60	
71.19/50.60	Problem 1: 
71.19/50.60	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
71.19/50.60	Confluence Problem:
71.19/50.60	(VAR x x')
71.19/50.60	(REPLACEMENT-MAP
71.19/50.60	(p 1)
71.19/50.60	(q 1)
71.19/50.60	(r 1)
71.19/50.60	(s 1)
71.19/50.60	(0)
71.19/50.60	(1)
71.19/50.60	(h 1)
71.19/50.60	)
71.19/50.60	(RULES
71.19/50.60	p(q(x)) -> p(r(x))
71.19/50.60	q(h(x)) -> r(x)
71.19/50.60	r(x) -> r(h(x)) | s(x) ->* 0
71.19/50.60	s(x) -> 1
71.19/50.60	)
71.19/50.60	
71.19/50.60	Critical Pairs:
71.19/50.60	<p(r(x')),p(r(h(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N1
71.19/50.60	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
71.19/50.60	
71.19/50.60	Conditional Critical Pairs Distributor Procedure
71.19/50.60	
71.19/50.60	Problem 1: 
71.19/50.60	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
71.19/50.60	Confluence Problem:
71.19/50.60	(VAR x x')
71.19/50.60	(REPLACEMENT-MAP
71.19/50.60	(p 1)
71.19/50.60	(q 1)
71.19/50.60	(r 1)
71.19/50.60	(s 1)
71.19/50.60	(0)
71.19/50.60	(1)
71.19/50.60	(h 1)
71.19/50.60	)
71.19/50.60	(RULES
71.19/50.60	p(q(x)) -> p(r(x))
71.19/50.60	q(h(x)) -> r(x)
71.19/50.60	r(x) -> r(h(x)) | s(x) ->* 0
71.19/50.60	s(x) -> 1
71.19/50.60	)
71.19/50.60	
71.19/50.60	Critical Pairs:
71.19/50.60	<p(r(x')),p(r(h(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N1
71.19/50.60	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
71.19/50.60	
71.19/50.60	Infeasible Convergence No Conditions CCP Procedure:
71.19/50.60	Infeasible convergence?
71.19/50.60	YES
71.19/50.60	
71.19/50.60	Problem 1: 
71.19/50.60	
71.19/50.60	Infeasibility Problem:
71.19/50.60	[(VAR vNonEmpty x xap vNonEmpty x xap z0)
71.19/50.60	(STRATEGY CONTEXTSENSITIVE
71.19/50.60	(p 1)
71.19/50.60	(q 1)
71.19/50.60	(r 1)
71.19/50.60	(s 1)
71.19/50.60	(0)
71.19/50.60	(1)
71.19/50.60	(c_xap)
71.19/50.60	(fSNonEmpty)
71.19/50.60	(h 1)
71.19/50.60	)
71.19/50.60	(RULES
71.19/50.60	p(q(x)) -> p(r(x))
71.19/50.60	q(h(x)) -> r(x)
71.19/50.60	r(x) -> r(h(x)) | s(x) ->* 0
71.19/50.60	s(x) -> 1
71.19/50.60	)
71.19/50.60	]
71.19/50.60	
71.19/50.60	Infeasibility Conditions:
71.19/50.60	p(r(c_xap)) ->* z0, p(r(h(c_xap))) ->* z0
71.19/50.60	
71.19/50.60	Problem 1: 
71.19/50.60	
71.19/50.60	Obtaining a model using Mace4:
71.19/50.60	
71.19/50.60	 -> Usable Rules:
71.19/50.60	p(q(x)) -> p(r(x))
71.19/50.60	r(x) -> r(h(x)) | s(x) ->* 0
71.19/50.60	s(x) -> 1
71.19/50.60	
71.19/50.60	 -> Mace4 Output:
71.19/50.60	============================== Mace4 =================================
71.19/50.60	Mace4 (64) version 2009-11A, November 2009.
71.19/50.60	Process 26833 was started by sandbox on z035.star.cs.uiowa.edu,
71.19/50.60	Tue Aug  1 07:34:01 2023
71.19/50.60	The command was "./mace4 -c -f /tmp/mace426821.in".
71.19/50.60	============================== end of head ===========================
71.19/50.60	
71.19/50.60	============================== INPUT =================================
71.19/50.60	
71.19/50.60	% Reading from file /tmp/mace426821.in
71.19/50.60	
71.19/50.60	assign(max_seconds,40).
71.19/50.60	
71.19/50.60	formulas(assumptions).
71.19/50.60	->(x1,y) -> ->(p(x1),p(y)) # label(congruence).
71.19/50.60	->(x1,y) -> ->(q(x1),q(y)) # label(congruence).
71.19/50.60	->(x1,y) -> ->(r(x1),r(y)) # label(congruence).
71.19/50.60	->(x1,y) -> ->(s(x1),s(y)) # label(congruence).
71.19/50.60	->(x1,y) -> ->(h(x1),h(y)) # label(congruence).
71.19/50.60	->(p(q(x1)),p(r(x1))) # label(replacement).
71.19/50.60	->*(s(x1),0) -> ->(r(x1),r(h(x1))) # label(replacement).
71.19/50.60	->(s(x1),1) # label(replacement).
71.19/50.60	->*(x,x) # label(reflexivity).
71.19/50.60	->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity).
71.19/50.60	end_of_list.
71.19/50.60	
71.19/50.60	formulas(goals).
71.19/50.60	(exists x6 (->*(p(r(c_xap)),x6) & ->*(p(r(h(c_xap))),x6))) # label(goal).
71.19/50.60	end_of_list.
71.19/50.60	
71.19/50.60	============================== end of input ==========================
71.19/50.60	
71.19/50.60	============================== PROCESS NON-CLAUSAL FORMULAS ==========
71.19/50.60	
71.19/50.60	% Formulas that are not ordinary clauses:
71.19/50.60	1 ->(x1,y) -> ->(p(x1),p(y)) # label(congruence) # label(non_clause).  [assumption].
71.19/50.60	2 ->(x1,y) -> ->(q(x1),q(y)) # label(congruence) # label(non_clause).  [assumption].
71.19/50.60	3 ->(x1,y) -> ->(r(x1),r(y)) # label(congruence) # label(non_clause).  [assumption].
71.19/50.60	4 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
71.19/50.60	5 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause).  [assumption].
71.19/50.60	6 ->*(s(x1),0) -> ->(r(x1),r(h(x1))) # label(replacement) # label(non_clause).  [assumption].
71.19/50.60	7 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause).  [assumption].
71.19/50.60	8 (exists x6 (->*(p(r(c_xap)),x6) & ->*(p(r(h(c_xap))),x6))) # label(goal) # label(non_clause) # label(goal).  [goal].
71.19/50.60	
71.19/50.60	============================== end of process non-clausal formulas ===
71.19/50.60	
71.19/50.60	============================== CLAUSES FOR SEARCH ====================
71.19/50.60	
71.19/50.60	formulas(mace4_clauses).
71.19/50.60	-->(x,y) | ->(p(x),p(y)) # label(congruence).
71.19/50.60	-->(x,y) | ->(q(x),q(y)) # label(congruence).
71.19/50.60	-->(x,y) | ->(r(x),r(y)) # label(congruence).
71.19/50.60	-->(x,y) | ->(s(x),s(y)) # label(congruence).
71.19/50.60	-->(x,y) | ->(h(x),h(y)) # label(congruence).
71.19/50.60	->(p(q(x)),p(r(x))) # label(replacement).
71.19/50.60	-->*(s(x),0) | ->(r(x),r(h(x))) # label(replacement).
71.19/50.60	->(s(x),1) # label(replacement).
71.19/50.60	->*(x,x) # label(reflexivity).
71.19/50.60	-->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity).
71.19/50.60	-->*(p(r(c_xap)),x) | -->*(p(r(h(c_xap))),x) # label(goal).
71.19/50.60	end_of_list.
71.19/50.60	
71.19/50.60	============================== end of clauses for search =============
71.19/50.60	
71.19/50.60	% There are no natural numbers in the input.
71.19/50.60	
71.19/50.60	============================== DOMAIN SIZE 2 =========================
71.19/50.60	
71.19/50.60	============================== MODEL =================================
71.19/50.60	
71.19/50.60	interpretation( 2, [number=1, seconds=0], [
71.19/50.60	
71.19/50.60	        function(0, [ 0 ]),
71.19/50.60	
71.19/50.60	        function(1, [ 1 ]),
71.19/50.60	
71.19/50.60	        function(c_xap, [ 0 ]),
71.19/50.60	
71.19/50.60	        function(h(_), [ 1, 0 ]),
71.19/50.60	
71.19/50.60	        function(p(_), [ 0, 1 ]),
71.19/50.60	
71.19/50.60	        function(q(_), [ 0, 1 ]),
71.19/50.60	
71.19/50.60	        function(r(_), [ 0, 1 ]),
71.19/50.60	
71.19/50.60	        function(s(_), [ 1, 1 ]),
71.19/50.60	
71.19/50.60	        relation(->*(_,_), [
71.19/50.60				   1, 0,
71.19/50.60				   0, 1 ]),
71.19/50.60	
71.19/50.60	        relation(->(_,_), [
71.19/50.60				   1, 0,
71.19/50.60				   0, 1 ])
71.19/50.60	]).
71.19/50.60	
71.19/50.60	============================== end of model ==========================
71.19/50.60	
71.19/50.60	============================== STATISTICS ============================
71.19/50.60	
71.19/50.60	For domain size 2.
71.19/50.60	
71.19/50.60	Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
71.19/50.60	Ground clauses: seen=38, kept=34.
71.19/50.60	Selections=946, assignments=1886, propagations=721, current_models=1.
71.19/50.60	Rewrite_terms=10715, rewrite_bools=6855, indexes=1756.
71.19/50.60	Rules_from_neg_clauses=69, cross_offs=69.
71.19/50.60	
71.19/50.60	============================== end of statistics =====================
71.19/50.60	
71.19/50.60	User_CPU=0.01, System_CPU=0.00, Wall_clock=0.
71.19/50.60	
71.19/50.60	Exiting with 1 model.
71.19/50.60	
71.19/50.60	Process 26833 exit (max_models) Tue Aug  1 07:34:01 2023
71.19/50.60	The process finished Tue Aug  1 07:34:01 2023
71.19/50.60	
71.19/50.60	
71.19/50.60	Mace4 cooked interpretation:
71.19/50.60	
71.19/50.60	% number = 1
71.19/50.60	% seconds = 0
71.19/50.60	
71.19/50.60	% Interpretation of size 2
71.19/50.60	
71.19/50.60	0 = 0.
71.19/50.60	
71.19/50.60	1 = 1.
71.19/50.60	
71.19/50.60	c_xap = 0.
71.19/50.60	
71.19/50.60	h(0) = 1.
71.19/50.60	h(1) = 0.
71.19/50.60	
71.19/50.60	p(0) = 0.
71.19/50.60	p(1) = 1.
71.19/50.60	
71.19/50.60	q(0) = 0.
71.19/50.60	q(1) = 1.
71.19/50.60	
71.19/50.60	r(0) = 0.
71.19/50.60	r(1) = 1.
71.19/50.60	
71.19/50.60	s(0) = 1.
71.19/50.60	s(1) = 1.
71.19/50.60	
71.19/50.60	  ->*(0,0).
71.19/50.60	- ->*(0,1).
71.19/50.60	- ->*(1,0).
71.19/50.60	  ->*(1,1).
71.19/50.60	
71.19/50.60	  ->(0,0).
71.19/50.60	- ->(0,1).
71.19/50.60	- ->(1,0).
71.19/50.60	  ->(1,1).
71.19/50.60	
71.19/50.60	
71.19/50.60	The problem is infeasible.
71.19/50.60	
71.19/50.60	
71.19/50.60	The problem is not confluent.
71.19/50.60	EOF