from :
"O’Rear subsequently devised a much simpler 748-rule machine that halts if ZF is inconsistent"