remove disjunctions by default

[KenSakayori]

We don't want to rely on PCSat, and thus, it is preferable to make an order n nuHFL formula tractable by translating it to an order (n + 1) formula.

I don't know how clever the preprocess is. I am wondering whether applying remove_disjunction procedure to an instance that didn't need this to be applied complicates the formula and prevents the solver to prove its (in)validity.

[moratorium08]

The reason why it's optional is that this feature was added after ReTHFL was initially created.

As far as I know, there is no instance where this feature causes "regression", so I also think that it is better to set it as the default.

[moratorium08]

I'm not sure how seriously we should manage ReTHFL, but it might be a good idea to keep remove-disjunction and perhaps issue a warning since some of our tool depends on ReTHFL, and possibly causes some trouble.

[KenSakayori]

I think it's fine to delete the option.
This repository has only been public for five months and I don't think that someone besides us is using ReTHFL.

It's true that we have some tools that are relying on ReTHFL, but we can fix how they invoke ReTHFL.
BTW, https://github.com/hopv/muhfl is currently broken (except for the docker image that bundles its own version of ReTHFL), so a breaking change is not a big issue for muHFL in the sense that it doesn't make a working tool not working.
And I'm planning to fix muHFL when I have time.