PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-egout.opb
MD5SUM	46c4db5f8baf54496e00a723c85beb20
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	58880896
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 numbers	34
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04084
Number of variables	1155
Total number of constraints	153
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	55
Number of constraints which are nor clauses,nor cardinality constraints	98
Minimum length of a constraint	1
Maximum length of a constraint	280
Trace number 15714

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-21 05:39:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16788 boxname=wulflinc15 idbench=1292 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  46c4db5f8baf54496e00a723c85beb20  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-egout.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-egout.opb
IDLAUNCH: 16788
/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:        715796 kB
Buffers:         33016 kB
Cached:         264248 kB
SwapCached:        440 kB
Active:          37780 kB
Inactive:       261696 kB
HighTotal:      131008 kB
HighFree:        30464 kB
LowTotal:       903652 kB
LowFree:        685332 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5360 kB
Slab:            13768 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 05:59:39 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 16788 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN 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 [1mFound solution: 98251161[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 90380944[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 83601220[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 75080280[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 72902771[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 70799895[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 68823191[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 66801712[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 65961920[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 65957568[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 64888022[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 64714286[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 64484352[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 64437712[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 64396544[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 62242606[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 62227456[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 61803904[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 61163008[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 61074176[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 60755072[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 60662144[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |     47100 |  503527  1182417 |  479053   22444   816272    36.4 | 11.519 % |
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#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.92 2/54 29214
Raw data (stat): 29214 (runsolver) R 29213 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 484402897 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.93 0.96 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 8199 0 0 0 976 21 0 0 25 0 1 0 484402897 37793792 7860 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9227 7860 603 41 0 9186 0
vsize: 36908
[startup+20.0006 s]
Raw data (loadavg): 0.94 0.96 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 13263 0 0 0 1967 30 0 0 25 0 1 0 484402897 62517248 12594 4294967295 134512640 134672761 3221224624 3221220592 134544722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15263 12594 603 41 0 15222 0
vsize: 61052
[startup+30.0011 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 16803 0 0 0 2958 39 0 0 25 0 1 0 484402897 75501568 16134 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18433 16134 603 41 0 18392 0
vsize: 73732
[startup+40.0006 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 16987 0 0 0 3957 40 0 0 25 0 1 0 484402897 75837440 16318 4294967295 134512640 134672761 3221224624 3221223760 134560622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18515 16318 603 41 0 18474 0
vsize: 74060
[startup+50.0011 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17039 0 0 0 4957 40 0 0 25 0 1 0 484402897 75890688 16350 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18528 16350 603 41 0 18487 0
vsize: 74112
[startup+60.0016 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17039 0 0 0 5956 40 0 0 25 0 1 0 484402897 75890688 16350 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18528 16350 603 41 0 18487 0
vsize: 74112
[startup+70.0021 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17066 0 0 0 6957 41 0 0 25 0 1 0 484402897 76025856 16377 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18561 16377 603 41 0 18520 0
vsize: 74244
[startup+80.0032 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17118 0 0 0 7956 41 0 0 25 0 1 0 484402897 76296192 16429 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18627 16429 603 41 0 18586 0
vsize: 74508
[startup+90.0032 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17190 0 0 0 8956 41 0 0 25 0 1 0 484402897 76431360 16483 4294967295 134512640 134672761 3221224624 3221220448 134544364 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18660 16483 603 41 0 18619 0
vsize: 74640
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17191 0 0 0 9955 42 0 0 25 0 1 0 484402897 76431360 16484 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18660 16484 603 41 0 18619 0
vsize: 74640
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17225 0 0 0 10954 42 0 0 25 0 1 0 484402897 76484608 16498 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18673 16498 603 41 0 18632 0
vsize: 74692
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17225 0 0 0 11954 42 0 0 25 0 1 0 484402897 76484608 16498 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18673 16498 603 41 0 18632 0
vsize: 74692
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17368 0 0 0 12954 42 0 0 25 0 1 0 484402897 77279232 16641 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18867 16641 603 41 0 18826 0
vsize: 75468
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17383 0 0 0 13954 42 0 0 25 0 1 0 484402897 77279232 16656 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18867 16656 603 41 0 18826 0
vsize: 75468
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17421 0 0 0 14954 42 0 0 25 0 1 0 484402897 77414400 16694 4294967295 134512640 134672761 3221224624 3221223792 134560808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18900 16694 603 41 0 18859 0
vsize: 75600
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17430 0 0 0 15954 42 0 0 25 0 1 0 484402897 77414400 16703 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18900 16703 603 41 0 18859 0
vsize: 75600
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17439 0 0 0 16955 42 0 0 25 0 1 0 484402897 77545472 16712 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18932 16712 603 41 0 18891 0
vsize: 75728
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17447 0 0 0 17955 42 0 0 25 0 1 0 484402897 77545472 16720 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18932 16720 603 41 0 18891 0
vsize: 75728
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17469 0 0 0 18955 42 0 0 25 0 1 0 484402897 77545472 16742 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18932 16742 603 41 0 18891 0
vsize: 75728
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17557 0 0 0 19955 43 0 0 25 0 1 0 484402897 77991936 16830 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19041 16830 603 41 0 19000 0
vsize: 76164
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17557 0 0 0 20955 43 0 0 25 0 1 0 484402897 77991936 16830 4294967295 134512640 134672761 3221224624 3221223776 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19041 16830 603 41 0 19000 0
vsize: 76164
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17557 0 0 0 21955 43 0 0 25 0 1 0 484402897 77991936 16830 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19041 16830 603 41 0 19000 0
vsize: 76164
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17595 0 0 0 22956 43 0 0 25 0 1 0 484402897 78032896 16851 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19051 16851 603 41 0 19010 0
vsize: 76204
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17595 0 0 0 23956 43 0 0 25 0 1 0 484402897 78032896 16851 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19051 16851 603 41 0 19010 0
vsize: 76204
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17600 0 0 0 24956 43 0 0 25 0 1 0 484402897 78168064 16856 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19084 16856 603 41 0 19043 0
vsize: 76336
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17719 0 0 0 25956 43 0 0 25 0 1 0 484402897 78479360 16961 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19160 16961 603 41 0 19119 0
vsize: 76640
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17754 0 0 0 26956 43 0 0 25 0 1 0 484402897 78548992 16978 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19177 16978 603 41 0 19136 0
vsize: 76708
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17760 0 0 0 27956 43 0 0 25 0 1 0 484402897 78667776 16984 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19206 16984 603 41 0 19165 0
vsize: 76824
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17783 0 0 0 28956 43 0 0 25 0 1 0 484402897 78667776 17007 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19206 17007 603 41 0 19165 0
vsize: 76824
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17863 0 0 0 29956 44 0 0 25 0 1 0 484402897 79138816 17087 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19321 17087 603 41 0 19280 0
vsize: 77284
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17908 0 0 0 30956 44 0 0 25 0 1 0 484402897 79273984 17132 4294967295 134512640 134672761 3221224624 3221223808 134558648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19354 17132 603 41 0 19313 0
vsize: 77416
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17932 0 0 0 31956 44 0 0 25 0 1 0 484402897 79409152 17156 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19387 17156 603 41 0 19346 0
vsize: 77548
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17991 0 0 0 32956 44 0 0 25 0 1 0 484402897 79478784 17194 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19404 17194 603 41 0 19363 0
vsize: 77616
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17991 0 0 0 33956 44 0 0 25 0 1 0 484402897 79478784 17194 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19404 17194 603 41 0 19363 0
vsize: 77616
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 17995 0 0 0 34956 44 0 0 25 0 1 0 484402897 79613952 17198 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19437 17198 603 41 0 19396 0
vsize: 77748
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18012 0 0 0 35956 44 0 0 25 0 1 0 484402897 79613952 17215 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19437 17215 603 41 0 19396 0
vsize: 77748
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18024 0 0 0 36957 44 0 0 25 0 1 0 484402897 79613952 17227 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19437 17227 603 41 0 19396 0
vsize: 77748
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18055 0 0 0 37956 44 0 0 25 0 1 0 484402897 79749120 17258 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19470 17258 603 41 0 19429 0
vsize: 77880
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18136 0 0 0 38957 44 0 0 25 0 1 0 484402897 79986688 17319 4294967295 134512640 134672761 3221224624 3221223924 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19528 17319 603 41 0 19487 0
vsize: 78112
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18137 0 0 0 39957 44 0 0 25 0 1 0 484402897 79986688 17320 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19528 17320 603 41 0 19487 0
vsize: 78112
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18178 0 0 0 40957 44 0 0 25 0 1 0 484402897 80068608 17340 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19548 17340 603 41 0 19507 0
vsize: 78192
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18185 0 0 0 41957 44 0 0 25 0 1 0 484402897 80195584 17347 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19579 17347 603 41 0 19538 0
vsize: 78316
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18210 0 0 0 42957 45 0 0 25 0 1 0 484402897 80195584 17372 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19579 17372 603 41 0 19538 0
vsize: 78316
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18226 0 0 0 43957 45 0 0 25 0 1 0 484402897 80326656 17388 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19611 17388 603 41 0 19570 0
vsize: 78444
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18241 0 0 0 44957 45 0 0 25 0 1 0 484402897 80326656 17403 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19611 17403 603 41 0 19570 0
vsize: 78444
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18257 0 0 0 45958 45 0 0 25 0 1 0 484402897 80457728 17419 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19643 17419 603 41 0 19602 0
vsize: 78572
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18310 0 0 0 46958 45 0 0 25 0 1 0 484402897 80715776 17472 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19706 17472 603 41 0 19665 0
vsize: 78824
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18416 0 0 0 47958 45 0 0 25 0 1 0 484402897 80797696 17520 4294967295 134512640 134672761 3221224624 3221222596 1075347030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19726 17520 603 41 0 19685 0
vsize: 78904
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18416 0 0 0 48958 45 0 0 25 0 1 0 484402897 80797696 17520 4294967295 134512640 134672761 3221224624 3221223792 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19726 17520 603 41 0 19685 0
vsize: 78904
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18431 0 0 0 49958 45 0 0 25 0 1 0 484402897 80932864 17535 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19759 17535 603 41 0 19718 0
vsize: 79036
[startup+510.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18450 0 0 0 50958 45 0 0 25 0 1 0 484402897 80932864 17554 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19759 17554 603 41 0 19718 0
vsize: 79036
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18468 0 0 0 51958 45 0 0 25 0 1 0 484402897 81063936 17572 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19791 17572 603 41 0 19750 0
vsize: 79164
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18486 0 0 0 52958 45 0 0 25 0 1 0 484402897 81199104 17590 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19824 17590 603 41 0 19783 0
vsize: 79296
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18512 0 0 0 53958 45 0 0 25 0 1 0 484402897 81199104 17616 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19824 17616 603 41 0 19783 0
vsize: 79296
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18533 0 0 0 54959 45 0 0 25 0 1 0 484402897 81326080 17637 4294967295 134512640 134672761 3221224624 3221223776 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19855 17637 603 41 0 19814 0
vsize: 79420
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18597 0 0 0 55959 45 0 0 25 0 1 0 484402897 81436672 17681 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19882 17681 603 41 0 19841 0
vsize: 79528
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18597 0 0 0 56959 45 0 0 25 0 1 0 484402897 81436672 17681 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19882 17681 603 41 0 19841 0
vsize: 79528
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18614 0 0 0 57959 45 0 0 25 0 1 0 484402897 81555456 17698 4294967295 134512640 134672761 3221224624 3221223824 134557814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19911 17698 603 41 0 19870 0
vsize: 79644
[startup+590.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18629 0 0 0 58959 46 0 0 25 0 1 0 484402897 81686528 17713 4294967295 134512640 134672761 3221224624 3221223792 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19943 17713 603 41 0 19902 0
vsize: 79772
[startup+600.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18692 0 0 0 59959 46 0 0 25 0 1 0 484402897 81735680 17755 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19955 17755 603 41 0 19914 0
vsize: 79820
[startup+610.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18692 0 0 0 60959 46 0 0 25 0 1 0 484402897 81735680 17755 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19955 17755 603 41 0 19914 0
vsize: 79820
[startup+620.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18692 0 0 0 61959 46 0 0 25 0 1 0 484402897 81735680 17755 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19955 17755 603 41 0 19914 0
vsize: 79820
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18700 0 0 0 62959 46 0 0 25 0 1 0 484402897 81858560 17763 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19985 17763 603 41 0 19944 0
vsize: 79940
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18719 0 0 0 63960 46 0 0 25 0 1 0 484402897 81858560 17782 4294967295 134512640 134672761 3221224624 3221223760 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19985 17782 603 41 0 19944 0
vsize: 79940
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18740 0 0 0 64960 46 0 0 25 0 1 0 484402897 81989632 17803 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20017 17803 603 41 0 19976 0
vsize: 80068
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18772 0 0 0 65960 46 0 0 25 0 1 0 484402897 82112512 17835 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20047 17835 603 41 0 20006 0
vsize: 80188
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18794 0 0 0 66960 46 0 0 25 0 1 0 484402897 82231296 17857 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20076 17857 603 41 0 20035 0
vsize: 80304
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18797 0 0 0 67960 46 0 0 25 0 1 0 484402897 82231296 17860 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20076 17860 603 41 0 20035 0
vsize: 80304
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18801 0 0 0 68960 46 0 0 25 0 1 0 484402897 82231296 17864 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20076 17864 603 41 0 20035 0
vsize: 80304
[startup+700.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18813 0 0 0 69961 46 0 0 25 0 1 0 484402897 82231296 17876 4294967295 134512640 134672761 3221224624 3221223728 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20076 17876 603 41 0 20035 0
vsize: 80304
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18882 0 0 0 70961 46 0 0 25 0 1 0 484402897 82427904 17925 4294967295 134512640 134672761 3221224624 3221223040 134597224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20124 17925 603 41 0 20083 0
vsize: 80496
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18882 0 0 0 71961 46 0 0 25 0 1 0 484402897 82427904 17925 4294967295 134512640 134672761 3221224624 3221223760 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20124 17925 603 41 0 20083 0
vsize: 80496
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18885 0 0 0 72961 46 0 0 25 0 1 0 484402897 82554880 17928 4294967295 134512640 134672761 3221224624 3221223776 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20155 17928 603 41 0 20114 0
vsize: 80620
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18897 0 0 0 73961 46 0 0 25 0 1 0 484402897 82554880 17940 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20155 17940 603 41 0 20114 0
vsize: 80620
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18910 0 0 0 74961 46 0 0 25 0 1 0 484402897 82554880 17953 4294967295 134512640 134672761 3221224624 3221223792 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20155 17953 603 41 0 20114 0
vsize: 80620
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18929 0 0 0 75962 46 0 0 25 0 1 0 484402897 82690048 17972 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20188 17972 603 41 0 20147 0
vsize: 80752
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18945 0 0 0 76962 46 0 0 25 0 1 0 484402897 82690048 17988 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20188 17988 603 41 0 20147 0
vsize: 80752
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18965 0 0 0 77962 47 0 0 25 0 1 0 484402897 82821120 18008 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20220 18008 603 41 0 20179 0
vsize: 80880
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18985 0 0 0 78962 47 0 0 25 0 1 0 484402897 82960384 18028 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20254 18028 603 41 0 20213 0
vsize: 81016
[startup+800.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 18998 0 0 0 79962 47 0 0 25 0 1 0 484402897 82960384 18041 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20254 18041 603 41 0 20213 0
vsize: 81016
[startup+810.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19014 0 0 0 80962 47 0 0 25 0 1 0 484402897 82960384 18057 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20254 18057 603 41 0 20213 0
vsize: 81016
[startup+820.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19024 0 0 0 81962 47 0 0 25 0 1 0 484402897 83091456 18067 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20286 18067 603 41 0 20245 0
vsize: 81144
[startup+830.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19039 0 0 0 82962 47 0 0 25 0 1 0 484402897 83091456 18082 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20286 18082 603 41 0 20245 0
vsize: 81144
[startup+840.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19054 0 0 0 83963 47 0 0 25 0 1 0 484402897 83218432 18097 4294967295 134512640 134672761 3221224624 3221223760 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 18097 603 41 0 20276 0
vsize: 81268
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19091 0 0 0 84963 47 0 0 25 0 1 0 484402897 83480576 18134 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20381 18134 603 41 0 20340 0
vsize: 81524
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19123 0 0 0 85963 47 0 0 25 0 1 0 484402897 83513344 18162 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20389 18162 603 41 0 20348 0
vsize: 81556
[startup+870.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19123 0 0 0 86963 47 0 0 25 0 1 0 484402897 83513344 18162 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20389 18162 603 41 0 20348 0
vsize: 81556
[startup+880.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19136 0 0 0 87963 47 0 0 25 0 1 0 484402897 83644416 18175 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20421 18175 603 41 0 20380 0
vsize: 81684
[startup+890.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19150 0 0 0 88963 47 0 0 25 0 1 0 484402897 83644416 18189 4294967295 134512640 134672761 3221224624 3221223760 134560625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20421 18189 603 41 0 20380 0
vsize: 81684
[startup+900.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19167 0 0 0 89963 48 0 0 25 0 1 0 484402897 83775488 18206 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20453 18206 603 41 0 20412 0
vsize: 81812
[startup+910.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19185 0 0 0 90963 48 0 0 25 0 1 0 484402897 83775488 18224 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20453 18224 603 41 0 20412 0
vsize: 81812
[startup+920.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19207 0 0 0 91963 48 0 0 25 0 1 0 484402897 83894272 18246 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20482 18246 603 41 0 20441 0
vsize: 81928
[startup+930.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19223 0 0 0 92964 48 0 0 25 0 1 0 484402897 84025344 18262 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20514 18262 603 41 0 20473 0
vsize: 82056
[startup+940.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19240 0 0 0 93964 48 0 0 25 0 1 0 484402897 84025344 18279 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20514 18279 603 41 0 20473 0
vsize: 82056
[startup+950.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19258 0 0 0 94964 48 0 0 25 0 1 0 484402897 84164608 18297 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20548 18297 603 41 0 20507 0
vsize: 82192
[startup+960.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19272 0 0 0 95964 48 0 0 25 0 1 0 484402897 84164608 18311 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20548 18311 603 41 0 20507 0
vsize: 82192
[startup+970.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19290 0 0 0 96964 48 0 0 25 0 1 0 484402897 84299776 18329 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20581 18329 603 41 0 20540 0
vsize: 82324
[startup+980.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19314 0 0 0 97964 48 0 0 25 0 1 0 484402897 84299776 18353 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20581 18353 603 41 0 20540 0
vsize: 82324
[startup+990.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19356 0 0 0 98964 48 0 0 25 0 1 0 484402897 84533248 18395 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20638 18395 603 41 0 20597 0
vsize: 82552
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19421 0 0 0 99964 48 0 0 25 0 1 0 484402897 84791296 18460 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20701 18460 603 41 0 20660 0
vsize: 82804
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19442 0 0 0 100965 48 0 0 25 0 1 0 484402897 84922368 18481 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20733 18481 603 41 0 20692 0
vsize: 82932
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19467 0 0 0 101965 48 0 0 25 0 1 0 484402897 84922368 18506 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20733 18506 603 41 0 20692 0
vsize: 82932
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19494 0 0 0 102965 48 0 0 25 0 1 0 484402897 85053440 18533 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20765 18533 603 41 0 20724 0
vsize: 83060
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19516 0 0 0 103965 48 0 0 25 0 1 0 484402897 85180416 18555 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20796 18555 603 41 0 20755 0
vsize: 83184
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19540 0 0 0 104965 49 0 0 25 0 1 0 484402897 85311488 18579 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20828 18579 603 41 0 20787 0
vsize: 83312
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19557 0 0 0 105965 49 0 0 25 0 1 0 484402897 85311488 18596 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20828 18596 603 41 0 20787 0
vsize: 83312
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19578 0 0 0 106965 49 0 0 25 0 1 0 484402897 85446656 18617 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20861 18617 603 41 0 20820 0
vsize: 83444
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19603 0 0 0 107965 49 0 0 25 0 1 0 484402897 85594112 18642 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20897 18642 603 41 0 20856 0
vsize: 83588
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19614 0 0 0 108966 49 0 0 25 0 1 0 484402897 85594112 18653 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20897 18653 603 41 0 20856 0
vsize: 83588
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19640 0 0 0 109966 49 0 0 25 0 1 0 484402897 85725184 18679 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20929 18679 603 41 0 20888 0
vsize: 83716
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19653 0 0 0 110966 49 0 0 25 0 1 0 484402897 85725184 18692 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20929 18692 603 41 0 20888 0
vsize: 83716
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19662 0 0 0 111966 49 0 0 25 0 1 0 484402897 85725184 18701 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20929 18701 603 41 0 20888 0
vsize: 83716
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19679 0 0 0 112966 49 0 0 25 0 1 0 484402897 85856256 18718 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20961 18718 603 41 0 20920 0
vsize: 83844
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19691 0 0 0 113966 49 0 0 25 0 1 0 484402897 85856256 18730 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20961 18730 603 41 0 20920 0
vsize: 83844
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19706 0 0 0 114967 49 0 0 25 0 1 0 484402897 85987328 18745 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20993 18745 603 41 0 20952 0
vsize: 83972
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19719 0 0 0 115967 49 0 0 25 0 1 0 484402897 85987328 18758 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20993 18758 603 41 0 20952 0
vsize: 83972
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19735 0 0 0 116967 49 0 0 25 0 1 0 484402897 86122496 18774 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21026 18774 603 41 0 20985 0
vsize: 84104
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19755 0 0 0 117967 49 0 0 25 0 1 0 484402897 86122496 18794 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21026 18794 603 41 0 20985 0
vsize: 84104
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19770 0 0 0 118967 49 0 0 25 0 1 0 484402897 86253568 18809 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21058 18809 603 41 0 21017 0
vsize: 84232
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29214
Raw data (stat): 29214 (minisat+) R 29213 29151 29150 0 -1 0 19776 0 0 0 119967 49 0 0 25 0 1 0 484402897 86253568 18815 4294967295 134512640 134672761 3221224624 3221223824 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21058 18815 603 41 0 21017 0
vsize: 84232
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 29214
Raw data (stat): 29214 (minisat+) Z 29213 29151 29150 0 -1 12 19779 0 0 0 119967 53 0 0 25 0 1 0 484402897 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.08
CPU time (s): 1200.21
CPU user time (s): 1199.68
CPU system time (s): 0.536918
CPU usage (%): 100.011
Max. virtual memory (Kb): 84232
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####