Неверная выходная аннотация в средстве проверки доказательств выражений логики

Я разрабатываю скрипт проверки доказательств алгебры логики на Python, он анализирует выражения и выводит ответ, являются ли они аксиомами, гипотезами, выведенными Modus Ponens или неизвестными. Однако я столкнулся с проблемой, когда некоторые строки неправильно помечаются как «[Неизвестно]», несмотря на то, что они, по-видимому, соответствуют критериям аксиом или Modus Ponens.

Например, учитывая ввод:

|-A&B->A
|-A&B->B
А&Б|-А
А&Б|-Б
А&Б|-Б->А->Б&А
А&Б|-А->Б&А
А&Б|-Б&А
|-А&Б->Б&А

Ожидаемые аннотации для строк 5 и 6 относятся к аксиомам или Modus Ponens, но я получаю «[Неизвестно]». В частности, строка 5 должна быть признана аксиомой 3, но это не так. Вот фрагмент кода, отвечающий за анализ и аннотирование выражений:

# Определения функций для parse_expression, check_parentheses, Split_expression и т. д.

def is_axiom(expression):
    def matches(expr, pattern):
        # Проверка, является ли шаблон строкой (в этом случае он может соответствовать любому выражению)
        if isinstance(pattern, str):
            return True
        # Проверка структурного соответствия выражения и шаблона
        if isinstance(expr, tuple) and isinstance(pattern, tuple) and expr[0] == pattern[0] and len(expr) == len(pattern):
            # Дополнительная проверка для аксиом 4 и 5
            if pattern in [('->', ('&', 'A', 'B'), 'A'), ('->', ('&', 'A', 'B'), 'B')]:
                # Проверяем, соответствует ли последний элемент выражения последнему элементу шаблона
                return expr[-1] == pattern[-1] and all(matches(e, p) for e, p in zip(expr[1:], pattern[1:]))
            # Стандартная проверка всех элементов выражения и шаблона
            return all(matches(e, p) for e, p in zip(expr[1:], pattern[1:]))
        return False

    # Шаблоны аксиом представлены в виде кортежей
    axiom_patterns = [
        ('->', 'A', ('->', 'B', 'A')),  # A -> B -> A
        ('->', ('->', 'A', 'B'), ('->', ('->', 'A', ('->', 'B', 'C')), ('->', 'A', 'C'))),  # (A -> B) -> (A -> B -> C) -> (A -> C)
        ('->', 'A', ('->', 'B', ('&', 'A', 'B'))),  # A -> B -> A & B
        ('->', ('&', 'A', 'B'), 'A'),  # A & B -> A
        ('->', ('&', 'A', 'B'), 'B'),  # A & B -> B
        ('->', 'A', ('|', 'A', 'B')),  # A -> A | B
        ('->', 'B', ('|', 'A', 'B')),  # B -> A | B
        ('->', ('->', 'A', 'C'), ('->', ('->', 'B', 'C'), ('->', ('|', 'A', 'B'), 'C'))),  # (A -> C) -> (B -> C) -> (A | B -> C)
        ('->', ('->', 'A', 'B'), ('->', ('->', 'A', ('NOT', 'B')), ('NOT', 'A'))),  # (A -> B) -> (A -> !B) -> !A
        ('->', ('NOT', ('NOT', 'A')), 'A')  # !!A -> A
    ]

   # Проверка соответствия выражения одному из шаблонов аксиом
    for i, pattern in enumerate(axiom_patterns, 1):
        if matches(expression, pattern):
            return i  # Возвращаем номер аксиомы, если найдено соответствие
    return None  # Возвращаем None, если выражение не соответствует ни одному из шаблонов аксиом

     ...
def apply_modus_ponens(proof_lines, current_index):
    if current_index >= len(proof_lines):
        return None

    current_context, current_conclusion = proof_lines[current_index]

    for index_implication, (context_implication, conclusion_implication) in enumerate(proof_lines[:current_index]):
        # Проверяем, является ли заключение импликацией, и совпадает ли второй компонент импликации с текущим заключением
        if (isinstance(conclusion_implication, tuple) and conclusion_implication[0] == '->' and
                conclusion_implication[2] == current_conclusion):
            # Ищем утверждение A в предшествующих строках, включая строку с импликацией
            for index_a, (context_a, conclusion_a) in enumerate(proof_lines[:index_implication + 1]):
                if conclusion_a == conclusion_implication[1]:
                    # Проверяем, является ли контекст импликации подмножеством текущего контекста
                    if set(context_implication).issubset(set(current_context)):
                        return (index_a + 1, index_implication + 1)

    return None

     ...
def can_be_proved(proof_lines, index):
    conclusion = proof_lines[index][1]

    axiom_result = is_axiom(conclusion)
    if axiom_result is not None:
        return f"Ax. {axiom_result}"
    
    if is_hypothesis(conclusion, proof_lines[index][0]):
        return "Hypothesis"
    
    mp_result = apply_modus_ponens(proof_lines, index)
    if mp_result:
        return f"M.P. {mp_result[0]}, {mp_result[1]}"
    
    deduced_lines = apply_deduction_theorem(proof_lines[:index + 1])
    for deduced_pair in deduced_lines:
        if deduced_pair[1] == index + 1:
            return f"Ded. {deduced_pair[0]}"

    return "Unknown"
     ...

# Другие важные функции и основная логика программы

Я подозреваю, что проблема может быть в функциях is_axiom или can_be_proved, или, возможно, в том, как я анализирую и разделяю выражения. Может Modus Ponens?