Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-mod013.opb
MD5SUMb964292d4197638ce79b3f213e8fe89b
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 4696832
Optimality of the best value was proved NO
Number of terms in the objective function 1008
Biggest coefficient in the objective function 366477312
Number of bits for the biggest coefficient in the objective function 29
Sum of the numbers in the objective function 12643636975
Number of bits of the sum of numbers in the objective function 34
Biggest number in a constraint 366477312
Number of bits of the biggest number in a constraint 29
Biggest sum of numbers in a constraint 12643636975
Number of bits of the biggest sum of numbers34
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.06
Number of variables1008
Total number of constraints110
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)48
Number of constraints which are nor clauses,nor cardinality constraints62
Minimum length of a constraint1
Maximum length of a constraint160

Trace number 6119

Launcher Data

LAUNCH ON wulflinc31 THE 2005-09-20 03:29:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3281 boxname=wulflinc31 idbench=937 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b964292d4197638ce79b3f213e8fe89b  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-mod013.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-mod013.opb
IDLAUNCH: 3281
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        926340 kB
Buffers:          3576 kB
Cached:          77100 kB
SwapCached:        992 kB
Active:          11608 kB
Inactive:        71648 kB
HighTotal:      131008 kB
HighFree:        50288 kB
LowTotal:       903652 kB
LowFree:        876052 kB
SwapTotal:     2097892 kB
SwapFree:      2096216 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5416 kB
Slab:            19372 kB
Committed_AS:    64376 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:50:01 (client local time) WITH STATUS 10 IN 1209.01 SECONDS
stats: 3281 7 1209.01 10

Solver Data

