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-egout.opb
MD5SUM46c4db5f8baf54496e00a723c85beb20
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 65869824
Optimality of the best value was proved NO
Number of terms in the objective function 1095
Biggest coefficient in the objective function 533200896
Number of bits for the biggest coefficient in the objective function 29
Sum of the numbers in the objective function 14929722305
Number of bits of the sum of numbers in the objective function 34
Biggest number in a constraint 533200896
Number of bits of the biggest number in a constraint 29
Biggest sum of numbers in a constraint 14929722305
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 benchmark1257.65
Number of variables1155
Total number of constraints153
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)55
Number of constraints which are nor clauses,nor cardinality constraints98
Minimum length of a constraint1
Maximum length of a constraint280

Trace number 6083

Launcher Data

LAUNCH ON wulflinc13 THE 2005-09-20 03:08:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3235 boxname=wulflinc13 idbench=891 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  46c4db5f8baf54496e00a723c85beb20  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-egout.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-egout.opb
IDLAUNCH: 3235
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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	: 2
cpu MHz		: 451.242
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:        901452 kB
Buffers:         28588 kB
Cached:          77608 kB
SwapCached:        700 kB
Active:          32924 kB
Inactive:        75852 kB
HighTotal:      131008 kB
HighFree:        49504 kB
LowTotal:       903652 kB
LowFree:        851948 kB
SwapTotal:     2097136 kB
SwapFree:      2095936 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5740 kB
Slab:            18828 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 03:28:46 (client local time) WITH STATUS 10 IN 1209.42 SECONDS
stats: 3235 7 1209.42 10

Solver Data

