Look into first order logic reasoning engines

It looks like z3 cannot prove even very simple unequivalence with ForAll (https://git.science.uu.nl/d.h.ogilvie2/javawlp/commit/9f58f2ce85189f2995075801d49f0da6f5e2d55b#abb63567c9d6fd227500c8306dbe43002f6c8612_0_35)

Possible alternative engines to use:

• https://hackage.haskell.org/package/prolog
• http://src.seereason.com/chiou-prover/report.ps report.pdf
• https://hackage.haskell.org/package/Folly
• https://hackage.haskell.org/package/logic-classes
• https://github.com/daijo/fol
• https://github.com/dillonhuff/Folly

Perhaps some of these could be implemented as a LogicIR.Backend