0.003/0.003	NO
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	
0.003/0.003	
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	Confluence Problem:
0.003/0.003	(VAR vNonEmpty x z)
0.003/0.003	(REPLACEMENT-MAP
0.003/0.003	(c)
0.003/0.003	(f 1)
0.003/0.003	(g 1, 2)
0.003/0.003	(s 1)
0.003/0.003	(a)
0.003/0.003	(b)
0.003/0.003	(fSNonEmpty)
0.003/0.003	(h 1, 2)
0.003/0.003	(k)
0.003/0.003	(l)
0.003/0.003	(t 1)
0.003/0.003	)
0.003/0.003	(RULES
0.003/0.003	c -> t(k)
0.003/0.003	c -> t(l)
0.003/0.003	f(x) -> z | s(x) ->* z
0.003/0.003	g(x,x) -> h(x,x)
0.003/0.003	s(a) -> c
0.003/0.003	s(b) -> c
0.003/0.003	)
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	
0.003/0.003	Inlining of Conditions Processor [STERN17]:
0.003/0.003	
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	Confluence Problem:
0.003/0.003	(VAR vNonEmpty x z)
0.003/0.003	(REPLACEMENT-MAP
0.003/0.003	(c)
0.003/0.003	(f 1)
0.003/0.003	(g 1, 2)
0.003/0.003	(s 1)
0.003/0.003	(a)
0.003/0.003	(b)
0.003/0.003	(fSNonEmpty)
0.003/0.003	(h 1, 2)
0.003/0.003	(k)
0.003/0.003	(l)
0.003/0.003	(t 1)
0.003/0.003	)
0.003/0.003	(RULES
0.003/0.003	c -> t(k)
0.003/0.003	c -> t(l)
0.003/0.003	f(x) -> s(x)
0.003/0.003	g(x,x) -> h(x,x)
0.003/0.003	s(a) -> c
0.003/0.003	s(b) -> c
0.003/0.003	)
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	
0.003/0.003	Clean CTRS Processor:
0.003/0.003	
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	Confluence Problem:
0.003/0.003	(VAR x)
0.003/0.003	(REPLACEMENT-MAP
0.003/0.003	(c)
0.003/0.003	(f 1)
0.003/0.003	(g 1, 2)
0.003/0.003	(s 1)
0.003/0.003	(a)
0.003/0.003	(b)
0.003/0.003	(fSNonEmpty)
0.003/0.003	(h 1, 2)
0.003/0.003	(k)
0.003/0.003	(l)
0.003/0.003	(t 1)
0.003/0.003	)
0.003/0.003	(RULES
0.003/0.003	c -> t(k)
0.003/0.003	c -> t(l)
0.003/0.003	f(x) -> s(x)
0.003/0.003	g(x,x) -> h(x,x)
0.003/0.003	s(a) -> c
0.003/0.003	s(b) -> c
0.003/0.003	)
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	
0.003/0.003	CRule InfChecker Info:
0.003/0.003	c -> t(k)
0.003/0.003	Rule remains
0.003/0.003	Proof:
0.003/0.003	NO_CONDS
0.003/0.003	
0.003/0.003	CRule InfChecker Info:
0.003/0.003	c -> t(l)
0.003/0.003	Rule remains
0.003/0.003	Proof:
0.003/0.003	NO_CONDS
0.003/0.003	
0.003/0.003	CRule InfChecker Info:
0.003/0.003	f(x) -> s(x)
0.003/0.003	Rule remains
0.003/0.003	Proof:
0.003/0.003	NO_CONDS
0.003/0.003	
0.003/0.003	CRule InfChecker Info:
0.003/0.003	g(x,x) -> h(x,x)
0.003/0.003	Rule remains
0.003/0.003	Proof:
0.003/0.003	NO_CONDS
0.003/0.003	
0.003/0.003	CRule InfChecker Info:
0.003/0.003	s(a) -> c
0.003/0.003	Rule remains
0.003/0.003	Proof:
0.003/0.003	NO_CONDS
0.003/0.003	
0.003/0.003	CRule InfChecker Info:
0.003/0.003	s(b) -> c
0.003/0.003	Rule remains
0.003/0.003	Proof:
0.003/0.003	NO_CONDS
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	
0.003/0.003	Transform No Conds CTRS Processor:
0.003/0.003	
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	Confluence Problem:
0.003/0.003	(VAR x)
0.003/0.003	(REPLACEMENT-MAP
0.003/0.003	(c)
0.003/0.003	(f 1)
0.003/0.003	(g 1, 2)
0.003/0.003	(s 1)
0.003/0.003	(a)
0.003/0.003	(b)
0.003/0.003	(fSNonEmpty)
0.003/0.003	(h 1, 2)
0.003/0.003	(k)
0.003/0.003	(l)
0.003/0.003	(t 1)
0.003/0.003	)
0.003/0.003	(RULES
0.003/0.003	c -> t(k)
0.003/0.003	c -> t(l)
0.003/0.003	f(x) -> s(x)
0.003/0.003	g(x,x) -> h(x,x)
0.003/0.003	s(a) -> c
0.003/0.003	s(b) -> c
0.003/0.003	)
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	Resulting R:
0.003/0.003	(VAR x)
0.003/0.003	(STRATEGY CONTEXTSENSITIVE
0.003/0.003	(c)
0.003/0.003	(f 1)
0.003/0.003	(g 1 2)
0.003/0.003	(s 1)
0.003/0.003	(a)
0.003/0.003	(b)
0.003/0.003	(fSNonEmpty)
0.003/0.003	(h 1 2)
0.003/0.003	(k)
0.003/0.003	(l)
0.003/0.003	(t 1)
0.003/0.003	)
0.003/0.003	(RULES
0.003/0.003	c -> t(k)
0.003/0.003	c -> t(l)
0.003/0.003	f(x) -> s(x)
0.003/0.003	g(x,x) -> h(x,x)
0.003/0.003	s(a) -> c
0.003/0.003	s(b) -> c
0.003/0.003	)
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	
0.003/0.003	CleanTRS Processor:
0.003/0.003	
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	Confluence Problem:
0.003/0.003	(VAR x)
0.003/0.003	(REPLACEMENT-MAP
0.003/0.003	(c)
0.003/0.003	(f 1)
0.003/0.003	(g 1, 2)
0.003/0.003	(s 1)
0.003/0.003	(a)
0.003/0.003	(b)
0.003/0.003	(fSNonEmpty)
0.003/0.003	(h 1, 2)
0.003/0.003	(k)
0.003/0.003	(l)
0.003/0.003	(t 1)
0.003/0.003	)
0.003/0.003	(RULES
0.003/0.003	c -> t(k)
0.003/0.003	c -> t(l)
0.003/0.003	f(x) -> s(x)
0.003/0.003	g(x,x) -> h(x,x)
0.003/0.003	s(a) -> c
0.003/0.003	s(b) -> c
0.003/0.003	)
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	
0.003/0.003	Modular Confluence Combinations Decomposition Processor:
0.003/0.003	
0.003/0.003	TRS combination:
0.003/0.003	{c -> t(k)
0.003/0.003	 c -> t(l)
0.003/0.003	 f(x) -> s(x)
0.003/0.003	 s(a) -> c
0.003/0.003	 s(b) -> c}
0.003/0.003	{g(x,x) -> h(x,x)}
0.003/0.003	Disjoint
0.003/0.003	Constructor-sharing
0.003/0.003	Not left linear
0.003/0.003	Layer-preserving
0.003/0.003	TRS1
0.003/0.003	Just (VAR x)
0.003/0.003	(STRATEGY CONTEXTSENSITIVE
0.003/0.003	(c)
0.003/0.003	(f 1)
0.003/0.003	(s 1)
0.003/0.003	(a)
0.003/0.003	(b)
0.003/0.003	(k)
0.003/0.003	(l)
0.003/0.003	(t 1)
0.003/0.003	)
0.003/0.003	(RULES
0.003/0.003	c -> t(k)
0.003/0.003	c -> t(l)
0.003/0.003	f(x) -> s(x)
0.003/0.003	s(a) -> c
0.003/0.003	s(b) -> c
0.003/0.003	)
0.003/0.003	
0.003/0.003	TRS2
0.003/0.003	Just (VAR x)
0.003/0.003	(STRATEGY CONTEXTSENSITIVE
0.003/0.003	(g 1 2)
0.003/0.003	(h 1 2)
0.003/0.003	)
0.003/0.003	(RULES
0.003/0.003	g(x,x) -> h(x,x)
0.003/0.003	)
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	Confluence Problem:
0.003/0.003	(VAR x)
0.003/0.003	(REPLACEMENT-MAP
0.003/0.003	(c)
0.003/0.003	(f 1)
0.003/0.003	(s 1)
0.003/0.003	(a)
0.003/0.003	(b)
0.003/0.003	(k)
0.003/0.003	(l)
0.003/0.003	(t 1)
0.003/0.003	)
0.003/0.003	(RULES
0.003/0.003	c -> t(k)
0.003/0.003	c -> t(l)
0.003/0.003	f(x) -> s(x)
0.003/0.003	s(a) -> c
0.003/0.003	s(b) -> c
0.003/0.003	)
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	
0.003/0.003	Huet Levy Processor:
0.003/0.003	-> Rules:
0.003/0.003	 c -> t(k)
0.003/0.003	 c -> t(l)
0.003/0.003	 f(x) -> s(x)
0.003/0.003	 s(a) -> c
0.003/0.003	 s(b) -> c
0.003/0.003	-> Vars:
0.003/0.003	 x
0.003/0.003	
0.003/0.003	-> Rlps:
0.003/0.003	 (rule: c -> t(k), id: 1, possubterms: c->[])
0.003/0.003	 (rule: c -> t(l), id: 2, possubterms: c->[])
0.003/0.003	 (rule: f(x) -> s(x), id: 3, possubterms: f(x)->[])
0.003/0.003	 (rule: s(a) -> c, id: 4, possubterms: s(a)->[], a->[1])
0.003/0.003	 (rule: s(b) -> c, id: 5, possubterms: s(b)->[], b->[1])
0.003/0.003	
0.003/0.003	-> Unifications:
0.003/0.003	(R2 unifies with R1 at p: [], l: c, lp: c, sig: {}, l': c, r: t(l), r': t(k))
0.003/0.003	
0.003/0.003	-> Critical pairs info:
0.003/0.003	<t(k),t(l)>   =>  Not trivial, Overlay, NW0, N1
0.003/0.003	
0.003/0.003	-> Problem conclusions:
0.003/0.003	 Left linear, Right linear, Linear
0.003/0.003	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
0.003/0.003	 Not Huet-Levy confluent, Not Newman confluent
0.003/0.003	 R is a TRS
0.003/0.003	
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	Different Normal CP Terms Processor:
0.003/0.003	<t(k),t(l)>   =>  Not trivial, Overlay, NW0, N1, Normal and not trivial cp
0.003/0.003	
0.003/0.003	The problem is not joinable.
0.003/0.003	0.00user 0.01system 0:00.03elapsed 54%CPU (0avgtext+0avgdata 9636maxresident)k
0.003/0.003	8inputs+0outputs (0major+1401minor)pagefaults 0swaps