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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Namesubmitted/een/normalized-p0201.opb
MD5SUMff4eb45c2603a47e5b79b2649e926ba4
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1523
Optimality of the best value was proved YES
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 numbers15
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark221.9
Number of variables195
Total number of constraints133
Number of constraints which are clauses20
Number of constraints which are cardinality constraints (but not clauses)26
Number of constraints which are nor clauses,nor cardinality constraints87
Minimum length of a constraint3
Maximum length of a constraint65

Trace number 2268

Launcher Data

LAUNCH ON wulflinc5 THE 2005-09-18 18:25:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2625 boxname=wulflinc5 idbench=281 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ff4eb45c2603a47e5b79b2649e926ba4  /oldhome/oroussel/tmp/wulflinc5/normalized-p0201.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-p0201.opb
IDLAUNCH: 2625
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        917876 kB
Buffers:         33892 kB
Cached:          59440 kB
SwapCached:        780 kB
Active:          59456 kB
Inactive:        36588 kB
HighTotal:      131008 kB
HighFree:        67928 kB
LowTotal:       903652 kB
LowFree:        849948 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5804 kB
Slab:            15216 kB
Committed_AS:    64264 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 18:45:19 (client local time) WITH STATUS 10 IN 1209.72 SECONDS
stats: 2625 7 1209.72 10

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 Found solution: 2321
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 Found solution: 2304
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 Found solution: 2221
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 Found solution: 2166
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 Found solution: 2136
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 Found solution: 1963
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 Found solution: 1959
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 Found solution: 1948
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 Found solution: 1939
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 Found solution: 1935
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 Found solution: 1931
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 Found solution: 1924
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 Found solution: 1914
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 Found solution: 1909
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 Found solution: 1759
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 Found solution: 1748
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 Found solution: 1744
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 Found solution: 1736
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 Found solution: 1729
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 Found solution: 1721
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 Found solution: 1716
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 Found solution: 1709
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 Found solution: 1704
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 Found solution: 1694
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 Found solution: 1691
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 Found solution: 1684
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 Found solution: 1667
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 Found solution: 1663
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 Found solution: 1661
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 Found solution: 1656
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 Found solution: 1652
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 Found solution: 1651
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 Found solution: 1644
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 Found solution: 1642
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 Found solution: 1639
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 Found solution: 1631
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 Found solution: 1623
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 % |

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/12218/stat): 12218 (minisat+_script) R 12217 12218 824 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785174303 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/12218/statm): 174 3 169 147 0 27 0
[pid=12218] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=12219
New process pid=12220
New process pid=12221
execve syscall for /bin/sed executable
One traced child (pid=12220) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=12221) exited with status: 0
One traced child (pid=12219) exited with status: 0
New process pid=12222
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-p0201.opb

[startup+10.0039 s]
Raw data (loadavg): 0.93 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 2240 0 0 0 979 8 0 0 25 0 1 0 1785174308 9809920 2174 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12222/statm): 2395 2174 145 145 0 2250 0
[pid=12222] vsize: 9580
Current children cumulated CPU time (s) 9.87
Current children cumulated vsize (Kb) 11704

[startup+20.0057 s]
Raw data (loadavg): 0.94 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 2380 0 0 0 1976 9 0 0 25 0 1 0 1785174308 10383360 2314 4294967295 134512640 135094434 3221224448 3221223108 134553499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 2535 2314 145 145 0 2390 0
[pid=12222] vsize: 10140
Current children cumulated CPU time (s) 19.85
Current children cumulated vsize (Kb) 12264

