Foutmelding

Warning: Verifying and/or autocompleting input structures.

Generating an unsatisfiable subset of the given theory. Error: Third-party, non-descript error thrown. This is the merged theory: theory Tverifications : V { (! h[Heap] m[Matches] p[Player] t[Time] : (~Takes(p,h,m,t) | (Turn(p,t) & ((m > 0) & (? m1[Matches] : (Nb(h,m1,t) & (m =< m1))))))) (! t[Time] : (GameOver(t) | (1 = #[ { h[Heap] m[Matches] p[Player] : Takes(p,h,m,t) : 1 } ]))) (! p[Player] t[Time] : (Winner(p,t) <=> (Turn(p,t) & (! h[Heap] : Nb(h,0,t))))) { ! h[Heap] m[Matches] : Nb(h,m,Start) <- I_Nb(h,m). ! h[Heap] m[Matches] t[Time] : Nb(h,m,Next(t)) <- (C_Nb(h,m,t) | (Nb(h,m,t) & ~(? m1[Matches] : (C_Nb(h,m1,t) & (m ~= m1))))). ! t[Time] : GameOver(Next(t)) <- (GameOver(t) | C_GameOver(t)). } { ! dm[Matches] h[Heap] m[Matches] t[Time] : C_Nb(h,-int,int : int,t) <- (? p[Player] : (Nb(h,m,t) & Takes(p,h,dm,t))). ! t[Time] : C_GameOver(t) <- (? p[Player] : Winner(p,t)). } { ! p[Player] : Turn(p,Start) <- I_Turn(p). ! p[Player] t[Time] : Turn(p,Next(t)) <- ~Turn(p,t). } }

Searching for a model

Comments (7)