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 17661

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        743316 kB
Buffers:          2620 kB
Cached:         265252 kB
SwapCached:        524 kB
Active:          56656 kB
Inactive:       213228 kB
HighTotal:      131008 kB
HighFree:         2800 kB
LowTotal:       903652 kB
LowFree:        740516 kB
SwapTotal:     2097892 kB
SwapFree:      2096460 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            15948 kB
Committed_AS:    63568 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:31:44 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 19264 7 1200.26 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   42175   148716 |   12652       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7353          
c   -- var.elim.:  2000/7353          
c   -- var.elim.:  3000/7353          
c   -- var.elim.:  4000/7353          
c   -- var.elim.:  5000/7353          
c   -- var.elim.:  6000/7353          
c   -- var.elim.:  7000/7353          
c   -- var.elim.:  7353/7353          
c   -- var.elim.:  1000/1656          
c   -- var.elim.:  1656/1656          
c   -- subsuming                       
c   -- var.elim.:  708/708          
c   -- var.elim.:  692/692          
c   -- subsuming                       
c |         0 |   36892   126266 |      --       0       --      -- |     --   | -3526/-12465
c |         0 |   36892   126266 |   14756       0        0     nan |  0.000 % |
c |       100 |   36892   126266 |   16232     100      318     3.2 | 27.717 % |
c |       250 |   36892   126266 |   17855     250      789     3.2 | 27.717 % |
c |       475 |   36892   126266 |   19641     475     1548     3.3 | 27.717 % |
c |       812 |   36828   126048 |   21567     811     2628     3.2 | 27.804 % |
c |      1319 |   36828   126048 |   23724    1318     4575     3.5 | 27.804 % |
c |      2078 |   36764   125830 |   26051    2075     8634     4.2 | 27.891 % |
c |      3218 |   36764   125830 |   28657    3215    15706     4.9 | 27.891 % |
c |      4926 |   36764   125830 |   31522    4923    25289     5.1 | 27.891 % |
c |      7489 |   36764   125830 |   34675    7486    43274     5.8 | 27.891 % |
c |     11333 |   36764   125830 |   38142   11330    83001     7.3 | 27.891 % |
c ==============================================================================
c (current CPU-time: 12.6721 s)
c ==============================================================================
c [1mFound solution: 2356368[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 6078   maxlim: 1748562   bits: 22/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     14241 |   79223   277522 |   23766   14238   106832     7.5 | 27.891 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7814          
c   -- var.elim.:  2000/7814          
c   -- var.elim.:  3000/7814          
c   -- var.elim.:  4000/7814          
c   -- var.elim.:  5000/7814          
c   -- var.elim.:  6000/7814          
c   -- var.elim.:  7000/7814          
c   -- var.elim.:  7814/7814          
c   -- var.elim.:  42/42          
c |     14241 |   79127   277071 |      --   14238       --      -- |     --   | -96/-439
c |     14241 |   79127   277071 |   31650   14238   106832     7.5 | 27.891 % |
c |     14341 |   79127   277071 |   34815   14338   107338     7.5 | 16.869 % |
c |     14491 |   79127   277071 |   38297   14488   108283     7.5 | 16.869 % |
c |     14716 |   79127   277071 |   42127   14713   109644     7.5 | 16.869 % |
c |     15053 |   79127   277071 |   46339   15050   116020     7.7 | 16.869 % |
c |     15559 |   79127   277071 |   50973   15556   120189     7.7 | 16.869 % |
c ==============================================================================
c (current CPU-time: 16.3785 s)
c ==============================================================================
c [1mFound solution: 2281409[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1823521   bits: 22/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     15774 |   79194   277395 |   23758   15771   123381     7.8 | 16.869 % |
c   -- subsuming                       
c   -- var.elim.:  63/63          
c   -- var.elim.:  21/21          
c |     15774 |   79182   277364 |      --   15771       --      -- |     --   | -12/-23
c |     15774 |   79182   277364 |   31672   15771   123381     7.8 | 16.869 % |
c |     15874 |   79182   277364 |   34840   15871   124138     7.8 | 16.903 % |
c |     16025 |   79182   277364 |   38324   16022   125372     7.8 | 16.903 % |
c |     16250 |   79182   277364 |   42156   16247   127845     7.9 | 16.903 % |
c |     16587 |   79182   277364 |   46372   16584   130456     7.9 | 16.903 % |
c |     17093 |   79170   277316 |   51001   17087   135114     7.9 | 16.910 % |
c |     17852 |   79170   277316 |   56101   17846   144021     8.1 | 16.910 % |
c |     18992 |   79170   277316 |   61711   18986   172226     9.1 | 16.910 % |
c ==============================================================================
c (current CPU-time: 22.0706 s)
c ==============================================================================
c [1mFound solution: 2120180[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1984750   bits: 22/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     19239 |   79219   277627 |   23765   19233   174321     9.1 | 16.910 % |
c   -- subsuming                       
c   -- var.elim.:  61/61          
c   -- var.elim.:  24/24          
c |     19239 |   79185   277427 |      --   19233       --      -- |     --   | -19/-44
c |     19239 |   79185   277427 |   31674   19233   174321     9.1 | 16.910 % |
c |     19339 |   79185   277427 |   34841   19333   175212     9.1 | 16.971 % |
c |     19489 |   79185   277427 |   38325   19483   176569     9.1 | 16.971 % |
c |     19714 |   79185   277427 |   42158   19708   178997     9.1 | 16.971 % |
c |     20052 |   79185   277427 |   46373   20046   183474     9.2 | 16.971 % |
c |     20558 |   79185   277427 |   51011   20552   188183     9.2 | 16.971 % |
c |     21317 |   79173   277379 |   56103   21309   192441     9.0 | 16.977 % |
c |     22456 |   79173   277379 |   61714   22448   207068     9.2 | 16.977 % |
c |     24164 |   79173   277379 |   67885   24156   223361     9.2 | 16.977 % |
c |     26726 |   79163   277344 |   74664   26716   289562    10.8 | 16.984 % |
c |     30571 |   79153   277309 |   82120   30560   373093    12.2 | 16.990 % |
c |     36338 |   79153   277309 |   90333   36327   860477    23.7 | 16.990 % |
c |     44987 |   79153   277309 |   99366   44976  1109232    24.7 | 16.990 % |
c |     57963 |   79153   277309 |  109303   57952  1940205    33.5 | 16.990 % |
c |     77424 |   79153   277309 |  120233   77413  4912296    63.5 | 16.990 % |
c |    106616 |   79153   277309 |  132256  106605  7403283    69.4 | 16.990 % |
c ==============================================================================
c (current CPU-time: 172.019 s)
c ==============================================================================
c [1mFound solution: 1472036[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2632894   bits: 22/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    130484 |   79207   277636 |   23762  130473 10803566    82.8 | 16.990 % |
c   -- subsuming                       
c   -- var.elim.:  80/80          
c   -- var.elim.:  37/37          
c |    130484 |   79122   277034 |      --  130473       --      -- |     --   | -19/-32
c |    130484 |   79122   277034 |   31648  123905  9859742    79.6 | 16.990 % |
c |    130584 |   79122   277034 |   34813   22327  2503716   112.1 | 17.058 % |
c |    130734 |   79122   277034 |   38295   22477  2504391   111.4 | 17.058 % |
c |    130959 |   79122   277034 |   42124   22702  2505620   110.4 | 17.058 % |
c |    131296 |   79122   277034 |   46337   23039  2507404   108.8 | 17.058 % |
c |    131802 |   79122   277034 |   50970   23545  2510144   106.6 | 17.058 % |
c |    132561 |   79122   277034 |   56067   24304  2514450   103.5 | 17.058 % |
c |    133700 |   79122   277034 |   61674   25443  2521319    99.1 | 17.058 % |
c |    135408 |   79122   277034 |   67842   27151  2535385    93.4 | 17.058 % |
c |    137971 |   79122   277034 |   74626   29714  2576371    86.7 | 17.058 % |
c |    141816 |   79122   277034 |   82088   33559  2627313    78.3 | 17.058 % |
c |    147582 |   79122   277034 |   90297   39325  2707653    68.9 | 17.058 % |
c |    156233 |   79122   277034 |   99327   47976  2906382    60.6 | 17.058 % |
c ==============================================================================
c (current CPU-time: 212.847 s)
c ==============================================================================
c [1mFound solution: 1326727[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2778203   bits: 22/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    160089 |   79155   277227 |   23746   51832  2988241    57.7 | 17.058 % |
c   -- subsuming                       
c   -- var.elim.:  51/51          
c   -- var.elim.:  26/26          
c |    160089 |   79135   277206 |      --   51832       --      -- |     --   | -20/-13
c |    160089 |   79135   277206 |   31654   51831  2988238    57.7 | 17.058 % |
c |    160189 |   79135   277206 |   34819   22174   312457    14.1 | 17.102 % |
c |    160339 |   79135   277206 |   38301   22324   313086    14.0 | 17.102 % |
c |    160564 |   79135   277206 |   42131   22549   314148    13.9 | 17.102 % |
c |    160901 |   79135   277206 |   46344   22886   316096    13.8 | 17.102 % |
c |    161407 |   79135   277206 |   50979   23392   318913    13.6 | 17.102 % |
c |    162166 |   79135   277206 |   56076   24151   324695    13.4 | 17.102 % |
c |    163305 |   79135   277206 |   61684   25290   336577    13.3 | 17.102 % |
c |    165013 |   79135   277206 |   67853   26998   363799    13.5 | 17.102 % |
c |    167575 |   79135   277206 |   74638   29560   436584    14.8 | 17.102 % |
c |    171421 |   79135   277206 |   82102   33406   604773    18.1 | 17.102 % |
c |    177189 |   79135   277206 |   90312   39174   757325    19.3 | 17.102 % |
c |    185838 |   79135   277206 |   99343   47823  1606141    33.6 | 17.102 % |
c |    198812 |   79135   277206 |  109278   60797  2778252    45.7 | 17.102 % |
c |    218276 |   79135   277206 |  120206   80261  4088842    50.9 | 17.102 % |
c |    247468 |   79135   277206 |  132226  109453  5635221    51.5 | 17.102 % |
c ==============================================================================
c (current CPU-time: 365.846 s)
c ==============================================================================
c [1mFound solution: 1260377[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2844553   bits: 22/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    275159 |   79169   277411 |   23750  137144  7485974    54.6 | 17.102 % |
c   -- subsuming                       
c   -- var.elim.:  36/36          
c   -- var.elim.:  22/22          
c |    275159 |   79163   277374 |      --  137144       --      -- |     --   | -6/-28
c |    275159 |   79163   277374 |   31665  137144  7485974    54.6 | 17.102 % |
c |    275259 |   79163   277374 |   34831   23529  1198575    50.9 | 17.148 % |
c |    275412 |   79163   277374 |   38314   23682  1199458    50.6 | 17.148 % |
c |    275637 |   79163   277374 |   42146   23907  1200651    50.2 | 17.148 % |
c |    275974 |   79163   277374 |   46361   24244  1202910    49.6 | 17.148 % |
c |    276480 |   79163   277374 |   50997   24750  1207899    48.8 | 17.148 % |
c |    277240 |   79163   277374 |   56096   25510  1216320    47.7 | 17.148 % |
c |    278380 |   79163   277374 |   61706   26650  1241232    46.6 | 17.148 % |
c |    280089 |   79163   277374 |   67877   28359  1290367    45.5 | 17.148 % |
c |    282652 |   79163   277374 |   74664   30922  1349104    43.6 | 17.148 % |
c |    286496 |   79163   277374 |   82131   34766  1404235    40.4 | 17.148 % |
c |    292262 |   79163   277374 |   90344   40532  1598862    39.4 | 17.148 % |
c |    300911 |   79163   277374 |   99378   49181  2205566    44.8 | 17.148 % |
c |    313885 |   79163   277374 |  109316   62155  2495126    40.1 | 17.148 % |
c |    333351 |   79163   277374 |  120248   81621  3398125    41.6 | 17.148 % |
c |    362543 |   79163   277374 |  132273  110813  6648452    60.0 | 17.148 % |
c |    406335 |   79163   277374 |  145500   34922  2727603    78.1 | 17.148 % |
c |    472019 |   79149   277315 |  160022  100602  6097144    60.6 | 17.155 % |
c |    570545 |   79149   277315 |  176024   63028  7358059   116.7 | 17.155 % |
c |    718334 |   79149   277315 |  193627   46616 11403229   244.6 | 17.155 % |
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_bi#### 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.87 0.97 0.92 1/54 30353
Raw data (stat): 30353 (runsolver) R 30352 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544617549 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.89 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 2307 0 0 0 992 6 0 0 25 0 1 0 544617549 10801152 2075 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2637 2075 603 41 0 2596 0
vsize: 10548
[startup+20.0014 s]
Raw data (loadavg): 0.90 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 7675 0 0 0 1978 19 0 0 25 0 1 0 544617549 27344896 6098 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6676 6098 603 41 0 6635 0
vsize: 26704
[startup+30.0016 s]
Raw data (loadavg): 0.92 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 8124 0 0 0 2977 21 0 0 25 0 1 0 544617549 28160000 6281 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6875 6281 603 41 0 6834 0
vsize: 27500
[startup+40.0027 s]
Raw data (loadavg): 0.93 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 8754 0 0 0 3975 22 0 0 25 0 1 0 544617549 30806016 6911 4294967295 134512640 134672761 3221224544 3221223712 134564705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7521 6911 603 41 0 7480 0
vsize: 30084
[startup+50.0035 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 9267 0 0 0 4974 24 0 0 25 0 1 0 544617549 32808960 7424 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8010 7424 603 41 0 7969 0
vsize: 32040
[startup+60.003 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 10173 0 0 0 5972 26 0 0 25 0 1 0 544617549 36515840 8330 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8915 8330 603 41 0 8874 0
vsize: 35660
[startup+70.0069 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 10815 0 0 0 6971 28 0 0 25 0 1 0 544617549 39415808 8972 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9623 8972 603 41 0 9582 0
vsize: 38492
[startup+80.0096 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 11634 0 0 0 7968 31 0 0 25 0 1 0 544617549 42717184 9791 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10429 9791 603 41 0 10388 0
vsize: 41716
[startup+90.011 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 12724 0 0 0 8966 33 0 0 25 0 1 0 544617549 47194112 10881 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11522 10881 603 41 0 11481 0
vsize: 46088
[startup+100.011 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 13441 0 0 0 9965 35 0 0 25 0 1 0 544617549 50077696 11598 4294967295 134512640 134672761 3221224544 3221223728 134615752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12226 11598 603 41 0 12185 0
vsize: 48904
[startup+110.011 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 14251 0 0 0 10962 38 0 0 25 0 1 0 544617549 53399552 12408 4294967295 134512640 134672761 3221224544 3221223584 134614348 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13037 12408 603 41 0 12996 0
vsize: 52148
[startup+120.012 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 15180 0 0 0 11959 41 0 0 25 0 1 0 544617549 57110528 13337 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13943 13337 603 41 0 13902 0
vsize: 55772
[startup+130.012 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 16030 0 0 0 12957 43 0 0 25 0 1 0 544617549 60551168 14187 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14783 14187 603 41 0 14742 0
vsize: 59132
[startup+140.012 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 16611 0 0 0 13956 44 0 0 25 0 1 0 544617549 62951424 14768 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15369 14768 603 41 0 15328 0
vsize: 61476
[startup+150.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 17717 0 0 0 14954 47 0 0 25 0 1 0 544617549 67465216 15874 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16471 15874 603 41 0 16430 0
vsize: 65884
[startup+160.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 18752 0 0 0 15951 49 0 0 25 0 1 0 544617549 71663616 16909 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17496 16909 603 41 0 17455 0
vsize: 69984
[startup+170.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 19716 0 0 0 16950 51 0 0 25 0 1 0 544617549 75608064 17873 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18459 17873 603 41 0 18418 0
vsize: 73836
[startup+180.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 20465 0 0 0 17947 53 0 0 25 0 1 0 544617549 77651968 18356 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18958 18356 603 41 0 18917 0
vsize: 75832
[startup+190.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 20465 0 0 0 18948 53 0 0 25 0 1 0 544617549 77651968 18356 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18958 18356 603 41 0 18917 0
vsize: 75832
[startup+200.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 20465 0 0 0 19948 53 0 0 25 0 1 0 544617549 77651968 18356 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18958 18356 603 41 0 18917 0
vsize: 75832
[startup+210.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 20465 0 0 0 20948 53 0 0 25 0 1 0 544617549 77651968 18356 4294967295 134512640 134672761 3221224544 3221223728 134616011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18958 18356 603 41 0 18917 0
vsize: 75832
[startup+220.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 20768 0 0 0 21947 54 0 0 25 0 1 0 544617549 76775424 18159 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18744 18159 603 41 0 18703 0
vsize: 74976
[startup+230.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 20768 0 0 0 22947 54 0 0 25 0 1 0 544617549 76775424 18159 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18744 18159 603 41 0 18703 0
vsize: 74976
[startup+240.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 20768 0 0 0 23947 54 0 0 25 0 1 0 544617549 76775424 18159 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18744 18159 603 41 0 18703 0
vsize: 74976
[startup+250.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 20768 0 0 0 24947 54 0 0 25 0 1 0 544617549 76775424 18159 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18744 18159 603 41 0 18703 0
vsize: 74976
[startup+260.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 20768 0 0 0 25947 54 0 0 25 0 1 0 544617549 76775424 18159 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18744 18159 603 41 0 18703 0
vsize: 74976
[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 20768 0 0 0 26947 54 0 0 25 0 1 0 544617549 76775424 18159 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18744 18159 603 41 0 18703 0
vsize: 74976
[startup+280.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 20768 0 0 0 27947 54 0 0 25 0 1 0 544617549 76775424 18159 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18744 18159 603 41 0 18703 0
vsize: 74976
[startup+290.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 20768 0 0 0 28947 55 0 0 25 0 1 0 544617549 76775424 18159 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18744 18159 603 41 0 18703 0
vsize: 74976
[startup+300.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 20768 0 0 0 29948 55 0 0 25 0 1 0 544617549 76775424 18159 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18744 18159 603 41 0 18703 0
vsize: 74976
[startup+310.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 20768 0 0 0 30948 55 0 0 25 0 1 0 544617549 76775424 18159 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18744 18159 603 41 0 18703 0
vsize: 74976
[startup+320.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 20768 0 0 0 31948 55 0 0 25 0 1 0 544617549 76775424 18159 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18744 18159 603 41 0 18703 0
vsize: 74976
[startup+330.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 20768 0 0 0 32948 55 0 0 25 0 1 0 544617549 76775424 18159 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18744 18159 603 41 0 18703 0
vsize: 74976
[startup+340.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 20768 0 0 0 33948 55 0 0 25 0 1 0 544617549 76775424 18159 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18744 18159 603 41 0 18703 0
vsize: 74976
[startup+350.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 20768 0 0 0 34948 55 0 0 25 0 1 0 544617549 76775424 18159 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18744 18159 603 41 0 18703 0
vsize: 74976
[startup+360.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 20770 0 0 0 35948 55 0 0 25 0 1 0 544617549 77299712 18161 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18872 18161 603 41 0 18831 0
vsize: 75488
[startup+370.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21259 0 0 0 36947 56 0 0 25 0 1 0 544617549 77299712 18172 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18872 18172 603 41 0 18831 0
vsize: 75488
[startup+380.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21259 0 0 0 37946 57 0 0 25 0 1 0 544617549 77299712 18172 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18872 18172 603 41 0 18831 0
vsize: 75488
[startup+390.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21259 0 0 0 38946 57 0 0 25 0 1 0 544617549 77299712 18172 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18872 18172 603 41 0 18831 0
vsize: 75488
[startup+400.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21259 0 0 0 39946 57 0 0 25 0 1 0 544617549 77299712 18172 4294967295 134512640 134672761 3221224544 3221223668 134566106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18872 18172 603 41 0 18831 0
vsize: 75488
[startup+410.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21259 0 0 0 40946 57 0 0 25 0 1 0 544617549 77299712 18172 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18872 18172 603 41 0 18831 0
vsize: 75488
[startup+420.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21259 0 0 0 41946 57 0 0 25 0 1 0 544617549 77299712 18172 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18872 18172 603 41 0 18831 0
vsize: 75488
[startup+430.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21259 0 0 0 42945 58 0 0 25 0 1 0 544617549 77299712 18172 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18872 18172 603 41 0 18831 0
vsize: 75488
[startup+440.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21259 0 0 0 43945 59 0 0 25 0 1 0 544617549 77299712 18172 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18872 18172 603 41 0 18831 0
vsize: 75488
[startup+450.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21259 0 0 0 44944 59 0 0 25 0 1 0 544617549 77299712 18172 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18872 18172 603 41 0 18831 0
vsize: 75488
[startup+460.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21259 0 0 0 45944 59 0 0 25 0 1 0 544617549 77299712 18172 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18872 18172 603 41 0 18831 0
vsize: 75488
[startup+470.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21259 0 0 0 46944 60 0 0 25 0 1 0 544617549 77299712 18172 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18872 18172 603 41 0 18831 0
vsize: 75488
[startup+480.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21259 0 0 0 47944 60 0 0 25 0 1 0 544617549 77299712 18172 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18872 18172 603 41 0 18831 0
vsize: 75488
[startup+490.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21259 0 0 0 48943 60 0 0 25 0 1 0 544617549 77299712 18172 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18872 18172 603 41 0 18831 0
vsize: 75488
[startup+500.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21259 0 0 0 49943 61 0 0 25 0 1 0 544617549 77299712 18172 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18872 18172 603 41 0 18831 0
vsize: 75488
[startup+510.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21259 0 0 0 50944 61 0 0 25 0 1 0 544617549 77299712 18172 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18872 18172 603 41 0 18831 0
vsize: 75488
[startup+520.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21425 0 0 0 51943 61 0 0 25 0 1 0 544617549 78438400 18338 4294967295 134512640 134672761 3221224544 3221223264 134645416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19150 18338 603 41 0 19109 0
vsize: 76600
[startup+530.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21430 0 0 0 52943 61 0 0 25 0 1 0 544617549 77389824 18204 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18894 18204 603 41 0 18853 0
vsize: 75576
[startup+540.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21430 0 0 0 53943 61 0 0 25 0 1 0 544617549 77389824 18204 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18894 18204 603 41 0 18853 0
vsize: 75576
[startup+550.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21430 0 0 0 54943 61 0 0 25 0 1 0 544617549 77389824 18204 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18894 18204 603 41 0 18853 0
vsize: 75576
[startup+560.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21430 0 0 0 55943 61 0 0 25 0 1 0 544617549 77389824 18204 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18894 18204 603 41 0 18853 0
vsize: 75576
[startup+570.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21430 0 0 0 56943 61 0 0 25 0 1 0 544617549 77389824 18204 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18894 18204 603 41 0 18853 0
vsize: 75576
[startup+580.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21430 0 0 0 57943 61 0 0 25 0 1 0 544617549 77389824 18204 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18894 18204 603 41 0 18853 0
vsize: 75576
[startup+590.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21430 0 0 0 58944 62 0 0 25 0 1 0 544617549 77389824 18204 4294967295 134512640 134672761 3221224544 3221223728 134616017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18894 18204 603 41 0 18853 0
vsize: 75576
[startup+600.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21430 0 0 0 59944 62 0 0 25 0 1 0 544617549 77389824 18204 4294967295 134512640 134672761 3221224544 3221223788 134615416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18894 18204 603 41 0 18853 0
vsize: 75576
[startup+610.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21430 0 0 0 60944 62 0 0 25 0 1 0 544617549 77389824 18204 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18894 18204 603 41 0 18853 0
vsize: 75576
[startup+620.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21430 0 0 0 61944 62 0 0 25 0 1 0 544617549 77389824 18204 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18894 18204 603 41 0 18853 0
vsize: 75576
[startup+630.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21430 0 0 0 62944 62 0 0 25 0 1 0 544617549 77389824 18204 4294967295 134512640 134672761 3221224544 3221223920 134620485 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18894 18204 603 41 0 18853 0
vsize: 75576
[startup+640.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21430 0 0 0 63944 62 0 0 25 0 1 0 544617549 77389824 18204 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18894 18204 603 41 0 18853 0
vsize: 75576
[startup+650.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21430 0 0 0 64945 62 0 0 25 0 1 0 544617549 77389824 18204 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18894 18204 603 41 0 18853 0
vsize: 75576
[startup+660.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21430 0 0 0 65945 62 0 0 25 0 1 0 544617549 77389824 18204 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18894 18204 603 41 0 18853 0
vsize: 75576
[startup+670.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 21430 0 0 0 66945 62 0 0 25 0 1 0 544617549 77389824 18204 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18894 18204 603 41 0 18853 0
vsize: 75576
[startup+680.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 22111 0 0 0 67943 64 0 0 25 0 1 0 544617549 80179200 18885 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19575 18885 603 41 0 19534 0
vsize: 78300
[startup+690.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 23983 0 0 0 68938 69 0 0 25 0 1 0 544617549 87879680 20757 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21455 20757 603 41 0 21414 0
vsize: 85820
[startup+700.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 25933 0 0 0 69935 72 0 0 25 0 1 0 544617549 95940608 22707 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23423 22707 603 41 0 23382 0
vsize: 93692
[startup+710.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 27293 0 0 0 70932 75 0 0 25 0 1 0 544617549 101527552 24067 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24787 24067 603 41 0 24746 0
vsize: 99148
[startup+720.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 28873 0 0 0 71930 78 0 0 25 0 1 0 544617549 107999232 25647 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26367 25647 603 41 0 26326 0
vsize: 105468
[startup+730.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 30112 0 0 0 72927 80 0 0 25 0 1 0 544617549 112951296 26886 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27576 26886 603 41 0 27535 0
vsize: 110304
[startup+740.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 31448 0 0 0 73924 84 0 0 25 0 1 0 544617549 118476800 28222 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28925 28222 603 41 0 28884 0
vsize: 115700
[startup+750.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 32585 0 0 0 74921 88 0 0 25 0 1 0 544617549 123097088 29359 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30053 29359 603 41 0 30012 0
vsize: 120212
[startup+760.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 33571 0 0 0 75919 89 0 0 25 0 1 0 544617549 127139840 30345 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31040 30345 603 41 0 30999 0
vsize: 124160
[startup+770.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 34508 0 0 0 76917 92 0 0 25 0 1 0 544617549 130969600 31282 4294967295 134512640 134672761 3221224544 3221223564 134565024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31975 31282 603 41 0 31934 0
vsize: 127900
[startup+780.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 35756 0 0 0 77914 95 0 0 25 0 1 0 544617549 136028160 32530 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33210 32530 603 41 0 33169 0
vsize: 132840
[startup+790.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 37255 0 0 0 78911 98 0 0 25 0 1 0 544617549 142278656 34029 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34736 34029 603 41 0 34695 0
vsize: 138944
[startup+800.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 38785 0 0 0 79909 100 0 0 25 0 1 0 544617549 148463616 35559 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36246 35559 603 41 0 36205 0
vsize: 144984
[startup+810.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 39939 0 0 0 80908 102 0 0 25 0 1 0 544617549 153145344 36713 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37389 36713 603 41 0 37348 0
vsize: 149556
[startup+820.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40542 0 0 0 81906 104 0 0 25 0 1 0 544617549 155660288 37316 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38003 37316 603 41 0 37962 0
vsize: 152012
[startup+830.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 82905 104 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223480 1075350790 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+840.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 83906 104 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+850.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 84906 105 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+860.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 85906 105 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+870.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 86906 105 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+880.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 87906 105 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223712 134564734 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+890.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 88906 105 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+900.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 89907 105 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+910.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 90907 105 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+920.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 91907 105 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223584 134613822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+930.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 92907 105 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+940.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 93907 105 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+950.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 94907 105 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+960.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 95907 105 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+970.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 96908 105 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+980.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 97908 105 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+990.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 98908 105 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 99908 105 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 100908 105 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 101908 105 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 102909 105 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40859 0 0 0 103909 105 0 0 25 0 1 0 544617549 156696576 37473 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37473 603 41 0 38215 0
vsize: 153024
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40863 0 0 0 104909 105 0 0 25 0 1 0 544617549 156696576 37477 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37477 603 41 0 38215 0
vsize: 153024
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40868 0 0 0 105909 105 0 0 25 0 1 0 544617549 156696576 37482 4294967295 134512640 134672761 3221224544 3221223800 134618476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37482 603 41 0 38215 0
vsize: 153024
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40873 0 0 0 106909 105 0 0 25 0 1 0 544617549 156696576 37487 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37487 603 41 0 38215 0
vsize: 153024
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40876 0 0 0 107909 105 0 0 25 0 1 0 544617549 156696576 37490 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37490 603 41 0 38215 0
vsize: 153024
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 40878 0 0 0 108910 105 0 0 25 0 1 0 544617549 156696576 37492 4294967295 134512640 134672761 3221224544 3221223584 134612791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37492 603 41 0 38215 0
vsize: 153024
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 41087 0 0 0 109909 106 0 0 25 0 1 0 544617549 156696576 37521 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37521 603 41 0 38215 0
vsize: 153024
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 41087 0 0 0 110910 106 0 0 25 0 1 0 544617549 156696576 37521 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37521 603 41 0 38215 0
vsize: 153024
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 41087 0 0 0 111910 106 0 0 25 0 1 0 544617549 156696576 37521 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37521 603 41 0 38215 0
vsize: 153024
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 41087 0 0 0 112910 106 0 0 25 0 1 0 544617549 156696576 37521 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37521 603 41 0 38215 0
vsize: 153024
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 41087 0 0 0 113910 106 0 0 25 0 1 0 544617549 156696576 37521 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37521 603 41 0 38215 0
vsize: 153024
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 41087 0 0 0 114910 106 0 0 25 0 1 0 544617549 156696576 37521 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37521 603 41 0 38215 0
vsize: 153024
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 41087 0 0 0 115910 106 0 0 25 0 1 0 544617549 156696576 37521 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37521 603 41 0 38215 0
vsize: 153024
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 41087 0 0 0 116910 106 0 0 25 0 1 0 544617549 156696576 37521 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37521 603 41 0 38215 0
vsize: 153024
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 41087 0 0 0 117911 106 0 0 25 0 1 0 544617549 156696576 37521 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37521 603 41 0 38215 0
vsize: 153024
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 41087 0 0 0 118911 106 0 0 25 0 1 0 544617549 156696576 37521 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37521 603 41 0 38215 0
vsize: 153024
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30353
Raw data (stat): 30353 (minisat+) R 30352 27222 27221 0 -1 0 41087 0 0 0 119911 106 0 0 25 0 1 0 544617549 156696576 37521 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38256 37521 603 41 0 38215 0
vsize: 153024
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 30353
Raw data (stat): 30353 (minisat+) Z 30352 27222 27221 0 -1 12 41088 0 0 0 119911 113 0 0 25 0 1 0 544617549 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.13
CPU time (s): 1200.26
CPU user time (s): 1199.12
CPU system time (s): 1.13983
CPU usage (%): 100.011
Max. virtual memory (Kb): 153024
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####