/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 ukojak/sum04-2.yml.witness.yml --witness.yaml.validate ukojak/sum04-2.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/sum04-2.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: (i <= (6) && (5) < i && (10) <= sn && sn <= (10)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (3) < i && i <= (4) && (6) <= sn && sn <= (6)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && sn <= (16) && (8) < i && (15) < sn) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (4) < i && sn <= (8) && (8) <= sn && i <= (5)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && sn <= (2) && i <= (2) && (2) <= sn && (2) <= i) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && i == (1) && sn == (0)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (12) <= sn && (6) < i && sn <= (12) && i <= (7)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (!((12) <= sn) || ((12) <= sn && !((6) < i)) || ((12) <= sn && (6) < i && !(sn <= (12))) || ((12) <= sn && (6) < i && sn <= (12) && !(i <= (7)))) && sn <= (14) && (7) < i && i <= (8) && (14) <= sn) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (!((12) <= sn) || ((12) <= sn && !((6) < i)) || ((12) <= sn && (6) < i && !(sn <= (12))) || ((12) <= sn && (6) < i && sn <= (12) && !(i <= (7)))) && (!(sn <= (14)) || (sn <= (14) && !((7) < i)) || (sn <= (14) && (7) < i && !(i <= (8))) || (sn <= (14) && (7) < i && i <= (8) && !((14) <= sn))) && sn <= (4) && i <= (3) && (4) <= sn && (2) < i) (../plain/sum04-2.i:25:5)
[Info][Witness] unassume invariant: ((((((((((((((((i <= 6 && 5 < i) && 10 <= sn) && sn <= 10) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && 3 < i) && i <= 4) && 6 <= sn) && sn <= 6)) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && sn <= 16) && 8 < i) && 15 < sn)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && 4 < i) && sn <= 8) && 8 <= sn) && i <= 5)) || ((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && sn <= 2) && i <= 2) && 2 <= sn) && 2 <= i)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && i == 1) && sn == 0)) || ((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && 12 <= sn) && 6 < i) && sn <= 12) && i <= 7)) || (((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && sn <= 14) && 7 < i) && i <= 8) && 14 <= sn)) || ((((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && (((! (sn <= 14) || (sn <= 14 && ! (7 < i))) || ((sn <= 14 && 7 < i) && ! (i <= 8))) || (((sn <= 14 && 7 < i) && i <= 8) && ! (14 <= sn)))) && sn <= 4) && i <= 3) && 4 <= sn) && 2 < i)) && (((((((((((i <= 6 && 5 < i) && 10 <= sn) && sn <= 10) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && 3 < i) && i <= 4) && 6 <= sn) && sn <= 6)) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && sn <= 16) && 8 < i) && 15 < sn)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && 4 < i) && sn <= 8) && 8 <= sn) && i <= 5)) || ((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && sn <= 2) && i <= 2) && 2 <= sn) && 2 <= i)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && i == 1) && sn == 0)) || ((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && 12 <= sn) && 6 < i) && sn <= 12) && i <= 7)) || (((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && sn <= 14) && 7 < i) && i <= 8) && 14 <= sn)) || ((((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && (((! (sn <= 14) || (sn <= 14 && ! (7 < i))) || ((sn <= 14 && 7 < i) && ! (i <= 8))) || (((sn <= 14 && 7 < i) && i <= 8) && ! (14 <= sn)))) && sn <= 4) && i <= 3) && 4 <= sn) && 2 < i))) && (((((((((((i <= 6 && 5 < i) && 10 <= sn) && sn <= 10) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && 3 < i) && i <= 4) && 6 <= sn) && sn <= 6)) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && sn <= 16) && 8 < i) && 15 < sn)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && 4 < i) && sn <= 8) && 8 <= sn) && i <= 5)) || ((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && sn <= 2) && i <= 2) && 2 <= sn) && 2 <= i)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && i == 1) && sn == 0)) || ((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && 12 <= sn) && 6 < i) && sn <= 12) && i <= 7)) || (((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && sn <= 14) && 7 < i) && i <= 8) && 14 <= sn)) || ((((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && (((! (sn <= 14) || (sn <= 14 && ! (7 < i))) || ((sn <= 14 && 7 < i) && ! (i <= 8))) || (((sn <= 14 && 7 < i) && i <= 8) && ! (14 <= sn)))) && sn <= 4) && i <= 3) && 4 <= sn) && 2 < i))) && (((((((((((i <= 6 && 5 < i) && 10 <= sn) && sn <= 10) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && 3 < i) && i <= 4) && 6 <= sn) && sn <= 6)) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && sn <= 16) && 8 < i) && 15 < sn)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && 4 < i) && sn <= 8) && 8 <= sn) && i <= 5)) || ((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && sn <= 2) && i <= 2) && 2 <= sn) && 2 <= i)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && i == 1) && sn == 0)) || ((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && 12 <= sn) && 6 < i) && sn <= 12) && i <= 7)) || (((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && sn <= 14) && 7 < i) && i <= 8) && 14 <= sn)) || ((((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && (((! (sn <= 14) || (sn <= 14 && ! (7 < i))) || ((sn <= 14 && 7 < i) && ! (i <= 8))) || (((sn <= 14 && 7 < i) && i <= 8) && ! (14 <= sn)))) && sn <= 4) && i <= 3) && 4 <= sn) && 2 < i))) && (((((((((((i <= 6 && 5 < i) && 10 <= sn) && sn <= 10) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && 3 < i) && i <= 4) && 6 <= sn) && sn <= 6)) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && sn <= 16) && 8 < i) && 15 < sn)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && 4 < i) && sn <= 8) && 8 <= sn) && i <= 5)) || ((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && sn <= 2) && i <= 2) && 2 <= sn) && 2 <= i)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && i == 1) && sn == 0)) || ((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && 12 <= sn) && 6 < i) && sn <= 12) && i <= 7)) || (((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && sn <= 14) && 7 < i) && i <= 8) && 14 <= sn)) || ((((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && (((! (sn <= 14) || (sn <= 14 && ! (7 < i))) || ((sn <= 14 && 7 < i) && ! (i <= 8))) || (((sn <= 14 && 7 < i) && i <= 8) && ! (14 <= sn)))) && sn <= 4) && i <= 3) && 4 <= sn) && 2 < i))) && (((((((((((i <= 6 && 5 < i) && 10 <= sn) && sn <= 10) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && 3 < i) && i <= 4) && 6 <= sn) && sn <= 6)) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && sn <= 16) && 8 < i) && 15 < sn)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && 4 < i) && sn <= 8) && 8 <= sn) && i <= 5)) || ((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && sn <= 2) && i <= 2) && 2 <= sn) && 2 <= i)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && i == 1) && sn == 0)) || ((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && 12 <= sn) && 6 < i) && sn <= 12) && i <= 7)) || (((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && sn <= 14) && 7 < i) && i <= 8) && 14 <= sn)) || ((((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && (((! (sn <= 14) || (sn <= 14 && ! (7 < i))) || ((sn <= 14 && 7 < i) && ! (i <= 8))) || (((sn <= 14 && 7 < i) && i <= 8) && ! (14 <= sn)))) && sn <= 4) && i <= 3) && 4 <= sn) && 2 < i))) && (((((((((((i <= 6 && 5 < i) && 10 <= sn) && sn <= 10) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && 3 < i) && i <= 4) && 6 <= sn) && sn <= 6)) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && sn <= 16) && 8 < i) && 15 < sn)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && 4 < i) && sn <= 8) && 8 <= sn) && i <= 5)) || ((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && sn <= 2) && i <= 2) && 2 <= sn) && 2 <= i)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && i == 1) && sn == 0)) || ((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && 12 <= sn) && 6 < i) && sn <= 12) && i <= 7)) || (((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && sn <= 14) && 7 < i) && i <= 8) && 14 <= sn)) || ((((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && (((! (sn <= 14) || (sn <= 14 && ! (7 < i))) || ((sn <= 14 && 7 < i) && ! (i <= 8))) || (((sn <= 14 && 7 < i) && i <= 8) && ! (14 <= sn)))) && sn <= 4) && i <= 3) && 4 <= sn) && 2 < i)) (../plain/sum04-2.i:24:6-24:21)
[Info][Witness] unassume invariant: ((((((((((((((((i <= 6 && 5 < i) && 10 <= sn) && sn <= 10) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && 3 < i) && i <= 4) && 6 <= sn) && sn <= 6)) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && sn <= 16) && 8 < i) && 15 < sn)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && 4 < i) && sn <= 8) && 8 <= sn) && i <= 5)) || ((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && sn <= 2) && i <= 2) && 2 <= sn) && 2 <= i)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && i == 1) && sn == 0)) || ((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && 12 <= sn) && 6 < i) && sn <= 12) && i <= 7)) || (((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && sn <= 14) && 7 < i) && i <= 8) && 14 <= sn)) || ((((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && (((! (sn <= 14) || (sn <= 14 && ! (7 < i))) || ((sn <= 14 && 7 < i) && ! (i <= 8))) || (((sn <= 14 && 7 < i) && i <= 8) && ! (14 <= sn)))) && sn <= 4) && i <= 3) && 4 <= sn) && 2 < i)) && (((((((((((i <= 6 && 5 < i) && 10 <= sn) && sn <= 10) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && 3 < i) && i <= 4) && 6 <= sn) && sn <= 6)) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && sn <= 16) && 8 < i) && 15 < sn)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && 4 < i) && sn <= 8) && 8 <= sn) && i <= 5)) || ((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && sn <= 2) && i <= 2) && 2 <= sn) && 2 <= i)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && i == 1) && sn == 0)) || ((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && 12 <= sn) && 6 < i) && sn <= 12) && i <= 7)) || (((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && sn <= 14) && 7 < i) && i <= 8) && 14 <= sn)) || ((((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && (((! (sn <= 14) || (sn <= 14 && ! (7 < i))) || ((sn <= 14 && 7 < i) && ! (i <= 8))) || (((sn <= 14 && 7 < i) && i <= 8) && ! (14 <= sn)))) && sn <= 4) && i <= 3) && 4 <= sn) && 2 < i))) && (((((((((((i <= 6 && 5 < i) && 10 <= sn) && sn <= 10) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && 3 < i) && i <= 4) && 6 <= sn) && sn <= 6)) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && sn <= 16) && 8 < i) && 15 < sn)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && 4 < i) && sn <= 8) && 8 <= sn) && i <= 5)) || ((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && sn <= 2) && i <= 2) && 2 <= sn) && 2 <= i)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && i == 1) && sn == 0)) || ((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && 12 <= sn) && 6 < i) && sn <= 12) && i <= 7)) || (((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && sn <= 14) && 7 < i) && i <= 8) && 14 <= sn)) || ((((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && (((! (sn <= 14) || (sn <= 14 && ! (7 < i))) || ((sn <= 14 && 7 < i) && ! (i <= 8))) || (((sn <= 14 && 7 < i) && i <= 8) && ! (14 <= sn)))) && sn <= 4) && i <= 3) && 4 <= sn) && 2 < i))) && (((((((((((i <= 6 && 5 < i) && 10 <= sn) && sn <= 10) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && 3 < i) && i <= 4) && 6 <= sn) && sn <= 6)) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && sn <= 16) && 8 < i) && 15 < sn)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && 4 < i) && sn <= 8) && 8 <= sn) && i <= 5)) || ((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && sn <= 2) && i <= 2) && 2 <= sn) && 2 <= i)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && i == 1) && sn == 0)) || ((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && 12 <= sn) && 6 < i) && sn <= 12) && i <= 7)) || (((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && sn <= 14) && 7 < i) && i <= 8) && 14 <= sn)) || ((((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && (((! (sn <= 14) || (sn <= 14 && ! (7 < i))) || ((sn <= 14 && 7 < i) && ! (i <= 8))) || (((sn <= 14 && 7 < i) && i <= 8) && ! (14 <= sn)))) && sn <= 4) && i <= 3) && 4 <= sn) && 2 < i))) && (((((((((((i <= 6 && 5 < i) && 10 <= sn) && sn <= 10) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && 3 < i) && i <= 4) && 6 <= sn) && sn <= 6)) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && sn <= 16) && 8 < i) && 15 < sn)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && 4 < i) && sn <= 8) && 8 <= sn) && i <= 5)) || ((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && sn <= 2) && i <= 2) && 2 <= sn) && 2 <= i)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && i == 1) && sn == 0)) || ((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && 12 <= sn) && 6 < i) && sn <= 12) && i <= 7)) || (((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && sn <= 14) && 7 < i) && i <= 8) && 14 <= sn)) || ((((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && (((! (sn <= 14) || (sn <= 14 && ! (7 < i))) || ((sn <= 14 && 7 < i) && ! (i <= 8))) || (((sn <= 14 && 7 < i) && i <= 8) && ! (14 <= sn)))) && sn <= 4) && i <= 3) && 4 <= sn) && 2 < i))) && (((((((((((i <= 6 && 5 < i) && 10 <= sn) && sn <= 10) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && 3 < i) && i <= 4) && 6 <= sn) && sn <= 6)) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && sn <= 16) && 8 < i) && 15 < sn)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && 4 < i) && sn <= 8) && 8 <= sn) && i <= 5)) || ((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && sn <= 2) && i <= 2) && 2 <= sn) && 2 <= i)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && i == 1) && sn == 0)) || ((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && 12 <= sn) && 6 < i) && sn <= 12) && i <= 7)) || (((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && sn <= 14) && 7 < i) && i <= 8) && 14 <= sn)) || ((((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && (((! (sn <= 14) || (sn <= 14 && ! (7 < i))) || ((sn <= 14 && 7 < i) && ! (i <= 8))) || (((sn <= 14 && 7 < i) && i <= 8) && ! (14 <= sn)))) && sn <= 4) && i <= 3) && 4 <= sn) && 2 < i))) && (((((((((((i <= 6 && 5 < i) && 10 <= sn) && sn <= 10) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && 3 < i) && i <= 4) && 6 <= sn) && sn <= 6)) || (((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && sn <= 16) && 8 < i) && 15 < sn)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && 4 < i) && sn <= 8) && 8 <= sn) && i <= 5)) || ((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && sn <= 2) && i <= 2) && 2 <= sn) && 2 <= i)) || (((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && i == 1) && sn == 0)) || ((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && 12 <= sn) && 6 < i) && sn <= 12) && i <= 7)) || (((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && sn <= 14) && 7 < i) && i <= 8) && 14 <= sn)) || ((((((((((((((! (i <= 6) || (i <= 6 && ! (5 < i))) || ((i <= 6 && 5 < i) && ! (10 <= sn))) || (((i <= 6 && 5 < i) && 10 <= sn) && ! (sn <= 10))) && (((! (3 < i) || (3 < i && ! (i <= 4))) || ((3 < i && i <= 4) && ! (6 <= sn))) || (((3 < i && i <= 4) && 6 <= sn) && ! (sn <= 6)))) && ((! (sn <= 16) || (sn <= 16 && ! (8 < i))) || ((sn <= 16 && 8 < i) && ! (15 < sn)))) && (((! (4 < i) || (4 < i && ! (sn <= 8))) || ((4 < i && sn <= 8) && ! (8 <= sn))) || (((4 < i && sn <= 8) && 8 <= sn) && ! (i <= 5)))) && (((! (sn <= 2) || (sn <= 2 && ! (i <= 2))) || ((sn <= 2 && i <= 2) && ! (2 <= sn))) || (((sn <= 2 && i <= 2) && 2 <= sn) && ! (2 <= i)))) && (! (i == 1) || (i == 1 && ! (sn == 0)))) && (((! (12 <= sn) || (12 <= sn && ! (6 < i))) || ((12 <= sn && 6 < i) && ! (sn <= 12))) || (((12 <= sn && 6 < i) && sn <= 12) && ! (i <= 7)))) && (((! (sn <= 14) || (sn <= 14 && ! (7 < i))) || ((sn <= 14 && 7 < i) && ! (i <= 8))) || (((sn <= 14 && 7 < i) && i <= 8) && ! (14 <= sn)))) && sn <= 4) && i <= 3) && 4 <= sn) && 2 < i)) (../plain/sum04-2.i:24:6-24:21)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 11
  dead: 0
  total lines: 11
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (../plain/sum04-2.i:12:73-12:74)
[Warning][Witness] invariant unconfirmed: (i <= (6) && (5) < i && (10) <= sn && sn <= (10)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (3) < i && i <= (4) && (6) <= sn && sn <= (6)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && sn <= (16) && (8) < i && (15) < sn) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (4) < i && sn <= (8) && (8) <= sn && i <= (5)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && sn <= (2) && i <= (2) && (2) <= sn && (2) <= i) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && i == (1) && sn == (0)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (12) <= sn && (6) < i && sn <= (12) && i <= (7)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (!((12) <= sn) || ((12) <= sn && !((6) < i)) || ((12) <= sn && (6) < i && !(sn <= (12))) || ((12) <= sn && (6) < i && sn <= (12) && !(i <= (7)))) && sn <= (14) && (7) < i && i <= (8) && (14) <= sn) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (!((12) <= sn) || ((12) <= sn && !((6) < i)) || ((12) <= sn && (6) < i && !(sn <= (12))) || ((12) <= sn && (6) < i && sn <= (12) && !(i <= (7)))) && (!(sn <= (14)) || (sn <= (14) && !((7) < i)) || (sn <= (14) && (7) < i && !(i <= (8))) || (sn <= (14) && (7) < i && i <= (8) && !((14) <= sn))) && sn <= (4) && i <= (3) && (4) <= sn && (2) < i) (../plain/sum04-2.i:18:3)
[Warning][Witness] invariant unconfirmed: (i <= (6) && (5) < i && (10) <= sn && sn <= (10)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (3) < i && i <= (4) && (6) <= sn && sn <= (6)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && sn <= (16) && (8) < i && (15) < sn) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (4) < i && sn <= (8) && (8) <= sn && i <= (5)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && sn <= (2) && i <= (2) && (2) <= sn && (2) <= i) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && i == (1) && sn == (0)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (12) <= sn && (6) < i && sn <= (12) && i <= (7)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (!((12) <= sn) || ((12) <= sn && !((6) < i)) || ((12) <= sn && (6) < i && !(sn <= (12))) || ((12) <= sn && (6) < i && sn <= (12) && !(i <= (7)))) && sn <= (14) && (7) < i && i <= (8) && (14) <= sn) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (!((12) <= sn) || ((12) <= sn && !((6) < i)) || ((12) <= sn && (6) < i && !(sn <= (12))) || ((12) <= sn && (6) < i && sn <= (12) && !(i <= (7)))) && (!(sn <= (14)) || (sn <= (14) && !((7) < i)) || (sn <= (14) && (7) < i && !(i <= (8))) || (sn <= (14) && (7) < i && i <= (8) && !((14) <= sn))) && sn <= (4) && i <= (3) && (4) <= sn && (2) < i) (../plain/sum04-2.i:16:5)
[Warning][Witness] invariant unconfirmed: (i <= (6) && (5) < i && (10) <= sn && sn <= (10)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (3) < i && i <= (4) && (6) <= sn && sn <= (6)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && sn <= (16) && (8) < i && (15) < sn) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (4) < i && sn <= (8) && (8) <= sn && i <= (5)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && sn <= (2) && i <= (2) && (2) <= sn && (2) <= i) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && i == (1) && sn == (0)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (12) <= sn && (6) < i && sn <= (12) && i <= (7)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (!((12) <= sn) || ((12) <= sn && !((6) < i)) || ((12) <= sn && (6) < i && !(sn <= (12))) || ((12) <= sn && (6) < i && sn <= (12) && !(i <= (7)))) && sn <= (14) && (7) < i && i <= (8) && (14) <= sn) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (!((12) <= sn) || ((12) <= sn && !((6) < i)) || ((12) <= sn && (6) < i && !(sn <= (12))) || ((12) <= sn && (6) < i && sn <= (12) && !(i <= (7)))) && (!(sn <= (14)) || (sn <= (14) && !((7) < i)) || (sn <= (14) && (7) < i && !(i <= (8))) || (sn <= (14) && (7) < i && i <= (8) && !((14) <= sn))) && sn <= (4) && i <= (3) && (4) <= sn && (2) < i) (../plain/sum04-2.i:12:69)
[Warning][Witness] invariant unconfirmed: (i <= (6) && (5) < i && (10) <= sn && sn <= (10)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (3) < i && i <= (4) && (6) <= sn && sn <= (6)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && sn <= (16) && (8) < i && (15) < sn) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (4) < i && sn <= (8) && (8) <= sn && i <= (5)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && sn <= (2) && i <= (2) && (2) <= sn && (2) <= i) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && i == (1) && sn == (0)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (12) <= sn && (6) < i && sn <= (12) && i <= (7)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (!((12) <= sn) || ((12) <= sn && !((6) < i)) || ((12) <= sn && (6) < i && !(sn <= (12))) || ((12) <= sn && (6) < i && sn <= (12) && !(i <= (7)))) && sn <= (14) && (7) < i && i <= (8) && (14) <= sn) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (!((12) <= sn) || ((12) <= sn && !((6) < i)) || ((12) <= sn && (6) < i && !(sn <= (12))) || ((12) <= sn && (6) < i && sn <= (12) && !(i <= (7)))) && (!(sn <= (14)) || (sn <= (14) && !((7) < i)) || (sn <= (14) && (7) < i && !(i <= (8))) || (sn <= (14) && (7) < i && i <= (8) && !((14) <= sn))) && sn <= (4) && i <= (3) && (4) <= sn && (2) < i) (../plain/sum04-2.i:16:13)
[Warning][Witness] invariant unconfirmed: (i <= (6) && (5) < i && (10) <= sn && sn <= (10)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (3) < i && i <= (4) && (6) <= sn && sn <= (6)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && sn <= (16) && (8) < i && (15) < sn) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (4) < i && sn <= (8) && (8) <= sn && i <= (5)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && sn <= (2) && i <= (2) && (2) <= sn && (2) <= i) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && i == (1) && sn == (0)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (12) <= sn && (6) < i && sn <= (12) && i <= (7)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (!((12) <= sn) || ((12) <= sn && !((6) < i)) || ((12) <= sn && (6) < i && !(sn <= (12))) || ((12) <= sn && (6) < i && sn <= (12) && !(i <= (7)))) && sn <= (14) && (7) < i && i <= (8) && (14) <= sn) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (!((12) <= sn) || ((12) <= sn && !((6) < i)) || ((12) <= sn && (6) < i && !(sn <= (12))) || ((12) <= sn && (6) < i && sn <= (12) && !(i <= (7)))) && (!(sn <= (14)) || (sn <= (14) && !((7) < i)) || (sn <= (14) && (7) < i && !(i <= (8))) || (sn <= (14) && (7) < i && i <= (8) && !((14) <= sn))) && sn <= (4) && i <= (3) && (4) <= sn && (2) < i) (../plain/sum04-2.i:12:83)
[Warning][Witness] invariant unconfirmed: (i <= (6) && (5) < i && (10) <= sn && sn <= (10)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (3) < i && i <= (4) && (6) <= sn && sn <= (6)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && sn <= (16) && (8) < i && (15) < sn) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (4) < i && sn <= (8) && (8) <= sn && i <= (5)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && sn <= (2) && i <= (2) && (2) <= sn && (2) <= i) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && i == (1) && sn == (0)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (12) <= sn && (6) < i && sn <= (12) && i <= (7)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (!((12) <= sn) || ((12) <= sn && !((6) < i)) || ((12) <= sn && (6) < i && !(sn <= (12))) || ((12) <= sn && (6) < i && sn <= (12) && !(i <= (7)))) && sn <= (14) && (7) < i && i <= (8) && (14) <= sn) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (!((12) <= sn) || ((12) <= sn && !((6) < i)) || ((12) <= sn && (6) < i && !(sn <= (12))) || ((12) <= sn && (6) < i && sn <= (12) && !(i <= (7)))) && (!(sn <= (14)) || (sn <= (14) && !((7) < i)) || (sn <= (14) && (7) < i && !(i <= (8))) || (sn <= (14) && (7) < i && i <= (8) && !((14) <= sn))) && sn <= (4) && i <= (3) && (4) <= sn && (2) < i) (../plain/sum04-2.i:24:3)
[Warning][Witness] invariant unconfirmed: (i <= (6) && (5) < i && (10) <= sn && sn <= (10)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (3) < i && i <= (4) && (6) <= sn && sn <= (6)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && sn <= (16) && (8) < i && (15) < sn) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (4) < i && sn <= (8) && (8) <= sn && i <= (5)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && sn <= (2) && i <= (2) && (2) <= sn && (2) <= i) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && i == (1) && sn == (0)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (12) <= sn && (6) < i && sn <= (12) && i <= (7)) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (!((12) <= sn) || ((12) <= sn && !((6) < i)) || ((12) <= sn && (6) < i && !(sn <= (12))) || ((12) <= sn && (6) < i && sn <= (12) && !(i <= (7)))) && sn <= (14) && (7) < i && i <= (8) && (14) <= sn) || ((!(i <= (6)) || (i <= (6) && !((5) < i)) || (i <= (6) && (5) < i && !((10) <= sn)) || (i <= (6) && (5) < i && (10) <= sn && !(sn <= (10)))) && (!((3) < i) || ((3) < i && !(i <= (4))) || ((3) < i && i <= (4) && !((6) <= sn)) || ((3) < i && i <= (4) && (6) <= sn && !(sn <= (6)))) && (!(sn <= (16)) || (sn <= (16) && !((8) < i)) || (sn <= (16) && (8) < i && !((15) < sn))) && (!((4) < i) || ((4) < i && !(sn <= (8))) || ((4) < i && sn <= (8) && !((8) <= sn)) || ((4) < i && sn <= (8) && (8) <= sn && !(i <= (5)))) && (!(sn <= (2)) || (sn <= (2) && !(i <= (2))) || (sn <= (2) && i <= (2) && !((2) <= sn)) || (sn <= (2) && i <= (2) && (2) <= sn && !((2) <= i))) && (!(i == (1)) || (i == (1) && !(sn == (0)))) && (!((12) <= sn) || ((12) <= sn && !((6) < i)) || ((12) <= sn && (6) < i && !(sn <= (12))) || ((12) <= sn && (6) < i && sn <= (12) && !(i <= (7)))) && (!(sn <= (14)) || (sn <= (14) && !((7) < i)) || (sn <= (14) && (7) < i && !(i <= (8))) || (sn <= (14) && (7) < i && i <= (8) && !((14) <= sn))) && sn <= (4) && i <= (3) && (4) <= sn && (2) < i) (../plain/sum04-2.i:12:23)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 7
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 8
SV-COMP result: unknown

