Some explanations

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

General information on the benchmark

Namenormalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-p0548.opb
MD5SUM10547c6c0f11ab5df74fcaff6ba6d160
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 14938
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 benchmark1244.18
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 17995 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-21 13:01:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18733 boxname=wulflinc17 idbench=1441 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  10547c6c0f11ab5df74fcaff6ba6d160  /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-p0548.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-p0548.opb /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-p0548.opb
IDLAUNCH: 18733
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        889008 kB
Buffers:         12140 kB
Cached:         107648 kB
SwapCached:        436 kB
Active:          41636 kB
Inactive:        80912 kB
HighTotal:      131008 kB
HighFree:        25760 kB
LowTotal:       903652 kB
LowFree:        863248 kB
SwapTotal:     2097892 kB
SwapFree:      2097220 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6032 kB
Slab:            17460 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 13:21:37 (client local time) WITH STATUS 0 IN 1200.2 SECONDS
stats: 18733 7 1200.2 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.94 0.98 0.92 2/55 30490
Raw data (stat): 30490 (runsolver) R 30489 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545288056 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.0009 s]
Raw data (loadavg): 0.94 0.98 0.92 2/55 30490
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 1816 0 0 0 995 4 0 0 25 0 1 0 545288056 9052160 1783 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2210 1783 603 41 0 2169 0
vsize: 8840
[startup+20.0015 s]
Raw data (loadavg): 0.95 0.98 0.92 2/55 30490
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 2098 0 0 0 1994 5 0 0 25 0 1 0 545288056 10248192 2065 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.0031 s]
Raw data (loadavg): 0.96 0.98 0.92 2/55 30490
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 2183 0 0 0 2993 5 0 0 25 0 1 0 545288056 10514432 2150 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2567 2150 603 41 0 2526 0
vsize: 10268
[startup+40.0037 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 30490
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 2301 0 0 0 3993 6 0 0 25 0 1 0 545288056 11051008 2268 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2698 2268 603 41 0 2657 0
vsize: 10792
[startup+50.0042 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 30490
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 2493 0 0 0 4992 7 0 0 25 0 1 0 545288056 11849728 2460 4294967295 134512640 134672761 3221224544 3221223632 134565745 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2893 2460 603 41 0 2852 0
vsize: 11572
[startup+60.0049 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 30490
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 2503 0 0 0 5992 8 0 0 25 0 1 0 545288056 11849728 2470 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2893 2470 603 41 0 2852 0
vsize: 11572
[startup+70.0055 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 30490
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 2521 0 0 0 6992 8 0 0 25 0 1 0 545288056 11997184 2488 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.0072 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 30490
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 2613 0 0 0 7991 9 0 0 25 0 1 0 545288056 12529664 2580 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3059 2580 603 41 0 3018 0
vsize: 12236
[startup+90.0074 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 30490
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 2622 0 0 0 8991 9 0 0 25 0 1 0 545288056 12529664 2589 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3059 2589 603 41 0 3018 0
vsize: 12236
[startup+100.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30490
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 2701 0 0 0 9991 9 0 0 25 0 1 0 545288056 12943360 2668 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30490
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 2808 0 0 0 10991 9 0 0 25 0 1 0 545288056 13348864 2775 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3259 2775 603 41 0 3218 0
vsize: 13036
[startup+120.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30490
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3064 0 0 0 11990 10 0 0 25 0 1 0 545288056 14438400 3031 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30490
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3064 0 0 0 12990 10 0 0 25 0 1 0 545288056 14438400 3031 4294967295 134512640 134672761 3221224544 3221223712 134560929 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.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30490
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3075 0 0 0 13990 10 0 0 25 0 1 0 545288056 14438400 3042 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3525 3042 603 41 0 3484 0
vsize: 14100
[startup+150.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30490
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3076 0 0 0 14991 10 0 0 25 0 1 0 545288056 14438400 3043 4294967295 134512640 134672761 3221224544 3221223696 134561040 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.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30492
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3077 0 0 0 15991 10 0 0 25 0 1 0 545288056 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.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30492
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3077 0 0 0 16991 10 0 0 25 0 1 0 545288056 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+180.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30492
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3114 0 0 0 17991 11 0 0 25 0 1 0 545288056 14573568 3081 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3558 3081 603 41 0 3517 0
vsize: 14232
[startup+190.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30492
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3146 0 0 0 18991 11 0 0 25 0 1 0 545288056 14716928 3113 4294967295 134512640 134672761 3221224544 3221223712 134560999 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.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30492
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3157 0 0 0 19991 11 0 0 25 0 1 0 545288056 14876672 3124 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3632 3124 603 41 0 3591 0
vsize: 14528
[startup+210.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30492
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3202 0 0 0 20991 11 0 0 25 0 1 0 545288056 15007744 3169 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3664 3169 603 41 0 3623 0
vsize: 14656
[startup+220.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30492
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3281 0 0 0 21991 11 0 0 25 0 1 0 545288056 15421440 3248 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3765 3248 603 41 0 3724 0
vsize: 15060
[startup+230.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30492
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3285 0 0 0 22991 11 0 0 25 0 1 0 545288056 15421440 3252 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3765 3252 603 41 0 3724 0
vsize: 15060
[startup+240.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3304 0 0 0 23991 11 0 0 25 0 1 0 545288056 15421440 3271 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3765 3271 603 41 0 3724 0
vsize: 15060
[startup+250.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3307 0 0 0 24991 11 0 0 25 0 1 0 545288056 15585280 3274 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3805 3274 603 41 0 3764 0
vsize: 15220
[startup+260.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3316 0 0 0 25991 12 0 0 25 0 1 0 545288056 15585280 3283 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3805 3283 603 41 0 3764 0
vsize: 15220
[startup+270.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3338 0 0 0 26991 12 0 0 25 0 1 0 545288056 15749120 3305 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3343 0 0 0 27992 12 0 0 25 0 1 0 545288056 15749120 3310 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3845 3310 603 41 0 3804 0
vsize: 15380
[startup+290.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3366 0 0 0 28992 12 0 0 25 0 1 0 545288056 15912960 3333 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3885 3333 603 41 0 3844 0
vsize: 15540
[startup+300.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3367 0 0 0 29992 12 0 0 25 0 1 0 545288056 15912960 3334 4294967295 134512640 134672761 3221224544 3221223680 134560688 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.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3367 0 0 0 30992 12 0 0 25 0 1 0 545288056 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+320.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3368 0 0 0 31992 12 0 0 25 0 1 0 545288056 15912960 3335 4294967295 134512640 134672761 3221224544 3221223712 134560994 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.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3368 0 0 0 32992 12 0 0 25 0 1 0 545288056 15912960 3335 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3885 3335 603 41 0 3844 0
vsize: 15540
[startup+340.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3382 0 0 0 33993 12 0 0 25 0 1 0 545288056 15912960 3349 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3885 3349 603 41 0 3844 0
vsize: 15540
[startup+350.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3392 0 0 0 34992 12 0 0 25 0 1 0 545288056 16076800 3359 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3925 3359 603 41 0 3884 0
vsize: 15700
[startup+360.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3613 0 0 0 35992 12 0 0 25 0 1 0 545288056 16883712 3580 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4122 3580 603 41 0 4081 0
vsize: 16488
[startup+370.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3629 0 0 0 36992 13 0 0 25 0 1 0 545288056 17018880 3596 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3596 603 41 0 4114 0
vsize: 16620
[startup+380.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3637 0 0 0 37992 13 0 0 25 0 1 0 545288056 17018880 3604 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3604 603 41 0 4114 0
vsize: 16620
[startup+390.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3655 0 0 0 38992 13 0 0 25 0 1 0 545288056 17182720 3622 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4195 3622 603 41 0 4154 0
vsize: 16780
[startup+400.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3694 0 0 0 39992 13 0 0 25 0 1 0 545288056 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+410.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3736 0 0 0 40992 13 0 0 25 0 1 0 545288056 17477632 3703 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4267 3703 603 41 0 4226 0
vsize: 17068
[startup+420.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3742 0 0 0 41992 13 0 0 25 0 1 0 545288056 17477632 3709 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4267 3709 603 41 0 4226 0
vsize: 17068
[startup+430.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3746 0 0 0 42993 13 0 0 25 0 1 0 545288056 17477632 3713 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4267 3713 603 41 0 4226 0
vsize: 17068
[startup+440.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3766 0 0 0 43993 13 0 0 25 0 1 0 545288056 17620992 3733 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4302 3733 603 41 0 4261 0
vsize: 17208
[startup+450.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30494
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3806 0 0 0 44993 13 0 0 25 0 1 0 545288056 17752064 3773 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4334 3773 603 41 0 4293 0
vsize: 17336
[startup+460.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3813 0 0 0 45993 13 0 0 25 0 1 0 545288056 17752064 3780 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4334 3780 603 41 0 4293 0
vsize: 17336
[startup+470.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3837 0 0 0 46993 13 0 0 25 0 1 0 545288056 17899520 3804 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4370 3804 603 41 0 4329 0
vsize: 17480
[startup+480.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 3943 0 0 0 47993 13 0 0 25 0 1 0 545288056 18432000 3910 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4500 3910 603 41 0 4459 0
vsize: 18000
[startup+490.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4209 0 0 0 48992 15 0 0 25 0 1 0 545288056 19492864 4176 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4759 4176 603 41 0 4718 0
vsize: 19036
[startup+500.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4212 0 0 0 49992 15 0 0 25 0 1 0 545288056 19492864 4179 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4212 0 0 0 50992 15 0 0 25 0 1 0 545288056 19492864 4179 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4759 4179 603 41 0 4718 0
vsize: 19036
[startup+520.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4215 0 0 0 51992 15 0 0 25 0 1 0 545288056 19492864 4182 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4759 4182 603 41 0 4718 0
vsize: 19036
[startup+530.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4257 0 0 0 52993 15 0 0 25 0 1 0 545288056 19648512 4224 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4797 4224 603 41 0 4756 0
vsize: 19188
[startup+540.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4274 0 0 0 53993 15 0 0 25 0 1 0 545288056 19783680 4241 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4830 4241 603 41 0 4789 0
vsize: 19320
[startup+550.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4350 0 0 0 54992 15 0 0 25 0 1 0 545288056 20062208 4317 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4350 0 0 0 55992 15 0 0 25 0 1 0 545288056 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+570.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4362 0 0 0 56991 16 0 0 25 0 1 0 545288056 20213760 4329 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4935 4329 603 41 0 4894 0
vsize: 19740
[startup+580.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4394 0 0 0 57990 16 0 0 25 0 1 0 545288056 20377600 4361 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4975 4361 603 41 0 4934 0
vsize: 19900
[startup+590.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4409 0 0 0 58990 17 0 0 25 0 1 0 545288056 20377600 4376 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4975 4376 603 41 0 4934 0
vsize: 19900
[startup+600.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4410 0 0 0 59990 17 0 0 25 0 1 0 545288056 20377600 4377 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4975 4377 603 41 0 4934 0
vsize: 19900
[startup+610.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4435 0 0 0 60990 17 0 0 25 0 1 0 545288056 20541440 4402 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5015 4402 603 41 0 4974 0
vsize: 20060
[startup+620.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4470 0 0 0 61990 17 0 0 25 0 1 0 545288056 20738048 4437 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5063 4437 603 41 0 5022 0
vsize: 20252
[startup+630.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4488 0 0 0 62990 17 0 0 25 0 1 0 545288056 20738048 4455 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5063 4455 603 41 0 5022 0
vsize: 20252
[startup+640.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4521 0 0 0 63991 17 0 0 25 0 1 0 545288056 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.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4521 0 0 0 64991 17 0 0 25 0 1 0 545288056 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.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4521 0 0 0 65991 17 0 0 25 0 1 0 545288056 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+670.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4521 0 0 0 66991 17 0 0 25 0 1 0 545288056 20934656 4488 4294967295 134512640 134672761 3221224544 3221223728 134559199 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5111 4488 603 41 0 5070 0
vsize: 20444
[startup+680.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4534 0 0 0 67990 17 0 0 25 0 1 0 545288056 20934656 4501 4294967295 134512640 134672761 3221224544 3221223728 134559176 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.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4534 0 0 0 68990 17 0 0 25 0 1 0 545288056 20934656 4501 4294967295 134512640 134672761 3221224544 3221223728 134559176 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.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4534 0 0 0 69991 17 0 0 25 0 1 0 545288056 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+710.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4534 0 0 0 70991 17 0 0 25 0 1 0 545288056 20934656 4501 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5111 4501 603 41 0 5070 0
vsize: 20444
[startup+720.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4628 0 0 0 71991 18 0 0 25 0 1 0 545288056 21352448 4595 4294967295 134512640 134672761 3221224544 3221223728 134559332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5213 4595 603 41 0 5172 0
vsize: 20852
[startup+730.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4639 0 0 0 72991 18 0 0 25 0 1 0 545288056 21516288 4606 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5253 4606 603 41 0 5212 0
vsize: 21012
[startup+740.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4661 0 0 0 73991 18 0 0 25 0 1 0 545288056 21516288 4628 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5253 4628 603 41 0 5212 0
vsize: 21012
[startup+750.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30496
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4681 0 0 0 74991 18 0 0 25 0 1 0 545288056 21680128 4648 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5293 4648 603 41 0 5252 0
vsize: 21172
[startup+760.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4702 0 0 0 75991 18 0 0 25 0 1 0 545288056 21872640 4669 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5340 4669 603 41 0 5299 0
vsize: 21360
[startup+770.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4704 0 0 0 76991 18 0 0 25 0 1 0 545288056 21872640 4671 4294967295 134512640 134672761 3221224544 3221223120 134565829 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.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4704 0 0 0 77991 18 0 0 25 0 1 0 545288056 21872640 4671 4294967295 134512640 134672761 3221224544 3221223728 134559367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5340 4671 603 41 0 5299 0
vsize: 21360
[startup+790.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4704 0 0 0 78992 18 0 0 25 0 1 0 545288056 21872640 4671 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5340 4671 603 41 0 5299 0
vsize: 21360
[startup+800.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4710 0 0 0 79993 18 0 0 25 0 1 0 545288056 21872640 4677 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5340 4677 603 41 0 5299 0
vsize: 21360
[startup+810.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4712 0 0 0 80993 18 0 0 25 0 1 0 545288056 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+820.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4712 0 0 0 81993 18 0 0 25 0 1 0 545288056 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+830.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4723 0 0 0 82993 18 0 0 25 0 1 0 545288056 21872640 4690 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5340 4690 603 41 0 5299 0
vsize: 21360
[startup+840.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4723 0 0 0 83994 18 0 0 25 0 1 0 545288056 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+850.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4725 0 0 0 84994 18 0 0 25 0 1 0 545288056 21872640 4692 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5340 4692 603 41 0 5299 0
vsize: 21360
[startup+860.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4725 0 0 0 85994 18 0 0 25 0 1 0 545288056 21872640 4692 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5340 4692 603 41 0 5299 0
vsize: 21360
[startup+870.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4735 0 0 0 86994 19 0 0 25 0 1 0 545288056 22036480 4702 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5380 4702 603 41 0 5339 0
vsize: 21520
[startup+880.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4737 0 0 0 87993 19 0 0 25 0 1 0 545288056 22036480 4704 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5380 4704 603 41 0 5339 0
vsize: 21520
[startup+890.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4909 0 0 0 88992 19 0 0 25 0 1 0 545288056 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.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4909 0 0 0 89992 19 0 0 25 0 1 0 545288056 22704128 4876 4294967295 134512640 134672761 3221224544 3221223688 134560555 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.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4909 0 0 0 90993 19 0 0 25 0 1 0 545288056 22704128 4876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5543 4876 603 41 0 5502 0
vsize: 22172
[startup+920.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4909 0 0 0 91993 19 0 0 25 0 1 0 545288056 22704128 4876 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5543 4876 603 41 0 5502 0
vsize: 22172
[startup+930.022 s]
Raw data (loadavg): 0.99 0.98 0.92 3/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 4909 0 0 0 92993 19 0 0 25 0 1 0 545288056 22704128 4876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5543 4876 603 41 0 5502 0
vsize: 22172
[startup+940.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 5206 0 0 0 93993 20 0 0 25 0 1 0 545288056 23904256 5173 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5836 5173 603 41 0 5795 0
vsize: 23344
[startup+950.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 5290 0 0 0 94993 20 0 0 25 0 1 0 545288056 24174592 5257 4294967295 134512640 134672761 3221224544 3221223648 134560054 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.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 5290 0 0 0 95993 20 0 0 25 0 1 0 545288056 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+970.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 5290 0 0 0 96993 20 0 0 25 0 1 0 545288056 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+980.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 5290 0 0 0 97993 20 0 0 25 0 1 0 545288056 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+990.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 5492 0 0 0 98993 21 0 0 25 0 1 0 545288056 25112576 5459 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6131 5459 603 41 0 6090 0
vsize: 24524
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 5787 0 0 0 99992 22 0 0 25 0 1 0 545288056 26324992 5754 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6427 5754 603 41 0 6386 0
vsize: 25708
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 5964 0 0 0 100991 23 0 0 25 0 1 0 545288056 27004928 5931 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6593 5931 603 41 0 6552 0
vsize: 26372
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 5970 0 0 0 101992 23 0 0 25 0 1 0 545288056 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+1030.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 5970 0 0 0 102992 23 0 0 25 0 1 0 545288056 27004928 5937 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6593 5937 603 41 0 6552 0
vsize: 26372
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 5970 0 0 0 103992 23 0 0 25 0 1 0 545288056 27004928 5937 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6593 5937 603 41 0 6552 0
vsize: 26372
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30498
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 5983 0 0 0 104992 23 0 0 25 0 1 0 545288056 27148288 5950 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6628 5950 603 41 0 6587 0
vsize: 26512
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30500
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 5990 0 0 0 105992 23 0 0 25 0 1 0 545288056 27148288 5957 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6628 5957 603 41 0 6587 0
vsize: 26512
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30500
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 5991 0 0 0 106993 23 0 0 25 0 1 0 545288056 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+1080.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30500
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 6000 0 0 0 107993 23 0 0 25 0 1 0 545288056 27148288 5967 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6628 5967 603 41 0 6587 0
vsize: 26512
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30500
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 6000 0 0 0 108993 23 0 0 25 0 1 0 545288056 27148288 5967 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6628 5967 603 41 0 6587 0
vsize: 26512
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30500
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 6001 0 0 0 109993 23 0 0 25 0 1 0 545288056 27148288 5968 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6628 5968 603 41 0 6587 0
vsize: 26512
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30500
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 6010 0 0 0 110993 23 0 0 25 0 1 0 545288056 27344896 5977 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6676 5977 603 41 0 6635 0
vsize: 26704
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30500
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 6012 0 0 0 111994 23 0 0 25 0 1 0 545288056 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+1130.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30500
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 6012 0 0 0 112994 23 0 0 25 0 1 0 545288056 27344896 5979 4294967295 134512640 134672761 3221224544 3221223712 134561201 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.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30500
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 6012 0 0 0 113994 23 0 0 25 0 1 0 545288056 27344896 5979 4294967295 134512640 134672761 3221224544 3221223712 134561151 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.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30500
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 6012 0 0 0 114994 23 0 0 25 0 1 0 545288056 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+1160.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30500
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 6012 0 0 0 115994 23 0 0 25 0 1 0 545288056 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+1170.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30500
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 6012 0 0 0 116994 23 0 0 25 0 1 0 545288056 27344896 5979 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6676 5979 603 41 0 6635 0
vsize: 26704
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30500
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 6022 0 0 0 117994 23 0 0 25 0 1 0 545288056 27344896 5989 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6676 5989 603 41 0 6635 0
vsize: 26704
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30500
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 6022 0 0 0 118994 23 0 0 25 0 1 0 545288056 27344896 5989 4294967295 134512640 134672761 3221224544 3221223724 134553617 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6676 5989 603 41 0 6635 0
vsize: 26704
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30500
Raw data (stat): 30490 (minisat+) R 30489 20838 20837 0 -1 0 6023 0 0 0 119994 23 0 0 25 0 1 0 545288056 27344896 5990 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6676 5990 603 41 0 6635 0
vsize: 26704
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.98 0.92 1/55 30500
Raw data (stat): 30490 (minisat+) Z 30489 20838 20837 0 -1 12 6025 0 0 0 119994 25 0 0 25 0 1 0 545288056 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.04
CPU time (s): 1200.2
CPU user time (s): 1199.95
CPU system time (s): 0.250961
CPU usage (%): 100.014
Max. virtual memory (Kb): 26704
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####