#File name: Example.txt

#Everything after a # symbol is a comment and is ignored by DensityChecker. The file format
#is fairly tolerant of whitespace characters (i.e. spaces, tabs, and newline characters) to
#help make the file more readable for humans. 

#This file can be found in the DensityChecker folder of the CD-ROM. It describes the data
#given by Razborov in the paper "On 3-hypergraphs with forbidden 4-vertex configurations"
#which proves that the Turan density is 5/9 when we forbid induced four vertex subgraphs to
#have one or four edges. To use DensityChecker to verify the data does prove an upper bound
#of 5/9, type "DensityChecker Example.txt" at the command-line.

#The data file should begin by specifying what program it has been written for.
Program : DensityChecker

#Next we declare the order of the graphs in our family $\mathcal{H}$. This is denoted by $l$
#in the thesis. The current implementation of DensityChecker can only handle 3-graphs with at
#most nine vertices.  
Order of subgraphs H : 6

#Description of the forbidden family $\mathcal{F}$. Note that a 3-graph is represented by
#a number (indicating its order, n say) folowed by a colon then its edge set (assuming its
#vertices are labelled 1,2,...,n).
Number of forbidden graphs : 2
Forbidden graphs           :
4 : {123, 124, 134, 234}
4 : {123}

#In the traditional definition of Turan density we forbid the forbidden graphs from appearing
#as subgraphs, and so assign "no" to the following setting. However, in this particular
#problem we wish to forbid the graphs from appearing as *induced* subgraphs so we instead
#set it to "yes".
Forbid only induced subgraphs : yes

Number of terms : 4 #The bound involves four postive semidefinite matrices.

#Each term consists of a positive semidefinite matrix, and the basis it is written in. Each
#member of the basis is a linear combination of flags, hence we also need to define the
#flags and their type.  


--- Term 1 --- #The start of the term is indicated by a simple header line.

#This term is equivalent to (9/5)[(e-4/9)^2]_1 in Razborov's notation.

#We need only define the order of the type. The edge set of the type can be determined from
#the flags. See term 2 for an example.
Order of type : 1

#The common order of the flags, denoted by $m$ in the thesis.
#Note that "order of flags"<=("order of type" + "order of subgraphs H")/2 must hold.
Order of flags : 3

#The number of flags in the flag list below.
Number of flags : 2

#The dimension of the matrix.
Matrix dimension : 1

#The edge sets of the flags used in describing the basis.
#The order of the flags has already been defined. The labelled vertices of the flag (which
#describe the type) are the vertices 1,...,"order of type". In this case there is only one
#labelled vertex: the vertex 1. 
Flags :
F1 : {}
F2 : {123}

#The basis the matrix is written in.
#Each element of the basis is a linear combination of flags in the form:
#<a rational coefficient>(<label of the flag in the flag list above>) + ...
Basis:
B1 : 5/9(F1) - 4/9(F2)

#The entries of the matrix.
#The program expects to read in a list of rational numbers separated by whitespaces, which
#represent the entries (1,1), (1,2), ..., (1,"matrix dimension"), (2,1), (2,2), ... etc.
Matrix :
9/5


--- Term 2 ---

Order of type    : 4
Order of flags   : 5
Number of flags  : 17
Matrix dimension : 4

#The order of the type is four. Hence the labelled vertices are 1,2,3,4. By looking at the
#flag "F1" we can determine the edge set of the type is {124, 134, 234}, this is denoted by
#$\tau_1$ in Razborov's paper.

Flags :
F1  : {124, 134, 234, 135, 235, 145, 245}
F2  : {124, 134, 234, 125, 235, 145, 345}
F3  : {124, 134, 234, 125, 135, 245, 345}
F4  : {124, 134, 234, 125, 135, 235, 245}
F5  : {124, 134, 234, 125, 135, 235, 345}
F6  : {124, 134, 234, 125, 135, 235, 145}
F7  : {124, 134, 234, 125, 135, 235}
F8  : {124, 134, 234, 145, 245, 345}
F9  : {124, 134, 234, 135, 235, 245}
F10 : {124, 134, 234, 125, 235, 345}
F11 : {124, 134, 234, 135, 235, 145}
F12 : {124, 134, 234, 125, 235, 145}
F13 : {124, 134, 234, 125, 135, 345}
F14 : {124, 134, 234, 125, 135, 245}
F15 : {124, 134, 234, 245, 345}
F16 : {124, 134, 234, 145, 345}
F17 : {124, 134, 234, 145, 245}

