/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 cpachecker/hard2_valuebound20.yml.witness.yml --witness.yaml.validate cpachecker/hard2_valuebound20.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/hard2_valuebound20.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: d == (1) && p == (1) && B == (1) && (q == (9) || (!(q == (9)) && q == (20)) || (!(q == (9)) && !(q == (20)) && q == (0)) || (!(q == (9)) && !(q == (20)) && !(q == (0)) && q == (3)) || (!(q == (9)) && !(q == (20)) && !(q == (0)) && !(q == (3)) && q == (12)) || (!(q == (9)) && !(q == (20)) && !(q == (0)) && !(q == (3)) && !(q == (12)) && q == (4)) || (!(q == (9)) && !(q == (20)) && !(q == (0)) && !(q == (3)) && !(q == (12)) && !(q == (4)) && q == (1)) || (!(q == (9)) && !(q == (20)) && !(q == (0)) && !(q == (3)) && !(q == (12)) && !(q == (4)) && !(q == (1)) && q == (2)) || (!(q == (9)) && !(q == (20)) && !(q == (0)) && !(q == (3)) && !(q == (12)) && !(q == (4)) && !(q == (1)) && !(q == (2)) && q == (18)) || (!(q == (9)) && !(q == (20)) && !(q == (0)) && !(q == (3)) && !(q == (12)) && !(q == (4)) && !(q == (1)) && !(q == (2)) && !(q == (18)) && q == (17)) || (!(q == (9)) && !(q == (20)) && !(q == (0)) && !(q == (3)) && !(q == (12)) && !(q == (4)) && !(q == (1)) && !(q == (2)) && !(q == (18)) && !(q == (17)) && q == (19)) || (!(q == (9)) && !(q == (20)) && !(q == (0)) && !(q == (3)) && !(q == (12)) && !(q == (4)) && !(q == (1)) && !(q == (2)) && !(q == (18)) && !(q == (17)) && !(q == (19)) && q == (11)) || (!(q == (9)) && !(q == (20)) && !(q == (0)) && !(q == (3)) && !(q == (12)) && !(q == (4)) && !(q == (1)) && !(q == (2)) && !(q == (18)) && !(q == (17)) && !(q == (19)) && !(q == (11)) && q == (6)) || (!(q == (9)) && !(q == (20)) && !(q == (0)) && !(q == (3)) && !(q == (12)) && !(q == (4)) && !(q == (1)) && !(q == (2)) && !(q == (18)) && !(q == (17)) && !(q == (19)) && !(q == (11)) && !(q == (6)) && q == (13)) || (!(q == (9)) && !(q == (20)) && !(q == (0)) && !(q == (3)) && !(q == (12)) && !(q == (4)) && !(q == (1)) && !(q == (2)) && !(q == (18)) && !(q == (17)) && !(q == (19)) && !(q == (11)) && !(q == (6)) && !(q == (13)) && q == (16)) || (!(q == (9)) && !(q == (20)) && !(q == (0)) && !(q == (3)) && !(q == (12)) && !(q == (4)) && !(q == (1)) && !(q == (2)) && !(q == (18)) && !(q == (17)) && !(q == (19)) && !(q == (11)) && !(q == (6)) && !(q == (13)) && !(q == (16)) && q == (7)) || (!(q == (9)) && !(q == (20)) && !(q == (0)) && !(q == (3)) && !(q == (12)) && !(q == (4)) && !(q == (1)) && !(q == (2)) && !(q == (18)) && !(q == (17)) && !(q == (19)) && !(q == (11)) && !(q == (6)) && !(q == (13)) && !(q == (16)) && !(q == (7)) && q == (15)) || (!(q == (9)) && !(q == (20)) && !(q == (0)) && !(q == (3)) && !(q == (12)) && !(q == (4)) && !(q == (1)) && !(q == (2)) && !(q == (18)) && !(q == (17)) && !(q == (19)) && !(q == (11)) && !(q == (6)) && !(q == (13)) && !(q == (16)) && !(q == (7)) && !(q == (15)) && q == (5)) || (!(q == (9)) && !(q == (20)) && !(q == (0)) && !(q == (3)) && !(q == (12)) && !(q == (4)) && !(q == (1)) && !(q == (2)) && !(q == (18)) && !(q == (17)) && !(q == (19)) && !(q == (11)) && !(q == (6)) && !(q == (13)) && !(q == (16)) && !(q == (7)) && !(q == (15)) && !(q == (5)) && q == (10)) || (!(q == (9)) && !(q == (20)) && !(q == (0)) && !(q == (3)) && !(q == (12)) && !(q == (4)) && !(q == (1)) && !(q == (2)) && !(q == (18)) && !(q == (17)) && !(q == (19)) && !(q == (11)) && !(q == (6)) && !(q == (13)) && !(q == (16)) && !(q == (7)) && !(q == (15)) && !(q == (5)) && !(q == (10)) && q == (8)) || (!(q == (9)) && !(q == (20)) && !(q == (0)) && !(q == (3)) && !(q == (12)) && !(q == (4)) && !(q == (1)) && !(q == (2)) && !(q == (18)) && !(q == (17)) && !(q == (19)) && !(q == (11)) && !(q == (6)) && !(q == (13)) && !(q == (16)) && !(q == (7)) && !(q == (15)) && !(q == (5)) && !(q == (10)) && !(q == (8)) && q == (14))) (../plain/hard2_valuebound20.c:48:24)
[Warning][Witness] couldn't locate invariant: (B == (1) && d == (2) && p == (2) && q == (16)) || (B == (1) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (16)))) && d == (16) && p == (16) && q == (0)) || (B == (1) && !(q == (16)) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (0)))) && d == (2) && p == (2) && q == (12)) || (B == (1) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (16)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (0)))) && (!(d == (2)) || (d == (2) && !(p == (2)))) && d == (1) && p == (1) && q == (12)) || (B == (1) && !(q == (16)) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (0)))) && !(q == (12)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && d == (2) && p == (2) && q == (4)) || (B == (1) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (16)))) && (!(d == (16)) || (d == (16) && !(p == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (12)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (12)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (4)))) && d == (8) && p == (8) && q == (0)) || (B == (1) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (16)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (0)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (12)) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (4)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (0)))) && d == (1) && p == (1) && q == (6)) || (B == (1) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (16)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (0)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (12)) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (4)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (0)))) && !(q == (6)) && d == (1) && p == (1) && q == (14)) || (B == (1) && !(q == (16)) && (!(d == (16)) || (d == (16) && !(p == (16)))) && !(q == (12)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && !(q == (4)) && (!(d == (8)) || (d == (8) && !(p == (8)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (6)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (14)))) && d == (2) && p == (2) && q == (0)) || (B == (1) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (16)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (0)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (12)) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (4)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (0)))) && !(q == (6)) && !(q == (14)) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (0)))) && d == (1) && p == (1) && q == (20)) || (B == (1) && !(q == (16)) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16))) && !(q == (12)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && !(q == (4)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (6)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (14)))) && !(q == (0)) && (!(d == (1)) || (d == (1) && !(p == (1)))) && d == (2) && p == (2) && q == (20)) || (B == (1) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (16)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (0)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (12)) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (4)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (0)))) && !(q == (6)) && !(q == (14)) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (0)))) && !(q == (20)) && d == (1) && p == (1) && q == (18)) || (B == (1) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (16)))) && (!(d == (16)) || (d == (16) && !(p == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (12)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (12)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (4)))) && (!(d == (8)) || (d == (8) && !(p == (8)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (6)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (14)))) && (!(d == (2)) || (d == (2) && !(p == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (20)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (20)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (18)))) && d == (4) && p == (4) && q == (0)) || (B == (1) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (16)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (0)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (12)) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (4)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (0)))) && !(q == (6)) && !(q == (14)) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (0)))) && !(q == (20)) && !(q == (18)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4) && !(q == (0)))) && d == (1) && p == (1) && q == (2)) || (B == (1) && !(q == (16)) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16))) && !(q == (12)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && !(q == (4)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (6)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (14)))) && !(q == (0)) && !(q == (20)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (18)))) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (2)))) && d == (2) && p == (2) && q == (8)) || (B == (1) && (!(d == (2)) || (d == (2) && !(p == (2)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (12)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (12)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (4)))) && !(q == (0)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (6)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (14)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (20)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (20)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (18)))) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (2)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (8)))) && d == (8) && p == (8) && q == (16)) || (B == (1) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (16)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (0)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (12)) && (!(d == (2)) || (d == (2) && !(p == (2)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (0)))) && !(q == (6)) && !(q == (14)) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (0)))) && !(q == (20)) && !(q == (18)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4) && !(q == (0)))) && !(q == (2)) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (8)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (16)))) && d == (1) && p == (1) && q == (4)) || (B == (1) && (!(d == (2)) || (d == (2) && !(p == (2)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (12)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (12)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (4)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (6)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (14)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (20)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (20)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (18)))) && !(q == (0)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (2)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (8)))) && (!(d == (8)) || (d == (8) && !(p == (8)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (4)))) && d == (4) && p == (4) && q == (16)) || (B == (1) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (16)))) && (!(d == (16)) || (d == (16) && !(p == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (12)) && (!(d == (8)) || (d == (8) && !(p == (8)))) && !(q == (6)) && !(q == (14)) && (!(d == (2)) || (d == (2) && !(p == (2)))) && !(q == (20)) && !(q == (18)) && (!(d == (4)) || (d == (4) && !(p == (4)))) && !(q == (2)) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (8)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (16)))) && !(q == (4)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4) && !(q == (16)))) && d == (1) && p == (1) && q == (0)) || (B == (1) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (16)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (12)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && !(q == (6)) && !(q == (14)) && !(q == (20)) && !(q == (18)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && !(q == (2)) && (!(d == (2)) || (d == (2) && !(p == (2)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (16)))) && !(q == (4)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4) && !(q == (16)))) && !(q == (0)) && d == (1) && p == (1) && q == (8)) || (B == (1) && (!(d == (2)) || (d == (2) && !(p == (2)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (12)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && !(q == (6)) && !(q == (14)) && !(q == (20)) && !(q == (18)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && !(q == (2)) && (!(d == (8)) || (d == (8) && !(p == (8)))) && !(q == (4)) && (!(d == (4)) || (d == (4) && !(p == (4)))) && !(q == (0)) && !(q == (8)) && d == (1) && p == (1) && q == (16)) || (B == (1) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16))) && !(q == (12)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && !(q == (6)) && !(q == (14)) && !(q == (20)) && !(q == (18)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && !(q == (2)) && !(q == (4)) && !(q == (0)) && !(q == (8)) && !(q == (16)) && d == (1) && p == (1) && q == (10)) || (B == (1) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (12)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (12)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (4)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (6)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (14)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (20)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (20)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (18)))) && !(q == (0)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (2)))) && (!(d == (2)) || (d == (2) && !(p == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (4)))) && !(q == (16)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && (!(d == (1)) || (d == (1) && !(p == (1)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (10)))) && d == (4) && p == (4) && q == (8)) (../plain/hard2_valuebound20.c:50:9)
[Warning][Witness] couldn't locate invariant: (B == (1) && d == (32) && p == (32) && q == (0)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32) && !(q == (0)))) && d == (16) && p == (16) && q == (16)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32) && !(q == (0)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && d == (2) && p == (2) && q == (20)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32) && !(q == (0)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (20)))) && d == (1) && p == (1) && q == (2)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32) && !(q == (0)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (20)))) && !(q == (2)) && d == (1) && p == (1) && q == (3)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32) && !(q == (0)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (20)))) && !(q == (2)) && !(q == (3)) && d == (1) && p == (1) && q == (5)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32) && !(q == (0)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (20)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (3)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (5)))) && d == (8) && p == (8) && q == (8)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32) && !(q == (0)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2)))) && !(q == (2)) && !(q == (3)) && !(q == (5)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (8)))) && d == (1) && p == (1) && q == (20)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32) && !(q == (0)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && !(q == (20)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (3)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (5)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (8)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && d == (2) && p == (2) && q == (18)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32) && !(q == (0)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (3)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (5)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (8)))) && (!(d == (1)) || (d == (1) && !(p == (1)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (18)))) && d == (4) && p == (4) && q == (20)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (20)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (3)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (5)))) && !(q == (8)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (20)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (18)))) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4) && !(q == (20)))) && d == (8) && p == (8) && q == (0)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32) && !(q == (0)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && !(q == (20)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (3)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (5)))) && (!(d == (8)) || (d == (8) && !(p == (8)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && !(q == (18)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (0)))) && d == (2) && p == (2) && q == (8)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32) && !(q == (0)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (2)) && !(q == (3)) && !(q == (5)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (8)))) && !(q == (20)) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (18)))) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (0)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (8)))) && d == (1) && p == (1) && q == (12)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32) && !(q == (0)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (2)) && !(q == (3)) && !(q == (5)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (8)))) && !(q == (20)) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (18)))) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (0)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (8)))) && !(q == (12)) && d == (1) && p == (1) && q == (10)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32) && !(q == (0)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (2)) && !(q == (3)) && !(q == (5)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (8)))) && !(q == (20)) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (18)))) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (0)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (8)))) && !(q == (12)) && !(q == (10)) && d == (1) && p == (1) && q == (1)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (3)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (5)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (8)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (18)))) && !(q == (20)) && (!(d == (8)) || (d == (8) && !(p == (8)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (8)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (12)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (10)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (1)))) && d == (4) && p == (4) && q == (0)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32) && !(q == (0)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && !(q == (20)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (3)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (5)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && !(q == (18)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (0)))) && !(q == (8)) && (!(d == (1)) || (d == (1) && !(p == (1)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (10)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (1)))) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4) && !(q == (0)))) && d == (2) && p == (2) && q == (12)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (2)) && !(q == (3)) && !(q == (5)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (8)))) && !(q == (20)) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (18)))) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (8)) || (d == (8) && !(p == (8)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (8)))) && !(q == (12)) && !(q == (10)) && !(q == (1)) && (!(d == (4)) || (d == (4) && !(p == (4)))) && d == (1) && p == (1) && q == (0)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (2)) && !(q == (3)) && !(q == (5)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (8)))) && !(q == (20)) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (18)))) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (8)))) && !(q == (12)) && !(q == (10)) && !(q == (1)) && !(q == (0)) && d == (1) && p == (1) && q == (17)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32))) && (!(d == (16)) || (d == (16) && !(p == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (20)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (3)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (5)))) && !(q == (8)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (20)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (18)))) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4) && !(q == (20)))) && !(q == (0)) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (12)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (10)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (1)))) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (12)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (17)))) && d == (8) && p == (8) && q == (16)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32) && !(q == (0)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && !(q == (20)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (3)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (5)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && !(q == (18)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (0)))) && !(q == (8)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (10)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (1)))) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4) && !(q == (0)))) && !(q == (12)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (0)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (17)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (16)))) && d == (2) && p == (2) && q == (4)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32) && !(q == (0)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && !(q == (20)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (3)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (5)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && !(q == (18)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (0)))) && !(q == (8)) && (!(d == (1)) || (d == (1) && !(p == (1)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (1)))) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4) && !(q == (0)))) && !(q == (12)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (0)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (17)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (16)))) && !(q == (4)) && d == (2) && p == (2) && q == (10)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32) && !(q == (0)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && !(q == (20)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (3)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (5)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && !(q == (18)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (0)))) && !(q == (8)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (1)))) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4) && !(q == (0)))) && !(q == (12)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (0)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (17)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (16)))) && !(q == (4)) && !(q == (10)) && d == (2) && p == (2) && q == (14)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (2)) && !(q == (3)) && !(q == (5)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (8)))) && !(q == (20)) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (18)))) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (8)))) && !(q == (12)) && !(q == (10)) && !(q == (1)) && !(q == (0)) && !(q == (17)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (4)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (14)))) && d == (1) && p == (1) && q == (15)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32) && !(q == (0)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && !(q == (20)) && (!(d == (1)) || (d == (1) && !(p == (1)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (3)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (5)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && !(q == (18)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (0)))) && !(q == (8)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (1)))) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4) && !(q == (0)))) && !(q == (12)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (0)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (17)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (16)))) && !(q == (4)) && !(q == (10)) && !(q == (14)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (15)))) && d == (2) && p == (2) && q == (2)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (2)) && !(q == (3)) && !(q == (5)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (8)))) && !(q == (20)) && (!(d == (2)) || (d == (2) && !(p == (2)))) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (8)))) && !(q == (12)) && !(q == (10)) && !(q == (1)) && !(q == (0)) && !(q == (17)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (4)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (14)))) && !(q == (15)) && d == (1) && p == (1) && q == (18)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (2)) && !(q == (3)) && !(q == (5)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (8)))) && !(q == (20)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (8)))) && !(q == (12)) && !(q == (10)) && !(q == (1)) && !(q == (0)) && !(q == (17)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (4)))) && (!(d == (2)) || (d == (2) && !(p == (2)))) && !(q == (15)) && !(q == (18)) && d == (1) && p == (1) && q == (14)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (3)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (5)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (8)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (18)))) && !(q == (20)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (8)))) && (!(d == (1)) || (d == (1) && !(p == (1)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (10)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (1)))) && !(q == (0)) && (!(d == (2)) || (d == (2) && !(p == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (17)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (4)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (10)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (14)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (15)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (18)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (14)))) && d == (4) && p == (4) && q == (12)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (2)) && !(q == (3)) && !(q == (5)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (8)))) && !(q == (20)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (8)))) && !(q == (12)) && !(q == (10)) && !(q == (1)) && !(q == (0)) && !(q == (17)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (4)))) && !(q == (15)) && !(q == (18)) && !(q == (14)) && d == (1) && p == (1) && q == (19)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (2)) && !(q == (3)) && !(q == (5)) && (!(d == (8)) || (d == (8) && !(p == (8)))) && !(q == (20)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && (!(d == (2)) || (d == (2) && !(p == (2)))) && !(q == (12)) && !(q == (10)) && !(q == (1)) && !(q == (0)) && !(q == (17)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (4)))) && !(q == (15)) && !(q == (18)) && !(q == (14)) && !(q == (19)) && d == (1) && p == (1) && q == (8)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32)))) && !(q == (16)) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (20)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (3)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (5)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (8)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (20)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (18)))) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4) && !(q == (20)))) && (!(d == (8)) || (d == (8) && !(p == (8)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (8)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (12)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (10)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (1)))) && (!(d == (4)) || (d == (4) && !(p == (4)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (12)))) && (!(d == (1)) || (d == (1) && !(p == (1)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (17)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (4)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (10)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (14)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (15)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (18)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (14)))) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4) && !(q == (12)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (19)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (8)))) && d == (16) && p == (16) && q == (0)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32))) && (!(d == (16)) || (d == (16) && !(p == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (2)) && !(q == (3)) && !(q == (5)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && !(q == (20)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && !(q == (12)) && !(q == (10)) && !(q == (1)) && !(q == (0)) && !(q == (17)) && (!(d == (8)) || (d == (8) && !(p == (8)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (4)))) && !(q == (15)) && !(q == (18)) && !(q == (14)) && !(q == (19)) && !(q == (8)) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16))) && d == (1) && p == (1) && q == (16)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (3)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (5)))) && (!(d == (8)) || (d == (8) && !(p == (8)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (18)))) && !(q == (20)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && (!(d == (2)) || (d == (2) && !(p == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (10)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (1)))) && !(q == (0)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (17)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (4)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (10)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (14)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (15)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (18)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (14)))) && !(q == (12)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (19)))) && (!(d == (1)) || (d == (1) && !(p == (1)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (16)))) && d == (4) && p == (4) && q == (8)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (2)) && !(q == (3)) && !(q == (5)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && !(q == (20)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && !(q == (12)) && !(q == (10)) && !(q == (1)) && !(q == (0)) && !(q == (17)) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (4)))) && !(q == (15)) && !(q == (18)) && !(q == (14)) && !(q == (19)) && !(q == (8)) && !(q == (16)) && d == (1) && p == (1) && q == (13)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (2)) && !(q == (3)) && !(q == (5)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && !(q == (20)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && !(q == (12)) && !(q == (10)) && !(q == (1)) && !(q == (0)) && !(q == (17)) && (!(d == (2)) || (d == (2) && !(p == (2)))) && !(q == (15)) && !(q == (18)) && !(q == (14)) && !(q == (19)) && !(q == (8)) && !(q == (16)) && !(q == (13)) && d == (1) && p == (1) && q == (4)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (2)) && !(q == (3)) && !(q == (5)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && !(q == (20)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && !(q == (12)) && !(q == (10)) && !(q == (1)) && !(q == (0)) && !(q == (17)) && !(q == (15)) && !(q == (18)) && !(q == (14)) && !(q == (19)) && !(q == (8)) && !(q == (16)) && !(q == (13)) && !(q == (4)) && d == (1) && p == (1) && q == (11)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (2)) && !(q == (3)) && !(q == (5)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && !(q == (20)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && !(q == (12)) && !(q == (10)) && !(q == (1)) && !(q == (0)) && !(q == (17)) && !(q == (15)) && !(q == (18)) && !(q == (14)) && !(q == (19)) && !(q == (8)) && !(q == (16)) && !(q == (13)) && !(q == (4)) && !(q == (11)) && d == (1) && p == (1) && q == (6)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32) && !(q == (0)))) && (!(d == (16)) || (d == (16) && !(p == (16)))) && !(q == (20)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (3)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (5)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && !(q == (18)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (0)))) && !(q == (8)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (1)))) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4) && !(q == (0)))) && !(q == (12)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (0)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (17)))) && (!(d == (8)) || (d == (8) && !(p == (8)))) && !(q == (4)) && !(q == (10)) && !(q == (14)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (15)))) && !(q == (2)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (19)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (0)))) && (!(d == (1)) || (d == (1) && !(p == (1)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (13)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (11)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (6)))) && d == (2) && p == (2) && q == (16)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16))) && !(q == (20)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (3)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (5)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && !(q == (18)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && (!(d == (8)) || (d == (8) && !(p == (8)))) && !(q == (8)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (1)))) && (!(d == (4)) || (d == (4) && !(p == (4)))) && !(q == (12)) && (!(d == (1)) || (d == (1) && !(p == (1)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (17)))) && !(q == (4)) && !(q == (10)) && !(q == (14)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (15)))) && !(q == (2)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (19)))) && (!(d == (16)) || (d == (16) && !(p == (16)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (13)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (11)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (6)))) && !(q == (16)) && d == (2) && p == (2) && q == (0)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (3)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (5)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (18)))) && !(q == (20)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (10)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (1)))) && !(q == (0)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (17)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8) && !(q == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (10)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (14)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (15)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (18)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (14)))) && !(q == (12)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (19)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (16)))) && !(q == (8)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (13)))) && (!(d == (1)) || (d == (1) && !(p == (1)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (11)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (6)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (16)))) && d == (4) && p == (4) && q == (4)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32))) && (!(d == (16)) || (d == (16) && !(p == (16)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (3)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (5)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (18)))) && !(q == (20)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (10)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (1)))) && !(q == (0)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (17)))) && (!(d == (8)) || (d == (8) && !(p == (8)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (10)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (14)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (15)))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2) && !(q == (2)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (18)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (14)))) && !(q == (12)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (19)))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16))) && (!(d == (1)) || (d == (1) && !(p == (1)))) && !(q == (8)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (13)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (11)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (6)))) && (!(d == (2)) || (d == (2) && !(p == (2)))) && !(q == (4)) && d == (4) && p == (4) && q == (16)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16))) && !(q == (20)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (3)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (5)))) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && !(q == (18)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && !(q == (8)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (1)))) && !(q == (12)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (17)))) && !(q == (4)) && !(q == (10)) && !(q == (14)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (15)))) && !(q == (2)) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (19)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (13)))) && (!(d == (1)) || (d == (1) && !(p == (1))) || (d == (1) && p == (1) && !(q == (11)))) && (!(d == (1)) || (d == (1) && !(p == (1)))) && !(q == (16)) && !(q == (0)) && d == (2) && p == (2) && q == (6)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (2)) && !(q == (3)) && !(q == (5)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && !(q == (20)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && !(q == (12)) && !(q == (10)) && !(q == (1)) && !(q == (0)) && !(q == (17)) && !(q == (15)) && !(q == (18)) && !(q == (14)) && !(q == (19)) && !(q == (8)) && !(q == (16)) && !(q == (13)) && !(q == (4)) && !(q == (11)) && !(q == (6)) && d == (1) && p == (1) && q == (7)) || (B == (1) && (!(d == (32)) || (d == (32) && !(p == (32))) || (d == (32) && p == (32))) && (!(d == (16)) || (d == (16) && !(p == (16))) || (d == (16) && p == (16))) && (!(d == (2)) || (d == (2) && !(p == (2))) || (d == (2) && p == (2))) && !(q == (2)) && !(q == (3)) && !(q == (5)) && (!(d == (8)) || (d == (8) && !(p == (8))) || (d == (8) && p == (8))) && !(q == (20)) && (!(d == (4)) || (d == (4) && !(p == (4))) || (d == (4) && p == (4))) && !(q == (12)) && !(q == (10)) && !(q == (1)) && !(q == (0)) && !(q == (17)) && !(q == (15)) && !(q == (18)) && !(q == (14)) && !(q == (19)) && !(q == (8)) && !(q == (16)) && !(q == (13)) && !(q == (4)) && !(q == (11)) && !(q == (6)) && !(q == (7)) && d == (1) && p == (1) && q == (9)) (../plain/hard2_valuebound20.c:46:9)

