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/synthesis-ptl-cmos-circuits/normalized-cmb.opb
MD5SUM	a8596c98551f801a6658f1ce91b33278
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1053
Optimality of the best value was proved	NO
Number of terms in the objective function	304
Biggest coefficient in the objective function	61
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	12887
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	12887
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.97785
Number of variables	304
Total number of constraints	671
Number of constraints which are clauses	671
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	1
Maximum length of a constraint	28
Trace number 6343

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-14 04:22:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4765 boxname=wulflinc23 idbench=253 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a8596c98551f801a6658f1ce91b33278  /oldhome/oroussel/tmp/wulflinc23/normalized-cmb.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc23/normalized-cmb.opb /oldhome/oroussel/tmp/wulflinc23/normalized-cmb.opb
IDLAUNCH: 4765
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 3
cpu MHz		: 451.037
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:        888988 kB
Buffers:         35056 kB
Cached:          67704 kB
SwapCached:        192 kB
Active:          53392 kB
Inactive:        52440 kB
HighTotal:      131008 kB
HighFree:        59472 kB
LowTotal:       903652 kB
LowFree:        829516 kB
SwapTotal:     2097136 kB
SwapFree:      2096944 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6908 kB
Slab:            34196 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:42:52 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 4765 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 667 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 |     667     3359 |     222       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 1524[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:43621     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  119231   280847 |   39743       0        0     nan |  0.000 % |
c |       100 |  118633   279488 |   43717      84      671     8.0 |  0.378 % |
c |       250 |  118633   279488 |   48089     234     1730     7.4 |  0.378 % |
c |       478 |  118633   279488 |   52897     462    15468    33.5 |  0.378 % |
c |       816 |  117902   277810 |   58187     784    23004    29.3 |  0.883 % |
c |      1323 |  117671   277277 |   64006    1290    42043    32.6 |  1.040 % |
c |      2082 |  117636   277199 |   70407    2048    73688    36.0 |  1.063 % |
c |      3223 |  117040   275814 |   77447    3175   101231    31.9 |  1.525 % |
c |      4931 |  117040   275814 |   85192    4883   211348    43.3 |  1.525 % |
c |      7493 |  116887   275465 |   93711    7438   367463    49.4 |  1.639 % |
c |     11337 |  116873   275433 |  103083   11280   725661    64.3 |  1.649 % |
c ==============================================================================
c [1mFound solution: 1305[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:36083     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11381 |  212844   500208 |   70948   11324   726473    64.2 |  1.649 % |
c |     11482 |  212844   500208 |   78042   11425   729153    63.8 |  0.935 % |
c |     11632 |  212844   500208 |   85847   11575   742169    64.1 |  0.935 % |
c |     11857 |  212628   499712 |   94431   11783   758055    64.3 |  1.020 % |
c |     12194 |  212628   499712 |  103874   12120   763085    63.0 |  1.020 % |
c |     12701 |  212506   499438 |  114262   12620   766405    60.7 |  1.066 % |
c |     13461 |  212506   499438 |  125688   13380   775322    57.9 |  1.066 % |
c |     14600 |  212415   499230 |  138257   14480   866276    59.8 |  1.103 % |
c |     16310 |  212303   498977 |  152083   16186   920502    56.9 |  1.142 % |
c |     18872 |  212256   498872 |  167291   18738  1029983    55.0 |  1.159 % |
c ==============================================================================
c [1mFound solution: 1297[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22122 |  212419   499354 |   70806   21987  1255633    57.1 |  1.159 % |
c |     22224 |  212419   499354 |   77886   22089  1261322    57.1 |  1.162 % |
c |     22374 |  212406   499324 |   85675   22222  1262491    56.8 |  1.168 % |
c |     22599 |  212406   499324 |   94242   22447  1263775    56.3 |  1.168 % |
c |     22937 |  212395   499300 |  103667   22784  1271907    55.8 |  1.172 % |
c |     23443 |  212395   499300 |  114033   23290  1397817    60.0 |  1.172 % |
c |     24205 |  212395   499300 |  125437   24052  1461396    60.8 |  1.172 % |
c |     25344 |  212369   499244 |  137980   25188  1500891    59.6 |  1.180 % |
c |     27052 |  212369   499244 |  151778   26896  1539827    57.3 |  1.180 % |
c |     29615 |  212314   499118 |  166956   29458  1770393    60.1 |  1.203 % |
c |     33460 |  212157   498763 |  183652   33268  1874894    56.4 |  1.261 % |
c ==============================================================================
c [1mFound solution: 1261[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33525 |  213689   502481 |   71229   33333  1877300    56.3 |  1.261 % |
c ==============================================================================
c [1mFound solution: 1256[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33547 |  213771   502721 |   71257   33355  1881778    56.4 |  1.261 % |
c |     33647 |  213771   502721 |   78382   33455  1893442    56.6 |  1.264 % |
c |     33799 |  213771   502721 |   86220   33607  1899371    56.5 |  1.264 % |
c |     34024 |  213771   502721 |   94843   33832  1903728    56.3 |  1.264 % |
c |     34361 |  213771   502721 |  104327   34169  1908706    55.9 |  1.264 % |
c |     34867 |  213771   502721 |  114760   34675  1912878    55.2 |  1.264 % |
c |     35626 |  213748   502672 |  126236   35420  1957518    55.3 |  1.269 % |
c |     36765 |  213748   502672 |  138859   36559  1973244    54.0 |  1.269 % |
c |     38474 |  213719   502606 |  152745   38267  1998864    52.2 |  1.279 % |
c |     41038 |  213719   502606 |  168020   40831  2040808    50.0 |  1.279 % |
c ==============================================================================
c [1mFound solution: 1232[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42892 |  213833   502924 |   71277   42685  2091251    49.0 |  1.279 % |
c |     42993 |  213833   502924 |   78404   42786  2103442    49.2 |  1.280 % |
c |     43144 |  213833   502924 |   86245   42937  2106685    49.1 |  1.280 % |
c |     43371 |  213833   502924 |   94869   43164  2111327    48.9 |  1.280 % |
c |     43708 |  213833   502924 |  104356   43501  2125598    48.9 |  1.280 % |
c |     44214 |  213833   502924 |  114792   44007  2133045    48.5 |  1.280 % |
c |     44973 |  213833   502924 |  126271   44766  2208087    49.3 |  1.280 % |
c |     46114 |  213833   502924 |  138898   45907  2308775    50.3 |  1.280 % |
c |     47822 |  213833   502924 |  152788   47615  2378467    50.0 |  1.280 % |
c |     50386 |  213833   502924 |  168067   50179  2733829    54.5 |  1.280 % |
c |     54230 |  213833   502924 |  184874   54023  3035701    56.2 |  1.280 % |
c |     59998 |  213805   502861 |  203361   59789  3824419    64.0 |  1.290 % |
c |     68647 |  213805   502861 |  223697   68438  5501056    80.4 |  1.290 % |
c |     81621 |  213805   502861 |  246067   81412  6728206    82.6 |  1.290 % |
c ==============================================================================
c [1mFound solution: 1230[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88398 |  213821   502901 |   71273   88189  7416626    84.1 |  1.290 % |
c |     88498 |  213821   502901 |   78400   22865  1309769    57.3 |  1.291 % |
c |     88649 |  213821   502901 |   86240   23016  1315092    57.1 |  1.291 % |
c |     88874 |  213799   502850 |   94864   23240  1316615    56.7 |  1.300 % |
c |     89211 |  213799   502850 |  104350   23577  1328936    56.4 |  1.300 % |
c |     89719 |  213799   502850 |  114785   24085  1343323    55.8 |  1.300 % |
c |     90479 |  213799   502850 |  126264   24845  1369250    55.1 |  1.300 % |
c |     91622 |  213799   502850 |  138890   25988  1410511    54.3 |  1.300 % |
c |     93332 |  213799   502850 |  152780   27698  1536124    55.5 |  1.300 % |
c |     95894 |  213799   502850 |  168058   30260  1631376    53.9 |  1.300 % |
c |     99738 |  213799   502850 |  184863   34104  1787531    52.4 |  1.300 % |
c |    105507 |  213633   502479 |  203350   39848  2527811    63.4 |  1.359 % |
#### 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.91 0.96 0.92 2/54 8488
Raw data (stat): 8488 (runsolver) R 8487 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481677715 1052672 99 4294967295 134512640 135381576 3221224480 3221219724 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.93 0.96 0.92 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 3798 0 0 0 988 9 0 0 25 0 1 0 481677715 18046976 3596 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4406 3596 603 41 0 4365 0
vsize: 17624
[startup+20.0004 s]
Raw data (loadavg): 0.94 0.96 0.92 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 3869 0 0 0 1987 10 0 0 25 0 1 0 481677715 18317312 3667 4294967295 134512640 134672761 3221224576 3221223712 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4472 3667 603 41 0 4431 0
vsize: 17888
[startup+30.0013 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 3970 0 0 0 2987 11 0 0 25 0 1 0 481677715 18718720 3768 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4570 3768 603 41 0 4529 0
vsize: 18280
[startup+40.001 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 4125 0 0 0 3986 12 0 0 25 0 1 0 481677715 19390464 3923 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4734 3923 603 41 0 4693 0
vsize: 18936
[startup+50.0013 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 4328 0 0 0 4986 12 0 0 25 0 1 0 481677715 20324352 4126 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4962 4126 603 41 0 4921 0
vsize: 19848
[startup+60.0013 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 4545 0 0 0 5986 13 0 0 25 0 1 0 481677715 21118976 4343 4294967295 134512640 134672761 3221224576 3221223720 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5156 4343 603 41 0 5115 0
vsize: 20624
[startup+70.0009 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 7076 0 0 0 6979 19 0 0 25 0 1 0 481677715 34172928 6832 4294967295 134512640 134672761 3221224576 3221223744 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8343 6832 603 41 0 8302 0
vsize: 33372
[startup+80.0013 s]
Raw data (loadavg): 1.06 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 7191 0 0 0 7979 19 0 0 25 0 1 0 481677715 34578432 6947 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8442 6947 603 41 0 8401 0
vsize: 33768
[startup+90.0012 s]
Raw data (loadavg): 1.05 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 7230 0 0 0 8979 20 0 0 25 0 1 0 481677715 34713600 6986 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8475 6986 603 41 0 8434 0
vsize: 33900
[startup+100.002 s]
Raw data (loadavg): 1.04 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 7312 0 0 0 9979 20 0 0 25 0 1 0 481677715 35213312 7068 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8597 7068 603 41 0 8556 0
vsize: 34388
[startup+110.002 s]
Raw data (loadavg): 1.03 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 7338 0 0 0 10979 20 0 0 25 0 1 0 481677715 35213312 7094 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8597 7094 603 41 0 8556 0
vsize: 34388
[startup+120.002 s]
Raw data (loadavg): 1.03 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 7368 0 0 0 11979 20 0 0 25 0 1 0 481677715 35348480 7124 4294967295 134512640 134672761 3221224576 3221223712 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 7124 603 41 0 8589 0
vsize: 34520
[startup+130.003 s]
Raw data (loadavg): 1.02 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 7504 0 0 0 12979 20 0 0 25 0 1 0 481677715 36012032 7260 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8792 7260 603 41 0 8751 0
vsize: 35168
[startup+140.002 s]
Raw data (loadavg): 1.02 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 7561 0 0 0 13979 20 0 0 25 0 1 0 481677715 36143104 7317 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8824 7317 603 41 0 8783 0
vsize: 35296
[startup+150.002 s]
Raw data (loadavg): 1.02 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 7610 0 0 0 14979 20 0 0 25 0 1 0 481677715 36413440 7366 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8890 7366 603 41 0 8849 0
vsize: 35560
[startup+160.003 s]
Raw data (loadavg): 1.01 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 7802 0 0 0 15978 21 0 0 25 0 1 0 481677715 37011456 7516 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9036 7516 603 41 0 8995 0
vsize: 36144
[startup+170.002 s]
Raw data (loadavg): 1.01 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 7939 0 0 0 16977 22 0 0 25 0 1 0 481677715 37539840 7653 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9165 7653 603 41 0 9124 0
vsize: 36660
[startup+180.003 s]
Raw data (loadavg): 1.01 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 7973 0 0 0 17978 23 0 0 25 0 1 0 481677715 37670912 7687 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9197 7687 603 41 0 9156 0
vsize: 36788
[startup+190.004 s]
Raw data (loadavg): 1.01 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 8030 0 0 0 18977 23 0 0 25 0 1 0 481677715 37941248 7744 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9263 7744 603 41 0 9222 0
vsize: 37052
[startup+200.003 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 8088 0 0 0 19977 23 0 0 25 0 1 0 481677715 38076416 7802 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9296 7802 603 41 0 9255 0
vsize: 37184
[startup+210.004 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 8171 0 0 0 20977 24 0 0 25 0 1 0 481677715 38469632 7885 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9392 7885 603 41 0 9351 0
vsize: 37568
[startup+220.004 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 8234 0 0 0 21977 24 0 0 25 0 1 0 481677715 38735872 7948 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9457 7948 603 41 0 9416 0
vsize: 37828
[startup+230.004 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 8328 0 0 0 22976 25 0 0 25 0 1 0 481677715 39137280 8042 4294967295 134512640 134672761 3221224576 3221223736 134561029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9555 8042 603 41 0 9514 0
vsize: 38220
[startup+240.005 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 8396 0 0 0 23975 25 0 0 25 0 1 0 481677715 39403520 8110 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9620 8110 603 41 0 9579 0
vsize: 38480
[startup+250.004 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 8459 0 0 0 24975 26 0 0 25 0 1 0 481677715 39800832 8173 4294967295 134512640 134672761 3221224576 3221223744 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9717 8173 603 41 0 9676 0
vsize: 38868
[startup+260.005 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 8638 0 0 0 25975 26 0 0 25 0 1 0 481677715 39878656 8219 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9736 8219 603 41 0 9695 0
vsize: 38944
[startup+270.005 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 8701 0 0 0 26974 26 0 0 25 0 1 0 481677715 40144896 8282 4294967295 134512640 134672761 3221224576 3221223712 134560645 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9801 8282 603 41 0 9760 0
vsize: 39204
[startup+280.005 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 8774 0 0 0 27974 27 0 0 25 0 1 0 481677715 40415232 8355 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9867 8355 603 41 0 9826 0
vsize: 39468
[startup+290.005 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 8825 0 0 0 28974 27 0 0 25 0 1 0 481677715 40685568 8406 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9933 8406 603 41 0 9892 0
vsize: 39732
[startup+300.005 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 8846 0 0 0 29975 27 0 0 25 0 1 0 481677715 40820736 8427 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9966 8427 603 41 0 9925 0
vsize: 39864
[startup+310.005 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 8865 0 0 0 30975 27 0 0 25 0 1 0 481677715 40820736 8446 4294967295 134512640 134672761 3221224576 3221223532 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9966 8446 603 41 0 9925 0
vsize: 39864
[startup+320.005 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 8882 0 0 0 31975 27 0 0 25 0 1 0 481677715 40955904 8463 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9999 8463 603 41 0 9958 0
vsize: 39996
[startup+330.005 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 9002 0 0 0 32974 27 0 0 25 0 1 0 481677715 41160704 8541 4294967295 134512640 134672761 3221224576 3221223760 134559417 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10049 8541 603 41 0 10008 0
vsize: 40196
[startup+340.005 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 9009 0 0 0 33975 27 0 0 25 0 1 0 481677715 41295872 8548 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10082 8548 603 41 0 10041 0
vsize: 40328
[startup+350.005 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 9087 0 0 0 34974 28 0 0 25 0 1 0 481677715 41562112 8626 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10147 8626 603 41 0 10106 0
vsize: 40588
[startup+360.005 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 9139 0 0 0 35975 28 0 0 25 0 1 0 481677715 41832448 8678 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10213 8678 603 41 0 10172 0
vsize: 40852
[startup+370.005 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 9193 0 0 0 36975 28 0 0 25 0 1 0 481677715 41967616 8732 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10246 8732 603 41 0 10205 0
vsize: 40984
[startup+380.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 9247 0 0 0 37975 28 0 0 25 0 1 0 481677715 42233856 8786 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10311 8786 603 41 0 10270 0
vsize: 41244
[startup+390.005 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 9320 0 0 0 38975 28 0 0 25 0 1 0 481677715 42504192 8859 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10377 8859 603 41 0 10336 0
vsize: 41508
[startup+400.005 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 9481 0 0 0 39975 29 0 0 25 0 1 0 481677715 43102208 9020 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10523 9020 603 41 0 10482 0
vsize: 42092
[startup+410.005 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 9639 0 0 0 40974 30 0 0 25 0 1 0 481677715 43761664 9178 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10684 9178 603 41 0 10643 0
vsize: 42736
[startup+420.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 9703 0 0 0 41974 30 0 0 25 0 1 0 481677715 44027904 9242 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10749 9242 603 41 0 10708 0
vsize: 42996
[startup+430.007 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 9758 0 0 0 42974 30 0 0 25 0 1 0 481677715 44298240 9297 4294967295 134512640 134672761 3221224576 3221223712 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10815 9297 603 41 0 10774 0
vsize: 43260
[startup+440.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 9844 0 0 0 43974 30 0 0 25 0 1 0 481677715 44564480 9383 4294967295 134512640 134672761 3221224576 3221223712 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10880 9383 603 41 0 10839 0
vsize: 43520
[startup+450.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 9879 0 0 0 44974 30 0 0 25 0 1 0 481677715 44699648 9418 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10913 9418 603 41 0 10872 0
vsize: 43652
[startup+460.007 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 9963 0 0 0 45974 30 0 0 25 0 1 0 481677715 45101056 9502 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11011 9502 603 41 0 10970 0
vsize: 44044
[startup+470.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 10020 0 0 0 46974 31 0 0 25 0 1 0 481677715 45367296 9559 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11076 9559 603 41 0 11035 0
vsize: 44304
[startup+480.007 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 10051 0 0 0 47974 31 0 0 25 0 1 0 481677715 45502464 9590 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11109 9590 603 41 0 11068 0
vsize: 44436
[startup+490.007 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 10092 0 0 0 48974 31 0 0 25 0 1 0 481677715 45633536 9631 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11141 9631 603 41 0 11100 0
vsize: 44564
[startup+500.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 10130 0 0 0 49974 31 0 0 25 0 1 0 481677715 45768704 9669 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11174 9669 603 41 0 11133 0
vsize: 44696
[startup+510.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 10198 0 0 0 50974 31 0 0 25 0 1 0 481677715 46039040 9737 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11240 9737 603 41 0 11199 0
vsize: 44960
[startup+520.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 10347 0 0 0 51973 32 0 0 25 0 1 0 481677715 46698496 9886 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11401 9886 603 41 0 11360 0
vsize: 45604
[startup+530.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 10466 0 0 0 52973 33 0 0 25 0 1 0 481677715 47099904 10005 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11499 10005 603 41 0 11458 0
vsize: 45996
[startup+540.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 10610 0 0 0 53973 33 0 0 25 0 1 0 481677715 47759360 10149 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11660 10149 603 41 0 11619 0
vsize: 46640
[startup+550.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 10766 0 0 0 54972 34 0 0 25 0 1 0 481677715 48414720 10305 4294967295 134512640 134672761 3221224576 3221223712 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11820 10305 603 41 0 11779 0
vsize: 47280
[startup+560.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 10860 0 0 0 55972 35 0 0 25 0 1 0 481677715 48803840 10399 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11915 10399 603 41 0 11874 0
vsize: 47660
[startup+570.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 10949 0 0 0 56971 35 0 0 25 0 1 0 481677715 49074176 10488 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11981 10488 603 41 0 11940 0
vsize: 47924
[startup+580.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 11117 0 0 0 57971 35 0 0 25 0 1 0 481677715 49741824 10656 4294967295 134512640 134672761 3221224576 3221223728 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12144 10656 603 41 0 12103 0
vsize: 48576
[startup+590.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 11270 0 0 0 58971 36 0 0 25 0 1 0 481677715 50405376 10809 4294967295 134512640 134672761 3221224576 3221223680 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12306 10809 603 41 0 12265 0
vsize: 49224
[startup+600.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 11451 0 0 0 59970 37 0 0 25 0 1 0 481677715 51212288 10990 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12503 10990 603 41 0 12462 0
vsize: 50012
[startup+610.007 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 11629 0 0 0 60970 37 0 0 25 0 1 0 481677715 51875840 11168 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12665 11168 603 41 0 12624 0
vsize: 50660
[startup+620.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 11850 0 0 0 61969 38 0 0 25 0 1 0 481677715 53080064 11389 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12959 11389 603 41 0 12918 0
vsize: 51836
[startup+630.007 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 12041 0 0 0 62969 38 0 0 25 0 1 0 481677715 53886976 11580 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13156 11580 603 41 0 13115 0
vsize: 52624
[startup+640.007 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 12261 0 0 0 63968 39 0 0 25 0 1 0 481677715 54689792 11800 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13352 11800 603 41 0 13311 0
vsize: 53408
[startup+650.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 12486 0 0 0 64968 40 0 0 25 0 1 0 481677715 55635968 12025 4294967295 134512640 134672761 3221224576 3221223716 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13583 12025 603 41 0 13542 0
vsize: 54332
[startup+660.007 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 12598 0 0 0 65968 40 0 0 25 0 1 0 481677715 56029184 12137 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13679 12137 603 41 0 13638 0
vsize: 54716
[startup+670.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 12713 0 0 0 66967 41 0 0 25 0 1 0 481677715 56553472 12252 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13807 12252 603 41 0 13766 0
vsize: 55228
[startup+680.007 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 12799 0 0 0 67967 41 0 0 25 0 1 0 481677715 56958976 12338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13906 12338 603 41 0 13865 0
vsize: 55624
[startup+690.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 12881 0 0 0 68967 42 0 0 25 0 1 0 481677715 57229312 12420 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13972 12420 603 41 0 13931 0
vsize: 55888
[startup+700.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 12952 0 0 0 69967 42 0 0 25 0 1 0 481677715 57495552 12491 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14037 12491 603 41 0 13996 0
vsize: 56148
[startup+710.007 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 13033 0 0 0 70966 43 0 0 25 0 1 0 481677715 57888768 12572 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14133 12572 603 41 0 14092 0
vsize: 56532
[startup+720.007 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 13124 0 0 0 71966 43 0 0 25 0 1 0 481677715 58273792 12663 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14227 12663 603 41 0 14186 0
vsize: 56908
[startup+730.007 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 13224 0 0 0 72966 43 0 0 25 0 1 0 481677715 58667008 12763 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14323 12763 603 41 0 14282 0
vsize: 57292
[startup+740.007 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 13303 0 0 0 73966 44 0 0 25 0 1 0 481677715 58929152 12842 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14387 12842 603 41 0 14346 0
vsize: 57548
[startup+750.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 13368 0 0 0 74966 44 0 0 25 0 1 0 481677715 59191296 12907 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14451 12907 603 41 0 14410 0
vsize: 57804
[startup+760.006 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 13459 0 0 0 75966 44 0 0 25 0 1 0 481677715 59596800 12998 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14550 12998 603 41 0 14509 0
vsize: 58200
[startup+770.007 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 13549 0 0 0 76965 45 0 0 25 0 1 0 481677715 59990016 13088 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14646 13090 603 41 0 14605 0
vsize: 58584
[startup+780.008 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 13643 0 0 0 77965 45 0 0 25 0 1 0 481677715 60395520 13182 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14745 13182 603 41 0 14704 0
vsize: 58980
[startup+790.007 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 13760 0 0 0 78965 45 0 0 25 0 1 0 481677715 60796928 13299 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14843 13299 603 41 0 14802 0
vsize: 59372
[startup+800.007 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 13901 0 0 0 79965 46 0 0 25 0 1 0 481677715 61329408 13440 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14973 13440 603 41 0 14932 0
vsize: 59892
[startup+810.007 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 13976 0 0 0 80964 46 0 0 25 0 1 0 481677715 61730816 13515 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15071 13515 603 41 0 15030 0
vsize: 60284
[startup+820.007 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14071 0 0 0 81964 46 0 0 25 0 1 0 481677715 62132224 13610 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15169 13610 603 41 0 15128 0
vsize: 60676
[startup+830.008 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14183 0 0 0 82964 47 0 0 25 0 1 0 481677715 62529536 13722 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15266 13722 603 41 0 15225 0
vsize: 61064
[startup+840.008 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14300 0 0 0 83964 47 0 0 25 0 1 0 481677715 63062016 13839 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15396 13839 603 41 0 15355 0
vsize: 61584
[startup+850.008 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14368 0 0 0 84964 47 0 0 25 0 1 0 481677715 63332352 13907 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15462 13907 603 41 0 15421 0
vsize: 61848
[startup+860.009 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14439 0 0 0 85964 47 0 0 25 0 1 0 481677715 63598592 13978 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15527 13978 603 41 0 15486 0
vsize: 62108
[startup+870.009 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14521 0 0 0 86964 48 0 0 25 0 1 0 481677715 63868928 14060 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15593 14060 603 41 0 15552 0
vsize: 62372
[startup+880.009 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 87964 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223232 134565745 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+890.009 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 88964 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+900.008 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 89964 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+910.009 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 90964 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+920.009 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 91964 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223712 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+930.009 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 92964 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+940.009 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 93965 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+950.009 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 94965 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+960.009 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 95965 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+970.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 96965 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+980.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 97966 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223776 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+990.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 98966 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 99966 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 100966 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 101966 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 102966 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 103966 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 104967 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 105967 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 106967 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 107967 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 108967 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 109968 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 110968 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 111968 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 112968 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 113968 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 114969 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 115969 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 116969 48 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 117969 49 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 118969 49 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8488
Raw data (stat): 8488 (minisat+) R 8487 3260 3259 0 -1 0 14757 0 0 0 119969 49 0 0 25 0 1 0 481677715 64495616 14223 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 14223 603 41 0 15705 0
vsize: 62984
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.98 0.93 1/54 8488
Raw data (stat): 8488 (minisat+) Z 8487 3260 3259 0 -1 12 14760 0 0 0 119969 51 0 0 25 0 1 0 481677715 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.04
CPU time (s): 1200.22
CPU user time (s): 1199.7
CPU system time (s): 0.51992
CPU usage (%): 100.015
Max. virtual memory (Kb): 62984
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####