%------------------------------------------------------------------------------
% File     : SWX231-1 : TPTP v9.3.0. Released v9.3.0.
% Domain   : Software Verification
% Problem  : Find a 3-coloring for a graph
% Version  : Especial.
% English  :

% Refs     : [CST26] Claessen et al. (2026), Email to Geoff Sutcliffe
% Source   : [CST26]
% Names    : Graph_prop_p31.p [CST26]

% Status   : Unsatisfiable
% Rating   : 1.00 v9.3.0
% Syntax   : Number of clauses     :   61 (  61 unt;   0 nHn;  23 RR)
%            Number of literals    :   61 (  61 equ;   1 neg)
%            Maximal clause size   :    1 (   1 avg)
%            Maximal term depth    :   11 (   2 avg)
%            Number of predicates  :    1 (   0 usr;   0 prp; 2-2 aty)
%            Number of functors    :   49 (  49 usr;  19 con; 0-5 aty)
%            Number of variables   :   77 (  20 sgn)
% SPC      : CNF_UNS_RFO_PEQ_UEQ

% Comments :
%------------------------------------------------------------------------------
cnf(axiom,axiom,
    aux(X,Y,btrue) = nil3 ).

cnf(axiom_001,axiom,
    aux(X,Y,bfalse) = cons3(X,enumFromToNat(suc(X),Y)) ).

cnf(axiom_002,axiom,
    aux2(A,Z,V,C1,nothing) = cons4(bfalse,colouring(A,Z)) ).

cnf(axiom_003,axiom,
    aux2(A,Z,V,C1,just(C2)) = cons4(notb(eq(C1,C2)),colouring(A,Z)) ).

cnf(axiom_004,axiom,
    aux3(A,Z,U,V,nothing) = cons4(bfalse,colouring(A,Z)) ).

cnf(axiom_005,axiom,
    aux3(A,Z,U,V,just(C1)) = aux2(A,Z,V,C1,index(A,V)) ).

cnf(axiom_006,axiom,
    ten = suc(suc(suc(suc(suc(suc(suc(suc(suc(suc(zero)))))))))) ).

cnf(axiom_007,axiom,
    predNat(zero) = zero ).

cnf(axiom_008,axiom,
    predNat(suc(Y)) = Y ).

cnf(axiom_009,axiom,
    petersen2(nil3) = nil ).

cnf(axiom_010,axiom,
    petersen2(cons3(Y,Z)) = cons(pair2(Y,suc(Y)),petersen2(Z)) ).

cnf(axiom_011,axiom,
    one = suc(zero) ).

cnf(axiom_012,axiom,
    two = suc(one) ).

cnf(axiom_013,axiom,
    three = suc(two) ).

cnf(axiom_014,axiom,
    notb(btrue) = bfalse ).

cnf(axiom_015,axiom,
    notb(bfalse) = btrue ).

cnf(axiom_016,axiom,
    lt(zero,zero) = bfalse ).

cnf(axiom_017,axiom,
    lt(zero,suc(Z)) = btrue ).

cnf(axiom_018,axiom,
    lt(suc(X2),zero) = bfalse ).

cnf(axiom_019,axiom,
    lt(suc(X2),suc(Y2)) = lt(X2,Y2) ).

cnf(axiom_020,axiom,
    prop_p31(nil3) = nil4 ).

cnf(axiom_021,axiom,
    prop_p31(cons3(Y,Z)) = cons4(lt(Y,three),prop_p31(Z)) ).

cnf(axiom_022,axiom,
    index(nil3,Y) = nothing ).

cnf(axiom_023,axiom,
    index(cons3(Z,X2),zero) = just(Z) ).

cnf(axiom_024,axiom,
    index(cons3(Z,X2),suc(N)) = index(X2,N) ).

cnf(axiom_025,axiom,
    four = suc(three) ).

cnf(axiom_026,axiom,
    five = suc(four) ).

cnf(axiom_027,axiom,
    seven = suc(suc(five)) ).

cnf(axiom_028,axiom,
    nine = suc(suc(seven)) ).

cnf(axiom_029,axiom,
    enumFromToNat(X,Y) = aux(X,Y,lt(Y,X)) ).

cnf(axiom_030,axiom,
    eleven = suc(suc(nine)) ).

cnf(axiom_031,axiom,
    colouring(A,nil) = nil4 ).

cnf(axiom_032,axiom,
    colouring(A,cons(pair2(U,V),Z)) = aux3(A,Z,U,V,index(A,U)) ).

cnf(axiom_033,axiom,
    append(nil,Y) = Y ).

cnf(axiom_034,axiom,
    append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)) ).

cnf(axiom_035,axiom,
    concat(nil2) = nil ).

cnf(axiom_036,axiom,
    concat(cons2(Y,Xs)) = append(Y,concat(Xs)) ).

cnf(axiom_037,axiom,
    andb(btrue,Q) = Q ).

cnf(axiom_038,axiom,
    andb(bfalse,Q) = bfalse ).

cnf(axiom_039,axiom,
    and2(nil4) = btrue ).

cnf(axiom_040,axiom,
    and2(cons4(Y,Xs)) = andb(Y,and2(Xs)) ).

cnf(axiom_041,axiom,
    colouring2(X,Y) = and2(colouring(Y,X)) ).

cnf(axiom_042,axiom,
    add(zero,Y) = Y ).

cnf(axiom_043,axiom,
    add(suc(Z),Y) = suc(add(Z,Y)) ).

cnf(axiom_044,axiom,
    petersen(X,nil) = nil2 ).

cnf(axiom_045,axiom,
    petersen(X,cons(pair2(U,V),X2)) = cons2(cons(pair2(U,V),cons(pair2(add(suc(X),U),add(suc(X),V)),nil)),petersen(X,X2)) ).

cnf(axiom_046,axiom,
    petersen3(X,nil3) = nil ).

cnf(axiom_047,axiom,
    petersen3(X,cons3(Z,X2)) = cons(pair2(Z,add(suc(X),Z)),petersen3(X,X2)) ).

cnf(axiom_048,axiom,
    petersen4(zero) = nil ).

cnf(axiom_049,axiom,
    petersen4(suc(Y)) = append(concat(petersen(Y,cons(pair2(Y,zero),petersen2(enumFromToNat(zero,Y))))),petersen3(Y,enumFromToNat(zero,suc(Y)))) ).

cnf(axiom_050,axiom,
    twentyOne = add(ten,eleven) ).

cnf(axiom_051,axiom,
    thirtyOne = add(twentyOne,ten) ).

cnf(axiom_052,axiom,
    prop_p312(X) = notb(andb(colouring2(petersen4(thirtyOne),X),and2(prop_p31(X)))) ).

cnf(axiom_053,axiom,
    eq2(bfalse,btrue) = bfalse ).

cnf(axiom_054,axiom,
    eq2(btrue,bfalse) = bfalse ).

cnf(axiom_055,axiom,
    eq(suc(X),suc(Y)) = eq(X,Y) ).

cnf(axiom_056,axiom,
    eq(zero,suc(X)) = bfalse ).

cnf(axiom_057,axiom,
    eq(suc(X),zero) = bfalse ).

cnf(axiom_058,axiom,
    eq(X,X) = btrue ).

cnf(axiom_059,axiom,
    eq2(X,X) = btrue ).

cnf(goal,negated_conjecture,
    eq2(prop_p312(X),bfalse) != btrue ).

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