{"n": 4, "D": 2, "result": "UNSAT", "iterations": 1, "time": 0.0, "clauses": 135, "vars": 42, "options": {}, "solve_time": 0.0, "check": ["c formula: 42 vars, 135 clauses read (header 135)", "c lemmas checked: 1 (RAT: 0), deletions: 23 (not found: 0)", "s VERIFIED"], "check_time": 0.0, "proof_lines": 25, "verified": true, "sha256_cnf": "9be70407ce3d62d97ddc24dff2f1d7df772c607b771e7c3306fa0beb6b61dc2e", "sha256_drat": "3236e2ac9eb9f0f721edab06950aa8cafe1f76acfc6da4201ab91f52b230381d", "proof_location": "certs/"}
{"n": 5, "D": 3, "result": "UNSAT", "iterations": 2, "time": 0.0, "clauses": 588, "vars": 110, "options": {}, "solve_time": 0.0, "check": ["c formula: 110 vars, 588 clauses read (header 588)", "c lemmas checked: 14 (RAT: 0), deletions: 81 (not found: 2)", "s VERIFIED"], "check_time": 0.0, "proof_lines": 98, "verified": true, "sha256_cnf": "8ffcd63488dfd7ecc309f2b34d71e5bd6f227b0a5a338d6fd75ed5734a4a085f", "sha256_drat": "93e6dbf4a0f5758b6dbba4b4c13feae9d0399285c218f0c903e50a168c7e90fc", "proof_location": "certs/"}
{"n": 6, "D": 4, "result": "UNSAT", "iterations": 6, "time": 0.0, "clauses": 2128, "vars": 245, "options": {}, "solve_time": 0.0, "check": ["c formula: 245 vars, 2128 clauses read (header 2128)", "c lemmas checked: 108 (RAT: 0), deletions: 278 (not found: 4)", "s VERIFIED"], "check_time": 0.0, "proof_lines": 391, "verified": true, "sha256_cnf": "3e7ebf2a8120a8a43f98e6dbe551df2048f8b51a11a6aa744f1c4615591f3c8b", "sha256_drat": "6c0c294daed015679463b9c622d13ac657f3fc6da39c844321fcff1bc4a2e3e2", "proof_location": "certs/"}
{"n": 7, "D": 6, "result": "UNSAT", "iterations": 10, "time": 0.0, "clauses": 7722, "vars": 560, "options": {}, "solve_time": 0.0, "check": ["c formula: 560 vars, 7722 clauses read (header 7722)", "c lemmas checked: 823 (RAT: 0), deletions: 2519 (not found: 31)", "s VERIFIED"], "check_time": 0.0, "proof_lines": 3374, "verified": true, "sha256_cnf": "479f2325c21cd287cb6fccdbb9ebdf17b597d54b9a9f8d052a5e6fa86bad4798", "sha256_drat": "13645dd9040880b5d88567991ce74d2c9550c1e73e58975a7d4648eec7961df6", "proof_location": "certs/"}
{"n": 8, "D": 7, "result": "UNSAT", "iterations": 30, "time": 0.1, "clauses": 19811, "vars": 988, "options": {}, "solve_time": 0.1, "check": ["c formula: 988 vars, 19811 clauses read (header 19811)", "c lemmas checked: 6965 (RAT: 0), deletions: 9972 (not found: 67)", "s VERIFIED"], "check_time": 0.1, "proof_lines": 17005, "verified": true, "sha256_cnf": "6facd6b7e63fabee1eba994f8bb53b1943288b39165376a61eac5d147b26a93f", "sha256_drat": "a6fe976aad81f5813c3e9e5030672e0fed2cdcb7a2a7264f31bf99554b6adc85", "proof_location": "certs/"}
{"n": 9, "D": 8, "result": "UNSAT", "iterations": 86, "time": 1.7, "clauses": 45838, "vars": 1629, "options": {}, "solve_time": 1.8, "check": ["c formula: 1629 vars, 45838 clauses read (header 45838)", "c lemmas checked: 70764 (RAT: 0), deletions: 78246 (not found: 194)", "s VERIFIED"], "check_time": 2.1, "proof_lines": 149205, "verified": true, "sha256_cnf": "5cb516e587704136111f312ab81477c888a5d4b35cec0625aa23d7cb81db7b69", "sha256_drat": "2e0e1ed2fafd2780b67d2e74bb3ba171cbb67858a6f89bf5f6bc315d560b4ee1", "proof_location": "certs/"}
{"n": 5, "D": 3, "result": "UNSAT", "iterations": 2, "time": 0.0, "clauses": 648, "vars": 120, "options": {"orientable": true}, "solve_time": 0.0, "check": ["c formula: 120 vars, 648 clauses read (header 648)", "c lemmas checked: 14 (RAT: 0), deletions: 81 (not found: 2)", "s VERIFIED"], "check_time": 0.0, "proof_lines": 98, "verified": true, "sha256_cnf": "85b21681992c6219adb3a118dce68e4ec67ef0f69e6dfa046d13ac24289046b0", "sha256_drat": "d0a6ae5bbb39944541fe8c2c0fa718f8b0948d78a08e5e93e9d1d5a75d7267ee", "proof_location": "certs/"}
{"n": 6, "D": 4, "result": "UNSAT", "iterations": 6, "time": 0.0, "clauses": 2306, "vars": 265, "options": {"orientable": true}, "solve_time": 0.0, "check": ["c formula: 265 vars, 2306 clauses read (header 2306)", "c lemmas checked: 87 (RAT: 0), deletions: 274 (not found: 4)", "s VERIFIED"], "check_time": 0.0, "proof_lines": 366, "verified": true, "sha256_cnf": "d402227c52f409de19d5cfd03c5c22d258007a4d41be9906c401af7bbf2d209a", "sha256_drat": "7c302b13ce6dca6ecae4f02456d6ad8ee2e4602226adceb0df660aa34ff5f214", "proof_location": "certs/"}
{"n": 7, "D": 5, "result": "UNSAT", "iterations": 17, "time": 0.0, "clauses": 6883, "vars": 518, "options": {"orientable": true}, "solve_time": 0.0, "check": ["c formula: 518 vars, 6883 clauses read (header 6883)", "c lemmas checked: 691 (RAT: 0), deletions: 1638 (not found: 18)", "s VERIFIED"], "check_time": 0.0, "proof_lines": 2349, "verified": true, "sha256_cnf": "33e634bedc0805c1630aaf84d9497df04b1c9763e087d9052fa6b2b47ddc9a37", "sha256_drat": "567c8c276ce7f62a80de6430a34b31fea95847122ac9b351bf6352d08c63523b", "proof_location": "certs/"}
{"n": 8, "D": 6, "result": "UNSAT", "iterations": 48, "time": 0.1, "clauses": 17907, "vars": 924, "options": {"orientable": true}, "solve_time": 0.1, "check": ["c formula: 924 vars, 17907 clauses read (header 17907)", "c lemmas checked: 7192 (RAT: 0), deletions: 8764 (not found: 53)", "s VERIFIED"], "check_time": 0.1, "proof_lines": 16010, "verified": true, "sha256_cnf": "dc2624c908dedc4ddf4732620132d87088b8059fb10c353a4d96e73ffb0aea82", "sha256_drat": "34122877f27a8bff5d8d440fc0ce2e316de7348298d5badd406da914f7aa170b", "proof_location": "certs/"}
{"n": 9, "D": 7, "result": "UNSAT", "iterations": 122, "time": 2.0, "clauses": 41803, "vars": 1536, "options": {"orientable": true}, "solve_time": 2.1, "check": ["c formula: 1536 vars, 41803 clauses read (header 41803)", "c lemmas checked: 82267 (RAT: 0), deletions: 76281 (not found: 166)", "s VERIFIED"], "check_time": 2.5, "proof_lines": 158715, "verified": true, "sha256_cnf": "4a489bcd022b85772605cb71f4091d9d33f593b126743fbd41dda7b867844a7a", "sha256_drat": "6c41fef4b835063d2c7428dfee21c39c744dac76f9226fbd6f44759c61988974", "proof_location": "certs/"}
