/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint --conf conf/svcomp-yaml-validate.json --enable dbg.timing.enabled --set 'ana.activated[+]' apron --set ana.apron.domain polyhedra --witness.yaml.unassume korn/in-de61.yml.witness.yml --witness.yaml.validate korn/in-de61.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/in-de61.c


--------------------------------------------------------------------------------


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] unassume invariant: (((((((((((((((((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && y >= 5U) || (((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! (n >= x))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && n >= x) && ! (x >= 2U))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && n >= x) && x >= 2U) && ! (y >= 5U))) && n == x) && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && y >= 2U)) || (((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! (n >= x))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && n >= x) && ! (n >= 3U))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && n >= x) && n >= 3U) && ! (x >= 2U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && (((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! (n >= 3U))) || (((n == x && z == 0U) && n >= 3U) && ! (y >= 2U)))) && n - z == 1U) && x == 1U) && y - z == 1U) && (long long )n <= 4294967295LL) && n >= 5U)) || ((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! (n >= x))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && n >= x) && ! (n >= 3U))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && n >= x) && n >= 3U) && ! (x >= 2U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && (((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! (n >= 3U))) || (((n == x && z == 0U) && n >= 3U) && ! (y >= 2U)))) && ((! (n - z == 1U) || (n - z == 1U && ! (x == 1U))) || ((n - z == 1U && x == 1U) && ! (y - z == 1U)))) && n == z) && x == 0U) && y == z) && (long long )n <= 4294967295LL) && n >= 5U)) || (((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && ((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && ((((! (n - z == 1U) || (n - z == 1U && ! (x == 1U))) || ((n - z == 1U && x == 1U) && ! (y - z == 1U))) || (((n - z == 1U && x == 1U) && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || ((((n - z == 1U && x == 1U) && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((((! (n == z) || (n == z && ! (x == 0U))) || ((n == z && x == 0U) && ! (y == z))) || (((n == z && x == 0U) && y == z) && ! ((long long )n <= 4294967295LL))) || ((((n == z && x == 0U) && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && n == 4U) && x == 3U) && y == 4U) && z == 1U)) || ((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && ((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && ((((! (n - z == 1U) || (n - z == 1U && ! (x == 1U))) || ((n - z == 1U && x == 1U) && ! (y - z == 1U))) || (((n - z == 1U && x == 1U) && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || ((((n - z == 1U && x == 1U) && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((((! (n == z) || (n == z && ! (x == 0U))) || ((n == z && x == 0U) && ! (y == z))) || (((n == z && x == 0U) && y == z) && ! ((long long )n <= 4294967295LL))) || ((((n == z && x == 0U) && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (! (x == 3U) || (x == 3U && ! (z == 1U)))) && n == 4U) && x == 2U) && y == 4U) && z == 2U)) || (((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && ((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && (((! (n - z == 1U) || (n - z == 1U && ! (y - z == 1U))) || ((n - z == 1U && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || (((n - z == 1U && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((((! (n == z) || (n == z && ! (x == 0U))) || ((n == z && x == 0U) && ! (y == z))) || (((n == z && x == 0U) && y == z) && ! ((long long )n <= 4294967295LL))) || ((((n == z && x == 0U) && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (! (x == 3U) || (x == 3U && ! (z == 1U)))) && (! (x == 2U) || (x == 2U && ! (z == 2U)))) && n == 4U) && x == 1U) && y == 4U) && z == 3U)) || ((((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && ((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && ((((! (n - z == 1U) || (n - z == 1U && ! (x == 1U))) || ((n - z == 1U && x == 1U) && ! (y - z == 1U))) || (((n - z == 1U && x == 1U) && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || ((((n - z == 1U && x == 1U) && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == z) || (n == z && ! (y == z))) || ((n == z && y == z) && ! ((long long )n <= 4294967295LL))) || (((n == z && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (! (x == 3U) || (x == 3U && ! (z == 1U)))) && (! (x == 2U) || (x == 2U && ! (z == 2U)))) && (! (x == 1U) || (x == 1U && ! (z == 3U)))) && n == 4U) && x == 0U) && y == 4U) && z == 4U)) || (((((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && ((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && ((((! (n - z == 1U) || (n - z == 1U && ! (x == 1U))) || ((n - z == 1U && x == 1U) && ! (y - z == 1U))) || (((n - z == 1U && x == 1U) && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || ((((n - z == 1U && x == 1U) && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((((! (n == z) || (n == z && ! (x == 0U))) || ((n == z && x == 0U) && ! (y == z))) || (((n == z && x == 0U) && y == z) && ! ((long long )n <= 4294967295LL))) || ((((n == z && x == 0U) && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((! (n == 4U) || (n == 4U && ! (x == 3U))) || ((n == 4U && x == 3U) && ! (y == 4U)))) && ((! (n == 4U) || (n == 4U && ! (y == 4U))) || ((n == 4U && y == 4U) && ! (z == 2U)))) && (((! (n == 4U) || (n == 4U && ! (x == 1U))) || ((n == 4U && x == 1U) && ! (y == 4U))) || (((n == 4U && x == 1U) && y == 4U) && ! (z == 3U)))) && (((! (n == 4U) || (n == 4U && ! (x == 0U))) || ((n == 4U && x == 0U) && ! (y == 4U))) || (((n == 4U && x == 0U) && y == 4U) && ! (z == 4U)))) && n == 3U) && x == 2U) && y == 3U) && z == 1U)) || ((((((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && ((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && (((! (n - z == 1U) || (n - z == 1U && ! (y - z == 1U))) || ((n - z == 1U && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || (((n - z == 1U && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((((! (n == z) || (n == z && ! (x == 0U))) || ((n == z && x == 0U) && ! (y == z))) || (((n == z && x == 0U) && y == z) && ! ((long long )n <= 4294967295LL))) || ((((n == z && x == 0U) && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == 4U) || (n == 4U && ! (x == 3U))) || ((n == 4U && x == 3U) && ! (y == 4U))) || (((n == 4U && x == 3U) && y == 4U) && ! (z == 1U)))) && ((! (n == 4U) || (n == 4U && ! (x == 2U))) || ((n == 4U && x == 2U) && ! (y == 4U)))) && ((! (n == 4U) || (n == 4U && ! (y == 4U))) || ((n == 4U && y == 4U) && ! (z == 3U)))) && (((! (n == 4U) || (n == 4U && ! (x == 0U))) || ((n == 4U && x == 0U) && ! (y == 4U))) || (((n == 4U && x == 0U) && y == 4U) && ! (z == 4U)))) && (! (x == 2U) || (x == 2U && ! (z == 1U)))) && n == 3U) && x == 1U) && y == 3U) && z == 2U)) || (((((((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && ((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && ((((! (n - z == 1U) || (n - z == 1U && ! (x == 1U))) || ((n - z == 1U && x == 1U) && ! (y - z == 1U))) || (((n - z == 1U && x == 1U) && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || ((((n - z == 1U && x == 1U) && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == z) || (n == z && ! (y == z))) || ((n == z && y == z) && ! ((long long )n <= 4294967295LL))) || (((n == z && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == 4U) || (n == 4U && ! (x == 3U))) || ((n == 4U && x == 3U) && ! (y == 4U))) || (((n == 4U && x == 3U) && y == 4U) && ! (z == 1U)))) && (((! (n == 4U) || (n == 4U && ! (x == 2U))) || ((n == 4U && x == 2U) && ! (y == 4U))) || (((n == 4U && x == 2U) && y == 4U) && ! (z == 2U)))) && ((! (n == 4U) || (n == 4U && ! (x == 1U))) || ((n == 4U && x == 1U) && ! (y == 4U)))) && ((! (n == 4U) || (n == 4U && ! (y == 4U))) || ((n == 4U && y == 4U) && ! (z == 4U)))) && (! (x == 2U) || (x == 2U && ! (z == 1U)))) && (! (x == 1U) || (x == 1U && ! (z == 2U)))) && n == 3U) && x == 0U) && y == 3U) && z == 3U)) || ((((((((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && (((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && ((((! (n - z == 1U) || (n - z == 1U && ! (x == 1U))) || ((n - z == 1U && x == 1U) && ! (y - z == 1U))) || (((n - z == 1U && x == 1U) && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || ((((n - z == 1U && x == 1U) && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((((! (n == z) || (n == z && ! (x == 0U))) || ((n == z && x == 0U) && ! (y == z))) || (((n == z && x == 0U) && y == z) && ! ((long long )n <= 4294967295LL))) || ((((n == z && x == 0U) && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == 4U) || (n == 4U && ! (x == 3U))) || ((n == 4U && x == 3U) && ! (y == 4U))) || (((n == 4U && x == 3U) && y == 4U) && ! (z == 1U)))) && ((! (n == 4U) || (n == 4U && ! (y == 4U))) || ((n == 4U && y == 4U) && ! (z == 2U)))) && (((! (n == 4U) || (n == 4U && ! (x == 1U))) || ((n == 4U && x == 1U) && ! (y == 4U))) || (((n == 4U && x == 1U) && y == 4U) && ! (z == 3U)))) && (((! (n == 4U) || (n == 4U && ! (x == 0U))) || ((n == 4U && x == 0U) && ! (y == 4U))) || (((n == 4U && x == 0U) && y == 4U) && ! (z == 4U)))) && ((! (n == 3U) || (n == 3U && ! (y == 3U))) || ((n == 3U && y == 3U) && ! (z == 1U)))) && (((! (n == 3U) || (n == 3U && ! (x == 1U))) || ((n == 3U && x == 1U) && ! (y == 3U))) || (((n == 3U && x == 1U) && y == 3U) && ! (z == 2U)))) && (((! (n == 3U) || (n == 3U && ! (x == 0U))) || ((n == 3U && x == 0U) && ! (y == 3U))) || (((n == 3U && x == 0U) && y == 3U) && ! (z == 3U)))) && n == 2U) && x == 2U) && y == 2U) && z == 0U)) || (((((((((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && ((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && (((! (n - z == 1U) || (n - z == 1U && ! (y - z == 1U))) || ((n - z == 1U && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || (((n - z == 1U && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((((! (n == z) || (n == z && ! (x == 0U))) || ((n == z && x == 0U) && ! (y == z))) || (((n == z && x == 0U) && y == z) && ! ((long long )n <= 4294967295LL))) || ((((n == z && x == 0U) && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((! (n == 4U) || (n == 4U && ! (x == 3U))) || ((n == 4U && x == 3U) && ! (y == 4U)))) && (((! (n == 4U) || (n == 4U && ! (x == 2U))) || ((n == 4U && x == 2U) && ! (y == 4U))) || (((n == 4U && x == 2U) && y == 4U) && ! (z == 2U)))) && ((! (n == 4U) || (n == 4U && ! (y == 4U))) || ((n == 4U && y == 4U) && ! (z == 3U)))) && (((! (n == 4U) || (n == 4U && ! (x == 0U))) || ((n == 4U && x == 0U) && ! (y == 4U))) || (((n == 4U && x == 0U) && y == 4U) && ! (z == 4U)))) && ((! (n == 3U) || (n == 3U && ! (x == 2U))) || ((n == 3U && x == 2U) && ! (y == 3U)))) && ((! (n == 3U) || (n == 3U && ! (y == 3U))) || ((n == 3U && y == 3U) && ! (z == 2U)))) && (((! (n == 3U) || (n == 3U && ! (x == 0U))) || ((n == 3U && x == 0U) && ! (y == 3U))) || (((n == 3U && x == 0U) && y == 3U) && ! (z == 3U)))) && (! (x == 2U) || (x == 2U && ! (z == 0U)))) && n == 2U) && x == 1U) && y == 2U) && z == 1U)) || ((((((((((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && ((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && ((((! (n - z == 1U) || (n - z == 1U && ! (x == 1U))) || ((n - z == 1U && x == 1U) && ! (y - z == 1U))) || (((n - z == 1U && x == 1U) && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || ((((n - z == 1U && x == 1U) && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == z) || (n == z && ! (y == z))) || ((n == z && y == z) && ! ((long long )n <= 4294967295LL))) || (((n == z && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == 4U) || (n == 4U && ! (x == 3U))) || ((n == 4U && x == 3U) && ! (y == 4U))) || (((n == 4U && x == 3U) && y == 4U) && ! (z == 1U)))) && ((! (n == 4U) || (n == 4U && ! (x == 2U))) || ((n == 4U && x == 2U) && ! (y == 4U)))) && (((! (n == 4U) || (n == 4U && ! (x == 1U))) || ((n == 4U && x == 1U) && ! (y == 4U))) || (((n == 4U && x == 1U) && y == 4U) && ! (z == 3U)))) && ((! (n == 4U) || (n == 4U && ! (y == 4U))) || ((n == 4U && y == 4U) && ! (z == 4U)))) && (((! (n == 3U) || (n == 3U && ! (x == 2U))) || ((n == 3U && x == 2U) && ! (y == 3U))) || (((n == 3U && x == 2U) && y == 3U) && ! (z == 1U)))) && ((! (n == 3U) || (n == 3U && ! (x == 1U))) || ((n == 3U && x == 1U) && ! (y == 3U)))) && ((! (n == 3U) || (n == 3U && ! (y == 3U))) || ((n == 3U && y == 3U) && ! (z == 3U)))) && (! (x == 2U) || (x == 2U && ! (z == 0U)))) && (! (x == 1U) || (x == 1U && ! (z == 1U)))) && n == 2U) && x == 0U) && y == 2U) && z == 2U)) || (((((((((((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && (((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && (((! (n - z == 1U) || (n - z == 1U && ! (y - z == 1U))) || ((n - z == 1U && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || (((n - z == 1U && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((((! (n == z) || (n == z && ! (x == 0U))) || ((n == z && x == 0U) && ! (y == z))) || (((n == z && x == 0U) && y == z) && ! ((long long )n <= 4294967295LL))) || ((((n == z && x == 0U) && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == 4U) || (n == 4U && ! (x == 3U))) || ((n == 4U && x == 3U) && ! (y == 4U))) || (((n == 4U && x == 3U) && y == 4U) && ! (z == 1U)))) && (((! (n == 4U) || (n == 4U && ! (x == 2U))) || ((n == 4U && x == 2U) && ! (y == 4U))) || (((n == 4U && x == 2U) && y == 4U) && ! (z == 2U)))) && ((! (n == 4U) || (n == 4U && ! (y == 4U))) || ((n == 4U && y == 4U) && ! (z == 3U)))) && (((! (n == 4U) || (n == 4U && ! (x == 0U))) || ((n == 4U && x == 0U) && ! (y == 4U))) || (((n == 4U && x == 0U) && y == 4U) && ! (z == 4U)))) && (((! (n == 3U) || (n == 3U && ! (x == 2U))) || ((n == 3U && x == 2U) && ! (y == 3U))) || (((n == 3U && x == 2U) && y == 3U) && ! (z == 1U)))) && ((! (n == 3U) || (n == 3U && ! (y == 3U))) || ((n == 3U && y == 3U) && ! (z == 2U)))) && (((! (n == 3U) || (n == 3U && ! (x == 0U))) || ((n == 3U && x == 0U) && ! (y == 3U))) || (((n == 3U && x == 0U) && y == 3U) && ! (z == 3U)))) && ((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (y == 2U)))) && ((! (n == 2U) || (n == 2U && ! (y == 2U))) || ((n == 2U && y == 2U) && ! (z == 1U)))) && (((! (n == 2U) || (n == 2U && ! (x == 0U))) || ((n == 2U && x == 0U) && ! (y == 2U))) || (((n == 2U && x == 0U) && y == 2U) && ! (z == 2U)))) && n == 1U) && x == 1U) && y == 1U) && z == 0U)) || ((((((((((((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && ((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && ((((! (n - z == 1U) || (n - z == 1U && ! (x == 1U))) || ((n - z == 1U && x == 1U) && ! (y - z == 1U))) || (((n - z == 1U && x == 1U) && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || ((((n - z == 1U && x == 1U) && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == z) || (n == z && ! (y == z))) || ((n == z && y == z) && ! ((long long )n <= 4294967295LL))) || (((n == z && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((! (n == 4U) || (n == 4U && ! (x == 3U))) || ((n == 4U && x == 3U) && ! (y == 4U)))) && (((! (n == 4U) || (n == 4U && ! (x == 2U))) || ((n == 4U && x == 2U) && ! (y == 4U))) || (((n == 4U && x == 2U) && y == 4U) && ! (z == 2U)))) && (((! (n == 4U) || (n == 4U && ! (x == 1U))) || ((n == 4U && x == 1U) && ! (y == 4U))) || (((n == 4U && x == 1U) && y == 4U) && ! (z == 3U)))) && ((! (n == 4U) || (n == 4U && ! (y == 4U))) || ((n == 4U && y == 4U) && ! (z == 4U)))) && ((! (n == 3U) || (n == 3U && ! (x == 2U))) || ((n == 3U && x == 2U) && ! (y == 3U)))) && (((! (n == 3U) || (n == 3U && ! (x == 1U))) || ((n == 3U && x == 1U) && ! (y == 3U))) || (((n == 3U && x == 1U) && y == 3U) && ! (z == 2U)))) && ((! (n == 3U) || (n == 3U && ! (y == 3U))) || ((n == 3U && y == 3U) && ! (z == 3U)))) && (((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (y == 2U))) || (((n == 2U && x == 2U) && y == 2U) && ! (z == 0U)))) && ((! (n == 2U) || (n == 2U && ! (x == 1U))) || ((n == 2U && x == 1U) && ! (y == 2U)))) && ((! (n == 2U) || (n == 2U && ! (y == 2U))) || ((n == 2U && y == 2U) && ! (z == 2U)))) && (! (x == 1U) || (x == 1U && ! (z == 0U)))) && n == 1U) && x == 0U) && y == 1U) && z == 1U)) || (((((((((((((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && (((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && ((((! (n - z == 1U) || (n - z == 1U && ! (x == 1U))) || ((n - z == 1U && x == 1U) && ! (y - z == 1U))) || (((n - z == 1U && x == 1U) && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || ((((n - z == 1U && x == 1U) && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == z) || (n == z && ! (y == z))) || ((n == z && y == z) && ! ((long long )n <= 4294967295LL))) || (((n == z && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == 4U) || (n == 4U && ! (x == 3U))) || ((n == 4U && x == 3U) && ! (y == 4U))) || (((n == 4U && x == 3U) && y == 4U) && ! (z == 1U)))) && (((! (n == 4U) || (n == 4U && ! (x == 2U))) || ((n == 4U && x == 2U) && ! (y == 4U))) || (((n == 4U && x == 2U) && y == 4U) && ! (z == 2U)))) && (((! (n == 4U) || (n == 4U && ! (x == 1U))) || ((n == 4U && x == 1U) && ! (y == 4U))) || (((n == 4U && x == 1U) && y == 4U) && ! (z == 3U)))) && ((! (n == 4U) || (n == 4U && ! (y == 4U))) || ((n == 4U && y == 4U) && ! (z == 4U)))) && (((! (n == 3U) || (n == 3U && ! (x == 2U))) || ((n == 3U && x == 2U) && ! (y == 3U))) || (((n == 3U && x == 2U) && y == 3U) && ! (z == 1U)))) && (((! (n == 3U) || (n == 3U && ! (x == 1U))) || ((n == 3U && x == 1U) && ! (y == 3U))) || (((n == 3U && x == 1U) && y == 3U) && ! (z == 2U)))) && ((! (n == 3U) || (n == 3U && ! (y == 3U))) || ((n == 3U && y == 3U) && ! (z == 3U)))) && ((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (y == 2U)))) && (((! (n == 2U) || (n == 2U && ! (x == 1U))) || ((n == 2U && x == 1U) && ! (y == 2U))) || (((n == 2U && x == 1U) && y == 2U) && ! (z == 1U)))) && ((! (n == 2U) || (n == 2U && ! (y == 2U))) || ((n == 2U && y == 2U) && ! (z == 2U)))) && ((! (n == 1U) || (n == 1U && ! (x == 1U))) || ((n == 1U && x == 1U) && ! (y == 1U)))) && ((! (n == 1U) || (n == 1U && ! (y == 1U))) || ((n == 1U && y == 1U) && ! (z == 1U)))) && n == 0U) && x == 0U) && y == 0U) && z == 0U) (../plain/in-de61.c:23:9-23:12)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/in-de61.c:32:5-32:8)
[Info][Witness] unassume invariant: (((((((((((((((((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && y >= 5U) || (((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! (n >= x))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && n >= x) && ! (x >= 2U))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && n >= x) && x >= 2U) && ! (y >= 5U))) && n == x) && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && y >= 2U)) || (((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! (n >= x))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && n >= x) && ! (n >= 3U))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && n >= x) && n >= 3U) && ! (x >= 2U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && (((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! (n >= 3U))) || (((n == x && z == 0U) && n >= 3U) && ! (y >= 2U)))) && n - z == 1U) && x == 1U) && y - z == 1U) && (long long )n <= 4294967295LL) && n >= 5U)) || ((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! (n >= x))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && n >= x) && ! (n >= 3U))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && n >= x) && n >= 3U) && ! (x >= 2U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && (((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! (n >= 3U))) || (((n == x && z == 0U) && n >= 3U) && ! (y >= 2U)))) && ((! (n - z == 1U) || (n - z == 1U && ! (x == 1U))) || ((n - z == 1U && x == 1U) && ! (y - z == 1U)))) && n == z) && x == 0U) && y == z) && (long long )n <= 4294967295LL) && n >= 5U)) || (((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && ((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && ((((! (n - z == 1U) || (n - z == 1U && ! (x == 1U))) || ((n - z == 1U && x == 1U) && ! (y - z == 1U))) || (((n - z == 1U && x == 1U) && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || ((((n - z == 1U && x == 1U) && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((((! (n == z) || (n == z && ! (x == 0U))) || ((n == z && x == 0U) && ! (y == z))) || (((n == z && x == 0U) && y == z) && ! ((long long )n <= 4294967295LL))) || ((((n == z && x == 0U) && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && n == 4U) && x == 3U) && y == 4U) && z == 1U)) || ((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && ((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && ((((! (n - z == 1U) || (n - z == 1U && ! (x == 1U))) || ((n - z == 1U && x == 1U) && ! (y - z == 1U))) || (((n - z == 1U && x == 1U) && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || ((((n - z == 1U && x == 1U) && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((((! (n == z) || (n == z && ! (x == 0U))) || ((n == z && x == 0U) && ! (y == z))) || (((n == z && x == 0U) && y == z) && ! ((long long )n <= 4294967295LL))) || ((((n == z && x == 0U) && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (! (x == 3U) || (x == 3U && ! (z == 1U)))) && n == 4U) && x == 2U) && y == 4U) && z == 2U)) || (((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && ((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && (((! (n - z == 1U) || (n - z == 1U && ! (y - z == 1U))) || ((n - z == 1U && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || (((n - z == 1U && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((((! (n == z) || (n == z && ! (x == 0U))) || ((n == z && x == 0U) && ! (y == z))) || (((n == z && x == 0U) && y == z) && ! ((long long )n <= 4294967295LL))) || ((((n == z && x == 0U) && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (! (x == 3U) || (x == 3U && ! (z == 1U)))) && (! (x == 2U) || (x == 2U && ! (z == 2U)))) && n == 4U) && x == 1U) && y == 4U) && z == 3U)) || ((((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && ((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && ((((! (n - z == 1U) || (n - z == 1U && ! (x == 1U))) || ((n - z == 1U && x == 1U) && ! (y - z == 1U))) || (((n - z == 1U && x == 1U) && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || ((((n - z == 1U && x == 1U) && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == z) || (n == z && ! (y == z))) || ((n == z && y == z) && ! ((long long )n <= 4294967295LL))) || (((n == z && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (! (x == 3U) || (x == 3U && ! (z == 1U)))) && (! (x == 2U) || (x == 2U && ! (z == 2U)))) && (! (x == 1U) || (x == 1U && ! (z == 3U)))) && n == 4U) && x == 0U) && y == 4U) && z == 4U)) || (((((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && ((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && ((((! (n - z == 1U) || (n - z == 1U && ! (x == 1U))) || ((n - z == 1U && x == 1U) && ! (y - z == 1U))) || (((n - z == 1U && x == 1U) && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || ((((n - z == 1U && x == 1U) && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((((! (n == z) || (n == z && ! (x == 0U))) || ((n == z && x == 0U) && ! (y == z))) || (((n == z && x == 0U) && y == z) && ! ((long long )n <= 4294967295LL))) || ((((n == z && x == 0U) && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((! (n == 4U) || (n == 4U && ! (x == 3U))) || ((n == 4U && x == 3U) && ! (y == 4U)))) && ((! (n == 4U) || (n == 4U && ! (y == 4U))) || ((n == 4U && y == 4U) && ! (z == 2U)))) && (((! (n == 4U) || (n == 4U && ! (x == 1U))) || ((n == 4U && x == 1U) && ! (y == 4U))) || (((n == 4U && x == 1U) && y == 4U) && ! (z == 3U)))) && (((! (n == 4U) || (n == 4U && ! (x == 0U))) || ((n == 4U && x == 0U) && ! (y == 4U))) || (((n == 4U && x == 0U) && y == 4U) && ! (z == 4U)))) && n == 3U) && x == 2U) && y == 3U) && z == 1U)) || ((((((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && ((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && (((! (n - z == 1U) || (n - z == 1U && ! (y - z == 1U))) || ((n - z == 1U && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || (((n - z == 1U && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((((! (n == z) || (n == z && ! (x == 0U))) || ((n == z && x == 0U) && ! (y == z))) || (((n == z && x == 0U) && y == z) && ! ((long long )n <= 4294967295LL))) || ((((n == z && x == 0U) && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == 4U) || (n == 4U && ! (x == 3U))) || ((n == 4U && x == 3U) && ! (y == 4U))) || (((n == 4U && x == 3U) && y == 4U) && ! (z == 1U)))) && ((! (n == 4U) || (n == 4U && ! (x == 2U))) || ((n == 4U && x == 2U) && ! (y == 4U)))) && ((! (n == 4U) || (n == 4U && ! (y == 4U))) || ((n == 4U && y == 4U) && ! (z == 3U)))) && (((! (n == 4U) || (n == 4U && ! (x == 0U))) || ((n == 4U && x == 0U) && ! (y == 4U))) || (((n == 4U && x == 0U) && y == 4U) && ! (z == 4U)))) && (! (x == 2U) || (x == 2U && ! (z == 1U)))) && n == 3U) && x == 1U) && y == 3U) && z == 2U)) || (((((((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && ((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && ((((! (n - z == 1U) || (n - z == 1U && ! (x == 1U))) || ((n - z == 1U && x == 1U) && ! (y - z == 1U))) || (((n - z == 1U && x == 1U) && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || ((((n - z == 1U && x == 1U) && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == z) || (n == z && ! (y == z))) || ((n == z && y == z) && ! ((long long )n <= 4294967295LL))) || (((n == z && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == 4U) || (n == 4U && ! (x == 3U))) || ((n == 4U && x == 3U) && ! (y == 4U))) || (((n == 4U && x == 3U) && y == 4U) && ! (z == 1U)))) && (((! (n == 4U) || (n == 4U && ! (x == 2U))) || ((n == 4U && x == 2U) && ! (y == 4U))) || (((n == 4U && x == 2U) && y == 4U) && ! (z == 2U)))) && ((! (n == 4U) || (n == 4U && ! (x == 1U))) || ((n == 4U && x == 1U) && ! (y == 4U)))) && ((! (n == 4U) || (n == 4U && ! (y == 4U))) || ((n == 4U && y == 4U) && ! (z == 4U)))) && (! (x == 2U) || (x == 2U && ! (z == 1U)))) && (! (x == 1U) || (x == 1U && ! (z == 2U)))) && n == 3U) && x == 0U) && y == 3U) && z == 3U)) || ((((((((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && (((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && ((((! (n - z == 1U) || (n - z == 1U && ! (x == 1U))) || ((n - z == 1U && x == 1U) && ! (y - z == 1U))) || (((n - z == 1U && x == 1U) && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || ((((n - z == 1U && x == 1U) && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((((! (n == z) || (n == z && ! (x == 0U))) || ((n == z && x == 0U) && ! (y == z))) || (((n == z && x == 0U) && y == z) && ! ((long long )n <= 4294967295LL))) || ((((n == z && x == 0U) && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == 4U) || (n == 4U && ! (x == 3U))) || ((n == 4U && x == 3U) && ! (y == 4U))) || (((n == 4U && x == 3U) && y == 4U) && ! (z == 1U)))) && ((! (n == 4U) || (n == 4U && ! (y == 4U))) || ((n == 4U && y == 4U) && ! (z == 2U)))) && (((! (n == 4U) || (n == 4U && ! (x == 1U))) || ((n == 4U && x == 1U) && ! (y == 4U))) || (((n == 4U && x == 1U) && y == 4U) && ! (z == 3U)))) && (((! (n == 4U) || (n == 4U && ! (x == 0U))) || ((n == 4U && x == 0U) && ! (y == 4U))) || (((n == 4U && x == 0U) && y == 4U) && ! (z == 4U)))) && ((! (n == 3U) || (n == 3U && ! (y == 3U))) || ((n == 3U && y == 3U) && ! (z == 1U)))) && (((! (n == 3U) || (n == 3U && ! (x == 1U))) || ((n == 3U && x == 1U) && ! (y == 3U))) || (((n == 3U && x == 1U) && y == 3U) && ! (z == 2U)))) && (((! (n == 3U) || (n == 3U && ! (x == 0U))) || ((n == 3U && x == 0U) && ! (y == 3U))) || (((n == 3U && x == 0U) && y == 3U) && ! (z == 3U)))) && n == 2U) && x == 2U) && y == 2U) && z == 0U)) || (((((((((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && ((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && (((! (n - z == 1U) || (n - z == 1U && ! (y - z == 1U))) || ((n - z == 1U && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || (((n - z == 1U && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((((! (n == z) || (n == z && ! (x == 0U))) || ((n == z && x == 0U) && ! (y == z))) || (((n == z && x == 0U) && y == z) && ! ((long long )n <= 4294967295LL))) || ((((n == z && x == 0U) && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((! (n == 4U) || (n == 4U && ! (x == 3U))) || ((n == 4U && x == 3U) && ! (y == 4U)))) && (((! (n == 4U) || (n == 4U && ! (x == 2U))) || ((n == 4U && x == 2U) && ! (y == 4U))) || (((n == 4U && x == 2U) && y == 4U) && ! (z == 2U)))) && ((! (n == 4U) || (n == 4U && ! (y == 4U))) || ((n == 4U && y == 4U) && ! (z == 3U)))) && (((! (n == 4U) || (n == 4U && ! (x == 0U))) || ((n == 4U && x == 0U) && ! (y == 4U))) || (((n == 4U && x == 0U) && y == 4U) && ! (z == 4U)))) && ((! (n == 3U) || (n == 3U && ! (x == 2U))) || ((n == 3U && x == 2U) && ! (y == 3U)))) && ((! (n == 3U) || (n == 3U && ! (y == 3U))) || ((n == 3U && y == 3U) && ! (z == 2U)))) && (((! (n == 3U) || (n == 3U && ! (x == 0U))) || ((n == 3U && x == 0U) && ! (y == 3U))) || (((n == 3U && x == 0U) && y == 3U) && ! (z == 3U)))) && (! (x == 2U) || (x == 2U && ! (z == 0U)))) && n == 2U) && x == 1U) && y == 2U) && z == 1U)) || ((((((((((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && ((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && ((((! (n - z == 1U) || (n - z == 1U && ! (x == 1U))) || ((n - z == 1U && x == 1U) && ! (y - z == 1U))) || (((n - z == 1U && x == 1U) && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || ((((n - z == 1U && x == 1U) && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == z) || (n == z && ! (y == z))) || ((n == z && y == z) && ! ((long long )n <= 4294967295LL))) || (((n == z && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == 4U) || (n == 4U && ! (x == 3U))) || ((n == 4U && x == 3U) && ! (y == 4U))) || (((n == 4U && x == 3U) && y == 4U) && ! (z == 1U)))) && ((! (n == 4U) || (n == 4U && ! (x == 2U))) || ((n == 4U && x == 2U) && ! (y == 4U)))) && (((! (n == 4U) || (n == 4U && ! (x == 1U))) || ((n == 4U && x == 1U) && ! (y == 4U))) || (((n == 4U && x == 1U) && y == 4U) && ! (z == 3U)))) && ((! (n == 4U) || (n == 4U && ! (y == 4U))) || ((n == 4U && y == 4U) && ! (z == 4U)))) && (((! (n == 3U) || (n == 3U && ! (x == 2U))) || ((n == 3U && x == 2U) && ! (y == 3U))) || (((n == 3U && x == 2U) && y == 3U) && ! (z == 1U)))) && ((! (n == 3U) || (n == 3U && ! (x == 1U))) || ((n == 3U && x == 1U) && ! (y == 3U)))) && ((! (n == 3U) || (n == 3U && ! (y == 3U))) || ((n == 3U && y == 3U) && ! (z == 3U)))) && (! (x == 2U) || (x == 2U && ! (z == 0U)))) && (! (x == 1U) || (x == 1U && ! (z == 1U)))) && n == 2U) && x == 0U) && y == 2U) && z == 2U)) || (((((((((((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && (((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && (((! (n - z == 1U) || (n - z == 1U && ! (y - z == 1U))) || ((n - z == 1U && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || (((n - z == 1U && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((((! (n == z) || (n == z && ! (x == 0U))) || ((n == z && x == 0U) && ! (y == z))) || (((n == z && x == 0U) && y == z) && ! ((long long )n <= 4294967295LL))) || ((((n == z && x == 0U) && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == 4U) || (n == 4U && ! (x == 3U))) || ((n == 4U && x == 3U) && ! (y == 4U))) || (((n == 4U && x == 3U) && y == 4U) && ! (z == 1U)))) && (((! (n == 4U) || (n == 4U && ! (x == 2U))) || ((n == 4U && x == 2U) && ! (y == 4U))) || (((n == 4U && x == 2U) && y == 4U) && ! (z == 2U)))) && ((! (n == 4U) || (n == 4U && ! (y == 4U))) || ((n == 4U && y == 4U) && ! (z == 3U)))) && (((! (n == 4U) || (n == 4U && ! (x == 0U))) || ((n == 4U && x == 0U) && ! (y == 4U))) || (((n == 4U && x == 0U) && y == 4U) && ! (z == 4U)))) && (((! (n == 3U) || (n == 3U && ! (x == 2U))) || ((n == 3U && x == 2U) && ! (y == 3U))) || (((n == 3U && x == 2U) && y == 3U) && ! (z == 1U)))) && ((! (n == 3U) || (n == 3U && ! (y == 3U))) || ((n == 3U && y == 3U) && ! (z == 2U)))) && (((! (n == 3U) || (n == 3U && ! (x == 0U))) || ((n == 3U && x == 0U) && ! (y == 3U))) || (((n == 3U && x == 0U) && y == 3U) && ! (z == 3U)))) && ((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (y == 2U)))) && ((! (n == 2U) || (n == 2U && ! (y == 2U))) || ((n == 2U && y == 2U) && ! (z == 1U)))) && (((! (n == 2U) || (n == 2U && ! (x == 0U))) || ((n == 2U && x == 0U) && ! (y == 2U))) || (((n == 2U && x == 0U) && y == 2U) && ! (z == 2U)))) && n == 1U) && x == 1U) && y == 1U) && z == 0U)) || ((((((((((((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && ((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && ((((! (n - z == 1U) || (n - z == 1U && ! (x == 1U))) || ((n - z == 1U && x == 1U) && ! (y - z == 1U))) || (((n - z == 1U && x == 1U) && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || ((((n - z == 1U && x == 1U) && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == z) || (n == z && ! (y == z))) || ((n == z && y == z) && ! ((long long )n <= 4294967295LL))) || (((n == z && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && ((! (n == 4U) || (n == 4U && ! (x == 3U))) || ((n == 4U && x == 3U) && ! (y == 4U)))) && (((! (n == 4U) || (n == 4U && ! (x == 2U))) || ((n == 4U && x == 2U) && ! (y == 4U))) || (((n == 4U && x == 2U) && y == 4U) && ! (z == 2U)))) && (((! (n == 4U) || (n == 4U && ! (x == 1U))) || ((n == 4U && x == 1U) && ! (y == 4U))) || (((n == 4U && x == 1U) && y == 4U) && ! (z == 3U)))) && ((! (n == 4U) || (n == 4U && ! (y == 4U))) || ((n == 4U && y == 4U) && ! (z == 4U)))) && ((! (n == 3U) || (n == 3U && ! (x == 2U))) || ((n == 3U && x == 2U) && ! (y == 3U)))) && (((! (n == 3U) || (n == 3U && ! (x == 1U))) || ((n == 3U && x == 1U) && ! (y == 3U))) || (((n == 3U && x == 1U) && y == 3U) && ! (z == 2U)))) && ((! (n == 3U) || (n == 3U && ! (y == 3U))) || ((n == 3U && y == 3U) && ! (z == 3U)))) && (((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (y == 2U))) || (((n == 2U && x == 2U) && y == 2U) && ! (z == 0U)))) && ((! (n == 2U) || (n == 2U && ! (x == 1U))) || ((n == 2U && x == 1U) && ! (y == 2U)))) && ((! (n == 2U) || (n == 2U && ! (y == 2U))) || ((n == 2U && y == 2U) && ! (z == 2U)))) && (! (x == 1U) || (x == 1U && ! (z == 0U)))) && n == 1U) && x == 0U) && y == 1U) && z == 1U)) || (((((((((((((((((((((((((! (n + (4294967295U * x - z) == 0U) || (n + (4294967295U * x - z) == 0U && ! ((x + y) - n >= 1U))) || ((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && ! ((long long )n <= 4294967295LL))) || (((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && ! (n >= x))) || ((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && ! (n >= 3U))) || (((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && ! (x >= 2U))) || ((((((n + (4294967295U * x - z) == 0U && (x + y) - n >= 1U) && (long long )n <= 4294967295LL) && n >= x) && n >= 3U) && x >= 2U) && ! (y >= 5U))) && (((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U)))) && ((((! (n - z == 1U) || (n - z == 1U && ! (x == 1U))) || ((n - z == 1U && x == 1U) && ! (y - z == 1U))) || (((n - z == 1U && x == 1U) && y - z == 1U) && ! ((long long )n <= 4294967295LL))) || ((((n - z == 1U && x == 1U) && y - z == 1U) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == z) || (n == z && ! (y == z))) || ((n == z && y == z) && ! ((long long )n <= 4294967295LL))) || (((n == z && y == z) && (long long )n <= 4294967295LL) && ! (n >= 5U)))) && (((! (n == 4U) || (n == 4U && ! (x == 3U))) || ((n == 4U && x == 3U) && ! (y == 4U))) || (((n == 4U && x == 3U) && y == 4U) && ! (z == 1U)))) && (((! (n == 4U) || (n == 4U && ! (x == 2U))) || ((n == 4U && x == 2U) && ! (y == 4U))) || (((n == 4U && x == 2U) && y == 4U) && ! (z == 2U)))) && (((! (n == 4U) || (n == 4U && ! (x == 1U))) || ((n == 4U && x == 1U) && ! (y == 4U))) || (((n == 4U && x == 1U) && y == 4U) && ! (z == 3U)))) && ((! (n == 4U) || (n == 4U && ! (y == 4U))) || ((n == 4U && y == 4U) && ! (z == 4U)))) && (((! (n == 3U) || (n == 3U && ! (x == 2U))) || ((n == 3U && x == 2U) && ! (y == 3U))) || (((n == 3U && x == 2U) && y == 3U) && ! (z == 1U)))) && (((! (n == 3U) || (n == 3U && ! (x == 1U))) || ((n == 3U && x == 1U) && ! (y == 3U))) || (((n == 3U && x == 1U) && y == 3U) && ! (z == 2U)))) && ((! (n == 3U) || (n == 3U && ! (y == 3U))) || ((n == 3U && y == 3U) && ! (z == 3U)))) && ((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (y == 2U)))) && (((! (n == 2U) || (n == 2U && ! (x == 1U))) || ((n == 2U && x == 1U) && ! (y == 2U))) || (((n == 2U && x == 1U) && y == 2U) && ! (z == 1U)))) && ((! (n == 2U) || (n == 2U && ! (y == 2U))) || ((n == 2U && y == 2U) && ! (z == 2U)))) && ((! (n == 1U) || (n == 1U && ! (x == 1U))) || ((n == 1U && x == 1U) && ! (y == 1U)))) && ((! (n == 1U) || (n == 1U && ! (y == 1U))) || ((n == 1U && y == 1U) && ! (z == 1U)))) && n == 0U) && x == 0U) && y == 0U) && z == 0U) (../plain/in-de61.c:32:5-32:8)
[Info][Witness] unassume invariant: ((((((((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && y >= 2U) || (((((((! (z == 0U) || (z == 0U && ! (y >= 2U))) && n == x) && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && y >= 0U) && z >= 1U)) || ((((((((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U))) && (((((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y + z >= 2U))) || ((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && ! (y >= 0U))) || (((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && y >= 0U) && ! (z >= 1U)))) && n == 2U) && x == 2U) && y == 2U) && z == 0U)) || ((((((((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U))) && (((((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y + z >= 2U))) || ((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && ! (y >= 0U))) || (((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && y >= 0U) && ! (z >= 1U)))) && (! (y == 2U) || (y == 2U && ! (z == 0U)))) && n == 2U) && x == 2U) && y == 1U) && z == 1U)) || (((((((((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U))) && (((((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y + z >= 2U))) || ((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && ! (y >= 0U))) || (((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && y >= 0U) && ! (z >= 1U)))) && (! (y == 2U) || (y == 2U && ! (z == 0U)))) && (! (y == 1U) || (y == 1U && ! (z == 1U)))) && n == 2U) && x == 2U) && y == 0U) && z >= 2U)) || (((((((((((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U))) && (((((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y + z >= 2U))) || ((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && ! (y >= 0U))) || (((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && y >= 0U) && ! (z >= 1U)))) && ((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (y == 2U)))) && ((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (z == 1U)))) && (((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (y == 0U))) || (((n == 2U && x == 2U) && y == 0U) && ! (z >= 2U)))) && n == 1U) && x == 1U) && y == 1U) && z == 0U)) || (((((((((((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U))) && (((((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y + z >= 2U))) || ((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && ! (y >= 0U))) || (((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && y >= 0U) && ! (z >= 1U)))) && (((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (y == 2U))) || (((n == 2U && x == 2U) && y == 2U) && ! (z == 0U)))) && ((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (y == 1U)))) && ((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (z >= 2U)))) && (! (y == 1U) || (y == 1U && ! (z == 0U)))) && n == 1U) && x == 1U) && y == 0U) && z == 1U)) || (((((((((((((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U))) && (((((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y + z >= 2U))) || ((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && ! (y >= 0U))) || (((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && y >= 0U) && ! (z >= 1U)))) && ((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (y == 2U)))) && (((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (y == 1U))) || (((n == 2U && x == 2U) && y == 1U) && ! (z == 1U)))) && ((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (z >= 2U)))) && ((! (n == 1U) || (n == 1U && ! (x == 1U))) || ((n == 1U && x == 1U) && ! (y == 1U)))) && ((! (n == 1U) || (n == 1U && ! (x == 1U))) || ((n == 1U && x == 1U) && ! (z == 1U)))) && n == 0U) && x == 0U) && y == 0U) && z == 0U) (../plain/in-de61.c:29:9-29:12)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/in-de61.c:38:5-38:8)
[Info][Witness] unassume invariant: ((((((((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && y >= 2U) || (((((((! (z == 0U) || (z == 0U && ! (y >= 2U))) && n == x) && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && y >= 0U) && z >= 1U)) || ((((((((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U))) && (((((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y + z >= 2U))) || ((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && ! (y >= 0U))) || (((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && y >= 0U) && ! (z >= 1U)))) && n == 2U) && x == 2U) && y == 2U) && z == 0U)) || ((((((((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U))) && (((((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y + z >= 2U))) || ((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && ! (y >= 0U))) || (((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && y >= 0U) && ! (z >= 1U)))) && (! (y == 2U) || (y == 2U && ! (z == 0U)))) && n == 2U) && x == 2U) && y == 1U) && z == 1U)) || (((((((((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U))) && (((((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y + z >= 2U))) || ((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && ! (y >= 0U))) || (((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && y >= 0U) && ! (z >= 1U)))) && (! (y == 2U) || (y == 2U && ! (z == 0U)))) && (! (y == 1U) || (y == 1U && ! (z == 1U)))) && n == 2U) && x == 2U) && y == 0U) && z >= 2U)) || (((((((((((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U))) && (((((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y + z >= 2U))) || ((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && ! (y >= 0U))) || (((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && y >= 0U) && ! (z >= 1U)))) && ((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (y == 2U)))) && ((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (z == 1U)))) && (((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (y == 0U))) || (((n == 2U && x == 2U) && y == 0U) && ! (z >= 2U)))) && n == 1U) && x == 1U) && y == 1U) && z == 0U)) || (((((((((((((! (n == x) || (n == x && ! (z == 0U))) || ((n == x && z == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && z == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && z == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U))) && (((((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y + z >= 2U))) || ((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && ! (y >= 0U))) || (((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && y >= 0U) && ! (z >= 1U)))) && (((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (y == 2U))) || (((n == 2U && x == 2U) && y == 2U) && ! (z == 0U)))) && ((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (y == 1U)))) && ((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (z >= 2U)))) && (! (y == 1U) || (y == 1U && ! (z == 0U)))) && n == 1U) && x == 1U) && y == 0U) && z == 1U)) || (((((((((((((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y >= 2U))) && (((((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (y + z >= 2U))) || ((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && ! (y >= 0U))) || (((((n == x && (long long )n <= 4294967295LL) && n >= 3U) && y + z >= 2U) && y >= 0U) && ! (z >= 1U)))) && ((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (y == 2U)))) && (((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (y == 1U))) || (((n == 2U && x == 2U) && y == 1U) && ! (z == 1U)))) && ((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (z >= 2U)))) && ((! (n == 1U) || (n == 1U && ! (x == 1U))) || ((n == 1U && x == 1U) && ! (y == 1U)))) && ((! (n == 1U) || (n == 1U && ! (x == 1U))) || ((n == 1U && x == 1U) && ! (z == 1U)))) && n == 0U) && x == 0U) && y == 0U) && z == 0U) (../plain/in-de61.c:38:5-38:8)
[Info][Witness] unassume invariant: (((((((((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && n >= 2U) && x >= 0U) && z >= 2U) || ((((((((! (n + (4294967295U * x - y) == 0U) || (n + (4294967295U * x - y) == 0U && ! (n - x >= 1U))) || ((n + (4294967295U * x - y) == 0U && n - x >= 1U) && ! (n >= 2U))) || (((n + (4294967295U * x - y) == 0U && n - x >= 1U) && n >= 2U) && ! (x >= 0U))) && n == x) && y == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && z >= 2U)) || (((((((((! (n + (4294967295U * x - y) == 0U) || (n + (4294967295U * x - y) == 0U && ! ((long long )n <= 4294967295LL))) || ((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && ! (n - x >= 1U))) || (((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && ! (n >= 2U))) || ((((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && n >= 2U) && ! (x >= 0U))) && ((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U)))) && n == 2U) && x == 2U) && y == 0U) && z >= 2U)) || (((((((((((! (n + (4294967295U * x - y) == 0U) || (n + (4294967295U * x - y) == 0U && ! ((long long )n <= 4294967295LL))) || ((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && ! (n - x >= 1U))) || (((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && ! (n >= 2U))) || ((((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && n >= 2U) && ! (x >= 0U))) || (((((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && n >= 2U) && x >= 0U) && ! (z >= 2U))) && (((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (z >= 2U)))) && ((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (z >= 2U)))) && n == 1U) && x == 1U) && y == 0U) && z == 1U)) || ((((((((((((! (n + (4294967295U * x - y) == 0U) || (n + (4294967295U * x - y) == 0U && ! ((long long )n <= 4294967295LL))) || ((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && ! (n - x >= 1U))) || (((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && ! (n >= 2U))) || ((((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && n >= 2U) && ! (x >= 0U))) || (((((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && n >= 2U) && x >= 0U) && ! (z >= 2U))) && ((((! (n == x) || (n == x && ! (y == 0U))) || ((n == x && y == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && y == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && y == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (z >= 2U)))) && (((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (y == 0U))) || (((n == 2U && x == 2U) && y == 0U) && ! (z >= 2U)))) && (! (x == 1U) || (x == 1U && ! (y == 0U)))) && n == 1U) && x == 0U) && y == 1U) && z == 1U)) || (((((((((((((! (n + (4294967295U * x - y) == 0U) || (n + (4294967295U * x - y) == 0U && ! ((long long )n <= 4294967295LL))) || ((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && ! (n - x >= 1U))) || (((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && ! (n >= 2U))) || ((((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && n >= 2U) && ! (x >= 0U))) || (((((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && n >= 2U) && x >= 0U) && ! (z >= 2U))) && (((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (z >= 2U)))) && ((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (z >= 2U)))) && ((! (n == 1U) || (n == 1U && ! (x == 1U))) || ((n == 1U && x == 1U) && ! (z == 1U)))) && ((! (n == 1U) || (n == 1U && ! (y == 1U))) || ((n == 1U && y == 1U) && ! (z == 1U)))) && n == 0U) && x == 0U) && y == 0U) && z >= 0U) (../plain/in-de61.c:35:9-35:12)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/in-de61.c:43:5-43:8)
[Info][Witness] unassume invariant: (((((((((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && n >= 2U) && x >= 0U) && z >= 2U) || ((((((((! (n + (4294967295U * x - y) == 0U) || (n + (4294967295U * x - y) == 0U && ! (n - x >= 1U))) || ((n + (4294967295U * x - y) == 0U && n - x >= 1U) && ! (n >= 2U))) || (((n + (4294967295U * x - y) == 0U && n - x >= 1U) && n >= 2U) && ! (x >= 0U))) && n == x) && y == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && z >= 2U)) || (((((((((! (n + (4294967295U * x - y) == 0U) || (n + (4294967295U * x - y) == 0U && ! ((long long )n <= 4294967295LL))) || ((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && ! (n - x >= 1U))) || (((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && ! (n >= 2U))) || ((((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && n >= 2U) && ! (x >= 0U))) && ((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U)))) && n == 2U) && x == 2U) && y == 0U) && z >= 2U)) || (((((((((((! (n + (4294967295U * x - y) == 0U) || (n + (4294967295U * x - y) == 0U && ! ((long long )n <= 4294967295LL))) || ((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && ! (n - x >= 1U))) || (((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && ! (n >= 2U))) || ((((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && n >= 2U) && ! (x >= 0U))) || (((((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && n >= 2U) && x >= 0U) && ! (z >= 2U))) && (((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (z >= 2U)))) && ((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (z >= 2U)))) && n == 1U) && x == 1U) && y == 0U) && z == 1U)) || ((((((((((((! (n + (4294967295U * x - y) == 0U) || (n + (4294967295U * x - y) == 0U && ! ((long long )n <= 4294967295LL))) || ((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && ! (n - x >= 1U))) || (((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && ! (n >= 2U))) || ((((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && n >= 2U) && ! (x >= 0U))) || (((((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && n >= 2U) && x >= 0U) && ! (z >= 2U))) && ((((! (n == x) || (n == x && ! (y == 0U))) || ((n == x && y == 0U) && ! ((long long )n <= 4294967295LL))) || (((n == x && y == 0U) && (long long )n <= 4294967295LL) && ! (n >= 3U))) || ((((n == x && y == 0U) && (long long )n <= 4294967295LL) && n >= 3U) && ! (z >= 2U)))) && (((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (y == 0U))) || (((n == 2U && x == 2U) && y == 0U) && ! (z >= 2U)))) && (! (x == 1U) || (x == 1U && ! (y == 0U)))) && n == 1U) && x == 0U) && y == 1U) && z == 1U)) || (((((((((((((! (n + (4294967295U * x - y) == 0U) || (n + (4294967295U * x - y) == 0U && ! ((long long )n <= 4294967295LL))) || ((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && ! (n - x >= 1U))) || (((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && ! (n >= 2U))) || ((((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && n >= 2U) && ! (x >= 0U))) || (((((n + (4294967295U * x - y) == 0U && (long long )n <= 4294967295LL) && n - x >= 1U) && n >= 2U) && x >= 0U) && ! (z >= 2U))) && (((! (n == x) || (n == x && ! ((long long )n <= 4294967295LL))) || ((n == x && (long long )n <= 4294967295LL) && ! (n >= 3U))) || (((n == x && (long long )n <= 4294967295LL) && n >= 3U) && ! (z >= 2U)))) && ((! (n == 2U) || (n == 2U && ! (x == 2U))) || ((n == 2U && x == 2U) && ! (z >= 2U)))) && ((! (n == 1U) || (n == 1U && ! (x == 1U))) || ((n == 1U && x == 1U) && ! (z == 1U)))) && ((! (n == 1U) || (n == 1U && ! (y == 1U))) || ((n == 1U && y == 1U) && ! (z == 1U)))) && n == 0U) && x == 0U) && y == 0U) && z >= 0U) (../plain/in-de61.c:44:5-44:8)
[Info][Witness] unassume invariant: (z >= 0U && x >= 0U) && ((((n == y && (long long )n <= 4294967295LL) && n >= 2U) || ((((! (n == y) || (n == y && ! ((long long )n <= 4294967295LL))) || ((n == y && (long long )n <= 4294967295LL) && ! (n >= 2U))) && n == 1U) && y == 1U)) || (((((! (n == y) || (n == y && ! ((long long )n <= 4294967295LL))) || ((n == y && (long long )n <= 4294967295LL) && ! (n >= 2U))) && (! (n == 1U) || (n == 1U && ! (y == 1U)))) && n == 0U) && y == 0U)) (../plain/in-de61.c:41:9-41:12)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/in-de61.c:50:5-50:8)
[Info][Witness] unassume invariant: (z >= 0U && x >= 0U) && ((((n == y && (long long )n <= 4294967295LL) && n >= 2U) || ((((! (n == y) || (n == y && ! ((long long )n <= 4294967295LL))) || ((n == y && (long long )n <= 4294967295LL) && ! (n >= 2U))) && n == 1U) && y == 1U)) || (((((! (n == y) || (n == y && ! ((long long )n <= 4294967295LL))) || ((n == y && (long long )n <= 4294967295LL) && ! (n >= 2U))) && (! (n == 1U) || (n == 1U && ! (y == 1U)))) && n == 0U) && y == 0U)) (../plain/in-de61.c:50:5-50:8)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 30
  dead: 0
  total lines: 30
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow
[Warning][Witness] invariant unconfirmed: (n == x && z == (0) && n <= (4294967295LL) && n >= (3) && y >= (2)) || ((!(z == (0)) || (z == (0) && !(y >= (2)))) && n == x && n <= (4294967295LL) && n >= (3) && (y + z) >= (2) && y >= (0) && z >= (1)) || ((!(n == x) || (n == x && !(n <= (4294967295LL))) || (n == x && n <= (4294967295LL) && !(n >= (3))) || (n == x && n <= (4294967295LL) && n >= (3) && !(y >= (2)))) && (!(n == x) || (n == x && !(n <= (4294967295LL))) || (n == x && n <= (4294967295LL) && !(n >= (3))) || (n == x && n <= (4294967295LL) && n >= (3) && !((y + z) >= (2))) || (n == x && n <= (4294967295LL) && n >= (3) && (y + z) >= (2) && !(y >= (0))) || (n == x && n <= (4294967295LL) && n >= (3) && (y + z) >= (2) && y >= (0) && !(z >= (1)))) && n == (2) && x == (2) && y == (2) && z == (0)) || ((!(n == x) || (n == x && !(z == (0))) || (n == x && z == (0) && !(n <= (4294967295LL))) || (n == x && z == (0) && n <= (4294967295LL) && !(n >= (3))) || (n == x && z == (0) && n <= (4294967295LL) && n >= (3) && !(y >= (2)))) && (!(n == x) || (n == x && !(n <= (4294967295LL))) || (n == x && n <= (4294967295LL) && !(n >= (3))) || (n == x && n <= (4294967295LL) && n >= (3) && !((y + z) >= (2))) || (n == x && n <= (4294967295LL) && n >= (3) && (y + z) >= (2) && !(y >= (0))) || (n == x && n <= (4294967295LL) && n >= (3) && (y + z) >= (2) && y >= (0) && !(z >= (1)))) && (!(y == (2)) || (y == (2) && !(z == (0)))) && n == (2) && x == (2) && y == (1) && z == (1)) || ((!(n == x) || (n == x && !(z == (0))) || (n == x && z == (0) && !(n <= (4294967295LL))) || (n == x && z == (0) && n <= (4294967295LL) && !(n >= (3))) || (n == x && z == (0) && n <= (4294967295LL) && n >= (3) && !(y >= (2)))) && (!(n == x) || (n == x && !(n <= (4294967295LL))) || (n == x && n <= (4294967295LL) && !(n >= (3))) || (n == x && n <= (4294967295LL) && n >= (3) && !((y + z) >= (2))) || (n == x && n <= (4294967295LL) && n >= (3) && (y + z) >= (2) && !(y >= (0))) || (n == x && n <= (4294967295LL) && n >= (3) && (y + z) >= (2) && y >= (0) && !(z >= (1)))) && (!(y == (2)) || (y == (2) && !(z == (0)))) && (!(y == (1)) || (y == (1) && !(z == (1)))) && n == (2) && x == (2) && y == (0) && z >= (2)) || ((!(n == x) || (n == x && !(n <= (4294967295LL))) || (n == x && n <= (4294967295LL) && !(n >= (3))) || (n == x && n <= (4294967295LL) && n >= (3) && !(y >= (2)))) && (!(n == x) || (n == x && !(n <= (4294967295LL))) || (n == x && n <= (4294967295LL) && !(n >= (3))) || (n == x && n <= (4294967295LL) && n >= (3) && !((y + z) >= (2))) || (n == x && n <= (4294967295LL) && n >= (3) && (y + z) >= (2) && !(y >= (0))) || (n == x && n <= (4294967295LL) && n >= (3) && (y + z) >= (2) && y >= (0) && !(z >= (1)))) && (!(n == (2)) || (n == (2) && !(x == (2))) || (n == (2) && x == (2) && !(y == (2)))) && (!(n == (2)) || (n == (2) && !(x == (2))) || (n == (2) && x == (2) && !(z == (1)))) && (!(n == (2)) || (n == (2) && !(x == (2))) || (n == (2) && x == (2) && !(y == (0))) || (n == (2) && x == (2) && y == (0) && !(z >= (2)))) && n == (1) && x == (1) && y == (1) && z == (0)) || ((!(n == x) || (n == x && !(z == (0))) || (n == x && z == (0) && !(n <= (4294967295LL))) || (n == x && z == (0) && n <= (4294967295LL) && !(n >= (3))) || (n == x && z == (0) && n <= (4294967295LL) && n >= (3) && !(y >= (2)))) && (!(n == x) || (n == x && !(n <= (4294967295LL))) || (n == x && n <= (4294967295LL) && !(n >= (3))) || (n == x && n <= (4294967295LL) && n >= (3) && !((y + z) >= (2))) || (n == x && n <= (4294967295LL) && n >= (3) && (y + z) >= (2) && !(y >= (0))) || (n == x && n <= (4294967295LL) && n >= (3) && (y + z) >= (2) && y >= (0) && !(z >= (1)))) && (!(n == (2)) || (n == (2) && !(x == (2))) || (n == (2) && x == (2) && !(y == (2))) || (n == (2) && x == (2) && y == (2) && !(z == (0)))) && (!(n == (2)) || (n == (2) && !(x == (2))) || (n == (2) && x == (2) && !(y == (1)))) && (!(n == (2)) || (n == (2) && !(x == (2))) || (n == (2) && x == (2) && !(z >= (2)))) && (!(y == (1)) || (y == (1) && !(z == (0)))) && n == (1) && x == (1) && y == (0) && z == (1)) || ((!(n == x) || (n == x && !(n <= (4294967295LL))) || (n == x && n <= (4294967295LL) && !(n >= (3))) || (n == x && n <= (4294967295LL) && n >= (3) && !(y >= (2)))) && (!(n == x) || (n == x && !(n <= (4294967295LL))) || (n == x && n <= (4294967295LL) && !(n >= (3))) || (n == x && n <= (4294967295LL) && n >= (3) && !((y + z) >= (2))) || (n == x && n <= (4294967295LL) && n >= (3) && (y + z) >= (2) && !(y >= (0))) || (n == x && n <= (4294967295LL) && n >= (3) && (y + z) >= (2) && y >= (0) && !(z >= (1)))) && (!(n == (2)) || (n == (2) && !(x == (2))) || (n == (2) && x == (2) && !(y == (2)))) && (!(n == (2)) || (n == (2) && !(x == (2))) || (n == (2) && x == (2) && !(y == (1))) || (n == (2) && x == (2) && y == (1) && !(z == (1)))) && (!(n == (2)) || (n == (2) && !(x == (2))) || (n == (2) && x == (2) && !(z >= (2)))) && (!(n == (1)) || (n == (1) && !(x == (1))) || (n == (1) && x == (1) && !(y == (1)))) && (!(n == (1)) || (n == (1) && !(x == (1))) || (n == (1) && x == (1) && !(z == (1)))) && n == (0) && x == (0) && y == (0) && z == (0)) (../plain/in-de61.c:35:3)
[Warning][Witness] invariant unconfirmed: z >= (0) && x >= (0) && ((n == y && n <= (4294967295LL) && n >= (2)) || ((!(n == y) || (n == y && !(n <= (4294967295LL))) || (n == y && n <= (4294967295LL) && !(n >= (2)))) && n == (1) && y == (1)) || ((!(n == y) || (n == y && !(n <= (4294967295LL))) || (n == y && n <= (4294967295LL) && !(n >= (2)))) && (!(n == (1)) || (n == (1) && !(y == (1)))) && n == (0) && y == (0))) (../plain/in-de61.c:47:3)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow

runtime: 00:00:10.166
vars: 49, evals: 111

|rho|=53
|called|=0
|stable|=53
|infl|=49
|wpoint|=0
|side_dep|=15
|side_infl|=25
|var_messages|=12
|rho_write|=18
|dep|=36
Found 4 contexts for 4 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_assert (2003) on ../plain/in-de61.c:5:1-10:1
1	contexts for entry state of reach_error (1999) on ../plain/in-de61.c:3:1-3:73
1	contexts for entry state of main (2006) on ../plain/in-de61.c:12:1-55:1
1	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140

Memory statistics: total=1203.93MB, max=24.88MB, minor=1200.52MB, major=77.37MB, promoted=73.95MB
    minor collections=579  major collections=15 compactions=0

[Warning][Witness] invariant unconfirmed: ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && x >= (2) && y >= (5)) || ((!((n + (((-1) * x) - z)) == (0)) || ((n + (((-1) * x) - z)) == (0) && !(((x + y) - n) >= (1))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && !(n >= x)) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n >= x && !(x >= (2))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n >= x && x >= (2) && !(y >= (5)))) && n == x && z == (0) && n <= (4294967295LL) && n >= (3) && y >= (2)) || ((!((n + (((-1) * x) - z)) == (0)) || ((n + (((-1) * x) - z)) == (0) && !(((x + y) - n) >= (1))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && !(n >= x)) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n >= x && !(n >= (3))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n >= x && n >= (3) && !(x >= (2))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n >= x && n >= (3) && x >= (2) && !(y >= (5)))) && (!(n == x) || (n == x && !(z == (0))) || (n == x && z == (0) && !(n >= (3))) || (n == x && z == (0) && n >= (3) && !(y >= (2)))) && (n - z) == (1) && x == (1) && (y - z) == (1) && n <= (4294967295LL) && n >= (5)) || ((!((n + (((-1) * x) - z)) == (0)) || ((n + (((-1) * x) - z)) == (0) && !(((x + y) - n) >= (1))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && !(n >= x)) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n >= x && !(n >= (3))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n >= x && n >= (3) && !(x >= (2))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n >= x && n >= (3) && x >= (2) && !(y >= (5)))) && (!(n == x) || (n == x && !(z == (0))) || (n == x && z == (0) && !(n >= (3))) || (n == x && z == (0) && n >= (3) && !(y >= (2)))) && (!((n - z) == (1)) || ((n - z) == (1) && !(x == (1))) || ((n - z) == (1) && x == (1) && !((y - z) == (1)))) && n == z && x == (0) && y == z && n <= (4294967295LL) && n >= (5)) || ((!((n + (((-1) * x) - z)) == (0)) || ((n + (((-1) * x) - z)) == (0) && !(((x + y) - n) >= (1))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && !(n <= (4294967295LL))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && !(n >= x)) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && !(n >= (3))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && !(x >= (2))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && x >= (2) && !(y >= (5)))) && (!(n == x) || (n == x && !(z == (0))) || (n == x && z == (0) && !(n <= (4294967295LL))) || (n == x && z == (0) && n <= (4294967295LL) && !(n >= (3))) || (n == x && z == (0) && n <= (4294967295LL) && n >= (3) && !(y >= (2)))) && (!((n - z) == (1)) || ((n - z) == (1) && !(x == (1))) || ((n - z) == (1) && x == (1) && !((y - z) == (1))) || ((n - z) == (1) && x == (1) && (y - z) == (1) && !(n <= (4294967295LL))) || ((n - z) == (1) && x == (1) && (y - z) == (1) && n <= (4294967295LL) && !(n >= (5)))) && (!(n == z) || (n == z && !(x == (0))) || (n == z && x == (0) && !(y == z)) || (n == z && x == (0) && y == z && !(n <= (4294967295LL))) || (n == z && x == (0) && y == z && n <= (4294967295LL) && !(n >= (5)))) && n == (4) && x == (3) && y == (4) && z == (1)) || ((!((n + (((-1) * x) - z)) == (0)) || ((n + (((-1) * x) - z)) == (0) && !(((x + y) - n) >= (1))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && !(n <= (4294967295LL))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && !(n >= x)) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && !(n >= (3))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && !(x >= (2))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && x >= (2) && !(y >= (5)))) && (!(n == x) || (n == x && !(z == (0))) || (n == x && z == (0) && !(n <= (4294967295LL))) || (n == x && z == (0) && n <= (4294967295LL) && !(n >= (3))) || (n == x && z == (0) && n <= (4294967295LL) && n >= (3) && !(y >= (2)))) && (!((n - z) == (1)) || ((n - z) == (1) && !(x == (1))) || ((n - z) == (1) && x == (1) && !((y - z) == (1))) || ((n - z) == (1) && x == (1) && (y - z) == (1) && !(n <= (4294967295LL))) || ((n - z) == (1) && x == (1) && (y - z) == (1) && n <= (4294967295LL) && !(n >= (5)))) && (!(n == z) || (n == z && !(x == (0))) || (n == z && x == (0) && !(y == z)) || (n == z && x == (0) && y == z && !(n <= (4294967295LL))) || (n == z && x == (0) && y == z && n <= (4294967295LL) && !(n >= (5)))) && (!(x == (3)) || (x == (3) && !(z == (1)))) && n == (4) && x == (2) && y == (4) && z == (2)) || ((!((n + (((-1) * x) - z)) == (0)) || ((n + (((-1) * x) - z)) == (0) && !(((x + y) - n) >= (1))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && !(n <= (4294967295LL))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && !(n >= x)) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && !(n >= (3))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && !(x >= (2))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && x >= (2) && !(y >= (5)))) && (!(n == x) || (n == x && !(z == (0))) || (n == x && z == (0) && !(n <= (4294967295LL))) || (n == x && z == (0) && n <= (4294967295LL) && !(n >= (3))) || (n == x && z == (0) && n <= (4294967295LL) && n >= (3) && !(y >= (2)))) && (!((n - z) == (1)) || ((n - z) == (1) && !((y - z) == (1))) || ((n - z) == (1) && (y - z) == (1) && !(n <= (4294967295LL))) || ((n - z) == (1) && (y - z) == (1) && n <= (4294967295LL) && !(n >= (5)))) && (!(n == z) || (n == z && !(x == (0))) || (n == z && x == (0) && !(y == z)) || (n == z && x == (0) && y == z && !(n <= (4294967295LL))) || (n == z && x == (0) && y == z && n <= (4294967295LL) && !(n >= (5)))) && (!(x == (3)) || (x == (3) && !(z == (1)))) && (!(x == (2)) || (x == (2) && !(z == (2)))) && n == (4) && x == (1) && y == (4) && z == (3)) || ((!((n + (((-1) * x) - z)) == (0)) || ((n + (((-1) * x) - z)) == (0) && !(((x + y) - n) >= (1))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && !(n <= (4294967295LL))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && !(n >= x)) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && !(n >= (3))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && !(x >= (2))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && x >= (2) && !(y >= (5)))) && (!(n == x) || (n == x && !(z == (0))) || (n == x && z == (0) && !(n <= (4294967295LL))) || (n == x && z == (0) && n <= (4294967295LL) && !(n >= (3))) || (n == x && z == (0) && n <= (4294967295LL) && n >= (3) && !(y >= (2)))) && (!((n - z) == (1)) || ((n - z) == (1) && !(x == (1))) || ((n - z) == (1) && x == (1) && !((y - z) == (1))) || ((n - z) == (1) && x == (1) && (y - z) == (1) && !(n <= (4294967295LL))) || ((n - z) == (1) && x == (1) && (y - z) == (1) && n <= (4294967295LL) && !(n >= (5)))) && (!(n == z) || (n == z && !(y == z)) || (n == z && y == z && !(n <= (4294967295LL))) || (n == z && y == z && n <= (4294967295LL) && !(n >= (5)))) && (!(x == (3)) || (x == (3) && !(z == (1)))) && (!(x == (2)) || (x == (2) && !(z == (2)))) && (!(x == (1)) || (x == (1) && !(z == (3)))) && n == (4) && x == (0) && y == (4) && z == (4)) || ((!((n + (((-1) * x) - z)) == (0)) || ((n + (((-1) * x) - z)) == (0) && !(((x + y) - n) >= (1))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && !(n <= (4294967295LL))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && !(n >= x)) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && !(n >= (3))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && !(x >= (2))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && x >= (2) && !(y >= (5)))) && (!(n == x) || (n == x && !(z == (0))) || (n == x && z == (0) && !(n <= (4294967295LL))) || (n == x && z == (0) && n <= (4294967295LL) && !(n >= (3))) || (n == x && z == (0) && n <= (4294967295LL) && n >= (3) && !(y >= (2)))) && (!((n - z) == (1)) || ((n - z) == (1) && !(x == (1))) || ((n - z) == (1) && x == (1) && !((y - z) == (1))) || ((n - z) == (1) && x == (1) && (y - z) == (1) && !(n <= (4294967295LL))) || ((n - z) == (1) && x == (1) && (y - z) == (1) && n <= (4294967295LL) && !(n >= (5)))) && (!(n == z) || (n == z && !(x == (0))) || (n == z && x == (0) && !(y == z)) || (n == z && x == (0) && y == z && !(n <= (4294967295LL))) || (n == z && x == (0) && y == z && n <= (4294967295LL) && !(n >= (5)))) && (!(n == (4)) || (n == (4) && !(x == (3))) || (n == (4) && x == (3) && !(y == (4)))) && (!(n == (4)) || (n == (4) && !(y == (4))) || (n == (4) && y == (4) && !(z == (2)))) && (!(n == (4)) || (n == (4) && !(x == (1))) || (n == (4) && x == (1) && !(y == (4))) || (n == (4) && x == (1) && y == (4) && !(z == (3)))) && (!(n == (4)) || (n == (4) && !(x == (0))) || (n == (4) && x == (0) && !(y == (4))) || (n == (4) && x == (0) && y == (4) && !(z == (4)))) && n == (3) && x == (2) && y == (3) && z == (1)) || ((!((n + (((-1) * x) - z)) == (0)) || ((n + (((-1) * x) - z)) == (0) && !(((x + y) - n) >= (1))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && !(n <= (4294967295LL))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && !(n >= x)) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && !(n >= (3))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && !(x >= (2))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && x >= (2) && !(y >= (5)))) && (!(n == x) || (n == x && !(z == (0))) || (n == x && z == (0) && !(n <= (4294967295LL))) || (n == x && z == (0) && n <= (4294967295LL) && !(n >= (3))) || (n == x && z == (0) && n <= (4294967295LL) && n >= (3) && !(y >= (2)))) && (!((n - z) == (1)) || ((n - z) == (1) && !((y - z) == (1))) || ((n - z) == (1) && (y - z) == (1) && !(n <= (4294967295LL))) || ((n - z) == (1) && (y - z) == (1) && n <= (4294967295LL) && !(n >= (5)))) && (!(n == z) || (n == z && !(x == (0))) || (n == z && x == (0) && !(y == z)) || (n == z && x == (0) && y == z && !(n <= (4294967295LL))) || (n == z && x == (0) && y == z && n <= (4294967295LL) && !(n >= (5)))) && (!(n == (4)) || (n == (4) && !(x == (3))) || (n == (4) && x == (3) && !(y == (4))) || (n == (4) && x == (3) && y == (4) && !(z == (1)))) && (!(n == (4)) || (n == (4) && !(x == (2))) || (n == (4) && x == (2) && !(y == (4)))) && (!(n == (4)) || (n == (4) && !(y == (4))) || (n == (4) && y == (4) && !(z == (3)))) && (!(n == (4)) || (n == (4) && !(x == (0))) || (n == (4) && x == (0) && !(y == (4))) || (n == (4) && x == (0) && y == (4) && !(z == (4)))) && (!(x == (2)) || (x == (2) && !(z == (1)))) && n == (3) && x == (1) && y == (3) && z == (2)) || ((!((n + (((-1) * x) - z)) == (0)) || ((n + (((-1) * x) - z)) == (0) && !(((x + y) - n) >= (1))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && !(n <= (4294967295LL))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && !(n >= x)) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && !(n >= (3))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && !(x >= (2))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && x >= (2) && !(y >= (5)))) && (!(n == x) || (n == x && !(z == (0))) || (n == x && z == (0) && !(n <= (4294967295LL))) || (n == x && z == (0) && n <= (4294967295LL) && !(n >= (3))) || (n == x && z == (0) && n <= (4294967295LL) && n >= (3) && !(y >= (2)))) && (!((n - z) == (1)) || ((n - z) == (1) && !(x == (1))) || ((n - z) == (1) && x == (1) && !((y - z) == (1))) || ((n - z) == (1) && x == (1) && (y - z) == (1) && !(n <= (4294967295LL))) || ((n - z) == (1) && x == (1) && (y - z) == (1) && n <= (4294967295LL) && !(n >= (5)))) && (!(n == z) || (n == z && !(y == z)) || (n == z && y == z && !(n <= (4294967295LL))) || (n == z && y == z && n <= (4294967295LL) && !(n >= (5)))) && (!(n == (4)) || (n == (4) && !(x == (3))) || (n == (4) && x == (3) && !(y == (4))) || (n == (4) && x == (3) && y == (4) && !(z == (1)))) && (!(n == (4)) || (n == (4) && !(x == (2))) || (n == (4) && x == (2) && !(y == (4))) || (n == (4) && x == (2) && y == (4) && !(z == (2)))) && (!(n == (4)) || (n == (4) && !(x == (1))) || (n == (4) && x == (1) && !(y == (4)))) && (!(n == (4)) || (n == (4) && !(y == (4))) || (n == (4) && y == (4) && !(z == (4)))) && (!(x == (2)) || (x == (2) && !(z == (1)))) && (!(x == (1)) || (x == (1) && !(z == (2)))) && n == (3) && x == (0) && y == (3) && z == (3)) || ((!((n + (((-1) * x) - z)) == (0)) || ((n + (((-1) * x) - z)) == (0) && !(((x + y) - n) >= (1))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && !(n <= (4294967295LL))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && !(n >= x)) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && !(n >= (3))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && !(x >= (2))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && x >= (2) && !(y >= (5)))) && (!(n == x) || (n == x && !(n <= (4294967295LL))) || (n == x && n <= (4294967295LL) && !(n >= (3))) || (n == x && n <= (4294967295LL) && n >= (3) && !(y >= (2)))) && (!((n - z) == (1)) || ((n - z) == (1) && !(x == (1))) || ((n - z) == (1) && x == (1) && !((y - z) == (1))) || ((n - z) == (1) && x == (1) && (y - z) == (1) && !(n <= (4294967295LL))) || ((n - z) == (1) && x == (1) && (y - z) == (1) && n <= (4294967295LL) && !(n >= (5)))) && (!(n == z) || (n == z && !(x == (0))) || (n == z && x == (0) && !(y == z)) || (n == z && x == (0) && y == z && !(n <= (4294967295LL))) || (n == z && x == (0) && y == z && n <= (4294967295LL) && !(n >= (5)))) && (!(n == (4)) || (n == (4) && !(x == (3))) || (n == (4) && x == (3) && !(y == (4))) || (n == (4) && x == (3) && y == (4) && !(z == (1)))) && (!(n == (4)) || (n == (4) && !(y == (4))) || (n == (4) && y == (4) && !(z == (2)))) && (!(n == (4)) || (n == (4) && !(x == (1))) || (n == (4) && x == (1) && !(y == (4))) || (n == (4) && x == (1) && y == (4) && !(z == (3)))) && (!(n == (4)) || (n == (4) && !(x == (0))) || (n == (4) && x == (0) && !(y == (4))) || (n == (4) && x == (0) && y == (4) && !(z == (4)))) && (!(n == (3)) || (n == (3) && !(y == (3))) || (n == (3) && y == (3) && !(z == (1)))) && (!(n == (3)) || (n == (3) && !(x == (1))) || (n == (3) && x == (1) && !(y == (3))) || (n == (3) && x == (1) && y == (3) && !(z == (2)))) && (!(n == (3)) || (n == (3) && !(x == (0))) || (n == (3) && x == (0) && !(y == (3))) || (n == (3) && x == (0) && y == (3) && !(z == (3)))) && n == (2) && x == (2) && y == (2) && z == (0)) || ((!((n + (((-1) * x) - z)) == (0)) || ((n + (((-1) * x) - z)) == (0) && !(((x + y) - n) >= (1))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && !(n <= (4294967295LL))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && !(n >= x)) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && !(n >= (3))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && !(x >= (2))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && x >= (2) && !(y >= (5)))) && (!(n == x) || (n == x && !(z == (0))) || (n == x && z == (0) && !(n <= (4294967295LL))) || (n == x && z == (0) && n <= (4294967295LL) && !(n >= (3))) || (n == x && z == (0) && n <= (4294967295LL) && n >= (3) && !(y >= (2)))) && (!((n - z) == (1)) || ((n - z) == (1) && !((y - z) == (1))) || ((n - z) == (1) && (y - z) == (1) && !(n <= (4294967295LL))) || ((n - z) == (1) && (y - z) == (1) && n <= (4294967295LL) && !(n >= (5)))) && (!(n == z) || (n == z && !(x == (0))) || (n == z && x == (0) && !(y == z)) || (n == z && x == (0) && y == z && !(n <= (4294967295LL))) || (n == z && x == (0) && y == z && n <= (4294967295LL) && !(n >= (5)))) && (!(n == (4)) || (n == (4) && !(x == (3))) || (n == (4) && x == (3) && !(y == (4)))) && (!(n == (4)) || (n == (4) && !(x == (2))) || (n == (4) && x == (2) && !(y == (4))) || (n == (4) && x == (2) && y == (4) && !(z == (2)))) && (!(n == (4)) || (n == (4) && !(y == (4))) || (n == (4) && y == (4) && !(z == (3)))) && (!(n == (4)) || (n == (4) && !(x == (0))) || (n == (4) && x == (0) && !(y == (4))) || (n == (4) && x == (0) && y == (4) && !(z == (4)))) && (!(n == (3)) || (n == (3) && !(x == (2))) || (n == (3) && x == (2) && !(y == (3)))) && (!(n == (3)) || (n == (3) && !(y == (3))) || (n == (3) && y == (3) && !(z == (2)))) && (!(n == (3)) || (n == (3) && !(x == (0))) || (n == (3) && x == (0) && !(y == (3))) || (n == (3) && x == (0) && y == (3) && !(z == (3)))) && (!(x == (2)) || (x == (2) && !(z == (0)))) && n == (2) && x == (1) && y == (2) && z == (1)) || ((!((n + (((-1) * x) - z)) == (0)) || ((n + (((-1) * x) - z)) == (0) && !(((x + y) - n) >= (1))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && !(n <= (4294967295LL))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && !(n >= x)) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && !(n >= (3))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && !(x >= (2))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && x >= (2) && !(y >= (5)))) && (!(n == x) || (n == x && !(z == (0))) || (n == x && z == (0) && !(n <= (4294967295LL))) || (n == x && z == (0) && n <= (4294967295LL) && !(n >= (3))) || (n == x && z == (0) && n <= (4294967295LL) && n >= (3) && !(y >= (2)))) && (!((n - z) == (1)) || ((n - z) == (1) && !(x == (1))) || ((n - z) == (1) && x == (1) && !((y - z) == (1))) || ((n - z) == (1) && x == (1) && (y - z) == (1) && !(n <= (4294967295LL))) || ((n - z) == (1) && x == (1) && (y - z) == (1) && n <= (4294967295LL) && !(n >= (5)))) && (!(n == z) || (n == z && !(y == z)) || (n == z && y == z && !(n <= (4294967295LL))) || (n == z && y == z && n <= (4294967295LL) && !(n >= (5)))) && (!(n == (4)) || (n == (4) && !(x == (3))) || (n == (4) && x == (3) && !(y == (4))) || (n == (4) && x == (3) && y == (4) && !(z == (1)))) && (!(n == (4)) || (n == (4) && !(x == (2))) || (n == (4) && x == (2) && !(y == (4)))) && (!(n == (4)) || (n == (4) && !(x == (1))) || (n == (4) && x == (1) && !(y == (4))) || (n == (4) && x == (1) && y == (4) && !(z == (3)))) && (!(n == (4)) || (n == (4) && !(y == (4))) || (n == (4) && y == (4) && !(z == (4)))) && (!(n == (3)) || (n == (3) && !(x == (2))) || (n == (3) && x == (2) && !(y == (3))) || (n == (3) && x == (2) && y == (3) && !(z == (1)))) && (!(n == (3)) || (n == (3) && !(x == (1))) || (n == (3) && x == (1) && !(y == (3)))) && (!(n == (3)) || (n == (3) && !(y == (3))) || (n == (3) && y == (3) && !(z == (3)))) && (!(x == (2)) || (x == (2) && !(z == (0)))) && (!(x == (1)) || (x == (1) && !(z == (1)))) && n == (2) && x == (0) && y == (2) && z == (2)) || ((!((n + (((-1) * x) - z)) == (0)) || ((n + (((-1) * x) - z)) == (0) && !(((x + y) - n) >= (1))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && !(n <= (4294967295LL))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && !(n >= x)) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && !(n >= (3))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && !(x >= (2))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && x >= (2) && !(y >= (5)))) && (!(n == x) || (n == x && !(n <= (4294967295LL))) || (n == x && n <= (4294967295LL) && !(n >= (3))) || (n == x && n <= (4294967295LL) && n >= (3) && !(y >= (2)))) && (!((n - z) == (1)) || ((n - z) == (1) && !((y - z) == (1))) || ((n - z) == (1) && (y - z) == (1) && !(n <= (4294967295LL))) || ((n - z) == (1) && (y - z) == (1) && n <= (4294967295LL) && !(n >= (5)))) && (!(n == z) || (n == z && !(x == (0))) || (n == z && x == (0) && !(y == z)) || (n == z && x == (0) && y == z && !(n <= (4294967295LL))) || (n == z && x == (0) && y == z && n <= (4294967295LL) && !(n >= (5)))) && (!(n == (4)) || (n == (4) && !(x == (3))) || (n == (4) && x == (3) && !(y == (4))) || (n == (4) && x == (3) && y == (4) && !(z == (1)))) && (!(n == (4)) || (n == (4) && !(x == (2))) || (n == (4) && x == (2) && !(y == (4))) || (n == (4) && x == (2) && y == (4) && !(z == (2)))) && (!(n == (4)) || (n == (4) && !(y == (4))) || (n == (4) && y == (4) && !(z == (3)))) && (!(n == (4)) || (n == (4) && !(x == (0))) || (n == (4) && x == (0) && !(y == (4))) || (n == (4) && x == (0) && y == (4) && !(z == (4)))) && (!(n == (3)) || (n == (3) && !(x == (2))) || (n == (3) && x == (2) && !(y == (3))) || (n == (3) && x == (2) && y == (3) && !(z == (1)))) && (!(n == (3)) || (n == (3) && !(y == (3))) || (n == (3) && y == (3) && !(z == (2)))) && (!(n == (3)) || (n == (3) && !(x == (0))) || (n == (3) && x == (0) && !(y == (3))) || (n == (3) && x == (0) && y == (3) && !(z == (3)))) && (!(n == (2)) || (n == (2) && !(x == (2))) || (n == (2) && x == (2) && !(y == (2)))) && (!(n == (2)) || (n == (2) && !(y == (2))) || (n == (2) && y == (2) && !(z == (1)))) && (!(n == (2)) || (n == (2) && !(x == (0))) || (n == (2) && x == (0) && !(y == (2))) || (n == (2) && x == (0) && y == (2) && !(z == (2)))) && n == (1) && x == (1) && y == (1) && z == (0)) || ((!((n + (((-1) * x) - z)) == (0)) || ((n + (((-1) * x) - z)) == (0) && !(((x + y) - n) >= (1))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && !(n <= (4294967295LL))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && !(n >= x)) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && !(n >= (3))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && !(x >= (2))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && x >= (2) && !(y >= (5)))) && (!(n == x) || (n == x && !(z == (0))) || (n == x && z == (0) && !(n <= (4294967295LL))) || (n == x && z == (0) && n <= (4294967295LL) && !(n >= (3))) || (n == x && z == (0) && n <= (4294967295LL) && n >= (3) && !(y >= (2)))) && (!((n - z) == (1)) || ((n - z) == (1) && !(x == (1))) || ((n - z) == (1) && x == (1) && !((y - z) == (1))) || ((n - z) == (1) && x == (1) && (y - z) == (1) && !(n <= (4294967295LL))) || ((n - z) == (1) && x == (1) && (y - z) == (1) && n <= (4294967295LL) && !(n >= (5)))) && (!(n == z) || (n == z && !(y == z)) || (n == z && y == z && !(n <= (4294967295LL))) || (n == z && y == z && n <= (4294967295LL) && !(n >= (5)))) && (!(n == (4)) || (n == (4) && !(x == (3))) || (n == (4) && x == (3) && !(y == (4)))) && (!(n == (4)) || (n == (4) && !(x == (2))) || (n == (4) && x == (2) && !(y == (4))) || (n == (4) && x == (2) && y == (4) && !(z == (2)))) && (!(n == (4)) || (n == (4) && !(x == (1))) || (n == (4) && x == (1) && !(y == (4))) || (n == (4) && x == (1) && y == (4) && !(z == (3)))) && (!(n == (4)) || (n == (4) && !(y == (4))) || (n == (4) && y == (4) && !(z == (4)))) && (!(n == (3)) || (n == (3) && !(x == (2))) || (n == (3) && x == (2) && !(y == (3)))) && (!(n == (3)) || (n == (3) && !(x == (1))) || (n == (3) && x == (1) && !(y == (3))) || (n == (3) && x == (1) && y == (3) && !(z == (2)))) && (!(n == (3)) || (n == (3) && !(y == (3))) || (n == (3) && y == (3) && !(z == (3)))) && (!(n == (2)) || (n == (2) && !(x == (2))) || (n == (2) && x == (2) && !(y == (2))) || (n == (2) && x == (2) && y == (2) && !(z == (0)))) && (!(n == (2)) || (n == (2) && !(x == (1))) || (n == (2) && x == (1) && !(y == (2)))) && (!(n == (2)) || (n == (2) && !(y == (2))) || (n == (2) && y == (2) && !(z == (2)))) && (!(x == (1)) || (x == (1) && !(z == (0)))) && n == (1) && x == (0) && y == (1) && z == (1)) || ((!((n + (((-1) * x) - z)) == (0)) || ((n + (((-1) * x) - z)) == (0) && !(((x + y) - n) >= (1))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && !(n <= (4294967295LL))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && !(n >= x)) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && !(n >= (3))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && !(x >= (2))) || ((n + (((-1) * x) - z)) == (0) && ((x + y) - n) >= (1) && n <= (4294967295LL) && n >= x && n >= (3) && x >= (2) && !(y >= (5)))) && (!(n == x) || (n == x && !(n <= (4294967295LL))) || (n == x && n <= (4294967295LL) && !(n >= (3))) || (n == x && n <= (4294967295LL) && n >= (3) && !(y >= (2)))) && (!((n - z) == (1)) || ((n - z) == (1) && !(x == (1))) || ((n - z) == (1) && x == (1) && !((y - z) == (1))) || ((n - z) == (1) && x == (1) && (y - z) == (1) && !(n <= (4294967295LL))) || ((n - z) == (1) && x == (1) && (y - z) == (1) && n <= (4294967295LL) && !(n >= (5)))) && (!(n == z) || (n == z && !(y == z)) || (n == z && y == z && !(n <= (4294967295LL))) || (n == z && y == z && n <= (4294967295LL) && !(n >= (5)))) && (!(n == (4)) || (n == (4) && !(x == (3))) || (n == (4) && x == (3) && !(y == (4))) || (n == (4) && x == (3) && y == (4) && !(z == (1)))) && (!(n == (4)) || (n == (4) && !(x == (2))) || (n == (4) && x == (2) && !(y == (4))) || (n == (4) && x == (2) && y == (4) && !(z == (2)))) && (!(n == (4)) || (n == (4) && !(x == (1))) || (n == (4) && x == (1) && !(y == (4))) || (n == (4) && x == (1) && y == (4) && !(z == (3)))) && (!(n == (4)) || (n == (4) && !(y == (4))) || (n == (4) && y == (4) && !(z == (4)))) && (!(n == (3)) || (n == (3) && !(x == (2))) || (n == (3) && x == (2) && !(y == (3))) || (n == (3) && x == (2) && y == (3) && !(z == (1)))) && (!(n == (3)) || (n == (3) && !(x == (1))) || (n == (3) && x == (1) && !(y == (3))) || (n == (3) && x == (1) && y == (3) && !(z == (2)))) && (!(n == (3)) || (n == (3) && !(y == (3))) || (n == (3) && y == (3) && !(z == (3)))) && (!(n == (2)) || (n == (2) && !(x == (2))) || (n == (2) && x == (2) && !(y == (2)))) && (!(n == (2)) || (n == (2) && !(x == (1))) || (n == (2) && x == (1) && !(y == (2))) || (n == (2) && x == (1) && y == (2) && !(z == (1)))) && (!(n == (2)) || (n == (2) && !(y == (2))) || (n == (2) && y == (2) && !(z == (2)))) && (!(n == (1)) || (n == (1) && !(x == (1))) || (n == (1) && x == (1) && !(y == (1)))) && (!(n == (1)) || (n == (1) && !(y == (1))) || (n == (1) && y == (1) && !(z == (1)))) && n == (0) && x == (0) && y == (0) && z == (0)) (../plain/in-de61.c:29:3)
[Warning][Witness] invariant unconfirmed: ((n + (((-1) * x) - y)) == (0) && n <= (4294967295LL) && (n - x) >= (1) && n >= (2) && x >= (0) && z >= (2)) || ((!((n + (((-1) * x) - y)) == (0)) || ((n + (((-1) * x) - y)) == (0) && !((n - x) >= (1))) || ((n + (((-1) * x) - y)) == (0) && (n - x) >= (1) && !(n >= (2))) || ((n + (((-1) * x) - y)) == (0) && (n - x) >= (1) && n >= (2) && !(x >= (0)))) && n == x && y == (0) && n <= (4294967295LL) && n >= (3) && z >= (2)) || ((!((n + (((-1) * x) - y)) == (0)) || ((n + (((-1) * x) - y)) == (0) && !(n <= (4294967295LL))) || ((n + (((-1) * x) - y)) == (0) && n <= (4294967295LL) && !((n - x) >= (1))) || ((n + (((-1) * x) - y)) == (0) && n <= (4294967295LL) && (n - x) >= (1) && !(n >= (2))) || ((n + (((-1) * x) - y)) == (0) && n <= (4294967295LL) && (n - x) >= (1) && n >= (2) && !(x >= (0)))) && (!(n == x) || (n == x && !(n <= (4294967295LL))) || (n == x && n <= (4294967295LL) && !(n >= (3)))) && n == (2) && x == (2) && y == (0) && z >= (2)) || ((!((n + (((-1) * x) - y)) == (0)) || ((n + (((-1) * x) - y)) == (0) && !(n <= (4294967295LL))) || ((n + (((-1) * x) - y)) == (0) && n <= (4294967295LL) && !((n - x) >= (1))) || ((n + (((-1) * x) - y)) == (0) && n <= (4294967295LL) && (n - x) >= (1) && !(n >= (2))) || ((n + (((-1) * x) - y)) == (0) && n <= (4294967295LL) && (n - x) >= (1) && n >= (2) && !(x >= (0))) || ((n + (((-1) * x) - y)) == (0) && n <= (4294967295LL) && (n - x) >= (1) && n >= (2) && x >= (0) && !(z >= (2)))) && (!(n == x) || (n == x && !(n <= (4294967295LL))) || (n == x && n <= (4294967295LL) && !(n >= (3))) || (n == x && n <= (4294967295LL) && n >= (3) && !(z >= (2)))) && (!(n == (2)) || (n == (2) && !(x == (2))) || (n == (2) && x == (2) && !(z >= (2)))) && n == (1) && x == (1) && y == (0) && z == (1)) || ((!((n + (((-1) * x) - y)) == (0)) || ((n + (((-1) * x) - y)) == (0) && !(n <= (4294967295LL))) || ((n + (((-1) * x) - y)) == (0) && n <= (4294967295LL) && !((n - x) >= (1))) || ((n + (((-1) * x) - y)) == (0) && n <= (4294967295LL) && (n - x) >= (1) && !(n >= (2))) || ((n + (((-1) * x) - y)) == (0) && n <= (4294967295LL) && (n - x) >= (1) && n >= (2) && !(x >= (0))) || ((n + (((-1) * x) - y)) == (0) && n <= (4294967295LL) && (n - x) >= (1) && n >= (2) && x >= (0) && !(z >= (2)))) && (!(n == x) || (n == x && !(y == (0))) || (n == x && y == (0) && !(n <= (4294967295LL))) || (n == x && y == (0) && n <= (4294967295LL) && !(n >= (3))) || (n == x && y == (0) && n <= (4294967295LL) && n >= (3) && !(z >= (2)))) && (!(n == (2)) || (n == (2) && !(x == (2))) || (n == (2) && x == (2) && !(y == (0))) || (n == (2) && x == (2) && y == (0) && !(z >= (2)))) && (!(x == (1)) || (x == (1) && !(y == (0)))) && n == (1) && x == (0) && y == (1) && z == (1)) || ((!((n + (((-1) * x) - y)) == (0)) || ((n + (((-1) * x) - y)) == (0) && !(n <= (4294967295LL))) || ((n + (((-1) * x) - y)) == (0) && n <= (4294967295LL) && !((n - x) >= (1))) || ((n + (((-1) * x) - y)) == (0) && n <= (4294967295LL) && (n - x) >= (1) && !(n >= (2))) || ((n + (((-1) * x) - y)) == (0) && n <= (4294967295LL) && (n - x) >= (1) && n >= (2) && !(x >= (0))) || ((n + (((-1) * x) - y)) == (0) && n <= (4294967295LL) && (n - x) >= (1) && n >= (2) && x >= (0) && !(z >= (2)))) && (!(n == x) || (n == x && !(n <= (4294967295LL))) || (n == x && n <= (4294967295LL) && !(n >= (3))) || (n == x && n <= (4294967295LL) && n >= (3) && !(z >= (2)))) && (!(n == (2)) || (n == (2) && !(x == (2))) || (n == (2) && x == (2) && !(z >= (2)))) && (!(n == (1)) || (n == (1) && !(x == (1))) || (n == (1) && x == (1) && !(z == (1)))) && (!(n == (1)) || (n == (1) && !(y == (1))) || (n == (1) && y == (1) && !(z == (1)))) && n == (0) && x == (0) && y == (0) && z >= (0)) (../plain/in-de61.c:41:3)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 4
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 4
SV-COMP result: unknown

vars = 49    evals = 111    narrow_reuses = 6

Timings:
                                  cputime   walltime   allocated   count
Default                           10.453s    10.458s   1217.19MB      1×
  preprocess                         0.023s     0.022s      0.01MB      1×
  FrontC                             0.004s     0.004s      4.09MB      4×
  Cabs2cil                           0.006s     0.006s      4.71MB      4×
  mergeCIL                           0.003s     0.003s      3.34MB      1×
  analysis                          10.413s    10.418s   1200.04MB      1×
    createCFG                          0.001s     0.001s      0.63MB      1×
      handle                             0.001s     0.001s      0.11MB     33×
      iter_connect                       0.001s     0.001s      0.41MB     33×
        computeSCCs                        0.001s     0.001s      0.24MB     34×
    FrontC                             0.041s     0.041s     16.87MB      8×
    Cabs2cil                           0.010s     0.011s     15.37MB      8×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            3.756s     3.758s    923.18MB      1×
      S.Dom.equal                        0.001s     0.001s      0.04MB    117×
      base unassume                      0.761s     0.761s    782.15MB     36×
      cheap_full_reach                   0.001s     0.001s      0.03MB      1×
      postsolver                         0.026s     0.026s     21.07MB      1×
        postsolver_iter                    0.026s     0.026s     21.03MB      1×
    warn_global                        0.001s     0.001s      0.13MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
