./goblint --conf conf/svcomp-yaml-validate.json --enable dbg.timing.enabled --set 'ana.activated[+]' apron --set ana.apron.domain polyhedra --witness.yaml.unassume /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/../../../results/st-lit-guide/convert-tmp.2023-01-31_11-34-58.files/cpachecker/bh-ex1-poly.yml/witness.yml --sets ana.specification /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/properties/unreach-call.prp --sets exp.architecture 64bit /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Warning][Witness] couldn't locate invariant: (j == (4) && i == (4)) || (i == (5) && j == (4)) || (j == (4) && i == (3)) || (j == (4) && i == (2)) (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i:26:5)
[Warning][Witness] couldn't locate invariant: j == (4) && i == (4) (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i:32:3)
[Info][Witness] unassume invariant: (((((((j == 4 && i == 1) || (j == 4 && i == 3)) || (j == 4 && i == 4)) || (j == 4 && i == 2)) || i == 0) || ((! (i == 0) && i == 1) && j == 4)) || ((! (i == 0) && i == 4) && j == 4)) || ((! (i == 0) && i == 3) && j == 4) (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i:15:7-15:12)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i:19:7-19:10)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i:22:7-22:36)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i:23:7-23:40)
[Info][Witness] unassume invariant: (((((((((((((((j == 0 && i == 1) || (j == 0 && i == 3)) || (j == 0 && i == 0)) || ((j == 0 && ! (i == 0)) && i == 2)) || ((! (j == 0) && i == 0) && j == 0)) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && j == 2)) || ((! (i == 0) && i == 3) && j == 0)) || (((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2) && j == 4)) || (((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (j == 4))) && i == 2) && j == 2)) || ((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) && i == 5) && j == 4)) || ((! (i == 0) && i == 1) && j == 0)) || (((((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) || (((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || ((((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) || ((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || ((((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) && ! (i == 5))) && ! (i == 1))) || (! (j == 0) && i == 1)) && i == 4) && j == 4)) || ((((((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) || (((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && ! (i == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5) && ! (j == 4))) || ((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5) && ! (j == 4))) && ! (i == 1))) || (! (j == 0) && i == 1)) || (((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) || (((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && ! (i == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5) && ! (j == 4))) || ((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5) && ! (j == 4))) && ! (i == 1))) || (! (j == 0) && i == 1)) && ! (i == 4))) || ((((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && ! (i == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) || (((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && ! (i == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && ! (i == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5)) || ((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5)) && ! (i == 1))) || (! (j == 0) && i == 1)) && i == 4) && ! (j == 4))) && i == 3) && j == 2)) || (((((((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5) && ! (j == 4))) || ((((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || ((((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) || ((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || ((((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5) && ! (j == 4))) && ! (i == 1))) || (! (j == 0) && i == 1)) || ((((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5)) || ((((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) || ((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5)) && ! (i == 1))) || (! (j == 0) && i == 1)) && ! (j == 4))) || (((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 2))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5) && ! (j == 4))) || ((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5) && ! (j == 4))) && ! (i == 1))) || (! (j == 0) && i == 1)) || ((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 2))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 2))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 2))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5)) || ((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5)) && ! (i == 1))) || (! (j == 0) && i == 1)) && ! (j == 4))) && ! (i == 3))) && i == 4) && j == 2)) || ((((((((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) && ! (i == 2))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) && ! (i == 2))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) && ! (i == 5))) && ! (i == 1))) || (! (j == 0) && i == 1)) || (((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) && ! (i == 2))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) && ! (i == 2))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) && ! (i == 5))) && ! (i == 1))) || (! (j == 0) && i == 1)) && ! (i == 4))) || ((((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) && ! (i == 1))) || (! (j == 0) && i == 1)) || (((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) && ! (i == 1))) || (! (j == 0) && i == 1)) && ! (i == 4))) && ! (j == 2))) || ((((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) && ! (i == 2))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) && ! (i == 2))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) && ! (i == 5))) && ! (i == 1))) || (! (j == 0) && i == 1)) || (((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) && ! (i == 1))) || (! (j == 0) && i == 1)) && ! (j == 2))) && ! (i == 4))) || ((((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) && ! (i == 1))) || (! (j == 0) && i == 1)) && i == 4) && ! (j == 2))) && i == 3) && j == 4)) && ((((j == 4 && i == 1) || (j == 4 && i == 2)) || i == 0) || ((! (i == 0) && i == 3) && j == 4)) (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i:24:7-24:32)
[Info][Witness] unassume invariant: (((((((((((((((j == 0 && i == 1) || (j == 0 && i == 3)) || (j == 0 && i == 0)) || ((j == 0 && ! (i == 0)) && i == 2)) || ((! (j == 0) && i == 0) && j == 0)) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && j == 2)) || ((! (i == 0) && i == 3) && j == 0)) || (((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2) && j == 4)) || (((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (j == 4))) && i == 2) && j == 2)) || ((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) && i == 5) && j == 4)) || ((! (i == 0) && i == 1) && j == 0)) || (((((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) || (((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || ((((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) || ((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || ((((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) && ! (i == 5))) && ! (i == 1))) || (! (j == 0) && i == 1)) && i == 4) && j == 4)) || ((((((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) || (((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && ! (i == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5) && ! (j == 4))) || ((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5) && ! (j == 4))) && ! (i == 1))) || (! (j == 0) && i == 1)) || (((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) || (((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && ! (i == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5) && ! (j == 4))) || ((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5) && ! (j == 4))) && ! (i == 1))) || (! (j == 0) && i == 1)) && ! (i == 4))) || ((((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && ! (i == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) || (((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && ! (i == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && ! (i == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5)) || ((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5)) && ! (i == 1))) || (! (j == 0) && i == 1)) && i == 4) && ! (j == 4))) && i == 3) && j == 2)) || (((((((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5) && ! (j == 4))) || ((((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || ((((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) || ((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || ((((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5) && ! (j == 4))) && ! (i == 1))) || (! (j == 0) && i == 1)) || ((((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5)) || ((((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) || ((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && ! (i == 2))) || (((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 3))) || (i == 3 && ! (j == 0))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5)) && ! (i == 1))) || (! (j == 0) && i == 1)) && ! (j == 4))) || (((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 2))) || ((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 2))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5) && ! (j == 4))) || ((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 4))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5) && ! (j == 4))) && ! (i == 1))) || (! (j == 0) && i == 1)) || ((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 2))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 2))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && ! (i == 2))) || (((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5)) || ((((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && i == 5)) && ! (i == 1))) || (! (j == 0) && i == 1)) && ! (j == 4))) && ! (i == 3))) && i == 4) && j == 2)) || ((((((((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) && ! (i == 2))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) && ! (i == 2))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) && ! (i == 5))) && ! (i == 1))) || (! (j == 0) && i == 1)) || (((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) && ! (i == 2))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) && ! (i == 2))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) && ! (i == 5))) && ! (i == 1))) || (! (j == 0) && i == 1)) && ! (i == 4))) || ((((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) && ! (i == 1))) || (! (j == 0) && i == 1)) || (((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) && ! (i == 1))) || (! (j == 0) && i == 1)) && ! (i == 4))) && ! (j == 2))) || ((((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) && ! (i == 2))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1) && ! (j == 2))) || ! (j == 0)) && ! (i == 2))) || ((((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || ((((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2) && ! (j == 2))) || (i == 2 && ! (j == 0))) && ! (i == 5))) && ! (i == 1))) || (! (j == 0) && i == 1)) || (((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) && ! (i == 1))) || (! (j == 0) && i == 1)) && ! (j == 2))) && ! (i == 4))) || ((((((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((((! (i == 0) || (i == 0 && ! (j == 0))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || ((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && ! (i == 2))) || (((((! (i == 0) || (i == 0 && ! (j == 0))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && ! (i == 1))) || (((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0)))) && i == 1)) || ! (j == 0)) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) || (((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) || ((((((i == 0 && ! (j == 0)) || (((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && ! (i == 0)) && ! (i == 2))) && (! (i == 0) || (i == 0 && ! (j == 0))))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && ! (i == 2))) || (((i == 0 && ! (j == 0)) || ((! (j == 0) || (j == 0 && ! (i == 0))) && (! (i == 0) || (i == 0 && ! (j == 0))))) && i == 2)) || (i == 2 && ! (j == 0))) && ! (i == 5))) && ! (i == 1))) || (! (j == 0) && i == 1)) && i == 4) && ! (j == 2))) && i == 3) && j == 4)) && ((((j == 4 && i == 1) || (j == 4 && i == 2)) || i == 0) || ((! (i == 0) && i == 3) && j == 4)) (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i:17:9-17:14)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i:27:5-27:34)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i:28:5-28:38)
[Info][Witness] unassume invariant: (((((((j == 4 && i == 1) || (j == 4 && i == 3)) || (j == 4 && i == 4)) || (j == 4 && i == 2)) || i == 0) || ((! (i == 0) && i == 1) && j == 4)) || ((! (i == 0) && i == 4) && j == 4)) || ((! (i == 0) && i == 3) && j == 4) (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i:30:5-30:22)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 19
  dead: 0
  total lines: 19
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i:12:73-12:74)
SV-COMP result: unknown

