### (0) Obligation:

JBC Problem based on JBC Program:
`No human-readable program information known.`

Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: LogAG

### (1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

### (2) Obligation:

FIGraph based on JBC Program:
Graph of 138 nodes with 1 SCC.

### (3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

### (4) Obligation:

ITRS problem:

The following function symbols are pre-defined:
 != ~ Neq: (Integer, Integer) -> Boolean * ~ Mul: (Integer, Integer) -> Integer >= ~ Ge: (Integer, Integer) -> Boolean -1 ~ UnaryMinus: (Integer) -> Integer | ~ Bwor: (Integer, Integer) -> Integer / ~ Div: (Integer, Integer) -> Integer = ~ Eq: (Integer, Integer) -> Boolean ~ Bwxor: (Integer, Integer) -> Integer || ~ Lor: (Boolean, Boolean) -> Boolean ! ~ Lnot: (Boolean) -> Boolean < ~ Lt: (Integer, Integer) -> Boolean - ~ Sub: (Integer, Integer) -> Integer <= ~ Le: (Integer, Integer) -> Boolean > ~ Gt: (Integer, Integer) -> Boolean ~ ~ Bwnot: (Integer) -> Integer % ~ Mod: (Integer, Integer) -> Integer & ~ Bwand: (Integer, Integer) -> Integer + ~ Add: (Integer, Integer) -> Integer && ~ Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Cond_Load416(TRUE, 1, i36, i33) → Load583(1, i36, i33, i36 - 2, 0)
Load583(1, i36, i33, i51, i48) → Cond_Load583(i51 > 1 && i48 + 1 > 0, 1, i36, i33, i51, i48)
Cond_Load583(TRUE, 1, i36, i33, i51, i48) → Load583(1, i36, i33, i51 - 2, i48 + 1)
Load583(1, i36, i33, i51, i48) → Cond_Load5831(i51 > 0 && i51 <= 1, 1, i36, i33, i51, i48)
Load594(1, i36, i33, i48) → Load416(1, i48 + 1, i33 + 1)
Load583(1, i36, i33, i50, i48) → Cond_Load5832(i50 <= 1 && i33 + 1 > 0 && i48 + 1 > 0, 1, i36, i33, i50, i48)
Cond_Load5832(TRUE, 1, i36, i33, i50, i48) → Load416(1, i48 + 1, i33 + 1)
The set Q consists of the following terms:
Cond_Load583(TRUE, 1, x0, x1, x2, x3)
Cond_Load5831(TRUE, 1, x0, x1, x2, x3)
Cond_Load5832(TRUE, 1, x0, x1, x2, x3)

### (5) GroundTermsRemoverProof (EQUIVALENT transformation)

Some arguments are removed because they always contain the same ground term.
We removed the following ground terms:
• 1

We removed arguments according to the following replacements:

Cond_Load5832(x1, x2, x3, x4, x5, x6) → Cond_Load5832(x1, x3, x4, x5, x6)
Cond_Load5831(x1, x2, x3, x4, x5, x6) → Cond_Load5831(x1, x3, x4, x5, x6)
Cond_Load583(x1, x2, x3, x4, x5, x6) → Cond_Load583(x1, x3, x4, x5, x6)

### (6) Obligation:

ITRS problem:

The following function symbols are pre-defined:
 != ~ Neq: (Integer, Integer) -> Boolean * ~ Mul: (Integer, Integer) -> Integer >= ~ Ge: (Integer, Integer) -> Boolean -1 ~ UnaryMinus: (Integer) -> Integer | ~ Bwor: (Integer, Integer) -> Integer / ~ Div: (Integer, Integer) -> Integer = ~ Eq: (Integer, Integer) -> Boolean ~ Bwxor: (Integer, Integer) -> Integer || ~ Lor: (Boolean, Boolean) -> Boolean ! ~ Lnot: (Boolean) -> Boolean < ~ Lt: (Integer, Integer) -> Boolean - ~ Sub: (Integer, Integer) -> Integer <= ~ Le: (Integer, Integer) -> Boolean > ~ Gt: (Integer, Integer) -> Boolean ~ ~ Bwnot: (Integer) -> Integer % ~ Mod: (Integer, Integer) -> Integer & ~ Bwand: (Integer, Integer) -> Integer + ~ Add: (Integer, Integer) -> Integer && ~ Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load583(i36, i33, i51, i48) → Cond_Load583(i51 > 1 && i48 + 1 > 0, i36, i33, i51, i48)
Cond_Load583(TRUE, i36, i33, i51, i48) → Load583(i36, i33, i51 - 2, i48 + 1)
Load583(i36, i33, i51, i48) → Cond_Load5831(i51 > 0 && i51 <= 1, i36, i33, i51, i48)
Load583(i36, i33, i50, i48) → Cond_Load5832(i50 <= 1 && i33 + 1 > 0 && i48 + 1 > 0, i36, i33, i50, i48)
Cond_Load5832(TRUE, i36, i33, i50, i48) → Load416(i48 + 1, i33 + 1)
The set Q consists of the following terms:

### (8) Obligation:

IDP problem:
The following function symbols are pre-defined:
 != ~ Neq: (Integer, Integer) -> Boolean * ~ Mul: (Integer, Integer) -> Integer >= ~ Ge: (Integer, Integer) -> Boolean -1 ~ UnaryMinus: (Integer) -> Integer | ~ Bwor: (Integer, Integer) -> Integer / ~ Div: (Integer, Integer) -> Integer = ~ Eq: (Integer, Integer) -> Boolean ~ Bwxor: (Integer, Integer) -> Integer || ~ Lor: (Boolean, Boolean) -> Boolean ! ~ Lnot: (Boolean) -> Boolean < ~ Lt: (Integer, Integer) -> Boolean - ~ Sub: (Integer, Integer) -> Integer <= ~ Le: (Integer, Integer) -> Boolean > ~ Gt: (Integer, Integer) -> Boolean ~ ~ Bwnot: (Integer) -> Integer % ~ Mod: (Integer, Integer) -> Integer & ~ Bwand: (Integer, Integer) -> Integer + ~ Add: (Integer, Integer) -> Integer && ~ Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

The ITRS R consists of the following rules:
Load583(i36, i33, i51, i48) → Cond_Load583(i51 > 1 && i48 + 1 > 0, i36, i33, i51, i48)
Cond_Load583(TRUE, i36, i33, i51, i48) → Load583(i36, i33, i51 - 2, i48 + 1)
Load583(i36, i33, i51, i48) → Cond_Load5831(i51 > 0 && i51 <= 1, i36, i33, i51, i48)
Load583(i36, i33, i50, i48) → Cond_Load5832(i50 <= 1 && i33 + 1 > 0 && i48 + 1 > 0, i36, i33, i50, i48)
Cond_Load5832(TRUE, i36, i33, i50, i48) → Load416(i48 + 1, i33 + 1)

The integer pair graph contains the following rules and edges:
(2): LOAD583(i36[2], i33[2], i51[2], i48[2]) → COND_LOAD583(i51[2] > 1 && i48[2] + 1 > 0, i36[2], i33[2], i51[2], i48[2])
(3): COND_LOAD583(TRUE, i36[3], i33[3], i51[3], i48[3]) → LOAD583(i36[3], i33[3], i51[3] - 2, i48[3] + 1)
(4): LOAD583(i36[4], i33[4], i51[4], i48[4]) → COND_LOAD5831(i51[4] > 0 && i51[4] <= 1, i36[4], i33[4], i51[4], i48[4])
(7): LOAD583(i36[7], i33[7], i50[7], i48[7]) → COND_LOAD5832(i50[7] <= 1 && i33[7] + 1 > 0 && i48[7] + 1 > 0, i36[7], i33[7], i50[7], i48[7])
(8): COND_LOAD5832(TRUE, i36[8], i33[8], i50[8], i48[8]) → LOAD416(i48[8] + 1, i33[8] + 1)

(0) -> (1), if ((i33[0]* i33[1])∧(i36[0] > 1* TRUE)∧(i36[0]* i36[1]))

(1) -> (2), if ((0* i48[2])∧(i36[1] - 2* i51[2])∧(i33[1]* i33[2])∧(i36[1]* i36[2]))

(1) -> (4), if ((i33[1]* i33[4])∧(i36[1]* i36[4])∧(0* i48[4])∧(i36[1] - 2* i51[4]))

(1) -> (7), if ((i36[1] - 2* i50[7])∧(i33[1]* i33[7])∧(0* i48[7])∧(i36[1]* i36[7]))

(2) -> (3), if ((i36[2]* i36[3])∧(i51[2]* i51[3])∧(i33[2]* i33[3])∧(i48[2]* i48[3])∧(i51[2] > 1 && i48[2] + 1 > 0* TRUE))

(3) -> (2), if ((i48[3] + 1* i48[2])∧(i51[3] - 2* i51[2])∧(i33[3]* i33[2])∧(i36[3]* i36[2]))

(3) -> (4), if ((i48[3] + 1* i48[4])∧(i36[3]* i36[4])∧(i33[3]* i33[4])∧(i51[3] - 2* i51[4]))

(3) -> (7), if ((i48[3] + 1* i48[7])∧(i51[3] - 2* i50[7])∧(i36[3]* i36[7])∧(i33[3]* i33[7]))

(4) -> (5), if ((i51[4] > 0 && i51[4] <= 1* TRUE)∧(i36[4]* i36[5])∧(i51[4]* i51[5])∧(i48[4]* i48[5])∧(i33[4]* i33[5]))

(5) -> (6), if ((i48[5]* i48[6])∧(i36[5]* i36[6])∧(i33[5]* i33[6]))

(6) -> (0), if ((i33[6] + 1* i33[0])∧(i48[6] + 1* i36[0]))

(7) -> (8), if ((i50[7]* i50[8])∧(i33[7]* i33[8])∧(i36[7]* i36[8])∧(i48[7]* i48[8])∧(i50[7] <= 1 && i33[7] + 1 > 0 && i48[7] + 1 > 0* TRUE))

(8) -> (0), if ((i48[8] + 1* i36[0])∧(i33[8] + 1* i33[0]))

The set Q consists of the following terms:

### (9) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

### (10) Obligation:

