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/submitted/een/normalized-p0548.opb
MD5SUM422c0da7d5380a26c4dac413428db5c9
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 14670
Optimality of the best value was proved NO
Number of terms in the objective function 416
Biggest coefficient in the objective function 11000
Number of bits for the biggest coefficient in the objective function 14
Sum of the numbers in the objective function 96797
Number of bits of the sum of numbers in the objective function 17
Biggest number in a constraint 11000
Number of bits of the biggest number in a constraint 14
Biggest sum of numbers in a constraint 96797
Number of bits of the biggest sum of numbers17
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1230.14
Number of variables527
Total number of constraints156
Number of constraints which are clauses40
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints116
Minimum length of a constraint2
Maximum length of a constraint134

Trace number 7155 

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        849744 kB
Buffers:         37192 kB
Cached:         125700 kB
SwapCached:       2144 kB
Active:          73436 kB
Inactive:        94476 kB
HighTotal:      131008 kB
HighFree:         1932 kB
LowTotal:       903652 kB
LowFree:        847812 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11364 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 22:01:55 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 5238 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 156 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................ss.ssssss.s.s.
c ---[ 125]---> BDD-cost:    3
c ---[ 124]---> BDD-cost:    3
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    3
c ---[ 119]---> BDD-cost:    3
c ---[ 118]---> BDD-cost:    3
c ---[ 117]---> BDD-cost:    3
c ---[ 116]---> BDD-cost:    3
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    3
c ---[ 113]---> BDD-cost:    3
c ---[ 112]---> BDD-cost:    3
c ---[ 111]---> BDD-cost:    3
c ---[ 110]---> BDD-cost:    3
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    3
c ---[ 107]---> BDD-cost:    3
c ---[ 106]---> BDD-cost:    3
c ---[ 105]---> BDD-cost:    3
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    5
c ---[ 102]---> BDD-cost:    8
c ---[ 101]---> BDD-cost:    6
c ---[ 100]---> BDD-cost:    8
c ---[  99]---> BDD-cost:    6
c ---[  98]---> BDD-cost:    7
c ---[  96]---> BDD-cost:   19
c ---[  93]---> BDD-cost:    8
c ---[  92]---> BDD-cost:   15
c ---[  91]---> BDD-cost:   15
c ---[  90]---> BDD-cost:    4
c ---[  89]---> BDD-cost:   24
c ---[  88]---> BDD-cost:   14
c ---[  87]---> BDD-cost:   12
c ---[  86]---> BDD-cost:   28
c ---[  85]---> BDD-cost:   13
c ---[  83]---> BDD-cost:    7
c ---[  82]---> BDD-cost:   14
c ---[  81]---> BDD-cost:    9
c ---[  80]---> BDD-cost:   25
c ---[  76]---> BDD-cost:   32
c ---[  75]---> BDD-cost:   10
c ---[  74]---> BDD-cost:   19
c ---[  72]---> BDD-cost:   24
c ---[  70]---> BDD-cost:   23
c ---[  69]---> BDD-cost:    8
c ---[  68]---> BDD-cost:   27
c ---[  67]---> BDD-cost:    9
c ---[  66]---> BDD-cost:   11
c ---[  65]---> BDD-cost:   56
c ---[  64]---> BDD-cost:   50
c ---[  63]---> BDD-cost:   20
c ---[  61]---> BDD-cost:   33
c ---[  60]---> BDD-cost:   12
c ---[  58]---> BDD-cost:    9
c ---[  57]---> BDD-cost:   34
c ---[  56]---> BDD-cost:   33
c ---[  55]---> BDD-cost:   23
c ---[  54]---> BDD-cost:   75
c ---[  53]---> BDD-cost:   24
c ---[  52]---> BDD-cost:   37
c ---[  51]---> BDD-cost:   37
c ---[  50]---> BDD-cost:   95
c ---[  49]---> BDD-cost:   11
c ---[  48]---> BDD-cost:  107
c ---[  47]---> BDD-cost:  115
c ---[  46]---> BDD-cost:  120
c ---[  45]---> BDD-cost:  104
c ---[  44]---> BDD-cost:   29
c ---[  43]---> BDD-cost:   51
c ---[  42]---> BDD-cost:   35
c ---[  41]---> BDD-cost:   24
c ---[  39]---> BDD-cost:   61
c ---[  38]---> BDD-cost:  109
c ---[  37]---> BDD-cost:  153
c ---[  36]---> BDD-cost:  120
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   25
c ---[  33]---> BDD-cost:  121
c ---[  32]---> BDD-cost:   32
c ---[  31]---> BDD-cost:   70
c ---[  30]---> BDD-cost:   56
c ---[  29]---> BDD-cost:   78
c ---[  28]---> BDD-cost:   84
c ---[  27]---> BDD-cost:   36
c ---[  26]---> BDD-cost:   91
c ---[  25]---> BDD-cost:   42
c ---[  23]---> BDD-cost:   39
c ---[  22]---> BDD-cost:  128
c ---[  21]---> BDD-cost:   61
c ---[  19]---> BDD-cost:   85
c ---[  18]---> BDD-cost:   55
c ---[  17]---> BDD-cost:   79
c ---[  16]---> BDD-cost: 1478
c ---[  15]---> BDD-cost:   26
c ---[  14]---> BDD-cost: 1140
c ---[  13]---> BDD-cost: 2534
c ---[  12]---> BDD-cost:   49
c ---[  11]---> BDD-cost:   49
c ---[  10]---> BDD-cost:142726
c ---[   9]---> BDD-cost:    2
c ---[   8]---> BDD-cost:    2
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:    2
c ---[   5]---> BDD-cost:    4
c ---[   4]---> BDD-cost:    7
c ---[   3]---> BDD-cost:    5
c ---[   2]---> BDD-cost:   11
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:   20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  444847  1328426 |  148282       0        0     nan |  0.000 % |
c |       100 |  440040  1315619 |  163110      89     1393    15.7 |  0.719 % |
c |       251 |  437753  1309903 |  179421     222     7790    35.1 |  1.351 % |
c |       476 |  437753  1309903 |  197363     447    24431    54.7 |  1.351 % |
c |       813 |  437753  1309903 |  217099     784    60564    77.2 |  1.351 % |
c |      1319 |  435873  1304493 |  238809    1259    77995    61.9 |  1.761 % |
c |      2078 |  434739  1301221 |  262690    1990   151621    76.2 |  2.026 % |
c |      3217 |  430155  1287857 |  288959    3086   328266   106.4 |  3.080 % |
c |      4925 |  427735  1280597 |  317855    4744   567203   119.6 |  3.614 % |
c ==============================================================================
c Found solution: 55123
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:109708     Base: 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5425 |  729348  1983598 |  243116    5147   622099   120.9 |  3.614 % |
c |      5526 |  727305  1977501 |  267427    5205   659897   126.8 |  2.717 % |
c |      5678 |  727305  1977501 |  294170    5357   665840   124.3 |  2.717 % |
c |      5903 |  726042  1973712 |  323587    5558   669509   120.5 |  2.882 % |
c |      6240 |  724470  1968996 |  355946    5831   676925   116.1 |  3.087 % |
c |      6746 |  724034  1967688 |  391540    6319   765507   121.1 |  3.145 % |
c |      7506 |  722684  1963638 |  430694    7045   941015   133.6 |  3.321 % |
c |      8645 |  720105  1955901 |  473764    8075  1034074   128.1 |  3.658 % |
c |     10353 |  719538  1954200 |  521140    9726  1253751   128.9 |  3.733 % |
c |     12915 |  712834  1934088 |  573254   11850  1385419   116.9 |  4.611 % |
c |     16759 |  707744  1918818 |  630580   15371  1947318   126.7 |  5.278 % |
c |     22528 |  698173  1890105 |  693638   20288  2483601   122.4 |  6.539 % |
c |     31178 |  695378  1881732 |  763002   28504  2975152   104.4 |  6.908 % |
c ==============================================================================
c Found solution: 38105
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32531 |  697233  1886435 |  232411   29857  3143595   105.3 |  6.908 % |
c |     32631 |  697233  1886435 |  255652   29957  3144255   105.0 |  6.880 % |
c |     32782 |  697233  1886435 |  281217   30108  3149145   104.6 |  6.880 % |
c |     33008 |  697233  1886435 |  309339   30334  3157812   104.1 |  6.880 % |
c |     33347 |  697233  1886435 |  340272   30673  3161819   103.1 |  6.880 % |
c |     33855 |  697233  1886435 |  374300   31181  3165702   101.5 |  6.880 % |
c |     34614 |  697224  1886408 |  411730   31931  3173280    99.4 |  6.881 % |
c |     35753 |  697224  1886408 |  452903   33070  3190765    96.5 |  6.881 % |
c |     37462 |  697191  1886309 |  498193   34763  3223962    92.7 |  6.885 % |
c |     40025 |  697191  1886309 |  548012   37326  3497670    93.7 |  6.885 % |
c |     43869 |  697191  1886309 |  602814   41170  3988612    96.9 |  6.885 % |
#### 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.91 0.95 0.90 2/54 10161
Raw data (stat): 10161 (runsolver) R 10160 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 429689583 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0018 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 13988 0 0 0 969 29 0 0 25 0 1 0 429689583 65056768 13045 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15883 13045 603 41 0 15842 0
vsize: 63532
[startup+20.0017 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 14053 0 0 0 1968 29 0 0 25 0 1 0 429689583 65323008 13110 4294967295 134512640 134672761 3221224560 3221223684 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15948 13110 603 41 0 15907 0
vsize: 63792
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 14174 0 0 0 2968 29 0 0 25 0 1 0 429689583 65798144 13231 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16064 13231 603 41 0 16023 0
vsize: 64256
[startup+40.0018 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 14225 0 0 0 3967 29 0 0 25 0 1 0 429689583 65933312 13282 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16097 13282 603 41 0 16056 0
vsize: 64388
[startup+50.0022 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 14361 0 0 0 4967 30 0 0 25 0 1 0 429689583 66613248 13418 4294967295 134512640 134672761 3221224560 3221223776 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16263 13418 603 41 0 16222 0
vsize: 65052
[startup+60.002 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 14488 0 0 0 5967 31 0 0 25 0 1 0 429689583 67010560 13545 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16360 13545 603 41 0 16319 0
vsize: 65440
[startup+70.0025 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 14529 0 0 0 6967 31 0 0 25 0 1 0 429689583 67293184 13586 4294967295 134512640 134672761 3221224560 3221223664 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16429 13586 603 41 0 16388 0
vsize: 65716
[startup+80.0027 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 14536 0 0 0 7967 31 0 0 25 0 1 0 429689583 67276800 13593 4294967295 134512640 134672761 3221224560 3221223664 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16425 13593 603 41 0 16384 0
vsize: 65700
[startup+90.0025 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 14599 0 0 0 8967 31 0 0 25 0 1 0 429689583 67538944 13656 4294967295 134512640 134672761 3221224560 3221223664 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16489 13656 603 41 0 16448 0
vsize: 65956
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 14601 0 0 0 9967 31 0 0 25 0 1 0 429689583 67538944 13658 4294967295 134512640 134672761 3221224560 3221223664 134560393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16489 13658 603 41 0 16448 0
vsize: 65956
[startup+110.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 14601 0 0 0 10967 31 0 0 25 0 1 0 429689583 67538944 13658 4294967295 134512640 134672761 3221224560 3221223664 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16489 13658 603 41 0 16448 0
vsize: 65956
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 14601 0 0 0 11967 31 0 0 25 0 1 0 429689583 67538944 13658 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16489 13658 603 41 0 16448 0
vsize: 65956
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 14601 0 0 0 12968 31 0 0 25 0 1 0 429689583 67538944 13658 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16489 13658 603 41 0 16448 0
vsize: 65956
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 14601 0 0 0 13968 31 0 0 25 0 1 0 429689583 67538944 13658 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16489 13658 603 41 0 16448 0
vsize: 65956
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 14605 0 0 0 14968 31 0 0 25 0 1 0 429689583 67538944 13662 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16489 13662 603 41 0 16448 0
vsize: 65956
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 14618 0 0 0 15968 31 0 0 25 0 1 0 429689583 67538944 13675 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16489 13675 603 41 0 16448 0
vsize: 65956
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 14686 0 0 0 16967 31 0 0 25 0 1 0 429689583 67932160 13743 4294967295 134512640 134672761 3221224560 3221223664 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16585 13743 603 41 0 16544 0
vsize: 66340
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 23388 0 0 0 17947 52 0 0 25 0 1 0 429689583 94564352 22115 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23087 22115 603 41 0 23046 0
vsize: 92348
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 23391 0 0 0 18947 52 0 0 25 0 1 0 429689583 94564352 22118 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23087 22118 603 41 0 23046 0
vsize: 92348
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 23436 0 0 0 19947 52 0 0 25 0 1 0 429689583 94834688 22163 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23153 22163 603 41 0 23112 0
vsize: 92612
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 23487 0 0 0 20947 52 0 0 25 0 1 0 429689583 94969856 22214 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23186 22214 603 41 0 23145 0
vsize: 92744
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 23494 0 0 0 21947 52 0 0 25 0 1 0 429689583 94969856 22221 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23186 22221 603 41 0 23145 0
vsize: 92744
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 23553 0 0 0 22947 52 0 0 25 0 1 0 429689583 95232000 22280 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23250 22280 603 41 0 23209 0
vsize: 93000
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 23678 0 0 0 23947 53 0 0 25 0 1 0 429689583 95780864 22405 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23384 22405 603 41 0 23343 0
vsize: 93536
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 23686 0 0 0 24947 53 0 0 25 0 1 0 429689583 95780864 22413 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23384 22413 603 41 0 23343 0
vsize: 93536
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 23701 0 0 0 25947 53 0 0 25 0 1 0 429689583 95911936 22428 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23416 22428 603 41 0 23375 0
vsize: 93664
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 23720 0 0 0 26948 53 0 0 25 0 1 0 429689583 95911936 22447 4294967295 134512640 134672761 3221224560 3221223664 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23416 22447 603 41 0 23375 0
vsize: 93664
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 23753 0 0 0 27947 53 0 0 25 0 1 0 429689583 96038912 22480 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23447 22480 603 41 0 23406 0
vsize: 93788
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 23794 0 0 0 28947 53 0 0 25 0 1 0 429689583 96292864 22521 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23509 22521 603 41 0 23468 0
vsize: 94036
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 23821 0 0 0 29948 53 0 0 25 0 1 0 429689583 96419840 22548 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23540 22548 603 41 0 23499 0
vsize: 94160
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 23862 0 0 0 30948 53 0 0 25 0 1 0 429689583 96546816 22589 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23571 22589 603 41 0 23530 0
vsize: 94284
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 23906 0 0 0 31948 54 0 0 25 0 1 0 429689583 96681984 22633 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23604 22633 603 41 0 23563 0
vsize: 94416
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 23980 0 0 0 32947 54 0 0 25 0 1 0 429689583 97079296 22707 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23701 22707 603 41 0 23660 0
vsize: 94804
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 23983 0 0 0 33948 54 0 0 25 0 1 0 429689583 97079296 22710 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23701 22710 603 41 0 23660 0
vsize: 94804
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 23984 0 0 0 34948 54 0 0 25 0 1 0 429689583 97079296 22711 4294967295 134512640 134672761 3221224560 3221223664 134560355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23701 22711 603 41 0 23660 0
vsize: 94804
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24046 0 0 0 35947 54 0 0 25 0 1 0 429689583 97349632 22773 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23767 22773 603 41 0 23726 0
vsize: 95068
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24083 0 0 0 36947 55 0 0 25 0 1 0 429689583 97480704 22810 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23799 22810 603 41 0 23758 0
vsize: 95196
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24095 0 0 0 37948 55 0 0 25 0 1 0 429689583 97480704 22822 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23799 22822 603 41 0 23758 0
vsize: 95196
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24163 0 0 0 38948 55 0 0 25 0 1 0 429689583 97742848 22890 4294967295 134512640 134672761 3221224560 3221223732 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23863 22890 603 41 0 23822 0
vsize: 95452
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24234 0 0 0 39948 55 0 0 25 0 1 0 429689583 98004992 22961 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23927 22961 603 41 0 23886 0
vsize: 95708
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24270 0 0 0 40948 55 0 0 25 0 1 0 429689583 98263040 22997 4294967295 134512640 134672761 3221224560 3221223732 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23990 22997 603 41 0 23949 0
vsize: 95960
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24296 0 0 0 41948 55 0 0 25 0 1 0 429689583 98263040 23023 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23990 23023 603 41 0 23949 0
vsize: 95960
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24315 0 0 0 42948 55 0 0 25 0 1 0 429689583 98398208 23042 4294967295 134512640 134672761 3221224560 3221223664 134560201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24023 23042 603 41 0 23982 0
vsize: 96092
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24325 0 0 0 43948 55 0 0 25 0 1 0 429689583 98398208 23052 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24023 23052 603 41 0 23982 0
vsize: 96092
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24335 0 0 0 44948 55 0 0 25 0 1 0 429689583 98516992 23062 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24052 23062 603 41 0 24011 0
vsize: 96208
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24360 0 0 0 45949 55 0 0 25 0 1 0 429689583 98516992 23087 4294967295 134512640 134672761 3221224560 3221223664 134560260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24052 23087 603 41 0 24011 0
vsize: 96208
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24388 0 0 0 46949 55 0 0 25 0 1 0 429689583 98652160 23115 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24085 23115 603 41 0 24044 0
vsize: 96340
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24422 0 0 0 47949 55 0 0 25 0 1 0 429689583 98770944 23149 4294967295 134512640 134672761 3221224560 3221223664 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24114 23149 603 41 0 24073 0
vsize: 96456
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24506 0 0 0 48949 55 0 0 25 0 1 0 429689583 99176448 23233 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24213 23233 603 41 0 24172 0
vsize: 96852
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24560 0 0 0 49949 56 0 0 25 0 1 0 429689583 99446784 23287 4294967295 134512640 134672761 3221224560 3221223776 134561990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24279 23287 603 41 0 24238 0
vsize: 97116
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24611 0 0 0 50948 56 0 0 25 0 1 0 429689583 99581952 23338 4294967295 134512640 134672761 3221224560 3221223664 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24312 23338 603 41 0 24271 0
vsize: 97248
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24662 0 0 0 51948 56 0 0 25 0 1 0 429689583 99868672 23389 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24382 23389 603 41 0 24341 0
vsize: 97528
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24689 0 0 0 52947 57 0 0 25 0 1 0 429689583 99852288 23416 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24378 23416 603 41 0 24337 0
vsize: 97512
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24702 0 0 0 53947 57 0 0 25 0 1 0 429689583 99979264 23429 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24409 23429 603 41 0 24368 0
vsize: 97636
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24759 0 0 0 54947 57 0 0 25 0 1 0 429689583 100237312 23486 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24472 23486 603 41 0 24431 0
vsize: 97888
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24807 0 0 0 55947 58 0 0 25 0 1 0 429689583 100470784 23534 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24529 23534 603 41 0 24488 0
vsize: 98116
[startup+570.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24819 0 0 0 56947 58 0 0 25 0 1 0 429689583 100470784 23546 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24529 23546 603 41 0 24488 0
vsize: 98116
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24852 0 0 0 57947 58 0 0 25 0 1 0 429689583 100589568 23579 4294967295 134512640 134672761 3221224560 3221223744 134558651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24558 23579 603 41 0 24517 0
vsize: 98232
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24882 0 0 0 58947 58 0 0 25 0 1 0 429689583 100728832 23609 4294967295 134512640 134672761 3221224560 3221223664 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24592 23609 603 41 0 24551 0
vsize: 98368
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24902 0 0 0 59947 58 0 0 25 0 1 0 429689583 100847616 23629 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24621 23629 603 41 0 24580 0
vsize: 98484
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24916 0 0 0 60948 58 0 0 25 0 1 0 429689583 100847616 23643 4294967295 134512640 134672761 3221224560 3221223664 134560184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24621 23643 603 41 0 24580 0
vsize: 98484
[startup+620.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24932 0 0 0 61948 58 0 0 25 0 1 0 429689583 100974592 23659 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24652 23659 603 41 0 24611 0
vsize: 98608
[startup+630.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24966 0 0 0 62948 58 0 0 25 0 1 0 429689583 101109760 23693 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24685 23693 603 41 0 24644 0
vsize: 98740
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 24990 0 0 0 63948 58 0 0 25 0 1 0 429689583 101244928 23717 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24718 23717 603 41 0 24677 0
vsize: 98872
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25010 0 0 0 64948 58 0 0 25 0 1 0 429689583 101244928 23737 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24718 23737 603 41 0 24677 0
vsize: 98872
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25016 0 0 0 65948 58 0 0 25 0 1 0 429689583 101244928 23743 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24718 23743 603 41 0 24677 0
vsize: 98872
[startup+670.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25030 0 0 0 66948 58 0 0 25 0 1 0 429689583 101376000 23757 4294967295 134512640 134672761 3221224560 3221223732 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24750 23757 603 41 0 24709 0
vsize: 99000
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25048 0 0 0 67949 58 0 0 25 0 1 0 429689583 101376000 23775 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24750 23775 603 41 0 24709 0
vsize: 99000
[startup+690.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25065 0 0 0 68949 58 0 0 25 0 1 0 429689583 101502976 23792 4294967295 134512640 134672761 3221224560 3221223664 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24781 23792 603 41 0 24740 0
vsize: 99124
[startup+700.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25076 0 0 0 69949 59 0 0 25 0 1 0 429689583 101502976 23803 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24781 23803 603 41 0 24740 0
vsize: 99124
[startup+710.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25102 0 0 0 70949 59 0 0 25 0 1 0 429689583 101621760 23829 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24810 23829 603 41 0 24769 0
vsize: 99240
[startup+720.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25124 0 0 0 71949 59 0 0 25 0 1 0 429689583 101752832 23851 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24842 23851 603 41 0 24801 0
vsize: 99368
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25182 0 0 0 72949 59 0 0 25 0 1 0 429689583 102014976 23909 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24906 23909 603 41 0 24865 0
vsize: 99624
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25211 0 0 0 73948 59 0 0 25 0 1 0 429689583 102154240 23938 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24940 23938 603 41 0 24899 0
vsize: 99760
[startup+750.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25232 0 0 0 74948 59 0 0 25 0 1 0 429689583 102154240 23959 4294967295 134512640 134672761 3221224560 3221223664 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24940 23959 603 41 0 24899 0
vsize: 99760
[startup+760.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25246 0 0 0 75948 60 0 0 25 0 1 0 429689583 102273024 23973 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24969 23973 603 41 0 24928 0
vsize: 99876
[startup+770.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25275 0 0 0 76948 60 0 0 25 0 1 0 429689583 102404096 24002 4294967295 134512640 134672761 3221224560 3221223768 134561960 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25001 24002 603 41 0 24960 0
vsize: 100004
[startup+780.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25281 0 0 0 77948 60 0 0 25 0 1 0 429689583 102404096 24008 4294967295 134512640 134672761 3221224560 3221223760 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25001 24008 603 41 0 24960 0
vsize: 100004
[startup+790.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25301 0 0 0 78948 60 0 0 25 0 1 0 429689583 102404096 24028 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25001 24028 603 41 0 24960 0
vsize: 100004
[startup+800.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25313 0 0 0 79948 60 0 0 25 0 1 0 429689583 102539264 24040 4294967295 134512640 134672761 3221224560 3221223664 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25034 24040 603 41 0 24993 0
vsize: 100136
[startup+810.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25325 0 0 0 80949 60 0 0 25 0 1 0 429689583 102539264 24052 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25034 24052 603 41 0 24993 0
vsize: 100136
[startup+820.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25398 0 0 0 81949 60 0 0 25 0 1 0 429689583 102809600 24125 4294967295 134512640 134672761 3221224560 3221223720 134561240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25100 24125 603 41 0 25059 0
vsize: 100400
[startup+830.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25430 0 0 0 82948 60 0 0 25 0 1 0 429689583 102944768 24157 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25133 24157 603 41 0 25092 0
vsize: 100532
[startup+840.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25450 0 0 0 83949 60 0 0 25 0 1 0 429689583 103079936 24177 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25166 24177 603 41 0 25125 0
vsize: 100664
[startup+850.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25485 0 0 0 84949 60 0 0 25 0 1 0 429689583 103219200 24212 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25200 24212 603 41 0 25159 0
vsize: 100800
[startup+860.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25529 0 0 0 85949 60 0 0 25 0 1 0 429689583 103354368 24256 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25233 24256 603 41 0 25192 0
vsize: 100932
[startup+870.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25670 0 0 0 86949 61 0 0 25 0 1 0 429689583 103895040 24397 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25365 24397 603 41 0 25324 0
vsize: 101460
[startup+880.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25773 0 0 0 87948 61 0 0 25 0 1 0 429689583 104300544 24500 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25464 24500 603 41 0 25423 0
vsize: 101856
[startup+890.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25843 0 0 0 88947 62 0 0 25 0 1 0 429689583 104566784 24570 4294967295 134512640 134672761 3221224560 3221223664 134560396 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25529 24570 603 41 0 25488 0
vsize: 102116
[startup+900.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 25901 0 0 0 89947 62 0 0 25 0 1 0 429689583 104824832 24628 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25592 24628 603 41 0 25551 0
vsize: 102368
[startup+910.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 26171 0 0 0 90946 63 0 0 25 0 1 0 429689583 105693184 24898 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25804 24898 603 41 0 25763 0
vsize: 103216
[startup+920.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 26228 0 0 0 91946 63 0 0 25 0 1 0 429689583 106090496 24955 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25901 24955 603 41 0 25860 0
vsize: 103604
[startup+930.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 26278 0 0 0 92947 63 0 0 25 0 1 0 429689583 106221568 25005 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25933 25005 603 41 0 25892 0
vsize: 103732
[startup+940.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 26320 0 0 0 93947 63 0 0 25 0 1 0 429689583 106467328 25047 4294967295 134512640 134672761 3221224560 3221223760 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25993 25047 603 41 0 25952 0
vsize: 103972
[startup+950.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 26380 0 0 0 94947 63 0 0 25 0 1 0 429689583 106602496 25107 4294967295 134512640 134672761 3221224560 3221223664 134560335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26026 25107 603 41 0 25985 0
vsize: 104104
[startup+960.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 26484 0 0 0 95947 64 0 0 25 0 1 0 429689583 107139072 25211 4294967295 134512640 134672761 3221224560 3221223664 134559991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26157 25211 603 41 0 26116 0
vsize: 104628
[startup+970.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 26511 0 0 0 96947 64 0 0 25 0 1 0 429689583 107139072 25238 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26157 25238 603 41 0 26116 0
vsize: 104628
[startup+980.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 26529 0 0 0 97947 64 0 0 25 0 1 0 429689583 107270144 25256 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26189 25256 603 41 0 26148 0
vsize: 104756
[startup+990.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 26567 0 0 0 98947 64 0 0 25 0 1 0 429689583 107405312 25294 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26222 25294 603 41 0 26181 0
vsize: 104888
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 26612 0 0 0 99947 64 0 0 25 0 1 0 429689583 107675648 25339 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26288 25339 603 41 0 26247 0
vsize: 105152
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 26661 0 0 0 100947 64 0 0 25 0 1 0 429689583 107814912 25388 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26322 25388 603 41 0 26281 0
vsize: 105288
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 26703 0 0 0 101947 64 0 0 25 0 1 0 429689583 107945984 25430 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26354 25430 603 41 0 26313 0
vsize: 105416
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 26741 0 0 0 102947 64 0 0 25 0 1 0 429689583 108081152 25468 4294967295 134512640 134672761 3221224560 3221223664 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26387 25468 603 41 0 26346 0
vsize: 105548
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 26783 0 0 0 103947 64 0 0 25 0 1 0 429689583 108351488 25510 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26453 25510 603 41 0 26412 0
vsize: 105812
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 26816 0 0 0 104947 64 0 0 25 0 1 0 429689583 108498944 25543 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26489 25543 603 41 0 26448 0
vsize: 105956
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 26861 0 0 0 105948 64 0 0 25 0 1 0 429689583 108638208 25588 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26523 25588 603 41 0 26482 0
vsize: 106092
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 26924 0 0 0 106948 64 0 0 25 0 1 0 429689583 108908544 25651 4294967295 134512640 134672761 3221224560 3221223664 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26589 25651 603 41 0 26548 0
vsize: 106356
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 26959 0 0 0 107948 64 0 0 25 0 1 0 429689583 109047808 25686 4294967295 134512640 134672761 3221224560 3221223664 134560313 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26623 25686 603 41 0 26582 0
vsize: 106492
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10161
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 26981 0 0 0 108948 64 0 0 25 0 1 0 429689583 109047808 25708 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26623 25708 603 41 0 26582 0
vsize: 106492
[startup+1100.02 s]
Raw data (loadavg): 1.15 1.00 0.92 2/54 10214
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 26991 0 0 0 109946 67 0 0 25 0 1 0 429689583 109182976 25718 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26656 25718 603 41 0 26615 0
vsize: 106624
[startup+1110.02 s]
Raw data (loadavg): 1.12 1.00 0.92 2/54 10214
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 27007 0 0 0 110946 67 0 0 25 0 1 0 429689583 109182976 25734 4294967295 134512640 134672761 3221224560 3221223664 134560352 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26656 25734 603 41 0 26615 0
vsize: 106624
[startup+1120.02 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 10214
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 27059 0 0 0 111945 68 0 0 25 0 1 0 429689583 109453312 25786 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26722 25786 603 41 0 26681 0
vsize: 106888
[startup+1130.02 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 10214
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 27090 0 0 0 112945 68 0 0 25 0 1 0 429689583 109592576 25817 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26756 25817 603 41 0 26715 0
vsize: 107024
[startup+1140.02 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 10214
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 27137 0 0 0 113945 68 0 0 25 0 1 0 429689583 109723648 25864 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26788 25864 603 41 0 26747 0
vsize: 107152
[startup+1150.02 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 10214
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 27157 0 0 0 114945 68 0 0 25 0 1 0 429689583 109858816 25884 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26821 25884 603 41 0 26780 0
vsize: 107284
[startup+1160.02 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 10214
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 27177 0 0 0 115945 68 0 0 25 0 1 0 429689583 109858816 25904 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26821 25904 603 41 0 26780 0
vsize: 107284
[startup+1170.02 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 10216
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 27213 0 0 0 116945 68 0 0 25 0 1 0 429689583 109985792 25940 4294967295 134512640 134672761 3221224560 3221223664 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26852 25940 603 41 0 26811 0
vsize: 107408
[startup+1180.02 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 10216
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 27366 0 0 0 117945 69 0 0 25 0 1 0 429689583 110661632 26093 4294967295 134512640 134672761 3221224560 3221223760 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27017 26093 603 41 0 26976 0
vsize: 108068
[startup+1190.02 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 10216
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 27552 0 0 0 118945 69 0 0 25 0 1 0 429689583 111464448 26279 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27213 26279 603 41 0 27172 0
vsize: 108852
[startup+1200.02 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 10216
Raw data (stat): 10161 (minisat+) R 10160 29151 29150 0 -1 0 27774 0 0 0 119944 70 0 0 25 0 1 0 429689583 112275456 26501 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27411 26501 603 41 0 27370 0
vsize: 109644
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.03 1.00 0.92 1/54 10216
Raw data (stat): 10161 (minisat+) Z 10160 29151 29150 0 -1 12 27777 0 0 0 119944 75 0 0 25 0 1 0 429689583 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.2
CPU user time (s): 1199.45
CPU system time (s): 0.755885
CPU usage (%): 100.011
Max. virtual memory (Kb): 109644
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####