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 14813

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-21 01:31:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19227 boxname=wulflinc8 idbench=1479 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  31a8734340f0544712ef974997c104b2  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-ran10x10c.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-ran10x10c.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-ran10x10c.opb
IDLAUNCH: 19227
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        627168 kB
Buffers:         34184 kB
Cached:         350628 kB
SwapCached:          0 kB
Active:         154188 kB
Inactive:       233472 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        626916 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            14132 kB
Committed_AS:    63560 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 01:51:52 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 19227 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]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 1972     Base: 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost: 2017     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 132]---> Sorter-cost: 1972     Base: 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 1972     Base: 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 1442     Base: 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 1972     Base: 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 1934     Base: 2 2 2 2 2 2 2 2
c ---[ 122]---> Sorter-cost: 1972     Base: 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 2017     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 1780     Base: 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 2045     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Sorter-cost: 1780     Base: 2 2 2 2 2 2 2
c ---[ 112]---> Sorter-cost: 2045     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Adder-cost: 178   maxlim: 8182   bits: 14/13
c ---[ 108]---> Adder-cost: 178   maxlim: 8438   bits: 14/14
c ---[ 106]---> Sorter-cost: 2013     Base: 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 2013     Base: 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 2045     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Sorter-cost: 1780     Base: 2 2 2 2 2 2 2
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 |   92067   220641 |   30689       0        0     nan |  0.000 % |
c |       100 |   92067   220641 |   33757     100      836     8.4 |  6.867 % |
c |       250 |   92067   220641 |   37133     250     1655     6.6 |  6.867 % |
c |       475 |   92067   220641 |   40847     475     2595     5.5 |  6.867 % |
c |       812 |   92067   220641 |   44931     812     4889     6.0 |  6.867 % |
c |      1318 |   91950   220378 |   49424    1313     7598     5.8 |  6.972 % |
c |      2077 |   91950   220378 |   54367    2072    12620     6.1 |  6.972 % |
c |      3216 |   91855   220161 |   59804    3208    19522     6.1 |  7.070 % |
c |      4924 |   91718   219849 |   65784    4914    30507     6.2 |  7.186 % |
c |      7486 |   91489   219267 |   72363    7450    46135     6.2 |  7.376 % |
c ==============================================================================
c [1mFound solution: 10935304[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4057   maxlim: 2046616   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8902 |  119679   320080 |   39893    8858    56033     6.3 |  7.376 % |
c |      9002 |  119655   320027 |   43882    8956    56572     6.3 |  6.690 % |
c |      9152 |  119592   319884 |   48270    9101    57367     6.3 |  6.739 % |
c |      9377 |  119514   319705 |   53097    9320    58674     6.3 |  6.799 % |
c |      9714 |  119497   319654 |   58407    9656    60525     6.3 |  6.810 % |
c ==============================================================================
c [1mFound solution: 10602252[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 8   maxlim: 2379668   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10147 |  119517   319867 |   39839   10085    63450     6.3 |  6.810 % |
c |     10247 |  119517   319867 |   43822   10185    64029     6.3 |  6.858 % |
c |     10397 |  119517   319867 |   48205   10335    64926     6.3 |  6.858 % |
c |     10622 |  119418   319646 |   53025   10548    66592     6.3 |  6.934 % |
c |     10959 |  119418   319646 |   58328   10885    68899     6.3 |  6.934 % |
c |     11465 |  119418   319646 |   64161   11391    75103     6.6 |  6.934 % |
c ==============================================================================
c [1mFound solution: 8817553[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 4164367   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12130 |  119106   319007 |   39702   12029    87601     7.3 |  6.934 % |
c |     12230 |  119106   319007 |   43672   12129    88114     7.3 |  7.231 % |
c |     12380 |  119084   318958 |   48039   12278    88870     7.2 |  7.247 % |
c |     12607 |  118986   318729 |   52843   12499    90930     7.3 |  7.326 % |
c |     12944 |  118986   318729 |   58127   12836    93360     7.3 |  7.326 % |
c |     13451 |  118986   318729 |   63940   13343   122213     9.2 |  7.326 % |
c |     14210 |  118825   318357 |   70334   14092   127330     9.0 |  7.457 % |
c |     15350 |  118825   318357 |   77367   15232   165598    10.9 |  7.457 % |
c |     17059 |  118825   318357 |   85104   16941   317794    18.8 |  7.457 % |
c ==============================================================================
c [1mFound solution: 7851911[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 5130009   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17710 |  118838   318525 |   39612   17589   328369    18.7 |  7.457 % |
c |     17810 |  118838   318525 |   43573   17689   328929    18.6 |  7.507 % |
c |     17960 |  118808   318458 |   47930   17837   329627    18.5 |  7.532 % |
c |     18186 |  118808   318458 |   52723   18063   331008    18.3 |  7.532 % |
c |     18525 |  118714   318245 |   57995   18391   333003    18.1 |  7.605 % |
c |     19031 |  118714   318245 |   63795   18897   338939    17.9 |  7.605 % |
c |     19790 |  118714   318245 |   70175   19656   367751    18.7 |  7.605 % |
c ==============================================================================
c [1mFound solution: 6698230[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6283690   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20368 |  118737   318451 |   39579   20234   432172    21.4 |  7.605 % |
c |     20469 |  118702   318372 |   43536   20334   432685    21.3 |  7.664 % |
c |     20619 |  118657   318268 |   47890   20472   433480    21.2 |  7.703 % |
c |     20844 |  118576   318082 |   52679   20682   451469    21.8 |  7.762 % |
c |     21181 |  118545   317979 |   57947   21011   462208    22.0 |  7.776 % |
c |     21687 |  118545   317979 |   63742   21517   468614    21.8 |  7.776 % |
c |     22447 |  118545   317979 |   70116   22277   491944    22.1 |  7.776 % |
c |     23587 |  118525   317935 |   77128   23415   512738    21.9 |  7.792 % |
c |     25297 |  118525   317935 |   84841   25125   775643    30.9 |  7.792 % |
c |     27862 |  118354   317522 |   93325   27637   942280    34.1 |  7.931 % |
c |     31710 |  118110   316966 |  102657   31461  1553703    49.4 |  8.119 % |
c |     37477 |  117851   316366 |  112923   37176  1891434    50.9 |  8.325 % |
c |     46127 |  117831   316304 |  124215   45822  3228113    70.4 |  8.336 % |
c ==============================================================================
c [1mFound solution: 6485043[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6496877   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57525 |  117776   316311 |   39258   57218  4010916    70.1 |  8.336 % |
c |     57625 |  117776   316311 |   43183   18585   855687    46.0 |  8.415 % |
c |     57775 |  117776   316311 |   47502   18735   857388    45.8 |  8.415 % |
c |     58000 |  117689   316113 |   52252   18956   858633    45.3 |  8.478 % |
c |     58337 |  117674   316080 |   57477   19292   860880    44.6 |  8.489 % |
c |     58844 |  117674   316080 |   63225   19799   867623    43.8 |  8.489 % |
c |     59604 |  117670   316070 |   69547   20558   880310    42.8 |  8.491 % |
c |     60744 |  117670   316070 |   76502   21698   914502    42.1 |  8.491 % |
c |     62453 |  117599   315905 |   84153   23406   974440    41.6 |  8.551 % |
c |     65015 |  117569   315836 |   92568   25966  1087674    41.9 |  8.578 % |
c |     68860 |  117554   315802 |  101825   29810  1311100    44.0 |  8.589 % |
c |     74627 |  117478   315629 |  112007   35571  1661907    46.7 |  8.652 % |
c |     83276 |  117414   315482 |  123208   44212  2143774    48.5 |  8.703 % |
c |     96250 |  117179   314943 |  135529   57164  3178733    55.6 |  8.894 % |
c |    115713 |  117175   314933 |  149082   76626  4444236    58.0 |  8.896 % |
c ==============================================================================
c [1mFound solution: 5071016[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7910904   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    123279 |  117198   315154 |   39066   84191  4856765    57.7 |  8.896 % |
c |    123379 |  117148   315041 |   42972   22049   834310    37.8 |  8.971 % |
c |    123529 |  117101   314931 |   47269   22183   835519    37.7 |  9.009 % |
c |    123754 |  117093   314912 |   51996   22405   837517    37.4 |  9.015 % |
c |    124091 |  117093   314912 |   57196   22742   841220    37.0 |  9.015 % |
c |    124597 |  116956   314597 |   62916   23236   849273    36.5 |  9.134 % |
c |    125357 |  116945   314573 |   69207   23995   893648    37.2 |  9.142 % |
c |    126496 |  116832   314310 |   76128   25114   940202    37.4 |  9.232 % |
c |    128205 |  116792   314220 |   83741   26821   972456    36.3 |  9.265 % |
c |    130768 |  116792   314220 |   92115   29384  1162580    39.6 |  9.265 % |
c |    134612 |  116792   314220 |  101327   33228  1672567    50.3 |  9.265 % |
c |    140379 |  116687   313978 |  111459   38978  2023176    51.9 |  9.360 % |
c |    149029 |  116429   313389 |  122605   47591  2599966    54.6 |  9.566 % |
c |    162003 |  116429   313389 |  134866   60565  3582029    59.1 |  9.566 % |
c |    181466 |  116137   312721 |  148353   80007  4984225    62.3 |  9.811 % |
c |    210659 |  115502   311247 |  163188  109153  8165075    74.8 | 10.335 % |
c |    254448 |  115475   311183 |  179507  152939 11737830    76.7 | 10.360 % |
c |    320132 |  115069   310235 |  197457   48523  2719147    56.0 | 10.705 % |
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_#### 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.85 0.97 0.93 2/54 20508
Raw data (stat): 20508 (runsolver) R 20507 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 469354636 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.87 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 5792 0 0 0 984 13 0 0 25 0 1 0 469354636 25337856 5131 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6186 5131 603 41 0 6145 0
vsize: 24744
[startup+20.0008 s]
Raw data (loadavg): 0.89 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 6006 0 0 0 1983 14 0 0 25 0 1 0 469354636 26157056 5333 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6386 5333 603 41 0 6345 0
vsize: 25544
[startup+30.0022 s]
Raw data (loadavg): 0.91 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 6404 0 0 0 2982 16 0 0 25 0 1 0 469354636 27693056 5690 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6761 5690 603 41 0 6720 0
vsize: 27044
[startup+40.0027 s]
Raw data (loadavg): 0.92 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 6591 0 0 0 3980 17 0 0 25 0 1 0 469354636 28495872 5877 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6957 5877 603 41 0 6916 0
vsize: 27828
[startup+50.0022 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 6973 0 0 0 4979 18 0 0 25 0 1 0 469354636 29958144 6259 4294967295 134512640 134672761 3221224544 3221223600 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7314 6259 603 41 0 7273 0
vsize: 29256
[startup+60.0023 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 7605 0 0 0 5978 20 0 0 25 0 1 0 469354636 32514048 6891 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7938 6891 603 41 0 7897 0
vsize: 31752
[startup+70.003 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 7902 0 0 0 6977 21 0 0 25 0 1 0 469354636 33845248 7188 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8263 7188 603 41 0 8222 0
vsize: 33052
[startup+80.0035 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 8177 0 0 0 7976 21 0 0 25 0 1 0 469354636 35065856 7463 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8561 7463 603 41 0 8520 0
vsize: 34244
[startup+90.0036 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 9026 0 0 0 8974 24 0 0 25 0 1 0 469354636 38432768 8312 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9383 8312 603 41 0 9342 0
vsize: 37532
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 9621 0 0 0 9973 25 0 0 25 0 1 0 469354636 40861696 8907 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9976 8907 603 41 0 9935 0
vsize: 39904
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 9916 0 0 0 10972 26 0 0 25 0 1 0 469354636 42074112 9202 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10272 9202 603 41 0 10231 0
vsize: 41088
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 10321 0 0 0 11971 27 0 0 25 0 1 0 469354636 43646976 9587 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10656 9587 603 41 0 10615 0
vsize: 42624
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 10321 0 0 0 12971 27 0 0 25 0 1 0 469354636 43646976 9587 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10656 9587 603 41 0 10615 0
vsize: 42624
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 10321 0 0 0 13971 27 0 0 25 0 1 0 469354636 43646976 9587 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10656 9587 603 41 0 10615 0
vsize: 42624
[startup+150.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 10321 0 0 0 14971 27 0 0 25 0 1 0 469354636 43646976 9587 4294967295 134512640 134672761 3221224544 3221223744 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10656 9587 603 41 0 10615 0
vsize: 42624
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 10321 0 0 0 15972 27 0 0 25 0 1 0 469354636 43646976 9587 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10656 9587 603 41 0 10615 0
vsize: 42624
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 10321 0 0 0 16972 27 0 0 25 0 1 0 469354636 43646976 9587 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10656 9587 603 41 0 10615 0
vsize: 42624
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 10321 0 0 0 17972 27 0 0 25 0 1 0 469354636 43646976 9587 4294967295 134512640 134672761 3221224544 3221223600 134565070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10656 9587 603 41 0 10615 0
vsize: 42624
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 10322 0 0 0 18972 27 0 0 25 0 1 0 469354636 43646976 9588 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10656 9588 603 41 0 10615 0
vsize: 42624
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 10328 0 0 0 19972 27 0 0 25 0 1 0 469354636 43646976 9594 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10656 9594 603 41 0 10615 0
vsize: 42624
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 10339 0 0 0 20973 27 0 0 25 0 1 0 469354636 43909120 9605 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10720 9605 603 41 0 10679 0
vsize: 42880
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 10683 0 0 0 21972 28 0 0 25 0 1 0 469354636 45387776 9949 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11081 9949 603 41 0 11040 0
vsize: 44324
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 11040 0 0 0 22971 30 0 0 25 0 1 0 469354636 46731264 10306 4294967295 134512640 134672761 3221224544 3221223680 134560650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11409 10306 603 41 0 11368 0
vsize: 45636
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 11235 0 0 0 23970 31 0 0 25 0 1 0 469354636 47538176 10501 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11606 10501 603 41 0 11565 0
vsize: 46424
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 11536 0 0 0 24969 32 0 0 25 0 1 0 469354636 48750592 10802 4294967295 134512640 134672761 3221224544 3221223728 134559489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11902 10802 603 41 0 11861 0
vsize: 47608
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 11625 0 0 0 25969 33 0 0 25 0 1 0 469354636 49086464 10870 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11984 10870 603 41 0 11943 0
vsize: 47936
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 11625 0 0 0 26969 33 0 0 25 0 1 0 469354636 49086464 10870 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11984 10870 603 41 0 11943 0
vsize: 47936
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 11625 0 0 0 27969 33 0 0 25 0 1 0 469354636 49086464 10870 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11984 10870 603 41 0 11943 0
vsize: 47936
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 11625 0 0 0 28969 33 0 0 25 0 1 0 469354636 49086464 10870 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11984 10870 603 41 0 11943 0
vsize: 47936
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 11625 0 0 0 29969 33 0 0 25 0 1 0 469354636 49086464 10870 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11984 10870 603 41 0 11943 0
vsize: 47936
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 11625 0 0 0 30969 33 0 0 25 0 1 0 469354636 49086464 10870 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11984 10870 603 41 0 11943 0
vsize: 47936
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 11625 0 0 0 31970 33 0 0 25 0 1 0 469354636 49086464 10870 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11984 10870 603 41 0 11943 0
vsize: 47936
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 11625 0 0 0 32970 33 0 0 25 0 1 0 469354636 49086464 10870 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11984 10870 603 41 0 11943 0
vsize: 47936
[startup+340.012 s]
Raw data (loadavg): 1.07 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 11625 0 0 0 33970 33 0 0 25 0 1 0 469354636 49086464 10870 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11984 10870 603 41 0 11943 0
vsize: 47936
[startup+350.012 s]
Raw data (loadavg): 1.06 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 11625 0 0 0 34969 33 0 0 25 0 1 0 469354636 49086464 10870 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11984 10870 603 41 0 11943 0
vsize: 47936
[startup+360.013 s]
Raw data (loadavg): 1.05 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 11625 0 0 0 35969 33 0 0 25 0 1 0 469354636 49086464 10870 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11984 10870 603 41 0 11943 0
vsize: 47936
[startup+370.013 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 11625 0 0 0 36969 33 0 0 25 0 1 0 469354636 49086464 10870 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11984 10870 603 41 0 11943 0
vsize: 47936
[startup+380.013 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 11625 0 0 0 37970 33 0 0 25 0 1 0 469354636 49086464 10870 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11984 10870 603 41 0 11943 0
vsize: 47936
[startup+390.014 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 11625 0 0 0 38970 33 0 0 25 0 1 0 469354636 49086464 10870 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11984 10870 603 41 0 11943 0
vsize: 47936
[startup+400.014 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 11675 0 0 0 39970 34 0 0 25 0 1 0 469354636 49352704 10920 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12049 10920 603 41 0 12008 0
vsize: 48196
[startup+410.014 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 11831 0 0 0 40970 34 0 0 25 0 1 0 469354636 49881088 11076 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12178 11076 603 41 0 12137 0
vsize: 48712
[startup+420.019 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 11965 0 0 0 41970 34 0 0 25 0 1 0 469354636 50417664 11210 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12309 11210 603 41 0 12268 0
vsize: 49236
[startup+430.023 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 12262 0 0 0 42970 34 0 0 25 0 1 0 469354636 51757056 11507 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12636 11507 603 41 0 12595 0
vsize: 50544
[startup+440.023 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 13168 0 0 0 43969 36 0 0 25 0 1 0 469354636 55353344 12413 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13514 12413 603 41 0 13473 0
vsize: 54056
[startup+450.023 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 13827 0 0 0 44968 37 0 0 25 0 1 0 469354636 58036224 13072 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14169 13072 603 41 0 14128 0
vsize: 56676
[startup+460.024 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 14017 0 0 0 45967 38 0 0 25 0 1 0 469354636 58839040 13262 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14365 13262 603 41 0 14324 0
vsize: 57460
[startup+470.023 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 14325 0 0 0 46966 39 0 0 25 0 1 0 469354636 60047360 13570 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14660 13570 603 41 0 14619 0
vsize: 58640
[startup+480.024 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 14683 0 0 0 47966 40 0 0 25 0 1 0 469354636 61530112 13928 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15022 13928 603 41 0 14981 0
vsize: 60088
[startup+490.025 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 14914 0 0 0 48965 41 0 0 25 0 1 0 469354636 62484480 14159 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15255 14159 603 41 0 15214 0
vsize: 61020
[startup+500.025 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 15098 0 0 0 49965 41 0 0 25 0 1 0 469354636 63287296 14343 4294967295 134512640 134672761 3221224544 3221223600 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15451 14343 603 41 0 15410 0
vsize: 61804
[startup+510.026 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 15276 0 0 0 50965 42 0 0 25 0 1 0 469354636 63971328 14521 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15618 14521 603 41 0 15577 0
vsize: 62472
[startup+520.025 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 15517 0 0 0 51964 42 0 0 25 0 1 0 469354636 64921600 14762 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15850 14762 603 41 0 15809 0
vsize: 63400
[startup+530.026 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 15674 0 0 0 52964 43 0 0 25 0 1 0 469354636 65597440 14919 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16015 14919 603 41 0 15974 0
vsize: 64060
[startup+540.026 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 15859 0 0 0 53963 44 0 0 25 0 1 0 469354636 66404352 15104 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16212 15104 603 41 0 16171 0
vsize: 64848
[startup+550.026 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 16065 0 0 0 54962 45 0 0 25 0 1 0 469354636 67215360 15310 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16410 15310 603 41 0 16369 0
vsize: 65640
[startup+560.026 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 16260 0 0 0 55962 45 0 0 25 0 1 0 469354636 67891200 15505 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16575 15505 603 41 0 16534 0
vsize: 66300
[startup+570.026 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 16494 0 0 0 56962 46 0 0 25 0 1 0 469354636 68964352 15739 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16837 15739 603 41 0 16796 0
vsize: 67348
[startup+580.027 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 16649 0 0 0 57961 46 0 0 25 0 1 0 469354636 69505024 15894 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16969 15894 603 41 0 16928 0
vsize: 67876
[startup+590.028 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 17033 0 0 0 58961 47 0 0 25 0 1 0 469354636 71643136 16278 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17491 16278 603 41 0 17450 0
vsize: 69964
[startup+600.027 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 17221 0 0 0 59961 47 0 0 25 0 1 0 469354636 72454144 16466 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17689 16466 603 41 0 17648 0
vsize: 70756
[startup+610.028 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 17508 0 0 0 60960 48 0 0 25 0 1 0 469354636 73658368 16753 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17983 16753 603 41 0 17942 0
vsize: 71932
[startup+620.028 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 17759 0 0 0 61960 48 0 0 25 0 1 0 469354636 74596352 17004 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18212 17004 603 41 0 18171 0
vsize: 72848
[startup+630.029 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 17990 0 0 0 62960 49 0 0 25 0 1 0 469354636 75538432 17235 4294967295 134512640 134672761 3221224544 3221223728 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18442 17235 603 41 0 18401 0
vsize: 73768
[startup+640.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 18204 0 0 0 63960 49 0 0 25 0 1 0 469354636 76484608 17449 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18673 17449 603 41 0 18632 0
vsize: 74692
[startup+650.029 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 18495 0 0 0 64959 50 0 0 25 0 1 0 469354636 77561856 17740 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18936 17740 603 41 0 18895 0
vsize: 75744
[startup+660.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 18738 0 0 0 65959 50 0 0 25 0 1 0 469354636 78643200 17983 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19200 17983 603 41 0 19159 0
vsize: 76800
[startup+670.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 19005 0 0 0 66959 51 0 0 25 0 1 0 469354636 79716352 18250 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19462 18250 603 41 0 19421 0
vsize: 77848
[startup+680.031 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 19180 0 0 0 67958 51 0 0 25 0 1 0 469354636 80384000 18425 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19625 18425 603 41 0 19584 0
vsize: 78500
[startup+690.031 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 19310 0 0 0 68957 52 0 0 25 0 1 0 469354636 80920576 18555 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19756 18555 603 41 0 19715 0
vsize: 79024
[startup+700.031 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 19452 0 0 0 69956 53 0 0 25 0 1 0 469354636 81461248 18697 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19888 18697 603 41 0 19847 0
vsize: 79552
[startup+710.032 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 19609 0 0 0 70956 54 0 0 25 0 1 0 469354636 82137088 18854 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20053 18854 603 41 0 20012 0
vsize: 80212
[startup+720.032 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 19759 0 0 0 71955 54 0 0 25 0 1 0 469354636 82808832 19004 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20217 19004 603 41 0 20176 0
vsize: 80868
[startup+730.033 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 19929 0 0 0 72955 55 0 0 25 0 1 0 469354636 83480576 19174 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20381 19174 603 41 0 20340 0
vsize: 81524
[startup+740.034 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 20114 0 0 0 73955 55 0 0 25 0 1 0 469354636 84164608 19359 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20548 19359 603 41 0 20507 0
vsize: 82192
[startup+750.033 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 20351 0 0 0 74954 56 0 0 25 0 1 0 469354636 85110784 19596 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20779 19596 603 41 0 20738 0
vsize: 83116
[startup+760.033 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 20543 0 0 0 75953 57 0 0 25 0 1 0 469354636 85921792 19788 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20977 19788 603 41 0 20936 0
vsize: 83908
[startup+770.033 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 20649 0 0 0 76953 57 0 0 25 0 1 0 469354636 86482944 19894 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21114 19894 603 41 0 21073 0
vsize: 84456
[startup+780.033 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 20741 0 0 0 77953 58 0 0 25 0 1 0 469354636 86753280 19986 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21180 19986 603 41 0 21139 0
vsize: 84720
[startup+790.034 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 20866 0 0 0 78953 58 0 0 25 0 1 0 469354636 87289856 20111 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21311 20111 603 41 0 21270 0
vsize: 85244
[startup+800.033 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 21582 0 0 0 79951 60 0 0 25 0 1 0 469354636 90259456 20827 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22036 20827 603 41 0 21995 0
vsize: 88144
[startup+810.034 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 21846 0 0 0 80950 61 0 0 25 0 1 0 469354636 91332608 21091 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22298 21091 603 41 0 22257 0
vsize: 89192
[startup+820.034 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 21977 0 0 0 81950 61 0 0 25 0 1 0 469354636 91869184 21222 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22429 21222 603 41 0 22388 0
vsize: 89716
[startup+830.035 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22094 0 0 0 82950 61 0 0 25 0 1 0 469354636 92278784 21339 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22529 21339 603 41 0 22488 0
vsize: 90116
[startup+840.034 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22204 0 0 0 83950 62 0 0 25 0 1 0 469354636 92680192 21449 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22627 21449 603 41 0 22586 0
vsize: 90508
[startup+850.036 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22341 0 0 0 84950 62 0 0 25 0 1 0 469354636 93351936 21586 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22791 21586 603 41 0 22750 0
vsize: 91164
[startup+860.036 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22485 0 0 0 85949 63 0 0 25 0 1 0 469354636 93892608 21730 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22923 21730 603 41 0 22882 0
vsize: 91692
[startup+870.035 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22644 0 0 0 86949 64 0 0 25 0 1 0 469354636 94568448 21889 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23088 21889 603 41 0 23047 0
vsize: 92352
[startup+880.037 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22701 0 0 0 87949 64 0 0 25 0 1 0 469354636 94838784 21946 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21946 603 41 0 23113 0
vsize: 92616
[startup+890.037 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22701 0 0 0 88949 64 0 0 25 0 1 0 469354636 94838784 21946 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21946 603 41 0 23113 0
vsize: 92616
[startup+900.037 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22701 0 0 0 89949 64 0 0 25 0 1 0 469354636 94838784 21946 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21946 603 41 0 23113 0
vsize: 92616
[startup+910.037 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22701 0 0 0 90949 64 0 0 25 0 1 0 469354636 94838784 21946 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21946 603 41 0 23113 0
vsize: 92616
[startup+920.038 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22701 0 0 0 91950 64 0 0 25 0 1 0 469354636 94838784 21946 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21946 603 41 0 23113 0
vsize: 92616
[startup+930.038 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22701 0 0 0 92950 64 0 0 25 0 1 0 469354636 94838784 21946 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21946 603 41 0 23113 0
vsize: 92616
[startup+940.038 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22701 0 0 0 93950 64 0 0 25 0 1 0 469354636 94838784 21946 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21946 603 41 0 23113 0
vsize: 92616
[startup+950.039 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22701 0 0 0 94950 64 0 0 25 0 1 0 469354636 94838784 21946 4294967295 134512640 134672761 3221224544 3221223668 134566103 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21946 603 41 0 23113 0
vsize: 92616
[startup+960.039 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22701 0 0 0 95950 64 0 0 25 0 1 0 469354636 94838784 21946 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21946 603 41 0 23113 0
vsize: 92616
[startup+970.041 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22701 0 0 0 96950 64 0 0 25 0 1 0 469354636 94838784 21946 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21946 603 41 0 23113 0
vsize: 92616
[startup+980.041 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22701 0 0 0 97950 64 0 0 25 0 1 0 469354636 94838784 21946 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21946 603 41 0 23113 0
vsize: 92616
[startup+990.042 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22701 0 0 0 98950 64 0 0 25 0 1 0 469354636 94838784 21946 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23154 21946 603 41 0 23113 0
vsize: 92616
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22701 0 0 0 99949 64 0 0 25 0 1 0 469354636 94838784 21946 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21946 603 41 0 23113 0
vsize: 92616
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22701 0 0 0 100949 64 0 0 25 0 1 0 469354636 94838784 21946 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21946 603 41 0 23113 0
vsize: 92616
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22701 0 0 0 101949 64 0 0 25 0 1 0 469354636 94838784 21946 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21946 603 41 0 23113 0
vsize: 92616
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22701 0 0 0 102950 64 0 0 25 0 1 0 469354636 94838784 21946 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21946 603 41 0 23113 0
vsize: 92616
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22701 0 0 0 103950 64 0 0 25 0 1 0 469354636 94838784 21946 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21946 603 41 0 23113 0
vsize: 92616
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22701 0 0 0 104950 64 0 0 25 0 1 0 469354636 94838784 21946 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21946 603 41 0 23113 0
vsize: 92616
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22701 0 0 0 105950 64 0 0 25 0 1 0 469354636 94838784 21946 4294967295 134512640 134672761 3221224544 3221223680 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21946 603 41 0 23113 0
vsize: 92616
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22702 0 0 0 106950 64 0 0 25 0 1 0 469354636 94838784 21947 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21947 603 41 0 23113 0
vsize: 92616
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22702 0 0 0 107951 64 0 0 25 0 1 0 469354636 94838784 21947 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21947 603 41 0 23113 0
vsize: 92616
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22703 0 0 0 108951 64 0 0 25 0 1 0 469354636 94838784 21948 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21948 603 41 0 23113 0
vsize: 92616
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22704 0 0 0 109951 64 0 0 25 0 1 0 469354636 94838784 21949 4294967295 134512640 134672761 3221224544 3221223600 1075349616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21949 603 41 0 23113 0
vsize: 92616
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22704 0 0 0 110951 64 0 0 25 0 1 0 469354636 94838784 21949 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21949 603 41 0 23113 0
vsize: 92616
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22704 0 0 0 111951 64 0 0 25 0 1 0 469354636 94838784 21949 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21949 603 41 0 23113 0
vsize: 92616
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22704 0 0 0 112952 64 0 0 25 0 1 0 469354636 94838784 21949 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21949 603 41 0 23113 0
vsize: 92616
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22705 0 0 0 113952 64 0 0 25 0 1 0 469354636 94838784 21950 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21950 603 41 0 23113 0
vsize: 92616
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22707 0 0 0 114952 64 0 0 25 0 1 0 469354636 94838784 21952 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21952 603 41 0 23113 0
vsize: 92616
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22707 0 0 0 115952 64 0 0 25 0 1 0 469354636 94838784 21952 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21952 603 41 0 23113 0
vsize: 92616
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22708 0 0 0 116952 64 0 0 25 0 1 0 469354636 94838784 21953 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21953 603 41 0 23113 0
vsize: 92616
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22708 0 0 0 117953 64 0 0 25 0 1 0 469354636 94838784 21953 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21953 603 41 0 23113 0
vsize: 92616
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22709 0 0 0 118953 64 0 0 25 0 1 0 469354636 94838784 21954 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21954 603 41 0 23113 0
vsize: 92616
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 20508
Raw data (stat): 20508 (minisat+) R 20507 26667 26666 0 -1 0 22709 0 0 0 119954 64 0 0 25 0 1 0 469354636 94838784 21954 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 21954 603 41 0 23113 0
vsize: 92616
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.94 1/54 20508
Raw data (stat): 20508 (minisat+) Z 20507 26667 26666 0 -1 12 22712 0 0 0 119954 69 0 0 25 0 1 0 469354636 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.11
CPU time (s): 1200.24
CPU user time (s): 1199.55
CPU system time (s): 0.691894
CPU usage (%): 100.011
Max. virtual memory (Kb): 92616
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####