IDP problem:
The following function symbols are pre-defined:
 != ~ Neq: (Integer, Integer) -> Boolean * ~ Mul: (Integer, Integer) -> Integer >= ~ Ge: (Integer, Integer) -> Boolean -1 ~ UnaryMinus: (Integer) -> Integer | ~ Bwor: (Integer, Integer) -> Integer / ~ Div: (Integer, Integer) -> Integer = ~ Eq: (Integer, Integer) -> Boolean ~ Bwxor: (Integer, Integer) -> Integer || ~ Lor: (Boolean, Boolean) -> Boolean ! ~ Lnot: (Boolean) -> Boolean < ~ Lt: (Integer, Integer) -> Boolean - ~ Sub: (Integer, Integer) -> Integer <= ~ Le: (Integer, Integer) -> Boolean > ~ Gt: (Integer, Integer) -> Boolean ~ ~ Bwnot: (Integer) -> Integer % ~ Mod: (Integer, Integer) -> Integer & ~ Bwand: (Integer, Integer) -> Integer + ~ Add: (Integer, Integer) -> Integer && ~ Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(2): LOAD583(i36[2], i33[2], i51[2], i48[2]) → COND_LOAD583(i51[2] > 1 && i48[2] + 1 > 0, i36[2], i33[2], i51[2], i48[2])
(3): COND_LOAD583(TRUE, i36[3], i33[3], i51[3], i48[3]) → LOAD583(i36[3], i33[3], i51[3] - 2, i48[3] + 1)
(4): LOAD583(i36[4], i33[4], i51[4], i48[4]) → COND_LOAD5831(i51[4] > 0 && i51[4] <= 1, i36[4], i33[4], i51[4], i48[4])
(7): LOAD583(i36[7], i33[7], i50[7], i48[7]) → COND_LOAD5832(i50[7] <= 1 && i33[7] + 1 > 0 && i48[7] + 1 > 0, i36[7], i33[7], i50[7], i48[7])
(8): COND_LOAD5832(TRUE, i36[8], i33[8], i50[8], i48[8]) → LOAD416(i48[8] + 1, i33[8] + 1)

(0) -> (1), if ((i33[0]* i33[1])∧(i36[0] > 1* TRUE)∧(i36[0]* i36[1]))

(1) -> (2), if ((0* i48[2])∧(i36[1] - 2* i51[2])∧(i33[1]* i33[2])∧(i36[1]* i36[2]))

(1) -> (4), if ((i33[1]* i33[4])∧(i36[1]* i36[4])∧(0* i48[4])∧(i36[1] - 2* i51[4]))

(1) -> (7), if ((i36[1] - 2* i50[7])∧(i33[1]* i33[7])∧(0* i48[7])∧(i36[1]* i36[7]))

(2) -> (3), if ((i36[2]* i36[3])∧(i51[2]* i51[3])∧(i33[2]* i33[3])∧(i48[2]* i48[3])∧(i51[2] > 1 && i48[2] + 1 > 0* TRUE))

(3) -> (2), if ((i48[3] + 1* i48[2])∧(i51[3] - 2* i51[2])∧(i33[3]* i33[2])∧(i36[3]* i36[2]))

(3) -> (4), if ((i48[3] + 1* i48[4])∧(i36[3]* i36[4])∧(i33[3]* i33[4])∧(i51[3] - 2* i51[4]))

(3) -> (7), if ((i48[3] + 1* i48[7])∧(i51[3] - 2* i50[7])∧(i36[3]* i36[7])∧(i33[3]* i33[7]))

(4) -> (5), if ((i51[4] > 0 && i51[4] <= 1* TRUE)∧(i36[4]* i36[5])∧(i51[4]* i51[5])∧(i48[4]* i48[5])∧(i33[4]* i33[5]))

(5) -> (6), if ((i48[5]* i48[6])∧(i36[5]* i36[6])∧(i33[5]* i33[6]))

(6) -> (0), if ((i33[6] + 1* i33[0])∧(i48[6] + 1* i36[0]))

(7) -> (8), if ((i50[7]* i50[8])∧(i33[7]* i33[8])∧(i36[7]* i36[8])∧(i48[7]* i48[8])∧(i50[7] <= 1 && i33[7] + 1 > 0 && i48[7] + 1 > 0* TRUE))

(8) -> (0), if ((i48[8] + 1* i36[0])∧(i33[8] + 1* i33[0]))

The set Q consists of the following terms:

### (11) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair LOAD416(i36, i33) → COND_LOAD416(>(i36, 1), i36, i33) the following chains were created:
• We consider the chain LOAD416(i36[0], i33[0]) → COND_LOAD416(>(i36[0], 1), i36[0], i33[0]), COND_LOAD416(TRUE, i36[1], i33[1]) → LOAD583(i36[1], i33[1], -(i36[1], 2), 0) which results in the following constraint:

