PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        775660 kB
Buffers:         11048 kB
Cached:         220276 kB
SwapCached:        556 kB
Active:          74780 kB
Inactive:       158608 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        775380 kB
SwapTotal:     2097892 kB
SwapFree:      2096436 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5200 kB
Slab:            19836 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 03:33:48 (client local time) WITH STATUS 30 IN 993.909 SECONDS
stats: 18304 0 993.909 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          (43 /sec)
c decisions             : 105634         (106 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 993.136 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.92 0.98 0.94 2/55 19524
Raw data (stat): 19524 (runsolver) D 19523 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541768296 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.93 0.98 0.94 2/55 19524
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 12630 0 0 0 969 29 0 0 25 0 1 0 541768296 60571648 12294 4294967295 134512640 134672761 3221224544 3221223696 134565153 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.0006 s]
Raw data (loadavg): 0.94 0.98 0.94 2/55 19524
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 12723 0 0 0 1968 30 0 0 25 0 1 0 541768296 60837888 12387 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 12387 603 41 0 14812 0
vsize: 59412
[startup+30.0013 s]
Raw data (loadavg): 0.95 0.98 0.94 2/55 19524
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 12761 0 0 0 2967 30 0 0 25 0 1 0 541768296 60973056 12425 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14886 12425 603 41 0 14845 0
vsize: 59544
[startup+40.0008 s]
Raw data (loadavg): 0.96 0.98 0.94 2/55 19524
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 12781 0 0 0 3967 30 0 0 25 0 1 0 541768296 61108224 12445 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14919 12445 603 41 0 14878 0
vsize: 59676
[startup+50.0009 s]
Raw data (loadavg): 0.96 0.98 0.94 2/55 19524
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 12866 0 0 0 4967 31 0 0 25 0 1 0 541768296 61394944 12530 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14989 12530 603 41 0 14948 0
vsize: 59956
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.98 0.94 2/55 19524
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 12910 0 0 0 5967 31 0 0 25 0 1 0 541768296 61661184 12574 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 12574 603 41 0 15013 0
vsize: 60216
[startup+70.0013 s]
Raw data (loadavg): 0.97 0.98 0.94 2/55 19524
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 12983 0 0 0 6967 31 0 0 25 0 1 0 541768296 61931520 12647 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15120 12647 603 41 0 15079 0
vsize: 60480
[startup+80.0025 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 19524
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 13029 0 0 0 7967 31 0 0 25 0 1 0 541768296 62066688 12693 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15153 12693 603 41 0 15112 0
vsize: 60612
[startup+90.0023 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 19524
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 13115 0 0 0 8967 32 0 0 25 0 1 0 541768296 62472192 12779 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15252 12779 603 41 0 15211 0
vsize: 61008
[startup+100.002 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 19524
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 13210 0 0 0 9966 32 0 0 25 0 1 0 541768296 62877696 12874 4294967295 134512640 134672761 3221224544 3221223712 134561382 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.007 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 19524
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 17865 0 0 0 10955 44 0 0 25 0 1 0 541768296 78860288 17199 4294967295 134512640 134672761 3221224544 3221222240 134544369 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19253 17199 603 41 0 19212 0
vsize: 77012
[startup+120.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19524
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 17944 0 0 0 11955 44 0 0 25 0 1 0 541768296 78942208 17246 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19273 17246 603 41 0 19232 0
vsize: 77092
[startup+130.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19524
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18009 0 0 0 12956 44 0 0 25 0 1 0 541768296 79101952 17287 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19312 17287 603 41 0 19271 0
vsize: 77248
[startup+140.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19524
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18010 0 0 0 13954 44 0 0 25 0 1 0 541768296 79101952 17288 4294967295 134512640 134672761 3221224544 3221223712 134561218 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.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19524
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18043 0 0 0 14954 44 0 0 25 0 1 0 541768296 79151104 17300 4294967295 134512640 134672761 3221224544 3221223844 134556598 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.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19524
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18048 0 0 0 15955 44 0 0 25 0 1 0 541768296 79286272 17305 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 17305 603 41 0 19316 0
vsize: 77428
[startup+170.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18068 0 0 0 16955 45 0 0 25 0 1 0 541768296 79286272 17325 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 17325 603 41 0 19316 0
vsize: 77428
[startup+180.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18091 0 0 0 17955 45 0 0 25 0 1 0 541768296 79532032 17348 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19417 17348 603 41 0 19376 0
vsize: 77668
[startup+190.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18143 0 0 0 18954 45 0 0 25 0 1 0 541768296 79532032 17380 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19417 17380 603 41 0 19376 0
vsize: 77668
[startup+200.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18175 0 0 0 19954 45 0 0 25 0 1 0 541768296 79667200 17412 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19450 17412 603 41 0 19409 0
vsize: 77800
[startup+210.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18200 0 0 0 20954 45 0 0 25 0 1 0 541768296 79802368 17437 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19483 17437 603 41 0 19442 0
vsize: 77932
[startup+220.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18220 0 0 0 21955 45 0 0 25 0 1 0 541768296 79937536 17457 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19516 17457 603 41 0 19475 0
vsize: 78064
[startup+230.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18292 0 0 0 22955 46 0 0 25 0 1 0 541768296 80048128 17508 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19543 17508 603 41 0 19502 0
vsize: 78172
[startup+240.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18293 0 0 0 23955 46 0 0 25 0 1 0 541768296 80048128 17509 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19543 17509 603 41 0 19502 0
vsize: 78172
[startup+250.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18321 0 0 0 24955 46 0 0 25 0 1 0 541768296 80179200 17537 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19575 17537 603 41 0 19534 0
vsize: 78300
[startup+260.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18369 0 0 0 25955 46 0 0 25 0 1 0 541768296 80445440 17585 4294967295 134512640 134672761 3221224544 3221223680 134565048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19640 17586 603 41 0 19599 0
vsize: 78560
[startup+270.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18395 0 0 0 26955 46 0 0 25 0 1 0 541768296 80576512 17611 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19672 17611 603 41 0 19631 0
vsize: 78688
[startup+280.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18418 0 0 0 27955 46 0 0 25 0 1 0 541768296 80576512 17634 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19672 17634 603 41 0 19631 0
vsize: 78688
[startup+290.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18463 0 0 0 28955 47 0 0 25 0 1 0 541768296 80842752 17679 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19737 17679 603 41 0 19696 0
vsize: 78948
[startup+300.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18555 0 0 0 29955 47 0 0 25 0 1 0 541768296 81121280 17752 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19805 17752 603 41 0 19764 0
vsize: 79220
[startup+310.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18591 0 0 0 30956 47 0 0 25 0 1 0 541768296 81195008 17770 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19823 17770 603 41 0 19782 0
vsize: 79292
[startup+320.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18596 0 0 0 31956 47 0 0 25 0 1 0 541768296 81330176 17775 4294967295 134512640 134672761 3221224544 3221223648 134559841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19856 17775 603 41 0 19815 0
vsize: 79424
[startup+330.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18618 0 0 0 32956 47 0 0 25 0 1 0 541768296 81330176 17797 4294967295 134512640 134672761 3221224544 3221223680 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19856 17797 603 41 0 19815 0
vsize: 79424
[startup+340.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18644 0 0 0 33957 47 0 0 25 0 1 0 541768296 81461248 17823 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19888 17823 603 41 0 19847 0
vsize: 79552
[startup+350.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18678 0 0 0 34957 47 0 0 25 0 1 0 541768296 81596416 17857 4294967295 134512640 134672761 3221224544 3221223712 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19921 17857 603 41 0 19880 0
vsize: 79684
[startup+360.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18710 0 0 0 35957 47 0 0 25 0 1 0 541768296 81723392 17889 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19952 17889 603 41 0 19911 0
vsize: 79808
[startup+370.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18768 0 0 0 36957 48 0 0 25 0 1 0 541768296 81899520 17944 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19995 17944 603 41 0 19954 0
vsize: 79980
[startup+380.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18768 0 0 0 37957 48 0 0 25 0 1 0 541768296 81899520 17944 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19995 17944 603 41 0 19954 0
vsize: 79980
[startup+390.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18848 0 0 0 38956 48 0 0 25 0 1 0 541768296 82161664 18009 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20059 18009 603 41 0 20018 0
vsize: 80236
[startup+400.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18848 0 0 0 39956 48 0 0 25 0 1 0 541768296 82161664 18009 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20059 18009 603 41 0 20018 0
vsize: 80236
[startup+410.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18889 0 0 0 40956 49 0 0 25 0 1 0 541768296 82251776 18031 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20081 18031 603 41 0 20040 0
vsize: 80324
[startup+420.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18889 0 0 0 41956 49 0 0 25 0 1 0 541768296 82251776 18031 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20081 18031 603 41 0 20040 0
vsize: 80324
[startup+430.035 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18890 0 0 0 42956 49 0 0 25 0 1 0 541768296 82251776 18032 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20081 18032 603 41 0 20040 0
vsize: 80324
[startup+440.035 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18915 0 0 0 43956 49 0 0 25 0 1 0 541768296 82382848 18057 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20113 18057 603 41 0 20072 0
vsize: 80452
[startup+450.035 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18976 0 0 0 44956 49 0 0 25 0 1 0 541768296 82526208 18099 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20148 18099 603 41 0 20107 0
vsize: 80592
[startup+460.036 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19526
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18977 0 0 0 45956 49 0 0 25 0 1 0 541768296 82526208 18100 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20148 18100 603 41 0 20107 0
vsize: 80592
[startup+470.036 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18981 0 0 0 46957 49 0 0 25 0 1 0 541768296 82657280 18104 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20180 18104 603 41 0 20139 0
vsize: 80720
[startup+480.037 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 18996 0 0 0 47957 49 0 0 25 0 1 0 541768296 82657280 18119 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20180 18119 603 41 0 20139 0
vsize: 80720
[startup+490.038 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19015 0 0 0 48957 50 0 0 25 0 1 0 541768296 82788352 18138 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20212 18138 603 41 0 20171 0
vsize: 80848
[startup+500.038 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19030 0 0 0 49957 50 0 0 25 0 1 0 541768296 82788352 18153 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20212 18153 603 41 0 20171 0
vsize: 80848
[startup+510.038 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19044 0 0 0 50957 50 0 0 25 0 1 0 541768296 82919424 18167 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20244 18167 603 41 0 20203 0
vsize: 80976
[startup+520.038 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19054 0 0 0 51957 50 0 0 25 0 1 0 541768296 82919424 18177 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20244 18177 603 41 0 20203 0
vsize: 80976
[startup+530.038 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19067 0 0 0 52957 50 0 0 25 0 1 0 541768296 82919424 18190 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20244 18190 603 41 0 20203 0
vsize: 80976
[startup+540.038 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19101 0 0 0 53957 50 0 0 25 0 1 0 541768296 83050496 18224 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20276 18224 603 41 0 20235 0
vsize: 81104
[startup+550.039 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19200 0 0 0 54957 51 0 0 25 0 1 0 541768296 83292160 18283 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20335 18283 603 41 0 20294 0
vsize: 81340
[startup+560.039 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19205 0 0 0 55957 51 0 0 25 0 1 0 541768296 83292160 18288 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20335 18288 603 41 0 20294 0
vsize: 81340
[startup+570.039 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19215 0 0 0 56957 51 0 0 25 0 1 0 541768296 83292160 18290 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20335 18290 603 41 0 20294 0
vsize: 81340
[startup+580.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19216 0 0 0 57957 51 0 0 25 0 1 0 541768296 83292160 18291 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20335 18291 603 41 0 20294 0
vsize: 81340
[startup+590.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19216 0 0 0 58957 51 0 0 25 0 1 0 541768296 83292160 18291 4294967295 134512640 134672761 3221224544 3221223712 134561275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20335 18291 603 41 0 20294 0
vsize: 81340
[startup+600.041 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19227 0 0 0 59957 51 0 0 25 0 1 0 541768296 83427328 18302 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 18302 603 41 0 20327 0
vsize: 81472
[startup+610.042 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19241 0 0 0 60958 51 0 0 25 0 1 0 541768296 83427328 18316 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 18316 603 41 0 20327 0
vsize: 81472
[startup+620.041 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19254 0 0 0 61958 51 0 0 25 0 1 0 541768296 83550208 18329 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20398 18329 603 41 0 20357 0
vsize: 81592
[startup+630.042 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19270 0 0 0 62958 51 0 0 25 0 1 0 541768296 83550208 18345 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20398 18345 603 41 0 20357 0
vsize: 81592
[startup+640.042 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19283 0 0 0 63958 51 0 0 25 0 1 0 541768296 83681280 18358 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20430 18358 603 41 0 20389 0
vsize: 81720
[startup+650.042 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19303 0 0 0 64958 51 0 0 25 0 1 0 541768296 83681280 18378 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20430 18378 603 41 0 20389 0
vsize: 81720
[startup+660.043 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19323 0 0 0 65958 51 0 0 25 0 1 0 541768296 83812352 18398 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20462 18398 603 41 0 20421 0
vsize: 81848
[startup+670.043 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19340 0 0 0 66958 52 0 0 25 0 1 0 541768296 83812352 18415 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20462 18415 603 41 0 20421 0
vsize: 81848
[startup+680.043 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19360 0 0 0 67958 52 0 0 25 0 1 0 541768296 83943424 18435 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20494 18435 603 41 0 20453 0
vsize: 81976
[startup+690.044 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19398 0 0 0 68958 52 0 0 25 0 1 0 541768296 84205568 18473 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20558 18473 603 41 0 20517 0
vsize: 82232
[startup+700.043 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19398 0 0 0 69958 52 0 0 25 0 1 0 541768296 84205568 18473 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20558 18473 603 41 0 20517 0
vsize: 82232
[startup+710.044 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19407 0 0 0 70959 52 0 0 25 0 1 0 541768296 84205568 18482 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20558 18482 603 41 0 20517 0
vsize: 82232
[startup+720.044 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19422 0 0 0 71959 52 0 0 25 0 1 0 541768296 84336640 18497 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20590 18497 603 41 0 20549 0
vsize: 82360
[startup+730.045 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19440 0 0 0 72959 52 0 0 25 0 1 0 541768296 84336640 18515 4294967295 134512640 134672761 3221224544 3221223704 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20590 18515 603 41 0 20549 0
vsize: 82360
[startup+740.045 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19459 0 0 0 73959 52 0 0 25 0 1 0 541768296 84467712 18534 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20622 18534 603 41 0 20581 0
vsize: 82488
[startup+750.046 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19520 0 0 0 74959 52 0 0 25 0 1 0 541768296 84570112 18575 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20647 18575 603 41 0 20606 0
vsize: 82588
[startup+760.046 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19528
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19521 0 0 0 75959 52 0 0 25 0 1 0 541768296 84570112 18576 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20647 18576 603 41 0 20606 0
vsize: 82588
[startup+770.046 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19533 0 0 0 76959 52 0 0 25 0 1 0 541768296 84705280 18588 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20680 18588 603 41 0 20639 0
vsize: 82720
[startup+780.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19534 0 0 0 77960 52 0 0 25 0 1 0 541768296 84705280 18589 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20680 18589 603 41 0 20639 0
vsize: 82720
[startup+790.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19554 0 0 0 78960 52 0 0 25 0 1 0 541768296 84705280 18609 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20680 18609 603 41 0 20639 0
vsize: 82720
[startup+800.048 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19565 0 0 0 79960 52 0 0 25 0 1 0 541768296 84824064 18620 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20709 18620 603 41 0 20668 0
vsize: 82836
[startup+810.048 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19581 0 0 0 80960 52 0 0 25 0 1 0 541768296 84824064 18636 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20709 18636 603 41 0 20668 0
vsize: 82836
[startup+820.048 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19598 0 0 0 81960 52 0 0 25 0 1 0 541768296 84951040 18653 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20740 18653 603 41 0 20699 0
vsize: 82960
[startup+830.048 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19612 0 0 0 82960 53 0 0 25 0 1 0 541768296 84951040 18667 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20740 18667 603 41 0 20699 0
vsize: 82960
[startup+840.048 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19628 0 0 0 83960 53 0 0 25 0 1 0 541768296 85078016 18683 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20771 18683 603 41 0 20730 0
vsize: 83084
[startup+850.048 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19643 0 0 0 84960 53 0 0 25 0 1 0 541768296 85078016 18698 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20771 18698 603 41 0 20730 0
vsize: 83084
[startup+860.049 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19663 0 0 0 85961 53 0 0 25 0 1 0 541768296 85209088 18718 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20803 18718 603 41 0 20762 0
vsize: 83212
[startup+870.049 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19677 0 0 0 86961 53 0 0 25 0 1 0 541768296 85209088 18732 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20803 18732 603 41 0 20762 0
vsize: 83212
[startup+880.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19693 0 0 0 87961 53 0 0 25 0 1 0 541768296 85331968 18748 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20833 18748 603 41 0 20792 0
vsize: 83332
[startup+890.049 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19714 0 0 0 88961 53 0 0 25 0 1 0 541768296 85454848 18769 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20863 18769 603 41 0 20822 0
vsize: 83452
[startup+900.049 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19731 0 0 0 89961 53 0 0 25 0 1 0 541768296 85454848 18786 4294967295 134512640 134672761 3221224544 3221223712 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20863 18786 603 41 0 20822 0
vsize: 83452
[startup+910.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19746 0 0 0 90961 53 0 0 25 0 1 0 541768296 85585920 18801 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20895 18801 603 41 0 20854 0
vsize: 83580
[startup+920.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19765 0 0 0 91961 53 0 0 25 0 1 0 541768296 85585920 18820 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20895 18820 603 41 0 20854 0
vsize: 83580
[startup+930.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19776 0 0 0 92962 53 0 0 25 0 1 0 541768296 85708800 18831 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20925 18831 603 41 0 20884 0
vsize: 83700
[startup+940.051 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19788 0 0 0 93962 53 0 0 25 0 1 0 541768296 85708800 18843 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20925 18843 603 41 0 20884 0
vsize: 83700
[startup+950.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19797 0 0 0 94962 53 0 0 25 0 1 0 541768296 85708800 18852 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20925 18852 603 41 0 20884 0
vsize: 83700
[startup+960.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 19808 0 0 0 95962 53 0 0 25 0 1 0 541768296 85835776 18863 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20956 18863 603 41 0 20915 0
vsize: 83824
[startup+970.051 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 23409 0 0 0 96954 61 0 0 25 0 1 0 541768296 113360896 22464 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27676 22464 603 41 0 27635 0
vsize: 110704
[startup+980.052 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 23494 0 0 0 97954 62 0 0 25 0 1 0 541768296 113496064 22549 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27709 22549 603 41 0 27668 0
vsize: 110836
[startup+990.052 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 23496 0 0 0 98954 62 0 0 25 0 1 0 541768296 113496064 22551 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27709 22551 603 41 0 27668 0
vsize: 110836
[startup+993.799 s]
Raw data (loadavg): 0.99 0.98 0.94 1/54 19530
Raw data (stat): 19524 (minisat+) R 19523 22929 22928 0 -1 0 23496 0 0 0 98954 62 0 0 25 0 1 0 541768296 113496064 22551 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27709 22551 603 41 0 27668 0
vsize: 0

Child status: 30
Real time (s): 993.798
CPU time (s): 993.909
CPU user time (s): 993.239
CPU system time (s): 0.669898
CPU usage (%): 100.011
Max. virtual memory (Kb): 110836
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	58880896
#### END VERIFIER DATA ####