c Parsing PB file...
c Converting 115 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ###########################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 113]---> Adder-cost: 273   maxlim: 13440   bits: 15/14
c ---[ 111]---> BDD-cost:   40
c ---[ 109]---> BDD-cost:   25
c ---[ 107]---> BDD-cost:   45
c ---[ 105]---> BDD-cost:   83
c ---[ 101]---> BDD-cost:   39
c ---[  99]---> BDD-cost:  100
c ---[  97]---> BDD-cost:   34
c ---[  91]---> BDD-cost:   55
c ---[  89]---> BDD-cost:   40
c ---[  85]---> BDD-cost:  128
c ---[  83]---> BDD-cost:   40
c ---[  81]---> BDD-cost:  112
c ---[  79]---> BDD-cost:   49
c ---[  75]---> BDD-cost:   45
c ---[  73]---> BDD-cost:   28
c ---[  71]---> Sorter-cost:  514     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  69]---> BDD-cost:   55
c ---[  67]---> Sorter-cost:  294     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  65]---> BDD-cost:  118
c ---[  59]---> BDD-cost:   51
c ---[  57]---> BDD-cost:   40
c ---[  55]---> BDD-cost:   40
c ---[  53]---> BDD-cost:   51
c ---[  49]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> BDD-cost:   49
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:    9
c ---[  41]---> BDD-cost:   10
c ---[  40]---> BDD-cost:   10
c ---[  39]---> BDD-cost:   11
c ---[  37]---> BDD-cost:   12
c ---[  36]---> BDD-cost:   12
c ---[  35]---> BDD-cost:   12
c ---[  34]---> BDD-cost:   12
c ---[  31]---> BDD-cost:   12
c ---[  30]---> BDD-cost:   12
c ---[  29]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   26
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   26
c ---[  24]---> BDD-cost:   26
c ---[  23]---> BDD-cost:   26
c ---[  21]---> BDD-cost:   10
c ---[  20]---> BDD-cost:   10
c ---[  19]---> BDD-cost:   10
c ---[  18]---> BDD-cost:   26
c ---[  17]---> BDD-cost:   26
c ---[  16]---> BDD-cost:   12
c ---[  15]---> BDD-cost:   12
c ---[  14]---> BDD-cost:   26
c ---[  13]---> BDD-cost:   26
c ---[  12]---> BDD-cost:   26
c ---[   9]---> BDD-cost:   26
c ---[   8]---> BDD-cost:   26
c ---[   7]---> BDD-cost:   26
c ---[   6]---> BDD-cost:   26
c ---[   4]---> BDD-cost:   26
c ---[   3]---> BDD-cost:   26
c ---[   2]---> BDD-cost:   26
c ---[   1]---> BDD-cost:   26
c ---[   0]---> BDD-cost:   26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    8871    23614 |    2957       0        0     nan |  0.000 % |
c |       100 |    8706    23213 |    3252      62      334     5.4 | 23.506 % |
c |       250 |    8614    23023 |    3577     176      817     4.6 | 24.498 % |
c |       477 |    8528    22841 |    3935     375     2437     6.5 | 25.341 % |
c ==============================================================================
c Found solution: 98251161
c ---[   0]---> Sorter-cost:93899     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       730 |  274243   643179 |   91414     601     3802     6.3 | 25.341 % |
c |       830 |  273012   640414 |  100555     689     4783     6.9 |  1.488 % |
c |       980 |  272757   639831 |  110610     835     6097     7.3 |  1.557 % |
c |      1209 |  272173   638509 |  121672    1057     7316     6.9 |  1.728 % |
c |      1546 |  271248   636409 |  133839    1388    10219     7.4 |  2.008 % |
c |      2053 |  270967   635780 |  147223    1885    16941     9.0 |  2.090 % |
c ==============================================================================
c Found solution: 90380944
c ---[   0]---> Sorter-cost:56645     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2528 |  421107   986844 |  140369    2270    26867    11.8 |  2.090 % |
c |      2628 |  420986   986571 |  154405    2368    27410    11.6 |  2.870 % |
c |      2778 |  418881   981794 |  169846    2509    29164    11.6 |  3.270 % |
c ==============================================================================
c Found solution: 83601220
c ---[   0]---> Sorter-cost:51266     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2859 |  560988  1313562 |  186996    2590    37268    14.4 |  3.270 % |
c |      2959 |  560234  1311863 |  205695    2684    37786    14.1 |  2.647 % |
c |      3109 |  560085  1311520 |  226265    2833    52989    18.7 |  2.671 % |
c |      3334 |  559906  1311131 |  248891    3057    54077    17.7 |  2.703 % |
c |      3672 |  559906  1311131 |  273780    3395    57914    17.1 |  2.703 % |
c ==============================================================================
c Found solution: 75080280
c ---[   0]---> Sorter-cost:   20     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3889 |  560311  1312659 |  186770    3605    66861    18.5 |  2.703 % |
c |      3989 |  560053  1312084 |  205447    3701    67324    18.2 |  2.799 % |
c |      4139 |  559865  1311660 |  225991    3849    71131    18.5 |  2.827 % |
c |      4364 |  559744  1311385 |  248590    4073    72701    17.8 |  2.846 % |
c |      4701 |  559733  1311361 |  273449    4409    75036    17.0 |  2.848 % |
c |      5207 |  559649  1311172 |  300794    4914    78073    15.9 |  2.858 % |
c ==============================================================================
c Found solution: 72902771
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5394 |  559424  1310762 |  186474    5083    83077    16.3 |  2.858 % |
c |      5494 |  559424  1310762 |  205121    5183    84108    16.2 |  2.900 % |
c |      5644 |  559424  1310762 |  225633    5333    94640    17.7 |  2.899 % |
c |      5869 |  559350  1310597 |  248196    5557   103255    18.6 |  2.910 % |
c |      6207 |  559293  1310471 |  273016    5888   119017    20.2 |  2.918 % |
c |      6715 |  558850  1309460 |  300318    6394   140155    21.9 |  2.985 % |
c ==============================================================================
c Found solution: 70799895
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7150 |  557562  1306544 |  185854    6823   185362    27.2 |  2.985 % |
c |      7250 |  557562  1306544 |  204439    6923   191283    27.6 |  3.180 % |
c |      7400 |  557562  1306544 |  224883    7073   196159    27.7 |  3.180 % |
c ==============================================================================
c Found solution: 68823191
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7433 |  557596  1306628 |  185865    7106   197145    27.7 |  3.180 % |
c |      7535 |  557596  1306628 |  204451    7208   207757    28.8 |  3.181 % |
c |      7689 |  557596  1306628 |  224896    7362   210303    28.6 |  3.181 % |
c ==============================================================================
c Found solution: 66801712
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7739 |  557622  1306690 |  185874    7412   211372    28.5 |  3.181 % |
c |      7839 |  557622  1306690 |  204461    7512   214674    28.6 |  3.181 % |
c |      7990 |  557622  1306690 |  224907    7663   221258    28.9 |  3.181 % |
c |      8215 |  557575  1306584 |  247398    7887   224224    28.4 |  3.187 % |
c |      8553 |  556893  1305042 |  272138    8018   226835    28.3 |  3.287 % |
c |      9059 |  556893  1305042 |  299351    8524   351418    41.2 |  3.287 % |
c |      9818 |  556828  1304894 |  329287    9282   372202    40.1 |  3.297 % |
c |     10957 |  555966  1302938 |  362215   10397   418014    40.2 |  3.424 % |
c ==============================================================================
c Found solution: 65961920
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12376 |  555644  1302223 |  185214   11760   470077    40.0 |  3.424 % |
c |     12477 |  555644  1302223 |  203735   11861   473070    39.9 |  3.486 % |
c |     12628 |  555140  1301079 |  224108   12008   479077    39.9 |  3.560 % |
c |     12853 |  555140  1301079 |  246519   12233   483370    39.5 |  3.560 % |
c |     13193 |  555140  1301079 |  271171   12572   490526    39.0 |  3.573 % |
c ==============================================================================
c Found solution: 65957568
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13361 |  554865  1300533 |  184955   12724   500141    39.3 |  3.573 % |
c |     13464 |  554865  1300533 |  203450   12827   503589    39.3 |  3.603 % |
c |     13618 |  554865  1300533 |  223795   12981   514623    39.6 |  3.603 % |
c |     13843 |  554865  1300533 |  246175   13206   519440    39.3 |  3.603 % |
c |     14180 |  554865  1300533 |  270792   13543   529329    39.1 |  3.603 % |
c ==============================================================================
c Found solution: 64888022
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14535 |  554886  1300584 |  184962   13898   594958    42.8 |  3.603 % |
c |     14636 |  554872  1300551 |  203458   13996   595705    42.6 |  3.606 % |
c |     14788 |  554843  1300486 |  223804   14134   596715    42.2 |  3.610 % |
c ==============================================================================
c Found solution: 64714286
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14980 |  554864  1300536 |  184954   14326   613466    42.8 |  3.610 % |
c |     15081 |  554864  1300536 |  203449   14427   616582    42.7 |  3.611 % |
c |     15231 |  554864  1300536 |  223794   14577   625465    42.9 |  3.611 % |
c |     15456 |  554864  1300536 |  246173   14802   646941    43.7 |  3.611 % |
c |     15795 |  554864  1300536 |  270791   15141   669297    44.2 |  3.611 % |
c |     16301 |  554864  1300536 |  297870   15647   708282    45.3 |  3.611 % |
c |     17060 |  554730  1300230 |  327657   16373   715663    43.7 |  3.633 % |
c |     18200 |  554730  1300230 |  360423   17513   730350    41.7 |  3.633 % |
c ==============================================================================
c Found solution: 64484352
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19484 |  554438  1299569 |  184812   18777   796102    42.4 |  3.633 % |
c |     19584 |  554438  1299569 |  203293   18877   799033    42.3 |  3.678 % |
c |     19735 |  554438  1299569 |  223622   19028   800696    42.1 |  3.678 % |
c |     19961 |  554438  1299569 |  245984   19254   807646    41.9 |  3.678 % |
c |     20299 |  554346  1299358 |  270583   19587   822303    42.0 |  3.696 % |
c |     20808 |  554342  1299350 |  297641   20093   845460    42.1 |  3.698 % |
c ==============================================================================
c Found solution: 64437712
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21505 |  554360  1299393 |  184786   20790   904089    43.5 |  3.698 % |
c |     21606 |  554360  1299393 |  203264   20891   909522    43.5 |  3.698 % |
c |     21757 |  554360  1299393 |  223591   21042   912661    43.4 |  3.698 % |
c ==============================================================================
c Found solution: 64396544
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21945 |  554376  1299432 |  184792   21230   918944    43.3 |  3.698 % |
c |     22046 |  554376  1299432 |  203271   21331   922113    43.2 |  3.698 % |
c |     22196 |  554376  1299432 |  223598   21481   931036    43.3 |  3.698 % |
c |     22421 |  554376  1299432 |  245958   21706   950010    43.8 |  3.698 % |
c |     22759 |  554376  1299432 |  270553   22044   962059    43.6 |  3.698 % |
c |     23266 |  554376  1299432 |  297609   22551   985413    43.7 |  3.698 % |
c |     24025 |  554376  1299432 |  327370   23310  1062588    45.6 |  3.698 % |
c ==============================================================================
c Found solution: 62242606
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24056 |  554406  1299510 |  184802   23341  1064546    45.6 |  3.698 % |
c ==============================================================================
c Found solution: 62227456
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24064 |  554420  1299552 |  184806   23349  1065485    45.6 |  3.698 % |
c ==============================================================================
c Found solution: 61803904
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24109 |  554437  1299595 |  184812   23394  1073902    45.9 |  3.698 % |
c |     24209 |  554437  1299595 |  203293   23494  1080333    46.0 |  3.699 % |
c |     24359 |  554437  1299595 |  223622   23644  1085303    45.9 |  3.699 % |
c |     24585 |  554437  1299595 |  245984   23870  1090840    45.7 |  3.699 % |
c |     24922 |  554437  1299595 |  270583   24207  1126010    46.5 |  3.699 % |
c |     25429 |  554437  1299595 |  297641   24714  1143562    46.3 |  3.699 % |
c |     26188 |  554437  1299595 |  327405   25473  1189554    46.7 |  3.699 % |
c ==============================================================================
c Found solution: 61163008
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26618 |  554456  1299640 |  184818   25903  1208767    46.7 |  3.699 % |
c |     26718 |  554456  1299640 |  203299   26003  1211182    46.6 |  3.699 % |
c |     26868 |  554456  1299640 |  223629   26153  1216316    46.5 |  3.699 % |
c |     27097 |  554456  1299640 |  245992   26382  1226946    46.5 |  3.699 % |
c |     27434 |  554456  1299640 |  270592   26719  1256775    47.0 |  3.699 % |
c ==============================================================================
c Found solution: 61074176
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27834 |  554469  1299675 |  184823   27119  1270285    46.8 |  3.699 % |
c |     27937 |  554469  1299675 |  203305   27222  1273811    46.8 |  3.700 % |
c |     28088 |  554469  1299675 |  223635   27373  1277562    46.7 |  3.700 % |
c |     28313 |  554469  1299675 |  245999   27598  1281403    46.4 |  3.700 % |
c |     28650 |  554368  1299448 |  270599   27338  1282042    46.9 |  3.716 % |
c |     29157 |  554368  1299448 |  297659   27845  1311748    47.1 |  3.716 % |
c |     29916 |  554368  1299448 |  327425   28604  1384699    48.4 |  3.716 % |
c |     31056 |  554270  1299227 |  360167   28464  1403177    49.3 |  3.736 % |
c ==============================================================================
c Found solution: 60755072
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31220 |  554285  1299261 |  184761   28628  1411761    49.3 |  3.736 % |
c |     31322 |  554285  1299261 |  203237   28730  1418292    49.4 |  3.737 % |
c |     31473 |  554285  1299261 |  223560   28881  1422836    49.3 |  3.737 % |
c |     31698 |  554285  1299261 |  245916   29106  1431324    49.2 |  3.737 % |
c |     32035 |  554278  1299246 |  270508   29441  1440465    48.9 |  3.738 % |
c |     32541 |  554278  1299246 |  297559   29947  1458101    48.7 |  3.738 % |
c |     33300 |  554278  1299246 |  327315   30706  1493978    48.7 |  3.738 % |
c |     34440 |  554078  1298787 |  360046   31691  1539085    48.6 |  3.771 % |
c ==============================================================================
c Found solution: 60662144
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35760 |  554090  1298817 |  184696   33011  1588723    48.1 |  3.771 % |
c |     35862 |  554090  1298817 |  203165   33113  1591007    48.0 |  3.771 % |
c |     36012 |  554090  1298817 |  223482   33263  1597886    48.0 |  3.771 % |
c |     36238 |  554090  1298817 |  245830   33489  1605823    48.0 |  3.771 % |
c |     36575 |  554090  1298817 |  270413   33826  1614991    47.7 |  3.771 % |
c |     37081 |  554080  1298795 |  297454   34330  1637375    47.7 |  3.772 % |
c |     37840 |  554080  1298795 |  327200   35089  1664108    47.4 |  3.772 % |
c |     38980 |  554080  1298795 |  359920   36229  1727605    47.7 |  3.773 % |
c |     40688 |  554080  1298795 |  395912   37937  1878610    49.5 |  3.772 % |
c |     43254 |  554032  1298686 |  435503   40502  2026738    50.0 |  3.784 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v I_0x2e_001_0x2e__0x2e__0x2e__bit0 -I_0x2e_001003_bit0 -I_0x2e_002003_bit0 -I_0x2e_002_0x2e__0x2e__0x2e__bit0 -I_0x2e_003005_bit0 I_0x2e_004005_bit0 -I_0x2e_004_0x2e__0x2e__0x2e__bit0 I_0x2e_005007_bit0 I_0x2e_006007_bit0 I_0x2e_007008_bit0 I_0x2e_008_0x2e__0x2e__0x2e__bit0 -I_0x2e_008009_bit0 I_0x2e_010012_bit0 I_0x2e_011012_bit0 -I_0x2e_012_0x2e__0x2e__0x2e__bit0 I_0x2e_012013_bit0 I_0x2e_013016_bit0 -I_0x2e_014015_bit0 I_0x2e_015016_bit0 I_0x2e_016_0x2e__0x2e__0x2e__bit0 -I_0x2e_016017_bit0 -I_0x2e_017018_bit0 -I_0x2e_009018_bit0 -I_0x2e_018019_bit0 I_0x2e_019024_bit0 -I_0x2e_024_0x2e__0x2e__0x2e__bit0 -I_0x2e_023024_bit0 -I_0x2e_022023_bit0 -I_0x2e_020022_bit0 I_0x2e_021022_bit0 I_0x2e_022_0x2e__0x2e__0x2e__bit0 I_0x2e_024026_bit0 I_0x2e_025026_bit0 -I_0x2e_025_0x2e__0x2e__0x2e__bit0 I_0x2e_026027_bit0 I_0x2e_027_0x2e__0x2e__0x2e__bit0 -I_0x2e_027032_bit0 -I_0x2e_030031_bit0 I_0x2e_031032_bit0 I_0x2e_029031_bit0 -I_0x2e_028029_bit0 -I_0x2e_028_0x2e__0x2e__0x2e__bit0 I_0x2e_032033_bit0 I_0x2e_033037_bit0 -I_0x2e_036037_bit0 -I_0x2e_034036_bit0 -I_0x2e_035036_bit0 I_0x2e_037038_bit0 I_0x2e_038040_bit0 I_0x2e_039040_bit0 -I_0x2e_040_0x2e__0x2e__0x2e__bit0 -I_0x2e_041_0x2e__0x2e__0x2e__bit0 I_0x2e_040041_bit0 I_0x2e_041042_bit0 I_0x2e_042_0x2e__0x2e__0x2e__bit0 -F_0x2e_001_0x2e__0x2e__0x2e__bit_7 -F_0x2e_001_0x2e__0x2e__0x2e__bit_6 -F_0x2e_001_0x2e__0x2e__0x2e__bit_5 -F_0x2e_001_0x2e__0x2e__0x2e__bit_4 -F_0x2e_001_0x2e__0x2e__0x2e__bit_3 -F_0x2e_001_0x2e__0x2e__0x2e__bit_2 -F_0x2e_001_0x2e__0x2e__0x2e__bit_1 -F_0x2e_001_0x2e__0x2e__0x2e__bit0 F_0x2e_001_0x2e__0x2e__0x2e__bit1 -F_0x2e_001_0x2e__0x2e__0x2e__bit2 -F_0x2e_001_0x2e__0x2e__0x2e__bit3 -F_0x2e_001_0x2e__0x2e__0x2e__bit4 -F_0x2e_001_0x2e__0x2e__0x2e__bit5 -F_0x2e_001_0x2e__0x2e__0x2e__bit6 -F_0x2e_001_0x2e__0x2e__0x2e__bit7 -F_0x2e_001_0x2e__0x2e__0x2e__bit8 -F_0x2e_001_0x2e__0x2e__0x2e__bit9 -F_0x2e_001_0x2e__0x2e__0x2e__bit10 -F_0x2e_001_0x2e__0x2e__0x2e__bit11 -F_0x2e_001_0x2e__0x2e__0x2e__bit12 -F_0x2e_001003_bit_7 -F_0x2e_001003_bit_6 -F_0x2e_001003_bit_5 -F_0x2e_001003_bit_4 -F_0x2e_001003_bit_3 -F_0x2e_001003_bit_2 -F_0x2e_001003_bit_1 -F_0x2e_001003_bit0 -F_0x2e_001003_bit1 -F_0x2e_001003_bit2 -F_0x2e_001003_bit3 -F_0x2e_001003_bit4 -F_0x2e_001003_bit5 -F_0x2e_001003_bit6 -F_0x2e_001003_bit7 -F_0x2e_001003_bit8 -F_0x2e_001003_bit9 -F_0x2e_001003_bit10 -F_0x2e_001003_bit11 -F_0x2e_001003_bit12 -F_0x2e_002003_bit_7 -F_0x2e_002003_bit_6 -F_0x2e_002003_bit_5 -F_0x2e_002003_bit_4 -F_0x2e_002003_bit_3 -F_0x2e_002003_bit_2 -F_0x2e_002003_bit_1 -F_0x2e_002003_bit0 -F_0x2e_002003_bit1 -F_0x2e_002003_bit2 -F_0x2e_002003_bit3 -F_0x2e_002003_bit4 -F_0x2e_002003_bit5 -F_0x2e_002003_bit6 -F_0x2e_002003_bit7 -F_0x2e_002003_bit8 -F_0x2e_002003_bit9 -F_0x2e_002003_bit10 -F_0x2e_002003_bit11 -F_0x2e_002003_bit12 -F_0x2e_002_0x2e__0x2e__0x2e__bit_7 -F_0x2e_002_0x2e__0x2e__0x2e__bit_6 -F_0x2e_002_0x2e__0x2e__0x2e__bit_5 -F_0x2e_002_0x2e__0x2e__0x2e__bit_4 -F_0x2e_002_0x2e__0x2e__0x2e__bit_3 -F_0x2e_002_0x2e__0x2e__0x2e__bit_2 -F_0x2e_002_0x2e__0x2e__0x2e__bit_1 -F_0x2e_002_0x2e__0x2e__0x2e__bit0 -F_0x2e_002_0x2e__0x2e__0x2e__bit1 -F_0x2e_002_0x2e__0x2e__0x2e__bit2 -F_0x2e_002_0x2e__0x2e__0x2e__bit3 -F_0x2e_002_0x2e__0x2e__0x2e__bit4 -F_0x2e_002_0x2e__0x2e__0x2e__bit5 -F_0x2e_002_0x2e__0x2e__0x2e__bit6 -F_0x2e_002_0x2e__0x2e__0x2e__bit7 -F_0x2e_002_0x2e__0x2e__0x2e__bit8 -F_0x2e_002_0x2e__0x2e__0x2e__bit9 -F_0x2e_002_0x2e__0x2e__0x2e__bit10 -F_0x2e_002_0x2e__0x2e__0x2e__bit11 -F_0x2e_002_0x2e__0x2e__0x2e__bit12 -F_0x2e_003005_bit_7 -F_0x2e_003005_bit_6 -F_0x2e_003005_bit_5 -F_0x2e_003005_bit_4 -F_0x2e_003005_bit_3 -F_0x2e_003005_bit_2 -F_0x2e_003005_bit_1 -F_0x2e_003005_bit0 -F_0x2e_003005_bit1 -F_0x2e_003005_bit2 -F_0x2e_003005_bit3 -F_0x2e_003005_bit4 -F_0x2e_003005_bit5 -F_0x2e_003005_bit6 -F_0x2e_003005_bit7 -F_0x2e_003005_bit8 -F_0x2e_003005_bit9 -F_0x2e_003005_bit10 -F_0x2e_003005_bit11 -F_0x2e_003005_bit12 -F_0x2e_004005_bit_7 -F_0x2e_004005_bit_6 -F_0x2e_004005_bit_5 -F_0x2e_004005_bit_4 -F_0x2e_004005_bit_3 -F_0x2e_004005_bit_2 -F_0x2e_004005_bit_1 F_0x2e_004005_bit0 F_0x2e_004005_bit1 F_0x2e_004005_bit2 -F_0x2e_004005_bit3 -F_0x2e_004005_bit4 -F_0x2e_004005_bit5 -F_0x2e_004005_bit6 -F_0x2e_004005_bit7 -F_0x2e_004005_bit8 -F_0x2e_004005_bit9 -F_0x2e_004005_bit10 -F_0x2e_004005_bit11 -F_0x2e_004005_bit12 -F_0x2e_004_0x2e__0x2e__0x2e__bit_7 -F_0x2e_004_0x2e__0x2e__0x2e__bit_6 -F_0x2e_004_0x2e__0x2e__0x2e__bit_5 -F_0x2e_004_0x2e__0x2e__0x2e__bit_4 -F_0x2e_004_0x2e__0x2e__0x2e__bit_3 -F_0x2e_004_0x2e__0x2e__0x2e__bit_2 -F_0x2e_004_0x2e__0x2e__0x2e__bit_1 -F_0x2e_004_0x2e__0x2e__0x2e__bit0 -F_0x2e_004_0x2e__0x2e__0x2e__bit1 -F_0x2e_004_0x2e__0x2e__0x2e__bit2 -F_0x2e_004_0x2e__0x2e__0x2e__bit3 -F_0x2e_004_0x2e__0x2e__0x2e__bit4 -F_0x2e_004_0x2e__0x2e__0x2e__bit5 -F_0x2e_004_0x2e__0x2e__0x2e__bit6 -F_0x2e_004_0x2e__0x2e__0x2e__bit7 -F_0x2e_004_0x2e__0x2e__0x2e__bit8 -F_0x2e_004_0x2e__0x2e__0x2e__bit9 -F_0x2e_004_0x2e__0x2e__0x2e__bit10 -F_0x2e_004_0x2e__0x2e__0x2e__bit11 -F_0x2e_004_0x2e__0x2e__0x2e__bit12 -F_0x2e_005007_bit_7 -F_0x2e_005007_bit_6 -F_0x2e_005007_bit_5 -F_0x2e_005007_bit_4 -F_0x2e_005007_bit_3 -F_0x2e_005007_bit_2 -F_0x2e_005007_bit_1 F_0x2e_005007_bit0 F_0x2e_005007_bit1 F_0x2e_005007_bit2 -F_0x2e_005007_bit3 -F_0x2e_005007_bit4 -F_0x2e_005007_bit5 -F_0x2e_005007_bit6 -F_0x2e_005007_bit7 -F_0x2e_005007_bit8 -F_0x2e_005007_bit9 -F_0x2e_005007_bit10 -F_0x2e_005007_bit11 -F_0x2e_005007_bit12 -F_0x2e_006007_bit_7 -F_0x2e_006007_bit_6 -F_0x2e_006007_bit_5 -F_0x2e_006007_bit_4 -F_0x2e_006007_bit_3 -F_0x2e_006007_bit_2 -F_0x2e_006007_bit_1 -F_0x2e_006007_bit0 -F_0x2e_006007_bit1 F_0x2e_006007_bit2 -F_0x2e_006007_bit3 -F_0x2e_006007_bit4 -F_0x2e_006007_bit5 -F_0x2e_006007_bit6 -F_0x2e_006007_bit7 -F_0x2e_006007_bit8 -F_0x2e_006007_bit9 -F_0x2e_006007_bit10 -F_0x2e_006007_bit11 -F_0x2e_006007_bit12 -F_0x2e_007008_bit_7 -F_0x2e_007008_bit_6 -F_0x2e_007008_bit_5 -F_0x2e_007008_bit_4 -F_0x2e_007008_bit_3 -F_0x2e_007008_bit_2 -F_0x2e_007008_bit_1 -F_0x2e_007008_bit0 -F_0x2e_007008_bit1 F_0x2e_007008_bit2 F_0x2e_007008_bit3 -F_0x2e_007008_bit4 -F_0x2e_007008_bit5 -F_0x2e_007008_bit6 -F_0x2e_007008_bit7 -F_0x2e_007008_bit8 -F_0x2e_007008_bit9 -F_0x2e_007008_bit10 -F_0x2e_007008_bit11 -F_0x2e_007008_bit12 -F_0x2e_008_0x2e__0x2e__0x2e__bit_7 -F_0x2e_008_0x2e__0x2e__0x2e__bit_6 -F_0x2e_008_0x2e__0x2e__0x2e__bit_5 -F_0x2e_008_0x2e__0x2e__0x2e__bit_4 -F_0x2e_008_0x2e__0x2e__0x2e__bit_3 -F_0x2e_008_0x2e__0x2e__0x2e__bit_2 -F_0x2e_008_0x2e__0x2e__0x2e__bit_1 -F_0x2e_008_0x2e__0x2e__0x2e__bit0 -F_0x2e_008_0x2e__0x2e__0x2e__bit1 F_0x2e_008_0x2e__0x2e__0x2e__bit2 F_0x2e_008_0x2e__0x2e__0x2e__bit3 -F_0x2e_008_0x2e__0x2e__0x2e__bit4 -F_0x2e_008_0x2e__0x2e__0x2e__bit5 -F_0x2e_008_0x2e__0x2e__0x2e__bit6 -F_0x2e_008_0x2e__0x2e__0x2e__bit7 -F_0x2e_008_0x2e__0x2e__0x2e__bit8 -F_0x2e_008_0x2e__0x2e__0x2e__bit9 -F_0x2e_008_0x2e__0x2e__0x2e__bit10 -F_0x2e_008_0x2e__0x2e__0x2e__bit11 -F_0x2e_008_0x2e__0x2e__0x2e__bit12 -F_0x2e_008009_bit_7 -F_0x2e_008009_bit_6 -F_0x2e_008009_bit_5 -F_0x2e_008009_bit_4 -F_0x2e_008009_bit_3 -F_0x2e_008009_bit_2 -F_0x2e_008009_bit_1 -F_0x2e_008009_bit0 -F_0x2e_008009_bit1 -F_0x2e_008009_bit2 -F_0x2e_008009_bit3 -F_0x2e_008009_bit4 -F_0x2e_008009_bit5 -F_0x2e_008009_bit6 -F_0x2e_008009_bit7 -F_0x2e_008009_bit8 -F_0x2e_008009_bit9 -F_0x2e_008009_bit10 -F_0x2e_008009_bit11 -F_0x2e_008009_bit12 -F_0x2e_010012_bit_7 -F_0x2e_010012_bit_6 -F_0x2e_010012_bit_5 -F_0x2e_010012_bit_4 -F_0x2e_010012_bit_3 -F_0x2e_010012_bit_2 -F_0x2e_010012_bit_1 F_0x2e_010012_bit0 -F_0x2e_010012_bit1 -F_0x2e_010012_bit2 -F_0x2e_010012_bit3 -F_0x2e_010012_bit4 -F_0x2e_010012_bit5 -F_0x2e_010012_bit6 -F_0x2e_010012_bit7 -F_0x2e_010012_bit8 -F_0x2e_010012_bit9 -F_0x2e_010012_bit10 -F_0x2e_010012_bit11 -F_0x2e_010012_bit12 -F_0x2e_012_0x2e__0x2e__0x2e__bit_7 -F_0x2e_012_0x2e__0x2e__0x2e__bit_6 -F_0x2e_012_0x2e__0x2e__0x2e__bit_5 -F_0x2e_012_0x2e__0x2e__0x2e__bit_4 -F_0x2e_012_0x2e__0x2e__0x2e__bit_3 -F_0x2e_012_0x2e__0x2e__0x2e__bit_2 -F_0x2e_012_0x2e__0x2e__0x2e__bit_1 -F_0x2e_012_0x2e__0x2e__0x2e__bit0 -F_0x2e_012_0x2e__0x2e__0x2e__bit1 -F_0x2e_012_0x2e__0x2e__0x2e__bit2 -F_0x2e_012_0x2e__0x2e__0x2e__bit3 -F_0x2e_012_0x2e__0x2e__0x2e__bit4 -F_0x2e_012_0x2e__0x2e__0x2e__bit5 -F_0x2e_012_0x2e__0x2e__0x2e__bit6 -F_0x2e_012_0x2e__0x2e__0x2e__bit7 -F_0x2e_012_0x2e__0x2e__0x2e__bit8 -F_0x2e_012_0x2e__0x2e__0x2e__bit9 -F_0x2e_012_0x2e__0x2e__0x2e__bit10 -F_0x2e_012_0x2e__0x2e__0x2e__bit11 -F_0x2e_012_0x2e__0x2e__0x2e__bit12 -F_0x2e_012013_bit_7 -F_0x2e_012013_bit_6 -F_0x2e_012013_bit_5 -F_0x2e_012013_bit_4 -F_0x2e_012013_bit_3 -F_0x2e_012013_bit_2 -F_0x2e_012013_bit_1 -F_0x2e_012013_bit0 F_0x2e_012013_bit1 F_0x2e_012013_bit2 -F_0x2e_012013_bit3 F_0x2e_012013_bit4 -F_0x2e_012013_bit5 -F_0x2e_012013_bit6 -F_0x2e_012013_bit7 -F_0x2e_012013_bit8 -F_0x2e_012013_bit9 -F_0x2e_012013_bit10 -F_0x2e_012013_bit11 -F_0x2e_012013_bit12 -F_0x2e_013016_bit_7 -F_0x2e_013016_bit_6 -F_0x2e_013016_bit_5 -F_0x2e_013016_bit_4 -F_0x2e_013016_bit_3 -F_0x2e_013016_bit_2 -F_0x2e_013016_bit_1 -F_0x2e_013016_bit0 F_0x2e_013016_bit1 -F_0x2e_013016_bit2 F_0x2e_013016_bit3 F_0x2e_013016_bit4 -F_0x2e_013016_bit5 -F_0x2e_013016_bit6 -F_0x2e_013016_bit7 -F_0x2e_013016_bit8 -F_0x2e_013016_bit9 -F_0x2e_013016_bit10 -F_0x2e_013016_bit11 -F_0x2e_013016_bit12 -F_0x2e_014015_bit_7 -F_0x2e_014015_bit_6 -F_0x2e_014015_bit_5 -F_0x2e_014015_bit_4 -F_0x2e_014015_bit_3 -F_0x2e_014015_bit_2 -F_0x2e_014015_bit_1 -F_0x2e_014015_bit0 -F_0x2e_014015_bit1 -F_0x2e_014015_bit2 -F_0x2e_014015_bit3 -F_0x2e_014015_bit4 -F_0x2e_014015_bit5 -F_0x2e_014015_bit6 -F_0x2e_014015_bit7 -F_0x2e_014015_bit8 -F_0x2e_014015_bit9 -F_0x2e_014015_bit10 -F_0x2e_014015_bit11 -F_0x2e_014015_bit12 -F_0x2e_015016_bit_7 -F_0x2e_015016_bit_6 -F_0x2e_015016_bit_5 -F_0x2e_015016_bit_4 -F_0x2e_015016_bit_3 -F_0x2e_015016_bit_2 -F_0x2e_015016_bit_1 F_0x2e_015016_bit0 -F_0x2e_015016_bit1 -F_0x2e_015016_bit2 -F_0x2e_015016_bit3 -F_0x2e_015016_bit4 -F_0x2e_015016_bit5 -F_0x2e_015016_bit6 -F_0x2e_015016_bit7 -F_0x2e_015016_bit8 -F_0x2e_015016_bit9 -F_0x2e_015016_bit10 -F_0x2e_015016_bit11 -F_0x2e_015016_bit12 -F_0x2e_016_0x2e__0x2e__0x2e__bit_7 -F_0x2e_016_0x2e__0x2e__0x2e__bit_6 -F_0x2e_016_0x2e__0x2e__0x2e__bit_5 -F_0x2e_016_0x2e__0x2e__0x2e__bit_4 -F_0x2e_016_0x2e__0x2e__0x2e__bit_3 -F_0x2e_016_0x2e__0x2e__0x2e__bit_2 -F_0x2e_016_0x2e__0x2e__0x2e__bit_1 F_0x2e_016_0x2e__0x2e__0x2e__bit0 F_0x2e_016_0x2e__0x2e__0x2e__bit1 -F_0x2e_016_0x2e__0x2e__0x2e__bit2 F_0x2e_016_0x2e__0x2e__0x2e__bit3 F_0x2e_016_0x2e__0x2e__0x2e__bit4 -F_0x2e_016_0x2e__0x2e__0x2e__bit5 -F_0x2e_016_0x2e__0x2e__0x2e__bit6 -F_0x2e_016_0x2e__0x2e__0x2e__bit7 -F_0x2e_016_0x2e__0x2e__0x2e__bit8 -F_0x2e_016_0x2e__0x2e__0x2e__bit9 -F_0x2e_016_0x2e__0x2e__0x2e__bit10 -F_0x2e_016_0x2e__0x2e__0x2e__bit11 -F_0x2e_016_0x2e__0x2e__0x2e__bit12 -F_0x2e_016017_bit_7 -F_0x2e_016017_bit_6 -F_0x2e_016017_bit_5 -F_0x2e_016017_bit_4 -F_0x2e_016017_bit_3 -F_0x2e_016017_bit_2 -F_0x2e_016017_bit_1 -F_0x2e_016017_bit0 -F_0x2e_016017_bit1 -F_0x2e_016017_bit2 -F_0x2e_016017_bit3 -F_0x2e_016017_bit4 -F_0x2e_016017_bit5 -F_0x2e_016017_bit6 -F_0x2e_016017_bit7 -F_0x2e_016017_bit8 -F_0x2e_016017_bit9 -F_0x2e_016017_bit10 -F_0x2e_016017_bit11 -F_0x2e_016017_bit12 -F_0x2e_017018_bit_7 -F_0x2e_017018_bit_6 -F_0x2e_017018_bit_5 -F_0x2e_017018_bit_4 -F_0x2e_017018_bit_3 -F_0x2e_017018_bit_2 -F_0x2e_017018_bit_1 -F_0x2e_017018_bit0 -F_0x2e_017018_bit1 -F_0x2e_017018_bit2 -F_0x2e_017018_bit3 -F_0x2e_017018_bit4 -F_0x2e_017018_bit5 -F_0x2e_017018_bit6 -F_0x2e_017018_bit7 -F_0x2e_017018_bit8 -F_0x2e_017018_bit9 -F_0x2e_017018_bit10 -F_0x2e_017018_bit11 -F_0x2e_017018_bit12 -F_0x2e_009018_bit_7 -F_0x2e_009018_bit_6 -F_0x2e_009018_bit_5 -F_0x2e_009018_bit_4 -F_0x2e_009018_bit_3 -F_0x2e_009018_bit_2 -F_0x2e_009018_bit_1 -F_0x2e_009018_bit0 -F_0x2e_009018_bit1 -F_0x2e_009018_bit2 -F_0x2e_009018_bit3 -F_0x2e_009018_bit4 -F_0x2e_009018_bit5 -F_0x2e_009018_bit6 -F_0x2e_009018_bit7 -F_0x2e_009018_bit8 -F_0x2e_009018_bit9 -F_0x2e_009018_bit10 -F_0x2e_009018_bit11 -F_0x2e_009018_bit12 -F_0x2e_018019_bit_7 -F_0x2e_018019_bit_6 -F_0x2e_018019_bit_5 -F_0x2e_018019_bit_4 -F_0x2e_018019_bit_3 -F_0x2e_018019_bit_2 -F_0x2e_018019_bit_1 -F_0x2e_018019_bit0 -F_0x2e_018019_bit1 -F_0x2e_018019_bit2 -F_0x2e_018019_bit3 -F_0x2e_018019_bit4 -F_0x2e_018019_bit5 -F_0x2e_018019_bit6 -F_0x2e_018019_bit7 -F_0x2e_018019_bit8 -F_0x2e_018019_bit9 -F_0x2e_018019_bit10 -F_0x2e_018019_bit11 -F_0x2e_018019_bit12 -F_0x2e_019024_bit_7 -F_0x2e_019024_bit_6 -F_0x2e_019024_bit_5 -F_0x2e_019024_bit_4 -F_0x2e_019024_bit_3 -F_0x2e_019024_bit_2 -F_0x2e_019024_bit_1 -F_0x2e_019024_bit0 F_0x2e_019024_bit1 -F_0x2e_019024_bit2 -F_0x2e_019024_bit3 -F_0x2e_019024_bit4 -F_0x2e_019024_bit5 -F_0x2e_019024_bit6 -F_0x2e_019024_bit7 -F_0x2e_019024_bit8 -F_0x2e_019024_bit9 -F_0x2e_019024_bit10 -F_0x2e_019024_bit11 -F_0x2e_019024_bit12 -F_0x2e_024_0x2e__0x2e__0x2e__bit_7 -F_0x2e_024_0x2e__0x2e__0x2e__bit_6 -F_0x2e_024_0x2e__0x2e__0x2e__bit_5 -F_0x2e_024_0x2e__0x2e__0x2e__bit_4 -F_0x2e_024_0x2e__0x2e__0x2e__bit_3 -F_0x2e_024_0x2e__0x2e__0x2e__bit_2 -F_0x2e_024_0x2e__0x2e__0x2e__bit_1 -F_0x2e_024_0x2e__0x2e__0x2e__bit0 -F_0x2e_024_0x2e__0x2e__0x2e__bit1 -F_0x2e_024_0x2e__0x2e__0x2e__bit2 -F_0x2e_024_0x2e__0x2e__0x2e__bit3 -F_0x2e_024_0x2e__0x2e__0x2e__bit4 -F_0x2e_024_0x2e__0x2e__0x2e__bit5 -F_0x2e_024_0x2e__0x2e__0x2e__bit6 -F_0x2e_024_0x2e__0x2e__0x2e__bit7 -F_0x2e_024_0x2e__0x2e__0x2e__bit8 -F_0x2e_024_0x2e__0x2e__0x2e__bit9 -F_0x2e_024_0x2e__0x2e__0x2e__bit10 -F_0x2e_024_0x2e__0x2e__0x2e__bit11 -F_0x2e_024_0x2e__0x2e__0x2e__bit12 -F_0x2e_023024_bit_7 -F_0x2e_023024_bit_6 -F_0x2e_023024_bit_5 -F_0x2e_023024_bit_4 -F_0x2e_023024_bit_3 -F_0x2e_023024_bit_2 -F_0x2e_023024_bit_1 -F_0x2e_023024_bit0 -F_0x2e_023024_bit1 -F_0x2e_023024_bit2 -F_0x2e_023024_bit3 -F_0x2e_023024_bit4 -F_0x2e_023024_bit5 -F_0x2e_023024_bit6 -F_0x2e_023024_bit7 -F_0x2e_023024_bit8 -F_0x2e_023024_bit9 -F_0x2e_023024_bit10 -F_0x2e_023024_bit11 -F_0x2e_023024_bit12 -F_0x2e_022023_bit_7 -F_0x2e_022023_bit_6 -F_0x2e_022023_bit_5 -F_0x2e_022023_bit_4 -F_0x2e_022023_bit_3 -F_0x2e_022023_bit_2 -F_0x2e_022023_bit_1 -F_0x2e_022023_bit0 -F_0x2e_022023_bit1 -F_0x2e_022023_bit2 -F_0x2e_022023_bit3 -F_0x2e_022023_bit4 -F_0x2e_022023_bit5 -F_0x2e_022023_bit6 -F_0x2e_022023_bit7 -F_0x2e_022023_bit8 -F_0x2e_022023_bit9 -F_0x2e_022023_bit10 -F_0x2e_022023_bit11 -F_0x2e_022023_bit12 -F_0x2e_020022_bit_7 -F_0x2e_020022_bit_6 -F_0x2e_020022_bit_5 -F_0x2e_020022_bit_4 -F_0x2e_020022_bit_3 -F_0x2e_020022_bit_2 -F_0x2e_020022_bit_1 -F_0x2e_020022_bit0 -F_0x2e_020022_bit1 -F_0x2e_020022_bit2 -F_0x2e_020022_bit3 -F_0x2e_020022_bit4 -F_0x2e_020022_bit5 -F_0x2e_020022_bit6 -F_0x2e_020022_bit7 -F_0x2e_020022_bit8 -F_0x2e_020022_bit9 -F_0x2e_020022_bit10 -F_0x2e_020022_bit11 -F_0x2e_020022_bit12 -F_0x2e_021022_bit_7 -F_0x2e_021022_bit_6 -F_0x2e_021022_bit_5 -F_0x2e_021022_bit_4 -F_0x2e_021022_bit_3 -F_0x2e_021022_bit_2 -F_0x2e_021022_bit_1 F_0x2e_021022_bit0 F_0x2e_021022_bit1 F_0x2e_021022_bit2 -F_0x2e_021022_bit3 -F_0x2e_021022_bit4 -F_0x2e_021022_bit5 -F_0x2e_021022_bit6 -F_0x2e_021022_bit7 -F_0x2e_021022_bit8 -F_0x2e_021022_bit9 -F_0x2e_021022_bit10 -F_0x2e_021022_bit11 -F_0x2e_021022_bit12 -F_0x2e_022_0x2e__0x2e__0x2e__bit_7 -F_0x2e_022_0x2e__0x2e__0x2e__bit_6 -F_0x2e_022_0x2e__0x2e__0x2e__bit_5 -F_0x2e_022_0x2e__0x2e__0x2e__bit_4 -F_0x2e_022_0x2e__0x2e__0x2e__bit_3 -F_0x2e_022_0x2e__0x2e__0x2e__bit_2 -F_0x2e_022_0x2e__0x2e__0x2e__bit_1 F_0x2e_022_0x2e__0x2e__0x2e__bit0 F_0x2e_022_0x2e__0x2e__0x2e__bit1 F_0x2e_022_0x2e__0x2e__0x2e__bit2 -F_0x2e_022_0x2e__0x2e__0x2e__bit3 -F_0x2e_022_0x2e__0x2e__0x2e__bit4 -F_0x2e_022_0x2e__0x2e__0x2e__bit5 -F_0x2e_022_0x2e__0x2e__0x2e__bit6 -F_0x2e_022_0x2e__0x2e__0x2e__bit7 -F_0x2e_022_0x2e__0x2e__0x2e__bit8 -F_0x2e_022_0x2e__0x2e__0x2e__bit9 -F_0x2e_022_0x2e__0x2e__0x2e__bit10 -F_0x2e_022_0x2e__0x2e__0x2e__bit11 -F_0x2e_022_0x2e__0x2e__0x2e__bit12 -F_0x2e_024026_bit_7 -F_0x2e_024026_bit_6 -F_0x2e_024026_bit_5 -F_0x2e_024026_bit_4 -F_0x2e_024026_bit_3 -F_0x2e_024026_bit_2 -F_0x2e_024026_bit_1 -F_0x2e_024026_bit0 F_0x2e_024026_bit1 -F_0x2e_024026_bit2 -F_0x2e_024026_bit3 -F_0x2e_024026_bit4 -F_0x2e_024026_bit5 -F_0x2e_024026_bit6 -F_0x2e_024026_bit7 -F_0x2e_024026_bit8 -F_0x2e_024026_bit9 -F_0x2e_024026_bit10 -F_0x2e_024026_bit11 -F_0x2e_024026_bit12 -F_0x2e_025026_bit_7 -F_0x2e_025026_bit_6 -F_0x2e_025026_bit_5 -F_0x2e_025026_bit_4 -F_0x2e_025026_bit_3 -F_0x2e_025026_bit_2 -F_0x2e_025026_bit_1 F_0x2e_025026_bit0 F_0x2e_025026_bit1 -F_0x2e_025026_bit2 -F_0x2e_025026_bit3 F_0x2e_025026_bit4 -F_0x2e_025026_bit5 -F_0x2e_025026_bit6 -F_0x2e_025026_bit7 -F_0x2e_025026_bit8 -F_0x2e_025026_bit9 -F_0x2e_025026_bit10 -F_0x2e_025026_bit11 -F_0x2e_025026_bit12 -F_0x2e_025_0x2e__0x2e__0x2e__bit_7 -F_0x2e_025_0x2e__0x2e__0x2e__bit_6 -F_0x2e_025_0x2e__0x2e__0x2e__bit_5 -F_0x2e_025_0x2e__0x2e__0x2e__bit_4 -F_0x2e_025_0x2e__0x2e__0x2e__bit_3 -F_0x2e_025_0x2e__0x2e__0x2e__bit_2 -F_0x2e_025_0x2e__0x2e__0x2e__bit_1 -F_0x2e_025_0x2e__0x2e__0x2e__bit0 -F_0x2e_025_0x2e__0x2e__0x2e__bit1 -F_0x2e_025_0x2e__0x2e__0x2e__bit2 -F_0x2e_025_0x2e__0x2e__0x2e__bit3 -F_0x2e_025_0x2e__0x2e__0x2e__bit4 -F_0x2e_025_0x2e__0x2e__0x2e__bit5 -F_0x2e_025_0x2e__0x2e__0x2e__bit6 -F_0x2e_025_0x2e__0x2e__0x2e__bit7 -F_0x2e_025_0x2e__0x2e__0x2e__bit8 -F_0x2e_025_0x2e__0x2e__0x2e__bit9 -F_0x2e_025_0x2e__0x2e__0x2e__bit10 -F_0x2e_025_0x2e__0x2e__0x2e__bit11 -F_0x2e_025_0x2e__0x2e__0x2e__bit12 -F_0x2e_026027_bit_7 -F_0x2e_026027_bit_6 -F_0x2e_026027_bit_5 -F_0x2e_026027_bit_4 -F_0x2e_026027_bit_3 -F_0x2e_026027_bit_2 -F_0x2e_026027_bit_1 F_0x2e_026027_bit0 F_0x2e_026027_bit1 F_0x2e_026027_bit2 F_0x2e_026027_bit3 F_0x2e_026027_bit4 -F_0x2e_026027_bit5 -F_0x2e_026027_bit6 -F_0x2e_026027_bit7 -F_0x2e_026027_bit8 -F_0x2e_026027_bit9 -F_0x2e_026027_bit10 -F_0x2e_026027_bit11 -F_0x2e_026027_bit12 -F_0x2e_027_0x2e__0x2e__0x2e__bit_7 -F_0x2e_027_0x2e__0x2e__0x2e__bit_6 -F_0x2e_027_0x2e__0x2e__0x2e__bit_5 -F_0x2e_027_0x2e__0x2e__0x2e__bit_4 -F_0x2e_027_0x2e__0x2e__0x2e__bit_3 -F_0x2e_027_0x2e__0x2e__0x2e__bit_2 -F_0x2e_027_0x2e__0x2e__0x2e__bit_1 F_0x2e_027_0x2e__0x2e__0x2e__bit0 F_0x2e_027_0x2e__0x2e__0x2e__bit1 F_0x2e_027_0x2e__0x2e__0x2e__bit2 F_0x2e_027_0x2e__0x2e__0x2e__bit3 F_0x2e_027_0x2e__0x2e__0x2e__bit4 -F_0x2e_027_0x2e__0x2e__0x2e__bit5 -F_0x2e_027_0x2e__0x2e__0x2e__bit6 -F_0x2e_027_0x2e__0x2e__0x2e__bit7 -F_0x2e_027_0x2e__0x2e__0x2e__bit8 -F_0x2e_027_0x2e__0x2e__0x2e__bit9 -F_0x2e_027_0x2e__0x2e__0x2e__bit10 -F_0x2e_027_0x2e__0x2e__0x2e__bit11 -F_0x2e_027_0x2e__0x2e__0x2e__bit12 -F_0x2e_027032_bit_7 -F_0x2e_027032_bit_6 -F_0x2e_027032_bit_5 -F_0x2e_027032_bit_4 -F_0x2e_027032_bit_3 -F_0x2e_027032_bit_2 -F_0x2e_027032_bit_1 -F_0x2e_027032_bit0 -F_0x2e_027032_bit1 -F_0x2e_027032_bit2 -F_0x2e_027032_bit3 -F_0x2e_027032_bit4 -F_0x2e_027032_bit5 -F_0x2e_027032_bit6 -F_0x2e_027032_bit7 -F_0x2e_027032_bit8 -F_0x2e_027032_bit9 -F_0x2e_027032_bit10 -F_0x2e_027032_bit11 -F_0x2e_027032_bit12 -F_0x2e_030031_bit_7 -F_0x2e_030031_bit_6 -F_0x2e_030031_bit_5 -F_0x2e_030031_bit_4 -F_0x2e_030031_bit_3 -F_0x2e_030031_bit_2 -F_0x2e_030031_bit_1 -F_0x2e_030031_bit0 -F_0x2e_030031_bit1 -F_0x2e_030031_bit2 -F_0x2e_030031_bit3 -F_0x2e_030031_bit4 -F_0x2e_030031_bit5 -F_0x2e_030031_bit6 -F_0x2e_030031_bit7 -F_0x2e_030031_bit8 -F_0x2e_030031_bit9 -F_0x2e_030031_bit10 -F_0x2e_030031_bit11 -F_0x2e_030031_bit12 -F_0x2e_031032_bit_7 -F_0x2e_031032_bit_6 -F_0x2e_031032_bit_5 -F_0x2e_031032_bit_4 -F_0x2e_031032_bit_3 -F_0x2e_031032_bit_2 -F_0x2e_031032_bit_1 F_0x2e_031032_bit0 -F_0x2e_031032_bit1 F_0x2e_031032_bit2 -F_0x2e_031032_bit3 -F_0x2e_031032_bit4 -F_0x2e_031032_bit5 -F_0x2e_031032_bit6 -F_0x2e_031032_bit7 -F_0x2e_031032_bit8 -F_0x2e_031032_bit9 -F_0x2e_031032_bit10 -F_0x2e_031032_bit11 -F_0x2e_031032_bit12 -F_0x2e_029031_bit_7 -F_0x2e_029031_bit_6 -F_0x2e_029031_bit_5 -F_0x2e_029031_bit_4 -F_0x2e_029031_bit_3 -F_0x2e_029031_bit_2 -F_0x2e_029031_bit_1 F_0x2e_029031_bit0 -F_0x2e_029031_bit1 F_0x2e_029031_bit2 -F_0x2e_029031_bit3 -F_0x2e_029031_bit4 -F_0x2e_029031_bit5 -F_0x2e_029031_bit6 -F_0x2e_029031_bit7 -F_0x2e_029031_bit8 -F_0x2e_029031_bit9 -F_0x2e_029031_bit10 -F_0x2e_029031_bit11 -F_0x2e_029031_bit12 -F_0x2e_028029_bit_7 -F_0x2e_028029_bit_6 -F_0x2e_028029_bit_5 -F_0x2e_028029_bit_4 -F_0x2e_028029_bit_3 -F_0x2e_028029_bit_2 -F_0x2e_028029_bit_1 -F_0x2e_028029_bit0 -F_0x2e_028029_bit1 -F_0x2e_028029_bit2 -F_0x2e_028029_bit3 -F_0x2e_028029_bit4 -F_0x2e_028029_bit5 -F_0x2e_028029_bit6 -F_0x2e_028029_bit7 -F_0x2e_028029_bit8 -F_0x2e_028029_bit9 -F_0x2e_028029_bit10 -F_0x2e_028029_bit11 -F_0x2e_028029_bit12 -F_0x2e_028_0x2e__0x2e__0x2e__bit_7 -F_0x2e_028_0x2e__0x2e__0x2e__bit_6 -F_0x2e_028_0x2e__0x2e__0x2e__bit_5 -F_0x2e_028_0x2e__0x2e__0x2e__bit_4 -F_0x2e_028_0x2e__0x2e__0x2e__bit_3 -F_0x2e_028_0x2e__0x2e__0x2e__bit_2 -F_0x2e_028_0x2e__0x2e__0x2e__bit_1 -F_0x2e_028_0x2e__0x2e__0x2e__bit0 -F_0x2e_028_0x2e__0x2e__0x2e__bit1 -F_0x2e_028_0x2e__0x2e__0x2e__bit2 -F_0x2e_028_0x2e__0x2e__0x2e__bit3 -F_0x2e_028_0x2e__0x2e__0x2e__bit4 -F_0x2e_028_0x2e__0x2e__0x2e__bit5 -F_0x2e_028_0x2e__0x2e__0x2e__bit6 -F_0x2e_028_0x2e__0x2e__0x2e__bit7 -F_0x2e_028_0x2e__0x2e__0x2e__bit8 -F_0x2e_028_0x2e__0x2e__0x2e__bit9 -F_0x2e_028_0x2e__0x2e__0x2e__bit10 -F_0x2e_028_0x2e__0x2e__0x2e__bit11 -F_0x2e_028_0x2e__0x2e__0x2e__bit12 -F_0x2e_032033_bit_7 -F_0x2e_032033_bit_6 -F_0x2e_032033_bit_5 -F_0x2e_032033_bit_4 -F_0x2e_032033_bit_3 -F_0x2e_032033_bit_2 -F_0x2e_032033_bit_1 F_0x2e_032033_bit0 -F_0x2e_032033_bit1 F_0x2e_032033_bit2 -F_0x2e_032033_bit3 -F_0x2e_032033_bit4 -F_0x2e_032033_bit5 -F_0x2e_032033_bit6 -F_0x2e_032033_bit7 -F_0x2e_032033_bit8 -F_0x2e_032033_bit9 -F_0x2e_032033_bit10 -F_0x2e_032033_bit11 -F_0x2e_032033_bit12 -F_0x2e_033037_bit_7 -F_0x2e_033037_bit_6 -F_0x2e_033037_bit_5 -F_0x2e_033037_bit_4 -F_0x2e_033037_bit_3 -F_0x2e_033037_bit_2 -F_0x2e_033037_bit_1 F_0x2e_033037_bit0 -F_0x2e_033037_bit1 F_0x2e_033037_bit2 -F_0x2e_033037_bit3 -F_0x2e_033037_bit4 -F_0x2e_033037_bit5 -F_0x2e_033037_bit6 -F_0x2e_033037_bit7 -F_0x2e_033037_bit8 -F_0x2e_033037_bit9 -F_0x2e_033037_bit10 -F_0x2e_033037_bit11 -F_0x2e_033037_bit12 -F_0x2e_034036_bit_7 -F_0x2e_034036_bit_6 -F_0x2e_034036_bit_5 -F_0x2e_034036_bit_4 -F_0x2e_034036_bit_3 -F_0x2e_034036_bit_2 -F_0x2e_034036_bit_1 -F_0x2e_034036_bit0 -F_0x2e_034036_bit1 -F_0x2e_034036_bit2 -F_0x2e_034036_bit3 -F_0x2e_034036_bit4 -F_0x2e_034036_bit5 -F_0x2e_034036_bit6 -F_0x2e_034036_bit7 -F_0x2e_034036_bit8 -F_0x2e_034036_bit9 -F_0x2e_034036_bit10 -F_0x2e_034036_bit11 -F_0x2e_034036_bit12 -F_0x2e_035036_bit_7 -F_0x2e_035036_bit_6 -F_0x2e_035036_bit_5 -F_0x2e_035036_bit_4 -F_0x2e_035036_bit_3 -F_0x2e_035036_bit_2 -F_0x2e_035036_bit_1 -F_0x2e_035036_bit0 -F_0x2e_035036_bit1 -F_0x2e_035036_bit2 -F_0x2e_035036_bit3 -F_0x2e_035036_bit4 -F_0x2e_035036_bit5 -F_0x2e_035036_bit6 -F_0x2e_035036_bit7 -F_0x2e_035036_bit8 -F_0x2e_035036_bit9 -F_0x2e_035036_bit10 -F_0x2e_035036_bit11 -F_0x2e_035036_bit12 -F_0x2e_037038_bit_7 -F_0x2e_037038_bit_6 -F_0x2e_037038_bit_5 -F_0x2e_037038_bit_4 -F_0x2e_037038_bit_3 -F_0x2e_037038_bit_2 -F_0x2e_037038_bit_1 F_0x2e_037038_bit0 -F_0x2e_037038_bit1 F_0x2e_037038_bit2 -F_0x2e_037038_bit3 -F_0x2e_037038_bit4 -F_0x2e_037038_bit5 -F_0x2e_037038_bit6 -F_0x2e_037038_bit7 -F_0x2e_037038_bit8 -F_0x2e_037038_bit9 -F_0x2e_037038_bit10 -F_0x2e_037038_bit11 -F_0x2e_037038_bit12 -F_0x2e_039040_bit_7 -F_0x2e_039040_bit_6 -F_0x2e_039040_bit_5 -F_0x2e_039040_bit_4 -F_0x2e_039040_bit_3 -F_0x2e_039040_bit_2 -F_0x2e_039040_bit_1 F_0x2e_039040_bit0 -F_0x2e_039040_bit1 F_0x2e_039040_bit2 -F_0x2e_039040_bit3 -F_0x2e_039040_bit4 -F_0x2e_039040_bit5 -F_0x2e_039040_bit6 -F_0x2e_039040_bit7 -F_0x2e_039040_bit8 -F_0x2e_039040_bit9 -F_0x2e_039040_bit10 -F_0x2e_039040_bit11 -F_0x2e_039040_bit12 -F_0x2e_040_0x2e__0x2e__0x2e__bit_7 -F_0x2e_040_0x2e__0x2e__0x2e__bit_6 -F_0x2e_040_0x2e__0x2e__0x2e__bit_5 -F_0x2e_040_0x2e__0x2e__0x2e__bit_4 -F_0x2e_040_0x2e__0x2e__0x2e__bit_3 -F_0x2e_040_0x2e__0x2e__0x2e__bit_2 -F_0x2e_040_0x2e__0x2e__0x2e__bit_1 -F_0x2e_040_0x2e__0x2e__0x2e__bit0 -F_0x2e_040_0x2e__0x2e__0x2e__bit1 -F_0x2e_040_0x2e__0x2e__0x2e__bit2 -F_0x2e_040_0x2e__0x2e__0x2e__bit3 -F_0x2e_040_0x2e__0x2e__0x2e__bit4 -F_0x2e_040_0x2e__0x2e__0x2e__bit5 -F_0x2e_040_0x2e__0x2e__0x2e__bit6 -F_0x2e_040_0x2e__0x2e__0x2e__bit7 -F_0x2e_040_0x2e__0x2e__0x2e__bit8 -F_0x2e_040_0x2e__0x2e__0x2e__bit9 -F_0x2e_040_0x2e__0x2e__0x2e__bit10 -F_0x2e_040_0x2e__0x2e__0x2e__bit11 -F_0x2e_040_0x2e__0x2e__0x2e__bit12 -F_0x2e_041_0x2e__0x2e__0x2e__bi

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/21774/stat): 21774 (minisat+_script) R 21773 21774 1333 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1796971020 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/21774/statm): 174 3 169 147 0 27 0
[pid=21774] 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=21775
New process pid=21776
New process pid=21777
execve syscall for /bin/sed executable
One traced child (pid=21776) 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=21777) exited with status: 0
One traced child (pid=21775) exited with status: 0
New process pid=21778
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-egout.opb