We simplified constraint (1) using rule (IV) which results in the following new constraint:

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(3)    (i36[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD416(>(i36[0], 1), i36[0], i33[0])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [bni_40]i36[0] ≥ 0∧[(-1)bso_41] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(4)    (i36[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD416(>(i36[0], 1), i36[0], i33[0])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [bni_40]i36[0] ≥ 0∧[(-1)bso_41] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(5)    (i36[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD416(>(i36[0], 1), i36[0], i33[0])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [bni_40]i36[0] ≥ 0∧[(-1)bso_41] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(6)    (i36[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD416(>(i36[0], 1), i36[0], i33[0])), ≥)∧0 = 0∧[(-1)bni_40 + (-1)Bound*bni_40] + [bni_40]i36[0] ≥ 0∧0 = 0∧[(-1)bso_41] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(7)    (i36[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD416(>(i36[0], 1), i36[0], i33[0])), ≥)∧0 = 0∧[bni_40 + (-1)Bound*bni_40] + [bni_40]i36[0] ≥ 0∧0 = 0∧[(-1)bso_41] ≥ 0)

For Pair COND_LOAD416(TRUE, i36, i33) → LOAD583(i36, i33, -(i36, 2), 0) the following chains were created:

(8)    (i48[5]=i48[6]i36[5]=i36[6]i33[5]=i33[6]+(i33[6], 1)=i33[0]+(i48[6], 1)=i36[0]i33[0]=i33[1]>(i36[0], 1)=TRUEi36[0]=i36[1]0=i48[2]-(i36[1], 2)=i51[2]i33[1]=i33[2]i36[1]=i36[2]i36[2]=i36[3]i51[2]=i51[3]i33[2]=i33[3]i48[2]=i48[3]&&(>(i51[2], 1), >(+(i48[2], 1), 0))=TRUECOND_LOAD416(TRUE, i36[1], i33[1])≥NonInfC∧COND_LOAD416(TRUE, i36[1], i33[1])≥LOAD583(i36[1], i33[1], -(i36[1], 2), 0)∧(UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥))

We simplified constraint (8) using rules (III), (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN) which results in the following new constraint:

(9)    (>(+(i48[6], 1), 1)=TRUE>(-(+(i48[6], 1), 2), 1)=TRUECOND_LOAD416(TRUE, +(i48[6], 1), +(i33[6], 1))≥NonInfC∧COND_LOAD416(TRUE, +(i48[6], 1), +(i33[6], 1))≥LOAD583(+(i48[6], 1), +(i33[6], 1), -(+(i48[6], 1), 2), 0)∧(UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥))

We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(10)    (i48[6] + [-1] ≥ 0∧i48[6] + [-3] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42] + [bni_42]i48[6] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(11)    (i48[6] + [-1] ≥ 0∧i48[6] + [-3] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42] + [bni_42]i48[6] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(12)    (i48[6] + [-1] ≥ 0∧i48[6] + [-3] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42] + [bni_42]i48[6] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (12) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(13)    (i48[6] + [-1] ≥ 0∧i48[6] + [-3] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧0 = 0∧[(-1)Bound*bni_42] + [bni_42]i48[6] ≥ 0∧0 = 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(14)    (i48[6] ≥ 0∧[-2] + i48[6] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧0 = 0∧[(-1)Bound*bni_42 + bni_42] + [bni_42]i48[6] ≥ 0∧0 = 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (14) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(15)    ([2] + i48[6] ≥ 0∧i48[6] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧0 = 0∧[(-1)Bound*bni_42 + (3)bni_42] + [bni_42]i48[6] ≥ 0∧0 = 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (16) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

(17)    (>(+(i48[6], 1), 1)=TRUE>(-(+(i48[6], 1), 2), 0)=TRUE<=(-(+(i48[6], 1), 2), 1)=TRUECOND_LOAD416(TRUE, +(i48[6], 1), +(i33[6], 1))≥NonInfC∧COND_LOAD416(TRUE, +(i48[6], 1), +(i33[6], 1))≥LOAD583(+(i48[6], 1), +(i33[6], 1), -(+(i48[6], 1), 2), 0)∧(UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥))

We simplified constraint (17) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(18)    (i48[6] + [-1] ≥ 0∧i48[6] + [-2] ≥ 0∧[2] + [-1]i48[6] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42] + [bni_42]i48[6] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (18) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(19)    (i48[6] + [-1] ≥ 0∧i48[6] + [-2] ≥ 0∧[2] + [-1]i48[6] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42] + [bni_42]i48[6] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (19) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(20)    (i48[6] + [-1] ≥ 0∧i48[6] + [-2] ≥ 0∧[2] + [-1]i48[6] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42] + [bni_42]i48[6] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (20) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(21)    (i48[6] + [-1] ≥ 0∧i48[6] + [-2] ≥ 0∧[2] + [-1]i48[6] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧0 = 0∧[(-1)Bound*bni_42] + [bni_42]i48[6] ≥ 0∧0 = 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (21) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(22)    (i48[6] ≥ 0∧[-1] + i48[6] ≥ 0∧[1] + [-1]i48[6] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧0 = 0∧[(-1)Bound*bni_42 + bni_42] + [bni_42]i48[6] ≥ 0∧0 = 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (22) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(23)    ([1] + i48[6] ≥ 0∧i48[6] ≥ 0∧[-1]i48[6] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧0 = 0∧[(-1)Bound*bni_42 + (2)bni_42] + [bni_42]i48[6] ≥ 0∧0 = 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (23) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(24)    ([1] ≥ 0∧0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧0 = 0∧[(-1)Bound*bni_42 + (2)bni_42] ≥ 0∧0 = 0∧[1 + (-1)bso_43] ≥ 0)

(25)    (i48[5]=i48[6]i36[5]=i36[6]i33[5]=i33[6]+(i33[6], 1)=i33[0]+(i48[6], 1)=i36[0]i33[0]=i33[1]>(i36[0], 1)=TRUEi36[0]=i36[1]-(i36[1], 2)=i50[7]i33[1]=i33[7]0=i48[7]i36[1]=i36[7]i50[7]=i50[8]i33[7]=i33[8]i36[7]=i36[8]i48[7]=i48[8]&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0))=TRUECOND_LOAD416(TRUE, i36[1], i33[1])≥NonInfC∧COND_LOAD416(TRUE, i36[1], i33[1])≥LOAD583(i36[1], i33[1], -(i36[1], 2), 0)∧(UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥))

We simplified constraint (25) using rules (III), (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN) which results in the following new constraint:

(26)    (>(+(i48[6], 1), 1)=TRUE<=(-(+(i48[6], 1), 2), 1)=TRUE>(+(+(i33[6], 1), 1), 0)=TRUECOND_LOAD416(TRUE, +(i48[6], 1), +(i33[6], 1))≥NonInfC∧COND_LOAD416(TRUE, +(i48[6], 1), +(i33[6], 1))≥LOAD583(+(i48[6], 1), +(i33[6], 1), -(+(i48[6], 1), 2), 0)∧(UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥))

We simplified constraint (26) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(27)    (i48[6] + [-1] ≥ 0∧[2] + [-1]i48[6] ≥ 0∧i33[6] + [1] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42] + [bni_42]i48[6] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (27) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(28)    (i48[6] + [-1] ≥ 0∧[2] + [-1]i48[6] ≥ 0∧i33[6] + [1] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42] + [bni_42]i48[6] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (28) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(29)    (i48[6] + [-1] ≥ 0∧[2] + [-1]i48[6] ≥ 0∧i33[6] + [1] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42] + [bni_42]i48[6] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (29) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(30)    (i48[6] ≥ 0∧[1] + [-1]i48[6] ≥ 0∧i33[6] + [1] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42 + bni_42] + [bni_42]i48[6] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (30) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

(31)    (i48[6] ≥ 0∧[1] + [-1]i48[6] ≥ 0∧i33[6] + [1] ≥ 0∧i33[6] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42 + bni_42] + [bni_42]i48[6] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

(32)    (i48[6] ≥ 0∧[1] + [-1]i48[6] ≥ 0∧[-1]i33[6] + [1] ≥ 0∧i33[6] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42 + bni_42] + [bni_42]i48[6] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

(33)    (i50[7]=i50[8]i33[7]=i33[8]i36[7]=i36[8]i48[7]=i48[8]&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0))=TRUE+(i48[8], 1)=i36[0]+(i33[8], 1)=i33[0]i33[0]=i33[1]>(i36[0], 1)=TRUEi36[0]=i36[1]0=i48[2]-(i36[1], 2)=i51[2]i33[1]=i33[2]i36[1]=i36[2]i36[2]=i36[3]i51[2]=i51[3]i33[2]=i33[3]i48[2]=i48[3]&&(>(i51[2], 1), >(+(i48[2], 1), 0))=TRUECOND_LOAD416(TRUE, i36[1], i33[1])≥NonInfC∧COND_LOAD416(TRUE, i36[1], i33[1])≥LOAD583(i36[1], i33[1], -(i36[1], 2), 0)∧(UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥))

We simplified constraint (33) using rules (III), (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN) which results in the following new constraint:

(34)    (>(+(i48[7], 1), 1)=TRUE>(+(i48[7], 1), 0)=TRUE>(-(+(i48[7], 1), 2), 1)=TRUE<=(i50[7], 1)=TRUE>(+(i33[7], 1), 0)=TRUECOND_LOAD416(TRUE, +(i48[7], 1), +(i33[7], 1))≥NonInfC∧COND_LOAD416(TRUE, +(i48[7], 1), +(i33[7], 1))≥LOAD583(+(i48[7], 1), +(i33[7], 1), -(+(i48[7], 1), 2), 0)∧(UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥))

We simplified constraint (34) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(35)    (i48[7] + [-1] ≥ 0∧i48[7] ≥ 0∧i48[7] + [-3] ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42] + [bni_42]i48[7] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (35) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(36)    (i48[7] + [-1] ≥ 0∧i48[7] ≥ 0∧i48[7] + [-3] ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42] + [bni_42]i48[7] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (36) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(37)    (i48[7] + [-1] ≥ 0∧i48[7] ≥ 0∧i48[7] + [-3] ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42] + [bni_42]i48[7] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (37) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(38)    (i48[7] ≥ 0∧[1] + i48[7] ≥ 0∧[-2] + i48[7] ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42 + bni_42] + [bni_42]i48[7] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (38) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(39)    ([2] + i48[7] ≥ 0∧[3] + i48[7] ≥ 0∧i48[7] ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42 + (3)bni_42] + [bni_42]i48[7] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (39) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(40)    ([2] + i48[7] ≥ 0∧[3] + i48[7] ≥ 0∧i48[7] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42 + (3)bni_42] + [bni_42]i48[7] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

(41)    (i50[7]=i50[8]i33[7]=i33[8]i36[7]=i36[8]i48[7]=i48[8]&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0))=TRUE+(i48[8], 1)=i36[0]+(i33[8], 1)=i33[0]i33[0]=i33[1]>(i36[0], 1)=TRUEi36[0]=i36[1]i33[1]=i33[4]i36[1]=i36[4]0=i48[4]-(i36[1], 2)=i51[4]&&(>(i51[4], 0), <=(i51[4], 1))=TRUEi36[4]=i36[5]i51[4]=i51[5]i48[4]=i48[5]i33[4]=i33[5]COND_LOAD416(TRUE, i36[1], i33[1])≥NonInfC∧COND_LOAD416(TRUE, i36[1], i33[1])≥LOAD583(i36[1], i33[1], -(i36[1], 2), 0)∧(UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥))

We simplified constraint (41) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

(42)    (>(+(i48[7], 1), 1)=TRUE>(+(i48[7], 1), 0)=TRUE>(-(+(i48[7], 1), 2), 0)=TRUE<=(-(+(i48[7], 1), 2), 1)=TRUE<=(i50[7], 1)=TRUE>(+(i33[7], 1), 0)=TRUECOND_LOAD416(TRUE, +(i48[7], 1), +(i33[7], 1))≥NonInfC∧COND_LOAD416(TRUE, +(i48[7], 1), +(i33[7], 1))≥LOAD583(+(i48[7], 1), +(i33[7], 1), -(+(i48[7], 1), 2), 0)∧(UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥))

We simplified constraint (42) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(43)    (i48[7] + [-1] ≥ 0∧i48[7] ≥ 0∧i48[7] + [-2] ≥ 0∧[2] + [-1]i48[7] ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42] + [bni_42]i48[7] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (43) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(44)    (i48[7] + [-1] ≥ 0∧i48[7] ≥ 0∧i48[7] + [-2] ≥ 0∧[2] + [-1]i48[7] ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42] + [bni_42]i48[7] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (44) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(45)    (i48[7] + [-1] ≥ 0∧i48[7] ≥ 0∧i48[7] + [-2] ≥ 0∧[2] + [-1]i48[7] ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42] + [bni_42]i48[7] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (45) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(46)    (i48[7] ≥ 0∧[1] + i48[7] ≥ 0∧[-1] + i48[7] ≥ 0∧[1] + [-1]i48[7] ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42 + bni_42] + [bni_42]i48[7] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (46) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(47)    ([1] + i48[7] ≥ 0∧[2] + i48[7] ≥ 0∧i48[7] ≥ 0∧[-1]i48[7] ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42 + (2)bni_42] + [bni_42]i48[7] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (47) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(48)    ([1] ≥ 0∧[2] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42 + (2)bni_42] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (48) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(49)    ([1] ≥ 0∧[2] ≥ 0∧0 ≥ 0∧0 ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42 + (2)bni_42] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (49) using rule (IDP_POLY_GCD) which results in the following new constraint:

(50)    ([1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧i33[7] ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42 + (2)bni_42] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

(51)    (i50[7]=i50[8]i33[7]=i33[8]i36[7]=i36[8]i48[7]=i48[8]&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0))=TRUE+(i48[8], 1)=i36[0]+(i33[8], 1)=i33[0]i33[0]=i33[1]>(i36[0], 1)=TRUEi36[0]=i36[1]-(i36[1], 2)=i50[7]1i33[1]=i33[7]10=i48[7]1i36[1]=i36[7]1i50[7]1=i50[8]1i33[7]1=i33[8]1i36[7]1=i36[8]1i48[7]1=i48[8]1&&(&&(<=(i50[7]1, 1), >(+(i33[7]1, 1), 0)), >(+(i48[7]1, 1), 0))=TRUECOND_LOAD416(TRUE, i36[1], i33[1])≥NonInfC∧COND_LOAD416(TRUE, i36[1], i33[1])≥LOAD583(i36[1], i33[1], -(i36[1], 2), 0)∧(UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥))

We simplified constraint (51) using rules (III), (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN) which results in the following new constraint:

(52)    (>(+(i48[7], 1), 1)=TRUE>(+(i48[7], 1), 0)=TRUE<=(i50[7], 1)=TRUE>(+(i33[7], 1), 0)=TRUE<=(-(+(i48[7], 1), 2), 1)=TRUE>(+(+(i33[7], 1), 1), 0)=TRUECOND_LOAD416(TRUE, +(i48[7], 1), +(i33[7], 1))≥NonInfC∧COND_LOAD416(TRUE, +(i48[7], 1), +(i33[7], 1))≥LOAD583(+(i48[7], 1), +(i33[7], 1), -(+(i48[7], 1), 2), 0)∧(UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥))

We simplified constraint (52) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(53)    (i48[7] + [-1] ≥ 0∧i48[7] ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0∧[2] + [-1]i48[7] ≥ 0∧i33[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42] + [bni_42]i48[7] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (53) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(54)    (i48[7] + [-1] ≥ 0∧i48[7] ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0∧[2] + [-1]i48[7] ≥ 0∧i33[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42] + [bni_42]i48[7] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (54) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(55)    (i48[7] + [-1] ≥ 0∧i48[7] ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0∧[2] + [-1]i48[7] ≥ 0∧i33[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42] + [bni_42]i48[7] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (55) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(56)    (i48[7] ≥ 0∧[1] + i48[7] ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0∧[1] + [-1]i48[7] ≥ 0∧i33[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42 + bni_42] + [bni_42]i48[7] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (56) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(57)    (i48[7] ≥ 0∧[1] + i48[7] ≥ 0∧i33[7] ≥ 0∧[1] + [-1]i48[7] ≥ 0∧i33[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42 + bni_42] + [bni_42]i48[7] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

For Pair LOAD583(i36, i33, i51, i48) → COND_LOAD583(&&(>(i51, 1), >(+(i48, 1), 0)), i36, i33, i51, i48) the following chains were created:
• We consider the chain LOAD583(i36[2], i33[2], i51[2], i48[2]) → COND_LOAD583(&&(>(i51[2], 1), >(+(i48[2], 1), 0)), i36[2], i33[2], i51[2], i48[2]), COND_LOAD583(TRUE, i36[3], i33[3], i51[3], i48[3]) → LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1)) which results in the following constraint:

(58)    (i36[2]=i36[3]i51[2]=i51[3]i33[2]=i33[3]i48[2]=i48[3]&&(>(i51[2], 1), >(+(i48[2], 1), 0))=TRUELOAD583(i36[2], i33[2], i51[2], i48[2])≥NonInfC∧LOAD583(i36[2], i33[2], i51[2], i48[2])≥COND_LOAD583(&&(>(i51[2], 1), >(+(i48[2], 1), 0)), i36[2], i33[2], i51[2], i48[2])∧(UIncreasing(COND_LOAD583(&&(>(i51[2], 1), >(+(i48[2], 1), 0)), i36[2], i33[2], i51[2], i48[2])), ≥))

We simplified constraint (58) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:

(59)    (>(i51[2], 1)=TRUE>(+(i48[2], 1), 0)=TRUELOAD583(i36[2], i33[2], i51[2], i48[2])≥NonInfC∧LOAD583(i36[2], i33[2], i51[2], i48[2])≥COND_LOAD583(&&(>(i51[2], 1), >(+(i48[2], 1), 0)), i36[2], i33[2], i51[2], i48[2])∧(UIncreasing(COND_LOAD583(&&(>(i51[2], 1), >(+(i48[2], 1), 0)), i36[2], i33[2], i51[2], i48[2])), ≥))

We simplified constraint (59) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(60)    (i51[2] + [-2] ≥ 0∧i48[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD583(&&(>(i51[2], 1), >(+(i48[2], 1), 0)), i36[2], i33[2], i51[2], i48[2])), ≥)∧[(-1)Bound*bni_44] + [bni_44]i48[2] + [bni_44]i51[2] ≥ 0∧[1 + (-1)bso_45] ≥ 0)

We simplified constraint (60) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(61)    (i51[2] + [-2] ≥ 0∧i48[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD583(&&(>(i51[2], 1), >(+(i48[2], 1), 0)), i36[2], i33[2], i51[2], i48[2])), ≥)∧[(-1)Bound*bni_44] + [bni_44]i48[2] + [bni_44]i51[2] ≥ 0∧[1 + (-1)bso_45] ≥ 0)

We simplified constraint (61) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(62)    (i51[2] + [-2] ≥ 0∧i48[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD583(&&(>(i51[2], 1), >(+(i48[2], 1), 0)), i36[2], i33[2], i51[2], i48[2])), ≥)∧[(-1)Bound*bni_44] + [bni_44]i48[2] + [bni_44]i51[2] ≥ 0∧[1 + (-1)bso_45] ≥ 0)

We simplified constraint (62) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(63)    (i51[2] + [-2] ≥ 0∧i48[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD583(&&(>(i51[2], 1), >(+(i48[2], 1), 0)), i36[2], i33[2], i51[2], i48[2])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_44] + [bni_44]i48[2] + [bni_44]i51[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_45] ≥ 0)

We simplified constraint (63) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(64)    (i51[2] ≥ 0∧i48[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD583(&&(>(i51[2], 1), >(+(i48[2], 1), 0)), i36[2], i33[2], i51[2], i48[2])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_44 + (2)bni_44] + [bni_44]i48[2] + [bni_44]i51[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_45] ≥ 0)

For Pair COND_LOAD583(TRUE, i36, i33, i51, i48) → LOAD583(i36, i33, -(i51, 2), +(i48, 1)) the following chains were created:

(65)    (i33[0]=i33[1]>(i36[0], 1)=TRUEi36[0]=i36[1]0=i48[2]-(i36[1], 2)=i51[2]i33[1]=i33[2]i36[1]=i36[2]i36[2]=i36[3]i51[2]=i51[3]i33[2]=i33[3]i48[2]=i48[3]&&(>(i51[2], 1), >(+(i48[2], 1), 0))=TRUE+(i48[3], 1)=i48[2]1-(i51[3], 2)=i51[2]1i33[3]=i33[2]1i36[3]=i36[2]1i36[2]1=i36[3]1i51[2]1=i51[3]1i33[2]1=i33[3]1i48[2]1=i48[3]1&&(>(i51[2]1, 1), >(+(i48[2]1, 1), 0))=TRUECOND_LOAD583(TRUE, i36[3], i33[3], i51[3], i48[3])≥NonInfC∧COND_LOAD583(TRUE, i36[3], i33[3], i51[3], i48[3])≥LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))∧(UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥))

We simplified constraint (65) using rules (III), (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN) which results in the following new constraint:

(66)    (>(i36[0], 1)=TRUE>(-(i36[0], 2), 1)=TRUE>(-(-(i36[0], 2), 2), 1)=TRUECOND_LOAD583(TRUE, i36[0], i33[0], -(i36[0], 2), 0)≥NonInfC∧COND_LOAD583(TRUE, i36[0], i33[0], -(i36[0], 2), 0)≥LOAD583(i36[0], i33[0], -(-(i36[0], 2), 2), +(0, 1))∧(UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥))

We simplified constraint (66) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(67)    (i36[0] + [-2] ≥ 0∧i36[0] + [-4] ≥ 0∧i36[0] + [-6] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧[(-3)bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (67) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(68)    (i36[0] + [-2] ≥ 0∧i36[0] + [-4] ≥ 0∧i36[0] + [-6] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧[(-3)bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (68) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(69)    (i36[0] + [-2] ≥ 0∧i36[0] + [-4] ≥ 0∧i36[0] + [-6] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧[(-3)bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (69) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(70)    (i36[0] + [-2] ≥ 0∧i36[0] + [-4] ≥ 0∧i36[0] + [-6] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧0 = 0∧[(-3)bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (70) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(71)    (i36[0] ≥ 0∧[-2] + i36[0] ≥ 0∧[-4] + i36[0] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧0 = 0∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (71) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(72)    ([2] + i36[0] ≥ 0∧i36[0] ≥ 0∧[-2] + i36[0] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧0 = 0∧[bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (72) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(73)    ([4] + i36[0] ≥ 0∧[2] + i36[0] ≥ 0∧i36[0] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧0 = 0∧[(3)bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧0 = 0∧[(-1)bso_47] ≥ 0)

(74)    (i33[0]=i33[1]>(i36[0], 1)=TRUEi36[0]=i36[1]0=i48[2]-(i36[1], 2)=i51[2]i33[1]=i33[2]i36[1]=i36[2]i36[2]=i36[3]i51[2]=i51[3]i33[2]=i33[3]i48[2]=i48[3]&&(>(i51[2], 1), >(+(i48[2], 1), 0))=TRUE+(i48[3], 1)=i48[4]i36[3]=i36[4]i33[3]=i33[4]-(i51[3], 2)=i51[4]&&(>(i51[4], 0), <=(i51[4], 1))=TRUEi36[4]=i36[5]i51[4]=i51[5]i48[4]=i48[5]i33[4]=i33[5]COND_LOAD583(TRUE, i36[3], i33[3], i51[3], i48[3])≥NonInfC∧COND_LOAD583(TRUE, i36[3], i33[3], i51[3], i48[3])≥LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))∧(UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥))

We simplified constraint (74) using rules (III), (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN) which results in the following new constraint:

(75)    (>(i36[0], 1)=TRUE>(-(i36[0], 2), 1)=TRUE>(-(-(i36[0], 2), 2), 0)=TRUE<=(-(-(i36[0], 2), 2), 1)=TRUECOND_LOAD583(TRUE, i36[0], i33[0], -(i36[0], 2), 0)≥NonInfC∧COND_LOAD583(TRUE, i36[0], i33[0], -(i36[0], 2), 0)≥LOAD583(i36[0], i33[0], -(-(i36[0], 2), 2), +(0, 1))∧(UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥))

We simplified constraint (75) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(76)    (i36[0] + [-2] ≥ 0∧i36[0] + [-4] ≥ 0∧i36[0] + [-5] ≥ 0∧[5] + [-1]i36[0] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧[(-3)bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (76) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(77)    (i36[0] + [-2] ≥ 0∧i36[0] + [-4] ≥ 0∧i36[0] + [-5] ≥ 0∧[5] + [-1]i36[0] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧[(-3)bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (77) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(78)    (i36[0] + [-2] ≥ 0∧i36[0] + [-4] ≥ 0∧i36[0] + [-5] ≥ 0∧[5] + [-1]i36[0] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧[(-3)bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (78) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(79)    (i36[0] + [-2] ≥ 0∧i36[0] + [-4] ≥ 0∧i36[0] + [-5] ≥ 0∧[5] + [-1]i36[0] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧0 = 0∧[(-3)bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (79) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(80)    (i36[0] ≥ 0∧[-2] + i36[0] ≥ 0∧[-3] + i36[0] ≥ 0∧[3] + [-1]i36[0] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧0 = 0∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (80) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(81)    ([2] + i36[0] ≥ 0∧i36[0] ≥ 0∧[-1] + i36[0] ≥ 0∧[1] + [-1]i36[0] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧0 = 0∧[bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (81) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(82)    ([3] + i36[0] ≥ 0∧[1] + i36[0] ≥ 0∧i36[0] ≥ 0∧[-1]i36[0] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (82) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(83)    ([3] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] ≥ 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (83) using rule (IDP_POLY_GCD) which results in the following new constraint:

(84)    ([1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] ≥ 0∧0 = 0∧[(-1)bso_47] ≥ 0)

(85)    (i33[0]=i33[1]>(i36[0], 1)=TRUEi36[0]=i36[1]0=i48[2]-(i36[1], 2)=i51[2]i33[1]=i33[2]i36[1]=i36[2]i36[2]=i36[3]i51[2]=i51[3]i33[2]=i33[3]i48[2]=i48[3]&&(>(i51[2], 1), >(+(i48[2], 1), 0))=TRUE+(i48[3], 1)=i48[7]-(i51[3], 2)=i50[7]i36[3]=i36[7]i33[3]=i33[7]i50[7]=i50[8]i33[7]=i33[8]i36[7]=i36[8]i48[7]=i48[8]&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0))=TRUECOND_LOAD583(TRUE, i36[3], i33[3], i51[3], i48[3])≥NonInfC∧COND_LOAD583(TRUE, i36[3], i33[3], i51[3], i48[3])≥LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))∧(UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥))

We simplified constraint (85) using rules (III), (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN) which results in the following new constraint:

(86)    (>(i36[0], 1)=TRUE>(-(i36[0], 2), 1)=TRUE<=(-(-(i36[0], 2), 2), 1)=TRUE>(+(i33[7], 1), 0)=TRUECOND_LOAD583(TRUE, i36[0], i33[7], -(i36[0], 2), 0)≥NonInfC∧COND_LOAD583(TRUE, i36[0], i33[7], -(i36[0], 2), 0)≥LOAD583(i36[0], i33[7], -(-(i36[0], 2), 2), +(0, 1))∧(UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥))

We simplified constraint (86) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(87)    (i36[0] + [-2] ≥ 0∧i36[0] + [-4] ≥ 0∧[5] + [-1]i36[0] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧[(-3)bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (87) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(88)    (i36[0] + [-2] ≥ 0∧i36[0] + [-4] ≥ 0∧[5] + [-1]i36[0] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧[(-3)bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (88) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(89)    (i36[0] + [-2] ≥ 0∧i36[0] + [-4] ≥ 0∧[5] + [-1]i36[0] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧[(-3)bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (89) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(90)    (i36[0] ≥ 0∧[-2] + i36[0] ≥ 0∧[3] + [-1]i36[0] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (90) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(91)    ([2] + i36[0] ≥ 0∧i36[0] ≥ 0∧[1] + [-1]i36[0] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧[bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧[(-1)bso_47] ≥ 0)

(92)    (i36[2]=i36[3]i51[2]=i51[3]i33[2]=i33[3]i48[2]=i48[3]&&(>(i51[2], 1), >(+(i48[2], 1), 0))=TRUE+(i48[3], 1)=i48[2]1-(i51[3], 2)=i51[2]1i33[3]=i33[2]1i36[3]=i36[2]1i36[2]1=i36[3]1i51[2]1=i51[3]1i33[2]1=i33[3]1i48[2]1=i48[3]1&&(>(i51[2]1, 1), >(+(i48[2]1, 1), 0))=TRUE+(i48[3]1, 1)=i48[2]2-(i51[3]1, 2)=i51[2]2i33[3]1=i33[2]2i36[3]1=i36[2]2i36[2]2=i36[3]2i51[2]2=i51[3]2i33[2]2=i33[3]2i48[2]2=i48[3]2&&(>(i51[2]2, 1), >(+(i48[2]2, 1), 0))=TRUECOND_LOAD583(TRUE, i36[3]1, i33[3]1, i51[3]1, i48[3]1)≥NonInfC∧COND_LOAD583(TRUE, i36[3]1, i33[3]1, i51[3]1, i48[3]1)≥LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))∧(UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥))

We simplified constraint (92) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

(93)    (>(i51[2], 1)=TRUE>(+(i48[2], 1), 0)=TRUE>(-(i51[2], 2), 1)=TRUE>(+(+(i48[2], 1), 1), 0)=TRUE>(-(-(i51[2], 2), 2), 1)=TRUE>(+(+(+(i48[2], 1), 1), 1), 0)=TRUECOND_LOAD583(TRUE, i36[2], i33[2], -(i51[2], 2), +(i48[2], 1))≥NonInfC∧COND_LOAD583(TRUE, i36[2], i33[2], -(i51[2], 2), +(i48[2], 1))≥LOAD583(i36[2], i33[2], -(-(i51[2], 2), 2), +(+(i48[2], 1), 1))∧(UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥))

We simplified constraint (93) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(94)    (i51[2] + [-2] ≥ 0∧i48[2] ≥ 0∧i51[2] + [-4] ≥ 0∧i48[2] + [1] ≥ 0∧i51[2] + [-6] ≥ 0∧i48[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (94) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(95)    (i51[2] + [-2] ≥ 0∧i48[2] ≥ 0∧i51[2] + [-4] ≥ 0∧i48[2] + [1] ≥ 0∧i51[2] + [-6] ≥ 0∧i48[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (95) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(96)    (i51[2] + [-2] ≥ 0∧i48[2] ≥ 0∧i51[2] + [-4] ≥ 0∧i48[2] + [1] ≥ 0∧i51[2] + [-6] ≥ 0∧i48[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (96) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(97)    (i51[2] + [-2] ≥ 0∧i48[2] ≥ 0∧i51[2] + [-4] ≥ 0∧i48[2] + [1] ≥ 0∧i51[2] + [-6] ≥ 0∧i48[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (97) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(98)    (i51[2] ≥ 0∧i48[2] ≥ 0∧[-2] + i51[2] ≥ 0∧i48[2] + [1] ≥ 0∧[-4] + i51[2] ≥ 0∧i48[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (98) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(99)    ([2] + i51[2] ≥ 0∧i48[2] ≥ 0∧i51[2] ≥ 0∧i48[2] + [1] ≥ 0∧[-2] + i51[2] ≥ 0∧i48[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (99) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(100)    ([4] + i51[2] ≥ 0∧i48[2] ≥ 0∧[2] + i51[2] ≥ 0∧i48[2] + [1] ≥ 0∧i51[2] ≥ 0∧i48[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(4)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (100) using rule (IDP_POLY_GCD) which results in the following new constraint:

(101)    ([4] + i51[2] ≥ 0∧i48[2] ≥ 0∧[2] + i51[2] ≥ 0∧i48[2] + [1] ≥ 0∧i51[2] ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(4)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)

(102)    (i36[2]=i36[3]i51[2]=i51[3]i33[2]=i33[3]i48[2]=i48[3]&&(>(i51[2], 1), >(+(i48[2], 1), 0))=TRUE+(i48[3], 1)=i48[2]1-(i51[3], 2)=i51[2]1i33[3]=i33[2]1i36[3]=i36[2]1i36[2]1=i36[3]1i51[2]1=i51[3]1i33[2]1=i33[3]1i48[2]1=i48[3]1&&(>(i51[2]1, 1), >(+(i48[2]1, 1), 0))=TRUE+(i48[3]1, 1)=i48[4]i36[3]1=i36[4]i33[3]1=i33[4]-(i51[3]1, 2)=i51[4]&&(>(i51[4], 0), <=(i51[4], 1))=TRUEi36[4]=i36[5]i51[4]=i51[5]i48[4]=i48[5]i33[4]=i33[5]COND_LOAD583(TRUE, i36[3]1, i33[3]1, i51[3]1, i48[3]1)≥NonInfC∧COND_LOAD583(TRUE, i36[3]1, i33[3]1, i51[3]1, i48[3]1)≥LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))∧(UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥))

We simplified constraint (102) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

(103)    (>(i51[2], 1)=TRUE>(+(i48[2], 1), 0)=TRUE>(-(i51[2], 2), 1)=TRUE>(+(+(i48[2], 1), 1), 0)=TRUE>(-(-(i51[2], 2), 2), 0)=TRUE<=(-(-(i51[2], 2), 2), 1)=TRUECOND_LOAD583(TRUE, i36[2], i33[2], -(i51[2], 2), +(i48[2], 1))≥NonInfC∧COND_LOAD583(TRUE, i36[2], i33[2], -(i51[2], 2), +(i48[2], 1))≥LOAD583(i36[2], i33[2], -(-(i51[2], 2), 2), +(+(i48[2], 1), 1))∧(UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥))

We simplified constraint (103) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(104)    (i51[2] + [-2] ≥ 0∧i48[2] ≥ 0∧i51[2] + [-4] ≥ 0∧i48[2] + [1] ≥ 0∧i51[2] + [-5] ≥ 0∧[5] + [-1]i51[2] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (104) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(105)    (i51[2] + [-2] ≥ 0∧i48[2] ≥ 0∧i51[2] + [-4] ≥ 0∧i48[2] + [1] ≥ 0∧i51[2] + [-5] ≥ 0∧[5] + [-1]i51[2] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (105) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(106)    (i51[2] + [-2] ≥ 0∧i48[2] ≥ 0∧i51[2] + [-4] ≥ 0∧i48[2] + [1] ≥ 0∧i51[2] + [-5] ≥ 0∧[5] + [-1]i51[2] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (106) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(107)    (i51[2] + [-2] ≥ 0∧i48[2] ≥ 0∧i51[2] + [-4] ≥ 0∧i48[2] + [1] ≥ 0∧i51[2] + [-5] ≥ 0∧[5] + [-1]i51[2] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (107) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(108)    (i51[2] ≥ 0∧i48[2] ≥ 0∧[-2] + i51[2] ≥ 0∧i48[2] + [1] ≥ 0∧[-3] + i51[2] ≥ 0∧[3] + [-1]i51[2] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (108) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(109)    ([2] + i51[2] ≥ 0∧i48[2] ≥ 0∧i51[2] ≥ 0∧i48[2] + [1] ≥ 0∧[-1] + i51[2] ≥ 0∧[1] + [-1]i51[2] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (109) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(110)    ([3] + i51[2] ≥ 0∧i48[2] ≥ 0∧[1] + i51[2] ≥ 0∧i48[2] + [1] ≥ 0∧i51[2] ≥ 0∧[-1]i51[2] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(3)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (110) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(111)    ([3] ≥ 0∧i48[2] ≥ 0∧[1] ≥ 0∧i48[2] + [1] ≥ 0∧0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(3)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (111) using rule (IDP_POLY_GCD) which results in the following new constraint:

(112)    (i48[2] ≥ 0∧[1] ≥ 0∧i48[2] + [1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(3)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)

(113)    (i36[2]=i36[3]i51[2]=i51[3]i33[2]=i33[3]i48[2]=i48[3]&&(>(i51[2], 1), >(+(i48[2], 1), 0))=TRUE+(i48[3], 1)=i48[2]1-(i51[3], 2)=i51[2]1i33[3]=i33[2]1i36[3]=i36[2]1i36[2]1=i36[3]1i51[2]1=i51[3]1i33[2]1=i33[3]1i48[2]1=i48[3]1&&(>(i51[2]1, 1), >(+(i48[2]1, 1), 0))=TRUE+(i48[3]1, 1)=i48[7]-(i51[3]1, 2)=i50[7]i36[3]1=i36[7]i33[3]1=i33[7]i50[7]=i50[8]i33[7]=i33[8]i36[7]=i36[8]i48[7]=i48[8]&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0))=TRUECOND_LOAD583(TRUE, i36[3]1, i33[3]1, i51[3]1, i48[3]1)≥NonInfC∧COND_LOAD583(TRUE, i36[3]1, i33[3]1, i51[3]1, i48[3]1)≥LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))∧(UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥))

We simplified constraint (113) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

(114)    (>(i51[2], 1)=TRUE>(+(i48[2], 1), 0)=TRUE>(-(i51[2], 2), 1)=TRUE>(+(+(i48[2], 1), 1), 0)=TRUE>(+(+(+(i48[2], 1), 1), 1), 0)=TRUE<=(-(-(i51[2], 2), 2), 1)=TRUE>(+(i33[7], 1), 0)=TRUECOND_LOAD583(TRUE, i36[2], i33[7], -(i51[2], 2), +(i48[2], 1))≥NonInfC∧COND_LOAD583(TRUE, i36[2], i33[7], -(i51[2], 2), +(i48[2], 1))≥LOAD583(i36[2], i33[7], -(-(i51[2], 2), 2), +(+(i48[2], 1), 1))∧(UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥))

We simplified constraint (114) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(115)    (i51[2] + [-2] ≥ 0∧i48[2] ≥ 0∧i51[2] + [-4] ≥ 0∧i48[2] + [1] ≥ 0∧i48[2] + [2] ≥ 0∧[5] + [-1]i51[2] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (115) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(116)    (i51[2] + [-2] ≥ 0∧i48[2] ≥ 0∧i51[2] + [-4] ≥ 0∧i48[2] + [1] ≥ 0∧i48[2] + [2] ≥ 0∧[5] + [-1]i51[2] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (116) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(117)    (i51[2] + [-2] ≥ 0∧i48[2] ≥ 0∧i51[2] + [-4] ≥ 0∧i48[2] + [1] ≥ 0∧i48[2] + [2] ≥ 0∧[5] + [-1]i51[2] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (117) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(118)    (i51[2] + [-2] ≥ 0∧i48[2] ≥ 0∧i51[2] + [-4] ≥ 0∧i48[2] + [1] ≥ 0∧i48[2] + [2] ≥ 0∧[5] + [-1]i51[2] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧0 = 0∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (118) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(119)    (i51[2] ≥ 0∧i48[2] ≥ 0∧[-2] + i51[2] ≥ 0∧i48[2] + [1] ≥ 0∧i48[2] + [2] ≥ 0∧[3] + [-1]i51[2] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧0 = 0∧[(-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (119) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(120)    ([2] + i51[2] ≥ 0∧i48[2] ≥ 0∧i51[2] ≥ 0∧i48[2] + [1] ≥ 0∧i48[2] + [2] ≥ 0∧[1] + [-1]i51[2] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (120) using rule (IDP_POLY_GCD) which results in the following new constraint:

(121)    ([2] + i51[2] ≥ 0∧i48[2] ≥ 0∧i51[2] ≥ 0∧i48[2] + [1] ≥ 0∧[1] + [-1]i51[2] ≥ 0∧i33[7] ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧0 = 0∧[(-1)bso_47] ≥ 0)

For Pair LOAD583(i36, i33, i51, i48) → COND_LOAD5831(&&(>(i51, 0), <=(i51, 1)), i36, i33, i51, i48) the following chains were created:
• We consider the chain LOAD583(i36[4], i33[4], i51[4], i48[4]) → COND_LOAD5831(&&(>(i51[4], 0), <=(i51[4], 1)), i36[4], i33[4], i51[4], i48[4]), COND_LOAD5831(TRUE, i36[5], i33[5], i51[5], i48[5]) → LOAD594(i36[5], i33[5], i48[5]) which results in the following constraint:

(122)    (&&(>(i51[4], 0), <=(i51[4], 1))=TRUEi36[4]=i36[5]i51[4]=i51[5]i48[4]=i48[5]i33[4]=i33[5]LOAD583(i36[4], i33[4], i51[4], i48[4])≥NonInfC∧LOAD583(i36[4], i33[4], i51[4], i48[4])≥COND_LOAD5831(&&(>(i51[4], 0), <=(i51[4], 1)), i36[4], i33[4], i51[4], i48[4])∧(UIncreasing(COND_LOAD5831(&&(>(i51[4], 0), <=(i51[4], 1)), i36[4], i33[4], i51[4], i48[4])), ≥))

We simplified constraint (122) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:

(123)    (>(i51[4], 0)=TRUE<=(i51[4], 1)=TRUELOAD583(i36[4], i33[4], i51[4], i48[4])≥NonInfC∧LOAD583(i36[4], i33[4], i51[4], i48[4])≥COND_LOAD5831(&&(>(i51[4], 0), <=(i51[4], 1)), i36[4], i33[4], i51[4], i48[4])∧(UIncreasing(COND_LOAD5831(&&(>(i51[4], 0), <=(i51[4], 1)), i36[4], i33[4], i51[4], i48[4])), ≥))

We simplified constraint (123) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(124)    (i51[4] + [-1] ≥ 0∧[1] + [-1]i51[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD5831(&&(>(i51[4], 0), <=(i51[4], 1)), i36[4], i33[4], i51[4], i48[4])), ≥)∧[(-1)Bound*bni_48] + [bni_48]i48[4] + [bni_48]i51[4] ≥ 0∧[-1 + (-1)bso_49] + i51[4] ≥ 0)

We simplified constraint (124) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(125)    (i51[4] + [-1] ≥ 0∧[1] + [-1]i51[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD5831(&&(>(i51[4], 0), <=(i51[4], 1)), i36[4], i33[4], i51[4], i48[4])), ≥)∧[(-1)Bound*bni_48] + [bni_48]i48[4] + [bni_48]i51[4] ≥ 0∧[-1 + (-1)bso_49] + i51[4] ≥ 0)

We simplified constraint (125) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(126)    (i51[4] + [-1] ≥ 0∧[1] + [-1]i51[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD5831(&&(>(i51[4], 0), <=(i51[4], 1)), i36[4], i33[4], i51[4], i48[4])), ≥)∧[(-1)Bound*bni_48] + [bni_48]i48[4] + [bni_48]i51[4] ≥ 0∧[-1 + (-1)bso_49] + i51[4] ≥ 0)

We simplified constraint (126) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(127)    (i51[4] + [-1] ≥ 0∧[1] + [-1]i51[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD5831(&&(>(i51[4], 0), <=(i51[4], 1)), i36[4], i33[4], i51[4], i48[4])), ≥)∧[bni_48] = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_48] + [bni_48]i51[4] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[-1 + (-1)bso_49] + i51[4] ≥ 0)

We simplified constraint (127) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(128)    (i51[4] ≥ 0∧[-1]i51[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD5831(&&(>(i51[4], 0), <=(i51[4], 1)), i36[4], i33[4], i51[4], i48[4])), ≥)∧[bni_48] = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_48 + bni_48] + [bni_48]i51[4] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_49] + i51[4] ≥ 0)

We simplified constraint (128) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(129)    (0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(COND_LOAD5831(&&(>(i51[4], 0), <=(i51[4], 1)), i36[4], i33[4], i51[4], i48[4])), ≥)∧[bni_48] = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_48 + bni_48] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_49] ≥ 0)

For Pair COND_LOAD5831(TRUE, i36, i33, i51, i48) → LOAD594(i36, i33, i48) the following chains were created:
• We consider the chain COND_LOAD5831(TRUE, i36[5], i33[5], i51[5], i48[5]) → LOAD594(i36[5], i33[5], i48[5]), LOAD594(i36[6], i33[6], i48[6]) → LOAD416(+(i48[6], 1), +(i33[6], 1)) which results in the following constraint:

We simplified constraint (130) using rule (IV) which results in the following new constraint:

We simplified constraint (131) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(132)    ((UIncreasing(LOAD594(i36[5], i33[5], i48[5])), ≥)∧[(-1)bso_51] ≥ 0)

We simplified constraint (132) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(133)    ((UIncreasing(LOAD594(i36[5], i33[5], i48[5])), ≥)∧[(-1)bso_51] ≥ 0)

We simplified constraint (133) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(134)    ((UIncreasing(LOAD594(i36[5], i33[5], i48[5])), ≥)∧[(-1)bso_51] ≥ 0)

We simplified constraint (134) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(135)    ((UIncreasing(LOAD594(i36[5], i33[5], i48[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_51] ≥ 0)

For Pair LOAD594(i36, i33, i48) → LOAD416(+(i48, 1), +(i33, 1)) the following chains were created:

We solved constraint (136) using rules (I), (II), (III), (IV), (IDP_CONSTANT_FOLD), (IDP_BOOLEAN).

We simplified constraint (137) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

(138)    (>(+(+(i48[3], 1), 1), 1)=TRUE>(-(i51[3], 2), 0)=TRUE<=(-(i51[3], 2), 1)=TRUELOAD594(i36[3], i33[3], +(i48[3], 1))≥NonInfC∧LOAD594(i36[3], i33[3], +(i48[3], 1))≥LOAD416(+(+(i48[3], 1), 1), +(i33[3], 1))∧(UIncreasing(LOAD416(+(i48[6], 1), +(i33[6], 1))), ≥))

We simplified constraint (138) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(139)    (i48[3] ≥ 0∧i51[3] + [-3] ≥ 0∧[3] + [-1]i51[3] ≥ 0 ⇒ (UIncreasing(LOAD416(+(i48[6], 1), +(i33[6], 1))), ≥)∧[bni_52 + (-1)Bound*bni_52] + [bni_52]i48[3] ≥ 0∧[(-1)bso_53] ≥ 0)

We simplified constraint (139) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(140)    (i48[3] ≥ 0∧i51[3] + [-3] ≥ 0∧[3] + [-1]i51[3] ≥ 0 ⇒ (UIncreasing(LOAD416(+(i48[6], 1), +(i33[6], 1))), ≥)∧[bni_52 + (-1)Bound*bni_52] + [bni_52]i48[3] ≥ 0∧[(-1)bso_53] ≥ 0)

We simplified constraint (140) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(141)    (i48[3] ≥ 0∧i51[3] + [-3] ≥ 0∧[3] + [-1]i51[3] ≥ 0 ⇒ (UIncreasing(LOAD416(+(i48[6], 1), +(i33[6], 1))), ≥)∧[bni_52 + (-1)Bound*bni_52] + [bni_52]i48[3] ≥ 0∧[(-1)bso_53] ≥ 0)

We simplified constraint (141) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:

(142)    (i48[3] ≥ 0∧[3] + [-1]i51[3] ≥ 0∧[-1] ≥ 0 ⇒ (UIncreasing(LOAD416(+(i48[6], 1), +(i33[6], 1))), ≥)∧0 = 0∧0 = 0∧[bni_52 + (-1)Bound*bni_52] + [bni_52]i48[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_53] ≥ 0)

For Pair LOAD583(i36, i33, i50, i48) → COND_LOAD5832(&&(&&(<=(i50, 1), >(+(i33, 1), 0)), >(+(i48, 1), 0)), i36, i33, i50, i48) the following chains were created:
• We consider the chain LOAD583(i36[7], i33[7], i50[7], i48[7]) → COND_LOAD5832(&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0)), i36[7], i33[7], i50[7], i48[7]), COND_LOAD5832(TRUE, i36[8], i33[8], i50[8], i48[8]) → LOAD416(+(i48[8], 1), +(i33[8], 1)) which results in the following constraint:

(143)    (i50[7]=i50[8]i33[7]=i33[8]i36[7]=i36[8]i48[7]=i48[8]&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0))=TRUELOAD583(i36[7], i33[7], i50[7], i48[7])≥NonInfC∧LOAD583(i36[7], i33[7], i50[7], i48[7])≥COND_LOAD5832(&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0)), i36[7], i33[7], i50[7], i48[7])∧(UIncreasing(COND_LOAD5832(&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0)), i36[7], i33[7], i50[7], i48[7])), ≥))

We simplified constraint (143) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:

(144)    (>(+(i48[7], 1), 0)=TRUE<=(i50[7], 1)=TRUE>(+(i33[7], 1), 0)=TRUELOAD583(i36[7], i33[7], i50[7], i48[7])≥NonInfC∧LOAD583(i36[7], i33[7], i50[7], i48[7])≥COND_LOAD5832(&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0)), i36[7], i33[7], i50[7], i48[7])∧(UIncreasing(COND_LOAD5832(&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0)), i36[7], i33[7], i50[7], i48[7])), ≥))

We simplified constraint (144) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(145)    (i48[7] ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD5832(&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0)), i36[7], i33[7], i50[7], i48[7])), ≥)∧[(-1)Bound*bni_54] + [bni_54]i48[7] + [bni_54]i50[7] ≥ 0∧[(-1)bso_55] ≥ 0)

We simplified constraint (145) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(146)    (i48[7] ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD5832(&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0)), i36[7], i33[7], i50[7], i48[7])), ≥)∧[(-1)Bound*bni_54] + [bni_54]i48[7] + [bni_54]i50[7] ≥ 0∧[(-1)bso_55] ≥ 0)

We simplified constraint (146) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(147)    (i48[7] ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD5832(&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0)), i36[7], i33[7], i50[7], i48[7])), ≥)∧[(-1)Bound*bni_54] + [bni_54]i48[7] + [bni_54]i50[7] ≥ 0∧[(-1)bso_55] ≥ 0)

We simplified constraint (147) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(148)    (i48[7] ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD5832(&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0)), i36[7], i33[7], i50[7], i48[7])), ≥)∧0 = 0∧[(-1)Bound*bni_54] + [bni_54]i48[7] + [bni_54]i50[7] ≥ 0∧0 = 0∧[(-1)bso_55] ≥ 0)

We simplified constraint (148) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

(149)    (i48[7] ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0∧i50[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD5832(&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0)), i36[7], i33[7], i50[7], i48[7])), ≥)∧0 = 0∧[(-1)Bound*bni_54] + [bni_54]i48[7] + [bni_54]i50[7] ≥ 0∧0 = 0∧[(-1)bso_55] ≥ 0)

(150)    (i48[7] ≥ 0∧[1] + i50[7] ≥ 0∧i33[7] ≥ 0∧i50[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD5832(&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0)), i36[7], i33[7], i50[7], i48[7])), ≥)∧0 = 0∧[(-1)Bound*bni_54] + [bni_54]i48[7] + [(-1)bni_54]i50[7] ≥ 0∧0 = 0∧[(-1)bso_55] ≥ 0)

For Pair COND_LOAD5832(TRUE, i36, i33, i50, i48) → LOAD416(+(i48, 1), +(i33, 1)) the following chains were created:

(151)    (i33[0]=i33[1]>(i36[0], 1)=TRUEi36[0]=i36[1]-(i36[1], 2)=i50[7]i33[1]=i33[7]0=i48[7]i36[1]=i36[7]i50[7]=i50[8]i33[7]=i33[8]i36[7]=i36[8]i48[7]=i48[8]&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0))=TRUE+(i48[8], 1)=i36[0]1+(i33[8], 1)=i33[0]1i33[0]1=i33[1]1>(i36[0]1, 1)=TRUEi36[0]1=i36[1]1COND_LOAD5832(TRUE, i36[8], i33[8], i50[8], i48[8])≥NonInfC∧COND_LOAD5832(TRUE, i36[8], i33[8], i50[8], i48[8])≥LOAD416(+(i48[8], 1), +(i33[8], 1))∧(UIncreasing(LOAD416(+(i48[8], 1), +(i33[8], 1))), ≥))

We solved constraint (151) using rules (I), (II), (III), (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN).

(152)    (i36[2]=i36[3]i51[2]=i51[3]i33[2]=i33[3]i48[2]=i48[3]&&(>(i51[2], 1), >(+(i48[2], 1), 0))=TRUE+(i48[3], 1)=i48[7]-(i51[3], 2)=i50[7]i36[3]=i36[7]i33[3]=i33[7]i50[7]=i50[8]i33[7]=i33[8]i36[7]=i36[8]i48[7]=i48[8]&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0))=TRUE+(i48[8], 1)=i36[0]+(i33[8], 1)=i33[0]i33[0]=i33[1]>(i36[0], 1)=TRUEi36[0]=i36[1]COND_LOAD5832(TRUE, i36[8], i33[8], i50[8], i48[8])≥NonInfC∧COND_LOAD5832(TRUE, i36[8], i33[8], i50[8], i48[8])≥LOAD416(+(i48[8], 1), +(i33[8], 1))∧(UIncreasing(LOAD416(+(i48[8], 1), +(i33[8], 1))), ≥))

We simplified constraint (152) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

(153)    (>(+(+(i48[2], 1), 1), 1)=TRUE>(i51[2], 1)=TRUE>(+(i48[2], 1), 0)=TRUE>(+(+(i48[2], 1), 1), 0)=TRUE<=(-(i51[2], 2), 1)=TRUE>(+(i33[7], 1), 0)=TRUECOND_LOAD5832(TRUE, i36[2], i33[7], -(i51[2], 2), +(i48[2], 1))≥NonInfC∧COND_LOAD5832(TRUE, i36[2], i33[7], -(i51[2], 2), +(i48[2], 1))≥LOAD416(+(+(i48[2], 1), 1), +(i33[7], 1))∧(UIncreasing(LOAD416(+(i48[8], 1), +(i33[8], 1))), ≥))

We simplified constraint (153) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(154)    (i48[2] ≥ 0∧i51[2] + [-2] ≥ 0∧i48[2] ≥ 0∧i48[2] + [1] ≥ 0∧[3] + [-1]i51[2] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD416(+(i48[8], 1), +(i33[8], 1))), ≥)∧[(-1)bni_56 + (-1)Bound*bni_56] + [bni_56]i48[2] + [bni_56]i51[2] ≥ 0∧[-2 + (-1)bso_57] + i51[2] ≥ 0)

We simplified constraint (154) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(155)    (i48[2] ≥ 0∧i51[2] + [-2] ≥ 0∧i48[2] ≥ 0∧i48[2] + [1] ≥ 0∧[3] + [-1]i51[2] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD416(+(i48[8], 1), +(i33[8], 1))), ≥)∧[(-1)bni_56 + (-1)Bound*bni_56] + [bni_56]i48[2] + [bni_56]i51[2] ≥ 0∧[-2 + (-1)bso_57] + i51[2] ≥ 0)

We simplified constraint (155) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(156)    (i48[2] ≥ 0∧i51[2] + [-2] ≥ 0∧i48[2] ≥ 0∧i48[2] + [1] ≥ 0∧[3] + [-1]i51[2] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD416(+(i48[8], 1), +(i33[8], 1))), ≥)∧[(-1)bni_56 + (-1)Bound*bni_56] + [bni_56]i48[2] + [bni_56]i51[2] ≥ 0∧[-2 + (-1)bso_57] + i51[2] ≥ 0)

