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	(f 1)
5.002/5.002	(h 1 2)
5.002/5.002	(A)
5.002/5.002	(d)
5.002/5.002	(e)
5.002/5.002	(fSNonEmpty)
5.002/5.002	(l)
5.002/5.002	)
5.002/5.002	(RULES
5.002/5.002	f(x:S) -> e | d ->* l
5.002/5.002	h(x:S,x:S) -> A
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	(f 1)
5.002/5.002	(h 1 2)
5.002/5.002	(A)
5.002/5.002	(d)
5.002/5.002	(e)
5.002/5.002	(fSNonEmpty)
5.002/5.002	(l)
5.002/5.002	)
5.002/5.002	(RULES
5.002/5.002	f(x:S) -> e | d ->* l
5.002/5.002	h(x:S,x:S) -> A
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	(f 1)
5.002/5.002	(h 1 2)
5.002/5.002	(A)
5.002/5.002	(d)
5.002/5.002	(e)
5.002/5.002	(fSNonEmpty)
5.002/5.002	(l)
5.002/5.002	)
5.002/5.002	(RULES
5.002/5.002	f(x:S) -> e | d ->* l
5.002/5.002	h(x:S,x:S) -> A
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	f(x:S) -> e | d ->* l
5.002/5.002	h(x:S,x:S) -> A
5.002/5.002	-> Vars:
5.002/5.002	"x", "x"
5.002/5.002	-> FVars:
5.002/5.002	"x2", "x3"
5.002/5.002	-> PVars:
5.002/5.002	"x": ["x2", "x3"]
5.002/5.002	
5.002/5.002	-> Rlps:
5.002/5.002	crule: f(x2:S) -> e | d ->* l, id: 1, possubterms: f(x2:S)-> []
5.002/5.002	crule: h(x3:S,x3:S) -> A, id: 2, possubterms: h(x3:S,x3: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	(f 1)
5.002/5.002	(h 1 2)
5.002/5.002	(A)
5.002/5.002	(e)
5.002/5.002	)
5.002/5.002	(RULES
5.002/5.002	f(x:S) -> e
5.002/5.002	h(x:S,x:S) -> A
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	f(xu58S:S) -> e
5.002/5.002	h(xu58S:S,xu58S:S) -> A
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	 f(xu58S:S) -> e
5.002/5.002	 h(xu58S:S,xu58S:S) -> A
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	 Empty
5.002/5.002	-> Rules:
5.002/5.002	 f(xu58S:S) -> e
5.002/5.002	 h(xu58S:S,xu58S:S) -> A
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	 Empty
5.002/5.002	-> Rules:
5.002/5.002	 f(xu58S:S) -> e
5.002/5.002	 h(xu58S:S,xu58S:S) -> A
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	(f 1)
5.002/5.002	(h 1 2)
5.002/5.002	(A)
5.002/5.002	(d)
5.002/5.002	(e)
5.002/5.002	(fSNonEmpty)
5.002/5.002	(l)
5.002/5.002	)
5.002/5.002	(RULES
5.002/5.002	f(x:S) -> e | d ->* l
5.002/5.002	h(x:S,x:S) -> A
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	(f 1)
5.002/5.002	(h 1 2)
5.002/5.002	(A)
5.002/5.002	(e)
5.002/5.002	(U8_1 1)
5.002/5.002	)
5.002/5.002	(RULES
5.002/5.002	f(x:S) -> U8_1(d)
5.002/5.002	h(x:S,x:S) -> A
5.002/5.002	U8_1(l) -> e
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	(f 1)
5.002/5.002	(h 1 2)
5.002/5.002	(A)
5.002/5.002	(e)
5.002/5.002	(U8_1 1)
5.002/5.002	)
5.002/5.002	(RULES
5.002/5.002	f(x:S) -> U8_1(d)
5.002/5.002	h(x:S,x:S) -> A
5.002/5.002	U8_1(l) -> e
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	 f(x:S) -> U8_1(d)
5.002/5.002	 h(x:S,x:S) -> A
5.002/5.002	 U8_1(l) -> e
5.002/5.002	-> Vars:
5.002/5.002	 x, x
5.002/5.002	-> FVars:
5.002/5.002	 x2, x3
5.002/5.002	-> PVars:
5.002/5.002	 x: [x2, x3]
5.002/5.002	
5.002/5.002	-> Rlps:
5.002/5.002	 (rule: f(x2:S) -> U8_1(d), id: 1, possubterms: f(x2:S)->[])
5.002/5.002	 (rule: h(x3:S,x3:S) -> A, id: 2, possubterms: h(x3:S,x3:S)->[])
5.002/5.002	 (rule: U8_1(l) -> e, id: 3, possubterms: U8_1(l)->[], l->[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.28user 0.02system 0:05.02elapsed 6%CPU (0avgtext+0avgdata 23576maxresident)k
5.002/5.002	0inputs+0outputs (0major+9337minor)pagefaults 0swaps