  First-order temporal logics are notorious for their bad computational
behaviour. It is known that even the two-variable monadic fragment is highly
undecidable over various linear timelines, and over branching time even
one-variable fragments might be undecidable. However, there have been several
attempts on finding well-behaved fragments of first-order temporal logics and
related temporal description logics, mostly either by restricting the available
quantifier patterns, or considering sub-Boolean languages. Here we analyse
seemingly `mild' extensions of decidable one-variable fragments with counting
capabilities, interpreted in models with constant, decreasing, and expanding
first-order domains. We show that over most classes of linear orders these
logics are (sometimes highly) undecidable, even without constant and function
symbols, and with the sole temporal operator `eventually'.
  We establish connections with bimodal logics over 2D product structures
having linear and `difference' (inequality) component relations, and prove our
results in this bimodal setting. We show a general result saying that
satisfiability over many classes of bimodal models with commuting linear and
difference relations is undecidable. As a by-product, we also obtain new
examples of finitely axiomatisable but Kripke incomplete bimodal logics. Our
results generalise similar lower bounds on bimodal logics over products of two
linear relations, and our proof methods are quite different from the proofs of
these results. Unlike previous proofs that first `diagonally encode' an
infinite grid, and then use reductions of tiling or Turing machine problems,
here we make direct use of the grid-like structure of product frames and obtain
undecidability by reductions of counter (Minsky) machine problems.
