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


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Warning][Witness] couldn't locate invariant: (a == (256LL) && q == (0LL)) || (!(a == (256LL)) && a == (1LL) && q == (0LL)) || ((!(a == (256LL)) || (a == (256LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (0LL)))) && a == (4LL) && q == (128LL)) || ((!(a == (256LL)) || (a == (256LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (0LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && a == (2LL) && q == (256LL)) || ((!(a == (256LL)) || (a == (256LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (0LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && !(q == (256LL)) && a == (2LL) && q == (24LL)) || ((!(a == (256LL)) || (a == (256LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (0LL)))) && !(q == (128LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && a == (4LL) && q == (16LL)) || (!(a == (256LL)) && !(a == (1LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && a == (1024LL) && q == (0LL)) || ((!(a == (256LL)) || (a == (256LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (0LL)))) && !(q == (256LL)) && !(q == (24LL)) && !(a == (4LL)) && (!(a == (1024LL)) || (a == (1024LL) && !(q == (0LL)))) && a == (2LL) && q == (16LL)) || ((!(a == (256LL)) || (a == (256LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (0LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && !(q == (256LL)) && !(q == (24LL)) && (!(a == (1024LL)) || (a == (1024LL) && !(q == (0LL)))) && !(q == (16LL)) && a == (2LL) && q == (8LL)) || ((!(a == (256LL)) || (a == (256LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (0LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && (!(a == (1024LL)) || (a == (1024LL) && !(q == (0LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && a == (8LL) && q == (32LL)) || (!(q == (0LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && a == (1LL) && q == (4LL)) || (!(q == (0LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && !(a == (8LL)) && !(q == (4LL)) && a == (1LL) && q == (32LL)) || (!(a == (256LL)) && !(a == (1LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && !(a == (1024LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && a == (128LL) && q == (0LL)) || (!(a == (256LL)) && !(a == (1LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && !(a == (1024LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && !(q == (32LL)) && !(a == (128LL)) && a == (8LL) && q == (0LL)) || ((!(a == (256LL)) || (a == (256LL) && !(q == (0LL)))) && !(q == (128LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && !(q == (16LL)) && (!(a == (1024LL)) || (a == (1024LL) && !(q == (0LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && !(a == (8LL)) && !(a == (1LL)) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && a == (4LL) && q == (32LL)) || (!(a == (256LL)) && !(a == (1LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && !(a == (1024LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && !(a == (128LL)) && !(a == (8LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && a == (512LL) && q == (0LL)) || (!(q == (0LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && !(q == (4LL)) && !(q == (32LL)) && a == (1LL) && q == (512LL)) || (!(a == (256LL)) && !(a == (1LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && !(a == (1024LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && !(a == (128LL)) && !(a == (8LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && !(a == (512LL)) && a == (2048LL) && q == (0LL)) || (!(q == (0LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && !(q == (4LL)) && !(q == (32LL)) && !(q == (512LL)) && a == (1LL) && q == (36LL)) || (!(q == (0LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && !(q == (4LL)) && !(q == (32LL)) && !(q == (512LL)) && !(q == (36LL)) && a == (1LL) && q == (40LL)) || (!(a == (256LL)) && !(a == (1LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && !(q == (256LL)) && !(q == (24LL)) && !(a == (1024LL)) && !(q == (16LL)) && !(q == (8LL)) && !(a == (128LL)) && !(a == (8LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && !(a == (512LL)) && !(a == (2048LL)) && a == (2LL) && q == (0LL)) || (!(a == (4LL)) && !(q == (256LL)) && !(q == (24LL)) && !(q == (16LL)) && !(q == (8LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (4LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (32LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (512LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (36LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (40LL)))) && !(q == (0LL)) && a == (2LL) && q == (128LL)) || (!(q == (0LL)) && !(a == (4LL)) && !(a == (2LL)) && !(q == (4LL)) && !(q == (32LL)) && !(q == (512LL)) && !(q == (36LL)) && !(q == (40LL)) && a == (1LL) && q == (16LL)) || (!(q == (0LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && !(q == (4LL)) && !(q == (32LL)) && !(q == (512LL)) && !(q == (36LL)) && !(q == (40LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && !(q == (16LL)) && a == (1LL) && q == (64LL)) || (!(a == (256LL)) && !(a == (1LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && !(a == (1024LL)) && !(a == (128LL)) && !(a == (8LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && !(a == (512LL)) && !(a == (2048LL)) && !(a == (2LL)) && a == (32LL) && q == (0LL)) || (!(q == (0LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && !(q == (4LL)) && !(q == (32LL)) && !(q == (512LL)) && !(q == (36LL)) && !(q == (40LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && !(q == (16LL)) && !(q == (64LL)) && a == (1LL) && q == (20LL)) || (!(a == (256LL)) && !(a == (1LL)) && !(q == (128LL)) && !(q == (16LL)) && !(a == (1024LL)) && !(a == (128LL)) && !(a == (8LL)) && !(q == (32LL)) && !(a == (512LL)) && !(a == (2048LL)) && !(a == (2LL)) && !(a == (32LL)) && a == (4LL) && q == (0LL)) || (!(q == (0LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && !(a == (2LL)) && !(q == (4LL)) && !(q == (32LL)) && !(q == (512LL)) && !(q == (36LL)) && !(q == (40LL)) && !(q == (16LL)) && !(q == (64LL)) && !(q == (20LL)) && a == (1LL) && q == (8LL)) || (!(q == (0LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && !(a == (2LL)) && !(q == (4LL)) && !(q == (32LL)) && !(q == (512LL)) && !(q == (36LL)) && !(q == (40LL)) && !(q == (16LL)) && !(q == (64LL)) && !(q == (20LL)) && !(q == (8LL)) && a == (1LL) && q == (24LL)) || (!(a == (256LL)) && !(a == (1LL)) && !(a == (1024LL)) && !(a == (128LL)) && !(a == (8LL)) && !(a == (512LL)) && !(a == (2048LL)) && !(a == (2LL)) && !(a == (32LL)) && !(a == (4LL)) && a == (64LL) && q == (0LL)) || (!(q == (0LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && !(q == (4LL)) && !(q == (32LL)) && !(q == (512LL)) && !(q == (36LL)) && !(q == (40LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && !(q == (16LL)) && !(q == (64LL)) && !(q == (20LL)) && !(q == (8LL)) && !(q == (24LL)) && a == (1LL) && q == (12LL)) || (!(q == (128LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && !(q == (16LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && !(q == (32LL)) && !(a == (1LL)) && !(q == (0LL)) && a == (4LL) && q == (64LL)) || (!(q == (0LL)) && !(a == (4LL)) && !(q == (4LL)) && !(q == (32LL)) && !(q == (512LL)) && !(q == (36LL)) && !(q == (40LL)) && !(a == (2LL)) && !(q == (16LL)) && !(q == (64LL)) && !(q == (20LL)) && !(q == (8LL)) && !(q == (24LL)) && !(q == (12LL)) && a == (1LL) && q == (128LL)) || (!(q == (0LL)) && !(a == (2LL)) && !(q == (4LL)) && !(q == (32LL)) && !(q == (512LL)) && !(q == (36LL)) && !(q == (40LL)) && !(q == (16LL)) && !(q == (64LL)) && !(q == (20LL)) && !(q == (8LL)) && !(q == (24LL)) && !(q == (12LL)) && !(q == (128LL)) && a == (1LL) && q == (256LL)) || (!(a == (256LL)) && !(a == (1LL)) && !(a == (1024LL)) && !(a == (128LL)) && !(a == (8LL)) && !(a == (512LL)) && !(a == (2048LL)) && !(a == (2LL)) && !(a == (32LL)) && !(a == (4LL)) && !(a == (64LL)) && a == (16LL) && q == (0LL)) || (!(q == (256LL)) && !(q == (24LL)) && !(q == (16LL)) && !(q == (8LL)) && !(a == (8LL)) && !(a == (1LL)) && !(a == (4LL)) && !(q == (0LL)) && !(q == (128LL)) && a == (2LL) && q == (32LL)) || (!(q == (256LL)) && !(q == (24LL)) && !(q == (16LL)) && !(q == (8LL)) && !(q == (0LL)) && !(q == (128LL)) && !(a == (1LL)) && !(a == (4LL)) && !(q == (32LL)) && a == (2LL) && q == (64LL)) || (!(q == (0LL)) && !(q == (4LL)) && !(q == (32LL)) && !(q == (512LL)) && !(q == (36LL)) && !(q == (40LL)) && !(q == (16LL)) && !(q == (64LL)) && !(q == (20LL)) && !(q == (8LL)) && !(q == (24LL)) && !(q == (12LL)) && !(q == (128LL)) && !(q == (256LL)) && a == (1LL) && q == (68LL)) || (!(q == (32LL)) && !(q == (0LL)) && !(a == (1LL)) && !(a == (4LL)) && !(a == (2LL)) && a == (8LL) && q == (64LL)) (../plain/cohendiv-ll.c:53:6)
[Warning][Witness] couldn't locate invariant: (a == (1LL) && q == (256LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (256LL)))) && a == (2LL) && q == (8LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && a == (4LL) && q == (64LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (256LL)))) && !(q == (8LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && a == (2LL) && q == (16LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && a == (8LL) && q == (32LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && !(a == (8LL)) && a == (16LL) && q == (32LL)) || (!(q == (256LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && a == (1LL) && q == (20LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (256LL)))) && !(q == (8LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (16LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (20LL)))) && a == (2LL) && q == (24LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (20LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && a == (128LL) && q == (0LL)) || (!(a == (1LL)) && !(q == (8LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (16LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (24LL)) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && a == (2LL) && q == (256LL)) || (!(q == (8LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (16LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (20LL)))) && !(q == (24LL)) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && !(q == (256LL)) && a == (2LL) && q == (512LL)) || (!(q == (8LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (16LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(a == (1LL)) && !(q == (24LL)) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && !(q == (256LL)) && !(q == (512LL)) && a == (2LL) && q == (20LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (20LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && !(a == (128LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (20LL)))) && a == (2048LL) && q == (0LL)) || (!(a == (1LL)) && !(q == (64LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && !(a == (2LL)) && (!(a == (2048LL)) || (a == (2048LL) && !(q == (0LL)))) && a == (4LL) && q == (256LL)) || (!(a == (2LL)) && !(q == (64LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (20LL)))) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && (!(a == (2048LL)) || (a == (2048LL) && !(q == (0LL)))) && !(q == (256LL)) && a == (4LL) && q == (8LL)) || (!(q == (256LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (20LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && !(a == (128LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && !(a == (2048LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && a == (1LL) && q == (0LL)) || (!(q == (64LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && !(a == (128LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (20LL)))) && !(a == (2048LL)) && !(q == (256LL)) && !(q == (8LL)) && !(a == (1LL)) && a == (4LL) && q == (0LL)) || (!(q == (256LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (20LL)) && !(a == (2LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && !(q == (0LL)) && a == (1LL) && q == (24LL)) || ((!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && !(a == (128LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (20LL)))) && !(a == (2048LL)) && !(a == (1LL)) && !(a == (4LL)) && a == (64LL) && q == (0LL)) || (!(q == (256LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (20LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && !(q == (0LL)) && !(q == (24LL)) && a == (1LL) && q == (40LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (256LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(a == (2LL)) && !(q == (32LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (20LL)))) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && (!(a == (2048LL)) || (a == (2048LL) && !(q == (0LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (256LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (0LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (24LL)))) && (!(a == (64LL)) || (a == (64LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (40LL)))) && a == (8LL) && q == (16LL)) || (!(q == (256LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (20LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && !(q == (0LL)) && !(q == (24LL)) && !(q == (40LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (16LL)))) && a == (1LL) && q == (68LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (32LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (20LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (20LL)))) && (!(a == (2048LL)) || (a == (2048LL) && !(q == (0LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (256LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (0LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (24LL)))) && (!(a == (64LL)) || (a == (64LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (40LL)))) && !(q == (16LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (68LL)))) && a == (8LL) && q == (128LL)) || ((!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && !(a == (128LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (20LL)))) && !(a == (2048LL)) && !(a == (1LL)) && !(a == (4LL)) && !(a == (64LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (16LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (128LL)))) && a == (512LL) && q == (0LL)) || (!(q == (256LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(a == (2LL)) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (20LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && !(q == (0LL)) && !(q == (24LL)) && !(q == (40LL)) && !(a == (8LL)) && !(q == (68LL)) && a == (1LL) && q == (16LL)) || ((!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && !(a == (128LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (20LL)))) && !(a == (2048LL)) && !(a == (1LL)) && !(a == (4LL)) && !(a == (64LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (16LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (128LL)))) && !(a == (512LL)) && a == (256LL) && q == (0LL)) || (!(q == (256LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (20LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && !(q == (0LL)) && !(q == (24LL)) && !(q == (40LL)) && !(q == (68LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (128LL)))) && !(q == (16LL)) && a == (1LL) && q == (10LL)) || (!(q == (8LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (16LL)) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (24LL)) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && !(q == (256LL)) && !(q == (512LL)) && !(q == (20LL)) && (!(a == (2048LL)) || (a == (2048LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (0LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (0LL)))) && (!(a == (64LL)) || (a == (64LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (40LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (68LL)))) && !(a == (8LL)) && (!(a == (512LL)) || (a == (512LL) && !(q == (0LL)))) && (!(a == (256LL)) || (a == (256LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (10LL)))) && a == (2LL) && q == (128LL)) || (!(q == (256LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (20LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && !(q == (0LL)) && !(q == (24LL)) && !(q == (40LL)) && !(q == (68LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (128LL)))) && !(q == (16LL)) && !(q == (10LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && a == (1LL) && q == (130LL)) || ((!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && !(a == (128LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (20LL)))) && !(a == (2048LL)) && !(a == (1LL)) && !(a == (4LL)) && !(a == (64LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (16LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (128LL)))) && !(a == (512LL)) && !(a == (256LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && a == (1024LL) && q == (0LL)) || ((!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && !(a == (128LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (20LL)))) && !(a == (2048LL)) && !(a == (1LL)) && !(a == (4LL)) && !(a == (64LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (16LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (128LL)))) && !(a == (512LL)) && !(a == (256LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && !(a == (1024LL)) && a == (32LL) && q == (0LL)) || (!(q == (64LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && !(a == (8LL)) && !(a == (16LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (20LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (20LL)))) && !(q == (256LL)) && !(q == (8LL)) && !(q == (0LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (24LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (40LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (68LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (16LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (10LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (130LL)))) && a == (4LL) && q == (32LL)) || (!(q == (256LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (20LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && !(q == (0LL)) && !(q == (24LL)) && !(q == (40LL)) && !(q == (68LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (128LL)))) && !(q == (16LL)) && !(q == (10LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && !(q == (130LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && a == (1LL) && q == (2LL)) || (!(q == (256LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (20LL)) && !(a == (2LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && !(q == (0LL)) && !(q == (24LL)) && !(q == (40LL)) && !(q == (68LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (128LL)))) && !(q == (16LL)) && !(q == (10LL)) && !(q == (130LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && !(q == (2LL)) && a == (1LL) && q == (512LL)) || (!(q == (64LL)) && !(a == (2LL)) && !(q == (256LL)) && !(q == (8LL)) && !(q == (0LL)) && !(a == (8LL)) && !(a == (1LL)) && !(q == (32LL)) && a == (4LL) && q == (16LL)) || (!(q == (256LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (20LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && !(q == (0LL)) && !(q == (24LL)) && !(q == (40LL)) && !(q == (68LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (128LL)))) && !(q == (16LL)) && !(q == (10LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && !(q == (130LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && !(q == (2LL)) && !(q == (512LL)) && a == (1LL) && q == (34LL)) || (!(q == (8LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (16LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (24LL)) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && !(q == (256LL)) && !(q == (512LL)) && !(q == (20LL)) && (!(a == (2048LL)) || (a == (2048LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (0LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (0LL)))) && (!(a == (64LL)) || (a == (64LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (40LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (68LL)))) && (!(a == (512LL)) || (a == (512LL) && !(q == (0LL)))) && (!(a == (256LL)) || (a == (256LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (10LL)))) && !(q == (128LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (130LL)))) && (!(a == (1024LL)) || (a == (1024LL) && !(q == (0LL)))) && (!(a == (32LL)) || (a == (32LL) && !(q == (0LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (2LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (34LL)))) && a == (2LL) && q == (4LL)) || (!(q == (8LL)) && !(q == (16LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (24LL)) && !(a == (128LL)) && !(q == (256LL)) && !(q == (512LL)) && !(q == (20LL)) && !(a == (2048LL)) && !(a == (1LL)) && !(a == (4LL)) && !(a == (64LL)) && !(a == (512LL)) && !(a == (256LL)) && !(q == (128LL)) && !(a == (1024LL)) && !(a == (32LL)) && !(q == (4LL)) && a == (2LL) && q == (0LL)) || (!(q == (256LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (20LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && !(q == (0LL)) && !(q == (24LL)) && !(q == (40LL)) && !(q == (68LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (128LL)))) && !(q == (16LL)) && !(q == (10LL)) && !(q == (130LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && !(q == (2LL)) && !(q == (512LL)) && !(q == (34LL)) && !(a == (2LL)) && a == (1LL) && q == (4LL)) || (!(q == (256LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (20LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && !(q == (0LL)) && !(q == (24LL)) && !(q == (40LL)) && !(q == (68LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (128LL)))) && !(q == (16LL)) && !(q == (10LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && !(q == (130LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && !(q == (2LL)) && !(q == (512LL)) && !(q == (34LL)) && !(q == (4LL)) && a == (1LL) && q == (12LL)) || (!(q == (256LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (20LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && !(q == (0LL)) && !(q == (24LL)) && !(q == (40LL)) && !(q == (68LL)) && !(a == (8LL)) && !(q == (16LL)) && !(q == (10LL)) && !(a == (2LL)) && !(q == (130LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && !(q == (2LL)) && !(q == (512LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (12LL)) && a == (1LL) && q == (128LL)) || (!(q == (256LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (20LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && !(q == (0LL)) && !(q == (24LL)) && !(q == (40LL)) && !(q == (68LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (130LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && !(q == (2LL)) && !(q == (512LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (12LL)) && !(q == (128LL)) && a == (1LL) && q == (14LL)) || (!(q == (256LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && !(a == (4LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (20LL)) && !(q == (0LL)) && !(q == (24LL)) && !(q == (40LL)) && !(q == (68LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (130LL)) && !(q == (2LL)) && !(q == (512LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (12LL)) && !(q == (128LL)) && !(q == (14LL)) && a == (1LL) && q == (64LL)) || (!(q == (64LL)) && !(q == (256LL)) && !(q == (8LL)) && !(q == (0LL)) && !(a == (8LL)) && !(a == (2LL)) && !(q == (32LL)) && !(q == (16LL)) && !(a == (1LL)) && a == (4LL) && q == (128LL)) || (!(q == (256LL)) && !(a == (2LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (20LL)) && !(a == (4LL)) && !(q == (0LL)) && !(q == (24LL)) && !(q == (40LL)) && !(q == (68LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (130LL)) && !(q == (2LL)) && !(q == (512LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (12LL)) && !(q == (128LL)) && !(q == (14LL)) && !(q == (64LL)) && a == (1LL) && q == (8LL)) || (!(q == (256LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (20LL)) && !(q == (0LL)) && !(q == (24LL)) && !(q == (40LL)) && !(q == (68LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (130LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && !(q == (2LL)) && !(q == (512LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (12LL)) && !(q == (128LL)) && !(q == (14LL)) && !(q == (64LL)) && !(q == (8LL)) && a == (1LL) && q == (36LL)) || (!(q == (8LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (16LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (24LL)) && !(q == (256LL)) && !(q == (512LL)) && !(q == (20LL)) && !(q == (128LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && !(q == (4LL)) && !(q == (0LL)) && !(a == (1LL)) && a == (2LL) && q == (36LL)) || (!(q == (256LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (20LL)) && !(q == (0LL)) && !(q == (24LL)) && !(q == (40LL)) && !(q == (68LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (130LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && !(q == (2LL)) && !(q == (512LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (12LL)) && !(q == (128LL)) && !(q == (14LL)) && !(q == (64LL)) && !(q == (8LL)) && !(q == (36LL)) && a == (1LL) && q == (66LL)) || (!(q == (256LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (20LL)) && !(q == (0LL)) && !(q == (24LL)) && !(q == (40LL)) && !(q == (68LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (130LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && !(q == (2LL)) && !(q == (512LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (12LL)) && !(q == (128LL)) && !(q == (14LL)) && !(q == (64LL)) && !(q == (8LL)) && !(q == (36LL)) && !(q == (66LL)) && a == (1LL) && q == (18LL)) || (!(q == (32LL)) && !(a == (128LL)) && !(a == (2048LL)) && !(a == (1LL)) && !(a == (4LL)) && !(a == (64LL)) && !(q == (16LL)) && !(q == (128LL)) && !(a == (512LL)) && !(a == (256LL)) && !(a == (1024LL)) && !(a == (32LL)) && !(a == (2LL)) && a == (8LL) && q == (0LL)) || (!(q == (256LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (32LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (32LL)))) && !(q == (20LL)) && !(q == (0LL)) && !(q == (24LL)) && !(q == (40LL)) && !(q == (68LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (130LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && !(q == (2LL)) && !(q == (512LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (12LL)) && !(q == (128LL)) && !(q == (14LL)) && !(q == (64LL)) && !(q == (8LL)) && !(q == (36LL)) && !(q == (66LL)) && !(q == (18LL)) && a == (1LL) && q == (22LL)) || ((!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && !(a == (4LL)) && !(q == (32LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (20LL)))) && !(q == (16LL)) && !(q == (128LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (4LL)))) && !(a == (1LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (36LL)))) && !(q == (0LL)) && a == (8LL) && q == (64LL)) || (!(q == (32LL)) && !(a == (128LL)) && !(a == (2048LL)) && !(a == (1LL)) && !(a == (4LL)) && !(a == (64LL)) && !(a == (512LL)) && !(a == (256LL)) && !(a == (1024LL)) && !(a == (32LL)) && !(a == (2LL)) && !(a == (8LL)) && a == (16LL) && q == (0LL)) || (!(q == (8LL)) && !(q == (16LL)) && !(a == (8LL)) && !(a == (16LL)) && !(q == (24LL)) && !(q == (256LL)) && !(q == (512LL)) && !(q == (20LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (40LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (68LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (10LL)))) && !(q == (128LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (130LL)))) && !(a == (4LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (2LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (34LL)))) && !(q == (4LL)) && !(q == (0LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (12LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (14LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (64LL)))) && !(q == (36LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (66LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (18LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (22LL)))) && a == (2LL) && q == (32LL)) || (!(q == (8LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (16LL)) && !(q == (24LL)) && !(q == (256LL)) && !(q == (512LL)) && !(q == (20LL)) && !(q == (128LL)) && !(q == (4LL)) && !(q == (0LL)) && !(a == (1LL)) && !(q == (36LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (64LL)))) && !(q == (32LL)) && a == (2LL) && q == (12LL)) || (!(q == (256LL)) && !(a == (8LL)) && !(a == (16LL)) && !(q == (20LL)) && !(q == (0LL)) && !(q == (24LL)) && !(q == (40LL)) && !(q == (68LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (130LL)) && !(a == (4LL)) && !(q == (2LL)) && !(q == (512LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (12LL)) && !(q == (128LL)) && !(q == (14LL)) && !(q == (64LL)) && !(q == (8LL)) && !(q == (36LL)) && !(q == (66LL)) && !(q == (18LL)) && !(q == (22LL)) && !(a == (2LL)) && a == (1LL) && q == (32LL)) || (!(q == (8LL)) && !(a == (4LL)) && !(q == (16LL)) && !(q == (24LL)) && !(q == (256LL)) && !(q == (512LL)) && !(q == (20LL)) && !(q == (128LL)) && !(q == (4LL)) && !(q == (0LL)) && !(a == (1LL)) && !(q == (36LL)) && !(a == (8LL)) && !(q == (32LL)) && !(q == (12LL)) && a == (2LL) && q == (64LL)) || (!(q == (256LL)) && !(q == (20LL)) && !(q == (0LL)) && !(q == (24LL)) && !(q == (40LL)) && !(q == (68LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (130LL)) && !(q == (2LL)) && !(q == (512LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (12LL)) && !(q == (128LL)) && !(q == (14LL)) && !(q == (64LL)) && !(q == (8LL)) && !(q == (36LL)) && !(q == (66LL)) && !(q == (18LL)) && !(q == (22LL)) && !(q == (32LL)) && a == (1LL) && q == (6LL)) || (!(q == (256LL)) && !(q == (20LL)) && !(q == (0LL)) && !(q == (24LL)) && !(q == (40LL)) && !(q == (68LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (130LL)) && !(q == (2LL)) && !(q == (512LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (12LL)) && !(q == (128LL)) && !(q == (14LL)) && !(q == (64LL)) && !(q == (8LL)) && !(q == (36LL)) && !(q == (66LL)) && !(q == (18LL)) && !(q == (22LL)) && !(q == (32LL)) && !(q == (6LL)) && a == (1LL) && q == (1024LL)) (../plain/cohendiv-ll.c:48:6)
[Warning][Witness] couldn't locate invariant: (a == (1LL) && q == (130LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (130LL)))) && a == (2LL) && q == (20LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (130LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (20LL)))) && a == (4LL) && q == (16LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (130LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (20LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && a == (512LL) && q == (0LL)) || (!(q == (130LL)) && !(a == (2LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && (!(a == (512LL)) || (a == (512LL) && !(q == (0LL)))) && a == (1LL) && q == (20LL)) || (!(q == (130LL)) && !(a == (4LL)) && (!(a == (512LL)) || (a == (512LL) && !(q == (0LL)))) && !(q == (20LL)) && a == (1LL) && q == (16LL)) || (!(q == (130LL)) && (!(a == (512LL)) || (a == (512LL) && !(q == (0LL)))) && !(q == (20LL)) && !(q == (16LL)) && a == (1LL) && q == (12LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (130LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (20LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && !(a == (512LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (20LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (16LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (12LL)))) && a == (128LL) && q == (0LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (130LL)))) && !(q == (20LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && !(a == (512LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (16LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (12LL)))) && !(a == (128LL)) && a == (2LL) && q == (0LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (130LL)))) && !(q == (20LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (16LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (12LL)))) && !(q == (0LL)) && a == (2LL) && q == (128LL)) || (!(q == (130LL)) && (!(a == (512LL)) || (a == (512LL) && !(q == (0LL)))) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (0LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && a == (1LL) && q == (6LL)) || (!(q == (130LL)) && (!(a == (512LL)) || (a == (512LL) && !(q == (0LL)))) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (0LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && !(q == (6LL)) && a == (1LL) && q == (14LL)) || (!(q == (130LL)) && (!(a == (512LL)) || (a == (512LL) && !(q == (0LL)))) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (0LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && !(q == (6LL)) && !(q == (14LL)) && a == (1LL) && q == (40LL)) || ((!(a == (2LL)) || (a == (2LL) && !(q == (20LL)))) && !(a == (4LL)) && (!(a == (512LL)) || (a == (512LL) && !(q == (0LL)))) && !(a == (1LL)) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (0LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && a == (8LL) && q == (16LL)) || (!(q == (130LL)) && (!(a == (512LL)) || (a == (512LL) && !(q == (0LL)))) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (0LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && !(q == (6LL)) && !(q == (14LL)) && !(q == (40LL)) && a == (1LL) && q == (256LL)) || ((!(a == (2LL)) || (a == (2LL) && !(q == (20LL)))) && !(q == (16LL)) && (!(a == (512LL)) || (a == (512LL) && !(q == (0LL)))) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (0LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && !(a == (1LL)) && a == (4LL) && q == (256LL)) || (!(q == (130LL)) && !(a == (512LL)) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && !(a == (128LL)) && !(a == (2LL)) && !(q == (6LL)) && !(q == (14LL)) && !(q == (40LL)) && !(q == (256LL)) && a == (1LL) && q == (0LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (130LL)))) && !(q == (20LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (16LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (12LL)))) && !(q == (0LL)) && !(q == (128LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (6LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (14LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (40LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (16LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (256LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (256LL)))) && a == (2LL) && q == (8LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (130LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (20LL)))) && !(q == (16LL)) && (!(a == (512LL)) || (a == (512LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (20LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (12LL)))) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (0LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (6LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (14LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (40LL)))) && !(q == (256LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (0LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && a == (4LL) && q == (64LL)) || (!(q == (130LL)) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && !(q == (6LL)) && !(q == (14LL)) && !(q == (40LL)) && !(q == (256LL)) && !(q == (0LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && a == (1LL) && q == (32LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (130LL)))) && !(q == (16LL)) && (!(a == (512LL)) || (a == (512LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (20LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (12LL)))) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && !(a == (2LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (6LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (14LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (40LL)))) && !(q == (256LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (0LL)))) && !(q == (64LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (32LL)))) && a == (4LL) && q == (128LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (130LL)))) && !(q == (20LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (16LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (12LL)))) && !(q == (0LL)) && !(q == (128LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (6LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (14LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (40LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (16LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (256LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (256LL)))) && !(q == (8LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (32LL)))) && a == (2LL) && q == (512LL)) || (!(q == (20LL)) && !(a == (4LL)) && !(a == (1LL)) && !(q == (0LL)) && !(q == (128LL)) && !(a == (8LL)) && !(q == (8LL)) && !(q == (512LL)) && a == (2LL) && q == (16LL)) || (!(q == (130LL)) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && !(q == (6LL)) && !(q == (14LL)) && !(q == (40LL)) && !(q == (256LL)) && !(q == (0LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (32LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && a == (1LL) && q == (36LL)) || (!(q == (130LL)) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && !(q == (6LL)) && !(q == (14LL)) && !(q == (40LL)) && !(q == (256LL)) && !(q == (0LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (32LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && !(q == (36LL)) && a == (1LL) && q == (10LL)) || ((!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && !(a == (512LL)) && !(a == (128LL)) && !(a == (2LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (16LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (256LL)))) && !(a == (1LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && a == (16LL) && q == (0LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (130LL)))) && (!(a == (512LL)) || (a == (512LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (20LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (12LL)))) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && !(a == (2LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (6LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (14LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (40LL)))) && !(q == (16LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (256LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (32LL)))) && !(a == (4LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (36LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (10LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (0LL)))) && a == (8LL) && q == (128LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (130LL)))) && !(q == (16LL)) && (!(a == (512LL)) || (a == (512LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (20LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (12LL)))) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (6LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (14LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (40LL)))) && !(q == (256LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (0LL)))) && !(a == (2LL)) && !(q == (64LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (32LL)))) && !(q == (128LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (36LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (10LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (0LL)))) && a == (4LL) && q == (8LL)) || ((!(a == (2LL)) || (a == (2LL) && !(q == (20LL)))) && !(q == (16LL)) && (!(a == (512LL)) || (a == (512LL) && !(q == (0LL)))) && (!(a == (128LL)) || (a == (128LL) && !(q == (0LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (0LL)))) && !(q == (256LL)) && !(q == (64LL)) && !(a == (1LL)) && !(q == (128LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && (!(a == (16LL)) || (a == (16LL) && !(q == (0LL)))) && !(q == (8LL)) && a == (4LL) && q == (32LL)) || (!(q == (20LL)) && !(q == (0LL)) && !(q == (128LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (256LL)))) && !(q == (8LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (512LL)) && !(q == (16LL)) && !(a == (1LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && a == (2LL) && q == (36LL)) || (!(a == (512LL)) && !(a == (128LL)) && !(a == (2LL)) && !(q == (16LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (256LL)))) && !(a == (1LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(a == (16LL)) && !(q == (128LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && a == (8LL) && q == (0LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (130LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (20LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (20LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (12LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (6LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (14LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (40LL)))) && !(q == (16LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && !(a == (4LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (32LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (36LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (10LL)))) && !(q == (128LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (36LL)))) && !(q == (0LL)) && a == (8LL) && q == (64LL)) || (!(q == (130LL)) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && !(q == (6LL)) && !(q == (14LL)) && !(q == (40LL)) && !(q == (256LL)) && !(q == (0LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (32LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && !(q == (36LL)) && !(q == (10LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (128LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (64LL)))) && a == (1LL) && q == (1024LL)) || (!(q == (20LL)) && !(q == (0LL)) && !(q == (128LL)) && !(q == (8LL)) && !(a == (1LL)) && !(q == (512LL)) && !(q == (16LL)) && !(a == (4LL)) && !(q == (36LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (64LL)))) && a == (2LL) && q == (32LL)) || ((!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && !(a == (512LL)) && !(a == (128LL)) && !(a == (2LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (256LL)))) && !(a == (1LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && !(a == (16LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && !(a == (8LL)) && a == (1024LL) && q == (0LL)) || ((!(a == (8LL)) || (a == (8LL) && !(q == (16LL)))) && !(a == (1LL)) && !(q == (0LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (128LL)))) && !(a == (4LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (64LL)))) && !(a == (2LL)) && a == (16LL) && q == (32LL)) || ((!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && !(a == (512LL)) && !(a == (128LL)) && !(a == (2LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (256LL)))) && !(a == (1LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && !(a == (16LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && !(a == (8LL)) && !(a == (1024LL)) && a == (2048LL) && q == (0LL)) || (!(q == (20LL)) && !(a == (1LL)) && !(q == (0LL)) && !(q == (128LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (256LL)))) && !(q == (8LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (512LL)) && !(q == (16LL)) && !(q == (36LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (64LL)))) && !(q == (32LL)) && a == (2LL) && q == (12LL)) || (!(q == (130LL)) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && !(q == (6LL)) && !(q == (14LL)) && !(q == (40LL)) && !(q == (256LL)) && !(q == (0LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (32LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && !(q == (36LL)) && !(q == (10LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (128LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (64LL)))) && !(q == (1024LL)) && a == (1LL) && q == (24LL)) || (!(q == (130LL)) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && !(q == (6LL)) && !(q == (14LL)) && !(q == (40LL)) && !(q == (256LL)) && !(q == (0LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (32LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && !(a == (2LL)) && !(q == (36LL)) && !(q == (10LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (128LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (64LL)))) && !(q == (1024LL)) && !(q == (24LL)) && a == (1LL) && q == (512LL)) || (!(q == (130LL)) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && !(q == (6LL)) && !(q == (14LL)) && !(q == (40LL)) && !(q == (256LL)) && !(q == (0LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (32LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && !(q == (36LL)) && !(q == (10LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (128LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (64LL)))) && !(q == (1024LL)) && !(q == (24LL)) && !(q == (512LL)) && a == (1LL) && q == (34LL)) || ((!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && !(a == (512LL)) && !(a == (128LL)) && !(a == (2LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (256LL)))) && !(a == (1LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && !(a == (16LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && !(a == (8LL)) && !(a == (1024LL)) && !(a == (2048LL)) && a == (256LL) && q == (0LL)) || (!(q == (20LL)) && !(q == (0LL)) && !(q == (128LL)) && !(a == (1LL)) && !(a == (4LL)) && !(q == (8LL)) && !(q == (512LL)) && !(q == (16LL)) && !(q == (36LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (64LL)))) && !(q == (32LL)) && !(q == (12LL)) && a == (2LL) && q == (256LL)) || (!(q == (20LL)) && !(q == (0LL)) && !(q == (128LL)) && !(q == (8LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (512LL)) && !(q == (16LL)) && !(q == (36LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (64LL)))) && !(q == (32LL)) && !(q == (12LL)) && !(a == (1LL)) && !(q == (256LL)) && a == (2LL) && q == (24LL)) || (!(q == (130LL)) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && !(q == (6LL)) && !(q == (14LL)) && !(q == (40LL)) && !(q == (256LL)) && !(q == (0LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (32LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && !(q == (36LL)) && !(q == (10LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (128LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (64LL)))) && !(q == (1024LL)) && !(q == (24LL)) && !(q == (512LL)) && !(q == (34LL)) && a == (1LL) && q == (66LL)) || (!(q == (130LL)) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && !(q == (6LL)) && !(q == (14LL)) && !(q == (40LL)) && !(q == (256LL)) && !(q == (0LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (32LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && !(q == (36LL)) && !(q == (10LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (128LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (64LL)))) && !(q == (1024LL)) && !(q == (24LL)) && !(q == (512LL)) && !(q == (34LL)) && !(q == (66LL)) && a == (1LL) && q == (2LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (130LL)))) && !(q == (20LL)) && !(q == (0LL)) && !(q == (128LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (6LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (14LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (40LL)))) && !(q == (8LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (512LL)) && !(q == (16LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (10LL)))) && !(q == (36LL)) && (!(a == (8LL)) || (a == (8LL) && !(q == (64LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (1024LL)))) && !(q == (32LL)) && !(q == (12LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (34LL)))) && !(q == (256LL)) && !(q == (24LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (66LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (2LL)))) && a == (2LL) && q == (4LL)) || (!(q == (130LL)) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && !(a == (2LL)) && !(q == (6LL)) && !(q == (14LL)) && !(q == (40LL)) && !(q == (256LL)) && !(q == (0LL)) && !(q == (32LL)) && !(a == (4LL)) && !(q == (36LL)) && !(q == (10LL)) && !(a == (8LL)) && !(q == (1024LL)) && !(q == (24LL)) && !(q == (512LL)) && !(q == (34LL)) && !(q == (66LL)) && !(q == (2LL)) && a == (1LL) && q == (128LL)) || ((!(a == (1LL)) || (a == (1LL) && !(q == (130LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (20LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (20LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (16LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (12LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (128LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (6LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (14LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (40LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && !(a == (4LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (512LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (16LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (36LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (10LL)))) && !(q == (0LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (36LL)))) && !(a == (8LL)) && (!(a == (1LL)) || (a == (1LL) && !(q == (1024LL)))) && !(q == (32LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (12LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (24LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (512LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (34LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (256LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (24LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (66LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (2LL)))) && (!(a == (2LL)) || (a == (2LL) && !(q == (4LL)))) && (!(a == (1LL)) || (a == (1LL) && !(q == (128LL)))) && a == (16LL) && q == (64LL)) || ((!(a == (4LL)) || (a == (4LL) && !(q == (16LL)))) && !(a == (512LL)) && !(a == (128LL)) && !(a == (2LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (256LL)))) && !(a == (1LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (128LL)))) && !(a == (16LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && (!(a == (4LL)) || (a == (4LL) && !(q == (32LL)))) && !(a == (8LL)) && !(a == (1024LL)) && !(a == (2048LL)) && !(a == (256LL)) && a == (32LL) && q == (0LL)) || (!(q == (130LL)) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && !(q == (6LL)) && !(q == (14LL)) && !(q == (40LL)) && !(q == (256LL)) && !(q == (0LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (64LL)))) && !(q == (32LL)) && !(q == (36LL)) && !(q == (10LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && (!(a == (8LL)) || (a == (8LL) && !(q == (64LL)))) && !(q == (1024LL)) && !(q == (24LL)) && !(q == (512LL)) && !(q == (34LL)) && !(q == (66LL)) && !(q == (2LL)) && !(a == (2LL)) && !(q == (128LL)) && (!(a == (16LL)) || (a == (16LL) && !(q == (64LL)))) && a == (1LL) && q == (4LL)) || (!(q == (130LL)) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && !(q == (6LL)) && !(q == (14LL)) && !(q == (40LL)) && !(q == (256LL)) && !(q == (0LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && !(a == (4LL)) && !(q == (32LL)) && !(q == (36LL)) && !(q == (10LL)) && !(a == (8LL)) && !(q == (1024LL)) && !(q == (24LL)) && !(q == (512LL)) && !(q == (34LL)) && !(q == (66LL)) && !(q == (2LL)) && !(q == (128LL)) && !(a == (16LL)) && !(q == (4LL)) && a == (1LL) && q == (64LL)) || (!(q == (16LL)) && !(a == (512LL)) && !(a == (128LL)) && !(a == (2LL)) && !(q == (256LL)) && !(a == (1LL)) && !(q == (64LL)) && !(q == (128LL)) && !(a == (16LL)) && !(q == (8LL)) && !(q == (32LL)) && !(a == (8LL)) && !(a == (1024LL)) && !(a == (2048LL)) && !(a == (256LL)) && !(a == (32LL)) && a == (4LL) && q == (0LL)) || (!(a == (512LL)) && !(a == (128LL)) && !(a == (2LL)) && !(a == (1LL)) && !(a == (16LL)) && !(a == (8LL)) && !(a == (1024LL)) && !(a == (2048LL)) && !(a == (256LL)) && !(a == (32LL)) && !(a == (4LL)) && a == (64LL) && q == (0LL)) || (!(q == (130LL)) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && !(q == (6LL)) && !(q == (14LL)) && !(q == (40LL)) && !(q == (256LL)) && !(q == (0LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && !(q == (32LL)) && !(q == (36LL)) && !(q == (10LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && !(q == (1024LL)) && !(q == (24LL)) && !(q == (512LL)) && !(q == (34LL)) && !(q == (66LL)) && !(q == (2LL)) && !(q == (128LL)) && !(q == (4LL)) && !(q == (64LL)) && a == (1LL) && q == (18LL)) || (!(q == (20LL)) && !(q == (0LL)) && !(q == (128LL)) && !(q == (8LL)) && !(a == (4LL)) && !(q == (512LL)) && !(q == (16LL)) && !(q == (36LL)) && !(a == (8LL)) && !(q == (32LL)) && !(q == (12LL)) && !(q == (256LL)) && !(q == (24LL)) && !(q == (4LL)) && !(a == (16LL)) && !(a == (1LL)) && a == (2LL) && q == (64LL)) || (!(q == (130LL)) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && !(q == (6LL)) && !(q == (14LL)) && !(q == (40LL)) && !(q == (256LL)) && !(q == (0LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && !(q == (32LL)) && !(q == (36LL)) && !(q == (10LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && !(q == (1024LL)) && !(q == (24LL)) && !(q == (512LL)) && !(q == (34LL)) && !(q == (66LL)) && !(q == (2LL)) && !(q == (128LL)) && !(q == (4LL)) && !(q == (64LL)) && !(q == (18LL)) && a == (1LL) && q == (68LL)) || (!(q == (16LL)) && !(a == (1LL)) && !(q == (128LL)) && !(a == (4LL)) && !(q == (0LL)) && !(q == (64LL)) && !(a == (2LL)) && !(a == (16LL)) && a == (8LL) && q == (32LL)) || (!(q == (130LL)) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && !(q == (6LL)) && !(q == (14LL)) && !(q == (40LL)) && !(q == (256LL)) && !(q == (0LL)) && (!(a == (2LL)) || (a == (2LL) && !(q == (8LL)))) && !(q == (32LL)) && !(q == (36LL)) && !(q == (10LL)) && (!(a == (4LL)) || (a == (4LL) && !(q == (8LL)))) && !(q == (1024LL)) && !(q == (24LL)) && !(q == (512LL)) && !(q == (34LL)) && !(q == (66LL)) && !(q == (2LL)) && !(q == (128LL)) && !(q == (4LL)) && !(q == (64LL)) && !(q == (18LL)) && !(q == (68LL)) && a == (1LL) && q == (22LL)) || (!(q == (130LL)) && !(q == (20LL)) && !(q == (16LL)) && !(q == (12LL)) && !(q == (6LL)) && !(q == (14LL)) && !(q == (40LL)) && !(q == (256LL)) && !(q == (0LL)) && !(a == (2LL)) && !(q == (32LL)) && !(q == (36LL)) && !(q == (10LL)) && !(a == (4LL)) && !(q == (1024LL)) && !(q == (24LL)) && !(q == (512LL)) && !(q == (34LL)) && !(q == (66LL)) && !(q == (2LL)) && !(q == (128LL)) && !(q == (4LL)) && !(q == (64LL)) && !(q == (18LL)) && !(q == (68LL)) && !(q == (22LL)) && a == (1LL) && q == (8LL)) (../plain/cohendiv-ll.c:47:6)

