cvc4 assumptions 72:
Y0 : INT;
X_ni : INT;
Y2 : INT;
X_nj : INT;
Y3 : INT;
Y1 : INT;
Y6 : [INT, ARRAY INT OF ([INT, ARRAY INT OF (REAL)])];
Y7 : [INT, ARRAY INT OF ([INT, ARRAY INT OF (REAL)])];
Y5 : [INT, ARRAY INT OF ([INT, ARRAY INT OF (REAL)])];
Y4 : [INT, ARRAY INT OF ([INT, ARRAY INT OF (REAL)])];
X_uin : [INT, ARRAY INT OF ([INT, ARRAY INT OF (REAL)])];
((EXISTS (t0 : INT, t1 : INT) : (((0) = ((t1) + (-1))) AND (((Y0) = (t0)*(2) + (t1)) AND (((t1) >= 0) AND ((t1) < (2))))))) AND (((0) = ((X_ni) + ((-1) * (Y2)) + (-1)))) AND (((0) = ((X_nj) + ((-1) * (Y3)) + (-1)))) AND (((0) = ((Y0) + ((-1) * (Y2)) + (1)))) AND (((0) = ((Y1) + ((-1) * (Y3)) + (1)))) AND (FORALL (_cc_bv_10__28 : INT) : (FORALL (_cc_bv_11__28 : INT) : ((((0) = (((((Y6).1)[_cc_bv_11__28]).1)[_cc_bv_10__28]))) OR ((0)  <=  ((X_ni) + ((-1) * (_cc_bv_11__28)) + (-2)))))) AND (FORALL (_cc_bv_10__29 : INT) : (FORALL (_cc_bv_11__29 : INT) : ((((0) = (((((Y6).1)[_cc_bv_11__29]).1)[_cc_bv_10__29]))) OR ((0)  <=  ((_cc_bv_11__29) + (-1)))))) AND (FORALL (_cc_bv_10__30 : INT) : ((FORALL (_cc_bv_11__30 : INT) : (((0) = (((((Y6).1)[_cc_bv_11__30]).1)[_cc_bv_10__30])))) OR ((0)  <=  ((X_nj) + ((-1) * (_cc_bv_10__30)) + (-2))))) AND (FORALL (_cc_bv_10__31 : INT) : ((FORALL (_cc_bv_11__31 : INT) : (((0) = (((((Y6).1)[_cc_bv_11__31]).1)[_cc_bv_10__31])))) OR ((0)  <=  ((_cc_bv_10__31) + (-1))))) AND (FORALL (_cc_bv_14__13 : INT) : (FORALL (_cc_bv_15__13 : INT) : ((((0) = ((Y0) + ((-1) * (_cc_bv_15__13))))) OR (((0) = ((((((Y6).1)[_cc_bv_15__13]).1)[_cc_bv_14__13]) + ((-1) * (((((Y7).1)[_cc_bv_15__13]).1)[_cc_bv_14__13])))))))) AND (FORALL (_cc_bv_14__14 : INT) : ((FORALL (_cc_bv_15__14 : INT) : (((0) = ((((((Y6).1)[_cc_bv_15__14]).1)[_cc_bv_14__14]) + ((-1) * (((((Y7).1)[_cc_bv_15__14]).1)[_cc_bv_14__14])))))) OR ((0)  <=  ((X_nj) + ((-1) * (_cc_bv_14__14)) + (-2))))) AND (FORALL (_cc_bv_14__15 : INT) : ((FORALL (_cc_bv_15__15 : INT) : (((0) = ((((((Y6).1)[_cc_bv_15__15]).1)[_cc_bv_14__15]) + ((-1) * (((((Y7).1)[_cc_bv_15__15]).1)[_cc_bv_14__15])))))) OR ((0)  <=  ((_cc_bv_14__15) + (-1))))) AND (FORALL (_cc_bv_18__3 : INT) : (FORALL (_cc_bv_19__3 : INT) : ((((0) = ((((((Y5).1)[_cc_bv_19__3]).1)[_cc_bv_18__3]) + ((-1) * (((((Y7).1)[_cc_bv_19__3]).1)[_cc_bv_18__3]))))) OR ((0)  <=  ((X_ni) + ((-1) * (_cc_bv_19__3)) + (-2)))))) AND (FORALL (_cc_bv_18__4 : INT) : (FORALL (_cc_bv_19__4 : INT) : ((((0) = ((((((Y5).1)[_cc_bv_19__4]).1)[_cc_bv_18__4]) + ((-1) * (((((Y7).1)[_cc_bv_19__4]).1)[_cc_bv_18__4]))))) OR ((0)  <=  ((_cc_bv_19__4) + (-1)))))) AND (FORALL (_cc_bv_18__5 : INT) : ((((0) = ((Y1) + ((-1) * (_cc_bv_18__5))))) OR (FORALL (_cc_bv_19__5 : INT) : (((0) = ((((((Y5).1)[_cc_bv_19__5]).1)[_cc_bv_18__5]) + ((-1) * (((((Y7).1)[_cc_bv_19__5]).1)[_cc_bv_18__5])))))))) AND (FORALL (i__27 : INT) : ((((0) = (((((Y4).1)[i__27]).1)[(X_nj) + (-1)]))) OR (((X_ni) + ((-1) * (i__27)))  <=  (0)) OR (((i__27) + (1))  <=  (0)))) AND (FORALL (i__28 : INT) : ((((0) = (((((Y4).1)[i__28]).1)[0]))) OR (((X_ni) + ((-1) * (i__28)))  <=  (0)) OR (((i__28) + (1))  <=  (0)))) AND (FORALL (i__29 : INT) : ((FORALL (j__27 : INT) : ((((0) = (((((((X_uin).1)[i__29]).1)[j__27])^2) + ((-1) * (((((Y4).1)[i__29]).1)[j__27]))))) OR (((X_nj) + ((-1) * (j__27)) + (-1))  <=  (0)) OR ((j__27)  <=  (0)))) OR (((X_ni) + ((-1) * (i__29)) + (-1))  <=  (0)) OR ((i__29)  <=  (0)))) AND (FORALL (j__28 : INT) : ((((0) = (((((Y4).1)[(X_ni) + (-1)]).1)[j__28]))) OR (((X_nj) + ((-1) * (j__28)))  <=  (0)) OR (((j__28) + (1))  <=  (0)))) AND (FORALL (j__29 : INT) : ((((0) = (((((Y4).1)[0]).1)[j__29]))) OR (((X_nj) + ((-1) * (j__29)))  <=  (0)) OR (((j__29) + (1))  <=  (0)))) AND (FORALL (k__26 : INT) : ((FORALL (t__28 : INT) : ((((0) = (((((((X_uin).1)[t__28]).1)[k__26])^2) + ((-1) * (((((Y6).1)[t__28]).1)[k__26]))))) OR (((Y0) + ((-1) * (t__28)))  <=  (0)) OR ((t__28)  <=  (0)))) OR ((k__26)  <=  (0)) OR ((0)  <=  ((IF ((0)  <=  ((t3) + (-1))) THEN ((t3) + (-1)) ELSE ((-1) * ((t3) + (-1))) ENDIF) + ((-1) * (X_nj)) + (k__26) + (1))))) AND (FORALL (t__26 : INT) : ((((0) = (((((((X_uin).1)[Y0]).1)[t__26])^2) + ((-1) * (((((Y7).1)[Y0]).1)[t__26]))))) OR (((Y3) + ((-1) * (t__26)))  <=  (0)) OR ((t__26)  <=  (0)))) AND (FORALL (t__27 : INT) : ((((0) = (((((((X_uin).1)[t__27]).1)[Y1])^2) + ((-1) * (((((Y5).1)[t__27]).1)[Y1]))))) OR (((Y2) + ((-1) * (t__27)))  <=  (0)) OR ((t__27)  <=  (0)))) AND ((0)  <=  ((X_ni) + (-4))) AND ((0)  <=  ((X_nj) + (-3))) AND ((0)  <=  ((Y0) + (-1))) AND ((0)  <=  ((Y2) + (-1))) AND ((0)  <=  ((Y3) + (-1))) AND ((((Y0) + (-1))  <=  (0)) OR (NOT((EXISTS (t4 : INT, t5 : INT) : (((0) = (t5)) AND (((Y1) = (t4)*(2) + (t5)) AND (((t5) >= 0) AND ((t5) < (2)))))))))

