PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii16d2.opb
MD5SUM	640e42314ccc494338715717ba212e02
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	785
Optimality of the best value was proved	NO
Number of terms in the objective function	1672
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	1672
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	1672
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	19.988
Number of variables	1672
Total number of constraints	13297
Number of constraints which are clauses	13297
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	16
Trace number 4686

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-13 19:49:47 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3527 boxname=wulflinc31 idbench=143 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  640e42314ccc494338715717ba212e02  /oldhome/oroussel/tmp/wulflinc31/normalized-ii16d2.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc31/normalized-ii16d2.opb /oldhome/oroussel/tmp/wulflinc31/normalized-ii16d2.opb
IDLAUNCH: 3527
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        912420 kB
Buffers:         34280 kB
Cached:          49444 kB
SwapCached:        392 kB
Active:          44616 kB
Inactive:        42312 kB
HighTotal:      131008 kB
HighFree:        77840 kB
LowTotal:       903652 kB
LowFree:        834580 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            29808 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:09:49 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 3527 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 13297 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 |   13297    39436 |    4432       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 810[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 3336   maxlim: 862   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        58 |   36597   122645 |   12199      58     1458    25.1 |  0.000 % |
c |       158 |   36597   122645 |   13418     158     4175    26.4 |  0.159 % |
c |       308 |   36597   122645 |   14760     308     8107    26.3 |  0.159 % |
c |       533 |   36597   122645 |   16236     533    16085    30.2 |  0.159 % |
c |       871 |   36597   122645 |   17860     871    25298    29.0 |  0.159 % |
c |      1378 |   36597   122645 |   19646    1378    36255    26.3 |  0.159 % |
c |      2137 |   36597   122645 |   21611    2137    53525    25.0 |  0.159 % |
c ==============================================================================
c [1mFound solution: 804[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 868   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2577 |   36602   122680 |   12200    2577    58694    22.8 |  0.159 % |
c |      2677 |   36602   122680 |   13420    2677    62265    23.3 |  0.219 % |
c |      2827 |   36602   122680 |   14762    2827    67743    24.0 |  0.219 % |
c |      3053 |   36602   122680 |   16238    3053    75185    24.6 |  0.219 % |
c |      3390 |   36602   122680 |   17862    3390    83655    24.7 |  0.219 % |
c |      3896 |   36602   122680 |   19648    3896    90372    23.2 |  0.219 % |
c |      4655 |   36602   122680 |   21613    4655   105247    22.6 |  0.219 % |
c |      5794 |   36602   122680 |   23774    5794   127516    22.0 |  0.219 % |
c |      7503 |   36602   122680 |   26151    7503   167019    22.3 |  0.219 % |
c |     10066 |   36602   122680 |   28766   10066   299755    29.8 |  0.219 % |
c |     13911 |   36602   122680 |   31643   13911   755576    54.3 |  0.219 % |
c |     19679 |   36602   122680 |   34808   19679  1418288    72.1 |  0.219 % |
c |     28329 |   36497   122454 |   38288   28203  2462961    87.3 |  0.259 % |
c ==============================================================================
c [1mFound solution: 803[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 3304   maxlim: 868   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28898 |   59572   204851 |   19857   28772  2486654    86.4 |  0.259 % |
c |     28999 |   59572   204851 |   21842   14053  1429081   101.7 |  0.228 % |
c |     29155 |   59572   204851 |   24026   14209  1432056   100.8 |  0.228 % |
c |     29380 |   59572   204851 |   26429   14434  1435615    99.5 |  0.228 % |
c |     29718 |   59572   204851 |   29072   14772  1440884    97.5 |  0.228 % |
c |     30224 |   59572   204851 |   31979   15278  1449813    94.9 |  0.228 % |
c |     30985 |   59572   204851 |   35177   16039  1476494    92.1 |  0.228 % |
c |     32124 |   59562   204813 |   38695   17052  1528889    89.7 |  0.240 % |
c |     33832 |   59562   204813 |   42565   18760  1685284    89.8 |  0.240 % |
c |     36394 |   59562   204813 |   46821   21322  1931137    90.6 |  0.240 % |
c |     40238 |   59562   204813 |   51503   25166  2101738    83.5 |  0.240 % |
c ==============================================================================
c [1mFound solution: 802[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 869   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40480 |   59563   204824 |   19854   25408  2104584    82.8 |  0.240 % |
c |     40580 |   59563   204824 |   21839   12804   663304    51.8 |  0.252 % |
c |     40730 |   59563   204824 |   24023   12954   664893    51.3 |  0.252 % |
c |     40956 |   59563   204824 |   26425   13180   668196    50.7 |  0.252 % |
c |     41294 |   59563   204824 |   29068   13518   679140    50.2 |  0.252 % |
c |     41800 |   59563   204824 |   31975   14024   685070    48.8 |  0.252 % |
c |     42559 |   59563   204824 |   35172   14783   698054    47.2 |  0.252 % |
c |     43699 |   59563   204824 |   38689   15923   779219    48.9 |  0.252 % |
c |     45408 |   59563   204824 |   42558   17632   881683    50.0 |  0.252 % |
c |     47971 |   59563   204824 |   46814   20195  1204890    59.7 |  0.252 % |
c |     51817 |   59563   204824 |   51496   24041  1796909    74.7 |  0.252 % |
c |     57583 |   59563   204824 |   56645   29807  2532401    85.0 |  0.252 % |
c |     66232 |   59563   204824 |   62310   38456  3838939    99.8 |  0.252 % |
c |     79208 |   59563   204824 |   68541   51432  6304858   122.6 |  0.252 % |
c |     98670 |   59563   204824 |   75395   70894 10562350   149.0 |  0.252 % |
c ==============================================================================
c [1mFound solution: 799[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 872   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99856 |   59567   204851 |   19855   72080 10608917   147.2 |  0.252 % |
c |     99957 |   59567   204851 |   21840   16395  2796222   170.6 |  0.276 % |
c |    100107 |   59567   204851 |   24024   16545  2797482   169.1 |  0.276 % |
c |    100333 |   59567   204851 |   26427   16771  2802557   167.1 |  0.276 % |
c |    100670 |   59567   204851 |   29069   17108  2811200   164.3 |  0.276 % |
c |    101178 |   59567   204851 |   31976   17616  2819201   160.0 |  0.276 % |
c |    101938 |   59567   204851 |   35174   18376  2897212   157.7 |  0.276 % |
c |    103078 |   59567   204851 |   38691   19516  2917182   149.5 |  0.276 % |
c |    104786 |   59567   204851 |   42560   21224  2962674   139.6 |  0.276 % |
c |    107350 |   59567   204851 |   46817   23788  3241575   136.3 |  0.276 % |
c |    111194 |   59567   204851 |   51498   27632  3552329   128.6 |  0.276 % |
c ==============================================================================
c [1mFound solution: 798[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 873   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    115957 |   59568   204862 |   19856   32395  4249280   131.2 |  0.276 % |
c |    116059 |   59568   204862 |   21841   14474  1299881    89.8 |  0.288 % |
c |    116209 |   59568   204862 |   24025   14624  1301630    89.0 |  0.288 % |
c |    116434 |   59568   204862 |   26428   14849  1305718    87.9 |  0.288 % |
c |    116771 |   59568   204862 |   29071   15186  1311107    86.3 |  0.288 % |
c |    117277 |   59568   204862 |   31978   15692  1324193    84.4 |  0.288 % |
c |    118036 |   59568   204862 |   35176   16451  1338535    81.4 |  0.288 % |
c |    119175 |   59568   204862 |   38693   17590  1382128    78.6 |  0.288 % |
c |    120883 |   59568   204862 |   42563   19298  1524686    79.0 |  0.288 % |
c ==============================================================================
c [1mFound solution: 797[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 874   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    122701 |   59573   204890 |   19857   21116  1719946    81.5 |  0.288 % |
c |    122801 |   59573   204890 |   21842   10658   472484    44.3 |  0.300 % |
c |    122952 |   59573   204890 |   24026   10809   475616    44.0 |  0.300 % |
c |    123178 |   59573   204890 |   26429   11035   479054    43.4 |  0.300 % |
c |    123516 |   59573   204890 |   29072   11373   488824    43.0 |  0.300 % |
c |    124022 |   59573   204890 |   31979   11879   517521    43.6 |  0.300 % |
c |    124782 |   59573   204890 |   35177   12639   559298    44.3 |  0.300 % |
c |    125921 |   59573   204890 |   38695   13778   661783    48.0 |  0.300 % |
c |    127629 |   59573   204890 |   42565   15486   806553    52.1 |  0.300 % |
c |    130191 |   59573   204890 |   46821   18048  1100469    61.0 |  0.300 % |
c |    134036 |   59573   204890 |   51503   21893  1592536    72.7 |  0.300 % |
c |    139802 |   59573   204890 |   56654   27659  2369997    85.7 |  0.300 % |
c |    148451 |   59573   204890 |   62319   36308  3843882   105.9 |  0.300 % |
c |    161425 |   59573   204890 |   68551   49282  6525942   132.4 |  0.300 % |
c |    180888 |   59573   204890 |   75406   68745  9950203   144.7 |  0.300 % |
c |    210080 |   59573   204890 |   82947   32317  6196960   191.8 |  0.300 % |
c |    253869 |   59573   204890 |   91242   76106 14386959   189.0 |  0.300 % |
c |    319554 |   59573   204890 |  100366   61445 13471043   219.2 |  0.300 % |
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 -x1325 x1326 x1327 -x1328 -x1329 x1330 -x1331 x1332 -x1333 x1334 x1335 -x1336 -x1337 x1338 x1339 -x1340 -x1341 x1342 -x1343 x1344 -x1345 x1346 -x1347 x1348 -x1349 x1350 x1351 -x1352 -x1353 x1354 -x1355 x1356 -x1357 x1358 x1359 -x1360 -x1361 x1362 x1363 -x1364 -x1365 x1366 -x1367 x1368 x1369 -x1370 -x1371 x1372 -x1373 x1374 -x1375 -x1376 x1377 -x1378 -x1379 x1380 -x1381 x1382 -x1383 x1384 -x1385 x1386 -x1387 x1388 -x1389 x1390 x1391 -x1392 x1393 -x1394 -x1395 x1396 -x1397 x1398 -x1399 x1400 -x1401 x1402 x1403 -x1404 -x1405 x1406 -x1407 x1408 -x1409 x1410 -x1411 x1412 x1413 -x1414 x1415 -x1416 -x1417 x1418 x1419 -x1420 #### 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.93 0.95 0.79 2/54 25285
Raw data (stat): 25285 (runsolver) R 25284 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478587294 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+9.99987 s]
Raw data (loadavg): 0.94 0.96 0.79 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 1559 0 0 0 994 5 0 0 25 0 1 0 478587294 7950336 1537 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1941 1537 603 41 0 1900 0
vsize: 7764
[startup+20.001 s]
Raw data (loadavg): 0.95 0.96 0.80 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 2718 0 0 0 1990 8 0 0 25 0 1 0 478587294 12677120 2696 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3095 2696 603 41 0 3054 0
vsize: 12380
[startup+30.0019 s]
Raw data (loadavg): 0.95 0.96 0.80 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 3729 0 0 0 2986 13 0 0 25 0 1 0 478587294 16842752 3707 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4112 3707 603 41 0 4071 0
vsize: 16448
[startup+40.0018 s]
Raw data (loadavg): 0.96 0.96 0.80 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 4168 0 0 0 3984 14 0 0 25 0 1 0 478587294 18976768 4146 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4633 4146 603 41 0 4592 0
vsize: 18532
[startup+50.0028 s]
Raw data (loadavg): 0.97 0.96 0.80 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 4169 0 0 0 4984 14 0 0 25 0 1 0 478587294 18976768 4146 4294967295 134512640 134672761 3221224576 3221223760 134558756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4633 4146 603 41 0 4592 0
vsize: 18532
[startup+60.0027 s]
Raw data (loadavg): 0.97 0.96 0.80 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 4169 0 0 0 5984 15 0 0 25 0 1 0 478587294 18976768 4146 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4633 4146 603 41 0 4592 0
vsize: 18532
[startup+70.0036 s]
Raw data (loadavg): 0.97 0.96 0.81 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 4331 0 0 0 6983 16 0 0 25 0 1 0 478587294 19652608 4308 4294967295 134512640 134672761 3221224576 3221223728 134565070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4798 4308 603 41 0 4757 0
vsize: 19192
[startup+80.0045 s]
Raw data (loadavg): 0.98 0.96 0.81 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 5047 0 0 0 7981 18 0 0 25 0 1 0 478587294 22732800 5024 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5550 5024 603 41 0 5509 0
vsize: 22200
[startup+90.0045 s]
Raw data (loadavg): 0.98 0.96 0.81 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 5728 0 0 0 8978 21 0 0 25 0 1 0 478587294 25411584 5705 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6204 5705 603 41 0 6163 0
vsize: 24816
[startup+100.006 s]
Raw data (loadavg): 0.98 0.96 0.81 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 6476 0 0 0 9976 23 0 0 25 0 1 0 478587294 28504064 6453 4294967295 134512640 134672761 3221224576 3221223712 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6959 6453 603 41 0 6918 0
vsize: 27836
[startup+110.006 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 7169 0 0 0 10975 25 0 0 25 0 1 0 478587294 31330304 7146 4294967295 134512640 134672761 3221224576 3221223680 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7649 7146 603 41 0 7608 0
vsize: 30596
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.82 3/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 7715 0 0 0 11972 27 0 0 25 0 1 0 478587294 33615872 7692 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8207 7692 603 41 0 8166 0
vsize: 32828
[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 8276 0 0 0 12971 29 0 0 25 0 1 0 478587294 35901440 8253 4294967295 134512640 134672761 3221224576 3221223680 134560002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8765 8253 603 41 0 8724 0
vsize: 35060
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 8979 0 0 0 13968 32 0 0 25 0 1 0 478587294 38727680 8956 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9455 8956 603 41 0 9414 0
vsize: 37820
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 9687 0 0 0 14966 34 0 0 25 0 1 0 478587294 41553920 9664 4294967295 134512640 134672761 3221224576 3221223680 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10145 9664 603 41 0 10104 0
vsize: 40580
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 10340 0 0 0 15963 37 0 0 25 0 1 0 478587294 44249088 10317 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10803 10317 603 41 0 10762 0
vsize: 43212
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 10989 0 0 0 16960 39 0 0 25 0 1 0 478587294 46940160 10966 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11460 10966 603 41 0 11419 0
vsize: 45840
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 11616 0 0 0 17958 42 0 0 25 0 1 0 478587294 49758208 11593 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12148 11593 603 41 0 12107 0
vsize: 48592
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 12215 0 0 0 18956 44 0 0 25 0 1 0 478587294 52183040 12192 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12740 12192 603 41 0 12699 0
vsize: 50960
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 12743 0 0 0 19954 46 0 0 25 0 1 0 478587294 54333440 12720 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13265 12720 603 41 0 13224 0
vsize: 53060
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 12784 0 0 0 20954 46 0 0 25 0 1 0 478587294 54452224 12761 4294967295 134512640 134672761 3221224576 3221223760 134559332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13294 12761 603 41 0 13253 0
vsize: 53176
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 12784 0 0 0 21954 47 0 0 25 0 1 0 478587294 54452224 12761 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13294 12761 603 41 0 13253 0
vsize: 53176
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 12784 0 0 0 22953 47 0 0 25 0 1 0 478587294 54452224 12761 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13294 12761 603 41 0 13253 0
vsize: 53176
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 12784 0 0 0 23953 48 0 0 25 0 1 0 478587294 54452224 12761 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13294 12761 603 41 0 13253 0
vsize: 53176
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 12784 0 0 0 24952 48 0 0 25 0 1 0 478587294 54452224 12761 4294967295 134512640 134672761 3221224576 3221223680 134559760 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13294 12761 603 41 0 13253 0
vsize: 53176
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 12784 0 0 0 25952 49 0 0 25 0 1 0 478587294 54452224 12761 4294967295 134512640 134672761 3221224576 3221223760 134559367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13294 12761 603 41 0 13253 0
vsize: 53176
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 12784 0 0 0 26951 49 0 0 25 0 1 0 478587294 54452224 12761 4294967295 134512640 134672761 3221224576 3221223680 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13294 12761 603 41 0 13253 0
vsize: 53176
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 12784 0 0 0 27951 50 0 0 25 0 1 0 478587294 54452224 12761 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13294 12761 603 41 0 13253 0
vsize: 53176
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 12784 0 0 0 28951 50 0 0 25 0 1 0 478587294 54452224 12761 4294967295 134512640 134672761 3221224576 3221223680 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13294 12761 603 41 0 13253 0
vsize: 53176
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 12784 0 0 0 29950 51 0 0 25 0 1 0 478587294 54452224 12761 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13294 12761 603 41 0 13253 0
vsize: 53176
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 12784 0 0 0 30950 51 0 0 25 0 1 0 478587294 54452224 12761 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13294 12761 603 41 0 13253 0
vsize: 53176
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 12784 0 0 0 31950 52 0 0 25 0 1 0 478587294 54452224 12761 4294967295 134512640 134672761 3221224576 3221223680 134560393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13294 12761 603 41 0 13253 0
vsize: 53176
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 12784 0 0 0 32950 52 0 0 25 0 1 0 478587294 54452224 12761 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13294 12761 603 41 0 13253 0
vsize: 53176
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 12784 0 0 0 33949 52 0 0 25 0 1 0 478587294 54452224 12761 4294967295 134512640 134672761 3221224576 3221223760 134558937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13294 12761 603 41 0 13253 0
vsize: 53176
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 12784 0 0 0 34949 53 0 0 25 0 1 0 478587294 54452224 12761 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13294 12761 603 41 0 13253 0
vsize: 53176
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 12784 0 0 0 35949 53 0 0 25 0 1 0 478587294 54452224 12761 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13294 12761 603 41 0 13253 0
vsize: 53176
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 12784 0 0 0 36949 53 0 0 25 0 1 0 478587294 54452224 12761 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13294 12761 603 41 0 13253 0
vsize: 53176
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 12838 0 0 0 37948 54 0 0 25 0 1 0 478587294 54722560 12815 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13360 12815 603 41 0 13319 0
vsize: 53440
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 13426 0 0 0 38946 56 0 0 25 0 1 0 478587294 57139200 13403 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13950 13403 603 41 0 13909 0
vsize: 55800
[startup+400.018 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 13870 0 0 0 39945 57 0 0 25 0 1 0 478587294 58888192 13847 4294967295 134512640 134672761 3221224576 3221223680 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13847 603 41 0 14336 0
vsize: 57508
[startup+410.019 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 14365 0 0 0 40944 59 0 0 25 0 1 0 478587294 60911616 14342 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14871 14342 603 41 0 14830 0
vsize: 59484
[startup+420.019 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 14495 0 0 0 41943 59 0 0 25 0 1 0 478587294 61448192 14472 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15002 14472 603 41 0 14961 0
vsize: 60008
[startup+430.019 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 14495 0 0 0 42943 60 0 0 25 0 1 0 478587294 61448192 14472 4294967295 134512640 134672761 3221224576 3221223680 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15002 14472 603 41 0 14961 0
vsize: 60008
[startup+440.019 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 14495 0 0 0 43943 60 0 0 25 0 1 0 478587294 61448192 14472 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15002 14472 603 41 0 14961 0
vsize: 60008
[startup+450.02 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 14495 0 0 0 44943 60 0 0 25 0 1 0 478587294 61448192 14472 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15002 14472 603 41 0 14961 0
vsize: 60008
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 14495 0 0 0 45943 60 0 0 25 0 1 0 478587294 61448192 14472 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15002 14472 603 41 0 14961 0
vsize: 60008
[startup+470.02 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 14495 0 0 0 46943 60 0 0 25 0 1 0 478587294 61448192 14472 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15002 14472 603 41 0 14961 0
vsize: 60008
[startup+480.021 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 14495 0 0 0 47942 61 0 0 25 0 1 0 478587294 61448192 14472 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15002 14472 603 41 0 14961 0
vsize: 60008
[startup+490.021 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 14495 0 0 0 48942 61 0 0 25 0 1 0 478587294 61448192 14472 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15002 14472 603 41 0 14961 0
vsize: 60008
[startup+500.022 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 14495 0 0 0 49942 62 0 0 25 0 1 0 478587294 61448192 14472 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15002 14472 603 41 0 14961 0
vsize: 60008
[startup+510.022 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 14496 0 0 0 50941 62 0 0 25 0 1 0 478587294 61448192 14473 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15002 14473 603 41 0 14961 0
vsize: 60008
[startup+520.023 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 14496 0 0 0 51941 63 0 0 25 0 1 0 478587294 61448192 14473 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15002 14473 603 41 0 14961 0
vsize: 60008
[startup+530.024 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 14496 0 0 0 52941 63 0 0 25 0 1 0 478587294 61448192 14473 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15002 14473 603 41 0 14961 0
vsize: 60008
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 14496 0 0 0 53941 63 0 0 25 0 1 0 478587294 61448192 14473 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15002 14473 603 41 0 14961 0
vsize: 60008
[startup+550.026 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 14496 0 0 0 54941 64 0 0 25 0 1 0 478587294 61448192 14473 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15002 14473 603 41 0 14961 0
vsize: 60008
[startup+560.026 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 14496 0 0 0 55940 64 0 0 25 0 1 0 478587294 61448192 14473 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15002 14473 603 41 0 14961 0
vsize: 60008
[startup+570.026 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 14496 0 0 0 56940 64 0 0 25 0 1 0 478587294 61448192 14473 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15002 14473 603 41 0 14961 0
vsize: 60008
[startup+580.026 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 14887 0 0 0 57938 66 0 0 25 0 1 0 478587294 63053824 14864 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15394 14864 603 41 0 15353 0
vsize: 61576
[startup+590.026 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 15350 0 0 0 58937 67 0 0 25 0 1 0 478587294 64933888 15327 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15853 15327 603 41 0 15812 0
vsize: 63412
[startup+600.027 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 15763 0 0 0 59936 69 0 0 25 0 1 0 478587294 66674688 15740 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16278 15740 603 41 0 16237 0
vsize: 65112
[startup+610.027 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 25285
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 16164 0 0 0 60935 70 0 0 25 0 1 0 478587294 68280320 16141 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16670 16141 603 41 0 16629 0
vsize: 66680
[startup+620.027 s]
Raw data (loadavg): 1.07 0.99 0.87 3/57 25325
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 16606 0 0 0 61932 72 0 0 25 0 1 0 478587294 70148096 16583 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17126 16583 603 41 0 17085 0
vsize: 68504
[startup+630.029 s]
Raw data (loadavg): 1.06 0.99 0.87 2/54 25338
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 17018 0 0 0 62931 73 0 0 25 0 1 0 478587294 71766016 16995 4294967295 134512640 134672761 3221224576 3221223680 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17521 16995 603 41 0 17480 0
vsize: 70084
[startup+640.03 s]
Raw data (loadavg): 1.05 0.99 0.87 2/54 25338
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 17432 0 0 0 63930 74 0 0 25 0 1 0 478587294 73515008 17409 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17948 17409 603 41 0 17907 0
vsize: 71792
[startup+650.031 s]
Raw data (loadavg): 1.04 0.99 0.87 2/54 25338
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 17925 0 0 0 64929 76 0 0 25 0 1 0 478587294 75554816 17902 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18446 17902 603 41 0 18405 0
vsize: 73784
[startup+660.031 s]
Raw data (loadavg): 1.04 0.99 0.88 2/54 25338
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 18413 0 0 0 65927 77 0 0 25 0 1 0 478587294 77565952 18390 4294967295 134512640 134672761 3221224576 3221223680 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18937 18390 603 41 0 18896 0
vsize: 75748
[startup+670.032 s]
Raw data (loadavg): 1.03 0.99 0.88 2/54 25338
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 18900 0 0 0 66926 79 0 0 25 0 1 0 478587294 79441920 18877 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19395 18877 603 41 0 19354 0
vsize: 77580
[startup+680.032 s]
Raw data (loadavg): 1.03 0.99 0.88 2/54 25338
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 19418 0 0 0 67925 80 0 0 25 0 1 0 478587294 81596416 19395 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19921 19395 603 41 0 19880 0
vsize: 79684
[startup+690.032 s]
Raw data (loadavg): 1.02 0.99 0.88 2/54 25338
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 19907 0 0 0 68924 82 0 0 25 0 1 0 478587294 83615744 19884 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20414 19884 603 41 0 20373 0
vsize: 81656
[startup+700.032 s]
Raw data (loadavg): 1.02 0.99 0.88 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 69923 82 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+710.032 s]
Raw data (loadavg): 1.01 0.99 0.88 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 70923 82 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+720.032 s]
Raw data (loadavg): 1.01 0.99 0.88 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 71923 82 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+730.032 s]
Raw data (loadavg): 1.01 0.99 0.88 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 72923 82 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+740.032 s]
Raw data (loadavg): 1.01 0.99 0.88 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 73924 82 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+750.033 s]
Raw data (loadavg): 1.01 0.99 0.88 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 74924 82 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+760.033 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 75924 82 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+770.033 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 76924 82 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223680 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+780.033 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 77924 82 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+790.033 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 78925 82 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+800.033 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 79925 82 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+810.033 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 80925 82 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+820.033 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 81925 82 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+830.033 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 82925 82 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+840.033 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 83925 82 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+850.034 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 84925 82 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223680 134559838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+860.034 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 85926 82 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+870.034 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 86926 82 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223680 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+880.034 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 87925 83 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+890.034 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 88925 83 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+900.035 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 89926 83 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+910.034 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 90926 83 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+920.034 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 25340
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 91926 83 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+930.034 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20296 0 0 0 92926 83 0 0 25 0 1 0 478587294 85225472 20273 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 20273 603 41 0 20766 0
vsize: 83228
[startup+940.034 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 20645 0 0 0 93926 83 0 0 25 0 1 0 478587294 86573056 20622 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21136 20622 603 41 0 21095 0
vsize: 84544
[startup+950.034 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 21176 0 0 0 94925 84 0 0 25 0 1 0 478587294 88854528 21153 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21693 21153 603 41 0 21652 0
vsize: 86772
[startup+960.035 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 21612 0 0 0 95924 85 0 0 25 0 1 0 478587294 90599424 21589 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22119 21589 603 41 0 22078 0
vsize: 88476
[startup+970.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 22056 0 0 0 96923 86 0 0 25 0 1 0 478587294 92344320 22033 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22545 22033 603 41 0 22504 0
vsize: 90180
[startup+980.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 22469 0 0 0 97922 87 0 0 25 0 1 0 478587294 94089216 22446 4294967295 134512640 134672761 3221224576 3221223760 134559415 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22971 22446 603 41 0 22930 0
vsize: 91884
[startup+990.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 22959 0 0 0 98920 89 0 0 25 0 1 0 478587294 96108544 22936 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23464 22936 603 41 0 23423 0
vsize: 93856
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 23523 0 0 0 99919 91 0 0 25 0 1 0 478587294 98402304 23500 4294967295 134512640 134672761 3221224576 3221223680 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24024 23500 603 41 0 23983 0
vsize: 96096
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 24040 0 0 0 100918 92 0 0 25 0 1 0 478587294 100556800 24017 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24550 24017 603 41 0 24509 0
vsize: 98200
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 24535 0 0 0 101917 93 0 0 25 0 1 0 478587294 102580224 24512 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25044 24512 603 41 0 25003 0
vsize: 100176
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 25011 0 0 0 102916 94 0 0 25 0 1 0 478587294 104468480 24988 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25505 24988 603 41 0 25464 0
vsize: 102020
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 25474 0 0 0 103915 96 0 0 25 0 1 0 478587294 106360832 25451 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25967 25451 603 41 0 25926 0
vsize: 103868
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 25922 0 0 0 104914 97 0 0 25 0 1 0 478587294 108249088 25899 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26428 25899 603 41 0 26387 0
vsize: 105712
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 25992 0 0 0 105914 97 0 0 25 0 1 0 478587294 108515328 25969 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26493 25969 603 41 0 26452 0
vsize: 105972
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 25992 0 0 0 106914 97 0 0 25 0 1 0 478587294 108515328 25969 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26493 25969 603 41 0 26452 0
vsize: 105972
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 25992 0 0 0 107914 97 0 0 25 0 1 0 478587294 108515328 25969 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26493 25969 603 41 0 26452 0
vsize: 105972
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 25992 0 0 0 108914 97 0 0 25 0 1 0 478587294 108515328 25969 4294967295 134512640 134672761 3221224576 3221223712 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26493 25969 603 41 0 26452 0
vsize: 105972
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 25992 0 0 0 109914 97 0 0 25 0 1 0 478587294 108515328 25969 4294967295 134512640 134672761 3221224576 3221223712 134560716 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26493 25969 603 41 0 26452 0
vsize: 105972
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 25992 0 0 0 110914 97 0 0 25 0 1 0 478587294 108515328 25969 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26493 25969 603 41 0 26452 0
vsize: 105972
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 25992 0 0 0 111915 97 0 0 25 0 1 0 478587294 108515328 25969 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26493 25969 603 41 0 26452 0
vsize: 105972
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 25992 0 0 0 112915 97 0 0 25 0 1 0 478587294 108515328 25969 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26493 25969 603 41 0 26452 0
vsize: 105972
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 25992 0 0 0 113915 97 0 0 25 0 1 0 478587294 108515328 25969 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26493 25969 603 41 0 26452 0
vsize: 105972
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 25992 0 0 0 114915 97 0 0 25 0 1 0 478587294 108515328 25969 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26493 25969 603 41 0 26452 0
vsize: 105972
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 25992 0 0 0 115915 97 0 0 25 0 1 0 478587294 108515328 25969 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26493 25969 603 41 0 26452 0
vsize: 105972
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 25992 0 0 0 116916 97 0 0 25 0 1 0 478587294 108515328 25969 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26493 25969 603 41 0 26452 0
vsize: 105972
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 25992 0 0 0 117916 97 0 0 25 0 1 0 478587294 108515328 25969 4294967295 134512640 134672761 3221224576 3221223680 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26493 25969 603 41 0 26452 0
vsize: 105972
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 25992 0 0 0 118916 97 0 0 25 0 1 0 478587294 108515328 25969 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26493 25969 603 41 0 26452 0
vsize: 105972
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25342
Raw data (stat): 25285 (minisat+) R 25284 23176 23175 0 -1 0 25992 0 0 0 119916 97 0 0 25 0 1 0 478587294 108515328 25969 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26493 25969 603 41 0 26452 0
vsize: 105972
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 25342
Raw data (stat): 25285 (minisat+) Z 25284 23176 23175 0 -1 12 25995 0 0 0 119916 102 0 0 25 0 1 0 478587294 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.1
CPU time (s): 1200.2
CPU user time (s): 1199.17
CPU system time (s): 1.02884
CPU usage (%): 100.009
Max. virtual memory (Kb): 105972
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####