The last examples we will consider are known as ``clique coloring problems.'' These are derivatives of pigeonhole problems where the exact nature of the pigeonhole problem is obscured. Somewhat more specifically, the problems indicate that a graph includes a clique of nodes (where every node in the clique is connected to every other), and that the graph must be colored in colors. If the graph itself is known to be a clique, the problem is equivalent to the pigeonhole problem. But if we know only that the clique can be embedded into the graph, the problem is more difficult.

In the axiomatization, we use to describe the edges of the
graph, to describe the coloring of the graph, and to
describe the embedding of the cli__Q__ue into the graph. The
graph has nodes, the clique is of size , and there are
colors available. So the axiomatization is:

Here means that there is an edge between graph nodes and , means that graph node is colored with the th color, and means that the th element of the clique is mapped to graph node . Thus the first axiom (13) says that two of the nodes in the graph cannot be the same color (of the colors available) if they are connected by an edge. (14) says that every graph node has a color. (15) says that every element of the clique appears in the graph, and (16) says that no two elements of the clique map to the same node in the graph. Finally, (17) says that the clique is indeed a clique - no two clique elements can map to disconnected nodes in the graph.

Since there is no polynomially sized resolution proof of the pigeonhole problem in Boolean satisfiability, there is obviously no polynomially sized proof of the clique coloring problems, either. But as we shall see, clique coloring problems can in some cases be used to distinguish among elements of the proof complexity hierarchy.