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

Nameweb/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:20:4.5:0.95:100.opb
MD5SUMf82b685b64af240616b701a750c82883
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 11
Optimality of the best value was proved NO
Number of terms in the objective function 934
Biggest coefficient in the objective function 546
Number of bits for the biggest coefficient in the objective function 10
Sum of the numbers in the objective function 2594
Number of bits of the sum of numbers in the objective function 12
Biggest number in a constraint 546
Number of bits of the biggest number in a constraint 10
Biggest sum of numbers in a constraint 2594
Number of bits of the biggest sum of numbers12
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1226.18
Number of variables934
Total number of constraints1996
Number of constraints which are clauses879
Number of constraints which are cardinality constraints (but not clauses)1117
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint20

Trace number 2602

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        903384 kB
Buffers:         34844 kB
Cached:          68456 kB
SwapCached:        536 kB
Active:          67172 kB
Inactive:        38652 kB
HighTotal:      131008 kB
HighFree:        60620 kB
LowTotal:       903652 kB
LowFree:        842764 kB
SwapTotal:     2097892 kB
SwapFree:      2096832 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5864 kB
Slab:            19844 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 20:29:26 (client local time) WITH STATUS 10 IN 1209 SECONDS
stats: 2747 7 1209 10

Solver Data

c Parsing PB file...
c Converting 1062 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 190]---> BDD-cost:   11
c ---[ 189]---> BDD-cost:   11
c ---[ 188]---> BDD-cost:   17
c ---[ 187]---> BDD-cost:   20
c ---[ 186]---> BDD-cost:   20
c ---[ 185]---> BDD-cost:   17
c ---[ 184]---> BDD-cost:   23
c ---[ 183]---> BDD-cost:   26
c ---[ 182]---> BDD-cost:   23
c ---[ 181]---> BDD-cost:   17
c ---[ 180]---> BDD-cost:   23
c ---[ 179]---> BDD-cost:   17
c ---[ 178]---> BDD-cost:   17
c ---[ 177]---> BDD-cost:   17
c ---[ 176]---> BDD-cost:   17
c ---[ 175]---> BDD-cost:   11
c ---[ 174]---> BDD-cost:    5
c ---[ 173]---> BDD-cost:   14
c ---[ 172]---> BDD-cost:   17
c ---[ 171]---> BDD-cost:   23
c ---[ 170]---> BDD-cost:   21
c ---[ 169]---> BDD-cost:   29
c ---[ 168]---> BDD-cost:   26
c ---[ 167]---> BDD-cost:   26
c ---[ 166]---> BDD-cost:   27
c ---[ 165]---> BDD-cost:   38
c ---[ 164]---> BDD-cost:   29
c ---[ 163]---> BDD-cost:   29
c ---[ 162]---> BDD-cost:   26
c ---[ 161]---> BDD-cost:   23
c ---[ 160]---> BDD-cost:   20
c ---[ 159]---> BDD-cost:   20
c ---[ 158]---> BDD-cost:   17
c ---[ 156]---> BDD-cost:   20
c ---[ 155]---> BDD-cost:   23
c ---[ 154]---> BDD-cost:   26
c ---[ 153]---> BDD-cost:   32
c ---[ 152]---> BDD-cost:   35
c ---[ 151]---> BDD-cost:   29
c ---[ 150]---> BDD-cost:   41
c ---[ 149]---> BDD-cost:   38
c ---[ 148]---> BDD-cost:   36
c ---[ 147]---> BDD-cost:   32
c ---[ 146]---> BDD-cost:   32
c ---[ 145]---> BDD-cost:   29
c ---[ 144]---> BDD-cost:   29
c ---[ 143]---> BDD-cost:   26
c ---[ 142]---> BDD-cost:   26
c ---[ 141]---> BDD-cost:   13
c ---[ 140]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:    7
c ---[ 136]---> BDD-cost:   21
c ---[ 135]---> BDD-cost:   29
c ---[ 134]---> BDD-cost:   35
c ---[ 133]---> BDD-cost:   32
c ---[ 132]---> BDD-cost:   44
c ---[ 131]---> BDD-cost:   44
c ---[ 130]---> BDD-cost:   44
c ---[ 129]---> BDD-cost:   38
c ---[ 128]---> BDD-cost:   38
c ---[ 127]---> BDD-cost:   32
c ---[ 126]---> BDD-cost:   35
c ---[ 125]---> BDD-cost:   32
c ---[ 124]---> BDD-cost:   38
c ---[ 123]---> BDD-cost:   32
c ---[ 122]---> BDD-cost:   26
c ---[ 121]---> BDD-cost:   20
c ---[ 120]---> BDD-cost:   18
c ---[ 118]---> BDD-cost:    7
c ---[ 117]---> BDD-cost:    5
c ---[ 116]---> BDD-cost:   29
c ---[ 115]---> BDD-cost:   32
c ---[ 114]---> BDD-cost:   38
c ---[ 113]---> BDD-cost:   44
c ---[ 112]---> BDD-cost:   50
c ---[ 111]---> BDD-cost:   41
c ---[ 110]---> BDD-cost:   42
c ---[ 109]---> BDD-cost:   38
c ---[ 108]---> BDD-cost:   41
c ---[ 107]---> BDD-cost:   35
c ---[ 106]---> BDD-cost:   38
c ---[ 105]---> BDD-cost:   38
c ---[ 104]---> BDD-cost:   35
c ---[ 103]---> BDD-cost:   32
c ---[ 102]---> BDD-cost:   26
c ---[ 101]---> BDD-cost:   23
c ---[ 100]---> BDD-cost:   26
c ---[  99]---> BDD-cost:   17
c ---[  98]---> BDD-cost:   17
c ---[  97]---> BDD-cost:    5
c ---[  96]---> BDD-cost:   23
c ---[  95]---> BDD-cost:   35
c ---[  94]---> BDD-cost:   41
c ---[  93]---> BDD-cost:   41
c ---[  92]---> BDD-cost:   47
c ---[  91]---> BDD-cost:   50
c ---[  90]---> BDD-cost:   53
c ---[  89]---> BDD-cost:   47
c ---[  88]---> BDD-cost:   38
c ---[  87]---> BDD-cost:   38
c ---[  86]---> BDD-cost:   35
c ---[  85]---> BDD-cost:   32
c ---[  84]---> BDD-cost:   32
c ---[  83]---> BDD-cost:   29
c ---[  82]---> BDD-cost:   32
c ---[  81]---> BDD-cost:   32
c ---[  80]---> BDD-cost:   26
c ---[  79]---> BDD-cost:   20
c ---[  78]---> BDD-cost:   14
c ---[  77]---> BDD-cost:    8
c ---[  76]---> BDD-cost:   23
c ---[  75]---> BDD-cost:   29
c ---[  74]---> BDD-cost:   32
c ---[  73]---> BDD-cost:   41
c ---[  72]---> BDD-cost:   41
c ---[  71]---> BDD-cost:   47
c ---[  70]---> BDD-cost:   44
c ---[  69]---> BDD-cost:   44
c ---[  68]---> BDD-cost:   26
c ---[  67]---> BDD-cost:   32
c ---[  66]---> BDD-cost:   32
c ---[  65]---> BDD-cost:   32
c ---[  64]---> BDD-cost:   33
c ---[  63]---> BDD-cost:   32
c ---[  62]---> BDD-cost:   26
c ---[  61]---> BDD-cost:   29
c ---[  60]---> BDD-cost:   23
c ---[  59]---> BDD-cost:   20
c ---[  58]---> BDD-cost:   14
c ---[  57]---> BDD-cost:    5
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   26
c ---[  54]---> BDD-cost:   23
c ---[  53]---> BDD-cost:   29
c ---[  52]---> BDD-cost:   32
c ---[  51]---> BDD-cost:   38
c ---[  50]---> BDD-cost:   32
c ---[  49]---> BDD-cost:   35
c ---[  48]---> BDD-cost:   26
c ---[  47]---> BDD-cost:   26
c ---[  46]---> BDD-cost:   26
c ---[  45]---> BDD-cost:   29
c ---[  44]---> BDD-cost:   26
c ---[  43]---> BDD-cost:   29
c ---[  42]---> BDD-cost:   20
c ---[  41]---> BDD-cost:   20
c ---[  40]---> BDD-cost:   14
c ---[  39]---> BDD-cost:   18
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   17
c ---[  34]---> BDD-cost:   20
c ---[  33]---> BDD-cost:   23
c ---[  32]---> BDD-cost:   26
c ---[  31]---> BDD-cost:   29
c ---[  30]---> BDD-cost:   23
c ---[  29]---> BDD-cost:   26
c ---[  28]---> BDD-cost:   20
c ---[  27]---> BDD-cost:   23
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   26
c ---[  24]---> BDD-cost:   14
c ---[  23]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   14
c ---[  21]---> BDD-cost:   15
c ---[  20]---> BDD-cost:    9
c ---[  18]---> BDD-cost:    5
c ---[  17]---> BDD-cost:   14
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   23
c ---[  14]---> BDD-cost:   20
c ---[  13]---> BDD-cost:   20
c ---[  12]---> BDD-cost:   17
c ---[  11]---> BDD-cost:   20
c ---[  10]---> BDD-cost:   17
c ---[   9]---> BDD-cost:   20
c ---[   8]---> BDD-cost:   11
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:   14
c ---[   5]---> BDD-cost:   14
c ---[   4]---> BDD-cost:   14
c ---[   3]---> BDD-cost:    7
c ---[   2]---> BDD-cost:    8
c ---[   1]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   11765    33737 |    3921       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 1032
c ---[   0]---> Adder-cost: 2083   maxlim: 470   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   26254    85464 |    8751       0        0     nan |  0.000 % |
c |       100 |   26254    85464 |    9626     100      343     3.4 |  2.467 % |
c |       250 |   26254    85464 |   10588     250     1104     4.4 |  2.467 % |
c |       475 |   26254    85464 |   11647     475     2363     5.0 |  2.467 % |
c ==============================================================================
c Found solution: 181
c ---[   0]---> Adder-cost: 6   maxlim: 1321   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       598 |   26298    85623 |    8766     598     3233     5.4 |  2.467 % |
c |       698 |   26298    85623 |    9642     698     3737     5.4 |  2.528 % |
c |       848 |   26298    85623 |   10606     848     4598     5.4 |  2.528 % |
c ==============================================================================
c Found solution: 163
c ---[   0]---> Adder-cost: 0   maxlim: 1339   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       947 |   26301    85653 |    8767     947     5260     5.6 |  2.528 % |
c |      1047 |   26301    85653 |    9643    1047    10883    10.4 |  2.566 % |
c |      1197 |   26301    85653 |   10608    1197    11640     9.7 |  2.566 % |
c |      1423 |   26301    85653 |   11668    1423    12608     8.9 |  2.566 % |
c |      1761 |   26301    85653 |   12835    1761    20677    11.7 |  2.566 % |
c |      2267 |   26301    85653 |   14119    2267    25319    11.2 |  2.566 % |
c |      3026 |   26301    85653 |   15531    3026    32992    10.9 |  2.566 % |
c |      4165 |   26301    85653 |   17084    4165    76574    18.4 |  2.566 % |
c ==============================================================================
c Found solution: 156
c ---[   0]---> Adder-cost: 0   maxlim: 1346   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5406 |   26304    85685 |    8768    5406   109895    20.3 |  2.566 % |
c |      5506 |   26304    85685 |    9644    5506   110609    20.1 |  2.604 % |
c |      5656 |   26304    85685 |   10609    5656   111837    19.8 |  2.604 % |
c |      5881 |   26304    85685 |   11670    5881   113973    19.4 |  2.604 % |
c |      6218 |   26304    85685 |   12837    6218   131714    21.2 |  2.604 % |
c |      6725 |   26304    85685 |   14120    6725   140326    20.9 |  2.604 % |
c ==============================================================================
c Found solution: 153
c ---[   0]---> Adder-cost: 0   maxlim: 1349   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6834 |   26307    85710 |    8769    6834   141638    20.7 |  2.604 % |
c |      6935 |   26307    85710 |    9645    6935   142296    20.5 |  2.629 % |
c |      7085 |   26307    85710 |   10610    7085   145694    20.6 |  2.629 % |
c |      7311 |   26307    85710 |   11671    7311   150011    20.5 |  2.629 % |
c |      7648 |   26307    85710 |   12838    7648   156902    20.5 |  2.629 % |
c |      8155 |   26307    85710 |   14122    8155   166831    20.5 |  2.629 % |
c ==============================================================================
c Found solution: 149
c ---[   0]---> Adder-cost: 0   maxlim: 1353   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8193 |   26310    85734 |    8770    8193   167205    20.4 |  2.629 % |
c |      8294 |   26310    85734 |    9647    8294   169827    20.5 |  2.653 % |
c |      8444 |   26310    85734 |   10611    8444   173171    20.5 |  2.653 % |
c ==============================================================================
c Found solution: 119
c ---[   0]---> Adder-cost: 0   maxlim: 1383   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8489 |   26313    85754 |    8771    8489   173868    20.5 |  2.653 % |
c |      8589 |   26313    85754 |    9648    8589   175445    20.4 |  2.678 % |
c |      8741 |   26313    85754 |   10612    8741   179565    20.5 |  2.678 % |
c |      8970 |   26313    85754 |   11674    8970   190687    21.3 |  2.678 % |
c ==============================================================================
c Found solution: 115
c ---[   0]---> Adder-cost: 0   maxlim: 1387   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9032 |   26314    85765 |    8771    9032   191792    21.2 |  2.678 % |
c |      9132 |   26314    85765 |    9648    4616    65488    14.2 |  2.691 % |
c |      9282 |   26314    85765 |   10612    4766    68161    14.3 |  2.691 % |
c |      9507 |   26314    85765 |   11674    4991    71384    14.3 |  2.691 % |
c ==============================================================================
c Found solution: 99
c ---[   0]---> Adder-cost: 0   maxlim: 1403   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9579 |   26319    85799 |    8773    5063    72243    14.3 |  2.691 % |
c |      9679 |   26319    85799 |    9650    5163    75617    14.6 |  2.727 % |
c |      9829 |   26319    85799 |   10615    5313    81023    15.2 |  2.727 % |
c |     10054 |   26319    85799 |   11676    5538    85759    15.5 |  2.727 % |
c |     10391 |   26319    85799 |   12844    5875   102244    17.4 |  2.727 % |
c |     10899 |   26319    85799 |   14129    6383   114696    18.0 |  2.727 % |
c |     11660 |   26319    85799 |   15541    7144   153240    21.5 |  2.727 % |
c |     12803 |   26319    85799 |   17096    8287   178552    21.5 |  2.727 % |
c |     14511 |   26319    85799 |   18805    9995   335353    33.6 |  2.727 % |
c |     17073 |   26319    85799 |   20686   12557   429140    34.2 |  2.727 % |
c |     20918 |   26319    85799 |   22754   16402   711043    43.4 |  2.727 % |
c |     26684 |   26319    85799 |   25030   22168  1226739    55.3 |  2.727 % |
c |     35333 |   26319    85799 |   27533   17951  1054818    58.8 |  2.727 % |
c |     48307 |   26319    85799 |   30286   30925  2515081    81.3 |  2.727 % |
c |     67770 |   26319    85799 |   33315   31790  3204216   100.8 |  2.727 % |
c |     96962 |   26319    85799 |   36646   18679  1913143   102.4 |  2.727 % |
c ==============================================================================
c Found solution: 95
c ---[   0]---> Adder-cost: 0   maxlim: 1407   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98583 |   26320    85805 |    8773   20300  1958586    96.5 |  2.727 % |
c |     98683 |   26320    85805 |    9650    5175   155331    30.0 |  2.740 % |
c |     98833 |   26320    85805 |   10615    5325   156444    29.4 |  2.740 % |
c |     99059 |   26320    85805 |   11676    5551   166652    30.0 |  2.740 % |
c |     99396 |   26320    85805 |   12844    5888   171971    29.2 |  2.740 % |
c |     99903 |   26320    85805 |   14129    6395   206962    32.4 |  2.740 % |
c |    100662 |   26320    85805 |   15541    7154   245414    34.3 |  2.740 % |
c |    101801 |   26320    85805 |   17096    8293   299653    36.1 |  2.740 % |
c |    103509 |   26320    85805 |   18805   10001   404090    40.4 |  2.740 % |
c |    106072 |   26320    85805 |   20686   12564   580738    46.2 |  2.740 % |
c |    109916 |   26320    85805 |   22754   16408   859132    52.4 |  2.740 % |
c |    115682 |   26320    85805 |   25030   22174  1205307    54.4 |  2.740 % |
c |    124334 |   26320    85805 |   27533   14392  1232687    85.7 |  2.740 % |
c |    137308 |   26320    85805 |   30286   27366  3191732   116.6 |  2.740 % |
c |    156769 |   26320    85805 |   33315   27184  3327775   122.4 |  2.740 % |
c |    185961 |   26320    85805 |   36646   34727  3023365    87.1 |  2.740 % |
c |    229750 |   26320    85805 |   40311   29036  4174333   143.8 |  2.740 % |
c |    295435 |   26320    85805 |   44342   35733  4821179   134.9 |  2.740 % |
c |    393962 |   26320    85805 |   48777   31245  7114255   227.7 |  2.740 % |
c ==============================================================================
c Found solution: 93
c ---[   0]---> Adder-cost: 0   maxlim: 1409   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    402965 |   26322    85819 |    8774   40248  7669094   190.5 |  2.740 % |
c |    403065 |   26322    85819 |    9651    7692   428249    55.7 |  2.752 % |
c |    403215 |   26322    85819 |   10616    7842   429152    54.7 |  2.752 % |
c |    403440 |   26322    85819 |   11678    8067   430639    53.4 |  2.752 % |
c |    403778 |   26322    85819 |   12846    8405   444954    52.9 |  2.752 % |
c |    404285 |   26322    85819 |   14130    8912   451552    50.7 |  2.752 % |
c |    405044 |   26322    85819 |   15543    9671   460234    47.6 |  2.752 % |
c |    406184 |   26322    85819 |   17098   10811   485817    44.9 |  2.752 % |
c |    407892 |   26322    85819 |   18807   12519   577961    46.2 |  2.752 % |
c |    410455 |   26322    85819 |   20688   15082   703570    46.6 |  2.752 % |
c |    414299 |   26322    85819 |   22757   18926   957487    50.6 |  2.752 % |
c |    420065 |   26322    85819 |   25033   24692  1288839    52.2 |  2.752 % |
c |    428714 |   26322    85819 |   27536   19026  1376838    72.4 |  2.752 % |
c |    441690 |   26322    85819 |   30290   32002  2455886    76.7 |  2.752 % |
c |    461154 |   26322    85819 |   33319   32530  2789845    85.8 |  2.752 % |
c |    490346 |   26322    85819 |   36651   18436  2229327   120.9 |  2.752 % |
c |    534136 |   26322    85819 |   40316   35911  6004074   167.2 |  2.752 % |
c |    599820 |   26322    85819 |   44347   43924  8128207   185.1 |  2.752 % |
c |    698346 |   26322    85819 |   48782   46314  7937399   171.4 |  2.752 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v853 v782 -v197 v102 -v21 v2 v855 -v103 v1 v785 -v384 -v272 -v196 -v20 v3 v856 -v786 -v76 -v55 v23 v4 -v383 -v275 -v202 -v75 -v54 v11 v763 -v387 -v276 -v200 v56 -v24 v5 v762 -v247 -v150 -v77 v57 -v26 v6 v764 -v613 -v388 -v201 -v79 v58 v39 -v27 -v7 v765 v612 -v513 -v250 -v205 -v149 -v65 v38 v766 -v618 -v251 -v80 v59 v40 v773 -v617 -v512 -v326 -v155 v125 -v82 -v60 v41 v767 -v619 -v153 -v83 -v61 v42 -v768 v623 v593 -v573 -v518 -v128 v49 -v769 v622 -v577 -v516 -v154 -v129 v43 v729 -v620 v596 -v576 -v158 v44 -v621 v597 -v517 v45 -v881 v728 -v521 -v852 v781 -v192 v104 -v17 v857 v787 -v537 -v468 -v271 -v198 -v22 -v14 -v541 -v71 v25 -v15 -v859 -v385 -v277 -v203 -v108 -v70 v29 v10 -v860 -v389 v28 -v790 -v246 -v206 -v145 -v78 v68 v8 -v204 -v81 v69 -v811 v776 -v638 -v508 -v391 -v322 -v280 -v252 -v151 -v85 -v64 v777 -v642 v614 -v392 -v84 v772 v615 -v514 -v325 -v156 v124 -v62 -v52 v616 -v53 v770 -v627 v592 -v519 -v255 -v159 -v130 v48 -v572 -v157 -v877 v598 -v574 -v522 v46 -v578 -v520 v880 v730 -v133 -v601 -v854 v783 v464 v267 v105 -v13 v858 -v379 -v191 v16 -v12 -v862 v788 -v536 -v488 -v467 -v378 -v273 -v193 v109 v18 -v861 -v540 v492 -v199 v107 v19 -v791 -v386 -v278 -v242 -v195 -v67 v33 -v789 -v390 -v207 -v72 -v66 -v807 v775 v394 v301 -v281 -v248 -v73 v9 v774 v393 -v279 -v144 -v74 -v810 -v637 -v321 -v253 -v146 v120 -v89 -v51 -v641 -v507 -v152 -v50 v630 -v588 -v509 -v327 -v256 -v148 v126 -v63 v631 -v515 -v254 -v160 v771 -v626 v594 -v511 -v131 v725 -v523 -v876 v724 -v709 -v624 v599 -v330 -v134 v47 -v575 -v132 v882 v731 -v602 v586 -v600 v582 v900 v732 -v581 -v904 v733 v851 -v779 v463 -v422 v106 v850 v784 -v426 v266 v110 v866 v780 -v662 -v538 -v487 -v469 v268 -v177 v36 v792 -v666 -v542 v491 -v380 -v274 -v194 v37 -v381 -v297 v270 -v222 -v215 -v32 v382 -v282 -v241 v226 -v211 -v806 -v544 -v472 -v398 -v317 v300 -v243 -v210 -v92 -v30 -v545 -v249 -v93 -v812 -v639 -v629 -v323 -v245 -v88 v643 -v628 -v257 -v147 v119 -v913 v836 -v328 -v168 v121 -v86 -v917 -v587 -v510 -v164 v127 v872 -v815 -v705 -v645 -v589 -v531 -v347 -v331 -v163 v123 -v646 v595 -v527 -v351 -v329 -v135 -v878 -v708 -v625 v591 v583 -v526 v726 v603 v585 -v95 v883 v727 -v94 v899 v884 v737 -v579 -v903 v885 v869 -v533 v465 -v421 -v173 -v118 -v35 v870 -v778 -v425 v114 -v34 v865 -v800 -v661 -v539 -v489 -v470 -v212 -v176 v113 -v796 -v665 -v543 v493 v269 -v214 v863 -v802 -v795 -v547 -v473 -v450 v401 -v296 v290 -v221 -v91 -v633 -v546 -v471 v402 -v286 v225 -v90 -v808 -v632 v495 -v397 v302 -v285 -v208 -v31 v496 -v316 -v244 -v832 -v813 -v752 -v640 -v395 -v318 -v265 -v209 -v165 v644 -v324 -v261 -v167 v912 v835 -v816 -v648 -v528 v320 -v305 -v260 -v87 -v916 -v814 -v647 -v530 v332 v122 -v704 -v346 -v161 v143 v871 -v590 v584 -v350 -v139 v873 -v710 -v611 -v524 -v162 -v138 -v879 -v607 v875 v740 -v606 v561 -v525 v886 v741 -v565 -v96 v901 v736 -v713 -v580 v97 -v905 v867 -v797 -v484 v461 -v423 -v172 -v117 -v799 -v532 v466 -v427 -v213 -v663 -v534 -v490 v462 -v446 v400 -v292 v287 -v178 v111 -v667 -v535 v494 -v474 v399 v289 v864 -v793 -v551 v498 v449 -v429 -v298 -v223 v112 -v801 v497 -v430 v227 -v803 -v794 -v748 -v687 -v669 v303 -v283 -v262 -v181 -v809 -v691 -v670 -v634 -v264 -v166 -v831 -v805 -v751 -v635 -v396 v306 -v284 v229 -v817 v636 -v529 -v319 v304 -v230 v914 v837 -v700 v652 v340 -v258 v140 -v918 v336 v142 -v706 -v608 -v348 v335 -v259 -v610 -v352 -v920 -v840 v739 -v711 -v412 -v371 -v136 -v921 -v896 v874 v738 v375 -v895 -v894 v714 -v604 v560 -v354 -v137 v890 v712 -v564 -v355 v902 -v889 v734 -v605 v100 -v906 v101 -v868 -v798 v658 v424 -v174 -v115 -v483 v460 -v428 v288 -v217 -v664 -v554 -v485 -v482 -v445 -v432 -v216 -v179 -v668 -v555 v486 v478 -v431 -v291 -v672 -v550 -v502 -v477 v451 -v293 -v224 -v182 -v671 -v299 -v263 v228 -v180 v827 -v747 -v686 -v548 v295 v232 -v908 -v804 v690 v307 v231 -v907 -v833 -v825 -v753 -v655 v454 -v337 -v821 -v656 -v342 v339 -v141 v915 v838 -v820 -v651 -v341 -v919 -v699 -v609 -v923 -v841 v756 -v701 -v649 v408 -v349 -v333 -v922 -v839 -v707 -v353 -v891 v703 -v411 -v370 v357 -v334 -v893 v715 v374 -v356 v562 -v99 -v897 -v566 -v98 v898 -v887 v

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/2088/stat): 2088 (minisat+_script) R 2087 2088 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1844021968 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/2088/statm): 174 3 169 147 0 27 0
[pid=2088] 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=2089
New process pid=2090
New process pid=2091
execve syscall for /bin/sed executable
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
One traced child (pid=2090) exited with status: 0
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=2091) exited with status: 0
One traced child (pid=2089) exited with status: 0
New process pid=2092
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-10:20:4.5:0.95:100.opb

