PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/een/normalized-l152lav.opb
MD5SUM	7ef542195551d721d26b015e392d6d4b
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	1989
Biggest coefficient in the objective function	268
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	382524
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	1961
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	382524
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.237962
Number of variables	1989
Total number of constraints	193
Number of constraints which are clauses	95
Number of constraints which are cardinality constraints (but not clauses)	97
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	3
Maximum length of a constraint	1989
Trace number 7126

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-14 21:36:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5225 boxname=wulflinc15 idbench=402 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7ef542195551d721d26b015e392d6d4b  /oldhome/oroussel/tmp/wulflinc15/normalized-l152lav.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc15/normalized-l152lav.opb /oldhome/oroussel/tmp/wulflinc15/normalized-l152lav.opb
IDLAUNCH: 5225
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        849296 kB
Buffers:         37176 kB
Cached:         125852 kB
SwapCached:       2144 kB
Active:          73584 kB
Inactive:        94440 kB
HighTotal:      131008 kB
HighFree:         1708 kB
LowTotal:       903652 kB
LowFree:        847588 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11712 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 21:41:46 (client local time) WITH STATUS 30 IN 304.907 SECONDS
stats: 5225 0 304.907 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 193 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ==========================================================================================
c   -- Clauses(.)/Splits(s): ......
c ---[ 191]---> BDD-cost:    3
c ---[ 189]---> BDD-cost:    7
c ---[ 187]---> BDD-cost:   17
c ---[ 185]---> BDD-cost:   21
c ---[ 183]---> BDD-cost:   35
c ---[ 181]---> BDD-cost:   39
c ---[ 179]---> BDD-cost:   41
c ---[ 177]---> BDD-cost:   45
c ---[ 175]---> BDD-cost:   49
c ---[ 173]---> BDD-cost:   51
c ---[ 171]---> BDD-cost:   59
c ---[ 170]---> BDD-cost:   59
c ---[ 167]---> BDD-cost:   61
c ---[ 165]---> BDD-cost:   61
c ---[ 163]---> BDD-cost:   63
c ---[ 161]---> BDD-cost:   67
c ---[ 159]---> BDD-cost:   71
c ---[ 157]---> BDD-cost:   71
c ---[ 155]---> BDD-cost:   71
c ---[ 153]---> BDD-cost:   77
c ---[ 151]---> BDD-cost:   81
c ---[ 148]---> BDD-cost:   81
c ---[ 147]---> BDD-cost:   81
c ---[ 145]---> BDD-cost:   83
c ---[ 143]---> BDD-cost:   85
c ---[ 141]---> BDD-cost:   85
c ---[ 139]---> BDD-cost:   85
c ---[ 137]---> BDD-cost:   87
c ---[ 135]---> BDD-cost:   89
c ---[ 133]---> BDD-cost:   91
c ---[ 131]---> BDD-cost:   93
c ---[ 129]---> BDD-cost:   91
c ---[ 127]---> BDD-cost:   93
c ---[ 125]---> BDD-cost:   95
c ---[ 123]---> BDD-cost:   97
c ---[ 120]---> BDD-cost:  101
c ---[ 119]---> BDD-cost:  101
c ---[ 117]---> BDD-cost:  103
c ---[ 115]---> BDD-cost:  105
c ---[ 113]---> BDD-cost:  109
c ---[ 111]---> BDD-cost:  109
c ---[ 109]---> BDD-cost:  113
c ---[ 107]---> BDD-cost:  117
c ---[ 105]---> BDD-cost:  121
c ---[ 103]---> BDD-cost:  121
c ---[ 101]---> BDD-cost:  129
c ---[  99]---> BDD-cost:  133
c ---[  97]---> BDD-cost:  133
c ---[  95]---> BDD-cost:  133
c ---[  93]---> BDD-cost:  143
c ---[  91]---> BDD-cost:  145
c ---[  89]---> BDD-cost:  147
c ---[  87]---> BDD-cost:  147
c ---[  85]---> BDD-cost:  147
c ---[  83]---> BDD-cost:  149
c ---[  81]---> BDD-cost:  151
c ---[  79]---> BDD-cost:  151
c ---[  77]---> BDD-cost:  153
c ---[  75]---> BDD-cost:  155
c ---[  73]---> BDD-cost:  149
c ---[  71]---> BDD-cost:  171
c ---[  69]---> BDD-cost:  173
c ---[  67]---> BDD-cost:  171
c ---[  65]---> BDD-cost:  179
c ---[  63]---> BDD-cost:  181
c ---[  61]---> BDD-cost:  179
c ---[  59]---> BDD-cost:  183
c ---[  57]---> BDD-cost:  181
c ---[  55]---> BDD-cost:  189
c ---[  53]---> BDD-cost:  189
c ---[  52]---> BDD-cost:  189
c ---[  49]---> BDD-cost:  191
c ---[  47]---> BDD-cost:  201
c ---[  45]---> BDD-cost:  201
c ---[  43]---> BDD-cost:  203
c ---[  41]---> BDD-cost:  205
c ---[  39]---> BDD-cost:  209
c ---[  37]---> BDD-cost:  213
c ---[  35]---> BDD-cost:  213
c ---[  33]---> BDD-cost:  211
c ---[  31]---> BDD-cost:  221
c ---[  29]---> BDD-cost:  225
c ---[  27]---> BDD-cost:  231
c ---[  25]---> BDD-cost:  239
c ---[  23]---> BDD-cost:  231
c ---[  21]---> BDD-cost:  235
c ---[  19]---> BDD-cost:  235
c ---[  17]---> BDD-cost:  253
c ---[  15]---> BDD-cost:  255
c ---[  13]---> BDD-cost:  271
c ---[  11]---> BDD-cost:  301
c ---[   9]---> BDD-cost:  317
c ---[   7]---> BDD-cost:  323
c ---[   5]---> BDD-cost:  339
c ---[   3]---> BDD-cost:  433
c ---[   2]---> BDD-cost:75537
c ---[   0]---> BDD-cost:56866
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  412580  1190079 |  137526       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 3544[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:715161     Base: 2 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        24 | 2251580  5483636 |  750526      24     1142    47.6 |  0.000 % |
c |       125 | 2251143  5482650 |  825578     119     3477    29.2 |  0.026 % |
c |       277 | 2251143  5482650 |  908136     271     4279    15.8 |  0.026 % |
c |       502 | 2251143  5482650 |  998950     496     7176    14.5 |  0.026 % |
c |       839 | 2250598  5481419 | 1098845     831    10626    12.8 |  0.058 % |
c ==============================================================================
c [1mFound solution: 1741[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       970 | 2246629  5474072 |  748876     841    17335    20.6 |  0.058 % |
c |      1070 | 2246629  5474072 |  823763     941    25629    27.2 |  0.334 % |
c |      1220 | 2246629  5474072 |  906139    1091    33887    31.1 |  0.334 % |
c |      1445 | 2246629  5474072 |  996753    1316    46371    35.2 |  0.334 % |
c |      1784 | 2246629  5474072 | 1096429    1655    49052    29.6 |  0.334 % |
c |      2290 | 2246333  5473398 | 1206072    2156    53356    24.7 |  0.345 % |
c ==============================================================================
c [1mFound solution: 1371[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2548 | 2244951  5471847 |  748317    2397    54837    22.9 |  0.345 % |
c |      2649 | 2244707  5471292 |  823148    2496    61102    24.5 |  0.404 % |
c |      2799 | 2238897  5457941 |  905463    2584    71575    27.7 |  0.619 % |
c |      3024 | 2235765  5450754 |  996009    2788    87270    31.3 |  0.734 % |
c ==============================================================================
c [1mFound solution: 971[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3134 | 2241201  5464042 |  747067    2898    89277    30.8 |  0.734 % |
c ==============================================================================
c [1mFound solution: 789[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3171 | 2240828  5464387 |  746942    2931    97810    33.4 |  0.734 % |
c ==============================================================================
c [1mFound solution: 788[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3209 | 2238907  5459978 |  746302    2959   103291    34.9 |  0.734 % |
c ==============================================================================
c [1mFound solution: 781[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3217 | 2238910  5459985 |  746303    2967   115320    38.9 |  0.734 % |
c |      3318 | 2237644  5457074 |  820933    3059   136738    44.7 |  0.866 % |
c ==============================================================================
c [1mFound solution: 418[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3359 | 2236223  5454290 |  745407    3028   131265    43.4 |  0.866 % |
c ==============================================================================
c [1mFound solution: 233[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:366303     Base: 2 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3370 | 3058701  7372070 | 1019567    2798   130072    46.5 |  0.866 % |
c ==============================================================================
c [1mFound solution: 228[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:511729     Base: 2 3 3 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3383 | 4364516 10420271 | 1454838    2751   133630    48.6 |  0.866 % |
c |      3483 | 4364202 10419573 | 1600321    2848   136745    48.0 |  4.320 % |
c ==============================================================================
c [1mFound solution: 0[0m
c [1mOptimal solution: 0[0m
s OPTIMUM FOUND
v -x0 -x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 -x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 -x101 -x102 -x103 -x104 -x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 -x192 -x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 -x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 -x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 -x266 -x267 -x268 -x269 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 -x301 -x302 -x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 -x317 -x318 -x319 -x320 -x321 -x322 -x323 -x324 -x325 -x326 -x327 -x328 -x329 -x330 -x331 -x332 -x333 -x334 -x335 -x336 -x337 -x338 -x339 -x340 -x341 -x342 -x343 -x344 -x345 -x346 -x347 -x348 -x349 -x350 -x351 -x352 -x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 -x361 -x362 -x363 -x364 -x365 -x366 -x367 -x368 -x369 -x370 -x371 -x372 -x373 -x374 -x375 -x376 -x377 -x378 -x379 -x380 -x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 -x389 -x390 -x391 -x392 -x393 -x394 -x395 -x396 -x397 -x398 -x399 -x400 -x401 -x402 -x403 -x404 -x405 -x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 -x415 -x416 -x417 -x418 -x419 -x420 -x421 -x422 -x423 -x424 -x425 -x426 -x427 -x428 -x429 -x430 -x431 -x432 -x433 -x434 -x435 -x436 -x437 -x438 -x439 -x440 -x441 -x442 -x443 -x444 -x445 -x446 -x447 -x448 -x449 -x450 -x451 -x452 -x453 -x454 -x455 -x456 -x457 -x458 -x459 -x460 -x461 -x462 -x463 -x464 -x465 -x466 -x467 -x468 -x469 -x470 -x471 -x472 -x473 -x474 -x475 -x476 -x477 -x478 -x479 -x480 -x481 -x482 -x483 -x484 -x485 -x486 -x487 -x488 -x489 -x490 -x491 -x492 -x493 -x494 -x495 -x496 -x497 -x498 -x499 -x500 -x501 -x502 -x503 -x504 -x505 -x506 -x507 -x508 -x509 -x510 -x511 -x512 -x513 -x514 -x515 -x516 -x517 -x518 -x519 -x520 -x521 -x522 -x523 -x524 -x525 -x526 -x527 -x528 -x529 -x530 -x531 -x532 -x533 -x534 -x535 -x536 -x537 -x538 -x539 -x540 -x541 -x542 -x543 -x544 -x545 -x546 -x547 -x548 -x549 -x550 -x551 -x552 -x553 -x554 -x555 -x556 -x557 -x558 -x559 -x560 -x561 -x562 -x563 -x564 -x565 -x566 -x567 -x568 -x569 -x570 -x571 -x572 -x573 -x574 -x575 -x576 -x577 -x578 -x579 -x580 -x581 -x582 -x583 -x584 -x585 -x586 -x587 -x588 -x589 -x590 -x591 -x592 -x593 -x594 -x595 -x596 -x597 -x598 -x599 -x600 -x601 -x602 -x603 -x604 -x605 -x606 -x607 -x608 -x609 -x610 -x611 -x612 -x613 -x614 -x615 -x616 -x617 -x618 -x619 -x620 -x621 -x622 -x623 -x624 -x625 -x626 -x627 -x628 -x629 -x630 -x631 -x632 -x633 -x634 -x635 -x636 -x637 -x638 -x639 -x640 -x641 -x642 -x643 -x644 -x645 -x646 -x647 -x648 -x649 -x650 -x651 -x652 -x653 -x654 -x655 -x656 -x657 -x658 -x659 -x660 -x661 -x662 -x663 -x664 -x665 -x666 -x667 -x668 -x669 -x670 -x671 -x672 -x673 -x674 -x675 -x676 -x677 -x678 -x679 -x680 -x681 -x682 -x683 -x684 -x685 -x686 -x687 -x688 -x689 -x690 -x691 -x692 -x693 -x694 -x695 -x696 -x697 -x698 -x699 -x700 -x701 -x702 -x703 -x704 -x705 -x706 -x707 -x708 -x709 -x710 -x711 -x712 -x713 -x714 -x715 -x716 -x717 -x718 -x719 -x720 -x721 -x722 -x723 -x724 -x725 -x726 -x727 -x728 -x729 -x730 -x731 -x732 -x733 -x734 -x735 -x736 -x737 -x738 -x739 -x740 -x741 -x742 -x743 -x744 -x745 -x746 -x747 -x748 -x749 -x750 -x751 -x752 -x753 -x754 -x755 -x756 -x757 -x758 -x759 -x760 -x761 -x762 -x763 -x764 -x765 -x766 -x767 -x768 -x769 -x770 -x771 -x772 -x773 -x774 -x775 -x776 -x777 -x778 -x779 -x780 -x781 -x782 -x783 -x784 -x785 -x786 -x787 -x788 -x789 -x790 -x791 -x792 -x793 -x794 -x795 -x796 -x797 -x798 -x799 -x800 -x801 -x802 -x803 -x804 -x805 -x806 -x807 -x808 -x809 -x810 -x811 -x812 -x813 -x814 -x815 -x816 -x817 -x818 -x819 -x820 -x821 -x822 -x823 -x824 -x825 -x826 -x827 -x828 -x829 -x830 -x831 -x832 -x833 -x834 -x835 -x836 -x837 -x838 -x839 -x840 -x841 -x842 -x843 -x844 -x845 -x846 -x847 -x848 -x849 -x850 -x851 -x852 -x853 -x854 -x855 -x856 -x857 -x858 -x859 -x860 -x861 -x862 -x863 -x864 -x865 -x866 -x867 -x868 -x869 -x870 -x871 -x872 -x873 -x874 -x875 -x876 -x877 -x878 -x879 -x880 -x881 -x882 -x883 -x884 -x885 -x886 -x887 -x888 -x889 -x890 -x891 -x892 -x893 -x894 -x895 -x896 -x897 -x898 -x899 -x900 -x901 -x902 -x903 -x904 -x905 -x906 -x907 -x908 -x909 -x910 -x911 -x912 -x913 -x914 -x915 -x916 -x917 -x918 -x919 -x920 -x921 -x922 -x923 -x924 -x925 -x926 -x927 -x928 -x929 -x930 -x931 -x932 -x933 -x934 -x935 -x936 -x937 -x938 -x939 -x940 -x941 -x942 -x943 -x944 -x945 -x946 -x947 -x948 -x949 -x950 -x951 -x952 -x953 -x954 -x955 -x956 -x957 -x958 -x959 -x960 -x961 -x962 -x963 -x964 -x965 -x966 -x967 -x968 -x969 -x970 -x971 -x972 -x973 -x974 -x975 -x976 -x977 -x978 -x979 -x980 -x981 -x982 -x983 -x984 -x985 -x986 -x987 -x988 -x989 -x990 -x991 -x992 -x993 -x994 -x995 -x996 -x997 -x998 -x999 -x1000 -x1001 -x1002 -x1003 -x1004 -x1005 -x1006 -x1007 -x1008 -x1009 -x1010 -x1011 -x1012 -x1013 -x1014 -x1015 -x1016 -x1017 -x1018 -x1019 -x1020 -x1021 -x1022 -x1023 -x1024 -x1025 -x1026 -x1027 -x1028 -x1029 -x1030 -x1031 -x1032 -x1033 -x1034 -x1035 -x1036 -x1037 -x1038 -x1039 -x1040 -x1041 -x1042 -x1043 -x1044 -x1045 -x1046 -x1047 -x1048 -x1049 -x1050 -x1051 -x1052 -x1053 -x1054 -x1055 -x1056 -x1057 -x1058 -x1059 -x1060 -x1061 -x1062 -x1063 -x1064 -x1065 -x1066 -x1067 -x1068 -x1069 -x1070 -x1071 -x1072 -x1073 -x1074 -x1075 -x1076 -x1077 -x1078 -x1079 -x1080 -x1081 -x1082 -x1083 -x1084 -x1085 -x1086 -x1087 -x1088 -x1089 -x1090 -x1091 -x1092 -x1093 -x1094 -x1095 -x1096 -x1097 -x1098 -x1099 -x1100 -x1101 -x1102 -x1103 -x1104 -x1105 -x1106 -x1107 -x1108 -x1109 -x1110 -x1111 -x1112 -x1113 -x1114 -x1115 -x1116 -x1117 -x1118 -x1119 -x1120 -x1121 -x1122 -x1123 -x1124 -x1125 -x1126 -x1127 -x1128 -x1129 -x1130 -x1131 -x1132 -x1133 -x1134 -x1135 -x1136 -x1137 -x1138 -x1139 -x1140 -x1141 -x1142 -x1143 -x1144 -x1145 -x1146 -x1147 -x1148 -x1149 -x1150 -x1151 -x1152 -x1153 -x1154 -x1155 -x1156 -x1157 -x1158 -x1159 -x1160 -x1161 -x1162 -x1163 -x1164 -x1165 -x1166 -x1167 -x1168 -x1169 -x1170 -x1171 -x1172 -x1173 -x1174 -x1175 -x1176 -x1177 -x1178 -x1179 -x1180 -x1181 -x1182 -x1183 -x1184 -x1185 -x1186 -x1187 -x1188 -x1189 -x1190 -x1191 -x1192 -x1193 -x1194 -x1195 -x1196 -x1197 -x1198 -x1199 -x1200 -x1201 -x1202 -x1203 -x1204 -x1205 -x1206 -x1207 -x1208 -x1209 -x1210 -x1211 -x1212 -x1213 -x1214 -x1215 -x1216 -x1217 -x1218 -x1219 -x1220 -x1221 -x1222 -x1223 -x1224 -x1225 -x1226 -x1227 -x1228 -x1229 -x1230 -x1231 -x1232 -x1233 -x1234 -x1235 -x1236 -x1237 -x1238 -x1239 -x1240 -x1241 -x1242 -x1243 -x1244 -x1245 -x1246 -x1247 -x1248 -x1249 -x1250 -x1251 -x1252 -x1253 -x1254 -x1255 -x1256 -x1257 -x1258 -x1259 -x1260 -x1261 -x1262 -x1263 -x1264 -x1265 -x1266 -x1267 -x1268 -x1269 -x1270 -x1271 -x1272 -x1273 -x1274 -x1275 -x1276 -x1277 -x1278 -x1279 -x1280 -x1281 -x1282 -x1283 -x1284 -x1285 -x1286 -x1287 -x1288 -x1289 -x1290 -x1291 -x1292 -x1293 -x1294 -x1295 -x1296 -x1297 -x1298 -x1299 -x1300 -x1301 -x1302 -x1303 -x1304 -x1305 -x1306 -x1307 -x1308 -x1309 -x1310 -x1311 -x1312 -x1313 -x1314 -x1315 -x1316 -x1317 -x1318 -x1319 -x1320 -x1321 -x1322 -x1323 -x1324 -x1325 -x1326 -x1327 -x1328 -x1329 -x1330 -x1331 -x1332 -x1333 -x1334 -x1335 -x1336 -x1337 -x1338 -x1339 -x1340 -x1341 -x1342 -x1343 -x1344 -x1345 -x1346 -x1347 -x1348 -x1349 -x1350 -x1351 -x1352 -x1353 -x1354 -x1355 -x1356 -x1357 -x1358 -x1359 -x1360 -x1361 -x1362 -x1363 -x1364 -x1365 -x1366 -x1367 -x1368 -x1369 -x1370 -x1371 -x1372 -x1373 -x1374 -x1375 -x1376 -x1377 -x1378 -x1379 -x1380 -x1381 -x1382 -x1383 -x1384 -x1385 -x1386 -x1387 -x1388 -x1389 -x1390 -x1391 -x1392 -x1393 -x1394 -x1395 -x1396 -x1397 -x1398 -x1399 -x1400 -x1401 -x1402 -x1403 -x1404 -x1405 -x1406 -x1407 -x1408 -x1409 -x1410 -x1411 -x1412 -x1413 -x1414 -x1415 -x1416 -x1417 -x1418 -x1419 -x1420 -x1421 -x1422 -x1423 -x1424 -x1425 -x1426 -x1427 -x1428 -x1429 -x1430 -x1431 -x1432 -x1433 -x1434 -x1435 -x1436 -x1437 -x1438 -x1439 -x1440 -x1441 -x1442 -x1443 -x1444 -x1445 -x1446 -x1447 -x1448 -x1449 -x1450 -x1451 -x1452 -x1453 -x1454 -x1455 -x1456 -x1457 -x1458 -x1459 -x1460 -x1461 -x1462 -x1463 -x1464 -x1465 -x1466 -x1467 -x1468 -x1469 -x1470 -x1471 -x1472 -x1473 -x1474 -x1475 -x1476 -x1477 -x1478 -x1479 -x1480 -x1481 -x1482 -x1483 -x1484 -x1485 -x1486 -x1487 -x1488 -x1489 -x1490 -x1491 -x1492 -x1493 -x1494 -x1495 -x1496 -x1497 -x1498 -x1499 -x1500 -x1501 -x1502 -x1503 -x1504 -x1505 -x1506 -x1507 -x1508 -x1509 -x1510 -x1511 -x1512 -x1513 -x1514 -x1515 -x1516 -x1517 -x1518 -x1519 -x1520 -x1521 -x1522 -x1523 -x1524 -x1525 -x1526 -x1527 -x1528 -x1529 -x1530 -x1531 -x1532 -x1533 -x1534 -x1535 -x1536 -x1537 -x1538 -x1539 -x1540 -x1541 -x1542 -x1543 -x1544 -x1545 -x1546 -x1547 -x1548 -x1549 -x1550 -x1551 -x1552 -x1553 -x1554 -x1555 -x1556 -x1557 -x1558 -x1559 -x1560 -x1561 -x1562 -x1563 -x1564 -x1565 -x1566 -x1567 -x1568 -x1569 -x1570 -x1571 -x1572 -x1573 -x1574 -x1575 -x1576 -x1577 -x1578 -x1579 -x1580 -x1581 -x1582 -x1583 -x1584 -x1585 -x1586 -x1587 -x1588 -x1589 -x1590 -x1591 -x1592 -x1593 -x1594 -x1595 -x1596 -x1597 -x1598 -x1599 -x1600 -x1601 -x1602 -x1603 -x1604 -x1605 -x1606 -x1607 -x1608 -x1609 -x1610 -x1611 -x1612 -x1613 -x1614 -x1615 -x1616 -x1617 -x1618 -x1619 -x1620 -x1621 -x1622 -x1623 -x1624 -x1625 -x1626 -x1627 -x1628 -x1629 -x1630 -x1631 -x1632 -x1633 -x1634 -x1635 -x1636 -x1637 -x1638 -x1639 -x1640 -x1641 -x1642 -x1643 -x1644 -x1645 -x1646 -x1647 -x1648 -x1649 -x1650 -x1651 -x1652 -x1653 -x1654 -x1655 -x1656 -x1657 -x1658 -x1659 -x1660 -x1661 -x1662 -x1663 -x1664 -x1665 -x1666 -x1667 -x1668 -x1669 -x1670 -x1671 -x1672 -x1673 -x1674 -x1675 -x1676 -x1677 -x1678 -x1679 -x1680 -x1681 -x1682 -x1683 -x1684 -x1685 -x1686 -x1687 -x1688 -x1689 -x1690 -x1691 -x1692 -x1693 -x1694 -x1695 -x1696 -x1697 -x1698 -x1699 -x1700 -x1701 -x1702 -x1703 -x1704 -x1705 -x1706 -x1707 -x1708 -x1709 -x1710 -x1711 -x1712 -x1713 -x1714 -x1715 -x1716 -x1717 -x1718 -x1719 -x1720 -x1721 -x1722 -x1723 -x1724 -x1725 -x1726 -x1727 -x1728 -x1729 -x1730 -x1731 -x1732 -x1733 -x1734 -x1735 -x1736 -x1737 -x1738 -x1739 -x1740 -x1741 -x1742 -x1743 -x1744 -x1745 -x1746 -x1747 -x1748 -x1749 -x1750 -x1751 -x1752 -x1753 -x1754 -x1755 -x1756 -x1757 -x1758 -x1759 -x1760 -x1761 -x1762 -x1763 -x1764 -x1765 -x1766 -x1767 -x1768 -x1769 -x1770 -x1771 -x1772 -x1773 -x1774 -x1775 -x1776 -x1777 -x1778 -x1779 -x1780 -x1781 -x1782 -x1783 -x1784 -x1785 -x1786 -x1787 -x1788 -x1789 -x1790 -x1791 -x1792 -x1793 -x1794 -x1795 -x1796 -x1797 -x1798 -x1799 -x1800 -x1801 -x1802 -x1803 -x1804 -x1805 -x1806 -x1807 -x1808 -x1809 -x1810 -x1811 -x1812 -x1813 -x1814 -x1815 -x1816 -x1817 -x1818 -x1819 -x1820 -x1821 -x1822 -x1823 -x1824 -x1825 -x1826 -x1827 -x1828 -x1829 -x1830 -x1831 -x1832 -x1833 -x1834 -x1835 -x1836 -x1837 -x1838 -x1839 -x1840 -x1841 -x1842 -x1843 -x1844 -x1845 -x1846 -x1847 -x1848 -x1849 -x1850 -x1851 -x1852 -x1853 -x1854 -x1855 -x1856 -x1857 -x1858 -x1859 -x1860 -x1861 -x1862 -x1863 -x1864 -x1865 -x1866 -x1867 -x1868 -x1869 -x1870 -x1871 -x1872 -x1873 -x1874 -x1875 -x1876 -x1877 -x1878 -x1879 -x1880 -x1881 -x1882 -x1883 -x1884 -x1885 -x1886 -x1887 -x1888 -x1889 -x1890 -x1891 -x1892 -x1893 -x1894 -x1895 -x1896 -x1897 -x1898 -x1899 -x1900 -x1901 -x1902 -x1903 -x1904 -x1905 -x1906 -x1907 -x1908 -x1909 -x1910 -x1911 -x1912 -x1913 -x1914 -x1915 -x1916 -x1917 -x1918 -x1919 -x1920 -x1921 -x1922 -x1923 -x1924 -x1925 -x1926 -x1927 -x1928 -x1929 -x1930 -x1931 -x1932 -x1933 -x1934 -x1935 -x1936 -x1937 -x1938 -x1939 -x1940 -x1941 -x1942 -x1943 -x1944 -x1945 -x1946 -x1947 -x1948 -x1949 -x1950 -x1951 -x1952 -x1953 -x1954 -x1955 -x1956 -x1957 -x1958 -x1959 -x1960 -x1961 -x1962 -x1963 -x1964 -x1965 -x1966 -x1967 -x1968 -x1969 -x1970 -x1971 -x1972 -x1973 -x1974 -x1975 -x1976 -x1977 -x1978 -x1979 -x1980 -x1981 -x1982 -x1983 -x1984 -x1985 -x1986 -x1987 -x1988
c _______________________________________________________________________________
c 
c restarts              : 25
c conflicts             : 3531           (12 /sec)
c decisions             : 282241         (939 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 300.685 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.88 0.97 0.91 2/54 10070
Raw data (stat): 10070 (runsolver) R 10069 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 429658339 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0032 s]
Raw data (loadavg): 0.90 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 39446 0 0 0 903 95 0 0 25 0 1 0 429658339 164200448 36231 4294967295 134512640 134672761 3221224560 3221177984 134556775 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40088 36232 603 41 0 40047 0
vsize: 160352
[startup+20.0041 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 68000 0 0 0 1835 163 0 0 25 0 1 0 429658339 295845888 64785 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72228 64785 603 41 0 72187 0
vsize: 288912
[startup+30.0048 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 68412 0 0 0 2834 164 0 0 25 0 1 0 429658339 296116224 65197 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72294 65197 603 41 0 72253 0
vsize: 289176
[startup+40.0045 s]
Raw data (loadavg): 0.94 0.97 0.91 3/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 68432 0 0 0 3833 165 0 0 25 0 1 0 429658339 296251392 65217 4294967295 134512640 134672761 3221224560 3221223728 134560849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72327 65217 603 41 0 72286 0
vsize: 289308
[startup+50.0054 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 68437 0 0 0 4833 165 0 0 25 0 1 0 429658339 296251392 65222 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72327 65222 603 41 0 72286 0
vsize: 289308
[startup+60.0052 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 69573 0 0 0 5830 168 0 0 25 0 1 0 429658339 300896256 66284 4294967295 134512640 134672761 3221224560 3221223860 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73461 66284 603 41 0 73420 0
vsize: 293844
[startup+70.0071 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 69584 0 0 0 6830 168 0 0 25 0 1 0 429658339 300896256 66295 4294967295 134512640 134672761 3221224560 3221223696 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73461 66295 603 41 0 73420 0
vsize: 293844
[startup+80.0082 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 69592 0 0 0 7830 168 0 0 25 0 1 0 429658339 300896256 66303 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73461 66303 603 41 0 73420 0
vsize: 293844
[startup+90.0078 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 69605 0 0 0 8829 168 0 0 25 0 1 0 429658339 301027328 66316 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73493 66316 603 41 0 73452 0
vsize: 293972
[startup+100.008 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 69617 0 0 0 9829 168 0 0 25 0 1 0 429658339 301027328 66328 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73493 66328 603 41 0 73452 0
vsize: 293972
[startup+110.008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 69772 0 0 0 10829 168 0 0 25 0 1 0 429658339 301309952 66409 4294967295 134512640 134672761 3221224560 3221223860 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73562 66409 603 41 0 73521 0
vsize: 294248
[startup+120.009 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 69772 0 0 0 11830 168 0 0 25 0 1 0 429658339 301309952 66409 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73562 66409 603 41 0 73521 0
vsize: 294248
[startup+130.009 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 69776 0 0 0 12830 168 0 0 25 0 1 0 429658339 301309952 66413 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73562 66413 603 41 0 73521 0
vsize: 294248
[startup+140.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 69782 0 0 0 13830 168 0 0 25 0 1 0 429658339 301309952 66419 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73562 66419 603 41 0 73521 0
vsize: 294248
[startup+150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 69784 0 0 0 14830 168 0 0 25 0 1 0 429658339 301445120 66421 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73595 66421 603 41 0 73554 0
vsize: 294380
[startup+160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 69792 0 0 0 15830 169 0 0 25 0 1 0 429658339 301445120 66429 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73595 66429 603 41 0 73554 0
vsize: 294380
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 70031 0 0 0 16830 169 0 0 25 0 1 0 429658339 302088192 66594 4294967295 134512640 134672761 3221224560 3221223684 134566075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73752 66594 603 41 0 73711 0
vsize: 295008
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 70167 0 0 0 17829 169 0 0 25 0 1 0 429658339 302100480 66656 4294967295 134512640 134672761 3221224560 3221223752 134556585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73755 66656 603 41 0 73714 0
vsize: 295020
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 70305 0 0 0 18829 170 0 0 25 0 1 0 429658339 302362624 66720 4294967295 134512640 134672761 3221224560 3221223824 134562361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73819 66720 603 41 0 73778 0
vsize: 295276
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 70412 0 0 0 19829 170 0 0 25 0 1 0 429658339 302497792 66753 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73852 66753 603 41 0 73811 0
vsize: 295408
[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 70544 0 0 0 20829 170 0 0 25 0 1 0 429658339 303546368 66885 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74108 66885 603 41 0 74067 0
vsize: 296432
[startup+220.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 70544 0 0 0 21829 170 0 0 25 0 1 0 429658339 303546368 66885 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74108 66885 603 41 0 74067 0
vsize: 296432
[startup+230.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 70656 0 0 0 22829 171 0 0 25 0 1 0 429658339 303812608 66920 4294967295 134512640 134672761 3221224560 3221223728 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74173 66920 603 41 0 74132 0
vsize: 296692
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 95327 0 0 0 23769 231 0 0 25 0 1 0 429658339 461594624 91591 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112694 91591 603 41 0 112653 0
vsize: 450776
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 112472 0 0 0 24728 272 0 0 25 0 1 0 429658339 500109312 106099 4294967295 134512640 134672761 3221224560 3221174256 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122097 106100 603 41 0 122056 0
vsize: 488388
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 136501 0 0 0 25674 327 0 0 25 0 1 0 429658339 590417920 130128 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 144145 130128 603 41 0 144104 0
vsize: 576580
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 136659 0 0 0 26674 327 0 0 25 0 1 0 429658339 590417920 130286 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 144145 130286 603 41 0 144104 0
vsize: 576580
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 136685 0 0 0 27674 327 0 0 25 0 1 0 429658339 590417920 130312 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 144145 130312 603 41 0 144104 0
vsize: 576580
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 136685 0 0 0 28674 327 0 0 25 0 1 0 429658339 590417920 130312 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 144145 130312 603 41 0 144104 0
vsize: 576580
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 136744 0 0 0 29674 327 0 0 25 0 1 0 429658339 590417920 130371 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 144145 130371 603 41 0 144104 0
vsize: 576580
[startup+304.902 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 10070
Raw data (stat): 10070 (minisat+) R 10069 29151 29150 0 -1 0 136744 0 0 0 29674 327 0 0 25 0 1 0 429658339 590417920 130371 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 144145 130371 603 41 0 144104 0
vsize: 0

Child status: 30
Real time (s): 304.902
CPU time (s): 304.907
CPU user time (s): 301.353
CPU system time (s): 3.55346
CPU usage (%): 100.002
Max. virtual memory (Kb): 576580
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	0
#### END VERIFIER DATA ####