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/logic-synthesis/normalized-alu4.b.opb
MD5SUM	db06e7fbd4f70a4af68f8f196fdb3636
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	50
Optimality of the best value was proved	NO
Number of terms in the objective function	808
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	808
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	808
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.03884
Number of variables	807
Total number of constraints	1838
Number of constraints which are clauses	1823
Number of constraints which are cardinality constraints (but not clauses)	15
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	98
Trace number 5409

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-13 23:46:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3821 boxname=wulflinc13 idbench=61 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  db06e7fbd4f70a4af68f8f196fdb3636  /oldhome/oroussel/tmp/wulflinc13/normalized-alu4.b.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc13/normalized-alu4.b.opb /oldhome/oroussel/tmp/wulflinc13/normalized-alu4.b.opb
IDLAUNCH: 3821
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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	: 2
cpu MHz		: 451.242
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        906384 kB
Buffers:         34652 kB
Cached:          73824 kB
SwapCached:        392 kB
Active:          53864 kB
Inactive:        57856 kB
HighTotal:      131008 kB
HighFree:        53228 kB
LowTotal:       903652 kB
LowFree:        853156 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10952 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:06:55 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 3821 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1695 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    1518    32515 |     455       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  451/451          
c |         0 |     811    18349 |      --       0       --      -- |     --   | -707/-14166
c |         0 |     811    18349 |     324       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.367944 s)
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:36470     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   41642   113578 |   12492       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/27483          
c   -- var.elim.:  2000/27483          
c   -- var.elim.:  3000/27483          
c   -- var.elim.:  4000/27483          
c   -- var.elim.:  5000/27483          
c   -- var.elim.:  6000/27483          
c   -- var.elim.:  7000/27483          
c   -- var.elim.:  8000/27483          
c   -- var.elim.:  9000/27483          
c   -- var.elim.:  10000/27483          
c   -- var.elim.:  11000/27483          
c   -- var.elim.:  12000/27483          
c   -- var.elim.:  13000/27483          
c   -- var.elim.:  14000/27483          
c   -- var.elim.:  15000/27483          
c   -- var.elim.:  16000/27483          
c   -- var.elim.:  17000/27483          
c   -- var.elim.:  18000/27483          
c   -- var.elim.:  19000/27483          
c   -- var.elim.:  20000/27483          
c   -- var.elim.:  21000/27483          
c   -- var.elim.:  22000/27483          
c   -- var.elim.:  23000/27483          
c   -- var.elim.:  24000/27483          
c   -- var.elim.:  25000/27483          
c   -- var.elim.:  26000/27483          
c   -- var.elim.:  27000/27483          
c   -- var.elim.:  27483/27483          
c   -- var.elim.:  1000/13691          
c   -- var.elim.:  2000/13691          
c   -- var.elim.:  3000/13691          
c   -- var.elim.:  4000/13691          
c   -- var.elim.:  5000/13691          
c   -- var.elim.:  6000/13691          
c   -- var.elim.:  7000/13691          
c   -- var.elim.:  8000/13691          
c   -- var.elim.:  9000/13691          
c   -- var.elim.:  10000/13691          
c   -- var.elim.:  11000/13691          
c   -- var.elim.:  12000/13691          
c   -- var.elim.:  13000/13691          
c   -- var.elim.:  13691/13691          
c   -- var.elim.:  760/760          
c   -- var.elim.:  270/270          
c   -- subsuming                       
c   -- var.elim.:  1000/11409          
c   -- var.elim.:  2000/11409          
c   -- var.elim.:  3000/11409          
c   -- var.elim.:  4000/11409          
c   -- var.elim.:  5000/11409          
c   -- var.elim.:  6000/11409          
c   -- var.elim.:  7000/11409          
c   -- var.elim.:  8000/11409          
c   -- var.elim.:  9000/11409          
c   -- var.elim.:  10000/11409          
c   -- var.elim.:  11000/11409          
c   -- var.elim.:  11409/11409          
c   -- var.elim.:  70/70          
c |         0 |   27994   208272 |      --       0       --      -- |     --   | -13564/94933
c |         0 |   27994   208272 |   11197       0        0     nan |  0.000 % |
c |       101 |   27844   207186 |   12251      95     4535    47.7 |  1.123 % |
c |       251 |   27842   207169 |   13475     244    13653    56.0 |  1.130 % |
c |       476 |   27842   207169 |   14823     469    25041    53.4 |  1.130 % |
c ==============================================================================
c (current CPU-time: 33.058 s)
c ==============================================================================
c [1mFound solution: 58[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       752 |   28403   208161 |    8520     744    35202    47.3 |  1.130 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2440          
c   -- var.elim.:  2000/2440          
c   -- var.elim.:  2440/2440          
c   -- var.elim.:  678/678          
c   -- var.elim.:  168/168          
c   -- var.elim.:  33/33          
c   -- var.elim.:  200/200          
c   -- subsuming                       
c   -- var.elim.:  35/35          
c |       752 |   27947   207628 |      --     744       --      -- |     --   | -445/-400
c |       752 |   27947   207628 |   11178     733    32982    45.0 |  1.130 % |
c |       852 |   27947   207628 |   12296     833    47265    56.7 |  1.247 % |
c |      1003 |   27947   207628 |   13526     984    63481    64.5 |  1.247 % |
c |      1228 |   27947   207628 |   14878    1209    75691    62.6 |  1.247 % |
c |      1566 |   27947   207628 |   16366    1547   111294    71.9 |  1.247 % |
c |      2072 |   27947   207628 |   18003    2053   137582    67.0 |  1.247 % |
c |      2831 |   27934   207514 |   19794    2810   209004    74.4 |  1.290 % |
c |      3970 |   27934   207514 |   21774    3949   374065    94.7 |  1.290 % |
c |      5683 |   27934   207514 |   23951    5662   587790   103.8 |  1.290 % |
c |      8245 |   27934   207514 |   26346    8224  1186748   144.3 |  1.290 % |
c ==============================================================================
c (current CPU-time: 47.5538 s)
c ==============================================================================
c [1mFound solution: 55[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      9900 |   28464   209004 |    8539    9879  1342196   135.9 |  1.290 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1309          
c   -- var.elim.:  1309/1309          
c   -- var.elim.:  506/506          
c   -- var.elim.:  72/72          
c   -- var.elim.:  251/251          
c |      9900 |   28002   208022 |      --    9879       --      -- |     --   | -462/-981
c |      9900 |   28002   208022 |   11200    9878  1342194   135.9 |  1.290 % |
c |     10001 |   28002   208022 |   12320    9979  1351544   135.4 |  1.311 % |
c |     10153 |   28002   208022 |   13552   10131  1365934   134.8 |  1.311 % |
c |     10379 |   28002   208022 |   14908   10357  1374510   132.7 |  1.311 % |
c |     10716 |   28002   208022 |   16399   10694  1400465   131.0 |  1.311 % |
c |     11223 |   28002   208022 |   18039   11201  1434127   128.0 |  1.311 % |
c |     11982 |   28002   208022 |   19842   11960  1498585   125.3 |  1.311 % |
c |     13122 |   28002   208022 |   21827   13100  1608984   122.8 |  1.311 % |
c |     14830 |   28002   208022 |   24009   14808  1721922   116.3 |  1.311 % |
c |     17393 |   28002   208022 |   26410   17371  2063834   118.8 |  1.311 % |
c |     21239 |   28002   208022 |   29051   21217  2725694   128.5 |  1.311 % |
c ==============================================================================
c (current CPU-time: 73.6428 s)
c ==============================================================================
c [1mFound solution: 52[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     23396 |   28404   209176 |    8521   23374  2989713   127.9 |  1.311 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1652          
c   -- var.elim.:  1652/1652          
c   -- var.elim.:  1000/1700          
c   -- var.elim.:  1700/1700          
c   -- var.elim.:  223/223          
c   -- var.elim.:  305/305          
c   -- subsuming                       
c   -- var.elim.:  204/204          
c |     23396 |   27747   205830 |      --   23374       --      -- |     --   | -415/-78
c |     23396 |   27747   205830 |   11098   21709  2582583   119.0 |  1.311 % |
c |     23497 |   27747   205830 |   12208    7889  1084787   137.5 |  1.634 % |
c |     23649 |   27747   205830 |   13429    8041  1093775   136.0 |  1.634 % |
c |     23875 |   27747   205830 |   14772    8267  1105282   133.7 |  1.634 % |
c |     24212 |   27747   205830 |   16249    8604  1116720   129.8 |  1.634 % |
c |     24718 |   27747   205830 |   17874    9110  1157637   127.1 |  1.634 % |
c |     25477 |   27747   205830 |   19662    9869  1185553   120.1 |  1.634 % |
c |     26620 |   27747   205830 |   21628   11012  1273266   115.6 |  1.634 % |
c |     28329 |   27747   205830 |   23791   12721  1493696   117.4 |  1.634 % |
c |     30891 |   27747   205830 |   26170   15283  1760694   115.2 |  1.634 % |
c |     34737 |   27747   205830 |   28787   19129  2220661   116.1 |  1.634 % |
c |     40503 |   27747   205830 |   31666   24895  2979418   119.7 |  1.634 % |
c |     49153 |   27747   205830 |   34832   33545  4411429   131.5 |  1.634 % |
c |     62127 |   27745   205810 |   38313   21523  3187621   148.1 |  1.641 % |
c |     81588 |   27745   205810 |   42144   14560  1859021   127.7 |  1.641 % |
c |    110780 |   27745   205810 |   46359   43752  6024592   137.7 |  1.641 % |
c |    154569 |   27745   205810 |   50995   52809 15394527   291.5 |  1.641 % |
c |    220254 |   27745   205810 |   56094   43171  6624744   153.5 |  1.641 % |
c |    318783 |   27745   205810 |   61703   57132  9421619   164.9 |  1.641 % |
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 -x60#### 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.80 0.92 0.89 2/54 3872
Raw data (stat): 3872 (runsolver) R 3871 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421805175 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.0003 s]
Raw data (loadavg): 0.83 0.93 0.90 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 3988 0 0 0 985 14 0 0 25 0 1 0 421805175 19267584 3963 4294967295 134512640 134672761 3221224576 3221223024 134643683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4704 3963 603 41 0 4663 0
vsize: 18816
[startup+20.001 s]
Raw data (loadavg): 0.85 0.93 0.90 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 3988 0 0 0 1984 14 0 0 25 0 1 0 421805175 19267584 3963 4294967295 134512640 134672761 3221224576 3221223136 134607908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4704 3963 603 41 0 4663 0
vsize: 18816
[startup+30.0011 s]
Raw data (loadavg): 0.88 0.93 0.90 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 4029 0 0 0 2983 14 0 0 25 0 1 0 421805175 19267584 3963 4294967295 134512640 134672761 3221224576 3221223024 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4704 3963 603 41 0 4663 0
vsize: 18816
[startup+40.0011 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 5403 0 0 0 3978 19 0 0 25 0 1 0 421805175 21254144 4455 4294967295 134512640 134672761 3221224576 3221223760 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5189 4455 603 41 0 5148 0
vsize: 20756
[startup+50.0015 s]
Raw data (loadavg): 0.91 0.93 0.90 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 7299 0 0 0 4971 26 0 0 25 0 1 0 421805175 25575424 5526 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6244 5526 603 41 0 6203 0
vsize: 24976
[startup+60.0012 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 7762 0 0 0 5969 27 0 0 25 0 1 0 421805175 27561984 5989 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6729 5989 603 41 0 6688 0
vsize: 26916
[startup+70.0011 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 8656 0 0 0 6966 30 0 0 25 0 1 0 421805175 31223808 6883 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7623 6883 603 41 0 7582 0
vsize: 30492
[startup+80.002 s]
Raw data (loadavg): 0.94 0.94 0.90 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 9819 0 0 0 7962 33 0 0 25 0 1 0 421805175 33570816 7481 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8196 7481 603 41 0 8155 0
vsize: 32784
[startup+90.002 s]
Raw data (loadavg): 0.95 0.94 0.90 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 9819 0 0 0 8963 33 0 0 25 0 1 0 421805175 33570816 7481 4294967295 134512640 134672761 3221224576 3221223728 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8196 7481 603 41 0 8155 0
vsize: 32784
[startup+100.003 s]
Raw data (loadavg): 0.96 0.94 0.90 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 9819 0 0 0 9963 33 0 0 25 0 1 0 421805175 33570816 7481 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8196 7481 603 41 0 8155 0
vsize: 32784
[startup+110.004 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 10061 0 0 0 10962 35 0 0 25 0 1 0 421805175 34627584 7723 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8454 7723 603 41 0 8413 0
vsize: 33816
[startup+120.003 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 10948 0 0 0 11959 37 0 0 25 0 1 0 421805175 38195200 8610 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9325 8610 603 41 0 9284 0
vsize: 37300
[startup+130.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 11523 0 0 0 12958 39 0 0 25 0 1 0 421805175 40710144 9185 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9939 9185 603 41 0 9898 0
vsize: 39756
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 11708 0 0 0 13958 39 0 0 25 0 1 0 421805175 41644032 9370 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10167 9370 603 41 0 10126 0
vsize: 40668
[startup+150.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 11708 0 0 0 14958 39 0 0 25 0 1 0 421805175 41644032 9370 4294967295 134512640 134672761 3221224576 3221223760 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10167 9370 603 41 0 10126 0
vsize: 40668
[startup+160.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 11708 0 0 0 15958 39 0 0 25 0 1 0 421805175 41644032 9370 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10167 9370 603 41 0 10126 0
vsize: 40668
[startup+170.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 11708 0 0 0 16958 39 0 0 25 0 1 0 421805175 41644032 9370 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10167 9370 603 41 0 10126 0
vsize: 40668
[startup+180.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 11708 0 0 0 17958 39 0 0 25 0 1 0 421805175 41644032 9370 4294967295 134512640 134672761 3221224576 3221223760 134615679 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10167 9370 603 41 0 10126 0
vsize: 40668
[startup+190.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 11863 0 0 0 18958 40 0 0 25 0 1 0 421805175 42172416 9525 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10296 9525 603 41 0 10255 0
vsize: 41184
[startup+200.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 12215 0 0 0 19958 41 0 0 25 0 1 0 421805175 43499520 9877 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10620 9877 603 41 0 10579 0
vsize: 42480
[startup+210.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 12596 0 0 0 20957 42 0 0 25 0 1 0 421805175 45121536 10258 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11016 10258 603 41 0 10975 0
vsize: 44064
[startup+220.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 12839 0 0 0 21956 43 0 0 25 0 1 0 421805175 45895680 10462 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11205 10462 603 41 0 11164 0
vsize: 44820
[startup+230.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 12839 0 0 0 22956 43 0 0 25 0 1 0 421805175 45895680 10462 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11205 10462 603 41 0 11164 0
vsize: 44820
[startup+240.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 12839 0 0 0 23956 43 0 0 25 0 1 0 421805175 45895680 10462 4294967295 134512640 134672761 3221224576 3221223760 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11205 10462 603 41 0 11164 0
vsize: 44820
[startup+250.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 12840 0 0 0 24956 43 0 0 25 0 1 0 421805175 45895680 10463 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11205 10463 603 41 0 11164 0
vsize: 44820
[startup+260.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 12840 0 0 0 25956 43 0 0 25 0 1 0 421805175 45895680 10463 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11205 10463 603 41 0 11164 0
vsize: 44820
[startup+270.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 12840 0 0 0 26957 43 0 0 25 0 1 0 421805175 45895680 10463 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11205 10463 603 41 0 11164 0
vsize: 44820
[startup+280.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 12841 0 0 0 27957 43 0 0 25 0 1 0 421805175 45895680 10464 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11205 10464 603 41 0 11164 0
vsize: 44820
[startup+290.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 13149 0 0 0 28955 45 0 0 25 0 1 0 421805175 47222784 10772 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11529 10772 603 41 0 11488 0
vsize: 46116
[startup+300.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 13770 0 0 0 29954 46 0 0 25 0 1 0 421805175 49741824 11393 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12144 11393 603 41 0 12103 0
vsize: 48576
[startup+310.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 14534 0 0 0 30953 48 0 0 25 0 1 0 421805175 52748288 12109 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12878 12109 603 41 0 12837 0
vsize: 51512
[startup+320.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 14534 0 0 0 31953 48 0 0 25 0 1 0 421805175 52748288 12109 4294967295 134512640 134672761 3221224576 3221223760 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12878 12109 603 41 0 12837 0
vsize: 51512
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 14534 0 0 0 32953 48 0 0 25 0 1 0 421805175 52748288 12109 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12878 12109 603 41 0 12837 0
vsize: 51512
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 14534 0 0 0 33953 48 0 0 25 0 1 0 421805175 52748288 12109 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12878 12109 603 41 0 12837 0
vsize: 51512
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 14875 0 0 0 34952 49 0 0 25 0 1 0 421805175 54206464 12450 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12450 603 41 0 13193 0
vsize: 52936
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 15720 0 0 0 35950 51 0 0 25 0 1 0 421805175 57618432 13295 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14067 13295 603 41 0 14026 0
vsize: 56268
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 16472 0 0 0 36948 53 0 0 25 0 1 0 421805175 60784640 14047 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14840 14047 603 41 0 14799 0
vsize: 59360
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 17266 0 0 0 37947 55 0 0 25 0 1 0 421805175 64012288 14841 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15628 14841 603 41 0 15587 0
vsize: 62512
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 17986 0 0 0 38944 57 0 0 25 0 1 0 421805175 67088384 15561 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16379 15561 603 41 0 16338 0
vsize: 65516
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 18631 0 0 0 39942 60 0 0 25 0 1 0 421805175 69730304 16206 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17024 16206 603 41 0 16983 0
vsize: 68096
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 19293 0 0 0 40940 62 0 0 25 0 1 0 421805175 72396800 16868 4294967295 134512640 134672761 3221224576 3221223760 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17675 16868 603 41 0 17634 0
vsize: 70700
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 19923 0 0 0 41940 63 0 0 25 0 1 0 421805175 75038720 17498 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18320 17498 603 41 0 18279 0
vsize: 73280
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 20546 0 0 0 42938 65 0 0 25 0 1 0 421805175 77537280 18121 4294967295 134512640 134672761 3221224576 3221223616 134612981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18930 18121 603 41 0 18889 0
vsize: 75720
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 21142 0 0 0 43937 66 0 0 25 0 1 0 421805175 80027648 18717 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18717 603 41 0 19497 0
vsize: 78152
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 21616 0 0 0 44935 68 0 0 25 0 1 0 421805175 82001920 19191 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20020 19191 603 41 0 19979 0
vsize: 80080
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 22171 0 0 0 45934 70 0 0 25 0 1 0 421805175 84234240 19746 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20565 19746 603 41 0 20524 0
vsize: 82260
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 22730 0 0 0 46932 71 0 0 25 0 1 0 421805175 86519808 20305 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21123 20305 603 41 0 21082 0
vsize: 84492
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23264 0 0 0 47931 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23264 0 0 0 48931 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23264 0 0 0 49931 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+510.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23264 0 0 0 50931 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23264 0 0 0 51931 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23264 0 0 0 52932 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23264 0 0 0 53932 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223616 134614340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23264 0 0 0 54932 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23264 0 0 0 55932 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23264 0 0 0 56932 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23264 0 0 0 57933 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23264 0 0 0 58933 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+600.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23264 0 0 0 59933 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134616023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23264 0 0 0 60933 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+620.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23264 0 0 0 61933 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+630.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23316 0 0 0 62934 73 0 0 25 0 1 0 421805175 88715264 20839 4294967295 134512640 134672761 3221224576 3221223632 134644275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21659 20839 603 41 0 21618 0
vsize: 86636
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23316 0 0 0 63934 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+650.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23316 0 0 0 64934 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+660.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23316 0 0 0 65934 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+670.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23316 0 0 0 66934 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+680.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23316 0 0 0 67934 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+690.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23316 0 0 0 68935 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+700.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23316 0 0 0 69935 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+710.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23316 0 0 0 70935 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223616 134612981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+720.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23316 0 0 0 71935 73 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+730.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23316 0 0 0 72935 74 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+740.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23316 0 0 0 73935 74 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+750.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23316 0 0 0 74935 74 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+760.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23316 0 0 0 75935 74 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+770.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23316 0 0 0 76935 74 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+780.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23316 0 0 0 77936 74 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+790.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3872
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23316 0 0 0 78936 74 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+800.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3925
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23316 0 0 0 79931 77 0 0 25 0 1 0 421805175 88453120 20787 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20787 603 41 0 21554 0
vsize: 86380
[startup+810.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3925
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23319 0 0 0 80932 78 0 0 25 0 1 0 421805175 88453120 20790 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20790 603 41 0 21554 0
vsize: 86380
[startup+820.014 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 3925
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23327 0 0 0 81932 78 0 0 25 0 1 0 421805175 88453120 20798 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20798 603 41 0 21554 0
vsize: 86380
[startup+830.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3925
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23327 0 0 0 82932 78 0 0 25 0 1 0 421805175 88453120 20798 4294967295 134512640 134672761 3221224576 3221223776 134610669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20798 603 41 0 21554 0
vsize: 86380
[startup+840.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3925
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23327 0 0 0 83932 78 0 0 25 0 1 0 421805175 88453120 20798 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20798 603 41 0 21554 0
vsize: 86380
[startup+850.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3925
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23327 0 0 0 84932 78 0 0 25 0 1 0 421805175 88453120 20798 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20798 603 41 0 21554 0
vsize: 86380
[startup+860.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23327 0 0 0 85933 78 0 0 25 0 1 0 421805175 88453120 20798 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20798 603 41 0 21554 0
vsize: 86380
[startup+870.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23327 0 0 0 86933 78 0 0 25 0 1 0 421805175 88453120 20798 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20798 603 41 0 21554 0
vsize: 86380
[startup+880.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23327 0 0 0 87933 78 0 0 25 0 1 0 421805175 88453120 20798 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20798 603 41 0 21554 0
vsize: 86380
[startup+890.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23327 0 0 0 88933 78 0 0 25 0 1 0 421805175 88453120 20798 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20798 603 41 0 21554 0
vsize: 86380
[startup+900.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23327 0 0 0 89933 78 0 0 25 0 1 0 421805175 88453120 20798 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20798 603 41 0 21554 0
vsize: 86380
[startup+910.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23327 0 0 0 90934 78 0 0 25 0 1 0 421805175 88453120 20798 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20798 603 41 0 21554 0
vsize: 86380
[startup+920.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23327 0 0 0 91934 78 0 0 25 0 1 0 421805175 88453120 20798 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20798 603 41 0 21554 0
vsize: 86380
[startup+930.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23327 0 0 0 92934 78 0 0 25 0 1 0 421805175 88453120 20798 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20798 603 41 0 21554 0
vsize: 86380
[startup+940.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23327 0 0 0 93934 78 0 0 25 0 1 0 421805175 88453120 20798 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20798 603 41 0 21554 0
vsize: 86380
[startup+950.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23327 0 0 0 94934 78 0 0 25 0 1 0 421805175 88453120 20798 4294967295 134512640 134672761 3221224576 3221223776 134610622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20798 603 41 0 21554 0
vsize: 86380
[startup+960.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23327 0 0 0 95935 78 0 0 25 0 1 0 421805175 88453120 20798 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20798 603 41 0 21554 0
vsize: 86380
[startup+970.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23327 0 0 0 96935 78 0 0 25 0 1 0 421805175 88453120 20798 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20798 603 41 0 21554 0
vsize: 86380
[startup+980.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23328 0 0 0 97935 78 0 0 25 0 1 0 421805175 88453120 20799 4294967295 134512640 134672761 3221224576 3221223616 134603512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20799 603 41 0 21554 0
vsize: 86380
[startup+990.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23328 0 0 0 98935 78 0 0 25 0 1 0 421805175 88453120 20799 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20799 603 41 0 21554 0
vsize: 86380
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23328 0 0 0 99936 78 0 0 25 0 1 0 421805175 88453120 20799 4294967295 134512640 134672761 3221224576 3221222400 134645414 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20799 603 41 0 21554 0
vsize: 86380
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23328 0 0 0 100936 78 0 0 25 0 1 0 421805175 88453120 20799 4294967295 134512640 134672761 3221224576 3221223760 134615649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20799 603 41 0 21554 0
vsize: 86380
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23328 0 0 0 101936 78 0 0 25 0 1 0 421805175 88453120 20799 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20799 603 41 0 21554 0
vsize: 86380
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23328 0 0 0 102936 78 0 0 25 0 1 0 421805175 88453120 20799 4294967295 134512640 134672761 3221224576 3221223776 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20799 603 41 0 21554 0
vsize: 86380
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23328 0 0 0 103936 78 0 0 25 0 1 0 421805175 88453120 20799 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20799 603 41 0 21554 0
vsize: 86380
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23328 0 0 0 104936 78 0 0 25 0 1 0 421805175 88453120 20799 4294967295 134512640 134672761 3221224576 3221223776 134610709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20799 603 41 0 21554 0
vsize: 86380
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23328 0 0 0 105936 78 0 0 25 0 1 0 421805175 88453120 20799 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20799 603 41 0 21554 0
vsize: 86380
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23328 0 0 0 106937 78 0 0 25 0 1 0 421805175 88453120 20799 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20799 603 41 0 21554 0
vsize: 86380
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23328 0 0 0 107937 78 0 0 25 0 1 0 421805175 88453120 20799 4294967295 134512640 134672761 3221224576 3221223616 134613001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20799 603 41 0 21554 0
vsize: 86380
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23328 0 0 0 108937 78 0 0 25 0 1 0 421805175 88453120 20799 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20799 603 41 0 21554 0
vsize: 86380
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3927
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23328 0 0 0 109937 78 0 0 25 0 1 0 421805175 88453120 20799 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20799 603 41 0 21554 0
vsize: 86380
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3929
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23328 0 0 0 110937 78 0 0 25 0 1 0 421805175 88453120 20799 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20799 603 41 0 21554 0
vsize: 86380
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3929
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23328 0 0 0 111938 78 0 0 25 0 1 0 421805175 88453120 20799 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20799 603 41 0 21554 0
vsize: 86380
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3929
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23328 0 0 0 112938 78 0 0 25 0 1 0 421805175 88453120 20799 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20799 603 41 0 21554 0
vsize: 86380
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3929
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23328 0 0 0 113938 78 0 0 25 0 1 0 421805175 88453120 20799 4294967295 134512640 134672761 3221224576 3221223760 134615649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20799 603 41 0 21554 0
vsize: 86380
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3929
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23328 0 0 0 114938 78 0 0 25 0 1 0 421805175 88453120 20799 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20799 603 41 0 21554 0
vsize: 86380
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3929
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23328 0 0 0 115938 78 0 0 25 0 1 0 421805175 88453120 20799 4294967295 134512640 134672761 3221224576 3221223760 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20799 603 41 0 21554 0
vsize: 86380
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3929
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23328 0 0 0 116938 78 0 0 25 0 1 0 421805175 88453120 20799 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20799 603 41 0 21554 0
vsize: 86380
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3929
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23332 0 0 0 117939 78 0 0 25 0 1 0 421805175 88453120 20803 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20803 603 41 0 21554 0
vsize: 86380
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3929
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23336 0 0 0 118939 78 0 0 25 0 1 0 421805175 88453120 20807 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20807 603 41 0 21554 0
vsize: 86380
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3929
Raw data (stat): 3872 (minisat+) R 3871 30701 30700 0 -1 0 23336 0 0 0 119939 78 0 0 25 0 1 0 421805175 88453120 20807 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21595 20807 603 41 0 21554 0
vsize: 86380
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 3929
Raw data (stat): 3872 (minisat+) Z 3871 30701 30700 0 -1 12 23337 0 0 0 119939 82 0 0 25 0 1 0 421805175 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.22
CPU user time (s): 1199.39
CPU system time (s): 0.821875
CPU usage (%): 100.013
Max. virtual memory (Kb): 86636
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####