Tool claims "success" despite crash (after java.lang.OutOfMemoryError)

[xamidi]

I wanted to test how reliable this prover is, and started with modifying maintest.scala to only prove 1. p→p and 2. Meredith's axiom.

val (p, q, r, s, t) = (Atom("p"), Atom("q"), Atom("r"), Atom("s"), Atom("t"))
//[...]
|- (p -> p)
|- ( ((((p -> q) -> (~r -> ~s)) -> r) -> t) -> ((t -> p) -> (s -> p)) )

Here is the output it generated:

$ sbt "run"
[info] welcome to sbt 1.10.10 (Oracle Corporation Java 22.0.1)
[info] loading project definition from C:\Users\user\Desktop\tmp\HilbertProver\project
[info] loading settings for project hilbertprover from build.sbt...
[info] set current project to hilbertprover (in build file:/C:/Users/user/Desktop/tmp/HilbertProver/)
[info] compiling 1 Scala source to C:\Users\user\Desktop\tmp\HilbertProver\target\scala-2.12\classes ...
[info] done compiling
[info] running prover.test.CoreTest
[info] prove for p -> p with assumption List()
[info] proved for total 5 cases
[info] the length of the proof of p -> p : 5
    1: p -> (<8> -> p)                                                                                     [L1]
    2: p -> ((<8> -> p) -> p)                                                                              [L1]
    3: (p -> ((<8> -> p) -> p)) -> ((p -> (<8> -> p)) -> (p -> p))                                         [L2]
    4: (p -> (<8> -> p)) -> (p -> p)                                                                       [MP]
    5: p -> p                                                                                              [MP]
[info] prove for ((((p -> q) -> (¬r -> ¬s)) -> r) -> t) -> ((t -> p) -> (s -> p)) with assumption List()
[info] proved for 50000 cases
[info] proved for 100000 cases
[info] proved for 150000 cases
[info] proved for 200000 cases
[info] proved for 250000 cases
[info] proved for 300000 cases
[info] proved for 350000 cases
[info] proved for 400000 cases
[info] proved for 450000 cases
[info] proved for 500000 cases
[info] proved for 550000 cases
[info] proved for 600000 cases
[info] proved for 650000 cases
[info] proved for 700000 cases
[info] proved for 750000 cases
[info] proved for 800000 cases
[info] proved for 850000 cases
[info] proved for 900000 cases
[info] proved for 950000 cases
[info] proved for 1000000 cases
[info] proved for 1050000 cases
[info] proved for 1100000 cases
[info] proved for 1150000 cases
[info] proved for 1200000 cases
[info] proved for 1250000 cases
[info] proved for 1300000 cases
[info] proved for 1350000 cases
[info] proved for 1400000 cases
[info] proved for 1450000 cases
[info] proved for 1500000 cases
[info] proved for 1550000 cases
[info] proved for 1600000 cases
[info] proved for 1650000 cases
[info] proved for 1700000 cases
[info] proved for 1750000 cases
[info] proved for 1800000 cases
[info] proved for 1850000 cases
[info] proved for 1900000 cases
[info] proved for 1950000 cases
[info] proved for 2000000 cases
[info] proved for 2050000 cases
[info] proved for 2100000 cases
[info] proved for 2150000 cases
[info] proved for 2200000 cases
[info] proved for 2250000 cases
[info] proved for 2300000 cases
[info] proved for 2350000 cases
[info] proved for 2400000 cases
[info] proved for 2450000 cases
[info] proved for 2500000 cases
[info] proved for 2550000 cases
[info] proved for 2600000 cases
[info] proved for 2650000 cases
[info] proved for 2700000 cases
[info] proved for 2750000 cases
[info] proved for 2800000 cases
[info] proved for 2850000 cases
[info] proved for 2900000 cases
[warn] In the last 10 seconds, 5.065 (51,5%) were spent in GC. [Heap: 0,03GB free of 1,00GB, max 1,00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.
[info] proved for 2950000 cases
[info] proved for 3000000 cases
[warn] In the last 10 seconds, 8.879 (94,3%) were spent in GC. [Heap: 0,01GB free of 1,00GB, max 1,00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.
[warn] In the last 10 seconds, 9.357 (97,7%) were spent in GC. [Heap: 0,00GB free of 1,00GB, max 1,00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.
[warn] In the last 10 seconds, 9.346 (98,6%) were spent in GC. [Heap: 0,00GB free of 1,00GB, max 1,00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.
[warn] In the last 10 seconds, 9.908 (99,1%) were spent in GC. [Heap: 0,01GB free of 1,00GB, max 1,00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.
[warn] In the last 10 seconds, 9.088 (97,6%) were spent in GC. [Heap: 0,00GB free of 1,00GB, max 1,00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.
[info] proved for 3050000 cases
[warn] In the last 10 seconds, 9.142 (98,1%) were spent in GC. [Heap: 0,00GB free of 1,00GB, max 1,00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.
[warn] In the last 10 seconds, 8.523 (91,3%) were spent in GC. [Heap: 0,00GB free of 1,00GB, max 1,00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.

Exception: java.lang.OutOfMemoryError thrown from the UncaughtExceptionHandler in thread "classloader-cache-cleanup-0"
Exception in thread "sbt-bg-threads-1" java.lang.OutOfMemoryError: Java heap space: failed reallocation of scalar replaced objects
[warn] In the last 10 seconds, 29.005 (306,3%) were spent in GC. [Heap: 0,96GB free of 1,00GB, max 1,00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.
[success] Total time: 133 s (0:02:13.0), completed 10.09.2025, 12:57:43