input rezolúció, de csak UNSAT esetre jó, egyébként végtelen

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Threading.Tasks;

namespace ConsoleApplication1
{
    class Program
    {
        // hogyan ábrázoljak egy klózt
        // pl: x1 vagy nem x2 vagy x3
        //     1           -2      3
        // x1 vagy nem x3 vagy nem x4
        // 1,-3,-4
        // ez egy int lista
        // azaz a klózokat int listával reprezentálom
        static void Main(string[] args)
        {
            List<int> klóz1 = new List<int> { 1, -2, 3 };
            List<int> klóz2 = new List<int> { 1, -3, -4 };
            List<int> klóz3 = Rezolúció(klóz1, klóz2);
            for (int i = 0; i < klóz3.Count; i++)
            {
                Console.WriteLine(klóz3[i]);
            }
            Console.ReadLine();
        }
        static int ElentétesPárokSzáma(List<int> klóz1, List<int> klóz2)
        {
            int db = 0;
            foreach(int lit in klóz1)
            {
                if (klóz2.Contains(-1 * lit)) db++;
            }
            return db;
        }
        static bool LehetERezolúció(List<int> klóz1, List<int> klóz2)
        {
            return ElentétesPárokSzáma(klóz1, klóz2) == 1;
        }
        static List<int> Rezolúció(List<int> klóz1, List<int> klóz2)
        {
            if (!LehetERezolúció(klóz1, klóz2)) return null;
            List<int> rezolvens = new List<int>();
            for (int i = 0; i < klóz1.Count; i++)
            {
                if (klóz2.Contains(-1 * klóz1[i])) continue;
                if (klóz2.Contains(+1 * klóz1[i])) continue;
                rezolvens.Add(klóz1[i]);
            }
            for (int i = 0; i < klóz2.Count; i++)
            {
                if (klóz1.Contains(-1 * klóz2[i])) continue;
                rezolvens.Add(klóz2[i]);
            }
            return rezolvens;
        }
        public bool InputRezolúció(List<List<int>> klózSzet)
        {
            if (klózSzet.Count == 0) return true; // az üres klózSzet SAT
            List<int> akt = klózSzet[0];
            while(akt.Count != 0)
            {
                bool voltE = false;
                for (int i = 0; i < klózSzet.Count; i++)
                {
                    if (LehetERezolúció(akt, klózSzet[i]))
                    {
                        akt = Rezolúció(akt, klózSzet[i]);
                        // if (!klózSzet.Cointains(új)) klózSzet.Add(új);
                        klózSzet.Add(akt);
                        voltE = true;
                        break;
                    }
                }
                if (voltE == false) return true; // kielégíthető
            }
            return false; // UNSAT
        }
    }
}