[startup+10.0042 s]
Raw data (loadavg): 0.64 0.81 0.85 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 2143 0 0 0 977 11 0 0 25 0 1 0 1844021973 8572928 1851 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 2093 1851 145 145 0 1948 0
[pid=2092] vsize: 8372
Current children cumulated CPU time (s) 9.9
Current children cumulated vsize (Kb) 10496

[startup+20.0059 s]
Raw data (loadavg): 0.70 0.82 0.85 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 3277 0 0 0 1959 18 0 0 25 0 1 0 1844021973 13225984 2985 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 3229 2985 145 145 0 3084 0
[pid=2092] vsize: 12916
Current children cumulated CPU time (s) 19.79
Current children cumulated vsize (Kb) 15040

[startup+30.0076 s]
Raw data (loadavg): 0.74 0.82 0.86 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 3590 0 0 0 2954 21 0 0 25 0 1 0 1844021973 14491648 3298 4294967295 134512640 135094434 3221224432 3221222896 134780892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 3538 3298 145 145 0 3393 0
[pid=2092] vsize: 14152
Current children cumulated CPU time (s) 29.77
Current children cumulated vsize (Kb) 16276

[startup+40.0083 s]
Raw data (loadavg): 0.78 0.83 0.86 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 4526 0 0 0 3938 27 0 0 25 0 1 0 1844021973 18313216 4234 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 4471 4234 145 145 0 4326 0
[pid=2092] vsize: 17884
Current children cumulated CPU time (s) 39.67
Current children cumulated vsize (Kb) 20008

