Results for mrs commit 40b17e46103c71888d09be3ec59430a92c724008

ongoing
[PPROD:fr22192@tlpnf9701:/DATA/ai/fr22192/mrs]$ crates/mrs-bench/casc.sh --systems mrs,vampire,eprover --jobs 30

ongoing
hack@pve:~/mrs$ crates/mrs-bench/casc.sh --systems mrs,vampire,eprover --jobs 4

Results for mrs commit 9f386fff39b43a4c77a631e066080524bc74231f

to be analyzed
hack@pve:~/mrs$ cargo run --release --bin mrs -- --time 480 ~/TPTP-v9.2.1/Problems/GRP/GRP751-1.p
    Finished `release` profile [optimized] target(s) in 0.27s
     Running `target/release/mrs --time 480 /home/hack/TPTP-v9.2.1/Problems/GRP/GRP751-1.p`
% Problem: GRP751-1 (0 axioms, 0 conjectures, 8 cnf clauses)
% SZS status Timeout for GRP751-1
% ------------------------------
% Version: mrs 0.1.10
% Termination reason: Timeout
% Time elapsed: 480.533 s
% Peak memory usage: 229 MB
% ------------------------------

Results for mrs commit 4345265f468dc6038471ada870239dbe9c8edec0

ongoing
[PPROD:fr22192@tlpnf9701:/DATA/ai/fr22192/mrs]$ crates/mrs-bench/casc.sh --systems reference,mrs --jobs 30 --time 240
     Running `target/debug/bench_report /DATA/ai/fr22192/mrs/crates/mrs-bench/results/casc-30/20260529_153630/run.csv`
CASC-30 Results — 2026-05-29 15:49  (1101 problems × 2 systems)
===============================================================

Division  Problems    mrs                   reference
                      Solved  Avg (s)      Solved  Avg (s)
------------------  --------------------  --------------------
FNE            100        26   27.331         100    0.032
FEQ            400        16   41.223         399    0.031
EPU            100         8    5.083         100    0.032
EPS            100         0    0.000         100    0.033
UEQ            300        26   50.078         300    0.031
ICU            101         2   17.092          57    0.031
------------------  --------------------  --------------------
TOTAL         1101        78   35.219        1056    0.031

DISAGREEMENTS — none detected.

POLARITY VIOLATIONS — none detected.

ongoing
[PPROD:fr22192@tlpnf9701:/DATA/ai/fr22192/mrs]$ crates/mrs-bench/casc.sh --systems reference,mrs --jobs 30
CASC-30 Results — 2026-05-29 12:17  (1101 problems × 2 systems)
===============================================================

Division  Problems    mrs                   reference
                      Solved  Avg (s)      Solved  Avg (s)
------------------  --------------------  --------------------
FNE            100        24   13.303         100    0.032
FEQ            400        16   21.884         399    0.031
EPU            100         8    3.534         100    0.032
EPS            100         0    0.000         100    0.033
UEQ            300        17   37.019         300    0.031
ICU            101         1    0.363          57    0.032
------------------  --------------------  --------------------
TOTAL         1101        66   20.112        1056    0.032

DISAGREEMENTS — none detected.

POLARITY VIOLATIONS — none detected.

ongoing
hack@pve:~/mrs$ TPTP=/home/hack/mrs/crates/mrs-bench/problems/casc-30 crates/mrs-bench/casc.sh --systems reference,mrs --jobs 3 --divisions ueq
CASC-30 Results — 2026-05-29 12:21  (300 problems × 2 systems)
==============================================================

Division  Problems    mrs                   reference
                      Solved  Avg (s)      Solved  Avg (s)
------------------  --------------------  --------------------
UEQ            300        18   32.820         300    0.014
------------------  --------------------  --------------------
TOTAL          300        18   32.820         300    0.014

DISAGREEMENTS — none detected.

POLARITY VIOLATIONS — none detected.

Results for mrs commit df21f4b06de8483420a0ff72aef7f2e3129dcc52

ongoing
[root@mtsdev02 mrs]# TPTP=/mnt/sda1/mrs/crates/mrs-bench/problems/casc-30 crates/mrs-bench/casc.sh --systems reference,mrs

Results for mrs commit b4b78ac62853b7903d64ab6654b2e7e86e426dd2

ongoing
[www@teenf9901 mrs]$ TPTP=/DATA/ai/mrs/crates/mrs-bench/problems/casc-30 crates/mrs-bench/casc.sh --systems reference,mrs

Results for mrs commit a5b220380d6a24234c59275a188a4f6a948f7160

[www@teenf9901 mrs]$ TPTP=/DATA/ai/mrs/crates/mrs-bench/problems/casc-30 crates/mrs-bench/casc.sh --systems reference,mrs --divisions fne
Division  Problems    mrs                   reference
                      Solved  Avg (s)      Solved  Avg (s)
