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


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


--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 == (4) && j == (7) && k == (1)) || ((!(i == (4)) || (i == (4) && !(j == (7)))) && i == (2) && j == (6) && k == (1)) || (!(i == (4)) && (!(i == (2)) || (i == (2) && !(j == (6)))) && i == (3) && j == (7) && k == (1)) || (!(i == (4)) && (!(i == (2)) || (i == (2) && !(j == (6)))) && !(i == (3)) && i == (5) && j == (7) && k == (1)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7) && !(k == (1)))) && (!(j == (6)) || (j == (6) && !(k == (1)))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7) && !(k == (1)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (1)))) && i == (2) && j == (5) && k == (2)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7) && !(k == (1)))) && (!(i == (2)) || (i == (2) && !(j == (6))) || (i == (2) && j == (6) && !(k == (1)))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7) && !(k == (1)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (1)))) && (!(i == (2)) || (i == (2) && !(j == (5)))) && i == (1) && j == (4) && k == (2)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7) && !(k == (1)))) && (!(i == (2)) || (i == (2) && !(j == (6))) || (i == (2) && j == (6) && !(k == (1)))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7) && !(k == (1)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (1)))) && (!(i == (2)) || (i == (2) && !(k == (2)))) && (!(j == (4)) || (j == (4) && !(k == (2)))) && i == (1) && j == (5) && k == (4)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7) && !(k == (1)))) && (!(i == (2)) || (i == (2) && !(k == (1)))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7) && !(k == (1)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (1)))) && (!(i == (2)) || (i == (2) && !(j == (5)))) && !(j == (4)) && (!(j == (5)) || (j == (5) && !(k == (4)))) && i == (1) && j == (6) && k == (2)) || ((!(j == (7)) || (j == (7) && !(k == (1)))) && (!(i == (2)) || (i == (2) && !(k == (1)))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7) && !(k == (1)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (1)))) && (!(i == (2)) || (i == (2) && !(j == (5)))) && !(i == (1)) && i == (4) && j == (6) && k == (2)) || ((!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (2)) || (i == (2) && !(j == (6)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5) && !(k == (2)))) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4) && !(k == (2)))) && (!(i == (1)) || (i == (1) && !(j == (5))) || (i == (1) && j == (5) && !(k == (4)))) && (!(i == (1)) || (i == (1) && !(j == (6))) || (i == (1) && j == (6) && !(k == (2)))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6) && !(k == (2)))) && i == (6) && j == (8) && k == (1)) || ((!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (2)) || (i == (2) && !(j == (6)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (2)) || (i == (2) && !(k == (2)))) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4) && !(k == (2)))) && (!(i == (1)) || (i == (1) && !(k == (4)))) && (!(i == (1)) || (i == (1) && !(j == (6))) || (i == (1) && j == (6) && !(k == (2)))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6) && !(k == (2)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && i == (-1) && j == (5) && k == (1)) || (!(i == (2)) && !(j == (7)) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4) && !(k == (2)))) && (!(i == (1)) || (i == (1) && !(j == (5))) || (i == (1) && j == (5) && !(k == (4)))) && (!(i == (1)) || (i == (1) && !(k == (2)))) && (!(i == (4)) || (i == (4) && !(k == (2)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (-1)) || (i == (-1) && !(j == (5)))) && i == (3) && j == (6) && k == (1)) || ((!(i == (4)) || (i == (4) && !(j == (7)))) && !(i == (2)) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4) && !(k == (2)))) && (!(i == (1)) || (i == (1) && !(k == (2)))) && (!(i == (4)) || (i == (4) && !(k == (2)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (5)) && !(i == (3)) && i == (-1) && j == (6) && k == (1)) || ((!(i == (2)) || (i == (2) && !(j == (6))) || (i == (2) && j == (6))) && !(k == (1)) && (!(i == (2)) || (i == (2) && !(j == (5)))) && (!(i == (1)) || (i == (1) && !(j == (4)))) && (!(i == (1)) || (i == (1) && !(j == (5))) || (i == (1) && j == (5) && !(k == (4)))) && (!(i == (1)) || (i == (1) && !(j == (6)))) && (!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5))) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6))) && (!(i == (-1)) || (i == (-1) && !(j == (6))) || (i == (-1) && j == (6))) && i == (5) && j == (7) && k == (2)) || ((!(i == (4)) || (i == (4) && !(j == (7)))) && !(i == (2)) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4) && !(k == (2)))) && (!(i == (1)) || (i == (1) && !(j == (5))) || (i == (1) && j == (5) && !(k == (4)))) && (!(i == (1)) || (i == (1) && !(k == (2)))) && (!(i == (4)) || (i == (4) && !(k == (2)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(i == (3)) && !(i == (-1)) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (2)))) && i == (0) && j == (6) && k == (1)) || ((!(i == (4)) || (i == (4) && !(j == (7)))) && !(j == (6)) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && !(k == (2)) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4))) && (!(i == (1)) || (i == (1) && !(k == (4)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(i == (-1)) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && i == (2) && j == (5) && k == (1)) || ((!(i == (2)) || (i == (2) && !(j == (6))) || (i == (2) && j == (6))) && !(k == (1)) && (!(i == (2)) || (i == (2) && !(j == (5)))) && (!(i == (1)) || (i == (1) && !(j == (4)))) && (!(i == (1)) || (i == (1) && !(j == (5))) || (i == (1) && j == (5) && !(k == (4)))) && (!(i == (1)) || (i == (1) && !(j == (6)))) && (!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5))) && (!(i == (-1)) || (i == (-1) && !(j == (6))) || (i == (-1) && j == (6))) && !(i == (5)) && (!(i == (0)) || (i == (0) && !(j == (6))) || (i == (0) && j == (6))) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5))) && i == (3) && j == (7) && k == (2)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7) && !(k == (1)))) && (!(j == (6)) || (j == (6) && !(k == (1)))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7) && !(k == (1)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (1)))) && !(j == (5)) && !(i == (1)) && (!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8) && !(k == (1)))) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6) && !(k == (1)))) && (!(i == (-1)) || (i == (-1) && !(j == (6))) || (i == (-1) && j == (6) && !(k == (1)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (0)) || (i == (0) && !(j == (6))) || (i == (0) && j == (6) && !(k == (1)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && i == (2) && j == (4) && k == (2)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && !(k == (2)) && !(i == (1)) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6))) && (!(i == (-1)) || (i == (-1) && !(j == (6))) || (i == (-1) && j == (6))) && (!(i == (0)) || (i == (0) && !(j == (6))) || (i == (0) && j == (6))) && !(k == (1)) && i == (2) && j == (5) && k == (4)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (2)) || (i == (2) && !(j == (6))) || (i == (2) && j == (6))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && (!(i == (2)) || (i == (2) && !(k == (2)))) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4) && !(k == (2)))) && (!(i == (1)) || (i == (1) && !(k == (4)))) && (!(i == (1)) || (i == (1) && !(j == (6))) || (i == (1) && j == (6) && !(k == (2)))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6) && !(k == (2)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && !(k == (1)) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (2)))) && (!(i == (0)) || (i == (0) && !(j == (6))) || (i == (0) && j == (6))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7) && !(k == (2)))) && (!(i == (2)) || (i == (2) && !(j == (4))) || (i == (2) && j == (4) && !(k == (2)))) && (!(i == (2)) || (i == (2) && !(k == (4)))) && i == (-1) && j == (5) && k == (3)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && !(k == (2)) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4))) && (!(i == (1)) || (i == (1) && !(j == (6))) || (i == (1) && j == (6))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6))) && (!(i == (0)) || (i == (0) && !(j == (6))) || (i == (0) && j == (6))) && !(k == (1)) && !(k == (4)) && !(i == (-1)) && i == (2) && j == (5) && k == (3)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7) && !(k == (1)))) && (!(j == (7)) || (j == (7) && !(k == (1)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (1)))) && !(i == (1)) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6) && !(k == (2)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8) && !(k == (1)))) && (!(i == (-1)) || (i == (-1) && !(k == (1)))) && (!(j == (6)) || (j == (6) && !(k == (1)))) && (!(i == (-1)) || (i == (-1) && !(j == (6))) || (i == (-1) && j == (6) && !(k == (1)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (2)))) && (!(i == (0)) || (i == (0) && !(j == (6))) || (i == (0) && j == (6) && !(k == (1)))) && (!(j == (7)) || (j == (7) && !(k == (2)))) && !(i == (2)) && (!(i == (-1)) || (i == (-1) && !(k == (3)))) && i == (3) && j == (5) && k == (4)) || ((!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(j == (4)) || (j == (4) && !(k == (2)))) && !(k == (4)) && (!(j == (6)) || (j == (6) && !(k == (2)))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6) && !(k == (2)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(i == (-1)) && (!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (2)))) && (!(i == (0)) || (i == (0) && !(j == (6)))) && !(i == (2)) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7) && !(k == (2)))) && i == (1) && j == (5) && k == (1)) || ((!(i == (2)) || (i == (2) && !(j == (5)))) && !(i == (1)) && !(i == (4)) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5))) && !(k == (1)) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5))) && !(j == (7)) && (!(i == (2)) || (i == (2) && !(j == (4)))) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5) && !(k == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5) && !(k == (3)))) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5) && !(k == (3)))) && (!(j == (5)) || (j == (5) && !(k == (4)))) && i == (3) && j == (6) && k == (2)) || (!(j == (7)) && !(i == (2)) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4))) && (!(i == (1)) || (i == (1) && !(j == (5))) || (i == (1) && j == (5) && !(k == (4)))) && !(k == (2)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(i == (3)) && !(i == (-1)) && !(i == (0)) && (!(i == (1)) || (i == (1) && !(j == (5)))) && i == (4) && j == (6) && k == (1)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (2)) || (i == (2) && !(j == (6))) || (i == (2) && j == (6))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && (!(i == (2)) || (i == (2) && !(j == (5)))) && (!(i == (1)) || (i == (1) && !(j == (4)))) && (!(i == (1)) || (i == (1) && !(j == (5))) || (i == (1) && j == (5) && !(k == (4)))) && (!(i == (1)) || (i == (1) && !(j == (6)))) && (!(i == (4)) || (i == (4) && !(j == (6)))) && !(k == (1)) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5))) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6))) && (!(i == (-1)) || (i == (-1) && !(j == (6))) || (i == (-1) && j == (6))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (0)) || (i == (0) && !(j == (6))) || (i == (0) && j == (6))) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (2)) || (i == (2) && !(j == (4)))) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5) && !(k == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5) && !(k == (3)))) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5) && !(k == (3)))) && (!(i == (3)) || (i == (3) && !(j == (5))) || (i == (3) && j == (5) && !(k == (4)))) && (!(i == (1)) || (i == (1) && !(j == (5))) || (i == (1) && j == (5))) && (!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6))) && i == (6) && j == (8) && k == (2)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && !(k == (1)) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4) && !(k == (2)))) && (!(i == (1)) || (i == (1) && !(k == (2)))) && (!(i == (4)) || (i == (4) && !(k == (2)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (2)))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7) && !(k == (2)))) && (!(j == (4)) || (j == (4) && !(k == (2)))) && !(j == (5)) && (!(i == (3)) || (i == (3) && !(k == (2)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8) && !(k == (2)))) && i == (2) && j == (6) && k == (3)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7) && !(k == (1)))) && (!(j == (7)) || (j == (7) && !(k == (1)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (1)))) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4) && !(k == (2)))) && (!(i == (1)) || (i == (1) && !(j == (6))) || (i == (1) && j == (6) && !(k == (2)))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6) && !(k == (2)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8) && !(k == (1)))) && (!(j == (6)) || (j == (6) && !(k == (1)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (2)))) && (!(i == (0)) || (i == (0) && !(j == (6))) || (i == (0) && j == (6) && !(k == (1)))) && (!(j == (7)) || (j == (7) && !(k == (2)))) && !(i == (-1)) && !(i == (2)) && !(k == (4)) && (!(i == (1)) || (i == (1) && !(k == (1)))) && (!(j == (6)) || (j == (6) && !(k == (2)))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6) && !(k == (1)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8) && !(k == (2)))) && i == (3) && j == (5) && k == (3)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7) && !(k == (1)))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7) && !(k == (1)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (1)))) && !(i == (1)) && (!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8) && !(k == (1)))) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5) && !(k == (1)))) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6) && !(k == (1)))) && (!(i == (-1)) || (i == (-1) && !(j == (6))) || (i == (-1) && j == (6) && !(k == (1)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(j == (6)) || (j == (6) && !(k == (1)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && !(i == (2)) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5) && !(k == (3)))) && (!(i == (3)) || (i == (3) && !(j == (5))) || (i == (3) && j == (5) && !(k == (4)))) && (!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6) && !(k == (1)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (3)) || (i == (3) && !(j == (5))) || (i == (3) && j == (5) && !(k == (3)))) && i == (0) && j == (4) && k == (2)) || ((!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(i == (-1)) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (2)))) && !(j == (6)) && !(i == (2)) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7) && !(k == (2)))) && (!(i == (3)) || (i == (3) && !(k == (4)))) && !(i == (1)) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8) && !(k == (2)))) && (!(i == (3)) || (i == (3) && !(k == (3)))) && (!(j == (4)) || (j == (4) && !(k == (2)))) && i == (0) && j == (5) && k == (1)) || (!(k == (1)) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && !(j == (5)) && !(i == (1)) && !(i == (4)) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && !(j == (4)) && !(i == (3)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(k == (3)) && i == (2) && j == (6) && k == (2)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && !(k == (1)) && !(k == (2)) && !(i == (2)) && !(j == (5)) && (!(i == (0)) || (i == (0) && !(j == (4))) || (i == (0) && j == (4))) && i == (3) && j == (6) && k == (3)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && !(i == (2)) && !(j == (4)) && !(k == (4)) && !(j == (6)) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (-1)) || (i == (-1) && !(k == (3)))) && !(k == (1)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (3)) || (i == (3) && !(k == (3)))) && i == (1) && j == (5) && k == (2)) || ((!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && !(i == (1)) && !(i == (4)) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && !(k == (1)) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5) && !(k == (3)))) && !(i == (3)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (4)) && !(i == (2)) && i == (0) && j == (6) && k == (2)) || (!(k == (1)) && (!(i == (2)) || (i == (2) && !(j == (5)))) && (!(i == (1)) || (i == (1) && !(j == (4)))) && (!(i == (1)) || (i == (1) && !(j == (5))) || (i == (1) && j == (5) && !(k == (4)))) && !(j == (6)) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5))) && !(i == (5)) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5))) && !(i == (3)) && (!(i == (2)) || (i == (2) && !(j == (4)))) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5) && !(k == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5) && !(k == (3)))) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5) && !(k == (3)))) && (!(i == (1)) || (i == (1) && !(j == (5))) || (i == (1) && j == (5))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (0)) || (i == (0) && !(j == (4)))) && (!(i == (0)) || (i == (0) && !(j == (5))) || (i == (0) && j == (5))) && (!(i == (1)) || (i == (1) && !(j == (5)))) && i == (4) && j == (7) && k == (2)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && !(i == (2)) && (!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && !(k == (1)) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (0)) || (i == (0) && !(j == (6))) || (i == (0) && j == (6))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && !(k == (3)) && (!(i == (3)) || (i == (3) && !(k == (4)))) && (!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (0)) || (i == (0) && !(j == (4)))) && !(i == (1)) && (!(i == (0)) || (i == (0) && !(j == (6)))) && (!(i == (4)) || (i == (4) && !(j == (7)))) && i == (-1) && j == (5) && k == (2)) || ((!(i == (2)) || (i == (2) && !(j == (6)))) && !(j == (7)) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5) && !(k == (2)))) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4) && !(k == (2)))) && (!(i == (1)) || (i == (1) && !(j == (5))) || (i == (1) && j == (5) && !(k == (4)))) && (!(i == (1)) || (i == (1) && !(j == (6))) || (i == (1) && j == (6) && !(k == (2)))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6) && !(k == (2)))) && !(i == (6)) && (!(i == (-1)) || (i == (-1) && !(j == (5)))) && (!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (-1)) || (i == (-1) && !(j == (6)))) && (!(i == (0)) || (i == (0) && !(j == (6)))) && (!(i == (2)) || (i == (2) && !(j == (5)))) && (!(i == (2)) || (i == (2) && !(j == (4))) || (i == (2) && j == (4) && !(k == (2)))) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5) && !(k == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5) && !(k == (3)))) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5) && !(k == (3)))) && (!(i == (3)) || (i == (3) && !(j == (5))) || (i == (3) && j == (5) && !(k == (4)))) && (!(i == (1)) || (i == (1) && !(j == (5)))) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6) && !(k == (2)))) && (!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (2)) || (i == (2) && !(j == (6))) || (i == (2) && j == (6) && !(k == (3)))) && (!(i == (3)) || (i == (3) && !(j == (5))) || (i == (3) && j == (5) && !(k == (3)))) && (!(i == (0)) || (i == (0) && !(j == (4))) || (i == (0) && j == (4) && !(k == (2)))) && (!(i == (0)) || (i == (0) && !(j == (5)))) && (!(i == (2)) || (i == (2) && !(j == (6))) || (i == (2) && j == (6) && !(k == (2)))) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6) && !(k == (3)))) && (!(i == (1)) || (i == (1) && !(j == (5))) || (i == (1) && j == (5) && !(k == (2)))) && (!(i == (0)) || (i == (0) && !(j == (6))) || (i == (0) && j == (6) && !(k == (2)))) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5) && !(k == (2)))) && i == (5) && j == (8) && k == (1)) || ((!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4))) && (!(i == (1)) || (i == (1) && !(j == (5))) || (i == (1) && j == (5) && !(k == (4)))) && !(k == (2)) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5))) && (!(i == (-1)) || (i == (-1) && !(j == (5)))) && (!(i == (1)) || (i == (1) && !(j == (5))) || (i == (1) && j == (5))) && !(k == (1)) && !(i == (2)) && (!(i == (0)) || (i == (0) && !(j == (4))) || (i == (0) && j == (4))) && (!(i == (0)) || (i == (0) && !(j == (5))) || (i == (0) && j == (5))) && !(i == (3)) && (!(i == (5)) || (i == (5) && !(j == (8))) || (i == (5) && j == (8))) && i == (4) && j == (6) && k == (3)) || (!(j == (7)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(i == (-1)) && !(j == (6)) && !(i == (2)) && !(k == (4)) && !(i == (1)) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8) && !(k == (2)))) && !(k == (3)) && !(i == (0)) && (!(i == (5)) || (i == (5) && !(j == (8)))) && i == (3) && j == (5) && k == (1)) || ((!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5))) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4))) && (!(i == (1)) || (i == (1) && !(j == (5)))) && !(k == (2)) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5))) && (!(i == (2)) || (i == (2) && !(j == (4))) || (i == (2) && j == (4))) && (!(i == (2)) || (i == (2) && !(j == (5)))) && (!(i == (3)) || (i == (3) && !(j == (5)))) && (!(i == (1)) || (i == (1) && !(j == (5))) || (i == (1) && j == (5))) && !(k == (1)) && (!(i == (3)) || (i == (3) && !(j == (5))) || (i == (3) && j == (5))) && (!(i == (0)) || (i == (0) && !(j == (4))) || (i == (0) && j == (4))) && (!(i == (0)) || (i == (0) && !(j == (5))) || (i == (0) && j == (5))) && (!(i == (5)) || (i == (5) && !(j == (8))) || (i == (5) && j == (8))) && !(k == (3)) && i == (4) && j == (6) && k == (4)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && !(i == (2)) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(k == (4)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (3)) || (i == (3) && !(k == (3)))) && !(j == (4)) && !(k == (1)) && !(i == (1)) && !(j == (6)) && (!(i == (4)) || (i == (4) && !(j == (7)))) && !(i == (-1)) && (!(i == (5)) || (i == (5) && !(j == (8))) || (i == (5) && j == (8))) && i == (0) && j == (5) && k == (2)) || (!(i == (4)) && !(j == (6)) && !(i == (3)) && !(i == (5)) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4) && !(k == (2)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (5)) && (!(j == (4)) || (j == (4) && !(k == (2)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8) && !(k == (2)))) && (!(i == (0)) || (i == (0) && !(j == (4))) || (i == (0) && j == (4) && !(k == (2)))) && i == (2) && j == (7) && k == (1)) || ((!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (1)) || (i == (1) && !(k == (2)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (5)) && !(j == (6)) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (2)))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7) && !(k == (2)))) && (!(i == (2)) || (i == (2) && !(k == (2)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8) && !(k == (2)))) && (!(i == (0)) || (i == (0) && !(k == (2)))) && (!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7) && !(k == (2)))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && (!(i == (2)) || (i == (2) && !(j == (7)))) && i == (-1) && j == (4) && k == (1)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7) && !(k == (1)))) && (!(i == (2)) || (i == (2) && !(j == (6))) || (i == (2) && j == (6) && !(k == (1)))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7) && !(k == (1)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (1)))) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5))) && !(k == (2)) && (!(j == (5)) || (j == (5) && !(k == (4)))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8) && !(k == (1)))) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5) && !(k == (1)))) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6) && !(k == (1)))) && (!(i == (-1)) || (i == (-1) && !(j == (6))) || (i == (-1) && j == (6) && !(k == (1)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && (!(i == (0)) || (i == (0) && !(j == (6))) || (i == (0) && j == (6) && !(k == (1)))) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5) && !(k == (1)))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7))) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5) && !(k == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (5)))) && (!(i == (2)) || (i == (2) && !(j == (5)))) && (!(i == (3)) || (i == (3) && !(j == (5))) || (i == (3) && j == (5) && !(k == (4)))) && (!(j == (5)) || (j == (5) && !(k == (1)))) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6) && !(k == (1)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (2)) || (i == (2) && !(j == (6)))) && (!(i == (3)) || (i == (3) && !(j == (5)))) && (!(i == (0)) || (i == (0) && !(j == (5))) || (i == (0) && j == (5) && !(k == (1)))) && (!(i == (2)) || (i == (2) && !(j == (6))) || (i == (2) && j == (6))) && (!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (0)) || (i == (0) && !(j == (6))) || (i == (0) && j == (6))) && (!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5))) && (!(i == (5)) || (i == (5) && !(j == (8))) || (i == (5) && j == (8) && !(k == (1)))) && (!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (3)) || (i == (3) && !(j == (5))) || (i == (3) && j == (5) && !(k == (1)))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6) && !(k == (4)))) && (!(i == (0)) || (i == (0) && !(j == (5))) || (i == (0) && j == (5))) && (!(i == (2)) || (i == (2) && !(j == (7))) || (i == (2) && j == (7) && !(k == (1)))) && (!(i == (-1)) || (i == (-1) && !(k == (1)))) && i == (1) && j == (4) && k == (3)) || (!(i == (2)) && (!(i == (5)) || (i == (5) && !(j == (7)))) && !(k == (2)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(i == (3)) && !(i == (-1)) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && !(i == (0)) && !(j == (5)) && !(i == (4)) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && (!(j == (4)) || (j == (4) && !(k == (3)))) && i == (1) && j == (6) && k == (1)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (2)) || (i == (2) && !(j == (6))) || (i == (2) && j == (6))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6) && !(k == (2)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (2)))) && (!(i == (0)) || (i == (0) && !(j == (6))) || (i == (0) && j == (6))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7) && !(k == (2)))) && (!(i == (2)) || (i == (2) && !(k == (2)))) && !(j == (5)) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6) && !(k == (2)))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8) && !(k == (2)))) && (!(i == (2)) || (i == (2) && !(j == (6)))) && (!(i == (0)) || (i == (0) && !(k == (2)))) && (!(i == (2)) || (i == (2) && !(j == (6))) || (i == (2) && j == (6) && !(k == (2)))) && (!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (0)) || (i == (0) && !(j == (6))) || (i == (0) && j == (6) && !(k == (2)))) && (!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7) && !(k == (2)))) && (!(i == (5)) || (i == (5) && !(j == (8))) || (i == (5) && j == (8))) && (!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6) && !(k == (4)))) && (!(i == (2)) || (i == (2) && !(j == (7))) || (i == (2) && j == (7))) && !(k == (1)) && !(i == (1)) && i == (-1) && j == (4) && k == (3)) || ((!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && !(k == (2)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7))) && !(j == (5)) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && (!(i == (2)) || (i == (2) && !(j == (7)))) && !(i == (-1)) && !(k == (3)) && !(j == (6)) && i == (1) && j == (4) && k == (1)) || ((!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && !(k == (1)) && (!(i == (2)) || (i == (2) && !(j == (4))) || (i == (2) && j == (4))) && !(j == (5)) && !(k == (2)) && (!(i == (0)) || (i == (0) && !(j == (4))) || (i == (0) && j == (4))) && !(k == (3)) && (!(i == (5)) || (i == (5) && !(j == (8))) || (i == (5) && j == (8))) && !(i == (4)) && (!(i == (2)) || (i == (2) && !(j == (7))) || (i == (2) && j == (7))) && (!(i == (-1)) || (i == (-1) && !(j == (4))) || (i == (-1) && j == (4))) && i == (3) && j == (6) && k == (4)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4))) && (!(i == (1)) || (i == (1) && !(k == (4)))) && (!(i == (1)) || (i == (1) && !(j == (6))) || (i == (1) && j == (6))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && !(i == (-1)) && !(i == (2)) && !(i == (3)) && !(k == (1)) && (!(i == (5)) || (i == (5) && !(j == (8))) || (i == (5) && j == (8))) && (!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6) && !(k == (4)))) && !(k == (2)) && (!(i == (1)) || (i == (1) && !(j == (4)))) && i == (0) && j == (5) && k == (3)) || (!(j == (6)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (5)) && !(k == (2)) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && !(j == (7)) && !(i == (-1)) && !(i == (1)) && i == (2) && j == (4) && k == (1)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && !(k == (4)) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && !(i == (-1)) && !(i == (2)) && !(k == (1)) && !(i == (3)) && !(k == (2)) && (!(i == (5)) || (i == (5) && !(j == (8))) || (i == (5) && j == (8))) && (!(i == (4)) || (i == (4) && !(j == (6)))) && !(j == (4)) && !(i == (0)) && i == (1) && j == (5) && k == (3)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7) && !(k == (1)))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7) && !(k == (1)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (1)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8) && !(k == (1)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (4)) && !(j == (6)) && (!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (8))) || (i == (5) && j == (8) && !(k == (1)))) && !(j == (5)) && (!(i == (2)) || (i == (2) && !(j == (7))) || (i == (2) && j == (7) && !(k == (1)))) && i == (0) && j == (3) && k == (2)) || (!(i == (2)) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && !(j == (7)) && !(k == (4)) && !(j == (6)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(k == (3)) && !(i == (1)) && !(i == (-1)) && (!(i == (5)) || (i == (5) && !(j == (8))) || (i == (5) && j == (8))) && !(k == (1)) && !(i == (0)) && i == (3) && j == (5) && k == (2)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7) && !(k == (1)))) && (!(i == (2)) || (i == (2) && !(j == (6))) || (i == (2) && j == (6) && !(k == (1)))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7) && !(k == (1)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (1)))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8) && !(k == (1)))) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6) && !(k == (1)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && (!(j == (6)) || (j == (6) && !(k == (1)))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7))) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6) && !(k == (1)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (2)) || (i == (2) && !(j == (6)))) && !(k == (2)) && (!(i == (2)) || (i == (2) && !(j == (6))) || (i == (2) && j == (6))) && (!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (8))) || (i == (5) && j == (8) && !(k == (1)))) && (!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6) && !(k == (4)))) && (!(i == (2)) || (i == (2) && !(j == (7))) || (i == (2) && j == (7) && !(k == (1)))) && !(i == (1)) && !(i == (-1)) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6) && !(k == (4)))) && !(j == (5)) && (!(i == (2)) || (i == (2) && !(k == (1)))) && i == (0) && j == (4) && k == (3)) || ((!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && !(j == (6)) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && !(k == (2)) && !(j == (5)) && (!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && !(i == (-1)) && !(i == (1)) && !(i == (2)) && !(k == (3)) && i == (0) && j == (4) && k == (1)) || ((!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (5)) && !(j == (6)) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (2)))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7) && !(k == (2)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8) && !(k == (2)))) && (!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7) && !(k == (2)))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && (!(i == (2)) || (i == (2) && !(j == (7)))) && !(j == (4)) && (!(i == (0)) || (i == (0) && !(k == (2)))) && i == (-1) && j == (3) && k == (1)) || ((!(i == (2)) || (i == (2) && !(j == (6))) || (i == (2) && j == (6))) && !(k == (1)) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5))) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4))) && (!(i == (1)) || (i == (1) && !(j == (5))) || (i == (1) && j == (5) && !(k == (4)))) && (!(i == (1)) || (i == (1) && !(j == (6))) || (i == (1) && j == (6))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5))) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6))) && (!(i == (-1)) || (i == (-1) && !(j == (6))) || (i == (-1) && j == (6))) && !(k == (2)) && (!(i == (0)) || (i == (0) && !(j == (6))) || (i == (0) && j == (6))) && (!(i == (2)) || (i == (2) && !(j == (4))) || (i == (2) && j == (4))) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5) && !(k == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (5)))) && (!(i == (2)) || (i == (2) && !(j == (5)))) && (!(i == (3)) || (i == (3) && !(j == (5))) || (i == (3) && j == (5) && !(k == (4)))) && (!(i == (1)) || (i == (1) && !(j == (5))) || (i == (1) && j == (5))) && (!(i == (2)) || (i == (2) && !(j == (6)))) && (!(i == (3)) || (i == (3) && !(j == (5)))) && (!(i == (0)) || (i == (0) && !(j == (4))) || (i == (0) && j == (4))) && (!(i == (0)) || (i == (0) && !(j == (5))) || (i == (0) && j == (5))) && (!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (3)) || (i == (3) && !(j == (5))) || (i == (3) && j == (5))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6) && !(k == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (4))) || (i == (-1) && j == (4))) && (!(i == (1)) || (i == (1) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (4)))) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6) && !(k == (4)))) && (!(i == (0)) || (i == (0) && !(j == (5)))) && (!(i == (1)) || (i == (1) && !(j == (5)))) && (!(i == (0)) || (i == (0) && !(j == (3))) || (i == (0) && j == (3))) && (!(i == (0)) || (i == (0) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (3))) || (i == (-1) && j == (3))) && i == (5) && j == (7) && k == (3)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && !(i == (1)) && (!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && !(i == (2)) && (!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(i == (0)) && (!(i == (4)) || (i == (4) && !(j == (7)))) && !(j == (5)) && (!(i == (5)) || (i == (5) && !(j == (8))) || (i == (5) && j == (8))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6) && !(k == (4)))) && !(k == (1)) && !(k == (3)) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6) && !(k == (4)))) && i == (-1) && j == (4) && k == (2)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && !(i == (1)) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (-1)) || (i == (-1) && !(j == (6))) || (i == (-1) && j == (6))) && !(i == (2)) && !(i == (3)) && !(k == (1)) && (!(i == (5)) || (i == (5) && !(j == (8))) || (i == (5) && j == (8))) && (!(i == (4)) || (i == (4) && !(j == (6)))) && !(k == (2)) && (!(i == (-1)) || (i == (-1) && !(j == (4))) || (i == (-1) && j == (4))) && !(k == (3)) && (!(i == (-1)) || (i == (-1) && !(j == (3))) || (i == (-1) && j == (3))) && i == (0) && j == (5) && k == (4)) || (!(j == (7)) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5) && !(k == (2)))) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4) && !(k == (2)))) && (!(i == (1)) || (i == (1) && !(j == (5))) || (i == (1) && j == (5) && !(k == (4)))) && !(i == (6)) && (!(i == (-1)) || (i == (-1) && !(j == (5)))) && (!(i == (2)) || (i == (2) && !(j == (5)))) && (!(i == (2)) || (i == (2) && !(j == (4))) || (i == (2) && j == (4) && !(k == (2)))) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5) && !(k == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5) && !(k == (3)))) && (!(i == (2)) || (i == (2) && !(j == (5))) || (i == (2) && j == (5) && !(k == (3)))) && (!(i == (3)) || (i == (3) && !(j == (5))) || (i == (3) && j == (5) && !(k == (4)))) && (!(i == (1)) || (i == (1) && !(j == (5)))) && !(j == (6)) && (!(i == (3)) || (i == (3) && !(j == (5))) || (i == (3) && j == (5) && !(k == (3)))) && (!(i == (0)) || (i == (0) && !(j == (4))) || (i == (0) && j == (4) && !(k == (2)))) && (!(i == (0)) || (i == (0) && !(j == (5)))) && (!(i == (1)) || (i == (1) && !(j == (5))) || (i == (1) && j == (5) && !(k == (2)))) && (!(i == (-1)) || (i == (-1) && !(j == (5))) || (i == (-1) && j == (5) && !(k == (2)))) && !(i == (5)) && (!(i == (3)) || (i == (3) && !(j == (5)))) && (!(i == (0)) || (i == (0) && !(j == (5))) || (i == (0) && j == (5) && !(k == (2)))) && (!(i == (-1)) || (i == (-1) && !(j == (4)))) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4) && !(k == (3)))) && (!(i == (-1)) || (i == (-1) && !(j == (4))) || (i == (-1) && j == (4) && !(k == (3)))) && (!(i == (1)) || (i == (1) && !(j == (4)))) && (!(i == (0)) || (i == (0) && !(j == (5))) || (i == (0) && j == (5) && !(k == (3)))) && (!(i == (2)) || (i == (2) && !(j == (4)))) && (!(i == (1)) || (i == (1) && !(j == (5))) || (i == (1) && j == (5) && !(k == (3)))) && (!(i == (0)) || (i == (0) && !(j == (3))) || (i == (0) && j == (3) && !(k == (2)))) && (!(i == (3)) || (i == (3) && !(j == (5))) || (i == (3) && j == (5) && !(k == (2)))) && (!(i == (0)) || (i == (0) && !(j == (4))) || (i == (0) && j == (4) && !(k == (3)))) && (!(i == (0)) || (i == (0) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (3)))) && (!(i == (-1)) || (i == (-1) && !(j == (4))) || (i == (-1) && j == (4) && !(k == (2)))) && (!(i == (0)) || (i == (0) && !(j == (5))) || (i == (0) && j == (5) && !(k == (4)))) && i == (4) && j == (8) && k == (1)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && !(k == (2)) && !(j == (5)) && !(j == (6)) && (!(i == (5)) || (i == (5) && !(j == (8))) || (i == (5) && j == (8))) && !(i == (1)) && !(i == (-1)) && !(k == (1)) && !(i == (0)) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (4)) || (i == (4) && !(j == (8))) || (i == (4) && j == (8))) && i == (2) && j == (4) && k == (3)) || ((!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && !(j == (6)) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && !(j == (5)) && (!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && (!(i == (2)) || (i == (2) && !(j == (7)))) && !(k == (2)) && !(j == (4)) && !(i == (-1)) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (3)))) && (!(i == (4)) || (i == (4) && !(j == (8)))) && i == (0) && j == (3) && k == (1)) || ((!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (2)))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7) && !(k == (2)))) && !(j == (5)) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8) && !(k == (2)))) && (!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7) && !(k == (2)))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && (!(i == (2)) || (i == (2) && !(j == (7)))) && !(j == (6)) && !(j == (4)) && !(i == (-1)) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (3)))) && (!(i == (4)) || (i == (4) && !(j == (8)))) && !(i == (0)) && i == (1) && j == (3) && k == (1)) || ((!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (5)) && !(j == (6)) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (2)))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7) && !(k == (2)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8) && !(k == (2)))) && (!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7) && !(k == (2)))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && (!(i == (2)) || (i == (2) && !(j == (7)))) && !(j == (4)) && !(j == (3)) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (3)))) && (!(i == (4)) || (i == (4) && !(j == (8)))) && i == (-1) && j == (2) && k == (1)) || ((!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (2)))) && !(j == (6)) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7) && !(k == (2)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8) && !(k == (2)))) && !(j == (5)) && (!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7) && !(k == (2)))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && (!(i == (2)) || (i == (2) && !(j == (7)))) && !(j == (4)) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (3)))) && (!(i == (4)) || (i == (4) && !(j == (8)))) && !(j == (3)) && !(i == (-1)) && i == (0) && j == (2) && k == (1)) || (!(i == (4)) && !(i == (3)) && !(i == (5)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (5)) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8) && !(k == (2)))) && !(i == (2)) && !(j == (6)) && !(j == (4)) && !(j == (3)) && (!(i == (-1)) || (i == (-1) && !(j == (2)))) && (!(i == (0)) || (i == (0) && !(j == (2)))) && i == (1) && j == (7) && k == (1)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (2)) || (i == (2) && !(j == (6))) || (i == (2) && j == (6))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && (!(i == (1)) || (i == (1) && !(j == (6)))) && (!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (2)) || (i == (2) && !(j == (6))) || (i == (2) && j == (6) && !(k == (3)))) && (!(i == (2)) || (i == (2) && !(j == (6)))) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6) && !(k == (3)))) && (!(i == (4)) || (i == (4) && !(j == (7)))) && !(j == (5)) && (!(i == (5)) || (i == (5) && !(j == (8))) || (i == (5) && j == (8))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6) && !(k == (3)))) && (!(i == (4)) || (i == (4) && !(j == (6))) || (i == (4) && j == (6) && !(k == (4)))) && (!(i == (2)) || (i == (2) && !(j == (7))) || (i == (2) && j == (7))) && (!(i == (1)) || (i == (1) && !(j == (6))) || (i == (1) && j == (6))) && (!(i == (3)) || (i == (3) && !(j == (6))) || (i == (3) && j == (6) && !(k == (4)))) && !(i == (0)) && !(k == (1)) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (3)))) && !(j == (4)) && (!(i == (4)) || (i == (4) && !(j == (8))) || (i == (4) && j == (8))) && (!(i == (1)) || (i == (1) && !(j == (7))) || (i == (1) && j == (7))) && i == (-1) && j == (3) && k == (2)) || ((!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && !(k == (2)) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && !(i == (2)) && !(i == (3)) && (!(i == (5)) || (i == (5) && !(j == (8))) || (i == (5) && j == (8))) && !(i == (4)) && !(j == (4)) && !(k == (1)) && !(j == (5)) && (!(i == (0)) || (i == (0) && !(j == (3))) || (i == (0) && j == (3))) && (!(i == (-1)) || (i == (-1) && !(j == (3))) || (i == (-1) && j == (3))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (-1)) || (i == (-1) && !(j == (2))) || (i == (-1) && j == (2))) && (!(i == (0)) || (i == (0) && !(j == (2))) || (i == (0) && j == (2))) && i == (1) && j == (6) && k == (3)) || ((!(i == (4)) || (i == (4) && !(j == (7))) || (i == (4) && j == (7))) && (!(i == (3)) || (i == (3) && !(j == (7))) || (i == (3) && j == (7))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && !(j == (4)) && !(j == (6)) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (5)) && (!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (8))) || (i == (5) && j == (8))) && (!(i == (2)) || (i == (2) && !(j == (7))) || (i == (2) && j == (7))) && !(i == (0)) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (3)))) && (!(i == (4)) || (i == (4) && !(j == (8))) || (i == (4) && j == (8))) && !(k == (1)) && !(i == (-1)) && i == (1) && j == (3) && k == (2)) || ((!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7))) && !(i == (1)) && !(i == (4)) && (!(i == (6)) || (i == (6) && !(j == (8))) || (i == (6) && j == (8))) && !(k == (1)) && (!(i == (5)) || (i == (5) && !(j == (7)))) && !(i == (3)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(i == (2)) && !(i == (0)) && !(j == (5)) && (!(i == (5)) || (i == (5) && !(j == (8))) || (i == (5) && j == (8))) && (!(i == (5)) || (i == (5) && !(j == (7))) || (i == (5) && j == (7) && !(k == (3)))) && !(j == (4)) && !(j == (3)) && i == (-1) && j == (6) && k == (2)) (../plain/insertion_sort-2.c:29:5)
[Warning][Witness] couldn't locate invariant: (i == (2) && j == (4) && k == (4)) || ((!(i == (2)) || (i == (2) && !(j == (4))) || (i == (2) && j == (4) && !(k == (4)))) && j == (1) && k == (1)) || (!(i == (2)) && (!(j == (1)) || (j == (1) && !(k == (1)))) && i == (0) && j == (4) && k == (4)) || ((!(i == (2)) || (i == (2) && !(j == (4))) || (i == (2) && j == (4) && !(k == (4)))) && (!(j == (1)) || (j == (1) && !(k == (1)))) && (!(j == (4)) || (j == (4) && !(k == (4)))) && i == (0) && j == (3) && k == (3)) || ((!(i == (2)) || (i == (2) && !(j == (4))) || (i == (2) && j == (4) && !(k == (4)))) && (!(j == (1)) || (j == (1) && !(k == (1)))) && (!(j == (4)) || (j == (4) && !(k == (4)))) && (!(j == (3)) || (j == (3) && !(k == (3)))) && i == (0) && j == (2) && k == (2)) || ((!(i == (2)) || (i == (2) && !(j == (4))) || (i == (2) && j == (4) && !(k == (4)))) && (!(j == (1)) || (j == (1) && !(k == (1)))) && !(i == (0)) && i == (-1) && j == (2) && k == (2)) || (!(i == (2)) && (!(j == (1)) || (j == (1) && !(k == (1)))) && !(i == (0)) && (!(j == (2)) || (j == (2) && !(k == (2)))) && i == (-1) && j == (4) && k == (4)) || (!(i == (2)) && (!(j == (1)) || (j == (1) && !(k == (1)))) && !(i == (0)) && !(i == (-1)) && i == (1) && j == (4) && k == (4)) || ((!(i == (2)) || (i == (2) && !(j == (4))) || (i == (2) && j == (4) && !(k == (4)))) && (!(j == (1)) || (j == (1) && !(k == (1)))) && !(i == (0)) && (!(j == (2)) || (j == (2) && !(k == (2)))) && (!(j == (4)) || (j == (4) && !(k == (4)))) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4) && !(k == (4)))) && i == (-1) && j == (3) && k == (3)) || ((!(i == (2)) || (i == (2) && !(j == (4))) || (i == (2) && j == (4) && !(k == (4)))) && (!(j == (1)) || (j == (1) && !(k == (1)))) && !(i == (0)) && (!(j == (4)) || (j == (4) && !(k == (4)))) && !(i == (-1)) && i == (1) && j == (3) && k == (3)) || ((!(j == (4)) || (j == (4) && !(k == (4)))) && (!(j == (1)) || (j == (1) && !(k == (1)))) && (!(i == (0)) || (i == (0) && !(j == (4))) || (i == (0) && j == (4) && !(k == (4)))) && (!(i == (0)) || (i == (0) && !(j == (3))) || (i == (0) && j == (3) && !(k == (3)))) && (!(i == (0)) || (i == (0) && !(j == (2))) || (i == (0) && j == (2) && !(k == (2)))) && (!(i == (-1)) || (i == (-1) && !(j == (2))) || (i == (-1) && j == (2) && !(k == (2)))) && (!(i == (-1)) || (i == (-1) && !(j == (4))) || (i == (-1) && j == (4) && !(k == (4)))) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4) && !(k == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (3))) || (i == (-1) && j == (3) && !(k == (3)))) && (!(i == (1)) || (i == (1) && !(j == (3))) || (i == (1) && j == (3) && !(k == (3)))) && i == (2) && j == (5) && k == (5)) || ((!(j == (1)) || (j == (1) && !(k == (1)))) && (!(i == (0)) || (i == (0) && !(j == (4))) || (i == (0) && j == (4) && !(k == (4)))) && (!(i == (0)) || (i == (0) && !(j == (3))) || (i == (0) && j == (3) && !(k == (3)))) && (!(i == (0)) || (i == (0) && !(j == (2))) || (i == (0) && j == (2) && !(k == (2)))) && (!(i == (-1)) || (i == (-1) && !(j == (2))) || (i == (-1) && j == (2) && !(k == (2)))) && (!(i == (-1)) || (i == (-1) && !(j == (4))) || (i == (-1) && j == (4) && !(k == (4)))) && (!(i == (1)) || (i == (1) && !(j == (4))) || (i == (1) && j == (4) && !(k == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (3))) || (i == (-1) && j == (3) && !(k == (3)))) && (!(i == (1)) || (i == (1) && !(j == (3))) || (i == (1) && j == (3) && !(k == (3)))) && !(i == (2)) && i == (3) && j == (5) && k == (5)) (../plain/insertion_sort-2.c:30:4)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/insertion_sort-2.c:17:8-17:23)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((j == 22 || (! (j == 22) && j == 11)) || ((! (j == 22) && ! (j == 11)) && j == 25)) || (((! (j == 22) && ! (j == 11)) && ! (j == 25)) && j == 27)) || ((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && j == 16)) || (((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && j == 8)) || ((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && j == 10)) || (((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && j == 3)) || ((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && j == 1)) || (((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && j == 2)) || ((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && j == 5)) || (((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && j == 12)) || ((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && j == 26)) || (((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && j == 9)) || ((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && j == 17)) || (((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && j == 0)) || ((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && j == 14)) || (((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && j == 18)) || ((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && j == 19)) || (((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && j == 6)) || ((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && j == 23)) || (((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && j == 15)) || ((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && j == 24)) || (((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && j == 28)) || ((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && j == 7)) || (((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && ! (j == 7)) && j == 13)) || ((((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && ! (j == 7)) && ! (j == 13)) && j == 4)) || (((((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && ! (j == 7)) && ! (j == 13)) && ! (j == 4)) && j == 20)) || ((((((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && ! (j == 7)) && ! (j == 13)) && ! (j == 4)) && ! (j == 20)) && j == 29)) || (((((((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && ! (j == 7)) && ! (j == 13)) && ! (j == 4)) && ! (j == 20)) && ! (j == 29)) && j == 21)) && (((((((((((((((((((((((((((((j == 22 || (! (j == 22) && j == 11)) || ((! (j == 22) && ! (j == 11)) && j == 25)) || (((! (j == 22) && ! (j == 11)) && ! (j == 25)) && j == 27)) || ((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && j == 16)) || (((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && j == 8)) || ((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && j == 10)) || (((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && j == 3)) || ((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && j == 1)) || (((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && j == 2)) || ((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && j == 5)) || (((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && j == 12)) || ((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && j == 26)) || (((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && j == 9)) || ((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && j == 17)) || (((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && j == 0)) || ((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && j == 14)) || (((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && j == 18)) || ((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && j == 19)) || (((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && j == 6)) || ((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && j == 23)) || (((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && j == 15)) || ((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && j == 24)) || (((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && j == 28)) || ((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && j == 7)) || (((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && ! (j == 7)) && j == 13)) || ((((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && ! (j == 7)) && ! (j == 13)) && j == 4)) || (((((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && ! (j == 7)) && ! (j == 13)) && ! (j == 4)) && j == 20)) || ((((((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && ! (j == 7)) && ! (j == 13)) && ! (j == 4)) && ! (j == 20)) && j == 29)) || (((((((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && ! (j == 7)) && ! (j == 13)) && ! (j == 4)) && ! (j == 20)) && ! (j == 29)) && j == 21)) (../plain/insertion_sort-2.c:19:8-19:23)
[Info][Witness] unassume invariant: ((((((((((((((((((((((((((((((((((i == 4 && j == 6) || (((! (i == 4) || (i == 4 && ! (j == 6))) && i == 3) && j == 5)) || (((! (i == 4) && ! (j == 5)) && i == 3) && j == 6)) || (((((! (i == 4) || (i == 4 && ! (j == 6))) && (! (i == 3) || (i == 3 && ! (j == 5)))) && (! (i == 3) || (i == 3 && ! (j == 6)))) && i == 5) && j == 7)) || (((((! (i == 4) || (i == 4 && ! (j == 6))) && ! (i == 3)) && (! (i == 5) || (i == 5 && ! (j == 7)))) && i == 2) && j == 5)) || ((((((! (i == 4) || (i == 4 && ! (j == 6))) && ! (i == 3)) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (i == 2)) && i == 0) && j == 5)) || ((((((((! (i == 4) || (i == 4 && ! (j == 6))) && (! (i == 3) || (i == 3 && ! (j == 5)))) && (! (i == 3) || (i == 3 && ! (j == 6)))) && (! (i == 5) || (i == 5 && ! (j == 7)))) && (! (i == 2) || (i == 2 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 5)))) && i == 1) && j == 4)) || ((((((((! (i == 4) || (i == 4 && ! (j == 6))) && ! (i == 3)) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (i == 2)) && ! (i == 0)) && (! (i == 1) || (i == 1 && ! (j == 4)))) && i == -1) && j == 5)) || ((((((! (i == 4) && ! (i == 3)) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (j == 5)) && (! (i == 1) || (i == 1 && ! (j == 4)))) && i == 2) && j == 6)) || (((((((! (i == 4) && ! (i == 3)) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (j == 5)) && (! (i == 1) || (i == 1 && ! (j == 4)))) && ! (i == 2)) && i == 0) && j == 6)) || ((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 5)) && ! (i == 1)) && ! (j == 6)) && i == 2) && j == 4)) || ((((((((((! (i == 4) || (i == 4 && ! (j == 6))) && (! (i == 3) || (i == 3 && ! (j == 6)))) && (! (i == 5) || (i == 5 && ! (j == 7)))) && (! (i == 1) || (i == 1 && ! (j == 4)))) && ! (j == 5)) && (! (i == 2) || (i == 2 && ! (j == 6)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && (! (i == 2) || (i == 2 && ! (j == 4)))) && i == -1) && j == 3)) || ((((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 5)) && ! (i == 1)) && ! (j == 6)) && ! (i == 2)) && (! (i == -1) || (i == -1 && ! (j == 3)))) && i == 0) && j == 4)) || ((((((((((((! (i == 4) || (i == 4 && ! (j == 6))) && (! (i == 3) || (i == 3 && ! (j == 6)))) && (! (i == 5) || (i == 5 && ! (j == 7)))) && (! (i == 1) || (i == 1 && ! (j == 4)))) && ! (j == 5)) && (! (i == 2) || (i == 2 && ! (j == 6)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && (! (i == 2) || (i == 2 && ! (j == 4)))) && ! (j == 3)) && (! (i == 0) || (i == 0 && ! (j == 4)))) && i == -1) && j == 2)) || (((((((((! (i == 4) || (i == 4 && ! (j == 6))) && ! (i == 3)) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (i == 2)) && ! (i == 0)) && ! (j == 4)) && ! (i == -1)) && i == 1) && j == 5)) || (((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 5)) && ! (j == 6)) && ! (i == -1)) && ! (j == 4)) && i == 0) && j == 3)) || (((((((((((! (i == 4) || (i == 4 && ! (j == 6))) && (! (i == 3) || (i == 3 && ! (j == 6)))) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (i == 1)) && ! (j == 5)) && ! (i == 2)) && ! (j == 3)) && ! (i == 0)) && ! (j == 2)) && i == -1) && j == 4)) || (((((((((((((((((((! (i == 4) || (i == 4 && ! (j == 6))) && (! (i == 3) || (i == 3 && ! (j == 5)))) && (! (i == 3) || (i == 3 && ! (j == 6)))) && (! (i == 5) || (i == 5 && ! (j == 7)))) && (! (i == 2) || (i == 2 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 5)))) && (! (i == 1) || (i == 1 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 5)))) && (! (i == 2) || (i == 2 && ! (j == 6)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && (! (i == 2) || (i == 2 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == 0) || (i == 0 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && (! (i == 1) || (i == 1 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 4)))) && i == 6) && j == 8)) || (((((((((((! (i == 4) && ! (i == 3)) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (j == 4)) && ! (i == 2)) && ! (i == 0)) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && ! (j == 5)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && i == 1) && j == 6)) || (((((((((((((! (i == 4) || (i == 4 && ! (j == 6))) && (! (i == 3) || (i == 3 && ! (j == 6)))) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (j == 5)) && (! (i == 2) || (i == 2 && ! (j == 6)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && ! (j == 3)) && ! (j == 2)) && ! (j == 4)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 1) || (i == 1 && ! (j == 6)))) && i == -1) && j == 1)) || (((((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 5)) && ! (j == 6)) && ! (j == 4)) && ! (i == -1)) && ! (j == 3)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && i == 0) && j == 2)) || ((((((((((((((! (j == 5) && ! (j == 6)) && ! (i == 5)) && (! (i == 1) || (i == 1 && ! (j == 4)))) && (! (i == 2) || (i == 2 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == 0) || (i == 0 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && (! (i == 0) || (i == 0 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 4)))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == -1) || (i == -1 && ! (j == 1)))) && (! (i == 0) || (i == 0 && ! (j == 2)))) && i == 3) && j == 7)) || ((((((((((((((((((! (j == 6) && ! (i == 5)) && (! (i == 2) || (i == 2 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 5)))) && (! (i == 1) || (i == 1 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 5)))) && (! (i == 2) || (i == 2 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == 0) || (i == 0 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && (! (i == 1) || (i == 1 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 4)))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == -1) || (i == -1 && ! (j == 1)))) && (! (i == 0) || (i == 0 && ! (j == 2)))) && ! (i == 3)) && i == 4) && j == 7)) || (((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 4)) && ! (i == -1)) && ! (j == 5)) && ! (i == 0)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (j == 6)) && (! (i == 3) || (i == 3 && ! (j == 7)))) && (! (i == 4) || (i == 4 && ! (j == 7)))) && i == 1) && j == 3)) || (((((((((((((! (i == 4) && ! (i == 3)) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (j == 5)) && ! (i == 2)) && ! (i == 0)) && ! (j == 3)) && ! (j == 2)) && ! (j == 4)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (i == 1)) && ! (j == 1)) && i == -1) && j == 6)) || ((((((((((((((! (i == 5) && ! (j == 5)) && ! (j == 6)) && ! (j == 4)) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && (! (i == 0) || (i == 0 && ! (j == 3)))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == -1) || (i == -1 && ! (j == 1)))) && (! (i == 0) || (i == 0 && ! (j == 2)))) && ! (i == 3)) && ! (i == 4)) && (! (i == 1) || (i == 1 && ! (j == 3)))) && i == 2) && j == 7)) || (((((((((((((((((((((((((! (i == 4) || (i == 4 && ! (j == 6))) && (! (i == 3) || (i == 3 && ! (j == 5)))) && (! (i == 3) || (i == 3 && ! (j == 6)))) && ! (j == 7)) && (! (i == 2) || (i == 2 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 5)))) && (! (i == 1) || (i == 1 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 5)))) && (! (i == 2) || (i == 2 && ! (j == 6)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && (! (i == 2) || (i == 2 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == 0) || (i == 0 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && (! (i == 1) || (i == 1 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 4)))) && ! (i == 6)) && (! (i == 1) || (i == 1 && ! (j == 6)))) && (! (i == -1) || (i == -1 && ! (j == 1)))) && (! (i == 0) || (i == 0 && ! (j == 2)))) && (! (i == 1) || (i == 1 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 6)))) && i == 5) && j == 8)) || ((((((((((! (j == 6) && ! (i == 3)) && ! (i == 2)) && ! (i == 0)) && ! (i == -1)) && ! (i == 1)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (j == 7)) && (! (i == 5) || (i == 5 && ! (j == 8)))) && i == 4) && j == 5)) || (((((((((! (i == 4) && ! (i == 3)) && ! (j == 7)) && ! (i == 2)) && ! (i == 0)) && ! (i == 1)) && ! (i == -1)) && ! (j == 8)) && i == 5) && j == 6)) || (((((((((((((((((((((! (i == 5) && (! (i == 0) || (i == 0 && ! (j == 5)))) && (! (i == 1) || (i == 1 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == 0) || (i == 0 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && (! (i == 1) || (i == 1 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 4)))) && ! (j == 8)) && (! (i == 1) || (i == 1 && ! (j == 6)))) && (! (i == -1) || (i == -1 && ! (j == 1)))) && (! (i == 0) || (i == 0 && ! (j == 2)))) && ! (i == 3)) && ! (i == 4)) && (! (i == 1) || (i == 1 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 6)))) && ! (i == 2)) && i == 6) && j == 7)) || ((((((((((! (j == 5) && ! (j == 6)) && ! (i == 1)) && ! (i == 2)) && ! (i == 0)) && ! (i == -1)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (j == 7)) && (! (i == 5) || (i == 5 && ! (j == 8)))) && i == 3) && j == 4)) || (((((((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 4)) && ! (i == -1)) && ! (j == 5)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (j == 6)) && ! (i == 0)) && (! (i == 3) || (i == 3 && ! (j == 7)))) && (! (i == 4) || (i == 4 && ! (j == 7)))) && ! (j == 3)) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && (! (i == 6) || (i == 6 && ! (j == 7)))) && i == 1) && j == 2)) || ((((((((((! (j == 5) && ! (j == 6)) && ! (j == 4)) && ! (i == -1)) && ! (i == 0)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (i == 1)) && ! (j == 7)) && (! (i == 5) || (i == 5 && ! (j == 8)))) && i == 2) && j == 3)) || ((((((((((((((((((((((((((((((((! (i == 4) || (i == 4 && ! (j == 6))) && (! (i == 3) || (i == 3 && ! (j == 5)))) && (! (i == 3) || (i == 3 && ! (j == 6)))) && (! (i == 2) || (i == 2 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 5)))) && (! (i == 1) || (i == 1 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 5)))) && (! (i == 2) || (i == 2 && ! (j == 6)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && (! (i == 2) || (i == 2 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == 0) || (i == 0 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && (! (i == 1) || (i == 1 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 4)))) && ! (i == 6)) && (! (i == 1) || (i == 1 && ! (j == 6)))) && (! (i == -1) || (i == -1 && ! (j == 1)))) && (! (i == 0) || (i == 0 && ! (j == 2)))) && (! (i == 3) || (i == 3 && ! (j == 7)))) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 1) || (i == 1 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 6)))) && (! (i == 2) || (i == 2 && ! (j == 7)))) && ! (i == 5)) && (! (i == 4) || (i == 4 && ! (j == 5)))) && (! (i == 3) || (i == 3 && ! (j == 4)))) && (! (i == 1) || (i == 1 && ! (j == 2)))) && (! (i == 2) || (i == 2 && ! (j == 3)))) && i == 7) && j == 8)) || ((((((((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 5)) && ! (j == 6)) && ! (j == 4)) && ! (j == 3)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (i == -1)) && ! (j == 2)) && (! (i == 3) || (i == 3 && ! (j == 7)))) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && (! (i == 6) || (i == 6 && ! (j == 7)))) && (! (i == 7) || (i == 7 && ! (j == 8)))) && i == 0) && j == 1) (../plain/insertion_sort-2.c:24:10-24:19)
[Info][Witness] unassume invariant: ((((((((((((((((((((((((((((((((((i == 4 && j == 6) || (((! (i == 4) || (i == 4 && ! (j == 6))) && i == 3) && j == 5)) || (((! (i == 4) && ! (j == 5)) && i == 3) && j == 6)) || (((((! (i == 4) || (i == 4 && ! (j == 6))) && (! (i == 3) || (i == 3 && ! (j == 5)))) && (! (i == 3) || (i == 3 && ! (j == 6)))) && i == 5) && j == 7)) || (((((! (i == 4) || (i == 4 && ! (j == 6))) && ! (i == 3)) && (! (i == 5) || (i == 5 && ! (j == 7)))) && i == 2) && j == 5)) || ((((((! (i == 4) || (i == 4 && ! (j == 6))) && ! (i == 3)) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (i == 2)) && i == 0) && j == 5)) || ((((((((! (i == 4) || (i == 4 && ! (j == 6))) && (! (i == 3) || (i == 3 && ! (j == 5)))) && (! (i == 3) || (i == 3 && ! (j == 6)))) && (! (i == 5) || (i == 5 && ! (j == 7)))) && (! (i == 2) || (i == 2 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 5)))) && i == 1) && j == 4)) || ((((((((! (i == 4) || (i == 4 && ! (j == 6))) && ! (i == 3)) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (i == 2)) && ! (i == 0)) && (! (i == 1) || (i == 1 && ! (j == 4)))) && i == -1) && j == 5)) || ((((((! (i == 4) && ! (i == 3)) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (j == 5)) && (! (i == 1) || (i == 1 && ! (j == 4)))) && i == 2) && j == 6)) || (((((((! (i == 4) && ! (i == 3)) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (j == 5)) && (! (i == 1) || (i == 1 && ! (j == 4)))) && ! (i == 2)) && i == 0) && j == 6)) || ((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 5)) && ! (i == 1)) && ! (j == 6)) && i == 2) && j == 4)) || ((((((((((! (i == 4) || (i == 4 && ! (j == 6))) && (! (i == 3) || (i == 3 && ! (j == 6)))) && (! (i == 5) || (i == 5 && ! (j == 7)))) && (! (i == 1) || (i == 1 && ! (j == 4)))) && ! (j == 5)) && (! (i == 2) || (i == 2 && ! (j == 6)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && (! (i == 2) || (i == 2 && ! (j == 4)))) && i == -1) && j == 3)) || ((((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 5)) && ! (i == 1)) && ! (j == 6)) && ! (i == 2)) && (! (i == -1) || (i == -1 && ! (j == 3)))) && i == 0) && j == 4)) || ((((((((((((! (i == 4) || (i == 4 && ! (j == 6))) && (! (i == 3) || (i == 3 && ! (j == 6)))) && (! (i == 5) || (i == 5 && ! (j == 7)))) && (! (i == 1) || (i == 1 && ! (j == 4)))) && ! (j == 5)) && (! (i == 2) || (i == 2 && ! (j == 6)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && (! (i == 2) || (i == 2 && ! (j == 4)))) && ! (j == 3)) && (! (i == 0) || (i == 0 && ! (j == 4)))) && i == -1) && j == 2)) || (((((((((! (i == 4) || (i == 4 && ! (j == 6))) && ! (i == 3)) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (i == 2)) && ! (i == 0)) && ! (j == 4)) && ! (i == -1)) && i == 1) && j == 5)) || (((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 5)) && ! (j == 6)) && ! (i == -1)) && ! (j == 4)) && i == 0) && j == 3)) || (((((((((((! (i == 4) || (i == 4 && ! (j == 6))) && (! (i == 3) || (i == 3 && ! (j == 6)))) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (i == 1)) && ! (j == 5)) && ! (i == 2)) && ! (j == 3)) && ! (i == 0)) && ! (j == 2)) && i == -1) && j == 4)) || (((((((((((((((((((! (i == 4) || (i == 4 && ! (j == 6))) && (! (i == 3) || (i == 3 && ! (j == 5)))) && (! (i == 3) || (i == 3 && ! (j == 6)))) && (! (i == 5) || (i == 5 && ! (j == 7)))) && (! (i == 2) || (i == 2 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 5)))) && (! (i == 1) || (i == 1 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 5)))) && (! (i == 2) || (i == 2 && ! (j == 6)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && (! (i == 2) || (i == 2 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == 0) || (i == 0 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && (! (i == 1) || (i == 1 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 4)))) && i == 6) && j == 8)) || (((((((((((! (i == 4) && ! (i == 3)) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (j == 4)) && ! (i == 2)) && ! (i == 0)) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && ! (j == 5)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && i == 1) && j == 6)) || (((((((((((((! (i == 4) || (i == 4 && ! (j == 6))) && (! (i == 3) || (i == 3 && ! (j == 6)))) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (j == 5)) && (! (i == 2) || (i == 2 && ! (j == 6)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && ! (j == 3)) && ! (j == 2)) && ! (j == 4)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 1) || (i == 1 && ! (j == 6)))) && i == -1) && j == 1)) || (((((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 5)) && ! (j == 6)) && ! (j == 4)) && ! (i == -1)) && ! (j == 3)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && i == 0) && j == 2)) || ((((((((((((((! (j == 5) && ! (j == 6)) && ! (i == 5)) && (! (i == 1) || (i == 1 && ! (j == 4)))) && (! (i == 2) || (i == 2 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == 0) || (i == 0 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && (! (i == 0) || (i == 0 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 4)))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == -1) || (i == -1 && ! (j == 1)))) && (! (i == 0) || (i == 0 && ! (j == 2)))) && i == 3) && j == 7)) || ((((((((((((((((((! (j == 6) && ! (i == 5)) && (! (i == 2) || (i == 2 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 5)))) && (! (i == 1) || (i == 1 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 5)))) && (! (i == 2) || (i == 2 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == 0) || (i == 0 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && (! (i == 1) || (i == 1 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 4)))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == -1) || (i == -1 && ! (j == 1)))) && (! (i == 0) || (i == 0 && ! (j == 2)))) && ! (i == 3)) && i == 4) && j == 7)) || (((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 4)) && ! (i == -1)) && ! (j == 5)) && ! (i == 0)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (j == 6)) && (! (i == 3) || (i == 3 && ! (j == 7)))) && (! (i == 4) || (i == 4 && ! (j == 7)))) && i == 1) && j == 3)) || (((((((((((((! (i == 4) && ! (i == 3)) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (j == 5)) && ! (i == 2)) && ! (i == 0)) && ! (j == 3)) && ! (j == 2)) && ! (j == 4)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (i == 1)) && ! (j == 1)) && i == -1) && j == 6)) || ((((((((((((((! (i == 5) && ! (j == 5)) && ! (j == 6)) && ! (j == 4)) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && (! (i == 0) || (i == 0 && ! (j == 3)))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == -1) || (i == -1 && ! (j == 1)))) && (! (i == 0) || (i == 0 && ! (j == 2)))) && ! (i == 3)) && ! (i == 4)) && (! (i == 1) || (i == 1 && ! (j == 3)))) && i == 2) && j == 7)) || (((((((((((((((((((((((((! (i == 4) || (i == 4 && ! (j == 6))) && (! (i == 3) || (i == 3 && ! (j == 5)))) && (! (i == 3) || (i == 3 && ! (j == 6)))) && ! (j == 7)) && (! (i == 2) || (i == 2 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 5)))) && (! (i == 1) || (i == 1 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 5)))) && (! (i == 2) || (i == 2 && ! (j == 6)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && (! (i == 2) || (i == 2 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == 0) || (i == 0 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && (! (i == 1) || (i == 1 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 4)))) && ! (i == 6)) && (! (i == 1) || (i == 1 && ! (j == 6)))) && (! (i == -1) || (i == -1 && ! (j == 1)))) && (! (i == 0) || (i == 0 && ! (j == 2)))) && (! (i == 1) || (i == 1 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 6)))) && i == 5) && j == 8)) || ((((((((((! (j == 6) && ! (i == 3)) && ! (i == 2)) && ! (i == 0)) && ! (i == -1)) && ! (i == 1)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (j == 7)) && (! (i == 5) || (i == 5 && ! (j == 8)))) && i == 4) && j == 5)) || (((((((((! (i == 4) && ! (i == 3)) && ! (j == 7)) && ! (i == 2)) && ! (i == 0)) && ! (i == 1)) && ! (i == -1)) && ! (j == 8)) && i == 5) && j == 6)) || (((((((((((((((((((((! (i == 5) && (! (i == 0) || (i == 0 && ! (j == 5)))) && (! (i == 1) || (i == 1 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == 0) || (i == 0 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && (! (i == 1) || (i == 1 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 4)))) && ! (j == 8)) && (! (i == 1) || (i == 1 && ! (j == 6)))) && (! (i == -1) || (i == -1 && ! (j == 1)))) && (! (i == 0) || (i == 0 && ! (j == 2)))) && ! (i == 3)) && ! (i == 4)) && (! (i == 1) || (i == 1 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 6)))) && ! (i == 2)) && i == 6) && j == 7)) || ((((((((((! (j == 5) && ! (j == 6)) && ! (i == 1)) && ! (i == 2)) && ! (i == 0)) && ! (i == -1)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (j == 7)) && (! (i == 5) || (i == 5 && ! (j == 8)))) && i == 3) && j == 4)) || (((((((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 4)) && ! (i == -1)) && ! (j == 5)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (j == 6)) && ! (i == 0)) && (! (i == 3) || (i == 3 && ! (j == 7)))) && (! (i == 4) || (i == 4 && ! (j == 7)))) && ! (j == 3)) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && (! (i == 6) || (i == 6 && ! (j == 7)))) && i == 1) && j == 2)) || ((((((((((! (j == 5) && ! (j == 6)) && ! (j == 4)) && ! (i == -1)) && ! (i == 0)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (i == 1)) && ! (j == 7)) && (! (i == 5) || (i == 5 && ! (j == 8)))) && i == 2) && j == 3)) || ((((((((((((((((((((((((((((((((! (i == 4) || (i == 4 && ! (j == 6))) && (! (i == 3) || (i == 3 && ! (j == 5)))) && (! (i == 3) || (i == 3 && ! (j == 6)))) && (! (i == 2) || (i == 2 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 5)))) && (! (i == 1) || (i == 1 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 5)))) && (! (i == 2) || (i == 2 && ! (j == 6)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && (! (i == 2) || (i == 2 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == 0) || (i == 0 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && (! (i == 1) || (i == 1 && ! (j == 5)))) && (! (i == 0) || (i == 0 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 4)))) && ! (i == 6)) && (! (i == 1) || (i == 1 && ! (j == 6)))) && (! (i == -1) || (i == -1 && ! (j == 1)))) && (! (i == 0) || (i == 0 && ! (j == 2)))) && (! (i == 3) || (i == 3 && ! (j == 7)))) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 1) || (i == 1 && ! (j == 3)))) && (! (i == -1) || (i == -1 && ! (j == 6)))) && (! (i == 2) || (i == 2 && ! (j == 7)))) && ! (i == 5)) && (! (i == 4) || (i == 4 && ! (j == 5)))) && (! (i == 3) || (i == 3 && ! (j == 4)))) && (! (i == 1) || (i == 1 && ! (j == 2)))) && (! (i == 2) || (i == 2 && ! (j == 3)))) && i == 7) && j == 8)) || ((((((((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 5)) && ! (j == 6)) && ! (j == 4)) && ! (j == 3)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (i == -1)) && ! (j == 2)) && (! (i == 3) || (i == 3 && ! (j == 7)))) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && (! (i == 6) || (i == 6 && ! (j == 7)))) && (! (i == 7) || (i == 7 && ! (j == 8)))) && i == 0) && j == 1) (../plain/insertion_sort-2.c:21:7-21:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/insertion_sort-2.c:19:8-19:23)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((j == 22 || (! (j == 22) && j == 11)) || ((! (j == 22) && ! (j == 11)) && j == 25)) || (((! (j == 22) && ! (j == 11)) && ! (j == 25)) && j == 27)) || ((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && j == 16)) || (((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && j == 8)) || ((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && j == 10)) || (((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && j == 3)) || ((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && j == 1)) || (((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && j == 2)) || ((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && j == 5)) || (((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && j == 12)) || ((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && j == 26)) || (((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && j == 9)) || ((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && j == 17)) || (((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && j == 0)) || ((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && j == 14)) || (((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && j == 18)) || ((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && j == 19)) || (((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && j == 6)) || ((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && j == 23)) || (((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && j == 15)) || ((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && j == 24)) || (((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && j == 28)) || ((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && j == 7)) || (((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && ! (j == 7)) && j == 13)) || ((((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && ! (j == 7)) && ! (j == 13)) && j == 4)) || (((((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && ! (j == 7)) && ! (j == 13)) && ! (j == 4)) && j == 20)) || ((((((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && ! (j == 7)) && ! (j == 13)) && ! (j == 4)) && ! (j == 20)) && j == 29)) || (((((((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && ! (j == 7)) && ! (j == 13)) && ! (j == 4)) && ! (j == 20)) && ! (j == 29)) && j == 21)) && (((((((((((((((((((((((((((((j == 22 || (! (j == 22) && j == 11)) || ((! (j == 22) && ! (j == 11)) && j == 25)) || (((! (j == 22) && ! (j == 11)) && ! (j == 25)) && j == 27)) || ((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && j == 16)) || (((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && j == 8)) || ((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && j == 10)) || (((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && j == 3)) || ((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && j == 1)) || (((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && j == 2)) || ((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && j == 5)) || (((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && j == 12)) || ((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && j == 26)) || (((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && j == 9)) || ((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && j == 17)) || (((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && j == 0)) || ((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && j == 14)) || (((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && j == 18)) || ((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && j == 19)) || (((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && j == 6)) || ((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && j == 23)) || (((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && j == 15)) || ((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && j == 24)) || (((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && j == 28)) || ((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && j == 7)) || (((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && ! (j == 7)) && j == 13)) || ((((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && ! (j == 7)) && ! (j == 13)) && j == 4)) || (((((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && ! (j == 7)) && ! (j == 13)) && ! (j == 4)) && j == 20)) || ((((((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && ! (j == 7)) && ! (j == 13)) && ! (j == 4)) && ! (j == 20)) && j == 29)) || (((((((((((((((((((((((((((((! (j == 22) && ! (j == 11)) && ! (j == 25)) && ! (j == 27)) && ! (j == 16)) && ! (j == 8)) && ! (j == 10)) && ! (j == 3)) && ! (j == 1)) && ! (j == 2)) && ! (j == 5)) && ! (j == 12)) && ! (j == 26)) && ! (j == 9)) && ! (j == 17)) && ! (j == 0)) && ! (j == 14)) && ! (j == 18)) && ! (j == 19)) && ! (j == 6)) && ! (j == 23)) && ! (j == 15)) && ! (j == 24)) && ! (j == 28)) && ! (j == 7)) && ! (j == 13)) && ! (j == 4)) && ! (j == 20)) && ! (j == 29)) && j == 21)) (../plain/insertion_sort-2.c:19:8-19:23)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((i == 3 && j == 6) || (((! (i == 3) || (i == 3 && ! (j == 6))) && i == 5) && j == 7)) || (((! (i == 3) && (! (i == 5) || (i == 5 && ! (j == 7)))) && i == -1) && j == 6)) || (((((! (i == 3) || (i == 3 && ! (j == 6))) && (! (i == 5) || (i == 5 && ! (j == 7)))) && (! (i == -1) || (i == -1 && ! (j == 6)))) && i == 6) && j == 8)) || (((((! (i == 3) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (i == -1)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && i == 4) && j == 6)) || ((((((! (i == 3) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (i == -1)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (i == 4)) && i == 0) && j == 6)) || ((((((((! (i == 3) || (i == 3 && ! (j == 6))) && ! (i == 5)) && (! (i == -1) || (i == -1 && ! (j == 6)))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 4) || (i == 4 && ! (j == 6)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && i == 2) && j == 7)) || ((((((((! (i == 3) || (i == 3 && ! (j == 6))) && ! (j == 7)) && (! (i == -1) || (i == -1 && ! (j == 6)))) && ! (i == 6)) && (! (i == 4) || (i == 4 && ! (j == 6)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && i == 5) && j == 8)) || ((((((! (j == 6) && (! (i == 5) || (i == 5 && ! (j == 7)))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && i == 3) && j == 5)) || ((((((((! (i == 3) && ! (i == -1)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (i == 4)) && ! (i == 0)) && ! (j == 7)) && (! (i == 5) || (i == 5 && ! (j == 8)))) && i == 2) && j == 6)) || (((((((((! (i == 3) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (i == -1)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (i == 4)) && ! (i == 0)) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (i == 2)) && i == 1) && j == 6)) || ((((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 6)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (i == 3)) && i == -1) && j == 5)) || ((((((((! (i == 6) || (i == 6 && ! (j == 8))) && ! (j == 7)) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (i == 3)) && ! (j == 6)) && ! (i == -1)) && i == 2) && j == 5)) || (((((((! (i == 5) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (j == 6)) && ! (i == 2)) && (! (i == 3) || (i == 3 && ! (j == 5)))) && (! (i == -1) || (i == -1 && ! (j == 5)))) && i == 4) && j == 7)) || (((((((! (j == 6) && ! (i == 5)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (i == 2)) && ! (j == 5)) && ! (i == 4)) && i == 3) && j == 7)) || ((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 6)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (j == 5)) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 3) || (i == 3 && ! (j == 7)))) && i == -1) && j == 4)) || (((((((((! (i == 6) && ! (j == 6)) && ! (i == 5)) && (! (i == 3) || (i == 3 && ! (j == 5)))) && (! (i == -1) || (i == -1 && ! (j == 5)))) && (! (i == 2) || (i == 2 && ! (j == 5)))) && ! (j == 7)) && (! (i == -1) || (i == -1 && ! (j == 4)))) && i == 4) && j == 8)) || (((((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (j == 6)) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && (! (i == 3) || (i == 3 && ! (j == 5)))) && (! (i == 2) || (i == 2 && ! (j == 5)))) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 3) || (i == 3 && ! (j == 7)))) && ! (i == -1)) && (! (i == 4) || (i == 4 && ! (j == 8)))) && i == 0) && j == 4)) || ((((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (j == 6)) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (i == 3)) && ! (i == -1)) && ! (i == 2)) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 4) || (i == 4 && ! (j == 8)))) && ! (j == 4)) && i == 0) && j == 5)) || ((((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (i == 3)) && ! (j == 6)) && ! (i == -1)) && ! (i == 2)) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 4) || (i == 4 && ! (j == 8)))) && ! (i == 0)) && i == 1) && j == 5)) || (((((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (j == 6)) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 3) || (i == 3 && ! (j == 7)))) && ! (i == -1)) && (! (i == 4) || (i == 4 && ! (j == 8)))) && ! (i == 0)) && ! (j == 5)) && i == 1) && j == 4)) || ((((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 6)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (j == 5)) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 3) || (i == 3 && ! (j == 7)))) && ! (j == 4)) && (! (i == 4) || (i == 4 && ! (j == 8)))) && i == -1) && j == 3)) || (((((((((((! (i == 6) || (i == 6 && ! (j == 8))) && ! (j == 7)) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (j == 6)) && ! (j == 5)) && ! (i == -1)) && (! (i == 4) || (i == 4 && ! (j == 8)))) && ! (i == 0)) && ! (i == 1)) && i == 2) && j == 4)) || (((((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (j == 6)) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 3) || (i == 3 && ! (j == 7)))) && (! (i == 4) || (i == 4 && ! (j == 8)))) && ! (j == 4)) && ! (j == 5)) && (! (i == -1) || (i == -1 && ! (j == 3)))) && i == 0) && j == 2)) || (((((((((((! (i == 5) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (i == 2)) && ! (j == 6)) && ! (i == 4)) && ! (i == 3)) && ! (j == 5)) && ! (j == 4)) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == 0) || (i == 0 && ! (j == 2)))) && i == 1) && j == 7)) || (((((((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 6)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (j == 5)) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 3) || (i == 3 && ! (j == 7)))) && ! (j == 4)) && (! (i == 4) || (i == 4 && ! (j == 8)))) && ! (j == 3)) && ! (i == 0)) && (! (i == 1) || (i == 1 && ! (j == 7)))) && i == -1) && j == 2)) || (((((((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (j == 6)) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 3) || (i == 3 && ! (j == 7)))) && (! (i == 4) || (i == 4 && ! (j == 8)))) && ! (j == 4)) && ! (j == 5)) && ! (i == -1)) && ! (j == 2)) && (! (i == 1) || (i == 1 && ! (j == 7)))) && i == 0) && j == 3)) || ((((((((((((((((((((((((((((! (i == 3) || (i == 3 && ! (j == 6))) && (! (i == 5) || (i == 5 && ! (j == 7)))) && (! (i == -1) || (i == -1 && ! (j == 6)))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 4) || (i == 4 && ! (j == 6)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && (! (i == 3) || (i == 3 && ! (j == 5)))) && (! (i == 2) || (i == 2 && ! (j == 6)))) && (! (i == 1) || (i == 1 && ! (j == 6)))) && (! (i == -1) || (i == -1 && ! (j == 5)))) && (! (i == 2) || (i == 2 && ! (j == 5)))) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 3) || (i == 3 && ! (j == 7)))) && (! (i == -1) || (i == -1 && ! (j == 4)))) && (! (i == 4) || (i == 4 && ! (j == 8)))) && (! (i == 0) || (i == 0 && ! (j == 4)))) && (! (i == 0) || (i == 0 && ! (j == 5)))) && (! (i == 1) || (i == 1 && ! (j == 5)))) && (! (i == 1) || (i == 1 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == 2) || (i == 2 && ! (j == 4)))) && (! (i == 0) || (i == 0 && ! (j == 2)))) && (! (i == 1) || (i == 1 && ! (j == 7)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && (! (i == 0) || (i == 0 && ! (j == 3)))) && j == 1)) || (((((((((((((! (i == 5) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (j == 6)) && ! (i == 2)) && ! (i == 4)) && ! (i == 3)) && ! (j == 4)) && ! (j == 5)) && ! (j == 2)) && ! (i == 1)) && ! (j == 3)) && ! (j == 1)) && i == 0) && j == 7)) || ((((((((((((((((! (j == 1) && ! (j == 6)) && ! (i == 6)) && ! (i == 5)) && ! (j == 5)) && ! (j == 7)) && (! (i == -1) || (i == -1 && ! (j == 4)))) && ! (i == 4)) && (! (i == 0) || (i == 0 && ! (j == 4)))) && (! (i == 1) || (i == 1 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == 2) || (i == 2 && ! (j == 4)))) && (! (i == 0) || (i == 0 && ! (j == 2)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && (! (i == 0) || (i == 0 && ! (j == 3)))) && i == 3) && j == 8)) || (((((((((((((((((((((((((((((((! (j == 1) && (! (i == 3) || (i == 3 && ! (j == 6)))) && (! (i == 5) || (i == 5 && ! (j == 7)))) && (! (i == -1) || (i == -1 && ! (j == 6)))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 4) || (i == 4 && ! (j == 6)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && (! (i == 3) || (i == 3 && ! (j == 5)))) && (! (i == 2) || (i == 2 && ! (j == 6)))) && (! (i == 1) || (i == 1 && ! (j == 6)))) && (! (i == -1) || (i == -1 && ! (j == 5)))) && (! (i == 2) || (i == 2 && ! (j == 5)))) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 3) || (i == 3 && ! (j == 7)))) && (! (i == -1) || (i == -1 && ! (j == 4)))) && (! (i == 4) || (i == 4 && ! (j == 8)))) && (! (i == 0) || (i == 0 && ! (j == 4)))) && (! (i == 0) || (i == 0 && ! (j == 5)))) && (! (i == 1) || (i == 1 && ! (j == 5)))) && (! (i == 1) || (i == 1 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == 2) || (i == 2 && ! (j == 4)))) && (! (i == 0) || (i == 0 && ! (j == 2)))) && (! (i == 1) || (i == 1 && ! (j == 7)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && (! (i == 0) || (i == 0 && ! (j == 3)))) && (! (i == 0) || (i == 0 && ! (j == 7)))) && (! (i == 3) || (i == 3 && ! (j == 8)))) && i == 7) && j == 9)) || (((((((((((((! (j == 1) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (j == 6)) && (! (i == 4) || (i == 4 && ! (j == 8)))) && ! (j == 5)) && ! (j == 4)) && ! (i == -1)) && ! (j == 7)) && ! (i == 0)) && (! (i == 3) || (i == 3 && ! (j == 8)))) && (! (i == 7) || (i == 7 && ! (j == 9)))) && i == 1) && j == 3) (../plain/insertion_sort-2.c:28:7-28:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/insertion_sort-2.c:28:7-28:22)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((i == 3 && j == 6) || (((! (i == 3) || (i == 3 && ! (j == 6))) && i == 5) && j == 7)) || (((! (i == 3) && (! (i == 5) || (i == 5 && ! (j == 7)))) && i == -1) && j == 6)) || (((((! (i == 3) || (i == 3 && ! (j == 6))) && (! (i == 5) || (i == 5 && ! (j == 7)))) && (! (i == -1) || (i == -1 && ! (j == 6)))) && i == 6) && j == 8)) || (((((! (i == 3) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (i == -1)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && i == 4) && j == 6)) || ((((((! (i == 3) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (i == -1)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (i == 4)) && i == 0) && j == 6)) || ((((((((! (i == 3) || (i == 3 && ! (j == 6))) && ! (i == 5)) && (! (i == -1) || (i == -1 && ! (j == 6)))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 4) || (i == 4 && ! (j == 6)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && i == 2) && j == 7)) || ((((((((! (i == 3) || (i == 3 && ! (j == 6))) && ! (j == 7)) && (! (i == -1) || (i == -1 && ! (j == 6)))) && ! (i == 6)) && (! (i == 4) || (i == 4 && ! (j == 6)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && i == 5) && j == 8)) || ((((((! (j == 6) && (! (i == 5) || (i == 5 && ! (j == 7)))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && i == 3) && j == 5)) || ((((((((! (i == 3) && ! (i == -1)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (i == 4)) && ! (i == 0)) && ! (j == 7)) && (! (i == 5) || (i == 5 && ! (j == 8)))) && i == 2) && j == 6)) || (((((((((! (i == 3) && (! (i == 5) || (i == 5 && ! (j == 7)))) && ! (i == -1)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (i == 4)) && ! (i == 0)) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (i == 2)) && i == 1) && j == 6)) || ((((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 6)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (i == 3)) && i == -1) && j == 5)) || ((((((((! (i == 6) || (i == 6 && ! (j == 8))) && ! (j == 7)) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (i == 3)) && ! (j == 6)) && ! (i == -1)) && i == 2) && j == 5)) || (((((((! (i == 5) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (j == 6)) && ! (i == 2)) && (! (i == 3) || (i == 3 && ! (j == 5)))) && (! (i == -1) || (i == -1 && ! (j == 5)))) && i == 4) && j == 7)) || (((((((! (j == 6) && ! (i == 5)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (i == 2)) && ! (j == 5)) && ! (i == 4)) && i == 3) && j == 7)) || ((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 6)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (j == 5)) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 3) || (i == 3 && ! (j == 7)))) && i == -1) && j == 4)) || (((((((((! (i == 6) && ! (j == 6)) && ! (i == 5)) && (! (i == 3) || (i == 3 && ! (j == 5)))) && (! (i == -1) || (i == -1 && ! (j == 5)))) && (! (i == 2) || (i == 2 && ! (j == 5)))) && ! (j == 7)) && (! (i == -1) || (i == -1 && ! (j == 4)))) && i == 4) && j == 8)) || (((((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (j == 6)) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && (! (i == 3) || (i == 3 && ! (j == 5)))) && (! (i == 2) || (i == 2 && ! (j == 5)))) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 3) || (i == 3 && ! (j == 7)))) && ! (i == -1)) && (! (i == 4) || (i == 4 && ! (j == 8)))) && i == 0) && j == 4)) || ((((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (j == 6)) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (i == 3)) && ! (i == -1)) && ! (i == 2)) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 4) || (i == 4 && ! (j == 8)))) && ! (j == 4)) && i == 0) && j == 5)) || ((((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (i == 3)) && ! (j == 6)) && ! (i == -1)) && ! (i == 2)) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 4) || (i == 4 && ! (j == 8)))) && ! (i == 0)) && i == 1) && j == 5)) || (((((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (j == 6)) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 3) || (i == 3 && ! (j == 7)))) && ! (i == -1)) && (! (i == 4) || (i == 4 && ! (j == 8)))) && ! (i == 0)) && ! (j == 5)) && i == 1) && j == 4)) || ((((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 6)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (j == 5)) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 3) || (i == 3 && ! (j == 7)))) && ! (j == 4)) && (! (i == 4) || (i == 4 && ! (j == 8)))) && i == -1) && j == 3)) || (((((((((((! (i == 6) || (i == 6 && ! (j == 8))) && ! (j == 7)) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (j == 6)) && ! (j == 5)) && ! (i == -1)) && (! (i == 4) || (i == 4 && ! (j == 8)))) && ! (i == 0)) && ! (i == 1)) && i == 2) && j == 4)) || (((((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (j == 6)) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 3) || (i == 3 && ! (j == 7)))) && (! (i == 4) || (i == 4 && ! (j == 8)))) && ! (j == 4)) && ! (j == 5)) && (! (i == -1) || (i == -1 && ! (j == 3)))) && i == 0) && j == 2)) || (((((((((((! (i == 5) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (i == 2)) && ! (j == 6)) && ! (i == 4)) && ! (i == 3)) && ! (j == 5)) && ! (j == 4)) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == 0) || (i == 0 && ! (j == 2)))) && i == 1) && j == 7)) || (((((((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && ! (j == 6)) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (j == 5)) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 3) || (i == 3 && ! (j == 7)))) && ! (j == 4)) && (! (i == 4) || (i == 4 && ! (j == 8)))) && ! (j == 3)) && ! (i == 0)) && (! (i == 1) || (i == 1 && ! (j == 7)))) && i == -1) && j == 2)) || (((((((((((((((! (i == 5) || (i == 5 && ! (j == 7))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (j == 6)) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 3) || (i == 3 && ! (j == 7)))) && (! (i == 4) || (i == 4 && ! (j == 8)))) && ! (j == 4)) && ! (j == 5)) && ! (i == -1)) && ! (j == 2)) && (! (i == 1) || (i == 1 && ! (j == 7)))) && i == 0) && j == 3)) || ((((((((((((((((((((((((((((! (i == 3) || (i == 3 && ! (j == 6))) && (! (i == 5) || (i == 5 && ! (j == 7)))) && (! (i == -1) || (i == -1 && ! (j == 6)))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 4) || (i == 4 && ! (j == 6)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && (! (i == 3) || (i == 3 && ! (j == 5)))) && (! (i == 2) || (i == 2 && ! (j == 6)))) && (! (i == 1) || (i == 1 && ! (j == 6)))) && (! (i == -1) || (i == -1 && ! (j == 5)))) && (! (i == 2) || (i == 2 && ! (j == 5)))) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 3) || (i == 3 && ! (j == 7)))) && (! (i == -1) || (i == -1 && ! (j == 4)))) && (! (i == 4) || (i == 4 && ! (j == 8)))) && (! (i == 0) || (i == 0 && ! (j == 4)))) && (! (i == 0) || (i == 0 && ! (j == 5)))) && (! (i == 1) || (i == 1 && ! (j == 5)))) && (! (i == 1) || (i == 1 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == 2) || (i == 2 && ! (j == 4)))) && (! (i == 0) || (i == 0 && ! (j == 2)))) && (! (i == 1) || (i == 1 && ! (j == 7)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && (! (i == 0) || (i == 0 && ! (j == 3)))) && j == 1)) || (((((((((((((! (i == 5) && (! (i == 6) || (i == 6 && ! (j == 8)))) && ! (j == 6)) && ! (i == 2)) && ! (i == 4)) && ! (i == 3)) && ! (j == 4)) && ! (j == 5)) && ! (j == 2)) && ! (i == 1)) && ! (j == 3)) && ! (j == 1)) && i == 0) && j == 7)) || ((((((((((((((((! (j == 1) && ! (j == 6)) && ! (i == 6)) && ! (i == 5)) && ! (j == 5)) && ! (j == 7)) && (! (i == -1) || (i == -1 && ! (j == 4)))) && ! (i == 4)) && (! (i == 0) || (i == 0 && ! (j == 4)))) && (! (i == 1) || (i == 1 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == 2) || (i == 2 && ! (j == 4)))) && (! (i == 0) || (i == 0 && ! (j == 2)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && (! (i == 0) || (i == 0 && ! (j == 3)))) && i == 3) && j == 8)) || (((((((((((((((((((((((((((((((! (j == 1) && (! (i == 3) || (i == 3 && ! (j == 6)))) && (! (i == 5) || (i == 5 && ! (j == 7)))) && (! (i == -1) || (i == -1 && ! (j == 6)))) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 4) || (i == 4 && ! (j == 6)))) && (! (i == 0) || (i == 0 && ! (j == 6)))) && (! (i == 2) || (i == 2 && ! (j == 7)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && (! (i == 3) || (i == 3 && ! (j == 5)))) && (! (i == 2) || (i == 2 && ! (j == 6)))) && (! (i == 1) || (i == 1 && ! (j == 6)))) && (! (i == -1) || (i == -1 && ! (j == 5)))) && (! (i == 2) || (i == 2 && ! (j == 5)))) && (! (i == 4) || (i == 4 && ! (j == 7)))) && (! (i == 3) || (i == 3 && ! (j == 7)))) && (! (i == -1) || (i == -1 && ! (j == 4)))) && (! (i == 4) || (i == 4 && ! (j == 8)))) && (! (i == 0) || (i == 0 && ! (j == 4)))) && (! (i == 0) || (i == 0 && ! (j == 5)))) && (! (i == 1) || (i == 1 && ! (j == 5)))) && (! (i == 1) || (i == 1 && ! (j == 4)))) && (! (i == -1) || (i == -1 && ! (j == 3)))) && (! (i == 2) || (i == 2 && ! (j == 4)))) && (! (i == 0) || (i == 0 && ! (j == 2)))) && (! (i == 1) || (i == 1 && ! (j == 7)))) && (! (i == -1) || (i == -1 && ! (j == 2)))) && (! (i == 0) || (i == 0 && ! (j == 3)))) && (! (i == 0) || (i == 0 && ! (j == 7)))) && (! (i == 3) || (i == 3 && ! (j == 8)))) && i == 7) && j == 9)) || (((((((((((((! (j == 1) && (! (i == 6) || (i == 6 && ! (j == 8)))) && (! (i == 5) || (i == 5 && ! (j == 8)))) && ! (j == 6)) && (! (i == 4) || (i == 4 && ! (j == 8)))) && ! (j == 5)) && ! (j == 4)) && ! (i == -1)) && ! (j == 7)) && ! (i == 0)) && (! (i == 3) || (i == 3 && ! (j == 8)))) && (! (i == 7) || (i == 7 && ! (j == 9)))) && i == 1) && j == 3) (../plain/insertion_sort-2.c:28:7-28:22)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 22
  dead: 0
  total lines: 22
[Warning][Witness] invariant unconfirmed: (i == (3) && j == (6)) || ((!(i == (3)) || (i == (3) && !(j == (6)))) && i == (5) && j == (7)) || (!(i == (3)) && (!(i == (5)) || (i == (5) && !(j == (7)))) && i == (-1) && j == (6)) || ((!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (-1)) || (i == (-1) && !(j == (6)))) && i == (6) && j == (8)) || (!(i == (3)) && (!(i == (5)) || (i == (5) && !(j == (7)))) && !(i == (-1)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && i == (4) && j == (6)) || (!(i == (3)) && (!(i == (5)) || (i == (5) && !(j == (7)))) && !(i == (-1)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(i == (4)) && i == (0) && j == (6)) || ((!(i == (3)) || (i == (3) && !(j == (6)))) && !(i == (5)) && (!(i == (-1)) || (i == (-1) && !(j == (6)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (0)) || (i == (0) && !(j == (6)))) && i == (2) && j == (7)) || ((!(i == (3)) || (i == (3) && !(j == (6)))) && !(j == (7)) && (!(i == (-1)) || (i == (-1) && !(j == (6)))) && !(i == (6)) && (!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (0)) || (i == (0) && !(j == (6)))) && i == (5) && j == (8)) || (!(j == (6)) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (2)) || (i == (2) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && i == (3) && j == (5)) || (!(i == (3)) && !(i == (-1)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(i == (4)) && !(i == (0)) && !(j == (7)) && (!(i == (5)) || (i == (5) && !(j == (8)))) && i == (2) && j == (6)) || (!(i == (3)) && (!(i == (5)) || (i == (5) && !(j == (7)))) && !(i == (-1)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(i == (4)) && !(i == (0)) && (!(i == (5)) || (i == (5) && !(j == (8)))) && !(i == (2)) && i == (1) && j == (6)) || ((!(i == (5)) || (i == (5) && !(j == (7)))) && !(j == (6)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (2)) || (i == (2) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && !(i == (3)) && i == (-1) && j == (5)) || ((!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (7)) && (!(i == (5)) || (i == (5) && !(j == (8)))) && !(i == (3)) && !(j == (6)) && !(i == (-1)) && i == (2) && j == (5)) || (!(i == (5)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (6)) && !(i == (2)) && (!(i == (3)) || (i == (3) && !(j == (5)))) && (!(i == (-1)) || (i == (-1) && !(j == (5)))) && i == (4) && j == (7)) || (!(j == (6)) && !(i == (5)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(i == (2)) && !(j == (5)) && !(i == (4)) && i == (3) && j == (7)) || ((!(i == (5)) || (i == (5) && !(j == (7)))) && !(j == (6)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (2)) || (i == (2) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && !(j == (5)) && (!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && i == (-1) && j == (4)) || (!(i == (6)) && !(j == (6)) && !(i == (5)) && (!(i == (3)) || (i == (3) && !(j == (5)))) && (!(i == (-1)) || (i == (-1) && !(j == (5)))) && (!(i == (2)) || (i == (2) && !(j == (5)))) && !(j == (7)) && (!(i == (-1)) || (i == (-1) && !(j == (4)))) && i == (4) && j == (8)) || ((!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (6)) && (!(i == (2)) || (i == (2) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && (!(i == (3)) || (i == (3) && !(j == (5)))) && (!(i == (2)) || (i == (2) && !(j == (5)))) && (!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && !(i == (-1)) && (!(i == (4)) || (i == (4) && !(j == (8)))) && i == (0) && j == (4)) || ((!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (6)) && (!(i == (5)) || (i == (5) && !(j == (8)))) && !(i == (3)) && !(i == (-1)) && !(i == (2)) && (!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (4)) || (i == (4) && !(j == (8)))) && !(j == (4)) && i == (0) && j == (5)) || ((!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && !(i == (3)) && !(j == (6)) && !(i == (-1)) && !(i == (2)) && (!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (4)) || (i == (4) && !(j == (8)))) && !(i == (0)) && i == (1) && j == (5)) || ((!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (2)) || (i == (2) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && !(j == (6)) && (!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && !(i == (-1)) && (!(i == (4)) || (i == (4) && !(j == (8)))) && !(i == (0)) && !(j == (5)) && i == (1) && j == (4)) || ((!(i == (5)) || (i == (5) && !(j == (7)))) && !(j == (6)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (2)) || (i == (2) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && !(j == (5)) && (!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && !(j == (4)) && (!(i == (4)) || (i == (4) && !(j == (8)))) && i == (-1) && j == (3)) || ((!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (7)) && (!(i == (5)) || (i == (5) && !(j == (8)))) && !(j == (6)) && !(j == (5)) && !(i == (-1)) && (!(i == (4)) || (i == (4) && !(j == (8)))) && !(i == (0)) && !(i == (1)) && i == (2) && j == (4)) || ((!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (6)) && (!(i == (2)) || (i == (2) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && (!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (4)) || (i == (4) && !(j == (8)))) && !(j == (4)) && !(j == (5)) && (!(i == (-1)) || (i == (-1) && !(j == (3)))) && i == (0) && j == (2)) || (!(i == (5)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(i == (2)) && !(j == (6)) && !(i == (4)) && !(i == (3)) && !(j == (5)) && !(j == (4)) && (!(i == (-1)) || (i == (-1) && !(j == (3)))) && (!(i == (0)) || (i == (0) && !(j == (2)))) && i == (1) && j == (7)) || ((!(i == (5)) || (i == (5) && !(j == (7)))) && !(j == (6)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (2)) || (i == (2) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && !(j == (5)) && (!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && !(j == (4)) && (!(i == (4)) || (i == (4) && !(j == (8)))) && !(j == (3)) && !(i == (0)) && (!(i == (1)) || (i == (1) && !(j == (7)))) && i == (-1) && j == (2)) || ((!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (6)) && (!(i == (2)) || (i == (2) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && (!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (4)) || (i == (4) && !(j == (8)))) && !(j == (4)) && !(j == (5)) && !(i == (-1)) && !(j == (2)) && (!(i == (1)) || (i == (1) && !(j == (7)))) && i == (0) && j == (3)) || ((!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (-1)) || (i == (-1) && !(j == (6)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (0)) || (i == (0) && !(j == (6)))) && (!(i == (2)) || (i == (2) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && (!(i == (3)) || (i == (3) && !(j == (5)))) && (!(i == (2)) || (i == (2) && !(j == (6)))) && (!(i == (1)) || (i == (1) && !(j == (6)))) && (!(i == (-1)) || (i == (-1) && !(j == (5)))) && (!(i == (2)) || (i == (2) && !(j == (5)))) && (!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (-1)) || (i == (-1) && !(j == (4)))) && (!(i == (4)) || (i == (4) && !(j == (8)))) && (!(i == (0)) || (i == (0) && !(j == (4)))) && (!(i == (0)) || (i == (0) && !(j == (5)))) && (!(i == (1)) || (i == (1) && !(j == (5)))) && (!(i == (1)) || (i == (1) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (3)))) && (!(i == (2)) || (i == (2) && !(j == (4)))) && (!(i == (0)) || (i == (0) && !(j == (2)))) && (!(i == (1)) || (i == (1) && !(j == (7)))) && (!(i == (-1)) || (i == (-1) && !(j == (2)))) && (!(i == (0)) || (i == (0) && !(j == (3)))) && j == (1)) || (!(i == (5)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (6)) && !(i == (2)) && !(i == (4)) && !(i == (3)) && !(j == (4)) && !(j == (5)) && !(j == (2)) && !(i == (1)) && !(j == (3)) && !(j == (1)) && i == (0) && j == (7)) || (!(j == (1)) && !(j == (6)) && !(i == (6)) && !(i == (5)) && !(j == (5)) && !(j == (7)) && (!(i == (-1)) || (i == (-1) && !(j == (4)))) && !(i == (4)) && (!(i == (0)) || (i == (0) && !(j == (4)))) && (!(i == (1)) || (i == (1) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (3)))) && (!(i == (2)) || (i == (2) && !(j == (4)))) && (!(i == (0)) || (i == (0) && !(j == (2)))) && (!(i == (-1)) || (i == (-1) && !(j == (2)))) && (!(i == (0)) || (i == (0) && !(j == (3)))) && i == (3) && j == (8)) || (!(j == (1)) && (!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (-1)) || (i == (-1) && !(j == (6)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (0)) || (i == (0) && !(j == (6)))) && (!(i == (2)) || (i == (2) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && (!(i == (3)) || (i == (3) && !(j == (5)))) && (!(i == (2)) || (i == (2) && !(j == (6)))) && (!(i == (1)) || (i == (1) && !(j == (6)))) && (!(i == (-1)) || (i == (-1) && !(j == (5)))) && (!(i == (2)) || (i == (2) && !(j == (5)))) && (!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (-1)) || (i == (-1) && !(j == (4)))) && (!(i == (4)) || (i == (4) && !(j == (8)))) && (!(i == (0)) || (i == (0) && !(j == (4)))) && (!(i == (0)) || (i == (0) && !(j == (5)))) && (!(i == (1)) || (i == (1) && !(j == (5)))) && (!(i == (1)) || (i == (1) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (3)))) && (!(i == (2)) || (i == (2) && !(j == (4)))) && (!(i == (0)) || (i == (0) && !(j == (2)))) && (!(i == (1)) || (i == (1) && !(j == (7)))) && (!(i == (-1)) || (i == (-1) && !(j == (2)))) && (!(i == (0)) || (i == (0) && !(j == (3)))) && (!(i == (0)) || (i == (0) && !(j == (7)))) && (!(i == (3)) || (i == (3) && !(j == (8)))) && i == (7) && j == (9)) || (!(j == (1)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && !(j == (6)) && (!(i == (4)) || (i == (4) && !(j == (8)))) && !(j == (5)) && !(j == (4)) && !(i == (-1)) && !(j == (7)) && !(i == (0)) && (!(i == (3)) || (i == (3) && !(j == (8)))) && (!(i == (7)) || (i == (7) && !(j == (9)))) && i == (1) && j == (3)) (../plain/insertion_sort-2.c:28:3)
[Warning][Witness] invariant unconfirmed: j == (22) || (!(j == (22)) && j == (11)) || (!(j == (22)) && !(j == (11)) && j == (25)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && j == (27)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && j == (16)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && j == (8)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && j == (10)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && j == (3)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && j == (1)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && j == (2)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && j == (5)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && j == (12)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && j == (26)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && j == (9)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && j == (17)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && j == (0)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && j == (14)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && j == (18)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && j == (19)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && j == (6)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && !(j == (6)) && j == (23)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && !(j == (6)) && !(j == (23)) && j == (15)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && !(j == (6)) && !(j == (23)) && !(j == (15)) && j == (24)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && !(j == (6)) && !(j == (23)) && !(j == (15)) && !(j == (24)) && j == (28)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && !(j == (6)) && !(j == (23)) && !(j == (15)) && !(j == (24)) && !(j == (28)) && j == (7)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && !(j == (6)) && !(j == (23)) && !(j == (15)) && !(j == (24)) && !(j == (28)) && !(j == (7)) && j == (13)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && !(j == (6)) && !(j == (23)) && !(j == (15)) && !(j == (24)) && !(j == (28)) && !(j == (7)) && !(j == (13)) && j == (4)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && !(j == (6)) && !(j == (23)) && !(j == (15)) && !(j == (24)) && !(j == (28)) && !(j == (7)) && !(j == (13)) && !(j == (4)) && j == (20)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && !(j == (6)) && !(j == (23)) && !(j == (15)) && !(j == (24)) && !(j == (28)) && !(j == (7)) && !(j == (13)) && !(j == (4)) && !(j == (20)) && j == (29)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && !(j == (6)) && !(j == (23)) && !(j == (15)) && !(j == (24)) && !(j == (28)) && !(j == (7)) && !(j == (13)) && !(j == (4)) && !(j == (20)) && !(j == (29)) && j == (21)) (../plain/insertion_sort-2.c:19:4)
[Warning][Witness] invariant unconfirmed: j == (22) || (!(j == (22)) && j == (11)) || (!(j == (22)) && !(j == (11)) && j == (25)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && j == (27)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && j == (16)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && j == (8)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && j == (10)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && j == (3)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && j == (1)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && j == (2)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && j == (5)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && j == (12)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && j == (26)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && j == (9)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && j == (17)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && j == (0)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && j == (14)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && j == (18)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && j == (19)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && j == (6)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && !(j == (6)) && j == (23)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && !(j == (6)) && !(j == (23)) && j == (15)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && !(j == (6)) && !(j == (23)) && !(j == (15)) && j == (24)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && !(j == (6)) && !(j == (23)) && !(j == (15)) && !(j == (24)) && j == (28)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && !(j == (6)) && !(j == (23)) && !(j == (15)) && !(j == (24)) && !(j == (28)) && j == (7)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && !(j == (6)) && !(j == (23)) && !(j == (15)) && !(j == (24)) && !(j == (28)) && !(j == (7)) && j == (13)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && !(j == (6)) && !(j == (23)) && !(j == (15)) && !(j == (24)) && !(j == (28)) && !(j == (7)) && !(j == (13)) && j == (4)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && !(j == (6)) && !(j == (23)) && !(j == (15)) && !(j == (24)) && !(j == (28)) && !(j == (7)) && !(j == (13)) && !(j == (4)) && j == (20)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && !(j == (6)) && !(j == (23)) && !(j == (15)) && !(j == (24)) && !(j == (28)) && !(j == (7)) && !(j == (13)) && !(j == (4)) && !(j == (20)) && j == (29)) || (!(j == (22)) && !(j == (11)) && !(j == (25)) && !(j == (27)) && !(j == (16)) && !(j == (8)) && !(j == (10)) && !(j == (3)) && !(j == (1)) && !(j == (2)) && !(j == (5)) && !(j == (12)) && !(j == (26)) && !(j == (9)) && !(j == (17)) && !(j == (0)) && !(j == (14)) && !(j == (18)) && !(j == (19)) && !(j == (6)) && !(j == (23)) && !(j == (15)) && !(j == (24)) && !(j == (28)) && !(j == (7)) && !(j == (13)) && !(j == (4)) && !(j == (20)) && !(j == (29)) && j == (21)) (../plain/insertion_sort-2.c:18:7)

runtime: 00:00:10.108
vars: 61, evals: 144

|rho|=53
|called|=0
|stable|=53
|infl|=48
|wpoint|=2
|side_dep|=16
|side_infl|=25
|var_messages|=9
|rho_write|=16
|dep|=35
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2005) on ../plain/insertion_sort-2.c:13:1-31:1
1	contexts for entry state of __VERIFIER_assert (2000) on ../plain/insertion_sort-2.c:5:1-10:1
1	contexts for entry state of reach_error (1999) on ../plain/insertion_sort-2.c:3:1-3:82
1	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140

Memory statistics: total=1673.80MB, max=21.63MB, minor=1669.74MB, major=106.21MB, promoted=102.15MB
    minor collections=805  major collections=20 compactions=0

[Warning][Witness] invariant unconfirmed: (i == (4) && j == (6)) || ((!(i == (4)) || (i == (4) && !(j == (6)))) && i == (3) && j == (5)) || (!(i == (4)) && !(j == (5)) && i == (3) && j == (6)) || ((!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (3)) || (i == (3) && !(j == (5)))) && (!(i == (3)) || (i == (3) && !(j == (6)))) && i == (5) && j == (7)) || ((!(i == (4)) || (i == (4) && !(j == (6)))) && !(i == (3)) && (!(i == (5)) || (i == (5) && !(j == (7)))) && i == (2) && j == (5)) || ((!(i == (4)) || (i == (4) && !(j == (6)))) && !(i == (3)) && (!(i == (5)) || (i == (5) && !(j == (7)))) && !(i == (2)) && i == (0) && j == (5)) || ((!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (3)) || (i == (3) && !(j == (5)))) && (!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (2)) || (i == (2) && !(j == (5)))) && (!(i == (0)) || (i == (0) && !(j == (5)))) && i == (1) && j == (4)) || ((!(i == (4)) || (i == (4) && !(j == (6)))) && !(i == (3)) && (!(i == (5)) || (i == (5) && !(j == (7)))) && !(i == (2)) && !(i == (0)) && (!(i == (1)) || (i == (1) && !(j == (4)))) && i == (-1) && j == (5)) || (!(i == (4)) && !(i == (3)) && (!(i == (5)) || (i == (5) && !(j == (7)))) && !(j == (5)) && (!(i == (1)) || (i == (1) && !(j == (4)))) && i == (2) && j == (6)) || (!(i == (4)) && !(i == (3)) && (!(i == (5)) || (i == (5) && !(j == (7)))) && !(j == (5)) && (!(i == (1)) || (i == (1) && !(j == (4)))) && !(i == (2)) && i == (0) && j == (6)) || ((!(i == (5)) || (i == (5) && !(j == (7)))) && !(j == (5)) && !(i == (1)) && !(j == (6)) && i == (2) && j == (4)) || ((!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (1)) || (i == (1) && !(j == (4)))) && !(j == (5)) && (!(i == (2)) || (i == (2) && !(j == (6)))) && (!(i == (0)) || (i == (0) && !(j == (6)))) && (!(i == (2)) || (i == (2) && !(j == (4)))) && i == (-1) && j == (3)) || ((!(i == (5)) || (i == (5) && !(j == (7)))) && !(j == (5)) && !(i == (1)) && !(j == (6)) && !(i == (2)) && (!(i == (-1)) || (i == (-1) && !(j == (3)))) && i == (0) && j == (4)) || ((!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (1)) || (i == (1) && !(j == (4)))) && !(j == (5)) && (!(i == (2)) || (i == (2) && !(j == (6)))) && (!(i == (0)) || (i == (0) && !(j == (6)))) && (!(i == (2)) || (i == (2) && !(j == (4)))) && !(j == (3)) && (!(i == (0)) || (i == (0) && !(j == (4)))) && i == (-1) && j == (2)) || ((!(i == (4)) || (i == (4) && !(j == (6)))) && !(i == (3)) && (!(i == (5)) || (i == (5) && !(j == (7)))) && !(i == (2)) && !(i == (0)) && !(j == (4)) && !(i == (-1)) && i == (1) && j == (5)) || ((!(i == (5)) || (i == (5) && !(j == (7)))) && !(j == (5)) && !(j == (6)) && !(i == (-1)) && !(j == (4)) && i == (0) && j == (3)) || ((!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && !(i == (1)) && !(j == (5)) && !(i == (2)) && !(j == (3)) && !(i == (0)) && !(j == (2)) && i == (-1) && j == (4)) || ((!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (3)) || (i == (3) && !(j == (5)))) && (!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && (!(i == (2)) || (i == (2) && !(j == (5)))) && (!(i == (0)) || (i == (0) && !(j == (5)))) && (!(i == (1)) || (i == (1) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (5)))) && (!(i == (2)) || (i == (2) && !(j == (6)))) && (!(i == (0)) || (i == (0) && !(j == (6)))) && (!(i == (2)) || (i == (2) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (3)))) && (!(i == (0)) || (i == (0) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (2)))) && (!(i == (1)) || (i == (1) && !(j == (5)))) && (!(i == (0)) || (i == (0) && !(j == (3)))) && (!(i == (-1)) || (i == (-1) && !(j == (4)))) && i == (6) && j == (8)) || (!(i == (4)) && !(i == (3)) && (!(i == (5)) || (i == (5) && !(j == (7)))) && !(j == (4)) && !(i == (2)) && !(i == (0)) && (!(i == (-1)) || (i == (-1) && !(j == (3)))) && (!(i == (-1)) || (i == (-1) && !(j == (2)))) && !(j == (5)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && i == (1) && j == (6)) || ((!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (5)) || (i == (5) && !(j == (7)))) && !(j == (5)) && (!(i == (2)) || (i == (2) && !(j == (6)))) && (!(i == (0)) || (i == (0) && !(j == (6)))) && !(j == (3)) && !(j == (2)) && !(j == (4)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (1)) || (i == (1) && !(j == (6)))) && i == (-1) && j == (1)) || ((!(i == (5)) || (i == (5) && !(j == (7)))) && !(j == (5)) && !(j == (6)) && !(j == (4)) && !(i == (-1)) && !(j == (3)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && i == (0) && j == (2)) || (!(j == (5)) && !(j == (6)) && !(i == (5)) && (!(i == (1)) || (i == (1) && !(j == (4)))) && (!(i == (2)) || (i == (2) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (3)))) && (!(i == (0)) || (i == (0) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (2)))) && (!(i == (0)) || (i == (0) && !(j == (3)))) && (!(i == (-1)) || (i == (-1) && !(j == (4)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (-1)) || (i == (-1) && !(j == (1)))) && (!(i == (0)) || (i == (0) && !(j == (2)))) && i == (3) && j == (7)) || (!(j == (6)) && !(i == (5)) && (!(i == (2)) || (i == (2) && !(j == (5)))) && (!(i == (0)) || (i == (0) && !(j == (5)))) && (!(i == (1)) || (i == (1) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (5)))) && (!(i == (2)) || (i == (2) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (3)))) && (!(i == (0)) || (i == (0) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (2)))) && (!(i == (1)) || (i == (1) && !(j == (5)))) && (!(i == (0)) || (i == (0) && !(j == (3)))) && (!(i == (-1)) || (i == (-1) && !(j == (4)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (-1)) || (i == (-1) && !(j == (1)))) && (!(i == (0)) || (i == (0) && !(j == (2)))) && !(i == (3)) && i == (4) && j == (7)) || ((!(i == (5)) || (i == (5) && !(j == (7)))) && !(j == (4)) && !(i == (-1)) && !(j == (5)) && !(i == (0)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (6)) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (4)) || (i == (4) && !(j == (7)))) && i == (1) && j == (3)) || (!(i == (4)) && !(i == (3)) && (!(i == (5)) || (i == (5) && !(j == (7)))) && !(j == (5)) && !(i == (2)) && !(i == (0)) && !(j == (3)) && !(j == (2)) && !(j == (4)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(i == (1)) && !(j == (1)) && i == (-1) && j == (6)) || (!(i == (5)) && !(j == (5)) && !(j == (6)) && !(j == (4)) && (!(i == (-1)) || (i == (-1) && !(j == (3)))) && (!(i == (-1)) || (i == (-1) && !(j == (2)))) && (!(i == (0)) || (i == (0) && !(j == (3)))) && (!(i == (6)) || (i == (6) && !(j == (8)))) && (!(i == (-1)) || (i == (-1) && !(j == (1)))) && (!(i == (0)) || (i == (0) && !(j == (2)))) && !(i == (3)) && !(i == (4)) && (!(i == (1)) || (i == (1) && !(j == (3)))) && i == (2) && j == (7)) || ((!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (3)) || (i == (3) && !(j == (5)))) && (!(i == (3)) || (i == (3) && !(j == (6)))) && !(j == (7)) && (!(i == (2)) || (i == (2) && !(j == (5)))) && (!(i == (0)) || (i == (0) && !(j == (5)))) && (!(i == (1)) || (i == (1) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (5)))) && (!(i == (2)) || (i == (2) && !(j == (6)))) && (!(i == (0)) || (i == (0) && !(j == (6)))) && (!(i == (2)) || (i == (2) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (3)))) && (!(i == (0)) || (i == (0) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (2)))) && (!(i == (1)) || (i == (1) && !(j == (5)))) && (!(i == (0)) || (i == (0) && !(j == (3)))) && (!(i == (-1)) || (i == (-1) && !(j == (4)))) && !(i == (6)) && (!(i == (1)) || (i == (1) && !(j == (6)))) && (!(i == (-1)) || (i == (-1) && !(j == (1)))) && (!(i == (0)) || (i == (0) && !(j == (2)))) && (!(i == (1)) || (i == (1) && !(j == (3)))) && (!(i == (-1)) || (i == (-1) && !(j == (6)))) && i == (5) && j == (8)) || (!(j == (6)) && !(i == (3)) && !(i == (2)) && !(i == (0)) && !(i == (-1)) && !(i == (1)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (7)) && (!(i == (5)) || (i == (5) && !(j == (8)))) && i == (4) && j == (5)) || (!(i == (4)) && !(i == (3)) && !(j == (7)) && !(i == (2)) && !(i == (0)) && !(i == (1)) && !(i == (-1)) && !(j == (8)) && i == (5) && j == (6)) || (!(i == (5)) && (!(i == (0)) || (i == (0) && !(j == (5)))) && (!(i == (1)) || (i == (1) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (5)))) && (!(i == (0)) || (i == (0) && !(j == (6)))) && (!(i == (-1)) || (i == (-1) && !(j == (3)))) && (!(i == (0)) || (i == (0) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (2)))) && (!(i == (1)) || (i == (1) && !(j == (5)))) && (!(i == (0)) || (i == (0) && !(j == (3)))) && (!(i == (-1)) || (i == (-1) && !(j == (4)))) && !(j == (8)) && (!(i == (1)) || (i == (1) && !(j == (6)))) && (!(i == (-1)) || (i == (-1) && !(j == (1)))) && (!(i == (0)) || (i == (0) && !(j == (2)))) && !(i == (3)) && !(i == (4)) && (!(i == (1)) || (i == (1) && !(j == (3)))) && (!(i == (-1)) || (i == (-1) && !(j == (6)))) && !(i == (2)) && i == (6) && j == (7)) || (!(j == (5)) && !(j == (6)) && !(i == (1)) && !(i == (2)) && !(i == (0)) && !(i == (-1)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (7)) && (!(i == (5)) || (i == (5) && !(j == (8)))) && i == (3) && j == (4)) || ((!(i == (5)) || (i == (5) && !(j == (7)))) && !(j == (4)) && !(i == (-1)) && !(j == (5)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(j == (6)) && !(i == (0)) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (4)) || (i == (4) && !(j == (7)))) && !(j == (3)) && (!(i == (2)) || (i == (2) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && (!(i == (6)) || (i == (6) && !(j == (7)))) && i == (1) && j == (2)) || (!(j == (5)) && !(j == (6)) && !(j == (4)) && !(i == (-1)) && !(i == (0)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(i == (1)) && !(j == (7)) && (!(i == (5)) || (i == (5) && !(j == (8)))) && i == (2) && j == (3)) || ((!(i == (4)) || (i == (4) && !(j == (6)))) && (!(i == (3)) || (i == (3) && !(j == (5)))) && (!(i == (3)) || (i == (3) && !(j == (6)))) && (!(i == (2)) || (i == (2) && !(j == (5)))) && (!(i == (0)) || (i == (0) && !(j == (5)))) && (!(i == (1)) || (i == (1) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (5)))) && (!(i == (2)) || (i == (2) && !(j == (6)))) && (!(i == (0)) || (i == (0) && !(j == (6)))) && (!(i == (2)) || (i == (2) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (3)))) && (!(i == (0)) || (i == (0) && !(j == (4)))) && (!(i == (-1)) || (i == (-1) && !(j == (2)))) && (!(i == (1)) || (i == (1) && !(j == (5)))) && (!(i == (0)) || (i == (0) && !(j == (3)))) && (!(i == (-1)) || (i == (-1) && !(j == (4)))) && !(i == (6)) && (!(i == (1)) || (i == (1) && !(j == (6)))) && (!(i == (-1)) || (i == (-1) && !(j == (1)))) && (!(i == (0)) || (i == (0) && !(j == (2)))) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (1)) || (i == (1) && !(j == (3)))) && (!(i == (-1)) || (i == (-1) && !(j == (6)))) && (!(i == (2)) || (i == (2) && !(j == (7)))) && !(i == (5)) && (!(i == (4)) || (i == (4) && !(j == (5)))) && (!(i == (3)) || (i == (3) && !(j == (4)))) && (!(i == (1)) || (i == (1) && !(j == (2)))) && (!(i == (2)) || (i == (2) && !(j == (3)))) && i == (7) && j == (8)) || ((!(i == (5)) || (i == (5) && !(j == (7)))) && !(j == (5)) && !(j == (6)) && !(j == (4)) && !(j == (3)) && (!(i == (6)) || (i == (6) && !(j == (8)))) && !(i == (-1)) && !(j == (2)) && (!(i == (3)) || (i == (3) && !(j == (7)))) && (!(i == (4)) || (i == (4) && !(j == (7)))) && (!(i == (2)) || (i == (2) && !(j == (7)))) && (!(i == (5)) || (i == (5) && !(j == (8)))) && (!(i == (6)) || (i == (6) && !(j == (7)))) && (!(i == (7)) || (i == (7) && !(j == (8)))) && i == (0) && j == (1)) (../plain/insertion_sort-2.c:22:7)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 4
  refuted: 0
  error: 2
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 6
SV-COMP result: unknown

vars = 61    evals = 144    narrow_reuses = 8

Timings:
                                  cputime   walltime   allocated   count
Default                           12.600s    12.602s   1748.20MB      1×
  preprocess                         0.023s     0.022s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.11MB      4×
  Cabs2cil                           0.005s     0.005s      4.72MB      4×
  mergeCIL                           0.003s     0.003s      3.34MB      1×
  analysis                          12.561s    12.562s   1731.05MB      1×
    createCFG                          0.001s     0.001s      0.62MB      1×
      handle                             0.001s     0.001s      0.10MB     33×
      iter_connect                       0.001s     0.001s      0.41MB     33×
        computeSCCs                        0.001s     0.001s      0.24MB     34×
    FrontC                             0.042s     0.042s     18.96MB      8×
    Cabs2cil                           0.013s     0.013s     13.61MB      8×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            3.906s     3.906s   1354.20MB      1×
      S.Dom.equal                        0.001s     0.001s      0.06MB    152×
      base unassume                      0.869s     0.870s   1068.16MB     37×
      cheap_full_reach                   0.001s     0.001s      0.02MB      1×
      postsolver                         0.025s     0.025s     22.55MB      1×
        postsolver_iter                    0.025s     0.025s     22.50MB      1×
    warn_global                        0.001s     0.001s      0.12MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