c Parsing PB file...
c Converting 76 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############
c   -- Clauses(.)/Splits(s): (none)
c ---[  74]---> Sorter-cost:  970     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  72]---> Sorter-cost:  970     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  70]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[  68]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[  66]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[  64]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[  63]---> BDD-cost:   19
c ---[  62]---> BDD-cost:   16
c ---[  61]---> BDD-cost:   17
c ---[  60]---> BDD-cost:   15
c ---[  58]---> Sorter-cost: 1495     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> BDD-cost:   15
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   19
c ---[  52]---> BDD-cost:   16
c ---[  51]---> BDD-cost:   17
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   14
c ---[  46]---> Sorter-cost: 1495     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> BDD-cost:   14
c ---[  44]---> BDD-cost:   13
c ---[  43]---> BDD-cost:   16
c ---[  42]---> BDD-cost:   16
c ---[  41]---> BDD-cost:   17
c ---[  40]---> BDD-cost:   15
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   14
c ---[  37]---> BDD-cost:   14
c ---[  36]---> BDD-cost:   13
c ---[  34]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   15
c ---[  30]---> BDD-cost:   15
c ---[  29]---> BDD-cost:   15
c ---[  28]---> BDD-cost:   14
c ---[  27]---> BDD-cost:   14
c ---[  26]---> BDD-cost:   13
c ---[  25]---> BDD-cost:   14
c ---[  24]---> BDD-cost:   14
c ---[  22]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   14
c ---[  17]---> BDD-cost:   14
c ---[  16]---> BDD-cost:   13
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   13
c ---[  12]---> BDD-cost:   13
c ---[  10]---> Sorter-cost: 1391     Base: 2 2 2 2 2 2 2 2 2
c ---[   9]---> BDD-cost:   13
c ---[   8]---> BDD-cost:   13
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   13
c ---[   4]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  955     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  970     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   39875    94300 |   13291       0        0     nan |  0.000 % |
c |       100 |   39796    94121 |   14620      97      326     3.4 |  8.098 % |
c |       250 |   39748    94013 |   16082     242     1150     4.8 |  8.194 % |
c |       475 |   39748    94013 |   17690     467     2209     4.7 |  8.194 % |
c ==============================================================================
c Found solution: 12142577
c ---[   0]---> Adder-cost: 4334   maxlim: 18821886   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       655 |   70015   202266 |   23338     647     2925     4.5 |  8.194 % |
c ==============================================================================
c Found solution: 12120899
c ---[   0]---> Adder-cost: 0   maxlim: 18843564   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       686 |   70030   202450 |   23343     678     3514     5.2 |  8.194 % |
c |       786 |   70030   202450 |   25677     778     4163     5.4 |  6.449 % |
c |       936 |   69944   202255 |   28245     919     4949     5.4 |  6.591 % |
c ==============================================================================
c Found solution: 11843450
c ---[   0]---> Adder-cost: 0   maxlim: 19121013   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1079 |   69965   202465 |   23321    1062     6637     6.2 |  6.591 % |
c |      1179 |   69965   202465 |   25653    1162     7103     6.1 |  6.649 % |
c |      1329 |   69965   202465 |   28218    1312     8775     6.7 |  6.649 % |
c |      1554 |   69965   202465 |   31040    1537    12933     8.4 |  6.649 % |
c |      1891 |   69965   202465 |   34144    1874    45220    24.1 |  6.649 % |
c |      2397 |   69915   202352 |   37558    2378    49651    20.9 |  6.728 % |
c |      3156 |   69910   202341 |   41314    3136   238956    76.2 |  6.739 % |
c ==============================================================================
c Found solution: 10725961
c ---[   0]---> Adder-cost: 0   maxlim: 20238502   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3758 |   69749   202103 |   23249    3730   255374    68.5 |  6.739 % |
c |      3858 |   69749   202103 |   25573    3830   255999    66.8 |  7.066 % |
c |      4008 |   69749   202103 |   28131    3980   257142    64.6 |  7.066 % |
c |      4233 |   69749   202103 |   30944    4205   260182    61.9 |  7.066 % |
c |      4571 |   69728   202056 |   34038    4541   270662    59.6 |  7.097 % |
c ==============================================================================
c Found solution: 10473014
c ---[   0]---> Adder-cost: 0   maxlim: 20491449   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4991 |   69712   202162 |   23237    4959   276994    55.9 |  7.097 % |
c |      5091 |   69712   202162 |   25560    5059   279009    55.2 |  7.203 % |
c ==============================================================================
c Found solution: 10204766
c ---[   0]---> Adder-cost: 0   maxlim: 20759697   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5176 |   69724   202276 |   23241    5144   280381    54.5 |  7.203 % |
c |      5276 |   69724   202276 |   25565    5244   281775    53.7 |  7.235 % |
c |      5426 |   69724   202276 |   28121    5394   284725    52.8 |  7.235 % |
c |      5651 |   69724   202276 |   30933    5619   289356    51.5 |  7.235 % |
c |      5989 |   69631   202064 |   34027    5947   319026    53.6 |  7.377 % |
c ==============================================================================
c Found solution: 9546584
c ---[   0]---> Adder-cost: 0   maxlim: 21417879   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6073 |   69652   202252 |   23217    6031   319676    53.0 |  7.377 % |
c |      6173 |   69652   202252 |   25538    6131   354707    57.9 |  7.433 % |
c |      6323 |   69620   202180 |   28092    6279   356329    56.7 |  7.486 % |
c |      6549 |   69620   202180 |   30901    6505   375138    57.7 |  7.486 % |
c ==============================================================================
c Found solution: 9188258
c ---[   0]---> Adder-cost: 0   maxlim: 21776205   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6720 |   69627   202318 |   23209    6674   377204    56.5 |  7.486 % |
c |      6821 |   69627   202318 |   25529    6775   380588    56.2 |  7.537 % |
c |      6971 |   69601   202257 |   28082    6924   384546    55.5 |  7.579 % |
c |      7196 |   69601   202257 |   30891    7149   390112    54.6 |  7.579 % |
c |      7535 |   69542   202125 |   33980    7486   397989    53.2 |  7.668 % |
c |      8042 |   69542   202125 |   37378    7993   408564    51.1 |  7.668 % |
c ==============================================================================
c Found solution: 8803184
c ---[   0]---> Adder-cost: 0   maxlim: 22161279   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8572 |   69546   202205 |   23182    8522   441774    51.8 |  7.668 % |
c |      8672 |   69546   202205 |   25500    8622   445203    51.6 |  7.710 % |
c |      8822 |   69413   201899 |   28050    8761   464523    53.0 |  7.930 % |
c |      9047 |   69413   201899 |   30855    8986   473601    52.7 |  7.930 % |
c |      9384 |   69392   201851 |   33940    9322   502835    53.9 |  7.956 % |
c |      9890 |   69392   201851 |   37334    9828   519206    52.8 |  7.956 % |
c |     10651 |   69392   201851 |   41068   10589   548183    51.8 |  7.956 % |
c ==============================================================================
c Found solution: 7726726
c ---[   0]---> Adder-cost: 0   maxlim: 23237737   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11787 |   69406   201995 |   23135   11725   673129    57.4 |  7.956 % |
c |     11887 |   69406   201995 |   25448   11825   673993    57.0 |  7.998 % |
c |     12037 |   69406   201995 |   27993   11975   682129    57.0 |  7.998 % |
c |     12263 |   69406   201995 |   30792   12201   706729    57.9 |  7.998 % |
c |     12600 |   69406   201995 |   33871   12538   717322    57.2 |  7.998 % |
c |     13107 |   69406   201995 |   37259   13045   774505    59.4 |  7.998 % |
c |     13867 |   69406   201995 |   40985   13805   935697    67.8 |  7.998 % |
c |     15007 |   69330   201822 |   45083   14923   998700    66.9 |  8.113 % |
c ==============================================================================
c Found solution: 6432738
c ---[   0]---> Adder-cost: 0   maxlim: 24531725   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15677 |   69338   201958 |   23112   15592  1024794    65.7 |  8.113 % |
c |     15777 |   69338   201958 |   25423   15692  1029024    65.6 |  8.173 % |
c |     15929 |   69338   201958 |   27965   15844  1089757    68.8 |  8.173 % |
c |     16155 |   69338   201958 |   30762   16070  1096632    68.2 |  8.173 % |
c |     16493 |   69338   201958 |   33838   16408  1113978    67.9 |  8.173 % |
c |     17001 |   69338   201958 |   37222   16916  1132920    67.0 |  8.173 % |
c |     17760 |   69338   201958 |   40944   17675  1365844    77.3 |  8.173 % |
c |     18901 |   69338   201958 |   45038   18816  1413462    75.1 |  8.173 % |
c ==============================================================================
c Found solution: 5957249
c ---[   0]---> Adder-cost: 0   maxlim: 25007214   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18930 |   69360   202165 |   23120   18845  1415342    75.1 |  8.173 % |
c |     19030 |   69360   202165 |   25432   18945  1436986    75.9 |  8.226 % |
c |     19182 |   69298   202022 |   27975   19083  1455480    76.3 |  8.320 % |
c |     19408 |   69298   202022 |   30772   19309  1468519    76.1 |  8.320 % |
c |     19747 |   69298   202022 |   33849   19648  1500516    76.4 |  8.320 % |
c |     20256 |   69204   201808 |   37234   20143  1541773    76.5 |  8.456 % |
c |     21015 |   69204   201808 |   40958   20902  1559530    74.6 |  8.456 % |
c |     22156 |   69204   201808 |   45054   22043  1686247    76.5 |  8.456 % |
c |     23866 |   69204   201808 |   49559   23753  1756872    74.0 |  8.456 % |
c |     26428 |   69204   201808 |   54515   26315  2280025    86.6 |  8.456 % |
c ==============================================================================
c Found solution: 5207530
c ---[   0]---> Adder-cost: 0   maxlim: 25756933   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27818 |   69049   199997 |   23016   27506  2341612    85.1 |  8.456 % |
c |     27920 |   69049   199997 |   25317   13855  1003478    72.4 |  8.551 % |
c |     28070 |   69049   199997 |   27849   14005  1005030    71.8 |  8.551 % |
c |     28298 |   69039   199974 |   30634   14232  1008191    70.8 |  8.566 % |
c |     28635 |   69003   199890 |   33697   14568  1049136    72.0 |  8.629 % |
c |     29141 |   69003   199890 |   37067   15074  1152404    76.4 |  8.629 % |
c |     29900 |   68962   199800 |   40774   15828  1192767    75.4 |  8.686 % |
c |     31043 |   68962   199800 |   44851   16971  1264285    74.5 |  8.686 % |
c |     32753 |   68962   199800 |   49336   18681  1419491    76.0 |  8.686 % |
c |     35315 |   68962   199800 |   54270   21243  1554273    73.2 |  8.686 % |
c |     39159 |   68962   199800 |   59697   25087  1756711    70.0 |  8.686 % |
c |     44925 |   68949   199771 |   65667   30851  2243946    72.7 |  8.702 % |
c |     53576 |   68949   199771 |   72234   39502  3007725    76.1 |  8.702 % |
c |     66553 |   68946   199765 |   79457   52478  4179697    79.6 |  8.707 % |
c |     86014 |   68922   199710 |   87403   71937  5584587    77.6 |  8.739 % |
c |    115206 |   68850   199546 |   96143   25886  1868537    72.2 |  8.848 % |
c |    158995 |   68840   199524 |  105757   69674  5540014    79.5 |  8.864 % |
c |    224679 |   68840   199524 |  116333   45502  3015422    66.3 |  8.864 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1_0x2e__bit_7 -C1_0x2e__bit_6 C1_0x2e__bit_5 -C1_0x2e__bit_4 -C1_0x2e__bit_3 -C1_0x2e__bit_2 -C1_0x2e__bit_1 C1_0x2e__bit0 C1_0x2e__bit1 C1_0x2e__bit2 C1_0x2e__bit3 -C1_0x2e__bit4 -C1_0x2e__bit5 -C1_0x2e__bit6 -C1_0x2e__bit7 -C1_0x2e__bit8 -C1_0x2e__bit9 -C1_0x2e__bit10 -C1_0x2e__bit11 -C1_0x2e__bit12 -C2_0x2e__bit_7 -C2_0x2e__bit_6 -C2_0x2e__bit_5 -C2_0x2e__bit_4 -C2_0x2e__bit_3 -C2_0x2e__bit_2 -C2_0x2e__bit_1 -C2_0x2e__bit0 -C2_0x2e__bit1 -C2_0x2e__bit2 -C2_0x2e__bit3 -C2_0x2e__bit4 -C2_0x2e__bit5 -C2_0x2e__bit6 -C2_0x2e__bit7 -C2_0x2e__bit8 -C2_0x2e__bit9 -C2_0x2e__bit10 -C2_0x2e__bit11 -C2_0x2e__bit12 -C3_0x2e__bit_7 -C3_0x2e__bit_6 C3_0x2e__bit_5 C3_0x2e__bit_4 -C3_0x2e__bit_3 -C3_0x2e__bit_2 -C3_0x2e__bit_1 -C3_0x2e__bit0 C3_0x2e__bit1 C3_0x2e__bit2 -C3_0x2e__bit3 C3_0x2e__bit4 -C3_0x2e__bit5 -C3_0x2e__bit6 -C3_0x2e__bit7 -C3_0x2e__bit8 -C3_0x2e__bit9 -C3_0x2e__bit10 -C3_0x2e__bit11 -C3_0x2e__bit12 -C4_0x2e__bit_7 -C4_0x2e__bit_6 -C4_0x2e__bit_5 -C4_0x2e__bit_4 -C4_0x2e__bit_3 -C4_0x2e__bit_2 -C4_0x2e__bit_1 -C4_0x2e__bit0 -C4_0x2e__bit1 -C4_0x2e__bit2 -C4_0x2e__bit3 -C4_0x2e__bit4 -C4_0x2e__bit5 -C4_0x2e__bit6 -C4_0x2e__bit7 -C4_0x2e__bit8 -C4_0x2e__bit9 -C4_0x2e__bit10 -C4_0x2e__bit11 -C4_0x2e__bit12 -C5_0x2e__bit_7 -C5_0x2e__bit_6 -C5_0x2e__bit_5 -C5_0x2e__bit_4 C5_0x2e__bit_3 C5_0x2e__bit_2 C5_0x2e__bit_1 C5_0x2e__bit0 C5_0x2e__bit1 C5_0x2e__bit2 -C5_0x2e__bit3 -C5_0x2e__bit4 -C5_0x2e__bit5 -C5_0x2e__bit6 -C5_0x2e__bit7 -C5_0x2e__bit8 -C5_0x2e__bit9 -C5_0x2e__bit10 -C5_0x2e__bit11 -C5_0x2e__bit12 -C6_0x2e__bit_7 -C6_0x2e__bit_6 -C6_0x2e__bit_5 -C6_0x2e__bit_4 -C6_0x2e__bit_3 -C6_0x2e__bit_2 -C6_0x2e__bit_1 -C6_0x2e__bit0 -C6_0x2e__bit1 -C6_0x2e__bit2 -C6_0x2e__bit3 -C6_0x2e__bit4 -C6_0x2e__bit5 -C6_0x2e__bit6 -C6_0x2e__bit7 -C6_0x2e__bit8 -C6_0x2e__bit9 -C6_0x2e__bit10 -C6_0x2e__bit11 -C6_0x2e__bit12 -C7_0x2e__bit_7 -C7_0x2e__bit_6 -C7_0x2e__bit_5 -C7_0x2e__bit_4 -C7_0x2e__bit_3 -C7_0x2e__bit_2 -C7_0x2e__bit_1 -C7_0x2e__bit0 -C7_0x2e__bit1 -C7_0x2e__bit2 -C7_0x2e__bit3 -C7_0x2e__bit4 -C7_0x2e__bit5 -C7_0x2e__bit6 -C7_0x2e__bit7 -C7_0x2e__bit8 -C7_0x2e__bit9 -C7_0x2e__bit10 -C7_0x2e__bit11 -C7_0x2e__bit12 -C8_0x2e__bit_7 -C8_0x2e__bit_6 -C8_0x2e__bit_5 -C8_0x2e__bit_4 -C8_0x2e__bit_3 -C8_0x2e__bit_2 -C8_0x2e__bit_1 -C8_0x2e__bit0 -C8_0x2e__bit1 -C8_0x2e__bit2 -C8_0x2e__bit3 -C8_0x2e__bit4 -C8_0x2e__bit5 -C8_0x2e__bit6 -C8_0x2e__bit7 -C8_0x2e__bit8 -C8_0x2e__bit9 -C8_0x2e__bit10 -C8_0x2e__bit11 -C8_0x2e__bit12 -C9_0x2e__bit_7 -C9_0x2e__bit_6 -C9_0x2e__bit_5 -C9_0x2e__bit_4 -C9_0x2e__bit_3 -C9_0x2e__bit_2 -C9_0x2e__bit_1 -C9_0x2e__bit0 -C9_0x2e__bit1 -C9_0x2e__bit2 C9_0x2e__bit3 -C9_0x2e__bit4 -C9_0x2e__bit5 -C9_0x2e__bit6 -C9_0x2e__bit7 -C9_0x2e__bit8 -C9_0x2e__bit9 -C9_0x2e__bit10 -C9_0x2e__bit11 -C9_0x2e__bit12 C10_0x2e__bit_7 -C10_0x2e__bit_6 -C10_0x2e__bit_5 -C10_0x2e__bit_4 -C10_0x2e__bit_3 -C10_0x2e__bit_2 -C10_0x2e__bit_1 -C10_0x2e__bit0 C10_0x2e__bit1 C10_0x2e__bit2 C10_0x2e__bit3 -C10_0x2e__bit4 -C10_0x2e__bit5 -C10_0x2e__bit6 -C10_0x2e__bit7 -C10_0x2e__bit8 -C10_0x2e__bit9 -C10_0x2e__bit10 -C10_0x2e__bit11 -C10_0x2e__bit12 -C11_0x2e__bit_7 -C11_0x2e__bit_6 -C11_0x2e__bit_5 -C11_0x2e__bit_4 -C11_0x2e__bit_3 -C11_0x2e__bit_2 -C11_0x2e__bit_1 -C11_0x2e__bit0 -C11_0x2e__bit1 -C11_0x2e__bit2 -C11_0x2e__bit3 -C11_0x2e__bit4 -C11_0x2e__bit5 -C11_0x2e__bit6 -C11_0x2e__bit7 -C11_0x2e__bit8 -C11_0x2e__bit9 -C11_0x2e__bit10 -C11_0x2e__bit11 -C11_0x2e__bit12 C12_0x2e__bit_7 C12_0x2e__bit_6 C12_0x2e__bit_5 C12_0x2e__bit_4 C12_0x2e__bit_3 C12_0x2e__bit_2 C12_0x2e__bit_1 C12_0x2e__bit0 -C12_0x2e__bit1 -C12_0x2e__bit2 -C12_0x2e__bit3 C12_0x2e__bit4 -C12_0x2e__bit5 -C12_0x2e__bit6 -C12_0x2e__bit7 -C12_0x2e__bit8 -C12_0x2e__bit9 -C12_0x2e__bit10 -C12_0x2e__bit11 -C12_0x2e__bit12 -C13_0x2e__bit_7 -C13_0x2e__bit_6 -C13_0x2e__bit_5 -C13_0x2e__bit_4 -C13_0x2e__bit_3 -C13_0x2e__bit_2 -C13_0x2e__bit_1 -C13_0x2e__bit0 -C13_0x2e__bit1 -C13_0x2e__bit2 -C13_0x2e__bit3 -C13_0x2e__bit4 -C13_0x2e__bit5 -C13_0x2e__bit6 -C13_0x2e__bit7 -C13_0x2e__bit8 -C13_0x2e__bit9 -C13_0x2e__bit10 -C13_0x2e__bit11 -C13_0x2e__bit12 -C14_0x2e__bit_7 -C14_0x2e__bit_6 -C14_0x2e__bit_5 -C14_0x2e__bit_4 -C14_0x2e__bit_3 -C14_0x2e__bit_2 -C14_0x2e__bit_1 -C14_0x2e__bit0 -C14_0x2e__bit1 -C14_0x2e__bit2 -C14_0x2e__bit3 -C14_0x2e__bit4 -C14_0x2e__bit5 -C14_0x2e__bit6 -C14_0x2e__bit7 -C14_0x2e__bit8 -C14_0x2e__bit9 -C14_0x2e__bit10 -C14_0x2e__bit11 -C14_0x2e__bit12 -C15_0x2e__bit_7 -C15_0x2e__bit_6 -C15_0x2e__bit_5 -C15_0x2e__bit_4 -C15_0x2e__bit_3 -C15_0x2e__bit_2 -C15_0x2e__bit_1 -C15_0x2e__bit0 -C15_0x2e__bit1 -C15_0x2e__bit2 -C15_0x2e__bit3 -C15_0x2e__bit4 -C15_0x2e__bit5 -C15_0x2e__bit6 -C15_0x2e__bit7 -C15_0x2e__bit8 -C15_0x2e__bit9 -C15_0x2e__bit10 -C15_0x2e__bit11 -C15_0x2e__bit12 -C16_0x2e__bit_7 -C16_0x2e__bit_6 -C16_0x2e__bit_5 -C16_0x2e__bit_4 -C16_0x2e__bit_3 -C16_0x2e__bit_2 -C16_0x2e__bit_1 -C16_0x2e__bit0 -C16_0x2e__bit1 -C16_0x2e__bit2 -C16_0x2e__bit3 -C16_0x2e__bit4 -C16_0x2e__bit5 -C16_0x2e__bit6 -C16_0x2e__bit7 -C16_0x2e__bit8 -C16_0x2e__bit9 -C16_0x2e__bit10 -C16_0x2e__bit11 -C16_0x2e__bit12 -C17_0x2e__bit_7 -C17_0x2e__bit_6 C17_0x2e__bit_5 -C17_0x2e__bit_4 C17_0x2e__bit_3 -C17_0x2e__bit_2 -C17_0x2e__bit_1 C17_0x2e__bit0 C17_0x2e__bit1 -C17_0x2e__bit2 C17_0x2e__bit3 -C17_0x2e__bit4 -C17_0x2e__bit5 -C17_0x2e__bit6 -C17_0x2e__bit7 -C17_0x2e__bit8 -C17_0x2e__bit9 -C17_0x2e__bit10 -C17_0x2e__bit11 -C17_0x2e__bit12 C18_0x2e__bit_7 C18_0x2e__bit_6 C18_0x2e__bit_5 C18_0x2e__bit_4 C18_0x2e__bit_3 C18_0x2e__bit_2 C18_0x2e__bit_1 C18_0x2e__bit0 C18_0x2e__bit1 C18_0x2e__bit2 C18_0x2e__bit3 -C18_0x2e__bit4 -C18_0x2e__bit5 -C18_0x2e__bit6 -C18_0x2e__bit7 -C18_0x2e__bit8 -C18_0x2e__bit9 -C18_0x2e__bit10 -C18_0x2e__bit11 -C18_0x2e__bit12 C19_0x2e__bit_7 -C19_0x2e__bit_6 C19_0x2e__bit_5 C19_0x2e__bit_4 -C19_0x2e__bit_3 C19_0x2e__bit_2 C19_0x2e__bit_1 -C19_0x2e__bit0 C19_0x2e__bit1 -C19_0x2e__bit2 -C19_0x2e__bit3 -C19_0x2e__bit4 -C19_0x2e__bit5 -C19_0x2e__bit6 -C19_0x2e__bit7 -C19_0x2e__bit8 -C19_0x2e__bit9 -C19_0x2e__bit10 -C19_0x2e__bit11 -C19_0x2e__bit12 -C20_0x2e__bit_7 -C20_0x2e__bit_6 -C20_0x2e__bit_5 -C20_0x2e__bit_4 -C20_0x2e__bit_3 -C20_0x2e__bit_2 -C20_0x2e__bit_1 -C20_0x2e__bit0 -C20_0x2e__bit1 -C20_0x2e__bit2 -C20_0x2e__bit3 -C20_0x2e__bit4 -C20_0x2e__bit5 -C20_0x2e__bit6 -C20_0x2e__bit7 -C20_0x2e__bit8 -C20_0x2e__bit9 -C20_0x2e__bit10 -C20_0x2e__bit11 -C20_0x2e__bit12 -C21_0x2e__bit_7 -C21_0x2e__bit_6 -C21_0x2e__bit_5 -C21_0x2e__bit_4 -C21_0x2e__bit_3 -C21_0x2e__bit_2 -C21_0x2e__bit_1 -C21_0x2e__bit0 -C21_0x2e__bit1 -C21_0x2e__bit2 -C21_0x2e__bit3 -C21_0x2e__bit4 -C21_0x2e__bit5 -C21_0x2e__bit6 -C21_0x2e__bit7 -C21_0x2e__bit8 -C21_0x2e__bit9 -C21_0x2e__bit10 -C21_0x2e__bit11 -C21_0x2e__bit12 -C22_0x2e__bit_7 -C22_0x2e__bit_6 -C22_0x2e__bit_5 -C22_0x2e__bit_4 -C22_0x2e__bit_3 -C22_0x2e__bit_2 -C22_0x2e__bit_1 -C22_0x2e__bit0 -C22_0x2e__bit1 -C22_0x2e__bit2 -C22_0x2e__bit3 -C22_0x2e__bit4 -C22_0x2e__bit5 -C22_0x2e__bit6 -C22_0x2e__bit7 -C22_0x2e__bit8 -C22_0x2e__bit9 -C22_0x2e__bit10 -C22_0x2e__bit11 -C22_0x2e__bit12 -C23_0x2e__bit_7 -C23_0x2e__bit_6 -C23_0x2e__bit_5 -C23_0x2e__bit_4 -C23_0x2e__bit_3 -C23_0x2e__bit_2 -C23_0x2e__bit_1 -C23_0x2e__bit0 -C23_0x2e__bit1 -C23_0x2e__bit2 -C23_0x2e__bit3 -C23_0x2e__bit4 -C23_0x2e__bit5 -C23_0x2e__bit6 -C23_0x2e__bit7 -C23_0x2e__bit8 -C23_0x2e__bit9 -C23_0x2e__bit10 -C23_0x2e__bit11 -C23_0x2e__bit12 -C24_0x2e__bit_7 -C24_0x2e__bit_6 -C24_0x2e__bit_5 -C24_0x2e__bit_4 -C24_0x2e__bit_3 -C24_0x2e__bit_2 -C24_0x2e__bit_1 -C24_0x2e__bit0 -C24_0x2e__bit1 -C24_0x2e__bit2 -C24_0x2e__bit3 -C24_0x2e__bit4 -C24_0x2e__bit5 -C24_0x2e__bit6 -C24_0x2e__bit7 -C24_0x2e__bit8 -C24_0x2e__bit9 -C24_0x2e__bit10 -C24_0x2e__bit11 -C24_0x2e__bit12 -C25_0x2e__bit_7 -C25_0x2e__bit_6 -C25_0x2e__bit_5 -C25_0x2e__bit_4 -C25_0x2e__bit_3 -C25_0x2e__bit_2 -C25_0x2e__bit_1 -C25_0x2e__bit0 -C25_0x2e__bit1 -C25_0x2e__bit2 -C25_0x2e__bit3 -C25_0x2e__bit4 -C25_0x2e__bit5 -C25_0x2e__bit6 -C25_0x2e__bit7 -C25_0x2e__bit8 -C25_0x2e__bit9 -C25_0x2e__bit10 -C25_0x2e__bit11 -C25_0x2e__bit12 -C26_0x2e__bit_7 -C26_0x2e__bit_6 -C26_0x2e__bit_5 -C26_0x2e__bit_4 -C26_0x2e__bit_3 -C26_0x2e__bit_2 -C26_0x2e__bit_1 -C26_0x2e__bit0 -C26_0x2e__bit1 -C26_0x2e__bit2 -C26_0x2e__bit3 -C26_0x2e__bit4 -C26_0x2e__bit5 -C26_0x2e__bit6 -C26_0x2e__bit7 -C26_0x2e__bit8 -C26_0x2e__bit9 -C26_0x2e__bit10 -C26_0x2e__bit11 -C26_0x2e__bit12 -C27_0x2e__bit_7 -C27_0x2e__bit_6 -C27_0x2e__bit_5 -C27_0x2e__bit_4 -C27_0x2e__bit_3 -C27_0x2e__bit_2 -C27_0x2e__bit_1 -C27_0x2e__bit0 -C27_0x2e__bit1 -C27_0x2e__bit2 -C27_0x2e__bit3 -C27_0x2e__bit4 -C27_0x2e__bit5 -C27_0x2e__bit6 -C27_0x2e__bit7 -C27_0x2e__bit8 -C27_0x2e__bit9 -C27_0x2e__bit10 -C27_0x2e__bit11 -C27_0x2e__bit12 -C28_0x2e__bit_7 -C28_0x2e__bit_6 -C28_0x2e__bit_5 -C28_0x2e__bit_4 -C28_0x2e__bit_3 -C28_0x2e__bit_2 -C28_0x2e__bit_1 -C28_0x2e__bit0 -C28_0x2e__bit1 -C28_0x2e__bit2 -C28_0x2e__bit3 -C28_0x2e__bit4 -C28_0x2e__bit5 -C28_0x2e__bit6 -C28_0x2e__bit7 -C28_0x2e__bit8 -C28_0x2e__bit9 -C28_0x2e__bit10 -C28_0x2e__bit11 -C28_0x2e__bit12 -C29_0x2e__bit_7 -C29_0x2e__bit_6 -C29_0x2e__bit_5 -C29_0x2e__bit_4 -C29_0x2e__bit_3 -C29_0x2e__bit_2 -C29_0x2e__bit_1 -C29_0x2e__bit0 -C29_0x2e__bit1 -C29_0x2e__bit2 -C29_0x2e__bit3 -C29_0x2e__bit4 -C29_0x2e__bit5 -C29_0x2e__bit6 -C29_0x2e__bit7 -C29_0x2e__bit8 -C29_0x2e__bit9 -C29_0x2e__bit10 -C29_0x2e__bit11 -C29_0x2e__bit12 -C30_0x2e__bit_7 -C30_0x2e__bit_6 -C30_0x2e__bit_5 -C30_0x2e__bit_4 -C30_0x2e__bit_3 -C30_0x2e__bit_2 -C30_0x2e__bit_1 -C30_0x2e__bit0 C30_0x2e__bit1 -C30_0x2e__bit2 C30_0x2e__bit3 -C30_0x2e__bit4 -C30_0x2e__bit5 -C30_0x2e__bit6 -C30_0x2e__bit7 -C30_0x2e__bit8 -C30_0x2e__bit9 -C30_0x2e__bit10 -C30_0x2e__bit11 -C30_0x2e__bit12 -C31_0x2e__bit_7 -C31_0x2e__bit_6 -C31_0x2e__bit_5 -C31_0x2e__bit_4 -C31_0x2e__bit_3 -C31_0x2e__bit_2 -C31_0x2e__bit_1 -C31_0x2e__bit0 C31_0x2e__bit1 -C31_0x2e__bit2 C31_0x2e__bit3 -C31_0x2e__bit4 -C31_0x2e__bit5 -C31_0x2e__bit6 -C31_0x2e__bit7 -C31_0x2e__bit8 -C31_0x2e__bit9 -C31_0x2e__bit10 -C31_0x2e__bit11 -C31_0x2e__bit12 -C32_0x2e__bit_7 -C32_0x2e__bit_6 -C32_0x2e__bit_5 -C32_0x2e__bit_4 -C32_0x2e__bit_3 -C32_0x2e__bit_2 -C32_0x2e__bit_1 -C32_0x2e__bit0 -C32_0x2e__bit1 -C32_0x2e__bit2 -C32_0x2e__bit3 -C32_0x2e__bit4 -C32_0x2e__bit5 -C32_0x2e__bit6 -C32_0x2e__bit7 -C32_0x2e__bit8 -C32_0x2e__bit9 -C32_0x2e__bit10 -C32_0x2e__bit11 -C32_0x2e__bit12 -C33_0x2e__bit_7 -C33_0x2e__bit_6 -C33_0x2e__bit_5 C33_0x2e__bit_4 -C33_0x2e__bit_3 C33_0x2e__bit_2 C33_0x2e__bit_1 -C33_0x2e__bit0 -C33_0x2e__bit1 -C33_0x2e__bit2 -C33_0x2e__bit3 -C33_0x2e__bit4 -C33_0x2e__bit5 -C33_0x2e__bit6 -C33_0x2e__bit7 -C33_0x2e__bit8 -C33_0x2e__bit9 -C33_0x2e__bit10 -C33_0x2e__bit11 -C33_0x2e__bit12 -C34_0x2e__bit_7 -C34_0x2e__bit_6 -C34_0x2e__bit_5 -C34_0x2e__bit_4 -C34_0x2e__bit_3 -C34_0x2e__bit_2 -C34_0x2e__bit_1 -C34_0x2e__bit0 -C34_0x2e__bit1 -C34_0x2e__bit2 -C34_0x2e__bit3 -C34_0x2e__bit4 -C34_0x2e__bit5 -C34_0x2e__bit6 -C34_0x2e__bit7 -C34_0x2e__bit8 -C34_0x2e__bit9 -C34_0x2e__bit10 -C34_0x2e__bit11 -C34_0x2e__bit12 -C35_0x2e__bit_7 -C35_0x2e__bit_6 -C35_0x2e__bit_5 -C35_0x2e__bit_4 -C35_0x2e__bit_3 -C35_0x2e__bit_2 -C35_0x2e__bit_1 -C35_0x2e__bit0 -C35_0x2e__bit1 -C35_0x2e__bit2 -C35_0x2e__bit3 -C35_0x2e__bit4 -C35_0x2e__bit5 -C35_0x2e__bit6 -C35_0x2e__bit7 -C35_0x2e__bit8 -C35_0x2e__bit9 -C35_0x2e__bit10 -C35_0x2e__bit11 -C35_0x2e__bit12 C36_0x2e__bit_7 -C36_0x2e__bit_6 -C36_0x2e__bit_5 -C36_0x2e__bit_4 -C36_0x2e__bit_3 -C36_0x2e__bit_2 -C36_0x2e__bit_1 -C36_0x2e__bit0 C36_0x2e__bit1 -C36_0x2e__bit2 -C36_0x2e__bit3 -C36_0x2e__bit4 -C36_0x2e__bit5 -C36_0x2e__bit6 -C36_0x2e__bit7 -C36_0x2e__bit8 -C36_0x2e__bit9 -C36_0x2e__bit10 -C36_0x2e__bit11 -C36_0x2e__bit12 -C37_0x2e__bit_7 -C37_0x2e__bit_6 -C37_0x2e__bit_5 -C37_0x2e__bit_4 C37_0x2e__bit_3 -C37_0x2e__bit_2 -C37_0x2e__bit_1 C37_0x2e__bit0 C37_0x2e__bit1 C37_0x2e__bit2 -C37_0x2e__bit3 -C37_0x2e__bit4 -C37_0x2e__bit5 -C37_0x2e__bit6 -C37_0x2e__bit7 -C37_0x2e__bit8 -C37_0x2e__bit9 -C37_0x2e__bit10 -C37_0x2e__bit11 -C37_0x2e__bit12 -C38_0x2e__bit_7 -C38_0x2e__bit_6 -C38_0x2e__bit_5 -C38_0x2e__bit_4 -C38_0x2e__bit_3 -C38_0x2e__bit_2 -C38_0x2e__bit_1 -C38_0x2e__bit0 -C38_0x2e__bit1 -C38_0x2e__bit2 -C38_0x2e__bit3 -C38_0x2e__bit4 -C38_0x2e__bit5 -C38_0x2e__bit6 -C38_0x2e__bit7 -C38_0x2e__bit8 -C38_0x2e__bit9 -C38

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/614/stat): 614 (minisat+_script) R 613 614 9102 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855266292 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/614/statm): 174 3 169 147 0 27 0
[pid=614] 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=615
New process pid=616
New process pid=617
execve syscall for /bin/sed executable
One traced child (pid=616) 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=617) exited with status: 0
One traced child (pid=615) exited with status: 0
New process pid=618
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-mod013.opb

