Pasted

from __future__ import annotations
from typing import List, Optional
 
 
class Node:
    pass
 
 
class Atom(Node):
 
    name: str
    args: List[Atom]
 
    def __init__(self, name: str, args: List[Atom] = []):
        self.name = name
        self.args = args
 
    def __str__(self):
        return f"Atom({self.name}, [{', '.join(map(str, self.args))}])"
 
    def __eq__(self, other):
        return isinstance(other, type(self))\
               and self.name == other.name \
               and len(self.args) == len(other.args) \
               and all(x == y for (x, y) in zip(self.args, other.args))
 
 
class Disjunction(Node):
 
    a: Node
    b: Node
 
    def __init__(self, a: Node, b: Node):
        self.a = a
        self.b = b
 
    def __str__(self):
        return f"OR({self.a}, {self.b})"
 
    def __eq__(self, other):
        return isinstance(other, type(self)) and self.a == other.a and self.b == other.b
 
 
class Conjunction(Node):
 
    a: Node
    b: Node
 
    def __init__(self, a: Node, b: Node):
        self.a = a
        self.b = b
 
    def __str__(self):
        return f"AND({self.a}, {self.b})"
 
    def __eq__(self, other):
        return isinstance(other, type(self)) and self.a == other.a and self.b == other.b
 
 
class Definition(Node):
 
    head: Atom
    body: Optional[Node]
 
    def __init__(self, head: Atom, body: Optional[Node]):
        self.head = head
        self.body = body
 
    def __str__(self):
        return f"{self.head} :- {self.body}"
 
    def __eq__(self, other):
        return isinstance(other, type(self)) and self.head == other.head and self.body == other.body