vector<string> Generator::step_generateMP() {
    vector <string> deduc1;
    deduc1.emplace_back("!B->(A->B)->!B");
    deduc1.emplace_back("!B");
    deduc1.emplace_back("(A->B)->!B");
    deduc1.emplace_back("((A->B)->!B)->((A->B)->!!B)->!(A->B))");
    deduc1.emplace_back("((A->B)->!!B)->!(A->B))");
    vector <string> deduc;
    deduc.emplace_back("(A->B)->(A->!B)->!A");
    deduc.emplace_back("A->B");
    deduc.emplace_back("(A->!B)->!A");
    deduc.emplace_back("!B->(A->!B)");
    deduc.emplace_back("!B");
    deduc.emplace_back("A->!B");
    deduc.emplace_back("!A");
    deduction(deduc, "!B", "!A");
    deduction(deduc, "A->B", "!B->!A");
    vector<string> deduc2;
    deduc2.emplace_back("((!B->!A)->(!B->!!A)->!!B)");
    deduc2.emplace_back("(!B->!A)");
    deduc2.emplace_back("((!B->!!A)->!!B)");
    deduc2.emplace_back("(!!A->(!B->!!A))");
    deduc2.emplace_back("(!!A)");
    deduc2.emplace_back("(!B->!!A)");
    deduc2.emplace_back("(!!B)");
    deduction(deduc2, "!!A", "!!B");
    deduction(deduc2, "(!B -> !A)", "(!!A->!!B)");
    deduc.emplace_back("(A->B)");
    deduc.emplace_back("(!B->!A)");
    for (auto& st: deduc2) {
        deduc.emplace_back(st);
    }
    deduc.emplace_back("(!!A->!!B)");
    deduc.emplace_back("!!A");
    deduc.emplace_back("!!B");
    deduction(deduc, "A->B", "!!B");
    for (auto& st: deduc) {
        deduc1.emplace_back(st);
    }
    deduc1.emplace_back("!(A->B)");
    deduction(deduc1, "!B", "!(A->B)");
    vector<string> final_mp;
    final_mp.emplace_back("!!(A->B)");
    final_mp.emplace_back("!!A");
    final_mp.emplace_back("((!(B)->(!(A->B)))->(!(B)->!!(A->B))->!!B)");
    final_mp.emplace_back("(!!(A->B)->!B->!!(A->B))");
    final_mp.emplace_back("!(B)->!(!(A->B))");
    for (auto& st: deduc1) {
        final_mp.emplace_back(st);
    }
    final_mp.emplace_back("(!(B)->!!(A->B))->!!B");
    final_mp.emplace_back("!!B");
    return final_mp;
}

void Generator::deduction(vector<string> &proof, string A, string B) {
    vector<string> ans;
    ProofCherker checker;
    ExpressionParser parser;
    A = "(" + A + ")";
    string strA = parser.parse(A)->toString();
    vector<string> parsed;
    parsed.reserve(proof.size());
    for (int i = 0; i < proof.size(); i++) {
        parsed.push_back(parser.parse(proof[i])->toString());
    }
    for (int i = 0; i < proof.size(); i++) {
        if (parsed[i] == strA) {
            string help3 = "((" + A + ")->(" + A + "))";
            string help1 = "((" + A + ")->(" + help3 + "))";
            string help2 = "((" + A + ")->((" + help3 + ")->(" + A + ")))";
            ans.emplace_back("((" + A + ")->(" + help3 + "))");
            ans.emplace_back("((" + help1 + ")->(" + help2 + ")->(" + help3 + "))");
            ans.emplace_back("((" + help2 + ")->(" + help3 + "))");
            ans.emplace_back(help2);
            ans.emplace_back(help3);
        } else {
            bool flag = false;
            for (int j = 0; j < i; j++) {
                string modus = "(" + parsed[j] + "->" + parsed[i] + ")";
                //modus = parser.parse(modus)->toString();
                for (int q = 0; q < i; q++) {
                    if (modus == parsed[q]) {
                        flag = true;
                        string b;
                        ans.emplace_back("(((" + A + ")->(" + parsed[j] + "))->(((" + A + ")->((" + parsed[j] + ")->(" + parsed[i] +
                                         ")))->((" + A + ")->(" + parsed[i] + "))");
                        ans.emplace_back("((((" + A + ")->((" + parsed[j] + ")->(" + parsed[i] + ")))->((" + A + ")->(" + parsed[i] + "))))");
                        ans.emplace_back("((" + A + ")->(" + parsed[i] + "))");
                        break;
                    }
                }
                if (flag) break;
            }
            if (!flag) {
                string b;
                ans.emplace_back(parsed[i]);
                ans.emplace_back("((" + parsed[i] + ")->((" + A + ")->(" + parsed[i] + ")))");
                ans.emplace_back("((" + A + ")->(" + parsed[i] + "))");
            }
        }
    }
    proof = ans;
}