YES

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(bar 1)
(foo 1)
(p 1)
(0 1)
(fSNonEmpty)
(s 1)
)
(RULES
bar(0(x)) -> 0(p(s(s(s(x)))))
bar(s(x)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x))))))))))))
foo(0(x)) -> 0(s(p(p(p(s(s(s(p(s(x))))))))))
foo(s(x)) -> p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x))))))))))))))))))))))))))
p(p(s(x))) -> p(x)
p(0(x)) -> 0(s(s(s(s(x)))))
p(s(x)) -> 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
(bar 1)
(foo 1)
(p 1)
(0 1)
(fSNonEmpty)
(s 1)
)
(RULES
bar(0(x)) -> 0(p(s(s(s(x)))))
bar(s(x)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x))))))))))))
foo(0(x)) -> 0(s(p(p(p(s(s(s(p(s(x))))))))))
foo(s(x)) -> p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x))))))))))))))))))))))))))
p(p(s(x))) -> p(x)
p(0(x)) -> 0(s(s(s(s(x)))))
p(s(x)) -> x
)
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 bar(0(x)) -> 0(p(s(s(s(x)))))
 bar(s(x)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x))))))))))))
 foo(0(x)) -> 0(s(p(p(p(s(s(s(p(s(x))))))))))
 foo(s(x)) -> p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x))))))))))))))))))))))))))
 p(p(s(x))) -> p(x)
 p(0(x)) -> 0(s(s(s(s(x)))))
 p(s(x)) -> x
-> Vars:
 x, x, x, x, x, x, x

-> Rlps:
 (rule: bar(0(x)) -> 0(p(s(s(s(x))))), id: 1, possubterms: bar(0(x))->[], 0(x)->[1])
 (rule: bar(s(x)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x)))))))))))), id: 2, possubterms: bar(s(x))->[], s(x)->[1])
 (rule: foo(0(x)) -> 0(s(p(p(p(s(s(s(p(s(x)))))))))), id: 3, possubterms: foo(0(x))->[], 0(x)->[1])
 (rule: foo(s(x)) -> p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x)))))))))))))))))))))))))), id: 4, possubterms: foo(s(x))->[], s(x)->[1])
 (rule: p(p(s(x))) -> p(x), id: 5, possubterms: p(p(s(x)))->[], p(s(x))->[1], s(x)->[1, 1])
 (rule: p(0(x)) -> 0(s(s(s(s(x))))), id: 6, possubterms: p(0(x))->[], 0(x)->[1])
 (rule: p(s(x)) -> x, id: 7, possubterms: p(s(x))->[], s(x)->[1])

-> Unifications:
(R5 unifies with R7 at p: [1], l: p(p(s(x))), lp: p(s(x)), sig: {x -> x'}, l': p(s(x')), r: p(x), r': x')

-> Critical pairs info:
<p(x'),p(x')>   =>  Trivial, Not overlay, Proper, NW0, N1

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


The problem is confluent.