Demonstration of the basics of delete - resoluation asymmetric tautology (DRAT) proof verification using Schur's Theorem for r=2, which I naively originally called the Boolean sum triples (BST) problem. This problem asks whether the set of numbers {1, ..., n} can be divided into two subsets where neither subset contains the entire triple (a, b, c) where a=b+c and a<b<c.

You can read my blog post that this is supporting material to here.

See also https://www.cs.utexas.edu/~marijn/ptn/#example

main.py contains the example. The output of this file is:

$ ./main.py
Brute force
3 : 1 2
        3

4 : 1 2   4
        3

5 : 1 2   4
        3   5

6 : 1 2   4
        3   5 6

7 : 1 2   4     7
        3   5 6

8 : 1 2   4       8
        3   5 6 7

9 : no solutions

10 : no solutions

Checking DRAT solution
For n=3: not UNSAT
For n=4: not UNSAT
For n=5: not UNSAT
For n=6: not UNSAT
For n=7: not UNSAT
For n=8: not UNSAT
For n=9: UNSAT
For n=10: UNSAT

bst_plain_*.cnf contain the DIMACS-encoded formulae for the BST problems from n=3 through n=10.