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-bal8x12.opb
MD5SUM	69e7430fb77e7d40f128bdde5f7776a3
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	13476271
Optimality of the best value was proved	NO
Number of terms in the objective function	2016
Biggest coefficient in the objective function	402653184
Number of bits for the biggest coefficient in the objective function	29
Sum of the numbers in the objective function	34444990400
Number of bits of the sum of numbers in the objective function	36
Biggest number in a constraint	402653184
Number of bits of the biggest number in a constraint	29
Biggest sum of numbers in a constraint	34444990400
Number of bits of the biggest sum of numbers	36
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.37
Number of variables	2016
Total number of constraints	116
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	116
Minimum length of a constraint	21
Maximum length of a constraint	240
Trace number 14944

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        792296 kB
Buffers:          5956 kB
Cached:         213208 kB
SwapCached:          0 kB
Active:          60308 kB
Inactive:       161720 kB
HighTotal:      131008 kB
HighFree:        69692 kB
LowTotal:       903652 kB
LowFree:        722604 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            14500 kB
Committed_AS:    63784 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 02:30:51 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 18967 7 1200.25 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 136 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 134]---> Adder-cost: 240   maxlim: 20596   bits: 15/15
c ---[ 132]---> Adder-cost: 254   maxlim: 32244   bits: 16/15
c ---[ 130]---> Adder-cost: 254   maxlim: 33140   bits: 16/16
c ---[ 128]---> Adder-cost: 254   maxlim: 34420   bits: 16/16
c ---[ 126]---> Adder-cost: 254   maxlim: 31604   bits: 16/15
c ---[ 124]---> Adder-cost: 254   maxlim: 34420   bits: 16/16
c ---[ 122]---> Adder-cost: 240   maxlim: 21236   bits: 15/15
c ---[ 120]---> Adder-cost: 254   maxlim: 31604   bits: 16/15
c ---[ 118]---> Sorter-cost: 1497     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost: 1497     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 1497     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 1497     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  98]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  96]---> Sorter-cost: 1497     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  95]---> BDD-cost:   15
c ---[  94]---> BDD-cost:   15
c ---[  93]---> BDD-cost:   14
c ---[  92]---> BDD-cost:   13
c ---[  91]---> BDD-cost:   15
c ---[  90]---> BDD-cost:   15
c ---[  89]---> BDD-cost:   15
c ---[  88]---> BDD-cost:   15
c ---[  87]---> BDD-cost:   13
c ---[  86]---> BDD-cost:   15
c ---[  85]---> BDD-cost:   15
c ---[  84]---> BDD-cost:   14
c ---[  83]---> BDD-cost:   15
c ---[  82]---> BDD-cost:   15
c ---[  81]---> BDD-cost:   15
c ---[  80]---> BDD-cost:   14
c ---[  79]---> BDD-cost:   13
c ---[  78]---> BDD-cost:   15
c ---[  77]---> BDD-cost:   15
c ---[  76]---> BDD-cost:   15
c ---[  75]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   13
c ---[  73]---> BDD-cost:   15
c ---[  72]---> BDD-cost:   15
c ---[  71]---> BDD-cost:   16
c ---[  70]---> BDD-cost:   14
c ---[  69]---> BDD-cost:   19
c ---[  68]---> BDD-cost:   17
c ---[  67]---> BDD-cost:   14
c ---[  66]---> BDD-cost:   13
c ---[  65]---> BDD-cost:   15
c ---[  64]---> BDD-cost:   15
c ---[  63]---> BDD-cost:   15
c ---[  62]---> BDD-cost:   15
c ---[  61]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  59]---> BDD-cost:   15
c ---[  58]---> BDD-cost:   16
c ---[  57]---> BDD-cost:   14
c ---[  56]---> BDD-cost:   19
c ---[  55]---> BDD-cost:   17
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   13
c ---[  52]---> BDD-cost:   15
c ---[  51]---> BDD-cost:   15
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   15
c ---[  47]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   15
c ---[  45]---> BDD-cost:   17
c ---[  44]---> BDD-cost:   14
c ---[  43]---> BDD-cost:   17
c ---[  42]---> BDD-cost:   17
c ---[  41]---> BDD-cost:   14
c ---[  40]---> BDD-cost:   13
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   15
c ---[  37]---> BDD-cost:   15
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   15
c ---[  34]---> BDD-cost:   13
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   16
c ---[  31]---> BDD-cost:   14
c ---[  30]---> BDD-cost:   19
c ---[  29]---> BDD-cost:   17
c ---[  28]---> BDD-cost:   14
c ---[  27]---> BDD-cost:   14
c ---[  26]---> BDD-cost:   13
c ---[  25]---> BDD-cost:   14
c ---[  24]---> BDD-cost:   14
c ---[  23]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   14
c ---[  21]---> BDD-cost:   13
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   14
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   14
c ---[  14]---> BDD-cost:   14
c ---[  13]---> BDD-cost:   13
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   15
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   13
c ---[   7]---> BDD-cost:   15
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   17
c ---[   4]---> BDD-cost:   14
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   17
c ---[   1]---> BDD-cost:   14
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   56429   149912 |   18809       0        0     nan |  0.000 % |
c |       100 |   56384   149751 |   20689      96      328     3.4 | 11.015 % |
c |       251 |   56361   149676 |   22758     243      890     3.7 | 11.036 % |
c |       476 |   56345   149641 |   25034     463     1663     3.6 | 11.063 % |
c |       814 |   56280   149477 |   27538     795     2916     3.7 | 11.153 % |
c |      1320 |   56265   149443 |   30292    1299     4845     3.7 | 11.180 % |
c |      2080 |   56240   149378 |   33321    2056     8411     4.1 | 11.217 % |
c |      3219 |   56225   149344 |   36653    3193    65915    20.6 | 11.244 % |
c |      4927 |   55756   148108 |   40318    4843    75498    15.6 | 11.877 % |
c |      7489 |   55344   147064 |   44350    7348    88149    12.0 | 12.484 % |
c ==============================================================================
c [1mFound solution: 27413710[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 9016   maxlim: 83025650   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9773 |  117753   370741 |   39251    9576   108114    11.3 | 12.484 % |
c |      9873 |  117753   370741 |   43176    9676   108647    11.2 |  9.156 % |
c |     10023 |  117753   370741 |   47493    9826   109698    11.2 |  9.156 % |
c |     10248 |  117674   370556 |   52243   10036   113408    11.3 |  9.253 % |
c |     10585 |  117564   370257 |   57467   10351   114969    11.1 |  9.361 % |
c |     11092 |  117564   370257 |   63214   10858   126381    11.6 |  9.361 % |
c |     11851 |  117553   370232 |   69535   11616   130841    11.3 |  9.372 % |
c |     12990 |  117527   370172 |   76489   12738   151390    11.9 |  9.401 % |
c |     14699 |  117288   369620 |   84138   14440   208971    14.5 |  9.678 % |
c |     17261 |  117232   369489 |   92551   16994   251614    14.8 |  9.735 % |
c ==============================================================================
c [1mFound solution: 24439908[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 85999452   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19604 |  117120   369414 |   39040   19319   284602    14.7 |  9.735 % |
c |     19705 |  117120   369414 |   42944   19420   285163    14.7 |  9.924 % |
c |     19855 |  117120   369414 |   47238   19570   286160    14.6 |  9.924 % |
c |     20080 |  117093   369354 |   51962   19791   287872    14.5 |  9.949 % |
c |     20418 |  117093   369354 |   57158   20129   291184    14.5 |  9.949 % |
c |     20924 |  116972   369077 |   62874   20617   295109    14.3 | 10.086 % |
c |     21683 |  116925   368970 |   69161   21375   312417    14.6 | 10.136 % |
c |     22822 |  116918   368955 |   76077   22512   352011    15.6 | 10.143 % |
c |     24530 |  116704   368458 |   83685   24201   412743    17.1 | 10.387 % |
c |     27092 |  116704   368458 |   92054   26763   841290    31.4 | 10.387 % |
c ==============================================================================
c [1mFound solution: 20279065[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 90160295   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28024 |  116729   368669 |   38909   27695   861086    31.1 | 10.387 % |
c |     28124 |  116723   368655 |   42799   27793   861522    31.0 | 10.438 % |
c |     28275 |  116713   368632 |   47079   27943   862289    30.9 | 10.453 % |
c |     28500 |  116713   368632 |   51787   28168   863650    30.7 | 10.453 % |
c |     28837 |  116713   368632 |   56966   28505   867090    30.4 | 10.453 % |
c |     29343 |  116713   368632 |   62663   29011   873574    30.1 | 10.453 % |
c |     30102 |  116713   368632 |   68929   29770   893557    30.0 | 10.453 % |
c |     31243 |  116699   368592 |   75822   30905   977721    31.6 | 10.467 % |
c |     32951 |  116699   368592 |   83404   32613  1259701    38.6 | 10.467 % |
c |     35516 |  116692   368574 |   91745   35177  1391738    39.6 | 10.474 % |
c |     39361 |  116495   368114 |  100919   39005  1693931    43.4 | 10.729 % |
c |     45128 |  116477   368052 |  111011   44766  2047631    45.7 | 10.736 % |
c ==============================================================================
c [1mFound solution: 17921195[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 92518165   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     52876 |  116503   368272 |   38834   52513  4208240    80.1 | 10.736 % |
c |     52976 |  116471   368197 |   42717   19235  2479398   128.9 | 10.816 % |
c |     53126 |  116332   367880 |   46989   19370  2480310   128.0 | 10.974 % |
c |     53353 |  116332   367880 |   51688   19597  2481687   126.6 | 10.974 % |
c |     53690 |  116332   367880 |   56856   19934  2484822   124.7 | 10.974 % |
c |     54196 |  116332   367880 |   62542   20440  2489310   121.8 | 10.974 % |
c |     54956 |  116310   367831 |   68796   21199  2493460   117.6 | 10.999 % |
c |     56095 |  116310   367831 |   75676   22338  2507046   112.2 | 10.999 % |
c |     57804 |  116310   367831 |   83244   24047  3037164   126.3 | 10.999 % |
c |     60366 |  116305   367820 |   91568   26608  3216251   120.9 | 11.006 % |
c |     64212 |  116284   367770 |  100725   30453  3837065   126.0 | 11.031 % |
c |     69978 |  116196   367569 |  110797   36208  5039520   139.2 | 11.132 % |
c |     78627 |  116105   367358 |  121877   44845  5924407   132.1 | 11.240 % |
c |     91601 |  116101   367348 |  134065   57818  8041753   139.1 | 11.243 % |
c |    111063 |  116070   367259 |  147472   77276 12240284   158.4 | 11.265 % |
c |    140255 |  116070   367259 |  162219  106468 19322178   181.5 | 11.265 % |
c |    184044 |  115999   367090 |  178441  150249 30112161   200.4 | 11.347 % |
c |    249728 |  115757   366528 |  196285   46021  7759811   168.6 | 11.641 % |
c |    348254 |  115739   366485 |  215913  144545 20475461   141.7 | 11.663 % |
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 -Y0_bit0 Y1_bit0 Y2_bit0 -Y3_bit0 Y4_bit0 -Y5_bit0 -Y6_bit0 -Y7_bit0 Y8_bit0 Y9_bit0 -Y10_bit0 Y11_bit0 -Y12_bit0 -Y13_bit0 Y14_bit0 -Y15_bit0 -Y16_bit0 -Y17_bit0 Y18_bit0 -Y19_bit0 Y20_bit0 -Y21_bit0 -Y22_bit0 Y23_bit0 Y24_bit0 Y25_bit0 -Y26_bit0 -Y27_bit0 Y28_bit0 Y29_bit0 Y30_bit0 -Y31_bit0 -Y32_bit0 Y33_bit0 Y34_bit0 -Y35_bit0 Y36_bit0 -Y37_bit0 Y38_bit0 Y39_bit0 -Y40_bit0 -Y41_bit0 Y42_bit0 Y43_bit0 Y44_bit0 Y45_bit0 Y46_bit0 -Y47_bit0 Y48_bit0 Y49_bit0 -Y50_bit0 Y51_bit0 Y52_bit0 Y53_bit0 Y54_bit0 Y55_bit0 Y56_bit0 -Y57_bit0 Y58_bit0 Y59_bit0 Y60_bit0 -Y61_bit0 -Y62_bit0 Y63_bit0 -Y64_bit0 Y65_bit0 Y66_bit0 -Y67_bit0 Y68_bit0 -Y69_bit0 -Y70_bit0 -Y71_bit0 -Y72_bit0 Y7#### 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.91 0.95 0.90 2/55 32635
Raw data (stat): 32635 (runsolver) R 32634 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 418638475 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 2124 0 0 0 994 5 0 0 25 0 1 0 418638475 10825728 2044 4294967295 134512640 134672761 3221224544 3221223712 134561051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2643 2044 603 41 0 2602 0
vsize: 10572
[startup+20.0019 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 8207 0 0 0 1980 19 0 0 25 0 1 0 418638475 32092160 6848 4294967295 134512640 134672761 3221224544 3221223760 134561987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7835 6848 603 41 0 7794 0
vsize: 31340
[startup+30.0023 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 8371 0 0 0 2979 20 0 0 25 0 1 0 418638475 32731136 7012 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7991 7012 603 41 0 7950 0
vsize: 31964
[startup+40.002 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 8652 0 0 0 3978 21 0 0 25 0 1 0 418638475 33509376 7225 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8181 7225 603 41 0 8140 0
vsize: 32724
[startup+50.0017 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 9176 0 0 0 4977 22 0 0 25 0 1 0 418638475 35651584 7749 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8704 7749 603 41 0 8663 0
vsize: 34816
[startup+60.0024 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 9408 0 0 0 5976 23 0 0 25 0 1 0 418638475 36270080 7895 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8855 7895 603 41 0 8814 0
vsize: 35420
[startup+70.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 9904 0 0 0 6975 25 0 0 25 0 1 0 418638475 38416384 8391 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9379 8391 603 41 0 9338 0
vsize: 37516
[startup+80.0042 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 10270 0 0 0 7974 26 0 0 25 0 1 0 418638475 39907328 8757 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9743 8757 603 41 0 9702 0
vsize: 38972
[startup+90.0044 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 10796 0 0 0 8971 29 0 0 25 0 1 0 418638475 42057728 9283 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10268 9283 603 41 0 10227 0
vsize: 41072
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 11905 0 0 0 9968 32 0 0 25 0 1 0 418638475 46608384 10392 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11379 10392 603 41 0 11338 0
vsize: 45516
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 12715 0 0 0 10966 34 0 0 25 0 1 0 418638475 49844224 11202 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12169 11202 603 41 0 12128 0
vsize: 48676
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 13028 0 0 0 11964 36 0 0 25 0 1 0 418638475 50618368 11407 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12358 11407 603 41 0 12317 0
vsize: 49432
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 13028 0 0 0 12965 36 0 0 25 0 1 0 418638475 50618368 11407 4294967295 134512640 134672761 3221224544 3221223728 134559156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12358 11407 603 41 0 12317 0
vsize: 49432
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 13028 0 0 0 13964 36 0 0 25 0 1 0 418638475 50618368 11407 4294967295 134512640 134672761 3221224544 3221223612 1075346698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12358 11407 603 41 0 12317 0
vsize: 49432
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 13167 0 0 0 14964 36 0 0 25 0 1 0 418638475 51294208 11546 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12523 11546 603 41 0 12482 0
vsize: 50092
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 13699 0 0 0 15963 38 0 0 25 0 1 0 418638475 53452800 12078 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13050 12078 603 41 0 13009 0
vsize: 52200
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 14033 0 0 0 16962 39 0 0 25 0 1 0 418638475 54804480 12412 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13380 12412 603 41 0 13339 0
vsize: 53520
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 14805 0 0 0 17960 41 0 0 25 0 1 0 418638475 57901056 13184 4294967295 134512640 134672761 3221224544 3221223728 134559417 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14136 13184 603 41 0 14095 0
vsize: 56544
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 15946 0 0 0 18957 44 0 0 25 0 1 0 418638475 62636032 14325 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15292 14325 603 41 0 15251 0
vsize: 61168
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 16738 0 0 0 19954 47 0 0 25 0 1 0 418638475 65863680 15117 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16080 15117 603 41 0 16039 0
vsize: 64320
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 17182 0 0 0 20952 49 0 0 25 0 1 0 418638475 67620864 15561 4294967295 134512640 134672761 3221224544 3221223728 134559599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16509 15561 603 41 0 16468 0
vsize: 66036
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 17876 0 0 0 21950 52 0 0 25 0 1 0 418638475 70455296 16255 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17201 16255 603 41 0 17160 0
vsize: 68804
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 18452 0 0 0 22948 54 0 0 25 0 1 0 418638475 73138176 16831 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17856 16831 603 41 0 17815 0
vsize: 71424
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 18758 0 0 0 23948 54 0 0 25 0 1 0 418638475 74350592 17137 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18152 17137 603 41 0 18111 0
vsize: 72608
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 19354 0 0 0 24945 57 0 0 25 0 1 0 418638475 76775424 17733 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18744 17733 603 41 0 18703 0
vsize: 74976
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 19944 0 0 0 25943 60 0 0 25 0 1 0 418638475 79196160 18323 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19335 18323 603 41 0 19294 0
vsize: 77340
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 20582 0 0 0 26941 61 0 0 25 0 1 0 418638475 81752064 18961 4294967295 134512640 134672761 3221224544 3221223648 134559841 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19959 18961 603 41 0 19918 0
vsize: 79836
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 21243 0 0 0 27940 63 0 0 25 0 1 0 418638475 84430848 19622 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20613 19622 603 41 0 20572 0
vsize: 82452
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 21740 0 0 0 28939 64 0 0 25 0 1 0 418638475 86470656 20119 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21111 20119 603 41 0 21070 0
vsize: 84444
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 22314 0 0 0 29937 66 0 0 25 0 1 0 418638475 88895488 20693 4294967295 134512640 134672761 3221224544 3221223728 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21703 20693 603 41 0 21662 0
vsize: 86812
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 23006 0 0 0 30936 67 0 0 25 0 1 0 418638475 91709440 21385 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22390 21385 603 41 0 22349 0
vsize: 89560
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 23697 0 0 0 31935 69 0 0 25 0 1 0 418638475 94523392 22076 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23077 22076 603 41 0 23036 0
vsize: 92308
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 24440 0 0 0 32934 70 0 0 25 0 1 0 418638475 97599488 22819 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23828 22819 603 41 0 23787 0
vsize: 95312
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 25062 0 0 0 33933 71 0 0 25 0 1 0 418638475 100024320 23441 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24420 23441 603 41 0 24379 0
vsize: 97680
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 25726 0 0 0 34931 73 0 0 25 0 1 0 418638475 102842368 24105 4294967295 134512640 134672761 3221224544 3221223648 134559998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25108 24105 603 41 0 25067 0
vsize: 100432
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 26280 0 0 0 35930 74 0 0 25 0 1 0 418638475 104992768 24659 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25633 24659 603 41 0 25592 0
vsize: 102532
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 26799 0 0 0 36929 75 0 0 25 0 1 0 418638475 107155456 25178 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26161 25178 603 41 0 26120 0
vsize: 104644
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 27329 0 0 0 37928 76 0 0 25 0 1 0 418638475 109309952 25708 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26687 25708 603 41 0 26646 0
vsize: 106748
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 27861 0 0 0 38926 78 0 0 25 0 1 0 418638475 111468544 26240 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27214 26240 603 41 0 27173 0
vsize: 108856
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 28334 0 0 0 39925 80 0 0 25 0 1 0 418638475 113483776 26713 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27706 26713 603 41 0 27665 0
vsize: 110824
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 28649 0 0 0 40924 81 0 0 25 0 1 0 418638475 114700288 27028 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28003 27028 603 41 0 27962 0
vsize: 112012
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 28927 0 0 0 41924 81 0 0 25 0 1 0 418638475 115904512 27306 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28297 27306 603 41 0 28256 0
vsize: 113188
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 29399 0 0 0 42923 82 0 0 25 0 1 0 418638475 117788672 27778 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28757 27778 603 41 0 28716 0
vsize: 115028
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 29814 0 0 0 43921 84 0 0 25 0 1 0 418638475 119414784 28193 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29154 28193 603 41 0 29113 0
vsize: 116616
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 30149 0 0 0 44920 85 0 0 25 0 1 0 418638475 120758272 28528 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29482 28528 603 41 0 29441 0
vsize: 117928
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 30571 0 0 0 45919 86 0 0 25 0 1 0 418638475 122499072 28950 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29907 28950 603 41 0 29866 0
vsize: 119628
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 31019 0 0 0 46918 87 0 0 25 0 1 0 418638475 124403712 29398 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30372 29398 603 41 0 30331 0
vsize: 121488
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 31391 0 0 0 47917 88 0 0 25 0 1 0 418638475 125898752 29770 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30737 29770 603 41 0 30696 0
vsize: 122948
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 31906 0 0 0 48916 90 0 0 25 0 1 0 418638475 128036864 30285 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31259 30285 603 41 0 31218 0
vsize: 125036
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 32482 0 0 0 49914 92 0 0 25 0 1 0 418638475 130351104 30861 4294967295 134512640 134672761 3221224544 3221223648 134560396 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31824 30861 603 41 0 31783 0
vsize: 127296
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 33065 0 0 0 50913 93 0 0 25 0 1 0 418638475 133181440 31444 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32515 31444 603 41 0 32474 0
vsize: 130060
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 33628 0 0 0 51912 95 0 0 25 0 1 0 418638475 135569408 32007 4294967295 134512640 134672761 3221224544 3221223648 134559896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33098 32007 603 41 0 33057 0
vsize: 132392
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 34121 0 0 0 52910 97 0 0 25 0 1 0 418638475 137596928 32500 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33593 32500 603 41 0 33552 0
vsize: 134372
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 34678 0 0 0 53909 98 0 0 25 0 1 0 418638475 139886592 33057 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34152 33057 603 41 0 34111 0
vsize: 136608
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 35220 0 0 0 54907 99 0 0 25 0 1 0 418638475 142016512 33599 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34672 33599 603 41 0 34631 0
vsize: 138688
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 35682 0 0 0 55906 100 0 0 25 0 1 0 418638475 143892480 34061 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35130 34061 603 41 0 35089 0
vsize: 140520
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 36090 0 0 0 56906 101 0 0 25 0 1 0 418638475 145641472 34469 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35557 34469 603 41 0 35516 0
vsize: 142228
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 36525 0 0 0 57904 103 0 0 25 0 1 0 418638475 147386368 34904 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35983 34904 603 41 0 35942 0
vsize: 143932
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 36968 0 0 0 58904 103 0 0 25 0 1 0 418638475 149270528 35347 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36443 35347 603 41 0 36402 0
vsize: 145772
[startup+600.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 37381 0 0 0 59902 105 0 0 25 0 1 0 418638475 150888448 35760 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36838 35760 603 41 0 36797 0
vsize: 147352
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 37799 0 0 0 60901 106 0 0 25 0 1 0 418638475 152608768 36178 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37258 36178 603 41 0 37217 0
vsize: 149032
[startup+620.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 38223 0 0 0 61900 107 0 0 25 0 1 0 418638475 154353664 36602 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37684 36602 603 41 0 37643 0
vsize: 150736
[startup+630.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 38604 0 0 0 62900 108 0 0 25 0 1 0 418638475 155836416 36983 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38046 36983 603 41 0 38005 0
vsize: 152184
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 39067 0 0 0 63898 109 0 0 25 0 1 0 418638475 157839360 37446 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38535 37446 603 41 0 38494 0
vsize: 154140
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 39476 0 0 0 64898 110 0 0 25 0 1 0 418638475 159457280 37855 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38930 37855 603 41 0 38889 0
vsize: 155720
[startup+660.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 39914 0 0 0 65897 111 0 0 25 0 1 0 418638475 161202176 38293 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39356 38293 603 41 0 39315 0
vsize: 157424
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 40630 0 0 0 66895 113 0 0 25 0 1 0 418638475 164159488 39009 4294967295 134512640 134672761 3221224544 3221223648 134560373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40078 39009 603 41 0 40037 0
vsize: 160312
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 41377 0 0 0 67893 115 0 0 25 0 1 0 418638475 167256064 39756 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40834 39756 603 41 0 40793 0
vsize: 163336
[startup+690.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 42075 0 0 0 68892 117 0 0 25 0 1 0 418638475 170086400 40454 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41525 40454 603 41 0 41484 0
vsize: 166100
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 42805 0 0 0 69890 118 0 0 25 0 1 0 418638475 173047808 41184 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42248 41184 603 41 0 42207 0
vsize: 168992
[startup+710.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 43415 0 0 0 70888 121 0 0 25 0 1 0 418638475 175484928 41794 4294967295 134512640 134672761 3221224544 3221223648 134560480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42843 41794 603 41 0 42802 0
vsize: 171372
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 44006 0 0 0 71887 122 0 0 25 0 1 0 418638475 177913856 42385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43436 42385 603 41 0 43395 0
vsize: 173744
[startup+730.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 44414 0 0 0 72887 122 0 0 25 0 1 0 418638475 179535872 42793 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43832 42793 603 41 0 43791 0
vsize: 175328
[startup+740.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 44791 0 0 0 73886 123 0 0 25 0 1 0 418638475 181161984 43170 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44229 43170 603 41 0 44188 0
vsize: 176916
[startup+750.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45165 0 0 0 74885 124 0 0 25 0 1 0 418638475 182640640 43544 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44590 43544 603 41 0 44549 0
vsize: 178360
[startup+760.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45552 0 0 0 75884 125 0 0 25 0 1 0 418638475 184287232 43931 4294967295 134512640 134672761 3221224544 3221223648 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44992 43931 603 41 0 44951 0
vsize: 179968
[startup+770.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45854 0 0 0 76884 126 0 0 25 0 1 0 418638475 185503744 44233 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44233 603 41 0 45248 0
vsize: 181156
[startup+780.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45854 0 0 0 77884 126 0 0 25 0 1 0 418638475 185503744 44233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44233 603 41 0 45248 0
vsize: 181156
[startup+790.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45854 0 0 0 78884 126 0 0 25 0 1 0 418638475 185503744 44233 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44233 603 41 0 45248 0
vsize: 181156
[startup+800.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45854 0 0 0 79884 126 0 0 25 0 1 0 418638475 185503744 44233 4294967295 134512640 134672761 3221224544 3221223648 134560393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44233 603 41 0 45248 0
vsize: 181156
[startup+810.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45854 0 0 0 80884 126 0 0 25 0 1 0 418638475 185503744 44233 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44233 603 41 0 45248 0
vsize: 181156
[startup+820.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45854 0 0 0 81884 126 0 0 25 0 1 0 418638475 185503744 44233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44233 603 41 0 45248 0
vsize: 181156
[startup+830.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45854 0 0 0 82884 126 0 0 25 0 1 0 418638475 185503744 44233 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44233 603 41 0 45248 0
vsize: 181156
[startup+840.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45854 0 0 0 83884 127 0 0 25 0 1 0 418638475 185503744 44233 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44233 603 41 0 45248 0
vsize: 181156
[startup+850.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45854 0 0 0 84884 127 0 0 25 0 1 0 418638475 185503744 44233 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44233 603 41 0 45248 0
vsize: 181156
[startup+860.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45854 0 0 0 85884 127 0 0 25 0 1 0 418638475 185503744 44233 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44233 603 41 0 45248 0
vsize: 181156
[startup+870.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45854 0 0 0 86884 127 0 0 25 0 1 0 418638475 185503744 44233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44233 603 41 0 45248 0
vsize: 181156
[startup+880.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45854 0 0 0 87884 127 0 0 25 0 1 0 418638475 185503744 44233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44233 603 41 0 45248 0
vsize: 181156
[startup+890.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45854 0 0 0 88884 127 0 0 25 0 1 0 418638475 185503744 44233 4294967295 134512640 134672761 3221224544 3221223648 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44233 603 41 0 45248 0
vsize: 181156
[startup+900.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45854 0 0 0 89884 127 0 0 25 0 1 0 418638475 185503744 44233 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44233 603 41 0 45248 0
vsize: 181156
[startup+910.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45855 0 0 0 90884 127 0 0 25 0 1 0 418638475 185503744 44234 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44234 603 41 0 45248 0
vsize: 181156
[startup+920.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45855 0 0 0 91884 128 0 0 25 0 1 0 418638475 185503744 44234 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44234 603 41 0 45248 0
vsize: 181156
[startup+930.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45855 0 0 0 92884 128 0 0 25 0 1 0 418638475 185503744 44234 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44234 603 41 0 45248 0
vsize: 181156
[startup+940.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45857 0 0 0 93884 128 0 0 25 0 1 0 418638475 185503744 44236 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44236 603 41 0 45248 0
vsize: 181156
[startup+950.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45858 0 0 0 94884 128 0 0 25 0 1 0 418638475 185503744 44237 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44237 603 41 0 45248 0
vsize: 181156
[startup+960.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45858 0 0 0 95885 128 0 0 25 0 1 0 418638475 185503744 44237 4294967295 134512640 134672761 3221224544 3221223648 134560177 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44237 603 41 0 45248 0
vsize: 181156
[startup+970.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45858 0 0 0 96885 128 0 0 25 0 1 0 418638475 185503744 44237 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44237 603 41 0 45248 0
vsize: 181156
[startup+980.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45858 0 0 0 97885 128 0 0 25 0 1 0 418638475 185503744 44237 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44237 603 41 0 45248 0
vsize: 181156
[startup+990.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45858 0 0 0 98885 128 0 0 25 0 1 0 418638475 185503744 44237 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44237 603 41 0 45248 0
vsize: 181156
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45858 0 0 0 99885 128 0 0 25 0 1 0 418638475 185503744 44237 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44237 603 41 0 45248 0
vsize: 181156
[startup+1010.02 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45859 0 0 0 100885 128 0 0 25 0 1 0 418638475 185503744 44238 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44238 603 41 0 45248 0
vsize: 181156
[startup+1020.02 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45859 0 0 0 101885 128 0 0 25 0 1 0 418638475 185503744 44238 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44238 603 41 0 45248 0
vsize: 181156
[startup+1030.01 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45859 0 0 0 102885 128 0 0 25 0 1 0 418638475 185503744 44238 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44238 603 41 0 45248 0
vsize: 181156
[startup+1040.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45859 0 0 0 103885 128 0 0 25 0 1 0 418638475 185503744 44238 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44238 603 41 0 45248 0
vsize: 181156
[startup+1050.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45859 0 0 0 104885 128 0 0 25 0 1 0 418638475 185503744 44238 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44238 603 41 0 45248 0
vsize: 181156
[startup+1060.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45859 0 0 0 105885 129 0 0 25 0 1 0 418638475 185503744 44238 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44238 603 41 0 45248 0
vsize: 181156
[startup+1070.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45859 0 0 0 106885 129 0 0 25 0 1 0 418638475 185503744 44238 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44238 603 41 0 45248 0
vsize: 181156
[startup+1080.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45860 0 0 0 107886 129 0 0 25 0 1 0 418638475 185503744 44239 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44239 603 41 0 45248 0
vsize: 181156
[startup+1090.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45860 0 0 0 108886 129 0 0 25 0 1 0 418638475 185503744 44239 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44239 603 41 0 45248 0
vsize: 181156
[startup+1100.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45860 0 0 0 109885 129 0 0 25 0 1 0 418638475 185503744 44239 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44239 603 41 0 45248 0
vsize: 181156
[startup+1110.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45860 0 0 0 110886 129 0 0 25 0 1 0 418638475 185503744 44239 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44239 603 41 0 45248 0
vsize: 181156
[startup+1120.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45860 0 0 0 111886 129 0 0 25 0 1 0 418638475 185503744 44239 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44239 603 41 0 45248 0
vsize: 181156
[startup+1130.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45861 0 0 0 112886 129 0 0 25 0 1 0 418638475 185503744 44240 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44240 603 41 0 45248 0
vsize: 181156
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45861 0 0 0 113885 130 0 0 25 0 1 0 418638475 185503744 44240 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44240 603 41 0 45248 0
vsize: 181156
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45861 0 0 0 114886 130 0 0 25 0 1 0 418638475 185503744 44240 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44240 603 41 0 45248 0
vsize: 181156
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45861 0 0 0 115886 130 0 0 25 0 1 0 418638475 185503744 44240 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44240 603 41 0 45248 0
vsize: 181156
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45861 0 0 0 116886 130 0 0 25 0 1 0 418638475 185503744 44240 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44240 603 41 0 45248 0
vsize: 181156
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45861 0 0 0 117886 130 0 0 25 0 1 0 418638475 185503744 44240 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44240 603 41 0 45248 0
vsize: 181156
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45861 0 0 0 118886 130 0 0 25 0 1 0 418638475 185503744 44240 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44240 603 41 0 45248 0
vsize: 181156
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 32635
Raw data (stat): 32635 (minisat+) R 32634 30927 30926 0 -1 0 45861 0 0 0 119886 130 0 0 25 0 1 0 418638475 185503744 44240 4294967295 134512640 134672761 3221224544 3221223648 134560184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45289 44240 603 41 0 45248 0
vsize: 181156
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.91 1/55 32635
Raw data (stat): 32635 (minisat+) Z 32634 30927 30926 0 -1 12 45864 0 0 0 119886 138 0 0 25 0 1 0 418638475 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.11
CPU time (s): 1200.25
CPU user time (s): 1198.87
CPU system time (s): 1.38779
CPU usage (%): 100.012
Max. virtual memory (Kb): 181156
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####