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/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-l152lav.opb
MD5SUM	00855a9538cee8df79108d56ee6867b4
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5046
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	268
Number of bits of the biggest number in a constraint	9
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	1176.34
Number of variables	1989
Total number of constraints	2086
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	2085
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	1989
Trace number 19203

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-21 18:16:01 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16897 boxname=wulflinc18 idbench=1300 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  00855a9538cee8df79108d56ee6867b4  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-l152lav.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-l152lav.opb /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-l152lav.opb
IDLAUNCH: 16897
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        822708 kB
Buffers:         11200 kB
Cached:         177960 kB
SwapCached:        764 kB
Active:          62200 kB
Inactive:       128984 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        822456 kB
SwapTotal:     2097892 kB
SwapFree:      2096152 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            15052 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 18:36:03 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 16897 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): (none)
c ---[ 192]---> Adder-cost: 5478   maxlim: 25152   bits: 15/15
c ---[ 190]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 188]---> Adder-cost: 228   maxlim: 128   bits: 8/8
c ---[ 186]---> Adder-cost: 124   maxlim: 74   bits: 7/7
c ---[ 184]---> Adder-cost: 76   maxlim: 42   bits: 6/6
c ---[ 182]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[ 180]---> Adder-cost: 152   maxlim: 79   bits: 7/7
c ---[ 178]---> Adder-cost: 232   maxlim: 122   bits: 7/7
c ---[ 176]---> Adder-cost: 332   maxlim: 170   bits: 8/8
c ---[ 174]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 172]---> Adder-cost: 20   maxlim: 13   bits: 4/4
c ---[ 170]---> Adder-cost: 204   maxlim: 151   bits: 8/8
c ---[ 168]---> Adder-cost: 158   maxlim: 91   bits: 7/7
c ---[ 166]---> Adder-cost: 76   maxlim: 44   bits: 6/6
c ---[ 164]---> Adder-cost: 68   maxlim: 36   bits: 6/6
c ---[ 162]---> Adder-cost: 62   maxlim: 34   bits: 6/6
c ---[ 160]---> Adder-cost: 60   maxlim: 31   bits: 6/5
c ---[ 158]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[ 156]---> Adder-cost: 36   maxlim: 20   bits: 5/5
c ---[ 154]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[ 152]---> Adder-cost: 142   maxlim: 74   bits: 7/7
c ---[ 150]---> Adder-cost: 188   maxlim: 95   bits: 7/7
c ---[ 148]---> Adder-cost: 210   maxlim: 111   bits: 7/7
c ---[ 146]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[ 144]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 142]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 140]---> Adder-cost: 52   maxlim: 30   bits: 5/5
c ---[ 138]---> Adder-cost: 164   maxlim: 86   bits: 7/7
c ---[ 136]---> Adder-cost: 38   maxlim: 30   bits: 5/5
c ---[ 134]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[ 132]---> Adder-cost: 146   maxlim: 76   bits: 7/7
c ---[ 130]---> Adder-cost: 142   maxlim: 74   bits: 7/7
c ---[ 128]---> Adder-cost: 244   maxlim: 159   bits: 8/8
c ---[ 126]---> Adder-cost: 172   maxlim: 101   bits: 7/7
c ---[ 124]---> Adder-cost: 94   maxlim: 53   bits: 6/6
c ---[ 122]---> Adder-cost: 96   maxlim: 51   bits: 6/6
c ---[ 120]---> Adder-cost: 112   maxlim: 61   bits: 6/6
c ---[ 118]---> Adder-cost: 130   maxlim: 67   bits: 7/7
c ---[ 116]---> Adder-cost: 146   maxlim: 75   bits: 7/7
c ---[ 114]---> Adder-cost: 162   maxlim: 95   bits: 7/7
c ---[ 112]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 110]---> Adder-cost: 172   maxlim: 101   bits: 7/7
c ---[ 108]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[ 106]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[ 104]---> Adder-cost: 114   maxlim: 61   bits: 6/6
c ---[ 102]---> Adder-cost: 326   maxlim: 217   bits: 8/8
c ---[ 100]---> Adder-cost: 188   maxlim: 96   bits: 7/7
c ---[  98]---> Adder-cost: 68   maxlim: 41   bits: 6/6
c ---[  96]---> Adder-cost: 68   maxlim: 36   bits: 6/6
c ---[  94]---> Adder-cost: 82   maxlim: 52   bits: 6/6
c ---[  92]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[  90]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  88]---> Adder-cost: 138   maxlim: 95   bits: 7/7
c ---[  86]---> Adder-cost: 176   maxlim: 117   bits: 7/7
c ---[  84]---> Adder-cost: 94   maxlim: 51   bits: 6/6
c ---[  82]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[  80]---> Adder-cost: 166   maxlim: 87   bits: 7/7
c ---[  78]---> Adder-cost: 176   maxlim: 92   bits: 7/7
c ---[  76]---> Adder-cost: 168   maxlim: 87   bits: 7/7
c ---[  74]---> Adder-cost: 232   maxlim: 120   bits: 7/7
c ---[  72]---> Adder-cost: 84   maxlim: 46   bits: 6/6
c ---[  70]---> Adder-cost: 198   maxlim: 136   bits: 8/8
c ---[  68]---> Adder-cost: 192   maxlim: 120   bits: 7/7
c ---[  66]---> Adder-cost: 100   maxlim: 57   bits: 6/6
c ---[  64]---> Adder-cost: 106   maxlim: 59   bits: 6/6
c ---[  62]---> Adder-cost: 216   maxlim: 111   bits: 7/7
c ---[  60]---> Adder-cost: 208   maxlim: 107   bits: 7/7
c ---[  58]---> Adder-cost: 142   maxlim: 73   bits: 7/7
c ---[  56]---> Adder-cost: 174   maxlim: 91   bits: 7/7
c ---[  54]---> Adder-cost: 170   maxlim: 107   bits: 7/7
c ---[  52]---> Adder-cost: 140   maxlim: 72   bits: 7/7
c ---[  50]---> Adder-cost: 154   maxlim: 105   bits: 7/7
c ---[  48]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[  46]---> Adder-cost: 186   maxlim: 103   bits: 7/7
c ---[  44]---> Adder-cost: 62   maxlim: 31   bits: 6/5
c ---[  42]---> Adder-cost: 178   maxlim: 113   bits: 7/7
c ---[  40]---> Adder-cost: 128   maxlim: 65   bits: 7/7
c ---[  38]---> Adder-cost: 190   maxlim: 127   bits: 8/7
c ---[  36]---> Adder-cost: 68   maxlim: 36   bits: 6/6
c ---[  34]---> Adder-cost: 158   maxlim: 102   bits: 7/7
c ---[  32]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  30]---> Adder-cost: 132   maxlim: 67   bits: 7/7
c ---[  28]---> Adder-cost: 258   maxlim: 162   bits: 8/8
c ---[  26]---> Adder-cost: 138   maxlim: 78   bits: 7/7
c ---[  24]---> Adder-cost: 80   maxlim: 45   bits: 6/6
c ---[  22]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[  20]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  18]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[  16]---> Adder-cost: 130   maxlim: 67   bits: 7/7
c ---[  14]---> Adder-cost: 226   maxlim: 124   bits: 7/7
c ---[  12]---> Adder-cost: 90   maxlim: 55   bits: 6/6
c ---[  10]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[   8]---> Adder-cost: 142   maxlim: 76   bits: 7/7
c ---[   6]---> Adder-cost: 176   maxlim: 91   bits: 7/7
c ---[   4]---> Adder-cost: 148   maxlim: 77   bits: 7/7
c ---[   2]---> Adder-cost: 174   maxlim: 93   bits: 7/7
c ---[   0]---> Adder-cost: 3056   maxlim: 1961   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  139973   498633 |   46657       0        0     nan |  0.000 % |
c |       100 |  139530   497080 |   51322      45      167     3.7 |  5.990 % |
c |       250 |  138813   494625 |   56454     123      486     4.0 |  6.529 % |
c |       475 |  137994   491808 |   62100     267     1006     3.8 |  7.142 % |
c |       812 |  136671   487241 |   68310     449     1839     4.1 |  8.134 % |
c |      1321 |  135885   484501 |   75141     864     3812     4.4 |  8.708 % |
c |      2081 |  134619   480107 |   82655    1445     7067     4.9 |  9.619 % |
c |      3220 |  132781   473581 |   90921    2347    12305     5.2 | 10.965 % |
c |      4929 |  130600   465768 |  100013    3792    22092     5.8 | 12.566 % |
c |      7491 |  125418   447614 |  110014    5669    35987     6.3 | 16.282 % |
c |     11337 |  116832   417706 |  121016    8327    60123     7.2 | 22.336 % |
c |     17104 |  108231   387892 |  133117   12938   108538     8.4 | 28.093 % |
c |     25755 |  104747   375806 |  146429   21050   328019    15.6 | 30.221 % |
c |     38731 |  102297   367308 |  161072   33634  1243695    37.0 | 31.705 % |
c |     58192 |  100644   361583 |  177179   52816  3572014    67.6 | 32.723 % |
c |     87385 |   98584   354509 |  194897   81496  7234569    88.8 | 34.199 % |
c |    131174 |   96830   348435 |  214387  124937 12773613   102.2 | 35.442 % |
#### 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.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (runsolver) R 4286 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547158034 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 2946 0 0 0 991 7 0 0 25 0 1 0 547158034 14516224 2854 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3544 2854 603 41 0 3503 0
vsize: 14176
[startup+20.0017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 2981 0 0 0 1990 7 0 0 25 0 1 0 547158034 14651392 2889 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3577 2889 603 41 0 3536 0
vsize: 14308
[startup+30.0029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 2988 0 0 0 2991 7 0 0 25 0 1 0 547158034 14651392 2896 4294967295 134512640 134672761 3221224544 3221223712 134564725 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3577 2896 603 41 0 3536 0
vsize: 14308
[startup+40.0025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 2992 0 0 0 3991 7 0 0 25 0 1 0 547158034 14651392 2900 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3577 2900 603 41 0 3536 0
vsize: 14308
[startup+50.0036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 3007 0 0 0 4991 7 0 0 25 0 1 0 547158034 14815232 2915 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3617 2915 603 41 0 3576 0
vsize: 14468
[startup+60.0036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 3011 0 0 0 5990 8 0 0 25 0 1 0 547158034 14815232 2919 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3617 2919 603 41 0 3576 0
vsize: 14468
[startup+70.0043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 3015 0 0 0 6989 8 0 0 25 0 1 0 547158034 14815232 2923 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3617 2923 603 41 0 3576 0
vsize: 14468
[startup+80.0052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 3020 0 0 0 7989 8 0 0 25 0 1 0 547158034 14815232 2928 4294967295 134512640 134672761 3221224544 3221223732 134557974 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3617 2928 603 41 0 3576 0
vsize: 14468
[startup+90.0054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 3024 0 0 0 8990 8 0 0 25 0 1 0 547158034 14815232 2932 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3617 2932 603 41 0 3576 0
vsize: 14468
[startup+100.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 3036 0 0 0 9989 8 0 0 25 0 1 0 547158034 14815232 2944 4294967295 134512640 134672761 3221224544 3221223668 134566133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3617 2944 603 41 0 3576 0
vsize: 14468
[startup+110.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 3038 0 0 0 10989 8 0 0 25 0 1 0 547158034 14815232 2946 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3617 2946 603 41 0 3576 0
vsize: 14468
[startup+120.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 3050 0 0 0 11988 9 0 0 25 0 1 0 547158034 14946304 2958 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3649 2958 603 41 0 3608 0
vsize: 14596
[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 3071 0 0 0 12988 9 0 0 25 0 1 0 547158034 14946304 2979 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3649 2979 603 41 0 3608 0
vsize: 14596
[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 3130 0 0 0 13988 9 0 0 25 0 1 0 547158034 15212544 3038 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3714 3038 603 41 0 3673 0
vsize: 14856
[startup+150.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 3278 0 0 0 14988 10 0 0 25 0 1 0 547158034 15863808 3186 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3873 3186 603 41 0 3832 0
vsize: 15492
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 3454 0 0 0 15987 11 0 0 25 0 1 0 547158034 16531456 3362 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4036 3362 603 41 0 3995 0
vsize: 16144
[startup+170.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 3725 0 0 0 16986 12 0 0 25 0 1 0 547158034 17743872 3633 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4332 3633 603 41 0 4291 0
vsize: 17328
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 3964 0 0 0 17985 13 0 0 25 0 1 0 547158034 18681856 3872 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4561 3872 603 41 0 4520 0
vsize: 18244
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 4246 0 0 0 18984 14 0 0 25 0 1 0 547158034 19763200 4154 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4825 4154 603 41 0 4784 0
vsize: 19300
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 4572 0 0 0 19983 15 0 0 25 0 1 0 547158034 21237760 4480 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5185 4480 603 41 0 5144 0
vsize: 20740
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 4795 0 0 0 20983 16 0 0 25 0 1 0 547158034 22171648 4703 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5413 4703 603 41 0 5372 0
vsize: 21652
[startup+220.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 5132 0 0 0 21981 17 0 0 25 0 1 0 547158034 23502848 5040 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5738 5040 603 41 0 5697 0
vsize: 22952
[startup+230.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 5579 0 0 0 22980 19 0 0 25 0 1 0 547158034 25370624 5487 4294967295 134512640 134672761 3221224544 3221223696 134565212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6194 5487 603 41 0 6153 0
vsize: 24776
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 5913 0 0 0 23979 20 0 0 25 0 1 0 547158034 26705920 5821 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6520 5821 603 41 0 6479 0
vsize: 26080
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 6249 0 0 0 24978 21 0 0 25 0 1 0 547158034 28037120 6157 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6845 6157 603 41 0 6804 0
vsize: 27380
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 6551 0 0 0 25978 22 0 0 25 0 1 0 547158034 29368320 6459 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7170 6459 603 41 0 7129 0
vsize: 28680
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4287
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 6863 0 0 0 26976 23 0 0 25 0 1 0 547158034 30568448 6771 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7463 6771 603 41 0 7422 0
vsize: 29852
[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 7126 0 0 0 27976 24 0 0 25 0 1 0 547158034 31633408 7034 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7723 7034 603 41 0 7682 0
vsize: 30892
[startup+290.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 7374 0 0 0 28976 24 0 0 25 0 1 0 547158034 32702464 7282 4294967295 134512640 134672761 3221224544 3221223648 134555076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7984 7282 603 41 0 7943 0
vsize: 31936
[startup+300.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 7627 0 0 0 29975 25 0 0 25 0 1 0 547158034 33640448 7535 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8213 7535 603 41 0 8172 0
vsize: 32852
[startup+310.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 7821 0 0 0 30974 26 0 0 25 0 1 0 547158034 34439168 7729 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8408 7729 603 41 0 8367 0
vsize: 33632
[startup+320.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 8072 0 0 0 31973 27 0 0 25 0 1 0 547158034 35508224 7980 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8669 7980 603 41 0 8628 0
vsize: 34676
[startup+330.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 8345 0 0 0 32973 28 0 0 25 0 1 0 547158034 36573184 8253 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8929 8253 603 41 0 8888 0
vsize: 35716
[startup+340.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 8670 0 0 0 33972 29 0 0 25 0 1 0 547158034 37896192 8578 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9252 8578 603 41 0 9211 0
vsize: 37008
[startup+350.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 8963 0 0 0 34971 30 0 0 25 0 1 0 547158034 39350272 8871 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 8871 603 41 0 9566 0
vsize: 38428
[startup+360.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 9172 0 0 0 35971 30 0 0 25 0 1 0 547158034 40284160 9080 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9835 9080 603 41 0 9794 0
vsize: 39340
[startup+370.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 9415 0 0 0 36971 31 0 0 25 0 1 0 547158034 41218048 9323 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10063 9323 603 41 0 10022 0
vsize: 40252
[startup+380.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 9663 0 0 0 37970 32 0 0 25 0 1 0 547158034 42299392 9571 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10327 9571 603 41 0 10286 0
vsize: 41308
[startup+390.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 9807 0 0 0 38970 32 0 0 25 0 1 0 547158034 42835968 9715 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10458 9715 603 41 0 10417 0
vsize: 41832
[startup+400.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 10034 0 0 0 39969 33 0 0 25 0 1 0 547158034 43778048 9942 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10688 9942 603 41 0 10647 0
vsize: 42752
[startup+410.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 10244 0 0 0 40969 34 0 0 25 0 1 0 547158034 44580864 10152 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10884 10152 603 41 0 10843 0
vsize: 43536
[startup+420.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 10406 0 0 0 41969 34 0 0 25 0 1 0 547158034 45252608 10314 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11048 10314 603 41 0 11007 0
vsize: 44192
[startup+430.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 10576 0 0 0 42968 35 0 0 25 0 1 0 547158034 45916160 10484 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11210 10484 603 41 0 11169 0
vsize: 44840
[startup+440.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 10744 0 0 0 43968 36 0 0 25 0 1 0 547158034 46575616 10652 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11371 10652 603 41 0 11330 0
vsize: 45484
[startup+450.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 10943 0 0 0 44967 37 0 0 25 0 1 0 547158034 47501312 10851 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11597 10851 603 41 0 11556 0
vsize: 46388
[startup+460.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 11110 0 0 0 45966 37 0 0 25 0 1 0 547158034 48156672 11018 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11757 11018 603 41 0 11716 0
vsize: 47028
[startup+470.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 11327 0 0 0 46966 38 0 0 25 0 1 0 547158034 49086464 11235 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11984 11235 603 41 0 11943 0
vsize: 47936
[startup+480.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 11533 0 0 0 47965 38 0 0 25 0 1 0 547158034 49889280 11441 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12180 11441 603 41 0 12139 0
vsize: 48720
[startup+490.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 11752 0 0 0 48965 38 0 0 25 0 1 0 547158034 50819072 11660 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12407 11660 603 41 0 12366 0
vsize: 49628
[startup+500.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 11974 0 0 0 49965 39 0 0 25 0 1 0 547158034 51621888 11882 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12603 11882 603 41 0 12562 0
vsize: 50412
[startup+510.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 12152 0 0 0 50964 40 0 0 25 0 1 0 547158034 52416512 12060 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12797 12060 603 41 0 12756 0
vsize: 51188
[startup+520.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 12349 0 0 0 51963 41 0 0 25 0 1 0 547158034 53211136 12257 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12991 12257 603 41 0 12950 0
vsize: 51964
[startup+530.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 12510 0 0 0 52963 41 0 0 25 0 1 0 547158034 53878784 12418 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13154 12418 603 41 0 13113 0
vsize: 52616
[startup+540.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 12676 0 0 0 53962 42 0 0 25 0 1 0 547158034 54546432 12584 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13317 12584 603 41 0 13276 0
vsize: 53268
[startup+550.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 12864 0 0 0 54962 43 0 0 25 0 1 0 547158034 55357440 12772 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13515 12772 603 41 0 13474 0
vsize: 54060
[startup+560.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 13020 0 0 0 55961 43 0 0 25 0 1 0 547158034 55889920 12928 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13645 12928 603 41 0 13604 0
vsize: 54580
[startup+570.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4289
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 13177 0 0 0 56961 44 0 0 25 0 1 0 547158034 56553472 13085 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13807 13085 603 41 0 13766 0
vsize: 55228
[startup+580.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 13360 0 0 0 57961 45 0 0 25 0 1 0 547158034 57348096 13268 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14001 13268 603 41 0 13960 0
vsize: 56004
[startup+590.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 13496 0 0 0 58961 45 0 0 25 0 1 0 547158034 57884672 13404 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14132 13404 603 41 0 14091 0
vsize: 56528
[startup+600.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 13686 0 0 0 59961 45 0 0 25 0 1 0 547158034 58679296 13594 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14326 13594 603 41 0 14285 0
vsize: 57304
[startup+610.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 13860 0 0 0 60960 46 0 0 25 0 1 0 547158034 59346944 13768 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14489 13768 603 41 0 14448 0
vsize: 57956
[startup+620.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 14034 0 0 0 61960 46 0 0 25 0 1 0 547158034 60145664 13942 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14684 13942 603 41 0 14643 0
vsize: 58736
[startup+630.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 14212 0 0 0 62960 46 0 0 25 0 1 0 547158034 60809216 14120 4294967295 134512640 134672761 3221224544 3221223744 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14846 14120 603 41 0 14805 0
vsize: 59384
[startup+640.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 14379 0 0 0 63960 46 0 0 25 0 1 0 547158034 61476864 14287 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15009 14287 603 41 0 14968 0
vsize: 60036
[startup+650.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 14516 0 0 0 64960 47 0 0 25 0 1 0 547158034 62005248 14424 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14424 603 41 0 15097 0
vsize: 60552
[startup+660.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 14698 0 0 0 65959 48 0 0 25 0 1 0 547158034 62824448 14606 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15338 14606 603 41 0 15297 0
vsize: 61352
[startup+670.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 14872 0 0 0 66959 48 0 0 25 0 1 0 547158034 63492096 14780 4294967295 134512640 134672761 3221224544 3221223728 134558918 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15501 14780 603 41 0 15460 0
vsize: 62004
[startup+680.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 15062 0 0 0 67959 48 0 0 25 0 1 0 547158034 64294912 14970 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15697 14970 603 41 0 15656 0
vsize: 62788
[startup+690.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 15223 0 0 0 68958 49 0 0 25 0 1 0 547158034 64962560 15131 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15860 15131 603 41 0 15819 0
vsize: 63440
[startup+700.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 15380 0 0 0 69958 50 0 0 25 0 1 0 547158034 65630208 15288 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16023 15288 603 41 0 15982 0
vsize: 64092
[startup+710.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 15602 0 0 0 70957 50 0 0 25 0 1 0 547158034 66555904 15510 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16249 15510 603 41 0 16208 0
vsize: 64996
[startup+720.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 15816 0 0 0 71957 51 0 0 25 0 1 0 547158034 67362816 15724 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16446 15724 603 41 0 16405 0
vsize: 65784
[startup+730.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 16007 0 0 0 72957 52 0 0 25 0 1 0 547158034 68157440 15915 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16640 15915 603 41 0 16599 0
vsize: 66560
[startup+740.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 16212 0 0 0 73956 53 0 0 25 0 1 0 547158034 68956160 16120 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16835 16120 603 41 0 16794 0
vsize: 67340
[startup+750.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 16406 0 0 0 74956 53 0 0 25 0 1 0 547158034 69758976 16314 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17031 16314 603 41 0 16990 0
vsize: 68124
[startup+760.037 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 16603 0 0 0 75955 54 0 0 25 0 1 0 547158034 70557696 16511 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17226 16511 603 41 0 17185 0
vsize: 68904
[startup+770.038 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 16742 0 0 0 76955 55 0 0 25 0 1 0 547158034 71094272 16650 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17357 16650 603 41 0 17316 0
vsize: 69428
[startup+780.038 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 16947 0 0 0 77954 55 0 0 25 0 1 0 547158034 72028160 16855 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17585 16855 603 41 0 17544 0
vsize: 70340
[startup+790.037 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 17060 0 0 0 78953 56 0 0 25 0 1 0 547158034 72429568 16968 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17683 16968 603 41 0 17642 0
vsize: 70732
[startup+800.038 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 17232 0 0 0 79953 56 0 0 25 0 1 0 547158034 73089024 17140 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17844 17140 603 41 0 17803 0
vsize: 71376
[startup+810.039 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 17445 0 0 0 80952 57 0 0 25 0 1 0 547158034 74014720 17353 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18070 17353 603 41 0 18029 0
vsize: 72280
[startup+820.039 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 17594 0 0 0 81952 58 0 0 25 0 1 0 547158034 74555392 17502 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18202 17502 603 41 0 18161 0
vsize: 72808
[startup+830.04 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 17777 0 0 0 82951 58 0 0 25 0 1 0 547158034 75874304 17685 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18524 17685 603 41 0 18483 0
vsize: 74096
[startup+840.04 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 17975 0 0 0 83951 59 0 0 25 0 1 0 547158034 76664832 17883 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18717 17883 603 41 0 18676 0
vsize: 74868
[startup+850.041 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 18090 0 0 0 84951 59 0 0 25 0 1 0 547158034 77193216 17998 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18846 17998 603 41 0 18805 0
vsize: 75384
[startup+860.042 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 18222 0 0 0 85951 60 0 0 25 0 1 0 547158034 77725696 18130 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18976 18130 603 41 0 18935 0
vsize: 75904
[startup+870.043 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 4291
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 18369 0 0 0 86951 60 0 0 25 0 1 0 547158034 78249984 18277 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19104 18277 603 41 0 19063 0
vsize: 76416
[startup+880.044 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 18504 0 0 0 87951 60 0 0 25 0 1 0 547158034 78790656 18412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19236 18412 603 41 0 19195 0
vsize: 76944
[startup+890.044 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 18769 0 0 0 88950 61 0 0 25 0 1 0 547158034 79888384 18677 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 18677 603 41 0 19463 0
vsize: 78016
[startup+900.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 18919 0 0 0 89950 61 0 0 25 0 1 0 547158034 80556032 18827 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19667 18827 603 41 0 19626 0
vsize: 78668
[startup+910.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 19080 0 0 0 90949 62 0 0 25 0 1 0 547158034 81215488 18988 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19828 18988 603 41 0 19787 0
vsize: 79312
[startup+920.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 19337 0 0 0 91949 63 0 0 25 0 1 0 547158034 82288640 19245 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20090 19245 603 41 0 20049 0
vsize: 80360
[startup+930.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 19508 0 0 0 92948 64 0 0 25 0 1 0 547158034 82964480 19416 4294967295 134512640 134672761 3221224544 3221223728 134558925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20255 19416 603 41 0 20214 0
vsize: 81020
[startup+940.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 19625 0 0 0 93948 64 0 0 25 0 1 0 547158034 83501056 19533 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20386 19533 603 41 0 20345 0
vsize: 81544
[startup+950.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 19733 0 0 0 94948 65 0 0 25 0 1 0 547158034 83906560 19641 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20485 19641 603 41 0 20444 0
vsize: 81940
[startup+960.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 19826 0 0 0 95948 65 0 0 25 0 1 0 547158034 84357120 19734 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20595 19734 603 41 0 20554 0
vsize: 82380
[startup+970.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 19948 0 0 0 96948 65 0 0 25 0 1 0 547158034 84758528 19856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20693 19856 603 41 0 20652 0
vsize: 82772
[startup+980.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 20078 0 0 0 97948 65 0 0 25 0 1 0 547158034 85323776 19986 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20831 19986 603 41 0 20790 0
vsize: 83324
[startup+990.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 20174 0 0 0 98948 65 0 0 25 0 1 0 547158034 85733376 20082 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20931 20082 603 41 0 20890 0
vsize: 83724
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 20312 0 0 0 99948 66 0 0 25 0 1 0 547158034 86274048 20220 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21063 20220 603 41 0 21022 0
vsize: 84252
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 20462 0 0 0 100947 66 0 0 25 0 1 0 547158034 86937600 20370 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21225 20370 603 41 0 21184 0
vsize: 84900
[startup+1020.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 20609 0 0 0 101947 67 0 0 25 0 1 0 547158034 87470080 20517 4294967295 134512640 134672761 3221224544 3221223648 134560237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21388 20517 603 41 0 21347 0
vsize: 85420
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 20748 0 0 0 102946 68 0 0 25 0 1 0 547158034 88133632 20656 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21517 20656 603 41 0 21476 0
vsize: 86068
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 20912 0 0 0 103946 68 0 0 25 0 1 0 547158034 88817664 20820 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21684 20820 603 41 0 21643 0
vsize: 86736
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 21055 0 0 0 104946 69 0 0 25 0 1 0 547158034 89350144 20963 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21814 20963 603 41 0 21773 0
vsize: 87256
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 21200 0 0 0 105945 69 0 0 25 0 1 0 547158034 90017792 21108 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21977 21108 603 41 0 21936 0
vsize: 87908
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 21372 0 0 0 106945 70 0 0 25 0 1 0 547158034 90677248 21280 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22138 21280 603 41 0 22097 0
vsize: 88552
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 21529 0 0 0 107944 71 0 0 25 0 1 0 547158034 91336704 21437 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22299 21437 603 41 0 22258 0
vsize: 89196
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 21661 0 0 0 108944 71 0 0 25 0 1 0 547158034 91873280 21569 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22430 21569 603 41 0 22389 0
vsize: 89720
[startup+1100.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 21775 0 0 0 109944 71 0 0 25 0 1 0 547158034 92274688 21683 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22528 21683 603 41 0 22487 0
vsize: 90112
[startup+1110.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 21905 0 0 0 110945 72 0 0 25 0 1 0 547158034 92807168 21813 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22658 21813 603 41 0 22617 0
vsize: 90632
[startup+1120.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 21999 0 0 0 111945 72 0 0 25 0 1 0 547158034 93200384 21907 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22754 21907 603 41 0 22713 0
vsize: 91016
[startup+1130.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 22116 0 0 0 112945 72 0 0 25 0 1 0 547158034 93736960 22024 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22885 22024 603 41 0 22844 0
vsize: 91540
[startup+1140.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 22242 0 0 0 113945 73 0 0 25 0 1 0 547158034 94273536 22150 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23016 22150 603 41 0 22975 0
vsize: 92064
[startup+1150.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 22351 0 0 0 114945 73 0 0 25 0 1 0 547158034 94679040 22259 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23115 22259 603 41 0 23074 0
vsize: 92460
[startup+1160.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 22481 0 0 0 115944 74 0 0 25 0 1 0 547158034 95215616 22389 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23246 22389 603 41 0 23205 0
vsize: 92984
[startup+1170.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4293
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 22647 0 0 0 116944 74 0 0 25 0 1 0 547158034 95895552 22555 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23412 22555 603 41 0 23371 0
vsize: 93648
[startup+1180.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4295
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 22785 0 0 0 117944 75 0 0 25 0 1 0 547158034 96432128 22693 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23543 22693 603 41 0 23502 0
vsize: 94172
[startup+1190.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4295
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 22876 0 0 0 118944 75 0 0 25 0 1 0 547158034 96829440 22784 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23640 22784 603 41 0 23599 0
vsize: 94560
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4295
Raw data (stat): 4287 (minisat+) R 4286 20024 20023 0 -1 0 22998 0 0 0 119944 75 0 0 25 0 1 0 547158034 97341440 22906 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23765 22906 603 41 0 23724 0
vsize: 95060
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.91 1/55 4295
Raw data (stat): 4287 (minisat+) Z 4286 20024 20023 0 -1 12 23000 0 0 0 119944 79 0 0 25 0 1 0 547158034 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: 0
Real time (s): 1200.11
CPU time (s): 1200.24
CPU user time (s): 1199.44
CPU system time (s): 0.796878
CPU usage (%): 100.01
Max. virtual memory (Kb): 95060
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####