void firstSituation(int numOfVar, expression* expr) {
    switch (numOfVar) {
        case 1:
            if (truthTable[0]){ //общедоказуемо
                vector <string> G;
                deductor(G, "!A", doc, docs[0]); // возможно, нужно поменять местами
                deductor(G, "A", doc, docs[1]);
                addEightAxiom(doc, new variable((string &) "A"), expr);
                printAnswer({}, expr, doc);
            } else {
                printAnswer({"A"}, expr, docs[1]);
            }
            break;
        case 2:
            if (truthTable[2]) {
                vector <string> G = {"B"};
                vector <expression* >tmp;
                deductor(G, "!A", tmp, docs[2]);
                deductor(G, "A", tmp, docs[3]);
                addEightAxiom(tmp, new variable((string &) "A"), expr);
                if (truthTable[1]) {
                    vector <expression*> tmp2;
                    deductor(G, "!A", tmp2, docs[0]);
                    deductor(G, "A", tmp2, docs[1]);
                    addEightAxiom(tmp2, new variable((string &) "A"), expr);
                    G.clear();
                    deductor(G, "!B", doc, tmp2);
                    deductor(G, "B", doc, tmp);
                    addEightAxiom(doc, new variable((string &) "B"), expr);
                    printAnswer({}, expr, doc);
                    return;
                }
                printAnswer({"B"}, expr, tmp);
            } else if (truthTable[1]) {
                vector <string> G = {"A"};
                deductor(G, "!B", doc, docs[1]);
                deductor(G, "B", doc, docs[3]);
                addEightAxiom(doc, new variable((string &) "B"), expr);
                printAnswer({"A"}, expr, doc);
                return;
            } else {
                printAnswer({"A", "B", "C"}, expr, docs[3]);
            }
            break;
        case 3:
            if (truthTable[6]) {
                vector <string> G = {"B", "C"};
                vector <expression* >tmp;
                deductor(G, "!A", tmp, docs[6]);
                deductor(G, "A", tmp, docs[7]);
                addEightAxiom(tmp, new variable((string &) "A"), expr);
                if (truthTable[5]) {
                    vector <expression*> tmp2;
                    deductor(G, "!A", tmp2, docs[4]);
                    deductor(G, "A", tmp2, docs[5]);
                    addEightAxiom(tmp2, new variable((string &) "A"), expr);
                    G = {"C"};
                    vector <expression*> tmp3;
                    deductor(G, "!B", tmp3, tmp2);
                    deductor(G, "B", tmp3, tmp);
                    addEightAxiom(tmp3, new variable((string &) "B"), expr);
                    if (truthTable[3]) {
                        G = {"B", "C"};
                        vector <expression*> tmp4;
                        deductor(G, "!A", tmp4, docs[2]);
                        deductor(G, "A", tmp4, docs[3]);
                        addEightAxiom(tmp4, new variable((string &) "A"), expr);
                        vector <expression*> tmp5;
                        deductor(G, "!A", tmp5, docs[0]);
                        deductor(G, "A", tmp5, docs[1]);
                        addEightAxiom(tmp5, new variable((string &) "A"), expr);
                        vector <expression *> tmp6;
                        G = {"C"};
                        deductor(G, "!B", tmp6, tmp4);
                        deductor(G, "B", tmp6, tmp5);
                        addEightAxiom(tmp6, new variable((string &) "B"), expr);
                        G.clear();
                        vector<expression*> nmp7;
                        deductor(G, "!C", doc, tmp6);
                        deductor(G, "C", doc, tmp3);
                        addEightAxiom(doc, new variable((string &) "C"), expr);
                        printAnswer({}, expr, doc);
                        return;
                    }
                    printAnswer(G, expr, tmp3);
                    return;
                }
                printAnswer(G, expr, tmp);
                return;
            }
            if (truthTable[5]) {
                vector <string> G = {"A", "C"};
                vector <expression*> tmp;
                deductor(G, "!B", tmp, docs[5]);
                deductor(G, "B", tmp, docs[7]);
                addEightAxiom(tmp, new variable((string &) "B"), expr);
                if (truthTable[3]) {
                    G = {"A", "C"};
                    vector <expression*> tmp2;
                    deductor(G, "!B", tmp2, docs[2]);
                    deductor(G, "B", tmp2, docs[4]);
                    addEightAxiom(tmp2, new variable((string &) "B"), expr);
                    G = {"A"};
                    deductor(G, "!C", doc, tmp2);
                    deductor(G, "C", doc, tmp);
                    addEightAxiom(doc, new variable((string &) "B"), expr);
                    printAnswer(G, expr, doc);
                    return;
                }
                printAnswer(G, expr, tmp);
                return;
            }
            if (truthTable[3]){
                vector <string> G = {"A", "B"};
                deductor(G, "!C", doc, docs[3]);
                deductor(G, "C", doc, docs[7]);
                addEightAxiom(doc, new variable((string &) "C"), expr);
                printAnswer(G, expr, doc);
                return;
            }
            printAnswer({"A", "B", "C"}, expr, docs[7]);
            break;
        default:
            break;
    }
}