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-ii32e2.opb
MD5SUM	4e882bbd92f288daf6e68ac3de757136
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	235
Optimality of the best value was proved	NO
Number of terms in the objective function	534
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	534
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	534
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.03084
Number of variables	534
Total number of constraints	3013
Number of constraints which are clauses	3013
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	32
Trace number 6225

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-14 03:59:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4671 boxname=wulflinc29 idbench=159 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4e882bbd92f288daf6e68ac3de757136  /oldhome/oroussel/tmp/wulflinc29/normalized-ii32e2.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc29/normalized-ii32e2.opb /oldhome/oroussel/tmp/wulflinc29/normalized-ii32e2.opb
IDLAUNCH: 4671
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
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:        817240 kB
Buffers:         36784 kB
Cached:         142996 kB
SwapCached:         12 kB
Active:          64920 kB
Inactive:       117764 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        816988 kB
SwapTotal:     2097892 kB
SwapFree:      2097880 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            29024 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:11:35 (client local time) WITH STATUS 30 IN 738.697 SECONDS
stats: 4671 0 738.697 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3013 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 |    3013    12801 |    1004       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 262[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:23900     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        51 |   58582   142792 |   19527      51     2400    47.1 |  0.000 % |
c |       151 |   58582   142792 |   21479     151     7683    50.9 |  0.116 % |
c ==============================================================================
c [1mFound solution: 254[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       183 |   58777   143306 |   19592     183     9583    52.4 |  0.116 % |
c |       283 |   58627   142968 |   21551     280    16597    59.3 |  0.468 % |
c |       434 |   58257   142131 |   23706     425    27373    64.4 |  0.989 % |
c |       660 |   58176   141945 |   26076     650    43200    66.5 |  1.099 % |
c |       998 |   58040   141635 |   28684     986    66620    67.6 |  1.289 % |
c ==============================================================================
c [1mFound solution: 253[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1395 |   58022   141620 |   19340    1382    94266    68.2 |  1.289 % |
c |      1495 |   57863   141254 |   21274    1480   101369    68.5 |  1.645 % |
c |      1646 |   57745   140986 |   23401    1629   110718    68.0 |  1.824 % |
c |      1872 |   57670   140817 |   25741    1854   125545    67.7 |  1.929 % |
c |      2213 |   57583   140619 |   28315    2194   145002    66.1 |  2.060 % |
c |      2720 |   57583   140619 |   31147    2701   175564    65.0 |  2.060 % |
c |      3482 |   57100   139516 |   34261    3456   216088    62.5 |  2.786 % |
c ==============================================================================
c [1mFound solution: 252[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3592 |   56841   138916 |   18947    3564   221477    62.1 |  2.786 % |
c ==============================================================================
c [1mFound solution: 251[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3642 |   56958   139222 |   18986    3614   225488    62.4 |  2.786 % |
c |      3742 |   56958   139222 |   20884    3714   229345    61.8 |  3.159 % |
c |      3892 |   56367   137852 |   22973    3847   229965    59.8 |  4.197 % |
c |      4117 |   55146   135046 |   25270    4026   237624    59.0 |  6.023 % |
c |      4454 |   54677   133977 |   27797    4356   255755    58.7 |  6.747 % |
c |      4961 |   54293   133098 |   30577    4753   274542    57.8 |  7.361 % |
c |      5722 |   51206   126002 |   33634    5469   310148    56.7 | 12.346 % |
c ==============================================================================
c [1mFound solution: 250[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6446 |   51041   125608 |   17013    6191   353824    57.2 | 12.346 % |
c |      6547 |   51041   125608 |   18714    6292   360922    57.4 | 12.612 % |
c |      6697 |   50582   124553 |   20585    6437   369990    57.5 | 13.347 % |
c |      6924 |   44720   111059 |   22644    6324   363757    57.5 | 22.895 % |
c |      7265 |   44559   110687 |   24908    6662   379992    57.0 | 23.162 % |
c |      7771 |   44559   110687 |   27399    7168   411152    57.4 | 23.162 % |
c ==============================================================================
c [1mFound solution: 240[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7918 |   44821   111349 |   14940    7274   415891    57.2 | 23.162 % |
c |      8020 |   44821   111349 |   16434    7376   422353    57.3 | 23.128 % |
c ==============================================================================
c [1mFound solution: 239[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8055 |   44941   111660 |   14980    7411   424515    57.3 | 23.128 % |
c ==============================================================================
c [1mFound solution: 238[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8135 |   44601   110867 |   14867    7439   425174    57.2 | 23.128 % |
c |      8235 |   43856   109147 |   16353    7528   425704    56.5 | 24.979 % |
c |      8387 |   39366    98734 |   17989    7578   427890    56.5 | 32.194 % |
c |      8613 |   39167    98277 |   19787    7801   437760    56.1 | 32.501 % |
c |      8950 |   39167    98277 |   21766    8138   458388    56.3 | 32.501 % |
c |      9457 |   38874    97603 |   23943    8639   492279    57.0 | 32.975 % |
c ==============================================================================
c [1mFound solution: 237[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9691 |   38939    97774 |   12979    8873   508459    57.3 | 32.975 % |
c |      9791 |   36899    93043 |   14276    8904   508525    57.1 | 36.425 % |
c |      9942 |   36423    91948 |   15704    9046   515244    57.0 | 37.196 % |
c ==============================================================================
c [1mFound solution: 236[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9972 |   36377    91810 |   12125    9055   512446    56.6 | 37.196 % |
c |     10072 |   36377    91810 |   13337    9155   518100    56.6 | 37.255 % |
c |     10223 |   36018    90983 |   14671    9302   519962    55.9 | 37.838 % |
c |     10448 |   32620    83128 |   16138    9391   519834    55.4 | 43.686 % |
c ==============================================================================
c [1mFound solution: 235[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10772 |   31893    81457 |   10631    9693   533532    55.0 | 43.686 % |
c |     10872 |   30663    78621 |   11694    9741   536241    55.0 | 46.867 % |
c |     11022 |   30538    78330 |   12863    9886   540542    54.7 | 47.086 % |
c |     11250 |   29620    76201 |   14149   10083   556329    55.2 | 48.646 % |
c |     11588 |   29620    76201 |   15564   10421   568869    54.6 | 48.646 % |
c |     12094 |   29620    76201 |   17121   10927   595654    54.5 | 48.646 % |
c |     12854 |   29620    76201 |   18833   11687   635084    54.3 | 48.646 % |
c |     13993 |   29620    76201 |   20716   12826   686020    53.5 | 48.646 % |
c |     15701 |   29144    75096 |   22788   14522   856761    59.0 | 49.441 % |
c |     18263 |   24849    65085 |   25067   16822   976917    58.1 | 56.663 % |
c |     22111 |   24465    64191 |   27574   20636  1187218    57.5 | 57.318 % |
c |     27877 |   22363    59269 |   30331   26247  1523555    58.0 | 60.870 % |
c |     36527 |   21400    57019 |   33364   34808  2246416    64.5 | 62.460 % |
c |     49503 |   20997    56073 |   36701   18871  1388750    73.6 | 63.100 % |
c |     68968 |   20857    55745 |   40371   38333  3191510    83.3 | 63.334 % |
c |     98161 |   20369    54586 |   44408   30558  1763922    57.7 | 64.098 % |
c |    141951 |   20369    54586 |   48849   34552  3080605    89.2 | 64.098 % |
c |    207636 |   19300    52053 |   53734   46663  3989889    85.5 | 66.001 % |
c ==============================================================================
c [1mOptimal solution: 235[0m
s OPTIMUM FOUND
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
c _______________________________________________________________________________
c 
c restarts              : 63
c conflicts             : 213722         (289 /sec)
c decisions             : 443632         (601 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 738.379 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 1569
Raw data (stat): 1569 (runsolver) R 1568 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481534704 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 1569
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 2357 0 0 0 992 6 0 0 25 0 1 0 481534704 11845632 2281 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2892 2281 603 41 0 2851 0
vsize: 11568
[startup+20.0014 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 1569
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 2533 0 0 0 1991 6 0 0 25 0 1 0 481534704 12533760 2457 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3060 2457 603 41 0 3019 0
vsize: 12240
[startup+30.0019 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 1569
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 2731 0 0 0 2990 7 0 0 25 0 1 0 481534704 13447168 2655 4294967295 134512640 134672761 3221224576 3221223724 1074733099 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3283 2655 603 41 0 3242 0
vsize: 13132
[startup+40.0014 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 1569
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 2983 0 0 0 3989 8 0 0 25 0 1 0 481534704 14393344 2907 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3514 2907 603 41 0 3473 0
vsize: 14056
[startup+50.0017 s]
Raw data (loadavg): 0.93 0.94 0.90 3/57 1606
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 3275 0 0 0 4988 9 0 0 25 0 1 0 481534704 15671296 3199 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3826 3199 603 41 0 3785 0
vsize: 15304
[startup+60.0025 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 1622
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 3567 0 0 0 5986 10 0 0 25 0 1 0 481534704 16887808 3491 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4123 3491 603 41 0 4082 0
vsize: 16492
[startup+70.0031 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 1622
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 3783 0 0 0 6986 10 0 0 25 0 1 0 481534704 17821696 3707 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4351 3707 603 41 0 4310 0
vsize: 17404
[startup+80.0039 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 1622
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 4000 0 0 0 7985 11 0 0 25 0 1 0 481534704 18628608 3924 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4548 3924 603 41 0 4507 0
vsize: 18192
[startup+90.0036 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 1622
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 4234 0 0 0 8984 12 0 0 25 0 1 0 481534704 19566592 4158 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4777 4158 603 41 0 4736 0
vsize: 19108
[startup+100.003 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 1622
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 4594 0 0 0 9983 13 0 0 25 0 1 0 481534704 21164032 4518 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5167 4518 603 41 0 5126 0
vsize: 20668
[startup+110.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1622
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 4837 0 0 0 10982 14 0 0 25 0 1 0 481534704 22245376 4761 4294967295 134512640 134672761 3221224576 3221223712 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5431 4761 603 41 0 5390 0
vsize: 21724
[startup+120.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 5089 0 0 0 11982 15 0 0 25 0 1 0 481534704 23199744 5013 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5664 5013 603 41 0 5623 0
vsize: 22656
[startup+130.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 5437 0 0 0 12981 16 0 0 25 0 1 0 481534704 24674304 5361 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6024 5361 603 41 0 5983 0
vsize: 24096
[startup+140.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 5639 0 0 0 13980 17 0 0 25 0 1 0 481534704 25460736 5563 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6216 5563 603 41 0 6175 0
vsize: 24864
[startup+150.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 5887 0 0 0 14980 17 0 0 25 0 1 0 481534704 26558464 5811 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6484 5811 603 41 0 6443 0
vsize: 25936
[startup+160.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 6009 0 0 0 15980 17 0 0 25 0 1 0 481534704 26959872 5933 4294967295 134512640 134672761 3221224576 3221223744 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6582 5933 603 41 0 6541 0
vsize: 26328
[startup+170.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 6029 0 0 0 16980 18 0 0 25 0 1 0 481534704 27111424 5953 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 5953 603 41 0 6578 0
vsize: 26476
[startup+180.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 6055 0 0 0 17980 18 0 0 25 0 1 0 481534704 27275264 5979 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6659 5979 603 41 0 6618 0
vsize: 26636
[startup+190.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 6065 0 0 0 18980 18 0 0 25 0 1 0 481534704 27275264 5989 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6659 5989 603 41 0 6618 0
vsize: 26636
[startup+200.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 6101 0 0 0 19980 18 0 0 25 0 1 0 481534704 27439104 6025 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6699 6025 603 41 0 6658 0
vsize: 26796
[startup+210.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 6119 0 0 0 20981 18 0 0 25 0 1 0 481534704 27602944 6043 4294967295 134512640 134672761 3221224576 3221223712 134560632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6739 6043 603 41 0 6698 0
vsize: 26956
[startup+220.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 6142 0 0 0 21981 18 0 0 25 0 1 0 481534704 27766784 6066 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6779 6066 603 41 0 6738 0
vsize: 27116
[startup+230.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 6148 0 0 0 22981 18 0 0 25 0 1 0 481534704 27766784 6072 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6779 6072 603 41 0 6738 0
vsize: 27116
[startup+240.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 6279 0 0 0 23980 19 0 0 25 0 1 0 481534704 28348416 6203 4294967295 134512640 134672761 3221224576 3221223680 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6921 6203 603 41 0 6880 0
vsize: 27684
[startup+250.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 6565 0 0 0 24980 20 0 0 25 0 1 0 481534704 29470720 6489 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7195 6489 603 41 0 7154 0
vsize: 28780
[startup+260.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 6914 0 0 0 25979 20 0 0 25 0 1 0 481534704 30949376 6838 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7556 6838 603 41 0 7515 0
vsize: 30224
[startup+270.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7166 0 0 0 26979 21 0 0 25 0 1 0 481534704 32018432 7090 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7817 7090 603 41 0 7776 0
vsize: 31268
[startup+280.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7264 0 0 0 27978 21 0 0 25 0 1 0 481534704 32423936 7188 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7916 7188 603 41 0 7875 0
vsize: 31664
[startup+290.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7375 0 0 0 28978 22 0 0 25 0 1 0 481534704 32829440 7299 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8015 7299 603 41 0 7974 0
vsize: 32060
[startup+300.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7378 0 0 0 29978 22 0 0 25 0 1 0 481534704 32829440 7302 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8015 7302 603 41 0 7974 0
vsize: 32060
[startup+310.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7378 0 0 0 30978 22 0 0 25 0 1 0 481534704 32829440 7302 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8015 7302 603 41 0 7974 0
vsize: 32060
[startup+320.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7379 0 0 0 31979 22 0 0 25 0 1 0 481534704 32829440 7303 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8015 7303 603 41 0 7974 0
vsize: 32060
[startup+330.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7379 0 0 0 32979 22 0 0 25 0 1 0 481534704 32829440 7303 4294967295 134512640 134672761 3221224576 3221223680 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8015 7303 603 41 0 7974 0
vsize: 32060
[startup+340.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7379 0 0 0 33979 22 0 0 25 0 1 0 481534704 32829440 7303 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8015 7303 603 41 0 7974 0
vsize: 32060
[startup+350.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7380 0 0 0 34979 22 0 0 25 0 1 0 481534704 32829440 7304 4294967295 134512640 134672761 3221224576 3221223680 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8015 7304 603 41 0 7974 0
vsize: 32060
[startup+360.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7380 0 0 0 35979 22 0 0 25 0 1 0 481534704 32829440 7304 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8015 7304 603 41 0 7974 0
vsize: 32060
[startup+370.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7381 0 0 0 36980 22 0 0 25 0 1 0 481534704 32829440 7305 4294967295 134512640 134672761 3221224576 3221223744 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8015 7305 603 41 0 7974 0
vsize: 32060
[startup+380.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7381 0 0 0 37980 22 0 0 25 0 1 0 481534704 32829440 7305 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8015 7305 603 41 0 7974 0
vsize: 32060
[startup+390.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1624
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7381 0 0 0 38980 22 0 0 25 0 1 0 481534704 32829440 7305 4294967295 134512640 134672761 3221224576 3221223776 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8015 7305 603 41 0 7974 0
vsize: 32060
[startup+400.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7381 0 0 0 39980 22 0 0 25 0 1 0 481534704 32829440 7305 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8015 7305 603 41 0 7974 0
vsize: 32060
[startup+410.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7411 0 0 0 40980 22 0 0 25 0 1 0 481534704 32960512 7335 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8047 7335 603 41 0 8006 0
vsize: 32188
[startup+420.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7660 0 0 0 41979 23 0 0 25 0 1 0 481534704 34058240 7584 4294967295 134512640 134672761 3221224576 3221223680 134559796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8315 7584 603 41 0 8274 0
vsize: 33260
[startup+430.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7793 0 0 0 42979 24 0 0 25 0 1 0 481534704 34586624 7717 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8444 7717 603 41 0 8403 0
vsize: 33776
[startup+440.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7793 0 0 0 43979 24 0 0 25 0 1 0 481534704 34586624 7717 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8444 7717 603 41 0 8403 0
vsize: 33776
[startup+450.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7793 0 0 0 44979 24 0 0 25 0 1 0 481534704 34586624 7717 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8444 7717 603 41 0 8403 0
vsize: 33776
[startup+460.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7793 0 0 0 45980 24 0 0 25 0 1 0 481534704 34586624 7717 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8444 7717 603 41 0 8403 0
vsize: 33776
[startup+470.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7793 0 0 0 46980 24 0 0 25 0 1 0 481534704 34586624 7717 4294967295 134512640 134672761 3221224576 3221223680 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8444 7717 603 41 0 8403 0
vsize: 33776
[startup+480.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7793 0 0 0 47980 24 0 0 25 0 1 0 481534704 34586624 7717 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8444 7717 603 41 0 8403 0
vsize: 33776
[startup+490.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7793 0 0 0 48980 24 0 0 25 0 1 0 481534704 34586624 7717 4294967295 134512640 134672761 3221224576 3221223760 134558513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8444 7717 603 41 0 8403 0
vsize: 33776
[startup+500.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7793 0 0 0 49980 24 0 0 25 0 1 0 481534704 34586624 7717 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8444 7717 603 41 0 8403 0
vsize: 33776
[startup+510.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7793 0 0 0 50980 24 0 0 25 0 1 0 481534704 34586624 7717 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8444 7717 603 41 0 8403 0
vsize: 33776
[startup+520.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7793 0 0 0 51980 24 0 0 25 0 1 0 481534704 34586624 7717 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8444 7717 603 41 0 8403 0
vsize: 33776
[startup+530.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7794 0 0 0 52981 24 0 0 25 0 1 0 481534704 34586624 7718 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8444 7718 603 41 0 8403 0
vsize: 33776
[startup+540.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7794 0 0 0 53981 24 0 0 25 0 1 0 481534704 34586624 7718 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8444 7718 603 41 0 8403 0
vsize: 33776
[startup+550.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7794 0 0 0 54981 24 0 0 25 0 1 0 481534704 34586624 7718 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8444 7718 603 41 0 8403 0
vsize: 33776
[startup+560.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7794 0 0 0 55981 24 0 0 25 0 1 0 481534704 34586624 7718 4294967295 134512640 134672761 3221224576 3221223744 134561256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8444 7718 603 41 0 8403 0
vsize: 33776
[startup+570.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 7794 0 0 0 56981 24 0 0 25 0 1 0 481534704 34586624 7718 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8444 7718 603 41 0 8403 0
vsize: 33776
[startup+580.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 8052 0 0 0 57981 25 0 0 25 0 1 0 481534704 35639296 7976 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8701 7976 603 41 0 8660 0
vsize: 34804
[startup+590.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 8399 0 0 0 58980 26 0 0 25 0 1 0 481534704 36982784 8323 4294967295 134512640 134672761 3221224576 3221223680 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9029 8323 603 41 0 8988 0
vsize: 36116
[startup+600.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 8671 0 0 0 59979 27 0 0 25 0 1 0 481534704 38178816 8595 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9321 8595 603 41 0 9280 0
vsize: 37284
[startup+610.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 8861 0 0 0 60979 27 0 0 25 0 1 0 481534704 38842368 8785 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9483 8785 603 41 0 9442 0
vsize: 37932
[startup+620.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 9034 0 0 0 61978 28 0 0 25 0 1 0 481534704 39645184 8958 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9679 8958 603 41 0 9638 0
vsize: 38716
[startup+630.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 9035 0 0 0 62978 28 0 0 25 0 1 0 481534704 39645184 8959 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9679 8959 603 41 0 9638 0
vsize: 38716
[startup+640.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 9040 0 0 0 63979 28 0 0 25 0 1 0 481534704 39645184 8964 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9679 8964 603 41 0 9638 0
vsize: 38716
[startup+650.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 9040 0 0 0 64979 28 0 0 25 0 1 0 481534704 39645184 8964 4294967295 134512640 134672761 3221224576 3221223744 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9679 8964 603 41 0 9638 0
vsize: 38716
[startup+660.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 9041 0 0 0 65979 28 0 0 25 0 1 0 481534704 39645184 8965 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9679 8965 603 41 0 9638 0
vsize: 38716
[startup+670.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 9041 0 0 0 66979 28 0 0 25 0 1 0 481534704 39645184 8965 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9679 8965 603 41 0 9638 0
vsize: 38716
[startup+680.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 9041 0 0 0 67979 28 0 0 25 0 1 0 481534704 39645184 8965 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9679 8965 603 41 0 9638 0
vsize: 38716
[startup+690.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 9041 0 0 0 68978 28 0 0 25 0 1 0 481534704 39645184 8965 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9679 8965 603 41 0 9638 0
vsize: 38716
[startup+700.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 9041 0 0 0 69978 28 0 0 25 0 1 0 481534704 39645184 8965 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9679 8965 603 41 0 9638 0
vsize: 38716
[startup+710.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 9068 0 0 0 70979 28 0 0 25 0 1 0 481534704 39800832 8992 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9717 8992 603 41 0 9676 0
vsize: 38868
[startup+720.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 9083 0 0 0 71978 29 0 0 25 0 1 0 481534704 39800832 9007 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9717 9007 603 41 0 9676 0
vsize: 38868
[startup+730.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 9096 0 0 0 72978 29 0 0 25 0 1 0 481534704 39997440 9020 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9765 9020 603 41 0 9724 0
vsize: 39060
[startup+738.646 s]
Raw data (loadavg): 1.00 0.97 0.91 1/53 1626
Raw data (stat): 1569 (minisat+) R 1568 27222 27221 0 -1 0 9096 0 0 0 72978 29 0 0 25 0 1 0 481534704 39997440 9020 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9765 9020 603 41 0 9724 0
vsize: 0

Child status: 30
Real time (s): 738.646
CPU time (s): 738.697
CPU user time (s): 738.388
CPU system time (s): 0.308953
CPU usage (%): 100.007
Max. virtual memory (Kb): 39060
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	235
#### END VERIFIER DATA ####