- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 51c2f5e0-d10c-4b00-a145-d035e868b510
    creation_time: 2025-03-22T16:54:54Z
    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'' ''64bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-numeric/Binomial.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-numeric/Binomial.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-numeric/Binomial.c: c204b56aba09d3ce87e17edffdff1d33aa0b4dc87a1e1140339548dffa982588
      data_model: LP64
      language: C
      specification: CHECK( init(main()), LTL(F end) )
  content:
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-numeric/Binomial.c
        line: 41
        column: 2
        function: main
      value: 0 <= y
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-numeric/Binomial.c
        line: 41
        column: 2
        function: main
      value: (2147483648LL + (long long )y) + (long long )z >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-numeric/Binomial.c
        line: 41
        column: 2
        function: main
      value: (4294967295LL - (long long )y) + (long long )z >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-numeric/Binomial.c
        line: 41
        column: 2
        function: main
      value: (2147483647LL + (long long )y) - (long long )z >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-numeric/Binomial.c
        line: 41
        column: 2
        function: main
      value: (4294967294LL - (long long )y) - (long long )z >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-numeric/Binomial.c
        line: 41
        column: 2
        function: main
      value: (((((((x <= 2147483639 && k <= 2147483640) && (1LL - (long long )n) +
        (long long )x >= 0LL) && (1LL - (long long )k) + (long long )x >= 0LL) &&
        (-1LL + (long long )k) - (long long )x >= 0LL) && (long long )k - (long long
        )n >= 0LL) && ((((((((((((((((((((((((((((((((((((0 <= x && 1 <= k) && (-2LL
        + (long long )k) + (long long )n >= 0LL) && (-1LL + (long long )n) + (long
        long )x >= 0LL) && (-1LL + (long long )n) + (long long )y >= 0LL) && (-1LL
        + (long long )k) + (long long )x >= 0LL) && (-1LL + (long long )k) + (long
        long )y >= 0LL) && (2147483647LL + (long long )n) + (long long )z >= 0LL)
        && (2147483647LL + (long long )k) + (long long )z >= 0LL) && (2147483648LL
        + (long long )x) + (long long )z >= 0LL) && (1LL - (long long )n) + (long
        long )y >= 0LL) && (2147483647LL - (long long )x) + (long long )y >= 0LL)
        && (2147483647LL - (long long )k) + (long long )n >= 0LL) && (2147483648LL
        - (long long )k) + (long long )y >= 0LL) && (2147483649LL - (long long )n)
        + (long long )z >= 0LL) && (4294967295LL - (long long )x) + (long long )z
        >= 0LL) && (4294967296LL - (long long )k) + (long long )z >= 0LL) && (long
        long )x + (long long )y >= 0LL) && (2147483646LL + (long long )n) - (long
        long )x >= 0LL) && (2147483646LL + (long long )n) - (long long )y >= 0LL)
        && (2147483646LL + (long long )n) - (long long )z >= 0LL) && (2147483646LL
        + (long long )k) - (long long )y >= 0LL) && (2147483646LL + (long long )k)
        - (long long )z >= 0LL) && (2147483647LL + (long long )x) - (long long )y
        >= 0LL) && (2147483647LL + (long long )x) - (long long )z >= 0LL) && (2147483648LL
        - (long long )n) - (long long )x >= 0LL) && (2147483648LL - (long long )n)
        - (long long )y >= 0LL) && (2147483648LL - (long long )n) - (long long )z
        >= 0LL) && (2147483649LL - (long long )k) - (long long )n >= 0LL) && (4294967294LL
        - (long long )x) - (long long )y >= 0LL) && (4294967294LL - (long long )x)
        - (long long )z >= 0LL) && (4294967295LL - (long long )k) - (long long )x
        >= 0LL) && (4294967295LL - (long long )k) - (long long )y >= 0LL) && (4294967295LL
        - (long long )k) - (long long )z >= 0LL) && n == 1) || ((((((((((((((((((((((((((((((((((1
        <= x && 2 <= k) && (-4LL + (long long )k) + (long long )n >= 0LL) && (-3LL
        + (long long )n) + (long long )x >= 0LL) && (-3LL + (long long )k) + (long
        long )x >= 0LL) && (-2LL + (long long )n) + (long long )y >= 0LL) && (-2LL
        + (long long )k) + (long long )y >= 0LL) && (-1LL + (long long )x) + (long
        long )y >= 0LL) && (2147483646LL + (long long )n) + (long long )z >= 0LL)
        && (2147483646LL + (long long )k) + (long long )z >= 0LL) && (2147483647LL
        + (long long )x) + (long long )z >= 0LL) && (2LL - (long long )n) + (long
        long )y >= 0LL) && (2147483638LL - (long long )k) + (long long )n >= 0LL)
        && (2147483639LL - (long long )x) + (long long )y >= 0LL) && (2147483640LL
        - (long long )k) + (long long )y >= 0LL) && (2147483650LL - (long long )n)
        + (long long )z >= 0LL) && (4294967287LL - (long long )x) + (long long )z
        >= 0LL) && (4294967288LL - (long long )k) + (long long )z >= 0LL) && (2147483637LL
        + (long long )n) - (long long )x >= 0LL) && (2147483645LL + (long long )n)
        - (long long )y >= 0LL) && (2147483645LL + (long long )n) - (long long )z
        >= 0LL) && (2147483645LL + (long long )k) - (long long )y >= 0LL) && (2147483645LL
        + (long long )k) - (long long )z >= 0LL) && (2147483646LL + (long long )x)
        - (long long )y >= 0LL) && (2147483646LL + (long long )x) - (long long )z
        >= 0LL) && (2147483641LL - (long long )n) - (long long )x >= 0LL) && (2147483642LL
        - (long long )k) - (long long )n >= 0LL) && (2147483649LL - (long long )n)
        - (long long )y >= 0LL) && (2147483649LL - (long long )n) - (long long )z
        >= 0LL) && (4294967279LL - (long long )k) - (long long )x >= 0LL) && (4294967286LL
        - (long long )x) - (long long )y >= 0LL) && (4294967286LL - (long long )x)
        - (long long )z >= 0LL) && (4294967287LL - (long long )k) - (long long )y
        >= 0LL) && (4294967287LL - (long long )k) - (long long )z >= 0LL) && n ==
        2)) || ((((((((((((((((((((((((((((((((((2 <= x && 3 <= k) && (-6LL + (long
        long )k) + (long long )n >= 0LL) && (-5LL + (long long )n) + (long long )x
        >= 0LL) && (-5LL + (long long )k) + (long long )x >= 0LL) && (-3LL + (long
        long )n) + (long long )y >= 0LL) && (-3LL + (long long )k) + (long long )y
        >= 0LL) && (-2LL + (long long )x) + (long long )y >= 0LL) && (2147483645LL
        + (long long )n) + (long long )z >= 0LL) && (2147483645LL + (long long )k)
        + (long long )z >= 0LL) && (2147483646LL + (long long )x) + (long long )z
        >= 0LL) && (3LL - (long long )n) + (long long )y >= 0LL) && (2147483637LL
        - (long long )k) + (long long )n >= 0LL) && (2147483639LL - (long long )x)
        + (long long )y >= 0LL) && (2147483640LL - (long long )k) + (long long )y
        >= 0LL) && (2147483651LL - (long long )n) + (long long )z >= 0LL) && (4294967287LL
        - (long long )x) + (long long )z >= 0LL) && (4294967288LL - (long long )k)
        + (long long )z >= 0LL) && (2147483636LL + (long long )n) - (long long )x
        >= 0LL) && (2147483644LL + (long long )n) - (long long )y >= 0LL) && (2147483644LL
        + (long long )n) - (long long )z >= 0LL) && (2147483644LL + (long long )k)
        - (long long )y >= 0LL) && (2147483644LL + (long long )k) - (long long )z
        >= 0LL) && (2147483645LL + (long long )x) - (long long )y >= 0LL) && (2147483645LL
        + (long long )x) - (long long )z >= 0LL) && (2147483642LL - (long long )n)
        - (long long )x >= 0LL) && (2147483643LL - (long long )k) - (long long )n
        >= 0LL) && (2147483650LL - (long long )n) - (long long )y >= 0LL) && (2147483650LL
        - (long long )n) - (long long )z >= 0LL) && (4294967279LL - (long long )k)
        - (long long )x >= 0LL) && (4294967286LL - (long long )x) - (long long )y
        >= 0LL) && (4294967286LL - (long long )x) - (long long )z >= 0LL) && (4294967287LL
        - (long long )k) - (long long )y >= 0LL) && (4294967287LL - (long long )k)
        - (long long )z >= 0LL) && n == 3))) || ((((((((((((((((((((((((((((((((((((((0
        <= x && (2147483648LL + (long long )x) + (long long )z >= 0LL) && (2147483648LL
        + (long long )n) + (long long )z >= 0LL) && (2147483648LL + (long long )k)
        + (long long )x >= 0LL) && (2147483648LL + (long long )k) + (long long )y
        >= 0LL) && (2147483648LL + (long long )k) + (long long )n >= 0LL) && (4294967296LL
        + (long long )k) + (long long )z >= 0LL) && (0LL - (long long )n) + (long
        long )x >= 0LL) && (0LL - (long long )n) + (long long )y >= 0LL) && (2147483647LL
        - (long long )x) + (long long )y >= 0LL) && (2147483647LL - (long long )k)
        + (long long )x >= 0LL) && (2147483647LL - (long long )k) + (long long )y
        >= 0LL) && (2147483647LL - (long long )k) + (long long )n >= 0LL) && (2147483648LL
        - (long long )n) + (long long )z >= 0LL) && (4294967295LL - (long long )x)
        + (long long )z >= 0LL) && (4294967295LL - (long long )k) + (long long )z
        >= 0LL) && (long long )x + (long long )y >= 0LL) && (long long )n + (long
        long )x >= 0LL) && (long long )n + (long long )y >= 0LL) && (2147483647LL
        + (long long )x) - (long long )y >= 0LL) && (2147483647LL + (long long )x)
        - (long long )z >= 0LL) && (2147483647LL + (long long )n) - (long long )x
        >= 0LL) && (2147483647LL + (long long )n) - (long long )y >= 0LL) && (2147483647LL
        + (long long )n) - (long long )z >= 0LL) && (2147483648LL + (long long )k)
        - (long long )n >= 0LL) && (4294967295LL + (long long )k) - (long long )x
        >= 0LL) && (4294967295LL + (long long )k) - (long long )y >= 0LL) && (4294967295LL
        + (long long )k) - (long long )z >= 0LL) && (2147483647LL - (long long )n)
        - (long long )x >= 0LL) && (2147483647LL - (long long )n) - (long long )y
        >= 0LL) && (2147483647LL - (long long )n) - (long long )z >= 0LL) && (2147483647LL
        - (long long )k) - (long long )n >= 0LL) && (4294967294LL - (long long )x)
        - (long long )y >= 0LL) && (4294967294LL - (long long )x) - (long long )z
        >= 0LL) && (4294967294LL - (long long )k) - (long long )x >= 0LL) && (4294967294LL
        - (long long )k) - (long long )y >= 0LL) && (4294967294LL - (long long )k)
        - (long long )z >= 0LL) && 0 == n) && n == 0)) || (((((((((((((((((((((((((((((((((((((((((3
        <= x && 4 <= n) && 4 <= k) && x <= 2147483639) && n <= 2147483628) && k <=
        2147483640) && (-8LL + (long long )k) + (long long )n >= 0LL) && (-7LL + (long
        long )n) + (long long )x >= 0LL) && (-7LL + (long long )k) + (long long )x
        >= 0LL) && (-4LL + (long long )n) + (long long )y >= 0LL) && (-4LL + (long
        long )k) + (long long )y >= 0LL) && (-3LL + (long long )x) + (long long )y
        >= 0LL) && (2147483644LL + (long long )n) + (long long )z >= 0LL) && (2147483644LL
        + (long long )k) + (long long )z >= 0LL) && (2147483645LL + (long long )x)
        + (long long )z >= 0LL) && (1LL - (long long )n) + (long long )x >= 0LL) &&
        (1LL - (long long )k) + (long long )x >= 0LL) && (2147483628LL - (long long
        )n) + (long long )y >= 0LL) && (2147483636LL - (long long )k) + (long long
        )n >= 0LL) && (2147483639LL - (long long )x) + (long long )y >= 0LL) && (2147483640LL
        - (long long )k) + (long long )y >= 0LL) && (4294967276LL - (long long )n)
        + (long long )z >= 0LL) && (4294967287LL - (long long )x) + (long long )z
        >= 0LL) && (4294967288LL - (long long )k) + (long long )z >= 0LL) && (-1LL
        + (long long )k) - (long long )x >= 0LL) && (2147483635LL + (long long )n)
        - (long long )x >= 0LL) && (2147483643LL + (long long )n) - (long long )y
        >= 0LL) && (2147483643LL + (long long )n) - (long long )z >= 0LL) && (2147483643LL
        + (long long )k) - (long long )y >= 0LL) && (2147483643LL + (long long )k)
        - (long long )z >= 0LL) && (2147483644LL + (long long )x) - (long long )y
        >= 0LL) && (2147483644LL + (long long )x) - (long long )z >= 0LL) && (4294967255LL
        - (long long )n) - (long long )x >= 0LL) && (4294967256LL - (long long )k)
        - (long long )n >= 0LL) && (4294967275LL - (long long )n) - (long long )y
        >= 0LL) && (4294967275LL - (long long )n) - (long long )z >= 0LL) && (4294967279LL
        - (long long )k) - (long long )x >= 0LL) && (4294967286LL - (long long )x)
        - (long long )y >= 0LL) && (4294967286LL - (long long )x) - (long long )z
        >= 0LL) && (4294967287LL - (long long )k) - (long long )y >= 0LL) && (4294967287LL
        - (long long )k) - (long long )z >= 0LL) && (long long )k - (long long )n
        >= 0LL)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-numeric/Binomial.c
        line: 42
        column: 6
        function: main
      value: 0 <= y
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-numeric/Binomial.c
        line: 42
        column: 6
        function: main
      value: (2147483648LL + (long long )y) + (long long )z >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-numeric/Binomial.c
        line: 42
        column: 6
        function: main
      value: (4294967295LL - (long long )y) + (long long )z >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-numeric/Binomial.c
        line: 42
        column: 6
        function: main
      value: (2147483647LL + (long long )y) - (long long )z >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-numeric/Binomial.c
        line: 42
        column: 6
        function: main
      value: (4294967294LL - (long long )y) - (long long )z >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-numeric/Binomial.c
        line: 42
        column: 6
        function: main
      value: (((((((((((((((((((((((x <= 2147483639 && (0LL - (long long )n) + (long
        long )x >= 0LL) && (((((((((((((((((((((((((((((((((((((((2 <= x && (-4LL
        + (long long )n) + (long long )x >= 0LL) && (-4LL + (long long )k) + (long
        long )x >= 0LL) && (-4LL + (long long )k) + (long long )n >= 0LL) && (-2LL
        + (long long )x) + (long long )y >= 0LL) && (-2LL + (long long )n) + (long
        long )y >= 0LL) && (-2LL + (long long )k) + (long long )y >= 0LL) && (2147483646LL
        + (long long )x) + (long long )z >= 0LL) && (2147483646LL + (long long )n)
        + (long long )z >= 0LL) && (2147483646LL + (long long )k) + (long long )z
        >= 0LL) && (0LL - (long long )k) + (long long )x >= 0LL) && (0LL - (long long
        )k) + (long long )n >= 0LL) && (2LL - (long long )n) + (long long )y >= 0LL)
        && (2LL - (long long )k) + (long long )y >= 0LL) && (2147483639LL - (long
        long )x) + (long long )y >= 0LL) && (2147483650LL - (long long )n) + (long
        long )z >= 0LL) && (2147483650LL - (long long )k) + (long long )z >= 0LL)
        && (4294967287LL - (long long )x) + (long long )z >= 0LL) && (2147483637LL
        + (long long )n) - (long long )x >= 0LL) && (2147483637LL + (long long )k)
        - (long long )x >= 0LL) && (2147483645LL + (long long )x) - (long long )y
        >= 0LL) && (2147483645LL + (long long )x) - (long long )z >= 0LL) && (2147483645LL
        + (long long )n) - (long long )y >= 0LL) && (2147483645LL + (long long )n)
        - (long long )z >= 0LL) && (2147483645LL + (long long )k) - (long long )y
        >= 0LL) && (2147483645LL + (long long )k) - (long long )z >= 0LL) && (4LL
        - (long long )k) - (long long )n >= 0LL) && (2147483641LL - (long long )n)
        - (long long )x >= 0LL) && (2147483641LL - (long long )k) - (long long )x
        >= 0LL) && (2147483649LL - (long long )n) - (long long )y >= 0LL) && (2147483649LL
        - (long long )n) - (long long )z >= 0LL) && (2147483649LL - (long long )k)
        - (long long )y >= 0LL) && (2147483649LL - (long long )k) - (long long )z
        >= 0LL) && (4294967286LL - (long long )x) - (long long )y >= 0LL) && (4294967286LL
        - (long long )x) - (long long )z >= 0LL) && (long long )k - (long long )n
        >= 0LL) && n == 2) && k == 2) || ((((((((((((((((((((((((((((((((((((((3 <=
        x && 4 <= k) && k <= 2147483640) && (-7LL + (long long )k) + (long long )x
        >= 0LL) && (-7LL + (long long )k) + (long long )n >= 0LL) && (-6LL + (long
        long )n) + (long long )x >= 0LL) && (-4LL + (long long )k) + (long long )y
        >= 0LL) && (-3LL + (long long )x) + (long long )y >= 0LL) && (-3LL + (long
        long )n) + (long long )y >= 0LL) && (2147483644LL + (long long )k) + (long
        long )z >= 0LL) && (2147483645LL + (long long )x) + (long long )z >= 0LL)
        && (2147483645LL + (long long )n) + (long long )z >= 0LL) && (1LL - (long
        long )k) + (long long )x >= 0LL) && (3LL - (long long )n) + (long long )y
        >= 0LL) && (2147483637LL - (long long )k) + (long long )n >= 0LL) && (2147483640LL
        - (long long )k) + (long long )y >= 0LL) && (2147483647LL - (long long )x)
        + (long long )y >= 0LL) && (2147483651LL - (long long )n) + (long long )z
        >= 0LL) && (4294967288LL - (long long )k) + (long long )z >= 0LL) && (4294967295LL
        - (long long )x) + (long long )z >= 0LL) && (-1LL + (long long )k) - (long
        long )n >= 0LL) && (2147483641LL + (long long )k) - (long long )x >= 0LL)
        && (2147483643LL + (long long )k) - (long long )y >= 0LL) && (2147483643LL
        + (long long )k) - (long long )z >= 0LL) && (2147483644LL + (long long )x)
        - (long long )y >= 0LL) && (2147483644LL + (long long )x) - (long long )z
        >= 0LL) && (2147483644LL + (long long )n) - (long long )x >= 0LL) && (2147483644LL
        + (long long )n) - (long long )y >= 0LL) && (2147483644LL + (long long )n)
        - (long long )z >= 0LL) && (2147483643LL - (long long )k) - (long long )n
        >= 0LL) && (2147483650LL - (long long )n) - (long long )x >= 0LL) && (2147483650LL
        - (long long )n) - (long long )y >= 0LL) && (2147483650LL - (long long )n)
        - (long long )z >= 0LL) && (4294967287LL - (long long )k) - (long long )x
        >= 0LL) && (4294967287LL - (long long )k) - (long long )y >= 0LL) && (4294967287LL
        - (long long )k) - (long long )z >= 0LL) && (4294967294LL - (long long )x)
        - (long long )y >= 0LL) && (4294967294LL - (long long )x) - (long long )z
        >= 0LL) && n == 3)) || (((((((((((((((((((((((((((((((((((((2 <= x && (-4LL
        + (long long )n) + (long long )x >= 0LL) && (-3LL + (long long )k) + (long
        long )x >= 0LL) && (-3LL + (long long )k) + (long long )n >= 0LL) && (-2LL
        + (long long )x) + (long long )y >= 0LL) && (-2LL + (long long )n) + (long
        long )y >= 0LL) && (-1LL + (long long )k) + (long long )y >= 0LL) && (2147483646LL
        + (long long )x) + (long long )z >= 0LL) && (2147483646LL + (long long )n)
        + (long long )z >= 0LL) && (2147483647LL + (long long )k) + (long long )z
        >= 0LL) && (-1LL - (long long )k) + (long long )x >= 0LL) && (-1LL - (long
        long )k) + (long long )n >= 0LL) && (1LL - (long long )k) + (long long )y
        >= 0LL) && (2LL - (long long )n) + (long long )y >= 0LL) && (2147483639LL
        - (long long )x) + (long long )y >= 0LL) && (2147483649LL - (long long )k)
        + (long long )z >= 0LL) && (2147483650LL - (long long )n) + (long long )z
        >= 0LL) && (4294967287LL - (long long )x) + (long long )z >= 0LL) && (1LL
        + (long long )k) - (long long )n >= 0LL) && (2147483637LL + (long long )n)
        - (long long )x >= 0LL) && (2147483638LL + (long long )k) - (long long )x
        >= 0LL) && (2147483645LL + (long long )x) - (long long )y >= 0LL) && (2147483645LL
        + (long long )x) - (long long )z >= 0LL) && (2147483645LL + (long long )n)
        - (long long )y >= 0LL) && (2147483645LL + (long long )n) - (long long )z
        >= 0LL) && (2147483646LL + (long long )k) - (long long )y >= 0LL) && (2147483646LL
        + (long long )k) - (long long )z >= 0LL) && (3LL - (long long )k) - (long
        long )n >= 0LL) && (2147483640LL - (long long )k) - (long long )x >= 0LL)
        && (2147483641LL - (long long )n) - (long long )x >= 0LL) && (2147483648LL
        - (long long )k) - (long long )y >= 0LL) && (2147483648LL - (long long )k)
        - (long long )z >= 0LL) && (2147483649LL - (long long )n) - (long long )y
        >= 0LL) && (2147483649LL - (long long )n) - (long long )z >= 0LL) && (4294967286LL
        - (long long )x) - (long long )y >= 0LL) && (4294967286LL - (long long )x)
        - (long long )z >= 0LL) && n == 2) && k == 1))) || ((((((((((((((((((((((((((((((((((((((((3
        <= x && 4 <= k) && k <= 2147483640) && (-7LL + (long long )k) + (long long
        )x >= 0LL) && (-4LL + (long long )k) + (long long )y >= 0LL) && (-4LL + (long
        long )k) + (long long )n >= 0LL) && (-3LL + (long long )x) + (long long )y
        >= 0LL) && (-3LL + (long long )n) + (long long )x >= 0LL) && (2147483644LL
        + (long long )k) + (long long )z >= 0LL) && (2147483645LL + (long long )x)
        + (long long )z >= 0LL) && (2147483648LL + (long long )n) + (long long )z
        >= 0LL) && (-3LL - (long long )n) + (long long )x >= 0LL) && (0LL - (long
        long )n) + (long long )y >= 0LL) && (1LL - (long long )k) + (long long )x
        >= 0LL) && (2147483640LL - (long long )k) + (long long )y >= 0LL) && (2147483640LL
        - (long long )k) + (long long )n >= 0LL) && (2147483647LL - (long long )x)
        + (long long )y >= 0LL) && (2147483648LL - (long long )n) + (long long )z
        >= 0LL) && (4294967288LL - (long long )k) + (long long )z >= 0LL) && (4294967295LL
        - (long long )x) + (long long )z >= 0LL) && (long long )n + (long long )y
        >= 0LL) && (-4LL + (long long )k) - (long long )n >= 0LL) && (2147483643LL
        + (long long )k) - (long long )x >= 0LL) && (2147483643LL + (long long )k)
        - (long long )y >= 0LL) && (2147483643LL + (long long )k) - (long long )z
        >= 0LL) && (2147483644LL + (long long )x) - (long long )y >= 0LL) && (2147483644LL
        + (long long )x) - (long long )z >= 0LL) && (2147483647LL + (long long )n)
        - (long long )x >= 0LL) && (2147483647LL + (long long )n) - (long long )y
        >= 0LL) && (2147483647LL + (long long )n) - (long long )z >= 0LL) && (2147483640LL
        - (long long )k) - (long long )n >= 0LL) && (2147483647LL - (long long )n)
        - (long long )x >= 0LL) && (2147483647LL - (long long )n) - (long long )y
        >= 0LL) && (2147483647LL - (long long )n) - (long long )z >= 0LL) && (4294967287LL
        - (long long )k) - (long long )x >= 0LL) && (4294967287LL - (long long )k)
        - (long long )y >= 0LL) && (4294967287LL - (long long )k) - (long long )z
        >= 0LL) && (4294967294LL - (long long )x) - (long long )y >= 0LL) && (4294967294LL
        - (long long )x) - (long long )z >= 0LL) && 0 == n) && n == 0)) || (((((((((((((((((((((((((((((((((((((((3
        <= x && x <= 2147483639) && (-6LL + (long long )n) + (long long )x >= 0LL)
        && (-6LL + (long long )k) + (long long )x >= 0LL) && (-6LL + (long long )k)
        + (long long )n >= 0LL) && (-3LL + (long long )x) + (long long )y >= 0LL)
        && (-3LL + (long long )n) + (long long )y >= 0LL) && (-3LL + (long long )k)
        + (long long )y >= 0LL) && (2147483645LL + (long long )x) + (long long )z
        >= 0LL) && (2147483645LL + (long long )n) + (long long )z >= 0LL) && (2147483645LL
        + (long long )k) + (long long )z >= 0LL) && (0LL - (long long )n) + (long
        long )x >= 0LL) && (0LL - (long long )k) + (long long )x >= 0LL) && (0LL -
        (long long )k) + (long long )n >= 0LL) && (3LL - (long long )n) + (long long
        )y >= 0LL) && (3LL - (long long )k) + (long long )y >= 0LL) && (2147483639LL
        - (long long )x) + (long long )y >= 0LL) && (2147483651LL - (long long )n)
        + (long long )z >= 0LL) && (2147483651LL - (long long )k) + (long long )z
        >= 0LL) && (4294967287LL - (long long )x) + (long long )z >= 0LL) && (2147483636LL
        + (long long )n) - (long long )x >= 0LL) && (2147483636LL + (long long )k)
        - (long long )x >= 0LL) && (2147483644LL + (long long )x) - (long long )y
        >= 0LL) && (2147483644LL + (long long )x) - (long long )z >= 0LL) && (2147483644LL
        + (long long )n) - (long long )y >= 0LL) && (2147483644LL + (long long )n)
        - (long long )z >= 0LL) && (2147483644LL + (long long )k) - (long long )y
        >= 0LL) && (2147483644LL + (long long )k) - (long long )z >= 0LL) && (6LL
        - (long long )k) - (long long )n >= 0LL) && (2147483642LL - (long long )n)
        - (long long )x >= 0LL) && (2147483642LL - (long long )k) - (long long )x
        >= 0LL) && (2147483650LL - (long long )n) - (long long )y >= 0LL) && (2147483650LL
        - (long long )n) - (long long )z >= 0LL) && (2147483650LL - (long long )k)
        - (long long )y >= 0LL) && (2147483650LL - (long long )k) - (long long )z
        >= 0LL) && (4294967286LL - (long long )x) - (long long )y >= 0LL) && (4294967286LL
        - (long long )x) - (long long )z >= 0LL) && (long long )k - (long long )n
        >= 0LL) && n == 3) && k == 3)) || ((((((((((((((((((((((((((((((((((((((((2
        <= x && x <= 2147483639) && (-4LL + (long long )n) + (long long )x >= 0LL)
        && (-2LL + (long long )x) + (long long )y >= 0LL) && (-2LL + (long long )n)
        + (long long )y >= 0LL) && (-2LL + (long long )k) + (long long )x >= 0LL)
        && (-2LL + (long long )k) + (long long )n >= 0LL) && (2147483646LL + (long
        long )x) + (long long )z >= 0LL) && (2147483646LL + (long long )n) + (long
        long )z >= 0LL) && (2147483648LL + (long long )k) + (long long )z >= 0LL)
        && (-2LL - (long long )k) + (long long )x >= 0LL) && (-2LL - (long long )k)
        + (long long )n >= 0LL) && (0LL - (long long )n) + (long long )x >= 0LL) &&
        (0LL - (long long )k) + (long long )y >= 0LL) && (2LL - (long long )n) + (long
        long )y >= 0LL) && (2147483639LL - (long long )x) + (long long )y >= 0LL)
        && (2147483648LL - (long long )k) + (long long )z >= 0LL) && (2147483650LL
        - (long long )n) + (long long )z >= 0LL) && (4294967287LL - (long long )x)
        + (long long )z >= 0LL) && (long long )k + (long long )y >= 0LL) && (2LL +
        (long long )k) - (long long )n >= 0LL) && (2147483637LL + (long long )n) -
        (long long )x >= 0LL) && (2147483639LL + (long long )k) - (long long )x >=
        0LL) && (2147483645LL + (long long )x) - (long long )y >= 0LL) && (2147483645LL
        + (long long )x) - (long long )z >= 0LL) && (2147483645LL + (long long )n)
        - (long long )y >= 0LL) && (2147483645LL + (long long )n) - (long long )z
        >= 0LL) && (2147483647LL + (long long )k) - (long long )y >= 0LL) && (2147483647LL
        + (long long )k) - (long long )z >= 0LL) && (2LL - (long long )k) - (long
        long )n >= 0LL) && (2147483639LL - (long long )k) - (long long )x >= 0LL)
        && (2147483641LL - (long long )n) - (long long )x >= 0LL) && (2147483647LL
        - (long long )k) - (long long )y >= 0LL) && (2147483647LL - (long long )k)
        - (long long )z >= 0LL) && (2147483649LL - (long long )n) - (long long )y
        >= 0LL) && (2147483649LL - (long long )n) - (long long )z >= 0LL) && (4294967286LL
        - (long long )x) - (long long )y >= 0LL) && (4294967286LL - (long long )x)
        - (long long )z >= 0LL) && 0 == k) && n == 2) && k == 0)) || (((((((((((((((((((((((((((((((((((((((2
        <= x && (-5LL + (long long )k) + (long long )x >= 0LL) && (-3LL + (long long
        )k) + (long long )y >= 0LL) && (-3LL + (long long )k) + (long long )n >= 0LL)
        && (-2LL + (long long )x) + (long long )y >= 0LL) && (-2LL + (long long )n)
        + (long long )x >= 0LL) && (2147483645LL + (long long )k) + (long long )z
        >= 0LL) && (2147483646LL + (long long )x) + (long long )z >= 0LL) && (2147483648LL
        + (long long )n) + (long long )z >= 0LL) && (-2LL - (long long )n) + (long
        long )x >= 0LL) && (0LL - (long long )n) + (long long )y >= 0LL) && (1LL -
        (long long )k) + (long long )x >= 0LL) && (3LL - (long long )k) + (long long
        )y >= 0LL) && (3LL - (long long )k) + (long long )n >= 0LL) && (2147483647LL
        - (long long )x) + (long long )y >= 0LL) && (2147483648LL - (long long )n)
        + (long long )z >= 0LL) && (2147483651LL - (long long )k) + (long long )z
        >= 0LL) && (4294967295LL - (long long )x) + (long long )z >= 0LL) && (long
        long )n + (long long )y >= 0LL) && (-3LL + (long long )k) - (long long )n
        >= 0LL) && (2147483644LL + (long long )k) - (long long )x >= 0LL) && (2147483644LL
        + (long long )k) - (long long )y >= 0LL) && (2147483644LL + (long long )k)
        - (long long )z >= 0LL) && (2147483645LL + (long long )x) - (long long )y
        >= 0LL) && (2147483645LL + (long long )x) - (long long )z >= 0LL) && (2147483647LL
        + (long long )n) - (long long )x >= 0LL) && (2147483647LL + (long long )n)
        - (long long )y >= 0LL) && (2147483647LL + (long long )n) - (long long )z
        >= 0LL) && (3LL - (long long )k) - (long long )n >= 0LL) && (2147483647LL
        - (long long )n) - (long long )x >= 0LL) && (2147483647LL - (long long )n)
        - (long long )y >= 0LL) && (2147483647LL - (long long )n) - (long long )z
        >= 0LL) && (2147483650LL - (long long )k) - (long long )x >= 0LL) && (2147483650LL
        - (long long )k) - (long long )y >= 0LL) && (2147483650LL - (long long )k)
        - (long long )z >= 0LL) && (4294967294LL - (long long )x) - (long long )y
        >= 0LL) && (4294967294LL - (long long )x) - (long long )z >= 0LL) && 0 ==
        n) && n == 0) && k == 3)) || (((((((((((((((((((((((((((((((((((((((3 <= x
        && x <= 2147483639) && (-6LL + (long long )n) + (long long )x >= 0LL) && (-5LL
        + (long long )k) + (long long )x >= 0LL) && (-5LL + (long long )k) + (long
        long )n >= 0LL) && (-3LL + (long long )x) + (long long )y >= 0LL) && (-3LL
        + (long long )n) + (long long )y >= 0LL) && (-2LL + (long long )k) + (long
        long )y >= 0LL) && (2147483645LL + (long long )x) + (long long )z >= 0LL)
        && (2147483645LL + (long long )n) + (long long )z >= 0LL) && (2147483646LL
        + (long long )k) + (long long )z >= 0LL) && (-1LL - (long long )k) + (long
        long )x >= 0LL) && (-1LL - (long long )k) + (long long )n >= 0LL) && (0LL
        - (long long )n) + (long long )x >= 0LL) && (2LL - (long long )k) + (long
        long )y >= 0LL) && (3LL - (long long )n) + (long long )y >= 0LL) && (2147483639LL
        - (long long )x) + (long long )y >= 0LL) && (2147483650LL - (long long )k)
        + (long long )z >= 0LL) && (2147483651LL - (long long )n) + (long long )z
        >= 0LL) && (4294967287LL - (long long )x) + (long long )z >= 0LL) && (1LL
        + (long long )k) - (long long )n >= 0LL) && (2147483636LL + (long long )n)
        - (long long )x >= 0LL) && (2147483637LL + (long long )k) - (long long )x
        >= 0LL) && (2147483644LL + (long long )x) - (long long )y >= 0LL) && (2147483644LL
        + (long long )x) - (long long )z >= 0LL) && (2147483644LL + (long long )n)
        - (long long )y >= 0LL) && (2147483644LL + (long long )n) - (long long )z
        >= 0LL) && (2147483645LL + (long long )k) - (long long )y >= 0LL) && (2147483645LL
        + (long long )k) - (long long )z >= 0LL) && (5LL - (long long )k) - (long
        long )n >= 0LL) && (2147483641LL - (long long )k) - (long long )x >= 0LL)
        && (2147483642LL - (long long )n) - (long long )x >= 0LL) && (2147483649LL
        - (long long )k) - (long long )y >= 0LL) && (2147483649LL - (long long )k)
        - (long long )z >= 0LL) && (2147483650LL - (long long )n) - (long long )y
        >= 0LL) && (2147483650LL - (long long )n) - (long long )z >= 0LL) && (4294967286LL
        - (long long )x) - (long long )y >= 0LL) && (4294967286LL - (long long )x)
        - (long long )z >= 0LL) && n == 3) && k == 2)) || (((((((((((((((((((((((((((((((((((((((((4
        <= x && 4 <= n) && 4 <= k) && x <= 2147483639) && n <= 2147483639) && k <=
        2147483628) && (-8LL + (long long )n) + (long long )x >= 0LL) && (-8LL + (long
        long )k) + (long long )x >= 0LL) && (-8LL + (long long )k) + (long long )n
        >= 0LL) && (-4LL + (long long )x) + (long long )y >= 0LL) && (-4LL + (long
        long )n) + (long long )y >= 0LL) && (-4LL + (long long )k) + (long long )y
        >= 0LL) && (2147483644LL + (long long )x) + (long long )z >= 0LL) && (2147483644LL
        + (long long )n) + (long long )z >= 0LL) && (2147483644LL + (long long )k)
        + (long long )z >= 0LL) && (0LL - (long long )n) + (long long )x >= 0LL) &&
        (1LL - (long long )k) + (long long )x >= 0LL) && (2147483529LL - (long long
        )k) + (long long )n >= 0LL) && (2147483628LL - (long long )k) + (long long
        )y >= 0LL) && (2147483639LL - (long long )n) + (long long )y >= 0LL) && (2147483647LL
        - (long long )x) + (long long )y >= 0LL) && (4294967276LL - (long long )k)
        + (long long )z >= 0LL) && (4294967287LL - (long long )n) + (long long )z
        >= 0LL) && (4294967295LL - (long long )x) + (long long )z >= 0LL) && (2147483635LL
        + (long long )k) - (long long )n >= 0LL) && (2147483643LL + (long long )x)
        - (long long )y >= 0LL) && (2147483643LL + (long long )x) - (long long )z
        >= 0LL) && (2147483643LL + (long long )n) - (long long )x >= 0LL) && (2147483643LL
        + (long long )n) - (long long )y >= 0LL) && (2147483643LL + (long long )n)
        - (long long )z >= 0LL) && (2147483643LL + (long long )k) - (long long )x
        >= 0LL) && (2147483643LL + (long long )k) - (long long )y >= 0LL) && (2147483643LL
        + (long long )k) - (long long )z >= 0LL) && (4294967267LL - (long long )k)
        - (long long )n >= 0LL) && (4294967275LL - (long long )k) - (long long )x
        >= 0LL) && (4294967275LL - (long long )k) - (long long )y >= 0LL) && (4294967275LL
        - (long long )k) - (long long )z >= 0LL) && (4294967286LL - (long long )n)
        - (long long )x >= 0LL) && (4294967286LL - (long long )n) - (long long )y
        >= 0LL) && (4294967286LL - (long long )n) - (long long )z >= 0LL) && (4294967294LL
        - (long long )x) - (long long )y >= 0LL) && (4294967294LL - (long long )x)
        - (long long )z >= 0LL)) || (((((((((((((((((((((((((((((((((((((((1 <= x
        && (-3LL + (long long )k) + (long long )x >= 0LL) && (-2LL + (long long )k)
        + (long long )y >= 0LL) && (-2LL + (long long )k) + (long long )n >= 0LL)
        && (-1LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )n)
        + (long long )x >= 0LL) && (2147483646LL + (long long )k) + (long long )z
        >= 0LL) && (2147483647LL + (long long )x) + (long long )z >= 0LL) && (2147483648LL
        + (long long )n) + (long long )z >= 0LL) && (-1LL - (long long )n) + (long
        long )x >= 0LL) && (0LL - (long long )n) + (long long )y >= 0LL) && (1LL -
        (long long )k) + (long long )x >= 0LL) && (2LL - (long long )k) + (long long
        )y >= 0LL) && (2LL - (long long )k) + (long long )n >= 0LL) && (2147483647LL
        - (long long )x) + (long long )y >= 0LL) && (2147483648LL - (long long )n)
        + (long long )z >= 0LL) && (2147483650LL - (long long )k) + (long long )z
        >= 0LL) && (4294967295LL - (long long )x) + (long long )z >= 0LL) && (long
        long )n + (long long )y >= 0LL) && (-2LL + (long long )k) - (long long )n
        >= 0LL) && (2147483645LL + (long long )k) - (long long )x >= 0LL) && (2147483645LL
        + (long long )k) - (long long )y >= 0LL) && (2147483645LL + (long long )k)
        - (long long )z >= 0LL) && (2147483646LL + (long long )x) - (long long )y
        >= 0LL) && (2147483646LL + (long long )x) - (long long )z >= 0LL) && (2147483647LL
        + (long long )n) - (long long )x >= 0LL) && (2147483647LL + (long long )n)
        - (long long )y >= 0LL) && (2147483647LL + (long long )n) - (long long )z
        >= 0LL) && (2LL - (long long )k) - (long long )n >= 0LL) && (2147483647LL
        - (long long )n) - (long long )x >= 0LL) && (2147483647LL - (long long )n)
        - (long long )y >= 0LL) && (2147483647LL - (long long )n) - (long long )z
        >= 0LL) && (2147483649LL - (long long )k) - (long long )x >= 0LL) && (2147483649LL
        - (long long )k) - (long long )y >= 0LL) && (2147483649LL - (long long )k)
        - (long long )z >= 0LL) && (4294967294LL - (long long )x) - (long long )y
        >= 0LL) && (4294967294LL - (long long )x) - (long long )z >= 0LL) && 0 ==
        n) && n == 0) && k == 2)) || (((((((((((((((((((((((((((((((((((((((3 <= x
        && x <= 2147483639) && (-6LL + (long long )n) + (long long )x >= 0LL) && (-4LL
        + (long long )k) + (long long )x >= 0LL) && (-4LL + (long long )k) + (long
        long )n >= 0LL) && (-3LL + (long long )x) + (long long )y >= 0LL) && (-3LL
        + (long long )n) + (long long )y >= 0LL) && (-1LL + (long long )k) + (long
        long )y >= 0LL) && (2147483645LL + (long long )x) + (long long )z >= 0LL)
        && (2147483645LL + (long long )n) + (long long )z >= 0LL) && (2147483647LL
        + (long long )k) + (long long )z >= 0LL) && (-2LL - (long long )k) + (long
        long )x >= 0LL) && (-2LL - (long long )k) + (long long )n >= 0LL) && (0LL
        - (long long )n) + (long long )x >= 0LL) && (1LL - (long long )k) + (long
        long )y >= 0LL) && (3LL - (long long )n) + (long long )y >= 0LL) && (2147483639LL
        - (long long )x) + (long long )y >= 0LL) && (2147483649LL - (long long )k)
        + (long long )z >= 0LL) && (2147483651LL - (long long )n) + (long long )z
        >= 0LL) && (4294967287LL - (long long )x) + (long long )z >= 0LL) && (2LL
        + (long long )k) - (long long )n >= 0LL) && (2147483636LL + (long long )n)
        - (long long )x >= 0LL) && (2147483638LL + (long long )k) - (long long )x
        >= 0LL) && (2147483644LL + (long long )x) - (long long )y >= 0LL) && (2147483644LL
        + (long long )x) - (long long )z >= 0LL) && (2147483644LL + (long long )n)
        - (long long )y >= 0LL) && (2147483644LL + (long long )n) - (long long )z
        >= 0LL) && (2147483646LL + (long long )k) - (long long )y >= 0LL) && (2147483646LL
        + (long long )k) - (long long )z >= 0LL) && (4LL - (long long )k) - (long
        long )n >= 0LL) && (2147483640LL - (long long )k) - (long long )x >= 0LL)
        && (2147483642LL - (long long )n) - (long long )x >= 0LL) && (2147483648LL
        - (long long )k) - (long long )y >= 0LL) && (2147483648LL - (long long )k)
        - (long long )z >= 0LL) && (2147483650LL - (long long )n) - (long long )y
        >= 0LL) && (2147483650LL - (long long )n) - (long long )z >= 0LL) && (4294967286LL
        - (long long )x) - (long long )y >= 0LL) && (4294967286LL - (long long )x)
        - (long long )z >= 0LL) && n == 3) && k == 1)) || ((((((((((((((((((((((((((((((((((((((((3
        <= x && 4 <= k) && x <= 2147483639) && k <= 2147483640) && (-7LL + (long long
        )k) + (long long )x >= 0LL) && (-5LL + (long long )k) + (long long )n >= 0LL)
        && (-4LL + (long long )n) + (long long )x >= 0LL) && (-4LL + (long long )k)
        + (long long )y >= 0LL) && (-3LL + (long long )x) + (long long )y >= 0LL)
        && (-1LL + (long long )n) + (long long )y >= 0LL) && (2147483644LL + (long
        long )k) + (long long )z >= 0LL) && (2147483645LL + (long long )x) + (long
        long )z >= 0LL) && (2147483647LL + (long long )n) + (long long )z >= 0LL)
        && (-2LL - (long long )n) + (long long )x >= 0LL) && (1LL - (long long )n)
        + (long long )y >= 0LL) && (1LL - (long long )k) + (long long )x >= 0LL) &&
        (2147483639LL - (long long )k) + (long long )n >= 0LL) && (2147483640LL -
        (long long )k) + (long long )y >= 0LL) && (2147483647LL - (long long )x) +
        (long long )y >= 0LL) && (2147483649LL - (long long )n) + (long long )z >=
        0LL) && (4294967288LL - (long long )k) + (long long )z >= 0LL) && (4294967295LL
        - (long long )x) + (long long )z >= 0LL) && (-3LL + (long long )k) - (long
        long )n >= 0LL) && (2147483643LL + (long long )k) - (long long )x >= 0LL)
        && (2147483643LL + (long long )k) - (long long )y >= 0LL) && (2147483643LL
        + (long long )k) - (long long )z >= 0LL) && (2147483644LL + (long long )x)
        - (long long )y >= 0LL) && (2147483644LL + (long long )x) - (long long )z
        >= 0LL) && (2147483646LL + (long long )n) - (long long )x >= 0LL) && (2147483646LL
        + (long long )n) - (long long )y >= 0LL) && (2147483646LL + (long long )n)
        - (long long )z >= 0LL) && (2147483641LL - (long long )k) - (long long )n
        >= 0LL) && (2147483648LL - (long long )n) - (long long )x >= 0LL) && (2147483648LL
        - (long long )n) - (long long )y >= 0LL) && (2147483648LL - (long long )n)
        - (long long )z >= 0LL) && (4294967287LL - (long long )k) - (long long )x
        >= 0LL) && (4294967287LL - (long long )k) - (long long )y >= 0LL) && (4294967287LL
        - (long long )k) - (long long )z >= 0LL) && (4294967294LL - (long long )x)
        - (long long )y >= 0LL) && (4294967294LL - (long long )x) - (long long )z
        >= 0LL) && n == 1)) || ((((((((((((((((((((((((((((((((((((((((4 <= x && 4
        <= n) && x <= 2147483639) && n <= 2147483628) && (-8LL + (long long )n) +
        (long long )x >= 0LL) && (-7LL + (long long )k) + (long long )x >= 0LL) &&
        (-7LL + (long long )k) + (long long )n >= 0LL) && (-4LL + (long long )x) +
        (long long )y >= 0LL) && (-4LL + (long long )n) + (long long )y >= 0LL) &&
        (-3LL + (long long )k) + (long long )y >= 0LL) && (2147483644LL + (long long
        )x) + (long long )z >= 0LL) && (2147483644LL + (long long )n) + (long long
        )z >= 0LL) && (2147483645LL + (long long )k) + (long long )z >= 0LL) && (-1LL
        - (long long )k) + (long long )x >= 0LL) && (-1LL - (long long )k) + (long
        long )n >= 0LL) && (0LL - (long long )n) + (long long )x >= 0LL) && (3LL -
        (long long )k) + (long long )y >= 0LL) && (2147483639LL - (long long )n) +
        (long long )y >= 0LL) && (2147483647LL - (long long )x) + (long long )y >=
        0LL) && (2147483651LL - (long long )k) + (long long )z >= 0LL) && (4294967287LL
        - (long long )n) + (long long )z >= 0LL) && (4294967295LL - (long long )x)
        + (long long )z >= 0LL) && (2147483636LL + (long long )k) - (long long )n
        >= 0LL) && (2147483643LL + (long long )x) - (long long )y >= 0LL) && (2147483643LL
        + (long long )x) - (long long )z >= 0LL) && (2147483643LL + (long long )n)
        - (long long )x >= 0LL) && (2147483643LL + (long long )n) - (long long )y
        >= 0LL) && (2147483643LL + (long long )n) - (long long )z >= 0LL) && (2147483644LL
        + (long long )k) - (long long )x >= 0LL) && (2147483644LL + (long long )k)
        - (long long )y >= 0LL) && (2147483644LL + (long long )k) - (long long )z
        >= 0LL) && (2147483642LL - (long long )k) - (long long )n >= 0LL) && (2147483650LL
        - (long long )k) - (long long )x >= 0LL) && (2147483650LL - (long long )k)
        - (long long )y >= 0LL) && (2147483650LL - (long long )k) - (long long )z
        >= 0LL) && (4294967286LL - (long long )n) - (long long )x >= 0LL) && (4294967286LL
        - (long long )n) - (long long )y >= 0LL) && (4294967286LL - (long long )n)
        - (long long )z >= 0LL) && (4294967294LL - (long long )x) - (long long )y
        >= 0LL) && (4294967294LL - (long long )x) - (long long )z >= 0LL) && k ==
        3)) || (((((((((((((((((((((((((((((((((((((((0 <= x && (-1LL + (long long
        )k) + (long long )x >= 0LL) && (-1LL + (long long )k) + (long long )y >= 0LL)
        && (-1LL + (long long )k) + (long long )n >= 0LL) && (2147483647LL + (long
        long )k) + (long long )z >= 0LL) && (2147483648LL + (long long )x) + (long
        long )z >= 0LL) && (2147483648LL + (long long )n) + (long long )z >= 0LL)
        && (0LL - (long long )n) + (long long )x >= 0LL) && (0LL - (long long )n)
        + (long long )y >= 0LL) && (1LL - (long long )k) + (long long )x >= 0LL) &&
        (1LL - (long long )k) + (long long )y >= 0LL) && (1LL - (long long )k) + (long
        long )n >= 0LL) && (2147483647LL - (long long )x) + (long long )y >= 0LL)
        && (2147483648LL - (long long )n) + (long long )z >= 0LL) && (2147483649LL
        - (long long )k) + (long long )z >= 0LL) && (4294967295LL - (long long )x)
        + (long long )z >= 0LL) && (long long )x + (long long )y >= 0LL) && (long
        long )n + (long long )x >= 0LL) && (long long )n + (long long )y >= 0LL) &&
        (-1LL + (long long )k) - (long long )n >= 0LL) && (2147483646LL + (long long
        )k) - (long long )x >= 0LL) && (2147483646LL + (long long )k) - (long long
        )y >= 0LL) && (2147483646LL + (long long )k) - (long long )z >= 0LL) && (2147483647LL
        + (long long )x) - (long long )y >= 0LL) && (2147483647LL + (long long )x)
        - (long long )z >= 0LL) && (2147483647LL + (long long )n) - (long long )x
        >= 0LL) && (2147483647LL + (long long )n) - (long long )y >= 0LL) && (2147483647LL
        + (long long )n) - (long long )z >= 0LL) && (1LL - (long long )k) - (long
        long )n >= 0LL) && (2147483647LL - (long long )n) - (long long )x >= 0LL)
        && (2147483647LL - (long long )n) - (long long )y >= 0LL) && (2147483647LL
        - (long long )n) - (long long )z >= 0LL) && (2147483648LL - (long long )k)
        - (long long )x >= 0LL) && (2147483648LL - (long long )k) - (long long )y
        >= 0LL) && (2147483648LL - (long long )k) - (long long )z >= 0LL) && (4294967294LL
        - (long long )x) - (long long )y >= 0LL) && (4294967294LL - (long long )x)
        - (long long )z >= 0LL) && 0 == n) && n == 0) && k == 1)) || ((((((((((((((((((((((((((((((((((((((((3
        <= x && x <= 2147483639) && (-6LL + (long long )n) + (long long )x >= 0LL)
        && (-3LL + (long long )x) + (long long )y >= 0LL) && (-3LL + (long long )n)
        + (long long )y >= 0LL) && (-3LL + (long long )k) + (long long )x >= 0LL)
        && (-3LL + (long long )k) + (long long )n >= 0LL) && (2147483645LL + (long
        long )x) + (long long )z >= 0LL) && (2147483645LL + (long long )n) + (long
        long )z >= 0LL) && (2147483648LL + (long long )k) + (long long )z >= 0LL)
        && (-3LL - (long long )k) + (long long )x >= 0LL) && (-3LL - (long long )k)
        + (long long )n >= 0LL) && (0LL - (long long )n) + (long long )x >= 0LL) &&
        (0LL - (long long )k) + (long long )y >= 0LL) && (3LL - (long long )n) + (long
        long )y >= 0LL) && (2147483639LL - (long long )x) + (long long )y >= 0LL)
        && (2147483648LL - (long long )k) + (long long )z >= 0LL) && (2147483651LL
        - (long long )n) + (long long )z >= 0LL) && (4294967287LL - (long long )x)
        + (long long )z >= 0LL) && (long long )k + (long long )y >= 0LL) && (3LL +
        (long long )k) - (long long )n >= 0LL) && (2147483636LL + (long long )n) -
        (long long )x >= 0LL) && (2147483639LL + (long long )k) - (long long )x >=
        0LL) && (2147483644LL + (long long )x) - (long long )y >= 0LL) && (2147483644LL
        + (long long )x) - (long long )z >= 0LL) && (2147483644LL + (long long )n)
        - (long long )y >= 0LL) && (2147483644LL + (long long )n) - (long long )z
        >= 0LL) && (2147483647LL + (long long )k) - (long long )y >= 0LL) && (2147483647LL
        + (long long )k) - (long long )z >= 0LL) && (3LL - (long long )k) - (long
        long )n >= 0LL) && (2147483639LL - (long long )k) - (long long )x >= 0LL)
        && (2147483642LL - (long long )n) - (long long )x >= 0LL) && (2147483647LL
        - (long long )k) - (long long )y >= 0LL) && (2147483647LL - (long long )k)
        - (long long )z >= 0LL) && (2147483650LL - (long long )n) - (long long )y
        >= 0LL) && (2147483650LL - (long long )n) - (long long )z >= 0LL) && (4294967286LL
        - (long long )x) - (long long )y >= 0LL) && (4294967286LL - (long long )x)
        - (long long )z >= 0LL) && 0 == k) && n == 3) && k == 0)) || (((((((((((((((((((((((((((((((((((((((2
        <= x && x <= 2147483639) && (-5LL + (long long )k) + (long long )x >= 0LL)
        && (-4LL + (long long )k) + (long long )n >= 0LL) && (-3LL + (long long )n)
        + (long long )x >= 0LL) && (-3LL + (long long )k) + (long long )y >= 0LL)
        && (-2LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )n)
        + (long long )y >= 0LL) && (2147483645LL + (long long )k) + (long long )z
        >= 0LL) && (2147483646LL + (long long )x) + (long long )z >= 0LL) && (2147483647LL
        + (long long )n) + (long long )z >= 0LL) && (-1LL - (long long )n) + (long
        long )x >= 0LL) && (1LL - (long long )n) + (long long )y >= 0LL) && (1LL -
        (long long )k) + (long long )x >= 0LL) && (2LL - (long long )k) + (long long
        )n >= 0LL) && (3LL - (long long )k) + (long long )y >= 0LL) && (2147483647LL
        - (long long )x) + (long long )y >= 0LL) && (2147483649LL - (long long )n)
        + (long long )z >= 0LL) && (2147483651LL - (long long )k) + (long long )z
        >= 0LL) && (4294967295LL - (long long )x) + (long long )z >= 0LL) && (-2LL
        + (long long )k) - (long long )n >= 0LL) && (2147483644LL + (long long )k)
        - (long long )x >= 0LL) && (2147483644LL + (long long )k) - (long long )y
        >= 0LL) && (2147483644LL + (long long )k) - (long long )z >= 0LL) && (2147483645LL
        + (long long )x) - (long long )y >= 0LL) && (2147483645LL + (long long )x)
        - (long long )z >= 0LL) && (2147483646LL + (long long )n) - (long long )x
        >= 0LL) && (2147483646LL + (long long )n) - (long long )y >= 0LL) && (2147483646LL
        + (long long )n) - (long long )z >= 0LL) && (4LL - (long long )k) - (long
        long )n >= 0LL) && (2147483648LL - (long long )n) - (long long )x >= 0LL)
        && (2147483648LL - (long long )n) - (long long )y >= 0LL) && (2147483648LL
        - (long long )n) - (long long )z >= 0LL) && (2147483650LL - (long long )k)
        - (long long )x >= 0LL) && (2147483650LL - (long long )k) - (long long )y
        >= 0LL) && (2147483650LL - (long long )k) - (long long )z >= 0LL) && (4294967294LL
        - (long long )x) - (long long )y >= 0LL) && (4294967294LL - (long long )x)
        - (long long )z >= 0LL) && n == 1) && k == 3)) || ((((((((((((((((((((((((((((((((((((((((4
        <= x && 4 <= n) && x <= 2147483639) && n <= 2147483628) && (-8LL + (long long
        )n) + (long long )x >= 0LL) && (-6LL + (long long )k) + (long long )x >= 0LL)
        && (-6LL + (long long )k) + (long long )n >= 0LL) && (-4LL + (long long )x)
        + (long long )y >= 0LL) && (-4LL + (long long )n) + (long long )y >= 0LL)
        && (-2LL + (long long )k) + (long long )y >= 0LL) && (2147483644LL + (long
        long )x) + (long long )z >= 0LL) && (2147483644LL + (long long )n) + (long
        long )z >= 0LL) && (2147483646LL + (long long )k) + (long long )z >= 0LL)
        && (-2LL - (long long )k) + (long long )x >= 0LL) && (-2LL - (long long )k)
        + (long long )n >= 0LL) && (0LL - (long long )n) + (long long )x >= 0LL) &&
        (2LL - (long long )k) + (long long )y >= 0LL) && (2147483639LL - (long long
        )n) + (long long )y >= 0LL) && (2147483647LL - (long long )x) + (long long
        )y >= 0LL) && (2147483650LL - (long long )k) + (long long )z >= 0LL) && (4294967287LL
        - (long long )n) + (long long )z >= 0LL) && (4294967295LL - (long long )x)
        + (long long )z >= 0LL) && (2147483637LL + (long long )k) - (long long )n
        >= 0LL) && (2147483643LL + (long long )x) - (long long )y >= 0LL) && (2147483643LL
        + (long long )x) - (long long )z >= 0LL) && (2147483643LL + (long long )n)
        - (long long )x >= 0LL) && (2147483643LL + (long long )n) - (long long )y
        >= 0LL) && (2147483643LL + (long long )n) - (long long )z >= 0LL) && (2147483645LL
        + (long long )k) - (long long )x >= 0LL) && (2147483645LL + (long long )k)
        - (long long )y >= 0LL) && (2147483645LL + (long long )k) - (long long )z
        >= 0LL) && (2147483641LL - (long long )k) - (long long )n >= 0LL) && (2147483649LL
        - (long long )k) - (long long )x >= 0LL) && (2147483649LL - (long long )k)
        - (long long )y >= 0LL) && (2147483649LL - (long long )k) - (long long )z
        >= 0LL) && (4294967286LL - (long long )n) - (long long )x >= 0LL) && (4294967286LL
        - (long long )n) - (long long )y >= 0LL) && (4294967286LL - (long long )n)
        - (long long )z >= 0LL) && (4294967294LL - (long long )x) - (long long )y
        >= 0LL) && (4294967294LL - (long long )x) - (long long )z >= 0LL) && k ==
        2)) || (((((((((((((((((((((((((((((((((((((((((0 <= x && (2147483648LL +
        (long long )x) + (long long )z >= 0LL) && (2147483648LL + (long long )n) +
        (long long )z >= 0LL) && (2147483648LL + (long long )k) + (long long )z >=
        0LL) && (0LL - (long long )n) + (long long )x >= 0LL) && (0LL - (long long
        )n) + (long long )y >= 0LL) && (0LL - (long long )k) + (long long )x >= 0LL)
        && (0LL - (long long )k) + (long long )y >= 0LL) && (0LL - (long long )k)
        + (long long )n >= 0LL) && (2147483647LL - (long long )x) + (long long )y
        >= 0LL) && (2147483648LL - (long long )n) + (long long )z >= 0LL) && (2147483648LL
        - (long long )k) + (long long )z >= 0LL) && (4294967295LL - (long long )x)
        + (long long )z >= 0LL) && (long long )x + (long long )y >= 0LL) && (long
        long )n + (long long )x >= 0LL) && (long long )n + (long long )y >= 0LL) &&
        (long long )k + (long long )x >= 0LL) && (long long )k + (long long )y >=
        0LL) && (long long )k + (long long )n >= 0LL) && (2147483647LL + (long long
        )x) - (long long )y >= 0LL) && (2147483647LL + (long long )x) - (long long
        )z >= 0LL) && (2147483647LL + (long long )n) - (long long )x >= 0LL) && (2147483647LL
        + (long long )n) - (long long )y >= 0LL) && (2147483647LL + (long long )n)
        - (long long )z >= 0LL) && (2147483647LL + (long long )k) - (long long )x
        >= 0LL) && (2147483647LL + (long long )k) - (long long )y >= 0LL) && (2147483647LL
        + (long long )k) - (long long )z >= 0LL) && (0LL - (long long )k) - (long
        long )n >= 0LL) && (2147483647LL - (long long )n) - (long long )x >= 0LL)
        && (2147483647LL - (long long )n) - (long long )y >= 0LL) && (2147483647LL
        - (long long )n) - (long long )z >= 0LL) && (2147483647LL - (long long )k)
        - (long long )x >= 0LL) && (2147483647LL - (long long )k) - (long long )y
        >= 0LL) && (2147483647LL - (long long )k) - (long long )z >= 0LL) && (4294967294LL
        - (long long )x) - (long long )y >= 0LL) && (4294967294LL - (long long )x)
        - (long long )z >= 0LL) && (long long )k - (long long )n >= 0LL) && 0 == n)
        && 0 == k) && n == 0) && n == k) && k == 0)) || ((((((((((((((((((((((((((((((((((((((((4
        <= x && 4 <= n) && x <= 2147483639) && n <= 2147483628) && (-8LL + (long long
        )n) + (long long )x >= 0LL) && (-5LL + (long long )k) + (long long )x >= 0LL)
        && (-5LL + (long long )k) + (long long )n >= 0LL) && (-4LL + (long long )x)
        + (long long )y >= 0LL) && (-4LL + (long long )n) + (long long )y >= 0LL)
        && (-1LL + (long long )k) + (long long )y >= 0LL) && (2147483644LL + (long
        long )x) + (long long )z >= 0LL) && (2147483644LL + (long long )n) + (long
        long )z >= 0LL) && (2147483647LL + (long long )k) + (long long )z >= 0LL)
        && (-3LL - (long long )k) + (long long )x >= 0LL) && (-3LL - (long long )k)
        + (long long )n >= 0LL) && (0LL - (long long )n) + (long long )x >= 0LL) &&
        (1LL - (long long )k) + (long long )y >= 0LL) && (2147483639LL - (long long
        )n) + (long long )y >= 0LL) && (2147483647LL - (long long )x) + (long long
        )y >= 0LL) && (2147483649LL - (long long )k) + (long long )z >= 0LL) && (4294967287LL
        - (long long )n) + (long long )z >= 0LL) && (4294967295LL - (long long )x)
        + (long long )z >= 0LL) && (2147483638LL + (long long )k) - (long long )n
        >= 0LL) && (2147483643LL + (long long )x) - (long long )y >= 0LL) && (2147483643LL
        + (long long )x) - (long long )z >= 0LL) && (2147483643LL + (long long )n)
        - (long long )x >= 0LL) && (2147483643LL + (long long )n) - (long long )y
        >= 0LL) && (2147483643LL + (long long )n) - (long long )z >= 0LL) && (2147483646LL
        + (long long )k) - (long long )x >= 0LL) && (2147483646LL + (long long )k)
        - (long long )y >= 0LL) && (2147483646LL + (long long )k) - (long long )z
        >= 0LL) && (2147483640LL - (long long )k) - (long long )n >= 0LL) && (2147483648LL
        - (long long )k) - (long long )x >= 0LL) && (2147483648LL - (long long )k)
        - (long long )y >= 0LL) && (2147483648LL - (long long )k) - (long long )z
        >= 0LL) && (4294967286LL - (long long )n) - (long long )x >= 0LL) && (4294967286LL
        - (long long )n) - (long long )y >= 0LL) && (4294967286LL - (long long )n)
        - (long long )z >= 0LL) && (4294967294LL - (long long )x) - (long long )y
        >= 0LL) && (4294967294LL - (long long )x) - (long long )z >= 0LL) && k ==
        1)) || (((((((((((((((((((((((((((((((((((((((1 <= x && x <= 2147483639) &&
        (-3LL + (long long )k) + (long long )x >= 0LL) && (-3LL + (long long )k) +
        (long long )n >= 0LL) && (-2LL + (long long )n) + (long long )x >= 0LL) &&
        (-2LL + (long long )k) + (long long )y >= 0LL) && (-1LL + (long long )x) +
        (long long )y >= 0LL) && (-1LL + (long long )n) + (long long )y >= 0LL) &&
        (2147483646LL + (long long )k) + (long long )z >= 0LL) && (2147483647LL +
        (long long )x) + (long long )z >= 0LL) && (2147483647LL + (long long )n) +
        (long long )z >= 0LL) && (0LL - (long long )n) + (long long )x >= 0LL) &&
        (1LL - (long long )n) + (long long )y >= 0LL) && (1LL - (long long )k) + (long
        long )x >= 0LL) && (1LL - (long long )k) + (long long )n >= 0LL) && (2LL -
        (long long )k) + (long long )y >= 0LL) && (2147483647LL - (long long )x) +
        (long long )y >= 0LL) && (2147483649LL - (long long )n) + (long long )z >=
        0LL) && (2147483650LL - (long long )k) + (long long )z >= 0LL) && (4294967295LL
        - (long long )x) + (long long )z >= 0LL) && (-1LL + (long long )k) - (long
        long )n >= 0LL) && (2147483645LL + (long long )k) - (long long )x >= 0LL)
        && (2147483645LL + (long long )k) - (long long )y >= 0LL) && (2147483645LL
        + (long long )k) - (long long )z >= 0LL) && (2147483646LL + (long long )x)
        - (long long )y >= 0LL) && (2147483646LL + (long long )x) - (long long )z
        >= 0LL) && (2147483646LL + (long long )n) - (long long )x >= 0LL) && (2147483646LL
        + (long long )n) - (long long )y >= 0LL) && (2147483646LL + (long long )n)
        - (long long )z >= 0LL) && (3LL - (long long )k) - (long long )n >= 0LL) &&
        (2147483648LL - (long long )n) - (long long )x >= 0LL) && (2147483648LL -
        (long long )n) - (long long )y >= 0LL) && (2147483648LL - (long long )n) -
        (long long )z >= 0LL) && (2147483649LL - (long long )k) - (long long )x >=
        0LL) && (2147483649LL - (long long )k) - (long long )y >= 0LL) && (2147483649LL
        - (long long )k) - (long long )z >= 0LL) && (4294967294LL - (long long )x)
        - (long long )y >= 0LL) && (4294967294LL - (long long )x) - (long long )z
        >= 0LL) && n == 1) && k == 2)) || ((((((((((((((((((((((((((((((((((((((((3
        <= x && 4 <= k) && x <= 2147483639) && k <= 2147483640) && (-7LL + (long long
        )k) + (long long )x >= 0LL) && (-6LL + (long long )k) + (long long )n >= 0LL)
        && (-5LL + (long long )n) + (long long )x >= 0LL) && (-4LL + (long long )k)
        + (long long )y >= 0LL) && (-3LL + (long long )x) + (long long )y >= 0LL)
        && (-2LL + (long long )n) + (long long )y >= 0LL) && (2147483644LL + (long
        long )k) + (long long )z >= 0LL) && (2147483645LL + (long long )x) + (long
        long )z >= 0LL) && (2147483646LL + (long long )n) + (long long )z >= 0LL)
        && (-1LL - (long long )n) + (long long )x >= 0LL) && (1LL - (long long )k)
        + (long long )x >= 0LL) && (2LL - (long long )n) + (long long )y >= 0LL) &&
        (2147483638LL - (long long )k) + (long long )n >= 0LL) && (2147483640LL -
        (long long )k) + (long long )y >= 0LL) && (2147483647LL - (long long )x) +
        (long long )y >= 0LL) && (2147483650LL - (long long )n) + (long long )z >=
        0LL) && (4294967288LL - (long long )k) + (long long )z >= 0LL) && (4294967295LL
        - (long long )x) + (long long )z >= 0LL) && (-2LL + (long long )k) - (long
        long )n >= 0LL) && (2147483641LL + (long long )k) - (long long )x >= 0LL)
        && (2147483643LL + (long long )k) - (long long )y >= 0LL) && (2147483643LL
        + (long long )k) - (long long )z >= 0LL) && (2147483644LL + (long long )x)
        - (long long )y >= 0LL) && (2147483644LL + (long long )x) - (long long )z
        >= 0LL) && (2147483645LL + (long long )n) - (long long )x >= 0LL) && (2147483645LL
        + (long long )n) - (long long )y >= 0LL) && (2147483645LL + (long long )n)
        - (long long )z >= 0LL) && (2147483642LL - (long long )k) - (long long )n
        >= 0LL) && (2147483649LL - (long long )n) - (long long )x >= 0LL) && (2147483649LL
        - (long long )n) - (long long )y >= 0LL) && (2147483649LL - (long long )n)
        - (long long )z >= 0LL) && (4294967287LL - (long long )k) - (long long )x
        >= 0LL) && (4294967287LL - (long long )k) - (long long )y >= 0LL) && (4294967287LL
        - (long long )k) - (long long )z >= 0LL) && (4294967294LL - (long long )x)
        - (long long )y >= 0LL) && (4294967294LL - (long long )x) - (long long )z
        >= 0LL) && n == 2)) || (((((((((((((((((((((((((((((((((((((((((4 <= x &&
        4 <= n) && x <= 2147483639) && n <= 2147483628) && (-8LL + (long long )n)
        + (long long )x >= 0LL) && (-4LL + (long long )x) + (long long )y >= 0LL)
        && (-4LL + (long long )n) + (long long )y >= 0LL) && (-4LL + (long long )k)
        + (long long )x >= 0LL) && (-4LL + (long long )k) + (long long )n >= 0LL)
        && (2147483644LL + (long long )x) + (long long )z >= 0LL) && (2147483644LL
        + (long long )n) + (long long )z >= 0LL) && (2147483648LL + (long long )k)
        + (long long )z >= 0LL) && (-4LL - (long long )k) + (long long )x >= 0LL)
        && (-4LL - (long long )k) + (long long )n >= 0LL) && (0LL - (long long )n)
        + (long long )x >= 0LL) && (0LL - (long long )k) + (long long )y >= 0LL) &&
        (2147483647LL - (long long )x) + (long long )y >= 0LL) && (2147483647LL -
        (long long )n) + (long long )y >= 0LL) && (2147483648LL - (long long )k) +
        (long long )z >= 0LL) && (4294967295LL - (long long )x) + (long long )z >=
        0LL) && (4294967295LL - (long long )n) + (long long )z >= 0LL) && (long long
        )k + (long long )y >= 0LL) && (2147483643LL + (long long )x) - (long long
        )y >= 0LL) && (2147483643LL + (long long )x) - (long long )z >= 0LL) && (2147483643LL
        + (long long )n) - (long long )x >= 0LL) && (2147483643LL + (long long )n)
        - (long long )y >= 0LL) && (2147483643LL + (long long )n) - (long long )z
        >= 0LL) && (2147483647LL + (long long )k) - (long long )x >= 0LL) && (2147483647LL
        + (long long )k) - (long long )y >= 0LL) && (2147483647LL + (long long )k)
        - (long long )z >= 0LL) && (2147483647LL + (long long )k) - (long long )n
        >= 0LL) && (2147483647LL - (long long )k) - (long long )x >= 0LL) && (2147483647LL
        - (long long )k) - (long long )y >= 0LL) && (2147483647LL - (long long )k)
        - (long long )z >= 0LL) && (2147483647LL - (long long )k) - (long long )n
        >= 0LL) && (4294967294LL - (long long )x) - (long long )y >= 0LL) && (4294967294LL
        - (long long )x) - (long long )z >= 0LL) && (4294967294LL - (long long )n)
        - (long long )x >= 0LL) && (4294967294LL - (long long )n) - (long long )y
        >= 0LL) && (4294967294LL - (long long )n) - (long long )z >= 0LL) && 0 ==
        k) && k == 0)) || (((((((((((((((((((((((((((((((((((((((1 <= x && x <= 2147483639)
        && (-2LL + (long long )n) + (long long )x >= 0LL) && (-2LL + (long long )k)
        + (long long )x >= 0LL) && (-2LL + (long long )k) + (long long )n >= 0LL)
        && (-1LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )n)
        + (long long )y >= 0LL) && (-1LL + (long long )k) + (long long )y >= 0LL)
        && (2147483647LL + (long long )x) + (long long )z >= 0LL) && (2147483647LL
        + (long long )n) + (long long )z >= 0LL) && (2147483647LL + (long long )k)
        + (long long )z >= 0LL) && (0LL - (long long )n) + (long long )x >= 0LL) &&
        (0LL - (long long )k) + (long long )x >= 0LL) && (0LL - (long long )k) + (long
        long )n >= 0LL) && (1LL - (long long )n) + (long long )y >= 0LL) && (1LL -
        (long long )k) + (long long )y >= 0LL) && (2147483647LL - (long long )x) +
        (long long )y >= 0LL) && (2147483649LL - (long long )n) + (long long )z >=
        0LL) && (2147483649LL - (long long )k) + (long long )z >= 0LL) && (4294967295LL
        - (long long )x) + (long long )z >= 0LL) && (2147483646LL + (long long )x)
        - (long long )y >= 0LL) && (2147483646LL + (long long )x) - (long long )z
        >= 0LL) && (2147483646LL + (long long )n) - (long long )x >= 0LL) && (2147483646LL
        + (long long )n) - (long long )y >= 0LL) && (2147483646LL + (long long )n)
        - (long long )z >= 0LL) && (2147483646LL + (long long )k) - (long long )x
        >= 0LL) && (2147483646LL + (long long )k) - (long long )y >= 0LL) && (2147483646LL
        + (long long )k) - (long long )z >= 0LL) && (2LL - (long long )k) - (long
        long )n >= 0LL) && (2147483648LL - (long long )n) - (long long )x >= 0LL)
        && (2147483648LL - (long long )n) - (long long )y >= 0LL) && (2147483648LL
        - (long long )n) - (long long )z >= 0LL) && (2147483648LL - (long long )k)
        - (long long )x >= 0LL) && (2147483648LL - (long long )k) - (long long )y
        >= 0LL) && (2147483648LL - (long long )k) - (long long )z >= 0LL) && (4294967294LL
        - (long long )x) - (long long )y >= 0LL) && (4294967294LL - (long long )x)
        - (long long )z >= 0LL) && (long long )k - (long long )n >= 0LL) && n == 1)
        && k == 1)) || (((((((((((((((((((((((((((((((((((((((2 <= x && x <= 2147483639)
        && (-5LL + (long long )k) + (long long )x >= 0LL) && (-5LL + (long long )k)
        + (long long )n >= 0LL) && (-4LL + (long long )n) + (long long )x >= 0LL)
        && (-3LL + (long long )k) + (long long )y >= 0LL) && (-2LL + (long long )x)
        + (long long )y >= 0LL) && (-2LL + (long long )n) + (long long )y >= 0LL)
        && (2147483645LL + (long long )k) + (long long )z >= 0LL) && (2147483646LL
        + (long long )x) + (long long )z >= 0LL) && (2147483646LL + (long long )n)
        + (long long )z >= 0LL) && (0LL - (long long )n) + (long long )x >= 0LL) &&
        (1LL - (long long )k) + (long long )x >= 0LL) && (1LL - (long long )k) + (long
        long )n >= 0LL) && (2LL - (long long )n) + (long long )y >= 0LL) && (3LL -
        (long long )k) + (long long )y >= 0LL) && (2147483639LL - (long long )x) +
        (long long )y >= 0LL) && (2147483650LL - (long long )n) + (long long )z >=
        0LL) && (2147483651LL - (long long )k) + (long long )z >= 0LL) && (4294967287LL
        - (long long )x) + (long long )z >= 0LL) && (-1LL + (long long )k) - (long
        long )n >= 0LL) && (2147483636LL + (long long )k) - (long long )x >= 0LL)
        && (2147483637LL + (long long )n) - (long long )x >= 0LL) && (2147483644LL
        + (long long )k) - (long long )y >= 0LL) && (2147483644LL + (long long )k)
        - (long long )z >= 0LL) && (2147483645LL + (long long )x) - (long long )y
        >= 0LL) && (2147483645LL + (long long )x) - (long long )z >= 0LL) && (2147483645LL
        + (long long )n) - (long long )y >= 0LL) && (2147483645LL + (long long )n)
        - (long long )z >= 0LL) && (5LL - (long long )k) - (long long )n >= 0LL) &&
        (2147483641LL - (long long )n) - (long long )x >= 0LL) && (2147483642LL -
        (long long )k) - (long long )x >= 0LL) && (2147483649LL - (long long )n) -
        (long long )y >= 0LL) && (2147483649LL - (long long )n) - (long long )z >=
        0LL) && (2147483650LL - (long long )k) - (long long )y >= 0LL) && (2147483650LL
        - (long long )k) - (long long )z >= 0LL) && (4294967286LL - (long long )x)
        - (long long )y >= 0LL) && (4294967286LL - (long long )x) - (long long )z
        >= 0LL) && n == 2) && k == 3)) || ((((((((((((((((((((((((((((((((((((((((1
        <= x && x <= 2147483639) && (-2LL + (long long )n) + (long long )x >= 0LL)
        && (-1LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )n)
        + (long long )y >= 0LL) && (-1LL + (long long )k) + (long long )x >= 0LL)
        && (-1LL + (long long )k) + (long long )n >= 0LL) && (2147483647LL + (long
        long )x) + (long long )z >= 0LL) && (2147483647LL + (long long )n) + (long
        long )z >= 0LL) && (2147483648LL + (long long )k) + (long long )z >= 0LL)
        && (-1LL - (long long )k) + (long long )x >= 0LL) && (-1LL - (long long )k)
        + (long long )n >= 0LL) && (0LL - (long long )n) + (long long )x >= 0LL) &&
        (0LL - (long long )k) + (long long )y >= 0LL) && (1LL - (long long )n) + (long
        long )y >= 0LL) && (2147483647LL - (long long )x) + (long long )y >= 0LL)
        && (2147483648LL - (long long )k) + (long long )z >= 0LL) && (2147483649LL
        - (long long )n) + (long long )z >= 0LL) && (4294967295LL - (long long )x)
        + (long long )z >= 0LL) && (long long )k + (long long )y >= 0LL) && (1LL +
        (long long )k) - (long long )n >= 0LL) && (2147483646LL + (long long )x) -
        (long long )y >= 0LL) && (2147483646LL + (long long )x) - (long long )z >=
        0LL) && (2147483646LL + (long long )n) - (long long )x >= 0LL) && (2147483646LL
        + (long long )n) - (long long )y >= 0LL) && (2147483646LL + (long long )n)
        - (long long )z >= 0LL) && (2147483647LL + (long long )k) - (long long )x
        >= 0LL) && (2147483647LL + (long long )k) - (long long )y >= 0LL) && (2147483647LL
        + (long long )k) - (long long )z >= 0LL) && (1LL - (long long )k) - (long
        long )n >= 0LL) && (2147483647LL - (long long )k) - (long long )x >= 0LL)
        && (2147483647LL - (long long )k) - (long long )y >= 0LL) && (2147483647LL
        - (long long )k) - (long long )z >= 0LL) && (2147483648LL - (long long )n)
        - (long long )x >= 0LL) && (2147483648LL - (long long )n) - (long long )y
        >= 0LL) && (2147483648LL - (long long )n) - (long long )z >= 0LL) && (4294967294LL
        - (long long )x) - (long long )y >= 0LL) && (4294967294LL - (long long )x)
        - (long long )z >= 0LL) && 0 == k) && n == 1) && k == 0)
      format: c_expression
