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/manquinho/primes-dimacs-cnf/normalized-ii8a4.opb
MD5SUM	8a77190c2eeefb9e88447a9087adfd6f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	283
Optimality of the best value was proved	NO
Number of terms in the objective function	792
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	792
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	792
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02084
Number of variables	792
Total number of constraints	3194
Number of constraints which are clauses	3194
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	8
Trace number 4737

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-13 20:07:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3550 boxname=wulflinc18 idbench=166 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  8a77190c2eeefb9e88447a9087adfd6f  /oldhome/oroussel/tmp/wulflinc18/normalized-ii8a4.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc18/normalized-ii8a4.opb /oldhome/oroussel/tmp/wulflinc18/normalized-ii8a4.opb
IDLAUNCH: 3550
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        908928 kB
Buffers:         33976 kB
Cached:          55668 kB
SwapCached:        320 kB
Active:          48180 kB
Inactive:        44668 kB
HighTotal:      131008 kB
HighFree:        71344 kB
LowTotal:       903652 kB
LowFree:        837584 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            27260 kB
Committed_AS:    63704 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:27:25 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 3550 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3194 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    3194     8388 |    1064       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 354[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1576   maxlim: 438   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         4 |   14180    47615 |    4726       4       26     6.5 |  0.000 % |
c |       104 |   14180    47615 |    5198     104     2108    20.3 |  0.295 % |
c |       254 |   14180    47615 |    5718     254     3193    12.6 |  0.295 % |
c |       479 |   14180    47615 |    6290     479     5594    11.7 |  0.295 % |
c |       816 |   14180    47615 |    6919     816    15442    18.9 |  0.295 % |
c |      1323 |   14180    47615 |    7611    1323    20712    15.7 |  0.295 % |
c ==============================================================================
c [1mFound solution: 342[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 450   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1546 |   14185    47647 |    4728    1546    22165    14.3 |  0.295 % |
c |      1647 |   14185    47647 |    5200    1647    22687    13.8 |  0.421 % |
c |      1797 |   14185    47647 |    5720    1797    23814    13.3 |  0.421 % |
c |      2022 |   14185    47647 |    6292    2022    25470    12.6 |  0.421 % |
c |      2360 |   14185    47647 |    6922    2360    28806    12.2 |  0.421 % |
c |      2867 |   14185    47647 |    7614    2867    33979    11.9 |  0.421 % |
c |      3626 |   14185    47647 |    8375    3626    70720    19.5 |  0.421 % |
c ==============================================================================
c [1mFound solution: 331[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 461   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3805 |   14192    47690 |    4730    3805    71685    18.8 |  0.421 % |
c |      3905 |   14192    47690 |    5203    3905    73037    18.7 |  0.546 % |
c |      4055 |   14192    47690 |    5723    4055    77526    19.1 |  0.546 % |
c |      4280 |   14192    47690 |    6295    4280    79546    18.6 |  0.546 % |
c |      4617 |   14192    47690 |    6925    4617    85906    18.6 |  0.546 % |
c |      5127 |   14192    47690 |    7617    5127   116419    22.7 |  0.546 % |
c |      5886 |   14192    47690 |    8379    5886   133538    22.7 |  0.546 % |
c |      7026 |   14192    47690 |    9217    7026   208828    29.7 |  0.546 % |
c |      8734 |   14192    47690 |   10139    8734   302360    34.6 |  0.546 % |
c |     11296 |   14192    47690 |   11153   11296   469947    41.6 |  0.546 % |
c |     15142 |   14192    47690 |   12268    9494   480880    50.7 |  0.546 % |
c |     20910 |   14192    47690 |   13495    8440   779345    92.3 |  0.546 % |
c ==============================================================================
c [1mFound solution: 325[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 467   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21977 |   14195    47708 |    4731    9507   792680    83.4 |  0.546 % |
c |     22077 |   14195    47708 |    5204    2477    36804    14.9 |  0.629 % |
c |     22231 |   14195    47708 |    5724    2631    38637    14.7 |  0.629 % |
c |     22456 |   14195    47708 |    6296    2856    40778    14.3 |  0.629 % |
c |     22793 |   14195    47708 |    6926    3193    49832    15.6 |  0.629 % |
c |     23302 |   14195    47708 |    7619    3702    60786    16.4 |  0.629 % |
c |     24062 |   14195    47708 |    8381    4462    99473    22.3 |  0.629 % |
c |     25201 |   14195    47708 |    9219    5601   159468    28.5 |  0.629 % |
c |     26911 |   14195    47708 |   10141    7311   223253    30.5 |  0.629 % |
c |     29473 |   14195    47708 |   11155    9873   316969    32.1 |  0.629 % |
c |     33317 |   14195    47708 |   12270    7235   300970    41.6 |  0.629 % |
c |     39085 |   14195    47708 |   13498   13003   808591    62.2 |  0.629 % |
c |     47736 |   14195    47708 |   14847   14185  1508478   106.3 |  0.629 % |
c |     60710 |   14195    47708 |   16332   10842  1479008   136.4 |  0.629 % |
c |     80171 |   14195    47708 |   17965   12425  1107117    89.1 |  0.629 % |
c |    109363 |   14195    47708 |   19762   12249  1188960    97.1 |  0.629 % |
c |    153152 |   14195    47708 |   21738   13380  1065265    79.6 |  0.629 % |
c |    218837 |   14195    47708 |   23912   21266  3188771   149.9 |  0.631 % |
c ==============================================================================
c [1mFound solution: 323[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 469   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    232802 |   14197    47720 |    4732   22441  1914605    85.3 |  0.631 % |
c |    232902 |   14197    47720 |    5205    2906   102660    35.3 |  0.671 % |
c |    233052 |   14197    47720 |    5725    3056   105475    34.5 |  0.671 % |
c |    233277 |   14197    47720 |    6298    3281   107454    32.8 |  0.672 % |
c |    233615 |   14197    47720 |    6928    3619   118688    32.8 |  0.671 % |
c |    234121 |   14197    47720 |    7620    4125   130601    31.7 |  0.671 % |
c |    234880 |   14197    47720 |    8383    4884   172713    35.4 |  0.671 % |
c |    236020 |   14197    47720 |    9221    6024   190010    31.5 |  0.671 % |
c |    237728 |   14197    47720 |   10143    7732   257551    33.3 |  0.671 % |
c |    240293 |   14197    47720 |   11157   10297   398159    38.7 |  0.671 % |
c |    244138 |   14197    47720 |   12273    8435   385358    45.7 |  0.671 % |
c |    249906 |   14197    47720 |   13500    7435   461232    62.0 |  0.671 % |
c |    258555 |   14197    47720 |   14851    8599   770308    89.6 |  0.671 % |
c |    271529 |   14197    47720 |   16336   13542  1260294    93.1 |  0.671 % |
c |    290990 |   14197    47720 |   17969   15348  1644616   107.2 |  0.671 % |
c |    320182 |   14197    47720 |   19766   15365  2243870   146.0 |  0.671 % |
c |    363972 |   14197    47720 |   21743   16256  1819108   111.9 |  0.671 % |
c |    429657 |   14197    47720 |   23917   11805  1200471   101.7 |  0.671 % |
c |    528184 |   14197    47720 |   26309   22012  2996969   136.2 |  0.671 % |
c ==============================================================================
c [1mFound solution: 322[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 470   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    643048 |   14199    47733 |    4733   25656  3974712   154.9 |  0.671 % |
c |    643148 |   14199    47733 |    5206    3307   223155    67.5 |  0.712 % |
c |    643298 |   14199    47733 |    5726    3457   224051    64.8 |  0.712 % |
c |    643523 |   14199    47733 |    6299    3682   230601    62.6 |  0.712 % |
c |    643860 |   14199    47733 |    6929    4019   233767    58.2 |  0.712 % |
c |    644367 |   14199    47733 |    7622    4526   242365    53.5 |  0.712 % |
c |    645126 |   14199    47733 |    8384    5285   258950    49.0 |  0.712 % |
c |    646266 |   14199    47733 |    9223    6425   334202    52.0 |  0.712 % |
c |    647975 |   14199    47733 |   10145    8134   424514    52.2 |  0.712 % |
c |    650538 |   14199    47733 |   11160   10697   585670    54.8 |  0.712 % |
c |    654382 |   14199    47733 |   12276    8183   488448    59.7 |  0.713 % |
c |    660151 |   14199    47733 |   13503    7110   611881    86.1 |  0.712 % |
c ==============================================================================
c [1mFound solution: 320[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 472   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    667666 |   14201    47752 |    4733   14625  1392514    95.2 |  0.712 % |
c |    667766 |   14201    47752 |    5206    3757   241480    64.3 |  0.795 % |
c |    667919 |   14201    47752 |    5726    3910   245198    62.7 |  0.795 % |
c |    668145 |   14201    47752 |    6299    4136   247456    59.8 |  0.795 % |
c |    668483 |   14201    47752 |    6929    4474   259361    58.0 |  0.795 % |
c |    668989 |   14201    47752 |    7622    4980   264123    53.0 |  0.795 % |
c |    669749 |   14201    47752 |    8384    5740   301354    52.5 |  0.795 % |
c |    670888 |   14201    47752 |    9223    6879   337236    49.0 |  0.796 % |
c |    672596 |   14201    47752 |   10145    8587   442568    51.5 |  0.795 % |
c |    675158 |   14201    47752 |   11160    5852   260198    44.5 |  0.795 % |
c |    679002 |   14201    47752 |   12276    9696   535813    55.3 |  0.795 % |
c |    684768 |   14201    47752 |   13503    9074   567941    62.6 |  0.795 % |
c |    693419 |   14201    47752 |   14854   10297   683827    66.4 |  0.795 % |
c |    706394 |   14201    47752 |   16339   15070  1810934   120.2 |  0.795 % |
c |    725858 |   14201    47752 |   17973   16742  1692185   101.1 |  0.795 % |
c |    755050 |   14201    47752 |   19770   17056  1491062    87.4 |  0.795 % |
c |    798840 |   14201    47752 |   21748   18889  2551967   135.1 |  0.795 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v 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#### 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.95 0.87 2/55 22811
Raw data (stat): 22811 (runsolver) R 22810 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478698105 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0008 s]
Raw data (loadavg): 0.87 0.95 0.87 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 1543 0 0 0 994 4 0 0 25 0 1 0 478698105 7847936 1521 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1916 1521 603 41 0 1875 0
vsize: 7664
[startup+20.0003 s]
Raw data (loadavg): 0.89 0.96 0.87 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 1660 0 0 0 1993 4 0 0 25 0 1 0 478698105 8388608 1638 4294967295 134512640 134672761 3221224576 3221223724 134565030 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2048 1638 603 41 0 2007 0
vsize: 8192
[startup+30.0013 s]
Raw data (loadavg): 0.91 0.96 0.87 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 2085 0 0 0 2993 5 0 0 25 0 1 0 478698105 10141696 2063 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2476 2063 603 41 0 2435 0
vsize: 9904
[startup+40.0015 s]
Raw data (loadavg): 0.92 0.96 0.87 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 2527 0 0 0 3991 6 0 0 25 0 1 0 478698105 12034048 2505 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2938 2505 603 41 0 2897 0
vsize: 11752
[startup+50.0024 s]
Raw data (loadavg): 0.93 0.96 0.87 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 2919 0 0 0 4991 7 0 0 25 0 1 0 478698105 13647872 2897 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3332 2897 603 41 0 3291 0
vsize: 13328
[startup+60.002 s]
Raw data (loadavg): 0.94 0.96 0.87 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 2958 0 0 0 5991 7 0 0 25 0 1 0 478698105 13783040 2936 4294967295 134512640 134672761 3221224576 3221223680 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3365 2936 603 41 0 3324 0
vsize: 13460
[startup+70.0022 s]
Raw data (loadavg): 0.95 0.96 0.87 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 2958 0 0 0 6991 7 0 0 25 0 1 0 478698105 13783040 2936 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3365 2936 603 41 0 3324 0
vsize: 13460
[startup+80.0028 s]
Raw data (loadavg): 0.96 0.96 0.87 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 2959 0 0 0 7991 7 0 0 25 0 1 0 478698105 13783040 2937 4294967295 134512640 134672761 3221224576 3221223744 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3365 2937 603 41 0 3324 0
vsize: 13460
[startup+90.0028 s]
Raw data (loadavg): 0.96 0.96 0.87 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 2959 0 0 0 8991 7 0 0 25 0 1 0 478698105 13783040 2937 4294967295 134512640 134672761 3221224576 3221223760 134559324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3365 2937 603 41 0 3324 0
vsize: 13460
[startup+100.004 s]
Raw data (loadavg): 0.97 0.96 0.88 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 3185 0 0 0 9991 8 0 0 25 0 1 0 478698105 14602240 3163 4294967295 134512640 134672761 3221224576 3221223680 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3565 3163 603 41 0 3524 0
vsize: 14260
[startup+110.005 s]
Raw data (loadavg): 0.97 0.96 0.88 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 3187 0 0 0 10990 8 0 0 25 0 1 0 478698105 14602240 3165 4294967295 134512640 134672761 3221224576 3221223680 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3565 3165 603 41 0 3524 0
vsize: 14260
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.88 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 3187 0 0 0 11990 9 0 0 25 0 1 0 478698105 14602240 3165 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3565 3165 603 41 0 3524 0
vsize: 14260
[startup+130.006 s]
Raw data (loadavg): 0.98 0.97 0.88 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 3187 0 0 0 12990 9 0 0 25 0 1 0 478698105 14602240 3165 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3565 3165 603 41 0 3524 0
vsize: 14260
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.88 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 3369 0 0 0 13990 9 0 0 25 0 1 0 478698105 15429632 3347 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3767 3347 603 41 0 3726 0
vsize: 15068
[startup+150.006 s]
Raw data (loadavg): 0.98 0.97 0.88 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 3369 0 0 0 14990 9 0 0 25 0 1 0 478698105 15429632 3347 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3767 3347 603 41 0 3726 0
vsize: 15068
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.88 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 3370 0 0 0 15990 9 0 0 25 0 1 0 478698105 15429632 3348 4294967295 134512640 134672761 3221224576 3221223680 134560237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3767 3348 603 41 0 3726 0
vsize: 15068
[startup+170.006 s]
Raw data (loadavg): 1.07 0.99 0.89 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 3371 0 0 0 16990 9 0 0 25 0 1 0 478698105 15429632 3349 4294967295 134512640 134672761 3221224576 3221223744 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3767 3349 603 41 0 3726 0
vsize: 15068
[startup+180.007 s]
Raw data (loadavg): 1.06 0.99 0.89 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4014 0 0 0 17988 11 0 0 25 0 1 0 478698105 17989632 3992 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4392 3992 603 41 0 4351 0
vsize: 17568
[startup+190.007 s]
Raw data (loadavg): 1.05 0.99 0.89 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4017 0 0 0 18988 11 0 0 25 0 1 0 478698105 18128896 3995 4294967295 134512640 134672761 3221224576 3221223680 134560269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4426 3995 603 41 0 4385 0
vsize: 17704
[startup+200.008 s]
Raw data (loadavg): 1.04 0.99 0.89 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4416 0 0 0 19987 13 0 0 25 0 1 0 478698105 19750912 4394 4294967295 134512640 134672761 3221224576 3221223680 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4822 4394 603 41 0 4781 0
vsize: 19288
[startup+210.008 s]
Raw data (loadavg): 1.03 0.99 0.89 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4416 0 0 0 20987 13 0 0 25 0 1 0 478698105 19750912 4394 4294967295 134512640 134672761 3221224576 3221223744 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4822 4394 603 41 0 4781 0
vsize: 19288
[startup+220.008 s]
Raw data (loadavg): 1.03 0.99 0.89 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4416 0 0 0 21987 13 0 0 25 0 1 0 478698105 19750912 4394 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4822 4394 603 41 0 4781 0
vsize: 19288
[startup+230.009 s]
Raw data (loadavg): 1.02 0.99 0.89 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4416 0 0 0 22987 13 0 0 25 0 1 0 478698105 19750912 4394 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4822 4394 603 41 0 4781 0
vsize: 19288
[startup+240.008 s]
Raw data (loadavg): 1.02 0.99 0.89 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4770 0 0 0 23986 14 0 0 25 0 1 0 478698105 21229568 4748 4294967295 134512640 134672761 3221224576 3221223680 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5183 4748 603 41 0 5142 0
vsize: 20732
[startup+250.01 s]
Raw data (loadavg): 1.02 0.99 0.90 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4777 0 0 0 24986 14 0 0 25 0 1 0 478698105 21229568 4755 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5183 4755 603 41 0 5142 0
vsize: 20732
[startup+260.009 s]
Raw data (loadavg): 1.01 0.99 0.90 2/55 22811
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4951 0 0 0 25986 15 0 0 25 0 1 0 478698105 21901312 4929 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4929 603 41 0 5306 0
vsize: 21388
[startup+270.009 s]
Raw data (loadavg): 1.01 0.99 0.90 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4951 0 0 0 26985 16 0 0 25 0 1 0 478698105 21901312 4929 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5347 4929 603 41 0 5306 0
vsize: 21388
[startup+280.011 s]
Raw data (loadavg): 1.01 0.99 0.90 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4951 0 0 0 27985 16 0 0 25 0 1 0 478698105 21901312 4929 4294967295 134512640 134672761 3221224576 3221223680 134560180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5347 4929 603 41 0 5306 0
vsize: 21388
[startup+290.012 s]
Raw data (loadavg): 1.01 0.99 0.90 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4951 0 0 0 28985 17 0 0 25 0 1 0 478698105 21901312 4929 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5347 4929 603 41 0 5306 0
vsize: 21388
[startup+300.012 s]
Raw data (loadavg): 1.00 0.99 0.90 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4951 0 0 0 29985 17 0 0 25 0 1 0 478698105 21901312 4929 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5347 4929 603 41 0 5306 0
vsize: 21388
[startup+310.012 s]
Raw data (loadavg): 1.00 0.99 0.90 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4951 0 0 0 30984 17 0 0 25 0 1 0 478698105 21901312 4929 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5347 4929 603 41 0 5306 0
vsize: 21388
[startup+320.013 s]
Raw data (loadavg): 1.00 0.99 0.90 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4951 0 0 0 31984 17 0 0 25 0 1 0 478698105 21901312 4929 4294967295 134512640 134672761 3221224576 3221223680 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4929 603 41 0 5306 0
vsize: 21388
[startup+330.013 s]
Raw data (loadavg): 1.00 0.99 0.90 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4951 0 0 0 32985 17 0 0 25 0 1 0 478698105 21901312 4929 4294967295 134512640 134672761 3221224576 3221223744 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4929 603 41 0 5306 0
vsize: 21388
[startup+340.013 s]
Raw data (loadavg): 1.00 0.99 0.90 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4951 0 0 0 33985 17 0 0 25 0 1 0 478698105 21901312 4929 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4929 603 41 0 5306 0
vsize: 21388
[startup+350.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4951 0 0 0 34985 17 0 0 25 0 1 0 478698105 21901312 4929 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4929 603 41 0 5306 0
vsize: 21388
[startup+360.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4951 0 0 0 35985 17 0 0 25 0 1 0 478698105 21901312 4929 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4929 603 41 0 5306 0
vsize: 21388
[startup+370.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4951 0 0 0 36985 17 0 0 25 0 1 0 478698105 21901312 4929 4294967295 134512640 134672761 3221224576 3221223680 134560347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4929 603 41 0 5306 0
vsize: 21388
[startup+380.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4951 0 0 0 37986 17 0 0 25 0 1 0 478698105 21901312 4929 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4929 603 41 0 5306 0
vsize: 21388
[startup+390.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4951 0 0 0 38985 17 0 0 25 0 1 0 478698105 21901312 4929 4294967295 134512640 134672761 3221224576 3221223680 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4929 603 41 0 5306 0
vsize: 21388
[startup+400.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4952 0 0 0 39986 18 0 0 25 0 1 0 478698105 21901312 4930 4294967295 134512640 134672761 3221224576 3221223584 134565745 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4930 603 41 0 5306 0
vsize: 21388
[startup+410.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4952 0 0 0 40986 18 0 0 25 0 1 0 478698105 21901312 4930 4294967295 134512640 134672761 3221224576 3221223728 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4930 603 41 0 5306 0
vsize: 21388
[startup+420.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4952 0 0 0 41986 18 0 0 25 0 1 0 478698105 21901312 4930 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4930 603 41 0 5306 0
vsize: 21388
[startup+430.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4952 0 0 0 42986 18 0 0 25 0 1 0 478698105 21901312 4930 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4930 603 41 0 5306 0
vsize: 21388
[startup+440.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4952 0 0 0 43986 18 0 0 25 0 1 0 478698105 21901312 4930 4294967295 134512640 134672761 3221224576 3221223760 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4930 603 41 0 5306 0
vsize: 21388
[startup+450.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4952 0 0 0 44986 18 0 0 25 0 1 0 478698105 21901312 4930 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4930 603 41 0 5306 0
vsize: 21388
[startup+460.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4952 0 0 0 45986 18 0 0 25 0 1 0 478698105 21901312 4930 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4930 603 41 0 5306 0
vsize: 21388
[startup+470.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4952 0 0 0 46986 18 0 0 25 0 1 0 478698105 21901312 4930 4294967295 134512640 134672761 3221224576 3221222896 134565829 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4930 603 41 0 5306 0
vsize: 21388
[startup+480.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4952 0 0 0 47987 18 0 0 25 0 1 0 478698105 21901312 4930 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4930 603 41 0 5306 0
vsize: 21388
[startup+490.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4952 0 0 0 48987 18 0 0 25 0 1 0 478698105 21901312 4930 4294967295 134512640 134672761 3221224576 3221223744 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4930 603 41 0 5306 0
vsize: 21388
[startup+500.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4952 0 0 0 49987 18 0 0 25 0 1 0 478698105 21901312 4930 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4930 603 41 0 5306 0
vsize: 21388
[startup+510.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4952 0 0 0 50987 18 0 0 25 0 1 0 478698105 21901312 4930 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4930 603 41 0 5306 0
vsize: 21388
[startup+520.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4952 0 0 0 51987 18 0 0 25 0 1 0 478698105 21901312 4930 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4930 603 41 0 5306 0
vsize: 21388
[startup+530.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4952 0 0 0 52987 19 0 0 25 0 1 0 478698105 21901312 4930 4294967295 134512640 134672761 3221224576 3221223760 134558918 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4930 603 41 0 5306 0
vsize: 21388
[startup+540.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4952 0 0 0 53987 19 0 0 25 0 1 0 478698105 21901312 4930 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4930 603 41 0 5306 0
vsize: 21388
[startup+550.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 4952 0 0 0 54988 19 0 0 25 0 1 0 478698105 21901312 4930 4294967295 134512640 134672761 3221224576 3221223760 134559345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5347 4930 603 41 0 5306 0
vsize: 21388
[startup+560.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22813
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5037 0 0 0 55987 19 0 0 25 0 1 0 478698105 22302720 5015 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5445 5015 603 41 0 5404 0
vsize: 21780
[startup+570.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5056 0 0 0 56987 19 0 0 25 0 1 0 478698105 22302720 5034 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5445 5034 603 41 0 5404 0
vsize: 21780
[startup+580.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5753 0 0 0 57985 22 0 0 25 0 1 0 478698105 25264128 5731 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6168 5731 603 41 0 6127 0
vsize: 24672
[startup+590.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5760 0 0 0 58985 22 0 0 25 0 1 0 478698105 25264128 5738 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6168 5738 603 41 0 6127 0
vsize: 24672
[startup+600.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5766 0 0 0 59985 22 0 0 25 0 1 0 478698105 25264128 5744 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6168 5744 603 41 0 6127 0
vsize: 24672
[startup+610.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5766 0 0 0 60985 22 0 0 25 0 1 0 478698105 25264128 5744 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6168 5744 603 41 0 6127 0
vsize: 24672
[startup+620.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5766 0 0 0 61985 22 0 0 25 0 1 0 478698105 25264128 5744 4294967295 134512640 134672761 3221224576 3221223680 134560335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6168 5744 603 41 0 6127 0
vsize: 24672
[startup+630.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5766 0 0 0 62986 22 0 0 25 0 1 0 478698105 25264128 5744 4294967295 134512640 134672761 3221224576 3221223744 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6168 5744 603 41 0 6127 0
vsize: 24672
[startup+640.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5766 0 0 0 63986 22 0 0 25 0 1 0 478698105 25264128 5744 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6168 5744 603 41 0 6127 0
vsize: 24672
[startup+650.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5767 0 0 0 64985 22 0 0 25 0 1 0 478698105 25264128 5745 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6168 5745 603 41 0 6127 0
vsize: 24672
[startup+660.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5767 0 0 0 65986 22 0 0 25 0 1 0 478698105 25264128 5745 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6168 5745 603 41 0 6127 0
vsize: 24672
[startup+670.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5767 0 0 0 66986 22 0 0 25 0 1 0 478698105 25264128 5745 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6168 5745 603 41 0 6127 0
vsize: 24672
[startup+680.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5767 0 0 0 67986 22 0 0 25 0 1 0 478698105 25264128 5745 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6168 5745 603 41 0 6127 0
vsize: 24672
[startup+690.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5767 0 0 0 68986 22 0 0 25 0 1 0 478698105 25264128 5745 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6168 5745 603 41 0 6127 0
vsize: 24672
[startup+700.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5769 0 0 0 69986 23 0 0 25 0 1 0 478698105 25264128 5747 4294967295 134512640 134672761 3221224576 3221223680 134560285 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6168 5747 603 41 0 6127 0
vsize: 24672
[startup+710.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5769 0 0 0 70985 23 0 0 25 0 1 0 478698105 25264128 5747 4294967295 134512640 134672761 3221224576 3221223760 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6168 5747 603 41 0 6127 0
vsize: 24672
[startup+720.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5769 0 0 0 71986 23 0 0 25 0 1 0 478698105 25264128 5747 4294967295 134512640 134672761 3221224576 3221223760 134559334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6168 5747 603 41 0 6127 0
vsize: 24672
[startup+730.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5769 0 0 0 72986 23 0 0 25 0 1 0 478698105 25264128 5747 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6168 5747 603 41 0 6127 0
vsize: 24672
[startup+740.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5769 0 0 0 73986 23 0 0 25 0 1 0 478698105 25264128 5747 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6168 5747 603 41 0 6127 0
vsize: 24672
[startup+750.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5769 0 0 0 74986 23 0 0 25 0 1 0 478698105 25264128 5747 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6168 5747 603 41 0 6127 0
vsize: 24672
[startup+760.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5805 0 0 0 75986 23 0 0 25 0 1 0 478698105 25399296 5783 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6201 5783 603 41 0 6160 0
vsize: 24804
[startup+770.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5805 0 0 0 76986 23 0 0 25 0 1 0 478698105 25399296 5783 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6201 5783 603 41 0 6160 0
vsize: 24804
[startup+780.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 5808 0 0 0 77986 23 0 0 25 0 1 0 478698105 25399296 5786 4294967295 134512640 134672761 3221224576 3221223760 134559572 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6201 5786 603 41 0 6160 0
vsize: 24804
[startup+790.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6021 0 0 0 78986 24 0 0 25 0 1 0 478698105 26345472 5999 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6432 5999 603 41 0 6391 0
vsize: 25728
[startup+800.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6023 0 0 0 79987 24 0 0 25 0 1 0 478698105 26345472 6001 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6432 6001 603 41 0 6391 0
vsize: 25728
[startup+810.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6031 0 0 0 80986 24 0 0 25 0 1 0 478698105 26345472 6009 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6432 6009 603 41 0 6391 0
vsize: 25728
[startup+820.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6367 0 0 0 81986 24 0 0 25 0 1 0 478698105 27688960 6345 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6760 6345 603 41 0 6719 0
vsize: 27040
[startup+830.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6367 0 0 0 82986 25 0 0 25 0 1 0 478698105 27688960 6345 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6760 6345 603 41 0 6719 0
vsize: 27040
[startup+840.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6367 0 0 0 83986 25 0 0 25 0 1 0 478698105 27688960 6345 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6760 6345 603 41 0 6719 0
vsize: 27040
[startup+850.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6367 0 0 0 84986 25 0 0 25 0 1 0 478698105 27688960 6345 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6760 6345 603 41 0 6719 0
vsize: 27040
[startup+860.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22815
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6385 0 0 0 85986 25 0 0 25 0 1 0 478698105 27824128 6363 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6793 6363 603 41 0 6752 0
vsize: 27172
[startup+870.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6385 0 0 0 86987 25 0 0 25 0 1 0 478698105 27824128 6363 4294967295 134512640 134672761 3221224576 3221223680 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6793 6363 603 41 0 6752 0
vsize: 27172
[startup+880.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6385 0 0 0 87987 25 0 0 25 0 1 0 478698105 27824128 6363 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6793 6363 603 41 0 6752 0
vsize: 27172
[startup+890.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6406 0 0 0 88987 25 0 0 25 0 1 0 478698105 27824128 6384 4294967295 134512640 134672761 3221224576 3221223680 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6793 6384 603 41 0 6752 0
vsize: 27172
[startup+900.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6406 0 0 0 89987 25 0 0 25 0 1 0 478698105 27824128 6384 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6793 6384 603 41 0 6752 0
vsize: 27172
[startup+910.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6406 0 0 0 90987 25 0 0 25 0 1 0 478698105 27824128 6384 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6793 6384 603 41 0 6752 0
vsize: 27172
[startup+920.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6413 0 0 0 91987 25 0 0 25 0 1 0 478698105 27987968 6391 4294967295 134512640 134672761 3221224576 3221223680 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6391 603 41 0 6792 0
vsize: 27332
[startup+930.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6425 0 0 0 92987 25 0 0 25 0 1 0 478698105 27987968 6403 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6403 603 41 0 6792 0
vsize: 27332
[startup+940.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6425 0 0 0 93987 25 0 0 25 0 1 0 478698105 27987968 6403 4294967295 134512640 134672761 3221224576 3221223680 134560301 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6403 603 41 0 6792 0
vsize: 27332
[startup+950.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6425 0 0 0 94988 25 0 0 25 0 1 0 478698105 27987968 6403 4294967295 134512640 134672761 3221224576 3221223680 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6403 603 41 0 6792 0
vsize: 27332
[startup+960.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6425 0 0 0 95987 25 0 0 25 0 1 0 478698105 27987968 6403 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6403 603 41 0 6792 0
vsize: 27332
[startup+970.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6425 0 0 0 96987 25 0 0 25 0 1 0 478698105 27987968 6403 4294967295 134512640 134672761 3221224576 3221223680 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6403 603 41 0 6792 0
vsize: 27332
[startup+980.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6425 0 0 0 97987 25 0 0 25 0 1 0 478698105 27987968 6403 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6403 603 41 0 6792 0
vsize: 27332
[startup+990.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6425 0 0 0 98987 26 0 0 25 0 1 0 478698105 27987968 6403 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6403 603 41 0 6792 0
vsize: 27332
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6425 0 0 0 99987 26 0 0 25 0 1 0 478698105 27987968 6403 4294967295 134512640 134672761 3221224576 3221223680 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6403 603 41 0 6792 0
vsize: 27332
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6425 0 0 0 100987 26 0 0 25 0 1 0 478698105 27987968 6403 4294967295 134512640 134672761 3221224576 3221223680 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6403 603 41 0 6792 0
vsize: 27332
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6425 0 0 0 101987 26 0 0 25 0 1 0 478698105 27987968 6403 4294967295 134512640 134672761 3221224576 3221223728 134565119 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6403 603 41 0 6792 0
vsize: 27332
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6426 0 0 0 102988 26 0 0 25 0 1 0 478698105 27987968 6404 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6404 603 41 0 6792 0
vsize: 27332
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6426 0 0 0 103988 26 0 0 25 0 1 0 478698105 27987968 6404 4294967295 134512640 134672761 3221224576 3221223680 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6404 603 41 0 6792 0
vsize: 27332
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6426 0 0 0 104988 26 0 0 25 0 1 0 478698105 27987968 6404 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6404 603 41 0 6792 0
vsize: 27332
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6426 0 0 0 105988 26 0 0 25 0 1 0 478698105 27987968 6404 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6404 603 41 0 6792 0
vsize: 27332
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6426 0 0 0 106988 26 0 0 25 0 1 0 478698105 27987968 6404 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6404 603 41 0 6792 0
vsize: 27332
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6426 0 0 0 107988 26 0 0 25 0 1 0 478698105 27987968 6404 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6404 603 41 0 6792 0
vsize: 27332
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6426 0 0 0 108989 26 0 0 25 0 1 0 478698105 27987968 6404 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6404 603 41 0 6792 0
vsize: 27332
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6426 0 0 0 109989 26 0 0 25 0 1 0 478698105 27987968 6404 4294967295 134512640 134672761 3221224576 3221223760 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6404 603 41 0 6792 0
vsize: 27332
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6426 0 0 0 110989 26 0 0 25 0 1 0 478698105 27987968 6404 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6404 603 41 0 6792 0
vsize: 27332
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6426 0 0 0 111989 26 0 0 25 0 1 0 478698105 27987968 6404 4294967295 134512640 134672761 3221224576 3221223700 134566052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6404 603 41 0 6792 0
vsize: 27332
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6426 0 0 0 112989 27 0 0 25 0 1 0 478698105 27987968 6404 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6404 603 41 0 6792 0
vsize: 27332
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6426 0 0 0 113989 27 0 0 25 0 1 0 478698105 27987968 6404 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6404 603 41 0 6792 0
vsize: 27332
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6426 0 0 0 114989 27 0 0 25 0 1 0 478698105 27987968 6404 4294967295 134512640 134672761 3221224576 3221223680 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6404 603 41 0 6792 0
vsize: 27332
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22817
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6426 0 0 0 115989 27 0 0 25 0 1 0 478698105 27987968 6404 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6404 603 41 0 6792 0
vsize: 27332
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22819
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6426 0 0 0 116989 27 0 0 25 0 1 0 478698105 27987968 6404 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6404 603 41 0 6792 0
vsize: 27332
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22819
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6426 0 0 0 117990 27 0 0 25 0 1 0 478698105 27987968 6404 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6404 603 41 0 6792 0
vsize: 27332
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22819
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6426 0 0 0 118990 27 0 0 25 0 1 0 478698105 27987968 6404 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6404 603 41 0 6792 0
vsize: 27332
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 22819
Raw data (stat): 22811 (minisat+) R 22810 20024 20023 0 -1 0 6426 0 0 0 119990 27 0 0 25 0 1 0 478698105 27987968 6404 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 6404 603 41 0 6792 0
vsize: 27332
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 1/55 22819
Raw data (stat): 22811 (minisat+) Z 22810 20024 20023 0 -1 12 6429 0 0 0 119990 29 0 0 25 0 1 0 478698105 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.19
CPU user time (s): 1199.9
CPU system time (s): 0.290955
CPU usage (%): 100.011
Max. virtual memory (Kb): 27332
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####