VAMPIRE: Fix lower bound structure

[ArenBabikian]

No description provided.

[ArenBabikian]

Mentioning a constant (ex. o1) in the input file triggers the solver to necessarily create it as a node in the generated finite model. This is problematic because currently, we are mentioning the list of constants for the scope minimum and maximum (ex. MinScope = (object <=> o1..o3), MaxSope = (object <=>o1..o6) ).
In this example, the solver will attempt to find finite models with 6 nodes because 6 constants are mentioned. These nodes may not all be objects because the scope minimum and maximum formula structure is logically correct, however, if the solver cannot handle finite models with 6 nodes (ex. timeout or memory limit reached), then no models at all will be generated.

[ArenBabikian]

The solution to this issue may rely in tweaking the solver itself (ex. through command line parameters, maybe).

[ArenBabikian]

A possibility would be to introduce model elements as skolem constants.