// Escribe en DIMACS el principio del palomar: pigeonhole HUECOS. Hay una paloma más que huecos, cada paloma
// va en algún hueco y dos palomas no comparten hueco. Se sabe a simple vista que no tiene solución.
#include <cstdlib>
#include <iostream>

int main(int argc, char* argv[]) {
    if (argc != 2) {
        std::cerr << "uso: pigeonhole HUECOS\n";
        return 1;
    }
    const int holes = std::atoi(argv[1]);
    const int pigeons = holes + 1;
    auto variable = [&](int pigeon, int hole) { return pigeon * holes + hole + 1; };
    const int clauses = pigeons + holes * pigeons * (pigeons - 1) / 2;
    std::cout << "p cnf " << pigeons * holes << ' ' << clauses << '\n';
    for (int p = 0; p < pigeons; p++) {
        for (int h = 0; h < holes; h++) std::cout << variable(p, h) << ' ';
        std::cout << "0\n";
    }
    for (int h = 0; h < holes; h++) {
        for (int p = 0; p < pigeons; p++) {
            for (int q = p + 1; q < pigeons; q++) std::cout << -variable(p, h) << ' ' << -variable(q, h) << " 0\n";
        }
    }
}