NO

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(1 1)
(b 1)
(h 1)
(fSNonEmpty)
(s 1)
(t 1)
)
(RULES
1(1(h(b(x)))) -> 1(1(s(b(x))))
1(s(x)) -> s(1(x))
1(t(x)) -> t(1(1(1(x))))
b(s(x)) -> b(h(x))
b(t(x)) -> b(h(x))
h(1(1(x))) -> 1(h(x))
h(1(b(x))) -> t(1(1(b(x))))
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

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

Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(1 1)
(b 1)
(h 1)
(fSNonEmpty)
(s 1)
(t 1)
)
(RULES
1(1(h(b(x)))) -> 1(1(s(b(x))))
1(s(x)) -> s(1(x))
1(t(x)) -> t(1(1(1(x))))
b(s(x)) -> b(h(x))
b(t(x)) -> b(h(x))
h(1(1(x))) -> 1(h(x))
h(1(b(x))) -> t(1(1(b(x))))
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 1(1(h(b(x)))) -> 1(1(s(b(x))))
 1(s(x)) -> s(1(x))
 1(t(x)) -> t(1(1(1(x))))
 b(s(x)) -> b(h(x))
 b(t(x)) -> b(h(x))
 h(1(1(x))) -> 1(h(x))
 h(1(b(x))) -> t(1(1(b(x))))
-> Vars:
 x, x, x, x, x, x, x

-> Rlps:
 (rule: 1(1(h(b(x)))) -> 1(1(s(b(x)))), id: 1, possubterms: 1(1(h(b(x))))->[], 1(h(b(x)))->[1], h(b(x))->[1, 1], b(x)->[1, 1, 1])
 (rule: 1(s(x)) -> s(1(x)), id: 2, possubterms: 1(s(x))->[], s(x)->[1])
 (rule: 1(t(x)) -> t(1(1(1(x)))), id: 3, possubterms: 1(t(x))->[], t(x)->[1])
 (rule: b(s(x)) -> b(h(x)), id: 4, possubterms: b(s(x))->[], s(x)->[1])
 (rule: b(t(x)) -> b(h(x)), id: 5, possubterms: b(t(x))->[], t(x)->[1])
 (rule: h(1(1(x))) -> 1(h(x)), id: 6, possubterms: h(1(1(x)))->[], 1(1(x))->[1], 1(x)->[1, 1])
 (rule: h(1(b(x))) -> t(1(1(b(x)))), id: 7, possubterms: h(1(b(x)))->[], 1(b(x))->[1], b(x)->[1, 1])

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

-> Critical pairs info:
<h(1(s(1(x')))),1(h(s(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N1
<1(1(h(b(h(x'))))),1(1(s(b(s(x')))))>   =>  Not trivial, Not overlay, Proper, NW0, N2
<h(1(t(1(1(1(x')))))),1(h(t(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N3
<h(1(1(1(s(b(x')))))),1(h(1(h(b(x')))))>   =>  Not trivial, Not overlay, Proper, NW0, N4
<h(1(b(h(x')))),t(1(1(b(t(x')))))>   =>  Not trivial, Not overlay, Proper, NW0, N5
<h(1(1(s(b(x'))))),1(h(h(b(x'))))>   =>  Not trivial, Not overlay, Proper, NW0, N6
<h(1(b(h(x')))),t(1(1(b(s(x')))))>   =>  Not trivial, Not overlay, Proper, NW0, N7
<1(1(h(b(h(x'))))),1(1(s(b(t(x')))))>   =>  Not trivial, Not overlay, Proper, NW0, N8

-> 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: h(1(s(1(x'))))
Nodes: [0,1]
Edges: [(0,1)]
ID: 0 => ('h(1(s(1(x'))))', D0)
ID: 1 => ('h(s(1(1(x'))))', D1, R2, P[1], S{x5 -> 1(x')}), NR: 's(1(1(x')))'
t: 1(h(s(x')))
Nodes: [0]
Edges: []
ID: 0 => ('1(h(s(x')))', D0)
h(1(s(1(x')))) ->* no union *<- 1(h(s(x')))
"Not joinable"

The problem is not confluent.