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-max1024.pi.opb
MD5SUM	6604a6c0d979e1f2b09762e6e4f70f84
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	259
Optimality of the best value was proved	NO
Number of terms in the objective function	1278
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	1278
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1278
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04584
Number of variables	1278
Total number of constraints	1087
Number of constraints which are clauses	1087
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	1
Maximum length of a constraint	18
Trace number 5406

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-13 23:44:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3818 boxname=wulflinc8 idbench=58 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6604a6c0d979e1f2b09762e6e4f70f84  /oldhome/oroussel/tmp/wulflinc8/normalized-max1024.pi.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc8/normalized-max1024.pi.opb /oldhome/oroussel/tmp/wulflinc8/normalized-max1024.pi.opb
IDLAUNCH: 3818
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        904052 kB
Buffers:         36820 kB
Cached:          74360 kB
SwapCached:          0 kB
Active:          72916 kB
Inactive:        41144 kB
HighTotal:      131008 kB
HighFree:        52696 kB
LowTotal:       903652 kB
LowFree:        851356 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6932 kB
Slab:            10944 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:04:19 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 3818 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1071 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: =====
c   -- Clauses(.)/Splits(s): .........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    1057     6882 |     317       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |    1040     6766 |      --       0       --      -- |     --   | -17/-116
c |         0 |    1040     6766 |     416       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.066989 s)
c ==============================================================================
c [1mFound solution: 300[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:69860     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   85956   205076 |   25786       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/57248          
c   -- var.elim.:  2000/57248          
c   -- var.elim.:  3000/57248          
c   -- var.elim.:  4000/57248          
c   -- var.elim.:  5000/57248          
c   -- var.elim.:  6000/57248          
c   -- var.elim.:  7000/57248          
c   -- var.elim.:  8000/57248          
c   -- var.elim.:  9000/57248          
c   -- var.elim.:  10000/57248          
c   -- var.elim.:  11000/57248          
c   -- var.elim.:  12000/57248          
c   -- var.elim.:  13000/57248          
c   -- var.elim.:  14000/57248          
c   -- var.elim.:  15000/57248          
c   -- var.elim.:  16000/57248          
c   -- var.elim.:  17000/57248          
c   -- var.elim.:  18000/57248          
c   -- var.elim.:  19000/57248          
c   -- var.elim.:  20000/57248          
c   -- var.elim.:  21000/57248          
c   -- var.elim.:  22000/57248          
c   -- var.elim.:  23000/57248          
c   -- var.elim.:  24000/57248          
c   -- var.elim.:  25000/57248          
c   -- var.elim.:  26000/57248          
c   -- var.elim.:  27000/57248          
c   -- var.elim.:  28000/57248          
c   -- var.elim.:  29000/57248          
c   -- var.elim.:  30000/57248          
c   -- var.elim.:  31000/57248          
c   -- var.elim.:  32000/57248          
c   -- var.elim.:  33000/57248          
c   -- var.elim.:  34000/57248          
c   -- var.elim.:  35000/57248          
c   -- var.elim.:  36000/57248          
c   -- var.elim.:  37000/57248          
c   -- var.elim.:  38000/57248          
c   -- var.elim.:  39000/57248          
c   -- var.elim.:  40000/57248          
c   -- var.elim.:  41000/57248          
c   -- var.elim.:  42000/57248          
c   -- var.elim.:  43000/57248          
c   -- var.elim.:  44000/57248          
c   -- var.elim.:  45000/57248          
c   -- var.elim.:  46000/57248          
c   -- var.elim.:  47000/57248          
c   -- var.elim.:  48000/57248          
c   -- var.elim.:  49000/57248          
c   -- var.elim.:  50000/57248          
c   -- var.elim.:  51000/57248          
c   -- var.elim.:  52000/57248          
c   -- var.elim.:  53000/57248          
c   -- var.elim.:  54000/57248          
c   -- var.elim.:  55000/57248          
c   -- var.elim.:  56000/57248          
c   -- var.elim.:  57000/57248          
c   -- var.elim.:  57248/57248          
c   -- var.elim.:  1000/28514          
c   -- var.elim.:  2000/28514          
c   -- var.elim.:  3000/28514          
c   -- var.elim.:  4000/28514          
c   -- var.elim.:  5000/28514          
c   -- var.elim.:  6000/28514          
c   -- var.elim.:  7000/28514          
c   -- var.elim.:  8000/28514          
c   -- var.elim.:  9000/28514          
c   -- var.elim.:  10000/28514          
c   -- var.elim.:  11000/28514          
c   -- var.elim.:  12000/28514          
c   -- var.elim.:  13000/28514          
c   -- var.elim.:  14000/28514          
c   -- var.elim.:  15000/28514          
c   -- var.elim.:  16000/28514          
c   -- var.elim.:  17000/28514          
c   -- var.elim.:  18000/28514          
c   -- var.elim.:  19000/28514          
c   -- var.elim.:  20000/28514          
c   -- var.elim.:  21000/28514          
c   -- var.elim.:  22000/28514          
c   -- var.elim.:  23000/28514          
c   -- var.elim.:  24000/28514          
c   -- var.elim.:  25000/28514          
c   -- var.elim.:  26000/28514          
c   -- var.elim.:  27000/28514          
c   -- var.elim.:  28000/28514          
c   -- var.elim.:  28514/28514          
c   -- subsuming                       
c   -- var.elim.:  1000/24599          
c   -- var.elim.:  2000/24599          
c   -- var.elim.:  3000/24599          
c   -- var.elim.:  4000/24599          
c   -- var.elim.:  5000/24599          
c   -- var.elim.:  6000/24599          
c   -- var.elim.:  7000/24599          
c   -- var.elim.:  8000/24599          
c   -- var.elim.:  9000/24599          
c   -- var.elim.:  10000/24599          
c   -- var.elim.:  11000/24599          
c   -- var.elim.:  12000/24599          
c   -- var.elim.:  13000/24599          
c   -- var.elim.:  14000/24599          
c   -- var.elim.:  15000/24599          
c   -- var.elim.:  16000/24599          
c   -- var.elim.:  17000/24599          
c   -- var.elim.:  18000/24599          
c   -- var.elim.:  19000/24599          
c   -- var.elim.:  20000/24599          
c   -- var.elim.:  21000/24599          
c   -- var.elim.:  22000/24599          
c   -- var.elim.:  23000/24599          
c   -- var.elim.:  24000/24599          
c   -- var.elim.:  24599/24599          
c   -- var.elim.:  368/368          
c |         0 |   57298   548049 |      --       0       --      -- |     --   | -28648/343003
c |         0 |   57298   548049 |   22919       0        0     nan |  0.000 % |
c |       100 |   56176   536301 |   24717      67     1251    18.7 |  2.740 % |
c |       250 |   55251   526388 |   26741     189     3577    18.9 |  4.321 % |
c |       475 |   54614   519770 |   29076     383     6866    17.9 |  5.425 % |
c |       812 |   54228   516080 |   31758     697    11246    16.1 |  6.080 % |
c |      1319 |   53814   511882 |   34667    1182    29785    25.2 |  6.791 % |
c |      2078 |   53456   508441 |   37880    1915    53402    27.9 |  7.380 % |
c |      3217 |   53414   508016 |   41635    3048   113785    37.3 |  7.454 % |
c |      4926 |   53108   504870 |   45536    4707   196396    41.7 |  7.965 % |
c |      7489 |   53085   504644 |   50068    7249   370849    51.2 |  8.004 % |
c |     11333 |   52961   503516 |   54946   11068   553209    50.0 |  8.197 % |
c |     17099 |   52756   501582 |   60207   16776  1002290    59.7 |  8.551 % |
c |     25748 |   52679   501000 |   66131   25390  2661798   104.8 |  8.670 % |
c |     38722 |   52626   500385 |   72671   38298  3644580    95.2 |  8.750 % |
c |     58184 |   52509   499208 |   79761   57569  4884617    84.8 |  8.947 % |
c |     87376 |   52442   498620 |   87625   86707 11117892   128.2 |  9.062 % |
c |    131165 |   52364   497986 |   96244   51627  7914927   153.3 |  9.195 % |
c ==============================================================================
c (current CPU-time: 709.092 s)
c ==============================================================================
c [1mFound solution: 290[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 |    141948 |   53494   501189 |   16048   62410  9949073   159.4 |  9.195 % |
c   -- subsuming                       
c   -- var.elim.:  1000/21028          
c   -- var.elim.:  2000/21028          
c   -- var.elim.:  3000/21028          
c   -- var.elim.:  4000/21028          
c   -- var.elim.:  5000/21028          
c   -- var.elim.:  6000/21028          
c   -- var.elim.:  7000/21028          
c   -- var.elim.:  8000/21028          
c   -- var.elim.:  9000/21028          
c   -- var.elim.:  10000/21028          
c   -- var.elim.:  11000/21028          
c   -- var.elim.:  12000/21028          
c   -- var.elim.:  13000/21028          
c   -- var.elim.:  14000/21028          
c   -- var.elim.:  15000/21028          
c   -- var.elim.:  16000/21028          
c   -- var.elim.:  17000/21028          
c   -- var.elim.:  18000/21028          
c   -- var.elim.:  19000/21028          
c   -- var.elim.:  20000/21028          
c   -- var.elim.:  21000/21028          
c   -- var.elim.:  21028/21028          
c   -- var.elim.:  1000/4441          
c   -- var.elim.:  2000/4441          
c   -- var.elim.:  3000/4441          
c   -- var.elim.:  4000/4441          
c   -- var.elim.:  4441/4441          
c   -- var.elim.:  415/415          
c   -- var.elim.:  430/430          
c   -- var.elim.:  590/590          
c   -- subsuming                       
c   -- var.elim.:  901/901          
c |    141948 |   52257   498331 |      --   62410       --      -- |     --   | -1142/-902
c |    141948 |   52257   498331 |   20902   49374  5725064   116.0 |  9.195 % |
c |    142049 |   52257   498331 |   22993   11457  1495293   130.5 | 10.007 % |
c |    142199 |   52257   498331 |   25292   11607  1500876   129.3 | 10.007 % |
c |    142424 |   52257   498331 |   27821   11832  1511729   127.8 | 10.007 % |
c |    142761 |   52243   498149 |   30595   12166  1522500   125.1 | 10.032 % |
c |    143268 |   52243   498149 |   33655   12673  1578521   124.6 | 10.032 % |
c |    144027 |   52211   497931 |   36997   13430  1606446   119.6 | 10.088 % |
c |    145168 |   52211   497931 |   40697   14571  1647830   113.1 | 10.088 % |
c |    146877 |   52209   497902 |   44765   16276  1791966   110.1 | 10.091 % |
c |    149439 |   52174   497610 |   49209   18833  2067328   109.8 | 10.150 % |
c |    153284 |   52137   497209 |   54091   22586  2413483   106.9 | 10.213 % |
c |    159050 |   52107   496885 |   59466   28331  3226968   113.9 | 10.266 % |
c |    167702 |   52105   496853 |   65411   36978  4113456   111.2 | 10.269 % |
c |    180676 |   52101   496809 |   71946   49948  5297117   106.1 | 10.276 % |
c |    200137 |   52077   496604 |   79104   69407  6708668    96.7 | 10.318 % |
c |    229329 |   52075   496574 |   87012   27233  4357810   160.0 | 10.322 % |
c |    273120 |   52075   496574 |   95713   71024  7197019   101.3 | 10.322 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v x1 -x2 -x3 x4 -x5 -x6 -x7 -x8 -x9 x10 -x11 -x12 -x13 -x14 x15 x16 -x17 -x18 -x19 x20 -x21 x22 -x23 -x24 x25 -x26 -x27 -x28 -x29 x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 x42 -x43 -x44 -x45 x46 -x47 -x48 -x49 -x50 -x51 -x52 x53 -x54 x55 -x56 -x57 -x58 -x59 -x60 x61 -x62 x63 -x64 -x65 -x66 -x67 -x68 -x69 x70 x71 x72 x73 -x74 x75 -x76 -x77 x78 -x79 -x80 x81 x82 -x83 x84 -x85 -x86 x87 -x88 -x89 -x90 x91 x92 -x93 -x94 -x95 -x96 x97 -x98 x99 -x100 -x101 x102 -x103 -x104 -x105 -x106 -x107 -x108 -x109 x110 -x111 x112 -x113 -x114 -x115 -x116 -x117 -x118 x119 -x120 x121 x122 -x123 x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 x136 -x137 x138 x139 -x140 -x141 -x142 -x143 x144 -x145 x146 -x147 -x148 -x149 x150 -x151 -x152 -x153 -x154 -x155 x156 -x157 x158 x159 -x160 -x161 -x162 -x163 -x164 -x165 x166 -x167 -x168 x169 -x170 -x171 -x172 -x173 -x174 x175 x176 -x177 -x178 -x179 x180 -x181 -x182 -x183 x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 -x192 -x193 x194 -x195 x196 -x197 -x198 -x199 -x200 -x201 x202 -x203 -x204 x205 -x206 -x207 -x208 x209 -x210 -x211 x212 -x213 -x214 -x215 -x216 x217 -x218 -x219 -x220 x221 -x222 x223 -x224 x225 -x226 -x227 -x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 x237 x238 -x239 -x240 -x241 -x242 -x243 -x244 x245 x246 -x247 x248 x249 -x250 -x251 -x252 x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 -x266 x267 -x268 x269 -x270 -x271 -x272 -x273 -x274 x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 x285 -x286 x287 -x288 -x289 -x290 x291 x292 -x293 -x294 -x295 x296 -x297 -x298 -x299 -x300 -x301 x302 x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 x317 -x318 -x319 -x320 -x321 x322 -x323 -x324 x325 -x326 -x327 -x328 -x329 x330 -x331 -x332 -x333 -x334 -x335 x336 -x337 x338 x339 -x340 -x341 x342 -x343 -x344 -x345 -x346 x347 -x348 x349 -x350 -x351 x352 -x353 -x354 x355 -x356 -x357 -x358 -x359 -x360 x361 -x362 -x363 -x364 -x365 -x366 -x367 -x368 -x369 x370 -x371 -x372 -x373 -x374 x375 x376 -x377 -x378 -x379 -x380 x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 -x389 -x390 -x391 -x392 x393 x394 -x395 -x396 x397 -x398 x399 -x400 -x401 -x402 x403 -x404 -x405 -x406 -x407 x408 -x409 x410 -x411 -x412 x413 -x414 -x415 -x416 -x417 -x418 x419 -x420 -x421 -x422 x423 -x424 -x425 -x426 -x427 -x428 -x429 -x430 -x431 -x432 -x433 x434 -x435 -x436 -x437 -x438 -x439 -x440 -x441 -x442 -x443 -x444 -x445 -x446 -x447 -x448 x449 -x450 x451 -x452 x453 -x454 -x455 x456 -x457 -x458 -x459 -x460 x461 x462 -x463 -x464 -x465 -x466 -x467 x468 -x469 -x470 -x471 -x472 -x473 -x474 -x475 -x476 -x477 -x478 -x479 x480 -x481 -x482 -x483 -x484 x485 x486 -x487 -x488 -x489 -x490 x491 -x492 -x493 x494 -x495 -x496 -x497 -x498 x499 -x500 -x501 -x502 x503 -x504 -x505 -x506 -x507 -x508 -x509 -x510 x511 -x512 -x513 -x514 -x515 -x516 x517 -x518 x519 -x520 -x521 x522 x523 -x524 x525 x526 -x527 -x528 -x529 -x530 -x531 -x532 -x533 -x534 x535 -x536 -x537 x538 -x539 x540 -x541 x542 -x543 x544 x545 -x546 -x547 -x548 -x549 x550 -x551 -x552 -x553 -x554 -x555 -x556 -x557 -x558 x559 -x560 -x561 -x562 -x563 x564 -x565 -x566 -x567 x568 x569 -x570 -x571 -x572 -x573 -x574 -x575 -x576 -x577 -x578 -x579 -x580 x581 -x582 x583 x584 -x585 x586 -x587 x588 -x589 -x590 -x591 -x592 x593 -x594 x595 -x596 -x597 x598 -x599 x600 -x601 -x602 -x603 -x604 x605 -x606 x607 -x608 -x609 x610 x611 -x612 -x613 -x614 -x615 -x616 x617 x618 -x619 -x620 -x621 -x622 -x623 x624 -x625 -x626 -x627 -x628 -x629 x630 -x631 -x632 -x633 -x634 x635 -x636 -x637 -x638 -x639 -x640 -x641 -x642 x643 -x644 -x645 -x646 -x647 -x648 -x649 -x650 -x651 -x652 -x653 x654 -x655 -x656 -x657 -x658 -x659 -x660 -x661 -x662 -x663 -x664 -x665 -x666 -x667 -x668 -x669 -x670 x671 -x672 -x673 -x674 x675 -x676 x677 -x678 -x679 -x680 x681 -x682 -x683 -x684 x685 -x686 -x687 -x688 x689 -x690 -x691 -x692 x693 -x694 -x695 -x696 x697 -x698 -x699 -x700 -x701 -x702 -x703 -x704 -x705 x706 -x707 -x708 -x709 -x710 x711 x7#### 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 30692
Raw data (stat): 30692 (runsolver) R 30691 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 408221388 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.001 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8570 0 0 0 964 34 0 0 25 0 1 0 408221388 38297600 8269 4294967295 134512640 134672761 3221224560 3221223008 134643777 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8269 603 41 0 9309 0
vsize: 37400
[startup+20.0017 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8576 0 0 0 1964 34 0 0 25 0 1 0 408221388 38297600 8275 4294967295 134512640 134672761 3221224560 3221223008 134644032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8275 603 41 0 9309 0
vsize: 37400
[startup+30.0011 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8576 0 0 0 2965 34 0 0 25 0 1 0 408221388 38297600 8275 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8275 603 41 0 9309 0
vsize: 37400
[startup+40.0015 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8579 0 0 0 3964 34 0 0 25 0 1 0 408221388 38297600 8278 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9350 8278 603 41 0 9309 0
vsize: 37400
[startup+50.0023 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8580 0 0 0 4963 34 0 0 25 0 1 0 408221388 38297600 8279 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9350 8279 603 41 0 9309 0
vsize: 37400
[startup+60.0025 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8582 0 0 0 5963 34 0 0 25 0 1 0 408221388 38297600 8281 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8281 603 41 0 9309 0
vsize: 37400
[startup+70.0036 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8589 0 0 0 6963 35 0 0 25 0 1 0 408221388 38404096 8288 4294967295 134512640 134672761 3221224560 3221223008 134643570 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9376 8288 603 41 0 9335 0
vsize: 37504
[startup+80.0033 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8708 0 0 0 7962 36 0 0 25 0 1 0 408221388 38686720 8351 4294967295 134512640 134672761 3221224560 3221223008 134643493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9445 8351 603 41 0 9404 0
vsize: 37780
[startup+90.0038 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8708 0 0 0 8962 36 0 0 25 0 1 0 408221388 38686720 8351 4294967295 134512640 134672761 3221224560 3221223040 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9445 8351 603 41 0 9404 0
vsize: 37780
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8709 0 0 0 9962 36 0 0 25 0 1 0 408221388 38686720 8352 4294967295 134512640 134672761 3221224560 3221223008 134643539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9445 8352 603 41 0 9404 0
vsize: 37780
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8709 0 0 0 10962 36 0 0 25 0 1 0 408221388 38686720 8352 4294967295 134512640 134672761 3221224560 3221223008 134643562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9445 8352 603 41 0 9404 0
vsize: 37780
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8710 0 0 0 11962 36 0 0 25 0 1 0 408221388 38686720 8353 4294967295 134512640 134672761 3221224560 3221223008 134643539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9445 8353 603 41 0 9404 0
vsize: 37780
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8710 0 0 0 12962 36 0 0 25 0 1 0 408221388 38686720 8353 4294967295 134512640 134672761 3221224560 3221223008 134643977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9445 8353 603 41 0 9404 0
vsize: 37780
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8710 0 0 0 13962 36 0 0 25 0 1 0 408221388 38686720 8353 4294967295 134512640 134672761 3221224560 3221223008 134643474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9445 8353 603 41 0 9404 0
vsize: 37780
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8710 0 0 0 14963 36 0 0 25 0 1 0 408221388 38686720 8353 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9445 8353 603 41 0 9404 0
vsize: 37780
[startup+160.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8714 0 0 0 15963 36 0 0 25 0 1 0 408221388 38686720 8357 4294967295 134512640 134672761 3221224560 3221223008 134643948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9445 8357 603 41 0 9404 0
vsize: 37780
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8970 0 0 0 16962 36 0 0 25 0 1 0 408221388 40112128 8543 4294967295 134512640 134672761 3221224560 3221222784 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 8543 603 41 0 9752 0
vsize: 39172
[startup+180.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8970 0 0 0 17963 36 0 0 25 0 1 0 408221388 40112128 8543 4294967295 134512640 134672761 3221224560 3221222960 134604097 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 8543 603 41 0 9752 0
vsize: 39172
[startup+190.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8970 0 0 0 18963 36 0 0 25 0 1 0 408221388 40112128 8543 4294967295 134512640 134672761 3221224560 3221222960 134605852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 8543 603 41 0 9752 0
vsize: 39172
[startup+200.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8970 0 0 0 19963 36 0 0 25 0 1 0 408221388 40112128 8543 4294967295 134512640 134672761 3221224560 3221223120 134607814 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 8543 603 41 0 9752 0
vsize: 39172
[startup+210.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8970 0 0 0 20963 36 0 0 25 0 1 0 408221388 40112128 8543 4294967295 134512640 134672761 3221224560 3221223024 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 8543 603 41 0 9752 0
vsize: 39172
[startup+220.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8970 0 0 0 21963 36 0 0 25 0 1 0 408221388 40112128 8543 4294967295 134512640 134672761 3221224560 3221223056 134606966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 8543 603 41 0 9752 0
vsize: 39172
[startup+230.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8970 0 0 0 22964 36 0 0 25 0 1 0 408221388 40112128 8543 4294967295 134512640 134672761 3221224560 3221223024 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 8543 603 41 0 9752 0
vsize: 39172
[startup+240.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8970 0 0 0 23964 36 0 0 25 0 1 0 408221388 40112128 8543 4294967295 134512640 134672761 3221224560 3221223024 134644277 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 8543 603 41 0 9752 0
vsize: 39172
[startup+250.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8970 0 0 0 24964 36 0 0 25 0 1 0 408221388 40112128 8543 4294967295 134512640 134672761 3221224560 3221223052 134642731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 8543 603 41 0 9752 0
vsize: 39172
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8970 0 0 0 25964 36 0 0 25 0 1 0 408221388 40112128 8543 4294967295 134512640 134672761 3221224560 3221223056 134606544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 8543 603 41 0 9752 0
vsize: 39172
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8971 0 0 0 26964 36 0 0 25 0 1 0 408221388 40112128 8544 4294967295 134512640 134672761 3221224560 3221223104 134621090 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 8544 603 41 0 9752 0
vsize: 39172
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8971 0 0 0 27965 36 0 0 25 0 1 0 408221388 40112128 8544 4294967295 134512640 134672761 3221224560 3221223104 134621062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 8544 603 41 0 9752 0
vsize: 39172
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8971 0 0 0 28965 36 0 0 25 0 1 0 408221388 40112128 8544 4294967295 134512640 134672761 3221224560 3221223104 134621207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 8544 603 41 0 9752 0
vsize: 39172
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 8971 0 0 0 29965 36 0 0 25 0 1 0 408221388 40112128 8544 4294967295 134512640 134672761 3221224560 3221223104 134621219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 8544 603 41 0 9752 0
vsize: 39172
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 9061 0 0 0 30965 37 0 0 25 0 1 0 408221388 38522880 8331 4294967295 134512640 134672761 3221224560 3221223008 134643572 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9405 8331 603 41 0 9364 0
vsize: 37620
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 9061 0 0 0 31965 37 0 0 25 0 1 0 408221388 38522880 8331 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9405 8331 603 41 0 9364 0
vsize: 37620
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 9061 0 0 0 32965 37 0 0 25 0 1 0 408221388 38522880 8331 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9405 8331 603 41 0 9364 0
vsize: 37620
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 9061 0 0 0 33965 37 0 0 25 0 1 0 408221388 38522880 8331 4294967295 134512640 134672761 3221224560 3221223008 134643963 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9405 8331 603 41 0 9364 0
vsize: 37620
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 9061 0 0 0 34966 37 0 0 25 0 1 0 408221388 38522880 8331 4294967295 134512640 134672761 3221224560 3221223008 134643969 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9405 8331 603 41 0 9364 0
vsize: 37620
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 9061 0 0 0 35966 37 0 0 25 0 1 0 408221388 38522880 8331 4294967295 134512640 134672761 3221224560 3221223008 134643984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9405 8331 603 41 0 9364 0
vsize: 37620
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 9071 0 0 0 36966 37 0 0 25 0 1 0 408221388 38522880 8341 4294967295 134512640 134672761 3221224560 3221223232 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9405 8341 603 41 0 9364 0
vsize: 37620
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 9077 0 0 0 37966 37 0 0 25 0 1 0 408221388 38670336 8347 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9441 8347 603 41 0 9400 0
vsize: 37764
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 9213 0 0 0 38966 37 0 0 25 0 1 0 408221388 39288832 8483 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9592 8483 603 41 0 9551 0
vsize: 38368
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 9656 0 0 0 39965 38 0 0 25 0 1 0 408221388 41136128 8926 4294967295 134512640 134672761 3221224560 3221223712 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10043 8926 603 41 0 10002 0
vsize: 40172
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 10059 0 0 0 40964 39 0 0 25 0 1 0 408221388 42770432 9329 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10442 9329 603 41 0 10401 0
vsize: 41768
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 11155 0 0 0 41960 43 0 0 25 0 1 0 408221388 47243264 10425 4294967295 134512640 134672761 3221224560 3221223392 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11534 10425 603 41 0 11493 0
vsize: 46136
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 11919 0 0 0 42958 45 0 0 25 0 1 0 408221388 50425856 11189 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12311 11189 603 41 0 12270 0
vsize: 49244
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 12382 0 0 0 43957 46 0 0 25 0 1 0 408221388 52404224 11652 4294967295 134512640 134672761 3221224560 3221223744 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12794 11652 603 41 0 12753 0
vsize: 51176
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 12861 0 0 0 44955 49 0 0 25 0 1 0 408221388 54382592 12131 4294967295 134512640 134672761 3221224560 3221223760 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13277 12131 603 41 0 13236 0
vsize: 53108
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 13145 0 0 0 45955 49 0 0 25 0 1 0 408221388 55439360 12415 4294967295 134512640 134672761 3221224560 3221223704 134616368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13535 12415 603 41 0 13494 0
vsize: 54140
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 13538 0 0 0 46953 50 0 0 25 0 1 0 408221388 57020416 12808 4294967295 134512640 134672761 3221224560 3221223600 134612565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13921 12808 603 41 0 13880 0
vsize: 55684
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 13939 0 0 0 47952 52 0 0 25 0 1 0 408221388 58744832 13209 4294967295 134512640 134672761 3221224560 3221223664 134604304 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14342 13209 603 41 0 14301 0
vsize: 57368
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 14262 0 0 0 48951 53 0 0 25 0 1 0 408221388 59932672 13532 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14632 13532 603 41 0 14591 0
vsize: 58528
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 14676 0 0 0 49950 55 0 0 25 0 1 0 408221388 61640704 13946 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15049 13946 603 41 0 15008 0
vsize: 60196
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 15260 0 0 0 50948 56 0 0 25 0 1 0 408221388 64290816 14530 4294967295 134512640 134672761 3221224560 3221223600 134613815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15696 14530 603 41 0 15655 0
vsize: 62784
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 16243 0 0 0 51946 59 0 0 25 0 1 0 408221388 68247552 15513 4294967295 134512640 134672761 3221224560 3221223720 134614557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16662 15513 603 41 0 16621 0
vsize: 66648
[startup+530.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 17140 0 0 0 52943 62 0 0 25 0 1 0 408221388 71929856 16410 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17561 16410 603 41 0 17520 0
vsize: 70244
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 17987 0 0 0 53941 64 0 0 25 0 1 0 408221388 75366400 17257 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18400 17257 603 41 0 18359 0
vsize: 73600
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 18872 0 0 0 54938 67 0 0 25 0 1 0 408221388 79056896 18142 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19301 18142 603 41 0 19260 0
vsize: 77204
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 19585 0 0 0 55937 69 0 0 25 0 1 0 408221388 81969152 18855 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20012 18855 603 41 0 19971 0
vsize: 80048
[startup+570.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 20313 0 0 0 56935 71 0 0 25 0 1 0 408221388 84996096 19583 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20751 19583 603 41 0 20710 0
vsize: 83004
[startup+580.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 20886 0 0 0 57934 72 0 0 25 0 1 0 408221388 87232512 20156 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21297 20156 603 41 0 21256 0
vsize: 85188
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 21329 0 0 0 58933 73 0 0 25 0 1 0 408221388 89079808 20599 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21748 20599 603 41 0 21707 0
vsize: 86992
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 21811 0 0 0 59933 74 0 0 25 0 1 0 408221388 90673152 20956 4294967295 134512640 134672761 3221224560 3221223744 134615523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22137 20956 603 41 0 22096 0
vsize: 88548
[startup+610.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 21811 0 0 0 60933 74 0 0 25 0 1 0 408221388 90673152 20956 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22137 20956 603 41 0 22096 0
vsize: 88548
[startup+620.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 21811 0 0 0 61933 74 0 0 25 0 1 0 408221388 90673152 20956 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22137 20956 603 41 0 22096 0
vsize: 88548
[startup+630.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 21811 0 0 0 62933 74 0 0 25 0 1 0 408221388 90673152 20956 4294967295 134512640 134672761 3221224560 3221223696 134614739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22137 20956 603 41 0 22096 0
vsize: 88548
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 21811 0 0 0 63933 74 0 0 25 0 1 0 408221388 90673152 20956 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22137 20956 603 41 0 22096 0
vsize: 88548
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 21811 0 0 0 64933 74 0 0 25 0 1 0 408221388 90673152 20956 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22137 20956 603 41 0 22096 0
vsize: 88548
[startup+660.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 21811 0 0 0 65932 74 0 0 25 0 1 0 408221388 90673152 20956 4294967295 134512640 134672761 3221224560 3221223600 134603512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22137 20956 603 41 0 22096 0
vsize: 88548
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 21811 0 0 0 66932 74 0 0 25 0 1 0 408221388 90673152 20956 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22137 20956 603 41 0 22096 0
vsize: 88548
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 21811 0 0 0 67932 74 0 0 25 0 1 0 408221388 90673152 20956 4294967295 134512640 134672761 3221224560 3221223600 134612819 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22137 20956 603 41 0 22096 0
vsize: 88548
[startup+690.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 21811 0 0 0 68933 74 0 0 25 0 1 0 408221388 90673152 20956 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22137 20956 603 41 0 22096 0
vsize: 88548
[startup+700.016 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 21815 0 0 0 69933 74 0 0 25 0 1 0 408221388 90673152 20960 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22137 20960 603 41 0 22096 0
vsize: 88548
[startup+710.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23241 0 0 0 70929 78 0 0 25 0 1 0 408221388 97300480 22322 4294967295 134512640 134672761 3221224560 3221222820 1075347027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23755 22322 603 41 0 23714 0
vsize: 95020
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23547 0 0 0 71926 81 0 0 25 0 1 0 408221388 92557312 21228 4294967295 134512640 134672761 3221224560 3221223104 134621068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22597 21228 603 41 0 22556 0
vsize: 90388
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23547 0 0 0 72926 81 0 0 25 0 1 0 408221388 92557312 21228 4294967295 134512640 134672761 3221224560 3221223104 134621095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22597 21228 603 41 0 22556 0
vsize: 90388
[startup+740.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23547 0 0 0 73927 81 0 0 25 0 1 0 408221388 92557312 21228 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22597 21228 603 41 0 22556 0
vsize: 90388
[startup+750.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23547 0 0 0 74926 81 0 0 25 0 1 0 408221388 92557312 21228 4294967295 134512640 134672761 3221224560 3221223104 134621090 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22597 21228 603 41 0 22556 0
vsize: 90388
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23594 0 0 0 75926 81 0 0 25 0 1 0 408221388 91181056 21060 4294967295 134512640 134672761 3221224560 3221222864 134621829 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22261 21060 603 41 0 22220 0
vsize: 89044
[startup+770.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23594 0 0 0 76926 81 0 0 25 0 1 0 408221388 91181056 21060 4294967295 134512640 134672761 3221224560 3221223008 134643963 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22261 21060 603 41 0 22220 0
vsize: 89044
[startup+780.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23594 0 0 0 77926 81 0 0 25 0 1 0 408221388 91181056 21060 4294967295 134512640 134672761 3221224560 3221223008 134643577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22261 21060 603 41 0 22220 0
vsize: 89044
[startup+790.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23594 0 0 0 78927 81 0 0 25 0 1 0 408221388 91181056 21060 4294967295 134512640 134672761 3221224560 3221223008 134643996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22261 21060 603 41 0 22220 0
vsize: 89044
[startup+800.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23594 0 0 0 79927 81 0 0 25 0 1 0 408221388 91181056 21060 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22261 21060 603 41 0 22220 0
vsize: 89044
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23762 0 0 0 80926 82 0 0 25 0 1 0 408221388 91181056 21060 4294967295 134512640 134672761 3221224560 3221223008 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22261 21060 603 41 0 22220 0
vsize: 89044
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23815 0 0 0 81927 82 0 0 25 0 1 0 408221388 91144192 21055 4294967295 134512640 134672761 3221224560 3221223744 134615985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21055 603 41 0 22211 0
vsize: 89008
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23816 0 0 0 82927 82 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23816 0 0 0 83927 82 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223512 1075347236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+850.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23816 0 0 0 84927 82 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+860.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23816 0 0 0 85927 82 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+870.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23816 0 0 0 86927 82 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+880.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23816 0 0 0 87928 82 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+890.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23816 0 0 0 88928 82 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+900.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23816 0 0 0 89928 82 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+910.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23816 0 0 0 90928 82 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23816 0 0 0 91928 82 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+930.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23816 0 0 0 92928 82 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+940.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30692
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23816 0 0 0 93929 82 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+950.023 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 30733
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23816 0 0 0 94928 82 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+960.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30745
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23816 0 0 0 95920 91 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+970.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30745
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23899 0 0 0 96919 91 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+980.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30745
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23899 0 0 0 97920 91 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+990.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30745
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23899 0 0 0 98920 91 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30745
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23899 0 0 0 99920 91 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30745
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23899 0 0 0 100920 91 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30747
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23899 0 0 0 101920 91 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30747
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23899 0 0 0 102920 91 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223696 134614753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30747
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23899 0 0 0 103921 91 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30747
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23899 0 0 0 104921 91 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30747
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23899 0 0 0 105921 91 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30747
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23899 0 0 0 106921 91 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223696 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30747
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23899 0 0 0 107921 91 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30747
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23899 0 0 0 108921 91 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30747
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23899 0 0 0 109921 91 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30747
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23899 0 0 0 110921 91 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30747
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23899 0 0 0 111921 91 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30747
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23899 0 0 0 112922 91 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134616023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30747
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23899 0 0 0 113922 91 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30747
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23899 0 0 0 114922 91 0 0 25 0 1 0 408221388 91144192 21056 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21056 603 41 0 22211 0
vsize: 89008
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30747
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23900 0 0 0 115922 91 0 0 25 0 1 0 408221388 91144192 21057 4294967295 134512640 134672761 3221224560 3221223432 1075352743 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21057 603 41 0 22211 0
vsize: 89008
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30747
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23904 0 0 0 116922 91 0 0 25 0 1 0 408221388 91144192 21061 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21061 603 41 0 22211 0
vsize: 89008
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30747
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 23907 0 0 0 117922 91 0 0 25 0 1 0 408221388 91144192 21064 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21064 603 41 0 22211 0
vsize: 89008
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30747
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 24027 0 0 0 118922 92 0 0 25 0 1 0 408221388 91672576 21184 4294967295 134512640 134672761 3221224560 3221223744 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22381 21184 603 41 0 22340 0
vsize: 89524
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30747
Raw data (stat): 30692 (minisat+) R 30691 26667 26666 0 -1 0 24406 0 0 0 119921 93 0 0 25 0 1 0 408221388 92696576 21457 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22631 21457 603 41 0 22590 0
vsize: 90524
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 30747
Raw data (stat): 30692 (minisat+) Z 30691 26667 26666 0 -1 12 24407 0 0 0 119921 98 0 0 25 0 1 0 408221388 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.08
CPU time (s): 1200.2
CPU user time (s): 1199.22
CPU system time (s): 0.988849
CPU usage (%): 100.01
Max. virtual memory (Kb): 95020
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####