YES
(VAR x y z)
(RULES
trans(CongrNot(x),CongrNot(y)) -> CongrNot(trans(x,y))
trans(CongrAnd1(x),AndTrue2()) -> trans(AndTrue2(),x)
trans(CongrAnd2(x),AndTrue1()) -> trans(AndTrue1(),x)
trans(CongrOr1(x),OrFalse2()) -> trans(OrFalse2(),x)
trans(CongrOr2(x),OrFalse1()) -> trans(OrFalse1(),x)
trans(CongrAnd2(x),AndFalse1()) -> AndFalse1()
trans(CongrAnd1(x),AndFalse2()) -> AndFalse2()
trans(CongrOr2(x),OrTrue1()) -> OrTrue1()
trans(CongrOr1(x),OrTrue2()) -> OrTrue2()
trans(x,trans(y,z)) -> trans(trans(x,y),z)
trans(trans(x,CongrOr2(y)),OrFalse1()) -> trans(trans(x,OrFalse1()),y)
trans(trans(x,CongrOr1(y)),OrFalse2()) -> trans(trans(x,OrFalse2()),y)
trans(trans(x,CongrAnd2(y)),AndTrue1()) -> trans(trans(x,AndTrue1()),y)
trans(trans(x,CongrAnd1(y)),AndTrue2()) -> trans(trans(x,AndTrue2()),y)
trans(CongrAnd1(x),CongrAnd1(y)) -> CongrAnd1(trans(x,y))
trans(CongrAnd2(x),CongrAnd2(y)) -> CongrAnd2(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(trans(CongrOr2(x),CongrOr1(y)),OrTrue1()) -> trans(CongrOr1(y),OrTrue1())
trans(trans(x,CongrAnd2(y)),CongrAnd1(z)) -> trans(trans(x,CongrAnd1(z)),CongrAnd2(y))
trans(trans(CongrAnd1(x),CongrAnd2(y)),AndTrue2()) -> trans(trans(CongrAnd2(y),AndTrue2()),x)
trans(trans(CongrAnd1(x),CongrAnd2(y)),AndFalse2()) -> trans(CongrAnd2(y),AndFalse2())
trans(trans(trans(x,CongrOr2(y)),CongrOr1(z)),OrFalse1()) -> trans(trans(trans(x,CongrOr1(z)),OrFalse1()),y)
trans(trans(x,CongrOr1(y)),CongrOr2(z)) -> trans(trans(x,CongrOr2(z)),CongrOr1(y))
trans(trans(trans(x,CongrAnd1(y)),CongrAnd2(z)),AndTrue2()) -> trans(trans(trans(x,CongrAnd2(z)),AndTrue2()),y)
trans(trans(trans(x,CongrAnd1(y)),CongrAnd2(z)),AndFalse2()) -> trans(trans(x,CongrAnd2(z)),AndFalse2())
trans(trans(trans(x,CongrOr2(y)),CongrOr1(z)),OrTrue1()) -> trans(trans(x,CongrOr1(z)),OrTrue1())
trans(trans(x,CongrAnd1(y)),CongrAnd1(z)) -> trans(x,CongrAnd1(trans(y,z)))
trans(trans(x,CongrAnd2(y)),CongrAnd2(z)) -> trans(x,CongrAnd2(trans(y,z)))
trans(trans(x,CongrOr2(y)),CongrOr2(z)) -> trans(x,CongrOr2(trans(y,z)))
trans(trans(x,CongrOr1(y)),CongrOr1(z)) -> trans(x,CongrOr1(trans(y,z)))
trans(trans(CongrOr2(x),CongrOr1(y)),OrFalse1()) -> trans(trans(CongrOr1(y),OrFalse1()),x)
trans(CongrAnd2(x),CongrAnd1(y)) -> trans(CongrAnd1(y),CongrAnd2(x))
trans(trans(x,CongrAnd2(y)),AndFalse1()) -> trans(x,AndFalse1())
trans(trans(x,CongrAnd1(y)),AndFalse2()) -> trans(x,AndFalse2())
trans(trans(x,CongrOr2(y)),OrTrue1()) -> trans(x,OrTrue1())
trans(trans(x,CongrOr1(y)),OrTrue2()) -> trans(x,OrTrue2())
trans(trans(x,CongrNot(y)),CongrNot(z)) -> trans(x,CongrNot(trans(y,z)))
trans(refl(),x) -> x
trans(x,refl()) -> x
CongrOr1(refl()) -> refl()
CongrOr2(refl()) -> refl()
CongrAnd1(refl()) -> refl()
CongrAnd2(refl()) -> refl()
CongrNot(refl()) -> refl()
)