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-ran12x12.opb
MD5SUM	eac61d4d68844395596b0518195dd6df
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	493056
Optimality of the best value was proved	NO
Number of terms in the objective function	3024
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	839045346
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	839045346
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	41.1977
Number of variables	3024
Total number of constraints	168
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	168
Minimum length of a constraint	21
Maximum length of a constraint	240
Trace number 17664

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        385864 kB
Buffers:         32972 kB
Cached:         585328 kB
SwapCached:         24 kB
Active:         172796 kB
Inactive:       448180 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        385612 kB
SwapTotal:     2097892 kB
SwapFree:      2097660 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            22052 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:32:00 (client local time) WITH STATUS 10 IN 1200.27 SECONDS
stats: 19263 7 1200.27 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 192 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 190]---> Adder-cost: 244   maxlim: 29300   bits: 15/15
c ---[ 188]---> Adder-cost: 220   maxlim: 11124   bits: 14/14
c ---[ 186]---> Adder-cost: 244   maxlim: 29812   bits: 15/15
c ---[ 184]---> Adder-cost: 236   maxlim: 18164   bits: 15/15
c ---[ 182]---> Adder-cost: 244   maxlim: 29812   bits: 15/15
c ---[ 180]---> Adder-cost: 244   maxlim: 28916   bits: 15/15
c ---[ 178]---> Adder-cost: 220   maxlim: 11252   bits: 14/14
c ---[ 176]---> Adder-cost: 244   maxlim: 29556   bits: 15/15
c ---[ 174]---> Adder-cost: 236   maxlim: 18420   bits: 15/15
c ---[ 172]---> Adder-cost: 244   maxlim: 30196   bits: 15/15
c ---[ 170]---> Adder-cost: 244   maxlim: 29172   bits: 15/15
c ---[ 168]---> Adder-cost: 244   maxlim: 30068   bits: 15/15
c ---[ 166]---> Adder-cost: 220   maxlim: 11380   bits: 14/14
c ---[ 164]---> Adder-cost: 220   maxlim: 11508   bits: 14/14
c ---[ 162]---> Adder-cost: 256   maxlim: 36468   bits: 16/16
c ---[ 160]---> Adder-cost: 256   maxlim: 35700   bits: 16/16
c ---[ 158]---> Adder-cost: 256   maxlim: 36724   bits: 16/16
c ---[ 156]---> Adder-cost: 220   maxlim: 11508   bits: 14/14
c ---[ 154]---> Adder-cost: 256   maxlim: 34804   bits: 16/16
c ---[ 152]---> Adder-cost: 256   maxlim: 36340   bits: 16/16
c ---[ 150]---> Adder-cost: 240   maxlim: 21108   bits: 15/15
c ---[ 148]---> Adder-cost: 198   maxlim: 5748   bits: 13/13
c ---[ 146]---> Adder-cost: 256   maxlim: 33268   bits: 16/16
c ---[ 144]---> Adder-cost: 240   maxlim: 21236   bits: 15/15
c ---[ 143]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 142]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 141]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 140]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[ 139]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 138]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 137]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 136]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[ 135]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 134]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 133]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[ 132]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 131]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 130]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 129]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 128]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 127]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 126]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 125]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 124]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 123]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 122]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 121]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 120]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 119]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 118]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 117]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 116]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 115]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 114]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 113]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 112]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 111]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 110]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 109]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 108]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 107]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 106]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 105]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 104]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 103]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 102]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 101]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 100]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  99]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  98]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  97]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  96]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  95]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  94]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  93]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  92]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  91]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  90]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  89]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  88]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  87]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  86]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  85]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  84]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  83]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  82]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  81]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  80]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  79]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  78]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  77]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  76]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  75]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  74]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  73]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  72]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  71]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  70]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  69]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  68]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  67]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  66]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  65]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  64]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  63]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  62]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  61]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  60]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  59]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  58]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  57]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  56]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  55]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  54]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  53]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  52]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  51]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  50]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  49]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  48]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  47]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  46]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  45]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  44]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  43]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  42]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  41]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  40]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  39]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  38]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  37]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  36]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  35]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  34]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  33]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  32]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  31]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  30]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  29]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  28]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  27]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  26]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  25]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  24]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  23]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  22]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  21]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  20]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  19]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  18]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  17]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  16]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  15]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  14]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  13]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  12]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  11]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  10]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[   9]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   8]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[   7]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[   6]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[   5]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[   4]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[   3]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   2]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[   1]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   0]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   43430   159842 |   14476       0        0     nan |  0.000 % |
c |       100 |   43430   159842 |   15923     100      281     2.8 | 31.433 % |
c |       250 |   43403   159747 |   17515     248     1673     6.7 | 31.476 % |
c |       475 |   43362   159606 |   19267     466     2687     5.8 | 31.537 % |
c |       812 |   43257   159253 |   21194     789     4243     5.4 | 31.693 % |
c |      1318 |   43233   159175 |   23313    1291     7335     5.7 | 31.728 % |
c |      2077 |   43076   158632 |   25645    2025    11216     5.5 | 31.962 % |
c |      3216 |   42926   158112 |   28209    3145    17180     5.5 | 32.188 % |
c |      4924 |   42647   157169 |   31030    4811    25503     5.3 | 32.622 % |
c |      7486 |   42312   156022 |   34133    7323    37879     5.2 | 33.142 % |
c |     11330 |   41990   154944 |   37547   11122    57869     5.2 | 33.654 % |
c |     17096 |   41820   154388 |   41301   16862    95722     5.7 | 33.932 % |
c |     25746 |   41567   153527 |   45431   25475   172943     6.8 | 34.331 % |
c ==============================================================================
c [1mFound solution: 2379500[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 6078   maxlim: 1725430   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36546 |   84025   305255 |   28008   36274   326650     9.0 | 34.331 % |
c |     36646 |   84025   305255 |   30808   18237   168665     9.2 | 22.543 % |
c |     36796 |   84025   305255 |   33889   18387   169556     9.2 | 22.543 % |
c |     37021 |   84025   305255 |   37278   18612   170865     9.2 | 22.543 % |
c |     37359 |   84025   305255 |   41006   18950   181454     9.6 | 22.543 % |
c |     37865 |   84025   305255 |   45107   19456   185616     9.5 | 22.543 % |
c |     38624 |   84025   305255 |   49617   20215   193305     9.6 | 22.543 % |
c |     39763 |   84007   305197 |   54579   21350   202696     9.5 | 22.566 % |
c |     41471 |   84007   305197 |   60037   23058   223588     9.7 | 22.566 % |
c |     44033 |   83984   305122 |   66041   25614   253836     9.9 | 22.589 % |
c |     47877 |   83925   304931 |   72645   29448   297848    10.1 | 22.657 % |
c |     53644 |   83925   304931 |   79910   35215   423285    12.0 | 22.657 % |
c ==============================================================================
c [1mFound solution: 2240974[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1863956   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     59232 |   83943   305080 |   27981   40803   501936    12.3 | 22.657 % |
c |     59334 |   83943   305080 |   30779   20504   222794    10.9 | 22.689 % |
c |     59484 |   83943   305080 |   33857   20654   224057    10.8 | 22.689 % |
c |     59709 |   83943   305080 |   37242   20879   225718    10.8 | 22.689 % |
c |     60047 |   83943   305080 |   40966   21217   228802    10.8 | 22.689 % |
c |     60553 |   83943   305080 |   45063   21723   232710    10.7 | 22.689 % |
c |     61312 |   83943   305080 |   49570   22482   249384    11.1 | 22.689 % |
c |     62451 |   83943   305080 |   54527   23621   257889    10.9 | 22.689 % |
c |     64159 |   83943   305080 |   59979   25329   272223    10.7 | 22.689 % |
c |     66722 |   83943   305080 |   65977   27892   305644    11.0 | 22.689 % |
c |     70566 |   83927   305028 |   72575   31734   378232    11.9 | 22.706 % |
c |     76332 |   83927   305028 |   79833   37500   447508    11.9 | 22.706 % |
c ==============================================================================
c [1mFound solution: 2240210[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1864720   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     81415 |   83933   305091 |   27977   42583   825934    19.4 | 22.706 % |
c |     81515 |   83933   305091 |   30774   21392   486616    22.7 | 22.718 % |
c |     81665 |   83933   305091 |   33852   21542   487420    22.6 | 22.718 % |
c |     81892 |   83933   305091 |   37237   21769   488776    22.5 | 22.718 % |
c |     82230 |   83933   305091 |   40961   22107   490742    22.2 | 22.718 % |
c |     82736 |   83933   305091 |   45057   22613   494579    21.9 | 22.718 % |
c |     83495 |   83933   305091 |   49562   23372   499894    21.4 | 22.718 % |
c |     84634 |   83933   305091 |   54519   24511   508712    20.8 | 22.718 % |
c |     86342 |   83933   305091 |   59971   26219   526115    20.1 | 22.718 % |
c |     88904 |   83933   305091 |   65968   28781   575501    20.0 | 22.718 % |
c ==============================================================================
c [1mFound solution: 2004139[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2100791   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     91304 |   83916   304831 |   27972   31181   601832    19.3 | 22.718 % |
c |     91404 |   83916   304831 |   30769   31281   602494    19.3 | 22.750 % |
c |     91554 |   83916   304831 |   33846   31431   603742    19.2 | 22.750 % |
c |     91779 |   83916   304831 |   37230   31656   606695    19.2 | 22.750 % |
c |     92116 |   83916   304831 |   40953   31993   609392    19.0 | 22.750 % |
c |     92623 |   83916   304831 |   45049   32500   614559    18.9 | 22.750 % |
c |     93382 |   83916   304831 |   49554   33259   627566    18.9 | 22.750 % |
c |     94521 |   83916   304831 |   54509   34398   638955    18.6 | 22.750 % |
c |     96229 |   83916   304831 |   59960   36106   663747    18.4 | 22.750 % |
c |     98792 |   83916   304831 |   65956   38669   702675    18.2 | 22.750 % |
c ==============================================================================
c [1mFound solution: 1761488[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2343442   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    100936 |   83932   304955 |   27977   40813   754595    18.5 | 22.750 % |
c |    101036 |   83932   304955 |   30774   20507   189633     9.2 | 22.783 % |
c |    101186 |   83932   304955 |   33852   20657   190287     9.2 | 22.783 % |
c |    101411 |   83932   304955 |   37237   20882   191640     9.2 | 22.783 % |
c |    101748 |   83932   304955 |   40961   21219   195941     9.2 | 22.783 % |
c |    102254 |   83932   304955 |   45057   21725   200351     9.2 | 22.783 % |
c |    103014 |   83932   304955 |   49562   22485   208684     9.3 | 22.783 % |
c |    104153 |   83932   304955 |   54519   23624   221608     9.4 | 22.783 % |
c |    105861 |   83932   304955 |   59971   25332   292602    11.6 | 22.783 % |
c |    108424 |   83932   304955 |   65968   27895   316031    11.3 | 22.783 % |
c |    112268 |   83932   304955 |   72565   31739   363331    11.4 | 22.783 % |
c |    118034 |   83932   304955 |   79821   37505  1456529    38.8 | 22.783 % |
c |    126683 |   83923   304924 |   87803   46149  1650186    35.8 | 22.788 % |
c ==============================================================================
c [1mFound solution: 1527485[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2577445   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    137249 |   83936   305035 |   27978   56715  2401326    42.3 | 22.788 % |
c |    137349 |   83936   305035 |   30775   23572   838320    35.6 | 22.823 % |
c |    137499 |   83936   305035 |   33853   23722   839182    35.4 | 22.823 % |
c |    137724 |   83936   305035 |   37238   23947   841283    35.1 | 22.823 % |
c |    138061 |   83936   305035 |   40962   24284   843090    34.7 | 22.823 % |
c |    138567 |   83936   305035 |   45058   24790   846284    34.1 | 22.823 % |
c |    139326 |   83936   305035 |   49564   25549   856749    33.5 | 22.823 % |
c |    140465 |   83936   305035 |   54521   26688   871523    32.7 | 22.823 % |
c |    142173 |   83936   305035 |   59973   28396   904933    31.9 | 22.823 % |
c |    144735 |   83936   305035 |   65970   30958   925705    29.9 | 22.823 % |
c |    148579 |   83936   305035 |   72567   34802   980426    28.2 | 22.823 % |
c |    154345 |   83936   305035 |   79824   40568  1183726    29.2 | 22.823 % |
c |    162995 |   83936   305035 |   87806   49218  1453136    29.5 | 22.823 % |
c |    175970 |   83936   305035 |   96587   62193  2333857    37.5 | 22.823 % |
c ==============================================================================
c [1mFound solution: 958543[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3146387   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    191363 |   83900   304748 |   27966   76562  2884565    37.7 | 22.823 % |
c |    191463 |   83900   304748 |   30762   23975   551805    23.0 | 22.863 % |
c |    191613 |   83900   304748 |   33838   24125   552470    22.9 | 22.863 % |
c |    191838 |   83900   304748 |   37222   24350   553590    22.7 | 22.863 % |
c |    192175 |   83900   304748 |   40945   24687   555126    22.5 | 22.863 % |
c |    192681 |   83900   304748 |   45039   25193   558252    22.2 | 22.863 % |
c |    193441 |   83900   304748 |   49543   25953   563940    21.7 | 22.863 % |
c |    194580 |   83900   304748 |   54497   27092   573580    21.2 | 22.863 % |
c |    196289 |   83900   304748 |   59947   28801   584566    20.3 | 22.863 % |
c |    198851 |   83900   304748 |   65942   31363   607349    19.4 | 22.863 % |
c |    202696 |   83900   304748 |   72536   35208   710514    20.2 | 22.863 % |
c |    208464 |   83900   304748 |   79790   40976  1267837    30.9 | 22.863 % |
c |    217113 |   83900   304748 |   87769   49625  1615933    32.6 | 22.863 % |
c |    230088 |   83900   304748 |   96546   62600  2007662    32.1 | 22.863 % |
c |    249549 |   83900   304748 |  106200   82061  3241228    39.5 | 22.863 % |
c |    278741 |   83900   304748 |  116820  111253  5846271    52.5 | 22.863 % |
c |    322530 |   83900   304748 |  128503   55525  3998937    72.0 | 22.863 % |
c |    388216 |   83900   304748 |  141353  121211 11076765    91.4 | 22.863 % |
c |    486745 |   83900   304748 |  155488   91007 18974494   208.5 | 22.863 % |
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 -X#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.79 0.92 0.92 2/54 1503
Raw data (stat): 1503 (runsolver) R 1502 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544620491 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.82 0.93 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 1504 0 0 0 995 3 0 0 25 0 1 0 544620491 8159232 1470 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1992 1470 603 41 0 1951 0
vsize: 7968
[startup+20.0011 s]
Raw data (loadavg): 0.85 0.93 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 1683 0 0 0 1994 3 0 0 25 0 1 0 544620491 8876032 1649 4294967295 134512640 134672761 3221224544 3221223696 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2167 1649 603 41 0 2126 0
vsize: 8668
[startup+30.0014 s]
Raw data (loadavg): 0.87 0.93 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 1983 0 0 0 2993 4 0 0 25 0 1 0 544620491 10092544 1949 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2464 1949 603 41 0 2423 0
vsize: 9856
[startup+40.0096 s]
Raw data (loadavg): 0.89 0.93 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 2830 0 0 0 3992 6 0 0 25 0 1 0 544620491 14176256 2750 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3461 2750 603 41 0 3420 0
vsize: 13844
[startup+50.0162 s]
Raw data (loadavg): 0.90 0.93 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 2944 0 0 0 4992 6 0 0 25 0 1 0 544620491 14577664 2864 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3559 2864 603 41 0 3518 0
vsize: 14236
[startup+60.0174 s]
Raw data (loadavg): 0.92 0.93 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 3190 0 0 0 5992 7 0 0 25 0 1 0 544620491 15593472 3110 4294967295 134512640 134672761 3221224544 3221223008 134565768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3807 3110 603 41 0 3766 0
vsize: 15228
[startup+70.0182 s]
Raw data (loadavg): 0.93 0.94 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 3190 0 0 0 6991 7 0 0 25 0 1 0 544620491 15593472 3110 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3807 3110 603 41 0 3766 0
vsize: 15228
[startup+80.0189 s]
Raw data (loadavg): 0.94 0.94 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 3190 0 0 0 7990 8 0 0 25 0 1 0 544620491 15593472 3110 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3807 3110 603 41 0 3766 0
vsize: 15228
[startup+90.0194 s]
Raw data (loadavg): 0.95 0.94 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 3574 0 0 0 8988 9 0 0 25 0 1 0 544620491 17113088 3494 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4178 3494 603 41 0 4137 0
vsize: 16712
[startup+100.019 s]
Raw data (loadavg): 0.96 0.94 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 3575 0 0 0 9988 9 0 0 25 0 1 0 544620491 17113088 3495 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4178 3495 603 41 0 4137 0
vsize: 16712
[startup+110.02 s]
Raw data (loadavg): 0.96 0.94 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 3575 0 0 0 10988 10 0 0 25 0 1 0 544620491 17113088 3495 4294967295 134512640 134672761 3221224544 3221223696 134565048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4178 3495 603 41 0 4137 0
vsize: 16712
[startup+120.02 s]
Raw data (loadavg): 0.97 0.94 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 3575 0 0 0 11988 10 0 0 25 0 1 0 544620491 17108992 3495 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4177 3495 603 41 0 4136 0
vsize: 16708
[startup+130.02 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 3846 0 0 0 12988 11 0 0 25 0 1 0 544620491 18325504 3766 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4474 3766 603 41 0 4433 0
vsize: 17896
[startup+140.021 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 4364 0 0 0 13987 12 0 0 25 0 1 0 544620491 20353024 4284 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4969 4284 603 41 0 4928 0
vsize: 19876
[startup+150.022 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 5024 0 0 0 14985 14 0 0 25 0 1 0 544620491 23048192 4944 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5627 4944 603 41 0 5586 0
vsize: 22508
[startup+160.022 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 5315 0 0 0 15984 15 0 0 25 0 1 0 544620491 24178688 5235 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5903 5235 603 41 0 5862 0
vsize: 23612
[startup+170.022 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 5315 0 0 0 16984 15 0 0 25 0 1 0 544620491 24178688 5235 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5903 5235 603 41 0 5862 0
vsize: 23612
[startup+180.022 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 5315 0 0 0 17984 15 0 0 25 0 1 0 544620491 24178688 5235 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5903 5235 603 41 0 5862 0
vsize: 23612
[startup+190.022 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 5315 0 0 0 18984 15 0 0 25 0 1 0 544620491 24178688 5235 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5903 5235 603 41 0 5862 0
vsize: 23612
[startup+200.022 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 5570 0 0 0 19984 16 0 0 25 0 1 0 544620491 25522176 5490 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6231 5490 603 41 0 6190 0
vsize: 24924
[startup+210.023 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 6081 0 0 0 20982 18 0 0 25 0 1 0 544620491 27496448 6001 4294967295 134512640 134672761 3221224544 3221223876 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6713 6001 603 41 0 6672 0
vsize: 26852
[startup+220.024 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 6081 0 0 0 21983 18 0 0 25 0 1 0 544620491 27496448 6001 4294967295 134512640 134672761 3221224544 3221223744 134557962 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6713 6001 603 41 0 6672 0
vsize: 26852
[startup+230.023 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 6081 0 0 0 22983 18 0 0 25 0 1 0 544620491 27496448 6001 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6713 6001 603 41 0 6672 0
vsize: 26852
[startup+240.024 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 6081 0 0 0 23983 18 0 0 25 0 1 0 544620491 27496448 6001 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6713 6001 603 41 0 6672 0
vsize: 26852
[startup+250.024 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 6081 0 0 0 24983 18 0 0 25 0 1 0 544620491 27496448 6001 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6713 6001 603 41 0 6672 0
vsize: 26852
[startup+260.024 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 6081 0 0 0 25983 18 0 0 25 0 1 0 544620491 27496448 6001 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6713 6001 603 41 0 6672 0
vsize: 26852
[startup+270.024 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 6088 0 0 0 26983 18 0 0 25 0 1 0 544620491 27631616 6008 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6746 6008 603 41 0 6705 0
vsize: 26984
[startup+280.024 s]
Raw data (loadavg): 1.07 0.98 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 6667 0 0 0 27982 20 0 0 25 0 1 0 544620491 29921280 6587 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7305 6587 603 41 0 7264 0
vsize: 29220
[startup+290.025 s]
Raw data (loadavg): 1.06 0.98 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 7260 0 0 0 28980 22 0 0 25 0 1 0 544620491 32346112 7180 4294967295 134512640 134672761 3221224544 3221223648 134560477 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7897 7180 603 41 0 7856 0
vsize: 31588
[startup+300.024 s]
Raw data (loadavg): 1.05 0.98 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 7711 0 0 0 29978 23 0 0 25 0 1 0 544620491 34099200 7631 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8325 7631 603 41 0 8284 0
vsize: 33300
[startup+310.025 s]
Raw data (loadavg): 1.12 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 8705 0 0 0 30975 27 0 0 25 0 1 0 544620491 38129664 8625 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9309 8625 603 41 0 9268 0
vsize: 37236
[startup+320.025 s]
Raw data (loadavg): 1.10 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 9539 0 0 0 31974 28 0 0 25 0 1 0 544620491 41635840 9459 4294967295 134512640 134672761 3221224544 3221223728 134559417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10165 9459 603 41 0 10124 0
vsize: 40660
[startup+330.024 s]
Raw data (loadavg): 1.08 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 9855 0 0 0 32973 29 0 0 25 0 1 0 544620491 42852352 9775 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10462 9775 603 41 0 10421 0
vsize: 41848
[startup+340.025 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 10030 0 0 0 33973 30 0 0 25 0 1 0 544620491 43528192 9950 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10627 9950 603 41 0 10586 0
vsize: 42508
[startup+350.025 s]
Raw data (loadavg): 1.06 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 10030 0 0 0 34973 30 0 0 25 0 1 0 544620491 43528192 9950 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10627 9950 603 41 0 10586 0
vsize: 42508
[startup+360.026 s]
Raw data (loadavg): 1.05 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 10030 0 0 0 35973 30 0 0 25 0 1 0 544620491 43528192 9950 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10627 9950 603 41 0 10586 0
vsize: 42508
[startup+370.025 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 10030 0 0 0 36973 30 0 0 25 0 1 0 544620491 43528192 9950 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10627 9950 603 41 0 10586 0
vsize: 42508
[startup+380.025 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 10030 0 0 0 37973 30 0 0 25 0 1 0 544620491 43528192 9950 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10627 9950 603 41 0 10586 0
vsize: 42508
[startup+390.026 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 10030 0 0 0 38973 30 0 0 25 0 1 0 544620491 43528192 9950 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10627 9950 603 41 0 10586 0
vsize: 42508
[startup+400.026 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 10030 0 0 0 39974 30 0 0 25 0 1 0 544620491 43528192 9950 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10627 9950 603 41 0 10586 0
vsize: 42508
[startup+410.027 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 10030 0 0 0 40974 30 0 0 25 0 1 0 544620491 43528192 9950 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10627 9950 603 41 0 10586 0
vsize: 42508
[startup+420.027 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 10030 0 0 0 41974 30 0 0 25 0 1 0 544620491 43528192 9950 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10627 9950 603 41 0 10586 0
vsize: 42508
[startup+430.027 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 10030 0 0 0 42974 30 0 0 25 0 1 0 544620491 43528192 9950 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10627 9950 603 41 0 10586 0
vsize: 42508
[startup+440.027 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 10228 0 0 0 43974 30 0 0 25 0 1 0 544620491 44331008 10148 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10823 10148 603 41 0 10782 0
vsize: 43292
[startup+450.027 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 10945 0 0 0 44973 32 0 0 25 0 1 0 544620491 47276032 10865 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11542 10865 603 41 0 11501 0
vsize: 46168
[startup+460.027 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 11594 0 0 0 45971 33 0 0 25 0 1 0 544620491 49954816 11514 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12196 11514 603 41 0 12155 0
vsize: 48784
[startup+470.028 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 12304 0 0 0 46970 36 0 0 25 0 1 0 544620491 52908032 12224 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12917 12224 603 41 0 12876 0
vsize: 51668
[startup+480.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 12916 0 0 0 47967 38 0 0 25 0 1 0 544620491 55328768 12836 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13508 12836 603 41 0 13467 0
vsize: 54032
[startup+490.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 13443 0 0 0 48966 39 0 0 25 0 1 0 544620491 57479168 13363 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14033 13363 603 41 0 13992 0
vsize: 56132
[startup+500.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 14063 0 0 0 49964 41 0 0 25 0 1 0 544620491 60022784 13983 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14654 13983 603 41 0 14613 0
vsize: 58616
[startup+510.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 14659 0 0 0 50963 43 0 0 25 0 1 0 544620491 62447616 14579 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15246 14579 603 41 0 15205 0
vsize: 60984
[startup+520.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 15063 0 0 0 51962 44 0 0 25 0 1 0 544620491 64192512 14983 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15672 14983 603 41 0 15631 0
vsize: 62688
[startup+530.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 15651 0 0 0 52960 46 0 0 25 0 1 0 544620491 67002368 15571 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16358 15571 603 41 0 16317 0
vsize: 65432
[startup+540.034 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 16362 0 0 0 53959 47 0 0 25 0 1 0 544620491 69963776 16282 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17081 16282 603 41 0 17040 0
vsize: 68324
[startup+550.034 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 16921 0 0 0 54957 49 0 0 25 0 1 0 544620491 72241152 16841 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17637 16841 603 41 0 17596 0
vsize: 70548
[startup+560.035 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 16921 0 0 0 55958 49 0 0 25 0 1 0 544620491 72241152 16841 4294967295 134512640 134672761 3221224544 3221223728 134559376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17637 16841 603 41 0 17596 0
vsize: 70548
[startup+570.036 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 16921 0 0 0 56958 49 0 0 25 0 1 0 544620491 72241152 16841 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17637 16841 603 41 0 17596 0
vsize: 70548
[startup+580.035 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 16921 0 0 0 57958 49 0 0 25 0 1 0 544620491 72241152 16841 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17637 16841 603 41 0 17596 0
vsize: 70548
[startup+590.036 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 16921 0 0 0 58958 49 0 0 25 0 1 0 544620491 72241152 16841 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17637 16841 603 41 0 17596 0
vsize: 70548
[startup+600.036 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 16921 0 0 0 59958 49 0 0 25 0 1 0 544620491 72241152 16841 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17637 16841 603 41 0 17596 0
vsize: 70548
[startup+610.036 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 16921 0 0 0 60959 49 0 0 25 0 1 0 544620491 72241152 16841 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17637 16841 603 41 0 17596 0
vsize: 70548
[startup+620.036 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 16921 0 0 0 61959 49 0 0 25 0 1 0 544620491 72241152 16841 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17637 16841 603 41 0 17596 0
vsize: 70548
[startup+630.036 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 16921 0 0 0 62959 49 0 0 25 0 1 0 544620491 72241152 16841 4294967295 134512640 134672761 3221224544 3221223728 134559367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17637 16841 603 41 0 17596 0
vsize: 70548
[startup+640.037 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 16921 0 0 0 63959 49 0 0 25 0 1 0 544620491 72241152 16841 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17637 16841 603 41 0 17596 0
vsize: 70548
[startup+650.036 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 16921 0 0 0 64959 49 0 0 25 0 1 0 544620491 72241152 16841 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17637 16841 603 41 0 17596 0
vsize: 70548
[startup+660.041 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 16921 0 0 0 65960 49 0 0 25 0 1 0 544620491 72241152 16841 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17637 16841 603 41 0 17596 0
vsize: 70548
[startup+670.042 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 16921 0 0 0 66960 49 0 0 25 0 1 0 544620491 72241152 16841 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17637 16841 603 41 0 17596 0
vsize: 70548
[startup+680.041 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 17398 0 0 0 67959 51 0 0 25 0 1 0 544620491 74141696 17318 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18101 17318 603 41 0 18060 0
vsize: 72404
[startup+690.041 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 17922 0 0 0 68957 53 0 0 25 0 1 0 544620491 76296192 17842 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18627 17842 603 41 0 18586 0
vsize: 74508
[startup+700.042 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 18542 0 0 0 69955 55 0 0 25 0 1 0 544620491 78876672 18462 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19257 18462 603 41 0 19216 0
vsize: 77028
[startup+710.042 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 19223 0 0 0 70954 57 0 0 25 0 1 0 544620491 81711104 19143 4294967295 134512640 134672761 3221224544 3221223728 134559332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19949 19143 603 41 0 19908 0
vsize: 79796
[startup+720.042 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 19865 0 0 0 71952 58 0 0 25 0 1 0 544620491 84254720 19785 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20570 19785 603 41 0 20529 0
vsize: 82280
[startup+730.042 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 20415 0 0 0 72952 59 0 0 25 0 1 0 544620491 86532096 20335 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21126 20335 603 41 0 21085 0
vsize: 84504
[startup+740.042 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 20956 0 0 0 73950 61 0 0 25 0 1 0 544620491 88817664 20876 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21684 20876 603 41 0 21643 0
vsize: 86736
[startup+750.043 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 21540 0 0 0 74948 63 0 0 25 0 1 0 544620491 91230208 21460 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22273 21460 603 41 0 22232 0
vsize: 89092
[startup+760.043 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 22028 0 0 0 75947 64 0 0 25 0 1 0 544620491 93274112 21948 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22772 21948 603 41 0 22731 0
vsize: 91088
[startup+770.044 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 22414 0 0 0 76946 66 0 0 25 0 1 0 544620491 94756864 22334 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23134 22334 603 41 0 23093 0
vsize: 92536
[startup+780.044 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 22866 0 0 0 77945 67 0 0 25 0 1 0 544620491 96641024 22786 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23594 22786 603 41 0 23553 0
vsize: 94376
[startup+790.044 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 23362 0 0 0 78943 69 0 0 25 0 1 0 544620491 98668544 23282 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24089 23282 603 41 0 24048 0
vsize: 96356
[startup+800.045 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 23654 0 0 0 79943 69 0 0 25 0 1 0 544620491 99897344 23574 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24389 23574 603 41 0 24348 0
vsize: 97556
[startup+810.046 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 24179 0 0 0 80941 71 0 0 25 0 1 0 544620491 102084608 24099 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24923 24099 603 41 0 24882 0
vsize: 99692
[startup+820.046 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 24641 0 0 0 81940 72 0 0 25 0 1 0 544620491 104140800 24561 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25425 24561 603 41 0 25384 0
vsize: 101700
[startup+830.046 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 24993 0 0 0 82939 73 0 0 25 0 1 0 544620491 105492480 24913 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25755 24913 603 41 0 25714 0
vsize: 103020
[startup+840.047 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 25286 0 0 0 83939 74 0 0 25 0 1 0 544620491 106708992 25206 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26052 25206 603 41 0 26011 0
vsize: 104208
[startup+850.047 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 26081 0 0 0 84937 76 0 0 25 0 1 0 544620491 109936640 26001 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26840 26001 603 41 0 26799 0
vsize: 107360
[startup+860.047 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 26985 0 0 0 85935 78 0 0 25 0 1 0 544620491 113700864 26905 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27759 26905 603 41 0 27718 0
vsize: 111036
[startup+870.047 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 27846 0 0 0 86933 80 0 0 25 0 1 0 544620491 117182464 27766 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28609 27766 603 41 0 28568 0
vsize: 114436
[startup+880.048 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 28677 0 0 0 87931 82 0 0 25 0 1 0 544620491 120655872 28597 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29457 28597 603 41 0 29416 0
vsize: 117828
[startup+890.048 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 29344 0 0 0 88929 85 0 0 25 0 1 0 544620491 123355136 29264 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30116 29264 603 41 0 30075 0
vsize: 120464
[startup+900.048 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 30064 0 0 0 89927 87 0 0 25 0 1 0 544620491 126300160 29984 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30835 29984 603 41 0 30794 0
vsize: 123340
[startup+910.049 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 30731 0 0 0 90926 88 0 0 25 0 1 0 544620491 128966656 30651 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31486 30651 603 41 0 31445 0
vsize: 125944
[startup+920.048 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 31387 0 0 0 91924 90 0 0 25 0 1 0 544620491 131657728 31307 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32143 31307 603 41 0 32102 0
vsize: 128572
[startup+930.048 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32079 0 0 0 92922 92 0 0 25 0 1 0 544620491 134459392 31999 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32827 31999 603 41 0 32786 0
vsize: 131308
[startup+940.049 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32309 0 0 0 93922 93 0 0 25 0 1 0 544620491 135405568 32229 4294967295 134512640 134672761 3221224544 3221223648 134560260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32229 603 41 0 33017 0
vsize: 132232
[startup+950.049 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32309 0 0 0 94922 93 0 0 25 0 1 0 544620491 135405568 32229 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32229 603 41 0 33017 0
vsize: 132232
[startup+960.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32310 0 0 0 95922 93 0 0 25 0 1 0 544620491 135405568 32230 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32230 603 41 0 33017 0
vsize: 132232
[startup+970.051 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32310 0 0 0 96923 93 0 0 25 0 1 0 544620491 135405568 32230 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32230 603 41 0 33017 0
vsize: 132232
[startup+980.051 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32310 0 0 0 97923 93 0 0 25 0 1 0 544620491 135405568 32230 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32230 603 41 0 33017 0
vsize: 132232
[startup+990.051 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32310 0 0 0 98923 93 0 0 25 0 1 0 544620491 135405568 32230 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32230 603 41 0 33017 0
vsize: 132232
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32310 0 0 0 99923 93 0 0 25 0 1 0 544620491 135405568 32230 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32230 603 41 0 33017 0
vsize: 132232
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32310 0 0 0 100923 93 0 0 25 0 1 0 544620491 135405568 32230 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32230 603 41 0 33017 0
vsize: 132232
[startup+1020.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32311 0 0 0 101924 93 0 0 25 0 1 0 544620491 135405568 32231 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32231 603 41 0 33017 0
vsize: 132232
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32311 0 0 0 102924 93 0 0 25 0 1 0 544620491 135405568 32231 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32231 603 41 0 33017 0
vsize: 132232
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32312 0 0 0 103924 93 0 0 25 0 1 0 544620491 135405568 32232 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32232 603 41 0 33017 0
vsize: 132232
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32312 0 0 0 104924 93 0 0 25 0 1 0 544620491 135405568 32232 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32232 603 41 0 33017 0
vsize: 132232
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32312 0 0 0 105924 93 0 0 25 0 1 0 544620491 135405568 32232 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32232 603 41 0 33017 0
vsize: 132232
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32312 0 0 0 106924 93 0 0 25 0 1 0 544620491 135405568 32232 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32232 603 41 0 33017 0
vsize: 132232
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32312 0 0 0 107925 93 0 0 25 0 1 0 544620491 135405568 32232 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32232 603 41 0 33017 0
vsize: 132232
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32312 0 0 0 108925 93 0 0 25 0 1 0 544620491 135405568 32232 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32232 603 41 0 33017 0
vsize: 132232
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32312 0 0 0 109925 93 0 0 25 0 1 0 544620491 135405568 32232 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32232 603 41 0 33017 0
vsize: 132232
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32312 0 0 0 110925 93 0 0 25 0 1 0 544620491 135405568 32232 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32232 603 41 0 33017 0
vsize: 132232
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32312 0 0 0 111925 93 0 0 25 0 1 0 544620491 135405568 32232 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32232 603 41 0 33017 0
vsize: 132232
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32312 0 0 0 112926 93 0 0 25 0 1 0 544620491 135405568 32232 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32232 603 41 0 33017 0
vsize: 132232
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32312 0 0 0 113926 93 0 0 25 0 1 0 544620491 135405568 32232 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32232 603 41 0 33017 0
vsize: 132232
[startup+1150.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32312 0 0 0 114926 93 0 0 25 0 1 0 544620491 135405568 32232 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32232 603 41 0 33017 0
vsize: 132232
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32312 0 0 0 115926 93 0 0 25 0 1 0 544620491 135405568 32232 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32232 603 41 0 33017 0
vsize: 132232
[startup+1170.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32312 0 0 0 116926 93 0 0 25 0 1 0 544620491 135405568 32232 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32232 603 41 0 33017 0
vsize: 132232
[startup+1180.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32312 0 0 0 117927 93 0 0 25 0 1 0 544620491 135405568 32232 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32232 603 41 0 33017 0
vsize: 132232
[startup+1190.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32312 0 0 0 118927 93 0 0 25 0 1 0 544620491 135405568 32232 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32232 603 41 0 33017 0
vsize: 132232
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 1503
Raw data (stat): 1503 (minisat+) R 1502 26298 26297 0 -1 0 32312 0 0 0 119927 93 0 0 25 0 1 0 544620491 135405568 32232 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33058 32232 603 41 0 33017 0
vsize: 132232
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.00 0.99 0.93 1/54 1503
Raw data (stat): 1503 (minisat+) Z 1502 26298 26297 0 -1 12 32315 0 0 0 119928 99 0 0 25 0 1 0 544620491 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.13
CPU time (s): 1200.27
CPU user time (s): 1199.28
CPU system time (s): 0.992849
CPU usage (%): 100.012
Max. virtual memory (Kb): 132232
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####