------------------  --------------------  --------------------
FNE            100        26   13.872         100    0.019
------------------  --------------------  --------------------
TOTAL          100        26   13.872         100    0.019

DISAGREEMENTS — 3 problem(s) where systems gave contradictory answers:
  FNE     LCL660+1.015                    mrs=CounterSatisfiable  reference=Theorem  ⚠ SOUNDNESS
  FNE     SYN938+1                        mrs=CounterSatisfiable  reference=Theorem  ⚠ SOUNDNESS
  FNE     SYN986+1.004                    mrs=CounterSatisfiable  reference=Theorem  ⚠ SOUNDNESS

POLARITY VIOLATIONS — none detected.

Results for mrs commit c6eb579c47b11726154c1eaa6c215c1edc21ea2c

[root@mtsdev02 mrs]# TPTP=/mnt/sda1/mrs/crates/mrs-bench/problems/casc-30 crates/mrs-bench/casc.sh --systems reference,mrs
CASC-30 Results — 2026-05-28 16:26  (1101 problems × 2 systems)
===============================================================

Division  Problems    mrs                   reference
                      Solved  Avg (s)      Solved  Avg (s)
------------------  --------------------  --------------------
FNE            100        25   11.442           0    0.000
FEQ            400       208   11.069           0    0.000
EPU            100        11   12.286           0    0.000
EPS            100        18    9.831           0    0.000
UEQ            300        26   12.263           0    0.000
ICU            101        40   15.654           0    0.000
------------------  --------------------  --------------------
TOTAL         1101       328   11.724           0    0.000

DISAGREEMENTS — none detected.

POLARITY VIOLATIONS — 13 case(s) of wrong SZS polarity:
  EPU     SYN885-1                        mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  EPS     NLP006-1                        mrs=Unsatisfiable  (expected one of ["CounterSatisfiable", "Satisfiable"])  ⚠ UNSOUND
  EPS     NLP008-1                        mrs=Unsatisfiable  (expected one of ["CounterSatisfiable", "Satisfiable"])  ⚠ UNSOUND
  EPS     NLP012-1                        mrs=Unsatisfiable  (expected one of ["CounterSatisfiable", "Satisfiable"])  ⚠ UNSOUND
  UEQ     LAT080-1                        mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     LAT081-1                        mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     LAT082-1                        mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     LAT084-1                        mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     LAT085-1                        mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     LAT092-1                        mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     LAT096-1                        mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     LAT097-1                        mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     LAT392-1                        mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND

Results for mrs commit 38f023ef0e0319226bf659fc5dc9f53511eb81c2

[www@teenf9901 mrs]$ TPTP=/DATA/ai/mrs/crates/mrs-bench/problems/casc-30 crates/mrs-bench/casc.sh --systems reference,mrs
CASC-30 Results — 2026-05-28 08:03  (1101 problems × 2 systems)
===============================================================

Division  Problems    mrs                   reference
                      Solved  Avg (s)      Solved  Avg (s)
------------------  --------------------  --------------------
FNE            100        16    9.517         100    0.019
FEQ            400        37    5.110         399    0.019
EPU            100        11   10.095         100    0.019
EPS            100        14    3.182         100    0.019
UEQ            300        19   34.888         300    0.019
ICU            101         7    0.058          57    0.019
------------------  --------------------  --------------------
TOTAL         1101       104   11.156        1056    0.019

DISAGREEMENTS — 3 problem(s) where systems gave contradictory answers:
  EPS     NLP006-1                        mrs=Unsatisfiable  reference=Satisfiable  ⚠ SOUNDNESS
  EPS     NLP008-1                        mrs=Unsatisfiable  reference=Satisfiable  ⚠ SOUNDNESS
  ICU     VVA001+1                        mrs=Theorem  reference=CounterSatisfiable  ⚠ SOUNDNESS

POLARITY VIOLATIONS — 2 case(s) of wrong SZS polarity:
  EPS     NLP006-1                        mrs=Unsatisfiable  (expected one of ["CounterSatisfiable", "Satisfiable"])  ⚠ UNSOUND
  EPS     NLP008-1                        mrs=Unsatisfiable  (expected one of ["CounterSatisfiable", "Satisfiable"])  ⚠ UNSOUND

ongoing
hack@pve:~/mrs$ TPTP=/home/hack/mrs/crates/mrs-bench/problems/casc-30 crates/mrs-bench/casc.sh --systems reference,mrs --divisions eps,epu,feq
CASC-30 Results — 2026-05-28 10:44  (600 problems × 2 systems)
==============================================================

Division  Problems    mrs                   reference
                      Solved  Avg (s)      Solved  Avg (s)