[startup+50.01 s]
Raw data (loadavg): 0.81 0.83 0.86 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 4713 0 0 0 4933 29 0 0 25 0 1 0 1844021973 19070976 4421 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 4656 4421 145 145 0 4511 0
[pid=2092] vsize: 18624
Current children cumulated CPU time (s) 49.64
Current children cumulated vsize (Kb) 20748

[startup+60.0107 s]
Raw data (loadavg): 0.84 0.84 0.86 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 5087 0 0 0 5925 33 0 0 25 0 1 0 1844021973 20602880 4795 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 5030 4795 145 145 0 4885 0
[pid=2092] vsize: 20120
Current children cumulated CPU time (s) 59.6
Current children cumulated vsize (Kb) 22244

[startup+70.0124 s]
Raw data (loadavg): 0.87 0.84 0.86 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 5748 0 0 0 6912 39 0 0 25 0 1 0 1844021973 23437312 5456 4294967295 134512640 135094434 3221224432 3221223056 134562115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 5722 5456 145 145 0 5577 0
[pid=2092] vsize: 22888
Current children cumulated CPU time (s) 69.53
Current children cumulated vsize (Kb) 25012

[startup+80.0141 s]
Raw data (loadavg): 0.89 0.85 0.86 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 5748 0 0 0 7911 39 0 0 25 0 1 0 1844021973 23437312 5456 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 5722 5456 145 145 0 5577 0
[pid=2092] vsize: 22888
Current children cumulated CPU time (s) 79.52
Current children cumulated vsize (Kb) 25012

