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