#include <iostream>
#include <string>
#include <algorithm>
#include <set>
#include <map>
#include <unordered_set>
#include <unordered_map>
#include <vector>
#include <queue>
#include <sstream>

class god {
private :

    class operation {
    public:
        std::string operator_sign;

        virtual std::string print() = 0;

        virtual size_t hash() const = 0;

        virtual bool operator==(  operation *oper) const = 0;

        virtual bool operator!=(  operation *oper) const {
            return !(this->operator==(oper));
        }


    };

    class abstract_operaiton : public operation {
    public :
        operation *left;
        operation *right;


        abstract_operaiton(operation *left, operation *right) : left(left), right(right) {};

        std::string print() override {
            return "(" + left->print() + " " + operator_sign + " " + right->print() + ")";
        }

        size_t hash() const override {
            return left->hash() * 31 + right->hash() * 17 + (std::hash<std::string>{}(operator_sign));
        }

        bool operator==(operation *oper) const override {
            if (dynamic_cast<abstract_operaiton *> (oper) != nullptr) {
                auto *box = dynamic_cast<abstract_operaiton *> (oper);
                return operator_sign == box->operator_sign && left->operator==(box->left) &&
                       right->operator==(box->right);
            }
            return false;
        }


    };

    using AO = abstract_operaiton;
    using first = operation;

    class AND : public AO {
    public :
        AND(first *left, first *right) : abstract_operaiton(left, right) {
            this->operator_sign = "&";
        };
    };

    class OR : public AO {
    public :
        OR(first *left, first *right) : AO(left, right) {
            this->operator_sign = "|";
        };
    };

    class SO : public AO {
    public :
        SO(first *left, first *right) : AO(left, right) {
            this->operator_sign = "->";
        };
    };

    class DEC : public operation {
    public :
        first *mid;

        explicit DEC(first *mid) : mid(mid) { this->operator_sign = "!"; };

        std::string print() override {
            return "!" + mid->print();
        }

        size_t hash() const override {
            return mid->hash() * 71 ;
        }

        bool operator==( operation *oper) const override {
            if (dynamic_cast<DEC * > (oper) != nullptr) {
                auto *box = dynamic_cast<DEC *> (oper);
                return mid->operator==(box->mid);
            }
            return false;
        }


    };


    class VAR : public operation {
    public :
        std::string var;

        explicit VAR(std::string &var) : var(var) { this->operator_sign = "var"; };

        std::string print() override {
            return var;
        }

        size_t hash() const override {
            return (std::hash<std::string>{}(var));
        }

        bool operator==(operation *oper) const override {
            if (dynamic_cast<VAR *> (oper) != nullptr) {
                auto *box = dynamic_cast<VAR *> (oper);
                return var == box->var;
            }
            return false;
        }

    };

    using PAIR = std::pair<operation *, int>;

    class parser {
    public :

        int current = 0;
        std::string str = "";

        parser() = default;

        std::string delete_spaces(std::string &exp) {
            std::string answer;
            for (auto &i : exp) if (i != ' ') answer.push_back(i);
            return answer;
        }

        operation *parse(std::string &exp) {
            str = delete_spaces(exp);
            current = 0;
            return parseSO();
        }


        operation *parseSO() {
            operation *answer = parseOR();
            while (current < str.size() && str[current] == '-') {
                current += 2;
                operation *answer2 = parseSO();
                answer = new SO(answer, answer2);
            }
            return answer;
        }

        operation *parseOR() {
            operation *answer = parseAND();
            while (current < str.size() && str[current] == '|') {
                ++current;
                operation *answer2 = parseAND();
                answer = new OR(answer, answer2);
            }
            return answer;
        }

        operation *parseAND() {
            operation *answer = parseB();
            for (;;) {
                if (current == str.size() || str[current] != '&') return answer;
                current++;
                operation *answer2 = parseB();
                answer = new AND(answer, answer2);
            }
        }

        operation *parseB() {
            if (str[current] == '!') {
                current++;
                operation *answer = parseB();
                return new DEC(answer);
            } else {
                if (str[current] == '(') {
                    ++current;
                    operation *answer = parseSO();
                    if (str[current] == ')') {
                        current++;
                    }
                    return answer;
                }
            }
            return parseVar();
        }

        operation *parseVar() {
            std::string var;
            while (current < str.size() && !is_operation(str[current])) {
                var.push_back(str[current]);
                current++;
            }
            operation *operation1 = new VAR(var);
            return operation1;
        }

