NO

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty y x)
(REPLACEMENT-MAP
(and 1, 2)
(not 1)
(or 1, 2)
(fSNonEmpty)
(false)
(true)
)
(RULES
and(false,false) -> false
and(true,true) -> true
and(true,y) -> y
and(x,true) -> x
not(and(x,y)) -> or(not(x),not(y))
not(or(x,y)) -> and(not(x),not(y))
not(false) -> true
not(true) -> false
or(false,false) -> false
or(true,y) -> true
or(x,true) -> true
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

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

Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty y x)
(REPLACEMENT-MAP
(and 1, 2)
(not 1)
(or 1, 2)
(fSNonEmpty)
(false)
(true)
)
(RULES
and(false,false) -> false
and(true,true) -> true
and(true,y) -> y
and(x,true) -> x
not(and(x,y)) -> or(not(x),not(y))
not(or(x,y)) -> and(not(x),not(y))
not(false) -> true
not(true) -> false
or(false,false) -> false
or(true,y) -> true
or(x,true) -> true
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 and(false,false) -> false
 and(true,true) -> true
 and(true,y) -> y
 and(x,true) -> x
 not(and(x,y)) -> or(not(x),not(y))
 not(or(x,y)) -> and(not(x),not(y))
 not(false) -> true
 not(true) -> false
 or(false,false) -> false
 or(true,y) -> true
 or(x,true) -> true
-> Vars:
 y, x, y, x, y, x, y, x

-> Rlps:
 (rule: and(false,false) -> false, id: 1, possubterms: and(false,false)->[], false->[1], false->[2])
 (rule: and(true,true) -> true, id: 2, possubterms: and(true,true)->[], true->[1], true->[2])
 (rule: and(true,y) -> y, id: 3, possubterms: and(true,y)->[], true->[1])
 (rule: and(x,true) -> x, id: 4, possubterms: and(x,true)->[], true->[2])
 (rule: not(and(x,y)) -> or(not(x),not(y)), id: 5, possubterms: not(and(x,y))->[], and(x,y)->[1])
 (rule: not(or(x,y)) -> and(not(x),not(y)), id: 6, possubterms: not(or(x,y))->[], or(x,y)->[1])
 (rule: not(false) -> true, id: 7, possubterms: not(false)->[], false->[1])
 (rule: not(true) -> false, id: 8, possubterms: not(true)->[], true->[1])
 (rule: or(false,false) -> false, id: 9, possubterms: or(false,false)->[], false->[1], false->[2])
 (rule: or(true,y) -> true, id: 10, possubterms: or(true,y)->[], true->[1])
 (rule: or(x,true) -> true, id: 11, possubterms: or(x,true)->[], true->[2])

-> Unifications:
(R3 unifies with R2 at p: [], l: and(true,y), lp: and(true,y), sig: {y -> true}, l': and(true,true), r: y, r': true)
(R4 unifies with R2 at p: [], l: and(x,true), lp: and(x,true), sig: {x -> true}, l': and(true,true), r: x, r': true)
(R4 unifies with R3 at p: [], l: and(x,true), lp: and(x,true), sig: {x -> true,y -> true}, l': and(true,y), r: x, r': y)
(R5 unifies with R1 at p: [1], l: not(and(x,y)), lp: and(x,y), sig: {y -> false,x -> false}, l': and(false,false), r: or(not(x),not(y)), r': false)
(R5 unifies with R2 at p: [1], l: not(and(x,y)), lp: and(x,y), sig: {y -> true,x -> true}, l': and(true,true), r: or(not(x),not(y)), r': true)
(R5 unifies with R3 at p: [1], l: not(and(x,y)), lp: and(x,y), sig: {y -> y',x -> true}, l': and(true,y'), r: or(not(x),not(y)), r': y')
(R5 unifies with R4 at p: [1], l: not(and(x,y)), lp: and(x,y), sig: {y -> true,x -> x'}, l': and(x',true), r: or(not(x),not(y)), r': x')
(R6 unifies with R9 at p: [1], l: not(or(x,y)), lp: or(x,y), sig: {y -> false,x -> false}, l': or(false,false), r: and(not(x),not(y)), r': false)
(R6 unifies with R10 at p: [1], l: not(or(x,y)), lp: or(x,y), sig: {y -> y',x -> true}, l': or(true,y'), r: and(not(x),not(y)), r': true)
(R6 unifies with R11 at p: [1], l: not(or(x,y)), lp: or(x,y), sig: {y -> true,x -> x'}, l': or(x',true), r: and(not(x),not(y)), r': true)
(R11 unifies with R10 at p: [], l: or(x,true), lp: or(x,true), sig: {x -> true,y -> true}, l': or(true,y), r: true, r': true)

-> Critical pairs info:
<not(false),or(not(false),not(false))>   =>  Not trivial, Not overlay, Proper, NW0, N1
<not(x'),or(not(x'),not(true))>   =>  Not trivial, Not overlay, Proper, NW0, N2
<not(false),and(not(false),not(false))>   =>  Not trivial, Not overlay, Proper, NW0, N3
<true,true>   =>  Trivial, Overlay, Proper, NW0, N4
<true,true>   =>  Trivial, Overlay, Proper, NW0, N5
<not(y'),or(not(true),not(y'))>   =>  Not trivial, Not overlay, Proper, NW0, N6
<true,true>   =>  Trivial, Overlay, Proper, NW0, N7
<true,true>   =>  Trivial, Overlay, Proper, NW0, N8
<not(true),and(not(x'),not(true))>   =>  Not trivial, Not overlay, Proper, NW0, N9
<not(true),and(not(true),not(y'))>   =>  Not trivial, Not overlay, Proper, NW0, N10
<not(true),or(not(true),not(true))>   =>  Not trivial, Not overlay, Proper, NW0, N11

-> 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: not(x')
Nodes: [0]
Edges: []
ID: 0 => ('not(x')', D0)
t: or(not(x'),not(true))
Nodes: [0,1]
Edges: [(0,1)]
ID: 0 => ('or(not(x'),not(true))', D0)
ID: 1 => ('or(not(x'),false)', D1, R8, P[2], S{}), NR: 'false'
not(x') ->* no union *<- or(not(x'),not(true))
"Not joinable"

The problem is not confluent.