A = rdf.Var()
for m in db.match([[A, rdf.type, pt.TrueSentence],
                   []]):
    pass



def recognizeFormulas(db, f):
    """Get any/all the formulas denoted by f, as described in db,
    along with the triples used to recognize it.
    

    Usually, you'd expect to get zero or one, but it's entirely
    possible to get several, because: (1) there may be equivalent
    terms for bits of the formula, and (2) the formula may not be
    schema-valid (it might be both a Triple and a Conjunction.

    If usedTriples is a db (such as []), then any/all triples used to
    perform the recognition are added to it.
    """
    s=rdf.Var(); p=rdf.Var(); o=rdf.Var()
    for m in db.match([[f, pt.subjectTerm, s],
                       [f, pt.predicateTerm, p],
                       [f, pt.objectTerm, o]]):
        for (ss,u1) in recognizeTerms(db, s.currentValue):
            for (pp,u2) in recognizeTerms(db, p.currentValue):
                for (oo,u3) in recognizeTerms(db, o.currentValue):
                    yield (['rdf', ss, pp, oo], m.triples+u1+u2+u3)

    l=rdf.Var(); r=rdf.Var()
    for m in db.match([[f, pt.conjLeft, l],
                       [f, pt.conjRight, r]]):
        for (ll,u1) in recognizeFormulas(db, l):
            for (rr,u2) in recognizeFormulas(db, r):
                yield (['&', ll, rr], m.triples+u1+u2)
    
    

def recognizeTerm(db, f):