        bool is_operation(char t) {
            return t == '-' || t == '&' || t == '!' || t == '|' || t == '(' || t == ')';
        }

    };

    struct operation_hash {
        std::size_t operator()(const operation *k) const {
            return k->hash();
        }
    };

    struct operation_equality {
        bool operator()(operation *k, operation *s) const {
            return k->operator==(s);
        }
    };


    class axiom {
    private:
        operation *kernel;
        std::unordered_map<std::string, operation *> flow_variable_map;
    public:
        axiom() = default;

        axiom(operation *ker) : kernel(ker) {};

        bool is_scheme(operation *kern, operation *expr) {
            if (dynamic_cast<abstract_operaiton *>(expr) != nullptr) {
                if (kern->operator_sign == expr->operator_sign) {
                    auto *box1 = dynamic_cast<abstract_operaiton *> (kern);
                    auto *box2 = dynamic_cast<abstract_operaiton *> (expr);
                    return is_scheme(box1->left, box2->left) && is_scheme(box1->right, box2->right);
                } else return false;
            }
            if (dynamic_cast<DEC *>(expr) != nullptr) {
                if (kern->operator_sign == expr->operator_sign) {
                    auto *box1 = dynamic_cast<DEC *> (kern);
                    auto *box2 = dynamic_cast<DEC *> (expr);
                    return is_scheme(box1->mid, box2->mid);
                } else return false;
            }
            if (dynamic_cast<VAR *>(expr) != nullptr) {
                std::string tree_string = expr->print();
                if (flow_variable_map.count(tree_string) == 0) {
                    flow_variable_map[tree_string] = kern;
                } else return flow_variable_map[tree_string]->operator==(kern);
            }
            return true;
        }

        bool is_scheme(operation *expr) {
            flow_variable_map.clear();
            return is_scheme(expr, kernel);
        }
    };

    struct META {
        int way = -1;
        int id = -1;
    };

    struct MP {
        std::unordered_set<operation *, operation_hash, operation_equality> possible_M = {};
    };

    struct MP_total {
        operation *L = nullptr;
    };


    class proof {
    private :

        std::string A;

        operation *A_op;

        std::string first_shit;

        std::vector<axiom> axioms;

        std::unordered_map<operation *, int, operation_hash, operation_equality> hypothesis;

        std::unordered_map<operation *, META, operation_hash, operation_equality> printed;

        std::vector<operation *> proofment;

        std::unordered_map<operation *, MP, operation_hash, operation_equality> MP_check;

        std::unordered_map<operation *, MP_total, operation_hash, operation_equality> MP_correct;

        std::unordered_map<operation *, int, operation_hash, operation_equality> index;

        std::unordered_map<operation *, int, operation_hash, operation_equality> old_index;

        std::unordered_map<operation *, bool, operation_hash, operation_equality> used;


        std::vector<std::pair<int, operation *>> min;

        parser parser1;

    public :
        explicit proof() {
            std::vector<std::string> axiomss(10);
            axioms.resize(10);
            axiomss[0] = "A->(B->A)";
            axiomss[1] = "(A->B)->((A->B->C)->(A->C))";
            axiomss[2] = "(A->(B->(A&B)))";
            axiomss[3] = "A&B->A";
            axiomss[4] = "A&B->B";
            axiomss[5] = "A ->A|B";
            axiomss[6] = "B->A|B";
            axiomss[7] = "(A->C)->((B->C)->((A|B)->C)";
            axiomss[8] = "(A->B)->((A->!B)->!A)";
            axiomss[9] = "!!A->A";
            for (int i = 0; i < 10; ++i) axioms[i] = {parser1.parse(axiomss[i])};
            take_context();
            if (!get_proof() || check_priveledge()) {
                std::cout << "Proof is incorrect";
                return;
            }
            minimize();
            print_answer();
        }

        bool check_priveledge() {
            if (proofment.empty()) return true;
            return proofment.back()->operator!=(A_op);
        }


        void take_context() {
            std::getline(std::cin, first_shit);
            int stop_position = find_hamma_symbol();
            fill_hypothesis(stop_position);
            get_A(stop_position);

        }

        int find_hamma_symbol() {
            for (int i = 1; i < first_shit.size(); ++i)
                if (first_shit[i] == '-' && first_shit[i - 1] == '|') return i - 1;
            return 0;
        }

