from:
https://www.quantamagazine.org/how-the-slowest-computer-programs-illuminate-maths-fundamental-limits-20201210/:
"O’Rear subsequently devised a much simpler 748-rule machine that halts if ZF is inconsistent"