Inconsistency with MONA

[weltoph]

The following file describes an instance of the Dining Philosophers problem where all philosophers share two global forks which they all take in the same order, i.e. first the one indexed by 0 and then the one indexed by 1. The forks have two states: free(F) and busy(B) while the philosophers have three states waiting(W), hungry(H) [representing: already grabbed the first fork] and eating(E) [representing: holding both forks]. The following file defines traps, i.e. collection of places in a Petrinet which once marked can never be unmarked again, by the predicate trap where a set is a five-tuple (XW, XH, XE, XF, XB) of monadic second-order variables and the place "philosopher i is hungry" is part of the set if and only if i in XH holds.

The file can be found here: https://gist.github.com/weltoph/077a49341da4402ad26ba332d2e61b28

According to MONA v1.4-17 this formula is unsatisfiable while gaston considers it satisfiable with the following example:

[*] Printing satisfying example of (56) length
n  : 00100000000100101100000010110000001000001000100100000101
MW : 00110000000111101111000010111111101111101110110111100111
MH : 00111111110111101111111111111111111111111111111111111111
ME : 11111111110011101111111010111111111111111111111111111111
MF : 10101011111000110001001101110001111000110101001100111011
MB : 01000110111011011011011111111011110101111011011011111111
IW : 11111111111111111111111111111111111111111011111111111111
IH : 11111111111111111111111111111111111111111011111111111111
IE : 11111111111011111111111111111111111111111011111111111111
IF : 11011111111111011001111111101111111111110111111111111111
IB : 11111110111001111001111111101111110111111111111111111111

Encoding this model into MONA and asking for a trap which invalidates the marking (as done by https://gist.github.com/weltoph/0a42044a223c85d4a2c12f303c067e29)
yields the following model:

n = 2
MW = {}
MH = {}
ME = {0,1}
MF = {0}
MB = {1}
IW = {0,1}
IH = {0,1}
IE = {0,1}
IF = {0,1}
IB = {0,1}
TW = {0,1}
TH = {}
TE = {}
TF = {}
TB = {0}

Intuitively, the variables TW, TH, TE, TF, TB encode a trap. Hence I am curious why gaston considers above model a satisfying example.

Are there subtle differences between gaston and MONA that I am not aware of? Is this a bug?