EQUATIONS: 
trans(trans(x1,x2),x3) = trans(x1,trans(x2,x3))
trans(refl(),x1) = x1
trans(x1,refl()) = x1
congror1(refl()) = refl()
congror2(refl()) = refl()
trans(congror1(x1),ortrue2()) = ortrue2()
trans(congror2(x1),ortrue1()) = ortrue1()
trans(orfalse1(),x1) = trans(congror2(x1),orfalse1())
trans(orfalse2(),x1) = trans(congror1(x1),orfalse2())
trans(trans(congror1(x1),congror2(x2)),trans(congror1(x3),congror2(x4))) =
  trans(congror1(trans(x1,x3)),congror2(trans(x2,x4)))
trans(ortrue1(),x1) = ortrue1()
trans(ortrue2(),x1) = ortrue2()

Fatal error: exception Maxcomp.Fail("I'm giving up
")