[startup+10.0041 s]
Raw data (loadavg): 0.93 0.97 0.96 2/58 618
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 3787 0 0 0 967 15 0 0 25 0 1 0 1855266297 16048128 3322 4294967295 134512640 135094434 3221224432 3221221808 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 3918 3322 145 145 0 3773 0
[pid=618] vsize: 15672
Current children cumulated CPU time (s) 9.83
Current children cumulated vsize (Kb) 17796

[startup+20.006 s]
Raw data (loadavg): 0.94 0.97 0.96 2/58 618
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 4651 0 0 0 1963 18 0 0 25 0 1 0 1855266297 17997824 3814 4294967295 134512640 135094434 3221224432 3221223024 134556757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 4394 3814 145 145 0 4249 0
[pid=618] vsize: 17576
Current children cumulated CPU time (s) 19.82
Current children cumulated vsize (Kb) 19700

[startup+30.007 s]
Raw data (loadavg): 0.95 0.97 0.96 2/58 618
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 5028 0 0 0 2960 19 0 0 25 0 1 0 1855266297 18755584 4001 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 4579 4001 145 145 0 4434 0
[pid=618] vsize: 18316
Current children cumulated CPU time (s) 29.8
Current children cumulated vsize (Kb) 20440

[startup+40.0069 s]
Raw data (loadavg): 0.95 0.97 0.96 2/58 620
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 5118 0 0 0 3958 20 0 0 25 0 1 0 1855266297 18944000 4049 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 4625 4049 145 145 0 4480 0
[pid=618] vsize: 18500
Current children cumulated CPU time (s) 39.79
Current children cumulated vsize (Kb) 20624

