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/miplib2003/normalized-mps-v2-20-10-opt1217.opb
MD5SUMdf52a42b636b50954671d81e4d85c221
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -12288
Optimality of the best value was proved NO
Number of terms in the objective function 19
Biggest coefficient in the objective function 262144
Number of bits for the biggest coefficient in the objective function 19
Sum of the numbers in the objective function 524287
Number of bits of the sum of numbers in the objective function 19
Biggest number in a constraint 393216
Number of bits of the biggest number in a constraint 19
Biggest sum of numbers in a constraint 917503
Number of bits of the biggest sum of numbers20
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.01
Number of variables787
Total number of constraints833
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)816
Number of constraints which are nor clauses,nor cardinality constraints17
Minimum length of a constraint1
Maximum length of a constraint67

Trace number 3927

Launcher Data

LAUNCH ON wulflinc25 THE 2005-09-19 03:48:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2932 boxname=wulflinc25 idbench=588 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  df52a42b636b50954671d81e4d85c221  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-opt1217.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-opt1217.opb
IDLAUNCH: 2932
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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.220
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        893648 kB
Buffers:         36384 kB
Cached:          77776 kB
SwapCached:        896 kB
Active:          71808 kB
Inactive:        44980 kB
HighTotal:      131008 kB
HighFree:        51828 kB
LowTotal:       903652 kB
LowFree:        841820 kB
SwapTotal:     2097892 kB
SwapFree:      2096496 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5720 kB
Slab:            18712 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 04:08:56 (client local time) WITH STATUS 10 IN 1208.34 SECONDS
stats: 2932 7 1208.34 10

Solver Data

