  We develop the rewriting theory for monoidal supercategories and
2-supercategories. This extends the theory of higher-dimensional rewriting
established for (linear) 2-categories to the super setting, providing a suite
of tools for constructing bases and normal forms for 2-supercategories given by
generators and relations. We then employ this newly developed theory to prove
the non-degeneracy conjecture for the odd categorification of quantum sl(2)
from arXiv:1307.7816 and arXiv:1701.04133. As a corollary, this gives a
classification of dg-structures on the odd 2-category conjectured in
arXiv:1808.04924.
