\documentclass{amsart}
    \advance\textheight by 1.75in
    \advance\textwidth by 2in
    \advance\topmargin by -1in
    \advance\oddsidemargin by -1in
    \advance\evensidemargin by -1in
    \usepackage{amssymb}
    \parindent0pt
    \begin{document}
    \textbf{GRA001+0.ax} Directed graphs and paths






$\forall e{:}\;( \mbox{edge}(e) \ \Rightarrow \ \mbox{head\_of}(e)\ne \mbox{tail\_of}(e) )\qquad\mbox{fof}(\mbox{no\_loops},\mbox{axiom})$

$\forall e{:}\;( \mbox{edge}(e) \ \Rightarrow \ ( \mbox{vertex}(\mbox{head\_of}(e))\mbox{ and }\mbox{vertex}(\mbox{tail\_of}(e)) ) )\qquad\mbox{fof}(\mbox{edge\_ends\_are\_vertices},\mbox{axiom})$

$\mbox{complete} \ \Rightarrow \ \forall v_1,v_2{:}\;( ( \mbox{vertex}(v_1)\mbox{ and }\mbox{vertex}(v_2)\mbox{ and }v_1\ne v_2 ) \ \Rightarrow \ \exists e{:}\;( \mbox{edge}(e)\mbox{ and }( ( v_1 = \mbox{head\_of}(e)\mbox{ and }v_2 = \mbox{tail\_of}(e) ) <~> ( v_2 = \mbox{head\_of}(e)\mbox{ and }v_1 = \mbox{tail\_of}(e) ) ) ) )\qquad\mbox{fof}(\mbox{complete\_properties},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Leftarrow \ ( \mbox{vertex}(v_1)\mbox{ and }\mbox{vertex}(v_2)\mbox{ and }\exists e{:}\;( \mbox{edge}(e)\mbox{ and }v_1 = \mbox{tail\_of}(e)\mbox{ and }( ( v_2 = \mbox{head\_of}(e)\mbox{ and }p = \mbox{path\_cons}(e,\mbox{empty}) )\mbox{ or }\exists \mbox{tP}{:}\;( \mbox{path}(\mbox{head\_of}(e),v_2,\mbox{tP})\mbox{ and }p = \mbox{path\_cons}(e,\mbox{tP}) ) ) ) ) )\qquad\mbox{fof}(\mbox{path\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ ( \mbox{vertex}(v_1)\mbox{ and }\mbox{vertex}(v_2)\mbox{ and }\exists e{:}\;( \mbox{edge}(e)\mbox{ and }v_1 = \mbox{tail\_of}(e)\mbox{ and }( ( v_2 = \mbox{head\_of}(e)\mbox{ and }p = \mbox{path\_cons}(e,\mbox{empty}) ) <~> \exists \mbox{tP}{:}\;( \mbox{path}(\mbox{head\_of}(e),v_2,\mbox{tP})\mbox{ and }p = \mbox{path\_cons}(e,\mbox{tP}) ) ) ) ) )\qquad\mbox{fof}(\mbox{path\_properties},\mbox{axiom})$

$\forall v_1,v_2,p,e{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\mbox{on\_path}(e,p) ) \ \Rightarrow \ ( \mbox{edge}(e)\mbox{ and }\mbox{in\_path}(\mbox{head\_of}(e),p)\mbox{ and }\mbox{in\_path}(\mbox{tail\_of}(e),p) ) )\qquad\mbox{fof}(\mbox{on\_path\_properties},\mbox{axiom})$

$\forall v_1,v_2,p,v{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\mbox{in\_path}(v,p) ) \ \Rightarrow \ ( \mbox{vertex}(v)\mbox{ and }\exists e{:}\;( \mbox{on\_path}(e,p)\mbox{ and }( v = \mbox{head\_of}(e)\mbox{ or }v = \mbox{tail\_of}(e) ) ) ) )\qquad\mbox{fof}(\mbox{in\_path\_properties},\mbox{axiom})$

$\forall e_1,e_2{:}\;( \mbox{sequential}(e_1,e_2)\iff ( \mbox{edge}(e_1)\mbox{ and }\mbox{edge}(e_2)\mbox{ and }e_1\ne e_2\mbox{ and }\mbox{head\_of}(e_1) = \mbox{tail\_of}(e_2) ) )\qquad\mbox{fof}(\mbox{sequential\_defn},\mbox{axiom})$

$\forall p,v_1,v_2{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \forall e_1,e_2{:}\;( \mbox{precedes}(e_1,e_2,p) \ \Leftarrow \ ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }( \mbox{sequential}(e_1,e_2)\mbox{ or }\exists e_3{:}\;( \mbox{sequential}(e_1,e_3)\mbox{ and }\mbox{precedes}(e_3,e_2,p) ) ) ) ) )\qquad\mbox{fof}(\mbox{precedes\_defn},\mbox{axiom})$

$\forall p,v_1,v_2{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \forall e_1,e_2{:}\;( \mbox{precedes}(e_1,e_2,p) \ \Rightarrow \ ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }( \mbox{sequential}(e_1,e_2) <~> \exists e_3{:}\;( \mbox{sequential}(e_1,e_3)\mbox{ and }\mbox{precedes}(e_3,e_2,p) ) ) ) ) )\qquad\mbox{fof}(\mbox{precedes\_properties},\mbox{axiom})$

$\forall v_1,v_2,\mbox{sP}{:}\;( \mbox{shortest\_path}(v_1,v_2,\mbox{sP})\iff ( \mbox{path}(v_1,v_2,\mbox{sP})\mbox{ and }v_1\ne v_2\mbox{ and }\forall p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{length\_of}(\mbox{sP}) \leq \mbox{length\_of}(p) ) ) )\qquad\mbox{fof}(\mbox{shortest\_path\_defn},\mbox{axiom})$

$\forall v_1,v_2,e_1,e_2,p{:}\;( ( \mbox{shortest\_path}(v_1,v_2,p)\mbox{ and }\mbox{precedes}(e_1,e_2,p) ) \ \Rightarrow \ ( \neg\,\exists e_3{:}\;( \mbox{tail\_of}(e_3) = \mbox{tail\_of}(e_1)\mbox{ and }\mbox{head\_of}(e_3) = \mbox{head\_of}(e_2) )\mbox{ and }\neg\,\mbox{precedes}(e_2,e_1,p) ) )\qquad\mbox{fof}(\mbox{shortest\_path\_properties},\mbox{axiom})$

\medskip\textbf{GRA010+2.p} Maximal shortest path length in terms of triangles

In a complete graph, if there is a shortest path P from V1 to
 V2 with edges E1 and E2, E1 sequential to E2 means there is an
 edge E3 such that E1, E2, and E3 form a triangle, then the
 number of sequential pairs in P is the number of triangles
 in P.




$\mbox{include}(\mbox{'Axioms/GRA001+0.ax'})$

$\forall e_1,e_2,e_3{:}\;( \mbox{triangle}(e_1,e_2,e_3)\iff ( \mbox{edge}(e_1)\mbox{ and }\mbox{edge}(e_2)\mbox{ and }\mbox{edge}(e_3)\mbox{ and }\mbox{sequential}(e_1,e_2)\mbox{ and }\mbox{sequential}(e_2,e_3)\mbox{ and }\mbox{sequential}(e_3,e_1) ) )\qquad\mbox{fof}(\mbox{triangle\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{length\_of}(p) = \mbox{number\_of\_in}(\mbox{edges},p) )\qquad\mbox{fof}(\mbox{length\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = -\mbox{length\_of}(p) )\qquad\mbox{fof}(\mbox{path\_length\_sequential\_pairs},\mbox{axiom})$

$\forall p,v_1,v_2{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) ) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{sequential\_pairs\_and\_triangles},\mbox{axiom})$

$\forall \mbox{things},\mbox{inThese}{:}\;\mbox{number\_of\_in}(\mbox{things},\mbox{inThese}) \leq \mbox{number\_of\_in}(\mbox{things},\mbox{graph})\qquad\mbox{fof}(\mbox{graph\_has\_them\_all},\mbox{axiom})$

$\mbox{complete} \ \Rightarrow \ \forall v_1,v_2,e_1,e_2,p{:}\;( ( \mbox{shortest\_path}(v_1,v_2,p)\mbox{ and }\mbox{precedes}(e_1,e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) )\qquad\mbox{fof}(\mbox{sequential\_is\_triangle},\mbox{lemma})$

$\mbox{complete} \ \Rightarrow \ \forall p,v_1,v_2{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) ) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{complete\_means\_sequential\_pairs\_and\_triangles},\mbox{conjecture})$

\medskip\textbf{GRA002+1.p} Maximal shortest path length in terms of triangles

In a complete directed graph, the maximal length of a shortest
 path between two vertices is the number of triangles in the
 graph minus 1.




$\mbox{include}(\mbox{'Axioms/GRA001+0.ax'})$

$\forall e_1,e_2,e_3{:}\;( \mbox{triangle}(e_1,e_2,e_3)\iff ( \mbox{edge}(e_1)\mbox{ and }\mbox{edge}(e_2)\mbox{ and }\mbox{edge}(e_3)\mbox{ and }\mbox{sequential}(e_1,e_2)\mbox{ and }\mbox{sequential}(e_2,e_3)\mbox{ and }\mbox{sequential}(e_3,e_1) ) )\qquad\mbox{fof}(\mbox{triangle\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{length\_of}(p) = \mbox{number\_of\_in}(\mbox{edges},p) )\qquad\mbox{fof}(\mbox{length\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = -\mbox{length\_of}(p) )\qquad\mbox{fof}(\mbox{path\_length\_sequential\_pairs},\mbox{axiom})$

$\forall p,v_1,v_2{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) ) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{sequential\_pairs\_and\_triangles},\mbox{axiom})$

$\forall \mbox{things},\mbox{inThese}{:}\;\mbox{number\_of\_in}(\mbox{things},\mbox{inThese}) \leq \mbox{number\_of\_in}(\mbox{things},\mbox{graph})\qquad\mbox{fof}(\mbox{graph\_has\_them\_all},\mbox{axiom})$

$\mbox{complete} \ \Rightarrow \ \forall p,v_1,v_2{:}\;( \mbox{shortest\_path}(v_1,v_2,p) \ \Rightarrow \ -\mbox{length\_of}(p) \leq \mbox{number\_of\_in}(\mbox{triangles},\mbox{graph}) )\qquad\mbox{fof}(\mbox{maximal\_path\_length},\mbox{conjecture})$

\medskip\textbf{GRA016+1.p} 2-colored completed graph size 12 without subgraph of size 4

Find a 2-colored completed graph of size 12 without a complete
 subgraph of size 4 which all the edges have the same color.




$n_1 < n_2\mbox{ and }n_2 < n_3\mbox{ and }n_3 < n_4\mbox{ and }n_4 < n_5\mbox{ and }n_5 < n_6\mbox{ and }n_6 < n_7\mbox{ and }n_7 < n_8\mbox{ and }n_8 < n_9\mbox{ and }n_9 < n_{10}\mbox{ and }n_{10} < n_{11}\mbox{ and }n_{11} < n_{12}\qquad\mbox{fof}(\mbox{ordering},\mbox{axiom})$

$\forall a,b,c,d{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{red}(a,c)\mbox{ and }\mbox{red}(b,c)\mbox{ and }\mbox{red}(a,d)\mbox{ and }\mbox{red}(b,d)\mbox{ and }\mbox{red}(c,d) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{red\_clique},\mbox{axiom})$

