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 17853

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-21 12:24:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18966 boxname=wulflinc27 idbench=1459 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  69e7430fb77e7d40f128bdde5f7776a3  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-bal8x12.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-bal8x12.opb /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-bal8x12.opb
IDLAUNCH: 18966
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        754024 kB
Buffers:         21980 kB
Cached:         234140 kB
SwapCached:        512 kB
Active:          16888 kB
Inactive:       241260 kB
HighTotal:      131008 kB
HighFree:        46004 kB
LowTotal:       903652 kB
LowFree:        708020 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5104 kB
Slab:            16804 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 12:44:57 (client local time) WITH STATUS 10 IN 1200.29 SECONDS
stats: 18966 7 1200.29 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]---> BDD-cost: 1586
c ---[ 132]---> BDD-cost: 1693
c ---[ 130]---> BDD-cost: 1884
c ---[ 128]---> BDD-cost: 1823
c ---[ 126]---> BDD-cost: 1741
c ---[ 124]---> BDD-cost: 1823
c ---[ 122]---> BDD-cost: 1497
c ---[ 120]---> BDD-cost: 1741
c ---[ 118]---> BDD-cost:  812
c ---[ 116]---> BDD-cost:  758
c ---[ 114]---> BDD-cost:  724
c ---[ 112]---> BDD-cost:  632
c ---[ 110]---> BDD-cost:  812
c ---[ 108]---> BDD-cost:  758
c ---[ 106]---> BDD-cost:  632
c ---[ 104]---> BDD-cost:  812
c ---[ 102]---> BDD-cost:  846
c ---[ 100]---> BDD-cost:  724
c ---[  98]---> BDD-cost:  873
c ---[  96]---> BDD-cost:  835
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 |   67031   193065 |   22343       0        0     nan |  0.000 % |
c |       100 |   67031   193065 |   24577     100     7580    75.8 |  3.782 % |
c ==============================================================================
c [1mFound solution: 26274564[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:430544     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       167 | 1268020  2995934 |  422673     167     8692    52.0 |  3.782 % |
c |       267 | 1268020  2995934 |  464940     267    10587    39.7 |  0.218 % |
c |       417 | 1268020  2995934 |  511434     417    11726    28.1 |  0.218 % |
c |       643 | 1268020  2995934 |  562577     643    14006    21.8 |  0.218 % |
c |       980 | 1266506  2992498 |  618835     964    18105    18.8 |  0.315 % |
c |      1486 | 1266470  2992417 |  680719    1468    26929    18.3 |  0.317 % |
c |      2245 | 1266458  2992390 |  748791    2226    33345    15.0 |  0.318 % |
c |      3384 | 1266458  2992390 |  823670    3365    56771    16.9 |  0.318 % |
c ==============================================================================
c [1mFound solution: 23713400[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4063 | 1267686  2998300 |  422562    4044    69267    17.1 |  0.318 % |
c |      4163 | 1267686  2998300 |  464818    4144    70081    16.9 |  0.317 % |
c |      4313 | 1267686  2998300 |  511300    4294    70717    16.5 |  0.317 % |
c |      4539 | 1267686  2998300 |  562430    4520    73691    16.3 |  0.317 % |
c ==============================================================================
c [1mFound solution: 19846589[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4875 | 1267752  2998726 |  422584    4855    76953    15.9 |  0.317 % |
c |      4975 | 1267570  2998316 |  464842    4952    82595    16.7 |  0.336 % |
c |      5125 | 1267383  2997893 |  511326    5098    84364    16.5 |  0.348 % |
c |      5350 | 1267280  2997659 |  562459    5319    86007    16.2 |  0.354 % |
c |      5687 | 1267280  2997659 |  618705    5656    93177    16.5 |  0.354 % |
c |      6193 | 1267280  2997659 |  680575    6162   116483    18.9 |  0.354 % |
c |      6953 | 1267280  2997659 |  748633    6922   122290    17.7 |  0.354 % |
c |      8093 | 1267280  2997659 |  823496    8062   173797    21.6 |  0.354 % |
c |      9801 | 1267280  2997659 |  905846    9770   270977    27.7 |  0.354 % |
c |     12364 | 1267280  2997659 |  996430   12333   300756    24.4 |  0.354 % |
c |     16209 | 1267171  2997411 | 1096074   16175   408784    25.3 |  0.361 % |
c |     21976 | 1265026  2992496 | 1205681   21855  2703738   123.7 |  0.508 % |
c |     30625 | 1264942  2992303 | 1326249   30503  2932701    96.1 |  0.513 % |
c |     43601 | 1264646  2991629 | 1458874   43471  3606968    83.0 |  0.533 % |
c |     63062 | 1264646  2991629 | 1604762   62932  3989012    63.4 |  0.533 % |
c |     92254 | 1264202  2990611 | 1765238   92117 12753288   138.4 |  0.563 % |
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 Y73_bit0 Y74_bit0 -Y75_bit0 -Y76_bit0 Y77_bit0 Y78_bit0 -Y79_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.81 0.93 0.90 2/54 19599
Raw data (stat): 19599 (runsolver) R 19598 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545057093 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.0003 s]
Raw data (loadavg): 0.84 0.93 0.90 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 34490 0 0 0 911 87 0 0 25 0 1 0 545057093 150732800 33163 4294967295 134512640 134672761 3221224528 3221186096 134527347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36800 33163 603 41 0 36759 0
vsize: 147200
[startup+20.0007 s]
Raw data (loadavg): 0.86 0.93 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 36421 0 0 0 1907 92 0 0 25 0 1 0 545057093 156815360 35094 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38285 35094 603 41 0 38244 0
vsize: 153140
[startup+30.0009 s]
Raw data (loadavg): 0.88 0.93 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 36467 0 0 0 2907 92 0 0 25 0 1 0 545057093 156950528 35140 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38318 35140 603 41 0 38277 0
vsize: 153272
[startup+40.0018 s]
Raw data (loadavg): 0.90 0.93 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 36590 0 0 0 3906 93 0 0 25 0 1 0 545057093 157220864 35263 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38384 35263 603 41 0 38343 0
vsize: 153536
[startup+50.0022 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 37264 0 0 0 4905 94 0 0 25 0 1 0 545057093 160710656 35886 4294967295 134512640 134672761 3221224528 3221223652 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39236 35886 603 41 0 39195 0
vsize: 156944
[startup+60.0023 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 37400 0 0 0 5904 95 0 0 25 0 1 0 545057093 160854016 35949 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39271 35949 603 41 0 39230 0
vsize: 157084
[startup+70.0033 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 37400 0 0 0 6904 95 0 0 25 0 1 0 545057093 160854016 35949 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39271 35949 603 41 0 39230 0
vsize: 157084
[startup+80.0037 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 37421 0 0 0 7904 95 0 0 25 0 1 0 545057093 160985088 35970 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39303 35970 603 41 0 39262 0
vsize: 157212
[startup+90.0049 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 37428 0 0 0 8904 96 0 0 25 0 1 0 545057093 160985088 35977 4294967295 134512640 134672761 3221224528 3221223664 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39303 35977 603 41 0 39262 0
vsize: 157212
[startup+100.006 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 37443 0 0 0 9904 96 0 0 25 0 1 0 545057093 161120256 35992 4294967295 134512640 134672761 3221224528 3221223712 134558654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39336 35992 603 41 0 39295 0
vsize: 157344
[startup+110.006 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 37452 0 0 0 10904 96 0 0 25 0 1 0 545057093 161120256 36001 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39336 36001 603 41 0 39295 0
vsize: 157344
[startup+120.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 37472 0 0 0 11904 96 0 0 25 0 1 0 545057093 161255424 36021 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39369 36021 603 41 0 39328 0
vsize: 157476
[startup+130.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 37489 0 0 0 12904 96 0 0 25 0 1 0 545057093 161255424 36038 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39369 36038 603 41 0 39328 0
vsize: 157476
[startup+140.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 37589 0 0 0 13903 97 0 0 25 0 1 0 545057093 161693696 36138 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39476 36138 603 41 0 39435 0
vsize: 157904
[startup+150.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 37680 0 0 0 14903 98 0 0 25 0 1 0 545057093 162095104 36229 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39574 36229 603 41 0 39533 0
vsize: 158296
[startup+160.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 37704 0 0 0 15902 98 0 0 25 0 1 0 545057093 162226176 36253 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39606 36253 603 41 0 39565 0
vsize: 158424
[startup+170.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 37738 0 0 0 16902 98 0 0 25 0 1 0 545057093 162361344 36287 4294967295 134512640 134672761 3221224528 3221223696 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39639 36287 603 41 0 39598 0
vsize: 158556
[startup+180.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 37786 0 0 0 17902 99 0 0 25 0 1 0 545057093 162496512 36335 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39672 36335 603 41 0 39631 0
vsize: 158688
[startup+190.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 37902 0 0 0 18902 99 0 0 25 0 1 0 545057093 163016704 36451 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39799 36451 603 41 0 39758 0
vsize: 159196
[startup+200.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 38145 0 0 0 19902 99 0 0 25 0 1 0 545057093 164065280 36694 4294967295 134512640 134672761 3221224528 3221223632 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40055 36694 603 41 0 40014 0
vsize: 160220
[startup+210.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 38366 0 0 0 20902 100 0 0 25 0 1 0 545057093 164868096 36915 4294967295 134512640 134672761 3221224528 3221223712 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40251 36915 603 41 0 40210 0
vsize: 161004
[startup+220.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 38622 0 0 0 21901 100 0 0 25 0 1 0 545057093 165957632 37171 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40517 37171 603 41 0 40476 0
vsize: 162068
[startup+230.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 38762 0 0 0 22901 101 0 0 25 0 1 0 545057093 166621184 37311 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40679 37311 603 41 0 40638 0
vsize: 162716
[startup+240.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 38871 0 0 0 23901 101 0 0 25 0 1 0 545057093 167022592 37420 4294967295 134512640 134672761 3221224528 3221223680 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40777 37420 603 41 0 40736 0
vsize: 163108
[startup+250.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 39179 0 0 0 24900 102 0 0 25 0 1 0 545057093 168243200 37728 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41075 37728 603 41 0 41034 0
vsize: 164300
[startup+260.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 39622 0 0 0 25899 103 0 0 25 0 1 0 545057093 170123264 38171 4294967295 134512640 134672761 3221224528 3221223632 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41534 38171 603 41 0 41493 0
vsize: 166136
[startup+270.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 39804 0 0 0 26899 104 0 0 25 0 1 0 545057093 170799104 38337 4294967295 134512640 134672761 3221224528 3221223672 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41699 38337 603 41 0 41658 0
vsize: 166796
[startup+280.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 39804 0 0 0 27899 104 0 0 25 0 1 0 545057093 170799104 38337 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41699 38337 603 41 0 41658 0
vsize: 166796
[startup+290.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 39895 0 0 0 28899 104 0 0 25 0 1 0 545057093 171196416 38428 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41796 38428 603 41 0 41755 0
vsize: 167184
[startup+300.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 40049 0 0 0 29898 105 0 0 25 0 1 0 545057093 171864064 38582 4294967295 134512640 134672761 3221224528 3221223664 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41959 38582 603 41 0 41918 0
vsize: 167836
[startup+310.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 40149 0 0 0 30898 105 0 0 25 0 1 0 545057093 172261376 38682 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42056 38682 603 41 0 42015 0
vsize: 168224
[startup+320.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 40209 0 0 0 31898 105 0 0 25 0 1 0 545057093 172527616 38742 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42121 38742 603 41 0 42080 0
vsize: 168484
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 40225 0 0 0 32898 105 0 0 25 0 1 0 545057093 172527616 38758 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42121 38758 603 41 0 42080 0
vsize: 168484
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 40237 0 0 0 33898 105 0 0 25 0 1 0 545057093 172658688 38770 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42153 38770 603 41 0 42112 0
vsize: 168612
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 40256 0 0 0 34898 105 0 0 25 0 1 0 545057093 172658688 38789 4294967295 134512640 134672761 3221224528 3221223712 134558360 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42153 38789 603 41 0 42112 0
vsize: 168612
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 40279 0 0 0 35898 105 0 0 25 0 1 0 545057093 172789760 38812 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42185 38812 603 41 0 42144 0
vsize: 168740
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 40302 0 0 0 36898 105 0 0 25 0 1 0 545057093 172924928 38835 4294967295 134512640 134672761 3221224528 3221223696 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42218 38835 603 41 0 42177 0
vsize: 168872
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 40324 0 0 0 37898 105 0 0 25 0 1 0 545057093 172924928 38857 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42218 38857 603 41 0 42177 0
vsize: 168872
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 40355 0 0 0 38899 105 0 0 25 0 1 0 545057093 173056000 38888 4294967295 134512640 134672761 3221224528 3221223664 134560625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42250 38888 603 41 0 42209 0
vsize: 169000
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 40391 0 0 0 39899 105 0 0 25 0 1 0 545057093 173191168 38924 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42283 38924 603 41 0 42242 0
vsize: 169132
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 40431 0 0 0 40899 105 0 0 25 0 1 0 545057093 173322240 38964 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42315 38964 603 41 0 42274 0
vsize: 169260
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 40581 0 0 0 41899 106 0 0 25 0 1 0 545057093 174116864 39114 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42509 39114 603 41 0 42468 0
vsize: 170036
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 40654 0 0 0 42899 106 0 0 25 0 1 0 545057093 174387200 39187 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42575 39187 603 41 0 42534 0
vsize: 170300
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 40854 0 0 0 43899 106 0 0 25 0 1 0 545057093 175210496 39387 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42776 39387 603 41 0 42735 0
vsize: 171104
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 40888 0 0 0 44898 107 0 0 25 0 1 0 545057093 175353856 39421 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42811 39421 603 41 0 42770 0
vsize: 171244
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 40927 0 0 0 45898 107 0 0 25 0 1 0 545057093 175489024 39460 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42844 39460 603 41 0 42803 0
vsize: 171376
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 40962 0 0 0 46899 107 0 0 25 0 1 0 545057093 175624192 39495 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42877 39495 603 41 0 42836 0
vsize: 171508
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 40989 0 0 0 47899 107 0 0 25 0 1 0 545057093 175759360 39522 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42910 39522 603 41 0 42869 0
vsize: 171640
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 41010 0 0 0 48898 107 0 0 25 0 1 0 545057093 175894528 39543 4294967295 134512640 134672761 3221224528 3221223664 134560560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42943 39543 603 41 0 42902 0
vsize: 171772
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 41030 0 0 0 49898 108 0 0 25 0 1 0 545057093 175894528 39563 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42943 39563 603 41 0 42902 0
vsize: 171772
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 41049 0 0 0 50898 108 0 0 25 0 1 0 545057093 176029696 39582 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42976 39582 603 41 0 42935 0
vsize: 171904
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 41096 0 0 0 51899 108 0 0 25 0 1 0 545057093 176164864 39629 4294967295 134512640 134672761 3221224528 3221223664 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43009 39629 603 41 0 42968 0
vsize: 172036
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 41139 0 0 0 52899 108 0 0 25 0 1 0 545057093 176431104 39672 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43074 39672 603 41 0 43033 0
vsize: 172296
[startup+540.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 41175 0 0 0 53899 108 0 0 25 0 1 0 545057093 176566272 39708 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43107 39708 603 41 0 43066 0
vsize: 172428
[startup+550.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 41250 0 0 0 54898 109 0 0 25 0 1 0 545057093 176832512 39783 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43172 39783 603 41 0 43131 0
vsize: 172688
[startup+560.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 41350 0 0 0 55898 109 0 0 25 0 1 0 545057093 177238016 39883 4294967295 134512640 134672761 3221224528 3221223696 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43271 39883 603 41 0 43230 0
vsize: 173084
[startup+570.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 41408 0 0 0 56898 109 0 0 25 0 1 0 545057093 177373184 39941 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43304 39941 603 41 0 43263 0
vsize: 173216
[startup+580.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 41453 0 0 0 57898 109 0 0 25 0 1 0 545057093 177643520 39986 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43370 39986 603 41 0 43329 0
vsize: 173480
[startup+590.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 41496 0 0 0 58898 109 0 0 25 0 1 0 545057093 177778688 40029 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43403 40029 603 41 0 43362 0
vsize: 173612
[startup+600.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 41573 0 0 0 59898 110 0 0 25 0 1 0 545057093 178040832 40106 4294967295 134512640 134672761 3221224528 3221223712 134559033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43467 40106 603 41 0 43426 0
vsize: 173868
[startup+610.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 41642 0 0 0 60898 110 0 0 25 0 1 0 545057093 178307072 40175 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43532 40175 603 41 0 43491 0
vsize: 174128
[startup+620.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 41777 0 0 0 61898 110 0 0 25 0 1 0 545057093 178843648 40310 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43663 40310 603 41 0 43622 0
vsize: 174652
[startup+630.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 41864 0 0 0 62898 110 0 0 25 0 1 0 545057093 179511296 40397 4294967295 134512640 134672761 3221224528 3221223712 134558380 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43826 40397 603 41 0 43785 0
vsize: 175304
[startup+640.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 41895 0 0 0 63898 111 0 0 25 0 1 0 545057093 179646464 40428 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43859 40428 603 41 0 43818 0
vsize: 175436
[startup+650.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 41939 0 0 0 64898 111 0 0 25 0 1 0 545057093 179777536 40472 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43891 40472 603 41 0 43850 0
vsize: 175564
[startup+660.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 41984 0 0 0 65898 111 0 0 25 0 1 0 545057093 180047872 40517 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43957 40517 603 41 0 43916 0
vsize: 175828
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 42053 0 0 0 66898 111 0 0 25 0 1 0 545057093 180314112 40586 4294967295 134512640 134672761 3221224528 3221223664 134560606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44022 40586 603 41 0 43981 0
vsize: 176088
[startup+680.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 42097 0 0 0 67898 111 0 0 25 0 1 0 545057093 180449280 40630 4294967295 134512640 134672761 3221224528 3221223696 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44055 40630 603 41 0 44014 0
vsize: 176220
[startup+690.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 42236 0 0 0 68898 112 0 0 25 0 1 0 545057093 180989952 40769 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44187 40769 603 41 0 44146 0
vsize: 176748
[startup+700.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 42503 0 0 0 69897 113 0 0 25 0 1 0 545057093 182059008 41036 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44448 41036 603 41 0 44407 0
vsize: 177792
[startup+710.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 42605 0 0 0 70897 113 0 0 25 0 1 0 545057093 182456320 41138 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44545 41138 603 41 0 44504 0
vsize: 178180
[startup+720.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 42762 0 0 0 71897 113 0 0 25 0 1 0 545057093 183087104 41295 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44699 41295 603 41 0 44658 0
vsize: 178796
[startup+730.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 42874 0 0 0 72897 114 0 0 25 0 1 0 545057093 183635968 41407 4294967295 134512640 134672761 3221224528 3221223696 134560808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44833 41407 603 41 0 44792 0
vsize: 179332
[startup+740.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 42987 0 0 0 73896 114 0 0 25 0 1 0 545057093 184025088 41520 4294967295 134512640 134672761 3221224528 3221223664 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44928 41520 603 41 0 44887 0
vsize: 179712
[startup+750.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 43164 0 0 0 74896 115 0 0 25 0 1 0 545057093 184709120 41697 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45095 41697 603 41 0 45054 0
vsize: 180380
[startup+760.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 43348 0 0 0 75896 115 0 0 25 0 1 0 545057093 185540608 41881 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45298 41881 603 41 0 45257 0
vsize: 181192
[startup+770.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 43614 0 0 0 76896 115 0 0 25 0 1 0 545057093 186630144 42147 4294967295 134512640 134672761 3221224528 3221223632 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45564 42147 603 41 0 45523 0
vsize: 182256
[startup+780.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 43808 0 0 0 77895 116 0 0 25 0 1 0 545057093 187473920 42341 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45770 42341 603 41 0 45729 0
vsize: 183080
[startup+790.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 44043 0 0 0 78895 116 0 0 25 0 1 0 545057093 188375040 42576 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45990 42576 603 41 0 45949 0
vsize: 183960
[startup+800.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 44319 0 0 0 79895 117 0 0 25 0 1 0 545057093 189423616 42852 4294967295 134512640 134672761 3221224528 3221223632 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46246 42852 603 41 0 46205 0
vsize: 184984
[startup+810.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 44573 0 0 0 80894 117 0 0 25 0 1 0 545057093 190521344 43106 4294967295 134512640 134672761 3221224528 3221223696 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46514 43106 603 41 0 46473 0
vsize: 186056
[startup+820.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 44875 0 0 0 81894 118 0 0 25 0 1 0 545057093 191774720 43408 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46820 43408 603 41 0 46779 0
vsize: 187280
[startup+830.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 45194 0 0 0 82894 118 0 0 25 0 1 0 545057093 193040384 43727 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47129 43727 603 41 0 47088 0
vsize: 188516
[startup+840.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 45512 0 0 0 83893 119 0 0 25 0 1 0 545057093 194347008 44045 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47448 44045 603 41 0 47407 0
vsize: 189792
[startup+850.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 45814 0 0 0 84893 120 0 0 25 0 1 0 545057093 195584000 44347 4294967295 134512640 134672761 3221224528 3221223632 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47750 44347 603 41 0 47709 0
vsize: 191000
[startup+860.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 46089 0 0 0 85892 121 0 0 25 0 1 0 545057093 196759552 44622 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48037 44622 603 41 0 47996 0
vsize: 192148
[startup+870.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 46393 0 0 0 86892 121 0 0 25 0 1 0 545057093 197988352 44926 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48337 44926 603 41 0 48296 0
vsize: 193348
[startup+880.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 46665 0 0 0 87892 121 0 0 25 0 1 0 545057093 199090176 45198 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48606 45198 603 41 0 48565 0
vsize: 194424
[startup+890.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 46947 0 0 0 88891 122 0 0 25 0 1 0 545057093 200224768 45480 4294967295 134512640 134672761 3221224528 3221223632 134560005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48883 45480 603 41 0 48842 0
vsize: 195532
[startup+900.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 47216 0 0 0 89891 123 0 0 25 0 1 0 545057093 201326592 45749 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49152 45749 603 41 0 49111 0
vsize: 196608
[startup+910.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 47450 0 0 0 90891 123 0 0 25 0 1 0 545057093 202276864 45983 4294967295 134512640 134672761 3221224528 3221223632 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49384 45983 603 41 0 49343 0
vsize: 197536
[startup+920.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 47746 0 0 0 91890 124 0 0 25 0 1 0 545057093 203448320 46279 4294967295 134512640 134672761 3221224528 3221223632 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49670 46279 603 41 0 49629 0
vsize: 198680
[startup+930.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 48060 0 0 0 92889 125 0 0 25 0 1 0 545057093 204845056 46593 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50011 46593 603 41 0 49970 0
vsize: 200044
[startup+940.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 48348 0 0 0 93889 125 0 0 25 0 1 0 545057093 205975552 46881 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50287 46881 603 41 0 50246 0
vsize: 201148
[startup+950.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 48640 0 0 0 94888 126 0 0 25 0 1 0 545057093 207126528 47173 4294967295 134512640 134672761 3221224528 3221223632 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50568 47173 603 41 0 50527 0
vsize: 202272
[startup+960.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 48922 0 0 0 95888 127 0 0 25 0 1 0 545057093 208281600 47455 4294967295 134512640 134672761 3221224528 3221223712 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50850 47455 603 41 0 50809 0
vsize: 203400
[startup+970.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 49224 0 0 0 96887 128 0 0 25 0 1 0 545057093 209559552 47757 4294967295 134512640 134672761 3221224528 3221223632 134560226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51162 47757 603 41 0 51121 0
vsize: 204648
[startup+980.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 49536 0 0 0 97886 128 0 0 25 0 1 0 545057093 210788352 48069 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51462 48069 603 41 0 51421 0
vsize: 205848
[startup+990.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 49819 0 0 0 98886 129 0 0 25 0 1 0 545057093 212049920 48352 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51770 48352 603 41 0 51729 0
vsize: 207080
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 50145 0 0 0 99885 130 0 0 25 0 1 0 545057093 213336064 48678 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52084 48678 603 41 0 52043 0
vsize: 208336
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 50414 0 0 0 100885 131 0 0 25 0 1 0 545057093 214413312 48947 4294967295 134512640 134672761 3221224528 3221223632 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52347 48947 603 41 0 52306 0
vsize: 209388
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 50541 0 0 0 101884 131 0 0 25 0 1 0 545057093 214953984 49074 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52479 49074 603 41 0 52438 0
vsize: 209916
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 50556 0 0 0 102883 131 0 0 25 0 1 0 545057093 214953984 49089 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52479 49089 603 41 0 52438 0
vsize: 209916
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 50584 0 0 0 103884 131 0 0 25 0 1 0 545057093 215089152 49117 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52512 49117 603 41 0 52471 0
vsize: 210048
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 50630 0 0 0 104884 131 0 0 25 0 1 0 545057093 215347200 49163 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52575 49163 603 41 0 52534 0
vsize: 210300
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 50661 0 0 0 105884 132 0 0 25 0 1 0 545057093 215482368 49194 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52608 49194 603 41 0 52567 0
vsize: 210432
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 50693 0 0 0 106884 132 0 0 25 0 1 0 545057093 215613440 49226 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52640 49226 603 41 0 52599 0
vsize: 210560
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 50708 0 0 0 107883 132 0 0 25 0 1 0 545057093 215613440 49241 4294967295 134512640 134672761 3221224528 3221223700 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52640 49241 603 41 0 52599 0
vsize: 210560
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 50720 0 0 0 108883 132 0 0 25 0 1 0 545057093 215613440 49253 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52640 49253 603 41 0 52599 0
vsize: 210560
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 50761 0 0 0 109883 133 0 0 25 0 1 0 545057093 215879680 49294 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52705 49294 603 41 0 52664 0
vsize: 210820
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 50787 0 0 0 110883 133 0 0 25 0 1 0 545057093 215879680 49320 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52705 49320 603 41 0 52664 0
vsize: 210820
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 50851 0 0 0 111883 133 0 0 25 0 1 0 545057093 216145920 49384 4294967295 134512640 134672761 3221224528 3221223664 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52770 49384 603 41 0 52729 0
vsize: 211080
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 51047 0 0 0 112882 134 0 0 25 0 1 0 545057093 216944640 49580 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52965 49580 603 41 0 52924 0
vsize: 211860
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 51259 0 0 0 113881 135 0 0 25 0 1 0 545057093 217886720 49792 4294967295 134512640 134672761 3221224528 3221223664 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53195 49792 603 41 0 53154 0
vsize: 212780
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 51361 0 0 0 114882 135 0 0 25 0 1 0 545057093 218284032 49894 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53292 49894 603 41 0 53251 0
vsize: 213168
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 51404 0 0 0 115882 135 0 0 25 0 1 0 545057093 218406912 49937 4294967295 134512640 134672761 3221224528 3221223632 134560250 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53322 49937 603 41 0 53281 0
vsize: 213288
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 51432 0 0 0 116882 135 0 0 25 0 1 0 545057093 218550272 49965 4294967295 134512640 134672761 3221224528 3221223632 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53357 49965 603 41 0 53316 0
vsize: 213428
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 51471 0 0 0 117882 135 0 0 25 0 1 0 545057093 218689536 50004 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53391 50004 603 41 0 53350 0
vsize: 213564
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 51578 0 0 0 118882 136 0 0 25 0 1 0 545057093 219197440 50111 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53515 50111 603 41 0 53474 0
vsize: 214060
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19599
Raw data (stat): 19599 (minisat+) R 19598 18865 18864 0 -1 0 51692 0 0 0 119882 136 0 0 25 0 1 0 545057093 219607040 50225 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53615 50225 603 41 0 53574 0
vsize: 214460
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 19599
Raw data (stat): 19599 (minisat+) Z 19598 18865 18864 0 -1 12 51695 0 0 0 119882 146 0 0 25 0 1 0 545057093 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.14
CPU time (s): 1200.29
CPU user time (s): 1198.83
CPU system time (s): 1.46178
CPU usage (%): 100.012
Max. virtual memory (Kb): 214460
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####