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-misc03.opb
MD5SUMa9018751ab90bc03ab8cd95317ace234
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1478528
Optimality of the best value was proved NO
Number of terms in the objective function 21
Biggest coefficient in the objective function 1048576
Number of bits for the biggest coefficient in the objective function 21
Sum of the numbers in the objective function 2097151
Number of bits of the sum of numbers in the objective function 21
Biggest number in a constraint 1048576
Number of bits of the biggest number in a constraint 21
Biggest sum of numbers in a constraint 11386239
Number of bits of the biggest sum of numbers24
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1.20882
Number of variables180
Total number of constraints255
Number of constraints which are clauses31
Number of constraints which are cardinality constraints (but not clauses)170
Number of constraints which are nor clauses,nor cardinality constraints54
Minimum length of a constraint1
Maximum length of a constraint159

Trace number 15116 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-21 02:57:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18563 boxname=wulflinc19 idbench=1428 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a9018751ab90bc03ab8cd95317ace234  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-misc03.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-misc03.opb /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-misc03.opb
IDLAUNCH: 18563
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 3
cpu MHz		: 451.037
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:        777544 kB
Buffers:          9396 kB
Cached:         220024 kB
SwapCached:        556 kB
Active:          74680 kB
Inactive:       156816 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        777292 kB
SwapTotal:     2097892 kB
SwapFree:      2096436 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5200 kB
Slab:            19924 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 03:17:07 (client local time) WITH STATUS 30 IN 1182.55 SECONDS
stats: 18563 0 1182.55 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 123 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###########################
c   -- Clauses(.)/Splits(s): ...............................
c ---[ 121]---> BDD-cost:531660
c ---[ 119]---> BDD-cost:   39
c ---[ 117]---> BDD-cost:   39
c ---[ 115]---> BDD-cost:   39
c ---[ 113]---> BDD-cost:   39
c ---[ 111]---> BDD-cost:   39
c ---[ 110]---> BDD-cost:   98
c ---[ 109]---> BDD-cost:   98
c ---[ 108]---> BDD-cost:   98
c ---[  75]---> BDD-cost:   46
c ---[  73]---> BDD-cost:   46
c ---[  71]---> BDD-cost:   46
c ---[  69]---> BDD-cost:   46
c ---[  67]---> BDD-cost:   46
c ---[  65]---> BDD-cost:   46
c ---[  63]---> BDD-cost:   46
c ---[  61]---> BDD-cost:   46
c ---[  59]---> BDD-cost:   46
c ---[  57]---> BDD-cost:   46
c ---[  55]---> BDD-cost:   46
c ---[  53]---> BDD-cost:   46
c ---[  51]---> BDD-cost:   46
c ---[  49]---> BDD-cost:   46
c ---[  47]---> BDD-cost:   46
c ---[  45]---> BDD-cost:   46
c ---[  43]---> BDD-cost:   46
c ---[  41]---> BDD-cost:   46
c ---[  39]---> BDD-cost:   46
c ---[  37]---> BDD-cost:   46
c ---[  35]---> BDD-cost:   46
c ---[  34]---> BDD-cost:   17
c ---[  33]---> BDD-cost:   17
c ---[  32]---> BDD-cost:   17
c ---[  31]---> BDD-cost:   11
c ---[  30]---> BDD-cost:   11
c ---[  29]---> BDD-cost:   21
c ---[  28]---> BDD-cost:   21
c ---[  27]---> BDD-cost:   21
c ---[  26]---> BDD-cost:   21
c ---[  25]---> BDD-cost:   21
c ---[  24]---> BDD-cost:   21
c ---[  23]---> BDD-cost:   38
c ---[  22]---> BDD-cost:   38
c ---[  21]---> BDD-cost:   38
c ---[  20]---> BDD-cost:   21
c ---[  19]---> BDD-cost:   21
c ---[  18]---> BDD-cost:   21
c ---[  17]---> BDD-cost:   38
c ---[  16]---> BDD-cost:   38
c ---[  15]---> BDD-cost:   38
c ---[  14]---> BDD-cost:   21
c ---[  13]---> BDD-cost:   21
c ---[  12]---> BDD-cost:   21
c ---[  11]---> BDD-cost:   38
c ---[  10]---> BDD-cost:   38
c ---[   9]---> BDD-cost:   38
c ---[   8]---> BDD-cost:   21
c ---[   7]---> BDD-cost:   21
c ---[   6]---> BDD-cost:   21
c ---[   5]---> BDD-cost:   38
c ---[   4]---> BDD-cost:   38
c ---[   3]---> BDD-cost:   38
c ---[   2]---> BDD-cost:   21
c ---[   1]---> BDD-cost:   21
c ---[   0]---> BDD-cost:   21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1546605  4535117 |  515535       0        0     nan |  0.000 % |
c |       100 | 1546605  4535117 |  567088     100     4043    40.4 |  0.012 % |
c ==============================================================================
c Found solution: 1663488
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       108 | 1546874  4535748 |  515624     108     4305    39.9 |  0.012 % |
c ==============================================================================
c Found solution: 1548288
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   34     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       118 | 1546930  4535883 |  515643     118     4741    40.2 |  0.012 % |
c |       219 | 1546930  4535883 |  567207     219     9401    42.9 |  0.013 % |
c ==============================================================================
c Found solution: 1527168
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   71     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       325 | 1547063  4536197 |  515687     325    14186    43.6 |  0.013 % |
c |       425 | 1547063  4536197 |  567255     425    18126    42.6 |  0.013 % |
c ==============================================================================
c Found solution: 1478528
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   60     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       501 | 1547168  4536446 |  515722     501    21377    42.7 |  0.013 % |
c |       601 | 1547168  4536446 |  567294     601    27500    45.8 |  0.013 % |
c |       756 | 1547168  4536446 |  624023     756    49317    65.2 |  0.013 % |
c |       984 | 1547168  4536446 |  686425     984    62896    63.9 |  0.013 % |
c |      1323 | 1547168  4536446 |  755068    1323    78224    59.1 |  0.013 % |
c |      1829 | 1547168  4536446 |  830575    1829   103047    56.3 |  0.013 % |
c |      2589 | 1547168  4536446 |  913632    2589   141039    54.5 |  0.013 % |
c |      3728 | 1547168  4536446 | 1004996    3728   189767    50.9 |  0.013 % |
c |      5437 | 1547168  4536446 | 1105495    5437   264426    48.6 |  0.013 % |
c ==============================================================================
c Optimal solution: 1478528
s OPTIMUM FOUND
v -COL160_bit_7 -COL160_bit_6 -COL160_bit_5 -COL160_bit_4 -COL160_bit_3 -COL160_bit_2 -COL160_bit_1 COL160_bit0 COL160_bit1 COL160_bit2 COL160_bit3 COL160_bit4 -COL160_bit5 -COL160_bit6 -COL160_bit7 COL160_bit8 -COL160_bit9 COL160_bit10 COL160_bit11 -COL160_bit12 COL160_bit13 -COL001_bit0 -COL002_bit0 -COL003_bit0 -COL004_bit0 -COL005_bit0 -COL006_bit0 -COL007_bit0 -COL008_bit0 -COL009_bit0 -COL010_bit0 -COL011_bit0 -COL012_bit0 -COL013_bit0 -COL014_bit0 -COL015_bit0 -COL016_bit0 -COL017_bit0 -COL018_bit0 -COL019_bit0 COL020_bit0 -COL021_bit0 -COL022_bit0 COL023_bit0 -COL024_bit0 -COL025_bit0 -COL026_bit0 -COL027_bit0 -COL028_bit0 -COL029_bit0 -COL030_bit0 -COL031_bit0 -COL032_bit0 -COL033_bit0 -COL034_bit0 -COL035_bit0 -COL036_bit0 -COL037_bit0 -COL038_bit0 -COL039_bit0 -COL040_bit0 -COL041_bit0 -COL042_bit0 -COL043_bit0 -COL044_bit0 -COL045_bit0 -COL046_bit0 -COL047_bit0 -COL048_bit0 -COL049_bit0 -COL050_bit0 -COL051_bit0 -COL052_bit0 -COL053_bit0 -COL054_bit0 -COL055_bit0 -COL056_bit0 -COL057_bit0 -COL058_bit0 -COL059_bit0 -COL060_bit0 COL061_bit0 -COL062_bit0 -COL063_bit0 -COL064_bit0 -COL065_bit0 -COL066_bit0 -COL067_bit0 -COL068_bit0 -COL069_bit0 -COL070_bit0 -COL071_bit0 -COL072_bit0 -COL073_bit0 -COL074_bit0 -COL075_bit0 -COL076_bit0 -COL077_bit0 -COL078_bit0 -COL079_bit0 -COL080_bit0 COL081_bit0 -COL082_bit0 -COL083_bit0 -COL084_bit0 -COL085_bit0 -COL086_bit0 -COL087_bit0 -COL088_bit0 -COL089_bit0 -COL090_bit0 -COL091_bit0 -COL092_bit0 -COL093_bit0 -COL094_bit0 -COL095_bit0 COL096_bit0 -COL097_bit0 -COL098_bit0 -COL099_bit0 -COL100_bit0 -COL101_bit0 -COL102_bit0 -COL103_bit0 -COL104_bit0 -COL105_bit0 -COL106_bit0 -COL107_bit0 -COL108_bit0 -COL109_bit0 -COL110_bit0 -COL111_bit0 -COL112_bit0 -COL113_bit0 -COL114_bit0 -COL115_bit0 -COL116_bit0 -COL117_bit0 -COL118_bit0 -COL119_bit0 COL120_bit0 -COL121_bit0 -COL122_bit0 -COL123_bit0 -COL124_bit0 -COL125_bit0 -COL126_bit0 -COL127_bit0 -COL128_bit0 -COL129_bit0 -COL130_bit0 COL131_bit0 -COL132_bit0 COL133_bit0 -COL134_bit0 -COL135_bit0 -COL136_bit0 -COL137_bit0 -COL138_bit0 -COL139_bit0 -COL140_bit0 -COL141_bit0 -COL142_bit0 -COL143_bit0 -COL144_bit0 -COL145_bit0 -COL146_bit0 -COL147_bit0 COL148_bit0 COL149_bit0 -COL150_bit0 COL151_bit0 -COL152_bit0 COL153_bit0 -COL154_bit0 COL155_bit0 COL156_bit0 -COL157_bit0 COL158_bit0 -COL159_bit0
c _______________________________________________________________________________
c 
c restarts              : 16
c conflicts             : 7471           (6 /sec)
c decisions             : 13883          (12 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 1180.93 s
c _______________________________________________________________________________
#### 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.92 0.98 0.93 2/55 19368
Raw data (stat): 19368 (runsolver) R 19367 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541649318 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.93 0.98 0.93 2/55 19368
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 48875 0 0 0 886 112 0 0 25 0 1 0 541649318 232267776 44912 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56706 44912 603 41 0 56665 0
vsize: 226824
[startup+20.0015 s]
Raw data (loadavg): 0.94 0.98 0.93 2/55 19368
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 49210 0 0 0 1884 113 0 0 25 0 1 0 541649318 232808448 45247 4294967295 134512640 134672761 3221224544 3221223688 134566157 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56838 45247 603 41 0 56797 0
vsize: 227352
[startup+30.0022 s]
Raw data (loadavg): 0.95 0.98 0.93 2/55 19368
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 49807 0 0 0 2882 115 0 0 25 0 1 0 541649318 237387776 45844 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57956 45844 603 41 0 57915 0
vsize: 231824
[startup+40.0027 s]
Raw data (loadavg): 0.96 0.98 0.93 2/55 19368
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 49818 0 0 0 3882 115 0 0 25 0 1 0 541649318 237387776 45855 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57956 45855 603 41 0 57915 0
vsize: 231824
[startup+50.0038 s]
Raw data (loadavg): 0.96 0.98 0.93 2/55 19368
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 49824 0 0 0 4882 115 0 0 25 0 1 0 541649318 237518848 45861 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57988 45861 603 41 0 57947 0
vsize: 231952
[startup+60.0036 s]
Raw data (loadavg): 0.97 0.98 0.93 2/55 19368
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 49831 0 0 0 5882 115 0 0 25 0 1 0 541649318 237518848 45868 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57988 45868 603 41 0 57947 0
vsize: 231952
[startup+70.0042 s]
Raw data (loadavg): 0.97 0.98 0.93 2/55 19368
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 49842 0 0 0 6882 115 0 0 25 0 1 0 541649318 237518848 45879 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57988 45879 603 41 0 57947 0
vsize: 231952
[startup+80.0043 s]
Raw data (loadavg): 0.98 0.98 0.93 2/55 19368
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 49862 0 0 0 7882 115 0 0 25 0 1 0 541649318 237641728 45899 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58018 45899 603 41 0 57977 0
vsize: 232072
[startup+90.0051 s]
Raw data (loadavg): 0.98 0.98 0.93 2/55 19368
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 49989 0 0 0 8882 115 0 0 25 0 1 0 541649318 238166016 46026 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58146 46026 603 41 0 58105 0
vsize: 232584
[startup+100.005 s]
Raw data (loadavg): 0.98 0.98 0.93 2/55 19368
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 49989 0 0 0 9882 115 0 0 25 0 1 0 541649318 238166016 46026 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58146 46026 603 41 0 58105 0
vsize: 232584
[startup+110.005 s]
Raw data (loadavg): 0.98 0.98 0.93 2/55 19368
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 49989 0 0 0 10883 116 0 0 25 0 1 0 541649318 238166016 46026 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58146 46026 603 41 0 58105 0
vsize: 232584
[startup+120.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 19368
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 49989 0 0 0 11883 116 0 0 25 0 1 0 541649318 238166016 46026 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58146 46026 603 41 0 58105 0
vsize: 232584
[startup+130.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 19368
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 49989 0 0 0 12883 116 0 0 25 0 1 0 541649318 238166016 46026 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58146 46026 603 41 0 58105 0
vsize: 232584
[startup+140.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 19368
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 49989 0 0 0 13883 116 0 0 25 0 1 0 541649318 238166016 46026 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58146 46026 603 41 0 58105 0
vsize: 232584
[startup+150.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 19368
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 49989 0 0 0 14883 116 0 0 25 0 1 0 541649318 238166016 46026 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58146 46026 603 41 0 58105 0
vsize: 232584
[startup+160.008 s]
Raw data (loadavg): 0.99 0.98 0.93 4/57 19372
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 49989 0 0 0 15883 116 0 0 25 0 1 0 541649318 238166016 46026 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58146 46026 603 41 0 58105 0
vsize: 232584
[startup+170.009 s]
Raw data (loadavg): 1.07 1.00 0.93 2/55 19423
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 49995 0 0 0 16883 116 0 0 25 0 1 0 541649318 238170112 46031 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58147 46031 603 41 0 58106 0
vsize: 232588
[startup+180.01 s]
Raw data (loadavg): 1.06 1.00 0.93 2/55 19423
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 49995 0 0 0 17883 117 0 0 25 0 1 0 541649318 238170112 46031 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58147 46031 603 41 0 58106 0
vsize: 232588
[startup+190.01 s]
Raw data (loadavg): 1.05 1.00 0.93 2/55 19423
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 49997 0 0 0 18883 117 0 0 25 0 1 0 541649318 238170112 46033 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58147 46033 603 41 0 58106 0
vsize: 232588
[startup+200.01 s]
Raw data (loadavg): 1.04 1.00 0.93 2/55 19423
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 49999 0 0 0 19882 117 0 0 25 0 1 0 541649318 238170112 46035 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58147 46035 603 41 0 58106 0
vsize: 232588
[startup+210.01 s]
Raw data (loadavg): 1.03 1.00 0.93 2/55 19423
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50015 0 0 0 20882 118 0 0 25 0 1 0 541649318 238256128 46051 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58168 46051 603 41 0 58127 0
vsize: 232672
[startup+220.011 s]
Raw data (loadavg): 1.03 1.00 0.93 2/55 19423
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50015 0 0 0 21882 118 0 0 25 0 1 0 541649318 238256128 46051 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58168 46051 603 41 0 58127 0
vsize: 232672
[startup+230.011 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50015 0 0 0 22881 119 0 0 25 0 1 0 541649318 238256128 46051 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58168 46051 603 41 0 58127 0
vsize: 232672
[startup+240.012 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50017 0 0 0 23881 120 0 0 25 0 1 0 541649318 238256128 46053 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58168 46053 603 41 0 58127 0
vsize: 232672
[startup+250.012 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50025 0 0 0 24881 120 0 0 25 0 1 0 541649318 238415872 46061 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58207 46061 603 41 0 58166 0
vsize: 232828
[startup+260.012 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50036 0 0 0 25880 121 0 0 25 0 1 0 541649318 238415872 46072 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58207 46072 603 41 0 58166 0
vsize: 232828
[startup+270.013 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50037 0 0 0 26880 121 0 0 25 0 1 0 541649318 238415872 46073 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58207 46073 603 41 0 58166 0
vsize: 232828
[startup+280.013 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50038 0 0 0 27880 121 0 0 25 0 1 0 541649318 238415872 46074 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58207 46074 603 41 0 58166 0
vsize: 232828
[startup+290.014 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50038 0 0 0 28880 122 0 0 25 0 1 0 541649318 238415872 46074 4294967295 134512640 134672761 3221224544 3221223680 134565064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58207 46074 603 41 0 58166 0
vsize: 232828
[startup+300.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50052 0 0 0 29879 122 0 0 25 0 1 0 541649318 238415872 46088 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58207 46088 603 41 0 58166 0
vsize: 232828
[startup+310.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50053 0 0 0 30879 123 0 0 25 0 1 0 541649318 238415872 46089 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58207 46089 603 41 0 58166 0
vsize: 232828
[startup+320.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50053 0 0 0 31879 123 0 0 25 0 1 0 541649318 238415872 46089 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58207 46089 603 41 0 58166 0
vsize: 232828
[startup+330.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50053 0 0 0 32879 123 0 0 25 0 1 0 541649318 238415872 46089 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58207 46089 603 41 0 58166 0
vsize: 232828
[startup+340.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50053 0 0 0 33879 124 0 0 25 0 1 0 541649318 238415872 46089 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58207 46089 603 41 0 58166 0
vsize: 232828
[startup+350.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50054 0 0 0 34879 124 0 0 25 0 1 0 541649318 238415872 46090 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58207 46090 603 41 0 58166 0
vsize: 232828
[startup+360.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50058 0 0 0 35879 124 0 0 25 0 1 0 541649318 238415872 46094 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58207 46094 603 41 0 58166 0
vsize: 232828
[startup+370.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50066 0 0 0 36878 125 0 0 25 0 1 0 541649318 238415872 46102 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58207 46102 603 41 0 58166 0
vsize: 232828
[startup+380.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50067 0 0 0 37878 125 0 0 25 0 1 0 541649318 238415872 46103 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58207 46103 603 41 0 58166 0
vsize: 232828
[startup+390.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50068 0 0 0 38878 126 0 0 25 0 1 0 541649318 238415872 46104 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58207 46104 603 41 0 58166 0
vsize: 232828
[startup+400.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50083 0 0 0 39878 126 0 0 25 0 1 0 541649318 238551040 46119 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58240 46119 603 41 0 58199 0
vsize: 232960
[startup+410.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50086 0 0 0 40878 126 0 0 25 0 1 0 541649318 238551040 46122 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58240 46122 603 41 0 58199 0
vsize: 232960
[startup+420.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50088 0 0 0 41877 127 0 0 25 0 1 0 541649318 238551040 46124 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58240 46124 603 41 0 58199 0
vsize: 232960
[startup+430.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50097 0 0 0 42877 127 0 0 25 0 1 0 541649318 238551040 46133 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58240 46133 603 41 0 58199 0
vsize: 232960
[startup+440.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50105 0 0 0 43877 127 0 0 25 0 1 0 541649318 238637056 46141 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58261 46141 603 41 0 58220 0
vsize: 233044
[startup+450.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19425
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50106 0 0 0 44877 128 0 0 25 0 1 0 541649318 238637056 46142 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58261 46142 603 41 0 58220 0
vsize: 233044
[startup+460.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19427
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50108 0 0 0 45876 129 0 0 25 0 1 0 541649318 238637056 46144 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58261 46144 603 41 0 58220 0
vsize: 233044
[startup+470.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50108 0 0 0 46876 129 0 0 25 0 1 0 541649318 238637056 46144 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58261 46144 603 41 0 58220 0
vsize: 233044
[startup+480.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50112 0 0 0 47876 130 0 0 25 0 1 0 541649318 238637056 46148 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58261 46148 603 41 0 58220 0
vsize: 233044
[startup+490.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50112 0 0 0 48876 130 0 0 25 0 1 0 541649318 238637056 46148 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58261 46148 603 41 0 58220 0
vsize: 233044
[startup+500.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50125 0 0 0 49876 130 0 0 25 0 1 0 541649318 238731264 46161 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58284 46161 603 41 0 58243 0
vsize: 233136
[startup+510.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50134 0 0 0 50876 130 0 0 25 0 1 0 541649318 238731264 46170 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58284 46170 603 41 0 58243 0
vsize: 233136
[startup+520.025 s]
Raw data (loadavg): 1.15 1.03 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50134 0 0 0 51876 130 0 0 25 0 1 0 541649318 238731264 46170 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58284 46170 603 41 0 58243 0
vsize: 233136
[startup+530.026 s]
Raw data (loadavg): 1.13 1.03 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50136 0 0 0 52876 130 0 0 25 0 1 0 541649318 238731264 46172 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58284 46172 603 41 0 58243 0
vsize: 233136
[startup+540.026 s]
Raw data (loadavg): 1.11 1.03 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50138 0 0 0 53877 130 0 0 25 0 1 0 541649318 238731264 46174 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58284 46174 603 41 0 58243 0
vsize: 233136
[startup+550.026 s]
Raw data (loadavg): 1.09 1.03 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50141 0 0 0 54877 130 0 0 25 0 1 0 541649318 238731264 46177 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58284 46177 603 41 0 58243 0
vsize: 233136
[startup+560.026 s]
Raw data (loadavg): 1.08 1.03 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50141 0 0 0 55877 130 0 0 25 0 1 0 541649318 238731264 46177 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58284 46177 603 41 0 58243 0
vsize: 233136
[startup+570.027 s]
Raw data (loadavg): 1.06 1.03 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50147 0 0 0 56877 130 0 0 25 0 1 0 541649318 238800896 46183 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58301 46183 603 41 0 58260 0
vsize: 233204
[startup+580.026 s]
Raw data (loadavg): 1.05 1.02 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50152 0 0 0 57877 130 0 0 25 0 1 0 541649318 238800896 46188 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58301 46188 603 41 0 58260 0
vsize: 233204
[startup+590.028 s]
Raw data (loadavg): 1.05 1.02 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50152 0 0 0 58877 130 0 0 25 0 1 0 541649318 238800896 46188 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58301 46188 603 41 0 58260 0
vsize: 233204
[startup+600.028 s]
Raw data (loadavg): 1.04 1.02 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50152 0 0 0 59877 130 0 0 25 0 1 0 541649318 238800896 46188 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58301 46188 603 41 0 58260 0
vsize: 233204
[startup+610.028 s]
Raw data (loadavg): 1.03 1.02 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50167 0 0 0 60877 130 0 0 25 0 1 0 541649318 238878720 46203 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58320 46203 603 41 0 58279 0
vsize: 233280
[startup+620.028 s]
Raw data (loadavg): 1.03 1.02 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50186 0 0 0 61877 130 0 0 25 0 1 0 541649318 238944256 46221 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58336 46221 603 41 0 58295 0
vsize: 233344
[startup+630.028 s]
Raw data (loadavg): 1.02 1.02 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50188 0 0 0 62878 130 0 0 25 0 1 0 541649318 238944256 46223 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58336 46223 603 41 0 58295 0
vsize: 233344
[startup+640.028 s]
Raw data (loadavg): 1.02 1.02 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50188 0 0 0 63878 130 0 0 25 0 1 0 541649318 238944256 46223 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58336 46223 603 41 0 58295 0
vsize: 233344
[startup+650.029 s]
Raw data (loadavg): 1.02 1.02 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50188 0 0 0 64878 130 0 0 25 0 1 0 541649318 238944256 46223 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58336 46223 603 41 0 58295 0
vsize: 233344
[startup+660.028 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50188 0 0 0 65878 130 0 0 25 0 1 0 541649318 238944256 46223 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58336 46223 603 41 0 58295 0
vsize: 233344
[startup+670.029 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50188 0 0 0 66878 130 0 0 25 0 1 0 541649318 238944256 46223 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58336 46223 603 41 0 58295 0
vsize: 233344
[startup+680.029 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50188 0 0 0 67878 130 0 0 25 0 1 0 541649318 238944256 46223 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58336 46223 603 41 0 58295 0
vsize: 233344
[startup+690.03 s]
Raw data (loadavg): 1.01 1.01 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50188 0 0 0 68879 130 0 0 25 0 1 0 541649318 238944256 46223 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58336 46223 603 41 0 58295 0
vsize: 233344
[startup+700.029 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50190 0 0 0 69879 130 0 0 25 0 1 0 541649318 238944256 46225 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58336 46225 603 41 0 58295 0
vsize: 233344
[startup+710.03 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50205 0 0 0 70879 130 0 0 25 0 1 0 541649318 239046656 46240 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58361 46240 603 41 0 58320 0
vsize: 233444
[startup+720.03 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50205 0 0 0 71879 130 0 0 25 0 1 0 541649318 239046656 46240 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58361 46240 603 41 0 58320 0
vsize: 233444
[startup+730.03 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50205 0 0 0 72879 130 0 0 25 0 1 0 541649318 239046656 46240 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58361 46240 603 41 0 58320 0
vsize: 233444
[startup+740.031 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50205 0 0 0 73879 131 0 0 25 0 1 0 541649318 239046656 46240 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58361 46240 603 41 0 58320 0
vsize: 233444
[startup+750.032 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 19429
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50206 0 0 0 74880 131 0 0 25 0 1 0 541649318 239046656 46241 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58361 46241 603 41 0 58320 0
vsize: 233444
[startup+760.031 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50222 0 0 0 75880 131 0 0 25 0 1 0 541649318 239046656 46257 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58361 46257 603 41 0 58320 0
vsize: 233444
[startup+770.032 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50222 0 0 0 76880 131 0 0 25 0 1 0 541649318 239046656 46257 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58361 46257 603 41 0 58320 0
vsize: 233444
[startup+780.032 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50223 0 0 0 77880 131 0 0 25 0 1 0 541649318 239046656 46258 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58361 46258 603 41 0 58320 0
vsize: 233444
[startup+790.033 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50224 0 0 0 78880 131 0 0 25 0 1 0 541649318 239046656 46259 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58361 46259 603 41 0 58320 0
vsize: 233444
[startup+800.033 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50237 0 0 0 79880 131 0 0 25 0 1 0 541649318 239153152 46272 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58387 46272 603 41 0 58346 0
vsize: 233548
[startup+810.033 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50237 0 0 0 80880 131 0 0 25 0 1 0 541649318 239153152 46272 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58387 46272 603 41 0 58346 0
vsize: 233548
[startup+820.034 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50237 0 0 0 81881 131 0 0 25 0 1 0 541649318 239153152 46272 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58387 46272 603 41 0 58346 0
vsize: 233548
[startup+830.035 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50237 0 0 0 82880 131 0 0 25 0 1 0 541649318 239153152 46272 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58387 46272 603 41 0 58346 0
vsize: 233548
[startup+840.036 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50237 0 0 0 83881 131 0 0 25 0 1 0 541649318 239153152 46272 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58387 46272 603 41 0 58346 0
vsize: 233548
[startup+850.036 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50254 0 0 0 84881 131 0 0 25 0 1 0 541649318 239210496 46288 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46288 603 41 0 58360 0
vsize: 233604
[startup+860.036 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50254 0 0 0 85881 131 0 0 25 0 1 0 541649318 239210496 46288 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46288 603 41 0 58360 0
vsize: 233604
[startup+870.037 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50254 0 0 0 86881 131 0 0 25 0 1 0 541649318 239210496 46288 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46288 603 41 0 58360 0
vsize: 233604
[startup+880.036 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50254 0 0 0 87881 131 0 0 25 0 1 0 541649318 239210496 46288 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46288 603 41 0 58360 0
vsize: 233604
[startup+890.038 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50256 0 0 0 88881 131 0 0 25 0 1 0 541649318 239210496 46290 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46290 603 41 0 58360 0
vsize: 233604
[startup+900.038 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50258 0 0 0 89882 131 0 0 25 0 1 0 541649318 239210496 46292 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46292 603 41 0 58360 0
vsize: 233604
[startup+910.038 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50265 0 0 0 90882 131 0 0 25 0 1 0 541649318 239210496 46299 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46299 603 41 0 58360 0
vsize: 233604
[startup+920.038 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50265 0 0 0 91882 131 0 0 25 0 1 0 541649318 239210496 46299 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46299 603 41 0 58360 0
vsize: 233604
[startup+930.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50265 0 0 0 92882 131 0 0 25 0 1 0 541649318 239210496 46299 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46299 603 41 0 58360 0
vsize: 233604
[startup+940.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50266 0 0 0 93882 131 0 0 25 0 1 0 541649318 239210496 46300 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46300 603 41 0 58360 0
vsize: 233604
[startup+950.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50266 0 0 0 94883 131 0 0 25 0 1 0 541649318 239210496 46300 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46300 603 41 0 58360 0
vsize: 233604
[startup+960.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50271 0 0 0 95883 131 0 0 25 0 1 0 541649318 239304704 46305 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58424 46305 603 41 0 58383 0
vsize: 233696
[startup+970.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50286 0 0 0 96883 131 0 0 25 0 1 0 541649318 239325184 46319 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58429 46319 603 41 0 58388 0
vsize: 233716
[startup+980.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50287 0 0 0 97883 131 0 0 25 0 1 0 541649318 239325184 46320 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58429 46320 603 41 0 58388 0
vsize: 233716
[startup+990.041 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50287 0 0 0 98883 131 0 0 25 0 1 0 541649318 239325184 46320 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58429 46320 603 41 0 58388 0
vsize: 233716
[startup+1000.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50288 0 0 0 99883 132 0 0 25 0 1 0 541649318 239325184 46321 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58429 46321 603 41 0 58388 0
vsize: 233716
[startup+1010.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50288 0 0 0 100883 132 0 0 25 0 1 0 541649318 239325184 46321 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58429 46321 603 41 0 58388 0
vsize: 233716
[startup+1020.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50288 0 0 0 101883 132 0 0 25 0 1 0 541649318 239325184 46321 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58429 46321 603 41 0 58388 0
vsize: 233716
[startup+1030.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50288 0 0 0 102883 132 0 0 25 0 1 0 541649318 239325184 46321 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58429 46321 603 41 0 58388 0
vsize: 233716
[startup+1040.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50289 0 0 0 103883 132 0 0 25 0 1 0 541649318 239325184 46322 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58429 46322 603 41 0 58388 0
vsize: 233716
[startup+1050.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19431
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50294 0 0 0 104884 132 0 0 25 0 1 0 541649318 239325184 46327 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58429 46327 603 41 0 58388 0
vsize: 233716
[startup+1060.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19433
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50297 0 0 0 105884 132 0 0 25 0 1 0 541649318 239325184 46330 4294967295 134512640 134672761 3221224544 3221223728 134558648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58429 46330 603 41 0 58388 0
vsize: 233716
[startup+1070.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19433
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50300 0 0 0 106884 132 0 0 25 0 1 0 541649318 239427584 46333 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58454 46333 603 41 0 58413 0
vsize: 233816
[startup+1080.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19433
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50305 0 0 0 107884 132 0 0 25 0 1 0 541649318 239427584 46338 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58454 46338 603 41 0 58413 0
vsize: 233816
[startup+1090.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19433
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50306 0 0 0 108885 132 0 0 25 0 1 0 541649318 239427584 46339 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58454 46339 603 41 0 58413 0
vsize: 233816
[startup+1100.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19433
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50312 0 0 0 109885 133 0 0 25 0 1 0 541649318 239427584 46345 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58454 46345 603 41 0 58413 0
vsize: 233816
[startup+1110.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19433
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50312 0 0 0 110885 133 0 0 25 0 1 0 541649318 239427584 46345 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58454 46345 603 41 0 58413 0
vsize: 233816
[startup+1120.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19433
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50315 0 0 0 111885 133 0 0 25 0 1 0 541649318 239427584 46348 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58454 46348 603 41 0 58413 0
vsize: 233816
[startup+1130.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19433
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50318 0 0 0 112885 133 0 0 25 0 1 0 541649318 239427584 46351 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58454 46351 603 41 0 58413 0
vsize: 233816
[startup+1140.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19433
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50322 0 0 0 113885 133 0 0 25 0 1 0 541649318 239427584 46355 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58454 46355 603 41 0 58413 0
vsize: 233816
[startup+1150.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19433
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50331 0 0 0 114886 133 0 0 25 0 1 0 541649318 239554560 46364 4294967295 134512640 134672761 3221224544 3221223696 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58485 46364 603 41 0 58444 0
vsize: 233940
[startup+1160.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19433
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50331 0 0 0 115886 133 0 0 25 0 1 0 541649318 239525888 46364 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58478 46364 603 41 0 58437 0
vsize: 233912
[startup+1170.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19433
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50331 0 0 0 116886 133 0 0 25 0 1 0 541649318 239525888 46364 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58478 46364 603 41 0 58437 0
vsize: 233912
[startup+1180.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19433
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50331 0 0 0 117886 133 0 0 25 0 1 0 541649318 239525888 46364 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58478 46364 603 41 0 58437 0
vsize: 233912
[startup+1182.41 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 19433
Raw data (stat): 19368 (minisat+) R 19367 22929 22928 0 -1 0 50331 0 0 0 117886 133 0 0 25 0 1 0 541649318 239525888 46364 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58478 46364 603 41 0 58437 0
vsize: 0

Child status: 30
Real time (s): 1182.41
CPU time (s): 1182.55
CPU user time (s): 1181.12
CPU system time (s): 1.42478
CPU usage (%): 100.012
Max. virtual memory (Kb): 233940
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	1478528
#### END VERIFIER DATA ####