Proba de baraj 2, problema 3
Demaonstrarea automata folosind metoda rezolutiei
Pe baza unor enunturi logice trebuie sa se demonstreze valabilitatea unei 
concluzii. Clauzele echivalente enunturilor si concluziei negate se vor citi 
dintr-un fisier text al carui nume se citeste de la tastatura. Daca exista 
mai multe demonstratii, se va prezenta una dintre ele. Demonstartia trebuie 
sa contina un numar de maxim 1000 clauze (inclusiv cele citite din fisierul 
de intrare). Daca dupa cele 1000 clauze generate demonstartia nu s-a incheiat, 
se va afissa un mesaj de eroare explicativ.
Date de intrare:
	Pe fiecare linie a fisierului se gaseste cate o clauza.
	Clauzele provenind din enunturi sunt separate printr-o linie vida de 
clauzele provenind din concluzie. Clauzele satisfac urmatoarele conditii:
- numele oricarui predicat este o litera mare;
- numele oricarei functii este o litera mica;
- numele oricarei constante este o litera mare;
- numele oricarei variabile este o litera mica;
- delimitatorii argumentelor predicatelor si functiilor sunt paranteze rotunde;
- separatorul termneilor din interiorul predicatelor si functiilor este , ;
- in locul negatiei logice se va folosi caracterul ~ ;
- in locul operatorului sau logic se va folosi caracterul | ;
- in aceste clauze nu exista nici un blanc;
- argumentele functiilor sunt numai constante sau variabile.
Date de iesire:
	In fisierul de iesire al carui nume se citeste de la tastatura, se vor 
scrie:
- clauzele reprezentand enunturile si concluzia negata (deci, cele citite din 
fisierul de intrare, numerotate in fata clauzei, numerotarea fiind separata 
de clauza printr-un blanc);
- clauzele deduse ulterior (numerotate) si numerele clauzelor folosite (in 
fata clauzei se afla numarul ei, urmat intre paranteze de numerele clauzelor 
folosite)
Observatie: Clauza vida se va nota cu caracterul '_'
Exemplu (tranzitivitatea relatiei de egalitate)
	Fie continutul fisierului de intrare:
P(A,B)
P(B,C)
~P(x,y)|~P(y,z)|P(x,z)

~P(A,C)
Continutul fisierului de iesire va putea fi
1 P(A,B)
2 P(B,C)
3 ~P(x,y)|~P(y,z)|P(x,z)
4 ~P(A,C)
5 (3,4) ~P(A,y)|~P(y,C)
6 (1,5) ~P(B,C)
7 (2,6) _
