algebraic:
    or-true: (OR ?a true) => true
    and-false: (AND ?a false) => false
    or-false: (OR ?a false) => ?a
    and-true: (AND ?a true) => ?a

    # Commutativity
    or-commutative: (OR ?a ?b) => (OR ?b ?a)
    and-commutative: (AND ?a ?b) => (AND ?b ?a)

    # Associativity
    or-associative: (OR (OR ?a ?b) ?c) => (OR ?a (OR ?b ?c))
    and-associative: (AND (AND ?a ?b) ?c) => (AND ?a (AND ?b ?c))

    # Distributivity
    or-distributive: (OR ?a (AND ?b ?c)) <=> (AND (OR ?a ?b) (OR ?a ?c))
    and-distributive: (AND ?a (OR ?b ?c)) <=> (OR (AND ?a ?b) (AND ?a ?c))

    # Complement Rules
    or-complement: (OR ?a (INV ?a)) => true
    and-complement: (AND ?a (INV ?a)) => false

    # De Morgan's Laws
    de-morgan-1: (INV (AND ?a ?b)) <=> (OR (INV ?a) (INV ?b))
    de-morgan-2: (INV (OR ?a ?b)) <=> (AND (INV ?a) (INV ?b))

    # Idempotent Laws
    or-idempotent: (OR ?a ?a) => ?a
    and-idempotent: (AND ?a ?a) => ?a

    # Absorption Laws
    or-absorption: (OR ?a (AND ?a ?b)) => ?a
    and-absorption: (AND ?a (OR ?a ?b)) => ?a

    # Consensus Rule
    consensus-rule: (OR (AND ?x ?y) (OR (AND (INV ?x) ?z) (AND ?y ?z))) <=> (OR (AND ?x ?y) (AND (INV ?x) ?z))

    # Negation Rules
    negation-cancel: ?a <=> (INV (INV ?a))

cells:
    and2_x1: (AND ?a ?b) => (AND2_X1 ?a ?b)
    nand2_x1: (INV (AND ?a ?b)) => (NAND2_X1 ?a ?b)
    or2_x1: (OR ?a ?b) => (OR2_X1 ?a ?b)
    nor2_x1: (INV (OR ?a ?b)) => (NOR2_X1 ?a ?b)
    xor2_x1: (OR (AND ?b (INV ?a)) (AND ?a (INV ?b))) => (XOR2_X1 ?a ?b)
    xnor2_x1: (OR (AND ?b ?a) (AND (INV ?a) (INV ?b))) => (XNOR2_X1 ?a ?b)
    and3_x1: (AND (AND ?a ?b) ?c) => (AND3_X1 ?a ?b ?c)
    nand3_x1: (INV (AND (AND ?a ?b) ?c)) => (NAND3_X1 ?a ?b ?c)
    or3_x1: (OR (OR ?a ?b) ?c) => (OR3_X1 ?a ?b ?c)
    nor3_x1: (INV (OR (OR ?a ?b) ?c)) => (NOR3_X1 ?a ?b ?c)
    and4_x1: (AND (AND ?a ?b) (AND ?c ?d)) => (AND4_X1 ?a ?b ?c ?d)
    nand4_x1: (INV (AND (AND ?a ?b) (AND ?c ?d))) => (NAND4_X1 ?a ?b ?c ?d)
    or4_x1: (OR (OR ?a ?b) (OR ?c ?d)) => (OR4_X1 ?a ?b ?c ?d)
    nor4_x1: (INV (OR (OR ?a ?b) (OR ?c ?d))) => (NOR4_X1 ?a ?b ?c ?d)
    inv_x1: (INV ?a) => (INV_X1 ?a)
    aoi21_x1: (INV (OR (AND ?b ?c) ?a)) => (AOI21_X1 ?a ?b ?c)
    oai21_x1: (INV (AND (OR ?b ?c) ?a)) => (OAI21_X1 ?a ?b ?c)
    aoi22_x1: (INV (OR (AND ?c ?d) (AND ?a ?b))) => (AOI22_X1 ?a ?b ?c ?d)
    oai22_x1: (INV (AND (OR ?c ?d) (OR ?a ?b))) => (OAI22_X1 ?a ?b ?c ?d)
    aoi211_x1: (INV (OR ?a (OR (AND ?c ?d) ?b))) => (AOI211_X1 ?a ?b ?c ?d)
    oai211_x1: (INV (AND ?a (AND (OR ?c ?d) ?b))) => (OAI211_X1 ?a ?b ?c ?d)
    aoi221_x1: (INV (OR (AND ?b ?c) (OR ?a (AND ?d ?e)))) => (AOI221_X1 ?a ?b ?c ?d ?e)
    oai221_x1: (INV (AND (OR ?b ?c) (AND ?a (OR ?d ?e)))) => (OAI221_X1 ?a ?b ?c ?d ?e)
    aoi222_x1: (INV (OR (AND ?e ?f) (OR (AND ?a ?b) (AND ?c ?d)))) => (AOI222_X1 ?a ?b ?c ?d ?e ?f)
    oai222_x1: (INV (AND (OR ?e ?f) (AND (OR ?a ?b) (OR ?c ?d)))) => (OAI222_X1 ?a ?b ?c ?d ?e ?f)
    mux2_x1: (OR (AND (INV ?s) ?b) (AND ?s ?a)) => (MUX2_X1 ?s ?a ?b)
