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