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	Transform No Conds 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	Resulting R:
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	Problem 1:
5.002/5.002	
5.002/5.002	CleanTRS 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	
5.002/5.002	Problem 1:
5.002/5.002	
5.002/5.002	Modular Confluence Combinations Decomposition Processor:
5.002/5.002	
5.002/5.002	No usable combinations
5.002/5.002	
5.002/5.002	Problem 1:
5.002/5.002	Linearity Processor:
5.002/5.002	Linear?
5.002/5.002	NO
5.002/5.002	Problem 1.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	Linear:NO
5.002/5.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
5.002/5.002	
5.002/5.002	Huet Levy 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	 (rule: 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	 Huet-Levy confluent, Not 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.27user 0.03system 0:05.02elapsed 6%CPU (0avgtext+0avgdata 23748maxresident)k
5.002/5.002	0inputs+0outputs (0major+9325minor)pagefaults 0swaps