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/mps-v2-20-10/plato.asu.edu/pub/fctp/normalized-mps-v2-20-10-ran10x10c.opb
MD5SUM	da5013babdadf38e39e51a27df2c50f3
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	18591744
Optimality of the best value was proved	NO
Number of terms in the objective function	3100
Biggest coefficient in the objective function	4831838208
Number of bits for the biggest coefficient in the objective function	33
Sum of the numbers in the objective function	515495338528
Number of bits of the sum of numbers in the objective function	39
Biggest number in a constraint	4831838208
Number of bits of the biggest number in a constraint	33
Biggest sum of numbers in a constraint	515495338528
Number of bits of the biggest sum of numbers	39
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1219.24
Number of variables	3100
Total number of constraints	120
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	120
Minimum length of a constraint	31
Maximum length of a constraint	300
Trace number 30876

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        846996 kB
Buffers:          6348 kB
Cached:         160168 kB
SwapCached:        968 kB
Active:          17288 kB
Inactive:       151436 kB
HighTotal:      131008 kB
HighFree:       108864 kB
LowTotal:       903652 kB
LowFree:        738132 kB
SwapTotal:     2097892 kB
SwapFree:      2096008 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            13200 kB
Committed_AS:    63916 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 20:47:14 (client local time) WITH STATUS 152 IN 1229.9 SECONDS
stats: 22279 7 1229.9 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 138]---> Sorter-cost: 2306     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 2620     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost: 2665     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 132]---> Sorter-cost: 2620     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 2620     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 2620     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Adder-cost: 232   maxlim: 62454   bits: 17/16
c ---[ 122]---> Sorter-cost: 2620     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 2665     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Adder-cost: 216   maxlim: 36854   bits: 16/16
c ---[ 116]---> Sorter-cost: 2693     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Adder-cost: 216   maxlim: 36854   bits: 16/16
c ---[ 112]---> Sorter-cost: 2693     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Adder-cost: 232   maxlim: 65526   bits: 17/16
c ---[ 108]---> Adder-cost: 232   maxlim: 67574   bits: 17/17
c ---[ 106]---> Sorter-cost: 2661     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 2661     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 2693     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Adder-cost: 216   maxlim: 36854   bits: 16/16
c ---[  99]---> BDD-cost:   13
c ---[  98]---> BDD-cost:   14
c ---[  97]---> BDD-cost:   13
c ---[  96]---> BDD-cost:   18
c ---[  95]---> BDD-cost:   13
c ---[  94]---> BDD-cost:   18
c ---[  93]---> BDD-cost:   15
c ---[  92]---> BDD-cost:   14
c ---[  91]---> BDD-cost:   18
c ---[  90]---> BDD-cost:   18
c ---[  89]---> BDD-cost:   18
c ---[  88]---> BDD-cost:   13
c ---[  87]---> BDD-cost:   13
c ---[  86]---> BDD-cost:   13
c ---[  85]---> BDD-cost:   16
c ---[  84]---> BDD-cost:   13
c ---[  83]---> BDD-cost:   16
c ---[  82]---> BDD-cost:   15
c ---[  81]---> BDD-cost:   14
c ---[  80]---> BDD-cost:   18
c ---[  79]---> BDD-cost:   16
c ---[  78]---> BDD-cost:   16
c ---[  77]---> BDD-cost:   13
c ---[  76]---> BDD-cost:   14
c ---[  75]---> BDD-cost:   13
c ---[  74]---> BDD-cost:   18
c ---[  73]---> BDD-cost:   13
c ---[  72]---> BDD-cost:   18
c ---[  71]---> BDD-cost:   15
c ---[  70]---> BDD-cost:   14
c ---[  69]---> BDD-cost:   18
c ---[  68]---> BDD-cost:   18
c ---[  67]---> BDD-cost:   18
c ---[  66]---> BDD-cost:   13
c ---[  65]---> BDD-cost:   14
c ---[  64]---> BDD-cost:   13
c ---[  63]---> BDD-cost:   17
c ---[  62]---> BDD-cost:   13
c ---[  61]---> BDD-cost:   17
c ---[  60]---> BDD-cost:   15
c ---[  59]---> BDD-cost:   14
c ---[  58]---> BDD-cost:   17
c ---[  57]---> BDD-cost:   17
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   12
c ---[  52]---> BDD-cost:   12
c ---[  51]---> BDD-cost:   12
c ---[  50]---> BDD-cost:   12
c ---[  49]---> BDD-cost:   12
c ---[  48]---> BDD-cost:   12
c ---[  47]---> BDD-cost:   12
c ---[  46]---> BDD-cost:   12
c ---[  45]---> BDD-cost:   12
c ---[  44]---> BDD-cost:   12
c ---[  43]---> BDD-cost:   14
c ---[  42]---> BDD-cost:   13
c ---[  41]---> BDD-cost:   18
c ---[  40]---> BDD-cost:   13
c ---[  39]---> BDD-cost:   18
c ---[  38]---> BDD-cost:   15
c ---[  37]---> BDD-cost:   14
c ---[  36]---> BDD-cost:   18
c ---[  35]---> BDD-cost:   16
c ---[  34]---> BDD-cost:   18
c ---[  33]---> BDD-cost:   13
c ---[  32]---> BDD-cost:   14
c ---[  31]---> BDD-cost:   13
c ---[  30]---> BDD-cost:   16
c ---[  29]---> BDD-cost:   13
c ---[  28]---> BDD-cost:   16
c ---[  27]---> BDD-cost:   15
c ---[  26]---> BDD-cost:   14
c ---[  25]---> BDD-cost:   16
c ---[  24]---> BDD-cost:   16
c ---[  23]---> BDD-cost:   16
c ---[  22]---> BDD-cost:   13
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   13
c ---[  19]---> BDD-cost:   18
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   18
c ---[  16]---> BDD-cost:   15
c ---[  15]---> BDD-cost:   14
c ---[  14]---> BDD-cost:   18
c ---[  13]---> BDD-cost:   18
c ---[  12]---> BDD-cost:   18
c ---[  11]---> BDD-cost:   13
c ---[  10]---> BDD-cost:   13
c ---[   9]---> BDD-cost:   13
c ---[   8]---> BDD-cost:   20
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   20
c ---[   5]---> BDD-cost:   15
c ---[   4]---> BDD-cost:   14
c ---[   3]---> BDD-cost:   18
c ---[   2]---> BDD-cost:   16
c ---[   1]---> BDD-cost:   20
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  105646   259466 |   35215       0        0     nan |  0.000 % |
c |       100 |  105646   259466 |   38736     100      705     7.0 |  8.015 % |
c |       250 |  105646   259466 |   42610     250     1320     5.3 |  8.015 % |
c |       475 |  105646   259466 |   46871     475     2399     5.1 |  8.015 % |
c |       812 |  105646   259466 |   51558     812     4080     5.0 |  8.015 % |
c |      1320 |  105630   259414 |   56714    1318     6910     5.2 |  8.023 % |
c |      2079 |  105564   259190 |   62385    2070    11012     5.3 |  8.056 % |
c |      3220 |  105403   258818 |   68624    3192    16614     5.2 |  8.175 % |
c |      4928 |  105343   258680 |   75486    4893    26367     5.4 |  8.218 % |
c |      7492 |  105343   258680 |   83035    7457    40139     5.4 |  8.218 % |
c |     11336 |  104896   257599 |   91338   11274    62479     5.5 |  8.574 % |
c |     17102 |  104515   256573 |  100472   16998    98189     5.8 |  8.828 % |
c |     25751 |  104267   255953 |  110519   25590   224926     8.8 |  9.004 % |
c ==============================================================================
c [1mFound solution: 99691608[0m
c ---[   0]---> Adder-cost: 4953   maxlim: 4167112   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28129 |  138497   378323 |   46165   27955   240787     8.6 |  9.004 % |
c |     28230 |  138497   378323 |   50781   28056   241294     8.6 |  8.019 % |
c |     28380 |  138497   378323 |   55859   28206   242155     8.6 |  8.019 % |
c |     28605 |  138497   378323 |   61445   28431   243648     8.6 |  8.019 % |
c |     28942 |  138497   378323 |   67590   28768   245877     8.5 |  8.019 % |
c ==============================================================================
c [1mFound solution: 97594485[0m
c ---[   0]---> Adder-cost: 35   maxlim: 6264235   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29291 |  138713   379191 |   46237   29116   248666     8.5 |  8.019 % |
c |     29391 |  138656   379060 |   50860   29213   249240     8.5 |  8.089 % |
c |     29541 |  138656   379060 |   55946   29363   250276     8.5 |  8.089 % |
c |     29766 |  138553   378824 |   61541   29587   251627     8.5 |  8.170 % |
c |     30104 |  138553   378824 |   67695   29925   288957     9.7 |  8.170 % |
c |     30611 |  138553   378824 |   74465   30432   292344     9.6 |  8.170 % |
c |     31370 |  138506   378704 |   81911   31187   306203     9.8 |  8.203 % |
c |     32509 |  138506   378704 |   90102   32326   328837    10.2 |  8.203 % |
c ==============================================================================
c [1mFound solution: 65247565[0m
c ---[   0]---> Adder-cost: 20   maxlim: 38611155   bits: 27/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33824 |  138656   379345 |   46218   33638   354051    10.5 |  8.203 % |
c |     33924 |  138656   379345 |   50839   33738   355423    10.5 |  8.233 % |
c |     34074 |  138656   379345 |   55923   33888   357263    10.5 |  8.233 % |
c |     34299 |  138656   379345 |   61516   34113   362594    10.6 |  8.233 % |
c |     34636 |  138640   379293 |   67667   34448   364887    10.6 |  8.240 % |
c |     35144 |  138640   379293 |   74434   34956   369137    10.6 |  8.240 % |
c |     35903 |  138640   379293 |   81878   35715   381275    10.7 |  8.240 % |
c |     37042 |  138640   379293 |   90065   36854   407823    11.1 |  8.240 % |
c |     38750 |  138640   379293 |   99072   38562   464898    12.1 |  8.240 % |
c |     41312 |  138640   379293 |  108979   41124   525472    12.8 |  8.240 % |
c |     45156 |  138640   379293 |  119877   44968   740250    16.5 |  8.240 % |
c ==============================================================================
c [1mFound solution: 64276304[0m
c ---[   0]---> Adder-cost: 0   maxlim: 39582416   bits: 27/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46797 |  138635   379489 |   46211   46605   812650    17.4 |  8.240 % |
c |     46897 |  138635   379489 |   50832   46705   813244    17.4 |  8.293 % |
c |     47049 |  138635   379489 |   55915   46857   814707    17.4 |  8.293 % |
c |     47274 |  138635   379489 |   61506   47082   819373    17.4 |  8.293 % |
c |     47612 |  138635   379489 |   67657   47420   822714    17.3 |  8.293 % |
c |     48118 |  138635   379489 |   74423   47926   829558    17.3 |  8.293 % |
c |     48879 |  138619   379437 |   81865   48684   842322    17.3 |  8.300 % |
c |     50018 |  138562   379309 |   90052   49817   911363    18.3 |  8.340 % |
c |     51727 |  138421   378983 |   99057   51494  1062374    20.6 |  8.436 % |
c |     54289 |  138402   378940 |  108963   54055  1141068    21.1 |  8.447 % |
c |     58136 |  138391   378915 |  119859   57901  1486487    25.7 |  8.455 % |
c |     63902 |  138325   378766 |  131845   63659  1773211    27.9 |  8.500 % |
c |     72551 |  138299   378708 |  145029   72303  2535782    35.1 |  8.519 % |
c ==============================================================================
c [1mFound solution: 62500645[0m
c ---[   0]---> Adder-cost: 0   maxlim: 41358075   bits: 27/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72952 |  138284   378866 |   46094   72701  2555567    35.2 |  8.519 % |
c |     73052 |  138284   378866 |   50703   22769   996443    43.8 |  8.568 % |
c |     73202 |  138284   378866 |   55773   22919   997315    43.5 |  8.568 % |
c |     73428 |  138214   378703 |   61351   23140   998377    43.1 |  8.613 % |
c |     73765 |  138214   378703 |   67486   23477  1001162    42.6 |  8.613 % |
c |     74271 |  138214   378703 |   74234   23983  1007222    42.0 |  8.613 % |
c |     75030 |  138214   378703 |   81658   24742  1064677    43.0 |  8.613 % |
c |     76169 |  138214   378703 |   89824   25881  1071124    41.4 |  8.613 % |
c |     77878 |  138214   378703 |   98806   27590  1141703    41.4 |  8.613 % |
c |     80440 |  138211   378697 |  108687   30151  1348483    44.7 |  8.615 % |
c |     84284 |  137973   378149 |  119555   33991  1406015    41.4 |  8.777 % |
c |     90050 |  137973   378149 |  131511   39757  1620800    40.8 |  8.777 % |
c |     98699 |  137973   378149 |  144662   48406  3294818    68.1 |  8.777 % |
c |    111673 |  137772   377685 |  159128   61361  3814730    62.2 |  8.926 % |
c |    131134 |  137750   377633 |  175041   80820  5408926    66.9 |  8.941 % |
c ==============================================================================
c [1mFound solution: 60904598[0m
c ---[   0]---> Adder-cost: 0   maxlim: 42954122   bits: 27/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    132500 |  137776   377892 |   45925   82186  5543726    67.5 |  8.941 % |
c |    132600 |  137776   377892 |   50517   22593   877249    38.8 |  8.969 % |
c |    132750 |  137656   377619 |   55569   22700   877766    38.7 |  9.048 % |
c |    132976 |  137656   377619 |   61126   22926   879059    38.3 |  9.048 % |
c |    133313 |  137613   377522 |   67238   23255   882589    38.0 |  9.081 % |
c |    133819 |  137597   377485 |   73962   23758   886347    37.3 |  9.093 % |
c |    134578 |  137597   377485 |   81358   24517   891943    36.4 |  9.093 % |
c |    135717 |  137597   377485 |   89494   25656   929101    36.2 |  9.093 % |
c |    137425 |  137597   377485 |   98444   27364   988200    36.1 |  9.093 % |
c |    139988 |  137557   377391 |  108288   29923  1029060    34.4 |  9.126 % |
c |    143834 |  137557   377391 |  119117   33769  1389147    41.1 |  9.126 % |
c |    149600 |  137388   377002 |  131029   39512  1617069    40.9 |  9.245 % |
c |    158249 |  137308   376816 |  144132   48153  2365211    49.1 |  9.300 % |
c |    171223 |  137015   376138 |  158545   61110  2975688    48.7 |  9.523 % |
c |    190684 |  136983   376067 |  174400   80569  4215636    52.3 |  9.544 % |
c |    219876 |  136901   375861 |  191840  109745  7879417    71.8 |  9.599 % |
c |    263668 |  136538   375015 |  211024  153513 10857470    70.7 |  9.846 % |
c |    329352 |  136341   374559 |  232126  219170 19164377    87.4 |  9.995 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 17858 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.93 0.97 0.91 2/55 17854
Raw data (stat): 17854 (runsolver) R 17853 32363 32362 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 719015915 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.94 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0009 s]
Raw data (loadavg): 0.95 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0007 s]
Raw data (loadavg): 0.96 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0013 s]
Raw data (loadavg): 0.96 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0009 s]
Raw data (loadavg): 0.97 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0024 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0016 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+909.999 s]
Raw data (loadavg): 1.07 0.99 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920 s]
Raw data (loadavg): 1.06 0.99 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930 s]
Raw data (loadavg): 1.05 0.99 0.91 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940 s]
Raw data (loadavg): 1.12 1.00 0.92 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950 s]
Raw data (loadavg): 1.10 1.00 0.92 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960 s]
Raw data (loadavg): 1.08 1.00 0.92 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+969.999 s]
Raw data (loadavg): 1.14 1.02 0.93 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+979.999 s]
Raw data (loadavg): 1.12 1.02 0.93 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990 s]
Raw data (loadavg): 1.10 1.02 0.93 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000 s]
Raw data (loadavg): 1.09 1.01 0.93 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010 s]
Raw data (loadavg): 1.15 1.03 0.93 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020 s]
Raw data (loadavg): 1.13 1.03 0.93 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030 s]
Raw data (loadavg): 1.11 1.03 0.93 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040 s]
Raw data (loadavg): 1.17 1.04 0.94 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050 s]
Raw data (loadavg): 1.22 1.06 0.94 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060 s]
Raw data (loadavg): 1.18 1.06 0.94 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070 s]
Raw data (loadavg): 1.16 1.05 0.94 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080 s]
Raw data (loadavg): 1.13 1.05 0.94 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090 s]
Raw data (loadavg): 1.11 1.05 0.94 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100 s]
Raw data (loadavg): 1.09 1.05 0.94 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110 s]
Raw data (loadavg): 1.08 1.05 0.94 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120 s]
Raw data (loadavg): 1.14 1.06 0.95 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130 s]
Raw data (loadavg): 1.12 1.06 0.95 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140 s]
Raw data (loadavg): 1.18 1.07 0.95 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150 s]
Raw data (loadavg): 1.15 1.07 0.95 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160 s]
Raw data (loadavg): 1.13 1.07 0.95 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170 s]
Raw data (loadavg): 1.11 1.06 0.95 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180 s]
Raw data (loadavg): 1.09 1.06 0.95 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190 s]
Raw data (loadavg): 1.16 1.07 0.96 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200 s]
Raw data (loadavg): 1.13 1.07 0.96 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210 s]
Raw data (loadavg): 1.11 1.07 0.96 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220 s]
Raw data (loadavg): 1.25 1.10 0.97 2/56 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.77 s]
Raw data (loadavg): 1.21 1.09 0.97 1/54 17858
Raw data (stat): 17854 (minisat+_script) S 17853 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719015915 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.77
CPU time (s): 1229.9
CPU user time (s): 1228.7
CPU system time (s): 1.20682
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####