[startup+90.0148 s]
Raw data (loadavg): 0.90 0.85 0.86 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 5899 0 0 0 8907 42 0 0 23 0 1 0 1844021973 24055808 5607 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 5873 5607 145 145 0 5728 0
[pid=2092] vsize: 23492
Current children cumulated CPU time (s) 89.51
Current children cumulated vsize (Kb) 25616

[startup+100.016 s]
Raw data (loadavg): 0.92 0.86 0.86 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 6742 0 0 0 9891 48 0 0 25 0 1 0 1844021973 27504640 6450 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 6715 6450 145 145 0 6570 0
[pid=2092] vsize: 26860
Current children cumulated CPU time (s) 99.41
Current children cumulated vsize (Kb) 28984

[startup+110.016 s]
Raw data (loadavg): 0.93 0.86 0.86 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 6751 0 0 0 10891 49 0 0 25 0 1 0 1844021973 27541504 6459 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 6724 6459 145 145 0 6579 0
[pid=2092] vsize: 26896
Current children cumulated CPU time (s) 109.42
Current children cumulated vsize (Kb) 29020

[startup+120.018 s]
Raw data (loadavg): 0.94 0.86 0.86 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 6751 0 0 0 11891 49 0 0 25 0 1 0 1844021973 27541504 6459 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 6724 6459 145 145 0 6579 0
[pid=2092] vsize: 26896
Current children cumulated CPU time (s) 119.42
Current children cumulated vsize (Kb) 29020

