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-ran10x10b.opb
MD5SUM	76a1809de3568e1012eb6c6785191a40
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	7588573
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	511129031204
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	511129031204
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	1217.92
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 32055

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-05-27 07:51:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23450 boxname=wulflinc4 idbench=1094 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  76a1809de3568e1012eb6c6785191a40  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-ran10x10b.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-ran10x10b.opb
IDLAUNCH: 23450
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        814748 kB
Buffers:         33668 kB
Cached:         165752 kB
SwapCached:        500 kB
Active:          52748 kB
Inactive:       149052 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        814496 kB
SwapTotal:     2097136 kB
SwapFree:      2096004 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5788 kB
Slab:            12416 kB
Committed_AS:    71792 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 08:12:27 (client local time) WITH STATUS 152 IN 1229.89 SECONDS
stats: 23450 7 1229.89 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]---> BDD-cost: 1570
c ---[ 136]---> BDD-cost: 1408
c ---[ 134]---> BDD-cost: 1321
c ---[ 132]---> BDD-cost: 1572
c ---[ 130]---> BDD-cost: 1353
c ---[ 128]---> BDD-cost: 1515
c ---[ 126]---> BDD-cost: 1466
c ---[ 124]---> BDD-cost: 1250
c ---[ 122]---> BDD-cost: 1321
c ---[ 120]---> BDD-cost: 1604
c ---[ 118]---> BDD-cost: 1252
c ---[ 116]---> BDD-cost: 1553
c ---[ 114]---> BDD-cost: 1395
c ---[ 112]---> BDD-cost: 1599
c ---[ 110]---> BDD-cost: 1588
c ---[ 108]---> BDD-cost: 1252
c ---[ 106]---> BDD-cost: 1599
c ---[ 104]---> BDD-cost: 1475
c ---[ 102]---> BDD-cost: 1040
c ---[ 100]---> BDD-cost: 1475
c ---[  99]---> BDD-cost:   14
c ---[  98]---> BDD-cost:   18
c ---[  97]---> BDD-cost:   14
c ---[  96]---> BDD-cost:   16
c ---[  95]---> BDD-cost:   15
c ---[  94]---> BDD-cost:   16
c ---[  93]---> BDD-cost:   16
c ---[  92]---> BDD-cost:   14
c ---[  91]---> BDD-cost:   16
c ---[  90]---> BDD-cost:   16
c ---[  89]---> BDD-cost:   12
c ---[  88]---> BDD-cost:   16
c ---[  87]---> BDD-cost:   15
c ---[  86]---> BDD-cost:   14
c ---[  85]---> BDD-cost:   14
c ---[  84]---> BDD-cost:   14
c ---[  83]---> BDD-cost:   14
c ---[  82]---> BDD-cost:   14
c ---[  81]---> BDD-cost:   14
c ---[  80]---> BDD-cost:   14
c ---[  79]---> BDD-cost:   14
c ---[  78]---> BDD-cost:   12
c ---[  77]---> BDD-cost:   14
c ---[  76]---> BDD-cost:   16
c ---[  75]---> BDD-cost:   14
c ---[  74]---> BDD-cost:   18
c ---[  73]---> BDD-cost:   15
c ---[  72]---> BDD-cost:   20
c ---[  71]---> BDD-cost:   20
c ---[  70]---> BDD-cost:   14
c ---[  69]---> BDD-cost:   20
c ---[  68]---> BDD-cost:   18
c ---[  67]---> BDD-cost:   12
c ---[  66]---> BDD-cost:   18
c ---[  65]---> BDD-cost:   16
c ---[  64]---> BDD-cost:   14
c ---[  63]---> BDD-cost:   16
c ---[  62]---> BDD-cost:   16
c ---[  61]---> BDD-cost:   16
c ---[  60]---> BDD-cost:   16
c ---[  59]---> BDD-cost:   14
c ---[  58]---> BDD-cost:   16
c ---[  57]---> BDD-cost:   16
c ---[  56]---> BDD-cost:   12
c ---[  55]---> BDD-cost:   16
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   14
c ---[  52]---> BDD-cost:   16
c ---[  51]---> BDD-cost:   15
c ---[  50]---> BDD-cost:   16
c ---[  49]---> BDD-cost:   16
c ---[  48]---> BDD-cost:   14
c ---[  47]---> BDD-cost:   16
c ---[  46]---> BDD-cost:   18
c ---[  45]---> BDD-cost:   12
c ---[  44]---> BDD-cost:   18
c ---[  43]---> BDD-cost:   16
c ---[  42]---> BDD-cost:   14
c ---[  41]---> BDD-cost:   18
c ---[  40]---> BDD-cost:   15
c ---[  39]---> BDD-cost:   18
c ---[  38]---> BDD-cost:   18
c ---[  37]---> BDD-cost:   14
c ---[  36]---> BDD-cost:   18
c ---[  35]---> BDD-cost:   18
c ---[  34]---> BDD-cost:   12
c ---[  33]---> BDD-cost:   18
c ---[  32]---> BDD-cost:   18
c ---[  31]---> BDD-cost:   14
c ---[  30]---> BDD-cost:   14
c ---[  29]---> BDD-cost:   14
c ---[  28]---> BDD-cost:   14
c ---[  27]---> BDD-cost:   14
c ---[  26]---> BDD-cost:   14
c ---[  25]---> BDD-cost:   14
c ---[  24]---> BDD-cost:   14
c ---[  23]---> BDD-cost:   12
c ---[  22]---> BDD-cost:   14
c ---[  21]---> BDD-cost:   12
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   14
c ---[  17]---> BDD-cost:   14
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   14
c ---[  14]---> BDD-cost:   14
c ---[  13]---> BDD-cost:   14
c ---[  12]---> BDD-cost:   12
c ---[  11]---> BDD-cost:   14
c ---[  10]---> BDD-cost:   18
c ---[   9]---> BDD-cost:   14
c ---[   8]---> BDD-cost:   18
c ---[   7]---> BDD-cost:   15
c ---[   6]---> BDD-cost:   19
c ---[   5]---> BDD-cost:   20
c ---[   4]---> BDD-cost:   14
c ---[   3]---> BDD-cost:   20
c ---[   2]---> BDD-cost:   18
c ---[   1]---> BDD-cost:   12
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   83138   239693 |   27712       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 28402562[0m
c ---[   0]---> Sorter-cost:178652     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        22 |  583443  1407598 |  194481      22      494    22.5 |  0.000 % |
c |       122 |  583443  1407598 |  213929     122     5169    42.4 |  0.904 % |
c |       272 |  583443  1407598 |  235322     272     6016    22.1 |  0.904 % |
c |       497 |  583443  1407598 |  258854     497     9075    18.3 |  0.904 % |
c |       836 |  583443  1407598 |  284739     836    10827    13.0 |  0.904 % |
c |      1342 |  583443  1407598 |  313213    1342    28530    21.3 |  0.904 % |
c |      2101 |  583443  1407598 |  344534    2101    40661    19.4 |  0.904 % |
c |      3240 |  583443  1407598 |  378988    3240    53758    16.6 |  0.904 % |
c |      4949 |  583443  1407598 |  416887    4949    70869    14.3 |  0.904 % |
c |      7511 |  583443  1407598 |  458576    7511   104246    13.9 |  0.904 % |
c |     11358 |  583443  1407598 |  504433   11358   425595    37.5 |  0.904 % |
c |     17125 |  583443  1407598 |  554876   17125   547356    32.0 |  0.904 % |
c |     25776 |  583443  1407598 |  610364   25776   684102    26.5 |  0.904 % |
c |     38750 |  583415  1407535 |  671401   38749  1104497    28.5 |  0.908 % |
c |     58211 |  583415  1407535 |  738541   58210  3376357    58.0 |  0.908 % |
c ==============================================================================
c [1mFound solution: 28375981[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     60276 |  583840  1409800 |  194613   60275  3878676    64.3 |  0.908 % |
c |     60376 |  583840  1409800 |  214074   60375  3880940    64.3 |  0.907 % |
c |     60526 |  583840  1409800 |  235481   60525  3881787    64.1 |  0.907 % |
c |     60751 |  583840  1409800 |  259029   60750  3883229    63.9 |  0.907 % |
c |     61089 |  583840  1409800 |  284932   61088  3889071    63.7 |  0.907 % |
c |     61595 |  583840  1409800 |  313426   61594  3926603    63.7 |  0.907 % |
c ==============================================================================
c [1mFound solution: 24816772[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61873 |  585065  1412982 |  195021   61871  3931989    63.6 |  0.907 % |
c |     61974 |  584447  1411579 |  214523   61953  3933627    63.5 |  0.995 % |
c |     62125 |  584447  1411579 |  235975   62104  3934500    63.4 |  0.995 % |
c |     62350 |  584447  1411579 |  259572   62329  3935652    63.1 |  0.995 % |
c |     62688 |  584447  1411579 |  285530   62667  3938886    62.9 |  0.995 % |
c |     63197 |  584447  1411579 |  314083   63176  3945402    62.5 |  0.995 % |
c |     63956 |  584447  1411579 |  345491   63935  4004706    62.6 |  0.995 % |
c |     65095 |  584447  1411579 |  380040   65074  4018762    61.8 |  0.995 % |
c |     66803 |  584447  1411579 |  418044   66782  4047321    60.6 |  0.995 % |
c |     69370 |  584447  1411579 |  459849   69349  4255522    61.4 |  0.995 % |
c ==============================================================================
c [1mFound solution: 21398365[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72482 |  583645  1409871 |  194548   72448  4440136    61.3 |  0.995 % |
c |     72582 |  583645  1409871 |  214002   72548  4449525    61.3 |  1.170 % |
c |     72732 |  583645  1409871 |  235403   72698  4450570    61.2 |  1.170 % |
c |     72957 |  583645  1409871 |  258943   72923  4455689    61.1 |  1.170 % |
c |     73294 |  583645  1409871 |  284837   73260  4466941    61.0 |  1.170 % |
c |     73800 |  582656  1407609 |  313321   73749  4479333    60.7 |  1.309 % |
c |     74561 |  582338  1406892 |  344653   74507  4488034    60.2 |  1.351 % |
c |     75701 |  582247  1406687 |  379119   75644  4497377    59.5 |  1.364 % |
c |     77409 |  582247  1406687 |  417030   77352  4515035    58.4 |  1.364 % |
c |     79973 |  582247  1406687 |  458734   79916  4604044    57.6 |  1.364 % |
c |     83819 |  582247  1406687 |  504607   83762  4661862    55.7 |  1.364 % |
c |     89585 |  582247  1406687 |  555068   89528  4822383    53.9 |  1.364 % |
c ==============================================================================
c [1mFound solution: 10069151[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90154 |  583041  1408664 |  194347   90097  4883326    54.2 |  1.364 % |
c |     90254 |  583041  1408664 |  213781   90197  4888191    54.2 |  1.361 % |
c |     90404 |  583041  1408664 |  235159   90347  4889785    54.1 |  1.361 % |
c |     90629 |  583041  1408664 |  258675   90572  4896458    54.1 |  1.361 % |
c |     90966 |  583041  1408664 |  284543   90909  4932535    54.3 |  1.361 % |
c |     91474 |  583041  1408664 |  312997   91417  4969419    54.4 |  1.361 % |
c |     92233 |  583041  1408664 |  344297   92176  5081665    55.1 |  1.361 % |
c |     93372 |  583041  1408664 |  378727   93315  5154032    55.2 |  1.361 % |
c |     95080 |  583033  1408646 |  416600   95022  5611135    59.1 |  1.362 % |
c |     97642 |  583033  1408646 |  458260   97584  5776693    59.2 |  1.362 % |
c |    101489 |  582403  1407206 |  504086  101423  5921980    58.4 |  1.454 % |
c |    107255 |  582403  1407206 |  554494  107189  7795468    72.7 |  1.454 % |
c ==============================================================================
c [1mFound solution: 9209411[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    114951 |  580799  1403553 |  193599  114861  9013565    78.5 |  1.454 % |
c |    115051 |  580799  1403553 |  212958  114961  9019035    78.5 |  1.705 % |
c ==============================================================================
c [1mFound solution: 8956834[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    115144 |  580838  1403658 |  193612  115054  9033339    78.5 |  1.705 % |
c |    115245 |  580838  1403658 |  212973  115155  9034080    78.5 |  1.706 % |
c |    115395 |  580838  1403658 |  234270  115305  9035023    78.4 |  1.706 % |
c |    115620 |  579595  1400824 |  257697  115504  9036970    78.2 |  1.885 % |
c |    115958 |  579525  1400662 |  283467  115841  9044839    78.1 |  1.896 % |
c |    116464 |  578585  1398497 |  311814  116328  9068840    78.0 |  2.038 % |
c ==============================================================================
c [1mFound solution: 6455552[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    117113 |  579181  1399956 |  193060  116977  9161074    78.3 |  2.038 % |
c |    117213 |  579181  1399956 |  212366  117077  9168136    78.3 |  2.038 % |
c |    117366 |  579181  1399956 |  233602  117230  9179839    78.3 |  2.038 % |
c |    117592 |  579181  1399956 |  256962  117456  9195992    78.3 |  2.038 % |
c |    117931 |  578644  1398725 |  282659  117779  9218643    78.3 |  2.115 % |
c |    118437 |  578644  1398725 |  310925  118285  9318942    78.8 |  2.115 % |
c |    119197 |  578551  1398512 |  342017  119044  9354335    78.6 |  2.129 % |
c |    120337 |  578162  1397627 |  376219  120165  9404585    78.3 |  2.182 % |
c |    122045 |  577908  1397055 |  413841  121171  9636661    79.5 |  2.215 % |
c |    124607 |  577908  1397055 |  455225  123733 10024389    81.0 |  2.215 % |
c |    128453 |  577894  1397023 |  500747  127575 10582438    83.0 |  2.217 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 14736 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.92 0.98 0.91 2/54 14732
Raw data (stat): 14732 (runsolver) R 14731 21152 21151 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 796273888 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.93 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0007 s]
Raw data (loadavg): 0.94 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0005 s]
Raw data (loadavg): 0.95 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0009 s]
Raw data (loadavg): 0.96 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0012 s]
Raw data (loadavg): 0.96 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0011 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0023 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0028 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0027 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.003 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.111 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.112 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.112 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.112 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.112 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.119 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.13 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.138 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14736
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.144 s]
Raw data (loadavg): 1.15 1.02 0.93 3/58 14785
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.144 s]
Raw data (loadavg): 1.27 1.05 0.94 2/55 14789
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.144 s]
Raw data (loadavg): 1.23 1.05 0.94 2/55 14789
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.144 s]
Raw data (loadavg): 1.19 1.04 0.94 2/55 14789
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.144 s]
Raw data (loadavg): 1.16 1.04 0.94 2/55 14789
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.145 s]
Raw data (loadavg): 1.14 1.04 0.94 2/55 14789
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.144 s]
Raw data (loadavg): 1.12 1.04 0.94 2/55 14789
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.145 s]
Raw data (loadavg): 1.10 1.04 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.145 s]
Raw data (loadavg): 1.08 1.03 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.145 s]
Raw data (loadavg): 1.07 1.03 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.145 s]
Raw data (loadavg): 1.06 1.03 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.146 s]
Raw data (loadavg): 1.05 1.03 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.146 s]
Raw data (loadavg): 1.04 1.03 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.146 s]
Raw data (loadavg): 1.03 1.03 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.147 s]
Raw data (loadavg): 1.03 1.03 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.147 s]
Raw data (loadavg): 1.02 1.02 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.147 s]
Raw data (loadavg): 1.02 1.02 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.148 s]
Raw data (loadavg): 1.02 1.02 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.149 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.149 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.154 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.159 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.16 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.16 s]
Raw data (loadavg): 1.00 1.02 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.16 s]
Raw data (loadavg): 1.00 1.02 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.161 s]
Raw data (loadavg): 1.00 1.02 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.161 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.161 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.163 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.162 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.163 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.163 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.164 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.165 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.165 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.166 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.165 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14791
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.165 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.173 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.172 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.172 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.172 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.172 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.172 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.173 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.173 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.173 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.174 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.175 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.174 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.17 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.18 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.76 s]
Raw data (loadavg): 1.00 1.00 0.94 1/53 14793
Raw data (stat): 14732 (minisat+_script) S 14731 21152 21151 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796273888 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

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