%------------------------------------------------------------------------------
% 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   : Unsatisfiable
% Rating   : 1.00 v9.3.0
% Syntax   : Number of clauses     :   93 (  93 unt;   0 nHn;  25 RR)
%            Number of literals    :   93 (  93 equ;   1 neg)
%            Maximal clause size   :    1 (   1 avg)
%            Maximal term depth    :   12 (   2 avg)
%            Number of predicates  :    1 (   0 usr;   0 prp; 2-2 aty)
%            Number of functors    :   61 (  61 usr;  14 con; 0-3 aty)
%            Number of variables   :  124 (  36 sgn)
% SPC      : CNF_UNS_RFO_PEQ_UEQ

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

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

cnf(axiom_002,axiom,
    aux2(X,Y,btrue) = nil4 ).

cnf(axiom_003,axiom,
    aux2(X,Y,bfalse) = cons4(X,enumFromToNat(suc(X),Y)) ).

cnf(axiom_004,axiom,
    aux3(Y,btrue) = cons6(o,bin(halfNat(suc(Y)))) ).

cnf(axiom_005,axiom,
    aux3(Y,bfalse) = cons6(i,bin(halfNat(suc(Y)))) ).

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

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

cnf(axiom_008,axiom,
    orb(btrue,Q) = btrue ).

cnf(axiom_009,axiom,
    orb(bfalse,Q) = Q ).

cnf(axiom_010,axiom,
    or2(nil5) = bfalse ).

cnf(axiom_011,axiom,
    or2(cons5(Y,Xs)) = orb(Y,or2(Xs)) ).

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

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

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

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

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

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

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

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

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

cnf(axiom_021,axiom,
    maxNat(X,Y) = aux(X,Y,lt(X,Y)) ).

cnf(axiom_022,axiom,
    maximum(X,nil2) = X ).

cnf(axiom_023,axiom,
    maximum(X,cons2(pair22(Y2,Z2),Yzs)) = maximum(maxNat(X,maxNat(Y2,Z2)),Yzs) ).

cnf(axiom_024,axiom,
    len(nil3) = zero ).

cnf(axiom_025,axiom,
    len(cons3(Y,Xs)) = suc(len(Xs)) ).

cnf(axiom_026,axiom,
    last(X,nil3) = X ).

cnf(axiom_027,axiom,
    last(X,cons3(Z,Ys)) = last(Z,Ys) ).

cnf(axiom_028,axiom,
    halfNat(zero) = zero ).

cnf(axiom_029,axiom,
    halfNat(suc(zero)) = zero ).

cnf(axiom_030,axiom,
    halfNat(suc(suc(N))) = suc(halfNat(N)) ).

cnf(axiom_031,axiom,
    evenNat(zero) = btrue ).

cnf(axiom_032,axiom,
    evenNat(suc(zero)) = bfalse ).

cnf(axiom_033,axiom,
    evenNat(suc(suc(N))) = evenNat(N) ).

cnf(axiom_034,axiom,
    enumFromToNat(X,Y) = aux2(X,Y,lt(Y,X)) ).

cnf(axiom_035,axiom,
    dodeca(nil4) = nil2 ).

cnf(axiom_036,axiom,
    dodeca(cons4(Y,Z)) = cons2(pair22(Y,suc(Y)),dodeca(Z)) ).

cnf(axiom_037,axiom,
    bin(zero) = nil6 ).

cnf(axiom_038,axiom,
    bin(suc(Y)) = aux3(Y,evenNat(suc(Y))) ).

cnf(axiom_039,axiom,
    bgraph(nil2) = nil ).

cnf(axiom_040,axiom,
    bgraph(cons2(pair22(U,V),Z)) = cons(pair2(bin(U),bin(V)),bgraph(Z)) ).

cnf(axiom_041,axiom,
    beq(nil6,nil6) = btrue ).

cnf(axiom_042,axiom,
    beq(nil6,cons6(Z,X2)) = bfalse ).

cnf(axiom_043,axiom,
    beq(cons6(i,Xs),nil6) = bfalse ).

cnf(axiom_044,axiom,
    beq(cons6(i,Xs),cons6(i,Ys)) = beq(Xs,Ys) ).

cnf(axiom_045,axiom,
    beq(cons6(i,Xs),cons6(o,Ys)) = bfalse ).

cnf(axiom_046,axiom,
    beq(cons6(o,Xs),nil6) = bfalse ).

cnf(axiom_047,axiom,
    beq(cons6(o,Xs),cons6(i,Zs)) = bfalse ).

cnf(axiom_048,axiom,
    beq(cons6(o,Xs),cons6(o,Zs)) = beq(Xs,Zs) ).

cnf(axiom_049,axiom,
    belem(X,nil3) = nil5 ).