------------------  --------------------  --------------------
EPS            100        15    3.939         100    0.011
EPU            100        11    4.952         100    0.011
FEQ            400        64    1.794         399    0.011
------------------  --------------------  --------------------
TOTAL          600        90    2.537         599    0.011

DISAGREEMENTS — 3 problem(s) where systems gave contradictory answers:
  EPS     NLP006-1                        mrs=Unsatisfiable  reference=Satisfiable  ⚠ SOUNDNESS
  EPS     NLP008-1                        mrs=Unsatisfiable  reference=Satisfiable  ⚠ SOUNDNESS
  EPS     NLP012-1                        mrs=Unsatisfiable  reference=Satisfiable  ⚠ SOUNDNESS

POLARITY VIOLATIONS — 3 case(s) of wrong SZS polarity:
  EPS     NLP006-1                        mrs=Unsatisfiable  (expected one of ["CounterSatisfiable", "Satisfiable"])  ⚠ UNSOUND
  EPS     NLP008-1                        mrs=Unsatisfiable  (expected one of ["CounterSatisfiable", "Satisfiable"])  ⚠ UNSOUND
  EPS     NLP012-1                        mrs=Unsatisfiable  (expected one of ["CounterSatisfiable", "Satisfiable"])  ⚠ UNSOUND

hack@pve:~/mrs$ TPTP=/home/hack/mrs/crates/mrs-bench/problems/casc-30 crates/mrs-bench/casc.sh --systems reference,mrs --divisions fne,ueq
[casc] Done. Results: /home/hack/mrs/crates/mrs-bench/results/casc-30/20260527_161327/run.csv
hack@pve:~/mrs$
────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
==============================================================

Division  Problems    mrs                   reference
                      Solved  Avg (s)      Solved  Avg (s)
------------------  --------------------  --------------------
FNE            100        19    4.990         100    0.011
UEQ            300        15   21.399         300    0.011
------------------  --------------------  --------------------
TOTAL          400        34   12.229         400    0.011

DISAGREEMENTS — none detected.

POLARITY VIOLATIONS — none detected.

Results for mrs commit 4c7418c39df5b1ea489d560d4b5fb8a97f5836f0
[www@teenf9901 mrs]$ cargo run -p mrs-bench --bin bench_report -- /DATA/ai/mrs/crates/mrs-bench/results/casc-30/20260527_095507/run.csv
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.03s
     Running `target/debug/bench_report /DATA/ai/mrs/crates/mrs-bench/results/casc-30/20260527_095507/run.csv`
CASC-30 Results — 2026-05-27 09:43  (100 problems × 1 systems)
==============================================================

Division  Problems    mrs
                      Solved  Avg (s)
------------------  --------------------
FNE            100         7    5.715
------------------  --------------------
TOTAL          100         7    5.715


Results for mrs commit d9dacb516c0cf5c17c5eda34d7b67436057ac138

mtsdev02 still ongoing [casc] 586/1101 completed
CASC-30 Results — 2026-05-28 06:42  (1101 problems × 1 systems)
===============================================================

Division  Problems    mrs
                      Solved  Avg (s)
------------------  --------------------
FNE            100         7    5.954
FEQ            400        63    3.385
EPU            100         8    3.063
EPS            100        35    3.533
UEQ            300        20   18.862
ICU            101         9    1.570
------------------  --------------------
TOTAL         1101       142    5.595

DISAGREEMENTS — none detected.

POLARITY VIOLATIONS — 8 case(s) of wrong SZS polarity:
  EPU     MSC024-1                        mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     LCL195-10                       mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     LCL203-10                       mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     LCL211-10                       mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     LCL224-10                       mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     LCL416-10                       mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     NUM284-10.014                   mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     RNG001-10                       mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND


[www@teenf9901 mrs]$ ./crates/mrs-bench/systems/vampire/bin/vampire --version
Vampire 5.0.1 (Release build, commit cb4838130 on 2026-05-26 10:04:53 +0200)
CaDiCaL: cadical-2.1.3
Linked to Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
[www@teenf9901 mrs]$ TPTP=/DATA/ai/mrs/crates/mrs-bench/problems/casc-30 crates/mrs-bench/casc.sh --systems mrs,vampire --divisions fne,ueq
[www@teenf9901 mrs]$ cargo run -p mrs-bench --bin bench_report -- /DATA/ai/mrs/crates/mrs-bench/results/casc-30/20260526_191646/run.csv
   Compiling mrs-bench v0.1.1 (/DATA/ai/mrs/crates/mrs-bench)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.68s
     Running `target/debug/bench_report /DATA/ai/mrs/crates/mrs-bench/results/casc-30/20260526_191646/run.csv`
CASC-30 Results — 2026-05-27 06:16  (400 problems × 2 systems)
==============================================================

