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/miplib3/normalized-mps-v2-13-7-pp08a.opb
MD5SUMd14265fdf4e5a3ef733af1f15b884cbe
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 6661373
Optimality of the best value was proved NO
Number of terms in the objective function 2304
Biggest coefficient in the objective function 1048576
Number of bits for the biggest coefficient in the objective function 21
Sum of the numbers in the objective function 178464600
Number of bits of the sum of numbers in the objective function 28
Biggest number in a constraint 1048576
Number of bits of the biggest number in a constraint 21
Biggest sum of numbers in a constraint 178464600
Number of bits of the biggest sum of numbers28
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.02
Number of variables3584
Total number of constraints136
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints136
Minimum length of a constraint21
Maximum length of a constraint160

Trace number 17951 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-21 12:50:05 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18784 boxname=wulflinc25 idbench=1445 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  d14265fdf4e5a3ef733af1f15b884cbe  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-pp08a.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-pp08a.opb /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-pp08a.opb
IDLAUNCH: 18784
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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	: 3
cpu MHz		: 451.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        806356 kB
Buffers:         22096 kB
Cached:         185784 kB
SwapCached:        744 kB
Active:          61516 kB
Inactive:       148260 kB
HighTotal:      131008 kB
HighFree:        39312 kB
LowTotal:       903652 kB
LowFree:        767044 kB
SwapTotal:     2097892 kB
SwapFree:      2096220 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4992 kB
Slab:            12776 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 13:10:07 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 18784 7 1200.24 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 200 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 199]---> BDD-cost: 1143
c ---[ 198]---> BDD-cost: 1143
c ---[ 197]---> BDD-cost: 1143
c ---[ 196]---> BDD-cost: 1165
c ---[ 195]---> BDD-cost: 1165
c ---[ 194]---> BDD-cost: 1165
c ---[ 193]---> BDD-cost: 1165
c ---[ 192]---> BDD-cost: 1176
c ---[ 190]---> BDD-cost:  158
c ---[ 188]---> BDD-cost:  585
c ---[ 186]---> BDD-cost:  585
c ---[ 184]---> BDD-cost:  580
c ---[ 182]---> BDD-cost:  580
c ---[ 180]---> BDD-cost:  570
c ---[ 178]---> BDD-cost:  537
c ---[ 176]---> BDD-cost:  183
c ---[ 174]---> BDD-cost:  178
c ---[ 172]---> BDD-cost:  566
c ---[ 170]---> BDD-cost:  576
c ---[ 168]---> BDD-cost:  576
c ---[ 166]---> BDD-cost:  576
c ---[ 164]---> BDD-cost:  529
c ---[ 162]---> BDD-cost:  566
c ---[ 160]---> BDD-cost:  181
c ---[ 158]---> BDD-cost:  180
c ---[ 156]---> BDD-cost:  585
c ---[ 154]---> BDD-cost:  537
c ---[ 152]---> BDD-cost:  580
c ---[ 150]---> BDD-cost:  575
c ---[ 148]---> BDD-cost:  570
c ---[ 146]---> BDD-cost:  585
c ---[ 144]---> BDD-cost:  174
c ---[ 142]---> BDD-cost:  158
c ---[ 140]---> BDD-cost:  580
c ---[ 138]---> BDD-cost:  580
c ---[ 136]---> BDD-cost:  585
c ---[ 134]---> BDD-cost:  565
c ---[ 132]---> BDD-cost:  585
c ---[ 130]---> BDD-cost:  580
c ---[ 128]---> BDD-cost:  183
c ---[ 126]---> BDD-cost:  181
c ---[ 124]---> BDD-cost:  529
c ---[ 122]---> BDD-cost:  571
c ---[ 120]---> BDD-cost:  566
c ---[ 118]---> BDD-cost:  576
c ---[ 116]---> BDD-cost:  576
c ---[ 114]---> BDD-cost:  571
c ---[ 112]---> BDD-cost:  181
c ---[ 110]---> BDD-cost:  186
c ---[ 108]---> BDD-cost:  575
c ---[ 106]---> BDD-cost:  575
c ---[ 104]---> BDD-cost:  575
c ---[ 102]---> BDD-cost:  580
c ---[ 100]---> BDD-cost:  580
c ---[  98]---> BDD-cost:  575
c ---[  96]---> BDD-cost:  186
c ---[  94]---> BDD-cost:  154
c ---[  92]---> BDD-cost:  571
c ---[  90]---> BDD-cost:  576
c ---[  88]---> BDD-cost:  576
c ---[  86]---> BDD-cost:  571
c ---[  84]---> BDD-cost:  571
c ---[  82]---> BDD-cost:  566
c ---[  80]---> BDD-cost:  175
c ---[  78]---> BDD-cost:  176
c ---[  76]---> BDD-cost:  562
c ---[  74]---> BDD-cost:  521
c ---[  72]---> BDD-cost:  521
c ---[  70]---> BDD-cost:  567
c ---[  68]---> BDD-cost:  567
c ---[  66]---> BDD-cost:  562
c ---[  64]---> BDD-cost:  176
c ---[  63]---> BDD-cost:   24
c ---[  62]---> BDD-cost:   24
c ---[  61]---> BDD-cost:   24
c ---[  60]---> BDD-cost:   21
c ---[  59]---> BDD-cost:   21
c ---[  58]---> BDD-cost:   21
c ---[  57]---> BDD-cost:   21
c ---[  56]---> BDD-cost:   23
c ---[  55]---> BDD-cost:   19
c ---[  54]---> BDD-cost:   19
c ---[  53]---> BDD-cost:   19
c ---[  52]---> BDD-cost:   19
c ---[  51]---> BDD-cost:   19
c ---[  50]---> BDD-cost:   19
c ---[  49]---> BDD-cost:   19
c ---[  48]---> BDD-cost:   19
c ---[  47]---> BDD-cost:   24
c ---[  46]---> BDD-cost:   24
c ---[  45]---> BDD-cost:   24
c ---[  44]---> BDD-cost:   21
c ---[  43]---> BDD-cost:   21
c ---[  42]---> BDD-cost:   21
c ---[  41]---> BDD-cost:   21
c ---[  40]---> BDD-cost:   23
c ---[  39]---> BDD-cost:   24
c ---[  38]---> BDD-cost:   24
c ---[  37]---> BDD-cost:   24
c ---[  36]---> BDD-cost:   21
c ---[  35]---> BDD-cost:   21
c ---[  34]---> BDD-cost:   21
c ---[  33]---> BDD-cost:   21
c ---[  32]---> BDD-cost:   23
c ---[  31]---> BDD-cost:   18
c ---[  30]---> BDD-cost:   18
c ---[  29]---> BDD-cost:   18
c ---[  28]---> BDD-cost:   18
c ---[  27]---> BDD-cost:   18
c ---[  26]---> BDD-cost:   18
c ---[  25]---> BDD-cost:   18
c ---[  24]---> BDD-cost:   18
c ---[  23]---> BDD-cost:   24
c ---[  22]---> BDD-cost:   24
c ---[  21]---> BDD-cost:   24
c ---[  20]---> BDD-cost:   21
c ---[  19]---> BDD-cost:   21
c ---[  18]---> BDD-cost:   21
c ---[  17]---> BDD-cost:   21
c ---[  16]---> BDD-cost:   21
c ---[  15]---> BDD-cost:   19
c ---[  14]---> BDD-cost:   19
c ---[  13]---> BDD-cost:   19
c ---[  12]---> BDD-cost:   19
c ---[  11]---> BDD-cost:   19
c ---[  10]---> BDD-cost:   19
c ---[   9]---> BDD-cost:   19
c ---[   8]---> BDD-cost:   19
c ---[   7]---> BDD-cost:   19
c ---[   6]---> BDD-cost:   19
c ---[   5]---> BDD-cost:   19
c ---[   4]---> BDD-cost:   19
c ---[   3]---> BDD-cost:   19
c ---[   2]---> BDD-cost:   19
c ---[   1]---> BDD-cost:   19
c ---[   0]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  107271   302166 |   35757       0        0     nan |  0.000 % |
c |       100 |  107271   302166 |   39332     100      868     8.7 |  1.022 % |
c |       250 |  107271   302166 |   43265     250     1801     7.2 |  1.022 % |
c |       475 |  107271   302166 |   47592     475     3242     6.8 |  1.022 % |
c |       814 |  107271   302166 |   52351     814     7939     9.8 |  1.022 % |
c |      1320 |  107271   302166 |   57587    1320    13062     9.9 |  1.022 % |
c |      2081 |  107271   302166 |   63345    2081    20055     9.6 |  1.022 % |
c |      3220 |  107271   302166 |   69680    3220    49647    15.4 |  1.022 % |
c |      4928 |  107271   302166 |   76648    4928    77726    15.8 |  1.022 % |
c |      7491 |  107271   302166 |   84313    7491   113248    15.1 |  1.022 % |
c |     11335 |  107271   302166 |   92744   11335   181836    16.0 |  1.022 % |
c |     17103 |  107271   302166 |  102018   17103   312333    18.3 |  1.022 % |
c |     25752 |  107271   302166 |  112220   25752   444926    17.3 |  1.022 % |
c |     38726 |  107271   302166 |  123442   38726   772271    19.9 |  1.022 % |
c |     58189 |  107271   302166 |  135787   58189  1285334    22.1 |  1.022 % |
c |     87381 |  107268   302157 |  149365   87376  1952103    22.3 |  1.024 % |
c |    131172 |  107268   302157 |  164302  131167  3139723    23.9 |  1.024 % |
c |    196856 |  107268   302157 |  180732   45309  1172827    25.9 |  1.024 % |
c |    295382 |  107244   302109 |  198805  143834  3970896    27.6 |  1.048 % |
c |    443172 |  107227   302075 |  218686  100372  2763503    27.5 |  1.064 % |
c |    664857 |  107204   302023 |  240555  110557  3411503    30.9 |  1.086 % |
c |    997383 |  107204   302023 |  264610  217089  7691050    35.4 |  1.086 % |
c |   1496171 |  107195   301996 |  291071  220199  5201055    23.6 |  1.093 % |
#### 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.62 0.78 0.84 2/54 6297
Raw data (stat): 6297 (runsolver) R 6296 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545221463 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.68 0.79 0.84 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 4602 0 0 0 984 14 0 0 25 0 1 0 545221463 22171648 4509 4294967295 134512640 134672761 3221224544 3221223728 134558324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5413 4509 603 41 0 5372 0
vsize: 21652
[startup+20.0008 s]
Raw data (loadavg): 0.73 0.80 0.84 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 5446 0 0 0 1981 18 0 0 25 0 1 0 545221463 25636864 5353 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6259 5353 603 41 0 6218 0
vsize: 25036
[startup+30.0014 s]
Raw data (loadavg): 0.77 0.80 0.84 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 6414 0 0 0 2977 22 0 0 25 0 1 0 545221463 29794304 6321 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7274 6321 603 41 0 7233 0
vsize: 29096
[startup+40.0014 s]
Raw data (loadavg): 0.80 0.81 0.85 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 6966 0 0 0 3976 23 0 0 25 0 1 0 545221463 32059392 6873 4294967295 134512640 134672761 3221224544 3221223696 134560074 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7827 6873 603 41 0 7786 0
vsize: 31308
[startup+50.0017 s]
Raw data (loadavg): 0.83 0.81 0.85 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 7379 0 0 0 4975 25 0 0 25 0 1 0 545221463 33701888 7286 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8228 7286 603 41 0 8187 0
vsize: 32912
[startup+60.0012 s]
Raw data (loadavg): 0.86 0.82 0.85 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 7882 0 0 0 5972 27 0 0 25 0 1 0 545221463 35713024 7789 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8719 7789 603 41 0 8678 0
vsize: 34876
[startup+70.0022 s]
Raw data (loadavg): 0.88 0.83 0.85 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 8283 0 0 0 6971 29 0 0 25 0 1 0 545221463 37871616 8190 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9246 8190 603 41 0 9205 0
vsize: 36984
[startup+80.0028 s]
Raw data (loadavg): 0.90 0.83 0.85 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 8685 0 0 0 7969 31 0 0 25 0 1 0 545221463 39493632 8592 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9642 8592 603 41 0 9601 0
vsize: 38568
[startup+90.0021 s]
Raw data (loadavg): 0.91 0.84 0.85 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 8961 0 0 0 8968 32 0 0 25 0 1 0 545221463 40574976 8868 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9906 8868 603 41 0 9865 0
vsize: 39624
[startup+100.002 s]
Raw data (loadavg): 0.93 0.84 0.85 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 9285 0 0 0 9967 33 0 0 25 0 1 0 545221463 41914368 9192 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10233 9192 603 41 0 10192 0
vsize: 40932
[startup+110.003 s]
Raw data (loadavg): 0.94 0.85 0.85 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 9520 0 0 0 10967 34 0 0 25 0 1 0 545221463 42909696 9427 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10476 9427 603 41 0 10435 0
vsize: 41904
[startup+120.003 s]
Raw data (loadavg): 0.95 0.85 0.85 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 9578 0 0 0 11966 34 0 0 25 0 1 0 545221463 43196416 9485 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10546 9485 603 41 0 10505 0
vsize: 42184
[startup+130.003 s]
Raw data (loadavg): 0.95 0.85 0.85 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 9579 0 0 0 12966 34 0 0 25 0 1 0 545221463 43196416 9486 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10546 9486 603 41 0 10505 0
vsize: 42184
[startup+140.003 s]
Raw data (loadavg): 0.96 0.86 0.85 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 9579 0 0 0 13966 35 0 0 25 0 1 0 545221463 43196416 9486 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10546 9486 603 41 0 10505 0
vsize: 42184
[startup+150.003 s]
Raw data (loadavg): 0.97 0.86 0.86 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 9579 0 0 0 14966 35 0 0 25 0 1 0 545221463 43196416 9486 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10546 9486 603 41 0 10505 0
vsize: 42184
[startup+160.01 s]
Raw data (loadavg): 0.97 0.87 0.86 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 9601 0 0 0 15967 35 0 0 25 0 1 0 545221463 43335680 9508 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10580 9508 603 41 0 10539 0
vsize: 42320
[startup+170.01 s]
Raw data (loadavg): 0.97 0.87 0.86 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 9649 0 0 0 16967 36 0 0 25 0 1 0 545221463 43528192 9556 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10627 9556 603 41 0 10586 0
vsize: 42508
[startup+180.01 s]
Raw data (loadavg): 0.98 0.87 0.86 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 9658 0 0 0 17967 36 0 0 25 0 1 0 545221463 43528192 9565 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10627 9565 603 41 0 10586 0
vsize: 42508
[startup+190.011 s]
Raw data (loadavg): 0.98 0.88 0.86 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 10089 0 0 0 18966 37 0 0 25 0 1 0 545221463 45314048 9996 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11063 9996 603 41 0 11022 0
vsize: 44252
[startup+200.011 s]
Raw data (loadavg): 0.98 0.88 0.86 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 10702 0 0 0 19963 40 0 0 25 0 1 0 545221463 47865856 10609 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11686 10609 603 41 0 11645 0
vsize: 46744
[startup+210.011 s]
Raw data (loadavg): 0.99 0.89 0.86 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 11310 0 0 0 20961 42 0 0 25 0 1 0 545221463 50278400 11217 4294967295 134512640 134672761 3221224544 3221223668 134566080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12275 11217 603 41 0 12234 0
vsize: 49100
[startup+220.012 s]
Raw data (loadavg): 0.99 0.89 0.86 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 12067 0 0 0 21959 44 0 0 25 0 1 0 545221463 53383168 11974 4294967295 134512640 134672761 3221224544 3221223648 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13033 11974 603 41 0 12992 0
vsize: 52132
[startup+230.013 s]
Raw data (loadavg): 0.99 0.89 0.86 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 12666 0 0 0 22957 47 0 0 25 0 1 0 545221463 55779328 12573 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13618 12573 603 41 0 13577 0
vsize: 54472
[startup+240.012 s]
Raw data (loadavg): 0.99 0.89 0.86 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 12666 0 0 0 23957 47 0 0 25 0 1 0 545221463 55779328 12573 4294967295 134512640 134672761 3221224544 3221223668 134566018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13618 12573 603 41 0 13577 0
vsize: 54472
[startup+250.012 s]
Raw data (loadavg): 0.99 0.90 0.87 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 12666 0 0 0 24956 47 0 0 25 0 1 0 545221463 55779328 12573 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13618 12573 603 41 0 13577 0
vsize: 54472
[startup+260.013 s]
Raw data (loadavg): 0.99 0.90 0.87 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 12666 0 0 0 25956 48 0 0 25 0 1 0 545221463 55779328 12573 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13618 12573 603 41 0 13577 0
vsize: 54472
[startup+270.013 s]
Raw data (loadavg): 0.99 0.90 0.87 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 12666 0 0 0 26956 48 0 0 25 0 1 0 545221463 55779328 12573 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13618 12573 603 41 0 13577 0
vsize: 54472
[startup+280.013 s]
Raw data (loadavg): 0.99 0.91 0.87 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 12666 0 0 0 27956 48 0 0 25 0 1 0 545221463 55779328 12573 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13618 12573 603 41 0 13577 0
vsize: 54472
[startup+290.013 s]
Raw data (loadavg): 0.99 0.91 0.87 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 12666 0 0 0 28956 48 0 0 25 0 1 0 545221463 55779328 12573 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13618 12573 603 41 0 13577 0
vsize: 54472
[startup+300.014 s]
Raw data (loadavg): 0.99 0.91 0.87 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 12685 0 0 0 29956 49 0 0 25 0 1 0 545221463 55922688 12592 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13653 12592 603 41 0 13612 0
vsize: 54612
[startup+310.014 s]
Raw data (loadavg): 0.99 0.91 0.87 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 12685 0 0 0 30956 49 0 0 25 0 1 0 545221463 55922688 12592 4294967295 134512640 134672761 3221224544 3221223716 134558791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13653 12592 603 41 0 13612 0
vsize: 54612
[startup+320.015 s]
Raw data (loadavg): 0.99 0.92 0.87 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 12685 0 0 0 31956 49 0 0 25 0 1 0 545221463 55922688 12592 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13653 12592 603 41 0 13612 0
vsize: 54612
[startup+330.015 s]
Raw data (loadavg): 0.99 0.92 0.87 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 12686 0 0 0 32956 49 0 0 25 0 1 0 545221463 55922688 12593 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13653 12593 603 41 0 13612 0
vsize: 54612
[startup+340.015 s]
Raw data (loadavg): 0.99 0.92 0.87 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 12693 0 0 0 33956 50 0 0 25 0 1 0 545221463 55922688 12600 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13653 12600 603 41 0 13612 0
vsize: 54612
[startup+350.015 s]
Raw data (loadavg): 0.99 0.92 0.88 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 12694 0 0 0 34955 51 0 0 25 0 1 0 545221463 55922688 12601 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13653 12601 603 41 0 13612 0
vsize: 54612
[startup+360.015 s]
Raw data (loadavg): 0.99 0.92 0.88 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 12837 0 0 0 35955 51 0 0 25 0 1 0 545221463 56594432 12744 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13817 12744 603 41 0 13776 0
vsize: 55268
[startup+370.015 s]
Raw data (loadavg): 0.99 0.93 0.88 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 13540 0 0 0 36953 53 0 0 25 0 1 0 545221463 59437056 13447 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14511 13447 603 41 0 14470 0
vsize: 58044
[startup+380.016 s]
Raw data (loadavg): 0.99 0.93 0.88 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 13808 0 0 0 37953 54 0 0 25 0 1 0 545221463 60506112 13715 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14772 13715 603 41 0 14731 0
vsize: 59088
[startup+390.016 s]
Raw data (loadavg): 0.99 0.93 0.88 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 13808 0 0 0 38953 54 0 0 25 0 1 0 545221463 60506112 13715 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14772 13715 603 41 0 14731 0
vsize: 59088
[startup+400.016 s]
Raw data (loadavg): 0.99 0.93 0.88 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 13808 0 0 0 39953 54 0 0 25 0 1 0 545221463 60506112 13715 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14772 13715 603 41 0 14731 0
vsize: 59088
[startup+410.016 s]
Raw data (loadavg): 0.99 0.93 0.88 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 13808 0 0 0 40953 54 0 0 25 0 1 0 545221463 60506112 13715 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14772 13715 603 41 0 14731 0
vsize: 59088
[startup+420.015 s]
Raw data (loadavg): 0.99 0.94 0.88 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 13808 0 0 0 41953 54 0 0 25 0 1 0 545221463 60506112 13715 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14772 13715 603 41 0 14731 0
vsize: 59088
[startup+430.016 s]
Raw data (loadavg): 0.99 0.94 0.88 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 13808 0 0 0 42954 54 0 0 25 0 1 0 545221463 60506112 13715 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14772 13715 603 41 0 14731 0
vsize: 59088
[startup+440.016 s]
Raw data (loadavg): 0.99 0.94 0.88 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 13808 0 0 0 43953 54 0 0 25 0 1 0 545221463 60506112 13715 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14772 13715 603 41 0 14731 0
vsize: 59088
[startup+450.016 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 13808 0 0 0 44952 54 0 0 25 0 1 0 545221463 60506112 13715 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14772 13715 603 41 0 14731 0
vsize: 59088
[startup+460.016 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 13808 0 0 0 45952 54 0 0 25 0 1 0 545221463 60506112 13715 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14772 13715 603 41 0 14731 0
vsize: 59088
[startup+470.015 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 13808 0 0 0 46953 54 0 0 25 0 1 0 545221463 60506112 13715 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14772 13715 603 41 0 14731 0
vsize: 59088
[startup+480.015 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 13836 0 0 0 47953 54 0 0 25 0 1 0 545221463 60506112 13743 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14772 13743 603 41 0 14731 0
vsize: 59088
[startup+490.014 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 14512 0 0 0 48951 56 0 0 25 0 1 0 545221463 63320064 14419 4294967295 134512640 134672761 3221224544 3221223648 134555133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15459 14419 603 41 0 15418 0
vsize: 61836
[startup+500.015 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 15100 0 0 0 49949 58 0 0 25 0 1 0 545221463 65732608 15007 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16048 15007 603 41 0 16007 0
vsize: 64192
[startup+510.015 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 15641 0 0 0 50948 60 0 0 25 0 1 0 545221463 67895296 15548 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16576 15548 603 41 0 16535 0
vsize: 66304
[startup+520.015 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 16050 0 0 0 51947 61 0 0 25 0 1 0 545221463 69636096 15957 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17001 15957 603 41 0 16960 0
vsize: 68004
[startup+530.016 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 16050 0 0 0 52947 61 0 0 25 0 1 0 545221463 69636096 15957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17001 15957 603 41 0 16960 0
vsize: 68004
[startup+540.015 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 16050 0 0 0 53947 61 0 0 25 0 1 0 545221463 69636096 15957 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17001 15957 603 41 0 16960 0
vsize: 68004
[startup+550.015 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 16050 0 0 0 54947 61 0 0 25 0 1 0 545221463 69636096 15957 4294967295 134512640 134672761 3221224544 3221223712 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17001 15957 603 41 0 16960 0
vsize: 68004
[startup+560.016 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 16050 0 0 0 55947 61 0 0 25 0 1 0 545221463 69636096 15957 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17001 15957 603 41 0 16960 0
vsize: 68004
[startup+570.015 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 16050 0 0 0 56948 61 0 0 25 0 1 0 545221463 69636096 15957 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17001 15957 603 41 0 16960 0
vsize: 68004
[startup+580.015 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 16052 0 0 0 57948 61 0 0 25 0 1 0 545221463 69636096 15959 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17001 15959 603 41 0 16960 0
vsize: 68004
[startup+590.014 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 6297
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 16052 0 0 0 58948 61 0 0 25 0 1 0 545221463 69636096 15959 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17001 15959 603 41 0 16960 0
vsize: 68004
[startup+600.015 s]
Raw data (loadavg): 0.99 0.96 0.90 3/57 6333
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 16053 0 0 0 59948 61 0 0 25 0 1 0 545221463 69636096 15960 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17001 15960 603 41 0 16960 0
vsize: 68004
[startup+610.016 s]
Raw data (loadavg): 1.22 1.01 0.92 2/54 6350
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 16053 0 0 0 60948 61 0 0 25 0 1 0 545221463 69636096 15960 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17001 15960 603 41 0 16960 0
vsize: 68004
[startup+620.016 s]
Raw data (loadavg): 1.18 1.00 0.92 2/54 6350
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 16058 0 0 0 61948 61 0 0 25 0 1 0 545221463 69636096 15965 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17001 15965 603 41 0 16960 0
vsize: 68004
[startup+630.016 s]
Raw data (loadavg): 1.15 1.00 0.92 2/54 6350
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 16067 0 0 0 62948 61 0 0 25 0 1 0 545221463 69636096 15974 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17001 15974 603 41 0 16960 0
vsize: 68004
[startup+640.016 s]
Raw data (loadavg): 1.13 1.00 0.92 2/54 6350
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 16079 0 0 0 63949 61 0 0 25 0 1 0 545221463 69787648 15986 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17038 15986 603 41 0 16997 0
vsize: 68152
[startup+650.016 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 6350
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 16080 0 0 0 64949 61 0 0 25 0 1 0 545221463 69787648 15987 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17038 15987 603 41 0 16997 0
vsize: 68152
[startup+660.015 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 6350
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 16080 0 0 0 65949 61 0 0 25 0 1 0 545221463 69787648 15987 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17038 15987 603 41 0 16997 0
vsize: 68152
[startup+670.015 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 6350
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 16080 0 0 0 66949 61 0 0 25 0 1 0 545221463 69787648 15987 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17038 15987 603 41 0 16997 0
vsize: 68152
[startup+680.015 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 16274 0 0 0 67949 61 0 0 25 0 1 0 545221463 70455296 16181 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17201 16181 603 41 0 17160 0
vsize: 68804
[startup+690.014 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 17022 0 0 0 68948 63 0 0 25 0 1 0 545221463 73539584 16929 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17954 16929 603 41 0 17913 0
vsize: 71816
[startup+700.015 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 17518 0 0 0 69947 64 0 0 25 0 1 0 545221463 75563008 17425 4294967295 134512640 134672761 3221224544 3221223728 134559055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18448 17425 603 41 0 18407 0
vsize: 73792
[startup+710.015 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 17988 0 0 0 70946 64 0 0 25 0 1 0 545221463 77582336 17895 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18941 17895 603 41 0 18900 0
vsize: 75764
[startup+720.014 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 18724 0 0 0 71944 67 0 0 25 0 1 0 545221463 80539648 18631 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19663 18631 603 41 0 19622 0
vsize: 78652
[startup+730.014 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 19496 0 0 0 72942 69 0 0 25 0 1 0 545221463 84692992 19403 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20677 19403 603 41 0 20636 0
vsize: 82708
[startup+740.014 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20196 0 0 0 73940 71 0 0 25 0 1 0 545221463 87519232 20103 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21367 20103 603 41 0 21326 0
vsize: 85468
[startup+750.014 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20502 0 0 0 74940 72 0 0 25 0 1 0 545221463 88862720 20409 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21695 20409 603 41 0 21654 0
vsize: 86780
[startup+760.014 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20502 0 0 0 75940 72 0 0 25 0 1 0 545221463 88862720 20409 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21695 20409 603 41 0 21654 0
vsize: 86780
[startup+770.013 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20502 0 0 0 76940 72 0 0 25 0 1 0 545221463 88862720 20409 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21695 20409 603 41 0 21654 0
vsize: 86780
[startup+780.014 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20502 0 0 0 77940 72 0 0 25 0 1 0 545221463 88862720 20409 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21695 20409 603 41 0 21654 0
vsize: 86780
[startup+790.013 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20502 0 0 0 78940 72 0 0 25 0 1 0 545221463 88862720 20409 4294967295 134512640 134672761 3221224544 3221223728 134559613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21695 20409 603 41 0 21654 0
vsize: 86780
[startup+800.014 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20502 0 0 0 79941 72 0 0 25 0 1 0 545221463 88862720 20409 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21695 20409 603 41 0 21654 0
vsize: 86780
[startup+810.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20503 0 0 0 80941 72 0 0 25 0 1 0 545221463 88862720 20410 4294967295 134512640 134672761 3221224544 3221223640 1075347174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21695 20410 603 41 0 21654 0
vsize: 86780
[startup+820.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20503 0 0 0 81941 72 0 0 25 0 1 0 545221463 88862720 20410 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21695 20410 603 41 0 21654 0
vsize: 86780
[startup+830.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20503 0 0 0 82941 72 0 0 25 0 1 0 545221463 88862720 20410 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21695 20410 603 41 0 21654 0
vsize: 86780
[startup+840.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20503 0 0 0 83941 72 0 0 25 0 1 0 545221463 88862720 20410 4294967295 134512640 134672761 3221224544 3221223744 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21695 20410 603 41 0 21654 0
vsize: 86780
[startup+850.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20503 0 0 0 84942 72 0 0 25 0 1 0 545221463 88862720 20410 4294967295 134512640 134672761 3221224544 3221223728 134559415 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21695 20410 603 41 0 21654 0
vsize: 86780
[startup+860.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20503 0 0 0 85942 72 0 0 25 0 1 0 545221463 88862720 20410 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21695 20410 603 41 0 21654 0
vsize: 86780
[startup+870.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20503 0 0 0 86942 72 0 0 25 0 1 0 545221463 88862720 20410 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21695 20410 603 41 0 21654 0
vsize: 86780
[startup+880.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20503 0 0 0 87942 72 0 0 25 0 1 0 545221463 88862720 20410 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21695 20410 603 41 0 21654 0
vsize: 86780
[startup+890.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20504 0 0 0 88942 72 0 0 25 0 1 0 545221463 88862720 20411 4294967295 134512640 134672761 3221224544 3221223680 134565070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21695 20411 603 41 0 21654 0
vsize: 86780
[startup+900.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20504 0 0 0 89943 72 0 0 25 0 1 0 545221463 88862720 20411 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21695 20411 603 41 0 21654 0
vsize: 86780
[startup+910.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20504 0 0 0 90943 72 0 0 25 0 1 0 545221463 88862720 20411 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21695 20411 603 41 0 21654 0
vsize: 86780
[startup+920.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20504 0 0 0 91943 72 0 0 25 0 1 0 545221463 88862720 20411 4294967295 134512640 134672761 3221224544 3221223648 134560065 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21695 20411 603 41 0 21654 0
vsize: 86780
[startup+930.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6352
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20504 0 0 0 92943 72 0 0 25 0 1 0 545221463 88862720 20411 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21695 20411 603 41 0 21654 0
vsize: 86780
[startup+940.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20504 0 0 0 93943 72 0 0 25 0 1 0 545221463 88862720 20411 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21695 20411 603 41 0 21654 0
vsize: 86780
[startup+950.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20534 0 0 0 94943 72 0 0 25 0 1 0 545221463 89006080 20441 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21730 20441 603 41 0 21689 0
vsize: 86920
[startup+960.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20801 0 0 0 95943 72 0 0 25 0 1 0 545221463 90083328 20708 4294967295 134512640 134672761 3221224544 3221223696 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20708 603 41 0 21952 0
vsize: 87972
[startup+970.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20805 0 0 0 96943 72 0 0 25 0 1 0 545221463 90083328 20712 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20712 603 41 0 21952 0
vsize: 87972
[startup+980.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20805 0 0 0 97943 72 0 0 25 0 1 0 545221463 90083328 20712 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20712 603 41 0 21952 0
vsize: 87972
[startup+990.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20805 0 0 0 98943 72 0 0 25 0 1 0 545221463 90083328 20712 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20712 603 41 0 21952 0
vsize: 87972
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20805 0 0 0 99943 72 0 0 25 0 1 0 545221463 90083328 20712 4294967295 134512640 134672761 3221224544 3221223696 134565143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20712 603 41 0 21952 0
vsize: 87972
[startup+1010.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20805 0 0 0 100944 72 0 0 25 0 1 0 545221463 90083328 20712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20712 603 41 0 21952 0
vsize: 87972
[startup+1020.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20806 0 0 0 101944 72 0 0 25 0 1 0 545221463 90083328 20713 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20713 603 41 0 21952 0
vsize: 87972
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20806 0 0 0 102944 72 0 0 25 0 1 0 545221463 90083328 20713 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20713 603 41 0 21952 0
vsize: 87972
[startup+1040.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20806 0 0 0 103944 72 0 0 25 0 1 0 545221463 90083328 20713 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20713 603 41 0 21952 0
vsize: 87972
[startup+1050.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20806 0 0 0 104944 72 0 0 25 0 1 0 545221463 90083328 20713 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20713 603 41 0 21952 0
vsize: 87972
[startup+1060.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20806 0 0 0 105945 72 0 0 25 0 1 0 545221463 90083328 20713 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20713 603 41 0 21952 0
vsize: 87972
[startup+1070.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20806 0 0 0 106945 72 0 0 25 0 1 0 545221463 90083328 20713 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20713 603 41 0 21952 0
vsize: 87972
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20806 0 0 0 107945 72 0 0 25 0 1 0 545221463 90083328 20713 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20713 603 41 0 21952 0
vsize: 87972
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20806 0 0 0 108945 72 0 0 25 0 1 0 545221463 90083328 20713 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20713 603 41 0 21952 0
vsize: 87972
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20806 0 0 0 109945 73 0 0 25 0 1 0 545221463 90083328 20713 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20713 603 41 0 21952 0
vsize: 87972
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20806 0 0 0 110945 73 0 0 25 0 1 0 545221463 90083328 20713 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20713 603 41 0 21952 0
vsize: 87972
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20806 0 0 0 111945 73 0 0 25 0 1 0 545221463 90083328 20713 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20713 603 41 0 21952 0
vsize: 87972
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20806 0 0 0 112946 73 0 0 25 0 1 0 545221463 90083328 20713 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20713 603 41 0 21952 0
vsize: 87972
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20806 0 0 0 113946 73 0 0 25 0 1 0 545221463 90083328 20713 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20713 603 41 0 21952 0
vsize: 87972
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20816 0 0 0 114946 73 0 0 25 0 1 0 545221463 90083328 20723 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20723 603 41 0 21952 0
vsize: 87972
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 20823 0 0 0 115946 73 0 0 25 0 1 0 545221463 90083328 20730 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 20730 603 41 0 21952 0
vsize: 87972
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 21306 0 0 0 116945 74 0 0 25 0 1 0 545221463 91955200 21213 4294967295 134512640 134672761 3221224544 3221223648 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22450 21213 603 41 0 22409 0
vsize: 89800
[startup+1180.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 21306 0 0 0 117945 74 0 0 25 0 1 0 545221463 91955200 21213 4294967295 134512640 134672761 3221224544 3221223728 134559514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22450 21213 603 41 0 22409 0
vsize: 89800
[startup+1190.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 21306 0 0 0 118945 74 0 0 25 0 1 0 545221463 91955200 21213 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22450 21213 603 41 0 22409 0
vsize: 89800
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 6354
Raw data (stat): 6297 (minisat+) R 6296 28099 28098 0 -1 0 21306 0 0 0 119945 74 0 0 25 0 1 0 545221463 91955200 21213 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22450 21213 603 41 0 22409 0
vsize: 89800
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 6354
Raw data (stat): 6297 (minisat+) Z 6296 28099 28098 0 -1 12 21308 0 0 0 119945 78 0 0 25 0 1 0 545221463 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.06
CPU time (s): 1200.24
CPU user time (s): 1199.46
CPU system time (s): 0.78488
CPU usage (%): 100.016
Max. virtual memory (Kb): 89800
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####