cvc4 predicate   72:
FORALL (i__30 : INT) : ((FORALL (j__30 : INT) : ((((0) = (((((((Y5).1) WITH [Y0] := ((X_nj,((((Y5).1)[Y0]).1) WITH [Y1] := ((((((X_uin).1)[Y0]).1)[Y1])^2))))[i__30]).1)[j__30]) + ((-1) * (((((Y4).1)[i__30]).1)[j__30]))))) OR (((X_nj) + ((-1) * (j__30)))  <=  (0)) OR (((j__30) + (1))  <=  (0)))) OR (((X_ni) + ((-1) * (i__30)))  <=  (0)) OR (((i__30) + (1))  <=  (0)))

cvc4 result      72: MAYBE

z3 assumptions 73:
(declare-const Y0 Int)
(declare-const X_ni Int)
(declare-const Y2 Int)
(declare-const X_nj Int)
(declare-const Y3 Int)
(declare-const Y1 Int)
(declare-datatypes (T) ((BigArray (mk-BigArray (bigArray-len Int) (bigArray-val (Array Int T))))))
(declare-const Y6 (BigArray (BigArray Real)))
(declare-const Y7 (BigArray (BigArray Real)))
(declare-const Y5 (BigArray (BigArray Real)))
(declare-const Y4 (BigArray (BigArray Real)))
(declare-const X_uin (BigArray (BigArray Real)))
(let ((t0 (= 0 (+ (mod Y0 2) -1))) ) (let ((t1 (= 0 (+ X_ni (* -1 Y2) -1))) ) (let ((t2 (= 0 (+ X_nj (* -1 Y3) -1))) ) (let ((t3 (= 0 (+ Y0 (* -1 Y2) 1))) ) (let ((t4 (= 0 (+ Y1 (* -1 Y3) 1))) ) (let ((t5 (forall ((_cc_bv_10__28 Int)) (forall ((_cc_bv_11__28 Int)) (or (= 0 (select (bigArray-val (select (bigArray-val Y6) _cc_bv_11__28)) _cc_bv_10__28)) (<= 0 (+ X_ni (* -1 _cc_bv_11__28) -2)))))) ) (let ((t6 (forall ((_cc_bv_10__29 Int)) (forall ((_cc_bv_11__29 Int)) (or (= 0 (select (bigArray-val (select (bigArray-val Y6) _cc_bv_11__29)) _cc_bv_10__29)) (<= 0 (+ _cc_bv_11__29 -1)))))) ) (let ((t7 (forall ((_cc_bv_10__30 Int)) (or (forall ((_cc_bv_11__30 Int)) (= 0 (select (bigArray-val (select (bigArray-val Y6) _cc_bv_11__30)) _cc_bv_10__30))) (<= 0 (+ X_nj (* -1 _cc_bv_10__30) -2))))) ) (let ((t8 (forall ((_cc_bv_10__31 Int)) (or (forall ((_cc_bv_11__31 Int)) (= 0 (select (bigArray-val (select (bigArray-val Y6) _cc_bv_11__31)) _cc_bv_10__31))) (<= 0 (+ _cc_bv_10__31 -1))))) ) (let ((t9 (forall ((_cc_bv_14__13 Int)) (forall ((_cc_bv_15__13 Int)) (or (= 0 (+ Y0 (* -1 _cc_bv_15__13))) (= 0 (+ (select (bigArray-val (select (bigArray-val Y6) _cc_bv_15__13)) _cc_bv_14__13) (* -1 (select (bigArray-val (select (bigArray-val Y7) _cc_bv_15__13)) _cc_bv_14__13)))))))) ) (let ((t10 (forall ((_cc_bv_14__14 Int)) (or (forall ((_cc_bv_15__14 Int)) (= 0 (+ (select (bigArray-val (select (bigArray-val Y6) _cc_bv_15__14)) _cc_bv_14__14) (* -1 (select (bigArray-val (select (bigArray-val Y7) _cc_bv_15__14)) _cc_bv_14__14))))) (<= 0 (+ X_nj (* -1 _cc_bv_14__14) -2))))) ) (let ((t11 (forall ((_cc_bv_14__15 Int)) (or (forall ((_cc_bv_15__15 Int)) (= 0 (+ (select (bigArray-val (select (bigArray-val Y6) _cc_bv_15__15)) _cc_bv_14__15) (* -1 (select (bigArray-val (select (bigArray-val Y7) _cc_bv_15__15)) _cc_bv_14__15))))) (<= 0 (+ _cc_bv_14__15 -1))))) ) (let ((t12 (forall ((_cc_bv_18__3 Int)) (forall ((_cc_bv_19__3 Int)) (or (= 0 (+ (select (bigArray-val (select (bigArray-val Y5) _cc_bv_19__3)) _cc_bv_18__3) (* -1 (select (bigArray-val (select (bigArray-val Y7) _cc_bv_19__3)) _cc_bv_18__3)))) (<= 0 (+ X_ni (* -1 _cc_bv_19__3) -2)))))) ) (let ((t13 (forall ((_cc_bv_18__4 Int)) (forall ((_cc_bv_19__4 Int)) (or (= 0 (+ (select (bigArray-val (select (bigArray-val Y5) _cc_bv_19__4)) _cc_bv_18__4) (* -1 (select (bigArray-val (select (bigArray-val Y7) _cc_bv_19__4)) _cc_bv_18__4)))) (<= 0 (+ _cc_bv_19__4 -1)))))) ) (let ((t14 (forall ((_cc_bv_18__5 Int)) (or (= 0 (+ Y1 (* -1 _cc_bv_18__5))) (forall ((_cc_bv_19__5 Int)) (= 0 (+ (select (bigArray-val (select (bigArray-val Y5) _cc_bv_19__5)) _cc_bv_18__5) (* -1 (select (bigArray-val (select (bigArray-val Y7) _cc_bv_19__5)) _cc_bv_18__5)))))))) ) (let ((t15 (forall ((i__27 Int)) (or (= 0 (select (bigArray-val (select (bigArray-val Y4) i__27)) (+ X_nj -1))) (<= (+ X_ni (* -1 i__27)) 0) (<= (+ i__27 1) 0)))) ) (let ((t16 (forall ((i__28 Int)) (or (= 0 (select (bigArray-val (select (bigArray-val Y4) i__28)) 0)) (<= (+ X_ni (* -1 i__28)) 0) (<= (+ i__28 1) 0)))) ) (let ((t17 (forall ((i__29 Int)) (or (forall ((j__27 Int)) (or (= 0 (+ (^ (select (bigArray-val (select (bigArray-val X_uin) i__29)) j__27) 2) (* -1 (select (bigArray-val (select (bigArray-val Y4) i__29)) j__27)))) (<= (+ X_nj (* -1 j__27) -1) 0) (<= j__27 0))) (<= (+ X_ni (* -1 i__29) -1) 0) (<= i__29 0)))) ) (let ((t18 (forall ((j__28 Int)) (or (= 0 (select (bigArray-val (select (bigArray-val Y4) (+ X_ni -1))) j__28)) (<= (+ X_nj (* -1 j__28)) 0) (<= (+ j__28 1) 0)))) ) (let ((t19 (forall ((j__29 Int)) (or (= 0 (select (bigArray-val (select (bigArray-val Y4) 0)) j__29)) (<= (+ X_nj (* -1 j__29)) 0) (<= (+ j__29 1) 0)))) ) (let ((t20 (forall ((k__26 Int)) (or (forall ((t__28 Int)) (or (= 0 (+ (^ (select (bigArray-val (select (bigArray-val X_uin) t__28)) k__26) 2) (* -1 (select (bigArray-val (select (bigArray-val Y6) t__28)) k__26)))) (<= (+ Y0 (* -1 t__28)) 0) (<= t__28 0))) (<= k__26 0) (<= 0 (+ (ite (<= 0 (+ (mod (+ X_nj -3) 2) -1)) (+ (mod (+ X_nj -3) 2) -1) (* -1 (+ (mod (+ X_nj -3) 2) -1))) (* -1 X_nj) k__26 1))))) ) (let ((t21 (forall ((t__26 Int)) (or (= 0 (+ (^ (select (bigArray-val (select (bigArray-val X_uin) Y0)) t__26) 2) (* -1 (select (bigArray-val (select (bigArray-val Y7) Y0)) t__26)))) (<= (+ Y3 (* -1 t__26)) 0) (<= t__26 0)))) ) (let ((t22 (forall ((t__27 Int)) (or (= 0 (+ (^ (select (bigArray-val (select (bigArray-val X_uin) t__27)) Y1) 2) (* -1 (select (bigArray-val (select (bigArray-val Y5) t__27)) Y1)))) (<= (+ Y2 (* -1 t__27)) 0) (<= t__27 0)))) ) (let ((t23 (or (<= (+ Y0 -1) 0) (not (= 0 (mod Y1 2))))) ) (let ((t24 (and t0 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 t16 t17 t18 t19 t20 t21 t22 (<= 0 (+ X_ni -4)) (<= 0 (+ X_nj -3)) (<= 0 (+ Y0 -1)) (<= 0 (+ Y2 -1)) (<= 0 (+ Y3 -1)) t23)) )  t24)))))))))))))))))))))))))