runtime: 00:00:10.259
vars: 60, evals: 126

|rho|=60
|called|=11
|stable|=55
|infl|=57
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=45
Found 7 contexts for 5 functions. Top 5 functions:
2	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
2	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohendiv-ll.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohendiv-ll.c:11:1-13:1
1	contexts for entry state of main (2012) on ../plain/cohendiv-ll.c:22:1-64:1
1	contexts for entry state of reach_error (1999) on ../plain/cohendiv-ll.c:8:1-8:77

Memory statistics: total=3951.00MB, max=87.53MB, minor=3946.72MB, major=276.34MB, promoted=272.06MB
    minor collections=1891  major collections=21 compactions=0


runtime: 00:00:20.276
vars: 60, evals: 169

|rho|=60
|called|=11
|stable|=58
|infl|=57
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=45
Found 7 contexts for 5 functions. Top 5 functions:
2	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
2	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohendiv-ll.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohendiv-ll.c:11:1-13:1
1	contexts for entry state of main (2012) on ../plain/cohendiv-ll.c:22:1-64:1
1	contexts for entry state of reach_error (1999) on ../plain/cohendiv-ll.c:8:1-8:77

Memory statistics: total=7368.65MB, max=87.53MB, minor=7364.19MB, major=534.57MB, promoted=530.11MB
    minor collections=3528  major collections=37 compactions=0


