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/miplib2003/normalized-mps-v2-13-7-misc07.opb
MD5SUMa3dd3cd7dd293e24bffaff8bb73da54c
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1408128
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 11486079
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 benchmark1189.01
Number of variables280
Total number of constraints471
Number of constraints which are clauses127
Number of constraints which are cardinality constraints (but not clauses)272
Number of constraints which are nor clauses,nor cardinality constraints72
Minimum length of a constraint1
Maximum length of a constraint253

Trace number 18644 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-21 15:55:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17692 boxname=wulflinc20 idbench=1361 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a3dd3cd7dd293e24bffaff8bb73da54c  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-misc07.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-misc07.opb /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-misc07.opb
IDLAUNCH: 17692
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        141424 kB
Buffers:         30364 kB
Cached:         837820 kB
SwapCached:        516 kB
Active:          75872 kB
Inactive:       794336 kB
HighTotal:      131008 kB
HighFree:          364 kB
LowTotal:       903652 kB
LowFree:        141060 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            17444 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 16:15:42 (client local time) WITH STATUS 10 IN 1200.37 SECONDS
stats: 17692 7 1200.37 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 247 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................
c ---[ 245]---> BDD-cost:1205780
c ---[ 244]---> BDD-cost:  239
c ---[ 233]---> BDD-cost:  239
c ---[ 200]---> BDD-cost:   78
c ---[ 197]---> BDD-cost:   78
c ---[ 195]---> BDD-cost:   78
c ---[ 193]---> BDD-cost:   78
c ---[ 191]---> BDD-cost:   78
c ---[ 189]---> BDD-cost:   78
c ---[ 187]---> BDD-cost:   78
c ---[ 185]---> BDD-cost:   78
c ---[ 183]---> BDD-cost:   78
c ---[ 181]---> BDD-cost:   78
c ---[ 179]---> BDD-cost:   78
c ---[ 176]---> BDD-cost:   78
c ---[ 174]---> BDD-cost:   78
c ---[ 172]---> BDD-cost:   78
c ---[ 170]---> BDD-cost:   78
c ---[ 168]---> BDD-cost:   78
c ---[ 166]---> BDD-cost:   78
c ---[ 164]---> BDD-cost:   78
c ---[ 162]---> BDD-cost:   78
c ---[ 160]---> BDD-cost:   78
c ---[ 158]---> BDD-cost:   78
c ---[ 155]---> BDD-cost:   78
c ---[ 153]---> BDD-cost:   78
c ---[ 151]---> BDD-cost:   78
c ---[ 149]---> BDD-cost:   78
c ---[ 147]---> BDD-cost:   78
c ---[ 145]---> BDD-cost:   78
c ---[ 144]---> BDD-cost:   25
c ---[ 143]---> BDD-cost:   25
c ---[ 142]---> BDD-cost:   25
c ---[ 141]---> BDD-cost:    7
c ---[ 139]---> BDD-cost:    7
c ---[ 138]---> BDD-cost:   50
c ---[ 137]---> BDD-cost:   27
c ---[ 136]---> BDD-cost:   27
c ---[ 135]---> BDD-cost:   27
c ---[ 134]---> BDD-cost:   27
c ---[ 133]---> BDD-cost:   27
c ---[ 132]---> BDD-cost:   50
c ---[ 131]---> BDD-cost:   50
c ---[ 130]---> BDD-cost:   50
c ---[ 128]---> BDD-cost:   27
c ---[ 127]---> BDD-cost:   27
c ---[ 126]---> BDD-cost:   27
c ---[ 125]---> BDD-cost:   50
c ---[ 124]---> BDD-cost:   50
c ---[ 123]---> BDD-cost:   50
c ---[ 122]---> BDD-cost:   27
c ---[ 121]---> BDD-cost:   27
c ---[ 120]---> BDD-cost:   27
c ---[ 119]---> BDD-cost:   50
c ---[ 117]---> BDD-cost:   50
c ---[ 116]---> BDD-cost:   50
c ---[ 115]---> BDD-cost:   27
c ---[ 114]---> BDD-cost:   27
c ---[ 113]---> BDD-cost:   27
c ---[ 112]---> BDD-cost:   50
c ---[ 111]---> BDD-cost:   50
c ---[ 110]---> BDD-cost:   50
c ---[ 109]---> BDD-cost:   27
c ---[ 108]---> BDD-cost:   27
c ---[ 106]---> BDD-cost:   51
c ---[ 104]---> BDD-cost:   27
c ---[ 103]---> BDD-cost:   50
c ---[ 102]---> BDD-cost:   50
c ---[ 101]---> BDD-cost:   50
c ---[ 100]---> BDD-cost:   27
c ---[  99]---> BDD-cost:   27
c ---[  98]---> BDD-cost:   27
c ---[  97]---> BDD-cost:   50
c ---[  96]---> BDD-cost:   50
c ---[  95]---> BDD-cost:   50
c ---[  93]---> BDD-cost:   27
c ---[  92]---> BDD-cost:   27
c ---[  91]---> BDD-cost:   27
c ---[  81]---> BDD-cost:   51
c ---[  69]---> BDD-cost:   51
c ---[  57]---> BDD-cost:   51
c ---[  45]---> BDD-cost:   51
c ---[  33]---> BDD-cost:   51
c ---[  21]---> BDD-cost:   51
c ---[  10]---> BDD-cost:  216
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 3565828 10573606 | 1188609       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 1634688
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  150     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        37 | 3566098 10574247 | 1188699      37      989    26.7 |  0.000 % |
c |       140 | 3566098 10574247 | 1307568     140     8895    63.5 |  0.007 % |
c ==============================================================================
c Found solution: 1628288
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       150 | 3566354 10574853 | 1188784     150     9858    65.7 |  0.007 % |
c ==============================================================================
c Found solution: 1511168
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   69     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 |       157 | 3566481 10575154 | 1188827     157    10140    64.6 |  0.007 % |
c ==============================================================================
c Found solution: 1444608
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   64     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 |       208 | 3566600 10575433 | 1188866     208    31823   153.0 |  0.007 % |
c |       309 | 3566600 10575433 | 1307752     309    40064   129.7 |  0.007 % |
c |       459 | 3566600 10575433 | 1438527     459    66997   146.0 |  0.007 % |
c |       685 | 3566600 10575433 | 1582380     685    95783   139.8 |  0.007 % |
c ==============================================================================
c Found solution: 1443968
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   79     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 |       809 | 3566745 10575771 | 1188915     809   108854   134.6 |  0.007 % |
c |       910 | 3566745 10575771 | 1307806     910   119354   131.2 |  0.007 % |
c ==============================================================================
c Found solution: 1442688
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   73     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 |      1017 | 3566877 10576080 | 1188959    1017   129556   127.4 |  0.007 % |
c ==============================================================================
c Found solution: 1426048
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   63     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 |      1079 | 3566991 10576348 | 1188997    1079   136979   126.9 |  0.007 % |
c |      1179 | 3566991 10576348 | 1307896    1179   146168   124.0 |  0.008 % |
c |      1331 | 3566991 10576348 | 1438686    1331   168060   126.3 |  0.008 % |
c |      1558 | 3566991 10576348 | 1582555    1558   192403   123.5 |  0.008 % |
c |      1900 | 3566991 10576348 | 1740810    1900   252225   132.8 |  0.008 % |
c |      2407 | 3566991 10576348 | 1914891    2407   314994   130.9 |  0.008 % |
c |      3166 | 3566991 10576348 | 2106380    3166   403101   127.3 |  0.008 % |
#### 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.78 0.94 0.92 2/54 9286
Raw data (stat): 9286 (runsolver) R 9285 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546323854 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.81 0.94 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 51953 0 0 0 876 122 0 0 25 0 1 0 546323854 216113152 44067 4294967295 134512640 134672761 3221224544 3221177728 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52762 44067 603 41 0 52721 0
vsize: 211048
[startup+20.0013 s]
Raw data (loadavg): 0.84 0.94 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 106379 0 0 0 1738 260 0 0 25 0 1 0 546323854 488292352 98493 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119212 98493 603 41 0 119171 0
vsize: 476848
[startup+30.001 s]
Raw data (loadavg): 0.87 0.94 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 111741 0 0 0 2725 273 0 0 25 0 1 0 546323854 505434112 103855 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123397 103855 603 41 0 123356 0
vsize: 493588
[startup+40.0011 s]
Raw data (loadavg): 0.89 0.94 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 111763 0 0 0 3725 273 0 0 25 0 1 0 546323854 505569280 103877 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123430 103877 603 41 0 123389 0
vsize: 493720
[startup+50.0013 s]
Raw data (loadavg): 0.90 0.94 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112026 0 0 0 4723 275 0 0 25 0 1 0 546323854 511664128 104139 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124918 104139 603 41 0 124877 0
vsize: 499672
[startup+60.0021 s]
Raw data (loadavg): 0.92 0.94 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112027 0 0 0 5723 275 0 0 25 0 1 0 546323854 511664128 104140 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124918 104140 603 41 0 124877 0
vsize: 499672
[startup+70.0033 s]
Raw data (loadavg): 0.93 0.95 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112044 0 0 0 6723 275 0 0 25 0 1 0 546323854 511803392 104157 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124952 104157 603 41 0 124911 0
vsize: 499808
[startup+80.004 s]
Raw data (loadavg): 0.94 0.95 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112071 0 0 0 7723 276 0 0 25 0 1 0 546323854 511856640 104183 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124965 104183 603 41 0 124924 0
vsize: 499860
[startup+90.0043 s]
Raw data (loadavg): 0.95 0.95 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112083 0 0 0 8723 276 0 0 25 0 1 0 546323854 511950848 104195 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124988 104195 603 41 0 124947 0
vsize: 499952
[startup+100.004 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112090 0 0 0 9722 276 0 0 25 0 1 0 546323854 511950848 104202 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124988 104202 603 41 0 124947 0
vsize: 499952
[startup+110.005 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112091 0 0 0 10722 277 0 0 25 0 1 0 546323854 511950848 104203 4294967295 134512640 134672761 3221224544 3221223648 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124988 104203 603 41 0 124947 0
vsize: 499952
[startup+120.005 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112120 0 0 0 11722 277 0 0 25 0 1 0 546323854 512212992 104232 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125052 104232 603 41 0 125011 0
vsize: 500208
[startup+130.006 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112120 0 0 0 12722 277 0 0 25 0 1 0 546323854 512081920 104231 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125020 104231 603 41 0 124979 0
vsize: 500080
[startup+140.008 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112120 0 0 0 13722 278 0 0 25 0 1 0 546323854 512081920 104231 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125020 104231 603 41 0 124979 0
vsize: 500080
[startup+150.008 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112132 0 0 0 14721 278 0 0 25 0 1 0 546323854 512081920 104243 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125020 104243 603 41 0 124979 0
vsize: 500080
[startup+160.009 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112132 0 0 0 15721 279 0 0 25 0 1 0 546323854 512081920 104243 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125020 104243 603 41 0 124979 0
vsize: 500080
[startup+170.009 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112143 0 0 0 16721 279 0 0 25 0 1 0 546323854 512204800 104254 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125050 104254 603 41 0 125009 0
vsize: 500200
[startup+180.009 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112152 0 0 0 17721 279 0 0 25 0 1 0 546323854 512221184 104262 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125054 104262 603 41 0 125013 0
vsize: 500216
[startup+190.01 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112155 0 0 0 18721 279 0 0 25 0 1 0 546323854 512221184 104265 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125054 104265 603 41 0 125013 0
vsize: 500216
[startup+200.01 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112158 0 0 0 19721 279 0 0 25 0 1 0 546323854 512221184 104268 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125054 104268 603 41 0 125013 0
vsize: 500216
[startup+210.01 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112158 0 0 0 20721 279 0 0 25 0 1 0 546323854 512221184 104268 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125054 104268 603 41 0 125013 0
vsize: 500216
[startup+220.011 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112175 0 0 0 21721 280 0 0 25 0 1 0 546323854 512290816 104285 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125071 104285 603 41 0 125030 0
vsize: 500284
[startup+230.01 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112175 0 0 0 22721 280 0 0 25 0 1 0 546323854 512290816 104285 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125071 104285 603 41 0 125030 0
vsize: 500284
[startup+240.011 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112186 0 0 0 23720 281 0 0 25 0 1 0 546323854 512323584 104295 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125079 104295 603 41 0 125038 0
vsize: 500316
[startup+250.011 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112186 0 0 0 24720 281 0 0 25 0 1 0 546323854 512323584 104295 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125079 104295 603 41 0 125038 0
vsize: 500316
[startup+260.012 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112192 0 0 0 25720 281 0 0 25 0 1 0 546323854 512393216 104301 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125096 104301 603 41 0 125055 0
vsize: 500384
[startup+270.012 s]
Raw data (loadavg): 1.23 1.02 0.94 2/54 9339
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112201 0 0 0 26717 283 0 0 25 0 1 0 546323854 512393216 104310 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125096 104310 603 41 0 125055 0
vsize: 500384
[startup+280.012 s]
Raw data (loadavg): 1.20 1.01 0.94 2/54 9339
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112202 0 0 0 27717 283 0 0 25 0 1 0 546323854 512393216 104311 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125096 104311 603 41 0 125055 0
vsize: 500384
[startup+290.013 s]
Raw data (loadavg): 1.17 1.01 0.94 2/54 9339
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112207 0 0 0 28718 283 0 0 25 0 1 0 546323854 512393216 104316 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125096 104316 603 41 0 125055 0
vsize: 500384
[startup+300.012 s]
Raw data (loadavg): 1.14 1.01 0.94 2/54 9339
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112218 0 0 0 29718 283 0 0 25 0 1 0 546323854 512462848 104327 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125113 104327 603 41 0 125072 0
vsize: 500452
[startup+310.013 s]
Raw data (loadavg): 1.12 1.01 0.94 2/54 9339
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112218 0 0 0 30718 283 0 0 25 0 1 0 546323854 512462848 104327 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125113 104327 603 41 0 125072 0
vsize: 500452
[startup+320.013 s]
Raw data (loadavg): 1.10 1.01 0.94 2/54 9339
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112237 0 0 0 31718 283 0 0 25 0 1 0 546323854 512516096 104345 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125126 104345 603 41 0 125085 0
vsize: 500504
[startup+330.012 s]
Raw data (loadavg): 1.08 1.01 0.94 2/54 9339
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112237 0 0 0 32718 284 0 0 25 0 1 0 546323854 512516096 104345 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125126 104345 603 41 0 125085 0
vsize: 500504
[startup+340.013 s]
Raw data (loadavg): 1.07 1.01 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112239 0 0 0 33718 284 0 0 25 0 1 0 546323854 512516096 104347 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125126 104347 603 41 0 125085 0
vsize: 500504
[startup+350.012 s]
Raw data (loadavg): 1.06 1.01 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112242 0 0 0 34718 284 0 0 25 0 1 0 546323854 512651264 104350 4294967295 134512640 134672761 3221224544 3221223876 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125159 104350 603 41 0 125118 0
vsize: 500636
[startup+360.013 s]
Raw data (loadavg): 1.05 1.01 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112265 0 0 0 35718 284 0 0 25 0 1 0 546323854 512651264 104373 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125159 104373 603 41 0 125118 0
vsize: 500636
[startup+370.013 s]
Raw data (loadavg): 1.04 1.01 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112265 0 0 0 36718 284 0 0 25 0 1 0 546323854 512651264 104373 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125159 104373 603 41 0 125118 0
vsize: 500636
[startup+380.012 s]
Raw data (loadavg): 1.04 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112268 0 0 0 37718 284 0 0 25 0 1 0 546323854 512651264 104376 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125159 104376 603 41 0 125118 0
vsize: 500636
[startup+390.013 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112268 0 0 0 38719 284 0 0 25 0 1 0 546323854 512651264 104376 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125159 104376 603 41 0 125118 0
vsize: 500636
[startup+400.013 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112268 0 0 0 39719 284 0 0 25 0 1 0 546323854 512651264 104376 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125159 104376 603 41 0 125118 0
vsize: 500636
[startup+410.013 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112275 0 0 0 40719 284 0 0 25 0 1 0 546323854 512675840 104382 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125165 104382 603 41 0 125124 0
vsize: 500660
[startup+420.013 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112284 0 0 0 41719 284 0 0 25 0 1 0 546323854 512712704 104390 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125174 104390 603 41 0 125133 0
vsize: 500696
[startup+430.013 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112287 0 0 0 42719 284 0 0 25 0 1 0 546323854 512729088 104392 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125178 104392 603 41 0 125137 0
vsize: 500712
[startup+440.014 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112288 0 0 0 43719 284 0 0 25 0 1 0 546323854 512729088 104393 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125178 104393 603 41 0 125137 0
vsize: 500712
[startup+450.013 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112288 0 0 0 44719 284 0 0 25 0 1 0 546323854 512729088 104393 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125178 104393 603 41 0 125137 0
vsize: 500712
[startup+460.014 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112294 0 0 0 45719 284 0 0 25 0 1 0 546323854 512729088 104399 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125178 104399 603 41 0 125137 0
vsize: 500712
[startup+470.015 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112295 0 0 0 46720 284 0 0 25 0 1 0 546323854 512729088 104400 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125178 104400 603 41 0 125137 0
vsize: 500712
[startup+480.014 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112303 0 0 0 47720 284 0 0 25 0 1 0 546323854 512827392 104408 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125202 104408 603 41 0 125161 0
vsize: 500808
[startup+490.014 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112309 0 0 0 48720 284 0 0 25 0 1 0 546323854 512827392 104414 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125202 104414 603 41 0 125161 0
vsize: 500808
[startup+500.015 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112309 0 0 0 49720 284 0 0 25 0 1 0 546323854 512827392 104414 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125202 104414 603 41 0 125161 0
vsize: 500808
[startup+510.015 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112324 0 0 0 50720 284 0 0 25 0 1 0 546323854 512909312 104429 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125222 104429 603 41 0 125181 0
vsize: 500888
[startup+520.015 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112330 0 0 0 51720 284 0 0 25 0 1 0 546323854 512909312 104435 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125222 104435 603 41 0 125181 0
vsize: 500888
[startup+530.015 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112332 0 0 0 52720 285 0 0 25 0 1 0 546323854 512909312 104437 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125222 104437 603 41 0 125181 0
vsize: 500888
[startup+540.016 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112368 0 0 0 53721 285 0 0 25 0 1 0 546323854 513048576 104473 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125256 104473 603 41 0 125215 0
vsize: 501024
[startup+550.016 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112371 0 0 0 54721 285 0 0 25 0 1 0 546323854 513081344 104475 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125264 104475 603 41 0 125223 0
vsize: 501056
[startup+560.016 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112375 0 0 0 55721 285 0 0 25 0 1 0 546323854 513081344 104479 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125264 104479 603 41 0 125223 0
vsize: 501056
[startup+570.017 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112375 0 0 0 56721 285 0 0 25 0 1 0 546323854 513081344 104479 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125264 104479 603 41 0 125223 0
vsize: 501056
[startup+580.017 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112381 0 0 0 57721 285 0 0 25 0 1 0 546323854 513081344 104485 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125264 104485 603 41 0 125223 0
vsize: 501056
[startup+590.017 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112381 0 0 0 58721 285 0 0 25 0 1 0 546323854 513081344 104485 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125264 104485 603 41 0 125223 0
vsize: 501056
[startup+600.017 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112387 0 0 0 59721 285 0 0 25 0 1 0 546323854 513150976 104491 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125281 104491 603 41 0 125240 0
vsize: 501124
[startup+610.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112387 0 0 0 60722 285 0 0 25 0 1 0 546323854 513150976 104491 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125281 104491 603 41 0 125240 0
vsize: 501124
[startup+620.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112393 0 0 0 61722 285 0 0 25 0 1 0 546323854 513150976 104497 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125281 104497 603 41 0 125240 0
vsize: 501124
[startup+630.017 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112397 0 0 0 62722 285 0 0 25 0 1 0 546323854 513150976 104501 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125281 104501 603 41 0 125240 0
vsize: 501124
[startup+640.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112401 0 0 0 63722 285 0 0 25 0 1 0 546323854 513150976 104505 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125281 104505 603 41 0 125240 0
vsize: 501124
[startup+650.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112414 0 0 0 64722 285 0 0 25 0 1 0 546323854 513282048 104518 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125313 104518 603 41 0 125272 0
vsize: 501252
[startup+660.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112421 0 0 0 65723 285 0 0 25 0 1 0 546323854 513282048 104525 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125313 104525 603 41 0 125272 0
vsize: 501252
[startup+670.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112421 0 0 0 66723 285 0 0 25 0 1 0 546323854 513282048 104525 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125313 104525 603 41 0 125272 0
vsize: 501252
[startup+680.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112421 0 0 0 67723 285 0 0 25 0 1 0 546323854 513282048 104525 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125313 104525 603 41 0 125272 0
vsize: 501252
[startup+690.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112422 0 0 0 68723 285 0 0 25 0 1 0 546323854 513282048 104526 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125313 104526 603 41 0 125272 0
vsize: 501252
[startup+700.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112436 0 0 0 69723 285 0 0 25 0 1 0 546323854 513376256 104540 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125336 104540 603 41 0 125295 0
vsize: 501344
[startup+710.019 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112437 0 0 0 70723 285 0 0 25 0 1 0 546323854 513376256 104541 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125336 104541 603 41 0 125295 0
vsize: 501344
[startup+720.019 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112455 0 0 0 71723 285 0 0 25 0 1 0 546323854 513404928 104558 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125343 104558 603 41 0 125302 0
vsize: 501372
[startup+730.019 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112455 0 0 0 72723 285 0 0 25 0 1 0 546323854 513404928 104558 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125343 104558 603 41 0 125302 0
vsize: 501372
[startup+740.019 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112459 0 0 0 73723 285 0 0 25 0 1 0 546323854 513404928 104562 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125343 104562 603 41 0 125302 0
vsize: 501372
[startup+750.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112465 0 0 0 74723 285 0 0 25 0 1 0 546323854 513458176 104567 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125356 104567 603 41 0 125315 0
vsize: 501424
[startup+760.021 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112477 0 0 0 75724 285 0 0 25 0 1 0 546323854 513495040 104578 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125365 104578 603 41 0 125324 0
vsize: 501460
[startup+770.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112477 0 0 0 76724 285 0 0 25 0 1 0 546323854 513495040 104578 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125365 104578 603 41 0 125324 0
vsize: 501460
[startup+780.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112477 0 0 0 77724 285 0 0 25 0 1 0 546323854 513495040 104578 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125365 104578 603 41 0 125324 0
vsize: 501460
[startup+790.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112477 0 0 0 78724 285 0 0 25 0 1 0 546323854 513495040 104578 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125365 104578 603 41 0 125324 0
vsize: 501460
[startup+800.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112479 0 0 0 79724 285 0 0 25 0 1 0 546323854 513495040 104580 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125365 104580 603 41 0 125324 0
vsize: 501460
[startup+810.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112482 0 0 0 80724 286 0 0 25 0 1 0 546323854 513495040 104583 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125365 104583 603 41 0 125324 0
vsize: 501460
[startup+820.021 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112503 0 0 0 81724 286 0 0 25 0 1 0 546323854 513609728 104604 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125393 104604 603 41 0 125352 0
vsize: 501572
[startup+830.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112506 0 0 0 82725 286 0 0 25 0 1 0 546323854 513609728 104607 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125393 104607 603 41 0 125352 0
vsize: 501572
[startup+840.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112510 0 0 0 83725 286 0 0 25 0 1 0 546323854 513609728 104611 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125393 104611 603 41 0 125352 0
vsize: 501572
[startup+850.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112510 0 0 0 84725 286 0 0 25 0 1 0 546323854 513609728 104611 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125393 104611 603 41 0 125352 0
vsize: 501572
[startup+860.021 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112511 0 0 0 85725 286 0 0 25 0 1 0 546323854 513609728 104612 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125393 104612 603 41 0 125352 0
vsize: 501572
[startup+870.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112526 0 0 0 86725 286 0 0 25 0 1 0 546323854 513712128 104627 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125418 104627 603 41 0 125377 0
vsize: 501672
[startup+880.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112526 0 0 0 87725 286 0 0 25 0 1 0 546323854 513712128 104627 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125418 104627 603 41 0 125377 0
vsize: 501672
[startup+890.021 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112526 0 0 0 88725 286 0 0 25 0 1 0 546323854 513712128 104627 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125418 104627 603 41 0 125377 0
vsize: 501672
[startup+900.021 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112527 0 0 0 89726 286 0 0 25 0 1 0 546323854 513712128 104628 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125418 104628 603 41 0 125377 0
vsize: 501672
[startup+910.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112527 0 0 0 90726 286 0 0 25 0 1 0 546323854 513712128 104628 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125418 104628 603 41 0 125377 0
vsize: 501672
[startup+920.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112530 0 0 0 91726 286 0 0 25 0 1 0 546323854 513712128 104631 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125418 104631 603 41 0 125377 0
vsize: 501672
[startup+930.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112538 0 0 0 92726 286 0 0 25 0 1 0 546323854 513712128 104639 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125418 104639 603 41 0 125377 0
vsize: 501672
[startup+940.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112543 0 0 0 93726 286 0 0 25 0 1 0 546323854 513789952 104644 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125437 104644 603 41 0 125396 0
vsize: 501748
[startup+950.021 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112547 0 0 0 94726 286 0 0 25 0 1 0 546323854 513789952 104648 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125437 104648 603 41 0 125396 0
vsize: 501748
[startup+960.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112550 0 0 0 95726 286 0 0 25 0 1 0 546323854 513789952 104651 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125437 104651 603 41 0 125396 0
vsize: 501748
[startup+970.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112554 0 0 0 96725 286 0 0 25 0 1 0 546323854 513789952 104655 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125437 104655 603 41 0 125396 0
vsize: 501748
[startup+980.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112569 0 0 0 97724 287 0 0 25 0 1 0 546323854 513896448 104670 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125463 104670 603 41 0 125422 0
vsize: 501852
[startup+990.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112569 0 0 0 98724 287 0 0 25 0 1 0 546323854 513896448 104670 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125463 104670 603 41 0 125422 0
vsize: 501852
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112576 0 0 0 99724 287 0 0 25 0 1 0 546323854 513896448 104677 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125463 104677 603 41 0 125422 0
vsize: 501852
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112581 0 0 0 100725 287 0 0 25 0 1 0 546323854 513896448 104682 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125463 104682 603 41 0 125422 0
vsize: 501852
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112587 0 0 0 101725 287 0 0 25 0 1 0 546323854 514002944 104688 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125489 104688 603 41 0 125448 0
vsize: 501956
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112587 0 0 0 102725 287 0 0 25 0 1 0 546323854 514002944 104688 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125489 104688 603 41 0 125448 0
vsize: 501956
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112590 0 0 0 103725 287 0 0 25 0 1 0 546323854 514002944 104691 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125489 104691 603 41 0 125448 0
vsize: 501956
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112595 0 0 0 104725 287 0 0 25 0 1 0 546323854 514002944 104696 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125489 104696 603 41 0 125448 0
vsize: 501956
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112606 0 0 0 105726 287 0 0 25 0 1 0 546323854 514027520 104706 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125495 104706 603 41 0 125454 0
vsize: 501980
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112610 0 0 0 106726 287 0 0 25 0 1 0 546323854 514027520 104710 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125495 104710 603 41 0 125454 0
vsize: 501980
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112614 0 0 0 107726 287 0 0 25 0 1 0 546323854 514027520 104714 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125495 104714 603 41 0 125454 0
vsize: 501980
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112623 0 0 0 108726 287 0 0 25 0 1 0 546323854 514134016 104723 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125521 104723 603 41 0 125480 0
vsize: 502084
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112624 0 0 0 109726 287 0 0 25 0 1 0 546323854 514134016 104724 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125521 104724 603 41 0 125480 0
vsize: 502084
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112630 0 0 0 110727 287 0 0 25 0 1 0 546323854 514134016 104730 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125521 104730 603 41 0 125480 0
vsize: 502084
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112635 0 0 0 111727 287 0 0 25 0 1 0 546323854 514134016 104735 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125521 104735 603 41 0 125480 0
vsize: 502084
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112635 0 0 0 112727 287 0 0 25 0 1 0 546323854 514134016 104735 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125521 104735 603 41 0 125480 0
vsize: 502084
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112637 0 0 0 113727 287 0 0 25 0 1 0 546323854 514134016 104737 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125521 104737 603 41 0 125480 0
vsize: 502084
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112663 0 0 0 114727 287 0 0 25 0 1 0 546323854 514232320 104763 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125545 104763 603 41 0 125504 0
vsize: 502180
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112663 0 0 0 115727 287 0 0 25 0 1 0 546323854 514232320 104763 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125545 104763 603 41 0 125504 0
vsize: 502180
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112670 0 0 0 116728 287 0 0 25 0 1 0 546323854 514232320 104770 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125545 104770 603 41 0 125504 0
vsize: 502180
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112670 0 0 0 117728 287 0 0 25 0 1 0 546323854 514232320 104770 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125545 104770 603 41 0 125504 0
vsize: 502180
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112672 0 0 0 118728 287 0 0 25 0 1 0 546323854 514334720 104772 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125570 104772 603 41 0 125529 0
vsize: 502280
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 9343
Raw data (stat): 9286 (minisat+) R 9285 27565 27564 0 -1 0 112688 0 0 0 119728 287 0 0 25 0 1 0 546323854 514334720 104788 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125570 104788 603 41 0 125529 0
vsize: 502280
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.24 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 9343
Raw data (stat): 9286 (minisat+) Z 9285 27565 27564 0 -1 12 112691 0 0 0 119728 308 0 0 25 0 1 0 546323854 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.24
CPU time (s): 1200.37
CPU user time (s): 1197.29
CPU system time (s): 3.08453
CPU usage (%): 100.011
Max. virtual memory (Kb): 502280
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####