abc        N=645 solved=552 sat=238 unsat=314 atime=9025  stime=6117  utime=2908  amem=24704 smem=16474 umem=8229  unsolved=22  ok=574 mo=0   to=67  nn=0 s6=4  s11=0
abmc       N=645 solved=208 sat=208 unsat=0   atime=36030 stime=36030 utime=0     amem=25482 smem=25482 umem=0     unsolved=287 ok=495 mo=0   to=150 nn=0 s6=0  s11=0
aigtrav    N=645 solved=254 sat=45  unsat=209 atime=11520 stime=1034  utime=10486 amem=35824 smem=10862 umem=24962 unsolved=0   ok=254 mo=338 to=53  nn=0 s6=0  s11=0
mcaiger    N=645 solved=412 sat=226 unsat=186 atime=6063  stime=3863  utime=2200  amem=2793  smem=2250  umem=543   unsolved=0   ok=412 mo=0   to=233 nn=0 s6=0  s11=0
mcaigerbmc N=645 solved=252 sat=243 unsat=9   atime=6569  stime=6569  utime=0     amem=5985  smem=5983  umem=2     unsolved=0   ok=252 mo=115 to=278 nn=0 s6=0  s11=0
nflbmc     N=645 solved=229 sat=229 unsat=0   atime=2858  stime=2858  utime=0     amem=14550 smem=14550 umem=0     unsolved=0   ok=229 mo=282 to=134 nn=0 s6=0  s11=0
nflsmv2qbf N=645 solved=398 sat=218 unsat=180 atime=1441  stime=821   utime=620   amem=21460 smem=16494 umem=4966  unsolved=0   ok=398 mo=189 to=58  nn=0 s6=0  s11=0
nusmvbmc   N=645 solved=239 sat=239 unsat=0   atime=6904  stime=6904  utime=0     amem=7314  smem=7314  umem=0     unsolved=0   ok=239 mo=6   to=382 nn=0 s6=18 s11=0
pdtravbdd  N=645 solved=370 sat=88  unsat=282 atime=14807 stime=5710  utime=9097  amem=15299 smem=3740  umem=11559 unsolved=0   ok=370 mo=0   to=273 nn=0 s6=2  s11=0
pdtravbmc  N=645 solved=260 sat=239 unsat=21  atime=8285  stime=8217  utime=68    amem=14557 smem=13826 umem=731   unsolved=0   ok=260 mo=4   to=308 nn=0 s6=70 s11=3
pdtravcbq  N=645 solved=473 sat=178 unsat=295 atime=28544 stime=16868 utime=11676 amem=32395 smem=15646 umem=16749 unsolved=0   ok=473 mo=0   to=131 nn=0 s6=40 s11=1
pdtravitp  N=645 solved=517 sat=215 unsat=302 atime=14947 stime=6156  utime=8791  amem=36292 smem=18713 umem=17579 unsolved=0   ok=517 mo=0   to=96  nn=0 s6=32 s11=0
tipbmc     N=645 solved=256 sat=247 unsat=9   atime=2611  stime=2611  utime=0     amem=3028  smem=3028  umem=0     unsolved=202 ok=458 mo=6   to=180 nn=0 s6=0  s11=1
tipidi     N=645 solved=413 sat=110 unsat=303 atime=16868 stime=8961  utime=7907  amem=8677  smem=2713  umem=5964  unsolved=0   ok=413 mo=3   to=229 nn=0 s6=0  s11=0
tipids     N=645 solved=417 sat=110 unsat=307 atime=16340 stime=8979  utime=7361  amem=6218  smem=3003  umem=3214  unsolved=0   ok=417 mo=2   to=226 nn=0 s6=0  s11=0
tipind     N=645 solved=522 sat=226 unsat=296 atime=37461 stime=31355 utime=6106  amem=4731  smem=3268  umem=1462  unsolved=2   ok=524 mo=0   to=121 nn=0 s6=0  s11=0