5.3
Macs: 5.6: 9.2.2 [mach==1206] [cput==0x139] [5.6.0.20040220]
SntF
C999856005365D999856131112C999960247610D999960260291C1120564643701D1120564653840
S13373
4
; ========== Premise ==========@x (Dodec(x) $ Medium(x)); ========== Conclusion =========/x Large(x) $ /x ~Dodec(x)