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-misc05.opb
MD5SUM	4f7891bf040f9fa135208e1a9808a8bc
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1430464
Optimality of the best value was proved	NO
Number of terms in the objective function	21
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	2097151
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	5242880
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	81788220
Number of bits of the biggest sum of numbers	27
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	6.00309
Number of variables	1320
Total number of constraints	374
Number of constraints which are clauses	155
Number of constraints which are cardinality constraints (but not clauses)	82
Number of constraints which are nor clauses,nor cardinality constraints	137
Minimum length of a constraint	1
Maximum length of a constraint	301
Trace number 19140

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-21 18:02:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16990 boxname=wulflinc7 idbench=1307 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4f7891bf040f9fa135208e1a9808a8bc  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-misc05.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-misc05.opb /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-misc05.opb
IDLAUNCH: 16990
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        746048 kB
Buffers:         15848 kB
Cached:         250816 kB
SwapCached:        304 kB
Active:          32352 kB
Inactive:       236804 kB
HighTotal:      131008 kB
HighFree:        52164 kB
LowTotal:       903652 kB
LowFree:        693884 kB
SwapTotal:     2097136 kB
SwapFree:      2096520 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6448 kB
Slab:            13800 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:22:53 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 16990 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 327 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppp
c   -- Detecting intervals from adjacent constraints: ############################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................ssssssssssssssssssssssss
c ---[ 349]---> BDD-cost:  219
c ---[ 345]---> BDD-cost:20222
c ---[ 343]---> BDD-cost:143665
c ---[ 341]---> BDD-cost:   13
c ---[ 339]---> BDD-cost:   13
c ---[ 337]---> BDD-cost:   13
c ---[ 335]---> BDD-cost:   11
c ---[ 333]---> BDD-cost:   13
c ---[ 331]---> BDD-cost:   13
c ---[ 329]---> BDD-cost:   13
c ---[ 200]---> BDD-cost:   56
c ---[ 198]---> BDD-cost:   78
c ---[ 196]---> BDD-cost:   78
c ---[ 194]---> BDD-cost:   69
c ---[ 192]---> BDD-cost:   78
c ---[ 190]---> BDD-cost:   78
c ---[ 188]---> BDD-cost:   78
c ---[ 186]---> BDD-cost:   78
c ---[ 184]---> BDD-cost:   78
c ---[ 182]---> BDD-cost: 3319
c ---[ 180]---> BDD-cost: 3970
c ---[ 178]---> BDD-cost: 3972
c ---[ 176]---> BDD-cost: 3292
c ---[ 174]---> BDD-cost: 3984
c ---[ 172]---> BDD-cost: 3998
c ---[ 170]---> BDD-cost: 3986
c ---[ 168]---> BDD-cost:   72
c ---[ 166]---> BDD-cost:   72
c ---[ 165]---> BDD-cost:  965
c ---[ 164]---> BDD-cost:  930
c ---[ 135]---> BDD-cost:   98
c ---[ 134]---> BDD-cost:   20
c ---[ 133]---> BDD-cost:   20
c ---[ 132]---> BDD-cost:   20
c ---[ 131]---> BDD-cost:   20
c ---[ 130]---> BDD-cost:   20
c ---[ 129]---> BDD-cost:   20
c ---[ 128]---> BDD-cost:   23
c ---[ 127]---> BDD-cost:   23
c ---[ 126]---> BDD-cost:   23
c ---[ 125]---> BDD-cost:   23
c ---[ 124]---> BDD-cost:   23
c ---[ 123]---> BDD-cost:   23
c ---[ 122]---> BDD-cost:   23
c ---[ 121]---> BDD-cost:   23
c ---[ 120]---> BDD-cost:   23
c ---[ 119]---> BDD-cost:   23
c ---[ 118]---> BDD-cost:   23
c ---[ 117]---> BDD-cost:   23
c ---[ 115]---> BDD-cost:   22
c ---[ 114]---> BDD-cost:   22
c ---[ 113]---> BDD-cost:   22
c ---[ 112]---> BDD-cost:   22
c ---[ 111]---> BDD-cost:   22
c ---[ 110]---> BDD-cost:   22
c ---[ 109]---> BDD-cost:   22
c ---[ 108]---> BDD-cost:   22
c ---[ 107]---> BDD-cost:   22
c ---[ 106]---> BDD-cost:   22
c ---[ 105]---> BDD-cost:   22
c ---[ 104]---> BDD-cost:   24
c ---[ 103]---> BDD-cost:   24
c ---[ 102]---> BDD-cost:   24
c ---[ 101]---> BDD-cost:   24
c ---[ 100]---> BDD-cost:   24
c ---[  99]---> BDD-cost:   24
c ---[  98]---> BDD-cost:   19
c ---[  97]---> BDD-cost:   19
c ---[  96]---> BDD-cost:   19
c ---[  95]---> BDD-cost:   19
c ---[  94]---> BDD-cost:   19
c ---[  93]---> BDD-cost:   19
c ---[  92]---> BDD-cost:   23
c ---[  91]---> BDD-cost:   23
c ---[  90]---> BDD-cost:   23
c ---[  89]---> BDD-cost:   23
c ---[  88]---> BDD-cost:   23
c ---[  87]---> BDD-cost:   23
c ---[  86]---> BDD-cost:   23
c ---[  85]---> BDD-cost:   23
c ---[  84]---> BDD-cost:   23
c ---[  83]---> BDD-cost:   23
c ---[  82]---> BDD-cost:   23
c ---[  81]---> BDD-cost:   23
c ---[  80]---> BDD-cost:   23
c ---[  79]---> BDD-cost:   23
c ---[  77]---> BDD-cost:    5
c ---[  76]---> BDD-cost:    7
c ---[  73]---> BDD-cost:    6
c ---[  72]---> BDD-cost:    7
c ---[  71]---> BDD-cost:    6
c ---[  70]---> BDD-cost:    8
c ---[  67]---> BDD-cost:    7
c ---[  66]---> BDD-cost:    7
c ---[  64]---> BDD-cost:    8
c ---[  61]---> BDD-cost:    7
c ---[  59]---> BDD-cost:    5
c ---[  56]---> BDD-cost:    6
c ---[  55]---> BDD-cost:    7
c ---[  53]---> BDD-cost:    6
c ---[  52]---> BDD-cost:    8
c ---[  50]---> BDD-cost:    7
c ---[  49]---> BDD-cost:    7
c ---[  47]---> BDD-cost:    6
c ---[  46]---> BDD-cost:    8
c ---[  44]---> BDD-cost:    7
c ---[  43]---> BDD-cost:    7
c ---[  41]---> BDD-cost:    6
c ---[  40]---> BDD-cost:    8
c ---[  37]---> BDD-cost:    7
c ---[  35]---> BDD-cost:    6
c ---[  34]---> BDD-cost:    8
c ---[  31]---> BDD-cost:    7
c ---[  30]---> BDD-cost:    7
c ---[  28]---> BDD-cost:    6
c ---[  27]---> BDD-cost:    8
c ---[  24]---> BDD-cost:    7
c ---[  23]---> BDD-cost:    3
c ---[  22]---> BDD-cost:    4
c ---[  21]---> BDD-cost:    4
c ---[  20]---> BDD-cost:    4
c ---[  19]---> BDD-cost:    4
c ---[  18]---> BDD-cost:    3
c ---[  17]---> BDD-cost:    4
c ---[  16]---> BDD-cost:    4
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    4
c ---[  13]---> BDD-cost:    4
c ---[  12]---> BDD-cost:    3
c ---[  11]---> BDD-cost:    4
c ---[  10]---> BDD-cost:    3
c ---[   9]---> BDD-cost:    4
c ---[   8]---> BDD-cost:    3
c ---[   7]---> BDD-cost:    4
c ---[   6]---> BDD-cost:    4
c ---[   5]---> BDD-cost:    3
c ---[   4]---> BDD-cost:    4
c ---[   3]---> BDD-cost:    4
c ---[   2]---> BDD-cost:    3
c ---[   1]---> BDD-cost:    4
c ---[   0]---> BDD-cost:    4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  564115  1659265 |  188038       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 1454400[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   94     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        35 |  562364  1654664 |  187454      34      436    12.8 |  0.000 % |
c ==============================================================================
c [1mFound solution: 1453376[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   56     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       113 |  562465  1654902 |  187488     112     5275    47.1 |  0.000 % |
c ==============================================================================
c [1mFound solution: 1447296[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   71     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       171 |  562477  1654905 |  187492     168     8681    51.7 |  0.000 % |
c ==============================================================================
c [1mFound solution: 1442496[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   80     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       225 |  562624  1655248 |  187541     222    11312    51.0 |  0.000 % |
c ==============================================================================
c [1mFound solution: 1434304[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   35     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       244 |  562686  1655396 |  187562     241    12652    52.5 |  0.000 % |
c ==============================================================================
c [1mFound solution: 1430976[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   62     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       280 |  562795  1655654 |  187598     277    16729    60.4 |  0.000 % |
c |       380 |  562795  1655654 |  206357     377    23858    63.3 |  0.552 % |
c |       531 |  562795  1655654 |  226993     528    40476    76.7 |  0.552 % |
c |       756 |  562795  1655654 |  249692     753    59749    79.3 |  0.552 % |
c |      1096 |  562795  1655654 |  274662    1093    83468    76.4 |  0.552 % |
c |      1605 |  562795  1655654 |  302128    1602   127752    79.7 |  0.552 % |
c |      2364 |  562795  1655654 |  332341    2361   210780    89.3 |  0.552 % |
c |      3504 |  562795  1655654 |  365575    3501   308244    88.0 |  0.552 % |
c ==============================================================================
c [1mFound solution: 1430464[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   58     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3523 |  562896  1655893 |  187632    3520   309459    87.9 |  0.552 % |
c |      3623 |  562896  1655893 |  206395    3620   316507    87.4 |  0.552 % |
c |      3776 |  562896  1655893 |  227034    3773   328490    87.1 |  0.552 % |
c |      4003 |  562896  1655893 |  249738    4000   346556    86.6 |  0.552 % |
c |      4342 |  562896  1655893 |  274712    4339   381744    88.0 |  0.552 % |
c |      4850 |  562896  1655893 |  302183    4847   427491    88.2 |  0.552 % |
c |      5609 |  562896  1655893 |  332401    5606   484925    86.5 |  0.552 % |
c |      6748 |  561453  1651909 |  365641    6744   579253    85.9 |  0.790 % |
c |      8457 |  561453  1651909 |  402205    8453   712661    84.3 |  0.790 % |
c |     11020 |  561453  1651909 |  442426   11016   927251    84.2 |  0.790 % |
c |     14865 |  561453  1651909 |  486669   14861  1299400    87.4 |  0.790 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -COL133_bit_7 -COL133_bit_6 -COL133_bit_5 -COL133_bit_4 -COL133_bit_3 -COL133_bit_2 COL133_bit_1 COL133_bit0 COL133_bit1 COL133_bit2 -COL133_bit3 -COL133_bit4 COL133_bit5 -COL133_bit6 COL133_bit7 COL133_bit8 COL133_bit9 -COL133_bit10 COL133_bit11 -COL133_bit12 COL133_bit13 -COL001_bit0 -COL002_bit0 -COL003_bit0 -COL004_bit0 -COL005_bit0 -COL006_bit0 COL007_bit0 -COL008_bit0 COL009_bit0 -COL010_bit0 -COL011_bit0 -COL012_bit0 -COL013_bit0 -COL014_bit0 -COL015_bit0 -COL016_bit0 -COL017_bit0 -COL018_bit0 COL019_bit0 -COL020_bit0 -COL021_bit0 -COL022_bit0 -COL023_bit0 -COL024_bit0 -COL025_bit0 -COL026_bit0 -COL027_bit0 -COL028_bit0 -COL029_bit0 -COL030_bit0 COL031_bit0 -COL032_bit0 -COL033_bit0 -COL034_bit0 -COL035_bit0 -COL036_bit0 -COL037_bit0 -COL038_bit0 -COL039_bit0 COL040_bit0 -COL041_bit0 -COL042_bit0 -COL043_bit0 -COL044_bit0 COL045_bit0 -COL046_bit0 -COL047_bit0 -COL048_bit0 -COL049_bit0 -COL050_bit0 -COL051_bit0 -COL052_bit0 -COL053_bit0 COL054_bit0 -COL055_bit0 -COL056_bit0 -COL057_bit0 COL058_bit0 COL059_bit0 -COL060_bit0 -COL061_bit0 -COL062_bit0 -COL063_bit0 -COL064_bit0 -COL065_bit0 -COL066_bit0 -COL067_bit0 -COL068_bit0 -COL069_bit0 -COL070_bit0 COL071_bit0 -COL072_bit0 COL129_bit0 COL130_bit0 -COL134_bit_7 -COL134_bit_6 -COL134_bit_5 -COL134_bit_4 -COL134_bit_3 -COL134_bit_2 -COL134_bit_1 COL134_bit0 COL134_bit1 -COL134_bit2 -COL134_bit3 -COL134_bit4 COL134_bit5 -COL134_bit6 COL134_bit7 -COL134_bit8 COL134_bit9 COL134_bit10 -COL134_bit11 -COL134_bit12 COL134_bit13 -COL135_bit_7 -COL135_bit_6 -COL135_bit_5 -COL135_bit_4 -COL135_bit_3 -COL135_bit_2 -COL135_bit_1 COL135_bit0 -COL135_bit1 COL135_bit2 -COL135_bit3 -COL135_bit4 -COL135_bit5 -COL135_bit6 COL135_bit7 COL135_bit8 COL135_bit9 -COL135_bit10 -COL135_bit11 -COL135_bit12 COL135_bit13 -COL136_bit_7 -COL136_bit_6 -COL136_bit_5 -COL136_bit_4 -COL136_bit_3 -COL136_bit_2 COL136_bit_1 COL136_bit0 -COL136_bit1 COL136_bit2 COL136_bit3 COL136_bit4 COL136_bit5 COL136_bit6 -COL136_bit7 COL136_bit8 -COL136_bit9 -COL136_bit10 -COL136_bit11 -COL136_bit12 COL136_bit13 -COL115_bit_7 -COL115_bit_6 -COL115_bit_5 -COL115_bit_4 -COL115_bit_3 -COL115_bit_2 -COL115_bit_1 -COL115_bit0 -COL115_bit1 -COL115_bit2 -COL115_bit3 -COL115_bit4 -COL115_bit5 -COL115_bit6 -COL115_bit7 -COL115_bit8 -COL115_bit9 -COL115_bit10 -COL115_bit11 -COL115_bit12 -COL116_bit_7 -COL116_bit_6 -COL116_bit_5 -COL116_bit_4 -COL116_bit_3 -COL116_bit_2 -COL116_bit_1 -COL116_bit0 -COL116_bit1 COL116_bit2 -COL116_bit3 COL116_bit4 -COL116_bit5 COL116_bit6 -COL116_bit7 COL116_bit8 -COL116_bit9 -COL116_bit10 -COL116_bit11 -COL116_bit12 -COL117_bit_7 -COL117_bit_6 -COL117_bit_5 -COL117_bit_4 -COL117_bit_3 -COL117_bit_2 -COL117_bit_1 -COL117_bit0 COL117_bit1 -COL117_bit2 -COL117_bit3 -COL117_bit4 -COL117_bit5 COL117_bit6 COL117_bit7 COL117_bit8 -COL117_bit9 -COL117_bit10 -COL117_bit11 -COL117_bit12 -COL118_bit_7 -COL118_bit_6 -COL118_bit_5 -COL118_bit_4 -COL118_bit_3 -COL118_bit_2 -COL118_bit_1 -COL118_bit0 -COL118_bit1 -COL118_bit2 -COL118_bit3 -COL118_bit4 -COL118_bit5 -COL118_bit6 -COL118_bit7 -COL118_bit8 -COL118_bit9 -COL118_bit10 -COL118_bit11 -COL118_bit12 -COL119_bit_7 -COL119_bit_6 -COL119_bit_5 -COL119_bit_4 -COL119_bit_3 -COL119_bit_2 -COL119_bit_1 -COL119_bit0 -COL119_bit1 -COL119_bit2 -COL119_bit3 -COL119_bit4 -COL119_bit5 -COL119_bit6 -COL119_bit7 -COL119_bit8 -COL119_bit9 -COL119_bit10 -COL119_bit11 -COL119_bit12 -COL120_bit_7 -COL120_bit_6 -COL120_bit_5 -COL120_bit_4 -COL120_bit_3 -COL120_bit_2 -COL120_bit_1 -COL120_bit0 -COL120_bit1 -COL120_bit2 -COL120_bit3 -COL120_bit4 -COL120_bit5 -COL120_bit6 -COL120_bit7 -COL120_bit8 -COL120_bit9 -COL120_bit10 -COL120_bit11 -COL120_bit12 -COL121_bit_7 -COL121_bit_6 -COL121_bit_5 -COL121_bit_4 -COL121_bit_3 -COL121_bit_2 -COL121_bit_1 -COL121_bit0 -COL121_bit1 -COL121_bit2 -COL121_bit3 -COL121_bit4 -COL121_bit5 -COL121_bit6 -COL121_bit7 -COL121_bit8 -COL121_bit9 -COL121_bit10 -COL121_bit11 -COL121_bit12 -COL122_bit_7 -COL122_bit_6 -COL122_bit_5 -COL122_bit_4 -COL122_bit_3 -COL122_bit_2 -COL122_bit_1 -COL122_bit0 -COL122_bit1 -COL122_bit2 -COL122_bit3 -COL122_bit4 -COL122_bit5 -COL122_bit6 -COL122_bit7 -COL122_bit8 -COL122_bit9 -COL122_bit10 -COL122_bit11 -COL122_bit12 -COL123_bit_7 -COL123_bit_6 -COL123_bit_5 -COL123_bit_4 -COL123_bit_3 -COL123_bit_2 -COL123_bit_1 -COL123_bit0 -COL123_bit1 -COL123_bit2 -COL123_bit3 -COL123_bit4 -COL123_bit5 -COL123_bit6 -COL123_bit7 -COL123_bit8 -COL123_bit9 -COL123_bit10 -COL123_bit11 -COL123_bit12 -COL124_bit_7 -COL124_bit_6 -COL124_bit_5 -COL124_bit_4 -COL124_bit_3 -COL124_bit_2 -COL124_bit_1 -COL124_bit0 -COL124_bit1 -COL124_bit2 -COL124_bit3 -COL124_bit4 -COL124_bit5 -COL124_bit6 -COL124_bit7 -COL124_bit8 -COL124_bit9 -COL124_bit10 -COL124_bit11 -COL124_bit12 -COL125_bit_7 -COL125_bit_6 -COL125_bit_5 -COL125_bit_4 -COL125_bit_3 -COL125_bit_2 -COL125_bit_1 -COL125_bit0 -COL125_bit1 -COL125_bit2 -COL125_bit3 -COL125_bit4 -COL125_bit5 -COL125_bit6 -COL125_bit7 -COL125_bit8 -COL125_bit9 -COL125_bit10 -COL125_bit11 -COL125_bit12 -COL126_bit_7 -COL126_bit_6 -COL126_bit_5 -COL126_bit_4 -COL126_bit_3 -COL126_bit_2 -COL126_bit_1 -COL126_bit0 -COL126_bit1 -COL126_bit2 -COL126_bit3 -COL126_bit4 -COL126_bit5 -COL126_bit6 -COL126_bit7 -COL126_bit8 -COL126_bit9 -COL126_bit10 -COL126_bit11 -COL126_bit12 -COL127_bit_7 -COL127_bit_6 -COL127_bit_5 -COL127_bit_4 -COL127_bit_3 -COL127_bit_2 -COL127_bit_1 -COL127_bit0 -COL127_bit1 -COL127_bit2 -COL127_bit3 -COL127_bit4 -COL127_bit5 -COL127_bit6 -COL127_bit7 -COL127_bit8 -COL127_bit9 -COL127_bit10 -COL127_bit11 -COL127_bit12 -COL128_bit_7 -COL128_bit_6 -COL128_bit_5 -COL128_bit_4 -COL128_bit_3 -COL128_bit_2 -COL128_bit_1 -COL128_bit0 COL128_bit1 COL128_bit2 COL128_bit3 -COL128_bit4 -COL128_bit5 -COL128_bit6 -COL128_bit7 COL128_bit8 -COL128_bit9 -COL128_bit10 -COL128_bit11 -COL128_bit12 -COL073_bit_7 -COL073_bit_6 -COL073_bit_5 -COL073_bit_4 -COL073_bit_3 -COL073_bit_2 -COL073_bit_1 -COL073_bit0 -COL073_bit1 -COL073_bit2 -COL073_bit3 -COL073_bit4 -COL073_bit5 -COL073_bit6 -COL073_bit7 -COL073_bit8 -COL073_bit9 -COL073_bit10 -COL073_bit11 -COL073_bit12 -COL074_bit_7 -COL074_bit_6 -COL074_bit_5 -COL074_bit_4 -COL074_bit_3 -COL074_bit_2 -COL074_bit_1 -COL074_bit0 -COL074_bit1 -COL074_bit2 -COL074_bit3 -COL074_bit4 -COL074_bit5 -COL074_bit6 -COL074_bit7 -COL074_bit8 -COL074_bit9 -COL074_bit10 -COL074_bit11 -COL074_bit12 -COL075_bit_7 -COL075_bit_6 -COL075_bit_5 -COL075_bit_4 -COL075_bit_3 -COL075_bit_2 -COL075_bit_1 -COL075_bit0 -COL075_bit1 -COL075_bit2 -COL075_bit3 -COL075_bit4 -COL075_bit5 -COL075_bit6 -COL075_bit7 -COL075_bit8 -COL075_bit9 -COL075_bit10 -COL075_bit11 -COL075_bit12 -COL076_bit_7 -COL076_bit_6 -COL076_bit_5 -COL076_bit_4 -COL076_bit_3 -COL076_bit_2 -COL076_bit_1 -COL076_bit0 -COL076_bit1 -COL076_bit2 -COL076_bit3 -COL076_bit4 -COL076_bit5 -COL076_bit6 -COL076_bit7 -COL076_bit8 -COL076_bit9 -COL076_bit10 -COL076_bit11 -COL076_bit12 -COL077_bit_7 -COL077_bit_6 -COL077_bit_5 -COL077_bit_4 -COL077_bit_3 -COL077_bit_2 -COL077_bit_1 -COL077_bit0 -COL077_bit1 -COL077_bit2 -COL077_bit3 -COL077_bit4 -COL077_bit5 -COL077_bit6 -COL077_bit7 -COL077_bit8 -COL077_bit9 -COL077_bit10 -COL077_bit11 -COL077_bit12 -COL078_bit_7 -COL078_bit_6 -COL078_bit_5 -COL078_bit_4 -COL078_bit_3 -COL078_bit_2 -COL078_bit_1 -COL078_bit0 -COL078_bit1 -COL078_bit2 -COL078_bit3 -COL078_bit4 -COL078_bit5 -COL078_bit6 -COL078_bit7 -COL078_bit8 -COL078_bit9 -COL078_bit10 -COL078_bit11 -COL078_bit12 -COL079_bit_7 -COL079_bit_6 -COL079_bit_5 -COL079_bit_4 -COL079_bit_3 -COL079_bit_2 -COL079_bit_1 -COL079_bit0 -COL079_bit1 COL079_bit2 COL079_bit3 -COL079_bit4 COL079_bit5 -COL079_bit6 -COL079_bit7 COL079_bit8 -COL079_bit9 -COL079_bit10 -COL079_bit11 -COL079_bit12 -COL085_bit_7 -COL085_bit_6 -COL085_bit_5 -COL085_bit_4 -COL085_bit_3 -COL085_bit_2 -COL085_bit_1 -COL085_bit0 -COL085_bit1 -COL085_bit2 -COL085_bit3 -COL085_bit4 -COL085_bit5 -COL085_bit6 -COL085_bit7 -COL085_bit8 -COL085_bit9 -COL085_bit10 -COL085_bit11 -COL085_bit12 -COL091_bit_7 -COL091_bit_6 -COL091_bit_5 -COL091_bit_4 -COL091_bit_3 -COL091_bit_2 -COL091_bit_1 -COL091_bit0 -COL091_bit1 -COL091_bit2 -COL091_bit3 -COL091_bit4 -COL091_bit5 -COL091_bit6 -COL091_bit7 -COL091_bit8 -COL091_bit9 -COL091_bit10 -COL091_bit11 -COL091_bit12 -COL097_bit_7 -COL097_bit_6 -COL097_bit_5 -COL097_bit_4 -COL097_bit_3 -COL097_bit_2 -COL097_bit_1 -COL097_bit0 -COL097_bit1 -COL097_bit2 -COL097_bit3 -COL097_bit4 -COL097_bit5 -COL097_bit6 -COL097_bit7 -COL097_bit8 -COL097_bit9 -COL097_bit10 -COL097_bit11 -COL097_bit12 -COL103_bit_7 -COL103_bit_6 -COL103_bit_5 -COL103_bit_4 -COL103_bit_3 -COL103_bit_2 -COL103_bit_1 -COL103_bit0 -COL103_bit1 -COL103_bit2 -COL103_bit3 -COL103_bit4 -COL103_bit5 -COL103_bit6 -COL103_bit7 -COL103_bit8 -COL103_bit9 -COL103_bit10 -COL103_bit11 -COL103_bit12 -COL109_bit_7 -COL109_bit_6 -COL109_bit_5 -COL109_bit_4 -COL109_bit_3 -COL109_bit_2 -COL109_bit_1 -COL109_bit0 -COL109_bit1 -COL109_bit2 -COL109_bit3 -COL109_bit4 -COL109_bit5 -COL109_bit6 -COL109_bit7 -COL109_bit8 -COL109_bit9 -COL109_bit10 -COL109_bit11 -COL109_bit12 -COL080_bit_7 -COL080_bit_6 -COL080_bit_5 -COL080_bit_4 -COL080_bit_3 -COL080_bit_2 -COL080_bit_1 -COL080_bit0 -COL080_bit1 -COL080_bit2 -COL080_bit3 -COL080_bit4 -COL080_bit5 -COL080_bit6 -COL080_bit7 -COL080_bit8 -COL080_bit9 -COL080_bit10 -COL080_bit11 -COL080_bit12 -COL081_bit_7 -COL081_bit_6 -COL081_bit_5 -COL081_bit_4 -COL081_bit_3 -COL081_bit_2 -COL081_bit_1 -COL081_bit0 -COL081_bit1 -COL081_bit2 -COL081_bit3 -COL081_bit4 -COL081_bit5 -COL081_bit6 -COL081_bit7 -COL081_bit8 -COL081_bit9 -COL081_bit10 -COL081_bit11 -COL081_bit12 -COL082_bit_7 -COL082_bit_6 -COL082_bit_5 -COL082_bit_4 -COL082_bit_3 -COL082_bit_2 -COL082_bit_1 -COL082_bit0 -COL082_bit1 -COL082_bit2 -COL082_bit3 -COL082_bit4 -COL082_bit5 -COL082_bit6 -COL082_bit7 -COL082_bit8 -COL082_bit9 -COL082_bit10 -COL082_bit11 -COL082_bit12 -COL083_bit_7 -COL083_bit_6 -COL083_bit_5 -COL083_bit_4 -COL083_bit_3 -COL083_bit_2 -COL083_bit_1 -COL083_bit0 -COL083_bit1 -COL083_bit2 -COL083_bit3 -COL083_bit4 -COL083_bit5 -COL083_bit6 -COL083_bit7 -COL083_bit8 -COL083_bit9 -COL083_bit10 -COL083_bit11 -COL083_bit12 -COL084_bit_7 -COL084_bit_6 -COL084_bit_5 -COL084_bit_4 -COL084_bit_3 -COL084_bit_2 -COL084_bit_1 -COL084_bit0 -COL084_bit1 -COL084_bit2 -COL084_bit3 -COL084_bit4 -COL084_bit5 -COL084_bit6 -COL084_bit7 -COL084_bit8 -COL084_bit9 -COL084_bit10 -COL084_bit11 -COL084_bit12 -COL086_bit_7 -COL086_bit_6 -COL086_bit_5 -COL086_bit_4 -COL086_bit_3 -COL086_bit_2 -COL086_bit_1 -COL086_bit0 -COL086_bit1 -COL086_bit2 -COL086_bit3 -COL086_bit4 -COL086_bit5 -COL086_bit6 -COL086_bit7 -COL086_bit8 -COL086_bit9 -COL086_bit10 -COL086_bit11 -COL086_bit12 -COL092_bit_7 -COL092_bit_6 -COL092_bit_5 -COL092_bit_4 -COL092_bit_3 -COL092_bit_2 -COL092_bit_1 -COL092_bit0 -COL092_bit1 -COL092_bit2 -COL092_bit3 -COL092_bit4 -COL092_bit5 -COL092_bit6 -COL092_bit7 -COL092_bit8 -COL092_bit9 -COL092_bit10 -COL092_bit11 -COL092_bit12 -COL098_bit_7 -COL098_bit_6 -COL098_bit_5 -COL098_bit_4 -COL098_bit_3 -COL098_bit_2 -COL098_bit_1 -COL098_bit0 -COL098_bit1 -COL098_bit2 -COL098_bit3 -COL098_bit4 -COL098_bit5 -COL098_bit6 -COL098_bit7 -COL098_bit8 -COL098_bit9 -COL098_bit10 -COL098_bit11 -COL098_bit12 -COL104_bit_7 -COL104_bit_6 -COL104_bit_5 -COL104_bit_4 -COL104_bit_3 -COL104_bit_2 -COL104_bit_1 -COL104_bit0 -COL104_bit1 -COL104_bit2 -COL104_bit3 -COL104_bit4 -COL104_bit5 -COL104_bit6 -COL104_bit7 -COL104_bit8 -COL104_bit9 -COL104_bit10 -COL104_bit11 -COL104_bit12 -COL110_bit_7 -COL110_bit_6 -COL110_bit_5 -COL110_bit_4 -COL110_bit_3 -COL110_bit_2 -COL110_bit_1 -COL110_bit0 -COL110_bit1 -COL110_bit2 -COL110_bit3 -COL110_bit4 -COL110_bit5 -COL110_bit6 -COL110_bit7 -COL110_bit8 -COL110_bit9 -COL110_bit10 -COL110_bit11 -COL110_bit12 -COL087_bit_7 -COL087_bit_6 -COL087_bit_5 -COL087_bit_4 -COL087_bit_3 -COL087_bit_2 -COL087_bit_1 -COL087_bit0 COL087_bit1 -COL087_bit2 COL087_bit3 COL087_bit4 COL087_bit5 COL087_bit6 COL087_bit7 -COL087_bit8 -COL087_bit9 -COL087_bit10 -COL087_bit11 -COL087_bit12 -COL088_bit_7 -COL088_bit_6 -COL088_bit_5 -COL088_bit_4 -COL088_bit_3 -COL088_bit_2 -COL088_bit_1 -COL088_bit0 -COL088_bit1 -COL088_bit2 -COL088_bit3 -COL088_bit4 -COL088_bit5 -COL088_bit6 -COL088_bit7 -COL088_bit8 -COL088_bit9 -COL088_bit10 -COL088_bit11 -COL088_bit12 -COL089_bit_7 -COL089_bit_6 -COL089_bit_5 -COL089_bit_4 -COL089_bit_3 -COL089_bit_2 -COL089_bit_1 -COL089_bit0 -COL089_bit1 -COL089_bit2 -COL089_bit3 -COL089_bit4 -COL089_bit5 -COL089_bit6 -COL089_bit7 -COL089_bit8 -COL089_bit9 -COL089_bit10 -COL089_bit11 -COL089_bit12 -COL090_bit_7 -COL090_bit_6 -COL090_bit_5 -COL090_bit_4 -COL090_bit_3 -COL090_bit_2 -COL090_bit_1 -COL090_bit0 -COL090_bit1 -COL090_bit2 -COL090_bit3 -COL090_bit4 -COL090_bit5 -COL090_bit6 -COL090_bit7 -COL090_bit8 -COL090_bit9 -COL090_bit10 -COL090_bit11 -COL090_bit12 -COL093_bit_7 -COL093_bit_6 -COL093_bit_5 -COL093_bit_4 -COL093_bit_3 -COL093_bit_2 -COL093_bit_1 -COL093_bit0 -COL093_bit1 -COL093_bit2 -COL093_bit3 -COL093_bit4 -COL093_bit5 -COL093_bit6 -COL093_bit7 -COL093_bit8 -COL093_bit9 -COL093_bit10 -COL093_bit11 -COL093_bit12 -COL099_bit_7 -COL099_bit_6 -COL099_bit_5 -COL099_bit_4 -COL099_bit_3 -COL099_bit_2 -COL099_bit_1 -COL099_bit0 -COL099_bit1 -COL099_bit2 -COL099_bit3 -COL099_bit4 -COL099_bit5 -COL099_bit6 -COL099_bit7 -COL099_bit8 -COL099_bit9 -COL099_bit10 -COL099_bit11 -COL099_bit12 -COL105_bit_7 -COL105_bit_6 -COL105_bit_5 -COL105_bit_4 -COL105_bit_3 -COL105_bit_2 -COL105_bit_1 -COL105_bit0 -COL105_bit1 -COL105_bit2 -COL105_bit3 -COL105_bit4 -COL105_bit5 -COL105_bit6 -COL105_bit7 -COL105_bit8 -COL105_bit9 -COL105_bit10 -COL105_bit11 -COL105_bit12 -COL111_bit_7 -COL111_bit_6 -COL111_bit_5 -COL111_bit_4 -COL111_bit_3 -COL111_bit_2 -COL111_bit_1 -COL111_bit0 -COL111_bit1 -COL111_bit2 -COL111_bit3 -COL111_bit4 -COL111_bit5 -COL111_bit6 -COL111_bit7 -COL111_bit8 -COL111_bit9 -COL111_bit10 -COL111_bit11 -COL111_bit12 -COL094_bit_7 -COL094_bit_6 -COL094_bit_5 -COL094_bit_4 -COL094_bit_3 -COL094_bit_2 -COL094_bit_1 -COL094_bit0 -COL094_bit1 -COL094_bit2 -COL094_bit3 -COL094_bit4 -COL094_bit5 -COL094_bit6 -COL094_bit7 -COL094_bit8 -COL094_bit9 -COL094_bit10 -COL094_bit11 -COL094_bit12 -COL095_bit_7 -COL095_bit_6 -COL095_bit_5 -COL095_bit_4 -COL095_bit_3 -COL095_bit_2 -COL095_bit_1 -COL095_bit0 -COL095_bit1 -COL095_bit2 -COL095_bit3 -COL095_bit4 -COL095_bit5 -COL095_bit6 -COL095_bit7 -COL095_bit8 -COL095_bit9 -COL095_bit10 -COL095_bit11 -COL095_bit12 -COL096_bit_7 -COL096_bit_6 -COL096_bit_5 -COL096_bit_4 -COL096_bit_3 -COL096_bit_2 -COL096_bit_1 -COL096_bit0 -COL096_bit1 -COL096_bit2 -COL096_bit3 -COL096_bit4 -COL096_bit5 -COL096_bit6 -COL096_bit7 -COL096_bit8 -COL096_bit9 -COL096_bit10 -COL096_bit11 -COL096_bit12 -COL100_bit_7 -COL100_bit_6 -COL100_bit_5 -COL100_bit_4 -COL100_bit_3 -COL100_bit_2 -COL100_bit_1 -COL100_bit0 -COL100_bit1 -COL100_bit2 -COL100_bit3 -COL100_bit4 -COL100_bit5 -COL100_bit6 -COL100_bit7 -COL100_bit8 -COL100_bit9 -COL100_bit10 -COL100_bit11 -COL100_bit12 -COL106_bit_7 -COL106_bit_6 -COL106_bit_5 -COL106_bit_4 -COL106_bit_3 -COL106_bit_2 -COL106_bit_1 -COL106_bit0 -COL106_bit1 -COL106_bit2 -COL106_bit3 -COL106_bit4 -COL106_bit5 -COL106_bit6 -COL106_bit7 -COL106_bit8 -COL106_bit9 -COL106_bit10 -COL106_bit11 -COL106_bit12 -COL112_bit_7 -COL112_bit_6 -COL112_bit_5 -COL112_bit_4 -COL112_bit_3 -COL112_bit_2 -COL112_bit_1 -COL112_bit0 -COL112_bit1 -COL112_bit2 -COL112_bit3 -COL112_bit4 -COL112_bit5 -COL112_bit6 -COL112_bit7 -COL112_bit8 -COL112_bit9 -COL112_bit10 -COL112_bit11 -COL112_bit12 -COL101_bit_7 -COL101_bit_6 -COL101_bit_5 -COL101_bit_4 -COL101_bit_3 -COL101_bit_2 -COL101_bit_1 -COL101_bit0 -COL101_bit1 -COL101_bit2 -COL101_bit3 -COL101_bit4 -COL101_bit5 -COL101_bit6 -COL101_bit7 -COL101_bit8 -COL101_bit9 -COL101_bit10 -COL101_bit11 -COL101_bit12 -COL102_bit_7 -COL102_bit_6 -COL102_bit_5 -COL102_bit_4 -COL102_bit_3 -COL102_bit_2 -COL102_bit_1 -COL102_bit0 -COL102_bit1 -COL102_bit2 -COL102_bit3 -COL102_bit4 -COL102_bit5 -COL102_bit6 -COL102_bit7 -COL102_bit8 -COL102_bit9 -COL102_bit10 -COL102_bit11 -COL102_bit12 -COL107_bit_7 -COL107_bit_6 -COL107_bit_5 -COL107_bit_4 -COL107_bit_3 -COL107_bit_2 -COL107_bit_1 -COL107_bit0 -COL107_bit1 COL107_bit2 COL107_bit3 COL107_bit4 COL107_bit5 -COL107_bit6 -COL107_bit7 -COL107_bit8 -COL107_bit9 -COL107_bit10 -COL107_bit11 -COL107_bit12 -COL11#### 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.80 0.95 0.91 2/54 12795
Raw data (stat): 12795 (runsolver) R 12794 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488871362 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.83 0.95 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18610 0 0 0 953 44 0 0 25 0 1 0 488871362 80785408 17250 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19723 17250 603 41 0 19682 0
vsize: 78892
[startup+20.0005 s]
Raw data (loadavg): 0.86 0.95 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18619 0 0 0 1953 44 0 0 25 0 1 0 488871362 80785408 17259 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19723 17259 603 41 0 19682 0
vsize: 78892
[startup+30.0015 s]
Raw data (loadavg): 0.88 0.95 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18637 0 0 0 2953 44 0 0 25 0 1 0 488871362 80916480 17277 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19755 17277 603 41 0 19714 0
vsize: 79020
[startup+40.0023 s]
Raw data (loadavg): 0.90 0.96 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18657 0 0 0 3953 45 0 0 25 0 1 0 488871362 80916480 17297 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19755 17297 603 41 0 19714 0
vsize: 79020
[startup+50.0024 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18678 0 0 0 4953 45 0 0 25 0 1 0 488871362 81043456 17318 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19786 17318 603 41 0 19745 0
vsize: 79144
[startup+60.002 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18696 0 0 0 5952 46 0 0 25 0 1 0 488871362 81174528 17336 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19818 17336 603 41 0 19777 0
vsize: 79272
[startup+70.0021 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18712 0 0 0 6952 46 0 0 25 0 1 0 488871362 81174528 17352 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19818 17352 603 41 0 19777 0
vsize: 79272
[startup+80.0033 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18731 0 0 0 7952 47 0 0 25 0 1 0 488871362 81301504 17371 4294967295 134512640 134672761 3221224544 3221223648 134560260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19849 17371 603 41 0 19808 0
vsize: 79396
[startup+90.003 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18756 0 0 0 8952 47 0 0 25 0 1 0 488871362 81428480 17396 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19880 17396 603 41 0 19839 0
vsize: 79520
[startup+100.003 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18775 0 0 0 9952 47 0 0 25 0 1 0 488871362 81428480 17415 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19880 17415 603 41 0 19839 0
vsize: 79520
[startup+110.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18794 0 0 0 10952 47 0 0 25 0 1 0 488871362 81555456 17434 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19911 17434 603 41 0 19870 0
vsize: 79644
[startup+120.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18821 0 0 0 11951 48 0 0 25 0 1 0 488871362 81686528 17461 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19943 17461 603 41 0 19902 0
vsize: 79772
[startup+130.005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18836 0 0 0 12951 48 0 0 25 0 1 0 488871362 81686528 17476 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19943 17476 603 41 0 19902 0
vsize: 79772
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18858 0 0 0 13951 49 0 0 25 0 1 0 488871362 81817600 17498 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19975 17498 603 41 0 19934 0
vsize: 79900
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18881 0 0 0 14951 49 0 0 25 0 1 0 488871362 81944576 17521 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20006 17521 603 41 0 19965 0
vsize: 80024
[startup+160.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18897 0 0 0 15950 49 0 0 25 0 1 0 488871362 81944576 17537 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20006 17537 603 41 0 19965 0
vsize: 80024
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18912 0 0 0 16951 49 0 0 25 0 1 0 488871362 82063360 17552 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20035 17552 603 41 0 19994 0
vsize: 80140
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18927 0 0 0 17951 49 0 0 25 0 1 0 488871362 82063360 17567 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20035 17567 603 41 0 19994 0
vsize: 80140
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18946 0 0 0 18951 49 0 0 25 0 1 0 488871362 82186240 17586 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20065 17586 603 41 0 20024 0
vsize: 80260
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18957 0 0 0 19951 49 0 0 25 0 1 0 488871362 82186240 17597 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20065 17597 603 41 0 20024 0
vsize: 80260
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12795
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18975 0 0 0 20951 49 0 0 25 0 1 0 488871362 82317312 17615 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20097 17615 603 41 0 20056 0
vsize: 80388
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 18986 0 0 0 21951 49 0 0 25 0 1 0 488871362 82317312 17626 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20097 17626 603 41 0 20056 0
vsize: 80388
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19002 0 0 0 22952 49 0 0 25 0 1 0 488871362 82456576 17642 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20131 17642 603 41 0 20090 0
vsize: 80524
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19028 0 0 0 23952 49 0 0 25 0 1 0 488871362 82456576 17668 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20131 17668 603 41 0 20090 0
vsize: 80524
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19044 0 0 0 24952 49 0 0 25 0 1 0 488871362 82579456 17684 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20161 17684 603 41 0 20120 0
vsize: 80644
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19061 0 0 0 25952 50 0 0 25 0 1 0 488871362 82579456 17701 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20161 17701 603 41 0 20120 0
vsize: 80644
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19079 0 0 0 26952 50 0 0 25 0 1 0 488871362 82714624 17719 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20194 17719 603 41 0 20153 0
vsize: 80776
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19093 0 0 0 27952 50 0 0 25 0 1 0 488871362 82714624 17733 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20194 17733 603 41 0 20153 0
vsize: 80776
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19111 0 0 0 28952 50 0 0 25 0 1 0 488871362 82845696 17751 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20226 17751 603 41 0 20185 0
vsize: 80904
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19127 0 0 0 29952 50 0 0 25 0 1 0 488871362 82845696 17767 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20226 17767 603 41 0 20185 0
vsize: 80904
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19144 0 0 0 30952 50 0 0 25 0 1 0 488871362 82976768 17784 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20258 17784 603 41 0 20217 0
vsize: 81032
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19164 0 0 0 31952 50 0 0 25 0 1 0 488871362 83107840 17804 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20290 17804 603 41 0 20249 0
vsize: 81160
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19183 0 0 0 32953 50 0 0 25 0 1 0 488871362 83107840 17823 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20290 17823 603 41 0 20249 0
vsize: 81160
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19204 0 0 0 33953 50 0 0 25 0 1 0 488871362 83230720 17844 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20320 17844 603 41 0 20279 0
vsize: 81280
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19225 0 0 0 34953 50 0 0 25 0 1 0 488871362 83357696 17865 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20351 17865 603 41 0 20310 0
vsize: 81404
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19237 0 0 0 35953 50 0 0 25 0 1 0 488871362 83357696 17877 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20351 17877 603 41 0 20310 0
vsize: 81404
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19252 0 0 0 36953 50 0 0 25 0 1 0 488871362 83357696 17892 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20351 17892 603 41 0 20310 0
vsize: 81404
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19269 0 0 0 37954 50 0 0 25 0 1 0 488871362 83488768 17909 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20383 17909 603 41 0 20342 0
vsize: 81532
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19285 0 0 0 38954 50 0 0 25 0 1 0 488871362 83488768 17925 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20383 17925 603 41 0 20342 0
vsize: 81532
[startup+400.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19297 0 0 0 39954 51 0 0 25 0 1 0 488871362 83619840 17937 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20415 17937 603 41 0 20374 0
vsize: 81660
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19307 0 0 0 40954 51 0 0 25 0 1 0 488871362 83619840 17947 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20415 17947 603 41 0 20374 0
vsize: 81660
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19321 0 0 0 41954 51 0 0 25 0 1 0 488871362 83738624 17961 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20444 17961 603 41 0 20403 0
vsize: 81776
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19339 0 0 0 42954 51 0 0 25 0 1 0 488871362 83738624 17979 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20444 17979 603 41 0 20403 0
vsize: 81776
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19354 0 0 0 43954 51 0 0 25 0 1 0 488871362 83857408 17994 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20473 17994 603 41 0 20432 0
vsize: 81892
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19372 0 0 0 44954 51 0 0 25 0 1 0 488871362 83857408 18012 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20473 18012 603 41 0 20432 0
vsize: 81892
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19388 0 0 0 45955 51 0 0 25 0 1 0 488871362 83976192 18028 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20502 18028 603 41 0 20461 0
vsize: 82008
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19412 0 0 0 46955 51 0 0 25 0 1 0 488871362 84127744 18052 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20539 18052 603 41 0 20498 0
vsize: 82156
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19427 0 0 0 47955 51 0 0 25 0 1 0 488871362 84127744 18067 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20539 18067 603 41 0 20498 0
vsize: 82156
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19442 0 0 0 48955 51 0 0 25 0 1 0 488871362 84258816 18082 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20571 18082 603 41 0 20530 0
vsize: 82284
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19456 0 0 0 49955 51 0 0 25 0 1 0 488871362 84258816 18096 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20571 18096 603 41 0 20530 0
vsize: 82284
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19470 0 0 0 50955 51 0 0 25 0 1 0 488871362 84365312 18110 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20597 18110 603 41 0 20556 0
vsize: 82388
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19491 0 0 0 51955 51 0 0 25 0 1 0 488871362 84492288 18131 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20628 18131 603 41 0 20587 0
vsize: 82512
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19526 0 0 0 52955 51 0 0 25 0 1 0 488871362 84615168 18166 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20658 18166 603 41 0 20617 0
vsize: 82632
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19536 0 0 0 53956 51 0 0 25 0 1 0 488871362 84615168 18176 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20658 18176 603 41 0 20617 0
vsize: 82632
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19556 0 0 0 54956 51 0 0 25 0 1 0 488871362 84738048 18196 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20688 18196 603 41 0 20647 0
vsize: 82752
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19569 0 0 0 55956 51 0 0 25 0 1 0 488871362 84738048 18209 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20688 18209 603 41 0 20647 0
vsize: 82752
[startup+570.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19584 0 0 0 56956 51 0 0 25 0 1 0 488871362 84844544 18224 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20714 18224 603 41 0 20673 0
vsize: 82856
[startup+580.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19602 0 0 0 57956 51 0 0 25 0 1 0 488871362 84844544 18242 4294967295 134512640 134672761 3221224544 3221223728 134559041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20714 18242 603 41 0 20673 0
vsize: 82856
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19613 0 0 0 58957 51 0 0 25 0 1 0 488871362 84963328 18253 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20743 18253 603 41 0 20702 0
vsize: 82972
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19625 0 0 0 59957 51 0 0 25 0 1 0 488871362 84963328 18265 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20743 18265 603 41 0 20702 0
vsize: 82972
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19643 0 0 0 60957 52 0 0 25 0 1 0 488871362 85098496 18283 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20776 18283 603 41 0 20735 0
vsize: 83104
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19660 0 0 0 61957 52 0 0 25 0 1 0 488871362 85098496 18300 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20776 18300 603 41 0 20735 0
vsize: 83104
[startup+630.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19672 0 0 0 62957 52 0 0 25 0 1 0 488871362 85204992 18312 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20802 18312 603 41 0 20761 0
vsize: 83208
[startup+640.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19697 0 0 0 63957 52 0 0 25 0 1 0 488871362 85315584 18337 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20829 18337 603 41 0 20788 0
vsize: 83316
[startup+650.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19711 0 0 0 64957 52 0 0 25 0 1 0 488871362 85315584 18351 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20829 18351 603 41 0 20788 0
vsize: 83316
[startup+660.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19740 0 0 0 65957 52 0 0 25 0 1 0 488871362 85450752 18380 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20862 18380 603 41 0 20821 0
vsize: 83448
[startup+670.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19762 0 0 0 66957 52 0 0 25 0 1 0 488871362 85573632 18402 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20892 18402 603 41 0 20851 0
vsize: 83568
[startup+680.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19783 0 0 0 67957 52 0 0 25 0 1 0 488871362 85696512 18423 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20922 18423 603 41 0 20881 0
vsize: 83688
[startup+690.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19801 0 0 0 68958 52 0 0 25 0 1 0 488871362 85696512 18441 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20922 18441 603 41 0 20881 0
vsize: 83688
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19826 0 0 0 69958 52 0 0 25 0 1 0 488871362 85819392 18466 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20952 18466 603 41 0 20911 0
vsize: 83808
[startup+710.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19845 0 0 0 70958 52 0 0 25 0 1 0 488871362 85954560 18485 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20985 18485 603 41 0 20944 0
vsize: 83940
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19866 0 0 0 71958 52 0 0 25 0 1 0 488871362 85954560 18506 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20985 18506 603 41 0 20944 0
vsize: 83940
[startup+730.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19887 0 0 0 72958 52 0 0 25 0 1 0 488871362 86073344 18527 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21014 18527 603 41 0 20973 0
vsize: 84056
[startup+740.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19905 0 0 0 73959 52 0 0 25 0 1 0 488871362 86192128 18545 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21043 18545 603 41 0 21002 0
vsize: 84172
[startup+750.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19923 0 0 0 74959 52 0 0 25 0 1 0 488871362 86192128 18563 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21043 18563 603 41 0 21002 0
vsize: 84172
[startup+760.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19938 0 0 0 75959 52 0 0 25 0 1 0 488871362 86327296 18578 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21076 18578 603 41 0 21035 0
vsize: 84304
[startup+770.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19956 0 0 0 76959 52 0 0 25 0 1 0 488871362 86327296 18596 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21076 18596 603 41 0 21035 0
vsize: 84304
[startup+780.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19971 0 0 0 77959 52 0 0 25 0 1 0 488871362 86450176 18611 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21106 18611 603 41 0 21065 0
vsize: 84424
[startup+790.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19983 0 0 0 78959 52 0 0 25 0 1 0 488871362 86450176 18623 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21106 18623 603 41 0 21065 0
vsize: 84424
[startup+800.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 19998 0 0 0 79959 52 0 0 25 0 1 0 488871362 86552576 18638 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21131 18638 603 41 0 21090 0
vsize: 84524
[startup+810.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20017 0 0 0 80960 52 0 0 25 0 1 0 488871362 86552576 18657 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21131 18657 603 41 0 21090 0
vsize: 84524
[startup+820.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20031 0 0 0 81960 52 0 0 25 0 1 0 488871362 86671360 18671 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21160 18671 603 41 0 21119 0
vsize: 84640
[startup+830.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20050 0 0 0 82960 53 0 0 25 0 1 0 488871362 86794240 18690 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21190 18690 603 41 0 21149 0
vsize: 84760
[startup+840.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20062 0 0 0 83960 53 0 0 25 0 1 0 488871362 86794240 18702 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21190 18702 603 41 0 21149 0
vsize: 84760
[startup+850.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20078 0 0 0 84960 53 0 0 25 0 1 0 488871362 86949888 18718 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21228 18718 603 41 0 21187 0
vsize: 84912
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20092 0 0 0 85961 53 0 0 25 0 1 0 488871362 86949888 18732 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21228 18732 603 41 0 21187 0
vsize: 84912
[startup+870.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20109 0 0 0 86961 53 0 0 25 0 1 0 488871362 86949888 18749 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21228 18749 603 41 0 21187 0
vsize: 84912
[startup+880.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20120 0 0 0 87959 53 0 0 25 0 1 0 488871362 87068672 18760 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21257 18760 603 41 0 21216 0
vsize: 85028
[startup+890.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20135 0 0 0 88958 54 0 0 25 0 1 0 488871362 87068672 18775 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21257 18775 603 41 0 21216 0
vsize: 85028
[startup+900.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20156 0 0 0 89958 54 0 0 25 0 1 0 488871362 87191552 18796 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21287 18796 603 41 0 21246 0
vsize: 85148
[startup+910.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20175 0 0 0 90958 54 0 0 25 0 1 0 488871362 87322624 18815 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21319 18815 603 41 0 21278 0
vsize: 85276
[startup+920.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20193 0 0 0 91958 55 0 0 25 0 1 0 488871362 87322624 18833 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21319 18833 603 41 0 21278 0
vsize: 85276
[startup+930.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20217 0 0 0 92958 55 0 0 25 0 1 0 488871362 87511040 18857 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21365 18857 603 41 0 21324 0
vsize: 85460
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20235 0 0 0 93958 55 0 0 25 0 1 0 488871362 87511040 18875 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21365 18875 603 41 0 21324 0
vsize: 85460
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20255 0 0 0 94957 56 0 0 25 0 1 0 488871362 87633920 18895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21395 18895 603 41 0 21354 0
vsize: 85580
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20273 0 0 0 95957 56 0 0 25 0 1 0 488871362 87822336 18913 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21441 18913 603 41 0 21400 0
vsize: 85764
[startup+970.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20281 0 0 0 96957 57 0 0 25 0 1 0 488871362 87822336 18921 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21441 18921 603 41 0 21400 0
vsize: 85764
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20297 0 0 0 97957 57 0 0 25 0 1 0 488871362 87822336 18937 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21441 18937 603 41 0 21400 0
vsize: 85764
[startup+990.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20313 0 0 0 98956 57 0 0 25 0 1 0 488871362 87949312 18953 4294967295 134512640 134672761 3221224544 3221223680 134565116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21472 18953 603 41 0 21431 0
vsize: 85888
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20325 0 0 0 99956 58 0 0 25 0 1 0 488871362 87949312 18965 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21472 18965 603 41 0 21431 0
vsize: 85888
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20344 0 0 0 100955 59 0 0 25 0 1 0 488871362 88076288 18984 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21503 18984 603 41 0 21462 0
vsize: 86012
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20360 0 0 0 101955 59 0 0 25 0 1 0 488871362 88076288 19000 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21503 19000 603 41 0 21462 0
vsize: 86012
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20377 0 0 0 102954 59 0 0 25 0 1 0 488871362 88207360 19017 4294967295 134512640 134672761 3221224544 3221223744 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21535 19017 603 41 0 21494 0
vsize: 86140
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20390 0 0 0 103955 59 0 0 25 0 1 0 488871362 88207360 19030 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21535 19030 603 41 0 21494 0
vsize: 86140
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20405 0 0 0 104955 59 0 0 25 0 1 0 488871362 88338432 19045 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21567 19045 603 41 0 21526 0
vsize: 86268
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20427 0 0 0 105955 59 0 0 25 0 1 0 488871362 88338432 19067 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21567 19067 603 41 0 21526 0
vsize: 86268
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20442 0 0 0 106955 59 0 0 25 0 1 0 488871362 88465408 19082 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21598 19082 603 41 0 21557 0
vsize: 86392
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20454 0 0 0 107955 59 0 0 25 0 1 0 488871362 88465408 19094 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21598 19094 603 41 0 21557 0
vsize: 86392
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20480 0 0 0 108955 59 0 0 25 0 1 0 488871362 88645632 19120 4294967295 134512640 134672761 3221224544 3221223728 134558658 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21642 19120 603 41 0 21601 0
vsize: 86568
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20495 0 0 0 109956 59 0 0 25 0 1 0 488871362 88645632 19135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21642 19135 603 41 0 21601 0
vsize: 86568
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20509 0 0 0 110956 60 0 0 25 0 1 0 488871362 88772608 19149 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21673 19149 603 41 0 21632 0
vsize: 86692
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20519 0 0 0 111956 60 0 0 25 0 1 0 488871362 88772608 19159 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21673 19159 603 41 0 21632 0
vsize: 86692
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20531 0 0 0 112956 60 0 0 25 0 1 0 488871362 88903680 19171 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21705 19171 603 41 0 21664 0
vsize: 86820
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20547 0 0 0 113955 60 0 0 25 0 1 0 488871362 88903680 19187 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21705 19187 603 41 0 21664 0
vsize: 86820
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20560 0 0 0 114955 60 0 0 25 0 1 0 488871362 89030656 19200 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21736 19200 603 41 0 21695 0
vsize: 86944
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20572 0 0 0 115956 60 0 0 25 0 1 0 488871362 89030656 19212 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21736 19212 603 41 0 21695 0
vsize: 86944
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20586 0 0 0 116956 60 0 0 25 0 1 0 488871362 89030656 19226 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21736 19226 603 41 0 21695 0
vsize: 86944
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20606 0 0 0 117956 60 0 0 25 0 1 0 488871362 89161728 19246 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21768 19246 603 41 0 21727 0
vsize: 87072
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20618 0 0 0 118956 60 0 0 25 0 1 0 488871362 89292800 19258 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21800 19258 603 41 0 21759 0
vsize: 87200
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12797
Raw data (stat): 12795 (minisat+) R 12794 22932 22931 0 -1 0 20633 0 0 0 119956 60 0 0 25 0 1 0 488871362 89292800 19273 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21800 19273 603 41 0 21759 0
vsize: 87200
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 12797
Raw data (stat): 12795 (minisat+) Z 12794 22932 22931 0 -1 12 20636 0 0 0 119956 64 0 0 25 0 1 0 488871362 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.21
CPU user time (s): 1199.57
CPU system time (s): 0.645901
CPU usage (%): 100.012
Max. virtual memory (Kb): 87200
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####