runtime: 00:00:10.123
vars: 75, evals: 264

|rho|=75
|called|=5
|stable|=66
|infl|=73
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=56
Found 8 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard2_valuebound20.c:14:1-20:1
2	contexts for entry state of reach_error (1999) on ../plain/hard2_valuebound20.c:8:1-8:71
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 assume_abort_if_not (2006) on ../plain/hard2_valuebound20.c:11:1-13:1
1	contexts for entry state of main (2012) on ../plain/hard2_valuebound20.c:22:1-61:1

Memory statistics: total=2877.09MB, max=43.51MB, minor=2873.57MB, major=333.14MB, promoted=329.62MB
    minor collections=1387  major collections=35 compactions=0


runtime: 00:00:20.141
vars: 75, evals: 387

|rho|=75
|called|=5
|stable|=74
|infl|=73
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=56
Found 8 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard2_valuebound20.c:14:1-20:1
2	contexts for entry state of reach_error (1999) on ../plain/hard2_valuebound20.c:8:1-8:71
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 assume_abort_if_not (2006) on ../plain/hard2_valuebound20.c:11:1-13:1
1	contexts for entry state of main (2012) on ../plain/hard2_valuebound20.c:22:1-61:1

Memory statistics: total=5514.90MB, max=43.51MB, minor=5511.14MB, major=645.58MB, promoted=641.82MB
    minor collections=2659  major collections=64 compactions=0


