TPTP Problem File: SWX232_1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX232_1 : TPTP v9.3.0. Released v9.3.0.
% Domain : Software Verification
% Problem : Find a tour in a graph
% Version : Especial.
% English :
% Refs : [CST26] Claessen et al. (2026), Email to Geoff Sutcliffe
% Source : [CST26]
% Names : Graph_prop_t3.p [CST26]
% Status : Theorem
% Rating : 1.00 v9.3.0
% Syntax : Number of formulae : 67 ( 56 unt; 1 typ; 0 def)
% Number of atoms : 353 ( 54 equ)
% Maximal formula atoms : 5 ( 5 avg)
% Number of connectives : 34 ( 13 ~; 3 |; 7 &)
% ( 7 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of FOOLs : 274 ( 268 fml; 6 var)
% Number of types : 2 ( 0 usr)
% Number of type conns : 2 ( 1 >; 1 *; 0 +; 0 <<)
% Number of predicates : 43 ( 42 usr; 7 prp; 0-3 aty)
% Number of functors : 1 ( 1 usr; 0 con; 2-2 aty)
% Number of variables : 110 ( 109 !; 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,
predNat(zero) = zero ).
tff(axiom_016,axiom,
! [Y] : ( predNat(suc(Y)) = Y ) ).
tff(axiom_017,axiom,
! [X,Y] : ( path(X,Y,nil) = nil3 ) ).
tff(axiom_018,axiom,
! [X,Y,X3,U,V] :
( path(X,Y,cons(pair2(U,V),X3)) = cons3(( ( ( U = X )
& ( V = Y ) )
| ( ( U = Y )
& ( V = X ) ) ),path(X,Y,X3)) ) ).
tff(axiom_019,axiom,
~ or2(nil3) ).
tff(axiom_020,axiom,
! [Y: $o,Xs] :
( or2(cons3((Y),Xs))
<=> ( (Y)
| or2(Xs) ) ) ).
tff(axiom_021,axiom,
! [Y] : path2(nil2,Y) ).
tff(axiom_022,axiom,
! [Y,Z] : path2(cons2(Z,nil2),Y) ).
tff(axiom_023,axiom,
! [Y,Z,Y2,Xs] :
( path2(cons2(Z,cons2(Y2,Xs)),Y)
<=> ( or2(path(Z,Y2,Y))
& path2(cons2(Y2,Xs),Y) ) ) ).
tff(axiom_024,axiom,
one = suc(zero) ).
tff(axiom_025,axiom,
two = suc(one) ).
tff(axiom_026,axiom,
three = suc(two) ).
tff(axiom_027,axiom,
~ lt(zero,zero) ).
tff(axiom_028,axiom,
! [Z] : lt(zero,suc(Z)) ).
tff(axiom_029,axiom,
! [X2] : ~ lt(suc(X2),zero) ).
tff(axiom_030,axiom,
! [X2,Y2] :
( lt(suc(X2),suc(Y2))
<=> lt(X2,Y2) ) ).
tff(axiom_031,axiom,
! [X,Y] :
( lt(X,Y)
=> ( maxNat(X,Y) = Y ) ) ).
tff(axiom_032,axiom,
! [X,Y] :
( ~ lt(X,Y)
=> ( maxNat(X,Y) = X ) ) ).
tff(axiom_033,axiom,
! [X] : ( maximum(X,nil) = X ) ).
tff(axiom_034,axiom,
! [X,Yzs,Y2,Z2] : ( maximum(X,cons(pair2(Y2,Z2),Yzs)) = maximum(maxNat(X,maxNat(Y2,Z2)),Yzs) ) ).
tff(axiom_035,axiom,
len(nil2) = zero ).
tff(axiom_036,axiom,
! [Y,Xs] : ( len(cons2(Y,Xs)) = suc(len(Xs)) ) ).
tff(axiom_037,axiom,
! [X] : ( last(X,nil2) = X ) ).
tff(axiom_038,axiom,
! [X,Z,Ys] : ( last(X,cons2(Z,Ys)) = last(Z,Ys) ) ).
tff(axiom_039,axiom,
! [X,Y] :
( lt(Y,X)
=> ( enumFromToNat(X,Y) = nil2 ) ) ).
tff(axiom_040,axiom,
! [X,Y] :
( ~ lt(Y,X)
=> ( enumFromToNat(X,Y) = cons2(X,enumFromToNat(suc(X),Y)) ) ) ).
tff(axiom_041,axiom,
! [X] : ~ elem(X,nil2) ).
tff(axiom_042,axiom,
! [X,Z,Xs] :
( elem(X,cons2(Z,Xs))
<=> ( ( Z = X )
| elem(X,Xs) ) ) ).
tff(axiom_043,axiom,
unique(nil2) ).
tff(axiom_044,axiom,
! [Y,Xs] :
( unique(cons2(Y,Xs))
<=> ( ~ elem(Y,Xs)
& unique(Xs) ) ) ).
tff(axiom_045,axiom,
dodeca(nil2) = nil ).
tff(axiom_046,axiom,
! [Y,Z] : ( dodeca(cons2(Y,Z)) = cons(pair2(Y,suc(Y)),dodeca(Z)) ) ).
tff(axiom_047,axiom,
! [Y] : ( append(nil,Y) = Y ) ).
tff(axiom_048,axiom,
! [Y,Z,Xs] : ( append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)) ) ).
tff(axiom_049,axiom,
! [Y] : ( add(zero,Y) = Y ) ).
tff(axiom_050,axiom,
! [Y,Z] : ( add(suc(Z),Y) = suc(add(Z,Y)) ) ).
tff(axiom_051,axiom,
! [X] : ( dodeca2(X,nil2) = nil ) ).
tff(axiom_052,axiom,
! [X,Z,X2] : ( dodeca2(X,cons2(Z,X2)) = cons(pair2(Z,add(suc(X),Z)),dodeca2(X,X2)) ) ).
tff(axiom_053,axiom,
! [X] : ( dodeca3(X,nil2) = nil ) ).
tff(axiom_054,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_055,axiom,
! [X] : ( dodeca4(X,nil2) = nil ) ).
tff(axiom_056,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_057,axiom,
! [X] : ( dodeca5(X,nil2) = nil ) ).
tff(axiom_058,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_059,axiom,
! [X] : ( dodeca6(X,nil2) = nil ) ).
tff(axiom_060,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_061,axiom,
dodeca7(zero) = nil ).
tff(axiom_062,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(axiom_063,axiom,
tour(nil2,nil) ).
tff(axiom_064,axiom,
! [Z,X2] : ~ tour(nil2,cons(Z,X2)) ).
tff(axiom_065,axiom,
! [X3,X4] : ~ tour(cons2(X3,X4),nil) ).
tff(axiom_066,axiom,
! [X3,X4,Vs,U,V] :
( tour(cons2(X3,X4),cons(pair2(U,V),Vs))
<=> ( ( X3 = last(X3,X4) )
& path2(cons2(X3,X4),cons(pair2(U,V),Vs))
& unique(X4)
& ( len(cons2(X3,X4)) = add(two,maximum(maxNat(U,V),Vs)) ) ) ) ).
tff(goal_067,conjecture,
? [P] : tour(P,dodeca7(three)) ).
%------------------------------------------------------------------------------