        void fill_hypothesis(int stp_pstn) {
            std::string str;
            int count = 1;
            for (int i = 0; i < stp_pstn; ++i) {
                if (first_shit[i] == ',') {
                    hypothesis[parser1.parse(str)] = count;
                    ++count;
                    str.clear();
                } else str.push_back(first_shit[i]);
            }
            if (!str.empty()) hypothesis[parser1.parse(str)] = count;
        }

        void get_A(int stp_pstn) {
            for (int i = stp_pstn + 2; i < first_shit.size(); ++i) A.push_back(first_shit[i]);
            A_op = parser1.parse(A);
        }

        bool is_printed(operation *oper) {
            return printed.find(oper) != printed.end();
        }

        bool get_proof() {
            std::string box;
            while (std::getline(std::cin, box)) {
                if (box.empty()) return true;
                operation *oper = parser1.parse(box);
                if (!is_printed(oper)) {
                    if (is_hypothesis(oper) || is_scheme(oper) || is_modus_ponens(oper)) {
                        proofment.push_back(oper);
                        used[oper] = false;
                        it_can_be_modens_ponens(oper);
                    } else {
                        return false;
                    }
                }
                if (oper->operator==(A_op)) return true ;
            }
            return true;
        }

        bool is_hypothesis(operation *oper) {
            if (hypothesis.find(oper) != hypothesis.end()) {
                printed[oper] = {0, hypothesis[oper]};
                return true;
            }
            return false;
        }

        bool is_scheme(operation *oper) {
            for (int i = 0; i < 10; ++i) {
                if (axioms[i].is_scheme(oper)) {
                    printed[oper] = {1, i + 1};
                    return true;
                }
            }
            return false;
        }

        bool is_modus_ponens(operation *oper) {
            if (MP_correct.find(oper) != MP_correct.end()) return true;
            if (!MP_check[oper].possible_M.empty()) {
                for (auto j : MP_check[oper].possible_M) {
                    if (printed.find(dynamic_cast<abstract_operaiton *>(j)->left) != printed.end()) {
                        printed[oper] = {2, 0};
                        MP_correct[oper].L = j;
                        return true;
                    }
                }
            }
            return false;
        }

        bool it_can_be_modens_ponens(operation *oper) {
            if (oper->operator_sign == "->") {
                auto *box = dynamic_cast<abstract_operaiton * > (oper);
                MP_check[box->right].possible_M.insert(box);
                return true;
            }
            return false;
        }

        static bool comp(const std::pair<int, operation *> &first, const std::pair<int, operation *> &second) {
            return first.first >= second.first;
        }

        void minimize() {
            for (int i = 0; i < proofment.size(); ++i) old_index[proofment[i]] = i;
            minimize(A_op);
            std::sort(min.begin(), min.end(), comp);
            for (int i = 0; i < min.size(); ++i) index[min[i].second] = i;
        }

        void minimize(operation *oper) {
            if (used[oper]) return;
            used[oper] = true;
            min.emplace_back(old_index[oper], oper);
            if (printed[oper].way == 0 || printed[oper].way == 1) return;
            if (printed[oper].way == 2) {
                minimize(MP_correct[oper].L);
                minimize(dynamic_cast<abstract_operaiton *>(MP_correct[oper].L)->left);
            }
        }

        void print_answer() {
            std::cout << first_shit << std::endl;
            for (int i = static_cast<int>(min.size() - 1); i >= 0; --i) {
                operation *cur = min[i].second;
                if (printed[cur].way == 0) {
                    std::cout << "[" << min.size() - i << ". Hypothesis " << printed[cur].id << "]" << " "
                              << cur->print() << std::endl;
                }
                if (printed[cur].way == 1) {
                    std::cout << "[" << min.size() - i << ". Ax. sch. " << printed[cur].id << "]" << " " << cur->print()
                              << std::endl;
                }
                if (printed[cur].way == 2) {
                    std::cout << "[" << min.size() - i << ". M.P. " << min.size() - index[MP_correct[cur].L] << ", "
                              << min.size() - index[dynamic_cast<abstract_operaiton *>(MP_correct[cur].L)->left] << "] "
                              << cur->print() << std::endl;
                }
            }
        }

    };

    proof proof1;
public :


};


int main() {
    god god1;
    return 0;
}