z3 predicate   73:
(declare-datatypes (T) ((BigArray (mk-BigArray (bigArray-len Int) (bigArray-val (Array Int T))))))
(forall ((i__30 Int)) (or (forall ((j__30 Int)) (or (= 0 (+ (select (bigArray-val (select (store (bigArray-val Y5) Y0 (mk-BigArray X_nj (store (bigArray-val (select (bigArray-val Y5) Y0)) Y1 (^ (select (bigArray-val (select (bigArray-val X_uin) Y0)) Y1) 2)))) i__30)) j__30) (* -1 (select (bigArray-val (select (bigArray-val Y4) i__30)) j__30)))) (<= (+ X_nj (* -1 j__30)) 0) (<= (+ j__30 1) 0))) (<= (+ X_ni (* -1 i__30)) 0) (<= (+ i__30 1) 0)))

z3 result      73: MAYBE

cvc3 assumptions 74:
Y0 : INT;
X_ni : INT;
Y2 : INT;
X_nj : INT;
Y3 : INT;
Y1 : INT;
Y6 : [INT, ARRAY INT OF ([INT, ARRAY INT OF (REAL)])];
Y7 : [INT, ARRAY INT OF ([INT, ARRAY INT OF (REAL)])];
Y5 : [INT, ARRAY INT OF ([INT, ARRAY INT OF (REAL)])];
Y4 : [INT, ARRAY INT OF ([INT, ARRAY INT OF (REAL)])];
X_uin : [INT, ARRAY INT OF ([INT, ARRAY INT OF (REAL)])];
((EXISTS (t0 : INT, t1 : INT) : (((0) = ((t1) + (-1))) AND (((Y0) = (t0)*(2) + (t1)) AND (((t1) >= 0) AND ((t1) < (2))))))) AND (((0) = ((X_ni) + ((-1) * (Y2)) + (-1)))) AND (((0) = ((X_nj) + ((-1) * (Y3)) + (-1)))) AND (((0) = ((Y0) + ((-1) * (Y2)) + (1)))) AND (((0) = ((Y1) + ((-1) * (Y3)) + (1)))) AND (FORALL (_cc_bv_10__28 : INT) : (FORALL (_cc_bv_11__28 : INT) : ((((0) = (((((Y6).1)[_cc_bv_11__28]).1)[_cc_bv_10__28]))) OR ((0)  <=  ((X_ni) + ((-1) * (_cc_bv_11__28)) + (-2)))))) AND (FORALL (_cc_bv_10__29 : INT) : (FORALL (_cc_bv_11__29 : INT) : ((((0) = (((((Y6).1)[_cc_bv_11__29]).1)[_cc_bv_10__29]))) OR ((0)  <=  ((_cc_bv_11__29) + (-1)))))) AND (FORALL (_cc_bv_10__30 : INT) : ((FORALL (_cc_bv_11__30 : INT) : (((0) = (((((Y6).1)[_cc_bv_11__30]).1)[_cc_bv_10__30])))) OR ((0)  <=  ((X_nj) + ((-1) * (_cc_bv_10__30)) + (-2))))) AND (FORALL (_cc_bv_10__31 : INT) : ((FORALL (_cc_bv_11__31 : INT) : (((0) = (((((Y6).1)[_cc_bv_11__31]).1)[_cc_bv_10__31])))) OR ((0)  <=  ((_cc_bv_10__31) + (-1))))) AND (FORALL (_cc_bv_14__13 : INT) : (FORALL (_cc_bv_15__13 : INT) : ((((0) = ((Y0) + ((-1) * (_cc_bv_15__13))))) OR (((0) = ((((((Y6).1)[_cc_bv_15__13]).1)[_cc_bv_14__13]) + ((-1) * (((((Y7).1)[_cc_bv_15__13]).1)[_cc_bv_14__13])))))))) AND (FORALL (_cc_bv_14__14 : INT) : ((FORALL (_cc_bv_15__14 : INT) : (((0) = ((((((Y6).1)[_cc_bv_15__14]).1)[_cc_bv_14__14]) + ((-1) * (((((Y7).1)[_cc_bv_15__14]).1)[_cc_bv_14__14])))))) OR ((0)  <=  ((X_nj) + ((-1) * (_cc_bv_14__14)) + (-2))))) AND (FORALL (_cc_bv_14__15 : INT) : ((FORALL (_cc_bv_15__15 : INT) : (((0) = ((((((Y6).1)[_cc_bv_15__15]).1)[_cc_bv_14__15]) + ((-1) * (((((Y7).1)[_cc_bv_15__15]).1)[_cc_bv_14__15])))))) OR ((0)  <=  ((_cc_bv_14__15) + (-1))))) AND (FORALL (_cc_bv_18__3 : INT) : (FORALL (_cc_bv_19__3 : INT) : ((((0) = ((((((Y5).1)[_cc_bv_19__3]).1)[_cc_bv_18__3]) + ((-1) * (((((Y7).1)[_cc_bv_19__3]).1)[_cc_bv_18__3]))))) OR ((0)  <=  ((X_ni) + ((-1) * (_cc_bv_19__3)) + (-2)))))) AND (FORALL (_cc_bv_18__4 : INT) : (FORALL (_cc_bv_19__4 : INT) : ((((0) = ((((((Y5).1)[_cc_bv_19__4]).1)[_cc_bv_18__4]) + ((-1) * (((((Y7).1)[_cc_bv_19__4]).1)[_cc_bv_18__4]))))) OR ((0)  <=  ((_cc_bv_19__4) + (-1)))))) AND (FORALL (_cc_bv_18__5 : INT) : ((((0) = ((Y1) + ((-1) * (_cc_bv_18__5))))) OR (FORALL (_cc_bv_19__5 : INT) : (((0) = ((((((Y5).1)[_cc_bv_19__5]).1)[_cc_bv_18__5]) + ((-1) * (((((Y7).1)[_cc_bv_19__5]).1)[_cc_bv_18__5])))))))) AND (FORALL (i__27 : INT) : ((((0) = (((((Y4).1)[i__27]).1)[(X_nj) + (-1)]))) OR (((X_ni) + ((-1) * (i__27)))  <=  (0)) OR (((i__27) + (1))  <=  (0)))) AND (FORALL (i__28 : INT) : ((((0) = (((((Y4).1)[i__28]).1)[0]))) OR (((X_ni) + ((-1) * (i__28)))  <=  (0)) OR (((i__28) + (1))  <=  (0)))) AND (FORALL (i__29 : INT) : ((FORALL (j__27 : INT) : ((((0) = (((((((X_uin).1)[i__29]).1)[j__27])^2) + ((-1) * (((((Y4).1)[i__29]).1)[j__27]))))) OR (((X_nj) + ((-1) * (j__27)) + (-1))  <=  (0)) OR ((j__27)  <=  (0)))) OR (((X_ni) + ((-1) * (i__29)) + (-1))  <=  (0)) OR ((i__29)  <=  (0)))) AND (FORALL (j__28 : INT) : ((((0) = (((((Y4).1)[(X_ni) + (-1)]).1)[j__28]))) OR (((X_nj) + ((-1) * (j__28)))  <=  (0)) OR (((j__28) + (1))  <=  (0)))) AND (FORALL (j__29 : INT) : ((((0) = (((((Y4).1)[0]).1)[j__29]))) OR (((X_nj) + ((-1) * (j__29)))  <=  (0)) OR (((j__29) + (1))  <=  (0)))) AND (FORALL (k__26 : INT) : ((FORALL (t__28 : INT) : ((((0) = (((((((X_uin).1)[t__28]).1)[k__26])^2) + ((-1) * (((((Y6).1)[t__28]).1)[k__26]))))) OR (((Y0) + ((-1) * (t__28)))  <=  (0)) OR ((t__28)  <=  (0)))) OR ((k__26)  <=  (0)) OR ((0)  <=  ((IF ((0)  <=  ((t3) + (-1))) THEN ((t3) + (-1)) ELSE ((-1) * ((t3) + (-1))) ENDIF) + ((-1) * (X_nj)) + (k__26) + (1))))) AND (FORALL (t__26 : INT) : ((((0) = (((((((X_uin).1)[Y0]).1)[t__26])^2) + ((-1) * (((((Y7).1)[Y0]).1)[t__26]))))) OR (((Y3) + ((-1) * (t__26)))  <=  (0)) OR ((t__26)  <=  (0)))) AND (FORALL (t__27 : INT) : ((((0) = (((((((X_uin).1)[t__27]).1)[Y1])^2) + ((-1) * (((((Y5).1)[t__27]).1)[Y1]))))) OR (((Y2) + ((-1) * (t__27)))  <=  (0)) OR ((t__27)  <=  (0)))) AND ((0)  <=  ((X_ni) + (-4))) AND ((0)  <=  ((X_nj) + (-3))) AND ((0)  <=  ((Y0) + (-1))) AND ((0)  <=  ((Y2) + (-1))) AND ((0)  <=  ((Y3) + (-1))) AND ((((Y0) + (-1))  <=  (0)) OR (NOT((EXISTS (t4 : INT, t5 : INT) : (((0) = (t5)) AND (((Y1) = (t4)*(2) + (t5)) AND (((t5) >= 0) AND ((t5) < (2)))))))))

