Apply unknownprop_affc49913747fa11b095e9305cedbaaa950055db35b087439dc7fd718eda5a78 with
TwoRamseyGraph_3_6_17 leaving 3 subgoals.
The subproof is completed by applying unknownprop_5cece90b225888ed5e86060411031b7dea9c395004ca9e7ebb9069250f2769f8.
The subproof is completed by applying unknownprop_97757aa046fc628a1493769feaf18aac5937e0cb3d98e54a6c0796c9e5514262.
The subproof is completed by applying unknownprop_7832fff82c852baccaa662f34d87e3cb9f0f480cec52038f1287bb5f734d4ead.