c Parsing PB file...
c Converting 113 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 111]---> Sorter-cost: 1326     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 110]---> Adder-cost: 115   maxlim: 131070   bits: 18/17
c ---[ 109]---> Adder-cost: 133   maxlim: 131070   bits: 18/17
c ---[ 108]---> Adder-cost: 148   maxlim: 131070   bits: 18/17
c ---[ 107]---> Adder-cost: 139   maxlim: 131070   bits: 18/17
c ---[ 106]---> Adder-cost: 142   maxlim: 131070   bits: 18/17
c ---[ 105]---> Adder-cost: 120   maxlim: 131070   bits: 18/17
c ---[ 104]---> Sorter-cost: 1358     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 102]---> BDD-cost:   29
c ---[ 100]---> BDD-cost:   29
c ---[  98]---> BDD-cost:   29
c ---[  97]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[  95]---> BDD-cost:   29
c ---[  93]---> BDD-cost:   29
c ---[  91]---> BDD-cost:   29
c ---[  89]---> BDD-cost:   29
c ---[  87]---> BDD-cost:   29
c ---[  85]---> BDD-cost:   29
c ---[  83]---> BDD-cost:   29
c ---[  81]---> BDD-cost:   29
c ---[  79]---> BDD-cost:   29
c ---[  77]---> BDD-cost:   29
c ---[  76]---> Sorter-cost: 1387     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[  74]---> BDD-cost:   29
c ---[  72]---> BDD-cost:   29
c ---[  70]---> BDD-cost:   29
c ---[  68]---> BDD-cost:   29
c ---[  66]---> BDD-cost:   29
c ---[  64]---> BDD-cost:   29
c ---[  62]---> BDD-cost:   29
c ---[  60]---> BDD-cost:   29
c ---[  58]---> BDD-cost:   29
c ---[  56]---> BDD-cost:   29
c ---[  55]---> Sorter-cost: 1605     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[  53]---> BDD-cost:   29
c ---[  51]---> BDD-cost:   29
c ---[  49]---> BDD-cost:   29
c ---[  47]---> BDD-cost:   29
c ---[  45]---> BDD-cost:   29
c ---[  43]---> BDD-cost:   29
c ---[  41]---> BDD-cost:   29
c ---[  39]---> BDD-cost:   29
c ---[  37]---> BDD-cost:   29
c ---[  35]---> BDD-cost:   29
c ---[  34]---> Adder-cost: 121   maxlim: 131070   bits: 18/17
c ---[  32]---> BDD-cost:   29
c ---[  30]---> BDD-cost:   29
c ---[  28]---> BDD-cost:   29
c ---[  26]---> BDD-cost:   29
c ---[  24]---> BDD-cost:   29
c ---[  22]---> BDD-cost:   29
c ---[  20]---> BDD-cost:   29
c ---[  18]---> BDD-cost:   29
c ---[  16]---> BDD-cost:   29
c ---[  14]---> BDD-cost:   29
c ---[  13]---> Sorter-cost: 1146     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[  11]---> BDD-cost:   29
c ---[   9]---> BDD-cost:   29
c ---[   7]---> BDD-cost:   29
c ---[   5]---> BDD-cost:   29
c ---[   3]---> BDD-cost:   29
c ---[   2]---> Sorter-cost: 1448     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[   1]---> Adder-cost: 135   maxlim: 131070   bits: 18/17
c ---[   0]---> Sorter-cost: 1460     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   36190    95093 |   12063       0        0     nan |  0.000 % |
c |       100 |   36190    95093 |   13269     100     9213    92.1 |  1.551 % |
c |       250 |   36190    95093 |   14596     250    23775    95.1 |  1.551 % |
c |       475 |   36190    95093 |   16055     475    27646    58.2 |  1.551 % |
c |       815 |   36190    95093 |   17661     815    37796    46.4 |  1.551 % |
c |      1321 |   36190    95093 |   19427    1321    64195    48.6 |  1.551 % |
c |      2080 |   36190    95093 |   21370    2080   150627    72.4 |  1.551 % |
c |      3219 |   36190    95093 |   23507    3219   240663    74.8 |  1.551 % |
c |      4927 |   36190    95093 |   25858    4927   444844    90.3 |  1.551 % |
c |      7490 |   36190    95093 |   28443    7490   630146    84.1 |  1.551 % |
c |     11334 |   36190    95093 |   31288   11334  1111947    98.1 |  1.551 % |
c |     17101 |   36190    95093 |   34417   17101  1995799   116.7 |  1.551 % |
c |     25750 |   36190    95093 |   37858   25750  4048815   157.2 |  1.551 % |
c |     38724 |   36190    95093 |   41644   38724  5509190   142.3 |  1.551 % |
c |     58187 |   36190    95093 |   45809   20391  4361127   213.9 |  1.551 % |
c |     87379 |   36190    95093 |   50390   49583 16357297   329.9 |  1.551 % |
c |    131168 |   36190    95093 |   55429   19264   936058    48.6 |  1.552 % |
c ==============================================================================
c Found solution: 0
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    131669 |   36193    95115 |   12064   19765   950917    48.1 |  1.552 % |
c |    131769 |   36193    95115 |   13270    9983   396054    39.7 |  1.559 % |
c |    131920 |   36193    95115 |   14597   10134   405730    40.0 |  1.559 % |
c |    132147 |   36193    95115 |   16057   10361   414268    40.0 |  1.559 % |
c |    132487 |   36193    95115 |   17662   10701   426919    39.9 |  1.559 % |
c |    132993 |   36193    95115 |   19429   11207   518652    46.3 |  1.559 % |
c |    133752 |   36193    95115 |   21372   11966   570541    47.7 |  1.559 % |
c |    134891 |   36193    95115 |   23509   13105   617310    47.1 |  1.559 % |
c |    136599 |   36193    95115 |   25860   14813   747975    50.5 |  1.559 % |
c |    139161 |   36193    95115 |   28446   17375  1203823    69.3 |  1.559 % |
c |    143005 |   36193    95115 |   31290   21219  1575109    74.2 |  1.559 % |
c |    148772 |   36193    95115 |   34419   26986  3208337   118.9 |  1.559 % |
c |    157421 |   36193    95115 |   37861   35635  3471213    97.4 |  1.559 % |
c |    170395 |   36193    95115 |   41648   20561  2520619   122.6 |  1.559 % |
c |    189856 |   36193    95115 |   45813   40022  6634675   165.8 |  1.559 % |
c |    219049 |   36193    95115 |   50394   31934  5790588   181.3 |  1.559 % |
c |    262838 |   36193    95115 |   55433   34208  6036210   176.5 |  1.559 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1_bit_10 -x1_bit_9 -x1_bit_8 -x1_bit_7 -x1_bit_6 -x1_bit_5 -x1_bit_4 -x1_bit_3 -x1_bit_2 -x1_bit_1 -x1_bit0 -x1_bit1 -x1_bit2 -x1_bit3 -x1_bit4 -x1_bit5 -x1_bit6 -x1_bit7 -x1_bit8 -x2_bit0 -x3_bit0 -x4_bit0 -x5_bit0 -x6_bit0 -x7_bit0 -x8_bit0 -x9_bit0 -x10_bit0 -x11_bit0 -x12_bit0 -x13_bit0 -x14_bit0 -x15_bit0 -x16_bit0 x17_bit0 -x18_bit0 -x19_bit0 -x20_bit0 -x21_bit0 -x22_bit0 -x23_bit0 -x24_bit0 -x25_bit0 -x26_bit0 -x27_bit0 -x28_bit0 -x29_bit0 -x30_bit0 -x31_bit0 -x32_bit0 -x33_bit0 -x34_bit0 -x35_bit0 -x36_bit0 -x37_bit0 -x38_bit0 -x39_bit0 -x40_bit0 -x41_bit0 -x42_bit0 -x43_bit0 -x44_bit0 -x45_bit0 -x46_bit0 -x47_bit0 -x48_bit0 x49_bit0 -x50_bit0 -x51_bit0 -x52_bit0 -x53_bit0 -x54_bit0 -x55_bit0 -x56_bit0 x57_bit0 -x58_bit0 -x59_bit0 -x60_bit0 x61_bit0 x62_bit0 -x63_bit0 -x64_bit0 -x65_bit0 -x66_bit0 -x67_bit0 -x68_bit0 -x69_bit0 -x70_bit0 -x71_bit0 -x72_bit0 x73_bit0 -x74_bit0 -x75_bit0 -x76_bit0 x77_bit0 x78_bit0 -x79_bit0 x80_bit0 x81_bit0 x82_bit0 x83_bit0 x84_bit0 -x85_bit0 x86_bit0 -x87_bit0 -x88_bit0 -x89_bit0 -x90_bit0 -x91_bit0 x92_bit0 x93_bit0 -x94_bit0 -x95_bit0 -x96_bit0 -x97_bit0 -x98_bit0 -x99_bit0 -x100_bit0 -x101_bit0 x102_bit0 x103_bit0 x104_bit0 -x105_bit0 x106_bit0 x107_bit0 -x108_bit0 -x109_bit0 -x110_bit0 x111_bit0 -x112_bit0 -x113_bit0 -x114_bit0 -x115_bit0 -x116_bit0 -x117_bit0 -x118_bit0 -x119_bit0 -x120_bit0 -x121_bit0 -x122_bit0 -x123_bit0 -x124_bit0 -x125_bit0 -x126_bit0 -x127_bit0 -x128_bit0 -x129_bit0 -x130_bit0 -x131_bit0 -x132_bit0 -x133_bit0 -x134_bit0 -x135_bit0 x136_bit0 -x137_bit0 -x138_bit0 -x139_bit0 -x140_bit0 -x141_bit0 -x142_bit0 -x143_bit0 -x144_bit0 -x145_bit0 -x146_bit0 -x147_bit0 -x148_bit0 -x149_bit0 -x150_bit0 -x151_bit0 -x152_bit0 -x153_bit0 -x154_bit0 -x155_bit0 -x156_bit0 -x157_bit0 -x158_bit0 -x159_bit0 -x160_bit0 -x161_bit0 -x162_bit0 -x163_bit0 -x164_bit0 -x165_bit0 -x166_bit0 -x167_bit0 -x168_bit0 -x169_bit0 -x170_bit0 -x171_bit0 -x172_bit0 -x173_bit0 -x174_bit0 -x175_bit0 -x176_bit0 -x177_bit0 -x178_bit0 -x179_bit0 -x180_bit0 -x181_bit0 -x182_bit0 -x183_bit0 -x184_bit0 -x185_bit0 -x186_bit0 -x187_bit0 -x188_bit0 -x189_bit0 -x190_bit0 -x191_bit0 -x192_bit0 -x193_bit0 -x194_bit0 -x195_bit0 -x196_bit0 -x197_bit0 -x198_bit0 -x199_bit0 -x200_bit0 -x201_bit0 -x202_bit0 -x203_bit0 -x204_bit0 -x205_bit0 -x206_bit0 -x207_bit0 -x208_bit0 -x209_bit0 -x210_bit0 -x211_bit0 -x212_bit0 -x213_bit0 -x214_bit0 -x215_bit0 -x216_bit0 -x217_bit0 -x218_bit0 -x219_bit0 -x220_bit0 -x221_bit0 -x222_bit0 -x223_bit0 -x224_bit0 -x225_bit0 -x226_bit0 -x227_bit0 -x228_bit0 -x229_bit0 -x230_bit0 -x231_bit0 -x232_bit0 -x233_bit0 -x234_bit0 -x235_bit0 -x236_bit0 -x237_bit0 -x238_bit0 -x239_bit0 -x240_bit0 x241_bit0 x242_bit0 x243_bit0 x244_bit0 -x245_bit0 -x246_bit0 -x247_bit0 -x248_bit0 -x249_bit0 -x250_bit0 -x251_bit0 x252_bit0 x253_bit0 x254_bit0 x255_bit0 -x256_bit0 x257_bit0 x258_bit0 x259_bit0 -x260_bit0 x261_bit0 x262_bit0 x263_bit0 -x264_bit0 -x265_bit0 x266_bit0 -x267_bit0 -x268_bit0 -x269_bit0 -x270_bit0 -x271_bit0 x272_bit0 -x273_bit0 x274_bit0 x275_bit0 -x276_bit0 x277_bit0 x278_bit0 -x279_bit0 -x280_bit0 x281_bit0 x282_bit0 x283_bit0 -x284_bit0 -x285_bit0 -x286_bit0 -x287_bit0 -x288_bit0 -x289_bit0 -x290_bit0 -x291_bit0 -x292_bit0 -x293_bit0 -x294_bit0 -x295_bit0 -x296_bit0 -x297_bit0 -x298_bit0 -x299_bit0 -x300_bit0 -x301_bit0 -x302_bit0 -x303_bit0 -x304_bit0 -x305_bit0 -x306_bit0 -x307_bit0 -x308_bit0 -x309_bit0 -x310_bit0 -x311_bit0 -x312_bit0 -x313_bit0 -x314_bit0 -x315_bit0 -x316_bit0 -x317_bit0 -x318_bit0 -x319_bit0 -x320_bit0 -x321_bit0 -x322_bit0 -x323_bit0 -x324_bit0 -x325_bit0 -x326_bit0 -x327_bit0 -x328_bit0 -x329_bit0 -x330_bit0 -x331_bit0 -x332_bit0 -x333_bit0 -x334_bit0 -x335_bit0 -x336_bit0 -x337_bit0 -x338_bit0 -x339_bit0 -x340_bit0 -x341_bit0 -x342_bit0 -x343_bit0 -x344_bit0 -x345_bit0 -x346_bit0 -x347_bit0 -x348_bit0 -x349_bit0 -x350_bit0 -x351_bit0 -x352_bit0 -x353_bit0 -x354_bit0 -x355_bit0 -x356_bit0 -x357_bit0 -x358_bit0 -x359_bit0 -x360_bit0 -x361_bit0 -x362_bit0 -x363_bit0 -x364_bit0 -x365_bit0 -x366_bit0 -x367_bit0 -x368_bit0 -x369_bit0 -x370_bit0 -x371_bit0 -x372_bit0 -x373_bit0 -x374_bit0 -x375_bit0 -x376_bit0 -x377_bit0 -x378_bit0 -x379_bit0 -x380_bit0 -x381_bit0 -x382_bit0 -x383_bit0 -x384_bit0 -x385_bit0 -x386_bit0 -x387_bit0 -x388_bit0 -x389_bit0 -x390_bit0 -x391_bit0 -x392_bit0 -x393_bit0 -x394_bit0 -x395_bit0 -x396_bit0 -x397_bit0 -x398_bit0 -x399_bit0 x400_bit0 -x401_bit0 -x402_bit0 -x403_bit0 -x404_bit0 -x405_bit0 -x406_bit0 -x407_bit0 -x408_bit0 -x409_bit0 -x410_bit0 -x411_bit0 -x412_bit0 -x413_bit0 -x414_bit0 -x415_bit0 -x416_bit0 -x417_bit0 -x418_bit0 -x419_bit0 -x420_bit0 -x421_bit0 -x422_bit0 -x423_bit0 -x424_bit0 -x425_bit0 -x426_bit0 -x427_bit0 -x428_bit0 -x429_bit0 -x430_bit0 -x431_bit0 -x432_bit0 -x433_bit0 -x434_bit0 -x435_bit0 -x436_bit0 -x437_bit0 -x438_bit0 -x439_bit0 -x440_bit0 -x441_bit0 -x442_bit0 -x443_bit0 -x444_bit0 -x445_bit0 -x446_bit0 -x447_bit0 -x448_bit0 -x449_bit0 -x450_bit0 -x451_bit0 -x452_bit0 -x453_bit0 -x454_bit0 -x455_bit0 -x456_bit0 -x457_bit0 -x458_bit0 -x459_bit0 -x460_bit0 -x461_bit0 -x462_bit0 -x463_bit0 -x464_bit0 -x465_bit0 -x466_bit0 -x467_bit0 -x468_bit0 -x469_bit0 -x470_bit0 -x471_bit0 -x472_bit0 -x473_bit0 -x474_bit0 -x475_bit0 -x476_bit0 -x477_bit0 -x478_bit0 -x479_bit0 -x480_bit0 -x481_bit0 -x482_bit0 -x483_bit0 -x484_bit0 -x485_bit0 -x486_bit0 -x487_bit0 -x488_bit0 -x489_bit0 -x490_bit0 -x491_bit0 -x492_bit0 -x493_bit0 -x494_bit0 -x495_bit0 -x496_bit0 -x497_bit0 -x498_bit0 -x499_bit0 -x500_bit0 -x501_bit0 -x502_bit0 -x503_bit0 -x504_bit0 -x505_bit0 -x506_bit0 -x507_bit0 -x508_bit0 -x509_bit0 -x510_bit0 -x511_bit0 -x512_bit0 -x513_bit0 -x514_bit0 -x515_bit0 -x516_bit0 -x517_bit0 -x518_bit0 -x519_bit0 -x520_bit0 -x521_bit0 -x522_bit0 -x523_bit0 -x524_bit0 -x525_bit0 -x526_bit0 -x527_bit0 -x528_bit0 -x529_bit0 -x530_bit0 -x531_bit0 -x532_bit0 -x533_bit0 -x534_bit0 -x535_bit0 -x536_bit0 -x537_bit0 -x538_bit0 -x539_bit0 -x540_bit0 -x541_bit0 -x542_bit0 -x543_bit0 -x544_bit0 -x545_bit0 -x546_bit0 -x547_bit0 -x548_bit0 -x549_bit0 -x550_bit0 -x551_bit0 -x552_bit0 -x553_bit0 -x554_bit0 -x555_bit0 -x556_bit0 -x557_bit0 -x558_bit0 -x559_bit0 -x560_bit0 -x561_bit0 -x562_bit0 -x563_bit0 -x564_bit0 -x565_bit0 -x566_bit0 -x567_bit0 -x568_bit0 -x569_bit0 -x570_bit0 -x571_bit0 -x572_bit0 -x573_bit0 -x574_bit0 -x575_bit0 -x576_bit0 -x577_bit0 -x578_bit0 -x579_bit0 -x580_bit0 -x581_bit0 -x582_bit0 -x583_bit0 -x584_bit0 -x585_bit0 -x586_bit0 -x587_bit0 -x588_bit0 -x589_bit0 -x590_bit0 -x591_bit0 -x592_bit0 -x593_bit0 -x594_bit0 -x595_bit0 -x596_bit0 -x597_bit0 -x598_bit0 -x599_bit0 -x600_bit0 -x601_bit0 -x602_bit0 -x603_bit0 -x604_bit0 -x605_bit0 -x606_bit0 -x607_bit0 -x608_bit0 -x609_bit0 -x610_bit0 -x611_bit0 -x612_bit0 -x613_bit0 -x614_bit0 -x615_bit0 -x616_bit0 -x617_bit0 -x618_bit0 -x619_bit0 -x620_bit0 -x621_bit0 -x622_bit0 -x623_bit0 -x624_bit0 -x625_bit0 -x626_bit0 -x627_bit0 -x628_bit0 -x629_bit0 -x630_bit0 -x631_bit0 -x632_bit0 -x633_bit0 -x634_bit0 -x635_bit0 -x636_bit0 -x637_bit0 -x638_bit0 -x639_bit0 -x640_bit0 -x641_bit0 -x642_bit0 -x643_bit0 -x644_bit0 -x645_bit0 -x646_bit0 -x647_bit0 -x648_bit0 -x649_bit0 -x650_bit0 -x651_bit0 -x652_bit0 -x653_bit0 -x654_bit0 -x655_bit0 -x656_bit0 -x657_bit0 -x658_bit0 -x659_bit0 -x660_bit0 -x661_bit0 -x662_bit0 -x663_bit0 -x664_bit0 -x665_bit0 -x666_bit0 -x667_bit0 -x668_bit0 -x669_bit0 -x670_bit0 -x671_bit0 -x672_bit0 -x673_bit0 -x674_bit0 -x675_bit0 -x676_bit0 -x677_bit0 -x678_bit0 -x679_bit0 -x680_bit0 -x681_bit0 -x682_bit0 -x683_bit0 -x684_bit0 -x685_bit0 -x686_bit0 -x687_bit0 -x688_bit0 -x689_bit0 -x690_bit0 -x691_bit0 -x692_bit0 -x693_bit0 -x694_bit0 -x695_bit0 -x696_bit0 -x697_bit0 -x698_bit0 -x699_bit0 -x700_bit0 -x701_bit0 -x702_bit0 -x703_bit0 -x704_bit0 -x705_bit0 -x706_bit0 -x707_bit0 -x708_bit0 -x709_bit0 -x710_bit0 -x711_bit0 -x712_bit0 -x713_bit0 -x714_bit0 -x715_bit0 -x716_bit0 -x717_bit0 -x718_bit0 -x719_bit0 -x720_bit0 -x721_bit0 -x722_bit0 x723_bit0 -x724_bit0 -x725_bit0 -x726_bit0 -x727_bit0 -x728_bit0 -x729_bit0 -x730_bit0 -x731_bit0 -x732_bit0 -x733_bit0 -x734_bit0 -x735_bit0 -x736_bit0 -x737_bit0 -x738_bit0 -x739_bit0 -x740_

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/19538/stat): 19538 (minisat+_script) R 19537 19538 4419 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846805926 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/19538/statm): 174 3 169 147 0 27 0
[pid=19538] 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=19539
New process pid=19540
New process pid=19541
execve syscall for /bin/sed executable
One traced child (pid=19540) 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=19541) exited with status: 0
One traced child (pid=19539) exited with status: 0
New process pid=19542
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-opt1217.opb

