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