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