[startup+10.0031 s]
Raw data (loadavg): 0.93 0.95 0.98 1/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) T 19538 19538 4419 0 -1 0 1742 0 0 0 976 9 0 0 25 0 1 0 1846805931 7569408 1691 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/19542/statm): 1848 1691 145 145 0 1703 0
[pid=19542] vsize: 7392
Current children cumulated CPU time (s) 9.85
Current children cumulated vsize (Kb) 9516

[startup+20.0048 s]
Raw data (loadavg): 0.94 0.96 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 2291 0 0 0 1965 13 0 0 25 0 1 0 1846805931 9830400 2240 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 2400 2240 145 145 0 2255 0
[pid=19542] vsize: 9600
Current children cumulated CPU time (s) 19.78
Current children cumulated vsize (Kb) 11724

[startup+30.0063 s]
Raw data (loadavg): 0.95 0.96 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) T 19538 19538 4419 0 -1 0 2905 0 0 0 2953 19 0 0 25 0 1 0 1846805931 12333056 2854 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/19542/statm): 3011 2854 145 145 0 2866 0
[pid=19542] vsize: 12044
Current children cumulated CPU time (s) 29.72
Current children cumulated vsize (Kb) 14168

[startup+40.0059 s]
Raw data (loadavg): 0.95 0.96 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 3473 0 0 0 3942 22 0 0 25 0 1 0 1846805931 14708736 3422 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 3591 3422 145 145 0 3446 0
[pid=19542] vsize: 14364
Current children cumulated CPU time (s) 39.64
Current children cumulated vsize (Kb) 16488

