YES

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(0 1)
(1 1)
(2 1)
(3 1)
(4 1)
(5 1)
(fSNonEmpty)
)
(RULES
0(1(2(3(4(x))))) -> 0(2(1(3(4(x)))))
0(5(1(2(4(3(x)))))) -> 0(5(2(1(4(3(x))))))
0(5(2(4(1(3(x)))))) -> 0(1(5(2(4(3(x))))))
0(5(3(1(2(4(x)))))) -> 0(1(5(3(2(4(x))))))
0(5(4(1(3(2(x)))))) -> 0(5(4(3(1(2(x))))))
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

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

Problem 1: 
Linearity Procedure:
Linear?
YES

Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(0 1)
(1 1)
(2 1)
(3 1)
(4 1)
(5 1)
(fSNonEmpty)
)
(RULES
0(1(2(3(4(x))))) -> 0(2(1(3(4(x)))))
0(5(1(2(4(3(x)))))) -> 0(5(2(1(4(3(x))))))
0(5(2(4(1(3(x)))))) -> 0(1(5(2(4(3(x))))))
0(5(3(1(2(4(x)))))) -> 0(1(5(3(2(4(x))))))
0(5(4(1(3(2(x)))))) -> 0(5(4(3(1(2(x))))))
)
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 0(1(2(3(4(x))))) -> 0(2(1(3(4(x)))))
 0(5(1(2(4(3(x)))))) -> 0(5(2(1(4(3(x))))))
 0(5(2(4(1(3(x)))))) -> 0(1(5(2(4(3(x))))))
 0(5(3(1(2(4(x)))))) -> 0(1(5(3(2(4(x))))))
 0(5(4(1(3(2(x)))))) -> 0(5(4(3(1(2(x))))))
-> Vars:
 x, x, x, x, x

-> Rlps:
 (rule: 0(1(2(3(4(x))))) -> 0(2(1(3(4(x))))), id: 1, possubterms: 0(1(2(3(4(x)))))->[], 1(2(3(4(x))))->[1], 2(3(4(x)))->[1, 1], 3(4(x))->[1, 1, 1], 4(x)->[1, 1, 1, 1])
 (rule: 0(5(1(2(4(3(x)))))) -> 0(5(2(1(4(3(x)))))), id: 2, possubterms: 0(5(1(2(4(3(x))))))->[], 5(1(2(4(3(x)))))->[1], 1(2(4(3(x))))->[1, 1], 2(4(3(x)))->[1, 1, 1], 4(3(x))->[1, 1, 1, 1], 3(x)->[1, 1, 1, 1, 1])
 (rule: 0(5(2(4(1(3(x)))))) -> 0(1(5(2(4(3(x)))))), id: 3, possubterms: 0(5(2(4(1(3(x))))))->[], 5(2(4(1(3(x)))))->[1], 2(4(1(3(x))))->[1, 1], 4(1(3(x)))->[1, 1, 1], 1(3(x))->[1, 1, 1, 1], 3(x)->[1, 1, 1, 1, 1])
 (rule: 0(5(3(1(2(4(x)))))) -> 0(1(5(3(2(4(x)))))), id: 4, possubterms: 0(5(3(1(2(4(x))))))->[], 5(3(1(2(4(x)))))->[1], 3(1(2(4(x))))->[1, 1], 1(2(4(x)))->[1, 1, 1], 2(4(x))->[1, 1, 1, 1], 4(x)->[1, 1, 1, 1, 1])
 (rule: 0(5(4(1(3(2(x)))))) -> 0(5(4(3(1(2(x)))))), id: 5, possubterms: 0(5(4(1(3(2(x))))))->[], 5(4(1(3(2(x)))))->[1], 4(1(3(2(x))))->[1, 1], 1(3(2(x)))->[1, 1, 1], 3(2(x))->[1, 1, 1, 1], 2(x)->[1, 1, 1, 1, 1])

-> Unifications:


-> Critical pairs info:


-> Problem conclusions:
 Left linear, Right linear, Linear
 Weakly orthogonal, Almost orthogonal, Orthogonal
 Huet-Levy confluent, Not Newman confluent
 R is a TRS 


The problem is confluent.