cvc3 predicate   74:
FORALL (i__30 : INT) : ((FORALL (j__30 : INT) : ((((0) = (((((((Y5).1) WITH [Y0] := ((X_nj,((((Y5).1)[Y0]).1) WITH [Y1] := ((((((X_uin).1)[Y0]).1)[Y1])^2))))[i__30]).1)[j__30]) + ((-1) * (((((Y4).1)[i__30]).1)[j__30]))))) OR (((X_nj) + ((-1) * (j__30)))  <=  (0)) OR (((j__30) + (1))  <=  (0)))) OR (((X_ni) + ((-1) * (i__30)))  <=  (0)) OR (((i__30) + (1))  <=  (0)))

cvc3 result      74: MAYBE


theory SARL_REAL
use import real.Real
function add (a b : real) : real = a + b
function sub (a b : real) : real = a - b
function mul (a b : real) : real = a * b
function neg (a : real) : real = (-a)
function (:-) (a b : real) : real = a / b
predicate lt (a b : real) = a < b
predicate lte (a b : real) = a <= b
clone import int.Exponentiation as POWREAL with type t = real
function sarl_power (a : real) (b : int) : real = (POWREAL.power a b)
use import real.PowerReal as POWREALREAL
function sarl_power_real (a : real) (b : real) : real = (POWREALREAL.pow a b)
end
theory Why3Query_75
use import int.EuclideanDivision
use import map.Map
use import int.Int
use import SARL_REAL as SR
constant _Y0 : int

