(benchmark ttt2
:logic QF_NIA
:status unknown
:extrafuns ((x4 Int)
            (x6 Int)
            (x13 Int)
            (x3 Int)
            (x10 Int)
            (x0 Int)
            (x9 Int)
            (x11 Int)
            (x1 Int)
            (x8 Int)
            (x5 Int)
            (x12 Int)
            )
:assumption (>= x4 0)
:assumption (>= x6 0)
:assumption (>= x13 0)
:assumption (>= x3 0)
:assumption (>= x10 0)
:assumption (>= x0 0)
:assumption (>= x9 0)
:assumption (>= x11 0)
:assumption (>= x1 0)
:assumption (>= x8 0)
:assumption (>= x5 0)
:assumption (>= x12 0)
:assumption (>= (+ (+ x0 (+ (+ x0 (+ x5 (* x3 x6))) (* x3 (+ x1 (* x4 x6))))) (+ x10 (* x8 x11))) 0)
:assumption (>= (+ (+ x1 (* x4 (+ x1 (* x4 x6)))) (* x9 x11)) 0)
:assumption (>= (+ x8 (* x3 x9)) 0)
:assumption (>= (* x4 x9) 1) 
:assumption (>= (+ (+ x0 (+ (+ x0 (+ x5 (* x3 x6))) (* x3 (+ x1 (* x4 x6))))) (+ (+ x0 (+ x12 (* x3 x13))) (* x8 (+ x1 (* x4 x13))))) (+ (+ x0 (+ x12 (* x3 x13))) (+ (+ x0 (+ (+ x0 (+ 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 (>= (+ x8 (* x3 x9)) (+ (+ x8 (* x3 x9)) (* x8 (* x4 x9))))
:assumption (>= (* x4 x9) (* x9 (* x4 x9)))
:assumption (> (+ (+ x0 (+ (+ x0 (+ x5 (* x3 x6))) (* x3 (+ x1 (* x4 x6))))) (+ x10 (* x8 x11))) 0)
:assumption (>= (+ (+ x0 (+ (+ x0 (+ x5 (* x3 x6))) (* x3 (+ x1 (* x4 x6))))) (+ x10 (* x8 x11))) 0)
:assumption (>= (+ (+ x1 (* x4 (+ x1 (* x4 x6)))) (* x9 x11)) 0)
:assumption (>= (+ x8 (* x3 x9)) 0)
:assumption (>= (* x4 x9) 1)
:assumption (> (+ (+ x0 (+ (+ x0 (+ x5 (* x3 x6))) (* x3 (+ x1 (* x4 x6))))) (+ (+ x0 (+ x12 (* x3 x13))) (* x8 (+ x1 (* x4 x13))))) (+ (+ x0 (+ x12 (* x3 x13))) (+ (+ x0 (+ (* 1 (+ x0 (+ x5 (* x3 x6)))) (* x3 (+ x1 (* x4 x6))))) (* x8 (+ x1 (* x4 (+ x1 (* x4 x6))))))))
:assumption (>= (+ (+ x0 (+ (+ x0 (+ x5 (* x3 x6))) (* x3 (+ x1 (* x4 x6))))) (+ (+ x0 (+ x12 (* x3 x13))) (* x8 (+ x1 (* x4 x13))))) (+ (+ x0 (+ x12 (* x3 x13))) (+ (+ x0 (+ (* 1 (+ x0 (+ 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 (>= (+ x8 (* x3 x9)) (+ (+ x8 (* x3 x9)) (* x8 (* x4 x9))))
:assumption (>= (* x4 x9) (* x9 (* x4 x9)))
:assumption (>= 1 x4)
:assumption (>= 1 x9)
:formula (true)
)