5.3
Macs: 5.6: 9.2.2 [mach==1206] [cput==0x139] [5.6.0.20040220]
SntF
C996359885006D996360452366C1120564948430D1120564960597
S9380
5
; ============= Premises ============/x /y (Dodec(x) & Tet(y) & Larger(x, y)) ~/x (Tet(x) & @y (Cube(y) $ Smaller(x, y))); =========== = Conclusion ===========/x (Large(x) & Cube(x)) $ @x (Large(x) $ Cube(x))