0.00/0.03	YES
0.00/0.03	
0.00/0.03	Problem 1: 
0.00/0.03	
0.00/0.03	
0.00/0.03	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.03	Confluence Problem:
0.00/0.03	(VAR x)
0.00/0.03	(REPLACEMENT-MAP
0.00/0.03	(f 1, 2)
0.00/0.03	(a)
0.00/0.03	(b)
0.00/0.03	(g 1)
0.00/0.03	)
0.00/0.03	(RULES
0.00/0.03	f(x,x) -> a | g(x) ->* b
0.00/0.03	)
0.00/0.03	
0.00/0.03	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.03	
0.00/0.03	
0.00/0.03	Problem 1: 
0.00/0.03	
0.00/0.03	Problem 1: 
0.00/0.03	
0.00/0.03	Clean CTRS Procedure:
0.00/0.03	
0.00/0.03	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.03	Confluence Problem:
0.00/0.03	(VAR x)
0.00/0.03	(REPLACEMENT-MAP
0.00/0.03	(f 1, 2)
0.00/0.03	(a)
0.00/0.03	(b)
0.00/0.03	(g 1)
0.00/0.03	)
0.00/0.03	(RULES
0.00/0.03	f(x,x) -> a | g(x) ->* b
0.00/0.03	)
0.00/0.03	
0.00/0.03	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.03	
0.00/0.03	CRule InfChecker Info:
0.00/0.03	f(x,x) -> a | g(x) ->* b
0.00/0.03	Rule remains
0.00/0.03	Proof:
0.00/0.03	HAS_EQUATIONAL_CONDS
0.00/0.03	
0.00/0.03	Problem 1: 
0.00/0.03	
0.00/0.03	Problem 1: 
0.00/0.03	
0.00/0.03	Problem 1: 
0.00/0.03	Underlying TRS Termination Procedure:
0.00/0.03	
0.00/0.03	Resulting Underlying TRS:
0.00/0.03	(VAR x)
0.00/0.03	(STRATEGY CONTEXTSENSITIVE
0.00/0.03	(f 1 2)
0.00/0.03	(a)
0.00/0.03	)
0.00/0.03	(RULES
0.00/0.03	f(x,x) -> a
0.00/0.03	)
0.00/0.03	
0.00/0.03	Underlying TRS terminating?
0.00/0.03	YES
0.00/0.03	
0.00/0.03	Problem 1: 
0.00/0.03	
0.00/0.03	(VAR vu95NonEmpty x)
0.00/0.03	(RULES
0.00/0.03	f(x,x) -> a
0.00/0.03	)
0.00/0.03	
0.00/0.03	
0.00/0.03	Problem 1: 
0.00/0.03	
0.00/0.03	Innermost Equivalent Processor:
0.00/0.03	-> Rules:
0.00/0.03	 f(x,x) -> a
0.00/0.03	-> The term rewriting system is non-overlaping or locally confluent overlay system. Therefore, innermost termination implies termination.
0.00/0.03	 
0.00/0.03	
0.00/0.03	Problem 1: 
0.00/0.03	
0.00/0.03	Dependency Pairs Processor:
0.00/0.03	-> Pairs:
0.00/0.03	 Empty
0.00/0.03	-> Rules:
0.00/0.03	 f(x,x) -> a
0.00/0.03	
0.00/0.03	Problem 1: 
0.00/0.03	
0.00/0.03	SCC Processor:
0.00/0.03	-> Pairs:
0.00/0.03	 Empty
0.00/0.03	-> Rules:
0.00/0.03	 f(x,x) -> a
0.00/0.03	->Strongly Connected Components:
0.00/0.03	 There is no strongly connected component
0.00/0.03	
0.00/0.03	The problem is finite.
0.00/0.03	
0.00/0.03	
0.00/0.03	-> Problem conclusions:
0.00/0.03	 Not left linear, Right linear, Not linear, Not weakly left-linear
0.00/0.03	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal, Strongly orthogonal
0.00/0.03	 CTRS Type: 1
0.00/0.03	 Deterministic, Strongly deterministic
0.00/0.03	 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS
0.00/0.03	 Maybe right-stable CTRS, Overlay CTRS
0.00/0.03	 Maybe normal CTRS, Maybe almost normal CTRS
0.00/0.03	 ECCPs not considered
0.00/0.03	 Terminating CTRS, Maybe operational terminating CTRS
0.00/0.03	 Maybe joinable CCPs
0.00/0.03	 Maybe level confluent, Maybe confluent
0.00/0.03	
0.00/0.03	Problem 1: 
0.00/0.03	
0.00/0.03	U Transform CTRS Procedure:
0.00/0.03	
0.00/0.03	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.03	Confluence Problem:
0.00/0.03	(VAR x)
0.00/0.03	(REPLACEMENT-MAP
0.00/0.03	(f 1, 2)
0.00/0.03	(a)
0.00/0.03	(b)
0.00/0.03	(g 1)
0.00/0.03	)
0.00/0.03	(RULES
0.00/0.03	f(x,x) -> a | g(x) ->* b
0.00/0.03	)
0.00/0.03	
0.00/0.03	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.03	Resulting U(R):
0.00/0.03	(VAR x)
0.00/0.03	(STRATEGY CONTEXTSENSITIVE
0.00/0.03	(f 1 2)
0.00/0.03	(a)
0.00/0.03	(b)
0.00/0.03	(g 1)
0.00/0.03	(U5_1 1 2)
0.00/0.03	)
0.00/0.03	(RULES
0.00/0.03	f(x,x) -> U5_1(g(x),x)
0.00/0.03	U5_1(b,x) -> a
0.00/0.03	)
0.00/0.03	
0.00/0.03	
0.00/0.03	Problem 1: 
0.00/0.03	
0.00/0.03	
0.00/0.03	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.03	Confluence Problem:
0.00/0.03	(VAR x)
0.00/0.03	(REPLACEMENT-MAP
0.00/0.03	(f 1, 2)
0.00/0.03	(a)
0.00/0.03	(b)
0.00/0.03	(g 1)
0.00/0.03	(U5_1 1, 2)
0.00/0.03	)
0.00/0.03	(RULES
0.00/0.03	f(x,x) -> U5_1(g(x),x)
0.00/0.03	U5_1(b,x) -> a
0.00/0.03	)
0.00/0.03	
0.00/0.03	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.03	
0.00/0.03	
0.00/0.03	Problem 1: 
0.00/0.03	
0.00/0.03	Problem 1: 
0.00/0.03	Not CS-TRS Procedure:
0.00/0.03	R is not a CS-TRS
0.00/0.03	
0.00/0.03	Problem 1: 
0.00/0.03	Termination Procedure:
0.00/0.03	Terminating?
0.00/0.03	YES
0.00/0.03	
0.00/0.03	Problem 1: 
0.00/0.03	
0.00/0.03	(VAR vu95NonEmpty x)
0.00/0.03	(RULES
0.00/0.03	U5_1(b,x) -> a
0.00/0.03	f(x,x) -> U5_1(g(x),x)
0.00/0.03	)
0.00/0.03	
0.00/0.03	
0.00/0.03	Problem 1: 
0.00/0.03	
0.00/0.03	Innermost Equivalent Processor:
0.00/0.03	-> Rules:
0.00/0.03	 U5_1(b,x) -> a
0.00/0.03	 f(x,x) -> U5_1(g(x),x)
0.00/0.03	-> The term rewriting system is non-overlaping or locally confluent overlay system. Therefore, innermost termination implies termination.
0.00/0.03	 
0.00/0.03	
0.00/0.03	Problem 1: 
0.00/0.03	
0.00/0.03	Dependency Pairs Processor:
0.00/0.03	-> Pairs:
0.00/0.03	 Empty
0.00/0.03	-> Rules:
0.00/0.03	 U5_1(b,x) -> a
0.00/0.03	 f(x,x) -> U5_1(g(x),x)
0.00/0.03	
0.00/0.03	Problem 1: 
0.00/0.03	
0.00/0.03	SCC Processor:
0.00/0.03	-> Pairs:
0.00/0.03	 Empty
0.00/0.03	-> Rules:
0.00/0.03	 U5_1(b,x) -> a
0.00/0.03	 f(x,x) -> U5_1(g(x),x)
0.00/0.03	->Strongly Connected Components:
0.00/0.03	 There is no strongly connected component
0.00/0.03	
0.00/0.03	The problem is finite.
0.00/0.03	
0.00/0.03	
0.00/0.03	Problem 1: 
0.00/0.03	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.03	Confluence Problem:
0.00/0.03	(VAR x)
0.00/0.03	(REPLACEMENT-MAP
0.00/0.03	(f 1, 2)
0.00/0.03	(a)
0.00/0.03	(U5_1 1, 2)
0.00/0.03	)
0.00/0.03	(RULES
0.00/0.03	f(x,x) -> U5_1(g(x),x)
0.00/0.03	U5_1(b,x) -> a
0.00/0.03	)
0.00/0.03	
0.00/0.03	Terminating:"YES"
0.00/0.03	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.03	
0.00/0.03	Huet Levy NW Procedure:
0.00/0.03	-> Rules:
0.00/0.03	 f(x,x) -> U5_1(g(x),x)
0.00/0.03	 U5_1(b,x) -> a
0.00/0.03	-> Vars:
0.00/0.03	 x, x
0.00/0.03	
0.00/0.03	-> Rlps:
0.00/0.03	 (rule: f(x,x) -> U5_1(g(x),x), id: 1, possubterms: f(x,x)->[])
0.00/0.03	 (rule: U5_1(b,x) -> a, id: 2, possubterms: U5_1(b,x)->[], b->[1])
0.00/0.03	
0.00/0.03	-> Unifications:
0.00/0.03	
0.00/0.03	
0.00/0.03	-> Critical pairs info:
0.00/0.03	
0.00/0.03	
0.00/0.03	-> Problem conclusions:
0.00/0.03	 Not left linear, Not right linear, Not linear
0.00/0.03	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal, Not strongly orthogonal
0.00/0.03	 Not Huet-Levy confluent, Newman confluent
0.00/0.03	 R is a TRS 
0.00/0.03	 Confluent
0.00/0.03	
0.00/0.03	
0.00/0.03	The problem is confluent.
0.00/1.06	EOF