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