2020-03-27 15:18:52 (GMT)
I have just added a flag --unif-bool to enable/disable unification of polymorphic variables with booleans. For example, if you have ¬p (which becomes p != true by CNF) and a polymorphic X = Y, then this should be satisfiable in FOL, but Zipperposition finds a proof (To be honest, I haven't tested this, but I am pretty sure).
The default of this option is of course true, as we need it for HO reasoning. I set it to false for the FO and lambda-free modes. Should it also be set to false if the problem is given in TFF format?
2020-03-27 15:21:35 (GMT)
And I added a warning message when this option is set to false because Petar asked for that. I am not sure if that makes sense.
2020-03-27 15:22:31 (GMT)
Can I delete bool_encode then?
2020-03-27 16:24:9 (GMT)
You can delete bool encode.
2020-03-27 16:24:59 (GMT)
If we need it we can get it back from the history