[startup+50.0066 s]
Raw data (loadavg): 0.96 0.96 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 4177 0 0 0 4930 28 0 0 25 0 1 0 1846805931 17580032 4126 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 4292 4126 145 145 0 4147 0
[pid=19542] vsize: 17168
Current children cumulated CPU time (s) 49.58
Current children cumulated vsize (Kb) 19292

[startup+60.0072 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 4829 0 0 0 5917 34 0 0 25 0 1 0 1846805931 20242432 4778 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 4942 4778 145 145 0 4797 0
[pid=19542] vsize: 19768
Current children cumulated CPU time (s) 59.51
Current children cumulated vsize (Kb) 21892

[startup+70.0088 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 5440 0 0 0 6905 39 0 0 25 0 1 0 1846805931 22736896 5389 4294967295 134512640 135094434 3221224432 3221223120 134554733 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 5551 5389 145 145 0 5406 0
[pid=19542] vsize: 22204
Current children cumulated CPU time (s) 69.44
Current children cumulated vsize (Kb) 24328

[startup+80.0094 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 5774 0 0 0 7897 43 0 0 25 0 1 0 1846805931 24080384 5723 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 5879 5723 145 145 0 5734 0
[pid=19542] vsize: 23516
Current children cumulated CPU time (s) 79.4
Current children cumulated vsize (Kb) 25640

[startup+90.01 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 6380 0 0 0 8887 48 0 0 17 0 1 0 1846805931 26681344 6329 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 6514 6329 145 145 0 6369 0
[pid=19542] vsize: 26056
Current children cumulated CPU time (s) 89.35
Current children cumulated vsize (Kb) 28180

[startup+100.011 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 7082 0 0 0 9876 52 0 0 25 0 1 0 1846805931 29544448 7031 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 7213 7031 145 145 0 7068 0
[pid=19542] vsize: 28852
Current children cumulated CPU time (s) 99.28
Current children cumulated vsize (Kb) 30976

[startup+110.011 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 7699 0 0 0 10865 57 0 0 25 0 1 0 1846805931 32055296 7648 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 7826 7648 145 145 0 7681 0
[pid=19542] vsize: 31304
Current children cumulated CPU time (s) 109.22
Current children cumulated vsize (Kb) 33428

[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 8400 0 0 0 11854 61 0 0 25 0 1 0 1846805931 34910208 8349 4294967295 134512640 135094434 3221224432 3221223024 134556815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 8523 8349 145 145 0 8378 0
[pid=19542] vsize: 34092
Current children cumulated CPU time (s) 119.15
Current children cumulated vsize (Kb) 36216

[startup+130.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 9078 0 0 0 12842 66 0 0 25 0 1 0 1846805931 37675008 9027 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 9198 9027 145 145 0 9053 0
[pid=19542] vsize: 36792
Current children cumulated CPU time (s) 129.08
Current children cumulated vsize (Kb) 38916

[startup+140.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 9444 0 0 0 13836 69 0 0 25 0 1 0 1846805931 39170048 9393 4294967295 134512640 135094434 3221224432 3221223104 134556401 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 9563 9393 145 145 0 9418 0
[pid=19542] vsize: 38252
Current children cumulated CPU time (s) 139.05
Current children cumulated vsize (Kb) 40376

[startup+150.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 9444 0 0 0 14836 69 0 0 25 0 1 0 1846805931 39170048 9393 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 9563 9393 145 145 0 9418 0
[pid=19542] vsize: 38252
Current children cumulated CPU time (s) 149.05
Current children cumulated vsize (Kb) 40376

[startup+160.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 9444 0 0 0 15836 69 0 0 25 0 1 0 1846805931 39170048 9393 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 9563 9393 145 145 0 9418 0
[pid=19542] vsize: 38252
Current children cumulated CPU time (s) 159.05
Current children cumulated vsize (Kb) 40376

[startup+170.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 9444 0 0 0 16837 69 0 0 25 0 1 0 1846805931 39170048 9393 4294967295 134512640 135094434 3221224432 3221223024 134557386 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 9563 9393 145 145 0 9418 0
[pid=19542] vsize: 38252
Current children cumulated CPU time (s) 169.06
Current children cumulated vsize (Kb) 40376

[startup+180.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 9444 0 0 0 17837 69 0 0 25 0 1 0 1846805931 39170048 9393 4294967295 134512640 135094434 3221224432 3221223024 134557306 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 9563 9393 145 145 0 9418 0
[pid=19542] vsize: 38252
Current children cumulated CPU time (s) 179.06
Current children cumulated vsize (Kb) 40376

[startup+190.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 9444 0 0 0 18837 69 0 0 25 0 1 0 1846805931 39170048 9393 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 9563 9393 145 145 0 9418 0
[pid=19542] vsize: 38252
Current children cumulated CPU time (s) 189.06
Current children cumulated vsize (Kb) 40376

[startup+200.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 9444 0 0 0 19837 69 0 0 25 0 1 0 1846805931 39170048 9393 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 9563 9393 145 145 0 9418 0
[pid=19542] vsize: 38252
Current children cumulated CPU time (s) 199.06
Current children cumulated vsize (Kb) 40376

[startup+210.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 9964 0 0 0 20828 72 0 0 25 0 1 0 1846805931 41299968 9913 4294967295 134512640 135094434 3221224432 3221223024 134556791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 10083 9913 145 145 0 9938 0
[pid=19542] vsize: 40332
Current children cumulated CPU time (s) 209
Current children cumulated vsize (Kb) 42456

[startup+220.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 10686 0 0 0 21816 77 0 0 25 0 1 0 1846805931 44277760 10635 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 10810 10635 145 145 0 10665 0
[pid=19542] vsize: 43240
Current children cumulated CPU time (s) 218.93
Current children cumulated vsize (Kb) 45364

[startup+230.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 11425 0 0 0 22804 82 0 0 25 0 1 0 1846805931 47316992 11374 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 11552 11374 145 145 0 11407 0
[pid=19542] vsize: 46208
Current children cumulated CPU time (s) 228.86
Current children cumulated vsize (Kb) 48332

[startup+240.017 s]
Raw data (loadavg): 0.99 0.97 0.98 1/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) T 19538 19538 4419 0 -1 0 12043 0 0 0 23794 86 0 0 25 0 1 0 1846805931 49872896 11992 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/19542/statm): 12176 11992 145 145 0 12031 0
[pid=19542] vsize: 48704
Current children cumulated CPU time (s) 238.8
Current children cumulated vsize (Kb) 50828

[startup+250.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 12638 0 0 0 24786 89 0 0 25 0 1 0 1846805931 52338688 12587 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 12778 12587 145 145 0 12633 0
[pid=19542] vsize: 51112
Current children cumulated CPU time (s) 248.75
Current children cumulated vsize (Kb) 53236

[startup+260.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 13216 0 0 0 25776 94 0 0 25 0 1 0 1846805931 54702080 13165 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 13355 13165 145 145 0 13210 0
[pid=19542] vsize: 53420
Current children cumulated CPU time (s) 258.7
Current children cumulated vsize (Kb) 55544

[startup+270.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 13744 0 0 0 26768 98 0 0 25 0 1 0 1846805931 56868864 13693 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 13884 13693 145 145 0 13739 0
[pid=19542] vsize: 55536
Current children cumulated CPU time (s) 268.66
Current children cumulated vsize (Kb) 57660

[startup+280.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 14268 0 0 0 27758 102 0 0 25 0 1 0 1846805931 58998784 14217 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 14404 14217 145 145 0 14259 0
[pid=19542] vsize: 57616
Current children cumulated CPU time (s) 278.6
Current children cumulated vsize (Kb) 59740

[startup+290.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 14693 0 0 0 28753 104 0 0 25 0 1 0 1846805931 60747776 14642 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 14831 14642 145 145 0 14686 0
[pid=19542] vsize: 59324
Current children cumulated CPU time (s) 288.57
Current children cumulated vsize (Kb) 61448

[startup+300.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 15105 0 0 0 29747 107 0 0 25 0 1 0 1846805931 62443520 15054 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 15245 15054 145 145 0 15100 0
[pid=19542] vsize: 60980
Current children cumulated CPU time (s) 298.54
Current children cumulated vsize (Kb) 63104

[startup+310.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) T 19538 19538 4419 0 -1 0 15570 0 0 0 30740 110 0 0 25 0 1 0 1846805931 64331776 15519 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/19542/statm): 15706 15519 145 145 0 15561 0
[pid=19542] vsize: 62824
Current children cumulated CPU time (s) 308.5
Current children cumulated vsize (Kb) 64948

[startup+320.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 16074 0 0 0 31731 114 0 0 25 0 1 0 1846805931 66420736 16023 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 16216 16023 145 145 0 16071 0
[pid=19542] vsize: 64864
Current children cumulated CPU time (s) 318.45
Current children cumulated vsize (Kb) 66988

[startup+330.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 16473 0 0 0 32725 116 0 0 25 0 1 0 1846805931 68157440 16422 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 16640 16422 145 145 0 16495 0
[pid=19542] vsize: 66560
Current children cumulated CPU time (s) 328.41
Current children cumulated vsize (Kb) 68684

[startup+340.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 16990 0 0 0 33716 120 0 0 25 0 1 0 1846805931 70307840 16939 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 17165 16939 145 145 0 17020 0
[pid=19542] vsize: 68660
Current children cumulated CPU time (s) 338.36
Current children cumulated vsize (Kb) 70784

[startup+350.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 17542 0 0 0 34707 124 0 0 25 0 1 0 1846805931 72560640 17491 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 17715 17491 145 145 0 17570 0
[pid=19542] vsize: 70860
Current children cumulated CPU time (s) 348.31
Current children cumulated vsize (Kb) 72984

[startup+360.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18042 0 0 0 35699 127 0 0 25 0 1 0 1846805931 74608640 17991 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 18215 17991 145 145 0 18070 0
[pid=19542] vsize: 72860
Current children cumulated CPU time (s) 358.26
Current children cumulated vsize (Kb) 74984

[startup+370.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18451 0 0 0 36692 130 0 0 25 0 1 0 1846805931 76300288 18400 4294967295 134512640 135094434 3221224432 3221223024 134556937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 18628 18400 145 145 0 18483 0
[pid=19542] vsize: 74512
Current children cumulated CPU time (s) 368.22
Current children cumulated vsize (Kb) 76636

[startup+380.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18610 0 0 0 37690 131 0 0 25 0 1 0 1846805931 76951552 18559 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 18787 18559 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 378.21
Current children cumulated vsize (Kb) 77272

[startup+390.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18610 0 0 0 38689 132 0 0 25 0 1 0 1846805931 76951552 18559 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 18787 18559 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 388.21
Current children cumulated vsize (Kb) 77272

[startup+400.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18610 0 0 0 39689 133 0 0 25 0 1 0 1846805931 76951552 18559 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 18787 18559 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 398.22
Current children cumulated vsize (Kb) 77272

[startup+410.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18610 0 0 0 40689 133 0 0 25 0 1 0 1846805931 76951552 18559 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18559 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 408.22
Current children cumulated vsize (Kb) 77272

[startup+420.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18610 0 0 0 41689 133 0 0 25 0 1 0 1846805931 76951552 18559 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18559 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 418.22
Current children cumulated vsize (Kb) 77272

[startup+430.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18610 0 0 0 42689 133 0 0 25 0 1 0 1846805931 76951552 18559 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18559 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 428.22
Current children cumulated vsize (Kb) 77272

[startup+440.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18610 0 0 0 43689 133 0 0 25 0 1 0 1846805931 76951552 18559 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18559 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 438.22
Current children cumulated vsize (Kb) 77272

[startup+450.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18610 0 0 0 44690 133 0 0 25 0 1 0 1846805931 76951552 18559 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18559 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 448.23
Current children cumulated vsize (Kb) 77272

[startup+460.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 45690 133 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 458.23
Current children cumulated vsize (Kb) 77272

[startup+470.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 46690 133 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 468.23
Current children cumulated vsize (Kb) 77272

[startup+480.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 47690 133 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 478.23
Current children cumulated vsize (Kb) 77272

[startup+490.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 48690 133 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 488.23
Current children cumulated vsize (Kb) 77272

[startup+500.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 49690 133 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223088 134557792 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 498.23
Current children cumulated vsize (Kb) 77272

[startup+510.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 50690 133 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 508.23
Current children cumulated vsize (Kb) 77272

[startup+520.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 51691 133 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 518.24
Current children cumulated vsize (Kb) 77272

[startup+530.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 52691 133 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223120 134554717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 528.24
Current children cumulated vsize (Kb) 77272

[startup+540.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 53691 133 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 538.24
Current children cumulated vsize (Kb) 77272

[startup+550.04 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 54691 133 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 548.24
Current children cumulated vsize (Kb) 77272

[startup+560.04 s]
Raw data (loadavg): 1.07 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 55690 134 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 558.24
Current children cumulated vsize (Kb) 77272

[startup+570.041 s]
Raw data (loadavg): 1.06 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 56690 134 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223056 134562108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 568.24
Current children cumulated vsize (Kb) 77272

[startup+580.042 s]
Raw data (loadavg): 1.05 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 57691 134 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223024 134556815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 578.25
Current children cumulated vsize (Kb) 77272

[startup+590.042 s]
Raw data (loadavg): 1.04 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 58691 134 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 588.25
Current children cumulated vsize (Kb) 77272

[startup+600.043 s]
Raw data (loadavg): 1.04 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 59691 134 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 598.25
Current children cumulated vsize (Kb) 77272

[startup+610.043 s]
Raw data (loadavg): 1.03 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 60691 134 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 608.25
Current children cumulated vsize (Kb) 77272

[startup+620.044 s]
Raw data (loadavg): 1.03 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 61691 134 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223024 134557393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 618.25
Current children cumulated vsize (Kb) 77272

[startup+630.045 s]
Raw data (loadavg): 1.02 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 62691 134 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 628.25
Current children cumulated vsize (Kb) 77272

[startup+640.044 s]
Raw data (loadavg): 1.02 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 63692 134 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 638.26
Current children cumulated vsize (Kb) 77272

[startup+650.046 s]
Raw data (loadavg): 1.01 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 64692 134 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 648.26
Current children cumulated vsize (Kb) 77272

[startup+660.047 s]
Raw data (loadavg): 1.01 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 65692 134 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 658.26
Current children cumulated vsize (Kb) 77272

[startup+670.047 s]
Raw data (loadavg): 1.01 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 66692 134 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 668.26
Current children cumulated vsize (Kb) 77272

[startup+680.048 s]
Raw data (loadavg): 1.01 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 67692 135 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 678.27
Current children cumulated vsize (Kb) 77272

[startup+690.048 s]
Raw data (loadavg): 1.01 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 68692 135 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 688.27
Current children cumulated vsize (Kb) 77272

[startup+700.049 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 69693 135 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 698.28
Current children cumulated vsize (Kb) 77272

[startup+710.049 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 70693 135 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 708.28
Current children cumulated vsize (Kb) 77272

[startup+720.05 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 71693 135 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223088 134558366 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 718.28
Current children cumulated vsize (Kb) 77272

[startup+730.051 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 72693 135 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 728.28
Current children cumulated vsize (Kb) 77272

[startup+740.051 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 73693 135 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223024 134557213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 738.28
Current children cumulated vsize (Kb) 77272

[startup+750.053 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 74693 135 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223024 134557275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 748.28
Current children cumulated vsize (Kb) 77272

[startup+760.053 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 75693 135 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 758.28
Current children cumulated vsize (Kb) 77272

[startup+770.054 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 76693 135 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 768.28
Current children cumulated vsize (Kb) 77272

[startup+780.055 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 77693 135 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223024 134557357 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 778.28
Current children cumulated vsize (Kb) 77272

[startup+790.054 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 78694 135 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 788.29
Current children cumulated vsize (Kb) 77272

[startup+800.055 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 79694 135 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223056 134557705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 798.29
Current children cumulated vsize (Kb) 77272

[startup+810.056 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18611 0 0 0 80694 135 0 0 25 0 1 0 1846805931 76951552 18560 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18560 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 808.29
Current children cumulated vsize (Kb) 77272

[startup+820.057 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18613 0 0 0 81694 135 0 0 25 0 1 0 1846805931 76951552 18562 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18562 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 818.29
Current children cumulated vsize (Kb) 77272

[startup+830.059 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18615 0 0 0 82695 135 0 0 25 0 1 0 1846805931 76951552 18564 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18564 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 828.3
Current children cumulated vsize (Kb) 77272

[startup+840.059 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18616 0 0 0 83695 135 0 0 25 0 1 0 1846805931 76951552 18565 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18565 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 838.3
Current children cumulated vsize (Kb) 77272

[startup+850.06 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18616 0 0 0 84695 135 0 0 25 0 1 0 1846805931 76951552 18565 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18565 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 848.3
Current children cumulated vsize (Kb) 77272

[startup+860.061 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18616 0 0 0 85695 136 0 0 25 0 1 0 1846805931 76951552 18565 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18565 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 858.31
Current children cumulated vsize (Kb) 77272

[startup+870.061 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18616 0 0 0 86695 136 0 0 25 0 1 0 1846805931 76951552 18565 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18565 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 868.31
Current children cumulated vsize (Kb) 77272

[startup+880.062 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18616 0 0 0 87696 136 0 0 25 0 1 0 1846805931 76951552 18565 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18565 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 878.32
Current children cumulated vsize (Kb) 77272

[startup+890.062 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18616 0 0 0 88696 136 0 0 25 0 1 0 1846805931 76951552 18565 4294967295 134512640 135094434 3221224432 3221223024 134557375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18565 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 888.32
Current children cumulated vsize (Kb) 77272

[startup+900.063 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18616 0 0 0 89696 136 0 0 25 0 1 0 1846805931 76951552 18565 4294967295 134512640 135094434 3221224432 3221223024 134557269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18565 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 898.32
Current children cumulated vsize (Kb) 77272

[startup+910.064 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18616 0 0 0 90696 136 0 0 25 0 1 0 1846805931 76951552 18565 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 18787 18565 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 908.32
Current children cumulated vsize (Kb) 77272

[startup+920.065 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18616 0 0 0 91696 136 0 0 25 0 1 0 1846805931 76951552 18565 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18565 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 918.32
Current children cumulated vsize (Kb) 77272

[startup+930.066 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18616 0 0 0 92696 136 0 0 25 0 1 0 1846805931 76951552 18565 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18565 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 928.32
Current children cumulated vsize (Kb) 77272

[startup+940.065 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18616 0 0 0 93696 136 0 0 25 0 1 0 1846805931 76951552 18565 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18565 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 938.32
Current children cumulated vsize (Kb) 77272

[startup+950.066 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18616 0 0 0 94696 136 0 0 25 0 1 0 1846805931 76951552 18565 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18565 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 948.32
Current children cumulated vsize (Kb) 77272

[startup+960.067 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18616 0 0 0 95696 136 0 0 25 0 1 0 1846805931 76951552 18565 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18565 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 958.32
Current children cumulated vsize (Kb) 77272

[startup+970.067 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18616 0 0 0 96697 136 0 0 25 0 1 0 1846805931 76951552 18565 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18565 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 968.33
Current children cumulated vsize (Kb) 77272

[startup+980.068 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18616 0 0 0 97697 136 0 0 25 0 1 0 1846805931 76951552 18565 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18565 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 978.33
Current children cumulated vsize (Kb) 77272

[startup+990.068 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18616 0 0 0 98697 136 0 0 25 0 1 0 1846805931 76951552 18565 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18565 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 988.33
Current children cumulated vsize (Kb) 77272

[startup+1000.07 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18616 0 0 0 99697 136 0 0 25 0 1 0 1846805931 76951552 18565 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18565 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 998.33
Current children cumulated vsize (Kb) 77272

[startup+1010.07 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18616 0 0 0 100698 136 0 0 25 0 1 0 1846805931 76951552 18565 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18565 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 1008.34
Current children cumulated vsize (Kb) 77272

[startup+1020.07 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18616 0 0 0 101698 137 0 0 25 0 1 0 1846805931 76951552 18565 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18565 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 1018.35
Current children cumulated vsize (Kb) 77272

[startup+1030.07 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18616 0 0 0 102698 137 0 0 25 0 1 0 1846805931 76951552 18565 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18565 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 1028.35
Current children cumulated vsize (Kb) 77272

[startup+1040.07 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18617 0 0 0 103698 137 0 0 25 0 1 0 1846805931 76951552 18566 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18566 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 1038.35
Current children cumulated vsize (Kb) 77272

[startup+1050.07 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18619 0 0 0 104698 137 0 0 25 0 1 0 1846805931 76951552 18568 4294967295 134512640 135094434 3221224432 3221223104 134555835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18568 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 1048.35
Current children cumulated vsize (Kb) 77272

[startup+1060.07 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18620 0 0 0 105698 137 0 0 25 0 1 0 1846805931 76951552 18569 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18787 18569 145 145 0 18642 0
[pid=19542] vsize: 75148
Current children cumulated CPU time (s) 1058.35
Current children cumulated vsize (Kb) 77272

[startup+1070.07 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 18747 0 0 0 106697 137 0 0 25 0 1 0 1846805931 77492224 18696 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 18919 18696 145 145 0 18774 0
[pid=19542] vsize: 75676
Current children cumulated CPU time (s) 1068.34
Current children cumulated vsize (Kb) 77800

[startup+1080.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 19258 0 0 0 107688 141 0 0 25 0 1 0 1846805931 79581184 19207 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 19429 19207 145 145 0 19284 0
[pid=19542] vsize: 77716
Current children cumulated CPU time (s) 1078.29
Current children cumulated vsize (Kb) 79840

[startup+1090.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 19567 0 0 0 108683 145 0 0 25 0 1 0 1846805931 81104896 19516 4294967295 134512640 135094434 3221224432 3221223024 134557143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 19801 19516 145 145 0 19656 0
[pid=19542] vsize: 79204
Current children cumulated CPU time (s) 1088.28
Current children cumulated vsize (Kb) 81328

[startup+1100.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 19567 0 0 0 109683 145 0 0 25 0 1 0 1846805931 81104896 19516 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 19801 19516 145 145 0 19656 0
[pid=19542] vsize: 79204
Current children cumulated CPU time (s) 1098.28
Current children cumulated vsize (Kb) 81328

[startup+1110.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 19567 0 0 0 110682 146 0 0 25 0 1 0 1846805931 81104896 19516 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 19801 19516 145 145 0 19656 0
[pid=19542] vsize: 79204
Current children cumulated CPU time (s) 1108.28
Current children cumulated vsize (Kb) 81328

[startup+1120.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 19567 0 0 0 111682 146 0 0 25 0 1 0 1846805931 81104896 19516 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 19801 19516 145 145 0 19656 0
[pid=19542] vsize: 79204
Current children cumulated CPU time (s) 1118.28
Current children cumulated vsize (Kb) 81328

[startup+1130.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 19567 0 0 0 112682 146 0 0 25 0 1 0 1846805931 81104896 19516 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 19801 19516 145 145 0 19656 0
[pid=19542] vsize: 79204
Current children cumulated CPU time (s) 1128.28
Current children cumulated vsize (Kb) 81328

[startup+1140.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 19567 0 0 0 113681 147 0 0 25 0 1 0 1846805931 81104896 19516 4294967295 134512640 135094434 3221224432 3221223104 134555850 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 19801 19516 145 145 0 19656 0
[pid=19542] vsize: 79204
Current children cumulated CPU time (s) 1138.28
Current children cumulated vsize (Kb) 81328

[startup+1150.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 19567 0 0 0 114681 148 0 0 25 0 1 0 1846805931 81104896 19516 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 19801 19516 145 145 0 19656 0
[pid=19542] vsize: 79204
Current children cumulated CPU time (s) 1148.29
Current children cumulated vsize (Kb) 81328

[startup+1160.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 19567 0 0 0 115680 148 0 0 25 0 1 0 1846805931 81104896 19516 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19542/statm): 19801 19516 145 145 0 19656 0
[pid=19542] vsize: 79204
Current children cumulated CPU time (s) 1158.28
Current children cumulated vsize (Kb) 81328

[startup+1170.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 19567 0 0 0 116680 148 0 0 25 0 1 0 1846805931 81104896 19516 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 19801 19516 145 145 0 19656 0
[pid=19542] vsize: 79204
Current children cumulated CPU time (s) 1168.28
Current children cumulated vsize (Kb) 81328

[startup+1180.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 19567 0 0 0 117680 148 0 0 25 0 1 0 1846805931 81104896 19516 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 19801 19516 145 145 0 19656 0
[pid=19542] vsize: 79204
Current children cumulated CPU time (s) 1178.28
Current children cumulated vsize (Kb) 81328

[startup+1190.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 19569 0 0 0 118680 149 0 0 25 0 1 0 1846805931 81104896 19518 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 19801 19518 145 145 0 19656 0
[pid=19542] vsize: 79204
Current children cumulated CPU time (s) 1188.29
Current children cumulated vsize (Kb) 81328

[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 19570 0 0 0 119681 149 0 0 25 0 1 0 1846805931 81104896 19519 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 19801 19519 145 145 0 19656 0
[pid=19542] vsize: 79204
Current children cumulated CPU time (s) 1198.3
Current children cumulated vsize (Kb) 81328

[startup+1210.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 19570 0 0 0 120681 149 0 0 25 0 1 0 1846805931 81104896 19519 4294967295 134512640 135094434 3221224432 3221223024 134557391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 19801 19519 145 145 0 19656 0
[pid=19542] vsize: 79204
Current children cumulated CPU time (s) 1208.3
Current children cumulated vsize (Kb) 81328



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 19542
Raw data (/proc/19538/stat): 19538 (minisat+_script) S 19537 19538 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846805926 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19538/statm): 531 226 485 147 0 384 0
[pid=19538] vsize: 2124
Raw data (/proc/19542/stat): 19542 (minisat+_64-bit) R 19538 19538 4419 0 -1 0 19570 0 0 0 120681 149 0 0 25 0 1 0 1846805931 81104896 19519 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19542/statm): 19801 19519 145 145 0 19656 0
[pid=19542] vsize: 79204
Current children cumulated CPU time (s) 1208.3
Current children cumulated vsize (Kb) 81328

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

Child status: 10
Real time (s): 1210.13
CPU time (s): 1208.34
CPU user time (s): 1206.82
CPU system time (s): 1.52777
CPU usage (%): 99.8524
Max. virtual memory (cumulated for all children) (Kb): 81328

Verifier Data

ERROR: no interpretation found !