(27, 7, 4, 1, 2) f=25 sb=1 | UNSAT drat:['s VERIFIED'] cnf=18366141204cc64acd95722d25d3a701a5985f17c87111d5576cf587241cf380 drat=c14d37f82cb045a7a280cffc7fc9c4e3f87616ae9b7b7f568cfdb56a4afe2929
(27, 7, 4, 1, 2) f=23 sb=1 | UNSAT drat:['s VERIFIED'] cnf=8f1440701b5d8c277b1bf290810b1a4fcd30be2db724700c5aa5c55aaf43248a drat=180cd5f397e10fe53b869a7480b87b1b2d007b0a3535f53a22d097afeee1de93
(27, 7, 4, 1, 2) f=5 sb=1 | UNSAT drat:['s VERIFIED'] cnf=c770b66e9d8c460c7d51942bdf61ce75dfcd056bc74c3fc0d7dc79cdc9b623c9 drat=48c7ddd6b00089119fe57b0cea495b3052df97f9df4887b5abe934beadbf3b9f
(27, 7, 4, 1, 2) f=3 sb=1 | UNSAT drat:['s VERIFIED'] cnf=330fe893100d3b56853538a7cf06ea3c15c83f9336cf5a4bd95c29b5d507c111 drat=f2aa38259317d19318e46f5d5decd4769350b449d45d445ee6d9e21d92a0a317
(27, 7, 4, 1, 2) f=1 sb=1 | UNSAT drat:['s VERIFIED'] cnf=be508ad5862af38543a878781563fc679bed76610f0870a055004a51e828a891 drat=b29e44cd39dee7d749ffd7ac241b7bbc9c49207a4cb146308daa1e432a4692eb
(15, 5, 2, 1, 2) f=13 sb=1 | SAT exact_check=True sha=e09a811cd0487c96
(15, 5, 2, 1, 2) f=13 sb=3 | SAT exact_check=True sha=44b03b43aebd1555
(15, 5, 2, 1, 2) f=13 sb=0 | SAT exact_check=True sha=2f274a045e042f56
(15, 5, 2, 1, 2) f=11 sb=1 | SAT exact_check=True sha=49247fd42157dad5
(15, 5, 2, 1, 2) f=11 sb=3 | SAT exact_check=True sha=d607981748b8e706
(15, 5, 2, 1, 2) f=11 sb=0 | SAT exact_check=True sha=6886dbc1cb865a87
(15, 5, 2, 1, 2) f=9 sb=1 | UNSAT
(15, 5, 2, 1, 2) f=9 sb=3 | UNSAT
(15, 5, 2, 1, 2) f=9 sb=0 | NO_VERDICT rc=124
(15, 5, 2, 1, 2) f=7 sb=1 | UNSAT
(15, 5, 2, 1, 2) f=7 sb=3 | UNSAT
(15, 5, 2, 1, 2) f=7 sb=0 | UNSAT
(15, 5, 2, 1, 2) f=5 sb=1 | UNSAT
(15, 5, 2, 1, 2) f=5 sb=3 | UNSAT
(15, 5, 2, 1, 2) f=5 sb=0 | UNSAT
(15, 5, 2, 1, 2) f=3 sb=1 | UNSAT
(15, 5, 2, 1, 2) f=3 sb=3 | UNSAT
(15, 5, 2, 1, 2) f=3 sb=0 | UNSAT
(15, 5, 2, 1, 2) f=1 sb=1 | UNSAT
(15, 5, 2, 1, 2) f=1 sb=3 | UNSAT
(15, 5, 2, 1, 2) f=1 sb=0 | UNSAT
(14, 5, 4, 1, 2) f=14 sb=1 | UNSAT
(16, 6, 3, 1, 3) f=16 sb=1 | UNSAT
(27, 8, 4, 3, 2) f=21 sb=1 | SAT exact_check=True sha=bad49d1544b3e2e4
(27, 8, 4, 3, 2) f=21 sb=0 | SAT exact_check=True sha=6d29f2b05282df73
(27, 8, 4, 3, 2) f=19 sb=1 | SAT exact_check=True sha=b7e76a67b7f76020
(27, 8, 4, 3, 2) f=19 sb=0 | SAT exact_check=True sha=017f128f68de1a80
(27, 8, 4, 3, 2) f=17 sb=1 | SAT exact_check=True sha=a9237e7e88ee3e7c
(27, 8, 4, 3, 2) f=17 sb=0 | SAT exact_check=True sha=70f85a0bffe127e2
(27, 8, 4, 3, 2) f=15 sb=1 | SAT exact_check=True sha=92e55ee5e1b29933
(27, 8, 4, 3, 2) f=15 sb=0 | SAT exact_check=True sha=57c8acf5e8401265
(27, 8, 4, 3, 2) f=13 sb=1 | SAT exact_check=True sha=ddc7225c006ce8a0
(27, 8, 4, 3, 2) f=13 sb=0 | SAT exact_check=True sha=0c1caba7cb4f25be
(27, 8, 4, 3, 2) f=11 sb=1 | SAT exact_check=True sha=202b5bd375e8cf72
(27, 8, 4, 3, 2) f=11 sb=0 | SAT exact_check=True sha=f63d1d9d0fbf9a45
(27, 8, 4, 3, 2) f=9 sb=1 | SAT exact_check=True sha=c5f0547df6329f2a
(27, 8, 4, 3, 2) f=9 sb=0 | SAT exact_check=True sha=52a724b1ad6188d6
(27, 8, 4, 3, 2) f=7 sb=1 | SAT exact_check=True sha=91469555955c80dd
(27, 8, 4, 3, 2) f=7 sb=0 | SAT exact_check=True sha=e44d3dbdc76ab2c7
(27, 8, 4, 3, 2) f=5 sb=1 | SAT exact_check=True sha=aca6cfc046d5aba6
(27, 8, 4, 3, 2) f=5 sb=0 | SAT exact_check=True sha=70b6d4ea6c45ddc5
(27, 8, 4, 3, 2) f=3 sb=1 | SAT exact_check=True sha=db3a4777bbf0f063
(27, 8, 4, 3, 2) f=3 sb=0 | SAT exact_check=True sha=3a22f7eade8b9395
(27, 8, 4, 3, 2) f=1 sb=1 | SAT exact_check=True sha=a432e940a4486ecf
(27, 8, 4, 3, 2) f=1 sb=0 | SAT exact_check=True sha=6744447f412c295b
(27, 10, 6, 3, 4) f=21 sb=1 | NO_VERDICT rc=124
(27, 10, 6, 3, 4) f=21 sb=0 | NO_VERDICT rc=124
(27, 10, 6, 3, 4) f=19 sb=1 | NO_VERDICT rc=124
