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:98.opb
MD5SUMa89f4ed95903fddf213992506514bcf0
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 15
Optimality of the best value was proved NO
Number of terms in the objective function 906
Biggest coefficient in the objective function 553
Number of bits for the biggest coefficient in the objective function 10
Sum of the numbers in the objective function 2526
Number of bits of the sum of numbers in the objective function 12
Biggest number in a constraint 553
Number of bits of the biggest number in a constraint 10
Biggest sum of numbers in a constraint 2526
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 benchmark1223.74
Number of variables906
Total number of constraints1944
Number of constraints which are clauses852
Number of constraints which are cardinality constraints (but not clauses)1092
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint18

Trace number 2360

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        931940 kB
Buffers:         28424 kB
Cached:          47356 kB
SwapCached:        516 kB
Active:          28784 kB
Inactive:        49420 kB
HighTotal:      131008 kB
HighFree:        79660 kB
LowTotal:       903652 kB
LowFree:        852280 kB
SwapTotal:     2097892 kB
SwapFree:      2096672 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5680 kB
Slab:            18760 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 19:31:50 (client local time) WITH STATUS 10 IN 1209.07 SECONDS
stats: 2740 7 1209.07 10

Solver Data

c Parsing PB file...
c Converting 1038 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 187]---> BDD-cost:    5
c ---[ 186]---> BDD-cost:    8
c ---[ 185]---> BDD-cost:   14
c ---[ 184]---> BDD-cost:   14
c ---[ 183]---> BDD-cost:   17
c ---[ 182]---> BDD-cost:   14
c ---[ 181]---> BDD-cost:   23
c ---[ 180]---> BDD-cost:   20
c ---[ 179]---> BDD-cost:   29
c ---[ 178]---> BDD-cost:   29
c ---[ 177]---> BDD-cost:   38
c ---[ 176]---> BDD-cost:   32
c ---[ 175]---> BDD-cost:   32
c ---[ 174]---> BDD-cost:   23
c ---[ 173]---> BDD-cost:   26
c ---[ 172]---> BDD-cost:   20
c ---[ 171]---> BDD-cost:   20
c ---[ 170]---> BDD-cost:   14
c ---[ 169]---> BDD-cost:   14
c ---[ 168]---> BDD-cost:    8
c ---[ 167]---> BDD-cost:    8
c ---[ 166]---> BDD-cost:   11
c ---[ 165]---> BDD-cost:   14
c ---[ 164]---> BDD-cost:   17
c ---[ 163]---> BDD-cost:   18
c ---[ 162]---> BDD-cost:   18
c ---[ 161]---> BDD-cost:   35
c ---[ 160]---> BDD-cost:   35
c ---[ 159]---> BDD-cost:   41
c ---[ 158]---> BDD-cost:   35
c ---[ 157]---> BDD-cost:   38
c ---[ 156]---> BDD-cost:   38
c ---[ 155]---> BDD-cost:   41
c ---[ 154]---> BDD-cost:   35
c ---[ 153]---> BDD-cost:   38
c ---[ 152]---> BDD-cost:   23
c ---[ 151]---> BDD-cost:   20
c ---[ 150]---> BDD-cost:   17
c ---[ 149]---> BDD-cost:   20
c ---[ 148]---> BDD-cost:   11
c ---[ 147]---> BDD-cost:    8
c ---[ 146]---> BDD-cost:   11
c ---[ 145]---> BDD-cost:   14
c ---[ 144]---> BDD-cost:   17
c ---[ 143]---> BDD-cost:   23
c ---[ 142]---> BDD-cost:   29
c ---[ 141]---> BDD-cost:   41
c ---[ 140]---> BDD-cost:   44
c ---[ 139]---> BDD-cost:   44
c ---[ 138]---> BDD-cost:   38
c ---[ 137]---> BDD-cost:   39
c ---[ 136]---> BDD-cost:   41
c ---[ 135]---> BDD-cost:   44
c ---[ 134]---> BDD-cost:   44
c ---[ 133]---> BDD-cost:   41
c ---[ 132]---> BDD-cost:   29
c ---[ 131]---> BDD-cost:   29
c ---[ 130]---> BDD-cost:   23
c ---[ 129]---> BDD-cost:   26
c ---[ 128]---> BDD-cost:   14
c ---[ 127]---> BDD-cost:    8
c ---[ 126]---> BDD-cost:   11
c ---[ 125]---> BDD-cost:   14
c ---[ 124]---> BDD-cost:   17
c ---[ 123]---> BDD-cost:   21
c ---[ 122]---> BDD-cost:   29
c ---[ 121]---> BDD-cost:   35
c ---[ 120]---> BDD-cost:   44
c ---[ 119]---> BDD-cost:   47
c ---[ 118]---> BDD-cost:   44
c ---[ 117]---> BDD-cost:   44
c ---[ 116]---> BDD-cost:   44
c ---[ 115]---> BDD-cost:   41
c ---[ 114]---> BDD-cost:   38
c ---[ 113]---> BDD-cost:   35
c ---[ 112]---> BDD-cost:   32
c ---[ 111]---> BDD-cost:   29
c ---[ 110]---> BDD-cost:   26
c ---[ 109]---> BDD-cost:   20
c ---[ 108]---> BDD-cost:    6
c ---[ 107]---> BDD-cost:    5
c ---[ 106]---> BDD-cost:   14
c ---[ 105]---> BDD-cost:   20
c ---[ 104]---> BDD-cost:   23
c ---[ 103]---> BDD-cost:   26
c ---[ 102]---> BDD-cost:   35
c ---[ 101]---> BDD-cost:   38
c ---[ 100]---> BDD-cost:   35
c ---[  99]---> BDD-cost:   41
c ---[  98]---> BDD-cost:   44
c ---[  97]---> BDD-cost:   41
c ---[  96]---> BDD-cost:   38
c ---[  95]---> BDD-cost:   41
c ---[  94]---> BDD-cost:   38
c ---[  93]---> BDD-cost:   29
c ---[  92]---> BDD-cost:   20
c ---[  91]---> BDD-cost:   26
c ---[  90]---> BDD-cost:   20
c ---[  89]---> BDD-cost:   14
c ---[  88]---> BDD-cost:    5
c ---[  87]---> BDD-cost:    5
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   20
c ---[  84]---> BDD-cost:   20
c ---[  83]---> BDD-cost:   32
c ---[  82]---> BDD-cost:   41
c ---[  81]---> BDD-cost:   38
c ---[  80]---> BDD-cost:   35
c ---[  79]---> BDD-cost:   32
c ---[  78]---> BDD-cost:   35
c ---[  77]---> BDD-cost:   44
c ---[  76]---> BDD-cost:   35
c ---[  75]---> BDD-cost:   38
c ---[  74]---> BDD-cost:   35
c ---[  73]---> BDD-cost:   29
c ---[  72]---> BDD-cost:   23
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   17
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    7
c ---[  66]---> BDD-cost:   11
c ---[  65]---> BDD-cost:   17
c ---[  64]---> BDD-cost:   23
c ---[  63]---> BDD-cost:   32
c ---[  62]---> BDD-cost:   26
c ---[  61]---> BDD-cost:   38
c ---[  60]---> BDD-cost:   32
c ---[  59]---> BDD-cost:   32
c ---[  58]---> BDD-cost:   35
c ---[  57]---> BDD-cost:   38
c ---[  56]---> BDD-cost:   32
c ---[  55]---> BDD-cost:   35
c ---[  54]---> BDD-cost:   29
c ---[  53]---> BDD-cost:   32
c ---[  52]---> BDD-cost:   29
c ---[  51]---> BDD-cost:   23
c ---[  50]---> BDD-cost:   17
c ---[  49]---> BDD-cost:   11
c ---[  47]---> BDD-cost:    8
c ---[  46]---> BDD-cost:   20
c ---[  45]---> BDD-cost:   14
c ---[  44]---> BDD-cost:   17
c ---[  43]---> BDD-cost:   20
c ---[  42]---> BDD-cost:   20
c ---[  41]---> BDD-cost:   35
c ---[  40]---> BDD-cost:   35
c ---[  39]---> BDD-cost:   35
c ---[  38]---> BDD-cost:   23
c ---[  37]---> BDD-cost:   26
c ---[  36]---> BDD-cost:   23
c ---[  35]---> BDD-cost:   23
c ---[  34]---> BDD-cost:   23
c ---[  33]---> BDD-cost:   26
c ---[  32]---> BDD-cost:   17
c ---[  31]---> BDD-cost:    5
c ---[  30]---> BDD-cost:    8
c ---[  29]---> BDD-cost:   14
c ---[  28]---> BDD-cost:   14
c ---[  27]---> BDD-cost:   14
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   20
c ---[  24]---> BDD-cost:   26
c ---[  23]---> BDD-cost:   17
c ---[  22]---> BDD-cost:   15
c ---[  21]---> BDD-cost:   20
c ---[  20]---> BDD-cost:   20
c ---[  19]---> BDD-cost:   17
c ---[  18]---> BDD-cost:   20
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:    8
c ---[  14]---> BDD-cost:    7
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:   14
c ---[  11]---> BDD-cost:   11
c ---[  10]---> BDD-cost:   17
c ---[   9]---> BDD-cost:   14
c ---[   8]---> BDD-cost:   14
c ---[   7]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   14
c ---[   5]---> BDD-cost:   14
c ---[   4]---> BDD-cost:   17
c ---[   3]---> BDD-cost:   14
c ---[   2]---> BDD-cost:   14
c ---[   1]---> BDD-cost:    8
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   11181    31975 |    3727       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 959
c ---[   0]---> Adder-cost: 2188   maxlim: 461   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   26442    86478 |    8814       0        0     nan |  0.000 % |
c |       100 |   26442    86478 |    9695     100      380     3.8 |  2.547 % |
c |       250 |   26433    86447 |   10664     248     1059     4.3 |  2.560 % |
c |       476 |   26433    86447 |   11731     474     2412     5.1 |  2.560 % |
c ==============================================================================
c Found solution: 206
c ---[   0]---> Adder-cost: 2   maxlim: 1214   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       806 |   26471    86617 |    8823     804     4288     5.3 |  2.560 % |
c ==============================================================================
c Found solution: 143
c ---[   0]---> Adder-cost: 0   maxlim: 1277   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       814 |   26480    86667 |    8826     812     4330     5.3 |  2.560 % |
c |       914 |   26480    86667 |    9708     912     8172     9.0 |  2.738 % |
c |      1064 |   26480    86667 |   10679    1062     8878     8.4 |  2.738 % |
c |      1289 |   26480    86667 |   11747    1287    13915    10.8 |  2.738 % |
c |      1626 |   26480    86667 |   12922    1624    15594     9.6 |  2.738 % |
c |      2132 |   26480    86667 |   14214    2130    18615     8.7 |  2.738 % |
c |      2892 |   26480    86667 |   15635    2890    40463    14.0 |  2.738 % |
c |      4031 |   26480    86667 |   17199    4029    61525    15.3 |  2.738 % |
c |      5740 |   26480    86667 |   18919    5738   145592    25.4 |  2.738 % |
c |      8302 |   26480    86667 |   20811    8300   400387    48.2 |  2.738 % |
c |     12147 |   26480    86667 |   22892   12145   750271    61.8 |  2.738 % |
c ==============================================================================
c Found solution: 130
c ---[   0]---> Adder-cost: 0   maxlim: 1290   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14029 |   26485    86701 |    8828   14027   824966    58.8 |  2.738 % |
c |     14129 |   26485    86701 |    9710    7114   431246    60.6 |  2.789 % |
c |     14279 |   26485    86701 |   10681    7264   431919    59.5 |  2.789 % |
c |     14505 |   26485    86701 |   11750    7490   433807    57.9 |  2.789 % |
c |     14842 |   26485    86701 |   12925    7827   440942    56.3 |  2.789 % |
c |     15349 |   26485    86701 |   14217    8334   463419    55.6 |  2.789 % |
c |     16108 |   26485    86701 |   15639    9093   482022    53.0 |  2.789 % |
c |     17247 |   26485    86701 |   17203   10232   538561    52.6 |  2.789 % |
c |     18955 |   26485    86701 |   18923   11940   602513    50.5 |  2.789 % |
c |     21519 |   26485    86701 |   20815   14504   833364    57.5 |  2.789 % |
c ==============================================================================
c Found solution: 127
c ---[   0]---> Adder-cost: 0   maxlim: 1293   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23171 |   26489    86723 |    8829   16156   882076    54.6 |  2.789 % |
c |     23272 |   26489    86723 |    9711    8179   357304    43.7 |  2.814 % |
c |     23422 |   26489    86723 |   10683    8329   358840    43.1 |  2.814 % |
c |     23647 |   26489    86723 |   11751    8554   363731    42.5 |  2.814 % |
c |     23984 |   26489    86723 |   12926    8891   369197    41.5 |  2.814 % |
c |     24490 |   26489    86723 |   14219    9397   396462    42.2 |  2.814 % |
c |     25250 |   26489    86723 |   15641   10157   425636    41.9 |  2.814 % |
c |     26389 |   26489    86723 |   17205   11296   470056    41.6 |  2.814 % |
c |     28097 |   26489    86723 |   18925   13004   538210    41.4 |  2.814 % |
c |     30662 |   26489    86723 |   20818   15569   771366    49.5 |  2.814 % |
c |     34507 |   26489    86723 |   22900   19414  1108591    57.1 |  2.814 % |
c |     40273 |   26489    86723 |   25190   25180  1530602    60.8 |  2.814 % |
c ==============================================================================
c Found solution: 117
c ---[   0]---> Adder-cost: 0   maxlim: 1303   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47450 |   26491    86738 |    8830   18237  1218106    66.8 |  2.814 % |
c |     47550 |   26491    86738 |    9713    4660   289106    62.0 |  2.839 % |
c |     47700 |   26491    86738 |   10684    4810   290323    60.4 |  2.839 % |
c |     47925 |   26491    86738 |   11752    5035   300392    59.7 |  2.839 % |
c |     48262 |   26491    86738 |   12928    5372   302069    56.2 |  2.839 % |
c |     48768 |   26491    86738 |   14220    5878   320891    54.6 |  2.839 % |
c |     49527 |   26491    86738 |   15642    6637   330420    49.8 |  2.839 % |
c |     50666 |   26491    86738 |   17207    7776   374858    48.2 |  2.839 % |
c |     52374 |   26491    86738 |   18927    9484   530806    56.0 |  2.839 % |
c |     54937 |   26491    86738 |   20820   12047   686209    57.0 |  2.839 % |
c |     58782 |   26491    86738 |   22902   15892   975705    61.4 |  2.839 % |
c ==============================================================================
c Found solution: 109
c ---[   0]---> Adder-cost: 0   maxlim: 1311   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     60887 |   26492    86744 |    8830   17997  1087821    60.4 |  2.839 % |
c |     60987 |   26492    86744 |    9713    9099   440274    48.4 |  2.852 % |
c |     61137 |   26492    86744 |   10684    9249   442243    47.8 |  2.852 % |
c |     61363 |   26492    86744 |   11752    9475   447923    47.3 |  2.852 % |
c |     61701 |   26492    86744 |   12928    9813   460334    46.9 |  2.852 % |
c |     62209 |   26492    86744 |   14220   10321   482479    46.7 |  2.852 % |
c |     62968 |   26492    86744 |   15642   11080   518644    46.8 |  2.852 % |
c |     64109 |   26492    86744 |   17207   12221   575864    47.1 |  2.852 % |
c |     65817 |   26492    86744 |   18927   13929   671448    48.2 |  2.852 % |
c |     68380 |   26492    86744 |   20820   16492   791321    48.0 |  2.852 % |
c |     72224 |   26492    86744 |   22902   20336  1038178    51.1 |  2.852 % |
c |     77993 |   26492    86744 |   25193   26105  1602134    61.4 |  2.852 % |
c |     86642 |   26492    86744 |   27712   21702  1613426    74.3 |  2.852 % |
c ==============================================================================
c Found solution: 107
c ---[   0]---> Adder-cost: 0   maxlim: 1313   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90492 |   26493    86754 |    8831   25552  1851614    72.5 |  2.852 % |
c |     90592 |   26493    86754 |    9714    6488   296083    45.6 |  2.865 % |
c |     90742 |   26493    86754 |   10685    6638   298105    44.9 |  2.865 % |
c |     90967 |   26493    86754 |   11754    6863   301577    43.9 |  2.865 % |
c |     91304 |   26493    86754 |   12929    7200   303911    42.2 |  2.865 % |
c |     91810 |   26493    86754 |   14222    7706   318504    41.3 |  2.865 % |
c |     92569 |   26493    86754 |   15644    8465   366545    43.3 |  2.865 % |
c |     93708 |   26493    86754 |   17209    9604   427191    44.5 |  2.865 % |
c |     95418 |   26493    86754 |   18930   11314   506391    44.8 |  2.865 % |
c |     97982 |   26493    86754 |   20823   13878   666721    48.0 |  2.865 % |
c |    101827 |   26493    86754 |   22905   17723  1003862    56.6 |  2.865 % |
c |    107595 |   26493    86754 |   25195   23491  1603772    68.3 |  2.865 % |
c |    116244 |   26493    86754 |   27715   18209  2007969   110.3 |  2.865 % |
c |    129219 |   26493    86754 |   30487   14477  1299051    89.7 |  2.865 % |
c |    148680 |   26493    86754 |   33535   33938  3505926   103.3 |  2.865 % |
c |    177873 |   26493    86754 |   36889   19569  1981304   101.2 |  2.865 % |
c ==============================================================================
c Found solution: 106
c ---[   0]---> Adder-cost: 0   maxlim: 1314   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    203130 |   26495    86767 |    8831   17932  2342869   130.7 |  2.865 % |
c |    203230 |   26495    86767 |    9714    9066  1059460   116.9 |  2.877 % |
c |    203380 |   26495    86767 |   10685    9216  1060308   115.1 |  2.877 % |
c |    203605 |   26495    86767 |   11754    9441  1061663   112.5 |  2.877 % |
c |    203942 |   26495    86767 |   12929    9778  1064191   108.8 |  2.877 % |
c |    204450 |   26495    86767 |   14222   10286  1076718   104.7 |  2.877 % |
c |    205211 |   26495    86767 |   15644   11047  1099524    99.5 |  2.877 % |
c |    206350 |   26495    86767 |   17209   12186  1151779    94.5 |  2.877 % |
c |    208058 |   26495    86767 |   18930   13894  1290178    92.9 |  2.877 % |
c |    210620 |   26495    86767 |   20823   16456  1424602    86.6 |  2.877 % |
c |    214466 |   26495    86767 |   22905   20302  1945374    95.8 |  2.877 % |
c |    220234 |   26495    86767 |   25195   13589  1290861    95.0 |  2.877 % |
c |    228886 |   26495    86767 |   27715   22241  2221897    99.9 |  2.877 % |
c |    241860 |   26495    86767 |   30487   16824  1624022    96.5 |  2.877 % |
c |    261324 |   26495    86767 |   33535   18036  1297748    72.0 |  2.877 % |
c |    290519 |   26495    86767 |   36889   27027  2715164   100.5 |  2.877 % |
c |    334311 |   26495    86767 |   40578   18135  1843579   101.7 |  2.877 % |
c |    399995 |   26495    86767 |   44636   25387  6045749   238.1 |  2.877 % |
c ==============================================================================
c Found solution: 98
c ---[   0]---> Adder-cost: 0   maxlim: 1322   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    445674 |   26500    86799 |    8833   37759  6320294   167.4 |  2.877 % |
c |    445774 |   26500    86799 |    9716    6732   774985   115.1 |  2.915 % |
c |    445924 |   26500    86799 |   10687    6882   775935   112.7 |  2.915 % |
c |    446151 |   26500    86799 |   11756    7109   777542   109.4 |  2.915 % |
c |    446488 |   26500    86799 |   12932    7446   782594   105.1 |  2.915 % |
c |    446994 |   26500    86799 |   14225    7952   795902   100.1 |  2.915 % |
c |    447753 |   26500    86799 |   15648    8711   803084    92.2 |  2.915 % |
c |    448892 |   26500    86799 |   17213    9850   821221    83.4 |  2.915 % |
c |    450600 |   26500    86799 |   18934   11558   878453    76.0 |  2.915 % |
c |    453165 |   26500    86799 |   20827   14123  1062292    75.2 |  2.915 % |
c |    457009 |   26500    86799 |   22910   17967  1272621    70.8 |  2.915 % |
c |    462775 |   26500    86799 |   25201   11982   661214    55.2 |  2.915 % |
c |    471427 |   26500    86799 |   27721   20634  1378808    66.8 |  2.915 % |
c |    484402 |   26500    86799 |   30493   14154  2586201   182.7 |  2.915 % |
c |    503864 |   26500    86799 |   33543   33616  5188761   154.4 |  2.915 % |
c |    533056 |   26500    86799 |   36897   18884  2969903   157.3 |  2.915 % |
c |    576845 |   26500    86799 |   40587   35392  5877484   166.1 |  2.915 % |
c |    642534 |   26500    86799 |   44646   42901  8342933   194.5 |  2.915 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v785 v740 v420 v82 -v860 v744 v418 -v859 -v784 v501 -v307 -v85 v788 v419 -v86 -v63 -v861 v504 -v424 v354 -v306 -v62 v863 -v789 -v573 v505 -v64 -v572 -v478 -v441 v353 -v312 -v65 -v27 v864 -v574 -v477 -v310 -v102 v66 v866 -v810 v575 -v479 -v440 -v359 -v262 -v185 -v101 v73 v26 v867 -v814 v576 -v482 -v357 -v311 -v190 v107 -v67 -v30 -v697 v583 v481 -v446 -v399 -v315 -v265 -v216 -v189 -v143 v106 -v68 -v701 v577 v486 -v444 -v358 -v266 -v142 v108 -v69 -v31 -v2 -v578 v485 -v398 v362 v192 -v166 -v144 v112 -v1 -v660 -v579 v483 -v445 v193 v147 v111 -v7 -v659 -v594 -v558 v484 -v449 -v404 -v196 v165 v146 v109 -v6 -v661 -v598 -v557 -v402 -v194 v151 v110 -v8 -v662 v559 -v332 -v195 v171 v150 -v12 v663 -v562 -v403 v169 v148 -v11 v668 v561 v407 -v335 v149 -v9 v664 v563 -v336 v170 -v10 v739 v421 v81 -v855 v743 -v854 -v786 v500 v425 -v302 -v87 v790 -v423 -v862 v506 -v349 -v308 v865 v869 -v835 -v792 -v436 v355 -v313 -v90 -v76 v868 -v839 -v793 -v77 -v809 -v586 -v509 -v442 v360 -v316 -v261 -v212 -v72 v28 -v813 -v587 v480 -v314 -v184 v103 -v32 -v696 v582 -v494 -v447 -v394 v363 -v267 -v215 -v186 v104 -v70 -v700 v490 v361 -v191 v105 v580 v489 -v450 -v400 v188 -v161 v116 -v34 -v448 -v197 -v145 -v35 -v3 -v593 -v542 -v405 -v270 v167 -v159 -v4 -v597 -v155 v5 v671 v408 -v331 v172 -v154 -v16 v672 v560 v406 v667 -v571 -v466 -v337 -v173 v567 v470 -v174 v781 v741 -v496 v422 v83 v745 v426 -v787 v502 -v88 -v856 v791 -v301 -v857 -v795 v747 v507 -v303 v91 -v75 v858 -v794 v748 -v348 -v309 -v89 -v74 -v22 v873 -v834 v761 -v585 -v510 v350 v305 -v257 -v21 -v838 -v765 -v584 -v508 -v435 v356 -v317 -v811 -v491 -v437 v352 -v263 -v211 v29 -v815 -v493 -v443 v364 -v33 -v698 -v439 -v268 -v217 v119 -v71 -v37 -v702 -v451 -v393 -v187 v120 -v36 -v817 v581 -v538 v487 -v395 -v271 -v205 -v156 v115 -v818 -v401 -v269 v201 -v160 -v158 -v704 v670 -v595 -v541 v488 v397 -v327 -v220 v200 -v162 v113 v19 -v705 v669 -v599 v409 v168 v20 -v722 -v568 -v333 v164 -v152 -v15 -v726 -v570 v175 v665 v601 -v465 -v338 -v153 -v131 -v13 v602 -v566 v469 v742 v434 -v79 v780 v746 -v495 v430 v84 v782 v750 -v497 v429 v80 v783 v749 v503 v92 -v876 v799 v499 v877 -v805 -v511 -v304 v872 -v836 v804 v760 v325 -v207 -v840 -v764 -v692 -v492 v351 v321 -v256 -v23 -v884 -v870 -v812 -v691 -v372 v320 v258 -v213 v118 -v24 -v888 -v816 -v438 -v368 -v264 v117 v25 -v842 -v820 -v699 -v459 -v367 v260 -v218 -v202 -v41 -v843 -v819 -v703 -v589 -v455 -v272 -v204 -v157 -v707 -v588 -v537 -v454 -v221 -v18 -v706 -v396 -v219 -v17 -v596 -v543 -v417 v198 -v114 -v600 -v569 -v413 -v326 -v163 -v721 v604 -v412 -v328 -v199 -v183 v127 -v725 v603 -v334 -v179 v666 v546 -v467 v330 -v178 v130 -v14 -v564 v471 v339 v903 v433 -v78 -v875 v802 -v754 v427 v100 -v874 -v830 v803 -v498 v96 -v829 v798 -v519 v428 -v322 v95 -v515 v324 -v837 -v796 v762 -v514 -v369 -v841 v806 v766 -v371 -v206 -v883 -v871 -v845 v807 -v456 -v318 -v291 -v208 v44 -v887 -v844 v808 -v693 -v458 v259 -v214 -v203 v45 -v824 -v768 -v694 v533 -v383 -v365 -v319 v280 -v210 -v40 -v769 -v695 v276 -v222 -v711 v619 v539 -v452 -v414 -v366 v275 -v38 v623 -v590 -v416 v591 -v544 -v453 -v180 v592 v461 -v182 -v723 -v608 v547 v460 -v410 v126 -v727 v545 -v329 -v468 -v411 -v347 -v176 v132 -v565 v472 v343 v801 -v431 v97 v800 v99 -v753 -v654 -v516 -v756 -v518 -v323 v755 -v751 v521 v93 -v831 v525 -v370 -v832 -v797 v763 -v512 v287 -v249 v94 v43 -v833 v767 -v457 v42 -v885 -v849 v827 v771 -v513 -v379 -v290 -v277 -v889 v828 -v770 v279 -v209 -v823 -v714 -v382 -v230 -v715 v532 -v415 -v226 v891 -v821 -v710 -v641 v618 v534 -v273 -v225 -v39 v892 -v717 -v645 v622 v540 -v181 -v716 -v708 -v679 v611 v536 -v274 -v122 -v55 -v683 v612 v548 -v724 -v607 -v344 v128 -v728 v462 -v346 v729 -v605 v463 -v240 -v177 v133 v730 v464 -v342 v904 -v432 v98 -v517 -v653 -v752 v520 -v245 -v879 v757 v524 -v878 -v852 -v826 v758 v286 v248 -v853 -v825 v759 -v278 -v886 -v848 v775 -v713 -v378 -v292 -v227 v890 -v712 -v229 v894 -v846 -v384 v893 -v822 -v640 v620 -v610 -v295 -v223 -v51 -v644 v624 -v609 v535 -v709 v678 v556 -v387 -v224 -v54 -v718 v682 -v552 -v345 v121 -v719 -v626 -v551 -v236 v123 v720 -v627 v12

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/26260/stat): 26260 (minisat+_script) R 26259 26260 19316 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843700651 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/26260/statm): 174 3 169 147 0 27 0
[pid=26260] 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=26261
New process pid=26262
New process pid=26263
execve syscall for /bin/sed executable
One traced child (pid=26262) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=26263) exited with status: 0
One traced child (pid=26261) exited with status: 0
New process pid=26264
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-10:20:4.5:0.95:98.opb

