solver fnd ok sat uns fld dis to mo s11 s6 sig uk time space max abcsuperprove 818 732 320 412 86 0 67 0 0 0 0 19 15235 39973 2509 19 times 2 pdtrav 818 731 308 423 87 0 84 0 0 2 0 1 28841 57557 1078 1 out of memory ic3 818 713 308 405 105 0 105 0 0 0 0 0 13476 22481 511 abcdprove 818 706 303 403 112 0 59 0 0 0 0 53 14985 25359 719 53 times 2 tipind 818 689 324 365 129 0 121 0 0 0 0 8 10576 7823 266 8 times UNKNOWN (> 1000 steps) cip 818 680 325 355 138 0 138 0 0 0 0 0 15568 32163 1831 abc08 818 676 311 365 142 0 88 0 0 4 0 50 5788 33635 211 50 times 2 bipzzimc 818 676 308 368 142 0 129 0 0 4 0 9 13415 26652 1547 7 mo, 4 assert, 2 s11 bip 818 664 307 357 154 0 138 0 0 6 0 10 10638 19469 2455 10 mo, 6 assert tiplnd 818 654 281 373 164 0 164 0 0 0 0 0 11360 9822 701 mcsti 818 586 312 274 232 0 229 0 3 0 0 0 11101 15492 672 3 s11 mcaigerind 818 513 297 216 305 0 302 0 0 0 0 3 5162 4894 159 ? (3 > 1000 steps) tipbmc 818 386 325 61 432 0 220 0 0 0 0 212 2639 5362 573 212 UNKNOWN (> 1000 steps) tipbmc08 818 337 324 13 481 0 235 0 16 0 0 230 2199 4570 504 230 UNKNOWN (> 1000 steps) mbmc 818 327 320 7 491 0 447 0 5 0 0 39 3236 20367 1828 35 UNKNOWN (?), 4 mo abcbmc2 818 326 326 0 492 0 457 35 0 0 0 0 4126 17679 4254 mcaigerbmc 818 321 312 9 497 0 308 9 0 0 0 180 2831 11714 2128 ? (180 > 1000 steps) nusmvbmc 818 311 311 0 507 0 486 0 0 0 0 21 9579 38472 959 21 times > 1000 steps abcbmc3 818 299 299 0 519 0 22 5 0 0 0 492 171 5509 497 492 times 2 aigtrav 818 288 61 227 530 0 358 172 0 0 0 0 6820 102731 6034 nusmvbdd 818 265 71 194 553 0 225 328 0 0 0 0 6230 37464 6710 fnd = found log files (should be 818) ok = status ok = sat + uns sat = solved satisfiable instances uns = solved unsatisfiable instances fld = unsolved instances = dis + to + mo + s11 + s6 + sig + uk dis = discrepancies (should be 0) to = time out of 900 seconds reached mo = memory out determined as determined by 'run' s11 = segmentation fault signal catched by 'run' s6 = abort signal cached by 'run' (typically an assertion failure) sig = other signal caught by 'run' (should be 0) uk = proper exit without producing sat/unsat result time = sum of the time needed to solve the 'ok' instances space = sum of the maximum memory needed for all 'fnd' instances max = maximum memory needed over all 'ok' instances last column describes the reasons of the 'uk' column some of them should have been added to the 'mo' manually but the rest of the data is generated automatically and thus we added this last part manually