Interoperate with provers for coherent logic

Via [Twitter](https://twitter.com/bblfish/status/1214928487393484803), Henry Story points to existing automated provers for coherent logic, particularly [EYE](https://github.com/josd/eye). What coherent logic provers are out there? Could they be integrated with Catlab to give a prover for distributive bicatgories of relations? When restricted to the regular fragment, this would also give a prover for (regular) bicategories of relations.