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