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-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-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	1176.54
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 21193

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-21 23:03:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13647 boxname=wulflinc13 idbench=1050 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ef7064a9be2b712276f7b600af28e2b0  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-mod010.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-mod010.opb /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-mod010.opb
IDLAUNCH: 13647
/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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        627048 kB
Buffers:         17712 kB
Cached:         368408 kB
SwapCached:        392 kB
Active:         161460 kB
Inactive:       226784 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        626796 kB
SwapTotal:     2097136 kB
SwapFree:      2095968 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5748 kB
Slab:            13740 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 23:23:38 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 13647 7 1200.25 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.69 0.91 0.89 2/54 30747
Raw data (stat): 30747 (runsolver) R 30746 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490675331 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.9996 s]
Raw data (loadavg): 0.74 0.91 0.89 2/54 30747
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 2947 0 0 0 992 6 0 0 25 0 1 0 490675331 14479360 2853 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3535 2853 603 41 0 3494 0
vsize: 14140
[startup+19.9997 s]
Raw data (loadavg): 0.78 0.91 0.89 2/54 30747
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 2991 0 0 0 1992 7 0 0 25 0 1 0 490675331 14614528 2897 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3568 2897 603 41 0 3527 0
vsize: 14272
[startup+30.0004 s]
Raw data (loadavg): 0.81 0.91 0.89 2/54 30747
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 3024 0 0 0 2991 7 0 0 25 0 1 0 490675331 14749696 2930 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3601 2930 603 41 0 3560 0
vsize: 14404
[startup+39.9996 s]
Raw data (loadavg): 0.84 0.92 0.89 2/54 30747
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 3046 0 0 0 3991 8 0 0 25 0 1 0 490675331 14880768 2952 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3633 2952 603 41 0 3592 0
vsize: 14532
[startup+50.0009 s]
Raw data (loadavg): 0.86 0.92 0.89 2/54 30747
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 3060 0 0 0 4991 8 0 0 25 0 1 0 490675331 14880768 2966 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3633 2966 603 41 0 3592 0
vsize: 14532
[startup+60.0013 s]
Raw data (loadavg): 0.88 0.92 0.90 2/54 30747
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 3073 0 0 0 5991 8 0 0 25 0 1 0 490675331 14880768 2979 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3633 2979 603 41 0 3592 0
vsize: 14532
[startup+70.0016 s]
Raw data (loadavg): 0.90 0.92 0.90 2/54 30747
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 3086 0 0 0 6990 9 0 0 25 0 1 0 490675331 15015936 2992 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3666 2992 603 41 0 3625 0
vsize: 14664
[startup+80.0028 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 30747
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 3123 0 0 0 7990 9 0 0 25 0 1 0 490675331 15147008 3029 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3698 3029 603 41 0 3657 0
vsize: 14792
[startup+90.0033 s]
Raw data (loadavg): 0.93 0.93 0.90 2/54 30747
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 3159 0 0 0 8990 10 0 0 25 0 1 0 490675331 15282176 3065 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3731 3065 603 41 0 3690 0
vsize: 14924
[startup+100.004 s]
Raw data (loadavg): 0.94 0.93 0.90 2/54 30747
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 3299 0 0 0 9989 10 0 0 25 0 1 0 490675331 15818752 3205 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3862 3205 603 41 0 3821 0
vsize: 15448
[startup+110.005 s]
Raw data (loadavg): 0.95 0.93 0.90 2/54 30747
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 3465 0 0 0 10988 11 0 0 25 0 1 0 490675331 16560128 3371 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4043 3371 603 41 0 4002 0
vsize: 16172
[startup+120.005 s]
Raw data (loadavg): 0.95 0.93 0.90 2/54 30747
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 3590 0 0 0 11988 12 0 0 25 0 1 0 490675331 17096704 3496 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4174 3496 603 41 0 4133 0
vsize: 16696
[startup+130.006 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 30747
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 3836 0 0 0 12986 14 0 0 25 0 1 0 490675331 18042880 3742 4294967295 134512640 134672761 3221224544 3221223728 134559324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4405 3742 603 41 0 4364 0
vsize: 17620
[startup+140.006 s]
Raw data (loadavg): 0.97 0.94 0.90 2/54 30747
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 4089 0 0 0 13985 15 0 0 25 0 1 0 490675331 19120128 3995 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4668 3995 603 41 0 4627 0
vsize: 18672
[startup+150.007 s]
Raw data (loadavg): 0.97 0.94 0.90 2/54 30747
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 4333 0 0 0 14984 16 0 0 25 0 1 0 490675331 20185088 4239 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4928 4239 603 41 0 4887 0
vsize: 19712
[startup+160.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 30747
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 4619 0 0 0 15983 18 0 0 25 0 1 0 490675331 21397504 4525 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5224 4525 603 41 0 5183 0
vsize: 20896
[startup+170.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 4854 0 0 0 16982 18 0 0 25 0 1 0 490675331 22343680 4760 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5455 4760 603 41 0 5414 0
vsize: 21820
[startup+180.009 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 5082 0 0 0 17981 20 0 0 25 0 1 0 490675331 23277568 4988 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5683 4988 603 41 0 5642 0
vsize: 22732
[startup+190.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 5236 0 0 0 18980 21 0 0 25 0 1 0 490675331 23814144 5142 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5814 5142 603 41 0 5773 0
vsize: 23256
[startup+200.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 5399 0 0 0 19980 21 0 0 25 0 1 0 490675331 24477696 5305 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5976 5305 603 41 0 5935 0
vsize: 23904
[startup+210.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 5596 0 0 0 20980 22 0 0 25 0 1 0 490675331 25288704 5502 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6174 5502 603 41 0 6133 0
vsize: 24696
[startup+220.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 5748 0 0 0 21979 23 0 0 25 0 1 0 490675331 25964544 5654 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6339 5654 603 41 0 6298 0
vsize: 25356
[startup+230.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 5929 0 0 0 22979 23 0 0 25 0 1 0 490675331 26636288 5835 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6503 5835 603 41 0 6462 0
vsize: 26012
[startup+240.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 6137 0 0 0 23978 24 0 0 25 0 1 0 490675331 27443200 6043 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6700 6043 603 41 0 6659 0
vsize: 26800
[startup+250.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 6308 0 0 0 24977 25 0 0 25 0 1 0 490675331 28250112 6214 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6897 6214 603 41 0 6856 0
vsize: 27588
[startup+260.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 6529 0 0 0 25976 26 0 0 25 0 1 0 490675331 29052928 6435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7093 6435 603 41 0 7052 0
vsize: 28372
[startup+270.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 6719 0 0 0 26974 28 0 0 25 0 1 0 490675331 29859840 6625 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7290 6625 603 41 0 7249 0
vsize: 29160
[startup+280.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 6952 0 0 0 27974 28 0 0 25 0 1 0 490675331 31059968 6858 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7583 6858 603 41 0 7542 0
vsize: 30332
[startup+290.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 7117 0 0 0 28974 29 0 0 25 0 1 0 490675331 31727616 7023 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7746 7023 603 41 0 7705 0
vsize: 30984
[startup+300.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 7273 0 0 0 29973 30 0 0 25 0 1 0 490675331 32387072 7179 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7907 7179 603 41 0 7866 0
vsize: 31628
[startup+310.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 7389 0 0 0 30972 30 0 0 25 0 1 0 490675331 32792576 7295 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8006 7295 603 41 0 7965 0
vsize: 32024
[startup+320.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 7582 0 0 0 31972 31 0 0 25 0 1 0 490675331 33611776 7488 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8206 7488 603 41 0 8165 0
vsize: 32824
[startup+330.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 7758 0 0 0 32971 32 0 0 25 0 1 0 490675331 34295808 7664 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8373 7664 603 41 0 8332 0
vsize: 33492
[startup+340.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 7866 0 0 0 33971 32 0 0 25 0 1 0 490675331 34836480 7772 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8505 7772 603 41 0 8464 0
vsize: 34020
[startup+350.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 7984 0 0 0 34971 32 0 0 25 0 1 0 490675331 35241984 7890 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8604 7890 603 41 0 8563 0
vsize: 34416
[startup+360.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 8156 0 0 0 35970 33 0 0 25 0 1 0 490675331 35913728 8062 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8768 8062 603 41 0 8727 0
vsize: 35072
[startup+370.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 8379 0 0 0 36969 34 0 0 25 0 1 0 490675331 36843520 8285 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8995 8285 603 41 0 8954 0
vsize: 35980
[startup+380.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 8573 0 0 0 37969 35 0 0 25 0 1 0 490675331 37658624 8479 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9194 8479 603 41 0 9153 0
vsize: 36776
[startup+390.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 8844 0 0 0 38968 35 0 0 25 0 1 0 490675331 38723584 8750 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9454 8750 603 41 0 9413 0
vsize: 37816
[startup+400.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 9061 0 0 0 39968 36 0 0 25 0 1 0 490675331 39661568 8967 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9683 8967 603 41 0 9642 0
vsize: 38732
[startup+410.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 9211 0 0 0 40968 36 0 0 25 0 1 0 490675331 40198144 9117 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9814 9117 603 41 0 9773 0
vsize: 39256
[startup+420.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 9372 0 0 0 41968 37 0 0 25 0 1 0 490675331 40869888 9278 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9978 9278 603 41 0 9937 0
vsize: 39912
[startup+430.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 9513 0 0 0 42967 38 0 0 25 0 1 0 490675331 41537536 9419 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10141 9419 603 41 0 10100 0
vsize: 40564
[startup+440.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 9689 0 0 0 43967 38 0 0 25 0 1 0 490675331 42205184 9595 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10304 9595 603 41 0 10263 0
vsize: 41216
[startup+450.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 9890 0 0 0 44967 38 0 0 25 0 1 0 490675331 43016192 9796 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10502 9796 603 41 0 10461 0
vsize: 42008
[startup+460.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 10023 0 0 0 45966 39 0 0 25 0 1 0 490675331 43540480 9929 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10630 9929 603 41 0 10589 0
vsize: 42520
[startup+470.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 10152 0 0 0 46966 39 0 0 25 0 1 0 490675331 44093440 10058 4294967295 134512640 134672761 3221224544 3221223648 134555105 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10765 10058 603 41 0 10724 0
vsize: 43060
[startup+480.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 10301 0 0 0 47966 40 0 0 25 0 1 0 490675331 44634112 10207 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 10482 0 0 0 48965 40 0 0 25 0 1 0 490675331 45428736 10388 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11091 10388 603 41 0 11050 0
vsize: 44364
[startup+500.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 10611 0 0 0 49965 41 0 0 25 0 1 0 490675331 45965312 10517 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11222 10517 603 41 0 11181 0
vsize: 44888
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 10772 0 0 0 50965 42 0 0 25 0 1 0 490675331 46645248 10678 4294967295 134512640 134672761 3221224544 3221223716 134556667 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.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 10912 0 0 0 51965 42 0 0 25 0 1 0 490675331 47177728 10818 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11518 10818 603 41 0 11477 0
vsize: 46072
[startup+530.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 11049 0 0 0 52964 42 0 0 25 0 1 0 490675331 47710208 10955 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10955 603 41 0 11607 0
vsize: 46592
[startup+540.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 11203 0 0 0 53964 43 0 0 25 0 1 0 490675331 48394240 11109 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11815 11109 603 41 0 11774 0
vsize: 47260
[startup+550.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 11323 0 0 0 54964 43 0 0 25 0 1 0 490675331 48930816 11229 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11946 11229 603 41 0 11905 0
vsize: 47784
[startup+560.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 11451 0 0 0 55964 44 0 0 25 0 1 0 490675331 49467392 11357 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12077 11357 603 41 0 12036 0
vsize: 48308
[startup+570.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 11587 0 0 0 56963 44 0 0 25 0 1 0 490675331 49999872 11493 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12207 11493 603 41 0 12166 0
vsize: 48828
[startup+580.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 11736 0 0 0 57963 45 0 0 25 0 1 0 490675331 50536448 11642 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12338 11642 603 41 0 12297 0
vsize: 49352
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 11909 0 0 0 58963 45 0 0 25 0 1 0 490675331 51347456 11815 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12536 11815 603 41 0 12495 0
vsize: 50144
[startup+600.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 12062 0 0 0 59962 46 0 0 25 0 1 0 490675331 51884032 11968 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12667 11968 603 41 0 12626 0
vsize: 50668
[startup+610.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 12213 0 0 0 60962 47 0 0 25 0 1 0 490675331 52563968 12119 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12833 12119 603 41 0 12792 0
vsize: 51332
[startup+620.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 12343 0 0 0 61961 47 0 0 25 0 1 0 490675331 53100544 12249 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12964 12249 603 41 0 12923 0
vsize: 51856
[startup+630.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 12452 0 0 0 62960 48 0 0 25 0 1 0 490675331 53514240 12358 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13065 12358 603 41 0 13024 0
vsize: 52260
[startup+640.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 12565 0 0 0 63960 48 0 0 25 0 1 0 490675331 53915648 12471 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13163 12471 603 41 0 13122 0
vsize: 52652
[startup+650.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 12682 0 0 0 64960 49 0 0 25 0 1 0 490675331 54484992 12588 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13302 12588 603 41 0 13261 0
vsize: 53208
[startup+660.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 12815 0 0 0 65959 49 0 0 25 0 1 0 490675331 55021568 12721 4294967295 134512640 134672761 3221224544 3221223680 134560579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13433 12721 603 41 0 13392 0
vsize: 53732
[startup+670.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 12985 0 0 0 66959 50 0 0 25 0 1 0 490675331 55693312 12891 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13597 12891 603 41 0 13556 0
vsize: 54388
[startup+680.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 13129 0 0 0 67959 50 0 0 25 0 1 0 490675331 56881152 13035 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13887 13035 603 41 0 13846 0
vsize: 55548
[startup+690.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 13212 0 0 0 68959 50 0 0 25 0 1 0 490675331 57147392 13118 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13952 13118 603 41 0 13911 0
vsize: 55808
[startup+700.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 13318 0 0 0 69959 51 0 0 25 0 1 0 490675331 57544704 13224 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14049 13224 603 41 0 14008 0
vsize: 56196
[startup+710.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 13449 0 0 0 70958 51 0 0 25 0 1 0 490675331 58077184 13355 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14179 13355 603 41 0 14138 0
vsize: 56716
[startup+720.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 13580 0 0 0 71958 52 0 0 25 0 1 0 490675331 58613760 13486 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14310 13486 603 41 0 14269 0
vsize: 57240
[startup+730.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 13695 0 0 0 72957 53 0 0 25 0 1 0 490675331 59162624 13601 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14444 13601 603 41 0 14403 0
vsize: 57776
[startup+740.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 13817 0 0 0 73957 53 0 0 25 0 1 0 490675331 59572224 13723 4294967295 134512640 134672761 3221224544 3221223732 134556676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14544 13723 603 41 0 14503 0
vsize: 58176
[startup+750.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 13952 0 0 0 74957 53 0 0 25 0 1 0 490675331 60137472 13858 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14682 13858 603 41 0 14641 0
vsize: 58728
[startup+760.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 14081 0 0 0 75957 54 0 0 25 0 1 0 490675331 60674048 13987 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14813 13987 603 41 0 14772 0
vsize: 59252
[startup+770.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 14187 0 0 0 76957 54 0 0 25 0 1 0 490675331 61210624 14093 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14944 14093 603 41 0 14903 0
vsize: 59776
[startup+780.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 14290 0 0 0 77957 54 0 0 25 0 1 0 490675331 61612032 14196 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15042 14196 603 41 0 15001 0
vsize: 60168
[startup+790.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 14404 0 0 0 78956 55 0 0 25 0 1 0 490675331 62038016 14310 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15146 14310 603 41 0 15105 0
vsize: 60584
[startup+800.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 14525 0 0 0 79956 56 0 0 25 0 1 0 490675331 62574592 14431 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15277 14431 603 41 0 15236 0
vsize: 61108
[startup+810.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 14653 0 0 0 80956 56 0 0 25 0 1 0 490675331 63115264 14559 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15409 14559 603 41 0 15368 0
vsize: 61636
[startup+820.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 14757 0 0 0 81955 57 0 0 25 0 1 0 490675331 63512576 14663 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15506 14663 603 41 0 15465 0
vsize: 62024
[startup+830.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 14878 0 0 0 82955 57 0 0 25 0 1 0 490675331 64040960 14784 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15635 14784 603 41 0 15594 0
vsize: 62540
[startup+840.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 15017 0 0 0 83955 57 0 0 25 0 1 0 490675331 64581632 14923 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15767 14923 603 41 0 15726 0
vsize: 63068
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 15163 0 0 0 84954 58 0 0 25 0 1 0 490675331 65118208 15069 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15898 15069 603 41 0 15857 0
vsize: 63592
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 15294 0 0 0 85954 59 0 0 25 0 1 0 490675331 65703936 15200 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16041 15200 603 41 0 16000 0
vsize: 64164
[startup+870.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 15414 0 0 0 86954 59 0 0 25 0 1 0 490675331 66154496 15320 4294967295 134512640 134672761 3221224544 3221223728 134558851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16151 15320 603 41 0 16110 0
vsize: 64604
[startup+880.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 15536 0 0 0 87954 59 0 0 25 0 1 0 490675331 66682880 15442 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16280 15442 603 41 0 16239 0
vsize: 65120
[startup+890.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 15678 0 0 0 88953 60 0 0 25 0 1 0 490675331 67371008 15584 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16448 15584 603 41 0 16407 0
vsize: 65792
[startup+900.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 15778 0 0 0 89953 60 0 0 25 0 1 0 490675331 67792896 15684 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16551 15684 603 41 0 16510 0
vsize: 66204
[startup+910.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 15861 0 0 0 90953 60 0 0 25 0 1 0 490675331 68059136 15767 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16616 15767 603 41 0 16575 0
vsize: 66464
[startup+920.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 15956 0 0 0 91953 61 0 0 25 0 1 0 490675331 68456448 15862 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16713 15862 603 41 0 16672 0
vsize: 66852
[startup+930.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 16048 0 0 0 92953 62 0 0 25 0 1 0 490675331 68890624 15954 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16819 15954 603 41 0 16778 0
vsize: 67276
[startup+940.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 16143 0 0 0 93953 62 0 0 25 0 1 0 490675331 69160960 16049 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16885 16049 603 41 0 16844 0
vsize: 67540
[startup+950.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 16242 0 0 0 94952 62 0 0 25 0 1 0 490675331 69697536 16148 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17016 16148 603 41 0 16975 0
vsize: 68064
[startup+960.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 16336 0 0 0 95952 63 0 0 25 0 1 0 490675331 70107136 16242 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17116 16242 603 41 0 17075 0
vsize: 68464
[startup+970.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 16442 0 0 0 96952 63 0 0 25 0 1 0 490675331 70512640 16348 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17215 16348 603 41 0 17174 0
vsize: 68860
[startup+980.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 16550 0 0 0 97952 63 0 0 25 0 1 0 490675331 70918144 16456 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17314 16456 603 41 0 17273 0
vsize: 69256
[startup+990.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 16658 0 0 0 98952 64 0 0 25 0 1 0 490675331 71319552 16564 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17412 16564 603 41 0 17371 0
vsize: 69648
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 16748 0 0 0 99952 64 0 0 25 0 1 0 490675331 71720960 16654 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17510 16654 603 41 0 17469 0
vsize: 70040
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 16842 0 0 0 100952 64 0 0 25 0 1 0 490675331 72122368 16748 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17608 16748 603 41 0 17567 0
vsize: 70432
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 16957 0 0 0 101952 64 0 0 25 0 1 0 490675331 72523776 16863 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17706 16863 603 41 0 17665 0
vsize: 70824
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 17077 0 0 0 102952 65 0 0 25 0 1 0 490675331 73060352 16983 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17837 16983 603 41 0 17796 0
vsize: 71348
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 17166 0 0 0 103951 65 0 0 25 0 1 0 490675331 73474048 17072 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17938 17072 603 41 0 17897 0
vsize: 71752
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 17276 0 0 0 104952 65 0 0 25 0 1 0 490675331 73875456 17182 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18036 17182 603 41 0 17995 0
vsize: 72144
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 17352 0 0 0 105952 65 0 0 25 0 1 0 490675331 74153984 17258 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18104 17258 603 41 0 18063 0
vsize: 72416
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 17441 0 0 0 106952 65 0 0 25 0 1 0 490675331 74555392 17347 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18202 17347 603 41 0 18161 0
vsize: 72808
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 17521 0 0 0 107952 66 0 0 25 0 1 0 490675331 74956800 17427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18300 17427 603 41 0 18259 0
vsize: 73200
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 17617 0 0 0 108951 66 0 0 25 0 1 0 490675331 75350016 17523 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18396 17523 603 41 0 18355 0
vsize: 73584
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 17728 0 0 0 109951 67 0 0 25 0 1 0 490675331 75755520 17634 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18495 17634 603 41 0 18454 0
vsize: 73980
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 17833 0 0 0 110951 67 0 0 25 0 1 0 490675331 76152832 17739 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18592 17739 603 41 0 18551 0
vsize: 74368
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 17942 0 0 0 111951 67 0 0 25 0 1 0 490675331 76681216 17848 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18721 17848 603 41 0 18680 0
vsize: 74884
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 18057 0 0 0 112951 67 0 0 25 0 1 0 490675331 77258752 17963 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18862 17963 603 41 0 18821 0
vsize: 75448
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 18150 0 0 0 113951 67 0 0 25 0 1 0 490675331 77549568 18056 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18933 18056 603 41 0 18892 0
vsize: 75732
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 18265 0 0 0 114951 68 0 0 25 0 1 0 490675331 78077952 18171 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19062 18171 603 41 0 19021 0
vsize: 76248
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 18380 0 0 0 115952 68 0 0 25 0 1 0 490675331 78479360 18286 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19160 18286 603 41 0 19119 0
vsize: 76640
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 18468 0 0 0 116952 68 0 0 25 0 1 0 490675331 78884864 18374 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19259 18374 603 41 0 19218 0
vsize: 77036
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 18579 0 0 0 117952 68 0 0 25 0 1 0 490675331 79286272 18485 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19357 18485 603 41 0 19316 0
vsize: 77428
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 18662 0 0 0 118952 68 0 0 25 0 1 0 490675331 79687680 18568 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19455 18568 603 41 0 19414 0
vsize: 77820
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30749
Raw data (stat): 30747 (minisat+) R 30746 30701 30700 0 -1 0 18747 0 0 0 119952 69 0 0 25 0 1 0 490675331 79953920 18653 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19520 18653 603 41 0 19479 0
vsize: 78080
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 30749
Raw data (stat): 30747 (minisat+) Z 30746 30701 30700 0 -1 12 18749 0 0 0 119952 72 0 0 25 0 1 0 490675331 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.08
CPU time (s): 1200.25
CPU user time (s): 1199.52
CPU system time (s): 0.727889
CPU usage (%): 100.014
Max. virtual memory (Kb): 78080
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####