TPTP Problem File: SWX230_1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX230_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_d5.p [CST26]
% Status : Theorem
% Rating : 1.00 v9.3.0
% Syntax : Number of formulae : 60 ( 50 unt; 1 typ; 0 def)
% Number of atoms : 337 ( 56 equ)
% Maximal formula atoms : 3 ( 5 avg)
% Number of connectives : 22 ( 9 ~; 0 |; 2 &)
% ( 4 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of FOOLs : 273 ( 267 fml; 6 var)
% Number of types : 2 ( 0 usr)
% Number of type conns : 2 ( 1 >; 1 *; 0 +; 0 <<)
% Number of predicates : 44 ( 42 usr; 11 prp; 0-2 aty)
% Number of functors : 1 ( 1 usr; 0 con; 2-2 aty)
% Number of variables : 94 ( 93 !; 1 ?; 4 :)
% SPC : TX0_THM_EQU_NAR
% Comments :
%------------------------------------------------------------------------------
tff(type_001,type,
cons3: ( $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: $o,X2] :
( head3(cons3((X),X2))
<=> (X) ) ).
tff(axiom_011,axiom,
! [X: $o,X2] : ( tail3(cons3((X),X2)) = X2 ) ).
tff(axiom_012,axiom,
! [X: $o,X2] : ( nil3 != cons3((X),X2) ) ).
tff(axiom_013,axiom,
! [X] : ( proj1Suc(suc(X)) = X ) ).
tff(axiom_014,axiom,
! [X] : ( zero != suc(X) ) ).
tff(axiom_015,axiom,
! [X] : ( proj1Just(just(X)) = X ) ).
tff(axiom_016,axiom,
! [X] : ( nothing != just(X) ) ).
tff(axiom_017,axiom,
predNat(zero) = zero ).
tff(axiom_018,axiom,
! [Y] : ( predNat(suc(Y)) = Y ) ).
tff(axiom_019,axiom,
one = suc(zero) ).
tff(axiom_020,axiom,
two = suc(one) ).
tff(axiom_021,axiom,
three = suc(two) ).
tff(axiom_022,axiom,
~ lt(zero,zero) ).
tff(axiom_023,axiom,
! [Z] : lt(zero,suc(Z)) ).
tff(axiom_024,axiom,
! [X2] : ~ lt(suc(X2),zero) ).
tff(axiom_025,axiom,
! [X2,Y2] :
( lt(suc(X2),suc(Y2))
<=> lt(X2,Y2) ) ).
tff(axiom_026,axiom,
! [Y] : ( index(nil2,Y) = nothing ) ).
tff(axiom_027,axiom,
! [Z,X2] : ( index(cons2(Z,X2),zero) = just(Z) ) ).
tff(axiom_028,axiom,
! [Z,X2,N] : ( index(cons2(Z,X2),suc(N)) = index(X2,N) ) ).
tff(axiom_029,axiom,
four = suc(three) ).
tff(axiom_030,axiom,
formula(nil2) = nil3 ).
tff(axiom_031,axiom,
! [Y,Z] : ( formula(cons2(Y,Z)) = cons3(lt(Y,three),formula(Z)) ) ).
tff(axiom_032,axiom,
five = suc(four) ).
tff(axiom_033,axiom,
! [X,Y] :
( lt(Y,X)
=> ( enumFromToNat(X,Y) = nil2 ) ) ).
tff(axiom_034,axiom,
! [X,Y] :
( ~ lt(Y,X)
=> ( enumFromToNat(X,Y) = cons2(X,enumFromToNat(suc(X),Y)) ) ) ).
tff(axiom_035,axiom,
dodeca(nil2) = nil ).
tff(axiom_036,axiom,
! [Y,Z] : ( dodeca(cons2(Y,Z)) = cons(pair2(Y,suc(Y)),dodeca(Z)) ) ).
tff(axiom_037,axiom,
! [A] : ( colouring(A,nil) = nil3 ) ).
tff(axiom_038,axiom,
! [A,Z,U,V] :
( ( index(A,U) = nothing )
=> ( colouring(A,cons(pair2(U,V),Z)) = cons3($false,colouring(A,Z)) ) ) ).
tff(axiom_039,axiom,
! [A,Z,U,V,C1] :
( ( index(A,U) = just(C1) )
=> ( ( index(A,V) = nothing )
=> ( colouring(A,cons(pair2(U,V),Z)) = cons3($false,colouring(A,Z)) ) ) ) ).
tff(axiom_040,axiom,
! [A,Z,U,V,C1,C2] :
( ( index(A,U) = just(C1) )
=> ( ( index(A,V) = just(C2) )
=> ( colouring(A,cons(pair2(U,V),Z)) = cons3(C1 != C2,colouring(A,Z)) ) ) ) ).
tff(axiom_041,axiom,
! [Y] : ( append(nil,Y) = Y ) ).
tff(axiom_042,axiom,
! [Y,Z,Xs] : ( append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)) ) ).
tff(axiom_043,axiom,
and2(nil3) ).
tff(axiom_044,axiom,
! [Y: $o,Xs] :
( and2(cons3((Y),Xs))
<=> ( (Y)
& and2(Xs) ) ) ).
tff(axiom_045,axiom,
! [X,Y] :
( colouring2(X,Y)
<=> and2(colouring(Y,X)) ) ).
tff(axiom_046,axiom,
! [Y] : ( add(zero,Y) = Y ) ).
tff(axiom_047,axiom,
! [Y,Z] : ( add(suc(Z),Y) = suc(add(Z,Y)) ) ).
tff(axiom_048,axiom,
! [X] : ( dodeca2(X,nil2) = nil ) ).
tff(axiom_049,axiom,
! [X,Z,X2] : ( dodeca2(X,cons2(Z,X2)) = cons(pair2(Z,add(suc(X),Z)),dodeca2(X,X2)) ) ).
tff(axiom_050,axiom,
! [X] : ( dodeca3(X,nil2) = nil ) ).
tff(axiom_051,axiom,
! [X,Z,X2] : ( dodeca3(X,cons2(Z,X2)) = cons(pair2(add(suc(X),Z),add(add(suc(X),suc(X)),Z)),dodeca3(X,X2)) ) ).
tff(axiom_052,axiom,
! [X] : ( dodeca4(X,nil2) = nil ) ).
tff(axiom_053,axiom,
! [X,Z,X2] : ( dodeca4(X,cons2(Z,X2)) = cons(pair2(add(suc(X),suc(Z)),add(add(suc(X),suc(X)),Z)),dodeca4(X,X2)) ) ).
tff(axiom_054,axiom,
! [X] : ( dodeca5(X,nil2) = nil ) ).
tff(axiom_055,axiom,
! [X,Z,X2] : ( dodeca5(X,cons2(Z,X2)) = cons(pair2(add(add(suc(X),suc(X)),Z),add(add(add(suc(X),suc(X)),suc(X)),Z)),dodeca5(X,X2)) ) ).
tff(axiom_056,axiom,
! [X] : ( dodeca6(X,nil2) = nil ) ).
tff(axiom_057,axiom,
! [X,Z,X2] : ( dodeca6(X,cons2(Z,X2)) = cons(pair2(add(add(add(suc(X),suc(X)),suc(X)),Z),add(add(add(suc(X),suc(X)),suc(X)),suc(Z))),dodeca6(X,X2)) ) ).
tff(axiom_058,axiom,
dodeca7(zero) = nil ).
tff(axiom_059,axiom,
! [Y] : ( dodeca7(suc(Y)) = append(cons(pair2(Y,zero),dodeca(enumFromToNat(zero,Y))),append(dodeca2(Y,enumFromToNat(zero,suc(Y))),append(dodeca3(Y,enumFromToNat(zero,suc(Y))),append(cons(pair2(suc(Y),add(add(suc(Y),suc(Y)),Y)),dodeca4(Y,enumFromToNat(zero,Y))),append(dodeca5(Y,enumFromToNat(zero,suc(Y))),cons(pair2(add(add(add(suc(Y),suc(Y)),suc(Y)),Y),add(add(add(suc(Y),suc(Y)),suc(Y)),zero)),dodeca6(Y,enumFromToNat(zero,Y)))))))) ) ).
tff(goal_060,conjecture,
? [A] :
( colouring2(dodeca7(five),A)
& and2(formula(A)) ) ).
%------------------------------------------------------------------------------