We simplified constraint (156) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(157)    (i48[2] ≥ 0∧i51[2] + [-2] ≥ 0∧i48[2] ≥ 0∧i48[2] + [1] ≥ 0∧[3] + [-1]i51[2] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD416(+(i48[8], 1), +(i33[8], 1))), ≥)∧0 = 0∧[(-1)bni_56 + (-1)Bound*bni_56] + [bni_56]i48[2] + [bni_56]i51[2] ≥ 0∧0 = 0∧[-2 + (-1)bso_57] + i51[2] ≥ 0)

We simplified constraint (157) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(158)    (i48[2] ≥ 0∧i51[2] ≥ 0∧i48[2] ≥ 0∧i48[2] + [1] ≥ 0∧[1] + [-1]i51[2] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD416(+(i48[8], 1), +(i33[8], 1))), ≥)∧0 = 0∧[bni_56 + (-1)Bound*bni_56] + [bni_56]i48[2] + [bni_56]i51[2] ≥ 0∧0 = 0∧[(-1)bso_57] + i51[2] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• (i36[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD416(>(i36[0], 1), i36[0], i33[0])), ≥)∧0 = 0∧[bni_40 + (-1)Bound*bni_40] + [bni_40]i36[0] ≥ 0∧0 = 0∧[(-1)bso_41] ≥ 0)

