t_f15_sb s VERIFIED guard: rc=0 active=12.1 paused=0.0 npause=0 peakMB=40 cnf=22ceb8447c41135743d04e5c8d9469f14121330f4107ba063c647eac1dd20c93 drat=a6ef75c4861ca3c23ba6252962a51ac11b3bff22898b195510f74fdf44a3dbd0 bytes=8899833
t_f13_sb s VERIFIED guard: rc=0 active=55.6 paused=0.0 npause=0 peakMB=95 cnf=2a21bad7e5bcb361bb0335bff64045269780fdd20f2605786da5f74a92e5b0c4 drat=610ca9398bcc813bb9a8d19361965da09d37163b623c01937772ddc6bb01c9d7 bytes=25973480
t_f21_sb3   cnf=8d6b934221c8976fe6a5d8eb3b15363857f2777d25e161a4a32df704e7343c82 drat=9c0867f5e879f0d4ef81589584825e4f1f213cc175577008faa316c37744dcf7 bytes=197496832
t_f21_sb2 s VERIFIED guard: rc=0 active=12.2 paused=0.0 npause=0 peakMB=43 cnf=b526003bfc7fe4dd08f2f8f67e752b890aba0c37c9da67b07e116044805aa3b2 drat=f77f3f82885d0b0cc14dc370e474d2886fdf95321128f329ff5430c1e5dbe6ee bytes=5868531
t_f19_sb2 s VERIFIED guard: rc=0 active=1.0 paused=0.0 npause=0 peakMB=29 cnf=ed01b3f16b3dc393d029e73921e1bc5b28b83a8d3c7abca7ce8d0acb5cba472e drat=6ef8bdf4336553e5ac5887b9f05148e8627efceda502e35756094cb588b61867 bytes=1127389
t_f17_sb2 s VERIFIED guard: rc=0 active=8.1 paused=0.0 npause=0 peakMB=39 cnf=dec0a448d37167740385f4885381617516ff002f9216f8b5823a0003b4ea952b drat=6cb06a6971d880d67700bd2b1255efa8b451539b1b35aaf0bb0b5ffb4a85f9e5 bytes=6076943
t_f15_sb2 s VERIFIED guard: rc=0 active=21.3 paused=0.0 npause=0 peakMB=41 cnf=daa1291bac50be9128062788bc2a635bd922e49d63069269c78bb92776f0c84e drat=b91f2850f5b5fa8a8d7a8531a67290da9b84c9dca85d4e8ccd036d25fc7d1b0d bytes=9947764
t_f13_sb2 s VERIFIED guard: rc=0 active=84.1 paused=35.0 npause=2 peakMB=109 cnf=5e9ea98e37402735f146ec2f3764873f150e529901a952aac22f2c3541337aa7 drat=fd017b8b27178dc6a6621ce1560de62f3530d912b613c9b2e1640978ef93d39c bytes=32273777
t_f11_sb s VERIFIED guard: rc=0 active=796.9 paused=1210.3 npause=11 peakMB=274 cnf=3fc45253a16e5bb79228f7351b997388dd819548fa15ee013572234197cc2ed4 drat=1e091ce7197f8bec3d55c919049f05788713df1437edf42dce8b4540343e5e4e bytes=190342393
t_f9_sb s VERIFIED guard: rc=0 active=497.8 paused=0.0 npause=0 peakMB=233 cnf=a4d60f549a52f1b6db59c351cdd154ce3976518272bf91b260324699b1882b49 drat=6d4243543cb7b2de69e69c095947a9f235b2c82092c93a0af4b46dd6bad463d2 bytes=107963528
A_DONE
t_f11_sb2 s VERIFIED guard: rc=0 active=883.5 paused=35.0 npause=1 peakMB=290 cnf=3e396e8ed16ab6073cd92beaa237b53b69e4bbb6de720710f7ffcd138b8eca68 drat=b37a3bf59207385cfbdf96d9e0669cca6250ed0b51d05a1979aed2b95363e3c6 bytes=201933634
e2_f21 s VERIFIED guard: rc=0 active=899.6 paused=25.0 npause=3 peakMB=313 cnf=3e34dee107aaea2f99fa92897626c4f3ed6df2de80080c31bc814f0ae9dedd54 drat=e9bf99cea4cc79dc8cfeab9ad698c676191529e97a4e20d0aa7d4e1b9fd3a668 bytes=227422158
e2_f19 s VERIFIED guard: rc=0 active=108.4 paused=0.0 npause=0 peakMB=148 cnf=87924be8ed0eb2ffd436997508de4e126a98cde07356e2df7c66b5dbd304d3d7 drat=f8c3059b46bcb268525e1fda150eb292c30239c5c0754122da0da873548f9dc7 bytes=71423206
e2_f17 s VERIFIED guard: rc=0 active=921.5 paused=15.0 npause=2 peakMB=337 cnf=bdf069c2d268e9921c13cf4008a06b49b6c99b6fdadf1f5d502eccc2949fc488 drat=52381a71d1b9abdcd98d10d97184d8ea3b83a9472c2a6dd6a10d34228d84e771 bytes=276735422
B3_DONE
e2_f15 NO_UNSAT_SKIPPED_CHECK
