5.3
Macs: 5.6: 9.2.2 [mach==1206] [cput==0x139] [5.6.0.20040220]
SntF
C996361187057D996361553131C1120564838905D1120564851585
S9356
6
; ============ Premises ============@x @y ((Cube(x) & Tet(y)) $ SameSize(x, y))/x /y (Cube(x) & Tet(y))/x (Dodec(x) & @y (Tet(y) $ Smaller(x, y))); ============ Conclusion ============@x @y ((Dodec(x) & Cube(y)) $ Larger(y, x))