Are there axioms satisfied in commutative rings and distributive lattices but not satisfied in commutative semirings?

Question

Consider the language of rigs (also called semirings): it has constants $0$ and $1$ and binary operations $+$ and $\times$. The theory of commutative rigs is generated by the usual axioms: $+$ is associative, commutative, and has unit $0$; $\times$ is associative, commutative, and has unit $1$; $\times$ distributes over $+$; and $0$ is absorbing for $\times$.

Every commutative ring is a commutative rig (of course), and every distributive lattice as well (interpreting $\bot$ as $0$, $\top$ as $1$, $\vee$ as $+$, and $\wedge$ as $\times$). In fact, the category of commutative rings is a full reflective subcategory of the category of commutative rigs, as is the category of distributive lattices. The intersection of the two is trivial, in the sense that only the trivial algebra is both a ring and a lattice. (In a lattice, $\top \vee \top = \top$; but in a ring $1 + 1 = 1$ implies $0 = 1$.) What I am wondering is how close do these two subcategories come to capturing "all" the possible behaviour of commutative rigs. More precisely:

Question 1. Is there a Horn clause in the language of rigs that is true in every commutative ring and every distributive lattice but false in some commutative rig?

Since commutative rings are not axiomatisable in the language of rigs using only Horn clauses, I would also be interested to hear about, say, cartesian sequents instead of Horn clauses. This can be phrased category theoretically:

Question 2. Is there a full reflective subcategory $\mathcal{C}$ of the category of commutative rigs that is closed under filtered colimits and contains the subcategories of commutative rings and distributive lattices but is not the whole category? (Furthermore, can we choose such a $\mathcal{C}$ so that the reflection of $\mathbb{N} [x]$ (= the free commutative rig on one generator) represents a monadic functor $\mathcal{C} \to \textbf{Set}$?)

I don't want to be too permissive, however – since commutative rings and distributive lattices can both be axiomatised by a single first order sentence in the language of rigs, taking their disjunction yields a sentence that is true in only commutative rings and distributive lattices but false in general commutative rigs.

Here is an example of a first-order axiom that is true in commutative rings and distributive lattices that is false in some commutative rig:

For all $a$ and $b$, there exist $c$ and $d$ such that $(c + d) a + d b = b$.

This axiom amounts to saying that every ideal is subtractive (which is a second-order axiom prima facie); it is the case that every ideal in a commutative ring or distributive lattice is subtractive. The way I prefer to think about it is that in a commutative ring, ideals are automatically subtractive because $-1$ exists, and in a distributive lattice, ideals are automatically subtractive because they are downward closed. As it turns out, this can be expressed as a first-order sentence, albeit not a cartesian sequent.

Answer 1

Following François's suggestion, I ran alg to find a unital commutative semiring which fails to satisfy $$ \forall x\, y\, z,\; x + z = y + z \land x \times z = y \times z \Rightarrow x = y. \tag{1} $$ The smallest one has size 3. Here is the output of the program, cut off after the first example.

    Theory unital_commutative_semiring.
    
    Constant 0 1.
    Binary + *.
    
    Axiom: 0 + x = x.
    Axiom: x + 0 = x.
    Axiom: x + (y + z) = (x + y) + z.
    Axiom: x + y = y + x.
    
    Axiom: 1 * x = x.
    Axiom: x * 1 = x.
    Axiom: x * (y * z) = (x * y) * z.
    Axiom: x * y = y * x.
    
    Axiom: (x + y) * z = x * z + y * z.
    Axiom: x * (y + z) = x * y + x * z.
    
    Axiom: 0 * x = 0.
    Axiom: x * 0 = 0.
    
    # Extra command-line axioms
    Axiom: not forall x y z, x + z = y + z /\ x * z = y * z => x = y.

# Size 3

### unital_commutative_semiring_with_extras_3_1


    + |  0  1  a
    --+---------
    0 |  0  1  a
    1 |  1  1  1
    a |  a  1  a


    * |  0  1  a
    --+---------
    0 |  0  0  0
    1 |  0  1  a
    a |  0  a  0

We can also count the structures. For commutative unital semirings the counts are

    size | count
    -----|------
       2 | 2
       3 | 6
       4 | 36
       5 | 228
       6 | 2075

The counts for commutative unital semirings that also satisfy (1):

    size | count
    -----|------
       2 | 2
       3 | 3
       4 | 9
       5 | 12
       6 | 23

So clearly there will be some, but it looks like not too many for small sizes.

It is a bit weird that $2, 6, 36, 228, 2075$ is not in OEIS.