TPTP Problem File: SWX231_1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% 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 : Theorem
% Rating : 1.00 v9.3.0
% Syntax : Number of formulae : 65 ( 55 unt; 1 typ; 0 def)
% Number of atoms : 298 ( 61 equ)
% Maximal formula atoms : 3 ( 4 avg)
% Number of connectives : 23 ( 10 ~; 0 |; 2 &)
% ( 4 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of FOOLs : 229 ( 223 fml; 6 var)
% Number of types : 2 ( 0 usr)
% Number of type conns : 2 ( 1 >; 1 *; 0 +; 0 <<)
% Number of predicates : 52 ( 50 usr; 18 prp; 0-2 aty)
% Number of functors : 1 ( 1 usr; 0 con; 2-2 aty)
% Number of variables : 91 ( 90 !; 1 ?; 4 :)
% SPC : TX0_THM_EQU_NAR
% Comments :
%------------------------------------------------------------------------------
tff(type_001,type,
cons4: ( $o * $i ) > $i ).
tff(axiom_002,axiom,
! [X,X2] : ( proj1pair(pair2(X,X2)) = X ) ).
tff(axiom_003,axiom,
! [X,X2] : ( proj2pair(pair2(X,X2)) = X2 ) ).
tff(axiom_004,axiom,
! [X,X2] : ( head(cons(X,X2)) = X ) ).
tff(axiom_005,axiom,
! [X,X2] : ( tail(cons(X,X2)) = X2 ) ).
tff(axiom_006,axiom,
! [X,X2] : ( nil != cons(X,X2) ) ).
tff(axiom_007,axiom,
! [X,X2] : ( head2(cons2(X,X2)) = X ) ).
tff(axiom_008,axiom,
! [X,X2] : ( tail2(cons2(X,X2)) = X2 ) ).
tff(axiom_009,axiom,
! [X,X2] : ( nil2 != cons2(X,X2) ) ).
tff(axiom_010,axiom,
! [X,X2] : ( head3(cons3(X,X2)) = X ) ).
tff(axiom_011,axiom,
! [X,X2] : ( tail3(cons3(X,X2)) = X2 ) ).
tff(axiom_012,axiom,
! [X,X2] : ( nil3 != cons3(X,X2) ) ).
tff(axiom_013,axiom,
! [X: $o,X2] :
( head4(cons4((X),X2))
<=> (X) ) ).
tff(axiom_014,axiom,
! [X: $o,X2] : ( tail4(cons4((X),X2)) = X2 ) ).
tff(axiom_015,axiom,
! [X: $o,X2] : ( nil4 != cons4((X),X2) ) ).
tff(axiom_016,axiom,
! [X] : ( proj1Suc(suc(X)) = X ) ).
tff(axiom_017,axiom,
! [X] : ( zero != suc(X) ) ).
tff(axiom_018,axiom,
! [X] : ( proj1Just(just(X)) = X ) ).
tff(axiom_019,axiom,
! [X] : ( nothing != just(X) ) ).
tff(axiom_020,axiom,
ten = suc(suc(suc(suc(suc(suc(suc(suc(suc(suc(zero)))))))))) ).
tff(axiom_021,axiom,
predNat(zero) = zero ).
tff(axiom_022,axiom,
! [Y] : ( predNat(suc(Y)) = Y ) ).
tff(axiom_023,axiom,
petersen2(nil3) = nil ).
tff(axiom_024,axiom,
! [Y,Z] : ( petersen2(cons3(Y,Z)) = cons(pair2(Y,suc(Y)),petersen2(Z)) ) ).
tff(axiom_025,axiom,
one = suc(zero) ).
tff(axiom_026,axiom,
two = suc(one) ).
tff(axiom_027,axiom,
three = suc(two) ).
tff(axiom_028,axiom,
~ lt(zero,zero) ).
tff(axiom_029,axiom,
! [Z] : lt(zero,suc(Z)) ).
tff(axiom_030,axiom,
! [X2] : ~ lt(suc(X2),zero) ).
tff(axiom_031,axiom,
! [X2,Y2] :
( lt(suc(X2),suc(Y2))
<=> lt(X2,Y2) ) ).
tff(axiom_032,axiom,
! [Y] : ( index(nil3,Y) = nothing ) ).
tff(axiom_033,axiom,
! [Z,X2] : ( index(cons3(Z,X2),zero) = just(Z) ) ).
tff(axiom_034,axiom,
! [Z,X2,N] : ( index(cons3(Z,X2),suc(N)) = index(X2,N) ) ).
tff(axiom_035,axiom,
four = suc(three) ).
tff(axiom_036,axiom,
formula(nil3) = nil4 ).
tff(axiom_037,axiom,
! [Y,Z] : ( formula(cons3(Y,Z)) = cons4(lt(Y,three),formula(Z)) ) ).
tff(axiom_038,axiom,
five = suc(four) ).
tff(axiom_039,axiom,
seven = suc(suc(five)) ).
tff(axiom_040,axiom,
nine = suc(suc(seven)) ).
tff(axiom_041,axiom,
! [X,Y] :
( lt(Y,X)
=> ( enumFromToNat(X,Y) = nil3 ) ) ).
tff(axiom_042,axiom,
! [X,Y] :
( ~ lt(Y,X)
=> ( enumFromToNat(X,Y) = cons3(X,enumFromToNat(suc(X),Y)) ) ) ).
tff(axiom_043,axiom,
eleven = suc(suc(nine)) ).
tff(axiom_044,axiom,
! [A] : ( colouring(A,nil) = nil4 ) ).
tff(axiom_045,axiom,
! [A,Z,U,V] :
( ( index(A,U) = nothing )
=> ( colouring(A,cons(pair2(U,V),Z)) = cons4($false,colouring(A,Z)) ) ) ).
tff(axiom_046,axiom,
! [A,Z,U,V,C1] :
( ( index(A,U) = just(C1) )
=> ( ( index(A,V) = nothing )
=> ( colouring(A,cons(pair2(U,V),Z)) = cons4($false,colouring(A,Z)) ) ) ) ).
tff(axiom_047,axiom,
! [A,Z,U,V,C1,C2] :
( ( index(A,U) = just(C1) )
=> ( ( index(A,V) = just(C2) )
=> ( colouring(A,cons(pair2(U,V),Z)) = cons4(C1 != C2,colouring(A,Z)) ) ) ) ).
tff(axiom_048,axiom,
! [Y] : ( append(nil,Y) = Y ) ).
tff(axiom_049,axiom,
! [Y,Z,Xs] : ( append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)) ) ).
tff(axiom_050,axiom,
concat(nil2) = nil ).
tff(axiom_051,axiom,
! [Y,Xs] : ( concat(cons2(Y,Xs)) = append(Y,concat(Xs)) ) ).
tff(axiom_052,axiom,
and2(nil4) ).
tff(axiom_053,axiom,
! [Y: $o,Xs] :
( and2(cons4((Y),Xs))
<=> ( (Y)
& and2(Xs) ) ) ).
tff(axiom_054,axiom,
! [X,Y] :
( colouring2(X,Y)
<=> and2(colouring(Y,X)) ) ).
tff(axiom_055,axiom,
! [Y] : ( add(zero,Y) = Y ) ).
tff(axiom_056,axiom,
! [Y,Z] : ( add(suc(Z),Y) = suc(add(Z,Y)) ) ).
tff(axiom_057,axiom,
! [X] : ( petersen(X,nil) = nil2 ) ).
tff(axiom_058,axiom,
! [X,X2,U,V] : ( 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)) ) ).
tff(axiom_059,axiom,
! [X] : ( petersen3(X,nil3) = nil ) ).
tff(axiom_060,axiom,
! [X,Z,X2] : ( petersen3(X,cons3(Z,X2)) = cons(pair2(Z,add(suc(X),Z)),petersen3(X,X2)) ) ).
tff(axiom_061,axiom,
petersen4(zero) = nil ).
tff(axiom_062,axiom,
! [Y] : ( petersen4(suc(Y)) = append(concat(petersen(Y,cons(pair2(Y,zero),petersen2(enumFromToNat(zero,Y))))),petersen3(Y,enumFromToNat(zero,suc(Y)))) ) ).
tff(axiom_063,axiom,
twentyOne = add(ten,eleven) ).
tff(axiom_064,axiom,
thirtyOne = add(twentyOne,ten) ).
tff(goal_065,conjecture,
? [A] :
( colouring2(petersen4(thirtyOne),A)
& and2(formula(A)) ) ).
%------------------------------------------------------------------------------