5.3
Macs: 5.6: 9.2.2 [mach==1206] [cput==0x139] [5.6.0.20040220]
SntF
C998478831770D998479105569C1120564181297D1120564197518
S9331
4
; ========== Premise ========@x Dodec(x) $ @x Small(x); ========== Conclusion ==========@x (Dodec(x) $ Small(x))