[startup+10.0031 s]
Raw data (loadavg): 0.93 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) T 26260 26260 19316 0 -1 0 2621 0 0 0 969 12 0 0 25 0 1 0 1843700656 11137024 2482 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/26264/statm): 2719 2482 145 145 0 2574 0
[pid=26264] vsize: 10876
Current children cumulated CPU time (s) 9.81
Current children cumulated vsize (Kb) 13000

[startup+20.0047 s]
Raw data (loadavg): 0.94 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 2822 0 0 0 1966 14 0 0 25 0 1 0 1843700656 11788288 2642 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 2878 2642 145 145 0 2733 0
[pid=26264] vsize: 11512
Current children cumulated CPU time (s) 19.8
Current children cumulated vsize (Kb) 13636

[startup+30.0053 s]
Raw data (loadavg): 0.95 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 3486 0 0 0 2956 18 0 0 25 0 1 0 1843700656 14532608 3306 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 3548 3306 145 145 0 3403 0
[pid=26264] vsize: 14192
Current children cumulated CPU time (s) 29.74
Current children cumulated vsize (Kb) 16316

[startup+40.0059 s]
Raw data (loadavg): 0.96 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 3735 0 0 0 3951 20 0 0 25 0 1 0 1843700656 15556608 3555 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 3798 3555 145 145 0 3653 0
[pid=26264] vsize: 15192
Current children cumulated CPU time (s) 39.71
Current children cumulated vsize (Kb) 17316

