Results Single Property Track HWMCC'11 ====================================== SAT+UNSAT ranking (1st column per group, 2nd column per solver) ------------------------+-----+------------------------------------------------------------ solver fnd | ok | sat uns fld dis to mo s11 s6 sig uk real time space max | | SAT+UNS | | A 1 suprove 465 | 395 | 83 312 70 0 70 0 0 0 0 0 15381 30904 95051 3406 2 simprove 465 | 383 | 87 296 82 0 82 0 0 0 0 0 10697 35204 93851 3299 3 simbip 465 | 381 | 90 291 84 0 84 0 0 0 0 0 12234 40909 83738 3074 B 4 pdthrd 465 | 377 | 81 296 88 0 74 0 5 9 0 0 19903 51735 102283 3219 5 pdtexpt 465 | 349 | 68 281 116 0 106 0 0 10 0 0 23195 23051 34945 884 C 6 iimc 465 | 341 | 75 266 124 0 124 0 0 0 0 0 26540 26334 74975 4411 7 abcsuperprove* 465 | 332 | 75 257 133 0 106 0 0 0 0 27 17412 14089 23438 1361 8 tip 465 | 331 | 76 255 134 0 134 0 0 0 0 0 9072 8986 4619 164 9 pdtrav* 465 | 319 | 61 258 146 0 142 0 0 3 0 1 25321 25141 36538 1078 10 ic3* 465 | 303 | 58 245 162 0 162 0 0 0 0 0 14377 14224 10783 497 11 tarmo 465 | 175 | 71 104 290 0 287 3 0 0 0 0 6216 24312 33269 2318 12 blimc 465 | 95 | 87 8 370 0 369 0 0 1 0 0 7014 6945 9383 1231 13 tipbmc 465 | 84 | 84 0 381 0 296 44 0 0 0 41 2981 2946 5579 581 14 abcbmc2* 465 | 83 | 83 0 382 0 354 28 0 0 0 0 4265 4230 9760 1009 15 tarmobmc 465 | 74 | 74 0 391 0 311 80 0 0 0 0 2442 9532 20944 1972 16 aigbmc 465 | 67 | 67 0 398 0 344 54 0 0 0 0 2870 2839 8362 1255 +-----+ abcsuperprove* winner HWMCC'10 SAT+UNSAT SAT ranking (1st column per group, 2nd column per solver) ----------------------------+-----+-------------------------------------------------------- solver fnd ok | SAT | uns fld dis to mo s11 s6 sig uk real time space max | | A 1 simbip 465 381 | 90 | 291 84 0 84 0 0 0 0 0 4267 13490 32419 2366 2 simprove 465 383 | 87 | 296 82 0 82 0 0 0 0 0 3546 11224 35996 3299 B 3 blimc 465 95 | 87 | 8 370 0 369 0 0 1 0 0 7012 6944 9376 1231 C 4 tipbmc 465 84 | 84 | 0 381 0 296 44 0 0 0 41 2981 2946 5579 581 5 suprove 465 395 | 83 | 312 70 0 70 0 0 0 0 0 1943 5101 28922 3298 6 abcbmc2* 465 83 | 83 | 0 382 0 354 28 0 0 0 0 4265 4230 9760 1009 7 pdthrd 465 377 | 81 | 296 88 0 74 0 5 9 0 0 6922 15208 28533 1233 8 tip 465 331 | 76 | 255 134 0 134 0 0 0 0 0 2120 2097 936 68 9 iimc 465 341 | 75 | 266 124 0 124 0 0 0 0 0 2621 2603 8976 2028 10 abcsuperprove* 465 332 | 75 | 257 133 0 106 0 0 0 0 27 6728 5880 8727 1361 11 tarmobmc 465 74 | 74 | 0 391 0 311 80 0 0 0 0 2442 9532 20944 1972 12 tarmo 465 175 | 71 | 104 290 0 287 3 0 0 0 0 3527 13825 20851 2318 13 pdtexpt 465 349 | 68 | 281 116 0 106 0 0 10 0 0 4413 4389 9402 884 14 aigbmc 465 67 | 67 | 0 398 0 344 54 0 0 0 0 2870 2839 8362 1255 15 pdtrav* 465 319 | 61 | 258 146 0 142 0 0 3 0 1 4796 4761 8491 1078 16 ic3* 465 303 | 58 | 245 162 0 162 0 0 0 0 0 5169 5141 2019 159 +-----+ abcbmc2* winner HWMCC'10 SAT UNSAT ranking (1st column per group, 2nd column per solver) --------------------------------+-----+---------------------------------------------------- solver fnd ok sat | UNS | fld dis to mo s11 s6 sig uk real time space max | | A 1 suprove 465 395 83 | 312 | 70 0 70 0 0 0 0 0 13438 25803 66129 3406 2 simprove 465 383 87 | 296 | 82 0 82 0 0 0 0 0 7151 23980 57856 3266 B 3 pdthrd 465 377 81 | 296 | 88 0 74 0 5 9 0 0 12981 36527 73750 3219 4 simbip 465 381 90 | 291 | 84 0 84 0 0 0 0 0 7967 27419 51319 3074 5 pdtexpt 465 349 68 | 281 | 116 0 106 0 0 10 0 0 18782 18662 25543 779 C 6 iimc 465 341 75 | 266 | 124 0 124 0 0 0 0 0 23919 23731 65999 4411 7 pdtrav* 465 319 61 | 258 | 146 0 142 0 0 3 0 1 20525 20380 28047 1065 8 abcsuperprove* 465 332 75 | 257 | 133 0 106 0 0 0 0 27 10684 8209 14711 652 9 tip 465 331 76 | 255 | 134 0 134 0 0 0 0 0 6952 6889 3683 164 10 ic3* 465 303 58 | 245 | 162 0 162 0 0 0 0 0 9209 9083 8763 497 11 tarmo 465 175 71 | 104 | 290 0 287 3 0 0 0 0 2689 10486 12419 1186 12 blimc 465 95 87 | 8 | 370 0 369 0 0 1 0 0 2 1 7 4 13 tipbmc 465 84 84 | 0 | 381 0 296 44 0 0 0 41 0 0 0 0 14 aigbmc 465 67 67 | 0 | 398 0 344 54 0 0 0 0 0 0 0 0 15 tarmobmc 465 74 74 | 0 | 391 0 311 80 0 0 0 0 0 0 0 0 16 abcbmc2* 465 83 83 | 0 | 382 0 354 28 0 0 0 0 0 0 0 0 +-----+ pdtrav* winner HWMCC'10 UNSAT -------------------------------------------------------------------------------------------- fnd = found log files ok = ok result = sat + uns sat = #sat uns = #unsat fld = remaining = fnd - ok dis = discrepancies to = time outs mo = memory outs s11 = signal 11 = segementation faults s6 = signal 6 = assertion failure / abort sig = othe signal uk = unknow result (bound k=100000 reached) real = real time = wall clock time time = process time space = sum of max memory for all runs max = maximum memory among all runs resources (real,time,space,max) restricted to sat+unsat,sat, resp. unsat benchmarks --------------------------------------------------------------------------------------- ic3* = another last year entrant from HWMCC'10