(declare-const H0 String)
(declare-const H1 String)
(declare-const H2 String)
(declare-const H3 String)
(declare-const H4 String)

(declare-const V0 String)
(declare-const V1 String)
(declare-const V2 String)
(declare-const V3 String)
(declare-const V4 String)

(assert (str.in.re H0
   (re.++ (re.union (str.to.re "I") (str.to.re "T"))
          (re.* (str.to.re "O"))
          (re.* (re.union (str.to.re "BE") (str.to.re "AD")))
          (re.* (str.to.re "O"))
   )
   ))
   
(assert (str.in.re H1
   (re.++ (re.+ (re.union (str.to.re "N") (str.to.re "O") (str.to.re "R") (str.to.re "M") (str.to.re "A") (str.to.re "L") ))
          (re.+ (str.to.re "T"))
   )
   ))
   
(assert (str.in.re H2
   (re.++ (re.* re.allchar)
          (re.union (str.to.re "XA") (str.to.re "BE"))
          (re.* re.allchar)
   )
   ))

   
(assert (str.in.re H3
   (re.++ (re.+ (re.union (str.to.re "EG") (str.to.re "UL")))
          (re.* (re.union (str.to.re "A") (str.to.re "L") (str.to.re "F")))
   )
   ))

(assert (str.in.re H4
   (re.++ (re.* (re.union (str.to.re "R") (str.to.re "E") (str.to.re "Q")))
          (re.union (str.to.re "G") (str.to.re "P"))
          (re.* re.allchar)
   )
   ))

(assert (str.in.re V0
   (re.++ (re.+ (re.union (str.to.re "R") (str.to.re "U") (str.to.re "T") (str.to.re "H")))
          (re.union (str.to.re "OE") (str.to.re "EO"))
          (re.* (re.union (str.to.re "R") (str.to.re "B")))
          )
          ))

(assert (str.in.re V1
   (re.++ (re.+ (re.union (str.to.re "BG") (str.to.re "ON") (str.to.re "KK")))
          (re.+ (re.union (str.to.re "R") (str.to.re "I") (str.to.re "F")))
          )
          ))

(assert (str.in.re V2
   (re.++ (re.union (str.to.re "MN") (str.to.re "BO") (str.to.re "FI"))
          (re.+ (re.union (str.to.re "E") (str.to.re "U")))
          )
          ))
          
(assert (str.in.re V3
   (re.++ (re.+ (re.union (str.to.re "KT") (str.to.re "AL") (str.to.re "ET")))
          (str.to.re "G")
          )
          ))
          
(assert (str.in.re V4
   (re.++ (re.union (str.to.re "O") (str.to.re "H"))
          (re.+ (re.union (str.to.re "PR") (str.to.re "AX") (str.to.re "TR")))
          )
          ))

(assert (str.in.re V4
   (re.++ re.allchar re.allchar re.allchar re.allchar re.allchar)))
   
(assert (= (str.at H0 0) (str.at V0 0) ))
(assert (= (str.at H1 0) (str.at V0 1) ))
(assert (= (str.at H2 0) (str.at V0 2) ))
(assert (= (str.at H3 0) (str.at V0 3) ))
(assert (= (str.at H4 0) (str.at V0 4) ))

(assert (= (str.at H0 1) (str.at V1 0) ))
(assert (= (str.at H1 1) (str.at V1 1) ))
(assert (= (str.at H2 1) (str.at V1 2) ))
(assert (= (str.at H3 1) (str.at V1 3) ))
(assert (= (str.at H4 1) (str.at V1 4) ))

(assert (= (str.at H0 2) (str.at V2 0) ))
(assert (= (str.at H1 2) (str.at V2 1) ))
(assert (= (str.at H2 2) (str.at V2 2) ))
(assert (= (str.at H3 2) (str.at V2 3) ))
(assert (= (str.at H4 2) (str.at V2 4) ))

(assert (= (str.at H0 3) (str.at V3 0) ))
(assert (= (str.at H1 3) (str.at V3 1) ))
(assert (= (str.at H2 3) (str.at V3 2) ))
(assert (= (str.at H3 3) (str.at V3 3) ))
(assert (= (str.at H4 3) (str.at V3 4) ))

(assert (= (str.at H0 4) (str.at V4 0) ))
(assert (= (str.at H1 4) (str.at V4 1) ))
(assert (= (str.at H2 4) (str.at V4 2) ))
(assert (= (str.at H3 4) (str.at V4 3) ))
(assert (= (str.at H4 4) (str.at V4 4) ))
(check-sat)
(get-model)