AU - cv3

Pohadka: 
Ostrov, lide jsou poctivci/lhari,
 k tomu mohou byt jeste elitni. 
Existuji tam kluby, elitnaci maji sve kluby.
 Existuji doplnkove kluby, takze kazdy, kdo neni v klubu Milujeme_Justina_Biebera_A_Nesnasime_Mrkew je v klubu Justin_Bieber_Je_Tulpas_A_Mrkev_Si_Strkam_Uplne_Vsude. 
Ke kazdemu klubu existuje alespon jeden clovek, ktery tvrdi, ze je jeho clenem. 

Mame dokazat, zda-li existuje alespon jeden neelitni poctivec. 

Predikaty: 
c(X)...X je clovek, ~c(X) znaci klub
e(X)...elitni
p(X)...poctivec X, ~p(X)..lhar X
k(C,K)...C je clenem klubu K


Axiomy:

  * Elitni poctivci tvori klub: 
fof(el_poc_klub,axiom,
(
?[x] (
       ~c(x) & ![y] (  c(y) & p(y) & e(y)  )
     )
<=> 
k(y,x)

--nebo jen--
c(y) => ((p(y) & e(y)) <=> k(y,x))
--end--

)
).




* Elitni padousi tvori klub (jen pridat 1 negaci): 
fof(el_pad_klub,axiom,
(
?[x] (
       ~c(x) & ![y] (  c(y) & ~p(y) & e(y)  )
     )
<=> 
k(y,x)

)
).



* Kazdy clovek c, kdo neni v klubu Kl, je v klubu Dopl: 
fof(dopln_klub,axiom,
(
![Kl] (~c(Kl) ?[Dopl] ( ~c(Dopl) ![c]( c(c)
  ~k(c,Kl) <=> k(c,Dopl)
 ) ))
)
).


* Ke kazdemu klubu k existuje clovek c, ktery tvrdi, ze je jeho clenem:
fof(clen,axiom,
(
![k] (~c(k) ?[c] ( c(c) & 
(
(p(c) & k(c,k))
|
(~p(c) & ~k(c,k))
) 
))

--nebo--
p(c) <=> k(c,k)
--end--
)
).


* Otazka: Existuje jeden neelitni poctivec?  
fof(neel_poc,conjecture,
(
?[x] (c(x) & p(x) & ~e(x) )
)
).

Nacpat to do solveru (pouzit EP) a doufat.