[startup+130.019 s]
Raw data (loadavg): 0.95 0.87 0.87 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 6751 0 0 0 12891 49 0 0 25 0 1 0 1844021973 27541504 6459 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 6724 6459 145 145 0 6579 0
[pid=2092] vsize: 26896
Current children cumulated CPU time (s) 129.42
Current children cumulated vsize (Kb) 29020

[startup+140.019 s]
Raw data (loadavg): 0.96 0.87 0.87 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 6751 0 0 0 13891 49 0 0 25 0 1 0 1844021973 27541504 6459 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 6724 6459 145 145 0 6579 0
[pid=2092] vsize: 26896
Current children cumulated CPU time (s) 139.42
Current children cumulated vsize (Kb) 29020

[startup+150.021 s]
Raw data (loadavg): 0.96 0.88 0.87 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 6751 0 0 0 14890 50 0 0 25 0 1 0 1844021973 27541504 6459 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 6724 6459 145 145 0 6579 0
[pid=2092] vsize: 26896
Current children cumulated CPU time (s) 149.42
Current children cumulated vsize (Kb) 29020

[startup+160.022 s]
Raw data (loadavg): 0.97 0.88 0.87 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 6751 0 0 0 15889 51 0 0 25 0 1 0 1844021973 27541504 6459 4294967295 134512640 135094434 3221224432 3221223104 134555795 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 6724 6459 145 145 0 6579 0
[pid=2092] vsize: 26896
Current children cumulated CPU time (s) 159.42
Current children cumulated vsize (Kb) 29020

[startup+170.023 s]
Raw data (loadavg): 0.97 0.88 0.87 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 6751 0 0 0 16889 52 0 0 25 0 1 0 1844021973 27541504 6459 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 6724 6459 145 145 0 6579 0
[pid=2092] vsize: 26896
Current children cumulated CPU time (s) 169.43
Current children cumulated vsize (Kb) 29020

[startup+180.024 s]
Raw data (loadavg): 0.98 0.89 0.87 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 6751 0 0 0 17888 52 0 0 25 0 1 0 1844021973 27541504 6459 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 6724 6459 145 145 0 6579 0
[pid=2092] vsize: 26896
Current children cumulated CPU time (s) 179.42
Current children cumulated vsize (Kb) 29020

[startup+190.025 s]
Raw data (loadavg): 0.98 0.89 0.87 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 6751 0 0 0 18888 53 0 0 25 0 1 0 1844021973 27541504 6459 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 6724 6459 145 145 0 6579 0
[pid=2092] vsize: 26896
Current children cumulated CPU time (s) 189.43
Current children cumulated vsize (Kb) 29020

[startup+200.027 s]
Raw data (loadavg): 0.98 0.89 0.87 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 6751 0 0 0 19887 54 0 0 25 0 1 0 1844021973 27541504 6459 4294967295 134512640 135094434 3221224432 3221223088 134557987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 6724 6459 145 145 0 6579 0
[pid=2092] vsize: 26896
Current children cumulated CPU time (s) 199.43
Current children cumulated vsize (Kb) 29020

[startup+210.027 s]
Raw data (loadavg): 0.98 0.89 0.87 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 6751 0 0 0 20887 54 0 0 25 0 1 0 1844021973 27541504 6459 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 6724 6459 145 145 0 6579 0
[pid=2092] vsize: 26896
Current children cumulated CPU time (s) 209.43
Current children cumulated vsize (Kb) 29020

[startup+220.029 s]
Raw data (loadavg): 0.99 0.90 0.87 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 6752 0 0 0 21886 54 0 0 25 0 1 0 1844021973 27541504 6460 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 6724 6460 145 145 0 6579 0
[pid=2092] vsize: 26896
Current children cumulated CPU time (s) 219.42
Current children cumulated vsize (Kb) 29020

[startup+230.031 s]
Raw data (loadavg): 0.99 0.90 0.87 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 6755 0 0 0 22886 55 0 0 25 0 1 0 1844021973 27541504 6463 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 6724 6463 145 145 0 6579 0
[pid=2092] vsize: 26896
Current children cumulated CPU time (s) 229.43
Current children cumulated vsize (Kb) 29020

[startup+240.031 s]
Raw data (loadavg): 0.99 0.90 0.88 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 6755 0 0 0 23885 55 0 0 25 0 1 0 1844021973 27541504 6463 4294967295 134512640 135094434 3221224432 3221223104 134555743 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 6724 6463 145 145 0 6579 0
[pid=2092] vsize: 26896
Current children cumulated CPU time (s) 239.42
Current children cumulated vsize (Kb) 29020

[startup+250.033 s]
Raw data (loadavg): 0.99 0.91 0.88 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 6755 0 0 0 24885 56 0 0 25 0 1 0 1844021973 27541504 6463 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 6724 6463 145 145 0 6579 0
[pid=2092] vsize: 26896
Current children cumulated CPU time (s) 249.43
Current children cumulated vsize (Kb) 29020

[startup+260.034 s]
Raw data (loadavg): 0.99 0.91 0.88 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 7363 0 0 0 25873 61 0 0 25 0 1 0 1844021973 30035968 7071 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 7333 7071 145 145 0 7188 0
[pid=2092] vsize: 29332
Current children cumulated CPU time (s) 259.36
Current children cumulated vsize (Kb) 31456

[startup+270.036 s]
Raw data (loadavg): 0.99 0.91 0.88 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 8081 0 0 0 26861 67 0 0 25 0 1 0 1844021973 32993280 7789 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 8055 7789 145 145 0 7910 0
[pid=2092] vsize: 32220
Current children cumulated CPU time (s) 269.3
Current children cumulated vsize (Kb) 34344

[startup+280.036 s]
Raw data (loadavg): 0.99 0.91 0.88 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 8325 0 0 0 27856 70 0 0 25 0 1 0 1844021973 33992704 8033 4294967295 134512640 135094434 3221224432 3221223024 134557407 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 8299 8033 145 145 0 8154 0
[pid=2092] vsize: 33196
Current children cumulated CPU time (s) 279.28
Current children cumulated vsize (Kb) 35320

[startup+290.037 s]
Raw data (loadavg): 0.99 0.92 0.88 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 8325 0 0 0 28856 70 0 0 25 0 1 0 1844021973 33992704 8033 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 8299 8033 145 145 0 8154 0
[pid=2092] vsize: 33196
Current children cumulated CPU time (s) 289.28
Current children cumulated vsize (Kb) 35320

