%------------------------------------------------------------------------------
% File     : SWX229_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_bt3.p [CST26]

% Status   : Theorem
% Rating   : 1.00 v9.3.0
% Syntax   : Number of formulae    :   99 (  83 unt;   1 typ;   0 def)
%            Number of atoms       :  493 (  70 equ)
%            Maximal formula atoms :    5 (   5 avg)
%            Number of connectives :   48 (  23   ~;   2   |;   7   &)
%                                         (  10 <=>;   6  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   10 (   3 avg)
%            Maximal term depth    :    2 (   1 avg)
%            Number of FOOLs       :  378 ( 372 fml;   6 var)
%            Number of types       :    2 (   0 usr)
%            Number of type conns  :    2 (   1   >;   1   *;   0   +;   0  <<)
%            Number of predicates  :   66 (  65 usr;  12 prp; 0-3 aty)
%            Number of functors    :    1 (   1 usr;   0 con; 2-2 aty)
%            Number of variables   :  153 ( 152   !;   1   ?;   4   :)
% SPC      : TX0_THM_EQU_NAR

% Comments :
%------------------------------------------------------------------------------
tff(type_001,type,
    cons6: ( $o * $i ) > $i ).

tff(axiom_002,axiom,
    ! [X,X2] : ( proj1pair(pair22(X,X2)) = X ) ).

tff(axiom_003,axiom,
    ! [X,X2] : ( proj2pair(pair22(X,X2)) = X2 ) ).

tff(axiom_004,axiom,
    ! [X,X2] : ( proj1pair2(pair23(X,X2)) = X ) ).

tff(axiom_005,axiom,
    ! [X,X2] : ( proj2pair2(pair23(X,X2)) = X2 ) ).

tff(axiom_006,axiom,
    ! [X,X2] : ( head(cons(X,X2)) = X ) ).

tff(axiom_007,axiom,
    ! [X,X2] : ( tail(cons(X,X2)) = X2 ) ).

tff(axiom_008,axiom,
    ! [X,X2] : ( nil != cons(X,X2) ) ).

tff(axiom_009,axiom,
    ! [X,X2] : ( head2(cons2(X,X2)) = X ) ).

tff(axiom_010,axiom,
    ! [X,X2] : ( tail2(cons2(X,X2)) = X2 ) ).

tff(axiom_011,axiom,
    ! [X,X2] : ( nil2 != cons2(X,X2) ) ).

tff(axiom_012,axiom,
    ! [X,X2] : ( head3(cons3(X,X2)) = X ) ).

tff(axiom_013,axiom,
    ! [X,X2] : ( tail3(cons3(X,X2)) = X2 ) ).

tff(axiom_014,axiom,
    ! [X,X2] : ( nil3 != cons3(X,X2) ) ).

tff(axiom_015,axiom,
    ! [X,X2] : ( head4(cons4(X,X2)) = X ) ).

tff(axiom_016,axiom,
    ! [X,X2] : ( tail4(cons4(X,X2)) = X2 ) ).

tff(axiom_017,axiom,
    ! [X,X2] : ( nil4 != cons4(X,X2) ) ).

tff(axiom_018,axiom,
    ! [X,X2] : ( head5(cons5(X,X2)) = X ) ).

tff(axiom_019,axiom,
    ! [X,X2] : ( tail5(cons5(X,X2)) = X2 ) ).

tff(axiom_020,axiom,
    ! [X,X2] : ( nil5 != cons5(X,X2) ) ).

tff(axiom_021,axiom,
    ! [X: $o,X2] :
      ( head6(cons6((X),X2))
    <=> (X) ) ).

tff(axiom_022,axiom,
    ! [X: $o,X2] : ( tail6(cons6((X),X2)) = X2 ) ).

tff(axiom_023,axiom,
    ! [X: $o,X2] : ( nil6 != cons6((X),X2) ) ).

tff(axiom_024,axiom,
    ! [X] : ( proj1Suc(suc(X)) = X ) ).

tff(axiom_025,axiom,
    ! [X] : ( zero != suc(X) ) ).

tff(axiom_026,axiom,
    i != o ).

tff(axiom_027,axiom,
    predNat(zero) = zero ).

tff(axiom_028,axiom,
    ! [Y] : ( predNat(suc(Y)) = Y ) ).

tff(axiom_029,axiom,
    ~ or2(nil6) ).

tff(axiom_030,axiom,
    ! [Y: $o,Xs] :
      ( or2(cons6((Y),Xs))
    <=> ( (Y)
        | or2(Xs) ) ) ).

tff(axiom_031,axiom,
    one = suc(zero) ).

tff(axiom_032,axiom,
    two = suc(one) ).

tff(axiom_033,axiom,
    three = suc(two) ).

tff(axiom_034,axiom,
    ~ lt(zero,zero) ).

tff(axiom_035,axiom,
    ! [Z] : lt(zero,suc(Z)) ).

tff(axiom_036,axiom,
    ! [X2] : ~ lt(suc(X2),zero) ).

tff(axiom_037,axiom,
    ! [X2,Y2] :
      ( lt(suc(X2),suc(Y2))
    <=> lt(X2,Y2) ) ).

tff(axiom_038,axiom,
    ! [X,Y] :
      ( lt(X,Y)
     => ( maxNat(X,Y) = Y ) ) ).

tff(axiom_039,axiom,
    ! [X,Y] :
      ( ~ lt(X,Y)
     => ( maxNat(X,Y) = X ) ) ).

tff(axiom_040,axiom,
    ! [X] : ( maximum(X,nil2) = X ) ).

tff(axiom_041,axiom,
    ! [X,Yzs,Y2,Z2] : ( maximum(X,cons2(pair23(Y2,Z2),Yzs)) = maximum(maxNat(X,maxNat(Y2,Z2)),Yzs) ) ).

tff(axiom_042,axiom,
    len(nil3) = zero ).

tff(axiom_043,axiom,
    ! [Y,Xs] : ( len(cons3(Y,Xs)) = suc(len(Xs)) ) ).

tff(axiom_044,axiom,
    ! [X] : ( last(X,nil3) = X ) ).

tff(axiom_045,axiom,
    ! [X,Z,Ys] : ( last(X,cons3(Z,Ys)) = last(Z,Ys) ) ).

tff(axiom_046,axiom,
    halfNat(zero) = zero ).

tff(axiom_047,axiom,
    halfNat(suc(zero)) = zero ).

tff(axiom_048,axiom,
    ! [N] : ( halfNat(suc(suc(N))) = suc(halfNat(N)) ) ).

tff(axiom_049,axiom,
    evenNat(zero) ).

tff(axiom_050,axiom,
    ~ evenNat(suc(zero)) ).

tff(axiom_051,axiom,
    ! [N] :
      ( evenNat(suc(suc(N)))
    <=> evenNat(N) ) ).

tff(axiom_052,axiom,
    ! [X,Y] :
      ( lt(Y,X)
     => ( enumFromToNat(X,Y) = nil4 ) ) ).

tff(axiom_053,axiom,
    ! [X,Y] :
      ( ~ lt(Y,X)
     => ( enumFromToNat(X,Y) = cons4(X,enumFromToNat(suc(X),Y)) ) ) ).

tff(axiom_054,axiom,
    dodeca(nil4) = nil2 ).

tff(axiom_055,axiom,
    ! [Y,Z] : ( dodeca(cons4(Y,Z)) = cons2(pair23(Y,suc(Y)),dodeca(Z)) ) ).

tff(axiom_056,axiom,
    bin(zero) = nil5 ).

tff(axiom_057,axiom,
    ! [Y] :
      ( evenNat(suc(Y))
     => ( bin(suc(Y)) = cons5(o,bin(halfNat(suc(Y)))) ) ) ).

tff(axiom_058,axiom,
    ! [Y] :
      ( ~ evenNat(suc(Y))
     => ( bin(suc(Y)) = cons5(i,bin(halfNat(suc(Y)))) ) ) ).

tff(axiom_059,axiom,
    bgraph(nil2) = nil ).

tff(axiom_060,axiom,
    ! [Z,U,V] : ( bgraph(cons2(pair23(U,V),Z)) = cons(pair22(bin(U),bin(V)),bgraph(Z)) ) ).

tff(axiom_061,axiom,
    beq(nil5,nil5) ).

tff(axiom_062,axiom,
    ! [Z,X2] : ~ beq(nil5,cons5(Z,X2)) ).

tff(axiom_063,axiom,
    ! [Xs] : ~ beq(cons5(i,Xs),nil5) ).

tff(axiom_064,axiom,
    ! [Xs,Ys] :
      ( beq(cons5(i,Xs),cons5(i,Ys))
    <=> beq(Xs,Ys) ) ).

tff(axiom_065,axiom,
    ! [Xs,Ys] : ~ beq(cons5(i,Xs),cons5(o,Ys)) ).

tff(axiom_066,axiom,
    ! [Xs] : ~ beq(cons5(o,Xs),nil5) ).

tff(axiom_067,axiom,
    ! [Xs,Zs] : ~ beq(cons5(o,Xs),cons5(i,Zs)) ).

tff(axiom_068,axiom,
    ! [Xs,Zs] :
      ( beq(cons5(o,Xs),cons5(o,Zs))
    <=> beq(Xs,Zs) ) ).

tff(axiom_069,axiom,
    ! [X,Y] : ( bpath(X,Y,nil) = nil6 ) ).

tff(axiom_070,axiom,
    ! [X,Y,X3,U,V] :
      ( bpath(X,Y,cons(pair22(U,V),X3)) = cons6(( ( beq(U,X)
            & beq(V,Y) )
          | ( beq(U,Y)
            & beq(V,X) ) ),bpath(X,Y,X3)) ) ).

tff(axiom_071,axiom,
    ! [Y] : bpath2(nil3,Y) ).

tff(axiom_072,axiom,
    ! [Y,Z] : bpath2(cons3(Z,nil3),Y) ).

tff(axiom_073,axiom,
    ! [Y,Z,Y2,Xs] :
      ( bpath2(cons3(Z,cons3(Y2,Xs)),Y)
    <=> ( or2(bpath(Z,Y2,Y))
        & bpath2(cons3(Y2,Xs),Y) ) ) ).

tff(axiom_074,axiom,
    ! [X] : ( belem(X,nil3) = nil6 ) ).

tff(axiom_075,axiom,
    ! [X,Z,X2] : ( belem(X,cons3(Z,X2)) = cons6(beq(X,Z),belem(X,X2)) ) ).

tff(axiom_076,axiom,
    ! [X,Y] :
      ( belem2(X,Y)
    <=> or2(belem(X,Y)) ) ).

tff(axiom_077,axiom,
    bunique(nil3) ).

tff(axiom_078,axiom,
    ! [Y,Xs] :
      ( bunique(cons3(Y,Xs))
    <=> ( ~ belem2(Y,Xs)
        & bunique(Xs) ) ) ).

tff(axiom_079,axiom,
    ! [Y] : ( append(nil2,Y) = Y ) ).

tff(axiom_080,axiom,
    ! [Y,Z,Xs] : ( append(cons2(Z,Xs),Y) = cons2(Z,append(Xs,Y)) ) ).

tff(axiom_081,axiom,
    ! [Y] : ( add(zero,Y) = Y ) ).

tff(axiom_082,axiom,
    ! [Y,Z] : ( add(suc(Z),Y) = suc(add(Z,Y)) ) ).

tff(axiom_083,axiom,
    btour(nil3,nil2) ).

tff(axiom_084,axiom,
    ! [Z,X2] : ~ btour(nil3,cons2(Z,X2)) ).

tff(axiom_085,axiom,
    ! [X3,X4] : ~ btour(cons3(X3,X4),nil2) ).

tff(axiom_086,axiom,
    ! [X3,X4,Vs,U,V] :
      ( btour(cons3(X3,X4),cons2(pair23(U,V),Vs))
    <=> ( beq(X3,last(X3,X4))
        & bpath2(cons3(X3,X4),bgraph(cons2(pair23(U,V),Vs)))
        & bunique(X4)
        & ( len(cons3(X3,X4)) = add(two,maximum(maxNat(U,V),Vs)) ) ) ) ).

tff(axiom_087,axiom,
    ! [X] : ( dodeca2(X,nil4) = nil2 ) ).

tff(axiom_088,axiom,
    ! [X,Z,X2] : ( dodeca2(X,cons4(Z,X2)) = cons2(pair23(Z,add(suc(X),Z)),dodeca2(X,X2)) ) ).

tff(axiom_089,axiom,
    ! [X] : ( dodeca3(X,nil4) = nil2 ) ).

tff(axiom_090,axiom,
    ! [X,Z,X2] : ( dodeca3(X,cons4(Z,X2)) = cons2(pair23(add(suc(X),Z),add(add(suc(X),suc(X)),Z)),dodeca3(X,X2)) ) ).

tff(axiom_091,axiom,
    ! [X] : ( dodeca4(X,nil4) = nil2 ) ).

tff(axiom_092,axiom,
    ! [X,Z,X2] : ( dodeca4(X,cons4(Z,X2)) = cons2(pair23(add(suc(X),suc(Z)),add(add(suc(X),suc(X)),Z)),dodeca4(X,X2)) ) ).

tff(axiom_093,axiom,
    ! [X] : ( dodeca5(X,nil4) = nil2 ) ).

tff(axiom_094,axiom,
    ! [X,Z,X2] : ( dodeca5(X,cons4(Z,X2)) = cons2(pair23(add(add(suc(X),suc(X)),Z),add(add(add(suc(X),suc(X)),suc(X)),Z)),dodeca5(X,X2)) ) ).

tff(axiom_095,axiom,
    ! [X] : ( dodeca6(X,nil4) = nil2 ) ).

tff(axiom_096,axiom,
    ! [X,Z,X2] : ( dodeca6(X,cons4(Z,X2)) = cons2(pair23(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_097,axiom,
    dodeca7(zero) = nil2 ).

tff(axiom_098,axiom,
    ! [Y] : ( dodeca7(suc(Y)) = append(cons2(pair23(Y,zero),dodeca(enumFromToNat(zero,Y))),append(dodeca2(Y,enumFromToNat(zero,suc(Y))),append(dodeca3(Y,enumFromToNat(zero,suc(Y))),append(cons2(pair23(suc(Y),add(add(suc(Y),suc(Y)),Y)),dodeca4(Y,enumFromToNat(zero,Y))),append(dodeca5(Y,enumFromToNat(zero,suc(Y))),cons2(pair23(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_099,conjecture,
    ? [P] : btour(P,dodeca7(three)) ).

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