0.002/0.002	YES
0.002/0.002	
0.002/0.002	Problem 1:
0.002/0.002	
0.002/0.002	
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	Confluence Problem:
0.002/0.002	(VAR vNonEmpty x)
0.002/0.002	(REPLACEMENT-MAP
0.002/0.002	(g 1)
0.002/0.002	(a)
0.002/0.002	(b)
0.002/0.002	(f 1, 2)
0.002/0.002	(fSNonEmpty)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	g(x) -> g(x) | g(x) ->* f(a,b)
0.002/0.002	g(x) -> f(x,x)
0.002/0.002	)
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	
0.002/0.002	
0.002/0.002	Problem 1:
0.002/0.002	
0.002/0.002	Inlining of Conditions Processor [STERN17]:
0.002/0.002	
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	Confluence Problem:
0.002/0.002	(VAR vNonEmpty x)
0.002/0.002	(REPLACEMENT-MAP
0.002/0.002	(g 1)
0.002/0.002	(a)
0.002/0.002	(b)
0.002/0.002	(f 1, 2)
0.002/0.002	(fSNonEmpty)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	g(x) -> g(x) | g(x) ->* f(a,b)
0.002/0.002	g(x) -> f(x,x)
0.002/0.002	)
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	
0.002/0.002	
0.002/0.002	Problem 1:
0.002/0.002	
0.002/0.002	Clean CTRS Processor:
0.002/0.002	
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	Confluence Problem:
0.002/0.002	(VAR x)
0.002/0.002	(REPLACEMENT-MAP
0.002/0.002	(g 1)
0.002/0.002	(a)
0.002/0.002	(b)
0.002/0.002	(f 1, 2)
0.002/0.002	(fSNonEmpty)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	g(x) -> f(x,x)
0.002/0.002	)
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	
0.002/0.002	CRule InfChecker Info:
0.002/0.002	g(x) -> g(x) | g(x) ->* f(a,b)
0.002/0.002	Rule deleted
0.002/0.002	Proof:
0.002/0.002	SAME_LHS_AND_RHS
0.002/0.002	
0.002/0.002	CRule InfChecker Info:
0.002/0.002	g(x) -> f(x,x)
0.002/0.002	Rule remains
0.002/0.002	Proof:
0.002/0.002	NO_CONDS
0.002/0.002	
0.002/0.002	Problem 1:
0.002/0.002	
0.002/0.002	Transform No Conds CTRS Processor:
0.002/0.002	
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	Confluence Problem:
0.002/0.002	(VAR x)
0.002/0.002	(REPLACEMENT-MAP
0.002/0.002	(g 1)
0.002/0.002	(a)
0.002/0.002	(b)
0.002/0.002	(f 1, 2)
0.002/0.002	(fSNonEmpty)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	g(x) -> f(x,x)
0.002/0.002	)
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	Resulting R:
0.002/0.002	(VAR x)
0.002/0.002	(STRATEGY CONTEXTSENSITIVE
0.002/0.002	(g 1)
0.002/0.002	(a)
0.002/0.002	(b)
0.002/0.002	(f 1 2)
0.002/0.002	(fSNonEmpty)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	g(x) -> f(x,x)
0.002/0.002	)
0.002/0.002	
0.002/0.002	Problem 1:
0.002/0.002	
0.002/0.002	CleanTRS Processor:
0.002/0.002	
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	Confluence Problem:
0.002/0.002	(VAR x)
0.002/0.002	(REPLACEMENT-MAP
0.002/0.002	(g 1)
0.002/0.002	(a)
0.002/0.002	(b)
0.002/0.002	(f 1, 2)
0.002/0.002	(fSNonEmpty)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	g(x) -> f(x,x)
0.002/0.002	)
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	
0.002/0.002	
0.002/0.002	Problem 1:
0.002/0.002	
0.002/0.002	Modular Confluence Combinations Decomposition Processor:
0.002/0.002	
0.002/0.002	No usable combinations
0.002/0.002	
0.002/0.002	Problem 1:
0.002/0.002	Linearity Processor:
0.002/0.002	Linear?
0.002/0.002	NO
0.002/0.002	Problem 1.1:
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	Confluence Problem:
0.002/0.002	(VAR x)
0.002/0.002	(REPLACEMENT-MAP
0.002/0.002	(g 1)
0.002/0.002	(a)
0.002/0.002	(b)
0.002/0.002	(f 1, 2)
0.002/0.002	(fSNonEmpty)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	g(x) -> f(x,x)
0.002/0.002	)
0.002/0.002	Linear:NO
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	
0.002/0.002	Huet Levy Processor:
0.002/0.002	-> Rules:
0.002/0.002	 g(x) -> f(x,x)
0.002/0.002	-> Vars:
0.002/0.002	 x
0.002/0.002	
0.002/0.002	-> Rlps:
0.002/0.002	 (rule: g(x) -> f(x,x), id: 1, possubterms: g(x)->[])
0.002/0.002	
0.002/0.002	-> Unifications:
0.002/0.002	
0.002/0.002	
0.002/0.002	-> Critical pairs info:
0.002/0.002	
0.002/0.002	
0.002/0.002	-> Problem conclusions:
0.002/0.002	 Left linear, Not right linear, Not linear
0.002/0.002	 Weakly orthogonal, Almost orthogonal, Orthogonal
0.002/0.002	 Huet-Levy confluent, Not Newman confluent
0.002/0.002	 R is a TRS
0.002/0.002	
0.002/0.002	
0.002/0.002	The problem is joinable.
0.002/0.002	0.01user 0.00system 0:00.02elapsed 52%CPU (0avgtext+0avgdata 9180maxresident)k
0.002/0.002	8inputs+0outputs (0major+1284minor)pagefaults 0swaps