write a code like this one:
import re
from collections import deque

# Helper functions to parse and operate on the KB
def implies_elimination(p, q, formulas):
    """Apply Modus Ponens (Implication Elimination): From p and p > q infer q"""
    if p in formulas and f"({p}>{q})" in formulas:
        return q
    return None

def and_elimination(formula):
    """Apply And Elimination: From p & q infer p or q"""
    match = re.match(r"\((.*)&(.*)\)", formula)
    if match:
        p, q = match.groups()
        return [p, q]
    return None

def not_elimination(formula):
    """Apply Not Elimination: From !!p infer p"""
    match = re.match(r"!!(.*)", formula)
    if match:
        return match.groups()[0]
    return None

def iff_elimination(formula):
    """Apply IFF elimination: From p = q infer (p > q) and (q > p)"""
    match = re.match(r"\((.*)=(.*)\)", formula)
    if match:
        p, q = match.groups()
        return [f"({p}>{q})", f"({q}>{p})"]
    return None

def parse_input():
    """Reads the input and returns KB, query, and number of propositions"""
    n, m = map(int, input().strip().split())
    formulas = []
    for _ in range(n):
        formula = input().split(":")[1].strip()
        formulas.append(formula)
    query = input().split(":")[1].strip()
    return formulas, query

def natural_deduction(formulas, query):
    """Main natural deduction algorithm to prove the query"""
    steps = []
    formulas_set = set(formulas)
    
    # Start with a queue to track possible deductions
    queue = deque(formulas)
    
    while queue:
        formula = queue.popleft()
        steps.append(formula)
        
        # Apply And Elimination
        and_results = and_elimination(formula)
        if and_results:
            for res in and_results:
                if res not in formulas_set:
                    formulas_set.add(res)
                    queue.append(res)
        
        # Apply Not Elimination
        not_result = not_elimination(formula)
        if not_result and not_result not in formulas_set:
            formulas_set.add(not_result)
            queue.append(not_result)

        # Apply IFF Elimination
        iff_results = iff_elimination(formula)
        if iff_results:
            for res in iff_results:
                if res not in formulas_set:
                    formulas_set.add(res)
                    queue.append(res)
        
        # Apply Implication Elimination (Modus Ponens)
        for p in formulas_set:
            for q in formulas_set:
                imp_result = implies_elimination(p, q, formulas_set)
                if imp_result and imp_result not in formulas_set:
                    formulas_set.add(imp_result)
                    queue.append(imp_result)

        # If we derive the query, we are done
        if query in formulas_set:
            print(f"Query: {query} derived in {len(steps)} steps.")
            return steps

    return steps

def main():
    formulas, query = parse_input()
    steps = natural_deduction(formulas, query)
    
    # Print the deduction steps
    for i, step in enumerate(steps, start=1):
        print(f"S{i}: {step}")
    print(f"Total steps taken: {len(steps)}")

if __name__ == "__main__":
    main()