10.001/10.001	YES
10.001/10.001	
10.001/10.001	Problem 1:
10.001/10.001	
10.001/10.001	
10.001/10.001	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
10.001/10.001	Confluence Problem:
10.001/10.001	(VAR vNonEmpty:S x:S y:S z:S)
10.001/10.001	(STRATEGY CONTEXTSENSITIVE
10.001/10.001	(f 1 2)
10.001/10.001	(g 1)
10.001/10.001	(c)
10.001/10.001	(d)
10.001/10.001	(fSNonEmpty)
10.001/10.001	)
10.001/10.001	(RULES
10.001/10.001	f(x:S,y:S) -> x:S | g(x:S) ->* z:S, g(y:S) ->* z:S
10.001/10.001	g(x:S) -> c | d ->* c
10.001/10.001	)
10.001/10.001	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
10.001/10.001	
10.001/10.001	
10.001/10.001	Problem 1:
10.001/10.001	
10.001/10.001	Inlining of Conditions Processor [STERN17]:
10.001/10.001	
10.001/10.001	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
10.001/10.001	Confluence Problem:
10.001/10.001	(VAR vNonEmpty:S x:S y:S z:S)
10.001/10.001	(STRATEGY CONTEXTSENSITIVE
10.001/10.001	(f 1 2)
10.001/10.001	(g 1)
10.001/10.001	(c)
10.001/10.001	(d)
10.001/10.001	(fSNonEmpty)
10.001/10.001	)
10.001/10.001	(RULES
10.001/10.001	f(x:S,y:S) -> x:S | g(x:S) ->* z:S, g(y:S) ->* z:S
10.001/10.001	g(x:S) -> c | d ->* c
10.001/10.001	)
10.001/10.001	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
10.001/10.001	
10.001/10.001	
10.001/10.001	Problem 1:
10.001/10.001	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
10.001/10.001	Confluence Problem:
10.001/10.001	(VAR vNonEmpty:S x:S y:S z:S)
10.001/10.001	(STRATEGY CONTEXTSENSITIVE
10.001/10.001	(f 1 2)
10.001/10.001	(g 1)
10.001/10.001	(c)
10.001/10.001	(d)
10.001/10.001	(fSNonEmpty)
10.001/10.001	)
10.001/10.001	(RULES
10.001/10.001	f(x:S,y:S) -> x:S | g(x:S) ->* z:S, g(y:S) ->* z:S
10.001/10.001	g(x:S) -> c | d ->* c
10.001/10.001	)
10.001/10.001	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
10.001/10.001	
10.001/10.001	Critical Pairs Processor:
10.001/10.001	-> Rules:
10.001/10.001	f(x:S,y:S) -> x:S | g(x:S) ->* z:S, g(y:S) ->* z:S
10.001/10.001	g(x:S) -> c | d ->* c
10.001/10.001	-> Vars:
10.001/10.001	"x", "y", "z", "x"
10.001/10.001	-> FVars:
10.001/10.001	"x4", "x5", "x6", "x7"
10.001/10.001	-> PVars:
10.001/10.001	"x": ["x4", "x7"], "y": ["x5"], "z": ["x6"]
10.001/10.001	
10.001/10.001	-> Rlps:
10.001/10.001	crule: f(x4:S,x5:S) -> x4:S | g(x4:S) ->* x6:S, g(x5:S) ->* x6:S, id: 1, possubterms: f(x4:S,x5:S)-> []
10.001/10.001	crule: g(x7:S) -> c | d ->* c, id: 2, possubterms: g(x7:S)-> []
10.001/10.001	
10.001/10.001	-> Unifications:
10.001/10.001	
10.001/10.001	
10.001/10.001	-> Critical pairs info:
10.001/10.001	
10.001/10.001	
10.001/10.001	-> Problem conclusions:
10.001/10.001	 Left linear, Right linear, Linear
10.001/10.001	 Weakly orthogonal, Almost orthogonal, Orthogonal
10.001/10.001	 CTRS Type: 2
10.001/10.001	 Deterministic, Maybe strongly deterministic
10.001/10.001	 Oriented CTRS, Properly oriented CTRS, Not join CTRS
10.001/10.001	 Maybe right-stable CTRS, Overlay CTRS
10.001/10.001	 Maybe normal CTRS, Maybe almost normal CTRS
10.001/10.001	 Maybe terminating CTRS, Joinable CCPs
10.001/10.001	 Maybe level confluent
10.001/10.001	 Maybe confluent
10.001/10.001	
10.001/10.001	Problem 1:
10.001/10.001	Underlying TRS Termination Processor:
10.001/10.001	
10.001/10.001	Resulting Underlying TRS:
10.001/10.001	(VAR vNonEmpty:S x:S y:S z:S)
10.001/10.001	(STRATEGY CONTEXTSENSITIVE
10.001/10.001	(f 1 2)
10.001/10.001	(g 1)
10.001/10.001	(c)
10.001/10.001	)
10.001/10.001	(RULES
10.001/10.001	f(x:S,y:S) -> x:S
10.001/10.001	g(x:S) -> c
10.001/10.001	)
10.001/10.001	Underlying TRS terminating?
10.001/10.001	YES
10.001/10.001	
10.001/10.001	Problem 1:
10.001/10.001	
10.001/10.001	(VAR vu95NonEmpty:S vNonEmptyu58S:S xu58S:S yu58S:S zu58S:S)
10.001/10.001	(RULES
10.001/10.001	f(xu58S:S,yu58S:S) -> xu58S:S
10.001/10.001	g(xu58S:S) -> c
10.001/10.001	)
10.001/10.001	
10.001/10.001	Problem 1:
10.001/10.001	
10.001/10.001	Innermost Equivalent Processor:
10.001/10.001	-> Rules:
10.001/10.001	 f(xu58S:S,yu58S:S) -> xu58S:S
10.001/10.001	 g(xu58S:S) -> c
10.001/10.001	-> The term rewriting system is non-overlaping or locally confluent overlay system. Therefore, innermost termination implies termination.
10.001/10.001	
10.001/10.001	
10.001/10.001	Problem 1:
10.001/10.001	
10.001/10.001	Dependency Pairs Processor:
10.001/10.001	-> Pairs:
10.001/10.001	 Empty
10.001/10.001	-> Rules:
10.001/10.001	 f(xu58S:S,yu58S:S) -> xu58S:S
10.001/10.001	 g(xu58S:S) -> c
10.001/10.001	
10.001/10.001	Problem 1:
10.001/10.001	
10.001/10.001	SCC Processor:
10.001/10.001	-> Pairs:
10.001/10.001	 Empty
10.001/10.001	-> Rules:
10.001/10.001	 f(xu58S:S,yu58S:S) -> xu58S:S
10.001/10.001	 g(xu58S:S) -> c
10.001/10.001	->Strongly Connected Components:
10.001/10.001	 There is no strongly connected component
10.001/10.001	
10.001/10.001	The problem is finite.
10.001/10.001	
10.001/10.001	
10.001/10.001	-> Problem conclusions:
10.001/10.001	 Left linear, Right linear, Linear
10.001/10.001	 Weakly orthogonal, Almost orthogonal, Orthogonal
10.001/10.001	 CTRS Type: 2
10.001/10.001	 Deterministic, Maybe strongly deterministic
10.001/10.001	 Oriented CTRS, Properly oriented CTRS, Not join CTRS
10.001/10.001	 Maybe right-stable CTRS, Overlay CTRS
10.001/10.001	 Maybe normal CTRS, Maybe almost normal CTRS
10.001/10.001	 Terminating CTRS, Joinable CCPs
10.001/10.001	 Maybe level confluent
10.001/10.001	 Maybe confluent
10.001/10.001	
10.001/10.001	Problem 1:
10.001/10.001	
10.001/10.001	Transform CTRS Processor:
10.001/10.001	
10.001/10.001	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
10.001/10.001	Confluence Problem:
10.001/10.001	(VAR vNonEmpty:S x:S y:S z:S)
10.001/10.001	(STRATEGY CONTEXTSENSITIVE
10.001/10.001	(f 1 2)
10.001/10.001	(g 1)
10.001/10.001	(c)
10.001/10.001	(d)
10.001/10.001	(fSNonEmpty)
10.001/10.001	)
10.001/10.001	(RULES
10.001/10.001	f(x:S,y:S) -> x:S | g(x:S) ->* z:S, g(y:S) ->* z:S
10.001/10.001	g(x:S) -> c | d ->* c
10.001/10.001	)
10.001/10.001	Critical Pairs:
10.001/10.001	
10.001/10.001	Terminating:YES
10.001/10.001	
10.001/10.001	-> Problem conclusions:
10.001/10.001	 Left linear, Right linear, Linear
10.001/10.001	 Weakly orthogonal, Almost orthogonal, Orthogonal
10.001/10.001	 CTRS Type: 2
10.001/10.001	 Deterministic, Maybe strongly deterministic
10.001/10.001	 Oriented CTRS, Properly oriented CTRS, Not join CTRS
10.001/10.001	 Maybe right-stable CTRS, Overlay CTRS
10.001/10.001	 Maybe normal CTRS, Maybe almost normal CTRS
10.001/10.001	 Terminating CTRS, Joinable CCPs
10.001/10.001	 Maybe level confluent
10.001/10.001	 Maybe confluent
10.001/10.001	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
10.001/10.001	Resulting U(R):
10.001/10.001	(VAR vNonEmpty:S x:S y:S z:S)
10.001/10.001	(STRATEGY CONTEXTSENSITIVE
10.001/10.001	(f 1 2)
10.001/10.001	(g 1)
10.001/10.001	(c)
10.001/10.001	(d)
10.001/10.001	(fSNonEmpty)
10.001/10.001	(U6_1 1 2 3)
10.001/10.001	(U6_2 1 2 3)
10.001/10.001	(U8_1 1)
10.001/10.001	)
10.001/10.001	(RULES
10.001/10.001	f(x:S,y:S) -> U6_1(g(x:S),x:S,y:S)
10.001/10.001	g(x:S) -> U8_1(d)
10.001/10.001	U6_1(z:S,x:S,y:S) -> U6_2(g(y:S),x:S,z:S)
10.001/10.001	U6_2(z:S,x:S,z:S) -> x:S
10.001/10.001	U8_1(c) -> c
10.001/10.001	)
10.001/10.001	
10.001/10.001	Problem 1:
10.001/10.001	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
10.001/10.001	Confluence Problem:
10.001/10.001	(VAR vNonEmpty:S x:S y:S z:S)
10.001/10.001	(STRATEGY CONTEXTSENSITIVE
10.001/10.001	(f 1 2)
10.001/10.001	(g 1)
10.001/10.001	(c)
10.001/10.001	(d)
10.001/10.001	(fSNonEmpty)
10.001/10.001	(U6_1 1 2 3)
10.001/10.001	(U6_2 1 2 3)
10.001/10.001	(U8_1 1)
10.001/10.001	)
10.001/10.001	(RULES
10.001/10.001	f(x:S,y:S) -> U6_1(g(x:S),x:S,y:S)
10.001/10.001	g(x:S) -> U8_1(d)
10.001/10.001	U6_1(z:S,x:S,y:S) -> U6_2(g(y:S),x:S,z:S)
10.001/10.001	U6_2(z:S,x:S,z:S) -> x:S
10.001/10.001	U8_1(c) -> c
10.001/10.001	)
10.001/10.001	Terminating:"YES"
10.001/10.001	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
10.001/10.001	
10.001/10.001	Huet Levy Processor:
10.001/10.001	-> Rules:
10.001/10.001	 f(x:S,y:S) -> U6_1(g(x:S),x:S,y:S)
10.001/10.001	 g(x:S) -> U8_1(d)
10.001/10.001	 U6_1(z:S,x:S,y:S) -> U6_2(g(y:S),x:S,z:S)
10.001/10.001	 U6_2(z:S,x:S,z:S) -> x:S
10.001/10.001	 U8_1(c) -> c
10.001/10.001	-> Vars:
10.001/10.001	 x, y, x, x, y, z, x, z
10.001/10.001	-> FVars:
10.001/10.001	 x4, x5, x6, x7, x8, x9, x10, x11
10.001/10.001	-> PVars:
10.001/10.001	 x: [x4, x6, x7, x10], y: [x5, x8], z: [x9, x11]
10.001/10.001	
10.001/10.001	-> Rlps:
10.001/10.001	 (rule: f(x4:S,x5:S) -> U6_1(g(x4:S),x4:S,x5:S), id: 1, possubterms: f(x4:S,x5:S)->[])
10.001/10.001	 (rule: g(x6:S) -> U8_1(d), id: 2, possubterms: g(x6:S)->[])
10.001/10.001	 (rule: U6_1(x9:S,x7:S,x8:S) -> U6_2(g(x8:S),x7:S,x9:S), id: 3, possubterms: U6_1(x9:S,x7:S,x8:S)->[])
10.001/10.001	 (rule: U6_2(x11:S,x10:S,x11:S) -> x10:S, id: 4, possubterms: U6_2(x11:S,x10:S,x11:S)->[])
10.001/10.001	 (rule: U8_1(c) -> c, id: 5, possubterms: U8_1(c)->[], c->[1])
10.001/10.001	
10.001/10.001	-> Unifications:
10.001/10.001	
10.001/10.001	
10.001/10.001	-> Critical pairs info:
10.001/10.001	
10.001/10.001	
10.001/10.001	-> Problem conclusions:
10.001/10.001	 Not left linear, Not right linear, Not linear
10.001/10.001	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
10.001/10.001	 Not Huet-Levy confluent, Newman confluent
10.001/10.001	 R is a TRS
10.001/10.001	
10.001/10.001	
10.001/10.001	The problem is joinable.
10.001/10.001	1.28user 0.06system 0:10.01elapsed 13%CPU (0avgtext+0avgdata 31276maxresident)k
10.001/10.001	8inputs+0outputs (0major+21394minor)pagefaults 0swaps