0.002/0.002	NO
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 y)
0.002/0.002	(REPLACEMENT-MAP
0.002/0.002	(G 1, 2)
0.002/0.002	(f 1)
0.002/0.002	(a)
0.002/0.002	(b)
0.002/0.002	(fSNonEmpty)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	G(x,y) -> x
0.002/0.002	G(x,y) -> y
0.002/0.002	f(x) -> f(x) | x ->*<- a, x ->*<- b
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 y)
0.002/0.002	(REPLACEMENT-MAP
0.002/0.002	(G 1, 2)
0.002/0.002	(f 1)
0.002/0.002	(a)
0.002/0.002	(b)
0.002/0.002	(fSNonEmpty)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	G(x,y) -> x
0.002/0.002	G(x,y) -> y
0.002/0.002	f(x) -> f(x) | x ->*<- a, x ->*<- b
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 y)
0.002/0.002	(REPLACEMENT-MAP
0.002/0.002	(G 1, 2)
0.002/0.002	(f 1)
0.002/0.002	(a)
0.002/0.002	(b)
0.002/0.002	(fSNonEmpty)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	G(x,y) -> x
0.002/0.002	G(x,y) -> y
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,y) -> 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	CRule InfChecker Info:
0.002/0.002	G(x,y) -> y
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	CRule InfChecker Info:
0.002/0.002	f(x) -> f(x) | x ->*<- a, x ->*<- 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	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 y)
0.002/0.002	(REPLACEMENT-MAP
0.002/0.002	(G 1, 2)
0.002/0.002	(f 1)
0.002/0.002	(a)
0.002/0.002	(b)
0.002/0.002	(fSNonEmpty)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	G(x,y) -> x
0.002/0.002	G(x,y) -> y
0.002/0.002	)
0.002/0.002	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	Resulting R:
0.002/0.002	(VAR x y)
0.002/0.002	(STRATEGY CONTEXTSENSITIVE
0.002/0.002	(G 1 2)
0.002/0.002	(f 1)
0.002/0.002	(a)
0.002/0.002	(b)
0.002/0.002	(fSNonEmpty)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	G(x,y) -> x
0.002/0.002	G(x,y) -> y
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 y)
0.002/0.002	(REPLACEMENT-MAP
0.002/0.002	(G 1, 2)
0.002/0.002	(f 1)
0.002/0.002	(a)
0.002/0.002	(b)
0.002/0.002	(fSNonEmpty)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	G(x,y) -> x
0.002/0.002	G(x,y) -> y
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	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.002/0.002	Confluence Problem:
0.002/0.002	(VAR x y)
0.002/0.002	(REPLACEMENT-MAP
0.002/0.002	(G 1, 2)
0.002/0.002	(f 1)
0.002/0.002	(a)
0.002/0.002	(b)
0.002/0.002	(fSNonEmpty)
0.002/0.002	)
0.002/0.002	(RULES
0.002/0.002	G(x,y) -> x
0.002/0.002	G(x,y) -> y
0.002/0.002	)
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,y) -> x
0.002/0.002	 G(x,y) -> y
0.002/0.002	-> Vars:
0.002/0.002	 x, y, x, y
0.002/0.002	
0.002/0.002	-> Rlps:
0.002/0.002	 (rule: G(x,y) -> x, id: 1, possubterms: G(x,y)->[])
0.002/0.002	 (rule: G(x,y) -> y, id: 2, possubterms: G(x,y)->[])
0.002/0.002	
0.002/0.002	-> Unifications:
0.002/0.002	(R2 unifies with R1 at p: [], l: G(x,y), lp: G(x,y), sig: {x -> x',y -> y'}, l': G(x',y'), r: y, r': x')
0.002/0.002	
0.002/0.002	-> Critical pairs info:
0.002/0.002	<x',y'>   =>  Not trivial, Overlay, NW0, N1
0.002/0.002	
0.002/0.002	-> Problem conclusions:
0.002/0.002	 Left linear, Right linear, Linear
0.002/0.002	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
0.002/0.002	 Not 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	Problem 1:
0.002/0.002	Different Normal CP Terms Processor:
0.002/0.002	<x',y'>   =>  Not trivial, Overlay, NW0, N1, Normal and not trivial cp
0.002/0.002	
0.002/0.002	The problem is not joinable.
0.002/0.002	0.00user 0.00system 0:00.02elapsed 58%CPU (0avgtext+0avgdata 9180maxresident)k
0.002/0.002	0inputs+0outputs (0major+1291minor)pagefaults 0swaps