5.003/5.003	YES
5.003/5.003	
5.003/5.003	Problem 1:
5.003/5.003	
5.003/5.003	
5.003/5.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
5.003/5.003	Confluence Problem:
5.003/5.003	(VAR vNonEmpty:S x:S)
5.003/5.003	(STRATEGY CONTEXTSENSITIVE
5.003/5.003	(a)
5.003/5.003	(f 1)
5.003/5.003	(g 1 2)
5.003/5.003	(h 1)
5.003/5.003	(A)
5.003/5.003	(b)
5.003/5.003	(fSNonEmpty)
5.003/5.003	(i 1)
5.003/5.003	)
5.003/5.003	(RULES
5.003/5.003	a -> b
5.003/5.003	f(x:S) -> A | x:S ->* b
5.003/5.003	g(x:S,x:S) -> h(x:S)
5.003/5.003	h(x:S) -> i(x:S)
5.003/5.003	)
5.003/5.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
5.003/5.003	
5.003/5.003	
5.003/5.003	Problem 1:
5.003/5.003	
5.003/5.003	Inlining of Conditions Processor [STERN17]:
5.003/5.003	
5.003/5.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
5.003/5.003	Confluence Problem:
5.003/5.003	(VAR vNonEmpty:S x:S)
5.003/5.003	(STRATEGY CONTEXTSENSITIVE
5.003/5.003	(a)
5.003/5.003	(f 1)
5.003/5.003	(g 1 2)
5.003/5.003	(h 1)
5.003/5.003	(A)
5.003/5.003	(b)
5.003/5.003	(fSNonEmpty)
5.003/5.003	(i 1)
5.003/5.003	)
5.003/5.003	(RULES
5.003/5.003	a -> b
5.003/5.003	f(x:S) -> A | x:S ->* b
5.003/5.003	g(x:S,x:S) -> h(x:S)
5.003/5.003	h(x:S) -> i(x:S)
5.003/5.003	)
5.003/5.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
5.003/5.003	
5.003/5.003	
5.003/5.003	Problem 1:
5.003/5.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
5.003/5.003	Confluence Problem:
5.003/5.003	(VAR vNonEmpty:S x:S)
5.003/5.003	(STRATEGY CONTEXTSENSITIVE
5.003/5.003	(a)
5.003/5.003	(f 1)
5.003/5.003	(g 1 2)
5.003/5.003	(h 1)
5.003/5.003	(A)
5.003/5.003	(b)
5.003/5.003	(fSNonEmpty)
5.003/5.003	(i 1)
5.003/5.003	)
5.003/5.003	(RULES
5.003/5.003	a -> b
5.003/5.003	f(x:S) -> A | x:S ->* b
5.003/5.003	g(x:S,x:S) -> h(x:S)
5.003/5.003	h(x:S) -> i(x:S)
5.003/5.003	)
5.003/5.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
5.003/5.003	
5.003/5.003	Critical Pairs Processor:
5.003/5.003	-> Rules:
5.003/5.003	a -> b
5.003/5.003	f(x:S) -> A | x:S ->* b
5.003/5.003	g(x:S,x:S) -> h(x:S)
5.003/5.003	h(x:S) -> i(x:S)
5.003/5.003	-> Vars:
5.003/5.003	"x", "x", "x"
5.003/5.003	-> FVars:
5.003/5.003	"x2", "x3", "x4"
5.003/5.003	-> PVars:
5.003/5.003	"x": ["x2", "x3", "x4"]
5.003/5.003	
5.003/5.003	-> Rlps:
5.003/5.003	crule: a -> b, id: 1, possubterms: a-> []
5.003/5.003	crule: f(x2:S) -> A | x2:S ->* b, id: 2, possubterms: f(x2:S)-> []
5.003/5.003	crule: g(x3:S,x3:S) -> h(x3:S), id: 3, possubterms: g(x3:S,x3:S)-> []
5.003/5.003	crule: h(x4:S) -> i(x4:S), id: 4, possubterms: h(x4:S)-> []
5.003/5.003	
5.003/5.003	-> Unifications:
5.003/5.003	
5.003/5.003	
5.003/5.003	-> Critical pairs info:
5.003/5.003	
5.003/5.003	
5.003/5.003	-> Problem conclusions:
5.003/5.003	 Not left linear, Right linear, Not linear
5.003/5.003	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
5.003/5.003	 CTRS Type: 1
5.003/5.003	 Deterministic, Strongly deterministic
5.003/5.003	 Oriented CTRS, Properly oriented CTRS, Not join CTRS
5.003/5.003	 Maybe right-stable CTRS, Overlay CTRS
5.003/5.003	 Maybe normal CTRS, Maybe almost normal CTRS
5.003/5.003	 Maybe terminating CTRS, Joinable CCPs
5.003/5.003	 Maybe level confluent
5.003/5.003	 Maybe confluent
5.003/5.003	
5.003/5.003	Problem 1:
5.003/5.003	Underlying TRS Termination Processor:
5.003/5.003	
5.003/5.003	Resulting Underlying TRS:
5.003/5.003	(VAR vNonEmpty:S x:S)
5.003/5.003	(STRATEGY CONTEXTSENSITIVE
5.003/5.003	(a)
5.003/5.003	(f 1)
5.003/5.003	(g 1 2)
5.003/5.003	(h 1)
5.003/5.003	(A)
5.003/5.003	(b)
5.003/5.003	(i 1)
5.003/5.003	)
5.003/5.003	(RULES
5.003/5.003	a -> b
5.003/5.003	f(x:S) -> A
5.003/5.003	g(x:S,x:S) -> h(x:S)
5.003/5.003	h(x:S) -> i(x:S)
5.003/5.003	)
5.003/5.003	Underlying TRS terminating?
5.003/5.003	YES
5.003/5.003	
5.003/5.003	Problem 1:
5.003/5.003	
5.003/5.003	(VAR vu95NonEmpty:S vNonEmptyu58S:S xu58S:S)
5.003/5.003	(RULES
5.003/5.003	a -> b
5.003/5.003	f(xu58S:S) -> A
5.003/5.003	g(xu58S:S,xu58S:S) -> h(xu58S:S)
5.003/5.003	h(xu58S:S) -> i(xu58S:S)
5.003/5.003	)
5.003/5.003	
5.003/5.003	Problem 1:
5.003/5.003	
5.003/5.003	Innermost Equivalent Processor:
5.003/5.003	-> Rules:
5.003/5.003	 a -> b
5.003/5.003	 f(xu58S:S) -> A
5.003/5.003	 g(xu58S:S,xu58S:S) -> h(xu58S:S)
5.003/5.003	 h(xu58S:S) -> i(xu58S:S)
5.003/5.003	-> The term rewriting system is non-overlaping or locally confluent overlay system. Therefore, innermost termination implies termination.
5.003/5.003	
5.003/5.003	
5.003/5.003	Problem 1:
5.003/5.003	
5.003/5.003	Dependency Pairs Processor:
5.003/5.003	-> Pairs:
5.003/5.003	 G(xu58S:S,xu58S:S) -> H(xu58S:S)
5.003/5.003	-> Rules:
5.003/5.003	 a -> b
5.003/5.003	 f(xu58S:S) -> A
5.003/5.003	 g(xu58S:S,xu58S:S) -> h(xu58S:S)
5.003/5.003	 h(xu58S:S) -> i(xu58S:S)
5.003/5.003	
5.003/5.003	Problem 1:
5.003/5.003	
5.003/5.003	SCC Processor:
5.003/5.003	-> Pairs:
5.003/5.003	 G(xu58S:S,xu58S:S) -> H(xu58S:S)
5.003/5.003	-> Rules:
5.003/5.003	 a -> b
5.003/5.003	 f(xu58S:S) -> A
5.003/5.003	 g(xu58S:S,xu58S:S) -> h(xu58S:S)
5.003/5.003	 h(xu58S:S) -> i(xu58S:S)
5.003/5.003	->Strongly Connected Components:
5.003/5.003	 There is no strongly connected component
5.003/5.003	
5.003/5.003	The problem is finite.
5.003/5.003	
5.003/5.003	
5.003/5.003	-> Problem conclusions:
5.003/5.003	 Not left linear, Right linear, Not linear
5.003/5.003	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
5.003/5.003	 CTRS Type: 1
5.003/5.003	 Deterministic, Strongly deterministic
5.003/5.003	 Oriented CTRS, Properly oriented CTRS, Not join CTRS
5.003/5.003	 Maybe right-stable CTRS, Overlay CTRS
5.003/5.003	 Maybe normal CTRS, Maybe almost normal CTRS
5.003/5.003	 Terminating CTRS, Joinable CCPs
5.003/5.003	 Maybe level confluent
5.003/5.003	 Maybe confluent
5.003/5.003	
5.003/5.003	Problem 1:
5.003/5.003	
5.003/5.003	Transform CTRS Processor:
5.003/5.003	
5.003/5.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
5.003/5.003	Confluence Problem:
5.003/5.003	(VAR vNonEmpty:S x:S)
5.003/5.003	(STRATEGY CONTEXTSENSITIVE
5.003/5.003	(a)
5.003/5.003	(f 1)
5.003/5.003	(g 1 2)
5.003/5.003	(h 1)
5.003/5.003	(A)
5.003/5.003	(b)
5.003/5.003	(fSNonEmpty)
5.003/5.003	(i 1)
5.003/5.003	)
5.003/5.003	(RULES
5.003/5.003	a -> b
5.003/5.003	f(x:S) -> A | x:S ->* b
5.003/5.003	g(x:S,x:S) -> h(x:S)
5.003/5.003	h(x:S) -> i(x:S)
5.003/5.003	)
5.003/5.003	Critical Pairs:
5.003/5.003	
5.003/5.003	Terminating:YES
5.003/5.003	
5.003/5.003	-> Problem conclusions:
5.003/5.003	 Not left linear, Right linear, Not linear
5.003/5.003	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
5.003/5.003	 CTRS Type: 1
5.003/5.003	 Deterministic, Strongly deterministic
5.003/5.003	 Oriented CTRS, Properly oriented CTRS, Not join CTRS
5.003/5.003	 Maybe right-stable CTRS, Overlay CTRS
5.003/5.003	 Maybe normal CTRS, Maybe almost normal CTRS
5.003/5.003	 Terminating CTRS, Joinable CCPs
5.003/5.003	 Maybe level confluent
5.003/5.003	 Maybe confluent
5.003/5.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
5.003/5.003	Resulting U(R):
5.003/5.003	(VAR vNonEmpty:S x:S)
5.003/5.003	(STRATEGY CONTEXTSENSITIVE
5.003/5.003	(a)
5.003/5.003	(f 1)
5.003/5.003	(g 1 2)
5.003/5.003	(h 1)
5.003/5.003	(A)
5.003/5.003	(b)
5.003/5.003	(fSNonEmpty)
5.003/5.003	(i 1)
5.003/5.003	(U9_1 1)
5.003/5.003	)
5.003/5.003	(RULES
5.003/5.003	a -> b
5.003/5.003	f(x:S) -> U9_1(x:S)
5.003/5.003	g(x:S,x:S) -> h(x:S)
5.003/5.003	h(x:S) -> i(x:S)
5.003/5.003	U9_1(b) -> A
5.003/5.003	)
5.003/5.003	
5.003/5.003	Problem 1:
5.003/5.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
5.003/5.003	Confluence Problem:
5.003/5.003	(VAR vNonEmpty:S x:S)
5.003/5.003	(STRATEGY CONTEXTSENSITIVE
5.003/5.003	(a)
5.003/5.003	(f 1)
5.003/5.003	(g 1 2)
5.003/5.003	(h 1)
5.003/5.003	(A)
5.003/5.003	(b)
5.003/5.003	(fSNonEmpty)
5.003/5.003	(i 1)
5.003/5.003	(U9_1 1)
5.003/5.003	)
5.003/5.003	(RULES
5.003/5.003	a -> b
5.003/5.003	f(x:S) -> U9_1(x:S)
5.003/5.003	g(x:S,x:S) -> h(x:S)
5.003/5.003	h(x:S) -> i(x:S)
5.003/5.003	U9_1(b) -> A
5.003/5.003	)
5.003/5.003	Terminating:"YES"
5.003/5.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
5.003/5.003	
5.003/5.003	Huet Levy Processor:
5.003/5.003	-> Rules:
5.003/5.003	 a -> b
5.003/5.003	 f(x:S) -> U9_1(x:S)
5.003/5.003	 g(x:S,x:S) -> h(x:S)
5.003/5.003	 h(x:S) -> i(x:S)
5.003/5.003	 U9_1(b) -> A
5.003/5.003	-> Vars:
5.003/5.003	 x, x, x
5.003/5.003	-> FVars:
5.003/5.003	 x2, x3, x4
5.003/5.003	-> PVars:
5.003/5.003	 x: [x2, x3, x4]
5.003/5.003	
5.003/5.003	-> Rlps:
5.003/5.003	 (rule: a -> b, id: 1, possubterms: a->[])
5.003/5.003	 (rule: f(x2:S) -> U9_1(x2:S), id: 2, possubterms: f(x2:S)->[])
5.003/5.003	 (rule: g(x3:S,x3:S) -> h(x3:S), id: 3, possubterms: g(x3:S,x3:S)->[])
5.003/5.003	 (rule: h(x4:S) -> i(x4:S), id: 4, possubterms: h(x4:S)->[])
5.003/5.003	 (rule: U9_1(b) -> A, id: 5, possubterms: U9_1(b)->[], b->[1])
5.003/5.003	
5.003/5.003	-> Unifications:
5.003/5.003	
5.003/5.003	
5.003/5.003	-> Critical pairs info:
5.003/5.003	
5.003/5.003	
5.003/5.003	-> Problem conclusions:
5.003/5.003	 Not left linear, Right linear, Not linear
5.003/5.003	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
5.003/5.003	 Not Huet-Levy confluent, Newman confluent
5.003/5.003	 R is a TRS
5.003/5.003	
5.003/5.003	
5.003/5.003	The problem is joinable.
5.003/5.003	0.39user 0.04system 0:05.03elapsed 8%CPU (0avgtext+0avgdata 34104maxresident)k
5.003/5.003	8inputs+0outputs (0major+12411minor)pagefaults 0swaps