NO

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(e 1)
(i 1)
(r 1)
(t 1)
(w 1)
(fSNonEmpty)
)
(RULES
e(r(x)) -> e(w(x))
e(w(x)) -> r(i(x))
i(t(x)) -> e(r(x))
r(e(x)) -> w(r(x))
r(i(t(e(r(x))))) -> e(w(r(i(t(e(x))))))
t(e(x)) -> r(e(x))
w(r(x)) -> i(t(x))
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

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

Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(e 1)
(i 1)
(r 1)
(t 1)
(w 1)
(fSNonEmpty)
)
(RULES
e(r(x)) -> e(w(x))
e(w(x)) -> r(i(x))
i(t(x)) -> e(r(x))
r(e(x)) -> w(r(x))
r(i(t(e(r(x))))) -> e(w(r(i(t(e(x))))))
t(e(x)) -> r(e(x))
w(r(x)) -> i(t(x))
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 e(r(x)) -> e(w(x))
 e(w(x)) -> r(i(x))
 i(t(x)) -> e(r(x))
 r(e(x)) -> w(r(x))
 r(i(t(e(r(x))))) -> e(w(r(i(t(e(x))))))
 t(e(x)) -> r(e(x))
 w(r(x)) -> i(t(x))
-> Vars:
 x, x, x, x, x, x, x

-> Rlps:
 (rule: e(r(x)) -> e(w(x)), id: 1, possubterms: e(r(x))->[], r(x)->[1])
 (rule: e(w(x)) -> r(i(x)), id: 2, possubterms: e(w(x))->[], w(x)->[1])
 (rule: i(t(x)) -> e(r(x)), id: 3, possubterms: i(t(x))->[], t(x)->[1])
 (rule: r(e(x)) -> w(r(x)), id: 4, possubterms: r(e(x))->[], e(x)->[1])
 (rule: r(i(t(e(r(x))))) -> e(w(r(i(t(e(x)))))), id: 5, possubterms: r(i(t(e(r(x)))))->[], i(t(e(r(x))))->[1], t(e(r(x)))->[1, 1], e(r(x))->[1, 1, 1], r(x)->[1, 1, 1, 1])
 (rule: t(e(x)) -> r(e(x)), id: 6, possubterms: t(e(x))->[], e(x)->[1])
 (rule: w(r(x)) -> i(t(x)), id: 7, possubterms: w(r(x))->[], r(x)->[1])

-> Unifications:
(R1 unifies with R4 at p: [1], l: e(r(x)), lp: r(x), sig: {x -> e(x')}, l': r(e(x')), r: e(w(x)), r': w(r(x')))
(R1 unifies with R5 at p: [1], l: e(r(x)), lp: r(x), sig: {x -> i(t(e(r(x'))))}, l': r(i(t(e(r(x'))))), r: e(w(x)), r': e(w(r(i(t(e(x')))))))
(R2 unifies with R7 at p: [1], l: e(w(x)), lp: w(x), sig: {x -> r(x')}, l': w(r(x')), r: r(i(x)), r': i(t(x')))
(R3 unifies with R6 at p: [1], l: i(t(x)), lp: t(x), sig: {x -> e(x')}, l': t(e(x')), r: e(r(x)), r': r(e(x')))
(R4 unifies with R1 at p: [1], l: r(e(x)), lp: e(x), sig: {x -> r(x')}, l': e(r(x')), r: w(r(x)), r': e(w(x')))
(R4 unifies with R2 at p: [1], l: r(e(x)), lp: e(x), sig: {x -> w(x')}, l': e(w(x')), r: w(r(x)), r': r(i(x')))
(R5 unifies with R3 at p: [1], l: r(i(t(e(r(x))))), lp: i(t(e(r(x)))), sig: {x' -> e(r(x))}, l': i(t(x')), r: e(w(r(i(t(e(x)))))), r': e(r(x')))
(R5 unifies with R6 at p: [1,1], l: r(i(t(e(r(x))))), lp: t(e(r(x))), sig: {x' -> r(x)}, l': t(e(x')), r: e(w(r(i(t(e(x)))))), r': r(e(x')))
(R5 unifies with R1 at p: [1,1,1], l: r(i(t(e(r(x))))), lp: e(r(x)), sig: {x -> x'}, l': e(r(x')), r: e(w(r(i(t(e(x)))))), r': e(w(x')))
(R5 unifies with R4 at p: [1,1,1,1], l: r(i(t(e(r(x))))), lp: r(x), sig: {x -> e(x')}, l': r(e(x')), r: e(w(r(i(t(e(x)))))), r': w(r(x')))
(R5 unifies with R5 at p: [1,1,1,1], l: r(i(t(e(r(x))))), lp: r(x), sig: {x -> i(t(e(r(x'))))}, l': r(i(t(e(r(x'))))), r: e(w(r(i(t(e(x)))))), r': e(w(r(i(t(e(x')))))))
(R6 unifies with R1 at p: [1], l: t(e(x)), lp: e(x), sig: {x -> r(x')}, l': e(r(x')), r: r(e(x)), r': e(w(x')))
(R6 unifies with R2 at p: [1], l: t(e(x)), lp: e(x), sig: {x -> w(x')}, l': e(w(x')), r: r(e(x)), r': r(i(x')))
(R7 unifies with R4 at p: [1], l: w(r(x)), lp: r(x), sig: {x -> e(x')}, l': r(e(x')), r: i(t(x)), r': w(r(x')))
(R7 unifies with R5 at p: [1], l: w(r(x)), lp: r(x), sig: {x -> i(t(e(r(x'))))}, l': r(i(t(e(r(x'))))), r: i(t(x)), r': e(w(r(i(t(e(x')))))))

-> Critical pairs info:
<e(i(t(x'))),r(i(r(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N1
<t(e(w(x'))),r(e(r(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N2
<e(w(r(x'))),e(w(e(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N3
<r(i(t(e(w(x'))))),e(w(r(i(t(e(x'))))))>   =>  Not trivial, Not overlay, Proper, NW0, N4
<r(e(r(e(r(x))))),e(w(r(i(t(e(x))))))>   =>  Not trivial, Not overlay, Proper, NW0, N5
<r(i(t(e(e(w(r(i(t(e(x')))))))))),e(w(r(i(t(e(i(t(e(r(x'))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N6
<e(e(w(r(i(t(e(x'))))))),e(w(i(t(e(r(x'))))))>   =>  Not trivial, Not overlay, Proper, NW0, N7
<r(i(r(e(r(x))))),e(w(r(i(t(e(x))))))>   =>  Not trivial, Not overlay, Proper, NW0, N8
<i(r(e(x'))),e(r(e(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N9
<r(r(i(x'))),w(r(w(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N10
<w(w(r(x'))),i(t(e(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N11
<t(r(i(x'))),r(e(w(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N12
<r(e(w(x'))),w(r(r(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N13
<r(i(t(e(w(r(x')))))),e(w(r(i(t(e(e(x')))))))>   =>  Not trivial, Not overlay, Proper, NW0, N14
<w(e(w(r(i(t(e(x'))))))),i(t(i(t(e(r(x'))))))>   =>  Not trivial, Not overlay, Proper, NW0, N15

-> 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: e(i(t(x')))
Nodes: [0,1,2,3,4,5]
Edges: [(0,1),(1,2),(2,3),(3,4),(4,5)]
ID: 0 => ('e(i(t(x')))', D0)
ID: 1 => ('e(e(r(x')))', D1, R3, P[1], S{x6 -> x'}), NR: 'e(r(x'))'
ID: 2 => ('e(e(w(x')))', D2, R1, P[1], S{x4 -> x'}), NR: 'e(w(x'))'
ID: 3 => ('e(r(i(x')))', D3, R2, P[1], S{x5 -> x'}), NR: 'r(i(x'))'
ID: 4 => ('e(w(i(x')))', D4, R1, P[], S{x4 -> i(x')}), NR: 'e(w(i(x')))'
ID: 5 => ('r(i(i(x')))', D5, R2, P[], S{x5 -> i(x')}), NR: 'r(i(i(x')))'
t: r(i(r(x')))
Nodes: [0]
Edges: []
ID: 0 => ('r(i(r(x')))', D0)
e(i(t(x'))) ->* no union *<- r(i(r(x')))
"Not joinable"

The problem is not confluent.