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-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-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	4742
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.33
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 16443

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-21 07:13:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13491 boxname=wulflinc12 idbench=1038 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9d4ce12b138a2bef65a1f401ec9d1f01  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-l152lav.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-l152lav.opb /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-l152lav.opb
IDLAUNCH: 13491
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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	: 2
cpu MHz		: 451.091
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:        751520 kB
Buffers:         29244 kB
Cached:         232308 kB
SwapCached:        316 kB
Active:          56552 kB
Inactive:       207272 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        751268 kB
SwapTotal:     2097136 kB
SwapFree:      2096236 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5748 kB
Slab:            13680 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 07:33:04 (client local time) WITH STATUS 0 IN 1200.4 SECONDS
stats: 13491 7 1200.4 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.92 0.97 0.91 2/54 22861
Raw data (stat): 22861 (runsolver) R 22860 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 484963430 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 2946 0 0 0 991 7 0 0 25 0 1 0 484963430 14516224 2854 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3544 2854 603 41 0 3503 0
vsize: 14176
[startup+20.001 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 2981 0 0 0 1990 7 0 0 25 0 1 0 484963430 14651392 2889 4294967295 134512640 134672761 3221224544 3221223780 134557472 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3577 2889 603 41 0 3536 0
vsize: 14308
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 2988 0 0 0 2990 7 0 0 25 0 1 0 484963430 14651392 2896 4294967295 134512640 134672761 3221224544 3221223668 134566092 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.002 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 2992 0 0 0 3990 7 0 0 25 0 1 0 484963430 14651392 2900 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.0026 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 3007 0 0 0 4990 7 0 0 25 0 1 0 484963430 14815232 2915 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.0027 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 3011 0 0 0 5990 7 0 0 25 0 1 0 484963430 14815232 2919 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.0035 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 3015 0 0 0 6990 7 0 0 25 0 1 0 484963430 14815232 2923 4294967295 134512640 134672761 3221224544 3221223668 134566057 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.0031 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 3020 0 0 0 7990 7 0 0 25 0 1 0 484963430 14815232 2928 4294967295 134512640 134672761 3221224544 3221223668 134566059 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.0032 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 3024 0 0 0 8990 7 0 0 25 0 1 0 484963430 14815232 2932 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 3036 0 0 0 9990 8 0 0 25 0 1 0 484963430 14815232 2944 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3617 2944 603 41 0 3576 0
vsize: 14468
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 3038 0 0 0 10990 8 0 0 25 0 1 0 484963430 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 3048 0 0 0 11990 8 0 0 25 0 1 0 484963430 14946304 2956 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 3070 0 0 0 12990 8 0 0 25 0 1 0 484963430 14946304 2978 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3649 2978 603 41 0 3608 0
vsize: 14596
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 3129 0 0 0 13990 8 0 0 25 0 1 0 484963430 15212544 3037 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3714 3037 603 41 0 3673 0
vsize: 14856
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 3273 0 0 0 14990 8 0 0 25 0 1 0 484963430 15863808 3181 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3873 3181 603 41 0 3832 0
vsize: 15492
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 3453 0 0 0 15990 9 0 0 25 0 1 0 484963430 16531456 3361 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4036 3361 603 41 0 3995 0
vsize: 16144
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 3721 0 0 0 16989 10 0 0 25 0 1 0 484963430 17608704 3629 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4299 3629 603 41 0 4258 0
vsize: 17196
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 3957 0 0 0 17988 11 0 0 25 0 1 0 484963430 18681856 3865 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4561 3865 603 41 0 4520 0
vsize: 18244
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 4242 0 0 0 18987 12 0 0 25 0 1 0 484963430 19763200 4150 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4825 4150 603 41 0 4784 0
vsize: 19300
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 4567 0 0 0 19986 13 0 0 25 0 1 0 484963430 21237760 4475 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5185 4475 603 41 0 5144 0
vsize: 20740
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 4788 0 0 0 20985 14 0 0 25 0 1 0 484963430 22171648 4696 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5413 4696 603 41 0 5372 0
vsize: 21652
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 5121 0 0 0 21985 15 0 0 25 0 1 0 484963430 23502848 5029 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5738 5029 603 41 0 5697 0
vsize: 22952
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 5566 0 0 0 22983 17 0 0 25 0 1 0 484963430 25235456 5474 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6161 5474 603 41 0 6120 0
vsize: 24644
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 5909 0 0 0 23982 18 0 0 25 0 1 0 484963430 26705920 5817 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6520 5817 603 41 0 6479 0
vsize: 26080
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 6242 0 0 0 24982 19 0 0 25 0 1 0 484963430 28037120 6150 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6845 6150 603 41 0 6804 0
vsize: 27380
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 6542 0 0 0 25981 20 0 0 25 0 1 0 484963430 29233152 6450 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7137 6450 603 41 0 7096 0
vsize: 28548
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 6858 0 0 0 26980 21 0 0 25 0 1 0 484963430 30568448 6766 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7463 6766 603 41 0 7422 0
vsize: 29852
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 7120 0 0 0 27979 21 0 0 25 0 1 0 484963430 31633408 7028 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7723 7028 603 41 0 7682 0
vsize: 30892
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 7374 0 0 0 28979 22 0 0 25 0 1 0 484963430 32702464 7282 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7984 7282 603 41 0 7943 0
vsize: 31936
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 7625 0 0 0 29978 23 0 0 25 0 1 0 484963430 33640448 7533 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8213 7533 603 41 0 8172 0
vsize: 32852
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 7818 0 0 0 30978 24 0 0 25 0 1 0 484963430 34439168 7726 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8408 7726 603 41 0 8367 0
vsize: 33632
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 8068 0 0 0 31977 25 0 0 25 0 1 0 484963430 35508224 7976 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8669 7976 603 41 0 8628 0
vsize: 34676
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 8341 0 0 0 32975 26 0 0 25 0 1 0 484963430 36573184 8249 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8929 8249 603 41 0 8888 0
vsize: 35716
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 8666 0 0 0 33975 27 0 0 25 0 1 0 484963430 37896192 8574 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9252 8574 603 41 0 9211 0
vsize: 37008
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 8961 0 0 0 34974 28 0 0 25 0 1 0 484963430 39350272 8869 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 8869 603 41 0 9566 0
vsize: 38428
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 9168 0 0 0 35974 29 0 0 25 0 1 0 484963430 40284160 9076 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9835 9076 603 41 0 9794 0
vsize: 39340
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 9413 0 0 0 36973 29 0 0 25 0 1 0 484963430 41218048 9321 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10063 9321 603 41 0 10022 0
vsize: 40252
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 9660 0 0 0 37973 30 0 0 25 0 1 0 484963430 42164224 9568 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10294 9568 603 41 0 10253 0
vsize: 41176
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 9806 0 0 0 38973 30 0 0 25 0 1 0 484963430 42835968 9714 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10458 9714 603 41 0 10417 0
vsize: 41832
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 10033 0 0 0 39972 31 0 0 25 0 1 0 484963430 43778048 9941 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10688 9941 603 41 0 10647 0
vsize: 42752
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 10243 0 0 0 40972 31 0 0 25 0 1 0 484963430 44580864 10151 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10884 10151 603 41 0 10843 0
vsize: 43536
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 10403 0 0 0 41972 32 0 0 25 0 1 0 484963430 45252608 10311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11048 10311 603 41 0 11007 0
vsize: 44192
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 10574 0 0 0 42972 32 0 0 25 0 1 0 484963430 45916160 10482 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11210 10482 603 41 0 11169 0
vsize: 44840
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 10741 0 0 0 43971 33 0 0 25 0 1 0 484963430 46575616 10649 4294967295 134512640 134672761 3221224544 3221223696 134565153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11371 10649 603 41 0 11330 0
vsize: 45484
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 10941 0 0 0 44970 33 0 0 25 0 1 0 484963430 47501312 10849 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11597 10849 603 41 0 11556 0
vsize: 46388
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 11110 0 0 0 45969 34 0 0 25 0 1 0 484963430 48156672 11018 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11757 11018 603 41 0 11716 0
vsize: 47028
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 11327 0 0 0 46969 35 0 0 25 0 1 0 484963430 49086464 11235 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11984 11235 603 41 0 11943 0
vsize: 47936
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 11533 0 0 0 47968 36 0 0 25 0 1 0 484963430 49889280 11441 4294967295 134512640 134672761 3221224544 3221223712 134561018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12180 11441 603 41 0 12139 0
vsize: 48720
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 11752 0 0 0 48968 36 0 0 25 0 1 0 484963430 50819072 11660 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12407 11660 603 41 0 12366 0
vsize: 49628
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 11975 0 0 0 49967 37 0 0 25 0 1 0 484963430 51621888 11883 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12603 11883 603 41 0 12562 0
vsize: 50412
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 12152 0 0 0 50967 37 0 0 25 0 1 0 484963430 52416512 12060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12797 12060 603 41 0 12756 0
vsize: 51188
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 12349 0 0 0 51967 38 0 0 25 0 1 0 484963430 53211136 12257 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12991 12257 603 41 0 12950 0
vsize: 51964
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 12510 0 0 0 52966 38 0 0 25 0 1 0 484963430 53878784 12418 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13154 12418 603 41 0 13113 0
vsize: 52616
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 12676 0 0 0 53966 39 0 0 25 0 1 0 484963430 54546432 12584 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13317 12584 603 41 0 13276 0
vsize: 53268
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 12864 0 0 0 54965 40 0 0 25 0 1 0 484963430 55357440 12772 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13515 12772 603 41 0 13474 0
vsize: 54060
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 13019 0 0 0 55965 41 0 0 25 0 1 0 484963430 55889920 12927 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13645 12927 603 41 0 13604 0
vsize: 54580
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 13177 0 0 0 56965 41 0 0 25 0 1 0 484963430 56553472 13085 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13807 13085 603 41 0 13766 0
vsize: 55228
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 13359 0 0 0 57965 41 0 0 25 0 1 0 484963430 57348096 13267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14001 13267 603 41 0 13960 0
vsize: 56004
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 13495 0 0 0 58965 41 0 0 25 0 1 0 484963430 57884672 13403 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14132 13403 603 41 0 14091 0
vsize: 56528
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 13683 0 0 0 59965 41 0 0 25 0 1 0 484963430 58679296 13591 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14326 13591 603 41 0 14285 0
vsize: 57304
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 13860 0 0 0 60965 42 0 0 25 0 1 0 484963430 59346944 13768 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14489 13768 603 41 0 14448 0
vsize: 57956
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 14030 0 0 0 61964 42 0 0 25 0 1 0 484963430 60014592 13938 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14652 13938 603 41 0 14611 0
vsize: 58608
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 14211 0 0 0 62964 43 0 0 25 0 1 0 484963430 60809216 14119 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14846 14119 603 41 0 14805 0
vsize: 59384
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 14377 0 0 0 63963 44 0 0 25 0 1 0 484963430 61476864 14285 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15009 14285 603 41 0 14968 0
vsize: 60036
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 14513 0 0 0 64963 44 0 0 25 0 1 0 484963430 62005248 14421 4294967295 134512640 134672761 3221224544 3221223616 134553544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14421 603 41 0 15097 0
vsize: 60552
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 14698 0 0 0 65963 45 0 0 25 0 1 0 484963430 62824448 14606 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15338 14606 603 41 0 15297 0
vsize: 61352
[startup+670.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 14869 0 0 0 66962 45 0 0 25 0 1 0 484963430 63492096 14777 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15501 14777 603 41 0 15460 0
vsize: 62004
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 15058 0 0 0 67962 46 0 0 25 0 1 0 484963430 64294912 14966 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15697 14966 603 41 0 15656 0
vsize: 62788
[startup+690.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 15222 0 0 0 68964 47 0 0 25 0 1 0 484963430 64962560 15130 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15860 15130 603 41 0 15819 0
vsize: 63440
[startup+700.163 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 15380 0 0 0 69975 47 0 0 25 0 1 0 484963430 65630208 15288 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16023 15288 603 41 0 15982 0
vsize: 64092
[startup+710.163 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 15602 0 0 0 70975 48 0 0 25 0 1 0 484963430 66555904 15510 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16249 15510 603 41 0 16208 0
vsize: 64996
[startup+720.164 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 15815 0 0 0 71974 48 0 0 25 0 1 0 484963430 67362816 15723 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16446 15723 603 41 0 16405 0
vsize: 65784
[startup+730.163 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 16006 0 0 0 72974 49 0 0 25 0 1 0 484963430 68157440 15914 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16640 15914 603 41 0 16599 0
vsize: 66560
[startup+740.164 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 16212 0 0 0 73974 49 0 0 25 0 1 0 484963430 68956160 16120 4294967295 134512640 134672761 3221224544 3221223600 134565140 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16835 16120 603 41 0 16794 0
vsize: 67340
[startup+750.164 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 16405 0 0 0 74972 51 0 0 25 0 1 0 484963430 69758976 16313 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17031 16313 603 41 0 16990 0
vsize: 68124
[startup+760.165 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 16601 0 0 0 75972 52 0 0 25 0 1 0 484963430 70557696 16509 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17226 16509 603 41 0 17185 0
vsize: 68904
[startup+770.165 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 16741 0 0 0 76972 52 0 0 25 0 1 0 484963430 71094272 16649 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17357 16649 603 41 0 17316 0
vsize: 69428
[startup+780.166 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 16944 0 0 0 77971 53 0 0 25 0 1 0 484963430 71892992 16852 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17552 16852 603 41 0 17511 0
vsize: 70208
[startup+790.166 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 17058 0 0 0 78971 53 0 0 25 0 1 0 484963430 72429568 16966 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17683 16966 603 41 0 17642 0
vsize: 70732
[startup+800.166 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 17232 0 0 0 79970 54 0 0 25 0 1 0 484963430 73089024 17140 4294967295 134512640 134672761 3221224544 3221223696 134565213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17844 17140 603 41 0 17803 0
vsize: 71376
[startup+810.166 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 17443 0 0 0 80970 54 0 0 25 0 1 0 484963430 74014720 17351 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18070 17351 603 41 0 18029 0
vsize: 72280
[startup+820.167 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 17592 0 0 0 81970 55 0 0 25 0 1 0 484963430 74555392 17500 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18202 17500 603 41 0 18161 0
vsize: 72808
[startup+830.167 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 17775 0 0 0 82969 56 0 0 25 0 1 0 484963430 75874304 17683 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18524 17683 603 41 0 18483 0
vsize: 74096
[startup+840.167 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 17975 0 0 0 83969 56 0 0 25 0 1 0 484963430 76664832 17883 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18717 17883 603 41 0 18676 0
vsize: 74868
[startup+850.168 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 18089 0 0 0 84968 56 0 0 25 0 1 0 484963430 77193216 17997 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18846 17997 603 41 0 18805 0
vsize: 75384
[startup+860.168 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 18222 0 0 0 85968 57 0 0 25 0 1 0 484963430 77725696 18130 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18976 18130 603 41 0 18935 0
vsize: 75904
[startup+870.168 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 18369 0 0 0 86967 58 0 0 25 0 1 0 484963430 78249984 18277 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19104 18277 603 41 0 19063 0
vsize: 76416
[startup+880.168 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 18501 0 0 0 87967 58 0 0 25 0 1 0 484963430 78790656 18409 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19236 18409 603 41 0 19195 0
vsize: 76944
[startup+890.169 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 18763 0 0 0 88967 59 0 0 25 0 1 0 484963430 79888384 18671 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19504 18671 603 41 0 19463 0
vsize: 78016
[startup+900.174 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 18912 0 0 0 89967 59 0 0 25 0 1 0 484963430 80556032 18820 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19667 18820 603 41 0 19626 0
vsize: 78668
[startup+910.177 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 19080 0 0 0 90967 60 0 0 25 0 1 0 484963430 81215488 18988 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19828 18988 603 41 0 19787 0
vsize: 79312
[startup+920.182 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 19330 0 0 0 91967 61 0 0 25 0 1 0 484963430 82288640 19238 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20090 19238 603 41 0 20049 0
vsize: 80360
[startup+930.198 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 19503 0 0 0 92968 61 0 0 25 0 1 0 484963430 82964480 19411 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20255 19411 603 41 0 20214 0
vsize: 81020
[startup+940.198 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 19623 0 0 0 93968 62 0 0 25 0 1 0 484963430 83501056 19531 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20386 19531 603 41 0 20345 0
vsize: 81544
[startup+950.199 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 19729 0 0 0 94968 62 0 0 25 0 1 0 484963430 83906560 19637 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20485 19637 603 41 0 20444 0
vsize: 81940
[startup+960.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 19823 0 0 0 95968 62 0 0 25 0 1 0 484963430 84357120 19731 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20595 19731 603 41 0 20554 0
vsize: 82380
[startup+970.199 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 19943 0 0 0 96968 62 0 0 25 0 1 0 484963430 84758528 19851 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20693 19851 603 41 0 20652 0
vsize: 82772
[startup+980.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 20072 0 0 0 97968 63 0 0 25 0 1 0 484963430 85323776 19980 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20831 19980 603 41 0 20790 0
vsize: 83324
[startup+990.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 20167 0 0 0 98967 63 0 0 25 0 1 0 484963430 85733376 20075 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20931 20075 603 41 0 20890 0
vsize: 83724
[startup+1000.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 20297 0 0 0 99967 63 0 0 25 0 1 0 484963430 86274048 20205 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21063 20205 603 41 0 21022 0
vsize: 84252
[startup+1010.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 20452 0 0 0 100967 63 0 0 25 0 1 0 484963430 86937600 20360 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21225 20360 603 41 0 21184 0
vsize: 84900
[startup+1020.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 20594 0 0 0 101967 64 0 0 25 0 1 0 484963430 87470080 20502 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21355 20502 603 41 0 21314 0
vsize: 85420
[startup+1030.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 20735 0 0 0 102967 64 0 0 25 0 1 0 484963430 87998464 20643 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21484 20643 603 41 0 21443 0
vsize: 85936
[startup+1040.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 20905 0 0 0 103967 64 0 0 25 0 1 0 484963430 88817664 20813 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21684 20813 603 41 0 21643 0
vsize: 86736
[startup+1050.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 21043 0 0 0 104967 65 0 0 25 0 1 0 484963430 89350144 20951 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21814 20951 603 41 0 21773 0
vsize: 87256
[startup+1060.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 21178 0 0 0 105966 65 0 0 25 0 1 0 484963430 89886720 21086 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21945 21086 603 41 0 21904 0
vsize: 87780
[startup+1070.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 21351 0 0 0 106966 66 0 0 25 0 1 0 484963430 90677248 21259 4294967295 134512640 134672761 3221224544 3221223648 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22138 21259 603 41 0 22097 0
vsize: 88552
[startup+1080.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 21511 0 0 0 107966 67 0 0 25 0 1 0 484963430 91336704 21419 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22299 21419 603 41 0 22258 0
vsize: 89196
[startup+1090.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 21649 0 0 0 108965 67 0 0 25 0 1 0 484963430 91873280 21557 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22430 21557 603 41 0 22389 0
vsize: 89720
[startup+1100.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 21757 0 0 0 109965 67 0 0 25 0 1 0 484963430 92274688 21665 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22528 21665 603 41 0 22487 0
vsize: 90112
[startup+1110.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 21891 0 0 0 110965 68 0 0 25 0 1 0 484963430 92807168 21799 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22658 21799 603 41 0 22617 0
vsize: 90632
[startup+1120.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 21988 0 0 0 111965 68 0 0 25 0 1 0 484963430 93200384 21896 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22754 21896 603 41 0 22713 0
vsize: 91016
[startup+1130.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 22095 0 0 0 112965 68 0 0 25 0 1 0 484963430 93601792 22003 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22852 22003 603 41 0 22811 0
vsize: 91408
[startup+1140.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 22220 0 0 0 113964 69 0 0 25 0 1 0 484963430 94138368 22128 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22983 22128 603 41 0 22942 0
vsize: 91932
[startup+1150.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 22333 0 0 0 114964 69 0 0 25 0 1 0 484963430 94679040 22241 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23115 22241 603 41 0 23074 0
vsize: 92460
[startup+1160.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 22462 0 0 0 115964 70 0 0 25 0 1 0 484963430 95084544 22370 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23214 22370 603 41 0 23173 0
vsize: 92856
[startup+1170.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 22618 0 0 0 116964 70 0 0 25 0 1 0 484963430 95756288 22526 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23378 22526 603 41 0 23337 0
vsize: 93512
[startup+1180.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 22747 0 0 0 117963 71 0 0 25 0 1 0 484963430 96296960 22655 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23510 22655 603 41 0 23469 0
vsize: 94040
[startup+1190.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 22876 0 0 0 118963 71 0 0 25 0 1 0 484963430 96829440 22784 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23640 22784 603 41 0 23599 0
vsize: 94560
[startup+1200.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22861
Raw data (stat): 22861 (minisat+) R 22860 25285 25284 0 -1 0 22989 0 0 0 119963 71 0 0 25 0 1 0 484963430 97341440 22897 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23765 22897 603 41 0 23724 0
vsize: 95060
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.25 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 22861
Raw data (stat): 22861 (minisat+) Z 22860 25285 25284 0 -1 12 22991 0 0 0 119964 75 0 0 25 0 1 0 484963430 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.25
CPU time (s): 1200.4
CPU user time (s): 1199.64
CPU system time (s): 0.757884
CPU usage (%): 100.012
Max. virtual memory (Kb): 95060
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####