runtime: 00:00:30.152
vars: 75, evals: 509

|rho|=75
|called|=5
|stable|=67
|infl|=73
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=56
Found 8 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard2_valuebound20.c:14:1-20:1
2	contexts for entry state of reach_error (1999) on ../plain/hard2_valuebound20.c:8:1-8:71
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 assume_abort_if_not (2006) on ../plain/hard2_valuebound20.c:11:1-13:1
1	contexts for entry state of main (2012) on ../plain/hard2_valuebound20.c:22:1-61:1

Memory statistics: total=8277.20MB, max=43.51MB, minor=8273.20MB, major=968.05MB, promoted=964.05MB
    minor collections=3990  major collections=92 compactions=0


runtime: 00:00:40.165
vars: 75, evals: 643

|rho|=75
|called|=5
|stable|=74
|infl|=73
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=56
Found 8 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard2_valuebound20.c:14:1-20:1
2	contexts for entry state of reach_error (1999) on ../plain/hard2_valuebound20.c:8:1-8:71
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 assume_abort_if_not (2006) on ../plain/hard2_valuebound20.c:11:1-13:1
1	contexts for entry state of main (2012) on ../plain/hard2_valuebound20.c:22:1-61:1

Memory statistics: total=10973.46MB, max=43.51MB, minor=10969.22MB, major=1290.48MB, promoted=1286.24MB
    minor collections=5291  major collections=122 compactions=0


