10 7 SAT 0.0 s (7, 1, True, 1, True)
10 8 SAT 0.1 s (8, -7, False, 1, True)
10 9 UNSAT 18.6 s 
RESULT n=10 options=[] max D found=8 (D=9 UNSAT)
11 8 SAT 0.1 s (8, 1, True, 1, True)
11 9 SAT 0.2 s (9, -10, False, 2, True)
11 10 UNSAT 1582.3 s 
RESULT n=11 options=[] max D found=9 (D=10 UNSAT)
12 9 SAT 0.4 s (9, -7, False, 1, True)
12 10 SAT 5.3 s (10, -12, False, 1, True)
12 11 (run stopped by hand at 20:02Z after ~55 min without a model; the explicit chain example gives 11)
