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-C432.opb
MD5SUM	6292e63147fb202dc159fbf5a9ff5c77
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4822
Optimality of the best value was proved	NO
Number of terms in the objective function	771
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	33355
Number of bits of the sum of numbers in the objective function	16
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	33355
Number of bits of the biggest sum of numbers	16
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02584
Number of variables	771
Total number of constraints	1951
Number of constraints which are clauses	1949
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	2
Minimum length of a constraint	1
Maximum length of a constraint	42
Trace number 30472

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-05-25 16:53:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=21830 boxname=wulflinc5 idbench=248 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  6292e63147fb202dc159fbf5a9ff5c77  /oldhome/oroussel/tmp/wulflinc5/normalized-C432.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-C432.opb
IDLAUNCH: 21830
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        699356 kB
Buffers:         33948 kB
Cached:         280556 kB
SwapCached:        472 kB
Active:          77416 kB
Inactive:       239192 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        699104 kB
SwapTotal:     2097136 kB
SwapFree:      2095792 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5228 kB
Slab:            13088 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 17:14:22 (client local time) WITH STATUS 152 IN 1229.89 SECONDS
stats: 21830 7 1229.89 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1905 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 |    1905     9279 |     635       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 7184[0m
c ---[   0]---> Sorter-cost:125007     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  296867   697871 |   98955       0        0     nan |  0.000 % |
c |       100 |  295982   695900 |  108850      91     3014    33.1 |  0.231 % |
c |       250 |  295982   695900 |  119735     241     3707    15.4 |  0.231 % |
c |       475 |  295982   695900 |  131709     466    10278    22.1 |  0.231 % |
c |       812 |  294997   693680 |  144880     789    11854    15.0 |  0.481 % |
c |      1320 |  294829   693311 |  159368    1295    20055    15.5 |  0.530 % |
c |      2079 |  294759   693152 |  175304    2050    88175    43.0 |  0.557 % |
c |      3218 |  294736   693103 |  192835    3187   108254    34.0 |  0.568 % |
c |      4926 |  294736   693103 |  212118    4895   153808    31.4 |  0.568 % |
c |      7488 |  294736   693103 |  233330    7457   270645    36.3 |  0.568 % |
c |     11333 |  294418   692379 |  256663   11299   313690    27.8 |  0.658 % |
c |     17100 |  294416   692375 |  282330   17065   662123    38.8 |  0.658 % |
c |     25751 |  294416   692375 |  310563   25716   813498    31.6 |  0.658 % |
c |     38728 |  294416   692375 |  341619   38693  1063269    27.5 |  0.658 % |
c |     58190 |  294408   692357 |  375781   58154  2180279    37.5 |  0.660 % |
c |     87382 |  294408   692357 |  413359   87346  7615229    87.2 |  0.660 % |
c ==============================================================================
c [1mFound solution: 7183[0m
c ---[   0]---> Sorter-cost:113803     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     94656 |  559505  1311181 |  186501   94615  7988355    84.4 |  0.660 % |
c |     94756 |  559505  1311181 |  205151   94715  7989688    84.4 |  0.371 % |
c |     94908 |  559505  1311181 |  225666   94867  7991107    84.2 |  0.371 % |
c |     95133 |  559505  1311181 |  248232   95092  7992665    84.1 |  0.371 % |
c |     95471 |  559505  1311181 |  273056   95430  7995137    83.8 |  0.371 % |
c |     95977 |  559505  1311181 |  300361   95936  8001388    83.4 |  0.371 % |
c |     96737 |  559283  1310683 |  330397   96692  8017970    82.9 |  0.399 % |
c |     97876 |  559283  1310683 |  363437   97831  8185359    83.7 |  0.399 % |
c |     99586 |  559257  1310623 |  399781   99539  8302907    83.4 |  0.403 % |
c |    102149 |  559257  1310623 |  439759  102102  8360519    81.9 |  0.403 % |
c |    105993 |  559257  1310623 |  483735  105946  8633190    81.5 |  0.403 % |
c |    111759 |  559222  1310544 |  532109  111705  8830790    79.1 |  0.409 % |
c ==============================================================================
c [1mFound solution: 7057[0m
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 |    119088 |  560348  1313511 |  186782  119034  9225789    77.5 |  0.409 % |
c |    119188 |  560306  1313413 |  205460  119125  9227282    77.5 |  0.415 % |
c |    119340 |  560306  1313413 |  226006  119277  9228056    77.4 |  0.415 % |
c |    119566 |  560306  1313413 |  248606  119503  9231202    77.2 |  0.415 % |
c |    119903 |  560306  1313413 |  273467  119840  9234987    77.1 |  0.415 % |
c |    120409 |  560306  1313413 |  300814  120346  9241080    76.8 |  0.415 % |
c |    121168 |  560306  1313413 |  330895  121105  9251183    76.4 |  0.415 % |
c |    122307 |  560306  1313413 |  363985  122244  9271616    75.8 |  0.415 % |
c |    124015 |  560306  1313413 |  400383  123952  9431695    76.1 |  0.415 % |
c |    126577 |  560306  1313413 |  440422  126514  9508990    75.2 |  0.415 % |
c |    130421 |  559913  1312537 |  484464  130355  9685336    74.3 |  0.467 % |
c |    136187 |  559913  1312537 |  532910  136121 10247409    75.3 |  0.467 % |
c ==============================================================================
c [1mFound solution: 6620[0m
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 |    137914 |  560751  1314600 |  186917  137848 10314918    74.8 |  0.467 % |
c |    138014 |  560751  1314600 |  205608  137948 10315911    74.8 |  0.466 % |
c |    138165 |  560751  1314600 |  226169  138099 10317492    74.7 |  0.466 % |
c |    138390 |  560751  1314600 |  248786  138324 10318668    74.6 |  0.466 % |
c |    138729 |  560751  1314600 |  273665  138663 10323472    74.5 |  0.466 % |
c |    139235 |  560751  1314600 |  301031  139169 10327920    74.2 |  0.466 % |
c |    139997 |  560751  1314600 |  331134  139931 10336052    73.9 |  0.466 % |
c |    141136 |  560751  1314600 |  364248  141070 10360456    73.4 |  0.466 % |
c |    142847 |  560751  1314600 |  400673  142781 10379767    72.7 |  0.466 % |
c |    145409 |  560739  1314573 |  440740  145342 10445617    71.9 |  0.468 % |
c |    149253 |  560739  1314573 |  484814  149186 10511984    70.5 |  0.468 % |
c ==============================================================================
c [1mFound solution: 6488[0m
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 |    151261 |  560761  1314653 |  186920  151191 10586361    70.0 |  0.468 % |
c |    151362 |  560761  1314653 |  205612  151292 10589236    70.0 |  0.475 % |
c |    151513 |  560761  1314653 |  226173  151443 10593887    70.0 |  0.475 % |
c |    151738 |  560761  1314653 |  248790  151668 10597787    69.9 |  0.475 % |
c |    152075 |  560761  1314653 |  273669  152005 10617281    69.8 |  0.475 % |
c |    152581 |  560761  1314653 |  301036  152511 10626184    69.7 |  0.475 % |
c |    153340 |  560761  1314653 |  331140  153270 10637022    69.4 |  0.475 % |
c |    154479 |  560761  1314653 |  364254  154409 10693941    69.3 |  0.475 % |
c |    156187 |  560740  1314603 |  400679  156108 10909790    69.9 |  0.478 % |
c |    158750 |  560740  1314603 |  440747  158671 11002600    69.3 |  0.478 % |
c |    162596 |  560682  1314473 |  484822  162494 11166367    68.7 |  0.487 % |
c |    168362 |  560631  1314359 |  533304  168259 11376430    67.6 |  0.493 % |
c |    177011 |  560584  1314259 |  586635  176902 11587917    65.5 |  0.502 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 24661 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.95 0.98 2/54 24657
Raw data (stat): 24657 (runsolver) R 24656 7266 7265 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 782251879 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99978 s]
Raw data (loadavg): 0.93 0.95 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0007 s]
Raw data (loadavg): 0.94 0.96 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0011 s]
Raw data (loadavg): 0.95 0.96 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0009 s]
Raw data (loadavg): 0.95 0.96 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0019 s]
Raw data (loadavg): 0.96 0.96 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0013 s]
Raw data (loadavg): 0.97 0.96 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0021 s]
Raw data (loadavg): 0.97 0.96 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0032 s]
Raw data (loadavg): 0.98 0.96 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0026 s]
Raw data (loadavg): 0.98 0.96 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24661
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24714
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24714
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24714
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24714
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24714
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24714
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24714
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24716
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.75 s]
Raw data (loadavg): 0.99 0.97 0.98 1/53 24718
Raw data (stat): 24657 (minisat+_script) S 24656 7266 7265 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782251879 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.75
CPU time (s): 1229.89
CPU user time (s): 1228.87
CPU system time (s): 1.02484
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####