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/miplib3/normalized-mps-v2-13-7-mod010.opb
MD5SUM	ef7064a9be2b712276f7b600af28e2b0
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	6571
Optimality of the best value was proved	NO
Number of terms in the objective function	2655
Biggest coefficient in the objective function	266
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	489211
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	266
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	489211
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.18
Number of variables	2655
Total number of constraints	2801
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	2800
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	2655
Trace number 18067

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-21 13:19:00 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18639 boxname=wulflinc4 idbench=1434 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ef7064a9be2b712276f7b600af28e2b0  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-mod010.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-mod010.opb /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-mod010.opb
IDLAUNCH: 18639
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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.169
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:        225608 kB
Buffers:         27036 kB
Cached:         758704 kB
SwapCached:          0 kB
Active:          54784 kB
Inactive:       733752 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        225356 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            14828 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 13:39:02 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 18639 7 1200.21 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 291 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 289]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[ 287]---> Adder-cost: 108   maxlim: 57   bits: 6/6
c ---[ 285]---> Adder-cost: 176   maxlim: 91   bits: 7/7
c ---[ 283]---> Adder-cost: 108   maxlim: 58   bits: 6/6
c ---[ 281]---> Adder-cost: 68   maxlim: 35   bits: 6/6
c ---[ 279]---> Adder-cost: 126   maxlim: 63   bits: 7/6
c ---[ 277]---> Adder-cost: 148   maxlim: 78   bits: 7/7
c ---[ 275]---> Adder-cost: 82   maxlim: 44   bits: 6/6
c ---[ 273]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[ 271]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[ 269]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[ 267]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 265]---> Adder-cost: 164   maxlim: 86   bits: 7/7
c ---[ 263]---> Adder-cost: 102   maxlim: 56   bits: 6/6
c ---[ 261]---> Adder-cost: 146   maxlim: 75   bits: 7/7
c ---[ 259]---> Adder-cost: 190   maxlim: 98   bits: 7/7
c ---[ 257]---> Adder-cost: 128   maxlim: 66   bits: 7/7
c ---[ 255]---> Adder-cost: 114   maxlim: 62   bits: 6/6
c ---[ 253]---> Adder-cost: 160   maxlim: 84   bits: 7/7
c ---[ 251]---> Adder-cost: 94   maxlim: 51   bits: 6/6
c ---[ 249]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[ 247]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 245]---> Adder-cost: 132   maxlim: 68   bits: 7/7
c ---[ 243]---> Adder-cost: 52   maxlim: 30   bits: 5/5
c ---[ 241]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[ 239]---> Adder-cost: 52   maxlim: 30   bits: 5/5
c ---[ 237]---> Adder-cost: 132   maxlim: 67   bits: 7/7
c ---[ 235]---> Adder-cost: 94   maxlim: 50   bits: 6/6
c ---[ 233]---> Adder-cost: 172   maxlim: 90   bits: 7/7
c ---[ 231]---> Adder-cost: 78   maxlim: 56   bits: 6/6
c ---[ 229]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 227]---> Adder-cost: 84   maxlim: 45   bits: 6/6
c ---[ 225]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[ 223]---> Adder-cost: 106   maxlim: 59   bits: 6/6
c ---[ 221]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 219]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[ 217]---> Adder-cost: 304   maxlim: 156   bits: 8/8
c ---[ 215]---> Adder-cost: 256   maxlim: 130   bits: 8/8
c ---[ 213]---> Adder-cost: 152   maxlim: 85   bits: 7/7
c ---[ 211]---> Adder-cost: 128   maxlim: 66   bits: 7/7
c ---[ 209]---> Adder-cost: 148   maxlim: 78   bits: 7/7
c ---[ 207]---> Adder-cost: 84   maxlim: 45   bits: 6/6
c ---[ 205]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[ 203]---> Adder-cost: 162   maxlim: 83   bits: 7/7
c ---[ 201]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[ 199]---> Adder-cost: 96   maxlim: 70   bits: 7/7
c ---[ 197]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[ 195]---> Adder-cost: 170   maxlim: 88   bits: 7/7
c ---[ 193]---> Adder-cost: 220   maxlim: 118   bits: 7/7
c ---[ 191]---> Adder-cost: 178   maxlim: 94   bits: 7/7
c ---[ 189]---> Adder-cost: 124   maxlim: 66   bits: 7/7
c ---[ 187]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 185]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 183]---> Adder-cost: 84   maxlim: 46   bits: 6/6
c ---[ 181]---> Adder-cost: 62   maxlim: 39   bits: 6/6
c ---[ 179]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[ 177]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 175]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 173]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[ 171]---> Adder-cost: 128   maxlim: 66   bits: 7/7
c ---[ 169]---> Adder-cost: 144   maxlim: 78   bits: 7/7
c ---[ 167]---> Adder-cost: 170   maxlim: 89   bits: 7/7
c ---[ 165]---> Adder-cost: 140   maxlim: 72   bits: 7/7
c ---[ 163]---> Adder-cost: 86   maxlim: 47   bits: 6/6
c ---[ 161]---> Adder-cost: 76   maxlim: 40   bits: 6/6
c ---[ 159]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 157]---> Adder-cost: 68   maxlim: 36   bits: 6/6
c ---[ 155]---> Adder-cost: 126   maxlim: 64   bits: 7/7
c ---[ 153]---> Adder-cost: 124   maxlim: 64   bits: 7/7
c ---[ 151]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[ 149]---> Adder-cost: 78   maxlim: 42   bits: 6/6
c ---[ 147]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[ 145]---> Adder-cost: 62   maxlim: 32   bits: 6/6
c ---[ 143]---> Adder-cost: 114   maxlim: 61   bits: 6/6
c ---[ 141]---> Adder-cost: 148   maxlim: 78   bits: 7/7
c ---[ 139]---> Adder-cost: 82   maxlim: 44   bits: 6/6
c ---[ 137]---> Adder-cost: 84   maxlim: 46   bits: 6/6
c ---[ 135]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[ 133]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[ 131]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 129]---> Adder-cost: 82   maxlim: 46   bits: 6/6
c ---[ 127]---> Adder-cost: 68   maxlim: 35   bits: 6/6
c ---[ 125]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 123]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[ 121]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 119]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 117]---> Adder-cost: 112   maxlim: 59   bits: 6/6
c ---[ 115]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[ 113]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 111]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[ 109]---> Adder-cost: 134   maxlim: 69   bits: 7/7
c ---[ 107]---> Adder-cost: 126   maxlim: 63   bits: 7/6
c ---[ 105]---> Adder-cost: 76   maxlim: 40   bits: 6/6
c ---[ 103]---> Adder-cost: 128   maxlim: 67   bits: 7/7
c ---[ 101]---> Adder-cost: 146   maxlim: 78   bits: 7/7
c ---[  99]---> Adder-cost: 134   maxlim: 70   bits: 7/7
c ---[  97]---> Adder-cost: 126   maxlim: 63   bits: 7/6
c ---[  95]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  93]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  91]---> Adder-cost: 156   maxlim: 79   bits: 7/7
c ---[  89]---> Adder-cost: 106   maxlim: 64   bits: 7/7
c ---[  87]---> Adder-cost: 162   maxlim: 100   bits: 7/7
c ---[  85]---> Adder-cost: 108   maxlim: 63   bits: 7/6
c ---[  83]---> Adder-cost: 96   maxlim: 54   bits: 6/6
c ---[  81]---> Adder-cost: 164   maxlim: 85   bits: 7/7
c ---[  79]---> Adder-cost: 108   maxlim: 58   bits: 6/6
c ---[  77]---> Adder-cost: 98   maxlim: 52   bits: 6/6
c ---[  75]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[  73]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  71]---> Adder-cost: 146   maxlim: 76   bits: 7/7
c ---[  69]---> Adder-cost: 194   maxlim: 100   bits: 7/7
c ---[  67]---> Adder-cost: 104   maxlim: 55   bits: 6/6
c ---[  65]---> Adder-cost: 110   maxlim: 66   bits: 7/7
c ---[  63]---> Adder-cost: 108   maxlim: 57   bits: 6/6
c ---[  61]---> Adder-cost: 168   maxlim: 87   bits: 7/7
c ---[  59]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[  57]---> Adder-cost: 170   maxlim: 87   bits: 7/7
c ---[  55]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[  53]---> Adder-cost: 68   maxlim: 36   bits: 6/6
c ---[  51]---> Adder-cost: 176   maxlim: 91   bits: 7/7
c ---[  49]---> Adder-cost: 228   maxlim: 121   bits: 7/7
c ---[  47]---> Adder-cost: 184   maxlim: 101   bits: 7/7
c ---[  45]---> Adder-cost: 170   maxlim: 87   bits: 7/7
c ---[  43]---> Adder-cost: 144   maxlim: 75   bits: 7/7
c ---[  41]---> Adder-cost: 156   maxlim: 79   bits: 7/7
c ---[  39]---> Adder-cost: 194   maxlim: 101   bits: 7/7
c ---[  37]---> Adder-cost: 112   maxlim: 65   bits: 7/7
c ---[  35]---> Adder-cost: 108   maxlim: 59   bits: 6/6
c ---[  33]---> Adder-cost: 172   maxlim: 89   bits: 7/7
c ---[  31]---> Adder-cost: 114   maxlim: 62   bits: 6/6
c ---[  29]---> Adder-cost: 128   maxlim: 66   bits: 7/7
c ---[  27]---> Adder-cost: 108   maxlim: 58   bits: 6/6
c ---[  25]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[  23]---> Adder-cost: 110   maxlim: 62   bits: 6/6
c ---[  21]---> Adder-cost: 48   maxlim: 28   bits: 5/5
c ---[  19]---> Adder-cost: 6   maxlim: 5   bits: 3/3
c ---[  17]---> Adder-cost: 94   maxlim: 50   bits: 6/6
c ---[  15]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  13]---> Adder-cost: 102   maxlim: 55   bits: 6/6
c ---[  11]---> Adder-cost: 148   maxlim: 77   bits: 7/7
c ---[   9]---> Adder-cost: 196   maxlim: 101   bits: 7/7
c ---[   7]---> Adder-cost: 132   maxlim: 67   bits: 7/7
c ---[   5]---> Adder-cost: 112   maxlim: 61   bits: 6/6
c ---[   3]---> Adder-cost: 160   maxlim: 86   bits: 7/7
c ---[   1]---> Adder-cost: 4164   maxlim: 2609   bits: 12/12
c ---[   0]---> Adder-cost: 628   maxlim: 1878   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  135245   481373 |   45081       0        0     nan |  0.000 % |
c |       100 |  134710   479515 |   49589      41      130     3.2 |  8.697 % |
c |       250 |  134286   478049 |   54548     141      489     3.5 |  8.996 % |
c |       475 |  133805   476372 |   60002     318     1127     3.5 |  9.346 % |
c |       814 |  132611   472274 |   66003     533     1991     3.7 | 10.215 % |
c |      1321 |  131478   468367 |   72603     911     3659     4.0 | 11.038 % |
c |      2080 |  130529   465100 |   79863    1566     6842     4.4 | 11.729 % |
c |      3221 |  129464   461360 |   87850    2571    16232     6.3 | 12.501 % |
c |      4931 |  128426   457722 |   96635    4154    37027     8.9 | 13.239 % |
c |      7493 |  124186   442796 |  106298    6185    61156     9.9 | 16.225 % |
c |     11338 |  116978   417826 |  116928    9028   102347    11.3 | 21.362 % |
c |     17104 |  111462   398706 |  128621   14009   215233    15.4 | 25.306 % |
c |     25753 |  107163   383929 |  141483   22037   503013    22.8 | 28.229 % |
c |     38727 |  104694   375438 |  155631   34673  1221496    35.2 | 29.970 % |
c |     58189 |  101363   363903 |  171195   53405  2404991    45.0 | 32.366 % |
c |     87383 |   97736   351344 |  188314   81777  4401068    53.8 | 34.905 % |
c |    131180 |   95077   342229 |  207145  124498  8009656    64.3 | 36.778 % |
c |    196865 |   91603   330179 |  227860  189032 13502626    71.4 | 39.262 % |
#### 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.95 0.98 0.92 2/54 8760
Raw data (stat): 8760 (runsolver) R 8759 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487158602 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+10.0012 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 2947 0 0 0 992 7 0 0 25 0 1 0 487158602 14479360 2853 4294967295 134512640 134672761 3221224544 3221223736 134556677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3535 2853 603 41 0 3494 0
vsize: 14140
[startup+20.0014 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 2991 0 0 0 1991 7 0 0 25 0 1 0 487158602 14614528 2897 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3568 2897 603 41 0 3527 0
vsize: 14272
[startup+30.0023 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 3024 0 0 0 2991 7 0 0 25 0 1 0 487158602 14749696 2930 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3601 2930 603 41 0 3560 0
vsize: 14404
[startup+40.0023 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 3046 0 0 0 3990 8 0 0 25 0 1 0 487158602 14880768 2952 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3633 2952 603 41 0 3592 0
vsize: 14532
[startup+50.0028 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 3060 0 0 0 4991 8 0 0 25 0 1 0 487158602 14880768 2966 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3633 2966 603 41 0 3592 0
vsize: 14532
[startup+60.0026 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 3075 0 0 0 5991 8 0 0 25 0 1 0 487158602 14880768 2981 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3633 2981 603 41 0 3592 0
vsize: 14532
[startup+70.003 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 3086 0 0 0 6991 8 0 0 25 0 1 0 487158602 15015936 2992 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3666 2992 603 41 0 3625 0
vsize: 14664
[startup+80.0032 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 3123 0 0 0 7990 8 0 0 25 0 1 0 487158602 15147008 3029 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3698 3029 603 41 0 3657 0
vsize: 14792
[startup+90.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 3167 0 0 0 8990 9 0 0 25 0 1 0 487158602 15282176 3073 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3731 3073 603 41 0 3690 0
vsize: 14924
[startup+100.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 3305 0 0 0 9990 9 0 0 25 0 1 0 487158602 15818752 3211 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3862 3211 603 41 0 3821 0
vsize: 15448
[startup+110.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 3478 0 0 0 10990 10 0 0 25 0 1 0 487158602 16560128 3384 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4043 3384 603 41 0 4002 0
vsize: 16172
[startup+120.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 3610 0 0 0 11989 10 0 0 25 0 1 0 487158602 17096704 3516 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4174 3516 603 41 0 4133 0
vsize: 16696
[startup+130.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 3848 0 0 0 12988 11 0 0 25 0 1 0 487158602 18178048 3754 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4438 3754 603 41 0 4397 0
vsize: 17752
[startup+140.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 4109 0 0 0 13988 12 0 0 25 0 1 0 487158602 19120128 4015 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4668 4015 603 41 0 4627 0
vsize: 18672
[startup+150.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 4349 0 0 0 14987 13 0 0 25 0 1 0 487158602 20320256 4255 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4961 4255 603 41 0 4920 0
vsize: 19844
[startup+160.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 4660 0 0 0 15986 14 0 0 25 0 1 0 487158602 21532672 4566 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5257 4566 603 41 0 5216 0
vsize: 21028
[startup+170.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 4877 0 0 0 16986 14 0 0 25 0 1 0 487158602 22343680 4783 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5455 4783 603 41 0 5414 0
vsize: 21820
[startup+180.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 5090 0 0 0 17985 15 0 0 25 0 1 0 487158602 23277568 4996 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5683 4996 603 41 0 5642 0
vsize: 22732
[startup+190.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 5242 0 0 0 18985 15 0 0 25 0 1 0 487158602 23945216 5148 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5846 5148 603 41 0 5805 0
vsize: 23384
[startup+200.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 5416 0 0 0 19984 16 0 0 25 0 1 0 487158602 24612864 5322 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6009 5322 603 41 0 5968 0
vsize: 24036
[startup+210.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 5615 0 0 0 20984 17 0 0 25 0 1 0 487158602 25423872 5521 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6207 5521 603 41 0 6166 0
vsize: 24828
[startup+220.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 5760 0 0 0 21983 18 0 0 25 0 1 0 487158602 25964544 5666 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6339 5666 603 41 0 6298 0
vsize: 25356
[startup+230.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 5948 0 0 0 22983 18 0 0 25 0 1 0 487158602 26771456 5854 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6536 5854 603 41 0 6495 0
vsize: 26144
[startup+240.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 6167 0 0 0 23983 19 0 0 25 0 1 0 487158602 27574272 6073 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6732 6073 603 41 0 6691 0
vsize: 26928
[startup+250.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 6339 0 0 0 24983 19 0 0 25 0 1 0 487158602 28250112 6245 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6897 6245 603 41 0 6856 0
vsize: 27588
[startup+260.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 6552 0 0 0 25982 19 0 0 25 0 1 0 487158602 29184000 6458 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7125 6458 603 41 0 7084 0
vsize: 28500
[startup+270.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 6747 0 0 0 26982 20 0 0 25 0 1 0 487158602 29995008 6653 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7323 6653 603 41 0 7282 0
vsize: 29292
[startup+280.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 6968 0 0 0 27981 20 0 0 25 0 1 0 487158602 31195136 6874 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7616 6874 603 41 0 7575 0
vsize: 30464
[startup+290.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 7135 0 0 0 28981 21 0 0 25 0 1 0 487158602 31858688 7041 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7778 7041 603 41 0 7737 0
vsize: 31112
[startup+300.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 7286 0 0 0 29981 21 0 0 25 0 1 0 487158602 32387072 7192 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7907 7192 603 41 0 7866 0
vsize: 31628
[startup+310.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 7406 0 0 0 30981 21 0 0 25 0 1 0 487158602 32927744 7312 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8039 7312 603 41 0 7998 0
vsize: 32156
[startup+320.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 7603 0 0 0 31980 22 0 0 25 0 1 0 487158602 33746944 7509 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8239 7509 603 41 0 8198 0
vsize: 32956
[startup+330.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 7768 0 0 0 32980 23 0 0 25 0 1 0 487158602 34430976 7674 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8406 7674 603 41 0 8365 0
vsize: 33624
[startup+340.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 7878 0 0 0 33980 23 0 0 25 0 1 0 487158602 34836480 7784 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8505 7784 603 41 0 8464 0
vsize: 34020
[startup+350.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 8009 0 0 0 34979 24 0 0 25 0 1 0 487158602 35373056 7915 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8636 7915 603 41 0 8595 0
vsize: 34544
[startup+360.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 8172 0 0 0 35979 24 0 0 25 0 1 0 487158602 36048896 8078 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8801 8078 603 41 0 8760 0
vsize: 35204
[startup+370.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 8396 0 0 0 36979 24 0 0 25 0 1 0 487158602 36978688 8302 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9028 8302 603 41 0 8987 0
vsize: 36112
[startup+380.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 8590 0 0 0 37978 25 0 0 25 0 1 0 487158602 37658624 8496 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9194 8496 603 41 0 9153 0
vsize: 36776
[startup+390.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 8875 0 0 0 38977 26 0 0 25 0 1 0 487158602 38854656 8781 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9486 8781 603 41 0 9445 0
vsize: 37944
[startup+400.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 9072 0 0 0 39977 27 0 0 25 0 1 0 487158602 39661568 8978 4294967295 134512640 134672761 3221224544 3221223648 134560474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9683 8978 603 41 0 9642 0
vsize: 38732
[startup+410.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 9224 0 0 0 40977 27 0 0 25 0 1 0 487158602 40329216 9130 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9130 603 41 0 9805 0
vsize: 39384
[startup+420.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 9380 0 0 0 41976 28 0 0 25 0 1 0 487158602 40869888 9286 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9978 9286 603 41 0 9937 0
vsize: 39912
[startup+430.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 9521 0 0 0 42976 28 0 0 25 0 1 0 487158602 41537536 9427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10141 9427 603 41 0 10100 0
vsize: 40564
[startup+440.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 9696 0 0 0 43976 28 0 0 25 0 1 0 487158602 42205184 9602 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10304 9602 603 41 0 10263 0
vsize: 41216
[startup+450.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 9893 0 0 0 44975 29 0 0 25 0 1 0 487158602 43016192 9799 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10502 9799 603 41 0 10461 0
vsize: 42008
[startup+460.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 10027 0 0 0 45975 29 0 0 25 0 1 0 487158602 43540480 9933 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10630 9933 603 41 0 10589 0
vsize: 42520
[startup+470.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 10154 0 0 0 46975 29 0 0 25 0 1 0 487158602 44093440 10060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10765 10060 603 41 0 10724 0
vsize: 43060
[startup+480.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 10301 0 0 0 47975 30 0 0 25 0 1 0 487158602 44634112 10207 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10897 10207 603 41 0 10856 0
vsize: 43588
[startup+490.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 10480 0 0 0 48974 31 0 0 25 0 1 0 487158602 45428736 10386 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11091 10386 603 41 0 11050 0
vsize: 44364
[startup+500.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 10609 0 0 0 49974 31 0 0 25 0 1 0 487158602 45965312 10515 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11222 10515 603 41 0 11181 0
vsize: 44888
[startup+510.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 10772 0 0 0 50973 32 0 0 25 0 1 0 487158602 46645248 10678 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11388 10678 603 41 0 11347 0
vsize: 45552
[startup+520.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 10908 0 0 0 51973 32 0 0 25 0 1 0 487158602 47177728 10814 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11518 10814 603 41 0 11477 0
vsize: 46072
[startup+530.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 11046 0 0 0 52973 33 0 0 25 0 1 0 487158602 47710208 10952 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10952 603 41 0 11607 0
vsize: 46592
[startup+540.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 11197 0 0 0 53972 33 0 0 25 0 1 0 487158602 48394240 11103 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11815 11103 603 41 0 11774 0
vsize: 47260
[startup+550.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 11315 0 0 0 54972 34 0 0 25 0 1 0 487158602 48795648 11221 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11913 11221 603 41 0 11872 0
vsize: 47652
[startup+560.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 11437 0 0 0 55972 34 0 0 25 0 1 0 487158602 49332224 11343 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12044 11343 603 41 0 12003 0
vsize: 48176
[startup+570.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 11576 0 0 0 56971 35 0 0 25 0 1 0 487158602 49868800 11482 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12175 11482 603 41 0 12134 0
vsize: 48700
[startup+580.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 11727 0 0 0 57971 36 0 0 25 0 1 0 487158602 50536448 11633 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12338 11633 603 41 0 12297 0
vsize: 49352
[startup+590.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 11899 0 0 0 58970 36 0 0 25 0 1 0 487158602 51212288 11805 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12503 11805 603 41 0 12462 0
vsize: 50012
[startup+600.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 12043 0 0 0 59970 37 0 0 25 0 1 0 487158602 51884032 11949 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12667 11949 603 41 0 12626 0
vsize: 50668
[startup+610.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 12196 0 0 0 60969 38 0 0 25 0 1 0 487158602 52432896 12102 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12801 12102 603 41 0 12760 0
vsize: 51204
[startup+620.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 12334 0 0 0 61969 38 0 0 25 0 1 0 487158602 53100544 12240 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12964 12240 603 41 0 12923 0
vsize: 51856
[startup+630.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 12447 0 0 0 62968 39 0 0 25 0 1 0 487158602 53514240 12353 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13065 12353 603 41 0 13024 0
vsize: 52260
[startup+640.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 12549 0 0 0 63967 39 0 0 25 0 1 0 487158602 53915648 12455 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13163 12455 603 41 0 13122 0
vsize: 52652
[startup+650.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 12668 0 0 0 64967 39 0 0 25 0 1 0 487158602 54484992 12574 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13302 12574 603 41 0 13261 0
vsize: 53208
[startup+660.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 12790 0 0 0 65967 40 0 0 25 0 1 0 487158602 54886400 12696 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13400 12696 603 41 0 13359 0
vsize: 53600
[startup+670.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 12963 0 0 0 66966 40 0 0 25 0 1 0 487158602 55693312 12869 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13597 12869 603 41 0 13556 0
vsize: 54388
[startup+680.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 13107 0 0 0 67966 41 0 0 25 0 1 0 487158602 56750080 13013 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13855 13013 603 41 0 13814 0
vsize: 55420
[startup+690.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 13209 0 0 0 68966 41 0 0 25 0 1 0 487158602 57147392 13115 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13952 13115 603 41 0 13911 0
vsize: 55808
[startup+700.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 13290 0 0 0 69966 41 0 0 25 0 1 0 487158602 57544704 13196 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14049 13196 603 41 0 14008 0
vsize: 56196
[startup+710.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 13430 0 0 0 70966 41 0 0 25 0 1 0 487158602 58077184 13336 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14179 13336 603 41 0 14138 0
vsize: 56716
[startup+720.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 13558 0 0 0 71966 41 0 0 25 0 1 0 487158602 58613760 13464 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14310 13464 603 41 0 14269 0
vsize: 57240
[startup+730.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 13659 0 0 0 72966 42 0 0 25 0 1 0 487158602 59031552 13565 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14412 13565 603 41 0 14371 0
vsize: 57648
[startup+740.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 13783 0 0 0 73966 42 0 0 25 0 1 0 487158602 59428864 13689 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14509 13689 603 41 0 14468 0
vsize: 58036
[startup+750.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 13923 0 0 0 74966 42 0 0 25 0 1 0 487158602 60002304 13829 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14649 13829 603 41 0 14608 0
vsize: 58596
[startup+760.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 14051 0 0 0 75966 42 0 0 25 0 1 0 487158602 60542976 13957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14781 13957 603 41 0 14740 0
vsize: 59124
[startup+770.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 14168 0 0 0 76965 43 0 0 25 0 1 0 487158602 61079552 14074 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14912 14074 603 41 0 14871 0
vsize: 59648
[startup+780.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 14270 0 0 0 77965 44 0 0 25 0 1 0 487158602 61476864 14176 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15009 14176 603 41 0 14968 0
vsize: 60036
[startup+790.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 14391 0 0 0 78964 45 0 0 25 0 1 0 487158602 62038016 14297 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15146 14297 603 41 0 15105 0
vsize: 60584
[startup+800.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 14488 0 0 0 79964 45 0 0 25 0 1 0 487158602 62439424 14394 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15244 14394 603 41 0 15203 0
vsize: 60976
[startup+810.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 14619 0 0 0 80964 45 0 0 25 0 1 0 487158602 62980096 14525 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15376 14525 603 41 0 15335 0
vsize: 61504
[startup+820.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 14718 0 0 0 81964 46 0 0 25 0 1 0 487158602 63381504 14624 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15474 14624 603 41 0 15433 0
vsize: 61896
[startup+830.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 14835 0 0 0 82963 46 0 0 25 0 1 0 487158602 63774720 14741 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15570 14741 603 41 0 15529 0
vsize: 62280
[startup+840.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 14987 0 0 0 83963 47 0 0 25 0 1 0 487158602 64446464 14893 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15734 14893 603 41 0 15693 0
vsize: 62936
[startup+850.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 15135 0 0 0 84963 47 0 0 25 0 1 0 487158602 64983040 15041 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15865 15041 603 41 0 15824 0
vsize: 63460
[startup+860.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 15257 0 0 0 85963 48 0 0 25 0 1 0 487158602 65568768 15163 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16008 15163 603 41 0 15967 0
vsize: 64032
[startup+870.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 15356 0 0 0 86962 48 0 0 25 0 1 0 487158602 66019328 15262 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16118 15262 603 41 0 16077 0
vsize: 64472
[startup+880.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 15496 0 0 0 87962 49 0 0 25 0 1 0 487158602 66551808 15402 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16248 15402 603 41 0 16207 0
vsize: 64992
[startup+890.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 15633 0 0 0 88962 49 0 0 25 0 1 0 487158602 67084288 15539 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16378 15539 603 41 0 16337 0
vsize: 65512
[startup+900.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 15738 0 0 0 89962 49 0 0 25 0 1 0 487158602 67506176 15644 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16481 15644 603 41 0 16440 0
vsize: 65924
[startup+910.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 15834 0 0 0 90962 49 0 0 25 0 1 0 487158602 67928064 15740 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16584 15740 603 41 0 16543 0
vsize: 66336
[startup+920.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 15908 0 0 0 91962 49 0 0 25 0 1 0 487158602 68190208 15814 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16648 15814 603 41 0 16607 0
vsize: 66592
[startup+930.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 16018 0 0 0 92962 49 0 0 25 0 1 0 487158602 68726784 15924 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16779 15924 603 41 0 16738 0
vsize: 67116
[startup+940.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 16094 0 0 0 93962 49 0 0 25 0 1 0 487158602 69021696 16000 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16851 16000 603 41 0 16810 0
vsize: 67404
[startup+950.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 16181 0 0 0 94962 50 0 0 25 0 1 0 487158602 69427200 16087 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16950 16087 603 41 0 16909 0
vsize: 67800
[startup+960.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 16304 0 0 0 95962 50 0 0 25 0 1 0 487158602 69840896 16210 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17051 16210 603 41 0 17010 0
vsize: 68204
[startup+970.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 16404 0 0 0 96962 51 0 0 25 0 1 0 487158602 70242304 16310 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17149 16310 603 41 0 17108 0
vsize: 68596
[startup+980.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 16499 0 0 0 97962 51 0 0 25 0 1 0 487158602 70647808 16405 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17248 16405 603 41 0 17207 0
vsize: 68992
[startup+990.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 16624 0 0 0 98962 51 0 0 25 0 1 0 487158602 71184384 16530 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17379 16530 603 41 0 17338 0
vsize: 69516
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 16716 0 0 0 99962 51 0 0 25 0 1 0 487158602 71589888 16622 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17478 16622 603 41 0 17437 0
vsize: 69912
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 16789 0 0 0 100962 51 0 0 25 0 1 0 487158602 71852032 16695 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17542 16695 603 41 0 17501 0
vsize: 70168
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 16908 0 0 0 101961 52 0 0 25 0 1 0 487158602 72388608 16814 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17673 16814 603 41 0 17632 0
vsize: 70692
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 17014 0 0 0 102961 52 0 0 25 0 1 0 487158602 72790016 16920 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17771 16920 603 41 0 17730 0
vsize: 71084
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 17115 0 0 0 103961 53 0 0 25 0 1 0 487158602 73207808 17021 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17873 17021 603 41 0 17832 0
vsize: 71492
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 17194 0 0 0 104961 53 0 0 25 0 1 0 487158602 73609216 17100 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17971 17100 603 41 0 17930 0
vsize: 71884
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 17314 0 0 0 105961 53 0 0 25 0 1 0 487158602 74018816 17220 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18071 17220 603 41 0 18030 0
vsize: 72284
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 17380 0 0 0 106961 54 0 0 25 0 1 0 487158602 74289152 17286 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18137 17286 603 41 0 18096 0
vsize: 72548
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 17479 0 0 0 107960 54 0 0 25 0 1 0 487158602 74821632 17385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18267 17385 603 41 0 18226 0
vsize: 73068
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 17552 0 0 0 108960 54 0 0 25 0 1 0 487158602 75087872 17458 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18332 17458 603 41 0 18291 0
vsize: 73328
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 17662 0 0 0 109960 55 0 0 25 0 1 0 487158602 75485184 17568 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18429 17568 603 41 0 18388 0
vsize: 73716
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 17776 0 0 0 110960 55 0 0 25 0 1 0 487158602 76021760 17682 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18560 17682 603 41 0 18519 0
vsize: 74240
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 17866 0 0 0 111959 55 0 0 25 0 1 0 487158602 76414976 17772 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18656 17772 603 41 0 18615 0
vsize: 74624
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 17991 0 0 0 112959 56 0 0 25 0 1 0 487158602 76812288 17897 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18753 17897 603 41 0 18712 0
vsize: 75012
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 18085 0 0 0 113959 56 0 0 25 0 1 0 487158602 77258752 17991 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18862 17991 603 41 0 18821 0
vsize: 75448
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 18189 0 0 0 114959 56 0 0 25 0 1 0 487158602 77680640 18095 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18965 18095 603 41 0 18924 0
vsize: 75860
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 18302 0 0 0 115959 57 0 0 25 0 1 0 487158602 78209024 18208 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19094 18208 603 41 0 19053 0
vsize: 76376
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 18415 0 0 0 116959 57 0 0 25 0 1 0 487158602 78614528 18321 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19193 18321 603 41 0 19152 0
vsize: 76772
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 18496 0 0 0 117959 57 0 0 25 0 1 0 487158602 79020032 18402 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19292 18402 603 41 0 19251 0
vsize: 77168
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 18608 0 0 0 118959 58 0 0 25 0 1 0 487158602 79421440 18514 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19390 18514 603 41 0 19349 0
vsize: 77560
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 8760
Raw data (stat): 8760 (minisat+) R 8759 5897 5896 0 -1 0 18684 0 0 0 119958 59 0 0 25 0 1 0 487158602 79822848 18590 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19488 18590 603 41 0 19447 0
vsize: 77952
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.98 0.92 1/54 8760
Raw data (stat): 8760 (minisat+) Z 8759 5897 5896 0 -1 12 18686 0 0 0 119958 62 0 0 25 0 1 0 487158602 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.06
CPU time (s): 1200.21
CPU user time (s): 1199.58
CPU system time (s): 0.627904
CPU usage (%): 100.012
Max. virtual memory (Kb): 77952
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####