Apply unknownprop_d26e0281874e3c848e67997f80ac522fccb7753bf982eb4fc97a3c179cc3f8fa 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.