[startup+10.0034 s]
Raw data (loadavg): 0.81 0.92 0.68 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 7994 0 0 0 935 31 0 0 25 0 1 0 1796971025 35749888 7665 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 8728 7665 145 145 0 8583 0
[pid=21778] vsize: 34912
Current children cumulated CPU time (s) 9.66
Current children cumulated vsize (Kb) 37036

[startup+20.0041 s]
Raw data (loadavg): 0.84 0.93 0.69 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 8221 0 0 0 1933 32 0 0 25 0 1 0 1796971025 36712448 7892 4294967295 134512640 135094434 3221224432 3221222144 134600246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 8963 7892 145 145 0 8818 0
[pid=21778] vsize: 35852
Current children cumulated CPU time (s) 19.65
Current children cumulated vsize (Kb) 37976

[startup+30.0058 s]
Raw data (loadavg): 0.86 0.93 0.69 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 16568 0 0 0 2869 63 0 0 25 0 1 0 1796971025 73404416 15909 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21778/statm): 17921 15909 145 145 0 17776 0
[pid=21778] vsize: 71684
Current children cumulated CPU time (s) 29.32
Current children cumulated vsize (Kb) 73808

[startup+40.0064 s]
Raw data (loadavg): 0.88 0.93 0.69 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 16626 0 0 0 3868 63 0 0 25 0 1 0 1796971025 73613312 15967 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 17972 15967 145 145 0 17827 0
[pid=21778] vsize: 71888
Current children cumulated CPU time (s) 39.31
Current children cumulated vsize (Kb) 74012

