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 17642

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-21 11:05:01 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19289 boxname=wulflinc12 idbench=1484 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  688d61d0de54e028c8c4910e094a132c  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-ran13x13.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-ran13x13.opb /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-ran13x13.opb
IDLAUNCH: 19289
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        842512 kB
Buffers:         12196 kB
Cached:         158792 kB
SwapCached:        508 kB
Active:          14708 kB
Inactive:       158388 kB
HighTotal:      131008 kB
HighFree:        83020 kB
LowTotal:       903652 kB
LowFree:        759492 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5276 kB
Slab:            13480 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:25:03 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 19289 7 1200.25 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]---> Adder-cost: 192   maxlim: 3187   bits: 12/12
c ---[ 171]---> Adder-cost: 272   maxlim: 32499   bits: 16/15
c ---[ 169]---> Adder-cost: 272   maxlim: 32755   bits: 16/15
c ---[ 168]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 167]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 166]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 165]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 164]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 163]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 162]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 161]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 160]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 159]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 158]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 157]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 156]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 155]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 154]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 153]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 152]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 151]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 150]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 149]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 148]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 147]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 146]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 145]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 144]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 143]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 142]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 141]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 140]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 139]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 138]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 137]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 136]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 135]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 134]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 133]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 132]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 131]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 130]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 129]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 128]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 127]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 126]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 125]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 124]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 123]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 122]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 121]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 120]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 119]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 118]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 117]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 116]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 115]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 114]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 113]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 112]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 111]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 110]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 109]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 108]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 107]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 106]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 105]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 104]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 103]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 102]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 101]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 100]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  99]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  98]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  97]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  96]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  95]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  94]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  93]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  92]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  91]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  90]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  89]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  88]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  87]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  86]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  85]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  84]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  83]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  82]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  81]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  80]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  79]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  78]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  77]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  76]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  75]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  74]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  73]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  72]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  71]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  70]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  69]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  68]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  67]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  66]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  65]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  64]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  63]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  62]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  61]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  60]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  59]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  58]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  57]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  56]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  55]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  54]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  53]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  52]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  51]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  50]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  49]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  48]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  47]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  46]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  45]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  44]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  43]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  42]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  41]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  40]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  39]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  38]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  37]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  36]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  35]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  34]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  33]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  32]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  31]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  30]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  29]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  28]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  27]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  26]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  25]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  24]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  23]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  22]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  21]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  20]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  19]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  18]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  17]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  16]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  15]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  14]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  13]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  12]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  11]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  10]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[   9]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   8]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   7]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   6]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   5]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[   4]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[   3]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   2]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[   1]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[   0]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   48623   178707 |   16207       0        0     nan |  0.000 % |
c |       100 |   48623   178707 |   17827     100      295     3.0 | 31.998 % |
c |       250 |   48608   178658 |   19610     247     1071     4.3 | 32.013 % |
c |       475 |   48599   178629 |   21571     471     2108     4.5 | 32.028 % |
c |       812 |   48541   178435 |   23728     801     3991     5.0 | 32.098 % |
c |      1318 |   48521   178371 |   26101    1304     7600     5.8 | 32.121 % |
c |      2077 |   48411   178001 |   28711    2049    11420     5.6 | 32.282 % |
c |      3217 |   48146   177110 |   31582    3159    17208     5.4 | 32.644 % |
c |      4925 |   47845   176099 |   34741    4825    25548     5.3 | 33.074 % |
c |      7488 |   47529   175041 |   38215    7335    39062     5.3 | 33.482 % |
c |     11333 |   47171   173841 |   42036   11118    59586     5.4 | 33.967 % |
c |     17099 |   46966   173144 |   46240   16841   103505     6.1 | 34.220 % |
c |     25748 |   46638   172046 |   50864   25439   360755    14.2 | 34.674 % |
c |     38723 |   46499   171577 |   55950   38395   670558    17.5 | 34.867 % |
c |     58184 |   46434   171362 |   61546   57843  1817884    31.4 | 34.951 % |
c |     87376 |   46403   171257 |   67700   41343  1241847    30.0 | 34.990 % |
c |    131165 |   46403   171257 |   74470   27072   564032    20.8 | 34.990 % |
c ==============================================================================
c [1mFound solution: 3567712[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 6664   maxlim: 2125082   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    162848 |   92949   337562 |   30983   58751  1065834    18.1 | 34.990 % |
c |    162948 |   92949   337562 |   34081   23113   333014    14.4 | 23.182 % |
c |    163098 |   92949   337562 |   37489   23263   334017    14.4 | 23.182 % |
c |    163323 |   92949   337562 |   41238   23488   335334    14.3 | 23.182 % |
c |    163661 |   92949   337562 |   45362   23826   337586    14.2 | 23.182 % |
c |    164167 |   92949   337562 |   49898   24332   343220    14.1 | 23.182 % |
c |    164926 |   92949   337562 |   54888   25091   350058    14.0 | 23.182 % |
c |    166065 |   92949   337562 |   60377   26230   358050    13.7 | 23.182 % |
c |    167774 |   92949   337562 |   66414   27939   380205    13.6 | 23.182 % |
c |    170337 |   92949   337562 |   73056   30502   442856    14.5 | 23.182 % |
c |    174181 |   92949   337562 |   80361   34346   504780    14.7 | 23.182 % |
c |    179947 |   92934   337511 |   88398   40108   583777    14.6 | 23.192 % |
c |    188597 |   92934   337511 |   97237   48758  1299506    26.7 | 23.192 % |
c ==============================================================================
c [1mFound solution: 3541142[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2151652   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    199987 |   92963   337732 |   30987   60148  1515182    25.2 | 23.192 % |
c |    200088 |   92963   337732 |   34085   25447   352433    13.8 | 23.227 % |
c |    200238 |   92963   337732 |   37494   25597   353016    13.8 | 23.227 % |
c |    200463 |   92963   337732 |   41243   25822   354278    13.7 | 23.227 % |
c |    200801 |   92963   337732 |   45368   26160   356198    13.6 | 23.227 % |
c |    201307 |   92963   337732 |   49904   26666   359330    13.5 | 23.227 % |
c |    202066 |   92963   337732 |   54895   27425   365579    13.3 | 23.227 % |
c |    203205 |   92963   337732 |   60384   28564   375570    13.1 | 23.227 % |
c |    204915 |   92963   337732 |   66423   30274   395651    13.1 | 23.227 % |
c |    207478 |   92963   337732 |   73065   32837   429133    13.1 | 23.227 % |
c |    211323 |   92963   337732 |   80372   36682   472427    12.9 | 23.227 % |
c |    217089 |   92963   337732 |   88409   42448   839113    19.8 | 23.227 % |
c |    225738 |   92963   337732 |   97250   51097  1513787    29.6 | 23.227 % |
c |    238713 |   92963   337732 |  106975   64072  3128164    48.8 | 23.227 % |
c ==============================================================================
c [1mFound solution: 2383791[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3309003   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    245929 |   92952   337825 |   30984   71283  3263930    45.8 | 23.227 % |
c |    246029 |   92952   337825 |   34082   23986   902627    37.6 | 23.306 % |
c |    246179 |   92952   337825 |   37490   24136   903388    37.4 | 23.306 % |
c |    246404 |   92952   337825 |   41239   24361   904420    37.1 | 23.306 % |
c |    246741 |   92952   337825 |   45363   24698   906312    36.7 | 23.306 % |
c |    247247 |   92952   337825 |   49900   25204   909975    36.1 | 23.306 % |
c |    248007 |   92952   337825 |   54890   25964   915108    35.2 | 23.306 % |
c |    249147 |   92952   337825 |   60379   27104   923859    34.1 | 23.306 % |
c |    250855 |   92952   337825 |   66416   28812   936901    32.5 | 23.306 % |
c |    253417 |   92952   337825 |   73058   31374   956660    30.5 | 23.306 % |
c |    257261 |   92946   337805 |   80364   35215   992195    28.2 | 23.311 % |
c |    263027 |   92946   337805 |   88400   40981  1071524    26.1 | 23.311 % |
c |    271676 |   92946   337805 |   97241   49630  2805442    56.5 | 23.311 % |
c |    284651 |   92946   337805 |  106965   62605  3186835    50.9 | 23.311 % |
c |    304112 |   92946   337805 |  117661   82066  3958370    48.2 | 23.311 % |
c ==============================================================================
c [1mFound solution: 1926978[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3765816   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    305048 |   92957   337957 |   30985   82999  3987511    48.0 | 23.311 % |
c |    305148 |   92957   337957 |   34083   19111   570471    29.9 | 23.355 % |
c |    305298 |   92957   337957 |   37491   19261   571259    29.7 | 23.355 % |
c |    305523 |   92957   337957 |   41241   19486   573450    29.4 | 23.355 % |
c |    305860 |   92957   337957 |   45365   19823   575290    29.0 | 23.355 % |
c |    306367 |   92957   337957 |   49901   20330   577799    28.4 | 23.355 % |
c |    307126 |   92957   337957 |   54891   21089   581476    27.6 | 23.355 % |
c |    308265 |   92957   337957 |   60380   22228   587264    26.4 | 23.355 % |
c |    309973 |   92957   337957 |   66419   23936   597341    25.0 | 23.355 % |
c |    312535 |   92957   337957 |   73061   26498   622401    23.5 | 23.355 % |
c |    316379 |   92957   337957 |   80367   30342   687046    22.6 | 23.355 % |
c |    322146 |   92957   337957 |   88403   36109   823731    22.8 | 23.355 % |
c |    330796 |   92951   337937 |   97244   44758  1115046    24.9 | 23.360 % |
c |    343770 |   92951   337937 |  106968   57732  1483223    25.7 | 23.360 % |
c |    363234 |   92945   337920 |  117665   77193  2455697    31.8 | 23.365 % |
c |    392427 |   92945   337920 |  129432  106386  3644798    34.3 | 23.365 % |
c |    436216 |   92945   337920 |  142375   38815  1837204    47.3 | 23.365 % |
c |    501901 |   92945   337920 |  156612  104500  4212994    40.3 | 23.365 % |
c |    600427 |   92929   337868 |  172274   60196  2513912    41.8 | 23.381 % |
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_bit0 Y40_bit0 -Y4#### 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.85 0.97 0.91 2/54 28517
Raw data (stat): 28517 (runsolver) R 28516 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486355501 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0004 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 28517
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 1597 0 0 0 994 4 0 0 25 0 1 0 486355501 8425472 1566 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2057 1566 603 41 0 2016 0
vsize: 8228
[startup+20.0017 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 28517
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 1710 0 0 0 1994 5 0 0 25 0 1 0 486355501 8847360 1679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2160 1679 603 41 0 2119 0
vsize: 8640
[startup+30.0025 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 28517
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 2097 0 0 0 2992 7 0 0 25 0 1 0 486355501 10547200 2066 4294967295 134512640 134672761 3221224544 3221223736 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2575 2066 603 41 0 2534 0
vsize: 10300
[startup+40.0034 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 28517
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 2532 0 0 0 3990 9 0 0 25 0 1 0 486355501 12427264 2501 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3034 2501 603 41 0 2993 0
vsize: 12136
[startup+50.0063 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 3382 0 0 0 4987 12 0 0 25 0 1 0 486355501 15794176 3351 4294967295 134512640 134672761 3221224544 3221223668 134566142 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3856 3351 603 41 0 3815 0
vsize: 15424
[startup+60.0061 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 4020 0 0 0 5985 14 0 0 25 0 1 0 486355501 18358272 3989 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4482 3989 603 41 0 4441 0
vsize: 17928
[startup+70.0065 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 4489 0 0 0 6983 16 0 0 25 0 1 0 486355501 20504576 4458 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5006 4458 603 41 0 4965 0
vsize: 20024
[startup+80.0078 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 4489 0 0 0 7983 16 0 0 25 0 1 0 486355501 20504576 4458 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5006 4458 603 41 0 4965 0
vsize: 20024
[startup+90.0087 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 4786 0 0 0 8982 17 0 0 25 0 1 0 486355501 21716992 4755 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5302 4755 603 41 0 5261 0
vsize: 21208
[startup+100.009 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 5223 0 0 0 9980 19 0 0 25 0 1 0 486355501 23461888 5192 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5728 5192 603 41 0 5687 0
vsize: 22912
[startup+110.01 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 5224 0 0 0 10980 19 0 0 25 0 1 0 486355501 23461888 5193 4294967295 134512640 134672761 3221224544 3221223712 134564686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5728 5193 603 41 0 5687 0
vsize: 22912
[startup+120.016 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 5224 0 0 0 11981 19 0 0 25 0 1 0 486355501 23461888 5193 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5728 5193 603 41 0 5687 0
vsize: 22912
[startup+130.016 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 5224 0 0 0 12981 20 0 0 25 0 1 0 486355501 23461888 5193 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5728 5193 603 41 0 5687 0
vsize: 22912
[startup+140.017 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 5545 0 0 0 13979 21 0 0 25 0 1 0 486355501 24981504 5470 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6099 5470 603 41 0 6058 0
vsize: 24396
[startup+150.017 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 5545 0 0 0 14979 21 0 0 25 0 1 0 486355501 24981504 5470 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6099 5470 603 41 0 6058 0
vsize: 24396
[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 5545 0 0 0 15979 21 0 0 25 0 1 0 486355501 24981504 5470 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6099 5470 603 41 0 6058 0
vsize: 24396
[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 5545 0 0 0 16979 22 0 0 25 0 1 0 486355501 24981504 5470 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6099 5470 603 41 0 6058 0
vsize: 24396
[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 5545 0 0 0 17979 22 0 0 25 0 1 0 486355501 24981504 5470 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6099 5470 603 41 0 6058 0
vsize: 24396
[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 5546 0 0 0 18978 22 0 0 25 0 1 0 486355501 24981504 5471 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6099 5471 603 41 0 6058 0
vsize: 24396
[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 5546 0 0 0 19978 23 0 0 25 0 1 0 486355501 24981504 5471 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6099 5471 603 41 0 6058 0
vsize: 24396
[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 5546 0 0 0 20978 23 0 0 25 0 1 0 486355501 24981504 5471 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6099 5471 603 41 0 6058 0
vsize: 24396
[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 5546 0 0 0 21978 23 0 0 25 0 1 0 486355501 24981504 5471 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6099 5471 603 41 0 6058 0
vsize: 24396
[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 6485 0 0 0 22976 25 0 0 25 0 1 0 486355501 28889088 6410 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7053 6410 603 41 0 7012 0
vsize: 28212
[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 6889 0 0 0 23975 26 0 0 25 0 1 0 486355501 30502912 6814 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7447 6814 603 41 0 7406 0
vsize: 29788
[startup+250.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 6988 0 0 0 24975 26 0 0 25 0 1 0 486355501 30855168 6908 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7533 6908 603 41 0 7492 0
vsize: 30132
[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 6988 0 0 0 25975 26 0 0 25 0 1 0 486355501 30855168 6908 4294967295 134512640 134672761 3221224544 3221223668 134566018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7533 6908 603 41 0 7492 0
vsize: 30132
[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 6988 0 0 0 26975 26 0 0 25 0 1 0 486355501 30855168 6908 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7533 6908 603 41 0 7492 0
vsize: 30132
[startup+280.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 6988 0 0 0 27975 26 0 0 25 0 1 0 486355501 30855168 6908 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7533 6908 603 41 0 7492 0
vsize: 30132
[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 6988 0 0 0 28976 26 0 0 25 0 1 0 486355501 30855168 6908 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7533 6908 603 41 0 7492 0
vsize: 30132
[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 6988 0 0 0 29976 26 0 0 25 0 1 0 486355501 30855168 6908 4294967295 134512640 134672761 3221224544 3221223728 134559611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7533 6908 603 41 0 7492 0
vsize: 30132
[startup+310.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 7226 0 0 0 30976 27 0 0 25 0 1 0 486355501 31936512 7146 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7797 7146 603 41 0 7756 0
vsize: 31188
[startup+320.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 7838 0 0 0 31974 29 0 0 25 0 1 0 486355501 34361344 7758 4294967295 134512640 134672761 3221224544 3221223744 134557876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8389 7758 603 41 0 8348 0
vsize: 33556
[startup+330.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 7960 0 0 0 32973 29 0 0 25 0 1 0 486355501 34811904 7878 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8499 7878 603 41 0 8458 0
vsize: 33996
[startup+340.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 7960 0 0 0 33974 29 0 0 25 0 1 0 486355501 34811904 7878 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8499 7878 603 41 0 8458 0
vsize: 33996
[startup+350.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 7960 0 0 0 34974 29 0 0 25 0 1 0 486355501 34811904 7878 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8499 7878 603 41 0 8458 0
vsize: 33996
[startup+360.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 7960 0 0 0 35974 30 0 0 25 0 1 0 486355501 34811904 7878 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8499 7878 603 41 0 8458 0
vsize: 33996
[startup+370.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 7960 0 0 0 36974 30 0 0 25 0 1 0 486355501 34811904 7878 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8499 7878 603 41 0 8458 0
vsize: 33996
[startup+380.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 7960 0 0 0 37974 30 0 0 25 0 1 0 486355501 34811904 7878 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8499 7878 603 41 0 8458 0
vsize: 33996
[startup+390.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 7960 0 0 0 38974 30 0 0 25 0 1 0 486355501 34811904 7878 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8499 7878 603 41 0 8458 0
vsize: 33996
[startup+400.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 7970 0 0 0 39974 30 0 0 25 0 1 0 486355501 34811904 7888 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8499 7888 603 41 0 8458 0
vsize: 33996
[startup+410.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 7981 0 0 0 40974 30 0 0 25 0 1 0 486355501 34811904 7899 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8499 7899 603 41 0 8458 0
vsize: 33996
[startup+420.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 8310 0 0 0 41973 31 0 0 25 0 1 0 486355501 36155392 8228 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8827 8228 603 41 0 8786 0
vsize: 35308
[startup+430.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 9233 0 0 0 42971 34 0 0 25 0 1 0 486355501 39936000 9151 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9750 9151 603 41 0 9709 0
vsize: 39000
[startup+440.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 9707 0 0 0 43969 36 0 0 25 0 1 0 486355501 42352640 9625 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10340 9625 603 41 0 10299 0
vsize: 41360
[startup+450.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 9954 0 0 0 44968 37 0 0 25 0 1 0 486355501 43417600 9872 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10600 9872 603 41 0 10559 0
vsize: 42400
[startup+460.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 9954 0 0 0 45968 37 0 0 25 0 1 0 486355501 43417600 9872 4294967295 134512640 134672761 3221224544 3221223712 134564490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10600 9872 603 41 0 10559 0
vsize: 42400
[startup+470.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 9954 0 0 0 46969 37 0 0 25 0 1 0 486355501 43417600 9872 4294967295 134512640 134672761 3221224544 3221223592 1075349622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10600 9872 603 41 0 10559 0
vsize: 42400
[startup+480.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 9954 0 0 0 47969 37 0 0 25 0 1 0 486355501 43417600 9872 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10600 9872 603 41 0 10559 0
vsize: 42400
[startup+490.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 9954 0 0 0 48969 37 0 0 25 0 1 0 486355501 43417600 9872 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10600 9872 603 41 0 10559 0
vsize: 42400
[startup+500.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 9954 0 0 0 49969 37 0 0 25 0 1 0 486355501 43417600 9872 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10600 9872 603 41 0 10559 0
vsize: 42400
[startup+510.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 9954 0 0 0 50969 37 0 0 25 0 1 0 486355501 43417600 9872 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10600 9872 603 41 0 10559 0
vsize: 42400
[startup+520.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 9954 0 0 0 51969 37 0 0 25 0 1 0 486355501 43417600 9872 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10600 9872 603 41 0 10559 0
vsize: 42400
[startup+530.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 9954 0 0 0 52970 37 0 0 25 0 1 0 486355501 43417600 9872 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10600 9872 603 41 0 10559 0
vsize: 42400
[startup+540.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 9954 0 0 0 53970 37 0 0 25 0 1 0 486355501 43417600 9872 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10600 9872 603 41 0 10559 0
vsize: 42400
[startup+550.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 9954 0 0 0 54970 37 0 0 25 0 1 0 486355501 43417600 9872 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10600 9872 603 41 0 10559 0
vsize: 42400
[startup+560.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 9954 0 0 0 55970 37 0 0 25 0 1 0 486355501 43417600 9872 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10600 9872 603 41 0 10559 0
vsize: 42400
[startup+570.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 10205 0 0 0 56970 37 0 0 25 0 1 0 486355501 44359680 10123 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10830 10123 603 41 0 10789 0
vsize: 43320
[startup+580.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 10660 0 0 0 57969 39 0 0 25 0 1 0 486355501 46247936 10578 4294967295 134512640 134672761 3221224544 3221223728 134559509 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11291 10578 603 41 0 11250 0
vsize: 45164
[startup+590.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 10986 0 0 0 58968 40 0 0 25 0 1 0 486355501 47599616 10904 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11621 10904 603 41 0 11580 0
vsize: 46484
[startup+600.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 11173 0 0 0 59968 40 0 0 25 0 1 0 486355501 48410624 11091 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11819 11091 603 41 0 11778 0
vsize: 47276
[startup+610.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 11413 0 0 0 60967 41 0 0 25 0 1 0 486355501 49348608 11331 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12048 11331 603 41 0 12007 0
vsize: 48192
[startup+620.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 11809 0 0 0 61966 42 0 0 25 0 1 0 486355501 50954240 11727 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12440 11727 603 41 0 12399 0
vsize: 49760
[startup+630.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 12229 0 0 0 62965 43 0 0 25 0 1 0 486355501 52568064 12147 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12834 12147 603 41 0 12793 0
vsize: 51336
[startup+640.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 12684 0 0 0 63965 44 0 0 25 0 1 0 486355501 54460416 12602 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13296 12602 603 41 0 13255 0
vsize: 53184
[startup+650.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 12697 0 0 0 64965 44 0 0 25 0 1 0 486355501 54460416 12615 4294967295 134512640 134672761 3221224544 3221223708 134564515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13296 12615 603 41 0 13255 0
vsize: 53184
[startup+660.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 12697 0 0 0 65965 44 0 0 25 0 1 0 486355501 54460416 12615 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13296 12615 603 41 0 13255 0
vsize: 53184
[startup+670.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 12697 0 0 0 66965 44 0 0 25 0 1 0 486355501 54460416 12615 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13296 12615 603 41 0 13255 0
vsize: 53184
[startup+680.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 12697 0 0 0 67965 44 0 0 25 0 1 0 486355501 54460416 12615 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13296 12615 603 41 0 13255 0
vsize: 53184
[startup+690.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 12697 0 0 0 68965 44 0 0 25 0 1 0 486355501 54460416 12615 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13296 12615 603 41 0 13255 0
vsize: 53184
[startup+700.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 12697 0 0 0 69964 44 0 0 25 0 1 0 486355501 54460416 12615 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13296 12615 603 41 0 13255 0
vsize: 53184
[startup+710.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 12697 0 0 0 70965 44 0 0 25 0 1 0 486355501 54460416 12615 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13296 12615 603 41 0 13255 0
vsize: 53184
[startup+720.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 12697 0 0 0 71965 44 0 0 25 0 1 0 486355501 54460416 12615 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13296 12615 603 41 0 13255 0
vsize: 53184
[startup+730.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 12697 0 0 0 72965 44 0 0 25 0 1 0 486355501 54460416 12615 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13296 12615 603 41 0 13255 0
vsize: 53184
[startup+740.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 12697 0 0 0 73965 44 0 0 25 0 1 0 486355501 54460416 12615 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13296 12615 603 41 0 13255 0
vsize: 53184
[startup+750.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 12697 0 0 0 74965 44 0 0 25 0 1 0 486355501 54460416 12615 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13296 12615 603 41 0 13255 0
vsize: 53184
[startup+760.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 12697 0 0 0 75965 44 0 0 25 0 1 0 486355501 54460416 12615 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13296 12615 603 41 0 13255 0
vsize: 53184
[startup+770.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 12697 0 0 0 76966 44 0 0 25 0 1 0 486355501 54460416 12615 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13296 12615 603 41 0 13255 0
vsize: 53184
[startup+780.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 12697 0 0 0 77966 44 0 0 25 0 1 0 486355501 54460416 12615 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13296 12615 603 41 0 13255 0
vsize: 53184
[startup+790.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 12697 0 0 0 78966 44 0 0 25 0 1 0 486355501 54460416 12615 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13296 12615 603 41 0 13255 0
vsize: 53184
[startup+800.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 12697 0 0 0 79966 45 0 0 25 0 1 0 486355501 54460416 12615 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13296 12615 603 41 0 13255 0
vsize: 53184
[startup+810.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 12932 0 0 0 80965 45 0 0 25 0 1 0 486355501 55533568 12850 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13558 12850 603 41 0 13517 0
vsize: 54232
[startup+820.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 13276 0 0 0 81965 46 0 0 25 0 1 0 486355501 56881152 13194 4294967295 134512640 134672761 3221224544 3221223728 134559514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13887 13194 603 41 0 13846 0
vsize: 55548
[startup+830.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 13628 0 0 0 82964 48 0 0 25 0 1 0 486355501 58351616 13546 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14246 13546 603 41 0 14205 0
vsize: 56984
[startup+840.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 13964 0 0 0 83963 48 0 0 25 0 1 0 486355501 59695104 13882 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14574 13882 603 41 0 14533 0
vsize: 58296
[startup+850.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 14273 0 0 0 84962 50 0 0 25 0 1 0 486355501 61030400 14191 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14900 14191 603 41 0 14859 0
vsize: 59600
[startup+860.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 14591 0 0 0 85961 51 0 0 25 0 1 0 486355501 62373888 14509 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15228 14509 603 41 0 15187 0
vsize: 60912
[startup+870.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 14926 0 0 0 86960 53 0 0 25 0 1 0 486355501 63746048 14844 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15563 14845 603 41 0 15522 0
vsize: 62252
[startup+880.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 15267 0 0 0 87959 54 0 0 25 0 1 0 486355501 65081344 15185 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15889 15185 603 41 0 15848 0
vsize: 63556
[startup+890.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 15576 0 0 0 88958 54 0 0 25 0 1 0 486355501 66326528 15494 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16193 15494 603 41 0 16152 0
vsize: 64772
[startup+900.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 15861 0 0 0 89958 55 0 0 25 0 1 0 486355501 67674112 15779 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16522 15779 603 41 0 16481 0
vsize: 66088
[startup+910.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 16136 0 0 0 90957 56 0 0 25 0 1 0 486355501 68747264 16054 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16784 16054 603 41 0 16743 0
vsize: 67136
[startup+920.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 16431 0 0 0 91957 56 0 0 25 0 1 0 486355501 69955584 16349 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16349 603 41 0 17038 0
vsize: 68316
[startup+930.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 16713 0 0 0 92956 57 0 0 25 0 1 0 486355501 71036928 16631 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17343 16631 603 41 0 17302 0
vsize: 69372
[startup+940.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 16971 0 0 0 93955 58 0 0 25 0 1 0 486355501 72118272 16889 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17607 16889 603 41 0 17566 0
vsize: 70428
[startup+950.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 17219 0 0 0 94954 59 0 0 25 0 1 0 486355501 73191424 17137 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17869 17137 603 41 0 17828 0
vsize: 71476
[startup+960.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 17487 0 0 0 95954 60 0 0 25 0 1 0 486355501 74276864 17405 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18134 17405 603 41 0 18093 0
vsize: 72536
[startup+970.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 17752 0 0 0 96953 61 0 0 25 0 1 0 486355501 75395072 17670 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18407 17670 603 41 0 18366 0
vsize: 73628
[startup+980.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 18017 0 0 0 97952 62 0 0 25 0 1 0 486355501 76464128 17935 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18668 17935 603 41 0 18627 0
vsize: 74672
[startup+990.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 18298 0 0 0 98952 62 0 0 25 0 1 0 486355501 77664256 18216 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18961 18216 603 41 0 18920 0
vsize: 75844
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 18567 0 0 0 99951 63 0 0 25 0 1 0 486355501 78733312 18485 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19222 18485 603 41 0 19181 0
vsize: 76888
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 18860 0 0 0 100951 64 0 0 25 0 1 0 486355501 79929344 18778 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19514 18778 603 41 0 19473 0
vsize: 78056
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 19123 0 0 0 101950 65 0 0 25 0 1 0 486355501 80990208 19041 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19773 19041 603 41 0 19732 0
vsize: 79092
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 19387 0 0 0 102950 65 0 0 25 0 1 0 486355501 82059264 19305 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20034 19305 603 41 0 19993 0
vsize: 80136
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 19640 0 0 0 103949 66 0 0 25 0 1 0 486355501 83185664 19558 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20309 19558 603 41 0 20268 0
vsize: 81236
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 19892 0 0 0 104949 66 0 0 25 0 1 0 486355501 84250624 19810 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20569 19810 603 41 0 20528 0
vsize: 82276
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 20146 0 0 0 105949 67 0 0 25 0 1 0 486355501 85192704 20064 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20799 20064 603 41 0 20758 0
vsize: 83196
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 20367 0 0 0 106949 67 0 0 25 0 1 0 486355501 86147072 20285 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21032 20285 603 41 0 20991 0
vsize: 84128
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 20608 0 0 0 107949 68 0 0 25 0 1 0 486355501 87080960 20526 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21260 20526 603 41 0 21219 0
vsize: 85040
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 20824 0 0 0 108948 68 0 0 25 0 1 0 486355501 88088576 20742 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21506 20742 603 41 0 21465 0
vsize: 86024
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 21030 0 0 0 109948 69 0 0 25 0 1 0 486355501 89001984 20948 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21729 20948 603 41 0 21688 0
vsize: 86916
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 21267 0 0 0 110947 70 0 0 25 0 1 0 486355501 89985024 21185 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21969 21185 603 41 0 21928 0
vsize: 87876
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 21497 0 0 0 111947 70 0 0 25 0 1 0 486355501 90955776 21415 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22206 21415 603 41 0 22165 0
vsize: 88824
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 21749 0 0 0 112947 71 0 0 25 0 1 0 486355501 92033024 21667 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22469 21667 603 41 0 22428 0
vsize: 89876
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 21969 0 0 0 113946 71 0 0 25 0 1 0 486355501 92835840 21887 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22665 21887 603 41 0 22624 0
vsize: 90660
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 22046 0 0 0 114946 72 0 0 25 0 1 0 486355501 93233152 21964 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22762 21964 603 41 0 22721 0
vsize: 91048
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 22046 0 0 0 115946 72 0 0 25 0 1 0 486355501 93233152 21964 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22762 21964 603 41 0 22721 0
vsize: 91048
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 22046 0 0 0 116946 72 0 0 25 0 1 0 486355501 93233152 21964 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22762 21964 603 41 0 22721 0
vsize: 91048
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 22046 0 0 0 117947 72 0 0 25 0 1 0 486355501 93233152 21964 4294967295 134512640 134672761 3221224544 3221223616 134553544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22762 21964 603 41 0 22721 0
vsize: 91048
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 22046 0 0 0 118947 72 0 0 25 0 1 0 486355501 93233152 21964 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22762 21964 603 41 0 22721 0
vsize: 91048
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28519
Raw data (stat): 28517 (minisat+) R 28516 25285 25284 0 -1 0 22046 0 0 0 119947 72 0 0 25 0 1 0 486355501 93233152 21964 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22762 21964 603 41 0 22721 0
vsize: 91048
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 28519
Raw data (stat): 28517 (minisat+) Z 28516 25285 25284 0 -1 12 22049 0 0 0 119948 76 0 0 25 0 1 0 486355501 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.11
CPU time (s): 1200.25
CPU user time (s): 1199.48
CPU system time (s): 0.763883
CPU usage (%): 100.011
Max. virtual memory (Kb): 91048
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####