5.3
Macs: 5.6: 9.2.2 [mach==1206] [cput==0x139] [5.6.0.20040220]
SntF
C996358984014D996359854076C1120565471182D1120565483348
S9452
10
Cube(a) & Tet(b) & Tet(c) & b # c ~@x (Tet(x) $ (x = b | x = c))@x (Tet(x) $ /y (Dodec(y) & Adjoins(y, x))) ~/x /y (Cube(x) & Dodec(y) & SameCol(x, y))/x /y (Cube(x) & Cube(y) & x # y & ~/z (Cube(z) & z # x & z # y))@x @y (~(Tet(x) & Tet(y)) | SameSize(x, y))@x @y ((Cube(x) & Tet(y)) $ Larger(x, y))@x (Cube(x) $ /y /z (Dodec(y) & Dodec(z) & Between(x, y, z)))@x@y((Cube(x) & Cube(y) & x # y) $ ~SameSize(x,y))/x(Dodec(x) & @y((Dodec(y) & y # x) $ Larger(x, y)))