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 5808

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-14 01:53:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4206 boxname=wulflinc21 idbench=70 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  43952ea8e0659c6ffd861c99c0b605de  /oldhome/oroussel/tmp/wulflinc21/normalized-jac3.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc21/normalized-jac3.opb /oldhome/oroussel/tmp/wulflinc21/normalized-jac3.opb
IDLAUNCH: 4206
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        879428 kB
Buffers:         27980 kB
Cached:         107340 kB
SwapCached:          0 kB
Active:          34804 kB
Inactive:       103400 kB
HighTotal:      131008 kB
HighFree:        20048 kB
LowTotal:       903652 kB
LowFree:        859380 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11504 kB
Committed_AS:    63788 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:13:30 (client local time) WITH STATUS 10 IN 1200.31 SECONDS
stats: 4206 7 1200.31 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]---> Sorter-cost:97868     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |  110205   278083 |   36735       1       48    48.0 |  0.000 % |
c |       101 |  110205   278083 |   40408     101    14250   141.1 |  0.044 % |
c |       251 |  110205   278083 |   44449     251    55613   221.6 |  0.044 % |
c |       476 |  110205   278083 |   48894     476   168307   353.6 |  0.044 % |
c ==============================================================================
c [1mFound solution: 22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       660 |  110196   278072 |   36732     660   219968   333.3 |  0.044 % |
c |       763 |  110196   278072 |   40405     763   253583   332.3 |  0.089 % |
c |       913 |  110196   278072 |   44445     913   301284   330.0 |  0.089 % |
c ==============================================================================
c [1mFound solution: 19[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       936 |  110218   278125 |   36739     936   305524   326.4 |  0.089 % |
c |      1039 |  110218   278125 |   40412    1039   338359   325.7 |  0.090 % |
c |      1189 |  110218   278125 |   44454    1189   381520   320.9 |  0.090 % |
c |      1415 |  110197   278083 |   48899    1412   432774   306.5 |  0.099 % |
c ==============================================================================
c [1mFound solution: 18[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1750 |  110163   278010 |   36721    1747   517263   296.1 |  0.099 % |
c |      1851 |  110163   278010 |   40393    1848   532389   288.1 |  0.147 % |
c |      2001 |  110163   278010 |   44432    1998   585883   293.2 |  0.147 % |
c |      2226 |  110163   278010 |   48875    2223   657899   296.0 |  0.147 % |
c |      2566 |  110163   278010 |   53763    2563   761791   297.2 |  0.147 % |
c |      3073 |  110163   278010 |   59139    3070   906805   295.4 |  0.147 % |
c |      3838 |  110163   278010 |   65053    3835  1124271   293.2 |  0.147 % |
c |      4977 |  110124   277931 |   71558    4968  1448624   291.6 |  0.165 % |
c |      6686 |  110124   277931 |   78714    6677  2048805   306.8 |  0.165 % |
c |      9250 |  110124   277931 |   86586    9241  3020614   326.9 |  0.165 % |
c |     13098 |  110124   277931 |   95244   13089  4289397   327.7 |  0.165 % |
c |     18864 |  110124   277931 |  104769   18855  5165029   273.9 |  0.165 % |
c |     27514 |  110124   277931 |  115246   27505  6636239   241.3 |  0.165 % |
c ==============================================================================
c [1mFound solution: 17[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32905 |  110137   277964 |   36712   32896  8485762   258.0 |  0.165 % |
c |     33005 |  110137   277964 |   40383   32996  8498932   257.6 |  0.166 % |
c |     33156 |  110137   277964 |   44421   33147  8527451   257.3 |  0.166 % |
c |     33384 |  110137   277964 |   48863   33375  8598579   257.6 |  0.166 % |
c |     33726 |  110137   277964 |   53750   33717  8747586   259.4 |  0.166 % |
c |     34232 |  110137   277964 |   59125   34223  8838071   258.2 |  0.166 % |
c |     34991 |  110137   277964 |   65037   34982  8985197   256.9 |  0.166 % |
c |     36130 |  110137   277964 |   71541   36121  9202755   254.8 |  0.166 % |
c |     37842 |  110137   277964 |   78695   37833  9865448   260.8 |  0.166 % |
c |     40404 |  110137   277964 |   86564   40395 10803351   267.4 |  0.166 % |
c |     44249 |  110137   277964 |   95221   44240 11888278   268.7 |  0.166 % |
c |     50018 |  110137   277964 |  104743   50009 13518821   270.3 |  0.166 % |
c |     58669 |  110137   277964 |  115217   58660 16274369   277.4 |  0.166 % |
c |     71643 |  110137   277964 |  126739   71634 20091801   280.5 |  0.166 % |
c |     91107 |  110137   277964 |  139413   91098 25758946   282.8 |  0.166 % |
c ==============================================================================
c [1mFound solution: 16[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97997 |  109438   276341 |   36479   84863 24188352   285.0 |  0.166 % |
c |     98098 |  109438   276341 |   40126   16580  4564890   275.3 |  0.839 % |
c |     98249 |  109438   276341 |   44139   16731  4596897   274.8 |  0.839 % |
c |     98474 |  109438   276341 |   48553   16956  4658844   274.8 |  0.839 % |
c |     98814 |  109438   276341 |   53408   17296  4697285   271.6 |  0.839 % |
c |     99322 |  109438   276341 |   58749   17804  4811233   270.2 |  0.839 % |
c |    100081 |  109438   276341 |   64624   18563  4970711   267.8 |  0.839 % |
c |    101220 |  109438   276341 |   71087   19702  5150917   261.4 |  0.839 % |
c |    102928 |  109438   276341 |   78195   21410  5713285   266.9 |  0.839 % |
c |    105491 |  109438   276341 |   86015   23973  6469534   269.9 |  0.839 % |
c |    109339 |  109438   276341 |   94617   27821  7284278   261.8 |  0.839 % |
c |    115105 |  109438   276341 |  104078   33587  9137507   272.1 |  0.839 % |
c |    123754 |  109438   276341 |  114486   42236 10932212   258.8 |  0.839 % |
c |    136728 |  109438   276341 |  125935   55210 14307690   259.2 |  0.839 % |
c |    156192 |  109438   276341 |  138528   74674 18686308   250.2 |  0.839 % |
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 -x#### 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.91 2/55 3395
Raw data (stat): 3395 (runsolver) R 3394 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 358045733 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.0005 s]
Raw data (loadavg): 0.93 0.95 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 6733 0 0 0 984 14 0 0 25 0 1 0 358045733 32313344 6392 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7889 6392 603 41 0 7848 0
vsize: 31556
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 7273 0 0 0 1982 16 0 0 25 0 1 0 358045733 34603008 6932 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8448 6932 603 41 0 8407 0
vsize: 33792
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 7843 0 0 0 2981 18 0 0 25 0 1 0 358045733 36880384 7502 4294967295 134512640 134672761 3221224560 3221223744 134558360 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9004 7502 603 41 0 8963 0
vsize: 36016
[startup+40.0015 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 8687 0 0 0 3978 21 0 0 25 0 1 0 358045733 40378368 8346 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9858 8346 603 41 0 9817 0
vsize: 39432
[startup+50.0021 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 9388 0 0 0 4976 23 0 0 25 0 1 0 358045733 43204608 9047 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10548 9047 603 41 0 10507 0
vsize: 42192
[startup+60.0023 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 9859 0 0 0 5976 23 0 0 25 0 1 0 358045733 45207552 9518 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11037 9518 603 41 0 10996 0
vsize: 44148
[startup+70.0026 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 10307 0 0 0 6975 24 0 0 25 0 1 0 358045733 46952448 9966 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11463 9966 603 41 0 11422 0
vsize: 45852
[startup+80.0033 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 10612 0 0 0 7974 25 0 0 25 0 1 0 358045733 48300032 10271 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11792 10271 603 41 0 11751 0
vsize: 47168
[startup+90.0029 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 10780 0 0 0 8974 26 0 0 25 0 1 0 358045733 48971776 10439 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11956 10439 603 41 0 11915 0
vsize: 47824
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 10948 0 0 0 9973 26 0 0 25 0 1 0 358045733 49639424 10607 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12119 10607 603 41 0 12078 0
vsize: 48476
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 11247 0 0 0 10972 27 0 0 25 0 1 0 358045733 50872320 10906 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12420 10906 603 41 0 12379 0
vsize: 49680
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 11527 0 0 0 11971 28 0 0 25 0 1 0 358045733 52080640 11186 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12715 11186 603 41 0 12674 0
vsize: 50860
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 11854 0 0 0 12971 29 0 0 25 0 1 0 358045733 53411840 11513 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13040 11513 603 41 0 12999 0
vsize: 52160
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 12127 0 0 0 13970 30 0 0 25 0 1 0 358045733 54480896 11786 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13301 11786 603 41 0 13260 0
vsize: 53204
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 12462 0 0 0 14969 31 0 0 25 0 1 0 358045733 55820288 12121 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13628 12121 603 41 0 13587 0
vsize: 54512
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 13006 0 0 0 15968 32 0 0 25 0 1 0 358045733 58109952 12665 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14187 12665 603 41 0 14146 0
vsize: 56748
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 13477 0 0 0 16966 34 0 0 25 0 1 0 358045733 60002304 13136 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14649 13136 603 41 0 14608 0
vsize: 58596
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 14336 0 0 0 17964 36 0 0 25 0 1 0 358045733 63479808 13995 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15498 13995 603 41 0 15457 0
vsize: 61992
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 15005 0 0 0 18962 38 0 0 25 0 1 0 358045733 66273280 14664 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16180 14664 603 41 0 16139 0
vsize: 64720
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 15447 0 0 0 19962 39 0 0 25 0 1 0 358045733 68120576 15106 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16631 15106 603 41 0 16590 0
vsize: 66524
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 15608 0 0 0 20962 39 0 0 25 0 1 0 358045733 68800512 15267 4294967295 134512640 134672761 3221224560 3221223728 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16797 15267 603 41 0 16756 0
vsize: 67188
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 16045 0 0 0 21960 41 0 0 25 0 1 0 358045733 70684672 15704 4294967295 134512640 134672761 3221224560 3221223744 134559663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17257 15704 603 41 0 17216 0
vsize: 69028
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 16803 0 0 0 22959 42 0 0 25 0 1 0 358045733 73719808 16462 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17998 16462 603 41 0 17957 0
vsize: 71992
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 17197 0 0 0 23957 44 0 0 25 0 1 0 358045733 75325440 16856 4294967295 134512640 134672761 3221224560 3221223704 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18390 16856 603 41 0 18349 0
vsize: 73560
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 17565 0 0 0 24957 45 0 0 25 0 1 0 358045733 76791808 17224 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18748 17224 603 41 0 18707 0
vsize: 74992
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 18047 0 0 0 25955 46 0 0 25 0 1 0 358045733 78798848 17706 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19238 17706 603 41 0 19197 0
vsize: 76952
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 18714 0 0 0 26954 48 0 0 25 0 1 0 358045733 81477632 18373 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19892 18373 603 41 0 19851 0
vsize: 79568
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 19085 0 0 0 27953 49 0 0 25 0 1 0 358045733 83087360 18744 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20285 18744 603 41 0 20244 0
vsize: 81140
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 19471 0 0 0 28952 50 0 0 25 0 1 0 358045733 84676608 19130 4294967295 134512640 134672761 3221224560 3221223664 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20673 19130 603 41 0 20632 0
vsize: 82692
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 19936 0 0 0 29951 51 0 0 25 0 1 0 358045733 86548480 19595 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21130 19595 603 41 0 21089 0
vsize: 84520
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 20206 0 0 0 30950 52 0 0 25 0 1 0 358045733 87629824 19865 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21394 19865 603 41 0 21353 0
vsize: 85576
[startup+320.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 20515 0 0 0 31949 53 0 0 25 0 1 0 358045733 88961024 20174 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21719 20174 603 41 0 21678 0
vsize: 86876
[startup+330.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 20797 0 0 0 32947 55 0 0 25 0 1 0 358045733 90030080 20456 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21980 20456 603 41 0 21939 0
vsize: 87920
[startup+340.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 21345 0 0 0 33946 57 0 0 25 0 1 0 358045733 92315648 21004 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22538 21004 603 41 0 22497 0
vsize: 90152
[startup+350.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 21654 0 0 0 34945 58 0 0 25 0 1 0 358045733 93548544 21313 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22839 21313 603 41 0 22798 0
vsize: 91356
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 22042 0 0 0 35944 59 0 0 25 0 1 0 358045733 95162368 21701 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23233 21701 603 41 0 23192 0
vsize: 92932
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 22432 0 0 0 36943 60 0 0 25 0 1 0 358045733 96780288 22091 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23628 22091 603 41 0 23587 0
vsize: 94512
[startup+380.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 23009 0 0 0 37941 62 0 0 25 0 1 0 358045733 99061760 22668 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24185 22668 603 41 0 24144 0
vsize: 96740
[startup+390.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3395
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 23314 0 0 0 38940 63 0 0 25 0 1 0 358045733 100409344 22973 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24514 22973 603 41 0 24473 0
vsize: 98056
[startup+400.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3448
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 23673 0 0 0 39938 65 0 0 25 0 1 0 358045733 101888000 23332 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24875 23332 603 41 0 24834 0
vsize: 99500
[startup+410.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3448
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 24143 0 0 0 40937 66 0 0 25 0 1 0 358045733 103755776 23802 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25331 23802 603 41 0 25290 0
vsize: 101324
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3448
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 24512 0 0 0 41936 67 0 0 25 0 1 0 358045733 105234432 24171 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25692 24171 603 41 0 25651 0
vsize: 102768
[startup+430.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3448
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 24883 0 0 0 42935 68 0 0 25 0 1 0 358045733 106831872 24542 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26082 24542 603 41 0 26041 0
vsize: 104328
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3448
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 25203 0 0 0 43935 69 0 0 25 0 1 0 358045733 108032000 24862 4294967295 134512640 134672761 3221224560 3221223640 134553505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26375 24862 603 41 0 26334 0
vsize: 105500
[startup+450.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3448
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 25530 0 0 0 44934 70 0 0 25 0 1 0 358045733 109625344 25189 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26764 25189 603 41 0 26723 0
vsize: 107056
[startup+460.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3450
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 25766 0 0 0 45933 71 0 0 25 0 1 0 358045733 110571520 25425 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26995 25425 603 41 0 26954 0
vsize: 107980
[startup+470.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3450
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 26180 0 0 0 46931 73 0 0 25 0 1 0 358045733 112312320 25839 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27420 25839 603 41 0 27379 0
vsize: 109680
[startup+480.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 26562 0 0 0 47930 74 0 0 25 0 1 0 358045733 113926144 26221 4294967295 134512640 134672761 3221224560 3221223760 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27814 26221 603 41 0 27773 0
vsize: 111256
[startup+490.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 26847 0 0 0 48928 75 0 0 25 0 1 0 358045733 115134464 26506 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28109 26506 603 41 0 28068 0
vsize: 112436
[startup+500.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 27108 0 0 0 49928 76 0 0 25 0 1 0 358045733 116076544 26767 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28339 26767 603 41 0 28298 0
vsize: 113356
[startup+510.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 27529 0 0 0 50927 77 0 0 25 0 1 0 358045733 117821440 27188 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28765 27188 603 41 0 28724 0
vsize: 115060
[startup+520.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 27858 0 0 0 51925 79 0 0 25 0 1 0 358045733 119173120 27517 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29095 27517 603 41 0 29054 0
vsize: 116380
[startup+530.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 28224 0 0 0 52924 80 0 0 25 0 1 0 358045733 120651776 27883 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29456 27883 603 41 0 29415 0
vsize: 117824
[startup+540.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 28683 0 0 0 53923 81 0 0 25 0 1 0 358045733 122523648 28342 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29913 28342 603 41 0 29872 0
vsize: 119652
[startup+550.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 29097 0 0 0 54922 82 0 0 25 0 1 0 358045733 124272640 28756 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30340 28756 603 41 0 30299 0
vsize: 121360
[startup+560.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 29444 0 0 0 55921 84 0 0 25 0 1 0 358045733 125751296 29103 4294967295 134512640 134672761 3221224560 3221223760 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30701 29103 603 41 0 30660 0
vsize: 122804
[startup+570.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 29679 0 0 0 56920 85 0 0 25 0 1 0 358045733 126693376 29338 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30931 29338 603 41 0 30890 0
vsize: 123724
[startup+580.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 30025 0 0 0 57920 85 0 0 25 0 1 0 358045733 128040960 29684 4294967295 134512640 134672761 3221224560 3221223760 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31260 29684 603 41 0 31219 0
vsize: 125040
[startup+590.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 30421 0 0 0 58919 86 0 0 25 0 1 0 358045733 129662976 30080 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31656 30080 603 41 0 31615 0
vsize: 126624
[startup+600.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 30858 0 0 0 59918 88 0 0 25 0 1 0 358045733 131551232 30517 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32117 30517 603 41 0 32076 0
vsize: 128468
[startup+610.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 31212 0 0 0 60917 89 0 0 25 0 1 0 358045733 132890624 30871 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32444 30871 603 41 0 32403 0
vsize: 129776
[startup+620.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 31548 0 0 0 61916 90 0 0 25 0 1 0 358045733 134361088 31207 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32803 31207 603 41 0 32762 0
vsize: 131212
[startup+630.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 31925 0 0 0 62915 91 0 0 25 0 1 0 358045733 135868416 31584 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33171 31584 603 41 0 33130 0
vsize: 132684
[startup+640.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 32233 0 0 0 63915 91 0 0 25 0 1 0 358045733 137080832 31892 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33467 31892 603 41 0 33426 0
vsize: 133868
[startup+650.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 32608 0 0 0 64914 92 0 0 25 0 1 0 358045733 138686464 32267 4294967295 134512640 134672761 3221224560 3221223664 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33859 32267 603 41 0 33818 0
vsize: 135436
[startup+660.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 32905 0 0 0 65914 93 0 0 25 0 1 0 358045733 139890688 32564 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34153 32564 603 41 0 34112 0
vsize: 136612
[startup+670.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 33209 0 0 0 66912 94 0 0 25 0 1 0 358045733 141090816 32868 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34446 32868 603 41 0 34405 0
vsize: 137784
[startup+680.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 33578 0 0 0 67912 95 0 0 25 0 1 0 358045733 142696448 33237 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34838 33237 603 41 0 34797 0
vsize: 139352
[startup+690.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 33949 0 0 0 68911 96 0 0 25 0 1 0 358045733 144158720 33608 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35195 33608 603 41 0 35154 0
vsize: 140780
[startup+700.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 34343 0 0 0 69909 97 0 0 25 0 1 0 358045733 145752064 34002 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35584 34002 603 41 0 35543 0
vsize: 142336
[startup+710.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3452
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 34675 0 0 0 70908 99 0 0 25 0 1 0 358045733 147095552 34334 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35912 34334 603 41 0 35871 0
vsize: 143648
[startup+720.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 34968 0 0 0 71908 99 0 0 25 0 1 0 358045733 148295680 34627 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36205 34627 603 41 0 36164 0
vsize: 144820
[startup+730.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35275 0 0 0 72907 100 0 0 25 0 1 0 358045733 149639168 34934 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36533 34934 603 41 0 36492 0
vsize: 146132
[startup+740.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35573 0 0 0 73906 101 0 0 25 0 1 0 358045733 150839296 35232 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36826 35232 603 41 0 36785 0
vsize: 147304
[startup+750.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 74906 102 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+760.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 75906 102 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223812 134562232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+770.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 76906 102 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+780.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 77906 102 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+790.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 78906 102 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+800.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 79906 102 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+810.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 80906 102 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+820.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 81906 102 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+830.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 82906 103 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+840.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 83907 103 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+850.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 84906 103 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223664 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+860.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 85906 103 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+870.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 86906 103 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223728 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+880.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 87906 103 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+890.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 88906 103 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+900.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 89916 103 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+910.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 90916 103 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+920.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 91917 104 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+930.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 92917 104 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+940.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 93917 104 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+950.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 94917 104 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223744 134559108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+960.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 95917 104 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+970.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 96916 104 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+980.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 97917 104 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223664 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+990.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 98917 104 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223728 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+1000.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 99917 104 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+1010.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 100917 104 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+1020.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 101917 104 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223576 1075352749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+1030.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 102917 104 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+1040.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 103917 104 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223664 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+1050.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35796 0 0 0 104917 105 0 0 25 0 1 0 358045733 151646208 35455 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35455 603 41 0 36982 0
vsize: 148092
[startup+1060.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35797 0 0 0 105917 105 0 0 25 0 1 0 358045733 151646208 35456 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35456 603 41 0 36982 0
vsize: 148092
[startup+1070.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35799 0 0 0 106917 105 0 0 25 0 1 0 358045733 151646208 35458 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35458 603 41 0 36982 0
vsize: 148092
[startup+1080.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35799 0 0 0 107917 105 0 0 25 0 1 0 358045733 151646208 35458 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35458 603 41 0 36982 0
vsize: 148092
[startup+1090.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35799 0 0 0 108917 105 0 0 25 0 1 0 358045733 151646208 35458 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35458 603 41 0 36982 0
vsize: 148092
[startup+1100.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35799 0 0 0 109917 105 0 0 25 0 1 0 358045733 151646208 35458 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35458 603 41 0 36982 0
vsize: 148092
[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35799 0 0 0 110917 105 0 0 25 0 1 0 358045733 151646208 35458 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35458 603 41 0 36982 0
vsize: 148092
[startup+1120.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35800 0 0 0 111917 105 0 0 25 0 1 0 358045733 151646208 35459 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35459 603 41 0 36982 0
vsize: 148092
[startup+1130.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35800 0 0 0 112917 106 0 0 25 0 1 0 358045733 151646208 35459 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35459 603 41 0 36982 0
vsize: 148092
[startup+1140.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35800 0 0 0 113917 106 0 0 25 0 1 0 358045733 151646208 35459 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35459 603 41 0 36982 0
vsize: 148092
[startup+1150.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35800 0 0 0 114917 106 0 0 25 0 1 0 358045733 151646208 35459 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35459 603 41 0 36982 0
vsize: 148092
[startup+1160.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35800 0 0 0 115917 106 0 0 25 0 1 0 358045733 151646208 35459 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35459 603 41 0 36982 0
vsize: 148092
[startup+1170.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35800 0 0 0 116917 106 0 0 25 0 1 0 358045733 151646208 35459 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35459 603 41 0 36982 0
vsize: 148092
[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35800 0 0 0 117917 106 0 0 25 0 1 0 358045733 151646208 35459 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35459 603 41 0 36982 0
vsize: 148092
[startup+1190.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35800 0 0 0 118917 106 0 0 25 0 1 0 358045733 151646208 35459 4294967295 134512640 134672761 3221224560 3221223728 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35459 603 41 0 36982 0
vsize: 148092
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 3454
Raw data (stat): 3395 (minisat+) R 3394 30927 30926 0 -1 0 35800 0 0 0 119917 107 0 0 25 0 1 0 358045733 151646208 35459 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37023 35459 603 41 0 36982 0
vsize: 148092
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 3454
Raw data (stat): 3395 (minisat+) Z 3394 30927 30926 0 -1 12 35803 0 0 0 119917 113 0 0 25 0 1 0 358045733 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.19
CPU time (s): 1200.31
CPU user time (s): 1199.18
CPU system time (s): 1.13683
CPU usage (%): 100.01
Max. virtual memory (Kb): 148092
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####