
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

[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
