'Decorate the proof output.'

@staticmethod
def _decorate_clauses(clauses):

    out = u''
    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 = u'A'
        taut = u''
        if clauses[i].is_tautology():
            taut = u'Tautology'
        if clauses[i]._parents:
            parents = str(clauses[i]._parents)
        parents = ((u'    ' * ((max_clause_len - len(str(clauses[i]))) + 1)) + parents)
        seq = ((u'    ' * (max_seq_len - len(str((i + 1))))) + str((i + 1)))
        out += (u'[%s]    %s    %s    %s\n' % (seq, clauses[i], parents, taut))
    return out
