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

Namemps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-air01.opb
MD5SUM90db1995bd949fc5ac74143a523f3bcf
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 3398
Optimality of the best value was proved YES
Number of terms in the objective function 771
Biggest coefficient in the objective function 3698
Number of bits for the biggest coefficient in the objective function 12
Sum of the numbers in the objective function 1192753
Number of bits of the sum of numbers in the objective function 21
Biggest number in a constraint 3698
Number of bits of the biggest number in a constraint 12
Biggest sum of numbers in a constraint 1192753
Number of bits of the biggest sum of numbers21
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark112.221
Number of variables771
Total number of constraints794
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)794
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint438

Trace number 6116

Launcher Data

LAUNCH ON wulflinc3 THE 2005-09-20 03:28:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3277 boxname=wulflinc3 idbench=933 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  90db1995bd949fc5ac74143a523f3bcf  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-air01.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-air01.opb
IDLAUNCH: 3277
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        917612 kB
Buffers:         12228 kB
Cached:          78272 kB
SwapCached:        824 kB
Active:          22684 kB
Inactive:        70452 kB
HighTotal:      131008 kB
HighFree:        48748 kB
LowTotal:       903652 kB
LowFree:        868864 kB
SwapTotal:     2097136 kB
SwapFree:      2095740 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5656 kB
Slab:            18200 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 03:48:50 (client local time) WITH STATUS 10 IN 1207.57 SECONDS
stats: 3277 7 1207.57 10

Solver Data

