5.3
Macs: 5.6: 9.2.2 [mach==1206] [cput==0x139] [5.6.0.20040220]
SntF
C999855132761D999855282841C999960265860D999960273970C1120564665007D1120564677173
S12908
6
; ========== Premises ==========@x (Small(x) | Large(x))@x (Small(x) % Tet(x))@x (Dodec(x) | ~Large(x)); ========== Conclusion =========@x (Tet(x) | Dodec(x))