(benchmark ttt2
:logic QF_NIA
:status unknown
:extrafuns ((x4 Int)
            (x6 Int)
            (x13 Int)
            (x3 Int)
            (x10 Int)
            (x0 Int)
            (x2 Int)
            (x9 Int)
            (x11 Int)
            (x1 Int)
            (x8 Int)
            (x5 Int)
            (x12 Int)
            (x7 Int))
:assumption (>= x4 0)
:assumption (>= x6 0)
:assumption (>= x13 0)
:assumption (>= x3 0)
:assumption (>= x10 0)
:assumption (>= x0 0)
:assumption (>= x2 0)
:assumption (>= x9 0)
:assumption (>= x11 0)
:assumption (>= x1 0)
:assumption (>= x8 0)
:assumption (>= x5 0)
:assumption (>= x12 0)
:assumption (>= x7 0)
:assumption (>= (+ (+ x0 (+ (* x2 (+ x0 (+ (* x2 x5) (* x3 x6)))) (* x3 (+ x1 (* x4 x6))))) (+ (* x7 x10) (* x8 x11))) 0)
:assumption (>= (+ (+ x1 (* x4 (+ x1 (* x4 x6)))) (* x9 x11)) 0)
:assumption (>= (* x2 x7) 1)
:assumption (>= (+ (* x2 x8) (* x3 x9)) 0)
:assumption (>= (* x4 x9) 1) 
:assumption (>= (+ (+ x0 (+ (* x2 (+ x0 (+ (* x2 x5) (* x3 x6)))) (* x3 (+ x1 (* x4 x6))))) (+ (* x7 (+ x0 (+ (* x2 x12) (* x3 x13)))) (* x8 (+ x1 (* x4 x13))))) (+ (+ x0 (+ (* x2 x12) (* x3 x13))) (+ (* x7 (+ x0 (+ (* x2 (+ x0 (+ (* x2 x5) (* x3 x6)))) (* x3 (+ x1 (* x4 x6)))))) (* x8 (+ x1 (* x4 (+ x1 (* x4 x6))))))))
:assumption (>= (+ (+ x1 (* x4 (+ x1 (* x4 x6)))) (* x9 (+ x1 (* x4 x13)))) (+ (+ x1 (* x4 x13)) (* x9 (+ x1 (* x4 (+ x1 (* x4 x6)))))))
:assumption (>= (* x2 x7) (* x7 (* x2 x7)))
:assumption (>= (+ (* x2 x8) (* x3 x9)) (+ (* x7 (+ (* x2 x8) (* x3 x9))) (* x8 (* x4 x9))))
:assumption (>= (* x4 x9) (* x9 (* x4 x9)))
:assumption (> (+ (+ x0 (+ (* x2 (+ x0 (+ (* x2 x5) (* x3 x6)))) (* x3 (+ x1 (* x4 x6))))) (+ (* x7 x10) (* x8 x11))) 0)
:assumption (>= (+ (+ x0 (+ (* x2 (+ x0 (+ (* x2 x5) (* x3 x6)))) (* x3 (+ x1 (* x4 x6))))) (+ (* x7 x10) (* x8 x11))) 0)
:assumption (>= (+ (+ x1 (* x4 (+ x1 (* x4 x6)))) (* x9 x11)) 0)
:assumption (>= (* x2 x7) 1)
:assumption (>= (+ (* x2 x8) (* x3 x9)) 0)
:assumption (>= (* x4 x9) 1)
:assumption (> (+ (+ x0 (+ (* x2 (+ x0 (+ (* x2 x5) (* x3 x6)))) (* x3 (+ x1 (* x4 x6))))) (+ (* x7 (+ x0 (+ (* x2 x12) (* x3 x13)))) (* x8 (+ x1 (* x4 x13))))) (+ (+ x0 (+ (* x2 x12) (* x3 x13))) (+ (* x7 (+ x0 (+ (* x2 (+ x0 (+ (* x2 x5) (* x3 x6)))) (* x3 (+ x1 (* x4 x6)))))) (* x8 (+ x1 (* x4 (+ x1 (* x4 x6))))))))
:assumption (>= (+ (+ x0 (+ (* x2 (+ x0 (+ (* x2 x5) (* x3 x6)))) (* x3 (+ x1 (* x4 x6))))) (+ (* x7 (+ x0 (+ (* x2 x12) (* x3 x13)))) (* x8 (+ x1 (* x4 x13))))) (+ (+ x0 (+ (* x2 x12) (* x3 x13))) (+ (* x7 (+ x0 (+ (* x2 (+ x0 (+ (* x2 x5) (* x3 x6)))) (* x3 (+ x1 (* x4 x6)))))) (* x8 (+ x1 (* x4 (+ x1 (* x4 x6))))))))
:assumption (>= (+ (+ x1 (* x4 (+ x1 (* x4 x6)))) (* x9 (+ x1 (* x4 x13)))) (+ (+ x1 (* x4 x13)) (* x9 (+ x1 (* x4 (+ x1 (* x4 x6)))))))
:assumption (>= (* x2 x7) (* x7 (* x2 x7)))
:assumption (>= (+ (* x2 x8) (* x3 x9)) (+ (* x7 (+ (* x2 x8) (* x3 x9))) (* x8 (* x4 x9))))
:assumption (>= (* x4 x9) (* x9 (* x4 x9)))
:assumption (>= x2 1)
:assumption (>= x7 1)
:assumption (>= 1 x2)
:assumption (>= 1 x4)
:assumption (>= 1 x7)
:assumption (>= 1 x9)
:formula (true)
)