27.90/53.06	NO
27.90/53.06	
27.90/53.06	Problem 1: 
27.90/53.06	
27.90/53.06	
27.90/53.06	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
27.90/53.06	Confluence Problem:
27.90/53.06	(VAR x)
27.90/53.06	(REPLACEMENT-MAP
27.90/53.06	(a)
27.90/53.06	(c)
27.90/53.06	(f 1)
27.90/53.06	(h 1)
27.90/53.06	(b)
27.90/53.06	(g 1)
27.90/53.06	(k 1)
27.90/53.06	)
27.90/53.06	(RULES
27.90/53.06	a -> b
27.90/53.06	c -> k(f(a))
27.90/53.06	c -> k(g(b))
27.90/53.06	f(x) -> g(x) | h(f(x)) ->* k(g(b))
27.90/53.06	h(f(a)) -> c
27.90/53.06	h(x) -> k(x)
27.90/53.06	)
27.90/53.06	
27.90/53.06	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
27.90/53.06	
27.90/53.06	
27.90/53.06	Problem 1: 
27.90/53.06	
27.90/53.06	Problem 1: 
27.90/53.06	
27.90/53.06	Clean CTRS Procedure:
27.90/53.06	
27.90/53.06	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
27.90/53.06	Confluence Problem:
27.90/53.06	(VAR x)
27.90/53.06	(REPLACEMENT-MAP
27.90/53.06	(a)
27.90/53.06	(c)
27.90/53.06	(f 1)
27.90/53.06	(h 1)
27.90/53.06	(b)
27.90/53.06	(g 1)
27.90/53.06	(k 1)
27.90/53.06	)
27.90/53.06	(RULES
27.90/53.06	a -> b
27.90/53.06	c -> k(f(a))
27.90/53.06	c -> k(g(b))
27.90/53.06	f(x) -> g(x) | h(f(x)) ->* k(g(b))
27.90/53.06	h(f(a)) -> c
27.90/53.06	h(x) -> k(x)
27.90/53.06	)
27.90/53.06	
27.90/53.06	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
27.90/53.06	
27.90/53.06	CRule InfChecker Info:
27.90/53.06	a -> b
27.90/53.06	Rule remains
27.90/53.06	Proof:
27.90/53.06	NO_CONDS
27.90/53.06	
27.90/53.06	CRule InfChecker Info:
27.90/53.06	c -> k(f(a))
27.90/53.06	Rule remains
27.90/53.06	Proof:
27.90/53.06	NO_CONDS
27.90/53.06	
27.90/53.06	CRule InfChecker Info:
27.90/53.06	c -> k(g(b))
27.90/53.06	Rule remains
27.90/53.06	Proof:
27.90/53.06	NO_CONDS
27.90/53.06	
27.90/53.06	CRule InfChecker Info:
27.90/53.06	f(x) -> g(x) | h(f(x)) ->* k(g(b))
27.90/53.06	Rule remains
27.90/53.06	Proof:
27.90/53.06	HAS_EQUATIONAL_CONDS
27.90/53.06	
27.90/53.06	CRule InfChecker Info:
27.90/53.06	h(f(a)) -> c
27.90/53.06	Rule remains
27.90/53.06	Proof:
27.90/53.06	NO_CONDS
27.90/53.06	
27.90/53.06	CRule InfChecker Info:
27.90/53.06	h(x) -> k(x)
27.90/53.06	Rule remains
27.90/53.06	Proof:
27.90/53.06	NO_CONDS
27.90/53.06	
27.90/53.06	Problem 1: 
27.90/53.06	
27.90/53.06	Problem 1: 
27.90/53.06	
27.90/53.06	Problem 1: 
27.90/53.06	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
27.90/53.06	Confluence Problem:
27.90/53.06	(VAR x)
27.90/53.06	(REPLACEMENT-MAP
27.90/53.06	(a)
27.90/53.06	(c)
27.90/53.06	(f 1)
27.90/53.06	(h 1)
27.90/53.06	(b)
27.90/53.06	(g 1)
27.90/53.06	(k 1)
27.90/53.06	)
27.90/53.06	(RULES
27.90/53.06	a -> b
27.90/53.06	c -> k(f(a))
27.90/53.06	c -> k(g(b))
27.90/53.06	f(x) -> g(x) | h(f(x)) ->* k(g(b))
27.90/53.06	h(f(a)) -> c
27.90/53.06	h(x) -> k(x)
27.90/53.06	)
27.90/53.06	
27.90/53.06	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
27.90/53.06	
27.90/53.06	Critical Pairs CProcedure:
27.90/53.06	-> Rules:
27.90/53.06	a -> b
27.90/53.06	c -> k(f(a))
27.90/53.06	c -> k(g(b))
27.90/53.06	f(x) -> g(x) | h(f(x)) ->* k(g(b))
27.90/53.06	h(f(a)) -> c
27.90/53.06	h(x) -> k(x)
27.90/53.06	-> Vars:
27.90/53.06	"x"
27.90/53.06	
27.90/53.06	-> Rlps:
27.90/53.06	crule: a -> b, id: 1, possubterms: a-> []
27.90/53.06	crule: c -> k(f(a)), id: 2, possubterms: c-> []
27.90/53.06	crule: c -> k(g(b)), id: 3, possubterms: c-> []
27.90/53.06	crule: f(x) -> g(x) | h(f(x)) ->* k(g(b)), id: 4, possubterms: f(x)-> []
27.90/53.06	crule: h(f(a)) -> c, id: 5, possubterms: h(f(a))-> [], f(a)-> [1], a-> [1,1]
27.90/53.06	crule: h(x) -> k(x), id: 6, possubterms: h(x)-> []
27.90/53.06	
27.90/53.06	-> Unifications:
27.90/53.06	R3 unifies with  R2 at  p: [], l: c, lp: c, conds: {}, sig: {}, l': c, r: k(g(b)), r': k(f(a))
27.90/53.06	R5 unifies with  R4 at  p: [1], l: h(f(a)), lp: f(a), conds: {h(f(x)) ->* k(g(b))}, sig: {x -> a}, l': f(x), r: c, r': g(x)
27.90/53.06	R5 unifies with  R1 at  p: [1,1], l: h(f(a)), lp: a, conds: {}, sig: {}, l': a, r: c, r': b
27.90/53.06	R6 unifies with  R5 at  p: [], l: h(x), lp: h(x), conds: {}, sig: {x -> f(a)}, l': h(f(a)), r: k(x), r': c
27.90/53.06	
27.90/53.06	-> Critical pairs info:
27.90/53.06	<k(f(a)),k(g(b))>   =>  Not trivial, Overlay, Proper, NW1, N1
27.90/53.06	<h(f(b)),c>   =>  Not trivial, Not overlay, Proper, NW0, N2
27.90/53.06	<c,k(f(a))>   =>  Not trivial, Overlay, Proper, NW0, N3
27.90/53.06	<h(g(a)),c> | h(f(a)) ->* k(g(b))  =>  Not trivial, Not overlay, Proper, NW0, N4
27.90/53.06	
27.90/53.06	-> Problem conclusions:
27.90/53.06	 Left linear, Right linear, Linear, Weakly left-Linear
27.90/53.06	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal, Not strongly orthogonal
27.90/53.06	 CTRS Type: 1
27.90/53.06	 Deterministic, Strongly deterministic
27.90/53.06	 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS
27.90/53.06	 Maybe right-stable CTRS, Not overlay CTRS
27.90/53.06	 Maybe normal CTRS, Maybe almost normal CTRS
27.90/53.06	 ECCPs not considered
27.90/53.06	 Maybe terminating CTRS, Maybe operational terminating CTRS
27.90/53.06	 Maybe joinable CCPs
27.90/53.06	 Maybe level confluent, Maybe confluent
27.90/53.06	
27.90/53.06	Problem 1: 
27.90/53.06	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
27.90/53.06	Confluence Problem:
27.90/53.06	(VAR x)
27.90/53.06	(REPLACEMENT-MAP
27.90/53.06	(a)
27.90/53.06	(c)
27.90/53.06	(f 1)
27.90/53.06	(h 1)
27.90/53.06	(b)
27.90/53.06	(g 1)
27.90/53.06	(k 1)
27.90/53.06	)
27.90/53.06	(RULES
27.90/53.06	a -> b
27.90/53.06	c -> k(f(a))
27.90/53.06	c -> k(g(b))
27.90/53.06	f(x) -> g(x) | h(f(x)) ->* k(g(b))
27.90/53.06	h(f(a)) -> c
27.90/53.06	h(x) -> k(x)
27.90/53.06	)
27.90/53.06	
27.90/53.06	Critical Pairs:
27.90/53.06	<k(f(a)),k(g(b))>   =>  Not trivial, Overlay, Proper, NW1, N1
27.90/53.06	<h(f(b)),c>   =>  Not trivial, Not overlay, Proper, NW0, N2
27.90/53.06	<c,k(f(a))>   =>  Not trivial, Overlay, Proper, NW0, N3
27.90/53.06	<h(g(a)),c> | h(f(a)) ->* k(g(b))  =>  Not trivial, Not overlay, Proper, NW0, N4
27.90/53.06	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
27.90/53.06	
27.90/53.06	Improper Critical Pairs Procedure:
27.90/53.06	No iCCPs found
27.90/53.06	
27.90/53.06	Problem 1: 
27.90/53.06	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
27.90/53.06	Confluence Problem:
27.90/53.06	(VAR x)
27.90/53.06	(REPLACEMENT-MAP
27.90/53.06	(a)
27.90/53.06	(c)
27.90/53.06	(f 1)
27.90/53.06	(h 1)
27.90/53.06	(b)
27.90/53.06	(g 1)
27.90/53.06	(k 1)
27.90/53.06	)
27.90/53.06	(RULES
27.90/53.06	a -> b
27.90/53.06	c -> k(f(a))
27.90/53.06	c -> k(g(b))
27.90/53.06	f(x) -> g(x) | h(f(x)) ->* k(g(b))
27.90/53.06	h(f(a)) -> c
27.90/53.06	h(x) -> k(x)
27.90/53.06	)
27.90/53.06	
27.90/53.06	Critical Pairs:
27.90/53.06	<k(f(a)),k(g(b))>   =>  Not trivial, Overlay, Proper, NW1, N1
27.90/53.06	<h(f(b)),c>   =>  Not trivial, Not overlay, Proper, NW0, N2
27.90/53.06	<c,k(f(a))>   =>  Not trivial, Overlay, Proper, NW0, N3
27.90/53.06	<h(g(a)),c> | h(f(a)) ->* k(g(b))  =>  Not trivial, Not overlay, Proper, NW0, N4
27.90/53.06	
27.90/53.06	-> Problem conclusions:
27.90/53.06	 Left linear, Right linear, Linear, Weakly left-Linear
27.90/53.06	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal, Not strongly orthogonal
27.90/53.06	 CTRS Type: 1
27.90/53.06	 Deterministic, Strongly deterministic
27.90/53.06	 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS
27.90/53.06	 Maybe right-stable CTRS, Not overlay CTRS
27.90/53.06	 Maybe normal CTRS, Maybe almost normal CTRS
27.90/53.06	 ECCPs considered
27.90/53.06	 Maybe terminating CTRS, Maybe operational terminating CTRS
27.90/53.06	 Maybe joinable CCPs
27.90/53.06	 Maybe level confluent, Maybe confluent
27.90/53.06	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
27.90/53.06	
27.90/53.06	Conditional Variable Pairs Procedure:
27.90/53.06	->Conditional Variable Pair:
27.90/53.06	 Rule 4 (l :-> r | cds) => f(x) -> g(x) | h(f(x)) ->* k(g(b))
27.90/53.06	 Critical variable => x
27.90/53.06	 Critical variable' => x'
27.90/53.06	 Pos x in l => [1]
27.90/53.06	 s => f(x')
27.90/53.06	 t => g(x)
27.90/53.06	 C => x -> x', h(f(x)) ->* k(g(b))
27.90/53.06	 
27.90/53.06	
27.90/53.06	<f(x'),g(x)> | x -> x', h(f(x)) ->* k(g(b))  =>  Not trivial, Not overlay, CVP, NW0, N5
27.90/53.06	
27.90/53.06	-> Problem conclusions:
27.90/53.06	 Left linear, Right linear, Linear, Weakly left-Linear
27.90/53.06	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal, Not strongly orthogonal
27.90/53.06	 CTRS Type: 1
27.90/53.06	 Deterministic, Strongly deterministic
27.90/53.06	 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS
27.90/53.06	 Maybe right-stable CTRS, Not overlay CTRS
27.90/53.06	 Maybe normal CTRS, Maybe almost normal CTRS
27.90/53.06	 ECCPs considered
27.90/53.06	 Maybe terminating CTRS, Maybe operational terminating CTRS
27.90/53.06	 Maybe joinable CCPs
27.90/53.06	 Maybe level confluent, Maybe confluent
27.90/53.06	
27.90/53.06	Problem 1: 
27.90/53.06	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
27.90/53.06	Confluence Problem:
27.90/53.06	(VAR x x')
27.90/53.06	(REPLACEMENT-MAP
27.90/53.06	(a)
27.90/53.06	(c)
27.90/53.06	(f 1)
27.90/53.06	(h 1)
27.90/53.06	(b)
27.90/53.06	(g 1)
27.90/53.06	(k 1)
27.90/53.06	)
27.90/53.06	(RULES
27.90/53.06	a -> b
27.90/53.06	c -> k(f(a))
27.90/53.06	c -> k(g(b))
27.90/53.06	f(x) -> g(x) | h(f(x)) ->* k(g(b))
27.90/53.06	h(f(a)) -> c
27.90/53.06	h(x) -> k(x)
27.90/53.06	)
27.90/53.06	
27.90/53.06	Critical Pairs:
27.90/53.06	<f(x'),g(x)> | x -> x', h(f(x)) ->* k(g(b))  =>  Not trivial, Not overlay, CVP, NW0, N5
27.90/53.06	<k(f(a)),k(g(b))>   =>  Not trivial, Overlay, Proper, NW1, N1
27.90/53.06	<h(f(b)),c>   =>  Not trivial, Not overlay, Proper, NW0, N2
27.90/53.06	<c,k(f(a))>   =>  Not trivial, Overlay, Proper, NW0, N3
27.90/53.06	<h(g(a)),c> | h(f(a)) ->* k(g(b))  =>  Not trivial, Not overlay, Proper, NW0, N4
27.90/53.06	
27.90/53.06	-> Problem conclusions:
27.90/53.06	 Left linear, Right linear, Linear, Weakly left-Linear
27.90/53.06	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal, Not strongly orthogonal
27.90/53.06	 CTRS Type: 1
27.90/53.06	 Deterministic, Strongly deterministic
27.90/53.06	 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS
27.90/53.06	 Maybe right-stable CTRS, Not overlay CTRS
27.90/53.06	 Maybe normal CTRS, Maybe almost normal CTRS
27.90/53.06	 ECCPs considered
27.90/53.06	 Maybe terminating CTRS, Maybe operational terminating CTRS
27.90/53.06	 Maybe joinable CCPs
27.90/53.06	 Maybe level confluent, Maybe confluent
27.90/53.06	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
27.90/53.06	
27.90/53.06	Conditional Critical Pairs Distributor Procedure
27.90/53.06	
27.90/53.06	Problem 1: 
27.90/53.06	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
27.90/53.06	Confluence Problem:
27.90/53.06	(VAR x x')
27.90/53.06	(REPLACEMENT-MAP
27.90/53.06	(a)
27.90/53.06	(c)
27.90/53.06	(f 1)
27.90/53.06	(h 1)
27.90/53.06	(b)
27.90/53.06	(g 1)
27.90/53.06	(k 1)
27.90/53.06	)
27.90/53.06	(RULES
27.90/53.06	a -> b
27.90/53.06	c -> k(f(a))
27.90/53.06	c -> k(g(b))
27.90/53.06	f(x) -> g(x) | h(f(x)) ->* k(g(b))
27.90/53.06	h(f(a)) -> c
27.90/53.06	h(x) -> k(x)
27.90/53.06	)
27.90/53.06	
27.90/53.06	Critical Pairs:
27.90/53.06	<f(x'),g(x)> | x -> x', h(f(x)) ->* k(g(b))  =>  Not trivial, Not overlay, CVP, NW0, N5
27.90/53.06	
27.90/53.06	-> Problem conclusions:
27.90/53.06	 Left linear, Right linear, Linear, Weakly left-Linear
27.90/53.06	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal, Not strongly orthogonal
27.90/53.06	 CTRS Type: 1
27.90/53.06	 Deterministic, Strongly deterministic
27.90/53.06	 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS
27.90/53.06	 Maybe right-stable CTRS, Not overlay CTRS
27.90/53.06	 Maybe normal CTRS, Maybe almost normal CTRS
27.90/53.06	 ECCPs considered
27.90/53.06	 Maybe terminating CTRS, Maybe operational terminating CTRS
27.90/53.06	 Maybe joinable CCPs
27.90/53.06	 Maybe level confluent, Maybe confluent
27.90/53.06	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
27.90/53.06	
27.90/53.06	Infeasible Convergence Simple Substitution ECCP Procedure:
27.90/53.06	 
27.90/53.06	Simple Substitution: {x -> a, x' -> b} 
27.90/53.06	ECCP after substitution: <f(b),g(a)> | a -> b, h(f(a)) ->* k(g(b)) 
27.90/53.06	Try number: 1
27.90/53.06	
27.90/53.06	Infeasible conditions?
27.90/53.06	NO
27.90/53.06	
27.90/53.06	Problem 1: 
27.90/53.06	
27.90/53.06	Infeasibility Problem:
27.90/53.06	[(VAR vNonEmpty x xap vNonEmpty x xap)
27.90/53.06	(STRATEGY CONTEXTSENSITIVE
27.90/53.06	(a)
27.90/53.06	(c)
27.90/53.06	(f 1)
27.90/53.06	(h 1)
27.90/53.06	(b)
27.90/53.06	(fSNonEmpty)
27.90/53.06	(g 1)
27.90/53.06	(k 1)
27.90/53.06	)
27.90/53.06	(RULES
27.90/53.06	a -> b
27.90/53.06	c -> k(f(a))
27.90/53.06	c -> k(g(b))
27.90/53.06	f(x) -> g(x) | h(f(x)) ->* k(g(b))
27.90/53.06	h(f(a)) -> c
27.90/53.06	h(x) -> k(x)
27.90/53.06	)
27.90/53.06	]
27.90/53.06	
27.90/53.06	Infeasibility Conditions:
27.90/53.06	a -> b, h(f(a)) ->* k(g(b))
27.90/53.06	
27.90/53.06	Problem 1: 
27.90/53.06	
27.90/53.06	Obtaining a proof using Prover9:
27.90/53.06	
27.90/53.06	 -> Prover9 Output:
27.90/53.06	============================== Prover9 ===============================
27.90/53.06	Prover9 (64) version 2009-11A, November 2009.
27.90/53.06	Process 6581 was started by sandbox on z028.star.cs.uiowa.edu,
27.90/53.06	Tue Aug  1 07:33:45 2023
27.90/53.06	The command was "./prover9 -f /tmp/prover96556.in".
27.90/53.06	============================== end of head ===========================
27.90/53.06	
27.90/53.06	============================== INPUT =================================
27.90/53.06	
27.90/53.06	% Reading from file /tmp/prover96556.in
27.90/53.06	
27.90/53.06	assign(max_seconds,20).
27.90/53.06	
27.90/53.06	formulas(assumptions).
27.90/53.06	->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence).
27.90/53.06	->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence).
27.90/53.06	->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence).
27.90/53.06	->_s0(x1,y) -> ->_s0(k(x1),k(y)) # label(congruence).
27.90/53.06	->_s0(a,b) # label(replacement).
27.90/53.06	->_s0(c,k(f(a))) # label(replacement).
27.90/53.06	->_s0(c,k(g(b))) # label(replacement).
27.90/53.06	->*_s0(h(f(x1)),k(g(b))) -> ->_s0(f(x1),g(x1)) # label(replacement).
27.90/53.06	->_s0(h(f(a)),c) # label(replacement).
27.90/53.06	->_s0(h(x1),k(x1)) # label(replacement).
27.90/53.06	->*_s0(x,x) # label(reflexivity).
27.90/53.06	->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
27.90/53.06	end_of_list.
27.90/53.06	
27.90/53.06	formulas(goals).
27.90/53.06	->_s0(a,b) & ->*_s0(h(f(a)),k(g(b))) # label(goal).
27.90/53.06	end_of_list.
27.90/53.06	
27.90/53.06	============================== end of input ==========================
27.90/53.06	
27.90/53.06	============================== PROCESS NON-CLAUSAL FORMULAS ==========
27.90/53.06	
27.90/53.06	% Formulas that are not ordinary clauses:
27.90/53.06	1 ->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence) # label(non_clause).  [assumption].
27.90/53.06	2 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence) # label(non_clause).  [assumption].
27.90/53.06	3 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence) # label(non_clause).  [assumption].
27.90/53.06	4 ->_s0(x1,y) -> ->_s0(k(x1),k(y)) # label(congruence) # label(non_clause).  [assumption].
27.90/53.06	5 ->*_s0(h(f(x1)),k(g(b))) -> ->_s0(f(x1),g(x1)) # label(replacement) # label(non_clause).  [assumption].
27.90/53.06	6 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
27.90/53.06	7 ->_s0(a,b) & ->*_s0(h(f(a)),k(g(b))) # label(goal) # label(non_clause) # label(goal).  [goal].
27.90/53.06	
27.90/53.06	============================== end of process non-clausal formulas ===
27.90/53.06	
27.90/53.06	============================== PROCESS INITIAL CLAUSES ===============
27.90/53.06	
27.90/53.06	% Clauses before input processing:
27.90/53.06	
27.90/53.06	formulas(usable).
27.90/53.06	end_of_list.
27.90/53.06	
27.90/53.06	formulas(sos).
27.90/53.06	-->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence).  [clausify(1)].
27.90/53.06	-->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence).  [clausify(2)].
27.90/53.06	-->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence).  [clausify(3)].
27.90/53.06	-->_s0(x,y) | ->_s0(k(x),k(y)) # label(congruence).  [clausify(4)].
27.90/53.06	->_s0(a,b) # label(replacement).  [assumption].
27.90/53.06	->_s0(c,k(f(a))) # label(replacement).  [assumption].
27.90/53.06	->_s0(c,k(g(b))) # label(replacement).  [assumption].
27.90/53.06	-->*_s0(h(f(x)),k(g(b))) | ->_s0(f(x),g(x)) # label(replacement).  [clausify(5)].
27.90/53.06	->_s0(h(f(a)),c) # label(replacement).  [assumption].
27.90/53.06	->_s0(h(x),k(x)) # label(replacement).  [assumption].
27.90/53.06	->*_s0(x,x) # label(reflexivity).  [assumption].
27.90/53.06	-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(6)].
27.90/53.06	-->_s0(a,b) | -->*_s0(h(f(a)),k(g(b))) # label(goal).  [deny(7)].
27.90/53.06	end_of_list.
27.90/53.06	
27.90/53.06	formulas(demodulators).
27.90/53.06	end_of_list.
27.90/53.06	
27.90/53.06	============================== PREDICATE ELIMINATION =================
27.90/53.06	
27.90/53.06	No predicates eliminated.
27.90/53.06	
27.90/53.06	============================== end predicate elimination =============
27.90/53.06	
27.90/53.06	Auto_denials:
27.90/53.06	  % copying label goal to answer in negative clause
27.90/53.06	
27.90/53.06	Term ordering decisions:
27.90/53.06	Predicate symbol precedence:  predicate_order([ ->_s0, ->*_s0 ]).
27.90/53.06	Function symbol precedence:  function_order([ a, c, b, f, k, h, g ]).
27.90/53.06	After inverse_order:  (no changes).
27.90/53.06	Unfolding symbols: (none).
27.90/53.06	
27.90/53.06	Auto_inference settings:
27.90/53.06	  % set(neg_binary_resolution).  % (HNE depth_diff=-3)
27.90/53.06	  % clear(ordered_res).  % (HNE depth_diff=-3)
27.90/53.06	  % set(ur_resolution).  % (HNE depth_diff=-3)
27.90/53.06	    % set(ur_resolution) -> set(pos_ur_resolution).
27.90/53.06	    % set(ur_resolution) -> set(neg_ur_resolution).
27.90/53.06	
27.90/53.06	Auto_process settings:
27.90/53.06	  % set(unit_deletion).  % (Horn set with negative nonunits)
27.90/53.06	
27.90/53.06	kept:      8 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence).  [clausify(1)].
27.90/53.06	kept:      9 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence).  [clausify(2)].
27.90/53.06	kept:      10 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence).  [clausify(3)].
27.90/53.06	kept:      11 -->_s0(x,y) | ->_s0(k(x),k(y)) # label(congruence).  [clausify(4)].
27.90/53.06	kept:      12 ->_s0(a,b) # label(replacement).  [assumption].
27.90/53.06	kept:      13 ->_s0(c,k(f(a))) # label(replacement).  [assumption].
27.90/53.06	kept:      14 ->_s0(c,k(g(b))) # label(replacement).  [assumption].
27.90/53.06	kept:      15 -->*_s0(h(f(x)),k(g(b))) | ->_s0(f(x),g(x)) # label(replacement).  [clausify(5)].
27.90/53.06	kept:      16 ->_s0(h(f(a)),c) # label(replacement).  [assumption].
27.90/53.06	kept:      17 ->_s0(h(x),k(x)) # label(replacement).  [assumption].
27.90/53.06	kept:      18 ->*_s0(x,x) # label(reflexivity).  [assumption].
27.90/53.06	kept:      19 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(6)].
27.90/53.06	           20 -->_s0(a,b) | -->*_s0(h(f(a)),k(g(b))) # label(goal) # answer(goal).  [deny(7)].
27.90/53.06	kept:      21 -->*_s0(h(f(a)),k(g(b))) # answer(goal).  [copy(20),unit_del(a,12)].
27.90/53.06	
27.90/53.06	============================== end of process initial clauses ========
27.90/53.06	
27.90/53.06	============================== CLAUSES FOR SEARCH ====================
27.90/53.06	
27.90/53.06	% Clauses after input processing:
27.90/53.06	
27.90/53.06	formulas(usable).
27.90/53.06	end_of_list.
27.90/53.06	
27.90/53.06	formulas(sos).
27.90/53.06	8 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence).  [clausify(1)].
27.90/53.06	9 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence).  [clausify(2)].
27.90/53.06	10 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence).  [clausify(3)].
27.90/53.06	11 -->_s0(x,y) | ->_s0(k(x),k(y)) # label(congruence).  [clausify(4)].
27.90/53.06	12 ->_s0(a,b) # label(replacement).  [assumption].
27.90/53.06	13 ->_s0(c,k(f(a))) # label(replacement).  [assumption].
27.90/53.06	14 ->_s0(c,k(g(b))) # label(replacement).  [assumption].
27.90/53.06	15 -->*_s0(h(f(x)),k(g(b))) | ->_s0(f(x),g(x)) # label(replacement).  [clausify(5)].
27.90/53.06	16 ->_s0(h(f(a)),c) # label(replacement).  [assumption].
27.90/53.06	17 ->_s0(h(x),k(x)) # label(replacement).  [assumption].
27.90/53.06	18 ->*_s0(x,x) # label(reflexivity).  [assumption].
27.90/53.06	19 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(6)].
27.90/53.06	21 -->*_s0(h(f(a)),k(g(b))) # answer(goal).  [copy(20),unit_del(a,12)].
27.90/53.06	end_of_list.
27.90/53.06	
27.90/53.06	formulas(demodulators).
27.90/53.06	end_of_list.
27.90/53.06	
27.90/53.06	============================== end of clauses for search =============
27.90/53.06	
27.90/53.06	============================== SEARCH ================================
27.90/53.06	
27.90/53.06	% Starting search at 0.00 seconds.
27.90/53.06	
27.90/53.06	given #1 (I,wt=8): 8 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence).  [clausify(1)].
27.90/53.06	
27.90/53.06	given #2 (I,wt=8): 9 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence).  [clausify(2)].
27.90/53.06	
27.90/53.06	given #3 (I,wt=8): 10 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence).  [clausify(3)].
27.90/53.06	
27.90/53.06	given #4 (I,wt=8): 11 -->_s0(x,y) | ->_s0(k(x),k(y)) # label(congruence).  [clausify(4)].
27.90/53.06	
27.90/53.06	given #5 (I,wt=3): 12 ->_s0(a,b) # label(replacement).  [assumption].
27.90/53.06	
27.90/53.06	given #6 (I,wt=5): 13 ->_s0(c,k(f(a))) # label(replacement).  [assumption].
27.90/53.06	
27.90/53.06	given #7 (I,wt=5): 14 ->_s0(c,k(g(b))) # label(replacement).  [assumption].
27.90/53.06	
27.90/53.06	given #8 (I,wt=12): 15 -->*_s0(h(f(x)),k(g(b))) | ->_s0(f(x),g(x)) # label(replacement).  [clausify(5)].
27.90/53.06	
27.90/53.06	given #9 (I,wt=5): 16 ->_s0(h(f(a)),c) # label(replacement).  [assumption].
27.90/53.06	
27.90/53.06	given #10 (I,wt=5): 17 ->_s0(h(x),k(x)) # label(replacement).  [assumption].
27.90/53.06	
27.90/53.06	given #11 (I,wt=3): 18 ->*_s0(x,x) # label(reflexivity).  [assumption].
27.90/53.06	
27.90/53.06	given #12 (I,wt=9): 19 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(6)].
27.90/53.06	
27.90/53.06	given #13 (I,wt=7): 21 -->*_s0(h(f(a)),k(g(b))) # answer(goal).  [copy(20),unit_del(a,12)].
27.90/53.06	
27.90/53.06	============================== PROOF =================================
27.90/53.06	
27.90/53.06	% Proof 1 at 0.00 (+ 0.00) seconds: goal.
27.90/53.06	% Length of proof is 11.
27.90/53.06	% Level of proof is 3.
27.90/53.06	% Maximum clause weight is 9.000.
27.90/53.06	% Given clauses 13.
27.90/53.06	
27.90/53.06	6 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
27.90/53.06	7 ->_s0(a,b) & ->*_s0(h(f(a)),k(g(b))) # label(goal) # label(non_clause) # label(goal).  [goal].
27.90/53.06	12 ->_s0(a,b) # label(replacement).  [assumption].
27.90/53.06	14 ->_s0(c,k(g(b))) # label(replacement).  [assumption].
27.90/53.06	16 ->_s0(h(f(a)),c) # label(replacement).  [assumption].
27.90/53.06	18 ->*_s0(x,x) # label(reflexivity).  [assumption].
27.90/53.06	19 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(6)].
27.90/53.06	20 -->_s0(a,b) | -->*_s0(h(f(a)),k(g(b))) # label(goal) # answer(goal).  [deny(7)].
27.90/53.06	21 -->*_s0(h(f(a)),k(g(b))) # answer(goal).  [copy(20),unit_del(a,12)].
27.90/53.06	44 ->*_s0(c,k(g(b))).  [ur(19,a,14,a,b,18,a)].
27.90/53.06	50 $F # answer(goal).  [ur(19,a,16,a,c,21,a),unit_del(a,44)].
27.90/53.06	
27.90/53.06	============================== end of proof ==========================
27.90/53.06	
27.90/53.06	============================== STATISTICS ============================
27.90/53.06	
27.90/53.06	Given=13. Generated=42. Kept=41. proofs=1.
27.90/53.06	Usable=13. Sos=25. Demods=0. Limbo=3, Disabled=13. Hints=0.
27.90/53.06	Kept_by_rule=0, Deleted_by_rule=0.
27.90/53.06	Forward_subsumed=0. Back_subsumed=0.
27.90/53.06	Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
27.90/53.06	New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
27.90/53.06	Demod_attempts=0. Demod_rewrites=0.
27.90/53.06	Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
27.90/53.06	Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=7.
27.90/53.06	Megabytes=0.10.
27.90/53.06	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
27.90/53.06	
27.90/53.06	============================== end of statistics =====================
27.90/53.06	
27.90/53.06	============================== end of search =========================
27.90/53.06	
27.90/53.06	THEOREM PROVED
27.90/53.06	
27.90/53.06	Exiting with 1 proof.
27.90/53.06	
27.90/53.06	Process 6581 exit (max_proofs) Tue Aug  1 07:33:45 2023
27.90/53.06	
27.90/53.06	
27.90/53.06	The problem is feasible.
27.90/53.06	
27.90/53.06	
27.90/53.06	Infeasible ECCP convergence?
27.90/53.06	YES
27.90/53.06	
27.90/53.06	Problem 1: 
27.90/53.06	
27.90/53.06	Infeasibility Problem:
27.90/53.06	[(VAR vNonEmpty x xap vNonEmpty x xap z0)
27.90/53.06	(STRATEGY CONTEXTSENSITIVE
27.90/53.06	(a)
27.90/53.06	(c)
27.90/53.06	(f 1)
27.90/53.06	(h 1)
27.90/53.06	(b)
27.90/53.06	(fSNonEmpty)
27.90/53.06	(g 1)
27.90/53.06	(k 1)
27.90/53.06	)
27.90/53.06	(RULES
27.90/53.06	a -> b
27.90/53.06	c -> k(f(a))
27.90/53.06	c -> k(g(b))
27.90/53.06	f(x) -> g(x) | h(f(x)) ->* k(g(b))
27.90/53.06	h(f(a)) -> c
27.90/53.06	h(x) -> k(x)
27.90/53.06	)
27.90/53.06	]
27.90/53.06	
27.90/53.06	Infeasibility Conditions:
27.90/53.06	a -> b, h(f(a)) ->* k(g(b)), f(b) ->* z0, g(a) ->* z0
27.90/53.06	
27.90/53.06	Problem 1: 
27.90/53.06	
27.90/53.06	Obtaining a model using Mace4:
27.90/53.06	
27.90/53.06	 -> Usable Rules:
27.90/53.06	a -> b
27.90/53.06	c -> k(f(a))
27.90/53.06	c -> k(g(b))
27.90/53.06	f(x) -> g(x) | h(f(x)) ->* k(g(b))
27.90/53.06	h(f(a)) -> c
27.90/53.06	h(x) -> k(x)
27.90/53.06	
27.90/53.06	 -> Mace4 Output:
27.90/53.06	============================== Mace4 =================================
27.90/53.06	Mace4 (64) version 2009-11A, November 2009.
27.90/53.06	Process 6628 was started by sandbox on z028.star.cs.uiowa.edu,
27.90/53.06	Tue Aug  1 07:33:45 2023
27.90/53.06	The command was "./mace4 -c -f /tmp/mace46605.in".
27.90/53.06	============================== end of head ===========================
27.90/53.06	
27.90/53.06	============================== INPUT =================================
27.90/53.06	
27.90/53.06	% Reading from file /tmp/mace46605.in
27.90/53.06	
27.90/53.06	assign(max_seconds,40).
27.90/53.06	
27.90/53.06	formulas(assumptions).
27.90/53.06	->(x1,y) -> ->(f(x1),f(y)) # label(congruence).
27.90/53.06	->(x1,y) -> ->(h(x1),h(y)) # label(congruence).
27.90/53.06	->(x1,y) -> ->(g(x1),g(y)) # label(congruence).
27.90/53.06	->(x1,y) -> ->(k(x1),k(y)) # label(congruence).
27.90/53.06	->(a,b) # label(replacement).
27.90/53.06	->(c,k(f(a))) # label(replacement).
27.90/53.06	->(c,k(g(b))) # label(replacement).
27.90/53.06	->*(h(f(x1)),k(g(b))) -> ->(f(x1),g(x1)) # label(replacement).
27.90/53.06	->(h(f(a)),c) # label(replacement).
27.90/53.06	->(h(x1),k(x1)) # label(replacement).
27.90/53.06	->*(x,x) # label(reflexivity).
27.90/53.06	->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity).
27.90/53.06	end_of_list.
27.90/53.06	
27.90/53.06	formulas(goals).
27.90/53.06	(exists x6 (->(a,b) & ->*(h(f(a)),k(g(b))) & ->*(f(b),x6) & ->*(g(a),x6))) # label(goal).
27.90/53.06	end_of_list.
27.90/53.06	
27.90/53.06	============================== end of input ==========================
27.90/53.06	
27.90/53.06	============================== PROCESS NON-CLAUSAL FORMULAS ==========
27.90/53.06	
27.90/53.06	% Formulas that are not ordinary clauses:
27.90/53.06	1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause).  [assumption].
27.90/53.06	2 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause).  [assumption].
27.90/53.06	3 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence) # label(non_clause).  [assumption].
27.90/53.06	4 ->(x1,y) -> ->(k(x1),k(y)) # label(congruence) # label(non_clause).  [assumption].
27.90/53.06	5 ->*(h(f(x1)),k(g(b))) -> ->(f(x1),g(x1)) # label(replacement) # label(non_clause).  [assumption].
27.90/53.06	6 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause).  [assumption].
27.90/53.06	7 (exists x6 (->(a,b) & ->*(h(f(a)),k(g(b))) & ->*(f(b),x6) & ->*(g(a),x6))) # label(goal) # label(non_clause) # label(goal).  [goal].
27.90/53.06	
27.90/53.06	============================== end of process non-clausal formulas ===
27.90/53.06	
27.90/53.06	============================== CLAUSES FOR SEARCH ====================
27.90/53.06	
27.90/53.06	formulas(mace4_clauses).
27.90/53.06	-->(x,y) | ->(f(x),f(y)) # label(congruence).
27.90/53.06	-->(x,y) | ->(h(x),h(y)) # label(congruence).
27.90/53.06	-->(x,y) | ->(g(x),g(y)) # label(congruence).
27.90/53.06	-->(x,y) | ->(k(x),k(y)) # label(congruence).
27.90/53.06	->(a,b) # label(replacement).
27.90/53.06	->(c,k(f(a))) # label(replacement).
27.90/53.06	->(c,k(g(b))) # label(replacement).
27.90/53.06	-->*(h(f(x)),k(g(b))) | ->(f(x),g(x)) # label(replacement).
27.90/53.06	->(h(f(a)),c) # label(replacement).
27.90/53.06	->(h(x),k(x)) # label(replacement).
27.90/53.06	->*(x,x) # label(reflexivity).
27.90/53.06	-->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity).
27.90/53.06	-->(a,b) | -->*(h(f(a)),k(g(b))) | -->*(f(b),x) | -->*(g(a),x) # label(goal).
27.90/53.06	end_of_list.
27.90/53.06	
27.90/53.06	============================== end of clauses for search =============
27.90/53.06	
27.90/53.06	% There are no natural numbers in the input.
27.90/53.06	
27.90/53.06	============================== DOMAIN SIZE 2 =========================
27.90/53.06	
27.90/53.06	============================== STATISTICS ============================
27.90/53.06	
27.90/53.06	For domain size 2.
27.90/53.06	
27.90/53.06	Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
27.90/53.06	Ground clauses: seen=36, kept=32.
27.90/53.06	Selections=387, assignments=773, propagations=662, current_models=0.
27.90/53.06	Rewrite_terms=6764, rewrite_bools=4091, indexes=1450.
27.90/53.06	Rules_from_neg_clauses=226, cross_offs=226.
27.90/53.06	
27.90/53.06	============================== end of statistics =====================
27.90/53.06	
27.90/53.06	============================== DOMAIN SIZE 3 =========================
27.90/53.06	
27.90/53.06	============================== MODEL =================================
27.90/53.06	
27.90/53.06	interpretation( 3, [number=1, seconds=0], [
27.90/53.06	
27.90/53.06	        function(a, [ 0 ]),
27.90/53.06	
27.90/53.06	        function(c, [ 0 ]),
27.90/53.06	
27.90/53.06	        function(b, [ 1 ]),
27.90/53.06	
27.90/53.06	        function(f(_), [ 0, 2, 0 ]),
27.90/53.06	
27.90/53.06	        function(h(_), [ 0, 0, 1 ]),
27.90/53.06	
27.90/53.06	        function(g(_), [ 1, 1, 1 ]),
27.90/53.06	
27.90/53.06	        function(k(_), [ 0, 0, 1 ]),
27.90/53.06	
27.90/53.06	        relation(->*(_,_), [
27.90/53.06				   1, 1, 1,
27.90/53.06				   0, 1, 0,
27.90/53.06				   0, 0, 1 ]),
27.90/53.06	
27.90/53.06	        relation(->(_,_), [
27.90/53.06				   1, 1, 1,
27.90/53.06				   0, 1, 0,
27.90/53.06				   0, 0, 1 ])
27.90/53.06	]).
27.90/53.06	
27.90/53.06	============================== end of model ==========================
27.90/53.06	
27.90/53.06	============================== STATISTICS ============================
27.90/53.06	
27.90/53.06	For domain size 3.
27.90/53.06	
27.90/53.06	Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
27.90/53.06	Ground clauses: seen=79, kept=70.
27.90/53.06	Selections=3398, assignments=9787, propagations=32061, current_models=1.
27.90/53.06	Rewrite_terms=105580, rewrite_bools=117647, indexes=25616.
27.90/53.06	Rules_from_neg_clauses=1016, cross_offs=2904.
27.90/53.06	
27.90/53.06	============================== end of statistics =====================
27.90/53.06	
27.90/53.06	User_CPU=0.01, System_CPU=0.00, Wall_clock=0.
27.90/53.06	
27.90/53.06	Exiting with 1 model.
27.90/53.06	
27.90/53.06	Process 6628 exit (max_models) Tue Aug  1 07:33:45 2023
27.90/53.06	The process finished Tue Aug  1 07:33:45 2023
27.90/53.06	
27.90/53.06	
27.90/53.06	Mace4 cooked interpretation:
27.90/53.06	
27.90/53.06	% number = 1
27.90/53.06	% seconds = 0
27.90/53.06	
27.90/53.06	% Interpretation of size 3
27.90/53.06	
27.90/53.06	a = 0.
27.90/53.06	
27.90/53.06	c = 0.
27.90/53.06	
27.90/53.06	b = 1.
27.90/53.06	
27.90/53.06	f(0) = 0.
27.90/53.06	f(1) = 2.
27.90/53.06	f(2) = 0.
27.90/53.06	
27.90/53.06	h(0) = 0.
27.90/53.06	h(1) = 0.
27.90/53.06	h(2) = 1.
27.90/53.06	
27.90/53.06	g(0) = 1.
27.90/53.06	g(1) = 1.
27.90/53.06	g(2) = 1.
27.90/53.06	
27.90/53.06	k(0) = 0.
27.90/53.06	k(1) = 0.
27.90/53.06	k(2) = 1.
27.90/53.06	
27.90/53.06	  ->*(0,0).
27.90/53.06	  ->*(0,1).
27.90/53.06	  ->*(0,2).
27.90/53.06	- ->*(1,0).
27.90/53.06	  ->*(1,1).
27.90/53.06	- ->*(1,2).
27.90/53.06	- ->*(2,0).
27.90/53.06	- ->*(2,1).
27.90/53.06	  ->*(2,2).
27.90/53.06	
27.90/53.06	  ->(0,0).
27.90/53.06	  ->(0,1).
27.90/53.06	  ->(0,2).
27.90/53.06	- ->(1,0).
27.90/53.06	  ->(1,1).
27.90/53.06	- ->(1,2).
27.90/53.06	- ->(2,0).
27.90/53.06	- ->(2,1).
27.90/53.06	  ->(2,2).
27.90/53.06	
27.90/53.06	
27.90/53.06	The problem is infeasible.
27.90/53.06	
27.90/53.06	
27.90/53.06	The problem is not confluent.
27.90/75.46	EOF