000/001

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) ;
  (
    (
      ef(NewF) = F ;
      ax(NewF) = F ;
      (neg(NewF) = F, NewNeg = true) ;

    ),
    (
      nextState(S, T, NextS),
      (
        (NewNeg = true ; 1=:=1),
        check(T, L, NextS, U, NewF, NewNeg)
      )
    )
  ), !.

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).