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/miplib3/normalized-mps-v2-13-7-egout.opb
MD5SUM	fd101f0ba1a3813e843a38997ab7ed84
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.04984
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 18290

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-21 14:13:49 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18296 boxname=wulflinc21 idbench=1408 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  fd101f0ba1a3813e843a38997ab7ed84  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-egout.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-egout.opb
IDLAUNCH: 18296
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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	: 3
cpu MHz		: 451.161
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:        868224 kB
Buffers:          2468 kB
Cached:         142236 kB
SwapCached:          0 kB
Active:          23456 kB
Inactive:       124220 kB
HighTotal:      131008 kB
HighFree:        82684 kB
LowTotal:       903652 kB
LowFree:        785540 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              48 kB
Writeback:           0 kB
Mapped:           6952 kB
Slab:            13144 kB
Committed_AS:    63796 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 14:33:51 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 18296 7 1200.22 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 
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.85 0.97 0.91 2/55 12555
Raw data (stat): 12555 (runsolver) R 12554 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 422977039 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.87 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 8199 0 0 0 977 22 0 0 25 0 1 0 422977039 37793792 7860 4294967295 134512640 134672761 3221224624 3221223840 134561950 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.0008 s]
Raw data (loadavg): 0.89 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 12529 0 0 0 1965 34 0 0 25 0 1 0 422977039 60899328 12190 4294967295 134512640 134672761 3221224624 3221221136 134522981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14868 12190 603 41 0 14827 0
vsize: 59472
[startup+30.0012 s]
Raw data (loadavg): 0.91 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 16803 0 0 0 2955 44 0 0 25 0 1 0 422977039 75501568 16134 4294967295 134512640 134672761 3221224624 3221223760 134560577 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.0009 s]
Raw data (loadavg): 0.92 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 16987 0 0 0 3955 45 0 0 25 0 1 0 422977039 75837440 16318 4294967295 134512640 134672761 3221224624 3221223760 134560588 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.0005 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17039 0 0 0 4954 45 0 0 25 0 1 0 422977039 75890688 16350 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18528 16350 603 41 0 18487 0
vsize: 74112
[startup+60.0012 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17039 0 0 0 5954 45 0 0 25 0 1 0 422977039 75890688 16350 4294967295 134512640 134672761 3221224624 3221223792 134561229 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.0019 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17062 0 0 0 6954 45 0 0 25 0 1 0 422977039 76025856 16373 4294967295 134512640 134672761 3221224624 3221223824 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18561 16373 603 41 0 18520 0
vsize: 74244
[startup+80.003 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17101 0 0 0 7954 45 0 0 25 0 1 0 422977039 76161024 16412 4294967295 134512640 134672761 3221224624 3221223788 134559748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18594 16412 603 41 0 18553 0
vsize: 74376
[startup+90.0033 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17173 0 0 0 8954 46 0 0 25 0 1 0 422977039 76431360 16483 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18660 16483 603 41 0 18619 0
vsize: 74640
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17191 0 0 0 9954 46 0 0 25 0 1 0 422977039 76431360 16484 4294967295 134512640 134672761 3221224624 3221223792 134560830 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.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17225 0 0 0 10954 46 0 0 25 0 1 0 422977039 76484608 16498 4294967295 134512640 134672761 3221224624 3221223824 134557852 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.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17225 0 0 0 11954 46 0 0 25 0 1 0 422977039 76484608 16498 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18673 16498 603 41 0 18632 0
vsize: 74692
[startup+130.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17368 0 0 0 12954 46 0 0 25 0 1 0 422977039 77279232 16641 4294967295 134512640 134672761 3221224624 3221223792 134560830 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.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17377 0 0 0 13954 46 0 0 25 0 1 0 422977039 77279232 16650 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 16650 603 41 0 18826 0
vsize: 75468
[startup+150.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17412 0 0 0 14954 46 0 0 25 0 1 0 422977039 77414400 16685 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18900 16685 603 41 0 18859 0
vsize: 75600
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17428 0 0 0 15954 46 0 0 25 0 1 0 422977039 77414400 16701 4294967295 134512640 134672761 3221224624 3221223824 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18900 16701 603 41 0 18859 0
vsize: 75600
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17437 0 0 0 16954 46 0 0 25 0 1 0 422977039 77414400 16710 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18900 16710 603 41 0 18859 0
vsize: 75600
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17445 0 0 0 17954 46 0 0 25 0 1 0 422977039 77545472 16718 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18932 16718 603 41 0 18891 0
vsize: 75728
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17454 0 0 0 18955 46 0 0 25 0 1 0 422977039 77545472 16727 4294967295 134512640 134672761 3221224624 3221223760 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18932 16727 603 41 0 18891 0
vsize: 75728
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17557 0 0 0 19954 47 0 0 25 0 1 0 422977039 77991936 16830 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19041 16830 603 41 0 19000 0
vsize: 76164
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17557 0 0 0 20955 47 0 0 25 0 1 0 422977039 77991936 16830 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19041 16830 603 41 0 19000 0
vsize: 76164
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17557 0 0 0 21955 47 0 0 25 0 1 0 422977039 77991936 16830 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19041 16830 603 41 0 19000 0
vsize: 76164
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17558 0 0 0 22955 47 0 0 25 0 1 0 422977039 77991936 16831 4294967295 134512640 134672761 3221224624 3221223748 134566054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19041 16831 603 41 0 19000 0
vsize: 76164
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17595 0 0 0 23955 47 0 0 25 0 1 0 422977039 78032896 16851 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19051 16851 603 41 0 19010 0
vsize: 76204
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17595 0 0 0 24955 47 0 0 25 0 1 0 422977039 78032896 16851 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19051 16851 603 41 0 19010 0
vsize: 76204
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17613 0 0 0 25955 47 0 0 25 0 1 0 422977039 78168064 16869 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19084 16869 603 41 0 19043 0
vsize: 76336
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17719 0 0 0 26955 47 0 0 25 0 1 0 422977039 78479360 16961 4294967295 134512640 134672761 3221224624 3221223748 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19160 16961 603 41 0 19119 0
vsize: 76640
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17755 0 0 0 27955 47 0 0 25 0 1 0 422977039 78548992 16979 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19177 16979 603 41 0 19136 0
vsize: 76708
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17779 0 0 0 28955 47 0 0 25 0 1 0 422977039 78667776 17003 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19206 17003 603 41 0 19165 0
vsize: 76824
[startup+300.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17800 0 0 0 29955 47 0 0 25 0 1 0 422977039 78798848 17024 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19238 17024 603 41 0 19197 0
vsize: 76952
[startup+310.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17875 0 0 0 30955 48 0 0 25 0 1 0 422977039 79138816 17099 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19321 17099 603 41 0 19280 0
vsize: 77284
[startup+320.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17928 0 0 0 31955 48 0 0 25 0 1 0 422977039 79409152 17152 4294967295 134512640 134672761 3221224624 3221223760 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19387 17152 603 41 0 19346 0
vsize: 77548
[startup+330.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17936 0 0 0 32955 48 0 0 25 0 1 0 422977039 79409152 17160 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19387 17160 603 41 0 19346 0
vsize: 77548
[startup+340.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17991 0 0 0 33955 48 0 0 25 0 1 0 422977039 79478784 17194 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19404 17194 603 41 0 19363 0
vsize: 77616
[startup+350.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 17991 0 0 0 34955 49 0 0 25 0 1 0 422977039 79478784 17194 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19404 17194 603 41 0 19363 0
vsize: 77616
[startup+360 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18001 0 0 0 35955 49 0 0 25 0 1 0 422977039 79613952 17204 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19437 17204 603 41 0 19396 0
vsize: 77748
[startup+370 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18018 0 0 0 36955 49 0 0 25 0 1 0 422977039 79613952 17221 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19437 17221 603 41 0 19396 0
vsize: 77748
[startup+380.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18031 0 0 0 37956 49 0 0 25 0 1 0 422977039 79749120 17234 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19470 17234 603 41 0 19429 0
vsize: 77880
[startup+390.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18066 0 0 0 38956 49 0 0 25 0 1 0 422977039 79867904 17269 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19499 17269 603 41 0 19458 0
vsize: 77996
[startup+400 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18137 0 0 0 39956 49 0 0 25 0 1 0 422977039 79986688 17320 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19528 17320 603 41 0 19487 0
vsize: 78112
[startup+410 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18178 0 0 0 40956 49 0 0 25 0 1 0 422977039 80068608 17340 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19548 17340 603 41 0 19507 0
vsize: 78192
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18178 0 0 0 41955 49 0 0 25 0 1 0 422977039 80068608 17340 4294967295 134512640 134672761 3221224624 3221223824 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19548 17340 603 41 0 19507 0
vsize: 78192
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18192 0 0 0 42955 49 0 0 25 0 1 0 422977039 80195584 17354 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19579 17354 603 41 0 19538 0
vsize: 78316
[startup+440.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18216 0 0 0 43955 49 0 0 25 0 1 0 422977039 80326656 17378 4294967295 134512640 134672761 3221224624 3221223824 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19611 17378 603 41 0 19570 0
vsize: 78444
[startup+450.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18233 0 0 0 44955 49 0 0 25 0 1 0 422977039 80326656 17395 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19611 17395 603 41 0 19570 0
vsize: 78444
[startup+460.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18242 0 0 0 45955 49 0 0 25 0 1 0 422977039 80326656 17404 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19611 17404 603 41 0 19570 0
vsize: 78444
[startup+470.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18260 0 0 0 46955 49 0 0 25 0 1 0 422977039 80457728 17422 4294967295 134512640 134672761 3221224624 3221223760 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19643 17422 603 41 0 19602 0
vsize: 78572
[startup+480.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18311 0 0 0 47955 49 0 0 25 0 1 0 422977039 80715776 17473 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19706 17473 603 41 0 19665 0
vsize: 78824
[startup+490.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18416 0 0 0 48955 50 0 0 25 0 1 0 422977039 80797696 17520 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19726 17520 603 41 0 19685 0
vsize: 78904
[startup+500.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18416 0 0 0 49955 50 0 0 25 0 1 0 422977039 80797696 17520 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19726 17520 603 41 0 19685 0
vsize: 78904
[startup+510.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18438 0 0 0 50955 50 0 0 25 0 1 0 422977039 80932864 17542 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19759 17542 603 41 0 19718 0
vsize: 79036
[startup+520.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18451 0 0 0 51955 50 0 0 25 0 1 0 422977039 81063936 17555 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19791 17555 603 41 0 19750 0
vsize: 79164
[startup+530.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18468 0 0 0 52956 50 0 0 25 0 1 0 422977039 81063936 17572 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19791 17572 603 41 0 19750 0
vsize: 79164
[startup+540.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18488 0 0 0 53955 50 0 0 25 0 1 0 422977039 81199104 17592 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19824 17592 603 41 0 19783 0
vsize: 79296
[startup+550.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18514 0 0 0 54956 50 0 0 25 0 1 0 422977039 81199104 17618 4294967295 134512640 134672761 3221224624 3221223824 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19824 17618 603 41 0 19783 0
vsize: 79296
[startup+560.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18533 0 0 0 55955 50 0 0 25 0 1 0 422977039 81326080 17637 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19855 17637 603 41 0 19814 0
vsize: 79420
[startup+570.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18597 0 0 0 56955 51 0 0 25 0 1 0 422977039 81436672 17681 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19882 17681 603 41 0 19841 0
vsize: 79528
[startup+580.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18597 0 0 0 57955 51 0 0 25 0 1 0 422977039 81436672 17681 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19882 17681 603 41 0 19841 0
vsize: 79528
[startup+590.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18614 0 0 0 58955 51 0 0 25 0 1 0 422977039 81555456 17698 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19911 17698 603 41 0 19870 0
vsize: 79644
[startup+600.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18629 0 0 0 59956 51 0 0 25 0 1 0 422977039 81686528 17713 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19943 17713 603 41 0 19902 0
vsize: 79772
[startup+610.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18692 0 0 0 60955 51 0 0 25 0 1 0 422977039 81735680 17755 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19955 17755 603 41 0 19914 0
vsize: 79820
[startup+620.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18692 0 0 0 61956 51 0 0 25 0 1 0 422977039 81735680 17755 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19955 17755 603 41 0 19914 0
vsize: 79820
[startup+630.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18692 0 0 0 62956 51 0 0 25 0 1 0 422977039 81735680 17755 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19955 17755 603 41 0 19914 0
vsize: 79820
[startup+640.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18699 0 0 0 63956 51 0 0 25 0 1 0 422977039 81858560 17762 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19985 17762 603 41 0 19944 0
vsize: 79940
[startup+650 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18719 0 0 0 64956 51 0 0 25 0 1 0 422977039 81858560 17782 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19985 17782 603 41 0 19944 0
vsize: 79940
[startup+660.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18732 0 0 0 65956 52 0 0 25 0 1 0 422977039 81989632 17795 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20017 17795 603 41 0 19976 0
vsize: 80068
[startup+670.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18772 0 0 0 66956 52 0 0 25 0 1 0 422977039 82112512 17835 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20047 17835 603 41 0 20006 0
vsize: 80188
[startup+680.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18794 0 0 0 67956 52 0 0 25 0 1 0 422977039 82231296 17857 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20076 17857 603 41 0 20035 0
vsize: 80304
[startup+690.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18797 0 0 0 68956 52 0 0 25 0 1 0 422977039 82231296 17860 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20076 17860 603 41 0 20035 0
vsize: 80304
[startup+700.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18801 0 0 0 69957 52 0 0 25 0 1 0 422977039 82231296 17864 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20076 17864 603 41 0 20035 0
vsize: 80304
[startup+710 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18808 0 0 0 70957 52 0 0 25 0 1 0 422977039 82231296 17871 4294967295 134512640 134672761 3221224624 3221223760 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20076 17871 603 41 0 20035 0
vsize: 80304
[startup+720 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18829 0 0 0 71957 52 0 0 25 0 1 0 422977039 82362368 17892 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20108 17892 603 41 0 20067 0
vsize: 80432
[startup+730 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18882 0 0 0 72957 52 0 0 25 0 1 0 422977039 82427904 17925 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20124 17925 603 41 0 20083 0
vsize: 80496
[startup+740 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18885 0 0 0 73957 52 0 0 25 0 1 0 422977039 82554880 17928 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20155 17928 603 41 0 20114 0
vsize: 80620
[startup+749.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18894 0 0 0 74957 52 0 0 25 0 1 0 422977039 82554880 17937 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20155 17937 603 41 0 20114 0
vsize: 80620
[startup+760 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18907 0 0 0 75957 52 0 0 25 0 1 0 422977039 82554880 17950 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20155 17950 603 41 0 20114 0
vsize: 80620
[startup+770 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18927 0 0 0 76957 52 0 0 25 0 1 0 422977039 82690048 17970 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 17970 603 41 0 20147 0
vsize: 80752
[startup+779.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18940 0 0 0 77957 52 0 0 25 0 1 0 422977039 82690048 17983 4294967295 134512640 134672761 3221224624 3221223792 134560849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 17983 603 41 0 20147 0
vsize: 80752
[startup+790 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18957 0 0 0 78957 52 0 0 25 0 1 0 422977039 82821120 18000 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20220 18000 603 41 0 20179 0
vsize: 80880
[startup+800 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18978 0 0 0 79958 52 0 0 25 0 1 0 422977039 82821120 18021 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20220 18021 603 41 0 20179 0
vsize: 80880
[startup+810 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 18996 0 0 0 80958 52 0 0 25 0 1 0 422977039 82960384 18039 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20254 18039 603 41 0 20213 0
vsize: 81016
[startup+820 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19010 0 0 0 81958 52 0 0 25 0 1 0 422977039 82960384 18053 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20254 18053 603 41 0 20213 0
vsize: 81016
[startup+830.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19022 0 0 0 82958 52 0 0 25 0 1 0 422977039 83091456 18065 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20286 18065 603 41 0 20245 0
vsize: 81144
[startup+840 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19034 0 0 0 83958 53 0 0 25 0 1 0 422977039 83091456 18077 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20286 18077 603 41 0 20245 0
vsize: 81144
[startup+850 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19049 0 0 0 84958 53 0 0 25 0 1 0 422977039 83218432 18092 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20317 18092 603 41 0 20276 0
vsize: 81268
[startup+860.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19091 0 0 0 85958 53 0 0 25 0 1 0 422977039 83480576 18134 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20381 18134 603 41 0 20340 0
vsize: 81524
[startup+870.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19123 0 0 0 86958 53 0 0 25 0 1 0 422977039 83513344 18162 4294967295 134512640 134672761 3221224624 3221223760 134560606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20389 18162 603 41 0 20348 0
vsize: 81556
[startup+880.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19123 0 0 0 87959 53 0 0 25 0 1 0 422977039 83513344 18162 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20389 18162 603 41 0 20348 0
vsize: 81556
[startup+890.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19125 0 0 0 88959 53 0 0 25 0 1 0 422977039 83644416 18164 4294967295 134512640 134672761 3221224624 3221223824 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20421 18164 603 41 0 20380 0
vsize: 81684
[startup+900.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19145 0 0 0 89959 53 0 0 25 0 1 0 422977039 83644416 18184 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20421 18184 603 41 0 20380 0
vsize: 81684
[startup+910.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19159 0 0 0 90959 53 0 0 25 0 1 0 422977039 83775488 18198 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20453 18198 603 41 0 20412 0
vsize: 81812
[startup+920.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19177 0 0 0 91959 53 0 0 25 0 1 0 422977039 83775488 18216 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20453 18216 603 41 0 20412 0
vsize: 81812
[startup+930.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19204 0 0 0 92959 53 0 0 25 0 1 0 422977039 83894272 18243 4294967295 134512640 134672761 3221224624 3221223792 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20482 18243 603 41 0 20441 0
vsize: 81928
[startup+940.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19216 0 0 0 93959 53 0 0 25 0 1 0 422977039 83894272 18255 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20482 18255 603 41 0 20441 0
vsize: 81928
[startup+950.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19228 0 0 0 94959 53 0 0 25 0 1 0 422977039 84025344 18267 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20514 18267 603 41 0 20473 0
vsize: 82056
[startup+960.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19245 0 0 0 95959 54 0 0 25 0 1 0 422977039 84025344 18284 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20514 18284 603 41 0 20473 0
vsize: 82056
[startup+970.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19264 0 0 0 96959 54 0 0 25 0 1 0 422977039 84164608 18303 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20548 18303 603 41 0 20507 0
vsize: 82192
[startup+980.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19279 0 0 0 97960 54 0 0 25 0 1 0 422977039 84164608 18318 4294967295 134512640 134672761 3221224624 3221223780 134565154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20548 18318 603 41 0 20507 0
vsize: 82192
[startup+990.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19295 0 0 0 98960 54 0 0 25 0 1 0 422977039 84299776 18334 4294967295 134512640 134672761 3221224624 3221223824 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20581 18334 603 41 0 20540 0
vsize: 82324
[startup+1000 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19323 0 0 0 99960 54 0 0 25 0 1 0 422977039 84430848 18362 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20613 18362 603 41 0 20572 0
vsize: 82452
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19391 0 0 0 100960 54 0 0 25 0 1 0 422977039 84668416 18430 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20671 18430 603 41 0 20630 0
vsize: 82684
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19429 0 0 0 101960 54 0 0 25 0 1 0 422977039 84791296 18468 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20701 18468 603 41 0 20660 0
vsize: 82804
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19449 0 0 0 102960 54 0 0 25 0 1 0 422977039 84922368 18488 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20733 18488 603 41 0 20692 0
vsize: 82932
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19477 0 0 0 103960 54 0 0 25 0 1 0 422977039 85053440 18516 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20765 18516 603 41 0 20724 0
vsize: 83060
[startup+1050 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19498 0 0 0 104960 55 0 0 25 0 1 0 422977039 85053440 18537 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20765 18537 603 41 0 20724 0
vsize: 83060
[startup+1060 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19527 0 0 0 105960 55 0 0 25 0 1 0 422977039 85180416 18566 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20796 18566 603 41 0 20755 0
vsize: 83184
[startup+1070 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19545 0 0 0 106960 55 0 0 25 0 1 0 422977039 85311488 18584 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20828 18584 603 41 0 20787 0
vsize: 83312
[startup+1080 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19564 0 0 0 107960 55 0 0 25 0 1 0 422977039 85446656 18603 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20861 18603 603 41 0 20820 0
vsize: 83444
[startup+1090 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19578 0 0 0 108960 55 0 0 25 0 1 0 422977039 85446656 18617 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20861 18617 603 41 0 20820 0
vsize: 83444
[startup+1100 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19603 0 0 0 109960 55 0 0 25 0 1 0 422977039 85594112 18642 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20897 18642 603 41 0 20856 0
vsize: 83588
[startup+1110 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19620 0 0 0 110960 56 0 0 25 0 1 0 422977039 85594112 18659 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20897 18659 603 41 0 20856 0
vsize: 83588
[startup+1120 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19640 0 0 0 111960 56 0 0 25 0 1 0 422977039 85725184 18679 4294967295 134512640 134672761 3221224624 3221223768 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20929 18679 603 41 0 20888 0
vsize: 83716
[startup+1130 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19656 0 0 0 112960 56 0 0 25 0 1 0 422977039 85725184 18695 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20929 18695 603 41 0 20888 0
vsize: 83716
[startup+1140 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19664 0 0 0 113961 56 0 0 25 0 1 0 422977039 85725184 18703 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20929 18703 603 41 0 20888 0
vsize: 83716
[startup+1150 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19681 0 0 0 114961 56 0 0 25 0 1 0 422977039 85856256 18720 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20961 18720 603 41 0 20920 0
vsize: 83844
[startup+1160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19694 0 0 0 115961 56 0 0 25 0 1 0 422977039 85856256 18733 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20961 18733 603 41 0 20920 0
vsize: 83844
[startup+1170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19706 0 0 0 116961 56 0 0 25 0 1 0 422977039 85987328 18745 4294967295 134512640 134672761 3221224624 3221223824 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20993 18745 603 41 0 20952 0
vsize: 83972
[startup+1180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19720 0 0 0 117961 56 0 0 25 0 1 0 422977039 85987328 18759 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20993 18759 603 41 0 20952 0
vsize: 83972
[startup+1190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19736 0 0 0 118961 56 0 0 25 0 1 0 422977039 86122496 18775 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21026 18775 603 41 0 20985 0
vsize: 84104
[startup+1200 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12555
Raw data (stat): 12555 (minisat+) R 12554 30927 30926 0 -1 0 19755 0 0 0 119961 56 0 0 25 0 1 0 422977039 86122496 18794 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21026 18794 603 41 0 20985 0
vsize: 84104
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 12555
Raw data (stat): 12555 (minisat+) Z 12554 30927 30926 0 -1 12 19758 0 0 0 119961 60 0 0 25 0 1 0 422977039 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.05
CPU time (s): 1200.22
CPU user time (s): 1199.62
CPU system time (s): 0.604908
CPU usage (%): 100.015
Max. virtual memory (Kb): 84104
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####