EQUATIONS: 
trans(trans(x,y),z) = trans(x,trans(y,z))
trans(refl(),x) = x
trans(x,refl()) = x
congror1(refl()) = refl()
congror2(refl()) = refl()
trans(congror1(x),ortrue2()) = ortrue2()
trans(congror2(x),ortrue1()) = ortrue1()
trans(congror2(x),orfalse1()) = trans(orfalse1(),x)
trans(congror1(x),orfalse2()) = trans(orfalse2(),x)
trans(trans(congror1(x),congror2(y)),trans(congror1(z),congror2(w))) =
  trans(congror1(trans(x,z)),congror2(trans(y,w)))
trans(ortrue1(),x) = ortrue1()
trans(ortrue2(),x) = ortrue2()

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