Division  Problems    mrs                   vampire
                      Solved  Avg (s)      Solved  Avg (s)
------------------  --------------------  --------------------
FNE            100         7    5.677          79   10.925
UEQ            300        22   28.067         233   16.129
------------------  --------------------  --------------------
TOTAL          400        29   22.663         312   14.812

DISAGREEMENTS — 8 problem(s) where systems gave contradictory answers:
  FNE     MGT067+1                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     SYN457+1                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     SYO606+1                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  UEQ     LCL195-10                       mrs=Satisfiable  vampire=Unsatisfiable  ⚠ SOUNDNESS
  UEQ     LCL203-10                       mrs=Satisfiable  vampire=Unsatisfiable  ⚠ SOUNDNESS
  UEQ     LCL211-10                       mrs=Satisfiable  vampire=Unsatisfiable  ⚠ SOUNDNESS
  UEQ     LCL224-10                       mrs=Satisfiable  vampire=Unsatisfiable  ⚠ SOUNDNESS
  UEQ     RNG001-10                       mrs=Satisfiable  vampire=Unsatisfiable  ⚠ SOUNDNESS

POLARITY VIOLATIONS — 6 case(s) of wrong SZS polarity:
  UEQ     LCL195-10                       mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     LCL203-10                       mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     LCL211-10                       mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     LCL224-10                       mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     NUM284-10.014                   mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     RNG001-10                       mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND

hack@pve:~/mrs$ ./crates/mrs-bench/systems/vampire/bin/vampire --version
Vampire 5.0.1 (Release build, commit 1b13eaf on 2026-01-18 12:14:50 +0000)
CaDiCaL: cadical-2.1.3
Linked to Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 NOTFOUND
hack@pve:~/mrs$ TPTP=/home/hack/mrs/crates/mrs-bench/problems/casc-30 crates/mrs-bench/casc.sh --systems mrs,vampire --divisions fne,ueq
hack@pve:~/mrs$ cargo run -p mrs-bench --bin bench_report -- /home/hack/mrs/crates/mrs-bench/results/casc-30/20260526_192617/run.csv
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.03s
     Running `target/debug/bench_report /home/hack/mrs/crates/mrs-bench/results/casc-30/20260526_192617/run.csv`
CASC-30 Results — 2026-05-27 06:08  (400 problems × 2 systems)
==============================================================

Division  Problems    mrs                   vampire
                      Solved  Avg (s)      Solved  Avg (s)
------------------  --------------------  --------------------
FNE            100        34    0.494          75    6.086
UEQ            300        21   21.547         216   16.426
------------------  --------------------  --------------------
TOTAL          400        55    8.533         291   13.761

DISAGREEMENTS — 32 problem(s) where systems gave contradictory answers:
  FNE     CSR026+3                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     CSR027+3                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     CSR033+3                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     CSR034+2                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     CSR036+2                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     CSR036+3                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     CSR039+2                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     CSR040+3                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     CSR052+3                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     CSR056+3                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     CSR060+2                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     CSR061+2                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     CSR073+2                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     CSR073+3                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     CSR115+31                       mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     CSR115+6                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     CSR115+91                       mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     CSR115+98                       mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     CSR116+27                       mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     CSR116+39                       mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     CSR116+6                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     LCL642+1.010                    mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     LCL642+1.015                    mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     LCL660+1.015                    mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     MGT067+1                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     NLP262+1                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     SYN457+1                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  FNE     SYN938+1                        mrs=CounterSatisfiable  vampire=Theorem  ⚠ SOUNDNESS
  UEQ     LCL195-10                       mrs=Satisfiable  vampire=Unsatisfiable  ⚠ SOUNDNESS
  UEQ     LCL203-10                       mrs=Satisfiable  vampire=Unsatisfiable  ⚠ SOUNDNESS
  UEQ     LCL211-10                       mrs=Satisfiable  vampire=Unsatisfiable  ⚠ SOUNDNESS
  UEQ     LCL224-10                       mrs=Satisfiable  vampire=Unsatisfiable  ⚠ SOUNDNESS

POLARITY VIOLATIONS — 7 case(s) of wrong SZS polarity:
  UEQ     LCL195-10                       mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     LCL203-10                       mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     LCL211-10                       mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     LCL224-10                       mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     LCL416-10                       mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     NUM284-10.014                   mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
  UEQ     RNG001-10                       mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND

[root@mtsdev02 mrs]# TPTP=/mnt/sda1/mrs/crates/mrs-bench/problems/casc-30 crates/mrs-bench/casc.sh --systems mrs
POLARITY VIOLATIONS — 1 case(s) of wrong SZS polarity:
  EPU     MSC024-1                        mrs=Satisfiable  (expected one of ["Unsatisfiable"])  ⚠ UNSOUND
