(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)
)