/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 graves-cpa/vogal-1.yml.witness.yml --witness.yaml.validate graves-cpa/vogal-1.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/vogal-1.i


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Warning][Witness] couldn't locate invariant: (cont == (0U) && cont_aux == (2) && i == (1U) && j == (2U) && n_caracter == (1U)) || (cont == (0U) && cont_aux == (0) && i == (0U) && n_caracter == (0U)) || ((!(cont == (0U)) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (0U)))) && cont == (1U) && cont_aux == (2) && i == (1U) && j == (2U) && n_caracter == (1U)) || ((!(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U)))) && cont == (1U) && !(cont_aux == (2)))) && cont == (2U) && cont_aux == (0) && i == (1U) && j == (2U) && n_caracter == (1U)) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && cont == (1U) && !(cont_aux == (2))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && cont == (1U) && !(cont_aux == (2)))) && !(cont == (2U)))) && cont == (0U) && cont_aux == (0) && i == (1U) && j == (2U) && n_caracter == (1U)) || ((!(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || ((!(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U)))) && cont == (1U) && !(cont_aux == (2))) || ((!(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || ((!(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U)))) && cont == (1U) && !(cont_aux == (2)))) && !(cont == (2U))) || (cont == (2U) && !(cont_aux == (0)))) && cont == (0U) && cont_aux == (1) && i == (1U) && j == (2U) && n_caracter == (1U)) || ((!(cont == (0U)) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (0U)))) && !(cont_aux == (2))) || ((!(cont == (0U)) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (0U)))) && !(cont_aux == (2)))) && !(cont == (2U))) || (cont == (2U) && !(cont_aux == (0)))) && cont == (1U) && cont_aux == (1) && i == (1U) && j == (2U) && n_caracter == (1U)) || ((!(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U)))) && !(cont_aux == (2))) || ((!(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U)))) && !(cont_aux == (2)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont_aux == (2))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont_aux == (2)))) && !(cont == (2U)))) && cont == (0U) && !(cont_aux == (1))) || ((!(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U)))) && !(cont_aux == (2))) || ((!(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U)))) && !(cont_aux == (2)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont_aux == (2))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont_aux == (2)))) && !(cont == (2U)))) && cont == (0U))) && !(cont_aux == (1)))) && cont == (1U) && cont_aux == (0) && i == (1U) && j == (2U) && n_caracter == (1U)) || ((!(cont == (0U)) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (0U)))) && cont == (1U) && !(cont_aux == (2))) || !(cont_aux == (0)) || ((!(cont == (0U)) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (0U))) || !(cont_aux == (0))) && !(cont == (1U))) || (cont == (1U) && !(cont_aux == (0)))) && cont == (2U) && cont_aux == (1) && i == (1U) && j == (2U) && n_caracter == (1U)) (../plain/vogal-1.i:58:3)
[Info][Witness] unassume invariant: (((((i == 5U && n_caracter == 0U) || ((i == 5U && ! (n_caracter == 0U)) && n_caracter == 2U)) || ((i == 5U && ! (n_caracter == 0U)) && n_caracter == 3U)) || ((i == 5U && ! (n_caracter == 0U)) && n_caracter == 1U)) || ((i == 5U && ! (n_caracter == 0U)) && n_caracter == 4U)) && (((((i == 1U || (! (i == 1U) && i == 0U)) || ((! (i == 1U) && ! (i == 0U)) && i == 3U)) || (((! (i == 1U) && ! (i == 0U)) && ! (i == 3U)) && i == 2U)) || ((((! (i == 1U) && ! (i == 0U)) && ! (i == 3U)) && ! (i == 2U)) && i == 4U)) && (((((i == 3U || (! (i == 3U) && i == 4U)) || ((! (i == 3U) && ! (i == 4U)) && i == 5U)) || (((! (i == 3U) && ! (i == 4U)) && ! (i == 5U)) && i == 2U)) || ((((! (i == 3U) && ! (i == 4U)) && ! (i == 5U)) && ! (i == 2U)) && i == 0U)) || (((((! (i == 3U) && ! (i == 4U)) && ! (i == 5U)) && ! (i == 2U)) && ! (i == 0U)) && i == 1U))) (../plain/vogal-1.i:37:3-37:17)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/vogal-1.i:39:5-39:17)
[Info][Witness] unassume invariant: (((((i == 5U && n_caracter == 0U) || ((i == 5U && ! (n_caracter == 0U)) && n_caracter == 2U)) || ((i == 5U && ! (n_caracter == 0U)) && n_caracter == 3U)) || ((i == 5U && ! (n_caracter == 0U)) && n_caracter == 1U)) || ((i == 5U && ! (n_caracter == 0U)) && n_caracter == 4U)) && (((((i == 1U || (! (i == 1U) && i == 0U)) || ((! (i == 1U) && ! (i == 0U)) && i == 3U)) || (((! (i == 1U) && ! (i == 0U)) && ! (i == 3U)) && i == 2U)) || ((((! (i == 1U) && ! (i == 0U)) && ! (i == 3U)) && ! (i == 2U)) && i == 4U)) && (((((i == 3U || (! (i == 3U) && i == 4U)) || ((! (i == 3U) && ! (i == 4U)) && i == 5U)) || (((! (i == 3U) && ! (i == 4U)) && ! (i == 5U)) && i == 2U)) || ((((! (i == 3U) && ! (i == 4U)) && ! (i == 5U)) && ! (i == 2U)) && i == 0U)) || (((((! (i == 3U) && ! (i == 4U)) && ! (i == 5U)) && ! (i == 2U)) && ! (i == 0U)) && i == 1U))) (../plain/vogal-1.i:39:5-39:17)
[Info][Witness] unassume invariant: (((((cont == 0U && i == 5U) && n_caracter == 0U) || (((cont == 0U && i == 5U) && ! (n_caracter == 0U)) && n_caracter == 2U)) || (((i == 5U && ! (n_caracter == 0U)) && cont == 0U) && n_caracter == 3U)) || (((i == 5U && ! (n_caracter == 0U)) && cont == 0U) && n_caracter == 1U)) || (((i == 5U && ! (n_caracter == 0U)) && cont == 0U) && n_caracter == 4U) (../plain/vogal-1.i:42:6-42:27)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/vogal-1.i:45:12-45:18)
[Info][Witness] unassume invariant: ((((((((((((((((((cont == 2U && i == 1U) && j == 2U) && n_caracter == 3U) || (((cont == 0U && i == 1U) && j == 2U) && n_caracter == 2U)) || ((cont == 0U && i == 0U) && n_caracter == 2U)) || (((cont == 1U && i == 1U) && j == 2U) && n_caracter == 4U)) || (((cont == 0U && i == 2U) && j == 2U) && n_caracter == 4U)) || (((cont == 2U && i == 1U) && j == 2U) && n_caracter == 2U)) || (((cont == 1U && i == 2U) && j == 2U) && n_caracter == 3U)) || (((cont == 1U && i == 1U) && j == 2U) && n_caracter == 2U)) || ((cont == 0U && i == 0U) && n_caracter == 4U)) || (((cont == 1U && i == 1U) && j == 2U) && n_caracter == 3U)) || (((cont == 0U && i == 1U) && j == 2U) && n_caracter == 4U)) || (((cont == 0U && i == 2U) && j == 2U) && n_caracter == 3U)) || (((cont == 2U && i == 1U) && j == 2U) && n_caracter == 4U)) || (((cont == 0U && i == 1U) && j == 2U) && n_caracter == 3U)) || (((cont == 2U && i == 2U) && j == 2U) && n_caracter == 3U)) || ((cont == 0U && i == 0U) && n_caracter == 1U)) || ((cont == 0U && i == 0U) && n_caracter == 3U) (../plain/vogal-1.i:43:9-43:23)
[Info][Witness] unassume invariant: ((((((((((((((((((cont == 2U && i == 1U) && j == 2U) && n_caracter == 3U) || (((cont == 0U && i == 1U) && j == 2U) && n_caracter == 2U)) || ((cont == 0U && i == 0U) && n_caracter == 2U)) || (((cont == 1U && i == 1U) && j == 2U) && n_caracter == 4U)) || (((cont == 0U && i == 2U) && j == 2U) && n_caracter == 4U)) || (((cont == 2U && i == 1U) && j == 2U) && n_caracter == 2U)) || (((cont == 1U && i == 2U) && j == 2U) && n_caracter == 3U)) || (((cont == 1U && i == 1U) && j == 2U) && n_caracter == 2U)) || ((cont == 0U && i == 0U) && n_caracter == 4U)) || (((cont == 1U && i == 1U) && j == 2U) && n_caracter == 3U)) || (((cont == 0U && i == 1U) && j == 2U) && n_caracter == 4U)) || (((cont == 0U && i == 2U) && j == 2U) && n_caracter == 3U)) || (((cont == 2U && i == 1U) && j == 2U) && n_caracter == 4U)) || (((cont == 0U && i == 1U) && j == 2U) && n_caracter == 3U)) || (((cont == 2U && i == 2U) && j == 2U) && n_caracter == 3U)) || ((cont == 0U && i == 0U) && n_caracter == 1U)) || ((cont == 0U && i == 0U) && n_caracter == 3U) (../plain/vogal-1.i:43:9-43:23)
[Info][Witness] unassume invariant: (((((cont == 0U && i == 5U) && n_caracter == 0U) || (((cont == 0U && i == 5U) && ! (n_caracter == 0U)) && n_caracter == 2U)) || (((i == 5U && ! (n_caracter == 0U)) && cont == 0U) && n_caracter == 3U)) || (((i == 5U && ! (n_caracter == 0U)) && cont == 0U) && n_caracter == 1U)) || (((i == 5U && ! (n_caracter == 0U)) && cont == 0U) && n_caracter == 4U) (../plain/vogal-1.i:42:6-42:27)
[Info][Witness] unassume invariant: ((((((((((((((((((((((((((((((((((i == 1U && j == 2U) && n_caracter == 1U) && cont == 1U) && cont_aux == 1) || ((((i == 1U && n_caracter == 1U) && j == 2U) && cont == 1U) && cont_aux == 2)) || ((((i == 1U && n_caracter == 1U) && j == 2U) && cont == 2U) && cont_aux == 0)) || ((((i == 1U && n_caracter == 1U) && j == 2U) && cont == 2U) && cont_aux == 1)) || ((((i == 1U && n_caracter == 1U) && j == 2U) && cont == 0U) && cont_aux == 1)) || ((((i == 1U && n_caracter == 1U) && j == 2U) && cont == 0U) && cont_aux == 2)) || ((((i == 1U && n_caracter == 1U) && j == 2U) && cont == 0U) && cont_aux == 0)) || (((((i == 1U && n_caracter == 1U) && j == 2U) && ! (cont == 0U)) && cont == 1U) && cont_aux == 0)) || (((((i == 1U && n_caracter == 1U) && j == 2U) && (((! (cont == 0U) || (cont == 0U && ! (cont_aux == 0))) || ((! (cont == 0U) || (cont == 0U && ! (cont_aux == 0))) && ! (cont == 1U))) || (cont == 1U && ! (cont_aux == 0)))) && cont == 2U) && cont_aux == 2)) || ((((i == 0U && cont_aux == 0) && cont == 2U) && j == 2U) && n_caracter == 1U)) || ((((i == 0U && cont_aux == 0) && cont == 0U) && j == 2U) && n_caracter == 2U)) || ((((i == 0U && cont_aux == 0) && cont == 3U) && j == 2U) && n_caracter == 2U)) || ((((i == 0U && cont_aux == 0) && cont == 1U) && j == 2U) && n_caracter == 2U)) || ((((i == 0U && cont_aux == 0) && cont == 0U) && j == 2U) && n_caracter == 1U)) || ((((i == 0U && cont_aux == 0) && cont == 2U) && j == 2U) && n_caracter == 2U)) || (((i == 0U && cont_aux == 0) && cont == 0U) && n_caracter == 0U)) || ((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && cont == 1U) && cont_aux == 0) && i == 0U) && j == 2U) && n_caracter == 1U)) || (((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && j == 2U) && n_caracter == 2U)) || ((((((((((! (i == 0U) || (i == 0U && ! (cont == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U))) || ! (cont == 0U)) || (cont == 0U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 1U) && cont_aux == 0) && i == 1U) && j == 2U) && n_caracter == 1U)) || (((((((((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || (((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) && ! (cont == 1U))) || (cont == 1U && ! (cont_aux == 0))) || ((cont == 1U && cont_aux == 0) && ! (i == 0U))) || (((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || (i == 0U && cont_aux == 0)) || ((i == 0U && cont_aux == 0) && ! (cont == 1U))) || (((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || (i == 0U && cont_aux == 0)) && ! (cont == 1U))) || (cont == 1U && ! (cont_aux == 0))) || ((cont == 1U && cont_aux == 0) && ! (i == 0U))) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || (((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) || ! (cont == 0U)) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 1U))) && cont == 2U) && cont_aux == 1) && i == 1U) && j == 2U) && n_caracter == 1U)) || ((((((((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (i == 0U && cont_aux == 0)) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (i == 0U && cont_aux == 0)) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (i == 0U && cont_aux == 0)) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U) && ! (cont_aux == 1))) && cont == 1U) && cont_aux == 2) && i == 1U) && j == 2U) && n_caracter == 1U)) || (((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && j == 2U) && n_caracter == 1U)) || (((((((((((((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && ! (i == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && i == 1U) && ! (n_caracter == 1U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && ! (i == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && i == 1U) && ! (n_caracter == 1U))) && ! (cont == 2U))) || ((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && ! (i == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && i == 1U) && ! (n_caracter == 1U))) && cont == 2U) && ! (cont_aux == 1))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && cont == 2U) && cont_aux == 1) && ! (i == 1U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && cont == 2U) && cont_aux == 1) && i == 1U) && ! (n_caracter == 1U))) || (((((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && ! (i == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && i == 1U) && ! (n_caracter == 1U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && ! (i == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && i == 1U) && ! (n_caracter == 1U))) && ! (cont == 2U))) || ((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && ! (i == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && i == 1U) && ! (n_caracter == 1U))) && cont == 2U) && ! (cont_aux == 1))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && cont == 2U) && cont_aux == 1) && ! (i == 1U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && cont == 2U) && cont_aux == 1) && i == 1U) && ! (n_caracter == 1U))) && ! (cont_aux == 2))) || (((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && ! (cont == 2U))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && cont == 2U) && ! (cont_aux == 1))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && cont == 2U) && cont_aux == 1)) && cont_aux == 2) && ! (i == 1U))) || (((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (cont == 2U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && cont == 2U) && ! (cont_aux == 1))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && cont == 2U) && cont_aux == 1)) && cont_aux == 2) && i == 1U) && ! (n_caracter == 1U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 1U))) && cont == 1U) && cont_aux == 0) && i == 0U) && j == 2U) && n_caracter == 2U)) || (((((((((((((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || (((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) && ! (cont == 1U))) || (cont == 1U && ! (cont_aux == 0))) || ((cont == 1U && cont_aux == 0) && ! (i == 0U))) || (((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || (i == 0U && cont_aux == 0)) || ((i == 0U && cont_aux == 0) && ! (cont == 1U))) || (((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || (i == 0U && cont_aux == 0)) && ! (cont == 1U))) || (cont == 1U && ! (cont_aux == 0))) || ((cont == 1U && cont_aux == 0) && ! (i == 0U))) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || (((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) || ! (cont == 0U)) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 1U))) || (((((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || (((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) && ! (cont == 1U))) || (cont == 1U && ! (cont_aux == 0))) || ((cont == 1U && cont_aux == 0) && ! (i == 0U))) || (((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || (i == 0U && cont_aux == 0)) || ((i == 0U && cont_aux == 0) && ! (cont == 1U))) || (((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || (i == 0U && cont_aux == 0)) && ! (cont == 1U))) || (cont == 1U && ! (cont_aux == 0))) || ((cont == 1U && cont_aux == 0) && ! (i == 0U))) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || (((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) || ! (cont == 0U)) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 1U))) && ! (cont_aux == 1))) || ((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) || ! (cont == 0U)) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || (((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) || ! (cont == 0U)) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 1))) && ! (cont == 1U))) || ! (cont == 0U)) || ((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (cont_aux == 1))) && cont == 1U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U) && cont_aux == 2) && i == 1U) && j == 2U) && n_caracter == 1U)) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && n_caracter == 0U)) || (((((((((((((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (i == 0U && cont_aux == 0)) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (i == 0U && cont_aux == 0)) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (i == 0U && cont_aux == 0)) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (i == 0U && cont_aux == 0)) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) && ! (cont_aux == 2))) || ! (cont == 0U)) || ((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (cont == 2U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (cont == 2U))) && ! (cont_aux == 2))) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (i == 0U && cont_aux == 0)) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (i == 0U && cont_aux == 0)) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (cont_aux == 2))) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || ((((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (i == 0U && cont_aux == 0)) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U) && ! (cont_aux == 2))) && (((! (cont == 0U) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U)))) && cont == 1U) && cont_aux == 1) && i == 1U) && j == 2U) && n_caracter == 1U)) || ((((((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((((((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (cont_aux == 1)) || (cont_aux == 1 && ! (i == 1U))) || ((cont_aux == 1 && i == 1U) && ! (n_caracter == 1U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 1U))) || ((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (cont_aux == 1)) || (cont_aux == 1 && ! (i == 1U))) || ((cont_aux == 1 && i == 1U) && ! (n_caracter == 1U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 1U))) && ! (cont_aux == 2))) || (cont_aux == 2 && ! (i == 1U))) || ((cont_aux == 2 && i == 1U) && ! (n_caracter == 1U))) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((((((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) && ! (i == 1U))) || (i == 1U && ! (n_caracter == 1U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) && ! (i == 1U))) || (i == 1U && ! (n_caracter == 1U))) && ! (cont_aux == 2))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) && cont_aux == 2) && ! (i == 1U))) || ((cont_aux == 2 && i == 1U) && ! (n_caracter == 1U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 1U))) || ((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) && ! (i == 1U))) || (i == 1U && ! (n_caracter == 1U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 1U))) && ! (cont_aux == 2))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 1U))) && cont_aux == 2) && ! (i == 1U))) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) || (((((((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) && ! (cont_aux == 2))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) && cont_aux == 2)) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 1U))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 1U))) && ! (cont_aux == 2))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 1U))) && cont_aux == 2)) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && cont == 1U) && cont_aux == 1) && ! (i == 1U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && cont == 1U) && cont_aux == 1) && i == 1U) && ! (n_caracter == 1U))) && cont == 2U) && cont_aux == 0) && i == 0U) && j == 2U) && n_caracter == 2U)) || ((((((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 1))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && cont_aux == 1) && ! (i == 1U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 1))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && cont_aux == 1) && ! (i == 1U))) && ! (cont_aux == 2))) || ((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 1))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && cont_aux == 1)) && cont_aux == 2) && ! (i == 1U))) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && ! (i == 1U))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && ! (i == 1U))) && ! (cont_aux == 2))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && cont_aux == 2) && ! (i == 1U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (i == 1U)) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (i == 1U)) && ! (cont_aux == 2))) || (cont_aux == 2 && ! (i == 1U))) && ! (n_caracter == 2U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && ! (i == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (i == 1U)) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) || ! (n_caracter == 2U)) && cont_aux == 2) && ! (i == 1U))) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) || (((((((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && cont_aux == 2)) || ! (n_caracter == 2U)) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) || ! (n_caracter == 2U)) && ! (cont_aux == 2))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) || ! (n_caracter == 2U)) && cont_aux == 2)) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && cont == 1U) && cont_aux == 1) && ! (i == 1U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || (((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (cont_aux == 1)) || (cont_aux == 1 && ! (i == 1U))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (cont_aux == 1)) || (cont_aux == 1 && ! (i == 1U))) && ! (cont_aux == 2))) || (cont_aux == 2 && ! (i == 1U))) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (i == 1U)) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (i == 1U)) && ! (cont_aux == 2))) || (cont_aux == 2 && ! (i == 1U))) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && cont == 1U) && cont_aux == 1) && ! (i == 1U))) && ! (n_caracter == 2U))) && cont == 2U) && cont_aux == 0) && i == 0U) && j == 2U) && n_caracter == 1U)) || (((((((((((((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || (((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U) && ! (cont_aux == 1))) && ((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || ((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U)) && ((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) || (((((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || (((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) && ! (cont == 2U))) || (cont == 2U && ! (cont_aux == 0))) || ((cont == 2U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 2U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && cont == 0U) && cont_aux == 2) && i == 1U) && j == 2U) && n_caracter == 1U)) || (((((((((((((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || (((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U) && ! (cont_aux == 2))) && ((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || (((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U)))) && ! (cont == 1U))) && ! (cont == 2U))) || (cont == 2U && ! (cont_aux == 0))) || ((cont == 2U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 2U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((((((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || (((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || ((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U)) && ((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || (((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U)))) && ! (cont == 1U))) && ! (cont == 2U))) || (cont == 2U && ! (cont_aux == 0))) || ((cont == 2U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 2U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && cont == 0U) && cont_aux == 1) && i == 1U) && j == 2U) && n_caracter == 1U)) || (((((((((((((! (cont == 0U) || (cont == 0U && ! (i == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U))) || ((((((((((! (i == 0U) || (i == 0U && ! (cont == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U))) || (i == 0U && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) || ! (cont == 0U)) || (cont == 0U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((((((! (i == 0U) || (i == 0U && ! (cont == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U))) || (i == 0U && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) || ! (cont == 0U)) || (cont == 0U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 1))) || ((((((((! (i == 0U) || (i == 0U && ! (cont == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U))) || (i == 0U && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) || ! (cont == 0U)) || (cont == 0U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((((((! (i == 0U) || (i == 0U && ! (cont == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U))) || (i == 0U && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) || ! (cont == 0U)) || (cont == 0U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 1))) && ! (cont_aux == 2))) && ((! (cont == 0U) || (cont == 0U && ! (i == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((((((((! (i == 0U) || (i == 0U && ! (cont == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U))) || ! (cont == 0U)) || (cont == 0U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 0U) && i == 0U) && ! (n_caracter == 2U))) || ((((((! (i == 0U) || (i == 0U && ! (cont == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U))) || ! (cont == 0U)) || (cont == 0U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (cont_aux == 2))) && i == 0U) && ! (n_caracter == 2U))) || (((((((! (i == 0U) || (i == 0U && ! (cont == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U))) || ! (cont == 0U)) || (cont == 0U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && ((! (cont == 0U) || (cont == 0U && ! (i == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) || ! (i == 0U)) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (cont_aux == 1)) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (cont_aux == 1)) && ! (cont_aux == 2))) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (cont_aux == 2)) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) && i == 0U) && ! (n_caracter == 2U))) || ((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 1))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 0U) && ! (cont_aux == 2))) || (((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U)) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U)) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && cont == 0U) && ! (cont_aux == 1))) && cont == 2U) && cont_aux == 0) && i == 1U) && j == 2U) && n_caracter == 1U)) || ((((((((((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || (((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U) && ! (cont_aux == 1))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 1))) && cont == 2U) && ! (cont_aux == 2))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U)) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U)) && ! (cont_aux == 2))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && ! (cont == 2U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U) && ! (cont_aux == 2))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) && ! (cont == 2U))) || (cont == 2U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 2U) && i == 0U) && ! (n_caracter == 2U))) || (((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || (((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U) && ! (cont_aux == 1))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 1))) && cont == 2U)) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U)) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) && ! (cont == 2U))) || (cont == 2U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 2U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) || ((((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || (((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U)) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U) && ! (cont_aux == 2))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U)) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U)) && ! (cont_aux == 2))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && ! (cont == 2U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U) && ! (cont_aux == 2))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U)) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U)) && ! (cont == 2U))) || (cont == 2U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 2U) && i == 0U) && ! (n_caracter == 2U))) || (((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U)) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U)) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U)) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U)) && ! (cont == 2U))) || (cont == 2U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 2U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && ! (cont_aux == 1))) || ((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) && ! (cont_aux == 2))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U)) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U)) && ! (cont_aux == 2))) && ! (cont_aux == 1))) && ! (cont == 2U))) && cont == 0U) && cont_aux == 0) && i == 1U) && j == 2U) && n_caracter == 1U) (../plain/vogal-1.i:48:7-48:19)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/vogal-1.i:54:12-54:22)
[Info][Witness] unassume invariant: ((((((((i == 0U && j == 2U) && cont_aux == 0) && cont == 0U) && n_caracter == 2U) || ((((j == 2U && i == 0U) && cont_aux == 0) && cont == 0U) && n_caracter == 1U)) || ((((j == 2U && i == 0U) && cont_aux == 0) && cont == 2U) && n_caracter == 1U)) || ((((j == 2U && i == 0U) && cont_aux == 0) && cont == 2U) && n_caracter == 2U)) || ((((j == 2U && i == 0U) && cont_aux == 0) && cont == 1U) && n_caracter == 1U)) || ((((j == 2U && i == 0U) && cont_aux == 0) && cont == 1U) && n_caracter == 2U) (../plain/vogal-1.i:51:8-51:22)
[Info][Witness] unassume invariant: ((((((((i == 0U && j == 2U) && cont_aux == 0) && cont == 0U) && n_caracter == 2U) || ((((j == 2U && i == 0U) && cont_aux == 0) && cont == 0U) && n_caracter == 1U)) || ((((j == 2U && i == 0U) && cont_aux == 0) && cont == 2U) && n_caracter == 1U)) || ((((j == 2U && i == 0U) && cont_aux == 0) && cont == 2U) && n_caracter == 2U)) || ((((j == 2U && i == 0U) && cont_aux == 0) && cont == 1U) && n_caracter == 1U)) || ((((j == 2U && i == 0U) && cont_aux == 0) && cont == 1U) && n_caracter == 2U) (../plain/vogal-1.i:51:8-51:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/vogal-1.i:56:5-56:8)
[Info][Witness] unassume invariant: ((((((((((((((((((((((((((((((((((i == 1U && j == 2U) && n_caracter == 1U) && cont == 1U) && cont_aux == 1) || ((((i == 1U && n_caracter == 1U) && j == 2U) && cont == 1U) && cont_aux == 2)) || ((((i == 1U && n_caracter == 1U) && j == 2U) && cont == 2U) && cont_aux == 0)) || ((((i == 1U && n_caracter == 1U) && j == 2U) && cont == 2U) && cont_aux == 1)) || ((((i == 1U && n_caracter == 1U) && j == 2U) && cont == 0U) && cont_aux == 1)) || ((((i == 1U && n_caracter == 1U) && j == 2U) && cont == 0U) && cont_aux == 2)) || ((((i == 1U && n_caracter == 1U) && j == 2U) && cont == 0U) && cont_aux == 0)) || (((((i == 1U && n_caracter == 1U) && j == 2U) && ! (cont == 0U)) && cont == 1U) && cont_aux == 0)) || (((((i == 1U && n_caracter == 1U) && j == 2U) && (((! (cont == 0U) || (cont == 0U && ! (cont_aux == 0))) || ((! (cont == 0U) || (cont == 0U && ! (cont_aux == 0))) && ! (cont == 1U))) || (cont == 1U && ! (cont_aux == 0)))) && cont == 2U) && cont_aux == 2)) || ((((i == 0U && cont_aux == 0) && cont == 2U) && j == 2U) && n_caracter == 1U)) || ((((i == 0U && cont_aux == 0) && cont == 0U) && j == 2U) && n_caracter == 2U)) || ((((i == 0U && cont_aux == 0) && cont == 3U) && j == 2U) && n_caracter == 2U)) || ((((i == 0U && cont_aux == 0) && cont == 1U) && j == 2U) && n_caracter == 2U)) || ((((i == 0U && cont_aux == 0) && cont == 0U) && j == 2U) && n_caracter == 1U)) || ((((i == 0U && cont_aux == 0) && cont == 2U) && j == 2U) && n_caracter == 2U)) || (((i == 0U && cont_aux == 0) && cont == 0U) && n_caracter == 0U)) || ((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && cont == 1U) && cont_aux == 0) && i == 0U) && j == 2U) && n_caracter == 1U)) || (((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && j == 2U) && n_caracter == 2U)) || ((((((((((! (i == 0U) || (i == 0U && ! (cont == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U))) || ! (cont == 0U)) || (cont == 0U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 1U) && cont_aux == 0) && i == 1U) && j == 2U) && n_caracter == 1U)) || (((((((((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || (((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) && ! (cont == 1U))) || (cont == 1U && ! (cont_aux == 0))) || ((cont == 1U && cont_aux == 0) && ! (i == 0U))) || (((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || (i == 0U && cont_aux == 0)) || ((i == 0U && cont_aux == 0) && ! (cont == 1U))) || (((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || (i == 0U && cont_aux == 0)) && ! (cont == 1U))) || (cont == 1U && ! (cont_aux == 0))) || ((cont == 1U && cont_aux == 0) && ! (i == 0U))) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || (((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) || ! (cont == 0U)) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 1U))) && cont == 2U) && cont_aux == 1) && i == 1U) && j == 2U) && n_caracter == 1U)) || ((((((((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (i == 0U && cont_aux == 0)) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (i == 0U && cont_aux == 0)) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (i == 0U && cont_aux == 0)) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U) && ! (cont_aux == 1))) && cont == 1U) && cont_aux == 2) && i == 1U) && j == 2U) && n_caracter == 1U)) || (((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && j == 2U) && n_caracter == 1U)) || (((((((((((((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && ! (i == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && i == 1U) && ! (n_caracter == 1U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && ! (i == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && i == 1U) && ! (n_caracter == 1U))) && ! (cont == 2U))) || ((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && ! (i == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && i == 1U) && ! (n_caracter == 1U))) && cont == 2U) && ! (cont_aux == 1))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && cont == 2U) && cont_aux == 1) && ! (i == 1U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && cont == 2U) && cont_aux == 1) && i == 1U) && ! (n_caracter == 1U))) || (((((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && ! (i == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && i == 1U) && ! (n_caracter == 1U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && ! (i == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && i == 1U) && ! (n_caracter == 1U))) && ! (cont == 2U))) || ((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && ! (i == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && i == 1U) && ! (n_caracter == 1U))) && cont == 2U) && ! (cont_aux == 1))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && cont == 2U) && cont_aux == 1) && ! (i == 1U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && cont == 2U) && cont_aux == 1) && i == 1U) && ! (n_caracter == 1U))) && ! (cont_aux == 2))) || (((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && ! (cont == 2U))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && cont == 2U) && ! (cont_aux == 1))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (n_caracter == 1U))) && cont == 2U) && cont_aux == 1)) && cont_aux == 2) && ! (i == 1U))) || (((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (cont == 2U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && cont == 2U) && ! (cont_aux == 1))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && cont == 2U) && cont_aux == 1)) && cont_aux == 2) && i == 1U) && ! (n_caracter == 1U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 1U))) && cont == 1U) && cont_aux == 0) && i == 0U) && j == 2U) && n_caracter == 2U)) || (((((((((((((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || (((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) && ! (cont == 1U))) || (cont == 1U && ! (cont_aux == 0))) || ((cont == 1U && cont_aux == 0) && ! (i == 0U))) || (((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || (i == 0U && cont_aux == 0)) || ((i == 0U && cont_aux == 0) && ! (cont == 1U))) || (((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || (i == 0U && cont_aux == 0)) && ! (cont == 1U))) || (cont == 1U && ! (cont_aux == 0))) || ((cont == 1U && cont_aux == 0) && ! (i == 0U))) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || (((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) || ! (cont == 0U)) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 1U))) || (((((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || (((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) && ! (cont == 1U))) || (cont == 1U && ! (cont_aux == 0))) || ((cont == 1U && cont_aux == 0) && ! (i == 0U))) || (((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || (i == 0U && cont_aux == 0)) || ((i == 0U && cont_aux == 0) && ! (cont == 1U))) || (((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || (i == 0U && cont_aux == 0)) && ! (cont == 1U))) || (cont == 1U && ! (cont_aux == 0))) || ((cont == 1U && cont_aux == 0) && ! (i == 0U))) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || (((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) || ! (cont == 0U)) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 1U))) && ! (cont_aux == 1))) || ((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) || ! (cont == 0U)) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || (((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ((i == 0U && cont_aux == 0) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) || ! (cont == 0U)) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 1))) && ! (cont == 1U))) || ! (cont == 0U)) || ((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (cont_aux == 1))) && cont == 1U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U) && cont_aux == 2) && i == 1U) && j == 2U) && n_caracter == 1U)) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && n_caracter == 0U)) || (((((((((((((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (i == 0U && cont_aux == 0)) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (i == 0U && cont_aux == 0)) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (i == 0U && cont_aux == 0)) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (i == 0U && cont_aux == 0)) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) && ! (cont_aux == 2))) || ! (cont == 0U)) || ((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (cont == 2U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (cont == 2U))) && ! (cont_aux == 2))) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (i == 0U && cont_aux == 0)) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (i == 0U && cont_aux == 0)) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (cont_aux == 2))) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || ((((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (cont == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (i == 0U && cont_aux == 0)) && ! (cont == 0U))) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U) && ! (cont_aux == 2))) && (((! (cont == 0U) || (cont == 0U && ! (cont_aux == 0))) || ((cont == 0U && cont_aux == 0) && ! (i == 0U))) || (((i == 0U && cont_aux == 0) && cont == 0U) && ! (n_caracter == 0U)))) && cont == 1U) && cont_aux == 1) && i == 1U) && j == 2U) && n_caracter == 1U)) || ((((((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((((((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (cont_aux == 1)) || (cont_aux == 1 && ! (i == 1U))) || ((cont_aux == 1 && i == 1U) && ! (n_caracter == 1U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 1U))) || ((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (cont_aux == 1)) || (cont_aux == 1 && ! (i == 1U))) || ((cont_aux == 1 && i == 1U) && ! (n_caracter == 1U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 1U))) && ! (cont_aux == 2))) || (cont_aux == 2 && ! (i == 1U))) || ((cont_aux == 2 && i == 1U) && ! (n_caracter == 1U))) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((((((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) && ! (i == 1U))) || (i == 1U && ! (n_caracter == 1U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) && ! (i == 1U))) || (i == 1U && ! (n_caracter == 1U))) && ! (cont_aux == 2))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) && cont_aux == 2) && ! (i == 1U))) || ((cont_aux == 2 && i == 1U) && ! (n_caracter == 1U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 1U))) || ((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) && ! (i == 1U))) || (i == 1U && ! (n_caracter == 1U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 1U))) && ! (cont_aux == 2))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 1U))) && cont_aux == 2) && ! (i == 1U))) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) || (((((((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) && ! (cont_aux == 2))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) && cont_aux == 2)) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 1U))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 1U))) && ! (cont_aux == 2))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (n_caracter == 1U)) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 1U))) && cont_aux == 2)) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && cont == 1U) && cont_aux == 1) && ! (i == 1U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && cont == 1U) && cont_aux == 1) && i == 1U) && ! (n_caracter == 1U))) && cont == 2U) && cont_aux == 0) && i == 0U) && j == 2U) && n_caracter == 2U)) || ((((((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 1))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && cont_aux == 1) && ! (i == 1U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 1))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && cont_aux == 1) && ! (i == 1U))) && ! (cont_aux == 2))) || ((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 1))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && cont_aux == 1)) && cont_aux == 2) && ! (i == 1U))) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && ! (i == 1U))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && ! (i == 1U))) && ! (cont_aux == 2))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && cont_aux == 2) && ! (i == 1U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (i == 1U)) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (i == 1U)) && ! (cont_aux == 2))) || (cont_aux == 2 && ! (i == 1U))) && ! (n_caracter == 2U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && ! (i == 1U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (i == 1U)) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) || ! (n_caracter == 2U)) && cont_aux == 2) && ! (i == 1U))) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) || (((((((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) && cont_aux == 2)) || ! (n_caracter == 2U)) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) || ! (n_caracter == 2U)) && ! (cont_aux == 2))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && cont == 0U) && ! (n_caracter == 2U))) || ! (n_caracter == 2U)) && cont_aux == 2)) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && cont == 1U) && cont_aux == 1) && ! (i == 1U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || (((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (cont_aux == 1)) || (cont_aux == 1 && ! (i == 1U))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (cont_aux == 1)) || (cont_aux == 1 && ! (i == 1U))) && ! (cont_aux == 2))) || (cont_aux == 2 && ! (i == 1U))) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (i == 1U)) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (i == 1U)) && ! (cont_aux == 2))) || (cont_aux == 2 && ! (i == 1U))) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && cont == 1U) && cont_aux == 1) && ! (i == 1U))) && ! (n_caracter == 2U))) && cont == 2U) && cont_aux == 0) && i == 0U) && j == 2U) && n_caracter == 1U)) || (((((((((((((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || (((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U) && ! (cont_aux == 1))) && ((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || ((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U)) && ((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) || (((((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || (((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) && ! (cont == 2U))) || (cont == 2U && ! (cont_aux == 0))) || ((cont == 2U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 2U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && cont == 0U) && cont_aux == 2) && i == 1U) && j == 2U) && n_caracter == 1U)) || (((((((((((((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || (((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U) && ! (cont_aux == 2))) && ((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || (((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U)))) && ! (cont == 1U))) && ! (cont == 2U))) || (cont == 2U && ! (cont_aux == 0))) || ((cont == 2U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 2U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((((((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || (((((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) || ((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || ((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U)) && ((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || (((((((! (i == 0U) || (i == 0U && ! (cont_aux == 0))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U))) || ! (cont_aux == 0)) || (cont_aux == 0 && ! (i == 0U))) || (((! (n_caracter == 0U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ((! (cont_aux == 0) || (cont_aux == 0 && ! (i == 0U))) || ((i == 0U && cont_aux == 0) && ! (n_caracter == 0U)))) && ! (cont == 1U))) && ! (cont == 2U))) || (cont == 2U && ! (cont_aux == 0))) || ((cont == 2U && cont_aux == 0) && ! (i == 0U))) || ((((! (n_caracter == 0U) && cont == 2U) && cont_aux == 0) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && cont == 0U) && cont_aux == 1) && i == 1U) && j == 2U) && n_caracter == 1U)) || (((((((((((((! (cont == 0U) || (cont == 0U && ! (i == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U))) || ((((((((((! (i == 0U) || (i == 0U && ! (cont == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U))) || (i == 0U && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) || ! (cont == 0U)) || (cont == 0U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((((((! (i == 0U) || (i == 0U && ! (cont == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U))) || (i == 0U && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) || ! (cont == 0U)) || (cont == 0U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 1))) || ((((((((! (i == 0U) || (i == 0U && ! (cont == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U))) || (i == 0U && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) || ! (cont == 0U)) || (cont == 0U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((((((! (i == 0U) || (i == 0U && ! (cont == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U))) || (i == 0U && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))))) || ! (cont == 0U)) || (cont == 0U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 1))) && ! (cont_aux == 2))) && ((! (cont == 0U) || (cont == 0U && ! (i == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((((((((! (i == 0U) || (i == 0U && ! (cont == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U))) || ! (cont == 0U)) || (cont == 0U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 0U) && i == 0U) && ! (n_caracter == 2U))) || ((((((! (i == 0U) || (i == 0U && ! (cont == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U))) || ! (cont == 0U)) || (cont == 0U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) || ((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && ! (cont_aux == 2))) && i == 0U) && ! (n_caracter == 2U))) || (((((((! (i == 0U) || (i == 0U && ! (cont == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U))) || ! (cont == 0U)) || (cont == 0U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && ((! (cont == 0U) || (cont == 0U && ! (i == 0U))) || ((i == 0U && cont == 0U) && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) || ! (i == 0U)) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (cont_aux == 1)) || (((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (cont_aux == 1)) && ! (cont_aux == 2))) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U))) || ! (cont_aux == 2)) && (! (cont == 0U) || (cont == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) && i == 0U) && ! (n_caracter == 2U))) || ((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 1))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 0U) && ! (cont_aux == 2))) || (((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U)) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U)) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && cont == 0U) && ! (cont_aux == 1))) && cont == 2U) && cont_aux == 0) && i == 1U) && j == 2U) && n_caracter == 1U)) || ((((((((((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || (((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U) && ! (cont_aux == 1))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 1))) && cont == 2U) && ! (cont_aux == 2))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U)) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U)) && ! (cont_aux == 2))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && ! (cont == 2U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U) && ! (cont_aux == 2))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) && ! (cont == 2U))) || (cont == 2U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 2U) && i == 0U) && ! (n_caracter == 2U))) || (((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || (((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U) && ! (cont_aux == 1))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 1))) && cont == 2U)) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U)) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) && ! (cont == 2U))) || (cont == 2U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 2U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) || ((((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || (((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U)) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U) && ! (cont_aux == 2))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U)) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U)) && ! (cont_aux == 2))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && ! (cont == 2U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U) && ! (cont_aux == 2))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U)) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U)) && ! (cont == 2U))) || (cont == 2U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 2U) && i == 0U) && ! (n_caracter == 2U))) || (((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U)) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && cont == 2U)) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U)) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U)) && ! (cont == 2U))) || (cont == 2U && ! (i == 0U))) || (((! (n_caracter == 0U) && cont == 2U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && ! (cont_aux == 1))) || ((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U) && ! (cont_aux == 1))) && ! (cont_aux == 2))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || (((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) || (((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && ! (cont_aux == 2))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U)) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && ! (cont == 1U))) || ((((! (i == 0U) || (i == 0U && ! (n_caracter == 0U))) || ((! (n_caracter == 0U) && i == 0U) && ! (n_caracter == 2U))) && (! (i == 0U) || (i == 0U && ! (n_caracter == 0U)))) && cont == 1U)) && ! (cont_aux == 2))) && ! (cont_aux == 1))) && ! (cont == 2U))) && cont == 0U) && cont_aux == 0) && i == 1U) && j == 2U) && n_caracter == 1U) (../plain/vogal-1.i:56:5-56:8)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (../plain/vogal-1.i:15:1-17:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 28
  dead: 2 (2 in uncalled functions)
  total lines: 30
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (../plain/vogal-1.i:12:73-12:74)
[Error][Witness] invariant refuted: (i == (1U) || (!(i == (1U)) && i == (0U)) || (!(i == (1U)) && !(i == (0U)) && i == (3U)) || (!(i == (1U)) && !(i == (0U)) && !(i == (3U)) && i == (2U)) || (!(i == (1U)) && !(i == (0U)) && !(i == (3U)) && !(i == (2U)) && i == (4U))) && (i == (3U) || (!(i == (3U)) && i == (4U)) || (!(i == (3U)) && !(i == (4U)) && i == (5U)) || (!(i == (3U)) && !(i == (4U)) && !(i == (5U)) && i == (2U)) || (!(i == (3U)) && !(i == (4U)) && !(i == (5U)) && !(i == (2U)) && i == (0U)) || (!(i == (3U)) && !(i == (4U)) && !(i == (5U)) && !(i == (2U)) && !(i == (0U)) && i == (1U))) (../plain/vogal-1.i:34:5)

runtime: 00:00:10.147
vars: 72, evals: 229

|rho|=73
|called|=0
|stable|=73
|infl|=69
|wpoint|=1
|side_dep|=19
|side_infl|=33
|var_messages|=14
|rho_write|=26
|dep|=52
Found 4 contexts for 4 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_assert (2023) on ../plain/vogal-1.i:18:1-23:1
1	contexts for entry state of reach_error (2015) on ../plain/vogal-1.i:12:1-12:160
1	contexts for entry state of main (2027) on ../plain/vogal-1.i:28:1-61:1
1	contexts for entry state of __VERIFIER_nondet_char (317) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:20:62-20:116

Memory statistics: total=2158.59MB, max=32.90MB, minor=2154.80MB, major=98.18MB, promoted=94.39MB
    minor collections=1035  major collections=16 compactions=0

[Warning][Witness] invariant unconfirmed: (i == (1U) && j == (2U) && n_caracter == (1U) && cont == (1U) && cont_aux == (1)) || (i == (1U) && n_caracter == (1U) && j == (2U) && cont == (1U) && cont_aux == (2)) || (i == (1U) && n_caracter == (1U) && j == (2U) && cont == (2U) && cont_aux == (0)) || (i == (1U) && n_caracter == (1U) && j == (2U) && cont == (2U) && cont_aux == (1)) || (i == (1U) && n_caracter == (1U) && j == (2U) && cont == (0U) && cont_aux == (1)) || (i == (1U) && n_caracter == (1U) && j == (2U) && cont == (0U) && cont_aux == (2)) || (i == (1U) && n_caracter == (1U) && j == (2U) && cont == (0U) && cont_aux == (0)) || (i == (1U) && n_caracter == (1U) && j == (2U) && !(cont == (0U)) && cont == (1U) && cont_aux == (0)) || (i == (1U) && n_caracter == (1U) && j == (2U) && (!(cont == (0U)) || (cont == (0U) && !(cont_aux == (0))) || ((!(cont == (0U)) || (cont == (0U) && !(cont_aux == (0)))) && !(cont == (1U))) || (cont == (1U) && !(cont_aux == (0)))) && cont == (2U) && cont_aux == (2)) || (i == (0U) && cont_aux == (0) && cont == (2U) && j == (2U) && n_caracter == (1U)) || (i == (0U) && cont_aux == (0) && cont == (0U) && j == (2U) && n_caracter == (2U)) || (i == (0U) && cont_aux == (0) && cont == (3U) && j == (2U) && n_caracter == (2U)) || (i == (0U) && cont_aux == (0) && cont == (1U) && j == (2U) && n_caracter == (2U)) || (i == (0U) && cont_aux == (0) && cont == (0U) && j == (2U) && n_caracter == (1U)) || (i == (0U) && cont_aux == (0) && cont == (2U) && j == (2U) && n_caracter == (2U)) || (i == (0U) && cont_aux == (0) && cont == (0U) && n_caracter == (0U)) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && cont == (1U) && cont_aux == (0) && i == (0U) && j == (2U) && n_caracter == (1U)) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && j == (2U) && n_caracter == (2U)) || ((!(i == (0U)) || (i == (0U) && !(cont == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U))) || !(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && i == (0U) && !(n_caracter == (2U)))) && cont == (1U) && cont_aux == (0) && i == (1U) && j == (2U) && n_caracter == (1U)) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || (i == (0U) && cont_aux == (0) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || (i == (0U) && cont_aux == (0) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))))) && !(cont == (1U))) || (cont == (1U) && !(cont_aux == (0))) || (cont == (1U) && cont_aux == (0) && !(i == (0U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0)) || (i == (0U) && cont_aux == (0) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0))) && !(cont == (1U))) || (cont == (1U) && !(cont_aux == (0))) || (cont == (1U) && cont_aux == (0) && !(i == (0U)))) && !(cont == (0U))) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || (i == (0U) && cont_aux == (0) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))))) || !(cont == (0U)) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (1U)))) && cont == (2U) && cont_aux == (1) && i == (1U) && j == (2U) && n_caracter == (1U)) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0))) && !(cont == (0U))) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0))) && !(cont == (0U))) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0))) && !(cont == (0U))) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && cont == (2U) && !(cont_aux == (1)))) && cont == (1U) && cont_aux == (2) && i == (1U) && j == (2U) && n_caracter == (1U)) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && j == (2U) && n_caracter == (1U)) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(n_caracter == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(n_caracter == (1U)))) && !(i == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && i == (1U) && !(n_caracter == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(n_caracter == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(n_caracter == (1U)))) && !(i == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && i == (1U) && !(n_caracter == (1U)))) && !(cont == (2U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(n_caracter == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(n_caracter == (1U)))) && !(i == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && i == (1U) && !(n_caracter == (1U)))) && cont == (2U) && !(cont_aux == (1))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(n_caracter == (1U)))) && cont == (2U) && cont_aux == (1) && !(i == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && cont == (2U) && cont_aux == (1) && i == (1U) && !(n_caracter == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(n_caracter == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(n_caracter == (1U)))) && !(i == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && i == (1U) && !(n_caracter == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(n_caracter == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(n_caracter == (1U)))) && !(i == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && i == (1U) && !(n_caracter == (1U)))) && !(cont == (2U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(n_caracter == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(n_caracter == (1U)))) && !(i == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && i == (1U) && !(n_caracter == (1U)))) && cont == (2U) && !(cont_aux == (1))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(n_caracter == (1U)))) && cont == (2U) && cont_aux == (1) && !(i == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && cont == (2U) && cont_aux == (1) && i == (1U) && !(n_caracter == (1U)))) && !(cont_aux == (2))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(n_caracter == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(n_caracter == (1U)))) && !(cont == (2U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(n_caracter == (1U)))) && cont == (2U) && !(cont_aux == (1))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(n_caracter == (1U)))) && cont == (2U) && cont_aux == (1))) && cont_aux == (2) && !(i == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(cont == (2U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && cont == (2U) && !(cont_aux == (1))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && cont == (2U) && cont_aux == (1))) && cont_aux == (2) && i == (1U) && !(n_caracter == (1U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (1U)))) && cont == (1U) && cont_aux == (0) && i == (0U) && j == (2U) && n_caracter == (2U)) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || (i == (0U) && cont_aux == (0) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || (i == (0U) && cont_aux == (0) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))))) && !(cont == (1U))) || (cont == (1U) && !(cont_aux == (0))) || (cont == (1U) && cont_aux == (0) && !(i == (0U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0)) || (i == (0U) && cont_aux == (0) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0))) && !(cont == (1U))) || (cont == (1U) && !(cont_aux == (0))) || (cont == (1U) && cont_aux == (0) && !(i == (0U)))) && !(cont == (0U))) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || (i == (0U) && cont_aux == (0) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))))) || !(cont == (0U)) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || (i == (0U) && cont_aux == (0) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || (i == (0U) && cont_aux == (0) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))))) && !(cont == (1U))) || (cont == (1U) && !(cont_aux == (0))) || (cont == (1U) && cont_aux == (0) && !(i == (0U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0)) || (i == (0U) && cont_aux == (0) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0))) && !(cont == (1U))) || (cont == (1U) && !(cont_aux == (0))) || (cont == (1U) && cont_aux == (0) && !(i == (0U)))) && !(cont == (0U))) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || (i == (0U) && cont_aux == (0) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))))) || !(cont == (0U)) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (1U)))) && !(cont_aux == (1))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || (i == (0U) && cont_aux == (0) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))))) || !(cont == (0U)) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || (i == (0U) && cont_aux == (0) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))))) || !(cont == (0U)) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (1)))) && !(cont == (1U))) || !(cont == (0U)) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(cont_aux == (1)))) && cont == (1U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && cont == (2U) && cont_aux == (2) && i == (1U) && j == (2U) && n_caracter == (1U)) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && n_caracter == (0U)) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0))) && !(cont == (0U))) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0))) && !(cont == (0U))) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0))) && !(cont == (0U))) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0))) && !(cont == (0U))) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (2U)))) && !(cont_aux == (2))) || !(cont == (0U)) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(cont == (2U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(cont == (2U)))) && !(cont_aux == (2)))) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0))) && !(cont == (0U))) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0))) && !(cont == (0U))) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (2))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(cont_aux == (2)))) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(cont == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0))) && !(cont == (0U))) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && cont == (2U) && !(cont_aux == (2)))) && (!(cont == (0U)) || (cont == (0U) && !(cont_aux == (0))) || (cont == (0U) && cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && cont == (0U) && !(n_caracter == (0U)))) && cont == (1U) && cont_aux == (1) && i == (1U) && j == (2U) && n_caracter == (1U)) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(cont_aux == (1)) || (cont_aux == (1) && !(i == (1U))) || (cont_aux == (1) && i == (1U) && !(n_caracter == (1U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(cont_aux == (1)) || (cont_aux == (1) && !(i == (1U))) || (cont_aux == (1) && i == (1U) && !(n_caracter == (1U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (1U)))) && !(cont_aux == (2))) || (cont_aux == (2) && !(i == (1U))) || (cont_aux == (2) && i == (1U) && !(n_caracter == (1U)))) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(n_caracter == (1U)) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(n_caracter == (1U))) && !(i == (1U))) || (i == (1U) && !(n_caracter == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(n_caracter == (1U)) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(n_caracter == (1U))) && !(i == (1U))) || (i == (1U) && !(n_caracter == (1U)))) && !(cont_aux == (2))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(n_caracter == (1U))) && cont_aux == (2) && !(i == (1U))) || (cont_aux == (2) && i == (1U) && !(n_caracter == (1U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(n_caracter == (1U)) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(n_caracter == (1U))) && !(i == (1U))) || (i == (1U) && !(n_caracter == (1U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (1U)))) && !(cont_aux == (2))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(n_caracter == (1U)) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (1U)))) && cont_aux == (2) && !(i == (1U)))) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && cont == (1U) && !(cont_aux == (1))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(n_caracter == (1U)) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(n_caracter == (1U))) && !(cont_aux == (2))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(n_caracter == (1U))) && cont_aux == (2)) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(n_caracter == (1U)) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (1U)))) && !(cont_aux == (2))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(n_caracter == (1U)) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (1U)))) && cont_aux == (2))) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && cont == (1U) && cont_aux == (1) && !(i == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && cont == (1U) && cont_aux == (1) && i == (1U) && !(n_caracter == (1U)))) && cont == (2U) && cont_aux == (0) && i == (0U) && j == (2U) && n_caracter == (2U)) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (1))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U)))) && cont_aux == (1) && !(i == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (1))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U)))) && cont_aux == (1) && !(i == (1U)))) && !(cont_aux == (2))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (1))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U)))) && cont_aux == (1))) && cont_aux == (2) && !(i == (1U)))) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U)))) && !(i == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U)))) && !(i == (1U)))) && !(cont_aux == (2))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U)))) && cont_aux == (2) && !(i == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(i == (1U)) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(i == (1U))) && !(cont_aux == (2))) || (cont_aux == (2) && !(i == (1U)))) && !(n_caracter == (2U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U)))) && !(i == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(i == (1U))) && !(n_caracter == (2U)))) && !(cont_aux == (2))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U))) || !(n_caracter == (2U))) && cont_aux == (2) && !(i == (1U)))) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && cont == (1U) && !(cont_aux == (1))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (2))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U)))) && cont_aux == (2)) || !(n_caracter == (2U)) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U))) || !(n_caracter == (2U))) && !(cont_aux == (2))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && !(n_caracter == (2U))) || !(n_caracter == (2U))) && cont_aux == (2))) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && cont == (1U) && cont_aux == (1) && !(i == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(cont_aux == (1)) || (cont_aux == (1) && !(i == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(cont_aux == (1)) || (cont_aux == (1) && !(i == (1U)))) && !(cont_aux == (2))) || (cont_aux == (2) && !(i == (1U)))) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(i == (1U)) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(i == (1U))) && !(cont_aux == (2))) || (cont_aux == (2) && !(i == (1U)))) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && cont == (1U) && !(cont_aux == (1))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && cont == (1U) && cont_aux == (1) && !(i == (1U)))) && !(n_caracter == (2U)))) && cont == (2U) && cont_aux == (0) && i == (0U) && j == (2U) && n_caracter == (1U)) || ((!(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && cont == (2U) && !(cont_aux == (1)))) && (!(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && cont == (2U))) && (!(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U)))) && cont == (1U) && !(cont_aux == (1))) || ((!(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && (!(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && (!(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U)))) && cont == (1U) && !(cont_aux == (1)))) && !(cont == (2U))) || (cont == (2U) && !(cont_aux == (0))) || (cont == (2U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (2U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && cont == (0U) && cont_aux == (2) && i == (1U) && j == (2U) && n_caracter == (1U)) || ((!(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && cont == (2U) && !(cont_aux == (2)))) && (!(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && (!(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U)))) && !(cont == (1U)))) && !(cont == (2U))) || (cont == (2U) && !(cont_aux == (0))) || (cont == (2U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (2U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U))) || ((!(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && cont == (2U))) && (!(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(cont_aux == (0))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U))) || !(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && (!(cont_aux == (0)) || (cont_aux == (0) && !(i == (0U))) || (i == (0U) && cont_aux == (0) && !(n_caracter == (0U)))) && !(cont == (1U)))) && !(cont == (2U))) || (cont == (2U) && !(cont_aux == (0))) || (cont == (2U) && cont_aux == (0) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (2U) && cont_aux == (0) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (2)))) && cont == (0U) && cont_aux == (1) && i == (1U) && j == (2U) && n_caracter == (1U)) || ((!(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(cont == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U))) || (i == (0U) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))))) || !(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U))) || (i == (0U) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))))) || !(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (1))) || ((!(i == (0U)) || (i == (0U) && !(cont == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U))) || (i == (0U) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))))) || !(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U))) || (i == (0U) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))))) || !(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (1)))) && !(cont_aux == (2)))) && (!(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(cont == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U))) || !(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U))) || !(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (2))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(cont_aux == (2)))) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(cont == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U))) || !(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (0U) && i == (0U) && !(n_caracter == (2U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (2)))) && (!(cont == (0U)) || (cont == (0U) && !(i == (0U))) || (i == (0U) && cont == (0U) && !(n_caracter == (0U)))) && cont == (1U) && !(cont_aux == (1))) || !(i == (0U)) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(cont_aux == (1)) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(cont_aux == (1))) && !(cont_aux == (2)))) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U))) || !(cont_aux == (2))) && (!(cont == (0U)) || (cont == (0U) && !(n_caracter == (0U)))) && cont == (1U) && !(cont_aux == (1)))) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (1)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && cont == (1U) && !(cont_aux == (1))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && cont == (0U) && !(cont_aux == (2))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (2)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (2)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && cont == (1U)) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && cont == (1U)) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (2)))) && cont == (0U) && !(cont_aux == (1)))) && cont == (2U) && cont_aux == (0) && i == (1U) && j == (2U) && n_caracter == (1U)) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && cont == (2U) && !(cont_aux == (1))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (1)))) && cont == (2U) && !(cont_aux == (2)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && cont == (2U)) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && cont == (2U))) && !(cont_aux == (2))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (2)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && cont == (2U) && !(cont_aux == (2)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && cont == (1U) && !(cont_aux == (1))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (2)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && cont == (1U) && !(cont_aux == (1)))) && !(cont == (2U))) || (cont == (2U) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (2U) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && cont == (2U) && !(cont_aux == (1))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (1)))) && cont == (2U))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && cont == (2U))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && cont == (1U) && !(cont_aux == (1))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && cont == (1U) && !(cont_aux == (1)))) && !(cont == (2U))) || (cont == (2U) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (2U) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (2))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && cont == (2U)) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && cont == (2U) && !(cont_aux == (2)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && cont == (2U)) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && cont == (2U))) && !(cont_aux == (2))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (2)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && cont == (2U) && !(cont_aux == (2)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && cont == (1U)) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (2)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && cont == (1U))) && !(cont == (2U))) || (cont == (2U) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (2U) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && cont == (2U))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && cont == (2U))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && cont == (1U)) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && cont == (1U))) && !(cont == (2U))) || (cont == (2U) && !(i == (0U))) || (!(n_caracter == (0U)) && cont == (2U) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (2)))) && !(cont_aux == (1))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (2)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && cont == (1U) && !(cont_aux == (1))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && cont == (1U) && !(cont_aux == (1)))) && !(cont_aux == (2))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && !(cont_aux == (2)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && cont == (1U)) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && !(cont == (1U))) || ((!(i == (0U)) || (i == (0U) && !(n_caracter == (0U))) || (!(n_caracter == (0U)) && i == (0U) && !(n_caracter == (2U)))) && (!(i == (0U)) || (i == (0U) && !(n_caracter == (0U)))) && cont == (1U))) && !(cont_aux == (2)))) && !(cont_aux == (1)))) && !(cont == (2U)))) && cont == (0U) && cont_aux == (0) && i == (1U) && j == (2U) && n_caracter == (1U)) (../plain/vogal-1.i:49:3)
[Warning][Witness] invariant unconfirmed: (i == (0U) && j == (2U) && cont_aux == (0) && cont == (0U) && n_caracter == (2U)) || (j == (2U) && i == (0U) && cont_aux == (0) && cont == (0U) && n_caracter == (1U)) || (j == (2U) && i == (0U) && cont_aux == (0) && cont == (2U) && n_caracter == (1U)) || (j == (2U) && i == (0U) && cont_aux == (0) && cont == (2U) && n_caracter == (2U)) || (j == (2U) && i == (0U) && cont_aux == (0) && cont == (1U) && n_caracter == (1U)) || (j == (2U) && i == (0U) && cont_aux == (0) && cont == (1U) && n_caracter == (2U)) (../plain/vogal-1.i:51:5)
[Warning][Witness] invariant unconfirmed: (i == (5U) && n_caracter == (0U)) || (i == (5U) && !(n_caracter == (0U)) && n_caracter == (2U)) || (i == (5U) && !(n_caracter == (0U)) && n_caracter == (3U)) || (i == (5U) && !(n_caracter == (0U)) && n_caracter == (1U)) || (i == (5U) && !(n_caracter == (0U)) && n_caracter == (4U)) (../plain/vogal-1.i:38:3)
[Warning][Witness] invariant unconfirmed: (cont == (2U) && i == (1U) && j == (2U) && n_caracter == (3U)) || (cont == (0U) && i == (1U) && j == (2U) && n_caracter == (2U)) || (cont == (0U) && i == (0U) && n_caracter == (2U)) || (cont == (1U) && i == (1U) && j == (2U) && n_caracter == (4U)) || (cont == (0U) && i == (2U) && j == (2U) && n_caracter == (4U)) || (cont == (2U) && i == (1U) && j == (2U) && n_caracter == (2U)) || (cont == (1U) && i == (2U) && j == (2U) && n_caracter == (3U)) || (cont == (1U) && i == (1U) && j == (2U) && n_caracter == (2U)) || (cont == (0U) && i == (0U) && n_caracter == (4U)) || (cont == (1U) && i == (1U) && j == (2U) && n_caracter == (3U)) || (cont == (0U) && i == (1U) && j == (2U) && n_caracter == (4U)) || (cont == (0U) && i == (2U) && j == (2U) && n_caracter == (3U)) || (cont == (2U) && i == (1U) && j == (2U) && n_caracter == (4U)) || (cont == (0U) && i == (1U) && j == (2U) && n_caracter == (3U)) || (cont == (2U) && i == (2U) && j == (2U) && n_caracter == (3U)) || (cont == (0U) && i == (0U) && n_caracter == (1U)) || (cont == (0U) && i == (0U) && n_caracter == (3U)) (../plain/vogal-1.i:43:6)
[Warning][Witness] invariant unconfirmed: (cont == (0U) && i == (5U) && n_caracter == (0U)) || (cont == (0U) && i == (5U) && !(n_caracter == (0U)) && n_caracter == (2U)) || (i == (5U) && !(n_caracter == (0U)) && cont == (0U) && n_caracter == (3U)) || (i == (5U) && !(n_caracter == (0U)) && cont == (0U) && n_caracter == (1U)) || (i == (5U) && !(n_caracter == (0U)) && cont == (0U) && n_caracter == (4U)) (../plain/vogal-1.i:41:3)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 5
  refuted: 1
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 7
SV-COMP result: false