[startup+50.008 s]
Raw data (loadavg): 0.90 0.93 0.70 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 16815 0 0 0 4868 64 0 0 25 0 1 0 1796971025 73949184 16156 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18054 16156 145 145 0 17909 0
[pid=21778] vsize: 72216
Current children cumulated CPU time (s) 49.32
Current children cumulated vsize (Kb) 74340

[startup+60.0087 s]
Raw data (loadavg): 0.91 0.93 0.70 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 16905 0 0 0 5867 64 0 0 25 0 1 0 1796971025 73969664 16168 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21778/statm): 18059 16168 145 145 0 17914 0
[pid=21778] vsize: 72236
Current children cumulated CPU time (s) 59.31
Current children cumulated vsize (Kb) 74360

[startup+70.0094 s]
Raw data (loadavg): 0.93 0.93 0.70 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 16916 0 0 0 6867 64 0 0 25 0 1 0 1796971025 74010624 16179 4294967295 134512640 135094434 3221224432 3221223092 134553475 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18069 16179 145 145 0 17924 0
[pid=21778] vsize: 72276
Current children cumulated CPU time (s) 69.31
Current children cumulated vsize (Kb) 74400

[startup+80.01 s]
Raw data (loadavg): 0.94 0.94 0.70 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 16939 0 0 0 7866 65 0 0 25 0 1 0 1796971025 74104832 16202 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18092 16202 145 145 0 17947 0
[pid=21778] vsize: 72368
Current children cumulated CPU time (s) 79.31
Current children cumulated vsize (Kb) 74492

