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 4914

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-13 20:48:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=1391 boxname=wulflinc17 idbench=155 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  151e246868267296e134c3c76a3cb289  /oldhome/oroussel/tmp/wulflinc17/normalized-ii32d1.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc17/normalized-ii32d1.opb
IDLAUNCH: 1391
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        849796 kB
Buffers:         34280 kB
Cached:         116004 kB
SwapCached:       2376 kB
Active:          51540 kB
Inactive:       104108 kB
HighTotal:      131008 kB
HighFree:        11424 kB
LowTotal:       903652 kB
LowFree:        838372 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            23568 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:08:55 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 1391 7 1200.19 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.86 0.93 0.90 2/55 25250
Raw data (stat): 25250 (runsolver) R 25249 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478962018 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0005 s]
Raw data (loadavg): 0.88 0.93 0.90 2/55 25250
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 2677 0 0 0 992 6 0 0 25 0 1 0 478962018 12935168 2604 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3158 2604 603 41 0 3117 0
vsize: 12632
[startup+20.001 s]
Raw data (loadavg): 0.90 0.93 0.90 2/55 25250
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 3010 0 0 0 1990 8 0 0 25 0 1 0 478962018 14282752 2937 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3487 2937 603 41 0 3446 0
vsize: 13948
[startup+30.0016 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 25250
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 3392 0 0 0 2989 10 0 0 25 0 1 0 478962018 15941632 3319 4294967295 134512640 134672761 3221224640 3221223744 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3892 3319 603 41 0 3851 0
vsize: 15568
[startup+40.0022 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 25250
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 3791 0 0 0 3987 12 0 0 25 0 1 0 478962018 17551360 3718 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4285 3718 603 41 0 4244 0
vsize: 17140
[startup+50.0028 s]
Raw data (loadavg): 0.94 0.94 0.90 2/55 25250
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 4113 0 0 0 4986 13 0 0 25 0 1 0 478962018 18878464 4040 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4609 4040 603 41 0 4568 0
vsize: 18436
[startup+60.0024 s]
Raw data (loadavg): 0.95 0.94 0.91 2/55 25250
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 4325 0 0 0 5985 14 0 0 25 0 1 0 478962018 19689472 4252 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4807 4252 603 41 0 4766 0
vsize: 19228
[startup+70.003 s]
Raw data (loadavg): 0.95 0.94 0.91 2/55 25250
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 4581 0 0 0 6983 15 0 0 25 0 1 0 478962018 20758528 4508 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5068 4508 603 41 0 5027 0
vsize: 20272
[startup+80.0036 s]
Raw data (loadavg): 0.96 0.94 0.91 2/55 25250
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 4874 0 0 0 7982 16 0 0 25 0 1 0 478962018 21966848 4801 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5363 4801 603 41 0 5322 0
vsize: 21452
[startup+90.0042 s]
Raw data (loadavg): 0.97 0.94 0.91 2/55 25250
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 5206 0 0 0 8980 18 0 0 25 0 1 0 478962018 23298048 5133 4294967295 134512640 134672761 3221224640 3221223744 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5688 5133 603 41 0 5647 0
vsize: 22752
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 25250
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 5428 0 0 0 9979 19 0 0 25 0 1 0 478962018 24215552 5355 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5912 5355 603 41 0 5871 0
vsize: 23648
[startup+110.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 5632 0 0 0 10977 21 0 0 25 0 1 0 478962018 25010176 5559 4294967295 134512640 134672761 3221224640 3221223744 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6106 5559 603 41 0 6065 0
vsize: 24424
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 5821 0 0 0 11976 22 0 0 25 0 1 0 478962018 25808896 5748 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6301 5748 603 41 0 6260 0
vsize: 25204
[startup+130.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 6011 0 0 0 12976 23 0 0 25 0 1 0 478962018 26599424 5938 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6494 5938 603 41 0 6453 0
vsize: 25976
[startup+140.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 6204 0 0 0 13975 24 0 0 25 0 1 0 478962018 27389952 6131 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6687 6131 603 41 0 6646 0
vsize: 26748
[startup+150.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 6404 0 0 0 14974 25 0 0 25 0 1 0 478962018 28319744 6331 4294967295 134512640 134672761 3221224640 3221223784 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6914 6331 603 41 0 6873 0
vsize: 27656
[startup+160.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 6607 0 0 0 15973 26 0 0 25 0 1 0 478962018 29122560 6534 4294967295 134512640 134672761 3221224640 3221223744 134560335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7110 6534 603 41 0 7069 0
vsize: 28440
[startup+170.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 6798 0 0 0 16972 26 0 0 25 0 1 0 478962018 29917184 6725 4294967295 134512640 134672761 3221224640 3221223744 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7304 6725 603 41 0 7263 0
vsize: 29216
[startup+180.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7021 0 0 0 17971 28 0 0 25 0 1 0 478962018 30842880 6948 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7530 6948 603 41 0 7489 0
vsize: 30120
[startup+190.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7267 0 0 0 18971 29 0 0 25 0 1 0 478962018 31907840 7194 4294967295 134512640 134672761 3221224640 3221223824 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7790 7194 603 41 0 7749 0
vsize: 31160
[startup+200.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7445 0 0 0 19969 30 0 0 25 0 1 0 478962018 32567296 7372 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7951 7372 603 41 0 7910 0
vsize: 31804
[startup+210.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7571 0 0 0 20968 31 0 0 25 0 1 0 478962018 33095680 7498 4294967295 134512640 134672761 3221224640 3221223808 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8080 7498 603 41 0 8039 0
vsize: 32320
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 21968 31 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223744 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+230.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 22967 32 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223744 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+240.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 23967 32 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+250.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 24967 32 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+260.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 25966 33 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+270.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 26966 33 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+280.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 27966 34 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223808 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+290.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 28965 34 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+300.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 29965 35 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223764 134565998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 30964 35 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 31964 36 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 32964 36 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 33964 36 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223776 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 34964 37 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223744 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+360.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 35964 37 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223808 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+370.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 36964 37 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+380.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 37963 37 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223824 134558423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+390.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 38963 37 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223744 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+400.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25252
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 39963 38 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 40963 38 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223824 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+420.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 41964 38 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+430.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 42964 38 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+440.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 43964 38 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+450.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 44964 38 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 45964 38 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223744 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+470.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 46965 38 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223808 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+480.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 47965 38 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 48965 38 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7572 0 0 0 49965 38 0 0 25 0 1 0 478962018 33095680 7499 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8080 7499 603 41 0 8039 0
vsize: 32320
[startup+510.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7574 0 0 0 50965 38 0 0 25 0 1 0 478962018 33095680 7501 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8080 7501 603 41 0 8039 0
vsize: 32320
[startup+520.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7575 0 0 0 51966 38 0 0 25 0 1 0 478962018 33095680 7502 4294967295 134512640 134672761 3221224640 3221223824 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8080 7502 603 41 0 8039 0
vsize: 32320
[startup+530.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7585 0 0 0 52966 38 0 0 25 0 1 0 478962018 33247232 7512 4294967295 134512640 134672761 3221224640 3221223744 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8117 7512 603 41 0 8076 0
vsize: 32468
[startup+540.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7588 0 0 0 53966 38 0 0 25 0 1 0 478962018 33247232 7515 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8117 7515 603 41 0 8076 0
vsize: 32468
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7589 0 0 0 54966 38 0 0 25 0 1 0 478962018 33247232 7516 4294967295 134512640 134672761 3221224640 3221223808 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8117 7516 603 41 0 8076 0
vsize: 32468
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7597 0 0 0 55966 38 0 0 25 0 1 0 478962018 33247232 7524 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8117 7524 603 41 0 8076 0
vsize: 32468
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7598 0 0 0 56967 38 0 0 25 0 1 0 478962018 33247232 7525 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8117 7525 603 41 0 8076 0
vsize: 32468
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7598 0 0 0 57967 38 0 0 25 0 1 0 478962018 33247232 7525 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8117 7525 603 41 0 8076 0
vsize: 32468
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7598 0 0 0 58967 38 0 0 25 0 1 0 478962018 33247232 7525 4294967295 134512640 134672761 3221224640 3221223792 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8117 7525 603 41 0 8076 0
vsize: 32468
[startup+600.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7598 0 0 0 59967 38 0 0 25 0 1 0 478962018 33247232 7525 4294967295 134512640 134672761 3221224640 3221223808 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8117 7525 603 41 0 8076 0
vsize: 32468
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7598 0 0 0 60967 38 0 0 25 0 1 0 478962018 33247232 7525 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8117 7525 603 41 0 8076 0
vsize: 32468
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7598 0 0 0 61968 38 0 0 25 0 1 0 478962018 33247232 7525 4294967295 134512640 134672761 3221224640 3221223824 134559532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8117 7525 603 41 0 8076 0
vsize: 32468
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7598 0 0 0 62968 38 0 0 25 0 1 0 478962018 33247232 7525 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8117 7525 603 41 0 8076 0
vsize: 32468
[startup+640.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7598 0 0 0 63968 38 0 0 25 0 1 0 478962018 33247232 7525 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8117 7525 603 41 0 8076 0
vsize: 32468
[startup+650.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7598 0 0 0 64968 38 0 0 25 0 1 0 478962018 33247232 7525 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8117 7525 603 41 0 8076 0
vsize: 32468
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7598 0 0 0 65968 38 0 0 25 0 1 0 478962018 33247232 7525 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8117 7525 603 41 0 8076 0
vsize: 32468
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25254
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7607 0 0 0 66969 38 0 0 25 0 1 0 478962018 33247232 7534 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8117 7534 603 41 0 8076 0
vsize: 32468
[startup+680.023 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 25307
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7620 0 0 0 67967 39 0 0 25 0 1 0 478962018 33443840 7547 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8165 7547 603 41 0 8124 0
vsize: 32660
[startup+690.022 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 25307
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7641 0 0 0 68967 40 0 0 25 0 1 0 478962018 33443840 7568 4294967295 134512640 134672761 3221224640 3221223596 1075350544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8165 7568 603 41 0 8124 0
vsize: 32660
[startup+700.023 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 25307
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7655 0 0 0 69967 40 0 0 25 0 1 0 478962018 33640448 7582 4294967295 134512640 134672761 3221224640 3221223824 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8213 7582 603 41 0 8172 0
vsize: 32852
[startup+710.022 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 25309
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7655 0 0 0 70967 40 0 0 25 0 1 0 478962018 33640448 7582 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8213 7582 603 41 0 8172 0
vsize: 32852
[startup+720.023 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 25309
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7670 0 0 0 71967 40 0 0 25 0 1 0 478962018 33640448 7597 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8213 7597 603 41 0 8172 0
vsize: 32852
[startup+730.023 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 25309
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7709 0 0 0 72967 40 0 0 25 0 1 0 478962018 33837056 7636 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7636 603 41 0 8220 0
vsize: 33044
[startup+740.022 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 25309
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7710 0 0 0 73967 40 0 0 25 0 1 0 478962018 33837056 7637 4294967295 134512640 134672761 3221224640 3221223744 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7637 603 41 0 8220 0
vsize: 33044
[startup+750.022 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 25309
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7710 0 0 0 74968 40 0 0 25 0 1 0 478962018 33837056 7637 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7637 603 41 0 8220 0
vsize: 33044
[startup+760.022 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7710 0 0 0 75968 40 0 0 25 0 1 0 478962018 33837056 7637 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7637 603 41 0 8220 0
vsize: 33044
[startup+770.023 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7710 0 0 0 76968 40 0 0 25 0 1 0 478962018 33837056 7637 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7637 603 41 0 8220 0
vsize: 33044
[startup+780.023 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7710 0 0 0 77968 40 0 0 25 0 1 0 478962018 33837056 7637 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7637 603 41 0 8220 0
vsize: 33044
[startup+790.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7710 0 0 0 78968 40 0 0 25 0 1 0 478962018 33837056 7637 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7637 603 41 0 8220 0
vsize: 33044
[startup+800.023 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7710 0 0 0 79968 40 0 0 25 0 1 0 478962018 33837056 7637 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7637 603 41 0 8220 0
vsize: 33044
[startup+810.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7710 0 0 0 80968 40 0 0 25 0 1 0 478962018 33837056 7637 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7637 603 41 0 8220 0
vsize: 33044
[startup+820.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7710 0 0 0 81969 40 0 0 25 0 1 0 478962018 33837056 7637 4294967295 134512640 134672761 3221224640 3221223808 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7637 603 41 0 8220 0
vsize: 33044
[startup+830.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7710 0 0 0 82969 40 0 0 25 0 1 0 478962018 33837056 7637 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7637 603 41 0 8220 0
vsize: 33044
[startup+840.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7710 0 0 0 83969 40 0 0 25 0 1 0 478962018 33837056 7637 4294967295 134512640 134672761 3221224640 3221223824 134558557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7637 603 41 0 8220 0
vsize: 33044
[startup+850.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7710 0 0 0 84969 40 0 0 25 0 1 0 478962018 33837056 7637 4294967295 134512640 134672761 3221224640 3221223744 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7637 603 41 0 8220 0
vsize: 33044
[startup+860.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7710 0 0 0 85969 40 0 0 25 0 1 0 478962018 33837056 7637 4294967295 134512640 134672761 3221224640 3221223808 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7637 603 41 0 8220 0
vsize: 33044
[startup+870.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7710 0 0 0 86969 40 0 0 25 0 1 0 478962018 33837056 7637 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7637 603 41 0 8220 0
vsize: 33044
[startup+880.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7715 0 0 0 87970 40 0 0 25 0 1 0 478962018 34000896 7642 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8301 7642 603 41 0 8260 0
vsize: 33204
[startup+890.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7720 0 0 0 88970 40 0 0 25 0 1 0 478962018 34000896 7647 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8301 7647 603 41 0 8260 0
vsize: 33204
[startup+900.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7726 0 0 0 89970 40 0 0 25 0 1 0 478962018 34000896 7653 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8301 7653 603 41 0 8260 0
vsize: 33204
[startup+910.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7726 0 0 0 90970 40 0 0 25 0 1 0 478962018 34000896 7653 4294967295 134512640 134672761 3221224640 3221223840 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8301 7653 603 41 0 8260 0
vsize: 33204
[startup+920.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7726 0 0 0 91971 40 0 0 25 0 1 0 478962018 34000896 7653 4294967295 134512640 134672761 3221224640 3221223808 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8301 7653 603 41 0 8260 0
vsize: 33204
[startup+930.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7726 0 0 0 92971 40 0 0 25 0 1 0 478962018 34000896 7653 4294967295 134512640 134672761 3221224640 3221223744 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8301 7653 603 41 0 8260 0
vsize: 33204
[startup+940.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7726 0 0 0 93971 40 0 0 25 0 1 0 478962018 34000896 7653 4294967295 134512640 134672761 3221224640 3221223744 134559979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8301 7653 603 41 0 8260 0
vsize: 33204
[startup+950.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7731 0 0 0 94971 40 0 0 25 0 1 0 478962018 34000896 7658 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8301 7658 603 41 0 8260 0
vsize: 33204
[startup+960.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7731 0 0 0 95971 40 0 0 25 0 1 0 478962018 34000896 7658 4294967295 134512640 134672761 3221224640 3221223808 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8301 7658 603 41 0 8260 0
vsize: 33204
[startup+970.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7731 0 0 0 96971 40 0 0 25 0 1 0 478962018 34000896 7658 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8301 7658 603 41 0 8260 0
vsize: 33204
[startup+980.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7731 0 0 0 97972 40 0 0 25 0 1 0 478962018 34000896 7658 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8301 7658 603 41 0 8260 0
vsize: 33204
[startup+990.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7741 0 0 0 98972 40 0 0 25 0 1 0 478962018 34164736 7668 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7668 603 41 0 8300 0
vsize: 33364
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25311
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7741 0 0 0 99972 40 0 0 25 0 1 0 478962018 34164736 7668 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7668 603 41 0 8300 0
vsize: 33364
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25313
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7748 0 0 0 100972 40 0 0 25 0 1 0 478962018 34164736 7675 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7675 603 41 0 8300 0
vsize: 33364
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25315
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7755 0 0 0 101972 40 0 0 25 0 1 0 478962018 34164736 7682 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7682 603 41 0 8300 0
vsize: 33364
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25315
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7755 0 0 0 102972 40 0 0 25 0 1 0 478962018 34164736 7682 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7682 603 41 0 8300 0
vsize: 33364
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25315
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7755 0 0 0 103972 40 0 0 25 0 1 0 478962018 34164736 7682 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7682 603 41 0 8300 0
vsize: 33364
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25315
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7755 0 0 0 104973 40 0 0 25 0 1 0 478962018 34164736 7682 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7682 603 41 0 8300 0
vsize: 33364
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25315
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7755 0 0 0 105973 40 0 0 25 0 1 0 478962018 34164736 7682 4294967295 134512640 134672761 3221224640 3221223744 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7682 603 41 0 8300 0
vsize: 33364
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25315
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7755 0 0 0 106973 40 0 0 25 0 1 0 478962018 34164736 7682 4294967295 134512640 134672761 3221224640 3221223824 134558690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7682 603 41 0 8300 0
vsize: 33364
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25315
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7755 0 0 0 107973 40 0 0 25 0 1 0 478962018 34164736 7682 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7682 603 41 0 8300 0
vsize: 33364
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25315
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7755 0 0 0 108973 40 0 0 25 0 1 0 478962018 34164736 7682 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7682 603 41 0 8300 0
vsize: 33364
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25315
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7755 0 0 0 109974 40 0 0 25 0 1 0 478962018 34164736 7682 4294967295 134512640 134672761 3221224640 3221223824 134559381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7682 603 41 0 8300 0
vsize: 33364
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25315
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7755 0 0 0 110974 40 0 0 25 0 1 0 478962018 34164736 7682 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7682 603 41 0 8300 0
vsize: 33364
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25315
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7755 0 0 0 111974 40 0 0 25 0 1 0 478962018 34164736 7682 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7682 603 41 0 8300 0
vsize: 33364
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25315
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7755 0 0 0 112974 40 0 0 25 0 1 0 478962018 34164736 7682 4294967295 134512640 134672761 3221224640 3221223744 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7682 603 41 0 8300 0
vsize: 33364
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25315
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7755 0 0 0 113974 40 0 0 25 0 1 0 478962018 34164736 7682 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7682 603 41 0 8300 0
vsize: 33364
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25315
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7755 0 0 0 114975 40 0 0 25 0 1 0 478962018 34164736 7682 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7682 603 41 0 8300 0
vsize: 33364
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25315
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7755 0 0 0 115975 40 0 0 25 0 1 0 478962018 34164736 7682 4294967295 134512640 134672761 3221224640 3221223824 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7682 603 41 0 8300 0
vsize: 33364
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25315
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7755 0 0 0 116975 40 0 0 25 0 1 0 478962018 34164736 7682 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7682 603 41 0 8300 0
vsize: 33364
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25315
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7755 0 0 0 117975 40 0 0 25 0 1 0 478962018 34164736 7682 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7682 603 41 0 8300 0
vsize: 33364
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25315
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7758 0 0 0 118975 40 0 0 25 0 1 0 478962018 34164736 7685 4294967295 134512640 134672761 3221224640 3221223824 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7685 603 41 0 8300 0
vsize: 33364
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25315
Raw data (stat): 25250 (minisat+) R 25249 20838 20837 0 -1 0 7758 0 0 0 119976 40 0 0 25 0 1 0 478962018 34164736 7685 4294967295 134512640 134672761 3221224640 3221223744 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7685 603 41 0 8300 0
vsize: 33364
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 1/55 25315
Raw data (stat): 25250 (minisat+) Z 25249 20838 20837 0 -1 12 7761 0 0 0 119976 42 0 0 25 0 1 0 478962018 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.04
CPU time (s): 1200.19
CPU user time (s): 1199.76
CPU system time (s): 0.424935
CPU usage (%): 100.012
Max. virtual memory (Kb): 33364
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####