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-ran10x10a.opb
MD5SUM	133d42fd76e8bbd92509939943f41498
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	398336
Optimality of the best value was proved	NO
Number of terms in the objective function	2100
Biggest coefficient in the objective function	4718592
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	539671039
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	4718592
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	539671039
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	913.784
Number of variables	2100
Total number of constraints	120
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	120
Minimum length of a constraint	21
Maximum length of a constraint	200
Trace number 17728

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-21 11:42:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19200 boxname=wulflinc25 idbench=1477 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  133d42fd76e8bbd92509939943f41498  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-ran10x10a.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-ran10x10a.opb /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-ran10x10a.opb
IDLAUNCH: 19200
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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.220
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        818592 kB
Buffers:         18004 kB
Cached:         177448 kB
SwapCached:        728 kB
Active:          65644 kB
Inactive:       131784 kB
HighTotal:      131008 kB
HighFree:        67564 kB
LowTotal:       903652 kB
LowFree:        751028 kB
SwapTotal:     2097892 kB
SwapFree:      2096220 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           4992 kB
Slab:            12976 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 12:02:37 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 19200 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 138]---> BDD-cost:  979
c ---[ 136]---> BDD-cost:  891
c ---[ 134]---> BDD-cost:  979
c ---[ 132]---> BDD-cost: 1039
c ---[ 130]---> BDD-cost: 1091
c ---[ 128]---> BDD-cost: 1066
c ---[ 126]---> BDD-cost: 1097
c ---[ 124]---> BDD-cost: 1147
c ---[ 122]---> BDD-cost:  958
c ---[ 120]---> BDD-cost: 1116
c ---[ 118]---> BDD-cost:  895
c ---[ 116]---> BDD-cost: 1032
c ---[ 114]---> BDD-cost: 1155
c ---[ 112]---> BDD-cost: 1124
c ---[ 110]---> BDD-cost: 1105
c ---[ 108]---> BDD-cost:  750
c ---[ 106]---> BDD-cost:  817
c ---[ 104]---> BDD-cost:  983
c ---[ 102]---> BDD-cost: 1124
c ---[ 100]---> BDD-cost: 1157
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:   13
c ---[  97]---> BDD-cost:   11
c ---[  96]---> BDD-cost:   11
c ---[  95]---> BDD-cost:   11
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   10
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   11
c ---[  89]---> BDD-cost:   11
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   13
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   13
c ---[  83]---> BDD-cost:   13
c ---[  82]---> BDD-cost:   13
c ---[  81]---> BDD-cost:   10
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   13
c ---[  78]---> BDD-cost:   13
c ---[  77]---> BDD-cost:   13
c ---[  76]---> BDD-cost:   13
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   12
c ---[  73]---> BDD-cost:   15
c ---[  72]---> BDD-cost:   15
c ---[  71]---> BDD-cost:   15
c ---[  70]---> BDD-cost:   10
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:   13
c ---[  67]---> BDD-cost:   15
c ---[  66]---> BDD-cost:   15
c ---[  65]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   11
c ---[  63]---> BDD-cost:   12
c ---[  62]---> BDD-cost:   13
c ---[  61]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  59]---> BDD-cost:   10
c ---[  58]---> BDD-cost:   11
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   13
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   10
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   12
c ---[  51]---> BDD-cost:   15
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   10
c ---[  47]---> BDD-cost:   11
c ---[  46]---> BDD-cost:   13
c ---[  45]---> BDD-cost:   15
c ---[  44]---> BDD-cost:   15
c ---[  43]---> BDD-cost:   11
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:   12
c ---[  40]---> BDD-cost:   15
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   15
c ---[  37]---> BDD-cost:   10
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   15
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   13
c ---[  31]---> BDD-cost:   11
c ---[  30]---> BDD-cost:   12
c ---[  29]---> BDD-cost:   13
c ---[  28]---> BDD-cost:   15
c ---[  27]---> BDD-cost:   15
c ---[  26]---> BDD-cost:   10
c ---[  25]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   15
c ---[  22]---> BDD-cost:   13
c ---[  21]---> BDD-cost:   13
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:   12
c ---[  18]---> BDD-cost:   12
c ---[  17]---> BDD-cost:   12
c ---[  16]---> BDD-cost:   12
c ---[  15]---> BDD-cost:   10
c ---[  14]---> BDD-cost:   11
c ---[  13]---> BDD-cost:   12
c ---[  12]---> BDD-cost:   12
c ---[  11]---> BDD-cost:   12
c ---[  10]---> BDD-cost:   13
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   12
c ---[   7]---> BDD-cost:   15
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   15
c ---[   4]---> BDD-cost:   10
c ---[   3]---> BDD-cost:   11
c ---[   2]---> BDD-cost:   13
c ---[   1]---> BDD-cost:   15
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   59636   171598 |   19878       0        0     nan |  0.000 % |
c |       100 |   59636   171598 |   21865     100     3900    39.0 |  4.827 % |
c |       250 |   59636   171598 |   24052     250     7273    29.1 |  4.827 % |
c ==============================================================================
c [1mFound solution: 1758504[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:152955     Base: 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 |       288 |  460933  1108742 |  153644     288     7892    27.4 |  4.827 % |
c |       390 |  460933  1108742 |  169008     390    11490    29.5 |  0.667 % |
c |       540 |  460847  1108549 |  185909     536    12324    23.0 |  0.681 % |
c |       767 |  460847  1108549 |  204500     763    22029    28.9 |  0.681 % |
c |      1104 |  460847  1108549 |  224950    1100    23931    21.8 |  0.681 % |
c |      1610 |  460847  1108549 |  247445    1606    28223    17.6 |  0.681 % |
c |      2369 |  460847  1108549 |  272189    2365    34675    14.7 |  0.681 % |
c |      3508 |  460847  1108549 |  299408    3504    44923    12.8 |  0.681 % |
c ==============================================================================
c [1mFound solution: 1751791[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 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 |      4200 |  463245  1115046 |  154415    4196    81401    19.4 |  0.681 % |
c |      4304 |  463245  1115046 |  169856    4300    81972    19.1 |  0.676 % |
c |      4454 |  462348  1113006 |  186842    4444    84858    19.1 |  0.824 % |
c |      4680 |  462348  1113006 |  205526    4670    86397    18.5 |  0.824 % |
c |      5017 |  462155  1112567 |  226079    5006    88171    17.6 |  0.856 % |
c |      5523 |  461604  1111317 |  248686    5503   103982    18.9 |  0.950 % |
c |      6282 |  461604  1111317 |  273555    6262   124474    19.9 |  0.950 % |
c |      7422 |  461604  1111317 |  300911    7402   136479    18.4 |  0.950 % |
c |      9130 |  461604  1111317 |  331002    9110   180236    19.8 |  0.950 % |
c |     11692 |  461604  1111317 |  364102   11672   219401    18.8 |  0.950 % |
c |     15536 |  461451  1110966 |  400512   15514   293009    18.9 |  0.978 % |
c |     21302 |  461451  1110966 |  440564   21280   452588    21.3 |  0.978 % |
c |     29953 |  460775  1109425 |  484620   29924  1781852    59.5 |  1.093 % |
c ==============================================================================
c [1mFound solution: 1735744[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 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 |     35137 |  460876  1110075 |  153625   35108  2290307    65.2 |  1.093 % |
c |     35237 |  460876  1110075 |  168987   35208  2291054    65.1 |  1.093 % |
c |     35388 |  460876  1110075 |  185886   35359  2292795    64.8 |  1.093 % |
c |     35614 |  460759  1109809 |  204474   35581  2295277    64.5 |  1.114 % |
c |     35951 |  460513  1109249 |  224922   35912  2299504    64.0 |  1.155 % |
c |     36459 |  460513  1109249 |  247414   36420  2306708    63.3 |  1.155 % |
c |     37218 |  460513  1109249 |  272156   37179  2314182    62.2 |  1.155 % |
c |     38357 |  460513  1109249 |  299371   38318  2329417    60.8 |  1.155 % |
c |     40065 |  460513  1109249 |  329308   40026  2359640    59.0 |  1.155 % |
c |     42629 |  460513  1109249 |  362239   42590  2409546    56.6 |  1.155 % |
c |     46473 |  460513  1109249 |  398463   46434  2782908    59.9 |  1.155 % |
c |     52240 |  460513  1109249 |  438310   52201  3759883    72.0 |  1.155 % |
c |     60889 |  460443  1109090 |  482141   60846  4137180    68.0 |  1.167 % |
c |     73863 |  460443  1109090 |  530355   73820  4599517    62.3 |  1.167 % |
c |     93325 |  460443  1109090 |  583390   93282  7623867    81.7 |  1.167 % |
c |    122517 |  460317  1108799 |  641729  122466  9566011    78.1 |  1.191 % |
c |    166306 |  460317  1108799 |  705902  166255 12582417    75.7 |  1.191 % |
c ==============================================================================
c [1mFound solution: 1533287[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 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 |    171505 |  460725  1110138 |  153575  171444 12829896    74.8 |  1.191 % |
c |    171605 |  460725  1110138 |  168932   34457  1229499    35.7 |  1.252 % |
c |    171755 |  460725  1110138 |  185825   34607  1230512    35.6 |  1.252 % |
c |    171980 |  460725  1110138 |  204408   34832  1231604    35.4 |  1.252 % |
c |    172317 |  460725  1110138 |  224849   35169  1234373    35.1 |  1.252 % |
c |    172823 |  460725  1110138 |  247334   35675  1242369    34.8 |  1.252 % |
c |    173582 |  460725  1110138 |  272067   36434  1249569    34.3 |  1.252 % |
c |    174722 |  460725  1110138 |  299274   37574  1287706    34.3 |  1.252 % |
c |    176430 |  460725  1110138 |  329201   39282  1315111    33.5 |  1.252 % |
c |    178992 |  460725  1110138 |  362121   41844  1575811    37.7 |  1.252 % |
c |    182837 |  460725  1110138 |  398333   45689  1715270    37.5 |  1.252 % |
c |    188603 |  460633  1109928 |  438167   51454  1796720    34.9 |  1.268 % |
c |    197252 |  460633  1109928 |  481984   60103  2225114    37.0 |  1.268 % |
c |    210226 |  460633  1109928 |  530182   73077  4214867    57.7 |  1.268 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 X4_bit_7 -X4_bit_6 X4_bit_5 X4_bit_4 X4_bit_3 X4_bit_2 -X4_bit_1 X4_bit0 X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 X9_bit0 X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 X12_bit_7 X12_bit_6 X12_bit_5 X12_bit_4 -X12_bit_3 X12_bit_2 X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 X13_bit_5 X13_bit_4 X13_bit_3 -X13_bit_2 -X13_bit_1 X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 X14_bit_4 X14_bit_3 -X14_bit_2 -X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X15_bit_7 -X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 -X15_bit_2 -X15_bit_1 -X15_bit0 -X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 -X17_bit_6 -X17_bit_5 -X17_bit_4 -X17_bit_3 -X17_bit_2 -X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 X18_bit_7 -X18_bit_6 X18_bit_5 X18_bit_4 X18_bit_3 -X18_bit_2 X18_bit_1 X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X19_bit_7 -X19_bit_6 -X19_bit_5 -X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 -X20_bit_7 -X20_bit_6 -X20_bit_5 -X20_bit_4 -X20_bit_3 -X20_bit_2 -X20_bit_1 -X20_bit0 -X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X21_bit_7 X21_bit_6 X21_bit_5 X21_bit_4 X21_bit_3 X21_bit_2 X21_bit_1 X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 X22_bit_2 -X22_bit_1 -X22_bit0 X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X23_bit_7 X23_bit_6 -X23_bit_5 X23_bit_4 X23_bit_3 -X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 X24_bit_7 -X24_bit_6 -X24_bit_5 X24_bit_4 -X24_bit_3 X24_bit_2 -X24_bit_1 -X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X25_bit_7 -X25_bit_6 -X25_bit_5 -X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 X26_bit_5 -X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X27_bit_7 X27_bit_6 -X27_bit_5 -X27_bit_4 -X27_bit_3 -X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 -X28_bit_6 X28_bit_5 X28_bit_4 -X28_bit_3 X28_bit_2 -X28_bit_1 X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 X29_bit_7 -X29_bit_6 X29_bit_5 X29_bit_4 -X29_bit_3 X29_bit_2 X29_bit_1 -X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 X32_bit_6 -X32_bit_5 -X32_bit_4 X32_bit_3 -X32_bit_2 X32_bit_1 X32_bit0 X32_bit1 X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X33_bit_7 -X33_bit_6 -X33_bit_5 -X33_bit_4 -X33_bit_3 -X33_bit_2 -X33_bit_1 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 X34_bit_7 -X34_bit_6 -X34_bit_5 X34_bit_4 X34_bit_3 X34_bit_2 -X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 -X35_bit_6 -X35_bit_5 -X35_bit_4 -X35_bit_3 -X35_bit_2 -X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X36_bit_7 -X36_bit_6 -X36_bit_5 -X36_bit_4 -X36_bit_3 -X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 X37_bit_7 X37_bit_6 -X37_bit_5 -X37_bit_4 -X37_bit_3 -X37_bit_2 -X37_bit_1 -X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X38_bit_7 -X38_bit_6 -X38_bit_5 -X38_bit_4 -X38_bit_3 X38_bit_2 -X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 X39_bit_7 -X39_bit_6 -X39_bit_5 -X39_bit_4 X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X40_bit_7 -X40_bit_6 -X40_bit_5 -X40_bit_4 -X40_bit_3 -X40_bit_2 -X40_bit_1 -X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 -X41_bit_7 X41_bit_6 X41_bit_5 X41_bit_4 X41_bit_3 X41_bit_2 -X41_bit_1 -X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X42_bit_7 X42_bit_6 X42_bit_5 X42_bit_4 -X42_bit_3 -X42_bit_2 -X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X43_bit_7 X43_bit_6 -X43_bit_5 X43_bit_4 X43_bit_3 X43_bit_2 X43_bit_1 X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 X44_bit_7 X44_bit_6 -X44_bit_5 X44_bit_4 -X44_bit_3 X44_bit_2 -X44_bit_1 -X44_bit0 X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X45_bit_7 -X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 X46_bit_6 X46_bit_5 X46_bit_4 -X46_bit_3 -X46_bit_2 X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 X47_bit_7 X47_bit_6 -X47_bit_5 -X47_bit_4 -X47_bit_3 -X47_bit_2 -X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 X48_bit_6 X48_bit_5 -X48_bit_4 -X48_bit_3 -X48_bit_2 X48_bit_1 X48_bit0 X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 -X49_bit_6 -X49_bit_5 X49_bit_4 X49_bit_3 X49_bit_2 X49_bit_1 -X49_bit0 X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 -X50_bit_7 -X50_bit_6 -X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 X51_bit_7 -X51_bit_6 -X51_bit_5 -X51_bit_4 -X51_bit_3 -X51_bit_2 -X51_bit_1 -X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 X52_bit_7 X52_bit_6 -X52_bit_5 -X52_bit_4 -X52_bit_3 -X52_bit_2 -X52_bit_1 -X52_bit0 X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 X53_bit_7 -X53_bit_6 -X53_bit_5 X53_bit_4 -X53_bit_3 X53_bit_2 X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 X54_bit_7 -X54_bit_6 -X54_bit_5 X54_bit_4 -X54_bit_3 -X54_bit_2 -X54_bit_1 X54_bit0 X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 -X55_bit_6 -X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 X56_bit_7 X56_bit_6 -X56_bit_5 -X56_bit_4 -X56_bit_3 -X56_bit_2 -X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 X57_bit_7 -X57_bit_6 X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 X57_bit0 X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X58_bit_7 -X58_bit_6 -X58_bit_5 -X58_bit_4 -X58_bit_3 -X58_bit_2 -X58_bit_1 -X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 -X59_bit_7 X59_bit_6 -X59_bit_5 -X59_bit_4 -X59_bit_3 -X59_bit_2 -X59_bit_1 -X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X60_bit_7 -X60_bit_6 -X60_bit_5 -X60_bit_4 -X60_bit_3 -X60_bit_2 -X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X61_bit_7 X61_bit_6 X61_bit_5 -X61_bit_4 X61_bit_3 -X61_bit_2 -X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 -X62_bit_7 X62_bit_6 X62_bit_5 X62_bit_4 X62_bit_3 X62_bit_2 X62_bit_1 X62_bit0 -X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 -X63_bit_7 -X63_bit_6 -X63_bit_5 X63_bit_4 X63_bit_3 -X63_bit_2 -X63_bit_1 X63_bit0 X63_bit1 -X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 X64_bit_7 -X64_bit_6 X64_bit_5 X64_bit_4 X64_bit_3 -X64_bit_2 -X64_bit_1 -X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 -X65_bit_7 -X65_bit_6 -X65_bit_5 -X65_bit_4 -X65_bit_3 -X65_bit_2 -X65_bit_1 -X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 -X66_bit_7 X66_bit_6 X66_bit_5 X66_bit_4 X66_bit_3 -X66_bit_2 -X66_bit_1 -X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 -X67_bit_7 X67_bit_6 X67_bit_5 X67_bit_4 X67_bit_3 -X67_bit_2 -X67_bit_1 -X67_bit0 -X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 X68_bit_7 X68_bit_6 X68_bit_5 X68_bit_4 X68_bit_3 -X68_bit_2 X68_bit_1 -X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 -X69_bit_7 -X69_bit_6 X69_bit_5 X69_bit_4 X69_bit_3 -X69_bit_2 -X69_bit_1 -X69_bit0 X69_bit1 X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 -X70_bit_6 -X70_bit_5 -X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 -X70_bit0 X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X71_bit_7 X71_bit_6 X71_bit_5 X71_bit_4 X71_bit_3 X71_bit_2 X71_bit_1 X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X72_bit_7 -X72_bit_6 -X72_bit_5 -X72_bit_4 -X72_bit_3 -X72_bit_2 -X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 X73_bit_7 X73_bit_6 X73_bit_5 X73_bit_4 X73_bit_3 X73_bit_2 -X73_bit_1 X73_bit0 X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 -X74_bit_7 X74_bit_6 X74_bit_5 X74_bit_4 X74_bit_3 X74_bit_2 X74_bit_1 X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 -X75_bit_7 -X75_bit_6 -X75_bit_5 -X75_bit_4 -X75_bit_3 -X75_bit_2 -X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X76_bit_7 X76_bit_6 X76_bit_5 X76_bit_4 X76_bit_3 X76_bit_2 X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 X77_bit_7 X77_bit_6 X77_bit_5 X77_bit_4 -X77_bit_3 X77_bit_2 -X77_bit_1 X77_bit0 X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X78_bit_7 -X78_bit_6 -X78_bit_5 X78_bit_4 X78_bit_3 -X78_bit_2 -X78_bit_1 -X78_bit0 X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X79_bit_7 -X79_bit_6 -X79_bit_5 -X79_bit_4 -X79_bit_3 -X79_bit_2 -X79_bit_1 -X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X80_bit_7 -X80_bit_6 -X80_bit_5 -X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 X81_bit_7 -X81_bit_6 -X81_bit_5 -X81_bit_4 X81_bit_3 X81_bit_2 X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X82_bit_7 X82_bit_6 -X82_bit_5 -X82_bit_4 X82_bit_3 -X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 X83_bit_7 -X83_bit_6 X83_bit_5 X83_bit_4 X83_bit_3 -X83_bit_2 -X83_bit_1 -X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X84_bit_7 -X84_bit_6 -X84_bit_5 -X84_bit_4 -X84_bit_3 -X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 -X85_bit_7 -X85_bit_6 -X85_bit_5 -X85_bit_4 -X85_bit_3 -X85_bit_2 -X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 X86_bit_7 X86_bit_6 X86_bit_5 X86_bit_4 -X86_bit_3 -X86_bit_2 X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 X87_bit_6 -X87_bit_5 X87_bit_4 -X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 -X88_bit_7 -X88_bit_6 X88_bit_5 X88_bit_4 X88_bit_3 -X88_bit_2 -X88_bit_1 -X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 X89_bit_7 X89_bit_6 -X89_bit_5 X89_bit_4 -X89_bit_3 X89_bit_2 X89_bit_1 X89_bit0 X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X90_bit_7 -X90_bit_6 -X90_bit_5 -X90_bit_4 -X90_bit_3 -X90_bit_2 -X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 X91_bit_7 -X91_bit_6 X91_bit_5 X91_bit_4 X91_bit_3 X91_bit_2 X91_bit_1 X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 -X92_bit_7 X92_bit_6 X92_bit_5 X92_bit_4 X92_bit_3 X92_bit_2 X92_bit_1 -X92_bit0 -X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 X93_bit_7 -X93_bit_6 -X93_bit_5 -X93_bit_4 X93_bit_3 X93_bit_2 X93_bit_1 X93_bit0 X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 -X94_bit_7 X94_bit_6 -X94_bit_5 X94_bit_4 X94_bit_3 X94_bit_2 X94_bit_1 -X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 -X95_bit_7 -X95_bit_6 -X95_bit_5 -X95_bit_4 -X95_bit_3 -X95_bit_2 -X95_bit_1 -X95_bit0 X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -X96_bit_7 -X96_bit_6 -X96_bit_5 -X96_bit_4 -X96_bit_3 -X96_bit_2 -X96_bit_1 -X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 -X97_bit_7 -X97_bit_6 X97_bit_5 X97_bit_4 X97_bit_3 -X97_bit_2 -X97_bit_1 -X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 -X98_bit_7 X98_bit_6 X98_bit_5 X98_bit_4 X98_bit_3 X98_bit_2 X98_bit_1 -X98_bit0 -X98_bit1 X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 -X99_bit_7 -X99_bit_6 -X99_bit_5 -X99_bit_4 -X99_bit_3 -X99_bit_2 -X99_bit_1 -X99_bit0 -X99_bit1 -X99_bit2 -X99_bit3#### 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.95 0.97 0.91 2/54 3856
Raw data (stat): 3856 (runsolver) R 3855 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544816377 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.95 0.97 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 14290 0 0 0 961 37 0 0 25 0 1 0 544816377 65249280 13620 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15930 13620 603 41 0 15889 0
vsize: 63720
[startup+20.0014 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 14661 0 0 0 1959 39 0 0 25 0 1 0 544816377 66453504 13991 4294967295 134512640 134672761 3221224528 3221223708 134556590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16224 13991 603 41 0 16183 0
vsize: 64896
[startup+30.0017 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 14712 0 0 0 2958 39 0 0 25 0 1 0 544816377 66588672 14042 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16257 14042 603 41 0 16216 0
vsize: 65028
[startup+40.0103 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 14749 0 0 0 3959 40 0 0 25 0 1 0 544816377 66723840 14079 4294967295 134512640 134672761 3221224528 3221223696 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16290 14079 603 41 0 16249 0
vsize: 65160
[startup+50.0114 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 14785 0 0 0 4959 40 0 0 25 0 1 0 544816377 66891776 14115 4294967295 134512640 134672761 3221224528 3221223680 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16331 14115 603 41 0 16290 0
vsize: 65324
[startup+60.0105 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 14911 0 0 0 5957 41 0 0 25 0 1 0 544816377 67428352 14241 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16462 14241 603 41 0 16421 0
vsize: 65848
[startup+70.0115 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 15053 0 0 0 6956 42 0 0 25 0 1 0 544816377 68059136 14383 4294967295 134512640 134672761 3221224528 3221223664 134560645 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16616 14383 603 41 0 16575 0
vsize: 66464
[startup+80.0121 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 15181 0 0 0 7955 43 0 0 25 0 1 0 544816377 68595712 14511 4294967295 134512640 134672761 3221224528 3221223696 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16747 14511 603 41 0 16706 0
vsize: 66988
[startup+90.0123 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 15294 0 0 0 8955 44 0 0 25 0 1 0 544816377 68997120 14624 4294967295 134512640 134672761 3221224528 3221223664 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16845 14624 603 41 0 16804 0
vsize: 67380
[startup+100.012 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 15454 0 0 0 9954 45 0 0 25 0 1 0 544816377 69672960 14784 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17010 14784 603 41 0 16969 0
vsize: 68040
[startup+110.013 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 15623 0 0 0 10953 46 0 0 25 0 1 0 544816377 70348800 14953 4294967295 134512640 134672761 3221224528 3221223712 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17175 14953 603 41 0 17134 0
vsize: 68700
[startup+120.013 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 15824 0 0 0 11952 47 0 0 25 0 1 0 544816377 71155712 15154 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17372 15154 603 41 0 17331 0
vsize: 69488
[startup+130.013 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 16050 0 0 0 12951 48 0 0 25 0 1 0 544816377 72097792 15380 4294967295 134512640 134672761 3221224528 3221223712 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17602 15380 603 41 0 17561 0
vsize: 70408
[startup+140.015 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 16259 0 0 0 13950 49 0 0 25 0 1 0 544816377 72904704 15589 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17799 15589 603 41 0 17758 0
vsize: 71196
[startup+150.015 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 16460 0 0 0 14950 49 0 0 25 0 1 0 544816377 73707520 15790 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 15790 603 41 0 17954 0
vsize: 71980
[startup+160.015 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 16652 0 0 0 15949 50 0 0 25 0 1 0 544816377 74641408 15982 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18223 15982 603 41 0 18182 0
vsize: 72892
[startup+170.016 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 16965 0 0 0 16949 50 0 0 25 0 1 0 544816377 76009472 16295 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18557 16295 603 41 0 18516 0
vsize: 74228
[startup+180.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 17129 0 0 0 17948 52 0 0 25 0 1 0 544816377 76582912 16438 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18697 16438 603 41 0 18656 0
vsize: 74788
[startup+190.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 17215 0 0 0 18948 52 0 0 25 0 1 0 544816377 76853248 16524 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18763 16524 603 41 0 18722 0
vsize: 75052
[startup+200.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 17302 0 0 0 19948 52 0 0 25 0 1 0 544816377 77258752 16611 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18862 16611 603 41 0 18821 0
vsize: 75448
[startup+210.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 17488 0 0 0 20947 53 0 0 25 0 1 0 544816377 77926400 16797 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19025 16797 603 41 0 18984 0
vsize: 76100
[startup+220.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 17627 0 0 0 21946 54 0 0 25 0 1 0 544816377 78471168 16936 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19158 16936 603 41 0 19117 0
vsize: 76632
[startup+230.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 17728 0 0 0 22946 54 0 0 25 0 1 0 544816377 78872576 17037 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19256 17037 603 41 0 19215 0
vsize: 77024
[startup+240.017 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 17864 0 0 0 23946 55 0 0 25 0 1 0 544816377 79536128 17173 4294967295 134512640 134672761 3221224528 3221223664 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19418 17173 603 41 0 19377 0
vsize: 77672
[startup+250.017 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 17975 0 0 0 24946 55 0 0 25 0 1 0 544816377 79921152 17284 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19512 17284 603 41 0 19471 0
vsize: 78048
[startup+260.017 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 18143 0 0 0 25945 56 0 0 25 0 1 0 544816377 80687104 17452 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19699 17452 603 41 0 19658 0
vsize: 78796
[startup+270.017 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 18282 0 0 0 26945 56 0 0 25 0 1 0 544816377 81227776 17591 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19831 17591 603 41 0 19790 0
vsize: 79324
[startup+280.017 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 18430 0 0 0 27945 57 0 0 25 0 1 0 544816377 81903616 17739 4294967295 134512640 134672761 3221224528 3221223696 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19996 17739 603 41 0 19955 0
vsize: 79984
[startup+290.018 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 18611 0 0 0 28944 57 0 0 25 0 1 0 544816377 82563072 17920 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20157 17920 603 41 0 20116 0
vsize: 80628
[startup+300.018 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 18707 0 0 0 29944 57 0 0 25 0 1 0 544816377 82968576 18016 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20256 18016 603 41 0 20215 0
vsize: 81024
[startup+310.018 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 19017 0 0 0 30944 58 0 0 25 0 1 0 544816377 84185088 18326 4294967295 134512640 134672761 3221224528 3221223696 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20553 18326 603 41 0 20512 0
vsize: 82212
[startup+320.018 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 19313 0 0 0 31943 59 0 0 25 0 1 0 544816377 85659648 18622 4294967295 134512640 134672761 3221224528 3221223696 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20913 18622 603 41 0 20872 0
vsize: 83652
[startup+330.019 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 19493 0 0 0 32943 60 0 0 25 0 1 0 544816377 86327296 18802 4294967295 134512640 134672761 3221224528 3221223696 134561256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21076 18802 603 41 0 21035 0
vsize: 84304
[startup+340.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 19709 0 0 0 33942 60 0 0 25 0 1 0 544816377 87261184 19018 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21304 19018 603 41 0 21263 0
vsize: 85216
[startup+350.019 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 19900 0 0 0 34942 60 0 0 25 0 1 0 544816377 88064000 19209 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21500 19209 603 41 0 21459 0
vsize: 86000
[startup+360.018 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 20316 0 0 0 35941 62 0 0 25 0 1 0 544816377 89673728 19625 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21893 19625 603 41 0 21852 0
vsize: 87572
[startup+370.027 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 20757 0 0 0 36941 63 0 0 25 0 1 0 544816377 91541504 20066 4294967295 134512640 134672761 3221224528 3221223696 134559068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 20066 603 41 0 22308 0
vsize: 89396
[startup+380.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 21188 0 0 0 37940 64 0 0 25 0 1 0 544816377 93286400 20497 4294967295 134512640 134672761 3221224528 3221223664 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22775 20497 603 41 0 22734 0
vsize: 91100
[startup+390.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 21588 0 0 0 38939 65 0 0 25 0 1 0 544816377 94904320 20897 4294967295 134512640 134672761 3221224528 3221223632 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23170 20897 603 41 0 23129 0
vsize: 92680
[startup+400.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 22009 0 0 0 39938 66 0 0 25 0 1 0 544816377 96636928 21318 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23593 21318 603 41 0 23552 0
vsize: 94372
[startup+410.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 22464 0 0 0 40937 67 0 0 25 0 1 0 544816377 98516992 21773 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24052 21773 603 41 0 24011 0
vsize: 96208
[startup+420.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 22884 0 0 0 41936 69 0 0 25 0 1 0 544816377 100118528 22193 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24443 22193 603 41 0 24402 0
vsize: 97772
[startup+430.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 22966 0 0 0 42936 69 0 0 25 0 1 0 544816377 100519936 22275 4294967295 134512640 134672761 3221224528 3221223696 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24541 22275 603 41 0 24500 0
vsize: 98164
[startup+440.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 23095 0 0 0 43936 70 0 0 25 0 1 0 544816377 101056512 22404 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24672 22404 603 41 0 24631 0
vsize: 98688
[startup+450.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 23189 0 0 0 44935 70 0 0 25 0 1 0 544816377 101322752 22498 4294967295 134512640 134672761 3221224528 3221223696 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24737 22498 603 41 0 24696 0
vsize: 98948
[startup+460.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 23269 0 0 0 45935 70 0 0 25 0 1 0 544816377 101724160 22578 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24835 22578 603 41 0 24794 0
vsize: 99340
[startup+470.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 23366 0 0 0 46935 70 0 0 25 0 1 0 544816377 102125568 22675 4294967295 134512640 134672761 3221224528 3221223664 134560694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24933 22675 603 41 0 24892 0
vsize: 99732
[startup+480.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 23513 0 0 0 47935 71 0 0 25 0 1 0 544816377 102658048 22822 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25063 22822 603 41 0 25022 0
vsize: 100252
[startup+490.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 23613 0 0 0 48935 71 0 0 25 0 1 0 544816377 103051264 22922 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25159 22922 603 41 0 25118 0
vsize: 100636
[startup+500.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 23724 0 0 0 49935 72 0 0 25 0 1 0 544816377 103452672 23033 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25257 23033 603 41 0 25216 0
vsize: 101028
[startup+510.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 23821 0 0 0 50935 72 0 0 25 0 1 0 544816377 103845888 23130 4294967295 134512640 134672761 3221224528 3221223632 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25353 23130 603 41 0 25312 0
vsize: 101412
[startup+520.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 23930 0 0 0 51935 72 0 0 25 0 1 0 544816377 104349696 23239 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25476 23239 603 41 0 25435 0
vsize: 101904
[startup+530.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 24026 0 0 0 52935 72 0 0 25 0 1 0 544816377 104742912 23335 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25572 23335 603 41 0 25531 0
vsize: 102288
[startup+540.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 24140 0 0 0 53934 73 0 0 25 0 1 0 544816377 105283584 23449 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25704 23449 603 41 0 25663 0
vsize: 102816
[startup+550.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 24286 0 0 0 54933 74 0 0 25 0 1 0 544816377 105807872 23595 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25832 23595 603 41 0 25791 0
vsize: 103328
[startup+560.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 24391 0 0 0 55933 74 0 0 25 0 1 0 544816377 106332160 23700 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25960 23700 603 41 0 25919 0
vsize: 103840
[startup+570.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 24571 0 0 0 56933 75 0 0 25 0 1 0 544816377 106979328 23880 4294967295 134512640 134672761 3221224528 3221223712 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26118 23880 603 41 0 26077 0
vsize: 104472
[startup+580.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 24686 0 0 0 57933 75 0 0 25 0 1 0 544816377 107491328 23995 4294967295 134512640 134672761 3221224528 3221223728 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26243 23995 603 41 0 26202 0
vsize: 104972
[startup+590.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 24761 0 0 0 58933 75 0 0 25 0 1 0 544816377 107753472 24070 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26307 24070 603 41 0 26266 0
vsize: 105228
[startup+600.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 24845 0 0 0 59933 75 0 0 25 0 1 0 544816377 108142592 24154 4294967295 134512640 134672761 3221224528 3221223728 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26402 24154 603 41 0 26361 0
vsize: 105608
[startup+610.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 24947 0 0 0 60933 76 0 0 25 0 1 0 544816377 108498944 24256 4294967295 134512640 134672761 3221224528 3221223680 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26489 24256 603 41 0 26448 0
vsize: 105956
[startup+620.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 25013 0 0 0 61932 76 0 0 25 0 1 0 544816377 108867584 24322 4294967295 134512640 134672761 3221224528 3221223712 134558374 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26579 24322 603 41 0 26538 0
vsize: 106316
[startup+630.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 25058 0 0 0 62933 76 0 0 25 0 1 0 544816377 108994560 24367 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26610 24367 603 41 0 26569 0
vsize: 106440
[startup+640.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 25146 0 0 0 63932 76 0 0 25 0 1 0 544816377 109400064 24455 4294967295 134512640 134672761 3221224528 3221223696 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26709 24455 603 41 0 26668 0
vsize: 106836
[startup+650.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 25413 0 0 0 64931 78 0 0 25 0 1 0 544816377 110473216 24722 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26971 24722 603 41 0 26930 0
vsize: 107884
[startup+660.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 25557 0 0 0 65929 78 0 0 25 0 1 0 544816377 111013888 24866 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27103 24866 603 41 0 27062 0
vsize: 108412
[startup+670.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 25685 0 0 0 66928 79 0 0 25 0 1 0 544816377 112074752 24994 4294967295 134512640 134672761 3221224528 3221223696 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27362 24994 603 41 0 27321 0
vsize: 109448
[startup+680.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 26049 0 0 0 67927 81 0 0 25 0 1 0 544816377 113549312 25358 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27722 25358 603 41 0 27681 0
vsize: 110888
[startup+690.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 26146 0 0 0 68927 81 0 0 25 0 1 0 544816377 113958912 25455 4294967295 134512640 134672761 3221224528 3221223632 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27822 25455 603 41 0 27781 0
vsize: 111288
[startup+700.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 26308 0 0 0 69927 81 0 0 25 0 1 0 544816377 114626560 25617 4294967295 134512640 134672761 3221224528 3221223664 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27985 25617 603 41 0 27944 0
vsize: 111940
[startup+710.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 26450 0 0 0 70927 82 0 0 25 0 1 0 544816377 115179520 25759 4294967295 134512640 134672761 3221224528 3221223696 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28120 25759 603 41 0 28079 0
vsize: 112480
[startup+720.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 26544 0 0 0 71927 82 0 0 25 0 1 0 544816377 115585024 25853 4294967295 134512640 134672761 3221224528 3221223728 134557897 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28219 25853 603 41 0 28178 0
vsize: 112876
[startup+730.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 26709 0 0 0 72927 82 0 0 25 0 1 0 544816377 116244480 26018 4294967295 134512640 134672761 3221224528 3221223664 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28380 26018 603 41 0 28339 0
vsize: 113520
[startup+740.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 26824 0 0 0 73926 83 0 0 25 0 1 0 544816377 116649984 26133 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28479 26133 603 41 0 28438 0
vsize: 113916
[startup+750.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 26961 0 0 0 74926 83 0 0 25 0 1 0 544816377 117186560 26270 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28610 26270 603 41 0 28569 0
vsize: 114440
[startup+760.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 27096 0 0 0 75926 83 0 0 25 0 1 0 544816377 117714944 26405 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28739 26405 603 41 0 28698 0
vsize: 114956
[startup+770.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 27329 0 0 0 76926 84 0 0 25 0 1 0 544816377 118661120 26638 4294967295 134512640 134672761 3221224528 3221223664 134560585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28970 26638 603 41 0 28929 0
vsize: 115880
[startup+780.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 27576 0 0 0 77925 84 0 0 25 0 1 0 544816377 119734272 26885 4294967295 134512640 134672761 3221224528 3221223632 134559838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29232 26885 603 41 0 29191 0
vsize: 116928
[startup+790.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 27709 0 0 0 78926 84 0 0 25 0 1 0 544816377 120274944 27018 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29364 27018 603 41 0 29323 0
vsize: 117456
[startup+800.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 27817 0 0 0 79925 85 0 0 25 0 1 0 544816377 120676352 27126 4294967295 134512640 134672761 3221224528 3221223484 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29462 27126 603 41 0 29421 0
vsize: 117848
[startup+810.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28052 0 0 0 80924 86 0 0 25 0 1 0 544816377 121630720 27361 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29695 27361 603 41 0 29654 0
vsize: 118780
[startup+820.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28394 0 0 0 81924 86 0 0 25 0 1 0 544816377 123080704 27703 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30049 27703 603 41 0 30008 0
vsize: 120196
[startup+830.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28540 0 0 0 82923 87 0 0 25 0 1 0 544816377 123621376 27849 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30181 27849 603 41 0 30140 0
vsize: 120724
[startup+840.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28612 0 0 0 83923 88 0 0 25 0 1 0 544816377 123891712 27921 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30247 27921 603 41 0 30206 0
vsize: 120988
[startup+850.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 84923 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223484 1075350790 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+860.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 85923 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223652 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+870.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 86923 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+880.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 87923 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+890.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 88923 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+900.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 89924 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+910.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 90924 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+920.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 91924 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+930.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 92924 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+940.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 93924 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223696 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+950.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 94925 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+960.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 95925 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+970.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 96925 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+980.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 97925 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+990.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 98925 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 99926 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 100926 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223676 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 101926 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 102926 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3856
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 103926 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.92 5/59 3882
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 104927 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1060.03 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 3909
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 105927 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223632 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1070.03 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 3909
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 106927 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1080.03 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 3909
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 107927 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223664 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1090.03 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 3909
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 108927 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223692 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1100.03 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 3909
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 109927 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223696 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1110.03 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 3909
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 110928 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1120.03 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 3909
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 111928 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223696 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1130.03 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 3911
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 112928 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1140.03 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 3911
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 113928 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1150.03 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 3911
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 114928 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1160.03 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 3911
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 115928 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1170.03 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 3911
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 116928 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223664 134560647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1180.03 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 3911
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 117929 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223664 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1190.03 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 3911
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 118929 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223632 134560313 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3911
Raw data (stat): 3856 (minisat+) R 3855 28099 28098 0 -1 0 28753 0 0 0 119929 88 0 0 25 0 1 0 544816377 124309504 28047 4294967295 134512640 134672761 3221224528 3221223632 134559890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 28047 603 41 0 30308 0
vsize: 121396
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 3911
Raw data (stat): 3856 (minisat+) Z 3855 28099 28098 0 -1 12 28756 0 0 0 119929 93 0 0 25 0 1 0 544816377 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.09
CPU time (s): 1200.24
CPU user time (s): 1199.3
CPU system time (s): 0.936857
CPU usage (%): 100.012
Max. virtual memory (Kb): 121396
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####