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