YES

Problem 1: 


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


Problem 1: 

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

Problem 1: 
Linearity Procedure:
Linear?
YES

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

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

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

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

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

-> 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.1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(B 1)
(W 1)
(I 1)
(J 1)
(fSNonEmpty)
)
(RULES
B(I(x)) -> J(x)
W(B(x)) -> W(x)
W(I(x)) -> W(J(x))
)
Critical Pairs:
<W(J(x')),W(I(x'))>   =>  Not trivial, Not overlay, Proper, NW0, N1
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Strong Confluence Procedure:
-> Rewritings:
s: W(J(x'))
Nodes: [0]
Edges: []
ID: 0 => ('W(J(x'))', D0)
t: W(I(x'))
Nodes: [0,1]
Edges: [(0,1)]
ID: 0 => ('W(I(x'))', D0)
ID: 1 => ('W(J(x'))', D1, R3, P[], S{x6 -> x'}), NR: 'W(J(x'))'
SNodesPath1: W(J(x'))
TNodesPath1: W(I(x')) -> W(J(x'))
SNodesPath2: W(J(x'))
TNodesPath2: W(I(x')) -> W(J(x'))
W(J(x')) ->= W(J(x')) *<- W(I(x'))
W(I(x')) ->= W(J(x')) *<- W(J(x'))
"Strongly closed critical pair"

The problem is confluent.