PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/manquinho/logic-synthesis/normalized-f51m.b.opb
MD5SUM	4fc22abde8250807abd95442a25fac44
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	18
Optimality of the best value was proved	NO
Number of terms in the objective function	407
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	407
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	407
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02684
Number of variables	406
Total number of constraints	538
Number of constraints which are clauses	520
Number of constraints which are cardinality constraints (but not clauses)	18
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	123
Trace number 6179

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-14 03:41:05 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4581 boxname=wulflinc2 idbench=69 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4fc22abde8250807abd95442a25fac44  /oldhome/oroussel/tmp/wulflinc2/normalized-f51m.b.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc2/normalized-f51m.b.opb /oldhome/oroussel/tmp/wulflinc2/normalized-f51m.b.opb
IDLAUNCH: 4581
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        893696 kB
Buffers:         35516 kB
Cached:          84840 kB
SwapCached:          4 kB
Active:          58136 kB
Inactive:        65088 kB
HighTotal:      131008 kB
HighFree:        42364 kB
LowTotal:       903652 kB
LowFree:        851332 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            12132 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:01:07 (client local time) WITH STATUS 10 IN 1200.16 SECONDS
stats: 4581 7 1200.16 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 498 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     498    13351 |     166       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:14920     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |   32445    88186 |   10815       1       18    18.0 |  0.000 % |
c |       101 |   32445    88186 |   11896     101      634     6.3 |  0.055 % |
c |       251 |   32430    88150 |   13086     250     3216    12.9 |  0.083 % |
c |       476 |   32419    88126 |   14394     474     4850    10.2 |  0.110 % |
c |       816 |   32419    88126 |   15834     814    16091    19.8 |  0.110 % |
c ==============================================================================
c [1mFound solution: 25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1205 |   32375    88025 |   10791    1202    21345    17.8 |  0.110 % |
c |      1307 |   32375    88025 |   11870    1304    22745    17.4 |  0.266 % |
c |      1458 |   32302    87862 |   13057    1369    23099    16.9 |  0.449 % |
c |      1683 |   32302    87862 |   14362    1594    31156    19.5 |  0.449 % |
c |      2020 |   32302    87862 |   15799    1931    44330    23.0 |  0.449 % |
c ==============================================================================
c [1mFound solution: 24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2184 |   32330    87933 |   10776    2095    47803    22.8 |  0.449 % |
c |      2284 |   32330    87933 |   11853    2195    50493    23.0 |  0.467 % |
c |      2434 |   32330    87933 |   13038    2345    52068    22.2 |  0.467 % |
c |      2660 |   32207    87658 |   14342    2425    52611    21.7 |  0.778 % |
c |      2997 |   32207    87658 |   15777    2762    75546    27.4 |  0.778 % |
c ==============================================================================
c [1mFound solution: 23[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3307 |   27823    77625 |    9274    2752    72417    26.3 |  0.778 % |
c |      3407 |   27784    77538 |   10201    2851    74418    26.1 | 12.913 % |
c |      3561 |   27784    77538 |   11221    3005    79103    26.3 | 12.913 % |
c ==============================================================================
c [1mFound solution: 22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3695 |   27811    77606 |    9270    3139    85648    27.3 | 12.913 % |
c |      3796 |   27811    77606 |   10197    3240    88815    27.4 | 12.911 % |
c ==============================================================================
c [1mFound solution: 21[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3937 |   27780    77523 |    9260    3283    94010    28.6 | 12.911 % |
c |      4038 |   27780    77523 |   10186    3384   101422    30.0 | 13.030 % |
c |      4188 |   27780    77523 |   11204    3534   108295    30.6 | 13.028 % |
c ==============================================================================
c [1mFound solution: 20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4213 |   27803    77580 |    9267    3559   109846    30.9 | 13.028 % |
c |      4315 |   27803    77580 |   10193    3661   114004    31.1 | 13.036 % |
c |      4467 |   27803    77580 |   11213    3813   120687    31.7 | 13.036 % |
c |      4692 |   27803    77580 |   12334    4038   131801    32.6 | 13.036 % |
c |      5029 |   27803    77580 |   13567    4375   148244    33.9 | 13.036 % |
c |      5535 |   27803    77580 |   14924    4881   167957    34.4 | 13.036 % |
c |      6294 |   27803    77580 |   16417    5640   221295    39.2 | 13.036 % |
c |      7433 |   27803    77580 |   18058    6779   298159    44.0 | 13.036 % |
c |      9141 |   27803    77580 |   19864    8487   374760    44.2 | 13.036 % |
c |     11703 |   27803    77580 |   21851   11049   481722    43.6 | 13.036 % |
c ==============================================================================
c [1mFound solution: 19[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13211 |   27463    76774 |    9154   12212   523652    42.9 | 13.036 % |
c |     13312 |   27463    76774 |   10069    6207   222101    35.8 | 14.047 % |
c |     13462 |   27463    76774 |   11076    6357   229393    36.1 | 14.047 % |
c |     13687 |   27463    76774 |   12183    6582   240050    36.5 | 14.047 % |
c |     14024 |   27463    76774 |   13402    6919   253868    36.7 | 14.047 % |
c |     14532 |   27463    76774 |   14742    7427   276080    37.2 | 14.047 % |
c |     15292 |   27463    76774 |   16216    8187   307132    37.5 | 14.047 % |
c |     16433 |   27463    76774 |   17838    9328   353593    37.9 | 14.047 % |
c |     18143 |   27463    76774 |   19622   11038   409460    37.1 | 14.047 % |
c |     20706 |   27463    76774 |   21584   13601   532070    39.1 | 14.047 % |
c |     24553 |   27463    76774 |   23743   17448   684730    39.2 | 14.047 % |
c |     30319 |   27463    76774 |   26117   23214   936867    40.4 | 14.047 % |
c |     38968 |   27463    76774 |   28729   14420   580313    40.2 | 14.047 % |
c ==============================================================================
c [1mFound solution: 18[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41503 |   27485    76828 |    9161   16955   682680    40.3 | 14.047 % |
c |     41604 |   27485    76828 |   10077    8579   312700    36.4 | 14.046 % |
c |     41755 |   27485    76828 |   11084    8730   317676    36.4 | 14.046 % |
c |     41982 |   27485    76828 |   12193    8957   325192    36.3 | 14.046 % |
c |     42328 |   27485    76828 |   13412    9303   338520    36.4 | 14.046 % |
c |     42834 |   27485    76828 |   14753    9809   355907    36.3 | 14.046 % |
c |     43593 |   27485    76828 |   16229   10568   380258    36.0 | 14.046 % |
c |     44733 |   27485    76828 |   17852   11708   418476    35.7 | 14.046 % |
c |     46444 |   27485    76828 |   19637   13419   471610    35.1 | 14.046 % |
c |     49007 |   27485    76828 |   21601   15982   553496    34.6 | 14.046 % |
c |     52852 |   27485    76828 |   23761   19827   658033    33.2 | 14.046 % |
c |     58618 |   27485    76828 |   26137   25593   854059    33.4 | 14.046 % |
c |     67268 |   27485    76828 |   28751   18563   557689    30.0 | 14.046 % |
c |     80242 |   27485    76828 |   31626   31537   999852    31.7 | 14.046 % |
c |     99703 |   27442    76729 |   34788   33262  1026630    30.9 | 14.174 % |
c |    128898 |   27442    76729 |   38267   18508   645811    34.9 | 14.174 % |
c |    172688 |   27442    76729 |   42094   34799  1260627    36.2 | 14.174 % |
c |    238373 |   27371    76565 |   46304   41184  1139588    27.7 | 14.374 % |
c |    336899 |   27312    76425 |   50934   37922  1051365    27.7 | 14.539 % |
#### 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 26335
Raw data (stat): 26335 (runsolver) R 26334 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423208750 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 1472 0 0 0 995 3 0 0 25 0 1 0 423208750 7999488 1446 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1953 1446 603 41 0 1912 0
vsize: 7812
[startup+20.0008 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 1796 0 0 0 1994 4 0 0 25 0 1 0 423208750 9338880 1770 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2280 1770 603 41 0 2239 0
vsize: 9120
[startup+30.0004 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 1979 0 0 0 2992 5 0 0 25 0 1 0 423208750 10096640 1953 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2465 1953 603 41 0 2424 0
vsize: 9860
[startup+40.0015 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 1979 0 0 0 3992 5 0 0 25 0 1 0 423208750 10096640 1953 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2465 1953 603 41 0 2424 0
vsize: 9860
[startup+50.0019 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 2087 0 0 0 4992 5 0 0 25 0 1 0 423208750 10502144 2061 4294967295 134512640 134672761 3221224576 3221223712 134560608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2564 2061 603 41 0 2523 0
vsize: 10256
[startup+60.0015 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 2250 0 0 0 5992 6 0 0 25 0 1 0 423208750 11198464 2224 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2734 2224 603 41 0 2693 0
vsize: 10936
[startup+70.0026 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 2450 0 0 0 6992 6 0 0 25 0 1 0 423208750 12001280 2424 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2930 2424 603 41 0 2889 0
vsize: 11720
[startup+80.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 2664 0 0 0 7991 8 0 0 25 0 1 0 423208750 12943360 2638 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3160 2638 603 41 0 3119 0
vsize: 12640
[startup+90.0037 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 2854 0 0 0 8991 8 0 0 25 0 1 0 423208750 13758464 2828 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3359 2828 603 41 0 3318 0
vsize: 13436
[startup+100.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 2990 0 0 0 9990 9 0 0 25 0 1 0 423208750 14295040 2964 4294967295 134512640 134672761 3221224576 3221223744 134561269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3490 2964 603 41 0 3449 0
vsize: 13960
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3015 0 0 0 10989 9 0 0 25 0 1 0 423208750 14450688 2989 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3528 2989 603 41 0 3487 0
vsize: 14112
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3031 0 0 0 11989 9 0 0 25 0 1 0 423208750 14450688 3005 4294967295 134512640 134672761 3221224576 3221223760 134559590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3528 3005 603 41 0 3487 0
vsize: 14112
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3047 0 0 0 12989 9 0 0 25 0 1 0 423208750 14598144 3021 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3564 3021 603 41 0 3523 0
vsize: 14256
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3056 0 0 0 13989 9 0 0 25 0 1 0 423208750 14598144 3030 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3564 3030 603 41 0 3523 0
vsize: 14256
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3096 0 0 0 14990 9 0 0 25 0 1 0 423208750 14745600 3070 4294967295 134512640 134672761 3221224576 3221223760 134558923 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3600 3070 603 41 0 3559 0
vsize: 14400
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3100 0 0 0 15990 9 0 0 25 0 1 0 423208750 14745600 3074 4294967295 134512640 134672761 3221224576 3221223712 134560657 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3600 3074 603 41 0 3559 0
vsize: 14400
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3137 0 0 0 16990 10 0 0 25 0 1 0 423208750 14942208 3111 4294967295 134512640 134672761 3221224576 3221223680 134555211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3648 3111 603 41 0 3607 0
vsize: 14592
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3154 0 0 0 17990 10 0 0 25 0 1 0 423208750 15138816 3128 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3696 3128 603 41 0 3655 0
vsize: 14784
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3154 0 0 0 18990 10 0 0 25 0 1 0 423208750 15138816 3128 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3696 3128 603 41 0 3655 0
vsize: 14784
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3155 0 0 0 19990 10 0 0 25 0 1 0 423208750 15138816 3129 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3696 3129 603 41 0 3655 0
vsize: 14784
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3162 0 0 0 20990 10 0 0 25 0 1 0 423208750 15138816 3136 4294967295 134512640 134672761 3221224576 3221223712 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3696 3136 603 41 0 3655 0
vsize: 14784
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3164 0 0 0 21990 10 0 0 25 0 1 0 423208750 15138816 3138 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3696 3138 603 41 0 3655 0
vsize: 14784
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3191 0 0 0 22991 10 0 0 25 0 1 0 423208750 15335424 3165 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3744 3165 603 41 0 3703 0
vsize: 14976
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3253 0 0 0 23990 10 0 0 25 0 1 0 423208750 15597568 3227 4294967295 134512640 134672761 3221224576 3221223680 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3808 3227 603 41 0 3767 0
vsize: 15232
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3253 0 0 0 24991 10 0 0 25 0 1 0 423208750 15597568 3227 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3808 3227 603 41 0 3767 0
vsize: 15232
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3253 0 0 0 25991 10 0 0 25 0 1 0 423208750 15597568 3227 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3808 3227 603 41 0 3767 0
vsize: 15232
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3253 0 0 0 26991 10 0 0 25 0 1 0 423208750 15597568 3227 4294967295 134512640 134672761 3221224576 3221223760 134558332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3808 3227 603 41 0 3767 0
vsize: 15232
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3253 0 0 0 27991 10 0 0 25 0 1 0 423208750 15597568 3227 4294967295 134512640 134672761 3221224576 3221223720 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3808 3227 603 41 0 3767 0
vsize: 15232
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3253 0 0 0 28991 10 0 0 25 0 1 0 423208750 15597568 3227 4294967295 134512640 134672761 3221224576 3221223744 134561278 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3808 3227 603 41 0 3767 0
vsize: 15232
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3256 0 0 0 29991 10 0 0 25 0 1 0 423208750 15597568 3230 4294967295 134512640 134672761 3221224576 3221223700 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3808 3230 603 41 0 3767 0
vsize: 15232
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3258 0 0 0 30992 10 0 0 25 0 1 0 423208750 15597568 3232 4294967295 134512640 134672761 3221224576 3221223744 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3808 3232 603 41 0 3767 0
vsize: 15232
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3274 0 0 0 31990 11 0 0 25 0 1 0 423208750 15794176 3248 4294967295 134512640 134672761 3221224576 3221223720 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3856 3248 603 41 0 3815 0
vsize: 15424
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3274 0 0 0 32990 11 0 0 25 0 1 0 423208750 15794176 3248 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3856 3248 603 41 0 3815 0
vsize: 15424
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3285 0 0 0 33990 11 0 0 25 0 1 0 423208750 15794176 3259 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3856 3259 603 41 0 3815 0
vsize: 15424
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3286 0 0 0 34990 11 0 0 25 0 1 0 423208750 15794176 3260 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3856 3260 603 41 0 3815 0
vsize: 15424
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3287 0 0 0 35990 11 0 0 25 0 1 0 423208750 15794176 3261 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3856 3261 603 41 0 3815 0
vsize: 15424
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3318 0 0 0 36990 11 0 0 25 0 1 0 423208750 15929344 3292 4294967295 134512640 134672761 3221224576 3221223744 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3889 3292 603 41 0 3848 0
vsize: 15556
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3321 0 0 0 37991 11 0 0 25 0 1 0 423208750 15929344 3295 4294967295 134512640 134672761 3221224576 3221223744 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3889 3295 603 41 0 3848 0
vsize: 15556
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3321 0 0 0 38991 11 0 0 25 0 1 0 423208750 15929344 3295 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3889 3295 603 41 0 3848 0
vsize: 15556
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3332 0 0 0 39991 11 0 0 25 0 1 0 423208750 16064512 3306 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3922 3306 603 41 0 3881 0
vsize: 15688
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3332 0 0 0 40991 11 0 0 25 0 1 0 423208750 16064512 3306 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3922 3306 603 41 0 3881 0
vsize: 15688
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3334 0 0 0 41991 11 0 0 25 0 1 0 423208750 16064512 3308 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3922 3308 603 41 0 3881 0
vsize: 15688
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3432 0 0 0 42991 11 0 0 25 0 1 0 423208750 16347136 3406 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3991 3406 603 41 0 3950 0
vsize: 15964
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3550 0 0 0 43991 11 0 0 25 0 1 0 423208750 16879616 3524 4294967295 134512640 134672761 3221224576 3221223776 134557796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4121 3524 603 41 0 4080 0
vsize: 16484
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3703 0 0 0 44990 12 0 0 25 0 1 0 423208750 17547264 3677 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4284 3677 603 41 0 4243 0
vsize: 17136
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3822 0 0 0 45990 13 0 0 25 0 1 0 423208750 17944576 3796 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4381 3796 603 41 0 4340 0
vsize: 17524
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3829 0 0 0 46991 13 0 0 25 0 1 0 423208750 18079744 3803 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4414 3803 603 41 0 4373 0
vsize: 17656
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3841 0 0 0 47991 13 0 0 25 0 1 0 423208750 18079744 3815 4294967295 134512640 134672761 3221224576 3221223760 134558937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4414 3815 603 41 0 4373 0
vsize: 17656
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3842 0 0 0 48991 13 0 0 25 0 1 0 423208750 18079744 3816 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4414 3816 603 41 0 4373 0
vsize: 17656
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3845 0 0 0 49991 13 0 0 25 0 1 0 423208750 18079744 3819 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4414 3819 603 41 0 4373 0
vsize: 17656
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3846 0 0 0 50991 13 0 0 25 0 1 0 423208750 18079744 3820 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4414 3820 603 41 0 4373 0
vsize: 17656
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3866 0 0 0 51990 13 0 0 25 0 1 0 423208750 18227200 3840 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4450 3840 603 41 0 4409 0
vsize: 17800
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3878 0 0 0 52990 13 0 0 25 0 1 0 423208750 18227200 3852 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4450 3852 603 41 0 4409 0
vsize: 17800
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3887 0 0 0 53990 13 0 0 25 0 1 0 423208750 18227200 3861 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4450 3861 603 41 0 4409 0
vsize: 17800
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3901 0 0 0 54991 13 0 0 25 0 1 0 423208750 18227200 3875 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4450 3875 603 41 0 4409 0
vsize: 17800
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3901 0 0 0 55991 13 0 0 25 0 1 0 423208750 18227200 3875 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4450 3875 603 41 0 4409 0
vsize: 17800
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3906 0 0 0 56991 13 0 0 25 0 1 0 423208750 18391040 3880 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3880 603 41 0 4449 0
vsize: 17960
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3911 0 0 0 57991 13 0 0 25 0 1 0 423208750 18391040 3885 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3885 603 41 0 4449 0
vsize: 17960
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3917 0 0 0 58992 13 0 0 25 0 1 0 423208750 18391040 3891 4294967295 134512640 134672761 3221224576 3221223744 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3891 603 41 0 4449 0
vsize: 17960
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3918 0 0 0 59992 13 0 0 25 0 1 0 423208750 18391040 3892 4294967295 134512640 134672761 3221224576 3221223744 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3892 603 41 0 4449 0
vsize: 17960
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3920 0 0 0 60992 13 0 0 25 0 1 0 423208750 18391040 3894 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3894 603 41 0 4449 0
vsize: 17960
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3921 0 0 0 61992 13 0 0 25 0 1 0 423208750 18391040 3895 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3895 603 41 0 4449 0
vsize: 17960
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3921 0 0 0 62992 13 0 0 25 0 1 0 423208750 18391040 3895 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3895 603 41 0 4449 0
vsize: 17960
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3921 0 0 0 63992 13 0 0 25 0 1 0 423208750 18391040 3895 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3895 603 41 0 4449 0
vsize: 17960
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3927 0 0 0 64993 13 0 0 25 0 1 0 423208750 18391040 3901 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3901 603 41 0 4449 0
vsize: 17960
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3927 0 0 0 65993 13 0 0 25 0 1 0 423208750 18391040 3901 4294967295 134512640 134672761 3221224576 3221223680 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3901 603 41 0 4449 0
vsize: 17960
[startup+670.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3927 0 0 0 66993 13 0 0 25 0 1 0 423208750 18391040 3901 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3901 603 41 0 4449 0
vsize: 17960
[startup+680.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3927 0 0 0 67993 13 0 0 25 0 1 0 423208750 18391040 3901 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3901 603 41 0 4449 0
vsize: 17960
[startup+690.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3927 0 0 0 68993 13 0 0 25 0 1 0 423208750 18391040 3901 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3901 603 41 0 4449 0
vsize: 17960
[startup+700.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3927 0 0 0 69994 13 0 0 25 0 1 0 423208750 18391040 3901 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3901 603 41 0 4449 0
vsize: 17960
[startup+710.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3927 0 0 0 70994 13 0 0 25 0 1 0 423208750 18391040 3901 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3901 603 41 0 4449 0
vsize: 17960
[startup+720.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3927 0 0 0 71994 13 0 0 25 0 1 0 423208750 18391040 3901 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3901 603 41 0 4449 0
vsize: 17960
[startup+730.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3945 0 0 0 72994 14 0 0 25 0 1 0 423208750 18554880 3919 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4530 3919 603 41 0 4489 0
vsize: 18120
[startup+740.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3949 0 0 0 73993 14 0 0 25 0 1 0 423208750 18554880 3923 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4530 3923 603 41 0 4489 0
vsize: 18120
[startup+750.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3952 0 0 0 74994 14 0 0 25 0 1 0 423208750 18554880 3926 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4530 3926 603 41 0 4489 0
vsize: 18120
[startup+760.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3954 0 0 0 75994 14 0 0 25 0 1 0 423208750 18554880 3928 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4530 3928 603 41 0 4489 0
vsize: 18120
[startup+770.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3954 0 0 0 76994 14 0 0 25 0 1 0 423208750 18554880 3928 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4530 3928 603 41 0 4489 0
vsize: 18120
[startup+780.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3954 0 0 0 77994 14 0 0 25 0 1 0 423208750 18554880 3928 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4530 3928 603 41 0 4489 0
vsize: 18120
[startup+790.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3954 0 0 0 78994 14 0 0 25 0 1 0 423208750 18554880 3928 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4530 3928 603 41 0 4489 0
vsize: 18120
[startup+800.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3954 0 0 0 79995 14 0 0 25 0 1 0 423208750 18554880 3928 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4530 3928 603 41 0 4489 0
vsize: 18120
[startup+810.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3955 0 0 0 80995 14 0 0 25 0 1 0 423208750 18554880 3929 4294967295 134512640 134672761 3221224576 3221223744 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4530 3929 603 41 0 4489 0
vsize: 18120
[startup+820.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3955 0 0 0 81995 14 0 0 25 0 1 0 423208750 18554880 3929 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4530 3929 603 41 0 4489 0
vsize: 18120
[startup+830.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3961 0 0 0 82995 14 0 0 25 0 1 0 423208750 18554880 3935 4294967295 134512640 134672761 3221224576 3221223776 134557892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4530 3935 603 41 0 4489 0
vsize: 18120
[startup+840.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3969 0 0 0 83995 14 0 0 25 0 1 0 423208750 18554880 3943 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4530 3943 603 41 0 4489 0
vsize: 18120
[startup+850.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3969 0 0 0 84995 14 0 0 25 0 1 0 423208750 18554880 3943 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4530 3943 603 41 0 4489 0
vsize: 18120
[startup+860.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3982 0 0 0 85996 14 0 0 25 0 1 0 423208750 18751488 3956 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4578 3956 603 41 0 4537 0
vsize: 18312
[startup+870.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4048 0 0 0 86996 14 0 0 25 0 1 0 423208750 19030016 4022 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4646 4022 603 41 0 4605 0
vsize: 18584
[startup+880.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4052 0 0 0 87996 14 0 0 25 0 1 0 423208750 19030016 4026 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4646 4026 603 41 0 4605 0
vsize: 18584
[startup+890.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4052 0 0 0 88996 14 0 0 25 0 1 0 423208750 19030016 4026 4294967295 134512640 134672761 3221224576 3221223744 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4646 4026 603 41 0 4605 0
vsize: 18584
[startup+900.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4052 0 0 0 89996 14 0 0 25 0 1 0 423208750 19030016 4026 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4646 4026 603 41 0 4605 0
vsize: 18584
[startup+910.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4052 0 0 0 90996 14 0 0 25 0 1 0 423208750 19030016 4026 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4646 4026 603 41 0 4605 0
vsize: 18584
[startup+920.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4052 0 0 0 91997 14 0 0 25 0 1 0 423208750 19030016 4026 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4646 4026 603 41 0 4605 0
vsize: 18584
[startup+930.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4058 0 0 0 92997 14 0 0 25 0 1 0 423208750 19030016 4032 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4646 4032 603 41 0 4605 0
vsize: 18584
[startup+940.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4058 0 0 0 93997 14 0 0 25 0 1 0 423208750 19030016 4032 4294967295 134512640 134672761 3221224576 3221223712 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4646 4032 603 41 0 4605 0
vsize: 18584
[startup+950.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4058 0 0 0 94997 14 0 0 25 0 1 0 423208750 19030016 4032 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4646 4032 603 41 0 4605 0
vsize: 18584
[startup+960.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4071 0 0 0 95997 14 0 0 25 0 1 0 423208750 19177472 4045 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4682 4045 603 41 0 4641 0
vsize: 18728
[startup+970.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4076 0 0 0 96997 14 0 0 25 0 1 0 423208750 19177472 4050 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4682 4050 603 41 0 4641 0
vsize: 18728
[startup+980.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4076 0 0 0 97997 14 0 0 25 0 1 0 423208750 19177472 4050 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4682 4050 603 41 0 4641 0
vsize: 18728
[startup+990.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4076 0 0 0 98998 14 0 0 25 0 1 0 423208750 19177472 4050 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4682 4050 603 41 0 4641 0
vsize: 18728
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4076 0 0 0 99998 14 0 0 25 0 1 0 423208750 19177472 4050 4294967295 134512640 134672761 3221224576 3221223760 134559572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4682 4050 603 41 0 4641 0
vsize: 18728
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4076 0 0 0 100998 14 0 0 25 0 1 0 423208750 19177472 4050 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4682 4050 603 41 0 4641 0
vsize: 18728
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4076 0 0 0 101998 14 0 0 25 0 1 0 423208750 19177472 4050 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4682 4050 603 41 0 4641 0
vsize: 18728
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4088 0 0 0 102998 14 0 0 25 0 1 0 423208750 19177472 4062 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4682 4062 603 41 0 4641 0
vsize: 18728
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4088 0 0 0 103997 14 0 0 25 0 1 0 423208750 19177472 4062 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4682 4062 603 41 0 4641 0
vsize: 18728
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4091 0 0 0 104997 14 0 0 25 0 1 0 423208750 19177472 4065 4294967295 134512640 134672761 3221224576 3221223712 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4682 4065 603 41 0 4641 0
vsize: 18728
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4091 0 0 0 105997 14 0 0 25 0 1 0 423208750 19177472 4065 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4682 4065 603 41 0 4641 0
vsize: 18728
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4101 0 0 0 106997 15 0 0 25 0 1 0 423208750 19324928 4075 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4718 4075 603 41 0 4677 0
vsize: 18872
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4104 0 0 0 107997 15 0 0 25 0 1 0 423208750 19324928 4078 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4718 4078 603 41 0 4677 0
vsize: 18872
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4107 0 0 0 108998 15 0 0 25 0 1 0 423208750 19324928 4081 4294967295 134512640 134672761 3221224576 3221223712 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4718 4081 603 41 0 4677 0
vsize: 18872
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4108 0 0 0 109998 15 0 0 25 0 1 0 423208750 19324928 4082 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4718 4082 603 41 0 4677 0
vsize: 18872
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4108 0 0 0 110998 15 0 0 25 0 1 0 423208750 19324928 4082 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4718 4082 603 41 0 4677 0
vsize: 18872
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4108 0 0 0 111998 15 0 0 25 0 1 0 423208750 19324928 4082 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4718 4082 603 41 0 4677 0
vsize: 18872
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26335
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4108 0 0 0 112999 15 0 0 25 0 1 0 423208750 19324928 4082 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4718 4082 603 41 0 4677 0
vsize: 18872
[startup+1140.02 s]
Raw data (loadavg): 1.07 0.99 0.92 2/57 26338
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4116 0 0 0 113999 15 0 0 25 0 1 0 423208750 19324928 4090 4294967295 134512640 134672761 3221224576 3221223712 134560585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4718 4090 603 41 0 4677 0
vsize: 18872
[startup+1150.02 s]
Raw data (loadavg): 1.14 1.00 0.93 2/54 26388
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4117 0 0 0 114999 15 0 0 25 0 1 0 423208750 19324928 4091 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4718 4091 603 41 0 4677 0
vsize: 18872
[startup+1160.02 s]
Raw data (loadavg): 1.11 1.00 0.93 2/54 26388
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4136 0 0 0 115999 15 0 0 25 0 1 0 423208750 19505152 4110 4294967295 134512640 134672761 3221224576 3221223744 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4762 4110 603 41 0 4721 0
vsize: 19048
[startup+1170.02 s]
Raw data (loadavg): 1.10 1.00 0.93 2/54 26388
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4137 0 0 0 116999 15 0 0 25 0 1 0 423208750 19505152 4111 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4762 4111 603 41 0 4721 0
vsize: 19048
[startup+1180.02 s]
Raw data (loadavg): 1.08 1.00 0.93 2/54 26388
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4137 0 0 0 117999 15 0 0 25 0 1 0 423208750 19505152 4111 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4762 4111 603 41 0 4721 0
vsize: 19048
[startup+1190.02 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 26388
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4158 0 0 0 118999 15 0 0 25 0 1 0 423208750 19505152 4132 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4762 4132 603 41 0 4721 0
vsize: 19048
[startup+1200.02 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 26388
Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4160 0 0 0 119999 15 0 0 25 0 1 0 423208750 19505152 4134 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4762 4134 603 41 0 4721 0
vsize: 19048
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.06 1.00 0.93 1/54 26388
Raw data (stat): 26335 (minisat+) Z 26334 20937 20936 0 -1 12 4163 0 0 0 119999 16 0 0 25 0 1 0 423208750 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: 10
Real time (s): 1200.03
CPU time (s): 1200.16
CPU user time (s): 1200
CPU system time (s): 0.162975
CPU usage (%): 100.011
Max. virtual memory (Kb): 19048
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####