// **************************************************************************
//
//    eses                   eses
//   eses                     eses
//  eses    eseses  esesese    eses   Embedded Systems Group
//  ese    ese  ese ese         ese
//  ese    eseseses eseseses    ese   Department of Computer Science
//  eses   eses          ese   eses
//   eses   eseses  eseseses  eses    University of Kaiserslautern
//    eses                   eses
//
// **************************************************************************
//
//  Ramsey's problem is to colour the edges of a complete graph with
//  V vertices with C colours such that no monocromatic triangle
//  occurs. The boolean array has thereby the following meaning:
//  e[v1][v2][c] is true iff the edge from vertex v1 to vertex v2
//  has color c.
//  The following is known for the formula Ramsey_V_C:
//      - for C=1, Ramsey_V_1 is a tautology for V>=3
//      - for C=2, Ramsey_V_2 is a tautology for V>=6
//      - for C=3, Ramsey_V_3 is a tautology for V>=17
//
// **************************************************************************

macro V = 5;
macro C = 3;

module Ramsey([V][V][C()]bool e) {
    nothing;
} satisfies {
    ramsey_V_C [DisProveA]: assert
        not(
            // -- each row contains a queen -------------
        (forall (i=0 .. V-2) forall(j=i+1..V-1) exists(k=0..C()-1)
                e[i][j][k] )
        &
            // -- no monochromatic triangle --------------------
        (forall (i=0..V-3) forall(j=i+1..V-2) forall(l=j+1..V()-1) forall(k=0..C-1)
                !(e[i][j][k] & e[j][l][k] & e[i][l][k]) )
    );
}