[startup+90.0106 s]
Raw data (loadavg): 0.95 0.94 0.71 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 16975 0 0 0 8865 65 0 0 25 0 1 0 1796971025 74252288 16238 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18128 16238 145 145 0 17983 0
[pid=21778] vsize: 72512
Current children cumulated CPU time (s) 89.3
Current children cumulated vsize (Kb) 74636

[startup+100.011 s]
Raw data (loadavg): 0.95 0.94 0.71 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17078 0 0 0 9865 65 0 0 25 0 1 0 1796971025 74522624 16305 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18194 16305 145 145 0 18049 0
[pid=21778] vsize: 72776
Current children cumulated CPU time (s) 99.3
Current children cumulated vsize (Kb) 74900

[startup+110.012 s]
Raw data (loadavg): 0.96 0.94 0.71 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17138 0 0 0 10865 65 0 0 25 0 1 0 1796971025 74477568 16293 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18183 16293 145 145 0 18038 0
[pid=21778] vsize: 72732
Current children cumulated CPU time (s) 109.3
Current children cumulated vsize (Kb) 74856

[startup+120.013 s]
Raw data (loadavg): 0.97 0.94 0.72 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17200 0 0 0 11864 66 0 0 25 0 1 0 1796971025 74567680 16316 4294967295 134512640 135094434 3221224432 3221221104 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18205 16316 145 145 0 18060 0
[pid=21778] vsize: 72820
Current children cumulated CPU time (s) 119.3
Current children cumulated vsize (Kb) 74944

