0.003/0.003	YES
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	
0.003/0.003	
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	Confluence Problem:
0.003/0.003	(VAR vNonEmpty x y)
0.003/0.003	(REPLACEMENT-MAP
0.003/0.003	(F 1, 2)
0.003/0.003	(a)
0.003/0.003	(G 1)
0.003/0.003	(b)
0.003/0.003	(fSNonEmpty)
0.003/0.003	)
0.003/0.003	(RULES
0.003/0.003	F(x,y) -> G(x) | x ->*<- y
0.003/0.003	a -> b
0.003/0.003	)
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	
0.003/0.003	Inlining of Conditions Processor [STERN17]:
0.003/0.003	
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	Confluence Problem:
0.003/0.003	(VAR vNonEmpty x y)
0.003/0.003	(REPLACEMENT-MAP
0.003/0.003	(F 1, 2)
0.003/0.003	(a)
0.003/0.003	(G 1)
0.003/0.003	(b)
0.003/0.003	(fSNonEmpty)
0.003/0.003	)
0.003/0.003	(RULES
0.003/0.003	F(x,y) -> G(x) | x ->*<- y
0.003/0.003	a -> b
0.003/0.003	)
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	Confluence Problem:
0.003/0.003	(VAR vNonEmpty x y)
0.003/0.003	(REPLACEMENT-MAP
0.003/0.003	(F 1, 2)
0.003/0.003	(a)
0.003/0.003	(G 1)
0.003/0.003	(b)
0.003/0.003	(fSNonEmpty)
0.003/0.003	)
0.003/0.003	(RULES
0.003/0.003	F(x,y) -> G(x) | x ->*<- y
0.003/0.003	a -> b
0.003/0.003	)
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	
0.003/0.003	Critical Pairs Processor:
0.003/0.003	-> Rules:
0.003/0.003	F(x,y) -> G(x) | x ->*<- y
0.003/0.003	a -> b
0.003/0.003	-> Vars:
0.003/0.003	"x", "y"
0.003/0.003	
0.003/0.003	-> Rlps:
0.003/0.003	crule: F(x,y) -> G(x) | x ->*<- y, id: 1, possubterms: F(x,y)-> []
0.003/0.003	crule: a -> b, id: 2, possubterms: a-> []
0.003/0.003	
0.003/0.003	-> Unifications:
0.003/0.003	
0.003/0.003	
0.003/0.003	-> Critical pairs info:
0.003/0.003	
0.003/0.003	
0.003/0.003	-> Problem conclusions:
0.003/0.003	 Left linear, Right linear, Linear
0.003/0.003	 Weakly orthogonal, Almost orthogonal, Orthogonal
0.003/0.003	 CTRS Type: 1
0.003/0.003	 Deterministic, Strongly deterministic
0.003/0.003	 Not oriented CTRS, Not properly oriented CTRS, Join CTRS, Not semiequational CTRS
0.003/0.003	 Maybe right-stable CTRS, Overlay CTRS
0.003/0.003	 Maybe normal CTRS, Maybe almost normal CTRS
0.003/0.003	 Maybe terminating CTRS, Maybe operational terminating CTRS, Joinable CCPs
0.003/0.003	 Maybe level confluent
0.003/0.003	 Maybe confluent
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	Underlying TRS Termination Processor:
0.003/0.003	
0.003/0.003	Resulting Underlying TRS:
0.003/0.003	(VAR x y)
0.003/0.003	(STRATEGY CONTEXTSENSITIVE
0.003/0.003	(F 1 2)
0.003/0.003	(a)
0.003/0.003	(G 1)
0.003/0.003	(b)
0.003/0.003	)
0.003/0.003	(RULES
0.003/0.003	F(x,y) -> G(x)
0.003/0.003	a -> b
0.003/0.003	)
0.003/0.003	Underlying TRS terminating?
0.003/0.003	YES
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	
0.003/0.003	(VAR vu95NonEmpty x y)
0.003/0.003	(RULES
0.003/0.003	F(x,y) -> G(x)
0.003/0.003	a -> b
0.003/0.003	)
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	
0.003/0.003	Innermost Equivalent Processor:
0.003/0.003	-> Rules:
0.003/0.003	 F(x,y) -> G(x)
0.003/0.003	 a -> b
0.003/0.003	-> The term rewriting system is non-overlaping or locally confluent overlay system. Therefore, innermost termination implies termination.
0.003/0.003	
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	
0.003/0.003	Dependency Pairs Processor:
0.003/0.003	-> Pairs:
0.003/0.003	 Empty
0.003/0.003	-> Rules:
0.003/0.003	 F(x,y) -> G(x)
0.003/0.003	 a -> b
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	
0.003/0.003	SCC Processor:
0.003/0.003	-> Pairs:
0.003/0.003	 Empty
0.003/0.003	-> Rules:
0.003/0.003	 F(x,y) -> G(x)
0.003/0.003	 a -> b
0.003/0.003	->Strongly Connected Components:
0.003/0.003	 There is no strongly connected component
0.003/0.003	
0.003/0.003	The problem is finite.
0.003/0.003	
0.003/0.003	
0.003/0.003	-> Problem conclusions:
0.003/0.003	 Left linear, Right linear, Linear
0.003/0.003	 Weakly orthogonal, Almost orthogonal, Orthogonal
0.003/0.003	 CTRS Type: 1
0.003/0.003	 Deterministic, Strongly deterministic
0.003/0.003	 Not oriented CTRS, Not properly oriented CTRS, Join CTRS, Not semiequational CTRS
0.003/0.003	 Maybe right-stable CTRS, Overlay CTRS
0.003/0.003	 Maybe normal CTRS, Maybe almost normal CTRS
0.003/0.003	 Terminating CTRS, Maybe operational terminating CTRS, Joinable CCPs
0.003/0.003	 Maybe level confluent
0.003/0.003	 Confluent
0.003/0.003	
0.003/0.003	The problem is joinable.
0.003/0.003	0.03user 0.00system 0:00.03elapsed 106%CPU (0avgtext+0avgdata 9480maxresident)k
0.003/0.003	0inputs+0outputs (0major+3374minor)pagefaults 0swaps