AU cv5: Alenka a lhari

Sice to vubec nefunguje, ale aspon se to zkompiluje :P

fof(v_po,axiom,
    ( v(po)=ne )).
fof(v_ut,axiom,
    ( v(ut)=po )).
fof(v_st,axiom,
    ( v(st)=ut )).
fof(v_ct,axiom,
    ( v(ct)=st )).
fof(v_pa,axiom,
    ( v(pa)=ct )).
fof(v_so,axiom,
    ( v(so)=pa )).
fof(v_ne,axiom,
    ( v(ne)=so )).

fof(ultimatniaxiom,axiom,
    ( ! [X]: (~(v(X)=X)) )).

fof(dny,axiom,
    ( ! [D]: ((D = po) | (D = ut) | (D = st) | (D = ct) | (D = pa) | (D = so) | (D = ne))  )).

fof(lze_lef,axiom,
    ( ! [X]: (ll(X) <=> ((X = po) | (X = ut) | (X = st))) )).

fof(lze_jedn,axiom,
    ( ! [X]: (lj(X) <=> ((X = ct) | (X = pa) | (X = so))) )).

fof(tvrz,conjecture,
    ( ? [Dnes]: (( (~ll(Dnes) <~> ll(v(Dnes))) & (~lj(Dnes) <~> lj(v(Dnes)))
                 ) => (Dnes = ct))
    )
   ).