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/miplib3/normalized-mps-v2-13-7-l152lav.opb
MD5SUM	9d4ce12b138a2bef65a1f401ec9d1f01
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	1175.69
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 18180

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        307452 kB
Buffers:         31408 kB
Cached:         671604 kB
SwapCached:        516 kB
Active:         175248 kB
Inactive:       529772 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        307200 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            16616 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 14:10:42 (client local time) WITH STATUS 0 IN 1200.27 SECONDS
stats: 18483 7 1200.27 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.85 0.95 0.91 2/54 8169
Raw data (stat): 8169 (runsolver) R 8168 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545573827 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.0009 s]
Raw data (loadavg): 0.87 0.95 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 2946 0 0 0 992 7 0 0 25 0 1 0 545573827 14516224 2854 4294967295 134512640 134672761 3221224544 3221223716 134556651 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.89 0.96 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 2979 0 0 0 1992 7 0 0 25 0 1 0 545573827 14651392 2887 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3577 2887 603 41 0 3536 0
vsize: 14308
[startup+30.002 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 2988 0 0 0 2991 7 0 0 25 0 1 0 545573827 14651392 2896 4294967295 134512640 134672761 3221224544 3221223692 134565968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3577 2896 603 41 0 3536 0
vsize: 14308
[startup+40.009 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 2992 0 0 0 3992 8 0 0 25 0 1 0 545573827 14651392 2900 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3577 2900 603 41 0 3536 0
vsize: 14308
[startup+50.0107 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 3007 0 0 0 4992 8 0 0 25 0 1 0 545573827 14815232 2915 4294967295 134512640 134672761 3221224544 3221223716 134556653 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.0101 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 3011 0 0 0 5992 8 0 0 25 0 1 0 545573827 14815232 2919 4294967295 134512640 134672761 3221224544 3221223696 134565073 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.0112 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 3015 0 0 0 6992 8 0 0 25 0 1 0 545573827 14815232 2923 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3617 2923 603 41 0 3576 0
vsize: 14468
[startup+80.0119 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 3020 0 0 0 7992 9 0 0 25 0 1 0 545573827 14815232 2928 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3617 2928 603 41 0 3576 0
vsize: 14468
[startup+90.0112 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 3024 0 0 0 8992 9 0 0 25 0 1 0 545573827 14815232 2932 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3617 2932 603 41 0 3576 0
vsize: 14468
[startup+100.011 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 3036 0 0 0 9992 9 0 0 25 0 1 0 545573827 14815232 2944 4294967295 134512640 134672761 3221224544 3221223712 134560806 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.012 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 3038 0 0 0 10991 9 0 0 25 0 1 0 545573827 14815232 2946 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.012 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 3048 0 0 0 11991 10 0 0 25 0 1 0 545573827 14946304 2956 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3649 2956 603 41 0 3608 0
vsize: 14596
[startup+130.013 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 3069 0 0 0 12991 10 0 0 25 0 1 0 545573827 14946304 2977 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3649 2977 603 41 0 3608 0
vsize: 14596
[startup+140.013 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 3128 0 0 0 13990 11 0 0 25 0 1 0 545573827 15212544 3036 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3714 3036 603 41 0 3673 0
vsize: 14856
[startup+150.014 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 3272 0 0 0 14989 12 0 0 25 0 1 0 545573827 15863808 3180 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3873 3180 603 41 0 3832 0
vsize: 15492
[startup+160.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 3452 0 0 0 15989 12 0 0 25 0 1 0 545573827 16531456 3360 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4036 3360 603 41 0 3995 0
vsize: 16144
[startup+170.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 3718 0 0 0 16988 14 0 0 25 0 1 0 545573827 17608704 3626 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4299 3626 603 41 0 4258 0
vsize: 17196
[startup+180.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 3949 0 0 0 17987 15 0 0 25 0 1 0 545573827 18546688 3857 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4528 3857 603 41 0 4487 0
vsize: 18112
[startup+190.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 4241 0 0 0 18986 16 0 0 25 0 1 0 545573827 19763200 4149 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4825 4149 603 41 0 4784 0
vsize: 19300
[startup+200.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 4567 0 0 0 19984 17 0 0 25 0 1 0 545573827 21237760 4475 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5185 4475 603 41 0 5144 0
vsize: 20740
[startup+210.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 4793 0 0 0 20984 18 0 0 25 0 1 0 545573827 22171648 4701 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5413 4701 603 41 0 5372 0
vsize: 21652
[startup+220.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 5136 0 0 0 21984 18 0 0 25 0 1 0 545573827 23502848 5044 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5738 5044 603 41 0 5697 0
vsize: 22952
[startup+230.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 5591 0 0 0 22983 19 0 0 25 0 1 0 545573827 25370624 5499 4294967295 134512640 134672761 3221224544 3221223728 134558930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6194 5499 603 41 0 6153 0
vsize: 24776
[startup+240.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 5916 0 0 0 23982 20 0 0 25 0 1 0 545573827 26705920 5824 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6520 5824 603 41 0 6479 0
vsize: 26080
[startup+250.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 6265 0 0 0 24982 21 0 0 25 0 1 0 545573827 28168192 6173 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6877 6173 603 41 0 6836 0
vsize: 27508
[startup+260.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 6578 0 0 0 25981 22 0 0 25 0 1 0 545573827 29368320 6486 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7170 6486 603 41 0 7129 0
vsize: 28680
[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 6884 0 0 0 26980 23 0 0 25 0 1 0 545573827 30699520 6792 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7495 6792 603 41 0 7454 0
vsize: 29980
[startup+280.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 7145 0 0 0 27979 24 0 0 25 0 1 0 545573827 31768576 7053 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7756 7053 603 41 0 7715 0
vsize: 31024
[startup+290.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 7396 0 0 0 28979 25 0 0 25 0 1 0 545573827 32702464 7304 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7984 7304 603 41 0 7943 0
vsize: 31936
[startup+300.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 7635 0 0 0 29979 25 0 0 25 0 1 0 545573827 33775616 7543 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8246 7543 603 41 0 8205 0
vsize: 32984
[startup+310.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 7855 0 0 0 30978 26 0 0 25 0 1 0 545573827 34574336 7763 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8441 7763 603 41 0 8400 0
vsize: 33764
[startup+320.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 8109 0 0 0 31978 26 0 0 25 0 1 0 545573827 35639296 8017 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8701 8017 603 41 0 8660 0
vsize: 34804
[startup+330.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 8374 0 0 0 32977 27 0 0 25 0 1 0 545573827 36704256 8282 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8961 8282 603 41 0 8920 0
vsize: 35844
[startup+340.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 8718 0 0 0 33976 28 0 0 25 0 1 0 545573827 38162432 8626 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9317 8626 603 41 0 9276 0
vsize: 37268
[startup+350.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 9001 0 0 0 34975 29 0 0 25 0 1 0 545573827 39481344 8909 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9639 8909 603 41 0 9598 0
vsize: 38556
[startup+360.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 9206 0 0 0 35974 30 0 0 25 0 1 0 545573827 40415232 9114 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9867 9114 603 41 0 9826 0
vsize: 39468
[startup+370.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 9453 0 0 0 36974 31 0 0 25 0 1 0 545573827 41349120 9361 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10095 9361 603 41 0 10054 0
vsize: 40380
[startup+380.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 9699 0 0 0 37973 32 0 0 25 0 1 0 545573827 42434560 9607 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10360 9607 603 41 0 10319 0
vsize: 41440
[startup+390.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 9854 0 0 0 38973 32 0 0 25 0 1 0 545573827 42971136 9762 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10491 9762 603 41 0 10450 0
vsize: 41964
[startup+400.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 10079 0 0 0 39973 33 0 0 25 0 1 0 545573827 43909120 9987 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10720 9987 603 41 0 10679 0
vsize: 42880
[startup+410.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 10284 0 0 0 40972 34 0 0 25 0 1 0 545573827 44711936 10192 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10916 10192 603 41 0 10875 0
vsize: 43664
[startup+420.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 10437 0 0 0 41971 35 0 0 25 0 1 0 545573827 45387776 10345 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11081 10345 603 41 0 11040 0
vsize: 44324
[startup+430.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 10612 0 0 0 42971 35 0 0 25 0 1 0 545573827 46047232 10520 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11242 10520 603 41 0 11201 0
vsize: 44968
[startup+440.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 10804 0 0 0 43971 35 0 0 25 0 1 0 545573827 46845952 10712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11437 10712 603 41 0 11396 0
vsize: 45748
[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 10994 0 0 0 44970 36 0 0 25 0 1 0 545573827 47632384 10902 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11629 10902 603 41 0 11588 0
vsize: 46516
[startup+460.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 11182 0 0 0 45970 37 0 0 25 0 1 0 545573827 48418816 11090 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11821 11090 603 41 0 11780 0
vsize: 47284
[startup+470.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 11400 0 0 0 46969 37 0 0 25 0 1 0 545573827 49352704 11308 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12049 11308 603 41 0 12008 0
vsize: 48196
[startup+480.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 11600 0 0 0 47970 38 0 0 25 0 1 0 545573827 50155520 11508 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12245 11508 603 41 0 12204 0
vsize: 48980
[startup+490.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 11796 0 0 0 48970 38 0 0 25 0 1 0 545573827 50954240 11704 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12440 11704 603 41 0 12399 0
vsize: 49760
[startup+500.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 12049 0 0 0 49970 39 0 0 25 0 1 0 545573827 52023296 11957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12701 11957 603 41 0 12660 0
vsize: 50804
[startup+510.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 12218 0 0 0 50969 40 0 0 25 0 1 0 545573827 52678656 12126 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12861 12126 603 41 0 12820 0
vsize: 51444
[startup+520.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 12416 0 0 0 51969 40 0 0 25 0 1 0 545573827 53477376 12324 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13056 12324 603 41 0 13015 0
vsize: 52224
[startup+530.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 12555 0 0 0 52969 40 0 0 25 0 1 0 545573827 54013952 12463 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13187 12463 603 41 0 13146 0
vsize: 52748
[startup+540.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 12718 0 0 0 53968 41 0 0 25 0 1 0 545573827 54681600 12626 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13350 12626 603 41 0 13309 0
vsize: 53400
[startup+550.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 12949 0 0 0 54968 42 0 0 25 0 1 0 545573827 55623680 12857 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13580 12857 603 41 0 13539 0
vsize: 54320
[startup+560.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8169
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 13112 0 0 0 55967 43 0 0 25 0 1 0 545573827 56287232 13020 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13742 13020 603 41 0 13701 0
vsize: 54968
[startup+570.039 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 8222
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 13270 0 0 0 56962 48 0 0 25 0 1 0 545573827 56950784 13178 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13904 13178 603 41 0 13863 0
vsize: 55616
[startup+580.039 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 8222
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 13423 0 0 0 57962 48 0 0 25 0 1 0 545573827 57618432 13331 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14067 13331 603 41 0 14026 0
vsize: 56268
[startup+590.039 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 8222
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 13586 0 0 0 58962 48 0 0 25 0 1 0 545573827 58286080 13494 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14230 13494 603 41 0 14189 0
vsize: 56920
[startup+600.039 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 8222
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 13776 0 0 0 59961 49 0 0 25 0 1 0 545573827 59076608 13684 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14423 13684 603 41 0 14382 0
vsize: 57692
[startup+610.039 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 8222
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 13949 0 0 0 60961 50 0 0 25 0 1 0 545573827 59752448 13857 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14588 13857 603 41 0 14547 0
vsize: 58352
[startup+620.04 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 8222
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 14121 0 0 0 61961 50 0 0 25 0 1 0 545573827 60411904 14029 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14749 14029 603 41 0 14708 0
vsize: 58996
[startup+630.04 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 8222
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 14289 0 0 0 62961 50 0 0 25 0 1 0 545573827 61075456 14197 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14911 14197 603 41 0 14870 0
vsize: 59644
[startup+640.04 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 14438 0 0 0 63960 51 0 0 25 0 1 0 545573827 61743104 14346 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15074 14346 603 41 0 15033 0
vsize: 60296
[startup+650.041 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 14625 0 0 0 64960 52 0 0 25 0 1 0 545573827 62423040 14533 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15240 14533 603 41 0 15199 0
vsize: 60960
[startup+660.041 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 14780 0 0 0 65960 52 0 0 25 0 1 0 545573827 63090688 14688 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15403 14688 603 41 0 15362 0
vsize: 61612
[startup+670.041 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 14955 0 0 0 66959 53 0 0 25 0 1 0 545573827 63897600 14863 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15600 14863 603 41 0 15559 0
vsize: 62400
[startup+680.041 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 15130 0 0 0 67959 53 0 0 25 0 1 0 545573827 64557056 15038 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15761 15038 603 41 0 15720 0
vsize: 63044
[startup+690.041 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 15333 0 0 0 68958 54 0 0 25 0 1 0 545573827 65363968 15241 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15958 15241 603 41 0 15917 0
vsize: 63832
[startup+700.042 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 15502 0 0 0 69958 54 0 0 25 0 1 0 545573827 66162688 15410 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16153 15410 603 41 0 16112 0
vsize: 64612
[startup+710.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 15722 0 0 0 70958 54 0 0 25 0 1 0 545573827 66957312 15630 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16347 15630 603 41 0 16306 0
vsize: 65388
[startup+720.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 15925 0 0 0 71957 55 0 0 25 0 1 0 545573827 67760128 15833 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16543 15833 603 41 0 16502 0
vsize: 66172
[startup+730.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 16140 0 0 0 72957 56 0 0 25 0 1 0 545573827 68685824 16048 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16769 16048 603 41 0 16728 0
vsize: 67076
[startup+740.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 16320 0 0 0 73956 57 0 0 25 0 1 0 545573827 69357568 16228 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16933 16228 603 41 0 16892 0
vsize: 67732
[startup+750.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 16526 0 0 0 74956 57 0 0 25 0 1 0 545573827 70299648 16434 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17163 16434 603 41 0 17122 0
vsize: 68652
[startup+760.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 16698 0 0 0 75956 57 0 0 25 0 1 0 545573827 70959104 16606 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17324 16606 603 41 0 17283 0
vsize: 69296
[startup+770.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 16898 0 0 0 76956 58 0 0 25 0 1 0 545573827 71761920 16806 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17520 16806 603 41 0 17479 0
vsize: 70080
[startup+780.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 17015 0 0 0 77955 58 0 0 25 0 1 0 545573827 72298496 16923 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17651 16923 603 41 0 17610 0
vsize: 70604
[startup+790.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 17177 0 0 0 78955 59 0 0 25 0 1 0 545573827 72826880 17085 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17780 17085 603 41 0 17739 0
vsize: 71120
[startup+800.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 17372 0 0 0 79955 59 0 0 25 0 1 0 545573827 73752576 17280 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18006 17280 603 41 0 17965 0
vsize: 72024
[startup+810.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 17558 0 0 0 80954 60 0 0 25 0 1 0 545573827 74424320 17466 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18170 17466 603 41 0 18129 0
vsize: 72680
[startup+820.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 17704 0 0 0 81954 61 0 0 25 0 1 0 545573827 75612160 17612 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18460 17612 603 41 0 18419 0
vsize: 73840
[startup+830.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 17935 0 0 0 82953 61 0 0 25 0 1 0 545573827 76537856 17843 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18686 17843 603 41 0 18645 0
vsize: 74744
[startup+840.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 18043 0 0 0 83953 62 0 0 25 0 1 0 545573827 76926976 17951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18781 17951 603 41 0 18740 0
vsize: 75124
[startup+850.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 18205 0 0 0 84953 62 0 0 25 0 1 0 545573827 77594624 18113 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18944 18113 603 41 0 18903 0
vsize: 75776
[startup+860.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 18339 0 0 0 85952 63 0 0 25 0 1 0 545573827 78114816 18247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19071 18247 603 41 0 19030 0
vsize: 76284
[startup+870.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 18480 0 0 0 86952 63 0 0 25 0 1 0 545573827 78790656 18388 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19236 18388 603 41 0 19195 0
vsize: 76944
[startup+880.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8224
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 18712 0 0 0 87952 63 0 0 25 0 1 0 545573827 79757312 18620 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19472 18620 603 41 0 19431 0
vsize: 77888
[startup+890.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 18905 0 0 0 88951 64 0 0 25 0 1 0 545573827 80556032 18813 4294967295 134512640 134672761 3221224544 3221223668 134566106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19667 18813 603 41 0 19626 0
vsize: 78668
[startup+900.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 19064 0 0 0 89951 65 0 0 25 0 1 0 545573827 81215488 18972 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19828 18972 603 41 0 19787 0
vsize: 79312
[startup+910.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 19293 0 0 0 90951 65 0 0 25 0 1 0 545573827 82022400 19201 4294967295 134512640 134672761 3221224544 3221223728 134559373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20025 19201 603 41 0 19984 0
vsize: 80100
[startup+920.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 19489 0 0 0 91951 66 0 0 25 0 1 0 545573827 82833408 19397 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20223 19397 603 41 0 20182 0
vsize: 80892
[startup+930.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 19607 0 0 0 92950 66 0 0 25 0 1 0 545573827 83365888 19515 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20353 19515 603 41 0 20312 0
vsize: 81412
[startup+940.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 19718 0 0 0 93951 66 0 0 25 0 1 0 545573827 83906560 19626 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20485 19626 603 41 0 20444 0
vsize: 81940
[startup+950.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 19810 0 0 0 94950 66 0 0 25 0 1 0 545573827 84176896 19718 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20551 19718 603 41 0 20510 0
vsize: 82204
[startup+960.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 19935 0 0 0 95950 67 0 0 25 0 1 0 545573827 84758528 19843 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20693 19843 603 41 0 20652 0
vsize: 82772
[startup+970.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 20065 0 0 0 96950 67 0 0 25 0 1 0 545573827 85323776 19973 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20831 19973 603 41 0 20790 0
vsize: 83324
[startup+980.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 20162 0 0 0 97950 67 0 0 25 0 1 0 545573827 85733376 20070 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20931 20070 603 41 0 20890 0
vsize: 83724
[startup+990.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 20290 0 0 0 98950 68 0 0 25 0 1 0 545573827 86274048 20198 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21063 20198 603 41 0 21022 0
vsize: 84252
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 20452 0 0 0 99949 68 0 0 25 0 1 0 545573827 86937600 20360 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21225 20360 603 41 0 21184 0
vsize: 84900
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 20595 0 0 0 100949 69 0 0 25 0 1 0 545573827 87470080 20503 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21355 20503 603 41 0 21314 0
vsize: 85420
[startup+1020.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 20738 0 0 0 101949 69 0 0 25 0 1 0 545573827 87998464 20646 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21484 20646 603 41 0 21443 0
vsize: 85936
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 20912 0 0 0 102948 70 0 0 25 0 1 0 545573827 88817664 20820 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21684 20820 603 41 0 21643 0
vsize: 86736
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 21050 0 0 0 103948 70 0 0 25 0 1 0 545573827 89350144 20958 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21814 20958 603 41 0 21773 0
vsize: 87256
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 21194 0 0 0 104948 71 0 0 25 0 1 0 545573827 90017792 21102 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21977 21102 603 41 0 21936 0
vsize: 87908
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 21370 0 0 0 105948 71 0 0 25 0 1 0 545573827 90677248 21278 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22138 21278 603 41 0 22097 0
vsize: 88552
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 21529 0 0 0 106948 71 0 0 25 0 1 0 545573827 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+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 21662 0 0 0 107947 72 0 0 25 0 1 0 545573827 91873280 21570 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22430 21570 603 41 0 22389 0
vsize: 89720
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 21778 0 0 0 108947 73 0 0 25 0 1 0 545573827 92405760 21686 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22560 21686 603 41 0 22519 0
vsize: 90240
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 21909 0 0 0 109947 73 0 0 25 0 1 0 545573827 92807168 21817 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22658 21817 603 41 0 22617 0
vsize: 90632
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 22003 0 0 0 110947 73 0 0 25 0 1 0 545573827 93200384 21911 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22754 21911 603 41 0 22713 0
vsize: 91016
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 22117 0 0 0 111946 74 0 0 25 0 1 0 545573827 93736960 22025 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22885 22025 603 41 0 22844 0
vsize: 91540
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 22245 0 0 0 112946 74 0 0 25 0 1 0 545573827 94273536 22153 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23016 22153 603 41 0 22975 0
vsize: 92064
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 22355 0 0 0 113946 74 0 0 25 0 1 0 545573827 94679040 22263 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23115 22263 603 41 0 23074 0
vsize: 92460
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 22503 0 0 0 114946 75 0 0 25 0 1 0 545573827 95350784 22411 4294967295 134512640 134672761 3221224544 3221223648 134560287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23279 22411 603 41 0 23238 0
vsize: 93116
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 22665 0 0 0 115946 75 0 0 25 0 1 0 545573827 96026624 22573 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23444 22573 603 41 0 23403 0
vsize: 93776
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 22811 0 0 0 116945 76 0 0 25 0 1 0 545573827 96567296 22719 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23576 22719 603 41 0 23535 0
vsize: 94304
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 22889 0 0 0 117945 76 0 0 25 0 1 0 545573827 96829440 22797 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23640 22797 603 41 0 23599 0
vsize: 94560
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 23016 0 0 0 118945 76 0 0 25 0 1 0 545573827 97472512 22924 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23797 22924 603 41 0 23756 0
vsize: 95188
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8226
Raw data (stat): 8169 (minisat+) R 8168 27565 27564 0 -1 0 23174 0 0 0 119945 77 0 0 25 0 1 0 545573827 98152448 23082 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23963 23082 603 41 0 23922 0
vsize: 95852
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 8226
Raw data (stat): 8169 (minisat+) Z 8168 27565 27564 0 -1 12 23176 0 0 0 119945 81 0 0 25 0 1 0 545573827 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.1
CPU time (s): 1200.27
CPU user time (s): 1199.45
CPU system time (s): 0.816875
CPU usage (%): 100.014
Max. virtual memory (Kb): 95852
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####