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-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-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.215
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 3890

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        887404 kB
Buffers:         35260 kB
Cached:          83792 kB
SwapCached:        696 kB
Active:          72500 kB
Inactive:        49112 kB
HighTotal:      131008 kB
HighFree:        43624 kB
LowTotal:       903652 kB
LowFree:        843780 kB
SwapTotal:     2097640 kB
SwapFree:      2096372 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5812 kB
Slab:            20028 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 03:46:43 (client local time) WITH STATUS 10 IN 1207.62 SECONDS
stats: 2893 7 1207.62 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/9152/stat): 9152 (minisat+_script) R 9151 9152 20115 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846656055 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/9152/statm): 174 3 169 147 0 27 0
[pid=9152] 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=9153
New process pid=9154
New process pid=9155
execve syscall for /bin/sed executable
One traced child (pid=9154) 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=9155) exited with status: 0
One traced child (pid=9153) exited with status: 0
New process pid=9156
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-air01.opb

[startup+10.0031 s]
Raw data (loadavg): 1.01 0.97 0.95 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 5591 0 0 0 959 19 0 0 25 0 1 0 1846656060 22994944 4601 4294967295 134512640 135094434 3221224432 3221221808 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 5614 4601 145 145 0 5469 0
[pid=9156] vsize: 22456
Current children cumulated CPU time (s) 9.79
Current children cumulated vsize (Kb) 24580

[startup+20.0048 s]
Raw data (loadavg): 1.08 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 5907 0 0 0 1958 20 0 0 25 0 1 0 1846656060 23220224 4681 4294967295 134512640 135094434 3221224432 3221221808 134676480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 5669 4681 145 145 0 5524 0
[pid=9156] vsize: 22676
Current children cumulated CPU time (s) 19.79
Current children cumulated vsize (Kb) 24800

[startup+30.0055 s]
Raw data (loadavg): 1.07 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 6113 0 0 0 2956 21 0 0 25 0 1 0 1846656060 23355392 4698 4294967295 134512640 135094434 3221224432 3221221860 134541720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 5702 4698 145 145 0 5557 0
[pid=9156] vsize: 22808
Current children cumulated CPU time (s) 29.78
Current children cumulated vsize (Kb) 24932

[startup+40.0062 s]
Raw data (loadavg): 1.06 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 6409 0 0 0 3955 22 0 0 25 0 1 0 1846656060 23490560 4732 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 5735 4732 145 145 0 5590 0
[pid=9156] vsize: 22940
Current children cumulated CPU time (s) 39.78
Current children cumulated vsize (Kb) 25064

[startup+50.0079 s]
Raw data (loadavg): 1.05 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 6945 0 0 0 4949 25 0 0 25 0 1 0 1846656060 23777280 4770 4294967295 134512640 135094434 3221224432 3221222160 134600225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 5805 4770 145 145 0 5660 0
[pid=9156] vsize: 23220
Current children cumulated CPU time (s) 49.75
Current children cumulated vsize (Kb) 25344

[startup+60.0076 s]
Raw data (loadavg): 1.04 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 7301 0 0 0 5946 27 0 0 25 0 1 0 1846656060 23797760 4775 4294967295 134512640 135094434 3221224432 3221221964 134676988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 5810 4775 145 145 0 5665 0
[pid=9156] vsize: 23240
Current children cumulated CPU time (s) 59.74
Current children cumulated vsize (Kb) 25364

[startup+70.0082 s]
Raw data (loadavg): 1.03 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 7638 0 0 0 6943 28 0 0 25 0 1 0 1846656060 23977984 4820 4294967295 134512640 135094434 3221224432 3221222608 134676280 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 5854 4820 145 145 0 5709 0
[pid=9156] vsize: 23416
Current children cumulated CPU time (s) 69.72
Current children cumulated vsize (Kb) 25540

[startup+80.0089 s]
Raw data (loadavg): 1.03 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 8008 0 0 0 7940 30 0 0 25 0 1 0 1846656060 24309760 4901 4294967295 134512640 135094434 3221224432 3221222220 134676610 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 5935 4901 145 145 0 5790 0
[pid=9156] vsize: 23740
Current children cumulated CPU time (s) 79.71
Current children cumulated vsize (Kb) 25864