[startup+130.013 s]
Raw data (loadavg): 0.97 0.94 0.72 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17234 0 0 0 12864 66 0 0 25 0 1 0 1796971025 74551296 16313 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18201 16313 145 145 0 18056 0
[pid=21778] vsize: 72804
Current children cumulated CPU time (s) 129.3
Current children cumulated vsize (Kb) 74928

[startup+140.014 s]
Raw data (loadavg): 0.98 0.95 0.72 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17255 0 0 0 13864 66 0 0 25 0 1 0 1796971025 74637312 16334 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18222 16334 145 145 0 18077 0
[pid=21778] vsize: 72888
Current children cumulated CPU time (s) 139.3
Current children cumulated vsize (Kb) 75012

[startup+150.016 s]
Raw data (loadavg): 0.98 0.95 0.72 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17395 0 0 0 14862 67 0 0 25 0 1 0 1796971025 75280384 16474 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18379 16474 145 145 0 18234 0
[pid=21778] vsize: 73516
Current children cumulated CPU time (s) 149.29
Current children cumulated vsize (Kb) 75640

[startup+160.016 s]
Raw data (loadavg): 0.98 0.95 0.73 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17407 0 0 0 15862 67 0 0 25 0 1 0 1796971025 75325440 16486 4294967295 134512640 135094434 3221224432 3221223056 134557675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18390 16486 145 145 0 18245 0
[pid=21778] vsize: 73560
Current children cumulated CPU time (s) 159.29
Current children cumulated vsize (Kb) 75684

[startup+170.016 s]
Raw data (loadavg): 0.98 0.95 0.73 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17446 0 0 0 16862 67 0 0 25 0 1 0 1796971025 75485184 16525 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18429 16525 145 145 0 18284 0
[pid=21778] vsize: 73716
Current children cumulated CPU time (s) 169.29
Current children cumulated vsize (Kb) 75840

[startup+180.016 s]
Raw data (loadavg): 0.99 0.95 0.73 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17454 0 0 0 17862 67 0 0 25 0 1 0 1796971025 75517952 16533 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18437 16533 145 145 0 18292 0
[pid=21778] vsize: 73748
Current children cumulated CPU time (s) 179.29
Current children cumulated vsize (Kb) 75872

[startup+190.017 s]
Raw data (loadavg): 0.99 0.95 0.73 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17463 0 0 0 18862 68 0 0 25 0 1 0 1796971025 75550720 16542 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18445 16542 145 145 0 18300 0
[pid=21778] vsize: 73780
Current children cumulated CPU time (s) 189.3
Current children cumulated vsize (Kb) 75904

[startup+200.018 s]
Raw data (loadavg): 0.99 0.95 0.74 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17471 0 0 0 19862 68 0 0 25 0 1 0 1796971025 75583488 16550 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18453 16550 145 145 0 18308 0
[pid=21778] vsize: 73812
Current children cumulated CPU time (s) 199.3
Current children cumulated vsize (Kb) 75936

[startup+210.018 s]
Raw data (loadavg): 0.99 0.95 0.74 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) T 21774 21774 1333 0 -1 0 17486 0 0 0 20863 68 0 0 25 0 1 0 1796971025 75644928 16565 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18468 16565 145 145 0 18323 0
[pid=21778] vsize: 73872
Current children cumulated CPU time (s) 209.31
Current children cumulated vsize (Kb) 75996

[startup+220.019 s]
Raw data (loadavg): 0.99 0.95 0.74 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17587 0 0 0 21862 68 0 0 25 0 1 0 1796971025 76107776 16666 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18581 16666 145 145 0 18436 0
[pid=21778] vsize: 74324
Current children cumulated CPU time (s) 219.3
Current children cumulated vsize (Kb) 76448

[startup+230.02 s]
Raw data (loadavg): 0.99 0.95 0.74 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17588 0 0 0 22862 68 0 0 25 0 1 0 1796971025 76107776 16667 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18581 16667 145 145 0 18436 0
[pid=21778] vsize: 74324
Current children cumulated CPU time (s) 229.3
Current children cumulated vsize (Kb) 76448

[startup+240.02 s]
Raw data (loadavg): 0.99 0.95 0.74 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17588 0 0 0 23862 68 0 0 25 0 1 0 1796971025 76107776 16667 4294967295 134512640 135094434 3221224432 3221223056 134562088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18581 16667 145 145 0 18436 0
[pid=21778] vsize: 74324
Current children cumulated CPU time (s) 239.3
Current children cumulated vsize (Kb) 76448

[startup+250.021 s]
Raw data (loadavg): 0.99 0.96 0.75 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17588 0 0 0 24862 68 0 0 25 0 1 0 1796971025 76107776 16667 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18581 16667 145 145 0 18436 0
[pid=21778] vsize: 74324
Current children cumulated CPU time (s) 249.3
Current children cumulated vsize (Kb) 76448

[startup+260.022 s]
Raw data (loadavg): 0.99 0.96 0.75 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17663 0 0 0 25862 68 0 0 25 0 1 0 1796971025 76103680 16667 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18580 16667 145 145 0 18435 0
[pid=21778] vsize: 74320
Current children cumulated CPU time (s) 259.3
Current children cumulated vsize (Kb) 76444

[startup+270.022 s]
Raw data (loadavg): 0.99 0.96 0.75 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17675 0 0 0 26861 70 0 0 25 0 1 0 1796971025 76152832 16679 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18592 16679 145 145 0 18447 0
[pid=21778] vsize: 74368
Current children cumulated CPU time (s) 269.31
Current children cumulated vsize (Kb) 76492

[startup+280.023 s]
Raw data (loadavg): 0.99 0.96 0.75 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17689 0 0 0 27860 71 0 0 25 0 1 0 1796971025 76210176 16693 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18606 16693 145 145 0 18461 0
[pid=21778] vsize: 74424
Current children cumulated CPU time (s) 279.31
Current children cumulated vsize (Kb) 76548

[startup+290.024 s]
Raw data (loadavg): 0.99 0.96 0.75 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17827 0 0 0 28858 72 0 0 25 0 1 0 1796971025 76611584 16792 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18704 16792 145 145 0 18559 0
[pid=21778] vsize: 74816
Current children cumulated CPU time (s) 289.3
Current children cumulated vsize (Kb) 76940

[startup+300.024 s]
Raw data (loadavg): 0.99 0.96 0.76 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17896 0 0 0 29858 72 0 0 25 0 1 0 1796971025 76595200 16786 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18700 16786 145 145 0 18555 0
[pid=21778] vsize: 74800
Current children cumulated CPU time (s) 299.3
Current children cumulated vsize (Kb) 76924

[startup+310.025 s]
Raw data (loadavg): 0.99 0.96 0.76 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17924 0 0 0 30858 73 0 0 25 0 1 0 1796971025 76701696 16814 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18726 16814 145 145 0 18581 0
[pid=21778] vsize: 74904
Current children cumulated CPU time (s) 309.31
Current children cumulated vsize (Kb) 77028

[startup+320.025 s]
Raw data (loadavg): 0.99 0.96 0.76 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17949 0 0 0 31858 73 0 0 25 0 1 0 1796971025 76800000 16839 4294967295 134512640 135094434 3221224432 3221223088 134557859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18750 16839 145 145 0 18605 0
[pid=21778] vsize: 75000
Current children cumulated CPU time (s) 319.31
Current children cumulated vsize (Kb) 77124

[startup+330.026 s]
Raw data (loadavg): 0.99 0.96 0.76 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 17997 0 0 0 32857 74 0 0 25 0 1 0 1796971025 76996608 16887 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18798 16887 145 145 0 18653 0
[pid=21778] vsize: 75192
Current children cumulated CPU time (s) 329.31
Current children cumulated vsize (Kb) 77316

[startup+340.027 s]
Raw data (loadavg): 0.99 0.96 0.76 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18060 0 0 0 33856 74 0 0 25 0 1 0 1796971025 77312000 16950 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18875 16950 145 145 0 18730 0
[pid=21778] vsize: 75500
Current children cumulated CPU time (s) 339.3
Current children cumulated vsize (Kb) 77624