[startup+300.038 s]
Raw data (loadavg): 0.99 0.92 0.88 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 8325 0 0 0 29856 70 0 0 25 0 1 0 1844021973 33992704 8033 4294967295 134512640 135094434 3221224432 3221223024 134557488 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 8299 8033 145 145 0 8154 0
[pid=2092] vsize: 33196
Current children cumulated CPU time (s) 299.28
Current children cumulated vsize (Kb) 35320

[startup+310.038 s]
Raw data (loadavg): 0.99 0.92 0.88 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 8328 0 0 0 30856 70 0 0 25 0 1 0 1844021973 33992704 8036 4294967295 134512640 135094434 3221224432 3221223024 134557372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 8299 8036 145 145 0 8154 0
[pid=2092] vsize: 33196
Current children cumulated CPU time (s) 309.28
Current children cumulated vsize (Kb) 35320

[startup+320.039 s]
Raw data (loadavg): 0.99 0.92 0.88 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 8491 0 0 0 31853 72 0 0 25 0 1 0 1844021973 34656256 8199 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 8461 8199 145 145 0 8316 0
[pid=2092] vsize: 33844
Current children cumulated CPU time (s) 319.27
Current children cumulated vsize (Kb) 35968

[startup+330.04 s]
Raw data (loadavg): 0.99 0.92 0.88 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 8491 0 0 0 32853 72 0 0 25 0 1 0 1844021973 34656256 8199 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 8461 8199 145 145 0 8316 0
[pid=2092] vsize: 33844
Current children cumulated CPU time (s) 329.27
Current children cumulated vsize (Kb) 35968

[startup+340.04 s]
Raw data (loadavg): 0.99 0.93 0.89 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 8491 0 0 0 33853 72 0 0 25 0 1 0 1844021973 34656256 8199 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 8461 8199 145 145 0 8316 0
[pid=2092] vsize: 33844
Current children cumulated CPU time (s) 339.27
Current children cumulated vsize (Kb) 35968

[startup+350.041 s]
Raw data (loadavg): 0.99 0.93 0.89 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 8491 0 0 0 34854 72 0 0 25 0 1 0 1844021973 34656256 8199 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 8461 8199 145 145 0 8316 0
[pid=2092] vsize: 33844
Current children cumulated CPU time (s) 349.28
Current children cumulated vsize (Kb) 35968

[startup+360.042 s]
Raw data (loadavg): 0.99 0.93 0.89 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 8491 0 0 0 35854 72 0 0 25 0 1 0 1844021973 34656256 8199 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 8461 8199 145 145 0 8316 0
[pid=2092] vsize: 33844
Current children cumulated CPU time (s) 359.28
Current children cumulated vsize (Kb) 35968

[startup+370.044 s]
Raw data (loadavg): 0.99 0.93 0.89 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 8491 0 0 0 36854 72 0 0 25 0 1 0 1844021973 34656256 8199 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 8461 8199 145 145 0 8316 0
[pid=2092] vsize: 33844
Current children cumulated CPU time (s) 369.28
Current children cumulated vsize (Kb) 35968

[startup+380.044 s]
Raw data (loadavg): 0.99 0.93 0.89 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 8491 0 0 0 37854 72 0 0 25 0 1 0 1844021973 34656256 8199 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 8461 8199 145 145 0 8316 0
[pid=2092] vsize: 33844
Current children cumulated CPU time (s) 379.28
Current children cumulated vsize (Kb) 35968

[startup+390.045 s]
Raw data (loadavg): 0.99 0.94 0.89 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 8491 0 0 0 38855 72 0 0 25 0 1 0 1844021973 34656256 8199 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 8461 8199 145 145 0 8316 0
[pid=2092] vsize: 33844
Current children cumulated CPU time (s) 389.29
Current children cumulated vsize (Kb) 35968

[startup+400.047 s]
Raw data (loadavg): 0.99 0.94 0.89 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 8491 0 0 0 39855 72 0 0 25 0 1 0 1844021973 34656256 8199 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 8461 8199 145 145 0 8316 0
[pid=2092] vsize: 33844
Current children cumulated CPU time (s) 399.29
Current children cumulated vsize (Kb) 35968

[startup+410.047 s]
Raw data (loadavg): 0.99 0.94 0.89 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 8491 0 0 0 40855 72 0 0 25 0 1 0 1844021973 34656256 8199 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 8461 8199 145 145 0 8316 0
[pid=2092] vsize: 33844
Current children cumulated CPU time (s) 409.29
Current children cumulated vsize (Kb) 35968

[startup+420.048 s]
Raw data (loadavg): 0.99 0.94 0.89 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 8491 0 0 0 41856 72 0 0 25 0 1 0 1844021973 34656256 8199 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 8461 8199 145 145 0 8316 0
[pid=2092] vsize: 33844
Current children cumulated CPU time (s) 419.3
Current children cumulated vsize (Kb) 35968

[startup+430.05 s]
Raw data (loadavg): 0.99 0.94 0.89 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 8491 0 0 0 42856 72 0 0 25 0 1 0 1844021973 34656256 8199 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 8461 8199 145 145 0 8316 0
[pid=2092] vsize: 33844
Current children cumulated CPU time (s) 429.3
Current children cumulated vsize (Kb) 35968

[startup+440.051 s]
Raw data (loadavg): 0.99 0.94 0.90 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 8953 0 0 0 43847 75 0 0 25 0 1 0 1844021973 36544512 8661 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 8922 8661 145 145 0 8777 0
[pid=2092] vsize: 35688
Current children cumulated CPU time (s) 439.24
Current children cumulated vsize (Kb) 37812

[startup+450.052 s]
Raw data (loadavg): 0.99 0.94 0.90 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 9352 0 0 0 44839 79 0 0 25 0 1 0 1844021973 38170624 9060 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 9319 9060 145 145 0 9174 0
[pid=2092] vsize: 37276
Current children cumulated CPU time (s) 449.2
Current children cumulated vsize (Kb) 39400

[startup+460.053 s]
Raw data (loadavg): 0.99 0.95 0.90 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 9352 0 0 0 45840 79 0 0 25 0 1 0 1844021973 38170624 9060 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 9319 9060 145 145 0 9174 0
[pid=2092] vsize: 37276
Current children cumulated CPU time (s) 459.21
Current children cumulated vsize (Kb) 39400

[startup+470.055 s]
Raw data (loadavg): 0.99 0.95 0.90 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 9352 0 0 0 46840 79 0 0 25 0 1 0 1844021973 38170624 9060 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 9319 9060 145 145 0 9174 0
[pid=2092] vsize: 37276
Current children cumulated CPU time (s) 469.21
Current children cumulated vsize (Kb) 39400

[startup+480.055 s]
Raw data (loadavg): 0.99 0.95 0.90 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 9353 0 0 0 47840 79 0 0 25 0 1 0 1844021973 38170624 9061 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 9319 9061 145 145 0 9174 0
[pid=2092] vsize: 37276
Current children cumulated CPU time (s) 479.21
Current children cumulated vsize (Kb) 39400

[startup+490.056 s]
Raw data (loadavg): 0.99 0.95 0.90 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 9353 0 0 0 48840 79 0 0 25 0 1 0 1844021973 38170624 9061 4294967295 134512640 135094434 3221224432 3221223088 134558002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 9319 9061 145 145 0 9174 0
[pid=2092] vsize: 37276
Current children cumulated CPU time (s) 489.21
Current children cumulated vsize (Kb) 39400

