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