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