c Parsing PB file...
c Converting 46 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######################
c   -- Clauses(.)/Splits(s): (none)
c ---[  44]---> BDD-cost:   49
c ---[  42]---> BDD-cost:   39
c ---[  40]---> BDD-cost:   41
c ---[  38]---> BDD-cost:   53
c ---[  36]---> BDD-cost:   63
c ---[  34]---> BDD-cost:   61
c ---[  32]---> BDD-cost:   83
c ---[  30]---> BDD-cost:  111
c ---[  28]---> BDD-cost:  139
c ---[  26]---> BDD-cost:  197
c ---[  24]---> BDD-cost:  233
c ---[  22]---> BDD-cost:  273
c ---[  20]---> BDD-cost:  353
c ---[  18]---> BDD-cost:  331
c ---[  16]---> BDD-cost:  527
c ---[  14]---> BDD-cost:  589
c ---[  12]---> BDD-cost:  607
c ---[  10]---> BDD-cost:  559
c ---[   8]---> BDD-cost:  755
c ---[   6]---> BDD-cost:  769
c ---[   4]---> BDD-cost:  741
c ---[   2]---> BDD-cost:  781
c ---[   0]---> BDD-cost:  873
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   20564    53488 |    6854       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 9600
c ---[   0]---> Adder-cost: 7920   maxlim: 1183153   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        26 |   75865   251014 |   25288      26     1591    61.2 |  0.000 % |
c ==============================================================================
c Found solution: 8437
c ---[   0]---> Adder-cost: 0   maxlim: 1184316   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        43 |   75889   251167 |   25296      43     2039    47.4 |  0.000 % |
c ==============================================================================
c Found solution: 8097
c ---[   0]---> Adder-cost: 0   maxlim: 1184656   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        43 |   75893   251220 |   25297      43     2039    47.4 |  0.000 % |
c ==============================================================================
c Found solution: 7212
c ---[   0]---> Adder-cost: 0   maxlim: 1185541   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        43 |   75898   251280 |   25299      43     2039    47.4 |  0.000 % |
c |       144 |   75898   251280 |   27828     144    12635    87.7 |  0.325 % |
c |       299 |   75898   251280 |   30611     299    56525   189.0 |  0.325 % |
c ==============================================================================
c Found solution: 7192
c ---[   0]---> Adder-cost: 0   maxlim: 1185561   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       380 |   75902   251328 |   25300     380    64997   171.0 |  0.325 % |
c |       482 |   75902   251328 |   27830     482    73689   152.9 |  0.342 % |
c ==============================================================================
c Found solution: 6795
c ---[   0]---> Adder-cost: 0   maxlim: 1185958   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       500 |   75913   251422 |   25304     500    75462   150.9 |  0.342 % |
c |       602 |   75911   251416 |   27834     589   101508   172.3 |  0.383 % |
c ==============================================================================
c Found solution: 6136
c ---[   0]---> Adder-cost: 0   maxlim: 1186617   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       627 |   75922   251503 |   25307     614   102021   166.2 |  0.383 % |
c ==============================================================================
c Found solution: 5674
c ---[   0]---> Adder-cost: 0   maxlim: 1187079   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       636 |   75926   251538 |   25308     623   104929   168.4 |  0.383 % |
c ==============================================================================
c Found solution: 5268
c ---[   0]---> Adder-cost: 0   maxlim: 1187485   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       707 |   75935   251625 |   25311     694   148809   214.4 |  0.383 % |
c |       807 |   75935   251625 |   27842     794   164116   206.7 |  0.471 % |
c |       959 |   75935   251625 |   30626     946   216548   228.9 |  0.471 % |
c ==============================================================================
c Found solution: 4967
c ---[   0]---> Adder-cost: 0   maxlim: 1187786   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1024 |   75947   251722 |   25315    1011   227278   224.8 |  0.471 % |
c |      1126 |   75849   251378 |   27846    1082   230798   213.3 |  0.618 % |
c |      1276 |   75849   251378 |   30631    1232   255783   207.6 |  0.618 % |
c |      1503 |   75849   251378 |   33694    1459   341321   233.9 |  0.618 % |
c |      1843 |   75849   251378 |   37063    1799   484561   269.4 |  0.618 % |
c |      2351 |   75849   251378 |   40770    2307   614206   266.2 |  0.618 % |
c ==============================================================================
c Found solution: 4424
c ---[   0]---> Adder-cost: 0   maxlim: 1188329   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2373 |   75863   251475 |   25287    2329   622610   267.3 |  0.618 % |
c |      2473 |   75863   251475 |   27815    2429   647783   266.7 |  0.659 % |
c ==============================================================================
c Found solution: 4031
c ---[   0]---> Adder-cost: 0   maxlim: 1188722   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2502 |   75874   251568 |   25291    2458   651822   265.2 |  0.659 % |
c |      2604 |   75874   251568 |   27820    2560   693972   271.1 |  0.700 % |
c |      2758 |   75874   251568 |   30602    2714   760000   280.0 |  0.700 % |
c |      2983 |   75858   251516 |   33662    2937   780081   265.6 |  0.717 % |
c |      3320 |   75778   251253 |   37028    3270   839332   256.7 |  0.747 % |
c |      3828 |   75778   251253 |   40731    3778   917899   243.0 |  0.747 % |
c |      4588 |   75778   251253 |   44804    4538  1017540   224.2 |  0.747 % |
c |      5740 |   75778   251253 |   49285    5690  1245667   218.9 |  0.747 % |
c |      7450 |   75740   251123 |   54213    7391  1736031   234.9 |  0.752 % |
c |     10012 |   75732   251093 |   59634    9950  2505022   251.8 |  0.788 % |
c |     13858 |   75641   250272 |   65598   13790  3638851   263.9 |  0.805 % |
c |     19627 |   75497   249754 |   72158   19517  5744723   294.3 |  0.946 % |
c |     28277 |   75249   248858 |   79373   28087  8142276   289.9 |  1.193 % |
c |     41260 |   74584   246540 |   87311   40517 12845986   317.1 |  1.834 % |
c ==============================================================================
c Found solution: 4028
c ---[   0]---> Adder-cost: 5870   maxlim: 1181265   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41313 |  115415   392358 |   38471   40551 12854302   317.0 |  1.834 % |
c |     41413 |  115315   392026 |   42318   14973  4495990   300.3 |  1.573 % |
c |     41564 |  115315   392026 |   46549   15124  4551965   301.0 |  1.573 % |
c |     41792 |  115228   391725 |   51204   15339  4602004   300.0 |  1.643 % |
c |     42129 |  115159   391482 |   56325   15665  4654142   297.1 |  1.695 % |
c |     42635 |  115159   391482 |   61957   16171  4847597   299.8 |  1.695 % |
c |     43394 |  115110   391319 |   68153   16923  5099834   301.4 |  1.735 % |
c |     44533 |  115110   391319 |   74969   18062  5440269   301.2 |  1.735 % |
c |     46242 |  114998   390919 |   82466   19703  5960565   302.5 |  1.813 % |
c |     48809 |  114805   390274 |   90712   22236  6719946   302.2 |  1.962 % |
c ==============================================================================
c Found solution: 3964
c ---[   0]---> Adder-cost: 0   maxlim: 1181329   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49554 |  114811   390324 |   38270   22981  6981447   303.8 |  1.962 % |
c |     49654 |  114811   390324 |   42097   23081  6996626   303.1 |  1.975 % |
c |     49807 |  114811   390324 |   46306   23234  7021554   302.2 |  1.975 % |
c |     50034 |  114811   390324 |   50937   23461  7067586   301.2 |  1.975 % |
c |     50371 |  114804   390301 |   56031   23796  7121915   299.3 |  1.979 % |
c |     50881 |  114804   390301 |   61634   24306  7286853   299.8 |  1.979 % |
c |     51640 |  114804   390301 |   67797   25065  7605785   303.4 |  1.979 % |
c |     52779 |  114804   390301 |   74577   26204  7898848   301.4 |  1.979 % |
c ==============================================================================
c Found solution: 3513
c ---[   0]---> Adder-cost: 4434   maxlim: 1178082   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     52959 |  145575   500184 |   48525   26382  7970230   302.1 |  1.979 % |
c |     53059 |  145575   500184 |   53377   26482  8010334   302.5 |  1.745 % |
c |     53213 |  145575   500184 |   58715   26636  8062283   302.7 |  1.745 % |
c |     53438 |  145575   500184 |   64586   26861  8163983   303.9 |  1.745 % |
c |     53776 |  145575   500184 |   71045   27199  8322697   306.0 |  1.745 % |
c |     54284 |  145575   500184 |   78149   27707  8492379   306.5 |  1.745 % |
c |     55043 |  145575   500184 |   85964   28466  8839787   310.5 |  1.745 % |
c |     56182 |  145559   500132 |   94561   29603  9240486   312.1 |  1.756 % |
c |     57890 |  145559   500132 |  104017   31311  9754725   311.5 |  1.756 % |
c |     60453 |  145559   500132 |  114419   33874 10762969   317.7 |  1.756 % |
c |     64297 |  145444   499735 |  125861   37706 12206060   323.7 |  1.807 % |
c |     70063 |  145444   499735 |  138447   43472 14511566   333.8 |  1.807 % |
c |     78713 |  145428   499683 |  152292   52119 17507350   335.9 |  1.818 % |
c |     91688 |  145301   499260 |  167521   65067 21564811   331.4 |  1.866 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -CL000001_bit0 -CL000002_bit0 -CL000003_bit0 -CL000004_bit0 CL000005_bit0 -CL000006_bit0 -CL000007_bit0 -CL000008_bit0 -CL000009_bit0 -CL000010_bit0 -CL000011_bit0 -CL000012_bit0 -CL000013_bit0 -CL000014_bit0 -CL000015_bit0 -CL000016_bit0 -CL000017_bit0 -CL000018_bit0 -CL000019_bit0 -CL000020_bit0 -CL000021_bit0 -CL000022_bit0 -CL000023_bit0 -CL000024_bit0 -CL000025_bit0 -CL000026_bit0 -CL000027_bit0 -CL000028_bit0 -CL000029_bit0 -CL000030_bit0 -CL000031_bit0 -CL000032_bit0 -CL000033_bit0 -CL000034_bit0 -CL000035_bit0 -CL000036_bit0 -CL000037_bit0 -CL000038_bit0 -CL000039_bit0 -CL000040_bit0 -CL000041_bit0 -CL000042_bit0 -CL000043_bit0 -CL000044_bit0 -CL000045_bit0 -CL000046_bit0 -CL000047_bit0 -CL000048_bit0 -CL000049_bit0 -CL000050_bit0 -CL000051_bit0 -CL000052_bit0 -CL000053_bit0 -CL000054_bit0 CL000055_bit0 -CL000056_bit0 -CL000057_bit0 -CL000058_bit0 -CL000059_bit0 -CL000060_bit0 -CL000061_bit0 -CL000062_bit0 -CL000063_bit0 -CL000064_bit0 -CL000065_bit0 -CL000066_bit0 -CL000067_bit0 -CL000068_bit0 -CL000069_bit0 -CL000070_bit0 -CL000071_bit0 -CL000072_bit0 -CL000073_bit0 -CL000074_bit0 -CL000075_bit0 -CL000076_bit0 -CL000077_bit0 -CL000078_bit0 -CL000079_bit0 -CL000080_bit0 -CL000081_bit0 -CL000082_bit0 -CL000083_bit0 -CL000084_bit0 -CL000085_bit0 -CL000086_bit0 -CL000087_bit0 -CL000088_bit0 -CL000089_bit0 -CL000090_bit0 -CL000091_bit0 -CL000092_bit0 -CL000093_bit0 -CL000094_bit0 -CL000095_bit0 -CL000096_bit0 -CL000097_bit0 -CL000098_bit0 -CL000099_bit0 -CL000100_bit0 -CL000101_bit0 -CL000102_bit0 -CL000103_bit0 -CL000104_bit0 -CL000105_bit0 -CL000106_bit0 -CL000107_bit0 -CL000108_bit0 -CL000109_bit0 -CL000110_bit0 -CL000111_bit0 -CL000112_bit0 -CL000113_bit0 -CL000114_bit0 -CL000115_bit0 -CL000116_bit0 -CL000117_bit0 -CL000118_bit0 -CL000119_bit0 -CL000120_bit0 -CL000121_bit0 -CL000122_bit0 -CL000123_bit0 -CL000124_bit0 -CL000125_bit0 -CL000126_bit0 -CL000127_bit0 -CL000128_bit0 CL000129_bit0 -CL000130_bit0 -CL000131_bit0 -CL000132_bit0 -CL000133_bit0 -CL000134_bit0 -CL000135_bit0 -CL000136_bit0 -CL000137_bit0 -CL000138_bit0 -CL000139_bit0 -CL000140_bit0 -CL000141_bit0 -CL000142_bit0 -CL000143_bit0 -CL000144_bit0 -CL000145_bit0 -CL000146_bit0 -CL000147_bit0 -CL000148_bit0 -CL000149_bit0 -CL000150_bit0 -CL000151_bit0 -CL000152_bit0 -CL000153_bit0 -CL000154_bit0 -CL000155_bit0 -CL000156_bit0 -CL000157_bit0 -CL000158_bit0 -CL000159_bit0 -CL000160_bit0 -CL000161_bit0 -CL000162_bit0 -CL000163_bit0 -CL000164_bit0 -CL000165_bit0 -CL000166_bit0 -CL000167_bit0 -CL000168_bit0 -CL000169_bit0 -CL000170_bit0 -CL000171_bit0 -CL000172_bit0 -CL000173_bit0 -CL000174_bit0 -CL000175_bit0 -CL000176_bit0 -CL000177_bit0 -CL000178_bit0 -CL000179_bit0 -CL000180_bit0 -CL000181_bit0 -CL000182_bit0 -CL000183_bit0 -CL000184_bit0 -CL000185_bit0 -CL000186_bit0 -CL000187_bit0 -CL000188_bit0 -CL000189_bit0 -CL000190_bit0 -CL000191_bit0 -CL000192_bit0 -CL000193_bit0 -CL000194_bit0 -CL000195_bit0 -CL000196_bit0 -CL000197_bit0 -CL000198_bit0 -CL000199_bit0 -CL000200_bit0 -CL000201_bit0 -CL000202_bit0 -CL000203_bit0 -CL000204_bit0 -CL000205_bit0 -CL000206_bit0 -CL000207_bit0 -CL000208_bit0 -CL000209_bit0 -CL000210_bit0 -CL000211_bit0 -CL000212_bit0 -CL000213_bit0 -CL000214_bit0 -CL000215_bit0 -CL000216_bit0 -CL000217_bit0 -CL000218_bit0 -CL000219_bit0 -CL000220_bit0 -CL000221_bit0 -CL000222_bit0 -CL000223_bit0 -CL000224_bit0 -CL000225_bit0 -CL000226_bit0 -CL000227_bit0 -CL000228_bit0 -CL000229_bit0 -CL000230_bit0 -CL000231_bit0 -CL000232_bit0 -CL000233_bit0 -CL000234_bit0 -CL000235_bit0 -CL000236_bit0 -CL000237_bit0 -CL000238_bit0 -CL000239_bit0 -CL000240_bit0 -CL000241_bit0 -CL000242_bit0 -CL000243_bit0 -CL000244_bit0 -CL000245_bit0 -CL000246_bit0 -CL000247_bit0 -CL000248_bit0 -CL000249_bit0 -CL000250_bit0 -CL000251_bit0 -CL000252_bit0 -CL000253_bit0 -CL000254_bit0 -CL000255_bit0 -CL000256_bit0 -CL000257_bit0 -CL000258_bit0 -CL000259_bit0 -CL000260_bit0 -CL000261_bit0 -CL000262_bit0 -CL000263_bit0 -CL000264_bit0 -CL000265_bit0 -CL000266_bit0 -CL000267_bit0 -CL000268_bit0 -CL000269_bit0 -CL000270_bit0 -CL000271_bit0 -CL000272_bit0 -CL000273_bit0 -CL000274_bit0 -CL000275_bit0 -CL000276_bit0 -CL000277_bit0 -CL000278_bit0 -CL000279_bit0 -CL000280_bit0 -CL000281_bit0 -CL000282_bit0 -CL000283_bit0 -CL000284_bit0 -CL000285_bit0 -CL000286_bit0 CL000287_bit0 -CL000288_bit0 -CL000289_bit0 -CL000290_bit0 -CL000291_bit0 -CL000292_bit0 -CL000293_bit0 -CL000294_bit0 -CL000295_bit0 -CL000296_bit0 -CL000297_bit0 -CL000298_bit0 -CL000299_bit0 -CL000300_bit0 -CL000301_bit0 -CL000302_bit0 -CL000303_bit0 -CL000304_bit0 -CL000305_bit0 -CL000306_bit0 -CL000307_bit0 -CL000308_bit0 -CL000309_bit0 -CL000310_bit0 -CL000311_bit0 -CL000312_bit0 -CL000313_bit0 -CL000314_bit0 -CL000315_bit0 -CL000316_bit0 -CL000317_bit0 -CL000318_bit0 -CL000319_bit0 -CL000320_bit0 -CL000321_bit0 -CL000322_bit0 -CL000323_bit0 -CL000324_bit0 -CL000325_bit0 -CL000326_bit0 -CL000327_bit0 -CL000328_bit0 -CL000329_bit0 -CL000330_bit0 -CL000331_bit0 -CL000332_bit0 -CL000333_bit0 -CL000334_bit0 -CL000335_bit0 -CL000336_bit0 -CL000337_bit0 -CL000338_bit0 -CL000339_bit0 -CL000340_bit0 -CL000341_bit0 -CL000342_bit0 -CL000343_bit0 -CL000344_bit0 -CL000345_bit0 -CL000346_bit0 -CL000347_bit0 -CL000348_bit0 -CL000349_bit0 -CL000350_bit0 -CL000351_bit0 -CL000352_bit0 -CL000353_bit0 -CL000354_bit0 -CL000355_bit0 -CL000356_bit0 -CL000357_bit0 -CL000358_bit0 -CL000359_bit0 -CL000360_bit0 -CL000361_bit0 -CL000362_bit0 -CL000363_bit0 -CL000364_bit0 -CL000365_bit0 -CL000366_bit0 -CL000367_bit0 -CL000368_bit0 -CL000369_bit0 -CL000370_bit0 -CL000371_bit0 -CL000372_bit0 -CL000373_bit0 -CL000374_bit0 -CL000375_bit0 -CL000376_bit0 -CL000377_bit0 -CL000378_bit0 -CL000379_bit0 -CL000380_bit0 -CL000381_bit0 -CL000382_bit0 -CL000383_bit0 -CL000384_bit0 -CL000385_bit0 -CL000386_bit0 -CL000387_bit0 -CL000388_bit0 -CL000389_bit0 -CL000390_bit0 -CL000391_bit0 -CL000392_bit0 -CL000393_bit0 -CL000394_bit0 -CL000395_bit0 -CL000396_bit0 -CL000397_bit0 -CL000398_bit0 -CL000399_bit0 -CL000400_bit0 -CL000401_bit0 -CL000402_bit0 -CL000403_bit0 -CL000404_bit0 -CL000405_bit0 -CL000406_bit0 -CL000407_bit0 -CL000408_bit0 -CL000409_bit0 -CL000410_bit0 -CL000411_bit0 -CL000412_bit0 -CL000413_bit0 -CL000414_bit0 -CL000415_bit0 -CL000416_bit0 -CL000417_bit0 -CL000418_bit0 -CL000419_bit0 -CL000420_bit0 -CL000421_bit0 -CL000422_bit0 -CL000423_bit0 -CL000424_bit0 -CL000425_bit0 -CL000426_bit0 -CL000427_bit0 -CL000428_bit0 -CL000429_bit0 -CL000430_bit0 -CL000431_bit0 -CL000432_bit0 -CL000433_bit0 -CL000434_bit0 -CL000435_bit0 -CL000436_bit0 -CL000437_bit0 -CL000438_bit0 -CL000439_bit0 -CL000440_bit0 -CL000441_bit0 -CL000442_bit0 -CL000443_bit0 -CL000444_bit0 -CL000445_bit0 -CL000446_bit0 -CL000447_bit0 -CL000448_bit0 -CL000449_bit0 -CL000450_bit0 -CL000451_bit0 -CL000452_bit0 -CL000453_bit0 -CL000454_bit0 -CL000455_bit0 -CL000456_bit0 -CL000457_bit0 -CL000458_bit0 -CL000459_bit0 -CL000460_bit0 -CL000461_bit0 -CL000462_bit0 -CL000463_bit0 -CL000464_bit0 -CL000465_bit0 -CL000466_bit0 -CL000467_bit0 -CL000468_bit0 -CL000469_bit0 -CL000470_bit0 -CL000471_bit0 -CL000472_bit0 -CL000473_bit0 -CL000474_bit0 -CL000475_bit0 -CL000476_bit0 -CL000477_bit0 -CL000478_bit0 -CL000479_bit0 -CL000480_bit0 -CL000481_bit0 -CL000482_bit0 -CL000483_bit0 -CL000484_bit0 -CL000485_bit0 -CL000486_bit0 -CL000487_bit0 -CL000488_bit0 -CL000489_bit0 -CL000490_bit0 -CL000491_bit0 -CL000492_bit0 -CL000493_bit0 -CL000494_bit0 -CL000495_bit0 -CL000496_bit0 -CL000497_bit0 -CL000498_bit0 -CL000499_bit0 -CL000500_bit0 -CL000501_bit0 -CL000502_bit0 -CL000503_bit0 -CL000504_bit0 -CL000505_bit0 -CL000506_bit0 -CL000507_bit0 -CL000508_bit0 -CL000509_bit0 -CL000510_bit0 -CL000511_bit0 -CL000512_bit0 CL000513_bit0 -CL000514_bit0 -CL000515_bit0 -CL000516_bit0 -CL000517_bit0 -CL000518_bit0 -CL000519_bit0 -CL000520_bit0 -CL000521_bit0 -CL000522_bit0 -CL000523_bit0 -CL000524_bit0 -CL000525_bit0 -CL000526_bit0 -CL000527_bit0 -CL000528_bit0 -CL000529_bit0 -CL000530_bit0 -CL000531_bit0 -CL000532_bit0 CL000533_bit0 -CL000534_bit0 -CL000535_bit0 -CL000536_bit0 -CL000537_bit0 -CL000538_bit0 -CL000539_bit0 -CL000540_bit0 -CL000541_bit0 -CL000542_bit0 -CL000543_bit0 -CL000544_bit

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/4111/stat): 4111 (minisat+_script) R 4110 4111 31915 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1797059792 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/4111/statm): 174 3 169 147 0 27 0
[pid=4111] 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=4112
New process pid=4113
New process pid=4114
execve syscall for /bin/sed executable
One traced child (pid=4113) 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=4114) exited with status: 0
One traced child (pid=4112) exited with status: 0
New process pid=4115
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-air01.opb

