5.3
Macs: 5.6: 9.2.2 [mach==1206] [cput==0x139] [5.6.0.20040220]
SntF
C999856557018D999857108158C999960289193D999960302872C1120564772990D1120564782129
S13224
4
: ========== Premises ==========/x (Tet(x) & @y (Cube(y) $Adjoins(y, x))): ========== Conclusion =========@x(Cube(x) $ /y (Tet(y) & Adjoins(x, y)))