[startup+30.0064 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 2637 0 0 0 2972 10 0 0 25 0 1 0 1785174308 11296768 2571 4294967295 134512640 135094434 3221224448 3221223108 134553489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 2758 2571 145 145 0 2613 0
[pid=12222] vsize: 11032
Current children cumulated CPU time (s) 29.82
Current children cumulated vsize (Kb) 13156

[startup+40.0071 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 2851 0 0 0 3969 12 0 0 25 0 1 0 1785174308 12136448 2785 4294967295 134512640 135094434 3221224448 3221223040 134557514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 2963 2785 145 145 0 2818 0
[pid=12222] vsize: 11852
Current children cumulated CPU time (s) 39.81
Current children cumulated vsize (Kb) 13976

[startup+50.0079 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3041 0 0 0 4965 13 0 0 25 0 1 0 1785174308 12914688 2975 4294967295 134512640 135094434 3221224448 3221223104 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 3153 2975 145 145 0 3008 0
[pid=12222] vsize: 12612
Current children cumulated CPU time (s) 49.78
Current children cumulated vsize (Kb) 14736

[startup+60.0076 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3254 0 0 0 5962 14 0 0 25 0 1 0 1785174308 13840384 3188 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 3379 3188 145 145 0 3234 0
[pid=12222] vsize: 13516
Current children cumulated CPU time (s) 59.76
Current children cumulated vsize (Kb) 15640

[startup+70.0083 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3514 0 0 0 6955 17 0 0 25 0 1 0 1785174308 14893056 3448 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 3636 3448 145 145 0 3491 0
[pid=12222] vsize: 14544
Current children cumulated CPU time (s) 69.72
Current children cumulated vsize (Kb) 16668

[startup+80.0091 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3731 0 0 0 7950 19 0 0 25 0 1 0 1785174308 15773696 3665 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 3851 3665 145 145 0 3706 0
[pid=12222] vsize: 15404
Current children cumulated CPU time (s) 79.69
Current children cumulated vsize (Kb) 17528

[startup+90.0098 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3896 0 0 0 8948 20 0 0 25 0 1 0 1785174308 16441344 3830 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 4014 3830 145 145 0 3869 0
[pid=12222] vsize: 16056
Current children cumulated CPU time (s) 89.68
Current children cumulated vsize (Kb) 18180

[startup+100.011 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3896 0 0 0 9948 20 0 0 25 0 1 0 1785174308 16441344 3830 4294967295 134512640 135094434 3221224448 3221223072 134557681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 4014 3830 145 145 0 3869 0
[pid=12222] vsize: 16056
Current children cumulated CPU time (s) 99.68
Current children cumulated vsize (Kb) 18180

[startup+110.011 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3896 0 0 0 10949 20 0 0 25 0 1 0 1785174308 16441344 3830 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 4014 3830 145 145 0 3869 0
[pid=12222] vsize: 16056
Current children cumulated CPU time (s) 109.69
Current children cumulated vsize (Kb) 18180

[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3896 0 0 0 11949 20 0 0 25 0 1 0 1785174308 16441344 3830 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 4014 3830 145 145 0 3869 0
[pid=12222] vsize: 16056
Current children cumulated CPU time (s) 119.69
Current children cumulated vsize (Kb) 18180

[startup+130.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3896 0 0 0 12949 20 0 0 25 0 1 0 1785174308 16441344 3830 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 4014 3830 145 145 0 3869 0
[pid=12222] vsize: 16056
Current children cumulated CPU time (s) 129.69
Current children cumulated vsize (Kb) 18180

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3938 0 0 0 13949 20 0 0 25 0 1 0 1785174308 16613376 3872 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 4056 3872 145 145 0 3911 0
[pid=12222] vsize: 16224
Current children cumulated CPU time (s) 139.69
Current children cumulated vsize (Kb) 18348

[startup+150.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3938 0 0 0 14949 20 0 0 25 0 1 0 1785174308 16613376 3872 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 4056 3872 145 145 0 3911 0
[pid=12222] vsize: 16224
Current children cumulated CPU time (s) 149.69
Current children cumulated vsize (Kb) 18348

[startup+160.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3938 0 0 0 15949 20 0 0 25 0 1 0 1785174308 16613376 3872 4294967295 134512640 135094434 3221224448 3221223104 134558284 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 4056 3872 145 145 0 3911 0
[pid=12222] vsize: 16224
Current children cumulated CPU time (s) 159.69
Current children cumulated vsize (Kb) 18348

[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3938 0 0 0 16949 20 0 0 25 0 1 0 1785174308 16613376 3872 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 4056 3872 145 145 0 3911 0
[pid=12222] vsize: 16224
Current children cumulated CPU time (s) 169.69
Current children cumulated vsize (Kb) 18348

[startup+180.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3948 0 0 0 17949 20 0 0 25 0 1 0 1785174308 16654336 3882 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 4066 3882 145 145 0 3921 0
[pid=12222] vsize: 16264
Current children cumulated CPU time (s) 179.69
Current children cumulated vsize (Kb) 18388

[startup+190.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3948 0 0 0 18950 20 0 0 25 0 1 0 1785174308 16654336 3882 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 4066 3882 145 145 0 3921 0
[pid=12222] vsize: 16264
Current children cumulated CPU time (s) 189.7
Current children cumulated vsize (Kb) 18388

[startup+200.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3948 0 0 0 19950 20 0 0 25 0 1 0 1785174308 16654336 3882 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 4066 3882 145 145 0 3921 0
[pid=12222] vsize: 16264
Current children cumulated CPU time (s) 199.7
Current children cumulated vsize (Kb) 18388

[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3948 0 0 0 20950 20 0 0 25 0 1 0 1785174308 16654336 3882 4294967295 134512640 135094434 3221224448 3221223076 134557564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 4066 3882 145 145 0 3921 0
[pid=12222] vsize: 16264
Current children cumulated CPU time (s) 209.7
Current children cumulated vsize (Kb) 18388

[startup+220.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3948 0 0 0 21950 20 0 0 25 0 1 0 1785174308 16654336 3882 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 4066 3882 145 145 0 3921 0
[pid=12222] vsize: 16264
Current children cumulated CPU time (s) 219.7
Current children cumulated vsize (Kb) 18388

[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3948 0 0 0 22951 20 0 0 25 0 1 0 1785174308 16654336 3882 4294967295 134512640 135094434 3221224448 3221223072 134557648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 4066 3882 145 145 0 3921 0
[pid=12222] vsize: 16264
Current children cumulated CPU time (s) 229.71
Current children cumulated vsize (Kb) 18388

[startup+240.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3950 0 0 0 23951 20 0 0 25 0 1 0 1785174308 16654336 3884 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 4066 3884 145 145 0 3921 0
[pid=12222] vsize: 16264
Current children cumulated CPU time (s) 239.71
Current children cumulated vsize (Kb) 18388

[startup+250.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 4064 0 0 0 24949 21 0 0 25 0 1 0 1785174308 17113088 3998 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 4178 3998 145 145 0 4033 0
[pid=12222] vsize: 16712
Current children cumulated CPU time (s) 249.7
Current children cumulated vsize (Kb) 18836

[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 4297 0 0 0 25944 23 0 0 25 0 1 0 1785174308 18059264 4231 4294967295 134512640 135094434 3221224448 3221223040 134557044 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 4409 4231 145 145 0 4264 0
[pid=12222] vsize: 17636
Current children cumulated CPU time (s) 259.67
Current children cumulated vsize (Kb) 19760

[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 4530 0 0 0 26941 24 0 0 25 0 1 0 1785174308 19140608 4464 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 4673 4464 145 145 0 4528 0
[pid=12222] vsize: 18692
Current children cumulated CPU time (s) 269.65
Current children cumulated vsize (Kb) 20816

[startup+280.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) T 12218 12218 824 0 -1 0 4740 0 0 0 27938 26 0 0 25 0 1 0 1785174308 19992576 4674 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/12222/statm): 4881 4674 145 145 0 4736 0
[pid=12222] vsize: 19524
Current children cumulated CPU time (s) 279.64
Current children cumulated vsize (Kb) 21648

[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 4921 0 0 0 28935 28 0 0 25 0 1 0 1785174308 20750336 4855 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5066 4855 145 145 0 4921 0
[pid=12222] vsize: 20264
Current children cumulated CPU time (s) 289.63
Current children cumulated vsize (Kb) 22388

[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5095 0 0 0 29932 29 0 0 25 0 1 0 1785174308 21454848 5029 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5238 5029 145 145 0 5093 0
[pid=12222] vsize: 20952
Current children cumulated CPU time (s) 299.61
Current children cumulated vsize (Kb) 23076

[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5230 0 0 0 30930 30 0 0 25 0 1 0 1785174308 21995520 5164 4294967295 134512640 135094434 3221224448 3221223072 134562068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5370 5164 145 145 0 5225 0
[pid=12222] vsize: 21480
Current children cumulated CPU time (s) 309.6
Current children cumulated vsize (Kb) 23604

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5347 0 0 0 31928 31 0 0 25 0 1 0 1785174308 22478848 5281 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5488 5281 145 145 0 5343 0
[pid=12222] vsize: 21952
Current children cumulated CPU time (s) 319.59
Current children cumulated vsize (Kb) 24076

[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5485 0 0 0 32926 32 0 0 25 0 1 0 1785174308 23040000 5419 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5625 5419 145 145 0 5480 0
[pid=12222] vsize: 22500
Current children cumulated CPU time (s) 329.58
Current children cumulated vsize (Kb) 24624

[startup+340.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 33923 33 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 339.56
Current children cumulated vsize (Kb) 25272

[startup+350.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 34923 33 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 349.56
Current children cumulated vsize (Kb) 25272

[startup+360.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 35923 33 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 359.56
Current children cumulated vsize (Kb) 25272

[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 36922 33 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 369.55
Current children cumulated vsize (Kb) 25272

[startup+380.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 37923 33 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 379.56
Current children cumulated vsize (Kb) 25272

[startup+390.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 38923 33 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 389.56
Current children cumulated vsize (Kb) 25272

[startup+400.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 39923 34 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 399.57
Current children cumulated vsize (Kb) 25272

[startup+410.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 40923 34 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 409.57
Current children cumulated vsize (Kb) 25272

[startup+420.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 41923 34 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 419.57
Current children cumulated vsize (Kb) 25272

[startup+430.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 42923 34 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 429.57
Current children cumulated vsize (Kb) 25272

[startup+440.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 43924 34 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 439.58
Current children cumulated vsize (Kb) 25272

[startup+450.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 44924 34 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 449.58
Current children cumulated vsize (Kb) 25272

[startup+460.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5651 0 0 0 45924 34 0 0 25 0 1 0 1785174308 23703552 5585 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5585 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 459.58
Current children cumulated vsize (Kb) 25272

[startup+470.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5651 0 0 0 46924 34 0 0 25 0 1 0 1785174308 23703552 5585 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5585 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 469.58
Current children cumulated vsize (Kb) 25272

[startup+480.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5651 0 0 0 47924 34 0 0 25 0 1 0 1785174308 23703552 5585 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5585 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 479.58
Current children cumulated vsize (Kb) 25272

[startup+490.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5651 0 0 0 48924 34 0 0 25 0 1 0 1785174308 23703552 5585 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5585 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 489.58
Current children cumulated vsize (Kb) 25272

[startup+500.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 49924 34 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223072 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 499.58
Current children cumulated vsize (Kb) 25272

[startup+510.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 50924 34 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223104 134561460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 509.58
Current children cumulated vsize (Kb) 25272

[startup+520.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 51924 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 519.59
Current children cumulated vsize (Kb) 25272

[startup+530.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 52924 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 529.59
Current children cumulated vsize (Kb) 25272

[startup+540.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 53925 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 539.6
Current children cumulated vsize (Kb) 25272

[startup+550.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 54925 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 549.6
Current children cumulated vsize (Kb) 25272

[startup+560.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 55925 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 559.6
Current children cumulated vsize (Kb) 25272

[startup+570.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 56925 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 569.6
Current children cumulated vsize (Kb) 25272

[startup+580.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 57925 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 579.6
Current children cumulated vsize (Kb) 25272

[startup+590.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 58925 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223040 134557334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 589.6
Current children cumulated vsize (Kb) 25272

[startup+600.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 59926 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223120 134556487 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 599.61
Current children cumulated vsize (Kb) 25272

[startup+610.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 60926 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 609.61
Current children cumulated vsize (Kb) 25272

[startup+620.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 61926 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 619.61
Current children cumulated vsize (Kb) 25272

[startup+630.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 62926 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 629.61
Current children cumulated vsize (Kb) 25272

[startup+640.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 63927 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223104 134558284 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 639.62
Current children cumulated vsize (Kb) 25272

[startup+650.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 64927 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 649.62
Current children cumulated vsize (Kb) 25272

[startup+660.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 65927 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 659.62
Current children cumulated vsize (Kb) 25272

[startup+670.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 66927 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223136 134554744 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 669.62
Current children cumulated vsize (Kb) 25272

[startup+680.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 67927 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 679.62
Current children cumulated vsize (Kb) 25272

[startup+690.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5653 0 0 0 68928 35 0 0 25 0 1 0 1785174308 23703552 5587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5587 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 689.63
Current children cumulated vsize (Kb) 25272

[startup+700.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5653 0 0 0 69928 35 0 0 25 0 1 0 1785174308 23703552 5587 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5587 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 699.63
Current children cumulated vsize (Kb) 25272

[startup+710.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5653 0 0 0 70928 35 0 0 25 0 1 0 1785174308 23703552 5587 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5587 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 709.63
Current children cumulated vsize (Kb) 25272

[startup+720.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5654 0 0 0 71929 35 0 0 25 0 1 0 1785174308 23703552 5588 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5588 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 719.64
Current children cumulated vsize (Kb) 25272

[startup+730.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5657 0 0 0 72929 35 0 0 25 0 1 0 1785174308 23703552 5591 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5591 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 729.64
Current children cumulated vsize (Kb) 25272

[startup+740.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5657 0 0 0 73929 35 0 0 25 0 1 0 1785174308 23703552 5591 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5591 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 739.64
Current children cumulated vsize (Kb) 25272

[startup+750.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5658 0 0 0 74929 35 0 0 25 0 1 0 1785174308 23703552 5592 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5592 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 749.64
Current children cumulated vsize (Kb) 25272

[startup+760.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5660 0 0 0 75930 35 0 0 25 0 1 0 1785174308 23703552 5594 4294967295 134512640 135094434 3221224448 3221223040 134557236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5594 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 759.65
Current children cumulated vsize (Kb) 25272

[startup+770.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 76930 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 769.65
Current children cumulated vsize (Kb) 25272

[startup+780.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 77930 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 779.65
Current children cumulated vsize (Kb) 25272

[startup+790.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 78930 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 789.65
Current children cumulated vsize (Kb) 25272

[startup+800.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 79930 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223040 134556961 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 799.65
Current children cumulated vsize (Kb) 25272

[startup+810.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 80931 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 809.66
Current children cumulated vsize (Kb) 25272

[startup+820.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 81931 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 819.66
Current children cumulated vsize (Kb) 25272

[startup+830.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 82931 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 829.66
Current children cumulated vsize (Kb) 25272

[startup+840.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 83931 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 839.66
Current children cumulated vsize (Kb) 25272

[startup+850.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 84932 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 849.67
Current children cumulated vsize (Kb) 25272

[startup+860.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 85932 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 859.67
Current children cumulated vsize (Kb) 25272

[startup+870.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 86932 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134558254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 869.67
Current children cumulated vsize (Kb) 25272

[startup+880.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 87932 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 879.68
Current children cumulated vsize (Kb) 25272

[startup+890.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 88932 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 889.68
Current children cumulated vsize (Kb) 25272

[startup+900.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 89933 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 899.69
Current children cumulated vsize (Kb) 25272

[startup+910.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 90933 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 909.69
Current children cumulated vsize (Kb) 25272

[startup+920.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 91933 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 919.69
Current children cumulated vsize (Kb) 25272

[startup+930.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 92933 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 929.69
Current children cumulated vsize (Kb) 25272

[startup+940.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 93934 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223072 134557645 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 939.7
Current children cumulated vsize (Kb) 25272

[startup+950.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 94934 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 949.7
Current children cumulated vsize (Kb) 25272

[startup+960.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 95934 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 959.7
Current children cumulated vsize (Kb) 25272

[startup+970.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 96934 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 969.7
Current children cumulated vsize (Kb) 25272

[startup+980.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 97935 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223040 134557310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 979.71
Current children cumulated vsize (Kb) 25272

[startup+990.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 98935 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 989.71
Current children cumulated vsize (Kb) 25272

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 99935 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 999.71
Current children cumulated vsize (Kb) 25272

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 100935 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 1009.71
Current children cumulated vsize (Kb) 25272

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 101936 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223040 134557287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 1019.72
Current children cumulated vsize (Kb) 25272

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 102936 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 1029.72
Current children cumulated vsize (Kb) 25272

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 103936 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223040 134557208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 1039.72
Current children cumulated vsize (Kb) 25272

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 104936 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 1049.72
Current children cumulated vsize (Kb) 25272

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 105936 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223040 134556902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 1059.72
Current children cumulated vsize (Kb) 25272

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 106937 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223120 134556309 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 1069.73
Current children cumulated vsize (Kb) 25272

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 107937 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223040 134557236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 1079.73
Current children cumulated vsize (Kb) 25272

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 108937 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 1089.73
Current children cumulated vsize (Kb) 25272

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 109937 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 1099.73
Current children cumulated vsize (Kb) 25272

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 110937 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 1109.73
Current children cumulated vsize (Kb) 25272

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 111938 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 1119.74
Current children cumulated vsize (Kb) 25272

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 112938 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0
[pid=12222] vsize: 23148
Current children cumulated CPU time (s) 1129.74
Current children cumulated vsize (Kb) 25272

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5732 0 0 0 113936 37 0 0 25 0 1 0 1785174308 23990272 5666 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5857 5666 145 145 0 5712 0
[pid=12222] vsize: 23428
Current children cumulated CPU time (s) 1139.73
Current children cumulated vsize (Kb) 25552

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5859 0 0 0 114934 38 0 0 25 0 1 0 1785174308 24510464 5793 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 5984 5793 145 145 0 5839 0
[pid=12222] vsize: 23936
Current children cumulated CPU time (s) 1149.72
Current children cumulated vsize (Kb) 26060

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5989 0 0 0 115933 38 0 0 25 0 1 0 1785174308 25042944 5923 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 6114 5923 145 145 0 5969 0
[pid=12222] vsize: 24456
Current children cumulated CPU time (s) 1159.71
Current children cumulated vsize (Kb) 26580

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 6086 0 0 0 116932 38 0 0 25 0 1 0 1785174308 25440256 6020 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 6211 6020 145 145 0 6066 0
[pid=12222] vsize: 24844
Current children cumulated CPU time (s) 1169.7
Current children cumulated vsize (Kb) 26968

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 6175 0 0 0 117930 39 0 0 25 0 1 0 1785174308 25817088 6109 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 6303 6109 145 145 0 6158 0
[pid=12222] vsize: 25212
Current children cumulated CPU time (s) 1179.69
Current children cumulated vsize (Kb) 27336

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 6190 0 0 0 118930 39 0 0 25 0 1 0 1785174308 25878528 6124 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 6318 6124 145 145 0 6173 0
[pid=12222] vsize: 25272
Current children cumulated CPU time (s) 1189.69
Current children cumulated vsize (Kb) 27396

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 6196 0 0 0 119930 39 0 0 25 0 1 0 1785174308 25907200 6130 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 6325 6130 145 145 0 6180 0
[pid=12222] vsize: 25300
Current children cumulated CPU time (s) 1199.69
Current children cumulated vsize (Kb) 27424

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 6204 0 0 0 120930 39 0 0 25 0 1 0 1785174308 25939968 6138 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 6333 6138 145 145 0 6188 0
[pid=12222] vsize: 25332
Current children cumulated CPU time (s) 1209.69
Current children cumulated vsize (Kb) 27456



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12222
Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12218/statm): 531 226 485 147 0 384 0
[pid=12218] vsize: 2124
Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 6204 0 0 0 120930 39 0 0 25 0 1 0 1785174308 25939968 6138 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12222/statm): 6333 6138 145 145 0 6188 0
[pid=12222] vsize: 25332
Current children cumulated CPU time (s) 1209.69
Current children cumulated vsize (Kb) 27456

Sending SIGTERM to -12218
Sleeping 2 seconds
One traced child (pid=12218) ended because it received signal 15 (SIGTERM)
One traced child (pid=12222) exited with status: 10
All traced children have exited ! Game is over.

Child status: 10
Real time (s): 1210.12
CPU time (s): 1209.72
CPU user time (s): 1209.31
CPU system time (s): 0.412937
CPU usage (%): 99.967
Max. virtual memory (cumulated for all children) (Kb): 27456

Verifier Data

ERROR: no interpretation found !