[startup+10.0033 s]
Raw data (loadavg): 0.76 0.92 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 5591 0 0 0 959 19 0 0 25 0 1 0 1797059797 22994944 4601 4294967295 134512640 135094434 3221224448 3221222000 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 5614 4601 145 145 0 5469 0
[pid=4115] vsize: 22456
Current children cumulated CPU time (s) 9.78
Current children cumulated vsize (Kb) 24580

[startup+20.0052 s]
Raw data (loadavg): 0.80 0.92 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 5907 0 0 0 1957 20 0 0 25 0 1 0 1797059797 23220224 4681 4294967295 134512640 135094434 3221224448 3221222164 134600159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 5669 4681 145 145 0 5524 0
[pid=4115] vsize: 22676
Current children cumulated CPU time (s) 19.77
Current children cumulated vsize (Kb) 24800

[startup+30.006 s]
Raw data (loadavg): 0.83 0.93 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 6113 0 0 0 2955 21 0 0 25 0 1 0 1797059797 23355392 4698 4294967295 134512640 135094434 3221224448 3221221952 134540740 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 5702 4698 145 145 0 5557 0
[pid=4115] vsize: 22808
Current children cumulated CPU time (s) 29.76
Current children cumulated vsize (Kb) 24932

[startup+40.0069 s]
Raw data (loadavg): 0.86 0.93 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 6409 0 0 0 3953 23 0 0 25 0 1 0 1797059797 23490560 4732 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 5735 4732 145 145 0 5590 0
[pid=4115] vsize: 22940
Current children cumulated CPU time (s) 39.76
Current children cumulated vsize (Kb) 25064