[startup+500.058 s]
Raw data (loadavg): 0.99 0.95 0.90 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 9353 0 0 0 49841 79 0 0 25 0 1 0 1844021973 38170624 9061 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 9319 9061 145 145 0 9174 0
[pid=2092] vsize: 37276
Current children cumulated CPU time (s) 499.22
Current children cumulated vsize (Kb) 39400

[startup+510.058 s]
Raw data (loadavg): 0.99 0.95 0.90 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 9664 0 0 0 50836 81 0 0 25 0 1 0 1844021973 39444480 9372 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 9630 9372 145 145 0 9485 0
[pid=2092] vsize: 38520
Current children cumulated CPU time (s) 509.19
Current children cumulated vsize (Kb) 40644

[startup+520.059 s]
Raw data (loadavg): 0.99 0.95 0.90 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 9881 0 0 0 51832 83 0 0 25 0 1 0 1844021973 40329216 9589 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 9846 9589 145 145 0 9701 0
[pid=2092] vsize: 39384
Current children cumulated CPU time (s) 519.17
Current children cumulated vsize (Kb) 41508

[startup+530.061 s]
Raw data (loadavg): 0.99 0.95 0.90 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 9881 0 0 0 52833 83 0 0 25 0 1 0 1844021973 40329216 9589 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 9846 9589 145 145 0 9701 0
[pid=2092] vsize: 39384
Current children cumulated CPU time (s) 529.18
Current children cumulated vsize (Kb) 41508

