@staticmethod
    def _decorate_clauses(clauses):
        out = ''
        max_clause_len = max([len(str(clause)) for clause in clauses])
        max_seq_len = len(str(len(clauses)))
        for i in range(len(clauses)):
            parents = 'A'
            taut = ''
            if clauses[i].is_tautology():
                taut = 'Tautology'
            if clauses[i]._parents:
                parents = str(clauses[i]._parents)
            parents = ' '*(max_clause_len-len(str(clauses[i]))+1) + parents
            seq = ' '*(max_seq_len-len(str(i+1))) + str(i+1)
            out += '[%s] %s %s %s\n' % (seq, clauses[i], parents, taut)
        return out
Decorate the proof output.
dataset/ETHPy150Open nltk/nltk/nltk/inference/resolution.py/ResolutionProverCommand._decorate_clauses