(benchmark B_
:logic QF_UFLIA
:extrafuns ((format Int Int))
:extrafuns ((arg1 Int))
:extrafuns ((fmt1 Int))
:extrafuns ((s_count Int Int))
:extrafuns ((fmt0 Int))
:extrafuns ((x_count Int Int))
:status sat
:formula
(flet ($n1 true)
(let (?n2 1)
(let (?n3 (~ ?n2))
(let (?n4 (* ?n3 fmt1))
(let (?n5 (+ ?n4 fmt0))
(let (?n6 8)
(let (?n7 (~ ?n6))
(flet ($n8 (>= ?n5 ?n7))
(let (?n9 6)
(let (?n10 (x_count ?n9))
(let (?n11 7)
(let (?n12 (x_count ?n11))
(let (?n13 (* ?n3 ?n12))
(let (?n14 (+ ?n10 ?n13))
(let (?n15 0)
(flet ($n16 (>= ?n14 ?n15))
(flet ($n17 (>= fmt1 ?n11))
(flet ($n18 (<= arg1 ?n9))
(let (?n19 2)
(let (?n20 (~ ?n19))
(let (?n21 (* ?n3 fmt0))
(let (?n22 (+ fmt1 ?n20 ?n21))
(let (?n23 (s_count ?n22))
(let (?n24 5)
(let (?n25 (s_count ?n24))
(let (?n26 (* ?n3 ?n25))
(let (?n27 (+ ?n23 ?n26))
(flet ($n28 (= ?n15 ?n27))
(flet ($n29 (not $n28))
(let (?n30 (~ ?n11))
(flet ($n31 (<= ?n5 ?n30))
(flet ($n32 false)
(let (?n33 (+ arg1 ?n21))
(flet ($n34 (<= ?n33 ?n2))
(let (?n35 (+ ?n4 arg1))
(flet ($n36 (<= ?n35 ?n15))
(flet ($n37 (or $n32 $n32 $n34 $n36))
(let (?n38 (x_count ?n2))
(flet ($n39 (>= ?n38 ?n15))
(let (?n40 (format ?n11))
(flet ($n41 (<= ?n40 ?n15))
(let (?n42 (x_count ?n22))
(let (?n43 (+ ?n13 ?n42))
(flet ($n44 (= ?n15 ?n43))
(let (?n45 (s_count ?n9))
(let (?n46 (* ?n3 ?n45))
(let (?n47 (+ ?n23 ?n46))
(flet ($n48 (= ?n15 ?n47))
(flet ($n49 (or $n32 $n32 $n32 $n32 $n32 $n39 $n44 $n48))
(let (?n50 (+ ?n2 fmt1))
(let (?n51 (format ?n50))
(flet ($n52 (>= ?n51 ?n15))
(let (?n53 4)
(let (?n54 (format ?n53))
(flet ($n55 (>= ?n54 ?n15))
(let (?n56 9)
(let (?n57 (format ?n56))
(flet ($n58 (<= ?n57 ?n15))
(let (?n59 (format fmt1))
(flet ($n60 (>= ?n59 ?n15))
(let (?n61 12)
(let (?n62 (format ?n61))
(flet ($n63 (>= ?n62 ?n15))
(let (?n64 (format arg1))
(flet ($n65 (= ?n15 ?n64))
(flet ($n66 (and $n1 $n8 $n16 $n17 $n18 $n29 $n31 $n37 $n39 $n41 $n49 $n52 $n55 $n58 $n60 $n63 $n65))
$n66
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))