NO

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty)
(REPLACEMENT-MAP
(a)
(f 1)
(h 1, 2)
(b)
(c)
(fSNonEmpty)
)
(RULES
a -> f(f(b))
f(c) -> f(f(a))
h(f(f(c)),h(c,h(c,h(h(f(b),f(f(f(f(b))))),b)))) -> h(h(a,a),f(c))
h(b,h(c,h(b,h(a,b)))) -> a
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

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

Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty)
(REPLACEMENT-MAP
(a)
(f 1)
(h 1, 2)
(b)
(c)
(fSNonEmpty)
)
(RULES
a -> f(f(b))
f(c) -> f(f(a))
h(f(f(c)),h(c,h(c,h(h(f(b),f(f(f(f(b))))),b)))) -> h(h(a,a),f(c))
h(b,h(c,h(b,h(a,b)))) -> a
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 a -> f(f(b))
 f(c) -> f(f(a))
 h(f(f(c)),h(c,h(c,h(h(f(b),f(f(f(f(b))))),b)))) -> h(h(a,a),f(c))
 h(b,h(c,h(b,h(a,b)))) -> a
-> Vars:


-> Rlps:
 (rule: a -> f(f(b)), id: 1, possubterms: a->[])
 (rule: f(c) -> f(f(a)), id: 2, possubterms: f(c)->[], c->[1])
 (rule: h(f(f(c)),h(c,h(c,h(h(f(b),f(f(f(f(b))))),b)))) -> h(h(a,a),f(c)), id: 3, possubterms: h(f(f(c)),h(c,h(c,h(h(f(b),f(f(f(f(b))))),b))))->[], f(f(c))->[1], f(c)->[1, 1], c->[1, 1, 1], h(c,h(c,h(h(f(b),f(f(f(f(b))))),b)))->[2], c->[2, 1], h(c,h(h(f(b),f(f(f(f(b))))),b))->[2, 2], c->[2, 2, 1], h(h(f(b),f(f(f(f(b))))),b)->[2, 2, 2], h(f(b),f(f(f(f(b)))))->[2, 2, 2, 1], f(b)->[2, 2, 2, 1, 1], b->[2, 2, 2, 1, 1, 1], f(f(f(f(b))))->[2, 2, 2, 1, 2], f(f(f(b)))->[2, 2, 2, 1, 2, 1], f(f(b))->[2, 2, 2, 1, 2, 1, 1], f(b)->[2, 2, 2, 1, 2, 1, 1, 1], b->[2, 2, 2, 1, 2, 1, 1, 1, 1], b->[2, 2, 2, 2])
 (rule: h(b,h(c,h(b,h(a,b)))) -> a, id: 4, possubterms: h(b,h(c,h(b,h(a,b))))->[], b->[1], h(c,h(b,h(a,b)))->[2], c->[2, 1], h(b,h(a,b))->[2, 2], b->[2, 2, 1], h(a,b)->[2, 2, 2], a->[2, 2, 2, 1], b->[2, 2, 2, 2])

-> Unifications:
(R3 unifies with R2 at p: [1,1], l: h(f(f(c)),h(c,h(c,h(h(f(b),f(f(f(f(b))))),b)))), lp: f(c), sig: {}, l': f(c), r: h(h(a,a),f(c)), r': f(f(a)))
(R4 unifies with R1 at p: [2,2,2,1], l: h(b,h(c,h(b,h(a,b)))), lp: a, sig: {}, l': a, r: a, r': f(f(b)))

-> Critical pairs info:
<h(f(f(f(a))),h(c,h(c,h(h(f(b),f(f(f(f(b))))),b)))),h(h(a,a),f(c))>   =>  Not trivial, Not overlay, Proper, NW0, N1
<h(b,h(c,h(b,h(f(f(b)),b)))),a>   =>  Not trivial, Not 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: h(f(f(f(a))),h(c,h(c,h(h(f(b),f(f(f(f(b))))),b))))
Nodes: [0,1]
Edges: [(0,1)]
ID: 0 => ('h(f(f(f(a))),h(c,h(c,h(h(f(b),f(f(f(f(b))))),b))))', D0)
ID: 1 => ('h(f(f(f(f(f(b))))),h(c,h(c,h(h(f(b),f(f(f(f(b))))),b))))', D1, R1, P[1, 1, 1, 1], S{}), NR: 'f(f(b))'
t: h(h(a,a),f(c))
Nodes: [0,1,2,3,4,5,6,7,8,9,10,11]
Edges: [(0,1),(0,2),(0,3),(1,4),(1,5),(2,4),(2,6),(3,5),(3,6),(3,7),(4,8),(5,8),(5,9),(6,8),(6,10),(7,9),(7,10),(8,11),(9,11),(10,11)]
ID: 0 => ('h(h(a,a),f(c))', D0)
ID: 1 => ('h(h(f(f(b)),a),f(c))', D1, R1, P[1, 1], S{}), NR: 'f(f(b))'
ID: 2 => ('h(h(a,f(f(b))),f(c))', D1, R1, P[1, 2], S{}), NR: 'f(f(b))'
ID: 3 => ('h(h(a,a),f(f(a)))', D1, R2, P[2], S{}), NR: 'f(f(a))'
ID: 4 => ('h(h(f(f(b)),f(f(b))),f(c))', D2, R1, P[1, 2], S{}), NR: 'f(f(b))'
ID: 5 => ('h(h(f(f(b)),a),f(f(a)))', D2, R2, P[2], S{}), NR: 'f(f(a))'
ID: 6 => ('h(h(a,f(f(b))),f(f(a)))', D2, R2, P[2], S{}), NR: 'f(f(a))'
ID: 7 => ('h(h(a,a),f(f(f(f(b)))))', D2, R1, P[2, 1, 1], S{}), NR: 'f(f(b))'
ID: 8 => ('h(h(f(f(b)),f(f(b))),f(f(a)))', D3, R2, P[2], S{}), NR: 'f(f(a))'
ID: 9 => ('h(h(f(f(b)),a),f(f(f(f(b)))))', D3, R1, P[2, 1, 1], S{}), NR: 'f(f(b))'
ID: 10 => ('h(h(a,f(f(b))),f(f(f(f(b)))))', D3, R1, P[2, 1, 1], S{}), NR: 'f(f(b))'
ID: 11 => ('h(h(f(f(b)),f(f(b))),f(f(f(f(b)))))', D4, R1, P[2, 1, 1], S{}), NR: 'f(f(b))'
h(f(f(f(a))),h(c,h(c,h(h(f(b),f(f(f(f(b))))),b)))) ->* no union *<- h(h(a,a),f(c))
"Not joinable"

The problem is not confluent.