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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-mod010.opb
MD5SUM4f0cac14ed3568050c2c57bb69fdb664
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
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 numbers19
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1175.78
Number of variables2655
Total number of constraints2801
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)2800
Number of constraints which are nor clauses,nor cardinality constraints1
Minimum length of a constraint1
Maximum length of a constraint2655

Trace number 15634 

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        715276 kB
Buffers:         33000 kB
Cached:         264468 kB
SwapCached:        440 kB
Active:          36476 kB
Inactive:       263156 kB
HighTotal:      131008 kB
HighFree:        30296 kB
LowTotal:       903652 kB
LowFree:        684980 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5360 kB
Slab:            14048 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 05:39:29 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 17040 7 1200.23 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.77 0.93 0.93 2/54 29121
Raw data (stat): 29121 (runsolver) R 29120 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 484281913 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.0006 s]
Raw data (loadavg): 0.80 0.93 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 2947 0 0 0 990 8 0 0 25 0 1 0 484281913 14479360 2853 4294967295 134512640 134672761 3221224544 3221223708 134564508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3535 2853 603 41 0 3494 0
vsize: 14140
[startup+20.0012 s]
Raw data (loadavg): 0.83 0.93 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 2991 0 0 0 1989 8 0 0 25 0 1 0 484281913 14614528 2897 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3568 2897 603 41 0 3527 0
vsize: 14272
[startup+30.0009 s]
Raw data (loadavg): 0.86 0.93 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 3024 0 0 0 2988 9 0 0 25 0 1 0 484281913 14749696 2930 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3601 2930 603 41 0 3560 0
vsize: 14404
[startup+40.001 s]
Raw data (loadavg): 0.88 0.93 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 3046 0 0 0 3988 9 0 0 25 0 1 0 484281913 14880768 2952 4294967295 134512640 134672761 3221224544 3221223716 134556627 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.0015 s]
Raw data (loadavg): 0.90 0.93 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 3060 0 0 0 4989 9 0 0 25 0 1 0 484281913 14880768 2966 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.0023 s]
Raw data (loadavg): 0.91 0.94 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 3073 0 0 0 5989 9 0 0 25 0 1 0 484281913 14880768 2979 4294967295 134512640 134672761 3221224544 3221223696 134565137 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.0025 s]
Raw data (loadavg): 0.93 0.94 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 3086 0 0 0 6989 9 0 0 25 0 1 0 484281913 15015936 2992 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.0019 s]
Raw data (loadavg): 0.94 0.94 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 3123 0 0 0 7989 9 0 0 25 0 1 0 484281913 15147008 3029 4294967295 134512640 134672761 3221224544 3221223712 134560956 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.0018 s]
Raw data (loadavg): 0.95 0.94 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 3160 0 0 0 8989 9 0 0 25 0 1 0 484281913 15282176 3066 4294967295 134512640 134672761 3221224544 3221223716 134556618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3731 3066 603 41 0 3690 0
vsize: 14924
[startup+100.002 s]
Raw data (loadavg): 0.95 0.94 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 3299 0 0 0 9989 9 0 0 25 0 1 0 484281913 15818752 3205 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.002 s]
Raw data (loadavg): 0.96 0.94 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 3468 0 0 0 10988 10 0 0 25 0 1 0 484281913 16560128 3374 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4043 3374 603 41 0 4002 0
vsize: 16172
[startup+120.004 s]
Raw data (loadavg): 0.97 0.95 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 3596 0 0 0 11988 10 0 0 25 0 1 0 484281913 17096704 3502 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4174 3502 603 41 0 4133 0
vsize: 16696
[startup+130.003 s]
Raw data (loadavg): 0.97 0.95 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 3841 0 0 0 12988 11 0 0 25 0 1 0 484281913 18042880 3747 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4405 3747 603 41 0 4364 0
vsize: 17620
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 4090 0 0 0 13987 12 0 0 25 0 1 0 484281913 19120128 3996 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4668 3996 603 41 0 4627 0
vsize: 18672
[startup+150.004 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 4337 0 0 0 14987 12 0 0 25 0 1 0 484281913 20185088 4243 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4928 4243 603 41 0 4887 0
vsize: 19712
[startup+160.005 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 4637 0 0 0 15986 13 0 0 25 0 1 0 484281913 21397504 4543 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5224 4543 603 41 0 5183 0
vsize: 20896
[startup+170.004 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 4857 0 0 0 16985 14 0 0 25 0 1 0 484281913 22343680 4763 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5455 4763 603 41 0 5414 0
vsize: 21820
[startup+180.005 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 5084 0 0 0 17985 15 0 0 25 0 1 0 484281913 23277568 4990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5683 4990 603 41 0 5642 0
vsize: 22732
[startup+190.006 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 5239 0 0 0 18984 16 0 0 25 0 1 0 484281913 23814144 5145 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5814 5145 603 41 0 5773 0
vsize: 23256
[startup+200.006 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 5400 0 0 0 19983 17 0 0 25 0 1 0 484281913 24477696 5306 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5976 5306 603 41 0 5935 0
vsize: 23904
[startup+210.007 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 5605 0 0 0 20982 18 0 0 25 0 1 0 484281913 25288704 5511 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6174 5511 603 41 0 6133 0
vsize: 24696
[startup+220.008 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 5750 0 0 0 21982 18 0 0 25 0 1 0 484281913 25964544 5656 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6339 5656 603 41 0 6298 0
vsize: 25356
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 5933 0 0 0 22982 18 0 0 25 0 1 0 484281913 26636288 5839 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6503 5839 603 41 0 6462 0
vsize: 26012
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 6147 0 0 0 23982 19 0 0 25 0 1 0 484281913 27574272 6053 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6732 6053 603 41 0 6691 0
vsize: 26928
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 6314 0 0 0 24982 20 0 0 25 0 1 0 484281913 28250112 6220 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6897 6220 603 41 0 6856 0
vsize: 27588
[startup+260.009 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 6531 0 0 0 25981 21 0 0 25 0 1 0 484281913 29052928 6437 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7093 6437 603 41 0 7052 0
vsize: 28372
[startup+270.009 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 6729 0 0 0 26980 21 0 0 25 0 1 0 484281913 29859840 6635 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7290 6635 603 41 0 7249 0
vsize: 29160
[startup+280.009 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 6957 0 0 0 27980 22 0 0 25 0 1 0 484281913 31059968 6863 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7583 6863 603 41 0 7542 0
vsize: 30332
[startup+290.009 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 7120 0 0 0 28979 22 0 0 25 0 1 0 484281913 31727616 7026 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7746 7026 603 41 0 7705 0
vsize: 30984
[startup+300.01 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 7279 0 0 0 29979 23 0 0 25 0 1 0 484281913 32387072 7185 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7907 7185 603 41 0 7866 0
vsize: 31628
[startup+310.01 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 7390 0 0 0 30979 23 0 0 25 0 1 0 484281913 32792576 7296 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8006 7296 603 41 0 7965 0
vsize: 32024
[startup+320.01 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 7586 0 0 0 31979 24 0 0 25 0 1 0 484281913 33611776 7492 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8206 7492 603 41 0 8165 0
vsize: 32824
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 7758 0 0 0 32979 24 0 0 25 0 1 0 484281913 34295808 7664 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8373 7664 603 41 0 8332 0
vsize: 33492
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 7867 0 0 0 33979 24 0 0 25 0 1 0 484281913 34836480 7773 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8505 7773 603 41 0 8464 0
vsize: 34020
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 7984 0 0 0 34978 25 0 0 25 0 1 0 484281913 35241984 7890 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8604 7890 603 41 0 8563 0
vsize: 34416
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 8152 0 0 0 35978 25 0 0 25 0 1 0 484281913 35913728 8058 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8768 8058 603 41 0 8727 0
vsize: 35072
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 8376 0 0 0 36976 26 0 0 25 0 1 0 484281913 36843520 8282 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8995 8282 603 41 0 8954 0
vsize: 35980
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 8556 0 0 0 37976 27 0 0 25 0 1 0 484281913 37523456 8462 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9161 8462 603 41 0 9120 0
vsize: 36644
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 8816 0 0 0 38975 28 0 0 25 0 1 0 484281913 38592512 8722 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9422 8722 603 41 0 9381 0
vsize: 37688
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 9050 0 0 0 39974 29 0 0 25 0 1 0 484281913 39526400 8956 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9650 8956 603 41 0 9609 0
vsize: 38600
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 9189 0 0 0 40975 29 0 0 25 0 1 0 484281913 40198144 9095 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9814 9095 603 41 0 9773 0
vsize: 39256
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 9352 0 0 0 41974 29 0 0 25 0 1 0 484281913 40869888 9258 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9978 9258 603 41 0 9937 0
vsize: 39912
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 9497 0 0 0 42974 29 0 0 25 0 1 0 484281913 41406464 9403 4294967295 134512640 134672761 3221224544 3221223680 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10109 9403 603 41 0 10068 0
vsize: 40436
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 9658 0 0 0 43974 30 0 0 25 0 1 0 484281913 42065920 9564 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10270 9564 603 41 0 10229 0
vsize: 41080
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 9870 0 0 0 44973 31 0 0 25 0 1 0 484281913 42881024 9776 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10469 9776 603 41 0 10428 0
vsize: 41876
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 9998 0 0 0 45973 31 0 0 25 0 1 0 484281913 43409408 9904 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10598 9904 603 41 0 10557 0
vsize: 42392
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 10135 0 0 0 46973 32 0 0 25 0 1 0 484281913 44093440 10041 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10765 10041 603 41 0 10724 0
vsize: 43060
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 10287 0 0 0 47972 33 0 0 25 0 1 0 484281913 44634112 10193 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10897 10193 603 41 0 10856 0
vsize: 43588
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 10463 0 0 0 48972 33 0 0 25 0 1 0 484281913 45297664 10369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11059 10369 603 41 0 11018 0
vsize: 44236
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 10594 0 0 0 49972 33 0 0 25 0 1 0 484281913 45965312 10500 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11222 10500 603 41 0 11181 0
vsize: 44888
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 10746 0 0 0 50972 34 0 0 25 0 1 0 484281913 46505984 10652 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11354 10652 603 41 0 11313 0
vsize: 45416
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 10887 0 0 0 51971 34 0 0 25 0 1 0 484281913 47042560 10793 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11485 10793 603 41 0 11444 0
vsize: 45940
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 11026 0 0 0 52971 35 0 0 25 0 1 0 484281913 47710208 10932 4294967295 134512640 134672761 3221224544 3221223648 134560279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11648 10932 603 41 0 11607 0
vsize: 46592
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 11176 0 0 0 53971 35 0 0 25 0 1 0 484281913 48259072 11082 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11782 11082 603 41 0 11741 0
vsize: 47128
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 11308 0 0 0 54971 35 0 0 25 0 1 0 484281913 48795648 11214 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11913 11214 603 41 0 11872 0
vsize: 47652
[startup+560.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 11421 0 0 0 55971 36 0 0 25 0 1 0 484281913 49332224 11327 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12044 11327 603 41 0 12003 0
vsize: 48176
[startup+570.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 11545 0 0 0 56971 36 0 0 25 0 1 0 484281913 49737728 11451 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12143 11451 603 41 0 12102 0
vsize: 48572
[startup+580.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 11717 0 0 0 57970 37 0 0 25 0 1 0 484281913 50536448 11623 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12338 11623 603 41 0 12297 0
vsize: 49352
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 11879 0 0 0 58970 37 0 0 25 0 1 0 484281913 51212288 11785 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12503 11785 603 41 0 12462 0
vsize: 50012
[startup+600.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 12025 0 0 0 59970 38 0 0 25 0 1 0 484281913 51748864 11931 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12634 11931 603 41 0 12593 0
vsize: 50536
[startup+610.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 12173 0 0 0 60970 38 0 0 25 0 1 0 484281913 52432896 12079 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12801 12079 603 41 0 12760 0
vsize: 51204
[startup+620.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 12318 0 0 0 61969 39 0 0 25 0 1 0 484281913 52965376 12224 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12931 12224 603 41 0 12890 0
vsize: 51724
[startup+630.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 12439 0 0 0 62969 39 0 0 25 0 1 0 484281913 53514240 12345 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13065 12345 603 41 0 13024 0
vsize: 52260
[startup+640.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 12535 0 0 0 63968 40 0 0 25 0 1 0 484281913 53915648 12441 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13163 12441 603 41 0 13122 0
vsize: 52652
[startup+650.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 12651 0 0 0 64968 40 0 0 25 0 1 0 484281913 54349824 12557 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13269 12557 603 41 0 13228 0
vsize: 53076
[startup+660.028 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 12776 0 0 0 65968 40 0 0 25 0 1 0 484281913 54886400 12682 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13400 12682 603 41 0 13359 0
vsize: 53600
[startup+670.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 12949 0 0 0 66967 41 0 0 25 0 1 0 484281913 55562240 12855 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13565 12855 603 41 0 13524 0
vsize: 54260
[startup+680.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 13086 0 0 0 67968 41 0 0 25 0 1 0 484281913 56619008 12992 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13823 12992 603 41 0 13782 0
vsize: 55292
[startup+690.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 13195 0 0 0 68968 41 0 0 25 0 1 0 484281913 57147392 13101 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13101 603 41 0 13911 0
vsize: 55808
[startup+700.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 13272 0 0 0 69967 41 0 0 25 0 1 0 484281913 57409536 13178 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14016 13178 603 41 0 13975 0
vsize: 56064
[startup+710.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 13417 0 0 0 70967 41 0 0 25 0 1 0 484281913 57942016 13323 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14146 13323 603 41 0 14105 0
vsize: 56584
[startup+720.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 13543 0 0 0 71967 42 0 0 25 0 1 0 484281913 58478592 13449 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14277 13449 603 41 0 14236 0
vsize: 57108
[startup+730.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 13652 0 0 0 72967 42 0 0 25 0 1 0 484281913 58884096 13558 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14376 13558 603 41 0 14335 0
vsize: 57504
[startup+740.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 13767 0 0 0 73967 42 0 0 25 0 1 0 484281913 59428864 13673 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14509 13673 603 41 0 14468 0
vsize: 58036
[startup+750.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 13905 0 0 0 74967 42 0 0 25 0 1 0 484281913 60002304 13811 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14649 13811 603 41 0 14608 0
vsize: 58596
[startup+760.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 14042 0 0 0 75967 43 0 0 25 0 1 0 484281913 60542976 13948 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14781 13948 603 41 0 14740 0
vsize: 59124
[startup+770.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 14159 0 0 0 76967 43 0 0 25 0 1 0 484281913 61079552 14065 4294967295 134512640 134672761 3221224544 3221223712 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14912 14065 603 41 0 14871 0
vsize: 59648
[startup+780.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 14263 0 0 0 77967 43 0 0 25 0 1 0 484281913 61476864 14169 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15009 14169 603 41 0 14968 0
vsize: 60036
[startup+790.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 14385 0 0 0 78967 43 0 0 25 0 1 0 484281913 61902848 14291 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15113 14291 603 41 0 15072 0
vsize: 60452
[startup+800.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 14487 0 0 0 79967 44 0 0 25 0 1 0 484281913 62439424 14393 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15244 14393 603 41 0 15203 0
vsize: 60976
[startup+810.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 14614 0 0 0 80966 44 0 0 25 0 1 0 484281913 62849024 14520 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15344 14520 603 41 0 15303 0
vsize: 61376
[startup+820.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 14711 0 0 0 81966 45 0 0 25 0 1 0 484281913 63246336 14617 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15441 14617 603 41 0 15400 0
vsize: 61764
[startup+830.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 14828 0 0 0 82966 45 0 0 25 0 1 0 484281913 63774720 14734 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15570 14734 603 41 0 15529 0
vsize: 62280
[startup+840.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 14981 0 0 0 83966 45 0 0 25 0 1 0 484281913 64446464 14887 4294967295 134512640 134672761 3221224544 3221223728 134559542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15734 14887 603 41 0 15693 0
vsize: 62936
[startup+850.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 15133 0 0 0 84966 46 0 0 25 0 1 0 484281913 64983040 15039 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15865 15039 603 41 0 15824 0
vsize: 63460
[startup+860.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 15257 0 0 0 85966 46 0 0 25 0 1 0 484281913 65568768 15163 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16008 15163 603 41 0 15967 0
vsize: 64032
[startup+870.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 15357 0 0 0 86966 46 0 0 25 0 1 0 484281913 66019328 15263 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16118 15263 603 41 0 16077 0
vsize: 64472
[startup+880.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 15498 0 0 0 87965 47 0 0 25 0 1 0 484281913 66551808 15404 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16248 15404 603 41 0 16207 0
vsize: 64992
[startup+890.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 15637 0 0 0 88965 47 0 0 25 0 1 0 484281913 67084288 15543 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16378 15543 603 41 0 16337 0
vsize: 65512
[startup+900.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 15744 0 0 0 89965 47 0 0 25 0 1 0 484281913 67637248 15650 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16513 15650 603 41 0 16472 0
vsize: 66052
[startup+910.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 15837 0 0 0 90965 48 0 0 25 0 1 0 484281913 67928064 15743 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16584 15743 603 41 0 16543 0
vsize: 66336
[startup+920.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 15908 0 0 0 91965 48 0 0 25 0 1 0 484281913 68190208 15814 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16648 15814 603 41 0 16607 0
vsize: 66592
[startup+930.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 16019 0 0 0 92965 48 0 0 25 0 1 0 484281913 68726784 15925 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16779 15925 603 41 0 16738 0
vsize: 67116
[startup+940.038 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 16102 0 0 0 93966 48 0 0 25 0 1 0 484281913 69021696 16008 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16851 16008 603 41 0 16810 0
vsize: 67404
[startup+950.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 16190 0 0 0 94966 48 0 0 25 0 1 0 484281913 69427200 16096 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16950 16096 603 41 0 16909 0
vsize: 67800
[startup+960.039 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 16307 0 0 0 95966 48 0 0 25 0 1 0 484281913 69971968 16213 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17083 16213 603 41 0 17042 0
vsize: 68332
[startup+970.039 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 16414 0 0 0 96966 48 0 0 25 0 1 0 484281913 70377472 16320 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16320 603 41 0 17141 0
vsize: 68728
[startup+980.039 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 16501 0 0 0 97966 49 0 0 25 0 1 0 484281913 70647808 16407 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17248 16407 603 41 0 17207 0
vsize: 68992
[startup+990.039 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 16629 0 0 0 98965 49 0 0 25 0 1 0 484281913 71184384 16535 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17379 16535 603 41 0 17338 0
vsize: 69516
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 16732 0 0 0 99966 49 0 0 25 0 1 0 484281913 71589888 16638 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17478 16638 603 41 0 17437 0
vsize: 69912
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 16802 0 0 0 100965 49 0 0 25 0 1 0 484281913 71987200 16708 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17575 16708 603 41 0 17534 0
vsize: 70300
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 16918 0 0 0 101965 50 0 0 25 0 1 0 484281913 72388608 16824 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17673 16824 603 41 0 17632 0
vsize: 70692
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 17041 0 0 0 102965 50 0 0 25 0 1 0 484281913 72925184 16947 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 16947 603 41 0 17763 0
vsize: 71216
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 17135 0 0 0 103965 51 0 0 25 0 1 0 484281913 73342976 17041 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17906 17041 603 41 0 17865 0
vsize: 71624
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 17214 0 0 0 104965 51 0 0 25 0 1 0 484281913 73609216 17120 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17971 17120 603 41 0 17930 0
vsize: 71884
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 17328 0 0 0 105965 51 0 0 25 0 1 0 484281913 74153984 17234 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18104 17234 603 41 0 18063 0
vsize: 72416
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 17406 0 0 0 106965 51 0 0 25 0 1 0 484281913 74420224 17312 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18169 17312 603 41 0 18128 0
vsize: 72676
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 17501 0 0 0 107965 51 0 0 25 0 1 0 484281913 74821632 17407 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18267 17407 603 41 0 18226 0
vsize: 73068
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 17584 0 0 0 108965 52 0 0 25 0 1 0 484281913 75218944 17490 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18364 17490 603 41 0 18323 0
vsize: 73456
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 17690 0 0 0 109965 52 0 0 25 0 1 0 484281913 75620352 17596 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18462 17596 603 41 0 18421 0
vsize: 73848
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 17801 0 0 0 110964 53 0 0 25 0 1 0 484281913 76021760 17707 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18560 17707 603 41 0 18519 0
vsize: 74240
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 17890 0 0 0 111964 53 0 0 25 0 1 0 484281913 76414976 17796 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18656 17796 603 41 0 18615 0
vsize: 74624
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 18020 0 0 0 112964 53 0 0 25 0 1 0 484281913 76959744 17926 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18789 17926 603 41 0 18748 0
vsize: 75156
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 18115 0 0 0 113964 54 0 0 25 0 1 0 484281913 77418496 18021 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18901 18021 603 41 0 18860 0
vsize: 75604
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 18223 0 0 0 114964 54 0 0 25 0 1 0 484281913 77815808 18129 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18998 18129 603 41 0 18957 0
vsize: 75992
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 18336 0 0 0 115963 55 0 0 25 0 1 0 484281913 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.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 18442 0 0 0 116963 55 0 0 25 0 1 0 484281913 78749696 18348 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19226 18348 603 41 0 19185 0
vsize: 76904
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 18537 0 0 0 117963 55 0 0 25 0 1 0 484281913 79151104 18443 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19324 18443 603 41 0 19283 0
vsize: 77296
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 18632 0 0 0 118963 55 0 0 25 0 1 0 484281913 79556608 18538 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19423 18538 603 41 0 19382 0
vsize: 77692
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 29121
Raw data (stat): 29121 (minisat+) R 29120 29151 29150 0 -1 0 18716 0 0 0 119962 56 0 0 25 0 1 0 484281913 79953920 18622 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19520 18622 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.93 1/54 29121
Raw data (stat): 29121 (minisat+) Z 29120 29151 29150 0 -1 12 18718 0 0 0 119962 60 0 0 25 0 1 0 484281913 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.08
CPU time (s): 1200.23
CPU user time (s): 1199.63
CPU system time (s): 0.601908
CPU usage (%): 100.012
Max. virtual memory (Kb): 78080
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####