• ([2] + i48[6] ≥ 0∧i48[6] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧0 = 0∧[(-1)Bound*bni_42 + (3)bni_42] + [bni_42]i48[6] ≥ 0∧0 = 0∧[1 + (-1)bso_43] ≥ 0)
• ([1] ≥ 0∧0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧0 = 0∧[(-1)Bound*bni_42 + (2)bni_42] ≥ 0∧0 = 0∧[1 + (-1)bso_43] ≥ 0)
• (i48[6] ≥ 0∧[1] + [-1]i48[6] ≥ 0∧i33[6] + [1] ≥ 0∧i33[6] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42 + bni_42] + [bni_42]i48[6] ≥ 0∧[1 + (-1)bso_43] ≥ 0)
• (i48[6] ≥ 0∧[1] + [-1]i48[6] ≥ 0∧[-1]i33[6] + [1] ≥ 0∧i33[6] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42 + bni_42] + [bni_42]i48[6] ≥ 0∧[1 + (-1)bso_43] ≥ 0)
• ([2] + i48[7] ≥ 0∧[3] + i48[7] ≥ 0∧i48[7] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42 + (3)bni_42] + [bni_42]i48[7] ≥ 0∧[1 + (-1)bso_43] ≥ 0)
• ([1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧i33[7] ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42 + (2)bni_42] ≥ 0∧[1 + (-1)bso_43] ≥ 0)
• (i48[7] ≥ 0∧[1] + i48[7] ≥ 0∧i33[7] ≥ 0∧[1] + [-1]i48[7] ≥ 0∧i33[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[1], i33[1], -(i36[1], 2), 0)), ≥)∧[(-1)Bound*bni_42 + bni_42] + [bni_42]i48[7] ≥ 0∧[1 + (-1)bso_43] ≥ 0)