runtime: 00:00:30.297
vars: 60, evals: 216

|rho|=60
|called|=11
|stable|=55
|infl|=57
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=45
Found 7 contexts for 5 functions. Top 5 functions:
2	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
2	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohendiv-ll.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohendiv-ll.c:11:1-13:1
1	contexts for entry state of main (2012) on ../plain/cohendiv-ll.c:22:1-64:1
1	contexts for entry state of reach_error (1999) on ../plain/cohendiv-ll.c:8:1-8:77

Memory statistics: total=10757.40MB, max=87.53MB, minor=10752.77MB, major=792.95MB, promoted=788.32MB
    minor collections=5150  major collections=50 compactions=0


runtime: 00:00:40.308
vars: 60, evals: 256

|rho|=60
|called|=11
|stable|=55
|infl|=57
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=45
Found 7 contexts for 5 functions. Top 5 functions:
2	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
2	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohendiv-ll.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohendiv-ll.c:11:1-13:1
1	contexts for entry state of main (2012) on ../plain/cohendiv-ll.c:22:1-64:1
1	contexts for entry state of reach_error (1999) on ../plain/cohendiv-ll.c:8:1-8:77

Memory statistics: total=14017.54MB, max=87.53MB, minor=14012.76MB, major=1034.05MB, promoted=1029.27MB
    minor collections=6711  major collections=67 compactions=0


