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/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran10x10b.opb
MD5SUM	c76102ddcf7f5ab3b2677033d320eaa3
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	756736
Optimality of the best value was proved	NO
Number of terms in the objective function	2100
Biggest coefficient in the objective function	4718592
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	502612132
Number of bits of the sum of numbers in the objective function	29
Biggest number in a constraint	4718592
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	502612132
Number of bits of the biggest sum of numbers	29
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	422.405
Number of variables	2100
Total number of constraints	120
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	120
Minimum length of a constraint	21
Maximum length of a constraint	200
Trace number 17692

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-21 11:23:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19214 boxname=wulflinc26 idbench=1478 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c76102ddcf7f5ab3b2677033d320eaa3  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-ran10x10b.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-ran10x10b.opb /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-ran10x10b.opb
IDLAUNCH: 19214
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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.061
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:        554024 kB
Buffers:         25876 kB
Cached:         424488 kB
SwapCached:         68 kB
Active:          55232 kB
Inactive:       398024 kB
HighTotal:      131008 kB
HighFree:         7532 kB
LowTotal:       903652 kB
LowFree:        546492 kB
SwapTotal:     2097892 kB
SwapFree:      2097800 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6876 kB
Slab:            21784 kB
Committed_AS:    63728 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:43:06 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 19214 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 138]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2
c ---[ 132]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 1985     Base: 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 1985     Base: 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 1780     Base: 2 2 2 2 2 2 2
c ---[ 122]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Adder-cost: 180   maxlim: 8950   bits: 14/14
c ---[ 112]---> Sorter-cost: 2083     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost: 2083     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 2083     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 1442     Base: 2 2 2 2 2 2 2
c ---[ 100]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:   15
c ---[  97]---> BDD-cost:   11
c ---[  96]---> BDD-cost:   13
c ---[  95]---> BDD-cost:   12
c ---[  94]---> BDD-cost:   13
c ---[  93]---> BDD-cost:   13
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   13
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:    9
c ---[  88]---> BDD-cost:   13
c ---[  87]---> BDD-cost:   12
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   11
c ---[  83]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   11
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   11
c ---[  78]---> BDD-cost:    9
c ---[  77]---> BDD-cost:   11
c ---[  76]---> BDD-cost:   13
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   12
c ---[  72]---> BDD-cost:   17
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   17
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:    9
c ---[  66]---> BDD-cost:   15
c ---[  65]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   11
c ---[  63]---> BDD-cost:   13
c ---[  62]---> BDD-cost:   13
c ---[  61]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:   13
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:    9
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   13
c ---[  51]---> BDD-cost:   12
c ---[  50]---> BDD-cost:   13
c ---[  49]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   11
c ---[  47]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   15
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:   15
c ---[  43]---> BDD-cost:   13
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   12
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   15
c ---[  37]---> BDD-cost:   11
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   15
c ---[  34]---> BDD-cost:    9
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   11
c ---[  30]---> BDD-cost:   11
c ---[  29]---> BDD-cost:   11
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:   11
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:    9
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:    9
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:   11
c ---[  18]---> BDD-cost:   11
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   11
c ---[  13]---> BDD-cost:   11
c ---[  12]---> BDD-cost:    9
c ---[  11]---> BDD-cost:   11
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   15
c ---[   7]---> BDD-cost:   12
c ---[   6]---> BDD-cost:   16
c ---[   5]---> BDD-cost:   17
c ---[   4]---> BDD-cost:   11
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   94999   226264 |   31666       0        0     nan |  0.000 % |
c |       101 |   94999   226264 |   34832     101      826     8.2 |  7.009 % |
c |       251 |   94960   226178 |   38315     247     1540     6.2 |  7.041 % |
c |       476 |   94960   226178 |   42147     472     2925     6.2 |  7.041 % |
c |       813 |   94801   225813 |   46362     802     4716     5.9 |  7.171 % |
c |      1319 |   94801   225813 |   50998    1308     7985     6.1 |  7.171 % |
c ==============================================================================
c [1mFound solution: 2814354[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 3932   maxlim: 1294866   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2058 |  122271   323945 |   40757    2047    13218     6.5 |  7.171 % |
c |      2158 |  122271   323945 |   44832    2147    13895     6.5 |  6.448 % |
c |      2308 |  122260   323919 |   49315    2296    14616     6.4 |  6.456 % |
c |      2533 |  122243   323881 |   54247    2519    15906     6.3 |  6.470 % |
c |      2870 |  122243   323881 |   59672    2856    17814     6.2 |  6.470 % |
c |      3377 |  122243   323881 |   65639    3363    21014     6.2 |  6.470 % |
c |      4137 |  122243   323881 |   72203    4123    55983    13.6 |  6.470 % |
c |      5278 |  122231   323855 |   79423    5262    64590    12.3 |  6.480 % |
c |      6986 |  122061   323456 |   87366    6955    77557    11.2 |  6.602 % |
c |      9548 |  121979   323221 |   96102    9514   132118    13.9 |  6.660 % |
c |     13393 |  121851   322906 |  105713   13338   163424    12.3 |  6.749 % |
c ==============================================================================
c [1mFound solution: 2813493[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1295727   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17658 |  121794   322843 |   40598   17599   508439    28.9 |  6.749 % |
c |     17758 |  121794   322843 |   44657   17699   508971    28.8 |  6.807 % |
c |     17908 |  121546   322269 |   49123   17830   509900    28.6 |  6.986 % |
c |     18133 |  121462   322073 |   54035   18046   511766    28.4 |  7.044 % |
c |     18470 |  121462   322073 |   59439   18383   514731    28.0 |  7.044 % |
c |     18977 |  121462   322073 |   65383   18890   518852    27.5 |  7.044 % |
c |     19736 |  121462   322073 |   71921   19649   541726    27.6 |  7.044 % |
c |     20875 |  121462   322073 |   79114   20788   684809    32.9 |  7.044 % |
c |     22583 |  121462   322073 |   87025   22496   755976    33.6 |  7.044 % |
c |     25145 |  121393   321920 |   95727   25052   799475    31.9 |  7.097 % |
c |     28989 |  121384   321889 |  105300   28894  1030291    35.7 |  7.099 % |
c ==============================================================================
c [1mFound solution: 2150706[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1958514   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29741 |  121256   321716 |   40418   29628  1057696    35.7 |  7.099 % |
c |     29841 |  121256   321716 |   44459   29728  1058679    35.6 |  7.246 % |
c |     29991 |  121256   321716 |   48905   29878  1059514    35.5 |  7.246 % |
c |     30216 |  121256   321716 |   53796   30103  1060852    35.2 |  7.246 % |
c |     30553 |  121256   321716 |   59175   30440  1068423    35.1 |  7.246 % |
c |     31060 |  121256   321716 |   65093   30947  1089797    35.2 |  7.246 % |
c |     31819 |  121256   321716 |   71602   31706  1122570    35.4 |  7.246 % |
c ==============================================================================
c [1mFound solution: 1605212[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2504008   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32085 |  121242   321499 |   40414   29638   962685    32.5 |  7.246 % |
c |     32185 |  121242   321499 |   44455   29738   963273    32.4 |  7.273 % |
c |     32335 |  121242   321499 |   48900   29888   964716    32.3 |  7.273 % |
c |     32561 |  121242   321499 |   53791   30114   966867    32.1 |  7.273 % |
c |     32898 |  120917   320757 |   59170   30415   974287    32.0 |  7.513 % |
c |     33404 |  120589   320007 |   65087   30886   991445    32.1 |  7.777 % |
c |     34165 |  120532   319877 |   71595   31639  1014690    32.1 |  7.827 % |
c |     35304 |  120532   319877 |   78755   32778  1085513    33.1 |  7.827 % |
c |     37012 |  120482   319763 |   86630   34485  1195750    34.7 |  7.861 % |
c |     39574 |  120482   319763 |   95294   37047  1273198    34.4 |  7.861 % |
c |     43419 |  120482   319763 |  104823   40892  1558393    38.1 |  7.861 % |
c |     49186 |  120474   319743 |  115305   46657  1885811    40.4 |  7.867 % |
c |     57835 |  120172   319042 |  126836   55283  3160888    57.2 |  8.115 % |
c |     70809 |  120067   318805 |  139520   68250  4024527    59.0 |  8.194 % |
c |     90270 |  119815   318218 |  153472   87631  5307749    60.6 |  8.397 % |
c |    119463 |  119413   317294 |  168819  116797  7716849    66.1 |  8.732 % |
c |    163256 |  119409   317284 |  185701  160589 11586544    72.2 |  8.734 % |
c ==============================================================================
c [1mFound solution: 1378231[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2730989   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    214293 |  119332   317247 |   39777   36575  1530673    41.9 |  8.734 % |
c |    214393 |  119310   317195 |   43754   36674  1531645    41.8 |  8.855 % |
c |    214543 |  119244   317045 |   48130   36820  1535645    41.7 |  8.905 % |
c |    214768 |  119244   317045 |   52943   37045  1542009    41.6 |  8.905 % |
c |    215106 |  119244   317045 |   58237   37383  1547964    41.4 |  8.905 % |
c |    215612 |  119220   316963 |   64061   37880  1564662    41.3 |  8.913 % |
c |    216371 |  119220   316963 |   70467   38639  1594375    41.3 |  8.913 % |
c |    217510 |  119213   316948 |   77514   39777  1655573    41.6 |  8.918 % |
c |    219220 |  119209   316939 |   85265   41486  1760284    42.4 |  8.921 % |
c |    221784 |  119195   316907 |   93792   44048  1889681    42.9 |  8.932 % |
c |    225629 |  119012   316485 |  103171   47864  2114585    44.2 |  9.071 % |
c |    231398 |  118948   316341 |  113488   53624  2530962    47.2 |  9.124 % |
c |    240049 |  118835   316081 |  124837   62264  3138840    50.4 |  9.214 % |
c |    253023 |  118361   314990 |  137320   75187  4001649    53.2 |  9.588 % |
c |    272484 |  118293   314820 |  151053   94636  6300357    66.6 |  9.635 % |
c |    301676 |  118164   314520 |  166158  123814  8870137    71.6 |  9.738 % |
c ==============================================================================
c [1mFound solution: 1212007[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2897213   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    302238 |  118191   314693 |   39397  124374  8911587    71.7 |  9.738 % |
c |    302338 |  118010   314276 |   43336   21872  1407487    64.4 |  9.932 % |
c |    302491 |  118010   314276 |   47670   22025  1408594    64.0 |  9.932 % |
c |    302716 |  118010   314276 |   52437   22250  1416182    63.6 |  9.932 % |
c |    303053 |  118010   314276 |   57681   22587  1430862    63.3 |  9.932 % |
c |    303559 |  118010   314276 |   63449   23093  1442377    62.5 |  9.932 % |
c |    304321 |  118005   314265 |   69794   23854  1467413    61.5 |  9.937 % |
c |    305460 |  117985   314218 |   76773   24991  1553972    62.2 |  9.953 % |
c |    307169 |  117812   313826 |   84450   26690  1591040    59.6 | 10.082 % |
c |    309732 |  117788   313773 |   92896   29250  1728207    59.1 | 10.101 % |
c |    313576 |  117772   313736 |  102185   33089  2115348    63.9 | 10.116 % |
c |    319342 |  117736   313653 |  112404   38849  2420718    62.3 | 10.143 % |
c |    327991 |  117736   313653 |  123644   47498  3236242    68.1 | 10.143 % |
c |    340965 |  117732   313643 |  136009   60471  4215274    69.7 | 10.145 % |
c |    360426 |  117675   313510 |  149610   79929  7926657    99.2 | 10.196 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 X2_bit_6 X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 X4_bit_7 -X4_bit_6 -X4_bit_5 X4_bit_4 X4_bit_3 -X4_bit_2 X4_bit_1 X4_bit0 X4_bit1 X4_bit2 X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 X11_bit_3 X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 -X12_bit_6 -X12_bit_5 -X12_bit_4 -X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 X13_bit_6 X13_bit_5 -X13_bit_4 X13_bit_3 -X13_bit_2 -X13_bit_1 X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X15_bit_7 -X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 -X15_bit_2 -X15_bit_1 -X15_bit0 -X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 -X17_bit_6 -X17_bit_5 -X17_bit_4 -X17_bit_3 -X17_bit_2 -X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X19_bit_7 X19_bit_6 -X19_bit_5 X19_bit_4 X19_bit_3 X19_bit_2 -X19_bit_1 X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 -X20_bit_7 -X20_bit_6 -X20_bit_5 -X20_bit_4 -X20_bit_3 -X20_bit_2 -X20_bit_1 -X20_bit0 -X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X21_bit_7 -X21_bit_6 -X21_bit_5 -X21_bit_4 -X21_bit_3 -X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X23_bit_7 -X23_bit_6 -X23_bit_5 -X23_bit_4 -X23_bit_3 -X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X24_bit_7 -X24_bit_6 -X24_bit_5 -X24_bit_4 -X24_bit_3 -X24_bit_2 -X24_bit_1 -X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 X25_bit_7 -X25_bit_6 X25_bit_5 X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 X26_bit_7 X26_bit_6 -X26_bit_5 -X26_bit_4 X26_bit_3 X26_bit_2 X26_bit_1 X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X27_bit_7 -X27_bit_6 -X27_bit_5 -X27_bit_4 -X27_bit_3 -X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 -X29_bit_7 -X29_bit_6 -X29_bit_5 -X29_bit_4 -X29_bit_3 -X29_bit_2 -X29_bit_1 -X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 -X32_bit_6 -X32_bit_5 -X32_bit_4 -X32_bit_3 -X32_bit_2 -X32_bit_1 -X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X33_bit_7 X33_bit_6 X33_bit_5 X33_bit_4 -X33_bit_3 -X33_bit_2 X33_bit_1 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X34_bit_7 -X34_bit_6 -X34_bit_5 -X34_bit_4 -X34_bit_3 -X34_bit_2 -X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 -X35_bit_6 -X35_bit_5 -X35_bit_4 -X35_bit_3 -X35_bit_2 -X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X36_bit_7 -X36_bit_6 -X36_bit_5 -X36_bit_4 X36_bit_3 X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 -X37_bit_7 X37_bit_6 -X37_bit_5 -X37_bit_4 -X37_bit_3 -X37_bit_2 -X37_bit_1 -X37_bit0 -X37_bit1 -X37_bit2 X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X38_bit_7 -X38_bit_6 -X38_bit_5 -X38_bit_4 -X38_bit_3 -X38_bit_2 -X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X39_bit_7 -X39_bit_6 -X39_bit_5 -X39_bit_4 -X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X40_bit_7 -X40_bit_6 -X40_bit_5 -X40_bit_4 -X40_bit_3 -X40_bit_2 -X40_bit_1 -X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 -X41_bit_7 -X41_bit_6 -X41_bit_5 -X41_bit_4 -X41_bit_3 -X41_bit_2 -X41_bit_1 -X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X42_bit_7 -X42_bit_6 -X42_bit_5 -X42_bit_4 -X42_bit_3 -X42_bit_2 -X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X43_bit_7 -X43_bit_6 -X43_bit_5 -X43_bit_4 -X43_bit_3 -X43_bit_2 -X43_bit_1 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X44_bit_7 -X44_bit_6 -X44_bit_5 -X44_bit_4 -X44_bit_3 -X44_bit_2 -X44_bit_1 -X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X45_bit_7 -X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 -X46_bit_6 -X46_bit_5 -X46_bit_4 -X46_bit_3 -X46_bit_2 -X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 -X47_bit_7 -X47_bit_6 -X47_bit_5 -X47_bit_4 -X47_bit_3 -X47_bit_2 -X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 -X48_bit_6 -X48_bit_5 -X48_bit_4 -X48_bit_3 -X48_bit_2 -X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 -X49_bit_6 -X49_bit_5 -X49_bit_4 -X49_bit_3 -X49_bit_2 -X49_bit_1 X49_bit0 -X49_bit1 X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 X50_bit_7 -X50_bit_6 -X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 -X51_bit_7 -X51_bit_6 -X51_bit_5 -X51_bit_4 -X51_bit_3 -X51_bit_2 -X51_bit_1 -X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X52_bit_7 -X52_bit_6 -X52_bit_5 -X52_bit_4 -X52_bit_3 -X52_bit_2 -X52_bit_1 -X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 X53_bit_7 X53_bit_6 X53_bit_5 -X53_bit_4 X53_bit_3 X53_bit_2 X53_bit_1 X53_bit0 X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 -X54_bit_6 -X54_bit_5 -X54_bit_4 -X54_bit_3 -X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 -X55_bit_6 -X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 X56_bit_7 -X56_bit_6 -X56_bit_5 -X56_bit_4 X56_bit_3 X56_bit_2 X56_bit_1 X56_bit0 -X56_bit1 X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 -X57_bit_6 -X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X58_bit_7 -X58_bit_6 -X58_bit_5 -X58_bit_4 -X58_bit_3 -X58_bit_2 -X58_bit_1 -X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 X59_bit_7 X59_bit_6 X59_bit_5 -X59_bit_4 X59_bit_3 -X59_bit_2 X59_bit_1 X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 X60_bit_7 X60_bit_6 X60_bit_5 X60_bit_4 X60_bit_3 X60_bit_2 -X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X61_bit_7 X61_bit_6 X61_bit_5 -X61_bit_4 -X61_bit_3 -X61_bit_2 -X61_bit_1 X61_bit0 X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 -X62_bit_7 -X62_bit_6 -X62_bit_5 -X62_bit_4 -X62_bit_3 -X62_bit_2 -X62_bit_1 -X62_bit0 -X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 X63_bit_7 X63_bit_6 X63_bit_5 X63_bit_4 X63_bit_3 X63_bit_2 X63_bit_1 X63_bit0 -X63_bit1 -X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 -X64_bit_7 -X64_bit_6 -X64_bit_5 -X64_bit_4 -X64_bit_3 -X64_bit_2 -X64_bit_1 -X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 -X65_bit_7 -X65_bit_6 -X65_bit_5 -X65_bit_4 -X65_bit_3 -X65_bit_2 -X65_bit_1 -X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 X66_bit_7 -X66_bit_6 X66_bit_5 X66_bit_4 X66_bit_3 -X66_bit_2 X66_bit_1 -X66_bit0 X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 X67_bit_7 X67_bit_6 X67_bit_5 X67_bit_4 X67_bit_3 -X67_bit_2 X67_bit_1 -X67_bit0 -X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 -X68_bit_7 -X68_bit_6 -X68_bit_5 -X68_bit_4 -X68_bit_3 -X68_bit_2 -X68_bit_1 -X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 -X69_bit_7 -X69_bit_6 -X69_bit_5 -X69_bit_4 -X69_bit_3 -X69_bit_2 -X69_bit_1 -X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 -X70_bit_6 -X70_bit_5 -X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X71_bit_7 -X71_bit_6 -X71_bit_5 -X71_bit_4 -X71_bit_3 -X71_bit_2 -X71_bit_1 -X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 X72_bit_7 -X72_bit_6 X72_bit_5 X72_bit_4 -X72_bit_3 X72_bit_2 -X72_bit_1 X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 -X73_bit_6 -X73_bit_5 -X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 -X74_bit_7 -X74_bit_6 -X74_bit_5 -X74_bit_4 X74_bit_3 X74_bit_2 -X74_bit_1 -X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 X75_bit_7 X75_bit_6 -X75_bit_5 -X75_bit_4 X75_bit_3 X75_bit_2 X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X76_bit_7 -X76_bit_6 -X76_bit_5 -X76_bit_4 -X76_bit_3 -X76_bit_2 -X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 -X77_bit_7 -X77_bit_6 -X77_bit_5 -X77_bit_4 -X77_bit_3 -X77_bit_2 -X77_bit_1 -X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X78_bit_7 -X78_bit_6 -X78_bit_5 -X78_bit_4 -X78_bit_3 -X78_bit_2 -X78_bit_1 -X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X79_bit_7 -X79_bit_6 -X79_bit_5 -X79_bit_4 X79_bit_3 X79_bit_2 -X79_bit_1 -X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X80_bit_7 -X80_bit_6 -X80_bit_5 -X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 X81_bit_7 X81_bit_6 X81_bit_5 X81_bit_4 X81_bit_3 X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 X82_bit_7 X82_bit_6 X82_bit_5 X82_bit_4 X82_bit_3 -X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 X83_bit_7 X83_bit_6 X83_bit_5 X83_bit_4 X83_bit_3 -X83_bit_2 X83_bit_1 -X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 X84_bit_7 X84_bit_6 X84_bit_5 -X84_bit_4 X84_bit_3 X84_bit_2 X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 -X85_bit_7 -X85_bit_6 -X85_bit_5 -X85_bit_4 -X85_bit_3 -X85_bit_2 -X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 X86_bit_7 X86_bit_6 X86_bit_5 X86_bit_4 -X86_bit_3 -X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 X87_bit_7 X87_bit_6 X87_bit_5 X87_bit_4 X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 X88_bit_7 X88_bit_6 X88_bit_5 X88_bit_4 X88_bit_3 -X88_bit_2 X88_bit_1 -X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 X89_bit_7 X89_bit_6 X89_bit_5 X89_bit_4 X89_bit_3 X89_bit_2 -X89_bit_1 -X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X90_bit_7 -X90_bit_6 -X90_bit_5 -X90_bit_4 -X90_bit_3 -X90_bit_2 -X90_bit_1 -X90_bit0 X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 X91_bit_7 X91_bit_6 -X91_bit_5 X91_bit_4 -X91_bit_3 -X91_bit_2 -X91_bit_1 X91_bit0 X91_bit1 X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 -X92_bit_7 X92_bit_6 X92_bit_5 X92_bit_4 -X92_bit_3 X92_bit_2 -X92_bit_1 -X92_bit0 -X92_bit1 X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 X93_bit_7 X93_bit_6 X93_bit_5 -X93_bit_4 -X93_bit_3 -X93_bit_2 X93_bit_1 X93_bit0 -X93_bit1 -X93_bit2 X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 -X94_bit_7 -X94_bit_6 -X94_bit_5 -X94_bit_4 -X94_bit_3 -X94_bit_2 -X94_bit_1 -X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 -X95_bit_7 -X95_bit_6 -X95_bit_5 -X95_bit_4 -X95_bit_3 -X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -X96_bit_7 -X96_bit_6 -X96_bit_5 -X96_bit_4 -X96_bit_3 -X96_bit_2 -X96_bit_1 -X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 -X97_bit_7 -X97_bit_6 -X97_bit_5 -X97_bit_4 -X97_bit_3 -X97_bit_2 -X97_bit_1 -X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 -X98_bit_7 -X98_bit_6 -X98_bit_5 -X98_bit_4 -X98_bit_3 -X98_bit_2 -X98_bit_1 -X98_bit0 -X98_bit1 -X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 -X99_bit_7 -X99_bit_6 -#### 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.92 0.95 0.93 2/54 31016
Raw data (stat): 31016 (runsolver) R 31015 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544693815 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0002 s]
Raw data (loadavg): 0.93 0.96 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 5927 0 0 0 985 12 0 0 25 0 1 0 544693815 25808896 5252 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6301 5253 603 41 0 6260 0
vsize: 25204
[startup+19.9999 s]
Raw data (loadavg): 0.94 0.96 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 6491 0 0 0 1983 14 0 0 25 0 1 0 544693815 28176384 5796 4294967295 134512640 134672761 3221224544 3221223876 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6879 5796 603 41 0 6838 0
vsize: 27516
[startup+30.0003 s]
Raw data (loadavg): 0.95 0.96 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 6735 0 0 0 2982 15 0 0 25 0 1 0 544693815 29114368 6040 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7108 6040 603 41 0 7067 0
vsize: 28432
[startup+40.0003 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 7171 0 0 0 3981 16 0 0 25 0 1 0 544693815 30765056 6455 4294967295 134512640 134672761 3221224544 3221223728 134593685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7511 6455 603 41 0 7470 0
vsize: 30044
[startup+49.9999 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 7289 0 0 0 4981 17 0 0 25 0 1 0 544693815 31141888 6552 4294967295 134512640 134672761 3221224544 3221223616 1074718162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7603 6552 603 41 0 7562 0
vsize: 30412
[startup+59.9994 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 7385 0 0 0 5980 17 0 0 25 0 1 0 544693815 31674368 6648 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7733 6648 603 41 0 7692 0
vsize: 30932
[startup+69.9995 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 7805 0 0 0 6980 18 0 0 25 0 1 0 544693815 33288192 7068 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8127 7068 603 41 0 8086 0
vsize: 32508
[startup+80 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 8195 0 0 0 7978 19 0 0 25 0 1 0 544693815 34918400 7458 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8525 7458 603 41 0 8484 0
vsize: 34100
[startup+89.9994 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 8688 0 0 0 8978 21 0 0 25 0 1 0 544693815 36941824 7951 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9019 7951 603 41 0 8978 0
vsize: 36076
[startup+99.9993 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 8959 0 0 0 9977 21 0 0 25 0 1 0 544693815 38014976 8222 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9281 8222 603 41 0 9240 0
vsize: 37124
[startup+110 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 9564 0 0 0 10976 23 0 0 25 0 1 0 544693815 40427520 8827 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9870 8827 603 41 0 9829 0
vsize: 39480
[startup+120 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 9950 0 0 0 11975 24 0 0 25 0 1 0 544693815 42045440 9213 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10265 9213 603 41 0 10224 0
vsize: 41060
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 10458 0 0 0 12973 26 0 0 25 0 1 0 544693815 44331008 9721 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10823 9721 603 41 0 10782 0
vsize: 43292
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 10698 0 0 0 13973 26 0 0 25 0 1 0 544693815 45404160 9961 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11085 9961 603 41 0 11044 0
vsize: 44340
[startup+150 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 11069 0 0 0 14972 28 0 0 25 0 1 0 544693815 46891008 10332 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11448 10332 603 41 0 11407 0
vsize: 45792
[startup+160 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 11369 0 0 0 15971 28 0 0 25 0 1 0 544693815 48095232 10632 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11742 10632 603 41 0 11701 0
vsize: 46968
[startup+170 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 11679 0 0 0 16970 29 0 0 25 0 1 0 544693815 49307648 10942 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12038 10942 603 41 0 11997 0
vsize: 48152
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 12038 0 0 0 17970 30 0 0 25 0 1 0 544693815 50778112 11301 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12397 11301 603 41 0 12356 0
vsize: 49588
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 12539 0 0 0 18969 31 0 0 25 0 1 0 544693815 52785152 11802 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12887 11802 603 41 0 12846 0
vsize: 51548
[startup+200 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 12994 0 0 0 19967 33 0 0 25 0 1 0 544693815 54673408 12257 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13348 12257 603 41 0 13307 0
vsize: 53392
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 13589 0 0 0 20966 34 0 0 25 0 1 0 544693815 57098240 12852 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13940 12852 603 41 0 13899 0
vsize: 55760
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 13812 0 0 0 21966 35 0 0 25 0 1 0 544693815 58040320 13075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14170 13075 603 41 0 14129 0
vsize: 56680
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 14049 0 0 0 22965 36 0 0 25 0 1 0 544693815 58978304 13312 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14399 13312 603 41 0 14358 0
vsize: 57596
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 14235 0 0 0 23964 37 0 0 25 0 1 0 544693815 59654144 13498 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14564 13498 603 41 0 14523 0
vsize: 58256
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 14422 0 0 0 24964 37 0 0 25 0 1 0 544693815 60461056 13685 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14761 13685 603 41 0 14720 0
vsize: 59044
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 14649 0 0 0 25963 38 0 0 25 0 1 0 544693815 61431808 13912 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14998 13912 603 41 0 14957 0
vsize: 59992
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 14860 0 0 0 26963 39 0 0 25 0 1 0 544693815 62238720 14123 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15195 14123 603 41 0 15154 0
vsize: 60780
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 15088 0 0 0 27962 39 0 0 25 0 1 0 544693815 63184896 14351 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15426 14351 603 41 0 15385 0
vsize: 61704
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 15300 0 0 0 28961 40 0 0 25 0 1 0 544693815 63991808 14563 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15623 14563 603 41 0 15582 0
vsize: 62492
[startup+300.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 15565 0 0 0 29961 41 0 0 25 0 1 0 544693815 65064960 14828 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15885 14828 603 41 0 15844 0
vsize: 63540
[startup+310.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 15880 0 0 0 30960 42 0 0 25 0 1 0 544693815 66412544 15143 4294967295 134512640 134672761 3221224544 3221223712 134561256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16214 15143 603 41 0 16173 0
vsize: 64856
[startup+320.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 16217 0 0 0 31959 43 0 0 25 0 1 0 544693815 68280320 15480 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16670 15480 603 41 0 16629 0
vsize: 66680
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 16503 0 0 0 32958 44 0 0 25 0 1 0 544693815 69480448 15766 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16963 15766 603 41 0 16922 0
vsize: 67852
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 16708 0 0 0 33958 45 0 0 25 0 1 0 544693815 70283264 15971 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17159 15971 603 41 0 17118 0
vsize: 68636
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 16930 0 0 0 34957 45 0 0 25 0 1 0 544693815 71229440 16193 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17390 16193 603 41 0 17349 0
vsize: 69560
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 17148 0 0 0 35957 46 0 0 25 0 1 0 544693815 72036352 16411 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17587 16411 603 41 0 17546 0
vsize: 70348
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 17372 0 0 0 36956 47 0 0 25 0 1 0 544693815 72998912 16635 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17822 16635 603 41 0 17781 0
vsize: 71288
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 17554 0 0 0 37956 47 0 0 25 0 1 0 544693815 73674752 16817 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 16817 603 41 0 17946 0
vsize: 71948
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 17727 0 0 0 38955 48 0 0 25 0 1 0 544693815 74477568 16990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18183 16990 603 41 0 18142 0
vsize: 72732
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 17910 0 0 0 39955 49 0 0 25 0 1 0 544693815 75153408 17173 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18348 17173 603 41 0 18307 0
vsize: 73392
[startup+410.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 18101 0 0 0 40954 50 0 0 25 0 1 0 544693815 75964416 17364 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18546 17364 603 41 0 18505 0
vsize: 74184
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 18284 0 0 0 41954 50 0 0 25 0 1 0 544693815 76775424 17547 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18744 17547 603 41 0 18703 0
vsize: 74976
[startup+430.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 18506 0 0 0 42954 50 0 0 25 0 1 0 544693815 77631488 17769 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18953 17769 603 41 0 18912 0
vsize: 75812
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 18698 0 0 0 43954 51 0 0 25 0 1 0 544693815 78454784 17961 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19154 17961 603 41 0 19113 0
vsize: 76616
[startup+450.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 18845 0 0 0 44953 52 0 0 25 0 1 0 544693815 78995456 18108 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19286 18108 603 41 0 19245 0
vsize: 77144
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 19043 0 0 0 45952 52 0 0 25 0 1 0 544693815 79802368 18306 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19483 18306 603 41 0 19442 0
vsize: 77932
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 19153 0 0 0 46952 53 0 0 25 0 1 0 544693815 80207872 18416 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19582 18416 603 41 0 19541 0
vsize: 78328
[startup+480.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 19308 0 0 0 47952 53 0 0 25 0 1 0 544693815 80883712 18571 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19747 18571 603 41 0 19706 0
vsize: 78988
[startup+490.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 19495 0 0 0 48951 54 0 0 25 0 1 0 544693815 81711104 18758 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19949 18758 603 41 0 19908 0
vsize: 79796
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 19670 0 0 0 49951 54 0 0 25 0 1 0 544693815 82378752 18933 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20112 18933 603 41 0 20071 0
vsize: 80448
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 19849 0 0 0 50951 55 0 0 25 0 1 0 544693815 83185664 19112 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20309 19112 603 41 0 20268 0
vsize: 81236
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 20022 0 0 0 51950 55 0 0 25 0 1 0 544693815 83873792 19285 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20477 19285 603 41 0 20436 0
vsize: 81908
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 20200 0 0 0 52950 56 0 0 25 0 1 0 544693815 84549632 19463 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20642 19463 603 41 0 20601 0
vsize: 82568
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 20353 0 0 0 53949 57 0 0 25 0 1 0 544693815 85225472 19616 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 19616 603 41 0 20766 0
vsize: 83228
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 20508 0 0 0 54948 58 0 0 25 0 1 0 544693815 85766144 19771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20939 19771 603 41 0 20898 0
vsize: 83756
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 20658 0 0 0 55948 58 0 0 25 0 1 0 544693815 86441984 19921 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21104 19921 603 41 0 21063 0
vsize: 84416
[startup+570.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 20817 0 0 0 56948 59 0 0 25 0 1 0 544693815 87130112 20080 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21272 20080 603 41 0 21231 0
vsize: 85088
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 20989 0 0 0 57948 59 0 0 25 0 1 0 544693815 87801856 20252 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21436 20252 603 41 0 21395 0
vsize: 85744
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21110 0 0 0 58947 60 0 0 25 0 1 0 544693815 88334336 20373 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21566 20373 603 41 0 21525 0
vsize: 86264
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21230 0 0 0 59947 60 0 0 25 0 1 0 544693815 88752128 20493 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21668 20493 603 41 0 21627 0
vsize: 86672
[startup+610.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21348 0 0 0 60947 60 0 0 25 0 1 0 544693815 89288704 20611 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21799 20611 603 41 0 21758 0
vsize: 87196
[startup+620.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21466 0 0 0 61947 60 0 0 25 0 1 0 544693815 89694208 20729 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21898 20729 603 41 0 21857 0
vsize: 87592
[startup+630.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21577 0 0 0 62947 61 0 0 25 0 1 0 544693815 90226688 20840 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22028 20840 603 41 0 21987 0
vsize: 88112
[startup+640.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21699 0 0 0 63947 61 0 0 25 0 1 0 544693815 90632192 20962 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22127 20962 603 41 0 22086 0
vsize: 88508
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 64947 61 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223648 134554665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+660.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 65947 61 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+670.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 66947 61 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+680.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 67947 61 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+690.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 68947 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+700.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 69947 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+710.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 70947 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+720.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 71947 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223728 134558423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 72948 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+740.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 73948 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+750.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 74948 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+760.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 75948 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+770.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 76948 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+780.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 77948 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223648 134560477 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+790.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 78949 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+800.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 79949 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+810.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 80949 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+820.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 81949 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+830.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 82949 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+840.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 83949 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223648 134559927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+850.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 84950 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+860.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 85950 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+870.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 86950 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+880.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 87950 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+890.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 88950 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223712 134564686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+900.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21774 0 0 0 89951 62 0 0 25 0 1 0 544693815 91033600 21037 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21037 603 41 0 22184 0
vsize: 88900
[startup+910.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21775 0 0 0 90951 62 0 0 25 0 1 0 544693815 91033600 21038 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21038 603 41 0 22184 0
vsize: 88900
[startup+920.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21775 0 0 0 91951 62 0 0 25 0 1 0 544693815 91033600 21038 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21038 603 41 0 22184 0
vsize: 88900
[startup+930.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21775 0 0 0 92951 62 0 0 25 0 1 0 544693815 91033600 21038 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21038 603 41 0 22184 0
vsize: 88900
[startup+940.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21775 0 0 0 93951 62 0 0 25 0 1 0 544693815 91033600 21038 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21038 603 41 0 22184 0
vsize: 88900
[startup+950.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21775 0 0 0 94951 62 0 0 25 0 1 0 544693815 91033600 21038 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21038 603 41 0 22184 0
vsize: 88900
[startup+960.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21775 0 0 0 95952 62 0 0 25 0 1 0 544693815 91033600 21038 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21038 603 41 0 22184 0
vsize: 88900
[startup+970.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21775 0 0 0 96952 62 0 0 25 0 1 0 544693815 91033600 21038 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21038 603 41 0 22184 0
vsize: 88900
[startup+980.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21775 0 0 0 97952 62 0 0 25 0 1 0 544693815 91033600 21038 4294967295 134512640 134672761 3221224544 3221223648 134559838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21038 603 41 0 22184 0
vsize: 88900
[startup+990.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21775 0 0 0 98952 62 0 0 25 0 1 0 544693815 91033600 21038 4294967295 134512640 134672761 3221224544 3221223648 134560355 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22225 21038 603 41 0 22184 0
vsize: 88900
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 99952 63 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 100951 63 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 101952 63 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 102952 63 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 103952 63 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 104952 63 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 105952 63 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 106952 63 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 107953 63 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 108953 63 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 109953 63 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 110953 63 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 111953 63 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 112954 63 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 113953 63 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 114953 64 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 115953 64 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223728 134559572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 116953 64 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 117954 64 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 118954 64 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31016
Raw data (stat): 31016 (minisat+) R 31015 22612 22611 0 -1 0 21776 0 0 0 119954 64 0 0 25 0 1 0 544693815 91000832 21039 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22217 21039 603 41 0 22176 0
vsize: 88868
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.93 1/54 31016
Raw data (stat): 31016 (minisat+) Z 31015 22612 22611 0 -1 12 21779 0 0 0 119954 68 0 0 25 0 1 0 544693815 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.06
CPU time (s): 1200.23
CPU user time (s): 1199.55
CPU system time (s): 0.684895
CPU usage (%): 100.014
Max. virtual memory (Kb): 88900
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####