- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 88911c20-cde4-4096-bc65-5bed54fbf16e
    creation_time: 2025-03-22T17:11:23Z
    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/locks/test_locks_8.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c: b7157ba450d9d62b74d19027a6860eb7210e35a76921ceb23a9c0a69add85337
      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/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p1) + (long long )p2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p1) + (long long )p3 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p1) + (long long )p4 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p1) + (long long )p5 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p1) + (long long )p6 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p1) + (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p1) + (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p2) + (long long )p3 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p2) + (long long )p4 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p2) + (long long )p5 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p2) + (long long )p6 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p2) + (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p2) + (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p3) + (long long )p4 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p3) + (long long )p5 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p3) + (long long )p6 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p3) + (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p3) + (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p4) + (long long )p5 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p4) + (long long )p6 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p4) + (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p4) + (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p5) + (long long )p6 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p5) + (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p5) + (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p6) + (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p6) + (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967296LL + (long long )p7) + (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p1) + (long long )p2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p1) + (long long )p3 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p1) + (long long )p4 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p1) + (long long )p5 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p1) + (long long )p6 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p1) + (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p1) + (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p2) + (long long )p3 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p2) + (long long )p4 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p2) + (long long )p5 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p2) + (long long )p6 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p2) + (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p2) + (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p3) + (long long )p4 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p3) + (long long )p5 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p3) + (long long )p6 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p3) + (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p3) + (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p4) + (long long )p5 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p4) + (long long )p6 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p4) + (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p4) + (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p5) + (long long )p6 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p5) + (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p5) + (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p6) + (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p6) + (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL - (long long )p7) + (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p1) - (long long )p2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p1) - (long long )p3 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p1) - (long long )p4 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p1) - (long long )p5 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p1) - (long long )p6 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p1) - (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p1) - (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p2) - (long long )p3 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p2) - (long long )p4 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p2) - (long long )p5 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p2) - (long long )p6 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p2) - (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p2) - (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p3) - (long long )p4 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p3) - (long long )p5 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p3) - (long long )p6 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p3) - (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p3) - (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p4) - (long long )p5 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p4) - (long long )p6 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p4) - (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p4) - (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p5) - (long long )p6 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p5) - (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p5) - (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p6) - (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p6) - (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967295LL + (long long )p7) - (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p1) - (long long )p2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p1) - (long long )p3 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p1) - (long long )p4 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p1) - (long long )p5 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p1) - (long long )p6 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p1) - (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p1) - (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p2) - (long long )p3 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p2) - (long long )p4 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p2) - (long long )p5 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p2) - (long long )p6 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p2) - (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p2) - (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p3) - (long long )p4 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p3) - (long long )p5 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p3) - (long long )p6 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p3) - (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p3) - (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p4) - (long long )p5 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p4) - (long long )p6 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p4) - (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p4) - (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p5) - (long long )p6 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p5) - (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p5) - (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p6) - (long long )p7 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p6) - (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (4294967294LL - (long long )p7) - (long long )p8 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/locks/test_locks_8.c
        line: 35
        column: 5
        function: main
      value: (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((2147483648LL
        + (long long )lk1) + (long long )p1 >= 0LL && (2147483648LL + (long long )lk1)
        + (long long )p2 >= 0LL) && (2147483648LL + (long long )lk1) + (long long
        )p3 >= 0LL) && (2147483648LL + (long long )lk1) + (long long )p4 >= 0LL) &&
        (2147483648LL + (long long )lk1) + (long long )p5 >= 0LL) && (2147483648LL
        + (long long )lk1) + (long long )p6 >= 0LL) && (2147483648LL + (long long
        )lk1) + (long long )p7 >= 0LL) && (2147483648LL + (long long )lk1) + (long
        long )p8 >= 0LL) && (2147483648LL + (long long )lk2) + (long long )p1 >= 0LL)
        && (2147483648LL + (long long )lk2) + (long long )p2 >= 0LL) && (2147483648LL
        + (long long )lk2) + (long long )p3 >= 0LL) && (2147483648LL + (long long
        )lk2) + (long long )p4 >= 0LL) && (2147483648LL + (long long )lk2) + (long
        long )p5 >= 0LL) && (2147483648LL + (long long )lk2) + (long long )p6 >= 0LL)
        && (2147483648LL + (long long )lk2) + (long long )p7 >= 0LL) && (2147483648LL
        + (long long )lk2) + (long long )p8 >= 0LL) && (2147483648LL + (long long
        )lk3) + (long long )p1 >= 0LL) && (2147483648LL + (long long )lk3) + (long
        long )p2 >= 0LL) && (2147483648LL + (long long )lk3) + (long long )p3 >= 0LL)
        && (2147483648LL + (long long )lk3) + (long long )p4 >= 0LL) && (2147483648LL
        + (long long )lk3) + (long long )p5 >= 0LL) && (2147483648LL + (long long
        )lk3) + (long long )p6 >= 0LL) && (2147483648LL + (long long )lk3) + (long
        long )p7 >= 0LL) && (2147483648LL + (long long )lk3) + (long long )p8 >= 0LL)
        && (2147483648LL + (long long )lk4) + (long long )p1 >= 0LL) && (2147483648LL
        + (long long )lk4) + (long long )p2 >= 0LL) && (2147483648LL + (long long
        )lk4) + (long long )p3 >= 0LL) && (2147483648LL + (long long )lk4) + (long
        long )p4 >= 0LL) && (2147483648LL + (long long )lk4) + (long long )p5 >= 0LL)
        && (2147483648LL + (long long )lk4) + (long long )p6 >= 0LL) && (2147483648LL
        + (long long )lk4) + (long long )p7 >= 0LL) && (2147483648LL + (long long
        )lk4) + (long long )p8 >= 0LL) && (2147483648LL + (long long )lk5) + (long
        long )p1 >= 0LL) && (2147483648LL + (long long )lk5) + (long long )p2 >= 0LL)
        && (2147483648LL + (long long )lk5) + (long long )p3 >= 0LL) && (2147483648LL
        + (long long )lk5) + (long long )p4 >= 0LL) && (2147483648LL + (long long
        )lk5) + (long long )p5 >= 0LL) && (2147483648LL + (long long )lk5) + (long
        long )p6 >= 0LL) && (2147483648LL + (long long )lk5) + (long long )p7 >= 0LL)
        && (2147483648LL + (long long )lk5) + (long long )p8 >= 0LL) && (2147483648LL
        + (long long )lk6) + (long long )p1 >= 0LL) && (2147483648LL + (long long
        )lk6) + (long long )p2 >= 0LL) && (2147483648LL + (long long )lk6) + (long
        long )p3 >= 0LL) && (2147483648LL + (long long )lk6) + (long long )p4 >= 0LL)
        && (2147483648LL + (long long )lk6) + (long long )p5 >= 0LL) && (2147483648LL
        + (long long )lk6) + (long long )p6 >= 0LL) && (2147483648LL + (long long
        )lk6) + (long long )p7 >= 0LL) && (2147483648LL + (long long )lk6) + (long
        long )p8 >= 0LL) && (2147483648LL + (long long )lk7) + (long long )p1 >= 0LL)
        && (2147483648LL + (long long )lk7) + (long long )p2 >= 0LL) && (2147483648LL
        + (long long )lk7) + (long long )p3 >= 0LL) && (2147483648LL + (long long
        )lk7) + (long long )p4 >= 0LL) && (2147483648LL + (long long )lk7) + (long
        long )p5 >= 0LL) && (2147483648LL + (long long )lk7) + (long long )p6 >= 0LL)
        && (2147483648LL + (long long )lk7) + (long long )p7 >= 0LL) && (2147483648LL
        + (long long )lk7) + (long long )p8 >= 0LL) && (2147483648LL + (long long
        )lk8) + (long long )p1 >= 0LL) && (2147483648LL + (long long )lk8) + (long
        long )p2 >= 0LL) && (2147483648LL + (long long )lk8) + (long long )p3 >= 0LL)
        && (2147483648LL + (long long )lk8) + (long long )p4 >= 0LL) && (2147483648LL
        + (long long )lk8) + (long long )p5 >= 0LL) && (2147483648LL + (long long
        )lk8) + (long long )p6 >= 0LL) && (2147483648LL + (long long )lk8) + (long
        long )p7 >= 0LL) && (2147483648LL + (long long )lk8) + (long long )p8 >= 0LL)
        && (1LL - (long long )lk1) + (long long )lk2 >= 0LL) && (1LL - (long long
        )lk1) + (long long )lk3 >= 0LL) && (1LL - (long long )lk1) + (long long )lk4
        >= 0LL) && (1LL - (long long )lk1) + (long long )lk5 >= 0LL) && (1LL - (long
        long )lk1) + (long long )lk6 >= 0LL) && (1LL - (long long )lk1) + (long long
        )lk7 >= 0LL) && (1LL - (long long )lk1) + (long long )lk8 >= 0LL) && (1LL
        - (long long )lk2) + (long long )lk3 >= 0LL) && (1LL - (long long )lk2) +
        (long long )lk4 >= 0LL) && (1LL - (long long )lk2) + (long long )lk5 >= 0LL)
        && (1LL - (long long )lk2) + (long long )lk6 >= 0LL) && (1LL - (long long
        )lk2) + (long long )lk7 >= 0LL) && (1LL - (long long )lk2) + (long long )lk8
        >= 0LL) && (1LL - (long long )lk3) + (long long )lk4 >= 0LL) && (1LL - (long
        long )lk3) + (long long )lk5 >= 0LL) && (1LL - (long long )lk3) + (long long
        )lk6 >= 0LL) && (1LL - (long long )lk3) + (long long )lk7 >= 0LL) && (1LL
        - (long long )lk3) + (long long )lk8 >= 0LL) && (1LL - (long long )lk4) +
        (long long )lk5 >= 0LL) && (1LL - (long long )lk4) + (long long )lk6 >= 0LL)
        && (1LL - (long long )lk4) + (long long )lk7 >= 0LL) && (1LL - (long long
        )lk4) + (long long )lk8 >= 0LL) && (1LL - (long long )lk5) + (long long )lk6
        >= 0LL) && (1LL - (long long )lk5) + (long long )lk7 >= 0LL) && (1LL - (long
        long )lk5) + (long long )lk8 >= 0LL) && (1LL - (long long )lk6) + (long long
        )lk7 >= 0LL) && (1LL - (long long )lk6) + (long long )lk8 >= 0LL) && (1LL
        - (long long )lk7) + (long long )lk8 >= 0LL) && (2147483648LL - (long long
        )lk1) + (long long )p1 >= 0LL) && (2147483648LL - (long long )lk2) + (long
        long )p2 >= 0LL) && (2147483648LL - (long long )lk3) + (long long )p3 >= 0LL)
        && (2147483648LL - (long long )lk4) + (long long )p4 >= 0LL) && (2147483648LL
        - (long long )lk5) + (long long )p5 >= 0LL) && (2147483648LL - (long long
        )lk6) + (long long )p6 >= 0LL) && (2147483648LL - (long long )lk7) + (long
        long )p7 >= 0LL) && (2147483648LL - (long long )lk8) + (long long )p8 >= 0LL)
        && (2147483649LL - (long long )lk1) + (long long )p2 >= 0LL) && (2147483649LL
        - (long long )lk1) + (long long )p3 >= 0LL) && (2147483649LL - (long long
        )lk1) + (long long )p4 >= 0LL) && (2147483649LL - (long long )lk1) + (long
        long )p5 >= 0LL) && (2147483649LL - (long long )lk1) + (long long )p6 >= 0LL)
        && (2147483649LL - (long long )lk1) + (long long )p7 >= 0LL) && (2147483649LL
        - (long long )lk1) + (long long )p8 >= 0LL) && (2147483649LL - (long long
        )lk2) + (long long )p1 >= 0LL) && (2147483649LL - (long long )lk2) + (long
        long )p3 >= 0LL) && (2147483649LL - (long long )lk2) + (long long )p4 >= 0LL)
        && (2147483649LL - (long long )lk2) + (long long )p5 >= 0LL) && (2147483649LL
        - (long long )lk2) + (long long )p6 >= 0LL) && (2147483649LL - (long long
        )lk2) + (long long )p7 >= 0LL) && (2147483649LL - (long long )lk2) + (long
        long )p8 >= 0LL) && (2147483649LL - (long long )lk3) + (long long )p1 >= 0LL)
        && (2147483649LL - (long long )lk3) + (long long )p2 >= 0LL) && (2147483649LL
        - (long long )lk3) + (long long )p4 >= 0LL) && (2147483649LL - (long long
        )lk3) + (long long )p5 >= 0LL) && (2147483649LL - (long long )lk3) + (long
        long )p6 >= 0LL) && (2147483649LL - (long long )lk3) + (long long )p7 >= 0LL)
        && (2147483649LL - (long long )lk3) + (long long )p8 >= 0LL) && (2147483649LL
        - (long long )lk4) + (long long )p1 >= 0LL) && (2147483649LL - (long long
        )lk4) + (long long )p2 >= 0LL) && (2147483649LL - (long long )lk4) + (long
        long )p3 >= 0LL) && (2147483649LL - (long long )lk4) + (long long )p5 >= 0LL)
        && (2147483649LL - (long long )lk4) + (long long )p6 >= 0LL) && (2147483649LL
        - (long long )lk4) + (long long )p7 >= 0LL) && (2147483649LL - (long long
        )lk4) + (long long )p8 >= 0LL) && (2147483649LL - (long long )lk5) + (long
        long )p1 >= 0LL) && (2147483649LL - (long long )lk5) + (long long )p2 >= 0LL)
        && (2147483649LL - (long long )lk5) + (long long )p3 >= 0LL) && (2147483649LL
        - (long long )lk5) + (long long )p4 >= 0LL) && (2147483649LL - (long long
        )lk5) + (long long )p6 >= 0LL) && (2147483649LL - (long long )lk5) + (long
        long )p7 >= 0LL) && (2147483649LL - (long long )lk5) + (long long )p8 >= 0LL)
        && (2147483649LL - (long long )lk6) + (long long )p1 >= 0LL) && (2147483649LL
        - (long long )lk6) + (long long )p2 >= 0LL) && (2147483649LL - (long long
        )lk6) + (long long )p3 >= 0LL) && (2147483649LL - (long long )lk6) + (long
        long )p4 >= 0LL) && (2147483649LL - (long long )lk6) + (long long )p5 >= 0LL)
        && (2147483649LL - (long long )lk6) + (long long )p7 >= 0LL) && (2147483649LL
        - (long long )lk6) + (long long )p8 >= 0LL) && (2147483649LL - (long long
        )lk7) + (long long )p1 >= 0LL) && (2147483649LL - (long long )lk7) + (long
        long )p2 >= 0LL) && (2147483649LL - (long long )lk7) + (long long )p3 >= 0LL)
        && (2147483649LL - (long long )lk7) + (long long )p4 >= 0LL) && (2147483649LL
        - (long long )lk7) + (long long )p5 >= 0LL) && (2147483649LL - (long long
        )lk7) + (long long )p6 >= 0LL) && (2147483649LL - (long long )lk7) + (long
        long )p8 >= 0LL) && (2147483649LL - (long long )lk8) + (long long )p1 >= 0LL)
        && (2147483649LL - (long long )lk8) + (long long )p2 >= 0LL) && (2147483649LL
        - (long long )lk8) + (long long )p3 >= 0LL) && (2147483649LL - (long long
        )lk8) + (long long )p4 >= 0LL) && (2147483649LL - (long long )lk8) + (long
        long )p5 >= 0LL) && (2147483649LL - (long long )lk8) + (long long )p6 >= 0LL)
        && (2147483649LL - (long long )lk8) + (long long )p7 >= 0LL) && (long long
        )lk1 + (long long )lk2 >= 0LL) && (long long )lk1 + (long long )lk3 >= 0LL)
        && (long long )lk1 + (long long )lk4 >= 0LL) && (long long )lk1 + (long long
        )lk5 >= 0LL) && (long long )lk1 + (long long )lk6 >= 0LL) && (long long )lk1
        + (long long )lk7 >= 0LL) && (long long )lk1 + (long long )lk8 >= 0LL) &&
        (long long )lk2 + (long long )lk3 >= 0LL) && (long long )lk2 + (long long
        )lk4 >= 0LL) && (long long )lk2 + (long long )lk5 >= 0LL) && (long long )lk2
        + (long long )lk6 >= 0LL) && (long long )lk2 + (long long )lk7 >= 0LL) &&
        (long long )lk2 + (long long )lk8 >= 0LL) && (long long )lk3 + (long long
        )lk4 >= 0LL) && (long long )lk3 + (long long )lk5 >= 0LL) && (long long )lk3
        + (long long )lk6 >= 0LL) && (long long )lk3 + (long long )lk7 >= 0LL) &&
        (long long )lk3 + (long long )lk8 >= 0LL) && (long long )lk4 + (long long
        )lk5 >= 0LL) && (long long )lk4 + (long long )lk6 >= 0LL) && (long long )lk4
        + (long long )lk7 >= 0LL) && (long long )lk4 + (long long )lk8 >= 0LL) &&
        (long long )lk5 + (long long )lk6 >= 0LL) && (long long )lk5 + (long long
        )lk7 >= 0LL) && (long long )lk5 + (long long )lk8 >= 0LL) && (long long )lk6
        + (long long )lk7 >= 0LL) && (long long )lk6 + (long long )lk8 >= 0LL) &&
        (long long )lk7 + (long long )lk8 >= 0LL) && (1LL + (long long )lk1) - (long
        long )lk2 >= 0LL) && (1LL + (long long )lk1) - (long long )lk3 >= 0LL) &&
        (1LL + (long long )lk1) - (long long )lk4 >= 0LL) && (1LL + (long long )lk1)
        - (long long )lk5 >= 0LL) && (1LL + (long long )lk1) - (long long )lk6 >=
        0LL) && (1LL + (long long )lk1) - (long long )lk7 >= 0LL) && (1LL + (long
        long )lk1) - (long long )lk8 >= 0LL) && (1LL + (long long )lk2) - (long long
        )lk3 >= 0LL) && (1LL + (long long )lk2) - (long long )lk4 >= 0LL) && (1LL
        + (long long )lk2) - (long long )lk5 >= 0LL) && (1LL + (long long )lk2) -
        (long long )lk6 >= 0LL) && (1LL + (long long )lk2) - (long long )lk7 >= 0LL)
        && (1LL + (long long )lk2) - (long long )lk8 >= 0LL) && (1LL + (long long
        )lk3) - (long long )lk4 >= 0LL) && (1LL + (long long )lk3) - (long long )lk5
        >= 0LL) && (1LL + (long long )lk3) - (long long )lk6 >= 0LL) && (1LL + (long
        long )lk3) - (long long )lk7 >= 0LL) && (1LL + (long long )lk3) - (long long
        )lk8 >= 0LL) && (1LL + (long long )lk4) - (long long )lk5 >= 0LL) && (1LL
        + (long long )lk4) - (long long )lk6 >= 0LL) && (1LL + (long long )lk4) -
        (long long )lk7 >= 0LL) && (1LL + (long long )lk4) - (long long )lk8 >= 0LL)
        && (1LL + (long long )lk5) - (long long )lk6 >= 0LL) && (1LL + (long long
        )lk5) - (long long )lk7 >= 0LL) && (1LL + (long long )lk5) - (long long )lk8
        >= 0LL) && (1LL + (long long )lk6) - (long long )lk7 >= 0LL) && (1LL + (long
        long )lk6) - (long long )lk8 >= 0LL) && (1LL + (long long )lk7) - (long long
        )lk8 >= 0LL) && (2147483647LL + (long long )lk1) - (long long )p1 >= 0LL)
        && (2147483647LL + (long long )lk1) - (long long )p2 >= 0LL) && (2147483647LL
        + (long long )lk1) - (long long )p3 >= 0LL) && (2147483647LL + (long long
        )lk1) - (long long )p4 >= 0LL) && (2147483647LL + (long long )lk1) - (long
        long )p5 >= 0LL) && (2147483647LL + (long long )lk1) - (long long )p6 >= 0LL)
        && (2147483647LL + (long long )lk1) - (long long )p7 >= 0LL) && (2147483647LL
        + (long long )lk1) - (long long )p8 >= 0LL) && (2147483647LL + (long long
        )lk2) - (long long )p1 >= 0LL) && (2147483647LL + (long long )lk2) - (long
        long )p2 >= 0LL) && (2147483647LL + (long long )lk2) - (long long )p3 >= 0LL)
        && (2147483647LL + (long long )lk2) - (long long )p4 >= 0LL) && (2147483647LL
        + (long long )lk2) - (long long )p5 >= 0LL) && (2147483647LL + (long long
        )lk2) - (long long )p6 >= 0LL) && (2147483647LL + (long long )lk2) - (long
        long )p7 >= 0LL) && (2147483647LL + (long long )lk2) - (long long )p8 >= 0LL)
        && (2147483647LL + (long long )lk3) - (long long )p1 >= 0LL) && (2147483647LL
        + (long long )lk3) - (long long )p2 >= 0LL) && (2147483647LL + (long long
        )lk3) - (long long )p3 >= 0LL) && (2147483647LL + (long long )lk3) - (long
        long )p4 >= 0LL) && (2147483647LL + (long long )lk3) - (long long )p5 >= 0LL)
        && (2147483647LL + (long long )lk3) - (long long )p6 >= 0LL) && (2147483647LL
        + (long long )lk3) - (long long )p7 >= 0LL) && (2147483647LL + (long long
        )lk3) - (long long )p8 >= 0LL) && (2147483647LL + (long long )lk4) - (long
        long )p1 >= 0LL) && (2147483647LL + (long long )lk4) - (long long )p2 >= 0LL)
        && (2147483647LL + (long long )lk4) - (long long )p3 >= 0LL) && (2147483647LL
        + (long long )lk4) - (long long )p4 >= 0LL) && (2147483647LL + (long long
        )lk4) - (long long )p5 >= 0LL) && (2147483647LL + (long long )lk4) - (long
        long )p6 >= 0LL) && (2147483647LL + (long long )lk4) - (long long )p7 >= 0LL)
        && (2147483647LL + (long long )lk4) - (long long )p8 >= 0LL) && (2147483647LL
        + (long long )lk5) - (long long )p1 >= 0LL) && (2147483647LL + (long long
        )lk5) - (long long )p2 >= 0LL) && (2147483647LL + (long long )lk5) - (long
        long )p3 >= 0LL) && (2147483647LL + (long long )lk5) - (long long )p4 >= 0LL)
        && (2147483647LL + (long long )lk5) - (long long )p5 >= 0LL) && (2147483647LL
        + (long long )lk5) - (long long )p6 >= 0LL) && (2147483647LL + (long long
        )lk5) - (long long )p7 >= 0LL) && (2147483647LL + (long long )lk5) - (long
        long )p8 >= 0LL) && (2147483647LL + (long long )lk6) - (long long )p1 >= 0LL)
        && (2147483647LL + (long long )lk6) - (long long )p2 >= 0LL) && (2147483647LL
        + (long long )lk6) - (long long )p3 >= 0LL) && (2147483647LL + (long long
        )lk6) - (long long )p4 >= 0LL) && (2147483647LL + (long long )lk6) - (long
        long )p5 >= 0LL) && (2147483647LL + (long long )lk6) - (long long )p6 >= 0LL)
        && (2147483647LL + (long long )lk6) - (long long )p7 >= 0LL) && (2147483647LL
        + (long long )lk6) - (long long )p8 >= 0LL) && (2147483647LL + (long long
        )lk7) - (long long )p1 >= 0LL) && (2147483647LL + (long long )lk7) - (long
        long )p2 >= 0LL) && (2147483647LL + (long long )lk7) - (long long )p3 >= 0LL)
        && (2147483647LL + (long long )lk7) - (long long )p4 >= 0LL) && (2147483647LL
        + (long long )lk7) - (long long )p5 >= 0LL) && (2147483647LL + (long long
        )lk7) - (long long )p6 >= 0LL) && (2147483647LL + (long long )lk7) - (long
        long )p7 >= 0LL) && (2147483647LL + (long long )lk7) - (long long )p8 >= 0LL)
        && (2147483647LL + (long long )lk8) - (long long )p1 >= 0LL) && (2147483647LL
        + (long long )lk8) - (long long )p2 >= 0LL) && (2147483647LL + (long long
        )lk8) - (long long )p3 >= 0LL) && (2147483647LL + (long long )lk8) - (long
        long )p4 >= 0LL) && (2147483647LL + (long long )lk8) - (long long )p5 >= 0LL)
        && (2147483647LL + (long long )lk8) - (long long )p6 >= 0LL) && (2147483647LL
        + (long long )lk8) - (long long )p7 >= 0LL) && (2147483647LL + (long long
        )lk8) - (long long )p8 >= 0LL) && (2LL - (long long )lk1) - (long long )lk2
        >= 0LL) && (2LL - (long long )lk1) - (long long )lk3 >= 0LL) && (2LL - (long
        long )lk1) - (long long )lk4 >= 0LL) && (2LL - (long long )lk1) - (long long
        )lk5 >= 0LL) && (2LL - (long long )lk1) - (long long )lk6 >= 0LL) && (2LL
        - (long long )lk1) - (long long )lk7 >= 0LL) && (2LL - (long long )lk1) -
        (long long )lk8 >= 0LL) && (2LL - (long long )lk2) - (long long )lk3 >= 0LL)
        && (2LL - (long long )lk2) - (long long )lk4 >= 0LL) && (2LL - (long long
        )lk2) - (long long )lk5 >= 0LL) && (2LL - (long long )lk2) - (long long )lk6
        >= 0LL) && (2LL - (long long )lk2) - (long long )lk7 >= 0LL) && (2LL - (long
        long )lk2) - (long long )lk8 >= 0LL) && (2LL - (long long )lk3) - (long long
        )lk4 >= 0LL) && (2LL - (long long )lk3) - (long long )lk5 >= 0LL) && (2LL
        - (long long )lk3) - (long long )lk6 >= 0LL) && (2LL - (long long )lk3) -
        (long long )lk7 >= 0LL) && (2LL - (long long )lk3) - (long long )lk8 >= 0LL)
        && (2LL - (long long )lk4) - (long long )lk5 >= 0LL) && (2LL - (long long
        )lk4) - (long long )lk6 >= 0LL) && (2LL - (long long )lk4) - (long long )lk7
        >= 0LL) && (2LL - (long long )lk4) - (long long )lk8 >= 0LL) && (2LL - (long
        long )lk5) - (long long )lk6 >= 0LL) && (2LL - (long long )lk5) - (long long
        )lk7 >= 0LL) && (2LL - (long long )lk5) - (long long )lk8 >= 0LL) && (2LL
        - (long long )lk6) - (long long )lk7 >= 0LL) && (2LL - (long long )lk6) -
        (long long )lk8 >= 0LL) && (2LL - (long long )lk7) - (long long )lk8 >= 0LL)
        && (2147483647LL - (long long )lk1) - (long long )p1 >= 0LL) && (2147483647LL
        - (long long )lk2) - (long long )p2 >= 0LL) && (2147483647LL - (long long
        )lk3) - (long long )p3 >= 0LL) && (2147483647LL - (long long )lk4) - (long
        long )p4 >= 0LL) && (2147483647LL - (long long )lk5) - (long long )p5 >= 0LL)
        && (2147483647LL - (long long )lk6) - (long long )p6 >= 0LL) && (2147483647LL
        - (long long )lk7) - (long long )p7 >= 0LL) && (2147483647LL - (long long
        )lk8) - (long long )p8 >= 0LL) && (2147483648LL - (long long )lk1) - (long
        long )p2 >= 0LL) && (2147483648LL - (long long )lk1) - (long long )p3 >= 0LL)
        && (2147483648LL - (long long )lk1) - (long long )p4 >= 0LL) && (2147483648LL
        - (long long )lk1) - (long long )p5 >= 0LL) && (2147483648LL - (long long
        )lk1) - (long long )p6 >= 0LL) && (2147483648LL - (long long )lk1) - (long
        long )p7 >= 0LL) && (2147483648LL - (long long )lk1) - (long long )p8 >= 0LL)
        && (2147483648LL - (long long )lk2) - (long long )p1 >= 0LL) && (2147483648LL
        - (long long )lk2) - (long long )p3 >= 0LL) && (2147483648LL - (long long
        )lk2) - (long long )p4 >= 0LL) && (2147483648LL - (long long )lk2) - (long
        long )p5 >= 0LL) && (2147483648LL - (long long )lk2) - (long long )p6 >= 0LL)
        && (2147483648LL - (long long )lk2) - (long long )p7 >= 0LL) && (2147483648LL
        - (long long )lk2) - (long long )p8 >= 0LL) && (2147483648LL - (long long
        )lk3) - (long long )p1 >= 0LL) && (2147483648LL - (long long )lk3) - (long
        long )p2 >= 0LL) && (2147483648LL - (long long )lk3) - (long long )p4 >= 0LL)
        && (2147483648LL - (long long )lk3) - (long long )p5 >= 0LL) && (2147483648LL
        - (long long )lk3) - (long long )p6 >= 0LL) && (2147483648LL - (long long
        )lk3) - (long long )p7 >= 0LL) && (2147483648LL - (long long )lk3) - (long
        long )p8 >= 0LL) && (2147483648LL - (long long )lk4) - (long long )p1 >= 0LL)
        && (2147483648LL - (long long )lk4) - (long long )p2 >= 0LL) && (2147483648LL
        - (long long )lk4) - (long long )p3 >= 0LL) && (2147483648LL - (long long
        )lk4) - (long long )p5 >= 0LL) && (2147483648LL - (long long )lk4) - (long
        long )p6 >= 0LL) && (2147483648LL - (long long )lk4) - (long long )p7 >= 0LL)
        && (2147483648LL - (long long )lk4) - (long long )p8 >= 0LL) && (2147483648LL
        - (long long )lk5) - (long long )p1 >= 0LL) && (2147483648LL - (long long
        )lk5) - (long long )p2 >= 0LL) && (2147483648LL - (long long )lk5) - (long
        long )p3 >= 0LL) && (2147483648LL - (long long )lk5) - (long long )p4 >= 0LL)
        && (2147483648LL - (long long )lk5) - (long long )p6 >= 0LL) && (2147483648LL
        - (long long )lk5) - (long long )p7 >= 0LL) && (2147483648LL - (long long
        )lk5) - (long long )p8 >= 0LL) && (2147483648LL - (long long )lk6) - (long
        long )p1 >= 0LL) && (2147483648LL - (long long )lk6) - (long long )p2 >= 0LL)
        && (2147483648LL - (long long )lk6) - (long long )p3 >= 0LL) && (2147483648LL
        - (long long )lk6) - (long long )p4 >= 0LL) && (2147483648LL - (long long
        )lk6) - (long long )p5 >= 0LL) && (2147483648LL - (long long )lk6) - (long
        long )p7 >= 0LL) && (2147483648LL - (long long )lk6) - (long long )p8 >= 0LL)
        && (2147483648LL - (long long )lk7) - (long long )p1 >= 0LL) && (2147483648LL
        - (long long )lk7) - (long long )p2 >= 0LL) && (2147483648LL - (long long
        )lk7) - (long long )p3 >= 0LL) && (2147483648LL - (long long )lk7) - (long
        long )p4 >= 0LL) && (2147483648LL - (long long )lk7) - (long long )p5 >= 0LL)
        && (2147483648LL - (long long )lk7) - (long long )p6 >= 0LL) && (2147483648LL
        - (long long )lk7) - (long long )p8 >= 0LL) && (2147483648LL - (long long
        )lk8) - (long long )p1 >= 0LL) && (2147483648LL - (long long )lk8) - (long
        long )p2 >= 0LL) && (2147483648LL - (long long )lk8) - (long long )p3 >= 0LL)
        && (2147483648LL - (long long )lk8) - (long long )p4 >= 0LL) && (2147483648LL
        - (long long )lk8) - (long long )p5 >= 0LL) && (2147483648LL - (long long
        )lk8) - (long long )p6 >= 0LL) && (2147483648LL - (long long )lk8) - (long
        long )p7 >= 0LL) && (lk1 == 0 || lk1 == 1)) && (lk2 == 0 || lk2 == 1)) &&
        (lk3 == 0 || lk3 == 1)) && (lk4 == 0 || lk4 == 1)) && (lk5 == 0 || lk5 ==
        1)) && (lk6 == 0 || lk6 == 1)) && (lk7 == 0 || lk7 == 1)) && (lk8 == 0 ||
        lk8 == 1)) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((4294967296LL
        + (long long )lk1) + (long long )p1 >= 0LL && (4294967296LL + (long long )lk1)
        + (long long )p2 >= 0LL) && (4294967296LL + (long long )lk1) + (long long
        )lk2 >= 0LL) && (4294967296LL + (long long )lk1) + (long long )p3 >= 0LL)
        && (4294967296LL + (long long )lk1) + (long long )lk3 >= 0LL) && (4294967296LL
        + (long long )lk1) + (long long )p4 >= 0LL) && (4294967296LL + (long long
        )lk1) + (long long )lk4 >= 0LL) && (4294967296LL + (long long )lk1) + (long
        long )p5 >= 0LL) && (4294967296LL + (long long )lk1) + (long long )lk5 >=
        0LL) && (4294967296LL + (long long )lk1) + (long long )p6 >= 0LL) && (4294967296LL
        + (long long )lk1) + (long long )lk6 >= 0LL) && (4294967296LL + (long long
        )lk1) + (long long )p7 >= 0LL) && (4294967296LL + (long long )lk1) + (long
        long )lk7 >= 0LL) && (4294967296LL + (long long )lk1) + (long long )p8 >=
        0LL) && (4294967296LL + (long long )lk1) + (long long )lk8 >= 0LL) && (4294967296LL
        + (long long )lk2) + (long long )p1 >= 0LL) && (4294967296LL + (long long
        )lk2) + (long long )p2 >= 0LL) && (4294967296LL + (long long )lk2) + (long
        long )p3 >= 0LL) && (4294967296LL + (long long )lk2) + (long long )lk3 >=
        0LL) && (4294967296LL + (long long )lk2) + (long long )p4 >= 0LL) && (4294967296LL
        + (long long )lk2) + (long long )lk4 >= 0LL) && (4294967296LL + (long long
        )lk2) + (long long )p5 >= 0LL) && (4294967296LL + (long long )lk2) + (long
        long )lk5 >= 0LL) && (4294967296LL + (long long )lk2) + (long long )p6 >=
        0LL) && (4294967296LL + (long long )lk2) + (long long )lk6 >= 0LL) && (4294967296LL
        + (long long )lk2) + (long long )p7 >= 0LL) && (4294967296LL + (long long
        )lk2) + (long long )lk7 >= 0LL) && (4294967296LL + (long long )lk2) + (long
        long )p8 >= 0LL) && (4294967296LL + (long long )lk2) + (long long )lk8 >=
        0LL) && (4294967296LL + (long long )lk3) + (long long )p1 >= 0LL) && (4294967296LL
        + (long long )lk3) + (long long )p2 >= 0LL) && (4294967296LL + (long long
        )lk3) + (long long )p3 >= 0LL) && (4294967296LL + (long long )lk3) + (long
        long )p4 >= 0LL) && (4294967296LL + (long long )lk3) + (long long )lk4 >=
        0LL) && (4294967296LL + (long long )lk3) + (long long )p5 >= 0LL) && (4294967296LL
        + (long long )lk3) + (long long )lk5 >= 0LL) && (4294967296LL + (long long
        )lk3) + (long long )p6 >= 0LL) && (4294967296LL + (long long )lk3) + (long
        long )lk6 >= 0LL) && (4294967296LL + (long long )lk3) + (long long )p7 >=
        0LL) && (4294967296LL + (long long )lk3) + (long long )lk7 >= 0LL) && (4294967296LL
        + (long long )lk3) + (long long )p8 >= 0LL) && (4294967296LL + (long long
        )lk3) + (long long )lk8 >= 0LL) && (4294967296LL + (long long )lk4) + (long
        long )p1 >= 0LL) && (4294967296LL + (long long )lk4) + (long long )p2 >= 0LL)
        && (4294967296LL + (long long )lk4) + (long long )p3 >= 0LL) && (4294967296LL
        + (long long )lk4) + (long long )p4 >= 0LL) && (4294967296LL + (long long
        )lk4) + (long long )p5 >= 0LL) && (4294967296LL + (long long )lk4) + (long
        long )lk5 >= 0LL) && (4294967296LL + (long long )lk4) + (long long )p6 >=
        0LL) && (4294967296LL + (long long )lk4) + (long long )lk6 >= 0LL) && (4294967296LL
        + (long long )lk4) + (long long )p7 >= 0LL) && (4294967296LL + (long long
        )lk4) + (long long )lk7 >= 0LL) && (4294967296LL + (long long )lk4) + (long
        long )p8 >= 0LL) && (4294967296LL + (long long )lk4) + (long long )lk8 >=
        0LL) && (4294967296LL + (long long )lk5) + (long long )p1 >= 0LL) && (4294967296LL
        + (long long )lk5) + (long long )p2 >= 0LL) && (4294967296LL + (long long
        )lk5) + (long long )p3 >= 0LL) && (4294967296LL + (long long )lk5) + (long
        long )p4 >= 0LL) && (4294967296LL + (long long )lk5) + (long long )p5 >= 0LL)
        && (4294967296LL + (long long )lk5) + (long long )p6 >= 0LL) && (4294967296LL
        + (long long )lk5) + (long long )lk6 >= 0LL) && (4294967296LL + (long long
        )lk5) + (long long )p7 >= 0LL) && (4294967296LL + (long long )lk5) + (long
        long )lk7 >= 0LL) && (4294967296LL + (long long )lk5) + (long long )p8 >=
        0LL) && (4294967296LL + (long long )lk5) + (long long )lk8 >= 0LL) && (4294967296LL
        + (long long )lk6) + (long long )p1 >= 0LL) && (4294967296LL + (long long
        )lk6) + (long long )p2 >= 0LL) && (4294967296LL + (long long )lk6) + (long
        long )p3 >= 0LL) && (4294967296LL + (long long )lk6) + (long long )p4 >= 0LL)
        && (4294967296LL + (long long )lk6) + (long long )p5 >= 0LL) && (4294967296LL
        + (long long )lk6) + (long long )p6 >= 0LL) && (4294967296LL + (long long
        )lk6) + (long long )p7 >= 0LL) && (4294967296LL + (long long )lk6) + (long
        long )lk7 >= 0LL) && (4294967296LL + (long long )lk6) + (long long )p8 >=
        0LL) && (4294967296LL + (long long )lk6) + (long long )lk8 >= 0LL) && (4294967296LL
        + (long long )lk7) + (long long )p1 >= 0LL) && (4294967296LL + (long long
        )lk7) + (long long )p2 >= 0LL) && (4294967296LL + (long long )lk7) + (long
        long )p3 >= 0LL) && (4294967296LL + (long long )lk7) + (long long )p4 >= 0LL)
        && (4294967296LL + (long long )lk7) + (long long )p5 >= 0LL) && (4294967296LL
        + (long long )lk7) + (long long )p6 >= 0LL) && (4294967296LL + (long long
        )lk7) + (long long )p7 >= 0LL) && (4294967296LL + (long long )lk7) + (long
        long )p8 >= 0LL) && (4294967296LL + (long long )lk7) + (long long )lk8 >=
        0LL) && (4294967296LL + (long long )lk8) + (long long )p1 >= 0LL) && (4294967296LL
        + (long long )lk8) + (long long )p2 >= 0LL) && (4294967296LL + (long long
        )lk8) + (long long )p3 >= 0LL) && (4294967296LL + (long long )lk8) + (long
        long )p4 >= 0LL) && (4294967296LL + (long long )lk8) + (long long )p5 >= 0LL)
        && (4294967296LL + (long long )lk8) + (long long )p6 >= 0LL) && (4294967296LL
        + (long long )lk8) + (long long )p7 >= 0LL) && (4294967296LL + (long long
        )lk8) + (long long )p8 >= 0LL) && (4294967295LL - (long long )lk1) + (long
        long )p1 >= 0LL) && (4294967295LL - (long long )lk1) + (long long )p2 >= 0LL)
        && (4294967295LL - (long long )lk1) + (long long )lk2 >= 0LL) && (4294967295LL
        - (long long )lk1) + (long long )p3 >= 0LL) && (4294967295LL - (long long
        )lk1) + (long long )lk3 >= 0LL) && (4294967295LL - (long long )lk1) + (long
        long )p4 >= 0LL) && (4294967295LL - (long long )lk1) + (long long )lk4 >=
        0LL) && (4294967295LL - (long long )lk1) + (long long )p5 >= 0LL) && (4294967295LL
        - (long long )lk1) + (long long )lk5 >= 0LL) && (4294967295LL - (long long
        )lk1) + (long long )p6 >= 0LL) && (4294967295LL - (long long )lk1) + (long
        long )lk6 >= 0LL) && (4294967295LL - (long long )lk1) + (long long )p7 >=
        0LL) && (4294967295LL - (long long )lk1) + (long long )lk7 >= 0LL) && (4294967295LL
        - (long long )lk1) + (long long )p8 >= 0LL) && (4294967295LL - (long long
        )lk1) + (long long )lk8 >= 0LL) && (4294967295LL - (long long )lk2) + (long
        long )p1 >= 0LL) && (4294967295LL - (long long )lk2) + (long long )p2 >= 0LL)
        && (4294967295LL - (long long )lk2) + (long long )p3 >= 0LL) && (4294967295LL
        - (long long )lk2) + (long long )lk3 >= 0LL) && (4294967295LL - (long long
        )lk2) + (long long )p4 >= 0LL) && (4294967295LL - (long long )lk2) + (long
        long )lk4 >= 0LL) && (4294967295LL - (long long )lk2) + (long long )p5 >=
        0LL) && (4294967295LL - (long long )lk2) + (long long )lk5 >= 0LL) && (4294967295LL
        - (long long )lk2) + (long long )p6 >= 0LL) && (4294967295LL - (long long
        )lk2) + (long long )lk6 >= 0LL) && (4294967295LL - (long long )lk2) + (long
        long )p7 >= 0LL) && (4294967295LL - (long long )lk2) + (long long )lk7 >=
        0LL) && (4294967295LL - (long long )lk2) + (long long )p8 >= 0LL) && (4294967295LL
        - (long long )lk2) + (long long )lk8 >= 0LL) && (4294967295LL - (long long
        )lk3) + (long long )p1 >= 0LL) && (4294967295LL - (long long )lk3) + (long
        long )p2 >= 0LL) && (4294967295LL - (long long )lk3) + (long long )p3 >= 0LL)
        && (4294967295LL - (long long )lk3) + (long long )p4 >= 0LL) && (4294967295LL
        - (long long )lk3) + (long long )lk4 >= 0LL) && (4294967295LL - (long long
        )lk3) + (long long )p5 >= 0LL) && (4294967295LL - (long long )lk3) + (long
        long )lk5 >= 0LL) && (4294967295LL - (long long )lk3) + (long long )p6 >=
        0LL) && (4294967295LL - (long long )lk3) + (long long )lk6 >= 0LL) && (4294967295LL
        - (long long )lk3) + (long long )p7 >= 0LL) && (4294967295LL - (long long
        )lk3) + (long long )lk7 >= 0LL) && (4294967295LL - (long long )lk3) + (long
        long )p8 >= 0LL) && (4294967295LL - (long long )lk3) + (long long )lk8 >=
        0LL) && (4294967295LL - (long long )lk4) + (long long )p1 >= 0LL) && (4294967295LL
        - (long long )lk4) + (long long )p2 >= 0LL) && (4294967295LL - (long long
        )lk4) + (long long )p3 >= 0LL) && (4294967295LL - (long long )lk4) + (long
        long )p4 >= 0LL) && (4294967295LL - (long long )lk4) + (long long )p5 >= 0LL)
        && (4294967295LL - (long long )lk4) + (long long )lk5 >= 0LL) && (4294967295LL
        - (long long )lk4) + (long long )p6 >= 0LL) && (4294967295LL - (long long
        )lk4) + (long long )lk6 >= 0LL) && (4294967295LL - (long long )lk4) + (long
        long )p7 >= 0LL) && (4294967295LL - (long long )lk4) + (long long )lk7 >=
        0LL) && (4294967295LL - (long long )lk4) + (long long )p8 >= 0LL) && (4294967295LL
        - (long long )lk4) + (long long )lk8 >= 0LL) && (4294967295LL - (long long
        )lk5) + (long long )p1 >= 0LL) && (4294967295LL - (long long )lk5) + (long
        long )p2 >= 0LL) && (4294967295LL - (long long )lk5) + (long long )p3 >= 0LL)
        && (4294967295LL - (long long )lk5) + (long long )p4 >= 0LL) && (4294967295LL
        - (long long )lk5) + (long long )p5 >= 0LL) && (4294967295LL - (long long
        )lk5) + (long long )p6 >= 0LL) && (4294967295LL - (long long )lk5) + (long
        long )lk6 >= 0LL) && (4294967295LL - (long long )lk5) + (long long )p7 >=
        0LL) && (4294967295LL - (long long )lk5) + (long long )lk7 >= 0LL) && (4294967295LL
        - (long long )lk5) + (long long )p8 >= 0LL) && (4294967295LL - (long long
        )lk5) + (long long )lk8 >= 0LL) && (4294967295LL - (long long )lk6) + (long
        long )p1 >= 0LL) && (4294967295LL - (long long )lk6) + (long long )p2 >= 0LL)
        && (4294967295LL - (long long )lk6) + (long long )p3 >= 0LL) && (4294967295LL
        - (long long )lk6) + (long long )p4 >= 0LL) && (4294967295LL - (long long
        )lk6) + (long long )p5 >= 0LL) && (4294967295LL - (long long )lk6) + (long
        long )p6 >= 0LL) && (4294967295LL - (long long )lk6) + (long long )p7 >= 0LL)
        && (4294967295LL - (long long )lk6) + (long long )lk7 >= 0LL) && (4294967295LL
        - (long long )lk6) + (long long )p8 >= 0LL) && (4294967295LL - (long long
        )lk6) + (long long )lk8 >= 0LL) && (4294967295LL - (long long )lk7) + (long
        long )p1 >= 0LL) && (4294967295LL - (long long )lk7) + (long long )p2 >= 0LL)
        && (4294967295LL - (long long )lk7) + (long long )p3 >= 0LL) && (4294967295LL
        - (long long )lk7) + (long long )p4 >= 0LL) && (4294967295LL - (long long
        )lk7) + (long long )p5 >= 0LL) && (4294967295LL - (long long )lk7) + (long
        long )p6 >= 0LL) && (4294967295LL - (long long )lk7) + (long long )p7 >= 0LL)
        && (4294967295LL - (long long )lk7) + (long long )p8 >= 0LL) && (4294967295LL
        - (long long )lk7) + (long long )lk8 >= 0LL) && (4294967295LL - (long long
        )lk8) + (long long )p1 >= 0LL) && (4294967295LL - (long long )lk8) + (long
        long )p2 >= 0LL) && (4294967295LL - (long long )lk8) + (long long )p3 >= 0LL)
        && (4294967295LL - (long long )lk8) + (long long )p4 >= 0LL) && (4294967295LL
        - (long long )lk8) + (long long )p5 >= 0LL) && (4294967295LL - (long long
        )lk8) + (long long )p6 >= 0LL) && (4294967295LL - (long long )lk8) + (long
        long )p7 >= 0LL) && (4294967295LL - (long long )lk8) + (long long )p8 >= 0LL)
        && (4294967295LL + (long long )lk1) - (long long )p1 >= 0LL) && (4294967295LL
        + (long long )lk1) - (long long )p2 >= 0LL) && (4294967295LL + (long long
        )lk1) - (long long )lk2 >= 0LL) && (4294967295LL + (long long )lk1) - (long
        long )p3 >= 0LL) && (4294967295LL + (long long )lk1) - (long long )lk3 >=
        0LL) && (4294967295LL + (long long )lk1) - (long long )p4 >= 0LL) && (4294967295LL
        + (long long )lk1) - (long long )lk4 >= 0LL) && (4294967295LL + (long long
        )lk1) - (long long )p5 >= 0LL) && (4294967295LL + (long long )lk1) - (long
        long )lk5 >= 0LL) && (4294967295LL + (long long )lk1) - (long long )p6 >=
        0LL) && (4294967295LL + (long long )lk1) - (long long )lk6 >= 0LL) && (4294967295LL
        + (long long )lk1) - (long long )p7 >= 0LL) && (4294967295LL + (long long
        )lk1) - (long long )lk7 >= 0LL) && (4294967295LL + (long long )lk1) - (long
        long )p8 >= 0LL) && (4294967295LL + (long long )lk1) - (long long )lk8 >=
        0LL) && (4294967295LL + (long long )lk2) - (long long )p1 >= 0LL) && (4294967295LL
        + (long long )lk2) - (long long )p2 >= 0LL) && (4294967295LL + (long long
        )lk2) - (long long )p3 >= 0LL) && (4294967295LL + (long long )lk2) - (long
        long )lk3 >= 0LL) && (4294967295LL + (long long )lk2) - (long long )p4 >=
        0LL) && (4294967295LL + (long long )lk2) - (long long )lk4 >= 0LL) && (4294967295LL
        + (long long )lk2) - (long long )p5 >= 0LL) && (4294967295LL + (long long
        )lk2) - (long long )lk5 >= 0LL) && (4294967295LL + (long long )lk2) - (long
        long )p6 >= 0LL) && (4294967295LL + (long long )lk2) - (long long )lk6 >=
        0LL) && (4294967295LL + (long long )lk2) - (long long )p7 >= 0LL) && (4294967295LL
        + (long long )lk2) - (long long )lk7 >= 0LL) && (4294967295LL + (long long
        )lk2) - (long long )p8 >= 0LL) && (4294967295LL + (long long )lk2) - (long
        long )lk8 >= 0LL) && (4294967295LL + (long long )lk3) - (long long )p1 >=
        0LL) && (4294967295LL + (long long )lk3) - (long long )p2 >= 0LL) && (4294967295LL
        + (long long )lk3) - (long long )p3 >= 0LL) && (4294967295LL + (long long
        )lk3) - (long long )p4 >= 0LL) && (4294967295LL + (long long )lk3) - (long
        long )lk4 >= 0LL) && (4294967295LL + (long long )lk3) - (long long )p5 >=
        0LL) && (4294967295LL + (long long )lk3) - (long long )lk5 >= 0LL) && (4294967295LL
        + (long long )lk3) - (long long )p6 >= 0LL) && (4294967295LL + (long long
        )lk3) - (long long )lk6 >= 0LL) && (4294967295LL + (long long )lk3) - (long
        long )p7 >= 0LL) && (4294967295LL + (long long )lk3) - (long long )lk7 >=
        0LL) && (4294967295LL + (long long )lk3) - (long long )p8 >= 0LL) && (4294967295LL
        + (long long )lk3) - (long long )lk8 >= 0LL) && (4294967295LL + (long long
        )lk4) - (long long )p1 >= 0LL) && (4294967295LL + (long long )lk4) - (long
        long )p2 >= 0LL) && (4294967295LL + (long long )lk4) - (long long )p3 >= 0LL)
        && (4294967295LL + (long long )lk4) - (long long )p4 >= 0LL) && (4294967295LL
        + (long long )lk4) - (long long )p5 >= 0LL) && (4294967295LL + (long long
        )lk4) - (long long )lk5 >= 0LL) && (4294967295LL + (long long )lk4) - (long
        long )p6 >= 0LL) && (4294967295LL + (long long )lk4) - (long long )lk6 >=
        0LL) && (4294967295LL + (long long )lk4) - (long long )p7 >= 0LL) && (4294967295LL
        + (long long )lk4) - (long long )lk7 >= 0LL) && (4294967295LL + (long long
        )lk4) - (long long )p8 >= 0LL) && (4294967295LL + (long long )lk4) - (long
        long )lk8 >= 0LL) && (4294967295LL + (long long )lk5) - (long long )p1 >=
        0LL) && (4294967295LL + (long long )lk5) - (long long )p2 >= 0LL) && (4294967295LL
        + (long long )lk5) - (long long )p3 >= 0LL) && (4294967295LL + (long long
        )lk5) - (long long )p4 >= 0LL) && (4294967295LL + (long long )lk5) - (long
        long )p5 >= 0LL) && (4294967295LL + (long long )lk5) - (long long )p6 >= 0LL)
        && (4294967295LL + (long long )lk5) - (long long )lk6 >= 0LL) && (4294967295LL
        + (long long )lk5) - (long long )p7 >= 0LL) && (4294967295LL + (long long
        )lk5) - (long long )lk7 >= 0LL) && (4294967295LL + (long long )lk5) - (long
        long )p8 >= 0LL) && (4294967295LL + (long long )lk5) - (long long )lk8 >=
        0LL) && (4294967295LL + (long long )lk6) - (long long )p1 >= 0LL) && (4294967295LL
        + (long long )lk6) - (long long )p2 >= 0LL) && (4294967295LL + (long long
        )lk6) - (long long )p3 >= 0LL) && (4294967295LL + (long long )lk6) - (long
        long )p4 >= 0LL) && (4294967295LL + (long long )lk6) - (long long )p5 >= 0LL)
        && (4294967295LL + (long long )lk6) - (long long )p6 >= 0LL) && (4294967295LL
        + (long long )lk6) - (long long )p7 >= 0LL) && (4294967295LL + (long long
        )lk6) - (long long )lk7 >= 0LL) && (4294967295LL + (long long )lk6) - (long
        long )p8 >= 0LL) && (4294967295LL + (long long )lk6) - (long long )lk8 >=
        0LL) && (4294967295LL + (long long )lk7) - (long long )p1 >= 0LL) && (4294967295LL
        + (long long )lk7) - (long long )p2 >= 0LL) && (4294967295LL + (long long
        )lk7) - (long long )p3 >= 0LL) && (4294967295LL + (long long )lk7) - (long
        long )p4 >= 0LL) && (4294967295LL + (long long )lk7) - (long long )p5 >= 0LL)
        && (4294967295LL + (long long )lk7) - (long long )p6 >= 0LL) && (4294967295LL
        + (long long )lk7) - (long long )p7 >= 0LL) && (4294967295LL + (long long
        )lk7) - (long long )p8 >= 0LL) && (4294967295LL + (long long )lk7) - (long
        long )lk8 >= 0LL) && (4294967295LL + (long long )lk8) - (long long )p1 >=
        0LL) && (4294967295LL + (long long )lk8) - (long long )p2 >= 0LL) && (4294967295LL
        + (long long )lk8) - (long long )p3 >= 0LL) && (4294967295LL + (long long
        )lk8) - (long long )p4 >= 0LL) && (4294967295LL + (long long )lk8) - (long
        long )p5 >= 0LL) && (4294967295LL + (long long )lk8) - (long long )p6 >= 0LL)
        && (4294967295LL + (long long )lk8) - (long long )p7 >= 0LL) && (4294967295LL
        + (long long )lk8) - (long long )p8 >= 0LL) && (4294967294LL - (long long
        )lk1) - (long long )p1 >= 0LL) && (4294967294LL - (long long )lk1) - (long
        long )p2 >= 0LL) && (4294967294LL - (long long )lk1) - (long long )lk2 >=
        0LL) && (4294967294LL - (long long )lk1) - (long long )p3 >= 0LL) && (4294967294LL
        - (long long )lk1) - (long long )lk3 >= 0LL) && (4294967294LL - (long long
        )lk1) - (long long )p4 >= 0LL) && (4294967294LL - (long long )lk1) - (long
        long )lk4 >= 0LL) && (4294967294LL - (long long )lk1) - (long long )p5 >=
        0LL) && (4294967294LL - (long long )lk1) - (long long )lk5 >= 0LL) && (4294967294LL
        - (long long )lk1) - (long long )p6 >= 0LL) && (4294967294LL - (long long
        )lk1) - (long long )lk6 >= 0LL) && (4294967294LL - (long long )lk1) - (long
        long )p7 >= 0LL) && (4294967294LL - (long long )lk1) - (long long )lk7 >=
        0LL) && (4294967294LL - (long long )lk1) - (long long )p8 >= 0LL) && (4294967294LL
        - (long long )lk1) - (long long )lk8 >= 0LL) && (4294967294LL - (long long
        )lk2) - (long long )p1 >= 0LL) && (4294967294LL - (long long )lk2) - (long
        long )p2 >= 0LL) && (4294967294LL - (long long )lk2) - (long long )p3 >= 0LL)
        && (4294967294LL - (long long )lk2) - (long long )lk3 >= 0LL) && (4294967294LL
        - (long long )lk2) - (long long )p4 >= 0LL) && (4294967294LL - (long long
        )lk2) - (long long )lk4 >= 0LL) && (4294967294LL - (long long )lk2) - (long
        long )p5 >= 0LL) && (4294967294LL - (long long )lk2) - (long long )lk5 >=
        0LL) && (4294967294LL - (long long )lk2) - (long long )p6 >= 0LL) && (4294967294LL
        - (long long )lk2) - (long long )lk6 >= 0LL) && (4294967294LL - (long long
        )lk2) - (long long )p7 >= 0LL) && (4294967294LL - (long long )lk2) - (long
        long )lk7 >= 0LL) && (4294967294LL - (long long )lk2) - (long long )p8 >=
        0LL) && (4294967294LL - (long long )lk2) - (long long )lk8 >= 0LL) && (4294967294LL
        - (long long )lk3) - (long long )p1 >= 0LL) && (4294967294LL - (long long
        )lk3) - (long long )p2 >= 0LL) && (4294967294LL - (long long )lk3) - (long
        long )p3 >= 0LL) && (4294967294LL - (long long )lk3) - (long long )p4 >= 0LL)
        && (4294967294LL - (long long )lk3) - (long long )lk4 >= 0LL) && (4294967294LL
        - (long long )lk3) - (long long )p5 >= 0LL) && (4294967294LL - (long long
        )lk3) - (long long )lk5 >= 0LL) && (4294967294LL - (long long )lk3) - (long
        long )p6 >= 0LL) && (4294967294LL - (long long )lk3) - (long long )lk6 >=
        0LL) && (4294967294LL - (long long )lk3) - (long long )p7 >= 0LL) && (4294967294LL
        - (long long )lk3) - (long long )lk7 >= 0LL) && (4294967294LL - (long long
        )lk3) - (long long )p8 >= 0LL) && (4294967294LL - (long long )lk3) - (long
        long )lk8 >= 0LL) && (4294967294LL - (long long )lk4) - (long long )p1 >=
        0LL) && (4294967294LL - (long long )lk4) - (long long )p2 >= 0LL) && (4294967294LL
        - (long long )lk4) - (long long )p3 >= 0LL) && (4294967294LL - (long long
        )lk4) - (long long )p4 >= 0LL) && (4294967294LL - (long long )lk4) - (long
        long )p5 >= 0LL) && (4294967294LL - (long long )lk4) - (long long )lk5 >=
        0LL) && (4294967294LL - (long long )lk4) - (long long )p6 >= 0LL) && (4294967294LL
        - (long long )lk4) - (long long )lk6 >= 0LL) && (4294967294LL - (long long
        )lk4) - (long long )p7 >= 0LL) && (4294967294LL - (long long )lk4) - (long
        long )lk7 >= 0LL) && (4294967294LL - (long long )lk4) - (long long )p8 >=
        0LL) && (4294967294LL - (long long )lk4) - (long long )lk8 >= 0LL) && (4294967294LL
        - (long long )lk5) - (long long )p1 >= 0LL) && (4294967294LL - (long long
        )lk5) - (long long )p2 >= 0LL) && (4294967294LL - (long long )lk5) - (long
        long )p3 >= 0LL) && (4294967294LL - (long long )lk5) - (long long )p4 >= 0LL)
        && (4294967294LL - (long long )lk5) - (long long )p5 >= 0LL) && (4294967294LL
        - (long long )lk5) - (long long )p6 >= 0LL) && (4294967294LL - (long long
        )lk5) - (long long )lk6 >= 0LL) && (4294967294LL - (long long )lk5) - (long
        long )p7 >= 0LL) && (4294967294LL - (long long )lk5) - (long long )lk7 >=
        0LL) && (4294967294LL - (long long )lk5) - (long long )p8 >= 0LL) && (4294967294LL
        - (long long )lk5) - (long long )lk8 >= 0LL) && (4294967294LL - (long long
        )lk6) - (long long )p1 >= 0LL) && (4294967294LL - (long long )lk6) - (long
        long )p2 >= 0LL) && (4294967294LL - (long long )lk6) - (long long )p3 >= 0LL)
        && (4294967294LL - (long long )lk6) - (long long )p4 >= 0LL) && (4294967294LL
        - (long long )lk6) - (long long )p5 >= 0LL) && (4294967294LL - (long long
        )lk6) - (long long )p6 >= 0LL) && (4294967294LL - (long long )lk6) - (long
        long )p7 >= 0LL) && (4294967294LL - (long long )lk6) - (long long )lk7 >=
        0LL) && (4294967294LL - (long long )lk6) - (long long )p8 >= 0LL) && (4294967294LL
        - (long long )lk6) - (long long )lk8 >= 0LL) && (4294967294LL - (long long
        )lk7) - (long long )p1 >= 0LL) && (4294967294LL - (long long )lk7) - (long
        long )p2 >= 0LL) && (4294967294LL - (long long )lk7) - (long long )p3 >= 0LL)
        && (4294967294LL - (long long )lk7) - (long long )p4 >= 0LL) && (4294967294LL
        - (long long )lk7) - (long long )p5 >= 0LL) && (4294967294LL - (long long
        )lk7) - (long long )p6 >= 0LL) && (4294967294LL - (long long )lk7) - (long
        long )p7 >= 0LL) && (4294967294LL - (long long )lk7) - (long long )p8 >= 0LL)
        && (4294967294LL - (long long )lk7) - (long long )lk8 >= 0LL) && (4294967294LL
        - (long long )lk8) - (long long )p1 >= 0LL) && (4294967294LL - (long long
        )lk8) - (long long )p2 >= 0LL) && (4294967294LL - (long long )lk8) - (long
        long )p3 >= 0LL) && (4294967294LL - (long long )lk8) - (long long )p4 >= 0LL)
        && (4294967294LL - (long long )lk8) - (long long )p5 >= 0LL) && (4294967294LL
        - (long long )lk8) - (long long )p6 >= 0LL) && (4294967294LL - (long long
        )lk8) - (long long )p7 >= 0LL) && (4294967294LL - (long long )lk8) - (long
        long )p8 >= 0LL)) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((2147483648LL
        + (long long )lk1) + (long long )p1 >= 0LL && (2147483648LL + (long long )lk1)
        + (long long )p2 >= 0LL) && (2147483648LL + (long long )lk1) + (long long
        )p3 >= 0LL) && (2147483648LL + (long long )lk1) + (long long )p4 >= 0LL) &&
        (2147483648LL + (long long )lk1) + (long long )p5 >= 0LL) && (2147483648LL
        + (long long )lk1) + (long long )p6 >= 0LL) && (2147483648LL + (long long
        )lk1) + (long long )p7 >= 0LL) && (2147483648LL + (long long )lk1) + (long
        long )p8 >= 0LL) && (2147483648LL + (long long )lk2) + (long long )p1 >= 0LL)
        && (2147483648LL + (long long )lk2) + (long long )p2 >= 0LL) && (2147483648LL
        + (long long )lk2) + (long long )p3 >= 0LL) && (2147483648LL + (long long
        )lk2) + (long long )p4 >= 0LL) && (2147483648LL + (long long )lk2) + (long
        long )p5 >= 0LL) && (2147483648LL + (long long )lk2) + (long long )p6 >= 0LL)
        && (2147483648LL + (long long )lk2) + (long long )p7 >= 0LL) && (2147483648LL
        + (long long )lk2) + (long long )p8 >= 0LL) && (2147483648LL + (long long
        )lk3) + (long long )p1 >= 0LL) && (2147483648LL + (long long )lk3) + (long
        long )p2 >= 0LL) && (2147483648LL + (long long )lk3) + (long long )p3 >= 0LL)
        && (2147483648LL + (long long )lk3) + (long long )p4 >= 0LL) && (2147483648LL
        + (long long )lk3) + (long long )p5 >= 0LL) && (2147483648LL + (long long
        )lk3) + (long long )p6 >= 0LL) && (2147483648LL + (long long )lk3) + (long
        long )p7 >= 0LL) && (2147483648LL + (long long )lk3) + (long long )p8 >= 0LL)
        && (2147483648LL + (long long )lk4) + (long long )p1 >= 0LL) && (2147483648LL
        + (long long )lk4) + (long long )p2 >= 0LL) && (2147483648LL + (long long
        )lk4) + (long long )p3 >= 0LL) && (2147483648LL + (long long )lk4) + (long
        long )p4 >= 0LL) && (2147483648LL + (long long )lk4) + (long long )p5 >= 0LL)
        && (2147483648LL + (long long )lk4) + (long long )p6 >= 0LL) && (2147483648LL
        + (long long )lk4) + (long long )p7 >= 0LL) && (2147483648LL + (long long
        )lk4) + (long long )p8 >= 0LL) && (2147483648LL + (long long )lk5) + (long
        long )p1 >= 0LL) && (2147483648LL + (long long )lk5) + (long long )p2 >= 0LL)
        && (2147483648LL + (long long )lk5) + (long long )p3 >= 0LL) && (2147483648LL
        + (long long )lk5) + (long long )p4 >= 0LL) && (2147483648LL + (long long
        )lk5) + (long long )p5 >= 0LL) && (2147483648LL + (long long )lk5) + (long
        long )p6 >= 0LL) && (2147483648LL + (long long )lk5) + (long long )p7 >= 0LL)
        && (2147483648LL + (long long )lk5) + (long long )p8 >= 0LL) && (2147483648LL
        + (long long )lk6) + (long long )p1 >= 0LL) && (2147483648LL + (long long
        )lk6) + (long long )p2 >= 0LL) && (2147483648LL + (long long )lk6) + (long
        long )p3 >= 0LL) && (2147483648LL + (long long )lk6) + (long long )p4 >= 0LL)
        && (2147483648LL + (long long )lk6) + (long long )p5 >= 0LL) && (2147483648LL
        + (long long )lk6) + (long long )p6 >= 0LL) && (2147483648LL + (long long
        )lk6) + (long long )p7 >= 0LL) && (2147483648LL + (long long )lk6) + (long
        long )p8 >= 0LL) && (2147483648LL + (long long )lk7) + (long long )p1 >= 0LL)
        && (2147483648LL + (long long )lk7) + (long long )p2 >= 0LL) && (2147483648LL
        + (long long )lk7) + (long long )p3 >= 0LL) && (2147483648LL + (long long
        )lk7) + (long long )p4 >= 0LL) && (2147483648LL + (long long )lk7) + (long
        long )p5 >= 0LL) && (2147483648LL + (long long )lk7) + (long long )p6 >= 0LL)
        && (2147483648LL + (long long )lk7) + (long long )p7 >= 0LL) && (2147483648LL
        + (long long )lk7) + (long long )p8 >= 0LL) && (2147483648LL + (long long
        )lk8) + (long long )p1 >= 0LL) && (2147483648LL + (long long )lk8) + (long
        long )p2 >= 0LL) && (2147483648LL + (long long )lk8) + (long long )p3 >= 0LL)
        && (2147483648LL + (long long )lk8) + (long long )p4 >= 0LL) && (2147483648LL
        + (long long )lk8) + (long long )p5 >= 0LL) && (2147483648LL + (long long
        )lk8) + (long long )p6 >= 0LL) && (2147483648LL + (long long )lk8) + (long
        long )p7 >= 0LL) && (2147483648LL + (long long )lk8) + (long long )p8 >= 0LL)
        && (1LL - (long long )lk1) + (long long )lk2 >= 0LL) && (1LL - (long long
        )lk1) + (long long )lk3 >= 0LL) && (1LL - (long long )lk1) + (long long )lk4
        >= 0LL) && (1LL - (long long )lk1) + (long long )lk5 >= 0LL) && (1LL - (long
        long )lk1) + (long long )lk6 >= 0LL) && (1LL - (long long )lk1) + (long long
        )lk7 >= 0LL) && (1LL - (long long )lk1) + (long long )lk8 >= 0LL) && (1LL
        - (long long )lk2) + (long long )lk3 >= 0LL) && (1LL - (long long )lk2) +
        (long long )lk4 >= 0LL) && (1LL - (long long )lk2) + (long long )lk5 >= 0LL)
        && (1LL - (long long )lk2) + (long long )lk6 >= 0LL) && (1LL - (long long
        )lk2) + (long long )lk7 >= 0LL) && (1LL - (long long )lk2) + (long long )lk8
        >= 0LL) && (1LL - (long long )lk3) + (long long )lk4 >= 0LL) && (1LL - (long
        long )lk3) + (long long )lk5 >= 0LL) && (1LL - (long long )lk3) + (long long
        )lk6 >= 0LL) && (1LL - (long long )lk3) + (long long )lk7 >= 0LL) && (1LL
        - (long long )lk3) + (long long )lk8 >= 0LL) && (1LL - (long long )lk4) +
        (long long )lk5 >= 0LL) && (1LL - (long long )lk4) + (long long )lk6 >= 0LL)
        && (1LL - (long long )lk4) + (long long )lk7 >= 0LL) && (1LL - (long long
        )lk4) + (long long )lk8 >= 0LL) && (1LL - (long long )lk5) + (long long )lk6
        >= 0LL) && (1LL - (long long )lk5) + (long long )lk7 >= 0LL) && (1LL - (long
        long )lk5) + (long long )lk8 >= 0LL) && (1LL - (long long )lk6) + (long long
        )lk7 >= 0LL) && (1LL - (long long )lk6) + (long long )lk8 >= 0LL) && (1LL
        - (long long )lk7) + (long long )lk8 >= 0LL) && (2147483648LL - (long long
        )lk1) + (long long )p1 >= 0LL) && (2147483648LL - (long long )lk2) + (long
        long )p2 >= 0LL) && (2147483648LL - (long long )lk3) + (long long )p3 >= 0LL)
        && (2147483648LL - (long long )lk4) + (long long )p4 >= 0LL) && (2147483648LL
        - (long long )lk5) + (long long )p5 >= 0LL) && (2147483648LL - (long long
        )lk6) + (long long )p6 >= 0LL) && (2147483648LL - (long long )lk7) + (long
        long )p7 >= 0LL) && (2147483648LL - (long long )lk8) + (long long )p8 >= 0LL)
        && (2147483649LL - (long long )lk1) + (long long )p2 >= 0LL) && (2147483649LL
        - (long long )lk1) + (long long )p3 >= 0LL) && (2147483649LL - (long long
        )lk1) + (long long )p4 >= 0LL) && (2147483649LL - (long long )lk1) + (long
        long )p5 >= 0LL) && (2147483649LL - (long long )lk1) + (long long )p6 >= 0LL)
        && (2147483649LL - (long long )lk1) + (long long )p7 >= 0LL) && (2147483649LL
        - (long long )lk1) + (long long )p8 >= 0LL) && (2147483649LL - (long long
        )lk2) + (long long )p1 >= 0LL) && (2147483649LL - (long long )lk2) + (long
        long )p3 >= 0LL) && (2147483649LL - (long long )lk2) + (long long )p4 >= 0LL)
        && (2147483649LL - (long long )lk2) + (long long )p5 >= 0LL) && (2147483649LL
        - (long long )lk2) + (long long )p6 >= 0LL) && (2147483649LL - (long long
        )lk2) + (long long )p7 >= 0LL) && (2147483649LL - (long long )lk2) + (long
        long )p8 >= 0LL) && (2147483649LL - (long long )lk3) + (long long )p1 >= 0LL)
        && (2147483649LL - (long long )lk3) + (long long )p2 >= 0LL) && (2147483649LL
        - (long long )lk3) + (long long )p4 >= 0LL) && (2147483649LL - (long long
        )lk3) + (long long )p5 >= 0LL) && (2147483649LL - (long long )lk3) + (long
        long )p6 >= 0LL) && (2147483649LL - (long long )lk3) + (long long )p7 >= 0LL)
        && (2147483649LL - (long long )lk3) + (long long )p8 >= 0LL) && (2147483649LL
        - (long long )lk4) + (long long )p1 >= 0LL) && (2147483649LL - (long long
        )lk4) + (long long )p2 >= 0LL) && (2147483649LL - (long long )lk4) + (long
        long )p3 >= 0LL) && (2147483649LL - (long long )lk4) + (long long )p5 >= 0LL)
        && (2147483649LL - (long long )lk4) + (long long )p6 >= 0LL) && (2147483649LL
        - (long long )lk4) + (long long )p7 >= 0LL) && (2147483649LL - (long long
        )lk4) + (long long )p8 >= 0LL) && (2147483649LL - (long long )lk5) + (long
        long )p1 >= 0LL) && (2147483649LL - (long long )lk5) + (long long )p2 >= 0LL)
        && (2147483649LL - (long long )lk5) + (long long )p3 >= 0LL) && (2147483649LL
        - (long long )lk5) + (long long )p4 >= 0LL) && (2147483649LL - (long long
        )lk5) + (long long )p6 >= 0LL) && (2147483649LL - (long long )lk5) + (long
        long )p7 >= 0LL) && (2147483649LL - (long long )lk5) + (long long )p8 >= 0LL)
        && (2147483649LL - (long long )lk6) + (long long )p1 >= 0LL) && (2147483649LL
        - (long long )lk6) + (long long )p2 >= 0LL) && (2147483649LL - (long long
        )lk6) + (long long )p3 >= 0LL) && (2147483649LL - (long long )lk6) + (long
        long )p4 >= 0LL) && (2147483649LL - (long long )lk6) + (long long )p5 >= 0LL)
        && (2147483649LL - (long long )lk6) + (long long )p7 >= 0LL) && (2147483649LL
        - (long long )lk6) + (long long )p8 >= 0LL) && (2147483649LL - (long long
        )lk7) + (long long )p1 >= 0LL) && (2147483649LL - (long long )lk7) + (long
        long )p2 >= 0LL) && (2147483649LL - (long long )lk7) + (long long )p3 >= 0LL)
        && (2147483649LL - (long long )lk7) + (long long )p4 >= 0LL) && (2147483649LL
        - (long long )lk7) + (long long )p5 >= 0LL) && (2147483649LL - (long long
        )lk7) + (long long )p6 >= 0LL) && (2147483649LL - (long long )lk7) + (long
        long )p8 >= 0LL) && (2147483649LL - (long long )lk8) + (long long )p1 >= 0LL)
        && (2147483649LL - (long long )lk8) + (long long )p2 >= 0LL) && (2147483649LL
        - (long long )lk8) + (long long )p3 >= 0LL) && (2147483649LL - (long long
        )lk8) + (long long )p4 >= 0LL) && (2147483649LL - (long long )lk8) + (long
        long )p5 >= 0LL) && (2147483649LL - (long long )lk8) + (long long )p6 >= 0LL)
        && (2147483649LL - (long long )lk8) + (long long )p7 >= 0LL) && (long long
        )lk1 + (long long )lk2 >= 0LL) && (long long )lk1 + (long long )lk3 >= 0LL)
        && (long long )lk1 + (long long )lk4 >= 0LL) && (long long )lk1 + (long long
        )lk5 >= 0LL) && (long long )lk1 + (long long )lk6 >= 0LL) && (long long )lk1
        + (long long )lk7 >= 0LL) && (long long )lk1 + (long long )lk8 >= 0LL) &&
        (long long )lk2 + (long long )lk3 >= 0LL) && (long long )lk2 + (long long
        )lk4 >= 0LL) && (long long )lk2 + (long long )lk5 >= 0LL) && (long long )lk2
        + (long long )lk6 >= 0LL) && (long long )lk2 + (long long )lk7 >= 0LL) &&
        (long long )lk2 + (long long )lk8 >= 0LL) && (long long )lk3 + (long long
        )lk4 >= 0LL) && (long long )lk3 + (long long )lk5 >= 0LL) && (long long )lk3
        + (long long )lk6 >= 0LL) && (long long )lk3 + (long long )lk7 >= 0LL) &&
        (long long )lk3 + (long long )lk8 >= 0LL) && (long long )lk4 + (long long
        )lk5 >= 0LL) && (long long )lk4 + (long long )lk6 >= 0LL) && (long long )lk4
        + (long long )lk7 >= 0LL) && (long long )lk4 + (long long )lk8 >= 0LL) &&
        (long long )lk5 + (long long )lk6 >= 0LL) && (long long )lk5 + (long long
        )lk7 >= 0LL) && (long long )lk5 + (long long )lk8 >= 0LL) && (long long )lk6
        + (long long )lk7 >= 0LL) && (long long )lk6 + (long long )lk8 >= 0LL) &&
        (long long )lk7 + (long long )lk8 >= 0LL) && (1LL + (long long )lk1) - (long
        long )lk2 >= 0LL) && (1LL + (long long )lk1) - (long long )lk3 >= 0LL) &&
        (1LL + (long long )lk1) - (long long )lk4 >= 0LL) && (1LL + (long long )lk1)
        - (long long )lk5 >= 0LL) && (1LL + (long long )lk1) - (long long )lk6 >=
        0LL) && (1LL + (long long )lk1) - (long long )lk7 >= 0LL) && (1LL + (long
        long )lk1) - (long long )lk8 >= 0LL) && (1LL + (long long )lk2) - (long long
        )lk3 >= 0LL) && (1LL + (long long )lk2) - (long long )lk4 >= 0LL) && (1LL
        + (long long )lk2) - (long long )lk5 >= 0LL) && (1LL + (long long )lk2) -
        (long long )lk6 >= 0LL) && (1LL + (long long )lk2) - (long long )lk7 >= 0LL)
        && (1LL + (long long )lk2) - (long long )lk8 >= 0LL) && (1LL + (long long
        )lk3) - (long long )lk4 >= 0LL) && (1LL + (long long )lk3) - (long long )lk5
        >= 0LL) && (1LL + (long long )lk3) - (long long )lk6 >= 0LL) && (1LL + (long
        long )lk3) - (long long )lk7 >= 0LL) && (1LL + (long long )lk3) - (long long
        )lk8 >= 0LL) && (1LL + (long long )lk4) - (long long )lk5 >= 0LL) && (1LL
        + (long long )lk4) - (long long )lk6 >= 0LL) && (1LL + (long long )lk4) -
        (long long )lk7 >= 0LL) && (1LL + (long long )lk4) - (long long )lk8 >= 0LL)
        && (1LL + (long long )lk5) - (long long )lk6 >= 0LL) && (1LL + (long long
        )lk5) - (long long )lk7 >= 0LL) && (1LL + (long long )lk5) - (long long )lk8
        >= 0LL) && (1LL + (long long )lk6) - (long long )lk7 >= 0LL) && (1LL + (long
        long )lk6) - (long long )lk8 >= 0LL) && (1LL + (long long )lk7) - (long long
        )lk8 >= 0LL) && (2147483647LL + (long long )lk1) - (long long )p1 >= 0LL)
        && (2147483647LL + (long long )lk1) - (long long )p2 >= 0LL) && (2147483647LL
        + (long long )lk1) - (long long )p3 >= 0LL) && (2147483647LL + (long long
        )lk1) - (long long )p4 >= 0LL) && (2147483647LL + (long long )lk1) - (long
        long )p5 >= 0LL) && (2147483647LL + (long long )lk1) - (long long )p6 >= 0LL)
        && (2147483647LL + (long long )lk1) - (long long )p7 >= 0LL) && (2147483647LL
        + (long long )lk1) - (long long )p8 >= 0LL) && (2147483647LL + (long long
        )lk2) - (long long )p1 >= 0LL) && (2147483647LL + (long long )lk2) - (long
        long )p2 >= 0LL) && (2147483647LL + (long long )lk2) - (long long )p3 >= 0LL)
        && (2147483647LL + (long long )lk2) - (long long )p4 >= 0LL) && (2147483647LL
        + (long long )lk2) - (long long )p5 >= 0LL) && (2147483647LL + (long long
        )lk2) - (long long )p6 >= 0LL) && (2147483647LL + (long long )lk2) - (long
        long )p7 >= 0LL) && (2147483647LL + (long long )lk2) - (long long )p8 >= 0LL)
        && (2147483647LL + (long long )lk3) - (long long )p1 >= 0LL) && (2147483647LL
        + (long long )lk3) - (long long )p2 >= 0LL) && (2147483647LL + (long long
        )lk3) - (long long )p3 >= 0LL) && (2147483647LL + (long long )lk3) - (long
        long )p4 >= 0LL) && (2147483647LL + (long long )lk3) - (long long )p5 >= 0LL)
        && (2147483647LL + (long long )lk3) - (long long )p6 >= 0LL) && (2147483647LL
        + (long long )lk3) - (long long )p7 >= 0LL) && (2147483647LL + (long long
        )lk3) - (long long )p8 >= 0LL) && (2147483647LL + (long long )lk4) - (long
        long )p1 >= 0LL) && (2147483647LL + (long long )lk4) - (long long )p2 >= 0LL)
        && (2147483647LL + (long long )lk4) - (long long )p3 >= 0LL) && (2147483647LL
        + (long long )lk4) - (long long )p4 >= 0LL) && (2147483647LL + (long long
        )lk4) - (long long )p5 >= 0LL) && (2147483647LL + (long long )lk4) - (long
        long )p6 >= 0LL) && (2147483647LL + (long long )lk4) - (long long )p7 >= 0LL)
        && (2147483647LL + (long long )lk4) - (long long )p8 >= 0LL) && (2147483647LL
        + (long long )lk5) - (long long )p1 >= 0LL) && (2147483647LL + (long long
        )lk5) - (long long )p2 >= 0LL) && (2147483647LL + (long long )lk5) - (long
        long )p3 >= 0LL) && (2147483647LL + (long long )lk5) - (long long )p4 >= 0LL)
        && (2147483647LL + (long long )lk5) - (long long )p5 >= 0LL) && (2147483647LL
        + (long long )lk5) - (long long )p6 >= 0LL) && (2147483647LL + (long long
        )lk5) - (long long )p7 >= 0LL) && (2147483647LL + (long long )lk5) - (long
        long )p8 >= 0LL) && (2147483647LL + (long long )lk6) - (long long )p1 >= 0LL)
        && (2147483647LL + (long long )lk6) - (long long )p2 >= 0LL) && (2147483647LL
        + (long long )lk6) - (long long )p3 >= 0LL) && (2147483647LL + (long long
        )lk6) - (long long )p4 >= 0LL) && (2147483647LL + (long long )lk6) - (long
        long )p5 >= 0LL) && (2147483647LL + (long long )lk6) - (long long )p6 >= 0LL)
        && (2147483647LL + (long long )lk6) - (long long )p7 >= 0LL) && (2147483647LL
        + (long long )lk6) - (long long )p8 >= 0LL) && (2147483647LL + (long long
        )lk7) - (long long )p1 >= 0LL) && (2147483647LL + (long long )lk7) - (long
        long )p2 >= 0LL) && (2147483647LL + (long long )lk7) - (long long )p3 >= 0LL)
        && (2147483647LL + (long long )lk7) - (long long )p4 >= 0LL) && (2147483647LL
        + (long long )lk7) - (long long )p5 >= 0LL) && (2147483647LL + (long long
        )lk7) - (long long )p6 >= 0LL) && (2147483647LL + (long long )lk7) - (long
        long )p7 >= 0LL) && (2147483647LL + (long long )lk7) - (long long )p8 >= 0LL)
        && (2147483647LL + (long long )lk8) - (long long )p1 >= 0LL) && (2147483647LL
        + (long long )lk8) - (long long )p2 >= 0LL) && (2147483647LL + (long long
        )lk8) - (long long )p3 >= 0LL) && (2147483647LL + (long long )lk8) - (long
        long )p4 >= 0LL) && (2147483647LL + (long long )lk8) - (long long )p5 >= 0LL)
        && (2147483647LL + (long long )lk8) - (long long )p6 >= 0LL) && (2147483647LL
        + (long long )lk8) - (long long )p7 >= 0LL) && (2147483647LL + (long long
        )lk8) - (long long )p8 >= 0LL) && (2LL - (long long )lk1) - (long long )lk2
        >= 0LL) && (2LL - (long long )lk1) - (long long )lk3 >= 0LL) && (2LL - (long
        long )lk1) - (long long )lk4 >= 0LL) && (2LL - (long long )lk1) - (long long
        )lk5 >= 0LL) && (2LL - (long long )lk1) - (long long )lk6 >= 0LL) && (2LL
        - (long long )lk1) - (long long )lk7 >= 0LL) && (2LL - (long long )lk1) -
        (long long )lk8 >= 0LL) && (2LL - (long long )lk2) - (long long )lk3 >= 0LL)
        && (2LL - (long long )lk2) - (long long )lk4 >= 0LL) && (2LL - (long long
        )lk2) - (long long )lk5 >= 0LL) && (2LL - (long long )lk2) - (long long )lk6
        >= 0LL) && (2LL - (long long )lk2) - (long long )lk7 >= 0LL) && (2LL - (long
        long )lk2) - (long long )lk8 >= 0LL) && (2LL - (long long )lk3) - (long long
        )lk4 >= 0LL) && (2LL - (long long )lk3) - (long long )lk5 >= 0LL) && (2LL
        - (long long )lk3) - (long long )lk6 >= 0LL) && (2LL - (long long )lk3) -
        (long long )lk7 >= 0LL) && (2LL - (long long )lk3) - (long long )lk8 >= 0LL)
        && (2LL - (long long )lk4) - (long long )lk5 >= 0LL) && (2LL - (long long
        )lk4) - (long long )lk6 >= 0LL) && (2LL - (long long )lk4) - (long long )lk7
        >= 0LL) && (2LL - (long long )lk4) - (long long )lk8 >= 0LL) && (2LL - (long
        long )lk5) - (long long )lk6 >= 0LL) && (2LL - (long long )lk5) - (long long
        )lk7 >= 0LL) && (2LL - (long long )lk5) - (long long )lk8 >= 0LL) && (2LL
        - (long long )lk6) - (long long )lk7 >= 0LL) && (2LL - (long long )lk6) -
        (long long )lk8 >= 0LL) && (2LL - (long long )lk7) - (long long )lk8 >= 0LL)
        && (2147483647LL - (long long )lk1) - (long long )p1 >= 0LL) && (2147483647LL
        - (long long )lk2) - (long long )p2 >= 0LL) && (2147483647LL - (long long
        )lk3) - (long long )p3 >= 0LL) && (2147483647LL - (long long )lk4) - (long
        long )p4 >= 0LL) && (2147483647LL - (long long )lk5) - (long long )p5 >= 0LL)
        && (2147483647LL - (long long )lk6) - (long long )p6 >= 0LL) && (2147483647LL
        - (long long )lk7) - (long long )p7 >= 0LL) && (2147483647LL - (long long
        )lk8) - (long long )p8 >= 0LL) && (2147483648LL - (long long )lk1) - (long
        long )p2 >= 0LL) && (2147483648LL - (long long )lk1) - (long long )p3 >= 0LL)
        && (2147483648LL - (long long )lk1) - (long long )p4 >= 0LL) && (2147483648LL
        - (long long )lk1) - (long long )p5 >= 0LL) && (2147483648LL - (long long
        )lk1) - (long long )p6 >= 0LL) && (2147483648LL - (long long )lk1) - (long
        long )p7 >= 0LL) && (2147483648LL - (long long )lk1) - (long long )p8 >= 0LL)
        && (2147483648LL - (long long )lk2) - (long long )p1 >= 0LL) && (2147483648LL
        - (long long )lk2) - (long long )p3 >= 0LL) && (2147483648LL - (long long
        )lk2) - (long long )p4 >= 0LL) && (2147483648LL - (long long )lk2) - (long
        long )p5 >= 0LL) && (2147483648LL - (long long )lk2) - (long long )p6 >= 0LL)
        && (2147483648LL - (long long )lk2) - (long long )p7 >= 0LL) && (2147483648LL
        - (long long )lk2) - (long long )p8 >= 0LL) && (2147483648LL - (long long
        )lk3) - (long long )p1 >= 0LL) && (2147483648LL - (long long )lk3) - (long
        long )p2 >= 0LL) && (2147483648LL - (long long )lk3) - (long long )p4 >= 0LL)
        && (2147483648LL - (long long )lk3) - (long long )p5 >= 0LL) && (2147483648LL
        - (long long )lk3) - (long long )p6 >= 0LL) && (2147483648LL - (long long
        )lk3) - (long long )p7 >= 0LL) && (2147483648LL - (long long )lk3) - (long
        long )p8 >= 0LL) && (2147483648LL - (long long )lk4) - (long long )p1 >= 0LL)
        && (2147483648LL - (long long )lk4) - (long long )p2 >= 0LL) && (2147483648LL
        - (long long )lk4) - (long long )p3 >= 0LL) && (2147483648LL - (long long
        )lk4) - (long long )p5 >= 0LL) && (2147483648LL - (long long )lk4) - (long
        long )p6 >= 0LL) && (2147483648LL - (long long )lk4) - (long long )p7 >= 0LL)
        && (2147483648LL - (long long )lk4) - (long long )p8 >= 0LL) && (2147483648LL
        - (long long )lk5) - (long long )p1 >= 0LL) && (2147483648LL - (long long
        )lk5) - (long long )p2 >= 0LL) && (2147483648LL - (long long )lk5) - (long
        long )p3 >= 0LL) && (2147483648LL - (long long )lk5) - (long long )p4 >= 0LL)
        && (2147483648LL - (long long )lk5) - (long long )p6 >= 0LL) && (2147483648LL
        - (long long )lk5) - (long long )p7 >= 0LL) && (2147483648LL - (long long
        )lk5) - (long long )p8 >= 0LL) && (2147483648LL - (long long )lk6) - (long
        long )p1 >= 0LL) && (2147483648LL - (long long )lk6) - (long long )p2 >= 0LL)
        && (2147483648LL - (long long )lk6) - (long long )p3 >= 0LL) && (2147483648LL
        - (long long )lk6) - (long long )p4 >= 0LL) && (2147483648LL - (long long
        )lk6) - (long long )p5 >= 0LL) && (2147483648LL - (long long )lk6) - (long
        long )p7 >= 0LL) && (2147483648LL - (long long )lk6) - (long long )p8 >= 0LL)
        && (2147483648LL - (long long )lk7) - (long long )p1 >= 0LL) && (2147483648LL
        - (long long )lk7) - (long long )p2 >= 0LL) && (2147483648LL - (long long
        )lk7) - (long long )p3 >= 0LL) && (2147483648LL - (long long )lk7) - (long
        long )p4 >= 0LL) && (2147483648LL - (long long )lk7) - (long long )p5 >= 0LL)
        && (2147483648LL - (long long )lk7) - (long long )p6 >= 0LL) && (2147483648LL
        - (long long )lk7) - (long long )p8 >= 0LL) && (2147483648LL - (long long
        )lk8) - (long long )p1 >= 0LL) && (2147483648LL - (long long )lk8) - (long
        long )p2 >= 0LL) && (2147483648LL - (long long )lk8) - (long long )p3 >= 0LL)
        && (2147483648LL - (long long )lk8) - (long long )p4 >= 0LL) && (2147483648LL
        - (long long )lk8) - (long long )p5 >= 0LL) && (2147483648LL - (long long
        )lk8) - (long long )p6 >= 0LL) && (2147483648LL - (long long )lk8) - (long
        long )p7 >= 0LL) && (lk1 == 0 || lk1 == 1)) && (lk2 == 0 || lk2 == 1)) &&
        (lk3 == 0 || lk3 == 1)) && (lk4 == 0 || lk4 == 1)) && (lk5 == 0 || lk5 ==
        1)) && (lk6 == 0 || lk6 == 1)) && (lk7 == 0 || lk7 == 1)) && (lk8 == 0 ||
        lk8 == 1))
      format: c_expression