constant _X_ni : int

constant _Y2 : int

constant _X_nj : int

constant _Y3 : int

constant _Y1 : int

constant _Y6 : (map int (map int real))

constant _Y7 : (map int (map int real))

constant _Y5 : (map int (map int real))

constant _Y4 : (map int (map int real))

constant _X_uin : (map int (map int real))

predicate _Axcontext = (((0)  =  ((mod _Y0 (2))  +  (-1)))  &&  ((0)  =  (_X_ni  +  ((-1)  *  _Y2)  +  (-1)))  &&  ((0)  =  (_X_nj  +  ((-1)  *  _Y3)  +  (-1)))  &&  ((0)  =  (_Y0  +  ((-1)  *  _Y2)  +  (1)))  &&  ((0)  =  (_Y1  +  ((-1)  *  _Y3)  +  (1)))  &&  (forall __cc_bv_10__28 : int. (forall __cc_bv_11__28 : int. ((0.0  =  (get (get _Y6 __cc_bv_11__28) __cc_bv_10__28))  ||  ((0)  <=  (_X_ni  +  ((-1)  *  __cc_bv_11__28)  +  (-2))))))  &&  (forall __cc_bv_10__29 : int. (forall __cc_bv_11__29 : int. ((0.0  =  (get (get _Y6 __cc_bv_11__29) __cc_bv_10__29))  ||  ((0)  <=  (__cc_bv_11__29  +  (-1))))))  &&  (forall __cc_bv_10__30 : int. ((forall __cc_bv_11__30 : int. (0.0  =  (get (get _Y6 __cc_bv_11__30) __cc_bv_10__30)))  ||  ((0)  <=  (_X_nj  +  ((-1)  *  __cc_bv_10__30)  +  (-2)))))  &&  (forall __cc_bv_10__31 : int. ((forall __cc_bv_11__31 : int. (0.0  =  (get (get _Y6 __cc_bv_11__31) __cc_bv_10__31)))  ||  ((0)  <=  (__cc_bv_10__31  +  (-1)))))  &&  (forall __cc_bv_14__13 : int. (forall __cc_bv_15__13 : int. (((0)  =  (_Y0  +  ((-1)  *  __cc_bv_15__13)))  ||  (0.0  =   ( SR.add (get (get _Y6 __cc_bv_15__13) __cc_bv_14__13)  ( SR.mul (SR.neg 1.0) (get (get _Y7 __cc_bv_15__13) __cc_bv_14__13)))))))  &&  (forall __cc_bv_14__14 : int. ((forall __cc_bv_15__14 : int. (0.0  =   ( SR.add (get (get _Y6 __cc_bv_15__14) __cc_bv_14__14)  ( SR.mul (SR.neg 1.0) (get (get _Y7 __cc_bv_15__14) __cc_bv_14__14)))))  ||  ((0)  <=  (_X_nj  +  ((-1)  *  __cc_bv_14__14)  +  (-2)))))  &&  (forall __cc_bv_14__15 : int. ((forall __cc_bv_15__15 : int. (0.0  =   ( SR.add (get (get _Y6 __cc_bv_15__15) __cc_bv_14__15)  ( SR.mul (SR.neg 1.0) (get (get _Y7 __cc_bv_15__15) __cc_bv_14__15)))))  ||  ((0)  <=  (__cc_bv_14__15  +  (-1)))))  &&  (forall __cc_bv_18__3 : int. (forall __cc_bv_19__3 : int. ((0.0  =   ( SR.add (get (get _Y5 __cc_bv_19__3) __cc_bv_18__3)  ( SR.mul (SR.neg 1.0) (get (get _Y7 __cc_bv_19__3) __cc_bv_18__3))))  ||  ((0)  <=  (_X_ni  +  ((-1)  *  __cc_bv_19__3)  +  (-2))))))  &&  (forall __cc_bv_18__4 : int. (forall __cc_bv_19__4 : int. ((0.0  =   ( SR.add (get (get _Y5 __cc_bv_19__4) __cc_bv_18__4)  ( SR.mul (SR.neg 1.0) (get (get _Y7 __cc_bv_19__4) __cc_bv_18__4))))  ||  ((0)  <=  (__cc_bv_19__4  +  (-1))))))  &&  (forall __cc_bv_18__5 : int. (((0)  =  (_Y1  +  ((-1)  *  __cc_bv_18__5)))  ||  (forall __cc_bv_19__5 : int. (0.0  =   ( SR.add (get (get _Y5 __cc_bv_19__5) __cc_bv_18__5)  ( SR.mul (SR.neg 1.0) (get (get _Y7 __cc_bv_19__5) __cc_bv_18__5)))))))  &&  (forall _i__27 : int. ((0.0  =  (get (get _Y4 _i__27) (_X_nj  +  (-1))))  ||  ((_X_ni  +  ((-1)  *  _i__27))  <=  (0))  ||  ((_i__27  +  (1))  <=  (0))))  &&  (forall _i__28 : int. ((0.0  =  (get (get _Y4 _i__28) (0)))  ||  ((_X_ni  +  ((-1)  *  _i__28))  <=  (0))  ||  ((_i__28  +  (1))  <=  (0))))  &&  (forall _i__29 : int. ((forall _j__27 : int. ((0.0  =   ( SR.add (SR.mul (get (get _X_uin _i__29) _j__27) (get (get _X_uin _i__29) _j__27))  ( SR.mul (SR.neg 1.0) (get (get _Y4 _i__29) _j__27))))  ||  ((_X_nj  +  ((-1)  *  _j__27)  +  (-1))  <=  (0))  ||  (_j__27  <=  (0))))  ||  ((_X_ni  +  ((-1)  *  _i__29)  +  (-1))  <=  (0))  ||  (_i__29  <=  (0))))  &&  (forall _j__28 : int. ((0.0  =  (get (get _Y4 (_X_ni  +  (-1))) _j__28))  ||  ((_X_nj  +  ((-1)  *  _j__28))  <=  (0))  ||  ((_j__28  +  (1))  <=  (0))))  &&  (forall _j__29 : int. ((0.0  =  (get (get _Y4 (0)) _j__29))  ||  ((_X_nj  +  ((-1)  *  _j__29))  <=  (0))  ||  ((_j__29  +  (1))  <=  (0))))  &&  (forall _k__26 : int. ((forall _t__28 : int. ((0.0  =   ( SR.add (SR.mul (get (get _X_uin _t__28) _k__26) (get (get _X_uin _t__28) _k__26))  ( SR.mul (SR.neg 1.0) (get (get _Y6 _t__28) _k__26))))  ||  ((_Y0  +  ((-1)  *  _t__28))  <=  (0))  ||  (_t__28  <=  (0))))  ||  (_k__26  <=  (0))  ||  ((0)  <=  ((if ((0)  <=  ((mod (_X_nj  +  (-3)) (2))  +  (-1))) then ((mod (_X_nj  +  (-3)) (2))  +  (-1)) else ((-1)  *  ((mod (_X_nj  +  (-3)) (2))  +  (-1))))  +  ((-1)  *  _X_nj)  +  _k__26  +  (1)))))  &&  (forall _t__26 : int. ((0.0  =   ( SR.add (SR.mul (get (get _X_uin _Y0) _t__26) (get (get _X_uin _Y0) _t__26))  ( SR.mul (SR.neg 1.0) (get (get _Y7 _Y0) _t__26))))  ||  ((_Y3  +  ((-1)  *  _t__26))  <=  (0))  ||  (_t__26  <=  (0))))  &&  (forall _t__27 : int. ((0.0  =   ( SR.add (SR.mul (get (get _X_uin _t__27) _Y1) (get (get _X_uin _t__27) _Y1))  ( SR.mul (SR.neg 1.0) (get (get _Y5 _t__27) _Y1))))  ||  ((_Y2  +  ((-1)  *  _t__27))  <=  (0))  ||  (_t__27  <=  (0))))  &&  ((0)  <=  (_X_ni  +  (-4)))  &&  ((0)  <=  (_X_nj  +  (-3)))  &&  ((0)  <=  (_Y0  +  (-1)))  &&  ((0)  <=  (_Y2  +  (-1)))  &&  ((0)  <=  (_Y3  +  (-1)))  &&  (((_Y0  +  (-1))  <=  (0))  ||  (not ((0)  =  (mod _Y1 (2))))))
predicate context = _Axcontext
goal G0: context -> (forall _i__30 : int. ((forall _j__30 : int. ((0.0  =   ( SR.add (get (get (set _Y5 _Y0 (set (get _Y5 _Y0) _Y1 (SR.mul (get (get _X_uin _Y0) _Y1) (get (get _X_uin _Y0) _Y1)))) _i__30) _j__30)  ( SR.mul (SR.neg 1.0) (get (get _Y4 _i__30) _j__30))))  ||  ((_X_nj  +  ((-1)  *  _j__30))  <=  (0))  ||  ((_j__30  +  (1))  <=  (0))))  ||  ((_X_ni  +  ((-1)  *  _i__30))  <=  (0))  ||  ((_i__30  +  (1))  <=  (0))))
end
