YES

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y)
(REPLACEMENT-MAP
(or 1, 2)
(F)
(T)
(fSNonEmpty)
)
(RULES
or(x,F) -> x
or(x,T) -> T
or(x,y) -> or(y,x)
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

Problem 1: 

Commutativity Transform Procedure:

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y)
(REPLACEMENT-MAP
(or 1, 2)
(F)
(T)
(fSNonEmpty)
)
(RULES
or(F,x) -> x
or(T,x) -> T
or(x,F) -> x
or(x,T) -> T
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y)
(REPLACEMENT-MAP
(or 1, 2)
(F)
(T)
(fSNonEmpty)
)
(RULES
or(F,x) -> x
or(T,x) -> T
or(x,F) -> x
or(x,T) -> T
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


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 y)
(REPLACEMENT-MAP
(or 1, 2)
(F)
(T)
(fSNonEmpty)
)
(RULES
or(F,x) -> x
or(T,x) -> T
or(x,F) -> x
or(x,T) -> T
)
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 or(F,x) -> x
 or(T,x) -> T
 or(x,F) -> x
 or(x,T) -> T
-> Vars:
 x, x, x, x

-> Rlps:
 (rule: or(F,x) -> x, id: 1, possubterms: or(F,x)->[], F->[1])
 (rule: or(T,x) -> T, id: 2, possubterms: or(T,x)->[], T->[1])
 (rule: or(x,F) -> x, id: 3, possubterms: or(x,F)->[], F->[2])
 (rule: or(x,T) -> T, id: 4, possubterms: or(x,T)->[], T->[2])

-> Unifications:
(R3 unifies with R1 at p: [], l: or(x,F), lp: or(x,F), sig: {x -> F,x' -> F}, l': or(F,x'), r: x, r': x')
(R3 unifies with R2 at p: [], l: or(x,F), lp: or(x,F), sig: {x -> T,x' -> F}, l': or(T,x'), r: x, r': T)
(R4 unifies with R1 at p: [], l: or(x,T), lp: or(x,T), sig: {x -> F,x' -> T}, l': or(F,x'), r: T, r': x')
(R4 unifies with R2 at p: [], l: or(x,T), lp: or(x,T), sig: {x -> T,x' -> T}, l': or(T,x'), r: T, r': T)

-> Critical pairs info:
<T,T>   =>  Trivial, Overlay, Proper, NW0, N1
<T,T>   =>  Trivial, Overlay, Proper, NW0, N2
<T,T>   =>  Trivial, Overlay, Proper, NW0, N3
<F,F>   =>  Trivial, Overlay, Proper, NW0, N4

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


The problem is confluent.