NO

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(B 1)
(W 1)
(I 1)
(S 1)
(fSNonEmpty)
)
(RULES
B(S(x)) -> S(x)
W(B(x)) -> I(x)
W(x) -> I(x)
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

Problem 1: 
Not CS-TRS Procedure:
R is not a CS-TRS

Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(B 1)
(W 1)
(I 1)
(S 1)
(fSNonEmpty)
)
(RULES
B(S(x)) -> S(x)
W(B(x)) -> I(x)
W(x) -> I(x)
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 B(S(x)) -> S(x)
 W(B(x)) -> I(x)
 W(x) -> I(x)
-> Vars:
 x, x, x

-> Rlps:
 (rule: B(S(x)) -> S(x), id: 1, possubterms: B(S(x))->[], S(x)->[1])
 (rule: W(B(x)) -> I(x), id: 2, possubterms: W(B(x))->[], B(x)->[1])
 (rule: W(x) -> I(x), id: 3, possubterms: W(x)->[])

-> Unifications:
(R2 unifies with R1 at p: [1], l: W(B(x)), lp: B(x), sig: {x -> S(x')}, l': B(S(x')), r: I(x), r': S(x'))
(R3 unifies with R2 at p: [], l: W(x), lp: W(x), sig: {x -> B(x')}, l': W(B(x')), r: I(x), r': I(x'))

-> Critical pairs info:
<W(S(x')),I(S(x'))>   =>  Not trivial, Not overlay, Proper, NW0, N1
<I(x'),I(B(x'))>   =>  Not trivial, Overlay, Proper, NW0, N2

-> Problem conclusions:
 Left linear, Right linear, Linear
 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
 Not Huet-Levy confluent, Not Newman confluent
 R is a TRS 


Problem 1: 
No Convergence Brute Force Procedure:
-> Rewritings:
s: I(x')
Nodes: [0]
Edges: []
ID: 0 => ('I(x')', D0)
t: I(B(x'))
Nodes: [0]
Edges: []
ID: 0 => ('I(B(x'))', D0)
I(x') ->* no union *<- I(B(x'))
"Not joinable"

The problem is not confluent.