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-ran13x13.opb
MD5SUM	52c9f5bb9e744e5b269906d75a40a640
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	8418073
Optimality of the best value was proved	NO
Number of terms in the objective function	5239
Biggest coefficient in the objective function	5368709120
Number of bits for the biggest coefficient in the objective function	33
Sum of the numbers in the objective function	968548072570
Number of bits of the sum of numbers in the objective function	40
Biggest number in a constraint	5368709120
Number of bits of the biggest number in a constraint	33
Biggest sum of numbers in a constraint	968548072570
Number of bits of the biggest sum of numbers	40
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1254.31
Number of variables	5239
Total number of constraints	195
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	195
Minimum length of a constraint	31
Maximum length of a constraint	390
Trace number 30888

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        360788 kB
Buffers:         37524 kB
Cached:         609904 kB
SwapCached:          0 kB
Active:          24788 kB
Inactive:       629564 kB
HighTotal:      131008 kB
HighFree:        20496 kB
LowTotal:       903652 kB
LowFree:        340292 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7068 kB
Slab:            13872 kB
Committed_AS:    63732 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 20:51:54 (client local time) WITH STATUS 152 IN 1229.87 SECONDS
stats: 22284 7 1229.87 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 221 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 219]---> Adder-cost: 322   maxlim: 135155   bits: 18/18
c ---[ 217]---> Adder-cost: 330   maxlim: 209907   bits: 18/18
c ---[ 215]---> Adder-cost: 330   maxlim: 215027   bits: 18/18
c ---[ 213]---> Adder-cost: 322   maxlim: 137203   bits: 18/18
c ---[ 211]---> Adder-cost: 330   maxlim: 210931   bits: 18/18
c ---[ 209]---> Adder-cost: 322   maxlim: 138227   bits: 18/18
c ---[ 207]---> Adder-cost: 330   maxlim: 202739   bits: 18/18
c ---[ 205]---> Adder-cost: 322   maxlim: 136179   bits: 18/18
c ---[ 203]---> Adder-cost: 306   maxlim: 84979   bits: 17/17
c ---[ 201]---> Adder-cost: 330   maxlim: 209907   bits: 18/18
c ---[ 199]---> Adder-cost: 306   maxlim: 84979   bits: 17/17
c ---[ 197]---> Adder-cost: 330   maxlim: 212979   bits: 18/18
c ---[ 195]---> Adder-cost: 322   maxlim: 137203   bits: 18/18
c ---[ 193]---> Adder-cost: 344   maxlim: 274419   bits: 19/19
c ---[ 191]---> Adder-cost: 344   maxlim: 266227   bits: 19/19
c ---[ 189]---> Adder-cost: 288   maxlim: 51187   bits: 16/16
c ---[ 187]---> Adder-cost: 330   maxlim: 187379   bits: 18/18
c ---[ 185]---> Adder-cost: 312   maxlim: 101363   bits: 17/17
c ---[ 183]---> Adder-cost: 330   maxlim: 183283   bits: 18/18
c ---[ 181]---> Adder-cost: 312   maxlim: 100339   bits: 17/17
c ---[ 179]---> Adder-cost: 288   maxlim: 50163   bits: 16/16
c ---[ 177]---> Adder-cost: 344   maxlim: 250867   bits: 19/18
c ---[ 175]---> Adder-cost: 312   maxlim: 102387   bits: 17/17
c ---[ 173]---> Adder-cost: 264   maxlim: 25587   bits: 15/15
c ---[ 171]---> Adder-cost: 344   maxlim: 260083   bits: 19/18
c ---[ 169]---> Adder-cost: 344   maxlim: 262131   bits: 19/18
c ---[ 168]---> BDD-cost:   17
c ---[ 167]---> BDD-cost:   17
c ---[ 166]---> BDD-cost:   13
c ---[ 165]---> BDD-cost:   16
c ---[ 164]---> BDD-cost:   13
c ---[ 163]---> BDD-cost:   16
c ---[ 162]---> BDD-cost:   16
c ---[ 161]---> BDD-cost:   19
c ---[ 160]---> BDD-cost:   19
c ---[ 159]---> BDD-cost:   18
c ---[ 158]---> BDD-cost:   15
c ---[ 157]---> BDD-cost:   14
c ---[ 156]---> BDD-cost:   19
c ---[ 155]---> BDD-cost:   18
c ---[ 154]---> BDD-cost:   14
c ---[ 153]---> BDD-cost:   12
c ---[ 152]---> BDD-cost:   19
c ---[ 151]---> BDD-cost:   19
c ---[ 150]---> BDD-cost:   13
c ---[ 149]---> BDD-cost:   18
c ---[ 148]---> BDD-cost:   16
c ---[ 147]---> BDD-cost:   16
c ---[ 146]---> BDD-cost:   16
c ---[ 145]---> BDD-cost:   16
c ---[ 144]---> BDD-cost:   16
c ---[ 143]---> BDD-cost:   15
c ---[ 142]---> BDD-cost:   14
c ---[ 141]---> BDD-cost:   16
c ---[ 140]---> BDD-cost:   14
c ---[ 139]---> BDD-cost:   12
c ---[ 138]---> BDD-cost:   16
c ---[ 137]---> BDD-cost:   16
c ---[ 136]---> BDD-cost:   13
c ---[ 135]---> BDD-cost:   18
c ---[ 134]---> BDD-cost:   16
c ---[ 133]---> BDD-cost:   18
c ---[ 132]---> BDD-cost:   16
c ---[ 131]---> BDD-cost:   16
c ---[ 130]---> BDD-cost:   18
c ---[ 129]---> BDD-cost:   15
c ---[ 128]---> BDD-cost:   14
c ---[ 127]---> BDD-cost:   16
c ---[ 126]---> BDD-cost:   14
c ---[ 125]---> BDD-cost:   12
c ---[ 124]---> BDD-cost:   16
c ---[ 123]---> BDD-cost:   16
c ---[ 122]---> BDD-cost:   20
c ---[ 121]---> BDD-cost:   13
c ---[ 120]---> BDD-cost:   18
c ---[ 119]---> BDD-cost:   16
c ---[ 118]---> BDD-cost:   16
c ---[ 117]---> BDD-cost:   16
c ---[ 116]---> BDD-cost:   16
c ---[ 115]---> BDD-cost:   15
c ---[ 114]---> BDD-cost:   14
c ---[ 113]---> BDD-cost:   16
c ---[ 112]---> BDD-cost:   14
c ---[ 111]---> BDD-cost:   18
c ---[ 110]---> BDD-cost:   12
c ---[ 109]---> BDD-cost:   16
c ---[ 108]---> BDD-cost:   16
c ---[ 107]---> BDD-cost:   13
c ---[ 106]---> BDD-cost:   18
c ---[ 105]---> BDD-cost:   16
c ---[ 104]---> BDD-cost:   18
c ---[ 103]---> BDD-cost:   18
c ---[ 102]---> BDD-cost:   18
c ---[ 101]---> BDD-cost:   15
c ---[ 100]---> BDD-cost:   15
c ---[  99]---> BDD-cost:   14
c ---[  98]---> BDD-cost:   18
c ---[  97]---> BDD-cost:   14
c ---[  96]---> BDD-cost:   12
c ---[  95]---> BDD-cost:   18
c ---[  94]---> BDD-cost:   18
c ---[  93]---> BDD-cost:   13
c ---[  92]---> BDD-cost:   18
c ---[  91]---> BDD-cost:   16
c ---[  90]---> BDD-cost:   14
c ---[  89]---> BDD-cost:   20
c ---[  88]---> BDD-cost:   14
c ---[  87]---> BDD-cost:   18
c ---[  86]---> BDD-cost:   12
c ---[  85]---> BDD-cost:   20
c ---[  84]---> BDD-cost:   20
c ---[  83]---> BDD-cost:   13
c ---[  82]---> BDD-cost:   18
c ---[  81]---> BDD-cost:   16
c ---[  80]---> BDD-cost:   18
c ---[  79]---> BDD-cost:   18
c ---[  78]---> BDD-cost:   18
c ---[  77]---> BDD-cost:   15
c ---[  76]---> BDD-cost:   15
c ---[  75]---> BDD-cost:   14
c ---[  74]---> BDD-cost:   18
c ---[  73]---> BDD-cost:   14
c ---[  72]---> BDD-cost:   12
c ---[  71]---> BDD-cost:   18
c ---[  70]---> BDD-cost:   18
c ---[  69]---> BDD-cost:   13
c ---[  68]---> BDD-cost:   18
c ---[  67]---> BDD-cost:   16
c ---[  66]---> BDD-cost:   18
c ---[  65]---> BDD-cost:   14
c ---[  64]---> BDD-cost:   18
c ---[  63]---> BDD-cost:   18
c ---[  62]---> BDD-cost:   15
c ---[  61]---> BDD-cost:   14
c ---[  60]---> BDD-cost:   18
c ---[  59]---> BDD-cost:   14
c ---[  58]---> BDD-cost:   12
c ---[  57]---> BDD-cost:   18
c ---[  56]---> BDD-cost:   18
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   17
c ---[  53]---> BDD-cost:   18
c ---[  52]---> BDD-cost:   16
c ---[  51]---> BDD-cost:   18
c ---[  50]---> BDD-cost:   18
c ---[  49]---> BDD-cost:   18
c ---[  48]---> BDD-cost:   15
c ---[  47]---> BDD-cost:   14
c ---[  46]---> BDD-cost:   18
c ---[  45]---> BDD-cost:   14
c ---[  44]---> BDD-cost:   12
c ---[  43]---> BDD-cost:   14
c ---[  42]---> BDD-cost:   18
c ---[  41]---> BDD-cost:   18
c ---[  40]---> BDD-cost:   13
c ---[  39]---> BDD-cost:   18
c ---[  38]---> BDD-cost:   16
c ---[  37]---> BDD-cost:   16
c ---[  36]---> BDD-cost:   16
c ---[  35]---> BDD-cost:   16
c ---[  34]---> BDD-cost:   15
c ---[  33]---> BDD-cost:   14
c ---[  32]---> BDD-cost:   12
c ---[  31]---> BDD-cost:   16
c ---[  30]---> BDD-cost:   14
c ---[  29]---> BDD-cost:   12
c ---[  28]---> BDD-cost:   16
c ---[  27]---> BDD-cost:   16
c ---[  26]---> BDD-cost:   13
c ---[  25]---> BDD-cost:   16
c ---[  24]---> BDD-cost:   16
c ---[  23]---> BDD-cost:   18
c ---[  22]---> BDD-cost:   20
c ---[  21]---> BDD-cost:   17
c ---[  20]---> BDD-cost:   18
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   14
c ---[  17]---> BDD-cost:   20
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   12
c ---[  14]---> BDD-cost:   20
c ---[  13]---> BDD-cost:   20
c ---[  12]---> BDD-cost:   13
c ---[  11]---> BDD-cost:   18
c ---[  10]---> BDD-cost:   17
c ---[   9]---> BDD-cost:   16
c ---[   8]---> BDD-cost:   16
c ---[   7]---> BDD-cost:   16
c ---[   6]---> BDD-cost:   16
c ---[   5]---> BDD-cost:   15
c ---[   4]---> BDD-cost:   14
c ---[   3]---> BDD-cost:   16
c ---[   2]---> BDD-cost:   14
c ---[   1]---> BDD-cost:   12
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   59169   205907 |   19723       0        0     nan |  0.000 % |
c |       100 |   58966   205226 |   21695      81      248     3.1 | 26.670 % |
c |       250 |   58929   205105 |   23864     224      679     3.0 | 26.710 % |
c |       475 |   58776   204580 |   26251     435     1416     3.3 | 26.899 % |
c |       812 |   58736   204450 |   28876     767     2502     3.3 | 26.946 % |
c |      1318 |   58704   204346 |   31764    1269     4112     3.2 | 26.986 % |
c |      2077 |   58650   204170 |   34940    2021     6941     3.4 | 27.033 % |
c |      3217 |   58607   204027 |   38434    3156    12260     3.9 | 27.081 % |
c |      4925 |   58558   203860 |   42278    4858    29543     6.1 | 27.134 % |
c |      7487 |   58532   203772 |   46505    7418    57519     7.8 | 27.168 % |
c |     11332 |   58499   203663 |   51156   11258    97364     8.6 | 27.202 % |
c |     17098 |   58499   203663 |   56272   17024   235102    13.8 | 27.202 % |
c |     25748 |   58358   203180 |   61899   25653   369038    14.4 | 27.363 % |
c |     38723 |   58332   203092 |   68089   38625  1061555    27.5 | 27.397 % |
c |     58184 |   58178   202572 |   74898   58063  1362471    23.5 | 27.579 % |
c |     87376 |   57836   201424 |   82387   29884   394312    13.2 | 28.003 % |
c ==============================================================================
c [1mFound solution: 33155221[0m
c ---[   0]---> Adder-cost: 8227   maxlim: 12393445   bits: 25/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    117520 |  115043   405890 |   38347   59987  1494905    24.9 | 28.003 % |
c |    117620 |  115036   405867 |   42181   22990   201489     8.8 | 18.278 % |
c |    117771 |  115029   405844 |   46399   23139   202349     8.7 | 18.283 % |
c |    117996 |  114987   405700 |   51039   23356   203616     8.7 | 18.309 % |
c |    118334 |  114978   405671 |   56143   23693   205716     8.7 | 18.317 % |
c |    118840 |  114978   405671 |   61758   24199   208869     8.6 | 18.317 % |
c |    119599 |  114978   405671 |   67934   24958   214627     8.6 | 18.317 % |
c |    120738 |  114978   405671 |   74727   26097   224536     8.6 | 18.317 % |
c |    122446 |  114971   405648 |   82200   27803   239431     8.6 | 18.322 % |
c |    125009 |  114897   405398 |   90420   30346   259028     8.5 | 18.374 % |
c |    128853 |  114840   405203 |   99462   34183   293418     8.6 | 18.413 % |
c |    134619 |  114777   404990 |  109408   39934   358967     9.0 | 18.460 % |
c |    143269 |  114777   404990 |  120349   48584   497222    10.2 | 18.460 % |
c ==============================================================================
c [1mFound solution: 28619477[0m
c ---[   0]---> Adder-cost: 2   maxlim: 16929189   bits: 26/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    149142 |  114806   405203 |   38268   54457   604992    11.1 | 18.460 % |
c |    149242 |  114806   405203 |   42094   24036   246610    10.3 | 18.489 % |
c |    149392 |  114806   405203 |   46304   24186   247331    10.2 | 18.489 % |
c |    149617 |  114797   405174 |   50934   24409   248759    10.2 | 18.497 % |
c |    149956 |  114797   405174 |   56028   24748   251161    10.1 | 18.497 % |
c |    150462 |  114797   405174 |   61630   25254   254327    10.1 | 18.497 % |
c |    151221 |  114773   405092 |   67794   26010   258715     9.9 | 18.515 % |
c |    152361 |  114773   405092 |   74573   27150   266147     9.8 | 18.515 % |
c |    154069 |  114773   405092 |   82030   28858   278656     9.7 | 18.515 % |
c |    156631 |  114773   405092 |   90233   31420   298787     9.5 | 18.515 % |
c |    160475 |  114758   405043 |   99257   35261   332503     9.4 | 18.528 % |
c |    166242 |  114749   405012 |  109183   41025   398407     9.7 | 18.532 % |
c |    174891 |  114740   404981 |  120101   49671   816775    16.4 | 18.536 % |
c |    187865 |  114680   404767 |  132111   62637  1096475    17.5 | 18.580 % |
c |    207326 |  114647   404656 |  145322   82094  4770429    58.1 | 18.606 % |
c |    236519 |  114614   404545 |  159854  111280 10147150    91.2 | 18.632 % |
c ==============================================================================
c [1mFound solution: 23702357[0m
c ---[   0]---> Adder-cost: 0   maxlim: 21846309   bits: 26/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    240672 |  114552   404460 |   38184  115418 10273582    89.0 | 18.632 % |
c |    240772 |  114552   404460 |   42002   22162  1907867    86.1 | 18.730 % |
c |    240922 |  114552   404460 |   46202   22312  1908900    85.6 | 18.730 % |
c |    241149 |  114552   404460 |   50822   22539  1911906    84.8 | 18.730 % |
c |    241487 |  114552   404460 |   55905   22877  1913606    83.6 | 18.730 % |
c |    241993 |  114552   404460 |   61495   23383  1916932    82.0 | 18.730 % |
c |    242754 |  114552   404460 |   67645   24144  1928308    79.9 | 18.730 % |
c |    243893 |  114552   404460 |   74409   25283  1936448    76.6 | 18.730 % |
c |    245601 |  114545   404437 |   81850   26989  1949899    72.2 | 18.735 % |
c |    248163 |  114545   404437 |   90035   29551  1978783    67.0 | 18.735 % |
c |    252008 |  114545   404437 |   99039   33396  2096875    62.8 | 18.735 % |
c |    257774 |  114545   404437 |  108943   39162  2241626    57.2 | 18.735 % |
c |    266423 |  114545   404437 |  119837   47811  2825493    59.1 | 18.735 % |
c |    279397 |  114545   404437 |  131821   60785  3650200    60.1 | 18.735 % |
c |    298858 |  114513   404333 |  145003   80240  4048618    50.5 | 18.761 % |
c |    328051 |  114513   404333 |  159504  109433  5806871    53.1 | 18.761 % |
c ==============================================================================
c [1mFound solution: 23459838[0m
c ---[   0]---> Adder-cost: 0   maxlim: 22088828   bits: 26/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    340331 |  114528   404551 |   38176  121711  6139137    50.4 | 18.761 % |
c |    340431 |  114528   404551 |   41993   25512   404097    15.8 | 18.803 % |
c |    340581 |  114528   404551 |   46192   25662   404810    15.8 | 18.803 % |
c |    340806 |  114528   404551 |   50812   25887   406459    15.7 | 18.803 % |
c |    341143 |  114528   404551 |   55893   26224   408841    15.6 | 18.803 % |
c |    341650 |  114528   404551 |   61482   26731   412457    15.4 | 18.803 % |
c |    342409 |  114519   404522 |   67631   27489   419514    15.3 | 18.812 % |
c |    343548 |  114519   404522 |   74394   28628   429035    15.0 | 18.812 % |
c |    345256 |  114519   404522 |   81833   30336   445719    14.7 | 18.812 % |
c |    347818 |  114519   404522 |   90017   32898   469615    14.3 | 18.812 % |
c |    351662 |  114519   404522 |   99018   36742   503239    13.7 | 18.812 % |
c |    357428 |  114519   404522 |  108920   42508   632366    14.9 | 18.812 % |
c ==============================================================================
c [1mFound solution: 18381569[0m
c ---[   0]---> Adder-cost: 0   maxlim: 27167097   bits: 26/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    365398 |  114540   404740 |   38180   50478   774054    15.3 | 18.812 % |
c |    365498 |  114540   404740 |   41998   22479   288028    12.8 | 18.853 % |
c |    365648 |  114540   404740 |   46197   22629   288914    12.8 | 18.853 % |
c |    365873 |  114540   404740 |   50817   22854   290254    12.7 | 18.853 % |
c |    366210 |  114540   404740 |   55899   23191   292257    12.6 | 18.853 % |
c |    366716 |  114540   404740 |   61489   23697   294992    12.4 | 18.853 % |
c |    367475 |  114540   404740 |   67638   24456   299578    12.2 | 18.853 % |
c |    368615 |  114540   404740 |   74402   25596   309766    12.1 | 18.853 % |
c |    370324 |  114531   404709 |   81842   27303   324841    11.9 | 18.857 % |
c |    372886 |  114531   404709 |   90026   29865   367423    12.3 | 18.857 % |
c |    376730 |  114531   404709 |   99029   33709   398490    11.8 | 18.857 % |
c |    382497 |  114531   404709 |  108931   39476   704678    17.9 | 18.857 % |
c |    391147 |  114531   404709 |  119825   48126   971762    20.2 | 18.857 % |
c |    404122 |  114531   404709 |  131807   61101  1320630    21.6 | 18.857 % |
c |    423583 |  114525   404689 |  144988   80561  1876626    23.3 | 18.861 % |
c |    452777 |  114525   404689 |  159487  109755  4572914    41.7 | 18.861 % |
c |    496566 |  114516   404658 |  175436  153542  8905116    58.0 | 18.866 % |
c |    562251 |  114516   404658 |  192979   44738  2231418    49.9 | 18.866 % |
c |    660777 |  114516   404658 |  212277  143264 10062228    70.2 | 18.866 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 22388 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.91 2/54 22384
Raw data (stat): 22384 (runsolver) R 22383 3132 3131 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 769991405 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+9.99997 s]
Raw data (loadavg): 0.93 0.95 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.94 0.96 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.0015 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.0011 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.0022 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.96 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.0028 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.0035 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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+910.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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+970.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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+980.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.07 s]
Raw data (loadavg): 1.06 0.99 0.92 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.07 s]
Raw data (loadavg): 1.05 0.99 0.92 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.07 s]
Raw data (loadavg): 1.04 0.99 0.92 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.07 s]
Raw data (loadavg): 1.04 0.99 0.92 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.07 s]
Raw data (loadavg): 1.03 0.99 0.92 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.07 s]
Raw data (loadavg): 1.03 0.99 0.92 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.07 s]
Raw data (loadavg): 1.02 0.99 0.92 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.07 s]
Raw data (loadavg): 1.02 0.99 0.92 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.07 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.07 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.73 s]
Raw data (loadavg): 1.01 0.99 0.92 1/53 22388
Raw data (stat): 22384 (minisat+_script) S 22383 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 769991405 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.73
CPU time (s): 1229.87
CPU user time (s): 1229.13
CPU system time (s): 0.740887
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####