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/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-sc50b.opb
MD5SUM	36d973d6ac0a73f611c4998ee3e157d3
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	20
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	1048575
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	5767168
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	22020075
Number of bits of the biggest sum of numbers	25
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	2.84657
Number of variables	960
Total number of constraints	48
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	48
Minimum length of a constraint	40
Maximum length of a constraint	80
Trace number 16093

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-21 06:14:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16169 boxname=wulflinc9 idbench=1244 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  36d973d6ac0a73f611c4998ee3e157d3  /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-sc50b.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-sc50b.opb /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-sc50b.opb
IDLAUNCH: 16169
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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:        460080 kB
Buffers:         35884 kB
Cached:         515316 kB
SwapCached:          8 kB
Active:         126108 kB
Inactive:       427908 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        459828 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6824 kB
Slab:            14820 kB
Committed_AS:    63580 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 06:34:35 (client local time) WITH STATUS 10 IN 1200.32 SECONDS
stats: 16169 7 1200.32 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 68 PB-constraints to clauses...
c   -- Unit propagations: ppppppp
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[  67]---> Adder-cost: 56   maxlim: 36348   bits: 16/16
c ---[  65]---> Adder-cost: 30   maxlim: 32767   bits: 16/15
c ---[  63]---> Adder-cost: 28   maxlim: 16383   bits: 15/14
c ---[  61]---> Adder-cost: 28   maxlim: 16383   bits: 15/14
c ---[  59]---> Adder-cost: 28   maxlim: 16383   bits: 15/14
c ---[  58]---> Adder-cost: 28   maxlim: 16382   bits: 15/14
c ---[  57]---> Adder-cost: 28   maxlim: 16382   bits: 15/14
c ---[  56]---> Adder-cost: 28   maxlim: 16382   bits: 15/14
c ---[  55]---> Adder-cost: 178   maxlim: 256502   bits: 19/18
c ---[  54]---> Adder-cost: 59   maxlim: 65533   bits: 17/16
c ---[  53]---> Adder-cost: 90   maxlim: 98300   bits: 18/17
c ---[  51]---> Adder-cost: 120   maxlim: 360437   bits: 20/19
c ---[  49]---> Adder-cost: 64   maxlim: 98302   bits: 18/17
c ---[  47]---> Adder-cost: 60   maxlim: 65535   bits: 17/16
c ---[  45]---> Adder-cost: 60   maxlim: 65535   bits: 17/16
c ---[  43]---> Adder-cost: 60   maxlim: 65535   bits: 17/16
c ---[  42]---> Adder-cost: 32   maxlim: 65534   bits: 17/16
c ---[  41]---> Adder-cost: 32   maxlim: 65534   bits: 17/16
c ---[  40]---> Adder-cost: 32   maxlim: 65534   bits: 17/16
c ---[  39]---> Adder-cost: 192   maxlim: 551414   bits: 20/20
c ---[  38]---> Adder-cost: 67   maxlim: 262141   bits: 19/18
c ---[  37]---> Adder-cost: 102   maxlim: 393212   bits: 20/19
c ---[  35]---> Adder-cost: 128   maxlim: 720885   bits: 21/20
c ---[  33]---> Adder-cost: 68   maxlim: 262142   bits: 19/18
c ---[  31]---> Adder-cost: 64   maxlim: 131071   bits: 18/17
c ---[  29]---> Adder-cost: 64   maxlim: 131071   bits: 18/17
c ---[  27]---> Adder-cost: 64   maxlim: 131071   bits: 18/17
c ---[  26]---> Adder-cost: 34   maxlim: 131070   bits: 18/17
c ---[  25]---> Adder-cost: 34   maxlim: 131070   bits: 18/17
c ---[  24]---> Adder-cost: 34   maxlim: 131070   bits: 18/17
c ---[  23]---> Adder-cost: 194   maxlim: 551414   bits: 20/20
c ---[  22]---> Adder-cost: 71   maxlim: 524285   bits: 20/19
c ---[  21]---> Adder-cost: 108   maxlim: 786428   bits: 21/20
c ---[  19]---> Adder-cost: 136   maxlim: 1441781   bits: 22/21
c ---[  17]---> Adder-cost: 72   maxlim: 524286   bits: 20/19
c ---[  15]---> Adder-cost: 68   maxlim: 262143   bits: 19/18
c ---[  13]---> Adder-cost: 68   maxlim: 262143   bits: 19/18
c ---[  11]---> Adder-cost: 68   maxlim: 262143   bits: 19/18
c ---[  10]---> Adder-cost: 36   maxlim: 262142   bits: 19/18
c ---[   9]---> Adder-cost: 36   maxlim: 262142   bits: 19/18
c ---[   8]---> Adder-cost: 36   maxlim: 262142   bits: 19/18
c ---[   7]---> Adder-cost: 206   maxlim: 1141238   bits: 21/21
c ---[   6]---> Adder-cost: 75   maxlim: 1048573   bits: 21/20
c ---[   5]---> Adder-cost: 114   maxlim: 1572860   bits: 22/21
c ---[   3]---> Adder-cost: 144   maxlim: 2883573   bits: 23/22
c ---[   2]---> Adder-cost: 174   maxlim: 786425   bits: 21/20
c ---[   1]---> Adder-cost: 71   maxlim: 524285   bits: 20/19
c ---[   0]---> Adder-cost: 108   maxlim: 786428   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   23026    84742 |    7675       0        0     nan |  0.000 % |
c |       100 |   23026    84742 |    8442     100      817     8.2 | 26.170 % |
c |       250 |   23026    84742 |    9286     250     2725    10.9 | 26.170 % |
c |       475 |   23019    84719 |   10215     474     4596     9.7 | 26.189 % |
c |       812 |   22999    84655 |   11236     808    15519    19.2 | 26.244 % |
c |      1318 |   22982    84600 |   12360    1312    23748    18.1 | 26.299 % |
c |      2079 |   22982    84600 |   13596    2073    31317    15.1 | 26.299 % |
c |      3219 |   22982    84600 |   14956    3213    45263    14.1 | 26.299 % |
c |      4929 |   22907    84357 |   16452    4905    64850    13.2 | 26.502 % |
c |      7491 |   22779    83937 |   18097    7398    93765    12.7 | 26.852 % |
c |     11336 |   22607    83347 |   19906   10957   130746    11.9 | 27.221 % |
c ==============================================================================
c [1mFound solution: 0[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14471 |   22121    81758 |    7373   13850   168762    12.2 | 27.221 % |
c |     14571 |   22121    81758 |    8110    7025    74828    10.7 | 28.474 % |
c |     14721 |   22085    81626 |    8921    6640    71176    10.7 | 28.492 % |
c |     14947 |   21963    81184 |    9813    6356    68044    10.7 | 28.621 % |
c |     15284 |   21947    81130 |   10794    6689    71844    10.7 | 28.658 % |
c |     15791 |   21907    80986 |   11874    7015    77016    11.0 | 28.714 % |
c |     16550 |   21907    80986 |   13061    7774    95179    12.2 | 28.714 % |
c |     17690 |   21907    80986 |   14367    8914   110037    12.3 | 28.714 % |
c |     19399 |   21683    80214 |   15804    9966   122384    12.3 | 29.230 % |
c |     21962 |   21674    80183 |   17385   12519   169098    13.5 | 29.266 % |
c |     25806 |   21626    80007 |   19123   16321   248392    15.2 | 29.340 % |
c |     31572 |   21450    79385 |   21036   11143   199508    17.9 | 29.561 % |
c |     40222 |   21436    79339 |   23139   19790   462664    23.4 | 29.598 % |
c |     53196 |   21401    79224 |   25453   19696   705009    35.8 | 29.690 % |
c |     72658 |   21385    79172 |   27998   23155   621235    26.8 | 29.746 % |
c |    101850 |   21264    78769 |   30798   21825   524760    24.0 | 30.059 % |
c |    145639 |   21126    78307 |   33878   31233   709914    22.7 | 30.391 % |
c |    211324 |   21126    78307 |   37266   35657  1755002    49.2 | 30.393 % |
c |    309851 |   21067    78094 |   40993   36256  2281989    62.9 | 30.446 % |
c |    457641 |   21060    78071 |   45092   43490  1467896    33.8 | 30.464 % |
c |    679325 |   21042    78009 |   49601   19050   719097    37.7 | 30.504 % |
c |   1011850 |   21018    77929 |   54562   36763  1626732    44.2 | 30.593 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -COL00004_bit_7 -COL00004_bit_6 -COL00004_bit_5 -COL00004_bit_4 -COL00004_bit_3 -COL00004_bit_2 -COL00004_bit_1 -COL00004_bit0 -COL00004_bit1 -COL00004_bit2 -COL00004_bit3 -COL00004_bit4 -COL00004_bit5 -COL00004_bit6 -COL00004_bit7 -COL00004_bit8 -COL00004_bit9 -COL00004_bit10 -COL00004_bit11 -COL00004_bit12 COL00001_bit_7 -COL00001_bit_6 -COL00001_bit_5 -COL00001_bit_4 -COL00001_bit_3 -COL00001_bit_2 -COL00001_bit_1 -COL00001_bit0 -COL00001_bit1 -COL00001_bit2 -COL00001_bit3 -COL00001_bit4 -COL00001_bit5 -COL00001_bit6 -COL00001_bit7 -COL00001_bit8 -COL00001_bit9 -COL00001_bit10 -COL00001_bit11 -COL00001_bit12 -COL00002_bit_7 -COL00002_bit_6 -COL00002_bit_5 -COL00002_bit_4 -COL00002_bit_3 -COL00002_bit_2 -COL00002_bit_1 -COL00002_bit0 -COL00002_bit1 -COL00002_bit2 -COL00002_bit3 -COL00002_bit4 -COL00002_bit5 -COL00002_bit6 -COL00002_bit7 -COL00002_bit8 -COL00002_bit9 -COL00002_bit10 -COL00002_bit11 -COL00002_bit12 -COL00003_bit_7 -COL00003_bit_6 -COL00003_bit_5 -COL00003_bit_4 -COL00003_bit_3 -COL00003_bit_2 -COL00003_bit_1 -COL00003_bit0 -COL00003_bit1 -COL00003_bit2 -COL00003_bit3 -COL00003_bit4 -COL00003_bit5 -COL00003_bit6 -COL00003_bit7 -COL00003_bit8 -COL00003_bit9 -COL00003_bit10 -COL00003_bit11 -COL00003_bit12 -COL00005_bit_7 -COL00005_bit_6 -COL00005_bit_5 -COL00005_bit_4 -COL00005_bit_3 -COL00005_bit_2 -COL00005_bit_1 -COL00005_bit0 -COL00005_bit1 -COL00005_bit2 -COL00005_bit3 -COL00005_bit4 -COL00005_bit5 -COL00005_bit6 -COL00005_bit7 -COL00005_bit8 -COL00005_bit9 -COL00005_bit10 -COL00005_bit11 -COL00005_bit12 COL00006_bit_7 -COL00006_bit_6 -COL00006_bit_5 -COL00006_bit_4 -COL00006_bit_3 -COL00006_bit_2 -COL00006_bit_1 -COL00006_bit0 -COL00006_bit1 -COL00006_bit2 -COL00006_bit3 -COL00006_bit4 -COL00006_bit5 -COL00006_bit6 -COL00006_bit7 -COL00006_bit8 -COL00006_bit9 -COL00006_bit10 -COL00006_bit11 -COL00006_bit12 -COL00007_bit_7 -COL00007_bit_6 -COL00007_bit_5 -COL00007_bit_4 -COL00007_bit_3 -COL00007_bit_2 -COL00007_bit_1 -COL00007_bit0 -COL00007_bit1 -COL00007_bit2 -COL00007_bit3 -COL00007_bit4 -COL00007_bit5 -COL00007_bit6 -COL00007_bit7 -COL00007_bit8 -COL00007_bit9 -COL00007_bit10 -COL00007_bit11 -COL00007_bit12 -COL00008_bit_7 -COL00008_bit_6 -COL00008_bit_5 -COL00008_bit_4 -COL00008_bit_3 -COL00008_bit_2 -COL00008_bit_1 -COL00008_bit0 -COL00008_bit1 -COL00008_bit2 -COL00008_bit3 -COL00008_bit4 -COL00008_bit5 -COL00008_bit6 -COL00008_bit7 -COL00008_bit8 -COL00008_bit9 -COL00008_bit10 -COL00008_bit11 -COL00008_bit12 COL00009_bit_7 -COL00009_bit_6 -COL00009_bit_5 -COL00009_bit_4 -COL00009_bit_3 -COL00009_bit_2 -COL00009_bit_1 -COL00009_bit0 -COL00009_bit1 -COL00009_bit2 -COL00009_bit3 -COL00009_bit4 -COL00009_bit5 -COL00009_bit6 -COL00009_bit7 -COL00009_bit8 -COL00009_bit9 -COL00009_bit10 -COL00009_bit11 -COL00009_bit12 -COL00010_bit_7 -COL00010_bit_6 -COL00010_bit_5 -COL00010_bit_4 -COL00010_bit_3 -COL00010_bit_2 -COL00010_bit_1 -COL00010_bit0 -COL00010_bit1 -COL00010_bit2 -COL00010_bit3 -COL00010_bit4 -COL00010_bit5 -COL00010_bit6 -COL00010_bit7 -COL00010_bit8 -COL00010_bit9 -COL00010_bit10 -COL00010_bit11 -COL00010_bit12 -COL00011_bit_7 -COL00011_bit_6 -COL00011_bit_5 -COL00011_bit_4 -COL00011_bit_3 -COL00011_bit_2 -COL00011_bit_1 -COL00011_bit0 -COL00011_bit1 -COL00011_bit2 -COL00011_bit3 -COL00011_bit4 -COL00011_bit5 -COL00011_bit6 -COL00011_bit7 -COL00011_bit8 -COL00011_bit9 -COL00011_bit10 -COL00011_bit11 -COL00011_bit12 COL00012_bit_7 COL00012_bit_6 COL00012_bit_5 COL00012_bit_4 -COL00012_bit_3 COL00012_bit_2 -COL00012_bit_1 -COL00012_bit0 -COL00012_bit1 -COL00012_bit2 -COL00012_bit3 -COL00012_bit4 -COL00012_bit5 -COL00012_bit6 -COL00012_bit7 -COL00012_bit8 -COL00012_bit9 -COL00012_bit10 -COL00012_bit11 -COL00012_bit12 -COL00013_bit_7 -COL00013_bit_6 COL00013_bit_5 COL00013_bit_4 COL00013_bit_3 -COL00013_bit_2 -COL00013_bit_1 -COL00013_bit0 -COL00013_bit1 -COL00013_bit2 -COL00013_bit3 -COL00013_bit4 -COL00013_bit5 COL00013_bit6 -COL00013_bit7 -COL00013_bit8 -COL00013_bit9 -COL00013_bit10 -COL00013_bit11 -COL00013_bit12 -COL00014_bit_7 -COL00014_bit_6 -COL00014_bit_5 -COL00014_bit_4 -COL00014_bit_3 -COL00014_bit_2 -COL00014_bit_1 -COL00014_bit0 -COL00014_bit1 -COL00014_bit2 -COL00014_bit3 -COL00014_bit4 -COL00014_bit5 -COL00014_bit6 -COL00014_bit7 -COL00014_bit8 -COL00014_bit9 -COL00014_bit10 -COL00014_bit11 -COL00014_bit12 -COL00015_bit_7 -COL00015_bit_6 -COL00015_bit_5 -COL00015_bit_4 -COL00015_bit_3 -COL00015_bit_2 -COL00015_bit_1 -COL00015_bit0 -COL00015_bit1 -COL00015_bit2 -COL00015_bit3 -COL00015_bit4 -COL00015_bit5 -COL00015_bit6 -COL00015_bit7 -COL00015_bit8 -COL00015_bit9 -COL00015_bit10 -COL00015_bit11 -COL00015_bit12 -COL00016_bit_7 -COL00016_bit_6 -COL00016_bit_5 -COL00016_bit_4 -COL00016_bit_3 -COL00016_bit_2 -COL00016_bit_1 -COL00016_bit0 -COL00016_bit1 -COL00016_bit2 -COL00016_bit3 -COL00016_bit4 -COL00016_bit5 -COL00016_bit6 -COL00016_bit7 -COL00016_bit8 -COL00016_bit9 -COL00016_bit10 -COL00016_bit11 -COL00016_bit12 -COL00017_bit_7 -COL00017_bit_6 -COL00017_bit_5 -COL00017_bit_4 COL00017_bit_3 COL00017_bit_2 -COL00017_bit_1 -COL00017_bit0 -COL00017_bit1 -COL00017_bit2 -COL00017_bit3 -COL00017_bit4 -COL00017_bit5 -COL00017_bit6 -COL00017_bit7 -COL00017_bit8 -COL00017_bit9 -COL00017_bit10 -COL00017_bit11 -COL00017_bit12 -COL00018_bit_7 -COL00018_bit_6 COL00018_bit_5 COL00018_bit_4 COL00018_bit_3 -COL00018_bit_2 -COL00018_bit_1 -COL00018_bit0 -COL00018_bit1 -COL00018_bit2 -COL00018_bit3 -COL00018_bit4 -COL00018_bit5 COL00018_bit6 -COL00018_bit7 -COL00018_bit8 -COL00018_bit9 -COL00018_bit10 -COL00018_bit11 -COL00018_bit12 -COL00019_bit_7 -COL00019_bit_6 -COL00019_bit_5 -COL00019_bit_4 -COL00019_bit_3 -COL00019_bit_2 -COL00019_bit_1 -COL00019_bit0 -COL00019_bit1 -COL00019_bit2 -COL00019_bit3 -COL00019_bit4 -COL00019_bit5 -COL00019_bit6 -COL00019_bit7 -COL00019_bit8 -COL00019_bit9 -COL00019_bit10 -COL00019_bit11 -COL00019_bit12 -COL00020_bit_7 -COL00020_bit_6 -COL00020_bit_5 -COL00020_bit_4 COL00020_bit_3 COL00020_bit_2 -COL00020_bit_1 -COL00020_bit0 -COL00020_bit1 -COL00020_bit2 -COL00020_bit3 -COL00020_bit4 -COL00020_bit5 -COL00020_bit6 -COL00020_bit7 -COL00020_bit8 -COL00020_bit9 -COL00020_bit10 -COL00020_bit11 -COL00020_bit12 COL00021_bit_7 -COL00021_bit_6 -COL00021_bit_5 COL00021_bit_4 -COL00021_bit_3 COL00021_bit_2 -COL00021_bit_1 -COL00021_bit0 -COL00021_bit1 -COL00021_bit2 -COL00021_bit3 -COL00021_bit4 -COL00021_bit5 -COL00021_bit6 -COL00021_bit7 -COL00021_bit8 -COL00021_bit9 -COL00021_bit10 -COL00021_bit11 -COL00021_bit12 -COL00022_bit_7 -COL00022_bit_6 -COL00022_bit_5 -COL00022_bit_4 -COL00022_bit_3 -COL00022_bit_2 -COL00022_bit_1 -COL00022_bit0 -COL00022_bit1 -COL00022_bit2 -COL00022_bit3 -COL00022_bit4 -COL00022_bit5 -COL00022_bit6 -COL00022_bit7 -COL00022_bit8 -COL00022_bit9 -COL00022_bit10 -COL00022_bit11 -COL00022_bit12 -COL00023_bit_7 COL00023_bit_6 -COL00023_bit_5 -COL00023_bit_4 -COL00023_bit_3 -COL00023_bit_2 -COL00023_bit_1 -COL00023_bit0 -COL00023_bit1 -COL00023_bit2 -COL00023_bit3 -COL00023_bit4 -COL00023_bit5 -COL00023_bit6 -COL00023_bit7 -COL00023_bit8 -COL00023_bit9 -COL00023_bit10 -COL00023_bit11 -COL00023_bit12 COL00024_bit_7 COL00024_bit_6 COL00024_bit_5 -COL00024_bit_4 -COL00024_bit_3 -COL00024_bit_2 -COL00024_bit_1 -COL00024_bit0 -COL00024_bit1 -COL00024_bit2 -COL00024_bit3 -COL00024_bit4 -COL00024_bit5 -COL00024_bit6 -COL00024_bit7 -COL00024_bit8 -COL00024_bit9 -COL00024_bit10 -COL00024_bit11 -COL00024_bit12 -COL00025_bit_7 -COL00025_bit_6 -COL00025_bit_5 -COL00025_bit_4 -COL00025_bit_3 -COL00025_bit_2 -COL00025_bit_1 -COL00025_bit0 -COL00025_bit1 -COL00025_bit2 -COL00025_bit3 -COL00025_bit4 -COL00025_bit5 -COL00025_bit6 -COL00025_bit7 -COL00025_bit8 -COL00025_bit9 -COL00025_bit10 -COL00025_bit11 -COL00025_bit12 -COL00026_bit_7 -COL00026_bit_6 -COL00026_bit_5 -COL00026_bit_4 -COL00026_bit_3 -COL00026_bit_2 -COL00026_bit_1 -COL00026_bit0 -COL00026_bit1 -COL00026_bit2 -COL00026_bit3 -COL00026_bit4 -COL00026_bit5 -COL00026_bit6 -COL00026_bit7 -COL00026_bit8 -COL00026_bit9 -COL00026_bit10 -COL00026_bit11 -COL00026_bit12 -COL00027_bit_7 -COL00027_bit_6 -COL00027_bit_5 -COL00027_bit_4 -COL00027_bit_3 -COL00027_bit_2 -COL00027_bit_1 -COL00027_bit0 -COL00027_bit1 -COL00027_bit2 -COL00027_bit3 -COL00027_bit4 -COL00027_bit5 -COL00027_bit6 -COL00027_bit7 -COL00027_bit8 -COL00027_bit9 -COL00027_bit10 -COL00027_bit11 -COL00027_bit12 -COL00028_bit_7 COL00028_bit_6 -COL00028_bit_5 -COL00028_bit_4 COL00028_bit_3 COL00028_bit_2 -COL00028_bit_1 -COL00028_bit0 -COL00028_bit1 -COL00028_bit2 -COL00028_bit3 -COL00028_bit4 -COL00028_bit5 -COL00028_bit6 -COL00028_bit7 -COL00028_bit8 -COL00028_bit9 -COL00028_bit10 -COL00028_bit11 -COL00028_bit12 COL00029_bit_7 COL00029_bit_6 -COL00029_bit_5 -COL00029_bit_4 -COL00029_bit_3 COL00029_bit_2 -COL00029_bit_1 -COL00029_bit0 -COL00029_bit1 -COL00029_bit2 -COL00029_bit3 -COL00029_bit4 -COL00029_bit5 COL00029_bit6 -COL00029_bit7 -COL00029_bit8 -COL00029_bit9 -COL00029_bit10 -COL00029_bit11 -COL00029_bit12 -COL00030_bit_7 -COL00030_bit_6 -COL00030_bit_5 -COL00030_bit_4 -COL00030_bit_3 -COL00030_bit_2 -COL00030_bit_1 -COL00030_bit0 -COL00030_bit1 -COL00030_bit2 -COL00030_bit3 -COL00030_bit4 -COL00030_bit5 -COL00030_bit6 -COL00030_bit7 -COL00030_bit8 -COL00030_bit9 -COL00030_bit10 -COL00030_bit11 -COL00030_bit12 -COL00031_bit_7 -COL00031_bit_6 -COL00031_bit_5 COL00031_bit_4 -COL00031_bit_3 -COL00031_bit_2 -COL00031_bit_1 -COL00031_bit0 -COL00031_bit1 -COL00031_bit2 -COL00031_bit3 -COL00031_bit4 -COL00031_bit5 -COL00031_bit6 -COL00031_bit7 -COL00031_bit8 -COL00031_bit9 -COL00031_bit10 -COL00031_bit11 -COL00031_bit12 COL00032_bit_7 COL00032_bit_6 -COL00032_bit_5 -COL00032_bit_4 -COL00032_bit_3 COL00032_bit_2 -COL00032_bit_1 -COL00032_bit0 -COL00032_bit1 -COL00032_bit2 -COL00032_bit3 -COL00032_bit4 -COL00032_bit5 COL00032_bit6 -COL00032_bit7 -COL00032_bit8 -COL00032_bit9 -COL00032_bit10 -COL00032_bit11 -COL00032_bit12 -COL00033_bit_7 -COL00033_bit_6 -COL00033_bit_5 -COL00033_bit_4 -COL00033_bit_3 -COL00033_bit_2 -COL00033_bit_1 -COL00033_bit0 -COL00033_bit1 -COL00033_bit2 -COL00033_bit3 -COL00033_bit4 -COL00033_bit5 -COL00033_bit6 -COL00033_bit7 -COL00033_bit8 -COL00033_bit9 -COL00033_bit10 -COL00033_bit11 -COL00033_bit12 COL00034_bit_7 -COL00034_bit_6 -COL00034_bit_5 -COL00034_bit_4 -COL00034_bit_3 -COL00034_bit_2 -COL00034_bit_1 -COL00034_bit0 -COL00034_bit1 -COL00034_bit2 -COL00034_bit3 -COL00034_bit4 COL00034_bit5 -COL00034_bit6 -COL00034_bit7 -COL00034_bit8 -COL00034_bit9 -COL00034_bit10 -COL00034_bit11 -COL00034_bit12 COL00035_bit_7 -COL00035_bit_6 COL00035_bit_5 -COL00035_bit_4 COL00035_bit_3 -COL00035_bit_2 -COL00035_bit_1 -COL00035_bit0 -COL00035_bit1 -COL00035_bit2 -COL00035_bit3 -COL00035_bit4 -COL00035_bit5 -COL00035_bit6 -COL00035_bit7 -COL00035_bit8 -COL00035_bit9 -COL00035_bit10 -COL00035_bit11 -COL00035_bit12 -COL00036_bit_7 -COL00036_bit_6 -COL00036_bit_5 COL00036_bit_4 -COL00036_bit_3 -COL00036_bit_2 COL00036_bit_1 -COL00036_bit0 -COL00036_bit1 -COL00036_bit2 -COL00036_bit3 -COL00036_bit4 -COL00036_bit5 COL00036_bit6 -COL00036_bit7 -COL00036_bit8 -COL00036_bit9 -COL00036_bit10 -COL00036_bit11 -COL00036_bit12 -COL00037_bit_7 -COL00037_bit_6 -COL00037_bit_5 -COL00037_bit_4 -COL00037_bit_3 -COL00037_bit_2 -COL00037_bit_1 -COL00037_bit0 -COL00037_bit1 -COL00037_bit2 -COL00037_bit3 -COL00037_bit4 -COL00037_bit5 -COL00037_bit6 -COL00037_bit7 -COL00037_bit8 -COL00037_bit9 -COL00037_bit10 -COL00037_bit11 -COL00037_bit12 -COL00038_bit_7 -COL00038_bit_6 -COL00038_bit_5 -COL00038_bit_4 -COL00038_bit_3 -COL00038_bit_2 -COL00038_bit_1 -COL00038_bit0 -COL00038_bit1 -COL00038_bit2 -COL00038_bit3 -COL00038_bit4 -COL00038_bit5 -COL00038_bit6 -COL00038_bit7 -COL00038_bit8 -COL00038_bit9 -COL00038_bit10 -COL00038_bit11 -COL00038_bit12 COL00039_bit_7 COL00039_bit_6 -COL00039_bit_5 -COL00039_bit_4 COL00039_bit_3 COL00039_bit_2 -COL00039_bit_1 -COL00039_bit0 -COL00039_bit1 -COL00039_bit2 -COL00039_bit3 -COL00039_bit4 COL00039_bit5 -COL00039_bit6 -COL00039_bit7 -COL00039_bit8 -COL00039_bit9 -COL00039_bit10 -COL00039_bit11 -COL00039_bit12 -COL00040_bit_7 -COL00040_bit_6 -COL00040_bit_5 COL00040_bit_4 COL00040_bit_3 COL00040_bit_2 -COL00040_bit_1 -COL00040_bit0 -COL00040_bit1 -COL00040_bit2 -COL00040_bit3 -COL00040_bit4 -COL00040_bit5 COL00040_bi#### 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.71 0.86 0.87 2/54 3698
Raw data (stat): 3698 (runsolver) R 3697 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 484616145 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99981 s]
Raw data (loadavg): 0.76 0.86 0.87 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 1405 0 0 0 994 4 0 0 25 0 1 0 484616145 7548928 1379 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1843 1379 603 41 0 1802 0
vsize: 7372
[startup+19.9999 s]
Raw data (loadavg): 0.79 0.86 0.88 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 1868 0 0 0 1993 6 0 0 25 0 1 0 484616145 9428992 1842 4294967295 134512640 134672761 3221224544 3221223728 134559363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2302 1842 603 41 0 2261 0
vsize: 9208
[startup+30.0007 s]
Raw data (loadavg): 0.82 0.87 0.88 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 2208 0 0 0 2992 7 0 0 25 0 1 0 484616145 10760192 2182 4294967295 134512640 134672761 3221224544 3221222540 134566343 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2182 603 41 0 2586 0
vsize: 10508
[startup+40.0001 s]
Raw data (loadavg): 0.85 0.87 0.88 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 2212 0 0 0 3992 7 0 0 25 0 1 0 484616145 10760192 2186 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2186 603 41 0 2586 0
vsize: 10508
[startup+50.0012 s]
Raw data (loadavg): 0.87 0.88 0.88 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 2229 0 0 0 4992 7 0 0 25 0 1 0 484616145 10895360 2203 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2660 2203 603 41 0 2619 0
vsize: 10640
[startup+60.0011 s]
Raw data (loadavg): 0.89 0.88 0.88 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 2290 0 0 0 5991 8 0 0 25 0 1 0 484616145 11169792 2264 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2727 2264 603 41 0 2686 0
vsize: 10908
[startup+70.0004 s]
Raw data (loadavg): 0.91 0.88 0.88 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 2340 0 0 0 6991 8 0 0 25 0 1 0 484616145 11304960 2314 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2760 2314 603 41 0 2719 0
vsize: 11040
[startup+80.0016 s]
Raw data (loadavg): 0.92 0.89 0.88 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 2399 0 0 0 7991 9 0 0 25 0 1 0 484616145 11702272 2373 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2857 2373 603 41 0 2816 0
vsize: 11428
[startup+90.0013 s]
Raw data (loadavg): 0.93 0.89 0.88 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 2428 0 0 0 8991 9 0 0 25 0 1 0 484616145 11849728 2402 4294967295 134512640 134672761 3221224544 3221223728 134559028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2893 2402 603 41 0 2852 0
vsize: 11572
[startup+100.002 s]
Raw data (loadavg): 0.94 0.89 0.88 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 2434 0 0 0 9991 9 0 0 25 0 1 0 484616145 11849728 2408 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2893 2408 603 41 0 2852 0
vsize: 11572
[startup+110.002 s]
Raw data (loadavg): 0.95 0.90 0.88 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 2473 0 0 0 10990 10 0 0 25 0 1 0 484616145 11980800 2447 4294967295 134512640 134672761 3221224544 3221223720 134559723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2925 2447 603 41 0 2884 0
vsize: 11700
[startup+120.003 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 2485 0 0 0 11990 10 0 0 25 0 1 0 484616145 12115968 2459 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2958 2459 603 41 0 2917 0
vsize: 11832
[startup+130.003 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 2549 0 0 0 12990 11 0 0 25 0 1 0 484616145 12390400 2523 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3025 2523 603 41 0 2984 0
vsize: 12100
[startup+140.004 s]
Raw data (loadavg): 0.97 0.90 0.89 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 2593 0 0 0 13989 11 0 0 25 0 1 0 484616145 12521472 2567 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3057 2567 603 41 0 3016 0
vsize: 12228
[startup+150.005 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 2770 0 0 0 14989 12 0 0 25 0 1 0 484616145 13193216 2744 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3221 2744 603 41 0 3180 0
vsize: 12884
[startup+160.004 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 3037 0 0 0 15988 13 0 0 25 0 1 0 484616145 14401536 3011 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3516 3011 603 41 0 3475 0
vsize: 14064
[startup+170.005 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 3592 0 0 0 16985 16 0 0 25 0 1 0 484616145 16576512 3566 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4047 3566 603 41 0 4006 0
vsize: 16188
[startup+180.005 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 3592 0 0 0 17985 16 0 0 25 0 1 0 484616145 16576512 3566 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4047 3566 603 41 0 4006 0
vsize: 16188
[startup+190.005 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 3595 0 0 0 18985 17 0 0 25 0 1 0 484616145 16719872 3569 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4082 3569 603 41 0 4041 0
vsize: 16328
[startup+200.006 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 3595 0 0 0 19985 17 0 0 25 0 1 0 484616145 16719872 3569 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4082 3569 603 41 0 4041 0
vsize: 16328
[startup+210.006 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 3600 0 0 0 20985 17 0 0 25 0 1 0 484616145 16719872 3574 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4082 3574 603 41 0 4041 0
vsize: 16328
[startup+220.019 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 3601 0 0 0 21986 17 0 0 25 0 1 0 484616145 16719872 3575 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4082 3575 603 41 0 4041 0
vsize: 16328
[startup+230.022 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 3601 0 0 0 22986 17 0 0 25 0 1 0 484616145 16719872 3575 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4082 3575 603 41 0 4041 0
vsize: 16328
[startup+240.022 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 3601 0 0 0 23986 17 0 0 25 0 1 0 484616145 16719872 3575 4294967295 134512640 134672761 3221224544 3221223728 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4082 3575 603 41 0 4041 0
vsize: 16328
[startup+250.022 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 3656 0 0 0 24986 18 0 0 25 0 1 0 484616145 16855040 3630 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4115 3630 603 41 0 4074 0
vsize: 16460
[startup+260.023 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 3656 0 0 0 25986 18 0 0 25 0 1 0 484616145 16855040 3630 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4115 3630 603 41 0 4074 0
vsize: 16460
[startup+270.022 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 3939 0 0 0 26985 19 0 0 25 0 1 0 484616145 18075648 3913 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4413 3913 603 41 0 4372 0
vsize: 17652
[startup+280.022 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4446 0 0 0 27984 21 0 0 25 0 1 0 484616145 20127744 4420 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4914 4420 603 41 0 4873 0
vsize: 19656
[startup+290.023 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4485 0 0 0 28983 21 0 0 25 0 1 0 484616145 20262912 4459 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4459 603 41 0 4906 0
vsize: 19788
[startup+300.023 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4485 0 0 0 29983 22 0 0 25 0 1 0 484616145 20262912 4459 4294967295 134512640 134672761 3221224544 3221223728 134558700 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4459 603 41 0 4906 0
vsize: 19788
[startup+310.024 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4485 0 0 0 30983 22 0 0 25 0 1 0 484616145 20262912 4459 4294967295 134512640 134672761 3221224544 3221223728 134558890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4459 603 41 0 4906 0
vsize: 19788
[startup+320.024 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4485 0 0 0 31983 22 0 0 25 0 1 0 484616145 20262912 4459 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4459 603 41 0 4906 0
vsize: 19788
[startup+330.024 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4486 0 0 0 32983 23 0 0 25 0 1 0 484616145 20262912 4460 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4460 603 41 0 4906 0
vsize: 19788
[startup+340.024 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4486 0 0 0 33983 23 0 0 25 0 1 0 484616145 20262912 4460 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4460 603 41 0 4906 0
vsize: 19788
[startup+350.025 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4487 0 0 0 34982 23 0 0 25 0 1 0 484616145 20262912 4461 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4461 603 41 0 4906 0
vsize: 19788
[startup+360.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4487 0 0 0 35983 23 0 0 25 0 1 0 484616145 20262912 4461 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4461 603 41 0 4906 0
vsize: 19788
[startup+370.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4487 0 0 0 36983 23 0 0 25 0 1 0 484616145 20262912 4461 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4461 603 41 0 4906 0
vsize: 19788
[startup+380.026 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4487 0 0 0 37983 23 0 0 25 0 1 0 484616145 20262912 4461 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4461 603 41 0 4906 0
vsize: 19788
[startup+390.026 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4487 0 0 0 38982 24 0 0 25 0 1 0 484616145 20262912 4461 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4461 603 41 0 4906 0
vsize: 19788
[startup+400.027 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4487 0 0 0 39982 24 0 0 25 0 1 0 484616145 20262912 4461 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4461 603 41 0 4906 0
vsize: 19788
[startup+410.027 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4491 0 0 0 40982 25 0 0 25 0 1 0 484616145 20262912 4465 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4465 603 41 0 4906 0
vsize: 19788
[startup+420.027 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4491 0 0 0 41981 25 0 0 25 0 1 0 484616145 20262912 4465 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4465 603 41 0 4906 0
vsize: 19788
[startup+430.027 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4491 0 0 0 42981 26 0 0 25 0 1 0 484616145 20262912 4465 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4465 603 41 0 4906 0
vsize: 19788
[startup+440.028 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4491 0 0 0 43981 26 0 0 25 0 1 0 484616145 20262912 4465 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4465 603 41 0 4906 0
vsize: 19788
[startup+450.028 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4491 0 0 0 44981 26 0 0 25 0 1 0 484616145 20262912 4465 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4465 603 41 0 4906 0
vsize: 19788
[startup+460.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4491 0 0 0 45981 26 0 0 25 0 1 0 484616145 20262912 4465 4294967295 134512640 134672761 3221224544 3221223728 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4465 603 41 0 4906 0
vsize: 19788
[startup+470.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4491 0 0 0 46981 27 0 0 25 0 1 0 484616145 20262912 4465 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4465 603 41 0 4906 0
vsize: 19788
[startup+480.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4540 0 0 0 47980 27 0 0 25 0 1 0 484616145 20529152 4514 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5012 4514 603 41 0 4971 0
vsize: 20048
[startup+490.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4540 0 0 0 48980 27 0 0 25 0 1 0 484616145 20529152 4514 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5012 4514 603 41 0 4971 0
vsize: 20048
[startup+500.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4540 0 0 0 49981 27 0 0 25 0 1 0 484616145 20529152 4514 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5012 4514 603 41 0 4971 0
vsize: 20048
[startup+510.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4540 0 0 0 50980 28 0 0 25 0 1 0 484616145 20529152 4514 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5012 4514 603 41 0 4971 0
vsize: 20048
[startup+520.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4540 0 0 0 51980 28 0 0 25 0 1 0 484616145 20529152 4514 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5012 4514 603 41 0 4971 0
vsize: 20048
[startup+530.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4540 0 0 0 52980 28 0 0 25 0 1 0 484616145 20529152 4514 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5012 4514 603 41 0 4971 0
vsize: 20048
[startup+540.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4540 0 0 0 53980 29 0 0 25 0 1 0 484616145 20529152 4514 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5012 4514 603 41 0 4971 0
vsize: 20048
[startup+550.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4540 0 0 0 54980 29 0 0 25 0 1 0 484616145 20529152 4514 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5012 4514 603 41 0 4971 0
vsize: 20048
[startup+560.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4540 0 0 0 55980 29 0 0 25 0 1 0 484616145 20529152 4514 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5012 4514 603 41 0 4971 0
vsize: 20048
[startup+570.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4541 0 0 0 56979 29 0 0 25 0 1 0 484616145 20529152 4515 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5012 4515 603 41 0 4971 0
vsize: 20048
[startup+580.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4596 0 0 0 57979 30 0 0 25 0 1 0 484616145 20799488 4570 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5078 4570 603 41 0 5037 0
vsize: 20312
[startup+590.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4607 0 0 0 58979 30 0 0 25 0 1 0 484616145 20799488 4581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5078 4581 603 41 0 5037 0
vsize: 20312
[startup+600.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 4660 0 0 0 59979 30 0 0 25 0 1 0 484616145 21082112 4634 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5147 4634 603 41 0 5106 0
vsize: 20588
[startup+610.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5103 0 0 0 60978 31 0 0 25 0 1 0 484616145 22827008 5077 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5573 5077 603 41 0 5532 0
vsize: 22292
[startup+620.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5179 0 0 0 61978 31 0 0 25 0 1 0 484616145 23097344 5153 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5639 5153 603 41 0 5598 0
vsize: 22556
[startup+630.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5196 0 0 0 62979 31 0 0 25 0 1 0 484616145 23240704 5170 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5674 5170 603 41 0 5633 0
vsize: 22696
[startup+640.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5210 0 0 0 63981 31 0 0 25 0 1 0 484616145 23240704 5184 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5674 5184 603 41 0 5633 0
vsize: 22696
[startup+650.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5488 0 0 0 64981 32 0 0 25 0 1 0 484616145 24506368 5462 4294967295 134512640 134672761 3221224544 3221223648 134559841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5983 5462 603 41 0 5942 0
vsize: 23932
[startup+660.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5808 0 0 0 65981 33 0 0 25 0 1 0 484616145 25837568 5782 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6308 5782 603 41 0 6267 0
vsize: 25232
[startup+670.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5808 0 0 0 66980 33 0 0 25 0 1 0 484616145 25837568 5782 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6308 5782 603 41 0 6267 0
vsize: 25232
[startup+680.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5808 0 0 0 67980 34 0 0 25 0 1 0 484616145 25837568 5782 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6308 5782 603 41 0 6267 0
vsize: 25232
[startup+690.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5812 0 0 0 68981 34 0 0 25 0 1 0 484616145 25837568 5786 4294967295 134512640 134672761 3221224544 3221223728 134558925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6308 5786 603 41 0 6267 0
vsize: 25232
[startup+700.102 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5812 0 0 0 69981 34 0 0 25 0 1 0 484616145 25837568 5786 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6308 5786 603 41 0 6267 0
vsize: 25232
[startup+710.108 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5812 0 0 0 70981 35 0 0 25 0 1 0 484616145 25837568 5786 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6308 5786 603 41 0 6267 0
vsize: 25232
[startup+720.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5812 0 0 0 71981 35 0 0 25 0 1 0 484616145 25837568 5786 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6308 5786 603 41 0 6267 0
vsize: 25232
[startup+730.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5813 0 0 0 72981 36 0 0 25 0 1 0 484616145 25837568 5787 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6308 5787 603 41 0 6267 0
vsize: 25232
[startup+740.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5813 0 0 0 73981 36 0 0 25 0 1 0 484616145 25837568 5787 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6308 5787 603 41 0 6267 0
vsize: 25232
[startup+750.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5816 0 0 0 74981 36 0 0 25 0 1 0 484616145 25837568 5790 4294967295 134512640 134672761 3221224544 3221223648 134560424 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6308 5790 603 41 0 6267 0
vsize: 25232
[startup+760.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5816 0 0 0 75981 36 0 0 25 0 1 0 484616145 25837568 5790 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6308 5790 603 41 0 6267 0
vsize: 25232
[startup+770.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5816 0 0 0 76981 36 0 0 25 0 1 0 484616145 25837568 5790 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6308 5790 603 41 0 6267 0
vsize: 25232
[startup+780.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5817 0 0 0 77981 36 0 0 25 0 1 0 484616145 25837568 5791 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6308 5791 603 41 0 6267 0
vsize: 25232
[startup+790.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5817 0 0 0 78981 36 0 0 25 0 1 0 484616145 25837568 5791 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6308 5791 603 41 0 6267 0
vsize: 25232
[startup+800.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5817 0 0 0 79981 37 0 0 25 0 1 0 484616145 25837568 5791 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6308 5791 603 41 0 6267 0
vsize: 25232
[startup+810.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5817 0 0 0 80981 37 0 0 25 0 1 0 484616145 25837568 5791 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6308 5791 603 41 0 6267 0
vsize: 25232
[startup+820.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5817 0 0 0 81980 37 0 0 25 0 1 0 484616145 25837568 5791 4294967295 134512640 134672761 3221224544 3221223696 134565132 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6308 5791 603 41 0 6267 0
vsize: 25232
[startup+830.115 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5817 0 0 0 82981 37 0 0 25 0 1 0 484616145 25837568 5791 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6308 5791 603 41 0 6267 0
vsize: 25232
[startup+840.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5817 0 0 0 83981 37 0 0 25 0 1 0 484616145 25837568 5791 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6308 5791 603 41 0 6267 0
vsize: 25232
[startup+850.115 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5817 0 0 0 84981 37 0 0 25 0 1 0 484616145 25837568 5791 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6308 5791 603 41 0 6267 0
vsize: 25232
[startup+860.115 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5817 0 0 0 85981 37 0 0 25 0 1 0 484616145 25837568 5791 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6308 5791 603 41 0 6267 0
vsize: 25232
[startup+870.115 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5828 0 0 0 86981 37 0 0 25 0 1 0 484616145 25837568 5802 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6308 5802 603 41 0 6267 0
vsize: 25232
[startup+880.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5842 0 0 0 87981 37 0 0 25 0 1 0 484616145 25997312 5816 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6347 5816 603 41 0 6306 0
vsize: 25388
[startup+890.115 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5844 0 0 0 88982 37 0 0 25 0 1 0 484616145 25997312 5818 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6347 5818 603 41 0 6306 0
vsize: 25388
[startup+900.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5852 0 0 0 89982 37 0 0 25 0 1 0 484616145 25997312 5826 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6347 5826 603 41 0 6306 0
vsize: 25388
[startup+910.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5854 0 0 0 90982 37 0 0 25 0 1 0 484616145 25997312 5828 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6347 5828 603 41 0 6306 0
vsize: 25388
[startup+920.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5861 0 0 0 91982 37 0 0 25 0 1 0 484616145 25997312 5835 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6347 5835 603 41 0 6306 0
vsize: 25388
[startup+930.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5869 0 0 0 92982 37 0 0 25 0 1 0 484616145 25997312 5843 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6347 5843 603 41 0 6306 0
vsize: 25388
[startup+940.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5875 0 0 0 93983 37 0 0 25 0 1 0 484616145 26161152 5849 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6387 5849 603 41 0 6346 0
vsize: 25548
[startup+950.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5875 0 0 0 94984 37 0 0 25 0 1 0 484616145 26161152 5849 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6387 5849 603 41 0 6346 0
vsize: 25548
[startup+960.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5886 0 0 0 95984 37 0 0 25 0 1 0 484616145 26161152 5860 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6387 5860 603 41 0 6346 0
vsize: 25548
[startup+970.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5887 0 0 0 96984 37 0 0 25 0 1 0 484616145 26161152 5861 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6387 5861 603 41 0 6346 0
vsize: 25548
[startup+980.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5888 0 0 0 97984 37 0 0 25 0 1 0 484616145 26161152 5862 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6387 5862 603 41 0 6346 0
vsize: 25548
[startup+990.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5899 0 0 0 98985 37 0 0 25 0 1 0 484616145 26161152 5873 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6387 5873 603 41 0 6346 0
vsize: 25548
[startup+1000.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5899 0 0 0 99985 37 0 0 25 0 1 0 484616145 26161152 5873 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6387 5873 603 41 0 6346 0
vsize: 25548
[startup+1010.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5899 0 0 0 100986 37 0 0 25 0 1 0 484616145 26161152 5873 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6387 5873 603 41 0 6346 0
vsize: 25548
[startup+1020.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5899 0 0 0 101987 37 0 0 25 0 1 0 484616145 26161152 5873 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6387 5873 603 41 0 6346 0
vsize: 25548
[startup+1030.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5899 0 0 0 102988 37 0 0 25 0 1 0 484616145 26161152 5873 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6387 5873 603 41 0 6346 0
vsize: 25548
[startup+1040.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5900 0 0 0 103988 37 0 0 25 0 1 0 484616145 26161152 5874 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6387 5874 603 41 0 6346 0
vsize: 25548
[startup+1050.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5900 0 0 0 104988 37 0 0 25 0 1 0 484616145 26161152 5874 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6387 5874 603 41 0 6346 0
vsize: 25548
[startup+1060.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5900 0 0 0 105988 37 0 0 25 0 1 0 484616145 26161152 5874 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6387 5874 603 41 0 6346 0
vsize: 25548
[startup+1070.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5910 0 0 0 106988 37 0 0 25 0 1 0 484616145 26357760 5884 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5884 603 41 0 6394 0
vsize: 25740
[startup+1080.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5910 0 0 0 107989 37 0 0 25 0 1 0 484616145 26357760 5884 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5884 603 41 0 6394 0
vsize: 25740
[startup+1090.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5919 0 0 0 108990 37 0 0 25 0 1 0 484616145 26357760 5893 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5893 603 41 0 6394 0
vsize: 25740
[startup+1100.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5919 0 0 0 109990 37 0 0 25 0 1 0 484616145 26357760 5893 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5893 603 41 0 6394 0
vsize: 25740
[startup+1110.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5919 0 0 0 110990 37 0 0 25 0 1 0 484616145 26357760 5893 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5893 603 41 0 6394 0
vsize: 25740
[startup+1120.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5919 0 0 0 111990 37 0 0 25 0 1 0 484616145 26357760 5893 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5893 603 41 0 6394 0
vsize: 25740
[startup+1130.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5919 0 0 0 112991 37 0 0 25 0 1 0 484616145 26357760 5893 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5893 603 41 0 6394 0
vsize: 25740
[startup+1140.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5919 0 0 0 113991 37 0 0 25 0 1 0 484616145 26357760 5893 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5893 603 41 0 6394 0
vsize: 25740
[startup+1150.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5919 0 0 0 114990 38 0 0 25 0 1 0 484616145 26357760 5893 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5893 603 41 0 6394 0
vsize: 25740
[startup+1160.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5923 0 0 0 115990 38 0 0 25 0 1 0 484616145 26357760 5897 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5897 603 41 0 6394 0
vsize: 25740
[startup+1170.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5923 0 0 0 116991 38 0 0 25 0 1 0 484616145 26357760 5897 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5897 603 41 0 6394 0
vsize: 25740
[startup+1180.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5923 0 0 0 117991 38 0 0 25 0 1 0 484616145 26357760 5897 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5897 603 41 0 6394 0
vsize: 25740
[startup+1190.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5923 0 0 0 118991 38 0 0 25 0 1 0 484616145 26357760 5897 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5897 603 41 0 6394 0
vsize: 25740
[startup+1200.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3698
Raw data (stat): 3698 (minisat+) R 3697 30854 30853 0 -1 0 5923 0 0 0 119991 38 0 0 25 0 1 0 484616145 26357760 5897 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5897 603 41 0 6394 0
vsize: 25740
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 3698
Raw data (stat): 3698 (minisat+) Z 3697 30854 30853 0 -1 12 5926 0 0 0 119991 39 0 0 25 0 1 0 484616145 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.19
CPU time (s): 1200.32
CPU user time (s): 1199.92
CPU system time (s): 0.395939
CPU usage (%): 100.01
Max. virtual memory (Kb): 25740
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####