Experiment: Egg vs. Z3 (validity checking)

[corwin-of-amber]

Collect benchmarks from unsat formulas. Translate formulas to terms and "forall" expressions to rewrite rules.

• Use early stopping
• Find dataset (SMTLIB)
• Implement deep case splitting
• Run colored
• Run cloned
  • Memory limit
• Run Z3, CVC5

Blocked by #7.