PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/submitted/een/normalized-l152lav.opb
MD5SUM	7ef542195551d721d26b015e392d6d4b
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	1989
Biggest coefficient in the objective function	268
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	382524
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	1961
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	382524
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.237962
Number of variables	1989
Total number of constraints	193
Number of constraints which are clauses	95
Number of constraints which are cardinality constraints (but not clauses)	97
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	3
Maximum length of a constraint	1989
Trace number 7143

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-14 21:36:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5223 boxname=wulflinc22 idbench=402 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7ef542195551d721d26b015e392d6d4b  /oldhome/oroussel/tmp/wulflinc22/normalized-l152lav.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc22/normalized-l152lav.opb /oldhome/oroussel/tmp/wulflinc22/normalized-l152lav.opb
IDLAUNCH: 5223
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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.031
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:        835412 kB
Buffers:         32192 kB
Cached:         124208 kB
SwapCached:          0 kB
Active:          25528 kB
Inactive:       133692 kB
HighTotal:      131008 kB
HighFree:         4984 kB
LowTotal:       903652 kB
LowFree:        830428 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            34348 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 21:56:29 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 5223 7 1200.24 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 193 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ==========================================================================================
c   -- Clauses(.)/Splits(s): ......
c ---[ 191]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 189]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 187]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 185]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 183]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 181]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 179]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[ 177]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 175]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[ 173]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[ 171]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[ 170]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[ 167]---> Adder-cost: 62   maxlim: 30   bits: 6/5
c ---[ 165]---> Adder-cost: 62   maxlim: 30   bits: 6/5
c ---[ 163]---> Adder-cost: 62   maxlim: 33   bits: 6/6
c ---[ 161]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[ 159]---> Adder-cost: 66   maxlim: 35   bits: 6/6
c ---[ 157]---> Adder-cost: 68   maxlim: 35   bits: 6/6
c ---[ 155]---> Adder-cost: 68   maxlim: 35   bits: 6/6
c ---[ 153]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[ 151]---> Adder-cost: 78   maxlim: 40   bits: 6/6
c ---[ 148]---> Adder-cost: 78   maxlim: 40   bits: 6/6
c ---[ 147]---> Adder-cost: 78   maxlim: 40   bits: 6/6
c ---[ 145]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[ 143]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[ 141]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[ 139]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[ 137]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[ 135]---> Adder-cost: 84   maxlim: 44   bits: 6/6
c ---[ 133]---> Adder-cost: 84   maxlim: 45   bits: 6/6
c ---[ 131]---> Adder-cost: 92   maxlim: 46   bits: 6/6
c ---[ 129]---> Adder-cost: 92   maxlim: 46   bits: 6/6
c ---[ 127]---> Adder-cost: 92   maxlim: 46   bits: 6/6
c ---[ 125]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[ 123]---> Adder-cost: 94   maxlim: 48   bits: 6/6
c ---[ 120]---> Adder-cost: 98   maxlim: 50   bits: 6/6
c ---[ 119]---> Adder-cost: 98   maxlim: 50   bits: 6/6
c ---[ 117]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[ 115]---> Adder-cost: 100   maxlim: 52   bits: 6/6
c ---[ 113]---> Adder-cost: 106   maxlim: 54   bits: 6/6
c ---[ 111]---> Adder-cost: 106   maxlim: 54   bits: 6/6
c ---[ 109]---> Adder-cost: 108   maxlim: 56   bits: 6/6
c ---[ 107]---> Adder-cost: 110   maxlim: 58   bits: 6/6
c ---[ 105]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[ 103]---> Adder-cost: 114   maxlim: 60   bits: 6/6
c ---[ 101]---> Adder-cost: 128   maxlim: 64   bits: 7/7
c ---[  99]---> Adder-cost: 130   maxlim: 66   bits: 7/7
c ---[  97]---> Adder-cost: 124   maxlim: 66   bits: 7/7
c ---[  95]---> Adder-cost: 132   maxlim: 66   bits: 7/7
c ---[  93]---> Adder-cost: 140   maxlim: 71   bits: 7/7
c ---[  91]---> Adder-cost: 142   maxlim: 72   bits: 7/7
c ---[  89]---> Adder-cost: 142   maxlim: 73   bits: 7/7
c ---[  87]---> Adder-cost: 140   maxlim: 73   bits: 7/7
c ---[  85]---> Adder-cost: 142   maxlim: 73   bits: 7/7
c ---[  83]---> Adder-cost: 146   maxlim: 74   bits: 7/7
c ---[  81]---> Adder-cost: 144   maxlim: 75   bits: 7/7
c ---[  79]---> Adder-cost: 146   maxlim: 75   bits: 7/7
c ---[  77]---> Adder-cost: 148   maxlim: 76   bits: 7/7
c ---[  75]---> Adder-cost: 146   maxlim: 77   bits: 7/7
c ---[  73]---> Adder-cost: 152   maxlim: 78   bits: 7/7
c ---[  71]---> Adder-cost: 150   maxlim: 85   bits: 7/7
c ---[  69]---> Adder-cost: 170   maxlim: 86   bits: 7/7
c ---[  67]---> Adder-cost: 166   maxlim: 86   bits: 7/7
c ---[  65]---> Adder-cost: 176   maxlim: 90   bits: 7/7
c ---[  63]---> Adder-cost: 172   maxlim: 90   bits: 7/7
c ---[  61]---> Adder-cost: 174   maxlim: 90   bits: 7/7
c ---[  59]---> Adder-cost: 176   maxlim: 91   bits: 7/7
c ---[  57]---> Adder-cost: 174   maxlim: 92   bits: 7/7
c ---[  55]---> Adder-cost: 188   maxlim: 94   bits: 7/7
c ---[  53]---> Adder-cost: 188   maxlim: 94   bits: 7/7
c ---[  52]---> Adder-cost: 188   maxlim: 94   bits: 7/7
c ---[  49]---> Adder-cost: 188   maxlim: 95   bits: 7/7
c ---[  47]---> Adder-cost: 196   maxlim: 100   bits: 7/7
c ---[  45]---> Adder-cost: 194   maxlim: 100   bits: 7/7
c ---[  43]---> Adder-cost: 194   maxlim: 101   bits: 7/7
c ---[  41]---> Adder-cost: 196   maxlim: 102   bits: 7/7
c ---[  39]---> Adder-cost: 200   maxlim: 104   bits: 7/7
c ---[  37]---> Adder-cost: 208   maxlim: 106   bits: 7/7
c ---[  35]---> Adder-cost: 206   maxlim: 106   bits: 7/7
c ---[  33]---> Adder-cost: 210   maxlim: 110   bits: 7/7
c ---[  31]---> Adder-cost: 216   maxlim: 110   bits: 7/7
c ---[  29]---> Adder-cost: 220   maxlim: 112   bits: 7/7
c ---[  27]---> Adder-cost: 202   maxlim: 116   bits: 7/7
c ---[  25]---> Adder-cost: 232   maxlim: 119   bits: 7/7
c ---[  23]---> Adder-cost: 218   maxlim: 119   bits: 7/7
c ---[  21]---> Adder-cost: 232   maxlim: 121   bits: 7/7
c ---[  19]---> Adder-cost: 222   maxlim: 123   bits: 7/7
c ---[  17]---> Adder-cost: 242   maxlim: 126   bits: 8/7
c ---[  15]---> Adder-cost: 198   maxlim: 127   bits: 8/7
c ---[  13]---> Adder-cost: 244   maxlim: 135   bits: 8/8
c ---[  11]---> Adder-cost: 274   maxlim: 150   bits: 8/8
c ---[   9]---> Adder-cost: 288   maxlim: 158   bits: 8/8
c ---[   7]---> Adder-cost: 278   maxlim: 161   bits: 8/8
c ---[   5]---> Adder-cost: 326   maxlim: 169   bits: 8/8
c ---[   3]---> Adder-cost: 408   maxlim: 216   bits: 8/8
c ---[   2]---> Adder-cost: 4746   maxlim: 25152   bits: 15/15
c ---[   0]---> Adder-cost: 3056   maxlim: 1960   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  140156   499983 |   46718       0        0     nan |  0.000 % |
c |       100 |  139678   498313 |   51389      34      107     3.1 |  3.561 % |
c |       250 |  138747   495023 |   56528      63      202     3.2 |  4.261 % |
c |       475 |  138103   492782 |   62181     205      661     3.2 |  4.747 % |
c |       812 |  137503   490680 |   68399     471     1537     3.3 |  5.241 % |
c |      1318 |  136721   487978 |   75239     875     3267     3.7 |  5.863 % |
c |      2077 |  136012   485507 |   82763    1533     6487     4.2 |  6.396 % |
c |      3217 |  135680   484372 |   91040    2629    13166     5.0 |  6.650 % |
c |      4926 |  135007   482022 |  100144    4241    24192     5.7 |  7.149 % |
c |      7489 |  134188   479222 |  110158    6676    47746     7.2 |  7.753 % |
c |     11333 |  133638   477293 |  121174   10451   136051    13.0 |  8.142 % |
c |     17103 |  133112   475443 |  133291   15886   457002    28.8 |  8.448 % |
c |     25752 |  132884   474663 |  146621   24494  1474111    60.2 |  8.614 % |
c |     38730 |  132392   472964 |  161283   37360  3089382    82.7 |  8.912 % |
c |     58194 |  131811   470939 |  177411   56361  5712628   101.4 |  9.258 % |
c |     87386 |  131067   468318 |  195152   84950  9649496   113.6 |  9.769 % |
c |    131176 |  130212   465338 |  214667  127951 15890339   124.2 | 10.316 % |
c |    196863 |  127772   456732 |  236134  191708 25155652   131.2 | 11.983 % |
#### 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.84 0.92 0.90 2/54 4060
Raw data (stat): 4060 (runsolver) R 4059 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487879567 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0005 s]
Raw data (loadavg): 0.86 0.92 0.90 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 2899 0 0 0 992 7 0 0 25 0 1 0 487879567 14270464 2817 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3484 2817 603 41 0 3443 0
vsize: 13936
[startup+20.0007 s]
Raw data (loadavg): 0.88 0.92 0.90 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 2939 0 0 0 1991 7 0 0 25 0 1 0 487879567 14426112 2857 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3522 2857 603 41 0 3481 0
vsize: 14088
[startup+30.001 s]
Raw data (loadavg): 0.90 0.92 0.90 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 2977 0 0 0 2991 8 0 0 25 0 1 0 487879567 14696448 2895 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3588 2895 603 41 0 3547 0
vsize: 14352
[startup+40.0007 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 3159 0 0 0 3990 9 0 0 25 0 1 0 487879567 15368192 3077 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3077 603 41 0 3711 0
vsize: 15008
[startup+50.0008 s]
Raw data (loadavg): 0.93 0.93 0.90 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 3642 0 0 0 4989 11 0 0 25 0 1 0 487879567 17371136 3560 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4241 3560 603 41 0 4200 0
vsize: 16964
[startup+60.0011 s]
Raw data (loadavg): 0.94 0.93 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 4290 0 0 0 5986 13 0 0 25 0 1 0 487879567 20058112 4208 4294967295 134512640 134672761 3221224560 3221223728 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4897 4208 603 41 0 4856 0
vsize: 19588
[startup+70.0008 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 4867 0 0 0 6984 15 0 0 25 0 1 0 487879567 22327296 4785 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5451 4785 603 41 0 5410 0
vsize: 21804
[startup+80.0019 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 5423 0 0 0 7982 18 0 0 25 0 1 0 487879567 24596480 5341 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6005 5341 603 41 0 5964 0
vsize: 24020
[startup+90.0023 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 5972 0 0 0 8980 20 0 0 25 0 1 0 487879567 26996736 5890 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6591 5890 603 41 0 6550 0
vsize: 26364
[startup+100.002 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 6344 0 0 0 9979 21 0 0 25 0 1 0 487879567 28483584 6262 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6954 6262 603 41 0 6913 0
vsize: 27816
[startup+110.003 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 6861 0 0 0 10977 23 0 0 25 0 1 0 487879567 30601216 6779 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7471 6779 603 41 0 7430 0
vsize: 29884
[startup+120.003 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 7306 0 0 0 11976 25 0 0 25 0 1 0 487879567 32477184 7224 4294967295 134512640 134672761 3221224560 3221223748 134556588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7929 7224 603 41 0 7888 0
vsize: 31716
[startup+130.004 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 7712 0 0 0 12974 26 0 0 25 0 1 0 487879567 34086912 7630 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8322 7630 603 41 0 8281 0
vsize: 33288
[startup+140.004 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 8167 0 0 0 13973 28 0 0 25 0 1 0 487879567 35946496 8085 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8776 8085 603 41 0 8735 0
vsize: 35104
[startup+150.004 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 8674 0 0 0 14971 29 0 0 25 0 1 0 487879567 37945344 8592 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9264 8592 603 41 0 9223 0
vsize: 37056
[startup+160.004 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 9042 0 0 0 15970 31 0 0 25 0 1 0 487879567 39563264 8960 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9659 8960 603 41 0 9618 0
vsize: 38636
[startup+170.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 9365 0 0 0 16969 32 0 0 25 0 1 0 487879567 40886272 9283 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9982 9283 603 41 0 9941 0
vsize: 39928
[startup+180.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 9805 0 0 0 17968 34 0 0 25 0 1 0 487879567 42610688 9723 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10403 9723 603 41 0 10362 0
vsize: 41612
[startup+190.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 10087 0 0 0 18967 34 0 0 25 0 1 0 487879567 43823104 10005 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10699 10005 603 41 0 10658 0
vsize: 42796
[startup+200.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 10378 0 0 0 19967 35 0 0 25 0 1 0 487879567 44888064 10296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10959 10296 603 41 0 10918 0
vsize: 43836
[startup+210.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 10722 0 0 0 20966 36 0 0 25 0 1 0 487879567 46616576 10640 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11381 10640 603 41 0 11340 0
vsize: 45524
[startup+220.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 11037 0 0 0 21965 37 0 0 25 0 1 0 487879567 47828992 10955 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11677 10955 603 41 0 11636 0
vsize: 46708
[startup+230.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 11325 0 0 0 22964 38 0 0 25 0 1 0 487879567 49041408 11243 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11973 11243 603 41 0 11932 0
vsize: 47892
[startup+240.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 11698 0 0 0 23963 39 0 0 25 0 1 0 487879567 50524160 11616 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12335 11616 603 41 0 12294 0
vsize: 49340
[startup+250.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 12022 0 0 0 24963 40 0 0 25 0 1 0 487879567 51859456 11940 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12661 11940 603 41 0 12620 0
vsize: 50644
[startup+260.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 12395 0 0 0 25962 41 0 0 25 0 1 0 487879567 53460992 12313 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13052 12313 603 41 0 13011 0
vsize: 52208
[startup+270.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 12660 0 0 0 26961 42 0 0 25 0 1 0 487879567 54530048 12578 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13313 12578 603 41 0 13272 0
vsize: 53252
[startup+280.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 12977 0 0 0 27960 43 0 0 25 0 1 0 487879567 55857152 12895 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13637 12895 603 41 0 13596 0
vsize: 54548
[startup+290.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 13266 0 0 0 28960 43 0 0 25 0 1 0 487879567 56926208 13184 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13898 13184 603 41 0 13857 0
vsize: 55592
[startup+300.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 13529 0 0 0 29959 44 0 0 25 0 1 0 487879567 57995264 13447 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14159 13447 603 41 0 14118 0
vsize: 56636
[startup+310.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 13748 0 0 0 30958 45 0 0 25 0 1 0 487879567 58933248 13666 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14388 13666 603 41 0 14347 0
vsize: 57552
[startup+320.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 14044 0 0 0 31958 45 0 0 25 0 1 0 487879567 60125184 13962 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14679 13962 603 41 0 14638 0
vsize: 58716
[startup+330.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 14228 0 0 0 32958 46 0 0 25 0 1 0 487879567 60928000 14146 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14875 14146 603 41 0 14834 0
vsize: 59500
[startup+340.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 14443 0 0 0 33957 46 0 0 25 0 1 0 487879567 61734912 14361 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15072 14361 603 41 0 15031 0
vsize: 60288
[startup+350.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 14707 0 0 0 34957 47 0 0 25 0 1 0 487879567 62808064 14625 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15334 14625 603 41 0 15293 0
vsize: 61336
[startup+360.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 14992 0 0 0 35956 48 0 0 25 0 1 0 487879567 64004096 14910 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15626 14910 603 41 0 15585 0
vsize: 62504
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 15197 0 0 0 36955 49 0 0 25 0 1 0 487879567 64802816 15115 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15821 15115 603 41 0 15780 0
vsize: 63284
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 15413 0 0 0 37955 49 0 0 25 0 1 0 487879567 65732608 15331 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16048 15331 603 41 0 16007 0
vsize: 64192
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 15761 0 0 0 38954 51 0 0 25 0 1 0 487879567 67207168 15679 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16408 15679 603 41 0 16367 0
vsize: 65632
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 16067 0 0 0 39954 51 0 0 25 0 1 0 487879567 68411392 15985 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16702 15985 603 41 0 16661 0
vsize: 66808
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 16316 0 0 0 40953 51 0 0 25 0 1 0 487879567 69484544 16234 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16964 16234 603 41 0 16923 0
vsize: 67856
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 16561 0 0 0 41953 52 0 0 25 0 1 0 487879567 70410240 16479 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17190 16479 603 41 0 17149 0
vsize: 68760
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 16695 0 0 0 42952 53 0 0 25 0 1 0 487879567 70942720 16613 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17320 16613 603 41 0 17279 0
vsize: 69280
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 17001 0 0 0 43952 53 0 0 25 0 1 0 487879567 72282112 16919 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17647 16919 603 41 0 17606 0
vsize: 70588
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 17268 0 0 0 44951 54 0 0 25 0 1 0 487879567 73351168 17186 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17908 17186 603 41 0 17867 0
vsize: 71632
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 17511 0 0 0 45951 55 0 0 25 0 1 0 487879567 74289152 17429 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18137 17429 603 41 0 18096 0
vsize: 72548
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 17750 0 0 0 46951 55 0 0 25 0 1 0 487879567 75210752 17668 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18362 17668 603 41 0 18321 0
vsize: 73448
[startup+480.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 17991 0 0 0 47950 56 0 0 25 0 1 0 487879567 76279808 17909 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18623 17909 603 41 0 18582 0
vsize: 74492
[startup+490.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 18264 0 0 0 48949 57 0 0 25 0 1 0 487879567 77340672 18182 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18882 18182 603 41 0 18841 0
vsize: 75528
[startup+500.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 18492 0 0 0 49949 58 0 0 25 0 1 0 487879567 78270464 18410 4294967295 134512640 134672761 3221224560 3221223728 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19109 18410 603 41 0 19068 0
vsize: 76436
[startup+510.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 18764 0 0 0 50948 59 0 0 25 0 1 0 487879567 79462400 18682 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19400 18682 603 41 0 19359 0
vsize: 77600
[startup+520.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 19048 0 0 0 51947 59 0 0 25 0 1 0 487879567 80531456 18966 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19661 18966 603 41 0 19620 0
vsize: 78644
[startup+530.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 19365 0 0 0 52947 60 0 0 25 0 1 0 487879567 81866752 19283 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19987 19283 603 41 0 19946 0
vsize: 79948
[startup+540.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 19608 0 0 0 53946 61 0 0 25 0 1 0 487879567 82800640 19526 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20215 19526 603 41 0 20174 0
vsize: 80860
[startup+550.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 19820 0 0 0 54946 61 0 0 25 0 1 0 487879567 83734528 19738 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20443 19738 603 41 0 20402 0
vsize: 81772
[startup+560.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 20084 0 0 0 55945 62 0 0 25 0 1 0 487879567 84807680 20002 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20705 20002 603 41 0 20664 0
vsize: 82820
[startup+570.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 20290 0 0 0 56944 63 0 0 25 0 1 0 487879567 85626880 20208 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20905 20208 603 41 0 20864 0
vsize: 83620
[startup+580.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 20505 0 0 0 57943 64 0 0 25 0 1 0 487879567 86560768 20423 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21133 20423 603 41 0 21092 0
vsize: 84532
[startup+590.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 20655 0 0 0 58943 64 0 0 25 0 1 0 487879567 87748608 20573 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21423 20573 603 41 0 21382 0
vsize: 85692
[startup+600.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 20780 0 0 0 59942 65 0 0 25 0 1 0 487879567 88141824 20698 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21519 20698 603 41 0 21478 0
vsize: 86076
[startup+610.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 20911 0 0 0 60942 65 0 0 25 0 1 0 487879567 88805376 20829 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21681 20829 603 41 0 21640 0
vsize: 86724
[startup+620.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 21183 0 0 0 61941 66 0 0 25 0 1 0 487879567 89858048 21101 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21938 21101 603 41 0 21897 0
vsize: 87752
[startup+630.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 21684 0 0 0 62941 67 0 0 25 0 1 0 487879567 91865088 21602 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22428 21602 603 41 0 22387 0
vsize: 89712
[startup+640.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 22060 0 0 0 63940 68 0 0 25 0 1 0 487879567 93466624 21978 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22819 21978 603 41 0 22778 0
vsize: 91276
[startup+650.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 22184 0 0 0 64940 68 0 0 25 0 1 0 487879567 94027776 22102 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22956 22102 603 41 0 22915 0
vsize: 91824
[startup+660.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 22335 0 0 0 65939 69 0 0 25 0 1 0 487879567 94564352 22253 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23087 22253 603 41 0 23046 0
vsize: 92348
[startup+670.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 22606 0 0 0 66939 70 0 0 25 0 1 0 487879567 95637504 22524 4294967295 134512640 134672761 3221224560 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23349 22524 603 41 0 23308 0
vsize: 93396
[startup+680.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 22875 0 0 0 67938 70 0 0 25 0 1 0 487879567 96706560 22793 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23610 22793 603 41 0 23569 0
vsize: 94440
[startup+690.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 23068 0 0 0 68938 71 0 0 25 0 1 0 487879567 97513472 22986 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23807 22986 603 41 0 23766 0
vsize: 95228
[startup+700.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 23250 0 0 0 69937 72 0 0 25 0 1 0 487879567 98316288 23168 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24003 23168 603 41 0 23962 0
vsize: 96012
[startup+710.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 23499 0 0 0 70937 72 0 0 25 0 1 0 487879567 99241984 23417 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24229 23417 603 41 0 24188 0
vsize: 96916
[startup+720.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 23689 0 0 0 71937 73 0 0 25 0 1 0 487879567 100036608 23607 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24423 23607 603 41 0 24382 0
vsize: 97692
[startup+730.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 23890 0 0 0 72936 73 0 0 25 0 1 0 487879567 100962304 23808 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24649 23808 603 41 0 24608 0
vsize: 98596
[startup+740.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 24040 0 0 0 73935 74 0 0 25 0 1 0 487879567 101498880 23958 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24780 23958 603 41 0 24739 0
vsize: 99120
[startup+750.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 24231 0 0 0 74935 75 0 0 25 0 1 0 487879567 102293504 24149 4294967295 134512640 134672761 3221224560 3221223664 134560303 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24974 24149 603 41 0 24933 0
vsize: 99896
[startup+760.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 24429 0 0 0 75935 76 0 0 25 0 1 0 487879567 103100416 24347 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25171 24347 603 41 0 25130 0
vsize: 100684
[startup+770.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 24652 0 0 0 76934 76 0 0 25 0 1 0 487879567 104034304 24570 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25399 24570 603 41 0 25358 0
vsize: 101596
[startup+780.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 24831 0 0 0 77934 77 0 0 25 0 1 0 487879567 104742912 24749 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25572 24749 603 41 0 25531 0
vsize: 102288
[startup+790.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 24986 0 0 0 78934 77 0 0 25 0 1 0 487879567 105406464 24904 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25734 24904 603 41 0 25693 0
vsize: 102936
[startup+800.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 25035 0 0 0 79934 77 0 0 25 0 1 0 487879567 105676800 24953 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25800 24953 603 41 0 25759 0
vsize: 103200
[startup+810.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 25312 0 0 0 80933 77 0 0 25 0 1 0 487879567 106733568 25230 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26058 25230 603 41 0 26017 0
vsize: 104232
[startup+820.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 25516 0 0 0 81933 78 0 0 25 0 1 0 487879567 107540480 25434 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26255 25434 603 41 0 26214 0
vsize: 105020
[startup+830.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 25609 0 0 0 82933 79 0 0 25 0 1 0 487879567 108068864 25527 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26384 25527 603 41 0 26343 0
vsize: 105536
[startup+840.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 25725 0 0 0 83932 79 0 0 25 0 1 0 487879567 108466176 25643 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26481 25643 603 41 0 26440 0
vsize: 105924
[startup+850.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 25854 0 0 0 84932 79 0 0 25 0 1 0 487879567 109047808 25772 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26623 25772 603 41 0 26582 0
vsize: 106492
[startup+860.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 25995 0 0 0 85932 80 0 0 25 0 1 0 487879567 109576192 25913 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26752 25913 603 41 0 26711 0
vsize: 107008
[startup+870.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 26150 0 0 0 86932 80 0 0 25 0 1 0 487879567 110235648 26068 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26913 26068 603 41 0 26872 0
vsize: 107652
[startup+880.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 26278 0 0 0 87932 80 0 0 25 0 1 0 487879567 110768128 26196 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27043 26196 603 41 0 27002 0
vsize: 108172
[startup+890.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 26461 0 0 0 88932 80 0 0 25 0 1 0 487879567 111587328 26379 4294967295 134512640 134672761 3221224560 3221223728 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27243 26379 603 41 0 27202 0
vsize: 108972
[startup+900.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 26589 0 0 0 89932 80 0 0 25 0 1 0 487879567 112119808 26507 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27373 26507 603 41 0 27332 0
vsize: 109492
[startup+910.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 26707 0 0 0 90932 81 0 0 25 0 1 0 487879567 112517120 26625 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27470 26625 603 41 0 27429 0
vsize: 109880
[startup+920.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 26815 0 0 0 91932 81 0 0 25 0 1 0 487879567 112930816 26733 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27571 26733 603 41 0 27530 0
vsize: 110284
[startup+930.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 27025 0 0 0 92931 82 0 0 25 0 1 0 487879567 113860608 26943 4294967295 134512640 134672761 3221224560 3221223696 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27798 26943 603 41 0 27757 0
vsize: 111192
[startup+940.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 27180 0 0 0 93931 82 0 0 25 0 1 0 487879567 114515968 27098 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27958 27098 603 41 0 27917 0
vsize: 111832
[startup+950.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 27350 0 0 0 94930 83 0 0 25 0 1 0 487879567 115179520 27268 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28120 27268 603 41 0 28079 0
vsize: 112480
[startup+960.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 27526 0 0 0 95930 84 0 0 25 0 1 0 487879567 115834880 27444 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28280 27444 603 41 0 28239 0
vsize: 113120
[startup+970.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 27697 0 0 0 96930 84 0 0 25 0 1 0 487879567 116490240 27615 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28440 27615 603 41 0 28399 0
vsize: 113760
[startup+980.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 27828 0 0 0 97929 85 0 0 25 0 1 0 487879567 117157888 27746 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28603 27746 603 41 0 28562 0
vsize: 114412
[startup+990.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 27880 0 0 0 98929 85 0 0 25 0 1 0 487879567 117293056 27798 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28636 27798 603 41 0 28595 0
vsize: 114544
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 27971 0 0 0 99929 85 0 0 25 0 1 0 487879567 117698560 27889 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28735 27889 603 41 0 28694 0
vsize: 114940
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 28066 0 0 0 100929 85 0 0 25 0 1 0 487879567 118099968 27984 4294967295 134512640 134672761 3221224560 3221223732 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28833 27984 603 41 0 28792 0
vsize: 115332
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 28172 0 0 0 101929 86 0 0 25 0 1 0 487879567 118497280 28090 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28930 28090 603 41 0 28889 0
vsize: 115720
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 28271 0 0 0 102929 86 0 0 25 0 1 0 487879567 118898688 28189 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29028 28189 603 41 0 28987 0
vsize: 116112
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 28384 0 0 0 103929 86 0 0 25 0 1 0 487879567 119316480 28302 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29130 28302 603 41 0 29089 0
vsize: 116520
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 28548 0 0 0 104929 86 0 0 25 0 1 0 487879567 119984128 28466 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29293 28466 603 41 0 29252 0
vsize: 117172
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 28704 0 0 0 105928 87 0 0 25 0 1 0 487879567 120684544 28622 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29464 28622 603 41 0 29423 0
vsize: 117856
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 28851 0 0 0 106928 88 0 0 25 0 1 0 487879567 121348096 28769 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29626 28769 603 41 0 29585 0
vsize: 118504
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 28996 0 0 0 107927 89 0 0 25 0 1 0 487879567 121872384 28914 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29754 28914 603 41 0 29713 0
vsize: 119016
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 29099 0 0 0 108927 89 0 0 25 0 1 0 487879567 122400768 29017 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29883 29017 603 41 0 29842 0
vsize: 119532
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 29186 0 0 0 109927 89 0 0 25 0 1 0 487879567 122662912 29104 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29947 29104 603 41 0 29906 0
vsize: 119788
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 29313 0 0 0 110927 90 0 0 25 0 1 0 487879567 123195392 29231 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30077 29231 603 41 0 30036 0
vsize: 120308
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 29448 0 0 0 111927 90 0 0 25 0 1 0 487879567 123727872 29366 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30207 29366 603 41 0 30166 0
vsize: 120828
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 29589 0 0 0 112927 90 0 0 25 0 1 0 487879567 124297216 29507 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30346 29507 603 41 0 30305 0
vsize: 121384
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 29688 0 0 0 113926 91 0 0 25 0 1 0 487879567 124698624 29606 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30444 29606 603 41 0 30403 0
vsize: 121776
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 29822 0 0 0 114926 91 0 0 25 0 1 0 487879567 125231104 29740 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30574 29740 603 41 0 30533 0
vsize: 122296
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 30006 0 0 0 115925 92 0 0 25 0 1 0 487879567 126029824 29924 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30769 29924 603 41 0 30728 0
vsize: 123076
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 30061 0 0 0 116925 92 0 0 25 0 1 0 487879567 126296064 29979 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30834 29979 603 41 0 30793 0
vsize: 123336
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 30113 0 0 0 117925 92 0 0 25 0 1 0 487879567 126427136 30031 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30866 30031 603 41 0 30825 0
vsize: 123464
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 30225 0 0 0 118925 93 0 0 25 0 1 0 487879567 126963712 30143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30997 30143 603 41 0 30956 0
vsize: 123988
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4060
Raw data (stat): 4060 (minisat+) R 4059 26298 26297 0 -1 0 30378 0 0 0 119925 93 0 0 25 0 1 0 487879567 127500288 30296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31128 30296 603 41 0 31087 0
vsize: 124512
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 4060
Raw data (stat): 4060 (minisat+) Z 4059 26298 26297 0 -1 12 30380 0 0 0 119925 98 0 0 25 0 1 0 487879567 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.07
CPU time (s): 1200.24
CPU user time (s): 1199.25
CPU system time (s): 0.988849
CPU usage (%): 100.015
Max. virtual memory (Kb): 124512
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####