/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 pesco/sqrt1-ll_unwindbound20.yml.witness.yml --witness.yaml.validate pesco/sqrt1-ll_unwindbound20.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/sqrt1-ll_unwindbound20.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: (counter == (17) && a == (16LL) && s == (289LL) && t == (33LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && counter == (21) && a == (20LL) && s == (441LL) && t == (41LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && counter == (15) && a == (14LL) && s == (225LL) && t == (29LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && counter == (2) && a == (1LL) && s == (4LL) && t == (3LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && counter == (18) && a == (17LL) && s == (324LL) && t == (35LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && counter == (3) && a == (2LL) && s == (9LL) && t == (5LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && counter == (11) && a == (10LL) && s == (121LL) && t == (21LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && counter == (4) && a == (3LL) && s == (16LL) && t == (7LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && counter == (14) && a == (13LL) && s == (196LL) && t == (27LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && counter == (20) && a == (19LL) && s == (400LL) && t == (39LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && counter == (9) && a == (8LL) && s == (81LL) && t == (17LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && counter == (13) && a == (12LL) && s == (169LL) && t == (25LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && counter == (16) && a == (15LL) && s == (256LL) && t == (31LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && counter == (19) && a == (18LL) && s == (361LL) && t == (37LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && counter == (5) && a == (4LL) && s == (25LL) && t == (9LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (5)) || (counter == (5) && !(a == (4LL))) || (counter == (5) && a == (4LL) && !(s == (25LL))) || (counter == (5) && a == (4LL) && s == (25LL) && !(t == (9LL)))) && counter == (6) && a == (5LL) && s == (36LL) && t == (11LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (5)) || (counter == (5) && !(a == (4LL))) || (counter == (5) && a == (4LL) && !(s == (25LL))) || (counter == (5) && a == (4LL) && s == (25LL) && !(t == (9LL)))) && (!(counter == (6)) || (counter == (6) && !(a == (5LL))) || (counter == (6) && a == (5LL) && !(s == (36LL))) || (counter == (6) && a == (5LL) && s == (36LL) && !(t == (11LL)))) && counter == (10) && a == (9LL) && s == (100LL) && t == (19LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (5)) || (counter == (5) && !(a == (4LL))) || (counter == (5) && a == (4LL) && !(s == (25LL))) || (counter == (5) && a == (4LL) && s == (25LL) && !(t == (9LL)))) && (!(counter == (6)) || (counter == (6) && !(a == (5LL))) || (counter == (6) && a == (5LL) && !(s == (36LL))) || (counter == (6) && a == (5LL) && s == (36LL) && !(t == (11LL)))) && (!(counter == (10)) || (counter == (10) && !(a == (9LL))) || (counter == (10) && a == (9LL) && !(s == (100LL))) || (counter == (10) && a == (9LL) && s == (100LL) && !(t == (19LL)))) && counter == (7) && a == (6LL) && s == (49LL) && t == (13LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (5)) || (counter == (5) && !(a == (4LL))) || (counter == (5) && a == (4LL) && !(s == (25LL))) || (counter == (5) && a == (4LL) && s == (25LL) && !(t == (9LL)))) && (!(counter == (6)) || (counter == (6) && !(a == (5LL))) || (counter == (6) && a == (5LL) && !(s == (36LL))) || (counter == (6) && a == (5LL) && s == (36LL) && !(t == (11LL)))) && (!(counter == (10)) || (counter == (10) && !(a == (9LL))) || (counter == (10) && a == (9LL) && !(s == (100LL))) || (counter == (10) && a == (9LL) && s == (100LL) && !(t == (19LL)))) && (!(counter == (7)) || (counter == (7) && !(a == (6LL))) || (counter == (7) && a == (6LL) && !(s == (49LL))) || (counter == (7) && a == (6LL) && s == (49LL) && !(t == (13LL)))) && counter == (1) && a == (0LL) && s == (1LL) && t == (1LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (5)) || (counter == (5) && !(a == (4LL))) || (counter == (5) && a == (4LL) && !(s == (25LL))) || (counter == (5) && a == (4LL) && s == (25LL) && !(t == (9LL)))) && (!(counter == (6)) || (counter == (6) && !(a == (5LL))) || (counter == (6) && a == (5LL) && !(s == (36LL))) || (counter == (6) && a == (5LL) && s == (36LL) && !(t == (11LL)))) && (!(counter == (10)) || (counter == (10) && !(a == (9LL))) || (counter == (10) && a == (9LL) && !(s == (100LL))) || (counter == (10) && a == (9LL) && s == (100LL) && !(t == (19LL)))) && (!(counter == (7)) || (counter == (7) && !(a == (6LL))) || (counter == (7) && a == (6LL) && !(s == (49LL))) || (counter == (7) && a == (6LL) && s == (49LL) && !(t == (13LL)))) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(s == (1LL))) || (counter == (1) && a == (0LL) && s == (1LL) && !(t == (1LL)))) && counter == (8) && a == (7LL) && s == (64LL) && t == (15LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (5)) || (counter == (5) && !(a == (4LL))) || (counter == (5) && a == (4LL) && !(s == (25LL))) || (counter == (5) && a == (4LL) && s == (25LL) && !(t == (9LL)))) && (!(counter == (6)) || (counter == (6) && !(a == (5LL))) || (counter == (6) && a == (5LL) && !(s == (36LL))) || (counter == (6) && a == (5LL) && s == (36LL) && !(t == (11LL)))) && (!(counter == (10)) || (counter == (10) && !(a == (9LL))) || (counter == (10) && a == (9LL) && !(s == (100LL))) || (counter == (10) && a == (9LL) && s == (100LL) && !(t == (19LL)))) && (!(counter == (7)) || (counter == (7) && !(a == (6LL))) || (counter == (7) && a == (6LL) && !(s == (49LL))) || (counter == (7) && a == (6LL) && s == (49LL) && !(t == (13LL)))) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(s == (1LL))) || (counter == (1) && a == (0LL) && s == (1LL) && !(t == (1LL)))) && (!(counter == (8)) || (counter == (8) && !(a == (7LL))) || (counter == (8) && a == (7LL) && !(s == (64LL))) || (counter == (8) && a == (7LL) && s == (64LL) && !(t == (15LL)))) && counter == (12) && a == (11LL) && s == (144LL) && t == (23LL)) (../plain/sqrt1-ll_unwindbound20.c:44:5)
[Warning][Witness] couldn't locate invariant: (counter == (17) && a == (16LL) && s == (289LL) && t == (33LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && counter == (21) && a == (20LL) && s == (441LL) && t == (41LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && counter == (15) && a == (14LL) && s == (225LL) && t == (29LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && counter == (2) && a == (1LL) && s == (4LL) && t == (3LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && counter == (18) && a == (17LL) && s == (324LL) && t == (35LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && counter == (3) && a == (2LL) && s == (9LL) && t == (5LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && counter == (11) && a == (10LL) && s == (121LL) && t == (21LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && counter == (4) && a == (3LL) && s == (16LL) && t == (7LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && counter == (14) && a == (13LL) && s == (196LL) && t == (27LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && counter == (20) && a == (19LL) && s == (400LL) && t == (39LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && counter == (9) && a == (8LL) && s == (81LL) && t == (17LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && counter == (13) && a == (12LL) && s == (169LL) && t == (25LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && counter == (16) && a == (15LL) && s == (256LL) && t == (31LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && counter == (19) && a == (18LL) && s == (361LL) && t == (37LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && counter == (5) && a == (4LL) && s == (25LL) && t == (9LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (5)) || (counter == (5) && !(a == (4LL))) || (counter == (5) && a == (4LL) && !(s == (25LL))) || (counter == (5) && a == (4LL) && s == (25LL) && !(t == (9LL)))) && counter == (6) && a == (5LL) && s == (36LL) && t == (11LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (5)) || (counter == (5) && !(a == (4LL))) || (counter == (5) && a == (4LL) && !(s == (25LL))) || (counter == (5) && a == (4LL) && s == (25LL) && !(t == (9LL)))) && (!(counter == (6)) || (counter == (6) && !(a == (5LL))) || (counter == (6) && a == (5LL) && !(s == (36LL))) || (counter == (6) && a == (5LL) && s == (36LL) && !(t == (11LL)))) && counter == (10) && a == (9LL) && s == (100LL) && t == (19LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (5)) || (counter == (5) && !(a == (4LL))) || (counter == (5) && a == (4LL) && !(s == (25LL))) || (counter == (5) && a == (4LL) && s == (25LL) && !(t == (9LL)))) && (!(counter == (6)) || (counter == (6) && !(a == (5LL))) || (counter == (6) && a == (5LL) && !(s == (36LL))) || (counter == (6) && a == (5LL) && s == (36LL) && !(t == (11LL)))) && (!(counter == (10)) || (counter == (10) && !(a == (9LL))) || (counter == (10) && a == (9LL) && !(s == (100LL))) || (counter == (10) && a == (9LL) && s == (100LL) && !(t == (19LL)))) && counter == (7) && a == (6LL) && s == (49LL) && t == (13LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (5)) || (counter == (5) && !(a == (4LL))) || (counter == (5) && a == (4LL) && !(s == (25LL))) || (counter == (5) && a == (4LL) && s == (25LL) && !(t == (9LL)))) && (!(counter == (6)) || (counter == (6) && !(a == (5LL))) || (counter == (6) && a == (5LL) && !(s == (36LL))) || (counter == (6) && a == (5LL) && s == (36LL) && !(t == (11LL)))) && (!(counter == (10)) || (counter == (10) && !(a == (9LL))) || (counter == (10) && a == (9LL) && !(s == (100LL))) || (counter == (10) && a == (9LL) && s == (100LL) && !(t == (19LL)))) && (!(counter == (7)) || (counter == (7) && !(a == (6LL))) || (counter == (7) && a == (6LL) && !(s == (49LL))) || (counter == (7) && a == (6LL) && s == (49LL) && !(t == (13LL)))) && counter == (1) && a == (0LL) && s == (1LL) && t == (1LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (5)) || (counter == (5) && !(a == (4LL))) || (counter == (5) && a == (4LL) && !(s == (25LL))) || (counter == (5) && a == (4LL) && s == (25LL) && !(t == (9LL)))) && (!(counter == (6)) || (counter == (6) && !(a == (5LL))) || (counter == (6) && a == (5LL) && !(s == (36LL))) || (counter == (6) && a == (5LL) && s == (36LL) && !(t == (11LL)))) && (!(counter == (10)) || (counter == (10) && !(a == (9LL))) || (counter == (10) && a == (9LL) && !(s == (100LL))) || (counter == (10) && a == (9LL) && s == (100LL) && !(t == (19LL)))) && (!(counter == (7)) || (counter == (7) && !(a == (6LL))) || (counter == (7) && a == (6LL) && !(s == (49LL))) || (counter == (7) && a == (6LL) && s == (49LL) && !(t == (13LL)))) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(s == (1LL))) || (counter == (1) && a == (0LL) && s == (1LL) && !(t == (1LL)))) && counter == (8) && a == (7LL) && s == (64LL) && t == (15LL)) || ((!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (21)) || (counter == (21) && !(a == (20LL))) || (counter == (21) && a == (20LL) && !(s == (441LL))) || (counter == (21) && a == (20LL) && s == (441LL) && !(t == (41LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (11)) || (counter == (11) && !(a == (10LL))) || (counter == (11) && a == (10LL) && !(s == (121LL))) || (counter == (11) && a == (10LL) && s == (121LL) && !(t == (21LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (5)) || (counter == (5) && !(a == (4LL))) || (counter == (5) && a == (4LL) && !(s == (25LL))) || (counter == (5) && a == (4LL) && s == (25LL) && !(t == (9LL)))) && (!(counter == (6)) || (counter == (6) && !(a == (5LL))) || (counter == (6) && a == (5LL) && !(s == (36LL))) || (counter == (6) && a == (5LL) && s == (36LL) && !(t == (11LL)))) && (!(counter == (10)) || (counter == (10) && !(a == (9LL))) || (counter == (10) && a == (9LL) && !(s == (100LL))) || (counter == (10) && a == (9LL) && s == (100LL) && !(t == (19LL)))) && (!(counter == (7)) || (counter == (7) && !(a == (6LL))) || (counter == (7) && a == (6LL) && !(s == (49LL))) || (counter == (7) && a == (6LL) && s == (49LL) && !(t == (13LL)))) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(s == (1LL))) || (counter == (1) && a == (0LL) && s == (1LL) && !(t == (1LL)))) && (!(counter == (8)) || (counter == (8) && !(a == (7LL))) || (counter == (8) && a == (7LL) && !(s == (64LL))) || (counter == (8) && a == (7LL) && s == (64LL) && !(t == (15LL)))) && counter == (12) && a == (11LL) && s == (144LL) && t == (23LL)) (../plain/sqrt1-ll_unwindbound20.c:37:13)
[Warning][Witness] couldn't locate invariant: (counter == (18) && a == (17LL) && s == (324LL) && t == (35LL)) || ((!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && counter == (17) && a == (16LL) && s == (289LL) && t == (33LL)) || ((!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && counter == (19) && a == (18LL) && s == (361LL) && t == (37LL)) || ((!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && counter == (20) && a == (19LL) && s == (400LL) && t == (39LL)) || ((!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && counter == (16) && a == (15LL) && s == (256LL) && t == (31LL)) || ((!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && counter == (2) && a == (1LL) && s == (4LL) && t == (3LL)) || ((!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && counter == (1) && a == (0LL) && s == (1LL) && t == (1LL)) || ((!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(s == (1LL))) || (counter == (1) && a == (0LL) && s == (1LL) && !(t == (1LL)))) && counter == (3) && a == (2LL) && s == (9LL) && t == (5LL)) || ((!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(s == (1LL))) || (counter == (1) && a == (0LL) && s == (1LL) && !(t == (1LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && counter == (15) && a == (14LL) && s == (225LL) && t == (29LL)) || ((!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(s == (1LL))) || (counter == (1) && a == (0LL) && s == (1LL) && !(t == (1LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && counter == (8) && a == (7LL) && s == (64LL) && t == (15LL)) || ((!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(s == (1LL))) || (counter == (1) && a == (0LL) && s == (1LL) && !(t == (1LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (8)) || (counter == (8) && !(a == (7LL))) || (counter == (8) && a == (7LL) && !(s == (64LL))) || (counter == (8) && a == (7LL) && s == (64LL) && !(t == (15LL)))) && counter == (4) && a == (3LL) && s == (16LL) && t == (7LL)) || ((!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(s == (1LL))) || (counter == (1) && a == (0LL) && s == (1LL) && !(t == (1LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (8)) || (counter == (8) && !(a == (7LL))) || (counter == (8) && a == (7LL) && !(s == (64LL))) || (counter == (8) && a == (7LL) && s == (64LL) && !(t == (15LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && counter == (14) && a == (13LL) && s == (196LL) && t == (27LL)) || ((!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(s == (1LL))) || (counter == (1) && a == (0LL) && s == (1LL) && !(t == (1LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (8)) || (counter == (8) && !(a == (7LL))) || (counter == (8) && a == (7LL) && !(s == (64LL))) || (counter == (8) && a == (7LL) && s == (64LL) && !(t == (15LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && counter == (12) && a == (11LL) && s == (144LL) && t == (23LL)) || ((!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(s == (1LL))) || (counter == (1) && a == (0LL) && s == (1LL) && !(t == (1LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (8)) || (counter == (8) && !(a == (7LL))) || (counter == (8) && a == (7LL) && !(s == (64LL))) || (counter == (8) && a == (7LL) && s == (64LL) && !(t == (15LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (12)) || (counter == (12) && !(a == (11LL))) || (counter == (12) && a == (11LL) && !(s == (144LL))) || (counter == (12) && a == (11LL) && s == (144LL) && !(t == (23LL)))) && counter == (6) && a == (5LL) && s == (36LL) && t == (11LL)) || ((!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(s == (1LL))) || (counter == (1) && a == (0LL) && s == (1LL) && !(t == (1LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (8)) || (counter == (8) && !(a == (7LL))) || (counter == (8) && a == (7LL) && !(s == (64LL))) || (counter == (8) && a == (7LL) && s == (64LL) && !(t == (15LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (12)) || (counter == (12) && !(a == (11LL))) || (counter == (12) && a == (11LL) && !(s == (144LL))) || (counter == (12) && a == (11LL) && s == (144LL) && !(t == (23LL)))) && (!(counter == (6)) || (counter == (6) && !(a == (5LL))) || (counter == (6) && a == (5LL) && !(s == (36LL))) || (counter == (6) && a == (5LL) && s == (36LL) && !(t == (11LL)))) && counter == (5) && a == (4LL) && s == (25LL) && t == (9LL)) || ((!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(s == (1LL))) || (counter == (1) && a == (0LL) && s == (1LL) && !(t == (1LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (8)) || (counter == (8) && !(a == (7LL))) || (counter == (8) && a == (7LL) && !(s == (64LL))) || (counter == (8) && a == (7LL) && s == (64LL) && !(t == (15LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (12)) || (counter == (12) && !(a == (11LL))) || (counter == (12) && a == (11LL) && !(s == (144LL))) || (counter == (12) && a == (11LL) && s == (144LL) && !(t == (23LL)))) && (!(counter == (6)) || (counter == (6) && !(a == (5LL))) || (counter == (6) && a == (5LL) && !(s == (36LL))) || (counter == (6) && a == (5LL) && s == (36LL) && !(t == (11LL)))) && (!(counter == (5)) || (counter == (5) && !(a == (4LL))) || (counter == (5) && a == (4LL) && !(s == (25LL))) || (counter == (5) && a == (4LL) && s == (25LL) && !(t == (9LL)))) && counter == (13) && a == (12LL) && s == (169LL) && t == (25LL)) || ((!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(s == (1LL))) || (counter == (1) && a == (0LL) && s == (1LL) && !(t == (1LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (8)) || (counter == (8) && !(a == (7LL))) || (counter == (8) && a == (7LL) && !(s == (64LL))) || (counter == (8) && a == (7LL) && s == (64LL) && !(t == (15LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (12)) || (counter == (12) && !(a == (11LL))) || (counter == (12) && a == (11LL) && !(s == (144LL))) || (counter == (12) && a == (11LL) && s == (144LL) && !(t == (23LL)))) && (!(counter == (6)) || (counter == (6) && !(a == (5LL))) || (counter == (6) && a == (5LL) && !(s == (36LL))) || (counter == (6) && a == (5LL) && s == (36LL) && !(t == (11LL)))) && (!(counter == (5)) || (counter == (5) && !(a == (4LL))) || (counter == (5) && a == (4LL) && !(s == (25LL))) || (counter == (5) && a == (4LL) && s == (25LL) && !(t == (9LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && counter == (7) && a == (6LL) && s == (49LL) && t == (13LL)) || ((!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(s == (1LL))) || (counter == (1) && a == (0LL) && s == (1LL) && !(t == (1LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (8)) || (counter == (8) && !(a == (7LL))) || (counter == (8) && a == (7LL) && !(s == (64LL))) || (counter == (8) && a == (7LL) && s == (64LL) && !(t == (15LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (12)) || (counter == (12) && !(a == (11LL))) || (counter == (12) && a == (11LL) && !(s == (144LL))) || (counter == (12) && a == (11LL) && s == (144LL) && !(t == (23LL)))) && (!(counter == (6)) || (counter == (6) && !(a == (5LL))) || (counter == (6) && a == (5LL) && !(s == (36LL))) || (counter == (6) && a == (5LL) && s == (36LL) && !(t == (11LL)))) && (!(counter == (5)) || (counter == (5) && !(a == (4LL))) || (counter == (5) && a == (4LL) && !(s == (25LL))) || (counter == (5) && a == (4LL) && s == (25LL) && !(t == (9LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && (!(counter == (7)) || (counter == (7) && !(a == (6LL))) || (counter == (7) && a == (6LL) && !(s == (49LL))) || (counter == (7) && a == (6LL) && s == (49LL) && !(t == (13LL)))) && counter == (10) && a == (9LL) && s == (100LL) && t == (19LL)) || ((!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(s == (1LL))) || (counter == (1) && a == (0LL) && s == (1LL) && !(t == (1LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (8)) || (counter == (8) && !(a == (7LL))) || (counter == (8) && a == (7LL) && !(s == (64LL))) || (counter == (8) && a == (7LL) && s == (64LL) && !(t == (15LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (12)) || (counter == (12) && !(a == (11LL))) || (counter == (12) && a == (11LL) && !(s == (144LL))) || (counter == (12) && a == (11LL) && s == (144LL) && !(t == (23LL)))) && (!(counter == (6)) || (counter == (6) && !(a == (5LL))) || (counter == (6) && a == (5LL) && !(s == (36LL))) || (counter == (6) && a == (5LL) && s == (36LL) && !(t == (11LL)))) && (!(counter == (5)) || (counter == (5) && !(a == (4LL))) || (counter == (5) && a == (4LL) && !(s == (25LL))) || (counter == (5) && a == (4LL) && s == (25LL) && !(t == (9LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && (!(counter == (7)) || (counter == (7) && !(a == (6LL))) || (counter == (7) && a == (6LL) && !(s == (49LL))) || (counter == (7) && a == (6LL) && s == (49LL) && !(t == (13LL)))) && (!(counter == (10)) || (counter == (10) && !(a == (9LL))) || (counter == (10) && a == (9LL) && !(s == (100LL))) || (counter == (10) && a == (9LL) && s == (100LL) && !(t == (19LL)))) && counter == (9) && a == (8LL) && s == (81LL) && t == (17LL)) || ((!(counter == (18)) || (counter == (18) && !(a == (17LL))) || (counter == (18) && a == (17LL) && !(s == (324LL))) || (counter == (18) && a == (17LL) && s == (324LL) && !(t == (35LL)))) && (!(counter == (17)) || (counter == (17) && !(a == (16LL))) || (counter == (17) && a == (16LL) && !(s == (289LL))) || (counter == (17) && a == (16LL) && s == (289LL) && !(t == (33LL)))) && (!(counter == (19)) || (counter == (19) && !(a == (18LL))) || (counter == (19) && a == (18LL) && !(s == (361LL))) || (counter == (19) && a == (18LL) && s == (361LL) && !(t == (37LL)))) && (!(counter == (20)) || (counter == (20) && !(a == (19LL))) || (counter == (20) && a == (19LL) && !(s == (400LL))) || (counter == (20) && a == (19LL) && s == (400LL) && !(t == (39LL)))) && (!(counter == (16)) || (counter == (16) && !(a == (15LL))) || (counter == (16) && a == (15LL) && !(s == (256LL))) || (counter == (16) && a == (15LL) && s == (256LL) && !(t == (31LL)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(s == (4LL))) || (counter == (2) && a == (1LL) && s == (4LL) && !(t == (3LL)))) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(s == (1LL))) || (counter == (1) && a == (0LL) && s == (1LL) && !(t == (1LL)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(s == (9LL))) || (counter == (3) && a == (2LL) && s == (9LL) && !(t == (5LL)))) && (!(counter == (15)) || (counter == (15) && !(a == (14LL))) || (counter == (15) && a == (14LL) && !(s == (225LL))) || (counter == (15) && a == (14LL) && s == (225LL) && !(t == (29LL)))) && (!(counter == (8)) || (counter == (8) && !(a == (7LL))) || (counter == (8) && a == (7LL) && !(s == (64LL))) || (counter == (8) && a == (7LL) && s == (64LL) && !(t == (15LL)))) && (!(counter == (4)) || (counter == (4) && !(a == (3LL))) || (counter == (4) && a == (3LL) && !(s == (16LL))) || (counter == (4) && a == (3LL) && s == (16LL) && !(t == (7LL)))) && (!(counter == (14)) || (counter == (14) && !(a == (13LL))) || (counter == (14) && a == (13LL) && !(s == (196LL))) || (counter == (14) && a == (13LL) && s == (196LL) && !(t == (27LL)))) && (!(counter == (12)) || (counter == (12) && !(a == (11LL))) || (counter == (12) && a == (11LL) && !(s == (144LL))) || (counter == (12) && a == (11LL) && s == (144LL) && !(t == (23LL)))) && (!(counter == (6)) || (counter == (6) && !(a == (5LL))) || (counter == (6) && a == (5LL) && !(s == (36LL))) || (counter == (6) && a == (5LL) && s == (36LL) && !(t == (11LL)))) && (!(counter == (5)) || (counter == (5) && !(a == (4LL))) || (counter == (5) && a == (4LL) && !(s == (25LL))) || (counter == (5) && a == (4LL) && s == (25LL) && !(t == (9LL)))) && (!(counter == (13)) || (counter == (13) && !(a == (12LL))) || (counter == (13) && a == (12LL) && !(s == (169LL))) || (counter == (13) && a == (12LL) && s == (169LL) && !(t == (25LL)))) && (!(counter == (7)) || (counter == (7) && !(a == (6LL))) || (counter == (7) && a == (6LL) && !(s == (49LL))) || (counter == (7) && a == (6LL) && s == (49LL) && !(t == (13LL)))) && (!(counter == (10)) || (counter == (10) && !(a == (9LL))) || (counter == (10) && a == (9LL) && !(s == (100LL))) || (counter == (10) && a == (9LL) && s == (100LL) && !(t == (19LL)))) && (!(counter == (9)) || (counter == (9) && !(a == (8LL))) || (counter == (9) && a == (8LL) && !(s == (81LL))) || (counter == (9) && a == (8LL) && s == (81LL) && !(t == (17LL)))) && counter == (11) && a == (10LL) && s == (121LL) && t == (21LL)) (../plain/sqrt1-ll_unwindbound20.c:31:9)

runtime: 00:00:10.212
vars: 43, evals: 51

|rho|=43
|called|=8
|stable|=36
|infl|=37
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=32
Found 5 contexts for 4 functions. Top 5 functions:
2	contexts for entry state of __VERIFIER_assert (2009) on ../plain/sqrt1-ll_unwindbound20.c:11:1-17:1
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of reach_error (1999) on ../plain/sqrt1-ll_unwindbound20.c:5:1-5:74
1	contexts for entry state of main (2013) on ../plain/sqrt1-ll_unwindbound20.c:21:1-49:1

Memory statistics: total=1446.05MB, max=87.53MB, minor=1442.05MB, major=155.14MB, promoted=151.14MB
    minor collections=702  major collections=14 compactions=0


runtime: 00:00:20.235
vars: 57, evals: 167

|rho|=57
|called|=17
|stable|=56
|infl|=51
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=43
Found 8 contexts for 4 functions. Top 5 functions:
4	contexts for entry state of __VERIFIER_assert (2009) on ../plain/sqrt1-ll_unwindbound20.c:11:1-17:1
2	contexts for entry state of reach_error (1999) on ../plain/sqrt1-ll_unwindbound20.c:5:1-5:74
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2013) on ../plain/sqrt1-ll_unwindbound20.c:21:1-49:1

Memory statistics: total=4754.48MB, max=87.53MB, minor=4750.27MB, major=451.35MB, promoted=447.14MB
    minor collections=2288  major collections=34 compactions=0


runtime: 00:00:30.259
vars: 57, evals: 283

|rho|=57
|called|=8
|stable|=57
|infl|=51
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=43
Found 8 contexts for 4 functions. Top 5 functions:
4	contexts for entry state of __VERIFIER_assert (2009) on ../plain/sqrt1-ll_unwindbound20.c:11:1-17:1
2	contexts for entry state of reach_error (1999) on ../plain/sqrt1-ll_unwindbound20.c:5:1-5:74
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2013) on ../plain/sqrt1-ll_unwindbound20.c:21:1-49:1

Memory statistics: total=8200.30MB, max=100.66MB, minor=8195.86MB, major=780.77MB, promoted=776.33MB
    minor collections=3939  major collections=52 compactions=0


runtime: 00:00:40.272
vars: 57, evals: 390

|rho|=57
|called|=8
|stable|=50
|infl|=51
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=43
Found 8 contexts for 4 functions. Top 5 functions:
4	contexts for entry state of __VERIFIER_assert (2009) on ../plain/sqrt1-ll_unwindbound20.c:11:1-17:1
2	contexts for entry state of reach_error (1999) on ../plain/sqrt1-ll_unwindbound20.c:5:1-5:74
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2013) on ../plain/sqrt1-ll_unwindbound20.c:21:1-49:1

Memory statistics: total=11661.84MB, max=100.66MB, minor=11657.17MB, major=1109.59MB, promoted=1104.92MB
    minor collections=5598  major collections=73 compactions=0


runtime: 00:00:50.273
vars: 57, evals: 517

|rho|=57
|called|=8
|stable|=57
|infl|=51
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=43
Found 8 contexts for 4 functions. Top 5 functions:
4	contexts for entry state of __VERIFIER_assert (2009) on ../plain/sqrt1-ll_unwindbound20.c:11:1-17:1
2	contexts for entry state of reach_error (1999) on ../plain/sqrt1-ll_unwindbound20.c:5:1-5:74
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2013) on ../plain/sqrt1-ll_unwindbound20.c:21:1-49:1

Memory statistics: total=15106.27MB, max=100.66MB, minor=15101.37MB, major=1439.17MB, promoted=1434.27MB
    minor collections=7247  major collections=90 compactions=0


runtime: 00:01:00.288
vars: 57, evals: 608

|rho|=57
|called|=8
|stable|=50
|infl|=51
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=43
Found 8 contexts for 4 functions. Top 5 functions:
4	contexts for entry state of __VERIFIER_assert (2009) on ../plain/sqrt1-ll_unwindbound20.c:11:1-17:1
2	contexts for entry state of reach_error (1999) on ../plain/sqrt1-ll_unwindbound20.c:5:1-5:74
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2013) on ../plain/sqrt1-ll_unwindbound20.c:21:1-49:1

Memory statistics: total=18561.75MB, max=100.66MB, minor=18556.62MB, major=1768.10MB, promoted=1762.97MB
    minor collections=8902  major collections=108 compactions=0

