YES
(VAR x1 x2 x3)
(RULES
trans(ortrue2(),x1) -> ortrue2()
trans(ortrue1(),x1) -> ortrue1()
trans(congror1(x1),orfalse2()) -> trans(orfalse2(),x1)
trans(congror2(x1),orfalse1()) -> trans(orfalse1(),x1)
trans(congror2(x1),ortrue1()) -> ortrue1()
trans(congror1(x1),ortrue2()) -> ortrue2()
trans(congror2(x1),trans(orfalse1(),x2)) -> trans(orfalse1(),trans(x1,x2))
trans(congror1(x1),trans(orfalse2(),x2)) -> trans(orfalse2(),trans(x1,x2))
trans(congror1(x1),congror2(x2)) -> trans(congror2(x2),congror1(x1))
trans(congror2(x1),congror2(x2)) -> congror2(trans(x1,x2))
trans(congror1(x1),congror1(x2)) -> congror1(trans(x1,x2))
trans(congror1(x1),trans(congror2(x2),x3)) -> trans(congror2(x2),trans(congror1(x1),x3))
trans(congror1(x1),trans(congror1(x2),x3)) -> trans(congror1(trans(x1,x2)),x3)
trans(congror2(x1),trans(congror2(x2),x3)) -> trans(congror2(trans(x1,x2)),x3)
trans(congror2(x1),trans(congror1(x2),ortrue1())) -> trans(congror1(x2),ortrue1())
trans(congror2(x1),trans(congror1(x2),orfalse1())) -> trans(congror1(x2),trans(orfalse1(),x1))
trans(congror2(x1),trans(congror1(x2),trans(orfalse1(),x3))) -> trans(congror1(x2),trans(orfalse1(),trans(x1,x3)))
trans(trans(x1,x2),x3) -> trans(x1,trans(x2,x3))
trans(refl(),x1) -> x1
trans(x1,refl()) -> x1
congror1(refl()) -> refl()
congror2(refl()) -> refl()
)