cnf(axiom_050,axiom,
    belem(X,cons3(Z,X2)) = cons5(beq(X,Z),belem(X,X2)) ).

cnf(axiom_051,axiom,
    belem2(X,Y) = or2(belem(X,Y)) ).

cnf(axiom_052,axiom,
    append(nil2,Y) = Y ).

cnf(axiom_053,axiom,
    append(cons2(Z,Xs),Y) = cons2(Z,append(Xs,Y)) ).

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

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

cnf(axiom_056,axiom,
    bpath(X,Y,nil) = nil5 ).

cnf(axiom_057,axiom,
    bpath(X,Y,cons(pair2(U,V),X3)) = cons5(orb(andb(beq(U,X),beq(V,Y)),andb(beq(U,Y),beq(V,X))),bpath(X,Y,X3)) ).

cnf(axiom_058,axiom,
    bpath2(nil3,Y) = btrue ).

cnf(axiom_059,axiom,
    bpath2(cons3(Z,nil3),Y) = btrue ).

cnf(axiom_060,axiom,
    bpath2(cons3(Z,cons3(Y2,Xs)),Y) = andb(or2(bpath(Z,Y2,Y)),bpath2(cons3(Y2,Xs),Y)) ).

cnf(axiom_061,axiom,
    bunique(nil3) = btrue ).

cnf(axiom_062,axiom,
    bunique(cons3(Y,Xs)) = andb(notb(belem2(Y,Xs)),bunique(Xs)) ).

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

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

cnf(axiom_065,axiom,
    btour(nil3,nil2) = btrue ).

cnf(axiom_066,axiom,
    btour(nil3,cons2(Z,X2)) = bfalse ).

cnf(axiom_067,axiom,
    btour(cons3(X3,X4),nil2) = bfalse ).

cnf(axiom_068,axiom,
    btour(cons3(X3,X4),cons2(pair22(U,V),Vs)) = andb(beq(X3,last(X3,X4)),andb(bpath2(cons3(X3,X4),bgraph(cons2(pair22(U,V),Vs))),andb(bunique(X4),eq(len(cons3(X3,X4)),add(two,maximum(maxNat(U,V),Vs)))))) ).

cnf(axiom_069,axiom,
    dodeca2(X,nil4) = nil2 ).

cnf(axiom_070,axiom,
    dodeca2(X,cons4(Z,X2)) = cons2(pair22(Z,add(suc(X),Z)),dodeca2(X,X2)) ).

cnf(axiom_071,axiom,
    dodeca3(X,nil4) = nil2 ).

cnf(axiom_072,axiom,
    dodeca3(X,cons4(Z,X2)) = cons2(pair22(add(suc(X),Z),add(add(suc(X),suc(X)),Z)),dodeca3(X,X2)) ).

cnf(axiom_073,axiom,
    dodeca4(X,nil4) = nil2 ).

cnf(axiom_074,axiom,
    dodeca4(X,cons4(Z,X2)) = cons2(pair22(add(suc(X),suc(Z)),add(add(suc(X),suc(X)),Z)),dodeca4(X,X2)) ).

cnf(axiom_075,axiom,
    dodeca5(X,nil4) = nil2 ).

cnf(axiom_076,axiom,
    dodeca5(X,cons4(Z,X2)) = cons2(pair22(add(add(suc(X),suc(X)),Z),add(add(add(suc(X),suc(X)),suc(X)),Z)),dodeca5(X,X2)) ).

cnf(axiom_077,axiom,
    dodeca6(X,nil4) = nil2 ).

cnf(axiom_078,axiom,
    dodeca6(X,cons4(Z,X2)) = cons2(pair22(add(add(add(suc(X),suc(X)),suc(X)),Z),add(add(add(suc(X),suc(X)),suc(X)),suc(Z))),dodeca6(X,X2)) ).

cnf(axiom_079,axiom,
    dodeca7(zero) = nil2 ).

cnf(axiom_080,axiom,
    dodeca7(suc(Y)) = append(cons2(pair22(Y,zero),dodeca(enumFromToNat(zero,Y))),append(dodeca2(Y,enumFromToNat(zero,suc(Y))),append(dodeca3(Y,enumFromToNat(zero,suc(Y))),append(cons2(pair22(suc(Y),add(add(suc(Y),suc(Y)),Y)),dodeca4(Y,enumFromToNat(zero,Y))),append(dodeca5(Y,enumFromToNat(zero,suc(Y))),cons2(pair22(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)))))))) ).

cnf(axiom_081,axiom,
    prop_bt3(X) = notb(btour(X,dodeca7(three))) ).

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

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

cnf(axiom_084,axiom,
    eq3(i,o) = bfalse ).

cnf(axiom_085,axiom,
    eq3(o,i) = bfalse ).

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

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

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

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

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

cnf(axiom_091,axiom,
    eq3(X,X) = btrue ).

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

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