5.3
Macs: 5.6: 9.2.2 [mach==1206] [cput==0x139] [5.6.0.20040220]
SntF
C996360466560D996360945701C1120564914958D1120564927639
S9196
7
; ============== Premises =============/x (Tet(x) & @y ((Tet(y) & y # x) $ Larger(x,y)))/x /y (Tet(x) & Tet(y) & y # x)@x @y ((Tet(x) & SameCol(x, y)) $ SameSize(x, y))@x /y (SameCol(x, y) & x # y); ============= Conclusion ============= ~/x /y (Tet(x) & Tet(y) & x # y & SameCol(x, y))