PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-egout.opb
MD5SUM	46c4db5f8baf54496e00a723c85beb20
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	58880896
Optimality of the best value was proved	NO
Number of terms in the objective function	1095
Biggest coefficient in the objective function	533200896
Number of bits for the biggest coefficient in the objective function	29
Sum of the numbers in the objective function	14929722305
Number of bits of the sum of numbers in the objective function	34
Biggest number in a constraint	533200896
Number of bits of the biggest number in a constraint	29
Biggest sum of numbers in a constraint	14929722305
Number of bits of the biggest sum of numbers	34
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04084
Number of variables	1155
Total number of constraints	153
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	55
Number of constraints which are nor clauses,nor cardinality constraints	98
Minimum length of a constraint	1
Maximum length of a constraint	280
Trace number 19254

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        574076 kB
Buffers:         32964 kB
Cached:         405876 kB
SwapCached:        440 kB
Active:          76880 kB
Inactive:       364096 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        573796 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5360 kB
Slab:            13880 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:48:41 (client local time) WITH STATUS 30 IN 990.662 SECONDS
stats: 16796 0 990.662 30
#### 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 |   11424    31612 |    3808       0        0     nan |  0.000 % |
c |       100 |   10955    30439 |    4188      42      115     2.7 | 24.647 % |
c |       251 |   10683    29792 |    4607     148      703     4.8 | 26.358 % |
c ==============================================================================
c [1mFound solution: 99705670[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:94010     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 |       351 |  281395   663365 |   93798     240     1337     5.6 | 26.358 % |
c |       451 |  281325   663189 |  103177     328     1760     5.4 |  1.168 % |
c ==============================================================================
c [1mFound solution: 88519139[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:61824     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 |       548 |  456818  1074371 |  152272     417     2285     5.5 |  1.168 % |
c |       648 |  450327  1059573 |  167499     504     2749     5.5 |  2.681 % |
c |       800 |  448072  1054409 |  184249     652     4524     6.9 |  2.681 % |
c |      1028 |  447966  1054163 |  202674     878     8317     9.5 |  2.704 % |
c |      1365 |  447789  1053758 |  222941    1211     9891     8.2 |  2.737 % |
c |      1871 |  444041  1045170 |  245235    1682    13981     8.3 |  3.442 % |
c |      2632 |  442149  1040825 |  269759    2434    46378    19.1 |  3.802 % |
c |      3771 |  440969  1038112 |  296735    3554    73736    20.7 |  4.029 % |
c |      5479 |  439251  1034131 |  326408    5201   123384    23.7 |  4.357 % |
c |      8044 |  437988  1031220 |  359049    7757   299347    38.6 |  4.598 % |
c |     11889 |  436907  1028750 |  394954   11563   453299    39.2 |  4.799 % |
c ==============================================================================
c [1mFound solution: 87395261[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:53407     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 |     13712 |  586480  1378939 |  195493   13350   491195    36.8 |  4.799 % |
c |     13812 |  586480  1378939 |  215042   13450   499220    37.1 |  3.982 % |
c ==============================================================================
c [1mFound solution: 79748872[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 |     13848 |  588322  1383771 |  196107   13486   499978    37.1 |  3.982 % |
c ==============================================================================
c [1mFound solution: 77592704[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 |     13873 |  589447  1386585 |  196482   13511   500335    37.0 |  3.982 % |
c |     13973 |  589392  1386462 |  216130   13610   510991    37.5 |  3.981 % |
c ==============================================================================
c [1mFound solution: 70179712[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 |     14069 |  590222  1388534 |  196740   13706   511836    37.3 |  3.981 % |
c ==============================================================================
c [1mFound solution: 70053120[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 |     14151 |  590243  1388648 |  196747   13786   516956    37.5 |  3.981 % |
c |     14251 |  590212  1388578 |  216421   13885   517837    37.3 |  3.999 % |
c ==============================================================================
c [1mFound solution: 69924480[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     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 |     14343 |  590074  1388274 |  196691   13975   519642    37.2 |  3.999 % |
c |     14443 |  590074  1388274 |  216360   14075   524158    37.2 |  4.022 % |
c |     14594 |  589980  1388064 |  237996   14224   525869    37.0 |  4.034 % |
c |     14819 |  589980  1388064 |  261795   14449   535102    37.0 |  4.034 % |
c ==============================================================================
c [1mFound solution: 69533760[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 |     15120 |  590018  1388158 |  196672   14750   541855    36.7 |  4.034 % |
c |     15220 |  590018  1388158 |  216339   14850   562934    37.9 |  4.034 % |
c |     15372 |  589639  1387309 |  237973   15001   564292    37.6 |  4.081 % |
c |     15598 |  589237  1386386 |  261770   15225   567756    37.3 |  4.139 % |
c |     15935 |  588586  1384912 |  287947   15556   572383    36.8 |  4.227 % |
c |     16443 |  588372  1384432 |  316742   16057   590268    36.8 |  4.256 % |
c ==============================================================================
c [1mFound solution: 69330304[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 |     16828 |  588360  1384413 |  196120   16440   611792    37.2 |  4.256 % |
c |     16931 |  588360  1384413 |  215732   16543   614350    37.1 |  4.261 % |
c |     17081 |  588356  1384404 |  237305   16692   617358    37.0 |  4.261 % |
c |     17306 |  588356  1384404 |  261035   16917   648178    38.3 |  4.261 % |
c |     17643 |  587597  1382684 |  287139   17224   657249    38.2 |  4.368 % |
c |     18151 |  587597  1382684 |  315853   17732   677469    38.2 |  4.368 % |
c |     18911 |  587568  1382618 |  347438   18491   718910    38.9 |  4.371 % |
c ==============================================================================
c [1mFound solution: 67674965[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 |     19039 |  587627  1382761 |  195875   18619   725845    39.0 |  4.371 % |
c |     19139 |  587582  1382663 |  215462   18714   726789    38.8 |  4.377 % |
c |     19290 |  587565  1382623 |  237008   18862   728050    38.6 |  4.380 % |
c |     19515 |  587462  1382395 |  260709   19072   730500    38.3 |  4.396 % |
c |     19852 |  587462  1382395 |  286780   19409   752950    38.8 |  4.396 % |
c |     20359 |  587301  1382035 |  315458   19787   769101    38.9 |  4.418 % |
c |     21118 |  587301  1382035 |  347004   20546   847145    41.2 |  4.418 % |
c ==============================================================================
c [1mFound solution: 65811776[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 |     21891 |  587369  1382201 |  195789   21319   934427    43.8 |  4.418 % |
c |     21992 |  587369  1382201 |  215367   21420   937241    43.8 |  4.418 % |
c ==============================================================================
c [1mFound solution: 65811770[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     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 |     22125 |  587416  1382316 |  195805   21553   948273    44.0 |  4.418 % |
c |     22225 |  587405  1382291 |  215385   21651   951751    44.0 |  4.420 % |
c |     22376 |  587405  1382291 |  236924   21802   970246    44.5 |  4.420 % |
c |     22601 |  587405  1382291 |  260616   22027   984111    44.7 |  4.420 % |
c |     22938 |  587405  1382291 |  286678   22364  1003785    44.9 |  4.420 % |
c |     23444 |  587405  1382291 |  315345   22870  1036452    45.3 |  4.420 % |
c ==============================================================================
c [1mFound solution: 65009650[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     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 |     24143 |  587440  1382378 |  195813   23569  1086745    46.1 |  4.420 % |
c |     24243 |  587440  1382378 |  215394   23669  1088930    46.0 |  4.420 % |
c |     24393 |  587440  1382378 |  236933   23819  1093088    45.9 |  4.420 % |
c |     24619 |  587440  1382378 |  260627   24045  1105510    46.0 |  4.420 % |
c ==============================================================================
c [1mFound solution: 63996032[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     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 |     24860 |  587465  1382441 |  195821   24286  1153329    47.5 |  4.420 % |
c |     24961 |  587423  1382345 |  215403   24380  1153856    47.3 |  4.426 % |
c |     25112 |  586970  1381309 |  236943   24479  1159390    47.4 |  4.491 % |
c |     25337 |  586970  1381309 |  260637   24704  1166529    47.2 |  4.491 % |
c |     25675 |  586941  1381242 |  286701   25031  1172412    46.8 |  4.495 % |
c ==============================================================================
c [1mFound solution: 63559808[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     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 |     25768 |  586728  1380762 |  195576   24582  1160590    47.2 |  4.495 % |
c |     25868 |  586728  1380762 |  215133   24682  1164049    47.2 |  4.529 % |
c |     26019 |  586728  1380762 |  236646   24833  1167541    47.0 |  4.529 % |
c |     26245 |  586308  1379803 |  260311   24968  1181924    47.3 |  4.591 % |
c |     26583 |  586308  1379803 |  286342   25306  1200880    47.5 |  4.591 % |
c ==============================================================================
c [1mFound solution: 63443456[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 |     27064 |  586329  1379858 |  195443   25787  1233664    47.8 |  4.591 % |
c |     27164 |  586329  1379858 |  214987   25887  1237374    47.8 |  4.592 % |
c |     27314 |  586329  1379858 |  236486   26037  1244956    47.8 |  4.592 % |
c |     27539 |  586329  1379858 |  260134   26262  1256863    47.9 |  4.592 % |
c |     27879 |  586329  1379858 |  286148   26602  1272088    47.8 |  4.592 % |
c |     28385 |  586329  1379858 |  314762   27108  1296934    47.8 |  4.592 % |
c |     29144 |  586205  1379572 |  346239   27865  1324080    47.5 |  4.610 % |
c ==============================================================================
c [1mFound solution: 62720896[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     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 |     29880 |  586147  1379442 |  195382   28600  1367475    47.8 |  4.610 % |
c ==============================================================================
c [1mFound solution: 62381184[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     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 |     29887 |  586193  1379558 |  195397   28607  1368242    47.8 |  4.610 % |
c ==============================================================================
c [1mFound solution: 61939584[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 |     29899 |  586223  1379634 |  195407   28619  1368928    47.8 |  4.610 % |
c ==============================================================================
c [1mFound solution: 60293760[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     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 |     29963 |  586255  1379714 |  195418   28683  1370935    47.8 |  4.610 % |
c |     30063 |  586255  1379714 |  214959   28783  1374345    47.7 |  4.624 % |
c ==============================================================================
c [1mFound solution: 59932672[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 |     30131 |  586289  1379796 |  195429   28851  1378516    47.8 |  4.624 % |
c |     30231 |  586289  1379796 |  214971   28951  1379960    47.7 |  4.624 % |
c |     30381 |  586289  1379796 |  236469   29101  1384666    47.6 |  4.624 % |
c |     30606 |  586289  1379796 |  260115   29326  1393564    47.5 |  4.624 % |
c |     30943 |  586135  1379440 |  286127   29660  1406599    47.4 |  4.648 % |
c |     31449 |  586135  1379440 |  314740   30166  1426068    47.3 |  4.648 % |
c |     32209 |  586135  1379440 |  346214   30926  1452936    47.0 |  4.648 % |
c |     33349 |  586135  1379440 |  380835   32066  1496264    46.7 |  4.648 % |
c |     35057 |  586135  1379440 |  418919   33774  1576268    46.7 |  4.648 % |
c ==============================================================================
c [1mFound solution: 59075456[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 |     35864 |  586158  1379497 |  195386   34581  1616036    46.7 |  4.648 % |
c |     35965 |  586158  1379497 |  214924   34682  1620167    46.7 |  4.648 % |
c |     36115 |  586158  1379497 |  236417   34832  1623408    46.6 |  4.648 % |
c |     36340 |  586158  1379497 |  260058   35057  1638073    46.7 |  4.648 % |
c |     36677 |  586158  1379497 |  286064   35394  1647503    46.5 |  4.648 % |
c |     37185 |  586158  1379497 |  314671   35902  1670361    46.5 |  4.648 % |
c |     37945 |  586145  1379469 |  346138   36660  1699646    46.4 |  4.650 % |
c |     39084 |  586145  1379469 |  380752   37799  1735523    45.9 |  4.650 % |
c |     40795 |  586119  1379410 |  418827   39507  1809021    45.8 |  4.653 % |
c ==============================================================================
c [1mFound solution: 58880896[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:71599     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 |     42500 |  735946  1732020 |  245315   26062   720219    27.6 |  4.653 % |
c |     42600 |  735946  1732020 |  269846   26162   724236    27.7 |  9.663 % |
c |     42752 |  735946  1732020 |  296831   26314   733477    27.9 |  9.663 % |
c |     42977 |  735946  1732020 |  326514   26539   736938    27.8 |  9.663 % |
c ==============================================================================
c [1mOptimal solution: 58880896[0m
s OPTIMUM FOUND
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__bit_7 -F_0x2e_041_0x2e__0x2e__0x2e__bit_6 -F_0x2e_041_0x2e__0x2e__0x2e__bit_5 -F_0x2e_041_0x2e__0x2e__0x2e__bit_4 -F_0x2e_041_0x2e__0x2e__0x2e__bit_3 -F_0x2e_041_0x2e__0x2e__0x2e__bit_2 -F_0x2e_041_0x2e__0x2e__0x2e__bit_1 -F_0x2e_041_0x2e__0x2e__0x2e__bit0 -F_0x2e_041_0x2e__0x2e__0x2e__bit1 -F_0x2e_041_0x2e__0x2e__0x2e__bit2 -F_0x2e_041_0x2e__0x2e__0x2e__bit3 -F_0x2e_041_0x2e__0x2e__0x2e__bit4 -F_0x2e_041_0x2e__0x2e__0x2e__bit5 -F_0x2e_041_0x2e__0x2e__0x2e__bit6 -F_0x2e_041_0x2e__0x2e__0x2e__bit7 -F_0x2e_041_0x2e__0x2e__0x2e__bit8 -F_0x2e_041_0x2e__0x2e__0x2e__bit9 -F_0x2e_041_0x2e__0x2e__0x2e__bit10 -F_0x2e_041_0x2e__0x2e__0x2e__bit11 -F_0x2e_041_0x2e__0x2e__0x2e__bit12 -F_0x2e_040041_bit_7 -F_0x2e_040041_bit_6 -F_0x2e_040041_bit_5 -F_0x2e_040041_bit_4 -F_0x2e_040041_bit_3 -F_0x2e_040041_bit_2 -F_0x2e_040041_bit_1 -F_0x2e_040041_bit0 F_0x2e_040041_bit1 F_0x2e_040041_bit2 F_0x2e_040041_bit3 -F_0x2e_040041_bit4 F_0x2e_040041_bit5 -F_0x2e_040041_bit6 -F_0x2e_040041_bit7 -F_0x2e_040041_bit8 -F_0x2e_040041_bit9 -F_0x2e_040041_bit10 -F_0x2e_040041_bit11 -F_0x2e_040041_bit12 -F_0x2e_041042_bit_7 -F_0x2e_041042_bit_6 -F_0x2e_041042_bit_5 -F_0x2e_041042_bit_4 -F_0x2e_041042_bit_3 -F_0x2e_041042_bit_2 -F_0x2e_041042_bit_1 F_0x2e_041042_bit0 F_0x2e_041042_bit1 -F_0x2e_041042_bit2 -F_0x2e_041042_bit3 F_0x2e_041042_bit4 F_0x2e_041042_bit5 -F_0x2e_041042_bit6 -F_0x2e_041042_bit7 -F_0x2e_041042_bit8 -F_0x2e_041042_bit9 -F_0x2e_041042_bit10 -F_0x2e_041042_bit11 -F_0x2e_041042_bit12 -F_0x2e_042_0x2e__0x2e__0x2e__bit_7 -F_0x2e_042_0x2e__0x2e__0x2e__bit_6 -F_0x2e_042_0x2e__0x2e__0x2e__bit_5 -F_0x2e_042_0x2e__0x2e__0x2e__bit_4 -F_0x2e_042_0x2e__0x2e__0x2e__bit_3 -F_0x2e_042_0x2e__0x2e__0x2e__bit_2 -F_0x2e_042_0x2e__0x2e__0x2e__bit_1 F_0x2e_042_0x2e__0x2e__0x2e__bit0 -F_0x2e_042_0x2e__0x2e__0x2e__bit1 -F_0x2e_042_0x2e__0x2e__0x2e__bit2 F_0x2e_042_0x2e__0x2e__0x2e__bit3 F_0x2e_042_0x2e__0x2e__0x2e__bit4 F_0x2e_042_0x2e__0x2e__0x2e__bit5 -F_0x2e_042_0x2e__0x2e__0x2e__bit6 -F_0x2e_042_0x2e__0x2e__0x2e__bit7 -F_0x2e_042_0x2e__0x2e__0x2e__bit8 -F_0x2e_042_0x2e__0x2e__0x2e__bit9 -F_0x2e_042_0x2e__0x2e__0x2e__bit10 -F_0x2e_042_0x2e__0x2e__0x2e__bit11 -F_0x2e_042_0x2e__0x2e__0x2e__bit12 -F_0x2e_011012_bit_7 -F_0x2e_011012_bit_6 -F_0x2e_011012_bit_5 -F_0x2e_011012_bit_4 -F_0x2e_011012_bit_3 -F_0x2e_011012_bit_2 -F_0x2e_011012_bit_1 F_0x2e_011012_bit0 -F_0x2e_011012_bit1 F_0x2e_011012_bit2 -F_0x2e_011012_bit3 F_0x2e_011012_bit4 -F_0x2e_011012_bit5 -F_0x2e_011012_bit6 -F_0x2e_011012_bit7 -F_0x2e_011012_bit8 -F_0x2e_011012_bit9 -F_0x2e_011012_bit10 -F_0x2e_011012_bit11 -F_0x2e_011012_bit12 -F_0x2e_036037_bit_7 -F_0x2e_036037_bit_6 -F_0x2e_036037_bit_5 -F_0x2e_036037_bit_4 -F_0x2e_036037_bit_3 -F_0x2e_036037_bit_2 -F_0x2e_036037_bit_1 -F_0x2e_036037_bit0 -F_0x2e_036037_bit1 -F_0x2e_036037_bit2 -F_0x2e_036037_bit3 -F_0x2e_036037_bit4 -F_0x2e_036037_bit5 -F_0x2e_036037_bit6 -F_0x2e_036037_bit7 -F_0x2e_036037_bit8 -F_0x2e_036037_bit9 -F_0x2e_036037_bit10 -F_0x2e_036037_bit11 -F_0x2e_036037_bit12 -F_0x2e_038040_bit_7 -F_0x2e_038040_bit_6 -F_0x2e_038040_bit_5 -F_0x2e_038040_bit_4 -F_0x2e_038040_bit_3 -F_0x2e_038040_bit_2 -F_0x2e_038040_bit_1 F_0x2e_038040_bit0 -F_0x2e_038040_bit1 -F_0x2e_038040_bit2 F_0x2e_038040_bit3 -F_0x2e_038040_bit4 F_0x2e_038040_bit5 -F_0x2e_038040_bit6 -F_0x2e_038040_bit7 -F_0x2e_038040_bit8 -F_0x2e_038040_bit9 -F_0x2e_038040_bit10 -F_0x2e_038040_bit11 -F_0x2e_038040_bit12
c _______________________________________________________________________________
c 
c restarts              : 104
c conflicts             : 43132          (44 /sec)
c decisions             : 105634         (107 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 989.894 s
c _______________________________________________________________________________
#### 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.96 0.92 0.90 2/54 12638
Raw data (stat): 12638 (runsolver) R 12637 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 489038890 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0009 s]
Raw data (loadavg): 0.96 0.92 0.90 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 12630 0 0 0 967 31 0 0 25 0 1 0 489038890 60571648 12294 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14788 12294 603 41 0 14747 0
vsize: 59152
[startup+20.0016 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 12723 0 0 0 1966 31 0 0 25 0 1 0 489038890 60837888 12387 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14853 12387 603 41 0 14812 0
vsize: 59412
[startup+30.0019 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 12761 0 0 0 2965 32 0 0 25 0 1 0 489038890 60973056 12425 4294967295 134512640 134672761 3221224544 3221223760 134561990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14886 12425 603 41 0 14845 0
vsize: 59544
[startup+40.0021 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 12781 0 0 0 3965 32 0 0 25 0 1 0 489038890 61108224 12445 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14919 12445 603 41 0 14878 0
vsize: 59676
[startup+50.0029 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 12866 0 0 0 4965 32 0 0 25 0 1 0 489038890 61394944 12530 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14989 12530 603 41 0 14948 0
vsize: 59956
[startup+60.0034 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 12910 0 0 0 5966 32 0 0 25 0 1 0 489038890 61661184 12574 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 12574 603 41 0 15013 0
vsize: 60216
[startup+70.0035 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 12983 0 0 0 6965 32 0 0 25 0 1 0 489038890 61931520 12647 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15120 12647 603 41 0 15079 0
vsize: 60480
[startup+80.0043 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 13029 0 0 0 7965 33 0 0 25 0 1 0 489038890 62066688 12693 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15153 12693 603 41 0 15112 0
vsize: 60612
[startup+90.0039 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 13118 0 0 0 8965 33 0 0 25 0 1 0 489038890 62472192 12782 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15252 12782 603 41 0 15211 0
vsize: 61008
[startup+100.004 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 13210 0 0 0 9965 33 0 0 25 0 1 0 489038890 62877696 12874 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15351 12874 603 41 0 15310 0
vsize: 61404
[startup+110.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 17870 0 0 0 10953 45 0 0 25 0 1 0 489038890 78860288 17204 4294967295 134512640 134672761 3221224544 3221223844 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19253 17204 603 41 0 19212 0
vsize: 77012
[startup+120.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 17944 0 0 0 11953 45 0 0 25 0 1 0 489038890 78942208 17246 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19273 17246 603 41 0 19232 0
vsize: 77092
[startup+130.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18009 0 0 0 12953 45 0 0 25 0 1 0 489038890 79101952 17287 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19312 17287 603 41 0 19271 0
vsize: 77248
[startup+140.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18010 0 0 0 13953 46 0 0 25 0 1 0 489038890 79101952 17288 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19312 17288 603 41 0 19271 0
vsize: 77248
[startup+150.014 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18043 0 0 0 14952 46 0 0 25 0 1 0 489038890 79151104 17300 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19324 17300 603 41 0 19283 0
vsize: 77296
[startup+160.015 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18048 0 0 0 15952 46 0 0 25 0 1 0 489038890 79286272 17305 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19357 17305 603 41 0 19316 0
vsize: 77428
[startup+170.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18068 0 0 0 16952 46 0 0 25 0 1 0 489038890 79286272 17325 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19357 17325 603 41 0 19316 0
vsize: 77428
[startup+180.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18091 0 0 0 17952 46 0 0 25 0 1 0 489038890 79532032 17348 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19417 17348 603 41 0 19376 0
vsize: 77668
[startup+190.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18149 0 0 0 18952 46 0 0 25 0 1 0 489038890 79667200 17386 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19450 17386 603 41 0 19409 0
vsize: 77800
[startup+200.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18179 0 0 0 19952 46 0 0 25 0 1 0 489038890 79802368 17416 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19483 17416 603 41 0 19442 0
vsize: 77932
[startup+210.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18200 0 0 0 20952 46 0 0 25 0 1 0 489038890 79802368 17437 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19483 17437 603 41 0 19442 0
vsize: 77932
[startup+220.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18221 0 0 0 21952 47 0 0 25 0 1 0 489038890 79937536 17458 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19516 17458 603 41 0 19475 0
vsize: 78064
[startup+230.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18292 0 0 0 22952 47 0 0 25 0 1 0 489038890 80048128 17508 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19543 17508 603 41 0 19502 0
vsize: 78172
[startup+240.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18294 0 0 0 23952 47 0 0 25 0 1 0 489038890 80179200 17510 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19575 17510 603 41 0 19534 0
vsize: 78300
[startup+250.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18331 0 0 0 24953 47 0 0 25 0 1 0 489038890 80310272 17547 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19607 17547 603 41 0 19566 0
vsize: 78428
[startup+260.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18373 0 0 0 25953 47 0 0 25 0 1 0 489038890 80445440 17589 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19640 17589 603 41 0 19599 0
vsize: 78560
[startup+270.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18397 0 0 0 26952 47 0 0 25 0 1 0 489038890 80576512 17613 4294967295 134512640 134672761 3221224544 3221223744 134557892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19672 17613 603 41 0 19631 0
vsize: 78688
[startup+280.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18421 0 0 0 27952 48 0 0 25 0 1 0 489038890 80576512 17637 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19672 17637 603 41 0 19631 0
vsize: 78688
[startup+290.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18469 0 0 0 28953 48 0 0 25 0 1 0 489038890 80842752 17685 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19737 17685 603 41 0 19696 0
vsize: 78948
[startup+300.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18555 0 0 0 29953 48 0 0 25 0 1 0 489038890 81121280 17752 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19805 17752 603 41 0 19764 0
vsize: 79220
[startup+310.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18591 0 0 0 30953 48 0 0 25 0 1 0 489038890 81195008 17770 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19823 17770 603 41 0 19782 0
vsize: 79292
[startup+320.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18598 0 0 0 31953 48 0 0 25 0 1 0 489038890 81330176 17777 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19856 17777 603 41 0 19815 0
vsize: 79424
[startup+330.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18621 0 0 0 32953 48 0 0 25 0 1 0 489038890 81330176 17800 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19856 17800 603 41 0 19815 0
vsize: 79424
[startup+340.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18646 0 0 0 33953 48 0 0 25 0 1 0 489038890 81461248 17825 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19888 17825 603 41 0 19847 0
vsize: 79552
[startup+350.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18680 0 0 0 34953 48 0 0 25 0 1 0 489038890 81596416 17859 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19921 17859 603 41 0 19880 0
vsize: 79684
[startup+360.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18710 0 0 0 35953 48 0 0 25 0 1 0 489038890 81723392 17889 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19952 17889 603 41 0 19911 0
vsize: 79808
[startup+370.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18768 0 0 0 36953 48 0 0 25 0 1 0 489038890 81899520 17944 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19995 17944 603 41 0 19954 0
vsize: 79980
[startup+380.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18768 0 0 0 37953 48 0 0 25 0 1 0 489038890 81899520 17944 4294967295 134512640 134672761 3221224544 3221223696 1074743801 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19995 17944 603 41 0 19954 0
vsize: 79980
[startup+390.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18848 0 0 0 38953 49 0 0 25 0 1 0 489038890 82161664 18009 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20059 18009 603 41 0 20018 0
vsize: 80236
[startup+400.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18848 0 0 0 39953 49 0 0 25 0 1 0 489038890 82161664 18009 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20059 18009 603 41 0 20018 0
vsize: 80236
[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18889 0 0 0 40954 49 0 0 25 0 1 0 489038890 82251776 18031 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20081 18031 603 41 0 20040 0
vsize: 80324
[startup+420.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18889 0 0 0 41954 49 0 0 25 0 1 0 489038890 82251776 18031 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20081 18031 603 41 0 20040 0
vsize: 80324
[startup+430.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18894 0 0 0 42954 49 0 0 25 0 1 0 489038890 82382848 18036 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20113 18036 603 41 0 20072 0
vsize: 80452
[startup+440.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18916 0 0 0 43954 49 0 0 25 0 1 0 489038890 82382848 18058 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20113 18058 603 41 0 20072 0
vsize: 80452
[startup+450.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18976 0 0 0 44954 49 0 0 25 0 1 0 489038890 82526208 18099 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20148 18099 603 41 0 20107 0
vsize: 80592
[startup+460.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18977 0 0 0 45954 49 0 0 25 0 1 0 489038890 82526208 18100 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20148 18100 603 41 0 20107 0
vsize: 80592
[startup+470.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18982 0 0 0 46954 49 0 0 25 0 1 0 489038890 82657280 18105 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20180 18105 603 41 0 20139 0
vsize: 80720
[startup+480.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 18997 0 0 0 47954 49 0 0 25 0 1 0 489038890 82657280 18120 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20180 18120 603 41 0 20139 0
vsize: 80720
[startup+490.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19018 0 0 0 48954 49 0 0 25 0 1 0 489038890 82788352 18141 4294967295 134512640 134672761 3221224544 3221223728 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20212 18141 603 41 0 20171 0
vsize: 80848
[startup+500.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19034 0 0 0 49955 49 0 0 25 0 1 0 489038890 82788352 18157 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20212 18157 603 41 0 20171 0
vsize: 80848
[startup+510.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19046 0 0 0 50955 49 0 0 25 0 1 0 489038890 82919424 18169 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20244 18169 603 41 0 20203 0
vsize: 80976
[startup+520.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19056 0 0 0 51955 49 0 0 25 0 1 0 489038890 82919424 18179 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20244 18179 603 41 0 20203 0
vsize: 80976
[startup+530.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19074 0 0 0 52955 49 0 0 25 0 1 0 489038890 82919424 18197 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20244 18197 603 41 0 20203 0
vsize: 80976
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19109 0 0 0 53955 50 0 0 25 0 1 0 489038890 83177472 18232 4294967295 134512640 134672761 3221224544 3221223704 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20307 18232 603 41 0 20266 0
vsize: 81228
[startup+550.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19205 0 0 0 54955 50 0 0 25 0 1 0 489038890 83292160 18288 4294967295 134512640 134672761 3221224544 3221222128 134522987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20335 18288 603 41 0 20294 0
vsize: 81340
[startup+560.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19205 0 0 0 55955 50 0 0 25 0 1 0 489038890 83292160 18288 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20335 18288 603 41 0 20294 0
vsize: 81340
[startup+570.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19215 0 0 0 56955 50 0 0 25 0 1 0 489038890 83292160 18290 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20335 18290 603 41 0 20294 0
vsize: 81340
[startup+580.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19216 0 0 0 57955 50 0 0 25 0 1 0 489038890 83292160 18291 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20335 18291 603 41 0 20294 0
vsize: 81340
[startup+590.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19216 0 0 0 58955 50 0 0 25 0 1 0 489038890 83292160 18291 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20335 18291 603 41 0 20294 0
vsize: 81340
[startup+600.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19232 0 0 0 59955 50 0 0 25 0 1 0 489038890 83427328 18307 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20368 18307 603 41 0 20327 0
vsize: 81472
[startup+610.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19243 0 0 0 60956 50 0 0 25 0 1 0 489038890 83427328 18318 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20368 18318 603 41 0 20327 0
vsize: 81472
[startup+620.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19257 0 0 0 61955 51 0 0 25 0 1 0 489038890 83550208 18332 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20398 18332 603 41 0 20357 0
vsize: 81592
[startup+630.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19272 0 0 0 62955 51 0 0 25 0 1 0 489038890 83550208 18347 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20398 18347 603 41 0 20357 0
vsize: 81592
[startup+640.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19288 0 0 0 63956 51 0 0 25 0 1 0 489038890 83681280 18363 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20430 18363 603 41 0 20389 0
vsize: 81720
[startup+650.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19308 0 0 0 64956 51 0 0 25 0 1 0 489038890 83681280 18383 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20430 18383 603 41 0 20389 0
vsize: 81720
[startup+660.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19328 0 0 0 65956 51 0 0 25 0 1 0 489038890 83812352 18403 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20462 18403 603 41 0 20421 0
vsize: 81848
[startup+670.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19344 0 0 0 66956 51 0 0 25 0 1 0 489038890 83812352 18419 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20462 18419 603 41 0 20421 0
vsize: 81848
[startup+680.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19362 0 0 0 67956 51 0 0 25 0 1 0 489038890 83943424 18437 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20494 18437 603 41 0 20453 0
vsize: 81976
[startup+690.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19398 0 0 0 68956 51 0 0 25 0 1 0 489038890 84205568 18473 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20558 18473 603 41 0 20517 0
vsize: 82232
[startup+700.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19398 0 0 0 69956 51 0 0 25 0 1 0 489038890 84205568 18473 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20558 18473 603 41 0 20517 0
vsize: 82232
[startup+710.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19410 0 0 0 70956 52 0 0 25 0 1 0 489038890 84205568 18485 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20558 18485 603 41 0 20517 0
vsize: 82232
[startup+720.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19429 0 0 0 71956 52 0 0 25 0 1 0 489038890 84336640 18504 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20590 18504 603 41 0 20549 0
vsize: 82360
[startup+730.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19443 0 0 0 72957 52 0 0 25 0 1 0 489038890 84336640 18518 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20590 18518 603 41 0 20549 0
vsize: 82360
[startup+740.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19465 0 0 0 73957 52 0 0 25 0 1 0 489038890 84467712 18540 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20622 18540 603 41 0 20581 0
vsize: 82488
[startup+750.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19520 0 0 0 74957 52 0 0 25 0 1 0 489038890 84570112 18575 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20647 18575 603 41 0 20606 0
vsize: 82588
[startup+760.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19521 0 0 0 75957 52 0 0 25 0 1 0 489038890 84570112 18576 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20647 18576 603 41 0 20606 0
vsize: 82588
[startup+770.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19533 0 0 0 76957 52 0 0 25 0 1 0 489038890 84705280 18588 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20680 18588 603 41 0 20639 0
vsize: 82720
[startup+780.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19538 0 0 0 77957 52 0 0 25 0 1 0 489038890 84705280 18593 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20680 18593 603 41 0 20639 0
vsize: 82720
[startup+790.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19556 0 0 0 78957 52 0 0 25 0 1 0 489038890 84824064 18611 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20709 18611 603 41 0 20668 0
vsize: 82836
[startup+800.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19570 0 0 0 79957 52 0 0 25 0 1 0 489038890 84824064 18625 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20709 18625 603 41 0 20668 0
vsize: 82836
[startup+810.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19586 0 0 0 80957 52 0 0 25 0 1 0 489038890 84951040 18641 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20740 18641 603 41 0 20699 0
vsize: 82960
[startup+820.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19601 0 0 0 81957 52 0 0 25 0 1 0 489038890 84951040 18656 4294967295 134512640 134672761 3221224544 3221223708 134565024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20740 18656 603 41 0 20699 0
vsize: 82960
[startup+830.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19619 0 0 0 82957 52 0 0 25 0 1 0 489038890 85078016 18674 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20771 18674 603 41 0 20730 0
vsize: 83084
[startup+840.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19632 0 0 0 83958 52 0 0 25 0 1 0 489038890 85078016 18687 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20771 18687 603 41 0 20730 0
vsize: 83084
[startup+850.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19648 0 0 0 84958 52 0 0 25 0 1 0 489038890 85209088 18703 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20803 18703 603 41 0 20762 0
vsize: 83212
[startup+860.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19664 0 0 0 85958 53 0 0 25 0 1 0 489038890 85209088 18719 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20803 18719 603 41 0 20762 0
vsize: 83212
[startup+870.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19682 0 0 0 86958 53 0 0 25 0 1 0 489038890 85331968 18737 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20833 18737 603 41 0 20792 0
vsize: 83332
[startup+880.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19697 0 0 0 87958 53 0 0 25 0 1 0 489038890 85331968 18752 4294967295 134512640 134672761 3221224544 3221223728 134558658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20833 18752 603 41 0 20792 0
vsize: 83332
[startup+890.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19717 0 0 0 88958 53 0 0 25 0 1 0 489038890 85454848 18772 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20863 18772 603 41 0 20822 0
vsize: 83452
[startup+900.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19736 0 0 0 89958 53 0 0 25 0 1 0 489038890 85454848 18791 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20863 18791 603 41 0 20822 0
vsize: 83452
[startup+910.036 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19750 0 0 0 90958 53 0 0 25 0 1 0 489038890 85585920 18805 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20895 18805 603 41 0 20854 0
vsize: 83580
[startup+920.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19767 0 0 0 91959 53 0 0 25 0 1 0 489038890 85585920 18822 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20895 18822 603 41 0 20854 0
vsize: 83580
[startup+930.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19777 0 0 0 92959 53 0 0 25 0 1 0 489038890 85708800 18832 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20925 18832 603 41 0 20884 0
vsize: 83700
[startup+940.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19790 0 0 0 93959 53 0 0 25 0 1 0 489038890 85708800 18845 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20925 18845 603 41 0 20884 0
vsize: 83700
[startup+950.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19800 0 0 0 94959 53 0 0 25 0 1 0 489038890 85708800 18855 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20925 18855 603 41 0 20884 0
vsize: 83700
[startup+960.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 19808 0 0 0 95959 53 0 0 25 0 1 0 489038890 85835776 18863 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20956 18863 603 41 0 20915 0
vsize: 83824
[startup+970.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 23409 0 0 0 96951 61 0 0 25 0 1 0 489038890 113360896 22464 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27676 22464 603 41 0 27635 0
vsize: 110704
[startup+980.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 23494 0 0 0 97951 61 0 0 25 0 1 0 489038890 113496064 22549 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27709 22549 603 41 0 27668 0
vsize: 110836
[startup+990.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 23496 0 0 0 98951 61 0 0 25 0 1 0 489038890 113496064 22551 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27709 22551 603 41 0 27668 0
vsize: 110836
[startup+990.567 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 12638
Raw data (stat): 12638 (minisat+) R 12637 29151 29150 0 -1 0 23496 0 0 0 98951 61 0 0 25 0 1 0 489038890 113496064 22551 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27709 22551 603 41 0 27668 0
vsize: 0

Child status: 30
Real time (s): 990.567
CPU time (s): 990.662
CPU user time (s): 990
CPU system time (s): 0.661899
CPU usage (%): 100.01
Max. virtual memory (Kb): 110836
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	58880896
#### END VERIFIER DATA ####