$\forall a,b,c,d{:}\;( ( \mbox{green}(a,b)\mbox{ and }\mbox{green}(a,c)\mbox{ and }\mbox{green}(b,c)\mbox{ and }\mbox{green}(a,d)\mbox{ and }\mbox{green}(b,d)\mbox{ and }\mbox{green}(c,d) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{green\_clique},\mbox{axiom})$

$\forall a,b{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{green}(a,b) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{no\_overlap},\mbox{axiom})$

$\forall a,b,c{:}\;( ( a < b\mbox{ and }b < c ) \ \Rightarrow \ a < c )\qquad\mbox{fof}(\mbox{less\_than\_transitive},\mbox{axiom})$

$\forall a,b{:}\;( a < b \ \Rightarrow \ ( \mbox{red}(a,b)\mbox{ or }\mbox{green}(a,b) ) )\qquad\mbox{fof}(\mbox{partition},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip\textbf{GRA002+2.p} Maximal shortest path length in terms of triangles

In a complete directed graph, the maximal length of a shortest
 path between two vertices is the number of triangles in the
 graph minus 1.




$\mbox{include}(\mbox{'Axioms/GRA001+0.ax'})$

$\forall e_1,e_2,e_3{:}\;( \mbox{triangle}(e_1,e_2,e_3)\iff ( \mbox{edge}(e_1)\mbox{ and }\mbox{edge}(e_2)\mbox{ and }\mbox{edge}(e_3)\mbox{ and }\mbox{sequential}(e_1,e_2)\mbox{ and }\mbox{sequential}(e_2,e_3)\mbox{ and }\mbox{sequential}(e_3,e_1) ) )\qquad\mbox{fof}(\mbox{triangle\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{length\_of}(p) = \mbox{number\_of\_in}(\mbox{edges},p) )\qquad\mbox{fof}(\mbox{length\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = -\mbox{length\_of}(p) )\qquad\mbox{fof}(\mbox{path\_length\_sequential\_pairs},\mbox{axiom})$

$\forall p,v_1,v_2{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) ) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{sequential\_pairs\_and\_triangles},\mbox{axiom})$

$\forall \mbox{things},\mbox{inThese}{:}\;\mbox{number\_of\_in}(\mbox{things},\mbox{inThese}) \leq \mbox{number\_of\_in}(\mbox{things},\mbox{graph})\qquad\mbox{fof}(\mbox{graph\_has\_them\_all},\mbox{axiom})$

$\mbox{complete} \ \Rightarrow \ \forall v_1,v_2,e_1,e_2,p{:}\;( ( \mbox{shortest\_path}(v_1,v_2,p)\mbox{ and }\mbox{precedes}(e_1,e_2,p) ) \ \Rightarrow \ \exists e_3{:}\;( \mbox{edge}(e_3)\mbox{ and }\mbox{tail\_of}(e_3) = \mbox{head\_of}(e_2)\mbox{ and }\mbox{head\_of}(e_3) = \mbox{tail\_of}(e_1) ) )\qquad\mbox{fof}(\mbox{back\_edge},\mbox{lemma})$

$\mbox{complete} \ \Rightarrow \ \forall p,v_1,v_2{:}\;( \mbox{shortest\_path}(v_1,v_2,p) \ \Rightarrow \ -\mbox{length\_of}(p) \leq \mbox{number\_of\_in}(\mbox{triangles},\mbox{graph}) )\qquad\mbox{fof}(\mbox{maximal\_path\_length},\mbox{conjecture})$

\medskip\textbf{GRA002+3.p} Maximal shortest path length in terms of triangles

In a complete directed graph, the maximal length of a shortest
 path between two vertices is the number of triangles in the
 graph minus 1.




$\mbox{include}(\mbox{'Axioms/GRA001+0.ax'})$

$\forall e_1,e_2,e_3{:}\;( \mbox{triangle}(e_1,e_2,e_3)\iff ( \mbox{edge}(e_1)\mbox{ and }\mbox{edge}(e_2)\mbox{ and }\mbox{edge}(e_3)\mbox{ and }\mbox{sequential}(e_1,e_2)\mbox{ and }\mbox{sequential}(e_2,e_3)\mbox{ and }\mbox{sequential}(e_3,e_1) ) )\qquad\mbox{fof}(\mbox{triangle\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{length\_of}(p) = \mbox{number\_of\_in}(\mbox{edges},p) )\qquad\mbox{fof}(\mbox{length\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = -\mbox{length\_of}(p) )\qquad\mbox{fof}(\mbox{path\_length\_sequential\_pairs},\mbox{axiom})$

$\forall p,v_1,v_2{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) ) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{sequential\_pairs\_and\_triangles},\mbox{axiom})$

$\forall \mbox{things},\mbox{inThese}{:}\;\mbox{number\_of\_in}(\mbox{things},\mbox{inThese}) \leq \mbox{number\_of\_in}(\mbox{things},\mbox{graph})\qquad\mbox{fof}(\mbox{graph\_has\_them\_all},\mbox{axiom})$

$\mbox{complete} \ \Rightarrow \ \forall v_1,v_2,e_1,e_2,p{:}\;( ( \mbox{shortest\_path}(v_1,v_2,p)\mbox{ and }\mbox{precedes}(e_1,e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) )\qquad\mbox{fof}(\mbox{sequential\_is\_triangle},\mbox{lemma})$

$\mbox{complete} \ \Rightarrow \ \forall p,v_1,v_2{:}\;( \mbox{shortest\_path}(v_1,v_2,p) \ \Rightarrow \ -\mbox{length\_of}(p) \leq \mbox{number\_of\_in}(\mbox{triangles},\mbox{graph}) )\qquad\mbox{fof}(\mbox{maximal\_path\_length},\mbox{conjecture})$

\medskip\textbf{GRA005+1.p} Maximal shortest path length in terms of triangles

In a shortest path P from V1 to V2 with edges E1 and E2, E1
 preceding E2, there is no edge from the tail of E1 to the
 head of E2.




$\mbox{include}(\mbox{'Axioms/GRA001+0.ax'})$

$\forall e_1,e_2,e_3{:}\;( \mbox{triangle}(e_1,e_2,e_3)\iff ( \mbox{edge}(e_1)\mbox{ and }\mbox{edge}(e_2)\mbox{ and }\mbox{edge}(e_3)\mbox{ and }\mbox{sequential}(e_1,e_2)\mbox{ and }\mbox{sequential}(e_2,e_3)\mbox{ and }\mbox{sequential}(e_3,e_1) ) )\qquad\mbox{fof}(\mbox{triangle\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{length\_of}(p) = \mbox{number\_of\_in}(\mbox{edges},p) )\qquad\mbox{fof}(\mbox{length\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = -\mbox{length\_of}(p) )\qquad\mbox{fof}(\mbox{path\_length\_sequential\_pairs},\mbox{axiom})$

$\forall p,v_1,v_2{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) ) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{sequential\_pairs\_and\_triangles},\mbox{axiom})$

$\forall \mbox{things},\mbox{inThese}{:}\;\mbox{number\_of\_in}(\mbox{things},\mbox{inThese}) \leq \mbox{number\_of\_in}(\mbox{things},\mbox{graph})\qquad\mbox{fof}(\mbox{graph\_has\_them\_all},\mbox{axiom})$

$\forall v_1,v_2,e_1,e_2,p{:}\;( ( \mbox{shortest\_path}(v_1,v_2,p)\mbox{ and }\mbox{precedes}(e_1,e_2,p) ) \ \Rightarrow \ \neg\,\exists e_3{:}\;( \mbox{edge}(e_3)\mbox{ and }\mbox{tail\_of}(e_3) = \mbox{tail\_of}(e_1)\mbox{ and }\mbox{head\_of}(e_3) = \mbox{head\_of}(e_2) ) )\qquad\mbox{fof}(\mbox{no\_short\_cut\_edge},\mbox{conjecture})$

\medskip\textbf{GRA032$\wedge$2.p} R(3,6) $>$ 16






$\exists g{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to ( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o}{:}\;( \forall \mbox{xx}{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xy}{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( ( g@ \mbox{xx}@ \mbox{xy} ) \ \Rightarrow \ ( g@ \mbox{xy}@ \mbox{xx} ) )\mbox{ and }\forall \mbox{xx}_0{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xx}_1{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xx}_2{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_0{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_1{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o}{:}\;( ( \mbox{xp}_0@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_0\mbox{ and }\mbox{xp}_1@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_2 ) \ \Rightarrow \ ( \neg\,g@ \mbox{xx}_1@ \mbox{xx}_0\mbox{ or }\neg\,g@ \mbox{xx}_2@ \mbox{xx}_0\mbox{ or }\neg\,g@ \mbox{xx}_2@ \mbox{xx}_1 ) )\mbox{ and }\forall \mbox{xx}_0{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xx}_1{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xx}_2{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xx}_3{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xx}_4{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xx}_5{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_0{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_1{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_2{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_3{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_4{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o}{:}\;( ( \mbox{xp}_0@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_4\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_5\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_0\mbox{ and }\mbox{xp}_1@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_4\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_5\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_1\mbox{ and }\mbox{xp}_2@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_4\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_5\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_2\mbox{ and }\mbox{xp}_3@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_4\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_5\mbox{ and }\neg\,\mbox{xp}_4@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_4@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_4@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_4@ \mbox{xx}_3\mbox{ and }\mbox{xp}_4@ \mbox{xx}_4\mbox{ and }\neg\,\mbox{xp}_4@ \mbox{xx}_5 ) \ \Rightarrow \ ( g@ \mbox{xx}_1@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_2@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_2@ \mbox{xx}_1\mbox{ or }g@ \mbox{xx}_3@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_3@ \mbox{xx}_1\mbox{ or }g@ \mbox{xx}_3@ \mbox{xx}_2\mbox{ or }g@ \mbox{xx}_4@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_4@ \mbox{xx}_1\mbox{ or }g@ \mbox{xx}_4@ \mbox{xx}_2\mbox{ or }g@ \mbox{xx}_4@ \mbox{xx}_3\mbox{ or }g@ \mbox{xx}_5@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_5@ \mbox{xx}_1\mbox{ or }g@ \mbox{xx}_5@ \mbox{xx}_2\mbox{ or }g@ \mbox{xx}_5@ \mbox{xx}_3\mbox{ or }g@ \mbox{xx}_5@ \mbox{xx}_4 ) ) )\qquad\mbox{thf}(\mbox{ramsey\_l\_3\_6\_16a},\mbox{conjecture})$

\medskip\textbf{GRA029$\wedge$2.p} R(4,4) $>$ 16






$\exists g{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to ( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o}{:}\;( \forall \mbox{xx}{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xy}{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( ( g@ \mbox{xx}@ \mbox{xy} ) \ \Rightarrow \ ( g@ \mbox{xy}@ \mbox{xx} ) )\mbox{ and }\forall \mbox{xx}_0{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xx}_1{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xx}_2{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xx}_3{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_0{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_1{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_2{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o}{:}\;( ( \mbox{xp}_0@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_0\mbox{ and }\mbox{xp}_1@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_1\mbox{ and }\mbox{xp}_2@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_3 ) \ \Rightarrow \ ( \neg\,g@ \mbox{xx}_1@ \mbox{xx}_0\mbox{ or }\neg\,g@ \mbox{xx}_2@ \mbox{xx}_0\mbox{ or }\neg\,g@ \mbox{xx}_2@ \mbox{xx}_1\mbox{ or }\neg\,g@ \mbox{xx}_3@ \mbox{xx}_0\mbox{ or }\neg\,g@ \mbox{xx}_3@ \mbox{xx}_1\mbox{ or }\neg\,g@ \mbox{xx}_3@ \mbox{xx}_2 ) )\mbox{ and }\forall \mbox{xx}_0{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xx}_1{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xx}_2{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xx}_3{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_0{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_1{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_2{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o}{:}\;( ( \mbox{xp}_0@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_0\mbox{ and }\mbox{xp}_1@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_1\mbox{ and }\mbox{xp}_2@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_3 ) \ \Rightarrow \ ( g@ \mbox{xx}_1@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_2@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_2@ \mbox{xx}_1\mbox{ or }g@ \mbox{xx}_3@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_3@ \mbox{xx}_1\mbox{ or }g@ \mbox{xx}_3@ \mbox{xx}_2 ) ) )\qquad\mbox{thf}(\mbox{ramsey\_l\_4\_4\_16a},\mbox{conjecture})$

\medskip\textbf{GRA025+1.p} 2-colored completed graph size 14 without subgraph of size 6

Find a 2-colored completed graph of size 14 without a complete
 subgraph of size 6 which all the edges have the same color.




$n_1 < n_2\mbox{ and }n_2 < n_3\mbox{ and }n_3 < n_4\mbox{ and }n_4 < n_5\mbox{ and }n_5 < n_6\mbox{ and }n_6 < n_7\mbox{ and }n_7 < n_8\mbox{ and }n_8 < n_9\mbox{ and }n_9 < n_{10}\mbox{ and }n_{10} < n_{11}\mbox{ and }n_{11} < n_{12}\mbox{ and }n_{12} < n_{13}\mbox{ and }n_{13} < n_{14}\qquad\mbox{fof}(\mbox{ordering},\mbox{axiom})$

$\forall a,b,c,d,e,f{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{red}(a,c)\mbox{ and }\mbox{red}(b,c)\mbox{ and }\mbox{red}(a,d)\mbox{ and }\mbox{red}(b,d)\mbox{ and }\mbox{red}(c,d)\mbox{ and }\mbox{red}(a,e)\mbox{ and }\mbox{red}(b,e)\mbox{ and }\mbox{red}(c,e)\mbox{ and }\mbox{red}(d,e)\mbox{ and }\mbox{red}(a,f)\mbox{ and }\mbox{red}(b,f)\mbox{ and }\mbox{red}(c,f)\mbox{ and }\mbox{red}(d,f)\mbox{ and }\mbox{red}(e,f) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{red\_clique},\mbox{axiom})$

$\forall a,b,c,d,e,f{:}\;( ( \mbox{green}(a,b)\mbox{ and }\mbox{green}(a,c)\mbox{ and }\mbox{green}(b,c)\mbox{ and }\mbox{green}(a,d)\mbox{ and }\mbox{green}(b,d)\mbox{ and }\mbox{green}(c,d)\mbox{ and }\mbox{green}(a,e)\mbox{ and }\mbox{green}(b,e)\mbox{ and }\mbox{green}(c,e)\mbox{ and }\mbox{green}(d,e)\mbox{ and }\mbox{green}(a,f)\mbox{ and }\mbox{green}(b,f)\mbox{ and }\mbox{green}(c,f)\mbox{ and }\mbox{green}(d,f)\mbox{ and }\mbox{green}(e,f) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{green\_clique},\mbox{axiom})$

$\forall a,b{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{green}(a,b) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{no\_overlap},\mbox{axiom})$

$\forall a,b,c{:}\;( ( a < b\mbox{ and }b < c ) \ \Rightarrow \ a < c )\qquad\mbox{fof}(\mbox{less\_than\_transitive},\mbox{axiom})$

$\forall a,b{:}\;( a < b \ \Rightarrow \ ( \mbox{red}(a,b)\mbox{ or }\mbox{green}(a,b) ) )\qquad\mbox{fof}(\mbox{partition},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip\textbf{GRA029$\wedge$1.p} R(4,4) $>$ 16






$\exists g{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to ( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( \forall \mbox{xx}{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xy}{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o}{:}\;( ( g@ \mbox{xx}@ \mbox{xy} ) \ \Rightarrow \ ( g@ \mbox{xy}@ \mbox{xx} ) )\mbox{ and }\forall \mbox{xx}_0{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xx}_1{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xx}_2{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xx}_3{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xp}_0{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_1{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_2{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( ( \mbox{xp}_0@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_0\mbox{ and }\mbox{xp}_1@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_1\mbox{ and }\mbox{xp}_2@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_3 ) \ \Rightarrow \ ( \neg\,g@ \mbox{xx}_1@ \mbox{xx}_0\mbox{ or }\neg\,g@ \mbox{xx}_2@ \mbox{xx}_0\mbox{ or }\neg\,g@ \mbox{xx}_2@ \mbox{xx}_1\mbox{ or }\neg\,g@ \mbox{xx}_3@ \mbox{xx}_0\mbox{ or }\neg\,g@ \mbox{xx}_3@ \mbox{xx}_1\mbox{ or }\neg\,g@ \mbox{xx}_3@ \mbox{xx}_2 ) )\mbox{ and }\forall \mbox{xx}_0{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xx}_1{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xx}_2{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xx}_3{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xp}_0{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_1{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_2{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( ( \mbox{xp}_0@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_0\mbox{ and }\mbox{xp}_1@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_1\mbox{ and }\mbox{xp}_2@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_3 ) \ \Rightarrow \ ( g@ \mbox{xx}_1@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_2@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_2@ \mbox{xx}_1\mbox{ or }g@ \mbox{xx}_3@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_3@ \mbox{xx}_1\mbox{ or }g@ \mbox{xx}_3@ \mbox{xx}_2 ) ) )\qquad\mbox{thf}(\mbox{ramsey\_l\_4\_4}_{16},\mbox{conjecture})$

\medskip\textbf{GRA014+1.p} 2-colored completed graph size 6 without subgraph of size 3

Find a 2-colored completed graph of size 6 without a complete
 subgraph of size 3 which all the edges have the same color.




$\forall a,b,c{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{red}(b,c)\mbox{ and }\mbox{red}(a,c) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{red\_clique},\mbox{axiom})$

$\forall a,b,c{:}\;( ( \mbox{green}(a,b)\mbox{ and }\mbox{green}(b,c)\mbox{ and }\mbox{green}(a,c) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{green\_clique},\mbox{axiom})$

$n_1 < n_2\mbox{ and }n_2 < n_3\mbox{ and }n_3 < n_4\mbox{ and }n_4 < n_5\mbox{ and }n_5 < n_6\qquad\mbox{fof}(\mbox{ordering},\mbox{axiom})$

$\forall a,b,c{:}\;( ( a < b\mbox{ and }b < c ) \ \Rightarrow \ a < c )\qquad\mbox{fof}(\mbox{less\_than\_transitive},\mbox{axiom})$

$\forall a,b{:}\;( a < b \ \Rightarrow \ ( \mbox{red}(a,b)\mbox{ or }\mbox{green}(a,b) ) )\qquad\mbox{fof}(\mbox{partition},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip\textbf{GRA001-1.p} Clauses from a labelled graph

Consider a graph with the edges labelled. For example
 *       :
 A /   \ B   :
 *--C--*    :
 D \   / E   :
 *       :
 Assign 0 or 1 arbitarily to nodes of the graph. For each node
 of the graph, we associate a set of clauses as follows :
 (1) Every label of an edge emanating from that node will
 occur in each clause (of the set of clauses generated
 from that node).
 (2) If the node is assigned 0, then the number of negated
 literals in each of the generated clauses is to be odd.
 Generate all such clauses for that node.
 (3) If the node is assigned 1, then the number of negated
 literals in each of the generated clauses is to be even.
 Generate all such clauses for that node.
 Tseitin's result is this: the sum (mod 2) of the 0's and 1's
 assigned to the nodes of the graph equals 1 iff the set
 of generated clauses is inconsistent. For example, if the top
 node of the above graph is assigned 1, and all other nodes
 0, then the set of generated clauses will be inconsistent.




$a\mbox{ or }b\qquad\mbox{cnf}(\mbox{clause}_1,\mbox{negated\_conjecture})$

$a \ \Rightarrow \ \neg\,b\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{negated\_conjecture})$

$d \ \Rightarrow \ ( a\mbox{ or }c )\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{negated\_conjecture})$

$c \ \Rightarrow \ ( a\mbox{ or }d )\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{negated\_conjecture})$

$a \ \Rightarrow \ ( c\mbox{ or }d )\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{negated\_conjecture})$

$( a\mbox{ and }c ) \ \Rightarrow \ \neg\,d\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{negated\_conjecture})$

$e \ \Rightarrow \ ( b\mbox{ or }c )\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{negated\_conjecture})$

$c \ \Rightarrow \ ( b\mbox{ or }e )\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{negated\_conjecture})$

$b \ \Rightarrow \ ( c\mbox{ or }e )\qquad\mbox{cnf}(\mbox{clause}_9,\mbox{negated\_conjecture})$

$( b\mbox{ and }c ) \ \Rightarrow \ \neg\,e\qquad\mbox{cnf}(\mbox{clause}_{10},\mbox{negated\_conjecture})$

$e \ \Rightarrow \ d\qquad\mbox{cnf}(\mbox{clause}_{11},\mbox{negated\_conjecture})$

$d \ \Rightarrow \ e\qquad\mbox{cnf}(\mbox{clause}_{12},\mbox{negated\_conjecture})$

\medskip\textbf{GRA027$\wedge$1.p} R(3,3) $>$ 4






$\exists g{:}\;( \mbox{\$o}\to \mbox{\$o} )\to ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( \forall \mbox{xx}{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xy}{:}\;\mbox{\$o}\to \mbox{\$o}{:}\;( ( g@ \mbox{xx}@ \mbox{xy} ) \ \Rightarrow \ ( g@ \mbox{xy}@ \mbox{xx} ) )\mbox{ and }\forall \mbox{xx}_0{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xx}_1{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xx}_2{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xp}_0{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_1{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( ( \mbox{xp}_0@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_0\mbox{ and }\mbox{xp}_1@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_2 ) \ \Rightarrow \ ( \neg\,g@ \mbox{xx}_1@ \mbox{xx}_0\mbox{ or }\neg\,g@ \mbox{xx}_2@ \mbox{xx}_0\mbox{ or }\neg\,g@ \mbox{xx}_2@ \mbox{xx}_1 ) )\mbox{ and }\forall \mbox{xx}_0{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xx}_1{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xx}_2{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xp}_0{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_1{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( ( \mbox{xp}_0@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_0\mbox{ and }\mbox{xp}_1@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_2 ) \ \Rightarrow \ ( g@ \mbox{xx}_1@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_2@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_2@ \mbox{xx}_1 ) ) )\qquad\mbox{thf}(\mbox{ramsey\_l\_3\_3}_4,\mbox{conjecture})$

\medskip\textbf{GRA007+1.p} Maximal shortest path length in terms of triangles

In a complete graph with a shortest path P from V1 to V2 with
 edges E1 and E2, E1 preceding E2, there's an edge from the
 head of E2 to the tail of E1 (a back edge).




$\mbox{include}(\mbox{'Axioms/GRA001+0.ax'})$

$\forall e_1,e_2,e_3{:}\;( \mbox{triangle}(e_1,e_2,e_3)\iff ( \mbox{edge}(e_1)\mbox{ and }\mbox{edge}(e_2)\mbox{ and }\mbox{edge}(e_3)\mbox{ and }\mbox{sequential}(e_1,e_2)\mbox{ and }\mbox{sequential}(e_2,e_3)\mbox{ and }\mbox{sequential}(e_3,e_1) ) )\qquad\mbox{fof}(\mbox{triangle\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{length\_of}(p) = \mbox{number\_of\_in}(\mbox{edges},p) )\qquad\mbox{fof}(\mbox{length\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = -\mbox{length\_of}(p) )\qquad\mbox{fof}(\mbox{path\_length\_sequential\_pairs},\mbox{axiom})$

$\forall p,v_1,v_2{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) ) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{sequential\_pairs\_and\_triangles},\mbox{axiom})$

$\forall \mbox{things},\mbox{inThese}{:}\;\mbox{number\_of\_in}(\mbox{things},\mbox{inThese}) \leq \mbox{number\_of\_in}(\mbox{things},\mbox{graph})\qquad\mbox{fof}(\mbox{graph\_has\_them\_all},\mbox{axiom})$

$\mbox{complete} \ \Rightarrow \ \forall v_1,v_2,e_1,e_2,p{:}\;( ( \mbox{shortest\_path}(v_1,v_2,p)\mbox{ and }\mbox{precedes}(e_1,e_2,p) ) \ \Rightarrow \ \exists e_3{:}\;( \mbox{edge}(e_3)\mbox{ and }\mbox{tail\_of}(e_3) = \mbox{head\_of}(e_2)\mbox{ and }\mbox{head\_of}(e_3) = \mbox{tail\_of}(e_1) ) )\qquad\mbox{fof}(\mbox{back\_edge},\mbox{conjecture})$

\medskip\textbf{GRA031$\wedge$1.p} R(3,5) $\leq$ 16






$\forall g{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to ( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( \forall \mbox{xx}{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xy}{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o}{:}\;( ( g@ \mbox{xx}@ \mbox{xy} ) \ \Rightarrow \ ( g@ \mbox{xy}@ \mbox{xx} ) ) \ \Rightarrow \ ( \exists \mbox{xx}_0{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xx}_1{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xx}_2{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xp}_0{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_1{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( \mbox{xp}_0@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_0\mbox{ and }\mbox{xp}_1@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_2\mbox{ and }g@ \mbox{xx}_1@ \mbox{xx}_0\mbox{ and }g@ \mbox{xx}_2@ \mbox{xx}_0\mbox{ and }g@ \mbox{xx}_2@ \mbox{xx}_1 )\mbox{ or }\exists \mbox{xx}_0{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xx}_1{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xx}_2{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xx}_3{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xx}_4{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xp}_0{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_1{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_2{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_3{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( \mbox{xp}_0@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_4\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_0\mbox{ and }\mbox{xp}_1@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_4\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_1\mbox{ and }\mbox{xp}_2@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_4\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_2\mbox{ and }\mbox{xp}_3@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_4\mbox{ and }\neg\,g@ \mbox{xx}_1@ \mbox{xx}_0\mbox{ and }\neg\,g@ \mbox{xx}_2@ \mbox{xx}_0\mbox{ and }\neg\,g@ \mbox{xx}_2@ \mbox{xx}_1\mbox{ and }\neg\,g@ \mbox{xx}_3@ \mbox{xx}_0\mbox{ and }\neg\,g@ \mbox{xx}_3@ \mbox{xx}_1\mbox{ and }\neg\,g@ \mbox{xx}_3@ \mbox{xx}_2\mbox{ and }\neg\,g@ \mbox{xx}_4@ \mbox{xx}_0\mbox{ and }\neg\,g@ \mbox{xx}_4@ \mbox{xx}_1\mbox{ and }\neg\,g@ \mbox{xx}_4@ \mbox{xx}_2\mbox{ and }\neg\,g@ \mbox{xx}_4@ \mbox{xx}_3 ) ) )\qquad\mbox{thf}(\mbox{ramsey\_u\_3\_5}_{16},\mbox{conjecture})$

\medskip\textbf{GRA021+1.p} 2-colored completed graph size 12 without subgraph of size 5

Find a 2-colored completed graph of size 12 without a complete
 subgraph of size 5 which all the edges have the same color.




$n_1 < n_2\mbox{ and }n_2 < n_3\mbox{ and }n_3 < n_4\mbox{ and }n_4 < n_5\mbox{ and }n_5 < n_6\mbox{ and }n_6 < n_7\mbox{ and }n_7 < n_8\mbox{ and }n_8 < n_9\mbox{ and }n_9 < n_{10}\mbox{ and }n_{10} < n_{11}\mbox{ and }n_{11} < n_{12}\qquad\mbox{fof}(\mbox{ordering},\mbox{axiom})$

$\forall a,b,c,d,e{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{red}(a,c)\mbox{ and }\mbox{red}(b,c)\mbox{ and }\mbox{red}(a,d)\mbox{ and }\mbox{red}(b,d)\mbox{ and }\mbox{red}(c,d)\mbox{ and }\mbox{red}(a,e)\mbox{ and }\mbox{red}(b,e)\mbox{ and }\mbox{red}(c,e)\mbox{ and }\mbox{red}(d,e) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{red\_clique},\mbox{axiom})$

$\forall a,b,c,d,e{:}\;( ( \mbox{green}(a,b)\mbox{ and }\mbox{green}(a,c)\mbox{ and }\mbox{green}(b,c)\mbox{ and }\mbox{green}(a,d)\mbox{ and }\mbox{green}(b,d)\mbox{ and }\mbox{green}(c,d)\mbox{ and }\mbox{green}(a,e)\mbox{ and }\mbox{green}(b,e)\mbox{ and }\mbox{green}(c,e)\mbox{ and }\mbox{green}(d,e) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{green\_clique},\mbox{axiom})$

$\forall a,b{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{green}(a,b) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{no\_overlap},\mbox{axiom})$

$\forall a,b,c{:}\;( ( a < b\mbox{ and }b < c ) \ \Rightarrow \ a < c )\qquad\mbox{fof}(\mbox{less\_than\_transitive},\mbox{axiom})$

$\forall a,b{:}\;( a < b \ \Rightarrow \ ( \mbox{red}(a,b)\mbox{ or }\mbox{green}(a,b) ) )\qquad\mbox{fof}(\mbox{partition},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip\textbf{GRA075+1.p} Directed graphs and paths






$\mbox{include}(\mbox{'Axioms/GRA001+0.ax'})$

\medskip\textbf{GRA026+1.p} 2-colored completed graph size 20 without subgraph of size 6

Find a 2-colored completed graph of size 20 without a complete
 subgraph of size 6 which all the edges have the same color.




$n_1 < n_2\mbox{ and }n_2 < n_3\mbox{ and }n_3 < n_4\mbox{ and }n_4 < n_5\mbox{ and }n_5 < n_6\mbox{ and }n_6 < n_7\mbox{ and }n_7 < n_8\mbox{ and }n_8 < n_9\mbox{ and }n_9 < n_{10}\mbox{ and }n_{10} < n_{11}\mbox{ and }n_{11} < n_{12}\mbox{ and }n_{12} < n_{13}\mbox{ and }n_{13} < n_{14}\mbox{ and }n_{14} < n_{15}\mbox{ and }n_{15} < n_{16}\mbox{ and }n_{16} < n_{17}\mbox{ and }n_{17} < n_{18}\mbox{ and }n_{18} < n_{19}\mbox{ and }n_{19} < n_{20}\qquad\mbox{fof}(\mbox{ordering},\mbox{axiom})$

$\forall a,b,c,d,e,f{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{red}(a,c)\mbox{ and }\mbox{red}(b,c)\mbox{ and }\mbox{red}(a,d)\mbox{ and }\mbox{red}(b,d)\mbox{ and }\mbox{red}(c,d)\mbox{ and }\mbox{red}(a,e)\mbox{ and }\mbox{red}(b,e)\mbox{ and }\mbox{red}(c,e)\mbox{ and }\mbox{red}(d,e)\mbox{ and }\mbox{red}(a,f)\mbox{ and }\mbox{red}(b,f)\mbox{ and }\mbox{red}(c,f)\mbox{ and }\mbox{red}(d,f)\mbox{ and }\mbox{red}(e,f) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{red\_clique},\mbox{axiom})$

$\forall a,b,c,d,e,f{:}\;( ( \mbox{green}(a,b)\mbox{ and }\mbox{green}(a,c)\mbox{ and }\mbox{green}(b,c)\mbox{ and }\mbox{green}(a,d)\mbox{ and }\mbox{green}(b,d)\mbox{ and }\mbox{green}(c,d)\mbox{ and }\mbox{green}(a,e)\mbox{ and }\mbox{green}(b,e)\mbox{ and }\mbox{green}(c,e)\mbox{ and }\mbox{green}(d,e)\mbox{ and }\mbox{green}(a,f)\mbox{ and }\mbox{green}(b,f)\mbox{ and }\mbox{green}(c,f)\mbox{ and }\mbox{green}(d,f)\mbox{ and }\mbox{green}(e,f) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{green\_clique},\mbox{axiom})$

$\forall a,b{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{green}(a,b) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{no\_overlap},\mbox{axiom})$

$\forall a,b,c{:}\;( ( a < b\mbox{ and }b < c ) \ \Rightarrow \ a < c )\qquad\mbox{fof}(\mbox{less\_than\_transitive},\mbox{axiom})$

$\forall a,b{:}\;( a < b \ \Rightarrow \ ( \mbox{red}(a,b)\mbox{ or }\mbox{green}(a,b) ) )\qquad\mbox{fof}(\mbox{partition},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip\textbf{GRA003+1.p} Parts of paths

In a shortest path P from V1 to V2 with edges E1 and E2, E1
 preceding E2, P is a path, V1 and V2 are vertices, and E1 and
 E2 are distinct edges.




$\mbox{include}(\mbox{'Axioms/GRA001+0.ax'})$

$\forall e_1,e_2,e_3{:}\;( \mbox{triangle}(e_1,e_2,e_3)\iff ( \mbox{edge}(e_1)\mbox{ and }\mbox{edge}(e_2)\mbox{ and }\mbox{edge}(e_3)\mbox{ and }\mbox{sequential}(e_1,e_2)\mbox{ and }\mbox{sequential}(e_2,e_3)\mbox{ and }\mbox{sequential}(e_3,e_1) ) )\qquad\mbox{fof}(\mbox{triangle\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{length\_of}(p) = \mbox{number\_of\_in}(\mbox{edges},p) )\qquad\mbox{fof}(\mbox{length\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = -\mbox{length\_of}(p) )\qquad\mbox{fof}(\mbox{path\_length\_sequential\_pairs},\mbox{axiom})$

$\forall p,v_1,v_2{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) ) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{sequential\_pairs\_and\_triangles},\mbox{axiom})$

$\forall \mbox{things},\mbox{inThese}{:}\;\mbox{number\_of\_in}(\mbox{things},\mbox{inThese}) \leq \mbox{number\_of\_in}(\mbox{things},\mbox{graph})\qquad\mbox{fof}(\mbox{graph\_has\_them\_all},\mbox{axiom})$

$\forall v_1,v_2,e_1,e_2,p{:}\;( ( \mbox{shortest\_path}(v_1,v_2,p)\mbox{ and }\mbox{precedes}(e_1,e_2,p) ) \ \Rightarrow \ ( \mbox{vertex}(v_1)\mbox{ and }\mbox{vertex}(v_2)\mbox{ and }v_1\ne v_2\mbox{ and }\mbox{edge}(e_1)\mbox{ and }\mbox{edge}(e_2)\mbox{ and }e_1\ne e_2\mbox{ and }\mbox{path}(v_1,v_2,p) ) )\qquad\mbox{fof}(\mbox{vertices\_and\_edges},\mbox{conjecture})$

\medskip\textbf{GRA008+1.p} Maximal shortest path length in terms of triangles

In a complete graph with a shortest path P from V1 to V2 with
 edges E1 and E2, E1 preceding and sequential to E2, there is
 an edge E3 such that E1, E2, and E3 form a triangle.




$\mbox{include}(\mbox{'Axioms/GRA001+0.ax'})$

$\forall e_1,e_2,e_3{:}\;( \mbox{triangle}(e_1,e_2,e_3)\iff ( \mbox{edge}(e_1)\mbox{ and }\mbox{edge}(e_2)\mbox{ and }\mbox{edge}(e_3)\mbox{ and }\mbox{sequential}(e_1,e_2)\mbox{ and }\mbox{sequential}(e_2,e_3)\mbox{ and }\mbox{sequential}(e_3,e_1) ) )\qquad\mbox{fof}(\mbox{triangle\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{length\_of}(p) = \mbox{number\_of\_in}(\mbox{edges},p) )\qquad\mbox{fof}(\mbox{length\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = -\mbox{length\_of}(p) )\qquad\mbox{fof}(\mbox{path\_length\_sequential\_pairs},\mbox{axiom})$

$\forall p,v_1,v_2{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) ) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{sequential\_pairs\_and\_triangles},\mbox{axiom})$

$\forall \mbox{things},\mbox{inThese}{:}\;\mbox{number\_of\_in}(\mbox{things},\mbox{inThese}) \leq \mbox{number\_of\_in}(\mbox{things},\mbox{graph})\qquad\mbox{fof}(\mbox{graph\_has\_them\_all},\mbox{axiom})$

$\mbox{complete} \ \Rightarrow \ \forall v_1,v_2,e_1,e_2,p{:}\;( ( \mbox{shortest\_path}(v_1,v_2,p)\mbox{ and }\mbox{precedes}(e_1,e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) )\qquad\mbox{fof}(\mbox{sequential\_is\_triangle},\mbox{conjecture})$

\medskip\textbf{GRA024+1.p} 2-colored completed graph size 11 without subgraph of size 6

Find a 2-colored completed graph of size 11 without a complete
 subgraph of size 6 which all the edges have the same color.




$n_1 < n_2\mbox{ and }n_2 < n_3\mbox{ and }n_3 < n_4\mbox{ and }n_4 < n_5\mbox{ and }n_5 < n_6\mbox{ and }n_6 < n_7\mbox{ and }n_7 < n_8\mbox{ and }n_8 < n_9\mbox{ and }n_9 < n_{10}\mbox{ and }n_{10} < n_{11}\qquad\mbox{fof}(\mbox{ordering},\mbox{axiom})$

$\forall a,b,c,d,e,f{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{red}(a,c)\mbox{ and }\mbox{red}(b,c)\mbox{ and }\mbox{red}(a,d)\mbox{ and }\mbox{red}(b,d)\mbox{ and }\mbox{red}(c,d)\mbox{ and }\mbox{red}(a,e)\mbox{ and }\mbox{red}(b,e)\mbox{ and }\mbox{red}(c,e)\mbox{ and }\mbox{red}(d,e)\mbox{ and }\mbox{red}(a,f)\mbox{ and }\mbox{red}(b,f)\mbox{ and }\mbox{red}(c,f)\mbox{ and }\mbox{red}(d,f)\mbox{ and }\mbox{red}(e,f) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{red\_clique},\mbox{axiom})$

$\forall a,b,c,d,e,f{:}\;( ( \mbox{green}(a,b)\mbox{ and }\mbox{green}(a,c)\mbox{ and }\mbox{green}(b,c)\mbox{ and }\mbox{green}(a,d)\mbox{ and }\mbox{green}(b,d)\mbox{ and }\mbox{green}(c,d)\mbox{ and }\mbox{green}(a,e)\mbox{ and }\mbox{green}(b,e)\mbox{ and }\mbox{green}(c,e)\mbox{ and }\mbox{green}(d,e)\mbox{ and }\mbox{green}(a,f)\mbox{ and }\mbox{green}(b,f)\mbox{ and }\mbox{green}(c,f)\mbox{ and }\mbox{green}(d,f)\mbox{ and }\mbox{green}(e,f) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{green\_clique},\mbox{axiom})$

$\forall a,b{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{green}(a,b) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{no\_overlap},\mbox{axiom})$

$\forall a,b,c{:}\;( ( a < b\mbox{ and }b < c ) \ \Rightarrow \ a < c )\qquad\mbox{fof}(\mbox{less\_than\_transitive},\mbox{axiom})$

$\forall a,b{:}\;( a < b \ \Rightarrow \ ( \mbox{red}(a,b)\mbox{ or }\mbox{green}(a,b) ) )\qquad\mbox{fof}(\mbox{partition},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip\textbf{GRA031$\wedge$2.p} R(3,5) $\leq$ 16






$\forall g{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to ( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o}{:}\;( \forall \mbox{xx}{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xy}{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( ( g@ \mbox{xx}@ \mbox{xy} ) \ \Rightarrow \ ( g@ \mbox{xy}@ \mbox{xx} ) ) \ \Rightarrow \ ( \exists \mbox{xx}_0{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xx}_1{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xx}_2{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_0{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_1{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o}{:}\;( \mbox{xp}_0@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_0\mbox{ and }\mbox{xp}_1@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_2\mbox{ and }g@ \mbox{xx}_1@ \mbox{xx}_0\mbox{ and }g@ \mbox{xx}_2@ \mbox{xx}_0\mbox{ and }g@ \mbox{xx}_2@ \mbox{xx}_1 )\mbox{ or }\exists \mbox{xx}_0{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xx}_1{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xx}_2{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xx}_3{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xx}_4{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_0{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_1{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_2{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_3{:}\;( ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o} )\to \mbox{\$o}{:}\;( \mbox{xp}_0@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_4\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_0\mbox{ and }\mbox{xp}_1@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_4\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_1\mbox{ and }\mbox{xp}_2@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_4\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_2\mbox{ and }\mbox{xp}_3@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_4\mbox{ and }\neg\,g@ \mbox{xx}_1@ \mbox{xx}_0\mbox{ and }\neg\,g@ \mbox{xx}_2@ \mbox{xx}_0\mbox{ and }\neg\,g@ \mbox{xx}_2@ \mbox{xx}_1\mbox{ and }\neg\,g@ \mbox{xx}_3@ \mbox{xx}_0\mbox{ and }\neg\,g@ \mbox{xx}_3@ \mbox{xx}_1\mbox{ and }\neg\,g@ \mbox{xx}_3@ \mbox{xx}_2\mbox{ and }\neg\,g@ \mbox{xx}_4@ \mbox{xx}_0\mbox{ and }\neg\,g@ \mbox{xx}_4@ \mbox{xx}_1\mbox{ and }\neg\,g@ \mbox{xx}_4@ \mbox{xx}_2\mbox{ and }\neg\,g@ \mbox{xx}_4@ \mbox{xx}_3 ) ) )\qquad\mbox{thf}(\mbox{ramsey\_u\_3\_5\_16a},\mbox{conjecture})$

\medskip\textbf{GRA009+1.p} Maximal shortest path length in terms of triangles

In a complete graph with a shortest path P from V1 to V2 with
 edges E1 and E2, E1 sequential to E2, there is an edge E3 such
 that E1, E2, and E3 form a triangle.




$\mbox{include}(\mbox{'Axioms/GRA001+0.ax'})$

$\forall e_1,e_2,e_3{:}\;( \mbox{triangle}(e_1,e_2,e_3)\iff ( \mbox{edge}(e_1)\mbox{ and }\mbox{edge}(e_2)\mbox{ and }\mbox{edge}(e_3)\mbox{ and }\mbox{sequential}(e_1,e_2)\mbox{ and }\mbox{sequential}(e_2,e_3)\mbox{ and }\mbox{sequential}(e_3,e_1) ) )\qquad\mbox{fof}(\mbox{triangle\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{length\_of}(p) = \mbox{number\_of\_in}(\mbox{edges},p) )\qquad\mbox{fof}(\mbox{length\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = -\mbox{length\_of}(p) )\qquad\mbox{fof}(\mbox{path\_length\_sequential\_pairs},\mbox{axiom})$

$\forall p,v_1,v_2{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) ) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{sequential\_pairs\_and\_triangles},\mbox{axiom})$

$\forall \mbox{things},\mbox{inThese}{:}\;\mbox{number\_of\_in}(\mbox{things},\mbox{inThese}) \leq \mbox{number\_of\_in}(\mbox{things},\mbox{graph})\qquad\mbox{fof}(\mbox{graph\_has\_them\_all},\mbox{axiom})$

$\mbox{complete} \ \Rightarrow \ \forall v_1,v_2,p,e_1,e_2{:}\;( ( \mbox{shortest\_path}(v_1,v_2,p)\mbox{ and }\mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) )\qquad\mbox{fof}(\mbox{complete\_means\_path\_and\_stuff\_means\_triangles},\mbox{conjecture})$

\medskip\textbf{GRA008+2.p} Maximal shortest path length in terms of triangles

In a complete graph with a shortest path P from V1 to V2 with
 edges E1 and E2, E1 preceding and sequential to E2, there is
 an edge E3 such that E1, E2, and E3 form a triangle.




$\mbox{include}(\mbox{'Axioms/GRA001+0.ax'})$

$\forall e_1,e_2,e_3{:}\;( \mbox{triangle}(e_1,e_2,e_3)\iff ( \mbox{edge}(e_1)\mbox{ and }\mbox{edge}(e_2)\mbox{ and }\mbox{edge}(e_3)\mbox{ and }\mbox{sequential}(e_1,e_2)\mbox{ and }\mbox{sequential}(e_2,e_3)\mbox{ and }\mbox{sequential}(e_3,e_1) ) )\qquad\mbox{fof}(\mbox{triangle\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{length\_of}(p) = \mbox{number\_of\_in}(\mbox{edges},p) )\qquad\mbox{fof}(\mbox{length\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = -\mbox{length\_of}(p) )\qquad\mbox{fof}(\mbox{path\_length\_sequential\_pairs},\mbox{axiom})$

$\forall p,v_1,v_2{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) ) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{sequential\_pairs\_and\_triangles},\mbox{axiom})$

$\forall \mbox{things},\mbox{inThese}{:}\;\mbox{number\_of\_in}(\mbox{things},\mbox{inThese}) \leq \mbox{number\_of\_in}(\mbox{things},\mbox{graph})\qquad\mbox{fof}(\mbox{graph\_has\_them\_all},\mbox{axiom})$

$\mbox{complete} \ \Rightarrow \ \forall v_1,v_2,e_1,e_2,p{:}\;( ( \mbox{shortest\_path}(v_1,v_2,p)\mbox{ and }\mbox{precedes}(e_1,e_2,p) ) \ \Rightarrow \ \exists e_3{:}\;( \mbox{edge}(e_3)\mbox{ and }\mbox{tail\_of}(e_3) = \mbox{head\_of}(e_2)\mbox{ and }\mbox{head\_of}(e_3) = \mbox{tail\_of}(e_1) ) )\qquad\mbox{fof}(\mbox{back\_edge},\mbox{lemma})$

$\mbox{complete} \ \Rightarrow \ \forall v_1,v_2,e_1,e_2,p{:}\;( ( \mbox{shortest\_path}(v_1,v_2,p)\mbox{ and }\mbox{precedes}(e_1,e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) )\qquad\mbox{fof}(\mbox{sequential\_is\_triangle},\mbox{conjecture})$

\medskip\textbf{GRA012+1.p} Maximal shortest path length in terms of triangles

In a complete graph, if there is a shortest path P from V1 to
 V2, then the number of triangles in P is the length of P minus
 one.




$\mbox{include}(\mbox{'Axioms/GRA001+0.ax'})$

$\forall e_1,e_2,e_3{:}\;( \mbox{triangle}(e_1,e_2,e_3)\iff ( \mbox{edge}(e_1)\mbox{ and }\mbox{edge}(e_2)\mbox{ and }\mbox{edge}(e_3)\mbox{ and }\mbox{sequential}(e_1,e_2)\mbox{ and }\mbox{sequential}(e_2,e_3)\mbox{ and }\mbox{sequential}(e_3,e_1) ) )\qquad\mbox{fof}(\mbox{triangle\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{length\_of}(p) = \mbox{number\_of\_in}(\mbox{edges},p) )\qquad\mbox{fof}(\mbox{length\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = -\mbox{length\_of}(p) )\qquad\mbox{fof}(\mbox{path\_length\_sequential\_pairs},\mbox{axiom})$

$\forall p,v_1,v_2{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) ) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{sequential\_pairs\_and\_triangles},\mbox{axiom})$

$\forall \mbox{things},\mbox{inThese}{:}\;\mbox{number\_of\_in}(\mbox{things},\mbox{inThese}) \leq \mbox{number\_of\_in}(\mbox{things},\mbox{graph})\qquad\mbox{fof}(\mbox{graph\_has\_them\_all},\mbox{axiom})$

$\mbox{complete} \ \Rightarrow \ \forall p,v_1,v_2{:}\;( \mbox{shortest\_path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{triangles},p) = -\mbox{length\_of}(p) )\qquad\mbox{fof}(\mbox{triangles\_on\_a\_path},\mbox{conjecture})$

\medskip\textbf{GRA015+1.p} 2-colored completed graph size 11 without subgraph of size 4

Find a 2-colored completed graph of size 11 without a complete
 subgraph of size 4 which all the edges have the same color.




$n_1 < n_2\mbox{ and }n_2 < n_3\mbox{ and }n_3 < n_4\mbox{ and }n_4 < n_5\mbox{ and }n_5 < n_6\mbox{ and }n_6 < n_7\mbox{ and }n_7 < n_8\mbox{ and }n_8 < n_9\mbox{ and }n_9 < n_{10}\mbox{ and }n_{10} < n_{11}\qquad\mbox{fof}(\mbox{ordering},\mbox{axiom})$

$\forall a,b,c,d{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{red}(a,c)\mbox{ and }\mbox{red}(b,c)\mbox{ and }\mbox{red}(a,d)\mbox{ and }\mbox{red}(b,d)\mbox{ and }\mbox{red}(c,d) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{red\_clique},\mbox{axiom})$

$\forall a,b,c,d{:}\;( ( \mbox{green}(a,b)\mbox{ and }\mbox{green}(a,c)\mbox{ and }\mbox{green}(b,c)\mbox{ and }\mbox{green}(a,d)\mbox{ and }\mbox{green}(b,d)\mbox{ and }\mbox{green}(c,d) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{green\_clique},\mbox{axiom})$

$\forall a,b{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{green}(a,b) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{no\_overlap},\mbox{axiom})$

$\forall a,b,c{:}\;( ( a < b\mbox{ and }b < c ) \ \Rightarrow \ a < c )\qquad\mbox{fof}(\mbox{less\_than\_transitive},\mbox{axiom})$

$\forall a,b{:}\;( a < b \ \Rightarrow \ ( \mbox{red}(a,b)\mbox{ or }\mbox{green}(a,b) ) )\qquad\mbox{fof}(\mbox{partition},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip\textbf{GRA007+2.p} Maximal shortest path length in terms of triangles

In a complete graph with a shortest path P from V1 to V2 with
 edges E1 and E2, E1 preceding E2, there's an edge from the
 head of E2 to the tail of E1 (a back edge).




$\mbox{include}(\mbox{'Axioms/GRA001+0.ax'})$

$\forall e_1,e_2,e_3{:}\;( \mbox{triangle}(e_1,e_2,e_3)\iff ( \mbox{edge}(e_1)\mbox{ and }\mbox{edge}(e_2)\mbox{ and }\mbox{edge}(e_3)\mbox{ and }\mbox{sequential}(e_1,e_2)\mbox{ and }\mbox{sequential}(e_2,e_3)\mbox{ and }\mbox{sequential}(e_3,e_1) ) )\qquad\mbox{fof}(\mbox{triangle\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{length\_of}(p) = \mbox{number\_of\_in}(\mbox{edges},p) )\qquad\mbox{fof}(\mbox{length\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = -\mbox{length\_of}(p) )\qquad\mbox{fof}(\mbox{path\_length\_sequential\_pairs},\mbox{axiom})$

$\forall p,v_1,v_2{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) ) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{sequential\_pairs\_and\_triangles},\mbox{axiom})$

$\forall \mbox{things},\mbox{inThese}{:}\;\mbox{number\_of\_in}(\mbox{things},\mbox{inThese}) \leq \mbox{number\_of\_in}(\mbox{things},\mbox{graph})\qquad\mbox{fof}(\mbox{graph\_has\_them\_all},\mbox{axiom})$

$\forall v_1,v_2,e_1,e_2,p{:}\;( ( \mbox{shortest\_path}(v_1,v_2,p)\mbox{ and }\mbox{precedes}(e_1,e_2,p) ) \ \Rightarrow \ \neg\,\exists e_3{:}\;( \mbox{edge}(e_3)\mbox{ and }\mbox{tail\_of}(e_3) = \mbox{tail\_of}(e_1)\mbox{ and }\mbox{head\_of}(e_3) = \mbox{head\_of}(e_2) ) )\qquad\mbox{fof}(\mbox{no\_short\_cut\_edge},\mbox{lemma})$

$\mbox{complete} \ \Rightarrow \ \forall v_1,v_2,e_1,e_2,p{:}\;( ( \mbox{shortest\_path}(v_1,v_2,p)\mbox{ and }\mbox{precedes}(e_1,e_2,p) ) \ \Rightarrow \ \exists e_3{:}\;( \mbox{edge}(e_3)\mbox{ and }\mbox{tail\_of}(e_3) = \mbox{head\_of}(e_2)\mbox{ and }\mbox{head\_of}(e_3) = \mbox{tail\_of}(e_1) ) )\qquad\mbox{fof}(\mbox{back\_edge},\mbox{conjecture})$

\medskip\textbf{GRA032$\wedge$1.p} R(3,6) $>$ 16






$\exists g{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to ( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( \forall \mbox{xx}{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xy}{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o}{:}\;( ( g@ \mbox{xx}@ \mbox{xy} ) \ \Rightarrow \ ( g@ \mbox{xy}@ \mbox{xx} ) )\mbox{ and }\forall \mbox{xx}_0{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xx}_1{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xx}_2{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xp}_0{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_1{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( ( \mbox{xp}_0@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_0\mbox{ and }\mbox{xp}_1@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_2 ) \ \Rightarrow \ ( \neg\,g@ \mbox{xx}_1@ \mbox{xx}_0\mbox{ or }\neg\,g@ \mbox{xx}_2@ \mbox{xx}_0\mbox{ or }\neg\,g@ \mbox{xx}_2@ \mbox{xx}_1 ) )\mbox{ and }\forall \mbox{xx}_0{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xx}_1{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xx}_2{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xx}_3{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xx}_4{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xx}_5{:}\;\mbox{\$o}\to \mbox{\$o}\to \mbox{\$o},\mbox{xp}_0{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_1{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_2{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_3{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_4{:}\;( \mbox{\$o}\to \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( ( \mbox{xp}_0@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_4\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_5\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_0\mbox{ and }\mbox{xp}_1@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_4\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_5\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_1\mbox{ and }\mbox{xp}_2@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_4\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_5\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_2\mbox{ and }\mbox{xp}_3@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_4\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_5\mbox{ and }\neg\,\mbox{xp}_4@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_4@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_4@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_4@ \mbox{xx}_3\mbox{ and }\mbox{xp}_4@ \mbox{xx}_4\mbox{ and }\neg\,\mbox{xp}_4@ \mbox{xx}_5 ) \ \Rightarrow \ ( g@ \mbox{xx}_1@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_2@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_2@ \mbox{xx}_1\mbox{ or }g@ \mbox{xx}_3@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_3@ \mbox{xx}_1\mbox{ or }g@ \mbox{xx}_3@ \mbox{xx}_2\mbox{ or }g@ \mbox{xx}_4@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_4@ \mbox{xx}_1\mbox{ or }g@ \mbox{xx}_4@ \mbox{xx}_2\mbox{ or }g@ \mbox{xx}_4@ \mbox{xx}_3\mbox{ or }g@ \mbox{xx}_5@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_5@ \mbox{xx}_1\mbox{ or }g@ \mbox{xx}_5@ \mbox{xx}_2\mbox{ or }g@ \mbox{xx}_5@ \mbox{xx}_3\mbox{ or }g@ \mbox{xx}_5@ \mbox{xx}_4 ) ) )\qquad\mbox{thf}(\mbox{ramsey\_l\_3\_6}_{16},\mbox{conjecture})$

\medskip\textbf{GRA028$\wedge$1.p} R(2,4) $\leq$ 4






$\forall g{:}\;( \mbox{\$o}\to \mbox{\$o} )\to ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( \forall \mbox{xx}{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xy}{:}\;\mbox{\$o}\to \mbox{\$o}{:}\;( ( g@ \mbox{xx}@ \mbox{xy} ) \ \Rightarrow \ ( g@ \mbox{xy}@ \mbox{xx} ) ) \ \Rightarrow \ ( \exists \mbox{xx}_0{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xx}_1{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xp}_0{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( \mbox{xp}_0@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_1\mbox{ and }g@ \mbox{xx}_1@ \mbox{xx}_0 )\mbox{ or }\exists \mbox{xx}_0{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xx}_1{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xx}_2{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xx}_3{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xp}_0{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_1{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_2{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( \mbox{xp}_0@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_0\mbox{ and }\mbox{xp}_1@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_1\mbox{ and }\mbox{xp}_2@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_3\mbox{ and }\neg\,g@ \mbox{xx}_1@ \mbox{xx}_0\mbox{ and }\neg\,g@ \mbox{xx}_2@ \mbox{xx}_0\mbox{ and }\neg\,g@ \mbox{xx}_2@ \mbox{xx}_1\mbox{ and }\neg\,g@ \mbox{xx}_3@ \mbox{xx}_0\mbox{ and }\neg\,g@ \mbox{xx}_3@ \mbox{xx}_1\mbox{ and }\neg\,g@ \mbox{xx}_3@ \mbox{xx}_2 ) ) )\qquad\mbox{thf}(\mbox{ramsey\_u\_2\_4}_4,\mbox{conjecture})$

\medskip\textbf{GRA030$\wedge$1.p} R(2,5) $>$ 4






$\exists g{:}\;( \mbox{\$o}\to \mbox{\$o} )\to ( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( \forall \mbox{xx}{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xy}{:}\;\mbox{\$o}\to \mbox{\$o}{:}\;( ( g@ \mbox{xx}@ \mbox{xy} ) \ \Rightarrow \ ( g@ \mbox{xy}@ \mbox{xx} ) )\mbox{ and }\forall \mbox{xx}_0{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xx}_1{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xp}_0{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( ( \mbox{xp}_0@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_1 ) \ \Rightarrow \ \neg\,g@ \mbox{xx}_1@ \mbox{xx}_0 )\mbox{ and }\forall \mbox{xx}_0{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xx}_1{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xx}_2{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xx}_3{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xx}_4{:}\;\mbox{\$o}\to \mbox{\$o},\mbox{xp}_0{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_1{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_2{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o},\mbox{xp}_3{:}\;( \mbox{\$o}\to \mbox{\$o} )\to \mbox{\$o}{:}\;( ( \mbox{xp}_0@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_0@ \mbox{xx}_4\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_0\mbox{ and }\mbox{xp}_1@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_1@ \mbox{xx}_4\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_1\mbox{ and }\mbox{xp}_2@ \mbox{xx}_2\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_2@ \mbox{xx}_4\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_0\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_1\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_2\mbox{ and }\mbox{xp}_3@ \mbox{xx}_3\mbox{ and }\neg\,\mbox{xp}_3@ \mbox{xx}_4 ) \ \Rightarrow \ ( g@ \mbox{xx}_1@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_2@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_2@ \mbox{xx}_1\mbox{ or }g@ \mbox{xx}_3@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_3@ \mbox{xx}_1\mbox{ or }g@ \mbox{xx}_3@ \mbox{xx}_2\mbox{ or }g@ \mbox{xx}_4@ \mbox{xx}_0\mbox{ or }g@ \mbox{xx}_4@ \mbox{xx}_1\mbox{ or }g@ \mbox{xx}_4@ \mbox{xx}_2\mbox{ or }g@ \mbox{xx}_4@ \mbox{xx}_3 ) ) )\qquad\mbox{thf}(\mbox{ramsey\_l\_2\_5}_4,\mbox{conjecture})$

\medskip\textbf{GRA020+1.p} 2-colored completed graph size 11 without subgraph of size 5

Find a 2-colored completed graph of size 11 without a complete
 subgraph of size 5 which all the edges have the same color.




$n_1 < n_2\mbox{ and }n_2 < n_3\mbox{ and }n_3 < n_4\mbox{ and }n_4 < n_5\mbox{ and }n_5 < n_6\mbox{ and }n_6 < n_7\mbox{ and }n_7 < n_8\mbox{ and }n_8 < n_9\mbox{ and }n_9 < n_{10}\mbox{ and }n_{10} < n_{11}\qquad\mbox{fof}(\mbox{ordering},\mbox{axiom})$

$\forall a,b,c,d,e{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{red}(a,c)\mbox{ and }\mbox{red}(b,c)\mbox{ and }\mbox{red}(a,d)\mbox{ and }\mbox{red}(b,d)\mbox{ and }\mbox{red}(c,d)\mbox{ and }\mbox{red}(a,e)\mbox{ and }\mbox{red}(b,e)\mbox{ and }\mbox{red}(c,e)\mbox{ and }\mbox{red}(d,e) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{red\_clique},\mbox{axiom})$

$\forall a,b,c,d,e{:}\;( ( \mbox{green}(a,b)\mbox{ and }\mbox{green}(a,c)\mbox{ and }\mbox{green}(b,c)\mbox{ and }\mbox{green}(a,d)\mbox{ and }\mbox{green}(b,d)\mbox{ and }\mbox{green}(c,d)\mbox{ and }\mbox{green}(a,e)\mbox{ and }\mbox{green}(b,e)\mbox{ and }\mbox{green}(c,e)\mbox{ and }\mbox{green}(d,e) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{green\_clique},\mbox{axiom})$

$\forall a,b{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{green}(a,b) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{no\_overlap},\mbox{axiom})$

$\forall a,b,c{:}\;( ( a < b\mbox{ and }b < c ) \ \Rightarrow \ a < c )\qquad\mbox{fof}(\mbox{less\_than\_transitive},\mbox{axiom})$

$\forall a,b{:}\;( a < b \ \Rightarrow \ ( \mbox{red}(a,b)\mbox{ or }\mbox{green}(a,b) ) )\qquad\mbox{fof}(\mbox{partition},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip\textbf{GRA002+4.p} Maximal shortest path length in terms of triangles

In a complete directed graph, the maximal length of a shortest
 path between two vertices is the number of triangles in the
 graph minus 1.




$\mbox{include}(\mbox{'Axioms/GRA001+0.ax'})$

$\forall e_1,e_2,e_3{:}\;( \mbox{triangle}(e_1,e_2,e_3)\iff ( \mbox{edge}(e_1)\mbox{ and }\mbox{edge}(e_2)\mbox{ and }\mbox{edge}(e_3)\mbox{ and }\mbox{sequential}(e_1,e_2)\mbox{ and }\mbox{sequential}(e_2,e_3)\mbox{ and }\mbox{sequential}(e_3,e_1) ) )\qquad\mbox{fof}(\mbox{triangle\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{length\_of}(p) = \mbox{number\_of\_in}(\mbox{edges},p) )\qquad\mbox{fof}(\mbox{length\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = -\mbox{length\_of}(p) )\qquad\mbox{fof}(\mbox{path\_length\_sequential\_pairs},\mbox{axiom})$

$\forall p,v_1,v_2{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) ) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{sequential\_pairs\_and\_triangles},\mbox{axiom})$

$\forall \mbox{things},\mbox{inThese}{:}\;\mbox{number\_of\_in}(\mbox{things},\mbox{inThese}) \leq \mbox{number\_of\_in}(\mbox{things},\mbox{graph})\qquad\mbox{fof}(\mbox{graph\_has\_them\_all},\mbox{axiom})$

$\mbox{complete} \ \Rightarrow \ \forall p,v_1,v_2{:}\;( \mbox{shortest\_path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{triangles\_and\_sequential\_pairs},\mbox{lemma})$

$\mbox{complete} \ \Rightarrow \ \forall p,v_1,v_2{:}\;( \mbox{shortest\_path}(v_1,v_2,p) \ \Rightarrow \ -\mbox{length\_of}(p) \leq \mbox{number\_of\_in}(\mbox{triangles},\mbox{graph}) )\qquad\mbox{fof}(\mbox{maximal\_path\_length},\mbox{conjecture})$

\medskip\textbf{GRA004+1.p} Maximal shortest path length in terms of triangles

In a shortest path P from V1 to V2 with edges E1 and E2, E1
 preceding E2, there is no edge from the tail of E1 to the
 head of E2, and the head of E2 is not the head or tail of E1.




$\mbox{include}(\mbox{'Axioms/GRA001+0.ax'})$

$\forall e_1,e_2,e_3{:}\;( \mbox{triangle}(e_1,e_2,e_3)\iff ( \mbox{edge}(e_1)\mbox{ and }\mbox{edge}(e_2)\mbox{ and }\mbox{edge}(e_3)\mbox{ and }\mbox{sequential}(e_1,e_2)\mbox{ and }\mbox{sequential}(e_2,e_3)\mbox{ and }\mbox{sequential}(e_3,e_1) ) )\qquad\mbox{fof}(\mbox{triangle\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{length\_of}(p) = \mbox{number\_of\_in}(\mbox{edges},p) )\qquad\mbox{fof}(\mbox{length\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = -\mbox{length\_of}(p) )\qquad\mbox{fof}(\mbox{path\_length\_sequential\_pairs},\mbox{axiom})$

$\forall p,v_1,v_2{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) ) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{sequential\_pairs\_and\_triangles},\mbox{axiom})$

$\forall \mbox{things},\mbox{inThese}{:}\;\mbox{number\_of\_in}(\mbox{things},\mbox{inThese}) \leq \mbox{number\_of\_in}(\mbox{things},\mbox{graph})\qquad\mbox{fof}(\mbox{graph\_has\_them\_all},\mbox{axiom})$

$\forall v_1,v_2,e_1,e_2,p{:}\;( ( \mbox{shortest\_path}(v_1,v_2,p)\mbox{ and }\mbox{precedes}(e_1,e_2,p) ) \ \Rightarrow \ ( \neg\,\exists e_3{:}\;( \mbox{tail\_of}(e_3) = \mbox{tail\_of}(e_1)\mbox{ and }\mbox{head\_of}(e_3) = \mbox{head\_of}(e_2) )\mbox{ and }\mbox{head\_of}(e_2)\ne \mbox{tail\_of}(e_1)\mbox{ and }\mbox{head\_of}(e_2)\ne \mbox{head\_of}(e_1) ) )\qquad\mbox{fof}(\mbox{shortest\_path\_properties\_lemma},\mbox{conjecture})$

\medskip\textbf{GRA017+1.p} 2-colored completed graph size 13 without subgraph of size 4

Find a 2-colored completed graph of size 13 without a complete
 subgraph of size 4 which all the edges have the same color.




$n_1 < n_2\mbox{ and }n_2 < n_3\mbox{ and }n_3 < n_4\mbox{ and }n_4 < n_5\mbox{ and }n_5 < n_6\mbox{ and }n_6 < n_7\mbox{ and }n_7 < n_8\mbox{ and }n_8 < n_9\mbox{ and }n_9 < n_{10}\mbox{ and }n_{10} < n_{11}\mbox{ and }n_{11} < n_{12}\mbox{ and }n_{12} < n_{13}\qquad\mbox{fof}(\mbox{ordering},\mbox{axiom})$

$\forall a,b,c,d{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{red}(a,c)\mbox{ and }\mbox{red}(b,c)\mbox{ and }\mbox{red}(a,d)\mbox{ and }\mbox{red}(b,d)\mbox{ and }\mbox{red}(c,d) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{red\_clique},\mbox{axiom})$

$\forall a,b,c,d{:}\;( ( \mbox{green}(a,b)\mbox{ and }\mbox{green}(a,c)\mbox{ and }\mbox{green}(b,c)\mbox{ and }\mbox{green}(a,d)\mbox{ and }\mbox{green}(b,d)\mbox{ and }\mbox{green}(c,d) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{green\_clique},\mbox{axiom})$

$\forall a,b{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{green}(a,b) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{no\_overlap},\mbox{axiom})$

$\forall a,b,c{:}\;( ( a < b\mbox{ and }b < c ) \ \Rightarrow \ a < c )\qquad\mbox{fof}(\mbox{less\_than\_transitive},\mbox{axiom})$

$\forall a,b{:}\;( a < b \ \Rightarrow \ ( \mbox{red}(a,b)\mbox{ or }\mbox{green}(a,b) ) )\qquad\mbox{fof}(\mbox{partition},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip\textbf{GRA013+1.p} 2-colored completed graph size 5 without subgraph of size 3

Find a 2-colored completed graph of size 5 without a complete
 subgraph of size 3 which all the edges have the same color.




$\forall a,b,c{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{red}(b,c)\mbox{ and }\mbox{red}(a,c) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{red\_clique},\mbox{axiom})$

$\forall a,b,c{:}\;( ( \mbox{green}(a,b)\mbox{ and }\mbox{green}(b,c)\mbox{ and }\mbox{green}(a,c) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{green\_clique},\mbox{axiom})$

$n_1 < n_2\mbox{ and }n_2 < n_3\mbox{ and }n_3 < n_4\mbox{ and }n_4 < n_5\qquad\mbox{fof}(\mbox{ordering},\mbox{axiom})$

$\forall a,b,c{:}\;( ( a < b\mbox{ and }b < c ) \ \Rightarrow \ a < c )\qquad\mbox{fof}(\mbox{less\_than\_transitive},\mbox{axiom})$

$\forall a,b{:}\;( a < b \ \Rightarrow \ ( \mbox{red}(a,b)\mbox{ or }\mbox{green}(a,b) ) )\qquad\mbox{fof}(\mbox{partition},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip\textbf{GRA010+1.p} Maximal shortest path length in terms of triangles

In a complete graph, if there is a shortest path P from V1 to
 V2 with edges E1 and E2, E1 sequential to E2 means there is an
 edge E3 such that E1, E2, and E3 form a triangle, then the
 number of sequential pairs in P is the number of triangles
 in P.




$\mbox{include}(\mbox{'Axioms/GRA001+0.ax'})$

$\forall e_1,e_2,e_3{:}\;( \mbox{triangle}(e_1,e_2,e_3)\iff ( \mbox{edge}(e_1)\mbox{ and }\mbox{edge}(e_2)\mbox{ and }\mbox{edge}(e_3)\mbox{ and }\mbox{sequential}(e_1,e_2)\mbox{ and }\mbox{sequential}(e_2,e_3)\mbox{ and }\mbox{sequential}(e_3,e_1) ) )\qquad\mbox{fof}(\mbox{triangle\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{length\_of}(p) = \mbox{number\_of\_in}(\mbox{edges},p) )\qquad\mbox{fof}(\mbox{length\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = -\mbox{length\_of}(p) )\qquad\mbox{fof}(\mbox{path\_length\_sequential\_pairs},\mbox{axiom})$

$\forall p,v_1,v_2{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) ) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{sequential\_pairs\_and\_triangles},\mbox{axiom})$

$\forall \mbox{things},\mbox{inThese}{:}\;\mbox{number\_of\_in}(\mbox{things},\mbox{inThese}) \leq \mbox{number\_of\_in}(\mbox{things},\mbox{graph})\qquad\mbox{fof}(\mbox{graph\_has\_them\_all},\mbox{axiom})$

$\mbox{complete} \ \Rightarrow \ \forall p,v_1,v_2{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) ) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{complete\_means\_sequential\_pairs\_and\_triangles},\mbox{conjecture})$

\medskip\textbf{GRA011+1.p} Maximal shortest path length in terms of triangles

In a complete graph, if there is a shortest path P from V1 to
 V2, then the number of sequential pairs in P is the number of
 triangles in P.




$\mbox{include}(\mbox{'Axioms/GRA001+0.ax'})$

$\forall e_1,e_2,e_3{:}\;( \mbox{triangle}(e_1,e_2,e_3)\iff ( \mbox{edge}(e_1)\mbox{ and }\mbox{edge}(e_2)\mbox{ and }\mbox{edge}(e_3)\mbox{ and }\mbox{sequential}(e_1,e_2)\mbox{ and }\mbox{sequential}(e_2,e_3)\mbox{ and }\mbox{sequential}(e_3,e_1) ) )\qquad\mbox{fof}(\mbox{triangle\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{length\_of}(p) = \mbox{number\_of\_in}(\mbox{edges},p) )\qquad\mbox{fof}(\mbox{length\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = -\mbox{length\_of}(p) )\qquad\mbox{fof}(\mbox{path\_length\_sequential\_pairs},\mbox{axiom})$

$\forall p,v_1,v_2{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) ) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{sequential\_pairs\_and\_triangles},\mbox{axiom})$

$\forall \mbox{things},\mbox{inThese}{:}\;\mbox{number\_of\_in}(\mbox{things},\mbox{inThese}) \leq \mbox{number\_of\_in}(\mbox{things},\mbox{graph})\qquad\mbox{fof}(\mbox{graph\_has\_them\_all},\mbox{axiom})$

$\mbox{complete} \ \Rightarrow \ \forall p,v_1,v_2{:}\;( \mbox{shortest\_path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{triangles\_and\_sequential\_pairs},\mbox{conjecture})$

\medskip\textbf{GRA019+1.p} 2-colored completed graph size 18 without subgraph of size 4

Find a 2-colored completed graph of size 18 without a complete
 subgraph of size 4 which all the edges have the same color.




$n_1 < n_2\mbox{ and }n_2 < n_3\mbox{ and }n_3 < n_4\mbox{ and }n_4 < n_5\mbox{ and }n_5 < n_6\mbox{ and }n_6 < n_7\mbox{ and }n_7 < n_8\mbox{ and }n_8 < n_9\mbox{ and }n_9 < n_{10}\mbox{ and }n_{10} < n_{11}\mbox{ and }n_{11} < n_{12}\mbox{ and }n_{12} < n_{13}\mbox{ and }n_{13} < n_{14}\mbox{ and }n_{14} < n_{15}\mbox{ and }n_{15} < n_{16}\mbox{ and }n_{16} < n_{17}\mbox{ and }n_{17} < n_{18}\qquad\mbox{fof}(\mbox{ordering},\mbox{axiom})$

$\forall a,b,c,d{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{red}(a,c)\mbox{ and }\mbox{red}(b,c)\mbox{ and }\mbox{red}(a,d)\mbox{ and }\mbox{red}(b,d)\mbox{ and }\mbox{red}(c,d) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{red\_clique},\mbox{axiom})$

$\forall a,b,c,d{:}\;( ( \mbox{green}(a,b)\mbox{ and }\mbox{green}(a,c)\mbox{ and }\mbox{green}(b,c)\mbox{ and }\mbox{green}(a,d)\mbox{ and }\mbox{green}(b,d)\mbox{ and }\mbox{green}(c,d) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{green\_clique},\mbox{axiom})$

$\forall a,b,c{:}\;( ( a < b\mbox{ and }b < c ) \ \Rightarrow \ a < c )\qquad\mbox{fof}(\mbox{less\_than\_transitive},\mbox{axiom})$

$\forall a,b{:}\;( a < b \ \Rightarrow \ ( \mbox{red}(a,b)\mbox{ or }\mbox{green}(a,b) ) )\qquad\mbox{fof}(\mbox{partition},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip\textbf{GRA006+1.p} Maximal shortest path length in terms of triangles

In a complete graph with a shortest path P from V1 to V2 with
 edges E1 and E2, either there's an edge from the tail of E1 to
 the head of E2, or there's an edge from the head of E2 to the
 tail of E1.




$\mbox{include}(\mbox{'Axioms/GRA001+0.ax'})$

$\forall e_1,e_2,e_3{:}\;( \mbox{triangle}(e_1,e_2,e_3)\iff ( \mbox{edge}(e_1)\mbox{ and }\mbox{edge}(e_2)\mbox{ and }\mbox{edge}(e_3)\mbox{ and }\mbox{sequential}(e_1,e_2)\mbox{ and }\mbox{sequential}(e_2,e_3)\mbox{ and }\mbox{sequential}(e_3,e_1) ) )\qquad\mbox{fof}(\mbox{triangle\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{length\_of}(p) = \mbox{number\_of\_in}(\mbox{edges},p) )\qquad\mbox{fof}(\mbox{length\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = -\mbox{length\_of}(p) )\qquad\mbox{fof}(\mbox{path\_length\_sequential\_pairs},\mbox{axiom})$

$\forall p,v_1,v_2{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) ) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{sequential\_pairs\_and\_triangles},\mbox{axiom})$

$\forall \mbox{things},\mbox{inThese}{:}\;\mbox{number\_of\_in}(\mbox{things},\mbox{inThese}) \leq \mbox{number\_of\_in}(\mbox{things},\mbox{graph})\qquad\mbox{fof}(\mbox{graph\_has\_them\_all},\mbox{axiom})$

$\mbox{complete} \ \Rightarrow \ \forall v_1,v_2,e_1,e_2,p{:}\;( ( \mbox{shortest\_path}(v_1,v_2,p)\mbox{ and }\mbox{precedes}(e_1,e_2,p) ) \ \Rightarrow \ \exists e_3{:}\;( \mbox{edge}(e_3)\mbox{ and }\mbox{tail\_of}(e_3) = \mbox{tail\_of}(e_1)\mbox{ and }\mbox{head\_of}(e_3) = \mbox{head\_of}(e_2) ) <~> \exists e_3{:}\;( \mbox{edge}(e_3)\mbox{ and }\mbox{tail\_of}(e_3) = \mbox{head\_of}(e_2)\mbox{ and }\mbox{head\_of}(e_3) = \mbox{tail\_of}(e_1) ) )\qquad\mbox{fof}(\mbox{edge\_some\_way},\mbox{conjecture})$

\medskip\textbf{GRA009+2.p} Maximal shortest path length in terms of triangles

In a complete graph with a shortest path P from V1 to V2 with
 edges E1 and E2, E1 sequential to E2, there is an edge E3 such
 that E1, E2, and E3 form a triangle.




$\mbox{include}(\mbox{'Axioms/GRA001+0.ax'})$

$\forall e_1,e_2,e_3{:}\;( \mbox{triangle}(e_1,e_2,e_3)\iff ( \mbox{edge}(e_1)\mbox{ and }\mbox{edge}(e_2)\mbox{ and }\mbox{edge}(e_3)\mbox{ and }\mbox{sequential}(e_1,e_2)\mbox{ and }\mbox{sequential}(e_2,e_3)\mbox{ and }\mbox{sequential}(e_3,e_1) ) )\qquad\mbox{fof}(\mbox{triangle\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{length\_of}(p) = \mbox{number\_of\_in}(\mbox{edges},p) )\qquad\mbox{fof}(\mbox{length\_defn},\mbox{axiom})$

$\forall v_1,v_2,p{:}\;( \mbox{path}(v_1,v_2,p) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = -\mbox{length\_of}(p) )\qquad\mbox{fof}(\mbox{path\_length\_sequential\_pairs},\mbox{axiom})$

$\forall p,v_1,v_2{:}\;( ( \mbox{path}(v_1,v_2,p)\mbox{ and }\forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) ) \ \Rightarrow \ \mbox{number\_of\_in}(\mbox{sequential\_pairs},p) = \mbox{number\_of\_in}(\mbox{triangles},p) )\qquad\mbox{fof}(\mbox{sequential\_pairs\_and\_triangles},\mbox{axiom})$

$\forall \mbox{things},\mbox{inThese}{:}\;\mbox{number\_of\_in}(\mbox{things},\mbox{inThese}) \leq \mbox{number\_of\_in}(\mbox{things},\mbox{graph})\qquad\mbox{fof}(\mbox{graph\_has\_them\_all},\mbox{axiom})$

$\mbox{complete} \ \Rightarrow \ \forall p,v_1,v_2{:}\;( \mbox{shortest\_path}(v_1,v_2,p) \ \Rightarrow \ \forall e_1,e_2{:}\;( ( \mbox{on\_path}(e_1,p)\mbox{ and }\mbox{on\_path}(e_2,p)\mbox{ and }\mbox{sequential}(e_1,e_2) ) \ \Rightarrow \ \exists e_3{:}\;\mbox{triangle}(e_1,e_2,e_3) ) )\qquad\mbox{fof}(\mbox{complete\_means\_path\_means\_stuff\_means\_triangles},\mbox{conjecture})$

\medskip\textbf{GRA023+1.p} 2-colored completed graph size 16 without subgraph of size 5

Find a 2-colored completed graph of size 16 without a complete
 subgraph of size 5 which all the edges have the same color.




$n_1 < n_2\mbox{ and }n_2 < n_3\mbox{ and }n_3 < n_4\mbox{ and }n_4 < n_5\mbox{ and }n_5 < n_6\mbox{ and }n_6 < n_7\mbox{ and }n_7 < n_8\mbox{ and }n_8 < n_9\mbox{ and }n_9 < n_{10}\mbox{ and }n_{10} < n_{11}\mbox{ and }n_{11} < n_{12}\mbox{ and }n_{12} < n_{13}\mbox{ and }n_{13} < n_{14}\mbox{ and }n_{14} < n_{15}\mbox{ and }n_{15} < n_{16}\qquad\mbox{fof}(\mbox{ordering},\mbox{axiom})$

$\forall a,b,c,d,e{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{red}(a,c)\mbox{ and }\mbox{red}(b,c)\mbox{ and }\mbox{red}(a,d)\mbox{ and }\mbox{red}(b,d)\mbox{ and }\mbox{red}(c,d)\mbox{ and }\mbox{red}(a,e)\mbox{ and }\mbox{red}(b,e)\mbox{ and }\mbox{red}(c,e)\mbox{ and }\mbox{red}(d,e) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{red\_clique},\mbox{axiom})$

$\forall a,b,c,d,e{:}\;( ( \mbox{green}(a,b)\mbox{ and }\mbox{green}(a,c)\mbox{ and }\mbox{green}(b,c)\mbox{ and }\mbox{green}(a,d)\mbox{ and }\mbox{green}(b,d)\mbox{ and }\mbox{green}(c,d)\mbox{ and }\mbox{green}(a,e)\mbox{ and }\mbox{green}(b,e)\mbox{ and }\mbox{green}(c,e)\mbox{ and }\mbox{green}(d,e) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{green\_clique},\mbox{axiom})$

$\forall a,b{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{green}(a,b) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{no\_overlap},\mbox{axiom})$

$\forall a,b,c{:}\;( ( a < b\mbox{ and }b < c ) \ \Rightarrow \ a < c )\qquad\mbox{fof}(\mbox{less\_than\_transitive},\mbox{axiom})$

$\forall a,b{:}\;( a < b \ \Rightarrow \ ( \mbox{red}(a,b)\mbox{ or }\mbox{green}(a,b) ) )\qquad\mbox{fof}(\mbox{partition},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip\textbf{GRA018+1.p} 2-colored completed graph size 17 without subgraph of size 4

Find a 2-colored completed graph of size 17 without a complete
 subgraph of size 4 which all the edges have the same color.




$n_1 < n_2\mbox{ and }n_2 < n_3\mbox{ and }n_3 < n_4\mbox{ and }n_4 < n_5\mbox{ and }n_5 < n_6\mbox{ and }n_6 < n_7\mbox{ and }n_7 < n_8\mbox{ and }n_8 < n_9\mbox{ and }n_9 < n_{10}\mbox{ and }n_{10} < n_{11}\mbox{ and }n_{11} < n_{12}\mbox{ and }n_{12} < n_{13}\mbox{ and }n_{13} < n_{14}\mbox{ and }n_{14} < n_{15}\mbox{ and }n_{15} < n_{16}\mbox{ and }n_{16} < n_{17}\qquad\mbox{fof}(\mbox{ordering},\mbox{axiom})$

$\forall a,b,c,d{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{red}(a,c)\mbox{ and }\mbox{red}(b,c)\mbox{ and }\mbox{red}(a,d)\mbox{ and }\mbox{red}(b,d)\mbox{ and }\mbox{red}(c,d) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{red\_clique},\mbox{axiom})$

$\forall a,b,c,d{:}\;( ( \mbox{green}(a,b)\mbox{ and }\mbox{green}(a,c)\mbox{ and }\mbox{green}(b,c)\mbox{ and }\mbox{green}(a,d)\mbox{ and }\mbox{green}(b,d)\mbox{ and }\mbox{green}(c,d) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{green\_clique},\mbox{axiom})$

$\forall a,b{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{green}(a,b) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{no\_overlap},\mbox{axiom})$

$\forall a,b,c{:}\;( ( a < b\mbox{ and }b < c ) \ \Rightarrow \ a < c )\qquad\mbox{fof}(\mbox{less\_than\_transitive},\mbox{axiom})$

$\forall a,b{:}\;( a < b \ \Rightarrow \ ( \mbox{red}(a,b)\mbox{ or }\mbox{green}(a,b) ) )\qquad\mbox{fof}(\mbox{partition},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip\textbf{GRA022+1.p} 2-colored completed graph size 13 without subgraph of size 5

Find a 2-colored completed graph of size 13 without a complete
 subgraph of size 5 which all the edges have the same color.




$n_1 < n_2\mbox{ and }n_2 < n_3\mbox{ and }n_3 < n_4\mbox{ and }n_4 < n_5\mbox{ and }n_5 < n_6\mbox{ and }n_6 < n_7\mbox{ and }n_7 < n_8\mbox{ and }n_8 < n_9\mbox{ and }n_9 < n_{10}\mbox{ and }n_{10} < n_{11}\mbox{ and }n_{11} < n_{12}\mbox{ and }n_{12} < n_{13}\qquad\mbox{fof}(\mbox{ordering},\mbox{axiom})$

$\forall a,b,c,d,e{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{red}(a,c)\mbox{ and }\mbox{red}(b,c)\mbox{ and }\mbox{red}(a,d)\mbox{ and }\mbox{red}(b,d)\mbox{ and }\mbox{red}(c,d)\mbox{ and }\mbox{red}(a,e)\mbox{ and }\mbox{red}(b,e)\mbox{ and }\mbox{red}(c,e)\mbox{ and }\mbox{red}(d,e) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{red\_clique},\mbox{axiom})$

$\forall a,b,c,d,e{:}\;( ( \mbox{green}(a,b)\mbox{ and }\mbox{green}(a,c)\mbox{ and }\mbox{green}(b,c)\mbox{ and }\mbox{green}(a,d)\mbox{ and }\mbox{green}(b,d)\mbox{ and }\mbox{green}(c,d)\mbox{ and }\mbox{green}(a,e)\mbox{ and }\mbox{green}(b,e)\mbox{ and }\mbox{green}(c,e)\mbox{ and }\mbox{green}(d,e) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{green\_clique},\mbox{axiom})$

$\forall a,b{:}\;( ( \mbox{red}(a,b)\mbox{ and }\mbox{green}(a,b) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{no\_overlap},\mbox{axiom})$

$\forall a,b,c{:}\;( ( a < b\mbox{ and }b < c ) \ \Rightarrow \ a < c )\qquad\mbox{fof}(\mbox{less\_than\_transitive},\mbox{axiom})$

$\forall a,b{:}\;( a < b \ \Rightarrow \ ( \mbox{red}(a,b)\mbox{ or }\mbox{green}(a,b) ) )\qquad\mbox{fof}(\mbox{partition},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip
\end{document}