vars = 32    evals = 28    narrow_reuses = 1

Timings:
                                  cputime   walltime   allocated   count
Default                            3.025s     3.028s    591.15MB      1×
  preprocess                         0.026s     0.024s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.10MB      4×
  Cabs2cil                           0.006s     0.006s      4.70MB      4×
  mergeCIL                           0.004s     0.004s      3.33MB      1×
  analysis                           2.982s     2.984s    574.06MB      1×
    createCFG                          0.001s     0.001s      0.60MB      1×
      handle                             0.001s     0.001s      0.09MB     33×
      iter_connect                       0.001s     0.001s      0.41MB     33×
        computeSCCs                        0.001s     0.001s      0.23MB     34×
    FrontC                             0.025s     0.025s     16.72MB     14×
    Cabs2cil                           0.023s     0.023s     13.58MB     14×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            0.775s     0.776s    399.51MB      1×
      S.Dom.equal                        0.001s     0.001s      0.01MB     29×
      base unassume                      0.239s     0.240s    341.60MB      5×
      cheap_full_reach                   0.001s     0.001s      0.02MB      1×
      postsolver                         0.023s     0.023s     15.70MB      1×
        postsolver_iter                    0.023s     0.023s     15.67MB      1×
    warn_global                        0.001s     0.001s      0.11MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
