Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-p0040.opb |
MD5SUM | 1c249519911563f3292efb34f4875b44 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 62027 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 40 |
Biggest coefficient in the objective function | 8161 |
Number of bits for the biggest coefficient in the objective function | 13 |
Sum of the numbers in the objective function | 265332 |
Number of bits of the sum of numbers in the objective function | 19 |
Biggest number in a constraint | 8161 |
Number of bits of the biggest number in a constraint | 13 |
Biggest sum of numbers in a constraint | 265332 |
Number of bits of the biggest sum of numbers | 19 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 0.276957 |
Number of variables | 40 |
Total number of constraints | 63 |
Number of constraints which are clauses | 10 |
Number of constraints which are cardinality constraints (but not clauses) | 50 |
Number of constraints which are nor clauses,nor cardinality constraints | 3 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 10 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc21 THE 2005-04-22 02:09:35 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=12115 boxname=wulflinc21 idbench=932 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 1c249519911563f3292efb34f4875b44 /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-p0040.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-p0040.opb /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-p0040.opb IDLAUNCH: 12115 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 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 : 3 cpu MHz : 451.161 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: 820740 kB Buffers: 1376 kB Cached: 192920 kB SwapCached: 1408 kB Active: 37996 kB Inactive: 158544 kB HighTotal: 131008 kB HighFree: 48188 kB LowTotal: 903652 kB LowFree: 772552 kB SwapTotal: 2097892 kB SwapFree: 2095700 kB Dirty: 48 kB Writeback: 0 kB Mapped: 4888 kB Slab: 11780 kB Committed_AS: 63796 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-22 02:10:12 (client local time) WITH STATUS 30 IN 36.3245 SECONDS stats: 12115 0 36.3245 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 23 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ########## c -- Clauses(.)/Splits(s): . c ---[ 21]---> BDD-cost: 5 c ---[ 19]---> BDD-cost: 5 c ---[ 17]---> BDD-cost: 5 c ---[ 15]---> BDD-cost: 5 c ---[ 13]---> BDD-cost: 5 c ---[ 11]---> BDD-cost: 5 c ---[ 9]---> BDD-cost: 5 c ---[ 7]---> BDD-cost: 5 c ---[ 5]---> BDD-cost: 5 c ---[ 3]---> BDD-cost: 5 c ---[ 2]---> BDD-cost: 17 c ---[ 1]---> BDD-cost: 16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 186 521 | 62 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 66539[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7884 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 19547 45827 | 6515 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 65737[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19 | 19777 46482 | 6592 16 536 33.5 | 0.000 % | c | 119 | 19528 45919 | 7251 101 1221 12.1 | 1.637 % | c ============================================================================== c [1mFound solution: 65380[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 170 | 19431 45784 | 6477 142 1778 12.5 | 1.637 % | c ============================================================================== c [1mFound solution: 65203[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 172 | 19449 45882 | 6483 144 1793 12.5 | 1.637 % | c ============================================================================== c [1mFound solution: 65108[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 173 | 19460 45907 | 6486 145 1796 12.4 | 1.637 % | c ============================================================================== c [1mFound solution: 64519[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 191 | 19550 46137 | 6516 163 3580 22.0 | 1.637 % | c | 291 | 19520 46069 | 7167 260 8533 32.8 | 3.079 % | c | 444 | 19432 45878 | 7884 335 8986 26.8 | 3.489 % | c | 669 | 19432 45878 | 8672 560 19185 34.3 | 3.489 % | c | 1009 | 19432 45878 | 9540 900 29806 33.1 | 3.489 % | c | 1516 | 19432 45878 | 10494 1407 48112 34.2 | 3.489 % | c | 2276 | 19420 45851 | 11543 2166 72597 33.5 | 3.530 % | c ============================================================================== c [1mFound solution: 64214[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3130 | 19437 45912 | 6479 3020 106884 35.4 | 3.530 % | c ============================================================================== c [1mFound solution: 64158[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3224 | 19424 45890 | 6474 3112 110084 35.4 | 3.530 % | c | 3325 | 19424 45890 | 7121 3213 112436 35.0 | 3.860 % | c | 3475 | 19424 45890 | 7833 3363 115645 34.4 | 3.860 % | c | 3701 | 19424 45890 | 8616 3589 121232 33.8 | 3.860 % | c ============================================================================== c [1mFound solution: 64135[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3966 | 19434 45912 | 6478 3854 131240 34.1 | 3.860 % | c | 4067 | 19352 45726 | 7125 3954 135460 34.3 | 4.198 % | c | 4217 | 19352 45726 | 7838 4104 141535 34.5 | 4.198 % | c ============================================================================== c [1mFound solution: 64003[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4272 | 19433 45929 | 6477 4159 144001 34.6 | 4.198 % | c | 4373 | 19433 45929 | 7124 4260 147968 34.7 | 4.209 % | c | 4523 | 19433 45929 | 7837 4410 150540 34.1 | 4.209 % | c | 4751 | 19433 45929 | 8620 4638 154035 33.2 | 4.209 % | c | 5088 | 19209 45415 | 9482 4972 158178 31.8 | 5.032 % | c | 5594 | 19209 45415 | 10431 5478 171051 31.2 | 5.032 % | c ============================================================================== c [1mFound solution: 63972[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6285 | 19188 45380 | 6396 6168 195709 31.7 | 5.032 % | c | 6387 | 19188 45380 | 7035 6270 198254 31.6 | 5.174 % | c | 6538 | 19188 45380 | 7739 6421 204483 31.8 | 5.174 % | c ============================================================================== c [1mFound solution: 63747[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6676 | 19202 45413 | 6400 6559 210550 32.1 | 5.174 % | c | 6777 | 19202 45413 | 7040 6660 212224 31.9 | 5.181 % | c | 6927 | 19198 45405 | 7744 6807 215854 31.7 | 5.208 % | c | 7152 | 19198 45405 | 8518 7032 224568 31.9 | 5.208 % | c ============================================================================== c [1mFound solution: 63485[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7309 | 19200 45411 | 6400 7177 230480 32.1 | 5.208 % | c | 7410 | 19200 45411 | 7040 3690 92122 25.0 | 5.258 % | c | 7560 | 19200 45411 | 7744 3840 97081 25.3 | 5.259 % | c | 7785 | 19200 45411 | 8518 4065 104678 25.8 | 5.259 % | c | 8122 | 19200 45411 | 9370 4402 114208 25.9 | 5.259 % | c | 8629 | 19200 45411 | 10307 4909 129858 26.5 | 5.259 % | c ============================================================================== c [1mFound solution: 63469[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9339 | 19208 45429 | 6402 5619 150031 26.7 | 5.259 % | c | 9441 | 19208 45429 | 7042 5721 156236 27.3 | 5.269 % | c | 9591 | 19208 45429 | 7746 5871 160687 27.4 | 5.269 % | c | 9817 | 19208 45429 | 8521 6097 167454 27.5 | 5.269 % | c | 10154 | 19208 45429 | 9373 6434 176638 27.5 | 5.269 % | c | 10660 | 19208 45429 | 10310 6940 189839 27.4 | 5.269 % | c ============================================================================== c [1mFound solution: 63444[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10890 | 19153 45305 | 6384 7166 198758 27.7 | 5.269 % | c | 10990 | 19153 45305 | 7022 3683 83383 22.6 | 5.545 % | c | 11140 | 19026 45010 | 7724 3828 85245 22.3 | 6.055 % | c ============================================================================== c [1mFound solution: 62690[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11198 | 19087 45156 | 6362 3886 86134 22.2 | 6.055 % | c | 11299 | 19087 45156 | 6998 3987 87540 22.0 | 6.078 % | c ============================================================================== c [1mFound solution: 62215[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11310 | 19102 45200 | 6367 3998 87816 22.0 | 6.078 % | c | 11410 | 19102 45200 | 7003 4098 90516 22.1 | 6.084 % | c | 11561 | 19102 45200 | 7704 4249 93807 22.1 | 6.084 % | c | 11788 | 19102 45200 | 8474 4476 97844 21.9 | 6.084 % | c | 12126 | 19102 45200 | 9321 4814 105320 21.9 | 6.083 % | c | 12632 | 19093 45181 | 10254 5319 118427 22.3 | 6.150 % | c | 13394 | 19093 45181 | 11279 6081 133889 22.0 | 6.150 % | c | 14533 | 19093 45181 | 12407 7220 161123 22.3 | 6.152 % | c ============================================================================== c [1mFound solution: 62191[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15008 | 19101 45199 | 6367 7689 171924 22.4 | 6.152 % | c | 15108 | 19101 45199 | 7003 3945 74220 18.8 | 6.198 % | c | 15258 | 19003 44977 | 7704 4091 78834 19.3 | 6.558 % | c | 15484 | 19003 44977 | 8474 4317 84306 19.5 | 6.558 % | c | 15822 | 19003 44977 | 9321 4655 92114 19.8 | 6.558 % | c ============================================================================== c [1mFound solution: 62180[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16282 | 19011 44998 | 6337 5115 103759 20.3 | 6.558 % | c | 16382 | 19011 44998 | 6970 5215 105949 20.3 | 6.567 % | c | 16532 | 19011 44998 | 7667 5365 108330 20.2 | 6.568 % | c | 16759 | 19011 44998 | 8434 5592 112725 20.2 | 6.568 % | c | 17097 | 19011 44998 | 9278 5930 121051 20.4 | 6.567 % | c ============================================================================== c [1mFound solution: 62159[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17223 | 18987 44943 | 6329 6054 123329 20.4 | 6.567 % | c ============================================================================== c [1mFound solution: 62156[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17235 | 18998 44970 | 6332 6066 123601 20.4 | 6.567 % | c ============================================================================== c [1mFound solution: 62119[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17243 | 19009 44996 | 6336 6074 123696 20.4 | 6.567 % | c | 17343 | 19009 44996 | 6969 6174 126980 20.6 | 6.735 % | c | 17494 | 19009 44996 | 7666 6325 132499 20.9 | 6.735 % | c ============================================================================== c [1mFound solution: 62104[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17710 | 19017 45015 | 6339 6541 139664 21.4 | 6.735 % | c ============================================================================== c [1mFound solution: 62027[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17723 | 19023 45029 | 6341 6554 139846 21.3 | 6.735 % | c | 17825 | 19023 45029 | 6975 6656 141781 21.3 | 6.754 % | c | 17975 | 19023 45029 | 7672 6806 146493 21.5 | 6.754 % | c | 18201 | 19023 45029 | 8439 7032 152199 21.6 | 6.753 % | c ============================================================================== c [1mOptimal solution: 62027[0m s OPTIMUM FOUND v -C1001_bit0 C1002_bit0 -C1003_bit0 -C1004_bit0 -C1005_bit0 C1006_bit0 -C1007_bit0 -C1008_bit0 C1009_bit0 -C1010_bit0 -C1011_bit0 -C1012_bit0 -C1013_bit0 -C1014_bit0 C1015_bit0 -C1016_bit0 -C1017_bit0 C1018_bit0 -C1019_bit0 -C1020_bit0 -C1021_bit0 C1022_bit0 -C1023_bit0 -C1024_bit0 -C1025_bit0 C1026_bit0 -C1027_bit0 -C1028_bit0 C1029_bit0 -C1030_bit0 -C1031_bit0 -C1032_bit0 -C1033_bit0 C1034_bit0 -C1035_bit0 -C1036_bit0 -C1037_bit0 C1038_bit0 -C1039_bit0 -C1040_bit0 c _______________________________________________________________________________ c c restarts : 80 c conflicts : 18521 (510 /sec) c decisions : 40216 (1108 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 36.2825 s c _______________________________________________________________________________ #### 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 Raw data (loadavg): 0.85 0.97 0.92 2/55 25845 Raw data (stat): 25845 (runsolver) R 25844 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 427272276 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0006 s] Raw data (loadavg): 0.87 0.97 0.92 2/55 25845 Raw data (stat): 25845 (minisat+) R 25844 30927 30926 0 -1 0 1095 0 0 0 996 2 0 0 25 0 1 0 427272276 6045696 1072 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1476 1072 603 41 0 1435 0 vsize: 5904 [startup+20.0013 s] Raw data (loadavg): 0.89 0.97 0.92 2/55 25845 Raw data (stat): 25845 (minisat+) R 25844 30927 30926 0 -1 0 1200 0 0 0 1996 2 0 0 25 0 1 0 427272276 6451200 1177 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1575 1177 603 41 0 1534 0 vsize: 6300 [startup+30.0014 s] Raw data (loadavg): 0.91 0.97 0.92 2/55 25845 Raw data (stat): 25845 (minisat+) R 25844 30927 30926 0 -1 0 1206 0 0 0 2996 3 0 0 25 0 1 0 427272276 6586368 1183 4294967295 134512640 134672761 3221224544 3221223552 1075349698 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1608 1183 603 41 0 1567 0 vsize: 6432 [startup+36.3281 s] Raw data (loadavg): 0.91 0.97 0.92 1/54 25845 Raw data (stat): 25845 (minisat+) R 25844 30927 30926 0 -1 0 1206 0 0 0 2996 3 0 0 25 0 1 0 427272276 6586368 1183 4294967295 134512640 134672761 3221224544 3221223552 1075349698 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1608 1183 603 41 0 1567 0 vsize: 0 Child status: 30 Real time (s): 36.3278 CPU time (s): 36.3245 CPU user time (s): 36.2865 CPU system time (s): 0.037994 CPU usage (%): 99.9909 Max. virtual memory (Kb): 6432 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 62027 #### END VERIFIER DATA ####