LeleLiliLuluMjauMjau

verify(Input) :-
  see(Input), read(T), read(L), read(S), read(F), seen,
  check(T, L, S, [], F, false).

check(T, L, S, U, F, Neg) :-
  verifyState(F, S, L, Neg) ;
  (
    (neg(_) = F, neg(T, L, S, U, F, Neg)) ;
    (or(_) = F , or(T, L, S, U, F, Neg)) ;
    (and(_) = F , and(T, L, S, U, F, Neg)) ;
    (ax(_) = F , ax(T, L, S, U, F, Neg)) ;
    (ag(_) = F , ag(T, L, S, U, F, Neg)) ;
    (af(_) = F , af(T, L, S, U, F, Neg)) ;
    (ex(_) = F , ex(T, L, S, U, F, Neg)) ;
    (eg(_) = F , eg(T, L, S, U, F, Neg)) ;
    (ef(_) = F , ef(T, L, S, U, F, Neg))
  ), !.

ef(T, L, S, U, F, Neg) :-
  not(member(S, U)),
  ef(NewF) = F,
  nextState(S, T, NextS),
  check(T, L, NextS, [S|U], NewF, true), !.

ax(T, L, S, U, F, Neg) :-
  not(member(S, U)),
  ax(NewF) = F,
  check(T, L, S, U, NewF, true).

neg(T, L, S, U, F, Neg) :-
  neg(NewF) = F,
  check(T, L, S, U, NewF, true).

and(T, L, S, U, F, Neg) :- !.

or(T, L, S, U, F, Neg) :- !.


verifyState(F, S, L, Neg) :-
  member([S, A], L),
  (
    (Neg = false, member(F, A)) ;
    not(member(F, A))
  ).

nextState(S, T, NextS) :-
  member([S, A], T),
  member(NextS, A).