(set-option :auto-config false)
(set-option :model true)
(set-option :model.partial false)

(set-option :smt.mbqi false)
(define-sort Str () Int)
(declare-fun strLen (Str) Int)
(declare-fun subString (Str Int Int) Str)
(declare-fun concatString (Str Str) Str)
(define-sort Elt () Int)
(define-sort Set () (Array Elt Bool))
(define-fun smt_set_emp () Set ((as const Set) false))
(define-fun smt_set_mem ((x Elt) (s Set)) Bool (select s x))
(define-fun smt_set_add ((s Set) (x Elt)) Set (store s x true))
(define-fun smt_set_cup ((s1 Set) (s2 Set)) Set ((_ map or) s1 s2))
(define-fun smt_set_cap ((s1 Set) (s2 Set)) Set ((_ map and) s1 s2))
(define-fun smt_set_com ((s Set)) Set ((_ map not) s))
(define-fun smt_set_dif ((s1 Set) (s2 Set)) Set (smt_set_cap s1 (smt_set_com s2)))
(define-fun smt_set_sub ((s1 Set) (s2 Set)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
(define-sort Map () (Array Elt Elt))
(define-fun smt_map_sel ((m Map) (k Elt)) Elt (select m k))
(define-fun smt_map_sto ((m Map) (k Elt) (v Elt)) Map (store m k v))
(define-fun smt_map_cup ((m1 Map) (m2 Map)) Map ((_ map (+ (Elt Elt) Elt)) m1 m2))
(define-fun smt_map_def ((v Elt)) Map ((as const (Map)) v))
(define-fun bool_to_int ((b Bool)) Int (ite b 1 0))
(define-fun Z3_OP_MUL ((x Int) (y Int)) Int (* x y))
(define-fun Z3_OP_DIV ((x Int) (y Int)) Int (div x y))
(declare-fun lq_karg$36$VV$35$$35$852$35$$35$k_$35$$35$853 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$1062 () Int)
(declare-fun runFun () Int)
(declare-fun VV$35$$35$F$35$$35$28 () Int)
(declare-fun cast_as_int () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$983 () Int)
(declare-fun x$35$$35$aTy () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c () Int)
(declare-fun VV$35$$35$F$35$$35$31 () Int)
(declare-fun lq_karg$36$VV$35$$35$982$35$$35$k_$35$$35$983 () Int)
(declare-fun lq_tmp$36$x$35$$35$685 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$44$$44$$44$$41$$35$$35$7 () Int)
(declare-fun addrLen () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k$35$$35$k_$35$$35$983 () Int)
(declare-fun lq_tmp$36$x$35$$35$784 () Int)
(declare-fun lq_tmp$36$x$35$$35$586 () Int)
(declare-fun papp5 () Int)
(declare-fun x_Tuple21 () Int)
(declare-fun lq_tmp$36$x$35$$35$1057 () Int)
(declare-fun lq_tmp$36$x$35$$35$821 () Int)
(declare-fun lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$853 () Int)
(declare-fun x_Tuple65 () Int)
(declare-fun lq_tmp$36$x$35$$35$1089 () Int)
(declare-fun lq_tmp$36$x$35$$35$743 () Int)
(declare-fun x_Tuple55 () Int)
(declare-fun is$36$GHC.Types.$91$$93$ () Int)
(declare-fun x_Tuple33 () Int)
(declare-fun is$36$GHC.Tuple.$40$$44$$44$$44$$44$$44$$41$ () Int)
(declare-fun is$36$GHC.Tuple.$40$$44$$44$$44$$41$ () Int)
(declare-fun is$36$GHC.Tuple.$40$$44$$41$ () Int)
(declare-fun GHC.Types.LT () Int)
(declare-fun x_Tuple77 () Int)
(declare-fun lq_tmp$36$x$35$$35$459 () Int)
(declare-fun x$35$$35$aTB () Int)
(declare-fun ys$35$$35$aTx () Int)
(declare-fun lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$1062 () Int)
(declare-fun VV$35$$35$1161 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$1062 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d () Int)
(declare-fun papp3 () Int)
(declare-fun x_Tuple63 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$41$$35$$35$1 () Int)
(declare-fun x_Tuple41 () Int)
(declare-fun Reverse.length () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l$35$$35$k_$35$$35$983 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$983 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$44$$41$$35$$35$1 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$44$$44$$44$$41$$35$$35$1 () Int)
(declare-fun lq_tmp$36$x$35$$35$1029 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$44$$44$$44$$41$$35$$35$6 () Int)
(declare-fun GHC.Types.$58$ () Int)
(declare-fun lq_tmp$36$x$35$$35$569 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$983 () Int)
(declare-fun papp4 () Int)
(declare-fun GHC.Types.Module () Int)
(declare-fun lq_tmp$36$x$35$$35$820 () Int)
(declare-fun VV$35$$35$F$35$$35$56 () Int)
(declare-fun x_Tuple64 () Int)
(declare-fun GHC.Types.I$35$ () Int)
(declare-fun lq_tmp$36$x$35$$35$1012 () Int)
(declare-fun GHC.Num.$36$fNumInt () Int)
(declare-fun ds_d15U () Int)
(declare-fun lq_tmp$36$x$35$$35$986 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p$35$$35$k_$35$$35$1062 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$853 () Int)
(declare-fun ds_d15H () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797843$35$$35$d16r () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797845$35$$35$d16t () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797847$35$$35$d16v () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a () Int)
(declare-fun xs$35$$35$aS1 () Int)
(declare-fun lq_tmp$36$x$35$$35$1097 () Int)
(declare-fun autolen () Int)
(declare-fun VV$35$$35$F$35$$35$6 () Int)
(declare-fun x_Tuple52 () Int)
(declare-fun lq_tmp$36$x$35$$35$623 () Int)
(declare-fun head () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$853 () Int)
(declare-fun is$36$GHC.Tuple.$40$$44$$44$$41$ () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797825$35$$35$d169 () Int)
(declare-fun is$36$GHC.Tuple.$40$$44$$44$$44$$44$$44$$44$$41$ () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e () Int)
(declare-fun is$36$GHC.Tuple.$40$$44$$44$$44$$44$$41$ () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$1062 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$983 () Int)
(declare-fun lq_tmp$36$x$35$$35$729 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m$35$$35$k_$35$$35$1062 () Int)
(declare-fun LiquidHaskell.ProofCombinators.QED () Int)
(declare-fun is$36$GHC.Types.$58$ () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797824$35$$35$d168 () Int)
(declare-fun papp2 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$1062 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g () Int)
(declare-fun x_Tuple62 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797840$35$$35$d16o$35$$35$k_$35$$35$1062 () Int)
(declare-fun VV$35$$35$F$35$$35$55 () Int)
(declare-fun Reverse.$43$$43$ () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$44$$41$$35$$35$5 () Int)
(declare-fun lit$36$main () Str)
(declare-fun lq_anf$36$$35$$35$7205759403792797840$35$$35$d16o () Int)
(declare-fun Reverse.reverse () Int)
(declare-fun fromJust () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$44$$44$$44$$41$$35$$35$5 () Int)
(declare-fun lq_tmp$36$x$35$$35$177 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$853 () Int)
(declare-fun papp7 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j$35$$35$k_$35$$35$983 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j () Int)
(declare-fun Reverse.singletonP () Int)
(declare-fun x_Tuple53 () Int)
(declare-fun lq_tmp$36$x$35$$35$622 () Int)
(declare-fun GHC.Types.$91$$93$ () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$44$$44$$41$$35$$35$6 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j$35$$35$k_$35$$35$1062 () Int)
(declare-fun x_Tuple71 () Int)
(declare-fun lq_tmp$36$x$35$$35$767 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$853 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$983 () Int)
(declare-fun VV$35$$35$F$35$$35$2 () Int)
(declare-fun xs$35$$35$aTz () Int)
(declare-fun lq_tmp$36$x$35$$35$300 () Int)
(declare-fun lq_tmp$36$x$35$$35$856 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$983 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$41$$35$$35$3 () Int)
(declare-fun GHC.Types.GT () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m$35$$35$k_$35$$35$983 () Int)
(declare-fun VV$35$$35$F$35$$35$64 () Int)
(declare-fun lq_tmp$36$x$35$$35$496 () Int)
(declare-fun VV$35$$35$F$35$$35$46 () Int)
(declare-fun x_Tuple74 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$44$$44$$41$$35$$35$3 () Int)
(declare-fun lq_tmp$36$x$35$$35$923 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$44$$44$$44$$41$$35$$35$4 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$853 () Int)
(declare-fun len () Int)
(declare-fun papp6 () Int)
(declare-fun VV$35$$35$F$35$$35$9 () Int)
(declare-fun x_Tuple22 () Int)
(declare-fun x_Tuple66 () Int)
(declare-fun x_Tuple44 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$44$$41$$35$$35$4 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q$35$$35$k_$35$$35$1062 () Int)
(declare-fun lq_tmp$36$x$35$$35$793 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$1062 () Int)
(declare-fun VV$35$$35$F$35$$35$62 () Int)
(declare-fun x_Tuple72 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$44$$44$$41$$35$$35$5 () Int)
(declare-fun lq_tmp$36$x$35$$35$951 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$853 () Int)
(declare-fun isJust () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q () Int)
(declare-fun ds_d161 () Int)
(declare-fun lq_tmp$36$x$35$$35$301 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$41$$35$$35$2 () Int)
(declare-fun lq_tmp$36$x$35$$35$1065 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l () Int)
(declare-fun x_Tuple31 () Int)
(declare-fun VV$35$$35$1158 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h () Int)
(declare-fun lq_tmp$36$x$35$$35$1038 () Int)
(declare-fun VV$35$$35$F$35$$35$65 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$44$$44$$41$$35$$35$2 () Int)
(declare-fun x_Tuple75 () Int)
(declare-fun lq_tmp$36$x$35$$35$705 () Int)
(declare-fun lq_tmp$36$x$35$$35$882 () Int)
(declare-fun LiquidHaskell.ProofCombinators.$61$$61$. () Int)
(declare-fun lit$36$Reverse () Str)
(declare-fun GHC.Types.TrNameS () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$983 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l$35$$35$k_$35$$35$1062 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$41$$35$$35$2 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$1062 () Int)
(declare-fun lq_tmp$36$x$35$$35$659 () Int)
(declare-fun papp1 () Int)
(declare-fun lq_tmp$36$x$35$$35$676 () Int)
(declare-fun x_Tuple61 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$41$$35$$35$3 () Int)
(declare-fun VV$35$$35$F$35$$35$53 () Int)
(declare-fun x_Tuple43 () Int)
(declare-fun tail () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$44$$41$$35$$35$3 () Int)
(declare-fun VV$35$$35$F$35$$35$68 () Int)
(declare-fun lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$983 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$44$$44$$44$$41$$35$$35$3 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$853 () Int)
(declare-fun lq_tmp$36$x$35$$35$419 () Int)
(declare-fun lq_tmp$36$x$35$$35$848 () Int)
(declare-fun lq_tmp$36$x$35$$35$914 () Int)
(declare-fun VV$35$$35$1138 () Int)
(declare-fun x_Tuple51 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k$35$$35$k_$35$$35$1062 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797822$35$$35$d166 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$41$$35$$35$4 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797821$35$$35$d165 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797823$35$$35$d167 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i () Int)
(declare-fun x$35$$35$aTv () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797820$35$$35$d164 () Int)
(declare-fun x_Tuple73 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$44$$44$$41$$35$$35$4 () Int)
(declare-fun GHC.Types.EQ () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$1062 () Int)
(declare-fun lq_tmp$36$x$35$$35$950 () Int)
(declare-fun lq_tmp$36$x$35$$35$458 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$983 () Int)
(declare-fun ds_d15N () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797818$35$$35$d162 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797819$35$$35$d163 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$41$$35$$35$1 () Int)
(declare-fun x_Tuple54 () Int)
(declare-fun VV$35$$35$F$35$$35$19 () Int)
(declare-fun lq_karg$36$VV$35$$35$1061$35$$35$k_$35$$35$1062 () Int)
(declare-fun lq_tmp$36$x$35$$35$302 () Int)
(declare-fun Reverse.$36$trModule () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$41$$35$$35$1 () Int)
(declare-fun lq_tmp$36$x$35$$35$595 () Int)
(declare-fun x_Tuple32 () Int)
(declare-fun VV$35$$35$F$35$$35$66 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n$35$$35$k_$35$$35$983 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$44$$44$$41$$35$$35$1 () Int)
(declare-fun x_Tuple76 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$853 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$44$$41$$35$$35$2 () Int)
(declare-fun lq_tmp$36$x$35$$35$978 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$44$$44$$44$$44$$41$$35$$35$2 () Int)
(declare-fun LiquidHaskell.ProofCombinators.$42$$42$$42$ () Int)
(declare-fun lq_tmp$36$x$35$$35$897 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f () Int)
(declare-fun GHC.Num.$43$ () Int)
(declare-fun VV$35$$35$1549 () Int)
(declare-fun lq_tmp$36$x$35$$35$428 () Int)
(declare-fun xs$35$$35$aTw () Int)
(declare-fun VV$35$$35$F$35$$35$16 () Int)
(declare-fun snd () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$1062 () Int)
(declare-fun fst () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$44$$41$$35$$35$2 () Int)
(declare-fun x_Tuple42 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n$35$$35$k_$35$$35$1062 () Int)
(declare-fun apply$35$$35$13 (Int (_ BitVec 32)) Bool)
(declare-fun apply$35$$35$9 (Int Str) Bool)
(declare-fun apply$35$$35$6 (Int Bool) Str)
(declare-fun apply$35$$35$11 (Int Str) (_ BitVec 32))
(declare-fun apply$35$$35$15 (Int (_ BitVec 32)) (_ BitVec 32))
(declare-fun apply$35$$35$0 (Int Int) Int)
(declare-fun apply$35$$35$8 (Int Str) Int)
(declare-fun apply$35$$35$1 (Int Int) Bool)
(declare-fun apply$35$$35$7 (Int Bool) (_ BitVec 32))
(declare-fun apply$35$$35$14 (Int (_ BitVec 32)) Str)
(declare-fun apply$35$$35$10 (Int Str) Str)
(declare-fun apply$35$$35$5 (Int Bool) Bool)
(declare-fun apply$35$$35$2 (Int Int) Str)
(declare-fun apply$35$$35$12 (Int (_ BitVec 32)) Int)
(declare-fun apply$35$$35$3 (Int Int) (_ BitVec 32))
(declare-fun apply$35$$35$4 (Int Bool) Int)
(declare-fun smt_lambda$35$$35$13 ((_ BitVec 32) Bool) Int)
(declare-fun smt_lambda$35$$35$9 (Str Bool) Int)
(declare-fun smt_lambda$35$$35$6 (Bool Str) Int)
(declare-fun smt_lambda$35$$35$11 (Str (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$15 ((_ BitVec 32) (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$0 (Int Int) Int)
(declare-fun smt_lambda$35$$35$8 (Str Int) Int)
(declare-fun smt_lambda$35$$35$1 (Int Bool) Int)
(declare-fun smt_lambda$35$$35$7 (Bool (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$14 ((_ BitVec 32) Str) Int)
(declare-fun smt_lambda$35$$35$10 (Str Str) Int)
(declare-fun smt_lambda$35$$35$5 (Bool Bool) Int)
(declare-fun smt_lambda$35$$35$2 (Int Str) Int)
(declare-fun smt_lambda$35$$35$12 ((_ BitVec 32) Int) Int)
(declare-fun smt_lambda$35$$35$3 (Int (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$4 (Bool Int) Int)
(declare-fun lam_arg$35$$35$1$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$2$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$3$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$4$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$5$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$6$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$7$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$1$35$$35$8 () Str)
(declare-fun lam_arg$35$$35$2$35$$35$8 () Str)
(declare-fun lam_arg$35$$35$3$35$$35$8 () Str)
(declare-fun lam_arg$35$$35$4$35$$35$8 () Str)
(declare-fun lam_arg$35$$35$5$35$$35$8 () Str)
(declare-fun lam_arg$35$$35$6$35$$35$8 () Str)
(declare-fun lam_arg$35$$35$7$35$$35$8 () Str)
(declare-fun lam_arg$35$$35$1$35$$35$12 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$2$35$$35$12 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$3$35$$35$12 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$4$35$$35$12 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$5$35$$35$12 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$6$35$$35$12 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$7$35$$35$12 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$1$35$$35$4 () Bool)
(declare-fun lam_arg$35$$35$2$35$$35$4 () Bool)
(declare-fun lam_arg$35$$35$3$35$$35$4 () Bool)
(declare-fun lam_arg$35$$35$4$35$$35$4 () Bool)
(declare-fun lam_arg$35$$35$5$35$$35$4 () Bool)
(declare-fun lam_arg$35$$35$6$35$$35$4 () Bool)
(declare-fun lam_arg$35$$35$7$35$$35$4 () Bool)

(assert (distinct lit$36$Reverse lit$36$main))
(assert (distinct GHC.Types.EQ GHC.Types.GT GHC.Types.LT))
(assert (= (strLen lit$36$main) 4))
(assert (= (strLen lit$36$Reverse) 7))
(push 1)
(assert (and (and (>= (apply$35$$35$0 (as Reverse.length Int) ds_d15H) 0) (>= (apply$35$$35$0 (as len Int) ds_d15H) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) ys$35$$35$aTx) 0) (>= (apply$35$$35$0 (as len Int) ys$35$$35$aTx) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (= lq_anf$36$$35$$35$7205759403792797821$35$$35$d165 ds_d15H) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (= lq_anf$36$$35$$35$7205759403792797821$35$$35$d165 ds_d15H) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (= lq_anf$36$$35$$35$7205759403792797821$35$$35$d165 ds_d15H) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) true) (= lq_anf$36$$35$$35$7205759403792797821$35$$35$d165 (as GHC.Types.$91$$93$ Int)) (= lq_anf$36$$35$$35$7205759403792797821$35$$35$d165 (as GHC.Types.$91$$93$ Int)) (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) true) (= lq_anf$36$$35$$35$7205759403792797821$35$$35$d165 (as GHC.Types.$91$$93$ Int)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$64) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$64) 0) (= VV$35$$35$F$35$$35$64 ys$35$$35$aTx) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$64) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$64) 0))))
(push 1)
(assert (not (= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$64) (+ (apply$35$$35$0 (as Reverse.length Int) ds_d15H) (apply$35$$35$0 (as Reverse.length Int) ys$35$$35$aTx)))))
(check-sat)
; SMT Says: Unsat
(pop 1)
(pop 1)
(push 1)
(assert (and (and (>= (apply$35$$35$0 (as len Int) xs$35$$35$aS1) 0) (=> (< (apply$35$$35$0 (as len Int) xs$35$$35$aS1) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aS1) 0)))) (and (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0))) (= lq_anf$36$$35$$35$7205759403792797818$35$$35$d162 ds_d15U) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0))) (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (+ 1 (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aS1))) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (+ 1 (apply$35$$35$0 (as len Int) xs$35$$35$aS1))) (= (apply$35$$35$0 (as tail Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) xs$35$$35$aS1) (= (apply$35$$35$0 (as head Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) ds_d161) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) xs$35$$35$aS1) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) ds_d161) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) false) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) xs$35$$35$aS1) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) ds_d161) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) xs$35$$35$aS1) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) ds_d161) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) false) (= lq_anf$36$$35$$35$7205759403792797818$35$$35$d162 (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) ds_d161) xs$35$$35$aS1)) (= lq_anf$36$$35$$35$7205759403792797818$35$$35$d162 (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) ds_d161) xs$35$$35$aS1)) (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (+ 1 (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aS1))) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (+ 1 (apply$35$$35$0 (as len Int) xs$35$$35$aS1))) (= (apply$35$$35$0 (as tail Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) xs$35$$35$aS1) (= (apply$35$$35$0 (as head Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) ds_d161) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) xs$35$$35$aS1) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) ds_d161) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) false) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) xs$35$$35$aS1) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) ds_d161) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) xs$35$$35$aS1) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) ds_d161) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) false) (= lq_anf$36$$35$$35$7205759403792797818$35$$35$d162 (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) ds_d161) xs$35$$35$aS1)) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0)))) (= lq_anf$36$$35$$35$7205759403792797819$35$$35$d163 1) (and (>= lq_anf$36$$35$$35$7205759403792797820$35$$35$d164 0) (= lq_anf$36$$35$$35$7205759403792797820$35$$35$d164 (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aS1)) (= lq_anf$36$$35$$35$7205759403792797820$35$$35$d164 (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aS1))) (and (>= (apply$35$$35$0 (as len Int) ds_d15U) 0) (=> (< (apply$35$$35$0 (as len Int) ds_d15U) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) ds_d15U) 0)))) (and (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0))) (= lq_anf$36$$35$$35$7205759403792797818$35$$35$d162 ds_d15U) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0)))) (= VV$35$$35$F$35$$35$65 (+ lq_anf$36$$35$$35$7205759403792797819$35$$35$d163 lq_anf$36$$35$$35$7205759403792797820$35$$35$d164)) (and (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0))) (= lq_anf$36$$35$$35$7205759403792797818$35$$35$d162 ds_d15U) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0))) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0))))))
(push 1)
(assert (not (and (>= VV$35$$35$F$35$$35$65 0) (= VV$35$$35$F$35$$35$65 (apply$35$$35$0 (as Reverse.length Int) ds_d15U)))))
(check-sat)
; SMT Says: Unsat
(pop 1)
(pop 1)
(push 1)
(assert (and (and (or  (exists ((lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$983 Int) (lq_karg$36$VV$35$$35$982$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$983 Int) (lq_tmp$36$x$35$$35$988 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$983 Int) (lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n$35$$35$k_$35$$35$983 Int)) (and (and (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$VV$35$$35$982$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797840$35$$35$d16o) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_tmp$36$x$35$$35$988 lq_anf$36$$35$$35$7205759403792797840$35$$35$d16o) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$983 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n)) (exists ((VV$35$$35$F$35$$35$19 Int)) (and (and (or  (exists ((lq_karg$36$VV$35$$35$852$35$$35$k_$35$$35$853 Int) (lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$853 Int)) (and (and (= lq_karg$36$VV$35$$35$852$35$$35$k_$35$$35$853 VV$35$$35$F$35$$35$19) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$853 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d)) (exists ((VV$35$$35$F$35$$35$31 Int)) (and (and (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$31)) (= VV$35$$35$F$35$$35$31 (apply$35$$35$0 (as Reverse.reverse Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c)) (= VV$35$$35$F$35$$35$31 (ite (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (as GHC.Types.$91$$93$ Int) (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) (apply$35$$35$0 (as Reverse.reverse Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c))) (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c)) (as GHC.Types.$91$$93$ Int))))) (= VV$35$$35$F$35$$35$31 (apply$35$$35$0 (as Reverse.reverse Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c)) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$31) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$31) 0) (= VV$35$$35$F$35$$35$31 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$31) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$31) 0)) (and (= lq_karg$36$VV$35$$35$852$35$$35$k_$35$$35$853 VV$35$$35$F$35$$35$31) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$853 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d)))))) (exists ((lq_karg$36$VV$35$$35$852$35$$35$k_$35$$35$853 Int) (lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$853 Int)) (and (and (= lq_karg$36$VV$35$$35$852$35$$35$k_$35$$35$853 VV$35$$35$F$35$$35$19) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$853 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d)) (exists ((VV$35$$35$F$35$$35$28 Int)) (and (and (= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$28) (+ (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h))) (= VV$35$$35$F$35$$35$28 (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h)) (= VV$35$$35$F$35$$35$28 (ite (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f)) (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f)) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h)))) (= VV$35$$35$F$35$$35$28 (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h)) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$28) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$28) 0) (= VV$35$$35$F$35$$35$28 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$28) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$28) 0)) (and (= lq_karg$36$VV$35$$35$852$35$$35$k_$35$$35$853 VV$35$$35$F$35$$35$28) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$853 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d))))))) (and (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$19) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$19) 0) (= VV$35$$35$F$35$$35$19 lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$19) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$19) 0))) (and (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$VV$35$$35$982$35$$35$k_$35$$35$983 VV$35$$35$F$35$$35$19) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$983 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n)))))) (exists ((lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$983 Int) (lq_karg$36$VV$35$$35$982$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$983 Int) (lq_tmp$36$x$35$$35$988 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$983 Int) (lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n$35$$35$k_$35$$35$983 Int)) (and (and (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$VV$35$$35$982$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797840$35$$35$d16o) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_tmp$36$x$35$$35$988 lq_anf$36$$35$$35$7205759403792797840$35$$35$d16o) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$983 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n)) (exists ((VV$35$$35$F$35$$35$16 Int)) (and (and (= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$16) (+ (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m))) (= VV$35$$35$F$35$$35$16 (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m)) (= VV$35$$35$F$35$$35$16 (ite (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k)) (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k)) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m)))) (= VV$35$$35$F$35$$35$16 (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m)) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$16) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$16) 0) (= VV$35$$35$F$35$$35$16 lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$16) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$16) 0)) (and (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$VV$35$$35$982$35$$35$k_$35$$35$983 VV$35$$35$F$35$$35$16) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$983 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n))))))) (or  (exists ((lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$1062 Int) (lq_tmp$36$x$35$$35$1067 Int) (lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797840$35$$35$d16o$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$1062 Int) (lq_karg$36$VV$35$$35$1061$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n$35$$35$k_$35$$35$1062 Int)) (and (and (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_tmp$36$x$35$$35$1067 lq_anf$36$$35$$35$7205759403792797843$35$$35$d16r) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$1062 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797840$35$$35$d16o$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797840$35$$35$d16o) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$VV$35$$35$1061$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797843$35$$35$d16r) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n)) (exists ((VV$35$$35$F$35$$35$9 Int)) (and (and (or  (exists ((lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$983 Int) (lq_karg$36$VV$35$$35$982$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$983 Int) (lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n$35$$35$k_$35$$35$983 Int)) (and (and (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$VV$35$$35$982$35$$35$k_$35$$35$983 VV$35$$35$F$35$$35$9) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$983 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n)) (exists ((VV$35$$35$F$35$$35$19 Int)) (and (and (or  (exists ((lq_karg$36$VV$35$$35$852$35$$35$k_$35$$35$853 Int) (lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$853 Int)) (and (and (= lq_karg$36$VV$35$$35$852$35$$35$k_$35$$35$853 VV$35$$35$F$35$$35$19) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$853 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d)) (exists ((VV$35$$35$F$35$$35$31 Int)) (and (and (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$31)) (= VV$35$$35$F$35$$35$31 (apply$35$$35$0 (as Reverse.reverse Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c)) (= VV$35$$35$F$35$$35$31 (ite (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (as GHC.Types.$91$$93$ Int) (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) (apply$35$$35$0 (as Reverse.reverse Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c))) (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c)) (as GHC.Types.$91$$93$ Int))))) (= VV$35$$35$F$35$$35$31 (apply$35$$35$0 (as Reverse.reverse Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c)) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$31) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$31) 0) (= VV$35$$35$F$35$$35$31 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$31) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$31) 0)) (and (= lq_karg$36$VV$35$$35$852$35$$35$k_$35$$35$853 VV$35$$35$F$35$$35$31) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$853 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d)))))) (exists ((lq_karg$36$VV$35$$35$852$35$$35$k_$35$$35$853 Int) (lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$853 Int)) (and (and (= lq_karg$36$VV$35$$35$852$35$$35$k_$35$$35$853 VV$35$$35$F$35$$35$19) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$853 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d)) (exists ((VV$35$$35$F$35$$35$28 Int)) (and (and (= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$28) (+ (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h))) (= VV$35$$35$F$35$$35$28 (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h)) (= VV$35$$35$F$35$$35$28 (ite (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f)) (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f)) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h)))) (= VV$35$$35$F$35$$35$28 (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h)) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$28) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$28) 0) (= VV$35$$35$F$35$$35$28 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$28) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$28) 0)) (and (= lq_karg$36$VV$35$$35$852$35$$35$k_$35$$35$853 VV$35$$35$F$35$$35$28) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$853 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d))))))) (and (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$19) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$19) 0) (= VV$35$$35$F$35$$35$19 lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$19) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$19) 0))) (and (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$VV$35$$35$982$35$$35$k_$35$$35$983 VV$35$$35$F$35$$35$19) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$983 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n)))))) (exists ((lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$983 Int) (lq_karg$36$VV$35$$35$982$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$983 Int) (lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$983 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n$35$$35$k_$35$$35$983 Int)) (and (and (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$VV$35$$35$982$35$$35$k_$35$$35$983 VV$35$$35$F$35$$35$9) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$983 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n)) (exists ((VV$35$$35$F$35$$35$16 Int)) (and (and (= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$16) (+ (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m))) (= VV$35$$35$F$35$$35$16 (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m)) (= VV$35$$35$F$35$$35$16 (ite (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k)) (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k)) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m)))) (= VV$35$$35$F$35$$35$16 (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m)) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$16) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$16) 0) (= VV$35$$35$F$35$$35$16 lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$16) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$16) 0)) (and (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$VV$35$$35$982$35$$35$k_$35$$35$983 VV$35$$35$F$35$$35$16) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$983 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n$35$$35$k_$35$$35$983 lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n))))))) (and (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$9) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$9) 0) (= VV$35$$35$F$35$$35$9 lq_anf$36$$35$$35$7205759403792797840$35$$35$d16o) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$9) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$9) 0))) (and (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$1062 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797840$35$$35$d16o$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797840$35$$35$d16o) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$VV$35$$35$1061$35$$35$k_$35$$35$1062 VV$35$$35$F$35$$35$9) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n)))))) (exists ((lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$1062 Int) (lq_tmp$36$x$35$$35$1067 Int) (lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797840$35$$35$d16o$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$1062 Int) (lq_karg$36$VV$35$$35$1061$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$1062 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n$35$$35$k_$35$$35$1062 Int)) (and (and (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_tmp$36$x$35$$35$1067 lq_anf$36$$35$$35$7205759403792797843$35$$35$d16r) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$1062 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797840$35$$35$d16o$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797840$35$$35$d16o) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$VV$35$$35$1061$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797843$35$$35$d16r) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n)) (exists ((VV$35$$35$F$35$$35$6 Int)) (and (and (= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$6) (+ 1 (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p))) (= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$6) (+ 1 (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p))) (= (apply$35$$35$0 (as tail Int) VV$35$$35$F$35$$35$6) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p) (= (apply$35$$35$0 (as head Int) VV$35$$35$F$35$$35$6) x$35$$35$aTB) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) VV$35$$35$F$35$$35$6) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) VV$35$$35$F$35$$35$6) x$35$$35$aTB) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) VV$35$$35$F$35$$35$6) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) VV$35$$35$F$35$$35$6) false) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) VV$35$$35$F$35$$35$6) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) VV$35$$35$F$35$$35$6) x$35$$35$aTB) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) VV$35$$35$F$35$$35$6) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) VV$35$$35$F$35$$35$6) x$35$$35$aTB) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) VV$35$$35$F$35$$35$6) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) VV$35$$35$F$35$$35$6) false) (= VV$35$$35$F$35$$35$6 (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTB) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p)) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$6) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$6) 0) (= VV$35$$35$F$35$$35$6 lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$6) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$6) 0)) (and (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$1062 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797840$35$$35$d16o$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797840$35$$35$d16o) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$VV$35$$35$1061$35$$35$k_$35$$35$1062 VV$35$$35$F$35$$35$6) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n$35$$35$k_$35$$35$1062 lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n))))))) (or  (exists ((lq_karg$36$VV$35$$35$852$35$$35$k_$35$$35$853 Int) (lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$853 Int) (lq_tmp$36$x$35$$35$858 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$853 Int)) (and (and (= lq_karg$36$VV$35$$35$852$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$853 x$35$$35$aTB) (= lq_tmp$36$x$35$$35$858 lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d)) (exists ((VV$35$$35$F$35$$35$31 Int)) (and (and (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$31)) (= VV$35$$35$F$35$$35$31 (apply$35$$35$0 (as Reverse.reverse Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c)) (= VV$35$$35$F$35$$35$31 (ite (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (as GHC.Types.$91$$93$ Int) (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) (apply$35$$35$0 (as Reverse.reverse Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c))) (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c)) (as GHC.Types.$91$$93$ Int))))) (= VV$35$$35$F$35$$35$31 (apply$35$$35$0 (as Reverse.reverse Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c)) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$31) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$31) 0) (= VV$35$$35$F$35$$35$31 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$31) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$31) 0)) (and (= lq_karg$36$VV$35$$35$852$35$$35$k_$35$$35$853 VV$35$$35$F$35$$35$31) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$853 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d)))))) (exists ((lq_karg$36$VV$35$$35$852$35$$35$k_$35$$35$853 Int) (lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$853 Int) (lq_tmp$36$x$35$$35$858 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$853 Int) (lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$853 Int)) (and (and (= lq_karg$36$VV$35$$35$852$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$853 x$35$$35$aTB) (= lq_tmp$36$x$35$$35$858 lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d)) (exists ((VV$35$$35$F$35$$35$28 Int)) (and (and (= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$28) (+ (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h))) (= VV$35$$35$F$35$$35$28 (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h)) (= VV$35$$35$F$35$$35$28 (ite (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f)) (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f)) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h)))) (= VV$35$$35$F$35$$35$28 (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h)) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$28) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$28) 0) (= VV$35$$35$F$35$$35$28 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$28) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$28) 0)) (and (= lq_karg$36$VV$35$$35$852$35$$35$k_$35$$35$853 VV$35$$35$F$35$$35$28) (= lq_karg$36$x$35$$35$aTB$35$$35$k_$35$$35$853 x$35$$35$aTB) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (= lq_karg$36$lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d$35$$35$k_$35$$35$853 lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d)))))))) (and (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) 0) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) 0) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) true) (= lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k (as GHC.Types.$91$$93$ Int)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) 0)) (and (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) 0) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) 0) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) true) (= lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b (as GHC.Types.$91$$93$ Int)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) 0)) (and (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) 0) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) 0) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) true) (= lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l (as GHC.Types.$91$$93$ Int)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) 0)) (and (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (+ 1 (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b))) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (+ 1 (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b))) (= (apply$35$$35$0 (as tail Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= (apply$35$$35$0 (as head Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) x$35$$35$aTB) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) x$35$$35$aTB) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) false) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) x$35$$35$aTB) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) x$35$$35$aTB) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) false) (= lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTB) lq_anf$36$$35$$35$7205759403792797827$35$$35$d16b)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) 0)) (and (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) (+ 1 (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l))) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) (+ 1 (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l))) (= (apply$35$$35$0 (as tail Int) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) (= (apply$35$$35$0 (as head Int) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) x$35$$35$aTB) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) x$35$$35$aTB) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) false) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) x$35$$35$aTB) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) x$35$$35$aTB) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) false) (= lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTB) lq_anf$36$$35$$35$7205759403792797837$35$$35$d16l)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m) 0)) (and (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d)) (= lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d (apply$35$$35$0 (as Reverse.reverse Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c)) (= lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d (ite (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c) (as GHC.Types.$91$$93$ Int) (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) (apply$35$$35$0 (as Reverse.reverse Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c))) (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c)) (as GHC.Types.$91$$93$ Int))))) (= lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d (apply$35$$35$0 (as Reverse.reverse Int) lq_anf$36$$35$$35$7205759403792797828$35$$35$d16c)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797829$35$$35$d16d) 0)) (and (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n) (+ (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m))) (= lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m)) (= lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n (ite (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k)) (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k)) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m)))) (= lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) lq_anf$36$$35$$35$7205759403792797836$35$$35$d16k) lq_anf$36$$35$$35$7205759403792797838$35$$35$d16m)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797839$35$$35$d16n) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797840$35$$35$d16o) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797840$35$$35$d16o) 0)) (and (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) 0) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) 0) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) true) (= lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e (as GHC.Types.$91$$93$ Int)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) 0)) (and (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f)) (= lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f (apply$35$$35$0 (as Reverse.reverse Int) lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e)) (= lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f (ite (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e) (as GHC.Types.$91$$93$ Int) (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) (apply$35$$35$0 (as Reverse.reverse Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e))) (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e)) (as GHC.Types.$91$$93$ Int))))) (= lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f (apply$35$$35$0 (as Reverse.reverse Int) lq_anf$36$$35$$35$7205759403792797830$35$$35$d16e)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) 0)) (and (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p) 0) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p) 0) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p) true) (= lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p (as GHC.Types.$91$$93$ Int)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p) 0)) (and (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) 0) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) 0) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) true) (= lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g (as GHC.Types.$91$$93$ Int)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) 0)) (and (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) (+ 1 (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p))) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) (+ 1 (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p))) (= (apply$35$$35$0 (as tail Int) lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p) (= (apply$35$$35$0 (as head Int) lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) x$35$$35$aTB) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) x$35$$35$aTB) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) false) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) x$35$$35$aTB) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) x$35$$35$aTB) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) false) (= lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTB) lq_anf$36$$35$$35$7205759403792797841$35$$35$d16p)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797842$35$$35$d16q) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797843$35$$35$d16r) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797843$35$$35$d16r) 0)) (and (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (+ 1 (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g))) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) (+ 1 (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g))) (= (apply$35$$35$0 (as tail Int) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= (apply$35$$35$0 (as head Int) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) x$35$$35$aTB) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) x$35$$35$aTB) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) false) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) x$35$$35$aTB) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) x$35$$35$aTB) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) false) (= lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTB) lq_anf$36$$35$$35$7205759403792797832$35$$35$d16g)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h) 0)) (and (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) (+ (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h))) (= lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h)) (= lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i (ite (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f)) (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f)) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h)))) (= lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) lq_anf$36$$35$$35$7205759403792797831$35$$35$d16f) lq_anf$36$$35$$35$7205759403792797833$35$$35$d16h)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797834$35$$35$d16i) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797835$35$$35$d16j) 0))))
(push 1)
(assert (not (= (apply$35$$35$0 (as Reverse.reverse Int) (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTB) (as GHC.Types.$91$$93$ Int))) (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTB) (as GHC.Types.$91$$93$ Int)))))
(check-sat)
; SMT Says: Unsat
(pop 1)
(pop 1)
(push 1)
(assert (and (and (>= (apply$35$$35$0 (as len Int) xs$35$$35$aS1) 0) (=> (< (apply$35$$35$0 (as len Int) xs$35$$35$aS1) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aS1) 0)))) (and (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0))) (= lq_anf$36$$35$$35$7205759403792797818$35$$35$d162 ds_d15U) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0))) (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (+ 1 (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aS1))) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (+ 1 (apply$35$$35$0 (as len Int) xs$35$$35$aS1))) (= (apply$35$$35$0 (as tail Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) xs$35$$35$aS1) (= (apply$35$$35$0 (as head Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) ds_d161) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) xs$35$$35$aS1) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) ds_d161) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) false) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) xs$35$$35$aS1) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) ds_d161) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) xs$35$$35$aS1) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) ds_d161) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) false) (= lq_anf$36$$35$$35$7205759403792797818$35$$35$d162 (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) ds_d161) xs$35$$35$aS1)) (= lq_anf$36$$35$$35$7205759403792797818$35$$35$d162 (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) ds_d161) xs$35$$35$aS1)) (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (+ 1 (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aS1))) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (+ 1 (apply$35$$35$0 (as len Int) xs$35$$35$aS1))) (= (apply$35$$35$0 (as tail Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) xs$35$$35$aS1) (= (apply$35$$35$0 (as head Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) ds_d161) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) xs$35$$35$aS1) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) ds_d161) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) false) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) xs$35$$35$aS1) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) ds_d161) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) xs$35$$35$aS1) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) ds_d161) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) false) (= lq_anf$36$$35$$35$7205759403792797818$35$$35$d162 (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) ds_d161) xs$35$$35$aS1)) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0)))) (= lq_anf$36$$35$$35$7205759403792797819$35$$35$d163 1) (and (>= (apply$35$$35$0 (as len Int) ds_d15U) 0) (=> (< (apply$35$$35$0 (as len Int) ds_d15U) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) ds_d15U) 0)))) (and (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0))) (= lq_anf$36$$35$$35$7205759403792797818$35$$35$d162 ds_d15U) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0)))) (and (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$66) 0) (=> (< (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$66) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$66) 0))) (= VV$35$$35$F$35$$35$66 xs$35$$35$aS1) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$66) 0) (=> (< (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$66) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$66) 0)))) (and (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0))) (= lq_anf$36$$35$$35$7205759403792797818$35$$35$d162 ds_d15U) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0))) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0))))))
(push 1)
(assert (not (and (< (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$66) (apply$35$$35$0 (as len Int) ds_d15U)) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$66) 0))))
(check-sat)
; SMT Says: Unsat
(pop 1)
(pop 1)
(push 1)
(assert (and (= VV$35$$35$F$35$$35$68 0) (and (>= (apply$35$$35$0 (as len Int) ds_d15U) 0) (=> (< (apply$35$$35$0 (as len Int) ds_d15U) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) ds_d15U) 0)))) (and (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0))) (= lq_anf$36$$35$$35$7205759403792797818$35$$35$d162 ds_d15U) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0)))) (and (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0))) (= lq_anf$36$$35$$35$7205759403792797818$35$$35$d162 ds_d15U) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0))) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0)))) (and (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0))) (= lq_anf$36$$35$$35$7205759403792797818$35$$35$d162 ds_d15U) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0))) (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) true) (= lq_anf$36$$35$$35$7205759403792797818$35$$35$d162 (as GHC.Types.$91$$93$ Int)) (= lq_anf$36$$35$$35$7205759403792797818$35$$35$d162 (as GHC.Types.$91$$93$ Int)) (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) true) (= lq_anf$36$$35$$35$7205759403792797818$35$$35$d162 (as GHC.Types.$91$$93$ Int)) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0) (=> (< (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) (apply$35$$35$0 (as len Int) ds_d15U)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797818$35$$35$d162) 0))))))
(push 1)
(assert (not (and (>= VV$35$$35$F$35$$35$68 0) (= VV$35$$35$F$35$$35$68 (apply$35$$35$0 (as Reverse.length Int) ds_d15U)))))
(check-sat)
; SMT Says: Unsat
(pop 1)
(pop 1)
(push 1)
(assert (and (and (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$53) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$53) 0) (= VV$35$$35$F$35$$35$53 xs$35$$35$aTw) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$53) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$53) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) ds_d15N) 0) (>= (apply$35$$35$0 (as len Int) ds_d15N) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (= lq_anf$36$$35$$35$7205759403792797823$35$$35$d167 ds_d15N) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (= lq_anf$36$$35$$35$7205759403792797823$35$$35$d167 ds_d15N) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aTw) 0) (>= (apply$35$$35$0 (as len Int) xs$35$$35$aTw) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (= lq_anf$36$$35$$35$7205759403792797823$35$$35$d167 ds_d15N) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) (+ 1 (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aTw))) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) (+ 1 (apply$35$$35$0 (as len Int) xs$35$$35$aTw))) (= (apply$35$$35$0 (as tail Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) xs$35$$35$aTw) (= (apply$35$$35$0 (as head Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) x$35$$35$aTv) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) xs$35$$35$aTw) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) x$35$$35$aTv) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) false) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) xs$35$$35$aTw) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) x$35$$35$aTv) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) xs$35$$35$aTw) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) x$35$$35$aTv) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) false) (= lq_anf$36$$35$$35$7205759403792797823$35$$35$d167 (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTv) xs$35$$35$aTw)) (= lq_anf$36$$35$$35$7205759403792797823$35$$35$d167 (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTv) xs$35$$35$aTw)) (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) (+ 1 (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aTw))) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) (+ 1 (apply$35$$35$0 (as len Int) xs$35$$35$aTw))) (= (apply$35$$35$0 (as tail Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) xs$35$$35$aTw) (= (apply$35$$35$0 (as head Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) x$35$$35$aTv) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) xs$35$$35$aTw) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) x$35$$35$aTv) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) false) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) xs$35$$35$aTw) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) x$35$$35$aTv) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) xs$35$$35$aTw) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) x$35$$35$aTv) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) false) (= lq_anf$36$$35$$35$7205759403792797823$35$$35$d167 (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTv) xs$35$$35$aTw)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0))))
(push 1)
(assert (not (and (< (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$53) (apply$35$$35$0 (as len Int) ds_d15N)) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$53) 0))))
(check-sat)
; SMT Says: Unsat
(pop 1)
(pop 1)
(push 1)
(assert (and (and (>= (apply$35$$35$0 (as Reverse.length Int) ds_d15N) 0) (>= (apply$35$$35$0 (as len Int) ds_d15N) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (= lq_anf$36$$35$$35$7205759403792797823$35$$35$d167 ds_d15N) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0)) (and (= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$55) 0) (= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$55) 0) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) VV$35$$35$F$35$$35$55) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) VV$35$$35$F$35$$35$55) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) VV$35$$35$F$35$$35$55) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) VV$35$$35$F$35$$35$55) true) (= VV$35$$35$F$35$$35$55 (as GHC.Types.$91$$93$ Int)) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$55) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$55) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (= lq_anf$36$$35$$35$7205759403792797823$35$$35$d167 ds_d15N) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (= lq_anf$36$$35$$35$7205759403792797823$35$$35$d167 ds_d15N) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) true) (= lq_anf$36$$35$$35$7205759403792797823$35$$35$d167 (as GHC.Types.$91$$93$ Int)) (= lq_anf$36$$35$$35$7205759403792797823$35$$35$d167 (as GHC.Types.$91$$93$ Int)) (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) true) (= lq_anf$36$$35$$35$7205759403792797823$35$$35$d167 (as GHC.Types.$91$$93$ Int)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0))))
(push 1)
(assert (not (= (apply$35$$35$0 (as Reverse.length Int) ds_d15N) (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$55))))
(check-sat)
; SMT Says: Unsat
(pop 1)
(pop 1)
(push 1)
(assert (and (and (= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$56) (+ 1 (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797822$35$$35$d166))) (= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$56) (+ 1 (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797822$35$$35$d166))) (= (apply$35$$35$0 (as tail Int) VV$35$$35$F$35$$35$56) lq_anf$36$$35$$35$7205759403792797822$35$$35$d166) (= (apply$35$$35$0 (as head Int) VV$35$$35$F$35$$35$56) x$35$$35$aTy) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) VV$35$$35$F$35$$35$56) lq_anf$36$$35$$35$7205759403792797822$35$$35$d166) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) VV$35$$35$F$35$$35$56) x$35$$35$aTy) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) VV$35$$35$F$35$$35$56) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) VV$35$$35$F$35$$35$56) false) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) VV$35$$35$F$35$$35$56) lq_anf$36$$35$$35$7205759403792797822$35$$35$d166) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) VV$35$$35$F$35$$35$56) x$35$$35$aTy) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) VV$35$$35$F$35$$35$56) lq_anf$36$$35$$35$7205759403792797822$35$$35$d166) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) VV$35$$35$F$35$$35$56) x$35$$35$aTy) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) VV$35$$35$F$35$$35$56) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) VV$35$$35$F$35$$35$56) false) (= VV$35$$35$F$35$$35$56 (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTy) lq_anf$36$$35$$35$7205759403792797822$35$$35$d166)) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$56) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$56) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) ds_d15H) 0) (>= (apply$35$$35$0 (as len Int) ds_d15H) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) ys$35$$35$aTx) 0) (>= (apply$35$$35$0 (as len Int) ys$35$$35$aTx) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (= lq_anf$36$$35$$35$7205759403792797821$35$$35$d165 ds_d15H) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (= lq_anf$36$$35$$35$7205759403792797821$35$$35$d165 ds_d15H) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aTz) 0) (>= (apply$35$$35$0 (as len Int) xs$35$$35$aTz) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (= lq_anf$36$$35$$35$7205759403792797821$35$$35$d165 ds_d15H) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) (+ 1 (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aTz))) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) (+ 1 (apply$35$$35$0 (as len Int) xs$35$$35$aTz))) (= (apply$35$$35$0 (as tail Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) xs$35$$35$aTz) (= (apply$35$$35$0 (as head Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) x$35$$35$aTy) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) xs$35$$35$aTz) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) x$35$$35$aTy) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) false) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) xs$35$$35$aTz) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) x$35$$35$aTy) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) xs$35$$35$aTz) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) x$35$$35$aTy) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) false) (= lq_anf$36$$35$$35$7205759403792797821$35$$35$d165 (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTy) xs$35$$35$aTz)) (= lq_anf$36$$35$$35$7205759403792797821$35$$35$d165 (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTy) xs$35$$35$aTz)) (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) (+ 1 (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aTz))) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) (+ 1 (apply$35$$35$0 (as len Int) xs$35$$35$aTz))) (= (apply$35$$35$0 (as tail Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) xs$35$$35$aTz) (= (apply$35$$35$0 (as head Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) x$35$$35$aTy) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) xs$35$$35$aTz) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) x$35$$35$aTy) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) false) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) xs$35$$35$aTz) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) x$35$$35$aTy) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) xs$35$$35$aTz) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) x$35$$35$aTy) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) false) (= lq_anf$36$$35$$35$7205759403792797821$35$$35$d165 (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTy) xs$35$$35$aTz)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0)) (and (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797822$35$$35$d166) (+ (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aTz) (apply$35$$35$0 (as Reverse.length Int) ys$35$$35$aTx))) (= lq_anf$36$$35$$35$7205759403792797822$35$$35$d166 (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) xs$35$$35$aTz) ys$35$$35$aTx)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797822$35$$35$d166) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797822$35$$35$d166) 0))))
(push 1)
(assert (not (= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$56) (+ (apply$35$$35$0 (as Reverse.length Int) ds_d15H) (apply$35$$35$0 (as Reverse.length Int) ys$35$$35$aTx)))))
(check-sat)
; SMT Says: Unsat
(pop 1)
(pop 1)
(push 1)
(assert (and (and (>= (apply$35$$35$0 (as Reverse.length Int) ds_d15N) 0) (>= (apply$35$$35$0 (as len Int) ds_d15N) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (= lq_anf$36$$35$$35$7205759403792797823$35$$35$d167 ds_d15N) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (= lq_anf$36$$35$$35$7205759403792797823$35$$35$d167 ds_d15N) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0)) (and (= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$46) (+ (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797824$35$$35$d168) (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a))) (= VV$35$$35$F$35$$35$46 (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) lq_anf$36$$35$$35$7205759403792797824$35$$35$d168) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a)) (= VV$35$$35$F$35$$35$46 (ite (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797824$35$$35$d168) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797824$35$$35$d168)) (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797824$35$$35$d168)) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a)))) (= VV$35$$35$F$35$$35$46 (apply$35$$35$0 (apply$35$$35$0 (as Reverse.$43$$43$ Int) lq_anf$36$$35$$35$7205759403792797824$35$$35$d168) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a)) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$46) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$46) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aTw) 0) (>= (apply$35$$35$0 (as len Int) xs$35$$35$aTw) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (= lq_anf$36$$35$$35$7205759403792797823$35$$35$d167 ds_d15N) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) (+ 1 (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aTw))) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) (+ 1 (apply$35$$35$0 (as len Int) xs$35$$35$aTw))) (= (apply$35$$35$0 (as tail Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) xs$35$$35$aTw) (= (apply$35$$35$0 (as head Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) x$35$$35$aTv) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) xs$35$$35$aTw) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) x$35$$35$aTv) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) false) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) xs$35$$35$aTw) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) x$35$$35$aTv) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) xs$35$$35$aTw) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) x$35$$35$aTv) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) false) (= lq_anf$36$$35$$35$7205759403792797823$35$$35$d167 (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTv) xs$35$$35$aTw)) (= lq_anf$36$$35$$35$7205759403792797823$35$$35$d167 (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTv) xs$35$$35$aTw)) (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) (+ 1 (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aTw))) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) (+ 1 (apply$35$$35$0 (as len Int) xs$35$$35$aTw))) (= (apply$35$$35$0 (as tail Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) xs$35$$35$aTw) (= (apply$35$$35$0 (as head Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) x$35$$35$aTv) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) xs$35$$35$aTw) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) x$35$$35$aTv) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) false) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) xs$35$$35$aTw) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) x$35$$35$aTv) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) xs$35$$35$aTw) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) x$35$$35$aTv) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) false) (= lq_anf$36$$35$$35$7205759403792797823$35$$35$d167 (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTv) xs$35$$35$aTw)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797823$35$$35$d167) 0)) (and (= (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aTw) (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797824$35$$35$d168)) (= lq_anf$36$$35$$35$7205759403792797824$35$$35$d168 (apply$35$$35$0 (as Reverse.reverse Int) xs$35$$35$aTw)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797824$35$$35$d168) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797824$35$$35$d168) 0)) (and (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797825$35$$35$d169) 0) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797825$35$$35$d169) 0) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797825$35$$35$d169) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797825$35$$35$d169) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797825$35$$35$d169) false) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797825$35$$35$d169) true) (= lq_anf$36$$35$$35$7205759403792797825$35$$35$d169 (as GHC.Types.$91$$93$ Int)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797825$35$$35$d169) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797825$35$$35$d169) 0)) (and (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a) (+ 1 (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797825$35$$35$d169))) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a) (+ 1 (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797825$35$$35$d169))) (= (apply$35$$35$0 (as tail Int) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a) lq_anf$36$$35$$35$7205759403792797825$35$$35$d169) (= (apply$35$$35$0 (as head Int) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a) x$35$$35$aTv) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a) lq_anf$36$$35$$35$7205759403792797825$35$$35$d169) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a) x$35$$35$aTv) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a) false) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a) lq_anf$36$$35$$35$7205759403792797825$35$$35$d169) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a) x$35$$35$aTv) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a) lq_anf$36$$35$$35$7205759403792797825$35$$35$d169) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a) x$35$$35$aTv) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a) false) (= lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTv) lq_anf$36$$35$$35$7205759403792797825$35$$35$d169)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797826$35$$35$d16a) 0))))
(push 1)
(assert (not (= (apply$35$$35$0 (as Reverse.length Int) ds_d15N) (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$46))))
(check-sat)
; SMT Says: Unsat
(pop 1)
(pop 1)
(push 1)
(assert (and (and (>= (apply$35$$35$0 (as Reverse.length Int) ds_d15H) 0) (>= (apply$35$$35$0 (as len Int) ds_d15H) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) ys$35$$35$aTx) 0) (>= (apply$35$$35$0 (as len Int) ys$35$$35$aTx) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (= lq_anf$36$$35$$35$7205759403792797821$35$$35$d165 ds_d15H) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$62) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$62) 0) (= VV$35$$35$F$35$$35$62 xs$35$$35$aTz) (>= (apply$35$$35$0 (as Reverse.length Int) VV$35$$35$F$35$$35$62) 0) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$62) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (= lq_anf$36$$35$$35$7205759403792797821$35$$35$d165 ds_d15H) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aTz) 0) (>= (apply$35$$35$0 (as len Int) xs$35$$35$aTz) 0)) (and (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (= lq_anf$36$$35$$35$7205759403792797821$35$$35$d165 ds_d15H) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) (+ 1 (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aTz))) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) (+ 1 (apply$35$$35$0 (as len Int) xs$35$$35$aTz))) (= (apply$35$$35$0 (as tail Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) xs$35$$35$aTz) (= (apply$35$$35$0 (as head Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) x$35$$35$aTy) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) xs$35$$35$aTz) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) x$35$$35$aTy) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) false) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) xs$35$$35$aTz) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) x$35$$35$aTy) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) xs$35$$35$aTz) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) x$35$$35$aTy) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) false) (= lq_anf$36$$35$$35$7205759403792797821$35$$35$d165 (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTy) xs$35$$35$aTz)) (= lq_anf$36$$35$$35$7205759403792797821$35$$35$d165 (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTy) xs$35$$35$aTz)) (= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) (+ 1 (apply$35$$35$0 (as Reverse.length Int) xs$35$$35$aTz))) (= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) (+ 1 (apply$35$$35$0 (as len Int) xs$35$$35$aTz))) (= (apply$35$$35$0 (as tail Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) xs$35$$35$aTz) (= (apply$35$$35$0 (as head Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) x$35$$35$aTy) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) xs$35$$35$aTz) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) x$35$$35$aTy) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) false) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) xs$35$$35$aTz) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) x$35$$35$aTy) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$2 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) xs$35$$35$aTz) (= (apply$35$$35$0 (as lqdc$35$$35$$36$select$35$$35$GHC.Types.$58$$35$$35$1 Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) x$35$$35$aTy) (= (apply$35$$35$1 (as is$36$GHC.Types.$58$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) true) (= (apply$35$$35$1 (as is$36$GHC.Types.$91$$93$ Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) false) (= lq_anf$36$$35$$35$7205759403792797821$35$$35$d165 (apply$35$$35$0 (apply$35$$35$0 (as GHC.Types.$58$ Int) x$35$$35$aTy) xs$35$$35$aTz)) (>= (apply$35$$35$0 (as Reverse.length Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0) (>= (apply$35$$35$0 (as len Int) lq_anf$36$$35$$35$7205759403792797821$35$$35$d165) 0))))
(push 1)
(assert (not (and (< (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$62) (apply$35$$35$0 (as len Int) ds_d15H)) (>= (apply$35$$35$0 (as len Int) VV$35$$35$F$35$$35$62) 0))))
(check-sat)
; SMT Says: Unsat
(pop 1)
(pop 1)
(exit)