SUCCESS
162.66 (total time)

COMPLETED TRS
CongrNot(refl) -> refl
CongrAnd2(refl) -> refl
CongrAnd1(refl) -> refl
CongrOr2(refl) -> refl
CongrOr1(refl) -> refl
trans(CongrNot(x), CongrNot(y)) -> CongrNot(trans(x, y))
trans(CongrNot(x), trans(CongrNot(y), z)) -> trans(CongrNot(trans(x, y)), z)
trans(CongrAnd2(y), trans(AndFalse1, x)) -> trans(AndFalse1, x)
trans(CongrAnd2(x), AndTrue1) -> trans(AndTrue1, x)
trans(CongrAnd2(x), AndFalse1) -> AndFalse1
trans(CongrAnd2(x), CongrAnd2(y)) -> CongrAnd2(trans(x, y))
trans(CongrAnd2(x), CongrAnd1(y)) -> trans(CongrAnd1(y), CongrAnd2(x))
trans(CongrAnd2(x), trans(AndTrue1, y)) -> trans(AndTrue1, trans(x, y))
trans(CongrAnd2(x), trans(CongrAnd2(y), z)) -> trans(CongrAnd2(trans(x, y)), z)
trans(CongrAnd2(x), trans(CongrAnd1(y), AndTrue1)) -> trans(CongrAnd1(y), trans(AndTrue1, x))
trans(CongrAnd2(x), trans(CongrAnd1(y), AndFalse1)) -> trans(CongrAnd1(y), AndFalse1)
trans(CongrAnd2(x), trans(CongrAnd1(y), CongrAnd2(z))) -> trans(CongrAnd1(y), CongrAnd2(trans(x, z)))
trans(CongrAnd2(x), trans(CongrAnd1(y), trans(AndTrue1, z))) -> trans(CongrAnd1(y), trans(AndTrue1, trans(x, z)))
trans(CongrAnd2(x), trans(CongrAnd1(y), trans(AndFalse1, z))) -> trans(CongrAnd1(y), trans(AndFalse1, z))
trans(CongrAnd1(y), trans(AndFalse2, x)) -> trans(AndFalse2, x)
trans(CongrAnd1(y), trans(CongrAnd2(x), z)) -> trans(CongrAnd2(x), trans(CongrAnd1(y), z))
trans(CongrAnd1(x), AndTrue2) -> trans(AndTrue2, x)
trans(CongrAnd1(x), AndFalse2) -> AndFalse2
trans(CongrAnd1(x), CongrAnd1(y)) -> CongrAnd1(trans(x, y))
trans(CongrAnd1(x), trans(AndTrue2, y)) -> trans(AndTrue2, trans(x, y))
trans(CongrAnd1(x), trans(CongrAnd1(y), z)) -> trans(CongrAnd1(trans(x, y)), z)
trans(CongrOr2(y), trans(OrTrue1, x)) -> trans(OrTrue1, x)
trans(CongrOr2(x), OrFalse1) -> trans(OrFalse1, x)
trans(CongrOr2(x), OrTrue1) -> OrTrue1
trans(CongrOr2(x), CongrOr2(y)) -> CongrOr2(trans(x, y))
trans(CongrOr2(x), CongrOr1(y)) -> trans(CongrOr1(y), CongrOr2(x))
trans(CongrOr2(x), trans(OrFalse1, y)) -> trans(OrFalse1, trans(x, y))
trans(CongrOr2(x), trans(CongrOr2(y), z)) -> trans(CongrOr2(trans(x, y)), z)
trans(CongrOr2(x), trans(CongrOr1(y), OrFalse1)) -> trans(CongrOr1(y), trans(OrFalse1, x))
trans(CongrOr2(x), trans(CongrOr1(y), OrTrue1)) -> trans(CongrOr1(y), OrTrue1)
trans(CongrOr2(x), trans(CongrOr1(y), CongrOr2(z))) -> trans(CongrOr1(y), CongrOr2(trans(x, z)))
trans(CongrOr2(x), trans(CongrOr1(y), trans(OrFalse1, z))) -> trans(CongrOr1(y), trans(OrFalse1, trans(x, z)))
trans(CongrOr2(x), trans(CongrOr1(y), trans(OrTrue1, z))) -> trans(CongrOr1(y), trans(OrTrue1, z))
trans(CongrOr1(y), trans(OrTrue2, x)) -> trans(OrTrue2, x)
trans(CongrOr1(y), trans(CongrOr2(x), z)) -> trans(CongrOr2(x), trans(CongrOr1(y), z))
trans(CongrOr1(x), OrFalse2) -> trans(OrFalse2, x)
trans(CongrOr1(x), OrTrue2) -> OrTrue2
trans(CongrOr1(x), CongrOr1(y)) -> CongrOr1(trans(x, y))
trans(CongrOr1(x), trans(OrFalse2, y)) -> trans(OrFalse2, trans(x, y))
trans(CongrOr1(x), trans(CongrOr1(y), z)) -> trans(CongrOr1(trans(x, y)), z)
trans(refl, x) -> x
trans(trans(x, y), z) -> trans(x, trans(y, z))
trans(x, refl) -> x