Ramsey type theorem Let $\mathcal{P}(\{0,\dotsc,7\})$ denote the power set of $\{0,\dotsc,7\}$.
Is the following true?

For any function $f: \mathcal{P}(\{0,\dotsc,7\})\rightarrow\{0,1\}$ there exists $0\leq k\leq 3$ and three mutually disjoint sets $A,B,C\subseteq \{0,\dotsc,7\}$ such that
  $\min A = 2k, \min B = 2k+1,$ and $$f(C) = f(A\cup C) = f(B\cup C) = f(A\cup B\cup C)?$$

 A: Yes, your conjecture is true.
Suppose otherwise. Then there exists a counterexample $f : \mathcal{P}(8) \rightarrow \{0, 1\}$. For each set $X \in \mathcal{P}(8)$, let the proposition $P_X$ denote $f(X) = 1$.
There are $5440$ different choices of the tuple $(A, B, C) \in \mathcal{P}(8)^3$ satisfying your constraints. For each such tuple, we obtain two clauses which must be true of the counterexample $f$:
$$ (\neg P_C \lor \neg P_{A \cup C} \lor \neg P_{B \cup C} \lor \neg P_{A \cup B \cup C}) $$
$$ (P_C \lor P_{A \cup C} \lor P_{B \cup C} \lor P_{A \cup B \cup C}) $$
This gives a succinct list of $10880$ clauses which must be true of the $256$ primitive propositions $\{ P_X : X \in \mathcal{P}(8) \}$.
Inputting this list of clauses into the SAT solver Glucose gives the response 'UNSAT' (meaning 'unsatisfiable'), so no such counterexample exists. It also exports a verifiable certificate of unsatisfiability which can be checked in polynomial time.
The proof is somewhat unilluminating, because it doesn't give any indication as to why your conjecture is true, just that it is.
