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/miplib3/normalized-mps-v2-13-7-egout.opb
MD5SUMfd101f0ba1a3813e843a38997ab7ed84
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 benchmark1246.13
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 6189

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        785220 kB
Buffers:         38492 kB
Cached:         183640 kB
SwapCached:        228 kB
Active:          83860 kB
Inactive:       141236 kB
HighTotal:      131008 kB
HighFree:         6160 kB
LowTotal:       903652 kB
LowFree:        779060 kB
SwapTotal:     2097136 kB
SwapFree:      2096756 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6280 kB
Slab:            18668 kB
Committed_AS:    64148 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 04:34:40 (client local time) WITH STATUS 10 IN 1209.39 SECONDS
stats: 3352 7 1209.39 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/14531/stat): 14531 (minisat+_script) R 14530 14531 22582 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1797383461 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/14531/statm): 174 3 169 147 0 27 0
[pid=14531] 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=14532
New process pid=14533
New process pid=14534
execve syscall for /bin/sed executable
One traced child (pid=14533) 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=14534) exited with status: 0
One traced child (pid=14532) exited with status: 0
New process pid=14535
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-egout.opb

[startup+10.004 s]
Raw data (loadavg): 0.93 0.95 0.90 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 7994 0 0 0 932 32 0 0 25 0 1 0 1797383466 35749888 7665 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14535/statm): 8728 7665 145 145 0 8583 0
[pid=14535] vsize: 34912
Current children cumulated CPU time (s) 9.66
Current children cumulated vsize (Kb) 37036

[startup+20.0046 s]
Raw data (loadavg): 0.94 0.96 0.91 1/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) T 14531 14531 22582 0 -1 0 8301 0 0 0 1930 33 0 0 25 0 1 0 1797383466 36872192 7972 4294967295 134512640 135094434 3221224432 3221219788 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/14535/statm): 9002 7972 145 145 0 8857 0
[pid=14535] vsize: 36008
Current children cumulated CPU time (s) 19.65
Current children cumulated vsize (Kb) 38132

[startup+30.0052 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 16568 0 0 0 2862 69 0 0 25 0 1 0 1797383466 73404416 15909 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14535/statm): 17921 15909 145 145 0 17776 0
[pid=14535] vsize: 71684
Current children cumulated CPU time (s) 29.33
Current children cumulated vsize (Kb) 73808