• LOAD583(i36, i33, i51, i48) → COND_LOAD583(&&(>(i51, 1), >(+(i48, 1), 0)), i36, i33, i51, i48)
• (i51[2] ≥ 0∧i48[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD583(&&(>(i51[2], 1), >(+(i48[2], 1), 0)), i36[2], i33[2], i51[2], i48[2])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_44 + (2)bni_44] + [bni_44]i48[2] + [bni_44]i51[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_45] ≥ 0)

• COND_LOAD583(TRUE, i36, i33, i51, i48) → LOAD583(i36, i33, -(i51, 2), +(i48, 1))
• ([4] + i36[0] ≥ 0∧[2] + i36[0] ≥ 0∧i36[0] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧0 = 0∧[(3)bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧0 = 0∧[(-1)bso_47] ≥ 0)
• ([1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] ≥ 0∧0 = 0∧[(-1)bso_47] ≥ 0)
• ([2] + i36[0] ≥ 0∧i36[0] ≥ 0∧[1] + [-1]i36[0] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))), ≥)∧[bni_46 + (-1)Bound*bni_46] + [bni_46]i36[0] ≥ 0∧[(-1)bso_47] ≥ 0)
• ([4] + i51[2] ≥ 0∧i48[2] ≥ 0∧[2] + i51[2] ≥ 0∧i48[2] + [1] ≥ 0∧i51[2] ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(4)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)
• (i48[2] ≥ 0∧[1] ≥ 0∧i48[2] + [1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(3)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)
• ([2] + i51[2] ≥ 0∧i48[2] ≥ 0∧i51[2] ≥ 0∧i48[2] + [1] ≥ 0∧[1] + [-1]i51[2] ≥ 0∧i33[7] ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD583(i36[3]1, i33[3]1, -(i51[3]1, 2), +(i48[3]1, 1))), ≥)∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] + [bni_46]i48[2] + [bni_46]i51[2] ≥ 0∧0 = 0∧[(-1)bso_47] ≥ 0)

