A Non-Theorem with Nice Axioms

Find a complete 2-colour graph of size 11 without a complete subgraph of size 4 in which all the edges have the same color. (A variant of GRA015+1.)

%------------------------------------------------------------------------------
%----A complete graph with 11 nodes
fof(ordering,axiom,
    ( edge(n1,n2)
    & edge(n2,n3)
    & edge(n3,n4)
    & edge(n4,n5)
    & edge(n5,n6)
    & edge(n6,n7)
    & edge(n7,n8)
    & edge(n8,n9)
    & edge(n9,n10)
    & edge(n10,n11) )).

fof(edge_transitive,axiom,(
    ! [A,B,C] :
      ( ( edge(A,B)
        & edge(B,C) )
     => edge(A,C) ) )).

%----All edges are red xor green
fof(partition,axiom,(
    ! [A,B] :
      ( edge(A,B)
     => ( red(A,B)
      <~> green(A,B) ) ) )).

%----The nodes are distinct
fof(distinct_nodes,axiom,
    ! [A,B] :
      ( edge(A,B)
     => A != B ) ).

%----A red clique of size 4
fof(red_clique,axiom,(
    ! [A,B,C,D] :
      ( ( red(A,B)
        & red(A,C)
        & red(B,C)
        & red(A,D)
        & red(B,D)
        & red(C,D) )
     => goal ) )).

%----A green clique of size 4
fof(green_clique,axiom,(
    ! [A,B,C,D] :
      ( ( green(A,B)
        & green(A,C)
        & green(B,C)
        & green(A,D)
        & green(B,D)
        & green(C,D) )
     => goal ) )).

%----Prove there is a red clique or a green clique
fof(goal_to_be_proved,conjecture,(
    goal )).
%------------------------------------------------------------------------------