[startup+50.0088 s]
Raw data (loadavg): 0.96 0.97 0.96 2/58 620
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 5367 0 0 0 4957 20 0 0 25 0 1 0 1855266297 19177472 4108 4294967295 134512640 135094434 3221224432 3221221632 134600310 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 4682 4108 145 145 0 4537 0
[pid=618] vsize: 18728
Current children cumulated CPU time (s) 49.78
Current children cumulated vsize (Kb) 20852

[startup+60.0098 s]
Raw data (loadavg): 0.97 0.97 0.96 2/58 620
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 5603 0 0 0 5955 22 0 0 25 0 1 0 1855266297 19681280 4232 4294967295 134512640 135094434 3221224432 3221223120 134596445 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 4805 4232 145 145 0 4660 0
[pid=618] vsize: 19220
Current children cumulated CPU time (s) 59.78
Current children cumulated vsize (Kb) 21344

[startup+70.0117 s]
Raw data (loadavg): 0.97 0.97 0.96 2/58 620
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 5955 0 0 0 6951 24 0 0 25 0 1 0 1855266297 20660224 4473 4294967295 134512640 135094434 3221224432 3221220176 134519159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 5044 4473 145 145 0 4899 0
[pid=618] vsize: 20176
Current children cumulated CPU time (s) 69.76
Current children cumulated vsize (Kb) 22300