[startup+540.062 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 9881 0 0 0 53833 83 0 0 25 0 1 0 1844021973 40329216 9589 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 9846 9589 145 145 0 9701 0
[pid=2092] vsize: 39384
Current children cumulated CPU time (s) 539.18
Current children cumulated vsize (Kb) 41508

[startup+550.062 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 9881 0 0 0 54833 83 0 0 25 0 1 0 1844021973 40329216 9589 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 9846 9589 145 145 0 9701 0
[pid=2092] vsize: 39384
Current children cumulated CPU time (s) 549.18
Current children cumulated vsize (Kb) 41508

[startup+560.063 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 9881 0 0 0 55833 83 0 0 25 0 1 0 1844021973 40329216 9589 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 9846 9589 145 145 0 9701 0
[pid=2092] vsize: 39384
Current children cumulated CPU time (s) 559.18
Current children cumulated vsize (Kb) 41508

[startup+570.065 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 10013 0 0 0 56831 84 0 0 25 0 1 0 1844021973 40869888 9721 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 9978 9721 145 145 0 9833 0
[pid=2092] vsize: 39912
Current children cumulated CPU time (s) 569.17
Current children cumulated vsize (Kb) 42036

[startup+580.065 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 10858 0 0 0 57818 89 0 0 25 0 1 0 1844021973 44331008 10566 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 10823 10566 145 145 0 10678 0
[pid=2092] vsize: 43292
Current children cumulated CPU time (s) 579.09
Current children cumulated vsize (Kb) 45416

[startup+590.066 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 58807 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 589.02
Current children cumulated vsize (Kb) 48016

[startup+600.068 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 59808 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223080 134557061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 599.03
Current children cumulated vsize (Kb) 48016

[startup+610.068 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 60808 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 609.03
Current children cumulated vsize (Kb) 48016

[startup+620.069 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 61808 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 619.03
Current children cumulated vsize (Kb) 48016

[startup+630.07 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 62808 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 629.03
Current children cumulated vsize (Kb) 48016

[startup+640.071 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 63809 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 639.04
Current children cumulated vsize (Kb) 48016

[startup+650.071 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 64808 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 649.03
Current children cumulated vsize (Kb) 48016

[startup+660.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 65808 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 659.03
Current children cumulated vsize (Kb) 48016

[startup+670.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 66809 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 669.04
Current children cumulated vsize (Kb) 48016

[startup+680.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 67809 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 679.04
Current children cumulated vsize (Kb) 48016

[startup+690.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 68809 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 689.04
Current children cumulated vsize (Kb) 48016

[startup+700.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 69809 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 699.04
Current children cumulated vsize (Kb) 48016

[startup+710.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 70809 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 709.04
Current children cumulated vsize (Kb) 48016

[startup+720.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 71809 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 719.04
Current children cumulated vsize (Kb) 48016

[startup+730.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 72810 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 729.05
Current children cumulated vsize (Kb) 48016

[startup+740.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 73810 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 739.05
Current children cumulated vsize (Kb) 48016

[startup+750.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 74810 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 749.05
Current children cumulated vsize (Kb) 48016

[startup+760.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 75810 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 759.05
Current children cumulated vsize (Kb) 48016

[startup+770.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 76811 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 769.06
Current children cumulated vsize (Kb) 48016

[startup+780.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 77811 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 779.06
Current children cumulated vsize (Kb) 48016

[startup+790.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 78811 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223024 134551463 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 789.06
Current children cumulated vsize (Kb) 48016

[startup+800.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 79811 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 799.06
Current children cumulated vsize (Kb) 48016

[startup+810.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 80812 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 809.07
Current children cumulated vsize (Kb) 48016

[startup+820.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 81812 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134558147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 819.07
Current children cumulated vsize (Kb) 48016

[startup+830.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 82812 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 829.07
Current children cumulated vsize (Kb) 48016

[startup+840.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 83812 93 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 839.07
Current children cumulated vsize (Kb) 48016

[startup+850.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 84812 94 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 849.08
Current children cumulated vsize (Kb) 48016

[startup+860.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 85812 94 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 859.08
Current children cumulated vsize (Kb) 48016

[startup+870.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 86813 94 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223104 134555795 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 869.09
Current children cumulated vsize (Kb) 48016

[startup+880.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 87813 94 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 879.09
Current children cumulated vsize (Kb) 48016

[startup+890.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 88813 94 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 889.09
Current children cumulated vsize (Kb) 48016

[startup+900.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 89813 94 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 899.09
Current children cumulated vsize (Kb) 48016

[startup+910.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 90814 94 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 909.1
Current children cumulated vsize (Kb) 48016

[startup+920.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 91814 94 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 919.1
Current children cumulated vsize (Kb) 48016

[startup+930.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11508 0 0 0 92814 94 0 0 25 0 1 0 1844021973 46993408 11216 4294967295 134512640 135094434 3221224432 3221223024 134557393 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11216 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 929.1
Current children cumulated vsize (Kb) 48016

[startup+940.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11509 0 0 0 93815 94 0 0 25 0 1 0 1844021973 46993408 11217 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11217 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 939.11
Current children cumulated vsize (Kb) 48016

[startup+950.097 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11509 0 0 0 94815 94 0 0 25 0 1 0 1844021973 46993408 11217 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11217 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 949.11
Current children cumulated vsize (Kb) 48016

[startup+960.097 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11509 0 0 0 95815 94 0 0 25 0 1 0 1844021973 46993408 11217 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11217 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 959.11
Current children cumulated vsize (Kb) 48016

[startup+970.097 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11509 0 0 0 96815 94 0 0 25 0 1 0 1844021973 46993408 11217 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11217 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 969.11
Current children cumulated vsize (Kb) 48016

[startup+980.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11509 0 0 0 97816 94 0 0 25 0 1 0 1844021973 46993408 11217 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11473 11217 145 145 0 11328 0
[pid=2092] vsize: 45892
Current children cumulated CPU time (s) 979.12
Current children cumulated vsize (Kb) 48016

[startup+990.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 11894 0 0 0 98810 95 0 0 25 0 1 0 1844021973 48570368 11602 4294967295 134512640 135094434 3221224432 3221223104 134556521 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 11858 11602 145 145 0 11713 0
[pid=2092] vsize: 47432
Current children cumulated CPU time (s) 989.07
Current children cumulated vsize (Kb) 49556

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 12263 0 0 0 99804 98 0 0 25 0 1 0 1844021973 50098176 11971 4294967295 134512640 135094434 3221224432 3221223088 134558238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 12231 11971 145 145 0 12086 0
[pid=2092] vsize: 48924
Current children cumulated CPU time (s) 999.04
Current children cumulated vsize (Kb) 51048

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 12263 0 0 0 100803 98 0 0 25 0 1 0 1844021973 50098176 11971 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 12231 11971 145 145 0 12086 0
[pid=2092] vsize: 48924
Current children cumulated CPU time (s) 1009.03
Current children cumulated vsize (Kb) 51048

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 12263 0 0 0 101804 98 0 0 25 0 1 0 1844021973 50098176 11971 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 12231 11971 145 145 0 12086 0
[pid=2092] vsize: 48924
Current children cumulated CPU time (s) 1019.04
Current children cumulated vsize (Kb) 51048

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 12263 0 0 0 102804 98 0 0 25 0 1 0 1844021973 50098176 11971 4294967295 134512640 135094434 3221224432 3221223024 134556894 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 12231 11971 145 145 0 12086 0
[pid=2092] vsize: 48924
Current children cumulated CPU time (s) 1029.04
Current children cumulated vsize (Kb) 51048

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 12263 0 0 0 103804 98 0 0 25 0 1 0 1844021973 50098176 11971 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 12231 11971 145 145 0 12086 0
[pid=2092] vsize: 48924
Current children cumulated CPU time (s) 1039.04
Current children cumulated vsize (Kb) 51048

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 12263 0 0 0 104804 98 0 0 25 0 1 0 1844021973 50098176 11971 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 12231 11971 145 145 0 12086 0
[pid=2092] vsize: 48924
Current children cumulated CPU time (s) 1049.04
Current children cumulated vsize (Kb) 51048

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 12263 0 0 0 105805 98 0 0 25 0 1 0 1844021973 50098176 11971 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 12231 11971 145 145 0 12086 0
[pid=2092] vsize: 48924
Current children cumulated CPU time (s) 1059.05
Current children cumulated vsize (Kb) 51048

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 12263 0 0 0 106805 98 0 0 25 0 1 0 1844021973 50098176 11971 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 12231 11971 145 145 0 12086 0
[pid=2092] vsize: 48924
Current children cumulated CPU time (s) 1069.05
Current children cumulated vsize (Kb) 51048

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 12263 0 0 0 107805 98 0 0 25 0 1 0 1844021973 50098176 11971 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 12231 11971 145 145 0 12086 0
[pid=2092] vsize: 48924
Current children cumulated CPU time (s) 1079.05
Current children cumulated vsize (Kb) 51048

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 12263 0 0 0 108805 98 0 0 25 0 1 0 1844021973 50098176 11971 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 12231 11971 145 145 0 12086 0
[pid=2092] vsize: 48924
Current children cumulated CPU time (s) 1089.05
Current children cumulated vsize (Kb) 51048

[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 12263 0 0 0 109805 98 0 0 25 0 1 0 1844021973 50098176 11971 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 12231 11971 145 145 0 12086 0
[pid=2092] vsize: 48924
Current children cumulated CPU time (s) 1099.05
Current children cumulated vsize (Kb) 51048

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 12263 0 0 0 110805 98 0 0 25 0 1 0 1844021973 50098176 11971 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 12231 11971 145 145 0 12086 0
[pid=2092] vsize: 48924
Current children cumulated CPU time (s) 1109.05
Current children cumulated vsize (Kb) 51048

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 12263 0 0 0 111806 98 0 0 25 0 1 0 1844021973 50098176 11971 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 12231 11971 145 145 0 12086 0
[pid=2092] vsize: 48924
Current children cumulated CPU time (s) 1119.06
Current children cumulated vsize (Kb) 51048

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 12263 0 0 0 112806 98 0 0 25 0 1 0 1844021973 50098176 11971 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 12231 11971 145 145 0 12086 0
[pid=2092] vsize: 48924
Current children cumulated CPU time (s) 1129.06
Current children cumulated vsize (Kb) 51048

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 12263 0 0 0 113806 98 0 0 25 0 1 0 1844021973 50098176 11971 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 12231 11971 145 145 0 12086 0
[pid=2092] vsize: 48924
Current children cumulated CPU time (s) 1139.06
Current children cumulated vsize (Kb) 51048

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 12263 0 0 0 114806 98 0 0 25 0 1 0 1844021973 50098176 11971 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2092/statm): 12231 11971 145 145 0 12086 0
[pid=2092] vsize: 48924
Current children cumulated CPU time (s) 1149.06
Current children cumulated vsize (Kb) 51048

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 12263 0 0 0 115806 99 0 0 25 0 1 0 1844021973 50098176 11971 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 12231 11971 145 145 0 12086 0
[pid=2092] vsize: 48924
Current children cumulated CPU time (s) 1159.07
Current children cumulated vsize (Kb) 51048

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 12788 0 0 0 116796 103 0 0 25 0 1 0 1844021973 52236288 12496 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 12753 12496 145 145 0 12608 0
[pid=2092] vsize: 51012
Current children cumulated CPU time (s) 1169.01
Current children cumulated vsize (Kb) 53136

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 13088 0 0 0 117791 105 0 0 25 0 1 0 1844021973 53456896 12796 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 13051 12796 145 145 0 12906 0
[pid=2092] vsize: 52204
Current children cumulated CPU time (s) 1178.98
Current children cumulated vsize (Kb) 54328

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 13088 0 0 0 118791 106 0 0 25 0 1 0 1844021973 53456896 12796 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 13051 12796 145 145 0 12906 0
[pid=2092] vsize: 52204
Current children cumulated CPU time (s) 1188.99
Current children cumulated vsize (Kb) 54328

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 13088 0 0 0 119790 106 0 0 25 0 1 0 1844021973 53456896 12796 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 13051 12796 145 145 0 12906 0
[pid=2092] vsize: 52204
Current children cumulated CPU time (s) 1198.98
Current children cumulated vsize (Kb) 54328

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 13088 0 0 0 120790 106 0 0 25 0 1 0 1844021973 53456896 12796 4294967295 134512640 135094434 3221224432 3221223024 134557022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 13051 12796 145 145 0 12906 0
[pid=2092] vsize: 52204
Current children cumulated CPU time (s) 1208.98
Current children cumulated vsize (Kb) 54328



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2092
Raw data (/proc/2088/stat): 2088 (minisat+_script) S 2087 2088 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1844021968 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/2088/statm): 531 226 485 147 0 384 0
[pid=2088] vsize: 2124
Raw data (/proc/2092/stat): 2092 (minisat+_64-bit) R 2088 2088 21452 0 -1 0 13088 0 0 0 120790 106 0 0 25 0 1 0 1844021973 53456896 12796 4294967295 134512640 135094434 3221224432 3221223024 134557022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2092/statm): 13051 12796 145 145 0 12906 0
[pid=2092] vsize: 52204
Current children cumulated CPU time (s) 1208.98
Current children cumulated vsize (Kb) 54328

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

Child status: 10
Real time (s): 1210.15
CPU time (s): 1209
CPU user time (s): 1207.91
CPU system time (s): 1.09483
CPU usage (%): 99.9052
Max. virtual memory (cumulated for all children) (Kb): 54328

Verifier Data

ERROR: no interpretation found !