YES

---- CR(R)
---- [Jouannaud and Kirchner, 1986]
R:
not(T()) -> F()
not(F()) -> T()
or(x,T()) -> T()
or(x,F()) -> x
or(x,y) -> or(y,x)
or(or(x,y),z) -> or(x,or(y,z))
and(x,T()) -> x
and(x,F()) -> F()
and(x,y) -> and(y,x)
and(and(x,y),z) -> and(x,and(y,z))
imply(x,y) -> or(not(x),y)
CP_AC(R):
T() -> or(x,T())
T() -> T()
or(x,T()) -> T()
T() -> T()
and(x,F()) -> F()
F() -> F()
F() -> and(x,F())
F() -> F()
T() -> or(x,y,T())
T() -> or(x,T())
T() -> or(x,T(),y)
T() -> or(T(),x)
T() -> or(x,T(),y,z)
T() -> or(T(),x,y)
T() -> or(x,y,T(),z)
T() -> or(x,T(),y)
T() -> or(x,y,z,T())
T() -> or(x,y,T())
or(T(),x) -> or(y,T(),z,x)
or(T(),x) -> or(T(),y,x)
or(T(),x) -> or(y,z,T(),x)
or(T(),x) -> or(y,T(),x)
T() -> or(x,T(),y,z)
T() -> or(T(),x,y)
T() -> or(x,y,T(),z)
T() -> or(x,T(),y)
T() -> or(x,y,z,T())
T() -> or(x,y,T())
or(x,T()) -> or(x,y,T(),z)
or(x,T()) -> or(x,T(),y)
or(x,T()) -> or(x,y,z,T())
or(x,T()) -> or(x,y,T())
or(x,y) -> or(y,x,F())
x -> or(x,F())
or(x,y) -> or(y,F(),x)
x -> or(F(),x)
or(x,y,z) -> or(x,F(),y,z)
or(x,y) -> or(F(),x,y)
or(x,y,z) -> or(x,y,F(),z)
or(x,y) -> or(x,F(),y)
or(x,y,z) -> or(x,y,z,F())
or(x,y) -> or(x,y,F())
or(x,y,z) -> or(x,F(),y,z)
or(x,y) -> or(F(),x,y)
or(x,y,z) -> or(x,y,F(),z)
or(x,y) -> or(x,F(),y)
or(x,y,z) -> or(x,F(),y,z)
or(x,y) -> or(F(),x,y)
or(x,y,z) -> or(x,y,F(),z)
or(x,y) -> or(x,F(),y)
or(x,y,z) -> or(x,y,z,F())
or(x,y) -> or(x,y,F())
or(x,y,z) -> or(x,y,F(),z)
or(x,y) -> or(x,F(),y)
or(x,y,z) -> or(x,y,z,F())
or(x,y) -> or(x,y,F())
and(x,y) -> and(y,x,T())
x -> and(x,T())
and(x,y) -> and(y,T(),x)
x -> and(T(),x)
and(x,y,z) -> and(x,T(),y,z)
and(x,y) -> and(T(),x,y)
and(x,y,z) -> and(x,y,T(),z)
and(x,y) -> and(x,T(),y)
and(x,y,z) -> and(x,y,z,T())
and(x,y) -> and(x,y,T())
and(x,y,z) -> and(x,T(),y,z)
and(x,y) -> and(T(),x,y)
and(x,y,z) -> and(x,y,T(),z)
and(x,y) -> and(x,T(),y)
and(x,y,z) -> and(x,T(),y,z)
and(x,y) -> and(T(),x,y)
and(x,y,z) -> and(x,y,T(),z)
and(x,y) -> and(x,T(),y)
and(x,y,z) -> and(x,y,z,T())
and(x,y) -> and(x,y,T())
and(x,y,z) -> and(x,y,T(),z)
and(x,y) -> and(x,T(),y)
and(x,y,z) -> and(x,y,z,T())
and(x,y) -> and(x,y,T())
F() -> and(x,y,F())
F() -> and(x,F())
F() -> and(x,F(),y)
F() -> and(F(),x)
F() -> and(x,F(),y,z)
F() -> and(F(),x,y)
F() -> and(x,y,F(),z)
F() -> and(x,F(),y)
F() -> and(x,y,z,F())
F() -> and(x,y,F())
and(F(),x) -> and(y,F(),z,x)
and(F(),x) -> and(F(),y,x)
and(F(),x) -> and(y,z,F(),x)
and(F(),x) -> and(y,F(),x)
F() -> and(x,F(),y,z)
F() -> and(F(),x,y)
F() -> and(x,y,F(),z)
F() -> and(x,F(),y)
F() -> and(x,y,z,F())
F() -> and(x,y,F())
and(x,F()) -> and(x,y,F(),z)
and(x,F()) -> and(x,F(),y)
and(x,F()) -> and(x,y,z,F())
and(x,F()) -> and(x,y,F())