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