5.3
Macs: 5.6: 9.2.2 [mach==1206] [cput==0x139] [5.6.0.20040220]
SntF
C995734626708D995734740289C1120509496625D1120509507278C1120563837527D1120563856291
S13408
2
 ~(Large(a) | Tet(a)) ~Large(a) | ~Tet(a)