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-jac3.opb
MD5SUM	43952ea8e0659c6ffd861c99c0b605de
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	15
Optimality of the best value was proved	NO
Number of terms in the objective function	1732
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	1732
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	1732
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.05384
Number of variables	1731
Total number of constraints	1254
Number of constraints which are clauses	1254
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	694
Trace number 4665

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-13 19:44:29 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3454 boxname=wulflinc25 idbench=70 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  43952ea8e0659c6ffd861c99c0b605de  /oldhome/oroussel/tmp/wulflinc25/normalized-jac3.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc25/normalized-jac3.opb /oldhome/oroussel/tmp/wulflinc25/normalized-jac3.opb
IDLAUNCH: 3454
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        907032 kB
Buffers:         32388 kB
Cached:          60872 kB
SwapCached:         36 kB
Active:          42876 kB
Inactive:        53216 kB
HighTotal:      131008 kB
HighFree:        66444 kB
LowTotal:       903652 kB
LowFree:        840588 kB
SwapTotal:     2097892 kB
SwapFree:      2097856 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            25996 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:04:31 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 3454 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1254 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 |    1254    24011 |     418       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 3454   maxlim: 1706   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |   25374   110144 |    8458       1       48    48.0 |  0.000 % |
c |       101 |   25227   109639 |    9303      74      279     3.8 |  0.655 % |
c |       251 |   25118   109262 |   10234     210      726     3.5 |  1.021 % |
c |       476 |   25118   109262 |   11257     435     1541     3.5 |  1.021 % |
c |       814 |   25109   109233 |   12383     772     2902     3.8 |  1.059 % |
c |      1320 |   25091   109173 |   13621    1274     5108     4.0 |  1.117 % |
c |      2082 |   25091   109173 |   14983    2036    27273    13.4 |  1.117 % |
c |      3225 |   25091   109173 |   16482    3179    87927    27.7 |  1.117 % |
c |      4933 |   25082   109142 |   18130    4886   177914    36.4 |  1.136 % |
c ==============================================================================
c [1mFound solution: 24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1708   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7388 |   25088   109172 |    8362    7341   448878    61.1 |  1.136 % |
c |      7489 |   25088   109172 |    9198    7442   453760    61.0 |  1.174 % |
c |      7640 |   25088   109172 |   10118    7593   470365    61.9 |  1.174 % |
c |      7865 |   25088   109172 |   11129    7818   492352    63.0 |  1.174 % |
c |      8204 |   25065   109093 |   12242    8154   550268    67.5 |  1.251 % |
c |      8712 |   25065   109093 |   13467    8662   621977    71.8 |  1.251 % |
c |      9472 |   25065   109093 |   14813    9422   844500    89.6 |  1.251 % |
c |     10613 |   25065   109093 |   16295   10563  1097381   103.9 |  1.251 % |
c |     12325 |   24982   108777 |   17924   12261  1560650   127.3 |  1.502 % |
c ==============================================================================
c [1mFound solution: 22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1710   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14762 |   24984   108792 |    8328   14698  2168437   147.5 |  1.502 % |
c |     14864 |   24984   108792 |    9160    7451  1150014   154.3 |  1.540 % |
c |     15014 |   24984   108792 |   10076    7601  1152620   151.6 |  1.540 % |
c |     15239 |   24984   108792 |   11084    7826  1164076   148.7 |  1.540 % |
c |     15576 |   24984   108792 |   12193    8163  1202775   147.3 |  1.540 % |
c |     16082 |   24776   108101 |   13412    8638  1264604   146.4 |  2.272 % |
c |     16842 |   24776   108101 |   14753    9398  1374337   146.2 |  2.271 % |
c |     17985 |   24776   108101 |   16228   10541  1565716   148.5 |  2.271 % |
c ==============================================================================
c [1mFound solution: 21[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1711   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18154 |   24777   108105 |    8259   10710  1579603   147.5 |  2.271 % |
c |     18256 |   24777   108105 |    9084    5457   411220    75.4 |  2.290 % |
c |     18408 |   24777   108105 |    9993    5609   420559    75.0 |  2.290 % |
c |     18635 |   24777   108105 |   10992    5836   443940    76.1 |  2.290 % |
c |     18974 |   24777   108105 |   12092    6175   493494    79.9 |  2.290 % |
c |     19481 |   24709   107869 |   13301    6647   563892    84.8 |  2.521 % |
c |     20240 |   24709   107869 |   14631    7406   718156    97.0 |  2.521 % |
c |     21380 |   24709   107869 |   16094    8546   930702   108.9 |  2.521 % |
c |     23088 |   24709   107869 |   17703   10254  1407662   137.3 |  2.521 % |
c |     25653 |   24700   107840 |   19474   12817  2150402   167.8 |  2.559 % |
c |     29498 |   24694   107820 |   21421   16659  4057436   243.6 |  2.578 % |
c ==============================================================================
c [1mFound solution: 20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1712   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29903 |   24697   107834 |    8232   17064  4210420   246.7 |  2.578 % |
c |     30003 |   24697   107834 |    9055    4366   641824   147.0 |  2.597 % |
c |     30153 |   24697   107834 |    9960    4516   644405   142.7 |  2.597 % |
c |     30378 |   24697   107834 |   10956    4741   652615   137.7 |  2.597 % |
c |     30715 |   24697   107834 |   12052    5078   676886   133.3 |  2.597 % |
c |     31221 |   24617   107558 |   13257    5574   743364   133.4 |  2.866 % |
c |     31981 |   24617   107558 |   14583    6334   902979   142.6 |  2.866 % |
c |     33123 |   24617   107558 |   16041    7476  1108735   148.3 |  2.866 % |
c |     34831 |   24617   107558 |   17646    9184  1355570   147.6 |  2.866 % |
c |     37397 |   24617   107558 |   19410   11750  1840952   156.7 |  2.866 % |
c ==============================================================================
c [1mFound solution: 19[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1713   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39404 |   24618   107565 |    8206   13757  2546341   185.1 |  2.866 % |
c |     39504 |   24618   107565 |    9026    6979  1020955   146.3 |  2.885 % |
c |     39654 |   24618   107565 |    9929    7129  1024044   143.6 |  2.885 % |
c |     39879 |   24618   107565 |   10922    7354  1032057   140.3 |  2.885 % |
c |     40218 |   24618   107565 |   12014    7693  1047920   136.2 |  2.885 % |
c |     40727 |   24618   107565 |   13215    8202  1110145   135.4 |  2.885 % |
c |     41488 |   24618   107565 |   14537    8963  1325838   147.9 |  2.885 % |
c |     42628 |   24618   107565 |   15991   10103  1636575   162.0 |  2.885 % |
c |     44339 |   24592   107475 |   17590   11809  2053738   173.9 |  2.962 % |
c ==============================================================================
c [1mFound solution: 18[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1714   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44817 |   24571   107406 |    8190   12281  2119350   172.6 |  2.962 % |
c |     44917 |   24571   107406 |    9009    6241   658796   105.6 |  3.057 % |
c |     45068 |   24571   107406 |    9909    6392   665240   104.1 |  3.057 % |
c |     45293 |   24571   107406 |   10900    6617   683272   103.3 |  3.057 % |
c |     45637 |   24571   107406 |   11990    6961   729705   104.8 |  3.057 % |
c |     46144 |   24571   107406 |   13190    7468   816071   109.3 |  3.057 % |
c |     46904 |   24571   107406 |   14509    8228   948842   115.3 |  3.057 % |
c |     48043 |   24571   107406 |   15959    9367  1126413   120.3 |  3.057 % |
c |     49752 |   24571   107406 |   17555   11076  1474950   133.2 |  3.057 % |
c |     52317 |   24571   107406 |   19311   13641  1925230   141.1 |  3.057 % |
c |     56163 |   24571   107406 |   21242   17487  2713393   155.2 |  3.057 % |
c |     61930 |   24571   107406 |   23367   12144  1553805   127.9 |  3.057 % |
c |     70581 |   24571   107406 |   25703   20795  4961583   238.6 |  3.057 % |
c |     83555 |   24571   107406 |   28274   20335  5732422   281.9 |  3.057 % |
c |    103019 |   24571   107406 |   31101   24951  6735497   269.9 |  3.057 % |
c |    132220 |   24571   107406 |   34211   20208  7355737   364.0 |  3.057 % |
c |    176009 |   24571   107406 |   37632   25501  9197945   360.7 |  3.057 % |
c |    241693 |   24571   107406 |   41396   23616  9249375   391.7 |  3.057 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 -x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 x74 -x75 -x76 -x77 x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 -x101 -x102 -x103 -x104 -x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 -x192 -x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 -x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 -x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 -x266 -x267 -x268 -x269 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 -x301 -x302 -x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 -x317 -x318 -x319 -x320 -x321 -x322 -x323 -x324 -x325 -x326 -x327 -x328 -x329 -x330 -x331 -x332 -x333 -x334 -x335 -x336 -x337 -x338 -x339 -x340 -x341 -x342 -x343 -x344 -x345 -x346 -x347 -x348 -x349 -x350 -x351 -x352 -x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 -x361 -x362 -x363 -x364 -x365 -x366 -x367 -x368 -x369 -x370 -x371 -x372 -x373 -x374 -x375 -x376 -x377 -x378 -x379 -x380 -x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 -x389 -x390 -x391 -x392 -x393 -x394 -x395 -x396 -x397 -x398 x399 -x400 -x401 -x402 -x403 -x404 -x405 -x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 -x415 -x416 -x417 -x418 -x419 -x420 -x421 -x422 x423 -x424 x425 -x426 -x427 -x428 -x429 -x430 -x431 x432 -x433 -x434 -x435 -x436 -x437 -x438 -x439 -x440 -x441 -x442 -x443 -x444 -x445 -x446 -x447 -x448 -x449 -x450 -x451 -x452 -x453 -x454 -x455 -x456 -x457 -x458 -x459 -x460 -x461 -x462 -x463 -x464 -x465 -x466 -x467 -x468 -x469 -x470 -x471 -x472 -x473 -x474 -x475 -x476 -x477 -x478 -x479 -x480 -x481 -x482 -x483 -x484 -x485 -x486 -x487 -x488 -x489 -x490 -x491 -x492 -x493 -x494 -x495 -x496 -x497 -x498 -x499 -x500 -x501 -x502 -x503 -x504 -x505 -x506 -x507 -x508 -x509 -x510 -x511 -x512 -x513 -x514 -x515 -x516 -x517 -x518 -x519 -x520 -x521 -x522 -x523 -x524 -x525 -x526 -x527 -x528 -x529 -x530 -x531 -x532 -x533 -x534 -x535 -x536 -x537 -x538 -x539 -x540 -x541 -x542 -x543 -x544 -x545 -x546 -x547 -x548 -x549 -x550 -x551 -x552 -x553 -x554 -x555 -x556 -x557 -x558 -x559 -x560 -x561 -x562 -x563 -x564 -x565 -x566 -x567 -x568 -x569 -x570 -x571 -x572 -x573 -x574 -x575 -x576 -x577 -x578 -x579 -x580 -x581 -x582 -x583 -x584 -x585 -x586 -x587 -x588 -x589 -x590 -x591 -x592 -x593 -x594 -x595 -x596 -x597 -x598 -x599 -x600 -x601 -x602 -x603 -x604 -x605 -x606 -x607 -x608 -x609 -x610 -x611 -x612 -x613 -x614 -x615 -x616 -x617 -x618 -x619 -x620 -x621 -x622 -x623 -x624 -x625 -x626 -x627 -x628 -x629 -x630 -x631 -x632 -x633 -x634 -x635 -x636 -x637 -x638 -x639 -x640 -x641 -x642 -x643 x644 -x645 -x646 -x647 -x648 -x649 -x650 -x651 -x652 -x653 -x654 -x655 -x656 -x657 -x658 -x659 -x660 -x661 -x662 -x663 -x664 -x665 -x666 -x667 -x668 -x669 -x670 -x671 -x672 -x673 -x674 -x675 -x676 -x677 -x678 -x679 -x680 -x681 -x682 -x683 -x684 -x685 -x686 -x687 -x688 -x689 -x690 -x691 -x692 -x693 -x694 -x695 -x696 -x697 -x698 -x699 -x700 -x701 -x702 -x703 -x704 -x705 -x706 -x707 -x708 -x709 -x710 -x711 -x712 -x713 -x714 -x715 -x716 -x717 -x718 -x719 -x720 -x721 -x722 -x723 -x724 -x725 -x726 -x727 -x728 -x729 -x730 -x731 -x732 -x733 -x734 -x735 -x736 -x737 -x738 -x739 -x740 -x741 -x742 -x743 -x744 -x745 -x746 -x747 -x748 -x749 -x750 -x751 -x752 -x753 -x754 -x755 -x756 -x757 -x758 -x759 -x760 -x761 -x762 -x763 -x764 -x765 -x766 -x767 -x768 -x769 -x770 x771 -x772 -x773 -x774 -x775 -x776 -x777 -x778 -x779 -x780 -x781 -x782 -x783 -x784 -x785 -x786 -x787 -x788 -x789 -x790 -x791 -x792 -x793 -x794 -x795 -x796 -x797 -x798 -x799 -x800 -x801 -x802 -x803 -x804 -x805 -x806 -x807 -x808 -x809 -x810 -x811 -x812 -x813 -x814 -x815 -x816 -x817 -x818 -x819 -x820 -x821 -x822 -x823 -x824 -x825 -x826 -x827 -x828 -x829 -x830 -x831 -x832 -x833 -x834 x835 -x836 -x837 -x838 -x839 -x840 -x841 -x842 -x843 -x844 -x845 -x846 -x847 -x848 -x849 -x850 -x851 -x852 -x853 -x854 -x855 -x856 -x857 -x858 -x859 -x860 -x861 -x862 -x863 -x864 -x865 -x866 -x867 -x868 -x869 -x870 -x871 -x872 -x873 -x874 -x875 -x876 -x877 -x878 -x879 -x880 -x881 -x882 -x883 -x884 -x885 -x886 -x887 -x888 -x889 -x890 -x891 -x892 -x893 -x894 -x895 -x896 -x897 -x898 -x899 -x900 -x901 -x902 -x903 -x904 -x905 -x906 -x907 -x908 -x909 -x910 -x911 -x912 -x913 -x914 -x915 -x916 -x917 -x918 -x919 -x920 -x921 -x922 -x923 -x924 -x925 -x926 -x927 -x928 -x929 -x930 -x931 -x932 -x933 -x934 -x935 -x936 -x937 -x938 -x939 -x940 -x941 -x942 -x943 -x944 -x945 -x946 -x947 -x948 -x949 -x950 -x951 -x952 -x953 -x954 -x955 -x956 -x957 -x958 -x959 -x960 -x961 -x962 -x963 -x964 -x965 -x966 -x967 -x968 -x969 -x970 -x971 -x972 -x973 -x974 -x975 -x976 -x977 -x978 -x979 -x980 -x981 -x982 -x983 -x984 -x985 -x986 -x987 -x988 -x989 -x990 -x991 -x992 -x993 -x994 -x995 -x996 -x997 -x998 -x999 -x1000 -x1001 -x1002 -x1003 -x1004 -x1005 -x1006 -x1007 -x1008 -x1009 -x1010 -x1011 -x1012 -x1013 -x1014 -x1015 -x1016 -x1017 -x1018 -x1019 -x1020 -x1021 -x1022 -x1023 -x1024 -x1025 -x1026 -x1027 -x1028 -x1029 -x1030 -x1031 -x1032 -x1033 -x1034 -x1035 -x1036 -x1037 -x1038 -x1039 -x1040 -x1041 -x1042 -x1043 -x1044 -x1045 -x1046 -x1047 -x1048 -x1049 -x1050 -x1051 -x1052 -x1053 -x1054 -x1055 -x1056 -x1057 -x1058 -x1059 -x1060 -x1061 -x1062 -x1063 -x1064 -x1065 -x1066 x1067 -x1068 -x1069 -x1070 -x1071 -x1072 -x1073 -x1074 -x1075 -x1076 -x1077 -x1078 -x1079 -x1080 -x1081 -x1082 -x1083 -x1084 -x1085 -x1086 -x1087 -x1088 -x1089 -x1090 -x1091 -x1092 -x1093 -x1094 -x1095 -x1096 -x1097 -x1098 -x1099 -x1100 -x1101 -x1102 -x1103 -x1104 -x1105 -x1106 -x1107 -x1108 -x1109 -x1110 -x1111 -x1112 -x1113 -x1114 -x1115 -x1116 x1117 -x1118 -x1119 -x1120 -x1121 -x1122 -x1123 -x1124 -x1125 -x1126 -x1127 -x1128 -x1129 -x1130 -x1131 -x1132 -x1133 -x1134 -x1135 -x1136 -x1137 -x1138 -x1139 -x1140 -x1141 -x1142 -x1143 -x1144 -x1145 -x1146 -x1147 -x1148 -x1149 -x1150 -x1151 -x1152 -x1153 -x1154 -x1155 -x1156 -x1157 -x1158 -x1159 -x1160 -x1161 -x1162 -x1163 -x1164 -x1165 -x1166 -x1167 -x1168 -x1169 -x1170 -x1171 -x1172 -x1173 -x1174 -x1175 -x1176 -x1177 -x1178 -x1179 -x1180 -x1181 -x1182 -x1183 -x1184 -x1185 -x1186 -x1187 -x1188 -x1189 -x1190 -x1191 -x1192 -x1193 -x1194 -x1195 -x1196 -x1197 -x1198 -x1199 -x1200 -x1201 -x1202 -x1203 -x1204 -x1205 -x1206 -x1207 -x1208 -x1209 -x1210 -x1211 -x1212 -x1213 -x1214 -x1215 -x1216 -x1217 -x1218 -x1219 -x1220 -x1221 -x1222 -x1223 -x1224 -x1225 -x1226 -x1227 -x1228 -x1229 -x1230 -x1231 -x1232 -x1233 -x1234 -x1235 -x1236 -x1237 -x1238 -x1239 -x1240 -x1241 -x1242 -x1243 -x1244 -x1245 -x1246 -x1247 -x1248 -x1249 -x1250 -x1251 -x1252 -x1253 -x1254 -x1255 -x1256 -x1257 -x1258 -x1259 -x1260 -x1261 -x1262 -x1263 -x1264 -x1265 -x1266 -x1267 -x1268 -x1269 -x1270 -x1271 -x1272 -x1273 -x1274 -x1275 -x1276 -x1277 -x1278 -x1279 -x1280 -x1281 -x1282 -x1283 -x1284 -x1285 -x1286 -x1287 -x1288 -x1289 -x1290 -x1291 -x1292 -x1293 -x1294 -x1295 -x1296 -x1297 -x1298 -x1299 -x1300 -x1301 -x1302 -x1303 -x1304 -x1305 -x1306 -x1307 -x1308 -x1309 -x1310 -x1311 -x1312 -x1313 -x1314 -x1315 -x1316 -x1317 -x1318 -x1319 -x1320 -x1321 -x1322 -x1323 -x1324 -x1#### 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.91 0.95 0.70 2/54 29483
Raw data (stat): 29483 (runsolver) R 29482 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478577939 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 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.93 0.95 0.70 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 1624 0 0 0 994 4 0 0 25 0 1 0 478577939 8396800 1602 4294967295 134512640 134672761 3221224576 3221223680 134555211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2050 1602 603 41 0 2009 0
vsize: 8200
[startup+19.9998 s]
Raw data (loadavg): 0.94 0.95 0.71 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 3064 0 0 0 1990 8 0 0 25 0 1 0 478577939 14188544 3042 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3464 3042 603 41 0 3423 0
vsize: 13856
[startup+30.0006 s]
Raw data (loadavg): 0.95 0.96 0.71 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 3238 0 0 0 2989 8 0 0 25 0 1 0 478577939 14876672 3216 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3632 3216 603 41 0 3591 0
vsize: 14528
[startup+39.9998 s]
Raw data (loadavg): 0.95 0.96 0.71 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 3252 0 0 0 3989 8 0 0 25 0 1 0 478577939 15007744 3230 4294967295 134512640 134672761 3221224576 3221223680 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3664 3230 603 41 0 3623 0
vsize: 14656
[startup+50.0005 s]
Raw data (loadavg): 0.96 0.96 0.71 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 5034 0 0 0 4986 12 0 0 25 0 1 0 478577939 22405120 5012 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5470 5012 603 41 0 5429 0
vsize: 21880
[startup+60.0006 s]
Raw data (loadavg): 0.97 0.96 0.72 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 5421 0 0 0 5985 13 0 0 25 0 1 0 478577939 23871488 5399 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5828 5399 603 41 0 5787 0
vsize: 23312
[startup+70.0007 s]
Raw data (loadavg): 0.97 0.96 0.72 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 5421 0 0 0 6984 13 0 0 25 0 1 0 478577939 23871488 5399 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5828 5399 603 41 0 5787 0
vsize: 23312
[startup+80.0013 s]
Raw data (loadavg): 0.98 0.96 0.72 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 5421 0 0 0 7984 13 0 0 25 0 1 0 478577939 23859200 5399 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5825 5399 603 41 0 5784 0
vsize: 23300
[startup+90.0011 s]
Raw data (loadavg): 0.98 0.96 0.73 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 5421 0 0 0 8985 13 0 0 25 0 1 0 478577939 23859200 5399 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5825 5399 603 41 0 5784 0
vsize: 23300
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.73 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 5421 0 0 0 9985 13 0 0 25 0 1 0 478577939 23859200 5399 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5825 5399 603 41 0 5784 0
vsize: 23300
[startup+110.001 s]
Raw data (loadavg): 0.98 0.96 0.73 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 5421 0 0 0 10985 13 0 0 25 0 1 0 478577939 23859200 5399 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5825 5399 603 41 0 5784 0
vsize: 23300
[startup+120.001 s]
Raw data (loadavg): 0.99 0.96 0.73 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 5423 0 0 0 11985 13 0 0 25 0 1 0 478577939 23859200 5401 4294967295 134512640 134672761 3221224576 3221223744 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5825 5401 603 41 0 5784 0
vsize: 23300
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 5426 0 0 0 12985 13 0 0 25 0 1 0 478577939 23859200 5404 4294967295 134512640 134672761 3221224576 3221223760 134559193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5825 5404 603 41 0 5784 0
vsize: 23300
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 5426 0 0 0 13985 13 0 0 25 0 1 0 478577939 23859200 5404 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5825 5404 603 41 0 5784 0
vsize: 23300
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 5426 0 0 0 14986 13 0 0 25 0 1 0 478577939 23859200 5404 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5825 5404 603 41 0 5784 0
vsize: 23300
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 6622 0 0 0 15983 16 0 0 25 0 1 0 478577939 28872704 6600 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7049 6600 603 41 0 7008 0
vsize: 28196
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 7405 0 0 0 16982 18 0 0 25 0 1 0 478577939 31956992 7383 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7802 7383 603 41 0 7761 0
vsize: 31208
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 8322 0 0 0 17979 20 0 0 25 0 1 0 478577939 35700736 8300 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8716 8300 603 41 0 8675 0
vsize: 34864
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 8662 0 0 0 18978 22 0 0 25 0 1 0 478577939 37171200 8640 4294967295 134512640 134672761 3221224576 3221223680 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9075 8640 603 41 0 9034 0
vsize: 36300
[startup+200 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 8662 0 0 0 19978 22 0 0 25 0 1 0 478577939 37171200 8640 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9075 8640 603 41 0 9034 0
vsize: 36300
[startup+210 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 8662 0 0 0 20979 22 0 0 25 0 1 0 478577939 37171200 8640 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9075 8640 603 41 0 9034 0
vsize: 36300
[startup+220 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 8662 0 0 0 21979 22 0 0 25 0 1 0 478577939 37171200 8640 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9075 8640 603 41 0 9034 0
vsize: 36300
[startup+229.999 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 9190 0 0 0 22977 23 0 0 25 0 1 0 478577939 39313408 9168 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9598 9168 603 41 0 9557 0
vsize: 38392
[startup+239.999 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 10128 0 0 0 23975 25 0 0 25 0 1 0 478577939 43163648 10106 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10538 10106 603 41 0 10497 0
vsize: 42152
[startup+249.999 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 10652 0 0 0 24974 27 0 0 25 0 1 0 478577939 45289472 10630 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11057 10630 603 41 0 11016 0
vsize: 44228
[startup+259.999 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 10652 0 0 0 25974 27 0 0 25 0 1 0 478577939 45289472 10630 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11057 10630 603 41 0 11016 0
vsize: 44228
[startup+269.999 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 10652 0 0 0 26974 27 0 0 25 0 1 0 478577939 45289472 10630 4294967295 134512640 134672761 3221224576 3221223712 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11057 10630 603 41 0 11016 0
vsize: 44228
[startup+279.999 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 10653 0 0 0 27975 27 0 0 25 0 1 0 478577939 45289472 10631 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11057 10631 603 41 0 11016 0
vsize: 44228
[startup+289.999 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 10654 0 0 0 28975 27 0 0 25 0 1 0 478577939 45289472 10632 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11057 10632 603 41 0 11016 0
vsize: 44228
[startup+300 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 10654 0 0 0 29975 27 0 0 25 0 1 0 478577939 45289472 10632 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11057 10632 603 41 0 11016 0
vsize: 44228
[startup+309.999 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 10654 0 0 0 30975 27 0 0 25 0 1 0 478577939 45289472 10632 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11057 10632 603 41 0 11016 0
vsize: 44228
[startup+319.999 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 10655 0 0 0 31975 27 0 0 25 0 1 0 478577939 45289472 10633 4294967295 134512640 134672761 3221224576 3221223680 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11057 10633 603 41 0 11016 0
vsize: 44228
[startup+329.998 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 10656 0 0 0 32976 27 0 0 25 0 1 0 478577939 45289472 10634 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11057 10634 603 41 0 11016 0
vsize: 44228
[startup+339.998 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 10656 0 0 0 33976 27 0 0 25 0 1 0 478577939 45289472 10634 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11057 10634 603 41 0 11016 0
vsize: 44228
[startup+349.998 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 10656 0 0 0 34976 27 0 0 25 0 1 0 478577939 45289472 10634 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11057 10634 603 41 0 11016 0
vsize: 44228
[startup+360 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 10656 0 0 0 35976 27 0 0 25 0 1 0 478577939 45289472 10634 4294967295 134512640 134672761 3221224576 3221223680 134560250 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11057 10634 603 41 0 11016 0
vsize: 44228
[startup+369.999 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 10656 0 0 0 36976 27 0 0 25 0 1 0 478577939 45289472 10634 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11057 10634 603 41 0 11016 0
vsize: 44228
[startup+379.998 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 10656 0 0 0 37977 27 0 0 25 0 1 0 478577939 45289472 10634 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11057 10634 603 41 0 11016 0
vsize: 44228
[startup+389.998 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 10822 0 0 0 38976 27 0 0 25 0 1 0 478577939 45953024 10800 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11219 10800 603 41 0 11178 0
vsize: 44876
[startup+399.998 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 12161 0 0 0 39973 30 0 0 25 0 1 0 478577939 51445760 12139 4294967295 134512640 134672761 3221224576 3221223744 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12560 12139 603 41 0 12519 0
vsize: 50240
[startup+409.998 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 13459 0 0 0 40970 33 0 0 25 0 1 0 478577939 56938496 13437 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13901 13437 603 41 0 13860 0
vsize: 55604
[startup+419.998 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 13553 0 0 0 41970 34 0 0 25 0 1 0 478577939 57344000 13531 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13531 603 41 0 13959 0
vsize: 56000
[startup+429.999 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 13553 0 0 0 42970 34 0 0 25 0 1 0 478577939 57344000 13531 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14000 13531 603 41 0 13959 0
vsize: 56000
[startup+439.998 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 13553 0 0 0 43970 34 0 0 25 0 1 0 478577939 57344000 13531 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14000 13531 603 41 0 13959 0
vsize: 56000
[startup+449.998 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 13553 0 0 0 44969 34 0 0 25 0 1 0 478577939 57344000 13531 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13531 603 41 0 13959 0
vsize: 56000
[startup+459.999 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 13553 0 0 0 45969 34 0 0 25 0 1 0 478577939 57344000 13531 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13531 603 41 0 13959 0
vsize: 56000
[startup+469.999 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 13553 0 0 0 46970 34 0 0 25 0 1 0 478577939 57344000 13531 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13531 603 41 0 13959 0
vsize: 56000
[startup+479.998 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 13553 0 0 0 47970 34 0 0 25 0 1 0 478577939 57344000 13531 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13531 603 41 0 13959 0
vsize: 56000
[startup+489.998 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 13720 0 0 0 48970 34 0 0 25 0 1 0 478577939 58019840 13698 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14165 13698 603 41 0 14124 0
vsize: 56660
[startup+499.998 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 14983 0 0 0 49968 36 0 0 25 0 1 0 478577939 63209472 14961 4294967295 134512640 134672761 3221224576 3221223680 134560352 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15432 14961 603 41 0 15391 0
vsize: 61728
[startup+509.998 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 15441 0 0 0 50967 37 0 0 25 0 1 0 478577939 65073152 15419 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15887 15419 603 41 0 15846 0
vsize: 63548
[startup+519.998 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 15441 0 0 0 51967 37 0 0 25 0 1 0 478577939 65073152 15419 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15887 15419 603 41 0 15846 0
vsize: 63548
[startup+529.998 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 15441 0 0 0 52967 37 0 0 25 0 1 0 478577939 65073152 15419 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15887 15419 603 41 0 15846 0
vsize: 63548
[startup+539.998 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 15441 0 0 0 53967 37 0 0 25 0 1 0 478577939 65073152 15419 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15887 15419 603 41 0 15846 0
vsize: 63548
[startup+549.999 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 15441 0 0 0 54967 37 0 0 25 0 1 0 478577939 65073152 15419 4294967295 134512640 134672761 3221224576 3221223680 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15887 15419 603 41 0 15846 0
vsize: 63548
[startup+559.999 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 15441 0 0 0 55968 37 0 0 25 0 1 0 478577939 65073152 15419 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15887 15419 603 41 0 15846 0
vsize: 63548
[startup+569.999 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 15441 0 0 0 56968 37 0 0 25 0 1 0 478577939 65073152 15419 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15887 15419 603 41 0 15846 0
vsize: 63548
[startup+579.998 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 15441 0 0 0 57968 37 0 0 25 0 1 0 478577939 65073152 15419 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15887 15419 603 41 0 15846 0
vsize: 63548
[startup+589.999 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 15441 0 0 0 58968 38 0 0 25 0 1 0 478577939 65073152 15419 4294967295 134512640 134672761 3221224576 3221223744 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15887 15419 603 41 0 15846 0
vsize: 63548
[startup+600 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 15441 0 0 0 59968 38 0 0 25 0 1 0 478577939 65073152 15419 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15887 15419 603 41 0 15846 0
vsize: 63548
[startup+609.999 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 15860 0 0 0 60967 39 0 0 25 0 1 0 478577939 66805760 15838 4294967295 134512640 134672761 3221224576 3221223744 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16310 15838 603 41 0 16269 0
vsize: 65240
[startup+619.999 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 15987 0 0 0 61967 39 0 0 25 0 1 0 478577939 67325952 15965 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16437 15965 603 41 0 16396 0
vsize: 65748
[startup+629.999 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 15987 0 0 0 62967 39 0 0 25 0 1 0 478577939 67325952 15965 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16437 15965 603 41 0 16396 0
vsize: 65748
[startup+639.999 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 15987 0 0 0 63968 39 0 0 25 0 1 0 478577939 67325952 15965 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16437 15965 603 41 0 16396 0
vsize: 65748
[startup+649.999 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 15987 0 0 0 64968 39 0 0 25 0 1 0 478577939 67325952 15965 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16437 15965 603 41 0 16396 0
vsize: 65748
[startup+660 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 15987 0 0 0 65968 39 0 0 25 0 1 0 478577939 67325952 15965 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16437 15965 603 41 0 16396 0
vsize: 65748
[startup+670 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 15987 0 0 0 66968 39 0 0 25 0 1 0 478577939 67325952 15965 4294967295 134512640 134672761 3221224576 3221223760 134559625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16437 15965 603 41 0 16396 0
vsize: 65748
[startup+680 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 15987 0 0 0 67968 39 0 0 25 0 1 0 478577939 67325952 15965 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16437 15965 603 41 0 16396 0
vsize: 65748
[startup+690 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 16391 0 0 0 68967 40 0 0 25 0 1 0 478577939 68947968 16369 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16833 16369 603 41 0 16792 0
vsize: 67332
[startup+700.001 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 17289 0 0 0 69966 42 0 0 25 0 1 0 478577939 72581120 17267 4294967295 134512640 134672761 3221224576 3221223680 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17720 17267 603 41 0 17679 0
vsize: 70880
[startup+710 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 18136 0 0 0 70964 44 0 0 25 0 1 0 478577939 76042240 18114 4294967295 134512640 134672761 3221224576 3221223680 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18565 18114 603 41 0 18524 0
vsize: 74260
[startup+720 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 18927 0 0 0 71962 46 0 0 25 0 1 0 478577939 79384576 18905 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19381 18905 603 41 0 19340 0
vsize: 77524
[startup+730 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 19241 0 0 0 72961 47 0 0 25 0 1 0 478577939 80584704 19219 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19674 19219 603 41 0 19633 0
vsize: 78696
[startup+740 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 19241 0 0 0 73961 47 0 0 25 0 1 0 478577939 80584704 19219 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19674 19219 603 41 0 19633 0
vsize: 78696
[startup+750 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 19242 0 0 0 74962 47 0 0 25 0 1 0 478577939 80584704 19220 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19674 19220 603 41 0 19633 0
vsize: 78696
[startup+760.001 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 19242 0 0 0 75962 47 0 0 25 0 1 0 478577939 80584704 19220 4294967295 134512640 134672761 3221224576 3221223680 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19674 19220 603 41 0 19633 0
vsize: 78696
[startup+770 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 19242 0 0 0 76962 47 0 0 25 0 1 0 478577939 80584704 19220 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19674 19220 603 41 0 19633 0
vsize: 78696
[startup+780 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 19242 0 0 0 77962 47 0 0 25 0 1 0 478577939 80584704 19220 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19674 19220 603 41 0 19633 0
vsize: 78696
[startup+790 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 19242 0 0 0 78962 47 0 0 25 0 1 0 478577939 80584704 19220 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19674 19220 603 41 0 19633 0
vsize: 78696
[startup+800 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 19242 0 0 0 79963 47 0 0 25 0 1 0 478577939 80584704 19220 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19674 19220 603 41 0 19633 0
vsize: 78696
[startup+810 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 19242 0 0 0 80963 47 0 0 25 0 1 0 478577939 80584704 19220 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19674 19220 603 41 0 19633 0
vsize: 78696
[startup+820 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 19242 0 0 0 81963 47 0 0 25 0 1 0 478577939 80584704 19220 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19674 19220 603 41 0 19633 0
vsize: 78696
[startup+830 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 19242 0 0 0 82963 47 0 0 25 0 1 0 478577939 80584704 19220 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19674 19220 603 41 0 19633 0
vsize: 78696
[startup+840 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 19242 0 0 0 83963 47 0 0 25 0 1 0 478577939 80584704 19220 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19674 19220 603 41 0 19633 0
vsize: 78696
[startup+850.001 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 19242 0 0 0 84964 47 0 0 25 0 1 0 478577939 80584704 19220 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19674 19220 603 41 0 19633 0
vsize: 78696
[startup+860.001 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 19242 0 0 0 85964 47 0 0 25 0 1 0 478577939 80584704 19220 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19674 19220 603 41 0 19633 0
vsize: 78696
[startup+870 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 19242 0 0 0 86964 47 0 0 25 0 1 0 478577939 80584704 19220 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19674 19220 603 41 0 19633 0
vsize: 78696
[startup+880 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 19242 0 0 0 87964 47 0 0 25 0 1 0 478577939 80584704 19220 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19674 19220 603 41 0 19633 0
vsize: 78696
[startup+890 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 19242 0 0 0 88964 47 0 0 25 0 1 0 478577939 80584704 19220 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19674 19220 603 41 0 19633 0
vsize: 78696
[startup+900.001 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 19882 0 0 0 89963 48 0 0 25 0 1 0 478577939 83255296 19860 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20326 19860 603 41 0 20285 0
vsize: 81304
[startup+910 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 20634 0 0 0 90961 50 0 0 25 0 1 0 478577939 86315008 20612 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21073 20612 603 41 0 21032 0
vsize: 84292
[startup+919.999 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21182 0 0 0 91960 52 0 0 25 0 1 0 478577939 88707072 21160 4294967295 134512640 134672761 3221224576 3221223680 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21657 21160 603 41 0 21616 0
vsize: 86628
[startup+929.999 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 29483
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21384 0 0 0 92959 53 0 0 25 0 1 0 478577939 89501696 21362 4294967295 134512640 134672761 3221224576 3221223760 134558920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21362 603 41 0 21810 0
vsize: 87404
[startup+939.999 s]
Raw data (loadavg): 1.07 0.99 0.86 2/58 29526
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21384 0 0 0 93959 53 0 0 25 0 1 0 478577939 89501696 21362 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21362 603 41 0 21810 0
vsize: 87404
[startup+949.999 s]
Raw data (loadavg): 1.06 0.99 0.86 2/54 29536
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21384 0 0 0 94959 53 0 0 25 0 1 0 478577939 89501696 21362 4294967295 134512640 134672761 3221224576 3221223532 1075350777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21362 603 41 0 21810 0
vsize: 87404
[startup+959.999 s]
Raw data (loadavg): 1.05 0.99 0.86 2/54 29536
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21384 0 0 0 95959 53 0 0 25 0 1 0 478577939 89501696 21362 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21362 603 41 0 21810 0
vsize: 87404
[startup+969.999 s]
Raw data (loadavg): 1.04 0.99 0.86 2/54 29536
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21384 0 0 0 96960 53 0 0 25 0 1 0 478577939 89501696 21362 4294967295 134512640 134672761 3221224576 3221223680 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21362 603 41 0 21810 0
vsize: 87404
[startup+979.999 s]
Raw data (loadavg): 1.04 0.99 0.87 2/54 29536
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21384 0 0 0 97960 53 0 0 25 0 1 0 478577939 89501696 21362 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21362 603 41 0 21810 0
vsize: 87404
[startup+989.999 s]
Raw data (loadavg): 1.03 0.99 0.87 2/54 29536
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21384 0 0 0 98960 53 0 0 25 0 1 0 478577939 89501696 21362 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21362 603 41 0 21810 0
vsize: 87404
[startup+999.999 s]
Raw data (loadavg): 1.03 0.99 0.87 2/54 29536
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21384 0 0 0 99960 53 0 0 25 0 1 0 478577939 89501696 21362 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21362 603 41 0 21810 0
vsize: 87404
[startup+1010 s]
Raw data (loadavg): 1.02 0.99 0.87 2/54 29536
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21384 0 0 0 100960 53 0 0 25 0 1 0 478577939 89501696 21362 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21362 603 41 0 21810 0
vsize: 87404
[startup+1020 s]
Raw data (loadavg): 1.02 0.99 0.87 2/54 29538
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21384 0 0 0 101961 53 0 0 25 0 1 0 478577939 89501696 21362 4294967295 134512640 134672761 3221224576 3221223680 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21362 603 41 0 21810 0
vsize: 87404
[startup+1030 s]
Raw data (loadavg): 1.01 0.99 0.87 2/54 29538
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21385 0 0 0 102961 53 0 0 25 0 1 0 478577939 89501696 21363 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21363 603 41 0 21810 0
vsize: 87404
[startup+1040 s]
Raw data (loadavg): 1.01 0.99 0.87 2/54 29538
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21385 0 0 0 103961 53 0 0 25 0 1 0 478577939 89501696 21363 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21363 603 41 0 21810 0
vsize: 87404
[startup+1050 s]
Raw data (loadavg): 1.01 0.99 0.87 2/54 29538
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21386 0 0 0 104961 53 0 0 25 0 1 0 478577939 89501696 21364 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21364 603 41 0 21810 0
vsize: 87404
[startup+1060 s]
Raw data (loadavg): 1.01 0.99 0.87 2/54 29538
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21386 0 0 0 105961 53 0 0 25 0 1 0 478577939 89501696 21364 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21364 603 41 0 21810 0
vsize: 87404
[startup+1070 s]
Raw data (loadavg): 1.01 0.99 0.87 2/54 29538
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21386 0 0 0 106962 53 0 0 25 0 1 0 478577939 89501696 21364 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21364 603 41 0 21810 0
vsize: 87404
[startup+1080 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 29538
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21386 0 0 0 107962 53 0 0 25 0 1 0 478577939 89501696 21364 4294967295 134512640 134672761 3221224576 3221223744 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21364 603 41 0 21810 0
vsize: 87404
[startup+1090 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 29538
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21386 0 0 0 108961 53 0 0 25 0 1 0 478577939 89501696 21364 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21364 603 41 0 21810 0
vsize: 87404
[startup+1100 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 29538
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21386 0 0 0 109962 53 0 0 25 0 1 0 478577939 89501696 21364 4294967295 134512640 134672761 3221224576 3221223760 134559512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21364 603 41 0 21810 0
vsize: 87404
[startup+1110 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 29538
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21386 0 0 0 110962 53 0 0 25 0 1 0 478577939 89501696 21364 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21364 603 41 0 21810 0
vsize: 87404
[startup+1120 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 29538
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21386 0 0 0 111962 53 0 0 25 0 1 0 478577939 89501696 21364 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21364 603 41 0 21810 0
vsize: 87404
[startup+1130 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 29538
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21386 0 0 0 112962 53 0 0 25 0 1 0 478577939 89501696 21364 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21364 603 41 0 21810 0
vsize: 87404
[startup+1140 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 29538
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21386 0 0 0 113962 53 0 0 25 0 1 0 478577939 89501696 21364 4294967295 134512640 134672761 3221224576 3221223760 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21364 603 41 0 21810 0
vsize: 87404
[startup+1150 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 29538
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21386 0 0 0 114963 53 0 0 25 0 1 0 478577939 89501696 21364 4294967295 134512640 134672761 3221224576 3221223760 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21364 603 41 0 21810 0
vsize: 87404
[startup+1160 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 29538
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21386 0 0 0 115963 53 0 0 25 0 1 0 478577939 89501696 21364 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21364 603 41 0 21810 0
vsize: 87404
[startup+1170 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 29538
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21386 0 0 0 116963 53 0 0 25 0 1 0 478577939 89501696 21364 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21364 603 41 0 21810 0
vsize: 87404
[startup+1180 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 29538
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21386 0 0 0 117963 53 0 0 25 0 1 0 478577939 89501696 21364 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21364 603 41 0 21810 0
vsize: 87404
[startup+1190 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 29538
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21388 0 0 0 118963 53 0 0 25 0 1 0 478577939 89501696 21366 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21366 603 41 0 21810 0
vsize: 87404
[startup+1200 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 29538
Raw data (stat): 29483 (minisat+) R 29482 28099 28098 0 -1 0 21389 0 0 0 119963 53 0 0 25 0 1 0 478577939 89501696 21367 4294967295 134512640 134672761 3221224576 3221223744 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 21367 603 41 0 21810 0
vsize: 87404
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.89 1/54 29538
Raw data (stat): 29483 (minisat+) Z 29482 28099 28098 0 -1 12 21392 0 0 0 119964 57 0 0 25 0 1 0 478577939 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.05
CPU time (s): 1200.22
CPU user time (s): 1199.64
CPU system time (s): 0.573912
CPU usage (%): 100.014
Max. virtual memory (Kb): 87404
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####