// This file is part of the SV-Benchmarks collection of verification tasks:
// https://github.com/sosy-lab/sv-benchmarks
//
// SPDX-FileCopyrightText: 2016 Gilles Audemard
// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
// SPDX-FileCopyrightText: 2020 The SV-Benchmarks Community
//
// SPDX-License-Identifier: MIT

extern void abort(void) __attribute__((__nothrow__, __leaf__))
__attribute__((__noreturn__));
extern void __assert_fail(const char *, const char *, unsigned int,
                          const char *) __attribute__((__nothrow__, __leaf__))
__attribute__((__noreturn__));
int __VERIFIER_nondet_int();
void reach_error() { __assert_fail("0", "Haystacks-09.c", 5, "reach_error"); }
void assume(int cond) {
  if (!cond)
    abort();
}
int main() {
  int cond0;
  int dummy = 0;
  int N;
  int var0;
  var0 = __VERIFIER_nondet_int();
  assume(var0 >= 0);
  assume(var0 <= 8);
  int var1;
  var1 = __VERIFIER_nondet_int();
  assume(var1 >= 0);
  assume(var1 <= 8);
  int var2;
  var2 = __VERIFIER_nondet_int();
  assume(var2 >= 0);
  assume(var2 <= 8);
  int var3;
  var3 = __VERIFIER_nondet_int();
  assume(var3 >= 0);
  assume(var3 <= 8);
  int var4;
  var4 = __VERIFIER_nondet_int();
  assume(var4 >= 0);
  assume(var4 <= 8);
  int var5;
  var5 = __VERIFIER_nondet_int();
  assume(var5 >= 0);
  assume(var5 <= 8);
  int var6;
  var6 = __VERIFIER_nondet_int();
  assume(var6 >= 0);
  assume(var6 <= 8);
  int var7;
  var7 = __VERIFIER_nondet_int();
  assume(var7 >= 0);
  assume(var7 <= 8);
  int var8;
  var8 = __VERIFIER_nondet_int();
  assume(var8 >= 0);
  assume(var8 <= 8);
  int var9;
  var9 = __VERIFIER_nondet_int();
  assume(var9 >= 0);
  assume(var9 <= 8);
  int var10;
  var10 = __VERIFIER_nondet_int();
  assume(var10 >= 0);
  assume(var10 <= 8);
  int var11;
  var11 = __VERIFIER_nondet_int();
  assume(var11 >= 0);
  assume(var11 <= 8);
  int var12;
  var12 = __VERIFIER_nondet_int();
  assume(var12 >= 0);
  assume(var12 <= 8);
  int var13;
  var13 = __VERIFIER_nondet_int();
  assume(var13 >= 0);
  assume(var13 <= 8);
  int var14;
  var14 = __VERIFIER_nondet_int();
  assume(var14 >= 0);
  assume(var14 <= 8);
  int var15;
  var15 = __VERIFIER_nondet_int();
  assume(var15 >= 0);
  assume(var15 <= 8);
  int var16;
  var16 = __VERIFIER_nondet_int();
  assume(var16 >= 0);
  assume(var16 <= 8);
  int var17;
  var17 = __VERIFIER_nondet_int();
  assume(var17 >= 0);
  assume(var17 <= 8);
  int var18;
  var18 = __VERIFIER_nondet_int();
  assume(var18 >= 0);
  assume(var18 <= 8);
  int var19;
  var19 = __VERIFIER_nondet_int();
  assume(var19 >= 0);
  assume(var19 <= 8);
  int var20;
  var20 = __VERIFIER_nondet_int();
  assume(var20 >= 0);
  assume(var20 <= 8);
  int var21;
  var21 = __VERIFIER_nondet_int();
  assume(var21 >= 0);
  assume(var21 <= 8);
  int var22;
  var22 = __VERIFIER_nondet_int();
  assume(var22 >= 0);
  assume(var22 <= 8);
  int var23;
  var23 = __VERIFIER_nondet_int();
  assume(var23 >= 0);
  assume(var23 <= 8);
  int var24;
  var24 = __VERIFIER_nondet_int();
  assume(var24 >= 0);
  assume(var24 <= 8);
  int var25;
  var25 = __VERIFIER_nondet_int();
  assume(var25 >= 0);
  assume(var25 <= 8);
  int var26;
  var26 = __VERIFIER_nondet_int();
  assume(var26 >= 0);
  assume(var26 <= 8);
  int var27;
  var27 = __VERIFIER_nondet_int();
  assume(var27 >= 0);
  assume(var27 <= 8);
  int var28;
  var28 = __VERIFIER_nondet_int();
  assume(var28 >= 0);
  assume(var28 <= 8);
  int var29;
  var29 = __VERIFIER_nondet_int();
  assume(var29 >= 0);
  assume(var29 <= 8);
  int var30;
  var30 = __VERIFIER_nondet_int();
  assume(var30 >= 0);
  assume(var30 <= 8);
  int var31;
  var31 = __VERIFIER_nondet_int();
  assume(var31 >= 0);
  assume(var31 <= 8);
  int var32;
  var32 = __VERIFIER_nondet_int();
  assume(var32 >= 0);
  assume(var32 <= 8);
  int var33;
  var33 = __VERIFIER_nondet_int();
  assume(var33 >= 0);
  assume(var33 <= 8);
  int var34;
  var34 = __VERIFIER_nondet_int();
  assume(var34 >= 0);
  assume(var34 <= 8);
  int var35;
  var35 = __VERIFIER_nondet_int();
  assume(var35 >= 0);
  assume(var35 <= 8);
  int var36;
  var36 = __VERIFIER_nondet_int();
  assume(var36 >= 0);
  assume(var36 <= 8);
  int var37;
  var37 = __VERIFIER_nondet_int();
  assume(var37 >= 0);
  assume(var37 <= 8);
  int var38;
  var38 = __VERIFIER_nondet_int();
  assume(var38 >= 0);
  assume(var38 <= 8);
  int var39;
  var39 = __VERIFIER_nondet_int();
  assume(var39 >= 0);
  assume(var39 <= 8);
  int var40;
  var40 = __VERIFIER_nondet_int();
  assume(var40 >= 0);
  assume(var40 <= 8);
  int var41;
  var41 = __VERIFIER_nondet_int();
  assume(var41 >= 0);
  assume(var41 <= 8);
  int var42;
  var42 = __VERIFIER_nondet_int();
  assume(var42 >= 0);
  assume(var42 <= 8);
  int var43;
  var43 = __VERIFIER_nondet_int();
  assume(var43 >= 0);
  assume(var43 <= 8);
  int var44;
  var44 = __VERIFIER_nondet_int();
  assume(var44 >= 0);
  assume(var44 <= 8);
  int var45;
  var45 = __VERIFIER_nondet_int();
  assume(var45 >= 0);
  assume(var45 <= 8);
  int var46;
  var46 = __VERIFIER_nondet_int();
  assume(var46 >= 0);
  assume(var46 <= 8);
  int var47;
  var47 = __VERIFIER_nondet_int();
  assume(var47 >= 0);
  assume(var47 <= 8);
  int var48;
  var48 = __VERIFIER_nondet_int();
  assume(var48 >= 0);
  assume(var48 <= 8);
  int var49;
  var49 = __VERIFIER_nondet_int();
  assume(var49 >= 0);
  assume(var49 <= 8);
  int var50;
  var50 = __VERIFIER_nondet_int();
  assume(var50 >= 0);
  assume(var50 <= 8);
  int var51;
  var51 = __VERIFIER_nondet_int();
  assume(var51 >= 0);
  assume(var51 <= 8);
  int var52;
  var52 = __VERIFIER_nondet_int();
  assume(var52 >= 0);
  assume(var52 <= 8);
  int var53;
  var53 = __VERIFIER_nondet_int();
  assume(var53 >= 0);
  assume(var53 <= 8);
  int var54;
  var54 = __VERIFIER_nondet_int();
  assume(var54 >= 0);
  assume(var54 <= 8);
  int var55;
  var55 = __VERIFIER_nondet_int();
  assume(var55 >= 0);
  assume(var55 <= 8);
  int var56;
  var56 = __VERIFIER_nondet_int();
  assume(var56 >= 0);
  assume(var56 <= 8);
  int var57;
  var57 = __VERIFIER_nondet_int();
  assume(var57 >= 0);
  assume(var57 <= 8);
  int var58;
  var58 = __VERIFIER_nondet_int();
  assume(var58 >= 0);
  assume(var58 <= 8);
  int var59;
  var59 = __VERIFIER_nondet_int();
  assume(var59 >= 0);
  assume(var59 <= 8);
  int var60;
  var60 = __VERIFIER_nondet_int();
  assume(var60 >= 0);
  assume(var60 <= 8);
  int var61;
  var61 = __VERIFIER_nondet_int();
  assume(var61 >= 0);
  assume(var61 <= 8);
  int var62;
  var62 = __VERIFIER_nondet_int();
  assume(var62 >= 0);
  assume(var62 <= 8);
  int var63;
  var63 = __VERIFIER_nondet_int();
  assume(var63 >= 0);
  assume(var63 <= 8);
  int var64;
  var64 = __VERIFIER_nondet_int();
  assume(var64 >= 0);
  assume(var64 <= 8);
  int var65;
  var65 = __VERIFIER_nondet_int();
  assume(var65 >= 0);
  assume(var65 <= 8);
  int var66;
  var66 = __VERIFIER_nondet_int();
  assume(var66 >= 0);
  assume(var66 <= 8);
  int var67;
  var67 = __VERIFIER_nondet_int();
  assume(var67 >= 0);
  assume(var67 <= 8);
  int var68;
  var68 = __VERIFIER_nondet_int();
  assume(var68 >= 0);
  assume(var68 <= 8);
  int var69;
  var69 = __VERIFIER_nondet_int();
  assume(var69 >= 0);
  assume(var69 <= 8);
  int var70;
  var70 = __VERIFIER_nondet_int();
  assume(var70 >= 0);
  assume(var70 <= 8);
  int var71;
  var71 = __VERIFIER_nondet_int();
  assume(var71 >= 0);
  assume(var71 <= 8);
  int var72;
  var72 = __VERIFIER_nondet_int();
  assume(var72 >= 0);
  assume(var72 <= 8);
  int var73;
  var73 = __VERIFIER_nondet_int();
  assume(var73 >= 0);
  assume(var73 <= 8);
  int var74;
  var74 = __VERIFIER_nondet_int();
  assume(var74 >= 0);
  assume(var74 <= 8);
  int var75;
  var75 = __VERIFIER_nondet_int();
  assume(var75 >= 0);
  assume(var75 <= 8);
  int var76;
  var76 = __VERIFIER_nondet_int();
  assume(var76 >= 0);
  assume(var76 <= 8);
  int var77;
  var77 = __VERIFIER_nondet_int();
  assume(var77 >= 0);
  assume(var77 <= 8);
  int var78;
  var78 = __VERIFIER_nondet_int();
  assume(var78 >= 0);
  assume(var78 <= 8);
  int var79;
  var79 = __VERIFIER_nondet_int();
  assume(var79 >= 0);
  assume(var79 <= 8);
  int var80;
  var80 = __VERIFIER_nondet_int();
  assume(var80 >= 0);
  assume(var80 <= 8);
  int myvar0 = 1;
  assume(var0 != var10);
  assume(var11 != var30);
  assume(var11 != var43);
  assume(var11 != var57);
  assume(var11 != var9);
  assume(var12 != var15);
  assume(var12 != var29);
  assume(var12 != var67);
  assume(var17 != var7);
  assume(var18 != var16);
  assume(var2 != var14);
  assume(var2 != var45);
  assume(var2 != var78);
  assume(var22 != var0);
  assume(var22 != var10);
  assume(var22 != var29);
  assume(var22 != var58);
  assume(var22 != var67);
  assume(var23 != var33);
  assume(var23 != var73);
  assume(var23 != var80);
  assume(var24 != var65);
  assume(var24 != var76);
  assume(var25 != var20);
  assume(var28 != var36);
  assume(var28 != var53);
  assume(var28 != var70);
  assume(var29 != var10);
  assume(var3 != var18);
  assume(var31 != var11);
  assume(var31 != var26);
  assume(var31 != var57);
  assume(var31 != var9);
  assume(var32 != var27);
  assume(var32 != var54);
  assume(var32 != var61);
  assume(var32 != var7);
  assume(var34 != var14);
  assume(var35 != var3);
  assume(var35 != var51);
  assume(var35 != var63);
  assume(var36 != var53);
  assume(var37 != var14);
  assume(var37 != var34);
  assume(var37 != var45);
  assume(var37 != var49);
  assume(var37 != var69);
  assume(var37 != var78);
  assume(var38 != var25);
  assume(var38 != var39);
  assume(var39 != var20);
  assume(var4 != var33);
  assume(var40 != var20);
  assume(var40 != var79);
  assume(var42 != var65);
  assume(var43 != var26);
  assume(var43 != var57);
  assume(var43 != var9);
  assume(var45 != var14);
  assume(var45 != var34);
  assume(var45 != var49);
  assume(var45 != var78);
  assume(var46 != var43);
  assume(var46 != var57);
  assume(var47 != var20);
  assume(var47 != var39);
  assume(var48 != var17);
  assume(var48 != var27);
  assume(var48 != var32);
  assume(var48 != var54);
  assume(var48 != var61);
  assume(var48 != var7);
  assume(var49 != var14);
  assume(var50 != var53);
  assume(var50 != var75);
  assume(var51 != var16);
  assume(var51 != var63);
  assume(var52 != var27);
  assume(var52 != var32);
  assume(var52 != var48);
  assume(var52 != var54);
  assume(var52 != var7);
  assume(var54 != var17);
  assume(var56 != var44);
  assume(var57 != var26);
  assume(var57 != var9);
  assume(var58 != var0);
  assume(var58 != var10);
  assume(var59 != var36);
  assume(var59 != var74);
  assume(var59 != var75);
  assume(var6 != var20);
  assume(var6 != var39);
  assume(var6 != var40);
  assume(var60 != var16);
  assume(var60 != var3);
  assume(var60 != var51);
  assume(var61 != var17);
  assume(var61 != var27);
  assume(var62 != var55);
  assume(var63 != var16);
  assume(var64 != var55);
  assume(var68 != var16);
  assume(var69 != var14);
  assume(var69 != var34);
  assume(var69 != var78);
  assume(var7 != var27);
  assume(var73 != var33);
  assume(var73 != var56);
  assume(var73 != var80);
  assume(var74 != var28);
  assume(var74 != var70);
  assume(var75 != var36);
  assume(var76 != var42);
  assume(var76 != var55);
  assume(var76 != var65);
  assume(var77 != var65);
  assume(var78 != var49);
  assume(var79 != var20);
  assume(var79 != var39);
  assume(var80 != var33);
  assume(var80 != var4);
  assume(var80 != var44);
  assume(var80 != var56);
  assume(0 > (var0 - var15) * (var15 - var0));
  assume(0 > (var11 - var26) * (var26 - var11));
  assume(0 > (var12 - var0) * (var0 - var12));
  assume(0 > (var12 - var10) * (var10 - var12));
  assume(0 > (var12 - var58) * (var58 - var12));
  assume(0 > (var15 - var10) * (var10 - var15));
  assume(0 > (var17 - var27) * (var27 - var17));
  assume(0 > (var2 - var34) * (var34 - var2));
  assume(0 > (var2 - var49) * (var49 - var2));
  assume(0 > (var22 - var12) * (var12 - var22));
  assume(0 > (var22 - var15) * (var15 - var22));
  assume(0 > (var23 - var21) * (var21 - var23));
  assume(0 > (var23 - var4) * (var4 - var23));
  assume(0 > (var23 - var44) * (var44 - var23));
  assume(0 > (var23 - var56) * (var56 - var23));
  assume(0 > (var24 - var42) * (var42 - var24));
  assume(0 > (var24 - var55) * (var55 - var24));
  assume(0 > (var25 - var39) * (var39 - var25));
  assume(0 > (var25 - var8) * (var8 - var25));
  assume(0 > (var29 - var0) * (var0 - var29));
  assume(0 > (var29 - var15) * (var15 - var29));
  assume(0 > (var29 - var58) * (var58 - var29));
  assume(0 > (var3 - var16) * (var16 - var3));
  assume(0 > (var3 - var63) * (var63 - var3));
  assume(0 > (var30 - var26) * (var26 - var30));
  assume(0 > (var31 - var30) * (var30 - var31));
  assume(0 > (var31 - var43) * (var43 - var31));
  assume(0 > (var32 - var17) * (var17 - var32));
  assume(0 > (var33 - var21) * (var21 - var33));
  assume(0 > (var34 - var49) * (var49 - var34));
  assume(0 > (var34 - var78) * (var78 - var34));
  assume(0 > (var35 - var16) * (var16 - var35));
  assume(0 > (var35 - var18) * (var18 - var35));
  assume(0 > (var35 - var60) * (var60 - var35));
  assume(0 > (var35 - var68) * (var68 - var35));
  assume(0 > (var37 - var2) * (var2 - var37));
  assume(0 > (var38 - var20) * (var20 - var38));
  assume(0 > (var38 - var8) * (var8 - var38));
  assume(0 > (var4 - var21) * (var21 - var4));
  assume(0 > (var4 - var44) * (var44 - var4));
  assume(0 > (var4 - var56) * (var56 - var4));
  assume(0 > (var40 - var25) * (var25 - var40));
  assume(0 > (var40 - var38) * (var38 - var40));
  assume(0 > (var40 - var39) * (var39 - var40));
  assume(0 > (var40 - var47) * (var47 - var40));
  assume(0 > (var40 - var8) * (var8 - var40));
  assume(0 > (var42 - var55) * (var55 - var42));
  assume(0 > (var43 - var30) * (var30 - var43));
  assume(0 > (var44 - var21) * (var21 - var44));
  assume(0 > (var44 - var33) * (var33 - var44));
  assume(0 > (var46 - var11) * (var11 - var46));
  assume(0 > (var46 - var26) * (var26 - var46));
  assume(0 > (var46 - var30) * (var30 - var46));
  assume(0 > (var46 - var31) * (var31 - var46));
  assume(0 > (var46 - var9) * (var9 - var46));
  assume(0 > (var47 - var25) * (var25 - var47));
  assume(0 > (var47 - var38) * (var38 - var47));
  assume(0 > (var47 - var79) * (var79 - var47));
  assume(0 > (var47 - var8) * (var8 - var47));
  assume(0 > (var50 - var28) * (var28 - var50));
  assume(0 > (var50 - var36) * (var36 - var50));
  assume(0 > (var50 - var59) * (var59 - var50));
  assume(0 > (var50 - var70) * (var70 - var50));
  assume(0 > (var50 - var74) * (var74 - var50));
  assume(0 > (var51 - var18) * (var18 - var51));
  assume(0 > (var51 - var3) * (var3 - var51));
  assume(0 > (var52 - var17) * (var17 - var52));
  assume(0 > (var52 - var61) * (var61 - var52));
  assume(0 > (var54 - var27) * (var27 - var54));
  assume(0 > (var54 - var7) * (var7 - var54));
  assume(0 > (var55 - var65) * (var65 - var55));
  assume(0 > (var56 - var21) * (var21 - var56));
  assume(0 > (var56 - var33) * (var33 - var56));
  assume(0 > (var57 - var30) * (var30 - var57));
  assume(0 > (var58 - var15) * (var15 - var58));
  assume(0 > (var59 - var28) * (var28 - var59));
  assume(0 > (var59 - var53) * (var53 - var59));
  assume(0 > (var59 - var70) * (var70 - var59));
  assume(0 > (var6 - var25) * (var25 - var6));
  assume(0 > (var6 - var38) * (var38 - var6));
  assume(0 > (var6 - var47) * (var47 - var6));
  assume(0 > (var6 - var79) * (var79 - var6));
  assume(0 > (var6 - var8) * (var8 - var6));
  assume(0 > (var60 - var18) * (var18 - var60));
  assume(0 > (var60 - var63) * (var63 - var60));
  assume(0 > (var61 - var54) * (var54 - var61));
  assume(0 > (var61 - var7) * (var7 - var61));
  assume(0 > (var62 - var24) * (var24 - var62));
  assume(0 > (var62 - var42) * (var42 - var62));
  assume(0 > (var62 - var64) * (var64 - var62));
  assume(0 > (var62 - var65) * (var65 - var62));
  assume(0 > (var62 - var76) * (var76 - var62));
  assume(0 > (var62 - var77) * (var77 - var62));
  assume(0 > (var63 - var18) * (var18 - var63));
  assume(0 > (var64 - var24) * (var24 - var64));
  assume(0 > (var64 - var42) * (var42 - var64));
  assume(0 > (var64 - var65) * (var65 - var64));
  assume(0 > (var64 - var76) * (var76 - var64));
  assume(0 > (var64 - var77) * (var77 - var64));
  assume(0 > (var67 - var0) * (var0 - var67));
  assume(0 > (var67 - var10) * (var10 - var67));
  assume(0 > (var67 - var15) * (var15 - var67));
  assume(0 > (var67 - var29) * (var29 - var67));
  assume(0 > (var67 - var58) * (var58 - var67));
  assume(0 > (var68 - var18) * (var18 - var68));
  assume(0 > (var68 - var3) * (var3 - var68));
  assume(0 > (var68 - var51) * (var51 - var68));
  assume(0 > (var68 - var60) * (var60 - var68));
  assume(0 > (var68 - var63) * (var63 - var68));
  assume(0 > (var69 - var2) * (var2 - var69));
  assume(0 > (var69 - var45) * (var45 - var69));
  assume(0 > (var69 - var49) * (var49 - var69));
  assume(0 > (var70 - var36) * (var36 - var70));
  assume(0 > (var70 - var53) * (var53 - var70));
  assume(0 > (var73 - var21) * (var21 - var73));
  assume(0 > (var73 - var4) * (var4 - var73));
  assume(0 > (var73 - var44) * (var44 - var73));
  assume(0 > (var74 - var36) * (var36 - var74));
  assume(0 > (var74 - var53) * (var53 - var74));
  assume(0 > (var74 - var75) * (var75 - var74));
  assume(0 > (var75 - var28) * (var28 - var75));
  assume(0 > (var75 - var53) * (var53 - var75));
  assume(0 > (var75 - var70) * (var70 - var75));
  assume(0 > (var77 - var24) * (var24 - var77));
  assume(0 > (var77 - var42) * (var42 - var77));
  assume(0 > (var77 - var55) * (var55 - var77));
  assume(0 > (var77 - var76) * (var76 - var77));
  assume(0 > (var78 - var14) * (var14 - var78));
  assume(0 > (var79 - var25) * (var25 - var79));
  assume(0 > (var79 - var38) * (var38 - var79));
  assume(0 > (var79 - var8) * (var8 - var79));
  assume(0 > (var8 - var20) * (var20 - var8));
  assume(0 > (var8 - var39) * (var39 - var8));
  assume(0 > (var80 - var21) * (var21 - var80));
  assume(0 > (var9 - var26) * (var26 - var9));
  assume(0 > (var9 - var30) * (var30 - var9));
  assume(var1 != var21);
  assume(var1 + var21 >= 2);
  assume(var1 != var23);
  assume(var1 + var23 >= 2);
  assume(var1 != var33);
  assume(var1 + var33 >= 2);
  assume(var1 != var4);
  assume(var1 + var4 >= 2);
  assume(var1 != var44);
  assume(var1 + var44 >= 2);
  assume(var1 != var56);
  assume(var1 + var56 >= 2);
  assume(var1 != var73);
  assume(var1 + var73 >= 2);
  assume(var1 != var80);
  assume(var1 + var80 >= 2);
  assume(var13 != var24);
  assume(var13 + var24 >= 2);
  assume(var13 != var42);
  assume(var13 + var42 >= 2);
  assume(var13 != var55);
  assume(var13 + var55 >= 2);
  assume(var13 != var62);
  assume(var13 + var62 >= 2);
  assume(var13 != var64);
  assume(var13 + var64 >= 2);
  assume(var13 != var65);
  assume(var13 + var65 >= 2);
  assume(var13 != var76);
  assume(var13 + var76 >= 2);
  assume(var13 != var77);
  assume(var13 + var77 >= 2);
  assume(var19 != var16);
  assume(var19 + var16 >= 2);
  assume(var19 != var18);
  assume(var19 + var18 >= 2);
  assume(var19 != var3);
  assume(var19 + var3 >= 2);
  assume(var19 != var35);
  assume(var19 + var35 >= 2);
  assume(var19 != var51);
  assume(var19 + var51 >= 2);
  assume(var19 != var60);
  assume(var19 + var60 >= 2);
  assume(var19 != var63);
  assume(var19 + var63 >= 2);
  assume(var19 != var68);
  assume(var19 + var68 >= 2);
  assume(var41 != var14);
  assume(var41 + var14 >= 2);
  assume(var41 != var2);
  assume(var41 + var2 >= 2);
  assume(var41 != var34);
  assume(var41 + var34 >= 2);
  assume(var41 != var37);
  assume(var41 + var37 >= 2);
  assume(var41 != var45);
  assume(var41 + var45 >= 2);
  assume(var41 != var49);
  assume(var41 + var49 >= 2);
  assume(var41 != var69);
  assume(var41 + var69 >= 2);
  assume(var41 != var78);
  assume(var41 + var78 >= 2);
  assume(var5 != var28);
  assume(var5 + var28 >= 2);
  assume(var5 != var36);
  assume(var5 + var36 >= 2);
  assume(var5 != var50);
  assume(var5 + var50 >= 2);
  assume(var5 != var53);
  assume(var5 + var53 >= 2);
  assume(var5 != var59);
  assume(var5 + var59 >= 2);
  assume(var5 != var70);
  assume(var5 + var70 >= 2);
  assume(var5 != var74);
  assume(var5 + var74 >= 2);
  assume(var5 != var75);
  assume(var5 + var75 >= 2);
  assume(var66 != var0);
  assume(var66 + var0 >= 2);
  assume(var66 != var10);
  assume(var66 + var10 >= 2);
  assume(var66 != var12);
  assume(var66 + var12 >= 2);
  assume(var66 != var15);
  assume(var66 + var15 >= 2);
  assume(var66 != var22);
  assume(var66 + var22 >= 2);
  assume(var66 != var29);
  assume(var66 + var29 >= 2);
  assume(var66 != var58);
  assume(var66 + var58 >= 2);
  assume(var66 != var67);
  assume(var66 + var67 >= 2);
  assume(var71 != var17);
  assume(var71 + var17 >= 2);
  assume(var71 != var27);
  assume(var71 + var27 >= 2);
  assume(var71 != var32);
  assume(var71 + var32 >= 2);
  assume(var71 != var48);
  assume(var71 + var48 >= 2);
  assume(var71 != var52);
  assume(var71 + var52 >= 2);
  assume(var71 != var54);
  assume(var71 + var54 >= 2);
  assume(var71 != var61);
  assume(var71 + var61 >= 2);
  assume(var71 != var7);
  assume(var71 + var7 >= 2);
  assume(var72 != var11);
  assume(var72 + var11 >= 2);
  assume(var72 != var26);
  assume(var72 + var26 >= 2);
  assume(var72 != var30);
  assume(var72 + var30 >= 2);
  assume(var72 != var31);
  assume(var72 + var31 >= 2);
  assume(var72 != var43);
  assume(var72 + var43 >= 2);
  assume(var72 != var46);
  assume(var72 + var46 >= 2);
  assume(var72 != var57);
  assume(var72 + var57 >= 2);
  assume(var72 != var9);
  assume(var72 + var9 >= 2);
  assume(var25 == var13);
  assume(var38 == var5);
  assume(var39 == var72);
  assume(var40 == var1);
  assume(var47 == var41);
  assume(var6 == var71);
  assume(var79 == var19);
  assume(var8 == var66);
  reach_error();
  return 0; /* 0 x[0]1 x[1]2 x[2]3 x[3]4 x[4]5 x[5]6 x[6]7 x[7]8 x[8]9 x[9]10
               x[10]11 x[11]12 x[12]13 x[13]14 x[14]15 x[15]16 x[16]17 x[17]18
               x[18]19 x[19]20 x[20]21 x[21]22 x[22]23 x[23]24 x[24]25 x[25]26
               x[26]27 x[27]28 x[28]29 x[29]30 x[30]31 x[31]32 x[32]33 x[33]34
               x[34]35 x[35]36 x[36]37 x[37]38 x[38]39 x[39]40 x[40]41 x[41]42
               x[42]43 x[43]44 x[44]45 x[45]46 x[46]47 x[47]48 x[48]49 x[49]50
               x[50]51 x[51]52 x[52]53 x[53]54 x[54]55 x[55]56 x[56]57 x[57]58
               x[58]59 x[59]60 x[60]61 x[61]62 x[62]63 x[63]64 x[64]65 x[65]66
               x[66]67 x[67]68 x[68]69 x[69]70 x[70]71 x[71]72 x[72]73 x[73]74
               x[74]75 x[75]76 x[76]77 x[77]78 x[78]79 x[79]80 x[80] */
}