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/miplib/normalized-mps-v2-20-10-l152lav.opb
MD5SUM	00855a9538cee8df79108d56ee6867b4
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5046
Optimality of the best value was proved	NO
Number of terms in the objective function	1989
Biggest coefficient in the objective function	268
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	382524
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	268
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	382524
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.28
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 17049

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        692304 kB
Buffers:         21200 kB
Cached:         298736 kB
SwapCached:          4 kB
Active:          72912 kB
Inactive:       249864 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        692052 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6940 kB
Slab:            13880 kB
Committed_AS:    63560 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 09:49:21 (client local time) WITH STATUS 0 IN 1200.2 SECONDS
stats: 11905 7 1200.2 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.79 0.92 0.90 2/54 3633
Raw data (stat): 3633 (runsolver) R 3632 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485789756 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0004 s]
Raw data (loadavg): 0.82 0.93 0.90 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 2946 0 0 0 991 7 0 0 25 0 1 0 485789756 14516224 2854 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.0008 s]
Raw data (loadavg): 0.85 0.93 0.90 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 2981 0 0 0 1991 7 0 0 25 0 1 0 485789756 14651392 2889 4294967295 134512640 134672761 3221224544 3221223712 134560940 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.0008 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 2988 0 0 0 2991 7 0 0 25 0 1 0 485789756 14651392 2896 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.0015 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 2993 0 0 0 3991 8 0 0 25 0 1 0 485789756 14651392 2901 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3577 2901 603 41 0 3536 0
vsize: 14308
[startup+50.0017 s]
Raw data (loadavg): 0.91 0.93 0.90 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 3007 0 0 0 4990 8 0 0 25 0 1 0 485789756 14815232 2915 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.92 0.93 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 3011 0 0 0 5990 9 0 0 25 0 1 0 485789756 14815232 2919 4294967295 134512640 134672761 3221224544 3221223716 134556646 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.0033 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 3015 0 0 0 6990 9 0 0 25 0 1 0 485789756 14815232 2923 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.0036 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 3021 0 0 0 7989 9 0 0 25 0 1 0 485789756 14815232 2929 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3617 2929 603 41 0 3576 0
vsize: 14468
[startup+90.0036 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 3025 0 0 0 8989 9 0 0 25 0 1 0 485789756 14815232 2933 4294967295 134512640 134672761 3221224544 3221223724 134556674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3617 2933 603 41 0 3576 0
vsize: 14468
[startup+100.003 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 3036 0 0 0 9989 10 0 0 25 0 1 0 485789756 14815232 2944 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.003 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 3039 0 0 0 10989 10 0 0 25 0 1 0 485789756 14946304 2947 4294967295 134512640 134672761 3221224544 3221223696 134565083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3649 2947 603 41 0 3608 0
vsize: 14596
[startup+120.004 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 3050 0 0 0 11989 10 0 0 25 0 1 0 485789756 14946304 2958 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3649 2958 603 41 0 3608 0
vsize: 14596
[startup+130.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 3073 0 0 0 12988 11 0 0 25 0 1 0 485789756 14946304 2981 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3649 2981 603 41 0 3608 0
vsize: 14596
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 3155 0 0 0 13988 11 0 0 25 0 1 0 485789756 15462400 3063 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3775 3063 603 41 0 3734 0
vsize: 15100
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 3301 0 0 0 14988 12 0 0 25 0 1 0 485789756 15994880 3209 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3905 3209 603 41 0 3864 0
vsize: 15620
[startup+160.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 3521 0 0 0 15987 13 0 0 25 0 1 0 485789756 16801792 3429 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3429 603 41 0 4061 0
vsize: 16408
[startup+170.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 3757 0 0 0 16986 14 0 0 25 0 1 0 485789756 17874944 3665 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4364 3665 603 41 0 4323 0
vsize: 17456
[startup+180.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 4027 0 0 0 17985 15 0 0 25 0 1 0 485789756 18952192 3935 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4627 3935 603 41 0 4586 0
vsize: 18508
[startup+190.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 4321 0 0 0 18984 17 0 0 25 0 1 0 485789756 20295680 4229 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4955 4229 603 41 0 4914 0
vsize: 19820
[startup+200.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 4636 0 0 0 19983 18 0 0 25 0 1 0 485789756 21504000 4544 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5250 4544 603 41 0 5209 0
vsize: 21000
[startup+210.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 4856 0 0 0 20982 19 0 0 25 0 1 0 485789756 22433792 4764 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5477 4764 603 41 0 5436 0
vsize: 21908
[startup+220.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 5260 0 0 0 21981 20 0 0 25 0 1 0 485789756 24031232 5168 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5867 5168 603 41 0 5826 0
vsize: 23468
[startup+230.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 5690 0 0 0 22980 21 0 0 25 0 1 0 485789756 25772032 5598 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6292 5598 603 41 0 6251 0
vsize: 25168
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 5976 0 0 0 23979 22 0 0 25 0 1 0 485789756 26972160 5884 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6585 5884 603 41 0 6544 0
vsize: 26340
[startup+250.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 6330 0 0 0 24977 24 0 0 25 0 1 0 485789756 28434432 6238 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6942 6238 603 41 0 6901 0
vsize: 27768
[startup+260.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 6647 0 0 0 25976 25 0 0 25 0 1 0 485789756 29638656 6555 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7236 6555 603 41 0 7195 0
vsize: 28944
[startup+270.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 6962 0 0 0 26975 26 0 0 25 0 1 0 485789756 30965760 6870 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7560 6870 603 41 0 7519 0
vsize: 30240
[startup+280.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 7192 0 0 0 27974 27 0 0 25 0 1 0 485789756 31899648 7100 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7788 7100 603 41 0 7747 0
vsize: 31152
[startup+290.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 7471 0 0 0 28973 28 0 0 25 0 1 0 485789756 33107968 7379 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8083 7379 603 41 0 8042 0
vsize: 32332
[startup+300.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 7691 0 0 0 29973 29 0 0 25 0 1 0 485789756 33906688 7599 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8278 7599 603 41 0 8237 0
vsize: 33112
[startup+310.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 7932 0 0 0 30972 30 0 0 25 0 1 0 485789756 34975744 7840 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8539 7840 603 41 0 8498 0
vsize: 34156
[startup+320.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 8135 0 0 0 31971 31 0 0 25 0 1 0 485789756 35774464 8043 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8734 8043 603 41 0 8693 0
vsize: 34936
[startup+330.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 8453 0 0 0 32970 32 0 0 25 0 1 0 485789756 37101568 8361 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9058 8361 603 41 0 9017 0
vsize: 36232
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 8790 0 0 0 33969 34 0 0 25 0 1 0 485789756 38686720 8698 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9445 8698 603 41 0 9404 0
vsize: 37780
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 9047 0 0 0 34967 35 0 0 25 0 1 0 485789756 39747584 8955 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9704 8955 603 41 0 9663 0
vsize: 38816
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 9276 0 0 0 35967 36 0 0 25 0 1 0 485789756 40681472 9184 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9932 9184 603 41 0 9891 0
vsize: 39728
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 9525 0 0 0 36966 37 0 0 25 0 1 0 485789756 41615360 9433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10160 9433 603 41 0 10119 0
vsize: 40640
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 9739 0 0 0 37965 38 0 0 25 0 1 0 485789756 42569728 9647 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10393 9647 603 41 0 10352 0
vsize: 41572
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 9927 0 0 0 38965 38 0 0 25 0 1 0 485789756 43372544 9835 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10589 9835 603 41 0 10548 0
vsize: 42356
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 10139 0 0 0 39964 39 0 0 25 0 1 0 485789756 44175360 10047 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10785 10047 603 41 0 10744 0
vsize: 43140
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 10333 0 0 0 40963 40 0 0 25 0 1 0 485789756 44982272 10241 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10982 10241 603 41 0 10941 0
vsize: 43928
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 10482 0 0 0 41963 41 0 0 25 0 1 0 485789756 45518848 10390 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11113 10390 603 41 0 11072 0
vsize: 44452
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 10655 0 0 0 42962 42 0 0 25 0 1 0 485789756 46309376 10563 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11306 10563 603 41 0 11265 0
vsize: 45224
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 10861 0 0 0 43962 42 0 0 25 0 1 0 485789756 47108096 10769 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11501 10769 603 41 0 11460 0
vsize: 46004
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 11045 0 0 0 44961 43 0 0 25 0 1 0 485789756 47894528 10953 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11693 10953 603 41 0 11652 0
vsize: 46772
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 11225 0 0 0 45959 45 0 0 25 0 1 0 485789756 48553984 11133 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11854 11133 603 41 0 11813 0
vsize: 47416
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 11479 0 0 0 46958 46 0 0 25 0 1 0 485789756 49618944 11387 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12114 11387 603 41 0 12073 0
vsize: 48456
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 11663 0 0 0 47958 47 0 0 25 0 1 0 485789756 50421760 11571 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12310 11571 603 41 0 12269 0
vsize: 49240
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 11881 0 0 0 48957 48 0 0 25 0 1 0 485789756 51351552 11789 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12537 11789 603 41 0 12496 0
vsize: 50148
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 12089 0 0 0 49957 48 0 0 25 0 1 0 485789756 52154368 11997 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12733 11997 603 41 0 12692 0
vsize: 50932
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 12272 0 0 0 50956 49 0 0 25 0 1 0 485789756 52813824 12180 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12894 12180 603 41 0 12853 0
vsize: 51576
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 12463 0 0 0 51955 50 0 0 25 0 1 0 485789756 53612544 12371 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13089 12371 603 41 0 13048 0
vsize: 52356
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 12620 0 0 0 52955 51 0 0 25 0 1 0 485789756 54280192 12528 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13252 12528 603 41 0 13211 0
vsize: 53008
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 12771 0 0 0 53954 51 0 0 25 0 1 0 485789756 54947840 12679 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13415 12679 603 41 0 13374 0
vsize: 53660
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 12994 0 0 0 54954 52 0 0 25 0 1 0 485789756 55754752 12902 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13612 12902 603 41 0 13571 0
vsize: 54448
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 13148 0 0 0 55953 53 0 0 25 0 1 0 485789756 56422400 13056 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13775 13056 603 41 0 13734 0
vsize: 55100
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 13306 0 0 0 56952 54 0 0 25 0 1 0 485789756 57085952 13214 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13937 13214 603 41 0 13896 0
vsize: 55748
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 13455 0 0 0 57952 55 0 0 25 0 1 0 485789756 57753600 13363 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14100 13363 603 41 0 14059 0
vsize: 56400
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 13629 0 0 0 58951 55 0 0 25 0 1 0 485789756 58417152 13537 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14262 13537 603 41 0 14221 0
vsize: 57048
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 13827 0 0 0 59951 56 0 0 25 0 1 0 485789756 59211776 13735 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14456 13735 603 41 0 14415 0
vsize: 57824
[startup+610.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 13987 0 0 0 60950 57 0 0 25 0 1 0 485789756 59883520 13895 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14620 13895 603 41 0 14579 0
vsize: 58480
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 14166 0 0 0 61950 57 0 0 25 0 1 0 485789756 60674048 14074 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14813 14074 603 41 0 14772 0
vsize: 59252
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 14341 0 0 0 62949 58 0 0 25 0 1 0 485789756 61341696 14249 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14976 14249 603 41 0 14935 0
vsize: 59904
[startup+640.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 14475 0 0 0 63948 59 0 0 25 0 1 0 485789756 61874176 14383 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15106 14383 603 41 0 15065 0
vsize: 60424
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 14677 0 0 0 64948 59 0 0 25 0 1 0 485789756 62685184 14585 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15304 14585 603 41 0 15263 0
vsize: 61216
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 14833 0 0 0 65948 60 0 0 25 0 1 0 485789756 63361024 14741 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15469 14741 603 41 0 15428 0
vsize: 61876
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 15024 0 0 0 66947 61 0 0 25 0 1 0 485789756 64163840 14932 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15665 14932 603 41 0 15624 0
vsize: 62660
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 15188 0 0 0 67947 61 0 0 25 0 1 0 485789756 64827392 15096 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15827 15096 603 41 0 15786 0
vsize: 63308
[startup+690.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 15359 0 0 0 68946 62 0 0 25 0 1 0 485789756 65499136 15267 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15991 15267 603 41 0 15950 0
vsize: 63964
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 15572 0 0 0 69946 63 0 0 25 0 1 0 485789756 66424832 15480 4294967295 134512640 134672761 3221224544 3221223744 134557806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16217 15480 603 41 0 16176 0
vsize: 64868
[startup+710.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 15789 0 0 0 70945 63 0 0 25 0 1 0 485789756 67227648 15697 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16413 15697 603 41 0 16372 0
vsize: 65652
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 15982 0 0 0 71945 64 0 0 25 0 1 0 485789756 68026368 15890 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16608 15890 603 41 0 16567 0
vsize: 66432
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 16193 0 0 0 72944 65 0 0 25 0 1 0 485789756 68956160 16101 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16835 16101 603 41 0 16794 0
vsize: 67340
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 16382 0 0 0 73944 65 0 0 25 0 1 0 485789756 69623808 16290 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16998 16290 603 41 0 16957 0
vsize: 67992
[startup+750.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 16582 0 0 0 74943 66 0 0 25 0 1 0 485789756 70426624 16490 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17194 16490 603 41 0 17153 0
vsize: 68776
[startup+760.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 16734 0 0 0 75943 66 0 0 25 0 1 0 485789756 71094272 16642 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17357 16642 603 41 0 17316 0
vsize: 69428
[startup+770.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 16934 0 0 0 76941 68 0 0 25 0 1 0 485789756 71892992 16842 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17552 16842 603 41 0 17511 0
vsize: 70208
[startup+780.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 17051 0 0 0 77941 68 0 0 25 0 1 0 485789756 72429568 16959 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17683 16959 603 41 0 17642 0
vsize: 70732
[startup+790.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 17232 0 0 0 78940 70 0 0 25 0 1 0 485789756 73089024 17140 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17844 17140 603 41 0 17803 0
vsize: 71376
[startup+800.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 17441 0 0 0 79939 71 0 0 25 0 1 0 485789756 74014720 17349 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18070 17349 603 41 0 18029 0
vsize: 72280
[startup+810.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 17594 0 0 0 80939 71 0 0 25 0 1 0 485789756 74555392 17502 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18202 17502 603 41 0 18161 0
vsize: 72808
[startup+820.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 17778 0 0 0 81938 72 0 0 25 0 1 0 485789756 75874304 17686 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18524 17686 603 41 0 18483 0
vsize: 74096
[startup+830.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 17979 0 0 0 82937 73 0 0 25 0 1 0 485789756 76664832 17887 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18717 17887 603 41 0 18676 0
vsize: 74868
[startup+840.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 18096 0 0 0 83937 73 0 0 25 0 1 0 485789756 77193216 18004 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18846 18004 603 41 0 18805 0
vsize: 75384
[startup+850.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 18229 0 0 0 84936 74 0 0 25 0 1 0 485789756 77725696 18137 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18976 18137 603 41 0 18935 0
vsize: 75904
[startup+860.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 18376 0 0 0 85936 75 0 0 25 0 1 0 485789756 78385152 18284 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19137 18284 603 41 0 19096 0
vsize: 76548
[startup+870.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 18515 0 0 0 86935 76 0 0 25 0 1 0 485789756 78921728 18423 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19268 18423 603 41 0 19227 0
vsize: 77072
[startup+880.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 18789 0 0 0 87934 77 0 0 25 0 1 0 485789756 80023552 18697 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19537 18697 603 41 0 19496 0
vsize: 78148
[startup+890.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 18948 0 0 0 88933 77 0 0 25 0 1 0 485789756 80687104 18856 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19699 18856 603 41 0 19658 0
vsize: 78796
[startup+900.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 19109 0 0 0 89932 78 0 0 25 0 1 0 485789756 81350656 19017 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19861 19017 603 41 0 19820 0
vsize: 79444
[startup+910.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 19365 0 0 0 90931 80 0 0 25 0 1 0 485789756 82423808 19273 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20123 19273 603 41 0 20082 0
vsize: 80492
[startup+920.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 19527 0 0 0 91931 80 0 0 25 0 1 0 485789756 82964480 19435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20255 19435 603 41 0 20214 0
vsize: 81020
[startup+930.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 19639 0 0 0 92931 81 0 0 25 0 1 0 485789756 83501056 19547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20386 19547 603 41 0 20345 0
vsize: 81544
[startup+940.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 19748 0 0 0 93930 81 0 0 25 0 1 0 485789756 83906560 19656 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20485 19656 603 41 0 20444 0
vsize: 81940
[startup+950.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 19843 0 0 0 94930 82 0 0 25 0 1 0 485789756 84357120 19751 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20595 19751 603 41 0 20554 0
vsize: 82380
[startup+960.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 19976 0 0 0 95929 82 0 0 25 0 1 0 485789756 84918272 19884 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20732 19884 603 41 0 20691 0
vsize: 82928
[startup+970.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 20097 0 0 0 96928 83 0 0 25 0 1 0 485789756 85458944 20005 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20864 20005 603 41 0 20823 0
vsize: 83456
[startup+980.027 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 20194 0 0 0 97928 84 0 0 25 0 1 0 485789756 85868544 20102 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20964 20102 603 41 0 20923 0
vsize: 83856
[startup+990.029 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 20349 0 0 0 98927 84 0 0 25 0 1 0 485789756 86405120 20257 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21095 20257 603 41 0 21054 0
vsize: 84380
[startup+1000.03 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 20489 0 0 0 99927 85 0 0 25 0 1 0 485789756 87072768 20397 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21258 20397 603 41 0 21217 0
vsize: 85032
[startup+1010.03 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 20638 0 0 0 100926 86 0 0 25 0 1 0 485789756 87605248 20546 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21388 20546 603 41 0 21347 0
vsize: 85552
[startup+1020.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 20806 0 0 0 101926 86 0 0 25 0 1 0 485789756 88420352 20714 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21587 20714 603 41 0 21546 0
vsize: 86348
[startup+1030.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 20944 0 0 0 102926 87 0 0 25 0 1 0 485789756 88952832 20852 4294967295 134512640 134672761 3221224544 3221223728 134559176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21717 20852 603 41 0 21676 0
vsize: 86868
[startup+1040.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 21096 0 0 0 103925 88 0 0 25 0 1 0 485789756 89616384 21004 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21879 21004 603 41 0 21838 0
vsize: 87516
[startup+1050.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 21247 0 0 0 104925 88 0 0 25 0 1 0 485789756 90152960 21155 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22010 21155 603 41 0 21969 0
vsize: 88040
[startup+1060.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 21420 0 0 0 105924 89 0 0 25 0 1 0 485789756 90939392 21328 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22202 21328 603 41 0 22161 0
vsize: 88808
[startup+1070.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 21566 0 0 0 106923 90 0 0 25 0 1 0 485789756 91471872 21474 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22332 21474 603 41 0 22291 0
vsize: 89328
[startup+1080.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 21698 0 0 0 107922 90 0 0 25 0 1 0 485789756 92004352 21606 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22462 21606 603 41 0 22421 0
vsize: 89848
[startup+1090.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 21815 0 0 0 108922 91 0 0 25 0 1 0 485789756 92536832 21723 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22592 21723 603 41 0 22551 0
vsize: 90368
[startup+1100.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 21933 0 0 0 109921 92 0 0 25 0 1 0 485789756 92938240 21841 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22690 21841 603 41 0 22649 0
vsize: 90760
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 22026 0 0 0 110922 92 0 0 25 0 1 0 485789756 93335552 21934 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22787 21934 603 41 0 22746 0
vsize: 91148
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 22156 0 0 0 111921 92 0 0 25 0 1 0 485789756 93872128 22064 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22918 22064 603 41 0 22877 0
vsize: 91672
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 22260 0 0 0 112921 93 0 0 25 0 1 0 485789756 94273536 22168 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23016 22168 603 41 0 22975 0
vsize: 92064
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 22387 0 0 0 113921 93 0 0 25 0 1 0 485789756 94814208 22295 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23148 22295 603 41 0 23107 0
vsize: 92592
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 22529 0 0 0 114921 93 0 0 25 0 1 0 485789756 95350784 22437 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23279 22437 603 41 0 23238 0
vsize: 93116
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 22695 0 0 0 115920 94 0 0 25 0 1 0 485789756 96161792 22603 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23477 22603 603 41 0 23436 0
vsize: 93908
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 22851 0 0 0 116920 94 0 0 25 0 1 0 485789756 96698368 22759 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23608 22759 603 41 0 23567 0
vsize: 94432
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 22920 0 0 0 117920 95 0 0 25 0 1 0 485789756 96976896 22828 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23676 22828 603 41 0 23635 0
vsize: 94704
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 23031 0 0 0 118920 95 0 0 25 0 1 0 485789756 97619968 22939 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23833 22939 603 41 0 23792 0
vsize: 95332
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3633
Raw data (stat): 3633 (minisat+) R 3632 22932 22931 0 -1 0 23193 0 0 0 119920 95 0 0 25 0 1 0 485789756 98152448 23101 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23963 23101 603 41 0 23922 0
vsize: 95852
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 3633
Raw data (stat): 3633 (minisat+) Z 3632 22932 22931 0 -1 12 23195 0 0 0 119920 100 0 0 25 0 1 0 485789756 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.08
CPU time (s): 1200.2
CPU user time (s): 1199.2
CPU system time (s): 1.00085
CPU usage (%): 100.011
Max. virtual memory (Kb): 95852
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####