NO

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y)
(REPLACEMENT-MAP
(inv 1)
(minus 1, 2)
(p 1)
(s 1)
(0)
(fSNonEmpty)
)
(RULES
inv(minus(x,y)) -> minus(y,x)
inv(p(x)) -> s(inv(x))
inv(s(x)) -> p(inv(x))
inv(0) -> 0
inv(x) -> minus(0,x)
minus(0,x) -> inv(x)
minus(x,p(y)) -> s(minus(x,y))
minus(x,s(y)) -> p(minus(x,y))
minus(x,0) -> x
p(s(x)) -> x
s(p(x)) -> x
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

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

Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y)
(REPLACEMENT-MAP
(inv 1)
(minus 1, 2)
(p 1)
(s 1)
(0)
(fSNonEmpty)
)
(RULES
inv(minus(x,y)) -> minus(y,x)
inv(p(x)) -> s(inv(x))
inv(s(x)) -> p(inv(x))
inv(0) -> 0
inv(x) -> minus(0,x)
minus(0,x) -> inv(x)
minus(x,p(y)) -> s(minus(x,y))
minus(x,s(y)) -> p(minus(x,y))
minus(x,0) -> x
p(s(x)) -> x
s(p(x)) -> x
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 inv(minus(x,y)) -> minus(y,x)
 inv(p(x)) -> s(inv(x))
 inv(s(x)) -> p(inv(x))
 inv(0) -> 0
 inv(x) -> minus(0,x)
 minus(0,x) -> inv(x)
 minus(x,p(y)) -> s(minus(x,y))
 minus(x,s(y)) -> p(minus(x,y))
 minus(x,0) -> x
 p(s(x)) -> x
 s(p(x)) -> x
-> Vars:
 x, y, x, x, x, x, x, y, x, y, x, x, x

-> Rlps:
 (rule: inv(minus(x,y)) -> minus(y,x), id: 1, possubterms: inv(minus(x,y))->[], minus(x,y)->[1])
 (rule: inv(p(x)) -> s(inv(x)), id: 2, possubterms: inv(p(x))->[], p(x)->[1])
 (rule: inv(s(x)) -> p(inv(x)), id: 3, possubterms: inv(s(x))->[], s(x)->[1])
 (rule: inv(0) -> 0, id: 4, possubterms: inv(0)->[], 0->[1])
 (rule: inv(x) -> minus(0,x), id: 5, possubterms: inv(x)->[])
 (rule: minus(0,x) -> inv(x), id: 6, possubterms: minus(0,x)->[], 0->[1])
 (rule: minus(x,p(y)) -> s(minus(x,y)), id: 7, possubterms: minus(x,p(y))->[], p(y)->[2])
 (rule: minus(x,s(y)) -> p(minus(x,y)), id: 8, possubterms: minus(x,s(y))->[], s(y)->[2])
 (rule: minus(x,0) -> x, id: 9, possubterms: minus(x,0)->[], 0->[2])
 (rule: p(s(x)) -> x, id: 10, possubterms: p(s(x))->[], s(x)->[1])
 (rule: s(p(x)) -> x, id: 11, possubterms: s(p(x))->[], p(x)->[1])

-> Unifications:
(R1 unifies with R6 at p: [1], l: inv(minus(x,y)), lp: minus(x,y), sig: {x -> 0,y -> x'}, l': minus(0,x'), r: minus(y,x), r': inv(x'))
(R1 unifies with R7 at p: [1], l: inv(minus(x,y)), lp: minus(x,y), sig: {x -> x',y -> p(y')}, l': minus(x',p(y')), r: minus(y,x), r': s(minus(x',y')))
(R1 unifies with R8 at p: [1], l: inv(minus(x,y)), lp: minus(x,y), sig: {x -> x',y -> s(y')}, l': minus(x',s(y')), r: minus(y,x), r': p(minus(x',y')))
(R1 unifies with R9 at p: [1], l: inv(minus(x,y)), lp: minus(x,y), sig: {x -> x',y -> 0}, l': minus(x',0), r: minus(y,x), r': x')
(R2 unifies with R10 at p: [1], l: inv(p(x)), lp: p(x), sig: {x -> s(x')}, l': p(s(x')), r: s(inv(x)), r': x')
(R3 unifies with R11 at p: [1], l: inv(s(x)), lp: s(x), sig: {x -> p(x')}, l': s(p(x')), r: p(inv(x)), r': x')
(R5 unifies with R1 at p: [], l: inv(x), lp: inv(x), sig: {x -> minus(x',y)}, l': inv(minus(x',y)), r: minus(0,x), r': minus(y,x'))
(R5 unifies with R2 at p: [], l: inv(x), lp: inv(x), sig: {x -> p(x')}, l': inv(p(x')), r: minus(0,x), r': s(inv(x')))
(R5 unifies with R3 at p: [], l: inv(x), lp: inv(x), sig: {x -> s(x')}, l': inv(s(x')), r: minus(0,x), r': p(inv(x')))
(R5 unifies with R4 at p: [], l: inv(x), lp: inv(x), sig: {x -> 0}, l': inv(0), r: minus(0,x), r': 0)
(R7 unifies with R6 at p: [], l: minus(x,p(y)), lp: minus(x,p(y)), sig: {x -> 0,x' -> p(y)}, l': minus(0,x'), r: s(minus(x,y)), r': inv(x'))
(R7 unifies with R10 at p: [2], l: minus(x,p(y)), lp: p(y), sig: {y -> s(x')}, l': p(s(x')), r: s(minus(x,y)), r': x')
(R8 unifies with R6 at p: [], l: minus(x,s(y)), lp: minus(x,s(y)), sig: {x -> 0,x' -> s(y)}, l': minus(0,x'), r: p(minus(x,y)), r': inv(x'))
(R8 unifies with R11 at p: [2], l: minus(x,s(y)), lp: s(y), sig: {y -> p(x')}, l': s(p(x')), r: p(minus(x,y)), r': x')
(R9 unifies with R6 at p: [], l: minus(x,0), lp: minus(x,0), sig: {x -> 0,x' -> 0}, l': minus(0,x'), r: x, r': inv(x'))
(R10 unifies with R11 at p: [1], l: p(s(x)), lp: s(x), sig: {x -> p(x')}, l': s(p(x')), r: x, r': x')
(R11 unifies with R10 at p: [1], l: s(p(x)), lp: p(x), sig: {x -> s(x')}, l': p(s(x')), r: x, r': x')

-> Critical pairs info:
<0,minus(0,0)>   =>  Not trivial, Overlay, Proper, NW0, N1
<inv(0),0>   =>  Not trivial, Overlay, Proper, NW0, N2
<inv(s(y)),p(minus(0,y))>   =>  Not trivial, Overlay, Proper, NW0, N3
<p(inv(x')),minus(0,s(x'))>   =>  Not trivial, Overlay, Proper, NW0, N4
<inv(x'),minus(0,x')>   =>  Not trivial, Not overlay, Proper, NW0, N5
<p(x'),p(x')>   =>  Trivial, Not overlay, Proper, NW0, N6
<minus(x,x'),s(minus(x,s(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N7
<inv(p(minus(x',y'))),minus(s(y'),x')>   =>  Not trivial, Not overlay, Proper, NW0, N8
<s(inv(x')),minus(0,p(x'))>   =>  Not trivial, Overlay, Proper, NW0, N9
<inv(p(y)),s(minus(0,y))>   =>  Not trivial, Overlay, Proper, NW0, N10
<minus(x,x'),p(minus(x,p(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N11
<inv(s(minus(x',y'))),minus(p(y'),x')>   =>  Not trivial, Not overlay, Proper, NW0, N12
<inv(inv(x')),minus(x',0)>   =>  Not trivial, Not overlay, Proper, NW0, N13
<inv(x'),s(inv(s(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N14
<minus(y,x'),minus(0,minus(x',y))>   =>  Not trivial, Overlay, Proper, NW0, N15
<inv(x'),p(inv(p(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N16
<s(x'),s(x')>   =>  Trivial, Not overlay, Proper, NW0, N17

-> 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: inv(p(minus(x',y')))
Nodes: [0,1,2,3,4]
Edges: [(0,1),(0,2),(1,3),(1,4),(2,0),(2,4),(4,1)]
ID: 0 => ('inv(p(minus(x',y')))', D0)
ID: 1 => ('s(inv(minus(x',y')))', D1, R2, P[], S{x8 -> minus(x',y')}), NR: 's(inv(minus(x',y')))'
ID: 2 => ('minus(0,p(minus(x',y')))', D1, R5, P[], S{x10 -> p(minus(x',y'))}), NR: 'minus(0,p(minus(x',y')))'
ID: 3 => ('s(minus(y',x'))', D2, R1, P[1], S{x6 -> x', x7 -> y'}), NR: 'minus(y',x')'
ID: 4 => ('s(minus(0,minus(x',y')))', D2, R5, P[1], S{x10 -> minus(x',y')}), NR: 'minus(0,minus(x',y'))'
t: minus(s(y'),x')
Nodes: [0]
Edges: []
ID: 0 => ('minus(s(y'),x')', D0)
inv(p(minus(x',y'))) ->* no union *<- minus(s(y'),x')
"Not joinable"

The problem is not confluent.