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


\begin{document}

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

\author{Wu's method used}

\maketitle





\section{Construction and prover internal state}





\subsection*{Construction commands:}

\begin{itemize}

\item 

Point $A$ 
\item 

Point $B$ 
\item 

Point $C$ 
\item 

Point $P$ 
\item 

Line $a$: $B$ $C$ 
\item 

Line $b$: $A$ $C$ 
\item 

Line $c$: $A$ $B$ 
\item 

Line $pa$: $P$ $A$ 
\item 

Line $pb$: $P$ $B$ 
\item 

Line $pc$: $P$ $C$ 
\item 

Intersection of lines, $D$: $a$ $pa$ 
\item 

Intersection of lines, $E$: $b$ $pb$ 
\item 

Intersection of lines, $F$: $c$ $pc$ 
\end{itemize}





\subsection*{Coordinates assigned to the points:}

\begin{itemize}

\item $A = (0, 0)$

\item $B = (u_{1}, 0)$

\item $C = (u_{2}, u_{3})$

\item $P = (u_{4}, u_{5})$

\item $D = (x_{2}, x_{1})$

\item $E = (x_{4}, x_{3})$

\item $F = (x_{6}, 0)$

\end{itemize}





\subsection*{Conjecture(s):}

\begin{enumerate}

\item Given conjecture

\begin{itemize}

\item \textbf{GCLC code:}


\begin{verbatim}
 equal { mult { mult { sratio A F F B } { sratio B D D C } } { sratio C E E A } } 1 
\end{verbatim}

\end{itemize}

\begin{itemize}

\item \textbf{Expression:}



$ \left( \left( \frac{\overrightarrow{AF}}{\overrightarrow{FB}} \cdot  \frac{\overrightarrow{BD}}{\overrightarrow{DC}}\right) \cdot  \frac{\overrightarrow{CE}}{\overrightarrow{EA}}\right)$ $=$ $ 1 $\item \textbf{Expression after rationalization:}



$ ( ( (x(A) - x(F)) \cdot  (y(B) - y(D))) \cdot  (y(C) - y(E)))$ $=$ $ ( ( ( 1  \cdot  (x(F) - x(B))) \cdot  (y(D) - y(C))) \cdot  (y(E) - y(A)))$\end{itemize}

\end{enumerate}

\hspace*{4.1mm}





\section{Resolving constructed lines}

\begin{itemize}

\item $a \ni B, C, D$ \item $b \ni A, C, E$ \item $c \ni A, B, F$ ; line is horizontal (i.e., $y(A) = y(B)$)\item $pa \ni P, A, D$ \item $pb \ni P, B, E$ \item $pc \ni P, C, F$ \end{itemize}





\section{Creating polynomials from hypotheses}

\begin{itemize}

\item 

Point $A$ 


no condition\item 

Point $B$ 


no condition\item 

Point $C$ 


no condition\item 

Point $P$ 


no condition\item 

Line $a$: $B$ $C$ 
\begin{itemize}

\item 

point $B$ is on the line ($B$, $C$)


no condition\item 

point $C$ is on the line ($B$, $C$)


no condition\end{itemize}

\item 

Line $b$: $A$ $C$ 
\begin{itemize}

\item 

point $A$ is on the line ($A$, $C$)


no condition\item 

point $C$ is on the line ($A$, $C$)


no condition\end{itemize}

\item 

Line $c$: $A$ $B$ 
\begin{itemize}

\item 

point $A$ is on the line ($A$, $B$)


no condition\item 

point $B$ is on the line ($A$, $B$)


no condition\end{itemize}

\item 

Line $pa$: $P$ $A$ 
\begin{itemize}

\item 

point $P$ is on the line ($P$, $A$)


no condition\item 

point $A$ is on the line ($P$, $A$)


no condition\end{itemize}

\item 

Line $pb$: $P$ $B$ 
\begin{itemize}

\item 

point $P$ is on the line ($P$, $B$)


no condition\item 

point $B$ is on the line ($P$, $B$)


no condition\end{itemize}

\item 

Line $pc$: $P$ $C$ 
\begin{itemize}

\item 

point $P$ is on the line ($P$, $C$)


no condition\item 

point $C$ is on the line ($P$, $C$)


no condition\end{itemize}

\item 

Intersection of lines, $D$: $a$ $pa$ 
\begin{itemize}

\item 

point $D$ is on the line ($B$, $C$)
$$
p_{1}  =  -u_{3}x_{2}+(u_{2}-u_{1})x_{1}+u_{3}u_{1}
$$
\item 

point $D$ is on the line ($P$, $A$)
$$
p_{2}  =  u_{5}x_{2}-u_{4}x_{1}
$$
\end{itemize}

\item 

Intersection of lines, $E$: $b$ $pb$ 
\begin{itemize}

\item 

point $E$ is on the line ($A$, $C$)
$$
p_{3}  =  -u_{3}x_{4}+u_{2}x_{3}
$$
\item 

point $E$ is on the line ($P$, $B$)
$$
p_{4}  =  u_{5}x_{4}+(-u_{4}+u_{1})x_{3}-u_{5}u_{1}
$$
\end{itemize}

\item 

Intersection of lines, $F$: $c$ $pc$ 
\begin{itemize}

\item 

point $F$ is on the line ($A$, $B$)
 --- true by the construction



no condition\item 

point $F$ is on the line ($P$, $C$)
$$
p_{5}  =  (u_{5}-u_{3})x_{6}+(-u_{5}u_{2}+u_{4}u_{3})
$$
\end{itemize}

\end{itemize}





\section{Creating polynomial from the conjecture}

\begin{itemize}

\item Processing given conjecture(s).

\end{itemize}

\begin{description}

\item [Conjecture 1:] $$
p_{6}  =  -2x_{6}x_{3}x_{1}+u_{3}x_{6}x_{3}+u_{3}x_{6}x_{1}+u_{1}x_{3}x_{1}-u_{3}u_{1}x_{3}
$$
\end{description}





\section{Invoking the theorem prover}

The used proving method is Wu's method.

The input system is:

\begin{eqnarray*}
p_{0} &=& -u_{3}x_{2}+(u_{2}-u_{1})x_{1}+u_{3}u_{1}\\
p_{1} &=& u_{5}x_{2}-u_{4}x_{1}\\
p_{2} &=& -u_{3}x_{4}+u_{2}x_{3}\\
p_{3} &=& u_{5}x_{4}+(-u_{4}+u_{1})x_{3}-u_{5}u_{1}\\
p_{4} &=& (u_{5}-u_{3})x_{6}+(-u_{5}u_{2}+u_{4}u_{3})\\
\end{eqnarray*}




\subsection{Triangulation, step 1}

\begin{description}

\item [Choosing variable:]  Trying the variable with index 6.

\item [Variable $x_{6}$ selected:]  The number of polynomials with this variable is 1.

\item [Single polynomial with chosen variable:]  No reduction needed.

\item The triangular system has not been changed.



\end{description}





\subsection{Triangulation, step 2}

\begin{description}

\item [Choosing variable:]  Trying the variable with index 5.

\item [Choosing variable:]  Trying the variable with index 4.

\item [Variable $x_{4}$ selected:]  The number of polynomials with this variable is 2.

\item [Minimal degrees:]  3 polynomials with degree 1 and 2 polynomials with degree 1.

\item [Polynomial with linear degree:]  Removing variable $x_{4}$ from all other polynomials by reducing them with polynomial $p_{3}$.

\end{description}

Finished a triangulation step, the current system is:

\begin{eqnarray*}
p_{0} &=& -u_{3}x_{2}+(u_{2}-u_{1})x_{1}+u_{3}u_{1}\\
p_{1} &=& u_{5}x_{2}-u_{4}x_{1}\\
p_{2} &=& (u_{5}u_{2}-u_{4}u_{3}+u_{3}u_{1})x_{3}-u_{5}u_{3}u_{1}\\
p_{3} &=& u_{5}x_{4}+(-u_{4}+u_{1})x_{3}-u_{5}u_{1}\\
p_{4} &=& (u_{5}-u_{3})x_{6}+(-u_{5}u_{2}+u_{4}u_{3})\\
\end{eqnarray*}




\subsection{Triangulation, step 3}

\begin{description}

\item [Choosing variable:]  Trying the variable with index 3.

\item [Variable $x_{3}$ selected:]  The number of polynomials with this variable is 1.

\item [Single polynomial with chosen variable:]  No reduction needed.

\item The triangular system has not been changed.



\end{description}





\subsection{Triangulation, step 4}

\begin{description}

\item [Choosing variable:]  Trying the variable with index 2.

\item [Variable $x_{2}$ selected:]  The number of polynomials with this variable is 2.

\item [Minimal degrees:]  1 polynomials with degree 1 and 0 polynomials with degree 1.

\item [Polynomial with linear degree:]  Removing variable $x_{2}$ from all other polynomials by reducing them with polynomial $p_{1}$.

\end{description}

Finished a triangulation step, the current system is:

\begin{eqnarray*}
p_{0} &=& (u_{5}u_{2}-u_{5}u_{1}-u_{4}u_{3})x_{1}+u_{5}u_{3}u_{1}\\
p_{1} &=& u_{5}x_{2}-u_{4}x_{1}\\
p_{2} &=& (u_{5}u_{2}-u_{4}u_{3}+u_{3}u_{1})x_{3}-u_{5}u_{3}u_{1}\\
p_{3} &=& u_{5}x_{4}+(-u_{4}+u_{1})x_{3}-u_{5}u_{1}\\
p_{4} &=& (u_{5}-u_{3})x_{6}+(-u_{5}u_{2}+u_{4}u_{3})\\
\end{eqnarray*}




\subsection{Triangulation, step 5}

\begin{description}

\item [Choosing variable:]  Trying the variable with index 1.

\item [Variable $x_{1}$ selected:]  The number of polynomials with this variable is 1.

\item [Single polynomial with chosen variable:]  No reduction needed.

\item The triangular system has not been changed.



\end{description}

The triangular system is:

\begin{eqnarray*}
p_{0} &=& (u_{5}u_{2}-u_{5}u_{1}-u_{4}u_{3})x_{1}+u_{5}u_{3}u_{1}\\
p_{1} &=& u_{5}x_{2}-u_{4}x_{1}\\
p_{2} &=& (u_{5}u_{2}-u_{4}u_{3}+u_{3}u_{1})x_{3}-u_{5}u_{3}u_{1}\\
p_{3} &=& u_{5}x_{4}+(-u_{4}+u_{1})x_{3}-u_{5}u_{1}\\
p_{4} &=& (u_{5}-u_{3})x_{6}+(-u_{5}u_{2}+u_{4}u_{3})\\
\end{eqnarray*}




\section{Final remainder}





\subsection{Final remainder for conjecture 1}

Calculating final remainder of the conclusion:
$$
g  =  -2x_{6}x_{3}x_{1}+u_{3}x_{6}x_{3}+u_{3}x_{6}x_{1}+u_{1}x_{3}x_{1}-u_{3}u_{1}x_{3}
$$
with respect to the triangular system.

\begin{enumerate}

\item Pseudo remainder with $p_{4}$ over variable $x_{6}$:
$$
g  =  (-2u_{5}u_{2}+u_{5}u_{1}+2u_{4}u_{3}-u_{3}u_{1})x_{3}x_{1}+
$$
$$
(u_{5}u_{3}u_{2}-u_{5}u_{3}u_{1}-u_{4}u_{3}^{2}+u_{3}^{2}u_{1})x_{3}+(u_{5}u_{3}u_{2}-u_{4}u_{3}^{2})x_{1}
$$
\item Pseudo remainder with $p_{3}$ over variable $x_{4}$:
$$
g  =  (-2u_{5}u_{2}+u_{5}u_{1}+2u_{4}u_{3}-u_{3}u_{1})x_{3}x_{1}+
$$
$$
(u_{5}u_{3}u_{2}-u_{5}u_{3}u_{1}-u_{4}u_{3}^{2}+u_{3}^{2}u_{1})x_{3}+(u_{5}u_{3}u_{2}-u_{4}u_{3}^{2})x_{1}
$$
\item Pseudo remainder with $p_{2}$ over variable $x_{3}$:
$$
g  =  (u_{5}^{2}u_{3}u_{2}^{2}-2u_{5}^{2}u_{3}u_{2}u_{1}+u_{5}^{2}u_{3}u_{1}^{2}-2u_{5}u_{4}u_{3}^{2}u_{2}+
$$
$$
2u_{5}u_{4}u_{3}^{2}u_{1}+u_{5}u_{3}^{2}u_{2}u_{1}-u_{5}u_{3}^{2}u_{1}^{2}+u_{4}^{2}u_{3}^{3}-u_{4}u_{3}^{3}u_{1})x_{1}+
$$
$$
(u_{5}^{2}u_{3}^{2}u_{2}u_{1}-u_{5}^{2}u_{3}^{2}u_{1}^{2}-u_{5}u_{4}u_{3}^{3}u_{1}+u_{5}u_{3}^{3}u_{1}^{2})
$$
\item Pseudo remainder with $p_{1}$ over variable $x_{2}$:
$$
g  =  (u_{5}^{2}u_{3}u_{2}^{2}-2u_{5}^{2}u_{3}u_{2}u_{1}+u_{5}^{2}u_{3}u_{1}^{2}-2u_{5}u_{4}u_{3}^{2}u_{2}+
$$
$$
2u_{5}u_{4}u_{3}^{2}u_{1}+u_{5}u_{3}^{2}u_{2}u_{1}-u_{5}u_{3}^{2}u_{1}^{2}+u_{4}^{2}u_{3}^{3}-u_{4}u_{3}^{3}u_{1})x_{1}+
$$
$$
(u_{5}^{2}u_{3}^{2}u_{2}u_{1}-u_{5}^{2}u_{3}^{2}u_{1}^{2}-u_{5}u_{4}u_{3}^{3}u_{1}+u_{5}u_{3}^{3}u_{1}^{2})
$$
\item Pseudo remainder with $p_{0}$ over variable $x_{1}$:
$$
g  =  0
$$
\end{enumerate}





\section{Prover report}

\begin{description}

\item [Status:]  The conjecture has been proved.

\item [Space Complexity:]  The biggest polynomial obtained during proof process contained 13 terms.

\item [Time Complexity:]  Time spent by the prover is 0.000 seconds.

\item[NDG conditions] are:

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

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

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

\end{itemize}
\end{description}

\end{document}
