Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namenormalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-p0548.opb
MD5SUM6f47095f2d417d23ced995954e641689
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 15249
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 benchmark1236.38
Number of variables548
Total number of constraints724
Number of constraints which are clauses40
Number of constraints which are cardinality constraints (but not clauses)550
Number of constraints which are nor clauses,nor cardinality constraints134
Minimum length of a constraint1
Maximum length of a constraint143

Trace number 19008 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-21 17:24:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17160 boxname=wulflinc15 idbench=1320 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6f47095f2d417d23ced995954e641689  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-p0548.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-p0548.opb /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-p0548.opb
IDLAUNCH: 17160
/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:        583636 kB
Buffers:         32020 kB
Cached:         397164 kB
SwapCached:        440 kB
Active:          69540 kB
Inactive:       361832 kB
HighTotal:      131008 kB
HighFree:          616 kB
LowTotal:       903652 kB
LowFree:        583020 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5360 kB
Slab:            14020 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 17:45:00 (client local time) WITH STATUS 0 IN 1200.16 SECONDS
stats: 17160 7 1200.16 0
#### 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): ssss.s..ssss........................................
c ---[ 164]---> BDD-cost:   12
c ---[ 163]---> BDD-cost:   46
c ---[ 162]---> BDD-cost:   27
c ---[ 161]---> BDD-cost:    8
c ---[ 160]---> BDD-cost:   48
c ---[ 159]---> BDD-cost:    7
c ---[ 157]---> BDD-cost:   75
c ---[ 156]---> BDD-cost:   23
c ---[ 154]---> BDD-cost:   54
c ---[ 153]---> BDD-cost:    8
c ---[ 152]---> BDD-cost:  105
c ---[ 151]---> BDD-cost:  104
c ---[ 150]---> BDD-cost:  120
c ---[ 149]---> BDD-cost:   79
c ---[ 148]---> BDD-cost:   19
c ---[ 147]---> BDD-cost:  115
c ---[ 146]---> BDD-cost:  107
c ---[ 145]---> BDD-cost:   11
c ---[ 144]---> BDD-cost:   55
c ---[ 143]---> BDD-cost:   87
c ---[ 142]---> BDD-cost:   54
c ---[ 141]---> BDD-cost:  164
c ---[ 140]---> BDD-cost:  151
c ---[ 139]---> BDD-cost:   31
c ---[ 138]---> BDD-cost:   26
c ---[ 136]---> BDD-cost:   28
c ---[ 135]---> BDD-cost:   77
c ---[ 134]---> BDD-cost:  153
c ---[ 133]---> BDD-cost:  109
c ---[ 131]---> BDD-cost:  137
c ---[ 130]---> BDD-cost:    6
c ---[ 129]---> BDD-cost:   56
c ---[ 128]---> BDD-cost:   23
c ---[ 127]---> BDD-cost:    7
c ---[ 126]---> BDD-cost:   32
c ---[ 125]---> BDD-cost:   15
c ---[ 123]---> BDD-cost:   14
c ---[ 121]---> BDD-cost:   10
c ---[ 120]---> BDD-cost:   19
c ---[ 119]---> BDD-cost:   12
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:   24
c ---[ 116]---> BDD-cost:   11
c ---[ 115]---> BDD-cost:    9
c ---[ 114]---> BDD-cost:   29
c ---[ 112]---> BDD-cost:    6
c ---[ 111]---> BDD-cost:   21
c ---[ 110]---> BDD-cost:   29
c ---[ 109]---> BDD-cost:   51
c ---[ 107]---> BDD-cost:    8
c ---[ 106]---> BDD-cost:   35
c ---[ 105]---> BDD-cost:   24
c ---[ 104]---> BDD-cost:   12
c ---[ 103]---> BDD-cost:   16
c ---[ 102]---> BDD-cost:   29
c ---[ 101]---> BDD-cost:   13
c ---[ 100]---> BDD-cost:   49
c ---[  99]---> BDD-cost:   60
c ---[  98]---> BDD-cost:    7
c ---[  97]---> BDD-cost:   12
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:   16
c ---[  93]---> BDD-cost:   68
c ---[  92]---> BDD-cost:   78
c ---[  91]---> BDD-cost:   47
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:   68
c ---[  88]---> BDD-cost:    8
c ---[  87]---> BDD-cost:   20
c ---[  86]---> BDD-cost:   18
c ---[  83]---> BDD-cost:   10
c ---[  81]---> BDD-cost:   12
c ---[  80]---> Adder-cost: 750   maxlim: 2650   bits: 13/12
c ---[  79]---> Sorter-cost: 1212     Base: 2 3 2 3
c ---[  78]---> Adder-cost: 171   maxlim: 103   bits: 8/7
c ---[  77]---> Adder-cost: 190   maxlim: 736   bits: 10/10
c ---[  76]---> BDD-cost:   37
c ---[  75]---> BDD-cost:    3
c ---[  73]---> BDD-cost:    3
c ---[  71]---> BDD-cost:    3
c ---[  69]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  59]---> BDD-cost:    3
c ---[  57]---> BDD-cost:    3
c ---[  55]---> BDD-cost:    3
c ---[  53]---> BDD-cost:    3
c ---[  47]---> BDD-cost:    3
c ---[  41]---> BDD-cost:    3
c ---[  33]---> BDD-cost:    3
c ---[  31]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    3
c ---[  27]---> BDD-cost:    3
c ---[  25]---> BDD-cost:    3
c ---[  23]---> BDD-cost:    3
c ---[  21]---> BDD-cost:    3
c ---[  19]---> BDD-cost:    3
c ---[  17]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  13]---> BDD-cost:   49
c ---[  12]---> BDD-cost:   49
c ---[  11]---> BDD-cost:   26
c ---[  10]---> BDD-cost:    5
c ---[   9]---> BDD-cost:    7
c ---[   8]---> BDD-cost:    9
c ---[   7]---> BDD-cost:   11
c ---[   6]---> BDD-cost:    5
c ---[   5]---> BDD-cost:   20
c ---[   4]---> BDD-cost:    4
c ---[   3]---> BDD-cost:    2
c ---[   2]---> BDD-cost:    9
c ---[   1]---> BDD-cost:    2
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   24239    72664 |    8079       0        0     nan |  0.000 % |
c |       100 |   24204    72543 |    8886      94      630     6.7 |  2.627 % |
c |       250 |   24204    72543 |    9775     244     1500     6.1 |  2.627 % |
c |       475 |   24168    72424 |   10753     463     3762     8.1 |  2.700 % |
c |       812 |   24147    72351 |   11828     793     6573     8.3 |  2.736 % |
c |      1318 |   24094    72172 |   13011    1287    11505     8.9 |  2.845 % |
c |      2077 |   24070    72093 |   14312    2044    36065    17.6 |  2.881 % |
c |      3216 |   24070    72093 |   15743    3183    66248    20.8 |  2.881 % |
c |      4924 |   24070    72093 |   17318    4891   129432    26.5 |  2.881 % |
c |      7486 |   24046    72024 |   19049    7452   225412    30.2 |  2.917 % |
c |     11330 |   24030    71968 |   20954   11293   381242    33.8 |  2.953 % |
c |     17096 |   24024    71948 |   23050   17058   532868    31.2 |  2.972 % |
c |     25746 |   24024    71948 |   25355   13467   596053    44.3 |  2.972 % |
c |     38720 |   24024    71948 |   27890   13378   350688    26.2 |  2.972 % |
c |     58184 |   24024    71948 |   30679   17530   691331    39.4 |  2.972 % |
c |     87376 |   24024    71948 |   33747   27765   906272    32.6 |  2.972 % |
c |    131165 |   24016    71928 |   37122   30146  1168742    38.8 |  3.008 % |
c |    196849 |   24016    71928 |   40835   26633   994072    37.3 |  3.008 % |
c |    295375 |   24016    71928 |   44918   22515   781186    34.7 |  3.008 % |
c |    443166 |   23998    71874 |   49410   21696   804926    37.1 |  3.080 % |
c |    664849 |   23994    71864 |   54351   37767  1328360    35.2 |  3.099 % |
#### 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.85 0.96 0.91 2/54 11482
Raw data (stat): 11482 (runsolver) R 11481 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488635556 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.001 s]
Raw data (loadavg): 0.87 0.96 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 1821 0 0 0 995 2 0 0 25 0 1 0 488635556 9052160 1788 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2210 1788 603 41 0 2169 0
vsize: 8840
[startup+20.0016 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 2098 0 0 0 1994 3 0 0 25 0 1 0 488635556 10248192 2065 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2502 2065 603 41 0 2461 0
vsize: 10008
[startup+30.0015 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 2183 0 0 0 2993 4 0 0 25 0 1 0 488635556 10514432 2150 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2567 2150 603 41 0 2526 0
vsize: 10268
[startup+40.0014 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 2301 0 0 0 3993 4 0 0 25 0 1 0 488635556 11051008 2268 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2698 2268 603 41 0 2657 0
vsize: 10792
[startup+50.0015 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 2493 0 0 0 4993 5 0 0 25 0 1 0 488635556 11849728 2460 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2893 2460 603 41 0 2852 0
vsize: 11572
[startup+60.002 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 2503 0 0 0 5993 5 0 0 25 0 1 0 488635556 11849728 2470 4294967295 134512640 134672761 3221224544 3221223612 1075346603 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2893 2470 603 41 0 2852 0
vsize: 11572
[startup+70.002 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 2521 0 0 0 6993 5 0 0 25 0 1 0 488635556 11997184 2488 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2929 2488 603 41 0 2888 0
vsize: 11716
[startup+80.0023 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 2613 0 0 0 7992 5 0 0 25 0 1 0 488635556 12529664 2580 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3059 2580 603 41 0 3018 0
vsize: 12236
[startup+90.0024 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 2661 0 0 0 8992 5 0 0 25 0 1 0 488635556 12664832 2628 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3092 2628 603 41 0 3051 0
vsize: 12368
[startup+100.002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 2701 0 0 0 9992 5 0 0 25 0 1 0 488635556 12943360 2668 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3160 2668 603 41 0 3119 0
vsize: 12640
[startup+110.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 2870 0 0 0 10992 6 0 0 25 0 1 0 488635556 13619200 2837 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3325 2837 603 41 0 3284 0
vsize: 13300
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3064 0 0 0 11991 7 0 0 25 0 1 0 488635556 14438400 3031 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3525 3031 603 41 0 3484 0
vsize: 14100
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3064 0 0 0 12991 7 0 0 25 0 1 0 488635556 14438400 3031 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3525 3031 603 41 0 3484 0
vsize: 14100
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3076 0 0 0 13991 7 0 0 25 0 1 0 488635556 14438400 3043 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3525 3043 603 41 0 3484 0
vsize: 14100
[startup+150.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3076 0 0 0 14992 7 0 0 25 0 1 0 488635556 14438400 3043 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3525 3043 603 41 0 3484 0
vsize: 14100
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3077 0 0 0 15992 7 0 0 25 0 1 0 488635556 14438400 3044 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3525 3044 603 41 0 3484 0
vsize: 14100
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3083 0 0 0 16992 7 0 0 25 0 1 0 488635556 14438400 3050 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3525 3050 603 41 0 3484 0
vsize: 14100
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3122 0 0 0 17992 7 0 0 25 0 1 0 488635556 14716928 3089 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3593 3089 603 41 0 3552 0
vsize: 14372
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3146 0 0 0 18992 8 0 0 25 0 1 0 488635556 14716928 3113 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3593 3113 603 41 0 3552 0
vsize: 14372
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3169 0 0 0 19992 8 0 0 25 0 1 0 488635556 14876672 3136 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3632 3136 603 41 0 3591 0
vsize: 14528
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3268 0 0 0 20992 8 0 0 25 0 1 0 488635556 15273984 3235 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3729 3235 603 41 0 3688 0
vsize: 14916
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3284 0 0 0 21992 8 0 0 25 0 1 0 488635556 15421440 3251 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3765 3251 603 41 0 3724 0
vsize: 15060
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3299 0 0 0 22993 8 0 0 25 0 1 0 488635556 15421440 3266 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3765 3266 603 41 0 3724 0
vsize: 15060
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3306 0 0 0 23993 8 0 0 25 0 1 0 488635556 15585280 3273 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3805 3273 603 41 0 3764 0
vsize: 15220
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3312 0 0 0 24993 8 0 0 25 0 1 0 488635556 15585280 3279 4294967295 134512640 134672761 3221224544 3221223648 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3805 3279 603 41 0 3764 0
vsize: 15220
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3329 0 0 0 25993 8 0 0 25 0 1 0 488635556 15585280 3296 4294967295 134512640 134672761 3221224544 3221223648 134560267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3805 3296 603 41 0 3764 0
vsize: 15220
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3338 0 0 0 26993 8 0 0 25 0 1 0 488635556 15749120 3305 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3845 3305 603 41 0 3804 0
vsize: 15380
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3365 0 0 0 27993 8 0 0 25 0 1 0 488635556 15912960 3332 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3885 3332 603 41 0 3844 0
vsize: 15540
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3367 0 0 0 28994 8 0 0 25 0 1 0 488635556 15912960 3334 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3885 3334 603 41 0 3844 0
vsize: 15540
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3367 0 0 0 29994 8 0 0 25 0 1 0 488635556 15912960 3334 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3885 3334 603 41 0 3844 0
vsize: 15540
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3367 0 0 0 30994 8 0 0 25 0 1 0 488635556 15912960 3334 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3885 3334 603 41 0 3844 0
vsize: 15540
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3368 0 0 0 31994 8 0 0 25 0 1 0 488635556 15912960 3335 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3885 3335 603 41 0 3844 0
vsize: 15540
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3380 0 0 0 32993 8 0 0 25 0 1 0 488635556 15912960 3347 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3885 3347 603 41 0 3844 0
vsize: 15540
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3392 0 0 0 33993 8 0 0 25 0 1 0 488635556 16076800 3359 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3925 3359 603 41 0 3884 0
vsize: 15700
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3572 0 0 0 34993 9 0 0 25 0 1 0 488635556 16748544 3539 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4089 3539 603 41 0 4048 0
vsize: 16356
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3623 0 0 0 35993 9 0 0 25 0 1 0 488635556 17018880 3590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3590 603 41 0 4114 0
vsize: 16620
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3631 0 0 0 36993 9 0 0 25 0 1 0 488635556 17018880 3598 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3598 603 41 0 4114 0
vsize: 16620
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3655 0 0 0 37993 9 0 0 25 0 1 0 488635556 17182720 3622 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4195 3622 603 41 0 4154 0
vsize: 16780
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3694 0 0 0 38993 9 0 0 25 0 1 0 488635556 17346560 3661 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4235 3661 603 41 0 4194 0
vsize: 16940
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3736 0 0 0 39993 9 0 0 25 0 1 0 488635556 17477632 3703 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4267 3703 603 41 0 4226 0
vsize: 17068
[startup+410.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3742 0 0 0 40993 10 0 0 25 0 1 0 488635556 17477632 3709 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4267 3709 603 41 0 4226 0
vsize: 17068
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3746 0 0 0 41993 10 0 0 25 0 1 0 488635556 17477632 3713 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4267 3713 603 41 0 4226 0
vsize: 17068
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3766 0 0 0 42993 10 0 0 25 0 1 0 488635556 17620992 3733 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4302 3733 603 41 0 4261 0
vsize: 17208
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3806 0 0 0 43994 10 0 0 25 0 1 0 488635556 17752064 3773 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4334 3773 603 41 0 4293 0
vsize: 17336
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3817 0 0 0 44994 10 0 0 25 0 1 0 488635556 17899520 3784 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4370 3784 603 41 0 4329 0
vsize: 17480
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3837 0 0 0 45994 10 0 0 25 0 1 0 488635556 17899520 3804 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4370 3804 603 41 0 4329 0
vsize: 17480
[startup+470.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 3982 0 0 0 46994 10 0 0 25 0 1 0 488635556 18567168 3949 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4533 3949 603 41 0 4492 0
vsize: 18132
[startup+480.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4209 0 0 0 47993 11 0 0 25 0 1 0 488635556 19492864 4176 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4759 4176 603 41 0 4718 0
vsize: 19036
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4212 0 0 0 48993 11 0 0 25 0 1 0 488635556 19492864 4179 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4759 4179 603 41 0 4718 0
vsize: 19036
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4212 0 0 0 49993 11 0 0 25 0 1 0 488635556 19492864 4179 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4759 4179 603 41 0 4718 0
vsize: 19036
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4230 0 0 0 50993 11 0 0 25 0 1 0 488635556 19648512 4197 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4797 4197 603 41 0 4756 0
vsize: 19188
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4257 0 0 0 51993 11 0 0 25 0 1 0 488635556 19648512 4224 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4797 4224 603 41 0 4756 0
vsize: 19188
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4330 0 0 0 52993 12 0 0 25 0 1 0 488635556 20062208 4297 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4297 603 41 0 4857 0
vsize: 19592
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4350 0 0 0 53992 12 0 0 25 0 1 0 488635556 20062208 4317 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4898 4317 603 41 0 4857 0
vsize: 19592
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4350 0 0 0 54992 12 0 0 25 0 1 0 488635556 20062208 4317 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4317 603 41 0 4857 0
vsize: 19592
[startup+560.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4368 0 0 0 55992 12 0 0 25 0 1 0 488635556 20213760 4335 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4935 4335 603 41 0 4894 0
vsize: 19740
[startup+570.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4403 0 0 0 56993 12 0 0 25 0 1 0 488635556 20377600 4370 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4975 4370 603 41 0 4934 0
vsize: 19900
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4409 0 0 0 57993 12 0 0 25 0 1 0 488635556 20377600 4376 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4975 4376 603 41 0 4934 0
vsize: 19900
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4431 0 0 0 58993 12 0 0 25 0 1 0 488635556 20541440 4398 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5015 4398 603 41 0 4974 0
vsize: 20060
[startup+600.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4447 0 0 0 59993 12 0 0 25 0 1 0 488635556 20541440 4414 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5015 4414 603 41 0 4974 0
vsize: 20060
[startup+610.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4487 0 0 0 60993 12 0 0 25 0 1 0 488635556 20738048 4454 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5063 4454 603 41 0 5022 0
vsize: 20252
[startup+620.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4510 0 0 0 61993 13 0 0 25 0 1 0 488635556 20934656 4477 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5111 4477 603 41 0 5070 0
vsize: 20444
[startup+630.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4521 0 0 0 62993 13 0 0 25 0 1 0 488635556 20934656 4488 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5111 4488 603 41 0 5070 0
vsize: 20444
[startup+640.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4521 0 0 0 63993 13 0 0 25 0 1 0 488635556 20934656 4488 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5111 4488 603 41 0 5070 0
vsize: 20444
[startup+650.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4521 0 0 0 64993 13 0 0 25 0 1 0 488635556 20934656 4488 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5111 4488 603 41 0 5070 0
vsize: 20444
[startup+660.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4533 0 0 0 65993 13 0 0 25 0 1 0 488635556 20934656 4500 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5111 4500 603 41 0 5070 0
vsize: 20444
[startup+670.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4534 0 0 0 66994 13 0 0 25 0 1 0 488635556 20934656 4501 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5111 4501 603 41 0 5070 0
vsize: 20444
[startup+680.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4534 0 0 0 67994 13 0 0 25 0 1 0 488635556 20934656 4501 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5111 4501 603 41 0 5070 0
vsize: 20444
[startup+690.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4534 0 0 0 68994 13 0 0 25 0 1 0 488635556 20934656 4501 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5111 4501 603 41 0 5070 0
vsize: 20444
[startup+700.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4587 0 0 0 69994 13 0 0 25 0 1 0 488635556 21204992 4554 4294967295 134512640 134672761 3221224544 3221223712 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5177 4554 603 41 0 5136 0
vsize: 20708
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4639 0 0 0 70994 13 0 0 25 0 1 0 488635556 21516288 4606 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5253 4606 603 41 0 5212 0
vsize: 21012
[startup+720.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4658 0 0 0 71994 13 0 0 25 0 1 0 488635556 21516288 4625 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5253 4625 603 41 0 5212 0
vsize: 21012
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4681 0 0 0 72995 13 0 0 25 0 1 0 488635556 21680128 4648 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5293 4648 603 41 0 5252 0
vsize: 21172
[startup+740.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4702 0 0 0 73995 13 0 0 25 0 1 0 488635556 21872640 4669 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5340 4669 603 41 0 5299 0
vsize: 21360
[startup+750.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4704 0 0 0 74995 13 0 0 25 0 1 0 488635556 21872640 4671 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5340 4671 603 41 0 5299 0
vsize: 21360
[startup+760.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4704 0 0 0 75995 13 0 0 25 0 1 0 488635556 21872640 4671 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5340 4671 603 41 0 5299 0
vsize: 21360
[startup+770.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4704 0 0 0 76995 13 0 0 25 0 1 0 488635556 21872640 4671 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5340 4671 603 41 0 5299 0
vsize: 21360
[startup+780.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4710 0 0 0 77995 13 0 0 25 0 1 0 488635556 21872640 4677 4294967295 134512640 134672761 3221224544 3221223728 134559532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5340 4677 603 41 0 5299 0
vsize: 21360
[startup+790.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4712 0 0 0 78995 13 0 0 25 0 1 0 488635556 21872640 4679 4294967295 134512640 134672761 3221224544 3221223728 134559045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5340 4679 603 41 0 5299 0
vsize: 21360
[startup+800.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4712 0 0 0 79996 13 0 0 25 0 1 0 488635556 21872640 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5340 4679 603 41 0 5299 0
vsize: 21360
[startup+810.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4723 0 0 0 80996 13 0 0 25 0 1 0 488635556 21872640 4690 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5340 4690 603 41 0 5299 0
vsize: 21360
[startup+820.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4723 0 0 0 81996 13 0 0 25 0 1 0 488635556 21872640 4690 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5340 4690 603 41 0 5299 0
vsize: 21360
[startup+830.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4725 0 0 0 82996 13 0 0 25 0 1 0 488635556 21872640 4692 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5340 4692 603 41 0 5299 0
vsize: 21360
[startup+840.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4725 0 0 0 83996 13 0 0 25 0 1 0 488635556 21872640 4692 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5340 4692 603 41 0 5299 0
vsize: 21360
[startup+850.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4735 0 0 0 84996 13 0 0 25 0 1 0 488635556 22036480 4702 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5380 4702 603 41 0 5339 0
vsize: 21520
[startup+860.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4737 0 0 0 85996 13 0 0 25 0 1 0 488635556 22036480 4704 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5380 4704 603 41 0 5339 0
vsize: 21520
[startup+870.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4909 0 0 0 86995 14 0 0 25 0 1 0 488635556 22704128 4876 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5543 4876 603 41 0 5502 0
vsize: 22172
[startup+880.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4909 0 0 0 87996 14 0 0 25 0 1 0 488635556 22704128 4876 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5543 4876 603 41 0 5502 0
vsize: 22172
[startup+890.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4909 0 0 0 88995 14 0 0 25 0 1 0 488635556 22704128 4876 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5543 4876 603 41 0 5502 0
vsize: 22172
[startup+900.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4909 0 0 0 89995 14 0 0 25 0 1 0 488635556 22704128 4876 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5543 4876 603 41 0 5502 0
vsize: 22172
[startup+910.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 4934 0 0 0 90995 14 0 0 25 0 1 0 488635556 22704128 4901 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5543 4901 603 41 0 5502 0
vsize: 22172
[startup+920.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 5284 0 0 0 91994 15 0 0 25 0 1 0 488635556 24174592 5251 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5902 5251 603 41 0 5861 0
vsize: 23608
[startup+930.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 5290 0 0 0 92995 15 0 0 25 0 1 0 488635556 24174592 5257 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5902 5257 603 41 0 5861 0
vsize: 23608
[startup+940.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 5290 0 0 0 93995 15 0 0 25 0 1 0 488635556 24174592 5257 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5902 5257 603 41 0 5861 0
vsize: 23608
[startup+950.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 5290 0 0 0 94995 15 0 0 25 0 1 0 488635556 24174592 5257 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5902 5257 603 41 0 5861 0
vsize: 23608
[startup+960.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 5290 0 0 0 95995 15 0 0 25 0 1 0 488635556 24174592 5257 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5902 5257 603 41 0 5861 0
vsize: 23608
[startup+970.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 5616 0 0 0 96995 15 0 0 25 0 1 0 488635556 25513984 5583 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6229 5583 603 41 0 6188 0
vsize: 24916
[startup+980.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 5909 0 0 0 97994 16 0 0 25 0 1 0 488635556 26730496 5876 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6526 5876 603 41 0 6485 0
vsize: 26104
[startup+990.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 5964 0 0 0 98994 17 0 0 25 0 1 0 488635556 27004928 5931 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6593 5931 603 41 0 6552 0
vsize: 26372
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 5970 0 0 0 99994 17 0 0 25 0 1 0 488635556 27004928 5937 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6593 5937 603 41 0 6552 0
vsize: 26372
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 5970 0 0 0 100994 17 0 0 25 0 1 0 488635556 27004928 5937 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6593 5937 603 41 0 6552 0
vsize: 26372
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 5982 0 0 0 101994 17 0 0 25 0 1 0 488635556 27148288 5949 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6628 5949 603 41 0 6587 0
vsize: 26512
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 5984 0 0 0 102995 17 0 0 25 0 1 0 488635556 27148288 5951 4294967295 134512640 134672761 3221224544 3221223728 134559385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6628 5951 603 41 0 6587 0
vsize: 26512
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 5991 0 0 0 103995 17 0 0 25 0 1 0 488635556 27148288 5958 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6628 5958 603 41 0 6587 0
vsize: 26512
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 5991 0 0 0 104995 17 0 0 25 0 1 0 488635556 27148288 5958 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6628 5958 603 41 0 6587 0
vsize: 26512
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 6000 0 0 0 105995 17 0 0 25 0 1 0 488635556 27148288 5967 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6628 5967 603 41 0 6587 0
vsize: 26512
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 6001 0 0 0 106995 17 0 0 25 0 1 0 488635556 27148288 5968 4294967295 134512640 134672761 3221224544 3221223776 134557473 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6628 5968 603 41 0 6587 0
vsize: 26512
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 6001 0 0 0 107995 17 0 0 25 0 1 0 488635556 27148288 5968 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6628 5968 603 41 0 6587 0
vsize: 26512
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 6011 0 0 0 108996 17 0 0 25 0 1 0 488635556 27344896 5978 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6676 5978 603 41 0 6635 0
vsize: 26704
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 6012 0 0 0 109996 17 0 0 25 0 1 0 488635556 27344896 5979 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6676 5979 603 41 0 6635 0
vsize: 26704
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 6012 0 0 0 110996 17 0 0 25 0 1 0 488635556 27344896 5979 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6676 5979 603 41 0 6635 0
vsize: 26704
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 6012 0 0 0 111996 17 0 0 25 0 1 0 488635556 27344896 5979 4294967295 134512640 134672761 3221224544 3221223728 134559594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6676 5979 603 41 0 6635 0
vsize: 26704
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 6012 0 0 0 112996 17 0 0 25 0 1 0 488635556 27344896 5979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6676 5979 603 41 0 6635 0
vsize: 26704
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 6012 0 0 0 113997 17 0 0 25 0 1 0 488635556 27344896 5979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6676 5979 603 41 0 6635 0
vsize: 26704
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 6022 0 0 0 114997 17 0 0 25 0 1 0 488635556 27344896 5989 4294967295 134512640 134672761 3221224544 3221222668 134566281 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6676 5989 603 41 0 6635 0
vsize: 26704
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 6022 0 0 0 115997 17 0 0 25 0 1 0 488635556 27344896 5989 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6676 5989 603 41 0 6635 0
vsize: 26704
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 6023 0 0 0 116997 17 0 0 25 0 1 0 488635556 27344896 5990 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6676 5990 603 41 0 6635 0
vsize: 26704
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 6024 0 0 0 117997 17 0 0 25 0 1 0 488635556 27344896 5991 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6676 5991 603 41 0 6635 0
vsize: 26704
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 6024 0 0 0 118997 17 0 0 25 0 1 0 488635556 27344896 5991 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6676 5991 603 41 0 6635 0
vsize: 26704
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11482
Raw data (stat): 11482 (minisat+) R 11481 29151 29150 0 -1 0 6024 0 0 0 119998 17 0 0 25 0 1 0 488635556 27344896 5991 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6676 5991 603 41 0 6635 0
vsize: 26704
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 11482
Raw data (stat): 11482 (minisat+) Z 11481 29151 29150 0 -1 12 6026 0 0 0 119998 18 0 0 25 0 1 0 488635556 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.03
CPU time (s): 1200.16
CPU user time (s): 1199.98
CPU system time (s): 0.183972
CPU usage (%): 100.011
Max. virtual memory (Kb): 26704
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####