vars = 41    evals = 220    narrow_reuses = 8

Timings:
                                  cputime   walltime   allocated   count
Default                            7.126s     7.127s   3057.39MB      1×
  preprocess                         0.027s     0.026s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.14MB      4×
  Cabs2cil                           0.007s     0.007s      4.75MB      4×
  mergeCIL                           0.004s     0.004s      3.34MB      1×
  analysis                           7.081s     7.081s   3040.38MB      1×
    createCFG                          0.001s     0.001s      0.60MB      1×
      handle                             0.001s     0.001s      0.09MB     33×
      iter_connect                       0.001s     0.001s      0.40MB     33×
        computeSCCs                        0.001s     0.001s      0.23MB     34×
    FrontC                             0.026s     0.026s     16.19MB      3×
    Cabs2cil                           0.012s     0.012s     10.78MB      3×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            7.028s     7.028s   2989.42MB      1×
      S.Dom.equal                        0.001s     0.001s      0.08MB    228×
      base unassume                      1.818s     1.818s   2530.82MB     26×
      cheap_full_reach                   0.001s     0.001s      0.02MB      1×
      postsolver                         0.029s     0.029s     26.61MB      1×
        postsolver_iter                    0.029s     0.029s     26.57MB      1×
    warn_global                        0.001s     0.001s      0.10MB      1×
    witness                            0.001s     0.001s      0.14MB      1×
      determine                          0.001s     0.001s      0.14MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
