Minisat ran out of memory

[mereolog]

Running the following command with Vampire 4.9:
./vampire --saturation_algorithm fmb -t 0 -m 1000000 bfo.tptp > bfo.szs
I got a 'Minisat ran out of memory' error - see below.

Note that the VM I use has 1TB of RAM, so the source does not seem to be related to the hardware limits.

Here is the input file: bfo.tptp.zip

% Running in auto input_syntax mode. Trying TPTP
Detected minimum model sizes of [35]
Detected maximum model sizes of [max]
TRYING [35]
Minisat ran out of memory
% ------------------------------
% Version: Vampire 4.9 (commit 5ad494e78 on 2024-06-14 14:05:27 +0100)
% Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d
% Termination reason: Unknown
% Termination phase: Finite model building constraint generation

% Memory used [KB]: 394148089
% Time elapsed: 1626.808 s
% ------------------------------
% ------------------------------
Version : Vampire 4.9 (commit 5ad494e78 on 2024-06-14 14:05:27 +0100)