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