YES

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y)
(REPLACEMENT-MAP
(B 1)
(F 1, 2)
(G 1)
(W 1)
(H 1)
(I 1)
(fSNonEmpty)
)
(RULES
B(I(x)) -> W(x)
F(H(x),y) -> F(H(x),G(y))
F(x,I(y)) -> F(G(x),I(y))
G(x) -> x
W(B(x)) -> B(x)
W(W(x)) -> W(x)
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

Problem 1: 

Modular Confluence Combinations Decomposition Procedure:
TRS combination:
{B(I(x)) -> W(x)
 W(B(x)) -> B(x)
 W(W(x)) -> W(x)}
{F(H(x),y) -> F(H(x),G(y))
 F(x,I(y)) -> F(G(x),I(y))
 G(x) -> x}
Not disjoint
Constructor-sharing
Not composable
Left linear
Not layer-preserving
TRS1
Just (VAR x)
(STRATEGY CONTEXTSENSITIVE
(B 1)
(W 1)
(I 1)
)
(RULES
B(I(x)) -> W(x)
W(B(x)) -> B(x)
W(W(x)) -> W(x)
)

TRS2
Just (VAR x y)
(STRATEGY CONTEXTSENSITIVE
(F 1 2)
(G 1)
(H 1)
(I 1)
)
(RULES
F(H(x),y) -> F(H(x),G(y))
F(x,I(y)) -> F(G(x),I(y))
G(x) -> x
)


The problem is decomposed in 2 subproblems.

Problem 1.1: 


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


Problem 1.1: 

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

Problem 1.1: 
Linearity Procedure:
Linear?
YES

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

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

-> Rlps:
 (rule: B(I(x)) -> W(x), id: 1, possubterms: B(I(x))->[], I(x)->[1])
 (rule: W(B(x)) -> B(x), id: 2, possubterms: W(B(x))->[], B(x)->[1])
 (rule: W(W(x)) -> W(x), id: 3, possubterms: W(W(x))->[], W(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: B(x), r': W(x'))
(R3 unifies with R2 at p: [1], l: W(W(x)), lp: W(x), sig: {x -> B(x')}, l': W(B(x')), r: W(x), r': B(x'))
(R3 unifies with R3 at p: [1], l: W(W(x)), lp: W(x), sig: {x -> W(x')}, l': W(W(x')), r: W(x), r': W(x'))

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

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

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

The problem is confluent.

Problem 1.2: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x y)
(REPLACEMENT-MAP
(F 1, 2)
(G 1)
(H 1)
(I 1)
)
(RULES
F(H(x),y) -> F(H(x),G(y))
F(x,I(y)) -> F(G(x),I(y))
G(x) -> x
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1.2: 

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

Problem 1.2: 
Linearity Procedure:
Linear?
YES

Problem 1.2: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x y)
(REPLACEMENT-MAP
(F 1, 2)
(G 1)
(H 1)
(I 1)
)
(RULES
F(H(x),y) -> F(H(x),G(y))
F(x,I(y)) -> F(G(x),I(y))
G(x) -> x
)
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 F(H(x),y) -> F(H(x),G(y))
 F(x,I(y)) -> F(G(x),I(y))
 G(x) -> x
-> Vars:
 x, y, x, y, x

-> Rlps:
 (rule: F(H(x),y) -> F(H(x),G(y)), id: 1, possubterms: F(H(x),y)->[], H(x)->[1])
 (rule: F(x,I(y)) -> F(G(x),I(y)), id: 2, possubterms: F(x,I(y))->[], I(y)->[2])
 (rule: G(x) -> x, id: 3, possubterms: G(x)->[])

-> Unifications:
(R2 unifies with R1 at p: [], l: F(x,I(y)), lp: F(x,I(y)), sig: {x -> H(x'),y' -> I(y)}, l': F(H(x'),y'), r: F(G(x),I(y)), r': F(H(x'),G(y')))

-> Critical pairs info:
<F(H(x'),G(I(y))),F(G(H(x')),I(y))>   =>  Not trivial, 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.2.1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x y x')
(REPLACEMENT-MAP
(F 1, 2)
(G 1)
(H 1)
(I 1)
)
(RULES
F(H(x),y) -> F(H(x),G(y))
F(x,I(y)) -> F(G(x),I(y))
G(x) -> x
)
Critical Pairs:
<F(H(x'),G(I(y))),F(G(H(x')),I(y))>   =>  Not trivial, Overlay, Proper, NW0, N1
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Strong Confluence Procedure:
-> Rewritings:
s: F(H(x'),G(I(y)))
Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16]
Edges: [(0,1),(0,2),(1,0),(1,0),(1,3),(2,0),(2,4),(3,1),(3,1),(3,1),(3,5),(4,2),(4,6),(5,3),(5,3),(5,3),(5,3),(5,7),(6,4),(6,4),(6,8),(7,5),(7,5),(7,5),(7,5),(7,5),(7,9),(8,6),(8,6),(8,6),(8,10),(9,7),(9,7),(9,7),(9,7),(9,7),(9,7),(9,11),(10,8),(10,8),(10,8),(10,8),(10,12),(11,9),(11,9),(11,9),(11,9),(11,9),(11,9),(11,9),(11,13),(12,10),(12,10),(12,10),(12,10),(12,10),(12,14),(13,11),(13,11),(13,11),(13,11),(13,11),(13,11),(13,11),(13,11),(13,15),(14,12),(14,12),(14,12),(14,12),(14,12),(14,12),(14,16)]
ID: 0 => ('F(H(x'),G(I(y)))', D0)
ID: 1 => ('F(H(x'),G(G(I(y))))', D1, R1, P[], S{x5 -> x', x6 -> G(I(y))}), NR: 'F(H(x'),G(G(I(y))))'
ID: 2 => ('F(H(x'),I(y))', D1, R3, P[2], S{x9 -> I(y)}), NR: 'I(y)'
ID: 3 => ('F(H(x'),G(G(G(I(y)))))', D2, R1, P[], S{x5 -> x', x6 -> G(G(I(y)))}), NR: 'F(H(x'),G(G(G(I(y)))))'
ID: 4 => ('F(G(H(x')),I(y))', D2, R2, P[], S{x7 -> H(x'), x8 -> y}), NR: 'F(G(H(x')),I(y))'
ID: 5 => ('F(H(x'),G(G(G(G(I(y))))))', D3, R1, P[], S{x5 -> x', x6 -> G(G(G(I(y))))}), NR: 'F(H(x'),G(G(G(G(I(y))))))'
ID: 6 => ('F(G(G(H(x'))),I(y))', D3, R2, P[], S{x7 -> G(H(x')), x8 -> y}), NR: 'F(G(G(H(x'))),I(y))'
ID: 7 => ('F(H(x'),G(G(G(G(G(I(y)))))))', D4, R1, P[], S{x5 -> x', x6 -> G(G(G(G(I(y)))))}), NR: 'F(H(x'),G(G(G(G(G(I(y)))))))'
ID: 8 => ('F(G(G(G(H(x')))),I(y))', D4, R2, P[], S{x7 -> G(G(H(x'))), x8 -> y}), NR: 'F(G(G(G(H(x')))),I(y))'
ID: 9 => ('F(H(x'),G(G(G(G(G(G(I(y))))))))', D5, R1, P[], S{x5 -> x', x6 -> G(G(G(G(G(I(y))))))}), NR: 'F(H(x'),G(G(G(G(G(G(I(y))))))))'
ID: 10 => ('F(G(G(G(G(H(x'))))),I(y))', D5, R2, P[], S{x7 -> G(G(G(H(x')))), x8 -> y}), NR: 'F(G(G(G(G(H(x'))))),I(y))'
ID: 11 => ('F(H(x'),G(G(G(G(G(G(G(I(y)))))))))', D6, R1, P[], S{x5 -> x', x6 -> G(G(G(G(G(G(I(y)))))))}), NR: 'F(H(x'),G(G(G(G(G(G(G(I(y)))))))))'
ID: 12 => ('F(G(G(G(G(G(H(x')))))),I(y))', D6, R2, P[], S{x7 -> G(G(G(G(H(x'))))), x8 -> y}), NR: 'F(G(G(G(G(G(H(x')))))),I(y))'
ID: 13 => ('F(H(x'),G(G(G(G(G(G(G(G(I(y))))))))))', D7, R1, P[], S{x5 -> x', x6 -> G(G(G(G(G(G(G(I(y))))))))}), NR: 'F(H(x'),G(G(G(G(G(G(G(G(I(y))))))))))'
ID: 14 => ('F(G(G(G(G(G(G(H(x'))))))),I(y))', D7, R2, P[], S{x7 -> G(G(G(G(G(H(x')))))), x8 -> y}), NR: 'F(G(G(G(G(G(G(H(x'))))))),I(y))'
ID: 15 => ('F(H(x'),G(G(G(G(G(G(G(G(G(I(y)))))))))))', D8, R1, P[], S{x5 -> x', x6 -> G(G(G(G(G(G(G(G(I(y)))))))))}), NR: 'F(H(x'),G(G(G(G(G(G(G(G(G(I(y)))))))))))'
ID: 16 => ('F(G(G(G(G(G(G(G(H(x')))))))),I(y))', D8, R2, P[], S{x7 -> G(G(G(G(G(G(H(x'))))))), x8 -> y}), NR: 'F(G(G(G(G(G(G(G(H(x')))))))),I(y))'
t: F(G(H(x')),I(y))
Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16]
Edges: [(0,1),(0,2),(1,0),(1,0),(1,3),(2,0),(2,4),(3,1),(3,1),(3,1),(3,5),(4,2),(4,6),(5,3),(5,3),(5,3),(5,3),(5,7),(6,4),(6,4),(6,8),(7,5),(7,5),(7,5),(7,5),(7,5),(7,9),(8,6),(8,6),(8,6),(8,10),(9,7),(9,7),(9,7),(9,7),(9,7),(9,7),(9,11),(10,8),(10,8),(10,8),(10,8),(10,12),(11,9),(11,9),(11,9),(11,9),(11,9),(11,9),(11,9),(11,13),(12,10),(12,10),(12,10),(12,10),(12,10),(12,14),(13,11),(13,11),(13,11),(13,11),(13,11),(13,11),(13,11),(13,11),(13,15),(14,12),(14,12),(14,12),(14,12),(14,12),(14,12),(14,16)]
ID: 0 => ('F(G(H(x')),I(y))', D0)
ID: 1 => ('F(G(G(H(x'))),I(y))', D1, R2, P[], S{x7 -> G(H(x')), x8 -> y}), NR: 'F(G(G(H(x'))),I(y))'
ID: 2 => ('F(H(x'),I(y))', D1, R3, P[1], S{x9 -> H(x')}), NR: 'H(x')'
ID: 3 => ('F(G(G(G(H(x')))),I(y))', D2, R2, P[], S{x7 -> G(G(H(x'))), x8 -> y}), NR: 'F(G(G(G(H(x')))),I(y))'
ID: 4 => ('F(H(x'),G(I(y)))', D2, R1, P[], S{x5 -> x', x6 -> I(y)}), NR: 'F(H(x'),G(I(y)))'
ID: 5 => ('F(G(G(G(G(H(x'))))),I(y))', D3, R2, P[], S{x7 -> G(G(G(H(x')))), x8 -> y}), NR: 'F(G(G(G(G(H(x'))))),I(y))'
ID: 6 => ('F(H(x'),G(G(I(y))))', D3, R1, P[], S{x5 -> x', x6 -> G(I(y))}), NR: 'F(H(x'),G(G(I(y))))'
ID: 7 => ('F(G(G(G(G(G(H(x')))))),I(y))', D4, R2, P[], S{x7 -> G(G(G(G(H(x'))))), x8 -> y}), NR: 'F(G(G(G(G(G(H(x')))))),I(y))'
ID: 8 => ('F(H(x'),G(G(G(I(y)))))', D4, R1, P[], S{x5 -> x', x6 -> G(G(I(y)))}), NR: 'F(H(x'),G(G(G(I(y)))))'
ID: 9 => ('F(G(G(G(G(G(G(H(x'))))))),I(y))', D5, R2, P[], S{x7 -> G(G(G(G(G(H(x')))))), x8 -> y}), NR: 'F(G(G(G(G(G(G(H(x'))))))),I(y))'
ID: 10 => ('F(H(x'),G(G(G(G(I(y))))))', D5, R1, P[], S{x5 -> x', x6 -> G(G(G(I(y))))}), NR: 'F(H(x'),G(G(G(G(I(y))))))'
ID: 11 => ('F(G(G(G(G(G(G(G(H(x')))))))),I(y))', D6, R2, P[], S{x7 -> G(G(G(G(G(G(H(x'))))))), x8 -> y}), NR: 'F(G(G(G(G(G(G(G(H(x')))))))),I(y))'
ID: 12 => ('F(H(x'),G(G(G(G(G(I(y)))))))', D6, R1, P[], S{x5 -> x', x6 -> G(G(G(G(I(y)))))}), NR: 'F(H(x'),G(G(G(G(G(I(y)))))))'
ID: 13 => ('F(G(G(G(G(G(G(G(G(H(x'))))))))),I(y))', D7, R2, P[], S{x7 -> G(G(G(G(G(G(G(H(x')))))))), x8 -> y}), NR: 'F(G(G(G(G(G(G(G(G(H(x'))))))))),I(y))'
ID: 14 => ('F(H(x'),G(G(G(G(G(G(I(y))))))))', D7, R1, P[], S{x5 -> x', x6 -> G(G(G(G(G(I(y))))))}), NR: 'F(H(x'),G(G(G(G(G(G(I(y))))))))'
ID: 15 => ('F(G(G(G(G(G(G(G(G(G(H(x')))))))))),I(y))', D8, R2, P[], S{x7 -> G(G(G(G(G(G(G(G(H(x'))))))))), x8 -> y}), NR: 'F(G(G(G(G(G(G(G(G(G(H(x')))))))))),I(y))'
ID: 16 => ('F(H(x'),G(G(G(G(G(G(G(I(y)))))))))', D8, R1, P[], S{x5 -> x', x6 -> G(G(G(G(G(G(I(y)))))))}), NR: 'F(H(x'),G(G(G(G(G(G(G(I(y)))))))))'
SNodesPath1: F(H(x'),G(I(y)))
TNodesPath1: 
SNodesPath2: 
TNodesPath2: F(G(H(x')),I(y))
F(H(x'),G(I(y))) ->= F(H(x'),G(I(y))) *<- F(G(H(x')),I(y))
F(G(H(x')),I(y)) ->= F(G(H(x')),I(y)) *<- F(H(x'),G(I(y)))
"Strongly closed critical pair"

The problem is confluent.