Ak vznikla prázdna rezolventa, tak systém nie je splniteľný, systém je kontradikcia. - tuším by to malo byť takto.
Ale problém sa ešte môže trochu zamotať, keď dokazuješ jej negáciu, čiže očakávaš prázdnu rezolventu a vtedy bude systém splniteľný.
Neviem to na sto percent, ale tak si myslím.