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


\begin{document}

\title{GCLC Prover Output for conjecture ``figure39'' }

\author{Area method used}

\maketitle



\begin{displayproof}
\proofstep{ \left( \left( \frac{\overrightarrow{AF}}{\overrightarrow{FB}} \cdot  \frac{\overrightarrow{BD}}{\overrightarrow{DC}}\right) \cdot  \frac{\overrightarrow{CE}}{\overrightarrow{EA}}\right)}{=}{ 1 }{by the statement}{1=1}
\proofstep{ \left( \left( \left( -1  \cdot  \frac{\overrightarrow{AF}}{\overrightarrow{BF}}\right) \cdot  \frac{\overrightarrow{BD}}{\overrightarrow{DC}}\right) \cdot  \frac{\overrightarrow{CE}}{\overrightarrow{EA}}\right)}{=}{ 1 }{by geometric simplifications}{1=1}
\proofstep{ \left( -1  \cdot  \left( \frac{\overrightarrow{AF}}{\overrightarrow{BF}} \cdot  \left( \frac{\overrightarrow{BD}}{\overrightarrow{DC}} \cdot  \frac{\overrightarrow{CE}}{\overrightarrow{EA}}\right)\right)\right)}{=}{ 1 }{by algebraic simplifications}{1=1}
\proofstep{ \left( -1  \cdot  \left( \frac{ S_{APC}}{ S_{BPC}} \cdot  \left( \frac{\overrightarrow{BD}}{\overrightarrow{DC}} \cdot  \frac{\overrightarrow{CE}}{\overrightarrow{EA}}\right)\right)\right)}{=}{ 1 }{by Lemma 8 (point $F$ eliminated)}{1=1}
\proofstep{ \left( -1  \cdot  \left( \frac{ S_{APC}}{ S_{BPC}} \cdot  \left( \frac{\overrightarrow{BD}}{\overrightarrow{DC}} \cdot  \left( -1  \cdot  \frac{\overrightarrow{CE}}{\overrightarrow{AE}}\right)\right)\right)\right)}{=}{ 1 }{by geometric simplifications}{1=1}
\proofstep{ \frac{ \left( S_{APC} \cdot  \left( \frac{\overrightarrow{BD}}{\overrightarrow{DC}} \cdot  \frac{\overrightarrow{CE}}{\overrightarrow{AE}}\right)\right)}{ S_{BPC}}}{=}{ 1 }{by algebraic simplifications}{1=1}
\proofstep{ \frac{ \left( S_{APC} \cdot  \left( \frac{\overrightarrow{BD}}{\overrightarrow{DC}} \cdot  \frac{ S_{CPB}}{ S_{APB}}\right)\right)}{ S_{BPC}}}{=}{ 1 }{by Lemma 8 (point $E$ eliminated)}{1=1}
\proofstep{ \frac{ \left( S_{APC} \cdot  \left( \left( -1  \cdot  \frac{\overrightarrow{BD}}{\overrightarrow{CD}}\right) \cdot  \frac{ S_{CPB}}{ S_{APB}}\right)\right)}{ \left( -1  \cdot  S_{CPB}\right)}}{=}{ 1 }{by geometric simplifications}{1=1}
\proofstep{ \frac{ \left( S_{APC} \cdot  \frac{\overrightarrow{BD}}{\overrightarrow{CD}}\right)}{ S_{APB}}}{=}{ 1 }{by algebraic simplifications}{1=1}
\proofstep{ \frac{ \left( S_{APC} \cdot  \frac{ S_{BPA}}{ S_{CPA}}\right)}{ S_{APB}}}{=}{ 1 }{by Lemma 8 (point $D$ eliminated)}{1=1}
\proofstep{ \frac{ \left( S_{APC} \cdot  \frac{ S_{BPA}}{ \left( -1  \cdot  S_{APC}\right)}\right)}{ \left( -1  \cdot  S_{BPA}\right)}}{=}{ 1 }{by geometric simplifications}{1=1}
\proofstep{ 1 }{=}{ 1 }{by algebraic simplifications}{1=1}
\end{displayproof}


\proveddisproved{1}


NDG conditions are:

$ S_{BPA}\neq S_{CPA}$ i.e., lines $BC$ and $PA$ are not parallel (construction based assumption)

$ S_{APB}\neq S_{CPB}$ i.e., lines $AC$ and $PB$ are not parallel (construction based assumption)

$ S_{APC}\neq S_{BPC}$ i.e., lines $AB$ and $PC$ are not parallel (construction based assumption)

$ P_{FBF}\neq 0 $ i.e., points $F$ and $B$ are not identical (conjecture based assumption)

$ P_{DCD}\neq 0 $ i.e., points $D$ and $C$ are not identical (conjecture based assumption)

$ P_{EAE}\neq 0 $ i.e., points $E$ and $A$ are not identical (conjecture based assumption)


\vspace*{2mm} \hrule \vspace*{2mm} 


Number of elimination proof steps:      3

Number of geometric proof steps:        6

Number of algebraic proof steps:       23

Total number of proof steps:           32


Time spent by the prover: 0.000 seconds


\end{document}

