Reconstruction of the 35-move Snaky certificate

import Mathlibnamespace OAInamespace SnakyCertificateinstance rotationModulus_neZero : NeZero 8 := @Nat.instNeZeroSucc 7instance digitModulus_neZero : NeZero 10 := @Nat.instNeZeroSucc 9abbrev Cell := ℤ × ℤdef origin : Cell := (0, 0)def snaky : Finset Cell := {(0, 0), (1, 0), (2, 0), (3, 0), (3, 1), (4, 1)}def orient (r : Fin 8) (p : Cell) : Cell :=  match r.val with  | 0 => (p.1, p.2)  | 1 => (p.2, p.1)  | 2 => (p.1, -p.2)  | 3 => (-p.2, p.1)  | 4 => (-p.1, p.2)  | 5 => (p.2, -p.1)  | 6 => (-p.1, -p.2)  | _ => (-p.2, -p.1)def placement (r : Fin 8) (t p : Cell) : Cell := orient r p + tdef basePoint (i : Fin 6) : Cell := ![(0,0),(1,0),(2,0),(3,0),(3,1),(4,1)] idef baseEnvelope (i : Fin 6) : Finset Cell :=  snaky.image (placement 0 (-basePoint i))def baseRequired (i : Fin 6) : Finset Cell := (baseEnvelope i).erase originstructure Term where  child : ℕ  rotation : Fin 8  xDigit : Fin 10  yDigit : Fin 10  deriving DecidableEq, Reprdef Term.shift (t : Term) : Cell := ((t.xDigit.val : ℤ) - 4, (t.yDigit.val : ℤ) - 4)structure Entry where  index : ℕ  terms : List Term  deriving DecidableEq, Reprdef emptyEntry : Entry := ⟨0, []⟩def entry_6 : Entry := ⟨6, [⟨0, 0, 0, 3⟩]⟩def entry_7 : Entry := ⟨7, [⟨4, 0, 3, 4⟩, ⟨6, 0, 5, 4⟩]⟩def entry_8 : Entry := ⟨8, [⟨0, 4, 8, 3⟩, ⟨6, 4, 3, 4⟩]⟩def entry_9 : Entry := ⟨9, [⟨0, 4, 5, 4⟩, ⟨6, 4, 0, 5⟩]⟩def entry_10 : Entry := ⟨10, [⟨2, 0, 2, 3⟩, ⟨2, 6, 2, 4⟩]⟩def entry_11 : Entry := ⟨11, [⟨6, 4, 2, 5⟩, ⟨6, 6, 2, 3⟩]⟩def entry_12 : Entry := ⟨12, [⟨0, 6, 5, 4⟩, ⟨0, 0, 0, 3⟩]⟩def entry_13 : Entry := ⟨13, [⟨6, 6, 0, 3⟩, ⟨6, 4, 0, 5⟩]⟩def entry_14 : Entry := ⟨14, [⟨0, 6, 5, 4⟩, ⟨3, 6, 1, 4⟩]⟩def entry_15 : Entry := ⟨15, [⟨0, 6, 6, 4⟩, ⟨3, 6, 2, 4⟩]⟩def entry_16 : Entry := ⟨16, [⟨3, 6, 3, 4⟩, ⟨0, 6, 7, 4⟩]⟩def entry_17 : Entry := ⟨17, [⟨0, 6, 5, 4⟩, ⟨3, 0, 3, 3⟩]⟩def entry_18 : Entry := ⟨18, [⟨3, 6, 2, 4⟩, ⟨3, 0, 4, 3⟩]⟩def entry_19 : Entry := ⟨19, [⟨6, 4, 1, 5⟩, ⟨6, 0, 6, 5⟩]⟩def entry_20 : Entry := ⟨20, [⟨6, 4, 0, 5⟩, ⟨6, 0, 5, 5⟩]⟩def entry_21 : Entry := ⟨21, [⟨4, 6, 2, 3⟩, ⟨6, 0, 6, 5⟩]⟩def entry_22 : Entry := ⟨22, [⟨0, 6, 7, 5⟩, ⟨3, 0, 5, 4⟩]⟩def entry_23 : Entry := ⟨23, [⟨0, 6, 6, 4⟩, ⟨0, 0, 1, 3⟩]⟩def entry_24 : Entry := ⟨24, [⟨0, 0, 0, 3⟩, ⟨17, 0, 5, 4⟩]⟩def entry_25 : Entry := ⟨25, [⟨0, 0, 0, 3⟩, ⟨14, 0, 5, 4⟩]⟩def entry_26 : Entry := ⟨26, [⟨0, 4, 6, 4⟩, ⟨6, 0, 6, 5⟩]⟩def entry_27 : Entry := ⟨27, [⟨0, 6, 5, 4⟩, ⟨6, 4, 0, 5⟩]⟩def entry_28 : Entry := ⟨28, [⟨6, 1, 4, 5⟩, ⟨0, 6, 6, 4⟩]⟩def entry_29 : Entry := ⟨29, [⟨1, 4, 7, 3⟩, ⟨6, 3, 4, 5⟩]⟩def entry_30 : Entry := ⟨30, [⟨0, 0, 1, 3⟩, ⟨14, 0, 6, 4⟩]⟩def entry_31 : Entry := ⟨31, [⟨0, 0, 1, 4⟩, ⟨17, 0, 6, 5⟩]⟩def entry_32 : Entry := ⟨32, [⟨0, 4, 8, 3⟩, ⟨6, 3, 4, 5⟩]⟩def entry_33 : Entry := ⟨33, [⟨0, 0, 2, 4⟩, ⟨17, 0, 7, 5⟩]⟩def entry_34 : Entry := ⟨34, [⟨6, 1, 4, 5⟩, ⟨1, 6, 5, 4⟩]⟩def entry_35 : Entry := ⟨35, [⟨0, 0, 2, 4⟩, ⟨14, 0, 7, 5⟩]⟩def entry_36 : Entry := ⟨36, [⟨0, 0, 3, 4⟩, ⟨17, 0, 8, 5⟩]⟩def entry_37 : Entry := ⟨37, [⟨6, 3, 4, 5⟩, ⟨2, 4, 6, 3⟩]⟩def entry_38 : Entry := ⟨38, [⟨3, 0, 3, 3⟩, ⟨16, 0, 2, 4⟩]⟩def entry_39 : Entry := ⟨39, [⟨0, 0, 1, 3⟩, ⟨17, 0, 6, 4⟩]⟩def entry_40 : Entry := ⟨40, [⟨3, 0, 4, 3⟩, ⟨16, 0, 3, 4⟩]⟩def entry_41 : Entry := ⟨41, [⟨6, 3, 3, 5⟩, ⟨1, 4, 6, 3⟩]⟩def entry_42 : Entry := ⟨42, [⟨0, 6, 6, 4⟩, ⟨6, 4, 1, 5⟩]⟩def entry_43 : Entry := ⟨43, [⟨2, 4, 5, 3⟩, ⟨6, 3, 3, 5⟩]⟩def entry_44 : Entry := ⟨44, [⟨4, 4, 1, 5⟩, ⟨7, 0, 4, 5⟩]⟩def entry_45 : Entry := ⟨45, [⟨6, 4, 0, 5⟩, ⟨7, 0, 4, 5⟩]⟩def entry_46 : Entry := ⟨46, [⟨6, 6, 0, 3⟩, ⟨7, 0, 4, 5⟩]⟩def entry_47 : Entry := ⟨47, [⟨6, 3, 3, 5⟩, ⟨6, 2, 7, 3⟩]⟩def entry_48 : Entry := ⟨48, [⟨6, 3, 4, 5⟩, ⟨6, 2, 8, 3⟩]⟩def entry_49 : Entry := ⟨49, [⟨4, 7, 3, 1⟩, ⟨7, 1, 5, 4⟩]⟩def entry_50 : Entry := ⟨50, [⟨6, 3, 3, 5⟩, ⟨7, 1, 5, 4⟩]⟩def entry_51 : Entry := ⟨51, [⟨10, 2, 5, 3⟩, ⟨10, 0, 5, 4⟩, ⟨26, 2, 3, 4⟩, ⟨26, 0, 3, 3⟩]⟩def entry_52 : Entry := ⟨52, [⟨0, 0, 0, 3⟩, ⟨0, 4, 7, 3⟩]⟩def entry_53 : Entry := ⟨53, [⟨6, 4, 3, 4⟩, ⟨3, 1, 4, 5⟩]⟩def entry_54 : Entry := ⟨54, [⟨22, 0, 2, 3⟩, ⟨3, 6, 1, 4⟩]⟩def entry_55 : Entry := ⟨55, [⟨7, 4, 0, 5⟩, ⟨7, 0, 4, 5⟩]⟩def entry_56 : Entry := ⟨56, [⟨7, 4, 0, 5⟩, ⟨7, 6, 0, 3⟩]⟩def entry_57 : Entry := ⟨57, [⟨0, 6, 5, 4⟩, ⟨7, 0, 4, 5⟩]⟩def entry_58 : Entry := ⟨58, [⟨0, 4, 5, 4⟩, ⟨7, 0, 4, 5⟩]⟩def entry_59 : Entry := ⟨59, [⟨0, 6, 5, 4⟩, ⟨7, 4, 0, 5⟩]⟩def entry_60 : Entry := ⟨60, [⟨6, 6, 1, 3⟩, ⟨49, 1, 6, 4⟩]⟩def entry_61 : Entry := ⟨61, [⟨6, 0, 5, 4⟩, ⟨14, 1, 4, 5⟩]⟩def entry_62 : Entry := ⟨62, [⟨6, 6, 0, 3⟩, ⟨53, 0, 1, 5⟩]⟩def entry_63 : Entry := ⟨63, [⟨4, 3, 4, 3⟩, ⟨50, 0, 5, 4⟩]⟩def entry_64 : Entry := ⟨64, [⟨6, 6, 3, 4⟩, ⟨49, 1, 8, 5⟩]⟩def entry_65 : Entry := ⟨65, [⟨6, 6, 0, 3⟩, ⟨49, 1, 5, 4⟩]⟩def entry_66 : Entry := ⟨66, [⟨6, 3, 4, 5⟩, ⟨53, 5, 6, 4⟩]⟩def entry_67 : Entry := ⟨67, [⟨6, 1, 4, 5⟩, ⟨9, 2, 5, 4⟩]⟩def entry_68 : Entry := ⟨68, [⟨6, 4, 0, 5⟩, ⟨44, 0, 5, 4⟩]⟩def entry_69 : Entry := ⟨69, [⟨6, 3, 4, 5⟩, ⟨34, 0, 6, 5⟩]⟩def entry_70 : Entry := ⟨70, [⟨4, 3, 4, 3⟩, ⟨41, 0, 5, 4⟩]⟩def entry_71 : Entry := ⟨71, [⟨6, 1, 4, 5⟩, ⟨23, 2, 4, 3⟩]⟩def entry_72 : Entry := ⟨72, [⟨0, 5, 3, 8⟩, ⟨8, 6, 5, 4⟩]⟩def entry_73 : Entry := ⟨73, [⟨4, 3, 3, 4⟩, ⟨50, 0, 4, 5⟩]⟩def entry_74 : Entry := ⟨74, [⟨2, 7, 4, 3⟩, ⟨53, 0, 3, 3⟩]⟩def entry_75 : Entry := ⟨75, [⟨0, 0, 1, 3⟩, ⟨9, 0, 7, 3⟩]⟩def entry_76 : Entry := ⟨76, [⟨0, 7, 5, 7⟩, ⟨14, 0, 7, 5⟩]⟩def entry_77 : Entry := ⟨77, [⟨0, 5, 3, 7⟩, ⟨12, 0, 5, 4⟩]⟩def entry_78 : Entry := ⟨78, [⟨6, 4, 3, 4⟩, ⟨52, 0, 5, 4⟩]⟩def entry_79 : Entry := ⟨79, [⟨6, 1, 5, 5⟩, ⟨48, 0, 3, 4⟩]⟩def entry_80 : Entry := ⟨80, [⟨0, 6, 6, 4⟩, ⟨13, 4, 2, 4⟩]⟩def entry_81 : Entry := ⟨81, [⟨4, 3, 4, 3⟩, ⟨43, 0, 5, 4⟩]⟩def entry_82 : Entry := ⟨82, [⟨6, 1, 4, 5⟩, ⟨36, 0, 1, 3⟩]⟩def entry_83 : Entry := ⟨83, [⟨0, 7, 5, 7⟩, ⟨67, 2, 6, 3⟩]⟩def entry_84 : Entry := ⟨84, [⟨6, 3, 4, 5⟩, ⟨67, 0, 6, 4⟩]⟩def entry_85 : Entry := ⟨85, [⟨9, 0, 6, 3⟩, ⟨8, 4, 5, 4⟩]⟩def entry_86 : Entry := ⟨86, [⟨0, 6, 5, 4⟩, ⟨67, 3, 1, 5⟩]⟩def entry_87 : Entry := ⟨87, [⟨0, 5, 3, 7⟩, ⟨24, 2, 5, 3⟩]⟩def entry_88 : Entry := ⟨88, [⟨0, 6, 6, 4⟩, ⟨67, 3, 2, 5⟩]⟩def entry_89 : Entry := ⟨89, [⟨8, 3, 3, 1⟩, ⟨7, 1, 5, 4⟩]⟩def entry_90 : Entry := ⟨90, [⟨31, 0, 3, 3⟩, ⟨54, 6, 0, 3⟩, ⟨54, 0, 5, 4⟩, ⟨31, 6, 2, 4⟩]⟩def entry_91 : Entry := ⟨91, [⟨6, 3, 4, 5⟩, ⟨74, 5, 7, 3⟩]⟩def entry_92 : Entry := ⟨92, [⟨6, 1, 4, 5⟩, ⟨33, 0, 2, 3⟩]⟩def entry_93 : Entry := ⟨93, [⟨4, 3, 4, 3⟩, ⟨47, 0, 5, 4⟩]⟩def entry_94 : Entry := ⟨94, [⟨6, 1, 4, 5⟩, ⟨27, 3, 3, 6⟩]⟩def entry_95 : Entry := ⟨95, [⟨0, 5, 3, 7⟩, ⟨29, 0, 2, 5⟩]⟩def entry_96 : Entry := ⟨96, [⟨6, 1, 5, 5⟩, ⟨70, 0, 3, 5⟩]⟩def entry_97 : Entry := ⟨97, [⟨6, 6, 0, 3⟩, ⟨44, 0, 5, 4⟩]⟩def entry_98 : Entry := ⟨98, [⟨6, 6, 2, 3⟩, ⟨44, 0, 7, 4⟩]⟩def entry_99 : Entry := ⟨99, [⟨2, 1, 3, 2⟩, ⟨24, 0, 5, 4⟩]⟩def entry_100 : Entry := ⟨100, [⟨0, 6, 5, 4⟩, ⟨48, 0, 1, 4⟩]⟩def entry_101 : Entry := ⟨101, [⟨0, 7, 4, 6⟩, ⟨24, 0, 5, 4⟩]⟩def entry_102 : Entry := ⟨102, [⟨6, 3, 4, 5⟩, ⟨25, 2, 6, 3⟩]⟩def entry_103 : Entry := ⟨103, [⟨6, 3, 4, 5⟩, ⟨71, 0, 6, 4⟩]⟩def entry_104 : Entry := ⟨104, [⟨6, 0, 5, 4⟩, ⟨75, 0, 3, 4⟩]⟩def entry_105 : Entry := ⟨105, [⟨6, 5, 4, 3⟩, ⟨77, 0, 4, 5⟩]⟩def entry_106 : Entry := ⟨106, [⟨6, 1, 4, 5⟩, ⟨36, 6, 5, 4⟩]⟩def entry_107 : Entry := ⟨107, [⟨6, 6, 0, 3⟩, ⟨63, 1, 5, 3⟩]⟩def entry_108 : Entry := ⟨108, [⟨4, 6, 1, 3⟩, ⟨63, 1, 5, 3⟩]⟩def entry_109 : Entry := ⟨109, [⟨4, 6, 1, 3⟩, ⟨55, 0, 5, 4⟩]⟩def entry_110 : Entry := ⟨110, [⟨6, 6, 1, 3⟩, ⟨63, 1, 6, 3⟩]⟩def entry_111 : Entry := ⟨111, [⟨6, 7, 4, 3⟩, ⟨83, 0, 4, 5⟩]⟩def entry_112 : Entry := ⟨112, [⟨4, 1, 5, 4⟩, ⟨93, 0, 3, 5⟩]⟩def entry_113 : Entry := ⟨113, [⟨1, 6, 6, 4⟩, ⟨36, 6, 7, 5⟩]⟩def entry_114 : Entry := ⟨114, [⟨6, 0, 6, 5⟩, ⟨67, 3, 2, 5⟩]⟩def entry_115 : Entry := ⟨115, [⟨6, 2, 7, 3⟩, ⟨70, 7, 2, 5⟩]⟩def entry_116 : Entry := ⟨116, [⟨0, 7, 4, 6⟩, ⟨24, 2, 5, 4⟩]⟩def entry_117 : Entry := ⟨117, [⟨6, 1, 4, 5⟩, ⟨100, 0, 5, 4⟩]⟩def entry_118 : Entry := ⟨118, [⟨4, 7, 3, 1⟩, ⟨61, 1, 5, 4⟩]⟩def entry_119 : Entry := ⟨119, [⟨6, 6, 1, 3⟩, ⟨55, 0, 6, 4⟩]⟩def entry_120 : Entry := ⟨120, [⟨4, 0, 4, 5⟩, ⟨58, 2, 5, 4⟩]⟩def entry_121 : Entry := ⟨121, [⟨9, 3, 4, 5⟩, ⟨7, 1, 5, 4⟩]⟩def entry_122 : Entry := ⟨122, [⟨6, 6, 3, 3⟩, ⟨105, 1, 4, 5⟩]⟩def entry_123 : Entry := ⟨123, [⟨6, 6, 1, 3⟩, ⟨64, 2, 2, 5⟩]⟩def entry_124 : Entry := ⟨124, [⟨6, 1, 4, 5⟩, ⟨31, 2, 5, 4⟩]⟩def entry_125 : Entry := ⟨125, [⟨3, 0, 4, 3⟩, ⟨31, 2, 4, 5⟩]⟩def entry_126 : Entry := ⟨126, [⟨6, 3, 4, 5⟩, ⟨46, 1, 5, 7⟩]⟩def entry_127 : Entry := ⟨127, [⟨7, 0, 4, 5⟩, ⟨44, 2, 5, 4⟩]⟩def entry_128 : Entry := ⟨128, [⟨9, 6, 1, 5⟩, ⟨57, 0, 6, 5⟩]⟩def entry_129 : Entry := ⟨129, [⟨6, 4, 2, 5⟩, ⟨58, 1, 3, 6⟩]⟩def entry_130 : Entry := ⟨130, [⟨6, 1, 4, 5⟩, ⟨60, 0, 5, 4⟩]⟩def entry_131 : Entry := ⟨131, [⟨45, 3, 4, 5⟩, ⟨7, 1, 5, 4⟩]⟩def entry_132 : Entry := ⟨132, [⟨6, 3, 4, 5⟩, ⟨89, 0, 5, 6⟩]⟩def entry_133 : Entry := ⟨133, [⟨6, 7, 3, 1⟩, ⟨92, 0, 5, 5⟩]⟩def entry_134 : Entry := ⟨134, [⟨6, 7, 3, 0⟩, ⟨82, 0, 5, 4⟩]⟩def entry_135 : Entry := ⟨135, [⟨7, 0, 4, 5⟩, ⟨75, 4, 2, 5⟩, ⟨44, 0, 5, 4⟩]⟩def entry_136 : Entry := ⟨136, [⟨6, 3, 3, 7⟩, ⟨102, 2, 3, 3⟩]⟩def entry_137 : Entry := ⟨137, [⟨4, 1, 4, 3⟩, ⟨96, 0, 3, 4⟩]⟩def entry_138 : Entry := ⟨138, [⟨27, 0, 5, 4⟩, ⟨10, 1, 4, 7⟩]⟩def entry_139 : Entry := ⟨139, [⟨28, 1, 4, 5⟩, ⟨27, 0, 5, 4⟩]⟩def entry_140 : Entry := ⟨140, [⟨6, 7, 3, 2⟩, ⟨82, 0, 5, 6⟩]⟩def entry_141 : Entry := ⟨141, [⟨7, 0, 4, 5⟩, ⟨78, 2, 1, 3⟩]⟩def entry_142 : Entry := ⟨142, [⟨72, 4, 2, 3⟩, ⟨32, 1, 4, 3⟩, ⟨55, 2, 5, 4⟩]⟩def entry_143 : Entry := ⟨143, [⟨6, 6, 3, 4⟩, ⟨108, 0, 8, 5⟩]⟩def entry_144 : Entry := ⟨144, [⟨7, 0, 4, 5⟩, ⟨104, 4, 1, 5⟩, ⟨55, 0, 5, 4⟩]⟩def entry_145 : Entry := ⟨145, [⟨0, 5, 4, 5⟩, ⟨91, 0, 3, 4⟩]⟩def entry_146 : Entry := ⟨146, [⟨36, 6, 5, 4⟩, ⟨24, 1, 4, 5⟩]⟩def entry_147 : Entry := ⟨147, [⟨53, 0, 1, 5⟩, ⟨44, 2, 5, 4⟩]⟩def entry_148 : Entry := ⟨148, [⟨7, 1, 5, 4⟩, ⟨46, 1, 4, 5⟩, ⟨94, 0, 5, 3⟩, ⟨97, 1, 4, 5⟩]⟩def entry_149 : Entry := ⟨149, [⟨16, 1, 4, 3⟩, ⟨24, 2, 5, 4⟩]⟩def entry_150 : Entry := ⟨150, [⟨4, 6, 1, 3⟩, ⟨126, 5, 2, 5⟩]⟩def entry_151 : Entry := ⟨151, [⟨2, 1, 4, 3⟩, ⟨101, 2, 6, 3⟩]⟩def entry_152 : Entry := ⟨152, [⟨6, 3, 4, 5⟩, ⟨73, 1, 7, 4⟩]⟩def entry_153 : Entry := ⟨153, [⟨59, 4, 0, 4⟩, ⟨27, 0, 5, 4⟩]⟩def entry_154 : Entry := ⟨154, [⟨7, 6, 4, 3⟩, ⟨104, 0, 7, 5⟩]⟩def entry_155 : Entry := ⟨155, [⟨7, 1, 5, 4⟩, ⟨55, 3, 4, 5⟩]⟩def entry_156 : Entry := ⟨156, [⟨11, 0, 2, 4⟩, ⟨98, 2, 2, 4⟩, ⟨33, 0, 2, 3⟩]⟩def entry_157 : Entry := ⟨157, [⟨6, 3, 4, 5⟩, ⟨57, 1, 5, 6⟩]⟩def entry_158 : Entry := ⟨158, [⟨66, 0, 3, 4⟩, ⟨45, 1, 4, 5⟩, ⟨46, 3, 4, 5⟩]⟩def entry_159 : Entry := ⟨159, [⟨45, 3, 4, 5⟩, ⟨65, 1, 4, 5⟩, ⟨7, 3, 3, 4⟩]⟩def entry_160 : Entry := ⟨160, [⟨63, 1, 8, 3⟩, ⟨32, 3, 4, 3⟩]⟩def entry_161 : Entry := ⟨161, [⟨15, 1, 4, 5⟩, ⟨86, 0, 5, 4⟩]⟩def entry_162 : Entry := ⟨162, [⟨7, 3, 3, 4⟩, ⟨127, 1, 4, 5⟩, ⟨63, 0, 3, 5⟩, ⟨157, 0, 3, 3⟩]⟩def entry_163 : Entry := ⟨163, [⟨44, 2, 5, 4⟩, ⟨49, 1, 5, 4⟩, ⟨56, 4, 0, 4⟩]⟩def entry_164 : Entry := ⟨164, [⟨6, 1, 4, 5⟩, ⟨110, 0, 5, 4⟩]⟩def entry_165 : Entry := ⟨165, [⟨0, 7, 5, 8⟩, ⟨107, 0, 7, 5⟩]⟩def entry_166 : Entry := ⟨166, [⟨2, 7, 4, 5⟩, ⟨107, 0, 6, 4⟩]⟩def entry_167 : Entry := ⟨167, [⟨57, 0, 5, 4⟩, ⟨57, 4, 0, 4⟩]⟩def entry_168 : Entry := ⟨168, [⟨6, 1, 5, 5⟩, ⟨152, 0, 3, 4⟩]⟩def entry_169 : Entry := ⟨169, [⟨28, 3, 4, 5⟩, ⟨63, 1, 8, 3⟩]⟩def entry_170 : Entry := ⟨170, [⟨4, 6, 1, 3⟩, ⟨127, 2, 5, 4⟩]⟩def entry_171 : Entry := ⟨171, [⟨6, 0, 5, 4⟩, ⟨91, 0, 0, 5⟩]⟩def entry_172 : Entry := ⟨172, [⟨63, 1, 5, 3⟩, ⟨55, 6, 0, 4⟩, ⟨64, 0, 1, 3⟩]⟩def entry_173 : Entry := ⟨173, [⟨63, 1, 5, 3⟩, ⟨64, 6, 4, 5⟩, ⟨55, 6, 0, 4⟩]⟩def entry_174 : Entry := ⟨174, [⟨58, 3, 4, 5⟩, ⟨57, 1, 4, 5⟩, ⟨84, 0, 3, 4⟩]⟩def entry_175 : Entry := ⟨175, [⟨141, 0, 5, 4⟩, ⟨7, 2, 4, 3⟩, ⟨63, 1, 5, 3⟩]⟩def entry_176 : Entry := ⟨176, [⟨63, 1, 5, 3⟩, ⟨64, 6, 4, 5⟩, ⟨55, 2, 5, 4⟩]⟩def entry_177 : Entry := ⟨177, [⟨6, 1, 4, 5⟩, ⟨136, 3, 5, 4⟩]⟩def entry_178 : Entry := ⟨178, [⟨37, 0, 3, 4⟩, ⟨68, 1, 4, 5⟩, ⟨46, 3, 4, 5⟩]⟩def entry_179 : Entry := ⟨179, [⟨6, 6, 0, 3⟩, ⟨148, 5, 5, 4⟩]⟩def entry_180 : Entry := ⟨180, [⟨7, 3, 3, 4⟩, ⟨63, 0, 3, 5⟩, ⟨155, 0, 4, 5⟩, ⟨132, 0, 3, 3⟩]⟩def entry_181 : Entry := ⟨181, [⟨24, 3, 4, 5⟩, ⟨87, 2, 6, 4⟩, ⟨90, 0, 7, 5⟩]⟩def entry_182 : Entry := ⟨182, [⟨12, 2, 7, 3⟩, ⟨139, 0, 7, 4⟩]⟩def entry_183 : Entry := ⟨183, [⟨64, 2, 1, 5⟩, ⟨63, 3, 0, 3⟩, ⟨55, 2, 5, 4⟩]⟩def entry_184 : Entry := ⟨184, [⟨34, 3, 4, 2⟩, ⟨35, 2, 5, 4⟩]⟩def entry_185 : Entry := ⟨185, [⟨44, 3, 4, 5⟩, ⟨49, 0, 4, 5⟩, ⟨84, 0, 3, 4⟩]⟩def entry_186 : Entry := ⟨186, [⟨7, 6, 0, 3⟩, ⟨141, 2, 5, 4⟩]⟩def entry_187 : Entry := ⟨187, [⟨6, 4, 3, 4⟩, ⟨108, 3, 4, 5⟩]⟩def entry_188 : Entry := ⟨188, [⟨6, 3, 4, 5⟩, ⟨112, 5, 7, 4⟩]⟩def entry_189 : Entry := ⟨189, [⟨12, 0, 5, 4⟩, ⟨86, 4, 1, 4⟩]⟩def entry_190 : Entry := ⟨190, [⟨46, 0, 5, 4⟩, ⟨85, 2, 3, 3⟩, ⟨111, 3, 4, 3⟩]⟩def entry_191 : Entry := ⟨191, [⟨6, 4, 3, 4⟩, ⟨145, 0, 4, 5⟩]⟩def entry_192 : Entry := ⟨192, [⟨64, 1, 3, 1⟩, ⟨103, 0, 3, 4⟩, ⟨55, 3, 4, 5⟩]⟩def entry_193 : Entry := ⟨193, [⟨6, 6, 2, 3⟩, ⟨162, 1, 7, 4⟩]⟩def entry_194 : Entry := ⟨194, [⟨0, 0, 0, 3⟩, ⟨146, 4, 2, 5⟩]⟩def entry_195 : Entry := ⟨195, [⟨6, 6, 0, 3⟩, ⟨162, 1, 5, 4⟩]⟩def entry_196 : Entry := ⟨196, [⟨6, 3, 4, 5⟩, ⟨187, 5, 6, 4⟩]⟩def entry_197 : Entry := ⟨197, [⟨63, 3, 0, 3⟩, ⟨63, 1, 5, 3⟩]⟩def entry_198 : Entry := ⟨198, [⟨7, 4, 0, 5⟩, ⟨131, 1, 5, 4⟩]⟩def entry_199 : Entry := ⟨199, [⟨55, 1, 4, 5⟩, ⟨64, 3, 5, 1⟩, ⟨84, 0, 3, 4⟩]⟩def entry_200 : Entry := ⟨200, [⟨103, 0, 3, 4⟩, ⟨64, 3, 5, 1⟩, ⟨55, 1, 4, 5⟩]⟩def entry_201 : Entry := ⟨201, [⟨45, 3, 5, 7⟩, ⟨82, 0, 6, 5⟩]⟩def entry_202 : Entry := ⟨202, [⟨150, 0, 5, 4⟩, ⟨7, 0, 4, 5⟩, ⟨108, 0, 5, 4⟩]⟩def entry_203 : Entry := ⟨203, [⟨18, 6, 1, 3⟩, ⟨107, 0, 5, 4⟩, ⟨163, 0, 5, 4⟩]⟩def entry_204 : Entry := ⟨204, [⟨2, 5, 4, 2⟩, ⟨166, 2, 5, 3⟩]⟩def entry_205 : Entry := ⟨205, [⟨4, 1, 4, 3⟩, ⟨168, 0, 3, 4⟩]⟩def entry_206 : Entry := ⟨206, [⟨28, 3, 4, 5⟩, ⟨135, 2, 8, 4⟩]⟩def entry_207 : Entry := ⟨207, [⟨28, 3, 4, 5⟩, ⟨127, 0, 8, 4⟩]⟩def entry_208 : Entry := ⟨208, [⟨7, 4, 0, 5⟩, ⟨127, 0, 5, 4⟩]⟩def entry_209 : Entry := ⟨209, [⟨25, 0, 5, 4⟩, ⟨81, 5, 5, 7⟩]⟩def entry_210 : Entry := ⟨210, [⟨58, 2, 5, 4⟩, ⟨57, 0, 5, 4⟩, ⟨117, 1, 4, 5⟩]⟩def entry_211 : Entry := ⟨211, [⟨49, 5, 5, 4⟩, ⟨6, 6, 0, 3⟩]⟩def entry_212 : Entry := ⟨212, [⟨6, 0, 5, 4⟩, ⟨188, 0, 0, 5⟩]⟩def entry_213 : Entry := ⟨213, [⟨6, 0, 7, 5⟩, ⟨191, 0, 3, 5⟩]⟩def entry_214 : Entry := ⟨214, [⟨7, 3, 3, 4⟩, ⟨108, 3, 4, 5⟩, ⟨95, 0, 5, 2⟩]⟩def entry_215 : Entry := ⟨215, [⟨107, 1, 4, 6⟩, ⟨24, 0, 5, 4⟩]⟩def entry_216 : Entry := ⟨216, [⟨7, 6, 0, 3⟩, ⟨155, 5, 5, 4⟩]⟩def entry_217 : Entry := ⟨217, [⟨111, 1, 1, 3⟩, ⟨55, 4, 0, 4⟩, ⟨64, 0, 1, 3⟩]⟩def entry_218 : Entry := ⟨218, [⟨0, 5, 3, 7⟩, ⟨182, 0, 2, 4⟩]⟩def entry_219 : Entry := ⟨219, [⟨0, 5, 3, 7⟩, ⟨179, 2, 6, 4⟩]⟩def entry_220 : Entry := ⟨220, [⟨56, 4, 0, 4⟩, ⟨63, 1, 5, 3⟩, ⟨144, 2, 5, 4⟩, ⟨154, 6, 5, 4⟩, ⟨155, 1, 5, 4⟩]⟩def entry_221 : Entry := ⟨221, [⟨6, 6, 0, 3⟩, ⟨180, 5, 5, 4⟩]⟩def entry_222 : Entry := ⟨222, [⟨6, 1, 4, 5⟩, ⟨158, 5, 5, 4⟩]⟩def entry_223 : Entry := ⟨223, [⟨63, 1, 5, 3⟩, ⟨135, 2, 5, 4⟩, ⟨128, 0, 3, 3⟩, ⟨111, 3, 4, 3⟩, ⟨127, 0, 5, 4⟩]⟩def entry_224 : Entry := ⟨224, [⟨6, 1, 4, 5⟩, ⟨212, 0, 6, 3⟩]⟩def entry_225 : Entry := ⟨225, [⟨111, 7, 7, 5⟩, ⟨61, 4, 4, 5⟩]⟩def entry_226 : Entry := ⟨226, [⟨10, 6, 0, 3⟩, ⟨203, 0, 5, 4⟩, ⟨33, 0, 2, 3⟩, ⟨193, 0, 2, 4⟩]⟩def entry_227 : Entry := ⟨227, [⟨6, 1, 5, 5⟩, ⟨212, 0, 7, 3⟩]⟩def entry_228 : Entry := ⟨228, [⟨82, 0, 6, 5⟩, ⟨68, 3, 5, 7⟩]⟩def entry_229 : Entry := ⟨229, [⟨171, 0, 7, 3⟩, ⟨45, 1, 4, 5⟩, ⟨46, 3, 4, 5⟩]⟩def entry_230 : Entry := ⟨230, [⟨10, 6, 3, 4⟩, ⟨193, 0, 5, 5⟩, ⟨203, 0, 8, 5⟩, ⟨33, 0, 5, 4⟩]⟩def entry_231 : Entry := ⟨231, [⟨6, 3, 4, 5⟩, ⟨222, 0, 6, 4⟩]⟩def entry_232 : Entry := ⟨232, [⟨24, 2, 5, 4⟩, ⟨107, 1, 4, 6⟩]⟩def entry_233 : Entry := ⟨233, [⟨32, 3, 3, 1⟩, ⟨133, 0, 6, 4⟩]⟩def entry_234 : Entry := ⟨234, [⟨180, 4, 4, 5⟩, ⟨37, 0, 3, 4⟩, ⟨129, 0, 5, 3⟩, ⟨63, 0, 3, 5⟩]⟩def entry_235 : Entry := ⟨235, [⟨7, 3, 3, 4⟩, ⟨110, 0, 6, 4⟩, ⟨70, 0, 3, 5⟩]⟩def entry_236 : Entry := ⟨236, [⟨38, 1, 4, 5⟩, ⟨122, 7, 3, 4⟩, ⟨181, 0, 2, 3⟩, ⟨30, 1, 4, 3⟩]⟩def entry_237 : Entry := ⟨237, [⟨6, 3, 4, 5⟩, ⟨172, 0, 7, 4⟩]⟩def entry_238 : Entry := ⟨238, [⟨6, 3, 4, 5⟩, ⟨178, 5, 7, 4⟩]⟩def entry_239 : Entry := ⟨239, [⟨0, 4, 7, 3⟩, ⟨174, 4, 3, 5⟩]⟩def entry_240 : Entry := ⟨240, [⟨6, 1, 4, 5⟩, ⟨237, 0, 2, 4⟩]⟩def entry_241 : Entry := ⟨241, [⟨131, 1, 5, 4⟩, ⟨159, 1, 5, 4⟩, ⟨61, 0, 4, 5⟩]⟩def entry_242 : Entry := ⟨242, [⟨6, 1, 4, 5⟩, ⟨190, 0, 5, 4⟩]⟩def entry_243 : Entry := ⟨243, [⟨6, 0, 5, 4⟩, ⟨233, 0, 2, 5⟩]⟩def entry_244 : Entry := ⟨244, [⟨99, 4, 2, 5⟩, ⟨99, 0, 4, 5⟩, ⟨11, 7, 3, 3⟩, ⟨173, 2, 5, 4⟩]⟩def entry_245 : Entry := ⟨245, [⟨64, 0, 1, 3⟩, ⟨175, 4, 0, 4⟩, ⟨143, 6, 4, 5⟩, ⟨186, 6, 0, 4⟩]⟩def entry_246 : Entry := ⟨246, [⟨64, 6, 4, 5⟩, ⟨175, 2, 5, 4⟩, ⟨186, 0, 5, 4⟩, ⟨143, 0, 1, 3⟩]⟩def entry_247 : Entry := ⟨247, [⟨6, 4, 3, 4⟩, ⟨229, 0, 4, 5⟩]⟩def entry_248 : Entry := ⟨248, [⟨186, 0, 7, 4⟩, ⟨143, 0, 3, 3⟩, ⟨175, 2, 7, 4⟩, ⟨64, 6, 6, 5⟩]⟩def entry_249 : Entry := ⟨249, [⟨0, 7, 4, 5⟩, ⟨225, 1, 4, 1⟩]⟩def entry_250 : Entry := ⟨250, [⟨6, 1, 4, 5⟩, ⟨238, 0, 2, 4⟩]⟩def entry_251 : Entry := ⟨251, [⟨6, 2, 5, 4⟩, ⟨239, 4, 3, 6⟩]⟩def entry_252 : Entry := ⟨252, [⟨111, 3, 4, 3⟩, ⟨154, 6, 5, 4⟩, ⟨144, 2, 5, 4⟩, ⟨63, 1, 5, 3⟩, ⟨155, 1, 5, 4⟩]⟩def entry_253 : Entry := ⟨253, [⟨29, 3, 3, 0⟩, ⟨177, 1, 6, 2⟩]⟩def entry_254 : Entry := ⟨254, [⟨96, 7, 4, 5⟩, ⟨108, 0, 8, 5⟩]⟩def entry_255 : Entry := ⟨255, [⟨69, 0, 3, 3⟩, ⟨205, 0, 5, 5⟩, ⟨7, 3, 3, 4⟩]⟩def entry_256 : Entry := ⟨256, [⟨0, 5, 4, 5⟩, ⟨231, 0, 3, 4⟩]⟩def entry_257 : Entry := ⟨257, [⟨4, 1, 5, 4⟩, ⟨235, 0, 4, 5⟩]⟩def entry_258 : Entry := ⟨258, [⟨6, 4, 3, 4⟩, ⟨227, 0, 4, 5⟩]⟩def entry_259 : Entry := ⟨259, [⟨6, 4, 3, 4⟩, ⟨231, 1, 7, 2⟩]⟩def entry_260 : Entry := ⟨260, [⟨0, 5, 4, 6⟩, ⟨231, 0, 3, 5⟩]⟩def entry_261 : Entry := ⟨261, [⟨6, 3, 4, 5⟩, ⟨242, 0, 6, 4⟩]⟩def entry_262 : Entry := ⟨262, [⟨0, 7, 5, 7⟩, ⟨213, 0, 3, 4⟩]⟩def entry_263 : Entry := ⟨263, [⟨144, 6, 0, 4⟩, ⟨143, 0, 1, 3⟩, ⟨175, 0, 5, 4⟩, ⟨55, 6, 0, 4⟩]⟩def entry_264 : Entry := ⟨264, [⟨6, 4, 3, 4⟩, ⟨250, 1, 7, 4⟩]⟩def entry_265 : Entry := ⟨265, [⟨6, 6, 3, 4⟩, ⟨247, 0, 4, 6⟩]⟩def entry_266 : Entry := ⟨266, [⟨6, 3, 3, 5⟩, ⟨242, 0, 5, 4⟩]⟩def entry_267 : Entry := ⟨267, [⟨175, 4, 1, 4⟩, ⟨144, 2, 6, 4⟩, ⟨55, 2, 6, 4⟩, ⟨143, 4, 5, 3⟩]⟩def entry_268 : Entry := ⟨268, [⟨6, 0, 5, 4⟩, ⟨251, 0, 4, 2⟩]⟩def entry_269 : Entry := ⟨269, [⟨28, 3, 3, 6⟩, ⟨202, 0, 7, 5⟩]⟩def entry_270 : Entry := ⟨270, [⟨63, 0, 3, 7⟩, ⟨6, 7, 3, 2⟩]⟩def entry_271 : Entry := ⟨271, [⟨107, 2, 7, 3⟩, ⟨107, 3, 4, 6⟩]⟩def entry_272 : Entry := ⟨272, [⟨1, 1, 3, 1⟩, ⟨249, 0, 4, 5⟩]⟩def entry_273 : Entry := ⟨273, [⟨6, 1, 4, 5⟩, ⟨223, 0, 5, 4⟩]⟩def entry_274 : Entry := ⟨274, [⟨6, 7, 3, 1⟩, ⟨240, 0, 5, 5⟩]⟩def entry_275 : Entry := ⟨275, [⟨63, 1, 5, 3⟩, ⟨198, 4, 0, 4⟩, ⟨44, 2, 5, 4⟩]⟩def entry_276 : Entry := ⟨276, [⟨7, 3, 3, 4⟩, ⟨177, 0, 5, 4⟩, ⟨63, 0, 3, 5⟩]⟩def entry_277 : Entry := ⟨277, [⟨14, 3, 4, 5⟩, ⟨204, 2, 3, 0⟩, ⟨33, 1, 3, 2⟩]⟩def entry_278 : Entry := ⟨278, [⟨63, 3, 3, 3⟩, ⟨162, 1, 8, 4⟩]⟩def entry_279 : Entry := ⟨279, [⟨6, 3, 4, 5⟩, ⟨234, 5, 7, 4⟩]⟩def entry_280 : Entry := ⟨280, [⟨184, 0, 1, 5⟩, ⟨116, 2, 4, 3⟩]⟩def entry_281 : Entry := ⟨281, [⟨36, 4, 5, 4⟩, ⟨163, 2, 5, 4⟩, ⟨189, 0, 4, 5⟩]⟩def entry_282 : Entry := ⟨282, [⟨56, 0, 5, 4⟩, ⟨64, 0, 1, 3⟩, ⟨55, 0, 5, 4⟩, ⟨265, 0, 1, 3⟩]⟩def entry_283 : Entry := ⟨283, [⟨64, 0, 1, 3⟩, ⟨196, 1, 4, 3⟩, ⟨55, 2, 5, 4⟩]⟩def entry_284 : Entry := ⟨284, [⟨45, 1, 4, 5⟩, ⟨224, 0, 5, 4⟩, ⟨46, 3, 4, 5⟩]⟩def entry_285 : Entry := ⟨285, [⟨6, 3, 4, 5⟩, ⟨273, 0, 6, 4⟩]⟩def entry_286 : Entry := ⟨286, [⟨6, 7, 3, 0⟩, ⟨261, 0, 3, 4⟩]⟩def entry_287 : Entry := ⟨287, [⟨64, 0, 1, 3⟩, ⟨55, 0, 5, 4⟩, ⟨56, 0, 5, 4⟩, ⟨264, 4, 4, 5⟩]⟩def entry_288 : Entry := ⟨288, [⟨130, 1, 4, 2⟩, ⟨96, 0, 1, 4⟩]⟩def entry_289 : Entry := ⟨289, [⟨6, 1, 4, 5⟩, ⟨279, 0, 2, 4⟩]⟩def entry_290 : Entry := ⟨290, [⟨67, 2, 5, 2⟩, ⟨231, 4, 5, 5⟩]⟩def entry_291 : Entry := ⟨291, [⟨89, 3, 3, 4⟩, ⟨202, 0, 8, 4⟩, ⟨55, 4, 3, 4⟩]⟩def entry_292 : Entry := ⟨292, [⟨39, 0, 3, 4⟩, ⟨219, 3, 3, 4⟩, ⟨79, 1, 4, 3⟩]⟩def entry_293 : Entry := ⟨293, [⟨2, 7, 4, 3⟩, ⟨280, 0, 5, 4⟩]⟩def entry_294 : Entry := ⟨294, [⟨63, 1, 5, 3⟩, ⟨196, 3, 1, 3⟩]⟩def entry_295 : Entry := ⟨295, [⟨63, 1, 5, 3⟩, ⟨64, 2, 1, 5⟩, ⟨55, 0, 5, 4⟩, ⟨265, 4, 4, 3⟩]⟩def entry_296 : Entry := ⟨296, [⟨107, 1, 4, 5⟩, ⟨209, 3, 3, 4⟩, ⟨65, 1, 4, 5⟩]⟩def entry_297 : Entry := ⟨297, [⟨6, 4, 3, 4⟩, ⟨289, 1, 7, 4⟩]⟩def entry_298 : Entry := ⟨298, [⟨24, 2, 7, 3⟩, ⟨24, 6, 3, 3⟩, ⟨107, 4, 3, 4⟩, ⟨195, 0, 7, 4⟩]⟩def entry_299 : Entry := ⟨299, [⟨6, 4, 3, 4⟩, ⟨284, 0, 4, 5⟩]⟩def entry_300 : Entry := ⟨300, [⟨64, 3, 5, 1⟩, ⟨240, 2, 5, 1⟩, ⟨55, 3, 4, 5⟩]⟩def entry_301 : Entry := ⟨301, [⟨59, 0, 5, 4⟩, ⟨57, 0, 5, 4⟩, ⟨258, 4, 4, 5⟩]⟩def entry_302 : Entry := ⟨302, [⟨125, 0, 5, 3⟩, ⟨162, 4, 3, 6⟩]⟩def entry_303 : Entry := ⟨303, [⟨49, 4, 4, 5⟩, ⟨44, 1, 4, 5⟩, ⟨63, 0, 3, 5⟩, ⟨261, 0, 3, 4⟩]⟩def entry_304 : Entry := ⟨304, [⟨55, 4, 3, 4⟩, ⟨202, 0, 8, 4⟩, ⟨131, 3, 3, 4⟩]⟩def entry_305 : Entry := ⟨305, [⟨6, 1, 4, 5⟩, ⟨278, 0, 1, 4⟩]⟩def entry_306 : Entry := ⟨306, [⟨4, 1, 4, 3⟩, ⟨288, 0, 6, 4⟩]⟩def entry_307 : Entry := ⟨307, [⟨0, 7, 4, 6⟩, ⟨273, 0, 5, 5⟩]⟩def entry_308 : Entry := ⟨308, [⟨6, 6, 3, 4⟩, ⟨299, 0, 4, 6⟩]⟩def entry_309 : Entry := ⟨309, [⟨28, 6, 3, 4⟩, ⟨268, 1, 5, 7⟩]⟩def entry_310 : Entry := ⟨310, [⟨6, 1, 4, 5⟩, ⟨281, 0, 5, 3⟩]⟩def entry_311 : Entry := ⟨311, [⟨6, 3, 3, 5⟩, ⟨278, 0, 2, 4⟩]⟩def entry_312 : Entry := ⟨312, [⟨9, 2, 5, 4⟩, ⟨272, 0, 4, 5⟩]⟩def entry_313 : Entry := ⟨313, [⟨162, 4, 4, 5⟩, ⟨148, 5, 6, 3⟩]⟩def entry_314 : Entry := ⟨314, [⟨6, 3, 4, 5⟩, ⟨305, 0, 6, 4⟩]⟩def entry_315 : Entry := ⟨315, [⟨6, 0, 5, 4⟩, ⟨296, 0, 4, 5⟩]⟩def entry_316 : Entry := ⟨316, [⟨6, 6, 3, 4⟩, ⟨306, 0, 5, 8⟩]⟩def entry_317 : Entry := ⟨317, [⟨263, 2, 6, 4⟩, ⟨26, 3, 4, 3⟩, ⟨99, 0, 5, 5⟩]⟩def entry_318 : Entry := ⟨318, [⟨64, 3, 5, 1⟩, ⟨63, 0, 3, 5⟩, ⟨261, 0, 3, 4⟩, ⟨55, 1, 4, 5⟩]⟩def entry_319 : Entry := ⟨319, [⟨39, 2, 3, 4⟩, ⟨109, 4, 0, 5⟩, ⟨266, 1, 4, 5⟩, ⟨122, 4, 4, 5⟩]⟩def entry_320 : Entry := ⟨320, [⟨19, 1, 4, 3⟩, ⟨267, 2, 6, 4⟩, ⟨115, 7, 4, 3⟩]⟩def entry_321 : Entry := ⟨321, [⟨165, 1, 3, 4⟩, ⟨97, 0, 7, 5⟩, ⟨223, 3, 4, 7⟩]⟩def entry_322 : Entry := ⟨322, [⟨96, 0, 1, 4⟩, ⟨205, 1, 5, 2⟩]⟩def entry_323 : Entry := ⟨323, [⟨165, 6, 4, 5⟩, ⟨278, 0, 1, 4⟩, ⟨25, 1, 4, 5⟩]⟩def entry_324 : Entry := ⟨324, [⟨6, 3, 4, 5⟩, ⟨298, 0, 3, 4⟩]⟩def entry_325 : Entry := ⟨325, [⟨25, 0, 6, 5⟩, ⟨313, 1, 6, 4⟩, ⟨24, 2, 6, 3⟩]⟩def entry_326 : Entry := ⟨326, [⟨63, 1, 5, 3⟩, ⟨255, 7, 0, 4⟩]⟩def entry_327 : Entry := ⟨327, [⟨24, 2, 6, 3⟩, ⟨195, 4, 2, 4⟩, ⟨195, 0, 6, 4⟩, ⟨24, 6, 2, 3⟩]⟩def entry_328 : Entry := ⟨328, [⟨49, 0, 4, 5⟩, ⟨44, 3, 4, 5⟩, ⟨285, 0, 3, 4⟩]⟩def entry_329 : Entry := ⟨329, [⟨0, 7, 4, 6⟩, ⟨305, 0, 5, 5⟩]⟩def entry_330 : Entry := ⟨330, [⟨63, 1, 5, 3⟩, ⟨268, 0, 4, 5⟩, ⟨144, 0, 5, 4⟩, ⟨154, 4, 5, 4⟩, ⟨155, 5, 5, 4⟩]⟩def entry_331 : Entry := ⟨331, [⟨113, 0, 1, 4⟩, ⟨15, 0, 3, 4⟩, ⟨298, 4, 4, 5⟩, ⟨90, 2, 5, 4⟩]⟩def entry_332 : Entry := ⟨332, [⟨67, 4, 3, 4⟩, ⟨289, 2, 5, 1⟩]⟩def entry_333 : Entry := ⟨333, [⟨317, 0, 5, 4⟩, ⟨1, 5, 4, 3⟩]⟩def entry_334 : Entry := ⟨334, [⟨67, 6, 3, 2⟩, ⟨289, 0, 5, 5⟩]⟩def entry_335 : Entry := ⟨335, [⟨196, 3, 1, 3⟩, ⟨162, 1, 5, 4⟩]⟩def entry_336 : Entry := ⟨336, [⟨25, 6, 2, 3⟩, ⟨199, 3, 2, 4⟩, ⟨65, 0, 6, 4⟩, ⟨304, 0, 2, 4⟩]⟩def entry_337 : Entry := ⟨337, [⟨107, 3, 3, 7⟩, ⟨230, 2, 1, 5⟩]⟩def entry_338 : Entry := ⟨338, [⟨241, 0, 6, 4⟩, ⟨275, 4, 2, 4⟩, ⟨107, 4, 2, 4⟩]⟩def entry_339 : Entry := ⟨339, [⟨4, 1, 4, 3⟩, ⟨322, 0, 6, 4⟩]⟩def entry_340 : Entry := ⟨340, [⟨25, 3, 3, 6⟩, ⟨300, 4, 4, 6⟩, ⟨24, 3, 3, 6⟩]⟩def entry_341 : Entry := ⟨341, [⟨162, 5, 5, 4⟩, ⟨259, 4, 4, 5⟩, ⟨208, 2, 5, 4⟩, ⟨143, 0, 1, 3⟩]⟩def entry_342 : Entry := ⟨342, [⟨210, 0, 5, 2⟩, ⟨88, 1, 4, 3⟩, ⟨260, 4, 4, 3⟩, ⟨290, 0, 4, 3⟩]⟩def entry_343 : Entry := ⟨343, [⟨0, 5, 4, 5⟩, ⟨250, 0, 5, 4⟩]⟩def entry_344 : Entry := ⟨344, [⟨7, 1, 5, 4⟩, ⟨108, 3, 4, 5⟩, ⟨262, 4, 5, 2⟩]⟩def entry_345 : Entry := ⟨345, [⟨6, 0, 5, 5⟩, ⟨320, 4, 4, 7⟩]⟩def entry_346 : Entry := ⟨346, [⟨60, 1, 4, 3⟩, ⟨255, 0, 1, 4⟩, ⟨276, 0, 1, 4⟩]⟩def entry_347 : Entry := ⟨347, [⟨6, 6, 3, 4⟩, ⟨339, 0, 5, 8⟩]⟩def entry_348 : Entry := ⟨348, [⟨312, 1, 5, 5⟩, ⟨114, 4, 3, 4⟩, ⟨139, 3, 4, 5⟩]⟩def entry_349 : Entry := ⟨349, [⟨14, 1, 4, 5⟩, ⟨17, 1, 4, 5⟩, ⟨332, 0, 3, 4⟩]⟩def entry_350 : Entry := ⟨350, [⟨24, 4, 2, 5⟩, ⟨107, 2, 6, 4⟩, ⟨271, 4, 5, 5⟩, ⟨215, 0, 5, 5⟩]⟩def entry_351 : Entry := ⟨351, [⟨163, 0, 5, 4⟩, ⟨287, 4, 1, 4⟩, ⟨25, 4, 1, 5⟩]⟩def entry_352 : Entry := ⟨352, [⟨214, 0, 4, 5⟩, ⟨91, 0, 3, 4⟩, ⟨63, 0, 3, 5⟩, ⟨344, 0, 4, 5⟩, ⟨180, 4, 4, 5⟩]⟩def entry_353 : Entry := ⟨353, [⟨6, 4, 0, 5⟩, ⟨347, 0, 1, 3⟩]⟩def entry_354 : Entry := ⟨354, [⟨138, 2, 5, 4⟩, ⟨114, 5, 4, 3⟩, ⟨312, 0, 5, 5⟩, ⟨182, 2, 2, 4⟩]⟩def entry_355 : Entry := ⟨355, [⟨12, 2, 7, 3⟩, ⟨167, 0, 7, 4⟩, ⟨342, 0, 6, 6⟩]⟩def entry_356 : Entry := ⟨356, [⟨24, 2, 6, 3⟩, ⟨24, 6, 2, 3⟩, ⟨211, 4, 2, 4⟩, ⟨179, 0, 6, 4⟩]⟩def entry_357 : Entry := ⟨357, [⟨82, 6, 2, 3⟩, ⟨283, 0, 5, 6⟩]⟩def entry_358 : Entry := ⟨358, [⟨6, 0, 5, 4⟩, ⟨346, 0, 4, 6⟩]⟩def entry_359 : Entry := ⟨359, [⟨134, 0, 4, 6⟩, ⟨24, 7, 3, 2⟩, ⟨323, 0, 5, 5⟩]⟩def entry_360 : Entry := ⟨360, [⟨155, 4, 4, 5⟩, ⟨7, 3, 3, 4⟩, ⟨337, 0, 5, 2⟩, ⟨228, 4, 5, 2⟩]⟩def entry_361 : Entry := ⟨361, [⟨6, 4, 3, 4⟩, ⟨352, 0, 4, 5⟩]⟩def entry_362 : Entry := ⟨362, [⟨4, 0, 3, 4⟩, ⟨345, 0, 4, 3⟩]⟩def entry_363 : Entry := ⟨363, [⟨137, 1, 4, 2⟩, ⟨248, 0, 2, 4⟩]⟩def entry_364 : Entry := ⟨364, [⟨63, 0, 3, 5⟩, ⟨314, 2, 3, 1⟩]⟩def entry_365 : Entry := ⟨365, [⟨6, 1, 4, 5⟩, ⟨354, 0, 4, 3⟩]⟩def entry_366 : Entry := ⟨366, [⟨6, 3, 4, 5⟩, ⟨357, 0, 6, 2⟩]⟩def entry_367 : Entry := ⟨367, [⟨6, 2, 5, 4⟩, ⟨361, 4, 4, 6⟩]⟩def entry_368 : Entry := ⟨368, [⟨6, 1, 4, 5⟩, ⟨366, 0, 2, 4⟩]⟩def entry_369 : Entry := ⟨369, [⟨6, 0, 5, 4⟩, ⟨367, 4, 1, 2⟩]⟩def entry_370 : Entry := ⟨370, [⟨199, 3, 1, 4⟩, ⟨286, 1, 5, 4⟩, ⟨24, 6, 1, 3⟩, ⟨319, 0, 5, 3⟩]⟩def entry_371 : Entry := ⟨371, [⟨267, 6, 2, 4⟩, ⟨137, 1, 4, 2⟩]⟩def entry_372 : Entry := ⟨372, [⟨40, 1, 4, 3⟩, ⟨333, 0, 2, 4⟩, ⟨120, 1, 3, 3⟩, ⟨161, 0, 4, 2⟩]⟩def entry_373 : Entry := ⟨373, [⟨156, 2, 7, 4⟩, ⟨226, 4, 3, 5⟩, ⟨80, 0, 5, 4⟩, ⟨327, 0, 5, 5⟩, ⟨156, 6, 3, 4⟩]⟩def entry_374 : Entry := ⟨374, [⟨65, 4, 3, 4⟩, ⟨335, 0, 7, 4⟩, ⟨24, 2, 7, 3⟩, ⟨163, 4, 3, 4⟩]⟩def entry_375 : Entry := ⟨375, [⟨24, 3, 3, 6⟩, ⟨327, 6, 3, 3⟩]⟩def entry_376 : Entry := ⟨376, [⟨162, 1, 5, 4⟩, ⟨285, 3, 1, 3⟩]⟩def entry_377 : Entry := ⟨377, [⟨29, 3, 3, 0⟩, ⟨362, 0, 7, 2⟩]⟩def entry_378 : Entry := ⟨378, [⟨295, 0, 5, 4⟩, ⟨176, 4, 1, 4⟩, ⟨183, 4, 1, 4⟩, ⟨172, 6, 1, 4⟩, ⟨294, 4, 1, 4⟩]⟩def entry_379 : Entry := ⟨379, [⟨63, 0, 3, 5⟩, ⟨64, 1, 3, 1⟩, ⟨55, 3, 4, 5⟩, ⟨368, 0, 5, 4⟩]⟩def entry_380 : Entry := ⟨380, [⟨101, 4, 2, 5⟩, ⟨271, 0, 2, 5⟩, ⟨223, 0, 5, 4⟩, ⟨192, 3, 1, 4⟩]⟩def entry_381 : Entry := ⟨381, [⟨211, 6, 3, 4⟩, ⟨24, 0, 7, 5⟩, ⟨163, 4, 3, 4⟩, ⟨341, 0, 7, 4⟩]⟩def entry_382 : Entry := ⟨382, [⟨124, 1, 5, 3⟩, ⟨2, 7, 4, 3⟩]⟩def entry_383 : Entry := ⟨383, [⟨192, 3, 2, 4⟩, ⟨271, 0, 3, 5⟩, ⟨197, 0, 6, 4⟩, ⟨172, 0, 6, 4⟩, ⟨215, 4, 3, 5⟩]⟩def entry_384 : Entry := ⟨384, [⟨173, 2, 6, 4⟩, ⟨282, 4, 2, 4⟩, ⟨220, 2, 6, 4⟩, ⟨246, 2, 6, 4⟩, ⟨263, 2, 6, 4⟩, ⟨183, 6, 2, 4⟩, ⟨295, 0, 6, 4⟩]⟩def entry_385 : Entry := ⟨385, [⟨63, 1, 5, 3⟩, ⟨64, 2, 1, 5⟩, ⟨55, 0, 5, 4⟩, ⟨369, 4, 1, 5⟩]⟩def entry_386 : Entry := ⟨386, [⟨217, 4, 1, 4⟩, ⟨172, 0, 5, 4⟩, ⟨173, 4, 1, 4⟩, ⟨217, 0, 5, 4⟩, ⟨294, 0, 5, 4⟩, ⟨294, 4, 1, 4⟩]⟩def entry_387 : Entry := ⟨387, [⟨14, 1, 4, 6⟩, ⟨370, 0, 5, 4⟩]⟩def entry_388 : Entry := ⟨388, [⟨6, 3, 4, 5⟩, ⟨374, 0, 3, 4⟩]⟩def entry_389 : Entry := ⟨389, [⟨197, 5, 4, 1⟩, ⟨215, 7, 3, 2⟩, ⟨271, 3, 3, 2⟩, ⟨236, 0, 5, 5⟩, ⟨192, 6, 4, 1⟩]⟩def entry_390 : Entry := ⟨390, [⟨372, 2, 5, 0⟩, ⟨167, 5, 4, 1⟩, ⟨12, 7, 3, 1⟩]⟩def entry_391 : Entry := ⟨391, [⟨6, 5, 5, 1⟩, ⟨388, 0, 3, 5⟩]⟩def entry_392 : Entry := ⟨392, [⟨24, 7, 3, 1⟩, ⟨107, 1, 4, 5⟩, ⟨236, 0, 5, 5⟩, ⟨364, 2, 4, 1⟩]⟩def entry_393 : Entry := ⟨393, [⟨107, 3, 4, 5⟩, ⟨348, 0, 6, 3⟩, ⟨65, 3, 4, 5⟩, ⟨303, 0, 4, 5⟩]⟩def entry_394 : Entry := ⟨394, [⟨226, 4, 1, 4⟩, ⟨226, 0, 5, 4⟩, ⟨327, 4, 3, 4⟩, ⟨327, 6, 3, 3⟩, ⟨226, 6, 1, 3⟩, ⟨226, 2, 5, 3⟩]⟩def entry_395 : Entry := ⟨395, [⟨211, 4, 2, 4⟩, ⟨376, 0, 6, 4⟩, ⟨24, 2, 6, 3⟩, ⟨236, 3, 2, 5⟩]⟩def entry_396 : Entry := ⟨396, [⟨107, 3, 4, 5⟩, ⟨365, 1, 7, 3⟩, ⟨303, 0, 4, 5⟩, ⟨65, 3, 4, 5⟩]⟩def entry_397 : Entry := ⟨397, [⟨24, 3, 4, 5⟩, ⟨374, 0, 3, 4⟩, ⟨65, 5, 5, 1⟩]⟩def entry_398 : Entry := ⟨398, [⟨257, 0, 1, 3⟩, ⟨363, 0, 5, 4⟩, ⟨130, 1, 4, 2⟩, ⟨177, 1, 4, 2⟩]⟩def entry_399 : Entry := ⟨399, [⟨192, 6, 4, 1⟩, ⟨271, 3, 3, 2⟩, ⟨173, 1, 4, 5⟩, ⟨319, 1, 3, 5⟩, ⟨215, 7, 3, 2⟩]⟩def entry_400 : Entry := ⟨400, [⟨283, 4, 2, 4⟩, ⟨252, 4, 2, 4⟩, ⟨176, 4, 2, 4⟩, ⟨197, 0, 6, 4⟩, ⟨283, 0, 6, 4⟩, ⟨245, 4, 2, 4⟩]⟩def entry_401 : Entry := ⟨401, [⟨24, 7, 3, 2⟩, ⟨286, 0, 4, 6⟩, ⟨364, 2, 4, 2⟩, ⟨319, 1, 3, 6⟩]⟩def entry_402 : Entry := ⟨402, [⟨29, 3, 3, 0⟩, ⟨384, 0, 5, 4⟩]⟩def entry_403 : Entry := ⟨403, [⟨202, 1, 4, 5⟩, ⟨180, 0, 4, 5⟩, ⟨314, 4, 5, 4⟩, ⟨63, 0, 3, 5⟩, ⟨388, 0, 3, 4⟩]⟩def entry_404 : Entry := ⟨404, [⟨82, 6, 2, 3⟩, ⟨388, 4, 4, 6⟩]⟩def entry_405 : Entry := ⟨405, [⟨391, 0, 4, 3⟩, ⟨301, 0, 5, 2⟩, ⟨42, 1, 4, 3⟩]⟩def entry_406 : Entry := ⟨406, [⟨295, 1, 4, 5⟩, ⟨172, 7, 4, 1⟩, ⟨245, 3, 4, 5⟩, ⟨197, 5, 4, 1⟩, ⟨236, 0, 5, 5⟩, ⟨176, 3, 4, 5⟩, ⟨364, 2, 4, 1⟩]⟩def entry_407 : Entry := ⟨407, [⟨285, 0, 3, 7⟩, ⟨314, 6, 5, 4⟩]⟩def entry_408 : Entry := ⟨408, [⟨357, 0, 5, 2⟩, ⟨229, 7, 2, 4⟩, ⟨223, 4, 2, 4⟩, ⟨223, 0, 6, 4⟩]⟩def entry_409 : Entry := ⟨409, [⟨136, 6, 4, 3⟩, ⟨384, 0, 5, 4⟩, ⟨133, 4, 4, 3⟩, ⟨110, 3, 4, 3⟩]⟩def entry_410 : Entry := ⟨410, [⟨0, 4, 5, 4⟩, ⟨405, 0, 3, 7⟩]⟩def entry_411 : Entry := ⟨411, [⟨252, 0, 7, 4⟩, ⟨263, 0, 7, 4⟩, ⟨300, 3, 3, 4⟩, ⟨379, 1, 7, 4⟩, ⟨173, 0, 7, 4⟩, ⟨246, 0, 7, 4⟩]⟩def entry_412 : Entry := ⟨412, [⟨0, 0, 0, 3⟩, ⟨403, 4, 3, 6⟩]⟩def entry_413 : Entry := ⟨413, [⟨3, 7, 4, 3⟩, ⟨403, 0, 4, 7⟩]⟩def entry_414 : Entry := ⟨414, [⟨374, 0, 2, 5⟩, ⟨199, 2, 4, 2⟩, ⟨185, 2, 4, 2⟩]⟩def entry_415 : Entry := ⟨415, [⟨177, 1, 4, 2⟩, ⟨164, 1, 4, 2⟩, ⟨205, 1, 5, 2⟩, ⟨384, 0, 3, 4⟩, ⟨371, 0, 5, 4⟩]⟩def entry_416 : Entry := ⟨416, [⟨176, 2, 5, 4⟩, ⟨385, 4, 1, 4⟩, ⟨197, 4, 1, 4⟩, ⟨295, 0, 5, 4⟩, ⟨245, 2, 5, 4⟩, ⟨220, 2, 5, 4⟩]⟩def entry_417 : Entry := ⟨417, [⟨409, 0, 2, 4⟩, ⟨11, 1, 4, 2⟩, ⟨270, 4, 4, 2⟩]⟩def entry_418 : Entry := ⟨418, [⟨68, 4, 1, 3⟩, ⟨62, 6, 1, 3⟩, ⟨147, 6, 1, 3⟩, ⟨413, 0, 4, 2⟩]⟩def entry_419 : Entry := ⟨419, [⟨243, 0, 4, 2⟩, ⟨164, 1, 4, 2⟩, ⟨402, 0, 2, 4⟩, ⟨253, 0, 2, 4⟩, ⟨377, 0, 2, 4⟩]⟩def entry_420 : Entry := ⟨420, [⟨29, 3, 3, 0⟩, ⟨415, 0, 6, 4⟩]⟩def entry_421 : Entry := ⟨421, [⟨24, 6, 2, 3⟩, ⟨397, 1, 5, 3⟩, ⟨25, 6, 2, 3⟩, ⟨241, 4, 2, 4⟩]⟩def entry_422 : Entry := ⟨422, [⟨45, 1, 3, 7⟩, ⟨106, 6, 2, 3⟩, ⟨419, 1, 6, 6⟩]⟩def entry_423 : Entry := ⟨423, [⟨378, 4, 2, 4⟩, ⟨386, 0, 5, 4⟩, ⟨226, 3, 3, 5⟩, ⟨386, 4, 2, 4⟩, ⟨378, 0, 5, 4⟩]⟩def entry_424 : Entry := ⟨424, [⟨55, 1, 4, 5⟩, ⟨394, 0, 6, 4⟩, ⟨216, 3, 4, 5⟩]⟩def entry_425 : Entry := ⟨425, [⟨386, 0, 5, 4⟩, ⟨226, 1, 4, 5⟩, ⟨378, 4, 2, 4⟩, ⟨378, 0, 5, 4⟩, ⟨386, 4, 2, 4⟩]⟩def entry_426 : Entry := ⟨426, [⟨300, 6, 4, 1⟩, ⟨252, 1, 4, 5⟩, ⟨397, 0, 3, 4⟩, ⟨291, 1, 4, 1⟩, ⟨328, 0, 4, 5⟩, ⟨319, 1, 3, 5⟩]⟩def entry_427 : Entry := ⟨427, [⟨45, 1, 3, 7⟩, ⟨106, 6, 2, 3⟩, ⟨420, 1, 6, 4⟩]⟩def entry_428 : Entry := ⟨428, [⟨26, 3, 4, 3⟩, ⟨416, 0, 5, 4⟩, ⟨244, 0, 5, 4⟩, ⟨329, 0, 4, 3⟩]⟩def entry_429 : Entry := ⟨429, [⟨128, 0, 6, 3⟩, ⟨28, 3, 4, 5⟩]⟩def entry_430 : Entry := ⟨430, [⟨277, 7, 1, 3⟩, ⟨338, 4, 3, 4⟩, ⟨336, 1, 4, 3⟩, ⟨375, 2, 4, 3⟩, ⟨277, 6, 3, 1⟩]⟩def entry_431 : Entry := ⟨431, [⟨73, 4, 3, 3⟩, ⟨302, 1, 5, 2⟩, ⟨415, 0, 6, 4⟩, ⟨398, 0, 6, 4⟩]⟩def entry_432 : Entry := ⟨432, [⟨42, 3, 4, 3⟩, ⟨428, 0, 5, 4⟩, ⟨274, 0, 4, 3⟩]⟩def entry_433 : Entry := ⟨433, [⟨63, 0, 3, 5⟩, ⟨7, 3, 3, 4⟩, ⟨427, 0, 5, 2⟩, ⟨422, 0, 5, 2⟩]⟩def entry_434 : Entry := ⟨434, [⟨418, 0, 4, 5⟩, ⟨263, 2, 5, 4⟩, ⟨295, 0, 5, 4⟩, ⟨176, 2, 5, 4⟩, ⟨116, 0, 4, 3⟩]⟩def entry_435 : Entry := ⟨435, [⟨6, 4, 3, 4⟩, ⟨431, 0, 5, 6⟩]⟩def entry_436 : Entry := ⟨436, [⟨51, 1, 5, 4⟩, ⟨60, 3, 4, 3⟩, ⟨274, 4, 4, 3⟩, ⟨428, 0, 5, 4⟩]⟩def entry_437 : Entry := ⟨437, [⟨55, 7, 4, 0⟩, ⟨427, 0, 5, 2⟩, ⟨63, 0, 3, 5⟩, ⟨422, 0, 5, 2⟩]⟩def entry_438 : Entry := ⟨438, [⟨0, 0, 1, 3⟩, ⟨432, 0, 4, 6⟩]⟩def entry_439 : Entry := ⟨439, [⟨176, 2, 5, 4⟩, ⟨295, 0, 5, 4⟩, ⟨263, 2, 5, 4⟩, ⟨418, 0, 4, 5⟩, ⟨149, 0, 4, 3⟩]⟩def entry_440 : Entry := ⟨440, [⟨6, 6, 1, 3⟩, ⟨435, 0, 2, 5⟩]⟩def entry_441 : Entry := ⟨441, [⟨6, 6, 3, 4⟩, ⟨435, 0, 4, 6⟩]⟩def entry_442 : Entry := ⟨442, [⟨63, 0, 3, 5⟩, ⟨7, 1, 5, 4⟩, ⟨433, 0, 4, 5⟩, ⟨201, 0, 3, 2⟩]⟩def entry_443 : Entry := ⟨443, [⟨6, 0, 5, 4⟩, ⟨438, 0, 3, 4⟩]⟩def entry_444 : Entry := ⟨444, [⟨194, 0, 5, 3⟩, ⟨160, 3, 4, 1⟩, ⟨142, 7, 4, 1⟩, ⟨236, 0, 5, 5⟩, ⟨353, 4, 1, 2⟩, ⟨412, 0, 5, 3⟩]⟩def entry_445 : Entry := ⟨445, [⟨9, 4, 3, 4⟩, ⟨432, 0, 5, 7⟩]⟩def entry_446 : Entry := ⟨446, [⟨4, 6, 4, 3⟩, ⟨438, 0, 6, 5⟩]⟩def entry_447 : Entry := ⟨447, [⟨0, 0, 0, 3⟩, ⟨436, 4, 4, 6⟩]⟩def entry_448 : Entry := ⟨448, [⟨9, 4, 1, 3⟩, ⟨436, 0, 3, 6⟩]⟩def entry_449 : Entry := ⟨449, [⟨26, 3, 4, 3⟩, ⟨244, 0, 5, 4⟩, ⟨439, 0, 5, 4⟩, ⟨307, 0, 4, 3⟩]⟩def entry_450 : Entry := ⟨450, [⟨6, 1, 5, 5⟩, ⟨440, 0, 6, 4⟩]⟩def entry_451 : Entry := ⟨451, [⟨1, 5, 4, 3⟩, ⟨449, 0, 5, 4⟩]⟩def entry_452 : Entry := ⟨452, [⟨24, 1, 5, 7⟩, ⟨451, 0, 3, 8⟩, ⟨25, 3, 3, 7⟩]⟩def entry_453 : Entry := ⟨453, [⟨359, 0, 4, 3⟩, ⟨226, 7, 3, 1⟩, ⟨386, 4, 2, 4⟩, ⟨389, 1, 5, 4⟩, ⟨414, 4, 3, 3⟩]⟩def entry_454 : Entry := ⟨454, [⟨58, 0, 6, 3⟩, ⟨436, 0, 3, 6⟩]⟩def entry_455 : Entry := ⟨455, [⟨20, 2, 4, 5⟩, ⟨118, 3, 0, 5⟩, ⟨39, 2, 3, 4⟩]⟩def entry_456 : Entry := ⟨456, [⟨308, 4, 4, 3⟩, ⟨64, 2, 1, 5⟩, ⟨63, 1, 5, 3⟩, ⟨55, 0, 5, 4⟩]⟩def entry_457 : Entry := ⟨457, [⟨28, 7, 3, 2⟩, ⟨454, 0, 5, 4⟩]⟩def entry_458 : Entry := ⟨458, [⟨130, 1, 4, 2⟩, ⟨177, 1, 4, 2⟩, ⟨450, 0, 1, 4⟩]⟩def entry_459 : Entry := ⟨459, [⟨97, 2, 7, 3⟩, ⟨448, 0, 5, 4⟩, ⟨65, 2, 7, 3⟩]⟩def entry_460 : Entry := ⟨460, [⟨183, 6, 1, 4⟩, ⟨173, 2, 5, 4⟩, ⟨295, 0, 5, 4⟩, ⟨282, 4, 1, 4⟩, ⟨246, 2, 5, 4⟩, ⟨263, 2, 5, 4⟩, ⟨220, 2, 5, 4⟩]⟩def entry_461 : Entry := ⟨461, [⟨4, 1, 4, 3⟩, ⟨458, 0, 6, 4⟩]⟩def entry_462 : Entry := ⟨462, [⟨452, 0, 3, 2⟩, ⟨86, 0, 5, 4⟩, ⟨328, 1, 5, 4⟩]⟩def entry_463 : Entry := ⟨463, [⟨170, 0, 6, 3⟩, ⟨76, 1, 3, 2⟩, ⟨447, 0, 5, 4⟩]⟩def entry_464 : Entry := ⟨464, [⟨63, 0, 3, 5⟩, ⟨224, 0, 5, 4⟩, ⟨315, 0, 7, 3⟩, ⟨306, 0, 5, 5⟩, ⟨358, 0, 7, 3⟩, ⟨461, 0, 5, 5⟩]⟩def entry_465 : Entry := ⟨465, [⟨55, 3, 4, 5⟩, ⟨285, 0, 3, 4⟩, ⟨64, 1, 3, 1⟩]⟩def entry_466 : Entry := ⟨466, [⟨395, 4, 3, 4⟩, ⟨360, 4, 2, 6⟩, ⟨417, 1, 5, 4⟩, ⟨325, 4, 3, 4⟩, ⟨324, 4, 3, 5⟩]⟩def entry_467 : Entry := ⟨467, [⟨64, 7, 5, 7⟩, ⟨314, 6, 5, 4⟩, ⟨443, 1, 5, 7⟩]⟩def entry_468 : Entry := ⟨468, [⟨6, 6, 3, 4⟩, ⟨464, 0, 4, 7⟩]⟩def entry_469 : Entry := ⟨469, [⟨55, 5, 4, 3⟩, ⟨443, 1, 5, 7⟩, ⟨314, 6, 5, 4⟩]⟩def entry_470 : Entry := ⟨470, [⟨6, 4, 3, 4⟩, ⟨468, 0, 4, 2⟩]⟩def entry_471 : Entry := ⟨471, [⟨6, 5, 4, 3⟩, ⟨466, 0, 5, 6⟩]⟩def entry_472 : Entry := ⟨472, [⟨6, 5, 5, 0⟩, ⟨466, 0, 6, 3⟩]⟩def entry_473 : Entry := ⟨473, [⟨121, 5, 5, 4⟩, ⟨436, 0, 3, 7⟩, ⟨445, 4, 5, 4⟩]⟩def entry_474 : Entry := ⟨474, [⟨463, 0, 6, 5⟩, ⟨70, 0, 3, 5⟩, ⟨83, 1, 5, 3⟩]⟩def entry_475 : Entry := ⟨475, [⟨63, 1, 5, 3⟩, ⟨261, 1, 4, 3⟩, ⟨457, 0, 2, 5⟩, ⟨269, 2, 2, 5⟩]⟩def entry_476 : Entry := ⟨476, [⟨0, 0, 1, 3⟩, ⟨473, 0, 5, 3⟩]⟩def entry_477 : Entry := ⟨477, [⟨55, 1, 4, 5⟩, ⟨154, 7, 4, 5⟩, ⟨154, 3, 4, 0⟩, ⟨471, 2, 5, 4⟩]⟩def entry_478 : Entry := ⟨478, [⟨25, 3, 4, 5⟩, ⟨165, 2, 4, 5⟩, ⟨190, 0, 7, 4⟩]⟩def entry_479 : Entry := ⟨479, [⟨55, 0, 5, 4⟩, ⟨443, 0, 4, 5⟩, ⟨443, 4, 1, 5⟩]⟩def entry_480 : Entry := ⟨480, [⟨108, 1, 4, 5⟩, ⟨4, 1, 5, 4⟩]⟩def entry_481 : Entry := ⟨481, [⟨303, 1, 5, 4⟩, ⟨429, 2, 1, 4⟩, ⟨309, 1, 1, 4⟩, ⟨206, 2, 1, 4⟩, ⟨169, 2, 1, 4⟩, ⟨207, 2, 1, 4⟩]⟩def entry_482 : Entry := ⟨482, [⟨6, 1, 4, 5⟩, ⟨218, 2, 4, 3⟩]⟩def entry_483 : Entry := ⟨483, [⟨173, 1, 4, 5⟩, ⟨292, 7, 3, 1⟩, ⟨319, 1, 3, 5⟩, ⟨192, 6, 4, 1⟩, ⟨475, 1, 4, 5⟩]⟩def entry_484 : Entry := ⟨484, [⟨25, 4, 1, 5⟩, ⟨107, 2, 5, 4⟩, ⟨349, 3, 1, 5⟩, ⟨163, 2, 5, 4⟩]⟩def entry_485 : Entry := ⟨485, [⟨484, 0, 5, 4⟩, ⟨2, 3, 4, 3⟩]⟩def entry_486 : Entry := ⟨486, [⟨2, 5, 4, 2⟩, ⟨485, 0, 5, 3⟩]⟩def entry_487 : Entry := ⟨487, [⟨2, 3, 4, 3⟩, ⟨481, 0, 5, 4⟩]⟩def entry_488 : Entry := ⟨488, [⟨0, 6, 6, 4⟩, ⟨247, 0, 2, 5⟩]⟩def entry_489 : Entry := ⟨489, [⟨356, 1, 3, 3⟩, ⟨197, 4, 1, 4⟩, ⟨172, 6, 1, 4⟩]⟩def entry_490 : Entry := ⟨490, [⟨64, 1, 3, 1⟩, ⟨471, 0, 5, 1⟩, ⟨470, 1, 5, 1⟩, ⟨111, 0, 3, 1⟩]⟩def entry_491 : Entry := ⟨491, [⟨6, 3, 3, 5⟩, ⟨273, 0, 5, 4⟩]⟩def entry_492 : Entry := ⟨492, [⟨62, 4, 3, 4⟩, ⟨107, 4, 3, 4⟩, ⟨487, 0, 6, 6⟩]⟩def entry_493 : Entry := ⟨493, [⟨225, 0, 1, 4⟩, ⟨455, 0, 5, 3⟩, ⟨236, 1, 5, 5⟩, ⟨221, 0, 5, 4⟩]⟩def entry_494 : Entry := ⟨494, [⟨297, 4, 4, 5⟩, ⟨268, 4, 1, 5⟩, ⟨162, 5, 5, 4⟩]⟩def entry_495 : Entry := ⟨495, [⟨25, 6, 1, 3⟩, ⟨167, 4, 1, 4⟩, ⟨456, 4, 1, 4⟩]⟩def entry_496 : Entry := ⟨496, [⟨25, 0, 7, 5⟩, ⟨107, 6, 3, 4⟩, ⟨163, 6, 3, 4⟩, ⟨494, 0, 7, 4⟩]⟩def entry_497 : Entry := ⟨497, [⟨36, 2, 3, 4⟩, ⟨167, 0, 7, 4⟩, ⟨410, 0, 7, 3⟩]⟩def entry_498 : Entry := ⟨498, [⟨14, 1, 4, 6⟩, ⟨298, 2, 2, 4⟩]⟩def entry_499 : Entry := ⟨499, [⟨493, 0, 5, 4⟩, ⟨25, 1, 4, 5⟩, ⟨478, 0, 2, 4⟩]⟩def entry_500 : Entry := ⟨500, [⟨1, 5, 3, 6⟩, ⟨351, 0, 5, 4⟩]⟩def entry_501 : Entry := ⟨501, [⟨6, 4, 0, 5⟩, ⟨316, 0, 1, 3⟩]⟩def entry_502 : Entry := ⟨502, [⟨215, 6, 2, 3⟩, ⟨232, 0, 4, 3⟩, ⟨192, 7, 1, 4⟩, ⟨173, 0, 5, 4⟩, ⟨271, 2, 2, 3⟩]⟩def entry_503 : Entry := ⟨503, [⟨63, 0, 3, 5⟩, ⟨55, 7, 4, 0⟩, ⟨420, 1, 7, 2⟩, ⟨419, 1, 7, 4⟩]⟩def entry_504 : Entry := ⟨504, [⟨381, 0, 3, 4⟩, ⟨310, 4, 4, 5⟩, ⟨159, 0, 5, 6⟩, ⟨351, 4, 3, 4⟩, ⟨496, 0, 3, 4⟩]⟩def entry_505 : Entry := ⟨505, [⟨173, 1, 4, 5⟩, ⟨499, 0, 5, 4⟩, ⟨183, 1, 4, 5⟩, ⟨282, 1, 4, 5⟩]⟩def entry_506 : Entry := ⟨506, [⟨99, 0, 4, 5⟩, ⟨200, 7, 1, 4⟩, ⟨318, 5, 5, 4⟩, ⟨173, 0, 5, 4⟩]⟩def entry_507 : Entry := ⟨507, [⟨151, 0, 2, 4⟩, ⟨33, 3, 4, 3⟩, ⟨481, 0, 5, 4⟩]⟩def entry_508 : Entry := ⟨508, [⟨6, 0, 5, 4⟩, ⟨393, 0, 1, 5⟩]⟩def entry_509 : Entry := ⟨509, [⟨252, 0, 6, 4⟩, ⟨241, 4, 2, 4⟩, ⟨455, 0, 6, 3⟩, ⟨68, 2, 6, 4⟩]⟩def entry_510 : Entry := ⟨510, [⟨6, 4, 3, 4⟩, ⟨508, 0, 7, 4⟩]⟩def entry_511 : Entry := ⟨511, [⟨15, 1, 4, 5⟩, ⟨331, 0, 5, 3⟩, ⟨380, 4, 2, 4⟩]⟩def entry_512 : Entry := ⟨512, [⟨62, 0, 5, 4⟩, ⟨107, 0, 5, 4⟩, ⟨507, 0, 4, 6⟩]⟩def entry_513 : Entry := ⟨513, [⟨6, 4, 3, 4⟩, ⟨396, 0, 4, 5⟩]⟩def entry_514 : Entry := ⟨514, [⟨57, 0, 5, 4⟩, ⟨443, 4, 1, 5⟩, ⟨510, 0, 1, 5⟩]⟩def entry_515 : Entry := ⟨515, [⟨2, 6, 2, 4⟩, ⟨512, 1, 1, 5⟩]⟩def entry_516 : Entry := ⟨516, [⟨329, 0, 4, 3⟩, ⟨244, 4, 2, 4⟩, ⟨10, 1, 4, 5⟩, ⟨506, 4, 2, 4⟩]⟩def entry_517 : Entry := ⟨517, [⟨496, 0, 2, 3⟩, ⟨140, 0, 4, 2⟩, ⟨193, 1, 4, 2⟩]⟩def entry_518 : Entry := ⟨518, [⟨9, 6, 3, 4⟩, ⟨514, 0, 7, 4⟩]⟩def entry_519 : Entry := ⟨519, [⟨498, 0, 4, 3⟩, ⟨311, 4, 3, 4⟩, ⟨38, 1, 4, 5⟩, ⟨408, 0, 3, 4⟩]⟩def entry_520 : Entry := ⟨520, [⟨254, 0, 2, 3⟩, ⟨200, 5, 6, 4⟩, ⟨271, 6, 5, 3⟩, ⟨215, 2, 5, 3⟩, ⟨252, 4, 2, 4⟩]⟩def entry_521 : Entry := ⟨521, [⟨492, 4, 5, 1⟩, ⟨2, 7, 4, 2⟩]⟩def entry_522 : Entry := ⟨522, [⟨176, 3, 4, 6⟩, ⟨338, 2, 3, 3⟩, ⟨252, 1, 4, 6⟩]⟩def entry_523 : Entry := ⟨523, [⟨303, 1, 5, 4⟩, ⟨25, 4, 1, 5⟩, ⟨107, 2, 5, 4⟩, ⟨511, 4, 1, 6⟩]⟩def entry_524 : Entry := ⟨524, [⟨504, 4, 5, 3⟩, ⟨504, 0, 3, 3⟩, ⟨180, 0, 4, 5⟩, ⟨180, 4, 4, 5⟩, ⟨261, 0, 3, 4⟩]⟩def entry_525 : Entry := ⟨525, [⟨303, 1, 5, 4⟩, ⟨25, 4, 1, 5⟩, ⟨430, 0, 4, 6⟩, ⟨107, 2, 5, 4⟩]⟩def entry_526 : Entry := ⟨526, [⟨359, 0, 4, 3⟩, ⟨416, 4, 2, 4⟩, ⟨327, 5, 4, 3⟩, ⟨489, 0, 5, 4⟩, ⟨399, 3, 2, 4⟩]⟩def entry_527 : Entry := ⟨527, [⟨387, 4, 4, 3⟩, ⟨38, 3, 4, 5⟩, ⟨491, 0, 5, 4⟩, ⟨519, 0, 6, 4⟩]⟩def entry_528 : Entry := ⟨528, [⟨414, 1, 3, 5⟩, ⟨386, 1, 4, 6⟩, ⟨502, 5, 4, 3⟩, ⟨226, 4, 1, 5⟩, ⟨359, 5, 3, 4⟩]⟩def entry_529 : Entry := ⟨529, [⟨55, 4, 3, 4⟩, ⟨441, 0, 4, 3⟩, ⟨63, 3, 3, 3⟩, ⟨64, 6, 7, 5⟩]⟩def entry_530 : Entry := ⟨530, [⟨456, 7, 4, 2⟩, ⟨336, 0, 5, 5⟩, ⟨283, 7, 4, 2⟩, ⟨271, 5, 5, 5⟩]⟩def entry_531 : Entry := ⟨531, [⟨425, 0, 5, 4⟩, ⟨336, 3, 4, 3⟩, ⟨340, 6, 4, 3⟩, ⟨394, 1, 5, 4⟩, ⟨423, 0, 5, 4⟩, ⟨526, 0, 5, 4⟩, ⟨401, 4, 4, 3⟩, ⟨453, 0, 5, 4⟩]⟩def entry_532 : Entry := ⟨532, [⟨504, 4, 5, 3⟩, ⟨6, 7, 3, 0⟩]⟩def entry_533 : Entry := ⟨533, [⟨318, 4, 4, 5⟩, ⟨319, 7, 5, 1⟩, ⟨407, 4, 4, 1⟩, ⟨173, 3, 4, 5⟩, ⟨217, 1, 4, 5⟩]⟩def entry_534 : Entry := ⟨534, [⟨434, 0, 4, 6⟩, ⟨12, 6, 1, 3⟩]⟩def entry_535 : Entry := ⟨535, [⟨444, 0, 4, 5⟩, ⟨426, 0, 4, 5⟩, ⟨25, 0, 5, 4⟩, ⟨321, 4, 4, 2⟩]⟩def entry_536 : Entry := ⟨536, [⟨307, 0, 4, 3⟩, ⟨244, 0, 5, 4⟩, ⟨26, 3, 4, 3⟩, ⟨534, 0, 5, 2⟩]⟩def entry_537 : Entry := ⟨537, [⟨373, 2, 2, 4⟩, ⟨271, 3, 3, 3⟩, ⟨176, 1, 4, 6⟩, ⟨330, 1, 4, 6⟩]⟩def entry_538 : Entry := ⟨538, [⟨63, 3, 3, 3⟩, ⟨470, 0, 4, 5⟩, ⟨64, 6, 7, 5⟩, ⟨55, 4, 3, 4⟩]⟩def entry_539 : Entry := ⟨539, [⟨51, 1, 5, 4⟩, ⟨488, 3, 4, 3⟩, ⟨428, 0, 5, 4⟩, ⟨516, 0, 5, 4⟩]⟩def entry_540 : Entry := ⟨540, [⟨334, 0, 4, 3⟩, ⟨51, 1, 5, 4⟩, ⟨88, 3, 4, 3⟩, ⟨536, 0, 5, 4⟩]⟩def entry_541 : Entry := ⟨541, [⟨236, 0, 5, 5⟩, ⟨142, 7, 4, 1⟩, ⟨160, 3, 4, 1⟩, ⟨194, 0, 5, 3⟩, ⟨501, 4, 1, 2⟩, ⟨412, 0, 5, 3⟩]⟩def entry_542 : Entry := ⟨542, [⟨6, 5, 5, 0⟩, ⟨442, 0, 4, 5⟩]⟩def entry_543 : Entry := ⟨543, [⟨493, 3, 2, 6⟩, ⟨107, 2, 5, 4⟩, ⟨318, 5, 5, 4⟩]⟩def entry_544 : Entry := ⟨544, [⟨263, 2, 7, 4⟩, ⟨9, 6, 3, 4⟩, ⟨451, 1, 8, 3⟩]⟩def entry_545 : Entry := ⟨545, [⟨256, 0, 4, 5⟩, ⟨448, 0, 5, 4⟩, ⟨153, 0, 6, 3⟩, ⟨343, 0, 4, 5⟩]⟩def entry_546 : Entry := ⟨546, [⟨64, 0, 4, 3⟩, ⟨482, 7, 4, 3⟩, ⟨443, 0, 7, 5⟩, ⟨64, 6, 7, 5⟩]⟩def entry_547 : Entry := ⟨547, [⟨443, 0, 7, 5⟩, ⟨510, 4, 7, 5⟩, ⟨131, 3, 3, 4⟩]⟩def entry_548 : Entry := ⟨548, [⟨426, 0, 4, 5⟩, ⟨541, 0, 4, 5⟩, ⟨25, 0, 5, 4⟩, ⟨321, 4, 4, 2⟩]⟩def entry_549 : Entry := ⟨549, [⟨385, 0, 6, 4⟩, ⟨385, 4, 2, 4⟩, ⟨330, 0, 6, 4⟩, ⟨252, 6, 2, 4⟩, ⟨326, 0, 6, 4⟩, ⟨529, 0, 2, 4⟩]⟩def entry_550 : Entry := ⟨550, [⟨424, 0, 4, 6⟩, ⟨172, 7, 4, 2⟩, ⟨215, 1, 5, 5⟩, ⟨456, 7, 4, 2⟩]⟩def entry_551 : Entry := ⟨551, [⟨300, 6, 4, 3⟩, ⟨172, 7, 4, 3⟩, ⟨319, 3, 5, 7⟩, ⟨527, 4, 5, 7⟩, ⟨176, 5, 4, 3⟩]⟩def entry_552 : Entry := ⟨552, [⟨443, 4, 1, 5⟩, ⟨64, 2, 1, 5⟩, ⟨504, 1, 3, 3⟩, ⟨404, 5, 2, 3⟩]⟩def entry_553 : Entry := ⟨553, [⟨63, 0, 3, 5⟩, ⟨261, 4, 5, 4⟩, ⟨471, 0, 5, 1⟩, ⟨442, 0, 4, 5⟩, ⟨504, 0, 3, 3⟩, ⟨180, 0, 4, 5⟩]⟩def entry_554 : Entry := ⟨554, [⟨30, 6, 5, 4⟩, ⟨96, 7, 4, 5⟩, ⟨474, 0, 4, 5⟩]⟩def entry_555 : Entry := ⟨555, [⟨504, 5, 3, 5⟩, ⟨513, 0, 1, 5⟩, ⟨55, 0, 5, 4⟩, ⟨443, 4, 1, 5⟩, ⟨471, 1, 1, 5⟩]⟩def entry_556 : Entry := ⟨556, [⟨34, 1, 4, 2⟩, ⟨549, 0, 3, 4⟩]⟩def entry_557 : Entry := ⟨557, [⟨460, 0, 5, 4⟩, ⟨460, 4, 2, 4⟩, ⟨460, 2, 5, 4⟩, ⟨411, 4, 5, 4⟩, ⟨531, 0, 3, 6⟩, ⟨531, 4, 4, 6⟩, ⟨406, 5, 5, 4⟩]⟩def entry_558 : Entry := ⟨558, [⟨180, 5, 5, 4⟩, ⟨443, 4, 1, 5⟩, ⟨513, 0, 1, 5⟩, ⟨442, 1, 5, 4⟩]⟩def entry_559 : Entry := ⟨559, [⟨228, 4, 5, 2⟩, ⟨7, 3, 3, 4⟩, ⟨155, 4, 4, 5⟩, ⟨538, 5, 4, 5⟩]⟩def entry_560 : Entry := ⟨560, [⟨517, 5, 5, 4⟩, ⟨416, 5, 4, 3⟩, ⟨359, 5, 3, 4⟩, ⟨356, 6, 3, 4⟩, ⟨483, 0, 4, 6⟩]⟩def entry_561 : Entry := ⟨561, [⟨295, 0, 5, 4⟩, ⟨173, 2, 5, 4⟩, ⟨263, 6, 1, 4⟩, ⟨236, 1, 5, 5⟩, ⟨546, 4, 5, 4⟩, ⟨176, 2, 5, 4⟩, ⟨535, 0, 4, 5⟩]⟩def entry_562 : Entry := ⟨562, [⟨6, 7, 3, 0⟩, ⟨559, 0, 4, 5⟩]⟩def entry_563 : Entry := ⟨563, [⟨167, 0, 7, 4⟩, ⟨538, 0, 3, 4⟩, ⟨514, 0, 7, 4⟩, ⟨330, 4, 3, 4⟩, ⟨545, 0, 5, 5⟩]⟩def entry_564 : Entry := ⟨564, [⟨560, 0, 4, 3⟩, ⟨421, 0, 3, 4⟩, ⟨401, 1, 3, 4⟩, ⟨340, 3, 3, 4⟩, ⟨509, 0, 3, 4⟩, ⟨528, 0, 4, 3⟩, ⟨423, 5, 4, 3⟩, ⟨425, 5, 4, 3⟩, ⟨336, 0, 3, 4⟩]⟩def entry_565 : Entry := ⟨565, [⟨443, 4, 4, 5⟩, ⟨131, 3, 3, 4⟩, ⟨538, 0, 3, 4⟩, ⟨459, 0, 5, 5⟩, ⟨144, 4, 3, 4⟩]⟩def entry_566 : Entry := ⟨566, [⟨314, 0, 3, 4⟩, ⟨180, 0, 4, 5⟩, ⟨442, 0, 4, 5⟩, ⟨466, 0, 6, 3⟩, ⟨504, 0, 3, 3⟩]⟩def entry_567 : Entry := ⟨567, [⟨21, 1, 4, 3⟩, ⟨561, 0, 6, 4⟩, ⟨500, 4, 3, 1⟩]⟩def entry_568 : Entry := ⟨568, [⟨538, 4, 6, 4⟩, ⟨547, 0, 2, 4⟩, ⟨275, 0, 6, 4⟩, ⟨565, 0, 2, 4⟩, ⟨330, 0, 6, 4⟩]⟩def entry_569 : Entry := ⟨569, [⟨34, 3, 4, 2⟩, ⟨568, 4, 5, 4⟩]⟩def entry_570 : Entry := ⟨570, [⟨569, 0, 2, 5⟩, ⟨2, 7, 4, 3⟩]⟩def entry_571 : Entry := ⟨571, [⟨293, 0, 4, 3⟩, ⟨570, 0, 4, 3⟩, ⟨382, 0, 4, 3⟩, ⟨556, 4, 2, 4⟩]⟩def entry_572 : Entry := ⟨572, [⟨564, 1, 6, 6⟩, ⟨465, 3, 3, 4⟩, ⟨385, 4, 3, 4⟩, ⟨364, 7, 3, 4⟩, ⟨499, 1, 6, 5⟩]⟩def entry_573 : Entry := ⟨573, [⟨527, 2, 3, 1⟩, ⟨499, 4, 3, 4⟩, ⟨527, 6, 5, 1⟩, ⟨499, 0, 5, 4⟩, ⟨407, 4, 4, 1⟩, ⟨531, 7, 2, 4⟩, ⟨407, 0, 4, 1⟩]⟩def entry_574 : Entry := ⟨574, [⟨497, 0, 2, 4⟩, ⟨539, 4, 4, 6⟩, ⟨355, 0, 2, 4⟩, ⟨390, 3, 2, 4⟩, ⟨544, 0, 2, 4⟩, ⟨462, 1, 4, 5⟩, ⟨563, 4, 5, 4⟩, ⟨540, 4, 4, 6⟩, ⟨518, 0, 2, 4⟩, ⟨495, 4, 2, 4⟩]⟩def entry_575 : Entry := ⟨575, [⟨314, 4, 5, 4⟩, ⟨504, 4, 5, 3⟩, ⟨180, 4, 4, 5⟩, ⟨442, 4, 4, 5⟩, ⟨559, 0, 4, 5⟩]⟩def entry_576 : Entry := ⟨576, [⟨495, 0, 5, 4⟩, ⟨544, 4, 5, 4⟩, ⟨462, 3, 3, 5⟩, ⟨540, 0, 3, 6⟩, ⟨355, 4, 5, 4⟩, ⟨539, 0, 3, 6⟩, ⟨497, 4, 5, 4⟩, ⟨390, 1, 5, 4⟩, ⟨563, 0, 2, 4⟩, ⟨518, 4, 5, 4⟩]⟩def entry_577 : Entry := ⟨577, [⟨64, 7, 5, 4⟩, ⟨64, 1, 3, 1⟩, ⟨443, 1, 5, 4⟩, ⟨443, 7, 3, 1⟩]⟩def entry_578 : Entry := ⟨578, [⟨574, 4, 4, 5⟩, ⟨2, 1, 4, 3⟩]⟩def entry_579 : Entry := ⟨579, [⟨2, 1, 4, 3⟩, ⟨576, 4, 4, 5⟩]⟩def entry_580 : Entry := ⟨580, [⟨2, 7, 4, 2⟩, ⟨579, 0, 3, 3⟩]⟩def entry_581 : Entry := ⟨581, [⟨578, 4, 5, 3⟩, ⟨2, 5, 4, 2⟩]⟩def entry_582 : Entry := ⟨582, [⟨40, 3, 4, 3⟩, ⟨446, 5, 5, 3⟩, ⟨523, 0, 7, 0⟩, ⟨480, 4, 5, 3⟩, ⟨567, 4, 5, 4⟩]⟩def entry_583 : Entry := ⟨583, [⟨25, 5, 4, 3⟩, ⟨525, 0, 5, 4⟩, ⟨582, 0, 2, 8⟩, ⟨221, 3, 3, 7⟩]⟩def entry_584 : Entry := ⟨584, [⟨263, 1, 4, 5⟩, ⟨236, 4, 3, 5⟩, ⟨548, 3, 3, 4⟩, ⟨295, 3, 4, 5⟩, ⟨577, 0, 4, 5⟩, ⟨173, 1, 4, 5⟩]⟩def entry_585 : Entry := ⟨585, [⟨236, 2, 5, 1⟩, ⟨300, 4, 4, 5⟩, ⟨479, 1, 4, 5⟩, ⟨577, 0, 4, 5⟩, ⟨183, 3, 4, 5⟩, ⟨527, 6, 5, 1⟩]⟩def entry_586 : Entry := ⟨586, [⟨465, 4, 4, 5⟩, ⟨558, 1, 4, 5⟩, ⟨385, 1, 4, 5⟩, ⟨379, 4, 4, 5⟩, ⟨524, 0, 4, 5⟩, ⟨469, 2, 4, 5⟩, ⟨467, 2, 4, 5⟩, ⟨527, 4, 5, 5⟩, ⟨553, 0, 4, 5⟩, ⟨552, 1, 4, 5⟩, ⟨555, 1, 4, 5⟩, ⟨564, 0, 6, 4⟩, ⟨583, 0, 5, 2⟩]⟩def entry_587 : Entry := ⟨587, [⟨300, 2, 4, 1⟩, ⟨479, 1, 4, 5⟩, ⟨319, 3, 5, 5⟩, ⟨477, 6, 4, 1⟩, ⟨252, 3, 4, 5⟩, ⟨467, 2, 4, 5⟩]⟩def entry_588 : Entry := ⟨588, [⟨3, 1, 3, 3⟩, ⟨586, 0, 4, 5⟩]⟩def entry_589 : Entry := ⟨589, [⟨4, 1, 4, 3⟩, ⟨588, 0, 4, 5⟩]⟩def entry_590 : Entry := ⟨590, [⟨295, 7, 4, 3⟩, ⟨173, 7, 4, 3⟩, ⟨577, 0, 4, 7⟩, ⟨490, 0, 4, 7⟩, ⟨217, 5, 4, 3⟩]⟩def entry_591 : Entry := ⟨591, [⟨524, 0, 4, 5⟩, ⟨529, 1, 4, 1⟩, ⟨529, 3, 4, 1⟩, ⟨538, 1, 4, 1⟩, ⟨538, 3, 4, 1⟩, ⟨197, 5, 4, 1⟩]⟩def entry_592 : Entry := ⟨592, [⟨588, 0, 4, 5⟩, ⟨108, 7, 3, 0⟩]⟩def entry_593 : Entry := ⟨593, [⟨2, 7, 4, 2⟩, ⟨586, 0, 4, 5⟩]⟩def entry_594 : Entry := ⟨594, [⟨30, 1, 4, 3⟩, ⟨476, 1, 4, 3⟩, ⟨588, 0, 4, 5⟩]⟩def entry_595 : Entry := ⟨595, [⟨460, 4, 2, 4⟩, ⟨460, 2, 5, 4⟩, ⟨586, 1, 5, 4⟩, ⟨411, 4, 5, 4⟩, ⟨551, 1, 2, 4⟩, ⟨406, 5, 5, 4⟩, ⟨572, 0, 2, 4⟩]⟩def entry_596 : Entry := ⟨596, [⟨385, 5, 4, 2⟩, ⟨592, 0, 5, 6⟩, ⟨330, 1, 4, 6⟩, ⟨529, 5, 4, 6⟩, ⟨385, 1, 4, 6⟩, ⟨330, 5, 4, 2⟩]⟩def entry_597 : Entry := ⟨597, [⟨24, 6, 2, 3⟩, ⟨221, 0, 6, 4⟩, ⟨199, 3, 2, 4⟩, ⟨594, 1, 6, 5⟩]⟩def entry_598 : Entry := ⟨598, [⟨594, 0, 5, 6⟩, ⟨456, 5, 4, 2⟩, ⟨254, 1, 3, 2⟩, ⟨554, 1, 3, 2⟩, ⟨465, 0, 4, 6⟩]⟩def entry_599 : Entry := ⟨599, [⟨578, 4, 5, 3⟩, ⟨492, 0, 3, 1⟩, ⟨512, 4, 3, 1⟩, ⟨586, 4, 4, 5⟩, ⟨485, 0, 5, 3⟩, ⟨579, 4, 5, 3⟩]⟩def entry_600 : Entry := ⟨600, [⟨448, 0, 4, 5⟩, ⟨278, 2, 1, 4⟩, ⟨592, 5, 5, 3⟩, ⟨403, 5, 5, 4⟩, ⟨146, 5, 4, 3⟩]⟩def entry_601 : Entry := ⟨601, [⟨437, 6, 4, 1⟩, ⟨553, 0, 4, 5⟩, ⟨592, 0, 5, 5⟩, ⟨236, 4, 3, 5⟩, ⟨469, 4, 4, 1⟩]⟩def entry_602 : Entry := ⟨602, [⟨553, 0, 4, 7⟩, ⟨467, 4, 4, 3⟩, ⟨592, 0, 5, 7⟩, ⟨437, 6, 4, 3⟩, ⟨236, 4, 3, 7⟩]⟩def entry_603 : Entry := ⟨603, [⟨505, 1, 5, 4⟩, ⟨505, 5, 5, 4⟩, ⟨586, 5, 5, 4⟩, ⟨551, 7, 5, 4⟩, ⟨531, 6, 4, 2⟩, ⟨586, 1, 5, 4⟩, ⟨585, 1, 5, 4⟩, ⟨585, 5, 5, 4⟩, ⟨551, 3, 5, 4⟩, ⟨573, 1, 5, 4⟩, ⟨533, 5, 5, 4⟩, ⟨533, 1, 5, 4⟩]⟩def entry_604 : Entry := ⟨604, [⟨597, 0, 3, 4⟩, ⟨375, 2, 4, 3⟩, ⟨597, 1, 4, 3⟩, ⟨375, 3, 3, 4⟩, ⟨350, 3, 4, 3⟩, ⟨350, 2, 3, 4⟩]⟩def entry_605 : Entry := ⟨605, [⟨400, 5, 4, 3⟩, ⟨383, 6, 3, 4⟩, ⟨530, 4, 4, 3⟩, ⟨596, 1, 3, 4⟩, ⟨522, 2, 4, 3⟩, ⟨598, 0, 4, 3⟩, ⟨537, 3, 3, 4⟩, ⟨520, 1, 4, 3⟩, ⟨550, 4, 4, 3⟩]⟩def entry_606 : Entry := ⟨606, [⟨123, 1, 4, 3⟩, ⟨274, 0, 4, 3⟩, ⟨605, 0, 6, 4⟩, ⟨119, 1, 4, 3⟩]⟩def entry_607 : Entry := ⟨607, [⟨420, 3, 1, 2⟩, ⟨419, 3, 1, 4⟩, ⟨589, 0, 5, 5⟩, ⟨314, 0, 3, 4⟩, ⟨571, 1, 7, 3⟩]⟩def entry_608 : Entry := ⟨608, [⟨486, 4, 4, 5⟩, ⟨515, 1, 4, 5⟩, ⟨580, 0, 4, 5⟩, ⟨521, 0, 4, 5⟩, ⟨581, 4, 4, 5⟩, ⟨593, 0, 4, 5⟩, ⟨599, 4, 4, 5⟩, ⟨606, 1, 6, 2⟩]⟩def entry_609 : Entry := ⟨609, [⟨286, 4, 4, 5⟩, ⟨107, 3, 4, 5⟩, ⟨532, 4, 4, 5⟩, ⟨542, 0, 4, 5⟩, ⟨221, 3, 4, 5⟩, ⟨562, 4, 4, 5⟩, ⟨575, 4, 4, 5⟩, ⟨604, 1, 6, 4⟩]⟩def entry_610 : Entry := ⟨610, [⟨221, 2, 5, 4⟩, ⟨286, 5, 5, 4⟩, ⟨107, 2, 5, 4⟩, ⟨472, 1, 5, 4⟩, ⟨566, 1, 5, 4⟩, ⟨532, 5, 5, 4⟩, ⟨542, 1, 5, 4⟩, ⟨609, 0, 2, 6⟩]⟩def entry_611 : Entry := ⟨611, [⟨456, 2, 5, 4⟩, ⟨456, 4, 1, 4⟩, ⟨594, 7, 1, 3⟩, ⟨594, 1, 5, 5⟩]⟩def entry_612 : Entry := ⟨612, [⟨589, 1, 5, 5⟩, ⟨589, 7, 0, 3⟩]⟩def entry_613 : Entry := ⟨613, [⟨607, 5, 5, 4⟩, ⟨503, 3, 1, 4⟩, ⟨592, 7, 1, 3⟩, ⟨592, 5, 5, 3⟩, ⟨607, 7, 1, 4⟩, ⟨612, 4, 1, 4⟩, ⟨612, 0, 5, 4⟩]⟩def entry_614 : Entry := ⟨614, [⟨608, 1, 7, 5⟩, ⟨543, 3, 5, 6⟩, ⟨370, 6, 3, 4⟩, ⟨392, 7, 3, 4⟩, ⟨610, 3, 5, 6⟩, ⟨600, 0, 6, 4⟩, ⟨613, 0, 6, 4⟩]⟩def entry_615 : Entry := ⟨615, [⟨602, 7, 6, 4⟩, ⟨614, 1, 4, 3⟩, ⟨533, 5, 6, 4⟩, ⟨590, 7, 6, 4⟩, ⟨611, 6, 3, 4⟩, ⟨587, 3, 3, 4⟩, ⟨601, 5, 6, 4⟩, ⟨406, 1, 6, 4⟩, ⟨591, 3, 3, 4⟩, ⟨586, 3, 3, 4⟩, ⟨584, 5, 6, 4⟩, ⟨406, 3, 3, 4⟩]⟩def tableChunk_0 : Array Entry := #[entry_6, entry_7, entry_8, entry_9, entry_10, entry_11, entry_12, entry_13, entry_14, entry_15, entry_16, entry_17, entry_18, entry_19, entry_20, entry_21, entry_22, entry_23, entry_24, entry_25]def tableChunk_1 : Array Entry := #[entry_26, entry_27, entry_28, entry_29, entry_30, entry_31, entry_32, entry_33, entry_34, entry_35, entry_36, entry_37, entry_38, entry_39, entry_40, entry_41, entry_42, entry_43, entry_44, entry_45]def tableChunk_2 : Array Entry := #[entry_46, entry_47, entry_48, entry_49, entry_50, entry_51, entry_52, entry_53, entry_54, entry_55, entry_56, entry_57, entry_58, entry_59, entry_60, entry_61, entry_62, entry_63, entry_64, entry_65]def tableChunk_3 : Array Entry := #[entry_66, entry_67, entry_68, entry_69, entry_70, entry_71, entry_72, entry_73, entry_74, entry_75, entry_76, entry_77, entry_78, entry_79, entry_80, entry_81, entry_82, entry_83, entry_84, entry_85]def tableChunk_4 : Array Entry := #[entry_86, entry_87, entry_88, entry_89, entry_90, entry_91, entry_92, entry_93, entry_94, entry_95, entry_96, entry_97, entry_98, entry_99, entry_100, entry_101, entry_102, entry_103, entry_104, entry_105]def tableChunk_5 : Array Entry := #[entry_106, entry_107, entry_108, entry_109, entry_110, entry_111, entry_112, entry_113, entry_114, entry_115, entry_116, entry_117, entry_118, entry_119, entry_120, entry_121, entry_122, entry_123, entry_124, entry_125]def tableChunk_6 : Array Entry := #[entry_126, entry_127, entry_128, entry_129, entry_130, entry_131, entry_132, entry_133, entry_134, entry_135, entry_136, entry_137, entry_138, entry_139, entry_140, entry_141, entry_142, entry_143, entry_144, entry_145]def tableChunk_7 : Array Entry := #[entry_146, entry_147, entry_148, entry_149, entry_150, entry_151, entry_152, entry_153, entry_154, entry_155, entry_156, entry_157, entry_158, entry_159, entry_160, entry_161, entry_162, entry_163, entry_164, entry_165]def tableChunk_8 : Array Entry := #[entry_166, entry_167, entry_168, entry_169, entry_170, entry_171, entry_172, entry_173, entry_174, entry_175, entry_176, entry_177, entry_178, entry_179, entry_180, entry_181, entry_182, entry_183, entry_184, entry_185]def tableChunk_9 : Array Entry := #[entry_186, entry_187, entry_188, entry_189, entry_190, entry_191, entry_192, entry_193, entry_194, entry_195, entry_196, entry_197, entry_198, entry_199, entry_200, entry_201, entry_202, entry_203, entry_204, entry_205]def tableChunk_10 : Array Entry := #[entry_206, entry_207, entry_208, entry_209, entry_210, entry_211, entry_212, entry_213, entry_214, entry_215, entry_216, entry_217, entry_218, entry_219, entry_220, entry_221, entry_222, entry_223, entry_224, entry_225]def tableChunk_11 : Array Entry := #[entry_226, entry_227, entry_228, entry_229, entry_230, entry_231, entry_232, entry_233, entry_234, entry_235, entry_236, entry_237, entry_238, entry_239, entry_240, entry_241, entry_242, entry_243, entry_244, entry_245]def tableChunk_12 : Array Entry := #[entry_246, entry_247, entry_248, entry_249, entry_250, entry_251, entry_252, entry_253, entry_254, entry_255, entry_256, entry_257, entry_258, entry_259, entry_260, entry_261, entry_262, entry_263, entry_264, entry_265]def tableChunk_13 : Array Entry := #[entry_266, entry_267, entry_268, entry_269, entry_270, entry_271, entry_272, entry_273, entry_274, entry_275, entry_276, entry_277, entry_278, entry_279, entry_280, entry_281, entry_282, entry_283, entry_284, entry_285]def tableChunk_14 : Array Entry := #[entry_286, entry_287, entry_288, entry_289, entry_290, entry_291, entry_292, entry_293, entry_294, entry_295, entry_296, entry_297, entry_298, entry_299, entry_300, entry_301, entry_302, entry_303, entry_304, entry_305]def tableChunk_15 : Array Entry := #[entry_306, entry_307, entry_308, entry_309, entry_310, entry_311, entry_312, entry_313, entry_314, entry_315, entry_316, entry_317, entry_318, entry_319, entry_320, entry_321, entry_322, entry_323, entry_324, entry_325]def tableChunk_16 : Array Entry := #[entry_326, entry_327, entry_328, entry_329, entry_330, entry_331, entry_332, entry_333, entry_334, entry_335, entry_336, entry_337, entry_338, entry_339, entry_340, entry_341, entry_342, entry_343, entry_344, entry_345]def tableChunk_17 : Array Entry := #[entry_346, entry_347, entry_348, entry_349, entry_350, entry_351, entry_352, entry_353, entry_354, entry_355, entry_356, entry_357, entry_358, entry_359, entry_360, entry_361, entry_362, entry_363, entry_364, entry_365]def tableChunk_18 : Array Entry := #[entry_366, entry_367, entry_368, entry_369, entry_370, entry_371, entry_372, entry_373, entry_374, entry_375, entry_376, entry_377, entry_378, entry_379, entry_380, entry_381, entry_382, entry_383, entry_384, entry_385]def tableChunk_19 : Array Entry := #[entry_386, entry_387, entry_388, entry_389, entry_390, entry_391, entry_392, entry_393, entry_394, entry_395, entry_396, entry_397, entry_398, entry_399, entry_400, entry_401, entry_402, entry_403, entry_404, entry_405]def tableChunk_20 : Array Entry := #[entry_406, entry_407, entry_408, entry_409, entry_410, entry_411, entry_412, entry_413, entry_414, entry_415, entry_416, entry_417, entry_418, entry_419, entry_420, entry_421, entry_422, entry_423, entry_424, entry_425]def tableChunk_21 : Array Entry := #[entry_426, entry_427, entry_428, entry_429, entry_430, entry_431, entry_432, entry_433, entry_434, entry_435, entry_436, entry_437, entry_438, entry_439, entry_440, entry_441, entry_442, entry_443, entry_444, entry_445]def tableChunk_22 : Array Entry := #[entry_446, entry_447, entry_448, entry_449, entry_450, entry_451, entry_452, entry_453, entry_454, entry_455, entry_456, entry_457, entry_458, entry_459, entry_460, entry_461, entry_462, entry_463, entry_464, entry_465]def tableChunk_23 : Array Entry := #[entry_466, entry_467, entry_468, entry_469, entry_470, entry_471, entry_472, entry_473, entry_474, entry_475, entry_476, entry_477, entry_478, entry_479, entry_480, entry_481, entry_482, entry_483, entry_484, entry_485]def tableChunk_24 : Array Entry := #[entry_486, entry_487, entry_488, entry_489, entry_490, entry_491, entry_492, entry_493, entry_494, entry_495, entry_496, entry_497, entry_498, entry_499, entry_500, entry_501, entry_502, entry_503, entry_504, entry_505]def tableChunk_25 : Array Entry := #[entry_506, entry_507, entry_508, entry_509, entry_510, entry_511, entry_512, entry_513, entry_514, entry_515, entry_516, entry_517, entry_518, entry_519, entry_520, entry_521, entry_522, entry_523, entry_524, entry_525]def tableChunk_26 : Array Entry := #[entry_526, entry_527, entry_528, entry_529, entry_530, entry_531, entry_532, entry_533, entry_534, entry_535, entry_536, entry_537, entry_538, entry_539, entry_540, entry_541, entry_542, entry_543, entry_544, entry_545]def tableChunk_27 : Array Entry := #[entry_546, entry_547, entry_548, entry_549, entry_550, entry_551, entry_552, entry_553, entry_554, entry_555, entry_556, entry_557, entry_558, entry_559, entry_560, entry_561, entry_562, entry_563, entry_564, entry_565]def tableChunk_28 : Array Entry := #[entry_566, entry_567, entry_568, entry_569, entry_570, entry_571, entry_572, entry_573, entry_574, entry_575, entry_576, entry_577, entry_578, entry_579, entry_580, entry_581, entry_582, entry_583, entry_584, entry_585]def tableChunk_29 : Array Entry := #[entry_586, entry_587, entry_588, entry_589, entry_590, entry_591, entry_592, entry_593, entry_594, entry_595, entry_596, entry_597, entry_598, entry_599, entry_600, entry_601, entry_602, entry_603, entry_604, entry_605]def tableChunk_30 : Array Entry := #[entry_606, entry_607, entry_608, entry_609, entry_610, entry_611, entry_612, entry_613, entry_614, entry_615]def table : Array Entry := ((((tableChunk_0 ++ (tableChunk_1 ++ tableChunk_2)) ++ ((tableChunk_3 ++ tableChunk_4) ++ (tableChunk_5 ++ tableChunk_6))) ++ (((tableChunk_7 ++ tableChunk_8) ++ (tableChunk_9 ++ tableChunk_10)) ++ ((tableChunk_11 ++ tableChunk_12) ++ (tableChunk_13 ++ tableChunk_14)))) ++ ((((tableChunk_15 ++ tableChunk_16) ++ (tableChunk_17 ++ tableChunk_18)) ++ ((tableChunk_19 ++ tableChunk_20) ++ (tableChunk_21 ++ tableChunk_22))) ++ (((tableChunk_23 ++ tableChunk_24) ++ (tableChunk_25 ++ tableChunk_26)) ++ ((tableChunk_27 ++ tableChunk_28) ++ (tableChunk_29 ++ tableChunk_30)))))def entryAt (i : ℕ) : Entry := table[i - 6]?.getD emptyEntrydef TableValid : Prop :=  table.size = 610 ∧ ∀ k, k < table.size →    let e := table[k]?.getD emptyEntry    e.index = k + 6 ∧ e.terms ≠ [] ∧ ∀ t ∈ e.terms, t.child < e.indexdef placementCount : ℕ := (table.toList.map fun e => e.terms.length).sumstructure RowData where  A : Finset Cell  H : Finset Cell  height : ℕ  deriving DecidableEqdef emptyRow : RowData := ⟨∅, ∅, 0⟩def baseRow (i : Fin 6) : RowData := ⟨baseRequired i, baseEnvelope i, 1⟩def placeRow (t : Term) (d : RowData) : RowData :=  ⟨d.A.image (placement t.rotation t.shift),   d.H.image (placement t.rotation t.shift), d.height⟩def unionA (ds : List RowData) : Finset Cell := (ds.map RowData.A).foldr (· ∪ ·) ∅def unionH (ds : List RowData) : Finset Cell := (ds.map RowData.H).foldr (· ∪ ·) ∅def commonH (ds : List RowData) : Finset Cell :=  match ds with  | [] => ∅  | d :: rest => (rest.map RowData.H).foldr (· ∩ ·) d.Hdef forkRow (ds : List RowData) : RowData :=  ⟨(unionA ds ∪ commonH ds).erase origin,   insert origin (unionH ds), 1 + (ds.map RowData.height).foldr max 0⟩def rowAt (i : ℕ) : RowData :=  if h : i < 6 then baseRow ⟨i, h⟩ else    forkRow ((entryAt i).terms.map fun t =>      placeRow t (if _ : t.child < i then rowAt t.child else emptyRow))termination_by idef Output (i : ℕ) (p : Cell) (size height : ℕ) (omitted : Set Cell) : Prop :=  (rowAt i).A = {p} ∧ (rowAt i).H.card = size ∧ (rowAt i).height = height ∧  Disjoint (↑(rowAt i).H : Set Cell) omitteddef AllRows : Prop := ∀ i, i < 616 →  (rowAt i).A ⊆ (rowAt i).H ∧ origin ∈ (rowAt i).H ∧  origin ∉ (rowAt i).A ∧ (rowAt i).height ≤ 34theorem certificate_correct :    TableValid ∧ placementCount = 1837 ∧    Output 557 (-1, 0) 118 19 {p | p.1 ≤ -3 ∧ p.2 ≤ -2} ∧    Output 595 (-1, 0) 222 27 {p | p.1 = -2 ∧ p.2 ≤ -2} ∧    Output 603 (-1, 0) 275 27 {p | p.1 ≤ -3 ∧ p.2 = 0} ∧    Output 615 (1, 0) 686 34 {(1, -1)} ∧    AllRows := by  sorryend SnakyCertificateend OAI