#include <string>
#include <cctype>

using namespace std;

class Parser
{
    string input;
    bool isValid;

    bool isEnd(size_t pos) const
    {
        return pos >= input.size();
    }

    bool readChar(size_t &pos, char c) const
    {
        if (isEnd(pos) || input[pos] != c) {
            return false;
        }

        ++pos;

        return true;
    }

    bool readString(size_t &pos, const string &str) const
    {
        if (input.substr(pos, str.size()) != str) {
            return false;
        }

        pos += str.size();

        return true;
    }

    bool isLetter(size_t pos) const
    {
        return isEnd(pos) == false && isalpha(input[pos]);
    }

    bool isAlphanumeric(size_t pos) const
    {
        return isEnd(pos) == false && isalnum(input[pos]);
    }

    bool readPropositionalLetter(size_t &pos) const
    {
        if (isLetter(pos) == false) {
            return false;
        }

        do {
            ++pos;
        } while (isLetter(pos));

        return true;
    }

    bool readSubformula(size_t &pos) const
    {
        if (isEnd(pos)) {
            return false;
        }

        if (readChar(pos, '-')) {
            return readSubformula(pos);
        }

        if (readChar(pos, '(')) {
            return readSubformula(pos) && readChar(pos, '>') && readSubformula(pos) && readChar(pos, ')');
        }

        return readPropositionalLetter(pos);
    }

    bool findImplication(size_t &pos) const
    {
        int brackets = 0;

        for (; isEnd(pos) == false; ++pos) {
            if (brackets == 0 && input[pos] == '>') {
                ++pos;

                return true;
            }

            if (input[pos] == '(') {
                ++brackets;
            } else if (input[pos] == ')') {
                --brackets;
            }
        }

        return false;
    }

public:
    Parser(const string &input) :
        input(input)
    {
        size_t pos = 0;

        if (readSubformula(pos) == false) {
            isValid = false;

            return;
        }

        if (isEnd(pos)) {
            isValid = true;

            return;
        }

        pos = 0;

        isValid = readSubformula(pos) && readChar(pos, '>') && readSubformula(pos) && isEnd(pos);
    }

    bool axiom1() const
    {
        if (isValid == false) {
            return false;
        }

        if (input.size() >= 2 && input[0] == '(' && input[input.size() - 1] == ')') {
            Parser tmp(input.substr(1, input.size() - 2));

            if (tmp.axiom1()) {
                return true;
            }
        }

        size_t pos = 0;

        if (findImplication(pos) == false) {
            return false;
        }

        string a = input.substr(0, pos - 1);

        return readChar(pos, '(') && findImplication(pos) && readString(pos, a + ")") && isEnd(pos);
    }

    bool axiom2() const
    {
        if (isValid == false) {
            return false;
        }

        if (input.size() >= 2 && input[0] == '(' && input[input.size() - 1] == ')') {
            Parser tmp(input.substr(1, input.size() - 2));

            if (tmp.axiom2()) {
                return true;
            }
        }

        size_t pos = 0;

        if (readChar(pos, '(') == false || findImplication(pos) == false) {
            return false;
        }

        string a = input.substr(1, pos - 2);

        if (readChar(pos, '(') == false || findImplication(pos) == false) {
            return false;
        }

        string b = input.substr(a.size() + 3, pos - a.size() - 4);

        pos = 0;

        if (findImplication(pos) == false) {
            return false;
        }

        string c = input.substr(a.size() + b.size() + 4, pos - a.size() - b.size() - 7);

        return readString(pos, string("((") + a + ">" + b + ")>(" + a + ">" + c + "))") && isEnd(pos);
    }

    bool axiom3() const
    {
        if (isValid == false) {
            return false;
        }

        size_t pos = 0;

        if (readString(pos, "((")) {
            Parser tmp(input.substr(1, input.size() - 2));

            return tmp.axiom3();
        }

        if (readString(pos, "(-") == false || findImplication(pos) == false) {
            return false;
        }

        string b = input.substr(2, pos - 3);

        pos = 0;

        if (findImplication(pos) == false) {
            return false;
        }

        string a = input.substr(b.size() + 4, pos - b.size() - 6);

        return readString(pos, string("(") + a + ">" + b + ")") && isEnd(pos);
    }
};