Apply not_TwoRamseyProp_4_6_35.
Apply unknownprop_aae4e03000d6619cc34e5a66244db6980d668b70bdfc22610af1046fd13449ea with
u4,
u6,
prim4 u5,
u35 leaving 2 subgoals.
The subproof is completed by applying unknownprop_43de35cd467c6862356fb78ea399101dda669611f505b0e232165d0fae004776.
The subproof is completed by applying H0.