NO

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(F 1)
(G 1)
(A)
(B)
(H 1)
(fSNonEmpty)
)
(RULES
F(x) -> G(F(x))
F(x) -> A
G(F(x)) -> F(H(x))
G(F(x)) -> B
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

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

Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(F 1)
(G 1)
(A)
(B)
(H 1)
(fSNonEmpty)
)
(RULES
F(x) -> G(F(x))
F(x) -> A
G(F(x)) -> F(H(x))
G(F(x)) -> B
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 F(x) -> G(F(x))
 F(x) -> A
 G(F(x)) -> F(H(x))
 G(F(x)) -> B
-> Vars:
 x, x, x, x

-> Rlps:
 (rule: F(x) -> G(F(x)), id: 1, possubterms: F(x)->[])
 (rule: F(x) -> A, id: 2, possubterms: F(x)->[])
 (rule: G(F(x)) -> F(H(x)), id: 3, possubterms: G(F(x))->[], F(x)->[1])
 (rule: G(F(x)) -> B, id: 4, possubterms: G(F(x))->[], F(x)->[1])

-> Unifications:
(R2 unifies with R1 at p: [], l: F(x), lp: F(x), sig: {x -> x'}, l': F(x'), r: A, r': G(F(x')))
(R3 unifies with R1 at p: [1], l: G(F(x)), lp: F(x), sig: {x -> x'}, l': F(x'), r: F(H(x)), r': G(F(x')))
(R3 unifies with R2 at p: [1], l: G(F(x)), lp: F(x), sig: {x -> x'}, l': F(x'), r: F(H(x)), r': A)
(R4 unifies with R3 at p: [], l: G(F(x)), lp: G(F(x)), sig: {x -> x'}, l': G(F(x')), r: B, r': F(H(x')))
(R4 unifies with R1 at p: [1], l: G(F(x)), lp: F(x), sig: {x -> x'}, l': F(x'), r: B, r': G(F(x')))
(R4 unifies with R2 at p: [1], l: G(F(x)), lp: F(x), sig: {x -> x'}, l': F(x'), r: B, r': A)

-> Critical pairs info:
<G(F(x')),A>   =>  Not trivial, Overlay, Proper, NW0, N1
<F(H(x')),B>   =>  Not trivial, Overlay, Proper, NW0, N2
<G(G(F(x'))),B>   =>  Not trivial, Not overlay, Proper, NW0, N3
<G(A),F(H(x'))>   =>  Not trivial, Not overlay, Proper, NW0, N4
<G(G(F(x'))),F(H(x'))>   =>  Not trivial, Not overlay, Proper, NW0, N5
<G(A),B>   =>  Not trivial, Not overlay, Proper, NW0, N6

-> 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: G(A)
Nodes: [0]
Edges: []
ID: 0 => ('G(A)', D0)
t: B
Nodes: [0]
Edges: []
ID: 0 => ('B', D0)
G(A) ->* no union *<- B
"Not joinable"

The problem is not confluent.