• LOAD583(i36, i33, i51, i48) → COND_LOAD5831(&&(>(i51, 0), <=(i51, 1)), i36, i33, i51, i48)
• (0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(COND_LOAD5831(&&(>(i51[4], 0), <=(i51[4], 1)), i36[4], i33[4], i51[4], i48[4])), ≥)∧[bni_48] = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_48 + bni_48] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_49] ≥ 0)

• ((UIncreasing(LOAD594(i36[5], i33[5], i48[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_51] ≥ 0)

• (i48[3] ≥ 0∧[3] + [-1]i51[3] ≥ 0∧[-1] ≥ 0 ⇒ (UIncreasing(LOAD416(+(i48[6], 1), +(i33[6], 1))), ≥)∧0 = 0∧0 = 0∧[bni_52 + (-1)Bound*bni_52] + [bni_52]i48[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_53] ≥ 0)

• LOAD583(i36, i33, i50, i48) → COND_LOAD5832(&&(&&(<=(i50, 1), >(+(i33, 1), 0)), >(+(i48, 1), 0)), i36, i33, i50, i48)
• (i48[7] ≥ 0∧[1] + [-1]i50[7] ≥ 0∧i33[7] ≥ 0∧i50[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD5832(&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0)), i36[7], i33[7], i50[7], i48[7])), ≥)∧0 = 0∧[(-1)Bound*bni_54] + [bni_54]i48[7] + [bni_54]i50[7] ≥ 0∧0 = 0∧[(-1)bso_55] ≥ 0)
• (i48[7] ≥ 0∧[1] + i50[7] ≥ 0∧i33[7] ≥ 0∧i50[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD5832(&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0)), i36[7], i33[7], i50[7], i48[7])), ≥)∧0 = 0∧[(-1)Bound*bni_54] + [bni_54]i48[7] + [(-1)bni_54]i50[7] ≥ 0∧0 = 0∧[(-1)bso_55] ≥ 0)

