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

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

af(T, L, S, U, F) :-
  not(member(S, U)),
  af(NewF) = F,
  (
    member([S, Nodes], T), !,
    nextState(S, T, SS),
  )


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

%For all paths, the next state must contain a valid formula
ax(T, L, S, U, F) :-
  not(member(S, U)),
  ax(NewF) = F,
  (
    member([S, Nodes], T), !,
    nextState(S, T, SS),
    setof(SS, checkFormula(L, SS, NewF), Nodes), !
  ),
  nextState(S, T, NextS),
  check(T, L, NextS, [S|U], NewF), !.

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

and(T, L, S, U, F) :- 
  and(X, Y) = F,
  (
    check(T, L, S, U, X),
    check(T, L, S, U, Y)
  ), !.

or(T, L, S, U, F) :-
  or(X, Y) = F,
  (
    check(T, L, S, U, X);
    check(T, L, S, U, Y)
  ), !.

verifyState(F, S, L) :-
  member([S, A], L),
  member(F, A).

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

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