0.093/0.093	YES
0.093/0.093	
0.093/0.093	Problem 1:
0.093/0.093	
0.093/0.093	
0.093/0.093	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.093/0.093	Confluence Problem:
0.093/0.093	(VAR vNonEmpty:S x:S)
0.093/0.093	(STRATEGY CONTEXTSENSITIVE
0.093/0.093	(a)
0.093/0.093	(b)
0.093/0.093	(f 1)
0.093/0.093	(c)
0.093/0.093	(fSNonEmpty)
0.093/0.093	)
0.093/0.093	(RULES
0.093/0.093	a -> c
0.093/0.093	b -> c
0.093/0.093	f(x:S) -> x:S | a ->* x:S
0.093/0.093	)
0.093/0.093	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.093/0.093	
0.093/0.093	
0.093/0.093	Problem 1:
0.093/0.093	
0.093/0.093	Inlining of Conditions Processor [STERN17]:
0.093/0.093	
0.093/0.093	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.093/0.093	Confluence Problem:
0.093/0.093	(VAR vNonEmpty:S x:S)
0.093/0.093	(STRATEGY CONTEXTSENSITIVE
0.093/0.093	(a)
0.093/0.093	(b)
0.093/0.093	(f 1)
0.093/0.093	(c)
0.093/0.093	(fSNonEmpty)
0.093/0.093	)
0.093/0.093	(RULES
0.093/0.093	a -> c
0.093/0.093	b -> c
0.093/0.093	f(x:S) -> x:S | a ->* x:S
0.093/0.093	)
0.093/0.093	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.093/0.093	
0.093/0.093	
0.093/0.093	Problem 1:
0.093/0.093	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.093/0.093	Confluence Problem:
0.093/0.093	(VAR vNonEmpty:S x:S)
0.093/0.093	(STRATEGY CONTEXTSENSITIVE
0.093/0.093	(a)
0.093/0.093	(b)
0.093/0.093	(f 1)
0.093/0.093	(c)
0.093/0.093	(fSNonEmpty)
0.093/0.093	)
0.093/0.093	(RULES
0.093/0.093	a -> c
0.093/0.093	b -> c
0.093/0.093	f(x:S) -> x:S | a ->* x:S
0.093/0.093	)
0.093/0.093	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.093/0.093	
0.093/0.093	Critical Pairs Processor:
0.093/0.093	-> Rules:
0.093/0.093	a -> c
0.093/0.093	b -> c
0.093/0.093	f(x:S) -> x:S | a ->* x:S
0.093/0.093	-> Vars:
0.093/0.093	"x"
0.093/0.093	-> FVars:
0.093/0.093	"x2"
0.093/0.093	-> PVars:
0.093/0.093	"x": ["x2"]
0.093/0.093	
0.093/0.093	-> Rlps:
0.093/0.093	crule: a -> c, id: 1, possubterms: a-> []
0.093/0.093	crule: b -> c, id: 2, possubterms: b-> []
0.093/0.093	crule: f(x2:S) -> x2:S | a ->* x2:S, id: 3, possubterms: f(x2:S)-> []
0.093/0.093	
0.093/0.093	-> Unifications:
0.093/0.093	
0.093/0.093	
0.093/0.093	-> Critical pairs info:
0.093/0.093	
0.093/0.093	
0.093/0.093	-> Problem conclusions:
0.093/0.093	 Left linear, Right linear, Linear
0.093/0.093	 Weakly orthogonal, Almost orthogonal, Orthogonal
0.093/0.093	 CTRS Type: 1
0.093/0.093	 Deterministic, Strongly deterministic
0.093/0.093	 Oriented CTRS, Properly oriented CTRS, Not join CTRS
0.093/0.093	 Maybe right-stable CTRS, Overlay CTRS
0.093/0.093	 Maybe normal CTRS, Maybe almost normal CTRS
0.093/0.093	 Maybe terminating CTRS, Joinable CCPs
0.093/0.093	 Maybe level confluent
0.093/0.093	 Maybe confluent
0.093/0.093	
0.093/0.093	Problem 1:
0.093/0.093	Underlying TRS Termination Processor:
0.093/0.093	
0.093/0.093	Resulting Underlying TRS:
0.093/0.093	(VAR vNonEmpty:S x:S)
0.093/0.093	(STRATEGY CONTEXTSENSITIVE
0.093/0.093	(a)
0.093/0.093	(b)
0.093/0.093	(f 1)
0.093/0.093	(c)
0.093/0.093	)
0.093/0.093	(RULES
0.093/0.093	a -> c
0.093/0.093	b -> c
0.093/0.093	f(x:S) -> x:S
0.093/0.093	)
0.093/0.093	Underlying TRS terminating?
0.093/0.093	YES
0.093/0.093	
0.093/0.093	Problem 1:
0.093/0.093	
0.093/0.093	(VAR vu95NonEmpty:S vNonEmptyu58S:S xu58S:S)
0.093/0.093	(RULES
0.093/0.093	a -> c
0.093/0.093	b -> c
0.093/0.093	f(xu58S:S) -> xu58S:S
0.093/0.093	)
0.093/0.093	
0.093/0.093	Problem 1:
0.093/0.093	
0.093/0.093	Innermost Equivalent Processor:
0.093/0.093	-> Rules:
0.093/0.093	 a -> c
0.093/0.093	 b -> c
0.093/0.093	 f(xu58S:S) -> xu58S:S
0.093/0.093	-> The term rewriting system is non-overlaping or locally confluent overlay system. Therefore, innermost termination implies termination.
0.093/0.093	
0.093/0.093	
0.093/0.093	Problem 1:
0.093/0.093	
0.093/0.093	Dependency Pairs Processor:
0.093/0.093	-> Pairs:
0.093/0.093	 Empty
0.093/0.093	-> Rules:
0.093/0.093	 a -> c
0.093/0.093	 b -> c
0.093/0.093	 f(xu58S:S) -> xu58S:S
0.093/0.093	
0.093/0.093	Problem 1:
0.093/0.093	
0.093/0.093	SCC Processor:
0.093/0.093	-> Pairs:
0.093/0.093	 Empty
0.093/0.093	-> Rules:
0.093/0.093	 a -> c
0.093/0.093	 b -> c
0.093/0.093	 f(xu58S:S) -> xu58S:S
0.093/0.093	->Strongly Connected Components:
0.093/0.093	 There is no strongly connected component
0.093/0.093	
0.093/0.093	The problem is finite.
0.093/0.093	
0.093/0.093	
0.093/0.093	-> Problem conclusions:
0.093/0.093	 Left linear, Right linear, Linear
0.093/0.093	 Weakly orthogonal, Almost orthogonal, Orthogonal
0.093/0.093	 CTRS Type: 1
0.093/0.093	 Deterministic, Strongly deterministic
0.093/0.093	 Oriented CTRS, Properly oriented CTRS, Not join CTRS
0.093/0.093	 Maybe right-stable CTRS, Overlay CTRS
0.093/0.093	 Maybe normal CTRS, Maybe almost normal CTRS
0.093/0.093	 Terminating CTRS, Joinable CCPs
0.093/0.093	 Maybe level confluent
0.093/0.093	 Confluent
0.093/0.093	
0.093/0.093	The problem is joinable.
0.093/0.093	0.93user 0.09system 0:00.93elapsed 110%CPU (0avgtext+0avgdata 130872maxresident)k
0.093/0.093	8inputs+0outputs (0major+69445minor)pagefaults 0swaps