[startup+40.0057 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 16653 0 0 0 3861 69 0 0 25 0 1 0 1797383466 73613312 15994 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 17972 15994 145 145 0 17827 0
[pid=14535] vsize: 71888
Current children cumulated CPU time (s) 39.32
Current children cumulated vsize (Kb) 74012

[startup+50.0062 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 16815 0 0 0 4860 70 0 0 25 0 1 0 1797383466 73949184 16156 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18054 16156 145 145 0 17909 0
[pid=14535] vsize: 72216
Current children cumulated CPU time (s) 49.32
Current children cumulated vsize (Kb) 74340

[startup+60.0068 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 16905 0 0 0 5860 70 0 0 25 0 1 0 1797383466 73969664 16168 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14535/statm): 18059 16168 145 145 0 17914 0
[pid=14535] vsize: 72236
Current children cumulated CPU time (s) 59.32
Current children cumulated vsize (Kb) 74360

[startup+70.0074 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 16918 0 0 0 6858 71 0 0 25 0 1 0 1797383466 74018816 16181 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18071 16181 145 145 0 17926 0
[pid=14535] vsize: 72284
Current children cumulated CPU time (s) 69.31
Current children cumulated vsize (Kb) 74408

[startup+80.0079 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 16941 0 0 0 7858 71 0 0 25 0 1 0 1797383466 74113024 16204 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18094 16204 145 145 0 17949 0
[pid=14535] vsize: 72376
Current children cumulated CPU time (s) 79.31
Current children cumulated vsize (Kb) 74500

[startup+90.0085 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 16979 0 0 0 8858 71 0 0 25 0 1 0 1797383466 74268672 16242 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18132 16242 145 145 0 17987 0
[pid=14535] vsize: 72528
Current children cumulated CPU time (s) 89.31
Current children cumulated vsize (Kb) 74652

[startup+100.009 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17078 0 0 0 9857 72 0 0 25 0 1 0 1797383466 74522624 16305 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18194 16305 145 145 0 18049 0
[pid=14535] vsize: 72776
Current children cumulated CPU time (s) 99.31
Current children cumulated vsize (Kb) 74900

[startup+110.01 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17139 0 0 0 10857 72 0 0 25 0 1 0 1797383466 74477568 16294 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18183 16294 145 145 0 18038 0
[pid=14535] vsize: 72732
Current children cumulated CPU time (s) 109.31
Current children cumulated vsize (Kb) 74856

[startup+120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17200 0 0 0 11856 72 0 0 25 0 1 0 1797383466 74567680 16316 4294967295 134512640 135094434 3221224432 3221222160 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18205 16316 145 145 0 18060 0
[pid=14535] vsize: 72820
Current children cumulated CPU time (s) 119.3
Current children cumulated vsize (Kb) 74944

[startup+130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17236 0 0 0 12856 72 0 0 25 0 1 0 1797383466 74559488 16315 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18203 16315 145 145 0 18058 0
[pid=14535] vsize: 72812
Current children cumulated CPU time (s) 129.3
Current children cumulated vsize (Kb) 74936

[startup+140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17278 0 0 0 13856 73 0 0 25 0 1 0 1797383466 74760192 16357 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18252 16357 145 145 0 18107 0
[pid=14535] vsize: 73008
Current children cumulated CPU time (s) 139.31
Current children cumulated vsize (Kb) 75132

[startup+150.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17395 0 0 0 14855 74 0 0 25 0 1 0 1797383466 75280384 16474 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18379 16474 145 145 0 18234 0
[pid=14535] vsize: 73516
Current children cumulated CPU time (s) 149.31
Current children cumulated vsize (Kb) 75640

[startup+160.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17410 0 0 0 15854 74 0 0 25 0 1 0 1797383466 75337728 16489 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18393 16489 145 145 0 18248 0
[pid=14535] vsize: 73572
Current children cumulated CPU time (s) 159.3
Current children cumulated vsize (Kb) 75696

[startup+170.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17447 0 0 0 16854 74 0 0 25 0 1 0 1797383466 75489280 16526 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18430 16526 145 145 0 18285 0
[pid=14535] vsize: 73720
Current children cumulated CPU time (s) 169.3
Current children cumulated vsize (Kb) 75844

[startup+180.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17456 0 0 0 17855 74 0 0 25 0 1 0 1797383466 75526144 16535 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18439 16535 145 145 0 18294 0
[pid=14535] vsize: 73756
Current children cumulated CPU time (s) 179.31
Current children cumulated vsize (Kb) 75880

[startup+190.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17465 0 0 0 18855 74 0 0 25 0 1 0 1797383466 75558912 16544 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18447 16544 145 145 0 18302 0
[pid=14535] vsize: 73788
Current children cumulated CPU time (s) 189.31
Current children cumulated vsize (Kb) 75912

[startup+200.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17474 0 0 0 19855 74 0 0 25 0 1 0 1797383466 75595776 16553 4294967295 134512640 135094434 3221224432 3221223056 134557568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18456 16553 145 145 0 18311 0
[pid=14535] vsize: 73824
Current children cumulated CPU time (s) 199.31
Current children cumulated vsize (Kb) 75948

[startup+210.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17505 0 0 0 20855 74 0 0 25 0 1 0 1797383466 75735040 16584 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18490 16584 145 145 0 18345 0
[pid=14535] vsize: 73960
Current children cumulated CPU time (s) 209.31
Current children cumulated vsize (Kb) 76084

[startup+220.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17587 0 0 0 21855 74 0 0 25 0 1 0 1797383466 76107776 16666 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18581 16666 145 145 0 18436 0
[pid=14535] vsize: 74324
Current children cumulated CPU time (s) 219.31
Current children cumulated vsize (Kb) 76448

[startup+230.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17588 0 0 0 22855 74 0 0 25 0 1 0 1797383466 76107776 16667 4294967295 134512640 135094434 3221224432 3221223084 134675711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18581 16667 145 145 0 18436 0
[pid=14535] vsize: 74324
Current children cumulated CPU time (s) 229.31
Current children cumulated vsize (Kb) 76448

[startup+240.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17588 0 0 0 23855 74 0 0 25 0 1 0 1797383466 76107776 16667 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18581 16667 145 145 0 18436 0
[pid=14535] vsize: 74324
Current children cumulated CPU time (s) 239.31
Current children cumulated vsize (Kb) 76448

[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17653 0 0 0 24855 75 0 0 25 0 1 0 1797383466 76070912 16657 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18572 16657 145 145 0 18427 0
[pid=14535] vsize: 74288
Current children cumulated CPU time (s) 249.32
Current children cumulated vsize (Kb) 76412

[startup+260.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17667 0 0 0 25855 75 0 0 25 0 1 0 1797383466 76120064 16671 4294967295 134512640 135094434 3221224432 3221222976 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18584 16671 145 145 0 18439 0
[pid=14535] vsize: 74336
Current children cumulated CPU time (s) 259.32
Current children cumulated vsize (Kb) 76460

[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17678 0 0 0 26854 75 0 0 25 0 1 0 1797383466 76165120 16682 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18595 16682 145 145 0 18450 0
[pid=14535] vsize: 74380
Current children cumulated CPU time (s) 269.31
Current children cumulated vsize (Kb) 76504

[startup+280.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17715 0 0 0 27854 75 0 0 25 0 1 0 1797383466 76316672 16719 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18632 16719 145 145 0 18487 0
[pid=14535] vsize: 74528
Current children cumulated CPU time (s) 279.31
Current children cumulated vsize (Kb) 76652

[startup+290.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17827 0 0 0 28854 76 0 0 25 0 1 0 1797383466 76611584 16792 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18704 16792 145 145 0 18559 0
[pid=14535] vsize: 74816
Current children cumulated CPU time (s) 289.32
Current children cumulated vsize (Kb) 76940

[startup+300.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17904 0 0 0 29853 76 0 0 25 0 1 0 1797383466 76619776 16794 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18706 16794 145 145 0 18561 0
[pid=14535] vsize: 74824
Current children cumulated CPU time (s) 299.31
Current children cumulated vsize (Kb) 76948

[startup+310.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17933 0 0 0 30853 76 0 0 25 0 1 0 1797383466 76738560 16823 4294967295 134512640 135094434 3221224432 3221223024 134557196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18735 16823 145 145 0 18590 0
[pid=14535] vsize: 74940
Current children cumulated CPU time (s) 309.31
Current children cumulated vsize (Kb) 77064

[startup+320.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 17953 0 0 0 31854 76 0 0 25 0 1 0 1797383466 76816384 16843 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18754 16843 145 145 0 18609 0
[pid=14535] vsize: 75016
Current children cumulated CPU time (s) 319.32
Current children cumulated vsize (Kb) 77140

[startup+330.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18037 0 0 0 32852 77 0 0 25 0 1 0 1797383466 77217792 16927 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18852 16927 145 145 0 18707 0
[pid=14535] vsize: 75408
Current children cumulated CPU time (s) 329.31
Current children cumulated vsize (Kb) 77532

[startup+340.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18086 0 0 0 33852 77 0 0 25 0 1 0 1797383466 77414400 16976 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18900 16976 145 145 0 18755 0
[pid=14535] vsize: 75600
Current children cumulated CPU time (s) 339.31
Current children cumulated vsize (Kb) 77724

[startup+350.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18099 0 0 0 34852 77 0 0 25 0 1 0 1797383466 77467648 16989 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18913 16989 145 145 0 18768 0
[pid=14535] vsize: 75652
Current children cumulated CPU time (s) 349.31
Current children cumulated vsize (Kb) 77776

[startup+360.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18187 0 0 0 35852 78 0 0 25 0 1 0 1797383466 77529088 17001 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18928 17001 145 145 0 18783 0
[pid=14535] vsize: 75712
Current children cumulated CPU time (s) 359.32
Current children cumulated vsize (Kb) 77836

[startup+370.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18200 0 0 0 36851 78 0 0 25 0 1 0 1797383466 77565952 17014 4294967295 134512640 135094434 3221224432 3221223088 134557984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18937 17014 145 145 0 18792 0
[pid=14535] vsize: 75748
Current children cumulated CPU time (s) 369.31
Current children cumulated vsize (Kb) 77872

[startup+380.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18215 0 0 0 37852 78 0 0 25 0 1 0 1797383466 77627392 17029 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18952 17029 145 145 0 18807 0
[pid=14535] vsize: 75808
Current children cumulated CPU time (s) 379.32
Current children cumulated vsize (Kb) 77932

[startup+390.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18233 0 0 0 38851 78 0 0 25 0 1 0 1797383466 77701120 17047 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18970 17047 145 145 0 18825 0
[pid=14535] vsize: 75880
Current children cumulated CPU time (s) 389.31
Current children cumulated vsize (Kb) 78004

[startup+400.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18243 0 0 0 39851 78 0 0 25 0 1 0 1797383466 77742080 17057 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 18980 17057 145 145 0 18835 0
[pid=14535] vsize: 75920
Current children cumulated CPU time (s) 399.31
Current children cumulated vsize (Kb) 78044

[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18276 0 0 0 40851 78 0 0 25 0 1 0 1797383466 77873152 17090 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19012 17090 145 145 0 18867 0
[pid=14535] vsize: 76048
Current children cumulated CPU time (s) 409.31
Current children cumulated vsize (Kb) 78172

[startup+420.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18362 0 0 0 41850 79 0 0 25 0 1 0 1797383466 78065664 17137 4294967295 134512640 135094434 3221224432 3221220752 134677310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19059 17137 145 145 0 18914 0
[pid=14535] vsize: 76236
Current children cumulated CPU time (s) 419.31
Current children cumulated vsize (Kb) 78360

[startup+430.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18397 0 0 0 42850 79 0 0 25 0 1 0 1797383466 78053376 17134 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19056 17134 145 145 0 18911 0
[pid=14535] vsize: 76224
Current children cumulated CPU time (s) 429.31
Current children cumulated vsize (Kb) 78348

[startup+440.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18488 0 0 0 43850 79 0 0 25 0 1 0 1797383466 78114816 17149 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19071 17149 145 145 0 18926 0
[pid=14535] vsize: 76284
Current children cumulated CPU time (s) 439.31
Current children cumulated vsize (Kb) 78408

[startup+450.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18508 0 0 0 44849 80 0 0 25 0 1 0 1797383466 78196736 17169 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19091 17169 145 145 0 18946 0
[pid=14535] vsize: 76364
Current children cumulated CPU time (s) 449.31
Current children cumulated vsize (Kb) 78488

[startup+460.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18535 0 0 0 45850 80 0 0 25 0 1 0 1797383466 78303232 17196 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19117 17196 145 145 0 18972 0
[pid=14535] vsize: 76468
Current children cumulated CPU time (s) 459.32
Current children cumulated vsize (Kb) 78592

[startup+470.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18554 0 0 0 46850 80 0 0 25 0 1 0 1797383466 78376960 17215 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19135 17215 145 145 0 18990 0
[pid=14535] vsize: 76540
Current children cumulated CPU time (s) 469.32
Current children cumulated vsize (Kb) 78664

[startup+480.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18568 0 0 0 47850 80 0 0 25 0 1 0 1797383466 78434304 17229 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19149 17229 145 145 0 19004 0
[pid=14535] vsize: 76596
Current children cumulated CPU time (s) 479.32
Current children cumulated vsize (Kb) 78720

[startup+490.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18583 0 0 0 48849 80 0 0 25 0 1 0 1797383466 78495744 17244 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19164 17244 145 145 0 19019 0
[pid=14535] vsize: 76656
Current children cumulated CPU time (s) 489.31
Current children cumulated vsize (Kb) 78780

[startup+500.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18609 0 0 0 49850 80 0 0 25 0 1 0 1797383466 78602240 17270 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19190 17270 145 145 0 19045 0
[pid=14535] vsize: 76760
Current children cumulated CPU time (s) 499.32
Current children cumulated vsize (Kb) 78884

[startup+510.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18702 0 0 0 50849 81 0 0 25 0 1 0 1797383466 78823424 17324 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19244 17324 145 145 0 19099 0
[pid=14535] vsize: 76976
Current children cumulated CPU time (s) 509.32
Current children cumulated vsize (Kb) 79100

[startup+520.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18865 0 0 0 51848 81 0 0 25 0 1 0 1797383466 78868480 17336 4294967295 134512640 135094434 3221224432 3221221516 134677228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19255 17336 145 145 0 19110 0
[pid=14535] vsize: 77020
Current children cumulated CPU time (s) 519.31
Current children cumulated vsize (Kb) 79144

[startup+530.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18898 0 0 0 52848 81 0 0 25 0 1 0 1797383466 78856192 17333 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19252 17333 145 145 0 19107 0
[pid=14535] vsize: 77008
Current children cumulated CPU time (s) 529.31
Current children cumulated vsize (Kb) 79132

[startup+540.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18926 0 0 0 53848 82 0 0 25 0 1 0 1797383466 78970880 17361 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19280 17361 145 145 0 19135 0
[pid=14535] vsize: 77120
Current children cumulated CPU time (s) 539.32
Current children cumulated vsize (Kb) 79244

[startup+550.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18949 0 0 0 54848 82 0 0 25 0 1 0 1797383466 79065088 17384 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19303 17384 145 145 0 19158 0
[pid=14535] vsize: 77212
Current children cumulated CPU time (s) 549.32
Current children cumulated vsize (Kb) 79336

[startup+560.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18965 0 0 0 55848 82 0 0 25 0 1 0 1797383466 79126528 17400 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19318 17400 145 145 0 19173 0
[pid=14535] vsize: 77272
Current children cumulated CPU time (s) 559.32
Current children cumulated vsize (Kb) 79396

[startup+570.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 18982 0 0 0 56847 82 0 0 25 0 1 0 1797383466 79196160 17417 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19335 17417 145 145 0 19190 0
[pid=14535] vsize: 77340
Current children cumulated CPU time (s) 569.31
Current children cumulated vsize (Kb) 79464

[startup+580.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19006 0 0 0 57847 82 0 0 25 0 1 0 1797383466 79294464 17441 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19359 17441 145 145 0 19214 0
[pid=14535] vsize: 77436
Current children cumulated CPU time (s) 579.31
Current children cumulated vsize (Kb) 79560

[startup+590.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19032 0 0 0 58847 82 0 0 25 0 1 0 1797383466 79396864 17467 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19384 17467 145 145 0 19239 0
[pid=14535] vsize: 77536
Current children cumulated CPU time (s) 589.31
Current children cumulated vsize (Kb) 79660

[startup+600.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19101 0 0 0 59847 83 0 0 25 0 1 0 1797383466 79515648 17496 4294967295 134512640 135094434 3221224432 3221222224 134677091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19413 17496 145 145 0 19268 0
[pid=14535] vsize: 77652
Current children cumulated CPU time (s) 599.32
Current children cumulated vsize (Kb) 79776

[startup+610.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19146 0 0 0 60846 83 0 0 25 0 1 0 1797383466 79548416 17505 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19421 17505 145 145 0 19276 0
[pid=14535] vsize: 77684
Current children cumulated CPU time (s) 609.31
Current children cumulated vsize (Kb) 79808

[startup+620.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19157 0 0 0 61846 83 0 0 25 0 1 0 1797383466 79585280 17516 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19430 17516 145 145 0 19285 0
[pid=14535] vsize: 77720
Current children cumulated CPU time (s) 619.31
Current children cumulated vsize (Kb) 79844

[startup+630.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19181 0 0 0 62846 84 0 0 25 0 1 0 1797383466 79683584 17540 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19454 17540 145 145 0 19309 0
[pid=14535] vsize: 77816
Current children cumulated CPU time (s) 629.32
Current children cumulated vsize (Kb) 79940

[startup+640.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19195 0 0 0 63846 84 0 0 25 0 1 0 1797383466 79745024 17554 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19469 17554 145 145 0 19324 0
[pid=14535] vsize: 77876
Current children cumulated CPU time (s) 639.32
Current children cumulated vsize (Kb) 80000

[startup+650.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19280 0 0 0 64845 84 0 0 25 0 1 0 1797383466 79773696 17562 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19476 17562 145 145 0 19331 0
[pid=14535] vsize: 77904
Current children cumulated CPU time (s) 649.31
Current children cumulated vsize (Kb) 80028

[startup+660.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19291 0 0 0 65845 84 0 0 25 0 1 0 1797383466 79814656 17573 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19486 17573 145 145 0 19341 0
[pid=14535] vsize: 77944
Current children cumulated CPU time (s) 659.31
Current children cumulated vsize (Kb) 80068

[startup+670.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19307 0 0 0 66845 85 0 0 25 0 1 0 1797383466 79880192 17589 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19502 17589 145 145 0 19357 0
[pid=14535] vsize: 78008
Current children cumulated CPU time (s) 669.32
Current children cumulated vsize (Kb) 80132

[startup+680.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19320 0 0 0 67845 85 0 0 25 0 1 0 1797383466 79933440 17602 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19515 17602 145 145 0 19370 0
[pid=14535] vsize: 78060
Current children cumulated CPU time (s) 679.32
Current children cumulated vsize (Kb) 80184

[startup+690.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19333 0 0 0 68844 85 0 0 25 0 1 0 1797383466 79986688 17615 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19528 17615 145 145 0 19383 0
[pid=14535] vsize: 78112
Current children cumulated CPU time (s) 689.31
Current children cumulated vsize (Kb) 80236

[startup+700.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19365 0 0 0 69844 85 0 0 25 0 1 0 1797383466 80121856 17647 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19561 17647 145 145 0 19416 0
[pid=14535] vsize: 78244
Current children cumulated CPU time (s) 699.31
Current children cumulated vsize (Kb) 80368

[startup+710.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19399 0 0 0 70844 85 0 0 25 0 1 0 1797383466 80257024 17681 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19594 17681 145 145 0 19449 0
[pid=14535] vsize: 78376
Current children cumulated CPU time (s) 709.31
Current children cumulated vsize (Kb) 80500

[startup+720.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19408 0 0 0 71844 85 0 0 25 0 1 0 1797383466 80289792 17690 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19602 17690 145 145 0 19457 0
[pid=14535] vsize: 78408
Current children cumulated CPU time (s) 719.31
Current children cumulated vsize (Kb) 80532

[startup+730.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19414 0 0 0 72845 85 0 0 25 0 1 0 1797383466 80314368 17696 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19608 17696 145 145 0 19463 0
[pid=14535] vsize: 78432
Current children cumulated CPU time (s) 729.32
Current children cumulated vsize (Kb) 80556

[startup+740.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19414 0 0 0 73845 85 0 0 25 0 1 0 1797383466 80314368 17696 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19608 17696 145 145 0 19463 0
[pid=14535] vsize: 78432
Current children cumulated CPU time (s) 739.32
Current children cumulated vsize (Kb) 80556

[startup+750.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19431 0 0 0 74845 85 0 0 25 0 1 0 1797383466 80384000 17713 4294967295 134512640 135094434 3221224432 3221223120 134554742 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19625 17713 145 145 0 19480 0
[pid=14535] vsize: 78500
Current children cumulated CPU time (s) 749.32
Current children cumulated vsize (Kb) 80624

[startup+760.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19521 0 0 0 75845 85 0 0 25 0 1 0 1797383466 80441344 17727 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19639 17727 145 145 0 19494 0
[pid=14535] vsize: 78556
Current children cumulated CPU time (s) 759.32
Current children cumulated vsize (Kb) 80680

[startup+770.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19542 0 0 0 76845 86 0 0 25 0 1 0 1797383466 80527360 17748 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19660 17748 145 145 0 19515 0
[pid=14535] vsize: 78640
Current children cumulated CPU time (s) 769.33
Current children cumulated vsize (Kb) 80764

[startup+780.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19553 0 0 0 77845 86 0 0 25 0 1 0 1797383466 80572416 17759 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19671 17759 145 145 0 19526 0
[pid=14535] vsize: 78684
Current children cumulated CPU time (s) 779.33
Current children cumulated vsize (Kb) 80808

[startup+790.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19565 0 0 0 78845 86 0 0 25 0 1 0 1797383466 80617472 17771 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19682 17771 145 145 0 19537 0
[pid=14535] vsize: 78728
Current children cumulated CPU time (s) 789.33
Current children cumulated vsize (Kb) 80852

[startup+800.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19583 0 0 0 79845 86 0 0 25 0 1 0 1797383466 80695296 17789 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19701 17789 145 145 0 19556 0
[pid=14535] vsize: 78804
Current children cumulated CPU time (s) 799.33
Current children cumulated vsize (Kb) 80928

[startup+810.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19597 0 0 0 80845 86 0 0 25 0 1 0 1797383466 80748544 17803 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19714 17803 145 145 0 19569 0
[pid=14535] vsize: 78856
Current children cumulated CPU time (s) 809.33
Current children cumulated vsize (Kb) 80980

[startup+820.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19614 0 0 0 81845 86 0 0 25 0 1 0 1797383466 80814080 17820 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19730 17820 145 145 0 19585 0
[pid=14535] vsize: 78920
Current children cumulated CPU time (s) 819.33
Current children cumulated vsize (Kb) 81044

[startup+830.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19634 0 0 0 82845 86 0 0 25 0 1 0 1797383466 80896000 17840 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19750 17840 145 145 0 19605 0
[pid=14535] vsize: 79000
Current children cumulated CPU time (s) 829.33
Current children cumulated vsize (Kb) 81124

[startup+840.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19652 0 0 0 83845 86 0 0 25 0 1 0 1797383466 80969728 17858 4294967295 134512640 135094434 3221224432 3221223024 134556961 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19768 17858 145 145 0 19623 0
[pid=14535] vsize: 79072
Current children cumulated CPU time (s) 839.33
Current children cumulated vsize (Kb) 81196

[startup+850.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19666 0 0 0 84845 86 0 0 25 0 1 0 1797383466 81027072 17872 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19782 17872 145 145 0 19637 0
[pid=14535] vsize: 79128
Current children cumulated CPU time (s) 849.33
Current children cumulated vsize (Kb) 81252

[startup+860.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19684 0 0 0 85844 86 0 0 25 0 1 0 1797383466 81096704 17890 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19799 17890 145 145 0 19654 0
[pid=14535] vsize: 79196
Current children cumulated CPU time (s) 859.32
Current children cumulated vsize (Kb) 81320

[startup+870.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19693 0 0 0 86844 87 0 0 25 0 1 0 1797383466 81133568 17899 4294967295 134512640 135094434 3221224432 3221223056 134562139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19808 17899 145 145 0 19663 0
[pid=14535] vsize: 79232
Current children cumulated CPU time (s) 869.33
Current children cumulated vsize (Kb) 81356

[startup+880.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19708 0 0 0 87844 87 0 0 25 0 1 0 1797383466 81195008 17914 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19823 17914 145 145 0 19678 0
[pid=14535] vsize: 79292
Current children cumulated CPU time (s) 879.33
Current children cumulated vsize (Kb) 81416

[startup+890.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19723 0 0 0 88844 87 0 0 25 0 1 0 1797383466 81256448 17929 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19838 17929 145 145 0 19693 0
[pid=14535] vsize: 79352
Current children cumulated CPU time (s) 889.33
Current children cumulated vsize (Kb) 81476

[startup+900.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19761 0 0 0 89844 87 0 0 25 0 1 0 1797383466 81543168 17967 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19908 17967 145 145 0 19763 0
[pid=14535] vsize: 79632
Current children cumulated CPU time (s) 899.33
Current children cumulated vsize (Kb) 81756

[startup+910.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19817 0 0 0 90844 87 0 0 25 0 1 0 1797383466 81608704 17984 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19924 17984 145 145 0 19779 0
[pid=14535] vsize: 79696
Current children cumulated CPU time (s) 909.33
Current children cumulated vsize (Kb) 81820

[startup+920.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19817 0 0 0 91844 87 0 0 25 0 1 0 1797383466 81608704 17984 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19924 17984 145 145 0 19779 0
[pid=14535] vsize: 79696
Current children cumulated CPU time (s) 919.33
Current children cumulated vsize (Kb) 81820

[startup+930.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19830 0 0 0 92844 87 0 0 25 0 1 0 1797383466 81666048 17997 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19938 17997 145 145 0 19793 0
[pid=14535] vsize: 79752
Current children cumulated CPU time (s) 929.33
Current children cumulated vsize (Kb) 81876

[startup+940.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19848 0 0 0 93844 87 0 0 25 0 1 0 1797383466 81739776 18015 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19956 18015 145 145 0 19811 0
[pid=14535] vsize: 79824
Current children cumulated CPU time (s) 939.33
Current children cumulated vsize (Kb) 81948

[startup+950.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19864 0 0 0 94844 88 0 0 25 0 1 0 1797383466 81801216 18031 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19971 18031 145 145 0 19826 0
[pid=14535] vsize: 79884
Current children cumulated CPU time (s) 949.34
Current children cumulated vsize (Kb) 82008

[startup+960.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19884 0 0 0 95844 88 0 0 25 0 1 0 1797383466 81883136 18051 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 19991 18051 145 145 0 19846 0
[pid=14535] vsize: 79964
Current children cumulated CPU time (s) 959.34
Current children cumulated vsize (Kb) 82088

[startup+970.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19908 0 0 0 96844 88 0 0 25 0 1 0 1797383466 81985536 18075 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20016 18075 145 145 0 19871 0
[pid=14535] vsize: 80064
Current children cumulated CPU time (s) 969.34
Current children cumulated vsize (Kb) 82188

[startup+980.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19922 0 0 0 97844 88 0 0 25 0 1 0 1797383466 82034688 18089 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20028 18089 145 145 0 19883 0
[pid=14535] vsize: 80112
Current children cumulated CPU time (s) 979.34
Current children cumulated vsize (Kb) 82236

[startup+990.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19937 0 0 0 98845 88 0 0 25 0 1 0 1797383466 82092032 18104 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20042 18104 145 145 0 19897 0
[pid=14535] vsize: 80168
Current children cumulated CPU time (s) 989.35
Current children cumulated vsize (Kb) 82292

[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19959 0 0 0 99845 88 0 0 25 0 1 0 1797383466 82186240 18126 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20065 18126 145 145 0 19920 0
[pid=14535] vsize: 80260
Current children cumulated CPU time (s) 999.35
Current children cumulated vsize (Kb) 82384

[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19971 0 0 0 100845 88 0 0 25 0 1 0 1797383466 82231296 18138 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20076 18138 145 145 0 19931 0
[pid=14535] vsize: 80304
Current children cumulated CPU time (s) 1009.35
Current children cumulated vsize (Kb) 82428

[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 19989 0 0 0 101845 88 0 0 25 0 1 0 1797383466 82305024 18156 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20094 18156 145 145 0 19949 0
[pid=14535] vsize: 80376
Current children cumulated CPU time (s) 1019.35
Current children cumulated vsize (Kb) 82500

[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) T 14531 14531 22582 0 -1 0 20008 0 0 0 102845 88 0 0 25 0 1 0 1797383466 82391040 18175 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20115 18175 145 145 0 19970 0
[pid=14535] vsize: 80460
Current children cumulated CPU time (s) 1029.35
Current children cumulated vsize (Kb) 82584

[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20034 0 0 0 103845 88 0 0 25 0 1 0 1797383466 82497536 18201 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20141 18201 145 145 0 19996 0
[pid=14535] vsize: 80564
Current children cumulated CPU time (s) 1039.35
Current children cumulated vsize (Kb) 82688

[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20113 0 0 0 104844 89 0 0 25 0 1 0 1797383466 82825216 18280 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20221 18280 145 145 0 20076 0
[pid=14535] vsize: 80884
Current children cumulated CPU time (s) 1049.35
Current children cumulated vsize (Kb) 83008

[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20141 0 0 0 105844 89 0 0 25 0 1 0 1797383466 82927616 18308 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20246 18308 145 145 0 20101 0
[pid=14535] vsize: 80984
Current children cumulated CPU time (s) 1059.35
Current children cumulated vsize (Kb) 83108

[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20161 0 0 0 106844 89 0 0 25 0 1 0 1797383466 83009536 18328 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20266 18328 145 145 0 20121 0
[pid=14535] vsize: 81064
Current children cumulated CPU time (s) 1069.35
Current children cumulated vsize (Kb) 83188

[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20192 0 0 0 107844 89 0 0 25 0 1 0 1797383466 83136512 18359 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20297 18359 145 145 0 20152 0
[pid=14535] vsize: 81188
Current children cumulated CPU time (s) 1079.35
Current children cumulated vsize (Kb) 83312

[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20210 0 0 0 108843 89 0 0 25 0 1 0 1797383466 83206144 18377 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20314 18377 145 145 0 20169 0
[pid=14535] vsize: 81256
Current children cumulated CPU time (s) 1089.34
Current children cumulated vsize (Kb) 83380

[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20236 0 0 0 109843 90 0 0 25 0 1 0 1797383466 83312640 18403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20340 18403 145 145 0 20195 0
[pid=14535] vsize: 81360
Current children cumulated CPU time (s) 1099.35
Current children cumulated vsize (Kb) 83484

[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20253 0 0 0 110843 90 0 0 25 0 1 0 1797383466 83382272 18420 4294967295 134512640 135094434 3221224432 3221223024 134557372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20357 18420 145 145 0 20212 0
[pid=14535] vsize: 81428
Current children cumulated CPU time (s) 1109.35
Current children cumulated vsize (Kb) 83552

[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20275 0 0 0 111843 90 0 0 25 0 1 0 1797383466 83476480 18442 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20380 18442 145 145 0 20235 0
[pid=14535] vsize: 81520
Current children cumulated CPU time (s) 1119.35
Current children cumulated vsize (Kb) 83644

[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20289 0 0 0 112843 90 0 0 25 0 1 0 1797383466 83537920 18456 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20395 18456 145 145 0 20250 0
[pid=14535] vsize: 81580
Current children cumulated CPU time (s) 1129.35
Current children cumulated vsize (Kb) 83704

[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20312 0 0 0 113843 90 0 0 25 0 1 0 1797383466 83632128 18479 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20418 18479 145 145 0 20273 0
[pid=14535] vsize: 81672
Current children cumulated CPU time (s) 1139.35
Current children cumulated vsize (Kb) 83796

[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20330 0 0 0 114843 90 0 0 25 0 1 0 1797383466 83701760 18497 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20435 18497 145 145 0 20290 0
[pid=14535] vsize: 81740
Current children cumulated CPU time (s) 1149.35
Current children cumulated vsize (Kb) 83864

[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20351 0 0 0 115844 90 0 0 25 0 1 0 1797383466 83787776 18518 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20456 18518 145 145 0 20311 0
[pid=14535] vsize: 81824
Current children cumulated CPU time (s) 1159.36
Current children cumulated vsize (Kb) 83948

[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20366 0 0 0 116843 90 0 0 25 0 1 0 1797383466 83853312 18533 4294967295 134512640 135094434 3221224432 3221223088 134558281 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20472 18533 145 145 0 20327 0
[pid=14535] vsize: 81888
Current children cumulated CPU time (s) 1169.35
Current children cumulated vsize (Kb) 84012

[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20372 0 0 0 117844 90 0 0 25 0 1 0 1797383466 83873792 18539 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20477 18539 145 145 0 20332 0
[pid=14535] vsize: 81908
Current children cumulated CPU time (s) 1179.36
Current children cumulated vsize (Kb) 84032

[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20387 0 0 0 118844 91 0 0 25 0 1 0 1797383466 83931136 18554 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20491 18554 145 145 0 20346 0
[pid=14535] vsize: 81964
Current children cumulated CPU time (s) 1189.37
Current children cumulated vsize (Kb) 84088

[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20401 0 0 0 119843 91 0 0 25 0 1 0 1797383466 83988480 18568 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20505 18568 145 145 0 20360 0
[pid=14535] vsize: 82020
Current children cumulated CPU time (s) 1199.36
Current children cumulated vsize (Kb) 84144

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20414 0 0 0 120844 91 0 0 25 0 1 0 1797383466 84054016 18581 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20521 18581 145 145 0 20376 0
[pid=14535] vsize: 82084
Current children cumulated CPU time (s) 1209.37
Current children cumulated vsize (Kb) 84208



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14535
Raw data (/proc/14531/stat): 14531 (minisat+_script) S 14530 14531 22582 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797383461 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14531/statm): 531 226 485 147 0 384 0
[pid=14531] vsize: 2124
Raw data (/proc/14535/stat): 14535 (minisat+_64-bit) R 14531 14531 22582 0 -1 0 20414 0 0 0 120844 91 0 0 25 0 1 0 1797383466 84054016 18581 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14535/statm): 20521 18581 145 145 0 20376 0
[pid=14535] vsize: 82084
Current children cumulated CPU time (s) 1209.37
Current children cumulated vsize (Kb) 84208

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

Child status: 10
Real time (s): 1210.11
CPU time (s): 1209.39
CPU user time (s): 1208.44
CPU system time (s): 0.948855
CPU usage (%): 99.9405
Max. virtual memory (cumulated for all children) (Kb): 84208

Verifier Data

ERROR: no interpretation found !