PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-05-25 16:27:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=21737 boxname=wulflinc12 idbench=155 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  151e246868267296e134c3c76a3cb289  /oldhome/oroussel/tmp/wulflinc12/normalized-ii32d1.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc12/normalized-ii32d1.opb
IDLAUNCH: 21737
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        347876 kB
Buffers:         34688 kB
Cached:         631012 kB
SwapCached:        564 kB
Active:          55424 kB
Inactive:       612672 kB
HighTotal:      131008 kB
HighFree:         2128 kB
LowTotal:       903652 kB
LowFree:        345748 kB
SwapTotal:     2097136 kB
SwapFree:      2096076 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5680 kB
Slab:            13200 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 16:48:03 (client local time) WITH STATUS 152 IN 1229.85 SECONDS
stats: 21737 7 1229.85 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3035 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    3035     9828 |    1011       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 319[0m
c ---[   0]---> Sorter-cost:30182     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        22 |   39401    94869 |   13133      22      879    40.0 |  0.000 % |
c ==============================================================================
c [1mFound solution: 304[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        78 |   39566    95345 |   13188      77     5158    67.0 |  0.000 % |
c ==============================================================================
c [1mFound solution: 294[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        82 |   39693    95707 |   13231      81     5475    67.6 |  0.000 % |
c |       182 |   39693    95707 |   14554     181    15088    83.4 |  0.172 % |
c |       334 |   39693    95707 |   16009     333    24915    74.8 |  0.172 % |
c |       559 |   39693    95707 |   17610     558    43774    78.4 |  0.172 % |
c |       897 |   39610    95534 |   19371     893    84437    94.6 |  0.353 % |
c |      1403 |   39610    95534 |   21308    1399   139614    99.8 |  0.353 % |
c |      2164 |   39439    95178 |   23439    2155   228675   106.1 |  0.718 % |
c |      3305 |   39396    95089 |   25783    3295   356671   108.2 |  0.806 % |
c |      5014 |   39147    94550 |   28361    4996   564213   112.9 |  1.379 % |
c ==============================================================================
c [1mFound solution: 293[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6786 |   39147    94597 |   13049    6766   805584   119.1 |  1.379 % |
c |      6886 |   38248    92654 |   14353    6843   807275   118.0 |  3.544 % |
c |      7036 |   38101    92333 |   15789    6978   810806   116.2 |  3.889 % |
c |      7261 |   38101    92333 |   17368    7203   835914   116.1 |  3.889 % |
c |      7598 |   38101    92333 |   19105    7540   859380   114.0 |  3.889 % |
c |      8107 |   38058    92242 |   21015    8048   902377   112.1 |  3.985 % |
c |      8867 |   37957    92027 |   23117    8806   985841   112.0 |  4.209 % |
c |     10007 |   37816    91714 |   25428    9942  1069396   107.6 |  4.550 % |
c |     11717 |   37684    91426 |   27971   11649  1217804   104.5 |  4.858 % |
c |     14279 |   37684    91426 |   30768   14211  1480329   104.2 |  4.858 % |
c |     18124 |   35697    87013 |   33845   17979  1810517   100.7 |  9.636 % |
c |     23891 |   35469    86509 |   37230   23742  2607070   109.8 | 10.169 % |
c |     32540 |   35409    86375 |   40953   32384  3450033   106.5 | 10.317 % |
c |     45515 |   35296    86126 |   45048   15064  1255595    83.4 | 10.585 % |
c ==============================================================================
c [1mFound solution: 292[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     51755 |   35264    86031 |   11754   21218  1737423    81.9 | 10.585 % |
c |     51858 |   35264    86031 |   12929   10712   660163    61.6 | 10.688 % |
c |     52010 |   35264    86031 |   14222   10864   673235    62.0 | 10.688 % |
c |     52238 |   35264    86031 |   15644   11092   680554    61.4 | 10.688 % |
c |     52575 |   35264    86031 |   17209   11429   710291    62.1 | 10.688 % |
c |     53081 |   35264    86031 |   18929   11935   753857    63.2 | 10.688 % |
c |     53840 |   35264    86031 |   20822   12694   821047    64.7 | 10.688 % |
c |     54983 |   35264    86031 |   22905   13837   917888    66.3 | 10.688 % |
c |     56691 |   35264    86031 |   25195   15545  1062283    68.3 | 10.688 % |
c |     59253 |   35264    86031 |   27715   18107  1325662    73.2 | 10.688 % |
c |     63098 |   35264    86031 |   30486   21952  1774222    80.8 | 10.688 % |
c |     68864 |   35212    85914 |   33535   27717  2220091    80.1 | 10.817 % |
c |     77513 |   35212    85914 |   36889   36366  2981361    82.0 | 10.817 % |
c |     90487 |   35212    85914 |   40577   23247  1770661    76.2 | 10.817 % |
c |    109948 |   35153    85787 |   44635   42707  3210142    75.2 | 10.953 % |
c |    139140 |   35153    85787 |   49099   40523  2721836    67.2 | 10.953 % |
c ==============================================================================
c [1mFound solution: 291[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    148770 |   35121    85732 |   11707   50152  3413506    68.1 | 10.953 % |
c |    148871 |   35121    85732 |   12877    9760   464349    47.6 | 11.093 % |
c |    149026 |   35121    85732 |   14165    9915   478892    48.3 | 11.093 % |
c |    149251 |   35121    85732 |   15582   10140   496222    48.9 | 11.093 % |
c |    149591 |   35121    85732 |   17140   10480   520952    49.7 | 11.093 % |
c |    150097 |   35121    85732 |   18854   10986   558194    50.8 | 11.093 % |
c |    150858 |   35121    85732 |   20739   11747   618457    52.6 | 11.093 % |
c |    151998 |   35121    85732 |   22813   12887   693350    53.8 | 11.093 % |
c |    153707 |   35121    85732 |   25094   14596   828225    56.7 | 11.093 % |
c |    156271 |   34396    84085 |   27604   17133   993365    58.0 | 12.902 % |
c |    160118 |   34396    84085 |   30364   20980  1393378    66.4 | 12.902 % |
c |    165886 |   34396    84085 |   33401   26748  2021075    75.6 | 12.902 % |
c |    174535 |   34396    84085 |   36741   35397  2864710    80.9 | 12.902 % |
c |    187509 |   34396    84085 |   40415   23543  1656176    70.3 | 12.902 % |
c ==============================================================================
c [1mFound solution: 290[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    205542 |   34380    84019 |   11460   41576  3086386    74.2 | 12.902 % |
c |    205642 |   34380    84019 |   12606    8593   377408    43.9 | 12.961 % |
c |    205794 |   34380    84019 |   13866    8745   388045    44.4 | 12.961 % |
c |    206019 |   34380    84019 |   15253    8970   404742    45.1 | 12.961 % |
c |    206356 |   34380    84019 |   16778    9307   431358    46.3 | 12.961 % |
c |    206863 |   34380    84019 |   18456    9814   473568    48.3 | 12.961 % |
c |    207622 |   34380    84019 |   20302   10573   515082    48.7 | 12.961 % |
c |    208764 |   34380    84019 |   22332   11715   574466    49.0 | 12.961 % |
c |    210472 |   34380    84019 |   24565   13423   669115    49.8 | 12.961 % |
c |    213034 |   34380    84019 |   27022   15985   795872    49.8 | 12.961 % |
c |    216881 |   34380    84019 |   29724   19832   998091    50.3 | 12.961 % |
c |    222647 |   34380    84019 |   32696   25598  1341738    52.4 | 12.961 % |
c |    231296 |   34380    84019 |   35966   34247  2022239    59.0 | 12.961 % |
c |    244270 |   34380    84019 |   39563   21209  1538693    72.5 | 12.961 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 14369 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.88 0.93 0.96 2/54 14365
Raw data (stat): 14365 (runsolver) R 14364 32284 32283 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 782087285 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+10.0017 s]
Raw data (loadavg): 0.90 0.93 0.96 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.0019 s]
Raw data (loadavg): 0.91 0.93 0.96 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.0018 s]
Raw data (loadavg): 0.93 0.94 0.96 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.0019 s]
Raw data (loadavg): 0.94 0.94 0.96 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.0024 s]
Raw data (loadavg): 0.95 0.94 0.96 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.0036 s]
Raw data (loadavg): 0.95 0.94 0.96 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.0046 s]
Raw data (loadavg): 0.96 0.94 0.96 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.0049 s]
Raw data (loadavg): 0.97 0.94 0.96 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.0048 s]
Raw data (loadavg): 0.97 0.95 0.96 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.005 s]
Raw data (loadavg): 0.98 0.95 0.96 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.006 s]
Raw data (loadavg): 0.98 0.95 0.96 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.007 s]
Raw data (loadavg): 0.98 0.95 0.96 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.007 s]
Raw data (loadavg): 0.98 0.95 0.96 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.007 s]
Raw data (loadavg): 0.99 0.95 0.96 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.007 s]
Raw data (loadavg): 0.99 0.95 0.96 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.008 s]
Raw data (loadavg): 0.99 0.95 0.96 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.008 s]
Raw data (loadavg): 1.07 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.008 s]
Raw data (loadavg): 1.06 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.009 s]
Raw data (loadavg): 1.05 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.008 s]
Raw data (loadavg): 1.04 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.009 s]
Raw data (loadavg): 1.03 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.01 s]
Raw data (loadavg): 1.03 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.01 s]
Raw data (loadavg): 1.02 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.011 s]
Raw data (loadavg): 1.02 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.011 s]
Raw data (loadavg): 1.02 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.011 s]
Raw data (loadavg): 1.01 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.011 s]
Raw data (loadavg): 1.01 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.011 s]
Raw data (loadavg): 1.01 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.012 s]
Raw data (loadavg): 1.01 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.012 s]
Raw data (loadavg): 1.01 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.013 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.013 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.013 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.014 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.015 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.016 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.017 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.017 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.017 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.017 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.018 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.018 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.018 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.018 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.018 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.019 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.02 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.02 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.022 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.023 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.022 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.023 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.023 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.023 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.022 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.023 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.024 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.023 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.023 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.024 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.023 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.024 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.024 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.024 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.025 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.026 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.027 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.027 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.027 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.028 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.027 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.028 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.029 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.029 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.03 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.03 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.031 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.031 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.031 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.032 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.031 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.032 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.032 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.032 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.033 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.033 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.034 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.034 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.033 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.034 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.034 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.034 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.034 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.034 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.035 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.034 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.037 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.05 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.04 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.05 s]
Raw data (loadavg): 1.00 0.97 0.97 2/55 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.72 s]
Raw data (loadavg): 1.00 0.97 0.97 1/53 14369
Raw data (stat): 14365 (minisat+_script) S 14364 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782087285 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.72
CPU time (s): 1229.85
CPU user time (s): 1229.58
CPU system time (s): 0.26296
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####