5.3
Macs: 5.6: 9.2.2 [mach==1206] [cput==0x139] [5.6.0.20040220]
SntF
C999959755789D999959922604C999960302872D999960313525C1120564818628D1120564828766
S12853
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) & Smaller(x, y))