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(v_12,axiom,
    ( ~(po=ut) & ~(po=st) & ~(po=ct)& ~(po=pa) & ~(po=so) & ~(po=ne) &
~(ut=st)  & ~(ut=ct)& ~(ut=pa) & ~(ut=so) & ~(ut=ne) &
 ~(st=ct)& ~(st=pa) & ~(st=so) & ~(st=ne) &
~(ct=pa) & ~(ct=so) & ~(ct=ne) &
 ~(pa=so) & ~(pa=ne) &
 ~(so=ne) 
 )).


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