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


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((m == 9 && x == 12) || (((! (m == 9) || (m == 9 && ! (x == 12))) && m == 8) && x == 11)) || ((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 8) || (m == 8 && ! (x == 11)))) && m == 2) && x == 10)) || (((((! (m == 9) || (m == 9 && ! (x == 12))) && ! (m == 8)) && (! (m == 2) || (m == 2 && ! (x == 10)))) && m == 7) && x == 11)) || ((((! (m == 9) && (! (m == 2) || (m == 2 && ! (x == 10)))) && ! (x == 11)) && m == 7) && x == 12)) || (((((! (m == 9) && (! (m == 8) || (m == 8 && ! (x == 11)))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && ! (m == 7)) && m == 11) && x == 12)) || (((((! (x == 12) && (! (m == 8) || (m == 8 && ! (x == 11)))) && ! (m == 2)) && (! (m == 7) || (m == 7 && ! (x == 11)))) && m == 9) && x == 10)) || ((((((! (m == 9) && (! (m == 8) || (m == 8 && ! (x == 11)))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && ! (m == 7)) && ! (m == 11)) && m == 10) && x == 12)) || (((((((((! (m == 8) || (m == 8 && ! (x == 11))) && ! (m == 2)) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && ! (m == 9)) && (! (m == 10) || (m == 10 && ! (x == 12)))) && m == 6) && x == 10)) || ((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && ! (x == 12)) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 6) || (m == 6 && ! (x == 10)))) && m == 11) && x == 13)) || ((((((((! (m == 9) && (! (m == 8) || (m == 8 && ! (x == 11)))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && ! (m == 7)) && ! (m == 11)) && ! (m == 10)) && (! (m == 6) || (m == 6 && ! (x == 10)))) && m == 4) && x == 12)) || ((((((! (x == 12) && ! (m == 8)) && ! (m == 7)) && ! (x == 10)) && (! (m == 11) || (m == 11 && ! (x == 13)))) && m == 9) && x == 11)) || ((((((((! (m == 8) && (! (m == 2) || (m == 2 && ! (x == 10)))) && ! (m == 7)) && ! (x == 12)) && (! (m == 6) || (m == 6 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && ! (m == 9)) && m == 10) && x == 11)) || (((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 6) || (m == 6 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && ! (x == 12)) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && m == 4) && x == 9)) || (((((((((! (m == 9) && (! (m == 8) || (m == 8 && ! (x == 11)))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && ! (m == 7)) && ! (m == 11)) && ! (m == 10)) && (! (m == 6) || (m == 6 && ! (x == 10)))) && ! (m == 4)) && m == 0) && x == 12)) || ((((((! (x == 12) && ! (x == 10)) && ! (m == 11)) && ! (x == 11)) && (! (m == 4) || (m == 4 && ! (x == 9)))) && m == 9) && x == 13)) || (((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 8) || (m == 8 && ! (x == 11)))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && ! (x == 10)) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && ! (m == 4)) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && m == 6) && x == 9)) || (((((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && ! (x == 10)) && ! (m == 11)) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && ! (m == 9)) && ! (x == 9)) && m == 6) && x == 13)) || (((((((((((! (m == 9) && (! (m == 8) || (m == 8 && ! (x == 11)))) && ! (m == 7)) && ! (m == 11)) && ! (m == 10)) && ! (x == 10)) && ! (m == 4)) && ! (m == 0)) && ! (x == 9)) && ! (x == 13)) && m == 6) && x == 12)) || ((((((((! (m == 2) && ! (x == 11)) && ! (x == 12)) && ! (m == 9)) && ! (m == 6)) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && m == 7) && x == 10)) || ((((((((((! (m == 9) && ! (x == 11)) && (! (m == 2) || (m == 2 && ! (x == 10)))) && ! (m == 7)) && ! (m == 11)) && ! (m == 10)) && ! (m == 4)) && ! (m == 0)) && ! (m == 6)) && m == 8) && x == 12)) || (((((((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 6) || (m == 6 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && ! (x == 12)) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && ! (x == 9)) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 13)))) && (! (m == 7) || (m == 7 && ! (x == 10)))) && m == 4) && x == 6)) || (((((((((((! (m == 2) || (m == 2 && ! (x == 10))) && ! (x == 12)) && ! (m == 11)) && ! (x == 11)) && (! (m == 4) || (m == 4 && ! (x == 9)))) && ! (m == 9)) && ! (m == 6)) && (! (m == 7) || (m == 7 && ! (x == 10)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && m == 10) && x == 13)) || ((((((((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && ! (m == 11)) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && ! (m == 9)) && ! (m == 6)) && (! (m == 7) || (m == 7 && ! (x == 10)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (m == 10)) && m == 12) && x == 13)) || (((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && ! (x == 10)) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && ! (x == 9)) && ! (x == 13)) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && m == 6) && x == 7)) || ((((((((((((! (x == 11) && (! (m == 2) || (m == 2 && ! (x == 10)))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && ! (m == 4)) && (! (m == 9) || (m == 9 && ! (x == 13)))) && ! (m == 6)) && (! (m == 7) || (m == 7 && ! (x == 10)))) && ! (x == 12)) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && m == 8) && x == 9)) || ((((((((((((((! (x == 11) && ! (x == 12)) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 13)))) && ! (x == 10)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && m == 7) && x == 8)) || (((((((((((! (m == 8) && ! (m == 7)) && ! (x == 10)) && ! (m == 9)) && ! (m == 10)) && ! (x == 9)) && ! (x == 13)) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (x == 7)) && m == 6) && x == 11)) || (((((((((((((! (x == 11) && (! (m == 2) || (m == 2 && ! (x == 10)))) && ! (m == 11)) && ! (m == 9)) && ! (m == 6)) && (! (m == 7) || (m == 7 && ! (x == 10)))) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (m == 10)) && ! (m == 12)) && ! (x == 9)) && (! (m == 7) || (m == 7 && ! (x == 8)))) && m == 8) && x == 13)) || ((((((((((! (x == 11) && ! (m == 2)) && ! (m == 9)) && ! (m == 6)) && ! (m == 7)) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (x == 9)) && ! (x == 13)) && m == 8) && x == 10)) || (((((((((((((! (x == 11) && ! (x == 12)) && ! (m == 11)) && (! (m == 4) || (m == 4 && ! (x == 9)))) && ! (m == 9)) && ! (m == 6)) && ! (x == 10)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (m == 10)) && ! (m == 12)) && ! (x == 8)) && ! (m == 8)) && m == 7) && x == 13)) || (((((((((((((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 8) || (m == 8 && ! (x == 11)))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 6) || (m == 6 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 12)))) && (! (m == 7) || (m == 7 && ! (x == 10)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && ! (m == 4)) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 6) || (m == 6 && ! (x == 11)))) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 13)))) && m == 5) && x == 6)) || ((((((((((((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 8) || (m == 8 && ! (x == 11)))) && ! (x == 10)) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 12)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 6) || (m == 6 && ! (x == 11)))) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 7) || (m == 7 && ! (x == 13)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && m == 2) && x == 4)) || (((((((((((((! (m == 9) && (! (m == 2) || (m == 2 && ! (x == 10)))) && ! (m == 7)) && ! (m == 11)) && ! (m == 10)) && ! (m == 4)) && ! (m == 0)) && ! (m == 6)) && ! (m == 8)) && (! (m == 12) || (m == 12 && ! (x == 13)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && m == 3) && x == 12)) || ((((((((((((((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && ! (x == 12)) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && ! (x == 9)) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 7) || (m == 7 && ! (x == 10)))) && ! (x == 6)) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 6)) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 13)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && m == 4) && x == 7)) || (((((((((((! (x == 11) && ! (x == 12)) && ! (m == 4)) && ! (m == 6)) && ! (x == 10)) && ! (m == 8)) && ! (x == 8)) && ! (x == 13)) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && m == 7) && x == 9)) || ((((((((((((((((((! (m == 8) && ! (x == 10)) && ! (m == 7)) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 12)))) && ! (m == 9)) && ! (m == 10)) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 6)) && (! (m == 5) || (m == 5 && ! (x == 6)))) && ! (x == 4)) && (! (m == 3) || (m == 3 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && m == 2) && x == 11)) || (((((((((((! (x == 10) && ! (x == 9)) && ! (x == 13)) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (x == 7)) && ! (m == 7)) && ! (x == 11)) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && m == 6) && x == 8)) || ((((((((((((((((((! (m == 2) && (! (m == 11) || (m == 11 && ! (x == 12)))) && ! (m == 9)) && (! (m == 10) || (m == 10 && ! (x == 12)))) && ! (m == 6)) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && ! (m == 7)) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 8)) && ! (x == 6)) && (! (m == 3) || (m == 3 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && m == 5) && x == 10)) || (((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && ! (m == 4)) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && ! (m == 6)) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 8)) && ! (x == 6)) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 12)))) && ! (m == 7)) && (! (m == 2) || (m == 2 && ! (x == 11)))) && ! (x == 10)) && m == 5) && x == 9)) || (((((((((((((((((! (m == 8) && ! (m == 7)) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 12)))) && ! (m == 9)) && ! (m == 10)) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 6)) && ! (x == 6)) && (! (m == 3) || (m == 3 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && ! (m == 2)) && ! (x == 10)) && ! (x == 9)) && m == 5) && x == 11)) || (((((((((((((((((((((((((((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 6) || (m == 6 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 13)))) && (! (m == 7) || (m == 7 && ! (x == 10)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 6) || (m == 6 && ! (x == 11)))) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 13)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 7) || (m == 7 && ! (x == 9)))) && (! (m == 2) || (m == 2 && ! (x == 11)))) && (! (m == 6) || (m == 6 && ! (x == 8)))) && (! (m == 5) || (m == 5 && ! (x == 10)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 11)))) && m == 3) && x == 5)) || (((((((((((((((! (m == 8) && ! (m == 7)) && (! (m == 11) || (m == 11 && ! (x == 13)))) && ! (x == 12)) && ! (m == 9)) && ! (m == 10)) && ! (x == 9)) && ! (x == 6)) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 6)) && ! (x == 7)) && ! (m == 2)) && ! (m == 5)) && (! (m == 3) || (m == 3 && ! (x == 5)))) && m == 4) && x == 11)) || ((((((((((((((((((((((! (m == 2) || (m == 2 && ! (x == 10))) && ! (m == 11)) && (! (m == 4) || (m == 4 && ! (x == 9)))) && ! (m == 9)) && ! (m == 6)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (m == 10)) && ! (m == 12)) && ! (m == 8)) && ! (m == 7)) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 2) || (m == 2 && ! (x == 11)))) && (! (m == 5) || (m == 5 && ! (x == 10)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 11)))) && ! (x == 5)) && (! (m == 4) || (m == 4 && ! (x == 11)))) && m == 3) && x == 13)) || ((((((((((((((((((((((! (m == 2) && (! (m == 11) || (m == 11 && ! (x == 12)))) && ! (m == 9)) && (! (m == 10) || (m == 10 && ! (x == 12)))) && ! (m == 6)) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && ! (m == 7)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 8)) && (! (m == 3) || (m == 3 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && ! (m == 5)) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 4) || (m == 4 && ! (x == 11)))) && (! (m == 3) || (m == 3 && ! (x == 13)))) && m == 1) && x == 10)) || ((((((((((((((((((((((! (m == 2) || (m == 2 && ! (x == 10))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && ! (x == 12)) && ! (x == 9)) && (! (m == 9) || (m == 9 && ! (x == 13)))) && ! (x == 6)) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 7)) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 10)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && ! (x == 7)) && ! (m == 6)) && (! (m == 5) || (m == 5 && ! (x == 10)))) && (! (m == 3) || (m == 3 && ! (x == 5)))) && ! (x == 11)) && (! (m == 3) || (m == 3 && ! (x == 13)))) && (! (m == 1) || (m == 1 && ! (x == 10)))) && m == 4) && x == 8)) || ((((((((((((((((((((! (x == 10) && ! (m == 11)) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && ! (m == 9)) && ! (m == 6)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (m == 10)) && ! (m == 12)) && ! (m == 8)) && ! (m == 7)) && (! (m == 5) || (m == 5 && ! (x == 6)))) && ! (x == 4)) && (! (m == 4) || (m == 4 && ! (x == 7)))) && ! (x == 11)) && (! (m == 5) || (m == 5 && ! (x == 9)))) && ! (m == 3)) && (! (m == 4) || (m == 4 && ! (x == 8)))) && m == 2) && x == 13)) || (((((((((((((((((((((((((! (m == 2) || (m == 2 && ! (x == 10))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 6) || (m == 6 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && ! (x == 12)) && ! (x == 9)) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 13)))) && (! (m == 7) || (m == 7 && ! (x == 10)))) && ! (x == 6)) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 13)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && ! (x == 7)) && (! (m == 5) || (m == 5 && ! (x == 10)))) && ! (m == 3)) && ! (x == 11)) && (! (m == 1) || (m == 1 && ! (x == 10)))) && ! (x == 8)) && (! (m == 2) || (m == 2 && ! (x == 13)))) && m == 4) && x == 5)) || (((((((((((((((((((((((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 6) || (m == 6 && ! (x == 10)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 7) || (m == 7 && ! (x == 10)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 6) || (m == 6 && ! (x == 11)))) && (! (m == 8) || (m == 8 && ! (x == 10)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && ! (m == 2)) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 7) || (m == 7 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 8)))) && (! (m == 5) || (m == 5 && ! (x == 10)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 11)))) && ! (x == 5)) && (! (m == 4) || (m == 4 && ! (x == 11)))) && ! (x == 13)) && (! (m == 1) || (m == 1 && ! (x == 10)))) && (! (m == 4) || (m == 4 && ! (x == 8)))) && m == 3) && x == 4)) || ((((((((((((((! (m == 8) && ! (m == 7)) && ! (m == 9)) && ! (m == 10)) && ! (m == 6)) && ! (x == 12)) && ! (m == 2)) && ! (m == 5)) && ! (x == 5)) && ! (m == 4)) && ! (x == 13)) && (! (m == 1) || (m == 1 && ! (x == 10)))) && ! (x == 4)) && m == 3) && x == 11)) || (((((((((((((((((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 8) || (m == 8 && ! (x == 11)))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 6)) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 7) || (m == 7 && ! (x == 13)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 12)))) && ! (m == 4)) && (! (m == 7) || (m == 7 && ! (x == 9)))) && (! (m == 2) || (m == 2 && ! (x == 11)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 11)))) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 13)))) && ! (x == 10)) && (! (m == 2) || (m == 2 && ! (x == 13)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 11)))) && m == 1) && x == 7)) || ((((((((((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 6)) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 7) || (m == 7 && ! (x == 13)))) && ! (x == 6)) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 12)))) && ! (m == 4)) && ! (x == 10)) && ! (x == 9)) && ! (x == 11)) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 13)))) && (! (m == 2) || (m == 2 && ! (x == 13)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && ! (m == 1)) && m == 5) && x == 7)) || (((((((((((((((((((((((! (x == 12) && ! (x == 10)) && ! (x == 11)) && (! (m == 4) || (m == 4 && ! (x == 9)))) && ! (x == 13)) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 7) || (m == 7 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 8)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 4) || (m == 4 && ! (x == 8)))) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && m == 9) && x == 14)) || (((((((((((((((((! (m == 2) && ! (m == 9)) && ! (m == 6)) && (! (m == 4) || (m == 4 && ! (x == 9)))) && ! (m == 7)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (m == 8)) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 7)))) && ! (m == 5)) && ! (x == 5)) && ! (x == 13)) && ! (m == 1)) && (! (m == 4) || (m == 4 && ! (x == 8)))) && ! (x == 4)) && ! (x == 11)) && m == 3) && x == 10)) || ((((((((((((((((((! (x == 11) && ! (x == 12)) && ! (x == 10)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && ! (x == 8)) && ! (x == 13)) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && ! (x == 9)) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && ! (m == 9)) && m == 7) && x == 14)) || ((((((((((((((((((! (m == 9) && ! (m == 7)) && ! (m == 11)) && ! (m == 10)) && ! (m == 4)) && ! (m == 0)) && ! (m == 6)) && ! (m == 8)) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (x == 6)) && (! (m == 2) || (m == 2 && ! (x == 4)))) && ! (m == 3)) && ! (x == 10)) && ! (x == 9)) && ! (x == 11)) && (! (m == 2) || (m == 2 && ! (x == 13)))) && ! (x == 7)) && m == 5) && x == 12)) || (((((((((((((((((! (m == 8) || (m == 8 && ! (x == 9))) && ! (m == 7)) && (! (m == 5) || (m == 5 && ! (x == 6)))) && ! (x == 12)) && ! (m == 6)) && (! (m == 5) || (m == 5 && ! (x == 9)))) && ! (x == 5)) && ! (x == 13)) && ! (m == 4)) && ! (x == 4)) && ! (x == 11)) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && (! (m == 9) || (m == 9 && ! (x == 14)))) && ! (x == 10)) && m == 3) && x == 8)) || ((((((((((((((((((((((((! (m == 11) && (! (m == 4) || (m == 4 && ! (x == 9)))) && ! (x == 12)) && ! (m == 9)) && ! (m == 6)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (m == 10)) && ! (m == 12)) && ! (m == 8)) && ! (m == 7)) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 10)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 11)))) && (! (m == 4) || (m == 4 && ! (x == 11)))) && ! (m == 3)) && (! (m == 1) || (m == 1 && ! (x == 10)))) && (! (m == 4) || (m == 4 && ! (x == 8)))) && ! (m == 2)) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && m == 0) && x == 13)) || (((((((((((((((((((((! (m == 11) || (m == 11 && ! (x == 13))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 7)) && (! (m == 8) || (m == 8 && ! (x == 13)))) && ! (x == 6)) && (! (m == 2) || (m == 2 && ! (x == 4)))) && ! (m == 6)) && ! (x == 10)) && ! (x == 9)) && ! (x == 11)) && ! (m == 4)) && (! (m == 2) || (m == 2 && ! (x == 13)))) && ! (x == 7)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && ! (x == 12)) && ! (m == 3)) && (! (m == 0) || (m == 0 && ! (x == 13)))) && m == 5) && x == 8)) || ((((((((((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 8) || (m == 8 && ! (x == 11)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && ! (m == 7)) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 2) || (m == 2 && ! (x == 11)))) && ! (m == 6)) && ! (x == 10)) && ! (m == 4)) && (! (m == 2) || (m == 2 && ! (x == 13)))) && ! (x == 7)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && ! (m == 3)) && (! (m == 0) || (m == 0 && ! (x == 13)))) && ! (m == 5)) && m == 1) && x == 8)) || ((((((((((((((((((((((((((((((((((((((((((((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 6) || (m == 6 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 12)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 11)))) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 10)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 2) || (m == 2 && ! (x == 11)))) && (! (m == 6) || (m == 6 && ! (x == 8)))) && (! (m == 5) || (m == 5 && ! (x == 10)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 11)))) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 4) || (m == 4 && ! (x == 11)))) && (! (m == 3) || (m == 3 && ! (x == 13)))) && (! (m == 1) || (m == 1 && ! (x == 10)))) && (! (m == 4) || (m == 4 && ! (x == 8)))) && (! (m == 2) || (m == 2 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 11)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && ! (m == 9)) && (! (m == 3) || (m == 3 && ! (x == 10)))) && ! (m == 7)) && (! (m == 5) || (m == 5 && ! (x == 12)))) && (! (m == 3) || (m == 3 && ! (x == 8)))) && (! (m == 0) || (m == 0 && ! (x == 13)))) && (! (m == 5) || (m == 5 && ! (x == 8)))) && (! (m == 1) || (m == 1 && ! (x == 8)))) && m == 13) && x == 14)) || ((((((((((((((((((((! (m == 11) && ! (m == 9)) && ! (m == 6)) && ! (m == 10)) && ! (m == 12)) && ! (m == 8)) && ! (m == 7)) && ! (x == 6)) && ! (x == 10)) && ! (x == 9)) && ! (x == 11)) && ! (m == 3)) && ! (m == 2)) && (! (m == 4) || (m == 4 && ! (x == 5)))) && ! (x == 7)) && ! (x == 12)) && ! (m == 0)) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && m == 5) && x == 13)) || (((((((((((((((((((! (m == 6) || (m == 6 && ! (x == 9))) && ! (m == 4)) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && ! (m == 5)) && ! (x == 12)) && (! (m == 7) || (m == 7 && ! (x == 9)))) && ! (x == 5)) && ! (x == 13)) && ! (x == 4)) && ! (x == 11)) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 9) || (m == 9 && ! (x == 14)))) && ! (x == 10)) && (! (m == 7) || (m == 7 && ! (x == 14)))) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && m == 3) && x == 6)) || ((((((((((((((((((! (m == 6) && (! (m == 8) || (m == 8 && ! (x == 9)))) && ! (x == 12)) && ! (m == 4)) && (! (m == 7) || (m == 7 && ! (x == 9)))) && ! (x == 5)) && ! (x == 13)) && ! (x == 4)) && ! (x == 11)) && ! (m == 1)) && ! (m == 5)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && ! (x == 10)) && (! (m == 7) || (m == 7 && ! (x == 14)))) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (x == 6)) && m == 3) && x == 7)) || (((((((((((((((((((((((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 6) || (m == 6 && ! (x == 10)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && ! (x == 12)) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 7) || (m == 7 && ! (x == 10)))) && ! (m == 4)) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 6) || (m == 6 && ! (x == 11)))) && (! (m == 8) || (m == 8 && ! (x == 10)))) && ! (m == 5)) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 7) || (m == 7 && ! (x == 9)))) && (! (m == 2) || (m == 2 && ! (x == 11)))) && (! (m == 6) || (m == 6 && ! (x == 8)))) && (! (m == 1) || (m == 1 && ! (x == 10)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && ! (x == 13)) && (! (m == 1) || (m == 1 && ! (x == 8)))) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (m == 3)) && m == 0) && x == 6)) || (((((((((((((((((((((! (m == 11) && ! (x == 12)) && ! (x == 9)) && ! (m == 9)) && ! (m == 6)) && ! (x == 6)) && ! (m == 10)) && ! (m == 12)) && ! (m == 8)) && ! (m == 7)) && ! (x == 7)) && ! (x == 11)) && ! (m == 3)) && (! (m == 1) || (m == 1 && ! (x == 10)))) && ! (x == 8)) && ! (m == 2)) && ! (x == 5)) && ! (m == 0)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (m == 5)) && m == 4) && x == 13)) || (((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && ! (x == 10)) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && ! (m == 7)) && ! (x == 4)) && ! (x == 11)) && ! (m == 6)) && ! (m == 4)) && ! (x == 13)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && ! (m == 3)) && ! (m == 5)) && ! (m == 1)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && (! (m == 0) || (m == 0 && ! (x == 6)))) && m == 2) && x == 8)) || ((((((((((((((((((((((((((((! (m == 2) || (m == 2 && ! (x == 10))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && ! (m == 4)) && ! (x == 12)) && ! (m == 6)) && ! (m == 8)) && (! (m == 2) || (m == 2 && ! (x == 4)))) && ! (m == 7)) && (! (m == 2) || (m == 2 && ! (x == 11)))) && ! (m == 5)) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 1) || (m == 1 && ! (x == 10)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 11)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 3) || (m == 3 && ! (x == 10)))) && (! (m == 3) || (m == 3 && ! (x == 8)))) && ! (x == 13)) && (! (m == 1) || (m == 1 && ! (x == 8)))) && (! (m == 13) || (m == 13 && ! (x == 14)))) && (! (m == 3) || (m == 3 && ! (x == 7)))) && ! (x == 6)) && (! (m == 2) || (m == 2 && ! (x == 8)))) && m == 0) && x == 9)) || (((((((((((((((((((((! (m == 8) && ! (m == 7)) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && ! (m == 9)) && ! (m == 10)) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 6)) && ! (m == 2)) && ! (m == 5)) && ! (m == 4)) && ! (x == 10)) && ! (m == 3)) && ! (x == 7)) && (! (m == 0) || (m == 0 && ! (x == 13)))) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && (! (m == 0) || (m == 0 && ! (x == 6)))) && (! (m == 0) || (m == 0 && ! (x == 9)))) && m == 1) && x == 11)) || (((((((((((((((((((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && ! (x == 10)) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 12)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && ! (x == 4)) && (! (m == 3) || (m == 3 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 7) || (m == 7 && ! (x == 9)))) && ! (x == 11)) && (! (m == 5) || (m == 5 && ! (x == 9)))) && (! (m == 3) || (m == 3 && ! (x == 5)))) && ! (x == 13)) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && (! (m == 5) || (m == 5 && ! (x == 12)))) && (! (m == 13) || (m == 13 && ! (x == 14)))) && (! (m == 3) || (m == 3 && ! (x == 6)))) && (! (m == 3) || (m == 3 && ! (x == 7)))) && (! (m == 0) || (m == 0 && ! (x == 6)))) && ! (x == 8)) && (! (m == 0) || (m == 0 && ! (x == 9)))) && m == 2) && x == 3)) || (((((((((((((((((((! (m == 2) && ! (m == 9)) && ! (m == 6)) && (! (m == 10) || (m == 10 && ! (x == 11)))) && ! (x == 12)) && ! (m == 7)) && ! (m == 8)) && (! (m == 4) || (m == 4 && ! (x == 7)))) && ! (m == 5)) && (! (m == 4) || (m == 4 && ! (x == 11)))) && ! (m == 1)) && (! (m == 4) || (m == 4 && ! (x == 8)))) && (! (m == 4) || (m == 4 && ! (x == 5)))) && ! (m == 3)) && ! (x == 13)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (x == 6)) && ! (x == 9)) && m == 0) && x == 10)) || (((((((((((((((((((((((((((((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && ! (x == 12)) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 6) || (m == 6 && ! (x == 11)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 2) || (m == 2 && ! (x == 11)))) && (! (m == 6) || (m == 6 && ! (x == 8)))) && (! (m == 5) || (m == 5 && ! (x == 11)))) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 4) || (m == 4 && ! (x == 11)))) && (! (m == 4) || (m == 4 && ! (x == 8)))) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 11)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && (! (m == 3) || (m == 3 && ! (x == 8)))) && ! (x == 13)) && (! (m == 5) || (m == 5 && ! (x == 8)))) && (! (m == 1) || (m == 1 && ! (x == 8)))) && (! (m == 13) || (m == 13 && ! (x == 14)))) && (! (m == 3) || (m == 3 && ! (x == 7)))) && ! (x == 6)) && (! (m == 2) || (m == 2 && ! (x == 8)))) && ! (x == 9)) && (! (m == 1) || (m == 1 && ! (x == 11)))) && (! (m == 2) || (m == 2 && ! (x == 3)))) && ! (x == 10)) && m == 0) && x == 2)) || (((((((((((((((((((! (m == 9) && ! (x == 10)) && ! (m == 7)) && ! (m == 11)) && ! (m == 10)) && ! (m == 4)) && ! (m == 0)) && ! (m == 6)) && ! (m == 8)) && ! (x == 4)) && ! (m == 3)) && ! (x == 11)) && ! (x == 13)) && (! (m == 1) || (m == 1 && ! (x == 7)))) && ! (m == 5)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (x == 8)) && ! (x == 3)) && m == 2) && x == 12)) || ((((((((((((((((((! (m == 8) && ! (m == 7)) && ! (m == 9)) && ! (m == 10)) && ! (x == 12)) && ! (m == 6)) && ! (m == 2)) && ! (m == 5)) && ! (m == 4)) && ! (m == 3)) && ! (x == 13)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (x == 6)) && ! (x == 9)) && ! (m == 1)) && ! (x == 10)) && ! (x == 2)) && m == 0) && x == 11)) || (((((((((((((((((((! (m == 2) && ! (m == 9)) && ! (m == 6)) && ! (x == 12)) && ! (x == 9)) && ! (m == 7)) && ! (x == 6)) && ! (m == 8)) && ! (x == 7)) && ! (m == 5)) && ! (x == 11)) && ! (m == 1)) && ! (x == 8)) && ! (x == 5)) && ! (m == 3)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (x == 13)) && ! (m == 0)) && m == 4) && x == 10)) || (((((((((((((((((((((((! (x == 12) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 6) || (m == 6 && ! (x == 8)))) && ! (m == 3)) && ! (m == 4)) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && ! (x == 13)) && (! (m == 5) || (m == 5 && ! (x == 8)))) && (! (m == 1) || (m == 1 && ! (x == 8)))) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (x == 6)) && (! (m == 2) || (m == 2 && ! (x == 8)))) && ! (x == 9)) && (! (m == 2) || (m == 2 && ! (x == 3)))) && ! (x == 10)) && ! (x == 2)) && ! (x == 11)) && m == 0) && x == 5)) || (((((((((((((((((((((((((((! (x == 12) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 6) || (m == 6 && ! (x == 8)))) && (! (m == 4) || (m == 4 && ! (x == 8)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && (! (m == 3) || (m == 3 && ! (x == 8)))) && ! (x == 13)) && (! (m == 5) || (m == 5 && ! (x == 8)))) && (! (m == 1) || (m == 1 && ! (x == 8)))) && (! (m == 13) || (m == 13 && ! (x == 14)))) && (! (m == 3) || (m == 3 && ! (x == 7)))) && ! (x == 6)) && (! (m == 2) || (m == 2 && ! (x == 8)))) && ! (x == 9)) && (! (m == 2) || (m == 2 && ! (x == 3)))) && ! (x == 10)) && ! (x == 2)) && ! (x == 11)) && ! (x == 5)) && m == 0) && x == 1)) || ((((((((((((((((((((! (x == 10) && (! (m == 6) || (m == 6 && ! (x == 9)))) && ! (m == 4)) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && ! (m == 5)) && ! (x == 4)) && (! (m == 7) || (m == 7 && ! (x == 9)))) && ! (x == 11)) && ! (x == 13)) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (m == 3)) && ! (m == 0)) && ! (x == 8)) && ! (x == 3)) && ! (x == 12)) && m == 2) && x == 6)) || ((((((((((((((((((((((((((! (x == 12) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 6) || (m == 6 && ! (x == 8)))) && (! (m == 4) || (m == 4 && ! (x == 8)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && (! (m == 3) || (m == 3 && ! (x == 8)))) && ! (x == 13)) && (! (m == 5) || (m == 5 && ! (x == 8)))) && (! (m == 1) || (m == 1 && ! (x == 8)))) && (! (m == 13) || (m == 13 && ! (x == 14)))) && (! (m == 3) || (m == 3 && ! (x == 7)))) && ! (x == 6)) && ! (x == 9)) && ! (m == 2)) && ! (x == 10)) && ! (x == 2)) && ! (x == 11)) && ! (x == 5)) && ! (x == 1)) && m == 0) && x == 3)) || (((((((((((((((((((! (m == 4) && ! (m == 6)) && ! (m == 8)) && ! (x == 12)) && ! (m == 7)) && ! (m == 5)) && ! (x == 5)) && ! (x == 13)) && ! (x == 4)) && ! (x == 11)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && ! (x == 10)) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (x == 6)) && ! (x == 7)) && ! (m == 0)) && (! (m == 2) || (m == 2 && ! (x == 3)))) && m == 3) && x == 9)) || ((((((((((((((((((((((((((((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 12)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 7) || (m == 7 && ! (x == 13)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 12)))) && (! (m == 7) || (m == 7 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 13)))) && ! (x == 10)) && (! (m == 2) || (m == 2 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && ! (x == 7)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && (! (m == 5) || (m == 5 && ! (x == 12)))) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && (! (m == 5) || (m == 5 && ! (x == 13)))) && (! (m == 3) || (m == 3 && ! (x == 6)))) && (! (m == 4) || (m == 4 && ! (x == 13)))) && ! (x == 11)) && (! (m == 2) || (m == 2 && ! (x == 3)))) && ! (m == 0)) && (! (m == 2) || (m == 2 && ! (x == 12)))) && (! (m == 2) || (m == 2 && ! (x == 6)))) && (! (m == 3) || (m == 3 && ! (x == 9)))) && m == 1) && x == 2)) || ((((((((((((((((((((((((((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 12)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 7) || (m == 7 && ! (x == 13)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && ! (m == 2)) && (! (m == 7) || (m == 7 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && ! (x == 10)) && (! (m == 4) || (m == 4 && ! (x == 5)))) && ! (m == 3)) && ! (x == 7)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && (! (m == 5) || (m == 5 && ! (x == 12)))) && (! (m == 0) || (m == 0 && ! (x == 13)))) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && (! (m == 5) || (m == 5 && ! (x == 13)))) && (! (m == 0) || (m == 0 && ! (x == 6)))) && (! (m == 4) || (m == 4 && ! (x == 13)))) && (! (m == 0) || (m == 0 && ! (x == 9)))) && ! (x == 11)) && (! (m == 0) || (m == 0 && ! (x == 5)))) && (! (m == 0) || (m == 0 && ! (x == 1)))) && (! (m == 0) || (m == 0 && ! (x == 3)))) && ! (x == 2)) && m == 1) && x == 4)) || ((((((((((((((((((((((((((((((((((((! (x == 11) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && ! (x == 9)) && ! (x == 13)) && ! (x == 10)) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 6) || (m == 6 && ! (x == 8)))) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 4) || (m == 4 && ! (x == 8)))) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && ! (m == 9)) && ! (m == 7)) && (! (m == 3) || (m == 3 && ! (x == 8)))) && (! (m == 5) || (m == 5 && ! (x == 8)))) && (! (m == 1) || (m == 1 && ! (x == 8)))) && ! (m == 13)) && (! (m == 3) || (m == 3 && ! (x == 6)))) && (! (m == 3) || (m == 3 && ! (x == 7)))) && (! (m == 0) || (m == 0 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 8)))) && (! (m == 2) || (m == 2 && ! (x == 3)))) && (! (m == 0) || (m == 0 && ! (x == 2)))) && (! (m == 0) || (m == 0 && ! (x == 5)))) && (! (m == 0) || (m == 0 && ! (x == 1)))) && (! (m == 2) || (m == 2 && ! (x == 6)))) && (! (m == 0) || (m == 0 && ! (x == 3)))) && (! (m == 1) || (m == 1 && ! (x == 2)))) && (! (m == 1) || (m == 1 && ! (x == 4)))) && m == 8) && x == 14)) || ((((((((((((((((((((! (m == 11) && ! (m == 9)) && ! (m == 6)) && ! (m == 10)) && ! (m == 12)) && ! (m == 8)) && ! (m == 7)) && ! (m == 3)) && ! (x == 10)) && ! (m == 2)) && ! (x == 7)) && ! (m == 0)) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (m == 5)) && ! (m == 4)) && ! (x == 11)) && ! (x == 2)) && ! (x == 4)) && m == 1) && x == 13)) || (((((((((((((((((((((((((((((! (x == 10) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && ! (x == 4)) && (! (m == 4) || (m == 4 && ! (x == 7)))) && ! (x == 11)) && (! (m == 5) || (m == 5 && ! (x == 9)))) && (! (m == 3) || (m == 3 && ! (x == 5)))) && ! (x == 13)) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && ! (m == 9)) && ! (m == 7)) && ! (m == 13)) && (! (m == 3) || (m == 3 && ! (x == 7)))) && ! (x == 8)) && (! (m == 0) || (m == 0 && ! (x == 9)))) && ! (x == 3)) && (! (m == 0) || (m == 0 && ! (x == 2)))) && ! (x == 12)) && (! (m == 0) || (m == 0 && ! (x == 5)))) && (! (m == 0) || (m == 0 && ! (x == 1)))) && ! (x == 6)) && (! (m == 3) || (m == 3 && ! (x == 9)))) && (! (m == 1) || (m == 1 && ! (x == 2)))) && ! (m == 8)) && m == 2) && x == 14)) || ((((((((((((((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 12)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 7) || (m == 7 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && ! (m == 3)) && ! (x == 10)) && ! (m == 4)) && ! (x == 7)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && (! (m == 5) || (m == 5 && ! (x == 12)))) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (x == 11)) && (! (m == 2) || (m == 2 && ! (x == 3)))) && (! (m == 2) || (m == 2 && ! (x == 12)))) && ! (m == 0)) && (! (m == 2) || (m == 2 && ! (x == 6)))) && ! (x == 2)) && ! (x == 4)) && (! (m == 8) || (m == 8 && ! (x == 14)))) && ! (x == 13)) && (! (m == 2) || (m == 2 && ! (x == 14)))) && m == 1) && x == 5)) || ((((((((((((((((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 12)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 3) || (m == 3 && ! (x == 12)))) && (! (m == 7) || (m == 7 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && ! (x == 10)) && ! (x == 7)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && (! (m == 5) || (m == 5 && ! (x == 12)))) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && (! (m == 3) || (m == 3 && ! (x == 6)))) && ! (x == 11)) && ! (m == 2)) && ! (m == 0)) && (! (m == 3) || (m == 3 && ! (x == 9)))) && ! (x == 2)) && ! (x == 4)) && (! (m == 8) || (m == 8 && ! (x == 14)))) && ! (x == 13)) && ! (x == 5)) && m == 1) && x == 3)) || ((((((((((((((((((((((((((((! (x == 10) && ! (x == 9)) && ! (x == 13)) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (x == 7)) && ! (x == 11)) && (! (m == 5) || (m == 5 && ! (x == 6)))) && ! (x == 8)) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && ! (m == 9)) && ! (m == 7)) && ! (m == 13)) && (! (m == 3) || (m == 3 && ! (x == 6)))) && (! (m == 0) || (m == 0 && ! (x == 6)))) && (! (m == 0) || (m == 0 && ! (x == 2)))) && (! (m == 0) || (m == 0 && ! (x == 5)))) && (! (m == 0) || (m == 0 && ! (x == 1)))) && (! (m == 0) || (m == 0 && ! (x == 3)))) && (! (m == 1) || (m == 1 && ! (x == 2)))) && (! (m == 1) || (m == 1 && ! (x == 4)))) && ! (m == 8)) && ! (m == 2)) && (! (m == 1) || (m == 1 && ! (x == 5)))) && (! (m == 1) || (m == 1 && ! (x == 3)))) && m == 6) && x == 14)) || ((((((((((((((((((((((((! (x == 12) && ! (m == 6)) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && ! (m == 4)) && ! (m == 1)) && ! (m == 5)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && ! (x == 13)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (m == 3)) && ! (x == 6)) && (! (m == 2) || (m == 2 && ! (x == 8)))) && ! (x == 9)) && ! (x == 10)) && ! (x == 2)) && ! (x == 11)) && ! (x == 5)) && ! (x == 1)) && ! (x == 3)) && (! (m == 8) || (m == 8 && ! (x == 14)))) && (! (m == 2) || (m == 2 && ! (x == 14)))) && m == 0) && x == 7)) || ((((((((((((((((((((((((((! (x == 6) && ! (x == 10)) && ! (x == 9)) && ! (x == 11)) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && ! (x == 7)) && ! (m == 9)) && ! (m == 7)) && ! (x == 12)) && ! (x == 8)) && ! (m == 13)) && ! (x == 13)) && (! (m == 0) || (m == 0 && ! (x == 2)))) && (! (m == 0) || (m == 0 && ! (x == 5)))) && (! (m == 0) || (m == 0 && ! (x == 1)))) && (! (m == 0) || (m == 0 && ! (x == 3)))) && (! (m == 1) || (m == 1 && ! (x == 2)))) && (! (m == 1) || (m == 1 && ! (x == 4)))) && ! (m == 8)) && ! (m == 2)) && (! (m == 1) || (m == 1 && ! (x == 5)))) && (! (m == 1) || (m == 1 && ! (x == 3)))) && ! (m == 6)) && m == 5) && x == 14)) || ((((((((((((((((((((! (x == 10) && ! (m == 4)) && ! (m == 6)) && ! (m == 8)) && ! (x == 4)) && ! (m == 7)) && ! (x == 11)) && ! (m == 5)) && ! (x == 13)) && (! (m == 1) || (m == 1 && ! (x == 7)))) && ! (x == 8)) && ! (m == 0)) && ! (x == 3)) && ! (x == 12)) && ! (x == 6)) && ! (m == 3)) && (! (m == 1) || (m == 1 && ! (x == 2)))) && ! (x == 14)) && (! (m == 1) || (m == 1 && ! (x == 5)))) && m == 2) && x == 9)) || ((((((((((((((((((((((! (m == 9) && ! (m == 7)) && ! (m == 11)) && ! (m == 10)) && ! (m == 4)) && ! (m == 0)) && ! (m == 6)) && ! (m == 8)) && ! (m == 3)) && ! (x == 10)) && ! (x == 7)) && ! (m == 5)) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (x == 11)) && ! (m == 2)) && ! (x == 2)) && ! (x == 4)) && ! (x == 13)) && ! (x == 5)) && ! (x == 3)) && m == 1) && x == 12)) || ((((((((((((((((((((((((! (x == 12) && (! (m == 4) || (m == 4 && ! (x == 8)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && ! (m == 9)) && ! (m == 7)) && (! (m == 3) || (m == 3 && ! (x == 8)))) && ! (x == 13)) && (! (m == 1) || (m == 1 && ! (x == 8)))) && ! (m == 13)) && ! (x == 6)) && ! (x == 9)) && ! (x == 10)) && ! (x == 2)) && ! (x == 11)) && ! (x == 5)) && ! (x == 1)) && ! (x == 3)) && (! (m == 1) || (m == 1 && ! (x == 4)))) && ! (m == 8)) && ! (m == 2)) && ! (m == 6)) && ! (x == 7)) && ! (m == 5)) && m == 0) && x == 14)) || (((((((((((((((((! (x == 10) && (! (m == 6) || (m == 6 && ! (x == 7)))) && ! (x == 4)) && ! (x == 11)) && ! (m == 3)) && ! (x == 13)) && ! (m == 4)) && (! (m == 5) || (m == 5 && ! (x == 7)))) && ! (x == 8)) && ! (x == 3)) && ! (x == 12)) && ! (m == 0)) && ! (x == 6)) && ! (x == 14)) && ! (m == 1)) && ! (x == 9)) && m == 2) && x == 5)) || ((((((((((((((((((((! (x == 12) && ! (m == 7)) && ! (m == 6)) && ! (m == 4)) && ! (m == 3)) && ! (x == 13)) && ! (m == 5)) && ! (m == 1)) && ! (x == 6)) && ! (m == 2)) && ! (x == 9)) && ! (x == 10)) && ! (x == 2)) && ! (x == 11)) && ! (x == 5)) && ! (x == 1)) && ! (x == 3)) && ! (x == 7)) && ! (x == 14)) && m == 0) && x == 8)) || (((((((((((((((((((((((((! (m == 6) || (m == 6 && ! (x == 9))) && ! (m == 4)) && (! (m == 8) || (m == 8 && ! (x == 9)))) && ! (m == 5)) && (! (m == 7) || (m == 7 && ! (x == 9)))) && ! (x == 10)) && ! (x == 7)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (m == 3)) && ! (m == 0)) && ! (x == 11)) && ! (m == 2)) && ! (x == 2)) && ! (x == 4)) && (! (m == 8) || (m == 8 && ! (x == 14)))) && ! (x == 13)) && ! (x == 5)) && ! (x == 3)) && (! (m == 6) || (m == 6 && ! (x == 14)))) && ! (x == 12)) && m == 1) && x == 6)) || ((((((((((((((((((! (x == 10) && ! (m == 6)) && ! (x == 4)) && ! (m == 4)) && ! (x == 11)) && ! (x == 13)) && ! (m == 1)) && ! (m == 5)) && ! (m == 3)) && ! (x == 8)) && ! (x == 3)) && ! (x == 12)) && ! (x == 6)) && ! (x == 14)) && ! (m == 0)) && ! (x == 9)) && ! (x == 5)) && m == 2) && x == 7)) || ((((((((((((((((((((((! (m == 4) && ! (m == 6)) && ! (m == 8)) && ! (m == 7)) && ! (m == 5)) && ! (x == 10)) && ! (x == 7)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (m == 0)) && ! (x == 11)) && ! (m == 3)) && ! (x == 2)) && ! (x == 4)) && ! (x == 13)) && ! (x == 5)) && ! (x == 3)) && ! (m == 2)) && ! (x == 12)) && ! (x == 6)) && m == 1) && x == 9)) || (((((((((((((((((((((! (x == 10) && ! (x == 7)) && ! (m == 9)) && ! (m == 7)) && ! (x == 8)) && ! (m == 13)) && ! (x == 11)) && ! (x == 2)) && ! (x == 4)) && ! (m == 8)) && ! (x == 13)) && ! (m == 2)) && ! (x == 5)) && ! (x == 3)) && ! (m == 6)) && ! (m == 5)) && ! (x == 12)) && ! (m == 0)) && ! (x == 6)) && ! (x == 9)) && m == 1) && x == 14)) || ((((((((((((((((((((((((((((! (x == 12) && ! (x == 13)) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 4) || (m == 4 && ! (x == 11)))) && (! (m == 4) || (m == 4 && ! (x == 8)))) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 11)))) && ! (m == 9)) && (! (m == 3) || (m == 3 && ! (x == 10)))) && ! (m == 7)) && (! (m == 3) || (m == 3 && ! (x == 8)))) && ! (m == 13)) && (! (m == 3) || (m == 3 && ! (x == 6)))) && (! (m == 3) || (m == 3 && ! (x == 7)))) && (! (m == 4) || (m == 4 && ! (x == 10)))) && (! (m == 3) || (m == 3 && ! (x == 9)))) && ! (m == 8)) && ! (m == 2)) && ! (m == 6)) && ! (m == 5)) && ! (m == 0)) && ! (m == 1)) && m == 11) && x == 14)) || (((((((((((((((((! (x == 12) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && ! (x == 13)) && ! (x == 6)) && ! (x == 9)) && ! (x == 10)) && ! (x == 2)) && ! (x == 11)) && ! (x == 5)) && ! (x == 1)) && ! (x == 3)) && (! (m == 1) || (m == 1 && ! (x == 4)))) && ! (x == 7)) && ! (x == 14)) && ! (x == 8)) && m == 0) && x == 0)) || (((((((((((((((((((((! (x == 12) && ! (x == 5)) && ! (x == 13)) && ! (x == 4)) && ! (x == 11)) && ! (m == 9)) && ! (x == 10)) && ! (m == 7)) && ! (x == 8)) && ! (m == 13)) && ! (x == 6)) && ! (x == 7)) && ! (x == 9)) && ! (m == 8)) && ! (m == 2)) && ! (m == 6)) && ! (m == 5)) && ! (m == 0)) && ! (m == 1)) && ! (m == 11)) && m == 3) && x == 14)) || ((((((((((((((((((! (x == 12) && ! (m == 2)) && ! (m == 3)) && ! (x == 13)) && ! (x == 6)) && ! (x == 9)) && ! (x == 10)) && ! (x == 2)) && ! (x == 11)) && ! (x == 5)) && ! (x == 1)) && ! (x == 3)) && ! (m == 1)) && ! (x == 7)) && ! (x == 14)) && ! (x == 8)) && ! (x == 0)) && m == 0) && x == 4)) || (((((((((((((((((((((! (x == 12) && ! (x == 9)) && ! (x == 6)) && ! (x == 7)) && ! (x == 11)) && ! (x == 8)) && ! (x == 5)) && ! (m == 9)) && ! (m == 7)) && ! (m == 13)) && ! (x == 13)) && ! (x == 10)) && ! (m == 8)) && ! (m == 2)) && ! (m == 6)) && ! (m == 5)) && ! (m == 0)) && ! (m == 1)) && ! (m == 11)) && ! (m == 3)) && m == 4) && x == 14)) || (((((((((((((((((! (m == 10) || (m == 10 && ! (x == 12))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && ! (x == 13)) && ! (m == 9)) && ! (m == 7)) && ! (m == 13)) && ! (m == 8)) && ! (m == 2)) && ! (m == 6)) && ! (m == 5)) && ! (m == 0)) && ! (m == 1)) && ! (m == 11)) && ! (m == 3)) && ! (m == 4)) && m == 12) && x == 14)) || (((((((((((((((((! (x == 12) && ! (x == 11)) && ! (x == 13)) && ! (m == 9)) && ! (m == 7)) && ! (m == 13)) && ! (m == 8)) && ! (m == 2)) && ! (m == 6)) && ! (m == 5)) && ! (m == 0)) && ! (m == 1)) && ! (m == 11)) && ! (m == 3)) && ! (m == 4)) && ! (m == 12)) && m == 10) && x == 14) (../plain/gj2007b.i:27:9-27:36)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((m == 9 && x == 12) || (((! (m == 9) || (m == 9 && ! (x == 12))) && m == 8) && x == 11)) || ((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 8) || (m == 8 && ! (x == 11)))) && m == 2) && x == 10)) || (((((! (m == 9) || (m == 9 && ! (x == 12))) && ! (m == 8)) && (! (m == 2) || (m == 2 && ! (x == 10)))) && m == 7) && x == 11)) || ((((! (m == 9) && (! (m == 2) || (m == 2 && ! (x == 10)))) && ! (x == 11)) && m == 7) && x == 12)) || (((((! (m == 9) && (! (m == 8) || (m == 8 && ! (x == 11)))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && ! (m == 7)) && m == 11) && x == 12)) || (((((! (x == 12) && (! (m == 8) || (m == 8 && ! (x == 11)))) && ! (m == 2)) && (! (m == 7) || (m == 7 && ! (x == 11)))) && m == 9) && x == 10)) || ((((((! (m == 9) && (! (m == 8) || (m == 8 && ! (x == 11)))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && ! (m == 7)) && ! (m == 11)) && m == 10) && x == 12)) || (((((((((! (m == 8) || (m == 8 && ! (x == 11))) && ! (m == 2)) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && ! (m == 9)) && (! (m == 10) || (m == 10 && ! (x == 12)))) && m == 6) && x == 10)) || ((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && ! (x == 12)) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 6) || (m == 6 && ! (x == 10)))) && m == 11) && x == 13)) || ((((((((! (m == 9) && (! (m == 8) || (m == 8 && ! (x == 11)))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && ! (m == 7)) && ! (m == 11)) && ! (m == 10)) && (! (m == 6) || (m == 6 && ! (x == 10)))) && m == 4) && x == 12)) || ((((((! (x == 12) && ! (m == 8)) && ! (m == 7)) && ! (x == 10)) && (! (m == 11) || (m == 11 && ! (x == 13)))) && m == 9) && x == 11)) || ((((((((! (m == 8) && (! (m == 2) || (m == 2 && ! (x == 10)))) && ! (m == 7)) && ! (x == 12)) && (! (m == 6) || (m == 6 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && ! (m == 9)) && m == 10) && x == 11)) || (((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 6) || (m == 6 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && ! (x == 12)) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && m == 4) && x == 9)) || (((((((((! (m == 9) && (! (m == 8) || (m == 8 && ! (x == 11)))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && ! (m == 7)) && ! (m == 11)) && ! (m == 10)) && (! (m == 6) || (m == 6 && ! (x == 10)))) && ! (m == 4)) && m == 0) && x == 12)) || ((((((! (x == 12) && ! (x == 10)) && ! (m == 11)) && ! (x == 11)) && (! (m == 4) || (m == 4 && ! (x == 9)))) && m == 9) && x == 13)) || (((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 8) || (m == 8 && ! (x == 11)))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && ! (x == 10)) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && ! (m == 4)) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && m == 6) && x == 9)) || (((((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && ! (x == 10)) && ! (m == 11)) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && ! (m == 9)) && ! (x == 9)) && m == 6) && x == 13)) || (((((((((((! (m == 9) && (! (m == 8) || (m == 8 && ! (x == 11)))) && ! (m == 7)) && ! (m == 11)) && ! (m == 10)) && ! (x == 10)) && ! (m == 4)) && ! (m == 0)) && ! (x == 9)) && ! (x == 13)) && m == 6) && x == 12)) || ((((((((! (m == 2) && ! (x == 11)) && ! (x == 12)) && ! (m == 9)) && ! (m == 6)) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && m == 7) && x == 10)) || ((((((((((! (m == 9) && ! (x == 11)) && (! (m == 2) || (m == 2 && ! (x == 10)))) && ! (m == 7)) && ! (m == 11)) && ! (m == 10)) && ! (m == 4)) && ! (m == 0)) && ! (m == 6)) && m == 8) && x == 12)) || (((((((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 6) || (m == 6 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && ! (x == 12)) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && ! (x == 9)) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 13)))) && (! (m == 7) || (m == 7 && ! (x == 10)))) && m == 4) && x == 6)) || (((((((((((! (m == 2) || (m == 2 && ! (x == 10))) && ! (x == 12)) && ! (m == 11)) && ! (x == 11)) && (! (m == 4) || (m == 4 && ! (x == 9)))) && ! (m == 9)) && ! (m == 6)) && (! (m == 7) || (m == 7 && ! (x == 10)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && m == 10) && x == 13)) || ((((((((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && ! (m == 11)) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && ! (m == 9)) && ! (m == 6)) && (! (m == 7) || (m == 7 && ! (x == 10)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (m == 10)) && m == 12) && x == 13)) || (((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && ! (x == 10)) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && ! (x == 9)) && ! (x == 13)) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && m == 6) && x == 7)) || ((((((((((((! (x == 11) && (! (m == 2) || (m == 2 && ! (x == 10)))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && ! (m == 4)) && (! (m == 9) || (m == 9 && ! (x == 13)))) && ! (m == 6)) && (! (m == 7) || (m == 7 && ! (x == 10)))) && ! (x == 12)) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && m == 8) && x == 9)) || ((((((((((((((! (x == 11) && ! (x == 12)) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 13)))) && ! (x == 10)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && m == 7) && x == 8)) || (((((((((((! (m == 8) && ! (m == 7)) && ! (x == 10)) && ! (m == 9)) && ! (m == 10)) && ! (x == 9)) && ! (x == 13)) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (x == 7)) && m == 6) && x == 11)) || (((((((((((((! (x == 11) && (! (m == 2) || (m == 2 && ! (x == 10)))) && ! (m == 11)) && ! (m == 9)) && ! (m == 6)) && (! (m == 7) || (m == 7 && ! (x == 10)))) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (m == 10)) && ! (m == 12)) && ! (x == 9)) && (! (m == 7) || (m == 7 && ! (x == 8)))) && m == 8) && x == 13)) || ((((((((((! (x == 11) && ! (m == 2)) && ! (m == 9)) && ! (m == 6)) && ! (m == 7)) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (x == 9)) && ! (x == 13)) && m == 8) && x == 10)) || (((((((((((((! (x == 11) && ! (x == 12)) && ! (m == 11)) && (! (m == 4) || (m == 4 && ! (x == 9)))) && ! (m == 9)) && ! (m == 6)) && ! (x == 10)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (m == 10)) && ! (m == 12)) && ! (x == 8)) && ! (m == 8)) && m == 7) && x == 13)) || (((((((((((((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 8) || (m == 8 && ! (x == 11)))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 6) || (m == 6 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 12)))) && (! (m == 7) || (m == 7 && ! (x == 10)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && ! (m == 4)) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 6) || (m == 6 && ! (x == 11)))) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 13)))) && m == 5) && x == 6)) || ((((((((((((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 8) || (m == 8 && ! (x == 11)))) && ! (x == 10)) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 12)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 6) || (m == 6 && ! (x == 11)))) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 7) || (m == 7 && ! (x == 13)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && m == 2) && x == 4)) || (((((((((((((! (m == 9) && (! (m == 2) || (m == 2 && ! (x == 10)))) && ! (m == 7)) && ! (m == 11)) && ! (m == 10)) && ! (m == 4)) && ! (m == 0)) && ! (m == 6)) && ! (m == 8)) && (! (m == 12) || (m == 12 && ! (x == 13)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && m == 3) && x == 12)) || ((((((((((((((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && ! (x == 12)) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && ! (x == 9)) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 7) || (m == 7 && ! (x == 10)))) && ! (x == 6)) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 6)) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 13)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && m == 4) && x == 7)) || (((((((((((! (x == 11) && ! (x == 12)) && ! (m == 4)) && ! (m == 6)) && ! (x == 10)) && ! (m == 8)) && ! (x == 8)) && ! (x == 13)) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && m == 7) && x == 9)) || ((((((((((((((((((! (m == 8) && ! (x == 10)) && ! (m == 7)) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 12)))) && ! (m == 9)) && ! (m == 10)) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 6)) && (! (m == 5) || (m == 5 && ! (x == 6)))) && ! (x == 4)) && (! (m == 3) || (m == 3 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && m == 2) && x == 11)) || (((((((((((! (x == 10) && ! (x == 9)) && ! (x == 13)) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (x == 7)) && ! (m == 7)) && ! (x == 11)) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && m == 6) && x == 8)) || ((((((((((((((((((! (m == 2) && (! (m == 11) || (m == 11 && ! (x == 12)))) && ! (m == 9)) && (! (m == 10) || (m == 10 && ! (x == 12)))) && ! (m == 6)) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && ! (m == 7)) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 8)) && ! (x == 6)) && (! (m == 3) || (m == 3 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && m == 5) && x == 10)) || (((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && ! (m == 4)) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && ! (m == 6)) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 8)) && ! (x == 6)) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 12)))) && ! (m == 7)) && (! (m == 2) || (m == 2 && ! (x == 11)))) && ! (x == 10)) && m == 5) && x == 9)) || (((((((((((((((((! (m == 8) && ! (m == 7)) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 12)))) && ! (m == 9)) && ! (m == 10)) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 6)) && ! (x == 6)) && (! (m == 3) || (m == 3 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && ! (m == 2)) && ! (x == 10)) && ! (x == 9)) && m == 5) && x == 11)) || (((((((((((((((((((((((((((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 6) || (m == 6 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 13)))) && (! (m == 7) || (m == 7 && ! (x == 10)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 6) || (m == 6 && ! (x == 11)))) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 13)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 7) || (m == 7 && ! (x == 9)))) && (! (m == 2) || (m == 2 && ! (x == 11)))) && (! (m == 6) || (m == 6 && ! (x == 8)))) && (! (m == 5) || (m == 5 && ! (x == 10)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 11)))) && m == 3) && x == 5)) || (((((((((((((((! (m == 8) && ! (m == 7)) && (! (m == 11) || (m == 11 && ! (x == 13)))) && ! (x == 12)) && ! (m == 9)) && ! (m == 10)) && ! (x == 9)) && ! (x == 6)) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 6)) && ! (x == 7)) && ! (m == 2)) && ! (m == 5)) && (! (m == 3) || (m == 3 && ! (x == 5)))) && m == 4) && x == 11)) || ((((((((((((((((((((((! (m == 2) || (m == 2 && ! (x == 10))) && ! (m == 11)) && (! (m == 4) || (m == 4 && ! (x == 9)))) && ! (m == 9)) && ! (m == 6)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (m == 10)) && ! (m == 12)) && ! (m == 8)) && ! (m == 7)) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 2) || (m == 2 && ! (x == 11)))) && (! (m == 5) || (m == 5 && ! (x == 10)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 11)))) && ! (x == 5)) && (! (m == 4) || (m == 4 && ! (x == 11)))) && m == 3) && x == 13)) || ((((((((((((((((((((((! (m == 2) && (! (m == 11) || (m == 11 && ! (x == 12)))) && ! (m == 9)) && (! (m == 10) || (m == 10 && ! (x == 12)))) && ! (m == 6)) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && ! (m == 7)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 8)) && (! (m == 3) || (m == 3 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && ! (m == 5)) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 4) || (m == 4 && ! (x == 11)))) && (! (m == 3) || (m == 3 && ! (x == 13)))) && m == 1) && x == 10)) || ((((((((((((((((((((((! (m == 2) || (m == 2 && ! (x == 10))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && ! (x == 12)) && ! (x == 9)) && (! (m == 9) || (m == 9 && ! (x == 13)))) && ! (x == 6)) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 7)) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 10)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && ! (x == 7)) && ! (m == 6)) && (! (m == 5) || (m == 5 && ! (x == 10)))) && (! (m == 3) || (m == 3 && ! (x == 5)))) && ! (x == 11)) && (! (m == 3) || (m == 3 && ! (x == 13)))) && (! (m == 1) || (m == 1 && ! (x == 10)))) && m == 4) && x == 8)) || ((((((((((((((((((((! (x == 10) && ! (m == 11)) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && ! (m == 9)) && ! (m == 6)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (m == 10)) && ! (m == 12)) && ! (m == 8)) && ! (m == 7)) && (! (m == 5) || (m == 5 && ! (x == 6)))) && ! (x == 4)) && (! (m == 4) || (m == 4 && ! (x == 7)))) && ! (x == 11)) && (! (m == 5) || (m == 5 && ! (x == 9)))) && ! (m == 3)) && (! (m == 4) || (m == 4 && ! (x == 8)))) && m == 2) && x == 13)) || (((((((((((((((((((((((((! (m == 2) || (m == 2 && ! (x == 10))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 6) || (m == 6 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && ! (x == 12)) && ! (x == 9)) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 13)))) && (! (m == 7) || (m == 7 && ! (x == 10)))) && ! (x == 6)) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 13)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && ! (x == 7)) && (! (m == 5) || (m == 5 && ! (x == 10)))) && ! (m == 3)) && ! (x == 11)) && (! (m == 1) || (m == 1 && ! (x == 10)))) && ! (x == 8)) && (! (m == 2) || (m == 2 && ! (x == 13)))) && m == 4) && x == 5)) || (((((((((((((((((((((((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 6) || (m == 6 && ! (x == 10)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 7) || (m == 7 && ! (x == 10)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 6) || (m == 6 && ! (x == 11)))) && (! (m == 8) || (m == 8 && ! (x == 10)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && ! (m == 2)) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 7) || (m == 7 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 8)))) && (! (m == 5) || (m == 5 && ! (x == 10)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 11)))) && ! (x == 5)) && (! (m == 4) || (m == 4 && ! (x == 11)))) && ! (x == 13)) && (! (m == 1) || (m == 1 && ! (x == 10)))) && (! (m == 4) || (m == 4 && ! (x == 8)))) && m == 3) && x == 4)) || ((((((((((((((! (m == 8) && ! (m == 7)) && ! (m == 9)) && ! (m == 10)) && ! (m == 6)) && ! (x == 12)) && ! (m == 2)) && ! (m == 5)) && ! (x == 5)) && ! (m == 4)) && ! (x == 13)) && (! (m == 1) || (m == 1 && ! (x == 10)))) && ! (x == 4)) && m == 3) && x == 11)) || (((((((((((((((((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 8) || (m == 8 && ! (x == 11)))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 6)) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 7) || (m == 7 && ! (x == 13)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 12)))) && ! (m == 4)) && (! (m == 7) || (m == 7 && ! (x == 9)))) && (! (m == 2) || (m == 2 && ! (x == 11)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 11)))) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 13)))) && ! (x == 10)) && (! (m == 2) || (m == 2 && ! (x == 13)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 11)))) && m == 1) && x == 7)) || ((((((((((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 6)) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 7) || (m == 7 && ! (x == 13)))) && ! (x == 6)) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 12)))) && ! (m == 4)) && ! (x == 10)) && ! (x == 9)) && ! (x == 11)) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 13)))) && (! (m == 2) || (m == 2 && ! (x == 13)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && ! (m == 1)) && m == 5) && x == 7)) || (((((((((((((((((((((((! (x == 12) && ! (x == 10)) && ! (x == 11)) && (! (m == 4) || (m == 4 && ! (x == 9)))) && ! (x == 13)) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 7) || (m == 7 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 8)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 4) || (m == 4 && ! (x == 8)))) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && m == 9) && x == 14)) || (((((((((((((((((! (m == 2) && ! (m == 9)) && ! (m == 6)) && (! (m == 4) || (m == 4 && ! (x == 9)))) && ! (m == 7)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (m == 8)) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 7)))) && ! (m == 5)) && ! (x == 5)) && ! (x == 13)) && ! (m == 1)) && (! (m == 4) || (m == 4 && ! (x == 8)))) && ! (x == 4)) && ! (x == 11)) && m == 3) && x == 10)) || ((((((((((((((((((! (x == 11) && ! (x == 12)) && ! (x == 10)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && ! (x == 8)) && ! (x == 13)) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && ! (x == 9)) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && ! (m == 9)) && m == 7) && x == 14)) || ((((((((((((((((((! (m == 9) && ! (m == 7)) && ! (m == 11)) && ! (m == 10)) && ! (m == 4)) && ! (m == 0)) && ! (m == 6)) && ! (m == 8)) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (x == 6)) && (! (m == 2) || (m == 2 && ! (x == 4)))) && ! (m == 3)) && ! (x == 10)) && ! (x == 9)) && ! (x == 11)) && (! (m == 2) || (m == 2 && ! (x == 13)))) && ! (x == 7)) && m == 5) && x == 12)) || (((((((((((((((((! (m == 8) || (m == 8 && ! (x == 9))) && ! (m == 7)) && (! (m == 5) || (m == 5 && ! (x == 6)))) && ! (x == 12)) && ! (m == 6)) && (! (m == 5) || (m == 5 && ! (x == 9)))) && ! (x == 5)) && ! (x == 13)) && ! (m == 4)) && ! (x == 4)) && ! (x == 11)) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && (! (m == 9) || (m == 9 && ! (x == 14)))) && ! (x == 10)) && m == 3) && x == 8)) || ((((((((((((((((((((((((! (m == 11) && (! (m == 4) || (m == 4 && ! (x == 9)))) && ! (x == 12)) && ! (m == 9)) && ! (m == 6)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (m == 10)) && ! (m == 12)) && ! (m == 8)) && ! (m == 7)) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 10)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 11)))) && (! (m == 4) || (m == 4 && ! (x == 11)))) && ! (m == 3)) && (! (m == 1) || (m == 1 && ! (x == 10)))) && (! (m == 4) || (m == 4 && ! (x == 8)))) && ! (m == 2)) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && m == 0) && x == 13)) || (((((((((((((((((((((! (m == 11) || (m == 11 && ! (x == 13))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 7)) && (! (m == 8) || (m == 8 && ! (x == 13)))) && ! (x == 6)) && (! (m == 2) || (m == 2 && ! (x == 4)))) && ! (m == 6)) && ! (x == 10)) && ! (x == 9)) && ! (x == 11)) && ! (m == 4)) && (! (m == 2) || (m == 2 && ! (x == 13)))) && ! (x == 7)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && ! (x == 12)) && ! (m == 3)) && (! (m == 0) || (m == 0 && ! (x == 13)))) && m == 5) && x == 8)) || ((((((((((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 8) || (m == 8 && ! (x == 11)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && ! (m == 7)) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 2) || (m == 2 && ! (x == 11)))) && ! (m == 6)) && ! (x == 10)) && ! (m == 4)) && (! (m == 2) || (m == 2 && ! (x == 13)))) && ! (x == 7)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && ! (m == 3)) && (! (m == 0) || (m == 0 && ! (x == 13)))) && ! (m == 5)) && m == 1) && x == 8)) || ((((((((((((((((((((((((((((((((((((((((((((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 6) || (m == 6 && ! (x == 10)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 12)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 11)))) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 10)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 2) || (m == 2 && ! (x == 11)))) && (! (m == 6) || (m == 6 && ! (x == 8)))) && (! (m == 5) || (m == 5 && ! (x == 10)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 11)))) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 4) || (m == 4 && ! (x == 11)))) && (! (m == 3) || (m == 3 && ! (x == 13)))) && (! (m == 1) || (m == 1 && ! (x == 10)))) && (! (m == 4) || (m == 4 && ! (x == 8)))) && (! (m == 2) || (m == 2 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 11)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && ! (m == 9)) && (! (m == 3) || (m == 3 && ! (x == 10)))) && ! (m == 7)) && (! (m == 5) || (m == 5 && ! (x == 12)))) && (! (m == 3) || (m == 3 && ! (x == 8)))) && (! (m == 0) || (m == 0 && ! (x == 13)))) && (! (m == 5) || (m == 5 && ! (x == 8)))) && (! (m == 1) || (m == 1 && ! (x == 8)))) && m == 13) && x == 14)) || ((((((((((((((((((((! (m == 11) && ! (m == 9)) && ! (m == 6)) && ! (m == 10)) && ! (m == 12)) && ! (m == 8)) && ! (m == 7)) && ! (x == 6)) && ! (x == 10)) && ! (x == 9)) && ! (x == 11)) && ! (m == 3)) && ! (m == 2)) && (! (m == 4) || (m == 4 && ! (x == 5)))) && ! (x == 7)) && ! (x == 12)) && ! (m == 0)) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && m == 5) && x == 13)) || (((((((((((((((((((! (m == 6) || (m == 6 && ! (x == 9))) && ! (m == 4)) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && ! (m == 5)) && ! (x == 12)) && (! (m == 7) || (m == 7 && ! (x == 9)))) && ! (x == 5)) && ! (x == 13)) && ! (x == 4)) && ! (x == 11)) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 9) || (m == 9 && ! (x == 14)))) && ! (x == 10)) && (! (m == 7) || (m == 7 && ! (x == 14)))) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && m == 3) && x == 6)) || ((((((((((((((((((! (m == 6) && (! (m == 8) || (m == 8 && ! (x == 9)))) && ! (x == 12)) && ! (m == 4)) && (! (m == 7) || (m == 7 && ! (x == 9)))) && ! (x == 5)) && ! (x == 13)) && ! (x == 4)) && ! (x == 11)) && ! (m == 1)) && ! (m == 5)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && ! (x == 10)) && (! (m == 7) || (m == 7 && ! (x == 14)))) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (x == 6)) && m == 3) && x == 7)) || (((((((((((((((((((((((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 2) || (m == 2 && ! (x == 10)))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 6) || (m == 6 && ! (x == 10)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && ! (x == 12)) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 7) || (m == 7 && ! (x == 10)))) && ! (m == 4)) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 6) || (m == 6 && ! (x == 11)))) && (! (m == 8) || (m == 8 && ! (x == 10)))) && ! (m == 5)) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 7) || (m == 7 && ! (x == 9)))) && (! (m == 2) || (m == 2 && ! (x == 11)))) && (! (m == 6) || (m == 6 && ! (x == 8)))) && (! (m == 1) || (m == 1 && ! (x == 10)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && ! (x == 13)) && (! (m == 1) || (m == 1 && ! (x == 8)))) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (m == 3)) && m == 0) && x == 6)) || (((((((((((((((((((((! (m == 11) && ! (x == 12)) && ! (x == 9)) && ! (m == 9)) && ! (m == 6)) && ! (x == 6)) && ! (m == 10)) && ! (m == 12)) && ! (m == 8)) && ! (m == 7)) && ! (x == 7)) && ! (x == 11)) && ! (m == 3)) && (! (m == 1) || (m == 1 && ! (x == 10)))) && ! (x == 8)) && ! (m == 2)) && ! (x == 5)) && ! (m == 0)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (m == 5)) && m == 4) && x == 13)) || (((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && ! (x == 10)) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && ! (m == 7)) && ! (x == 4)) && ! (x == 11)) && ! (m == 6)) && ! (m == 4)) && ! (x == 13)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && ! (m == 3)) && ! (m == 5)) && ! (m == 1)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && (! (m == 0) || (m == 0 && ! (x == 6)))) && m == 2) && x == 8)) || ((((((((((((((((((((((((((((! (m == 2) || (m == 2 && ! (x == 10))) && (! (m == 9) || (m == 9 && ! (x == 10)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && ! (m == 4)) && ! (x == 12)) && ! (m == 6)) && ! (m == 8)) && (! (m == 2) || (m == 2 && ! (x == 4)))) && ! (m == 7)) && (! (m == 2) || (m == 2 && ! (x == 11)))) && ! (m == 5)) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 1) || (m == 1 && ! (x == 10)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 11)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 3) || (m == 3 && ! (x == 10)))) && (! (m == 3) || (m == 3 && ! (x == 8)))) && ! (x == 13)) && (! (m == 1) || (m == 1 && ! (x == 8)))) && (! (m == 13) || (m == 13 && ! (x == 14)))) && (! (m == 3) || (m == 3 && ! (x == 7)))) && ! (x == 6)) && (! (m == 2) || (m == 2 && ! (x == 8)))) && m == 0) && x == 9)) || (((((((((((((((((((((! (m == 8) && ! (m == 7)) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && ! (m == 9)) && ! (m == 10)) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && ! (m == 6)) && ! (m == 2)) && ! (m == 5)) && ! (m == 4)) && ! (x == 10)) && ! (m == 3)) && ! (x == 7)) && (! (m == 0) || (m == 0 && ! (x == 13)))) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && (! (m == 0) || (m == 0 && ! (x == 6)))) && (! (m == 0) || (m == 0 && ! (x == 9)))) && m == 1) && x == 11)) || (((((((((((((((((((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && ! (x == 10)) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 12)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && ! (x == 4)) && (! (m == 3) || (m == 3 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 7) || (m == 7 && ! (x == 9)))) && ! (x == 11)) && (! (m == 5) || (m == 5 && ! (x == 9)))) && (! (m == 3) || (m == 3 && ! (x == 5)))) && ! (x == 13)) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && (! (m == 5) || (m == 5 && ! (x == 12)))) && (! (m == 13) || (m == 13 && ! (x == 14)))) && (! (m == 3) || (m == 3 && ! (x == 6)))) && (! (m == 3) || (m == 3 && ! (x == 7)))) && (! (m == 0) || (m == 0 && ! (x == 6)))) && ! (x == 8)) && (! (m == 0) || (m == 0 && ! (x == 9)))) && m == 2) && x == 3)) || (((((((((((((((((((! (m == 2) && ! (m == 9)) && ! (m == 6)) && (! (m == 10) || (m == 10 && ! (x == 11)))) && ! (x == 12)) && ! (m == 7)) && ! (m == 8)) && (! (m == 4) || (m == 4 && ! (x == 7)))) && ! (m == 5)) && (! (m == 4) || (m == 4 && ! (x == 11)))) && ! (m == 1)) && (! (m == 4) || (m == 4 && ! (x == 8)))) && (! (m == 4) || (m == 4 && ! (x == 5)))) && ! (m == 3)) && ! (x == 13)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (x == 6)) && ! (x == 9)) && m == 0) && x == 10)) || (((((((((((((((((((((((((((((((((((((! (m == 8) || (m == 8 && ! (x == 11))) && (! (m == 7) || (m == 7 && ! (x == 11)))) && (! (m == 9) || (m == 9 && ! (x == 11)))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && ! (x == 12)) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 6) || (m == 6 && ! (x == 11)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 2) || (m == 2 && ! (x == 11)))) && (! (m == 6) || (m == 6 && ! (x == 8)))) && (! (m == 5) || (m == 5 && ! (x == 11)))) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 4) || (m == 4 && ! (x == 11)))) && (! (m == 4) || (m == 4 && ! (x == 8)))) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 11)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && (! (m == 3) || (m == 3 && ! (x == 8)))) && ! (x == 13)) && (! (m == 5) || (m == 5 && ! (x == 8)))) && (! (m == 1) || (m == 1 && ! (x == 8)))) && (! (m == 13) || (m == 13 && ! (x == 14)))) && (! (m == 3) || (m == 3 && ! (x == 7)))) && ! (x == 6)) && (! (m == 2) || (m == 2 && ! (x == 8)))) && ! (x == 9)) && (! (m == 1) || (m == 1 && ! (x == 11)))) && (! (m == 2) || (m == 2 && ! (x == 3)))) && ! (x == 10)) && m == 0) && x == 2)) || (((((((((((((((((((! (m == 9) && ! (x == 10)) && ! (m == 7)) && ! (m == 11)) && ! (m == 10)) && ! (m == 4)) && ! (m == 0)) && ! (m == 6)) && ! (m == 8)) && ! (x == 4)) && ! (m == 3)) && ! (x == 11)) && ! (x == 13)) && (! (m == 1) || (m == 1 && ! (x == 7)))) && ! (m == 5)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (x == 8)) && ! (x == 3)) && m == 2) && x == 12)) || ((((((((((((((((((! (m == 8) && ! (m == 7)) && ! (m == 9)) && ! (m == 10)) && ! (x == 12)) && ! (m == 6)) && ! (m == 2)) && ! (m == 5)) && ! (m == 4)) && ! (m == 3)) && ! (x == 13)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (x == 6)) && ! (x == 9)) && ! (m == 1)) && ! (x == 10)) && ! (x == 2)) && m == 0) && x == 11)) || (((((((((((((((((((! (m == 2) && ! (m == 9)) && ! (m == 6)) && ! (x == 12)) && ! (x == 9)) && ! (m == 7)) && ! (x == 6)) && ! (m == 8)) && ! (x == 7)) && ! (m == 5)) && ! (x == 11)) && ! (m == 1)) && ! (x == 8)) && ! (x == 5)) && ! (m == 3)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (x == 13)) && ! (m == 0)) && m == 4) && x == 10)) || (((((((((((((((((((((((! (x == 12) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 6) || (m == 6 && ! (x == 8)))) && ! (m == 3)) && ! (m == 4)) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && ! (x == 13)) && (! (m == 5) || (m == 5 && ! (x == 8)))) && (! (m == 1) || (m == 1 && ! (x == 8)))) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (x == 6)) && (! (m == 2) || (m == 2 && ! (x == 8)))) && ! (x == 9)) && (! (m == 2) || (m == 2 && ! (x == 3)))) && ! (x == 10)) && ! (x == 2)) && ! (x == 11)) && m == 0) && x == 5)) || (((((((((((((((((((((((((((! (x == 12) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 6) || (m == 6 && ! (x == 8)))) && (! (m == 4) || (m == 4 && ! (x == 8)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && (! (m == 3) || (m == 3 && ! (x == 8)))) && ! (x == 13)) && (! (m == 5) || (m == 5 && ! (x == 8)))) && (! (m == 1) || (m == 1 && ! (x == 8)))) && (! (m == 13) || (m == 13 && ! (x == 14)))) && (! (m == 3) || (m == 3 && ! (x == 7)))) && ! (x == 6)) && (! (m == 2) || (m == 2 && ! (x == 8)))) && ! (x == 9)) && (! (m == 2) || (m == 2 && ! (x == 3)))) && ! (x == 10)) && ! (x == 2)) && ! (x == 11)) && ! (x == 5)) && m == 0) && x == 1)) || ((((((((((((((((((((! (x == 10) && (! (m == 6) || (m == 6 && ! (x == 9)))) && ! (m == 4)) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && ! (m == 5)) && ! (x == 4)) && (! (m == 7) || (m == 7 && ! (x == 9)))) && ! (x == 11)) && ! (x == 13)) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (m == 3)) && ! (m == 0)) && ! (x == 8)) && ! (x == 3)) && ! (x == 12)) && m == 2) && x == 6)) || ((((((((((((((((((((((((((! (x == 12) && (! (m == 6) || (m == 6 && ! (x == 7)))) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 6) || (m == 6 && ! (x == 8)))) && (! (m == 4) || (m == 4 && ! (x == 8)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && (! (m == 3) || (m == 3 && ! (x == 8)))) && ! (x == 13)) && (! (m == 5) || (m == 5 && ! (x == 8)))) && (! (m == 1) || (m == 1 && ! (x == 8)))) && (! (m == 13) || (m == 13 && ! (x == 14)))) && (! (m == 3) || (m == 3 && ! (x == 7)))) && ! (x == 6)) && ! (x == 9)) && ! (m == 2)) && ! (x == 10)) && ! (x == 2)) && ! (x == 11)) && ! (x == 5)) && ! (x == 1)) && m == 0) && x == 3)) || (((((((((((((((((((! (m == 4) && ! (m == 6)) && ! (m == 8)) && ! (x == 12)) && ! (m == 7)) && ! (m == 5)) && ! (x == 5)) && ! (x == 13)) && ! (x == 4)) && ! (x == 11)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && ! (x == 10)) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (x == 6)) && ! (x == 7)) && ! (m == 0)) && (! (m == 2) || (m == 2 && ! (x == 3)))) && m == 3) && x == 9)) || ((((((((((((((((((((((((((((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 12)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 7) || (m == 7 && ! (x == 13)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 12)))) && (! (m == 7) || (m == 7 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 13)))) && ! (x == 10)) && (! (m == 2) || (m == 2 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && ! (x == 7)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && (! (m == 5) || (m == 5 && ! (x == 12)))) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && (! (m == 5) || (m == 5 && ! (x == 13)))) && (! (m == 3) || (m == 3 && ! (x == 6)))) && (! (m == 4) || (m == 4 && ! (x == 13)))) && ! (x == 11)) && (! (m == 2) || (m == 2 && ! (x == 3)))) && ! (m == 0)) && (! (m == 2) || (m == 2 && ! (x == 12)))) && (! (m == 2) || (m == 2 && ! (x == 6)))) && (! (m == 3) || (m == 3 && ! (x == 9)))) && m == 1) && x == 2)) || ((((((((((((((((((((((((((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 13)))) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 0) || (m == 0 && ! (x == 12)))) && (! (m == 9) || (m == 9 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 13)))) && (! (m == 6) || (m == 6 && ! (x == 12)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 10) || (m == 10 && ! (x == 13)))) && (! (m == 12) || (m == 12 && ! (x == 13)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 8) || (m == 8 && ! (x == 13)))) && (! (m == 7) || (m == 7 && ! (x == 13)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && ! (m == 2)) && (! (m == 7) || (m == 7 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && ! (x == 10)) && (! (m == 4) || (m == 4 && ! (x == 5)))) && ! (m == 3)) && ! (x == 7)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && (! (m == 5) || (m == 5 && ! (x == 12)))) && (! (m == 0) || (m == 0 && ! (x == 13)))) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && (! (m == 5) || (m == 5 && ! (x == 13)))) && (! (m == 0) || (m == 0 && ! (x == 6)))) && (! (m == 4) || (m == 4 && ! (x == 13)))) && (! (m == 0) || (m == 0 && ! (x == 9)))) && ! (x == 11)) && (! (m == 0) || (m == 0 && ! (x == 5)))) && (! (m == 0) || (m == 0 && ! (x == 1)))) && (! (m == 0) || (m == 0 && ! (x == 3)))) && ! (x == 2)) && m == 1) && x == 4)) || ((((((((((((((((((((((((((((((((((((! (x == 11) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && ! (x == 9)) && ! (x == 13)) && ! (x == 10)) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 6) || (m == 6 && ! (x == 8)))) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 4) || (m == 4 && ! (x == 8)))) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && ! (m == 9)) && ! (m == 7)) && (! (m == 3) || (m == 3 && ! (x == 8)))) && (! (m == 5) || (m == 5 && ! (x == 8)))) && (! (m == 1) || (m == 1 && ! (x == 8)))) && ! (m == 13)) && (! (m == 3) || (m == 3 && ! (x == 6)))) && (! (m == 3) || (m == 3 && ! (x == 7)))) && (! (m == 0) || (m == 0 && ! (x == 6)))) && (! (m == 2) || (m == 2 && ! (x == 8)))) && (! (m == 2) || (m == 2 && ! (x == 3)))) && (! (m == 0) || (m == 0 && ! (x == 2)))) && (! (m == 0) || (m == 0 && ! (x == 5)))) && (! (m == 0) || (m == 0 && ! (x == 1)))) && (! (m == 2) || (m == 2 && ! (x == 6)))) && (! (m == 0) || (m == 0 && ! (x == 3)))) && (! (m == 1) || (m == 1 && ! (x == 2)))) && (! (m == 1) || (m == 1 && ! (x == 4)))) && m == 8) && x == 14)) || ((((((((((((((((((((! (m == 11) && ! (m == 9)) && ! (m == 6)) && ! (m == 10)) && ! (m == 12)) && ! (m == 8)) && ! (m == 7)) && ! (m == 3)) && ! (x == 10)) && ! (m == 2)) && ! (x == 7)) && ! (m == 0)) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (m == 5)) && ! (m == 4)) && ! (x == 11)) && ! (x == 2)) && ! (x == 4)) && m == 1) && x == 13)) || (((((((((((((((((((((((((((((! (x == 10) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 7)))) && ! (x == 4)) && (! (m == 4) || (m == 4 && ! (x == 7)))) && ! (x == 11)) && (! (m == 5) || (m == 5 && ! (x == 9)))) && (! (m == 3) || (m == 3 && ! (x == 5)))) && ! (x == 13)) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 1) || (m == 1 && ! (x == 7)))) && (! (m == 5) || (m == 5 && ! (x == 7)))) && ! (m == 9)) && ! (m == 7)) && ! (m == 13)) && (! (m == 3) || (m == 3 && ! (x == 7)))) && ! (x == 8)) && (! (m == 0) || (m == 0 && ! (x == 9)))) && ! (x == 3)) && (! (m == 0) || (m == 0 && ! (x == 2)))) && ! (x == 12)) && (! (m == 0) || (m == 0 && ! (x == 5)))) && (! (m == 0) || (m == 0 && ! (x == 1)))) && ! (x == 6)) && (! (m == 3) || (m == 3 && ! (x == 9)))) && (! (m == 1) || (m == 1 && ! (x == 2)))) && ! (m == 8)) && m == 2) && x == 14)) || ((((((((((((((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 12)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 7) || (m == 7 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && ! (m == 3)) && ! (x == 10)) && ! (m == 4)) && ! (x == 7)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && (! (m == 5) || (m == 5 && ! (x == 12)))) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (x == 11)) && (! (m == 2) || (m == 2 && ! (x == 3)))) && (! (m == 2) || (m == 2 && ! (x == 12)))) && ! (m == 0)) && (! (m == 2) || (m == 2 && ! (x == 6)))) && ! (x == 2)) && ! (x == 4)) && (! (m == 8) || (m == 8 && ! (x == 14)))) && ! (x == 13)) && (! (m == 2) || (m == 2 && ! (x == 14)))) && m == 1) && x == 5)) || ((((((((((((((((((((((((((((((((((! (m == 9) || (m == 9 && ! (x == 12))) && (! (m == 7) || (m == 7 && ! (x == 12)))) && (! (m == 11) || (m == 11 && ! (x == 12)))) && (! (m == 10) || (m == 10 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 9)))) && (! (m == 6) || (m == 6 && ! (x == 12)))) && (! (m == 8) || (m == 8 && ! (x == 12)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 8) || (m == 8 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 6)))) && (! (m == 3) || (m == 3 && ! (x == 12)))) && (! (m == 7) || (m == 7 && ! (x == 9)))) && (! (m == 5) || (m == 5 && ! (x == 9)))) && ! (x == 10)) && ! (x == 7)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && (! (m == 5) || (m == 5 && ! (x == 12)))) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && (! (m == 3) || (m == 3 && ! (x == 6)))) && ! (x == 11)) && ! (m == 2)) && ! (m == 0)) && (! (m == 3) || (m == 3 && ! (x == 9)))) && ! (x == 2)) && ! (x == 4)) && (! (m == 8) || (m == 8 && ! (x == 14)))) && ! (x == 13)) && ! (x == 5)) && m == 1) && x == 3)) || ((((((((((((((((((((((((((((! (x == 10) && ! (x == 9)) && ! (x == 13)) && ! (x == 12)) && (! (m == 4) || (m == 4 && ! (x == 6)))) && ! (x == 7)) && ! (x == 11)) && (! (m == 5) || (m == 5 && ! (x == 6)))) && ! (x == 8)) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && ! (m == 9)) && ! (m == 7)) && ! (m == 13)) && (! (m == 3) || (m == 3 && ! (x == 6)))) && (! (m == 0) || (m == 0 && ! (x == 6)))) && (! (m == 0) || (m == 0 && ! (x == 2)))) && (! (m == 0) || (m == 0 && ! (x == 5)))) && (! (m == 0) || (m == 0 && ! (x == 1)))) && (! (m == 0) || (m == 0 && ! (x == 3)))) && (! (m == 1) || (m == 1 && ! (x == 2)))) && (! (m == 1) || (m == 1 && ! (x == 4)))) && ! (m == 8)) && ! (m == 2)) && (! (m == 1) || (m == 1 && ! (x == 5)))) && (! (m == 1) || (m == 1 && ! (x == 3)))) && m == 6) && x == 14)) || ((((((((((((((((((((((((! (x == 12) && ! (m == 6)) && (! (m == 7) || (m == 7 && ! (x == 8)))) && (! (m == 2) || (m == 2 && ! (x == 4)))) && ! (m == 4)) && ! (m == 1)) && ! (m == 5)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && ! (x == 13)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (m == 3)) && ! (x == 6)) && (! (m == 2) || (m == 2 && ! (x == 8)))) && ! (x == 9)) && ! (x == 10)) && ! (x == 2)) && ! (x == 11)) && ! (x == 5)) && ! (x == 1)) && ! (x == 3)) && (! (m == 8) || (m == 8 && ! (x == 14)))) && (! (m == 2) || (m == 2 && ! (x == 14)))) && m == 0) && x == 7)) || ((((((((((((((((((((((((((! (x == 6) && ! (x == 10)) && ! (x == 9)) && ! (x == 11)) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && ! (x == 7)) && ! (m == 9)) && ! (m == 7)) && ! (x == 12)) && ! (x == 8)) && ! (m == 13)) && ! (x == 13)) && (! (m == 0) || (m == 0 && ! (x == 2)))) && (! (m == 0) || (m == 0 && ! (x == 5)))) && (! (m == 0) || (m == 0 && ! (x == 1)))) && (! (m == 0) || (m == 0 && ! (x == 3)))) && (! (m == 1) || (m == 1 && ! (x == 2)))) && (! (m == 1) || (m == 1 && ! (x == 4)))) && ! (m == 8)) && ! (m == 2)) && (! (m == 1) || (m == 1 && ! (x == 5)))) && (! (m == 1) || (m == 1 && ! (x == 3)))) && ! (m == 6)) && m == 5) && x == 14)) || ((((((((((((((((((((! (x == 10) && ! (m == 4)) && ! (m == 6)) && ! (m == 8)) && ! (x == 4)) && ! (m == 7)) && ! (x == 11)) && ! (m == 5)) && ! (x == 13)) && (! (m == 1) || (m == 1 && ! (x == 7)))) && ! (x == 8)) && ! (m == 0)) && ! (x == 3)) && ! (x == 12)) && ! (x == 6)) && ! (m == 3)) && (! (m == 1) || (m == 1 && ! (x == 2)))) && ! (x == 14)) && (! (m == 1) || (m == 1 && ! (x == 5)))) && m == 2) && x == 9)) || ((((((((((((((((((((((! (m == 9) && ! (m == 7)) && ! (m == 11)) && ! (m == 10)) && ! (m == 4)) && ! (m == 0)) && ! (m == 6)) && ! (m == 8)) && ! (m == 3)) && ! (x == 10)) && ! (x == 7)) && ! (m == 5)) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (x == 11)) && ! (m == 2)) && ! (x == 2)) && ! (x == 4)) && ! (x == 13)) && ! (x == 5)) && ! (x == 3)) && m == 1) && x == 12)) || ((((((((((((((((((((((((! (x == 12) && (! (m == 4) || (m == 4 && ! (x == 8)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && ! (m == 9)) && ! (m == 7)) && (! (m == 3) || (m == 3 && ! (x == 8)))) && ! (x == 13)) && (! (m == 1) || (m == 1 && ! (x == 8)))) && ! (m == 13)) && ! (x == 6)) && ! (x == 9)) && ! (x == 10)) && ! (x == 2)) && ! (x == 11)) && ! (x == 5)) && ! (x == 1)) && ! (x == 3)) && (! (m == 1) || (m == 1 && ! (x == 4)))) && ! (m == 8)) && ! (m == 2)) && ! (m == 6)) && ! (x == 7)) && ! (m == 5)) && m == 0) && x == 14)) || (((((((((((((((((! (x == 10) && (! (m == 6) || (m == 6 && ! (x == 7)))) && ! (x == 4)) && ! (x == 11)) && ! (m == 3)) && ! (x == 13)) && ! (m == 4)) && (! (m == 5) || (m == 5 && ! (x == 7)))) && ! (x == 8)) && ! (x == 3)) && ! (x == 12)) && ! (m == 0)) && ! (x == 6)) && ! (x == 14)) && ! (m == 1)) && ! (x == 9)) && m == 2) && x == 5)) || ((((((((((((((((((((! (x == 12) && ! (m == 7)) && ! (m == 6)) && ! (m == 4)) && ! (m == 3)) && ! (x == 13)) && ! (m == 5)) && ! (m == 1)) && ! (x == 6)) && ! (m == 2)) && ! (x == 9)) && ! (x == 10)) && ! (x == 2)) && ! (x == 11)) && ! (x == 5)) && ! (x == 1)) && ! (x == 3)) && ! (x == 7)) && ! (x == 14)) && m == 0) && x == 8)) || (((((((((((((((((((((((((! (m == 6) || (m == 6 && ! (x == 9))) && ! (m == 4)) && (! (m == 8) || (m == 8 && ! (x == 9)))) && ! (m == 5)) && (! (m == 7) || (m == 7 && ! (x == 9)))) && ! (x == 10)) && ! (x == 7)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && (! (m == 7) || (m == 7 && ! (x == 14)))) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (m == 3)) && ! (m == 0)) && ! (x == 11)) && ! (m == 2)) && ! (x == 2)) && ! (x == 4)) && (! (m == 8) || (m == 8 && ! (x == 14)))) && ! (x == 13)) && ! (x == 5)) && ! (x == 3)) && (! (m == 6) || (m == 6 && ! (x == 14)))) && ! (x == 12)) && m == 1) && x == 6)) || ((((((((((((((((((! (x == 10) && ! (m == 6)) && ! (x == 4)) && ! (m == 4)) && ! (x == 11)) && ! (x == 13)) && ! (m == 1)) && ! (m == 5)) && ! (m == 3)) && ! (x == 8)) && ! (x == 3)) && ! (x == 12)) && ! (x == 6)) && ! (x == 14)) && ! (m == 0)) && ! (x == 9)) && ! (x == 5)) && m == 2) && x == 7)) || ((((((((((((((((((((((! (m == 4) && ! (m == 6)) && ! (m == 8)) && ! (m == 7)) && ! (m == 5)) && ! (x == 10)) && ! (x == 7)) && (! (m == 9) || (m == 9 && ! (x == 14)))) && ! (x == 8)) && (! (m == 13) || (m == 13 && ! (x == 14)))) && ! (m == 0)) && ! (x == 11)) && ! (m == 3)) && ! (x == 2)) && ! (x == 4)) && ! (x == 13)) && ! (x == 5)) && ! (x == 3)) && ! (m == 2)) && ! (x == 12)) && ! (x == 6)) && m == 1) && x == 9)) || (((((((((((((((((((((! (x == 10) && ! (x == 7)) && ! (m == 9)) && ! (m == 7)) && ! (x == 8)) && ! (m == 13)) && ! (x == 11)) && ! (x == 2)) && ! (x == 4)) && ! (m == 8)) && ! (x == 13)) && ! (m == 2)) && ! (x == 5)) && ! (x == 3)) && ! (m == 6)) && ! (m == 5)) && ! (x == 12)) && ! (m == 0)) && ! (x == 6)) && ! (x == 9)) && m == 1) && x == 14)) || ((((((((((((((((((((((((((((! (x == 12) && ! (x == 13)) && (! (m == 10) || (m == 10 && ! (x == 11)))) && (! (m == 4) || (m == 4 && ! (x == 9)))) && (! (m == 4) || (m == 4 && ! (x == 6)))) && (! (m == 4) || (m == 4 && ! (x == 7)))) && (! (m == 3) || (m == 3 && ! (x == 5)))) && (! (m == 4) || (m == 4 && ! (x == 11)))) && (! (m == 4) || (m == 4 && ! (x == 8)))) && (! (m == 4) || (m == 4 && ! (x == 5)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 11)))) && ! (m == 9)) && (! (m == 3) || (m == 3 && ! (x == 10)))) && ! (m == 7)) && (! (m == 3) || (m == 3 && ! (x == 8)))) && ! (m == 13)) && (! (m == 3) || (m == 3 && ! (x == 6)))) && (! (m == 3) || (m == 3 && ! (x == 7)))) && (! (m == 4) || (m == 4 && ! (x == 10)))) && (! (m == 3) || (m == 3 && ! (x == 9)))) && ! (m == 8)) && ! (m == 2)) && ! (m == 6)) && ! (m == 5)) && ! (m == 0)) && ! (m == 1)) && m == 11) && x == 14)) || (((((((((((((((((! (x == 12) && (! (m == 2) || (m == 2 && ! (x == 4)))) && (! (m == 3) || (m == 3 && ! (x == 4)))) && ! (x == 13)) && ! (x == 6)) && ! (x == 9)) && ! (x == 10)) && ! (x == 2)) && ! (x == 11)) && ! (x == 5)) && ! (x == 1)) && ! (x == 3)) && (! (m == 1) || (m == 1 && ! (x == 4)))) && ! (x == 7)) && ! (x == 14)) && ! (x == 8)) && m == 0) && x == 0)) || (((((((((((((((((((((! (x == 12) && ! (x == 5)) && ! (x == 13)) && ! (x == 4)) && ! (x == 11)) && ! (m == 9)) && ! (x == 10)) && ! (m == 7)) && ! (x == 8)) && ! (m == 13)) && ! (x == 6)) && ! (x == 7)) && ! (x == 9)) && ! (m == 8)) && ! (m == 2)) && ! (m == 6)) && ! (m == 5)) && ! (m == 0)) && ! (m == 1)) && ! (m == 11)) && m == 3) && x == 14)) || ((((((((((((((((((! (x == 12) && ! (m == 2)) && ! (m == 3)) && ! (x == 13)) && ! (x == 6)) && ! (x == 9)) && ! (x == 10)) && ! (x == 2)) && ! (x == 11)) && ! (x == 5)) && ! (x == 1)) && ! (x == 3)) && ! (m == 1)) && ! (x == 7)) && ! (x == 14)) && ! (x == 8)) && ! (x == 0)) && m == 0) && x == 4)) || (((((((((((((((((((((! (x == 12) && ! (x == 9)) && ! (x == 6)) && ! (x == 7)) && ! (x == 11)) && ! (x == 8)) && ! (x == 5)) && ! (m == 9)) && ! (m == 7)) && ! (m == 13)) && ! (x == 13)) && ! (x == 10)) && ! (m == 8)) && ! (m == 2)) && ! (m == 6)) && ! (m == 5)) && ! (m == 0)) && ! (m == 1)) && ! (m == 11)) && ! (m == 3)) && m == 4) && x == 14)) || (((((((((((((((((! (m == 10) || (m == 10 && ! (x == 12))) && (! (m == 10) || (m == 10 && ! (x == 11)))) && ! (x == 13)) && ! (m == 9)) && ! (m == 7)) && ! (m == 13)) && ! (m == 8)) && ! (m == 2)) && ! (m == 6)) && ! (m == 5)) && ! (m == 0)) && ! (m == 1)) && ! (m == 11)) && ! (m == 3)) && ! (m == 4)) && m == 12) && x == 14)) || (((((((((((((((((! (x == 12) && ! (x == 11)) && ! (x == 13)) && ! (m == 9)) && ! (m == 7)) && ! (m == 13)) && ! (m == 8)) && ! (m == 2)) && ! (m == 6)) && ! (m == 5)) && ! (m == 0)) && ! (m == 1)) && ! (m == 11)) && ! (m == 3)) && ! (m == 4)) && ! (m == 12)) && m == 10) && x == 14) (../plain/gj2007b.i:32:2-32:11)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (../plain/gj2007b.i:14:1-16:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 17
  dead: 2 (2 in uncalled functions)
  total lines: 19
[Warning][Deadcode][CWE-571] condition 'm >= 0' (possibly inserted by CIL) is always true (../plain/gj2007b.i:34:5-34:42)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (../plain/gj2007b.i:12:73-12:74)

runtime: 00:00:10.173
vars: 59, evals: 66

|rho|=60
|called|=0
|stable|=60
|infl|=56
|wpoint|=1
|side_dep|=17
|side_infl|=33
|var_messages|=2
|rho_write|=22
|dep|=41
Found 6 contexts for 4 functions. Top 5 functions:
2	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
2	contexts for entry state of __VERIFIER_assert (2023) on ../plain/gj2007b.i:17:1-22:1
1	contexts for entry state of main (2027) on ../plain/gj2007b.i:24:1-37:1
1	contexts for entry state of reach_error (2015) on ../plain/gj2007b.i:12:1-12:159

Memory statistics: total=2658.75MB, max=100.66MB, minor=2654.56MB, major=386.80MB, promoted=382.61MB
    minor collections=1277  major collections=27 compactions=0


runtime: 00:00:20.182
vars: 59, evals: 66

|rho|=60
|called|=0
|stable|=60
|infl|=56
|wpoint|=1
|side_dep|=17
|side_infl|=33
|var_messages|=2
|rho_write|=22
|dep|=41
Found 6 contexts for 4 functions. Top 5 functions:
2	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
2	contexts for entry state of __VERIFIER_assert (2023) on ../plain/gj2007b.i:17:1-22:1
1	contexts for entry state of main (2027) on ../plain/gj2007b.i:24:1-37:1
1	contexts for entry state of reach_error (2015) on ../plain/gj2007b.i:12:1-12:159

Memory statistics: total=2962.96MB, max=100.66MB, minor=2958.76MB, major=395.08MB, promoted=390.88MB
    minor collections=1423  major collections=28 compactions=0


runtime: 00:00:30.205
vars: 59, evals: 66

|rho|=60
|called|=0
|stable|=60
|infl|=56
|wpoint|=1
|side_dep|=17
|side_infl|=33
|var_messages|=2
|rho_write|=22
|dep|=41
Found 6 contexts for 4 functions. Top 5 functions:
2	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
2	contexts for entry state of __VERIFIER_assert (2023) on ../plain/gj2007b.i:17:1-22:1
1	contexts for entry state of main (2027) on ../plain/gj2007b.i:24:1-37:1
1	contexts for entry state of reach_error (2015) on ../plain/gj2007b.i:12:1-12:159

Memory statistics: total=3256.57MB, max=100.66MB, minor=3252.36MB, major=403.29MB, promoted=399.08MB
    minor collections=1563  major collections=28 compactions=0


runtime: 00:00:40.214
vars: 59, evals: 66

|rho|=60
|called|=0
|stable|=60
|infl|=56
|wpoint|=1
|side_dep|=17
|side_infl|=33
|var_messages|=2
|rho_write|=22
|dep|=41
Found 6 contexts for 4 functions. Top 5 functions:
2	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
2	contexts for entry state of __VERIFIER_assert (2023) on ../plain/gj2007b.i:17:1-22:1
1	contexts for entry state of main (2027) on ../plain/gj2007b.i:24:1-37:1
1	contexts for entry state of reach_error (2015) on ../plain/gj2007b.i:12:1-12:159

Memory statistics: total=3538.85MB, max=100.66MB, minor=3534.63MB, major=410.93MB, promoted=406.71MB
    minor collections=1697  major collections=28 compactions=0


runtime: 00:00:50.227
vars: 59, evals: 66

|rho|=60
|called|=0
|stable|=60
|infl|=56
|wpoint|=1
|side_dep|=17
|side_infl|=33
|var_messages|=2
|rho_write|=22
|dep|=41
Found 6 contexts for 4 functions. Top 5 functions:
2	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
2	contexts for entry state of __VERIFIER_assert (2023) on ../plain/gj2007b.i:17:1-22:1
1	contexts for entry state of main (2027) on ../plain/gj2007b.i:24:1-37:1
1	contexts for entry state of reach_error (2015) on ../plain/gj2007b.i:12:1-12:159

Memory statistics: total=3807.92MB, max=100.66MB, minor=3803.71MB, major=418.19MB, promoted=413.97MB
    minor collections=1826  major collections=29 compactions=0


runtime: 00:01:00.247
vars: 59, evals: 66

|rho|=60
|called|=0
|stable|=60
|infl|=56
|wpoint|=1
|side_dep|=17
|side_infl|=33
|var_messages|=2
|rho_write|=22
|dep|=41
Found 6 contexts for 4 functions. Top 5 functions:
2	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
2	contexts for entry state of __VERIFIER_assert (2023) on ../plain/gj2007b.i:17:1-22:1
1	contexts for entry state of main (2027) on ../plain/gj2007b.i:24:1-37:1
1	contexts for entry state of reach_error (2015) on ../plain/gj2007b.i:12:1-12:159

Memory statistics: total=4086.02MB, max=100.66MB, minor=4081.78MB, major=426.06MB, promoted=421.82MB
    minor collections=1959  major collections=29 compactions=0

