Параллельный метод резолюции

using System;
using System.Collections.Generic;
using System.IO;
using System.Linq;
using System.Text;
using System.Threading.Tasks;
using System.Threading;
 
namespace ParallelResolution
{
    class Program
    {
        public static readonly List<Resolution> CL = new List<Resolution>();
        public static readonly List<Thread> WaitingThreads = new List<Thread>();  // Очередь ожидающих нитей
        public static int LastSentForResolving = 0;
        public static int LastAdded;
        public static Semaphore Sem;
 
        static void Main(string[] args)
        {
            var m = Convert.ToInt32(args[1]);
            string[] s;
            Sem = new Semaphore(1, 1);
            using (var sr = new StreamReader(args[0]))
            {
                s = sr.ReadToEnd().Trim().Split(new[] { "," }, StringSplitOptions.RemoveEmptyEntries);
            }
            for (int i = 0; i < s.Length; i++)
            {
                var res = new Resolution
                {
                    Disjuncts = s[i].Split(new[] { "v" }, StringSplitOptions.RemoveEmptyEntries).ToList()
                };
                CL.Add(res);
            }
            LastAdded = CL.Count;
            var startingTime = DateTime.Now;
            var threadList = new List<Thread>();
            //Execution();
            for (int i = 0; i < m; i++)
            {
                threadList.Add(new Thread(Execution));
                threadList[i].Start();
            }
            foreach (var thread in threadList)
            {
                thread.Join();
            }
            Console.WriteLine("Time = "+(DateTime.Now-startingTime).ToString("g"));
            Console.WriteLine("Очередь дизъюнктов:");
            foreach (var resolution in CL)
            {
                foreach (var dis in resolution.Disjuncts)
                {
                    if(resolution.Disjuncts[resolution.Disjuncts.Count-1]==dis)
                        Console.Write(dis+", ");
                    else
                    {
                        Console.Write(dis+"v");
                    }
                }
            }
        }
 
        public static async void Execution()
        {
            while (true)
            {
                if (CL.Exists(res => res.Disjuncts.SequenceEqual(new[] { "empty" }.ToList())))
                    return;
                Sem.WaitOne();
                if (LastSentForResolving == LastAdded)
                {
                    Sem.Release();
                    WaitingThreads.Add(Thread.CurrentThread);
                    //Thread.CurrentThread.Suspend();
                    continue;
                }
                var number = LastSentForResolving + 1;/*
                if (number >= CL.Count)
                {
                    Console.WriteLine("Высказывание не может быть выведено из существующих дизъюнктов.");
                    Thread.CurrentThread.Abort();
                }*/
                LastSentForResolving++;
                var i = 0;
                while (true)
                {
                    if (i >= number)
                    {
                        Sem.Release();
                        break;
                    }
                    else
                    {
                        var newDisj = Resolve(CL[i].Disjuncts, CL[number].Disjuncts);
                        var oldCount = CL.Count;
                        if (!CL.Exists(res=>res.Disjuncts.SequenceEqual(newDisj)) && newDisj.Any())
                        {
                            CL.Add(new Resolution(){Disjuncts=newDisj});
                        }
                        var newCount = CL.Count;
                        LastAdded = newCount;
                        if (newCount > oldCount && WaitingThreads.Any())
                        {
                            Sem.Release();
                            var tempThread = WaitingThreads[0];
                            WaitingThreads.Remove(tempThread);
                            //tempThread.Resume();
                        }
                        else
                        {
                            i++;
                            if (CL.Exists(res => res.Disjuncts.SequenceEqual(new[] { "empty" }.ToList())))
                            {
                                Sem.Release();
                                break;
                            }
                        }
                    }
                }
                //Thread.CurrentThread.Abort();
            }
        }
 
        static List<string> Resolve(List<string> c1, List<string> c2)
        {
            var tempC1 = new List<string>();
            tempC1.AddRange(c1);
            var tempC2 = new List<string>();
            tempC2.AddRange(c2);
            var s1 = new List<string>();
            var s2 = new List<string>();
            var newDisjunkt = new List<string>();
            var have = false;
            foreach (var dis1 in tempC1)
            {
                foreach (var dis2 in tempC2)
                {
                    if (dis1 == "-" + dis2 || "-" + dis1 == dis2)
                    {
                        s1.Add(dis1);
                        s2.Add(dis2);
                        have = true;
                        break;
                    }
                    
                }
            }
            if (have)
            {
                foreach (var dis1 in s1) //удаляем контрарные пары
                {
                    tempC1.Remove(dis1);
                }
                foreach (var dis2 in s2)
                {
                    tempC2.Remove(dis2);
                }
                if (!tempC1.Any()&&!tempC2.Any()) // если оба списка после удаления контрарных пар пустые, возвращаем пустой дизъюнкт
                {
                    newDisjunkt.Add("empty");
                    return newDisjunkt;
                }
                if (tempC1.Any())
                {
                    newDisjunkt.AddRange(tempC1);
                }
                if (tempC2.Any())
                {
                    newDisjunkt.AddRange(tempC2);
                }
                return newDisjunkt; // иначе возвращаем резольвенту
            }
            return new List<string>(); // если контрарных пар не было, возвращаем пустой список, что значит перейти далее
        }
    }
 
    class Resolution
    {
        public List<string> Disjuncts;
    }
}