5.3
Macs: 5.6: 9.2.2 [mach==1206] [cput==0x139] [5.6.0.20040220]
SntF
C999855286896D999855452198C1120564123492D1120564150367
S8899
5
========== Premises ==========@x (Small(x) $ Cube(x))@x Dodec(x)==========Conclusion =========@x ~Small(x)