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