[startup+50.0065 s]
Raw data (loadavg): 0.96 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 3740 0 0 0 4951 20 0 0 25 0 1 0 1843700656 15556608 3560 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 3798 3560 145 145 0 3653 0
[pid=26264] vsize: 15192
Current children cumulated CPU time (s) 49.71
Current children cumulated vsize (Kb) 17316

[startup+60.0061 s]
Raw data (loadavg): 0.97 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 3740 0 0 0 5952 20 0 0 25 0 1 0 1843700656 15556608 3560 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 3798 3560 145 145 0 3653 0
[pid=26264] vsize: 15192
Current children cumulated CPU time (s) 59.72
Current children cumulated vsize (Kb) 17316

[startup+70.0067 s]
Raw data (loadavg): 0.97 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 3828 0 0 0 6951 21 0 0 25 0 1 0 1843700656 15917056 3648 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 3886 3648 145 145 0 3741 0
[pid=26264] vsize: 15544
Current children cumulated CPU time (s) 69.72
Current children cumulated vsize (Kb) 17668

[startup+80.0073 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 4052 0 0 0 7947 22 0 0 25 0 1 0 1843700656 16670720 3832 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 4070 3832 145 145 0 3925 0
[pid=26264] vsize: 16280
Current children cumulated CPU time (s) 79.69
Current children cumulated vsize (Kb) 18404

[startup+90.0079 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 4335 0 0 0 8943 24 0 0 25 0 1 0 1843700656 17829888 4115 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 4353 4115 145 145 0 4208 0
[pid=26264] vsize: 17412
Current children cumulated CPU time (s) 89.67
Current children cumulated vsize (Kb) 19536

[startup+100.009 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 4616 0 0 0 9939 25 0 0 25 0 1 0 1843700656 18980864 4396 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 4634 4396 145 145 0 4489 0
[pid=26264] vsize: 18536
Current children cumulated CPU time (s) 99.64
Current children cumulated vsize (Kb) 20660

[startup+110.009 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 5548 0 0 0 10925 32 0 0 25 0 1 0 1843700656 22794240 5328 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 5565 5328 145 145 0 5420 0
[pid=26264] vsize: 22260
Current children cumulated CPU time (s) 109.57
Current children cumulated vsize (Kb) 24384

[startup+120.011 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 5563 0 0 0 11925 32 0 0 25 0 1 0 1843700656 22851584 5343 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 5579 5343 145 145 0 5434 0
[pid=26264] vsize: 22316
Current children cumulated CPU time (s) 119.57
Current children cumulated vsize (Kb) 24440

[startup+130.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 5563 0 0 0 12925 32 0 0 25 0 1 0 1843700656 22851584 5343 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 5579 5343 145 145 0 5434 0
[pid=26264] vsize: 22316
Current children cumulated CPU time (s) 129.57
Current children cumulated vsize (Kb) 24440

[startup+140.011 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 5882 0 0 0 13919 35 0 0 25 0 1 0 1843700656 24289280 5662 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 5930 5662 145 145 0 5785 0
[pid=26264] vsize: 23720
Current children cumulated CPU time (s) 139.54
Current children cumulated vsize (Kb) 25844

[startup+150.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 5882 0 0 0 14919 35 0 0 25 0 1 0 1843700656 24289280 5662 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 5930 5662 145 145 0 5785 0
[pid=26264] vsize: 23720
Current children cumulated CPU time (s) 149.54
Current children cumulated vsize (Kb) 25844

[startup+160.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 5882 0 0 0 15920 35 0 0 25 0 1 0 1843700656 24289280 5662 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 5930 5662 145 145 0 5785 0
[pid=26264] vsize: 23720
Current children cumulated CPU time (s) 159.55
Current children cumulated vsize (Kb) 25844

[startup+170.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 6425 0 0 0 16910 39 0 0 25 0 1 0 1843700656 26505216 6205 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 6471 6205 145 145 0 6326 0
[pid=26264] vsize: 25884
Current children cumulated CPU time (s) 169.49
Current children cumulated vsize (Kb) 28008

[startup+180.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 6425 0 0 0 17909 39 0 0 25 0 1 0 1843700656 26505216 6205 4294967295 134512640 135094434 3221224432 3221223072 134538540 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 6471 6205 145 145 0 6326 0
[pid=26264] vsize: 25884
Current children cumulated CPU time (s) 179.48
Current children cumulated vsize (Kb) 28008

[startup+190.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 6425 0 0 0 18909 40 0 0 25 0 1 0 1843700656 26505216 6205 4294967295 134512640 135094434 3221224432 3221223024 134552008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 6471 6205 145 145 0 6326 0
[pid=26264] vsize: 25884
Current children cumulated CPU time (s) 189.49
Current children cumulated vsize (Kb) 28008

[startup+200.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 6569 0 0 0 19906 41 0 0 25 0 1 0 1843700656 27095040 6349 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 6615 6349 145 145 0 6470 0
[pid=26264] vsize: 26460
Current children cumulated CPU time (s) 199.47
Current children cumulated vsize (Kb) 28584

[startup+210.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7453 0 0 0 20892 48 0 0 25 0 1 0 1843700656 30711808 7233 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 7498 7233 145 145 0 7353 0
[pid=26264] vsize: 29992
Current children cumulated CPU time (s) 209.4
Current children cumulated vsize (Kb) 32116

[startup+220.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 21884 51 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0
[pid=26264] vsize: 31796
Current children cumulated CPU time (s) 219.35
Current children cumulated vsize (Kb) 33920

[startup+230.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 22884 51 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223056 134557728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0
[pid=26264] vsize: 31796
Current children cumulated CPU time (s) 229.35
Current children cumulated vsize (Kb) 33920

[startup+240.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 23883 52 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0
[pid=26264] vsize: 31796
Current children cumulated CPU time (s) 239.35
Current children cumulated vsize (Kb) 33920

[startup+250.02 s]
Raw data (loadavg): 0.99 0.97 0.98 3/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 24883 52 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0
[pid=26264] vsize: 31796
Current children cumulated CPU time (s) 249.35
Current children cumulated vsize (Kb) 33920

[startup+260.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 25883 53 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0
[pid=26264] vsize: 31796
Current children cumulated CPU time (s) 259.36
Current children cumulated vsize (Kb) 33920

[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 26882 53 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0
[pid=26264] vsize: 31796
Current children cumulated CPU time (s) 269.35
Current children cumulated vsize (Kb) 33920

[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 27883 53 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0
[pid=26264] vsize: 31796
Current children cumulated CPU time (s) 279.36
Current children cumulated vsize (Kb) 33920

[startup+290.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 28882 54 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0
[pid=26264] vsize: 31796
Current children cumulated CPU time (s) 289.36
Current children cumulated vsize (Kb) 33920

[startup+300.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 29881 54 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0
[pid=26264] vsize: 31796
Current children cumulated CPU time (s) 299.35
Current children cumulated vsize (Kb) 33920

[startup+310.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 30881 54 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0
[pid=26264] vsize: 31796
Current children cumulated CPU time (s) 309.35
Current children cumulated vsize (Kb) 33920

[startup+320.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 31880 55 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0
[pid=26264] vsize: 31796
Current children cumulated CPU time (s) 319.35
Current children cumulated vsize (Kb) 33920

[startup+330.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 32880 55 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0
[pid=26264] vsize: 31796
Current children cumulated CPU time (s) 329.35
Current children cumulated vsize (Kb) 33920

[startup+340.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 33879 56 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0
[pid=26264] vsize: 31796
Current children cumulated CPU time (s) 339.35
Current children cumulated vsize (Kb) 33920

[startup+350.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 34880 56 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0
[pid=26264] vsize: 31796
Current children cumulated CPU time (s) 349.36
Current children cumulated vsize (Kb) 33920

[startup+360.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 35880 56 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0
[pid=26264] vsize: 31796
Current children cumulated CPU time (s) 359.36
Current children cumulated vsize (Kb) 33920

[startup+370.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 36880 57 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223024 134557321 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0
[pid=26264] vsize: 31796
Current children cumulated CPU time (s) 369.37
Current children cumulated vsize (Kb) 33920

[startup+380.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 37880 57 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0
[pid=26264] vsize: 31796
Current children cumulated CPU time (s) 379.37
Current children cumulated vsize (Kb) 33920

[startup+390.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 38880 57 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0
[pid=26264] vsize: 31796
Current children cumulated CPU time (s) 389.37
Current children cumulated vsize (Kb) 33920

[startup+400.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 39880 57 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0
[pid=26264] vsize: 31796
Current children cumulated CPU time (s) 399.37
Current children cumulated vsize (Kb) 33920

[startup+410.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 8271 0 0 0 40875 59 0 0 25 0 1 0 1843700656 34054144 8051 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 8314 8051 145 145 0 8169 0
[pid=26264] vsize: 33256
Current children cumulated CPU time (s) 409.34
Current children cumulated vsize (Kb) 35380

[startup+420.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 9065 0 0 0 41860 65 0 0 25 0 1 0 1843700656 37289984 8845 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 9104 8845 145 145 0 8959 0
[pid=26264] vsize: 36416
Current children cumulated CPU time (s) 419.25
Current children cumulated vsize (Kb) 38540

[startup+430.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 9065 0 0 0 42860 65 0 0 25 0 1 0 1843700656 37289984 8845 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 9104 8845 145 145 0 8959 0
[pid=26264] vsize: 36416
Current children cumulated CPU time (s) 429.25
Current children cumulated vsize (Kb) 38540

[startup+440.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 9070 0 0 0 43860 65 0 0 25 0 1 0 1843700656 37322752 8850 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 9112 8850 145 145 0 8967 0
[pid=26264] vsize: 36448
Current children cumulated CPU time (s) 439.25
Current children cumulated vsize (Kb) 38572

[startup+450.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 9070 0 0 0 44860 65 0 0 25 0 1 0 1843700656 37322752 8850 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 9112 8850 145 145 0 8967 0
[pid=26264] vsize: 36448
Current children cumulated CPU time (s) 449.25
Current children cumulated vsize (Kb) 38572

[startup+460.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 9298 0 0 0 45856 66 0 0 25 0 1 0 1843700656 38256640 9078 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 9340 9078 145 145 0 9195 0
[pid=26264] vsize: 37360
Current children cumulated CPU time (s) 459.22
Current children cumulated vsize (Kb) 39484

[startup+470.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 10147 0 0 0 46842 73 0 0 25 0 1 0 1843700656 41754624 9927 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 10194 9927 145 145 0 10049 0
[pid=26264] vsize: 40776
Current children cumulated CPU time (s) 469.15
Current children cumulated vsize (Kb) 42900

[startup+480.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 10860 0 0 0 47831 78 0 0 25 0 1 0 1843700656 44675072 10640 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 10907 10640 145 145 0 10762 0
[pid=26264] vsize: 43628
Current children cumulated CPU time (s) 479.09
Current children cumulated vsize (Kb) 45752

[startup+490.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 11618 0 0 0 48819 84 0 0 25 0 1 0 1843700656 47800320 11398 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 11670 11398 145 145 0 11525 0
[pid=26264] vsize: 46680
Current children cumulated CPU time (s) 489.03
Current children cumulated vsize (Kb) 48804

[startup+500.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 12351 0 0 0 49806 89 0 0 25 0 1 0 1843700656 50802688 12131 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 12403 12131 145 145 0 12258 0
[pid=26264] vsize: 49612
Current children cumulated CPU time (s) 498.95
Current children cumulated vsize (Kb) 51736

[startup+510.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13066 0 0 0 50794 95 0 0 25 0 1 0 1843700656 53755904 12846 4294967295 134512640 135094434 3221224432 3221223024 134557277 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13124 12846 145 145 0 12979 0
[pid=26264] vsize: 52496
Current children cumulated CPU time (s) 508.89
Current children cumulated vsize (Kb) 54620

[startup+520.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13274 0 0 0 51791 96 0 0 25 0 1 0 1843700656 54607872 13054 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13332 13054 145 145 0 13187 0
[pid=26264] vsize: 53328
Current children cumulated CPU time (s) 518.87
Current children cumulated vsize (Kb) 55452

[startup+530.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13274 0 0 0 52791 96 0 0 25 0 1 0 1843700656 54607872 13054 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13332 13054 145 145 0 13187 0
[pid=26264] vsize: 53328
Current children cumulated CPU time (s) 528.87
Current children cumulated vsize (Kb) 55452

[startup+540.041 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13275 0 0 0 53792 96 0 0 25 0 1 0 1843700656 54607872 13055 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 13332 13055 145 145 0 13187 0
[pid=26264] vsize: 53328
Current children cumulated CPU time (s) 538.88
Current children cumulated vsize (Kb) 55452

[startup+550.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13275 0 0 0 54791 96 0 0 25 0 1 0 1843700656 54607872 13055 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13332 13055 145 145 0 13187 0
[pid=26264] vsize: 53328
Current children cumulated CPU time (s) 548.87
Current children cumulated vsize (Kb) 55452

[startup+560.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13275 0 0 0 55791 97 0 0 25 0 1 0 1843700656 54607872 13055 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13332 13055 145 145 0 13187 0
[pid=26264] vsize: 53328
Current children cumulated CPU time (s) 558.88
Current children cumulated vsize (Kb) 55452

[startup+570.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13275 0 0 0 56792 97 0 0 25 0 1 0 1843700656 54607872 13055 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13332 13055 145 145 0 13187 0
[pid=26264] vsize: 53328
Current children cumulated CPU time (s) 568.89
Current children cumulated vsize (Kb) 55452

[startup+580.043 s]
Raw data (loadavg): 1.07 0.99 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13276 0 0 0 57792 97 0 0 25 0 1 0 1843700656 54607872 13056 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13332 13056 145 145 0 13187 0
[pid=26264] vsize: 53328
Current children cumulated CPU time (s) 578.89
Current children cumulated vsize (Kb) 55452

[startup+590.044 s]
Raw data (loadavg): 1.14 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 58792 97 0 0 25 0 1 0 1843700656 54411264 13010 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13284 13010 145 145 0 13139 0
[pid=26264] vsize: 53136
Current children cumulated CPU time (s) 588.89
Current children cumulated vsize (Kb) 55260

[startup+600.044 s]
Raw data (loadavg): 1.11 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 59792 97 0 0 25 0 1 0 1843700656 54411264 13010 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13284 13010 145 145 0 13139 0
[pid=26264] vsize: 53136
Current children cumulated CPU time (s) 598.89
Current children cumulated vsize (Kb) 55260

[startup+610.045 s]
Raw data (loadavg): 1.10 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 60793 97 0 0 25 0 1 0 1843700656 54411264 13010 4294967295 134512640 135094434 3221224432 3221223024 134557435 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13284 13010 145 145 0 13139 0
[pid=26264] vsize: 53136
Current children cumulated CPU time (s) 608.9
Current children cumulated vsize (Kb) 55260

[startup+620.046 s]
Raw data (loadavg): 1.08 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 61793 97 0 0 25 0 1 0 1843700656 54411264 13010 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13284 13010 145 145 0 13139 0
[pid=26264] vsize: 53136
Current children cumulated CPU time (s) 618.9
Current children cumulated vsize (Kb) 55260

[startup+630.046 s]
Raw data (loadavg): 1.07 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 62793 97 0 0 25 0 1 0 1843700656 54411264 13010 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13284 13010 145 145 0 13139 0
[pid=26264] vsize: 53136
Current children cumulated CPU time (s) 628.9
Current children cumulated vsize (Kb) 55260

[startup+640.048 s]
Raw data (loadavg): 1.06 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 63793 97 0 0 25 0 1 0 1843700656 54411264 13010 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13284 13010 145 145 0 13139 0
[pid=26264] vsize: 53136
Current children cumulated CPU time (s) 638.9
Current children cumulated vsize (Kb) 55260

[startup+650.048 s]
Raw data (loadavg): 1.05 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 64793 97 0 0 25 0 1 0 1843700656 54112256 12937 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13211 12937 145 145 0 13066 0
[pid=26264] vsize: 52844
Current children cumulated CPU time (s) 648.9
Current children cumulated vsize (Kb) 54968

[startup+660.049 s]
Raw data (loadavg): 1.04 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 65793 97 0 0 25 0 1 0 1843700656 54112256 12937 4294967295 134512640 135094434 3221224432 3221223024 134557485 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13211 12937 145 145 0 13066 0
[pid=26264] vsize: 52844
Current children cumulated CPU time (s) 658.9
Current children cumulated vsize (Kb) 54968

[startup+670.05 s]
Raw data (loadavg): 1.03 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 66794 97 0 0 25 0 1 0 1843700656 54112256 12937 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13211 12937 145 145 0 13066 0
[pid=26264] vsize: 52844
Current children cumulated CPU time (s) 668.91
Current children cumulated vsize (Kb) 54968

[startup+680.05 s]
Raw data (loadavg): 1.03 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 67794 97 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 678.91
Current children cumulated vsize (Kb) 54640

[startup+690.052 s]
Raw data (loadavg): 1.02 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 68794 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 688.92
Current children cumulated vsize (Kb) 54640

[startup+700.053 s]
Raw data (loadavg): 1.02 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 69794 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223024 134557372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 698.92
Current children cumulated vsize (Kb) 54640

[startup+710.053 s]
Raw data (loadavg): 1.02 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 70794 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 708.92
Current children cumulated vsize (Kb) 54640

[startup+720.054 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 71794 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 718.92
Current children cumulated vsize (Kb) 54640

[startup+730.054 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 72795 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 728.93
Current children cumulated vsize (Kb) 54640

[startup+740.055 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 73795 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 738.93
Current children cumulated vsize (Kb) 54640

[startup+750.056 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 74795 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 748.93
Current children cumulated vsize (Kb) 54640

[startup+760.056 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 75795 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 758.93
Current children cumulated vsize (Kb) 54640

[startup+770.057 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 76795 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 768.93
Current children cumulated vsize (Kb) 54640

[startup+780.057 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 77795 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 778.93
Current children cumulated vsize (Kb) 54640

[startup+790.058 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 78796 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 788.94
Current children cumulated vsize (Kb) 54640

[startup+800.058 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 79796 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 798.94
Current children cumulated vsize (Kb) 54640

[startup+810.059 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 80796 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 808.94
Current children cumulated vsize (Kb) 54640

[startup+820.061 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 81797 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 818.95
Current children cumulated vsize (Kb) 54640

[startup+830.061 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 82797 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 828.95
Current children cumulated vsize (Kb) 54640

[startup+840.062 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 83797 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223024 134551457 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 838.95
Current children cumulated vsize (Kb) 54640

[startup+850.062 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 84797 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 848.95
Current children cumulated vsize (Kb) 54640

[startup+860.063 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 85797 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 858.95
Current children cumulated vsize (Kb) 54640

[startup+870.064 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 86798 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 868.96
Current children cumulated vsize (Kb) 54640

[startup+880.064 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 87797 99 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 878.96
Current children cumulated vsize (Kb) 54640

[startup+890.068 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 88797 100 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 888.97
Current children cumulated vsize (Kb) 54640

[startup+900.068 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 89797 100 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 898.97
Current children cumulated vsize (Kb) 54640

[startup+910.069 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 90797 101 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 908.98
Current children cumulated vsize (Kb) 54640

[startup+920.071 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 91797 101 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 918.98
Current children cumulated vsize (Kb) 54640

[startup+930.071 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 92797 101 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 928.98
Current children cumulated vsize (Kb) 54640

[startup+940.072 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 93797 101 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 938.98
Current children cumulated vsize (Kb) 54640

[startup+950.072 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 94797 101 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 948.98
Current children cumulated vsize (Kb) 54640

[startup+960.073 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 95797 101 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 958.98
Current children cumulated vsize (Kb) 54640

[startup+970.074 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 96797 101 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 968.98
Current children cumulated vsize (Kb) 54640

[startup+980.074 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 97798 101 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 978.99
Current children cumulated vsize (Kb) 54640

[startup+990.076 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 98797 102 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 988.99
Current children cumulated vsize (Kb) 54640

[startup+1000.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 99798 102 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 999
Current children cumulated vsize (Kb) 54640

[startup+1010.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 100798 102 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1009
Current children cumulated vsize (Kb) 54640

[startup+1020.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 101797 102 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1018.99
Current children cumulated vsize (Kb) 54640

[startup+1030.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 102797 102 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1028.99
Current children cumulated vsize (Kb) 54640

[startup+1040.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 103797 102 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1038.99
Current children cumulated vsize (Kb) 54640

[startup+1050.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 104798 102 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1049
Current children cumulated vsize (Kb) 54640

[startup+1060.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 105798 102 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223104 134556336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1059
Current children cumulated vsize (Kb) 54640

[startup+1070.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 106798 102 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1069
Current children cumulated vsize (Kb) 54640

[startup+1080.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 107798 102 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1079
Current children cumulated vsize (Kb) 54640

[startup+1090.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 108798 102 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1089
Current children cumulated vsize (Kb) 54640

[startup+1100.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 109799 102 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1099.01
Current children cumulated vsize (Kb) 54640

[startup+1110.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 110798 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223024 134557494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1109.01
Current children cumulated vsize (Kb) 54640

[startup+1120.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 111799 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1119.02
Current children cumulated vsize (Kb) 54640

[startup+1130.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 112799 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1129.02
Current children cumulated vsize (Kb) 54640

[startup+1140.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 113799 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1139.02
Current children cumulated vsize (Kb) 54640

[startup+1150.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 114799 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1149.02
Current children cumulated vsize (Kb) 54640

[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 115799 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223104 134555673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1159.02
Current children cumulated vsize (Kb) 54640

[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 116800 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1169.03
Current children cumulated vsize (Kb) 54640

[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 117800 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1179.03
Current children cumulated vsize (Kb) 54640

[startup+1190.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 118800 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1189.03
Current children cumulated vsize (Kb) 54640

[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 119800 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1199.03
Current children cumulated vsize (Kb) 54640

[startup+1210.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 120801 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1209.04
Current children cumulated vsize (Kb) 54640



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 26264
Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26260/statm): 531 226 485 147 0 384 0
[pid=26260] vsize: 2124
Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 120801 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0
[pid=26264] vsize: 52516
Current children cumulated CPU time (s) 1209.04
Current children cumulated vsize (Kb) 54640

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

Child status: 10
Real time (s): 1210.12
CPU time (s): 1209.07
CPU user time (s): 1208.02
CPU system time (s): 1.05884
CPU usage (%): 99.9134
Max. virtual memory (cumulated for all children) (Kb): 55452

Verifier Data

ERROR: no interpretation found !