- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 2244c1d0-8174-429f-8e58-ccb05485e1fd
    creation_time: 2025-03-22T18:08:14Z
    producer:
      name: Goblint
      version: heads/master-0-g66dff5a90-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp.json'' ''--disable'' ''witness.graphml.enabled''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/termination.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(F end) )
  content:
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-invgen/heapsort.i
        line: 38
        column: 5
        function: main
      value: 1 <= l
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-invgen/heapsort.i
        line: 38
        column: 5
        function: main
      value: n <= 1000000
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-invgen/heapsort.i
        line: 38
        column: 5
        function: main
      value: r <= 1000000
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-invgen/heapsort.i
        line: 38
        column: 5
        function: main
      value: (999999LL + (long long )l) - (long long )n >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-invgen/heapsort.i
        line: 38
        column: 5
        function: main
      value: (999999LL + (long long )l) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-invgen/heapsort.i
        line: 38
        column: 5
        function: main
      value: (2000000LL - (long long )n) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-invgen/heapsort.i
        line: 38
        column: 5
        function: main
      value: (long long )n - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-invgen/heapsort.i
        line: 38
        column: 5
        function: main
      value: (((0LL - (long long )i) + (long long )r >= 0LL && (((((((((((((((((((((((l
        <= 499998 && (3LL - (long long )n) + (long long )r >= 0LL) && (1499998LL -
        (long long )l) - (long long )n >= 0LL) && (1499998LL - (long long )l) - (long
        long )r >= 0LL) && (((0LL - (long long )i) + (long long )n >= 0LL && (((((((((((((((i
        <= 1000000 && j <= 2000000) && (999999LL - (long long )i) + (long long )l
        >= 0LL) && (1000000LL - (long long )j) + (long long )n >= 0LL) && (1000000LL
        - (long long )j) + (long long )r >= 0LL) && (1999999LL - (long long )j) +
        (long long )l >= 0LL) && (1000000LL + (long long )i) - (long long )j >= 0LL)
        && (1499998LL - (long long )i) - (long long )l >= 0LL) && (2000000LL - (long
        long )i) - (long long )n >= 0LL) && (2000000LL - (long long )i) - (long long
        )r >= 0LL) && (2499998LL - (long long )j) - (long long )l >= 0LL) && (3000000LL
        - (long long )i) - (long long )j >= 0LL) && (3000000LL - (long long )j) -
        (long long )n >= 0LL) && (3000000LL - (long long )j) - (long long )r >= 0LL)
        && (((((((((((((((((((((((8 <= n && 8 <= r) && 8 <= i) && 16 <= j) && (-24LL
        + (long long )i) + (long long )j >= 0LL) && (-24LL + (long long )j) + (long
        long )n >= 0LL) && (-24LL + (long long )j) + (long long )r >= 0LL) && (-17LL
        + (long long )j) + (long long )l >= 0LL) && (-16LL + (long long )n) + (long
        long )r >= 0LL) && (-16LL + (long long )i) + (long long )n >= 0LL) && (-16LL
        + (long long )i) + (long long )r >= 0LL) && (-9LL + (long long )l) + (long
        long )n >= 0LL) && (-9LL + (long long )l) + (long long )r >= 0LL) && (-9LL
        + (long long )i) + (long long )l >= 0LL) && (-8LL - (long long )i) + (long
        long )j >= 0LL) && (-7LL - (long long )l) + (long long )n >= 0LL) && (-7LL
        - (long long )l) + (long long )r >= 0LL) && (-15LL + (long long )j) - (long
        long )l >= 0LL) && (-7LL + (long long )i) - (long long )l >= 0LL) && (999984LL
        + (long long )j) - (long long )n >= 0LL) && (999984LL + (long long )j) - (long
        long )r >= 0LL) && (999992LL + (long long )i) - (long long )n >= 0LL) && (999992LL
        + (long long )i) - (long long )r >= 0LL) || ((((((((((((((((((((((4 <= n &&
        4 <= r) && 4 <= i) && 8 <= j) && (-12LL + (long long )i) + (long long )j >=
        0LL) && (-12LL + (long long )j) + (long long )n >= 0LL) && (-12LL + (long
        long )j) + (long long )r >= 0LL) && (-9LL + (long long )j) + (long long )l
        >= 0LL) && (-8LL + (long long )n) + (long long )r >= 0LL) && (-8LL + (long
        long )i) + (long long )n >= 0LL) && (-8LL + (long long )i) + (long long )r
        >= 0LL) && (-5LL + (long long )l) + (long long )n >= 0LL) && (-5LL + (long
        long )l) + (long long )r >= 0LL) && (-5LL + (long long )i) + (long long )l
        >= 0LL) && (-4LL - (long long )i) + (long long )j >= 0LL) && (-3LL - (long
        long )l) + (long long )n >= 0LL) && (-3LL - (long long )l) + (long long )r
        >= 0LL) && (-7LL + (long long )j) - (long long )l >= 0LL) && (-3LL + (long
        long )i) - (long long )l >= 0LL) && (999992LL + (long long )j) - (long long
        )n >= 0LL) && (999992LL + (long long )j) - (long long )r >= 0LL) && (999996LL
        + (long long )i) - (long long )n >= 0LL) && (999996LL + (long long )i) - (long
        long )r >= 0LL))) || ((((((((((((((((((((((((((((((((((((2 <= n && 2 <= r)
        && 2 <= i) && 4 <= j) && i <= 999997) && j <= 1999994) && (-6LL + (long long
        )i) + (long long )j >= 0LL) && (-6LL + (long long )j) + (long long )n >= 0LL)
        && (-6LL + (long long )j) + (long long )r >= 0LL) && (-5LL + (long long )j)
        + (long long )l >= 0LL) && (-4LL + (long long )n) + (long long )r >= 0LL)
        && (-4LL + (long long )i) + (long long )n >= 0LL) && (-4LL + (long long )i)
        + (long long )r >= 0LL) && (-3LL + (long long )l) + (long long )n >= 0LL)
        && (-3LL + (long long )l) + (long long )r >= 0LL) && (-3LL + (long long )i)
        + (long long )l >= 0LL) && (-2LL - (long long )i) + (long long )j >= 0LL)
        && (-1LL - (long long )l) + (long long )n >= 0LL) && (-1LL - (long long )l)
        + (long long )r >= 0LL) && (499999LL - (long long )i) + (long long )l >= 0LL)
        && (999997LL - (long long )j) + (long long )n >= 0LL) && (999997LL - (long
        long )j) + (long long )r >= 0LL) && (1499996LL - (long long )j) + (long long
        )l >= 0LL) && (-3LL + (long long )j) - (long long )l >= 0LL) && (-1LL + (long
        long )i) - (long long )l >= 0LL) && (999996LL + (long long )j) - (long long
        )n >= 0LL) && (999996LL + (long long )j) - (long long )r >= 0LL) && (999997LL
        + (long long )i) - (long long )j >= 0LL) && (999998LL + (long long )i) - (long
        long )n >= 0LL) && (999998LL + (long long )i) - (long long )r >= 0LL) && (1499995LL
        - (long long )i) - (long long )l >= 0LL) && (1999997LL - (long long )i) -
        (long long )n >= 0LL) && (1999997LL - (long long )i) - (long long )r >= 0LL)
        && (2499992LL - (long long )j) - (long long )l >= 0LL) && (2999991LL - (long
        long )i) - (long long )j >= 0LL) && (2999994LL - (long long )j) - (long long
        )n >= 0LL) && (2999994LL - (long long )j) - (long long )r >= 0LL))) || ((((((((((((((((((((((((((((((((((((((1
        <= i && 2 <= n) && 2 <= r) && 2 <= j) && i <= 499998) && j <= 999996) && (-4LL
        + (long long )n) + (long long )r >= 0LL) && (-4LL + (long long )j) + (long
        long )n >= 0LL) && (-4LL + (long long )j) + (long long )r >= 0LL) && (-3LL
        + (long long )l) + (long long )n >= 0LL) && (-3LL + (long long )l) + (long
        long )r >= 0LL) && (-3LL + (long long )i) + (long long )n >= 0LL) && (-3LL
        + (long long )i) + (long long )r >= 0LL) && (-3LL + (long long )i) + (long
        long )j >= 0LL) && (-3LL + (long long )j) + (long long )l >= 0LL) && (-2LL
        + (long long )i) + (long long )l >= 0LL) && (-1LL - (long long )l) + (long
        long )n >= 0LL) && (-1LL - (long long )i) + (long long )n >= 0LL) && (-1LL
        - (long long )i) + (long long )j >= 0LL) && (0LL - (long long )l) + (long
        long )r >= 0LL) && (0LL - (long long )i) + (long long )l >= 0LL) && (499997LL
        - (long long )j) + (long long )n >= 0LL) && (499998LL - (long long )j) + (long
        long )l >= 0LL) && (499998LL - (long long )j) + (long long )r >= 0LL) && (-1LL
        + (long long )j) - (long long )l >= 0LL) && (499998LL + (long long )i) - (long
        long )j >= 0LL) && (999998LL + (long long )j) - (long long )n >= 0LL) && (999998LL
        + (long long )j) - (long long )r >= 0LL) && (999999LL + (long long )i) - (long
        long )n >= 0LL) && (999999LL + (long long )i) - (long long )r >= 0LL) && (999996LL
        - (long long )i) - (long long )l >= 0LL) && (1499994LL - (long long )i) -
        (long long )j >= 0LL) && (1499994LL - (long long )j) - (long long )l >= 0LL)
        && (1499998LL - (long long )i) - (long long )n >= 0LL) && (1499998LL - (long
        long )i) - (long long )r >= 0LL) && (1999996LL - (long long )j) - (long long
        )n >= 0LL) && (1999996LL - (long long )j) - (long long )r >= 0LL) && (long
        long )i - (long long )l >= 0LL) && l == i))) || (((((((((((((((((((((((((((((((((((((((((16
        <= n && 16 <= r) && 16 <= i) && 32 <= j) && l <= 499996) && i <= 1000000)
        && j <= 2000000) && (-48LL + (long long )i) + (long long )j >= 0LL) && (-48LL
        + (long long )j) + (long long )n >= 0LL) && (-48LL + (long long )j) + (long
        long )r >= 0LL) && (-33LL + (long long )j) + (long long )l >= 0LL) && (-32LL
        + (long long )n) + (long long )r >= 0LL) && (-32LL + (long long )i) + (long
        long )n >= 0LL) && (-32LL + (long long )i) + (long long )r >= 0LL) && (-17LL
        + (long long )l) + (long long )n >= 0LL) && (-17LL + (long long )l) + (long
        long )r >= 0LL) && (-17LL + (long long )i) + (long long )l >= 0LL) && (-16LL
        - (long long )i) + (long long )j >= 0LL) && (-15LL - (long long )l) + (long
        long )n >= 0LL) && (-15LL - (long long )l) + (long long )r >= 0LL) && (0LL
        - (long long )i) + (long long )n >= 0LL) && (999984LL - (long long )n) + (long
        long )r >= 0LL) && (999999LL - (long long )i) + (long long )l >= 0LL) && (1000000LL
        - (long long )j) + (long long )n >= 0LL) && (1000000LL - (long long )j) +
        (long long )r >= 0LL) && (1999999LL - (long long )j) + (long long )l >= 0LL)
        && (-31LL + (long long )j) - (long long )l >= 0LL) && (-15LL + (long long
        )i) - (long long )l >= 0LL) && (999968LL + (long long )j) - (long long )n
        >= 0LL) && (999968LL + (long long )j) - (long long )r >= 0LL) && (999984LL
        + (long long )i) - (long long )n >= 0LL) && (999984LL + (long long )i) - (long
        long )r >= 0LL) && (1000000LL + (long long )i) - (long long )j >= 0LL) &&
        (1499996LL - (long long )l) - (long long )n >= 0LL) && (1499996LL - (long
        long )l) - (long long )r >= 0LL) && (1499996LL - (long long )i) - (long long
        )l >= 0LL) && (2000000LL - (long long )i) - (long long )n >= 0LL) && (2000000LL
        - (long long )i) - (long long )r >= 0LL) && (2499996LL - (long long )j) -
        (long long )l >= 0LL) && (3000000LL - (long long )i) - (long long )j >= 0LL)
        && (3000000LL - (long long )j) - (long long )n >= 0LL) && (3000000LL - (long
        long )j) - (long long )r >= 0LL)) || (((((((((((((((((((((((((((((((((((((((((16
        <= n && 16 <= r) && 16 <= i) && 32 <= j) && l <= 499999) && i <= 1000000)
        && j <= 2000000) && (-48LL + (long long )i) + (long long )j >= 0LL) && (-48LL
        + (long long )j) + (long long )n >= 0LL) && (-48LL + (long long )j) + (long
        long )r >= 0LL) && (-33LL + (long long )j) + (long long )l >= 0LL) && (-32LL
        + (long long )n) + (long long )r >= 0LL) && (-32LL + (long long )i) + (long
        long )n >= 0LL) && (-32LL + (long long )i) + (long long )r >= 0LL) && (-17LL
        + (long long )l) + (long long )n >= 0LL) && (-17LL + (long long )l) + (long
        long )r >= 0LL) && (-17LL + (long long )i) + (long long )l >= 0LL) && (-16LL
        - (long long )i) + (long long )j >= 0LL) && (-15LL - (long long )l) + (long
        long )n >= 0LL) && (-15LL - (long long )l) + (long long )r >= 0LL) && (0LL
        - (long long )i) + (long long )n >= 0LL) && (2LL - (long long )n) + (long
        long )r >= 0LL) && (999999LL - (long long )i) + (long long )l >= 0LL) && (1000000LL
        - (long long )j) + (long long )n >= 0LL) && (1000000LL - (long long )j) +
        (long long )r >= 0LL) && (1999999LL - (long long )j) + (long long )l >= 0LL)
        && (-31LL + (long long )j) - (long long )l >= 0LL) && (-15LL + (long long
        )i) - (long long )l >= 0LL) && (999968LL + (long long )j) - (long long )n
        >= 0LL) && (999968LL + (long long )j) - (long long )r >= 0LL) && (999984LL
        + (long long )i) - (long long )n >= 0LL) && (999984LL + (long long )i) - (long
        long )r >= 0LL) && (1000000LL + (long long )i) - (long long )j >= 0LL) &&
        (1499999LL - (long long )l) - (long long )n >= 0LL) && (1499999LL - (long
        long )l) - (long long )r >= 0LL) && (1499999LL - (long long )i) - (long long
        )l >= 0LL) && (2000000LL - (long long )i) - (long long )n >= 0LL) && (2000000LL
        - (long long )i) - (long long )r >= 0LL) && (2499999LL - (long long )j) -
        (long long )l >= 0LL) && (3000000LL - (long long )i) - (long long )j >= 0LL)
        && (3000000LL - (long long )j) - (long long )n >= 0LL) && (3000000LL - (long
        long )j) - (long long )r >= 0LL)) || (((((((((((((((((((((((((((((((((((((((((8
        <= n && 8 <= r) && 8 <= i) && 16 <= j) && l <= 499996) && i <= 1000000) &&
        j <= 2000000) && (-24LL + (long long )i) + (long long )j >= 0LL) && (-24LL
        + (long long )j) + (long long )n >= 0LL) && (-24LL + (long long )j) + (long
        long )r >= 0LL) && (-17LL + (long long )j) + (long long )l >= 0LL) && (-16LL
        + (long long )n) + (long long )r >= 0LL) && (-16LL + (long long )i) + (long
        long )n >= 0LL) && (-16LL + (long long )i) + (long long )r >= 0LL) && (-9LL
        + (long long )l) + (long long )n >= 0LL) && (-9LL + (long long )l) + (long
        long )r >= 0LL) && (-9LL + (long long )i) + (long long )l >= 0LL) && (-8LL
        - (long long )i) + (long long )j >= 0LL) && (-7LL - (long long )l) + (long
        long )n >= 0LL) && (-7LL - (long long )l) + (long long )r >= 0LL) && (0LL
        - (long long )i) + (long long )n >= 0LL) && (999992LL - (long long )n) + (long
        long )r >= 0LL) && (999999LL - (long long )i) + (long long )l >= 0LL) && (1000000LL
        - (long long )j) + (long long )n >= 0LL) && (1000000LL - (long long )j) +
        (long long )r >= 0LL) && (1999999LL - (long long )j) + (long long )l >= 0LL)
        && (-15LL + (long long )j) - (long long )l >= 0LL) && (-7LL + (long long )i)
        - (long long )l >= 0LL) && (999984LL + (long long )j) - (long long )n >= 0LL)
        && (999984LL + (long long )j) - (long long )r >= 0LL) && (999992LL + (long
        long )i) - (long long )n >= 0LL) && (999992LL + (long long )i) - (long long
        )r >= 0LL) && (1000000LL + (long long )i) - (long long )j >= 0LL) && (1499996LL
        - (long long )l) - (long long )n >= 0LL) && (1499996LL - (long long )l) -
        (long long )r >= 0LL) && (1499996LL - (long long )i) - (long long )l >= 0LL)
        && (2000000LL - (long long )i) - (long long )n >= 0LL) && (2000000LL - (long
        long )i) - (long long )r >= 0LL) && (2499996LL - (long long )j) - (long long
        )l >= 0LL) && (3000000LL - (long long )i) - (long long )j >= 0LL) && (3000000LL
        - (long long )j) - (long long )n >= 0LL) && (3000000LL - (long long )j) -
        (long long )r >= 0LL)) || (((((((((((((((((((((((((((((((((((((((((8 <= n
        && 8 <= r) && 8 <= i) && 16 <= j) && l <= 499999) && i <= 1000000) && j <=
        2000000) && (-24LL + (long long )i) + (long long )j >= 0LL) && (-24LL + (long
        long )j) + (long long )n >= 0LL) && (-24LL + (long long )j) + (long long )r
        >= 0LL) && (-17LL + (long long )j) + (long long )l >= 0LL) && (-16LL + (long
        long )n) + (long long )r >= 0LL) && (-16LL + (long long )i) + (long long )n
        >= 0LL) && (-16LL + (long long )i) + (long long )r >= 0LL) && (-9LL + (long
        long )l) + (long long )n >= 0LL) && (-9LL + (long long )l) + (long long )r
        >= 0LL) && (-9LL + (long long )i) + (long long )l >= 0LL) && (-8LL - (long
        long )i) + (long long )j >= 0LL) && (-7LL - (long long )l) + (long long )n
        >= 0LL) && (-7LL - (long long )l) + (long long )r >= 0LL) && (0LL - (long
        long )i) + (long long )n >= 0LL) && (2LL - (long long )n) + (long long )r
        >= 0LL) && (999999LL - (long long )i) + (long long )l >= 0LL) && (1000000LL
        - (long long )j) + (long long )n >= 0LL) && (1000000LL - (long long )j) +
        (long long )r >= 0LL) && (1999999LL - (long long )j) + (long long )l >= 0LL)
        && (-15LL + (long long )j) - (long long )l >= 0LL) && (-7LL + (long long )i)
        - (long long )l >= 0LL) && (999984LL + (long long )j) - (long long )n >= 0LL)
        && (999984LL + (long long )j) - (long long )r >= 0LL) && (999992LL + (long
        long )i) - (long long )n >= 0LL) && (999992LL + (long long )i) - (long long
        )r >= 0LL) && (1000000LL + (long long )i) - (long long )j >= 0LL) && (1499999LL
        - (long long )l) - (long long )n >= 0LL) && (1499999LL - (long long )l) -
        (long long )r >= 0LL) && (1499999LL - (long long )i) - (long long )l >= 0LL)
        && (2000000LL - (long long )i) - (long long )n >= 0LL) && (2000000LL - (long
        long )i) - (long long )r >= 0LL) && (2499999LL - (long long )j) - (long long
        )l >= 0LL) && (3000000LL - (long long )i) - (long long )j >= 0LL) && (3000000LL
        - (long long )j) - (long long )n >= 0LL) && (3000000LL - (long long )j) -
        (long long )r >= 0LL)) || (((((((((((((((((((((((((((((((((((((((((4 <= n
        && 4 <= r) && 4 <= i) && 8 <= j) && l <= 499996) && i <= 1000000) && j <=
        2000000) && (-12LL + (long long )i) + (long long )j >= 0LL) && (-12LL + (long
        long )j) + (long long )n >= 0LL) && (-12LL + (long long )j) + (long long )r
        >= 0LL) && (-9LL + (long long )j) + (long long )l >= 0LL) && (-8LL + (long
        long )n) + (long long )r >= 0LL) && (-8LL + (long long )i) + (long long )n
        >= 0LL) && (-8LL + (long long )i) + (long long )r >= 0LL) && (-5LL + (long
        long )l) + (long long )n >= 0LL) && (-5LL + (long long )l) + (long long )r
        >= 0LL) && (-5LL + (long long )i) + (long long )l >= 0LL) && (-4LL - (long
        long )i) + (long long )j >= 0LL) && (-3LL - (long long )l) + (long long )n
        >= 0LL) && (-3LL - (long long )l) + (long long )r >= 0LL) && (0LL - (long
        long )i) + (long long )n >= 0LL) && (999996LL - (long long )n) + (long long
        )r >= 0LL) && (999999LL - (long long )i) + (long long )l >= 0LL) && (1000000LL
        - (long long )j) + (long long )n >= 0LL) && (1000000LL - (long long )j) +
        (long long )r >= 0LL) && (1999999LL - (long long )j) + (long long )l >= 0LL)
        && (-7LL + (long long )j) - (long long )l >= 0LL) && (-3LL + (long long )i)
        - (long long )l >= 0LL) && (999992LL + (long long )j) - (long long )n >= 0LL)
        && (999992LL + (long long )j) - (long long )r >= 0LL) && (999996LL + (long
        long )i) - (long long )n >= 0LL) && (999996LL + (long long )i) - (long long
        )r >= 0LL) && (1000000LL + (long long )i) - (long long )j >= 0LL) && (1499996LL
        - (long long )l) - (long long )n >= 0LL) && (1499996LL - (long long )l) -
        (long long )r >= 0LL) && (1499996LL - (long long )i) - (long long )l >= 0LL)
        && (2000000LL - (long long )i) - (long long )n >= 0LL) && (2000000LL - (long
        long )i) - (long long )r >= 0LL) && (2499996LL - (long long )j) - (long long
        )l >= 0LL) && (3000000LL - (long long )i) - (long long )j >= 0LL) && (3000000LL
        - (long long )j) - (long long )n >= 0LL) && (3000000LL - (long long )j) -
        (long long )r >= 0LL)) || (((((((((((((((((((((((((((((((((((((((((4 <= n
        && 4 <= r) && 4 <= i) && 8 <= j) && l <= 499999) && i <= 1000000) && j <=
        2000000) && (-12LL + (long long )i) + (long long )j >= 0LL) && (-12LL + (long
        long )j) + (long long )n >= 0LL) && (-12LL + (long long )j) + (long long )r
        >= 0LL) && (-9LL + (long long )j) + (long long )l >= 0LL) && (-8LL + (long
        long )n) + (long long )r >= 0LL) && (-8LL + (long long )i) + (long long )n
        >= 0LL) && (-8LL + (long long )i) + (long long )r >= 0LL) && (-5LL + (long
        long )l) + (long long )n >= 0LL) && (-5LL + (long long )l) + (long long )r
        >= 0LL) && (-5LL + (long long )i) + (long long )l >= 0LL) && (-4LL - (long
        long )i) + (long long )j >= 0LL) && (-3LL - (long long )l) + (long long )n
        >= 0LL) && (-3LL - (long long )l) + (long long )r >= 0LL) && (0LL - (long
        long )i) + (long long )n >= 0LL) && (2LL - (long long )n) + (long long )r
        >= 0LL) && (999999LL - (long long )i) + (long long )l >= 0LL) && (1000000LL
        - (long long )j) + (long long )n >= 0LL) && (1000000LL - (long long )j) +
        (long long )r >= 0LL) && (1999999LL - (long long )j) + (long long )l >= 0LL)
        && (-7LL + (long long )j) - (long long )l >= 0LL) && (-3LL + (long long )i)
        - (long long )l >= 0LL) && (999992LL + (long long )j) - (long long )n >= 0LL)
        && (999992LL + (long long )j) - (long long )r >= 0LL) && (999996LL + (long
        long )i) - (long long )n >= 0LL) && (999996LL + (long long )i) - (long long
        )r >= 0LL) && (1000000LL + (long long )i) - (long long )j >= 0LL) && (1499999LL
        - (long long )l) - (long long )n >= 0LL) && (1499999LL - (long long )l) -
        (long long )r >= 0LL) && (1499999LL - (long long )i) - (long long )l >= 0LL)
        && (2000000LL - (long long )i) - (long long )n >= 0LL) && (2000000LL - (long
        long )i) - (long long )r >= 0LL) && (2499999LL - (long long )j) - (long long
        )l >= 0LL) && (3000000LL - (long long )i) - (long long )j >= 0LL) && (3000000LL
        - (long long )j) - (long long )n >= 0LL) && (3000000LL - (long long )j) -
        (long long )r >= 0LL)) || (((((((((((((((((((((((((((((((((((((((((2 <= n
        && 2 <= r) && 2 <= i) && 4 <= j) && l <= 499996) && i <= 999993) && j <= 1999986)
        && (-6LL + (long long )i) + (long long )j >= 0LL) && (-6LL + (long long )j)
        + (long long )n >= 0LL) && (-6LL + (long long )j) + (long long )r >= 0LL)
        && (-5LL + (long long )j) + (long long )l >= 0LL) && (-4LL + (long long )n)
        + (long long )r >= 0LL) && (-4LL + (long long )i) + (long long )n >= 0LL)
        && (-4LL + (long long )i) + (long long )r >= 0LL) && (-3LL + (long long )l)
        + (long long )n >= 0LL) && (-3LL + (long long )l) + (long long )r >= 0LL)
        && (-3LL + (long long )i) + (long long )l >= 0LL) && (-2LL - (long long )i)
        + (long long )j >= 0LL) && (-1LL - (long long )l) + (long long )n >= 0LL)
        && (-1LL - (long long )l) + (long long )r >= 0LL) && (0LL - (long long )i)
        + (long long )n >= 0LL) && (499997LL - (long long )i) + (long long )l >= 0LL)
        && (999993LL - (long long )j) + (long long )n >= 0LL) && (999993LL - (long
        long )j) + (long long )r >= 0LL) && (999998LL - (long long )n) + (long long
        )r >= 0LL) && (1499990LL - (long long )j) + (long long )l >= 0LL) && (-3LL
        + (long long )j) - (long long )l >= 0LL) && (-1LL + (long long )i) - (long
        long )l >= 0LL) && (999993LL + (long long )i) - (long long )j >= 0LL) && (999996LL
        + (long long )j) - (long long )n >= 0LL) && (999996LL + (long long )j) - (long
        long )r >= 0LL) && (999998LL + (long long )i) - (long long )n >= 0LL) && (999998LL
        + (long long )i) - (long long )r >= 0LL) && (1499989LL - (long long )i) -
        (long long )l >= 0LL) && (1499996LL - (long long )l) - (long long )n >= 0LL)
        && (1499996LL - (long long )l) - (long long )r >= 0LL) && (1999993LL - (long
        long )i) - (long long )n >= 0LL) && (1999993LL - (long long )i) - (long long
        )r >= 0LL) && (2499982LL - (long long )j) - (long long )l >= 0LL) && (2999979LL
        - (long long )i) - (long long )j >= 0LL) && (2999986LL - (long long )j) -
        (long long )n >= 0LL) && (2999986LL - (long long )j) - (long long )r >= 0LL))
        || (((((((((((((((((((((((((((((((((((((((((2 <= n && 2 <= r) && 2 <= i) &&
        4 <= j) && l <= 499999) && i <= 999999) && j <= 1999998) && (-6LL + (long
        long )i) + (long long )j >= 0LL) && (-6LL + (long long )j) + (long long )n
        >= 0LL) && (-6LL + (long long )j) + (long long )r >= 0LL) && (-5LL + (long
        long )j) + (long long )l >= 0LL) && (-4LL + (long long )n) + (long long )r
        >= 0LL) && (-4LL + (long long )i) + (long long )n >= 0LL) && (-4LL + (long
        long )i) + (long long )r >= 0LL) && (-3LL + (long long )l) + (long long )n
        >= 0LL) && (-3LL + (long long )l) + (long long )r >= 0LL) && (-3LL + (long
        long )i) + (long long )l >= 0LL) && (-2LL - (long long )i) + (long long )j
        >= 0LL) && (-1LL - (long long )l) + (long long )n >= 0LL) && (-1LL - (long
        long )l) + (long long )r >= 0LL) && (0LL - (long long )i) + (long long )n
        >= 0LL) && (2LL - (long long )n) + (long long )r >= 0LL) && (500000LL - (long
        long )i) + (long long )l >= 0LL) && (999999LL - (long long )j) + (long long
        )n >= 0LL) && (999999LL - (long long )j) + (long long )r >= 0LL) && (1499999LL
        - (long long )j) + (long long )l >= 0LL) && (-3LL + (long long )j) - (long
        long )l >= 0LL) && (-1LL + (long long )i) - (long long )l >= 0LL) && (999996LL
        + (long long )j) - (long long )n >= 0LL) && (999996LL + (long long )j) - (long
        long )r >= 0LL) && (999998LL + (long long )i) - (long long )n >= 0LL) && (999998LL
        + (long long )i) - (long long )r >= 0LL) && (999999LL + (long long )i) - (long
        long )j >= 0LL) && (1499998LL - (long long )i) - (long long )l >= 0LL) &&
        (1499999LL - (long long )l) - (long long )n >= 0LL) && (1499999LL - (long
        long )l) - (long long )r >= 0LL) && (1999999LL - (long long )i) - (long long
        )n >= 0LL) && (1999999LL - (long long )i) - (long long )r >= 0LL) && (2499997LL
        - (long long )j) - (long long )l >= 0LL) && (2999997LL - (long long )i) -
        (long long )j >= 0LL) && (2999998LL - (long long )j) - (long long )n >= 0LL)
        && (2999998LL - (long long )j) - (long long )r >= 0LL)) || ((((((((((((((((((((((((((((((((((((((((((1
        <= i && 2 <= n) && 2 <= r) && 2 <= j) && l <= 499996) && i <= 499996) && j
        <= 999992) && (-4LL + (long long )n) + (long long )r >= 0LL) && (-4LL + (long
        long )j) + (long long )n >= 0LL) && (-4LL + (long long )j) + (long long )r
        >= 0LL) && (-3LL + (long long )l) + (long long )n >= 0LL) && (-3LL + (long
        long )l) + (long long )r >= 0LL) && (-3LL + (long long )i) + (long long )n
        >= 0LL) && (-3LL + (long long )i) + (long long )r >= 0LL) && (-3LL + (long
        long )i) + (long long )j >= 0LL) && (-3LL + (long long )j) + (long long )l
        >= 0LL) && (-2LL + (long long )i) + (long long )l >= 0LL) && (-1LL - (long
        long )l) + (long long )n >= 0LL) && (-1LL - (long long )i) + (long long )n
        >= 0LL) && (-1LL - (long long )i) + (long long )j >= 0LL) && (0LL - (long
        long )l) + (long long )r >= 0LL) && (0LL - (long long )i) + (long long )l
        >= 0LL) && (499995LL - (long long )j) + (long long )n >= 0LL) && (499996LL
        - (long long )j) + (long long )l >= 0LL) && (499996LL - (long long )j) + (long
        long )r >= 0LL) && (999998LL - (long long )n) + (long long )r >= 0LL) && (-1LL
        + (long long )j) - (long long )l >= 0LL) && (499996LL + (long long )i) - (long
        long )j >= 0LL) && (999998LL + (long long )j) - (long long )n >= 0LL) && (999998LL
        + (long long )j) - (long long )r >= 0LL) && (999999LL + (long long )i) - (long
        long )n >= 0LL) && (999999LL + (long long )i) - (long long )r >= 0LL) && (999992LL
        - (long long )i) - (long long )l >= 0LL) && (1499988LL - (long long )i) -
        (long long )j >= 0LL) && (1499988LL - (long long )j) - (long long )l >= 0LL)
        && (1499996LL - (long long )l) - (long long )n >= 0LL) && (1499996LL - (long
        long )l) - (long long )r >= 0LL) && (1499996LL - (long long )i) - (long long
        )n >= 0LL) && (1499996LL - (long long )i) - (long long )r >= 0LL) && (1999992LL
        - (long long )j) - (long long )n >= 0LL) && (1999992LL - (long long )j) -
        (long long )r >= 0LL) && (long long )i - (long long )l >= 0LL) && l == i))
        || ((((((((((((((((((((((((((((((((((((((((((1 <= i && 2 <= n) && 2 <= r)
        && 2 <= j) && l <= 499999) && i <= 499999) && j <= 999998) && (-4LL + (long
        long )n) + (long long )r >= 0LL) && (-4LL + (long long )j) + (long long )n
        >= 0LL) && (-4LL + (long long )j) + (long long )r >= 0LL) && (-3LL + (long
        long )l) + (long long )n >= 0LL) && (-3LL + (long long )l) + (long long )r
        >= 0LL) && (-3LL + (long long )i) + (long long )n >= 0LL) && (-3LL + (long
        long )i) + (long long )r >= 0LL) && (-3LL + (long long )i) + (long long )j
        >= 0LL) && (-3LL + (long long )j) + (long long )l >= 0LL) && (-2LL + (long
        long )i) + (long long )l >= 0LL) && (-1LL - (long long )l) + (long long )n
        >= 0LL) && (-1LL - (long long )i) + (long long )n >= 0LL) && (-1LL - (long
        long )i) + (long long )j >= 0LL) && (0LL - (long long )l) + (long long )r
        >= 0LL) && (0LL - (long long )i) + (long long )l >= 0LL) && (2LL - (long long
        )n) + (long long )r >= 0LL) && (499998LL - (long long )j) + (long long )n
        >= 0LL) && (499999LL - (long long )j) + (long long )l >= 0LL) && (499999LL
        - (long long )j) + (long long )r >= 0LL) && (-1LL + (long long )j) - (long
        long )l >= 0LL) && (499999LL + (long long )i) - (long long )j >= 0LL) && (999998LL
        + (long long )j) - (long long )n >= 0LL) && (999998LL + (long long )j) - (long
        long )r >= 0LL) && (999999LL + (long long )i) - (long long )n >= 0LL) && (999999LL
        + (long long )i) - (long long )r >= 0LL) && (999998LL - (long long )i) - (long
        long )l >= 0LL) && (1499997LL - (long long )i) - (long long )j >= 0LL) &&
        (1499997LL - (long long )j) - (long long )l >= 0LL) && (1499999LL - (long
        long )l) - (long long )n >= 0LL) && (1499999LL - (long long )l) - (long long
        )r >= 0LL) && (1499999LL - (long long )i) - (long long )n >= 0LL) && (1499999LL
        - (long long )i) - (long long )r >= 0LL) && (1999998LL - (long long )j) -
        (long long )n >= 0LL) && (1999998LL - (long long )j) - (long long )r >= 0LL)
        && (long long )i - (long long )l >= 0LL) && l == i)) || (((((((((((((((((((((((((((((((((((((((((16
        <= n && 16 <= r) && 16 <= i) && 32 <= j) && l <= 499997) && i <= 1000000)
        && j <= 2000000) && (-48LL + (long long )i) + (long long )j >= 0LL) && (-48LL
        + (long long )j) + (long long )n >= 0LL) && (-48LL + (long long )j) + (long
        long )r >= 0LL) && (-33LL + (long long )j) + (long long )l >= 0LL) && (-32LL
        + (long long )n) + (long long )r >= 0LL) && (-32LL + (long long )i) + (long
        long )n >= 0LL) && (-32LL + (long long )i) + (long long )r >= 0LL) && (-17LL
        + (long long )l) + (long long )n >= 0LL) && (-17LL + (long long )l) + (long
        long )r >= 0LL) && (-17LL + (long long )i) + (long long )l >= 0LL) && (-16LL
        - (long long )i) + (long long )j >= 0LL) && (-15LL - (long long )l) + (long
        long )n >= 0LL) && (-15LL - (long long )l) + (long long )r >= 0LL) && (0LL
        - (long long )i) + (long long )n >= 0LL) && (4LL - (long long )n) + (long
        long )r >= 0LL) && (999999LL - (long long )i) + (long long )l >= 0LL) && (1000000LL
        - (long long )j) + (long long )n >= 0LL) && (1000000LL - (long long )j) +
        (long long )r >= 0LL) && (1999999LL - (long long )j) + (long long )l >= 0LL)
        && (-31LL + (long long )j) - (long long )l >= 0LL) && (-15LL + (long long
        )i) - (long long )l >= 0LL) && (999968LL + (long long )j) - (long long )n
        >= 0LL) && (999968LL + (long long )j) - (long long )r >= 0LL) && (999984LL
        + (long long )i) - (long long )n >= 0LL) && (999984LL + (long long )i) - (long
        long )r >= 0LL) && (1000000LL + (long long )i) - (long long )j >= 0LL) &&
        (1499997LL - (long long )l) - (long long )n >= 0LL) && (1499997LL - (long
        long )l) - (long long )r >= 0LL) && (1499997LL - (long long )i) - (long long
        )l >= 0LL) && (2000000LL - (long long )i) - (long long )n >= 0LL) && (2000000LL
        - (long long )i) - (long long )r >= 0LL) && (2499997LL - (long long )j) -
        (long long )l >= 0LL) && (3000000LL - (long long )i) - (long long )j >= 0LL)
        && (3000000LL - (long long )j) - (long long )n >= 0LL) && (3000000LL - (long
        long )j) - (long long )r >= 0LL)) || (((((((((((((((((((((((((((((((((((((((((16
        <= n && 16 <= r) && 16 <= i) && 32 <= j) && l <= 500000) && i <= 1000000)
        && j <= 2000000) && (-48LL + (long long )i) + (long long )j >= 0LL) && (-48LL
        + (long long )j) + (long long )n >= 0LL) && (-48LL + (long long )j) + (long
        long )r >= 0LL) && (-33LL + (long long )j) + (long long )l >= 0LL) && (-32LL
        + (long long )n) + (long long )r >= 0LL) && (-32LL + (long long )i) + (long
        long )n >= 0LL) && (-32LL + (long long )i) + (long long )r >= 0LL) && (-17LL
        + (long long )l) + (long long )n >= 0LL) && (-17LL + (long long )l) + (long
        long )r >= 0LL) && (-17LL + (long long )i) + (long long )l >= 0LL) && (-16LL
        - (long long )i) + (long long )j >= 0LL) && (-15LL - (long long )l) + (long
        long )n >= 0LL) && (-15LL - (long long )l) + (long long )r >= 0LL) && (0LL
        - (long long )i) + (long long )n >= 0LL) && (1LL - (long long )n) + (long
        long )r >= 0LL) && (999999LL - (long long )i) + (long long )l >= 0LL) && (1000000LL
        - (long long )j) + (long long )n >= 0LL) && (1000000LL - (long long )j) +
        (long long )r >= 0LL) && (1999999LL - (long long )j) + (long long )l >= 0LL)
        && (-31LL + (long long )j) - (long long )l >= 0LL) && (-15LL + (long long
        )i) - (long long )l >= 0LL) && (999968LL + (long long )j) - (long long )n
        >= 0LL) && (999968LL + (long long )j) - (long long )r >= 0LL) && (999984LL
        + (long long )i) - (long long )n >= 0LL) && (999984LL + (long long )i) - (long
        long )r >= 0LL) && (1000000LL + (long long )i) - (long long )j >= 0LL) &&
        (1500000LL - (long long )l) - (long long )n >= 0LL) && (1500000LL - (long
        long )l) - (long long )r >= 0LL) && (1500000LL - (long long )i) - (long long
        )l >= 0LL) && (2000000LL - (long long )i) - (long long )n >= 0LL) && (2000000LL
        - (long long )i) - (long long )r >= 0LL) && (2500000LL - (long long )j) -
        (long long )l >= 0LL) && (3000000LL - (long long )i) - (long long )j >= 0LL)
        && (3000000LL - (long long )j) - (long long )n >= 0LL) && (3000000LL - (long
        long )j) - (long long )r >= 0LL)) || (((((((((((((((((((((((((((((((((((((((((8
        <= n && 8 <= r) && 8 <= i) && 16 <= j) && l <= 499997) && i <= 1000000) &&
        j <= 2000000) && (-24LL + (long long )i) + (long long )j >= 0LL) && (-24LL
        + (long long )j) + (long long )n >= 0LL) && (-24LL + (long long )j) + (long
        long )r >= 0LL) && (-17LL + (long long )j) + (long long )l >= 0LL) && (-16LL
        + (long long )n) + (long long )r >= 0LL) && (-16LL + (long long )i) + (long
        long )n >= 0LL) && (-16LL + (long long )i) + (long long )r >= 0LL) && (-9LL
        + (long long )l) + (long long )n >= 0LL) && (-9LL + (long long )l) + (long
        long )r >= 0LL) && (-9LL + (long long )i) + (long long )l >= 0LL) && (-8LL
        - (long long )i) + (long long )j >= 0LL) && (-7LL - (long long )l) + (long
        long )n >= 0LL) && (-7LL - (long long )l) + (long long )r >= 0LL) && (0LL
        - (long long )i) + (long long )n >= 0LL) && (4LL - (long long )n) + (long
        long )r >= 0LL) && (999999LL - (long long )i) + (long long )l >= 0LL) && (1000000LL
        - (long long )j) + (long long )n >= 0LL) && (1000000LL - (long long )j) +
        (long long )r >= 0LL) && (1999999LL - (long long )j) + (long long )l >= 0LL)
        && (-15LL + (long long )j) - (long long )l >= 0LL) && (-7LL + (long long )i)
        - (long long )l >= 0LL) && (999984LL + (long long )j) - (long long )n >= 0LL)
        && (999984LL + (long long )j) - (long long )r >= 0LL) && (999992LL + (long
        long )i) - (long long )n >= 0LL) && (999992LL + (long long )i) - (long long
        )r >= 0LL) && (1000000LL + (long long )i) - (long long )j >= 0LL) && (1499997LL
        - (long long )l) - (long long )n >= 0LL) && (1499997LL - (long long )l) -
        (long long )r >= 0LL) && (1499997LL - (long long )i) - (long long )l >= 0LL)
        && (2000000LL - (long long )i) - (long long )n >= 0LL) && (2000000LL - (long
        long )i) - (long long )r >= 0LL) && (2499997LL - (long long )j) - (long long
        )l >= 0LL) && (3000000LL - (long long )i) - (long long )j >= 0LL) && (3000000LL
        - (long long )j) - (long long )n >= 0LL) && (3000000LL - (long long )j) -
        (long long )r >= 0LL)) || (((((((((((((((((((((((((((((((((((((((((8 <= n
        && 8 <= r) && 8 <= i) && 16 <= j) && l <= 500000) && i <= 1000000) && j <=
        2000000) && (-24LL + (long long )i) + (long long )j >= 0LL) && (-24LL + (long
        long )j) + (long long )n >= 0LL) && (-24LL + (long long )j) + (long long )r
        >= 0LL) && (-17LL + (long long )j) + (long long )l >= 0LL) && (-16LL + (long
        long )n) + (long long )r >= 0LL) && (-16LL + (long long )i) + (long long )n
        >= 0LL) && (-16LL + (long long )i) + (long long )r >= 0LL) && (-9LL + (long
        long )l) + (long long )n >= 0LL) && (-9LL + (long long )l) + (long long )r
        >= 0LL) && (-9LL + (long long )i) + (long long )l >= 0LL) && (-8LL - (long
        long )i) + (long long )j >= 0LL) && (-7LL - (long long )l) + (long long )n
        >= 0LL) && (-7LL - (long long )l) + (long long )r >= 0LL) && (0LL - (long
        long )i) + (long long )n >= 0LL) && (1LL - (long long )n) + (long long )r
        >= 0LL) && (999999LL - (long long )i) + (long long )l >= 0LL) && (1000000LL
        - (long long )j) + (long long )n >= 0LL) && (1000000LL - (long long )j) +
        (long long )r >= 0LL) && (1999999LL - (long long )j) + (long long )l >= 0LL)
        && (-15LL + (long long )j) - (long long )l >= 0LL) && (-7LL + (long long )i)
        - (long long )l >= 0LL) && (999984LL + (long long )j) - (long long )n >= 0LL)
        && (999984LL + (long long )j) - (long long )r >= 0LL) && (999992LL + (long
        long )i) - (long long )n >= 0LL) && (999992LL + (long long )i) - (long long
        )r >= 0LL) && (1000000LL + (long long )i) - (long long )j >= 0LL) && (1500000LL
        - (long long )l) - (long long )n >= 0LL) && (1500000LL - (long long )l) -
        (long long )r >= 0LL) && (1500000LL - (long long )i) - (long long )l >= 0LL)
        && (2000000LL - (long long )i) - (long long )n >= 0LL) && (2000000LL - (long
        long )i) - (long long )r >= 0LL) && (2500000LL - (long long )j) - (long long
        )l >= 0LL) && (3000000LL - (long long )i) - (long long )j >= 0LL) && (3000000LL
        - (long long )j) - (long long )n >= 0LL) && (3000000LL - (long long )j) -
        (long long )r >= 0LL)) || (((((((((((((((((((((((((((((((((((((((((4 <= n
        && 4 <= r) && 4 <= i) && 8 <= j) && l <= 499997) && i <= 1000000) && j <=
        2000000) && (-12LL + (long long )i) + (long long )j >= 0LL) && (-12LL + (long
        long )j) + (long long )n >= 0LL) && (-12LL + (long long )j) + (long long )r
        >= 0LL) && (-9LL + (long long )j) + (long long )l >= 0LL) && (-8LL + (long
        long )n) + (long long )r >= 0LL) && (-8LL + (long long )i) + (long long )n
        >= 0LL) && (-8LL + (long long )i) + (long long )r >= 0LL) && (-5LL + (long
        long )l) + (long long )n >= 0LL) && (-5LL + (long long )l) + (long long )r
        >= 0LL) && (-5LL + (long long )i) + (long long )l >= 0LL) && (-4LL - (long
        long )i) + (long long )j >= 0LL) && (-3LL - (long long )l) + (long long )n
        >= 0LL) && (-3LL - (long long )l) + (long long )r >= 0LL) && (0LL - (long
        long )i) + (long long )n >= 0LL) && (4LL - (long long )n) + (long long )r
        >= 0LL) && (999999LL - (long long )i) + (long long )l >= 0LL) && (1000000LL
        - (long long )j) + (long long )n >= 0LL) && (1000000LL - (long long )j) +
        (long long )r >= 0LL) && (1999999LL - (long long )j) + (long long )l >= 0LL)
        && (-7LL + (long long )j) - (long long )l >= 0LL) && (-3LL + (long long )i)
        - (long long )l >= 0LL) && (999992LL + (long long )j) - (long long )n >= 0LL)
        && (999992LL + (long long )j) - (long long )r >= 0LL) && (999996LL + (long
        long )i) - (long long )n >= 0LL) && (999996LL + (long long )i) - (long long
        )r >= 0LL) && (1000000LL + (long long )i) - (long long )j >= 0LL) && (1499997LL
        - (long long )l) - (long long )n >= 0LL) && (1499997LL - (long long )l) -
        (long long )r >= 0LL) && (1499997LL - (long long )i) - (long long )l >= 0LL)
        && (2000000LL - (long long )i) - (long long )n >= 0LL) && (2000000LL - (long
        long )i) - (long long )r >= 0LL) && (2499997LL - (long long )j) - (long long
        )l >= 0LL) && (3000000LL - (long long )i) - (long long )j >= 0LL) && (3000000LL
        - (long long )j) - (long long )n >= 0LL) && (3000000LL - (long long )j) -
        (long long )r >= 0LL)) || (((((((((((((((((((((((((((((((((((((((((4 <= n
        && 4 <= r) && 4 <= i) && 8 <= j) && l <= 500000) && i <= 1000000) && j <=
        2000000) && (-12LL + (long long )i) + (long long )j >= 0LL) && (-12LL + (long
        long )j) + (long long )n >= 0LL) && (-12LL + (long long )j) + (long long )r
        >= 0LL) && (-9LL + (long long )j) + (long long )l >= 0LL) && (-8LL + (long
        long )n) + (long long )r >= 0LL) && (-8LL + (long long )i) + (long long )n
        >= 0LL) && (-8LL + (long long )i) + (long long )r >= 0LL) && (-5LL + (long
        long )l) + (long long )n >= 0LL) && (-5LL + (long long )l) + (long long )r
        >= 0LL) && (-5LL + (long long )i) + (long long )l >= 0LL) && (-4LL - (long
        long )i) + (long long )j >= 0LL) && (-3LL - (long long )l) + (long long )n
        >= 0LL) && (-3LL - (long long )l) + (long long )r >= 0LL) && (0LL - (long
        long )i) + (long long )n >= 0LL) && (1LL - (long long )n) + (long long )r
        >= 0LL) && (999999LL - (long long )i) + (long long )l >= 0LL) && (1000000LL
        - (long long )j) + (long long )n >= 0LL) && (1000000LL - (long long )j) +
        (long long )r >= 0LL) && (1999999LL - (long long )j) + (long long )l >= 0LL)
        && (-7LL + (long long )j) - (long long )l >= 0LL) && (-3LL + (long long )i)
        - (long long )l >= 0LL) && (999992LL + (long long )j) - (long long )n >= 0LL)
        && (999992LL + (long long )j) - (long long )r >= 0LL) && (999996LL + (long
        long )i) - (long long )n >= 0LL) && (999996LL + (long long )i) - (long long
        )r >= 0LL) && (1000000LL + (long long )i) - (long long )j >= 0LL) && (1500000LL
        - (long long )l) - (long long )n >= 0LL) && (1500000LL - (long long )l) -
        (long long )r >= 0LL) && (1500000LL - (long long )i) - (long long )l >= 0LL)
        && (2000000LL - (long long )i) - (long long )n >= 0LL) && (2000000LL - (long
        long )i) - (long long )r >= 0LL) && (2500000LL - (long long )j) - (long long
        )l >= 0LL) && (3000000LL - (long long )i) - (long long )j >= 0LL) && (3000000LL
        - (long long )j) - (long long )n >= 0LL) && (3000000LL - (long long )j) -
        (long long )r >= 0LL)) || (((((((((((((((((((((((((((((((((((((((((2 <= n
        && 2 <= r) && 2 <= i) && 4 <= j) && l <= 499997) && i <= 999995) && j <= 1999990)
        && (-6LL + (long long )i) + (long long )j >= 0LL) && (-6LL + (long long )j)
        + (long long )n >= 0LL) && (-6LL + (long long )j) + (long long )r >= 0LL)
        && (-5LL + (long long )j) + (long long )l >= 0LL) && (-4LL + (long long )n)
        + (long long )r >= 0LL) && (-4LL + (long long )i) + (long long )n >= 0LL)
        && (-4LL + (long long )i) + (long long )r >= 0LL) && (-3LL + (long long )l)
        + (long long )n >= 0LL) && (-3LL + (long long )l) + (long long )r >= 0LL)
        && (-3LL + (long long )i) + (long long )l >= 0LL) && (-2LL - (long long )i)
        + (long long )j >= 0LL) && (-1LL - (long long )l) + (long long )n >= 0LL)
        && (-1LL - (long long )l) + (long long )r >= 0LL) && (0LL - (long long )i)
        + (long long )n >= 0LL) && (4LL - (long long )n) + (long long )r >= 0LL) &&
        (499998LL - (long long )i) + (long long )l >= 0LL) && (999995LL - (long long
        )j) + (long long )n >= 0LL) && (999995LL - (long long )j) + (long long )r
        >= 0LL) && (1499993LL - (long long )j) + (long long )l >= 0LL) && (-3LL +
        (long long )j) - (long long )l >= 0LL) && (-1LL + (long long )i) - (long long
        )l >= 0LL) && (999995LL + (long long )i) - (long long )j >= 0LL) && (999996LL
        + (long long )j) - (long long )n >= 0LL) && (999996LL + (long long )j) - (long
        long )r >= 0LL) && (999998LL + (long long )i) - (long long )n >= 0LL) && (999998LL
        + (long long )i) - (long long )r >= 0LL) && (1499992LL - (long long )i) -
        (long long )l >= 0LL) && (1499997LL - (long long )l) - (long long )n >= 0LL)
        && (1499997LL - (long long )l) - (long long )r >= 0LL) && (1999995LL - (long
        long )i) - (long long )n >= 0LL) && (1999995LL - (long long )i) - (long long
        )r >= 0LL) && (2499987LL - (long long )j) - (long long )l >= 0LL) && (2999985LL
        - (long long )i) - (long long )j >= 0LL) && (2999990LL - (long long )j) -
        (long long )n >= 0LL) && (2999990LL - (long long )j) - (long long )r >= 0LL))
        || (((((((((((((((((((((((((((((((((((((((((2 <= n && 2 <= r) && 2 <= i) &&
        4 <= j) && l <= 500000) && i <= 1000000) && j <= 2000000) && (-6LL + (long
        long )i) + (long long )j >= 0LL) && (-6LL + (long long )j) + (long long )n
        >= 0LL) && (-6LL + (long long )j) + (long long )r >= 0LL) && (-5LL + (long
        long )j) + (long long )l >= 0LL) && (-4LL + (long long )n) + (long long )r
        >= 0LL) && (-4LL + (long long )i) + (long long )n >= 0LL) && (-4LL + (long
        long )i) + (long long )r >= 0LL) && (-3LL + (long long )l) + (long long )n
        >= 0LL) && (-3LL + (long long )l) + (long long )r >= 0LL) && (-3LL + (long
        long )i) + (long long )l >= 0LL) && (-2LL - (long long )i) + (long long )j
        >= 0LL) && (-1LL - (long long )l) + (long long )n >= 0LL) && (-1LL - (long
        long )l) + (long long )r >= 0LL) && (0LL - (long long )i) + (long long )n
        >= 0LL) && (1LL - (long long )n) + (long long )r >= 0LL) && (500001LL - (long
        long )i) + (long long )l >= 0LL) && (1000000LL - (long long )j) + (long long
        )n >= 0LL) && (1000000LL - (long long )j) + (long long )r >= 0LL) && (1500001LL
        - (long long )j) + (long long )l >= 0LL) && (-3LL + (long long )j) - (long
        long )l >= 0LL) && (-1LL + (long long )i) - (long long )l >= 0LL) && (999996LL
        + (long long )j) - (long long )n >= 0LL) && (999996LL + (long long )j) - (long
        long )r >= 0LL) && (999998LL + (long long )i) - (long long )n >= 0LL) && (999998LL
        + (long long )i) - (long long )r >= 0LL) && (1000000LL + (long long )i) -
        (long long )j >= 0LL) && (1500000LL - (long long )l) - (long long )n >= 0LL)
        && (1500000LL - (long long )l) - (long long )r >= 0LL) && (1500000LL - (long
        long )i) - (long long )l >= 0LL) && (2000000LL - (long long )i) - (long long
        )n >= 0LL) && (2000000LL - (long long )i) - (long long )r >= 0LL) && (2500000LL
        - (long long )j) - (long long )l >= 0LL) && (3000000LL - (long long )i) -
        (long long )j >= 0LL) && (3000000LL - (long long )j) - (long long )n >= 0LL)
        && (3000000LL - (long long )j) - (long long )r >= 0LL)) || ((((((((((((((((((((((((((((((((((((((((((1
        <= i && 2 <= n) && 2 <= r) && 2 <= j) && l <= 499997) && i <= 499997) && j
        <= 999994) && (-4LL + (long long )n) + (long long )r >= 0LL) && (-4LL + (long
        long )j) + (long long )n >= 0LL) && (-4LL + (long long )j) + (long long )r
        >= 0LL) && (-3LL + (long long )l) + (long long )n >= 0LL) && (-3LL + (long
        long )l) + (long long )r >= 0LL) && (-3LL + (long long )i) + (long long )n
        >= 0LL) && (-3LL + (long long )i) + (long long )r >= 0LL) && (-3LL + (long
        long )i) + (long long )j >= 0LL) && (-3LL + (long long )j) + (long long )l
        >= 0LL) && (-2LL + (long long )i) + (long long )l >= 0LL) && (-1LL - (long
        long )l) + (long long )n >= 0LL) && (-1LL - (long long )i) + (long long )n
        >= 0LL) && (-1LL - (long long )i) + (long long )j >= 0LL) && (0LL - (long
        long )l) + (long long )r >= 0LL) && (0LL - (long long )i) + (long long )l
        >= 0LL) && (4LL - (long long )n) + (long long )r >= 0LL) && (499996LL - (long
        long )j) + (long long )n >= 0LL) && (499997LL - (long long )j) + (long long
        )l >= 0LL) && (499997LL - (long long )j) + (long long )r >= 0LL) && (-1LL
        + (long long )j) - (long long )l >= 0LL) && (499997LL + (long long )i) - (long
        long )j >= 0LL) && (999998LL + (long long )j) - (long long )n >= 0LL) && (999998LL
        + (long long )j) - (long long )r >= 0LL) && (999999LL + (long long )i) - (long
        long )n >= 0LL) && (999999LL + (long long )i) - (long long )r >= 0LL) && (999994LL
        - (long long )i) - (long long )l >= 0LL) && (1499991LL - (long long )i) -
        (long long )j >= 0LL) && (1499991LL - (long long )j) - (long long )l >= 0LL)
        && (1499997LL - (long long )l) - (long long )n >= 0LL) && (1499997LL - (long
        long )l) - (long long )r >= 0LL) && (1499997LL - (long long )i) - (long long
        )n >= 0LL) && (1499997LL - (long long )i) - (long long )r >= 0LL) && (1999994LL
        - (long long )j) - (long long )n >= 0LL) && (1999994LL - (long long )j) -
        (long long )r >= 0LL) && (long long )i - (long long )l >= 0LL) && l == i)))
        || (((((((((((((((((((((((((((((((((((((((((((1 <= n && 1 <= i) && 2 <= r)
        && 2 <= j) && l <= 500000) && i <= 500000) && j <= 1000000) && (-4LL + (long
        long )n) + (long long )r >= 0LL) && (-4LL + (long long )j) + (long long )n
        >= 0LL) && (-4LL + (long long )j) + (long long )r >= 0LL) && (-3LL + (long
        long )l) + (long long )n >= 0LL) && (-3LL + (long long )l) + (long long )r
        >= 0LL) && (-3LL + (long long )i) + (long long )n >= 0LL) && (-3LL + (long
        long )i) + (long long )r >= 0LL) && (-3LL + (long long )i) + (long long )j
        >= 0LL) && (-3LL + (long long )j) + (long long )l >= 0LL) && (-2LL + (long
        long )i) + (long long )l >= 0LL) && (-1LL - (long long )i) + (long long )j
        >= 0LL) && (0LL - (long long )i) + (long long )l >= 0LL) && (1LL - (long long
        )n) + (long long )r >= 0LL) && (499998LL - (long long )l) + (long long )n
        >= 0LL) && (499998LL - (long long )l) + (long long )r >= 0LL) && (499998LL
        - (long long )i) + (long long )n >= 0LL) && (499998LL - (long long )i) + (long
        long )r >= 0LL) && (500000LL - (long long )j) + (long long )l >= 0LL) && (999998LL
        - (long long )j) + (long long )n >= 0LL) && (999998LL - (long long )j) + (long
        long )r >= 0LL) && (-1LL + (long long )j) - (long long )l >= 0LL) && (500000LL
        + (long long )i) - (long long )j >= 0LL) && (999998LL + (long long )j) - (long
        long )n >= 0LL) && (999998LL + (long long )j) - (long long )r >= 0LL) && (999999LL
        + (long long )i) - (long long )n >= 0LL) && (999999LL + (long long )i) - (long
        long )r >= 0LL) && (1000000LL - (long long )i) - (long long )l >= 0LL) &&
        (1500000LL - (long long )l) - (long long )n >= 0LL) && (1500000LL - (long
        long )l) - (long long )r >= 0LL) && (1500000LL - (long long )i) - (long long
        )n >= 0LL) && (1500000LL - (long long )i) - (long long )r >= 0LL) && (1500000LL
        - (long long )i) - (long long )j >= 0LL) && (1500000LL - (long long )j) -
        (long long )l >= 0LL) && (2000000LL - (long long )j) - (long long )n >= 0LL)
        && (2000000LL - (long long )j) - (long long )r >= 0LL) && (long long )i -
        (long long )l >= 0LL) && l == i)) || ((((((((((((((((((((((((((((((((((((((((((16
        <= n && 16 <= r) && 16 <= i) && 32 <= j) && l <= 499998) && i <= 1000000)
        && j <= 2000000) && (-48LL + (long long )i) + (long long )j >= 0LL) && (-48LL
        + (long long )j) + (long long )n >= 0LL) && (-48LL + (long long )j) + (long
        long )r >= 0LL) && (-33LL + (long long )j) + (long long )l >= 0LL) && (-32LL
        + (long long )n) + (long long )r >= 0LL) && (-32LL + (long long )i) + (long
        long )n >= 0LL) && (-32LL + (long long )i) + (long long )r >= 0LL) && (-17LL
        + (long long )l) + (long long )n >= 0LL) && (-17LL + (long long )l) + (long
        long )r >= 0LL) && (-17LL + (long long )i) + (long long )l >= 0LL) && (-16LL
        - (long long )i) + (long long )j >= 0LL) && (-15LL - (long long )l) + (long
        long )n >= 0LL) && (-15LL - (long long )l) + (long long )r >= 0LL) && (0LL
        - (long long )i) + (long long )n >= 0LL) && (0LL - (long long )i) + (long
        long )r >= 0LL) && (3LL - (long long )n) + (long long )r >= 0LL) && (999999LL
        - (long long )i) + (long long )l >= 0LL) && (1000000LL - (long long )j) +
        (long long )n >= 0LL) && (1000000LL - (long long )j) + (long long )r >= 0LL)
        && (1999999LL - (long long )j) + (long long )l >= 0LL) && (-31LL + (long long
        )j) - (long long )l >= 0LL) && (-15LL + (long long )i) - (long long )l >=
        0LL) && (999968LL + (long long )j) - (long long )n >= 0LL) && (999968LL +
        (long long )j) - (long long )r >= 0LL) && (999984LL + (long long )i) - (long
        long )n >= 0LL) && (999984LL + (long long )i) - (long long )r >= 0LL) && (1000000LL
        + (long long )i) - (long long )j >= 0LL) && (1499998LL - (long long )l) -
        (long long )n >= 0LL) && (1499998LL - (long long )l) - (long long )r >= 0LL)
        && (1499998LL - (long long )i) - (long long )l >= 0LL) && (2000000LL - (long
        long )i) - (long long )n >= 0LL) && (2000000LL - (long long )i) - (long long
        )r >= 0LL) && (2499998LL - (long long )j) - (long long )l >= 0LL) && (3000000LL
        - (long long )i) - (long long )j >= 0LL) && (3000000LL - (long long )j) -
        (long long )n >= 0LL) && (3000000LL - (long long )j) - (long long )r >= 0LL)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-invgen/heapsort.i
        line: 35
        column: 3
        function: main
      value: 1 <= l
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-invgen/heapsort.i
        line: 35
        column: 3
        function: main
      value: n <= 1000000
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-invgen/heapsort.i
        line: 35
        column: 3
        function: main
      value: r <= 1000000
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-invgen/heapsort.i
        line: 35
        column: 3
        function: main
      value: (999999LL + (long long )l) - (long long )n >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-invgen/heapsort.i
        line: 35
        column: 3
        function: main
      value: (999999LL + (long long )l) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-invgen/heapsort.i
        line: 35
        column: 3
        function: main
      value: (2000000LL - (long long )n) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-invgen/heapsort.i
        line: 35
        column: 3
        function: main
      value: (long long )n - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-invgen/heapsort.i
        line: 35
        column: 3
        function: main
      value: (((((((((((((((((((((((((((((((((((1 <= r && 1 <= i) && 2 <= n) && 2
        <= j) && i <= 1000000) && j <= 2000000) && (-4LL + (long long )j) + (long
        long )n >= 0LL) && (-3LL + (long long )n) + (long long )r >= 0LL) && (-3LL
        + (long long )l) + (long long )n >= 0LL) && (-3LL + (long long )i) + (long
        long )n >= 0LL) && (-3LL + (long long )i) + (long long )j >= 0LL) && (-3LL
        + (long long )j) + (long long )l >= 0LL) && (-3LL + (long long )j) + (long
        long )r >= 0LL) && (-2LL + (long long )l) + (long long )r >= 0LL) && (-2LL
        + (long long )i) + (long long )l >= 0LL) && (-2LL + (long long )i) + (long
        long )r >= 0LL) && (-1LL - (long long )l) + (long long )n >= 0LL) && (-1LL
        - (long long )i) + (long long )j >= 0LL) && (0LL - (long long )l) + (long
        long )r >= 0LL) && (999999LL - (long long )i) + (long long )l >= 0LL) && (1000000LL
        - (long long )j) + (long long )n >= 0LL) && (1000001LL - (long long )j) +
        (long long )r >= 0LL) && (1999999LL - (long long )j) + (long long )l >= 0LL)
        && (-1LL + (long long )j) - (long long )l >= 0LL) && (999997LL + (long long
        )j) - (long long )r >= 0LL) && (999998LL + (long long )i) - (long long )r
        >= 0LL) && (999998LL + (long long )j) - (long long )n >= 0LL) && (999999LL
        + (long long )i) - (long long )n >= 0LL) && (1000000LL + (long long )i) -
        (long long )j >= 0LL) && (2000000LL - (long long )i) - (long long )n >= 0LL)
        && (2000000LL - (long long )i) - (long long )r >= 0LL) && (3000000LL - (long
        long )i) - (long long )j >= 0LL) && (3000000LL - (long long )j) - (long long
        )n >= 0LL) && (3000000LL - (long long )j) - (long long )r >= 0LL) && (long
        long )i - (long long )l >= 0LL) && (((((0LL - (long long )i) + (long long
        )n >= 0LL && (1LL - (long long )i) + (long long )r >= 0LL) && ((((((l <= 499998
        && (3LL - (long long )n) + (long long )r >= 0LL) && (1499998LL - (long long
        )l) - (long long )n >= 0LL) && (1499998LL - (long long )l) - (long long )r
        >= 0LL) && (1499998LL - (long long )i) - (long long )l >= 0LL) && (2499998LL
        - (long long )j) - (long long )l >= 0LL) || (((((l <= 499996 && (999999LL
        - (long long )n) + (long long )r >= 0LL) && (1499996LL - (long long )l) -
        (long long )n >= 0LL) && (1499996LL - (long long )l) - (long long )r >= 0LL)
        && (1499996LL - (long long )i) - (long long )l >= 0LL) && (2499996LL - (long
        long )j) - (long long )l >= 0LL))) || (((((((l <= 499999 && (2LL - (long long
        )n) + (long long )r >= 0LL) && (499998LL - (long long )i) + (long long )n
        >= 0LL) && (499999LL - (long long )i) + (long long )r >= 0LL) && (1499999LL
        - (long long )l) - (long long )n >= 0LL) && (1499999LL - (long long )l) -
        (long long )r >= 0LL) && (1499999LL - (long long )i) - (long long )l >= 0LL)
        && (2499999LL - (long long )j) - (long long )l >= 0LL)) || (((((((l <= 499997
        && (0LL - (long long )i) + (long long )n >= 0LL) && (1LL - (long long )i)
        + (long long )r >= 0LL) && (4LL - (long long )n) + (long long )r >= 0LL) &&
        (1499997LL - (long long )l) - (long long )n >= 0LL) && (1499997LL - (long
        long )l) - (long long )r >= 0LL) && (1499997LL - (long long )i) - (long long
        )l >= 0LL) && (2499997LL - (long long )j) - (long long )l >= 0LL))) || ((((((((((((((((((((((((((((((((((((((0
        <= r && 1 <= n) && l <= 500000) && (-2LL + (long long )l) + (long long )n
        >= 0LL) && (-1LL + (long long )n) + (long long )r >= 0LL) && (-1LL + (long
        long )l) + (long long )r >= 0LL) && (2147483647LL + (long long )i) + (long
        long )n >= 0LL) && (2147483647LL + (long long )i) + (long long )l >= 0LL)
        && (2147483647LL + (long long )j) + (long long )n >= 0LL) && (2147483647LL
        + (long long )j) + (long long )l >= 0LL) && (2147483648LL + (long long )i)
        + (long long )r >= 0LL) && (2147483648LL + (long long )j) + (long long )r
        >= 0LL) && (4294967296LL + (long long )i) + (long long )j >= 0LL) && (1LL
        - (long long )n) + (long long )r >= 0LL) && (499999LL - (long long )l) + (long
        long )n >= 0LL) && (499999LL - (long long )l) + (long long )r >= 0LL) && (2147483646LL
        - (long long )i) + (long long )n >= 0LL) && (2147483646LL - (long long )i)
        + (long long )l >= 0LL) && (2147483646LL - (long long )j) + (long long )n
        >= 0LL) && (2147483646LL - (long long )j) + (long long )l >= 0LL) && (2147483647LL
        - (long long )i) + (long long )r >= 0LL) && (2147483647LL - (long long )j)
        + (long long )r >= 0LL) && (4294967295LL - (long long )i) + (long long )j
        >= 0LL) && (2147983648LL + (long long )i) - (long long )l >= 0LL) && (2147983648LL
        + (long long )j) - (long long )l >= 0LL) && (2148483648LL + (long long )i)
        - (long long )n >= 0LL) && (2148483648LL + (long long )i) - (long long )r
        >= 0LL) && (2148483648LL + (long long )j) - (long long )n >= 0LL) && (2148483648LL
        + (long long )j) - (long long )r >= 0LL) && (4294967295LL + (long long )i)
        - (long long )j >= 0LL) && (1500000LL - (long long )l) - (long long )n >=
        0LL) && (1500000LL - (long long )l) - (long long )r >= 0LL) && (2147983647LL
        - (long long )i) - (long long )l >= 0LL) && (2147983647LL - (long long )j)
        - (long long )l >= 0LL) && (2148483647LL - (long long )i) - (long long )n
        >= 0LL) && (2148483647LL - (long long )i) - (long long )r >= 0LL) && (2148483647LL
        - (long long )j) - (long long )n >= 0LL) && (2148483647LL - (long long )j)
        - (long long )r >= 0LL) && (4294967294LL - (long long )i) - (long long )j
        >= 0LL)
      format: c_expression