[startup+90.0096 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 8378 0 0 0 8935 32 0 0 25 0 1 0 1846656060 25698304 5237 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 6274 5237 145 145 0 6129 0
[pid=9156] vsize: 25096
Current children cumulated CPU time (s) 89.68
Current children cumulated vsize (Kb) 27220

[startup+100.01 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 9070 0 0 0 9929 36 0 0 25 0 1 0 1846656060 26116096 5340 4294967295 134512640 135094434 3221224432 3221221808 134601029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 6376 5340 145 145 0 6231 0
[pid=9156] vsize: 25504
Current children cumulated CPU time (s) 99.66
Current children cumulated vsize (Kb) 27628

[startup+110.011 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 9232 0 0 0 10926 37 0 0 25 0 1 0 1846656060 26644480 5469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 6505 5469 145 145 0 6360 0
[pid=9156] vsize: 26020
Current children cumulated CPU time (s) 109.64
Current children cumulated vsize (Kb) 28144

[startup+120.012 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 9489 0 0 0 11921 40 0 0 25 0 1 0 1846656060 27705344 5726 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 6764 5726 145 145 0 6619 0
[pid=9156] vsize: 27056
Current children cumulated CPU time (s) 119.62
Current children cumulated vsize (Kb) 29180

[startup+130.012 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 9767 0 0 0 12916 43 0 0 25 0 1 0 1846656060 28839936 6004 4294967295 134512640 135094434 3221224432 3221223024 134557131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 7041 6004 145 145 0 6896 0
[pid=9156] vsize: 28164
Current children cumulated CPU time (s) 129.6
Current children cumulated vsize (Kb) 30288

[startup+140.013 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 10121 0 0 0 13910 45 0 0 25 0 1 0 1846656060 30273536 6358 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 7391 6358 145 145 0 7246 0
[pid=9156] vsize: 29564
Current children cumulated CPU time (s) 139.56
Current children cumulated vsize (Kb) 31688

[startup+150.014 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 10473 0 0 0 14905 47 0 0 25 0 1 0 1846656060 31739904 6710 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 7749 6710 145 145 0 7604 0
[pid=9156] vsize: 30996
Current children cumulated CPU time (s) 149.53
Current children cumulated vsize (Kb) 33120

[startup+160.013 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 10817 0 0 0 15899 49 0 0 25 0 1 0 1846656060 33140736 7054 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 8091 7054 145 145 0 7946 0
[pid=9156] vsize: 32364
Current children cumulated CPU time (s) 159.49
Current children cumulated vsize (Kb) 34488

[startup+170.014 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 11156 0 0 0 16894 51 0 0 25 0 1 0 1846656060 34525184 7393 4294967295 134512640 135094434 3221224432 3221223024 134556791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 8429 7393 145 145 0 8284 0
[pid=9156] vsize: 33716
Current children cumulated CPU time (s) 169.46
Current children cumulated vsize (Kb) 35840

[startup+180.014 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 11543 0 0 0 17886 55 0 0 25 0 1 0 1846656060 36106240 7780 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 8815 7780 145 145 0 8670 0
[pid=9156] vsize: 35260
Current children cumulated CPU time (s) 179.42
Current children cumulated vsize (Kb) 37384

[startup+190.014 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 11901 0 0 0 18880 58 0 0 25 0 1 0 1846656060 37568512 8138 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 9172 8138 145 145 0 9027 0
[pid=9156] vsize: 36688
Current children cumulated CPU time (s) 189.39
Current children cumulated vsize (Kb) 38812

[startup+200.015 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 12214 0 0 0 19874 60 0 0 25 0 1 0 1846656060 38846464 8451 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 9484 8451 145 145 0 9339 0
[pid=9156] vsize: 37936
Current children cumulated CPU time (s) 199.35
Current children cumulated vsize (Kb) 40060

[startup+210.015 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 12592 0 0 0 20867 63 0 0 25 0 1 0 1846656060 40386560 8829 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 9860 8829 145 145 0 9715 0
[pid=9156] vsize: 39440
Current children cumulated CPU time (s) 209.31
Current children cumulated vsize (Kb) 41564

[startup+220.016 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 12869 0 0 0 21862 66 0 0 25 0 1 0 1846656060 41521152 9106 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 10137 9106 145 145 0 9992 0
[pid=9156] vsize: 40548
Current children cumulated CPU time (s) 219.29
Current children cumulated vsize (Kb) 42672

[startup+230.016 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 13199 0 0 0 22858 68 0 0 25 0 1 0 1846656060 42934272 9436 4294967295 134512640 135094434 3221224432 3221223112 134553433 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 10482 9436 145 145 0 10337 0
[pid=9156] vsize: 41928
Current children cumulated CPU time (s) 229.27
Current children cumulated vsize (Kb) 44052

[startup+240.017 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 13658 0 0 0 23851 71 0 0 25 0 1 0 1846656060 44810240 9895 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 10940 9895 145 145 0 10795 0
[pid=9156] vsize: 43760
Current children cumulated CPU time (s) 239.23
Current children cumulated vsize (Kb) 45884

[startup+250.018 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 14038 0 0 0 24847 73 0 0 25 0 1 0 1846656060 46362624 10275 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 11319 10275 145 145 0 11174 0
[pid=9156] vsize: 45276
Current children cumulated CPU time (s) 249.21
Current children cumulated vsize (Kb) 47400

[startup+260.018 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 14472 0 0 0 25840 75 0 0 25 0 1 0 1846656060 48144384 10709 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 11754 10709 145 145 0 11609 0
[pid=9156] vsize: 47016
Current children cumulated CPU time (s) 259.16
Current children cumulated vsize (Kb) 49140

[startup+270.019 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 14905 0 0 0 26835 78 0 0 25 0 1 0 1846656060 49905664 11142 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 12184 11142 145 145 0 12039 0
[pid=9156] vsize: 48736
Current children cumulated CPU time (s) 269.14
Current children cumulated vsize (Kb) 50860

[startup+280.02 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 15308 0 0 0 27829 80 0 0 25 0 1 0 1846656060 51552256 11545 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 12586 11545 145 145 0 12441 0
[pid=9156] vsize: 50344
Current children cumulated CPU time (s) 279.1
Current children cumulated vsize (Kb) 52468

[startup+290.021 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 15463 0 0 0 28828 81 0 0 25 0 1 0 1846656060 52183040 11700 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 12740 11700 145 145 0 12595 0
[pid=9156] vsize: 50960
Current children cumulated CPU time (s) 289.1
Current children cumulated vsize (Kb) 53084

[startup+300.022 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 15811 0 0 0 29822 84 0 0 25 0 1 0 1846656060 53604352 12048 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 13087 12048 145 145 0 12942 0
[pid=9156] vsize: 52348
Current children cumulated CPU time (s) 299.07
Current children cumulated vsize (Kb) 54472

[startup+310.022 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 16148 0 0 0 30814 87 0 0 25 0 1 0 1846656060 54980608 12385 4294967295 134512640 135094434 3221224432 3221223120 134554739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 13423 12385 145 145 0 13278 0
[pid=9156] vsize: 53692
Current children cumulated CPU time (s) 309.02
Current children cumulated vsize (Kb) 55816

[startup+320.022 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 16435 0 0 0 31808 89 0 0 25 0 1 0 1846656060 56147968 12672 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 13708 12672 145 145 0 13563 0
[pid=9156] vsize: 54832
Current children cumulated CPU time (s) 318.98
Current children cumulated vsize (Kb) 56956

[startup+330.023 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 16733 0 0 0 32803 92 0 0 25 0 1 0 1846656060 57368576 12970 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 14006 12970 145 145 0 13861 0
[pid=9156] vsize: 56024
Current children cumulated CPU time (s) 328.96
Current children cumulated vsize (Kb) 58148

[startup+340.024 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 16991 0 0 0 33798 94 0 0 25 0 1 0 1846656060 58425344 13228 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 14264 13228 145 145 0 14119 0
[pid=9156] vsize: 57056
Current children cumulated CPU time (s) 338.93
Current children cumulated vsize (Kb) 59180

[startup+350.024 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 17300 0 0 0 34793 96 0 0 25 0 1 0 1846656060 59686912 13537 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 14572 13537 145 145 0 14427 0
[pid=9156] vsize: 58288
Current children cumulated CPU time (s) 348.9
Current children cumulated vsize (Kb) 60412

[startup+360.025 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 17674 0 0 0 35787 99 0 0 25 0 1 0 1846656060 61214720 13911 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 14945 13911 145 145 0 14800 0
[pid=9156] vsize: 59780
Current children cumulated CPU time (s) 358.87
Current children cumulated vsize (Kb) 61904

[startup+370.026 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 18038 0 0 0 36782 101 0 0 25 0 1 0 1846656060 62701568 14275 4294967295 134512640 135094434 3221224432 3221223056 134562108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 15308 14275 145 145 0 15163 0
[pid=9156] vsize: 61232
Current children cumulated CPU time (s) 368.84
Current children cumulated vsize (Kb) 63356

[startup+380.027 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 18241 0 0 0 37779 103 0 0 25 0 1 0 1846656060 63528960 14478 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 15510 14478 145 145 0 15365 0
[pid=9156] vsize: 62040
Current children cumulated CPU time (s) 378.83
Current children cumulated vsize (Kb) 64164

[startup+390.028 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 18394 0 0 0 38777 103 0 0 25 0 1 0 1846656060 64163840 14631 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 15665 14631 145 145 0 15520 0
[pid=9156] vsize: 62660
Current children cumulated CPU time (s) 388.81
Current children cumulated vsize (Kb) 64784

[startup+400.029 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 18675 0 0 0 39772 105 0 0 25 0 1 0 1846656060 65441792 14912 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 15977 14912 145 145 0 15832 0
[pid=9156] vsize: 63908
Current children cumulated CPU time (s) 398.78
Current children cumulated vsize (Kb) 66032

[startup+410.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 18985 0 0 0 40767 107 0 0 25 0 1 0 1846656060 66707456 15222 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 16286 15222 145 145 0 16141 0
[pid=9156] vsize: 65144
Current children cumulated CPU time (s) 408.75
Current children cumulated vsize (Kb) 67268

[startup+420.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 19327 0 0 0 41761 110 0 0 25 0 1 0 1846656060 68108288 15564 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 16628 15564 145 145 0 16483 0
[pid=9156] vsize: 66512
Current children cumulated CPU time (s) 418.72
Current children cumulated vsize (Kb) 68636

[startup+430.031 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 19684 0 0 0 42755 112 0 0 25 0 1 0 1846656060 69570560 15921 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 16985 15921 145 145 0 16840 0
[pid=9156] vsize: 67940
Current children cumulated CPU time (s) 428.68
Current children cumulated vsize (Kb) 70064

[startup+440.032 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 20024 0 0 0 43749 115 0 0 25 0 1 0 1846656060 70959104 16261 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 17324 16261 145 145 0 17179 0
[pid=9156] vsize: 69296
Current children cumulated CPU time (s) 438.65
Current children cumulated vsize (Kb) 71420

[startup+450.032 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 20364 0 0 0 44745 117 0 0 25 0 1 0 1846656060 72347648 16601 4294967295 134512640 135094434 3221224432 3221223024 134556966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 17663 16601 145 145 0 17518 0
[pid=9156] vsize: 70652
Current children cumulated CPU time (s) 448.63
Current children cumulated vsize (Kb) 72776

[startup+460.033 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 20706 0 0 0 45740 119 0 0 25 0 1 0 1846656060 73748480 16943 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 18005 16943 145 145 0 17860 0
[pid=9156] vsize: 72020
Current children cumulated CPU time (s) 458.6
Current children cumulated vsize (Kb) 74144

[startup+470.035 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 21057 0 0 0 46735 122 0 0 25 0 1 0 1846656060 75186176 17294 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 18356 17294 145 145 0 18211 0
[pid=9156] vsize: 73424
Current children cumulated CPU time (s) 468.58
Current children cumulated vsize (Kb) 75548

[startup+480.035 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 21456 0 0 0 47729 124 0 0 25 0 1 0 1846656060 76824576 17693 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 18756 17693 145 145 0 18611 0
[pid=9156] vsize: 75024
Current children cumulated CPU time (s) 478.54
Current children cumulated vsize (Kb) 77148

[startup+490.036 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 21814 0 0 0 48725 126 0 0 25 0 1 0 1846656060 78299136 18051 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19116 18051 145 145 0 18971 0
[pid=9156] vsize: 76464
Current children cumulated CPU time (s) 488.52
Current children cumulated vsize (Kb) 78588

[startup+500.038 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22608 0 0 0 49718 129 0 0 25 0 1 0 1846656060 79720448 18524 4294967295 134512640 135094434 3221224432 3221223248 134558992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19463 18524 145 145 0 19318 0
[pid=9156] vsize: 77852
Current children cumulated CPU time (s) 498.48
Current children cumulated vsize (Kb) 79976

[startup+510.038 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22614 0 0 0 50717 130 0 0 25 0 1 0 1846656060 79720448 18530 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19463 18530 145 145 0 19318 0
[pid=9156] vsize: 77852
Current children cumulated CPU time (s) 508.48
Current children cumulated vsize (Kb) 79976

[startup+520.039 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22614 0 0 0 51717 130 0 0 25 0 1 0 1846656060 79720448 18530 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19463 18530 145 145 0 19318 0
[pid=9156] vsize: 77852
Current children cumulated CPU time (s) 518.48
Current children cumulated vsize (Kb) 79976

[startup+530.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22614 0 0 0 52716 131 0 0 25 0 1 0 1846656060 79720448 18530 4294967295 134512640 135094434 3221224432 3221223104 134555556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19463 18530 145 145 0 19318 0
[pid=9156] vsize: 77852
Current children cumulated CPU time (s) 528.48
Current children cumulated vsize (Kb) 79976

[startup+540.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22614 0 0 0 53716 131 0 0 25 0 1 0 1846656060 79720448 18530 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19463 18530 145 145 0 19318 0
[pid=9156] vsize: 77852
Current children cumulated CPU time (s) 538.48
Current children cumulated vsize (Kb) 79976

[startup+550.041 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22614 0 0 0 54716 131 0 0 25 0 1 0 1846656060 79720448 18530 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19463 18530 145 145 0 19318 0
[pid=9156] vsize: 77852
Current children cumulated CPU time (s) 548.48
Current children cumulated vsize (Kb) 79976

[startup+560.042 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22614 0 0 0 55716 131 0 0 25 0 1 0 1846656060 79720448 18530 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19463 18530 145 145 0 19318 0
[pid=9156] vsize: 77852
Current children cumulated CPU time (s) 558.48
Current children cumulated vsize (Kb) 79976

[startup+570.044 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22614 0 0 0 56715 131 0 0 25 0 1 0 1846656060 79720448 18530 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19463 18530 145 145 0 19318 0
[pid=9156] vsize: 77852
Current children cumulated CPU time (s) 568.47
Current children cumulated vsize (Kb) 79976

[startup+580.044 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22614 0 0 0 57715 132 0 0 25 0 1 0 1846656060 79720448 18530 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19463 18530 145 145 0 19318 0
[pid=9156] vsize: 77852
Current children cumulated CPU time (s) 578.48
Current children cumulated vsize (Kb) 79976

[startup+590.046 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22614 0 0 0 58715 132 0 0 25 0 1 0 1846656060 79720448 18530 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19463 18530 145 145 0 19318 0
[pid=9156] vsize: 77852
Current children cumulated CPU time (s) 588.48
Current children cumulated vsize (Kb) 79976

[startup+600.048 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22774 0 0 0 59714 133 0 0 25 0 1 0 1846656060 79867904 18565 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19499 18565 145 145 0 19354 0
[pid=9156] vsize: 77996
Current children cumulated CPU time (s) 598.48
Current children cumulated vsize (Kb) 80120

[startup+610.048 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22774 0 0 0 60713 133 0 0 25 0 1 0 1846656060 79867904 18565 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19499 18565 145 145 0 19354 0
[pid=9156] vsize: 77996
Current children cumulated CPU time (s) 608.47
Current children cumulated vsize (Kb) 80120

[startup+620.05 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22774 0 0 0 61713 134 0 0 25 0 1 0 1846656060 79867904 18565 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19499 18565 145 145 0 19354 0
[pid=9156] vsize: 77996
Current children cumulated CPU time (s) 618.48
Current children cumulated vsize (Kb) 80120

[startup+630.051 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22774 0 0 0 62712 134 0 0 25 0 1 0 1846656060 79867904 18565 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19499 18565 145 145 0 19354 0
[pid=9156] vsize: 77996
Current children cumulated CPU time (s) 628.47
Current children cumulated vsize (Kb) 80120

[startup+640.051 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22899 0 0 0 63712 135 0 0 25 0 1 0 1846656060 79867904 18565 4294967295 134512640 135094434 3221224432 3221221360 134541721 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19499 18565 145 145 0 19354 0
[pid=9156] vsize: 77996
Current children cumulated CPU time (s) 638.48
Current children cumulated vsize (Kb) 80120

[startup+650.052 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 64711 135 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0
[pid=9156] vsize: 78508
Current children cumulated CPU time (s) 648.47
Current children cumulated vsize (Kb) 80632

[startup+660.053 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 65711 135 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0
[pid=9156] vsize: 78508
Current children cumulated CPU time (s) 658.47
Current children cumulated vsize (Kb) 80632

[startup+670.054 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 66711 136 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0
[pid=9156] vsize: 78508
Current children cumulated CPU time (s) 668.48
Current children cumulated vsize (Kb) 80632

[startup+680.055 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 67711 136 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0
[pid=9156] vsize: 78508
Current children cumulated CPU time (s) 678.48
Current children cumulated vsize (Kb) 80632

[startup+690.057 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 68710 136 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0
[pid=9156] vsize: 78508
Current children cumulated CPU time (s) 688.47
Current children cumulated vsize (Kb) 80632

[startup+700.058 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 69710 136 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0
[pid=9156] vsize: 78508
Current children cumulated CPU time (s) 698.47
Current children cumulated vsize (Kb) 80632

[startup+710.058 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 70710 136 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0
[pid=9156] vsize: 78508
Current children cumulated CPU time (s) 708.47
Current children cumulated vsize (Kb) 80632

[startup+720.06 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 71710 136 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0
[pid=9156] vsize: 78508
Current children cumulated CPU time (s) 718.47
Current children cumulated vsize (Kb) 80632

[startup+730.061 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 72709 137 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0
[pid=9156] vsize: 78508
Current children cumulated CPU time (s) 728.47
Current children cumulated vsize (Kb) 80632

[startup+740.062 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 73709 137 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0
[pid=9156] vsize: 78508
Current children cumulated CPU time (s) 738.47
Current children cumulated vsize (Kb) 80632

[startup+750.063 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 74709 138 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0
[pid=9156] vsize: 78508
Current children cumulated CPU time (s) 748.48
Current children cumulated vsize (Kb) 80632

[startup+760.063 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 75709 138 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0
[pid=9156] vsize: 78508
Current children cumulated CPU time (s) 758.48
Current children cumulated vsize (Kb) 80632

[startup+770.064 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 76709 138 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0
[pid=9156] vsize: 78508
Current children cumulated CPU time (s) 768.48
Current children cumulated vsize (Kb) 80632

[startup+780.065 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 23050 0 0 0 77709 138 0 0 25 0 1 0 1846656060 80609280 18716 4294967295 134512640 135094434 3221224432 3221223088 134558026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 19680 18716 145 145 0 19535 0
[pid=9156] vsize: 78720
Current children cumulated CPU time (s) 778.48
Current children cumulated vsize (Kb) 80844

[startup+790.066 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 23322 0 0 0 78705 140 0 0 25 0 1 0 1846656060 81723392 18988 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 19952 18988 145 145 0 19807 0
[pid=9156] vsize: 79808
Current children cumulated CPU time (s) 788.46
Current children cumulated vsize (Kb) 81932

[startup+800.066 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 23623 0 0 0 79699 142 0 0 25 0 1 0 1846656060 82956288 19289 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 20253 19289 145 145 0 20108 0
[pid=9156] vsize: 81012
Current children cumulated CPU time (s) 798.42
Current children cumulated vsize (Kb) 83136

[startup+810.067 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 23948 0 0 0 80694 145 0 0 25 0 1 0 1846656060 84287488 19614 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 20578 19614 145 145 0 20433 0
[pid=9156] vsize: 82312
Current children cumulated CPU time (s) 808.4
Current children cumulated vsize (Kb) 84436

[startup+820.068 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 24332 0 0 0 81689 147 0 0 25 0 1 0 1846656060 85856256 19998 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 20961 19998 145 145 0 20816 0
[pid=9156] vsize: 83844
Current children cumulated CPU time (s) 818.37
Current children cumulated vsize (Kb) 85968

[startup+830.068 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 24684 0 0 0 82684 149 0 0 25 0 1 0 1846656060 87298048 20350 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 21313 20350 145 145 0 21168 0
[pid=9156] vsize: 85252
Current children cumulated CPU time (s) 828.34
Current children cumulated vsize (Kb) 87376

[startup+840.069 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 25037 0 0 0 83679 151 0 0 25 0 1 0 1846656060 88748032 20703 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 21667 20703 145 145 0 21522 0
[pid=9156] vsize: 86668
Current children cumulated CPU time (s) 838.31
Current children cumulated vsize (Kb) 88792

[startup+850.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 25360 0 0 0 84674 153 0 0 25 0 1 0 1846656060 90066944 21026 4294967295 134512640 135094434 3221224432 3221223024 134556891 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 21989 21026 145 145 0 21844 0
[pid=9156] vsize: 87956
Current children cumulated CPU time (s) 848.28
Current children cumulated vsize (Kb) 90080

[startup+860.071 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 25671 0 0 0 85669 155 0 0 25 0 1 0 1846656060 91336704 21337 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 22299 21337 145 145 0 22154 0
[pid=9156] vsize: 89196
Current children cumulated CPU time (s) 858.25
Current children cumulated vsize (Kb) 91320

[startup+870.072 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 26001 0 0 0 86664 157 0 0 25 0 1 0 1846656060 92684288 21667 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 22628 21667 145 145 0 22483 0
[pid=9156] vsize: 90512
Current children cumulated CPU time (s) 868.22
Current children cumulated vsize (Kb) 92636

[startup+880.073 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 26245 0 0 0 87659 159 0 0 25 0 1 0 1846656060 93683712 21911 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 22872 21911 145 145 0 22727 0
[pid=9156] vsize: 91488
Current children cumulated CPU time (s) 878.19
Current children cumulated vsize (Kb) 93612

[startup+890.074 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 26546 0 0 0 88655 161 0 0 25 0 1 0 1846656060 94912512 22212 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 23172 22212 145 145 0 23027 0
[pid=9156] vsize: 92688
Current children cumulated CPU time (s) 888.17
Current children cumulated vsize (Kb) 94812

[startup+900.074 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 26872 0 0 0 89649 163 0 0 25 0 1 0 1846656060 96243712 22538 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 23497 22538 145 145 0 23352 0
[pid=9156] vsize: 93988
Current children cumulated CPU time (s) 898.13
Current children cumulated vsize (Kb) 96112

[startup+910.074 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 27154 0 0 0 90646 164 0 0 25 0 1 0 1846656060 97398784 22820 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 23779 22820 145 145 0 23634 0
[pid=9156] vsize: 95116
Current children cumulated CPU time (s) 908.11
Current children cumulated vsize (Kb) 97240

[startup+920.075 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 27492 0 0 0 91640 166 0 0 25 0 1 0 1846656060 98779136 23158 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 24116 23158 145 145 0 23971 0
[pid=9156] vsize: 96464
Current children cumulated CPU time (s) 918.07
Current children cumulated vsize (Kb) 98588

[startup+930.075 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 27753 0 0 0 92637 168 0 0 25 0 1 0 1846656060 99852288 23419 4294967295 134512640 135094434 3221224432 3221222960 134783376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 24378 23419 145 145 0 24233 0
[pid=9156] vsize: 97512
Current children cumulated CPU time (s) 928.06
Current children cumulated vsize (Kb) 99636

[startup+940.076 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 27963 0 0 0 93633 169 0 0 25 0 1 0 1846656060 100708352 23629 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 24587 23629 145 145 0 24442 0
[pid=9156] vsize: 98348
Current children cumulated CPU time (s) 938.03
Current children cumulated vsize (Kb) 100472

[startup+950.077 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 28173 0 0 0 94630 171 0 0 25 0 1 0 1846656060 101568512 23839 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 24797 23839 145 145 0 24652 0
[pid=9156] vsize: 99188
Current children cumulated CPU time (s) 948.02
Current children cumulated vsize (Kb) 101312

[startup+960.076 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 28361 0 0 0 95628 172 0 0 25 0 1 0 1846656060 102338560 24027 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 24985 24027 145 145 0 24840 0
[pid=9156] vsize: 99940
Current children cumulated CPU time (s) 958.01
Current children cumulated vsize (Kb) 102064

[startup+970.077 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 28485 0 0 0 96627 173 0 0 25 0 1 0 1846656060 102842368 24151 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 25108 24151 145 145 0 24963 0
[pid=9156] vsize: 100432
Current children cumulated CPU time (s) 968.01
Current children cumulated vsize (Kb) 102556

[startup+980.078 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 28625 0 0 0 97624 173 0 0 25 0 1 0 1846656060 103415808 24291 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 25248 24291 145 145 0 25103 0
[pid=9156] vsize: 100992
Current children cumulated CPU time (s) 977.98
Current children cumulated vsize (Kb) 103116

[startup+990.078 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 28846 0 0 0 98621 175 0 0 25 0 1 0 1846656060 104321024 24512 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 25469 24512 145 145 0 25324 0
[pid=9156] vsize: 101876
Current children cumulated CPU time (s) 987.97
Current children cumulated vsize (Kb) 104000

[startup+1000.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 29042 0 0 0 99617 176 0 0 25 0 1 0 1846656060 105119744 24708 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 25664 24708 145 145 0 25519 0
[pid=9156] vsize: 102656
Current children cumulated CPU time (s) 997.94
Current children cumulated vsize (Kb) 104780

[startup+1010.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 29294 0 0 0 100612 178 0 0 25 0 1 0 1846656060 106151936 24960 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 25916 24960 145 145 0 25771 0
[pid=9156] vsize: 103664
Current children cumulated CPU time (s) 1007.91
Current children cumulated vsize (Kb) 105788

[startup+1020.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 29484 0 0 0 101609 179 0 0 25 0 1 0 1846656060 106926080 25150 4294967295 134512640 135094434 3221224432 3221223024 134556931 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 26105 25150 145 145 0 25960 0
[pid=9156] vsize: 104420
Current children cumulated CPU time (s) 1017.89
Current children cumulated vsize (Kb) 106544

[startup+1030.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 29734 0 0 0 102606 180 0 0 25 0 1 0 1846656060 107954176 25400 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 26356 25400 145 145 0 26211 0
[pid=9156] vsize: 105424
Current children cumulated CPU time (s) 1027.87
Current children cumulated vsize (Kb) 107548

[startup+1040.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 29910 0 0 0 103604 181 0 0 25 0 1 0 1846656060 108670976 25576 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 26531 25576 145 145 0 26386 0
[pid=9156] vsize: 106124
Current children cumulated CPU time (s) 1037.86
Current children cumulated vsize (Kb) 108248

[startup+1050.08 s]
Raw data (loadavg): 1.00 0.99 0.96 3/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 30120 0 0 0 104601 182 0 0 25 0 1 0 1846656060 109531136 25786 4294967295 134512640 135094434 3221224432 3221223120 134554728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 26741 25786 145 145 0 26596 0
[pid=9156] vsize: 106964
Current children cumulated CPU time (s) 1047.84
Current children cumulated vsize (Kb) 109088

[startup+1060.08 s]
Raw data (loadavg): 1.00 0.99 0.96 1/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) T 9152 9152 20115 0 -1 0 30302 0 0 0 105597 183 0 0 25 0 1 0 1846656060 110272512 25968 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/9156/statm): 26922 25968 145 145 0 26777 0
[pid=9156] vsize: 107688
Current children cumulated CPU time (s) 1057.81
Current children cumulated vsize (Kb) 109812

[startup+1070.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 30532 0 0 0 106593 186 0 0 25 0 1 0 1846656060 111218688 26198 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 27153 26198 145 145 0 27008 0
[pid=9156] vsize: 108612
Current children cumulated CPU time (s) 1067.8
Current children cumulated vsize (Kb) 110736

[startup+1080.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 30774 0 0 0 107590 187 0 0 25 0 1 0 1846656060 112209920 26440 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 27395 26440 145 145 0 27250 0
[pid=9156] vsize: 109580
Current children cumulated CPU time (s) 1077.78
Current children cumulated vsize (Kb) 111704

[startup+1090.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 30945 0 0 0 108588 188 0 0 25 0 1 0 1846656060 112910336 26611 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 27566 26611 145 145 0 27421 0
[pid=9156] vsize: 110264
Current children cumulated CPU time (s) 1087.77
Current children cumulated vsize (Kb) 112388

[startup+1100.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 31161 0 0 0 109585 190 0 0 25 0 1 0 1846656060 113795072 26827 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 27782 26827 145 145 0 27637 0
[pid=9156] vsize: 111128
Current children cumulated CPU time (s) 1097.76
Current children cumulated vsize (Kb) 113252

[startup+1110.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 31401 0 0 0 110582 191 0 0 25 0 1 0 1846656060 114769920 27067 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 28020 27067 145 145 0 27875 0
[pid=9156] vsize: 112080
Current children cumulated CPU time (s) 1107.74
Current children cumulated vsize (Kb) 114204

[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 31635 0 0 0 111578 193 0 0 25 0 1 0 1846656060 115720192 27301 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 28252 27301 145 145 0 28107 0
[pid=9156] vsize: 113008
Current children cumulated CPU time (s) 1117.72
Current children cumulated vsize (Kb) 115132

[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 31835 0 0 0 112574 195 0 0 25 0 1 0 1846656060 116539392 27501 4294967295 134512640 135094434 3221224432 3221223024 134556908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 28452 27501 145 145 0 28307 0
[pid=9156] vsize: 113808
Current children cumulated CPU time (s) 1127.7
Current children cumulated vsize (Kb) 115932

[startup+1140.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 32047 0 0 0 113571 196 0 0 25 0 1 0 1846656060 117399552 27713 4294967295 134512640 135094434 3221224432 3221223024 134557248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 28662 27713 145 145 0 28517 0
[pid=9156] vsize: 114648
Current children cumulated CPU time (s) 1137.68
Current children cumulated vsize (Kb) 116772

[startup+1150.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 32294 0 0 0 114568 197 0 0 25 0 1 0 1846656060 118411264 27960 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 28909 27960 145 145 0 28764 0
[pid=9156] vsize: 115636
Current children cumulated CPU time (s) 1147.66
Current children cumulated vsize (Kb) 117760

[startup+1160.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 32479 0 0 0 115565 198 0 0 25 0 1 0 1846656060 119164928 28145 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9156/statm): 29093 28145 145 145 0 28948 0
[pid=9156] vsize: 116372
Current children cumulated CPU time (s) 1157.64
Current children cumulated vsize (Kb) 118496

[startup+1170.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 32579 0 0 0 116564 199 0 0 25 0 1 0 1846656060 119865344 28245 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 29264 28245 145 145 0 29119 0
[pid=9156] vsize: 117056
Current children cumulated CPU time (s) 1167.64
Current children cumulated vsize (Kb) 119180

[startup+1180.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 32759 0 0 0 117562 200 0 0 25 0 1 0 1846656060 120606720 28425 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 29445 28425 145 145 0 29300 0
[pid=9156] vsize: 117780
Current children cumulated CPU time (s) 1177.63
Current children cumulated vsize (Kb) 119904

[startup+1190.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 32967 0 0 0 118558 202 0 0 25 0 1 0 1846656060 121462784 28633 4294967295 134512640 135094434 3221224432 3221223120 134554726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 29654 28633 145 145 0 29509 0
[pid=9156] vsize: 118616
Current children cumulated CPU time (s) 1187.61
Current children cumulated vsize (Kb) 120740

[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 33281 0 0 0 119554 204 0 0 25 0 1 0 1846656060 122744832 28947 4294967295 134512640 135094434 3221224432 3221223024 134557375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9156/statm): 29967 28947 145 145 0 29822 0
[pid=9156] vsize: 119868
Current children cumulated CPU time (s) 1197.59
Current children cumulated vsize (Kb) 121992

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.96 1/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) T 9152 9152 20115 0 -1 0 33613 0 0 0 120550 206 0 0 25 0 1 0 1846656060 124108800 29279 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/9156/statm): 30300 29279 145 145 0 30155 0
[pid=9156] vsize: 121200
Current children cumulated CPU time (s) 1207.57
Current children cumulated vsize (Kb) 123324



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.96 1/57 9156
Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9152/statm): 531 226 485 147 0 384 0
[pid=9152] vsize: 2124
Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) T 9152 9152 20115 0 -1 0 33613 0 0 0 120550 206 0 0 25 0 1 0 1846656060 124108800 29279 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/9156/statm): 30300 29279 145 145 0 30155 0
[pid=9156] vsize: 121200
Current children cumulated CPU time (s) 1207.57
Current children cumulated vsize (Kb) 123324

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

Child status: 10
Real time (s): 1210.16
CPU time (s): 1207.62
CPU user time (s): 1205.5
CPU system time (s): 2.11868
CPU usage (%): 99.7905
Max. virtual memory (cumulated for all children) (Kb): 123324

Verifier Data

ERROR: no interpretation found !