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-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-vpm1.opb
MD5SUMeb50800dc2fc522dd2f29a347fbab1da
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 20
Optimality of the best value was proved NO
Number of terms in the objective function 168
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 168
Number of bits of the sum of numbers in the objective function 8
Biggest number in a constraint 819200
Number of bits of the biggest number in a constraint 20
Biggest sum of numbers in a constraint 4941871
Number of bits of the biggest sum of numbers23
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark454.966
Number of variables2754
Total number of constraints612
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)168
Number of constraints which are nor clauses,nor cardinality constraints444
Minimum length of a constraint1
Maximum length of a constraint82

Trace number 13790 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-20 21:45:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13949 boxname=wulflinc25 idbench=1073 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  eb50800dc2fc522dd2f29a347fbab1da  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-vpm1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-vpm1.opb /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-vpm1.opb
IDLAUNCH: 13949
/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:        815116 kB
Buffers:          4552 kB
Cached:         195024 kB
SwapCached:        820 kB
Active:          29884 kB
Inactive:       171736 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        814864 kB
SwapTotal:     2097892 kB
SwapFree:      2096248 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           4988 kB
Slab:            12228 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 22:05:41 (client local time) WITH STATUS 0 IN 1200.47 SECONDS
stats: 13949 7 1200.47 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 485]---> BDD-cost:   10
c ---[ 484]---> BDD-cost:   10
c ---[ 483]---> BDD-cost:   10
c ---[ 482]---> BDD-cost:   10
c ---[ 481]---> BDD-cost:   10
c ---[ 480]---> BDD-cost:   10
c ---[ 479]---> BDD-cost:   10
c ---[ 478]---> BDD-cost:   10
c ---[ 477]---> BDD-cost:   10
c ---[ 474]---> BDD-cost:   10
c ---[ 473]---> BDD-cost:   10
c ---[ 472]---> BDD-cost:   10
c ---[ 471]---> BDD-cost:   10
c ---[ 468]---> BDD-cost:   10
c ---[ 467]---> BDD-cost:   10
c ---[ 466]---> BDD-cost:   10
c ---[ 465]---> BDD-cost:   10
c ---[ 462]---> BDD-cost:   10
c ---[ 459]---> BDD-cost:   10
c ---[ 458]---> BDD-cost:   10
c ---[ 457]---> BDD-cost:   10
c ---[ 454]---> BDD-cost:   10
c ---[ 453]---> BDD-cost:   10
c ---[ 452]---> BDD-cost:   10
c ---[ 451]---> BDD-cost:   10
c ---[ 450]---> BDD-cost:   10
c ---[ 448]---> BDD-cost:   10
c ---[ 447]---> BDD-cost:   10
c ---[ 446]---> BDD-cost:   10
c ---[ 445]---> BDD-cost:   10
c ---[ 444]---> BDD-cost:   10
c ---[ 441]---> BDD-cost:   10
c ---[ 440]---> BDD-cost:   10
c ---[ 439]---> BDD-cost:   10
c ---[ 433]---> BDD-cost:   10
c ---[ 427]---> BDD-cost:   10
c ---[ 422]---> BDD-cost:   10
c ---[ 421]---> BDD-cost:   10
c ---[ 415]---> BDD-cost:   10
c ---[ 409]---> BDD-cost:   10
c ---[ 408]---> BDD-cost:   10
c ---[ 402]---> BDD-cost:   10
c ---[ 397]---> BDD-cost:   10
c ---[ 396]---> BDD-cost:   10
c ---[ 391]---> BDD-cost:   10
c ---[ 390]---> BDD-cost:   10
c ---[ 386]---> BDD-cost:   10
c ---[ 385]---> BDD-cost:   10
c ---[ 384]---> BDD-cost:   10
c ---[ 380]---> BDD-cost:   10
c ---[ 379]---> BDD-cost:   10
c ---[ 378]---> BDD-cost:   10
c ---[ 374]---> BDD-cost:   10
c ---[ 373]---> BDD-cost:   10
c ---[ 372]---> BDD-cost:   10
c ---[ 368]---> BDD-cost:   10
c ---[ 367]---> BDD-cost:   10
c ---[ 366]---> BDD-cost:   10
c ---[ 365]---> BDD-cost:   10
c ---[ 364]---> BDD-cost:   10
c ---[ 359]---> BDD-cost:   10
c ---[ 353]---> BDD-cost:   10
c ---[ 347]---> BDD-cost:   10
c ---[ 339]---> BDD-cost:   10
c ---[ 333]---> BDD-cost:   10
c ---[ 327]---> BDD-cost:   10
c ---[ 321]---> BDD-cost:   10
c ---[ 317]---> BDD-cost:   17
c ---[ 316]---> BDD-cost:   17
c ---[ 315]---> BDD-cost:   17
c ---[ 314]---> BDD-cost:   17
c ---[ 313]---> BDD-cost:   17
c ---[ 312]---> BDD-cost:   17
c ---[ 310]---> BDD-cost:   17
c ---[ 309]---> BDD-cost:   17
c ---[ 308]---> BDD-cost:   17
c ---[ 307]---> BDD-cost:   17
c ---[ 306]---> BDD-cost:   17
c ---[ 302]---> BDD-cost:   16
c ---[ 301]---> BDD-cost:   16
c ---[ 300]---> BDD-cost:   16
c ---[ 295]---> BDD-cost:   16
c ---[ 294]---> BDD-cost:   16
c ---[ 290]---> BDD-cost:   18
c ---[ 289]---> BDD-cost:   18
c ---[ 288]---> BDD-cost:   18
c ---[ 287]---> BDD-cost:   16
c ---[ 286]---> BDD-cost:   16
c ---[ 285]---> BDD-cost:   16
c ---[ 284]---> BDD-cost:   16
c ---[ 283]---> BDD-cost:   16
c ---[ 282]---> BDD-cost:   16
c ---[ 280]---> BDD-cost:   16
c ---[ 279]---> BDD-cost:   16
c ---[ 278]---> BDD-cost:   16
c ---[ 277]---> BDD-cost:   16
c ---[ 276]---> BDD-cost:   16
c ---[ 274]---> Sorter-cost: 3227     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3
c ---[ 264]---> Sorter-cost: 3277     Base: 2 2 2 5 5 2 2 2 2 2 2 3 2 2 2
c ---[ 260]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 258]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 256]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[ 254]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[ 252]---> Adder-cost: 352   maxlim: 2104143   bits: 22/22
c ---[ 250]---> Sorter-cost: 2487     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2
c ---[ 248]---> Adder-cost: 304   maxlim: 2309043   bits: 22/22
c ---[ 246]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[ 244]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[ 242]---> Adder-cost: 288   maxlim: 1694643   bits: 21/21
c ---[ 236]---> Sorter-cost: 2294     Base: 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 234]---> Adder-cost: 312   maxlim: 2587171   bits: 22/22
c ---[ 232]---> Adder-cost: 260   maxlim: 897571   bits: 20/20
c ---[ 224]---> Sorter-cost: 2815     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3
c ---[ 222]---> Adder-cost: 350   maxlim: 1768271   bits: 22/21
c ---[ 216]---> Adder-cost: 274   maxlim: 1228100   bits: 21/21
c ---[ 214]---> Adder-cost: 312   maxlim: 1957187   bits: 22/21
c ---[ 212]---> Adder-cost: 312   maxlim: 1854787   bits: 22/21
c ---[ 210]---> Adder-cost: 390   maxlim: 2279471   bits: 22/22
c ---[ 208]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 206]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 204]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 202]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 200]---> Sorter-cost: 3241     Base: 2 2 2 2 5 5 2 2 2 2 2 2 5
c ---[ 198]---> Adder-cost: 440   maxlim: 3713071   bits: 23/22
c ---[ 196]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 194]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 192]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 191]---> BDD-cost:   48
c ---[ 190]---> Sorter-cost:  386     Base: 2 2 2 2 2 2 2 2 2
c ---[ 189]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2
c ---[ 188]---> Sorter-cost:  801     Base: 2 2 2 2 2 2 2 2 2
c ---[ 187]---> Sorter-cost: 1088     Base: 2 2 2 2 2 2 2 2 2
c ---[ 186]---> Sorter-cost:  982     Base: 2 2 2 2 2 2 2 2 2
c ---[ 185]---> BDD-cost:   48
c ---[ 184]---> Sorter-cost:  386     Base: 2 2 2 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2
c ---[ 182]---> Sorter-cost:  781     Base: 2 2 2 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost: 1034     Base: 2 2 2 2 2 2 2 2 2
c ---[ 180]---> Sorter-cost: 1032     Base: 2 2 2 2 2 2 2 2 2
c ---[ 179]---> BDD-cost:   48
c ---[ 178]---> Sorter-cost:  386     Base: 2 2 2 2 2 2 2 2 2
c ---[ 177]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2
c ---[ 176]---> Sorter-cost:  788     Base: 2 2 2 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost: 1047     Base: 2 2 2 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost: 1019     Base: 2 2 2 2 2 2 2 2 2
c ---[ 173]---> BDD-cost:   48
c ---[ 172]---> Sorter-cost:  370     Base: 2 2 2 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost: 1022     Base: 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost:  952     Base: 2 2 2 2 2 2 2 2 2
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    3
c ---[ 165]---> BDD-cost:    3
c ---[ 164]---> BDD-cost:    3
c ---[ 163]---> BDD-cost:    3
c ---[ 162]---> BDD-cost:    3
c ---[ 161]---> BDD-cost:    3
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:    3
c ---[ 158]---> BDD-cost:   10
c ---[ 157]---> BDD-cost:   10
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:   10
c ---[ 151]---> BDD-cost:   10
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:   10
c ---[ 145]---> BDD-cost:   10
c ---[ 144]---> BDD-cost:    3
c ---[ 142]---> BDD-cost:   10
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:   10
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    3
c ---[ 132]---> BDD-cost:    3
c ---[ 130]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    3
c ---[ 128]---> BDD-cost:    3
c ---[ 127]---> BDD-cost:    3
c ---[ 126]---> BDD-cost:    3
c ---[ 124]---> BDD-cost:   10
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:   10
c ---[ 116]---> BDD-cost:   10
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    9
c ---[ 110]---> BDD-cost:   10
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    9
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    3
c ---[ 102]---> BDD-cost:    9
c ---[  98]---> BDD-cost:   10
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:    9
c ---[  91]---> BDD-cost:    3
c ---[  90]---> BDD-cost:    3
c ---[  85]---> BDD-cost:   10
c ---[  84]---> BDD-cost:    3
c ---[  79]---> BDD-cost:    3
c ---[  78]---> BDD-cost:    3
c ---[  73]---> BDD-cost:    3
c ---[  72]---> BDD-cost:    3
c ---[  68]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    3
c ---[  66]---> BDD-cost:    3
c ---[  62]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  60]---> BDD-cost:    3
c ---[  56]---> BDD-cost:    3
c ---[  55]---> BDD-cost:    3
c ---[  54]---> BDD-cost:    3
c ---[  50]---> BDD-cost:    3
c ---[  49]---> BDD-cost:    3
c ---[  48]---> BDD-cost:    3
c ---[  47]---> BDD-cost:    3
c ---[  46]---> BDD-cost:    3
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:    9
c ---[  41]---> BDD-cost:    3
c ---[  40]---> BDD-cost:   10
c ---[  39]---> BDD-cost:    9
c ---[  38]---> BDD-cost:    9
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:    9
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:   10
c ---[  33]---> BDD-cost:    8
c ---[  32]---> BDD-cost:    8
c ---[  31]---> BDD-cost:    8
c ---[  30]---> BDD-cost:    8
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:   10
c ---[  27]---> BDD-cost:    8
c ---[  26]---> BDD-cost:    8
c ---[  25]---> BDD-cost:    8
c ---[  24]---> BDD-cost:    8
c ---[  22]---> BDD-cost:   10
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    9
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:    9
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    9
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:    9
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    9
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:    9
c ---[   4]---> BDD-cost:    9
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    8
c ---[   1]---> BDD-cost:    8
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  136974   386371 |   45658       0        0     nan |  0.000 % |
c |       100 |  136958   386319 |   50223      98      400     4.1 |  6.776 % |
c |       250 |  136942   386267 |   55246     246     2083     8.5 |  6.784 % |
c |       476 |  136915   386207 |   60770     471     3476     7.4 |  6.802 % |
c |       813 |  136828   386012 |   66847     807     5963     7.4 |  6.858 % |
c |      1320 |  136727   385772 |   73532    1301    13310    10.2 |  6.920 % |
c |      2079 |  136696   385703 |   80885    2059    21977    10.7 |  6.941 % |
c |      3218 |  136509   385281 |   88974    3193    36342    11.4 |  7.060 % |
c |      4926 |  136435   385098 |   97871    4891    54411    11.1 |  7.109 % |
c |      7489 |  136392   385002 |  107659    7453    90936    12.2 |  7.137 % |
c |     11333 |  136258   384661 |  118425   11278   151608    13.4 |  7.222 % |
c |     17101 |  135693   383357 |  130267   16967   236451    13.9 |  7.615 % |
c |     25750 |  135442   382723 |  143294   25580   374080    14.6 |  7.770 % |
c |     38725 |  135230   382216 |  157623   38526   623273    16.2 |  7.912 % |
c |     58186 |  134907   381435 |  173386   57948  1013349    17.5 |  8.131 % |
c |     87380 |  134555   380614 |  190724   87063  1637273    18.8 |  8.397 % |
c |    131169 |  134042   379340 |  209797  130769  2791932    21.4 |  8.722 % |
c |    196853 |  133828   378809 |  230777  196431  5226112    26.6 |  8.856 % |
c |    295380 |  133420   377870 |  253854   71774  2364572    32.9 |  9.156 % |
c |    443170 |  132512   375752 |  279240  219500  7855049    35.8 |  9.886 % |
#### 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.50 0.80 0.88 2/54 22887
Raw data (stat): 22887 (runsolver) R 22886 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539794060 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.57 0.81 0.89 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 4243 0 0 0 988 10 0 0 25 0 1 0 539794060 20410368 4066 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4983 4066 603 41 0 4942 0
vsize: 19932
[startup+20.0006 s]
Raw data (loadavg): 0.64 0.81 0.89 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 4644 0 0 0 1985 12 0 0 25 0 1 0 539794060 22048768 4467 4294967295 134512640 134672761 3221224544 3221223648 134554735 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5383 4467 603 41 0 5342 0
vsize: 21532
[startup+30.0005 s]
Raw data (loadavg): 0.69 0.82 0.89 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 5204 0 0 0 2985 13 0 0 25 0 1 0 539794060 24322048 5027 4294967295 134512640 134672761 3221224544 3221223680 134560611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5938 5027 603 41 0 5897 0
vsize: 23752
[startup+40.0011 s]
Raw data (loadavg): 0.74 0.82 0.89 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 5742 0 0 0 3983 14 0 0 25 0 1 0 539794060 26472448 5565 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6463 5565 603 41 0 6422 0
vsize: 25852
[startup+50.0014 s]
Raw data (loadavg): 0.78 0.83 0.89 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 6204 0 0 0 4982 16 0 0 25 0 1 0 539794060 28614656 6027 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6027 603 41 0 6945 0
vsize: 27944
[startup+60.0013 s]
Raw data (loadavg): 0.81 0.83 0.89 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 6547 0 0 0 5980 18 0 0 25 0 1 0 539794060 29958144 6370 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7314 6370 603 41 0 7273 0
vsize: 29256
[startup+70.0019 s]
Raw data (loadavg): 0.84 0.84 0.89 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 6909 0 0 0 6979 19 0 0 25 0 1 0 539794060 31432704 6732 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6732 603 41 0 7633 0
vsize: 30696
[startup+80.0022 s]
Raw data (loadavg): 0.87 0.84 0.89 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 7356 0 0 0 7977 21 0 0 25 0 1 0 539794060 33177600 7179 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8100 7179 603 41 0 8059 0
vsize: 32400
[startup+90.0031 s]
Raw data (loadavg): 0.89 0.85 0.89 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 7732 0 0 0 8976 22 0 0 25 0 1 0 539794060 34652160 7555 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8460 7555 603 41 0 8419 0
vsize: 33840
[startup+100.003 s]
Raw data (loadavg): 0.90 0.85 0.89 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 8065 0 0 0 9975 23 0 0 25 0 1 0 539794060 35999744 7888 4294967295 134512640 134672761 3221224544 3221223692 1074733103 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8789 7888 603 41 0 8748 0
vsize: 35156
[startup+110.002 s]
Raw data (loadavg): 0.92 0.86 0.89 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 8543 0 0 0 10973 25 0 0 25 0 1 0 539794060 38522880 8366 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9405 8366 603 41 0 9364 0
vsize: 37620
[startup+120.003 s]
Raw data (loadavg): 0.93 0.86 0.90 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 8998 0 0 0 11972 26 0 0 25 0 1 0 539794060 40255488 8821 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9828 8821 603 41 0 9787 0
vsize: 39312
[startup+130.003 s]
Raw data (loadavg): 0.94 0.87 0.90 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 9381 0 0 0 12971 27 0 0 25 0 1 0 539794060 41857024 9204 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10219 9204 603 41 0 10178 0
vsize: 40876
[startup+140.003 s]
Raw data (loadavg): 0.95 0.87 0.90 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 9713 0 0 0 13970 29 0 0 25 0 1 0 539794060 43188224 9536 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10544 9536 603 41 0 10503 0
vsize: 42176
[startup+150.004 s]
Raw data (loadavg): 0.96 0.87 0.90 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 9989 0 0 0 14969 30 0 0 25 0 1 0 539794060 44277760 9812 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10810 9812 603 41 0 10769 0
vsize: 43240
[startup+160.004 s]
Raw data (loadavg): 0.96 0.88 0.90 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 10343 0 0 0 15968 31 0 0 25 0 1 0 539794060 45756416 10166 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11171 10166 603 41 0 11130 0
vsize: 44684
[startup+170.004 s]
Raw data (loadavg): 0.97 0.88 0.90 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 10819 0 0 0 16967 33 0 0 25 0 1 0 539794060 47632384 10642 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11629 10642 603 41 0 11588 0
vsize: 46516
[startup+180.004 s]
Raw data (loadavg): 0.97 0.88 0.90 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 11413 0 0 0 17965 34 0 0 25 0 1 0 539794060 50057216 11236 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12221 11236 603 41 0 12180 0
vsize: 48884
[startup+190.004 s]
Raw data (loadavg): 0.98 0.89 0.90 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 11804 0 0 0 18964 35 0 0 25 0 1 0 539794060 51564544 11627 4294967295 134512640 134672761 3221224544 3221223728 134559334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12589 11627 603 41 0 12548 0
vsize: 50356
[startup+200.005 s]
Raw data (loadavg): 0.98 0.89 0.90 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 12307 0 0 0 19963 37 0 0 25 0 1 0 539794060 53579776 12130 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13081 12130 603 41 0 13040 0
vsize: 52324
[startup+210.005 s]
Raw data (loadavg): 0.98 0.89 0.90 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 12744 0 0 0 20962 38 0 0 25 0 1 0 539794060 55332864 12567 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13509 12567 603 41 0 13468 0
vsize: 54036
[startup+220.005 s]
Raw data (loadavg): 0.98 0.90 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13033 0 0 0 21961 39 0 0 25 0 1 0 539794060 56541184 12856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13804 12856 603 41 0 13763 0
vsize: 55216
[startup+230.005 s]
Raw data (loadavg): 0.99 0.90 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13321 0 0 0 22961 40 0 0 25 0 1 0 539794060 57737216 13144 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14096 13144 603 41 0 14055 0
vsize: 56384
[startup+240.006 s]
Raw data (loadavg): 0.99 0.90 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 23961 40 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+250.006 s]
Raw data (loadavg): 0.99 0.91 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 24961 40 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+260.007 s]
Raw data (loadavg): 0.99 0.91 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 25961 40 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+270.007 s]
Raw data (loadavg): 0.99 0.91 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 26961 40 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+280.007 s]
Raw data (loadavg): 0.99 0.91 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 27961 40 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+290.007 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 28962 40 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+300.007 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 29962 40 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+310.007 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 30962 40 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+320.007 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 31961 40 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+330.009 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 32962 40 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+340.009 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 33961 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+350.009 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 34961 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+360.009 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 35961 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+370.01 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 36961 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+380.009 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 37962 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+390.01 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 38962 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+400.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 39962 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+410.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 40962 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+420.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 41962 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+430.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 42963 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+440.011 s]
Raw data (loadavg): 1.07 0.96 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 43963 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+450.011 s]
Raw data (loadavg): 1.06 0.96 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 44963 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+460.011 s]
Raw data (loadavg): 1.05 0.96 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 45963 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+470.012 s]
Raw data (loadavg): 1.04 0.96 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 46964 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223728 134558324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+480.012 s]
Raw data (loadavg): 1.04 0.96 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 47964 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+490.012 s]
Raw data (loadavg): 1.03 0.96 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 48964 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+500.012 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 49964 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+510.115 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 50975 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+520.116 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 51975 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+530.122 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 52976 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+540.13 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13480 0 0 0 53977 41 0 0 25 0 1 0 539794060 58396672 13303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13303 603 41 0 14216 0
vsize: 57028
[startup+550.132 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13481 0 0 0 54977 41 0 0 25 0 1 0 539794060 58396672 13304 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13304 603 41 0 14216 0
vsize: 57028
[startup+560.131 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13494 0 0 0 55977 41 0 0 25 0 1 0 539794060 58396672 13317 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13317 603 41 0 14216 0
vsize: 57028
[startup+570.14 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13513 0 0 0 56978 41 0 0 25 0 1 0 539794060 58568704 13336 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14299 13336 603 41 0 14258 0
vsize: 57196
[startup+580.14 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13524 0 0 0 57978 41 0 0 25 0 1 0 539794060 58568704 13347 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14299 13347 603 41 0 14258 0
vsize: 57196
[startup+590.139 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13524 0 0 0 58978 41 0 0 25 0 1 0 539794060 58568704 13347 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14299 13347 603 41 0 14258 0
vsize: 57196
[startup+600.139 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13529 0 0 0 59978 41 0 0 25 0 1 0 539794060 58568704 13352 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14299 13352 603 41 0 14258 0
vsize: 57196
[startup+610.138 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13529 0 0 0 60978 41 0 0 25 0 1 0 539794060 58568704 13352 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14299 13352 603 41 0 14258 0
vsize: 57196
[startup+620.139 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13540 0 0 0 61979 41 0 0 25 0 1 0 539794060 58732544 13363 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14339 13363 603 41 0 14298 0
vsize: 57356
[startup+630.138 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13540 0 0 0 62979 41 0 0 25 0 1 0 539794060 58732544 13363 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14339 13363 603 41 0 14298 0
vsize: 57356
[startup+640.138 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13567 0 0 0 63979 41 0 0 25 0 1 0 539794060 58896384 13390 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14379 13390 603 41 0 14338 0
vsize: 57516
[startup+650.138 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13601 0 0 0 64979 41 0 0 25 0 1 0 539794060 59092992 13424 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14427 13424 603 41 0 14386 0
vsize: 57708
[startup+660.138 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13609 0 0 0 65979 41 0 0 25 0 1 0 539794060 59092992 13432 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14427 13432 603 41 0 14386 0
vsize: 57708
[startup+670.139 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13611 0 0 0 66980 41 0 0 25 0 1 0 539794060 59092992 13434 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14427 13434 603 41 0 14386 0
vsize: 57708
[startup+680.139 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13626 0 0 0 67980 41 0 0 25 0 1 0 539794060 59092992 13449 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14427 13449 603 41 0 14386 0
vsize: 57708
[startup+690.139 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13628 0 0 0 68980 41 0 0 25 0 1 0 539794060 59092992 13451 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14427 13451 603 41 0 14386 0
vsize: 57708
[startup+700.139 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13628 0 0 0 69980 41 0 0 25 0 1 0 539794060 59092992 13451 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14427 13451 603 41 0 14386 0
vsize: 57708
[startup+710.139 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13638 0 0 0 70980 41 0 0 25 0 1 0 539794060 59256832 13461 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14467 13461 603 41 0 14426 0
vsize: 57868
[startup+720.147 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13638 0 0 0 71981 41 0 0 25 0 1 0 539794060 59256832 13461 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14467 13461 603 41 0 14426 0
vsize: 57868
[startup+730.147 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13638 0 0 0 72981 41 0 0 25 0 1 0 539794060 59256832 13461 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14467 13461 603 41 0 14426 0
vsize: 57868
[startup+740.147 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13640 0 0 0 73982 41 0 0 25 0 1 0 539794060 59256832 13463 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14467 13463 603 41 0 14426 0
vsize: 57868
[startup+750.148 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13689 0 0 0 74982 41 0 0 25 0 1 0 539794060 59387904 13512 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14499 13512 603 41 0 14458 0
vsize: 57996
[startup+760.25 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13769 0 0 0 75992 41 0 0 25 0 1 0 539794060 59793408 13592 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14598 13592 603 41 0 14557 0
vsize: 58392
[startup+770.25 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13850 0 0 0 76991 42 0 0 25 0 1 0 539794060 60063744 13673 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14664 13673 603 41 0 14623 0
vsize: 58656
[startup+780.25 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 13925 0 0 0 77992 42 0 0 25 0 1 0 539794060 60469248 13748 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14763 13748 603 41 0 14722 0
vsize: 59052
[startup+790.25 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 14015 0 0 0 78992 42 0 0 25 0 1 0 539794060 60878848 13838 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14863 13838 603 41 0 14822 0
vsize: 59452
[startup+800.25 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 14126 0 0 0 79992 42 0 0 25 0 1 0 539794060 61304832 13949 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14967 13949 603 41 0 14926 0
vsize: 59868
[startup+810.25 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 14218 0 0 0 80992 42 0 0 25 0 1 0 539794060 61710336 14041 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15066 14041 603 41 0 15025 0
vsize: 60264
[startup+820.262 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 14307 0 0 0 81993 43 0 0 25 0 1 0 539794060 62119936 14130 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15166 14130 603 41 0 15125 0
vsize: 60664
[startup+830.269 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 14377 0 0 0 82993 43 0 0 25 0 1 0 539794060 62386176 14200 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15231 14200 603 41 0 15190 0
vsize: 60924
[startup+840.269 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 14465 0 0 0 83993 44 0 0 25 0 1 0 539794060 62791680 14288 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15330 14288 603 41 0 15289 0
vsize: 61320
[startup+850.27 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 14532 0 0 0 84993 44 0 0 25 0 1 0 539794060 63057920 14355 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15395 14355 603 41 0 15354 0
vsize: 61580
[startup+860.285 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 14584 0 0 0 85994 44 0 0 25 0 1 0 539794060 63193088 14407 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15428 14407 603 41 0 15387 0
vsize: 61712
[startup+870.285 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22887
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 14636 0 0 0 86994 45 0 0 25 0 1 0 539794060 63463424 14459 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15494 14459 603 41 0 15453 0
vsize: 61976
[startup+880.285 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 22940
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 14699 0 0 0 87990 48 0 0 25 0 1 0 539794060 63733760 14522 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15560 14522 603 41 0 15519 0
vsize: 62240
[startup+890.292 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 22940
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 14772 0 0 0 88991 48 0 0 25 0 1 0 539794060 64049152 14595 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15637 14595 603 41 0 15596 0
vsize: 62548
[startup+900.292 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 22940
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 14833 0 0 0 89991 49 0 0 25 0 1 0 539794060 64315392 14656 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15702 14656 603 41 0 15661 0
vsize: 62808
[startup+910.292 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 22940
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 14889 0 0 0 90991 49 0 0 25 0 1 0 539794060 64585728 14712 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15768 14712 603 41 0 15727 0
vsize: 63072
[startup+920.292 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 22940
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 15012 0 0 0 91990 49 0 0 25 0 1 0 539794060 65122304 14835 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15899 14835 603 41 0 15858 0
vsize: 63596
[startup+930.292 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 22940
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 15186 0 0 0 92990 50 0 0 25 0 1 0 539794060 65785856 15009 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16061 15009 603 41 0 16020 0
vsize: 64244
[startup+940.292 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 22940
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 15249 0 0 0 93990 50 0 0 25 0 1 0 539794060 66052096 15072 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16126 15072 603 41 0 16085 0
vsize: 64504
[startup+950.292 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 15320 0 0 0 94988 51 0 0 25 0 1 0 539794060 66322432 15143 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16192 15143 603 41 0 16151 0
vsize: 64768
[startup+960.292 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 15487 0 0 0 95988 51 0 0 25 0 1 0 539794060 66994176 15310 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16356 15310 603 41 0 16315 0
vsize: 65424
[startup+970.293 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 15567 0 0 0 96988 51 0 0 25 0 1 0 539794060 67448832 15390 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16467 15390 603 41 0 16426 0
vsize: 65868
[startup+980.292 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 15616 0 0 0 97988 51 0 0 25 0 1 0 539794060 67584000 15439 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16500 15439 603 41 0 16459 0
vsize: 66000
[startup+990.292 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 15689 0 0 0 98987 52 0 0 25 0 1 0 539794060 67854336 15512 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16566 15512 603 41 0 16525 0
vsize: 66264
[startup+1000.29 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 15755 0 0 0 99987 52 0 0 25 0 1 0 539794060 68124672 15578 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16632 15578 603 41 0 16591 0
vsize: 66528
[startup+1010.29 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 15807 0 0 0 100987 52 0 0 25 0 1 0 539794060 68415488 15630 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16703 15630 603 41 0 16662 0
vsize: 66812
[startup+1020.29 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 15941 0 0 0 101987 53 0 0 25 0 1 0 539794060 68943872 15764 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16832 15764 603 41 0 16791 0
vsize: 67328
[startup+1030.29 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 16215 0 0 0 102987 53 0 0 25 0 1 0 539794060 70053888 16038 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17103 16038 603 41 0 17062 0
vsize: 68412
[startup+1040.29 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 16304 0 0 0 103986 54 0 0 25 0 1 0 539794060 70455296 16127 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17201 16127 603 41 0 17160 0
vsize: 68804
[startup+1050.29 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 16360 0 0 0 104986 54 0 0 25 0 1 0 539794060 70721536 16183 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17266 16183 603 41 0 17225 0
vsize: 69064
[startup+1060.29 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 16420 0 0 0 105986 54 0 0 25 0 1 0 539794060 70987776 16243 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17331 16243 603 41 0 17290 0
vsize: 69324
[startup+1070.29 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 16485 0 0 0 106986 55 0 0 25 0 1 0 539794060 71122944 16308 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17364 16308 603 41 0 17323 0
vsize: 69456
[startup+1080.29 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 16535 0 0 0 107986 55 0 0 25 0 1 0 539794060 71393280 16358 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17430 16358 603 41 0 17389 0
vsize: 69720
[startup+1090.29 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 16612 0 0 0 108986 55 0 0 25 0 1 0 539794060 71688192 16435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16435 603 41 0 17461 0
vsize: 70008
[startup+1100.29 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 16694 0 0 0 109986 55 0 0 25 0 1 0 539794060 72085504 16517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16517 603 41 0 17558 0
vsize: 70396
[startup+1110.29 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 16806 0 0 0 110986 56 0 0 25 0 1 0 539794060 72491008 16629 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17698 16629 603 41 0 17657 0
vsize: 70792
[startup+1120.29 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 16918 0 0 0 111986 56 0 0 25 0 1 0 539794060 73027584 16741 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17829 16741 603 41 0 17788 0
vsize: 71316
[startup+1130.29 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 17006 0 0 0 112986 56 0 0 25 0 1 0 539794060 73293824 16829 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17894 16829 603 41 0 17853 0
vsize: 71576
[startup+1140.29 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 17084 0 0 0 113986 57 0 0 25 0 1 0 539794060 73695232 16907 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17992 16907 603 41 0 17951 0
vsize: 71968
[startup+1150.29 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 17300 0 0 0 114986 57 0 0 25 0 1 0 539794060 75579392 17123 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18452 17123 603 41 0 18411 0
vsize: 73808
[startup+1160.29 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 17451 0 0 0 115985 57 0 0 25 0 1 0 539794060 76120064 17274 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18584 17274 603 41 0 18543 0
vsize: 74336
[startup+1170.29 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 17516 0 0 0 116985 58 0 0 25 0 1 0 539794060 76525568 17339 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18683 17339 603 41 0 18642 0
vsize: 74732
[startup+1180.29 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 17564 0 0 0 117985 58 0 0 25 0 1 0 539794060 76656640 17387 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18715 17387 603 41 0 18674 0
vsize: 74860
[startup+1190.29 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 17611 0 0 0 118984 58 0 0 25 0 1 0 539794060 76791808 17434 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18748 17434 603 41 0 18707 0
vsize: 74992
[startup+1200.29 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22942
Raw data (stat): 22887 (minisat+) R 22886 28099 28098 0 -1 0 17661 0 0 0 119984 58 0 0 25 0 1 0 539794060 77062144 17484 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18814 17484 603 41 0 18773 0
vsize: 75256
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.33 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 22942
Raw data (stat): 22887 (minisat+) Z 22886 28099 28098 0 -1 12 17663 0 0 0 119984 62 0 0 25 0 1 0 539794060 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.33
CPU time (s): 1200.47
CPU user time (s): 1199.85
CPU system time (s): 0.620905
CPU usage (%): 100.012
Max. virtual memory (Kb): 75256
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####