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-ii8e2.opb
MD5SUM	66ef5c48f4a7492e24281157b7778ffb
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	514
Optimality of the best value was proved	NO
Number of terms in the objective function	1740
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	1740
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1740
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04884
Number of variables	1740
Total number of constraints	6991
Number of constraints which are clauses	6991
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	10
Trace number 30410

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        643128 kB
Buffers:         34088 kB
Cached:         335740 kB
SwapCached:         92 kB
Active:          60712 kB
Inactive:       311824 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        642876 kB
SwapTotal:     2097136 kB
SwapFree:      2096752 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6392 kB
Slab:            13392 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 16:58:57 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 21758 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6991 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 |    6991    16290 |    2330       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 590[0m
c ---[   0]---> Sorter-cost:98402     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         4 |  128567   300131 |   42855       4       22     5.5 |  0.000 % |
c |       106 |  128430   299852 |   47140     102     3326    32.6 |  0.102 % |
c |       257 |  128430   299852 |   51854     253     7574    29.9 |  0.102 % |
c |       482 |  128430   299852 |   57040     478    12756    26.7 |  0.102 % |
c |       819 |  128430   299852 |   62744     815    19346    23.7 |  0.102 % |
c |      1326 |  127377   297611 |   69018    1223    87028    71.2 |  0.826 % |
c |      2085 |  127264   297372 |   75920    1980   106712    53.9 |  0.903 % |
c |      3225 |  127264   297372 |   83512    3120   139734    44.8 |  0.903 % |
c |      4933 |  127208   297252 |   91863    4827   190149    39.4 |  0.942 % |
c |      7495 |  126172   294982 |  101049    7371   620898    84.2 |  1.694 % |
c |     11339 |  126168   294974 |  111154   11213   773205    69.0 |  1.696 % |
c ==============================================================================
c [1mFound solution: 574[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15699 |  126007   294731 |   42002   15567  2039083   131.0 |  1.696 % |
c |     15799 |  125560   293728 |   46202   15658  2041962   130.4 |  2.288 % |
c |     15954 |  125468   293528 |   50822   15793  2051349   129.9 |  2.354 % |
c |     16182 |  125045   292603 |   55904   16012  2055877   128.4 |  2.660 % |
c |     16523 |  125045   292603 |   61495   16353  2063549   126.2 |  2.660 % |
c |     17031 |  125041   292595 |   67644   16860  2075782   123.1 |  2.662 % |
c |     17790 |  125041   292595 |   74409   17619  2121233   120.4 |  2.662 % |
c |     18929 |  124707   291849 |   81850   18753  2161700   115.3 |  2.913 % |
c |     20638 |  124446   291276 |   90035   20456  2323907   113.6 |  3.102 % |
c ==============================================================================
c [1mFound solution: 555[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21743 |  124549   291618 |   41516   21386  2359361   110.3 |  3.102 % |
c |     21843 |  124523   291562 |   45667   21485  2368288   110.2 |  3.194 % |
c |     21993 |  124523   291562 |   50234   21635  2372240   109.6 |  3.194 % |
c |     22219 |  124523   291562 |   55257   21861  2378958   108.8 |  3.194 % |
c |     22556 |  124263   290984 |   60783   22191  2414231   108.8 |  3.388 % |
c |     23063 |  124080   290577 |   66861   22674  2426492   107.0 |  3.524 % |
c |     23822 |  124080   290577 |   73548   23433  2454764   104.8 |  3.524 % |
c |     24961 |  123797   289950 |   80902   24567  2535712   103.2 |  3.732 % |
c ==============================================================================
c [1mFound solution: 494[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25686 |  124281   291166 |   41427   25208  2510359    99.6 |  3.732 % |
c |     25788 |  124281   291166 |   45569   25310  2517812    99.5 |  3.736 % |
c |     25941 |  124281   291166 |   50126   25463  2521177    99.0 |  3.736 % |
c |     26166 |  124281   291166 |   55139   25688  2544728    99.1 |  3.736 % |
c |     26504 |  124281   291166 |   60653   26026  2552818    98.1 |  3.736 % |
c |     27010 |  124281   291166 |   66718   26532  2566479    96.7 |  3.736 % |
c |     27769 |  124281   291166 |   73390   27291  2649683    97.1 |  3.736 % |
c |     28909 |  124268   291139 |   80729   28426  2831024    99.6 |  3.745 % |
c |     30620 |  123560   289545 |   88802   30124  2971797    98.7 |  4.281 % |
c |     33183 |  123560   289545 |   97682   32687  3060042    93.6 |  4.281 % |
c |     37027 |  122823   287902 |  107450   36485  3318331    91.0 |  4.829 % |
c |     42795 |  122823   287902 |  118196   42253  3563411    84.3 |  4.829 % |
c |     51444 |  122349   286858 |  130015   50853  4043393    79.5 |  5.174 % |
c |     64418 |  122229   286580 |  143017   63803  4620873    72.4 |  5.269 % |
c |     83879 |  121410   284759 |  157318   83153  7456425    89.7 |  5.875 % |
c |    113072 |  121372   284671 |  173050  112319 10057431    89.5 |  5.906 % |
c |    156862 |  121119   284108 |  190355  156017 12155915    77.9 |  6.093 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 32591 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.96 1/54 32587
Raw data (stat): 32587 (runsolver) R 32586 15547 15546 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 782172741 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0014 s]
Raw data (loadavg): 0.93 0.95 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.94 0.96 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.0019 s]
Raw data (loadavg): 0.95 0.96 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.002 s]
Raw data (loadavg): 0.95 0.96 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.0026 s]
Raw data (loadavg): 0.96 0.96 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.0026 s]
Raw data (loadavg): 0.97 0.96 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.0036 s]
Raw data (loadavg): 0.97 0.96 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.0043 s]
Raw data (loadavg): 0.98 0.96 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.0044 s]
Raw data (loadavg): 0.98 0.96 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.004 s]
Raw data (loadavg): 0.98 0.96 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.96 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.73 s]
Raw data (loadavg): 0.99 0.97 0.96 1/53 32591
Raw data (stat): 32587 (minisat+_script) S 32586 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782172741 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.73
CPU time (s): 1229.88
CPU user time (s): 1229.05
CPU system time (s): 0.834873
CPU usage (%): 100.013
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####