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 17660

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-21 11:11:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19266 boxname=wulflinc7 idbench=1482 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  eac61d4d68844395596b0518195dd6df  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-ran12x12.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-ran12x12.opb /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-ran12x12.opb
IDLAUNCH: 19266
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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	: 2
cpu MHz		: 451.050
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:        686776 kB
Buffers:         12280 kB
Cached:         313572 kB
SwapCached:          4 kB
Active:         157152 kB
Inactive:       171604 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        686524 kB
SwapTotal:     2097136 kB
SwapFree:      2097128 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            13544 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:31:35 (client local time) WITH STATUS 10 IN 1200.27 SECONDS
stats: 19266 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]---> BDD-cost:   13
c ---[ 142]---> BDD-cost:   12
c ---[ 141]---> BDD-cost:   17
c ---[ 140]---> BDD-cost:   14
c ---[ 139]---> BDD-cost:   15
c ---[ 138]---> BDD-cost:   15
c ---[ 137]---> BDD-cost:   11
c ---[ 136]---> BDD-cost:   14
c ---[ 135]---> BDD-cost:   14
c ---[ 134]---> BDD-cost:   17
c ---[ 133]---> BDD-cost:   14
c ---[ 132]---> BDD-cost:   13
c ---[ 131]---> BDD-cost:   12
c ---[ 130]---> BDD-cost:   17
c ---[ 129]---> BDD-cost:   17
c ---[ 128]---> BDD-cost:   12
c ---[ 127]---> BDD-cost:   17
c ---[ 126]---> BDD-cost:   17
c ---[ 125]---> BDD-cost:   15
c ---[ 124]---> BDD-cost:   11
c ---[ 123]---> BDD-cost:   17
c ---[ 122]---> BDD-cost:   14
c ---[ 121]---> BDD-cost:   17
c ---[ 120]---> BDD-cost:   17
c ---[ 119]---> BDD-cost:   13
c ---[ 118]---> BDD-cost:   13
c ---[ 117]---> BDD-cost:   12
c ---[ 116]---> BDD-cost:   17
c ---[ 115]---> BDD-cost:   12
c ---[ 114]---> BDD-cost:   17
c ---[ 113]---> BDD-cost:   17
c ---[ 112]---> BDD-cost:   15
c ---[ 111]---> BDD-cost:   11
c ---[ 110]---> BDD-cost:   17
c ---[ 109]---> BDD-cost:   14
c ---[ 108]---> BDD-cost:   13
c ---[ 107]---> BDD-cost:   17
c ---[ 106]---> BDD-cost:   17
c ---[ 105]---> BDD-cost:   13
c ---[ 104]---> BDD-cost:   12
c ---[ 103]---> BDD-cost:   14
c ---[ 102]---> BDD-cost:   12
c ---[ 101]---> BDD-cost:   14
c ---[ 100]---> BDD-cost:   14
c ---[  99]---> BDD-cost:   15
c ---[  98]---> BDD-cost:   11
c ---[  97]---> BDD-cost:   13
c ---[  96]---> BDD-cost:   14
c ---[  95]---> BDD-cost:   14
c ---[  94]---> BDD-cost:   14
c ---[  93]---> BDD-cost:   14
c ---[  92]---> BDD-cost:   13
c ---[  91]---> BDD-cost:   13
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:   13
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   17
c ---[  86]---> BDD-cost:   13
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   13
c ---[  83]---> BDD-cost:   13
c ---[  82]---> BDD-cost:   13
c ---[  81]---> BDD-cost:   12
c ---[  80]---> BDD-cost:   17
c ---[  79]---> BDD-cost:   12
c ---[  78]---> BDD-cost:   17
c ---[  77]---> BDD-cost:   17
c ---[  76]---> BDD-cost:   12
c ---[  75]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   11
c ---[  73]---> BDD-cost:   17
c ---[  72]---> BDD-cost:   14
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   17
c ---[  69]---> BDD-cost:   13
c ---[  68]---> BDD-cost:   12
c ---[  67]---> BDD-cost:   17
c ---[  66]---> BDD-cost:   12
c ---[  65]---> BDD-cost:   17
c ---[  64]---> BDD-cost:   16
c ---[  63]---> BDD-cost:   15
c ---[  62]---> BDD-cost:   15
c ---[  61]---> BDD-cost:   11
c ---[  60]---> BDD-cost:   16
c ---[  59]---> BDD-cost:   14
c ---[  58]---> BDD-cost:   17
c ---[  57]---> BDD-cost:   17
c ---[  56]---> BDD-cost:   11
c ---[  55]---> BDD-cost:   11
c ---[  54]---> BDD-cost:   15
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   11
c ---[  49]---> BDD-cost:   11
c ---[  48]---> BDD-cost:   11
c ---[  47]---> BDD-cost:   11
c ---[  46]---> BDD-cost:   11
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:   15
c ---[  42]---> BDD-cost:   13
c ---[  41]---> BDD-cost:   12
c ---[  40]---> BDD-cost:   17
c ---[  39]---> BDD-cost:   12
c ---[  38]---> BDD-cost:   17
c ---[  37]---> BDD-cost:   15
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:   17
c ---[  33]---> BDD-cost:   14
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:   17
c ---[  30]---> BDD-cost:   17
c ---[  29]---> BDD-cost:   13
c ---[  28]---> BDD-cost:   12
c ---[  27]---> BDD-cost:   13
c ---[  26]---> BDD-cost:   12
c ---[  25]---> BDD-cost:   13
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   15
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:   17
c ---[  20]---> BDD-cost:   13
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   13
c ---[  16]---> BDD-cost:   13
c ---[  15]---> BDD-cost:   12
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   12
c ---[  12]---> BDD-cost:   13
c ---[  11]---> BDD-cost:   13
c ---[  10]---> BDD-cost:   14
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   11
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   14
c ---[   5]---> BDD-cost:   13
c ---[   4]---> BDD-cost:   13
c ---[   3]---> BDD-cost:   13
c ---[   2]---> BDD-cost:   12
c ---[   1]---> BDD-cost:   17
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   41409   144003 |   13803       0        0     nan |  0.000 % |
c |       100 |   41258   143478 |   15183      81      262     3.2 | 22.772 % |
c |       250 |   41169   143173 |   16701     219      715     3.3 | 22.925 % |
c |       475 |   41062   142808 |   18371     432     1441     3.3 | 23.118 % |
c |       812 |   40973   142507 |   20208     756     2472     3.3 | 23.271 % |
c |      1318 |   40766   141794 |   22229    1232     3996     3.2 | 23.638 % |
c |      2079 |   40625   141303 |   24452    1973     7147     3.6 | 23.852 % |
c |      3218 |   40416   140592 |   26898    3087    13307     4.3 | 24.239 % |
c |      4926 |   40346   140358 |   29587    4787    26119     5.5 | 24.361 % |
c |      7488 |   40259   140065 |   32546    7338    52630     7.2 | 24.534 % |
c |     11332 |   40126   139600 |   35801   11169    85450     7.7 | 24.758 % |
c |     17098 |   39925   138945 |   39381   16906   147794     8.7 | 25.165 % |
c ==============================================================================
c [1mFound solution: 2361773[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 6078   maxlim: 1743157   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23701 |   82294   290334 |   27431   23491   218858     9.3 | 25.165 % |
c |     23801 |   82294   290334 |   30174   23591   219764     9.3 | 15.735 % |
c |     23951 |   82294   290334 |   33191   23741   222076     9.4 | 15.735 % |
c |     24176 |   82294   290334 |   36510   23966   223996     9.3 | 15.735 % |
c |     24513 |   82276   290276 |   40161   24301   226216     9.3 | 15.760 % |
c |     25019 |   82257   290211 |   44177   24805   231303     9.3 | 15.786 % |
c ==============================================================================
c [1mFound solution: 2298228[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1806702   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25678 |   82269   290370 |   27423   25463   237862     9.3 | 15.786 % |
c |     25779 |   82269   290370 |   30165   25564   238540     9.3 | 15.848 % |
c |     25929 |   82269   290370 |   33181   25714   239976     9.3 | 15.848 % |
c |     26154 |   82234   290253 |   36500   25935   241955     9.3 | 15.892 % |
c |     26491 |   82207   290166 |   40150   26269   245037     9.3 | 15.930 % |
c |     26998 |   82189   290104 |   44165   26774   251161     9.4 | 15.948 % |
c |     27757 |   82189   290104 |   48581   27533   264024     9.6 | 15.948 % |
c |     28896 |   82173   290052 |   53439   28669   277010     9.7 | 15.967 % |
c |     30605 |   82132   289919 |   58783   30372   297059     9.8 | 16.018 % |
c |     33168 |   82075   289724 |   64661   32929   335056    10.2 | 16.080 % |
c ==============================================================================
c [1mFound solution: 2252052[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1852878   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34443 |   82088   289880 |   27362   34201   345706    10.1 | 16.080 % |
c |     34543 |   82088   289880 |   30098   17201   147077     8.6 | 16.143 % |
c |     34693 |   82088   289880 |   33108   17351   148039     8.5 | 16.143 % |
c |     34918 |   82088   289880 |   36418   17576   150098     8.5 | 16.143 % |
c |     35255 |   82088   289880 |   40060   17913   152719     8.5 | 16.143 % |
c |     35761 |   82088   289880 |   44066   18419   158383     8.6 | 16.143 % |
c |     36520 |   82088   289880 |   48473   19178   168830     8.8 | 16.143 % |
c |     37659 |   82088   289880 |   53320   20317   179402     8.8 | 16.143 % |
c |     39367 |   82088   289880 |   58652   22025   199598     9.1 | 16.143 % |
c |     41929 |   82031   289695 |   64518   24576   219678     8.9 | 16.212 % |
c |     45773 |   82022   289666 |   70969   28418   288209    10.1 | 16.224 % |
c ==============================================================================
c [1mFound solution: 2189349[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1915581   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46242 |   82039   289848 |   27346   28887   294372    10.2 | 16.224 % |
c |     46342 |   82039   289848 |   30080   28987   295258    10.2 | 16.280 % |
c |     46492 |   82039   289848 |   33088   29137   296899    10.2 | 16.280 % |
c |     46717 |   82039   289848 |   36397   29362   305206    10.4 | 16.280 % |
c |     47054 |   82039   289848 |   40037   29699   316104    10.6 | 16.280 % |
c |     47560 |   82023   289796 |   44041   30202   324080    10.7 | 16.299 % |
c |     48319 |   82023   289796 |   48445   30961   332742    10.7 | 16.299 % |
c |     49458 |   82023   289796 |   53289   32100   356442    11.1 | 16.299 % |
c |     51167 |   82023   289796 |   58618   33809   462259    13.7 | 16.299 % |
c |     53729 |   82014   289767 |   64480   36369   491014    13.5 | 16.311 % |
c |     57573 |   82014   289767 |   70928   40213   795894    19.8 | 16.311 % |
c |     63339 |   82014   289767 |   78021   45979   878936    19.1 | 16.311 % |
c ==============================================================================
c [1mFound solution: 2022281[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2082649   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     64663 |   82036   289939 |   27345   47303   947958    20.0 | 16.311 % |
c |     64763 |   82036   289939 |   30079   20625   491517    23.8 | 16.366 % |
c |     64913 |   82036   289939 |   33087   20775   492411    23.7 | 16.366 % |
c |     65138 |   82036   289939 |   36396   21000   493680    23.5 | 16.366 % |
c |     65475 |   82036   289939 |   40035   21337   497123    23.3 | 16.366 % |
c |     65981 |   82036   289939 |   44039   21843   501871    23.0 | 16.366 % |
c |     66740 |   82036   289939 |   48443   22602   509179    22.5 | 16.366 % |
c |     67879 |   82029   289916 |   53287   23740   519162    21.9 | 16.372 % |
c |     69587 |   82029   289916 |   58616   25448   548840    21.6 | 16.372 % |
c |     72150 |   82029   289916 |   64478   28011   583313    20.8 | 16.372 % |
c |     75994 |   82013   289864 |   70925   31851   689900    21.7 | 16.391 % |
c |     81760 |   82009   289854 |   78018   37616  1054856    28.0 | 16.397 % |
c ==============================================================================
c [1mFound solution: 1868284[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2236646   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87307 |   81970   289230 |   27323   43156  1156005    26.8 | 16.397 % |
c |     87407 |   81970   289230 |   30055   19934   493342    24.7 | 16.442 % |
c |     87557 |   81961   289201 |   33060   20083   494164    24.6 | 16.455 % |
c |     87782 |   81961   289201 |   36366   20308   495476    24.4 | 16.455 % |
c |     88119 |   81961   289201 |   40003   20645   497996    24.1 | 16.455 % |
c |     88625 |   81961   289201 |   44003   21151   501593    23.7 | 16.455 % |
c |     89385 |   81961   289201 |   48404   21911   508375    23.2 | 16.455 % |
c |     90524 |   81961   289201 |   53244   23050   528137    22.9 | 16.455 % |
c |     92232 |   81961   289201 |   58569   24758   550439    22.2 | 16.455 % |
c |     94795 |   81961   289201 |   64426   27321   841407    30.8 | 16.455 % |
c |     98639 |   81961   289201 |   70868   31165   886466    28.4 | 16.455 % |
c |    104408 |   81961   289201 |   77955   36934  1064773    28.8 | 16.455 % |
c |    113057 |   81961   289201 |   85751   45583  1689826    37.1 | 16.455 % |
c |    126031 |   81952   289170 |   94326   58554  2335962    39.9 | 16.461 % |
c ==============================================================================
c [1mFound solution: 1457042[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2647888   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    131072 |   81992   289346 |   27330   63595  2614659    41.1 | 16.461 % |
c |    131172 |   81992   289346 |   30063   23007   600105    26.1 | 16.502 % |
c |    131322 |   81992   289346 |   33069   23157   600914    25.9 | 16.502 % |
c |    131547 |   81992   289346 |   36376   23382   602279    25.8 | 16.502 % |
c |    131884 |   81992   289346 |   40013   23719   605997    25.5 | 16.502 % |
c |    132390 |   81992   289346 |   44015   24225   610269    25.2 | 16.502 % |
c |    133150 |   81992   289346 |   48416   24985   615807    24.6 | 16.502 % |
c |    134290 |   81992   289346 |   53258   26125   645442    24.7 | 16.502 % |
c |    135998 |   81992   289346 |   58584   27833   660553    23.7 | 16.502 % |
c |    138560 |   81976   289294 |   64442   30392   685001    22.5 | 16.521 % |
c |    142405 |   81976   289294 |   70886   34237   735576    21.5 | 16.521 % |
c |    148173 |   81972   289284 |   77975   40004   842964    21.1 | 16.527 % |
c |    156822 |   81963   289262 |   85773   48651  1461365    30.0 | 16.539 % |
c ==============================================================================
c [1mFound solution: 1231976[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2872954   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    163315 |   82004   289491 |   27334   55144  1595073    28.9 | 16.539 % |
c |    163415 |   82004   289491 |   30067   22873   626587    27.4 | 16.599 % |
c |    163566 |   82004   289491 |   33074   23024   627336    27.2 | 16.599 % |
c |    163792 |   82004   289491 |   36381   23250   628572    27.0 | 16.599 % |
c |    164129 |   82004   289491 |   40019   23587   630843    26.7 | 16.599 % |
c |    164635 |   82004   289491 |   44021   24093   634892    26.4 | 16.599 % |
c |    165396 |   82004   289491 |   48423   24854   640338    25.8 | 16.599 % |
c |    166535 |   82004   289491 |   53266   25993   658039    25.3 | 16.599 % |
c |    168243 |   82000   289481 |   58592   27700   672924    24.3 | 16.605 % |
c |    170806 |   81991   289450 |   64452   30258   726892    24.0 | 16.611 % |
c |    174650 |   81987   289440 |   70897   34101   782047    22.9 | 16.618 % |
c |    180417 |   81987   289440 |   77987   39868  1112826    27.9 | 16.618 % |
c |    189066 |   81987   289440 |   85785   48517  1476051    30.4 | 16.618 % |
c |    202040 |   81987   289440 |   94364   61491  2234604    36.3 | 16.618 % |
c |    221502 |   81983   289430 |  103800   80952  4074918    50.3 | 16.624 % |
c |    250694 |   81983   289430 |  114180  110144  6839592    62.1 | 16.624 % |
c |    294484 |   81983   289430 |  125598   47000  2444787    52.0 | 16.624 % |
c |    360168 |   81979   289420 |  138158  112683  5660728    50.2 | 16.630 % |
c |    458694 |   81970   289398 |  151974   85889  3710606    43.2 | 16.643 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 X4_bit_7 -X4_bit_6 X4_bit_5 -X4_bit_4 X4_bit_3 -X4_bit_2 -X4_bit_1 X4_bit0 X4_bit1 -X4_bit2 X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 X5_bit_7 X5_bit_6 -X5_bit_5 X5_bit_4 X5_bit_3 X5_bit_2 X5_bit_1 X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 X8_bit_7 X8_bit_6 X8_bit_5 -X8_bit_4 -X8_bit_3 X8_bit_2 X8_bit_1 X8_bit0 -X8_bit1 -X8_bit2 X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 X10_bit_7 -X10_bit_6 -X10_bit_5 X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 -X12_bit_6 -X12_bit_5 -X12_bit_4 -X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X15_bit_7 -X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 -X15_bit_2 -X15_bit_1 -X15_bit0 -X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 -X17_bit_6 -X17_bit_5 -X17_bit_4 -X17_bit_3 -X17_bit_2 -X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 X19_bit_7 X19_bit_6 -X19_bit_5 X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 X20_bit_7 X20_bit_6 -X20_bit_5 -X20_bit_4 -X20_bit_3 -X20_bit_2 X20_bit_1 X20_bit0 X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X21_bit_7 X21_bit_6 X21_bit_5 -X21_bit_4 -X21_bit_3 -X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X23_bit_7 -X23_bit_6 X23_bit_5 X23_bit_4 -X23_bit_3 X23_bit_2 -X23_bit_1 X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X24_bit_7 -X24_bit_6 -X24_bit_5 -X24_bit_4 -X24_bit_3 -X24_bit_2 -X24_bit_1 -X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 X25_bit_7 -X25_bit_6 -X25_bit_5 -X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 -X26_bit_5 -X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X27_bit_7 -X27_bit_6 -X27_bit_5 -X27_bit_4 -X27_bit_3 -X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 X28_bit0 X28_bit1 X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 -X29_bit_7 -X29_bit_6 -X29_bit_5 -X29_bit_4 -X29_bit_3 -X29_bit_2 X29_bit_1 X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 X32_bit_6 -X32_bit_5 -X32_bit_4 X32_bit_3 -X32_bit_2 -X32_bit_1 -X32_bit0 -X32_bit1 X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X33_bit_7 -X33_bit_6 -X33_bit_5 -X33_bit_4 -X33_bit_3 -X33_bit_2 -X33_bit_1 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X34_bit_7 -X34_bit_6 -X34_bit_5 -X34_bit_4 -X34_bit_3 -X34_bit_2 -X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 -X35_bit_6 X35_bit_5 X35_bit_4 -X35_bit_3 X35_bit_2 -X35_bit_1 X35_bit0 -X35_bit1 X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 X36_bit_7 -X36_bit_6 X36_bit_5 X36_bit_4 X36_bit_3 X36_bit_2 X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 -X37_bit_7 -X37_bit_6 -X37_bit_5 -X37_bit_4 -X37_bit_3 -X37_bit_2 -X37_bit_1 -X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X38_bit_7 -X38_bit_6 -X38_bit_5 -X38_bit_4 -X38_bit_3 -X38_bit_2 -X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X39_bit_7 X39_bit_6 X39_bit_5 -X39_bit_4 X39_bit_3 -X39_bit_2 -X39_bit_1 X39_bit0 X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 X40_bit_7 X40_bit_6 X40_bit_5 X40_bit_4 -X40_bit_3 -X40_bit_2 -X40_bit_1 X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 X41_bit_7 X41_bit_6 X41_bit_5 X41_bit_4 X41_bit_3 X41_bit_2 -X41_bit_1 -X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X42_bit_7 X42_bit_6 X42_bit_5 X42_bit_4 -X42_bit_3 -X42_bit_2 X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 X43_bit_7 X43_bit_6 -X43_bit_5 X43_bit_4 -X43_bit_3 -X43_bit_2 -X43_bit_1 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 X44_bit_7 X44_bit_6 X44_bit_5 -X44_bit_4 -X44_bit_3 -X44_bit_2 X44_bit_1 X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X45_bit_7 -X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 X46_bit_7 X46_bit_6 X46_bit_5 X46_bit_4 X46_bit_3 X46_bit_2 X46_bit_1 X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 -X47_bit_7 -X47_bit_6 -X47_bit_5 -X47_bit_4 -X47_bit_3 -X47_bit_2 -X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 X48_bit_7 -X48_bit_6 -X48_bit_5 -X48_bit_4 -X48_bit_3 X48_bit_2 X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 -X49_bit_6 -X49_bit_5 -X49_bit_4 -X49_bit_3 -X49_bit_2 -X49_bit_1 -X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 -X50_bit_7 -X50_bit_6 -X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 X51_bit_7 -X51_bit_6 X51_bit_5 -X51_bit_4 X51_bit_3 -X51_bit_2 -X51_bit_1 -X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 X52_bit_7 -X52_bit_6 -X52_bit_5 -X52_bit_4 -X52_bit_3 -X52_bit_2 -X52_bit_1 -X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 X53_bit_7 X53_bit_6 -X53_bit_5 X53_bit_4 -X53_bit_3 -X53_bit_2 -X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 -X54_bit_6 -X54_bit_5 -X54_bit_4 -X54_bit_3 -X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 -X55_bit_6 -X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 -X56_bit_7 -X56_bit_6 -X56_bit_5 -X56_bit_4 -X56_bit_3 -X56_bit_2 -X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 -X57_bit_6 -X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 X58_bit_7 X58_bit_6 X58_bit_5 X58_bit_4 X58_bit_3 X58_bit_2 X58_bit_1 -X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 X59_bit_7 X59_bit_6 X59_bit_5 X59_bit_4 X59_bit_3 X59_bit_2 X59_bit_1 X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X60_bit_7 -X60_bit_6 -X60_bit_5 -X60_bit_4 -X60_bit_3 -X60_bit_2 -X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X61_bit_7 -X61_bit_6 -X61_bit_5 -X61_bit_4 -X61_bit_3 -X61_bit_2 -X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 X62_bit_7 -X62_bit_6 X62_bit_5 X62_bit_4 X62_bit_3 X62_bit_2 X62_bit_1 X62_bit0 X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 -X63_bit_7 -X63_bit_6 -X63_bit_5 -X63_bit_4 X63_bit_3 -X63_bit_2 X63_bit_1 -X63_bit0 X63_bit1 -X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 -X64_bit_7 -X64_bit_6 -X64_bit_5 -X64_bit_4 -X64_bit_3 -X64_bit_2 -X64_bit_1 -X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 X65_bit_7 X65_bit_6 -X65_bit_5 X65_bit_4 X65_bit_3 X65_bit_2 -X65_bit_1 -X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 -X66_bit_7 X66_bit_6 X66_bit_5 X66_bit_4 -X66_bit_3 -X66_bit_2 X66_bit_1 -X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 -X67_bit_7 -X67_bit_6 -X67_bit_5 -X67_bit_4 -X67_bit_3 -X67_bit_2 -X67_bit_1 -X67_bit0 -X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 X68_bit_7 -X68_bit_6 X68_bit_5 -X68_bit_4 X68_bit_3 -X68_bit_2 X68_bit_1 X68_bit0 X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 -X69_bit_7 -X69_bit_6 -X69_bit_5 -X69_bit_4 -X69_bit_3 -X69_bit_2 -X69_bit_1 -X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 X70_bit_7 -X70_bit_6 X70_bit_5 -X70_bit_4 X70_bit_3 -X70_bit_2 X70_bit_1 X70_bit0 -X70_bit1 -X70_bit2 X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X71_bit_7 -X71_bit_6 -X71_bit_5 -X71_bit_4 -X71_bit_3 -X71_bit_2 -X71_bit_1 -X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X72_bit_7 -X72_bit_6 -X72_bit_5 -X72_bit_4 -X72_bit_3 -X72_bit_2 -X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 -X73_bit_6 -X73_bit_5 -X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 X74_bit_7 X74_bit_6 X74_bit_5 -X74_bit_4 X74_bit_3 X74_bit_2 X74_bit_1 -X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 -X75_bit_7 -X75_bit_6 -X75_bit_5 -X75_bit_4 -X75_bit_3 -X75_bit_2 -X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X76_bit_7 -X76_bit_6 -X76_bit_5 -X76_bit_4 -X76_bit_3 -X76_bit_2 -X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 X77_bit_7 -X77_bit_6 -X77_bit_5 -X77_bit_4 -X77_bit_3 X77_bit_2 X77_bit_1 X77_bit0 X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 X78_bit_7 X78_bit_6 -X78_bit_5 X78_bit_4 -X78_bit_3 -X78_bit_2 X78_bit_1 X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X79_bit_7 -X79_bit_6 -X79_bit_5 -X79_bit_4 -X79_bit_3 -X79_bit_2 -X79_bit_1 -X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X80_bit_7 -X80_bit_6 -X80_bit_5 -X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 -X81_bit_5 -X81_bit_4 -X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 X82_bit_7 X82_bit_6 X82_bit_5 X82_bit_4 -X82_bit_3 X82_bit_2 X82_bit_1 X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 X83_bit_6 X83_bit_5 X83_bit_4 -X83_bit_3 X83_bit_2 X83_bit_1 X83_bit0 X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 X84_bit_7 X84_bit_6 -X84_bit_5 -X84_bit_4 -X84_bit_3 X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 X85_bit_7 -X85_bit_6 -X85_bit_5 X85_bit_4 -X85_bit_3 -X85_bit_2 -X85_bit_1 X85_bit0 X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X86_bit_7 -X86_bit_6 -X86_bit_5 -X86_bit_4 -X86_bit_3 -X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 -X87_bit_6 -X87_bit_5 -X87_bit_4 -X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 X88_bit_7 -X88_bit_6 -X88_bit_5 -X88_bit_4 X88_bit_3 X88_bit_2 X88_bit_1 -X88_bit0 X88_bit1 X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 X89_bit_7 -X89_bit_6 -X89_bit_5 X89_bit_4 X89_bit_3 -X89_bit_2 -X89_bit_1 X89_bit0 X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X90_bit_7 X90_bit_6 X90_bit_5 X90_bit_4 -X90_bit_3 -X90_bit_2 X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 -X91_bit_7 -X91_bit_6 -X91_bit_5 -X91_bit_4 -X91_bit_3 -X91_bit_2 -X91_bit_1 -X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 X92_bit_7 -X92_bit_6 -X92_bit_5 X92_bit_4 -X92_bit_3 -X92_bit_2 -X92_bit_1 -X92_bit0 -X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 -X93_bit_7 -X93_bit_6 -X93_bit_5 -X93_bit_4 -X93_bit_3 -X93_bit_2 -X93_bit_1 -X93_bit0 -X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 X94_bit_7 X94_bit_6 -X94_bit_5 -X94_bit_4 X94_bit_3 X94_bit_2 X94_bit_1 X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 -X95_bit_7 -X95_bit_6 -X95_bit_5 -X95_bit_4 -X95_bit_3 -X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 X96_bit_7 X96_bit_6 X96_bit_5 X96_bit_4 X96_bit_3 X96_bit_2 -X96_bit_1 X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 -X97_bit_7 -X97_bit_6 -X97_bit_5 -X97_bit_4 -X97_bit_3 -X97_bit_2 -X97_bit_1 -X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 -X98_bit_7 -X98_bit_6 -X98_bit_5 -X98_bit_4 -X98_bit_3 -X98_bit_2 -X98_bit_1 -X98_bit0 -X98_bit1 -X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 -X99_bit_7 -X99_bit_6 -X99_bit_5 -X99_bit_4 -X99_bit_3 -X99_bit_2 -X99_bit_1 -X99_bit0 -X99_bit1 -X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 -X100_bit_7 -X100_bit_6 -X100_bit_5 -X100_bit_4 -X100_bit_3 -X100_bit_2 -X100_bit_1 -X100_bit0 -X100_bit1 -X100_bit2 -X100_bit3 -X100_bit4 -X100_bit5 -X100_bit6 -X100_bit7 -X100_bit8 -X100_bit9 -X100_bit10 -X100_bit11 -X100_bit12 X101_bit_7 X101_bit_6 X101_bit_5 X101_bit_4 X101_bit_3 X101_bit_2 X101_bit_1 X101_bit0 X101_bit1 -X101_bit2 -X101_bit3 -X101_bit4 -X101_bit5 -X101_bit6 -X101_bit7 -X101_bit8 -X101_bit9 -X101_bit10 -X101_bit11 -X101_bit12 X102_bit_7 X102_bit_6 X102_bit_5 X102_bit_4 -X102_bit_3 -X102_bit_2 -X102_bit_1 X102_bit0 X102_bit1 X102_bit2 -X102_bit3 -X102_bit4 -X102_bit5 -X102_bit6 -X102_bit7 -X102_bit8 -X102_bit9 -X102_bit10 -X102_bit11 -X102_bit12 X103_bit_7 X103_bit_6 X103_bit_5 -X103_bit_4 -X103_bit_3 X103_bit_2 X103_bit_1 -X103_bit0 X103_bit1 -X103_bit2 -X103_bit3 -X103_bit4 -X103_bit5 -X103_bit6 -X103_bit7 -X103_bit8 -X103_bit9 -X103_bit10 -X103_bit11 -X103_bit12 -X104_bit_7 -X104_bit_6 -X104_bit_5 -X104_bit_4 -X104_bit_3 -X104_bit_2 -X104_bit_1 -X104_bit0 -X104_bit1 -X104_bit2 -X104_bit3 -X104_bit4 -X104_bit5 -X104_bit6 -X104_bit7 -X104_bit8 -X104_bit9 -X104_bit10 -X104_bit11 -X104_bit12 -X105_bit_7 -X105_bit_6 -X105_bit_5 -X105_bit_4 -X105_bit_3 -X105_bit_2 -X105_bit_1 -X105_bit0 -X105_bit1 -X105_bit2 -X105_bit3 -X105_bit4 -X105_bit5 -X105_bit6 -X105_bit7 -X105_bit8 -X105_bit9 -X105_bit10 -X105_bit11 -X105_bit12 X106_bit_7 X106_bit_6 X106_bit_5 X106_bit_4 X106_bit_3 -X106_bit_2 X106_bit_1 -X106_bit0 -X106_bit1 -X106_bit2 -X106_bit3 -X106_bit4 -X106_bit5 -X106_bit6 -X106_bit7 -X106_bit8 -X106_bit9 -X106_bit10 -X106_bit11 -X106_bit12 X107_bit_7 -X107_bit_6 X107_bit_5 X107_bit_4 -X107_bit_3 X107_bit_2 X107_bit_1 X107_bit0 X107_bit1 X107_bit2 -X107_bit3 -X107_bit4 -X107_bit5 -X107_bit6 -X107_bit7 -X107_bit8 -X107_bit9 -X107_bit10 -X107_bit11 -X107_bit12 -X108_bit_7 X108_bit_6 X108_bit_5 X108_bit_4 X108_bit_3 -X108_bit_2 X108_bit_1 X108_bit0 -X108_bit1 -X108_bit2 -X108_bit3 -X108_bit4 -X108_bit5 -X108_bit6 -X108_bit7 -X108_bit8 -X108_bit9 -X108_bit10 -X108_bit11 -X108_bit12 -X109_bit_7 -X109_bit_6 -X109_bit_5 -X109_bit_4 -X109_bit_3 -X109_bit_2 -X109_bit_1 -X109_bit0 -X109_bit1 -X109_bit2 -X109_bit3 -X109_bit4 -X109_bit5 -X109_bit6 -X109_bit7 -X109_bit8 -X109_bit9 -X109_bit10 -X109_bit11 -X109_bit12 -X110_bit_7 -X110_bit_6 -X110_bit_5 -X110_bit_4 -X110_bit_3 -X110_bit_2 -X110_bit_1 -X110_bit0 -X110_bit1 -X110_bit2 -X110_bit3 -X110_bit4 -X110_bit5 -X110_bit6 -X110_bit7 -X110_bit8 -X110_bit9 -X110_bit10 -X110_bit11 -X110_bit12 -X111_bit_7 -X111_bit_6 -X111_bit_5 -X111_bit_4 -X111_bit_3 -X111_bit_2 -X111_bit_1 -X111_bit0 -X111_bit1 -X111_bit2 -X111_bit3 -X111_bit4 -X111_bit5 -X111_bit6 -X111_bit7 -X111_bit8 -X111_bit9 -X111_bit10 -X111_bit11 -X111_bit12 X112_bit_7 X112_bit_6 X112_bit_5 X112_bit_4 X112_bit_3 -X112_bit_2 -X112_bit_1 -X112_bit0 X112_bit1 -X112_bit2 -X112_bit3 -X112_bit4 -X112_bit5 -X112_bit6 -X112_bit7 -X112_bit8 -X112_bit9 -X112_bit10 -X112_bit11 -X112_bit12 X113_bit_7 X113_bit_6 X113_bit_5 X113_bit_4 X113_bit_3 -X113_bit_2 -X113_bit_1 -X113_bit0 X113_bit1 -X113_bit2 -X113_bit3 -X113_bit4 -X113_bit5 -X113_bit6 -X113_bit7 -X113_bit8 -X113_bit9 -X113_bit10 -X113_bit11 -X113_bit12 X114_bit_7 X114_bit_6 X114_bit_5 X114_bit_4 X114_bit_3 -X114_bit_2 -X114_bit_1 -X114_bit0 -X114_bit1 -X114_bit2 -X114_bit3 -X114_bit4 -X114_bit5 -X114_bit6 -X114_bit7 -X114_bit8 -X114_bit9 -X114_bit10 -X114_bit11 -X114_bit12 -X115_bit_7 -X115_bit_6 -X115_bit_5 -X115_bit_4 -X115_bit_3 -X115_bit_2 -X115_bit_1 -X115_bit0 -X115_bit1 -X115_bit2 -X115_bit3 -X115_bit4 -X115_bit5 -X115_bit6 -X115_bit7 -X115_bit8 -X115_bit9 -X115_bit10 -X115_bit11 -X115_bit12 X116_bit_7 X116_bit_6 X116_bit_5 X116_bit_4 X116_bit_3 -X116_bit_2 -X116_bit_1 X116_bit0 -X116_bit1 X116_bit2 -X116_bit3 -X116_bit4 -X116_bit5 -X116_bit6 -X116_bit7 -X116_bit8 -X116_bit9 -X116_bit10 -X116_bit11 -X116_bit12 X117_bit_7 X117_bit_6 X117_bit_5 X117_bit_4 X117_bit_3 -X117_bit_2 X117_bit_1 -X117_bit0 -X117_bit1 -X117_bit2 -X117_bit3 -X117_bit4 -X117_bit5 -X117_bit6 -X117_bit7 -X117_bit8 -X117_bit9 -X117_bit10 -X117_bit11 -X117_bit12 -X118_bit_7 -X118_bit_6 -X118_bit_5 -X118_bit_4 -X118_bit_3 -X118_bit_2 -X118_bit_1 -X118_bit0 -X118_bit1 -X118_bit2 -X118_bit3 -X118_bit4 -X118_bit5 -X118_bit6 -X118_bit7 -X118_bit8 -X118_bit9 -X118_bit10 -X118_bit11 -X118_bit12 X119_bit_7 X119_bit_6 X119_bit_5 -X119_bit_4 -X119_bit_3 -X119_bit_2 X119_bit_1 -X119_bit0 -X119_bit1 X119_bit2 -X119_bit3 -X119_bit4 -X119_bit5 -X119_bit6 -X119_bit7 -X119_bit8 -X119_bit9 -X119_bit10 -X119_bit11 -X119_bit12 -X120_bit_7 X120_bit_6 X120_bit_5 -X120_bit_4 -X120_bit_3 -X120_bit_2 -X120_bit_1 -X120_bit0 -X120_bit1 -X120_bit2 -X120_bit3 -X120_bit4 -X120_bit5 -X120_bit6 -X120_bit7 -X120_bit8 -X120_bit9 -X120_bit10 -X120_bit11 -X120_bit12 X121_bit_7 X121_bit_6 X121_bit_5 X121_bit_4 X121_bit_3 X121_bit_2 -X121_bit_1 -X121_bit0 -X121_bit1 -X121_bit2 -X121_bit3 -X121_bit4 -X121_bit5 -X121_bit6 -X121_bit7 -X121_bit8 -X121_bit9 -X121_bit10 -X121_bit11 -X121_bit12 -X122_bit_7 -X122_bit_6 X122_bit_5 X122_bit_4 -X122_bit_3 -X122_bit_2 -X122_bit_1 -X122_bit0 -X122_bit1 X122_bit2 X122_bit3 -X122_bit4 -X122_bit5 -X122_bit6 -X122_bit7 -X122_bit8 -X122_bit9 -X122_bit10 -X122_bit11 -X122_bit12 X123_bit_7 -X123_bit_6 X123_bit_5 -X123_bit_4 -X123_bit_3 -X123_bit_2 -X123_bit_1 -X123_bit0 -X123_bit1 -X123_bit2 -X123_bit3 -X123_bit4 -X123_bit5 -X123_bit6 -X123_bit7 -X123_bit8 -X123_bit9 -X123_bit10 -X123_bit11 -X123_bit12 X124_bit_7 -X124_bit_6 X124_bit_5 X124_bit_4 -X124_bit_3 -X124_bit_2 X124_bit_1 -X124_bit0 -X124_bit1 -X124_bit2 -X124_bit3 -X124_bit4 -X124_bit5 -X124_bit6 -X124_bit7 -X124_bit8 -X124_bit9 -X124_bit10 -X124_bit11 -X124_bit12 X125_bit_7 -X125_bit_6 -X125_bit_5 X125_bit_4 -X125_bit_3 -X125_bit_2 -X125_bit_1 -X125_bit0 -X125_bit1 -X125_bit2 -X125_bit3 -X125_bit4 -X125_bit5 -X125_bit6 -X125_bit7 -X125_bit8 -X125_bit9 -X125_bit10 -X125_bit11 -X125_bit12 -X126_bit_7 -X126_bit_6 -X126_bit_5 -X126_bit_4 -X126_bit_3 -X126_bit_2 -X126_bit_1 -X126_bit0 -X126_bit1 -X126_bit2 -X126_bit3 -X126_bit4 -X126_bit5 -X126_bit6 -X126_bit7 -X126_bit8 -X126_bit9 -X126_bit10 -X126_bit11 -X126_bit12 X127_bit_7 X127_bit_6 -X127_bit_5 -X127_bit_4 -X127_bit_3 -X127_bit_2 -X127_bit_1 -X127_bit0 -X127_bit1 -X127_bit2 -X127_bit3 -X127_bit4 -X127_bit5 -X127_bit6 -X127_bit7 -X127_bit8 -X127_bit9 -X127_bit10 -X127_bit11 -X127_bit12 -X128_bit_7 -X128_bit_6 -X128_bit_5 -X128_bit_4 -X128_bit_3 -X128_bit_2 -X128_bit_1 -X128_bit0 -X128_bit1 -X128_bit2 -X128_bit3 -X128_bit4 -X128_bit5 -X128_bit6 -X128_bit7 -X128_bit8 -X128_bit9 -X128_bit10 -X128_bit11 -X128_bit12 X129_bit_7 X129_bit_6 X129_bit_5 -X129_bit_4 -X129_bit_3 X129_bit_2 X129_bit_1 X129_bit0 X129_bit1 -X129_bit2 -X129_bit3 -X129_bit4 -X129_bit5 -X129_bit6 -X129_bit7 -X129_bit8 -X129_bit9 -X129_bit10 -X129_bit11 -X129_bit12 X130_bit_7 X130_bit_6 -X130_bit_5 -X130_bit_4 -X130_bit_3 X130_bit_2 X130_bit_1 X130_bit0 -X130_bit1 -X130_bit2 -X130_bit3 -X130_bit4 -X130_bit5 -X130_bit6 -X130_bit7 -X130_bit8 -X130_bit9 -X130_bit10 -X130_bit11 -X130_bit12 X131_bit_7 X131_bit_6 X131_bit_5 -X131_bit_4 -X131_bit_3 -X131_bit_2 -X131_bit_1 -X131_bit0 -X131_bit1 -X131_bit2 -X131_bit3 -X131_bit4 -X131_bit5 -X131_bit6 -X131_bit7 -X131_bit8 -X131_bit9 -X131_bit10 -X131_bit11 -X131_bit12 -X132_bit_7 -X132_bit_6 X132_bit_5 X132_bit_4 X132_bit_3 -X132_bit_2 X132_bit_1 X132_bit0 -X132_bit1 -X132_bit2 -X132_bit3 -X132_bit4 -X132_bit5 -X132_bit6 -X132_bit7 -X132_bit8 -X132_bit9 -X132_bit10 -X132_bit11 -X132_bit12 X133_bit_7 X133_bit_6 X133_bit_5 -X133_bit_4 X133_bit_3 X133_bit_2 -X133_bit_1 X133_bit0 -X133_bit1 -X133_bit2 -X133_bit3 -X133_bit4 -X133_bit5 -X133_bit6 -X133_bit7 -X133_bit8 -X133_bit9 -X133_bit10 -X133_bit11 -X133_bit12 -X134_bit_7 -X134_bit_6 -X134_bit_5 -X134_bit_4 -X134_bit_3 -X134_bit_2 -X134_bit_1 -X134_bit0 -X134_bit1 -X134_bit2 -X134_bit3 -X134_bit4 -X134_bit5 -X134_bit6 -X134_bit7 -X134_bit8 -X134_bit9 -X134_bit10 -X134_bit11 -X134_bit12 -X135_bit_7 -X135_bit_6 -X135_bit_5 -X135_bit_4 -X135_bit_3 -X135_bit_2 -X135_bit_1 -X135_bit0 -X135_bit1 -X135_bit2 -X135_bit#### 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.75 0.92 0.89 2/54 5505
Raw data (stat): 5505 (runsolver) R 5504 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486403270 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.79 0.93 0.90 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 1434 0 0 0 995 3 0 0 25 0 1 0 486403270 7802880 1403 4294967295 134512640 134672761 3221224544 3221223760 134558086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1905 1403 603 41 0 1864 0
vsize: 7620
[startup+20.0007 s]
Raw data (loadavg): 0.82 0.93 0.90 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 1710 0 0 0 1993 5 0 0 25 0 1 0 486403270 8847360 1679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2160 1679 603 41 0 2119 0
vsize: 8640
[startup+30.0008 s]
Raw data (loadavg): 0.85 0.93 0.90 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 5611 0 0 0 2984 13 0 0 25 0 1 0 486403270 22269952 4945 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5437 4945 603 41 0 5396 0
vsize: 21748
[startup+40.0015 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 5829 0 0 0 3984 14 0 0 25 0 1 0 486403270 23175168 5146 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5658 5146 603 41 0 5617 0
vsize: 22632
[startup+50.0016 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 5829 0 0 0 4983 14 0 0 25 0 1 0 486403270 23175168 5146 4294967295 134512640 134672761 3221224544 3221223712 134564493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5658 5146 603 41 0 5617 0
vsize: 22632
[startup+60.0076 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 5930 0 0 0 5983 15 0 0 25 0 1 0 486403270 23576576 5247 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5756 5247 603 41 0 5715 0
vsize: 23024
[startup+70.0153 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 6359 0 0 0 6982 17 0 0 25 0 1 0 486403270 25333760 5676 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6185 5676 603 41 0 6144 0
vsize: 24740
[startup+80.0155 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 6625 0 0 0 7981 18 0 0 25 0 1 0 486403270 26308608 5925 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6423 5925 603 41 0 6382 0
vsize: 25692
[startup+90.0165 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 6625 0 0 0 8981 18 0 0 25 0 1 0 486403270 26308608 5925 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6423 5925 603 41 0 6382 0
vsize: 25692
[startup+100.017 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 6894 0 0 0 9981 19 0 0 25 0 1 0 486403270 27369472 6178 4294967295 134512640 134672761 3221224544 3221220416 134523192 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6682 6178 603 41 0 6641 0
vsize: 26728
[startup+110.017 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 6903 0 0 0 10980 19 0 0 25 0 1 0 486403270 27369472 6187 4294967295 134512640 134672761 3221224544 3221223712 134560976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6682 6187 603 41 0 6641 0
vsize: 26728
[startup+120.017 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 6903 0 0 0 11980 20 0 0 25 0 1 0 486403270 27369472 6187 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6682 6187 603 41 0 6641 0
vsize: 26728
[startup+130.017 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 7580 0 0 0 12978 22 0 0 25 0 1 0 486403270 30191616 6864 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6864 603 41 0 7330 0
vsize: 29484
[startup+140.018 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 8124 0 0 0 13976 24 0 0 25 0 1 0 486403270 32346112 7408 4294967295 134512640 134672761 3221224544 3221223696 134565080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7897 7408 603 41 0 7856 0
vsize: 31588
[startup+150.018 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 8575 0 0 0 14975 25 0 0 25 0 1 0 486403270 34086912 7842 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8322 7842 603 41 0 8281 0
vsize: 33288
[startup+160.018 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 8575 0 0 0 15974 26 0 0 25 0 1 0 486403270 34086912 7842 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8322 7842 603 41 0 8281 0
vsize: 33288
[startup+170.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 8575 0 0 0 16974 26 0 0 25 0 1 0 486403270 34086912 7842 4294967295 134512640 134672761 3221224544 3221223600 134565039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8322 7842 603 41 0 8281 0
vsize: 33288
[startup+180.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 8575 0 0 0 17974 26 0 0 25 0 1 0 486403270 34086912 7842 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8322 7842 603 41 0 8281 0
vsize: 33288
[startup+190.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 8576 0 0 0 18974 27 0 0 25 0 1 0 486403270 34086912 7843 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8322 7843 603 41 0 8281 0
vsize: 33288
[startup+200.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 8576 0 0 0 19974 27 0 0 25 0 1 0 486403270 34086912 7843 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8322 7843 603 41 0 8281 0
vsize: 33288
[startup+210.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 8576 0 0 0 20974 27 0 0 25 0 1 0 486403270 34086912 7843 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8322 7843 603 41 0 8281 0
vsize: 33288
[startup+220.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 8576 0 0 0 21974 27 0 0 25 0 1 0 486403270 34086912 7843 4294967295 134512640 134672761 3221224544 3221223728 134559019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8322 7843 603 41 0 8281 0
vsize: 33288
[startup+230.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 8577 0 0 0 22974 27 0 0 25 0 1 0 486403270 34086912 7844 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8322 7844 603 41 0 8281 0
vsize: 33288
[startup+240.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 9084 0 0 0 23971 30 0 0 25 0 1 0 486403270 36503552 8351 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8912 8351 603 41 0 8871 0
vsize: 35648
[startup+250.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 10037 0 0 0 24968 33 0 0 25 0 1 0 486403270 40284160 9304 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9835 9304 603 41 0 9794 0
vsize: 39340
[startup+260.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 10647 0 0 0 25966 36 0 0 25 0 1 0 486403270 42844160 9914 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10460 9914 603 41 0 10419 0
vsize: 41840
[startup+270.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 11211 0 0 0 26964 37 0 0 25 0 1 0 486403270 45137920 10478 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11020 10478 603 41 0 10979 0
vsize: 44080
[startup+280.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 11726 0 0 0 27963 39 0 0 25 0 1 0 486403270 47161344 10993 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11514 10993 603 41 0 11473 0
vsize: 46056
[startup+290.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 12524 0 0 0 28961 41 0 0 25 0 1 0 486403270 50393088 11791 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12303 11791 603 41 0 12262 0
vsize: 49212
[startup+300.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 13333 0 0 0 29957 45 0 0 25 0 1 0 486403270 53755904 12600 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13124 12600 603 41 0 13083 0
vsize: 52496
[startup+310.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 13713 0 0 0 30955 47 0 0 25 0 1 0 486403270 55242752 12980 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13487 12980 603 41 0 13446 0
vsize: 53948
[startup+320.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14019 0 0 0 31954 48 0 0 25 0 1 0 486403270 56459264 13286 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13784 13286 603 41 0 13743 0
vsize: 55136
[startup+330.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14020 0 0 0 32954 49 0 0 25 0 1 0 486403270 56459264 13287 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13784 13287 603 41 0 13743 0
vsize: 55136
[startup+340.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14020 0 0 0 33954 49 0 0 25 0 1 0 486403270 56459264 13287 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13784 13287 603 41 0 13743 0
vsize: 55136
[startup+350.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14021 0 0 0 34954 49 0 0 25 0 1 0 486403270 56459264 13288 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13784 13288 603 41 0 13743 0
vsize: 55136
[startup+360.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14024 0 0 0 35954 49 0 0 25 0 1 0 486403270 56459264 13291 4294967295 134512640 134672761 3221224544 3221223728 134559601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13784 13291 603 41 0 13743 0
vsize: 55136
[startup+370.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14024 0 0 0 36953 49 0 0 25 0 1 0 486403270 56459264 13291 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13784 13291 603 41 0 13743 0
vsize: 55136
[startup+380.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14024 0 0 0 37953 50 0 0 25 0 1 0 486403270 56459264 13291 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13784 13291 603 41 0 13743 0
vsize: 55136
[startup+390.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14024 0 0 0 38953 50 0 0 25 0 1 0 486403270 56459264 13291 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13784 13291 603 41 0 13743 0
vsize: 55136
[startup+400.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14024 0 0 0 39953 51 0 0 25 0 1 0 486403270 56459264 13291 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13784 13291 603 41 0 13743 0
vsize: 55136
[startup+410.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14024 0 0 0 40953 51 0 0 25 0 1 0 486403270 56459264 13291 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13784 13291 603 41 0 13743 0
vsize: 55136
[startup+420.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14024 0 0 0 41952 51 0 0 25 0 1 0 486403270 56459264 13291 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13784 13291 603 41 0 13743 0
vsize: 55136
[startup+430.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14024 0 0 0 42952 51 0 0 25 0 1 0 486403270 56459264 13291 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13784 13291 603 41 0 13743 0
vsize: 55136
[startup+440.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14024 0 0 0 43952 52 0 0 25 0 1 0 486403270 56459264 13291 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13784 13291 603 41 0 13743 0
vsize: 55136
[startup+450.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14024 0 0 0 44952 52 0 0 25 0 1 0 486403270 56459264 13291 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13784 13291 603 41 0 13743 0
vsize: 55136
[startup+460.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14024 0 0 0 45952 52 0 0 25 0 1 0 486403270 56459264 13291 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13784 13291 603 41 0 13743 0
vsize: 55136
[startup+470.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14025 0 0 0 46952 52 0 0 25 0 1 0 486403270 56459264 13292 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13784 13292 603 41 0 13743 0
vsize: 55136
[startup+480.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14048 0 0 0 47951 53 0 0 25 0 1 0 486403270 56594432 13315 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13817 13315 603 41 0 13776 0
vsize: 55268
[startup+490.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14273 0 0 0 48951 54 0 0 25 0 1 0 486403270 57925632 13540 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14142 13540 603 41 0 14101 0
vsize: 56568
[startup+500.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14647 0 0 0 49950 55 0 0 25 0 1 0 486403270 59539456 13914 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14536 13914 603 41 0 14495 0
vsize: 58144
[startup+510.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14857 0 0 0 50949 56 0 0 25 0 1 0 486403270 60342272 14124 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14732 14124 603 41 0 14691 0
vsize: 58928
[startup+520.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14857 0 0 0 51949 56 0 0 25 0 1 0 486403270 60342272 14124 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14732 14124 603 41 0 14691 0
vsize: 58928
[startup+530.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14857 0 0 0 52949 56 0 0 25 0 1 0 486403270 60342272 14124 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14732 14124 603 41 0 14691 0
vsize: 58928
[startup+540.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14857 0 0 0 53949 56 0 0 25 0 1 0 486403270 60342272 14124 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14732 14124 603 41 0 14691 0
vsize: 58928
[startup+550.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14857 0 0 0 54949 56 0 0 25 0 1 0 486403270 60342272 14124 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14732 14124 603 41 0 14691 0
vsize: 58928
[startup+560.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14857 0 0 0 55949 56 0 0 25 0 1 0 486403270 60342272 14124 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14732 14124 603 41 0 14691 0
vsize: 58928
[startup+570.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14857 0 0 0 56950 56 0 0 25 0 1 0 486403270 60342272 14124 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14732 14124 603 41 0 14691 0
vsize: 58928
[startup+580.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14857 0 0 0 57950 56 0 0 25 0 1 0 486403270 60342272 14124 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14732 14124 603 41 0 14691 0
vsize: 58928
[startup+590.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14857 0 0 0 58949 56 0 0 25 0 1 0 486403270 60342272 14124 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14732 14124 603 41 0 14691 0
vsize: 58928
[startup+600.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14857 0 0 0 59949 56 0 0 25 0 1 0 486403270 60342272 14124 4294967295 134512640 134672761 3221224544 3221223712 134564490 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14732 14124 603 41 0 14691 0
vsize: 58928
[startup+610.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14857 0 0 0 60949 56 0 0 25 0 1 0 486403270 60342272 14124 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14732 14124 603 41 0 14691 0
vsize: 58928
[startup+620.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14857 0 0 0 61949 56 0 0 25 0 1 0 486403270 60342272 14124 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14732 14124 603 41 0 14691 0
vsize: 58928
[startup+630.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 14857 0 0 0 62950 56 0 0 25 0 1 0 486403270 60342272 14124 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14732 14124 603 41 0 14691 0
vsize: 58928
[startup+640.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 15459 0 0 0 63949 57 0 0 25 0 1 0 486403270 62754816 14726 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15321 14726 603 41 0 15280 0
vsize: 61284
[startup+650.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 16501 0 0 0 64947 59 0 0 25 0 1 0 486403270 67035136 15768 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16366 15768 603 41 0 16325 0
vsize: 65464
[startup+660.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 17553 0 0 0 65944 62 0 0 25 0 1 0 486403270 71348224 16820 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17419 16820 603 41 0 17378 0
vsize: 69676
[startup+670.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 18609 0 0 0 66942 65 0 0 25 0 1 0 486403270 75673600 17876 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18475 17876 603 41 0 18434 0
vsize: 73900
[startup+680.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 19765 0 0 0 67940 67 0 0 25 0 1 0 486403270 80392192 19032 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19627 19032 603 41 0 19586 0
vsize: 78508
[startup+690.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 20973 0 0 0 68937 70 0 0 25 0 1 0 486403270 85381120 20240 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20845 20240 603 41 0 20804 0
vsize: 83380
[startup+700.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 21998 0 0 0 69935 72 0 0 25 0 1 0 486403270 89563136 21265 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21866 21265 603 41 0 21825 0
vsize: 87464
[startup+710.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 22917 0 0 0 70932 75 0 0 25 0 1 0 486403270 93360128 22184 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22793 22184 603 41 0 22752 0
vsize: 91172
[startup+720.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 23961 0 0 0 71930 77 0 0 25 0 1 0 486403270 97665024 23228 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23844 23228 603 41 0 23803 0
vsize: 95376
[startup+730.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 25058 0 0 0 72928 80 0 0 25 0 1 0 486403270 102129664 24325 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24934 24325 603 41 0 24893 0
vsize: 99736
[startup+740.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 26130 0 0 0 73926 82 0 0 25 0 1 0 486403270 106536960 25397 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26010 25397 603 41 0 25969 0
vsize: 104040
[startup+750.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 27133 0 0 0 74924 84 0 0 25 0 1 0 486403270 110587904 26400 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26999 26400 603 41 0 26958 0
vsize: 107996
[startup+760.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 28004 0 0 0 75923 86 0 0 25 0 1 0 486403270 114221056 27271 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27886 27271 603 41 0 27845 0
vsize: 111544
[startup+770.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 28890 0 0 0 76921 88 0 0 25 0 1 0 486403270 117878784 28157 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28779 28157 603 41 0 28738 0
vsize: 115116
[startup+780.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 29832 0 0 0 77919 90 0 0 25 0 1 0 486403270 121667584 29099 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29704 29099 603 41 0 29663 0
vsize: 118816
[startup+790.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 30667 0 0 0 78918 91 0 0 25 0 1 0 486403270 125042688 29934 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30528 29934 603 41 0 30487 0
vsize: 122112
[startup+800.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 31553 0 0 0 79917 93 0 0 25 0 1 0 486403270 128704512 30820 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31422 30820 603 41 0 31381 0
vsize: 125688
[startup+810.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 32170 0 0 0 80915 94 0 0 25 0 1 0 486403270 131256320 31437 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32045 31437 603 41 0 32004 0
vsize: 128180
[startup+820.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 32932 0 0 0 81914 96 0 0 25 0 1 0 486403270 134348800 32199 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32800 32199 603 41 0 32759 0
vsize: 131200
[startup+830.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 33672 0 0 0 82912 98 0 0 25 0 1 0 486403270 137367552 32939 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33537 32939 603 41 0 33496 0
vsize: 134148
[startup+840.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 34443 0 0 0 83911 99 0 0 25 0 1 0 486403270 140554240 33710 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34315 33710 603 41 0 34274 0
vsize: 137260
[startup+850.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 84910 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+860.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 85910 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+870.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 86911 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+880.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 87911 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+890.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 88911 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+900.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 89911 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223648 134559771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+910.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 90911 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+920.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 91912 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+930.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 92912 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+940.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 93912 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+950.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 94912 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+960.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 95912 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+970.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 96912 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+980.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 97913 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+990.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 98913 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 99913 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 100913 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 101913 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 102914 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223728 134559611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 103914 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 104914 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 105914 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223648 134555211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 106914 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35058 0 0 0 107915 100 0 0 25 0 1 0 486403270 143089664 34325 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34934 34325 603 41 0 34893 0
vsize: 139736
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 35786 0 0 0 108913 102 0 0 25 0 1 0 486403270 145960960 35053 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35635 35053 603 41 0 35594 0
vsize: 142540
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 36604 0 0 0 109911 104 0 0 25 0 1 0 486403270 149417984 35871 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36479 35871 603 41 0 36438 0
vsize: 145916
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 37403 0 0 0 110909 106 0 0 25 0 1 0 486403270 152625152 36670 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37262 36670 603 41 0 37221 0
vsize: 149048
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 38145 0 0 0 111908 107 0 0 25 0 1 0 486403270 155684864 37412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38009 37412 603 41 0 37968 0
vsize: 152036
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 38865 0 0 0 112907 109 0 0 25 0 1 0 486403270 158621696 38132 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38726 38132 603 41 0 38685 0
vsize: 154904
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 39559 0 0 0 113906 110 0 0 25 0 1 0 486403270 161505280 38826 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39430 38826 603 41 0 39389 0
vsize: 157720
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 40259 0 0 0 114905 111 0 0 25 0 1 0 486403270 164306944 39526 4294967295 134512640 134672761 3221224544 3221223648 134560293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40114 39526 603 41 0 40073 0
vsize: 160456
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 40798 0 0 0 115903 113 0 0 25 0 1 0 486403270 166563840 40065 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40665 40065 603 41 0 40624 0
vsize: 162660
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 41269 0 0 0 116902 115 0 0 25 0 1 0 486403270 168435712 40536 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41122 40536 603 41 0 41081 0
vsize: 164488
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 41863 0 0 0 117900 116 0 0 25 0 1 0 486403270 170991616 41130 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41746 41130 603 41 0 41705 0
vsize: 166984
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 42572 0 0 0 118899 118 0 0 25 0 1 0 486403270 173817856 41839 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42436 41839 603 41 0 42395 0
vsize: 169744
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5505
Raw data (stat): 5505 (minisat+) R 5504 22932 22931 0 -1 0 43325 0 0 0 119898 120 0 0 25 0 1 0 486403270 176918528 42592 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43193 42592 603 41 0 43152 0
vsize: 172772
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 5505
Raw data (stat): 5505 (minisat+) Z 5504 22932 22931 0 -1 12 43328 0 0 0 119898 128 0 0 25 0 1 0 486403270 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): 1198.99
CPU system time (s): 1.28081
CPU usage (%): 100.012
Max. virtual memory (Kb): 172772
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####