CASC-J4
- 13th CASC
- 26 systems and variants
- 10 new systems
- 6 winners from CASC-J3
- 4 demonstration systems (1 intuitionistic)
- 5 "really meta"-provers
- Changes from CASC-21
- LTB division
- CNF and SAT proof/model classes cancelled
- Stricter standardization of output
- Open source licenses encouraged
- 50 2.4Ghz computers, at the University of Manchester
26 2.4MHz computers, the the University of Miami
- 710 problems
- 200 FOF - 50 FNE; 150 FEQ
- 100 FNT - 50 FNN; 50 FNQ
- 100 CNF - 15 HEQ, HNE, NNE, PEQ; 40 NEQ
- 80 SAT - 40 SNE; 40 SEQ
- 80 EPR - 40 EPT; 40 EPS
- 80 UEQ
- 150 LTB - 50 CYC; 70 MZR; 30 SMO
- 300 seconds per problem in non-LTB
240 econds per problem in LTB