Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-fast0507.opb |
MD5SUM | 2854384016ebafb26c8bfb47f81aee87 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 324 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 63009 |
Biggest coefficient in the objective function | 2 |
Number of bits for the biggest coefficient in the objective function | 2 |
Sum of the numbers in the objective function | 122425 |
Number of bits of the sum of numbers in the objective function | 17 |
Biggest number in a constraint | 2 |
Number of bits of the biggest number in a constraint | 2 |
Biggest sum of numbers in a constraint | 122425 |
Number of bits of the biggest sum of numbers | 17 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1189.18 |
Number of variables | 63009 |
Total number of constraints | 63516 |
Number of constraints which are clauses | 507 |
Number of constraints which are cardinality constraints (but not clauses) | 63009 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 7753 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc4 THE 2005-06-09 15:51:42 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=29626 boxname=wulflinc4 idbench=1410 idsolver=21 numberseed=0 MD5SUM SOLVER: 174a32271cb3bba0a277d6d7724e60fb /oldhome/oroussel/solvers/bsolo_lpr_cuts-v2 MD5SUM BENCH: 2854384016ebafb26c8bfb47f81aee87 /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-fast0507.opb REAL COMMAND: bsolo_lpr_cuts-v2 /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-fast0507.opb IDLAUNCH: 29626 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 892548 kB Buffers: 2000 kB Cached: 119196 kB SwapCached: 864 kB Active: 35812 kB Inactive: 87428 kB HighTotal: 131008 kB HighFree: 8680 kB LowTotal: 903652 kB LowFree: 883868 kB SwapTotal: 2097136 kB SwapFree: 2095216 kB Dirty: 28 kB Writeback: 0 kB Mapped: 4924 kB Slab: 13012 kB Committed_AS: 71796 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-06-09 15:58:17 (client local time) WITH STATUS 0 IN 391.891 SECONDS stats: 29626 7 391.891 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c INFO: OSL Context initialized. #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Enforcing Stack size limit: 67108864 bytes Current StackSize limit: 67108864 bytes Raw data (loadavg): 0.92 0.95 0.90 1/54 18182 Raw data (stat): 18182 (runsolver) D 18181 21152 21151 0 -1 64 8 0 0 0 0 0 0 0 18 0 1 0 911486654 884736 94 4294967295 134512640 135332820 3221224448 3221219628 135092226 0 2147483391 7 90112 3225161850 0 0 17 0 0 0 Raw data (statm): 216 94 205 205 0 11 0 vsize: 864 [startup+10.0004 s] Raw data (loadavg): 0.93 0.96 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 4730 0 0 0 983 10 0 0 25 0 1 0 911486654 31657984 4650 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 7729 4650 1111 63 0 7666 0 vsize: 30916 [startup+20.0015 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 8895 0 0 0 1976 18 0 0 25 0 1 0 911486654 48664576 8815 4294967295 134512640 134716908 3221224560 3221222788 1077414426 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 11881 8815 1111 63 0 11818 0 vsize: 47524 [startup+30.0023 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 13097 0 0 0 2968 26 0 0 25 0 1 0 911486654 65957888 13017 4294967295 134512640 134716908 3221224560 3221222788 1077414358 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 16103 13017 1111 63 0 16040 0 vsize: 64412 [startup+40.0029 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 17333 0 0 0 3959 35 0 0 25 0 1 0 911486654 83279872 17253 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 20332 17253 1111 63 0 20269 0 vsize: 81328 [startup+50.003 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 21603 0 0 0 4953 42 0 0 25 0 1 0 911486654 100745216 21523 4294967295 134512640 134716908 3221224560 3221222788 1077414420 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 24596 21523 1111 63 0 24533 0 vsize: 98384 [startup+60.0042 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 25923 0 0 0 5945 50 0 0 25 0 1 0 911486654 118484992 25843 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 28927 25843 1111 63 0 28864 0 vsize: 115708 [startup+70.0045 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 30280 0 0 0 6939 56 0 0 25 0 1 0 911486654 136253440 30200 4294967295 134512640 134716908 3221224560 3221222788 1077414351 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 33265 30200 1111 63 0 33202 0 vsize: 133060 [startup+80.0057 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 34680 0 0 0 7932 63 0 0 25 0 1 0 911486654 154316800 34600 4294967295 134512640 134716908 3221224560 3221222788 1077414395 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 37675 34600 1111 63 0 37612 0 vsize: 150700 [startup+90.0065 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 39135 0 0 0 8924 71 0 0 25 0 1 0 911486654 172535808 39055 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 42123 39055 1111 63 0 42060 0 vsize: 168492 [startup+100.006 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 43631 0 0 0 9916 80 0 0 25 0 1 0 911486654 190898176 43551 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 46606 43551 1111 63 0 46543 0 vsize: 186424 [startup+110.007 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 48175 0 0 0 10909 87 0 0 25 0 1 0 911486654 209559552 48095 4294967295 134512640 134716908 3221224560 3221222788 1077414395 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 51162 48095 1111 63 0 51099 0 vsize: 204648 [startup+120.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 52780 0 0 0 11901 95 0 0 25 0 1 0 911486654 228519936 52700 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 55791 52700 1111 63 0 55728 0 vsize: 223164 [startup+130.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 57429 0 0 0 12893 104 0 0 25 0 1 0 911486654 247480320 57349 4294967295 134512640 134716908 3221224560 3221222788 1077414345 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 60420 57349 1111 63 0 60357 0 vsize: 241680 [startup+140.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 62157 0 0 0 13884 113 0 0 25 0 1 0 911486654 266891264 62077 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 65159 62077 1111 63 0 65096 0 vsize: 260636 [startup+150.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 66940 0 0 0 14876 121 0 0 25 0 1 0 911486654 286453760 66860 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 69935 66860 1111 63 0 69872 0 vsize: 279740 [startup+160.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 71777 0 0 0 15869 128 0 0 25 0 1 0 911486654 306307072 71697 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 74782 71697 1111 63 0 74719 0 vsize: 299128 [startup+170.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 76664 0 0 0 16861 137 0 0 25 0 1 0 911486654 326316032 76584 4294967295 134512640 134716908 3221224560 3221222788 1077414420 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 79667 76584 1111 63 0 79604 0 vsize: 318668 [startup+180.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 81616 0 0 0 17852 145 0 0 25 0 1 0 911486654 346619904 81536 4294967295 134512640 134716908 3221224560 3221222788 1077414351 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 84624 81536 1111 63 0 84561 0 vsize: 338496 [startup+190.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 86625 0 0 0 18845 153 0 0 25 0 1 0 911486654 367075328 86545 4294967295 134512640 134716908 3221224560 3221222428 1077270166 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 89618 86545 1111 63 0 89555 0 vsize: 358472 [startup+200.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 91697 0 0 0 19836 162 0 0 25 0 1 0 911486654 387825664 91617 4294967295 134512640 134716908 3221224560 3221222788 1077414351 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 94684 91617 1111 63 0 94621 0 vsize: 378736 [startup+210.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 96843 0 0 0 20827 171 0 0 25 0 1 0 911486654 408875008 96763 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 99823 96763 1111 63 0 99760 0 vsize: 399292 [startup+220.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 102080 0 0 0 21816 182 0 0 25 0 1 0 911486654 430444544 102000 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 105089 102000 1111 63 0 105026 0 vsize: 420356 [startup+230.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 107386 0 0 0 22807 192 0 0 25 0 1 0 911486654 452247552 107306 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 110412 107306 1111 63 0 110349 0 vsize: 441648 [startup+240.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 112789 0 0 0 23797 202 0 0 25 0 1 0 911486654 474345472 112709 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 115807 112709 1111 63 0 115744 0 vsize: 463228 [startup+250.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 118276 0 0 0 24787 211 0 0 25 0 1 0 911486654 496738304 118196 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 121274 118196 1111 63 0 121211 0 vsize: 485096 [startup+260.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 123971 0 0 0 25778 221 0 0 25 0 1 0 911486654 520179712 123891 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 126997 123891 1111 63 0 126934 0 vsize: 507988 [startup+270.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 129829 0 0 0 26769 230 0 0 25 0 1 0 911486654 544067584 129749 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 132829 129749 1111 63 0 132766 0 vsize: 531316 [startup+280.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 135882 0 0 0 27759 240 0 0 25 0 1 0 911486654 568852480 135802 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 138880 135802 1111 63 0 138817 0 vsize: 555520 [startup+290.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 142184 0 0 0 28747 252 0 0 25 0 1 0 911486654 594681856 142104 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 145186 142104 1111 63 0 145123 0 vsize: 580744 [startup+300.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 148815 0 0 0 29736 264 0 0 25 0 1 0 911486654 621850624 148735 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 151819 148735 1111 63 0 151756 0 vsize: 607276 [startup+310.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 155766 0 0 0 30723 277 0 0 25 0 1 0 911486654 650371072 155686 4294967295 134512640 134716908 3221224560 3221222788 1077414426 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 158782 155686 1111 63 0 158719 0 vsize: 635128 [startup+320.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 163155 0 0 0 31710 290 0 0 25 0 1 0 911486654 680529920 163075 4294967295 134512640 134716908 3221224560 3221222788 1077414385 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 166145 163075 1111 63 0 166082 0 vsize: 664580 [startup+330.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 171209 0 0 0 32697 303 0 0 25 0 1 0 911486654 713527296 171129 4294967295 134512640 134716908 3221224560 3221222912 134567410 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 174201 171129 1111 63 0 174138 0 vsize: 696804 [startup+340.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 179534 0 0 0 33684 317 0 0 25 0 1 0 911486654 747569152 179454 4294967295 134512640 134716908 3221224560 3221222788 1077414358 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 182512 179454 1111 63 0 182449 0 vsize: 730048 [startup+350.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 188376 0 0 0 34668 332 0 0 25 0 1 0 911486654 783851520 188296 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 191370 188296 1111 63 0 191307 0 vsize: 765480 [startup+360.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 197414 0 0 0 35653 348 0 0 25 0 1 0 911486654 821088256 197334 4294967295 134512640 134716908 3221224560 3221222788 1077414410 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 200461 197334 1111 63 0 200398 0 vsize: 801844 [startup+370.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 206657 0 0 0 36637 364 0 0 25 0 1 0 911486654 859013120 206577 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 209720 206577 1111 63 0 209657 0 vsize: 838880 [startup+380.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) R 18181 21152 21151 0 -1 0 216284 0 0 0 37622 379 0 0 25 0 1 0 911486654 898433024 216204 4294967295 134512640 134716908 3221224560 3221223216 134527946 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 219344 216204 1111 63 0 219281 0 vsize: 877376 [startup+390.018 s] Raw data (loadavg): 1.07 0.99 0.91 1/54 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) D 18181 21152 21151 0 -1 0 225724 0 26 0 38562 402 0 0 18 0 1 0 911486654 936656896 218526 4294967295 134512640 134716908 3221224560 3221222892 1077399560 0 0 7 0 3222515881 0 0 17 0 0 0 Raw data (statm): 228676 218526 1111 63 0 228613 0 vsize: 914704 [startup+394.817 s] Raw data (loadavg): 1.07 0.99 0.91 1/53 18182 Raw data (stat): 18182 (bsolo_lpr_cuts-) D 18181 21152 21151 0 -1 0 225724 0 26 0 38562 402 0 0 18 0 1 0 911486654 936656896 218526 4294967295 134512640 134716908 3221224560 3221222892 1077399560 0 0 7 0 3222515881 0 0 17 0 0 0 Raw data (statm): 228676 218526 1111 63 0 228613 0 vsize: 0 Child ended because it received signal 6 (SIGABRT) Real time (s): 394.816 CPU time (s): 391.891 CPU user time (s): 387.416 CPU system time (s): 4.47532 CPU usage (%): 99.2592 Max. virtual memory (Kb): 914704 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####