(benchmark mathsat
:logic QF_UFLIA
:extrafuns ((s_count Int Int))
:extrafuns ((fmt1 Int))
:extrafuns ((fmt_length Int))
:status unsat
:formula
(let (?n1 0)
(let (?n2 6)
(let (?n3 (s_count ?n2))
(flet ($n4 (= ?n1 ?n3))
(let (?n5 5)
(let (?n6 (s_count ?n5))
(flet ($n7 (= ?n1 ?n6))
(let (?n8 4)
(let (?n9 (s_count ?n8))
(flet ($n10 (= ?n1 ?n9))
(let (?n11 3)
(let (?n12 (s_count ?n11))
(flet ($n13 (= ?n1 ?n12))
(let (?n14 1)
(let (?n15 (s_count ?n1))
(flet ($n16 (= ?n14 ?n15))
(let (?n17 (s_count ?n14))
(flet ($n18 (= ?n1 ?n17))
(flet ($n19 (and $n16 $n18))
(let (?n20 2)
(let (?n21 (s_count ?n20))
(flet ($n22 (= ?n1 ?n21))
(flet ($n23 (and $n19 $n22))
(flet ($n24 (and $n13 $n23))
(flet ($n25 (and $n10 $n24))
(flet ($n26 (and $n7 $n25))
(flet ($n27 (and $n4 $n26))
(let (?n28 9)
(flet ($n29 (= ?n28 fmt_length))
(flet ($n30 (> fmt1 ?n14))
(flet ($n31 (< fmt1 fmt_length))
(flet ($n32 (and $n30 $n31))
(let (?n33 (- fmt1 ?n20))
(let (?n34 (s_count ?n33))
(let (?n35 (+ ?n14 ?n34))
(flet ($n36 (= ?n1 ?n35))
(flet ($n37 (and $n32 $n36))
(flet ($n38 (and $n29 $n37))
(flet ($n39 (and $n27 $n38))
$n39
))))))))))))))))))))))))))))))))))))))))