• (i48[2] ≥ 0∧i51[2] ≥ 0∧i48[2] ≥ 0∧i48[2] + [1] ≥ 0∧[1] + [-1]i51[2] ≥ 0∧i33[7] ≥ 0 ⇒ (UIncreasing(LOAD416(+(i48[8], 1), +(i33[8], 1))), ≥)∧0 = 0∧[bni_56 + (-1)Bound*bni_56] + [bni_56]i48[2] + [bni_56]i51[2] ≥ 0∧0 = 0∧[(-1)bso_57] + i51[2] ≥ 0)

The constraints for P> respective Pbound are constructed from P where we just replace every occurence of "t ≥ s" in P by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(LOAD416(x1, x2)) = [-1] + x1
POL(COND_LOAD416(x1, x2, x3)) = [-1] + x2
POL(>(x1, x2)) = [-1]
POL(1) = [1]
POL(LOAD583(x1, x2, x3, x4)) = x4 + x3
POL(-(x1, x2)) = x1 + [-1]x2
POL(2) = [2]
POL(0) = 0
POL(COND_LOAD583(x1, x2, x3, x4, x5)) = [-1] + x5 + x4
POL(&&(x1, x2)) = [-1]
POL(+(x1, x2)) = x1 + x2
POL(COND_LOAD5831(x1, x2, x3, x4, x5)) = x5 + [-1]x1
POL(<=(x1, x2)) = [-1]
POL(COND_LOAD5832(x1, x2, x3, x4, x5)) = x5 + x4

The following pairs are in P>:

LOAD583(i36[2], i33[2], i51[2], i48[2]) → COND_LOAD583(&&(>(i51[2], 1), >(+(i48[2], 1), 0)), i36[2], i33[2], i51[2], i48[2])

The following pairs are in Pbound:

LOAD583(i36[2], i33[2], i51[2], i48[2]) → COND_LOAD583(&&(>(i51[2], 1), >(+(i48[2], 1), 0)), i36[2], i33[2], i51[2], i48[2])
COND_LOAD583(TRUE, i36[3], i33[3], i51[3], i48[3]) → LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))

The following pairs are in P:

COND_LOAD583(TRUE, i36[3], i33[3], i51[3], i48[3]) → LOAD583(i36[3], i33[3], -(i51[3], 2), +(i48[3], 1))
LOAD583(i36[4], i33[4], i51[4], i48[4]) → COND_LOAD5831(&&(>(i51[4], 0), <=(i51[4], 1)), i36[4], i33[4], i51[4], i48[4])
LOAD583(i36[7], i33[7], i50[7], i48[7]) → COND_LOAD5832(&&(&&(<=(i50[7], 1), >(+(i33[7], 1), 0)), >(+(i48[7], 1), 0)), i36[7], i33[7], i50[7], i48[7])

At least the following rules have been oriented under context sensitive arithmetic replacement:

TRUE1&&(TRUE, TRUE)1
FALSE1&&(TRUE, FALSE)1
FALSE1&&(FALSE, TRUE)1
FALSE1&&(FALSE, FALSE)1

### (13) Obligation:

IDP problem:
The following function symbols are pre-defined:
 != ~ Neq: (Integer, Integer) -> Boolean * ~ Mul: (Integer, Integer) -> Integer >= ~ Ge: (Integer, Integer) -> Boolean -1 ~ UnaryMinus: (Integer) -> Integer | ~ Bwor: (Integer, Integer) -> Integer / ~ Div: (Integer, Integer) -> Integer = ~ Eq: (Integer, Integer) -> Boolean ~ Bwxor: (Integer, Integer) -> Integer || ~ Lor: (Boolean, Boolean) -> Boolean ! ~ Lnot: (Boolean) -> Boolean < ~ Lt: (Integer, Integer) -> Boolean - ~ Sub: (Integer, Integer) -> Integer <= ~ Le: (Integer, Integer) -> Boolean > ~ Gt: (Integer, Integer) -> Boolean ~ ~ Bwnot: (Integer) -> Integer % ~ Mod: (Integer, Integer) -> Integer & ~ Bwand: (Integer, Integer) -> Integer + ~ Add: (Integer, Integer) -> Integer && ~ Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(3): COND_LOAD583(TRUE, i36[3], i33[3], i51[3], i48[3]) → LOAD583(i36[3], i33[3], i51[3] - 2, i48[3] + 1)
(4): LOAD583(i36[4], i33[4], i51[4], i48[4]) → COND_LOAD5831(i51[4] > 0 && i51[4] <= 1, i36[4], i33[4], i51[4], i48[4])
(7): LOAD583(i36[7], i33[7], i50[7], i48[7]) → COND_LOAD5832(i50[7] <= 1 && i33[7] + 1 > 0 && i48[7] + 1 > 0, i36[7], i33[7], i50[7], i48[7])
(8): COND_LOAD5832(TRUE, i36[8], i33[8], i50[8], i48[8]) → LOAD416(i48[8] + 1, i33[8] + 1)

(8) -> (0), if ((i48[8] + 1* i36[0])∧(i33[8] + 1* i33[0]))

(3) -> (4), if ((i48[3] + 1* i48[4])∧(i36[3]* i36[4])∧(i33[3]* i33[4])∧(i51[3] - 2* i51[4]))

(4) -> (5), if ((i51[4] > 0 && i51[4] <= 1* TRUE)∧(i36[4]* i36[5])∧(i51[4]* i51[5])∧(i48[4]* i48[5])∧(i33[4]* i33[5]))

(3) -> (7), if ((i48[3] + 1* i48[7])∧(i51[3] - 2* i50[7])∧(i36[3]* i36[7])∧(i33[3]* i33[7]))

(7) -> (8), if ((i50[7]* i50[8])∧(i33[7]* i33[8])∧(i36[7]* i36[8])∧(i48[7]* i48[8])∧(i50[7] <= 1 && i33[7] + 1 > 0 && i48[7] + 1 > 0* TRUE))

The set Q consists of the following terms:

### (14) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 6 less nodes.

### (16) Obligation:

IDP problem:
The following function symbols are pre-defined:
 != ~ Neq: (Integer, Integer) -> Boolean * ~ Mul: (Integer, Integer) -> Integer >= ~ Ge: (Integer, Integer) -> Boolean -1 ~ UnaryMinus: (Integer) -> Integer | ~ Bwor: (Integer, Integer) -> Integer / ~ Div: (Integer, Integer) -> Integer = ~ Eq: (Integer, Integer) -> Boolean ~ Bwxor: (Integer, Integer) -> Integer || ~ Lor: (Boolean, Boolean) -> Boolean ! ~ Lnot: (Boolean) -> Boolean < ~ Lt: (Integer, Integer) -> Boolean - ~ Sub: (Integer, Integer) -> Integer <= ~ Le: (Integer, Integer) -> Boolean > ~ Gt: (Integer, Integer) -> Boolean ~ ~ Bwnot: (Integer) -> Integer % ~ Mod: (Integer, Integer) -> Integer & ~ Bwand: (Integer, Integer) -> Integer + ~ Add: (Integer, Integer) -> Integer && ~ Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(4): LOAD583(i36[4], i33[4], i51[4], i48[4]) → COND_LOAD5831(i51[4] > 0 && i51[4] <= 1, i36[4], i33[4], i51[4], i48[4])
(7): LOAD583(i36[7], i33[7], i50[7], i48[7]) → COND_LOAD5832(i50[7] <= 1 && i33[7] + 1 > 0 && i48[7] + 1 > 0, i36[7], i33[7], i50[7], i48[7])

(4) -> (5), if ((i51[4] > 0 && i51[4] <= 1* TRUE)∧(i36[4]* i36[5])∧(i51[4]* i51[5])∧(i48[4]* i48[5])∧(i33[4]* i33[5]))

The set Q consists of the following terms: