Equilibrium Logic is a logical characterisation of Answer Set Program- ming (ASP) that is very successfully used for the study of ASP foundations and extensions. One of such extensions is Temporal Equilibrium Logic (TEL), that allowed for incorporating temporal modal operators from Linear Temporal Logic (LTL) into ASP. Following the steps of Equilibrium Logic, TEL is defined by selecting models from a temporal extension of the intermediate logic of Here- and-There (HT). These models have the form of traces obtained by some kind of truth minimisation analogous to the one performed in non-temporal ASP. Recently, the variant called contracted TEL (cTEL) introduced an additional minimisation that may also shorten the length of the trace. Each contracted trace obtained with cTEL can be seen as a “summarisation” of a family of temporal stable models of a given theory. One irregularity of cTEL is that it is based on a variant of THT which, for non-temporal formulas, does not collapse to HT, but corresponds to a weaker intermediate logic instead. In this paper, we propose another variant of TEL, called brief TEL (bTEL), that performs a different trace length minimisation in which traces become “shortest witnesses” of the formula or theory. The new variant bTHT collapses to HT for non-temporal theories and it allows for applying Kamp’s translation of temporal logic into Monadic First Order Logic, interpreting the obtained formulas under Quantified HT with dynamic domains. Specifically, we provide the bTEL definition, illustrate its effect on some examples, and prove that Kamp’s translation is sound.