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/MIPLIB/miplib/normalized-mps-v2-13-7-mod013.opb
MD5SUM	b964292d4197638ce79b3f213e8fe89b
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5130240
Optimality of the best value was proved	NO
Number of terms in the objective function	1008
Biggest coefficient in the objective function	366477312
Number of bits for the biggest coefficient in the objective function	29
Sum of the numbers in the objective function	12643636975
Number of bits of the sum of numbers in the objective function	34
Biggest number in a constraint	366477312
Number of bits of the biggest number in a constraint	29
Biggest sum of numbers in a constraint	12643636975
Number of bits of the biggest sum of numbers	34
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	1008
Total number of constraints	110
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	48
Number of constraints which are nor clauses,nor cardinality constraints	62
Minimum length of a constraint	1
Maximum length of a constraint	160
Trace number 19063

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-21 17:45:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17054 boxname=wulflinc1 idbench=1312 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b964292d4197638ce79b3f213e8fe89b  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-mod013.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-mod013.opb /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-mod013.opb
IDLAUNCH: 17054
/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:        738148 kB
Buffers:          7608 kB
Cached:         263372 kB
SwapCached:          0 kB
Active:          59040 kB
Inactive:       215092 kB
HighTotal:      131008 kB
HighFree:        14168 kB
LowTotal:       903652 kB
LowFree:        723980 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7220 kB
Slab:            16476 kB
Committed_AS:    92784 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:05:19 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 17054 7 1200.26 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 76 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############
c   -- Clauses(.)/Splits(s): (none)
c ---[  74]---> Sorter-cost:  970     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  72]---> Sorter-cost:  970     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  70]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[  68]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[  66]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[  64]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[  63]---> BDD-cost:   19
c ---[  62]---> BDD-cost:   16
c ---[  61]---> BDD-cost:   17
c ---[  60]---> BDD-cost:   15
c ---[  58]---> Sorter-cost: 1495     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> BDD-cost:   15
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   19
c ---[  52]---> BDD-cost:   16
c ---[  51]---> BDD-cost:   17
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   14
c ---[  46]---> Sorter-cost: 1495     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> BDD-cost:   14
c ---[  44]---> BDD-cost:   13
c ---[  43]---> BDD-cost:   16
c ---[  42]---> BDD-cost:   16
c ---[  41]---> BDD-cost:   17
c ---[  40]---> BDD-cost:   15
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   14
c ---[  37]---> BDD-cost:   14
c ---[  36]---> BDD-cost:   13
c ---[  34]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   15
c ---[  30]---> BDD-cost:   15
c ---[  29]---> BDD-cost:   15
c ---[  28]---> BDD-cost:   14
c ---[  27]---> BDD-cost:   14
c ---[  26]---> BDD-cost:   13
c ---[  25]---> BDD-cost:   14
c ---[  24]---> BDD-cost:   14
c ---[  22]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   14
c ---[  17]---> BDD-cost:   14
c ---[  16]---> BDD-cost:   13
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   13
c ---[  12]---> BDD-cost:   13
c ---[  10]---> Sorter-cost: 1391     Base: 2 2 2 2 2 2 2 2 2
c ---[   9]---> BDD-cost:   13
c ---[   8]---> BDD-cost:   13
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   13
c ---[   4]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  955     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  970     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   41833    98574 |   12549       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13458          
c   -- var.elim.:  2000/13458          
c   -- var.elim.:  3000/13458          
c   -- var.elim.:  4000/13458          
c   -- var.elim.:  5000/13458          
c   -- var.elim.:  6000/13458          
c   -- var.elim.:  7000/13458          
c   -- var.elim.:  8000/13458          
c   -- var.elim.:  9000/13458          
c   -- var.elim.:  10000/13458          
c   -- var.elim.:  11000/13458          
c   -- var.elim.:  12000/13458          
c   -- var.elim.:  13000/13458          
c   -- var.elim.:  13458/13458          
c   -- var.elim.:  1000/7655          
c   -- var.elim.:  2000/7655          
c   -- var.elim.:  3000/7655          
c   -- var.elim.:  4000/7655          
c   -- var.elim.:  5000/7655          
c   -- var.elim.:  6000/7655          
c   -- var.elim.:  7000/7655          
c   -- var.elim.:  7655/7655          
c   -- var.elim.:  160/160          
c   -- subsuming                       
c   -- var.elim.:  967/967          
c   -- var.elim.:  757/757          
c   -- var.elim.:  53/53          
c   -- var.elim.:  50/50          
c   -- var.elim.:  26/26          
c   -- subsuming                       
c   -- var.elim.:  279/279          
c   -- var.elim.:  113/113          
c |         0 |   35188   105208 |      --       0       --      -- |     --   | -4687/11532
c |         0 |   35188   105208 |   14075       0        0     nan |  0.000 % |
c |       100 |   35188   105208 |   15482     100      493     4.9 | 13.678 % |
c |       250 |   35188   105208 |   17030     250     1195     4.8 | 13.678 % |
c |       475 |   35188   105208 |   18734     475     2658     5.6 | 13.678 % |
c ==============================================================================
c (current CPU-time: 2.42763 s)
c ==============================================================================
c [1mFound solution: 12043788[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4334   maxlim: 18920675   bits: 25/25
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       661 |   65348   212943 |   19604     651     3657     5.6 | 13.678 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4970          
c   -- var.elim.:  2000/4970          
c   -- var.elim.:  3000/4970          
c   -- var.elim.:  4000/4970          
c   -- var.elim.:  4970/4970          
c   -- var.elim.:  94/94          
c |       661 |   65298   212946 |      --     651       --      -- |     --   | -46/37
c |       661 |   65298   212946 |   26119     651     3657     5.6 | 13.678 % |
c |       761 |   65298   212946 |   28731     751     4503     6.0 |  9.281 % |
c ==============================================================================
c (current CPU-time: 4.40033 s)
c ==============================================================================
c [1mFound solution: 12023261[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 18941202   bits: 25/25
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       874 |   65352   213233 |   19605     864     5297     6.1 |  9.281 % |
c   -- subsuming                       
c   -- var.elim.:  73/73          
c   -- var.elim.:  28/28          
c |       874 |   65336   213278 |      --     864       --      -- |     --   | -16/51
c |       874 |   65336   213278 |   26134     864     5297     6.1 |  9.281 % |
c |       974 |   65336   213278 |   28747     964     5884     6.1 |  9.318 % |
c |      1124 |   65336   213278 |   31622    1114     7199     6.5 |  9.318 % |
c |      1349 |   65336   213278 |   34784    1339     8328     6.2 |  9.318 % |
c ==============================================================================
c (current CPU-time: 6.36003 s)
c ==============================================================================
c [1mFound solution: 11052902[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 19911561   bits: 25/25
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1458 |   65386   213581 |   19615    1448    11791     8.1 |  9.318 % |
c   -- subsuming                       
c   -- var.elim.:  57/57          
c   -- var.elim.:  22/22          
c |      1458 |   65358   213266 |      --    1448       --      -- |     --   | -14/-49
c |      1458 |   65358   213266 |   26143    1448    11791     8.1 |  9.318 % |
c |      1558 |   65358   213266 |   28757    1548    17774    11.5 |  9.402 % |
c |      1709 |   65358   213266 |   31633    1699    31321    18.4 |  9.402 % |
c |      1934 |   65358   213266 |   34796    1924    32692    17.0 |  9.402 % |
c |      2272 |   65358   213266 |   38276    2262    44291    19.6 |  9.402 % |
c ==============================================================================
c (current CPU-time: 8.78466 s)
c ==============================================================================
c [1mFound solution: 8572680[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22391783   bits: 25/25
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2551 |   65417   213608 |   19625    2541    47474    18.7 |  9.402 % |
c   -- subsuming                       
c   -- var.elim.:  60/60          
c   -- var.elim.:  35/35          
c |      2551 |   65331   213037 |      --    2541       --      -- |     --   | -36/-32
c |      2551 |   65331   213037 |   26132    2536    47406    18.7 |  9.402 % |
c |      2651 |   65331   213037 |   28745    2636    48702    18.5 |  9.497 % |
c |      2801 |   65297   212900 |   31603    2785    49390    17.7 |  9.528 % |
c |      3026 |   65297   212900 |   34764    3010    50769    16.9 |  9.528 % |
c |      3364 |   65297   212900 |   38240    3348   140262    41.9 |  9.528 % |
c ==============================================================================
c (current CPU-time: 11.3613 s)
c ==============================================================================
c [1mFound solution: 8363822[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22600641   bits: 25/25
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3484 |   65362   213240 |   19608    3468   141441    40.8 |  9.528 % |
c   -- subsuming                       
c   -- var.elim.:  93/93          
c   -- var.elim.:  54/54          
c   -- var.elim.:  12/12          
c |      3484 |   65341   213182 |      --    3468       --      -- |     --   | -21/-48
c |      3484 |   65341   213182 |   26136    3467   141438    40.8 |  9.528 % |
c |      3584 |   65341   213182 |   28750    3567   142517    40.0 |  9.602 % |
c |      3736 |   65341   213182 |   31625    3719   165888    44.6 |  9.602 % |
c |      3961 |   65341   213182 |   34787    3944   168343    42.7 |  9.602 % |
c |      4298 |   65341   213182 |   38266    4281   228955    53.5 |  9.602 % |
c |      4804 |   65341   213182 |   42092    4787   353774    73.9 |  9.602 % |
c |      5563 |   65341   213182 |   46302    5546   500812    90.3 |  9.602 % |
c |      6703 |   65341   213182 |   50932    6686   805446   120.5 |  9.602 % |
c |      8412 |   65214   212707 |   55916    8392   864733   103.0 |  9.763 % |
c |     10974 |   65194   212643 |   61489   10950  1094403    99.9 |  9.779 % |
c |     14820 |   65101   212284 |   67542   14786  1573919   106.4 |  9.871 % |
c |     20586 |   65101   212284 |   74296   20552  3206798   156.0 |  9.871 % |
c |     29238 |   65101   212284 |   81725   29204  4179280   143.1 |  9.871 % |
c ==============================================================================
c (current CPU-time: 52.393 s)
c ==============================================================================
c [1mFound solution: 7653984[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23310479   bits: 25/25
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     31487 |   65123   212419 |   19536   31453  4340462   138.0 |  9.871 % |
c   -- subsuming                       
c   -- var.elim.:  212/212          
c   -- var.elim.:  147/147          
c   -- var.elim.:  21/21          
c   -- subsuming                       
c   -- var.elim.:  71/71          
c   -- var.elim.:  65/65          
c   -- var.elim.:  25/25          
c   -- var.elim.:  24/24          
c |     31487 |   64930   211872 |      --   31453       --      -- |     --   | -182/-395
c |     31487 |   64930   211872 |   25972   30837  4119406   133.6 |  9.871 % |
c |     31587 |   64921   211837 |   28565   13319  1123500    84.4 | 10.042 % |
c |     31738 |   64921   211837 |   31421   13470  1124566    83.5 | 10.042 % |
c |     31963 |   64921   211837 |   34563   13695  1147626    83.8 | 10.042 % |
c |     32301 |   64885   211690 |   37999   14029  1170160    83.4 | 10.065 % |
c |     32810 |   64831   211508 |   41764   14536  1181176    81.3 | 10.135 % |
c |     33570 |   64831   211508 |   45940   15296  1264219    82.7 | 10.135 % |
c |     34713 |   64797   211382 |   50508   16436  1332997    81.1 | 10.166 % |
c |     36423 |   64797   211382 |   55559   18146  1648744    90.9 | 10.166 % |
c |     38986 |   64797   211382 |   61115   20709  2269803   109.6 | 10.166 % |
c |     42833 |   64797   211382 |   67226   24556  2465334   100.4 | 10.166 % |
c |     48600 |   64768   211297 |   73916   30318  3397605   112.1 | 10.189 % |
c |     57249 |   64768   211297 |   81307   38967  6684152   171.5 | 10.189 % |
c ==============================================================================
c (current CPU-time: 151.898 s)
c ==============================================================================
c [1mFound solution: 7632388[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23332075   bits: 25/25
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     69109 |   64782   211422 |   19434   50825 10991394   216.3 | 10.189 % |
c   -- subsuming                       
c   -- var.elim.:  163/163          
c   -- var.elim.:  111/111          
c   -- var.elim.:  14/14          
c |     69109 |   64685   211238 |      --   50825       --      -- |     --   | -97/-177
c |     69109 |   64685   211238 |   25874   50825 10991394   216.3 | 10.189 % |
c |     69209 |   64685   211238 |   28461   12347  1917880   155.3 | 10.331 % |
c |     69359 |   64665   211171 |   31297   12496  1919746   153.6 | 10.354 % |
c |     69585 |   64665   211171 |   34427   12722  1928893   151.6 | 10.354 % |
c ==============================================================================
c (current CPU-time: 155.612 s)
c ==============================================================================
c [1mFound solution: 5955720[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 25008743   bits: 25/25
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     69888 |   64686   211336 |   19405   13025  1970982   151.3 | 10.354 % |
c   -- subsuming                       
c   -- var.elim.:  95/95          
c   -- var.elim.:  47/47          
c |     69888 |   64643   211097 |      --   13025       --      -- |     --   | -33/-46
c |     69888 |   64643   211097 |   25857   12295  1624037   132.1 | 10.354 % |
c |     69988 |   64643   211097 |   28442   12395  1626007   131.2 | 10.441 % |
c |     70138 |   64631   211056 |   31281   12543  1630262   130.0 | 10.449 % |
c |     70364 |   64631   211056 |   34409   12769  1632348   127.8 | 10.449 % |
c |     70701 |   64631   211056 |   37850   13106  1643651   125.4 | 10.449 % |
c |     71208 |   64631   211056 |   41635   13613  1682272   123.6 | 10.449 % |
c |     71967 |   64631   211056 |   45799   14372  2003323   139.4 | 10.449 % |
c |     73106 |   64544   210772 |   50311   15506  2046337   132.0 | 10.564 % |
c |     74816 |   64498   210608 |   55302   17209  2115399   122.9 | 10.618 % |
c |     77378 |   64460   210471 |   60797   19768  2487252   125.8 | 10.657 % |
c |     81225 |   64440   210398 |   66856   23612  3045016   129.0 | 10.672 % |
c |     86991 |   64335   210052 |   73422   29376  3997017   136.1 | 10.795 % |
c |     95643 |   64323   210015 |   80749   38014  4481091   117.9 | 10.811 % |
c |    108619 |   64307   209952 |   88802   50989  6250938   122.6 | 10.819 % |
c |    128080 |   64307   209952 |   97682   70450  9740937   138.3 | 10.819 % |
c |    157272 |   64307   209952 |  107450   99642 21190841   212.7 | 10.819 % |
c |    201063 |   64223   209698 |  118041   47928  5405257   112.8 | 10.896 % |
c |    266748 |   64179   209553 |  129756  113608 16178672   142.4 | 10.949 % |
c |    365275 |   64166   209510 |  142703   94054 20769045   220.8 | 10.973 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v C1_0x2e__bit_7 C1_0x2e__bit_6 C1_0x2e__bit_5 C1_0x2e__bit_4 C1_0x2e__bit_3 -C1_0x2e__bit_2 -C1_0x2e__bit_1 -C1_0x2e__bit0 -C1_0x2e__bit1 C1_0x2e__bit2 C1_0x2e__bit3 -C1_0x2e__bit4 -C1_0x2e__bit5 -C1_0x2e__bit6 -C1_0x2e__bit7 -C1_0x2e__bit8 -C1_0x2e__bit9 -C1_0x2e__bit10 -C1_0x2e__bit11 -C1_0x2e__bit12 -C2_0x2e__bit_7 -C2_0x2e__bit_6 -C2_0x2e__bit_5 -C2_0x2e__bit_4 -C2_0x2e__bit_3 -C2_0x2e__bit_2 -C2_0x2e__bit_1 -C2_0x2e__bit0 -C2_0x2e__bit1 -C2_0x2e__bit2 -C2_0x2e__bit3 -C2_0x2e__bit4 -C2_0x2e__bit5 -C2_0x2e__bit6 -C2_0x2e__bit7 -C2_0x2e__bit8 -C2_0x2e__bit9 -C2_0x2e__bit10 -C2_0x2e__bit11 -C2_0x2e__bit12 -C3_0x2e__bit_7 -C3_0x2e__bit_6 -C3_0x2e__bit_5 -C3_0x2e__bit_4 -C3_0x2e__bit_3 -C3_0x2e__bit_2 -C3_0x2e__bit_1 C3_0x2e__bit0 -C3_0x2e__bit1 -C3_0x2e__bit2 C3_0x2e__bit3 C3_0x2e__bit4 -C3_0x2e__bit5 -C3_0x2e__bit6 -C3_0x2e__bit7 -C3_0x2e__bit8 -C3_0x2e__bit9 -C3_0x2e__bit10 -C3_0x2e__bit11 -C3_0x2e__bit12 -C4_0x2e__bit_7 -C4_0x2e__bit_6 -C4_0x2e__bit_5 -C4_0x2e__bit_4 -C4_0x2e__bit_3 -C4_0x2e__bit_2 -C4_0x2e__bit_1 -C4_0x2e__bit0 -C4_0x2e__bit1 -C4_0x2e__bit2 -C4_0x2e__bit3 -C4_0x2e__bit4 -C4_0x2e__bit5 -C4_0x2e__bit6 -C4_0x2e__bit7 -C4_0x2e__bit8 -C4_0x2e__bit9 -C4_0x2e__bit10 -C4_0x2e__bit11 -C4_0x2e__bit12 -C5_0x2e__bit_7 -C5_0x2e__bit_6 -C5_0x2e__bit_5 -C5_0x2e__bit_4 -C5_0x2e__bit_3 -C5_0x2e__bit_2 -C5_0x2e__bit_1 -C5_0x2e__bit0 -C5_0x2e__bit1 -C5_0x2e__bit2 -C5_0x2e__bit3 -C5_0x2e__bit4 -C5_0x2e__bit5 -C5_0x2e__bit6 -C5_0x2e__bit7 -C5_0x2e__bit8 -C5_0x2e__bit9 -C5_0x2e__bit10 -C5_0x2e__bit11 -C5_0x2e__bit12 -C6_0x2e__bit_7 -C6_0x2e__bit_6 -C6_0x2e__bit_5 -C6_0x2e__bit_4 -C6_0x2e__bit_3 -C6_0x2e__bit_2 -C6_0x2e__bit_1 -C6_0x2e__bit0 -C6_0x2e__bit1 -C6_0x2e__bit2 -C6_0x2e__bit3 -C6_0x2e__bit4 -C6_0x2e__bit5 -C6_0x2e__bit6 -C6_0x2e__bit7 -C6_0x2e__bit8 -C6_0x2e__bit9 -C6_0x2e__bit10 -C6_0x2e__bit11 -C6_0x2e__bit12 C7_0x2e__bit_7 -C7_0x2e__bit_6 -C7_0x2e__bit_5 -C7_0x2e__bit_4 -C7_0x2e__bit_3 C7_0x2e__bit_2 C7_0x2e__bit_1 C7_0x2e__bit0 C7_0x2e__bit1 C7_0x2e__bit2 -C7_0x2e__bit3 -C7_0x2e__bit4 -C7_0x2e__bit5 -C7_0x2e__bit6 -C7_0x2e__bit7 -C7_0x2e__bit8 -C7_0x2e__bit9 -C7_0x2e__bit10 -C7_0x2e__bit11 -C7_0x2e__bit12 -C8_0x2e__bit_7 -C8_0x2e__bit_6 -C8_0x2e__bit_5 -C8_0x2e__bit_4 -C8_0x2e__bit_3 -C8_0x2e__bit_2 -C8_0x2e__bit_1 -C8_0x2e__bit0 -C8_0x2e__bit1 -C8_0x2e__bit2 -C8_0x2e__bit3 -C8_0x2e__bit4 -C8_0x2e__bit5 -C8_0x2e__bit6 -C8_0x2e__bit7 -C8_0x2e__bit8 -C8_0x2e__bit9 -C8_0x2e__bit10 -C8_0x2e__bit11 -C8_0x2e__bit12 C9_0x2e__bit_7 C9_0x2e__bit_6 -C9_0x2e__bit_5 C9_0x2e__bit_4 -C9_0x2e__bit_3 -C9_0x2e__bit_2 C9_0x2e__bit_1 -C9_0x2e__bit0 C9_0x2e__bit1 -C9_0x2e__bit2 C9_0x2e__bit3 -C9_0x2e__bit4 -C9_0x2e__bit5 -C9_0x2e__bit6 -C9_0x2e__bit7 -C9_0x2e__bit8 -C9_0x2e__bit9 -C9_0x2e__bit10 -C9_0x2e__bit11 -C9_0x2e__bit12 -C10_0x2e__bit_7 -C10_0x2e__bit_6 -C10_0x2e__bit_5 -C10_0x2e__bit_4 -C10_0x2e__bit_3 -C10_0x2e__bit_2 -C10_0x2e__bit_1 -C10_0x2e__bit0 -C10_0x2e__bit1 -C10_0x2e__bit2 -C10_0x2e__bit3 -C10_0x2e__bit4 -C10_0x2e__bit5 -C10_0x2e__bit6 -C10_0x2e__bit7 -C10_0x2e__bit8 -C10_0x2e__bit9 -C10_0x2e__bit10 -C10_0x2e__bit11 -C10_0x2e__bit12 -C11_0x2e__bit_7 -C11_0x2e__bit_6 -C11_0x2e__bit_5 -C11_0x2e__bit_4 -C11_0x2e__bit_3 -C11_0x2e__bit_2 -C11_0x2e__bit_1 -C11_0x2e__bit0 -C11_0x2e__bit1 -C11_0x2e__bit2 -C11_0x2e__bit3 -C11_0x2e__bit4 -C11_0x2e__bit5 -C11_0x2e__bit6 -C11_0x2e__bit7 -C11_0x2e__bit8 -C11_0x2e__bit9 -C11_0x2e__bit10 -C11_0x2e__bit11 -C11_0x2e__bit12 -C12_0x2e__bit_7 -C12_0x2e__bit_6 C12_0x2e__bit_5 C12_0x2e__bit_4 -C12_0x2e__bit_3 C12_0x2e__bit_2 -C12_0x2e__bit_1 C12_0x2e__bit0 C12_0x2e__bit1 -C12_0x2e__bit2 -C12_0x2e__bit3 C12_0x2e__bit4 -C12_0x2e__bit5 -C12_0x2e__bit6 -C12_0x2e__bit7 -C12_0x2e__bit8 -C12_0x2e__bit9 -C12_0x2e__bit10 -C12_0x2e__bit11 -C12_0x2e__bit12 -C13_0x2e__bit_7 C13_0x2e__bit_6 -C13_0x2e__bit_5 C13_0x2e__bit_4 -C13_0x2e__bit_3 -C13_0x2e__bit_2 C13_0x2e__bit_1 C13_0x2e__bit0 -C13_0x2e__bit1 -C13_0x2e__bit2 C13_0x2e__bit3 -C13_0x2e__bit4 -C13_0x2e__bit5 -C13_0x2e__bit6 -C13_0x2e__bit7 -C13_0x2e__bit8 -C13_0x2e__bit9 -C13_0x2e__bit10 -C13_0x2e__bit11 -C13_0x2e__bit12 -C14_0x2e__bit_7 -C14_0x2e__bit_6 -C14_0x2e__bit_5 -C14_0x2e__bit_4 -C14_0x2e__bit_3 -C14_0x2e__bit_2 -C14_0x2e__bit_1 -C14_0x2e__bit0 -C14_0x2e__bit1 -C14_0x2e__bit2 -C14_0x2e__bit3 -C14_0x2e__bit4 -C14_0x2e__bit5 -C14_0x2e__bit6 -C14_0x2e__bit7 -C14_0x2e__bit8 -C14_0x2e__bit9 -C14_0x2e__bit10 -C14_0x2e__bit11 -C14_0x2e__bit12 -C15_0x2e__bit_7 -C15_0x2e__bit_6 -C15_0x2e__bit_5 -C15_0x2e__bit_4 -C15_0x2e__bit_3 -C15_0x2e__bit_2 -C15_0x2e__bit_1 -C15_0x2e__bit0 -C15_0x2e__bit1 -C15_0x2e__bit2 -C15_0x2e__bit3 -C15_0x2e__bit4 -C15_0x2e__bit5 -C15_0x2e__bit6 -C15_0x2e__bit7 -C15_0x2e__bit8 -C15_0x2e__bit9 -C15_0x2e__bit10 -C15_0x2e__bit11 -C15_0x2e__bit12 C16_0x2e__bit_7 C16_0x2e__bit_6 C16_0x2e__bit_5 C16_0x2e__bit_4 C16_0x2e__bit_3 C16_0x2e__bit_2 -C16_0x2e__bit_1 -C16_0x2e__bit0 -C16_0x2e__bit1 -C16_0x2e__bit2 -C16_0x2e__bit3 -C16_0x2e__bit4 -C16_0x2e__bit5 -C16_0x2e__bit6 -C16_0x2e__bit7 -C16_0x2e__bit8 -C16_0x2e__bit9 -C16_0x2e__bit10 -C16_0x2e__bit11 -C16_0x2e__bit12 C17_0x2e__bit_7 C17_0x2e__bit_6 C17_0x2e__bit_5 C17_0x2e__bit_4 -C17_0x2e__bit_3 -C17_0x2e__bit_2 -C17_0x2e__bit_1 -C17_0x2e__bit0 C17_0x2e__bit1 -C17_0x2e__bit2 C17_0x2e__bit3 -C17_0x2e__bit4 -C17_0x2e__bit5 -C17_0x2e__bit6 -C17_0x2e__bit7 -C17_0x2e__bit8 -C17_0x2e__bit9 -C17_0x2e__bit10 -C17_0x2e__bit11 -C17_0x2e__bit12 C18_0x2e__bit_7 -C18_0x2e__bit_6 -C18_0x2e__bit_5 -C18_0x2e__bit_4 C18_0x2e__bit_3 C18_0x2e__bit_2 C18_0x2e__bit_1 C18_0x2e__bit0 C18_0x2e__bit1 -C18_0x2e__bit2 -C18_0x2e__bit3 C18_0x2e__bit4 -C18_0x2e__bit5 -C18_0x2e__bit6 -C18_0x2e__bit7 -C18_0x2e__bit8 -C18_0x2e__bit9 -C18_0x2e__bit10 -C18_0x2e__bit11 -C18_0x2e__bit12 -C19_0x2e__bit_7 -C19_0x2e__bit_6 -C19_0x2e__bit_5 -C19_0x2e__bit_4 -C19_0x2e__bit_3 -C19_0x2e__bit_2 -C19_0x2e__bit_1 -C19_0x2e__bit0 -C19_0x2e__bit1 -C19_0x2e__bit2 -C19_0x2e__bit3 -C19_0x2e__bit4 -C19_0x2e__bit5 -C19_0x2e__bit6 -C19_0x2e__bit7 -C19_0x2e__bit8 -C19_0x2e__bit9 -C19_0x2e__bit10 -C19_0x2e__bit11 -C19_0x2e__bit12 -C20_0x2e__bit_7 -C20_0x2e__bit_6 -C20_0x2e__bit_5 -C20_0x2e__bit_4 -C20_0x2e__bit_3 -C20_0x2e__bit_2 -C20_0x2e__bit_1 -C20_0x2e__bit0 -C20_0x2e__bit1 -C20_0x2e__bit2 -C20_0x2e__bit3 -C20_0x2e__bit4 -C20_0x2e__bit5 -C20_0x2e__bit6 -C20_0x2e__bit7 -C20_0x2e__bit8 -C20_0x2e__bit9 -C20_0x2e__bit10 -C20_0x2e__bit11 -C20_0x2e__bit12 -C21_0x2e__bit_7 -C21_0x2e__bit_6 -C21_0x2e__bit_5 -C21_0x2e__bit_4 -C21_0x2e__bit_3 -C21_0x2e__bit_2 -C21_0x2e__bit_1 -C21_0x2e__bit0 -C21_0x2e__bit1 -C21_0x2e__bit2 -C21_0x2e__bit3 -C21_0x2e__bit4 -C21_0x2e__bit5 -C21_0x2e__bit6 -C21_0x2e__bit7 -C21_0x2e__bit8 -C21_0x2e__bit9 -C21_0x2e__bit10 -C21_0x2e__bit11 -C21_0x2e__bit12 -C22_0x2e__bit_7 -C22_0x2e__bit_6 -C22_0x2e__bit_5 -C22_0x2e__bit_4 -C22_0x2e__bit_3 -C22_0x2e__bit_2 -C22_0x2e__bit_1 -C22_0x2e__bit0 -C22_0x2e__bit1 -C22_0x2e__bit2 -C22_0x2e__bit3 -C22_0x2e__bit4 -C22_0x2e__bit5 -C22_0x2e__bit6 -C22_0x2e__bit7 -C22_0x2e__bit8 -C22_0x2e__bit9 -C22_0x2e__bit10 -C22_0x2e__bit11 -C22_0x2e__bit12 -C23_0x2e__bit_7 -C23_0x2e__bit_6 -C23_0x2e__bit_5 -C23_0x2e__bit_4 -C23_0x2e__bit_3 -C23_0x2e__bit_2 -C23_0x2e__bit_1 -C23_0x2e__bit0 -C23_0x2e__bit1 -C23_0x2e__bit2 -C23_0x2e__bit3 -C23_0x2e__bit4 -C23_0x2e__bit5 -C23_0x2e__bit6 -C23_0x2e__bit7 -C23_0x2e__bit8 -C23_0x2e__bit9 -C23_0x2e__bit10 -C23_0x2e__bit11 -C23_0x2e__bit12 -C24_0x2e__bit_7 -C24_0x2e__bit_6 -C24_0x2e__bit_5 -C24_0x2e__bit_4 -C24_0x2e__bit_3 -C24_0x2e__bit_2 -C24_0x2e__bit_1 -C24_0x2e__bit0 -C24_0x2e__bit1 -C24_0x2e__bit2 -C24_0x2e__bit3 -C24_0x2e__bit4 -C24_0x2e__bit5 -C24_0x2e__bit6 -C24_0x2e__bit7 -C24_0x2e__bit8 -C24_0x2e__bit9 -C24_0x2e__bit10 -C24_0x2e__bit11 -C24_0x2e__bit12 -C25_0x2e__bit_7 -C25_0x2e__bit_6 -C25_0x2e__bit_5 -C25_0x2e__bit_4 -C25_0x2e__bit_3 -C25_0x2e__bit_2 -C25_0x2e__bit_1 -C25_0x2e__bit0 -C25_0x2e__bit1 -C25_0x2e__bit2 -C25_0x2e__bit3 -C25_0x2e__bit4 -C25_0x2e__bit5 -C25_0x2e__bit6 -C25_0x2e__bit7 -C25_0x2e__bit8 -C25_0x2e__bit9 -C25_0x2e__bit10 -C25_0x2e__bit11 -C25_0x2e__bit12 C26_0x2e__bit_7 C26_0x2e__bit_6 C26_0x2e__bit_5 C26_0x2e__bit_4 -C26_0x2e__bit_3 -C26_0x2e__bit_2 -C26_0x2e__bit_1 -C26_0x2e__bit0 C26_0x2e__bit1 -C26_0x2e__bit2 C26_0x2e__bit3 -C26_0x2e__bit4 -C26_0x2e__bit5 -C26_0x2e__bit6 -C26_0x2e__bit7 -C26_0x2e__bit8 -C26_0x2e__bit9 -C26_0x2e__bit10 -C26_0x2e__bit11 -C26_0x2e__bit12 -C27_0x2e__bit_7 -C27_0x2e__bit_6 -C27_0x2e__bit_5 -C27_0x2e__bit_4 -C27_0x2e__bit_3 -C27_0x2e__bit_2 -C27_0x2e__bit_1 -C27_0x2e__bit0 -C27_0x2e__bit1 -C27_0x2e__bit2 -C27_0x2e__bit3 -C27_0x2e__bit4 -C27_0x2e__bit5 -C27_0x2e__bit6 -C27_0x2e__bit7 -C27_0x2e__bit8 -C27_0x2e__bit9 -C27_0x2e__bit10 -C27_0x2e__bit11 -C27_0x2e__bit12 -C28_0x2e__bit_7 -C28_0x2e__bit_6 C28_0x2e__bit_5 -C28_0x2e__bit_4 C28_0x2e__bit_3 -C28_0x2e__bit_2 C28_0x2e__bit_1 -C28_0x2e__bit0 -C28_0x2e__bit1 -C28_0x2e__bit2 -C28_0x2e__bit3 -C28_0x2e__bit4 -C28_0x2e__bit5 -C28_0x2e__bit6 -C28_0x2e__bit7 -C28_0x2e__bit8 -C28_0x2e__bit9 -C28_0x2e__bit10 -C28_0x2e__bit11 -C28_0x2e__bit12 -C29_0x2e__bit_7 -C29_0x2e__bit_6 -C29_0x2e__bit_5 -C29_0x2e__bit_4 -C29_0x2e__bit_3 -C29_0x2e__bit_2 -C29_0x2e__bit_1 -C29_0x2e__bit0 -C29_0x2e__bit1 -C29_0x2e__bit2 -C29_0x2e__bit3 -C29_0x2e__bit4 -C29_0x2e__bit5 -C29_0x2e__bit6 -C29_0x2e__bit7 -C29_0x2e__bit8 -C29_0x2e__bit9 -C29_0x2e__bit10 -C29_0x2e__bit11 -C29_0x2e__bit12 C30_0x2e__bit_7 C30_0x2e__bit_6 C30_0x2e__bit_5 C30_0x2e__bit_4 -C30_0x2e__bit_3 C30_0x2e__bit_2 -C30_0x2e__bit_1 C30_0x2e__bit0 -C30_0x2e__bit1 C30_0x2e__bit2 -C30_0x2e__bit3 -C30_0x2e__bit4 -C30_0x2e__bit5 -C30_0x2e__bit6 -C30_0x2e__bit7 -C30_0x2e__bit8 -C30_0x2e__bit9 -C30_0x2e__bit10 -C30_0x2e__bit11 -C30_0x2e__bit12 -C31_0x2e__bit_7 -C31_0x2e__bit_6 -C31_0x2e__bit_5 -C31_0x2e__bit_4 -C31_0x2e__bit_3 -C31_0x2e__bit_2 -C31_0x2e__bit_1 -C31_0x2e__bit0 -C31_0x2e__bit1 -C31_0x2e__bit2 -C31_0x2e__bit3 -C31_0x2e__bit4 -C31_0x2e__bit5 -C31_0x2e__bit6 -C31_0x2e__bit7 -C31_0x2e__bit8 -C31_0x2e__bit9 -C31_0x2e__bit10 -C31_0x2e__bit11 -C31_0x2e__bit12 -C32_0x2e__bit_7 C32_0x2e__bit_6 C32_0x2e__bit_5 C32_0x2e__bit_4 -C32_0x2e__bit_3 C32_0x2e__bit_2 C32_0x2e__bit_1 C32_0x2e__bit0 C32_0x2e__bit1 -C32_0x2e__bit2 -C32_0x2e__bit3 -C32_0x2e__bit4 -C32_0x2e__bit5 -C32_0x2e__bit6 -C32_0x2e__bit7 -C32_0x2e__bit8 -C32_0x2e__bit9 -C32_0x2e__bit10 -C32_0x2e__bit11 -C32_0x2e__bit12 -C33_0x2e__bit_7 -C33_0x2e__bit_6 -C33_0x2e__bit_5 -C33_0x2e__bit_4 -C33_0x2e__bit_3 -C33_0x2e__bit_2 -C33_0x2e__bit_1 -C33_0x2e__bit0 -C33_0x2e__bit1 -C33_0x2e__bit2 -C33_0x2e__bit3 -C33_0x2e__bit4 -C33_0x2e__bit5 -C33_0x2e__bit6 -C33_0x2e__bit7 -C33_0x2e__bit8 -C33_0x2e__bit9 -C33_0x2e__bit10 -C33_0x2e__bit11 -C33_0x2e__bit12 -C34_0x2e__bit_7 -C34_0x2e__bit_6 -C34_0x2e__bit_5 -C34_0x2e__bit_4 -C34_0x2e__bit_3 -C34_0x2e__bit_2 -C34_0x2e__bit_1 -C34_0x2e__bit0 -C34_0x2e__bit1 -C34_0x2e__bit2 -C34_0x2e__bit3 -C34_0x2e__bit4 -C34_0x2e__bit5 -C34_0x2e__bit6 -C34_0x2e__bit7 -C34_0x2e__bit8 -C34_0x2e__bit9 -C34_0x2e__bit10 -C34_0x2e__bit11 -C34_0x2e__bit12 -C35_0x2e__bit_7 -C35_0x2e__bit_6 -C35_0x2e__bit_5 -C35_0x2e__bit_4 -C35_0x2e__bit_3 -C35_0x2e__bit_2 -C35_0x2e__bit_1 -C35_0x2e__bit0 -C35_0x2e__bit1 -C35_0x2e__bit2 -C35_0x2e__bit3 -C35_0x2e__bit4 -C35_0x2e__bit5 -C35_0x2e__bit6 -C35_0x2e__bit7 -C35_0x2e__bit8 -C35_0x2e__bit9 -C35_0x2e__bit10 -C35_0x2e__bit11 -C35_0x2e__bit12 -C36_0x2e__bit_7 -C36_0x2e__bit_6 -C36_0x2e__bit_5 -C36_0x2e__bit_4 -C36_0x2e__bit_3 -C36_0x2e__bit_2 -C36_0x2e__bit_1 -C36_0x2e__bit0 -C36_0x2e__bit1 -C36_0x2e__bit2 -C36_0x2e__bit3 -C36_0x2e__bit4 -C36_0x2e__bit5 -C36_0x2e__bit6 -C36_0x2e__bit7 -C36_0x2e__bit8 -C36_0x2e__bit9 -C36_0x2e__bit10 -C36_0x2e__bit11 -C36_0x2e__bit12 -C37_0x2e__bit_7 C37_0x2e__bit_6 C37_0x2e__bit_5 -C37_0x2e__bit_4 C37_0x2e__bit_3 C37_0x2e__bit_2 -C37_0x2e__bit_1 C37_0x2e__bit0 -C37_0x2e__bit1 C37_0x2e__bit2 -C37_0x2e__bit3 -C37_0x2e__bit4 -C37_0x2e__bit5 -C37_0x2e__bit6 -C37_0x2e__bit7 -C37_0x2e__bit8 -C37_0x2e__bit9 -C37_0x2e__bit10 -C37_0x2e__bit11 -C37_0x2e__bit12 -C38_0x2e__bit_7 C38_0x2e__bit_6 -C38_0x2e__bit_5 C38_0x2e__bit_4 -C38_0x2e__bit_3 -C38_0x2e__bit_2 C38_0x2e__bit_1 -C38_0x2e__bit0 -C38_0x2e__bit1 C38_0x2e__bit2 -C38_0x2e__bit3 -C38_0x2e__bit4 -C38_0x2e__bit5 -C38_0x2e__bit6 -C38_0x2e__bit7 -C38_0x2e__bit8 -C38_0x2e__bit9 -C38_0x2e__bit10 -C38_0x2e__bit11 -C38_0x2e__bit12 -C39_0x2e__bit_7 -C39_0x2e__bit_6 -C39_0x2e__bit_5 -C39_0x2e__bit_4 -C39_0x2e__bit_3 -C39_0x2e__bit_2 -C39_0x2e__bit_1 -C39_0x2e__bit0 -C39_0x2e__bit1 -C39_0x2e__bit2 -C39_0x2e__bit3 -C39_0x2e__bit4 -C39_0x2e__bit5 -C39_0x2e__bit6 -C39_0x2e__bit7 -C39_0x2e__bit8 -C39_0x2e__bit9 -C39_0x2e__bit10 -C39_0x2e__bit11 -C39_0x2e__bit12 -C40_0x2e__bit_7 -C40_0x2e__bit_6 -C40_0x2e__bit_5 -C40_0x2e__bit_4 -C40_0x2e__bit_3 -C40_0x2e__bit_2 -C40_0x2e__bit_1 -C40_0x2e__bit0 -C40_0x2e__bit1 -C40_0x2e__bit2 -C40_0x2e__bit3 -C40_0x2e__bit4 -C40_0x2e__bit5 -C40_0x2e__bit6 -C40_0x2e__bit7 -C40_0x2e__bit8 -C40_0x2e__bit9 -C40_0x2e__bit10 -C40_0x2e__bit11 -C40_0x2e__bit12 C41_0x2e__bit_7 C41_0x2e__bit_6 C41_0x2e__bit_5 -C41_0x2e__bit_4 -C41_0x2e__bit_3 -C41_0x2e__bit_2 -C41_0x2e__bit_1 -C41_0x2e__bit0 C41_0x2e__bit1 -C41_0x2e__bit2 -C41_0x2e__bit3 -C41_0x2e__bit4 -C41_0x2e__bit5 -C41_0x2e__bit6 -C41_0x2e__bit7 -C41_0x2e__bit8 -C41_0x2e__bit9 -C41_0x2e__bit10 -C41_0x2e__bit11 -C41_0x2e__bit12 -C42_0x2e__bit_7 -C42_0x2e__bit_6 -C42_0x2e__bit_5 -C42_0x2e__bit_4 -C42_0x2e__bit_3 -C42_0x2e__bit_2 -C42_0x2e__bit_1 -C42_0x2e__bit0 -C42_0x2e__bit1 -C42_0x2e__bit2 -C42_0x2e__bit3 -C42_0x2e__bit4 -C42_0x2e__bit5 -C42_0x2e__bit6 -C42_0x2e__bit7 -C42_0x2e__bit8 -C42_0x2e__bit9 -C42_0x2e__bit10 -C42_0x2e__bit11 -C42_0x2e__bit12 -C43_0x2e__bit_7 -C43_0x2e__bit_6 -C43_0x2e__bit_5 -C43_0x2e__bit_4 -C43_0x2e__bit_3 -C43_0x2e__bit_2 -C43_0x2e__bit_1 -C43_0x2e__bit0 -C43_0x2e__bit1 -C43_0x2e__bit2 -C43_0x2e__bit3 -C43_0x2e__bit4 -C43_0x2e__bit5 -C43_0x2e__bit6 -C43_0x2e__bit7 -C43_0x2e__bit8 -C43_0x2e__bit9 -C43_0x2e__bit10 -C43_0x2e__bit11 -C43_0x2e__bit12 -C44_0x2e__bit_7 -C44_0x2e__bit_6 -C44_0x2e__bit_5 -C44_0x2e__bit_4 -C44_0x2e__bit_3 -C44_0x2e__bit_2 -C44_0x2e__bit_1 -C44_0x2e__bit0 -C44_0x2e__bit1 -C44_0x2e__bit2 -C44_0x2e__bit3 -C44_0x2e__bit4 -C44_0x2e__bit5 -C44_0x2e__bit6 -C44_0x2e__bit7 -C44_0x2e__bit8 -C44_0x2e__bit9 -C44_0x2e__bit10 -C44_0x2e__bit11 -C44_0x2e__bit12 -C45_0x2e__bit_7 -C45_0x2e__bit_6 -C45_0x2e__bit_5 -C45_0x2e__bit_4 -C45_0x2e__bit_3 -C45_0x2e__bit_2 -C45_0x2e__bit_1 -C45_0x2e__#### 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.59 0.86 0.88 2/56 31348
Raw data (stat): 31348 (runsolver) R 31347 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 431905991 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0007 s]
Raw data (loadavg): 0.65 0.87 0.88 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 8158 0 0 0 975 24 0 0 25 0 1 0 431905991 26169344 5354 4294967295 134512640 134672761 3221224544 3221221584 134522987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6389 5354 603 41 0 6348 0
vsize: 25556
[startup+20.0014 s]
Raw data (loadavg): 0.71 0.87 0.88 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 9216 0 0 0 1972 26 0 0 25 0 1 0 431905991 27783168 5834 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6783 5834 603 41 0 6742 0
vsize: 27132
[startup+30.0012 s]
Raw data (loadavg): 0.75 0.88 0.88 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 10323 0 0 0 2969 29 0 0 25 0 1 0 431905991 32301056 6941 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7886 6941 603 41 0 7845 0
vsize: 31544
[startup+40.0025 s]
Raw data (loadavg): 0.79 0.88 0.88 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 11622 0 0 0 3967 31 0 0 25 0 1 0 431905991 37765120 8240 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9220 8240 603 41 0 9179 0
vsize: 36880
[startup+50.0028 s]
Raw data (loadavg): 0.82 0.88 0.88 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 12749 0 0 0 4964 34 0 0 25 0 1 0 431905991 42258432 9367 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10317 9367 603 41 0 10276 0
vsize: 41268
[startup+60.0036 s]
Raw data (loadavg): 0.85 0.89 0.88 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 13622 0 0 0 5962 37 0 0 25 0 1 0 431905991 44879872 9921 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10957 9921 603 41 0 10916 0
vsize: 43828
[startup+70.0044 s]
Raw data (loadavg): 0.87 0.89 0.88 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 13622 0 0 0 6962 37 0 0 25 0 1 0 431905991 44879872 9921 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10957 9921 603 41 0 10916 0
vsize: 43828
[startup+80.0041 s]
Raw data (loadavg): 0.89 0.89 0.88 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 13622 0 0 0 7962 37 0 0 25 0 1 0 431905991 44879872 9921 4294967295 134512640 134672761 3221224544 3221223728 134615554 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10957 9921 603 41 0 10916 0
vsize: 43828
[startup+90.0049 s]
Raw data (loadavg): 0.91 0.90 0.88 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 13622 0 0 0 8962 38 0 0 25 0 1 0 431905991 44879872 9921 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10957 9921 603 41 0 10916 0
vsize: 43828
[startup+100.005 s]
Raw data (loadavg): 0.92 0.90 0.89 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 14360 0 0 0 9960 39 0 0 25 0 1 0 431905991 47611904 10659 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11624 10659 603 41 0 11583 0
vsize: 46496
[startup+110.007 s]
Raw data (loadavg): 0.93 0.90 0.89 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 15688 0 0 0 10958 42 0 0 25 0 1 0 431905991 52957184 11987 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12929 11987 603 41 0 12888 0
vsize: 51716
[startup+120.006 s]
Raw data (loadavg): 0.94 0.90 0.89 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 16495 0 0 0 11956 44 0 0 25 0 1 0 431905991 56254464 12794 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13734 12794 603 41 0 13693 0
vsize: 54936
[startup+130.006 s]
Raw data (loadavg): 0.95 0.91 0.89 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 17957 0 0 0 12953 47 0 0 25 0 1 0 431905991 62275584 14256 4294967295 134512640 134672761 3221224544 3221223728 134616004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15204 14256 603 41 0 15163 0
vsize: 60816
[startup+140.007 s]
Raw data (loadavg): 0.96 0.91 0.89 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 19111 0 0 0 13950 50 0 0 25 0 1 0 431905991 66969600 15410 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16350 15410 603 41 0 16309 0
vsize: 65400
[startup+150.008 s]
Raw data (loadavg): 0.96 0.91 0.89 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 20087 0 0 0 14948 52 0 0 25 0 1 0 431905991 71081984 16386 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17354 16386 603 41 0 17313 0
vsize: 69416
[startup+160.009 s]
Raw data (loadavg): 0.97 0.91 0.89 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 21346 0 0 0 15944 56 0 0 25 0 1 0 431905991 72052736 16655 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17591 16655 603 41 0 17550 0
vsize: 70364
[startup+170.009 s]
Raw data (loadavg): 0.97 0.92 0.89 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 21346 0 0 0 16944 57 0 0 25 0 1 0 431905991 72052736 16655 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17591 16655 603 41 0 17550 0
vsize: 70364
[startup+180.009 s]
Raw data (loadavg): 0.98 0.92 0.89 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 21346 0 0 0 17945 57 0 0 25 0 1 0 431905991 72052736 16655 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17591 16655 603 41 0 17550 0
vsize: 70364
[startup+190.009 s]
Raw data (loadavg): 0.98 0.92 0.89 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 21346 0 0 0 18945 57 0 0 25 0 1 0 431905991 72052736 16655 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17591 16655 603 41 0 17550 0
vsize: 70364
[startup+200.008 s]
Raw data (loadavg): 0.98 0.92 0.90 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 21346 0 0 0 19945 57 0 0 25 0 1 0 431905991 72052736 16655 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17591 16655 603 41 0 17550 0
vsize: 70364
[startup+210.009 s]
Raw data (loadavg): 0.98 0.92 0.90 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 21346 0 0 0 20945 57 0 0 25 0 1 0 431905991 72052736 16655 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17591 16655 603 41 0 17550 0
vsize: 70364
[startup+220.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 21346 0 0 0 21945 57 0 0 25 0 1 0 431905991 72052736 16655 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17591 16655 603 41 0 17550 0
vsize: 70364
[startup+230.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 21346 0 0 0 22945 57 0 0 25 0 1 0 431905991 72052736 16655 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17591 16655 603 41 0 17550 0
vsize: 70364
[startup+240.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 21346 0 0 0 23946 57 0 0 25 0 1 0 431905991 72052736 16655 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17591 16655 603 41 0 17550 0
vsize: 70364
[startup+250.008 s]
Raw data (loadavg): 0.99 0.93 0.90 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 21346 0 0 0 24946 57 0 0 25 0 1 0 431905991 72052736 16655 4294967295 134512640 134672761 3221224544 3221223728 134616014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17591 16655 603 41 0 17550 0
vsize: 70364
[startup+260.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 21346 0 0 0 25946 57 0 0 25 0 1 0 431905991 72052736 16655 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17591 16655 603 41 0 17550 0
vsize: 70364
[startup+270.009 s]
Raw data (loadavg): 0.99 0.94 0.90 2/56 31348
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 21346 0 0 0 26946 57 0 0 25 0 1 0 431905991 72052736 16655 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17591 16655 603 41 0 17550 0
vsize: 70364
[startup+280.009 s]
Raw data (loadavg): 0.99 0.94 0.90 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 21416 0 0 0 27946 57 0 0 25 0 1 0 431905991 72577024 16725 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17719 16725 603 41 0 17678 0
vsize: 70876
[startup+290.01 s]
Raw data (loadavg): 0.99 0.94 0.90 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 21419 0 0 0 28946 57 0 0 25 0 1 0 431905991 72577024 16728 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17719 16728 603 41 0 17678 0
vsize: 70876
[startup+300.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 22204 0 0 0 29945 58 0 0 25 0 1 0 431905991 75853824 17513 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18519 17513 603 41 0 18478 0
vsize: 74076
[startup+310.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 23223 0 0 0 30942 62 0 0 25 0 1 0 431905991 80039936 18532 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19541 18532 603 41 0 19500 0
vsize: 78164
[startup+320.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 24171 0 0 0 31940 64 0 0 25 0 1 0 431905991 83841024 19480 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20469 19480 603 41 0 20428 0
vsize: 81876
[startup+330.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 25298 0 0 0 32937 67 0 0 25 0 1 0 431905991 88526848 20607 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21613 20607 603 41 0 21572 0
vsize: 86452
[startup+340.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 26234 0 0 0 33935 69 0 0 25 0 1 0 431905991 92319744 21543 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22539 21543 603 41 0 22498 0
vsize: 90156
[startup+350.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 27207 0 0 0 34933 71 0 0 25 0 1 0 431905991 96264192 22516 4294967295 134512640 134672761 3221224544 3221223680 134614753 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23502 22516 603 41 0 23461 0
vsize: 94008
[startup+360.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 28202 0 0 0 35930 74 0 0 25 0 1 0 431905991 100335616 23511 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24496 23511 603 41 0 24455 0
vsize: 97984
[startup+370.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 29178 0 0 0 36928 77 0 0 25 0 1 0 431905991 104390656 24487 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25486 24487 603 41 0 25445 0
vsize: 101944
[startup+380.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 30183 0 0 0 37925 79 0 0 25 0 1 0 431905991 108437504 25492 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26474 25492 603 41 0 26433 0
vsize: 105896
[startup+390.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 31321 0 0 0 38922 83 0 0 25 0 1 0 431905991 113164288 26630 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27628 26630 603 41 0 27587 0
vsize: 110512
[startup+400.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 32129 0 0 0 39920 85 0 0 25 0 1 0 431905991 116436992 27438 4294967295 134512640 134672761 3221224544 3221223704 134541793 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28427 27438 603 41 0 28386 0
vsize: 113708
[startup+410.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 32836 0 0 0 40919 86 0 0 25 0 1 0 431905991 119296000 28145 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29125 28145 603 41 0 29084 0
vsize: 116500
[startup+420.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 33509 0 0 0 41918 88 0 0 25 0 1 0 431905991 122028032 28818 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29792 28818 603 41 0 29751 0
vsize: 119168
[startup+430.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 33828 0 0 0 42917 89 0 0 25 0 1 0 431905991 123355136 29137 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30116 29137 603 41 0 30075 0
vsize: 120464
[startup+440.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34277 0 0 0 43916 90 0 0 25 0 1 0 431905991 125177856 29586 4294967295 134512640 134672761 3221224544 3221222336 134645591 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29586 603 41 0 30520 0
vsize: 122244
[startup+450.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 44916 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+460.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 45916 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+470.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 46916 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+480.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 47917 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+490.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 48917 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+500.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 49917 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+510.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 50917 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+520.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 51917 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+530.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 52918 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 53918 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 54918 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 55918 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31350
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 56918 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+580.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 57918 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 58919 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 59919 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 60919 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+620.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 61919 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+630.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 62919 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+640.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 63919 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+650.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 64920 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+660.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 65920 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+670.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 66920 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+680.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 67920 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+690.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 68920 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+700.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 69920 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+710.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 70921 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+720.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 71921 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34371 0 0 0 72921 90 0 0 25 0 1 0 431905991 125177856 29570 4294967295 134512640 134672761 3221224544 3221223728 134615635 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29570 603 41 0 30520 0
vsize: 122244
[startup+740.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34372 0 0 0 73921 90 0 0 25 0 1 0 431905991 125177856 29571 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29571 603 41 0 30520 0
vsize: 122244
[startup+750.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34373 0 0 0 74921 90 0 0 25 0 1 0 431905991 125177856 29572 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29572 603 41 0 30520 0
vsize: 122244
[startup+760.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34376 0 0 0 75921 90 0 0 25 0 1 0 431905991 125177856 29575 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29575 603 41 0 30520 0
vsize: 122244
[startup+770.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34379 0 0 0 76922 90 0 0 25 0 1 0 431905991 125177856 29578 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29578 603 41 0 30520 0
vsize: 122244
[startup+780.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34381 0 0 0 77922 90 0 0 25 0 1 0 431905991 125177856 29580 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29580 603 41 0 30520 0
vsize: 122244
[startup+790.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34383 0 0 0 78922 90 0 0 25 0 1 0 431905991 125177856 29582 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29582 603 41 0 30520 0
vsize: 122244
[startup+800.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34386 0 0 0 79922 90 0 0 25 0 1 0 431905991 125177856 29585 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29585 603 41 0 30520 0
vsize: 122244
[startup+810.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34388 0 0 0 80922 90 0 0 25 0 1 0 431905991 125177856 29587 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30561 29587 603 41 0 30520 0
vsize: 122244
[startup+820.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34390 0 0 0 81922 90 0 0 25 0 1 0 431905991 125702144 29589 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29589 603 41 0 30648 0
vsize: 122756
[startup+830.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34392 0 0 0 82922 90 0 0 25 0 1 0 431905991 125702144 29591 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29591 603 41 0 30648 0
vsize: 122756
[startup+840.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34527 0 0 0 83922 90 0 0 25 0 1 0 431905991 126750720 29726 4294967295 134512640 134672761 3221224544 3221223600 134644281 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30945 29726 603 41 0 30904 0
vsize: 123780
[startup+850.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34549 0 0 0 84922 90 0 0 25 0 1 0 431905991 125702144 29615 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29615 603 41 0 30648 0
vsize: 122756
[startup+860.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34549 0 0 0 85923 90 0 0 25 0 1 0 431905991 125702144 29615 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29615 603 41 0 30648 0
vsize: 122756
[startup+870.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31352
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34549 0 0 0 86923 90 0 0 25 0 1 0 431905991 125702144 29615 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29615 603 41 0 30648 0
vsize: 122756
[startup+880.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31354
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34549 0 0 0 87923 90 0 0 25 0 1 0 431905991 125702144 29615 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29615 603 41 0 30648 0
vsize: 122756
[startup+890.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31407
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34549 0 0 0 88923 90 0 0 25 0 1 0 431905991 125702144 29615 4294967295 134512640 134672761 3221224544 3221223728 134615683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29615 603 41 0 30648 0
vsize: 122756
[startup+900.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31407
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34549 0 0 0 89923 90 0 0 25 0 1 0 431905991 125702144 29615 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29615 603 41 0 30648 0
vsize: 122756
[startup+910.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31407
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34549 0 0 0 90923 90 0 0 25 0 1 0 431905991 125702144 29615 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29615 603 41 0 30648 0
vsize: 122756
[startup+920.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31407
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34549 0 0 0 91924 90 0 0 25 0 1 0 431905991 125702144 29615 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29615 603 41 0 30648 0
vsize: 122756
[startup+930.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31407
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34549 0 0 0 92924 90 0 0 25 0 1 0 431905991 125702144 29615 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29615 603 41 0 30648 0
vsize: 122756
[startup+940.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31407
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34549 0 0 0 93924 90 0 0 25 0 1 0 431905991 125702144 29615 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29615 603 41 0 30648 0
vsize: 122756
[startup+950.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31409
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34549 0 0 0 94924 90 0 0 25 0 1 0 431905991 125702144 29615 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29615 603 41 0 30648 0
vsize: 122756
[startup+960.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34549 0 0 0 95924 90 0 0 25 0 1 0 431905991 125702144 29615 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29615 603 41 0 30648 0
vsize: 122756
[startup+970.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34549 0 0 0 96924 90 0 0 25 0 1 0 431905991 125702144 29615 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29615 603 41 0 30648 0
vsize: 122756
[startup+980.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34549 0 0 0 97925 90 0 0 25 0 1 0 431905991 125702144 29615 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29615 603 41 0 30648 0
vsize: 122756
[startup+990.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34550 0 0 0 98925 90 0 0 25 0 1 0 431905991 125702144 29616 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29616 603 41 0 30648 0
vsize: 122756
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34550 0 0 0 99925 90 0 0 25 0 1 0 431905991 125702144 29616 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29616 603 41 0 30648 0
vsize: 122756
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34550 0 0 0 100925 90 0 0 25 0 1 0 431905991 125702144 29616 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29616 603 41 0 30648 0
vsize: 122756
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34550 0 0 0 101925 90 0 0 25 0 1 0 431905991 125702144 29616 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29616 603 41 0 30648 0
vsize: 122756
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34550 0 0 0 102925 90 0 0 25 0 1 0 431905991 125702144 29616 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29616 603 41 0 30648 0
vsize: 122756
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34550 0 0 0 103926 90 0 0 25 0 1 0 431905991 125702144 29616 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29616 603 41 0 30648 0
vsize: 122756
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34550 0 0 0 104926 90 0 0 25 0 1 0 431905991 125702144 29616 4294967295 134512640 134672761 3221224544 3221223728 134615551 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29616 603 41 0 30648 0
vsize: 122756
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34550 0 0 0 105926 90 0 0 25 0 1 0 431905991 125702144 29616 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29616 603 41 0 30648 0
vsize: 122756
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34550 0 0 0 106926 90 0 0 25 0 1 0 431905991 125702144 29616 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29616 603 41 0 30648 0
vsize: 122756
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34550 0 0 0 107926 90 0 0 25 0 1 0 431905991 125702144 29616 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29616 603 41 0 30648 0
vsize: 122756
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34550 0 0 0 108926 90 0 0 25 0 1 0 431905991 125702144 29616 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29616 603 41 0 30648 0
vsize: 122756
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34550 0 0 0 109926 90 0 0 25 0 1 0 431905991 125702144 29616 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29616 603 41 0 30648 0
vsize: 122756
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34550 0 0 0 110927 90 0 0 25 0 1 0 431905991 125702144 29616 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29616 603 41 0 30648 0
vsize: 122756
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34550 0 0 0 111927 90 0 0 25 0 1 0 431905991 125702144 29616 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29616 603 41 0 30648 0
vsize: 122756
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 34776 0 0 0 112926 92 0 0 25 0 1 0 431905991 126636032 29842 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30917 29842 603 41 0 30876 0
vsize: 123668
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 35701 0 0 0 113923 95 0 0 25 0 1 0 431905991 130437120 30767 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31845 30767 603 41 0 31804 0
vsize: 127380
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 36545 0 0 0 114920 97 0 0 25 0 1 0 431905991 133877760 31611 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32685 31611 603 41 0 32644 0
vsize: 130740
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 37377 0 0 0 115918 100 0 0 25 0 1 0 431905991 137310208 32443 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33523 32443 603 41 0 33482 0
vsize: 134092
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31411
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 38108 0 0 0 116917 101 0 0 25 0 1 0 431905991 140357632 33174 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34267 33174 603 41 0 34226 0
vsize: 137068
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31413
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 38756 0 0 0 117915 103 0 0 25 0 1 0 431905991 142974976 33822 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34906 33822 603 41 0 34865 0
vsize: 139624
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31413
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 39388 0 0 0 118914 104 0 0 25 0 1 0 431905991 145616896 34454 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35551 34454 603 41 0 35510 0
vsize: 142204
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 31413
Raw data (stat): 31348 (minisat+) R 31347 12452 12451 0 -1 0 39617 0 0 0 119914 105 0 0 25 0 1 0 431905991 146542592 34683 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35777 34683 603 41 0 35736 0
vsize: 143108
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 31413
Raw data (stat): 31348 (minisat+) Z 31347 12452 12451 0 -1 12 39618 0 0 0 119914 111 0 0 25 0 1 0 431905991 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.26
CPU user time (s): 1199.15
CPU system time (s): 1.11883
CPU usage (%): 100.015
Max. virtual memory (Kb): 143108
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####