[startup+350.028 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18096 0 0 0 34856 74 0 0 25 0 1 0 1796971025 77455360 16986 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18910 16986 145 145 0 18765 0
[pid=21778] vsize: 75640
Current children cumulated CPU time (s) 349.3
Current children cumulated vsize (Kb) 77764

[startup+360.028 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18161 0 0 0 35855 75 0 0 25 0 1 0 1796971025 77561856 17012 4294967295 134512640 135094434 3221224432 3221222040 134676609 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18936 17012 145 145 0 18791 0
[pid=21778] vsize: 75744
Current children cumulated CPU time (s) 359.3
Current children cumulated vsize (Kb) 77868

[startup+370.029 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18190 0 0 0 36855 75 0 0 25 0 1 0 1796971025 77529088 17004 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18928 17004 145 145 0 18783 0
[pid=21778] vsize: 75712
Current children cumulated CPU time (s) 369.3
Current children cumulated vsize (Kb) 77836

[startup+380.029 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18201 0 0 0 37855 75 0 0 25 0 1 0 1796971025 77570048 17015 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18938 17015 145 145 0 18793 0
[pid=21778] vsize: 75752
Current children cumulated CPU time (s) 379.3
Current children cumulated vsize (Kb) 77876

[startup+390.03 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18223 0 0 0 38855 76 0 0 25 0 1 0 1796971025 77660160 17037 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18960 17037 145 145 0 18815 0
[pid=21778] vsize: 75840
Current children cumulated CPU time (s) 389.31
Current children cumulated vsize (Kb) 77964

[startup+400.032 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18239 0 0 0 39855 76 0 0 25 0 1 0 1796971025 77725696 17053 4294967295 134512640 135094434 3221224432 3221223056 134557660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18976 17053 145 145 0 18831 0
[pid=21778] vsize: 75904
Current children cumulated CPU time (s) 399.31
Current children cumulated vsize (Kb) 78028

[startup+410.032 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18257 0 0 0 40854 76 0 0 25 0 1 0 1796971025 77795328 17071 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 18993 17071 145 145 0 18848 0
[pid=21778] vsize: 75972
Current children cumulated CPU time (s) 409.3
Current children cumulated vsize (Kb) 78096

[startup+420.033 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18292 0 0 0 41854 76 0 0 25 0 1 0 1796971025 77938688 17106 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19028 17106 145 145 0 18883 0
[pid=21778] vsize: 76112
Current children cumulated CPU time (s) 419.3
Current children cumulated vsize (Kb) 78236

[startup+430.035 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18391 0 0 0 42852 77 0 0 25 0 1 0 1796971025 78032896 17128 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19051 17128 145 145 0 18906 0
[pid=21778] vsize: 76204
Current children cumulated CPU time (s) 429.29
Current children cumulated vsize (Kb) 78328

[startup+440.035 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18460 0 0 0 43852 78 0 0 25 0 1 0 1796971025 78151680 17158 4294967295 134512640 135094434 3221224432 3221220320 134677021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19080 17158 145 145 0 18935 0
[pid=21778] vsize: 76320
Current children cumulated CPU time (s) 439.3
Current children cumulated vsize (Kb) 78444

[startup+450.037 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18497 0 0 0 44851 78 0 0 25 0 1 0 1796971025 78151680 17158 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19080 17158 145 145 0 18935 0
[pid=21778] vsize: 76320
Current children cumulated CPU time (s) 449.29
Current children cumulated vsize (Kb) 78444

[startup+460.038 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18518 0 0 0 45852 78 0 0 25 0 1 0 1796971025 78233600 17179 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19100 17179 145 145 0 18955 0
[pid=21778] vsize: 76400
Current children cumulated CPU time (s) 459.3
Current children cumulated vsize (Kb) 78524

[startup+470.038 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18541 0 0 0 46852 78 0 0 25 0 1 0 1796971025 78327808 17202 4294967295 134512640 135094434 3221224432 3221223088 134557804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19123 17202 145 145 0 18978 0
[pid=21778] vsize: 76492
Current children cumulated CPU time (s) 469.3
Current children cumulated vsize (Kb) 78616

[startup+480.039 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18558 0 0 0 47852 78 0 0 25 0 1 0 1796971025 78393344 17219 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19139 17219 145 145 0 18994 0
[pid=21778] vsize: 76556
Current children cumulated CPU time (s) 479.3
Current children cumulated vsize (Kb) 78680

[startup+490.04 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18574 0 0 0 48851 79 0 0 25 0 1 0 1796971025 78458880 17235 4294967295 134512640 135094434 3221224432 3221223088 134558284 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19155 17235 145 145 0 19010 0
[pid=21778] vsize: 76620
Current children cumulated CPU time (s) 489.3
Current children cumulated vsize (Kb) 78744

[startup+500.041 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18589 0 0 0 49852 79 0 0 25 0 1 0 1796971025 78520320 17250 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19170 17250 145 145 0 19025 0
[pid=21778] vsize: 76680
Current children cumulated CPU time (s) 499.31
Current children cumulated vsize (Kb) 78804

[startup+510.042 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18629 0 0 0 50851 79 0 0 25 0 1 0 1796971025 78684160 17290 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19210 17290 145 145 0 19065 0
[pid=21778] vsize: 76840
Current children cumulated CPU time (s) 509.3
Current children cumulated vsize (Kb) 78964

[startup+520.043 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18779 0 0 0 51850 80 0 0 25 0 1 0 1796971025 78831616 17326 4294967295 134512640 135094434 3221224432 3221221280 134600254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19246 17326 145 145 0 19101 0
[pid=21778] vsize: 76984
Current children cumulated CPU time (s) 519.3
Current children cumulated vsize (Kb) 79108

[startup+530.043 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18891 0 0 0 52849 81 0 0 25 0 1 0 1796971025 78835712 17326 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19247 17326 145 145 0 19102 0
[pid=21778] vsize: 76988
Current children cumulated CPU time (s) 529.3
Current children cumulated vsize (Kb) 79112

[startup+540.044 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18902 0 0 0 53849 81 0 0 25 0 1 0 1796971025 78872576 17337 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19256 17337 145 145 0 19111 0
[pid=21778] vsize: 77024
Current children cumulated CPU time (s) 539.3
Current children cumulated vsize (Kb) 79148

[startup+550.045 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18939 0 0 0 54849 81 0 0 25 0 1 0 1796971025 79024128 17374 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19293 17374 145 145 0 19148 0
[pid=21778] vsize: 77172
Current children cumulated CPU time (s) 549.3
Current children cumulated vsize (Kb) 79296

[startup+560.045 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18957 0 0 0 55849 81 0 0 25 0 1 0 1796971025 79097856 17392 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19311 17392 145 145 0 19166 0
[pid=21778] vsize: 77244
Current children cumulated CPU time (s) 559.3
Current children cumulated vsize (Kb) 79368

[startup+570.046 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18969 0 0 0 56849 81 0 0 25 0 1 0 1796971025 79142912 17404 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19322 17404 145 145 0 19177 0
[pid=21778] vsize: 77288
Current children cumulated CPU time (s) 569.3
Current children cumulated vsize (Kb) 79412

[startup+580.047 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 18988 0 0 0 57849 81 0 0 25 0 1 0 1796971025 79220736 17423 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19341 17423 145 145 0 19196 0
[pid=21778] vsize: 77364
Current children cumulated CPU time (s) 579.3
Current children cumulated vsize (Kb) 79488

[startup+590.047 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19018 0 0 0 58849 82 0 0 25 0 1 0 1796971025 79339520 17453 4294967295 134512640 135094434 3221224432 3221223024 134557334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19370 17453 145 145 0 19225 0
[pid=21778] vsize: 77480
Current children cumulated CPU time (s) 589.31
Current children cumulated vsize (Kb) 79604

[startup+600.049 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19034 0 0 0 59849 82 0 0 25 0 1 0 1796971025 79405056 17469 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19386 17469 145 145 0 19241 0
[pid=21778] vsize: 77544
Current children cumulated CPU time (s) 599.31
Current children cumulated vsize (Kb) 79668

[startup+610.049 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19124 0 0 0 60848 83 0 0 25 0 1 0 1796971025 79454208 17483 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19398 17483 145 145 0 19253 0
[pid=21778] vsize: 77592
Current children cumulated CPU time (s) 609.31
Current children cumulated vsize (Kb) 79716

[startup+620.049 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19146 0 0 0 61848 83 0 0 25 0 1 0 1796971025 79548416 17505 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19421 17505 145 145 0 19276 0
[pid=21778] vsize: 77684
Current children cumulated CPU time (s) 619.31
Current children cumulated vsize (Kb) 79808

[startup+630.051 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19161 0 0 0 62848 83 0 0 25 0 1 0 1796971025 79601664 17520 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19434 17520 145 145 0 19289 0
[pid=21778] vsize: 77736
Current children cumulated CPU time (s) 629.31
Current children cumulated vsize (Kb) 79860

[startup+640.051 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19183 0 0 0 63848 83 0 0 25 0 1 0 1796971025 79691776 17542 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19456 17542 145 145 0 19311 0
[pid=21778] vsize: 77824
Current children cumulated CPU time (s) 639.31
Current children cumulated vsize (Kb) 79948

[startup+650.052 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19253 0 0 0 64848 83 0 0 25 0 1 0 1796971025 79818752 17573 4294967295 134512640 135094434 3221224432 3221220576 134676489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19487 17573 145 145 0 19342 0
[pid=21778] vsize: 77948
Current children cumulated CPU time (s) 649.31
Current children cumulated vsize (Kb) 80072

[startup+660.053 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19282 0 0 0 65847 83 0 0 25 0 1 0 1796971025 79781888 17564 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19478 17564 145 145 0 19333 0
[pid=21778] vsize: 77912
Current children cumulated CPU time (s) 659.3
Current children cumulated vsize (Kb) 80036

[startup+670.053 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19294 0 0 0 66847 83 0 0 25 0 1 0 1796971025 79831040 17576 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19490 17576 145 145 0 19345 0
[pid=21778] vsize: 77960
Current children cumulated CPU time (s) 669.3
Current children cumulated vsize (Kb) 80084

[startup+680.054 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19307 0 0 0 67847 84 0 0 25 0 1 0 1796971025 79880192 17589 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19502 17589 145 145 0 19357 0
[pid=21778] vsize: 78008
Current children cumulated CPU time (s) 679.31
Current children cumulated vsize (Kb) 80132

[startup+690.055 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19323 0 0 0 68847 84 0 0 25 0 1 0 1796971025 79945728 17605 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19518 17605 145 145 0 19373 0
[pid=21778] vsize: 78072
Current children cumulated CPU time (s) 689.31
Current children cumulated vsize (Kb) 80196

[startup+700.056 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19333 0 0 0 69847 84 0 0 25 0 1 0 1796971025 79986688 17615 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19528 17615 145 145 0 19383 0
[pid=21778] vsize: 78112
Current children cumulated CPU time (s) 699.31
Current children cumulated vsize (Kb) 80236

[startup+710.057 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19370 0 0 0 70847 84 0 0 25 0 1 0 1796971025 80142336 17652 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19566 17652 145 145 0 19421 0
[pid=21778] vsize: 78264
Current children cumulated CPU time (s) 709.31
Current children cumulated vsize (Kb) 80388

[startup+720.058 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19400 0 0 0 71847 84 0 0 25 0 1 0 1796971025 80257024 17682 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19594 17682 145 145 0 19449 0
[pid=21778] vsize: 78376
Current children cumulated CPU time (s) 719.31
Current children cumulated vsize (Kb) 80500

[startup+730.058 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19408 0 0 0 72847 84 0 0 25 0 1 0 1796971025 80289792 17690 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19602 17690 145 145 0 19457 0
[pid=21778] vsize: 78408
Current children cumulated CPU time (s) 729.31
Current children cumulated vsize (Kb) 80532

[startup+740.059 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19414 0 0 0 73847 84 0 0 25 0 1 0 1796971025 80314368 17696 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19608 17696 145 145 0 19463 0
[pid=21778] vsize: 78432
Current children cumulated CPU time (s) 739.31
Current children cumulated vsize (Kb) 80556

[startup+750.061 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19414 0 0 0 74847 85 0 0 25 0 1 0 1796971025 80314368 17696 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19608 17696 145 145 0 19463 0
[pid=21778] vsize: 78432
Current children cumulated CPU time (s) 749.32
Current children cumulated vsize (Kb) 80556

[startup+760.061 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19432 0 0 0 75847 85 0 0 25 0 1 0 1796971025 80388096 17714 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19626 17714 145 145 0 19481 0
[pid=21778] vsize: 78504
Current children cumulated CPU time (s) 759.32
Current children cumulated vsize (Kb) 80628

[startup+770.062 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) T 21774 21774 1333 0 -1 0 19527 0 0 0 76847 85 0 0 25 0 1 0 1796971025 80465920 17733 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19645 17733 145 145 0 19500 0
[pid=21778] vsize: 78580
Current children cumulated CPU time (s) 769.32
Current children cumulated vsize (Kb) 80704

[startup+780.063 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19542 0 0 0 77847 85 0 0 25 0 1 0 1796971025 80527360 17748 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19660 17748 145 145 0 19515 0
[pid=21778] vsize: 78640
Current children cumulated CPU time (s) 779.32
Current children cumulated vsize (Kb) 80764

[startup+790.063 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19553 0 0 0 78847 85 0 0 25 0 1 0 1796971025 80572416 17759 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19671 17759 145 145 0 19526 0
[pid=21778] vsize: 78684
Current children cumulated CPU time (s) 789.32
Current children cumulated vsize (Kb) 80808

[startup+800.064 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19569 0 0 0 79847 85 0 0 25 0 1 0 1796971025 80633856 17775 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19686 17775 145 145 0 19541 0
[pid=21778] vsize: 78744
Current children cumulated CPU time (s) 799.32
Current children cumulated vsize (Kb) 80868

[startup+810.066 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19583 0 0 0 80847 85 0 0 25 0 1 0 1796971025 80695296 17789 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19701 17789 145 145 0 19556 0
[pid=21778] vsize: 78804
Current children cumulated CPU time (s) 809.32
Current children cumulated vsize (Kb) 80928

[startup+820.066 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19597 0 0 0 81847 85 0 0 25 0 1 0 1796971025 80748544 17803 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19714 17803 145 145 0 19569 0
[pid=21778] vsize: 78856
Current children cumulated CPU time (s) 819.32
Current children cumulated vsize (Kb) 80980

[startup+830.067 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19614 0 0 0 82847 85 0 0 25 0 1 0 1796971025 80814080 17820 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19730 17820 145 145 0 19585 0
[pid=21778] vsize: 78920
Current children cumulated CPU time (s) 829.32
Current children cumulated vsize (Kb) 81044

[startup+840.067 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19634 0 0 0 83847 86 0 0 25 0 1 0 1796971025 80896000 17840 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19750 17840 145 145 0 19605 0
[pid=21778] vsize: 79000
Current children cumulated CPU time (s) 839.33
Current children cumulated vsize (Kb) 81124

[startup+850.069 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19652 0 0 0 84847 86 0 0 25 0 1 0 1796971025 80969728 17858 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19768 17858 145 145 0 19623 0
[pid=21778] vsize: 79072
Current children cumulated CPU time (s) 849.33
Current children cumulated vsize (Kb) 81196

[startup+860.07 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19665 0 0 0 85847 86 0 0 25 0 1 0 1796971025 81022976 17871 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19781 17871 145 145 0 19636 0
[pid=21778] vsize: 79124
Current children cumulated CPU time (s) 859.33
Current children cumulated vsize (Kb) 81248

[startup+870.07 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19681 0 0 0 86846 87 0 0 25 0 1 0 1796971025 81084416 17887 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19796 17887 145 145 0 19651 0
[pid=21778] vsize: 79184
Current children cumulated CPU time (s) 869.33
Current children cumulated vsize (Kb) 81308

[startup+880.072 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19691 0 0 0 87845 88 0 0 25 0 1 0 1796971025 81125376 17897 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19806 17897 145 145 0 19661 0
[pid=21778] vsize: 79224
Current children cumulated CPU time (s) 879.33
Current children cumulated vsize (Kb) 81348

[startup+890.073 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19705 0 0 0 88845 88 0 0 25 0 1 0 1796971025 81182720 17911 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19820 17911 145 145 0 19675 0
[pid=21778] vsize: 79280
Current children cumulated CPU time (s) 889.33
Current children cumulated vsize (Kb) 81404

[startup+900.074 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19721 0 0 0 89845 88 0 0 25 0 1 0 1796971025 81248256 17927 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19836 17927 145 145 0 19691 0
[pid=21778] vsize: 79344
Current children cumulated CPU time (s) 899.33
Current children cumulated vsize (Kb) 81468

[startup+910.075 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19761 0 0 0 90845 89 0 0 25 0 1 0 1796971025 81543168 17967 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19908 17967 145 145 0 19763 0
[pid=21778] vsize: 79632
Current children cumulated CPU time (s) 909.34
Current children cumulated vsize (Kb) 81756

[startup+920.075 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19817 0 0 0 91844 89 0 0 25 0 1 0 1796971025 81608704 17984 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19924 17984 145 145 0 19779 0
[pid=21778] vsize: 79696
Current children cumulated CPU time (s) 919.33
Current children cumulated vsize (Kb) 81820

[startup+930.076 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19817 0 0 0 92844 90 0 0 25 0 1 0 1796971025 81608704 17984 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19924 17984 145 145 0 19779 0
[pid=21778] vsize: 79696
Current children cumulated CPU time (s) 929.34
Current children cumulated vsize (Kb) 81820

[startup+940.077 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19826 0 0 0 93844 90 0 0 25 0 1 0 1796971025 81649664 17993 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19934 17993 145 145 0 19789 0
[pid=21778] vsize: 79736
Current children cumulated CPU time (s) 939.34
Current children cumulated vsize (Kb) 81860

[startup+950.078 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19848 0 0 0 94844 90 0 0 25 0 1 0 1796971025 81739776 18015 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19956 18015 145 145 0 19811 0
[pid=21778] vsize: 79824
Current children cumulated CPU time (s) 949.34
Current children cumulated vsize (Kb) 81948

[startup+960.078 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19861 0 0 0 95844 90 0 0 25 0 1 0 1796971025 81788928 18028 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19968 18028 145 145 0 19823 0
[pid=21778] vsize: 79872
Current children cumulated CPU time (s) 959.34
Current children cumulated vsize (Kb) 81996

[startup+970.079 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19881 0 0 0 96844 90 0 0 25 0 1 0 1796971025 81870848 18048 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 19988 18048 145 145 0 19843 0
[pid=21778] vsize: 79952
Current children cumulated CPU time (s) 969.34
Current children cumulated vsize (Kb) 82076

[startup+980.08 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19908 0 0 0 97844 91 0 0 25 0 1 0 1796971025 81985536 18075 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20016 18075 145 145 0 19871 0
[pid=21778] vsize: 80064
Current children cumulated CPU time (s) 979.35
Current children cumulated vsize (Kb) 82188

[startup+990.08 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19920 0 0 0 98844 91 0 0 25 0 1 0 1796971025 82026496 18087 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20026 18087 145 145 0 19881 0
[pid=21778] vsize: 80104
Current children cumulated CPU time (s) 989.35
Current children cumulated vsize (Kb) 82228

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19931 0 0 0 99844 91 0 0 25 0 1 0 1796971025 82071552 18098 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20037 18098 145 145 0 19892 0
[pid=21778] vsize: 80148
Current children cumulated CPU time (s) 999.35
Current children cumulated vsize (Kb) 82272

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19949 0 0 0 100843 91 0 0 25 0 1 0 1796971025 82141184 18116 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20054 18116 145 145 0 19909 0
[pid=21778] vsize: 80216
Current children cumulated CPU time (s) 1009.34
Current children cumulated vsize (Kb) 82340

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19967 0 0 0 101844 91 0 0 25 0 1 0 1796971025 82214912 18134 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20072 18134 145 145 0 19927 0
[pid=21778] vsize: 80288
Current children cumulated CPU time (s) 1019.35
Current children cumulated vsize (Kb) 82412

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 19982 0 0 0 102844 91 0 0 25 0 1 0 1796971025 82276352 18149 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20087 18149 145 145 0 19942 0
[pid=21778] vsize: 80348
Current children cumulated CPU time (s) 1029.35
Current children cumulated vsize (Kb) 82472

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20000 0 0 0 103844 91 0 0 25 0 1 0 1796971025 82345984 18167 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20104 18167 145 145 0 19959 0
[pid=21778] vsize: 80416
Current children cumulated CPU time (s) 1039.35
Current children cumulated vsize (Kb) 82540

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20025 0 0 0 104843 92 0 0 25 0 1 0 1796971025 82456576 18192 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20131 18192 145 145 0 19986 0
[pid=21778] vsize: 80524
Current children cumulated CPU time (s) 1049.35
Current children cumulated vsize (Kb) 82648

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20084 0 0 0 105843 92 0 0 25 0 1 0 1796971025 82706432 18251 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20192 18251 145 145 0 20047 0
[pid=21778] vsize: 80768
Current children cumulated CPU time (s) 1059.35
Current children cumulated vsize (Kb) 82892

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20132 0 0 0 106843 92 0 0 25 0 1 0 1796971025 82890752 18299 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20237 18299 145 145 0 20092 0
[pid=21778] vsize: 80948
Current children cumulated CPU time (s) 1069.35
Current children cumulated vsize (Kb) 83072

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20152 0 0 0 107843 92 0 0 25 0 1 0 1796971025 82972672 18319 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20257 18319 145 145 0 20112 0
[pid=21778] vsize: 81028
Current children cumulated CPU time (s) 1079.35
Current children cumulated vsize (Kb) 83152

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20178 0 0 0 108843 93 0 0 25 0 1 0 1796971025 83079168 18345 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20283 18345 145 145 0 20138 0
[pid=21778] vsize: 81132
Current children cumulated CPU time (s) 1089.36
Current children cumulated vsize (Kb) 83256

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20202 0 0 0 109842 93 0 0 25 0 1 0 1796971025 83173376 18369 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20306 18369 145 145 0 20161 0
[pid=21778] vsize: 81224
Current children cumulated CPU time (s) 1099.35
Current children cumulated vsize (Kb) 83348

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20226 0 0 0 110842 93 0 0 25 0 1 0 1796971025 83271680 18393 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20330 18393 145 145 0 20185 0
[pid=21778] vsize: 81320
Current children cumulated CPU time (s) 1109.35
Current children cumulated vsize (Kb) 83444

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20249 0 0 0 111842 93 0 0 25 0 1 0 1796971025 83365888 18416 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20353 18416 145 145 0 20208 0
[pid=21778] vsize: 81412
Current children cumulated CPU time (s) 1119.35
Current children cumulated vsize (Kb) 83536

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20266 0 0 0 112842 93 0 0 25 0 1 0 1796971025 83435520 18433 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20370 18433 145 145 0 20225 0
[pid=21778] vsize: 81480
Current children cumulated CPU time (s) 1129.35
Current children cumulated vsize (Kb) 83604

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20284 0 0 0 113842 93 0 0 25 0 1 0 1796971025 83517440 18451 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20390 18451 145 145 0 20245 0
[pid=21778] vsize: 81560
Current children cumulated CPU time (s) 1139.35
Current children cumulated vsize (Kb) 83684

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20308 0 0 0 114842 94 0 0 25 0 1 0 1796971025 83623936 18475 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20416 18475 145 145 0 20271 0
[pid=21778] vsize: 81664
Current children cumulated CPU time (s) 1149.36
Current children cumulated vsize (Kb) 83788

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20319 0 0 0 115842 94 0 0 25 0 1 0 1796971025 83660800 18486 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20425 18486 145 145 0 20280 0
[pid=21778] vsize: 81700
Current children cumulated CPU time (s) 1159.36
Current children cumulated vsize (Kb) 83824

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20345 0 0 0 116842 94 0 0 25 0 1 0 1796971025 83763200 18512 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20450 18512 145 145 0 20305 0
[pid=21778] vsize: 81800
Current children cumulated CPU time (s) 1169.36
Current children cumulated vsize (Kb) 83924

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20358 0 0 0 117842 94 0 0 25 0 1 0 1796971025 83816448 18525 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20463 18525 145 145 0 20318 0
[pid=21778] vsize: 81852
Current children cumulated CPU time (s) 1179.36
Current children cumulated vsize (Kb) 83976

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20367 0 0 0 118842 94 0 0 25 0 1 0 1796971025 83853312 18534 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20472 18534 145 145 0 20327 0
[pid=21778] vsize: 81888
Current children cumulated CPU time (s) 1189.36
Current children cumulated vsize (Kb) 84012

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20384 0 0 0 119843 94 0 0 25 0 1 0 1796971025 83922944 18551 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20489 18551 145 145 0 20344 0
[pid=21778] vsize: 81956
Current children cumulated CPU time (s) 1199.37
Current children cumulated vsize (Kb) 84080

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20395 0 0 0 120842 94 0 0 25 0 1 0 1796971025 83963904 18562 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20499 18562 145 145 0 20354 0
[pid=21778] vsize: 81996
Current children cumulated CPU time (s) 1209.36
Current children cumulated vsize (Kb) 84120



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 21778
Raw data (/proc/21774/stat): 21774 (minisat+_script) S 21773 21774 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796971020 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21774/statm): 531 226 485 147 0 384 0
[pid=21774] vsize: 2124
Raw data (/proc/21778/stat): 21778 (minisat+_64-bit) R 21774 21774 1333 0 -1 0 20395 0 0 0 120842 94 0 0 25 0 1 0 1796971025 83963904 18562 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21778/statm): 20499 18562 145 145 0 20354 0
[pid=21778] vsize: 81996
Current children cumulated CPU time (s) 1209.36
Current children cumulated vsize (Kb) 84120

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

Child status: 10
Real time (s): 1210.15
CPU time (s): 1209.42
CPU user time (s): 1208.43
CPU system time (s): 0.98485
CPU usage (%): 99.9396
Max. virtual memory (cumulated for all children) (Kb): 84120

Verifier Data

ERROR: no interpretation found !