[startup+80.0136 s]
Raw data (loadavg): 0.98 0.97 0.96 2/58 620
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 6434 0 0 0 7944 28 0 0 25 0 1 0 1855266297 22159360 4840 4294967295 134512640 135094434 3221224432 3221220960 134780706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 5410 4840 145 145 0 5265 0
[pid=618] vsize: 21640
Current children cumulated CPU time (s) 79.73
Current children cumulated vsize (Kb) 23764

[startup+90.0136 s]
Raw data (loadavg): 0.98 0.97 0.96 2/58 620
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 6688 0 0 0 8940 30 0 0 25 0 1 0 1855266297 23257088 5094 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 5678 5094 145 145 0 5533 0
[pid=618] vsize: 22712
Current children cumulated CPU time (s) 89.71
Current children cumulated vsize (Kb) 24836

[startup+100.015 s]
Raw data (loadavg): 0.98 0.97 0.96 2/58 622
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 7012 0 0 0 9935 33 0 0 25 0 1 0 1855266297 24109056 5306 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 5886 5306 145 145 0 5741 0
[pid=618] vsize: 23544
Current children cumulated CPU time (s) 99.69
Current children cumulated vsize (Kb) 25668

[startup+110.015 s]
Raw data (loadavg): 0.98 0.97 0.96 2/58 622
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 7335 0 0 0 10929 36 0 0 25 0 1 0 1855266297 25415680 5629 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 6205 5629 145 145 0 6060 0
[pid=618] vsize: 24820
Current children cumulated CPU time (s) 109.66
Current children cumulated vsize (Kb) 26944

