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/miplib/normalized-mps-v2-20-10-mod010.opb
MD5SUM	4f0cac14ed3568050c2c57bb69fdb664
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.14
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 22143

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-22 02:18:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12048 boxname=wulflinc1 idbench=927 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4f0cac14ed3568050c2c57bb69fdb664  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-mod010.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-mod010.opb /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-mod010.opb
IDLAUNCH: 12048
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        506400 kB
Buffers:          4988 kB
Cached:         498552 kB
SwapCached:          0 kB
Active:          89144 kB
Inactive:       417580 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        506148 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7172 kB
Slab:            15792 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 02:38:55 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 12048 7 1200.22 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.92 0.95 0.93 2/56 8451
Raw data (stat): 8451 (runsolver) R 8450 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 434988000 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.96 0.93 2/56 8451
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 2947 0 0 0 992 6 0 0 25 0 1 0 434988000 14479360 2853 4294967295 134512640 134672761 3221224544 3221223712 134560806 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.0001 s]
Raw data (loadavg): 0.94 0.96 0.93 2/56 8451
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 2991 0 0 0 1992 6 0 0 25 0 1 0 434988000 14614528 2897 4294967295 134512640 134672761 3221224544 3221223668 134566037 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.0014 s]
Raw data (loadavg): 0.95 0.96 0.93 2/56 8451
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 3026 0 0 0 2992 7 0 0 25 0 1 0 434988000 14749696 2932 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3601 2932 603 41 0 3560 0
vsize: 14404
[startup+40.0016 s]
Raw data (loadavg): 0.96 0.96 0.93 2/56 8451
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 3047 0 0 0 3992 7 0 0 25 0 1 0 434988000 14880768 2953 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3633 2953 603 41 0 3592 0
vsize: 14532
[startup+50.0024 s]
Raw data (loadavg): 0.96 0.96 0.93 2/56 8451
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 3060 0 0 0 4992 7 0 0 25 0 1 0 434988000 14880768 2966 4294967295 134512640 134672761 3221224544 3221223680 134560640 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.0022 s]
Raw data (loadavg): 0.97 0.96 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 3075 0 0 0 5992 7 0 0 25 0 1 0 434988000 14880768 2981 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3633 2981 603 41 0 3592 0
vsize: 14532
[startup+70.0019 s]
Raw data (loadavg): 0.97 0.96 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 3086 0 0 0 6992 7 0 0 25 0 1 0 434988000 15015936 2992 4294967295 134512640 134672761 3221224544 3221223728 134556589 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.0027 s]
Raw data (loadavg): 0.98 0.96 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 3123 0 0 0 7992 7 0 0 25 0 1 0 434988000 15147008 3029 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.0028 s]
Raw data (loadavg): 0.98 0.96 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 3169 0 0 0 8992 7 0 0 25 0 1 0 434988000 15282176 3075 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3731 3075 603 41 0 3690 0
vsize: 14924
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 3306 0 0 0 9992 8 0 0 25 0 1 0 434988000 15818752 3212 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3862 3212 603 41 0 3821 0
vsize: 15448
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 3478 0 0 0 10992 8 0 0 25 0 1 0 434988000 16560128 3384 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4043 3384 603 41 0 4002 0
vsize: 16172
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 3610 0 0 0 11991 9 0 0 25 0 1 0 434988000 17096704 3516 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4174 3516 603 41 0 4133 0
vsize: 16696
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 3850 0 0 0 12991 9 0 0 25 0 1 0 434988000 18178048 3756 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4438 3756 603 41 0 4397 0
vsize: 17752
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 4119 0 0 0 13990 10 0 0 25 0 1 0 434988000 19251200 4025 4294967295 134512640 134672761 3221224544 3221223648 134560231 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4700 4025 603 41 0 4659 0
vsize: 18800
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 4353 0 0 0 14990 11 0 0 25 0 1 0 434988000 20320256 4259 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4961 4259 603 41 0 4920 0
vsize: 19844
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 4675 0 0 0 15989 12 0 0 25 0 1 0 434988000 21532672 4581 4294967295 134512640 134672761 3221224544 3221223712 134564738 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5257 4581 603 41 0 5216 0
vsize: 21028
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 4882 0 0 0 16988 12 0 0 25 0 1 0 434988000 22474752 4788 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5487 4788 603 41 0 5446 0
vsize: 21948
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 5104 0 0 0 17987 13 0 0 25 0 1 0 434988000 23277568 5010 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5683 5010 603 41 0 5642 0
vsize: 22732
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 5257 0 0 0 18987 14 0 0 25 0 1 0 434988000 23945216 5163 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5846 5163 603 41 0 5805 0
vsize: 23384
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 5426 0 0 0 19986 15 0 0 25 0 1 0 434988000 24612864 5332 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6009 5332 603 41 0 5968 0
vsize: 24036
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 5627 0 0 0 20986 15 0 0 25 0 1 0 434988000 25423872 5533 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6207 5533 603 41 0 6166 0
vsize: 24828
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 5770 0 0 0 21985 16 0 0 25 0 1 0 434988000 25964544 5676 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6339 5676 603 41 0 6298 0
vsize: 25356
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 5967 0 0 0 22985 17 0 0 25 0 1 0 434988000 26771456 5873 4294967295 134512640 134672761 3221224544 3221223648 134560474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6536 5873 603 41 0 6495 0
vsize: 26144
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 6180 0 0 0 23984 17 0 0 25 0 1 0 434988000 27705344 6086 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6764 6086 603 41 0 6723 0
vsize: 27056
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 6353 0 0 0 24984 18 0 0 25 0 1 0 434988000 28385280 6259 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6930 6259 603 41 0 6889 0
vsize: 27720
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 6572 0 0 0 25983 19 0 0 25 0 1 0 434988000 29319168 6478 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7158 6478 603 41 0 7117 0
vsize: 28632
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 6767 0 0 0 26982 20 0 0 25 0 1 0 434988000 29995008 6673 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7323 6673 603 41 0 7282 0
vsize: 29292
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 6983 0 0 0 27982 20 0 0 25 0 1 0 434988000 31195136 6889 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7616 6889 603 41 0 7575 0
vsize: 30464
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 7152 0 0 0 28981 21 0 0 25 0 1 0 434988000 31858688 7058 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7778 7058 603 41 0 7737 0
vsize: 31112
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 7312 0 0 0 29981 21 0 0 25 0 1 0 434988000 32522240 7218 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7940 7218 603 41 0 7899 0
vsize: 31760
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 7428 0 0 0 30981 21 0 0 25 0 1 0 434988000 33067008 7334 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8073 7334 603 41 0 8032 0
vsize: 32292
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 7633 0 0 0 31980 22 0 0 25 0 1 0 434988000 33882112 7539 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8272 7539 603 41 0 8231 0
vsize: 33088
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 7794 0 0 0 32980 22 0 0 25 0 1 0 434988000 34430976 7700 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8406 7700 603 41 0 8365 0
vsize: 33624
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 7897 0 0 0 33980 23 0 0 25 0 1 0 434988000 34836480 7803 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8505 7803 603 41 0 8464 0
vsize: 34020
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8453
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 8028 0 0 0 34979 23 0 0 25 0 1 0 434988000 35373056 7934 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8636 7934 603 41 0 8595 0
vsize: 34544
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 8194 0 0 0 35979 24 0 0 25 0 1 0 434988000 36048896 8100 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8801 8100 603 41 0 8760 0
vsize: 35204
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 8437 0 0 0 36978 25 0 0 25 0 1 0 434988000 37113856 8343 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9061 8343 603 41 0 9020 0
vsize: 36244
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 8618 0 0 0 37977 26 0 0 25 0 1 0 434988000 37793792 8524 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9227 8524 603 41 0 9186 0
vsize: 36908
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 8958 0 0 0 38976 27 0 0 25 0 1 0 434988000 39251968 8864 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9583 8864 603 41 0 9542 0
vsize: 38332
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 9103 0 0 0 39976 28 0 0 25 0 1 0 434988000 39796736 9009 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9716 9009 603 41 0 9675 0
vsize: 38864
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 9263 0 0 0 40975 28 0 0 25 0 1 0 434988000 40464384 9169 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9879 9169 603 41 0 9838 0
vsize: 39516
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 9428 0 0 0 41975 29 0 0 25 0 1 0 434988000 41136128 9334 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10043 9334 603 41 0 10002 0
vsize: 40172
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 9570 0 0 0 42974 30 0 0 25 0 1 0 434988000 41668608 9476 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10173 9476 603 41 0 10132 0
vsize: 40692
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 9758 0 0 0 43974 30 0 0 25 0 1 0 434988000 42475520 9664 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10370 9664 603 41 0 10329 0
vsize: 41480
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 9920 0 0 0 44973 31 0 0 25 0 1 0 434988000 43147264 9826 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10534 9826 603 41 0 10493 0
vsize: 42136
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 10050 0 0 0 45973 31 0 0 25 0 1 0 434988000 43675648 9956 4294967295 134512640 134672761 3221224544 3221223724 134553617 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10663 9956 603 41 0 10622 0
vsize: 42652
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 10202 0 0 0 46973 32 0 0 25 0 1 0 434988000 44363776 10108 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10831 10108 603 41 0 10790 0
vsize: 43324
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 10347 0 0 0 47973 32 0 0 25 0 1 0 434988000 44900352 10253 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10962 10253 603 41 0 10921 0
vsize: 43848
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 10513 0 0 0 48972 33 0 0 25 0 1 0 434988000 45563904 10419 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11124 10419 603 41 0 11083 0
vsize: 44496
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 10673 0 0 0 49972 33 0 0 25 0 1 0 434988000 46235648 10579 4294967295 134512640 134672761 3221224544 3221223728 134559590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11288 10579 603 41 0 11247 0
vsize: 45152
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 10793 0 0 0 50972 33 0 0 25 0 1 0 434988000 46776320 10699 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11420 10699 603 41 0 11379 0
vsize: 45680
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 10952 0 0 0 51971 34 0 0 25 0 1 0 434988000 47308800 10858 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11550 10858 603 41 0 11509 0
vsize: 46200
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 11104 0 0 0 52971 35 0 0 25 0 1 0 434988000 47992832 11010 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11717 11010 603 41 0 11676 0
vsize: 46868
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 11239 0 0 0 53970 35 0 0 25 0 1 0 434988000 48525312 11145 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11847 11145 603 41 0 11806 0
vsize: 47388
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 11351 0 0 0 54970 36 0 0 25 0 1 0 434988000 49061888 11257 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11978 11257 603 41 0 11937 0
vsize: 47912
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 11483 0 0 0 55970 36 0 0 25 0 1 0 434988000 49602560 11389 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12110 11389 603 41 0 12069 0
vsize: 48440
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 11629 0 0 0 56969 37 0 0 25 0 1 0 434988000 50130944 11535 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12239 11535 603 41 0 12198 0
vsize: 48956
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 11766 0 0 0 57969 38 0 0 25 0 1 0 434988000 50671616 11672 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12371 11672 603 41 0 12330 0
vsize: 49484
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 11951 0 0 0 58968 38 0 0 25 0 1 0 434988000 51478528 11857 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12568 11857 603 41 0 12527 0
vsize: 50272
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 12094 0 0 0 59968 39 0 0 25 0 1 0 434988000 52015104 12000 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12699 12000 603 41 0 12658 0
vsize: 50796
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 12257 0 0 0 60967 40 0 0 25 0 1 0 434988000 52695040 12163 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12865 12163 603 41 0 12824 0
vsize: 51460
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 12377 0 0 0 61967 40 0 0 25 0 1 0 434988000 53235712 12283 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12997 12283 603 41 0 12956 0
vsize: 51988
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 12483 0 0 0 62966 41 0 0 25 0 1 0 434988000 53649408 12389 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13098 12389 603 41 0 13057 0
vsize: 52392
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 12585 0 0 0 63966 41 0 0 25 0 1 0 434988000 54050816 12491 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13196 12491 603 41 0 13155 0
vsize: 52784
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8455
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 12727 0 0 0 64965 42 0 0 25 0 1 0 434988000 54616064 12633 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13334 12633 603 41 0 13293 0
vsize: 53336
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 12880 0 0 0 65964 43 0 0 25 0 1 0 434988000 55291904 12786 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13499 12786 603 41 0 13458 0
vsize: 53996
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 13024 0 0 0 66964 44 0 0 25 0 1 0 434988000 56352768 12930 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13758 12930 603 41 0 13717 0
vsize: 55032
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 13159 0 0 0 67963 44 0 0 25 0 1 0 434988000 57016320 13065 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13920 13065 603 41 0 13879 0
vsize: 55680
[startup+690.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 13239 0 0 0 68964 44 0 0 25 0 1 0 434988000 57278464 13145 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13984 13145 603 41 0 13943 0
vsize: 55936
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 13364 0 0 0 69963 45 0 0 25 0 1 0 434988000 57810944 13270 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14114 13270 603 41 0 14073 0
vsize: 56456
[startup+710.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 13481 0 0 0 70963 45 0 0 25 0 1 0 434988000 58212352 13387 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14212 13387 603 41 0 14171 0
vsize: 56848
[startup+720.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 13615 0 0 0 71963 46 0 0 25 0 1 0 434988000 58748928 13521 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14343 13521 603 41 0 14302 0
vsize: 57372
[startup+730.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 13728 0 0 0 72962 46 0 0 25 0 1 0 434988000 59293696 13634 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14476 13634 603 41 0 14435 0
vsize: 57904
[startup+740.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 13843 0 0 0 73962 46 0 0 25 0 1 0 434988000 59731968 13749 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14583 13749 603 41 0 14542 0
vsize: 58332
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 13972 0 0 0 74962 47 0 0 25 0 1 0 434988000 60272640 13878 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14715 13878 603 41 0 14674 0
vsize: 58860
[startup+760.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 14093 0 0 0 75962 47 0 0 25 0 1 0 434988000 60809216 13999 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14846 13999 603 41 0 14805 0
vsize: 59384
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 14197 0 0 0 76962 48 0 0 25 0 1 0 434988000 61210624 14103 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14944 14103 603 41 0 14903 0
vsize: 59776
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 14306 0 0 0 77962 48 0 0 25 0 1 0 434988000 61612032 14212 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15042 14212 603 41 0 15001 0
vsize: 60168
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 14419 0 0 0 78962 48 0 0 25 0 1 0 434988000 62038016 14325 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15146 14325 603 41 0 15105 0
vsize: 60584
[startup+800.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 14541 0 0 0 79961 49 0 0 25 0 1 0 434988000 62574592 14447 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15277 14447 603 41 0 15236 0
vsize: 61108
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 14665 0 0 0 80961 49 0 0 25 0 1 0 434988000 63115264 14571 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15409 14571 603 41 0 15368 0
vsize: 61636
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 14762 0 0 0 81961 49 0 0 25 0 1 0 434988000 63512576 14668 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15506 14668 603 41 0 15465 0
vsize: 62024
[startup+830.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 14898 0 0 0 82961 50 0 0 25 0 1 0 434988000 64040960 14804 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15635 14804 603 41 0 15594 0
vsize: 62540
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 15027 0 0 0 83960 50 0 0 25 0 1 0 434988000 64581632 14933 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15767 14933 603 41 0 15726 0
vsize: 63068
[startup+850.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 15170 0 0 0 84960 51 0 0 25 0 1 0 434988000 65118208 15076 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15898 15076 603 41 0 15857 0
vsize: 63592
[startup+860.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 15294 0 0 0 85959 52 0 0 25 0 1 0 434988000 65703936 15200 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16041 15200 603 41 0 16000 0
vsize: 64164
[startup+870.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 15417 0 0 0 86959 52 0 0 25 0 1 0 434988000 66285568 15323 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16183 15323 603 41 0 16142 0
vsize: 64732
[startup+880.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 15536 0 0 0 87959 52 0 0 25 0 1 0 434988000 66682880 15442 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16280 15442 603 41 0 16239 0
vsize: 65120
[startup+890.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 15678 0 0 0 88959 53 0 0 25 0 1 0 434988000 67371008 15584 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16448 15584 603 41 0 16407 0
vsize: 65792
[startup+900.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 15778 0 0 0 89959 53 0 0 25 0 1 0 434988000 67792896 15684 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16551 15684 603 41 0 16510 0
vsize: 66204
[startup+910.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 15859 0 0 0 90959 53 0 0 25 0 1 0 434988000 68059136 15765 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16616 15765 603 41 0 16575 0
vsize: 66464
[startup+920.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 15947 0 0 0 91958 54 0 0 25 0 1 0 434988000 68456448 15853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16713 15853 603 41 0 16672 0
vsize: 66852
[startup+930.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 16045 0 0 0 92958 54 0 0 25 0 1 0 434988000 68890624 15951 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16819 15951 603 41 0 16778 0
vsize: 67276
[startup+940.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 16136 0 0 0 93958 55 0 0 25 0 1 0 434988000 69160960 16042 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16885 16042 603 41 0 16844 0
vsize: 67540
[startup+950.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8457
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 16232 0 0 0 94958 55 0 0 25 0 1 0 434988000 69562368 16138 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16983 16138 603 41 0 16942 0
vsize: 67932
[startup+960.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 16322 0 0 0 95957 55 0 0 25 0 1 0 434988000 69971968 16228 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17083 16228 603 41 0 17042 0
vsize: 68332
[startup+970.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 16427 0 0 0 96958 55 0 0 25 0 1 0 434988000 70377472 16333 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16333 603 41 0 17141 0
vsize: 68728
[startup+980.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 16529 0 0 0 97958 56 0 0 25 0 1 0 434988000 70782976 16435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17281 16435 603 41 0 17240 0
vsize: 69124
[startup+990.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 16644 0 0 0 98957 57 0 0 25 0 1 0 434988000 71319552 16550 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17412 16550 603 41 0 17371 0
vsize: 69648
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 16739 0 0 0 99957 57 0 0 25 0 1 0 434988000 71720960 16645 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17510 16645 603 41 0 17469 0
vsize: 70040
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 16826 0 0 0 100956 58 0 0 25 0 1 0 434988000 71987200 16732 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17575 16732 603 41 0 17534 0
vsize: 70300
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 16934 0 0 0 101956 58 0 0 25 0 1 0 434988000 72523776 16840 4294967295 134512640 134672761 3221224544 3221223728 134559244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17706 16840 603 41 0 17665 0
vsize: 70824
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 17052 0 0 0 102956 58 0 0 25 0 1 0 434988000 72925184 16958 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 16958 603 41 0 17763 0
vsize: 71216
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 17141 0 0 0 103956 59 0 0 25 0 1 0 434988000 73342976 17047 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17906 17047 603 41 0 17865 0
vsize: 71624
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 17237 0 0 0 104956 59 0 0 25 0 1 0 434988000 73744384 17143 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18004 17143 603 41 0 17963 0
vsize: 72016
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 17339 0 0 0 105956 59 0 0 25 0 1 0 434988000 74153984 17245 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18104 17245 603 41 0 18063 0
vsize: 72416
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 17420 0 0 0 106956 59 0 0 25 0 1 0 434988000 74555392 17326 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18202 17326 603 41 0 18161 0
vsize: 72808
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 17512 0 0 0 107955 60 0 0 25 0 1 0 434988000 74956800 17418 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18300 17418 603 41 0 18259 0
vsize: 73200
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 17594 0 0 0 108955 60 0 0 25 0 1 0 434988000 75218944 17500 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18364 17500 603 41 0 18323 0
vsize: 73456
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 17703 0 0 0 109955 60 0 0 25 0 1 0 434988000 75755520 17609 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18495 17609 603 41 0 18454 0
vsize: 73980
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 17802 0 0 0 110955 61 0 0 25 0 1 0 434988000 76152832 17708 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18592 17708 603 41 0 18551 0
vsize: 74368
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 17896 0 0 0 111955 61 0 0 25 0 1 0 434988000 76550144 17802 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18689 17802 603 41 0 18648 0
vsize: 74756
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 18024 0 0 0 112955 61 0 0 25 0 1 0 434988000 77094912 17930 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18822 17930 603 41 0 18781 0
vsize: 75288
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 18119 0 0 0 113955 62 0 0 25 0 1 0 434988000 77418496 18025 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18901 18025 603 41 0 18860 0
vsize: 75604
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 18224 0 0 0 114954 62 0 0 25 0 1 0 434988000 77815808 18130 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18998 18130 603 41 0 18957 0
vsize: 75992
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 18336 0 0 0 115954 63 0 0 25 0 1 0 434988000 78340096 18242 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19126 18242 603 41 0 19085 0
vsize: 76504
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 18441 0 0 0 116954 63 0 0 25 0 1 0 434988000 78749696 18347 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19226 18347 603 41 0 19185 0
vsize: 76904
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 18534 0 0 0 117954 63 0 0 25 0 1 0 434988000 79151104 18440 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19324 18440 603 41 0 19283 0
vsize: 77296
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 18631 0 0 0 118954 64 0 0 25 0 1 0 434988000 79556608 18537 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19423 18537 603 41 0 19382 0
vsize: 77692
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 8459
Raw data (stat): 8451 (minisat+) R 8450 12452 12451 0 -1 0 18714 0 0 0 119953 64 0 0 25 0 1 0 434988000 79822848 18620 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19488 18620 603 41 0 19447 0
vsize: 77952
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.93 1/56 8459
Raw data (stat): 8451 (minisat+) Z 8450 12452 12451 0 -1 12 18716 0 0 0 119953 67 0 0 25 0 1 0 434988000 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.07
CPU time (s): 1200.22
CPU user time (s): 1199.54
CPU system time (s): 0.677896
CPU usage (%): 100.013
Max. virtual memory (Kb): 77952
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####