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-ran10x10c.opb
MD5SUM	31a8734340f0544712ef974997c104b2
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2677632
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	515723936
Number of bits of the sum of numbers in the objective function	29
Biggest number in a constraint	4718592
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	515723936
Number of bits of the biggest sum of numbers	29
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
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 17690

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-21 11:22:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19226 boxname=wulflinc1 idbench=1479 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  31a8734340f0544712ef974997c104b2  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-ran10x10c.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-ran10x10c.opb /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-ran10x10c.opb
IDLAUNCH: 19226
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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	: 2
cpu MHz		: 451.053
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:        794328 kB
Buffers:          2912 kB
Cached:         212308 kB
SwapCached:          0 kB
Active:          48520 kB
Inactive:       169856 kB
HighTotal:      131008 kB
HighFree:        63700 kB
LowTotal:       903652 kB
LowFree:        730628 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           7220 kB
Slab:            16200 kB
Committed_AS:    92808 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:42:36 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 19226 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:  817
c ---[ 136]---> BDD-cost: 1034
c ---[ 134]---> BDD-cost: 1141
c ---[ 132]---> BDD-cost: 1061
c ---[ 130]---> BDD-cost: 1053
c ---[ 128]---> BDD-cost:  607
c ---[ 126]---> BDD-cost: 1110
c ---[ 124]---> BDD-cost:  977
c ---[ 122]---> BDD-cost: 1061
c ---[ 120]---> BDD-cost: 1143
c ---[ 118]---> BDD-cost:  748
c ---[ 116]---> BDD-cost: 1143
c ---[ 114]---> BDD-cost:  748
c ---[ 112]---> BDD-cost: 1169
c ---[ 110]---> BDD-cost:  954
c ---[ 108]---> BDD-cost:  888
c ---[ 106]---> BDD-cost: 1062
c ---[ 104]---> BDD-cost: 1086
c ---[ 102]---> BDD-cost: 1197
c ---[ 100]---> BDD-cost:  748
c ---[  99]---> BDD-cost:   10
c ---[  98]---> BDD-cost:   11
c ---[  97]---> BDD-cost:   10
c ---[  96]---> BDD-cost:   15
c ---[  95]---> BDD-cost:   10
c ---[  94]---> BDD-cost:   15
c ---[  93]---> BDD-cost:   12
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   15
c ---[  90]---> BDD-cost:   15
c ---[  89]---> BDD-cost:   15
c ---[  88]---> BDD-cost:   10
c ---[  87]---> BDD-cost:   10
c ---[  86]---> BDD-cost:   10
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   10
c ---[  83]---> BDD-cost:   13
c ---[  82]---> BDD-cost:   12
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   15
c ---[  79]---> BDD-cost:   13
c ---[  78]---> BDD-cost:   13
c ---[  77]---> BDD-cost:   10
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   10
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   10
c ---[  72]---> BDD-cost:   15
c ---[  71]---> BDD-cost:   12
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   15
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:   15
c ---[  66]---> BDD-cost:   10
c ---[  65]---> BDD-cost:   11
c ---[  64]---> BDD-cost:   10
c ---[  63]---> BDD-cost:   14
c ---[  62]---> BDD-cost:   10
c ---[  61]---> BDD-cost:   14
c ---[  60]---> BDD-cost:   12
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:   14
c ---[  57]---> BDD-cost:   14
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   10
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:    9
c ---[  52]---> BDD-cost:    9
c ---[  51]---> BDD-cost:    9
c ---[  50]---> BDD-cost:    9
c ---[  49]---> BDD-cost:    9
c ---[  48]---> BDD-cost:    9
c ---[  47]---> BDD-cost:    9
c ---[  46]---> BDD-cost:    9
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:   11
c ---[  42]---> BDD-cost:   10
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   10
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   12
c ---[  37]---> BDD-cost:   11
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   15
c ---[  33]---> BDD-cost:   10
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:   10
c ---[  30]---> BDD-cost:   13
c ---[  29]---> BDD-cost:   10
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   12
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:   13
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   13
c ---[  22]---> BDD-cost:   10
c ---[  21]---> BDD-cost:   11
c ---[  20]---> BDD-cost:   10
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   12
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   15
c ---[  13]---> BDD-cost:   15
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   10
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:   10
c ---[   8]---> BDD-cost:   17
c ---[   7]---> BDD-cost:   10
c ---[   6]---> BDD-cost:   17
c ---[   5]---> BDD-cost:   12
c ---[   4]---> BDD-cost:   11
c ---[   3]---> BDD-cost:   15
c ---[   2]---> BDD-cost:   13
c ---[   1]---> BDD-cost:   17
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   57457   165221 |   19152       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 12461981[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:143862     Base: 2 2 2 2 2 2 2 2 2 2 3 3 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        29 |  465966  1118983 |  155322      29      528    18.2 |  0.000 % |
c |       129 |  465966  1118983 |  170854     129    18497   143.4 |  0.712 % |
c |       279 |  465880  1118789 |  187939     278    20652    74.3 |  0.725 % |
c |       504 |  465778  1118557 |  206733     502    21705    43.2 |  0.744 % |
c |       843 |  465119  1117061 |  227406     820    23464    28.6 |  0.859 % |
c |      1349 |  465119  1117061 |  250147    1326    74627    56.3 |  0.859 % |
c ==============================================================================
c [1mFound solution: 6603958[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 3 3 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1678 |  466587  1121636 |  155529    1655    81661    49.3 |  0.859 % |
c |      1778 |  465774  1119783 |  171081    1743    82414    47.3 |  0.997 % |
c |      1928 |  465774  1119783 |  188190    1893    83321    44.0 |  0.997 % |
c |      2155 |  465526  1119220 |  207009    2111    85063    40.3 |  1.042 % |
c |      2492 |  464364  1116567 |  227710    2417    86942    36.0 |  1.255 % |
c |      3000 |  464364  1116567 |  250481    2925    89895    30.7 |  1.255 % |
c |      3759 |  464356  1116549 |  275529    3683    96343    26.2 |  1.256 % |
c |      4898 |  464356  1116549 |  303082    4822   108010    22.4 |  1.256 % |
c |      6606 |  464356  1116549 |  333390    6530   126203    19.3 |  1.256 % |
c |      9168 |  464356  1116549 |  366729    9092   443910    48.8 |  1.256 % |
c |     13012 |  463965  1115651 |  403402   12927   983621    76.1 |  1.329 % |
c ==============================================================================
c [1mFound solution: 4926880[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 3 3 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15049 |  464439  1116883 |  154813   14809  1140868    77.0 |  1.329 % |
c |     15149 |  464439  1116883 |  170294   14909  1142400    76.6 |  1.363 % |
c |     15299 |  464439  1116883 |  187323   15059  1143754    76.0 |  1.363 % |
c |     15524 |  464439  1116883 |  206056   15284  1145206    74.9 |  1.363 % |
c |     15863 |  464439  1116883 |  226661   15623  1148990    73.5 |  1.363 % |
c |     16369 |  464439  1116883 |  249327   16129  1153401    71.5 |  1.363 % |
c |     17128 |  464439  1116883 |  274260   16888  1162575    68.8 |  1.363 % |
c |     18268 |  464439  1116883 |  301686   18028  1199418    66.5 |  1.363 % |
c |     19976 |  464439  1116883 |  331855   19736  1220790    61.9 |  1.363 % |
c |     22538 |  464439  1116883 |  365040   22298  1457358    65.4 |  1.363 % |
c |     26384 |  464395  1116783 |  401545   26143  1528959    58.5 |  1.370 % |
c ==============================================================================
c [1mFound solution: 4772380[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 3 3 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31232 |  465109  1118631 |  155036   30991  2818819    91.0 |  1.370 % |
c |     31332 |  464838  1118011 |  170539   31082  2822575    90.8 |  1.421 % |
c |     31482 |  464838  1118011 |  187593   31232  2824137    90.4 |  1.421 % |
c |     31707 |  464006  1116105 |  206352   31419  2825963    89.9 |  1.577 % |
c |     32044 |  464006  1116105 |  226988   31756  2865528    90.2 |  1.577 % |
c |     32553 |  464006  1116105 |  249687   32265  2898261    89.8 |  1.577 % |
c |     33313 |  464006  1116105 |  274655   33025  2928269    88.7 |  1.577 % |
c |     34452 |  464006  1116105 |  302121   34164  3033784    88.8 |  1.577 % |
c |     36160 |  463090  1113997 |  332333   35822  3112841    86.9 |  1.750 % |
c |     38722 |  463063  1113938 |  365566   38383  3358856    87.5 |  1.755 % |
c |     42566 |  463063  1113938 |  402123   42227  3634636    86.1 |  1.755 % |
c |     48333 |  462393  1112401 |  442335   47979  3871000    80.7 |  1.882 % |
c ==============================================================================
c [1mFound solution: 4529410[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 3 3 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     50046 |  462562  1112967 |  154187   49687  3924581    79.0 |  1.882 % |
c |     50146 |  462562  1112967 |  169605   49787  3925225    78.8 |  1.891 % |
c |     50297 |  462562  1112967 |  186566   49938  3926837    78.6 |  1.891 % |
c |     50524 |  462562  1112967 |  205222   50165  3928189    78.3 |  1.891 % |
c |     50861 |  462562  1112967 |  225745   50502  3937036    78.0 |  1.891 % |
c |     51367 |  462558  1112958 |  248319   51007  3968200    77.8 |  1.892 % |
c |     52127 |  462408  1112616 |  273151   51766  4023243    77.7 |  1.919 % |
c |     53266 |  462296  1112360 |  300466   52903  4109630    77.7 |  1.939 % |
c |     54977 |  461899  1111444 |  330513   54578  4847745    88.8 |  2.017 % |
c |     57539 |  461656  1110882 |  363564   57133  5088634    89.1 |  2.064 % |
c ==============================================================================
c [1mFound solution: 4515501[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 2 3 3 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61231 |  461517  1110594 |  153839   60819  5477880    90.1 |  2.064 % |
c |     61331 |  461517  1110594 |  169222   60919  5484008    90.0 |  2.093 % |
c |     61482 |  461517  1110594 |  186145   61070  5493732    90.0 |  2.093 % |
c |     61707 |  461517  1110594 |  204759   61295  5519604    90.0 |  2.093 % |
c |     62044 |  461517  1110594 |  225235   61632  5533687    89.8 |  2.093 % |
c |     62550 |  460644  1108586 |  247759   62072  5537675    89.2 |  2.259 % |
c |     63311 |  460644  1108586 |  272535   62833  5547566    88.3 |  2.259 % |
c |     64453 |  460644  1108586 |  299788   63975  5559773    86.9 |  2.259 % |
c |     66161 |  460614  1108518 |  329767   65682  5603143    85.3 |  2.264 % |
c |     68723 |  460614  1108518 |  362744   68244  5989138    87.8 |  2.264 % |
c |     72567 |  460590  1108464 |  399018   72087  6797213    94.3 |  2.268 % |
c |     78333 |  460590  1108464 |  438920   77853  7534987    96.8 |  2.268 % |
c |     86984 |  460590  1108464 |  482812   86504  8760906   101.3 |  2.268 % |
c ==============================================================================
c [1mFound solution: 3847060[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 3 3 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97334 |  460210  1107633 |  153403   96841 11722134   121.0 |  2.268 % |
c |     97434 |  460210  1107633 |  168743   96941 11724996   120.9 |  2.351 % |
c |     97584 |  460210  1107633 |  185617   97091 11727871   120.8 |  2.351 % |
c |     97809 |  460034  1107233 |  204179   97311 11732839   120.6 |  2.382 % |
c |     98146 |  460034  1107233 |  224597   97648 11817981   121.0 |  2.382 % |
c |     98652 |  460034  1107233 |  247057   98154 11830636   120.5 |  2.382 % |
c |     99411 |  460034  1107233 |  271762   98913 11838684   119.7 |  2.382 % |
c ==============================================================================
c [1mFound solution: 3843251[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 3 3 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99663 |  460054  1107278 |  153351   99165 11859813   119.6 |  2.382 % |
c |     99763 |  460054  1107278 |  168686   99265 11862626   119.5 |  2.382 % |
c |     99914 |  460054  1107278 |  185554   99416 11865724   119.4 |  2.382 % |
c |    100140 |  460054  1107278 |  204110   99642 11896849   119.4 |  2.382 % |
c |    100481 |  460054  1107278 |  224521   99983 11902836   119.0 |  2.382 % |
c |    100988 |  459870  1106854 |  246973  100481 11908214   118.5 |  2.417 % |
c |    101747 |  459852  1106813 |  271670  101239 11966293   118.2 |  2.420 % |
c |    102887 |  458697  1104161 |  298837  102297 12107846   118.4 |  2.636 % |
c |    104596 |  458670  1104100 |  328721  104005 12153140   116.9 |  2.641 % |
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 -#### 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.73 0.93 0.97 2/56 27371
Raw data (stat): 27371 (runsolver) R 27370 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 429609354 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.77 0.94 0.97 2/56 27371
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 13304 0 0 0 963 36 0 0 25 0 1 0 429609354 62750720 12972 4294967295 134512640 134672761 3221224528 3221223664 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15320 12972 603 41 0 15279 0
vsize: 61280
[startup+20.0013 s]
Raw data (loadavg): 0.81 0.94 0.97 2/56 27371
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 13362 0 0 0 1963 36 0 0 25 0 1 0 429609354 63012864 13030 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15384 13030 603 41 0 15343 0
vsize: 61536
[startup+30.001 s]
Raw data (loadavg): 0.84 0.94 0.97 2/56 27371
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 13612 0 0 0 2962 37 0 0 25 0 1 0 429609354 63848448 13280 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15588 13280 603 41 0 15547 0
vsize: 62352
[startup+40.0008 s]
Raw data (loadavg): 0.86 0.94 0.97 2/56 27371
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 13712 0 0 0 3961 37 0 0 25 0 1 0 429609354 64380928 13380 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15718 13380 603 41 0 15677 0
vsize: 62872
[startup+50.0016 s]
Raw data (loadavg): 0.88 0.94 0.97 2/56 27371
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 13805 0 0 0 4961 38 0 0 25 0 1 0 429609354 64651264 13473 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15784 13473 603 41 0 15743 0
vsize: 63136
[startup+60.0024 s]
Raw data (loadavg): 0.90 0.94 0.97 2/56 27371
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 13941 0 0 0 5960 39 0 0 25 0 1 0 429609354 65302528 13609 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15943 13609 603 41 0 15902 0
vsize: 63772
[startup+70.0037 s]
Raw data (loadavg): 0.91 0.95 0.97 2/56 27371
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 14061 0 0 0 6960 40 0 0 25 0 1 0 429609354 65826816 13729 4294967295 134512640 134672761 3221224528 3221223664 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16071 13729 603 41 0 16030 0
vsize: 64284
[startup+80.004 s]
Raw data (loadavg): 0.93 0.95 0.97 2/56 27371
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 14246 0 0 0 7959 40 0 0 25 0 1 0 429609354 66494464 13914 4294967295 134512640 134672761 3221224528 3221223696 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16234 13914 603 41 0 16193 0
vsize: 64936
[startup+90.0038 s]
Raw data (loadavg): 0.94 0.95 0.97 2/56 27371
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 14386 0 0 0 8959 40 0 0 25 0 1 0 429609354 67162112 14054 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16397 14054 603 41 0 16356 0
vsize: 65588
[startup+100.004 s]
Raw data (loadavg): 0.95 0.95 0.97 2/56 27371
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 14456 0 0 0 9959 41 0 0 25 0 1 0 429609354 67432448 14124 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16463 14124 603 41 0 16422 0
vsize: 65852
[startup+110.004 s]
Raw data (loadavg): 0.95 0.95 0.97 2/56 27371
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 14576 0 0 0 10958 41 0 0 25 0 1 0 429609354 67837952 14244 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16562 14244 603 41 0 16521 0
vsize: 66248
[startup+120.005 s]
Raw data (loadavg): 0.96 0.95 0.97 2/56 27371
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 14626 0 0 0 11958 42 0 0 25 0 1 0 429609354 68108288 14294 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16628 14294 603 41 0 16587 0
vsize: 66512
[startup+130.005 s]
Raw data (loadavg): 0.97 0.95 0.97 2/56 27371
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 14712 0 0 0 12958 42 0 0 25 0 1 0 429609354 68423680 14380 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16705 14380 603 41 0 16664 0
vsize: 66820
[startup+140.006 s]
Raw data (loadavg): 0.97 0.95 0.97 2/56 27371
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 14741 0 0 0 13958 42 0 0 25 0 1 0 429609354 68558848 14409 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16738 14409 603 41 0 16697 0
vsize: 66952
[startup+150.007 s]
Raw data (loadavg): 0.98 0.95 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 14829 0 0 0 14958 42 0 0 25 0 1 0 429609354 68923392 14485 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16827 14485 603 41 0 16786 0
vsize: 67308
[startup+160.007 s]
Raw data (loadavg): 0.98 0.95 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 14892 0 0 0 15958 43 0 0 25 0 1 0 429609354 69185536 14548 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16891 14548 603 41 0 16850 0
vsize: 67564
[startup+170.007 s]
Raw data (loadavg): 0.98 0.95 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 14972 0 0 0 16957 43 0 0 25 0 1 0 429609354 69451776 14628 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16956 14628 603 41 0 16915 0
vsize: 67824
[startup+180.007 s]
Raw data (loadavg): 0.98 0.96 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 15122 0 0 0 17957 44 0 0 25 0 1 0 429609354 70119424 14778 4294967295 134512640 134672761 3221224528 3221223664 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17119 14778 603 41 0 17078 0
vsize: 68476
[startup+190.008 s]
Raw data (loadavg): 0.99 0.96 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 15179 0 0 0 18956 45 0 0 25 0 1 0 429609354 70389760 14835 4294967295 134512640 134672761 3221224528 3221223676 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17185 14835 603 41 0 17144 0
vsize: 68740
[startup+200.008 s]
Raw data (loadavg): 0.99 0.96 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 15219 0 0 0 19956 45 0 0 25 0 1 0 429609354 70524928 14875 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17218 14875 603 41 0 17177 0
vsize: 68872
[startup+210.009 s]
Raw data (loadavg): 0.99 0.96 0.97 3/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 15365 0 0 0 20956 46 0 0 25 0 1 0 429609354 71065600 15021 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17350 15021 603 41 0 17309 0
vsize: 69400
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 15566 0 0 0 21955 47 0 0 25 0 1 0 429609354 71860224 15222 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17544 15222 603 41 0 17503 0
vsize: 70176
[startup+230.01 s]
Raw data (loadavg): 0.99 0.96 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 15786 0 0 0 22954 48 0 0 25 0 1 0 429609354 72785920 15442 4294967295 134512640 134672761 3221224528 3221223664 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17770 15442 603 41 0 17729 0
vsize: 71080
[startup+240.01 s]
Raw data (loadavg): 0.99 0.96 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 15943 0 0 0 23954 48 0 0 25 0 1 0 429609354 73461760 15599 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17935 15599 603 41 0 17894 0
vsize: 71740
[startup+250.01 s]
Raw data (loadavg): 0.99 0.96 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 16143 0 0 0 24953 49 0 0 25 0 1 0 429609354 74285056 15799 4294967295 134512640 134672761 3221224528 3221223632 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18136 15799 603 41 0 18095 0
vsize: 72544
[startup+260.011 s]
Raw data (loadavg): 0.99 0.96 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 16359 0 0 0 25953 49 0 0 25 0 1 0 429609354 75100160 16015 4294967295 134512640 134672761 3221224528 3221223664 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18335 16015 603 41 0 18294 0
vsize: 73340
[startup+270.011 s]
Raw data (loadavg): 0.99 0.96 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 16546 0 0 0 26953 50 0 0 25 0 1 0 429609354 75911168 16202 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18533 16202 603 41 0 18492 0
vsize: 74132
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 16631 0 0 0 27953 50 0 0 25 0 1 0 429609354 76103680 16270 4294967295 134512640 134672761 3221224528 3221223612 134565156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18580 16270 603 41 0 18539 0
vsize: 74320
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 16686 0 0 0 28953 50 0 0 25 0 1 0 429609354 76374016 16325 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18646 16325 603 41 0 18605 0
vsize: 74584
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 16755 0 0 0 29952 51 0 0 25 0 1 0 429609354 76771328 16394 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 16394 603 41 0 18702 0
vsize: 74972
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 16818 0 0 0 30952 51 0 0 25 0 1 0 429609354 77037568 16457 4294967295 134512640 134672761 3221224528 3221223724 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 16457 603 41 0 18767 0
vsize: 75232
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 16926 0 0 0 31952 51 0 0 25 0 1 0 429609354 77443072 16565 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18907 16565 603 41 0 18866 0
vsize: 75628
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 17044 0 0 0 32951 52 0 0 25 0 1 0 429609354 77975552 16683 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19037 16683 603 41 0 18996 0
vsize: 76148
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 17136 0 0 0 33951 52 0 0 25 0 1 0 429609354 78368768 16775 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19133 16775 603 41 0 19092 0
vsize: 76532
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 17209 0 0 0 34951 52 0 0 25 0 1 0 429609354 78635008 16848 4294967295 134512640 134672761 3221224528 3221223664 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19198 16848 603 41 0 19157 0
vsize: 76792
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 17259 0 0 0 35951 53 0 0 25 0 1 0 429609354 78766080 16898 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19230 16898 603 41 0 19189 0
vsize: 76920
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 17323 0 0 0 36950 53 0 0 25 0 1 0 429609354 79036416 16962 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19296 16962 603 41 0 19255 0
vsize: 77184
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 17363 0 0 0 37951 53 0 0 25 0 1 0 429609354 79171584 17002 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19329 17002 603 41 0 19288 0
vsize: 77316
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 17448 0 0 0 38950 54 0 0 25 0 1 0 429609354 79568896 17087 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19426 17087 603 41 0 19385 0
vsize: 77704
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 17546 0 0 0 39950 54 0 0 25 0 1 0 429609354 79966208 17185 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19523 17185 603 41 0 19482 0
vsize: 78092
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 17609 0 0 0 40950 54 0 0 25 0 1 0 429609354 80236544 17248 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19589 17248 603 41 0 19548 0
vsize: 78356
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 17662 0 0 0 41950 54 0 0 25 0 1 0 429609354 80502784 17301 4294967295 134512640 134672761 3221224528 3221223664 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19654 17301 603 41 0 19613 0
vsize: 78616
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 17727 0 0 0 42950 55 0 0 25 0 1 0 429609354 80637952 17366 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19687 17366 603 41 0 19646 0
vsize: 78748
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27373
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 17805 0 0 0 43950 55 0 0 25 0 1 0 429609354 81039360 17444 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19785 17444 603 41 0 19744 0
vsize: 79140
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 17883 0 0 0 44949 55 0 0 25 0 1 0 429609354 81252352 17506 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19837 17506 603 41 0 19796 0
vsize: 79348
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 17960 0 0 0 45950 55 0 0 25 0 1 0 429609354 81522688 17583 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19903 17583 603 41 0 19862 0
vsize: 79612
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 18052 0 0 0 46950 55 0 0 25 0 1 0 429609354 81928192 17675 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20002 17675 603 41 0 19961 0
vsize: 80008
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 18169 0 0 0 47950 56 0 0 25 0 1 0 429609354 82341888 17792 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20103 17792 603 41 0 20062 0
vsize: 80412
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 18421 0 0 0 48948 57 0 0 25 0 1 0 429609354 83394560 18044 4294967295 134512640 134672761 3221224528 3221223632 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20360 18044 603 41 0 20319 0
vsize: 81440
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 18737 0 0 0 49948 58 0 0 25 0 1 0 429609354 84721664 18360 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20684 18360 603 41 0 20643 0
vsize: 82736
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 18817 0 0 0 50948 58 0 0 25 0 1 0 429609354 84992000 18440 4294967295 134512640 134672761 3221224528 3221223712 134558513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20750 18440 603 41 0 20709 0
vsize: 83000
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 18937 0 0 0 51948 58 0 0 25 0 1 0 429609354 85524480 18560 4294967295 134512640 134672761 3221224528 3221223712 134559139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20880 18560 603 41 0 20839 0
vsize: 83520
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 19040 0 0 0 52947 59 0 0 25 0 1 0 429609354 85917696 18663 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20976 18663 603 41 0 20935 0
vsize: 83904
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 19087 0 0 0 53947 59 0 0 25 0 1 0 429609354 86188032 18710 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21042 18710 603 41 0 21001 0
vsize: 84168
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 19165 0 0 0 54947 59 0 0 25 0 1 0 429609354 86458368 18788 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21108 18788 603 41 0 21067 0
vsize: 84432
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 19278 0 0 0 55947 59 0 0 25 0 1 0 429609354 86847488 18901 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21203 18901 603 41 0 21162 0
vsize: 84812
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 19355 0 0 0 56948 59 0 0 25 0 1 0 429609354 87236608 18978 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21298 18978 603 41 0 21257 0
vsize: 85192
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 19447 0 0 0 57948 59 0 0 25 0 1 0 429609354 87506944 19070 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21364 19070 603 41 0 21323 0
vsize: 85456
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 19511 0 0 0 58948 59 0 0 25 0 1 0 429609354 87695360 19117 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21410 19117 603 41 0 21369 0
vsize: 85640
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 19546 0 0 0 59948 59 0 0 25 0 1 0 429609354 87957504 19152 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21474 19152 603 41 0 21433 0
vsize: 85896
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 19602 0 0 0 60948 60 0 0 25 0 1 0 429609354 88088576 19208 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21506 19208 603 41 0 21465 0
vsize: 86024
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 19643 0 0 0 61948 60 0 0 25 0 1 0 429609354 88481792 19249 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21602 19249 603 41 0 21561 0
vsize: 86408
[startup+630.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 19744 0 0 0 62947 61 0 0 25 0 1 0 429609354 89018368 19350 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21733 19350 603 41 0 21692 0
vsize: 86932
[startup+640.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 19852 0 0 0 63947 61 0 0 25 0 1 0 429609354 89419776 19458 4294967295 134512640 134672761 3221224528 3221223692 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21831 19458 603 41 0 21790 0
vsize: 87324
[startup+650.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 19980 0 0 0 64947 62 0 0 25 0 1 0 429609354 89956352 19586 4294967295 134512640 134672761 3221224528 3221223696 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21962 19586 603 41 0 21921 0
vsize: 87848
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 20001 0 0 0 65946 62 0 0 25 0 1 0 429609354 89956352 19607 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21962 19607 603 41 0 21921 0
vsize: 87848
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 20045 0 0 0 66947 62 0 0 25 0 1 0 429609354 90222592 19651 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22027 19651 603 41 0 21986 0
vsize: 88108
[startup+680.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 20194 0 0 0 67946 62 0 0 25 0 1 0 429609354 90759168 19800 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22158 19800 603 41 0 22117 0
vsize: 88632
[startup+690.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 20304 0 0 0 68947 62 0 0 25 0 1 0 429609354 91295744 19910 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22289 19910 603 41 0 22248 0
vsize: 89156
[startup+700.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 20429 0 0 0 69946 63 0 0 25 0 1 0 429609354 91705344 20035 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22389 20035 603 41 0 22348 0
vsize: 89556
[startup+710.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 20623 0 0 0 70946 63 0 0 25 0 1 0 429609354 92516352 20229 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22587 20229 603 41 0 22546 0
vsize: 90348
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 20858 0 0 0 71946 64 0 0 25 0 1 0 429609354 93458432 20464 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22817 20464 603 41 0 22776 0
vsize: 91268
[startup+730.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 20967 0 0 0 72945 64 0 0 25 0 1 0 429609354 93999104 20573 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22949 20573 603 41 0 22908 0
vsize: 91796
[startup+740.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27375
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 21035 0 0 0 73945 65 0 0 25 0 1 0 429609354 94269440 20641 4294967295 134512640 134672761 3221224528 3221223696 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23015 20641 603 41 0 22974 0
vsize: 92060
[startup+750.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 21120 0 0 0 74945 65 0 0 25 0 1 0 429609354 94539776 20726 4294967295 134512640 134672761 3221224528 3221223664 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23081 20726 603 41 0 23040 0
vsize: 92324
[startup+760.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 21199 0 0 0 75945 65 0 0 25 0 1 0 429609354 94941184 20805 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23179 20805 603 41 0 23138 0
vsize: 92716
[startup+770.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 21289 0 0 0 76945 65 0 0 25 0 1 0 429609354 95211520 20895 4294967295 134512640 134672761 3221224528 3221223668 134560629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23245 20895 603 41 0 23204 0
vsize: 92980
[startup+780.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 21359 0 0 0 77945 66 0 0 25 0 1 0 429609354 95481856 20965 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23311 20965 603 41 0 23270 0
vsize: 93244
[startup+790.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 21438 0 0 0 78945 66 0 0 25 0 1 0 429609354 95883264 21044 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23409 21044 603 41 0 23368 0
vsize: 93636
[startup+800.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 21486 0 0 0 79945 66 0 0 25 0 1 0 429609354 96018432 21092 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23442 21092 603 41 0 23401 0
vsize: 93768
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 21553 0 0 0 80945 66 0 0 25 0 1 0 429609354 96280576 21159 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23506 21159 603 41 0 23465 0
vsize: 94024
[startup+820.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 21626 0 0 0 81945 67 0 0 25 0 1 0 429609354 96681984 21232 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23604 21232 603 41 0 23563 0
vsize: 94416
[startup+830.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 21696 0 0 0 82945 67 0 0 25 0 1 0 429609354 96952320 21302 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23670 21302 603 41 0 23629 0
vsize: 94680
[startup+840.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 21759 0 0 0 83945 67 0 0 25 0 1 0 429609354 97218560 21365 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23735 21365 603 41 0 23694 0
vsize: 94940
[startup+850.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 21914 0 0 0 84945 67 0 0 25 0 1 0 429609354 97746944 21520 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23864 21520 603 41 0 23823 0
vsize: 95456
[startup+860.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 22009 0 0 0 85944 68 0 0 25 0 1 0 429609354 98144256 21615 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23961 21615 603 41 0 23920 0
vsize: 95844
[startup+870.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 22110 0 0 0 86944 68 0 0 25 0 1 0 429609354 98545664 21716 4294967295 134512640 134672761 3221224528 3221223728 134557820 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24059 21716 603 41 0 24018 0
vsize: 96236
[startup+880.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 22264 0 0 0 87944 69 0 0 25 0 1 0 429609354 99213312 21870 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24222 21870 603 41 0 24181 0
vsize: 96888
[startup+890.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 22443 0 0 0 88943 69 0 0 25 0 1 0 429609354 100007936 22049 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24416 22049 603 41 0 24375 0
vsize: 97664
[startup+900.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 22576 0 0 0 89943 70 0 0 25 0 1 0 429609354 100544512 22182 4294967295 134512640 134672761 3221224528 3221223696 134561272 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24547 22182 603 41 0 24506 0
vsize: 98188
[startup+910.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 22692 0 0 0 90943 70 0 0 25 0 1 0 429609354 100941824 22298 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24644 22298 603 41 0 24603 0
vsize: 98576
[startup+920.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 22816 0 0 0 91943 70 0 0 25 0 1 0 429609354 101474304 22422 4294967295 134512640 134672761 3221224528 3221223728 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24774 22422 603 41 0 24733 0
vsize: 99096
[startup+930.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 22907 0 0 0 92943 70 0 0 25 0 1 0 429609354 101875712 22513 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24872 22513 603 41 0 24831 0
vsize: 99488
[startup+940.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 22971 0 0 0 93943 71 0 0 25 0 1 0 429609354 102137856 22577 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24936 22577 603 41 0 24895 0
vsize: 99744
[startup+950.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 23073 0 0 0 94942 71 0 0 25 0 1 0 429609354 102535168 22679 4294967295 134512640 134672761 3221224528 3221223632 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25033 22679 603 41 0 24992 0
vsize: 100132
[startup+960.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 23250 0 0 0 95942 72 0 0 25 0 1 0 429609354 103186432 22856 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25192 22856 603 41 0 25151 0
vsize: 100768
[startup+970.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 23428 0 0 0 96942 72 0 0 25 0 1 0 429609354 103968768 23034 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25383 23034 603 41 0 25342 0
vsize: 101532
[startup+980.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 23642 0 0 0 97941 73 0 0 25 0 1 0 429609354 104804352 23248 4294967295 134512640 134672761 3221224528 3221223632 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25587 23248 603 41 0 25546 0
vsize: 102348
[startup+990.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 23771 0 0 0 98941 73 0 0 25 0 1 0 429609354 105353216 23377 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25721 23377 603 41 0 25680 0
vsize: 102884
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 23921 0 0 0 99941 74 0 0 25 0 1 0 429609354 106020864 23527 4294967295 134512640 134672761 3221224528 3221223632 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25884 23527 603 41 0 25843 0
vsize: 103536
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 24147 0 0 0 100940 75 0 0 25 0 1 0 429609354 106827776 23753 4294967295 134512640 134672761 3221224528 3221223632 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26081 23753 603 41 0 26040 0
vsize: 104324
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 24352 0 0 0 101940 75 0 0 25 0 1 0 429609354 107773952 23958 4294967295 134512640 134672761 3221224528 3221223712 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26312 23958 603 41 0 26271 0
vsize: 105248
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 24576 0 0 0 102939 76 0 0 25 0 1 0 429609354 108707840 24182 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26540 24182 603 41 0 26499 0
vsize: 106160
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27377
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 24776 0 0 0 103939 76 0 0 25 0 1 0 429609354 109514752 24382 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26737 24382 603 41 0 26696 0
vsize: 106948
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27379
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 24994 0 0 0 104939 76 0 0 25 0 1 0 429609354 110333952 24600 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26937 24600 603 41 0 26896 0
vsize: 107748
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27379
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 25160 0 0 0 105939 77 0 0 25 0 1 0 429609354 111001600 24766 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27100 24766 603 41 0 27059 0
vsize: 108400
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27379
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 25361 0 0 0 106939 77 0 0 25 0 1 0 429609354 111804416 24967 4294967295 134512640 134672761 3221224528 3221223664 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27296 24967 603 41 0 27255 0
vsize: 109184
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27379
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 25574 0 0 0 107938 78 0 0 25 0 1 0 429609354 112734208 25180 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27523 25180 603 41 0 27482 0
vsize: 110092
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27379
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 25793 0 0 0 108938 78 0 0 25 0 1 0 429609354 113651712 25399 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27747 25399 603 41 0 27706 0
vsize: 110988
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27379
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 25961 0 0 0 109938 79 0 0 25 0 1 0 429609354 114323456 25567 4294967295 134512640 134672761 3221224528 3221223696 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27911 25567 603 41 0 27870 0
vsize: 111644
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27379
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 26028 0 0 0 110938 79 0 0 25 0 1 0 429609354 114438144 25617 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27939 25617 603 41 0 27898 0
vsize: 111756
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27379
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 26109 0 0 0 111938 79 0 0 25 0 1 0 429609354 114855936 25698 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28041 25698 603 41 0 28000 0
vsize: 112164
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27379
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 26204 0 0 0 112937 80 0 0 25 0 1 0 429609354 115077120 25776 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28095 25776 603 41 0 28054 0
vsize: 112380
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27379
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 26222 0 0 0 113937 80 0 0 25 0 1 0 429609354 115204096 25794 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28126 25794 603 41 0 28085 0
vsize: 112504
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27379
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 26264 0 0 0 114937 80 0 0 25 0 1 0 429609354 115339264 25836 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28159 25836 603 41 0 28118 0
vsize: 112636
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27379
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 26291 0 0 0 115937 80 0 0 25 0 1 0 429609354 115474432 25863 4294967295 134512640 134672761 3221224528 3221223700 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28192 25863 603 41 0 28151 0
vsize: 112768
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27379
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 26391 0 0 0 116937 80 0 0 25 0 1 0 429609354 115884032 25963 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28292 25963 603 41 0 28251 0
vsize: 113168
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27379
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 26449 0 0 0 117937 80 0 0 25 0 1 0 429609354 116158464 26021 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28359 26021 603 41 0 28318 0
vsize: 113436
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27379
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 26509 0 0 0 118937 80 0 0 25 0 1 0 429609354 116424704 26081 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28424 26081 603 41 0 28383 0
vsize: 113696
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 27379
Raw data (stat): 27371 (minisat+) R 27370 12452 12451 0 -1 0 26656 0 0 0 119936 81 0 0 25 0 1 0 429609354 116965376 26228 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28556 26228 603 41 0 28515 0
vsize: 114224
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.97 1/56 27379
Raw data (stat): 27371 (minisat+) Z 27370 12452 12451 0 -1 12 26659 0 0 0 119937 87 0 0 25 0 1 0 429609354 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.08
CPU time (s): 1200.24
CPU user time (s): 1199.37
CPU system time (s): 0.870867
CPU usage (%): 100.014
Max. virtual memory (Kb): 114224
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####