YES
(VAR x y z)
(RULES
trans(ortrue2(),x) -> ortrue2()
trans(ortrue1(),x) -> ortrue1()
trans(congror1(x),orfalse2()) -> trans(orfalse2(),x)
trans(congror2(x),orfalse1()) -> trans(orfalse1(),x)
trans(congror2(x),ortrue1()) -> ortrue1()
trans(congror1(x),ortrue2()) -> ortrue2()
trans(congror2(x),trans(orfalse1(),y)) -> trans(orfalse1(),trans(x,y))
trans(congror1(x),trans(orfalse2(),y)) -> trans(orfalse2(),trans(x,y))
trans(congror1(x),congror2(y)) -> trans(congror2(y),congror1(x))
trans(congror2(x),congror2(y)) -> congror2(trans(x,y))
trans(congror1(x),congror1(y)) -> congror1(trans(x,y))
trans(congror1(x),trans(congror2(y),z)) -> trans(congror2(y),trans(congror1(x),z))
trans(congror1(x),trans(congror1(y),z)) -> trans(congror1(trans(x,y)),z)
trans(congror2(x),trans(congror2(y),z)) -> trans(congror2(trans(x,y)),z)
trans(congror2(x),trans(congror1(y),ortrue1())) -> trans(congror1(y),ortrue1())
trans(congror2(x),trans(congror1(y),orfalse1())) -> trans(congror1(y),trans(orfalse1(),x))
trans(congror2(x),trans(congror1(y),trans(orfalse1(),z))) -> trans(congror1(y),trans(orfalse1(),trans(x,z)))
trans(trans(x,y),z) -> trans(x,trans(y,z))
trans(refl(),x) -> x
trans(x,refl()) -> x
congror1(refl()) -> refl()
congror2(refl()) -> refl()
)