\documentclass[a4paper]{article}
\usepackage{gclc_proof}


\begin{document}



\begin{displayproof}
\proofstep{ S_{ABD}}{=}{ S_{CBD}}{by the statement}{-325.000000=-325.000000}
\proofstep{ \left( S_{ABC} +  \left( 1  \cdot  \left( S_{ABB} +  \left( -1  \cdot  S_{ABA}\right)\right)\right)\right)}{=}{ S_{CBD}}{by Lemma 29 (point $D$ eliminated)}{-325.000000=-325.000000}
\proofstep{ \left( S_{ABC} +  \left( 1  \cdot  \left( 0  +  \left( -1  \cdot  0 \right)\right)\right)\right)}{=}{ S_{CBD}}{by geometric simplifications}{-325.000000=-325.000000}
\proofstep{ S_{ABC}}{=}{ S_{CBD}}{by algebraic simplifications}{-325.000000=-325.000000}
\proofstep{ S_{ABC}}{=}{ \left( S_{CBC} +  \left( 1  \cdot  \left( S_{CBB} +  \left( -1  \cdot  S_{CBA}\right)\right)\right)\right)}{by Lemma 29 (point $D$ eliminated)}{-325.000000=-325.000000}
\proofstep{ S_{ABC}}{=}{ \left( 0  +  \left( 1  \cdot  \left( 0  +  \left( -1  \cdot  \left( -1  \cdot  S_{ABC}\right)\right)\right)\right)\right)}{by geometric simplifications}{-325.000000=-325.000000}
\proofstep{ 0 }{=}{ 0 }{by algebraic simplifications}{0=0}
\end{displayproof}


\proveddisproved{1}
There are no ndg conditions.



Number of elimination proof steps:      2

Number of geometric proof steps:        5

Number of algebraic proof steps:       11

Total number of proof steps:           18


Time spent by the prover: 0.000 seconds


\end{document}

