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	(g 1)
5.002/5.002	(a)
5.002/5.002	(b)
5.002/5.002	(f 1 2)
5.002/5.002	(fSNonEmpty)
5.002/5.002	)
5.002/5.002	(RULES
5.002/5.002	g(x:S) -> g(x:S) | g(x:S) ->* f(a,b)
5.002/5.002	g(x:S) -> f(x:S,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	(g 1)
5.002/5.002	(a)
5.002/5.002	(b)
5.002/5.002	(f 1 2)
5.002/5.002	(fSNonEmpty)
5.002/5.002	)
5.002/5.002	(RULES
5.002/5.002	g(x:S) -> g(x:S) | g(x:S) ->* f(a,b)
5.002/5.002	g(x:S) -> f(x:S,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	Clean CTRS Processor:
5.002/5.002	
5.002/5.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
5.002/5.002	Confluence Problem:
5.002/5.002	(VAR x:S)
5.002/5.002	(STRATEGY CONTEXTSENSITIVE
5.002/5.002	(g 1)
5.002/5.002	(a)
5.002/5.002	(b)
5.002/5.002	(f 1 2)
5.002/5.002	(fSNonEmpty)
5.002/5.002	)
5.002/5.002	(RULES
5.002/5.002	g(x:S) -> f(x:S,x:S)
5.002/5.002	)
5.002/5.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
5.002/5.002	
5.002/5.002	CRule InfChecker Info:
5.002/5.002	g(x:S) -> g(x:S) | g(x:S) ->* f(a,b)
5.002/5.002	Rule deleted
5.002/5.002	Proof:
5.002/5.002	SAME_LHS_AND_RHS
5.002/5.002	
5.002/5.002	CRule InfChecker Info:
5.002/5.002	g(x:S) -> f(x:S,x:S)
5.002/5.002	Rule remains
5.002/5.002	Proof:
5.002/5.002	NO_CONDS
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 x:S)
5.002/5.002	(STRATEGY CONTEXTSENSITIVE
5.002/5.002	(g 1)
5.002/5.002	(a)
5.002/5.002	(b)
5.002/5.002	(f 1 2)
5.002/5.002	(fSNonEmpty)
5.002/5.002	)
5.002/5.002	(RULES
5.002/5.002	g(x:S) -> f(x:S,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	g(x:S) -> f(x:S,x:S)
5.002/5.002	-> Vars:
5.002/5.002	"x"
5.002/5.002	-> FVars:
5.002/5.002	"x2"
5.002/5.002	-> PVars:
5.002/5.002	"x": ["x2"]
5.002/5.002	
5.002/5.002	-> Rlps:
5.002/5.002	crule: g(x2:S) -> f(x2:S,x2:S), id: 1, possubterms: g(x2: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	 Left linear, Not right linear, Not linear
5.002/5.002	 Weakly orthogonal, Almost orthogonal, Orthogonal
5.002/5.002	 CTRS Type: 1
5.002/5.002	 Deterministic, Strongly deterministic
5.002/5.002	 Oriented CTRS, Properly oriented CTRS, Join CTRS
5.002/5.002	 Maybe right-stable CTRS, Overlay CTRS
5.002/5.002	 Normal CTRS, Almost normal CTRS
5.002/5.002	 Maybe terminating CTRS, Joinable CCPs
5.002/5.002	 Level confluent
5.002/5.002	 Confluent
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 23756maxresident)k
5.002/5.002	8inputs+0outputs (0major+9318minor)pagefaults 0swaps