/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/hard-ll_valuebound50.yml.witness.yml --witness.yaml.validate graves-cpa/hard-ll_valuebound50.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/hard-ll_valuebound50.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: (p == (1LL) && q == (49LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && p == (2LL) && q == (22LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && p == (1LL) && q == (20LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && !(q == (22LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && p == (2LL) && q == (38LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && !(q == (22LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && !(q == (38LL)) && p == (2LL) && q == (50LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && p == (1LL) && q == (5LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && p == (1LL) && q == (3LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && p == (1LL) && q == (48LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && p == (1LL) && q == (26LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && p == (1LL) && q == (6LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && !(q == (22LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && !(q == (38LL)) && !(q == (50LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (5LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (3LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (48LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (26LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (6LL)))) && p == (2LL) && q == (16LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && p == (1LL) && q == (31LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && !(q == (31LL)) && p == (1LL) && q == (10LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && !(q == (31LL)) && !(q == (10LL)) && p == (1LL) && q == (21LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && !(q == (22LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && !(q == (38LL)) && !(q == (50LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (5LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (3LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (48LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (26LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (6LL)))) && !(q == (16LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (31LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (21LL)))) && p == (2LL) && q == (14LL)) || (!(q == (49LL)) && !(q == (20LL)) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(p == (2LL)) && p == (1LL) && q == (14LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (5LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (3LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (48LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (26LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (6LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (31LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (21LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (14LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (14LL)))) && p == (64LL) && q == (0LL)) || (!(q == (22LL)) && !(q == (38LL)) && !(q == (50LL)) && !(p == (1LL)) && !(q == (16LL)) && !(q == (14LL)) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && p == (2LL) && q == (6LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (5LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (3LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (48LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (26LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (6LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (31LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (21LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (14LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (14LL)))) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (6LL)))) && p == (4LL) && q == (44LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && !(q == (22LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && !(q == (38LL)) && !(q == (50LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (5LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (3LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (48LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (26LL)))) && !(q == (16LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (31LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (21LL)))) && !(q == (14LL)) && !(p == (64LL)) && !(q == (6LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && p == (2LL) && q == (0LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && p == (1LL) && q == (19LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && !(q == (19LL)) && p == (1LL) && q == (34LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (5LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (3LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (48LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (26LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (6LL)))) && !(p == (2LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (31LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (21LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (14LL)))) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && !(q == (44LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (19LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (34LL)))) && p == (4LL) && q == (16LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (5LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (3LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (48LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (26LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (6LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (31LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (21LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (14LL)))) && !(p == (64LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(p == (2LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (19LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (34LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && p == (32LL) && q == (0LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && !(q == (19LL)) && !(q == (34LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && p == (1LL) && q == (2LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && !(q == (19LL)) && !(q == (34LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && !(q == (2LL)) && p == (1LL) && q == (18LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && !(q == (22LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && !(q == (38LL)) && !(q == (50LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (5LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (3LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (48LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (26LL)))) && !(q == (16LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (31LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (21LL)))) && !(q == (14LL)) && !(q == (6LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(q == (0LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (19LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (34LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && p == (2LL) && q == (42LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && !(q == (19LL)) && !(q == (34LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && p == (1LL) && q == (36LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (5LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (3LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (48LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (26LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (6LL)))) && !(p == (2LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (31LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (21LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (14LL)))) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (19LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (34LL)))) && !(p == (4LL)) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (36LL)))) && p == (16LL) && q == (16LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && !(q == (19LL)) && !(q == (34LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && p == (1LL) && q == (17LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && !(q == (19LL)) && !(q == (34LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (17LL)) && p == (1LL) && q == (23LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (5LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (3LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (48LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (26LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (6LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (31LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (21LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (14LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (14LL)))) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (6LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (19LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (34LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (36LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (17LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (23LL)))) && p == (8LL) && q == (24LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && !(q == (19LL)) && !(q == (34LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (23LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (24LL)))) && p == (1LL) && q == (27LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && !(q == (19LL)) && !(q == (34LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (23LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (24LL)))) && !(q == (27LL)) && p == (1LL) && q == (8LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && !(q == (19LL)) && !(q == (34LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (23LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (24LL)))) && !(q == (27LL)) && !(q == (8LL)) && p == (1LL) && q == (33LL)) || (!(q == (49LL)) && !(q == (20LL)) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(p == (64LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(p == (2LL)) && !(q == (19LL)) && !(q == (34LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && !(p == (32LL)) && !(q == (2LL)) && !(q == (18LL)) && !(q == (36LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (23LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (24LL)))) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && p == (1LL) && q == (0LL)) || (!(q == (22LL)) && !(p == (1LL)) && !(q == (38LL)) && !(q == (50LL)) && !(q == (16LL)) && !(q == (14LL)) && !(q == (6LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(q == (0LL)) && !(q == (42LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (24LL)))) && p == (2LL) && q == (20LL)) || (!(q == (22LL)) && !(q == (38LL)) && !(q == (50LL)) && !(q == (16LL)) && !(q == (14LL)) && !(q == (6LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(q == (0LL)) && !(q == (42LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (24LL)))) && !(p == (1LL)) && !(q == (20LL)) && p == (2LL) && q == (8LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(q == (19LL)) && !(q == (34LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (23LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (24LL)))) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && p == (1LL) && q == (32LL)) || (!(q == (22LL)) && !(q == (38LL)) && !(q == (50LL)) && !(p == (1LL)) && !(q == (16LL)) && !(q == (14LL)) && !(q == (6LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(q == (0LL)) && !(q == (42LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (24LL)))) && !(q == (20LL)) && !(q == (8LL)) && p == (2LL) && q == (26LL)) || (!(q == (49LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(q == (19LL)) && !(q == (34LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (23LL)) && !(p == (8LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && p == (1LL) && q == (24LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (5LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (3LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (48LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (26LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (6LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (31LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (21LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (14LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (14LL)))) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (6LL)))) && !(q == (44LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (19LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (34LL)))) && !(q == (16LL)) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (36LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (17LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (23LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (24LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (27LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (8LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (33LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (20LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (8LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (32LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (26LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (24LL)))) && p == (4LL) && q == (40LL)) || (!(q == (22LL)) && !(q == (38LL)) && !(q == (50LL)) && !(q == (16LL)) && !(q == (14LL)) && !(q == (6LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(q == (0LL)) && !(p == (1LL)) && !(q == (42LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (24LL)))) && !(q == (20LL)) && !(q == (8LL)) && !(q == (26LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && p == (2LL) && q == (18LL)) || (!(q == (49LL)) && !(p == (2LL)) && !(q == (20LL)) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(q == (19LL)) && !(q == (34LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && !(q == (2LL)) && !(q == (18LL)) && !(q == (36LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && p == (1LL) && q == (22LL)) || (!(q == (49LL)) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(q == (19LL)) && !(q == (34LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && !(q == (22LL)) && p == (1LL) && q == (35LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (14LL)))) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (6LL)))) && !(q == (44LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && !(q == (16LL)) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(p == (8LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (20LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (8LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (26LL)))) && !(p == (1LL)) && !(q == (40LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (18LL)))) && p == (4LL) && q == (24LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (5LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (3LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (48LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (26LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (6LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (31LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (21LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (14LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (14LL)))) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (6LL)))) && !(q == (44LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (19LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (34LL)))) && !(q == (16LL)) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (36LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (17LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (23LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (27LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (8LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (33LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (20LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (8LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (32LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (26LL)))) && !(q == (40LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (18LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (22LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (35LL)))) && !(q == (24LL)) && p == (4LL) && q == (12LL)) || (!(q == (22LL)) && !(q == (38LL)) && !(q == (50LL)) && !(p == (1LL)) && !(q == (16LL)) && !(q == (14LL)) && !(q == (6LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(q == (0LL)) && !(q == (42LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (24LL)))) && !(q == (20LL)) && !(q == (8LL)) && !(q == (26LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && !(q == (18LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (12LL)))) && p == (2LL) && q == (48LL)) || (!(q == (22LL)) && !(q == (38LL)) && !(q == (50LL)) && !(q == (16LL)) && !(q == (14LL)) && !(q == (6LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(q == (0LL)) && !(q == (42LL)) && !(p == (1LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (24LL)))) && !(q == (20LL)) && !(q == (8LL)) && !(q == (26LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && !(q == (18LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (12LL)))) && !(q == (48LL)) && p == (2LL) && q == (36LL)) || (!(q == (49LL)) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && !(q == (22LL)) && !(q == (35LL)) && !(p == (4LL)) && p == (1LL) && q == (12LL)) || (!(q == (22LL)) && !(q == (38LL)) && !(q == (50LL)) && !(q == (16LL)) && !(q == (14LL)) && !(q == (6LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(q == (0LL)) && !(q == (42LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (24LL)))) && !(q == (20LL)) && !(q == (8LL)) && !(p == (1LL)) && !(q == (26LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && !(q == (18LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (12LL)))) && !(q == (48LL)) && !(q == (36LL)) && p == (2LL) && q == (32LL)) || (!(p == (1LL)) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && !(q == (44LL)) && !(q == (16LL)) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && !(q == (40LL)) && !(q == (24LL)) && !(q == (12LL)) && !(p == (2LL)) && p == (4LL) && q == (48LL)) || ((!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && !(q == (44LL)) && !(q == (16LL)) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && !(p == (1LL)) && !(p == (2LL)) && !(q == (40LL)) && !(q == (24LL)) && !(q == (12LL)) && !(q == (48LL)) && p == (4LL) && q == (8LL)) || (!(q == (49LL)) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(p == (4LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && p == (1LL) && q == (44LL)) || (!(p == (1LL)) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && !(q == (44LL)) && !(q == (16LL)) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && !(p == (2LL)) && !(q == (40LL)) && !(q == (24LL)) && !(q == (12LL)) && !(q == (48LL)) && !(q == (8LL)) && p == (4LL) && q == (20LL)) || (!(q == (49LL)) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && p == (1LL) && q == (47LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (5LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (3LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (48LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (26LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (6LL)))) && !(p == (2LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (31LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (21LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (14LL)))) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (19LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (34LL)))) && !(p == (4LL)) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (36LL)))) && !(p == (16LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (17LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (23LL)))) && !(q == (24LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (27LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (8LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (33LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (32LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (22LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (35LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (12LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (44LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (47LL)))) && p == (8LL) && q == (16LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && !(q == (22LL)) && !(q == (38LL)) && !(q == (50LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (5LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (3LL)))) && !(q == (16LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (31LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (21LL)))) && !(q == (14LL)) && !(q == (6LL)) && !(q == (0LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (19LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (34LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && !(q == (42LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (17LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (23LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (24LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (27LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (33LL)))) && !(q == (20LL)) && !(q == (8LL)) && !(q == (26LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (24LL)))) && !(p == (4LL)) && !(q == (18LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (35LL)))) && !(q == (48LL)) && !(q == (36LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (12LL)))) && !(q == (32LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (44LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (47LL)))) && p == (2LL) && q == (40LL)) || (!(p == (1LL)) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && !(q == (24LL)) && !(p == (2LL)) && !(p == (4LL)) && !(q == (16LL)) && p == (8LL) && q == (48LL)) || (!(q == (49LL)) && !(q == (20LL)) && !(p == (2LL)) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && !(q == (2LL)) && !(q == (18LL)) && !(q == (36LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && p == (1LL) && q == (50LL)) || (!(q == (49LL)) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && !(q == (50LL)) && p == (1LL) && q == (45LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (5LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (3LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (26LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (6LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (31LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (21LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (14LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (14LL)))) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (6LL)))) && !(q == (44LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (19LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (34LL)))) && !(q == (16LL)) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (36LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (17LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (23LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (27LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (33LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (32LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (26LL)))) && !(q == (40LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (18LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (22LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (35LL)))) && !(q == (24LL)) && !(q == (12LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (36LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (32LL)))) && !(q == (48LL)) && !(q == (8LL)) && !(q == (20LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (47LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (50LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (45LL)))) && p == (4LL) && q == (28LL)) || (!(q == (49LL)) && !(q == (20LL)) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(p == (2LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(p == (4LL)) && !(q == (2LL)) && !(q == (18LL)) && !(q == (36LL)) && !(p == (16LL)) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && !(p == (8LL)) && !(q == (50LL)) && !(q == (45LL)) && p == (1LL) && q == (16LL)) || (!(p == (64LL)) && !(q == (44LL)) && !(p == (2LL)) && !(q == (16LL)) && !(p == (32LL)) && !(p == (1LL)) && !(q == (40LL)) && !(q == (24LL)) && !(q == (12LL)) && !(q == (48LL)) && !(q == (8LL)) && !(q == (20LL)) && !(q == (28LL)) && p == (4LL) && q == (0LL)) || (!(q == (49LL)) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && !(q == (50LL)) && !(q == (45LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && !(q == (16LL)) && p == (1LL) && q == (4LL)) || (!(q == (49LL)) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && !(q == (50LL)) && !(q == (45LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && !(q == (16LL)) && !(q == (4LL)) && p == (1LL) && q == (41LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && !(q == (22LL)) && !(q == (38LL)) && !(q == (50LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (5LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (3LL)))) && !(q == (16LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (31LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (21LL)))) && !(q == (14LL)) && !(q == (6LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(q == (0LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (19LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (34LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && !(q == (42LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (17LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (23LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (24LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (27LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (33LL)))) && !(q == (20LL)) && !(q == (8LL)) && !(q == (26LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (24LL)))) && !(q == (18LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (35LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (12LL)))) && !(q == (48LL)) && !(q == (36LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (12LL)))) && !(q == (32LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (44LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (47LL)))) && !(q == (40LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (45LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (4LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (41LL)))) && p == (2LL) && q == (46LL)) || (!(q == (49LL)) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && !(q == (50LL)) && !(q == (45LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && !(q == (16LL)) && !(q == (4LL)) && !(q == (41LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (46LL)))) && p == (1LL) && q == (43LL)) || (!(p == (1LL)) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && !(q == (16LL)) && !(p == (2LL)) && !(p == (4LL)) && !(p == (8LL)) && p == (16LL) && q == (48LL)) || (!(q == (22LL)) && !(q == (38LL)) && !(q == (50LL)) && !(q == (16LL)) && !(q == (14LL)) && !(q == (6LL)) && !(q == (0LL)) && !(q == (42LL)) && !(p == (8LL)) && !(q == (20LL)) && !(q == (8LL)) && !(q == (26LL)) && !(p == (1LL)) && !(q == (18LL)) && !(p == (4LL)) && !(q == (48LL)) && !(q == (36LL)) && !(q == (32LL)) && !(q == (40LL)) && !(q == (46LL)) && p == (2LL) && q == (24LL)) || (!(q == (22LL)) && !(q == (38LL)) && !(q == (50LL)) && !(q == (16LL)) && !(q == (14LL)) && !(q == (6LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(q == (0LL)) && !(p == (1LL)) && !(q == (42LL)) && !(q == (20LL)) && !(q == (8LL)) && !(q == (26LL)) && !(q == (18LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (12LL)))) && !(q == (48LL)) && !(q == (36LL)) && !(q == (32LL)) && !(q == (40LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && !(q == (46LL)) && !(q == (24LL)) && p == (2LL) && q == (2LL)) || ((!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && !(q == (24LL)) && !(p == (1LL)) && !(p == (2LL)) && !(p == (4LL)) && !(q == (16LL)) && !(q == (48LL)) && p == (8LL) && q == (8LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (22LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (50LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (14LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (6LL)))) && !(q == (44LL)) && !(q == (16LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (26LL)))) && !(q == (40LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (18LL)))) && !(q == (24LL)) && !(q == (12LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (36LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (32LL)))) && !(q == (48LL)) && !(q == (8LL)) && !(q == (20LL)) && !(q == (28LL)) && !(q == (0LL)) && !(p == (1LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (46LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (2LL)))) && p == (4LL) && q == (4LL)) || (!(q == (44LL)) && !(q == (16LL)) && !(p == (1LL)) && !(q == (40LL)) && !(q == (24LL)) && !(q == (12LL)) && !(p == (2LL)) && !(q == (48LL)) && !(q == (8LL)) && !(q == (20LL)) && !(q == (28LL)) && !(q == (0LL)) && !(q == (4LL)) && p == (4LL) && q == (36LL)) || (!(q == (49LL)) && !(q == (20LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (38LL)))) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && !(q == (50LL)) && !(q == (45LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && !(q == (16LL)) && !(q == (4LL)) && !(q == (41LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (46LL)))) && !(q == (43LL)) && p == (1LL) && q == (11LL)) || ((!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && !(q == (0LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (24LL)))) && !(p == (1LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (12LL)))) && !(p == (2LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (48LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (8LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (20LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (48LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (48LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (8LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (4LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (36LL)))) && p == (32LL) && q == (32LL)) || (!(q == (22LL)) && !(q == (38LL)) && !(q == (50LL)) && !(q == (16LL)) && !(p == (1LL)) && !(q == (14LL)) && !(q == (6LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(q == (0LL)) && !(q == (42LL)) && !(q == (20LL)) && !(q == (8LL)) && !(q == (26LL)) && !(q == (18LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (12LL)))) && !(q == (48LL)) && !(q == (36LL)) && !(q == (32LL)) && !(q == (40LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && !(q == (46LL)) && !(q == (24LL)) && !(q == (2LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (4LL)))) && p == (2LL) && q == (10LL)) || (!(q == (49LL)) && !(q == (20LL)) && !(p == (2LL)) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && !(q == (36LL)) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && !(q == (50LL)) && !(q == (45LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && !(q == (16LL)) && !(q == (4LL)) && !(q == (41LL)) && !(q == (43LL)) && !(q == (11LL)) && p == (1LL) && q == (38LL)) || (!(q == (49LL)) && !(q == (20LL)) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && !(q == (50LL)) && !(q == (45LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && !(q == (16LL)) && !(q == (4LL)) && !(q == (41LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (46LL)))) && !(q == (43LL)) && !(q == (11LL)) && !(q == (38LL)) && p == (1LL) && q == (30LL)) || (!(q == (49LL)) && !(q == (20LL)) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && !(q == (50LL)) && !(q == (45LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && !(q == (16LL)) && !(q == (4LL)) && !(q == (41LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (46LL)))) && !(q == (43LL)) && !(q == (11LL)) && !(q == (38LL)) && !(q == (30LL)) && p == (1LL) && q == (29LL)) || (!(q == (22LL)) && !(q == (38LL)) && !(q == (50LL)) && !(q == (16LL)) && !(q == (14LL)) && !(q == (6LL)) && !(q == (0LL)) && !(q == (42LL)) && !(q == (20LL)) && !(q == (8LL)) && !(q == (26LL)) && !(q == (18LL)) && !(p == (4LL)) && !(q == (48LL)) && !(q == (36LL)) && !(p == (1LL)) && !(q == (32LL)) && !(q == (40LL)) && !(q == (46LL)) && !(q == (24LL)) && !(q == (2LL)) && !(q == (10LL)) && p == (2LL) && q == (12LL)) || (!(q == (22LL)) && !(q == (38LL)) && !(q == (50LL)) && !(q == (16LL)) && !(q == (14LL)) && !(q == (6LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(q == (0LL)) && !(q == (42LL)) && !(q == (20LL)) && !(q == (8LL)) && !(q == (26LL)) && !(q == (18LL)) && !(q == (48LL)) && !(q == (36LL)) && !(q == (32LL)) && !(q == (40LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && !(q == (46LL)) && !(q == (24LL)) && !(q == (2LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (4LL)))) && !(q == (10LL)) && !(p == (1LL)) && !(q == (12LL)) && p == (2LL) && q == (30LL)) || (!(q == (22LL)) && !(q == (38LL)) && !(q == (50LL)) && !(q == (16LL)) && !(q == (14LL)) && !(q == (6LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(q == (0LL)) && !(p == (1LL)) && !(q == (42LL)) && !(q == (20LL)) && !(q == (8LL)) && !(q == (26LL)) && !(q == (18LL)) && !(q == (48LL)) && !(q == (36LL)) && !(q == (32LL)) && !(q == (40LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && !(q == (46LL)) && !(q == (24LL)) && !(q == (2LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (4LL)))) && !(q == (10LL)) && !(q == (12LL)) && !(q == (30LL)) && p == (2LL) && q == (34LL)) || ((!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(q == (24LL)) && !(p == (1LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (12LL)))) && !(p == (2LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (20LL)))) && !(q == (16LL)) && !(q == (48LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && !(q == (8LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (4LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (36LL)))) && !(p == (32LL)) && p == (8LL) && q == (32LL)) || (!(q == (49LL)) && !(q == (20LL)) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && !(q == (50LL)) && !(q == (45LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && !(q == (16LL)) && !(q == (4LL)) && !(q == (41LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (46LL)))) && !(q == (43LL)) && !(q == (11LL)) && !(q == (38LL)) && !(q == (30LL)) && !(q == (29LL)) && p == (1LL) && q == (25LL)) || (!(q == (49LL)) && !(q == (20LL)) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && !(q == (36LL)) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && !(q == (50LL)) && !(q == (45LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && !(q == (16LL)) && !(q == (4LL)) && !(q == (41LL)) && !(p == (2LL)) && !(q == (43LL)) && !(q == (11LL)) && !(q == (38LL)) && !(q == (30LL)) && !(q == (29LL)) && !(q == (25LL)) && p == (1LL) && q == (46LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && !(q == (22LL)) && !(q == (38LL)) && !(q == (50LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (5LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (3LL)))) && !(q == (16LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (31LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (21LL)))) && !(q == (14LL)) && !(q == (6LL)) && !(q == (0LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (19LL)))) && !(q == (42LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (17LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (23LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (27LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (33LL)))) && !(q == (20LL)) && !(q == (8LL)) && !(q == (26LL)) && !(q == (18LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (35LL)))) && !(q == (48LL)) && !(q == (36LL)) && !(q == (32LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (44LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (47LL)))) && !(q == (40LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (45LL)))) && !(p == (4LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (4LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (41LL)))) && !(q == (46LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (43LL)))) && !(q == (24LL)) && !(q == (2LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (11LL)))) && !(q == (10LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (29LL)))) && !(q == (12LL)) && !(q == (30LL)) && !(q == (34LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (25LL)))) && p == (2LL) && q == (28LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (49LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (5LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (3LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (26LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (6LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (31LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (21LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (14LL)))) && (!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (19LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (34LL)))) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (36LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (17LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (23LL)))) && !(q == (24LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (27LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (33LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (0LL)))) && !(p == (4LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (22LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (35LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (12LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (44LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (47LL)))) && !(q == (16LL)) && !(p == (2LL)) && !(q == (48LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (50LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (45LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (4LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (41LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (43LL)))) && !(q == (8LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (11LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (38LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (30LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (29LL)))) && !(q == (32LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (25LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (46LL)))) && p == (8LL) && q == (40LL)) || ((!(p == (64LL)) || (p == (64LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (44LL)))) && !(q == (16LL)) && !(p == (1LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (40LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (12LL)))) && !(p == (2LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (8LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (20LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && !(q == (48LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (4LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (36LL)))) && !(p == (32LL)) && !(p == (8LL)) && p == (16LL) && q == (32LL)) || (!(q == (49LL)) && !(q == (20LL)) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && !(q == (36LL)) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && !(p == (4LL)) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && !(p == (2LL)) && !(q == (50LL)) && !(q == (45LL)) && !(q == (16LL)) && !(q == (4LL)) && !(q == (41LL)) && !(q == (43LL)) && !(q == (11LL)) && !(q == (38LL)) && !(q == (30LL)) && !(q == (29LL)) && !(q == (25LL)) && !(q == (46LL)) && !(p == (8LL)) && p == (1LL) && q == (40LL)) || (!(p == (64LL)) && !(p == (2LL)) && !(p == (32LL)) && !(q == (24LL)) && !(p == (1LL)) && !(q == (16LL)) && !(q == (48LL)) && !(p == (4LL)) && !(q == (8LL)) && !(q == (32LL)) && !(q == (40LL)) && p == (8LL) && q == (0LL)) || (!(q == (49LL)) && !(q == (20LL)) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && !(q == (50LL)) && !(q == (45LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && !(q == (16LL)) && !(q == (4LL)) && !(q == (41LL)) && !(q == (43LL)) && !(q == (11LL)) && !(q == (38LL)) && !(q == (30LL)) && !(q == (29LL)) && !(q == (25LL)) && !(q == (46LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && !(q == (40LL)) && p == (1LL) && q == (13LL)) || (!(q == (49LL)) && !(q == (20LL)) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && !(q == (50LL)) && !(q == (45LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && !(q == (16LL)) && !(q == (4LL)) && !(q == (41LL)) && !(q == (43LL)) && !(q == (11LL)) && !(q == (38LL)) && !(q == (30LL)) && !(q == (29LL)) && !(q == (25LL)) && !(q == (46LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && !(q == (40LL)) && !(q == (13LL)) && p == (1LL) && q == (7LL)) || (!(q == (49LL)) && !(q == (20LL)) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (42LL)))) && !(q == (36LL)) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && !(q == (50LL)) && !(q == (45LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && !(q == (16LL)) && !(q == (4LL)) && !(q == (41LL)) && !(q == (43LL)) && !(q == (11LL)) && !(q == (38LL)) && !(q == (30LL)) && !(q == (29LL)) && !(q == (25LL)) && !(q == (46LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && !(q == (40LL)) && !(q == (13LL)) && !(q == (7LL)) && p == (1LL) && q == (15LL)) || (!(q == (49LL)) && !(q == (20LL)) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && !(p == (2LL)) && !(q == (36LL)) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && !(q == (50LL)) && !(q == (45LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && !(q == (16LL)) && !(q == (4LL)) && !(q == (41LL)) && !(q == (43LL)) && !(q == (11LL)) && !(q == (38LL)) && !(q == (30LL)) && !(q == (29LL)) && !(q == (25LL)) && !(q == (46LL)) && !(q == (40LL)) && !(q == (13LL)) && !(q == (7LL)) && !(q == (15LL)) && p == (1LL) && q == (42LL)) || (!(q == (49LL)) && !(q == (20LL)) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && !(q == (36LL)) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && !(q == (50LL)) && !(q == (45LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && !(q == (16LL)) && !(q == (4LL)) && !(q == (41LL)) && !(q == (43LL)) && !(q == (11LL)) && !(q == (38LL)) && !(q == (30LL)) && !(q == (29LL)) && !(q == (25LL)) && !(q == (46LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && !(q == (40LL)) && !(q == (13LL)) && !(q == (7LL)) && !(q == (15LL)) && !(q == (42LL)) && p == (1LL) && q == (37LL)) || (!(q == (49LL)) && !(q == (20LL)) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && !(q == (36LL)) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && !(q == (50LL)) && !(q == (45LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (28LL)))) && !(q == (16LL)) && !(q == (4LL)) && !(q == (41LL)) && !(q == (43LL)) && !(q == (11LL)) && !(q == (38LL)) && !(q == (30LL)) && !(q == (29LL)) && !(q == (25LL)) && !(q == (46LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && !(q == (40LL)) && !(q == (13LL)) && !(q == (7LL)) && !(q == (15LL)) && !(q == (42LL)) && !(q == (37LL)) && p == (1LL) && q == (1LL)) || (!(q == (49LL)) && !(q == (20LL)) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && !(q == (36LL)) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && !(q == (50LL)) && !(q == (45LL)) && !(p == (4LL)) && !(q == (16LL)) && !(q == (4LL)) && !(q == (41LL)) && !(q == (43LL)) && !(q == (11LL)) && !(q == (38LL)) && !(q == (30LL)) && !(q == (29LL)) && !(q == (25LL)) && !(q == (46LL)) && !(p == (2LL)) && !(q == (40LL)) && !(q == (13LL)) && !(q == (7LL)) && !(q == (15LL)) && !(q == (42LL)) && !(q == (37LL)) && !(q == (1LL)) && p == (1LL) && q == (28LL)) || (!(q == (22LL)) && !(q == (38LL)) && !(q == (50LL)) && !(q == (16LL)) && !(q == (14LL)) && !(q == (6LL)) && !(p == (4LL)) && !(q == (0LL)) && !(q == (42LL)) && !(q == (20LL)) && !(q == (8LL)) && !(q == (26LL)) && !(q == (18LL)) && !(q == (48LL)) && !(q == (36LL)) && !(q == (32LL)) && !(p == (1LL)) && !(q == (40LL)) && !(q == (46LL)) && !(q == (24LL)) && !(q == (2LL)) && !(q == (10LL)) && !(q == (12LL)) && !(q == (30LL)) && !(q == (34LL)) && !(q == (28LL)) && p == (2LL) && q == (44LL)) || (!(q == (49LL)) && !(q == (20LL)) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && !(q == (36LL)) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && !(q == (50LL)) && !(q == (45LL)) && !(q == (16LL)) && !(q == (4LL)) && !(q == (41LL)) && !(q == (43LL)) && !(q == (11LL)) && !(q == (38LL)) && !(q == (30LL)) && !(q == (29LL)) && !(q == (25LL)) && !(q == (46LL)) && !(q == (40LL)) && !(q == (13LL)) && !(q == (7LL)) && !(q == (15LL)) && !(q == (42LL)) && !(q == (37LL)) && !(q == (1LL)) && !(q == (28LL)) && p == (1LL) && q == (9LL)) || (!(q == (44LL)) && !(q == (16LL)) && !(p == (1LL)) && !(q == (40LL)) && !(q == (24LL)) && !(q == (12LL)) && !(p == (2LL)) && !(q == (48LL)) && !(q == (8LL)) && !(q == (20LL)) && !(q == (28LL)) && !(q == (0LL)) && !(q == (4LL)) && !(q == (36LL)) && !(p == (32LL)) && !(p == (8LL)) && !(p == (16LL)) && p == (4LL) && q == (32LL)) || (!(q == (22LL)) && !(q == (38LL)) && !(q == (50LL)) && !(q == (16LL)) && !(q == (14LL)) && !(q == (6LL)) && !(q == (0LL)) && !(q == (42LL)) && !(q == (20LL)) && !(q == (8LL)) && !(q == (26LL)) && !(q == (18LL)) && !(q == (48LL)) && !(q == (36LL)) && !(q == (32LL)) && !(q == (40LL)) && !(p == (1LL)) && !(q == (46LL)) && !(q == (24LL)) && !(q == (2LL)) && !(p == (4LL)) && !(q == (10LL)) && !(q == (12LL)) && !(q == (30LL)) && !(q == (34LL)) && !(q == (28LL)) && !(q == (44LL)) && p == (2LL) && q == (4LL)) || (!(q == (49LL)) && !(q == (20LL)) && !(q == (5LL)) && !(q == (3LL)) && !(q == (48LL)) && !(q == (26LL)) && !(q == (6LL)) && !(q == (31LL)) && !(q == (10LL)) && !(q == (21LL)) && !(q == (14LL)) && !(q == (19LL)) && !(q == (34LL)) && !(q == (2LL)) && !(q == (18LL)) && !(q == (36LL)) && !(q == (17LL)) && !(q == (23LL)) && !(q == (27LL)) && !(q == (8LL)) && !(q == (33LL)) && !(q == (0LL)) && !(q == (32LL)) && !(q == (24LL)) && !(q == (22LL)) && !(q == (35LL)) && !(q == (12LL)) && !(q == (44LL)) && !(q == (47LL)) && !(q == (50LL)) && !(q == (45LL)) && !(q == (16LL)) && !(q == (4LL)) && !(q == (41LL)) && !(q == (43LL)) && !(q == (11LL)) && !(q == (38LL)) && !(q == (30LL)) && !(q == (29LL)) && !(q == (25LL)) && !(q == (46LL)) && !(q == (40LL)) && !(q == (13LL)) && !(q == (7LL)) && !(q == (15LL)) && !(q == (42LL)) && !(q == (37LL)) && !(q == (1LL)) && !(q == (28LL)) && !(q == (9LL)) && p == (1LL) && q == (39LL)) || (!(p == (64LL)) && !(p == (2LL)) && !(p == (32LL)) && !(q == (16LL)) && !(p == (1LL)) && !(p == (4LL)) && !(q == (48LL)) && !(q == (32LL)) && !(p == (8LL)) && p == (16LL) && q == (0LL)) (../plain/hard-ll_valuebound50.c:48:9)
[Warning][Witness] couldn't locate invariant: p == (1LL) && (q == (31LL) || (!(q == (31LL)) && q == (5LL)) || (!(q == (31LL)) && !(q == (5LL)) && q == (42LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && q == (17LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && q == (35LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && q == (39LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && q == (27LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && q == (40LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && q == (15LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && q == (45LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && q == (6LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && q == (37LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && q == (46LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && q == (14LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && q == (36LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && q == (16LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && q == (25LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && q == (50LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && q == (23LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && q == (47LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && q == (1LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && q == (18LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && q == (28LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && q == (8LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && q == (10LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && q == (26LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && q == (9LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && q == (49LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && q == (22LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && q == (38LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && q == (0LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && !(q == (0LL)) && q == (30LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && !(q == (0LL)) && !(q == (30LL)) && q == (32LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && !(q == (0LL)) && !(q == (30LL)) && !(q == (32LL)) && q == (43LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && !(q == (0LL)) && !(q == (30LL)) && !(q == (32LL)) && !(q == (43LL)) && q == (3LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && !(q == (0LL)) && !(q == (30LL)) && !(q == (32LL)) && !(q == (43LL)) && !(q == (3LL)) && q == (24LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && !(q == (0LL)) && !(q == (30LL)) && !(q == (32LL)) && !(q == (43LL)) && !(q == (3LL)) && !(q == (24LL)) && q == (48LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && !(q == (0LL)) && !(q == (30LL)) && !(q == (32LL)) && !(q == (43LL)) && !(q == (3LL)) && !(q == (24LL)) && !(q == (48LL)) && q == (20LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && !(q == (0LL)) && !(q == (30LL)) && !(q == (32LL)) && !(q == (43LL)) && !(q == (3LL)) && !(q == (24LL)) && !(q == (48LL)) && !(q == (20LL)) && q == (34LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && !(q == (0LL)) && !(q == (30LL)) && !(q == (32LL)) && !(q == (43LL)) && !(q == (3LL)) && !(q == (24LL)) && !(q == (48LL)) && !(q == (20LL)) && !(q == (34LL)) && q == (4LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && !(q == (0LL)) && !(q == (30LL)) && !(q == (32LL)) && !(q == (43LL)) && !(q == (3LL)) && !(q == (24LL)) && !(q == (48LL)) && !(q == (20LL)) && !(q == (34LL)) && !(q == (4LL)) && q == (44LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && !(q == (0LL)) && !(q == (30LL)) && !(q == (32LL)) && !(q == (43LL)) && !(q == (3LL)) && !(q == (24LL)) && !(q == (48LL)) && !(q == (20LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (44LL)) && q == (7LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && !(q == (0LL)) && !(q == (30LL)) && !(q == (32LL)) && !(q == (43LL)) && !(q == (3LL)) && !(q == (24LL)) && !(q == (48LL)) && !(q == (20LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (44LL)) && !(q == (7LL)) && q == (2LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && !(q == (0LL)) && !(q == (30LL)) && !(q == (32LL)) && !(q == (43LL)) && !(q == (3LL)) && !(q == (24LL)) && !(q == (48LL)) && !(q == (20LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (44LL)) && !(q == (7LL)) && !(q == (2LL)) && q == (21LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && !(q == (0LL)) && !(q == (30LL)) && !(q == (32LL)) && !(q == (43LL)) && !(q == (3LL)) && !(q == (24LL)) && !(q == (48LL)) && !(q == (20LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (44LL)) && !(q == (7LL)) && !(q == (2LL)) && !(q == (21LL)) && q == (19LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && !(q == (0LL)) && !(q == (30LL)) && !(q == (32LL)) && !(q == (43LL)) && !(q == (3LL)) && !(q == (24LL)) && !(q == (48LL)) && !(q == (20LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (44LL)) && !(q == (7LL)) && !(q == (2LL)) && !(q == (21LL)) && !(q == (19LL)) && q == (29LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && !(q == (0LL)) && !(q == (30LL)) && !(q == (32LL)) && !(q == (43LL)) && !(q == (3LL)) && !(q == (24LL)) && !(q == (48LL)) && !(q == (20LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (44LL)) && !(q == (7LL)) && !(q == (2LL)) && !(q == (21LL)) && !(q == (19LL)) && !(q == (29LL)) && q == (12LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && !(q == (0LL)) && !(q == (30LL)) && !(q == (32LL)) && !(q == (43LL)) && !(q == (3LL)) && !(q == (24LL)) && !(q == (48LL)) && !(q == (20LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (44LL)) && !(q == (7LL)) && !(q == (2LL)) && !(q == (21LL)) && !(q == (19LL)) && !(q == (29LL)) && !(q == (12LL)) && q == (11LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && !(q == (0LL)) && !(q == (30LL)) && !(q == (32LL)) && !(q == (43LL)) && !(q == (3LL)) && !(q == (24LL)) && !(q == (48LL)) && !(q == (20LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (44LL)) && !(q == (7LL)) && !(q == (2LL)) && !(q == (21LL)) && !(q == (19LL)) && !(q == (29LL)) && !(q == (12LL)) && !(q == (11LL)) && q == (41LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && !(q == (0LL)) && !(q == (30LL)) && !(q == (32LL)) && !(q == (43LL)) && !(q == (3LL)) && !(q == (24LL)) && !(q == (48LL)) && !(q == (20LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (44LL)) && !(q == (7LL)) && !(q == (2LL)) && !(q == (21LL)) && !(q == (19LL)) && !(q == (29LL)) && !(q == (12LL)) && !(q == (11LL)) && !(q == (41LL)) && q == (13LL)) || (!(q == (31LL)) && !(q == (5LL)) && !(q == (42LL)) && !(q == (17LL)) && !(q == (35LL)) && !(q == (39LL)) && !(q == (27LL)) && !(q == (40LL)) && !(q == (15LL)) && !(q == (45LL)) && !(q == (6LL)) && !(q == (37LL)) && !(q == (46LL)) && !(q == (14LL)) && !(q == (36LL)) && !(q == (16LL)) && !(q == (25LL)) && !(q == (50LL)) && !(q == (23LL)) && !(q == (47LL)) && !(q == (1LL)) && !(q == (18LL)) && !(q == (28LL)) && !(q == (8LL)) && !(q == (10LL)) && !(q == (26LL)) && !(q == (9LL)) && !(q == (49LL)) && !(q == (22LL)) && !(q == (38LL)) && !(q == (0LL)) && !(q == (30LL)) && !(q == (32LL)) && !(q == (43LL)) && !(q == (3LL)) && !(q == (24LL)) && !(q == (48LL)) && !(q == (20LL)) && !(q == (34LL)) && !(q == (4LL)) && !(q == (44LL)) && !(q == (7LL)) && !(q == (2LL)) && !(q == (21LL)) && !(q == (19LL)) && !(q == (29LL)) && !(q == (12LL)) && !(q == (11LL)) && !(q == (41LL)) && !(q == (13LL)) && q == (33LL))) (../plain/hard-ll_valuebound50.c:50:24)
[Warning][Witness] couldn't locate invariant: (p == (1LL) && q == (2LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && p == (8LL) && q == (32LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && p == (4LL) && q == (0LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && !(q == (32LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && p == (8LL) && q == (48LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (48LL)))) && p == (2LL) && q == (28LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (48LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && p == (1LL) && q == (36LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && !(p == (8LL)) && !(q == (28LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (36LL)))) && p == (2LL) && q == (48LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (48LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && !(q == (36LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (48LL)))) && p == (1LL) && q == (46LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (48LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && !(q == (36LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (48LL)))) && !(q == (46LL)) && p == (1LL) && q == (44LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && !(p == (4LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (48LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (36LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (48LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (46LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (44LL)))) && p == (16LL) && q == (0LL)) || ((!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && !(q == (28LL)) && !(q == (48LL)) && !(p == (1LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && p == (2LL) && q == (44LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && !(q == (0LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (48LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (36LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (48LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (46LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (44LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (44LL)))) && p == (4LL) && q == (24LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && !(q == (28LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (36LL)))) && !(q == (48LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (46LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && !(q == (44LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && p == (2LL) && q == (40LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && !(q == (32LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && !(q == (48LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (36LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (46LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (44LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (44LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && p == (8LL) && q == (16LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && !(p == (8LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (36LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (48LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (46LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (44LL)))) && !(q == (0LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (44LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && p == (16LL) && q == (32LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (48LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && !(q == (36LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (48LL)))) && !(q == (46LL)) && !(q == (44LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && p == (1LL) && q == (34LL)) || (!(q == (2LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && !(q == (36LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (48LL)))) && !(q == (46LL)) && !(q == (44LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && !(p == (8LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(q == (34LL)) && p == (1LL) && q == (16LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (48LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && !(q == (36LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (48LL)))) && !(q == (46LL)) && !(q == (44LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(q == (34LL)) && !(q == (16LL)) && p == (1LL) && q == (10LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (48LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && !(q == (36LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (48LL)))) && !(q == (46LL)) && !(q == (44LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(q == (34LL)) && !(q == (16LL)) && !(q == (10LL)) && p == (1LL) && q == (50LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (48LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && !(q == (36LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (48LL)))) && !(q == (46LL)) && !(q == (44LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(q == (34LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (50LL)) && p == (1LL) && q == (20LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (48LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && !(q == (36LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (48LL)))) && !(q == (46LL)) && !(q == (44LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(q == (34LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (50LL)) && !(q == (20LL)) && p == (1LL) && q == (8LL)) || ((!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && !(q == (28LL)) && !(p == (1LL)) && !(q == (48LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && !(q == (44LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && !(q == (40LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && p == (2LL) && q == (36LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && !(q == (28LL)) && !(q == (48LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (46LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && !(q == (44LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && !(q == (40LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (34LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (16LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (50LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (8LL)))) && !(q == (36LL)) && p == (2LL) && q == (12LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (48LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && !(q == (36LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (48LL)))) && !(q == (46LL)) && !(q == (44LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(q == (34LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (50LL)) && !(q == (20LL)) && !(q == (8LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (12LL)))) && p == (1LL) && q == (18LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (48LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && !(q == (36LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (48LL)))) && !(q == (46LL)) && !(q == (44LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && !(p == (4LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(q == (34LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (50LL)) && !(q == (20LL)) && !(q == (8LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (12LL)))) && !(q == (18LL)) && p == (1LL) && q == (24LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && !(p == (4LL)) && !(q == (28LL)) && !(q == (48LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (46LL)))) && !(p == (16LL)) && !(q == (44LL)) && !(q == (40LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (34LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (16LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (50LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (8LL)))) && !(q == (36LL)) && !(q == (12LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (24LL)))) && p == (2LL) && q == (0LL)) || ((!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && !(q == (28LL)) && !(q == (48LL)) && !(q == (44LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && !(q == (40LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(p == (1LL)) && !(q == (36LL)) && !(q == (12LL)) && !(q == (0LL)) && p == (2LL) && q == (8LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && !(p == (8LL)) && !(q == (28LL)) && !(q == (48LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (46LL)))) && !(q == (44LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && !(q == (40LL)) && !(p == (16LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (34LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (16LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (50LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && !(q == (36LL)) && !(q == (12LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (24LL)))) && !(q == (0LL)) && !(q == (8LL)) && p == (2LL) && q == (32LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (48LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && !(q == (36LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (48LL)))) && !(q == (46LL)) && !(q == (44LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(q == (34LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (50LL)) && !(q == (20LL)) && !(q == (8LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (12LL)))) && !(q == (18LL)) && !(q == (24LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (32LL)))) && p == (1LL) && q == (14LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (48LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && !(q == (36LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (48LL)))) && !(q == (46LL)) && !(q == (44LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(q == (34LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (50LL)) && !(q == (20LL)) && !(q == (8LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (12LL)))) && !(q == (18LL)) && !(q == (24LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (32LL)))) && !(q == (14LL)) && p == (1LL) && q == (30LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && !(q == (32LL)) && !(p == (4LL)) && !(q == (48LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (36LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (46LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (44LL)))) && !(p == (16LL)) && !(q == (16LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (34LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (50LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (8LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (24LL)))) && !(p == (2LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (14LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (30LL)))) && p == (8LL) && q == (0LL)) || (!(q == (28LL)) && !(q == (48LL)) && !(q == (44LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && !(q == (40LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && !(p == (1LL)) && !(q == (36LL)) && !(q == (12LL)) && !(q == (0LL)) && !(q == (8LL)) && !(q == (32LL)) && p == (2LL) && q == (20LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (48LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && !(q == (36LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (48LL)))) && !(q == (46LL)) && !(q == (44LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(q == (34LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (50LL)) && !(q == (20LL)) && !(q == (8LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (12LL)))) && !(q == (18LL)) && !(q == (24LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (32LL)))) && !(q == (14LL)) && !(q == (30LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (0LL)))) && p == (1LL) && q == (22LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (48LL)))) && !(p == (2LL)) && !(q == (36LL)) && !(q == (46LL)) && !(q == (44LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(q == (34LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (50LL)) && !(q == (20LL)) && !(q == (8LL)) && !(q == (18LL)) && !(q == (24LL)) && !(q == (14LL)) && !(q == (30LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (0LL)))) && !(q == (22LL)) && p == (1LL) && q == (28LL)) || (!(q == (2LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && !(p == (8LL)) && !(q == (36LL)) && !(p == (2LL)) && !(q == (46LL)) && !(q == (44LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(q == (34LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (50LL)) && !(q == (20LL)) && !(q == (8LL)) && !(q == (18LL)) && !(q == (24LL)) && !(q == (14LL)) && !(q == (30LL)) && !(q == (22LL)) && !(q == (28LL)) && p == (1LL) && q == (48LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && !(q == (36LL)) && !(q == (46LL)) && !(q == (44LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(q == (34LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (50LL)) && !(q == (20LL)) && !(q == (8LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (12LL)))) && !(q == (18LL)) && !(q == (24LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (32LL)))) && !(q == (14LL)) && !(q == (30LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (0LL)))) && !(q == (22LL)) && !(q == (28LL)) && !(q == (48LL)) && p == (1LL) && q == (4LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && !(q == (36LL)) && !(q == (46LL)) && !(q == (44LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && !(p == (2LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(q == (34LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (50LL)) && !(q == (20LL)) && !(q == (8LL)) && !(q == (18LL)) && !(q == (24LL)) && !(q == (14LL)) && !(q == (30LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (0LL)))) && !(q == (22LL)) && !(q == (28LL)) && !(q == (48LL)) && !(q == (4LL)) && p == (1LL) && q == (40LL)) || (!(q == (28LL)) && !(q == (48LL)) && !(q == (44LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (24LL)))) && !(q == (40LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && !(q == (36LL)) && !(q == (12LL)) && !(q == (0LL)) && !(q == (8LL)) && !(q == (32LL)) && !(q == (20LL)) && !(p == (1LL)) && p == (2LL) && q == (4LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && !(p == (4LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (36LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (46LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (44LL)))) && !(p == (16LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (34LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (16LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (50LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (8LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (24LL)))) && !(p == (2LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (14LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (30LL)))) && !(p == (8LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (22LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (28LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (48LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (4LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (40LL)))) && p == (32LL) && q == (0LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && !(q == (36LL)) && !(q == (46LL)) && !(q == (44LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(q == (34LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (50LL)) && !(q == (20LL)) && !(q == (8LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (12LL)))) && !(q == (18LL)) && !(q == (24LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (32LL)))) && !(q == (14LL)) && !(q == (30LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (0LL)))) && !(q == (22LL)) && !(q == (28LL)) && !(q == (48LL)) && !(q == (4LL)) && !(q == (40LL)) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && p == (1LL) && q == (26LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && !(q == (36LL)) && !(q == (46LL)) && !(q == (44LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(q == (34LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (50LL)) && !(q == (20LL)) && !(q == (8LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (12LL)))) && !(q == (18LL)) && !(q == (24LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (32LL)))) && !(q == (14LL)) && !(q == (30LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (0LL)))) && !(q == (22LL)) && !(q == (28LL)) && !(q == (48LL)) && !(q == (4LL)) && !(q == (40LL)) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && !(q == (26LL)) && p == (1LL) && q == (42LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (0LL)))) && !(q == (36LL)) && !(q == (46LL)) && !(q == (44LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(q == (34LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (50LL)) && !(q == (20LL)) && !(q == (8LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (12LL)))) && !(q == (18LL)) && !(q == (24LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (32LL)))) && !(q == (14LL)) && !(q == (30LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (0LL)))) && !(q == (22LL)) && !(q == (28LL)) && !(q == (48LL)) && !(q == (4LL)) && !(q == (40LL)) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && !(q == (26LL)) && !(q == (42LL)) && p == (1LL) && q == (6LL)) || (!(q == (0LL)) && !(p == (8LL)) && !(p == (2LL)) && !(q == (24LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(p == (1LL)) && p == (4LL) && q == (48LL)) || (!(q == (2LL)) && !(p == (4LL)) && !(q == (36LL)) && !(q == (46LL)) && !(q == (44LL)) && !(p == (16LL)) && !(q == (34LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (50LL)) && !(q == (20LL)) && !(q == (8LL)) && !(q == (18LL)) && !(q == (24LL)) && !(p == (2LL)) && !(q == (14LL)) && !(q == (30LL)) && !(p == (8LL)) && !(q == (22LL)) && !(q == (28LL)) && !(q == (48LL)) && !(q == (4LL)) && !(q == (40LL)) && !(p == (32LL)) && !(q == (26LL)) && !(q == (42LL)) && !(q == (6LL)) && p == (1LL) && q == (0LL)) || (!(q == (0LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (28LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (44LL)))) && !(q == (24LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (40LL)))) && !(p == (8LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(p == (1LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (36LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (12LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (8LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (32LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (20LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (4LL)))) && !(q == (48LL)) && p == (4LL) && q == (16LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (2LL)))) && !(p == (8LL)) && !(q == (0LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (36LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (46LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (44LL)))) && !(q == (24LL)) && !(p == (16LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (34LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (10LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (50LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (8LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && !(p == (2LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (14LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (30LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (22LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (28LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (4LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (40LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (26LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (42LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (6LL)))) && !(q == (48LL)) && !(q == (16LL)) && p == (4LL) && q == (32LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && !(q == (36LL)) && !(q == (46LL)) && !(q == (44LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(q == (34LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (50LL)) && !(q == (20LL)) && !(q == (8LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (12LL)))) && !(q == (18LL)) && !(q == (24LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (32LL)))) && !(q == (14LL)) && !(q == (30LL)) && !(q == (22LL)) && !(q == (28LL)) && !(q == (48LL)) && !(q == (4LL)) && !(q == (40LL)) && !(q == (26LL)) && !(q == (42LL)) && !(q == (6LL)) && !(q == (0LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (32LL)))) && p == (1LL) && q == (38LL)) || (!(q == (0LL)) && !(q == (24LL)) && !(p == (2LL)) && !(p == (1LL)) && !(q == (48LL)) && !(q == (16LL)) && !(q == (32LL)) && p == (4LL) && q == (40LL)) || (!(q == (2LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (32LL)))) && !(q == (36LL)) && !(q == (46LL)) && !(q == (44LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (32LL)))) && !(q == (34LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (50LL)) && !(q == (20LL)) && !(q == (8LL)) && !(p == (2LL)) && !(q == (18LL)) && !(q == (24LL)) && !(q == (14LL)) && !(q == (30LL)) && !(q == (22LL)) && !(q == (28LL)) && !(q == (48LL)) && !(q == (4LL)) && !(q == (40LL)) && !(q == (26LL)) && !(q == (42LL)) && !(q == (6LL)) && !(q == (0LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (32LL)))) && !(q == (38LL)) && p == (1LL) && q == (12LL)) || (!(q == (0LL)) && !(q == (24LL)) && !(p == (1LL)) && !(p == (2LL)) && !(q == (48LL)) && !(q == (16LL)) && !(q == (32LL)) && !(q == (40LL)) && p == (4LL) && q == (8LL)) || (!(q == (28LL)) && !(q == (48LL)) && !(q == (44LL)) && !(q == (40LL)) && !(p == (8LL)) && !(p == (1LL)) && !(q == (36LL)) && !(q == (12LL)) && !(q == (0LL)) && !(q == (8LL)) && !(q == (32LL)) && !(q == (20LL)) && !(q == (4LL)) && !(p == (4LL)) && p == (2LL) && q == (16LL)) || (!(q == (2LL)) && !(p == (8LL)) && !(q == (36LL)) && !(q == (46LL)) && !(q == (44LL)) && !(p == (16LL)) && !(q == (34LL)) && !(q == (16LL)) && !(q == (10LL)) && !(q == (50LL)) && !(q == (20LL)) && !(q == (8LL)) && !(q == (18LL)) && !(q == (24LL)) && !(p == (2LL)) && !(q == (14LL)) && !(q == (30LL)) && !(q == (22LL)) && !(q == (28LL)) && !(q == (48LL)) && !(q == (4LL)) && !(q == (40LL)) && !(q == (26LL)) && !(q == (42LL)) && !(q == (6LL)) && !(q == (0LL)) && !(p == (4LL)) && !(q == (38LL)) && !(q == (12LL)) && p == (1LL) && q == (32LL)) || (!(q == (28LL)) && !(q == (48LL)) && !(q == (44LL)) && !(p == (4LL)) && !(q == (40LL)) && !(q == (36LL)) && !(q == (12LL)) && !(p == (1LL)) && !(q == (0LL)) && !(q == (8LL)) && !(q == (32LL)) && !(q == (20LL)) && !(q == (4LL)) && !(q == (16LL)) && p == (2LL) && q == (24LL)) (../plain/hard-ll_valuebound50.c:52:9)

runtime: 00:00:10.146
vars: 111, evals: 210

|rho|=111
|called|=5
|stable|=111
|infl|=107
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=84
Found 14 contexts for 5 functions. Top 5 functions:
5	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll_valuebound50.c:14:1-20:1
3	contexts for entry state of reach_error (1999) on ../plain/hard-ll_valuebound50.c:8:1-8:73
3	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll_valuebound50.c:11:1-13:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
1	contexts for entry state of main (2012) on ../plain/hard-ll_valuebound50.c:22:1-63:1

Memory statistics: total=3123.74MB, max=87.53MB, minor=3119.70MB, major=417.56MB, promoted=413.51MB
    minor collections=1501  major collections=32 compactions=0


runtime: 00:00:20.161
vars: 111, evals: 274

|rho|=111
|called|=5
|stable|=110
|infl|=109
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=84
Found 14 contexts for 5 functions. Top 5 functions:
5	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll_valuebound50.c:14:1-20:1
3	contexts for entry state of reach_error (1999) on ../plain/hard-ll_valuebound50.c:8:1-8:73
3	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll_valuebound50.c:11:1-13:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
1	contexts for entry state of main (2012) on ../plain/hard-ll_valuebound50.c:22:1-63:1

Memory statistics: total=6303.55MB, max=87.53MB, minor=6299.18MB, major=857.99MB, promoted=853.62MB
    minor collections=3028  major collections=59 compactions=0


runtime: 00:00:30.185
vars: 111, evals: 327

|rho|=111
|called|=5
|stable|=110
|infl|=109
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=84
Found 14 contexts for 5 functions. Top 5 functions:
5	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll_valuebound50.c:14:1-20:1
3	contexts for entry state of reach_error (1999) on ../plain/hard-ll_valuebound50.c:8:1-8:73
3	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll_valuebound50.c:11:1-13:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
1	contexts for entry state of main (2012) on ../plain/hard-ll_valuebound50.c:22:1-63:1

Memory statistics: total=9229.82MB, max=87.53MB, minor=9225.16MB, major=1263.44MB, promoted=1258.78MB
    minor collections=4435  major collections=84 compactions=0


runtime: 00:00:40.203
vars: 111, evals: 380

|rho|=111
|called|=5
|stable|=110
|infl|=109
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=84
Found 14 contexts for 5 functions. Top 5 functions:
5	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll_valuebound50.c:14:1-20:1
3	contexts for entry state of reach_error (1999) on ../plain/hard-ll_valuebound50.c:8:1-8:73
3	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll_valuebound50.c:11:1-13:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
1	contexts for entry state of main (2012) on ../plain/hard-ll_valuebound50.c:22:1-63:1

Memory statistics: total=12147.72MB, max=87.53MB, minor=12142.76MB, major=1669.75MB, promoted=1664.79MB
    minor collections=5836  major collections=108 compactions=0


runtime: 00:00:50.216
vars: 111, evals: 434

|rho|=111
|called|=5
|stable|=102
|infl|=109
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=84
Found 14 contexts for 5 functions. Top 5 functions:
5	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll_valuebound50.c:14:1-20:1
3	contexts for entry state of reach_error (1999) on ../plain/hard-ll_valuebound50.c:8:1-8:73
3	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll_valuebound50.c:11:1-13:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
1	contexts for entry state of main (2012) on ../plain/hard-ll_valuebound50.c:22:1-63:1

Memory statistics: total=15349.87MB, max=87.53MB, minor=15344.58MB, major=2109.46MB, promoted=2104.18MB
    minor collections=7374  major collections=130 compactions=0


runtime: 00:01:00.232
vars: 111, evals: 487

|rho|=111
|called|=5
|stable|=102
|infl|=109
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=84
Found 14 contexts for 5 functions. Top 5 functions:
5	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll_valuebound50.c:14:1-20:1
3	contexts for entry state of reach_error (1999) on ../plain/hard-ll_valuebound50.c:8:1-8:73
3	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll_valuebound50.c:11:1-13:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
1	contexts for entry state of main (2012) on ../plain/hard-ll_valuebound50.c:22:1-63:1

Memory statistics: total=18274.18MB, max=87.53MB, minor=18268.60MB, major=2515.68MB, promoted=2510.10MB
    minor collections=8778  major collections=153 compactions=0