[startup+120.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 622
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 7953 0 0 0 11919 40 0 0 25 0 1 0 1855266297 27930624 6247 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 6819 6247 145 145 0 6674 0
[pid=618] vsize: 27276
Current children cumulated CPU time (s) 119.6
Current children cumulated vsize (Kb) 29400

[startup+130.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 622
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 8140 0 0 0 12917 41 0 0 25 0 1 0 1855266297 28241920 6323 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 6895 6323 145 145 0 6750 0
[pid=618] vsize: 27580
Current children cumulated CPU time (s) 129.59
Current children cumulated vsize (Kb) 29704

[startup+140.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 622
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 8140 0 0 0 13916 42 0 0 25 0 1 0 1855266297 28241920 6323 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 6895 6323 145 145 0 6750 0
[pid=618] vsize: 27580
Current children cumulated CPU time (s) 139.59
Current children cumulated vsize (Kb) 29704

[startup+150.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 622
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 8140 0 0 0 14916 42 0 0 25 0 1 0 1855266297 28241920 6323 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 6895 6323 145 145 0 6750 0
[pid=618] vsize: 27580
Current children cumulated CPU time (s) 149.59
Current children cumulated vsize (Kb) 29704

[startup+160.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 624
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 8140 0 0 0 15915 43 0 0 25 0 1 0 1855266297 28241920 6323 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 6895 6323 145 145 0 6750 0
[pid=618] vsize: 27580
Current children cumulated CPU time (s) 159.59
Current children cumulated vsize (Kb) 29704

[startup+170.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 624
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 8160 0 0 0 16915 44 0 0 25 0 1 0 1855266297 28307456 6343 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 6911 6343 145 145 0 6766 0
[pid=618] vsize: 27644
Current children cumulated CPU time (s) 169.6
Current children cumulated vsize (Kb) 29768

[startup+180.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 624
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 8493 0 0 0 17908 47 0 0 25 0 1 0 1855266297 29790208 6676 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 7273 6676 145 145 0 7128 0
[pid=618] vsize: 29092
Current children cumulated CPU time (s) 179.56
Current children cumulated vsize (Kb) 31216

[startup+190.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 624
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 8785 0 0 0 18902 50 0 0 25 0 1 0 1855266297 30973952 6968 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 7562 6968 145 145 0 7417 0
[pid=618] vsize: 30248
Current children cumulated CPU time (s) 189.53
Current children cumulated vsize (Kb) 32372

[startup+200.028 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 624
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 9104 0 0 0 19894 53 0 0 25 0 1 0 1855266297 32268288 7287 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 7878 7287 145 145 0 7733 0
[pid=618] vsize: 31512
Current children cumulated CPU time (s) 199.48
Current children cumulated vsize (Kb) 33636

[startup+210.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 624
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 9510 0 0 0 20886 57 0 0 25 0 1 0 1855266297 33914880 7693 4294967295 134512640 135094434 3221224432 3221223104 134555583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/618/statm): 8280 7693 145 145 0 8135 0
[pid=618] vsize: 33120
Current children cumulated CPU time (s) 209.44
Current children cumulated vsize (Kb) 35244

[startup+220.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 626
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 9845 0 0 0 21879 60 0 0 25 0 1 0 1855266297 35274752 8028 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 8612 8028 145 145 0 8467 0
[pid=618] vsize: 34448
Current children cumulated CPU time (s) 219.4
Current children cumulated vsize (Kb) 36572

[startup+230.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 626
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 10018 0 0 0 22875 61 0 0 25 0 1 0 1855266297 35971072 8201 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 8782 8201 145 145 0 8637 0
[pid=618] vsize: 35128
Current children cumulated CPU time (s) 229.37
Current children cumulated vsize (Kb) 37252

[startup+240.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 626
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 10171 0 0 0 23872 63 0 0 25 0 1 0 1855266297 36589568 8354 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 8933 8354 145 145 0 8788 0
[pid=618] vsize: 35732
Current children cumulated CPU time (s) 239.36
Current children cumulated vsize (Kb) 37856

[startup+250.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 626
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 10326 0 0 0 24869 64 0 0 25 0 1 0 1855266297 37220352 8509 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 9087 8509 145 145 0 8942 0
[pid=618] vsize: 36348
Current children cumulated CPU time (s) 249.34
Current children cumulated vsize (Kb) 38472

[startup+260.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 626
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 10472 0 0 0 25866 66 0 0 25 0 1 0 1855266297 37810176 8655 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 9231 8655 145 145 0 9086 0
[pid=618] vsize: 36924
Current children cumulated CPU time (s) 259.33
Current children cumulated vsize (Kb) 39048

[startup+270.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 626
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 10642 0 0 0 26864 67 0 0 25 0 1 0 1855266297 38498304 8825 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 9399 8825 145 145 0 9254 0
[pid=618] vsize: 37596
Current children cumulated CPU time (s) 269.32
Current children cumulated vsize (Kb) 39720

[startup+280.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 628
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 10791 0 0 0 27862 68 0 0 25 0 1 0 1855266297 39100416 8974 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 9546 8974 145 145 0 9401 0
[pid=618] vsize: 38184
Current children cumulated CPU time (s) 279.31
Current children cumulated vsize (Kb) 40308

[startup+290.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 628
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 10962 0 0 0 28858 69 0 0 25 0 1 0 1855266297 39792640 9145 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 9715 9145 145 145 0 9570 0
[pid=618] vsize: 38860
Current children cumulated CPU time (s) 289.28
Current children cumulated vsize (Kb) 40984

[startup+300.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 628
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 11135 0 0 0 29855 71 0 0 25 0 1 0 1855266297 40493056 9318 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 9886 9318 145 145 0 9741 0
[pid=618] vsize: 39544
Current children cumulated CPU time (s) 299.27
Current children cumulated vsize (Kb) 41668

[startup+310.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 628
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 11297 0 0 0 30852 72 0 0 25 0 1 0 1855266297 41418752 9480 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 10112 9480 145 145 0 9967 0
[pid=618] vsize: 40448
Current children cumulated CPU time (s) 309.25
Current children cumulated vsize (Kb) 42572

[startup+320.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 628
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 11457 0 0 0 31849 74 0 0 25 0 1 0 1855266297 42070016 9640 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 10271 9640 145 145 0 10126 0
[pid=618] vsize: 41084
Current children cumulated CPU time (s) 319.24
Current children cumulated vsize (Kb) 43208

[startup+330.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 628
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 11602 0 0 0 32846 75 0 0 25 0 1 0 1855266297 42651648 9785 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 10413 9785 145 145 0 10268 0
[pid=618] vsize: 41652
Current children cumulated CPU time (s) 329.22
Current children cumulated vsize (Kb) 43776

[startup+340.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 630
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 11733 0 0 0 33844 76 0 0 25 0 1 0 1855266297 43184128 9916 4294967295 134512640 135094434 3221224432 3221223072 134562113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 10543 9916 145 145 0 10398 0
[pid=618] vsize: 42172
Current children cumulated CPU time (s) 339.21
Current children cumulated vsize (Kb) 44296

[startup+350.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 630
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 11909 0 0 0 34842 77 0 0 25 0 1 0 1855266297 43900928 10092 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 10718 10092 145 145 0 10573 0
[pid=618] vsize: 42872
Current children cumulated CPU time (s) 349.2
Current children cumulated vsize (Kb) 44996

[startup+360.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 630
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 12029 0 0 0 35840 78 0 0 25 0 1 0 1855266297 44384256 10212 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 10836 10212 145 145 0 10691 0
[pid=618] vsize: 43344
Current children cumulated CPU time (s) 359.19
Current children cumulated vsize (Kb) 45468

[startup+370.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 630
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 12152 0 0 0 36838 79 0 0 25 0 1 0 1855266297 44892160 10335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 10960 10335 145 145 0 10815 0
[pid=618] vsize: 43840
Current children cumulated CPU time (s) 369.18
Current children cumulated vsize (Kb) 45964

[startup+380.045 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 630
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 12290 0 0 0 37836 80 0 0 25 0 1 0 1855266297 45445120 10473 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 11095 10473 145 145 0 10950 0
[pid=618] vsize: 44380
Current children cumulated CPU time (s) 379.17
Current children cumulated vsize (Kb) 46504

[startup+390.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 630
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 12637 0 0 0 38830 82 0 0 25 0 1 0 1855266297 46854144 10820 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 11439 10820 145 145 0 11294 0
[pid=618] vsize: 45756
Current children cumulated CPU time (s) 389.13
Current children cumulated vsize (Kb) 47880

[startup+400.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 632
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 12817 0 0 0 39827 84 0 0 25 0 1 0 1855266297 47583232 11000 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 11617 11000 145 145 0 11472 0
[pid=618] vsize: 46468
Current children cumulated CPU time (s) 399.12
Current children cumulated vsize (Kb) 48592

[startup+410.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 632
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 12963 0 0 0 40825 85 0 0 25 0 1 0 1855266297 48181248 11146 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 11763 11146 145 145 0 11618 0
[pid=618] vsize: 47052
Current children cumulated CPU time (s) 409.11
Current children cumulated vsize (Kb) 49176

[startup+420.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 632
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13085 0 0 0 41822 86 0 0 25 0 1 0 1855266297 48676864 11268 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 11884 11268 145 145 0 11739 0
[pid=618] vsize: 47536
Current children cumulated CPU time (s) 419.09
Current children cumulated vsize (Kb) 49660

[startup+430.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 632
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13202 0 0 0 42822 87 0 0 25 0 1 0 1855266297 49152000 11385 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12000 11385 145 145 0 11855 0
[pid=618] vsize: 48000
Current children cumulated CPU time (s) 429.1
Current children cumulated vsize (Kb) 50124

[startup+440.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 632
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13358 0 0 0 43818 88 0 0 25 0 1 0 1855266297 49782784 11541 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12154 11541 145 145 0 12009 0
[pid=618] vsize: 48616
Current children cumulated CPU time (s) 439.07
Current children cumulated vsize (Kb) 50740

[startup+450.051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 632
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13529 0 0 0 44815 89 0 0 25 0 1 0 1855266297 50475008 11712 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12323 11712 145 145 0 12178 0
[pid=618] vsize: 49292
Current children cumulated CPU time (s) 449.05
Current children cumulated vsize (Kb) 51416

[startup+460.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 634
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13654 0 0 0 45814 90 0 0 25 0 1 0 1855266297 50982912 11837 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11837 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 459.05
Current children cumulated vsize (Kb) 51912

[startup+470.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 634
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13654 0 0 0 46814 90 0 0 25 0 1 0 1855266297 50982912 11837 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11837 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 469.05
Current children cumulated vsize (Kb) 51912

[startup+480.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 634
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13654 0 0 0 47814 90 0 0 25 0 1 0 1855266297 50982912 11837 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11837 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 479.05
Current children cumulated vsize (Kb) 51912

[startup+490.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 634
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13654 0 0 0 48814 90 0 0 25 0 1 0 1855266297 50982912 11837 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11837 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 489.05
Current children cumulated vsize (Kb) 51912

[startup+500.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 634
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13654 0 0 0 49814 90 0 0 25 0 1 0 1855266297 50982912 11837 4294967295 134512640 135094434 3221224432 3221223088 134557823 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11837 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 499.05
Current children cumulated vsize (Kb) 51912

[startup+510.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 634
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13654 0 0 0 50814 90 0 0 25 0 1 0 1855266297 50982912 11837 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11837 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 509.05
Current children cumulated vsize (Kb) 51912

[startup+520.058 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 636
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13654 0 0 0 51815 90 0 0 25 0 1 0 1855266297 50982912 11837 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11837 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 519.06
Current children cumulated vsize (Kb) 51912

[startup+530.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 636
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13654 0 0 0 52815 90 0 0 25 0 1 0 1855266297 50982912 11837 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11837 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 529.06
Current children cumulated vsize (Kb) 51912

[startup+540.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 636
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13654 0 0 0 53815 90 0 0 25 0 1 0 1855266297 50982912 11837 4294967295 134512640 135094434 3221224432 3221223024 134557263 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11837 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 539.06
Current children cumulated vsize (Kb) 51912

[startup+550.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 636
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13654 0 0 0 54815 90 0 0 25 0 1 0 1855266297 50982912 11837 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11837 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 549.06
Current children cumulated vsize (Kb) 51912

[startup+560.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 636
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13654 0 0 0 55815 90 0 0 25 0 1 0 1855266297 50982912 11837 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11837 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 559.06
Current children cumulated vsize (Kb) 51912

[startup+570.061 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 636
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13654 0 0 0 56816 90 0 0 25 0 1 0 1855266297 50982912 11837 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11837 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 569.07
Current children cumulated vsize (Kb) 51912

[startup+580.062 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 638
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13654 0 0 0 57816 90 0 0 25 0 1 0 1855266297 50982912 11837 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11837 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 579.07
Current children cumulated vsize (Kb) 51912

[startup+590.063 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 638
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13654 0 0 0 58816 90 0 0 25 0 1 0 1855266297 50982912 11837 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11837 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 589.07
Current children cumulated vsize (Kb) 51912

[startup+600.064 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 638
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13654 0 0 0 59816 90 0 0 25 0 1 0 1855266297 50982912 11837 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11837 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 599.07
Current children cumulated vsize (Kb) 51912

[startup+610.065 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 638
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13654 0 0 0 60817 90 0 0 25 0 1 0 1855266297 50982912 11837 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11837 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 609.08
Current children cumulated vsize (Kb) 51912

[startup+620.066 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 638
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13655 0 0 0 61817 90 0 0 25 0 1 0 1855266297 50982912 11838 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11838 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 619.08
Current children cumulated vsize (Kb) 51912

[startup+630.067 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 638
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13655 0 0 0 62817 90 0 0 25 0 1 0 1855266297 50982912 11838 4294967295 134512640 135094434 3221224432 3221223056 134557734 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11838 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 629.08
Current children cumulated vsize (Kb) 51912

[startup+640.067 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 640
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13655 0 0 0 63817 90 0 0 25 0 1 0 1855266297 50982912 11838 4294967295 134512640 135094434 3221224432 3221223104 134555763 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11838 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 639.08
Current children cumulated vsize (Kb) 51912

[startup+650.068 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 640
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13655 0 0 0 64817 90 0 0 25 0 1 0 1855266297 50982912 11838 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11838 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 649.08
Current children cumulated vsize (Kb) 51912

[startup+660.069 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 640
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13655 0 0 0 65818 90 0 0 25 0 1 0 1855266297 50982912 11838 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11838 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 659.09
Current children cumulated vsize (Kb) 51912

[startup+670.071 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 640
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13656 0 0 0 66818 90 0 0 25 0 1 0 1855266297 50982912 11839 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11839 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 669.09
Current children cumulated vsize (Kb) 51912

[startup+680.072 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 640
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13656 0 0 0 67818 90 0 0 25 0 1 0 1855266297 50982912 11839 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11839 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 679.09
Current children cumulated vsize (Kb) 51912

[startup+690.072 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 640
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13656 0 0 0 68819 90 0 0 25 0 1 0 1855266297 50982912 11839 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11839 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 689.1
Current children cumulated vsize (Kb) 51912

[startup+700.072 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 642
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13656 0 0 0 69819 90 0 0 25 0 1 0 1855266297 50982912 11839 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11839 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 699.1
Current children cumulated vsize (Kb) 51912

[startup+710.073 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 642
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13656 0 0 0 70819 90 0 0 25 0 1 0 1855266297 50982912 11839 4294967295 134512640 135094434 3221224432 3221223024 134557055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11839 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 709.1
Current children cumulated vsize (Kb) 51912

[startup+720.074 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 642
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13656 0 0 0 71819 90 0 0 25 0 1 0 1855266297 50982912 11839 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12447 11839 145 145 0 12302 0
[pid=618] vsize: 49788
Current children cumulated CPU time (s) 719.1
Current children cumulated vsize (Kb) 51912

[startup+730.075 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 642
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13802 0 0 0 72817 91 0 0 25 0 1 0 1855266297 51580928 11985 4294967295 134512640 135094434 3221224432 3221223080 134558260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12593 11985 145 145 0 12448 0
[pid=618] vsize: 50372
Current children cumulated CPU time (s) 729.09
Current children cumulated vsize (Kb) 52496

[startup+740.076 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 642
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 13947 0 0 0 73814 92 0 0 25 0 1 0 1855266297 52174848 12130 4294967295 134512640 135094434 3221224432 3221223088 134558033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12738 12130 145 145 0 12593 0
[pid=618] vsize: 50952
Current children cumulated CPU time (s) 739.07
Current children cumulated vsize (Kb) 53076

[startup+750.077 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 642
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 14066 0 0 0 74812 93 0 0 25 0 1 0 1855266297 52678656 12249 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 12861 12249 145 145 0 12716 0
[pid=618] vsize: 51444
Current children cumulated CPU time (s) 749.06
Current children cumulated vsize (Kb) 53568

[startup+760.078 s]
Raw data (loadavg): 1.15 1.01 0.97 2/58 644
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 14210 0 0 0 75811 94 0 0 25 0 1 0 1855266297 53260288 12393 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 13003 12393 145 145 0 12858 0
[pid=618] vsize: 52012
Current children cumulated CPU time (s) 759.06
Current children cumulated vsize (Kb) 54136

[startup+770.08 s]
Raw data (loadavg): 1.13 1.00 0.97 2/58 644
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 14396 0 0 0 76807 95 0 0 25 0 1 0 1855266297 54018048 12579 4294967295 134512640 135094434 3221224432 3221223024 134557168 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 13188 12579 145 145 0 13043 0
[pid=618] vsize: 52752
Current children cumulated CPU time (s) 769.03
Current children cumulated vsize (Kb) 54876

[startup+780.081 s]
Raw data (loadavg): 1.11 1.00 0.97 2/58 644
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 14545 0 0 0 77805 97 0 0 25 0 1 0 1855266297 54620160 12728 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 13335 12728 145 145 0 13190 0
[pid=618] vsize: 53340
Current children cumulated CPU time (s) 779.03
Current children cumulated vsize (Kb) 55464

[startup+790.081 s]
Raw data (loadavg): 1.09 1.00 0.97 2/58 644
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 14699 0 0 0 78803 98 0 0 25 0 1 0 1855266297 55246848 12882 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 13488 12882 145 145 0 13343 0
[pid=618] vsize: 53952
Current children cumulated CPU time (s) 789.02
Current children cumulated vsize (Kb) 56076

[startup+800.082 s]
Raw data (loadavg): 1.08 1.00 0.97 2/58 644
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 14836 0 0 0 79801 99 0 0 25 0 1 0 1855266297 55799808 13019 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 13623 13019 145 145 0 13478 0
[pid=618] vsize: 54492
Current children cumulated CPU time (s) 799.01
Current children cumulated vsize (Kb) 56616

[startup+810.083 s]
Raw data (loadavg): 1.07 1.00 0.97 2/58 644
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 14949 0 0 0 80799 99 0 0 25 0 1 0 1855266297 56274944 13132 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 13739 13132 145 145 0 13594 0
[pid=618] vsize: 54956
Current children cumulated CPU time (s) 808.99
Current children cumulated vsize (Kb) 57080

[startup+820.084 s]
Raw data (loadavg): 1.06 1.00 0.97 2/58 646
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15084 0 0 0 81797 100 0 0 25 0 1 0 1855266297 56811520 13267 4294967295 134512640 135094434 3221224432 3221223088 134558135 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 13870 13267 145 145 0 13725 0
[pid=618] vsize: 55480
Current children cumulated CPU time (s) 818.98
Current children cumulated vsize (Kb) 57604

[startup+830.085 s]
Raw data (loadavg): 1.05 1.00 0.97 2/58 646
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15228 0 0 0 82794 101 0 0 25 0 1 0 1855266297 57397248 13411 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14013 13411 145 145 0 13868 0
[pid=618] vsize: 56052
Current children cumulated CPU time (s) 828.96
Current children cumulated vsize (Kb) 58176

[startup+840.086 s]
Raw data (loadavg): 1.04 1.00 0.97 2/58 646
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15353 0 0 0 83792 102 0 0 25 0 1 0 1855266297 57909248 13536 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14138 13536 145 145 0 13993 0
[pid=618] vsize: 56552
Current children cumulated CPU time (s) 838.95
Current children cumulated vsize (Kb) 58676

[startup+850.087 s]
Raw data (loadavg): 1.03 1.00 0.97 2/58 646
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15473 0 0 0 84791 103 0 0 25 0 1 0 1855266297 58392576 13656 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14256 13656 145 145 0 14111 0
[pid=618] vsize: 57024
Current children cumulated CPU time (s) 848.95
Current children cumulated vsize (Kb) 59148

[startup+860.087 s]
Raw data (loadavg): 1.03 1.00 0.97 2/58 646
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 85789 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223024 134551469 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 858.93
Current children cumulated vsize (Kb) 59536

[startup+870.088 s]
Raw data (loadavg): 1.02 1.00 0.97 2/58 646
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 86790 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 868.94
Current children cumulated vsize (Kb) 59536

[startup+880.089 s]
Raw data (loadavg): 1.02 1.00 0.97 2/58 648
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 87790 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223024 134557238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 878.94
Current children cumulated vsize (Kb) 59536

[startup+890.09 s]
Raw data (loadavg): 1.02 1.00 0.97 2/58 648
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 88790 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 888.94
Current children cumulated vsize (Kb) 59536

[startup+900.091 s]
Raw data (loadavg): 1.01 1.00 0.97 2/58 648
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 89791 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 898.95
Current children cumulated vsize (Kb) 59536

[startup+910.092 s]
Raw data (loadavg): 1.01 1.00 0.97 2/58 648
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 90791 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223056 134562158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 908.95
Current children cumulated vsize (Kb) 59536

[startup+920.094 s]
Raw data (loadavg): 1.01 1.00 0.97 2/58 648
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 91791 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 918.95
Current children cumulated vsize (Kb) 59536

[startup+930.095 s]
Raw data (loadavg): 1.01 1.00 0.97 2/58 648
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 92791 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 928.95
Current children cumulated vsize (Kb) 59536

[startup+940.095 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 650
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 93791 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 938.95
Current children cumulated vsize (Kb) 59536

[startup+950.097 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 650
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 94792 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 948.96
Current children cumulated vsize (Kb) 59536

[startup+960.098 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 650
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 95792 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 958.96
Current children cumulated vsize (Kb) 59536

[startup+970.099 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 650
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 96792 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 968.96
Current children cumulated vsize (Kb) 59536

[startup+980.1 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 650
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 97792 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 978.96
Current children cumulated vsize (Kb) 59536

[startup+990.1 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 650
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 98792 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 988.96
Current children cumulated vsize (Kb) 59536

[startup+1000.1 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 652
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 99792 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 998.96
Current children cumulated vsize (Kb) 59536

[startup+1010.1 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 652
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 100793 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 1008.97
Current children cumulated vsize (Kb) 59536

[startup+1020.1 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 652
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 101793 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 1018.97
Current children cumulated vsize (Kb) 59536

[startup+1030.1 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 652
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 102793 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 1028.97
Current children cumulated vsize (Kb) 59536

[startup+1040.1 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 652
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 103793 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 1038.97
Current children cumulated vsize (Kb) 59536

[startup+1050.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 652
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 104794 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 1048.98
Current children cumulated vsize (Kb) 59536

[startup+1060.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 654
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 105794 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 1058.98
Current children cumulated vsize (Kb) 59536

[startup+1070.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 654
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 106794 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134558147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 1068.98
Current children cumulated vsize (Kb) 59536

[startup+1080.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 654
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 107795 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223104 134555763 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 1078.99
Current children cumulated vsize (Kb) 59536

[startup+1090.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 654
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 108795 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 1088.99
Current children cumulated vsize (Kb) 59536

[startup+1100.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 654
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 109795 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 1098.99
Current children cumulated vsize (Kb) 59536

[startup+1110.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 654
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 110795 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 1108.99
Current children cumulated vsize (Kb) 59536

[startup+1120.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 656
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 111796 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 1119
Current children cumulated vsize (Kb) 59536

[startup+1130.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 656
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 112796 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223104 134556540 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 1129
Current children cumulated vsize (Kb) 59536

[startup+1140.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 656
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 113796 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223056 134557660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 1139
Current children cumulated vsize (Kb) 59536

[startup+1150.12 s]
Raw data (loadavg): 1.00 1.00 0.97 2/58 656
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 114796 103 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 1149
Current children cumulated vsize (Kb) 59536

[startup+1160.12 s]
Raw data (loadavg): 1.08 1.02 0.98 2/58 707
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 115795 104 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 1159
Current children cumulated vsize (Kb) 59536

[startup+1170.12 s]
Raw data (loadavg): 1.07 1.02 0.98 2/58 707
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 116795 104 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 1169
Current children cumulated vsize (Kb) 59536

[startup+1180.12 s]
Raw data (loadavg): 1.06 1.01 0.98 2/58 709
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 117796 104 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 1179.01
Current children cumulated vsize (Kb) 59536

[startup+1190.12 s]
Raw data (loadavg): 1.05 1.01 0.98 2/58 709
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15571 0 0 0 118796 104 0 0 25 0 1 0 1855266297 58789888 13754 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14353 13754 145 145 0 14208 0
[pid=618] vsize: 57412
Current children cumulated CPU time (s) 1189.01
Current children cumulated vsize (Kb) 59536

[startup+1200.12 s]
Raw data (loadavg): 1.04 1.01 0.98 2/58 709
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15702 0 0 0 119792 105 0 0 25 0 1 0 1855266297 59330560 13885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14485 13885 145 145 0 14340 0
[pid=618] vsize: 57940
Current children cumulated CPU time (s) 1198.98
Current children cumulated vsize (Kb) 60064

[startup+1210.12 s]
Raw data (loadavg): 1.03 1.01 0.98 2/58 709
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15900 0 0 0 120790 107 0 0 25 0 1 0 1855266297 60141568 14083 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14683 14083 145 145 0 14538 0
[pid=618] vsize: 58732
Current children cumulated CPU time (s) 1208.98
Current children cumulated vsize (Kb) 60856



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 1.03 1.01 0.98 2/58 709
Raw data (/proc/614/stat): 614 (minisat+_script) S 613 614 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855266292 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/614/statm): 531 226 485 147 0 384 0
[pid=614] vsize: 2124
Raw data (/proc/618/stat): 618 (minisat+_64-bit) R 614 614 9102 0 -1 0 15900 0 0 0 120790 107 0 0 25 0 1 0 1855266297 60141568 14083 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/618/statm): 14683 14083 145 145 0 14538 0
[pid=618] vsize: 58732
Current children cumulated CPU time (s) 1208.98
Current children cumulated vsize (Kb) 60856

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

Child status: 10
Real time (s): 1210.16
CPU time (s): 1209.01
CPU user time (s): 1207.91
CPU system time (s): 1.09783
CPU usage (%): 99.9049
Max. virtual memory (cumulated for all children) (Kb): 60856

Verifier Data

ERROR: no interpretation found !