%------------------------------------------------------------------------------
% File     : GRA166-1 : TPTP v9.3.0. Released v9.3.0.
% Domain   : Graph Theory
% Problem  : Ramsey-like (directed) graph theory problem o3_h
% Version  : Especial.
% English  : Acyclic directed Ramsey graph with two colours, infinite domain.
%            a: 4 vertices, edges 0-1,1-2,0-3,1-3
%            b: 4 vertices, edges 0-1,0-2,1-2,2-3
%            c: 4 vertices, edges 0-1,0-2,1-2,0-3,2-3
%            d: 4 vertices, edges 0-1,0-2,1-2,1-3,2-3
%            f: 5 vertices, edges 0-1,0-2,1-2,0-3,2-3,0-4,1-4,2-4
%            g: 5 vertices, edges 0-1,0-2,1-2,1-3,2-3,0-4,1-4,2-4
%            h: 5 vertices, edges 0-1,1-2,0-3,1-3,2-4,3-4
%            i: 5 vertices, edges 0-1,1-2,0-3,1-3,0-4,2-4,3-4
%            j: 5 vertices, edges 0-1,1-2,0-3,1-3,1-4,2-4,3-4
%            k: 5 vertices, edges 0-1,1-2,0-3,1-3,0-4,1-4,2-4,3-4
%            l: 5 vertices, edges 0-1,0-2,1-2,2-3,3-4}
%            m: 5 vertices, edges 0-1,0-2,1-2,2-3,0-4,3-4
%            n: 5 vertices, edges 0-1,0-2,1-2,2-3,1-4,3-4
%            p: 5 vertices, edges 0-1,0-2,1-2,2-3,0-4,1-4,3-4
%            q: 5 vertices, edges 0-1,0-2,1-2,2-3,2-4,3-4
%            o3 : 3 vertices, edges 0-1,0-2,1-2

% Refs     : [HH74]  Harary & Hell (1974), Generalized Ramsey Theory for Gr
%          : [BJ21]  Brown & Janota (2021), First-Order Instantiation using
%          : [Raw25] Rawson (2025), Email to Geoff Sutcliffe
% Source   : [Raw25]
% Names    : adr_o3_h_rb_inf_cnf.p [Raw25]

% Status   : Unsatisfiable
% Rating   : 0.42 v9.3.0
% Syntax   : Number of clauses     :    7 (   3 unt;   1 nHn;   6 RR)
%            Number of literals    :   17 (   4 equ;  13 neg)
%            Maximal clause size   :    6 (   2 avg)
%            Maximal term depth    :    2 (   1 avg)
%            Number of predicates  :    3 (   2 usr;   0 prp; 2-2 aty)
%            Number of functors    :    2 (   2 usr;   1 con; 0-1 aty)
%            Number of variables   :   15 (   1 sgn)
% SPC      : CNF_UNS_RFO_SEQ_NHN

% Comments :
%------------------------------------------------------------------------------
cnf(snz,axiom,
    s(X) != z ).

cnf(sinj,axiom,
    ( s(X) != s(Y)
    | X = Y ) ).

cnf(ri,axiom,
    ~ r(X,X) ).

cnf(bi,axiom,
    ~ b(X,X) ).

cnf(rb,axiom,
    ( X = Y
    | r(X,Y)
    | b(X,Y) ) ).

cnf(axr,axiom,
    ( ~ r(X0,X1)
    | ~ r(X0,X2)
    | ~ r(X1,X2) ) ).

cnf(axb,axiom,
    ( ~ b(X0,X1)
    | ~ b(X1,X2)
    | ~ b(X0,X3)
    | ~ b(X1,X3)
    | ~ b(X2,X4)
    | ~ b(X3,X4) ) ).

%------------------------------------------------------------------------------