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/primes-dimacs-cnf/normalized-ii32d1.opb
MD5SUM	151e246868267296e134c3c76a3cb289
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	285
Optimality of the best value was proved	NO
Number of terms in the objective function	664
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	664
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	664
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02484
Number of variables	664
Total number of constraints	3035
Number of constraints which are clauses	3035
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	32
Trace number 5880

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-14 02:08:23 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4291 boxname=wulflinc10 idbench=155 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  151e246868267296e134c3c76a3cb289  /oldhome/oroussel/tmp/wulflinc10/normalized-ii32d1.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc10/normalized-ii32d1.opb /oldhome/oroussel/tmp/wulflinc10/normalized-ii32d1.opb
IDLAUNCH: 4291
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        865192 kB
Buffers:         35272 kB
Cached:         114844 kB
SwapCached:        164 kB
Active:          54072 kB
Inactive:        99012 kB
HighTotal:      131008 kB
HighFree:        12600 kB
LowTotal:       903652 kB
LowFree:        852592 kB
SwapTotal:     2097136 kB
SwapFree:      2096972 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10916 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:28:25 (client local time) WITH STATUS 10 IN 1200.13 SECONDS
stats: 4291 7 1200.13 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3035 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 |    3035     9828 |    1011       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 319[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:30182     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        22 |   39401    94869 |   13133      22      879    40.0 |  0.000 % |
c ==============================================================================
c [1mFound solution: 304[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 |        78 |   39566    95345 |   13188      77     5158    67.0 |  0.000 % |
c ==============================================================================
c [1mFound solution: 294[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 |        82 |   39693    95707 |   13231      81     5475    67.6 |  0.000 % |
c |       182 |   39693    95707 |   14554     181    15088    83.4 |  0.172 % |
c |       334 |   39693    95707 |   16009     333    24915    74.8 |  0.172 % |
c |       559 |   39693    95707 |   17610     558    43774    78.4 |  0.172 % |
c |       897 |   39610    95534 |   19371     893    84437    94.6 |  0.353 % |
c |      1403 |   39610    95534 |   21308    1399   139614    99.8 |  0.353 % |
c |      2164 |   39439    95178 |   23439    2155   228675   106.1 |  0.718 % |
c |      3305 |   39396    95089 |   25783    3295   356671   108.2 |  0.806 % |
c |      5014 |   39147    94550 |   28361    4996   564213   112.9 |  1.379 % |
c ==============================================================================
c [1mFound solution: 293[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 |      6786 |   39147    94597 |   13049    6766   805584   119.1 |  1.379 % |
c |      6886 |   38248    92654 |   14353    6843   807275   118.0 |  3.544 % |
c |      7036 |   38101    92333 |   15789    6978   810806   116.2 |  3.889 % |
c |      7261 |   38101    92333 |   17368    7203   835914   116.1 |  3.889 % |
c |      7598 |   38101    92333 |   19105    7540   859380   114.0 |  3.889 % |
c |      8107 |   38058    92242 |   21015    8048   902377   112.1 |  3.985 % |
c |      8867 |   37957    92027 |   23117    8806   985841   112.0 |  4.209 % |
c |     10007 |   37816    91714 |   25428    9942  1069396   107.6 |  4.550 % |
c |     11717 |   37684    91426 |   27971   11649  1217804   104.5 |  4.858 % |
c |     14279 |   37684    91426 |   30768   14211  1480329   104.2 |  4.858 % |
c |     18124 |   35697    87013 |   33845   17979  1810517   100.7 |  9.636 % |
c |     23891 |   35469    86509 |   37230   23742  2607070   109.8 | 10.169 % |
c |     32540 |   35409    86375 |   40953   32384  3450033   106.5 | 10.317 % |
c |     45515 |   35296    86126 |   45048   15064  1255595    83.4 | 10.585 % |
c ==============================================================================
c [1mFound solution: 292[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 |     51755 |   35264    86031 |   11754   21218  1737423    81.9 | 10.585 % |
c |     51858 |   35264    86031 |   12929   10712   660163    61.6 | 10.688 % |
c |     52010 |   35264    86031 |   14222   10864   673235    62.0 | 10.688 % |
c |     52238 |   35264    86031 |   15644   11092   680554    61.4 | 10.688 % |
c |     52575 |   35264    86031 |   17209   11429   710291    62.1 | 10.688 % |
c |     53081 |   35264    86031 |   18929   11935   753857    63.2 | 10.688 % |
c |     53840 |   35264    86031 |   20822   12694   821047    64.7 | 10.688 % |
c |     54983 |   35264    86031 |   22905   13837   917888    66.3 | 10.688 % |
c |     56691 |   35264    86031 |   25195   15545  1062283    68.3 | 10.688 % |
c |     59253 |   35264    86031 |   27715   18107  1325662    73.2 | 10.688 % |
c |     63098 |   35264    86031 |   30486   21952  1774222    80.8 | 10.688 % |
c |     68864 |   35212    85914 |   33535   27717  2220091    80.1 | 10.817 % |
c |     77513 |   35212    85914 |   36889   36366  2981361    82.0 | 10.817 % |
c |     90487 |   35212    85914 |   40577   23247  1770661    76.2 | 10.817 % |
c |    109948 |   35153    85787 |   44635   42707  3210142    75.2 | 10.953 % |
c |    139140 |   35153    85787 |   49099   40523  2721836    67.2 | 10.953 % |
c ==============================================================================
c [1mFound solution: 291[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 |    148770 |   35121    85732 |   11707   50152  3413506    68.1 | 10.953 % |
c |    148871 |   35121    85732 |   12877    9760   464349    47.6 | 11.093 % |
c |    149026 |   35121    85732 |   14165    9915   478892    48.3 | 11.093 % |
c |    149251 |   35121    85732 |   15582   10140   496222    48.9 | 11.093 % |
c |    149591 |   35121    85732 |   17140   10480   520952    49.7 | 11.093 % |
c |    150097 |   35121    85732 |   18854   10986   558194    50.8 | 11.093 % |
c |    150858 |   35121    85732 |   20739   11747   618457    52.6 | 11.093 % |
c |    151998 |   35121    85732 |   22813   12887   693350    53.8 | 11.093 % |
c |    153707 |   35121    85732 |   25094   14596   828225    56.7 | 11.093 % |
c |    156271 |   34396    84085 |   27604   17133   993365    58.0 | 12.902 % |
c |    160118 |   34396    84085 |   30364   20980  1393378    66.4 | 12.902 % |
c |    165886 |   34396    84085 |   33401   26748  2021075    75.6 | 12.902 % |
c |    174535 |   34396    84085 |   36741   35397  2864710    80.9 | 12.902 % |
c |    187509 |   34396    84085 |   40415   23543  1656176    70.3 | 12.902 % |
c ==============================================================================
c [1mFound solution: 290[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 |    205542 |   34380    84019 |   11460   41576  3086386    74.2 | 12.902 % |
c |    205642 |   34380    84019 |   12606    8593   377408    43.9 | 12.961 % |
c |    205794 |   34380    84019 |   13866    8745   388045    44.4 | 12.961 % |
c |    206019 |   34380    84019 |   15253    8970   404742    45.1 | 12.961 % |
c |    206356 |   34380    84019 |   16778    9307   431358    46.3 | 12.961 % |
c |    206863 |   34380    84019 |   18456    9814   473568    48.3 | 12.961 % |
c |    207622 |   34380    84019 |   20302   10573   515082    48.7 | 12.961 % |
c |    208764 |   34380    84019 |   22332   11715   574466    49.0 | 12.961 % |
c |    210472 |   34380    84019 |   24565   13423   669115    49.8 | 12.961 % |
c |    213034 |   34380    84019 |   27022   15985   795872    49.8 | 12.961 % |
c |    216881 |   34380    84019 |   29724   19832   998091    50.3 | 12.961 % |
c |    222647 |   34380    84019 |   32696   25598  1341738    52.4 | 12.961 % |
c |    231296 |   34380    84019 |   35966   34247  2022239    59.0 | 12.961 % |
c |    244270 |   34380    84019 |   39563   21209  1538693    72.5 | 12.961 % |
#### 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.94 0.97 0.92 2/54 31216
Raw data (stat): 31216 (runsolver) R 31215 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422657700 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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+9.99986 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 2652 0 0 0 991 8 0 0 25 0 1 0 422657700 12869632 2576 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3142 2576 603 41 0 3101 0
vsize: 12568
[startup+20.0009 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 2980 0 0 0 1989 9 0 0 25 0 1 0 422657700 14192640 2904 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3465 2904 603 41 0 3424 0
vsize: 13860
[startup+30.001 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 3359 0 0 0 2989 9 0 0 25 0 1 0 422657700 15716352 3283 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3837 3283 603 41 0 3796 0
vsize: 15348
[startup+40.0015 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 3756 0 0 0 3987 11 0 0 25 0 1 0 422657700 17326080 3680 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4230 3680 603 41 0 4189 0
vsize: 16920
[startup+50.0025 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 4075 0 0 0 4986 12 0 0 25 0 1 0 422657700 18657280 3999 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4555 3999 603 41 0 4514 0
vsize: 18220
[startup+60.0016 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 4288 0 0 0 5985 13 0 0 25 0 1 0 422657700 19599360 4212 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4785 4212 603 41 0 4744 0
vsize: 19140
[startup+70.0022 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 4544 0 0 0 6984 14 0 0 25 0 1 0 422657700 20664320 4468 4294967295 134512640 134672761 3221224560 3221223744 134559572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5045 4468 603 41 0 5004 0
vsize: 20180
[startup+80.0032 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 4829 0 0 0 7982 16 0 0 25 0 1 0 422657700 21860352 4753 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5337 4753 603 41 0 5296 0
vsize: 21348
[startup+90.0033 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 5159 0 0 0 8981 17 0 0 25 0 1 0 422657700 23207936 5083 4294967295 134512640 134672761 3221224560 3221223664 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5666 5083 603 41 0 5625 0
vsize: 22664
[startup+100.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 5388 0 0 0 9980 18 0 0 25 0 1 0 422657700 24129536 5312 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5891 5312 603 41 0 5850 0
vsize: 23564
[startup+110.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 5587 0 0 0 10978 19 0 0 25 0 1 0 422657700 24920064 5511 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6084 5511 603 41 0 6043 0
vsize: 24336
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 5776 0 0 0 11977 21 0 0 25 0 1 0 422657700 25718784 5700 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6279 5700 603 41 0 6238 0
vsize: 25116
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 5961 0 0 0 12977 21 0 0 25 0 1 0 422657700 26378240 5885 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6440 5885 603 41 0 6399 0
vsize: 25760
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 6159 0 0 0 13976 22 0 0 25 0 1 0 422657700 27185152 6083 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6637 6083 603 41 0 6596 0
vsize: 26548
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 6351 0 0 0 14975 23 0 0 25 0 1 0 422657700 28119040 6275 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6865 6275 603 41 0 6824 0
vsize: 27460
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 6555 0 0 0 15973 24 0 0 25 0 1 0 422657700 28913664 6479 4294967295 134512640 134672761 3221224560 3221223704 134560555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7059 6479 603 41 0 7018 0
vsize: 28236
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 6749 0 0 0 16972 25 0 0 25 0 1 0 422657700 29700096 6673 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7251 6673 603 41 0 7210 0
vsize: 29004
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 6956 0 0 0 17971 26 0 0 25 0 1 0 422657700 30621696 6880 4294967295 134512640 134672761 3221224560 3221223664 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6880 603 41 0 7435 0
vsize: 29904
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7204 0 0 0 18969 28 0 0 25 0 1 0 422657700 31551488 7128 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7703 7128 603 41 0 7662 0
vsize: 30812
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7394 0 0 0 19969 29 0 0 25 0 1 0 422657700 32346112 7318 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7897 7318 603 41 0 7856 0
vsize: 31588
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 20968 29 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223744 134559324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 21968 29 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223760 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 22968 30 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 23967 30 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 24967 30 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223664 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 25966 31 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 26966 31 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 27966 31 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 28965 32 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 29965 32 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 30964 33 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223664 134560002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 31964 33 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 32964 33 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 33963 33 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 34963 34 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 35962 34 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 36962 34 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223728 134559670 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 37962 35 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 38961 35 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 39962 35 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223664 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 40962 35 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 41962 35 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7551 0 0 0 42962 35 0 0 25 0 1 0 422657700 33009664 7475 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8059 7475 603 41 0 8018 0
vsize: 32236
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7560 0 0 0 43963 35 0 0 25 0 1 0 422657700 33189888 7484 4294967295 134512640 134672761 3221224560 3221223716 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7484 603 41 0 8062 0
vsize: 32412
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7561 0 0 0 44963 35 0 0 25 0 1 0 422657700 33189888 7485 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7485 603 41 0 8062 0
vsize: 32412
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7561 0 0 0 45963 35 0 0 25 0 1 0 422657700 33189888 7485 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7485 603 41 0 8062 0
vsize: 32412
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7561 0 0 0 46963 35 0 0 25 0 1 0 422657700 33189888 7485 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7485 603 41 0 8062 0
vsize: 32412
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7561 0 0 0 47963 35 0 0 25 0 1 0 422657700 33189888 7485 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7485 603 41 0 8062 0
vsize: 32412
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7561 0 0 0 48963 35 0 0 25 0 1 0 422657700 33189888 7485 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7485 603 41 0 8062 0
vsize: 32412
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7561 0 0 0 49964 35 0 0 25 0 1 0 422657700 33189888 7485 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7485 603 41 0 8062 0
vsize: 32412
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7562 0 0 0 50964 35 0 0 25 0 1 0 422657700 33189888 7486 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7486 603 41 0 8062 0
vsize: 32412
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7564 0 0 0 51964 35 0 0 25 0 1 0 422657700 33189888 7488 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7488 603 41 0 8062 0
vsize: 32412
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7574 0 0 0 52964 35 0 0 25 0 1 0 422657700 33189888 7498 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7498 603 41 0 8062 0
vsize: 32412
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7576 0 0 0 53964 35 0 0 25 0 1 0 422657700 33189888 7500 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7500 603 41 0 8062 0
vsize: 32412
[startup+550.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7578 0 0 0 54964 35 0 0 25 0 1 0 422657700 33189888 7502 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7502 603 41 0 8062 0
vsize: 32412
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7586 0 0 0 55965 35 0 0 25 0 1 0 422657700 33189888 7510 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7510 603 41 0 8062 0
vsize: 32412
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7587 0 0 0 56965 35 0 0 25 0 1 0 422657700 33189888 7511 4294967295 134512640 134672761 3221224560 3221223728 134561261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7511 603 41 0 8062 0
vsize: 32412
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7587 0 0 0 57965 35 0 0 25 0 1 0 422657700 33189888 7511 4294967295 134512640 134672761 3221224560 3221223760 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7511 603 41 0 8062 0
vsize: 32412
[startup+590.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7587 0 0 0 58965 35 0 0 25 0 1 0 422657700 33189888 7511 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7511 603 41 0 8062 0
vsize: 32412
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7587 0 0 0 59965 35 0 0 25 0 1 0 422657700 33189888 7511 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7511 603 41 0 8062 0
vsize: 32412
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7587 0 0 0 60966 35 0 0 25 0 1 0 422657700 33189888 7511 4294967295 134512640 134672761 3221224560 3221223664 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7511 603 41 0 8062 0
vsize: 32412
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7587 0 0 0 61966 35 0 0 25 0 1 0 422657700 33189888 7511 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7511 603 41 0 8062 0
vsize: 32412
[startup+630.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7587 0 0 0 62966 35 0 0 25 0 1 0 422657700 33189888 7511 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7511 603 41 0 8062 0
vsize: 32412
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7587 0 0 0 63966 35 0 0 25 0 1 0 422657700 33189888 7511 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7511 603 41 0 8062 0
vsize: 32412
[startup+650.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7587 0 0 0 64966 35 0 0 25 0 1 0 422657700 33189888 7511 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7511 603 41 0 8062 0
vsize: 32412
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7587 0 0 0 65966 35 0 0 25 0 1 0 422657700 33189888 7511 4294967295 134512640 134672761 3221224560 3221223692 1075347104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7511 603 41 0 8062 0
vsize: 32412
[startup+670.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7597 0 0 0 66967 35 0 0 25 0 1 0 422657700 33353728 7521 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8143 7521 603 41 0 8102 0
vsize: 32572
[startup+680.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7609 0 0 0 67967 35 0 0 25 0 1 0 422657700 33353728 7533 4294967295 134512640 134672761 3221224560 3221223696 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8143 7533 603 41 0 8102 0
vsize: 32572
[startup+690.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7630 0 0 0 68966 35 0 0 25 0 1 0 422657700 33550336 7554 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8191 7554 603 41 0 8150 0
vsize: 32764
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7644 0 0 0 69965 36 0 0 25 0 1 0 422657700 33550336 7568 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8191 7568 603 41 0 8150 0
vsize: 32764
[startup+710.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7644 0 0 0 70966 36 0 0 25 0 1 0 422657700 33550336 7568 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8191 7568 603 41 0 8150 0
vsize: 32764
[startup+720.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7681 0 0 0 71966 36 0 0 25 0 1 0 422657700 33746944 7605 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8239 7605 603 41 0 8198 0
vsize: 32956
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7698 0 0 0 72966 36 0 0 25 0 1 0 422657700 33746944 7622 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8239 7622 603 41 0 8198 0
vsize: 32956
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 73966 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+750.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 74966 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+760.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 75966 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+770.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 76966 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223664 134559964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+780.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 77967 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+790.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 78967 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+800.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 79967 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223696 134560622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+810.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 80967 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223664 134559890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+820.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 81967 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+830.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 82967 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+840.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 83968 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223664 134560279 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+850.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 84968 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+860.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 85968 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+870.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 86968 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+880.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 87968 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+890.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 88969 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+900.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 89969 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+910.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 90969 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+920.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 91969 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+930.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 92969 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+940.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 93969 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+950.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 94970 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223664 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+960.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 95970 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+970.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 96970 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+980.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 97970 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+990.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 98970 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 99971 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7700 0 0 0 100971 36 0 0 25 0 1 0 422657700 33943552 7624 4294967295 134512640 134672761 3221224560 3221223744 134558513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7624 603 41 0 8246 0
vsize: 33148
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7701 0 0 0 101971 36 0 0 25 0 1 0 422657700 33943552 7625 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7625 603 41 0 8246 0
vsize: 33148
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7701 0 0 0 102971 36 0 0 25 0 1 0 422657700 33943552 7625 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7625 603 41 0 8246 0
vsize: 33148
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7701 0 0 0 103971 36 0 0 25 0 1 0 422657700 33943552 7625 4294967295 134512640 134672761 3221224560 3221223720 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7625 603 41 0 8246 0
vsize: 33148
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7701 0 0 0 104972 36 0 0 25 0 1 0 422657700 33943552 7625 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7625 603 41 0 8246 0
vsize: 33148
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7701 0 0 0 105972 36 0 0 25 0 1 0 422657700 33943552 7625 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7625 603 41 0 8246 0
vsize: 33148
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7701 0 0 0 106972 36 0 0 25 0 1 0 422657700 33943552 7625 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7625 603 41 0 8246 0
vsize: 33148
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7701 0 0 0 107972 36 0 0 25 0 1 0 422657700 33943552 7625 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7625 603 41 0 8246 0
vsize: 33148
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7701 0 0 0 108972 36 0 0 25 0 1 0 422657700 33943552 7625 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7625 603 41 0 8246 0
vsize: 33148
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7701 0 0 0 109972 36 0 0 25 0 1 0 422657700 33943552 7625 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7625 603 41 0 8246 0
vsize: 33148
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7701 0 0 0 110973 36 0 0 25 0 1 0 422657700 33943552 7625 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7625 603 41 0 8246 0
vsize: 33148
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7701 0 0 0 111973 36 0 0 25 0 1 0 422657700 33943552 7625 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7625 603 41 0 8246 0
vsize: 33148
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7701 0 0 0 112973 36 0 0 25 0 1 0 422657700 33943552 7625 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7625 603 41 0 8246 0
vsize: 33148
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7701 0 0 0 113973 36 0 0 25 0 1 0 422657700 33943552 7625 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7625 603 41 0 8246 0
vsize: 33148
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7701 0 0 0 114973 36 0 0 25 0 1 0 422657700 33943552 7625 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7625 603 41 0 8246 0
vsize: 33148
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7701 0 0 0 115973 36 0 0 25 0 1 0 422657700 33943552 7625 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7625 603 41 0 8246 0
vsize: 33148
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7701 0 0 0 116974 36 0 0 25 0 1 0 422657700 33943552 7625 4294967295 134512640 134672761 3221224560 3221223744 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7625 603 41 0 8246 0
vsize: 33148
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7701 0 0 0 117974 36 0 0 25 0 1 0 422657700 33943552 7625 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7625 603 41 0 8246 0
vsize: 33148
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7701 0 0 0 118974 36 0 0 25 0 1 0 422657700 33943552 7625 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7625 603 41 0 8246 0
vsize: 33148
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31216
Raw data (stat): 31216 (minisat+) R 31215 25347 25346 0 -1 0 7701 0 0 0 119974 36 0 0 25 0 1 0 422657700 33943552 7625 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7625 603 41 0 8246 0
vsize: 33148
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 31216
Raw data (stat): 31216 (minisat+) Z 31215 25347 25346 0 -1 12 7704 0 0 0 119974 37 0 0 25 0 1 0 422657700 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: 10
Real time (s): 1200.03
CPU time (s): 1200.13
CPU user time (s): 1199.75
CPU system time (s): 0.378942
CPU usage (%): 100.008
Max. virtual memory (Kb): 33148
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####