[startup+50.0087 s]
Raw data (loadavg): 0.88 0.93 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 6945 0 0 0 4949 25 0 0 25 0 1 0 1797059797 23777280 4770 4294967295 134512640 135094434 3221224448 3221221824 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 5805 4770 145 145 0 5660 0
[pid=4115] vsize: 23220
Current children cumulated CPU time (s) 49.74
Current children cumulated vsize (Kb) 25344

[startup+60.0095 s]
Raw data (loadavg): 0.90 0.93 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 7301 0 0 0 5945 27 0 0 25 0 1 0 1797059797 23797760 4775 4294967295 134512640 135094434 3221224448 3221221744 134677035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 5810 4775 145 145 0 5665 0
[pid=4115] vsize: 23240
Current children cumulated CPU time (s) 59.72
Current children cumulated vsize (Kb) 25364

[startup+70.0103 s]
Raw data (loadavg): 0.91 0.93 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 7638 0 0 0 6943 28 0 0 25 0 1 0 1797059797 23977984 4820 4294967295 134512640 135094434 3221224448 3221222332 134676988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 5854 4820 145 145 0 5709 0
[pid=4115] vsize: 23416
Current children cumulated CPU time (s) 69.71
Current children cumulated vsize (Kb) 25540

[startup+80.0112 s]
Raw data (loadavg): 0.92 0.93 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 8008 0 0 0 7940 30 0 0 25 0 1 0 1797059797 24309760 4901 4294967295 134512640 135094434 3221224448 3221222324 134676380 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 5935 4901 145 145 0 5790 0
[pid=4115] vsize: 23740
Current children cumulated CPU time (s) 79.7
Current children cumulated vsize (Kb) 25864

[startup+90.012 s]
Raw data (loadavg): 0.94 0.94 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 8377 0 0 0 8936 32 0 0 25 0 1 0 1797059797 25694208 5236 4294967295 134512640 135094434 3221224448 3221223120 134556490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 6273 5236 145 145 0 6128 0
[pid=4115] vsize: 25092
Current children cumulated CPU time (s) 89.68
Current children cumulated vsize (Kb) 27216

[startup+100.013 s]
Raw data (loadavg): 0.94 0.94 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 9070 0 0 0 9931 35 0 0 25 0 1 0 1797059797 26116096 5340 4294967295 134512640 135094434 3221224448 3221222060 134677228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 6376 5340 145 145 0 6231 0
[pid=4115] vsize: 25504
Current children cumulated CPU time (s) 99.66
Current children cumulated vsize (Kb) 27628

[startup+110.014 s]
Raw data (loadavg): 0.95 0.94 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 9232 0 0 0 10929 36 0 0 25 0 1 0 1797059797 26644480 5469 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 6505 5469 145 145 0 6360 0
[pid=4115] vsize: 26020
Current children cumulated CPU time (s) 109.65
Current children cumulated vsize (Kb) 28144

[startup+120.016 s]
Raw data (loadavg): 0.96 0.94 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 9497 0 0 0 11924 38 0 0 25 0 1 0 1797059797 27738112 5734 4294967295 134512640 135094434 3221224448 3221223040 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 6772 5734 145 145 0 6627 0
[pid=4115] vsize: 27088
Current children cumulated CPU time (s) 119.62
Current children cumulated vsize (Kb) 29212

[startup+130.016 s]
Raw data (loadavg): 0.97 0.94 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 9776 0 0 0 12918 41 0 0 25 0 1 0 1797059797 28876800 6013 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 7050 6013 145 145 0 6905 0
[pid=4115] vsize: 28200
Current children cumulated CPU time (s) 129.59
Current children cumulated vsize (Kb) 30324

[startup+140.018 s]
Raw data (loadavg): 0.97 0.94 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 10142 0 0 0 13912 44 0 0 25 0 1 0 1797059797 30355456 6379 4294967295 134512640 135094434 3221224448 3221223072 134557691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 7411 6379 145 145 0 7266 0
[pid=4115] vsize: 29644
Current children cumulated CPU time (s) 139.56
Current children cumulated vsize (Kb) 31768

[startup+150.02 s]
Raw data (loadavg): 0.97 0.95 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 10492 0 0 0 14907 46 0 0 25 0 1 0 1797059797 31813632 6729 4294967295 134512640 135094434 3221224448 3221223040 134556941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 7767 6729 145 145 0 7622 0
[pid=4115] vsize: 31068
Current children cumulated CPU time (s) 149.53
Current children cumulated vsize (Kb) 33192

