0 JBC
↳1 JBC2FIG (⇐)
↳2 FIGraph
↳3 FIGtoITRSProof (⇐)
↳4 AND
↳5 ITRS
↳6 GroundTermsRemoverProof (⇔)
↳7 ITRS
↳8 DuplicateArgsRemoverProof (⇔)
↳9 ITRS
↳10 ITRStoIDPProof (⇔)
↳11 IDP
↳12 UsableRulesProof (⇔)
↳13 IDP
↳14 ItpfGraphProof (⇔)
↳15 IDP
↳16 IDPNonInfProof (⇐)
↳17 AND
↳18 IDP
↳19 IDependencyGraphProof (⇔)
↳20 IDP
↳21 IDPNonInfProof (⇐)
↳22 AND
↳23 IDP
↳24 IDependencyGraphProof (⇔)
↳25 IDP
↳26 IDPNonInfProof (⇐)
↳27 IDP
↳28 IDependencyGraphProof (⇔)
↳29 TRUE
↳30 IDP
↳31 IDependencyGraphProof (⇔)
↳32 TRUE
↳33 IDP
↳34 IDependencyGraphProof (⇔)
↳35 TRUE
↳36 ITRS
↳37 DuplicateArgsRemoverProof (⇔)
↳38 ITRS
↳39 ITRStoIDPProof (⇔)
↳40 IDP
↳41 UsableRulesProof (⇔)
↳42 IDP
↳43 ItpfGraphProof (⇔)
↳44 IDP
↳45 IDPNonInfProof (⇐)
↳46 AND
↳47 IDP
↳48 IDependencyGraphProof (⇔)
↳49 TRUE
↳50 IDP
↳51 IDependencyGraphProof (⇔)
↳52 TRUE
↳53 ITRS
↳54 ITRStoIDPProof (⇔)
↳55 IDP
↳56 UsableRulesProof (⇔)
↳57 IDP
↳58 ItpfGraphProof (⇔)
↳59 IDP
↳60 IDPNonInfProof (⇐)
↳61 AND
↳62 IDP
↳63 IDependencyGraphProof (⇔)
↳64 TRUE
↳65 IDP
↳66 IDependencyGraphProof (⇔)
↳67 TRUE
No human-readable program information known.
!= | ~ | 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 |
Cond_Load36072(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load36072(x1, x2, x3, x4, x5, x6, x7)
!= | ~ | 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 |
Load3607(x1, x2, x3, x4, x5, x6, x7) → Load3607(x1, x2, x4, x5, x6, x7)
Return3818(x1, x2, x3, x4, x5, x6) → Return3818(x1, x2, x4, x5, x6)
Load3637(x1, x2, x3, x4, x5, x6) → Load3637(x1, x2, x4, x5, x6)
JMP3960(x1, x2, x3, x4, x5, x6, x7) → JMP3960(x1, x2, x4, x5, x6, x7)
Cond_Load36073(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load36073(x1, x2, x3, x5, x7, x8)
Cond_Load36072(x1, x2, x3, x4, x5, x6, x7) → Cond_Load36072(x1, x2, x3, x5, x6, x7)
Cond_Load36071(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load36071(x1, x2, x3, x5, x6, x7, x8)
Cond_Load3607(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load3607(x1, x2, x3, x5, x6, x7, x8)
!= | ~ | 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 |
!= | ~ | 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 |
Boolean, Integer
(0) -> (1), if ((java.lang.Object(IntList(o1856[0], i480[0])) →* java.lang.Object(IntList(o1856[1], i480[1])))∧(i118[0] →* i118[1])∧(i477[0] →* i477[1])∧(java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])) →* java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1])))∧(java.lang.Object(ARRAY(i3[0], a2436data[0])) →* java.lang.Object(ARRAY(i3[1], a2436data[1]))))
(1) -> (2), if ((i118[1] > 0 && i118[1] < i3[1] && i477[1] > 0 && i118[1] + 1 > 0 →* TRUE)∧(i477[1] →* i477[2])∧(java.lang.Object(IntList(o1856[1], i480[1])) →* java.lang.Object(IntList(o1856[2], i480[2])))∧(java.lang.Object(ARRAY(i3[1], a2436data[1])) →* java.lang.Object(ARRAY(i3[2], a2436data[2])))∧(java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1])) →* java.lang.Object(java.lang.String(i771[2], i770[2], i772[2], a3255[2])))∧(i118[1] →* i118[2]))
(2) -> (4), if ((o1856[2] →* java.lang.Object(IntList(o3274[4], i1311[4])))∧(i118[2] + 1 →* i615[4])∧(i771[2] →* i1238[4])∧(java.lang.Object(ARRAY(i3[2], a2436data[2])) →* java.lang.Object(ARRAY(i3[4], a4210data[4])))∧(i477[2] →* i477[4])∧(o1856[2] →* o3142[4]))
(2) -> (6), if ((o1856[2] →* o3142[6])∧(java.lang.Object(ARRAY(i3[2], a2436data[2])) →* java.lang.Object(ARRAY(i3[6], a4210data[6])))∧(o1856[2] →* o3141[6])∧(i118[2] + 1 →* i615[6])∧(i771[2] →* i1238[6])∧(i477[2] →* i477[6]))
(2) -> (8), if ((i771[2] →* i1238[8])∧(java.lang.Object(ARRAY(i3[2], a2436data[2])) →* java.lang.Object(ARRAY(i3[8], a4210data[8])))∧(i477[2] →* i477[8])∧(i118[2] + 1 →* i615[8])∧(o1856[2] →* o3142[8])∧(o1856[2] →* NULL))
(2) -> (13), if ((i771[2] →* 0)∧(o1856[2] →* o3142[13])∧(i477[2] →* i477[13])∧(java.lang.Object(ARRAY(i3[2], a2436data[2])) →* java.lang.Object(ARRAY(i3[13], a4210data[13])))∧(o1856[2] →* java.lang.Object(IntList(o3234[13], i1289[13])))∧(i118[2] + 1 →* i615[13]))
(2) -> (14), if ((java.lang.Object(ARRAY(i3[2], a2436data[2])) →* java.lang.Object(ARRAY(i3[14], a4210data[14])))∧(i477[2] →* i477[14])∧(o1856[2] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(i771[2] →* i1238[14])∧(i118[2] + 1 →* i615[14]))
(2) -> (17), if ((java.lang.Object(ARRAY(i3[2], a2436data[2])) →* java.lang.Object(ARRAY(i3[17], a4210data[17])))∧(o1856[2] →* o3142[17])∧(i771[2] →* 0)∧(o1856[2] →* NULL)∧(i477[2] →* i477[17])∧(i118[2] + 1 →* i615[17]))
(2) -> (19), if ((o1856[2] →* java.lang.Object(IntList(o3239[19], i1291[19])))∧(i477[2] →* i477[19])∧(i771[2] →* 0)∧(java.lang.Object(ARRAY(i3[2], a2436data[2])) →* java.lang.Object(ARRAY(i3[19], a4210data[19])))∧(i118[2] + 1 →* i615[19]))
(3) -> (4), if ((i477[3] →* i477[4])∧(o3274[3] →* java.lang.Object(IntList(o3274[4], i1311[4])))∧(java.lang.Object(ARRAY(i3[3], a4210data[3])) →* java.lang.Object(ARRAY(i3[4], a4210data[4])))∧(i615[3] →* i615[4])∧(o3142[3] →* o3142[4])∧(i1284[3] →* i1238[4]))
(3) -> (6), if ((i615[3] →* i615[6])∧(i477[3] →* i477[6])∧(java.lang.Object(ARRAY(i3[3], a4210data[3])) →* java.lang.Object(ARRAY(i3[6], a4210data[6])))∧(o3142[3] →* o3142[6])∧(o3274[3] →* o3141[6])∧(i1284[3] →* i1238[6]))
(3) -> (8), if ((o3142[3] →* o3142[8])∧(java.lang.Object(ARRAY(i3[3], a4210data[3])) →* java.lang.Object(ARRAY(i3[8], a4210data[8])))∧(i1284[3] →* i1238[8])∧(o3274[3] →* NULL)∧(i477[3] →* i477[8])∧(i615[3] →* i615[8]))
(3) -> (13), if ((i477[3] →* i477[13])∧(java.lang.Object(ARRAY(i3[3], a4210data[3])) →* java.lang.Object(ARRAY(i3[13], a4210data[13])))∧(o3274[3] →* java.lang.Object(IntList(o3234[13], i1289[13])))∧(i1284[3] →* 0)∧(i615[3] →* i615[13])∧(o3142[3] →* o3142[13]))
(3) -> (14), if ((o3274[3] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(java.lang.Object(ARRAY(i3[3], a4210data[3])) →* java.lang.Object(ARRAY(i3[14], a4210data[14])))∧(i1284[3] →* i1238[14])∧(o3142[3] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(i477[3] →* i477[14])∧(i615[3] →* i615[14]))
(3) -> (17), if ((i477[3] →* i477[17])∧(o3142[3] →* o3142[17])∧(java.lang.Object(ARRAY(i3[3], a4210data[3])) →* java.lang.Object(ARRAY(i3[17], a4210data[17])))∧(o3274[3] →* NULL)∧(i615[3] →* i615[17])∧(i1284[3] →* 0))
(3) -> (19), if ((o3274[3] →* java.lang.Object(IntList(o3239[19], i1291[19])))∧(i477[3] →* i477[19])∧(i615[3] →* i615[19])∧(i1284[3] →* 0)∧(java.lang.Object(ARRAY(i3[3], a4210data[3])) →* java.lang.Object(ARRAY(i3[19], a4210data[19])))∧(o3142[3] →* java.lang.Object(IntList(o3239[19], i1291[19]))))
(4) -> (5), if ((i477[4] →* i477[5])∧(i1238[4] →* i1238[5])∧(java.lang.Object(IntList(o3274[4], i1311[4])) →* java.lang.Object(IntList(o3274[5], i1311[5])))∧(o3142[4] →* o3142[5])∧(i615[4] →* i615[5])∧(i1238[4] > 1 →* TRUE)∧(java.lang.Object(ARRAY(i3[4], a4210data[4])) →* java.lang.Object(ARRAY(i3[5], a4210data[5]))))
(5) -> (4), if ((i477[5] →* i477[4])∧(o3142[5] →* o3142[4])∧(o3274[5] →* java.lang.Object(IntList(o3274[4], i1311[4])))∧(i1238[5] + -1 →* i1238[4])∧(i615[5] →* i615[4])∧(java.lang.Object(ARRAY(i3[5], a4210data[5])) →* java.lang.Object(ARRAY(i3[4], a4210data[4]))))
(5) -> (6), if ((i615[5] →* i615[6])∧(i1238[5] + -1 →* i1238[6])∧(o3274[5] →* o3141[6])∧(o3142[5] →* o3142[6])∧(i477[5] →* i477[6])∧(java.lang.Object(ARRAY(i3[5], a4210data[5])) →* java.lang.Object(ARRAY(i3[6], a4210data[6]))))
(5) -> (8), if ((o3142[5] →* o3142[8])∧(i615[5] →* i615[8])∧(java.lang.Object(ARRAY(i3[5], a4210data[5])) →* java.lang.Object(ARRAY(i3[8], a4210data[8])))∧(o3274[5] →* NULL)∧(i477[5] →* i477[8])∧(i1238[5] + -1 →* i1238[8]))
(5) -> (13), if ((i1238[5] + -1 →* 0)∧(i615[5] →* i615[13])∧(o3142[5] →* o3142[13])∧(o3274[5] →* java.lang.Object(IntList(o3234[13], i1289[13])))∧(i477[5] →* i477[13])∧(java.lang.Object(ARRAY(i3[5], a4210data[5])) →* java.lang.Object(ARRAY(i3[13], a4210data[13]))))
(5) -> (14), if ((i615[5] →* i615[14])∧(i477[5] →* i477[14])∧(o3142[5] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(o3274[5] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(i1238[5] + -1 →* i1238[14])∧(java.lang.Object(ARRAY(i3[5], a4210data[5])) →* java.lang.Object(ARRAY(i3[14], a4210data[14]))))
(5) -> (17), if ((i1238[5] + -1 →* 0)∧(i477[5] →* i477[17])∧(java.lang.Object(ARRAY(i3[5], a4210data[5])) →* java.lang.Object(ARRAY(i3[17], a4210data[17])))∧(i615[5] →* i615[17])∧(o3274[5] →* NULL)∧(o3142[5] →* o3142[17]))
(5) -> (19), if ((o3274[5] →* java.lang.Object(IntList(o3239[19], i1291[19])))∧(o3142[5] →* java.lang.Object(IntList(o3239[19], i1291[19])))∧(java.lang.Object(ARRAY(i3[5], a4210data[5])) →* java.lang.Object(ARRAY(i3[19], a4210data[19])))∧(i1238[5] + -1 →* 0)∧(i615[5] →* i615[19])∧(i477[5] →* i477[19]))
(6) -> (7), if ((i1238[6] > 0 && i1238[6] <= 1 →* TRUE)∧(i1238[6] →* i1238[7])∧(java.lang.Object(ARRAY(i3[6], a4210data[6])) →* java.lang.Object(ARRAY(i3[7], a4210data[7])))∧(o3141[6] →* o3141[7])∧(i477[6] →* i477[7])∧(i615[6] →* i615[7])∧(o3142[6] →* o3142[7]))
(7) -> (12), if ((i615[7] →* i615[12])∧(o3141[7] →* java.lang.Object(IntList(o3234[12], i1289[12])))∧(i477[7] →* i477[12])∧(java.lang.Object(ARRAY(i3[7], a4210data[7])) →* java.lang.Object(ARRAY(i3[12], a4210data[12])))∧(o3142[7] →* o3142[12]))
(7) -> (16), if ((o3141[7] →* NULL)∧(i615[7] →* i615[16])∧(i477[7] →* i477[16])∧(java.lang.Object(ARRAY(i3[7], a4210data[7])) →* java.lang.Object(ARRAY(i3[16], a4210data[16])))∧(o3142[7] →* o3142[16]))
(7) -> (18), if ((java.lang.Object(ARRAY(i3[7], a4210data[7])) →* java.lang.Object(ARRAY(i3[18], a4210data[18])))∧(o3142[7] →* java.lang.Object(IntList(o3239[18], i1291[18])))∧(i477[7] →* i477[18])∧(o3141[7] →* java.lang.Object(IntList(o3239[18], i1291[18])))∧(i615[7] →* i615[18]))
(8) -> (9), if ((i477[8] →* i477[9])∧(o3142[8] →* o3142[9])∧(i615[8] →* i615[9])∧(java.lang.Object(ARRAY(i3[8], a4210data[8])) →* java.lang.Object(ARRAY(i3[9], a4210data[9])))∧(i1238[8] →* i1238[9])∧(i1238[8] > 1 →* TRUE))
(9) -> (12), if ((i615[9] →* i615[12])∧(java.lang.Object(ARRAY(i3[9], a4210data[9])) →* java.lang.Object(ARRAY(i3[12], a4210data[12])))∧(NULL →* java.lang.Object(IntList(o3234[12], i1289[12])))∧(o3142[9] →* o3142[12])∧(i477[9] →* i477[12]))
(9) -> (16), if ((i477[9] →* i477[16])∧(java.lang.Object(ARRAY(i3[9], a4210data[9])) →* java.lang.Object(ARRAY(i3[16], a4210data[16])))∧(i615[9] →* i615[16])∧(o3142[9] →* o3142[16]))
(9) -> (18), if ((NULL →* java.lang.Object(IntList(o3239[18], i1291[18])))∧(i477[9] →* i477[18])∧(java.lang.Object(ARRAY(i3[9], a4210data[9])) →* java.lang.Object(ARRAY(i3[18], a4210data[18])))∧(o3142[9] →* java.lang.Object(IntList(o3239[18], i1291[18])))∧(i615[9] →* i615[18]))
(10) -> (0), if ((i1289[10] →* i477[0])∧(i615[10] →* i118[0])∧(o3142[10] →* java.lang.Object(IntList(o1856[0], i480[0])))∧(java.lang.Object(ARRAY(i3[10], a4210data[10])) →* java.lang.Object(ARRAY(i3[0], a2436data[0]))))
(11) -> (0), if ((i615[11] →* i118[0])∧(i1289[11] →* i477[0])∧(o3142[11] →* java.lang.Object(IntList(o1856[0], i480[0])))∧(java.lang.Object(ARRAY(i3[11], a4210data[11])) →* java.lang.Object(ARRAY(i3[0], a2436data[0]))))
(12) -> (0), if ((o3142[12] →* java.lang.Object(IntList(o1856[0], i480[0])))∧(i1289[12] →* i477[0])∧(i615[12] →* i118[0])∧(java.lang.Object(ARRAY(i3[12], a4210data[12])) →* java.lang.Object(ARRAY(i3[0], a2436data[0]))))
(13) -> (0), if ((i1289[13] →* i477[0])∧(o3142[13] →* java.lang.Object(IntList(o1856[0], i480[0])))∧(i615[13] →* i118[0])∧(java.lang.Object(ARRAY(i3[13], a4210data[13])) →* java.lang.Object(ARRAY(i3[0], a2436data[0]))))
(14) -> (15), if ((i477[14] →* i477[15])∧(i1238[14] →* i1238[15])∧(i1238[14] > 1 →* TRUE)∧(java.lang.Object(ARRAY(i3[14], a4210data[14])) →* java.lang.Object(ARRAY(i3[15], a4210data[15])))∧(i615[14] →* i615[15])∧(java.lang.Object(IntList(o3280[14], i1314[14])) →* java.lang.Object(IntList(o3280[15], i1314[15]))))
(15) -> (3), if ((i1238[15] + -1 →* i1284[3])∧(i477[15] →* i477[3])∧(i615[15] →* i615[3])∧(java.lang.Object(IntList(o3280[15], i1314[15])) →* o3142[3])∧(java.lang.Object(ARRAY(i3[15], a4210data[15])) →* java.lang.Object(ARRAY(i3[3], a4210data[3])))∧(o3280[15] →* o3274[3]))
(16) -> (10), if ((i615[16] →* i615[10])∧(o3142[16] →* o3142[10])∧(java.lang.Object(ARRAY(i3[16], a4210data[16])) →* java.lang.Object(ARRAY(i3[10], a4210data[10])))∧(0 →* i1289[10])∧(i477[16] →* i477[10]))
(17) -> (10), if ((o3142[17] →* o3142[10])∧(i477[17] →* i477[10])∧(java.lang.Object(ARRAY(i3[17], a4210data[17])) →* java.lang.Object(ARRAY(i3[10], a4210data[10])))∧(0 →* i1289[10])∧(i615[17] →* i615[10]))
(18) -> (11), if ((java.lang.Object(IntList(o3239[18], i1291[18])) →* o3142[11])∧(i615[18] →* i615[11])∧(i477[18] →* i477[11])∧(i1291[18] →* i1289[11])∧(java.lang.Object(ARRAY(i3[18], a4210data[18])) →* java.lang.Object(ARRAY(i3[11], a4210data[11]))))
(19) -> (11), if ((java.lang.Object(ARRAY(i3[19], a4210data[19])) →* java.lang.Object(ARRAY(i3[11], a4210data[11])))∧(java.lang.Object(IntList(o3239[19], i1291[19])) →* o3142[11])∧(i1291[19] →* i1289[11])∧(i477[19] →* i477[11])∧(i615[19] →* i615[11]))
!= | ~ | 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 |
Boolean, Integer
(0) -> (1), if ((java.lang.Object(IntList(o1856[0], i480[0])) →* java.lang.Object(IntList(o1856[1], i480[1])))∧(i118[0] →* i118[1])∧(i477[0] →* i477[1])∧(java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])) →* java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1])))∧(java.lang.Object(ARRAY(i3[0], a2436data[0])) →* java.lang.Object(ARRAY(i3[1], a2436data[1]))))
(1) -> (2), if ((i118[1] > 0 && i118[1] < i3[1] && i477[1] > 0 && i118[1] + 1 > 0 →* TRUE)∧(i477[1] →* i477[2])∧(java.lang.Object(IntList(o1856[1], i480[1])) →* java.lang.Object(IntList(o1856[2], i480[2])))∧(java.lang.Object(ARRAY(i3[1], a2436data[1])) →* java.lang.Object(ARRAY(i3[2], a2436data[2])))∧(java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1])) →* java.lang.Object(java.lang.String(i771[2], i770[2], i772[2], a3255[2])))∧(i118[1] →* i118[2]))
(2) -> (4), if ((o1856[2] →* java.lang.Object(IntList(o3274[4], i1311[4])))∧(i118[2] + 1 →* i615[4])∧(i771[2] →* i1238[4])∧(java.lang.Object(ARRAY(i3[2], a2436data[2])) →* java.lang.Object(ARRAY(i3[4], a4210data[4])))∧(i477[2] →* i477[4])∧(o1856[2] →* o3142[4]))
(2) -> (6), if ((o1856[2] →* o3142[6])∧(java.lang.Object(ARRAY(i3[2], a2436data[2])) →* java.lang.Object(ARRAY(i3[6], a4210data[6])))∧(o1856[2] →* o3141[6])∧(i118[2] + 1 →* i615[6])∧(i771[2] →* i1238[6])∧(i477[2] →* i477[6]))
(2) -> (8), if ((i771[2] →* i1238[8])∧(java.lang.Object(ARRAY(i3[2], a2436data[2])) →* java.lang.Object(ARRAY(i3[8], a4210data[8])))∧(i477[2] →* i477[8])∧(i118[2] + 1 →* i615[8])∧(o1856[2] →* o3142[8])∧(o1856[2] →* NULL))
(2) -> (13), if ((i771[2] →* 0)∧(o1856[2] →* o3142[13])∧(i477[2] →* i477[13])∧(java.lang.Object(ARRAY(i3[2], a2436data[2])) →* java.lang.Object(ARRAY(i3[13], a4210data[13])))∧(o1856[2] →* java.lang.Object(IntList(o3234[13], i1289[13])))∧(i118[2] + 1 →* i615[13]))
(2) -> (14), if ((java.lang.Object(ARRAY(i3[2], a2436data[2])) →* java.lang.Object(ARRAY(i3[14], a4210data[14])))∧(i477[2] →* i477[14])∧(o1856[2] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(i771[2] →* i1238[14])∧(i118[2] + 1 →* i615[14]))
(2) -> (17), if ((java.lang.Object(ARRAY(i3[2], a2436data[2])) →* java.lang.Object(ARRAY(i3[17], a4210data[17])))∧(o1856[2] →* o3142[17])∧(i771[2] →* 0)∧(o1856[2] →* NULL)∧(i477[2] →* i477[17])∧(i118[2] + 1 →* i615[17]))
(2) -> (19), if ((o1856[2] →* java.lang.Object(IntList(o3239[19], i1291[19])))∧(i477[2] →* i477[19])∧(i771[2] →* 0)∧(java.lang.Object(ARRAY(i3[2], a2436data[2])) →* java.lang.Object(ARRAY(i3[19], a4210data[19])))∧(i118[2] + 1 →* i615[19]))
(3) -> (4), if ((i477[3] →* i477[4])∧(o3274[3] →* java.lang.Object(IntList(o3274[4], i1311[4])))∧(java.lang.Object(ARRAY(i3[3], a4210data[3])) →* java.lang.Object(ARRAY(i3[4], a4210data[4])))∧(i615[3] →* i615[4])∧(o3142[3] →* o3142[4])∧(i1284[3] →* i1238[4]))
(3) -> (6), if ((i615[3] →* i615[6])∧(i477[3] →* i477[6])∧(java.lang.Object(ARRAY(i3[3], a4210data[3])) →* java.lang.Object(ARRAY(i3[6], a4210data[6])))∧(o3142[3] →* o3142[6])∧(o3274[3] →* o3141[6])∧(i1284[3] →* i1238[6]))
(3) -> (8), if ((o3142[3] →* o3142[8])∧(java.lang.Object(ARRAY(i3[3], a4210data[3])) →* java.lang.Object(ARRAY(i3[8], a4210data[8])))∧(i1284[3] →* i1238[8])∧(o3274[3] →* NULL)∧(i477[3] →* i477[8])∧(i615[3] →* i615[8]))
(3) -> (13), if ((i477[3] →* i477[13])∧(java.lang.Object(ARRAY(i3[3], a4210data[3])) →* java.lang.Object(ARRAY(i3[13], a4210data[13])))∧(o3274[3] →* java.lang.Object(IntList(o3234[13], i1289[13])))∧(i1284[3] →* 0)∧(i615[3] →* i615[13])∧(o3142[3] →* o3142[13]))
(3) -> (14), if ((o3274[3] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(java.lang.Object(ARRAY(i3[3], a4210data[3])) →* java.lang.Object(ARRAY(i3[14], a4210data[14])))∧(i1284[3] →* i1238[14])∧(o3142[3] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(i477[3] →* i477[14])∧(i615[3] →* i615[14]))
(3) -> (17), if ((i477[3] →* i477[17])∧(o3142[3] →* o3142[17])∧(java.lang.Object(ARRAY(i3[3], a4210data[3])) →* java.lang.Object(ARRAY(i3[17], a4210data[17])))∧(o3274[3] →* NULL)∧(i615[3] →* i615[17])∧(i1284[3] →* 0))
(3) -> (19), if ((o3274[3] →* java.lang.Object(IntList(o3239[19], i1291[19])))∧(i477[3] →* i477[19])∧(i615[3] →* i615[19])∧(i1284[3] →* 0)∧(java.lang.Object(ARRAY(i3[3], a4210data[3])) →* java.lang.Object(ARRAY(i3[19], a4210data[19])))∧(o3142[3] →* java.lang.Object(IntList(o3239[19], i1291[19]))))
(4) -> (5), if ((i477[4] →* i477[5])∧(i1238[4] →* i1238[5])∧(java.lang.Object(IntList(o3274[4], i1311[4])) →* java.lang.Object(IntList(o3274[5], i1311[5])))∧(o3142[4] →* o3142[5])∧(i615[4] →* i615[5])∧(i1238[4] > 1 →* TRUE)∧(java.lang.Object(ARRAY(i3[4], a4210data[4])) →* java.lang.Object(ARRAY(i3[5], a4210data[5]))))
(5) -> (4), if ((i477[5] →* i477[4])∧(o3142[5] →* o3142[4])∧(o3274[5] →* java.lang.Object(IntList(o3274[4], i1311[4])))∧(i1238[5] + -1 →* i1238[4])∧(i615[5] →* i615[4])∧(java.lang.Object(ARRAY(i3[5], a4210data[5])) →* java.lang.Object(ARRAY(i3[4], a4210data[4]))))
(5) -> (6), if ((i615[5] →* i615[6])∧(i1238[5] + -1 →* i1238[6])∧(o3274[5] →* o3141[6])∧(o3142[5] →* o3142[6])∧(i477[5] →* i477[6])∧(java.lang.Object(ARRAY(i3[5], a4210data[5])) →* java.lang.Object(ARRAY(i3[6], a4210data[6]))))
(5) -> (8), if ((o3142[5] →* o3142[8])∧(i615[5] →* i615[8])∧(java.lang.Object(ARRAY(i3[5], a4210data[5])) →* java.lang.Object(ARRAY(i3[8], a4210data[8])))∧(o3274[5] →* NULL)∧(i477[5] →* i477[8])∧(i1238[5] + -1 →* i1238[8]))
(5) -> (13), if ((i1238[5] + -1 →* 0)∧(i615[5] →* i615[13])∧(o3142[5] →* o3142[13])∧(o3274[5] →* java.lang.Object(IntList(o3234[13], i1289[13])))∧(i477[5] →* i477[13])∧(java.lang.Object(ARRAY(i3[5], a4210data[5])) →* java.lang.Object(ARRAY(i3[13], a4210data[13]))))
(5) -> (14), if ((i615[5] →* i615[14])∧(i477[5] →* i477[14])∧(o3142[5] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(o3274[5] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(i1238[5] + -1 →* i1238[14])∧(java.lang.Object(ARRAY(i3[5], a4210data[5])) →* java.lang.Object(ARRAY(i3[14], a4210data[14]))))
(5) -> (17), if ((i1238[5] + -1 →* 0)∧(i477[5] →* i477[17])∧(java.lang.Object(ARRAY(i3[5], a4210data[5])) →* java.lang.Object(ARRAY(i3[17], a4210data[17])))∧(i615[5] →* i615[17])∧(o3274[5] →* NULL)∧(o3142[5] →* o3142[17]))
(5) -> (19), if ((o3274[5] →* java.lang.Object(IntList(o3239[19], i1291[19])))∧(o3142[5] →* java.lang.Object(IntList(o3239[19], i1291[19])))∧(java.lang.Object(ARRAY(i3[5], a4210data[5])) →* java.lang.Object(ARRAY(i3[19], a4210data[19])))∧(i1238[5] + -1 →* 0)∧(i615[5] →* i615[19])∧(i477[5] →* i477[19]))
(6) -> (7), if ((i1238[6] > 0 && i1238[6] <= 1 →* TRUE)∧(i1238[6] →* i1238[7])∧(java.lang.Object(ARRAY(i3[6], a4210data[6])) →* java.lang.Object(ARRAY(i3[7], a4210data[7])))∧(o3141[6] →* o3141[7])∧(i477[6] →* i477[7])∧(i615[6] →* i615[7])∧(o3142[6] →* o3142[7]))
(7) -> (12), if ((i615[7] →* i615[12])∧(o3141[7] →* java.lang.Object(IntList(o3234[12], i1289[12])))∧(i477[7] →* i477[12])∧(java.lang.Object(ARRAY(i3[7], a4210data[7])) →* java.lang.Object(ARRAY(i3[12], a4210data[12])))∧(o3142[7] →* o3142[12]))
(7) -> (16), if ((o3141[7] →* NULL)∧(i615[7] →* i615[16])∧(i477[7] →* i477[16])∧(java.lang.Object(ARRAY(i3[7], a4210data[7])) →* java.lang.Object(ARRAY(i3[16], a4210data[16])))∧(o3142[7] →* o3142[16]))
(7) -> (18), if ((java.lang.Object(ARRAY(i3[7], a4210data[7])) →* java.lang.Object(ARRAY(i3[18], a4210data[18])))∧(o3142[7] →* java.lang.Object(IntList(o3239[18], i1291[18])))∧(i477[7] →* i477[18])∧(o3141[7] →* java.lang.Object(IntList(o3239[18], i1291[18])))∧(i615[7] →* i615[18]))
(8) -> (9), if ((i477[8] →* i477[9])∧(o3142[8] →* o3142[9])∧(i615[8] →* i615[9])∧(java.lang.Object(ARRAY(i3[8], a4210data[8])) →* java.lang.Object(ARRAY(i3[9], a4210data[9])))∧(i1238[8] →* i1238[9])∧(i1238[8] > 1 →* TRUE))
(9) -> (12), if ((i615[9] →* i615[12])∧(java.lang.Object(ARRAY(i3[9], a4210data[9])) →* java.lang.Object(ARRAY(i3[12], a4210data[12])))∧(NULL →* java.lang.Object(IntList(o3234[12], i1289[12])))∧(o3142[9] →* o3142[12])∧(i477[9] →* i477[12]))
(9) -> (16), if ((i477[9] →* i477[16])∧(java.lang.Object(ARRAY(i3[9], a4210data[9])) →* java.lang.Object(ARRAY(i3[16], a4210data[16])))∧(i615[9] →* i615[16])∧(o3142[9] →* o3142[16]))
(9) -> (18), if ((NULL →* java.lang.Object(IntList(o3239[18], i1291[18])))∧(i477[9] →* i477[18])∧(java.lang.Object(ARRAY(i3[9], a4210data[9])) →* java.lang.Object(ARRAY(i3[18], a4210data[18])))∧(o3142[9] →* java.lang.Object(IntList(o3239[18], i1291[18])))∧(i615[9] →* i615[18]))
(10) -> (0), if ((i1289[10] →* i477[0])∧(i615[10] →* i118[0])∧(o3142[10] →* java.lang.Object(IntList(o1856[0], i480[0])))∧(java.lang.Object(ARRAY(i3[10], a4210data[10])) →* java.lang.Object(ARRAY(i3[0], a2436data[0]))))
(11) -> (0), if ((i615[11] →* i118[0])∧(i1289[11] →* i477[0])∧(o3142[11] →* java.lang.Object(IntList(o1856[0], i480[0])))∧(java.lang.Object(ARRAY(i3[11], a4210data[11])) →* java.lang.Object(ARRAY(i3[0], a2436data[0]))))
(12) -> (0), if ((o3142[12] →* java.lang.Object(IntList(o1856[0], i480[0])))∧(i1289[12] →* i477[0])∧(i615[12] →* i118[0])∧(java.lang.Object(ARRAY(i3[12], a4210data[12])) →* java.lang.Object(ARRAY(i3[0], a2436data[0]))))
(13) -> (0), if ((i1289[13] →* i477[0])∧(o3142[13] →* java.lang.Object(IntList(o1856[0], i480[0])))∧(i615[13] →* i118[0])∧(java.lang.Object(ARRAY(i3[13], a4210data[13])) →* java.lang.Object(ARRAY(i3[0], a2436data[0]))))
(14) -> (15), if ((i477[14] →* i477[15])∧(i1238[14] →* i1238[15])∧(i1238[14] > 1 →* TRUE)∧(java.lang.Object(ARRAY(i3[14], a4210data[14])) →* java.lang.Object(ARRAY(i3[15], a4210data[15])))∧(i615[14] →* i615[15])∧(java.lang.Object(IntList(o3280[14], i1314[14])) →* java.lang.Object(IntList(o3280[15], i1314[15]))))
(15) -> (3), if ((i1238[15] + -1 →* i1284[3])∧(i477[15] →* i477[3])∧(i615[15] →* i615[3])∧(java.lang.Object(IntList(o3280[15], i1314[15])) →* o3142[3])∧(java.lang.Object(ARRAY(i3[15], a4210data[15])) →* java.lang.Object(ARRAY(i3[3], a4210data[3])))∧(o3280[15] →* o3274[3]))
(16) -> (10), if ((i615[16] →* i615[10])∧(o3142[16] →* o3142[10])∧(java.lang.Object(ARRAY(i3[16], a4210data[16])) →* java.lang.Object(ARRAY(i3[10], a4210data[10])))∧(0 →* i1289[10])∧(i477[16] →* i477[10]))
(17) -> (10), if ((o3142[17] →* o3142[10])∧(i477[17] →* i477[10])∧(java.lang.Object(ARRAY(i3[17], a4210data[17])) →* java.lang.Object(ARRAY(i3[10], a4210data[10])))∧(0 →* i1289[10])∧(i615[17] →* i615[10]))
(18) -> (11), if ((java.lang.Object(IntList(o3239[18], i1291[18])) →* o3142[11])∧(i615[18] →* i615[11])∧(i477[18] →* i477[11])∧(i1291[18] →* i1289[11])∧(java.lang.Object(ARRAY(i3[18], a4210data[18])) →* java.lang.Object(ARRAY(i3[11], a4210data[11]))))
(19) -> (11), if ((java.lang.Object(ARRAY(i3[19], a4210data[19])) →* java.lang.Object(ARRAY(i3[11], a4210data[11])))∧(java.lang.Object(IntList(o3239[19], i1291[19])) →* o3142[11])∧(i1291[19] →* i1289[11])∧(i477[19] →* i477[11])∧(i615[19] →* i615[11]))
!= | ~ | 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 |
Boolean, Integer
(0) -> (1), if (((o1856[0] →* o1856[1])∧(i480[0] →* i480[1]))∧(i118[0] →* i118[1])∧(i477[0] →* i477[1])∧((i771[0] →* i771[1])∧(i770[0] →* i770[1])∧(i772[0] →* i772[1])∧(a3255[0] →* a3255[1]))∧((i3[0] →* i3[1])∧(a2436data[0] →* a2436data[1])))
(1) -> (2), if ((i118[1] > 0 && i118[1] < i3[1] && i477[1] > 0 && i118[1] + 1 > 0 →* TRUE)∧(i477[1] →* i477[2])∧((o1856[1] →* o1856[2])∧(i480[1] →* i480[2]))∧((i3[1] →* i3[2])∧(a2436data[1] →* a2436data[2]))∧((i771[1] →* i771[2])∧(i770[1] →* i770[2])∧(i772[1] →* i772[2])∧(a3255[1] →* a3255[2]))∧(i118[1] →* i118[2]))
(2) -> (4), if ((o1856[2] →* java.lang.Object(IntList(o3274[4], i1311[4])))∧(i118[2] + 1 →* i615[4])∧(i771[2] →* i1238[4])∧((i3[2] →* i3[4])∧(a2436data[2] →* a4210data[4]))∧(i477[2] →* i477[4])∧(o1856[2] →* o3142[4]))
(2) -> (6), if ((o1856[2] →* o3142[6])∧((i3[2] →* i3[6])∧(a2436data[2] →* a4210data[6]))∧(o1856[2] →* o3141[6])∧(i118[2] + 1 →* i615[6])∧(i771[2] →* i1238[6])∧(i477[2] →* i477[6]))
(2) -> (8), if ((i771[2] →* i1238[8])∧((i3[2] →* i3[8])∧(a2436data[2] →* a4210data[8]))∧(i477[2] →* i477[8])∧(i118[2] + 1 →* i615[8])∧(o1856[2] →* o3142[8])∧(o1856[2] →* NULL))
(2) -> (13), if ((i771[2] →* 0)∧(o1856[2] →* o3142[13])∧(i477[2] →* i477[13])∧((i3[2] →* i3[13])∧(a2436data[2] →* a4210data[13]))∧(o1856[2] →* java.lang.Object(IntList(o3234[13], i1289[13])))∧(i118[2] + 1 →* i615[13]))
(2) -> (14), if (((i3[2] →* i3[14])∧(a2436data[2] →* a4210data[14]))∧(i477[2] →* i477[14])∧(o1856[2] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(i771[2] →* i1238[14])∧(i118[2] + 1 →* i615[14]))
(2) -> (17), if (((i3[2] →* i3[17])∧(a2436data[2] →* a4210data[17]))∧(o1856[2] →* o3142[17])∧(i771[2] →* 0)∧(o1856[2] →* NULL)∧(i477[2] →* i477[17])∧(i118[2] + 1 →* i615[17]))
(2) -> (19), if ((o1856[2] →* java.lang.Object(IntList(o3239[19], i1291[19])))∧(i477[2] →* i477[19])∧(i771[2] →* 0)∧((i3[2] →* i3[19])∧(a2436data[2] →* a4210data[19]))∧(i118[2] + 1 →* i615[19]))
(3) -> (4), if ((i477[3] →* i477[4])∧(o3274[3] →* java.lang.Object(IntList(o3274[4], i1311[4])))∧((i3[3] →* i3[4])∧(a4210data[3] →* a4210data[4]))∧(i615[3] →* i615[4])∧(o3142[3] →* o3142[4])∧(i1284[3] →* i1238[4]))
(3) -> (6), if ((i615[3] →* i615[6])∧(i477[3] →* i477[6])∧((i3[3] →* i3[6])∧(a4210data[3] →* a4210data[6]))∧(o3142[3] →* o3142[6])∧(o3274[3] →* o3141[6])∧(i1284[3] →* i1238[6]))
(3) -> (8), if ((o3142[3] →* o3142[8])∧((i3[3] →* i3[8])∧(a4210data[3] →* a4210data[8]))∧(i1284[3] →* i1238[8])∧(o3274[3] →* NULL)∧(i477[3] →* i477[8])∧(i615[3] →* i615[8]))
(3) -> (13), if ((i477[3] →* i477[13])∧((i3[3] →* i3[13])∧(a4210data[3] →* a4210data[13]))∧(o3274[3] →* java.lang.Object(IntList(o3234[13], i1289[13])))∧(i1284[3] →* 0)∧(i615[3] →* i615[13])∧(o3142[3] →* o3142[13]))
(3) -> (14), if ((o3274[3] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧((i3[3] →* i3[14])∧(a4210data[3] →* a4210data[14]))∧(i1284[3] →* i1238[14])∧(o3142[3] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(i477[3] →* i477[14])∧(i615[3] →* i615[14]))
(3) -> (17), if ((i477[3] →* i477[17])∧(o3142[3] →* o3142[17])∧((i3[3] →* i3[17])∧(a4210data[3] →* a4210data[17]))∧(o3274[3] →* NULL)∧(i615[3] →* i615[17])∧(i1284[3] →* 0))
(3) -> (19), if ((o3274[3] →* java.lang.Object(IntList(o3239[19], i1291[19])))∧(i477[3] →* i477[19])∧(i615[3] →* i615[19])∧(i1284[3] →* 0)∧((i3[3] →* i3[19])∧(a4210data[3] →* a4210data[19]))∧(o3142[3] →* java.lang.Object(IntList(o3239[19], i1291[19]))))
(4) -> (5), if ((i477[4] →* i477[5])∧(i1238[4] →* i1238[5])∧((o3274[4] →* o3274[5])∧(i1311[4] →* i1311[5]))∧(o3142[4] →* o3142[5])∧(i615[4] →* i615[5])∧(i1238[4] > 1 →* TRUE)∧((i3[4] →* i3[5])∧(a4210data[4] →* a4210data[5])))
(5) -> (4), if ((i477[5] →* i477[4])∧(o3142[5] →* o3142[4])∧(o3274[5] →* java.lang.Object(IntList(o3274[4], i1311[4])))∧(i1238[5] + -1 →* i1238[4])∧(i615[5] →* i615[4])∧((i3[5] →* i3[4])∧(a4210data[5] →* a4210data[4])))
(5) -> (6), if ((i615[5] →* i615[6])∧(i1238[5] + -1 →* i1238[6])∧(o3274[5] →* o3141[6])∧(o3142[5] →* o3142[6])∧(i477[5] →* i477[6])∧((i3[5] →* i3[6])∧(a4210data[5] →* a4210data[6])))
(5) -> (8), if ((o3142[5] →* o3142[8])∧(i615[5] →* i615[8])∧((i3[5] →* i3[8])∧(a4210data[5] →* a4210data[8]))∧(o3274[5] →* NULL)∧(i477[5] →* i477[8])∧(i1238[5] + -1 →* i1238[8]))
(5) -> (13), if ((i1238[5] + -1 →* 0)∧(i615[5] →* i615[13])∧(o3142[5] →* o3142[13])∧(o3274[5] →* java.lang.Object(IntList(o3234[13], i1289[13])))∧(i477[5] →* i477[13])∧((i3[5] →* i3[13])∧(a4210data[5] →* a4210data[13])))
(5) -> (14), if ((i615[5] →* i615[14])∧(i477[5] →* i477[14])∧(o3142[5] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(o3274[5] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(i1238[5] + -1 →* i1238[14])∧((i3[5] →* i3[14])∧(a4210data[5] →* a4210data[14])))
(5) -> (17), if ((i1238[5] + -1 →* 0)∧(i477[5] →* i477[17])∧((i3[5] →* i3[17])∧(a4210data[5] →* a4210data[17]))∧(i615[5] →* i615[17])∧(o3274[5] →* NULL)∧(o3142[5] →* o3142[17]))
(5) -> (19), if ((o3274[5] →* java.lang.Object(IntList(o3239[19], i1291[19])))∧(o3142[5] →* java.lang.Object(IntList(o3239[19], i1291[19])))∧((i3[5] →* i3[19])∧(a4210data[5] →* a4210data[19]))∧(i1238[5] + -1 →* 0)∧(i615[5] →* i615[19])∧(i477[5] →* i477[19]))
(6) -> (7), if ((i1238[6] > 0 && i1238[6] <= 1 →* TRUE)∧(i1238[6] →* i1238[7])∧((i3[6] →* i3[7])∧(a4210data[6] →* a4210data[7]))∧(o3141[6] →* o3141[7])∧(i477[6] →* i477[7])∧(i615[6] →* i615[7])∧(o3142[6] →* o3142[7]))
(7) -> (12), if ((i615[7] →* i615[12])∧(o3141[7] →* java.lang.Object(IntList(o3234[12], i1289[12])))∧(i477[7] →* i477[12])∧((i3[7] →* i3[12])∧(a4210data[7] →* a4210data[12]))∧(o3142[7] →* o3142[12]))
(7) -> (16), if ((o3141[7] →* NULL)∧(i615[7] →* i615[16])∧(i477[7] →* i477[16])∧((i3[7] →* i3[16])∧(a4210data[7] →* a4210data[16]))∧(o3142[7] →* o3142[16]))
(7) -> (18), if (((i3[7] →* i3[18])∧(a4210data[7] →* a4210data[18]))∧(o3142[7] →* java.lang.Object(IntList(o3239[18], i1291[18])))∧(i477[7] →* i477[18])∧(o3141[7] →* java.lang.Object(IntList(o3239[18], i1291[18])))∧(i615[7] →* i615[18]))
(8) -> (9), if ((i477[8] →* i477[9])∧(o3142[8] →* o3142[9])∧(i615[8] →* i615[9])∧((i3[8] →* i3[9])∧(a4210data[8] →* a4210data[9]))∧(i1238[8] →* i1238[9])∧(i1238[8] > 1 →* TRUE))
(9) -> (12), if ((i615[9] →* i615[12])∧((i3[9] →* i3[12])∧(a4210data[9] →* a4210data[12]))∧false∧(o3142[9] →* o3142[12])∧(i477[9] →* i477[12]))
(9) -> (16), if ((i477[9] →* i477[16])∧((i3[9] →* i3[16])∧(a4210data[9] →* a4210data[16]))∧(i615[9] →* i615[16])∧(o3142[9] →* o3142[16]))
(9) -> (18), if (false∧(i477[9] →* i477[18])∧((i3[9] →* i3[18])∧(a4210data[9] →* a4210data[18]))∧(o3142[9] →* java.lang.Object(IntList(o3239[18], i1291[18])))∧(i615[9] →* i615[18]))
(10) -> (0), if ((i1289[10] →* i477[0])∧(i615[10] →* i118[0])∧(o3142[10] →* java.lang.Object(IntList(o1856[0], i480[0])))∧((i3[10] →* i3[0])∧(a4210data[10] →* a2436data[0])))
(11) -> (0), if ((i615[11] →* i118[0])∧(i1289[11] →* i477[0])∧(o3142[11] →* java.lang.Object(IntList(o1856[0], i480[0])))∧((i3[11] →* i3[0])∧(a4210data[11] →* a2436data[0])))
(12) -> (0), if ((o3142[12] →* java.lang.Object(IntList(o1856[0], i480[0])))∧(i1289[12] →* i477[0])∧(i615[12] →* i118[0])∧((i3[12] →* i3[0])∧(a4210data[12] →* a2436data[0])))
(13) -> (0), if ((i1289[13] →* i477[0])∧(o3142[13] →* java.lang.Object(IntList(o1856[0], i480[0])))∧(i615[13] →* i118[0])∧((i3[13] →* i3[0])∧(a4210data[13] →* a2436data[0])))
(14) -> (15), if ((i477[14] →* i477[15])∧(i1238[14] →* i1238[15])∧(i1238[14] > 1 →* TRUE)∧((i3[14] →* i3[15])∧(a4210data[14] →* a4210data[15]))∧(i615[14] →* i615[15])∧((o3280[14] →* o3280[15])∧(i1314[14] →* i1314[15])))
(15) -> (3), if ((i1238[15] + -1 →* i1284[3])∧(i477[15] →* i477[3])∧(i615[15] →* i615[3])∧(java.lang.Object(IntList(o3280[15], i1314[15])) →* o3142[3])∧((i3[15] →* i3[3])∧(a4210data[15] →* a4210data[3]))∧(o3280[15] →* o3274[3]))
(16) -> (10), if ((i615[16] →* i615[10])∧(o3142[16] →* o3142[10])∧((i3[16] →* i3[10])∧(a4210data[16] →* a4210data[10]))∧(0 →* i1289[10])∧(i477[16] →* i477[10]))
(17) -> (10), if ((o3142[17] →* o3142[10])∧(i477[17] →* i477[10])∧((i3[17] →* i3[10])∧(a4210data[17] →* a4210data[10]))∧(0 →* i1289[10])∧(i615[17] →* i615[10]))
(18) -> (11), if ((java.lang.Object(IntList(o3239[18], i1291[18])) →* o3142[11])∧(i615[18] →* i615[11])∧(i477[18] →* i477[11])∧(i1291[18] →* i1289[11])∧((i3[18] →* i3[11])∧(a4210data[18] →* a4210data[11])))
(19) -> (11), if (((i3[19] →* i3[11])∧(a4210data[19] →* a4210data[11]))∧(java.lang.Object(IntList(o3239[19], i1291[19])) →* o3142[11])∧(i1291[19] →* i1289[11])∧(i477[19] →* i477[11])∧(i615[19] →* i615[11]))
(1) (i1289[10]=i477[0]∧i615[10]=i118[0]∧o3142[10]=java.lang.Object(IntList(o1856[0], i480[0]))∧i3[10]=i3[0]∧a4210data[10]=a2436data[0]∧o1856[0]=o1856[1]∧i480[0]=i480[1]∧i118[0]=i118[1]∧i477[0]=i477[1]∧i771[0]=i771[1]∧i770[0]=i770[1]∧i772[0]=i772[1]∧a3255[0]=a3255[1]∧i3[0]=i3[1]∧a2436data[0]=a2436data[1] ⇒ LOAD2305(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0])≥NonInfC∧LOAD2305(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0])≥LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))∧(UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥))
(2) (LOAD2305(java.lang.Object(ARRAY(i3[10], a4210data[10])), i615[10], java.lang.Object(IntList(o1856[0], i480[0])), i1289[10])≥NonInfC∧LOAD2305(java.lang.Object(ARRAY(i3[10], a4210data[10])), i615[10], java.lang.Object(IntList(o1856[0], i480[0])), i1289[10])≥LOAD2305ARR1(java.lang.Object(ARRAY(i3[10], a4210data[10])), i615[10], java.lang.Object(IntList(o1856[0], i480[0])), i1289[10], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))∧(UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥))
(3) ((UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥)∧[(-1)bso_96] ≥ 0)
(4) ((UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥)∧[(-1)bso_96] ≥ 0)
(5) ((UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥)∧[(-1)bso_96] ≥ 0)
(6) ((UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_96] ≥ 0)
(7) (i615[11]=i118[0]∧i1289[11]=i477[0]∧o3142[11]=java.lang.Object(IntList(o1856[0], i480[0]))∧i3[11]=i3[0]∧a4210data[11]=a2436data[0]∧o1856[0]=o1856[1]∧i480[0]=i480[1]∧i118[0]=i118[1]∧i477[0]=i477[1]∧i771[0]=i771[1]∧i770[0]=i770[1]∧i772[0]=i772[1]∧a3255[0]=a3255[1]∧i3[0]=i3[1]∧a2436data[0]=a2436data[1] ⇒ LOAD2305(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0])≥NonInfC∧LOAD2305(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0])≥LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))∧(UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥))
(8) (LOAD2305(java.lang.Object(ARRAY(i3[11], a4210data[11])), i615[11], java.lang.Object(IntList(o1856[0], i480[0])), i1289[11])≥NonInfC∧LOAD2305(java.lang.Object(ARRAY(i3[11], a4210data[11])), i615[11], java.lang.Object(IntList(o1856[0], i480[0])), i1289[11])≥LOAD2305ARR1(java.lang.Object(ARRAY(i3[11], a4210data[11])), i615[11], java.lang.Object(IntList(o1856[0], i480[0])), i1289[11], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))∧(UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥))
(9) ((UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥)∧[(-1)bso_96] ≥ 0)
(10) ((UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥)∧[(-1)bso_96] ≥ 0)
(11) ((UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥)∧[(-1)bso_96] ≥ 0)
(12) ((UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_96] ≥ 0)
(13) (o3142[12]=java.lang.Object(IntList(o1856[0], i480[0]))∧i1289[12]=i477[0]∧i615[12]=i118[0]∧i3[12]=i3[0]∧a4210data[12]=a2436data[0]∧o1856[0]=o1856[1]∧i480[0]=i480[1]∧i118[0]=i118[1]∧i477[0]=i477[1]∧i771[0]=i771[1]∧i770[0]=i770[1]∧i772[0]=i772[1]∧a3255[0]=a3255[1]∧i3[0]=i3[1]∧a2436data[0]=a2436data[1] ⇒ LOAD2305(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0])≥NonInfC∧LOAD2305(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0])≥LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))∧(UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥))
(14) (LOAD2305(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], java.lang.Object(IntList(o1856[0], i480[0])), i1289[12])≥NonInfC∧LOAD2305(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], java.lang.Object(IntList(o1856[0], i480[0])), i1289[12])≥LOAD2305ARR1(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], java.lang.Object(IntList(o1856[0], i480[0])), i1289[12], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))∧(UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥))
(15) ((UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥)∧[(-1)bso_96] ≥ 0)
(16) ((UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥)∧[(-1)bso_96] ≥ 0)
(17) ((UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥)∧[(-1)bso_96] ≥ 0)
(18) ((UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_96] ≥ 0)
(19) (i1289[13]=i477[0]∧o3142[13]=java.lang.Object(IntList(o1856[0], i480[0]))∧i615[13]=i118[0]∧i3[13]=i3[0]∧a4210data[13]=a2436data[0]∧o1856[0]=o1856[1]∧i480[0]=i480[1]∧i118[0]=i118[1]∧i477[0]=i477[1]∧i771[0]=i771[1]∧i770[0]=i770[1]∧i772[0]=i772[1]∧a3255[0]=a3255[1]∧i3[0]=i3[1]∧a2436data[0]=a2436data[1] ⇒ LOAD2305(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0])≥NonInfC∧LOAD2305(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0])≥LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))∧(UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥))
(20) (LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], java.lang.Object(IntList(o1856[0], i480[0])), i1289[13])≥NonInfC∧LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], java.lang.Object(IntList(o1856[0], i480[0])), i1289[13])≥LOAD2305ARR1(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], java.lang.Object(IntList(o1856[0], i480[0])), i1289[13], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))∧(UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥))
(21) ((UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥)∧[(-1)bso_96] ≥ 0)
(22) ((UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥)∧[(-1)bso_96] ≥ 0)
(23) ((UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥)∧[(-1)bso_96] ≥ 0)
(24) ((UIncreasing(LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_96] ≥ 0)
(25) (&&(&&(&&(>(i118[1], 0), <(i118[1], i3[1])), >(i477[1], 0)), >(+(i118[1], 1), 0))=TRUE∧i477[1]=i477[2]∧o1856[1]=o1856[2]∧i480[1]=i480[2]∧i3[1]=i3[2]∧a2436data[1]=a2436data[2]∧i771[1]=i771[2]∧i770[1]=i770[2]∧i772[1]=i772[2]∧a3255[1]=a3255[2]∧i118[1]=i118[2] ⇒ LOAD2305ARR1(java.lang.Object(ARRAY(i3[1], a2436data[1])), i118[1], java.lang.Object(IntList(o1856[1], i480[1])), i477[1], java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1])))≥NonInfC∧LOAD2305ARR1(java.lang.Object(ARRAY(i3[1], a2436data[1])), i118[1], java.lang.Object(IntList(o1856[1], i480[1])), i477[1], java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1])))≥COND_LOAD2305ARR1(&&(&&(&&(>(i118[1], 0), <(i118[1], i3[1])), >(i477[1], 0)), >(+(i118[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a2436data[1])), i118[1], java.lang.Object(IntList(o1856[1], i480[1])), i477[1], java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1])))∧(UIncreasing(COND_LOAD2305ARR1(&&(&&(&&(>(i118[1], 0), <(i118[1], i3[1])), >(i477[1], 0)), >(+(i118[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a2436data[1])), i118[1], java.lang.Object(IntList(o1856[1], i480[1])), i477[1], java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1])))), ≥))
(26) (&&(&&(&&(>(i118[1], 0), <(i118[1], i3[1])), >(i477[1], 0)), >(+(i118[1], 1), 0))=TRUE ⇒ LOAD2305ARR1(java.lang.Object(ARRAY(i3[1], a2436data[1])), i118[1], java.lang.Object(IntList(o1856[1], i480[1])), i477[1], java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1])))≥NonInfC∧LOAD2305ARR1(java.lang.Object(ARRAY(i3[1], a2436data[1])), i118[1], java.lang.Object(IntList(o1856[1], i480[1])), i477[1], java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1])))≥COND_LOAD2305ARR1(&&(&&(&&(>(i118[1], 0), <(i118[1], i3[1])), >(i477[1], 0)), >(+(i118[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a2436data[1])), i118[1], java.lang.Object(IntList(o1856[1], i480[1])), i477[1], java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1])))∧(UIncreasing(COND_LOAD2305ARR1(&&(&&(&&(>(i118[1], 0), <(i118[1], i3[1])), >(i477[1], 0)), >(+(i118[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a2436data[1])), i118[1], java.lang.Object(IntList(o1856[1], i480[1])), i477[1], java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1])))), ≥))
(27) (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD2305ARR1(&&(&&(&&(>(i118[1], 0), <(i118[1], i3[1])), >(i477[1], 0)), >(+(i118[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a2436data[1])), i118[1], java.lang.Object(IntList(o1856[1], i480[1])), i477[1], java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1])))), ≥)∧[(-1)Bound*bni_97] + [(2)bni_97]o1856[1] ≥ 0∧[(-1)bso_98] ≥ 0)
(28) (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD2305ARR1(&&(&&(&&(>(i118[1], 0), <(i118[1], i3[1])), >(i477[1], 0)), >(+(i118[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a2436data[1])), i118[1], java.lang.Object(IntList(o1856[1], i480[1])), i477[1], java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1])))), ≥)∧[(-1)Bound*bni_97] + [(2)bni_97]o1856[1] ≥ 0∧[(-1)bso_98] ≥ 0)
(29) (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD2305ARR1(&&(&&(&&(>(i118[1], 0), <(i118[1], i3[1])), >(i477[1], 0)), >(+(i118[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a2436data[1])), i118[1], java.lang.Object(IntList(o1856[1], i480[1])), i477[1], java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1])))), ≥)∧[(-1)Bound*bni_97] + [(2)bni_97]o1856[1] ≥ 0∧[(-1)bso_98] ≥ 0)
(30) (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD2305ARR1(&&(&&(&&(>(i118[1], 0), <(i118[1], i3[1])), >(i477[1], 0)), >(+(i118[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a2436data[1])), i118[1], java.lang.Object(IntList(o1856[1], i480[1])), i477[1], java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(2)bni_97] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)Bound*bni_97] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_98] ≥ 0)
(31) (&&(&&(&&(>(i118[1], 0), <(i118[1], i3[1])), >(i477[1], 0)), >(+(i118[1], 1), 0))=TRUE∧i477[1]=i477[2]∧o1856[1]=o1856[2]∧i480[1]=i480[2]∧i3[1]=i3[2]∧a2436data[1]=a2436data[2]∧i771[1]=i771[2]∧i770[1]=i770[2]∧i772[1]=i772[2]∧a3255[1]=a3255[2]∧i118[1]=i118[2] ⇒ COND_LOAD2305ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a2436data[2])), i118[2], java.lang.Object(IntList(o1856[2], i480[2])), i477[2], java.lang.Object(java.lang.String(i771[2], i770[2], i772[2], a3255[2])))≥NonInfC∧COND_LOAD2305ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a2436data[2])), i118[2], java.lang.Object(IntList(o1856[2], i480[2])), i477[2], java.lang.Object(java.lang.String(i771[2], i770[2], i772[2], a3255[2])))≥LOAD3607(java.lang.Object(ARRAY(i3[2], a2436data[2])), +(i118[2], 1), i477[2], o1856[2], i771[2], o1856[2])∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[2], a2436data[2])), +(i118[2], 1), i477[2], o1856[2], i771[2], o1856[2])), ≥))
(32) (&&(&&(&&(>(i118[1], 0), <(i118[1], i3[1])), >(i477[1], 0)), >(+(i118[1], 1), 0))=TRUE ⇒ COND_LOAD2305ARR1(TRUE, java.lang.Object(ARRAY(i3[1], a2436data[1])), i118[1], java.lang.Object(IntList(o1856[1], i480[1])), i477[1], java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1])))≥NonInfC∧COND_LOAD2305ARR1(TRUE, java.lang.Object(ARRAY(i3[1], a2436data[1])), i118[1], java.lang.Object(IntList(o1856[1], i480[1])), i477[1], java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1])))≥LOAD3607(java.lang.Object(ARRAY(i3[1], a2436data[1])), +(i118[1], 1), i477[1], o1856[1], i771[1], o1856[1])∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[2], a2436data[2])), +(i118[2], 1), i477[2], o1856[2], i771[2], o1856[2])), ≥))
(33) (0 ≥ 0 ⇒ (UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[2], a2436data[2])), +(i118[2], 1), i477[2], o1856[2], i771[2], o1856[2])), ≥)∧[(-1)Bound*bni_99] + [(2)bni_99]o1856[1] ≥ 0∧[(-1)bso_100] ≥ 0)
(34) (0 ≥ 0 ⇒ (UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[2], a2436data[2])), +(i118[2], 1), i477[2], o1856[2], i771[2], o1856[2])), ≥)∧[(-1)Bound*bni_99] + [(2)bni_99]o1856[1] ≥ 0∧[(-1)bso_100] ≥ 0)
(35) (0 ≥ 0 ⇒ (UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[2], a2436data[2])), +(i118[2], 1), i477[2], o1856[2], i771[2], o1856[2])), ≥)∧[(-1)Bound*bni_99] + [(2)bni_99]o1856[1] ≥ 0∧[(-1)bso_100] ≥ 0)
(36) (0 ≥ 0 ⇒ (UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[2], a2436data[2])), +(i118[2], 1), i477[2], o1856[2], i771[2], o1856[2])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(2)bni_99] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)Bound*bni_99] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_100] ≥ 0)
(37) (i477[3]=i477[4]∧o3274[3]=java.lang.Object(IntList(o3274[4], i1311[4]))∧i3[3]=i3[4]∧a4210data[3]=a4210data[4]∧i615[3]=i615[4]∧o3142[3]=o3142[4]∧i1284[3]=i1238[4] ⇒ JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(38) (JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], java.lang.Object(IntList(o3274[4], i1311[4])))≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], java.lang.Object(IntList(o3274[4], i1311[4])))≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], java.lang.Object(IntList(o3274[4], i1311[4])))∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(39) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(40) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(41) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(42) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_102] ≥ 0)
(43) (i615[3]=i615[6]∧i477[3]=i477[6]∧i3[3]=i3[6]∧a4210data[3]=a4210data[6]∧o3142[3]=o3142[6]∧o3274[3]=o3141[6]∧i1284[3]=i1238[6] ⇒ JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(44) (JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(45) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(46) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(47) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(48) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_102] ≥ 0)
(49) (o3142[3]=o3142[8]∧i3[3]=i3[8]∧a4210data[3]=a4210data[8]∧i1284[3]=i1238[8]∧o3274[3]=NULL∧i477[3]=i477[8]∧i615[3]=i615[8] ⇒ JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(50) (JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], NULL)≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], NULL)≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], NULL)∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(51) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(52) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(53) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(54) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_102] ≥ 0)
(55) (i477[3]=i477[13]∧i3[3]=i3[13]∧a4210data[3]=a4210data[13]∧o3274[3]=java.lang.Object(IntList(o3234[13], i1289[13]))∧i1284[3]=0∧i615[3]=i615[13]∧o3142[3]=o3142[13] ⇒ JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(56) (JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], 0, java.lang.Object(IntList(o3234[13], i1289[13])))≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], 0, java.lang.Object(IntList(o3234[13], i1289[13])))≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], 0, java.lang.Object(IntList(o3234[13], i1289[13])))∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(57) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(58) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(59) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(60) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_102] ≥ 0)
(61) (o3274[3]=java.lang.Object(IntList(o3280[14], i1314[14]))∧i3[3]=i3[14]∧a4210data[3]=a4210data[14]∧i1284[3]=i1238[14]∧o3142[3]=java.lang.Object(IntList(o3280[14], i1314[14]))∧i477[3]=i477[14]∧i615[3]=i615[14] ⇒ JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(62) (JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], java.lang.Object(IntList(o3280[14], i1314[14])), i1284[3], java.lang.Object(IntList(o3280[14], i1314[14])))≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], java.lang.Object(IntList(o3280[14], i1314[14])), i1284[3], java.lang.Object(IntList(o3280[14], i1314[14])))≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], java.lang.Object(IntList(o3280[14], i1314[14])), i1284[3], java.lang.Object(IntList(o3280[14], i1314[14])))∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(63) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(64) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(65) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(66) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_102] ≥ 0)
(67) (i477[3]=i477[17]∧o3142[3]=o3142[17]∧i3[3]=i3[17]∧a4210data[3]=a4210data[17]∧o3274[3]=NULL∧i615[3]=i615[17]∧i1284[3]=0 ⇒ JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(68) (JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], 0, NULL)≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], 0, NULL)≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], 0, NULL)∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(69) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(70) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(71) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(72) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_102] ≥ 0)
(73) (o3274[3]=java.lang.Object(IntList(o3239[19], i1291[19]))∧i477[3]=i477[19]∧i615[3]=i615[19]∧i1284[3]=0∧i3[3]=i3[19]∧a4210data[3]=a4210data[19]∧o3142[3]=java.lang.Object(IntList(o3239[19], i1291[19])) ⇒ JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(74) (JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(75) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(76) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(77) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_102] ≥ 0)
(78) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_102] ≥ 0)
(79) (i477[4]=i477[5]∧i1238[4]=i1238[5]∧o3274[4]=o3274[5]∧i1311[4]=i1311[5]∧o3142[4]=o3142[5]∧i615[4]=i615[5]∧>(i1238[4], 1)=TRUE∧i3[4]=i3[5]∧a4210data[4]=a4210data[5] ⇒ LOAD3607(java.lang.Object(ARRAY(i3[4], a4210data[4])), i615[4], i477[4], o3142[4], i1238[4], java.lang.Object(IntList(o3274[4], i1311[4])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[4], a4210data[4])), i615[4], i477[4], o3142[4], i1238[4], java.lang.Object(IntList(o3274[4], i1311[4])))≥COND_LOAD3607(>(i1238[4], 1), java.lang.Object(ARRAY(i3[4], a4210data[4])), i615[4], i477[4], o3142[4], i1238[4], java.lang.Object(IntList(o3274[4], i1311[4])))∧(UIncreasing(COND_LOAD3607(>(i1238[4], 1), java.lang.Object(ARRAY(i3[4], a4210data[4])), i615[4], i477[4], o3142[4], i1238[4], java.lang.Object(IntList(o3274[4], i1311[4])))), ≥))
(80) (>(i1238[4], 1)=TRUE ⇒ LOAD3607(java.lang.Object(ARRAY(i3[4], a4210data[4])), i615[4], i477[4], o3142[4], i1238[4], java.lang.Object(IntList(o3274[4], i1311[4])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[4], a4210data[4])), i615[4], i477[4], o3142[4], i1238[4], java.lang.Object(IntList(o3274[4], i1311[4])))≥COND_LOAD3607(>(i1238[4], 1), java.lang.Object(ARRAY(i3[4], a4210data[4])), i615[4], i477[4], o3142[4], i1238[4], java.lang.Object(IntList(o3274[4], i1311[4])))∧(UIncreasing(COND_LOAD3607(>(i1238[4], 1), java.lang.Object(ARRAY(i3[4], a4210data[4])), i615[4], i477[4], o3142[4], i1238[4], java.lang.Object(IntList(o3274[4], i1311[4])))), ≥))
(81) (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD3607(>(i1238[4], 1), java.lang.Object(ARRAY(i3[4], a4210data[4])), i615[4], i477[4], o3142[4], i1238[4], java.lang.Object(IntList(o3274[4], i1311[4])))), ≥)∧[(-1)Bound*bni_103] + [(2)bni_103]o3274[4] + [bni_103]o3142[4] ≥ 0∧[(-1)bso_104] ≥ 0)
(82) (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD3607(>(i1238[4], 1), java.lang.Object(ARRAY(i3[4], a4210data[4])), i615[4], i477[4], o3142[4], i1238[4], java.lang.Object(IntList(o3274[4], i1311[4])))), ≥)∧[(-1)Bound*bni_103] + [(2)bni_103]o3274[4] + [bni_103]o3142[4] ≥ 0∧[(-1)bso_104] ≥ 0)
(83) (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD3607(>(i1238[4], 1), java.lang.Object(ARRAY(i3[4], a4210data[4])), i615[4], i477[4], o3142[4], i1238[4], java.lang.Object(IntList(o3274[4], i1311[4])))), ≥)∧[(-1)Bound*bni_103] + [(2)bni_103]o3274[4] + [bni_103]o3142[4] ≥ 0∧[(-1)bso_104] ≥ 0)
(84) (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD3607(>(i1238[4], 1), java.lang.Object(ARRAY(i3[4], a4210data[4])), i615[4], i477[4], o3142[4], i1238[4], java.lang.Object(IntList(o3274[4], i1311[4])))), ≥)∧0 ≥ 0∧[(2)bni_103] ≥ 0∧0 ≥ 0∧[bni_103] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)Bound*bni_103] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_104] ≥ 0)
(85) (i477[4]=i477[5]∧i1238[4]=i1238[5]∧o3274[4]=o3274[5]∧i1311[4]=i1311[5]∧o3142[4]=o3142[5]∧i615[4]=i615[5]∧>(i1238[4], 1)=TRUE∧i3[4]=i3[5]∧a4210data[4]=a4210data[5] ⇒ COND_LOAD3607(TRUE, java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], o3142[5], i1238[5], java.lang.Object(IntList(o3274[5], i1311[5])))≥NonInfC∧COND_LOAD3607(TRUE, java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], o3142[5], i1238[5], java.lang.Object(IntList(o3274[5], i1311[5])))≥LOAD3607(java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], o3142[5], +(i1238[5], -1), o3274[5])∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], o3142[5], +(i1238[5], -1), o3274[5])), ≥))
(86) (>(i1238[4], 1)=TRUE ⇒ COND_LOAD3607(TRUE, java.lang.Object(ARRAY(i3[4], a4210data[4])), i615[4], i477[4], o3142[4], i1238[4], java.lang.Object(IntList(o3274[4], i1311[4])))≥NonInfC∧COND_LOAD3607(TRUE, java.lang.Object(ARRAY(i3[4], a4210data[4])), i615[4], i477[4], o3142[4], i1238[4], java.lang.Object(IntList(o3274[4], i1311[4])))≥LOAD3607(java.lang.Object(ARRAY(i3[4], a4210data[4])), i615[4], i477[4], o3142[4], +(i1238[4], -1), o3274[4])∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], o3142[5], +(i1238[5], -1), o3274[5])), ≥))
(87) (0 ≥ 0 ⇒ (UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], o3142[5], +(i1238[5], -1), o3274[5])), ≥)∧[(-1)Bound*bni_105] + [(2)bni_105]o3274[4] + [bni_105]o3142[4] ≥ 0∧[(-1)bso_106] + o3274[4] ≥ 0)
(88) (0 ≥ 0 ⇒ (UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], o3142[5], +(i1238[5], -1), o3274[5])), ≥)∧[(-1)Bound*bni_105] + [(2)bni_105]o3274[4] + [bni_105]o3142[4] ≥ 0∧[(-1)bso_106] + o3274[4] ≥ 0)
(89) (0 ≥ 0 ⇒ (UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], o3142[5], +(i1238[5], -1), o3274[5])), ≥)∧[(-1)Bound*bni_105] + [(2)bni_105]o3274[4] + [bni_105]o3142[4] ≥ 0∧[(-1)bso_106] + o3274[4] ≥ 0)
(90) (0 ≥ 0 ⇒ (UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], o3142[5], +(i1238[5], -1), o3274[5])), ≥)∧0 ≥ 0∧[(2)bni_105] ≥ 0∧0 ≥ 0∧[bni_105] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)Bound*bni_105] ≥ 0∧0 ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_106] ≥ 0)
(91) (&&(>(i1238[6], 0), <=(i1238[6], 1))=TRUE∧i1238[6]=i1238[7]∧i3[6]=i3[7]∧a4210data[6]=a4210data[7]∧o3141[6]=o3141[7]∧i477[6]=i477[7]∧i615[6]=i615[7]∧o3142[6]=o3142[7] ⇒ LOAD3607(java.lang.Object(ARRAY(i3[6], a4210data[6])), i615[6], i477[6], o3142[6], i1238[6], o3141[6])≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[6], a4210data[6])), i615[6], i477[6], o3142[6], i1238[6], o3141[6])≥COND_LOAD36071(&&(>(i1238[6], 0), <=(i1238[6], 1)), java.lang.Object(ARRAY(i3[6], a4210data[6])), i615[6], i477[6], o3142[6], i1238[6], o3141[6])∧(UIncreasing(COND_LOAD36071(&&(>(i1238[6], 0), <=(i1238[6], 1)), java.lang.Object(ARRAY(i3[6], a4210data[6])), i615[6], i477[6], o3142[6], i1238[6], o3141[6])), ≥))
(92) (&&(>(i1238[6], 0), <=(i1238[6], 1))=TRUE ⇒ LOAD3607(java.lang.Object(ARRAY(i3[6], a4210data[6])), i615[6], i477[6], o3142[6], i1238[6], o3141[6])≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[6], a4210data[6])), i615[6], i477[6], o3142[6], i1238[6], o3141[6])≥COND_LOAD36071(&&(>(i1238[6], 0), <=(i1238[6], 1)), java.lang.Object(ARRAY(i3[6], a4210data[6])), i615[6], i477[6], o3142[6], i1238[6], o3141[6])∧(UIncreasing(COND_LOAD36071(&&(>(i1238[6], 0), <=(i1238[6], 1)), java.lang.Object(ARRAY(i3[6], a4210data[6])), i615[6], i477[6], o3142[6], i1238[6], o3141[6])), ≥))
(93) (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD36071(&&(>(i1238[6], 0), <=(i1238[6], 1)), java.lang.Object(ARRAY(i3[6], a4210data[6])), i615[6], i477[6], o3142[6], i1238[6], o3141[6])), ≥)∧[(-1)Bound*bni_107] + [bni_107]o3141[6] + [bni_107]o3142[6] ≥ 0∧[(-1)bso_108] + o3141[6] ≥ 0)
(94) (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD36071(&&(>(i1238[6], 0), <=(i1238[6], 1)), java.lang.Object(ARRAY(i3[6], a4210data[6])), i615[6], i477[6], o3142[6], i1238[6], o3141[6])), ≥)∧[(-1)Bound*bni_107] + [bni_107]o3141[6] + [bni_107]o3142[6] ≥ 0∧[(-1)bso_108] + o3141[6] ≥ 0)
(95) (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD36071(&&(>(i1238[6], 0), <=(i1238[6], 1)), java.lang.Object(ARRAY(i3[6], a4210data[6])), i615[6], i477[6], o3142[6], i1238[6], o3141[6])), ≥)∧[(-1)Bound*bni_107] + [bni_107]o3141[6] + [bni_107]o3142[6] ≥ 0∧[(-1)bso_108] + o3141[6] ≥ 0)
(96) (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD36071(&&(>(i1238[6], 0), <=(i1238[6], 1)), java.lang.Object(ARRAY(i3[6], a4210data[6])), i615[6], i477[6], o3142[6], i1238[6], o3141[6])), ≥)∧[bni_107] ≥ 0∧0 ≥ 0∧[bni_107] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)Bound*bni_107] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_108] ≥ 0)
(97) (i615[7]=i615[12]∧o3141[7]=java.lang.Object(IntList(o3234[12], i1289[12]))∧i477[7]=i477[12]∧i3[7]=i3[12]∧a4210data[7]=a4210data[12]∧o3142[7]=o3142[12] ⇒ COND_LOAD36071(TRUE, java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], i1238[7], o3141[7])≥NonInfC∧COND_LOAD36071(TRUE, java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], i1238[7], o3141[7])≥LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])∧(UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])), ≥))
(98) (COND_LOAD36071(TRUE, java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], i1238[7], java.lang.Object(IntList(o3234[12], i1289[12])))≥NonInfC∧COND_LOAD36071(TRUE, java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], i1238[7], java.lang.Object(IntList(o3234[12], i1289[12])))≥LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], java.lang.Object(IntList(o3234[12], i1289[12])))∧(UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])), ≥))
(99) ((UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])), ≥)∧[(-1)bso_110] ≥ 0)
(100) ((UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])), ≥)∧[(-1)bso_110] ≥ 0)
(101) ((UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])), ≥)∧[(-1)bso_110] ≥ 0)
(102) ((UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_110] ≥ 0)
(103) (o3141[7]=NULL∧i615[7]=i615[16]∧i477[7]=i477[16]∧i3[7]=i3[16]∧a4210data[7]=a4210data[16]∧o3142[7]=o3142[16] ⇒ COND_LOAD36071(TRUE, java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], i1238[7], o3141[7])≥NonInfC∧COND_LOAD36071(TRUE, java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], i1238[7], o3141[7])≥LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])∧(UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])), ≥))
(104) (COND_LOAD36071(TRUE, java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], i1238[7], NULL)≥NonInfC∧COND_LOAD36071(TRUE, java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], i1238[7], NULL)≥LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], NULL)∧(UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])), ≥))
(105) ((UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])), ≥)∧[(-1)bso_110] ≥ 0)
(106) ((UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])), ≥)∧[(-1)bso_110] ≥ 0)
(107) ((UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])), ≥)∧[(-1)bso_110] ≥ 0)
(108) ((UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_110] ≥ 0)
(109) (i3[7]=i3[18]∧a4210data[7]=a4210data[18]∧o3142[7]=java.lang.Object(IntList(o3239[18], i1291[18]))∧i477[7]=i477[18]∧o3141[7]=java.lang.Object(IntList(o3239[18], i1291[18]))∧i615[7]=i615[18] ⇒ COND_LOAD36071(TRUE, java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], i1238[7], o3141[7])≥NonInfC∧COND_LOAD36071(TRUE, java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], i1238[7], o3141[7])≥LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])∧(UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])), ≥))
(110) (COND_LOAD36071(TRUE, java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], java.lang.Object(IntList(o3239[18], i1291[18])), i1238[7], java.lang.Object(IntList(o3239[18], i1291[18])))≥NonInfC∧COND_LOAD36071(TRUE, java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], java.lang.Object(IntList(o3239[18], i1291[18])), i1238[7], java.lang.Object(IntList(o3239[18], i1291[18])))≥LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], java.lang.Object(IntList(o3239[18], i1291[18])), java.lang.Object(IntList(o3239[18], i1291[18])))∧(UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])), ≥))
(111) ((UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])), ≥)∧[(-1)bso_110] ≥ 0)
(112) ((UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])), ≥)∧[(-1)bso_110] ≥ 0)
(113) ((UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])), ≥)∧[(-1)bso_110] ≥ 0)
(114) ((UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_110] ≥ 0)
(115) (i477[8]=i477[9]∧o3142[8]=o3142[9]∧i615[8]=i615[9]∧i3[8]=i3[9]∧a4210data[8]=a4210data[9]∧i1238[8]=i1238[9]∧>(i1238[8], 1)=TRUE ⇒ LOAD3607(java.lang.Object(ARRAY(i3[8], a4210data[8])), i615[8], i477[8], o3142[8], i1238[8], NULL)≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[8], a4210data[8])), i615[8], i477[8], o3142[8], i1238[8], NULL)≥COND_LOAD36072(>(i1238[8], 1), java.lang.Object(ARRAY(i3[8], a4210data[8])), i615[8], i477[8], o3142[8], i1238[8])∧(UIncreasing(COND_LOAD36072(>(i1238[8], 1), java.lang.Object(ARRAY(i3[8], a4210data[8])), i615[8], i477[8], o3142[8], i1238[8])), ≥))
(116) (>(i1238[8], 1)=TRUE ⇒ LOAD3607(java.lang.Object(ARRAY(i3[8], a4210data[8])), i615[8], i477[8], o3142[8], i1238[8], NULL)≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[8], a4210data[8])), i615[8], i477[8], o3142[8], i1238[8], NULL)≥COND_LOAD36072(>(i1238[8], 1), java.lang.Object(ARRAY(i3[8], a4210data[8])), i615[8], i477[8], o3142[8], i1238[8])∧(UIncreasing(COND_LOAD36072(>(i1238[8], 1), java.lang.Object(ARRAY(i3[8], a4210data[8])), i615[8], i477[8], o3142[8], i1238[8])), ≥))
(117) (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD36072(>(i1238[8], 1), java.lang.Object(ARRAY(i3[8], a4210data[8])), i615[8], i477[8], o3142[8], i1238[8])), ≥)∧[bni_111 + (-1)Bound*bni_111] + [bni_111]o3142[8] ≥ 0∧[(-1)bso_112] ≥ 0)
(118) (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD36072(>(i1238[8], 1), java.lang.Object(ARRAY(i3[8], a4210data[8])), i615[8], i477[8], o3142[8], i1238[8])), ≥)∧[bni_111 + (-1)Bound*bni_111] + [bni_111]o3142[8] ≥ 0∧[(-1)bso_112] ≥ 0)
(119) (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD36072(>(i1238[8], 1), java.lang.Object(ARRAY(i3[8], a4210data[8])), i615[8], i477[8], o3142[8], i1238[8])), ≥)∧[bni_111 + (-1)Bound*bni_111] + [bni_111]o3142[8] ≥ 0∧[(-1)bso_112] ≥ 0)
(120) (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD36072(>(i1238[8], 1), java.lang.Object(ARRAY(i3[8], a4210data[8])), i615[8], i477[8], o3142[8], i1238[8])), ≥)∧0 ≥ 0∧[bni_111] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[bni_111 + (-1)Bound*bni_111] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_112] ≥ 0)
(121) (COND_LOAD36072(TRUE, java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], i1238[9])≥NonInfC∧COND_LOAD36072(TRUE, java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], i1238[9])≥LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)∧(UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)), ≥))
(122) ((UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)), ≥)∧[1 + (-1)bso_114] ≥ 0)
(123) ((UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)), ≥)∧[1 + (-1)bso_114] ≥ 0)
(124) ((UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)), ≥)∧[1 + (-1)bso_114] ≥ 0)
(125) ((UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_114] ≥ 0)
(126) (i477[8]=i477[9]∧o3142[8]=o3142[9]∧i615[8]=i615[9]∧i3[8]=i3[9]∧a4210data[8]=a4210data[9]∧i1238[8]=i1238[9]∧>(i1238[8], 1)=TRUE∧i477[9]=i477[16]∧i3[9]=i3[16]∧a4210data[9]=a4210data[16]∧i615[9]=i615[16]∧o3142[9]=o3142[16] ⇒ COND_LOAD36072(TRUE, java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], i1238[9])≥NonInfC∧COND_LOAD36072(TRUE, java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], i1238[9])≥LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)∧(UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)), ≥))
(127) (>(i1238[8], 1)=TRUE ⇒ COND_LOAD36072(TRUE, java.lang.Object(ARRAY(i3[8], a4210data[8])), i615[8], i477[8], o3142[8], i1238[8])≥NonInfC∧COND_LOAD36072(TRUE, java.lang.Object(ARRAY(i3[8], a4210data[8])), i615[8], i477[8], o3142[8], i1238[8])≥LOAD3637(java.lang.Object(ARRAY(i3[8], a4210data[8])), i615[8], i477[8], o3142[8], NULL)∧(UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)), ≥))
(128) (0 ≥ 0 ⇒ (UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)), ≥)∧0 ≥ 0∧[1 + (-1)bso_114] ≥ 0)
(129) (0 ≥ 0 ⇒ (UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)), ≥)∧0 ≥ 0∧[1 + (-1)bso_114] ≥ 0)
(130) (0 ≥ 0 ⇒ (UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)), ≥)∧0 ≥ 0∧[1 + (-1)bso_114] ≥ 0)
(131) (0 ≥ 0 ⇒ (UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_114] ≥ 0)
(132) (COND_LOAD36072(TRUE, java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], i1238[9])≥NonInfC∧COND_LOAD36072(TRUE, java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], i1238[9])≥LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)∧(UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)), ≥))
(133) ((UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)), ≥)∧[1 + (-1)bso_114] ≥ 0)
(134) ((UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)), ≥)∧[1 + (-1)bso_114] ≥ 0)
(135) ((UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)), ≥)∧[1 + (-1)bso_114] ≥ 0)
(136) ((UIncreasing(LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_114] ≥ 0)
(137) (i1289[10]=i477[0]∧i615[10]=i118[0]∧o3142[10]=java.lang.Object(IntList(o1856[0], i480[0]))∧i3[10]=i3[0]∧a4210data[10]=a2436data[0] ⇒ STORE3886(java.lang.Object(ARRAY(i3[10], a4210data[10])), i615[10], o3142[10], i477[10], i1289[10])≥NonInfC∧STORE3886(java.lang.Object(ARRAY(i3[10], a4210data[10])), i615[10], o3142[10], i477[10], i1289[10])≥LOAD2305(java.lang.Object(ARRAY(i3[10], a4210data[10])), i615[10], o3142[10], i1289[10])∧(UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[10], a4210data[10])), i615[10], o3142[10], i1289[10])), ≥))
(138) (STORE3886(java.lang.Object(ARRAY(i3[10], a4210data[10])), i615[10], java.lang.Object(IntList(o1856[0], i480[0])), i477[10], i1289[10])≥NonInfC∧STORE3886(java.lang.Object(ARRAY(i3[10], a4210data[10])), i615[10], java.lang.Object(IntList(o1856[0], i480[0])), i477[10], i1289[10])≥LOAD2305(java.lang.Object(ARRAY(i3[10], a4210data[10])), i615[10], java.lang.Object(IntList(o1856[0], i480[0])), i1289[10])∧(UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[10], a4210data[10])), i615[10], o3142[10], i1289[10])), ≥))
(139) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[10], a4210data[10])), i615[10], o3142[10], i1289[10])), ≥)∧[(-1)bso_116] + [2]i1289[10] ≥ 0)
(140) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[10], a4210data[10])), i615[10], o3142[10], i1289[10])), ≥)∧[(-1)bso_116] + [2]i1289[10] ≥ 0)
(141) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[10], a4210data[10])), i615[10], o3142[10], i1289[10])), ≥)∧[(-1)bso_116] + [2]i1289[10] ≥ 0)
(142) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[10], a4210data[10])), i615[10], o3142[10], i1289[10])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_116] ≥ 0∧[1] ≥ 0)
(143) (i615[11]=i118[0]∧i1289[11]=i477[0]∧o3142[11]=java.lang.Object(IntList(o1856[0], i480[0]))∧i3[11]=i3[0]∧a4210data[11]=a2436data[0] ⇒ RETURN3818(java.lang.Object(ARRAY(i3[11], a4210data[11])), i615[11], i477[11], o3142[11], i1289[11])≥NonInfC∧RETURN3818(java.lang.Object(ARRAY(i3[11], a4210data[11])), i615[11], i477[11], o3142[11], i1289[11])≥LOAD2305(java.lang.Object(ARRAY(i3[11], a4210data[11])), i615[11], o3142[11], i1289[11])∧(UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[11], a4210data[11])), i615[11], o3142[11], i1289[11])), ≥))
(144) (RETURN3818(java.lang.Object(ARRAY(i3[11], a4210data[11])), i615[11], i477[11], java.lang.Object(IntList(o1856[0], i480[0])), i1289[11])≥NonInfC∧RETURN3818(java.lang.Object(ARRAY(i3[11], a4210data[11])), i615[11], i477[11], java.lang.Object(IntList(o1856[0], i480[0])), i1289[11])≥LOAD2305(java.lang.Object(ARRAY(i3[11], a4210data[11])), i615[11], java.lang.Object(IntList(o1856[0], i480[0])), i1289[11])∧(UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[11], a4210data[11])), i615[11], o3142[11], i1289[11])), ≥))
(145) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[11], a4210data[11])), i615[11], o3142[11], i1289[11])), ≥)∧[(-1)bso_118] ≥ 0)
(146) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[11], a4210data[11])), i615[11], o3142[11], i1289[11])), ≥)∧[(-1)bso_118] ≥ 0)
(147) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[11], a4210data[11])), i615[11], o3142[11], i1289[11])), ≥)∧[(-1)bso_118] ≥ 0)
(148) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[11], a4210data[11])), i615[11], o3142[11], i1289[11])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_118] ≥ 0)
(149) (i615[7]=i615[12]∧o3141[7]=java.lang.Object(IntList(o3234[12], i1289[12]))∧i477[7]=i477[12]∧i3[7]=i3[12]∧a4210data[7]=a4210data[12]∧o3142[7]=o3142[12]∧o3142[12]=java.lang.Object(IntList(o1856[0], i480[0]))∧i1289[12]=i477[0]∧i615[12]=i118[0]∧i3[12]=i3[0]∧a4210data[12]=a2436data[0] ⇒ LOAD3637(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], i477[12], o3142[12], java.lang.Object(IntList(o3234[12], i1289[12])))≥NonInfC∧LOAD3637(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], i477[12], o3142[12], java.lang.Object(IntList(o3234[12], i1289[12])))≥LOAD2305(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], o3142[12], i1289[12])∧(UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], o3142[12], i1289[12])), ≥))
(150) (LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], java.lang.Object(IntList(o1856[0], i480[0])), java.lang.Object(IntList(o3234[12], i1289[12])))≥NonInfC∧LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], java.lang.Object(IntList(o1856[0], i480[0])), java.lang.Object(IntList(o3234[12], i1289[12])))≥LOAD2305(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], java.lang.Object(IntList(o1856[0], i480[0])), i1289[12])∧(UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], o3142[12], i1289[12])), ≥))
(151) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], o3142[12], i1289[12])), ≥)∧[(-1)bso_120] ≥ 0)
(152) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], o3142[12], i1289[12])), ≥)∧[(-1)bso_120] ≥ 0)
(153) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], o3142[12], i1289[12])), ≥)∧[(-1)bso_120] ≥ 0)
(154) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], o3142[12], i1289[12])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_120] ≥ 0)
(155) (LOAD3637(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], i477[12], o3142[12], java.lang.Object(IntList(o3234[12], i1289[12])))≥NonInfC∧LOAD3637(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], i477[12], o3142[12], java.lang.Object(IntList(o3234[12], i1289[12])))≥LOAD2305(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], o3142[12], i1289[12])∧(UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], o3142[12], i1289[12])), ≥))
(156) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], o3142[12], i1289[12])), ≥)∧[(-1)bso_120] ≥ 0)
(157) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], o3142[12], i1289[12])), ≥)∧[(-1)bso_120] ≥ 0)
(158) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], o3142[12], i1289[12])), ≥)∧[(-1)bso_120] ≥ 0)
(159) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], o3142[12], i1289[12])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_120] ≥ 0)
(160) (i771[2]=0∧o1856[2]=o3142[13]∧i477[2]=i477[13]∧i3[2]=i3[13]∧a2436data[2]=a4210data[13]∧o1856[2]=java.lang.Object(IntList(o3234[13], i1289[13]))∧+(i118[2], 1)=i615[13]∧i1289[13]=i477[0]∧o3142[13]=java.lang.Object(IntList(o1856[0], i480[0]))∧i615[13]=i118[0]∧i3[13]=i3[0]∧a4210data[13]=a2436data[0] ⇒ LOAD3607(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], i477[13], o3142[13], 0, java.lang.Object(IntList(o3234[13], i1289[13])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], i477[13], o3142[13], 0, java.lang.Object(IntList(o3234[13], i1289[13])))≥LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])∧(UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])), ≥))
(161) (LOAD3607(java.lang.Object(ARRAY(i3[2], a2436data[2])), +(i118[2], 1), i477[2], java.lang.Object(IntList(o3234[13], i1289[13])), 0, java.lang.Object(IntList(o3234[13], i1289[13])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[2], a2436data[2])), +(i118[2], 1), i477[2], java.lang.Object(IntList(o3234[13], i1289[13])), 0, java.lang.Object(IntList(o3234[13], i1289[13])))≥LOAD2305(java.lang.Object(ARRAY(i3[2], a2436data[2])), +(i118[2], 1), java.lang.Object(IntList(o3234[13], i1289[13])), i1289[13])∧(UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])), ≥))
(162) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])), ≥)∧[(-1)bso_122] + [2]o3234[13] ≥ 0)
(163) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])), ≥)∧[(-1)bso_122] + [2]o3234[13] ≥ 0)
(164) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])), ≥)∧[(-1)bso_122] + [2]o3234[13] ≥ 0)
(165) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_122] ≥ 0∧[1] ≥ 0)
(166) (i477[3]=i477[13]∧i3[3]=i3[13]∧a4210data[3]=a4210data[13]∧o3274[3]=java.lang.Object(IntList(o3234[13], i1289[13]))∧i1284[3]=0∧i615[3]=i615[13]∧o3142[3]=o3142[13]∧i1289[13]=i477[0]∧o3142[13]=java.lang.Object(IntList(o1856[0], i480[0]))∧i615[13]=i118[0]∧i3[13]=i3[0]∧a4210data[13]=a2436data[0] ⇒ LOAD3607(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], i477[13], o3142[13], 0, java.lang.Object(IntList(o3234[13], i1289[13])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], i477[13], o3142[13], 0, java.lang.Object(IntList(o3234[13], i1289[13])))≥LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])∧(UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])), ≥))
(167) (LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], java.lang.Object(IntList(o1856[0], i480[0])), 0, java.lang.Object(IntList(o3234[13], i1289[13])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], java.lang.Object(IntList(o1856[0], i480[0])), 0, java.lang.Object(IntList(o3234[13], i1289[13])))≥LOAD2305(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], java.lang.Object(IntList(o1856[0], i480[0])), i1289[13])∧(UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])), ≥))
(168) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])), ≥)∧[(-1)bso_122] + [2]o3234[13] ≥ 0)
(169) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])), ≥)∧[(-1)bso_122] + [2]o3234[13] ≥ 0)
(170) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])), ≥)∧[(-1)bso_122] + [2]o3234[13] ≥ 0)
(171) ((UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_122] ≥ 0∧[1] ≥ 0)
(172) (+(i1238[5], -1)=0∧i615[5]=i615[13]∧o3142[5]=o3142[13]∧o3274[5]=java.lang.Object(IntList(o3234[13], i1289[13]))∧i477[5]=i477[13]∧i3[5]=i3[13]∧a4210data[5]=a4210data[13]∧i1289[13]=i477[0]∧o3142[13]=java.lang.Object(IntList(o1856[0], i480[0]))∧i615[13]=i118[0]∧i3[13]=i3[0]∧a4210data[13]=a2436data[0] ⇒ LOAD3607(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], i477[13], o3142[13], 0, java.lang.Object(IntList(o3234[13], i1289[13])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], i477[13], o3142[13], 0, java.lang.Object(IntList(o3234[13], i1289[13])))≥LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])∧(UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])), ≥))
(173) (+(i1238[5], -1)=0 ⇒ LOAD3607(java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], java.lang.Object(IntList(o1856[0], i480[0])), 0, java.lang.Object(IntList(o3234[13], i1289[13])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], java.lang.Object(IntList(o1856[0], i480[0])), 0, java.lang.Object(IntList(o3234[13], i1289[13])))≥LOAD2305(java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], java.lang.Object(IntList(o1856[0], i480[0])), i1289[13])∧(UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])), ≥))
(174) (0 ≥ 0 ⇒ (UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])), ≥)∧0 ≥ 0∧[(-1)bso_122] + [2]o3234[13] ≥ 0)
(175) (0 ≥ 0 ⇒ (UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])), ≥)∧0 ≥ 0∧[(-1)bso_122] + [2]o3234[13] ≥ 0)
(176) (0 ≥ 0 ⇒ (UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])), ≥)∧0 ≥ 0∧[(-1)bso_122] + [2]o3234[13] ≥ 0)
(177) (0 ≥ 0 ⇒ (UIncreasing(LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_122] ≥ 0∧[1] ≥ 0)
(178) (i477[14]=i477[15]∧i1238[14]=i1238[15]∧>(i1238[14], 1)=TRUE∧i3[14]=i3[15]∧a4210data[14]=a4210data[15]∧i615[14]=i615[15]∧o3280[14]=o3280[15]∧i1314[14]=i1314[15] ⇒ LOAD3607(java.lang.Object(ARRAY(i3[14], a4210data[14])), i615[14], i477[14], java.lang.Object(IntList(o3280[14], i1314[14])), i1238[14], java.lang.Object(IntList(o3280[14], i1314[14])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[14], a4210data[14])), i615[14], i477[14], java.lang.Object(IntList(o3280[14], i1314[14])), i1238[14], java.lang.Object(IntList(o3280[14], i1314[14])))≥COND_LOAD36073(>(i1238[14], 1), java.lang.Object(ARRAY(i3[14], a4210data[14])), i615[14], i477[14], i1238[14], java.lang.Object(IntList(o3280[14], i1314[14])))∧(UIncreasing(COND_LOAD36073(>(i1238[14], 1), java.lang.Object(ARRAY(i3[14], a4210data[14])), i615[14], i477[14], i1238[14], java.lang.Object(IntList(o3280[14], i1314[14])))), ≥))
(179) (>(i1238[14], 1)=TRUE ⇒ LOAD3607(java.lang.Object(ARRAY(i3[14], a4210data[14])), i615[14], i477[14], java.lang.Object(IntList(o3280[14], i1314[14])), i1238[14], java.lang.Object(IntList(o3280[14], i1314[14])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[14], a4210data[14])), i615[14], i477[14], java.lang.Object(IntList(o3280[14], i1314[14])), i1238[14], java.lang.Object(IntList(o3280[14], i1314[14])))≥COND_LOAD36073(>(i1238[14], 1), java.lang.Object(ARRAY(i3[14], a4210data[14])), i615[14], i477[14], i1238[14], java.lang.Object(IntList(o3280[14], i1314[14])))∧(UIncreasing(COND_LOAD36073(>(i1238[14], 1), java.lang.Object(ARRAY(i3[14], a4210data[14])), i615[14], i477[14], i1238[14], java.lang.Object(IntList(o3280[14], i1314[14])))), ≥))
(180) (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD36073(>(i1238[14], 1), java.lang.Object(ARRAY(i3[14], a4210data[14])), i615[14], i477[14], i1238[14], java.lang.Object(IntList(o3280[14], i1314[14])))), ≥)∧[(-1)Bound*bni_123] + [(4)bni_123]o3280[14] ≥ 0∧[(-1)bso_124] ≥ 0)
(181) (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD36073(>(i1238[14], 1), java.lang.Object(ARRAY(i3[14], a4210data[14])), i615[14], i477[14], i1238[14], java.lang.Object(IntList(o3280[14], i1314[14])))), ≥)∧[(-1)Bound*bni_123] + [(4)bni_123]o3280[14] ≥ 0∧[(-1)bso_124] ≥ 0)
(182) (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD36073(>(i1238[14], 1), java.lang.Object(ARRAY(i3[14], a4210data[14])), i615[14], i477[14], i1238[14], java.lang.Object(IntList(o3280[14], i1314[14])))), ≥)∧[(-1)Bound*bni_123] + [(4)bni_123]o3280[14] ≥ 0∧[(-1)bso_124] ≥ 0)
(183) (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD36073(>(i1238[14], 1), java.lang.Object(ARRAY(i3[14], a4210data[14])), i615[14], i477[14], i1238[14], java.lang.Object(IntList(o3280[14], i1314[14])))), ≥)∧0 ≥ 0∧[(4)bni_123] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)Bound*bni_123] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_124] ≥ 0)
(184) (i477[14]=i477[15]∧i1238[14]=i1238[15]∧>(i1238[14], 1)=TRUE∧i3[14]=i3[15]∧a4210data[14]=a4210data[15]∧i615[14]=i615[15]∧o3280[14]=o3280[15]∧i1314[14]=i1314[15]∧+(i1238[15], -1)=i1284[3]∧i477[15]=i477[3]∧i615[15]=i615[3]∧java.lang.Object(IntList(o3280[15], i1314[15]))=o3142[3]∧i3[15]=i3[3]∧a4210data[15]=a4210data[3]∧o3280[15]=o3274[3] ⇒ COND_LOAD36073(TRUE, java.lang.Object(ARRAY(i3[15], a4210data[15])), i615[15], i477[15], i1238[15], java.lang.Object(IntList(o3280[15], i1314[15])))≥NonInfC∧COND_LOAD36073(TRUE, java.lang.Object(ARRAY(i3[15], a4210data[15])), i615[15], i477[15], i1238[15], java.lang.Object(IntList(o3280[15], i1314[15])))≥JMP3960'(java.lang.Object(ARRAY(i3[15], a4210data[15])), i615[15], i477[15], java.lang.Object(IntList(o3280[15], i1314[15])), +(i1238[15], -1), o3280[15])∧(UIncreasing(JMP3960'(java.lang.Object(ARRAY(i3[15], a4210data[15])), i615[15], i477[15], java.lang.Object(IntList(o3280[15], i1314[15])), +(i1238[15], -1), o3280[15])), ≥))
(185) (>(i1238[14], 1)=TRUE ⇒ COND_LOAD36073(TRUE, java.lang.Object(ARRAY(i3[14], a4210data[14])), i615[14], i477[14], i1238[14], java.lang.Object(IntList(o3280[14], i1314[14])))≥NonInfC∧COND_LOAD36073(TRUE, java.lang.Object(ARRAY(i3[14], a4210data[14])), i615[14], i477[14], i1238[14], java.lang.Object(IntList(o3280[14], i1314[14])))≥JMP3960'(java.lang.Object(ARRAY(i3[14], a4210data[14])), i615[14], i477[14], java.lang.Object(IntList(o3280[14], i1314[14])), +(i1238[14], -1), o3280[14])∧(UIncreasing(JMP3960'(java.lang.Object(ARRAY(i3[15], a4210data[15])), i615[15], i477[15], java.lang.Object(IntList(o3280[15], i1314[15])), +(i1238[15], -1), o3280[15])), ≥))
(186) (0 ≥ 0 ⇒ (UIncreasing(JMP3960'(java.lang.Object(ARRAY(i3[15], a4210data[15])), i615[15], i477[15], java.lang.Object(IntList(o3280[15], i1314[15])), +(i1238[15], -1), o3280[15])), ≥)∧[(-1)Bound*bni_125] + [(4)bni_125]o3280[14] ≥ 0∧[(-1)bso_126] + o3280[14] ≥ 0)
(187) (0 ≥ 0 ⇒ (UIncreasing(JMP3960'(java.lang.Object(ARRAY(i3[15], a4210data[15])), i615[15], i477[15], java.lang.Object(IntList(o3280[15], i1314[15])), +(i1238[15], -1), o3280[15])), ≥)∧[(-1)Bound*bni_125] + [(4)bni_125]o3280[14] ≥ 0∧[(-1)bso_126] + o3280[14] ≥ 0)
(188) (0 ≥ 0 ⇒ (UIncreasing(JMP3960'(java.lang.Object(ARRAY(i3[15], a4210data[15])), i615[15], i477[15], java.lang.Object(IntList(o3280[15], i1314[15])), +(i1238[15], -1), o3280[15])), ≥)∧[(-1)Bound*bni_125] + [(4)bni_125]o3280[14] ≥ 0∧[(-1)bso_126] + o3280[14] ≥ 0)
(189) (0 ≥ 0 ⇒ (UIncreasing(JMP3960'(java.lang.Object(ARRAY(i3[15], a4210data[15])), i615[15], i477[15], java.lang.Object(IntList(o3280[15], i1314[15])), +(i1238[15], -1), o3280[15])), ≥)∧0 ≥ 0∧[(4)bni_125] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)Bound*bni_125] ≥ 0∧0 ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_126] ≥ 0)
(190) (o3141[7]=NULL∧i615[7]=i615[16]∧i477[7]=i477[16]∧i3[7]=i3[16]∧a4210data[7]=a4210data[16]∧o3142[7]=o3142[16]∧i615[16]=i615[10]∧o3142[16]=o3142[10]∧i3[16]=i3[10]∧a4210data[16]=a4210data[10]∧0=i1289[10]∧i477[16]=i477[10] ⇒ LOAD3637(java.lang.Object(ARRAY(i3[16], a4210data[16])), i615[16], i477[16], o3142[16], NULL)≥NonInfC∧LOAD3637(java.lang.Object(ARRAY(i3[16], a4210data[16])), i615[16], i477[16], o3142[16], NULL)≥STORE3886(java.lang.Object(ARRAY(i3[16], a4210data[16])), i615[16], o3142[16], i477[16], 0)∧(UIncreasing(STORE3886(java.lang.Object(ARRAY(i3[16], a4210data[16])), i615[16], o3142[16], i477[16], 0)), ≥))
(191) (LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], NULL)≥NonInfC∧LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], NULL)≥STORE3886(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], o3142[7], i477[7], 0)∧(UIncreasing(STORE3886(java.lang.Object(ARRAY(i3[16], a4210data[16])), i615[16], o3142[16], i477[16], 0)), ≥))
(192) ((UIncreasing(STORE3886(java.lang.Object(ARRAY(i3[16], a4210data[16])), i615[16], o3142[16], i477[16], 0)), ≥)∧[(-1)bso_128] ≥ 0)
(193) ((UIncreasing(STORE3886(java.lang.Object(ARRAY(i3[16], a4210data[16])), i615[16], o3142[16], i477[16], 0)), ≥)∧[(-1)bso_128] ≥ 0)
(194) ((UIncreasing(STORE3886(java.lang.Object(ARRAY(i3[16], a4210data[16])), i615[16], o3142[16], i477[16], 0)), ≥)∧[(-1)bso_128] ≥ 0)
(195) ((UIncreasing(STORE3886(java.lang.Object(ARRAY(i3[16], a4210data[16])), i615[16], o3142[16], i477[16], 0)), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_128] ≥ 0)
(196) (i477[9]=i477[16]∧i3[9]=i3[16]∧a4210data[9]=a4210data[16]∧i615[9]=i615[16]∧o3142[9]=o3142[16]∧i615[16]=i615[10]∧o3142[16]=o3142[10]∧i3[16]=i3[10]∧a4210data[16]=a4210data[10]∧0=i1289[10]∧i477[16]=i477[10] ⇒ LOAD3637(java.lang.Object(ARRAY(i3[16], a4210data[16])), i615[16], i477[16], o3142[16], NULL)≥NonInfC∧LOAD3637(java.lang.Object(ARRAY(i3[16], a4210data[16])), i615[16], i477[16], o3142[16], NULL)≥STORE3886(java.lang.Object(ARRAY(i3[16], a4210data[16])), i615[16], o3142[16], i477[16], 0)∧(UIncreasing(STORE3886(java.lang.Object(ARRAY(i3[16], a4210data[16])), i615[16], o3142[16], i477[16], 0)), ≥))
(197) (LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)≥NonInfC∧LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)≥STORE3886(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], o3142[9], i477[9], 0)∧(UIncreasing(STORE3886(java.lang.Object(ARRAY(i3[16], a4210data[16])), i615[16], o3142[16], i477[16], 0)), ≥))
(198) ((UIncreasing(STORE3886(java.lang.Object(ARRAY(i3[16], a4210data[16])), i615[16], o3142[16], i477[16], 0)), ≥)∧[(-1)bso_128] ≥ 0)
(199) ((UIncreasing(STORE3886(java.lang.Object(ARRAY(i3[16], a4210data[16])), i615[16], o3142[16], i477[16], 0)), ≥)∧[(-1)bso_128] ≥ 0)
(200) ((UIncreasing(STORE3886(java.lang.Object(ARRAY(i3[16], a4210data[16])), i615[16], o3142[16], i477[16], 0)), ≥)∧[(-1)bso_128] ≥ 0)
(201) ((UIncreasing(STORE3886(java.lang.Object(ARRAY(i3[16], a4210data[16])), i615[16], o3142[16], i477[16], 0)), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_128] ≥ 0)
(202) (o3142[17]=o3142[10]∧i477[17]=i477[10]∧i3[17]=i3[10]∧a4210data[17]=a4210data[10]∧0=i1289[10]∧i615[17]=i615[10] ⇒ LOAD3607(java.lang.Object(ARRAY(i3[17], a4210data[17])), i615[17], i477[17], o3142[17], 0, NULL)≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[17], a4210data[17])), i615[17], i477[17], o3142[17], 0, NULL)≥STORE3886(java.lang.Object(ARRAY(i3[17], a4210data[17])), i615[17], o3142[17], i477[17], 0)∧(UIncreasing(STORE3886(java.lang.Object(ARRAY(i3[17], a4210data[17])), i615[17], o3142[17], i477[17], 0)), ≥))
(203) (LOAD3607(java.lang.Object(ARRAY(i3[17], a4210data[17])), i615[17], i477[17], o3142[17], 0, NULL)≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[17], a4210data[17])), i615[17], i477[17], o3142[17], 0, NULL)≥STORE3886(java.lang.Object(ARRAY(i3[17], a4210data[17])), i615[17], o3142[17], i477[17], 0)∧(UIncreasing(STORE3886(java.lang.Object(ARRAY(i3[17], a4210data[17])), i615[17], o3142[17], i477[17], 0)), ≥))
(204) ((UIncreasing(STORE3886(java.lang.Object(ARRAY(i3[17], a4210data[17])), i615[17], o3142[17], i477[17], 0)), ≥)∧[1 + (-1)bso_130] ≥ 0)
(205) ((UIncreasing(STORE3886(java.lang.Object(ARRAY(i3[17], a4210data[17])), i615[17], o3142[17], i477[17], 0)), ≥)∧[1 + (-1)bso_130] ≥ 0)
(206) ((UIncreasing(STORE3886(java.lang.Object(ARRAY(i3[17], a4210data[17])), i615[17], o3142[17], i477[17], 0)), ≥)∧[1 + (-1)bso_130] ≥ 0)
(207) ((UIncreasing(STORE3886(java.lang.Object(ARRAY(i3[17], a4210data[17])), i615[17], o3142[17], i477[17], 0)), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_130] ≥ 0)
(208) (i3[7]=i3[18]∧a4210data[7]=a4210data[18]∧o3142[7]=java.lang.Object(IntList(o3239[18], i1291[18]))∧i477[7]=i477[18]∧o3141[7]=java.lang.Object(IntList(o3239[18], i1291[18]))∧i615[7]=i615[18]∧java.lang.Object(IntList(o3239[18], i1291[18]))=o3142[11]∧i615[18]=i615[11]∧i477[18]=i477[11]∧i1291[18]=i1289[11]∧i3[18]=i3[11]∧a4210data[18]=a4210data[11] ⇒ LOAD3637(java.lang.Object(ARRAY(i3[18], a4210data[18])), i615[18], i477[18], java.lang.Object(IntList(o3239[18], i1291[18])), java.lang.Object(IntList(o3239[18], i1291[18])))≥NonInfC∧LOAD3637(java.lang.Object(ARRAY(i3[18], a4210data[18])), i615[18], i477[18], java.lang.Object(IntList(o3239[18], i1291[18])), java.lang.Object(IntList(o3239[18], i1291[18])))≥RETURN3818(java.lang.Object(ARRAY(i3[18], a4210data[18])), i615[18], i477[18], java.lang.Object(IntList(o3239[18], i1291[18])), i1291[18])∧(UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[18], a4210data[18])), i615[18], i477[18], java.lang.Object(IntList(o3239[18], i1291[18])), i1291[18])), ≥))
(209) (LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], java.lang.Object(IntList(o3239[18], i1291[18])), java.lang.Object(IntList(o3239[18], i1291[18])))≥NonInfC∧LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], java.lang.Object(IntList(o3239[18], i1291[18])), java.lang.Object(IntList(o3239[18], i1291[18])))≥RETURN3818(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], java.lang.Object(IntList(o3239[18], i1291[18])), i1291[18])∧(UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[18], a4210data[18])), i615[18], i477[18], java.lang.Object(IntList(o3239[18], i1291[18])), i1291[18])), ≥))
(210) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[18], a4210data[18])), i615[18], i477[18], java.lang.Object(IntList(o3239[18], i1291[18])), i1291[18])), ≥)∧[(-1)bso_132] ≥ 0)
(211) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[18], a4210data[18])), i615[18], i477[18], java.lang.Object(IntList(o3239[18], i1291[18])), i1291[18])), ≥)∧[(-1)bso_132] ≥ 0)
(212) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[18], a4210data[18])), i615[18], i477[18], java.lang.Object(IntList(o3239[18], i1291[18])), i1291[18])), ≥)∧[(-1)bso_132] ≥ 0)
(213) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[18], a4210data[18])), i615[18], i477[18], java.lang.Object(IntList(o3239[18], i1291[18])), i1291[18])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_132] ≥ 0)
(214) (LOAD3637(java.lang.Object(ARRAY(i3[18], a4210data[18])), i615[18], i477[18], java.lang.Object(IntList(o3239[18], i1291[18])), java.lang.Object(IntList(o3239[18], i1291[18])))≥NonInfC∧LOAD3637(java.lang.Object(ARRAY(i3[18], a4210data[18])), i615[18], i477[18], java.lang.Object(IntList(o3239[18], i1291[18])), java.lang.Object(IntList(o3239[18], i1291[18])))≥RETURN3818(java.lang.Object(ARRAY(i3[18], a4210data[18])), i615[18], i477[18], java.lang.Object(IntList(o3239[18], i1291[18])), i1291[18])∧(UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[18], a4210data[18])), i615[18], i477[18], java.lang.Object(IntList(o3239[18], i1291[18])), i1291[18])), ≥))
(215) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[18], a4210data[18])), i615[18], i477[18], java.lang.Object(IntList(o3239[18], i1291[18])), i1291[18])), ≥)∧[(-1)bso_132] ≥ 0)
(216) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[18], a4210data[18])), i615[18], i477[18], java.lang.Object(IntList(o3239[18], i1291[18])), i1291[18])), ≥)∧[(-1)bso_132] ≥ 0)
(217) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[18], a4210data[18])), i615[18], i477[18], java.lang.Object(IntList(o3239[18], i1291[18])), i1291[18])), ≥)∧[(-1)bso_132] ≥ 0)
(218) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[18], a4210data[18])), i615[18], i477[18], java.lang.Object(IntList(o3239[18], i1291[18])), i1291[18])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_132] ≥ 0)
(219) (o1856[2]=java.lang.Object(IntList(o3239[19], i1291[19]))∧i477[2]=i477[19]∧i771[2]=0∧i3[2]=i3[19]∧a2436data[2]=a4210data[19]∧+(i118[2], 1)=i615[19]∧i3[19]=i3[11]∧a4210data[19]=a4210data[11]∧java.lang.Object(IntList(o3239[19], i1291[19]))=o3142[11]∧i1291[19]=i1289[11]∧i477[19]=i477[11]∧i615[19]=i615[11] ⇒ LOAD3607(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])∧(UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥))
(220) (LOAD3607(java.lang.Object(ARRAY(i3[2], a2436data[2])), +(i118[2], 1), i477[2], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[2], a2436data[2])), +(i118[2], 1), i477[2], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥RETURN3818(java.lang.Object(ARRAY(i3[2], a2436data[2])), +(i118[2], 1), i477[2], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])∧(UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥))
(221) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧[(-1)bso_134] + [2]o3239[19] ≥ 0)
(222) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧[(-1)bso_134] + [2]o3239[19] ≥ 0)
(223) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧[(-1)bso_134] + [2]o3239[19] ≥ 0)
(224) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_134] ≥ 0∧[1] ≥ 0)
(225) (o3274[3]=java.lang.Object(IntList(o3239[19], i1291[19]))∧i477[3]=i477[19]∧i615[3]=i615[19]∧i1284[3]=0∧i3[3]=i3[19]∧a4210data[3]=a4210data[19]∧o3142[3]=java.lang.Object(IntList(o3239[19], i1291[19]))∧i3[19]=i3[11]∧a4210data[19]=a4210data[11]∧java.lang.Object(IntList(o3239[19], i1291[19]))=o3142[11]∧i1291[19]=i1289[11]∧i477[19]=i477[11]∧i615[19]=i615[11] ⇒ LOAD3607(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])∧(UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥))
(226) (LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥RETURN3818(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])∧(UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥))
(227) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧[(-1)bso_134] + [2]o3239[19] ≥ 0)
(228) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧[(-1)bso_134] + [2]o3239[19] ≥ 0)
(229) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧[(-1)bso_134] + [2]o3239[19] ≥ 0)
(230) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_134] ≥ 0∧[1] ≥ 0)
(231) (o3274[5]=java.lang.Object(IntList(o3239[19], i1291[19]))∧o3142[5]=java.lang.Object(IntList(o3239[19], i1291[19]))∧i3[5]=i3[19]∧a4210data[5]=a4210data[19]∧+(i1238[5], -1)=0∧i615[5]=i615[19]∧i477[5]=i477[19]∧i3[19]=i3[11]∧a4210data[19]=a4210data[11]∧java.lang.Object(IntList(o3239[19], i1291[19]))=o3142[11]∧i1291[19]=i1289[11]∧i477[19]=i477[11]∧i615[19]=i615[11] ⇒ LOAD3607(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])∧(UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥))
(232) (+(i1238[5], -1)=0 ⇒ LOAD3607(java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥RETURN3818(java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])∧(UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥))
(233) (0 ≥ 0 ⇒ (UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧0 ≥ 0∧[(-1)bso_134] + [2]o3239[19] ≥ 0)
(234) (0 ≥ 0 ⇒ (UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧0 ≥ 0∧[(-1)bso_134] + [2]o3239[19] ≥ 0)
(235) (0 ≥ 0 ⇒ (UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧0 ≥ 0∧[(-1)bso_134] + [2]o3239[19] ≥ 0)
(236) (0 ≥ 0 ⇒ (UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_134] ≥ 0∧[1] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(LOAD2305(x1, x2, x3, x4)) = x3
POL(java.lang.Object(x1)) = x1
POL(ARRAY(x1, x2)) = 0
POL(IntList(x1, x2)) = [2]x1
POL(LOAD2305ARR1(x1, x2, x3, x4, x5)) = x3
POL(java.lang.String(x1, x2, x3, x4)) = 0
POL(COND_LOAD2305ARR1(x1, x2, x3, x4, x5, x6)) = x4
POL(&&(x1, x2)) = 0
POL(>(x1, x2)) = 0
POL(0) = 0
POL(<(x1, x2)) = 0
POL(+(x1, x2)) = 0
POL(1) = 0
POL(LOAD3607(x1, x2, x3, x4, x5, x6)) = x6 + x4
POL(JMP3960'(x1, x2, x3, x4, x5, x6)) = x6 + x4
POL(COND_LOAD3607(x1, x2, x3, x4, x5, x6, x7)) = x7 + x5
POL(-1) = 0
POL(COND_LOAD36071(x1, x2, x3, x4, x5, x6, x7)) = x5
POL(<=(x1, x2)) = 0
POL(LOAD3637(x1, x2, x3, x4, x5)) = x4
POL(NULL) = [1]
POL(COND_LOAD36072(x1, x2, x3, x4, x5, x6)) = [1] + x5
POL(STORE3886(x1, x2, x3, x4, x5)) = [2]x5 + x3
POL(RETURN3818(x1, x2, x3, x4, x5)) = x4
POL(COND_LOAD36073(x1, x2, x3, x4, x5, x6)) = [2]x6
COND_LOAD36072(TRUE, java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], i1238[9]) → LOAD3637(java.lang.Object(ARRAY(i3[9], a4210data[9])), i615[9], i477[9], o3142[9], NULL)
LOAD3607(java.lang.Object(ARRAY(i3[17], a4210data[17])), i615[17], i477[17], o3142[17], 0, NULL) → STORE3886(java.lang.Object(ARRAY(i3[17], a4210data[17])), i615[17], o3142[17], i477[17], 0)
LOAD2305ARR1(java.lang.Object(ARRAY(i3[1], a2436data[1])), i118[1], java.lang.Object(IntList(o1856[1], i480[1])), i477[1], java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1]))) → COND_LOAD2305ARR1(&&(&&(&&(>(i118[1], 0), <(i118[1], i3[1])), >(i477[1], 0)), >(+(i118[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a2436data[1])), i118[1], java.lang.Object(IntList(o1856[1], i480[1])), i477[1], java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1])))
COND_LOAD2305ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a2436data[2])), i118[2], java.lang.Object(IntList(o1856[2], i480[2])), i477[2], java.lang.Object(java.lang.String(i771[2], i770[2], i772[2], a3255[2]))) → LOAD3607(java.lang.Object(ARRAY(i3[2], a2436data[2])), +(i118[2], 1), i477[2], o1856[2], i771[2], o1856[2])
LOAD3607(java.lang.Object(ARRAY(i3[4], a4210data[4])), i615[4], i477[4], o3142[4], i1238[4], java.lang.Object(IntList(o3274[4], i1311[4]))) → COND_LOAD3607(>(i1238[4], 1), java.lang.Object(ARRAY(i3[4], a4210data[4])), i615[4], i477[4], o3142[4], i1238[4], java.lang.Object(IntList(o3274[4], i1311[4])))
COND_LOAD3607(TRUE, java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], o3142[5], i1238[5], java.lang.Object(IntList(o3274[5], i1311[5]))) → LOAD3607(java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], o3142[5], +(i1238[5], -1), o3274[5])
LOAD3607(java.lang.Object(ARRAY(i3[6], a4210data[6])), i615[6], i477[6], o3142[6], i1238[6], o3141[6]) → COND_LOAD36071(&&(>(i1238[6], 0), <=(i1238[6], 1)), java.lang.Object(ARRAY(i3[6], a4210data[6])), i615[6], i477[6], o3142[6], i1238[6], o3141[6])
LOAD3607(java.lang.Object(ARRAY(i3[8], a4210data[8])), i615[8], i477[8], o3142[8], i1238[8], NULL) → COND_LOAD36072(>(i1238[8], 1), java.lang.Object(ARRAY(i3[8], a4210data[8])), i615[8], i477[8], o3142[8], i1238[8])
LOAD3607(java.lang.Object(ARRAY(i3[14], a4210data[14])), i615[14], i477[14], java.lang.Object(IntList(o3280[14], i1314[14])), i1238[14], java.lang.Object(IntList(o3280[14], i1314[14]))) → COND_LOAD36073(>(i1238[14], 1), java.lang.Object(ARRAY(i3[14], a4210data[14])), i615[14], i477[14], i1238[14], java.lang.Object(IntList(o3280[14], i1314[14])))
COND_LOAD36073(TRUE, java.lang.Object(ARRAY(i3[15], a4210data[15])), i615[15], i477[15], i1238[15], java.lang.Object(IntList(o3280[15], i1314[15]))) → JMP3960'(java.lang.Object(ARRAY(i3[15], a4210data[15])), i615[15], i477[15], java.lang.Object(IntList(o3280[15], i1314[15])), +(i1238[15], -1), o3280[15])
LOAD2305(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0]) → LOAD2305ARR1(java.lang.Object(ARRAY(i3[0], a2436data[0])), i118[0], java.lang.Object(IntList(o1856[0], i480[0])), i477[0], java.lang.Object(java.lang.String(i771[0], i770[0], i772[0], a3255[0])))
LOAD2305ARR1(java.lang.Object(ARRAY(i3[1], a2436data[1])), i118[1], java.lang.Object(IntList(o1856[1], i480[1])), i477[1], java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1]))) → COND_LOAD2305ARR1(&&(&&(&&(>(i118[1], 0), <(i118[1], i3[1])), >(i477[1], 0)), >(+(i118[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a2436data[1])), i118[1], java.lang.Object(IntList(o1856[1], i480[1])), i477[1], java.lang.Object(java.lang.String(i771[1], i770[1], i772[1], a3255[1])))
COND_LOAD2305ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a2436data[2])), i118[2], java.lang.Object(IntList(o1856[2], i480[2])), i477[2], java.lang.Object(java.lang.String(i771[2], i770[2], i772[2], a3255[2]))) → LOAD3607(java.lang.Object(ARRAY(i3[2], a2436data[2])), +(i118[2], 1), i477[2], o1856[2], i771[2], o1856[2])
JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3]) → LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])
LOAD3607(java.lang.Object(ARRAY(i3[4], a4210data[4])), i615[4], i477[4], o3142[4], i1238[4], java.lang.Object(IntList(o3274[4], i1311[4]))) → COND_LOAD3607(>(i1238[4], 1), java.lang.Object(ARRAY(i3[4], a4210data[4])), i615[4], i477[4], o3142[4], i1238[4], java.lang.Object(IntList(o3274[4], i1311[4])))
COND_LOAD3607(TRUE, java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], o3142[5], i1238[5], java.lang.Object(IntList(o3274[5], i1311[5]))) → LOAD3607(java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], o3142[5], +(i1238[5], -1), o3274[5])
LOAD3607(java.lang.Object(ARRAY(i3[6], a4210data[6])), i615[6], i477[6], o3142[6], i1238[6], o3141[6]) → COND_LOAD36071(&&(>(i1238[6], 0), <=(i1238[6], 1)), java.lang.Object(ARRAY(i3[6], a4210data[6])), i615[6], i477[6], o3142[6], i1238[6], o3141[6])
COND_LOAD36071(TRUE, java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], i1238[7], o3141[7]) → LOAD3637(java.lang.Object(ARRAY(i3[7], a4210data[7])), i615[7], i477[7], o3142[7], o3141[7])
LOAD3607(java.lang.Object(ARRAY(i3[8], a4210data[8])), i615[8], i477[8], o3142[8], i1238[8], NULL) → COND_LOAD36072(>(i1238[8], 1), java.lang.Object(ARRAY(i3[8], a4210data[8])), i615[8], i477[8], o3142[8], i1238[8])
STORE3886(java.lang.Object(ARRAY(i3[10], a4210data[10])), i615[10], o3142[10], i477[10], i1289[10]) → LOAD2305(java.lang.Object(ARRAY(i3[10], a4210data[10])), i615[10], o3142[10], i1289[10])
RETURN3818(java.lang.Object(ARRAY(i3[11], a4210data[11])), i615[11], i477[11], o3142[11], i1289[11]) → LOAD2305(java.lang.Object(ARRAY(i3[11], a4210data[11])), i615[11], o3142[11], i1289[11])
LOAD3637(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], i477[12], o3142[12], java.lang.Object(IntList(o3234[12], i1289[12]))) → LOAD2305(java.lang.Object(ARRAY(i3[12], a4210data[12])), i615[12], o3142[12], i1289[12])
LOAD3607(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], i477[13], o3142[13], 0, java.lang.Object(IntList(o3234[13], i1289[13]))) → LOAD2305(java.lang.Object(ARRAY(i3[13], a4210data[13])), i615[13], o3142[13], i1289[13])
LOAD3607(java.lang.Object(ARRAY(i3[14], a4210data[14])), i615[14], i477[14], java.lang.Object(IntList(o3280[14], i1314[14])), i1238[14], java.lang.Object(IntList(o3280[14], i1314[14]))) → COND_LOAD36073(>(i1238[14], 1), java.lang.Object(ARRAY(i3[14], a4210data[14])), i615[14], i477[14], i1238[14], java.lang.Object(IntList(o3280[14], i1314[14])))
COND_LOAD36073(TRUE, java.lang.Object(ARRAY(i3[15], a4210data[15])), i615[15], i477[15], i1238[15], java.lang.Object(IntList(o3280[15], i1314[15]))) → JMP3960'(java.lang.Object(ARRAY(i3[15], a4210data[15])), i615[15], i477[15], java.lang.Object(IntList(o3280[15], i1314[15])), +(i1238[15], -1), o3280[15])
LOAD3637(java.lang.Object(ARRAY(i3[16], a4210data[16])), i615[16], i477[16], o3142[16], NULL) → STORE3886(java.lang.Object(ARRAY(i3[16], a4210data[16])), i615[16], o3142[16], i477[16], 0)
LOAD3637(java.lang.Object(ARRAY(i3[18], a4210data[18])), i615[18], i477[18], java.lang.Object(IntList(o3239[18], i1291[18])), java.lang.Object(IntList(o3239[18], i1291[18]))) → RETURN3818(java.lang.Object(ARRAY(i3[18], a4210data[18])), i615[18], i477[18], java.lang.Object(IntList(o3239[18], i1291[18])), i1291[18])
LOAD3607(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19]))) → RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])
&&(TRUE, TRUE)1 ↔ TRUE1
&&(TRUE, FALSE)1 ↔ FALSE1
&&(FALSE, TRUE)1 ↔ FALSE1
&&(FALSE, FALSE)1 ↔ FALSE1
!= | ~ | 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 |
Boolean, Integer
(10) -> (0), if ((i1289[10] →* i477[0])∧(i615[10] →* i118[0])∧(o3142[10] →* java.lang.Object(IntList(o1856[0], i480[0])))∧((i3[10] →* i3[0])∧(a4210data[10] →* a2436data[0])))
(11) -> (0), if ((i615[11] →* i118[0])∧(i1289[11] →* i477[0])∧(o3142[11] →* java.lang.Object(IntList(o1856[0], i480[0])))∧((i3[11] →* i3[0])∧(a4210data[11] →* a2436data[0])))
(12) -> (0), if ((o3142[12] →* java.lang.Object(IntList(o1856[0], i480[0])))∧(i1289[12] →* i477[0])∧(i615[12] →* i118[0])∧((i3[12] →* i3[0])∧(a4210data[12] →* a2436data[0])))
(13) -> (0), if ((i1289[13] →* i477[0])∧(o3142[13] →* java.lang.Object(IntList(o1856[0], i480[0])))∧(i615[13] →* i118[0])∧((i3[13] →* i3[0])∧(a4210data[13] →* a2436data[0])))
(0) -> (1), if (((o1856[0] →* o1856[1])∧(i480[0] →* i480[1]))∧(i118[0] →* i118[1])∧(i477[0] →* i477[1])∧((i771[0] →* i771[1])∧(i770[0] →* i770[1])∧(i772[0] →* i772[1])∧(a3255[0] →* a3255[1]))∧((i3[0] →* i3[1])∧(a2436data[0] →* a2436data[1])))
(1) -> (2), if ((i118[1] > 0 && i118[1] < i3[1] && i477[1] > 0 && i118[1] + 1 > 0 →* TRUE)∧(i477[1] →* i477[2])∧((o1856[1] →* o1856[2])∧(i480[1] →* i480[2]))∧((i3[1] →* i3[2])∧(a2436data[1] →* a2436data[2]))∧((i771[1] →* i771[2])∧(i770[1] →* i770[2])∧(i772[1] →* i772[2])∧(a3255[1] →* a3255[2]))∧(i118[1] →* i118[2]))
(15) -> (3), if ((i1238[15] + -1 →* i1284[3])∧(i477[15] →* i477[3])∧(i615[15] →* i615[3])∧(java.lang.Object(IntList(o3280[15], i1314[15])) →* o3142[3])∧((i3[15] →* i3[3])∧(a4210data[15] →* a4210data[3]))∧(o3280[15] →* o3274[3]))
(2) -> (4), if ((o1856[2] →* java.lang.Object(IntList(o3274[4], i1311[4])))∧(i118[2] + 1 →* i615[4])∧(i771[2] →* i1238[4])∧((i3[2] →* i3[4])∧(a2436data[2] →* a4210data[4]))∧(i477[2] →* i477[4])∧(o1856[2] →* o3142[4]))
(3) -> (4), if ((i477[3] →* i477[4])∧(o3274[3] →* java.lang.Object(IntList(o3274[4], i1311[4])))∧((i3[3] →* i3[4])∧(a4210data[3] →* a4210data[4]))∧(i615[3] →* i615[4])∧(o3142[3] →* o3142[4])∧(i1284[3] →* i1238[4]))
(5) -> (4), if ((i477[5] →* i477[4])∧(o3142[5] →* o3142[4])∧(o3274[5] →* java.lang.Object(IntList(o3274[4], i1311[4])))∧(i1238[5] + -1 →* i1238[4])∧(i615[5] →* i615[4])∧((i3[5] →* i3[4])∧(a4210data[5] →* a4210data[4])))
(4) -> (5), if ((i477[4] →* i477[5])∧(i1238[4] →* i1238[5])∧((o3274[4] →* o3274[5])∧(i1311[4] →* i1311[5]))∧(o3142[4] →* o3142[5])∧(i615[4] →* i615[5])∧(i1238[4] > 1 →* TRUE)∧((i3[4] →* i3[5])∧(a4210data[4] →* a4210data[5])))
(2) -> (6), if ((o1856[2] →* o3142[6])∧((i3[2] →* i3[6])∧(a2436data[2] →* a4210data[6]))∧(o1856[2] →* o3141[6])∧(i118[2] + 1 →* i615[6])∧(i771[2] →* i1238[6])∧(i477[2] →* i477[6]))
(3) -> (6), if ((i615[3] →* i615[6])∧(i477[3] →* i477[6])∧((i3[3] →* i3[6])∧(a4210data[3] →* a4210data[6]))∧(o3142[3] →* o3142[6])∧(o3274[3] →* o3141[6])∧(i1284[3] →* i1238[6]))
(5) -> (6), if ((i615[5] →* i615[6])∧(i1238[5] + -1 →* i1238[6])∧(o3274[5] →* o3141[6])∧(o3142[5] →* o3142[6])∧(i477[5] →* i477[6])∧((i3[5] →* i3[6])∧(a4210data[5] →* a4210data[6])))
(6) -> (7), if ((i1238[6] > 0 && i1238[6] <= 1 →* TRUE)∧(i1238[6] →* i1238[7])∧((i3[6] →* i3[7])∧(a4210data[6] →* a4210data[7]))∧(o3141[6] →* o3141[7])∧(i477[6] →* i477[7])∧(i615[6] →* i615[7])∧(o3142[6] →* o3142[7]))
(2) -> (8), if ((i771[2] →* i1238[8])∧((i3[2] →* i3[8])∧(a2436data[2] →* a4210data[8]))∧(i477[2] →* i477[8])∧(i118[2] + 1 →* i615[8])∧(o1856[2] →* o3142[8])∧(o1856[2] →* NULL))
(3) -> (8), if ((o3142[3] →* o3142[8])∧((i3[3] →* i3[8])∧(a4210data[3] →* a4210data[8]))∧(i1284[3] →* i1238[8])∧(o3274[3] →* NULL)∧(i477[3] →* i477[8])∧(i615[3] →* i615[8]))
(5) -> (8), if ((o3142[5] →* o3142[8])∧(i615[5] →* i615[8])∧((i3[5] →* i3[8])∧(a4210data[5] →* a4210data[8]))∧(o3274[5] →* NULL)∧(i477[5] →* i477[8])∧(i1238[5] + -1 →* i1238[8]))
(16) -> (10), if ((i615[16] →* i615[10])∧(o3142[16] →* o3142[10])∧((i3[16] →* i3[10])∧(a4210data[16] →* a4210data[10]))∧(0 →* i1289[10])∧(i477[16] →* i477[10]))
(18) -> (11), if ((java.lang.Object(IntList(o3239[18], i1291[18])) →* o3142[11])∧(i615[18] →* i615[11])∧(i477[18] →* i477[11])∧(i1291[18] →* i1289[11])∧((i3[18] →* i3[11])∧(a4210data[18] →* a4210data[11])))
(19) -> (11), if (((i3[19] →* i3[11])∧(a4210data[19] →* a4210data[11]))∧(java.lang.Object(IntList(o3239[19], i1291[19])) →* o3142[11])∧(i1291[19] →* i1289[11])∧(i477[19] →* i477[11])∧(i615[19] →* i615[11]))
(7) -> (12), if ((i615[7] →* i615[12])∧(o3141[7] →* java.lang.Object(IntList(o3234[12], i1289[12])))∧(i477[7] →* i477[12])∧((i3[7] →* i3[12])∧(a4210data[7] →* a4210data[12]))∧(o3142[7] →* o3142[12]))
(2) -> (13), if ((i771[2] →* 0)∧(o1856[2] →* o3142[13])∧(i477[2] →* i477[13])∧((i3[2] →* i3[13])∧(a2436data[2] →* a4210data[13]))∧(o1856[2] →* java.lang.Object(IntList(o3234[13], i1289[13])))∧(i118[2] + 1 →* i615[13]))
(3) -> (13), if ((i477[3] →* i477[13])∧((i3[3] →* i3[13])∧(a4210data[3] →* a4210data[13]))∧(o3274[3] →* java.lang.Object(IntList(o3234[13], i1289[13])))∧(i1284[3] →* 0)∧(i615[3] →* i615[13])∧(o3142[3] →* o3142[13]))
(5) -> (13), if ((i1238[5] + -1 →* 0)∧(i615[5] →* i615[13])∧(o3142[5] →* o3142[13])∧(o3274[5] →* java.lang.Object(IntList(o3234[13], i1289[13])))∧(i477[5] →* i477[13])∧((i3[5] →* i3[13])∧(a4210data[5] →* a4210data[13])))
(2) -> (14), if (((i3[2] →* i3[14])∧(a2436data[2] →* a4210data[14]))∧(i477[2] →* i477[14])∧(o1856[2] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(i771[2] →* i1238[14])∧(i118[2] + 1 →* i615[14]))
(3) -> (14), if ((o3274[3] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧((i3[3] →* i3[14])∧(a4210data[3] →* a4210data[14]))∧(i1284[3] →* i1238[14])∧(o3142[3] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(i477[3] →* i477[14])∧(i615[3] →* i615[14]))
(5) -> (14), if ((i615[5] →* i615[14])∧(i477[5] →* i477[14])∧(o3142[5] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(o3274[5] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(i1238[5] + -1 →* i1238[14])∧((i3[5] →* i3[14])∧(a4210data[5] →* a4210data[14])))
(14) -> (15), if ((i477[14] →* i477[15])∧(i1238[14] →* i1238[15])∧(i1238[14] > 1 →* TRUE)∧((i3[14] →* i3[15])∧(a4210data[14] →* a4210data[15]))∧(i615[14] →* i615[15])∧((o3280[14] →* o3280[15])∧(i1314[14] →* i1314[15])))
(7) -> (16), if ((o3141[7] →* NULL)∧(i615[7] →* i615[16])∧(i477[7] →* i477[16])∧((i3[7] →* i3[16])∧(a4210data[7] →* a4210data[16]))∧(o3142[7] →* o3142[16]))
(7) -> (18), if (((i3[7] →* i3[18])∧(a4210data[7] →* a4210data[18]))∧(o3142[7] →* java.lang.Object(IntList(o3239[18], i1291[18])))∧(i477[7] →* i477[18])∧(o3141[7] →* java.lang.Object(IntList(o3239[18], i1291[18])))∧(i615[7] →* i615[18]))
(2) -> (19), if ((o1856[2] →* java.lang.Object(IntList(o3239[19], i1291[19])))∧(i477[2] →* i477[19])∧(i771[2] →* 0)∧((i3[2] →* i3[19])∧(a2436data[2] →* a4210data[19]))∧(i118[2] + 1 →* i615[19]))
(3) -> (19), if ((o3274[3] →* java.lang.Object(IntList(o3239[19], i1291[19])))∧(i477[3] →* i477[19])∧(i615[3] →* i615[19])∧(i1284[3] →* 0)∧((i3[3] →* i3[19])∧(a4210data[3] →* a4210data[19]))∧(o3142[3] →* java.lang.Object(IntList(o3239[19], i1291[19]))))
(5) -> (19), if ((o3274[5] →* java.lang.Object(IntList(o3239[19], i1291[19])))∧(o3142[5] →* java.lang.Object(IntList(o3239[19], i1291[19])))∧((i3[5] →* i3[19])∧(a4210data[5] →* a4210data[19]))∧(i1238[5] + -1 →* 0)∧(i615[5] →* i615[19])∧(i477[5] →* i477[19]))
!= | ~ | 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 |
Integer, Boolean
(10) -> (0), if ((i1289[10] →* i477[0])∧(i615[10] →* i118[0])∧(o3142[10] →* java.lang.Object(IntList(o1856[0], i480[0])))∧((i3[10] →* i3[0])∧(a4210data[10] →* a2436data[0])))
(11) -> (0), if ((i615[11] →* i118[0])∧(i1289[11] →* i477[0])∧(o3142[11] →* java.lang.Object(IntList(o1856[0], i480[0])))∧((i3[11] →* i3[0])∧(a4210data[11] →* a2436data[0])))
(12) -> (0), if ((o3142[12] →* java.lang.Object(IntList(o1856[0], i480[0])))∧(i1289[12] →* i477[0])∧(i615[12] →* i118[0])∧((i3[12] →* i3[0])∧(a4210data[12] →* a2436data[0])))
(13) -> (0), if ((i1289[13] →* i477[0])∧(o3142[13] →* java.lang.Object(IntList(o1856[0], i480[0])))∧(i615[13] →* i118[0])∧((i3[13] →* i3[0])∧(a4210data[13] →* a2436data[0])))
(0) -> (1), if (((o1856[0] →* o1856[1])∧(i480[0] →* i480[1]))∧(i118[0] →* i118[1])∧(i477[0] →* i477[1])∧((i771[0] →* i771[1])∧(i770[0] →* i770[1])∧(i772[0] →* i772[1])∧(a3255[0] →* a3255[1]))∧((i3[0] →* i3[1])∧(a2436data[0] →* a2436data[1])))
(1) -> (2), if ((i118[1] > 0 && i118[1] < i3[1] && i477[1] > 0 && i118[1] + 1 > 0 →* TRUE)∧(i477[1] →* i477[2])∧((o1856[1] →* o1856[2])∧(i480[1] →* i480[2]))∧((i3[1] →* i3[2])∧(a2436data[1] →* a2436data[2]))∧((i771[1] →* i771[2])∧(i770[1] →* i770[2])∧(i772[1] →* i772[2])∧(a3255[1] →* a3255[2]))∧(i118[1] →* i118[2]))
(15) -> (3), if ((i1238[15] + -1 →* i1284[3])∧(i477[15] →* i477[3])∧(i615[15] →* i615[3])∧(java.lang.Object(IntList(o3280[15], i1314[15])) →* o3142[3])∧((i3[15] →* i3[3])∧(a4210data[15] →* a4210data[3]))∧(o3280[15] →* o3274[3]))
(2) -> (4), if ((o1856[2] →* java.lang.Object(IntList(o3274[4], i1311[4])))∧(i118[2] + 1 →* i615[4])∧(i771[2] →* i1238[4])∧((i3[2] →* i3[4])∧(a2436data[2] →* a4210data[4]))∧(i477[2] →* i477[4])∧(o1856[2] →* o3142[4]))
(3) -> (4), if ((i477[3] →* i477[4])∧(o3274[3] →* java.lang.Object(IntList(o3274[4], i1311[4])))∧((i3[3] →* i3[4])∧(a4210data[3] →* a4210data[4]))∧(i615[3] →* i615[4])∧(o3142[3] →* o3142[4])∧(i1284[3] →* i1238[4]))
(5) -> (4), if ((i477[5] →* i477[4])∧(o3142[5] →* o3142[4])∧(o3274[5] →* java.lang.Object(IntList(o3274[4], i1311[4])))∧(i1238[5] + -1 →* i1238[4])∧(i615[5] →* i615[4])∧((i3[5] →* i3[4])∧(a4210data[5] →* a4210data[4])))
(4) -> (5), if ((i477[4] →* i477[5])∧(i1238[4] →* i1238[5])∧((o3274[4] →* o3274[5])∧(i1311[4] →* i1311[5]))∧(o3142[4] →* o3142[5])∧(i615[4] →* i615[5])∧(i1238[4] > 1 →* TRUE)∧((i3[4] →* i3[5])∧(a4210data[4] →* a4210data[5])))
(2) -> (6), if ((o1856[2] →* o3142[6])∧((i3[2] →* i3[6])∧(a2436data[2] →* a4210data[6]))∧(o1856[2] →* o3141[6])∧(i118[2] + 1 →* i615[6])∧(i771[2] →* i1238[6])∧(i477[2] →* i477[6]))
(3) -> (6), if ((i615[3] →* i615[6])∧(i477[3] →* i477[6])∧((i3[3] →* i3[6])∧(a4210data[3] →* a4210data[6]))∧(o3142[3] →* o3142[6])∧(o3274[3] →* o3141[6])∧(i1284[3] →* i1238[6]))
(5) -> (6), if ((i615[5] →* i615[6])∧(i1238[5] + -1 →* i1238[6])∧(o3274[5] →* o3141[6])∧(o3142[5] →* o3142[6])∧(i477[5] →* i477[6])∧((i3[5] →* i3[6])∧(a4210data[5] →* a4210data[6])))
(6) -> (7), if ((i1238[6] > 0 && i1238[6] <= 1 →* TRUE)∧(i1238[6] →* i1238[7])∧((i3[6] →* i3[7])∧(a4210data[6] →* a4210data[7]))∧(o3141[6] →* o3141[7])∧(i477[6] →* i477[7])∧(i615[6] →* i615[7])∧(o3142[6] →* o3142[7]))
(16) -> (10), if ((i615[16] →* i615[10])∧(o3142[16] →* o3142[10])∧((i3[16] →* i3[10])∧(a4210data[16] →* a4210data[10]))∧(0 →* i1289[10])∧(i477[16] →* i477[10]))
(18) -> (11), if ((java.lang.Object(IntList(o3239[18], i1291[18])) →* o3142[11])∧(i615[18] →* i615[11])∧(i477[18] →* i477[11])∧(i1291[18] →* i1289[11])∧((i3[18] →* i3[11])∧(a4210data[18] →* a4210data[11])))
(19) -> (11), if (((i3[19] →* i3[11])∧(a4210data[19] →* a4210data[11]))∧(java.lang.Object(IntList(o3239[19], i1291[19])) →* o3142[11])∧(i1291[19] →* i1289[11])∧(i477[19] →* i477[11])∧(i615[19] →* i615[11]))
(7) -> (12), if ((i615[7] →* i615[12])∧(o3141[7] →* java.lang.Object(IntList(o3234[12], i1289[12])))∧(i477[7] →* i477[12])∧((i3[7] →* i3[12])∧(a4210data[7] →* a4210data[12]))∧(o3142[7] →* o3142[12]))
(2) -> (13), if ((i771[2] →* 0)∧(o1856[2] →* o3142[13])∧(i477[2] →* i477[13])∧((i3[2] →* i3[13])∧(a2436data[2] →* a4210data[13]))∧(o1856[2] →* java.lang.Object(IntList(o3234[13], i1289[13])))∧(i118[2] + 1 →* i615[13]))
(3) -> (13), if ((i477[3] →* i477[13])∧((i3[3] →* i3[13])∧(a4210data[3] →* a4210data[13]))∧(o3274[3] →* java.lang.Object(IntList(o3234[13], i1289[13])))∧(i1284[3] →* 0)∧(i615[3] →* i615[13])∧(o3142[3] →* o3142[13]))
(5) -> (13), if ((i1238[5] + -1 →* 0)∧(i615[5] →* i615[13])∧(o3142[5] →* o3142[13])∧(o3274[5] →* java.lang.Object(IntList(o3234[13], i1289[13])))∧(i477[5] →* i477[13])∧((i3[5] →* i3[13])∧(a4210data[5] →* a4210data[13])))
(2) -> (14), if (((i3[2] →* i3[14])∧(a2436data[2] →* a4210data[14]))∧(i477[2] →* i477[14])∧(o1856[2] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(i771[2] →* i1238[14])∧(i118[2] + 1 →* i615[14]))
(3) -> (14), if ((o3274[3] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧((i3[3] →* i3[14])∧(a4210data[3] →* a4210data[14]))∧(i1284[3] →* i1238[14])∧(o3142[3] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(i477[3] →* i477[14])∧(i615[3] →* i615[14]))
(5) -> (14), if ((i615[5] →* i615[14])∧(i477[5] →* i477[14])∧(o3142[5] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(o3274[5] →* java.lang.Object(IntList(o3280[14], i1314[14])))∧(i1238[5] + -1 →* i1238[14])∧((i3[5] →* i3[14])∧(a4210data[5] →* a4210data[14])))
(14) -> (15), if ((i477[14] →* i477[15])∧(i1238[14] →* i1238[15])∧(i1238[14] > 1 →* TRUE)∧((i3[14] →* i3[15])∧(a4210data[14] →* a4210data[15]))∧(i615[14] →* i615[15])∧((o3280[14] →* o3280[15])∧(i1314[14] →* i1314[15])))
(7) -> (16), if ((o3141[7] →* NULL)∧(i615[7] →* i615[16])∧(i477[7] →* i477[16])∧((i3[7] →* i3[16])∧(a4210data[7] →* a4210data[16]))∧(o3142[7] →* o3142[16]))
(7) -> (18), if (((i3[7] →* i3[18])∧(a4210data[7] →* a4210data[18]))∧(o3142[7] →* java.lang.Object(IntList(o3239[18], i1291[18])))∧(i477[7] →* i477[18])∧(o3141[7] →* java.lang.Object(IntList(o3239[18], i1291[18])))∧(i615[7] →* i615[18]))
(2) -> (19), if ((o1856[2] →* java.lang.Object(IntList(o3239[19], i1291[19])))∧(i477[2] →* i477[19])∧(i771[2] →* 0)∧((i3[2] →* i3[19])∧(a2436data[2] →* a4210data[19]))∧(i118[2] + 1 →* i615[19]))
(3) -> (19), if ((o3274[3] →* java.lang.Object(IntList(o3239[19], i1291[19])))∧(i477[3] →* i477[19])∧(i615[3] →* i615[19])∧(i1284[3] →* 0)∧((i3[3] →* i3[19])∧(a4210data[3] →* a4210data[19]))∧(o3142[3] →* java.lang.Object(IntList(o3239[19], i1291[19]))))
(5) -> (19), if ((o3274[5] →* java.lang.Object(IntList(o3239[19], i1291[19])))∧(o3142[5] →* java.lang.Object(IntList(o3239[19], i1291[19])))∧((i3[5] →* i3[19])∧(a4210data[5] →* a4210data[19]))∧(i1238[5] + -1 →* 0)∧(i615[5] →* i615[19])∧(i477[5] →* i477[19]))
(1) (o1856[2]=java.lang.Object(IntList(o3239[19], i1291[19]))∧i477[2]=i477[19]∧i771[2]=0∧i3[2]=i3[19]∧a2436data[2]=a4210data[19]∧+(i118[2], 1)=i615[19]∧i3[19]=i3[11]∧a4210data[19]=a4210data[11]∧java.lang.Object(IntList(o3239[19], i1291[19]))=o3142[11]∧i1291[19]=i1289[11]∧i477[19]=i477[11]∧i615[19]=i615[11] ⇒ LOAD3607(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])∧(UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥))
(2) (LOAD3607(java.lang.Object(ARRAY(i3[2], a2436data[2])), +(i118[2], 1), i477[2], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[2], a2436data[2])), +(i118[2], 1), i477[2], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥RETURN3818(java.lang.Object(ARRAY(i3[2], a2436data[2])), +(i118[2], 1), i477[2], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])∧(UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥))
(3) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧[1 + (-1)bso_89] + [2]i1291[19] + [2]o3239[19] ≥ 0)
(4) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧[1 + (-1)bso_89] + [2]i1291[19] + [2]o3239[19] ≥ 0)
(5) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧[1 + (-1)bso_89] + [2]i1291[19] + [2]o3239[19] ≥ 0)
(6) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_89] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
(7) (o3274[3]=java.lang.Object(IntList(o3239[19], i1291[19]))∧i477[3]=i477[19]∧i615[3]=i615[19]∧i1284[3]=0∧i3[3]=i3[19]∧a4210data[3]=a4210data[19]∧o3142[3]=java.lang.Object(IntList(o3239[19], i1291[19]))∧i3[19]=i3[11]∧a4210data[19]=a4210data[11]∧java.lang.Object(IntList(o3239[19], i1291[19]))=o3142[11]∧i1291[19]=i1289[11]∧i477[19]=i477[11]∧i615[19]=i615[11] ⇒ LOAD3607(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])∧(UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥))
(8) (LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥RETURN3818(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])∧(UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥))
(9) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧[1 + (-1)bso_89] + [2]i1291[19] + [2]o3239[19] ≥ 0)
(10) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧[1 + (-1)bso_89] + [2]i1291[19] + [2]o3239[19] ≥ 0)
(11) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧[1 + (-1)bso_89] + [2]i1291[19] + [2]o3239[19] ≥ 0)
(12) ((UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_89] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
(13) (o3274[5]=java.lang.Object(IntList(o3239[19], i1291[19]))∧o3142[5]=java.lang.Object(IntList(o3239[19], i1291[19]))∧i3[5]=i3[19]∧a4210data[5]=a4210data[19]∧+(i1238[5], -1)=0∧i615[5]=i615[19]∧i477[5]=i477[19]∧i3[19]=i3[11]∧a4210data[19]=a4210data[11]∧java.lang.Object(IntList(o3239[19], i1291[19]))=o3142[11]∧i1291[19]=i1289[11]∧i477[19]=i477[11]∧i615[19]=i615[11] ⇒ LOAD3607(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])∧(UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥))
(14) (+(i1238[5], -1)=0 ⇒ LOAD3607(java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥NonInfC∧LOAD3607(java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥RETURN3818(java.lang.Object(ARRAY(i3[5], a4210data[5])), i615[5], i477[5], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])∧(UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥))
(15) (0 ≥ 0 ⇒ (UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧0 ≥ 0∧[1 + (-1)bso_89] + [2]i1291[19] + [2]o3239[19] ≥ 0)
(16) (0 ≥ 0 ⇒ (UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧0 ≥ 0∧[1 + (-1)bso_89] + [2]i1291[19] + [2]o3239[19] ≥ 0)
(17) (0 ≥ 0 ⇒ (UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧0 ≥ 0∧[1 + (-1)bso_89] + [2]i1291[19] + [2]o3239[19] ≥ 0)
(18) (0 ≥ 0 ⇒ (UIncreasing(RETURN3818(java.lang.Object(ARRAY(i3[19], a4210data[19])), i615[19], i477[19], java.lang.Object(IntList(o3239[19], i1291[19])), i1291[19])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_89] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
(19) (i477[3]=i477[4]∧o3274[3]=java.lang.Object(IntList(o3274[4], i1311[4]))∧i3[3]=i3[4]∧a4210data[3]=a4210data[4]∧i615[3]=i615[4]∧o3142[3]=o3142[4]∧i1284[3]=i1238[4] ⇒ JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(20) (JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], java.lang.Object(IntList(o3274[4], i1311[4])))≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], java.lang.Object(IntList(o3274[4], i1311[4])))≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], java.lang.Object(IntList(o3274[4], i1311[4])))∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(21) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_91] ≥ 0)
(22) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_91] ≥ 0)
(23) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_91] ≥ 0)
(24) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_91] ≥ 0)
(25) (i615[3]=i615[6]∧i477[3]=i477[6]∧i3[3]=i3[6]∧a4210data[3]=a4210data[6]∧o3142[3]=o3142[6]∧o3274[3]=o3141[6]∧i1284[3]=i1238[6] ⇒ JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(26) (JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(27) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_91] ≥ 0)
(28) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_91] ≥ 0)
(29) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_91] ≥ 0)
(30) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_91] ≥ 0)
(31) (i477[3]=i477[13]∧i3[3]=i3[13]∧a4210data[3]=a4210data[13]∧o3274[3]=java.lang.Object(IntList(o3234[13], i1289[13]))∧i1284[3]=0∧i615[3]=i615[13]∧o3142[3]=o3142[13] ⇒ JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(32) (JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], 0, java.lang.Object(IntList(o3234[13], i1289[13])))≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], 0, java.lang.Object(IntList(o3234[13], i1289[13])))≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], 0, java.lang.Object(IntList(o3234[13], i1289[13])))∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(33) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_91] ≥ 0)
(34) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_91] ≥ 0)
(35) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_91] ≥ 0)
(36) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_91] ≥ 0)
(37) (o3274[3]=java.lang.Object(IntList(o3280[14], i1314[14]))∧i3[3]=i3[14]∧a4210data[3]=a4210data[14]∧i1284[3]=i1238[14]∧o3142[3]=java.lang.Object(IntList(o3280[14], i1314[14]))∧i477[3]=i477[14]∧i615[3]=i615[14] ⇒ JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(38) (JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], java.lang.Object(IntList(o3280[14], i1314[14])), i1284[3], java.lang.Object(IntList(o3280[14], i1314[14])))≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], java.lang.Object(IntList(o3280[14], i1314[14])), i1284[3], java.lang.Object(IntList(o3280[14], i1314[14])))≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], java.lang.Object(IntList(o3280[14], i1314[14])), i1284[3], java.lang.Object(IntList(o3280[14], i1314[14])))∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(39) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_91] ≥ 0)
(40) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_91] ≥ 0)
(41) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧[(-1)bso_91] ≥ 0)
(42) ((UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_91] ≥ 0)
(43) (o3274[3]=java.lang.Object(IntList(o3239[19], i1291[19]))∧i477[3]=i477[19]∧i615[3]=i615[19]∧i1284[3]=0∧i3[3]=i3[19]∧a4210data[3]=a4210data[19]∧o3142[3]=java.lang.Object(IntList(o3239[19], i1291[19])) ⇒ JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])∧(UIncreasing(LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], o3142[3], i1284[3], o3274[3])), ≥))
(44) (JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥NonInfC∧JMP3960'(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.Object(IntList(o3239[19], i1291[19])))≥LOAD3607(java.lang.Object(ARRAY(i3[3], a4210data[3])), i615[3], i477[3], java.lang.Object(IntList(o3239[19], i1291[19])), 0, java.lang.