- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 530812b0-77c5-401b-9afc-05adc42782d0
    creation_time: 2025-03-22T20:54:00Z
    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/recursified_loop-simple/recursified_nested_6.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c: 76648bc32cf18f500eee0df5c8487c6c0f67ad1050d870973d578953c78cde5c
      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/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (-12LL + (long long )c) + (long long )d >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (-12LL + (long long )c) + (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (-12LL + (long long )c) + (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (-12LL + (long long )d) + (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (-12LL + (long long )d) + (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (-12LL + (long long )e) + (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (0LL - (long long )c) + (long long )d >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (0LL - (long long )c) + (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (0LL - (long long )c) + (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (0LL - (long long )d) + (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (0LL - (long long )d) + (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (0LL - (long long )e) + (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (12LL - (long long )c) - (long long )d >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (12LL - (long long )c) - (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (12LL - (long long )c) - (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (12LL - (long long )d) - (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (12LL - (long long )d) - (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (12LL - (long long )e) - (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (long long )c - (long long )d >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (long long )c - (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (long long )c - (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (long long )d - (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (long long )d - (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: (long long )e - (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: c == 6
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: d == 6
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: e == 6
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: f == 6
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 114
        column: 11
        function: main
      value: ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((-12LL
        + (long long )b) + (long long )c >= 0LL && (-12LL + (long long )b) + (long
        long )d >= 0LL) && (-12LL + (long long )b) + (long long )e >= 0LL) && (-12LL
        + (long long )b) + (long long )f >= 0LL) && (-7LL + (long long )a) + (long
        long )b >= 0LL) && (-7LL + (long long )a) + (long long )c >= 0LL) && (-7LL
        + (long long )a) + (long long )d >= 0LL) && (-7LL + (long long )a) + (long
        long )e >= 0LL) && (-7LL + (long long )a) + (long long )f >= 0LL) && (0LL
        - (long long )b) + (long long )c >= 0LL) && (0LL - (long long )b) + (long
        long )d >= 0LL) && (0LL - (long long )b) + (long long )e >= 0LL) && (0LL -
        (long long )b) + (long long )f >= 0LL) && (5LL + (long long )a) - (long long
        )b >= 0LL) && (5LL + (long long )a) - (long long )c >= 0LL) && (5LL + (long
        long )a) - (long long )d >= 0LL) && (5LL + (long long )a) - (long long )e
        >= 0LL) && (5LL + (long long )a) - (long long )f >= 0LL) && (12LL - (long
        long )b) - (long long )c >= 0LL) && (12LL - (long long )b) - (long long )d
        >= 0LL) && (12LL - (long long )b) - (long long )e >= 0LL) && (12LL - (long
        long )b) - (long long )f >= 0LL) && (long long )b - (long long )c >= 0LL)
        && (long long )b - (long long )d >= 0LL) && (long long )b - (long long )e
        >= 0LL) && (long long )b - (long long )f >= 0LL) && a == 4) && b == 6) ||
        (((((((((((((((((((((((((((((((((((((((-8LL + (long long )a) + (long long
        )c >= 0LL && (-8LL + (long long )a) + (long long )d >= 0LL) && (-8LL + (long
        long )a) + (long long )e >= 0LL) && (-8LL + (long long )a) + (long long )f
        >= 0LL) && (-6LL + (long long )b) + (long long )c >= 0LL) && (-6LL + (long
        long )b) + (long long )d >= 0LL) && (-6LL + (long long )b) + (long long )e
        >= 0LL) && (-6LL + (long long )b) + (long long )f >= 0LL) && (-2LL + (long
        long )a) + (long long )b >= 0LL) && (-6LL - (long long )b) + (long long )c
        >= 0LL) && (-6LL - (long long )b) + (long long )d >= 0LL) && (-6LL - (long
        long )b) + (long long )e >= 0LL) && (-6LL - (long long )b) + (long long )f
        >= 0LL) && (-4LL - (long long )a) + (long long )c >= 0LL) && (-4LL - (long
        long )a) + (long long )d >= 0LL) && (-4LL - (long long )a) + (long long )e
        >= 0LL) && (-4LL - (long long )a) + (long long )f >= 0LL) && (2LL - (long
        long )a) + (long long )b >= 0LL) && (-2LL + (long long )a) - (long long )b
        >= 0LL) && (4LL + (long long )a) - (long long )c >= 0LL) && (4LL + (long long
        )a) - (long long )d >= 0LL) && (4LL + (long long )a) - (long long )e >= 0LL)
        && (4LL + (long long )a) - (long long )f >= 0LL) && (6LL + (long long )b)
        - (long long )c >= 0LL) && (6LL + (long long )b) - (long long )d >= 0LL) &&
        (6LL + (long long )b) - (long long )e >= 0LL) && (6LL + (long long )b) - (long
        long )f >= 0LL) && (2LL - (long long )a) - (long long )b >= 0LL) && (6LL -
        (long long )b) - (long long )c >= 0LL) && (6LL - (long long )b) - (long long
        )d >= 0LL) && (6LL - (long long )b) - (long long )e >= 0LL) && (6LL - (long
        long )b) - (long long )f >= 0LL) && (8LL - (long long )a) - (long long )c
        >= 0LL) && (8LL - (long long )a) - (long long )d >= 0LL) && (8LL - (long long
        )a) - (long long )e >= 0LL) && (8LL - (long long )a) - (long long )f >= 0LL)
        && 0 == b) && a == 2) && b == 0)) || ((((((((((((((((((((((((((((-11LL + (long
        long )b) + (long long )c >= 0LL && (-11LL + (long long )b) + (long long )d
        >= 0LL) && (-11LL + (long long )b) + (long long )e >= 0LL) && (-11LL + (long
        long )b) + (long long )f >= 0LL) && (-7LL + (long long )a) + (long long )c
        >= 0LL) && (-7LL + (long long )a) + (long long )d >= 0LL) && (-7LL + (long
        long )a) + (long long )e >= 0LL) && (-7LL + (long long )a) + (long long )f
        >= 0LL) && (-6LL + (long long )a) + (long long )b >= 0LL) && (-1LL - (long
        long )b) + (long long )c >= 0LL) && (-1LL - (long long )b) + (long long )d
        >= 0LL) && (-1LL - (long long )b) + (long long )e >= 0LL) && (-1LL - (long
        long )b) + (long long )f >= 0LL) && (1LL + (long long )b) - (long long )c
        >= 0LL) && (1LL + (long long )b) - (long long )d >= 0LL) && (1LL + (long long
        )b) - (long long )e >= 0LL) && (1LL + (long long )b) - (long long )f >= 0LL)
        && (4LL + (long long )a) - (long long )b >= 0LL) && (5LL + (long long )a)
        - (long long )c >= 0LL) && (5LL + (long long )a) - (long long )d >= 0LL) &&
        (5LL + (long long )a) - (long long )e >= 0LL) && (5LL + (long long )a) - (long
        long )f >= 0LL) && (11LL - (long long )b) - (long long )c >= 0LL) && (11LL
        - (long long )b) - (long long )d >= 0LL) && (11LL - (long long )b) - (long
        long )e >= 0LL) && (11LL - (long long )b) - (long long )f >= 0LL) && a ==
        4) && b == 5)) || ((((((((((((((((((((((((((((-10LL + (long long )b) + (long
        long )c >= 0LL && (-10LL + (long long )b) + (long long )d >= 0LL) && (-10LL
        + (long long )b) + (long long )e >= 0LL) && (-10LL + (long long )b) + (long
        long )f >= 0LL) && (-7LL + (long long )a) + (long long )c >= 0LL) && (-7LL
        + (long long )a) + (long long )d >= 0LL) && (-7LL + (long long )a) + (long
        long )e >= 0LL) && (-7LL + (long long )a) + (long long )f >= 0LL) && (-5LL
        + (long long )a) + (long long )b >= 0LL) && (-2LL - (long long )b) + (long
        long )c >= 0LL) && (-2LL - (long long )b) + (long long )d >= 0LL) && (-2LL
        - (long long )b) + (long long )e >= 0LL) && (-2LL - (long long )b) + (long
        long )f >= 0LL) && (2LL + (long long )b) - (long long )c >= 0LL) && (2LL +
        (long long )b) - (long long )d >= 0LL) && (2LL + (long long )b) - (long long
        )e >= 0LL) && (2LL + (long long )b) - (long long )f >= 0LL) && (3LL + (long
        long )a) - (long long )b >= 0LL) && (5LL + (long long )a) - (long long )c
        >= 0LL) && (5LL + (long long )a) - (long long )d >= 0LL) && (5LL + (long long
        )a) - (long long )e >= 0LL) && (5LL + (long long )a) - (long long )f >= 0LL)
        && (10LL - (long long )b) - (long long )c >= 0LL) && (10LL - (long long )b)
        - (long long )d >= 0LL) && (10LL - (long long )b) - (long long )e >= 0LL)
        && (10LL - (long long )b) - (long long )f >= 0LL) && a == 4) && b == 4)) ||
        ((((((((((((((((((((((((((((-12LL + (long long )b) + (long long )c >= 0LL
        && (-12LL + (long long )b) + (long long )d >= 0LL) && (-12LL + (long long
        )b) + (long long )e >= 0LL) && (-12LL + (long long )b) + (long long )f >=
        0LL) && (-7LL + (long long )a) + (long long )b >= 0LL) && (-7LL + (long long
        )a) + (long long )c >= 0LL) && (-7LL + (long long )a) + (long long )d >= 0LL)
        && (-7LL + (long long )a) + (long long )e >= 0LL) && (-7LL + (long long )a)
        + (long long )f >= 0LL) && (0LL - (long long )b) + (long long )c >= 0LL) &&
        (0LL - (long long )b) + (long long )d >= 0LL) && (0LL - (long long )b) + (long
        long )e >= 0LL) && (0LL - (long long )b) + (long long )f >= 0LL) && (5LL +
        (long long )a) - (long long )b >= 0LL) && (5LL + (long long )a) - (long long
        )c >= 0LL) && (5LL + (long long )a) - (long long )d >= 0LL) && (5LL + (long
        long )a) - (long long )e >= 0LL) && (5LL + (long long )a) - (long long )f
        >= 0LL) && (12LL - (long long )b) - (long long )c >= 0LL) && (12LL - (long
        long )b) - (long long )d >= 0LL) && (12LL - (long long )b) - (long long )e
        >= 0LL) && (12LL - (long long )b) - (long long )f >= 0LL) && (long long )b
        - (long long )c >= 0LL) && (long long )b - (long long )d >= 0LL) && (long
        long )b - (long long )e >= 0LL) && (long long )b - (long long )f >= 0LL) &&
        a == 1) && b == 6)) || ((((((((((((((((((((((((((((-9LL + (long long )b) +
        (long long )c >= 0LL && (-9LL + (long long )b) + (long long )d >= 0LL) &&
        (-9LL + (long long )b) + (long long )e >= 0LL) && (-9LL + (long long )b) +
        (long long )f >= 0LL) && (-7LL + (long long )a) + (long long )c >= 0LL) &&
        (-7LL + (long long )a) + (long long )d >= 0LL) && (-7LL + (long long )a) +
        (long long )e >= 0LL) && (-7LL + (long long )a) + (long long )f >= 0LL) &&
        (-4LL + (long long )a) + (long long )b >= 0LL) && (-3LL - (long long )b) +
        (long long )c >= 0LL) && (-3LL - (long long )b) + (long long )d >= 0LL) &&
        (-3LL - (long long )b) + (long long )e >= 0LL) && (-3LL - (long long )b) +
        (long long )f >= 0LL) && (2LL + (long long )a) - (long long )b >= 0LL) &&
        (3LL + (long long )b) - (long long )c >= 0LL) && (3LL + (long long )b) - (long
        long )d >= 0LL) && (3LL + (long long )b) - (long long )e >= 0LL) && (3LL +
        (long long )b) - (long long )f >= 0LL) && (5LL + (long long )a) - (long long
        )c >= 0LL) && (5LL + (long long )a) - (long long )d >= 0LL) && (5LL + (long
        long )a) - (long long )e >= 0LL) && (5LL + (long long )a) - (long long )f
        >= 0LL) && (9LL - (long long )b) - (long long )c >= 0LL) && (9LL - (long long
        )b) - (long long )d >= 0LL) && (9LL - (long long )b) - (long long )e >= 0LL)
        && (9LL - (long long )b) - (long long )f >= 0LL) && a == 4) && b == 3)) ||
        ((((((((((((((((((((((((((((-11LL + (long long )b) + (long long )c >= 0LL
        && (-11LL + (long long )b) + (long long )d >= 0LL) && (-11LL + (long long
        )b) + (long long )e >= 0LL) && (-11LL + (long long )b) + (long long )f >=
        0LL) && (-7LL + (long long )a) + (long long )c >= 0LL) && (-7LL + (long long
        )a) + (long long )d >= 0LL) && (-7LL + (long long )a) + (long long )e >= 0LL)
        && (-7LL + (long long )a) + (long long )f >= 0LL) && (-6LL + (long long )a)
        + (long long )b >= 0LL) && (-1LL - (long long )b) + (long long )c >= 0LL)
        && (-1LL - (long long )b) + (long long )d >= 0LL) && (-1LL - (long long )b)
        + (long long )e >= 0LL) && (-1LL - (long long )b) + (long long )f >= 0LL)
        && (1LL + (long long )b) - (long long )c >= 0LL) && (1LL + (long long )b)
        - (long long )d >= 0LL) && (1LL + (long long )b) - (long long )e >= 0LL) &&
        (1LL + (long long )b) - (long long )f >= 0LL) && (4LL + (long long )a) - (long
        long )b >= 0LL) && (5LL + (long long )a) - (long long )c >= 0LL) && (5LL +
        (long long )a) - (long long )d >= 0LL) && (5LL + (long long )a) - (long long
        )e >= 0LL) && (5LL + (long long )a) - (long long )f >= 0LL) && (11LL - (long
        long )b) - (long long )c >= 0LL) && (11LL - (long long )b) - (long long )d
        >= 0LL) && (11LL - (long long )b) - (long long )e >= 0LL) && (11LL - (long
        long )b) - (long long )f >= 0LL) && a == 1) && b == 5)) || ((((((((((((((((((((((((((((-8LL
        + (long long )b) + (long long )c >= 0LL && (-8LL + (long long )b) + (long
        long )d >= 0LL) && (-8LL + (long long )b) + (long long )e >= 0LL) && (-8LL
        + (long long )b) + (long long )f >= 0LL) && (-7LL + (long long )a) + (long
        long )c >= 0LL) && (-7LL + (long long )a) + (long long )d >= 0LL) && (-7LL
        + (long long )a) + (long long )e >= 0LL) && (-7LL + (long long )a) + (long
        long )f >= 0LL) && (-3LL + (long long )a) + (long long )b >= 0LL) && (-4LL
        - (long long )b) + (long long )c >= 0LL) && (-4LL - (long long )b) + (long
        long )d >= 0LL) && (-4LL - (long long )b) + (long long )e >= 0LL) && (-4LL
        - (long long )b) + (long long )f >= 0LL) && (1LL + (long long )a) - (long
        long )b >= 0LL) && (4LL + (long long )b) - (long long )c >= 0LL) && (4LL +
        (long long )b) - (long long )d >= 0LL) && (4LL + (long long )b) - (long long
        )e >= 0LL) && (4LL + (long long )b) - (long long )f >= 0LL) && (5LL + (long
        long )a) - (long long )c >= 0LL) && (5LL + (long long )a) - (long long )d
        >= 0LL) && (5LL + (long long )a) - (long long )e >= 0LL) && (5LL + (long long
        )a) - (long long )f >= 0LL) && (8LL - (long long )b) - (long long )c >= 0LL)
        && (8LL - (long long )b) - (long long )d >= 0LL) && (8LL - (long long )b)
        - (long long )e >= 0LL) && (8LL - (long long )b) - (long long )f >= 0LL) &&
        a == 4) && b == 2)) || ((((((((((((((((((((((((((((-10LL + (long long )b)
        + (long long )c >= 0LL && (-10LL + (long long )b) + (long long )d >= 0LL)
        && (-10LL + (long long )b) + (long long )e >= 0LL) && (-10LL + (long long
        )b) + (long long )f >= 0LL) && (-7LL + (long long )a) + (long long )c >= 0LL)
        && (-7LL + (long long )a) + (long long )d >= 0LL) && (-7LL + (long long )a)
        + (long long )e >= 0LL) && (-7LL + (long long )a) + (long long )f >= 0LL)
        && (-5LL + (long long )a) + (long long )b >= 0LL) && (-2LL - (long long )b)
        + (long long )c >= 0LL) && (-2LL - (long long )b) + (long long )d >= 0LL)
        && (-2LL - (long long )b) + (long long )e >= 0LL) && (-2LL - (long long )b)
        + (long long )f >= 0LL) && (2LL + (long long )b) - (long long )c >= 0LL) &&
        (2LL + (long long )b) - (long long )d >= 0LL) && (2LL + (long long )b) - (long
        long )e >= 0LL) && (2LL + (long long )b) - (long long )f >= 0LL) && (3LL +
        (long long )a) - (long long )b >= 0LL) && (5LL + (long long )a) - (long long
        )c >= 0LL) && (5LL + (long long )a) - (long long )d >= 0LL) && (5LL + (long
        long )a) - (long long )e >= 0LL) && (5LL + (long long )a) - (long long )f
        >= 0LL) && (10LL - (long long )b) - (long long )c >= 0LL) && (10LL - (long
        long )b) - (long long )d >= 0LL) && (10LL - (long long )b) - (long long )e
        >= 0LL) && (10LL - (long long )b) - (long long )f >= 0LL) && a == 1) && b
        == 4)) || ((((((((((((((((((((((((((((-7LL + (long long )a) + (long long )c
        >= 0LL && (-7LL + (long long )a) + (long long )d >= 0LL) && (-7LL + (long
        long )a) + (long long )e >= 0LL) && (-7LL + (long long )a) + (long long )f
        >= 0LL) && (-7LL + (long long )b) + (long long )c >= 0LL) && (-7LL + (long
        long )b) + (long long )d >= 0LL) && (-7LL + (long long )b) + (long long )e
        >= 0LL) && (-7LL + (long long )b) + (long long )f >= 0LL) && (-2LL + (long
        long )a) + (long long )b >= 0LL) && (-5LL - (long long )b) + (long long )c
        >= 0LL) && (-5LL - (long long )b) + (long long )d >= 0LL) && (-5LL - (long
        long )b) + (long long )e >= 0LL) && (-5LL - (long long )b) + (long long )f
        >= 0LL) && (5LL + (long long )a) - (long long )c >= 0LL) && (5LL + (long long
        )a) - (long long )d >= 0LL) && (5LL + (long long )a) - (long long )e >= 0LL)
        && (5LL + (long long )a) - (long long )f >= 0LL) && (5LL + (long long )b)
        - (long long )c >= 0LL) && (5LL + (long long )b) - (long long )d >= 0LL) &&
        (5LL + (long long )b) - (long long )e >= 0LL) && (5LL + (long long )b) - (long
        long )f >= 0LL) && (7LL - (long long )b) - (long long )c >= 0LL) && (7LL -
        (long long )b) - (long long )d >= 0LL) && (7LL - (long long )b) - (long long
        )e >= 0LL) && (7LL - (long long )b) - (long long )f >= 0LL) && (long long
        )a - (long long )b >= 0LL) && a == 4) && b == 1)) || ((((((((((((((((((((((((((((-9LL
        + (long long )b) + (long long )c >= 0LL && (-9LL + (long long )b) + (long
        long )d >= 0LL) && (-9LL + (long long )b) + (long long )e >= 0LL) && (-9LL
        + (long long )b) + (long long )f >= 0LL) && (-7LL + (long long )a) + (long
        long )c >= 0LL) && (-7LL + (long long )a) + (long long )d >= 0LL) && (-7LL
        + (long long )a) + (long long )e >= 0LL) && (-7LL + (long long )a) + (long
        long )f >= 0LL) && (-4LL + (long long )a) + (long long )b >= 0LL) && (-3LL
        - (long long )b) + (long long )c >= 0LL) && (-3LL - (long long )b) + (long
        long )d >= 0LL) && (-3LL - (long long )b) + (long long )e >= 0LL) && (-3LL
        - (long long )b) + (long long )f >= 0LL) && (2LL + (long long )a) - (long
        long )b >= 0LL) && (3LL + (long long )b) - (long long )c >= 0LL) && (3LL +
        (long long )b) - (long long )d >= 0LL) && (3LL + (long long )b) - (long long
        )e >= 0LL) && (3LL + (long long )b) - (long long )f >= 0LL) && (5LL + (long
        long )a) - (long long )c >= 0LL) && (5LL + (long long )a) - (long long )d
        >= 0LL) && (5LL + (long long )a) - (long long )e >= 0LL) && (5LL + (long long
        )a) - (long long )f >= 0LL) && (9LL - (long long )b) - (long long )c >= 0LL)
        && (9LL - (long long )b) - (long long )d >= 0LL) && (9LL - (long long )b)
        - (long long )e >= 0LL) && (9LL - (long long )b) - (long long )f >= 0LL) &&
        a == 1) && b == 3)) || (((((((((((((((((((((((((((((((((((((((-10LL + (long
        long )a) + (long long )c >= 0LL && (-10LL + (long long )a) + (long long )d
        >= 0LL) && (-10LL + (long long )a) + (long long )e >= 0LL) && (-10LL + (long
        long )a) + (long long )f >= 0LL) && (-6LL + (long long )b) + (long long )c
        >= 0LL) && (-6LL + (long long )b) + (long long )d >= 0LL) && (-6LL + (long
        long )b) + (long long )e >= 0LL) && (-6LL + (long long )b) + (long long )f
        >= 0LL) && (-4LL + (long long )a) + (long long )b >= 0LL) && (-6LL - (long
        long )b) + (long long )c >= 0LL) && (-6LL - (long long )b) + (long long )d
        >= 0LL) && (-6LL - (long long )b) + (long long )e >= 0LL) && (-6LL - (long
        long )b) + (long long )f >= 0LL) && (-2LL - (long long )a) + (long long )c
        >= 0LL) && (-2LL - (long long )a) + (long long )d >= 0LL) && (-2LL - (long
        long )a) + (long long )e >= 0LL) && (-2LL - (long long )a) + (long long )f
        >= 0LL) && (4LL - (long long )a) + (long long )b >= 0LL) && (-4LL + (long
        long )a) - (long long )b >= 0LL) && (2LL + (long long )a) - (long long )c
        >= 0LL) && (2LL + (long long )a) - (long long )d >= 0LL) && (2LL + (long long
        )a) - (long long )e >= 0LL) && (2LL + (long long )a) - (long long )f >= 0LL)
        && (6LL + (long long )b) - (long long )c >= 0LL) && (6LL + (long long )b)
        - (long long )d >= 0LL) && (6LL + (long long )b) - (long long )e >= 0LL) &&
        (6LL + (long long )b) - (long long )f >= 0LL) && (4LL - (long long )a) - (long
        long )b >= 0LL) && (6LL - (long long )b) - (long long )c >= 0LL) && (6LL -
        (long long )b) - (long long )d >= 0LL) && (6LL - (long long )b) - (long long
        )e >= 0LL) && (6LL - (long long )b) - (long long )f >= 0LL) && (10LL - (long
        long )a) - (long long )c >= 0LL) && (10LL - (long long )a) - (long long )d
        >= 0LL) && (10LL - (long long )a) - (long long )e >= 0LL) && (10LL - (long
        long )a) - (long long )f >= 0LL) && 0 == b) && a == 4) && b == 0)) || ((((((((((((((((((((((((((((-8LL
        + (long long )b) + (long long )c >= 0LL && (-8LL + (long long )b) + (long
        long )d >= 0LL) && (-8LL + (long long )b) + (long long )e >= 0LL) && (-8LL
        + (long long )b) + (long long )f >= 0LL) && (-7LL + (long long )a) + (long
        long )c >= 0LL) && (-7LL + (long long )a) + (long long )d >= 0LL) && (-7LL
        + (long long )a) + (long long )e >= 0LL) && (-7LL + (long long )a) + (long
        long )f >= 0LL) && (-3LL + (long long )a) + (long long )b >= 0LL) && (-4LL
        - (long long )b) + (long long )c >= 0LL) && (-4LL - (long long )b) + (long
        long )d >= 0LL) && (-4LL - (long long )b) + (long long )e >= 0LL) && (-4LL
        - (long long )b) + (long long )f >= 0LL) && (1LL + (long long )a) - (long
        long )b >= 0LL) && (4LL + (long long )b) - (long long )c >= 0LL) && (4LL +
        (long long )b) - (long long )d >= 0LL) && (4LL + (long long )b) - (long long
        )e >= 0LL) && (4LL + (long long )b) - (long long )f >= 0LL) && (5LL + (long
        long )a) - (long long )c >= 0LL) && (5LL + (long long )a) - (long long )d
        >= 0LL) && (5LL + (long long )a) - (long long )e >= 0LL) && (5LL + (long long
        )a) - (long long )f >= 0LL) && (8LL - (long long )b) - (long long )c >= 0LL)
        && (8LL - (long long )b) - (long long )d >= 0LL) && (8LL - (long long )b)
        - (long long )e >= 0LL) && (8LL - (long long )b) - (long long )f >= 0LL) &&
        a == 1) && b == 2)) || ((((((((((((((((((((((((((((-7LL + (long long )a) +
        (long long )c >= 0LL && (-7LL + (long long )a) + (long long )d >= 0LL) &&
        (-7LL + (long long )a) + (long long )e >= 0LL) && (-7LL + (long long )a) +
        (long long )f >= 0LL) && (-7LL + (long long )b) + (long long )c >= 0LL) &&
        (-7LL + (long long )b) + (long long )d >= 0LL) && (-7LL + (long long )b) +
        (long long )e >= 0LL) && (-7LL + (long long )b) + (long long )f >= 0LL) &&
        (-2LL + (long long )a) + (long long )b >= 0LL) && (-5LL - (long long )b) +
        (long long )c >= 0LL) && (-5LL - (long long )b) + (long long )d >= 0LL) &&
        (-5LL - (long long )b) + (long long )e >= 0LL) && (-5LL - (long long )b) +
        (long long )f >= 0LL) && (5LL + (long long )a) - (long long )c >= 0LL) &&
        (5LL + (long long )a) - (long long )d >= 0LL) && (5LL + (long long )a) - (long
        long )e >= 0LL) && (5LL + (long long )a) - (long long )f >= 0LL) && (5LL +
        (long long )b) - (long long )c >= 0LL) && (5LL + (long long )b) - (long long
        )d >= 0LL) && (5LL + (long long )b) - (long long )e >= 0LL) && (5LL + (long
        long )b) - (long long )f >= 0LL) && (7LL - (long long )b) - (long long )c
        >= 0LL) && (7LL - (long long )b) - (long long )d >= 0LL) && (7LL - (long long
        )b) - (long long )e >= 0LL) && (7LL - (long long )b) - (long long )f >= 0LL)
        && (long long )a - (long long )b >= 0LL) && a == 1) && b == 1)) || ((((((((((((((((((((((((((((-12LL
        + (long long )b) + (long long )c >= 0LL && (-12LL + (long long )b) + (long
        long )d >= 0LL) && (-12LL + (long long )b) + (long long )e >= 0LL) && (-12LL
        + (long long )b) + (long long )f >= 0LL) && (-7LL + (long long )a) + (long
        long )b >= 0LL) && (-7LL + (long long )a) + (long long )c >= 0LL) && (-7LL
        + (long long )a) + (long long )d >= 0LL) && (-7LL + (long long )a) + (long
        long )e >= 0LL) && (-7LL + (long long )a) + (long long )f >= 0LL) && (0LL
        - (long long )b) + (long long )c >= 0LL) && (0LL - (long long )b) + (long
        long )d >= 0LL) && (0LL - (long long )b) + (long long )e >= 0LL) && (0LL -
        (long long )b) + (long long )f >= 0LL) && (5LL + (long long )a) - (long long
        )b >= 0LL) && (5LL + (long long )a) - (long long )c >= 0LL) && (5LL + (long
        long )a) - (long long )d >= 0LL) && (5LL + (long long )a) - (long long )e
        >= 0LL) && (5LL + (long long )a) - (long long )f >= 0LL) && (12LL - (long
        long )b) - (long long )c >= 0LL) && (12LL - (long long )b) - (long long )d
        >= 0LL) && (12LL - (long long )b) - (long long )e >= 0LL) && (12LL - (long
        long )b) - (long long )f >= 0LL) && (long long )b - (long long )c >= 0LL)
        && (long long )b - (long long )d >= 0LL) && (long long )b - (long long )e
        >= 0LL) && (long long )b - (long long )f >= 0LL) && a == 3) && b == 6)) ||
        (((((((((((((((((((((((((((((((((((((((-7LL + (long long )a) + (long long
        )c >= 0LL && (-7LL + (long long )a) + (long long )d >= 0LL) && (-7LL + (long
        long )a) + (long long )e >= 0LL) && (-7LL + (long long )a) + (long long )f
        >= 0LL) && (-6LL + (long long )b) + (long long )c >= 0LL) && (-6LL + (long
        long )b) + (long long )d >= 0LL) && (-6LL + (long long )b) + (long long )e
        >= 0LL) && (-6LL + (long long )b) + (long long )f >= 0LL) && (-1LL + (long
        long )a) + (long long )b >= 0LL) && (-6LL - (long long )b) + (long long )c
        >= 0LL) && (-6LL - (long long )b) + (long long )d >= 0LL) && (-6LL - (long
        long )b) + (long long )e >= 0LL) && (-6LL - (long long )b) + (long long )f
        >= 0LL) && (-5LL - (long long )a) + (long long )c >= 0LL) && (-5LL - (long
        long )a) + (long long )d >= 0LL) && (-5LL - (long long )a) + (long long )e
        >= 0LL) && (-5LL - (long long )a) + (long long )f >= 0LL) && (1LL - (long
        long )a) + (long long )b >= 0LL) && (-1LL + (long long )a) - (long long )b
        >= 0LL) && (5LL + (long long )a) - (long long )c >= 0LL) && (5LL + (long long
        )a) - (long long )d >= 0LL) && (5LL + (long long )a) - (long long )e >= 0LL)
        && (5LL + (long long )a) - (long long )f >= 0LL) && (6LL + (long long )b)
        - (long long )c >= 0LL) && (6LL + (long long )b) - (long long )d >= 0LL) &&
        (6LL + (long long )b) - (long long )e >= 0LL) && (6LL + (long long )b) - (long
        long )f >= 0LL) && (1LL - (long long )a) - (long long )b >= 0LL) && (6LL -
        (long long )b) - (long long )c >= 0LL) && (6LL - (long long )b) - (long long
        )d >= 0LL) && (6LL - (long long )b) - (long long )e >= 0LL) && (6LL - (long
        long )b) - (long long )f >= 0LL) && (7LL - (long long )a) - (long long )c
        >= 0LL) && (7LL - (long long )a) - (long long )d >= 0LL) && (7LL - (long long
        )a) - (long long )e >= 0LL) && (7LL - (long long )a) - (long long )f >= 0LL)
        && 0 == b) && a == 1) && b == 0)) || ((((((((((((((((((((((((((((-11LL + (long
        long )b) + (long long )c >= 0LL && (-11LL + (long long )b) + (long long )d
        >= 0LL) && (-11LL + (long long )b) + (long long )e >= 0LL) && (-11LL + (long
        long )b) + (long long )f >= 0LL) && (-7LL + (long long )a) + (long long )c
        >= 0LL) && (-7LL + (long long )a) + (long long )d >= 0LL) && (-7LL + (long
        long )a) + (long long )e >= 0LL) && (-7LL + (long long )a) + (long long )f
        >= 0LL) && (-6LL + (long long )a) + (long long )b >= 0LL) && (-1LL - (long
        long )b) + (long long )c >= 0LL) && (-1LL - (long long )b) + (long long )d
        >= 0LL) && (-1LL - (long long )b) + (long long )e >= 0LL) && (-1LL - (long
        long )b) + (long long )f >= 0LL) && (1LL + (long long )b) - (long long )c
        >= 0LL) && (1LL + (long long )b) - (long long )d >= 0LL) && (1LL + (long long
        )b) - (long long )e >= 0LL) && (1LL + (long long )b) - (long long )f >= 0LL)
        && (4LL + (long long )a) - (long long )b >= 0LL) && (5LL + (long long )a)
        - (long long )c >= 0LL) && (5LL + (long long )a) - (long long )d >= 0LL) &&
        (5LL + (long long )a) - (long long )e >= 0LL) && (5LL + (long long )a) - (long
        long )f >= 0LL) && (11LL - (long long )b) - (long long )c >= 0LL) && (11LL
        - (long long )b) - (long long )d >= 0LL) && (11LL - (long long )b) - (long
        long )e >= 0LL) && (11LL - (long long )b) - (long long )f >= 0LL) && a ==
        3) && b == 5)) || ((((((((((((((((((((((((((((-10LL + (long long )b) + (long
        long )c >= 0LL && (-10LL + (long long )b) + (long long )d >= 0LL) && (-10LL
        + (long long )b) + (long long )e >= 0LL) && (-10LL + (long long )b) + (long
        long )f >= 0LL) && (-7LL + (long long )a) + (long long )c >= 0LL) && (-7LL
        + (long long )a) + (long long )d >= 0LL) && (-7LL + (long long )a) + (long
        long )e >= 0LL) && (-7LL + (long long )a) + (long long )f >= 0LL) && (-5LL
        + (long long )a) + (long long )b >= 0LL) && (-2LL - (long long )b) + (long
        long )c >= 0LL) && (-2LL - (long long )b) + (long long )d >= 0LL) && (-2LL
        - (long long )b) + (long long )e >= 0LL) && (-2LL - (long long )b) + (long
        long )f >= 0LL) && (2LL + (long long )b) - (long long )c >= 0LL) && (2LL +
        (long long )b) - (long long )d >= 0LL) && (2LL + (long long )b) - (long long
        )e >= 0LL) && (2LL + (long long )b) - (long long )f >= 0LL) && (3LL + (long
        long )a) - (long long )b >= 0LL) && (5LL + (long long )a) - (long long )c
        >= 0LL) && (5LL + (long long )a) - (long long )d >= 0LL) && (5LL + (long long
        )a) - (long long )e >= 0LL) && (5LL + (long long )a) - (long long )f >= 0LL)
        && (10LL - (long long )b) - (long long )c >= 0LL) && (10LL - (long long )b)
        - (long long )d >= 0LL) && (10LL - (long long )b) - (long long )e >= 0LL)
        && (10LL - (long long )b) - (long long )f >= 0LL) && a == 3) && b == 4)) ||
        (((((((((((((((((((((((((((((((((((((((-12LL + (long long )b) + (long long
        )c >= 0LL && (-12LL + (long long )b) + (long long )d >= 0LL) && (-12LL + (long
        long )b) + (long long )e >= 0LL) && (-12LL + (long long )b) + (long long )f
        >= 0LL) && (-6LL + (long long )a) + (long long )b >= 0LL) && (-6LL + (long
        long )a) + (long long )c >= 0LL) && (-6LL + (long long )a) + (long long )d
        >= 0LL) && (-6LL + (long long )a) + (long long )e >= 0LL) && (-6LL + (long
        long )a) + (long long )f >= 0LL) && (-6LL - (long long )a) + (long long )b
        >= 0LL) && (-6LL - (long long )a) + (long long )c >= 0LL) && (-6LL - (long
        long )a) + (long long )d >= 0LL) && (-6LL - (long long )a) + (long long )e
        >= 0LL) && (-6LL - (long long )a) + (long long )f >= 0LL) && (0LL - (long
        long )b) + (long long )c >= 0LL) && (0LL - (long long )b) + (long long )d
        >= 0LL) && (0LL - (long long )b) + (long long )e >= 0LL) && (0LL - (long long
        )b) + (long long )f >= 0LL) && (6LL + (long long )a) - (long long )b >= 0LL)
        && (6LL + (long long )a) - (long long )c >= 0LL) && (6LL + (long long )a)
        - (long long )d >= 0LL) && (6LL + (long long )a) - (long long )e >= 0LL) &&
        (6LL + (long long )a) - (long long )f >= 0LL) && (6LL - (long long )a) - (long
        long )b >= 0LL) && (6LL - (long long )a) - (long long )c >= 0LL) && (6LL -
        (long long )a) - (long long )d >= 0LL) && (6LL - (long long )a) - (long long
        )e >= 0LL) && (6LL - (long long )a) - (long long )f >= 0LL) && (12LL - (long
        long )b) - (long long )c >= 0LL) && (12LL - (long long )b) - (long long )d
        >= 0LL) && (12LL - (long long )b) - (long long )e >= 0LL) && (12LL - (long
        long )b) - (long long )f >= 0LL) && (long long )b - (long long )c >= 0LL)
        && (long long )b - (long long )d >= 0LL) && (long long )b - (long long )e
        >= 0LL) && (long long )b - (long long )f >= 0LL) && 0 == a) && a == 0) &&
        b == 6)) || ((((((((((((((((((((((((((((-9LL + (long long )b) + (long long
        )c >= 0LL && (-9LL + (long long )b) + (long long )d >= 0LL) && (-9LL + (long
        long )b) + (long long )e >= 0LL) && (-9LL + (long long )b) + (long long )f
        >= 0LL) && (-7LL + (long long )a) + (long long )c >= 0LL) && (-7LL + (long
        long )a) + (long long )d >= 0LL) && (-7LL + (long long )a) + (long long )e
        >= 0LL) && (-7LL + (long long )a) + (long long )f >= 0LL) && (-4LL + (long
        long )a) + (long long )b >= 0LL) && (-3LL - (long long )b) + (long long )c
        >= 0LL) && (-3LL - (long long )b) + (long long )d >= 0LL) && (-3LL - (long
        long )b) + (long long )e >= 0LL) && (-3LL - (long long )b) + (long long )f
        >= 0LL) && (2LL + (long long )a) - (long long )b >= 0LL) && (3LL + (long long
        )b) - (long long )c >= 0LL) && (3LL + (long long )b) - (long long )d >= 0LL)
        && (3LL + (long long )b) - (long long )e >= 0LL) && (3LL + (long long )b)
        - (long long )f >= 0LL) && (5LL + (long long )a) - (long long )c >= 0LL) &&
        (5LL + (long long )a) - (long long )d >= 0LL) && (5LL + (long long )a) - (long
        long )e >= 0LL) && (5LL + (long long )a) - (long long )f >= 0LL) && (9LL -
        (long long )b) - (long long )c >= 0LL) && (9LL - (long long )b) - (long long
        )d >= 0LL) && (9LL - (long long )b) - (long long )e >= 0LL) && (9LL - (long
        long )b) - (long long )f >= 0LL) && a == 3) && b == 3)) || (((((((((((((((((((((((((((((((((((((((-11LL
        + (long long )b) + (long long )c >= 0LL && (-11LL + (long long )b) + (long
        long )d >= 0LL) && (-11LL + (long long )b) + (long long )e >= 0LL) && (-11LL
        + (long long )b) + (long long )f >= 0LL) && (-6LL + (long long )a) + (long
        long )c >= 0LL) && (-6LL + (long long )a) + (long long )d >= 0LL) && (-6LL
        + (long long )a) + (long long )e >= 0LL) && (-6LL + (long long )a) + (long
        long )f >= 0LL) && (-5LL + (long long )a) + (long long )b >= 0LL) && (-6LL
        - (long long )a) + (long long )c >= 0LL) && (-6LL - (long long )a) + (long
        long )d >= 0LL) && (-6LL - (long long )a) + (long long )e >= 0LL) && (-6LL
        - (long long )a) + (long long )f >= 0LL) && (-5LL - (long long )a) + (long
        long )b >= 0LL) && (-1LL - (long long )b) + (long long )c >= 0LL) && (-1LL
        - (long long )b) + (long long )d >= 0LL) && (-1LL - (long long )b) + (long
        long )e >= 0LL) && (-1LL - (long long )b) + (long long )f >= 0LL) && (1LL
        + (long long )b) - (long long )c >= 0LL) && (1LL + (long long )b) - (long
        long )d >= 0LL) && (1LL + (long long )b) - (long long )e >= 0LL) && (1LL +
        (long long )b) - (long long )f >= 0LL) && (5LL + (long long )a) - (long long
        )b >= 0LL) && (6LL + (long long )a) - (long long )c >= 0LL) && (6LL + (long
        long )a) - (long long )d >= 0LL) && (6LL + (long long )a) - (long long )e
        >= 0LL) && (6LL + (long long )a) - (long long )f >= 0LL) && (5LL - (long long
        )a) - (long long )b >= 0LL) && (6LL - (long long )a) - (long long )c >= 0LL)
        && (6LL - (long long )a) - (long long )d >= 0LL) && (6LL - (long long )a)
        - (long long )e >= 0LL) && (6LL - (long long )a) - (long long )f >= 0LL) &&
        (11LL - (long long )b) - (long long )c >= 0LL) && (11LL - (long long )b) -
        (long long )d >= 0LL) && (11LL - (long long )b) - (long long )e >= 0LL) &&
        (11LL - (long long )b) - (long long )f >= 0LL) && 0 == a) && a == 0) && b
        == 5)) || ((((((((((((((((((((((((((((-8LL + (long long )b) + (long long )c
        >= 0LL && (-8LL + (long long )b) + (long long )d >= 0LL) && (-8LL + (long
        long )b) + (long long )e >= 0LL) && (-8LL + (long long )b) + (long long )f
        >= 0LL) && (-7LL + (long long )a) + (long long )c >= 0LL) && (-7LL + (long
        long )a) + (long long )d >= 0LL) && (-7LL + (long long )a) + (long long )e
        >= 0LL) && (-7LL + (long long )a) + (long long )f >= 0LL) && (-3LL + (long
        long )a) + (long long )b >= 0LL) && (-4LL - (long long )b) + (long long )c
        >= 0LL) && (-4LL - (long long )b) + (long long )d >= 0LL) && (-4LL - (long
        long )b) + (long long )e >= 0LL) && (-4LL - (long long )b) + (long long )f
        >= 0LL) && (1LL + (long long )a) - (long long )b >= 0LL) && (4LL + (long long
        )b) - (long long )c >= 0LL) && (4LL + (long long )b) - (long long )d >= 0LL)
        && (4LL + (long long )b) - (long long )e >= 0LL) && (4LL + (long long )b)
        - (long long )f >= 0LL) && (5LL + (long long )a) - (long long )c >= 0LL) &&
        (5LL + (long long )a) - (long long )d >= 0LL) && (5LL + (long long )a) - (long
        long )e >= 0LL) && (5LL + (long long )a) - (long long )f >= 0LL) && (8LL -
        (long long )b) - (long long )c >= 0LL) && (8LL - (long long )b) - (long long
        )d >= 0LL) && (8LL - (long long )b) - (long long )e >= 0LL) && (8LL - (long
        long )b) - (long long )f >= 0LL) && a == 3) && b == 2)) || (((((((((((((((((((((((((((((((((((((((-10LL
        + (long long )b) + (long long )c >= 0LL && (-10LL + (long long )b) + (long
        long )d >= 0LL) && (-10LL + (long long )b) + (long long )e >= 0LL) && (-10LL
        + (long long )b) + (long long )f >= 0LL) && (-6LL + (long long )a) + (long
        long )c >= 0LL) && (-6LL + (long long )a) + (long long )d >= 0LL) && (-6LL
        + (long long )a) + (long long )e >= 0LL) && (-6LL + (long long )a) + (long
        long )f >= 0LL) && (-4LL + (long long )a) + (long long )b >= 0LL) && (-6LL
        - (long long )a) + (long long )c >= 0LL) && (-6LL - (long long )a) + (long
        long )d >= 0LL) && (-6LL - (long long )a) + (long long )e >= 0LL) && (-6LL
        - (long long )a) + (long long )f >= 0LL) && (-4LL - (long long )a) + (long
        long )b >= 0LL) && (-2LL - (long long )b) + (long long )c >= 0LL) && (-2LL
        - (long long )b) + (long long )d >= 0LL) && (-2LL - (long long )b) + (long
        long )e >= 0LL) && (-2LL - (long long )b) + (long long )f >= 0LL) && (2LL
        + (long long )b) - (long long )c >= 0LL) && (2LL + (long long )b) - (long
        long )d >= 0LL) && (2LL + (long long )b) - (long long )e >= 0LL) && (2LL +
        (long long )b) - (long long )f >= 0LL) && (4LL + (long long )a) - (long long
        )b >= 0LL) && (6LL + (long long )a) - (long long )c >= 0LL) && (6LL + (long
        long )a) - (long long )d >= 0LL) && (6LL + (long long )a) - (long long )e
        >= 0LL) && (6LL + (long long )a) - (long long )f >= 0LL) && (4LL - (long long
        )a) - (long long )b >= 0LL) && (6LL - (long long )a) - (long long )c >= 0LL)
        && (6LL - (long long )a) - (long long )d >= 0LL) && (6LL - (long long )a)
        - (long long )e >= 0LL) && (6LL - (long long )a) - (long long )f >= 0LL) &&
        (10LL - (long long )b) - (long long )c >= 0LL) && (10LL - (long long )b) -
        (long long )d >= 0LL) && (10LL - (long long )b) - (long long )e >= 0LL) &&
        (10LL - (long long )b) - (long long )f >= 0LL) && 0 == a) && a == 0) && b
        == 4)) || ((((((((((((((((((((((((((((-7LL + (long long )a) + (long long )c
        >= 0LL && (-7LL + (long long )a) + (long long )d >= 0LL) && (-7LL + (long
        long )a) + (long long )e >= 0LL) && (-7LL + (long long )a) + (long long )f
        >= 0LL) && (-7LL + (long long )b) + (long long )c >= 0LL) && (-7LL + (long
        long )b) + (long long )d >= 0LL) && (-7LL + (long long )b) + (long long )e
        >= 0LL) && (-7LL + (long long )b) + (long long )f >= 0LL) && (-2LL + (long
        long )a) + (long long )b >= 0LL) && (-5LL - (long long )b) + (long long )c
        >= 0LL) && (-5LL - (long long )b) + (long long )d >= 0LL) && (-5LL - (long
        long )b) + (long long )e >= 0LL) && (-5LL - (long long )b) + (long long )f
        >= 0LL) && (5LL + (long long )a) - (long long )c >= 0LL) && (5LL + (long long
        )a) - (long long )d >= 0LL) && (5LL + (long long )a) - (long long )e >= 0LL)
        && (5LL + (long long )a) - (long long )f >= 0LL) && (5LL + (long long )b)
        - (long long )c >= 0LL) && (5LL + (long long )b) - (long long )d >= 0LL) &&
        (5LL + (long long )b) - (long long )e >= 0LL) && (5LL + (long long )b) - (long
        long )f >= 0LL) && (7LL - (long long )b) - (long long )c >= 0LL) && (7LL -
        (long long )b) - (long long )d >= 0LL) && (7LL - (long long )b) - (long long
        )e >= 0LL) && (7LL - (long long )b) - (long long )f >= 0LL) && (long long
        )a - (long long )b >= 0LL) && a == 3) && b == 1)) || ((((((((((((((((((((((((((((-12LL
        + (long long )b) + (long long )c >= 0LL && (-12LL + (long long )b) + (long
        long )d >= 0LL) && (-12LL + (long long )b) + (long long )e >= 0LL) && (-12LL
        + (long long )b) + (long long )f >= 0LL) && (-7LL + (long long )a) + (long
        long )b >= 0LL) && (-7LL + (long long )a) + (long long )c >= 0LL) && (-7LL
        + (long long )a) + (long long )d >= 0LL) && (-7LL + (long long )a) + (long
        long )e >= 0LL) && (-7LL + (long long )a) + (long long )f >= 0LL) && (0LL
        - (long long )b) + (long long )c >= 0LL) && (0LL - (long long )b) + (long
        long )d >= 0LL) && (0LL - (long long )b) + (long long )e >= 0LL) && (0LL -
        (long long )b) + (long long )f >= 0LL) && (5LL + (long long )a) - (long long
        )b >= 0LL) && (5LL + (long long )a) - (long long )c >= 0LL) && (5LL + (long
        long )a) - (long long )d >= 0LL) && (5LL + (long long )a) - (long long )e
        >= 0LL) && (5LL + (long long )a) - (long long )f >= 0LL) && (12LL - (long
        long )b) - (long long )c >= 0LL) && (12LL - (long long )b) - (long long )d
        >= 0LL) && (12LL - (long long )b) - (long long )e >= 0LL) && (12LL - (long
        long )b) - (long long )f >= 0LL) && (long long )b - (long long )c >= 0LL)
        && (long long )b - (long long )d >= 0LL) && (long long )b - (long long )e
        >= 0LL) && (long long )b - (long long )f >= 0LL) && a == 5) && b == 6)) ||
        (((((((((((((((((((((((((((((((((((((((-9LL + (long long )b) + (long long
        )c >= 0LL && (-9LL + (long long )b) + (long long )d >= 0LL) && (-9LL + (long
        long )b) + (long long )e >= 0LL) && (-9LL + (long long )b) + (long long )f
        >= 0LL) && (-6LL + (long long )a) + (long long )c >= 0LL) && (-6LL + (long
        long )a) + (long long )d >= 0LL) && (-6LL + (long long )a) + (long long )e
        >= 0LL) && (-6LL + (long long )a) + (long long )f >= 0LL) && (-3LL + (long
        long )a) + (long long )b >= 0LL) && (-6LL - (long long )a) + (long long )c
        >= 0LL) && (-6LL - (long long )a) + (long long )d >= 0LL) && (-6LL - (long
        long )a) + (long long )e >= 0LL) && (-6LL - (long long )a) + (long long )f
        >= 0LL) && (-3LL - (long long )a) + (long long )b >= 0LL) && (-3LL - (long
        long )b) + (long long )c >= 0LL) && (-3LL - (long long )b) + (long long )d
        >= 0LL) && (-3LL - (long long )b) + (long long )e >= 0LL) && (-3LL - (long
        long )b) + (long long )f >= 0LL) && (3LL + (long long )a) - (long long )b
        >= 0LL) && (3LL + (long long )b) - (long long )c >= 0LL) && (3LL + (long long
        )b) - (long long )d >= 0LL) && (3LL + (long long )b) - (long long )e >= 0LL)
        && (3LL + (long long )b) - (long long )f >= 0LL) && (6LL + (long long )a)
        - (long long )c >= 0LL) && (6LL + (long long )a) - (long long )d >= 0LL) &&
        (6LL + (long long )a) - (long long )e >= 0LL) && (6LL + (long long )a) - (long
        long )f >= 0LL) && (3LL - (long long )a) - (long long )b >= 0LL) && (6LL -
        (long long )a) - (long long )c >= 0LL) && (6LL - (long long )a) - (long long
        )d >= 0LL) && (6LL - (long long )a) - (long long )e >= 0LL) && (6LL - (long
        long )a) - (long long )f >= 0LL) && (9LL - (long long )b) - (long long )c
        >= 0LL) && (9LL - (long long )b) - (long long )d >= 0LL) && (9LL - (long long
        )b) - (long long )e >= 0LL) && (9LL - (long long )b) - (long long )f >= 0LL)
        && 0 == a) && a == 0) && b == 3)) || (((((((((((((((((((((((((((((((((((((((-9LL
        + (long long )a) + (long long )c >= 0LL && (-9LL + (long long )a) + (long
        long )d >= 0LL) && (-9LL + (long long )a) + (long long )e >= 0LL) && (-9LL
        + (long long )a) + (long long )f >= 0LL) && (-6LL + (long long )b) + (long
        long )c >= 0LL) && (-6LL + (long long )b) + (long long )d >= 0LL) && (-6LL
        + (long long )b) + (long long )e >= 0LL) && (-6LL + (long long )b) + (long
        long )f >= 0LL) && (-3LL + (long long )a) + (long long )b >= 0LL) && (-6LL
        - (long long )b) + (long long )c >= 0LL) && (-6LL - (long long )b) + (long
        long )d >= 0LL) && (-6LL - (long long )b) + (long long )e >= 0LL) && (-6LL
        - (long long )b) + (long long )f >= 0LL) && (-3LL - (long long )a) + (long
        long )c >= 0LL) && (-3LL - (long long )a) + (long long )d >= 0LL) && (-3LL
        - (long long )a) + (long long )e >= 0LL) && (-3LL - (long long )a) + (long
        long )f >= 0LL) && (3LL - (long long )a) + (long long )b >= 0LL) && (-3LL
        + (long long )a) - (long long )b >= 0LL) && (3LL + (long long )a) - (long
        long )c >= 0LL) && (3LL + (long long )a) - (long long )d >= 0LL) && (3LL +
        (long long )a) - (long long )e >= 0LL) && (3LL + (long long )a) - (long long
        )f >= 0LL) && (6LL + (long long )b) - (long long )c >= 0LL) && (6LL + (long
        long )b) - (long long )d >= 0LL) && (6LL + (long long )b) - (long long )e
        >= 0LL) && (6LL + (long long )b) - (long long )f >= 0LL) && (3LL - (long long
        )a) - (long long )b >= 0LL) && (6LL - (long long )b) - (long long )c >= 0LL)
        && (6LL - (long long )b) - (long long )d >= 0LL) && (6LL - (long long )b)
        - (long long )e >= 0LL) && (6LL - (long long )b) - (long long )f >= 0LL) &&
        (9LL - (long long )a) - (long long )c >= 0LL) && (9LL - (long long )a) - (long
        long )d >= 0LL) && (9LL - (long long )a) - (long long )e >= 0LL) && (9LL -
        (long long )a) - (long long )f >= 0LL) && 0 == b) && a == 3) && b == 0)) ||
        ((((((((((((((((((((((((((((-11LL + (long long )b) + (long long )c >= 0LL
        && (-11LL + (long long )b) + (long long )d >= 0LL) && (-11LL + (long long
        )b) + (long long )e >= 0LL) && (-11LL + (long long )b) + (long long )f >=
        0LL) && (-7LL + (long long )a) + (long long )c >= 0LL) && (-7LL + (long long
        )a) + (long long )d >= 0LL) && (-7LL + (long long )a) + (long long )e >= 0LL)
        && (-7LL + (long long )a) + (long long )f >= 0LL) && (-6LL + (long long )a)
        + (long long )b >= 0LL) && (-1LL - (long long )b) + (long long )c >= 0LL)
        && (-1LL - (long long )b) + (long long )d >= 0LL) && (-1LL - (long long )b)
        + (long long )e >= 0LL) && (-1LL - (long long )b) + (long long )f >= 0LL)
        && (1LL + (long long )b) - (long long )c >= 0LL) && (1LL + (long long )b)
        - (long long )d >= 0LL) && (1LL + (long long )b) - (long long )e >= 0LL) &&
        (1LL + (long long )b) - (long long )f >= 0LL) && (4LL + (long long )a) - (long
        long )b >= 0LL) && (5LL + (long long )a) - (long long )c >= 0LL) && (5LL +
        (long long )a) - (long long )d >= 0LL) && (5LL + (long long )a) - (long long
        )e >= 0LL) && (5LL + (long long )a) - (long long )f >= 0LL) && (11LL - (long
        long )b) - (long long )c >= 0LL) && (11LL - (long long )b) - (long long )d
        >= 0LL) && (11LL - (long long )b) - (long long )e >= 0LL) && (11LL - (long
        long )b) - (long long )f >= 0LL) && a == 5) && b == 5)) || (((((((((((((((((((((((((((((((((((((((-8LL
        + (long long )b) + (long long )c >= 0LL && (-8LL + (long long )b) + (long
        long )d >= 0LL) && (-8LL + (long long )b) + (long long )e >= 0LL) && (-8LL
        + (long long )b) + (long long )f >= 0LL) && (-6LL + (long long )a) + (long
        long )c >= 0LL) && (-6LL + (long long )a) + (long long )d >= 0LL) && (-6LL
        + (long long )a) + (long long )e >= 0LL) && (-6LL + (long long )a) + (long
        long )f >= 0LL) && (-2LL + (long long )a) + (long long )b >= 0LL) && (-6LL
        - (long long )a) + (long long )c >= 0LL) && (-6LL - (long long )a) + (long
        long )d >= 0LL) && (-6LL - (long long )a) + (long long )e >= 0LL) && (-6LL
        - (long long )a) + (long long )f >= 0LL) && (-4LL - (long long )b) + (long
        long )c >= 0LL) && (-4LL - (long long )b) + (long long )d >= 0LL) && (-4LL
        - (long long )b) + (long long )e >= 0LL) && (-4LL - (long long )b) + (long
        long )f >= 0LL) && (-2LL - (long long )a) + (long long )b >= 0LL) && (2LL
        + (long long )a) - (long long )b >= 0LL) && (4LL + (long long )b) - (long
        long )c >= 0LL) && (4LL + (long long )b) - (long long )d >= 0LL) && (4LL +
        (long long )b) - (long long )e >= 0LL) && (4LL + (long long )b) - (long long
        )f >= 0LL) && (6LL + (long long )a) - (long long )c >= 0LL) && (6LL + (long
        long )a) - (long long )d >= 0LL) && (6LL + (long long )a) - (long long )e
        >= 0LL) && (6LL + (long long )a) - (long long )f >= 0LL) && (2LL - (long long
        )a) - (long long )b >= 0LL) && (6LL - (long long )a) - (long long )c >= 0LL)
        && (6LL - (long long )a) - (long long )d >= 0LL) && (6LL - (long long )a)
        - (long long )e >= 0LL) && (6LL - (long long )a) - (long long )f >= 0LL) &&
        (8LL - (long long )b) - (long long )c >= 0LL) && (8LL - (long long )b) - (long
        long )d >= 0LL) && (8LL - (long long )b) - (long long )e >= 0LL) && (8LL -
        (long long )b) - (long long )f >= 0LL) && 0 == a) && a == 0) && b == 2)) ||
        ((((((((((((((((((((((((((((-10LL + (long long )b) + (long long )c >= 0LL
        && (-10LL + (long long )b) + (long long )d >= 0LL) && (-10LL + (long long
        )b) + (long long )e >= 0LL) && (-10LL + (long long )b) + (long long )f >=
        0LL) && (-7LL + (long long )a) + (long long )c >= 0LL) && (-7LL + (long long
        )a) + (long long )d >= 0LL) && (-7LL + (long long )a) + (long long )e >= 0LL)
        && (-7LL + (long long )a) + (long long )f >= 0LL) && (-5LL + (long long )a)
        + (long long )b >= 0LL) && (-2LL - (long long )b) + (long long )c >= 0LL)
        && (-2LL - (long long )b) + (long long )d >= 0LL) && (-2LL - (long long )b)
        + (long long )e >= 0LL) && (-2LL - (long long )b) + (long long )f >= 0LL)
        && (2LL + (long long )b) - (long long )c >= 0LL) && (2LL + (long long )b)
        - (long long )d >= 0LL) && (2LL + (long long )b) - (long long )e >= 0LL) &&
        (2LL + (long long )b) - (long long )f >= 0LL) && (3LL + (long long )a) - (long
        long )b >= 0LL) && (5LL + (long long )a) - (long long )c >= 0LL) && (5LL +
        (long long )a) - (long long )d >= 0LL) && (5LL + (long long )a) - (long long
        )e >= 0LL) && (5LL + (long long )a) - (long long )f >= 0LL) && (10LL - (long
        long )b) - (long long )c >= 0LL) && (10LL - (long long )b) - (long long )d
        >= 0LL) && (10LL - (long long )b) - (long long )e >= 0LL) && (10LL - (long
        long )b) - (long long )f >= 0LL) && a == 5) && b == 4)) || (((((((((((((((((((((((((((((((((((((((-7LL
        + (long long )b) + (long long )c >= 0LL && (-7LL + (long long )b) + (long
        long )d >= 0LL) && (-7LL + (long long )b) + (long long )e >= 0LL) && (-7LL
        + (long long )b) + (long long )f >= 0LL) && (-6LL + (long long )a) + (long
        long )c >= 0LL) && (-6LL + (long long )a) + (long long )d >= 0LL) && (-6LL
        + (long long )a) + (long long )e >= 0LL) && (-6LL + (long long )a) + (long
        long )f >= 0LL) && (-1LL + (long long )a) + (long long )b >= 0LL) && (-6LL
        - (long long )a) + (long long )c >= 0LL) && (-6LL - (long long )a) + (long
        long )d >= 0LL) && (-6LL - (long long )a) + (long long )e >= 0LL) && (-6LL
        - (long long )a) + (long long )f >= 0LL) && (-5LL - (long long )b) + (long
        long )c >= 0LL) && (-5LL - (long long )b) + (long long )d >= 0LL) && (-5LL
        - (long long )b) + (long long )e >= 0LL) && (-5LL - (long long )b) + (long
        long )f >= 0LL) && (-1LL - (long long )a) + (long long )b >= 0LL) && (1LL
        + (long long )a) - (long long )b >= 0LL) && (5LL + (long long )b) - (long
        long )c >= 0LL) && (5LL + (long long )b) - (long long )d >= 0LL) && (5LL +
        (long long )b) - (long long )e >= 0LL) && (5LL + (long long )b) - (long long
        )f >= 0LL) && (6LL + (long long )a) - (long long )c >= 0LL) && (6LL + (long
        long )a) - (long long )d >= 0LL) && (6LL + (long long )a) - (long long )e
        >= 0LL) && (6LL + (long long )a) - (long long )f >= 0LL) && (1LL - (long long
        )a) - (long long )b >= 0LL) && (6LL - (long long )a) - (long long )c >= 0LL)
        && (6LL - (long long )a) - (long long )d >= 0LL) && (6LL - (long long )a)
        - (long long )e >= 0LL) && (6LL - (long long )a) - (long long )f >= 0LL) &&
        (7LL - (long long )b) - (long long )c >= 0LL) && (7LL - (long long )b) - (long
        long )d >= 0LL) && (7LL - (long long )b) - (long long )e >= 0LL) && (7LL -
        (long long )b) - (long long )f >= 0LL) && 0 == a) && a == 0) && b == 1)) ||
        ((((((((((((((((((((((((((((-12LL + (long long )b) + (long long )c >= 0LL
        && (-12LL + (long long )b) + (long long )d >= 0LL) && (-12LL + (long long
        )b) + (long long )e >= 0LL) && (-12LL + (long long )b) + (long long )f >=
        0LL) && (-7LL + (long long )a) + (long long )b >= 0LL) && (-7LL + (long long
        )a) + (long long )c >= 0LL) && (-7LL + (long long )a) + (long long )d >= 0LL)
        && (-7LL + (long long )a) + (long long )e >= 0LL) && (-7LL + (long long )a)
        + (long long )f >= 0LL) && (0LL - (long long )b) + (long long )c >= 0LL) &&
        (0LL - (long long )b) + (long long )d >= 0LL) && (0LL - (long long )b) + (long
        long )e >= 0LL) && (0LL - (long long )b) + (long long )f >= 0LL) && (5LL +
        (long long )a) - (long long )b >= 0LL) && (5LL + (long long )a) - (long long
        )c >= 0LL) && (5LL + (long long )a) - (long long )d >= 0LL) && (5LL + (long
        long )a) - (long long )e >= 0LL) && (5LL + (long long )a) - (long long )f
        >= 0LL) && (12LL - (long long )b) - (long long )c >= 0LL) && (12LL - (long
        long )b) - (long long )d >= 0LL) && (12LL - (long long )b) - (long long )e
        >= 0LL) && (12LL - (long long )b) - (long long )f >= 0LL) && (long long )b
        - (long long )c >= 0LL) && (long long )b - (long long )d >= 0LL) && (long
        long )b - (long long )e >= 0LL) && (long long )b - (long long )f >= 0LL) &&
        a == 2) && b == 6)) || ((((((((((((((((((((((((((((-9LL + (long long )b) +
        (long long )c >= 0LL && (-9LL + (long long )b) + (long long )d >= 0LL) &&
        (-9LL + (long long )b) + (long long )e >= 0LL) && (-9LL + (long long )b) +
        (long long )f >= 0LL) && (-7LL + (long long )a) + (long long )c >= 0LL) &&
        (-7LL + (long long )a) + (long long )d >= 0LL) && (-7LL + (long long )a) +
        (long long )e >= 0LL) && (-7LL + (long long )a) + (long long )f >= 0LL) &&
        (-4LL + (long long )a) + (long long )b >= 0LL) && (-3LL - (long long )b) +
        (long long )c >= 0LL) && (-3LL - (long long )b) + (long long )d >= 0LL) &&
        (-3LL - (long long )b) + (long long )e >= 0LL) && (-3LL - (long long )b) +
        (long long )f >= 0LL) && (2LL + (long long )a) - (long long )b >= 0LL) &&
        (3LL + (long long )b) - (long long )c >= 0LL) && (3LL + (long long )b) - (long
        long )d >= 0LL) && (3LL + (long long )b) - (long long )e >= 0LL) && (3LL +
        (long long )b) - (long long )f >= 0LL) && (5LL + (long long )a) - (long long
        )c >= 0LL) && (5LL + (long long )a) - (long long )d >= 0LL) && (5LL + (long
        long )a) - (long long )e >= 0LL) && (5LL + (long long )a) - (long long )f
        >= 0LL) && (9LL - (long long )b) - (long long )c >= 0LL) && (9LL - (long long
        )b) - (long long )d >= 0LL) && (9LL - (long long )b) - (long long )e >= 0LL)
        && (9LL - (long long )b) - (long long )f >= 0LL) && a == 5) && b == 3)) ||
        (((((((((((((((((((((((((((((((((((((((((((((((((((-6LL + (long long )a) +
        (long long )c >= 0LL && (-6LL + (long long )a) + (long long )d >= 0LL) &&
        (-6LL + (long long )a) + (long long )e >= 0LL) && (-6LL + (long long )a) +
        (long long )f >= 0LL) && (-6LL + (long long )b) + (long long )c >= 0LL) &&
        (-6LL + (long long )b) + (long long )d >= 0LL) && (-6LL + (long long )b) +
        (long long )e >= 0LL) && (-6LL + (long long )b) + (long long )f >= 0LL) &&
        (-6LL - (long long )a) + (long long )c >= 0LL) && (-6LL - (long long )a) +
        (long long )d >= 0LL) && (-6LL - (long long )a) + (long long )e >= 0LL) &&
        (-6LL - (long long )a) + (long long )f >= 0LL) && (-6LL - (long long )b) +
        (long long )c >= 0LL) && (-6LL - (long long )b) + (long long )d >= 0LL) &&
        (-6LL - (long long )b) + (long long )e >= 0LL) && (-6LL - (long long )b) +
        (long long )f >= 0LL) && (0LL - (long long )a) + (long long )b >= 0LL) &&
        (long long )a + (long long )b >= 0LL) && (6LL + (long long )a) - (long long
        )c >= 0LL) && (6LL + (long long )a) - (long long )d >= 0LL) && (6LL + (long
        long )a) - (long long )e >= 0LL) && (6LL + (long long )a) - (long long )f
        >= 0LL) && (6LL + (long long )b) - (long long )c >= 0LL) && (6LL + (long long
        )b) - (long long )d >= 0LL) && (6LL + (long long )b) - (long long )e >= 0LL)
        && (6LL + (long long )b) - (long long )f >= 0LL) && (0LL - (long long )a)
        - (long long )b >= 0LL) && (6LL - (long long )a) - (long long )c >= 0LL) &&
        (6LL - (long long )a) - (long long )d >= 0LL) && (6LL - (long long )a) - (long
        long )e >= 0LL) && (6LL - (long long )a) - (long long )f >= 0LL) && (6LL -
        (long long )b) - (long long )c >= 0LL) && (6LL - (long long )b) - (long long
        )d >= 0LL) && (6LL - (long long )b) - (long long )e >= 0LL) && (6LL - (long
        long )b) - (long long )f >= 0LL) && (long long )a - (long long )b >= 0LL)
        && 0 == a) && 0 == b) && 6 == c) && 6 == d) && 6 == e) && 6 == f) && a ==
        0) && a == b) && b == 0) && c == d) && c == e) && c == f) && d == e) && d
        == f) && e == f)) || ((((((((((((((((((((((((((((-11LL + (long long )b) +
        (long long )c >= 0LL && (-11LL + (long long )b) + (long long )d >= 0LL) &&
        (-11LL + (long long )b) + (long long )e >= 0LL) && (-11LL + (long long )b)
        + (long long )f >= 0LL) && (-7LL + (long long )a) + (long long )c >= 0LL)
        && (-7LL + (long long )a) + (long long )d >= 0LL) && (-7LL + (long long )a)
        + (long long )e >= 0LL) && (-7LL + (long long )a) + (long long )f >= 0LL)
        && (-6LL + (long long )a) + (long long )b >= 0LL) && (-1LL - (long long )b)
        + (long long )c >= 0LL) && (-1LL - (long long )b) + (long long )d >= 0LL)
        && (-1LL - (long long )b) + (long long )e >= 0LL) && (-1LL - (long long )b)
        + (long long )f >= 0LL) && (1LL + (long long )b) - (long long )c >= 0LL) &&
        (1LL + (long long )b) - (long long )d >= 0LL) && (1LL + (long long )b) - (long
        long )e >= 0LL) && (1LL + (long long )b) - (long long )f >= 0LL) && (4LL +
        (long long )a) - (long long )b >= 0LL) && (5LL + (long long )a) - (long long
        )c >= 0LL) && (5LL + (long long )a) - (long long )d >= 0LL) && (5LL + (long
        long )a) - (long long )e >= 0LL) && (5LL + (long long )a) - (long long )f
        >= 0LL) && (11LL - (long long )b) - (long long )c >= 0LL) && (11LL - (long
        long )b) - (long long )d >= 0LL) && (11LL - (long long )b) - (long long )e
        >= 0LL) && (11LL - (long long )b) - (long long )f >= 0LL) && a == 2) && b
        == 5)) || ((((((((((((((((((((((((((((-8LL + (long long )b) + (long long )c
        >= 0LL && (-8LL + (long long )b) + (long long )d >= 0LL) && (-8LL + (long
        long )b) + (long long )e >= 0LL) && (-8LL + (long long )b) + (long long )f
        >= 0LL) && (-7LL + (long long )a) + (long long )c >= 0LL) && (-7LL + (long
        long )a) + (long long )d >= 0LL) && (-7LL + (long long )a) + (long long )e
        >= 0LL) && (-7LL + (long long )a) + (long long )f >= 0LL) && (-3LL + (long
        long )a) + (long long )b >= 0LL) && (-4LL - (long long )b) + (long long )c
        >= 0LL) && (-4LL - (long long )b) + (long long )d >= 0LL) && (-4LL - (long
        long )b) + (long long )e >= 0LL) && (-4LL - (long long )b) + (long long )f
        >= 0LL) && (1LL + (long long )a) - (long long )b >= 0LL) && (4LL + (long long
        )b) - (long long )c >= 0LL) && (4LL + (long long )b) - (long long )d >= 0LL)
        && (4LL + (long long )b) - (long long )e >= 0LL) && (4LL + (long long )b)
        - (long long )f >= 0LL) && (5LL + (long long )a) - (long long )c >= 0LL) &&
        (5LL + (long long )a) - (long long )d >= 0LL) && (5LL + (long long )a) - (long
        long )e >= 0LL) && (5LL + (long long )a) - (long long )f >= 0LL) && (8LL -
        (long long )b) - (long long )c >= 0LL) && (8LL - (long long )b) - (long long
        )d >= 0LL) && (8LL - (long long )b) - (long long )e >= 0LL) && (8LL - (long
        long )b) - (long long )f >= 0LL) && a == 5) && b == 2)) || ((((((((((((((((((((((((((((-10LL
        + (long long )b) + (long long )c >= 0LL && (-10LL + (long long )b) + (long
        long )d >= 0LL) && (-10LL + (long long )b) + (long long )e >= 0LL) && (-10LL
        + (long long )b) + (long long )f >= 0LL) && (-7LL + (long long )a) + (long
        long )c >= 0LL) && (-7LL + (long long )a) + (long long )d >= 0LL) && (-7LL
        + (long long )a) + (long long )e >= 0LL) && (-7LL + (long long )a) + (long
        long )f >= 0LL) && (-5LL + (long long )a) + (long long )b >= 0LL) && (-2LL
        - (long long )b) + (long long )c >= 0LL) && (-2LL - (long long )b) + (long
        long )d >= 0LL) && (-2LL - (long long )b) + (long long )e >= 0LL) && (-2LL
        - (long long )b) + (long long )f >= 0LL) && (2LL + (long long )b) - (long
        long )c >= 0LL) && (2LL + (long long )b) - (long long )d >= 0LL) && (2LL +
        (long long )b) - (long long )e >= 0LL) && (2LL + (long long )b) - (long long
        )f >= 0LL) && (3LL + (long long )a) - (long long )b >= 0LL) && (5LL + (long
        long )a) - (long long )c >= 0LL) && (5LL + (long long )a) - (long long )d
        >= 0LL) && (5LL + (long long )a) - (long long )e >= 0LL) && (5LL + (long long
        )a) - (long long )f >= 0LL) && (10LL - (long long )b) - (long long )c >= 0LL)
        && (10LL - (long long )b) - (long long )d >= 0LL) && (10LL - (long long )b)
        - (long long )e >= 0LL) && (10LL - (long long )b) - (long long )f >= 0LL)
        && a == 2) && b == 4)) || ((((((((((((((((((((((((((((-7LL + (long long )a)
        + (long long )c >= 0LL && (-7LL + (long long )a) + (long long )d >= 0LL) &&
        (-7LL + (long long )a) + (long long )e >= 0LL) && (-7LL + (long long )a) +
        (long long )f >= 0LL) && (-7LL + (long long )b) + (long long )c >= 0LL) &&
        (-7LL + (long long )b) + (long long )d >= 0LL) && (-7LL + (long long )b) +
        (long long )e >= 0LL) && (-7LL + (long long )b) + (long long )f >= 0LL) &&
        (-2LL + (long long )a) + (long long )b >= 0LL) && (-5LL - (long long )b) +
        (long long )c >= 0LL) && (-5LL - (long long )b) + (long long )d >= 0LL) &&
        (-5LL - (long long )b) + (long long )e >= 0LL) && (-5LL - (long long )b) +
        (long long )f >= 0LL) && (5LL + (long long )a) - (long long )c >= 0LL) &&
        (5LL + (long long )a) - (long long )d >= 0LL) && (5LL + (long long )a) - (long
        long )e >= 0LL) && (5LL + (long long )a) - (long long )f >= 0LL) && (5LL +
        (long long )b) - (long long )c >= 0LL) && (5LL + (long long )b) - (long long
        )d >= 0LL) && (5LL + (long long )b) - (long long )e >= 0LL) && (5LL + (long
        long )b) - (long long )f >= 0LL) && (7LL - (long long )b) - (long long )c
        >= 0LL) && (7LL - (long long )b) - (long long )d >= 0LL) && (7LL - (long long
        )b) - (long long )e >= 0LL) && (7LL - (long long )b) - (long long )f >= 0LL)
        && (long long )a - (long long )b >= 0LL) && a == 5) && b == 1)) || ((((((((((((((((((((((((((((-9LL
        + (long long )b) + (long long )c >= 0LL && (-9LL + (long long )b) + (long
        long )d >= 0LL) && (-9LL + (long long )b) + (long long )e >= 0LL) && (-9LL
        + (long long )b) + (long long )f >= 0LL) && (-7LL + (long long )a) + (long
        long )c >= 0LL) && (-7LL + (long long )a) + (long long )d >= 0LL) && (-7LL
        + (long long )a) + (long long )e >= 0LL) && (-7LL + (long long )a) + (long
        long )f >= 0LL) && (-4LL + (long long )a) + (long long )b >= 0LL) && (-3LL
        - (long long )b) + (long long )c >= 0LL) && (-3LL - (long long )b) + (long
        long )d >= 0LL) && (-3LL - (long long )b) + (long long )e >= 0LL) && (-3LL
        - (long long )b) + (long long )f >= 0LL) && (2LL + (long long )a) - (long
        long )b >= 0LL) && (3LL + (long long )b) - (long long )c >= 0LL) && (3LL +
        (long long )b) - (long long )d >= 0LL) && (3LL + (long long )b) - (long long
        )e >= 0LL) && (3LL + (long long )b) - (long long )f >= 0LL) && (5LL + (long
        long )a) - (long long )c >= 0LL) && (5LL + (long long )a) - (long long )d
        >= 0LL) && (5LL + (long long )a) - (long long )e >= 0LL) && (5LL + (long long
        )a) - (long long )f >= 0LL) && (9LL - (long long )b) - (long long )c >= 0LL)
        && (9LL - (long long )b) - (long long )d >= 0LL) && (9LL - (long long )b)
        - (long long )e >= 0LL) && (9LL - (long long )b) - (long long )f >= 0LL) &&
        a == 2) && b == 3)) || (((((((((((((((((((((((((((((((((((((((-11LL + (long
        long )a) + (long long )c >= 0LL && (-11LL + (long long )a) + (long long )d
        >= 0LL) && (-11LL + (long long )a) + (long long )e >= 0LL) && (-11LL + (long
        long )a) + (long long )f >= 0LL) && (-6LL + (long long )b) + (long long )c
        >= 0LL) && (-6LL + (long long )b) + (long long )d >= 0LL) && (-6LL + (long
        long )b) + (long long )e >= 0LL) && (-6LL + (long long )b) + (long long )f
        >= 0LL) && (-5LL + (long long )a) + (long long )b >= 0LL) && (-6LL - (long
        long )b) + (long long )c >= 0LL) && (-6LL - (long long )b) + (long long )d
        >= 0LL) && (-6LL - (long long )b) + (long long )e >= 0LL) && (-6LL - (long
        long )b) + (long long )f >= 0LL) && (-1LL - (long long )a) + (long long )c
        >= 0LL) && (-1LL - (long long )a) + (long long )d >= 0LL) && (-1LL - (long
        long )a) + (long long )e >= 0LL) && (-1LL - (long long )a) + (long long )f
        >= 0LL) && (5LL - (long long )a) + (long long )b >= 0LL) && (-5LL + (long
        long )a) - (long long )b >= 0LL) && (1LL + (long long )a) - (long long )c
        >= 0LL) && (1LL + (long long )a) - (long long )d >= 0LL) && (1LL + (long long
        )a) - (long long )e >= 0LL) && (1LL + (long long )a) - (long long )f >= 0LL)
        && (6LL + (long long )b) - (long long )c >= 0LL) && (6LL + (long long )b)
        - (long long )d >= 0LL) && (6LL + (long long )b) - (long long )e >= 0LL) &&
        (6LL + (long long )b) - (long long )f >= 0LL) && (5LL - (long long )a) - (long
        long )b >= 0LL) && (6LL - (long long )b) - (long long )c >= 0LL) && (6LL -
        (long long )b) - (long long )d >= 0LL) && (6LL - (long long )b) - (long long
        )e >= 0LL) && (6LL - (long long )b) - (long long )f >= 0LL) && (11LL - (long
        long )a) - (long long )c >= 0LL) && (11LL - (long long )a) - (long long )d
        >= 0LL) && (11LL - (long long )a) - (long long )e >= 0LL) && (11LL - (long
        long )a) - (long long )f >= 0LL) && 0 == b) && a == 5) && b == 0)) || ((((((((((((((((((((((((((((-8LL
        + (long long )b) + (long long )c >= 0LL && (-8LL + (long long )b) + (long
        long )d >= 0LL) && (-8LL + (long long )b) + (long long )e >= 0LL) && (-8LL
        + (long long )b) + (long long )f >= 0LL) && (-7LL + (long long )a) + (long
        long )c >= 0LL) && (-7LL + (long long )a) + (long long )d >= 0LL) && (-7LL
        + (long long )a) + (long long )e >= 0LL) && (-7LL + (long long )a) + (long
        long )f >= 0LL) && (-3LL + (long long )a) + (long long )b >= 0LL) && (-4LL
        - (long long )b) + (long long )c >= 0LL) && (-4LL - (long long )b) + (long
        long )d >= 0LL) && (-4LL - (long long )b) + (long long )e >= 0LL) && (-4LL
        - (long long )b) + (long long )f >= 0LL) && (1LL + (long long )a) - (long
        long )b >= 0LL) && (4LL + (long long )b) - (long long )c >= 0LL) && (4LL +
        (long long )b) - (long long )d >= 0LL) && (4LL + (long long )b) - (long long
        )e >= 0LL) && (4LL + (long long )b) - (long long )f >= 0LL) && (5LL + (long
        long )a) - (long long )c >= 0LL) && (5LL + (long long )a) - (long long )d
        >= 0LL) && (5LL + (long long )a) - (long long )e >= 0LL) && (5LL + (long long
        )a) - (long long )f >= 0LL) && (8LL - (long long )b) - (long long )c >= 0LL)
        && (8LL - (long long )b) - (long long )d >= 0LL) && (8LL - (long long )b)
        - (long long )e >= 0LL) && (8LL - (long long )b) - (long long )f >= 0LL) &&
        a == 2) && b == 2)) || ((((((((((((((((((((((((((((-7LL + (long long )a) +
        (long long )c >= 0LL && (-7LL + (long long )a) + (long long )d >= 0LL) &&
        (-7LL + (long long )a) + (long long )e >= 0LL) && (-7LL + (long long )a) +
        (long long )f >= 0LL) && (-7LL + (long long )b) + (long long )c >= 0LL) &&
        (-7LL + (long long )b) + (long long )d >= 0LL) && (-7LL + (long long )b) +
        (long long )e >= 0LL) && (-7LL + (long long )b) + (long long )f >= 0LL) &&
        (-2LL + (long long )a) + (long long )b >= 0LL) && (-5LL - (long long )b) +
        (long long )c >= 0LL) && (-5LL - (long long )b) + (long long )d >= 0LL) &&
        (-5LL - (long long )b) + (long long )e >= 0LL) && (-5LL - (long long )b) +
        (long long )f >= 0LL) && (5LL + (long long )a) - (long long )c >= 0LL) &&
        (5LL + (long long )a) - (long long )d >= 0LL) && (5LL + (long long )a) - (long
        long )e >= 0LL) && (5LL + (long long )a) - (long long )f >= 0LL) && (5LL +
        (long long )b) - (long long )c >= 0LL) && (5LL + (long long )b) - (long long
        )d >= 0LL) && (5LL + (long long )b) - (long long )e >= 0LL) && (5LL + (long
        long )b) - (long long )f >= 0LL) && (7LL - (long long )b) - (long long )c
        >= 0LL) && (7LL - (long long )b) - (long long )d >= 0LL) && (7LL - (long long
        )b) - (long long )e >= 0LL) && (7LL - (long long )b) - (long long )f >= 0LL)
        && (long long )a - (long long )b >= 0LL) && a == 2) && b == 1)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (-12LL + (long long )b) + (long long )c >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (-12LL + (long long )b) + (long long )d >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (-12LL + (long long )b) + (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (-12LL + (long long )b) + (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (-12LL + (long long )c) + (long long )d >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (-12LL + (long long )c) + (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (-12LL + (long long )c) + (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (-12LL + (long long )d) + (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (-12LL + (long long )d) + (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (-12LL + (long long )e) + (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (0LL - (long long )b) + (long long )c >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (0LL - (long long )b) + (long long )d >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (0LL - (long long )b) + (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (0LL - (long long )b) + (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (0LL - (long long )c) + (long long )d >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (0LL - (long long )c) + (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (0LL - (long long )c) + (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (0LL - (long long )d) + (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (0LL - (long long )d) + (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (0LL - (long long )e) + (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (12LL - (long long )b) - (long long )c >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (12LL - (long long )b) - (long long )d >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (12LL - (long long )b) - (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (12LL - (long long )b) - (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (12LL - (long long )c) - (long long )d >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (12LL - (long long )c) - (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (12LL - (long long )c) - (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (12LL - (long long )d) - (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (12LL - (long long )d) - (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (12LL - (long long )e) - (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (long long )b - (long long )c >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (long long )b - (long long )d >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (long long )b - (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (long long )b - (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (long long )c - (long long )d >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (long long )c - (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (long long )c - (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (long long )d - (long long )e >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (long long )d - (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: (long long )e - (long long )f >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: b == 6
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: c == 6
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: d == 6
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: e == 6
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: f == 6
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/recursified_loop-simple/recursified_nested_6.c
        line: 109
        column: 5
        function: main
      value: ((((((((((((((((((((((((((-8LL + (long long )a) + (long long )b >= 0LL
        && (-8LL + (long long )a) + (long long )c >= 0LL) && (-8LL + (long long )a)
        + (long long )d >= 0LL) && (-8LL + (long long )a) + (long long )e >= 0LL)
        && (-8LL + (long long )a) + (long long )f >= 0LL) && (-4LL - (long long )a)
        + (long long )b >= 0LL) && (-4LL - (long long )a) + (long long )c >= 0LL)
        && (-4LL - (long long )a) + (long long )d >= 0LL) && (-4LL - (long long )a)
        + (long long )e >= 0LL) && (-4LL - (long long )a) + (long long )f >= 0LL)
        && (4LL + (long long )a) - (long long )b >= 0LL) && (4LL + (long long )a)
        - (long long )c >= 0LL) && (4LL + (long long )a) - (long long )d >= 0LL) &&
        (4LL + (long long )a) - (long long )e >= 0LL) && (4LL + (long long )a) - (long
        long )f >= 0LL) && (8LL - (long long )a) - (long long )b >= 0LL) && (8LL -
        (long long )a) - (long long )c >= 0LL) && (8LL - (long long )a) - (long long
        )d >= 0LL) && (8LL - (long long )a) - (long long )e >= 0LL) && (8LL - (long
        long )a) - (long long )f >= 0LL) && a == 2) || (((((((((((((((((((((-10LL
        + (long long )a) + (long long )b >= 0LL && (-10LL + (long long )a) + (long
        long )c >= 0LL) && (-10LL + (long long )a) + (long long )d >= 0LL) && (-10LL
        + (long long )a) + (long long )e >= 0LL) && (-10LL + (long long )a) + (long
        long )f >= 0LL) && (-2LL - (long long )a) + (long long )b >= 0LL) && (-2LL
        - (long long )a) + (long long )c >= 0LL) && (-2LL - (long long )a) + (long
        long )d >= 0LL) && (-2LL - (long long )a) + (long long )e >= 0LL) && (-2LL
        - (long long )a) + (long long )f >= 0LL) && (2LL + (long long )a) - (long
        long )b >= 0LL) && (2LL + (long long )a) - (long long )c >= 0LL) && (2LL +
        (long long )a) - (long long )d >= 0LL) && (2LL + (long long )a) - (long long
        )e >= 0LL) && (2LL + (long long )a) - (long long )f >= 0LL) && (10LL - (long
        long )a) - (long long )b >= 0LL) && (10LL - (long long )a) - (long long )c
        >= 0LL) && (10LL - (long long )a) - (long long )d >= 0LL) && (10LL - (long
        long )a) - (long long )e >= 0LL) && (10LL - (long long )a) - (long long )f
        >= 0LL) && a == 4)) || (((((((((((((((((((((-7LL + (long long )a) + (long
        long )b >= 0LL && (-7LL + (long long )a) + (long long )c >= 0LL) && (-7LL
        + (long long )a) + (long long )d >= 0LL) && (-7LL + (long long )a) + (long
        long )e >= 0LL) && (-7LL + (long long )a) + (long long )f >= 0LL) && (-5LL
        - (long long )a) + (long long )b >= 0LL) && (-5LL - (long long )a) + (long
        long )c >= 0LL) && (-5LL - (long long )a) + (long long )d >= 0LL) && (-5LL
        - (long long )a) + (long long )e >= 0LL) && (-5LL - (long long )a) + (long
        long )f >= 0LL) && (5LL + (long long )a) - (long long )b >= 0LL) && (5LL +
        (long long )a) - (long long )c >= 0LL) && (5LL + (long long )a) - (long long
        )d >= 0LL) && (5LL + (long long )a) - (long long )e >= 0LL) && (5LL + (long
        long )a) - (long long )f >= 0LL) && (7LL - (long long )a) - (long long )b
        >= 0LL) && (7LL - (long long )a) - (long long )c >= 0LL) && (7LL - (long long
        )a) - (long long )d >= 0LL) && (7LL - (long long )a) - (long long )e >= 0LL)
        && (7LL - (long long )a) - (long long )f >= 0LL) && a == 1)) || (((((((((((((((((((((-12LL
        + (long long )a) + (long long )b >= 0LL && (-12LL + (long long )a) + (long
        long )c >= 0LL) && (-12LL + (long long )a) + (long long )d >= 0LL) && (-12LL
        + (long long )a) + (long long )e >= 0LL) && (-12LL + (long long )a) + (long
        long )f >= 0LL) && (0LL - (long long )a) + (long long )b >= 0LL) && (0LL -
        (long long )a) + (long long )c >= 0LL) && (0LL - (long long )a) + (long long
        )d >= 0LL) && (0LL - (long long )a) + (long long )e >= 0LL) && (0LL - (long
        long )a) + (long long )f >= 0LL) && (12LL - (long long )a) - (long long )b
        >= 0LL) && (12LL - (long long )a) - (long long )c >= 0LL) && (12LL - (long
        long )a) - (long long )d >= 0LL) && (12LL - (long long )a) - (long long )e
        >= 0LL) && (12LL - (long long )a) - (long long )f >= 0LL) && (long long )a
        - (long long )b >= 0LL) && (long long )a - (long long )c >= 0LL) && (long
        long )a - (long long )d >= 0LL) && (long long )a - (long long )e >= 0LL) &&
        (long long )a - (long long )f >= 0LL) && a == 6)) || (((((((((((((((((((((-9LL
        + (long long )a) + (long long )b >= 0LL && (-9LL + (long long )a) + (long
        long )c >= 0LL) && (-9LL + (long long )a) + (long long )d >= 0LL) && (-9LL
        + (long long )a) + (long long )e >= 0LL) && (-9LL + (long long )a) + (long
        long )f >= 0LL) && (-3LL - (long long )a) + (long long )b >= 0LL) && (-3LL
        - (long long )a) + (long long )c >= 0LL) && (-3LL - (long long )a) + (long
        long )d >= 0LL) && (-3LL - (long long )a) + (long long )e >= 0LL) && (-3LL
        - (long long )a) + (long long )f >= 0LL) && (3LL + (long long )a) - (long
        long )b >= 0LL) && (3LL + (long long )a) - (long long )c >= 0LL) && (3LL +
        (long long )a) - (long long )d >= 0LL) && (3LL + (long long )a) - (long long
        )e >= 0LL) && (3LL + (long long )a) - (long long )f >= 0LL) && (9LL - (long
        long )a) - (long long )b >= 0LL) && (9LL - (long long )a) - (long long )c
        >= 0LL) && (9LL - (long long )a) - (long long )d >= 0LL) && (9LL - (long long
        )a) - (long long )e >= 0LL) && (9LL - (long long )a) - (long long )f >= 0LL)
        && a == 3)) || (((((((((((((((((((((((((((((((((((((-6LL + (long long )a)
        + (long long )b >= 0LL && (-6LL + (long long )a) + (long long )c >= 0LL) &&
        (-6LL + (long long )a) + (long long )d >= 0LL) && (-6LL + (long long )a) +
        (long long )e >= 0LL) && (-6LL + (long long )a) + (long long )f >= 0LL) &&
        (-6LL - (long long )a) + (long long )b >= 0LL) && (-6LL - (long long )a) +
        (long long )c >= 0LL) && (-6LL - (long long )a) + (long long )d >= 0LL) &&
        (-6LL - (long long )a) + (long long )e >= 0LL) && (-6LL - (long long )a) +
        (long long )f >= 0LL) && (6LL + (long long )a) - (long long )b >= 0LL) &&
        (6LL + (long long )a) - (long long )c >= 0LL) && (6LL + (long long )a) - (long
        long )d >= 0LL) && (6LL + (long long )a) - (long long )e >= 0LL) && (6LL +
        (long long )a) - (long long )f >= 0LL) && (6LL - (long long )a) - (long long
        )b >= 0LL) && (6LL - (long long )a) - (long long )c >= 0LL) && (6LL - (long
        long )a) - (long long )d >= 0LL) && (6LL - (long long )a) - (long long )e
        >= 0LL) && (6LL - (long long )a) - (long long )f >= 0LL) && 0 == a) && 6 ==
        b) && 6 == c) && 6 == d) && 6 == e) && 6 == f) && a == 0) && b == c) && b
        == d) && b == e) && b == f) && c == d) && c == e) && c == f) && d == e) &&
        d == f) && e == f)) || (((((((((((((((((((((-11LL + (long long )a) + (long
        long )b >= 0LL && (-11LL + (long long )a) + (long long )c >= 0LL) && (-11LL
        + (long long )a) + (long long )d >= 0LL) && (-11LL + (long long )a) + (long
        long )e >= 0LL) && (-11LL + (long long )a) + (long long )f >= 0LL) && (-1LL
        - (long long )a) + (long long )b >= 0LL) && (-1LL - (long long )a) + (long
        long )c >= 0LL) && (-1LL - (long long )a) + (long long )d >= 0LL) && (-1LL
        - (long long )a) + (long long )e >= 0LL) && (-1LL - (long long )a) + (long
        long )f >= 0LL) && (1LL + (long long )a) - (long long )b >= 0LL) && (1LL +
        (long long )a) - (long long )c >= 0LL) && (1LL + (long long )a) - (long long
        )d >= 0LL) && (1LL + (long long )a) - (long long )e >= 0LL) && (1LL + (long
        long )a) - (long long )f >= 0LL) && (11LL - (long long )a) - (long long )b
        >= 0LL) && (11LL - (long long )a) - (long long )c >= 0LL) && (11LL - (long
        long )a) - (long long )d >= 0LL) && (11LL - (long long )a) - (long long )e
        >= 0LL) && (11LL - (long long )a) - (long long )f >= 0LL) && a == 5)
      format: c_expression
