SUCCESS
2.52 (total time)

COMPLETED TRS
congror2(refl) -> refl
congror1(refl) -> refl
trans(ortrue1, x) -> ortrue1
trans(ortrue2, x) -> ortrue2
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(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