PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/een/normalized-p0201.opb
MD5SUM	ff4eb45c2603a47e5b79b2649e926ba4
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1523
Optimality of the best value was proved	NO
Number of terms in the objective function	201
Biggest coefficient in the objective function	1920
Number of bits for the biggest coefficient in the objective function	11
Sum of the numbers in the objective function	19980
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	1920
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	19980
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01984
Number of variables	195
Total number of constraints	133
Number of constraints which are clauses	20
Number of constraints which are cardinality constraints (but not clauses)	26
Number of constraints which are nor clauses,nor cardinality constraints	87
Minimum length of a constraint	3
Maximum length of a constraint	65
Trace number 30595

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-05-25 17:56:23 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=21979 boxname=wulflinc27 idbench=397 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  ff4eb45c2603a47e5b79b2649e926ba4  /oldhome/oroussel/tmp/wulflinc27/normalized-p0201.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-p0201.opb
IDLAUNCH: 21979
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
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:        364540 kB
Buffers:         35004 kB
Cached:         613620 kB
SwapCached:        640 kB
Active:         107852 kB
Inactive:       543232 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        364288 kB
SwapTotal:     2097892 kB
SwapFree:      2096760 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5644 kB
Slab:            13456 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 18:16:53 (client local time) WITH STATUS 152 IN 1229.85 SECONDS
stats: 21979 7 1229.85 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 133 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################
c   -- Clauses(.)/Splits(s): .sssss
c ---[ 137]---> BDD-cost:    3
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    3
c ---[ 132]---> BDD-cost:    3
c ---[ 131]---> BDD-cost:    3
c ---[ 130]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    3
c ---[ 128]---> BDD-cost:   11
c ---[ 127]---> BDD-cost:   11
c ---[ 126]---> BDD-cost:   11
c ---[ 125]---> BDD-cost:   11
c ---[ 124]---> BDD-cost:   11
c ---[ 123]---> BDD-cost:   11
c ---[ 122]---> BDD-cost:   11
c ---[ 121]---> BDD-cost:   11
c ---[ 120]---> BDD-cost:   11
c ---[ 119]---> BDD-cost:   11
c ---[ 118]---> BDD-cost:   11
c ---[ 117]---> BDD-cost:   11
c ---[ 116]---> BDD-cost:   11
c ---[ 115]---> BDD-cost:   11
c ---[ 114]---> BDD-cost:   11
c ---[ 113]---> BDD-cost:   11
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   11
c ---[ 110]---> BDD-cost:   11
c ---[ 109]---> BDD-cost:   11
c ---[ 108]---> BDD-cost:   11
c ---[ 107]---> BDD-cost:   11
c ---[ 106]---> BDD-cost:   11
c ---[ 105]---> BDD-cost:   11
c ---[ 104]---> BDD-cost:   11
c ---[ 103]---> BDD-cost:   11
c ---[ 102]---> BDD-cost:   11
c ---[ 101]---> BDD-cost:   11
c ---[ 100]---> BDD-cost:   11
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:   11
c ---[  97]---> BDD-cost:   11
c ---[  96]---> BDD-cost:   11
c ---[  95]---> BDD-cost:   11
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   11
c ---[  89]---> BDD-cost:   11
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   11
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   11
c ---[  83]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   11
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   11
c ---[  78]---> BDD-cost:   11
c ---[  77]---> BDD-cost:   11
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   11
c ---[  72]---> BDD-cost:   13
c ---[  70]---> BDD-cost:   15
c ---[  68]---> BDD-cost:   15
c ---[  66]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   13
c ---[  62]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  58]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   13
c ---[  52]---> BDD-cost:   13
c ---[  50]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   13
c ---[  44]---> BDD-cost:   13
c ---[  42]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   13
c ---[  38]---> BDD-cost:   13
c ---[  36]---> BDD-cost:   13
c ---[  31]---> BDD-cost:   39
c ---[  28]---> BDD-cost:   54
c ---[  27]---> BDD-cost:   42
c ---[  26]---> BDD-cost:   42
c ---[  25]---> BDD-cost:   73
c ---[  24]---> BDD-cost:   73
c ---[  23]---> BDD-cost:   98
c ---[  22]---> BDD-cost:  160
c ---[  21]---> BDD-cost:   85
c ---[  20]---> BDD-cost:   85
c ---[  19]---> BDD-cost:  201
c ---[  18]---> BDD-cost:  107
c ---[  17]---> BDD-cost:  107
c ---[  16]---> BDD-cost:  241
c ---[  15]---> BDD-cost:  128
c ---[  14]---> BDD-cost:  128
c ---[  13]---> BDD-cost:  150
c ---[  12]---> BDD-cost:  150
c ---[  11]---> BDD-cost:  281
c ---[  10]---> BDD-cost:  321
c ---[   9]---> BDD-cost:  172
c ---[   8]---> BDD-cost:  172
c ---[   7]---> BDD-cost:  194
c ---[   6]---> BDD-cost:  194
c ---[   5]---> BDD-cost:  361
c ---[   4]---> BDD-cost:    1
c ---[   3]---> BDD-cost:    1
c ---[   2]---> BDD-cost:    1
c ---[   1]---> BDD-cost:    1
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   11741    34627 |    3913       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 2321[0m
c ---[   0]---> Sorter-cost:21987     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        22 |   60840   149261 |   20280      21      108     5.1 |  0.000 % |
c |       122 |   60771   149095 |   22308     116     9072    78.2 |  0.586 % |
c |       272 |   60333   148103 |   24538     263    10198    38.8 |  1.087 % |
c ==============================================================================
c [1mFound solution: 2304[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       464 |   59190   145572 |   19730     360    10756    29.9 |  1.087 % |
c |       564 |   56937   140394 |   21703     431    11589    26.9 |  6.067 % |
c |       715 |   56667   139775 |   23873     579    15674    27.1 |  6.418 % |
c |       940 |   56053   138362 |   26260     791    17405    22.0 |  7.522 % |
c ==============================================================================
c [1mFound solution: 2221[0m
c ---[   0]---> Sorter-cost:    1     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       973 |   55214   136433 |   18404     810    17568    21.7 |  7.522 % |
c |      1073 |   55078   136119 |   20244     909    31790    35.0 |  8.517 % |
c |      1223 |   53987   133608 |   22268    1036    32305    31.2 |  9.937 % |
c |      1452 |   53445   132352 |   24495    1232    40064    32.5 | 10.686 % |
c ==============================================================================
c [1mFound solution: 2166[0m
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1536 |   52668   130555 |   17556    1307    41474    31.7 | 10.686 % |
c |      1637 |   52668   130555 |   19311    1408    46677    33.2 | 11.681 % |
c |      1787 |   52668   130555 |   21242    1558    51594    33.1 | 11.682 % |
c ==============================================================================
c [1mFound solution: 2136[0m
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1825 |   52689   130614 |   17563    1596    52210    32.7 | 11.682 % |
c |      1925 |   52689   130614 |   19319    1696    54746    32.3 | 11.679 % |
c |      2080 |   52689   130614 |   21251    1851    60799    32.8 | 11.679 % |
c ==============================================================================
c [1mFound solution: 1963[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2126 |   52479   130144 |   17493    1888    62844    33.3 | 11.679 % |
c |      2226 |   52479   130144 |   19242    1988    64360    32.4 | 12.091 % |
c |      2377 |   52479   130144 |   21166    2139    70843    33.1 | 12.091 % |
c ==============================================================================
c [1mFound solution: 1959[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2471 |   52489   130172 |   17496    2233    72955    32.7 | 12.091 % |
c |      2571 |   52322   129787 |   19245    2328    74840    32.1 | 12.323 % |
c |      2721 |   51285   127390 |   21170    2429    80367    33.1 | 13.717 % |
c |      2947 |   50170   124809 |   23287    2621    85422    32.6 | 15.200 % |
c |      3287 |   48847   121747 |   25615    2911   101992    35.0 | 16.952 % |
c |      3793 |   48358   120612 |   28177    3403   113615    33.4 | 17.588 % |
c ==============================================================================
c [1mFound solution: 1948[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4119 |   48366   120631 |   16122    3729   137025    36.7 | 17.588 % |
c |      4219 |   48366   120631 |   17734    3829   138803    36.3 | 17.588 % |
c |      4369 |   48048   119892 |   19507    3958   145830    36.8 | 18.022 % |
c |      4594 |   46695   116764 |   21458    4091   147117    36.0 | 19.828 % |
c |      4932 |   46689   116746 |   23604    4428   161011    36.4 | 19.837 % |
c |      5439 |   46689   116746 |   25964    4935   174660    35.4 | 19.837 % |
c ==============================================================================
c [1mFound solution: 1939[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5595 |   46694   116758 |   15564    5091   183472    36.0 | 19.837 % |
c |      5695 |   46694   116758 |   17120    5191   187041    36.0 | 19.838 % |
c |      5846 |   46694   116758 |   18832    5342   193524    36.2 | 19.838 % |
c |      6071 |   46694   116758 |   20715    5567   199369    35.8 | 19.838 % |
c ==============================================================================
c [1mFound solution: 1935[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6244 |   46756   116908 |   15585    5740   205127    35.7 | 19.838 % |
c |      6346 |   46610   116564 |   17143    5837   209713    35.9 | 20.053 % |
c |      6496 |   46529   116378 |   18857    5981   213413    35.7 | 20.158 % |
c |      6721 |   46529   116378 |   20743    6206   228623    36.8 | 20.158 % |
c ==============================================================================
c [1mFound solution: 1931[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6870 |   44969   112759 |   14989    6212   230635    37.1 | 20.158 % |
c |      6971 |   44969   112759 |   16487    6313   236280    37.4 | 22.294 % |
c |      7121 |   44539   111755 |   18136    6433   238185    37.0 | 22.870 % |
c |      7348 |   44147   110835 |   19950    6616   255984    38.7 | 23.437 % |
c |      7687 |   44141   110817 |   21945    6953   266703    38.4 | 23.445 % |
c |      8195 |   44132   110790 |   24139    7455   285481    38.3 | 23.458 % |
c ==============================================================================
c [1mFound solution: 1924[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8652 |   43344   108952 |   14448    7850   318221    40.5 | 23.458 % |
c |      8753 |   43191   108593 |   15892    7939   320098    40.3 | 24.773 % |
c |      8903 |   43162   108520 |   17482    8088   328118    40.6 | 24.824 % |
c |      9130 |   43162   108520 |   19230    8315   335246    40.3 | 24.824 % |
c ==============================================================================
c [1mFound solution: 1914[0m
c ---[   0]---> Sorter-cost: 3291     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9281 |   45828   114675 |   15276    8466   342248    40.4 | 24.824 % |
c |      9382 |   45828   114675 |   16803    8567   345184    40.3 | 23.183 % |
c |      9532 |   45828   114675 |   18483    8717   356244    40.9 | 23.183 % |
c |      9757 |   45828   114675 |   20332    8942   380246    42.5 | 23.183 % |
c |     10096 |   45411   113705 |   22365    9242   389539    42.1 | 23.724 % |
c |     10604 |   45101   112977 |   24602    9691   417766    43.1 | 24.120 % |
c |     11364 |   45101   112977 |   27062   10451   459434    44.0 | 24.120 % |
c ==============================================================================
c [1mFound solution: 1909[0m
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11707 |   44947   112614 |   14982   10785   486650    45.1 | 24.120 % |
c |     11807 |   44926   112551 |   16480   10883   491738    45.2 | 24.394 % |
c |     11958 |   44926   112551 |   18128   11034   493878    44.8 | 24.394 % |
c |     12184 |   44926   112551 |   19941   11260   511699    45.4 | 24.394 % |
c ==============================================================================
c [1mFound solution: 1759[0m
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12229 |   44945   112599 |   14981   11305   512517    45.3 | 24.394 % |
c |     12332 |   44851   112382 |   16479   11400   515625    45.2 | 24.509 % |
c |     12483 |   44851   112382 |   18127   11551   525382    45.5 | 24.509 % |
c |     12708 |   44851   112382 |   19939   11776   530560    45.1 | 24.509 % |
c |     13046 |   44847   112373 |   21933   12112   554374    45.8 | 24.513 % |
c |     13553 |   44847   112373 |   24127   12619   586073    46.4 | 24.513 % |
c |     14312 |   44395   111348 |   26539   13291   609205    45.8 | 25.144 % |
c |     15452 |   44357   111261 |   29193   14408   672095    46.6 | 25.195 % |
c |     17160 |   44357   111261 |   32113   16116   732967    45.5 | 25.195 % |
c |     19724 |   44099   110658 |   35324   18624   917611    49.3 | 25.536 % |
c |     23568 |   43596   109488 |   38856   22420  1217299    54.3 | 26.195 % |
c ==============================================================================
c [1mFound solution: 1748[0m
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27185 |   43512   109291 |   14504   26028  1445048    55.5 | 26.195 % |
c |     27285 |   43512   109291 |   15954   13114   718324    54.8 | 26.347 % |
c |     27435 |   43512   109291 |   17549   13264   723440    54.5 | 26.347 % |
c |     27662 |   43512   109291 |   19304   13491   742053    55.0 | 26.347 % |
c |     28001 |   43457   109164 |   21235   13826   756100    54.7 | 26.418 % |
c |     28507 |   43457   109164 |   23358   14332   788988    55.1 | 26.418 % |
c |     29266 |   43457   109164 |   25694   15091   851678    56.4 | 26.418 % |
c |     30405 |   43457   109164 |   28264   16230   917258    56.5 | 26.418 % |
c |     32116 |   43445   109128 |   31090   17939  1028851    57.4 | 26.433 % |
c |     34678 |   43445   109128 |   34199   20501  1145720    55.9 | 26.433 % |
c |     38524 |   43445   109128 |   37619   24347  1331202    54.7 | 26.433 % |
c ==============================================================================
c [1mFound solution: 1744[0m
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40084 |   43451   109141 |   14483   25907  1413810    54.6 | 26.433 % |
c |     40184 |   43451   109141 |   15931   13054   485055    37.2 | 26.434 % |
c |     40334 |   43451   109141 |   17524   13204   494401    37.4 | 26.434 % |
c |     40560 |   43451   109141 |   19276   13430   510472    38.0 | 26.434 % |
c |     40897 |   43451   109141 |   21204   13767   528771    38.4 | 26.434 % |
c |     41405 |   43451   109141 |   23325   14275   562681    39.4 | 26.434 % |
c |     42165 |   43451   109141 |   25657   15035   600347    39.9 | 26.434 % |
c |     43307 |   43451   109141 |   28223   16177   663217    41.0 | 26.434 % |
c |     45017 |   42985   108057 |   31045   17876   742191    41.5 | 27.022 % |
c ==============================================================================
c [1mFound solution: 1736[0m
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45161 |   42991   108073 |   14330   18020   750130    41.6 | 27.022 % |
c |     45261 |   42991   108073 |   15763   18120   757033    41.8 | 27.022 % |
c |     45412 |   42991   108073 |   17339   18271   763489    41.8 | 27.022 % |
c |     45638 |   42991   108073 |   19073   18497   771489    41.7 | 27.022 % |
c |     45975 |   42991   108073 |   20980   18834   791375    42.0 | 27.022 % |
c |     46481 |   42987   108064 |   23078   19337   809336    41.9 | 27.026 % |
c |     47240 |   42987   108064 |   25386   20096   863745    43.0 | 27.026 % |
c |     48382 |   42987   108064 |   27925   21238   943746    44.4 | 27.026 % |
c ==============================================================================
c [1mFound solution: 1729[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49754 |   42993   108079 |   14331   22610  1015698    44.9 | 27.026 % |
c |     49859 |   42993   108079 |   15764   11410   419418    36.8 | 27.025 % |
c |     50010 |   42993   108079 |   17340   11561   424641    36.7 | 27.025 % |
c |     50235 |   42993   108079 |   19074   11786   438359    37.2 | 27.025 % |
c |     50573 |   42993   108079 |   20982   12124   460647    38.0 | 27.025 % |
c |     51079 |   42993   108079 |   23080   12630   483267    38.3 | 27.025 % |
c |     51838 |   42993   108079 |   25388   13389   517484    38.6 | 27.025 % |
c |     52980 |   42993   108079 |   27927   14531   578959    39.8 | 27.025 % |
c |     54689 |   42993   108079 |   30719   16240   670254    41.3 | 27.025 % |
c |     57253 |   42993   108079 |   33791   18804   805986    42.9 | 27.025 % |
c |     61097 |   42993   108079 |   37170   22648  1043110    46.1 | 27.025 % |
c |     66863 |   42984   108057 |   40888   28410  1338415    47.1 | 27.037 % |
c |     75512 |   42921   107897 |   44976   37050  2118376    57.2 | 27.123 % |
c ==============================================================================
c [1mFound solution: 1721[0m
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86999 |   42811   107624 |   14270   48513  2865417    59.1 | 27.123 % |
c |     87099 |   42811   107624 |   15697   18350   839087    45.7 | 27.265 % |
c |     87249 |   42811   107624 |   17266   18500   845161    45.7 | 27.265 % |
c ==============================================================================
c [1mFound solution: 1716[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87420 |   42818   107641 |   14272   18671   852903    45.7 | 27.265 % |
c |     87522 |   42818   107641 |   15699   18773   858915    45.8 | 27.263 % |
c |     87673 |   42818   107641 |   17269   18924   867102    45.8 | 27.263 % |
c ==============================================================================
c [1mFound solution: 1709[0m
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87754 |   42824   107655 |   14274   19005   873644    46.0 | 27.263 % |
c |     87854 |   42824   107655 |   15701   19105   878102    46.0 | 27.263 % |
c |     88006 |   42824   107655 |   17271   19257   883087    45.9 | 27.263 % |
c |     88231 |   42824   107655 |   18998   19482   899073    46.1 | 27.263 % |
c |     88568 |   42824   107655 |   20898   19819   907472    45.8 | 27.263 % |
c |     89074 |   42824   107655 |   22988   20325   927868    45.7 | 27.263 % |
c |     89835 |   42824   107655 |   25287   21086   959351    45.5 | 27.263 % |
c |     90975 |   42824   107655 |   27815   22226  1009265    45.4 | 27.263 % |
c |     92683 |   42812   107619 |   30597   23931  1116385    46.7 | 27.279 % |
c |     95247 |   42743   107460 |   33657   26491  1332738    50.3 | 27.365 % |
c ==============================================================================
c [1mFound solution: 1704[0m
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97966 |   42741   107458 |   14247   29207  1573586    53.9 | 27.365 % |
c |     98067 |   42501   106900 |   15671   14695   680378    46.3 | 27.689 % |
c |     98221 |   42501   106900 |   17238   14849   692647    46.6 | 27.689 % |
c |     98446 |   42501   106900 |   18962   15074   711042    47.2 | 27.689 % |
c |     98783 |   42501   106900 |   20859   15411   737707    47.9 | 27.689 % |
c |     99289 |   42501   106900 |   22944   15917   771236    48.5 | 27.689 % |
c |    100049 |   42395   106656 |   25239   16670   793350    47.6 | 27.823 % |
c ==============================================================================
c [1mFound solution: 1694[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    100789 |   42400   106668 |   14133   17410   820456    47.1 | 27.823 % |
c |    100891 |   42316   106471 |   15546   17506   822128    47.0 | 27.941 % |
c |    101041 |   42316   106471 |   17100   17656   830622    47.0 | 27.941 % |
c |    101266 |   42316   106471 |   18811   17881   833523    46.6 | 27.941 % |
c |    101603 |   42296   106424 |   20692   18216   854152    46.9 | 27.968 % |
c |    102109 |   42296   106424 |   22761   18722   881251    47.1 | 27.968 % |
c |    102869 |   42296   106424 |   25037   19482   923636    47.4 | 27.968 % |
c |    104008 |   42296   106424 |   27541   20621  1002974    48.6 | 27.968 % |
c |    105717 |   42201   106203 |   30295   22325  1112136    49.8 | 28.094 % |
c ==============================================================================
c [1mFound solution: 1691[0m
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    106698 |   42206   106214 |   14068   23306  1194126    51.2 | 28.094 % |
c |    106800 |   42206   106214 |   15474   11755   439579    37.4 | 28.094 % |
c |    106951 |   41960   105641 |   17022   11888   442183    37.2 | 28.419 % |
c |    107176 |   41960   105641 |   18724   12113   454948    37.6 | 28.419 % |
c |    107513 |   41960   105641 |   20596   12450   472512    38.0 | 28.419 % |
c ==============================================================================
c [1mFound solution: 1684[0m
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    107802 |   41965   105652 |   13988   12739   489211    38.4 | 28.419 % |
c |    107902 |   41965   105652 |   15386   12839   496709    38.7 | 28.419 % |
c |    108054 |   41959   105640 |   16925   12989   500059    38.5 | 28.427 % |
c |    108283 |   41794   105269 |   18618   12922   495216    38.3 | 28.635 % |
c |    108621 |   41735   105135 |   20479   13241   500692    37.8 | 28.705 % |
c |    109127 |   41732   105126 |   22527   13746   535569    39.0 | 28.709 % |
c |    109886 |   41732   105126 |   24780   14505   561412    38.7 | 28.709 % |
c |    111025 |   41726   105108 |   27258   15643   673525    43.1 | 28.717 % |
c |    112734 |   41102   103658 |   29984   17271   759767    44.0 | 29.546 % |
c ==============================================================================
c [1mFound solution: 1667[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    112862 |   41147   103764 |   13715   17399   768153    44.1 | 29.546 % |
c |    112962 |   41147   103764 |   15086   17499   771190    44.1 | 29.533 % |
c |    113112 |   41147   103764 |   16595   17649   775472    43.9 | 29.533 % |
c |    113338 |   41147   103764 |   18254   17875   782287    43.8 | 29.533 % |
c |    113676 |   41125   103714 |   20080   18207   795126    43.7 | 29.564 % |
c |    114182 |   41125   103714 |   22088   18713   822570    44.0 | 29.564 % |
c |    114943 |   41125   103714 |   24296   19474   860623    44.2 | 29.564 % |
c |    116083 |   41125   103714 |   26726   20614   921723    44.7 | 29.564 % |
c ==============================================================================
c [1mFound solution: 1663[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    117182 |   41130   103725 |   13710   21713   983432    45.3 | 29.564 % |
c |    117283 |   41130   103725 |   15081   10958   348621    31.8 | 29.566 % |
c |    117434 |   41130   103725 |   16589   11109   350539    31.6 | 29.566 % |
c |    117659 |   41130   103725 |   18248   11334   357808    31.6 | 29.566 % |
c |    117996 |   40870   103125 |   20072   11654   367895    31.6 | 29.882 % |
c |    118502 |   40870   103125 |   22080   12160   387551    31.9 | 29.882 % |
c |    119261 |   40870   103125 |   24288   12919   408418    31.6 | 29.882 % |
c ==============================================================================
c [1mFound solution: 1661[0m
c ---[   0]---> Sorter-cost:    1     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    119511 |   40884   103161 |   13628   13169   421521    32.0 | 29.882 % |
c |    119614 |   40741   102828 |   14990   13263   423078    31.9 | 30.071 % |
c |    119764 |   40741   102828 |   16489   13413   428871    32.0 | 30.071 % |
c |    119990 |   40741   102828 |   18138   13639   440457    32.3 | 30.071 % |
c |    120329 |   40741   102828 |   19952   13978   459794    32.9 | 30.071 % |
c |    120835 |   40741   102828 |   21948   14484   478929    33.1 | 30.071 % |
c |    121595 |   40741   102828 |   24142   15244   512143    33.6 | 30.071 % |
c |    122736 |   40741   102828 |   26557   16385   573126    35.0 | 30.071 % |
c |    124444 |   40741   102828 |   29212   18093   664548    36.7 | 30.071 % |
c |    127008 |   40741   102828 |   32134   20657   777134    37.6 | 30.071 % |
c ==============================================================================
c [1mFound solution: 1656[0m
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    130089 |   40745   102841 |   13581   23738   899116    37.9 | 30.071 % |
c |    130192 |   40745   102841 |   14939   11972   322953    27.0 | 30.071 % |
c |    130342 |   40745   102841 |   16433   12122   329170    27.2 | 30.071 % |
c |    130567 |   40745   102841 |   18076   12347   333628    27.0 | 30.072 % |
c |    130904 |   40745   102841 |   19883   12684   346118    27.3 | 30.072 % |
c |    131412 |   40745   102841 |   21872   13192   369164    28.0 | 30.072 % |
c |    132173 |   40745   102841 |   24059   13953   409035    29.3 | 30.071 % |
c |    133313 |   40725   102794 |   26465   15088   439980    29.2 | 30.099 % |
c |    135021 |   40715   102768 |   29112   16793   516035    30.7 | 30.114 % |
c ==============================================================================
c [1mFound solution: 1652[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    135571 |   40722   102793 |   13574   17343   537198    31.0 | 30.114 % |
c |    135673 |   40722   102793 |   14931   17445   543058    31.1 | 30.112 % |
c |    135824 |   40722   102793 |   16424   17596   547935    31.1 | 30.112 % |
c |    136051 |   40722   102793 |   18066   17823   558959    31.4 | 30.112 % |
c |    136388 |   40722   102793 |   19873   18160   570744    31.4 | 30.112 % |
c |    136900 |   40722   102793 |   21861   18672   606492    32.5 | 30.113 % |
c |    137659 |   40722   102793 |   24047   19431   650239    33.5 | 30.112 % |
c |    138801 |   40722   102793 |   26451   20573   705072    34.3 | 30.112 % |
c |    140509 |   40722   102793 |   29097   22281   792761    35.6 | 30.112 % |
c ==============================================================================
c [1mFound solution: 1651[0m
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    142457 |   40716   102777 |   13572   24224   905816    37.4 | 30.112 % |
c |    142557 |   40716   102777 |   14929   12212   387737    31.8 | 30.128 % |
c |    142707 |   40716   102777 |   16422   12362   392691    31.8 | 30.128 % |
c |    142933 |   40716   102777 |   18064   12588   399321    31.7 | 30.128 % |
c |    143270 |   40716   102777 |   19870   12925   415415    32.1 | 30.128 % |
c |    143776 |   40716   102777 |   21857   13431   436400    32.5 | 30.128 % |
c |    144537 |   40716   102777 |   24043   14192   469687    33.1 | 30.128 % |
c |    145676 |   40716   102777 |   26447   15331   521292    34.0 | 30.128 % |
c ==============================================================================
c [1mFound solution: 1644[0m
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    146892 |   40720   102787 |   13573   16547   575446    34.8 | 30.128 % |
c |    146995 |   40720   102787 |   14930   16650   581097    34.9 | 30.129 % |
c |    147146 |   40720   102787 |   16423   16801   582869    34.7 | 30.129 % |
c |    147371 |   40720   102787 |   18065   17026   591875    34.8 | 30.129 % |
c |    147712 |   40720   102787 |   19872   17367   600578    34.6 | 30.129 % |
c |    148219 |   40720   102787 |   21859   17874   617502    34.5 | 30.129 % |
c |    148978 |   40720   102787 |   24045   18633   648881    34.8 | 30.129 % |
c |    150117 |   40720   102787 |   26449   19772   710266    35.9 | 30.129 % |
c |    151825 |   40720   102787 |   29094   21480   785614    36.6 | 30.129 % |
c |    154387 |   40720   102787 |   32004   24042   880535    36.6 | 30.129 % |
c ==============================================================================
c [1mFound solution: 1642[0m
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    154777 |   40726   102802 |   13575   24432   906188    37.1 | 30.129 % |
c |    154877 |   40726   102802 |   14932   12316   335227    27.2 | 30.128 % |
c |    155027 |   40726   102802 |   16425   12466   342339    27.5 | 30.128 % |
c |    155252 |   40726   102802 |   18068   12691   355758    28.0 | 30.128 % |
c |    155590 |   40726   102802 |   19875   13029   368814    28.3 | 30.128 % |
c |    156099 |   40726   102802 |   21862   13538   389774    28.8 | 30.128 % |
c |    156858 |   40726   102802 |   24048   14297   425274    29.7 | 30.128 % |
c |    157997 |   40726   102802 |   26453   15436   460574    29.8 | 30.128 % |
c |    159706 |   40726   102802 |   29099   17145   510125    29.8 | 30.128 % |
c |    162272 |   40726   102802 |   32009   19711   608934    30.9 | 30.128 % |
c |    166116 |   40726   102802 |   35210   23555   759486    32.2 | 30.128 % |
c |    171882 |   40726   102802 |   38731   29321  1114603    38.0 | 30.128 % |
c |    180531 |   40726   102802 |   42604   37970  1447309    38.1 | 30.128 % |
c |    193506 |   40711   102757 |   46864   50940  2113661    41.5 | 30.148 % |
c ==============================================================================
c [1mFound solution: 1639[0m
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    195154 |   40714   102764 |   13571   52588  2224442    42.3 | 30.148 % |
c |    195255 |   40714   102764 |   14928   19845   732694    36.9 | 30.149 % |
c |    195408 |   40714   102764 |   16420   19998   741441    37.1 | 30.149 % |
c ==============================================================================
c [1mFound solution: 1631[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    195571 |   40720   102778 |   13573   20161   748582    37.1 | 30.149 % |
c |    195671 |   40720   102778 |   14930   20261   750087    37.0 | 30.148 % |
c |    195821 |   40714   102764 |   16423   20408   752993    36.9 | 30.156 % |
c |    196047 |   40714   102764 |   18065   20634   763296    37.0 | 30.156 % |
c |    196384 |   40714   102764 |   19872   20971   786775    37.5 | 30.156 % |
c |    196892 |   40714   102764 |   21859   21479   819658    38.2 | 30.156 % |
c |    197652 |   40708   102746 |   24045   22238   864204    38.9 | 30.164 % |
c |    198792 |   40708   102746 |   26449   23378   920169    39.4 | 30.164 % |
c |    200501 |   40708   102746 |   29094   25087  1032119    41.1 | 30.164 % |
c |    203063 |   40708   102746 |   32004   27649  1212199    43.8 | 30.164 % |
c |    206908 |   40708   102746 |   35204   31494  1422349    45.2 | 30.164 % |
c |    212675 |   40708   102746 |   38725   37261  1761049    47.3 | 30.164 % |
c |    221324 |   40708   102746 |   42597   45910  2183773    47.6 | 30.164 % |
c |    234298 |   40652   102615 |   46857   25366   975711    38.5 | 30.234 % |
c ==============================================================================
c [1mFound solution: 1623[0m
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    248606 |   40658   102629 |   13552   39674  2053944    51.8 | 30.234 % |
c |    248706 |   40516   102298 |   14907   16548  1008096    60.9 | 30.421 % |
c |    248858 |   40516   102298 |   16397   16700  1013335    60.7 | 30.421 % |
c |    249083 |   40513   102289 |   18037   16923  1023539    60.5 | 30.424 % |
c |    249421 |   40513   102289 |   19841   17261  1032090    59.8 | 30.424 % |
c |    249928 |   40513   102289 |   21825   17768  1050100    59.1 | 30.424 % |
c |    250689 |   40513   102289 |   24008   18529  1075792    58.1 | 30.424 % |
c |    251829 |   40513   102289 |   26409   19669  1120189    57.0 | 30.424 % |
c |    253537 |   40352   101910 |   29049   21357  1252590    58.7 | 30.647 % |
c |    256100 |   40352   101910 |   31954   23920  1396669    58.4 | 30.647 % |
c |    259945 |   40352   101910 |   35150   27765  1641354    59.1 | 30.647 % |
c |    265711 |   40352   101910 |   38665   33531  1958634    58.4 | 30.647 % |
c |    274360 |   40352   101910 |   42531   42180  2471283    58.6 | 30.647 % |
c |    287334 |   40342   101886 |   46785   21232   859949    40.5 | 30.662 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 20446 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.95 0.97 2/54 20442
Raw data (stat): 20442 (runsolver) R 20441 3394 3393 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 840842915 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.93 0.95 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0017 s]
Raw data (loadavg): 0.94 0.96 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0022 s]
Raw data (loadavg): 0.95 0.96 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0024 s]
Raw data (loadavg): 0.96 0.96 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0032 s]
Raw data (loadavg): 0.96 0.96 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0043 s]
Raw data (loadavg): 0.97 0.96 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0054 s]
Raw data (loadavg): 0.97 0.96 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0066 s]
Raw data (loadavg): 0.98 0.96 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s]
Raw data (loadavg): 0.98 0.96 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s]
Raw data (loadavg): 0.98 0.96 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.007 s]
Raw data (loadavg): 0.98 0.96 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 20446
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/56 20447
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.013 s]
Raw data (loadavg): 1.07 0.99 0.97 2/55 20499
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.013 s]
Raw data (loadavg): 1.06 0.99 0.97 2/55 20499
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s]
Raw data (loadavg): 1.05 0.99 0.97 2/55 20499
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s]
Raw data (loadavg): 1.04 0.99 0.97 2/55 20499
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.015 s]
Raw data (loadavg): 1.03 0.99 0.97 2/55 20499
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s]
Raw data (loadavg): 1.03 0.99 0.97 2/55 20499
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s]
Raw data (loadavg): 1.02 0.99 0.97 2/55 20499
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s]
Raw data (loadavg): 1.02 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s]
Raw data (loadavg): 1.02 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.015 s]
Raw data (loadavg): 1.01 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.016 s]
Raw data (loadavg): 1.01 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.015 s]
Raw data (loadavg): 1.01 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.015 s]
Raw data (loadavg): 1.01 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.015 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.016 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.016 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.015 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.016 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.016 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.018 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.018 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.024 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.024 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.024 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.097 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.097 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.098 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.105 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.105 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.105 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20501
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.106 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.106 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.106 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.11 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.109 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.11 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.112 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.112 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.112 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.112 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.112 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.112 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.112 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.113 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.113 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.114 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.113 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.113 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.113 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.113 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.114 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.114 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.113 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.113 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.113 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.114 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.114 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.114 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.114 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.114 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.115 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.116 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.115 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.115 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.116 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.117 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.117 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.117 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.117 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.117 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.118 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.119 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.119 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.13 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.13 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.13 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.13 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.13 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.13 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.13 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.13 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.13 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.13 s]
Raw data (loadavg): 1.00 0.99 0.97 2/55 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.7 s]
Raw data (loadavg): 1.00 0.99 0.97 1/53 20503
Raw data (stat): 20442 (minisat+_script) S 20441 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840842915 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.7
CPU time (s): 1229.85
CPU user time (s): 1229.48
CPU system time (s): 0.371943
CPU usage (%): 100.013
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####