runtime: 00:00:50.182
vars: 75, evals: 765

|rho|=75
|called|=5
|stable|=67
|infl|=73
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=56
Found 8 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard2_valuebound20.c:14:1-20:1
2	contexts for entry state of reach_error (1999) on ../plain/hard2_valuebound20.c:8:1-8:71
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 assume_abort_if_not (2006) on ../plain/hard2_valuebound20.c:11:1-13:1
1	contexts for entry state of main (2012) on ../plain/hard2_valuebound20.c:22:1-61:1

Memory statistics: total=13628.25MB, max=43.51MB, minor=13623.77MB, major=1602.27MB, promoted=1597.80MB
    minor collections=6571  major collections=150 compactions=0


runtime: 00:01:00.195
vars: 75, evals: 899

|rho|=75
|called|=5
|stable|=74
|infl|=73
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=56
Found 8 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard2_valuebound20.c:14:1-20:1
2	contexts for entry state of reach_error (1999) on ../plain/hard2_valuebound20.c:8:1-8:71
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 assume_abort_if_not (2006) on ../plain/hard2_valuebound20.c:11:1-13:1
1	contexts for entry state of main (2012) on ../plain/hard2_valuebound20.c:22:1-61:1

Memory statistics: total=16246.76MB, max=43.51MB, minor=16242.04MB, major=1922.48MB, promoted=1917.76MB
    minor collections=7834  major collections=179 compactions=0