Basis :
B1 : (F1)+(F2)+(F3)-(F4)-(F5)-(F6)
B2 : (F1)+(F2)+(F3)+2(F7)-(F8)
B3 : (F9)+(F10)+(F11)+(F12)+(F13)+(F14)
B4 : (F15)+(F16)+(F17)

#The matrix M_1 in Razborov's paper (multiplied by 9/5).
Matrix :
 96/40 -12/40 -66/40  75/40
-12/40  48/40   3/40 -39/40
-66/40   3/40  51/40 -51/40
 75/40 -39/40 -51/40  81/40

#We have used whitespaces to arrange the entries as they would appear in a matrix. This is to
#make it easier to read for humans. DensityChecker treats this the same as:
#Matrix: 96/40 -12/40 -66/40 75/40 -12/40 48/40 3/40 -39/40 -66/40 3/40 51/40 -51/40 75/40
#-39/40 -51/40 81/40


--- Term 3 ---
#The type is {134, 234} denoted by $\tau_2$ in Razborov's paper.

Order of type    : 4
Order of flags   : 5
Number of flags  : 15
Matrix dimension : 5

Flags :
F1  : {134, 234, 125, 135, 235, 145, 245}
F2  : {134, 234, 135, 235, 145, 245}
F3  : {134, 234, 345}
F4  : {134, 234, 125, 135, 235, 245}
F5  : {134, 234, 125, 235, 145, 245}
F6  : {134, 234, 125, 135, 235, 145}
F7  : {134, 234, 125, 135, 145, 245}
F8  : {134, 234, 125, 235, 145, 345}
F9  : {134, 234, 125, 135, 245, 345}
F10 : {134, 234, 125, 235, 145}
F11 : {134, 234, 125, 135, 245}
F12 : {134, 234, 145, 245, 345}
F13 : {134, 234, 135, 235, 345}
F14 : {134, 234, 145, 245}
F15 : {134, 234, 135, 235}

Basis :
B1 : (F1)-(F2)
B2 : (F1)-(F3)
B3 : (F4)+(F5)+(F6)+(F7)
B4 : (F8)+(F9)
B5 : (F12)+(F13)

#The matrix M_2 in Razborov's paper (multiplied by 9/5).
Matrix :
 192/40  -60/40   18/40 -126/40 132/40
 -60/40  120/40   75/40 -123/40 -57/40
  18/40   75/40   84/40 -165/40  -3/40
-126/40 -123/40 -165/40  393/40 -54/40
 132/40  -57/40   -3/40  -54/40  99/40


--- Term 4 ---
#The type is {134, 234} denoted by $\tau_2$ in Razborov's paper.

Order of type    : 4
Order of flags   : 5
Number of flags  : 15
Matrix dimension : 1

Flags :
F1  : {134, 234, 125, 135, 235, 145, 245}
F2  : {134, 234, 135, 235, 145, 245}
F3  : {134, 234, 345}
F4  : {134, 234, 125, 135, 235, 245}
F5  : {134, 234, 125, 235, 145, 245}
F6  : {134, 234, 125, 135, 235, 145}
F7  : {134, 234, 125, 135, 145, 245}
F8  : {134, 234, 125, 235, 145, 345}
F9  : {134, 234, 125, 135, 245, 345}
F10 : {134, 234, 125, 235, 145}
F11 : {134, 234, 125, 135, 245}
F12 : {134, 234, 145, 245, 345}
F13 : {134, 234, 135, 235, 345}
F14 : {134, 234, 145, 245}
F15 : {134, 234, 135, 235}

#The element g_0 in Razborov's paper.
Basis :
B1 : -(F4)+(F5)+(F6)-(F7)+2(F8)-2(F9)+2(F10)-2(F11)

Matrix :
9/10 #9/5 times 1/2. 