runtime: 00:00:50.317
vars: 74, evals: 322

|rho|=74
|called|=11
|stable|=73
|infl|=71
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=56
Found 10 contexts for 5 functions. Top 5 functions:
4	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohendiv-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
2	contexts for entry state of reach_error (1999) on ../plain/cohendiv-ll.c:8:1-8:77
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohendiv-ll.c:11:1-13:1
1	contexts for entry state of main (2012) on ../plain/cohendiv-ll.c:22:1-64:1

Memory statistics: total=17543.24MB, max=87.53MB, minor=17538.27MB, major=1305.78MB, promoted=1300.81MB
    minor collections=8399  major collections=82 compactions=0


runtime: 00:01:00.324
vars: 74, evals: 355

|rho|=74
|called|=11
|stable|=74
|infl|=71
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=56
Found 10 contexts for 5 functions. Top 5 functions:
4	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohendiv-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
2	contexts for entry state of reach_error (1999) on ../plain/cohendiv-ll.c:8:1-8:77
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohendiv-ll.c:11:1-13:1
1	contexts for entry state of main (2012) on ../plain/cohendiv-ll.c:22:1-64:1

Memory statistics: total=21027.34MB, max=87.53MB, minor=21022.23MB, major=1529.12MB, promoted=1524.02MB
    minor collections=10065  major collections=94 compactions=0