[startup+160.02 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 10845 0 0 0 15901 48 0 0 25 0 1 0 1797059797 33255424 7082 4294967295 134512640 135094434 3221224448 3221223040 134557528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 8119 7082 145 145 0 7974 0
[pid=4115] vsize: 32476
Current children cumulated CPU time (s) 159.49
Current children cumulated vsize (Kb) 34600

[startup+170.021 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 11186 0 0 0 16897 50 0 0 25 0 1 0 1797059797 34648064 7423 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 8459 7423 145 145 0 8314 0
[pid=4115] vsize: 33836
Current children cumulated CPU time (s) 169.47
Current children cumulated vsize (Kb) 35960

[startup+180.022 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 11580 0 0 0 17889 53 0 0 25 0 1 0 1797059797 36257792 7817 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 8852 7817 145 145 0 8707 0
[pid=4115] vsize: 35408
Current children cumulated CPU time (s) 179.42
Current children cumulated vsize (Kb) 37532

[startup+190.023 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 11927 0 0 0 18882 56 0 0 25 0 1 0 1797059797 37675008 8164 4294967295 134512640 135094434 3221224448 3221223072 134557655 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 9198 8164 145 145 0 9053 0
[pid=4115] vsize: 36792
Current children cumulated CPU time (s) 189.38
Current children cumulated vsize (Kb) 38916

[startup+200.024 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 12242 0 0 0 19877 59 0 0 25 0 1 0 1797059797 38961152 8479 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 9512 8479 145 145 0 9367 0
[pid=4115] vsize: 38048
Current children cumulated CPU time (s) 199.36
Current children cumulated vsize (Kb) 40172

[startup+210.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 12616 0 0 0 20873 60 0 0 25 0 1 0 1797059797 40484864 8853 4294967295 134512640 135094434 3221224448 3221223040 134557004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 9884 8853 145 145 0 9739 0
[pid=4115] vsize: 39536
Current children cumulated CPU time (s) 209.33
Current children cumulated vsize (Kb) 41660

[startup+220.026 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 12908 0 0 0 21869 63 0 0 25 0 1 0 1797059797 41680896 9145 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 10176 9145 145 145 0 10031 0
[pid=4115] vsize: 40704
Current children cumulated CPU time (s) 219.32
Current children cumulated vsize (Kb) 42828

[startup+230.027 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 13227 0 0 0 22865 65 0 0 25 0 1 0 1797059797 43048960 9464 4294967295 134512640 135094434 3221224448 3221223040 134556876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 10510 9464 145 145 0 10365 0
[pid=4115] vsize: 42040
Current children cumulated CPU time (s) 229.3
Current children cumulated vsize (Kb) 44164

[startup+240.028 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 13694 0 0 0 23857 68 0 0 25 0 1 0 1797059797 44961792 9931 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 10977 9931 145 145 0 10832 0
[pid=4115] vsize: 43908
Current children cumulated CPU time (s) 239.25
Current children cumulated vsize (Kb) 46032

[startup+250.028 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 14070 0 0 0 24852 71 0 0 25 0 1 0 1797059797 46493696 10307 4294967295 134512640 135094434 3221224448 3221223040 134557372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 11351 10307 145 145 0 11206 0
[pid=4115] vsize: 45404
Current children cumulated CPU time (s) 249.23
Current children cumulated vsize (Kb) 47528

[startup+260.028 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 14513 0 0 0 25846 74 0 0 25 0 1 0 1797059797 48304128 10750 4294967295 134512640 135094434 3221224448 3221223040 134557404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 11793 10750 145 145 0 11648 0
[pid=4115] vsize: 47172
Current children cumulated CPU time (s) 259.2
Current children cumulated vsize (Kb) 49296

[startup+270.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 14939 0 0 0 26841 76 0 0 25 0 1 0 1797059797 50049024 11176 4294967295 134512640 135094434 3221224448 3221223040 134556880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 12219 11176 145 145 0 12074 0
[pid=4115] vsize: 48876
Current children cumulated CPU time (s) 269.17
Current children cumulated vsize (Kb) 51000

[startup+280.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 15331 0 0 0 27835 78 0 0 25 0 1 0 1797059797 51646464 11568 4294967295 134512640 135094434 3221224448 3221223040 134557302 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 12609 11568 145 145 0 12464 0
[pid=4115] vsize: 50436
Current children cumulated CPU time (s) 279.13
Current children cumulated vsize (Kb) 52560

[startup+290.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 15479 0 0 0 28833 79 0 0 25 0 1 0 1797059797 52248576 11716 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 12756 11716 145 145 0 12611 0
[pid=4115] vsize: 51024
Current children cumulated CPU time (s) 289.12
Current children cumulated vsize (Kb) 53148

[startup+300.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 15842 0 0 0 29826 82 0 0 25 0 1 0 1797059797 53731328 12079 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 13118 12079 145 145 0 12973 0
[pid=4115] vsize: 52472
Current children cumulated CPU time (s) 299.08
Current children cumulated vsize (Kb) 54596

[startup+310.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 16178 0 0 0 30820 84 0 0 25 0 1 0 1797059797 55099392 12415 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 13452 12415 145 145 0 13307 0
[pid=4115] vsize: 53808
Current children cumulated CPU time (s) 309.04
Current children cumulated vsize (Kb) 55932

[startup+320.033 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 16450 0 0 0 31814 86 0 0 25 0 1 0 1797059797 56209408 12687 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 13723 12687 145 145 0 13578 0
[pid=4115] vsize: 54892
Current children cumulated CPU time (s) 319
Current children cumulated vsize (Kb) 57016

[startup+330.034 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 16756 0 0 0 32808 88 0 0 25 0 1 0 1797059797 57462784 12993 4294967295 134512640 135094434 3221224448 3221223120 134555274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 14029 12993 145 145 0 13884 0
[pid=4115] vsize: 56116
Current children cumulated CPU time (s) 328.96
Current children cumulated vsize (Kb) 58240

[startup+340.035 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) T 4111 4111 31915 0 -1 0 17001 0 0 0 33803 90 0 0 25 0 1 0 1797059797 58466304 13238 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/4115/statm): 14274 13238 145 145 0 14129 0
[pid=4115] vsize: 57096
Current children cumulated CPU time (s) 338.93
Current children cumulated vsize (Kb) 59220

[startup+350.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 17309 0 0 0 34797 92 0 0 25 0 1 0 1797059797 59723776 13546 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 14581 13546 145 145 0 14436 0
[pid=4115] vsize: 58324
Current children cumulated CPU time (s) 348.89
Current children cumulated vsize (Kb) 60448

[startup+360.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 17686 0 0 0 35792 94 0 0 18 0 1 0 1797059797 61263872 13923 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 14957 13923 145 145 0 14812 0
[pid=4115] vsize: 59828
Current children cumulated CPU time (s) 358.86
Current children cumulated vsize (Kb) 61952

[startup+370.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 18041 0 0 0 36786 96 0 0 25 0 1 0 1797059797 62713856 14278 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 15311 14278 145 145 0 15166 0
[pid=4115] vsize: 61244
Current children cumulated CPU time (s) 368.82
Current children cumulated vsize (Kb) 63368

[startup+380.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 18250 0 0 0 37782 98 0 0 25 0 1 0 1797059797 63565824 14487 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 15519 14487 145 145 0 15374 0
[pid=4115] vsize: 62076
Current children cumulated CPU time (s) 378.8
Current children cumulated vsize (Kb) 64200

[startup+390.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 18394 0 0 0 38780 99 0 0 25 0 1 0 1797059797 64163840 14631 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 15665 14631 145 145 0 15520 0
[pid=4115] vsize: 62660
Current children cumulated CPU time (s) 388.79
Current children cumulated vsize (Kb) 64784

[startup+400.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 18682 0 0 0 39776 101 0 0 25 0 1 0 1797059797 65470464 14919 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 15984 14919 145 145 0 15839 0
[pid=4115] vsize: 63936
Current children cumulated CPU time (s) 398.77
Current children cumulated vsize (Kb) 66060

[startup+410.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 18992 0 0 0 40771 103 0 0 25 0 1 0 1797059797 66736128 15229 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 16293 15229 145 145 0 16148 0
[pid=4115] vsize: 65172
Current children cumulated CPU time (s) 408.74
Current children cumulated vsize (Kb) 67296

[startup+420.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 19332 0 0 0 41765 105 0 0 25 0 1 0 1797059797 68128768 15569 4294967295 134512640 135094434 3221224448 3221223040 134557002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 16633 15569 145 145 0 16488 0
[pid=4115] vsize: 66532
Current children cumulated CPU time (s) 418.7
Current children cumulated vsize (Kb) 68656

[startup+430.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 19691 0 0 0 42758 108 0 0 25 0 1 0 1797059797 69599232 15928 4294967295 134512640 135094434 3221224448 3221223040 134556937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 16992 15928 145 145 0 16847 0
[pid=4115] vsize: 67968
Current children cumulated CPU time (s) 428.66
Current children cumulated vsize (Kb) 70092

[startup+440.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 20029 0 0 0 43753 110 0 0 25 0 1 0 1797059797 70979584 16266 4294967295 134512640 135094434 3221224448 3221223040 134556966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 17329 16266 145 145 0 17184 0
[pid=4115] vsize: 69316
Current children cumulated CPU time (s) 438.63
Current children cumulated vsize (Kb) 71440

[startup+450.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 20366 0 0 0 44749 112 0 0 25 0 1 0 1797059797 72355840 16603 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 17665 16603 145 145 0 17520 0
[pid=4115] vsize: 70660
Current children cumulated CPU time (s) 448.61
Current children cumulated vsize (Kb) 72784

[startup+460.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 20710 0 0 0 45742 115 0 0 25 0 1 0 1797059797 73764864 16947 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 18009 16947 145 145 0 17864 0
[pid=4115] vsize: 72036
Current children cumulated CPU time (s) 458.57
Current children cumulated vsize (Kb) 74160

[startup+470.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 21059 0 0 0 46737 117 0 0 25 0 1 0 1797059797 75194368 17296 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 18358 17296 145 145 0 18213 0
[pid=4115] vsize: 73432
Current children cumulated CPU time (s) 468.54
Current children cumulated vsize (Kb) 75556

[startup+480.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 21457 0 0 0 47732 119 0 0 25 0 1 0 1797059797 76828672 17694 4294967295 134512640 135094434 3221224448 3221223136 134554707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 18757 17694 145 145 0 18612 0
[pid=4115] vsize: 75028
Current children cumulated CPU time (s) 478.51
Current children cumulated vsize (Kb) 77152

[startup+490.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 21814 0 0 0 48728 120 0 0 25 0 1 0 1797059797 78299136 18051 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 19116 18051 145 145 0 18971 0
[pid=4115] vsize: 76464
Current children cumulated CPU time (s) 488.48
Current children cumulated vsize (Kb) 78588

[startup+500.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22608 0 0 0 49722 124 0 0 25 0 1 0 1797059797 79720448 18524 4294967295 134512640 135094434 3221224448 3221223236 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 19463 18524 145 145 0 19318 0
[pid=4115] vsize: 77852
Current children cumulated CPU time (s) 498.46
Current children cumulated vsize (Kb) 79976

[startup+510.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22614 0 0 0 50721 124 0 0 25 0 1 0 1797059797 79720448 18530 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 19463 18530 145 145 0 19318 0
[pid=4115] vsize: 77852
Current children cumulated CPU time (s) 508.45
Current children cumulated vsize (Kb) 79976

[startup+520.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22614 0 0 0 51721 124 0 0 25 0 1 0 1797059797 79720448 18530 4294967295 134512640 135094434 3221224448 3221223120 134555566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 19463 18530 145 145 0 19318 0
[pid=4115] vsize: 77852
Current children cumulated CPU time (s) 518.45
Current children cumulated vsize (Kb) 79976

[startup+530.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22614 0 0 0 52720 125 0 0 25 0 1 0 1797059797 79720448 18530 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 19463 18530 145 145 0 19318 0
[pid=4115] vsize: 77852
Current children cumulated CPU time (s) 528.45
Current children cumulated vsize (Kb) 79976

[startup+540.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22614 0 0 0 53720 125 0 0 25 0 1 0 1797059797 79720448 18530 4294967295 134512640 135094434 3221224448 3221223040 134556845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 19463 18530 145 145 0 19318 0
[pid=4115] vsize: 77852
Current children cumulated CPU time (s) 538.45
Current children cumulated vsize (Kb) 79976

[startup+550.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22614 0 0 0 54720 125 0 0 25 0 1 0 1797059797 79720448 18530 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 19463 18530 145 145 0 19318 0
[pid=4115] vsize: 77852
Current children cumulated CPU time (s) 548.45
Current children cumulated vsize (Kb) 79976

[startup+560.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22614 0 0 0 55719 126 0 0 25 0 1 0 1797059797 79720448 18530 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 19463 18530 145 145 0 19318 0
[pid=4115] vsize: 77852
Current children cumulated CPU time (s) 558.45
Current children cumulated vsize (Kb) 79976

[startup+570.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22614 0 0 0 56719 126 0 0 25 0 1 0 1797059797 79720448 18530 4294967295 134512640 135094434 3221224448 3221223040 134556937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 19463 18530 145 145 0 19318 0
[pid=4115] vsize: 77852
Current children cumulated CPU time (s) 568.45
Current children cumulated vsize (Kb) 79976

[startup+580.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22614 0 0 0 57718 126 0 0 25 0 1 0 1797059797 79720448 18530 4294967295 134512640 135094434 3221224448 3221223040 134556987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 19463 18530 145 145 0 19318 0
[pid=4115] vsize: 77852
Current children cumulated CPU time (s) 578.44
Current children cumulated vsize (Kb) 79976

[startup+590.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22614 0 0 0 58718 127 0 0 25 0 1 0 1797059797 79720448 18530 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 19463 18530 145 145 0 19318 0
[pid=4115] vsize: 77852
Current children cumulated CPU time (s) 588.45
Current children cumulated vsize (Kb) 79976

[startup+600.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22774 0 0 0 59716 128 0 0 25 0 1 0 1797059797 79867904 18565 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 19499 18565 145 145 0 19354 0
[pid=4115] vsize: 77996
Current children cumulated CPU time (s) 598.44
Current children cumulated vsize (Kb) 80120

[startup+610.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22774 0 0 0 60716 129 0 0 25 0 1 0 1797059797 79867904 18565 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 19499 18565 145 145 0 19354 0
[pid=4115] vsize: 77996
Current children cumulated CPU time (s) 608.45
Current children cumulated vsize (Kb) 80120

[startup+620.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22774 0 0 0 61715 129 0 0 25 0 1 0 1797059797 79867904 18565 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 19499 18565 145 145 0 19354 0
[pid=4115] vsize: 77996
Current children cumulated CPU time (s) 618.44
Current children cumulated vsize (Kb) 80120

[startup+630.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22774 0 0 0 62715 129 0 0 25 0 1 0 1797059797 79867904 18565 4294967295 134512640 135094434 3221224448 3221223040 134556958 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 19499 18565 145 145 0 19354 0
[pid=4115] vsize: 77996
Current children cumulated CPU time (s) 628.44
Current children cumulated vsize (Kb) 80120

[startup+640.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22899 0 0 0 63714 130 0 0 25 0 1 0 1797059797 79867904 18565 4294967295 134512640 135094434 3221224448 3221221280 134784948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 19499 18565 145 145 0 19354 0
[pid=4115] vsize: 77996
Current children cumulated CPU time (s) 638.44
Current children cumulated vsize (Kb) 80120

[startup+650.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 64714 130 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0
[pid=4115] vsize: 78508
Current children cumulated CPU time (s) 648.44
Current children cumulated vsize (Kb) 80632

[startup+660.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 65713 131 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0
[pid=4115] vsize: 78508
Current children cumulated CPU time (s) 658.44
Current children cumulated vsize (Kb) 80632

[startup+670.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 66713 131 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0
[pid=4115] vsize: 78508
Current children cumulated CPU time (s) 668.44
Current children cumulated vsize (Kb) 80632

[startup+680.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 67713 131 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223040 134557025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0
[pid=4115] vsize: 78508
Current children cumulated CPU time (s) 678.44
Current children cumulated vsize (Kb) 80632

[startup+690.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 68713 131 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223104 134558298 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0
[pid=4115] vsize: 78508
Current children cumulated CPU time (s) 688.44
Current children cumulated vsize (Kb) 80632

[startup+700.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 69713 131 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0
[pid=4115] vsize: 78508
Current children cumulated CPU time (s) 698.44
Current children cumulated vsize (Kb) 80632

[startup+710.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 70714 131 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0
[pid=4115] vsize: 78508
Current children cumulated CPU time (s) 708.45
Current children cumulated vsize (Kb) 80632

[startup+720.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 71713 132 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0
[pid=4115] vsize: 78508
Current children cumulated CPU time (s) 718.45
Current children cumulated vsize (Kb) 80632

[startup+730.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 72714 132 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0
[pid=4115] vsize: 78508
Current children cumulated CPU time (s) 728.46
Current children cumulated vsize (Kb) 80632

[startup+740.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 73714 132 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0
[pid=4115] vsize: 78508
Current children cumulated CPU time (s) 738.46
Current children cumulated vsize (Kb) 80632

[startup+750.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 74714 132 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0
[pid=4115] vsize: 78508
Current children cumulated CPU time (s) 748.46
Current children cumulated vsize (Kb) 80632

[startup+760.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 75714 132 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0
[pid=4115] vsize: 78508
Current children cumulated CPU time (s) 758.46
Current children cumulated vsize (Kb) 80632

[startup+770.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 76714 132 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0
[pid=4115] vsize: 78508
Current children cumulated CPU time (s) 768.46
Current children cumulated vsize (Kb) 80632

[startup+780.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 23029 0 0 0 77714 132 0 0 25 0 1 0 1797059797 80523264 18695 4294967295 134512640 135094434 3221224448 3221223072 134557683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 19659 18695 145 145 0 19514 0
[pid=4115] vsize: 78636
Current children cumulated CPU time (s) 778.46
Current children cumulated vsize (Kb) 80760

[startup+790.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 23304 0 0 0 78709 135 0 0 25 0 1 0 1797059797 81653760 18970 4294967295 134512640 135094434 3221224448 3221223040 134557028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 19935 18970 145 145 0 19790 0
[pid=4115] vsize: 79740
Current children cumulated CPU time (s) 788.44
Current children cumulated vsize (Kb) 81864

[startup+800.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 23601 0 0 0 79705 136 0 0 25 0 1 0 1797059797 82866176 19267 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 20231 19267 145 145 0 20086 0
[pid=4115] vsize: 80924
Current children cumulated CPU time (s) 798.41
Current children cumulated vsize (Kb) 83048

[startup+810.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 23919 0 0 0 80700 138 0 0 25 0 1 0 1797059797 84168704 19585 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 20549 19585 145 145 0 20404 0
[pid=4115] vsize: 82196
Current children cumulated CPU time (s) 808.38
Current children cumulated vsize (Kb) 84320

[startup+820.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 24306 0 0 0 81695 140 0 0 25 0 1 0 1797059797 85753856 19972 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 20936 19972 145 145 0 20791 0
[pid=4115] vsize: 83744
Current children cumulated CPU time (s) 818.35
Current children cumulated vsize (Kb) 85868

[startup+830.083 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) T 4111 4111 31915 0 -1 0 24658 0 0 0 82690 142 0 0 25 0 1 0 1797059797 87195648 20324 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/4115/statm): 21288 20324 145 145 0 21143 0
[pid=4115] vsize: 85152
Current children cumulated CPU time (s) 828.32
Current children cumulated vsize (Kb) 87276

[startup+840.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 25013 0 0 0 83685 144 0 0 25 0 1 0 1797059797 88645632 20679 4294967295 134512640 135094434 3221224448 3221223120 134556505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 21642 20679 145 145 0 21497 0
[pid=4115] vsize: 86568
Current children cumulated CPU time (s) 838.29
Current children cumulated vsize (Kb) 88692

[startup+850.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 25338 0 0 0 84680 146 0 0 25 0 1 0 1797059797 89976832 21004 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 21967 21004 145 145 0 21822 0
[pid=4115] vsize: 87868
Current children cumulated CPU time (s) 848.26
Current children cumulated vsize (Kb) 89992

[startup+860.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 25637 0 0 0 85675 149 0 0 25 0 1 0 1797059797 91197440 21303 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 22265 21303 145 145 0 22120 0
[pid=4115] vsize: 89060
Current children cumulated CPU time (s) 858.24
Current children cumulated vsize (Kb) 91184

[startup+870.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 25990 0 0 0 86670 151 0 0 25 0 1 0 1797059797 92639232 21656 4294967295 134512640 135094434 3221224448 3221223040 134557336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 22617 21656 145 145 0 22472 0
[pid=4115] vsize: 90468
Current children cumulated CPU time (s) 868.21
Current children cumulated vsize (Kb) 92592

[startup+880.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 26218 0 0 0 87668 152 0 0 25 0 1 0 1797059797 93573120 21884 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 22845 21884 145 145 0 22700 0
[pid=4115] vsize: 91380
Current children cumulated CPU time (s) 878.2
Current children cumulated vsize (Kb) 93504

[startup+890.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 26525 0 0 0 88664 154 0 0 25 0 1 0 1797059797 94826496 22191 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 23151 22191 145 145 0 23006 0
[pid=4115] vsize: 92604
Current children cumulated CPU time (s) 888.18
Current children cumulated vsize (Kb) 94728

[startup+900.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 26839 0 0 0 89659 157 0 0 25 0 1 0 1797059797 96108544 22505 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 23464 22505 145 145 0 23319 0
[pid=4115] vsize: 93856
Current children cumulated CPU time (s) 898.16
Current children cumulated vsize (Kb) 95980

[startup+910.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 27123 0 0 0 90654 159 0 0 25 0 1 0 1797059797 97271808 22789 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 23748 22789 145 145 0 23603 0
[pid=4115] vsize: 94992
Current children cumulated CPU time (s) 908.13
Current children cumulated vsize (Kb) 97116

[startup+920.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 27460 0 0 0 91648 162 0 0 25 0 1 0 1797059797 98648064 23126 4294967295 134512640 135094434 3221224448 3221223040 134557141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 24084 23126 145 145 0 23939 0
[pid=4115] vsize: 96336
Current children cumulated CPU time (s) 918.1
Current children cumulated vsize (Kb) 98460

[startup+930.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 27735 0 0 0 92644 164 0 0 25 0 1 0 1797059797 99778560 23401 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 24360 23401 145 145 0 24215 0
[pid=4115] vsize: 97440
Current children cumulated CPU time (s) 928.08
Current children cumulated vsize (Kb) 99564

[startup+940.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 27932 0 0 0 93640 165 0 0 25 0 1 0 1797059797 100581376 23598 4294967295 134512640 135094434 3221224448 3221223040 134557210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 24556 23598 145 145 0 24411 0
[pid=4115] vsize: 98224
Current children cumulated CPU time (s) 938.05
Current children cumulated vsize (Kb) 100348

[startup+950.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 28142 0 0 0 94637 167 0 0 25 0 1 0 1797059797 101441536 23808 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 24766 23808 145 145 0 24621 0
[pid=4115] vsize: 99064
Current children cumulated CPU time (s) 948.04
Current children cumulated vsize (Kb) 101188

[startup+960.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 28343 0 0 0 95634 168 0 0 25 0 1 0 1797059797 102264832 24009 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 24967 24009 145 145 0 24822 0
[pid=4115] vsize: 99868
Current children cumulated CPU time (s) 958.02
Current children cumulated vsize (Kb) 101992

[startup+970.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 28485 0 0 0 96632 169 0 0 25 0 1 0 1797059797 102842368 24151 4294967295 134512640 135094434 3221224448 3221223108 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 25108 24151 145 145 0 24963 0
[pid=4115] vsize: 100432
Current children cumulated CPU time (s) 968.01
Current children cumulated vsize (Kb) 102556

[startup+980.097 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) T 4111 4111 31915 0 -1 0 28599 0 0 0 97630 170 0 0 25 0 1 0 1797059797 103309312 24265 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/4115/statm): 25222 24265 145 145 0 25077 0
[pid=4115] vsize: 100888
Current children cumulated CPU time (s) 978
Current children cumulated vsize (Kb) 103012

[startup+990.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 28819 0 0 0 98627 171 0 0 25 0 1 0 1797059797 104206336 24485 4294967295 134512640 135094434 3221224448 3221223040 134557022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 25441 24485 145 145 0 25296 0
[pid=4115] vsize: 101764
Current children cumulated CPU time (s) 987.98
Current children cumulated vsize (Kb) 103888

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 29014 0 0 0 99623 172 0 0 25 0 1 0 1797059797 105005056 24680 4294967295 134512640 135094434 3221224448 3221223040 134557227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 25636 24680 145 145 0 25491 0
[pid=4115] vsize: 102544
Current children cumulated CPU time (s) 997.95
Current children cumulated vsize (Kb) 104668

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 29268 0 0 0 100619 174 0 0 25 0 1 0 1797059797 106045440 24934 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 25890 24934 145 145 0 25745 0
[pid=4115] vsize: 103560
Current children cumulated CPU time (s) 1007.93
Current children cumulated vsize (Kb) 105684

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 29463 0 0 0 101617 175 0 0 25 0 1 0 1797059797 106840064 25129 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 26084 25129 145 145 0 25939 0
[pid=4115] vsize: 104336
Current children cumulated CPU time (s) 1017.92
Current children cumulated vsize (Kb) 106460

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 29709 0 0 0 102613 177 0 0 25 0 1 0 1797059797 107851776 25375 4294967295 134512640 135094434 3221224448 3221223120 134555943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 26331 25375 145 145 0 26186 0
[pid=4115] vsize: 105324
Current children cumulated CPU time (s) 1027.9
Current children cumulated vsize (Kb) 107448

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 29889 0 0 0 103609 179 0 0 25 0 1 0 1797059797 108584960 25555 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 26510 25555 145 145 0 26365 0
[pid=4115] vsize: 106040
Current children cumulated CPU time (s) 1037.88
Current children cumulated vsize (Kb) 108164

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 30100 0 0 0 104605 180 0 0 25 0 1 0 1797059797 109449216 25766 4294967295 134512640 135094434 3221224448 3221223040 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 26721 25766 145 145 0 26576 0
[pid=4115] vsize: 106884
Current children cumulated CPU time (s) 1047.85
Current children cumulated vsize (Kb) 109008

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 30278 0 0 0 105602 181 0 0 25 0 1 0 1797059797 110174208 25944 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 26898 25944 145 145 0 26753 0
[pid=4115] vsize: 107592
Current children cumulated CPU time (s) 1057.83
Current children cumulated vsize (Kb) 109716

[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 30502 0 0 0 106599 182 0 0 25 0 1 0 1797059797 111099904 26168 4294967295 134512640 135094434 3221224448 3221223040 134556843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 27124 26168 145 145 0 26979 0
[pid=4115] vsize: 108496
Current children cumulated CPU time (s) 1067.81
Current children cumulated vsize (Kb) 110620

[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 30752 0 0 0 107595 184 0 0 25 0 1 0 1797059797 112119808 26418 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 27373 26418 145 145 0 27228 0
[pid=4115] vsize: 109492
Current children cumulated CPU time (s) 1077.79
Current children cumulated vsize (Kb) 111616

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 30925 0 0 0 108592 186 0 0 25 0 1 0 1797059797 112828416 26591 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 27546 26591 145 145 0 27401 0
[pid=4115] vsize: 110184
Current children cumulated CPU time (s) 1087.78
Current children cumulated vsize (Kb) 112308

[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 31131 0 0 0 109589 186 0 0 25 0 1 0 1797059797 113672192 26797 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4115/statm): 27752 26797 145 145 0 27607 0
[pid=4115] vsize: 111008
Current children cumulated CPU time (s) 1097.75
Current children cumulated vsize (Kb) 113132

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 31370 0 0 0 110584 188 0 0 25 0 1 0 1797059797 114642944 27036 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 27989 27036 145 145 0 27844 0
[pid=4115] vsize: 111956
Current children cumulated CPU time (s) 1107.72
Current children cumulated vsize (Kb) 114080

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 31610 0 0 0 111579 190 0 0 25 0 1 0 1797059797 115617792 27276 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 28227 27276 145 145 0 28082 0
[pid=4115] vsize: 112908
Current children cumulated CPU time (s) 1117.69
Current children cumulated vsize (Kb) 115032

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 31816 0 0 0 112575 191 0 0 25 0 1 0 1797059797 116461568 27482 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 28433 27482 145 145 0 28288 0
[pid=4115] vsize: 113732
Current children cumulated CPU time (s) 1127.66
Current children cumulated vsize (Kb) 115856

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 32026 0 0 0 113572 193 0 0 25 0 1 0 1797059797 117313536 27692 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 28641 27692 145 145 0 28496 0
[pid=4115] vsize: 114564
Current children cumulated CPU time (s) 1137.65
Current children cumulated vsize (Kb) 116688

[startup+1150.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 32279 0 0 0 114566 195 0 0 25 0 1 0 1797059797 118349824 27945 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 28894 27945 145 145 0 28749 0
[pid=4115] vsize: 115576
Current children cumulated CPU time (s) 1147.61
Current children cumulated vsize (Kb) 117700

[startup+1160.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 32466 0 0 0 115564 196 0 0 25 0 1 0 1797059797 119111680 28132 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 29080 28132 145 145 0 28935 0
[pid=4115] vsize: 116320
Current children cumulated CPU time (s) 1157.6
Current children cumulated vsize (Kb) 118444

[startup+1170.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 32568 0 0 0 116562 197 0 0 25 0 1 0 1797059797 119816192 28234 4294967295 134512640 135094434 3221224448 3221223040 134556843 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 29252 28234 145 145 0 29107 0
[pid=4115] vsize: 117008
Current children cumulated CPU time (s) 1167.59
Current children cumulated vsize (Kb) 119132

[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 32745 0 0 0 117558 198 0 0 25 0 1 0 1797059797 120549376 28411 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 29431 28411 145 145 0 29286 0
[pid=4115] vsize: 117724
Current children cumulated CPU time (s) 1177.56
Current children cumulated vsize (Kb) 119848

[startup+1190.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 32957 0 0 0 118554 200 0 0 25 0 1 0 1797059797 121421824 28623 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 29644 28623 145 145 0 29499 0
[pid=4115] vsize: 118576
Current children cumulated CPU time (s) 1187.54
Current children cumulated vsize (Kb) 120700

[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 33265 0 0 0 119549 203 0 0 25 0 1 0 1797059797 122679296 28931 4294967295 134512640 135094434 3221224448 3221223040 134556961 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 29951 28931 145 145 0 29806 0
[pid=4115] vsize: 119804
Current children cumulated CPU time (s) 1197.52
Current children cumulated vsize (Kb) 121928

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 33606 0 0 0 120546 205 0 0 25 0 1 0 1797059797 124080128 29272 4294967295 134512640 135094434 3221224448 3221223040 134557022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 30293 29272 145 145 0 30148 0
[pid=4115] vsize: 121172
Current children cumulated CPU time (s) 1207.51
Current children cumulated vsize (Kb) 123296



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4115
Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/4111/statm): 531 226 485 147 0 384 0
[pid=4111] vsize: 2124
Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 33606 0 0 0 120546 205 0 0 25 0 1 0 1797059797 124080128 29272 4294967295 134512640 135094434 3221224448 3221223040 134557022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4115/statm): 30293 29272 145 145 0 30148 0
[pid=4115] vsize: 121172
Current children cumulated CPU time (s) 1207.51
Current children cumulated vsize (Kb) 123296

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

Child status: 10
Real time (s): 1210.19
CPU time (s): 1207.57
CPU user time (s): 1205.46
CPU system time (s): 2.10668
CPU usage (%): 99.7838
Max. virtual memory (cumulated for all children) (Kb): 123296

Verifier Data

ERROR: no interpretation found !