vars = 72    evals = 229    narrow_reuses = 15

Timings:
                                  cputime   walltime   allocated   count
Default                           16.357s    16.372s   2359.82MB      1×
  preprocess                         0.026s     0.025s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.20MB      4×
  Cabs2cil                           0.006s     0.006s      4.87MB      4×
  mergeCIL                           0.003s     0.003s      3.36MB      1×
  analysis                          16.314s    16.329s   2342.35MB      1×
    createCFG                          0.001s     0.001s      0.70MB      1×
      handle                             0.001s     0.001s      0.12MB     34×
      iter_connect                       0.001s     0.001s      0.46MB     34×
        computeSCCs                        0.001s     0.001s      0.27MB     35×
    FrontC                             0.026s     0.026s     21.22MB     12×
    Cabs2cil                           0.015s     0.015s     16.20MB     12×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            6.291s     6.305s   1925.18MB      1×
      S.Dom.equal                        0.001s     0.001s      0.09MB    244×
      base unassume                      0.775s     0.776s    903.79MB     85×
      cheap_full_reach                   0.001s     0.001s      0.03MB      1×
      postsolver                         0.052s     0.052s     40.28MB      1×
        postsolver_iter                    0.052s     0.052s     40.21MB      1×
    warn_global                        0.001s     0.001s      0.21MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
