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-ran13x13.opb
MD5SUM	688d61d0de54e028c8c4910e094a132c
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	893343
Optimality of the best value was proved	NO
Number of terms in the objective function	3549
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	949933178
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	5242880
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	949933178
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
Number of variables	3549
Total number of constraints	195
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	195
Minimum length of a constraint	21
Maximum length of a constraint	260
Trace number 17650

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-21 11:07:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19284 boxname=wulflinc2 idbench=1484 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  688d61d0de54e028c8c4910e094a132c  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-ran13x13.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-ran13x13.opb
IDLAUNCH: 19284
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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:        705980 kB
Buffers:         14096 kB
Cached:         292692 kB
SwapCached:        504 kB
Active:          46472 kB
Inactive:       262528 kB
HighTotal:      131008 kB
HighFree:        16856 kB
LowTotal:       903652 kB
LowFree:        689124 kB
SwapTotal:     2097136 kB
SwapFree:      2095900 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5712 kB
Slab:            13800 kB
Committed_AS:    71748 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:27:30 (client local time) WITH STATUS 10 IN 1200.3 SECONDS
stats: 19284 7 1200.3 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 221 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 219]---> Adder-cost: 250   maxlim: 16883   bits: 15/15
c ---[ 217]---> Adder-cost: 258   maxlim: 26227   bits: 15/15
c ---[ 215]---> Adder-cost: 258   maxlim: 26867   bits: 15/15
c ---[ 213]---> Adder-cost: 250   maxlim: 17139   bits: 15/15
c ---[ 211]---> Adder-cost: 258   maxlim: 26355   bits: 15/15
c ---[ 209]---> Adder-cost: 250   maxlim: 17267   bits: 15/15
c ---[ 207]---> Adder-cost: 258   maxlim: 25331   bits: 15/15
c ---[ 205]---> Adder-cost: 250   maxlim: 17011   bits: 15/15
c ---[ 203]---> Adder-cost: 234   maxlim: 10611   bits: 14/14
c ---[ 201]---> Adder-cost: 258   maxlim: 26227   bits: 15/15
c ---[ 199]---> Adder-cost: 234   maxlim: 10611   bits: 14/14
c ---[ 197]---> Adder-cost: 258   maxlim: 26611   bits: 15/15
c ---[ 195]---> Adder-cost: 250   maxlim: 17139   bits: 15/15
c ---[ 193]---> Adder-cost: 272   maxlim: 34291   bits: 16/16
c ---[ 191]---> Adder-cost: 272   maxlim: 33267   bits: 16/16
c ---[ 189]---> Adder-cost: 216   maxlim: 6387   bits: 13/13
c ---[ 187]---> Adder-cost: 258   maxlim: 23411   bits: 15/15
c ---[ 185]---> Adder-cost: 240   maxlim: 12659   bits: 14/14
c ---[ 183]---> Adder-cost: 258   maxlim: 22899   bits: 15/15
c ---[ 181]---> Adder-cost: 240   maxlim: 12531   bits: 14/14
c ---[ 179]---> Adder-cost: 216   maxlim: 6259   bits: 13/13
c ---[ 177]---> Adder-cost: 272   maxlim: 31347   bits: 16/15
c ---[ 175]---> Adder-cost: 240   maxlim: 12787   bits: 14/14
c ---[ 173]---> Sorter-cost: 2075     Base: 2 2 2 2 2 2 2
c ---[ 171]---> Adder-cost: 272   maxlim: 32499   bits: 16/15
c ---[ 169]---> Adder-cost: 272   maxlim: 32755   bits: 16/15
c ---[ 168]---> BDD-cost:   14
c ---[ 167]---> BDD-cost:   14
c ---[ 166]---> BDD-cost:   10
c ---[ 165]---> BDD-cost:   13
c ---[ 164]---> BDD-cost:   10
c ---[ 163]---> BDD-cost:   13
c ---[ 162]---> BDD-cost:   13
c ---[ 161]---> BDD-cost:   16
c ---[ 160]---> BDD-cost:   16
c ---[ 159]---> BDD-cost:   15
c ---[ 158]---> BDD-cost:   12
c ---[ 157]---> BDD-cost:   11
c ---[ 156]---> BDD-cost:   16
c ---[ 155]---> BDD-cost:   15
c ---[ 154]---> BDD-cost:   11
c ---[ 153]---> BDD-cost:    9
c ---[ 152]---> BDD-cost:   16
c ---[ 151]---> BDD-cost:   16
c ---[ 150]---> BDD-cost:   10
c ---[ 149]---> BDD-cost:   15
c ---[ 148]---> BDD-cost:   13
c ---[ 147]---> BDD-cost:   13
c ---[ 146]---> BDD-cost:   13
c ---[ 145]---> BDD-cost:   13
c ---[ 144]---> BDD-cost:   13
c ---[ 143]---> BDD-cost:   12
c ---[ 142]---> BDD-cost:   11
c ---[ 141]---> BDD-cost:   13
c ---[ 140]---> BDD-cost:   11
c ---[ 139]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:   13
c ---[ 137]---> BDD-cost:   13
c ---[ 136]---> BDD-cost:   10
c ---[ 135]---> BDD-cost:   15
c ---[ 134]---> BDD-cost:   13
c ---[ 133]---> BDD-cost:   15
c ---[ 132]---> BDD-cost:   13
c ---[ 131]---> BDD-cost:   13
c ---[ 130]---> BDD-cost:   15
c ---[ 129]---> BDD-cost:   12
c ---[ 128]---> BDD-cost:   11
c ---[ 127]---> BDD-cost:   13
c ---[ 126]---> BDD-cost:   11
c ---[ 125]---> BDD-cost:    9
c ---[ 124]---> BDD-cost:   13
c ---[ 123]---> BDD-cost:   13
c ---[ 122]---> BDD-cost:   17
c ---[ 121]---> BDD-cost:   10
c ---[ 120]---> BDD-cost:   15
c ---[ 119]---> BDD-cost:   13
c ---[ 118]---> BDD-cost:   13
c ---[ 117]---> BDD-cost:   13
c ---[ 116]---> BDD-cost:   13
c ---[ 115]---> BDD-cost:   12
c ---[ 114]---> BDD-cost:   11
c ---[ 113]---> BDD-cost:   13
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   15
c ---[ 110]---> BDD-cost:    9
c ---[ 109]---> BDD-cost:   13
c ---[ 108]---> BDD-cost:   13
c ---[ 107]---> BDD-cost:   10
c ---[ 106]---> BDD-cost:   15
c ---[ 105]---> BDD-cost:   13
c ---[ 104]---> BDD-cost:   15
c ---[ 103]---> BDD-cost:   15
c ---[ 102]---> BDD-cost:   15
c ---[ 101]---> BDD-cost:   12
c ---[ 100]---> BDD-cost:   12
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:   15
c ---[  97]---> BDD-cost:   11
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:   15
c ---[  94]---> BDD-cost:   15
c ---[  93]---> BDD-cost:   10
c ---[  92]---> BDD-cost:   15
c ---[  91]---> BDD-cost:   13
c ---[  90]---> BDD-cost:   11
c ---[  89]---> BDD-cost:   17
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   15
c ---[  86]---> BDD-cost:    9
c ---[  85]---> BDD-cost:   17
c ---[  84]---> BDD-cost:   17
c ---[  83]---> BDD-cost:   10
c ---[  82]---> BDD-cost:   15
c ---[  81]---> BDD-cost:   13
c ---[  80]---> BDD-cost:   15
c ---[  79]---> BDD-cost:   15
c ---[  78]---> BDD-cost:   15
c ---[  77]---> BDD-cost:   12
c ---[  76]---> BDD-cost:   12
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   11
c ---[  72]---> BDD-cost:    9
c ---[  71]---> BDD-cost:   15
c ---[  70]---> BDD-cost:   15
c ---[  69]---> BDD-cost:   10
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:   13
c ---[  66]---> BDD-cost:   15
c ---[  65]---> BDD-cost:   11
c ---[  64]---> BDD-cost:   15
c ---[  63]---> BDD-cost:   15
c ---[  62]---> BDD-cost:   12
c ---[  61]---> BDD-cost:   11
c ---[  60]---> BDD-cost:   15
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:    9
c ---[  57]---> BDD-cost:   15
c ---[  56]---> BDD-cost:   15
c ---[  55]---> BDD-cost:   10
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   15
c ---[  52]---> BDD-cost:   13
c ---[  51]---> BDD-cost:   15
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   12
c ---[  47]---> BDD-cost:   11
c ---[  46]---> BDD-cost:   15
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:   11
c ---[  42]---> BDD-cost:   15
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   10
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   13
c ---[  37]---> BDD-cost:   13
c ---[  36]---> BDD-cost:   13
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   12
c ---[  33]---> BDD-cost:   11
c ---[  32]---> BDD-cost:    9
c ---[  31]---> BDD-cost:   13
c ---[  30]---> BDD-cost:   11
c ---[  29]---> BDD-cost:    9
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   13
c ---[  26]---> BDD-cost:   10
c ---[  25]---> BDD-cost:   13
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   15
c ---[  22]---> BDD-cost:   17
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   15
c ---[  19]---> BDD-cost:   12
c ---[  18]---> BDD-cost:   11
c ---[  17]---> BDD-cost:   17
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:    9
c ---[  14]---> BDD-cost:   17
c ---[  13]---> BDD-cost:   17
c ---[  12]---> BDD-cost:   10
c ---[  11]---> BDD-cost:   15
c ---[  10]---> BDD-cost:   14
c ---[   9]---> BDD-cost:   13
c ---[   8]---> BDD-cost:   13
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   13
c ---[   5]---> BDD-cost:   12
c ---[   4]---> BDD-cost:   11
c ---[   3]---> BDD-cost:   13
c ---[   2]---> BDD-cost:   11
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   49961   167448 |   16653       0        0     nan |  0.000 % |
c |       101 |   49827   167107 |   18318      93      434     4.7 | 20.562 % |
c |       252 |   49788   166980 |   20150     238      965     4.1 | 20.617 % |
c |       477 |   49519   166320 |   22165     443     1783     4.0 | 21.187 % |
c |       815 |   49377   165842 |   24381     768     2903     3.8 | 21.390 % |
c |      1321 |   49087   165095 |   26819    1253     4530     3.6 | 22.006 % |
c |      2080 |   48957   164719 |   29501    1995     7982     4.0 | 22.225 % |
c |      3220 |   48957   164719 |   32451    3135    14990     4.8 | 22.225 % |
c |      4929 |   48556   163744 |   35697    4828    30968     6.4 | 23.224 % |
c |      7492 |   48457   163458 |   39266    7380    56954     7.7 | 23.404 % |
c |     11336 |   48242   162798 |   43193   11203   116759    10.4 | 23.794 % |
c |     17103 |   48174   162576 |   47512   16959   372390    22.0 | 23.880 % |
c |     25752 |   48057   162220 |   52264   25595  1058459    41.4 | 24.114 % |
c |     38727 |   47376   160224 |   57490   38486  1289829    33.5 | 25.379 % |
c |     58188 |   47002   159003 |   63239   57887  1746797    30.2 | 25.941 % |
c ==============================================================================
c [1mFound solution: 4024630[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 6663   maxlim: 1668164   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63706 |   93412   324815 |   31137   63382  1833123    28.9 | 25.941 % |
c |     63806 |   93412   324815 |   34250   21313   322945    15.2 | 17.225 % |
c |     63956 |   93412   324815 |   37675   21463   325652    15.2 | 17.225 % |
c |     64181 |   93412   324815 |   41443   21688   327834    15.1 | 17.225 % |
c |     64519 |   93412   324815 |   45587   22026   331360    15.0 | 17.225 % |
c |     65025 |   93405   324798 |   50146   22531   337207    15.0 | 17.236 % |
c |     65784 |   93405   324798 |   55161   23290   345611    14.8 | 17.236 % |
c |     66924 |   93405   324798 |   60677   24430   357901    14.7 | 17.236 % |
c |     68633 |   93278   324443 |   66744   26100   380811    14.6 | 17.384 % |
c |     71195 |   93245   324330 |   73419   28654   412333    14.4 | 17.410 % |
c |     75039 |   93139   323968 |   80761   32473   463203    14.3 | 17.497 % |
c ==============================================================================
c [1mFound solution: 3886697[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1806097   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75559 |   93170   324170 |   31056   32993   470167    14.3 | 17.497 % |
c |     75659 |   93170   324170 |   34161   33093   471064    14.2 | 17.535 % |
c |     75809 |   93170   324170 |   37577   33243   472570    14.2 | 17.535 % |
c |     76034 |   93170   324170 |   41335   33468   474817    14.2 | 17.535 % |
c |     76371 |   93161   324141 |   45469   33804   484509    14.3 | 17.546 % |
c |     76877 |   93152   324110 |   50015   34307   488624    14.2 | 17.551 % |
c |     77636 |   93152   324110 |   55017   35066   500194    14.3 | 17.551 % |
c |     78775 |   93143   324081 |   60519   36204   526126    14.5 | 17.561 % |
c ==============================================================================
c [1mFound solution: 3643228[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2049566   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     80098 |   93168   324292 |   31056   37527   541695    14.4 | 17.561 % |
c |     80198 |   93168   324292 |   34161   18864   174598     9.3 | 17.606 % |
c |     80349 |   93159   324272 |   37577   19014   175573     9.2 | 17.621 % |
c |     80574 |   93159   324272 |   41335   19239   177301     9.2 | 17.621 % |
c |     80911 |   93159   324272 |   45469   19576   181915     9.3 | 17.621 % |
c |     81417 |   93159   324272 |   50015   20082   187299     9.3 | 17.621 % |
c |     82176 |   93159   324272 |   55017   20841   193212     9.3 | 17.621 % |
c |     83315 |   93126   324194 |   60519   21976   201431     9.2 | 17.683 % |
c |     85023 |   93101   324113 |   66571   23681   220770     9.3 | 17.708 % |
c ==============================================================================
c [1mFound solution: 3634438[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2058356   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86716 |   93115   324255 |   31038   25374   239138     9.4 | 17.708 % |
c |     86816 |   93115   324255 |   34141   25474   239884     9.4 | 17.735 % |
c |     86967 |   93115   324255 |   37555   25625   241334     9.4 | 17.735 % |
c |     87192 |   93115   324255 |   41311   25850   243683     9.4 | 17.735 % |
c |     87529 |   93115   324255 |   45442   26187   262950    10.0 | 17.735 % |
c |     88035 |   93115   324255 |   49987   26693   267803    10.0 | 17.735 % |
c ==============================================================================
c [1mFound solution: 3490387[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 2202407   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88371 |   93137   324407 |   31045   27029   271480    10.0 | 17.735 % |
c |     88471 |   93137   324407 |   34149   27129   272716    10.1 | 17.770 % |
c |     88621 |   93130   324384 |   37564   27278   274062    10.0 | 17.775 % |
c |     88846 |   93130   324384 |   41320   27503   276299    10.0 | 17.775 % |
c |     89183 |   93130   324384 |   45452   27840   280352    10.1 | 17.775 % |
c |     89689 |   93130   324384 |   49998   28346   284703    10.0 | 17.775 % |
c |     90448 |   93121   324353 |   54998   29103   292534    10.1 | 17.781 % |
c |     91587 |   93112   324322 |   60497   30236   305192    10.1 | 17.786 % |
c |     93295 |   93112   324322 |   66547   31944   432924    13.6 | 17.786 % |
c |     95857 |   93112   324322 |   73202   34506   484766    14.0 | 17.786 % |
c |     99701 |   93112   324322 |   80522   38350   747982    19.5 | 17.786 % |
c |    105469 |   93078   324219 |   88575   44113  1262340    28.6 | 17.827 % |
c ==============================================================================
c [1mFound solution: 3347499[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2345295   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    107685 |   93080   324297 |   31026   46327  1311358    28.3 | 17.827 % |
c |    107785 |   93080   324297 |   34128   20519   855845    41.7 | 17.868 % |
c |    107936 |   93080   324297 |   37541   20670   856908    41.5 | 17.868 % |
c |    108161 |   93080   324297 |   41295   20895   858293    41.1 | 17.868 % |
c |    108498 |   93080   324297 |   45425   21232   860559    40.5 | 17.868 % |
c |    109005 |   93080   324297 |   49967   21739   864916    39.8 | 17.868 % |
c |    109764 |   93080   324297 |   54964   22498   872415    38.8 | 17.868 % |
c |    110903 |   93080   324297 |   60460   23637   881764    37.3 | 17.868 % |
c |    112611 |   93080   324297 |   66506   25345   894589    35.3 | 17.868 % |
c |    115173 |   93080   324297 |   73157   27907   913145    32.7 | 17.868 % |
c |    119017 |   93071   324266 |   80473   31750   958208    30.2 | 17.873 % |
c |    124786 |   92987   324066 |   88520   37511  1466662    39.1 | 17.996 % |
c |    133435 |   92951   323963 |   97372   46151  1843380    39.9 | 18.042 % |
c ==============================================================================
c [1mFound solution: 3283408[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2409386   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    137890 |   92948   324082 |   30982   50605  2139997    42.3 | 18.042 % |
c |    137990 |   92948   324082 |   34080   21283   666148    31.3 | 18.102 % |
c |    138140 |   92948   324082 |   37488   21433   667480    31.1 | 18.102 % |
c |    138365 |   92948   324082 |   41237   21658   669391    30.9 | 18.102 % |
c |    138702 |   92948   324082 |   45360   21995   671373    30.5 | 18.102 % |
c |    139208 |   92948   324082 |   49896   22501   674557    30.0 | 18.102 % |
c |    139967 |   92948   324082 |   54886   23260   679684    29.2 | 18.102 % |
c |    141106 |   92942   324062 |   60375   24398   688282    28.2 | 18.107 % |
c |    142814 |   92942   324062 |   66412   26106   704913    27.0 | 18.107 % |
c |    145376 |   92942   324062 |   73053   28668   726695    25.3 | 18.107 % |
c |    149221 |   92942   324062 |   80359   32513   766271    23.6 | 18.107 % |
c |    154987 |   92942   324062 |   88395   38279   832015    21.7 | 18.107 % |
c |    163638 |   92942   324062 |   97234   46930  2548251    54.3 | 18.107 % |
c |    176616 |   92920   323988 |  106958   59900  3196261    53.4 | 18.123 % |
c ==============================================================================
c [1mFound solution: 1741875[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3950919   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    190860 |   92932   324088 |   30977   74144  3969570    53.5 | 18.123 % |
c |    190961 |   92932   324088 |   34074   23456   743205    31.7 | 18.153 % |
c |    191111 |   92932   324088 |   37482   23606   744104    31.5 | 18.153 % |
c |    191336 |   92923   324059 |   41230   23830   745741    31.3 | 18.163 % |
c |    191673 |   92923   324059 |   45353   24167   748173    31.0 | 18.163 % |
c |    192179 |   92923   324059 |   49888   24673   753078    30.5 | 18.163 % |
c |    192938 |   92923   324059 |   54877   25432   759316    29.9 | 18.163 % |
c |    194077 |   92899   323997 |   60365   26569   774123    29.1 | 18.204 % |
c |    195785 |   92890   323966 |   66401   28274   797590    28.2 | 18.209 % |
c |    198348 |   92890   323966 |   73042   30837   845219    27.4 | 18.209 % |
c |    202195 |   92890   323966 |   80346   34684   964322    27.8 | 18.209 % |
c |    207961 |   92890   323966 |   88380   40450  1087358    26.9 | 18.209 % |
c |    216613 |   92890   323966 |   97219   49102  1398742    28.5 | 18.209 % |
c |    229587 |   92881   323935 |  106941   62073  1844783    29.7 | 18.214 % |
c |    249049 |   92874   323915 |  117635   81533  2966279    36.4 | 18.219 % |
c |    278243 |   92837   323818 |  129398  110725  5102966    46.1 | 18.280 % |
c |    322034 |   92837   323818 |  142338   30827  5136593   166.6 | 18.280 % |
c |    387718 |   92837   323818 |  156572   96511  8750292    90.7 | 18.280 % |
c |    486245 |   92822   323784 |  172229   45653  8072144   176.8 | 18.301 % |
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 -X99_bit_5 -X99_bit_4 -X99_bit_3 -X99_bit_2 -X99_bit_1 -X99_bit0 -X99_bit1 -X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 -X100_bit_7 -X100_bit_6 -X100_bit_5 -X100_bit_4 -X100_bit_3 -X100_bit_2 -X100_bit_1 -X100_bit0 -X100_bit1 -X100_bit2 -X100_bit3 -X100_bit4 -X100_bit5 -X100_bit6 -X100_bit7 -X100_bit8 -X100_bit9 -X100_bit10 -X100_bit11 -X100_bit12 X101_bit_7 -X101_bit_6 -X101_bit_5 -X101_bit_4 X101_bit_3 -X101_bit_2 X101_bit_1 X101_bit0 -X101_bit1 -X101_bit2 -X101_bit3 -X101_bit4 -X101_bit5 -X101_bit6 -X101_bit7 -X101_bit8 -X101_bit9 -X101_bit10 -X101_bit11 -X101_bit12 -X102_bit_7 -X102_bit_6 -X102_bit_5 -X102_bit_4 -X102_bit_3 -X102_bit_2 -X102_bit_1 -X102_bit0 -X102_bit1 -X102_bit2 -X102_bit3 -X102_bit4 -X102_bit5 -X102_bit6 -X102_bit7 -X102_bit8 -X102_bit9 -X102_bit10 -X102_bit11 -X102_bit12 -X103_bit_7 -X103_bit_6 X103_bit_5 X103_bit_4 -X103_bit_3 X103_bit_2 -X103_bit_1 -X103_bit0 -X103_bit1 -X103_bit2 -X103_bit3 -X103_bit4 -X103_bit5 -X103_bit6 -X103_bit7 -X103_bit8 -X103_bit9 -X103_bit10 -X103_bit11 -X103_bit12 -X104_bit_7 -X104_bit_6 X104_bit_5 X104_bit_4 X104_bit_3 -X104_bit_2 X104_bit_1 -X104_bit0 -X104_bit1 -X104_bit2 -X104_bit3 -X104_bit4 -X104_bit5 -X104_bit6 -X104_bit7 -X104_bit8 -X104_bit9 -X104_bit10 -X104_bit11 -X104_bit12 X105_bit_7 X105_bit_6 X105_bit_5 X105_bit_4 X105_bit_3 -X105_bit_2 -X105_bit_1 -X105_bit0 -X105_bit1 -X105_bit2 X105_bit3 -X105_bit4 -X105_bit5 -X105_bit6 -X105_bit7 -X105_bit8 -X105_bit9 -X105_bit10 -X105_bit11 -X105_bit12 -X106_bit_7 -X106_bit_6 -X106_bit_5 -X106_bit_4 -X106_bit_3 -X106_bit_2 -X106_bit_1 -X106_bit0 -X106_bit1 -X106_bit2 -X106_bit3 -X106_bit4 -X106_bit5 -X106_bit6 -X106_bit7 -X106_bit8 -X106_bit9 -X106_bit10 -X106_bit11 -X106_bit12 -X107_bit_7 -X107_bit_6 -X107_bit_5 -X107_bit_4 -X107_bit_3 -X107_bit_2 -X107_bit_1 -X107_bit0 -X107_bit1 -X107_bit2 -X107_bit3 -X107_bit4 -X107_bit5 -X107_bit6 -X107_bit7 -X107_bit8 -X107_bit9 -X107_bit10 -X107_bit11 -X107_bit12 -X108_bit_7 -X108_bit_6 -X108_bit_5 -X108_bit_4 -X108_bit_3 -X108_bit_2 -X108_bit_1 -X108_bit0 -X108_bit1 -X108_bit2 -X108_bit3 -X108_bit4 -X108_bit5 -X108_bit6 -X108_bit7 -X108_bit8 -X108_bit9 -X108_bit10 -X108_bit11 -X108_bit12 -X109_bit_7 -X109_bit_6 -X109_bit_5 -X109_bit_4 -X109_bit_3 -X109_bit_2 -X109_bit_1 -X109_bit0 -X109_bit1 -X109_bit2 -X109_bit3 -X109_bit4 -X109_bit5 -X109_bit6 -X109_bit7 -X109_bit8 -X109_bit9 -X109_bit10 -X109_bit11 -X109_bit12 X110_bit_7 X110_bit_6 X110_bit_5 X110_bit_4 X110_bit_3 -X110_bit_2 -X110_bit_1 -X110_bit0 -X110_bit1 -X110_bit2 -X110_bit3 -X110_bit4 -X110_bit5 -X110_bit6 -X110_bit7 -X110_bit8 -X110_bit9 -X110_bit10 -X110_bit11 -X110_bit12 -X111_bit_7 -X111_bit_6 -X111_bit_5 -X111_bit_4 -X111_bit_3 -X111_bit_2 -X111_bit_1 -X111_bit0 -X111_bit1 -X111_bit2 -X111_bit3 -X111_bit4 -X111_bit5 -X111_bit6 -X111_bit7 -X111_bit8 -X111_bit9 -X111_bit10 -X111_bit11 -X111_bit12 -X112_bit_7 -X112_bit_6 X112_bit_5 X112_bit_4 X112_bit_3 -X112_bit_2 X112_bit_1 -X112_bit0 -X112_bit1 -X112_bit2 X112_bit3 -X112_bit4 -X112_bit5 -X112_bit6 -X112_bit7 -X112_bit8 -X112_bit9 -X112_bit10 -X112_bit11 -X112_bit12 -X113_bit_7 -X113_bit_6 -X113_bit_5 -X113_bit_4 -X113_bit_3 -X113_bit_2 -X113_bit_1 -X113_bit0 -X113_bit1 -X113_bit2 -X113_bit3 -X113_bit4 -X113_bit5 -X113_bit6 -X113_bit7 -X113_bit8 -X113_bit9 -X113_bit10 -X113_bit11 -X113_bit12 -X114_bit_7 -X114_bit_6 -X114_bit_5 -X114_bit_4 -X114_bit_3 -X114_bit_2 -X114_bit_1 -X114_bit0 -X114_bit1 -X114_bit2 -X114_bit3 -X114_bit4 -X114_bit5 -X114_bit6 -X114_bit7 -X114_bit8 -X114_bit9 -X114_bit10 -X114_bit11 -X114_bit12 -X115_bit_7 X115_bit_6 -X115_bit_5 X115_bit_4 -X115_bit_3 -X115_bit_2 -X115_bit_1 -X115_bit0 -X115_bit1 -X115_bit2 -X115_bit3 -X115_bit4 -X115_bit5 -X115_bit6 -X115_bit7 -X115_bit8 -X115_bit9 -X115_bit10 -X115_bit11 -X115_bit12 -X116_bit_7 -X116_bit_6 -X116_bit_5 -X116_bit_4 -X116_bit_3 -X116_bit_2 -X116_bit_1 -X116_bit0 -X116_bit1 -X116_bit2 -X116_bit3 -X116_bit4 -X116_bit5 -X116_bit6 -X116_bit7 -X116_bit8 -X116_bit9 -X116_bit10 -X116_bit11 -X116_bit12 X117_bit_7 -X117_bit_6 -X117_bit_5 X117_bit_4 X117_bit_3 -X117_bit_2 -X117_bit_1 X117_bit0 -X117_bit1 -X117_bit2 X117_bit3 -X117_bit4 -X117_bit5 -X117_bit6 -X117_bit7 -X117_bit8 -X117_bit9 -X117_bit10 -X117_bit11 -X117_bit12 -X118_bit_7 -X118_bit_6 -X118_bit_5 -X118_bit_4 -X118_bit_3 -X118_bit_2 -X118_bit_1 -X118_bit0 -X118_bit1 -X118_bit2 -X118_bit3 -X118_bit4 -X118_bit5 -X118_bit6 -X118_bit7 -X118_bit8 -X118_bit9 -X118_bit10 -X118_bit11 -X118_bit12 -X119_bit_7 -X119_bit_6 -X119_bit_5 -X119_bit_4 -X119_bit_3 -X119_bit_2 -X119_bit_1 -X119_bit0 -X119_bit1 -X119_bit2 -X119_bit3 -X119_bit4 -X119_bit5 -X119_bit6 -X119_bit7 -X119_bit8 -X119_bit9 -X119_bit10 -X119_bit11 -X119_bit12 X120_bit_7 X120_bit_6 X120_bit_5 X120_bit_4 -X120_bit_3 -X120_bit_2 -X120_bit_1 -X120_bit0 -X120_bit1 -X120_bit2 -X120_bit3 -X120_bit4 -X120_bit5 -X120_bit6 -X120_bit7 -X120_bit8 -X120_bit9 -X120_bit10 -X120_bit11 -X120_bit12 -X121_bit_7 -X121_bit_6 -X121_bit_5 -X121_bit_4 -X121_bit_3 -X121_bit_2 -X121_bit_1 -X121_bit0 -X121_bit1 -X121_bit2 -X121_bit3 -X121_bit4 -X121_bit5 -X121_bit6 -X121_bit7 -X121_bit8 -X121_bit9 -X121_bit10 -X121_bit11 -X121_bit12 -X122_bit_7 -X122_bit_6 -X122_bit_5 X122_bit_4 X122_bit_3 -X122_bit_2 X122_bit_1 -X122_bit0 X122_bit1 -X122_bit2 -X122_bit3 -X122_bit4 -X122_bit5 -X122_bit6 -X122_bit7 -X122_bit8 -X122_bit9 -X122_bit10 -X122_bit11 -X122_bit12 -X123_bit_7 -X123_bit_6 -X123_bit_5 -X123_bit_4 -X123_bit_3 -X123_bit_2 -X123_bit_1 -X123_bit0 -X123_bit1 -X123_bit2 -X123_bit3 -X123_bit4 -X123_bit5 -X123_bit6 -X123_bit7 -X123_bit8 -X123_bit9 -X123_bit10 -X123_bit11 -X123_bit12 -X124_bit_7 -X124_bit_6 -X124_bit_5 -X124_bit_4 -X124_bit_3 -X124_bit_2 -X124_bit_1 -X124_bit0 -X124_bit1 -X124_bit2 -X124_bit3 -X124_bit4 -X124_bit5 -X124_bit6 -X124_bit7 -X124_bit8 -X124_bit9 -X124_bit10 -X124_bit11 -X124_bit12 -X125_bit_7 -X125_bit_6 -X125_bit_5 -X125_bit_4 -X125_bit_3 -X125_bit_2 -X125_bit_1 -X125_bit0 -X125_bit1 -X125_bit2 -X125_bit3 -X125_bit4 -X125_bit5 -X125_bit6 -X125_bit7 -X125_bit8 -X125_bit9 -X125_bit10 -X125_bit11 -X125_bit12 -X126_bit_7 -X126_bit_6 -X126_bit_5 -X126_bit_4 -X126_bit_3 -X126_bit_2 -X126_bit_1 -X126_bit0 -X126_bit1 -X126_bit2 -X126_bit3 -X126_bit4 -X126_bit5 -X126_bit6 -X126_bit7 -X126_bit8 -X126_bit9 -X126_bit10 -X126_bit11 -X126_bit12 -X127_bit_7 -X127_bit_6 -X127_bit_5 -X127_bit_4 -X127_bit_3 -X127_bit_2 -X127_bit_1 -X127_bit0 -X127_bit1 -X127_bit2 -X127_bit3 -X127_bit4 -X127_bit5 -X127_bit6 -X127_bit7 -X127_bit8 -X127_bit9 -X127_bit10 -X127_bit11 -X127_bit12 -X128_bit_7 -X128_bit_6 -X128_bit_5 -X128_bit_4 -X128_bit_3 -X128_bit_2 -X128_bit_1 -X128_bit0 -X128_bit1 -X128_bit2 -X128_bit3 -X128_bit4 -X128_bit5 -X128_bit6 -X128_bit7 -X128_bit8 -X128_bit9 -X128_bit10 -X128_bit11 -X128_bit12 -X129_bit_7 -X129_bit_6 -X129_bit_5 -X129_bit_4 -X129_bit_3 -X129_bit_2 -X129_bit_1 -X129_bit0 -X129_bit1 -X129_bit2 -X129_bit3 -X129_bit4 -X129_bit5 -X129_bit6 -X129_bit7 -X129_bit8 -X129_bit9 -X129_bit10 -X129_bit11 -X129_bit12 X130_bit_7 X130_bit_6 X130_bit_5 -X130_bit_4 -X130_bit_3 -X130_bit_2 X130_bit_1 -X130_bit0 X130_bit1 X130_bit2 -X130_bit3 -X130_bit4 -X130_bit5 -X130_bit6 -X130_bit7 -X130_bit8 -X130_bit9 -X130_bit10 -X130_bit11 -X130_bit12 -X131_bit_7 -X131_bit_6 -X131_bit_5 -X131_bit_4 -X131_bit_3 -X131_bit_2 -X131_bit_1 -X131_bit0 -X131_bit1 -X131_bit2 -X131_bit3 -X131_bit4 -X131_bit5 -X131_bit6 -X131_bit7 -X131_bit8 -X131_bit9 -X131_bit10 -X131_bit11 -X131_bit12 -X132_bit_7 -X132_bit_6 -X132_bit_5 -X132_bit_4 -X132_bit_3 -X132_bit_2 -X132_bit_1 -X132_bit0 -X132_bit1 -X132_bit2 -X132_bit3 -X132_bit4 -X132_bit5 -X132_bit6 -X132_bit7 -X132_bit8 -X132_bit9 -X132_bit10 -X132_bit11 -X132_bit12 -X133_bit_7 -X133_bit_6 -X133_bit_5 -X133_bit_4 -X133_bit_3 -X133_bit_2 -X133_bit_1 -X133_bit0 -X133_bit1 -X133_bit2 -X133_bit3 -X133_bit4 -X133_bit5 -X133_bit6 -X133_bit7 -X133_bit8 -X133_bit9 -X133_bit10 -X133_bit11 -X133_bit12 X134_bit_7 X134_bit_6 -X134_bit_5 X134_bit_4 -X134_bit_3 -X134_bit_2 -X134_bit_1 -X134_bit0 -X134_bit1 -X134_bit2 -X134_bit3 -X134_bit4 -X134_bit5 -X134_bit6 -X134_bit7 -X134_bit8 -X134_bit9 -X134_bit10 -X134_bit11 -X134_bit12 X135_bit_7 X135_bit_6 X135_bit_5 X135_bit_4 -X135_bit_3 -X135_bit_2 -X135_bit_1 -X135_bit0 X135_bit1 -X135_bit2 -X135_bit3 -X135_bit4 -X135_bit5 -X135_bit6 -X135_bit7 -X135_bit8 -X135_bit9 -X135_bit10 -X135_bit11 -X135_bit12 X136_bit_7 X136_bit_6 X136_bit_5 X136_bit_4 -X136_bit_3 -X136_bit_2 X136_bit_1 -X136_bit0 -X136_bit1 -X136_bit2 -X136_bit3 -X136_bit4 -X136_bit5 -X136_bit6 -X136_bit7 -X136_bit8 -X136_bit9 -X136_bit10 -X136_bit11 -X136_bit12 -X137_bit_7 -X137_bit_6 -X137_bit_5 -X137_bit_4 -X137_bit_3 -X137_bit_2 -X137_bit_1 -X137_bit0 -X137_bit1 -X137_bit2 -X137_bit3 -X137_bit4 -X137_bit5 -X137_bit6 -X137_bit7 -X137_bit8 -X137_bit9 -X137_bit10 -X137_bit11 -X137_bit12 -X138_bit_7 -X138_bit_6 -X138_bit_5 -X138_bit_4 -X138_bit_3 -X138_bit_2 -X138_bit_1 -X138_bit0 -X138_bit1 -X138_bit2 -X138_bit3 -X138_bit4 -X138_bit5 -X138_bit6 -X138_bit7 -X138_bit8 -X138_bit9 -X138_bit10 -X138_bit11 -X138_bit12 -X139_bit_7 -X139_bit_6 -X139_bit_5 -X139_bit_4 -X139_bit_3 -X139_bit_2 -X139_bit_1 -X139_bit0 -X139_bit1 -X139_bit2 -X139_bit3 -X139_bit4 -X139_bit5 -X139_bit6 -X139_bit7 -X139_bit8 -X139_bit9 -X139_bit10 -X139_bit11 -X139_bit12 -X140_bit_7 -X140_bit_6 -X140_bit_5 -X140_bit_4 -X140_bit_3 -X140_bit_2 -X140_bit_1 -X140_bit0 -X140_bit1 -X140_bit2 -X140_bit3 -X140_bit4 -X140_bit5 -X140_bit6 -X140_bit7 -X140_bit8 -X140_bit9 -X140_bit10 -X140_bit11 -X140_bit12 X141_bit_7 X141_bit_6 X141_bit_5 -X141_bit_4 -X141_bit_3 -X141_bit_2 X141_bit_1 -X141_bit0 X141_bit1 X141_bit2 -X141_bit3 -X141_bit4 -X141_bit5 -X141_bit6 -X141_bit7 -X141_bit8 -X141_bit9 -X141_bit10 -X141_bit11 -X141_bit12 X142_bit_7 -X142_bit_6 -X142_bit_5 X142_bit_4 -X142_bit_3 -X142_bit_2 -X142_bit_1 -X142_bit0 -X142_bit1 -X142_bit2 -X142_bit3 -X142_bit4 -X142_bit5 -X142_bit6 -X142_bit7 -X142_bit8 -X142_bit9 -X142_bit10 -X142_bit11 -X142_bit12 -X143_bit_7 -X143_bit_6 -X143_bit_5 -X143_bit_4 -X143_bit_3 -X143_bit_2 -X143_bit_1 -X143_bit0 -X143_bit1 -X143_bit2 -X143_bit3 -X143_bit4 -X143_bit5 -X143_bit6 -X143_bit7 -X143_bit8 -X143_bit9 -X143_bit10 -X143_bit11 -X143_bit12 X144_bit_7 X144_bit_6 X144_bit_5 -X144_bit_4 -X144_bit_3 -X144_bit_2 X144_bit_1 -X144_bit0 -X144_bit1 -X144_bit2 -X144_bit3 -X144_bit4 -X144_bit5 -X144_bit6 -X144_bit7 -X144_bit8 -X144_bit9 -X144_bit10 -X144_bit11 -X144_bit12 -X145_bit_7 -X145_bit_6 -X145_bit_5 -X145_bit_4 -X145_bit_3 -X145_bit_2 -X145_bit_1 -X145_bit0 -X145_bit1 -X145_bit2 -X145_bit3 -X145_bit4 -X145_bit5 -X145_bit6 -X145_bit7 -X145_bit8 -X145_bit9 -X145_bit10 -X145_bit11 -X145_bit12 -X146_bit_7 -X146_bit_6 -X146_bit_5 -X146_bit_4 -X146_bit_3 -X146_bit_2 -X146_bit_1 -X146_bit0 -X146_bit1 -X146_bit2 -X146_bit3 -X146_bit4 -X146_bit5 -X146_bit6 -X146_bit7 -X146_bit8 -X146_bit9 -X146_bit10 -X146_bit11 -X146_bit12 X147_bit_7 X147_bit_6 X147_bit_5 -X147_bit_4 -X147_bit_3 -X147_bit_2 -X147_bit_1 -X147_bit0 -X147_bit1 -X147_bit2 -X147_bit3 -X147_bit4 -X147_bit5 -X147_bit6 -X147_bit7 -X147_bit8 -X147_bit9 -X147_bit10 -X147_bit11 -X147_bit12 X148_bit_7 X148_bit_6 X148_bit_5 -X148_bit_4 X148_bit_3 -X148_bit_2 -X148_bit_1 X148_bit0 X148_bit1 X148_bit2 -X148_bit3 -X148_bit4 -X148_bit5 -X148_bit6 -X148_bit7 -X148_bit8 -X148_bit9 -X148_bit10 -X148_bit11 -X148_bit12 X149_bit_7 -X149_bit_6 -X149_bit_5 -X149_bit_4 -X149_bit_3 -X149_bit_2 X149_bit_1 -X149_bit0 X149_bit1 -X149_bit2 -X149_bit3 -X149_bit4 -X149_bit5 -X149_bit6 -X149_bit7 -X149_bit8 -X149_bit9 -X149_bit10 -X149_bit11 -X149_bit12 X150_bit_7 X150_bit_6 -X150_bit_5 -X150_bit_4 -X150_bit_3 -X150_bit_2 X150_bit_1 -X150_bit0 -X150_bit1 -X150_bit2 -X150_bit3 -X150_bit4 -X150_bit5 -X150_bit6 -X150_bit7 -X150_bit8 -X150_bit9 -X150_bit10 -X150_bit11 -X150_bit12 -X151_bit_7 -X151_bit_6 -X151_bit_5 -X151_bit_4 -X151_bit_3 -X151_bit_2 -X151_bit_1 -X151_bit0 -X151_bit1 -X151_bit2 -X151_bit3 -X151_bit4 -X151_bit5 -X151_bit6 -X151_bit7 -X151_bit8 -X151_bit9 -X151_bit10 -X151_bit11 -X151_bit12 -X152_bit_7 -X152_bit_6 -X152_bit_5 -X152_bit_4 -X152_bit_3 -X152_bit_2 -X152_bit_1 -X152_bit0 -X152_bit1 -X152_bit2 -X152_bit3 -X152_bit4 -X152_bit5 -X152_bit6 -X152_bit7 -X152_bit8 -X152_bit9 -X152_bit10 -X152_bit11 -X152_bit12 X153_bit_7 -X153_bit_6 X153_bit_5 -X153_bit_4 -X153_bit_3 -X153_bit_2 -X153_bit_1 -X153_bit0 -X153_bit1 -X153_bit2 -X153_bit3 -X153_bit4 -X153_bit5 -X153_bit6 -X153_bit7 -X153_bit8 -X153_bit9 -X153_bit10 -X153_bit11 -X153_bit12 X154_bit_7 -X154_bit_6 X154_bit_5 -X154_bit_4 -X154_bit_3 -X154_bit_2 -X154_bit_1 X154_bit0 -X154_bit1 -X154_bit2 -X154_bit3 -X154_bit4 -X154_bit5 -X154_bit6 -X154_bit7 -X154_bit8 -X154_bit9 -X154_bit10 -X154_bit11 -X154_bit12 X155_bit_7 -X155_bit_6 X155_bit_5 X155_bit_4 -X155_bit_3 -X155_bit_2 -X155_bit_1 -X155_bit0 -X155_bit1 -X155_bit2 -X155_bit3 -X155_bit4 -X155_bit5 -X155_bit6 -X155_bit7 -X155_bit8 -X155_bit9 -X155_bit10 -X155_bit11 -X155_bit12 -X156_bit_7 -X156_bit_6 -X156_bit_5 -X156_bit_4 -X156_bit_3 -X156_bit_2 -X156_bit_1 -X156_bit0 -X156_bit1 -X156_bit2 -X156_bit3 -X156_bit4 -X156_bit5 -X156_bit6 -X156_bit7 -X156_bit8 -X156_bit9 -X156_bit10 -X156_bit11 -X156_bit12 -X157_bit_7 -X157_bit_6 -X157_bit_5 -X157_bit_4 -X157_bit_3 -X157_bit_2 -X157_bit_1 -X157_bit0 -X157_bit1 -X157_bit2 -X157_bit3 -X157_bit4 -X157_bit5 -X157_bit6 -X157_bit7 -X157_bit8 -X157_bit9 -X157_bit10 -X157_bit11 -X157_bit12 -X158_bit_7 -X158_bit_6 -X158_bit_5 -X158_bit_4 -X158_bit_3 -X158_bit_2 -X158_bit_1 -X158_bit0 X158_bit1 -X158_bit2 -X158_bit3 -X158_bit4 -X158_bit5 -X158_bit6 -X158_bit7 -X158_bit8 -X158_bit9 -X158_bit10 -X158_bit11 -X158_bit12 -X159_bit_7 -X159_bit_6 -X159_bit_5 -X159_bit_4 -X159_bit_3 -X159_bit_2 -X159_bit_1 -X159_bit0 -X159_bit1 -X159_bit2 -X159_bit3 -X159_bit4 -X159_bit5 -X159_bit6 -X159_bit7 -X159_bit8 -X159_bit9 -X159_bit10 -X159_bit11 -X159_bit12 -X160_bit_7 -X160_bit_6 -X160_bit_5 -X160_bit_4 -X160_bit_3 -X160_bit_2 -X160_bit_1 -X160_bit0 -X160_bit1 -X160_bit2 -X160_bit3 -X160_bit4 -X160_bit5 -X160_bit6 -X160_bit7 -X160_bit8 -X160_bit9 -X160_bit10 -X160_bit11 -X160_bit12 -X161_bit_7 -X161_bit_6 -X161_bit_5 -X161_bit_4 -X161_bit_3 -X161_bit_2 -X161_bit_1 -X161_bit0 X161_bit1 -X161_bit2 -X161_bit3 X161_bit4 -X161_bit5 -X161_bit6 -X161_bit7 -X161_bit8 -X161_bit9 -X161_bit10 -X161_bit11 -X161_bit12 -X162_bit_7 -X162_bit_6 -X162_bit_5 -X162_bit_4 -X162_bit_3 -X162_bit_2 -X162_bit_1 -X162_bit0 -X162_bit1 -X162_bit2 -X162_bit3 -X162_bit4 -X162_bit5 -X162_bit6 -X162_bit7 -X162_bit8 -X162_bit9 -X162_bit10 -X162_bit11 -X162_bit12 -X163_bit_7 -X163_bit_6 -X163_bit_5 -X163_bit_4 -X163_bit_3 -X163_bit_2 -X163_bit_1 -X163_bit0 -X163_bit1 -X163_bit2 -X163_bit3 -X163_bit4 -X163_bit5 -X163_bit6 -X163_bit7 -X163_bit8 -X163_bit9 -X163_bit10 -X163_bit11 -X163_bit12 -X164_bit_7 -X164_bit_6 -X164_bit_5 -X164_bit_4 -X164_bit_3 -X164_bit_2 -X164_bit_1 -X164_bit0 -X164_bit1 -X164_bit2 -X164_bit3 -X164_bit4 -X164_bit5 -X164_bit6 -X164_bit7 -X164_bit8 -X164_bit9 -X164_bit10 -X164_bit11 -X164_bit12 -X165_bit_7 -X165_bit_6 -X165_bit_5 -X165_bit_4 -X165_bit_3 -X165_bit_2 -X165_bit_1 -X165_bit0 -X165_bit1 -X165_bit2 -X165_bit3 -X165_bit4 -X165_bit5 -X165_bit6 -X165_bit7 -X165_bit8 -X165_bit9 -X165_bit10 -X165_bit11 -X165_bit12 -X166_bit_7 -X166_bit_6 -X166_bit_5 -X166_bit_4 -X166_bit_3 -X166_bit_2 -X166_bit_1 -X166_bit0 -X166_bit1 -X166_bit2 -X166_bit3 -X166_bit4 -X166_bit5 -X166_bit6 -X166_bit7 -X166_bit8 -X166_bit9 -X166_bit10 -X166_bit11 -X166_bit12 -X167_bit_7 -X167_bit_6 -X167_bit_5 -X167_bit_4 -X167_bit_3 -X167_bit_2 -X167_bit_1 -X167_bit0 -X167_bit1 -X167_bit2 -X167_bit3 -X167_bit4 -X167_bit5 -X167_bit6 -X167_bit7 -X167_bit8 -X167_bit9 -X167_bit10 -X167_bit11 -X167_bit12 -X168_bit_7 -X168_bit_6 -X168_bit_5 -X168_bit_4 -X168_bit_3 -X168_bit_2 -X168_bit_1 -X168_bit0 -X168_bit1 -X168_bit2 -X168_bit3 -X168_bit4 -X168_bit5 -X168_bit6 -X168_bit7 -X168_bit8 -X168_bit9 -X168_bit10 -X168_bit11 -X168_bit12 Y0_bit0 -Y1_bit0 -Y2_bit0 -Y3_bit0 -Y4_bit0 Y5_bit0 -Y6_bit0 Y7_bit0 Y8_bit0 -Y9_bit0 -Y10_bit0 Y11_bit0 Y12_bit0 Y13_bit0 Y14_bit0 -Y15_bit0 -Y16_bit0 Y17_bit0 Y18_bit0 -Y19_bit0 -Y20_bit0 -Y21_bit0 Y22_bit0 Y23_bit0 Y24_bit0 -Y25_bit0 Y26_bit0 Y27_bit0 -Y28_bit0 Y29_bit0 -Y30_bit0 -Y31_bit0 Y32_bit0 -Y33_bit0 Y34_bit0 Y35_bit0 -Y36_bit0 Y37_bit0 Y38_bit0 -Y39#### 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.86 0.95 0.92 2/54 26654
Raw data (stat): 26654 (runsolver) R 26653 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486375829 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.88 0.95 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 1653 0 0 0 996 3 0 0 25 0 1 0 486375829 8441856 1617 4294967295 134512640 134672761 3221224624 3221223792 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2061 1617 603 41 0 2020 0
vsize: 8244
[startup+20.0013 s]
Raw data (loadavg): 0.90 0.96 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 2671 0 0 0 1992 7 0 0 25 0 1 0 486375829 12644352 2635 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3087 2635 603 41 0 3046 0
vsize: 12348
[startup+30.0014 s]
Raw data (loadavg): 0.91 0.96 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 3014 0 0 0 2991 8 0 0 25 0 1 0 486375829 14123008 2978 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3448 2978 603 41 0 3407 0
vsize: 13792
[startup+40.0021 s]
Raw data (loadavg): 0.93 0.96 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 3306 0 0 0 3989 10 0 0 25 0 1 0 486375829 15204352 3270 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3712 3270 603 41 0 3671 0
vsize: 14848
[startup+50.0022 s]
Raw data (loadavg): 0.94 0.96 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 3600 0 0 0 4988 11 0 0 25 0 1 0 486375829 16420864 3564 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4009 3564 603 41 0 3968 0
vsize: 16036
[startup+60.0033 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 3963 0 0 0 5987 13 0 0 25 0 1 0 486375829 17907712 3927 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4372 3927 603 41 0 4331 0
vsize: 17488
[startup+70.004 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 7842 0 0 0 6978 22 0 0 25 0 1 0 486375829 31891456 7136 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7786 7136 603 41 0 7745 0
vsize: 31144
[startup+80.0043 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 7842 0 0 0 7978 22 0 0 25 0 1 0 486375829 31891456 7136 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7786 7136 603 41 0 7745 0
vsize: 31144
[startup+90.0045 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 7989 0 0 0 8977 22 0 0 25 0 1 0 486375829 31997952 7199 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7812 7199 603 41 0 7771 0
vsize: 31248
[startup+100.004 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 7989 0 0 0 9977 23 0 0 25 0 1 0 486375829 31997952 7199 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7812 7199 603 41 0 7771 0
vsize: 31248
[startup+110.005 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 8078 0 0 0 10977 23 0 0 25 0 1 0 486375829 31997952 7204 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7812 7204 603 41 0 7771 0
vsize: 31248
[startup+120.006 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 8078 0 0 0 11977 23 0 0 25 0 1 0 486375829 31997952 7204 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7812 7204 603 41 0 7771 0
vsize: 31248
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 8120 0 0 0 12977 24 0 0 25 0 1 0 486375829 31997952 7204 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7812 7204 603 41 0 7771 0
vsize: 31248
[startup+140.006 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 8120 0 0 0 13977 24 0 0 25 0 1 0 486375829 31997952 7204 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7812 7204 603 41 0 7771 0
vsize: 31248
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 8120 0 0 0 14977 24 0 0 25 0 1 0 486375829 31997952 7204 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7812 7204 603 41 0 7771 0
vsize: 31248
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 8120 0 0 0 15976 25 0 0 25 0 1 0 486375829 31997952 7204 4294967295 134512640 134672761 3221224624 3221223748 134566029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7812 7204 603 41 0 7771 0
vsize: 31248
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 8519 0 0 0 16975 27 0 0 25 0 1 0 486375829 33615872 7603 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8207 7603 603 41 0 8166 0
vsize: 32828
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 8821 0 0 0 17973 28 0 0 25 0 1 0 486375829 34566144 7845 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8439 7845 603 41 0 8398 0
vsize: 33756
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 8821 0 0 0 18974 28 0 0 25 0 1 0 486375829 34566144 7845 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8439 7845 603 41 0 8398 0
vsize: 33756
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 8821 0 0 0 19974 28 0 0 25 0 1 0 486375829 34566144 7845 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8439 7845 603 41 0 8398 0
vsize: 33756
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 8821 0 0 0 20974 28 0 0 25 0 1 0 486375829 34566144 7845 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8439 7845 603 41 0 8398 0
vsize: 33756
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 9156 0 0 0 21972 30 0 0 25 0 1 0 486375829 36044800 8180 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8800 8180 603 41 0 8759 0
vsize: 35200
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 9401 0 0 0 22971 32 0 0 25 0 1 0 486375829 36990976 8425 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9031 8425 603 41 0 8990 0
vsize: 36124
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 10016 0 0 0 23969 34 0 0 25 0 1 0 486375829 39542784 9040 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9654 9040 603 41 0 9613 0
vsize: 38616
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 10462 0 0 0 24968 34 0 0 25 0 1 0 486375829 41558016 9486 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10146 9486 603 41 0 10105 0
vsize: 40584
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 10904 0 0 0 25967 36 0 0 25 0 1 0 486375829 43077632 9869 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10517 9869 603 41 0 10476 0
vsize: 42068
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 10904 0 0 0 26967 37 0 0 25 0 1 0 486375829 43077632 9869 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10517 9869 603 41 0 10476 0
vsize: 42068
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 10904 0 0 0 27966 37 0 0 25 0 1 0 486375829 43077632 9869 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10517 9869 603 41 0 10476 0
vsize: 42068
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 10904 0 0 0 28966 37 0 0 25 0 1 0 486375829 43077632 9869 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10517 9869 603 41 0 10476 0
vsize: 42068
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 10904 0 0 0 29966 38 0 0 25 0 1 0 486375829 43077632 9869 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10517 9869 603 41 0 10476 0
vsize: 42068
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 10904 0 0 0 30966 38 0 0 25 0 1 0 486375829 43077632 9869 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10517 9869 603 41 0 10476 0
vsize: 42068
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 10909 0 0 0 31966 38 0 0 25 0 1 0 486375829 43077632 9874 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10517 9874 603 41 0 10476 0
vsize: 42068
[startup+330.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 10915 0 0 0 32966 38 0 0 25 0 1 0 486375829 43077632 9880 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10517 9880 603 41 0 10476 0
vsize: 42068
[startup+340.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 10922 0 0 0 33966 39 0 0 25 0 1 0 486375829 43077632 9887 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10517 9887 603 41 0 10476 0
vsize: 42068
[startup+350.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 11655 0 0 0 34964 41 0 0 25 0 1 0 486375829 46174208 10620 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11273 10620 603 41 0 11232 0
vsize: 45092
[startup+360.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 12020 0 0 0 35963 42 0 0 25 0 1 0 486375829 47525888 10985 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11603 10985 603 41 0 11562 0
vsize: 46412
[startup+370.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 12410 0 0 0 36961 44 0 0 25 0 1 0 486375829 49139712 11375 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11997 11375 603 41 0 11956 0
vsize: 47988
[startup+380.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 13105 0 0 0 37960 46 0 0 25 0 1 0 486375829 51965952 12070 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12687 12070 603 41 0 12646 0
vsize: 50748
[startup+390.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 13954 0 0 0 38957 49 0 0 25 0 1 0 486375829 55459840 12919 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13540 12919 603 41 0 13499 0
vsize: 54160
[startup+400.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 14672 0 0 0 39954 51 0 0 25 0 1 0 486375829 58425344 13637 4294967295 134512640 134672761 3221224624 3221223728 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13637 603 41 0 14223 0
vsize: 57056
[startup+410.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 15432 0 0 0 40952 54 0 0 25 0 1 0 486375829 61521920 14397 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15020 14397 603 41 0 14979 0
vsize: 60080
[startup+420.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 16279 0 0 0 41950 56 0 0 25 0 1 0 486375829 65417216 15244 4294967295 134512640 134672761 3221224624 3221223728 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15971 15244 603 41 0 15930 0
vsize: 63884
[startup+430.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17042 0 0 0 42947 59 0 0 25 0 1 0 486375829 68521984 16007 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16729 16007 603 41 0 16688 0
vsize: 66916
[startup+440.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17748 0 0 0 43946 61 0 0 25 0 1 0 486375829 71483392 16713 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17452 16713 603 41 0 17411 0
vsize: 69808
[startup+450.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17883 0 0 0 44945 62 0 0 25 0 1 0 486375829 72011776 16848 4294967295 134512640 134672761 3221224624 3221223808 134559592 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16848 603 41 0 17540 0
vsize: 70324
[startup+460.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17883 0 0 0 45945 62 0 0 25 0 1 0 486375829 72011776 16848 4294967295 134512640 134672761 3221224624 3221223728 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16848 603 41 0 17540 0
vsize: 70324
[startup+470.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17883 0 0 0 46945 62 0 0 25 0 1 0 486375829 72011776 16848 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16848 603 41 0 17540 0
vsize: 70324
[startup+480.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17883 0 0 0 47945 62 0 0 25 0 1 0 486375829 72011776 16848 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16848 603 41 0 17540 0
vsize: 70324
[startup+490.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17885 0 0 0 48945 62 0 0 25 0 1 0 486375829 72011776 16850 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16850 603 41 0 17540 0
vsize: 70324
[startup+500.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17885 0 0 0 49945 63 0 0 25 0 1 0 486375829 72011776 16850 4294967295 134512640 134672761 3221224624 3221223792 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16850 603 41 0 17540 0
vsize: 70324
[startup+510.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17885 0 0 0 50945 63 0 0 25 0 1 0 486375829 72011776 16850 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16850 603 41 0 17540 0
vsize: 70324
[startup+520.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17885 0 0 0 51945 63 0 0 25 0 1 0 486375829 72011776 16850 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16850 603 41 0 17540 0
vsize: 70324
[startup+530.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17885 0 0 0 52945 63 0 0 25 0 1 0 486375829 72011776 16850 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16850 603 41 0 17540 0
vsize: 70324
[startup+540.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17885 0 0 0 53945 64 0 0 25 0 1 0 486375829 72011776 16850 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16850 603 41 0 17540 0
vsize: 70324
[startup+550.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17885 0 0 0 54945 64 0 0 25 0 1 0 486375829 72011776 16850 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16850 603 41 0 17540 0
vsize: 70324
[startup+560.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17885 0 0 0 55945 64 0 0 25 0 1 0 486375829 72011776 16850 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16850 603 41 0 17540 0
vsize: 70324
[startup+570.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17885 0 0 0 56945 65 0 0 25 0 1 0 486375829 72011776 16850 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16850 603 41 0 17540 0
vsize: 70324
[startup+580.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17885 0 0 0 57944 65 0 0 25 0 1 0 486375829 72011776 16850 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16850 603 41 0 17540 0
vsize: 70324
[startup+590.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17885 0 0 0 58944 65 0 0 25 0 1 0 486375829 72011776 16850 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16850 603 41 0 17540 0
vsize: 70324
[startup+600.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17885 0 0 0 59944 66 0 0 25 0 1 0 486375829 72011776 16850 4294967295 134512640 134672761 3221224624 3221223864 134564425 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16850 603 41 0 17540 0
vsize: 70324
[startup+610.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17885 0 0 0 60944 66 0 0 25 0 1 0 486375829 72011776 16850 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16850 603 41 0 17540 0
vsize: 70324
[startup+620.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17885 0 0 0 61944 66 0 0 25 0 1 0 486375829 72011776 16850 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16850 603 41 0 17540 0
vsize: 70324
[startup+630.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17885 0 0 0 62944 66 0 0 25 0 1 0 486375829 72011776 16850 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16850 603 41 0 17540 0
vsize: 70324
[startup+640.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17885 0 0 0 63944 67 0 0 25 0 1 0 486375829 72011776 16850 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16850 603 41 0 17540 0
vsize: 70324
[startup+650.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 17885 0 0 0 64944 67 0 0 25 0 1 0 486375829 72011776 16850 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17581 16850 603 41 0 17540 0
vsize: 70324
[startup+660.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 18117 0 0 0 65943 68 0 0 25 0 1 0 486375829 72949760 17082 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17810 17082 603 41 0 17769 0
vsize: 71240
[startup+670.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 18884 0 0 0 66940 71 0 0 25 0 1 0 486375829 76042240 17849 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18565 17849 603 41 0 18524 0
vsize: 74260
[startup+680.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 19747 0 0 0 67938 74 0 0 25 0 1 0 486375829 79642624 18712 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19444 18713 603 41 0 19403 0
vsize: 77776
[startup+690.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 20479 0 0 0 68936 75 0 0 25 0 1 0 486375829 82595840 19444 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20165 19444 603 41 0 20124 0
vsize: 80660
[startup+700.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 21170 0 0 0 69933 78 0 0 25 0 1 0 486375829 85405696 20135 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20851 20135 603 41 0 20810 0
vsize: 83404
[startup+710.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 21897 0 0 0 70931 81 0 0 25 0 1 0 486375829 88354816 20862 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21571 20862 603 41 0 21530 0
vsize: 86284
[startup+720.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 22712 0 0 0 71929 83 0 0 25 0 1 0 486375829 91701248 21677 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22388 21677 603 41 0 22347 0
vsize: 89552
[startup+730.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 23415 0 0 0 72927 85 0 0 25 0 1 0 486375829 94650368 22380 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23108 22380 603 41 0 23067 0
vsize: 92432
[startup+740.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 24093 0 0 0 73925 87 0 0 25 0 1 0 486375829 97325056 23058 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23761 23058 603 41 0 23720 0
vsize: 95044
[startup+750.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 24835 0 0 0 74923 89 0 0 25 0 1 0 486375829 100397056 23800 4294967295 134512640 134672761 3221224624 3221223808 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24511 23801 603 41 0 24470 0
vsize: 98044
[startup+760.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 25508 0 0 0 75921 91 0 0 25 0 1 0 486375829 103096320 24473 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25170 24473 603 41 0 25129 0
vsize: 100680
[startup+770.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 26215 0 0 0 76919 94 0 0 25 0 1 0 486375829 106049536 25180 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25891 25180 603 41 0 25850 0
vsize: 103564
[startup+780.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 26908 0 0 0 77917 96 0 0 25 0 1 0 486375829 108838912 25873 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26572 25873 603 41 0 26531 0
vsize: 106288
[startup+790.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27525 0 0 0 78917 97 0 0 25 0 1 0 486375829 111370240 26490 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26490 603 41 0 27149 0
vsize: 108760
[startup+800.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27527 0 0 0 79916 97 0 0 25 0 1 0 486375829 111370240 26492 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26492 603 41 0 27149 0
vsize: 108760
[startup+810.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27527 0 0 0 80916 97 0 0 25 0 1 0 486375829 111370240 26492 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26492 603 41 0 27149 0
vsize: 108760
[startup+820.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27527 0 0 0 81916 98 0 0 25 0 1 0 486375829 111370240 26492 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26492 603 41 0 27149 0
vsize: 108760
[startup+830.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27527 0 0 0 82916 98 0 0 25 0 1 0 486375829 111370240 26492 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26492 603 41 0 27149 0
vsize: 108760
[startup+840.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27527 0 0 0 83916 98 0 0 25 0 1 0 486375829 111370240 26492 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26492 603 41 0 27149 0
vsize: 108760
[startup+850.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27527 0 0 0 84916 98 0 0 25 0 1 0 486375829 111370240 26492 4294967295 134512640 134672761 3221224624 3221223776 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26492 603 41 0 27149 0
vsize: 108760
[startup+860.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27527 0 0 0 85916 98 0 0 25 0 1 0 486375829 111370240 26492 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26492 603 41 0 27149 0
vsize: 108760
[startup+870.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27527 0 0 0 86916 99 0 0 25 0 1 0 486375829 111370240 26492 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26492 603 41 0 27149 0
vsize: 108760
[startup+880.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27527 0 0 0 87916 99 0 0 25 0 1 0 486375829 111370240 26492 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26492 603 41 0 27149 0
vsize: 108760
[startup+890.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27527 0 0 0 88916 99 0 0 25 0 1 0 486375829 111370240 26492 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26492 603 41 0 27149 0
vsize: 108760
[startup+900.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27528 0 0 0 89915 100 0 0 25 0 1 0 486375829 111370240 26493 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26493 603 41 0 27149 0
vsize: 108760
[startup+910.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27528 0 0 0 90915 100 0 0 25 0 1 0 486375829 111370240 26493 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26493 603 41 0 27149 0
vsize: 108760
[startup+920.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27528 0 0 0 91915 100 0 0 25 0 1 0 486375829 111370240 26493 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26493 603 41 0 27149 0
vsize: 108760
[startup+930.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27528 0 0 0 92915 100 0 0 25 0 1 0 486375829 111370240 26493 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26493 603 41 0 27149 0
vsize: 108760
[startup+940.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27528 0 0 0 93915 101 0 0 25 0 1 0 486375829 111370240 26493 4294967295 134512640 134672761 3221224624 3221223728 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26493 603 41 0 27149 0
vsize: 108760
[startup+950.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27528 0 0 0 94915 101 0 0 25 0 1 0 486375829 111370240 26493 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26493 603 41 0 27149 0
vsize: 108760
[startup+960.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27528 0 0 0 95915 101 0 0 25 0 1 0 486375829 111370240 26493 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26493 603 41 0 27149 0
vsize: 108760
[startup+970.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27528 0 0 0 96915 101 0 0 25 0 1 0 486375829 111370240 26493 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26493 603 41 0 27149 0
vsize: 108760
[startup+980.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27528 0 0 0 97914 102 0 0 25 0 1 0 486375829 111370240 26493 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26493 603 41 0 27149 0
vsize: 108760
[startup+990.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27528 0 0 0 98914 102 0 0 25 0 1 0 486375829 111370240 26493 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26493 603 41 0 27149 0
vsize: 108760
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 27528 0 0 0 99914 102 0 0 25 0 1 0 486375829 111370240 26493 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27190 26493 603 41 0 27149 0
vsize: 108760
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 28348 0 0 0 100912 105 0 0 25 0 1 0 486375829 114712576 27313 4294967295 134512640 134672761 3221224624 3221223728 134560322 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28006 27313 603 41 0 27965 0
vsize: 112024
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 29252 0 0 0 101910 107 0 0 25 0 1 0 486375829 118472704 28217 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28924 28217 603 41 0 28883 0
vsize: 115696
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 30091 0 0 0 102907 110 0 0 25 0 1 0 486375829 121913344 29056 4294967295 134512640 134672761 3221224624 3221223808 134559482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29764 29056 603 41 0 29723 0
vsize: 119056
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 30940 0 0 0 103905 113 0 0 25 0 1 0 486375829 125390848 29905 4294967295 134512640 134672761 3221224624 3221223728 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30613 29905 603 41 0 30572 0
vsize: 122452
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 31733 0 0 0 104903 115 0 0 25 0 1 0 486375829 128589824 30698 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31394 30698 603 41 0 31353 0
vsize: 125576
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 32493 0 0 0 105901 117 0 0 25 0 1 0 486375829 131780608 31458 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32173 31458 603 41 0 32132 0
vsize: 128692
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 33210 0 0 0 106899 119 0 0 25 0 1 0 486375829 134717440 32175 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32890 32175 603 41 0 32849 0
vsize: 131560
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 33918 0 0 0 107898 120 0 0 25 0 1 0 486375829 137641984 32883 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33604 32883 603 41 0 33563 0
vsize: 134416
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 34558 0 0 0 108896 122 0 0 25 0 1 0 486375829 140226560 33523 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34235 33523 603 41 0 34194 0
vsize: 136940
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 35232 0 0 0 109893 125 0 0 25 0 1 0 486375829 142921728 34197 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34893 34197 603 41 0 34852 0
vsize: 139572
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 35982 0 0 0 110892 127 0 0 25 0 1 0 486375829 146018304 34947 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35649 34947 603 41 0 35608 0
vsize: 142596
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 36698 0 0 0 111889 130 0 0 25 0 1 0 486375829 148955136 35663 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36366 35663 603 41 0 36325 0
vsize: 145464
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 37425 0 0 0 112887 132 0 0 25 0 1 0 486375829 151912448 36390 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37088 36390 603 41 0 37047 0
vsize: 148352
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 38013 0 0 0 113885 134 0 0 25 0 1 0 486375829 154308608 36978 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37673 36978 603 41 0 37632 0
vsize: 150692
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 38732 0 0 0 114884 135 0 0 25 0 1 0 486375829 157261824 37697 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38394 37697 603 41 0 38353 0
vsize: 153576
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.92 3/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 39454 0 0 0 115882 137 0 0 25 0 1 0 486375829 160292864 38419 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39134 38419 603 41 0 39093 0
vsize: 156536
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 40071 0 0 0 116881 139 0 0 25 0 1 0 486375829 162832384 39036 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39754 39036 603 41 0 39713 0
vsize: 159016
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 40819 0 0 0 117878 141 0 0 25 0 1 0 486375829 165892096 39784 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40501 39784 603 41 0 40460 0
vsize: 162004
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 41505 0 0 0 118876 144 0 0 25 0 1 0 486375829 168681472 40470 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41182 40470 603 41 0 41141 0
vsize: 164728
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 26654
Raw data (stat): 26654 (minisat+) R 26653 20937 20936 0 -1 0 42184 0 0 0 119874 146 0 0 25 0 1 0 486375829 171491328 41149 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41868 41149 603 41 0 41827 0
vsize: 167472
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 26654
Raw data (stat): 26654 (minisat+) Z 26653 20937 20936 0 -1 12 42187 0 0 0 119875 154 0 0 25 0 1 0 486375829 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.13
CPU time (s): 1200.3
CPU user time (s): 1198.75
CPU system time (s): 1.54477
CPU usage (%): 100.014
Max. virtual memory (Kb): 167472
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####