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 : Unsatisfiable
% Rating : 1.00 v9.3.0
% Syntax : Number of clauses : 71 ( 71 unt; 0 nHn; 16 RR)
% Number of literals : 71 ( 71 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 : 45 ( 45 usr; 9 con; 0-3 aty)
% Number of variables : 105 ( 31 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) = nil2 ).
cnf(axiom_003,axiom,
aux2(X,Y,bfalse) = cons2(X,enumFromToNat(suc(X),Y)) ).
cnf(axiom_004,axiom,
aux3(Y,Xs,btrue) = bfalse ).
cnf(axiom_005,axiom,
aux3(Y,Xs,bfalse) = unique(Xs) ).
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(nil3) = bfalse ).
cnf(axiom_011,axiom,
or2(cons3(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,nil) = X ).
cnf(axiom_023,axiom,
maximum(X,cons(pair2(Y2,Z2),Yzs)) = maximum(maxNat(X,maxNat(Y2,Z2)),Yzs) ).
cnf(axiom_024,axiom,
len(nil2) = zero ).
cnf(axiom_025,axiom,
len(cons2(Y,Xs)) = suc(len(Xs)) ).
cnf(axiom_026,axiom,
last(X,nil2) = X ).
cnf(axiom_027,axiom,
last(X,cons2(Z,Ys)) = last(Z,Ys) ).
cnf(axiom_028,axiom,
enumFromToNat(X,Y) = aux2(X,Y,lt(Y,X)) ).
cnf(axiom_029,axiom,
elem(X,nil2) = bfalse ).
cnf(axiom_030,axiom,
elem(X,cons2(Z,Xs)) = orb(eq(Z,X),elem(X,Xs)) ).
cnf(axiom_031,axiom,
unique(nil2) = btrue ).
cnf(axiom_032,axiom,
unique(cons2(Y,Xs)) = aux3(Y,Xs,elem(Y,Xs)) ).
cnf(axiom_033,axiom,
dodeca(nil2) = nil ).
cnf(axiom_034,axiom,
dodeca(cons2(Y,Z)) = cons(pair2(Y,suc(Y)),dodeca(Z)) ).
cnf(axiom_035,axiom,
append(nil,Y) = Y ).
cnf(axiom_036,axiom,
append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)) ).
cnf(axiom_037,axiom,
andb(btrue,Q) = Q ).
cnf(axiom_038,axiom,
andb(bfalse,Q) = bfalse ).
cnf(axiom_039,axiom,
path(X,Y,nil) = nil3 ).
cnf(axiom_040,axiom,
path(X,Y,cons(pair2(U,V),X3)) = cons3(orb(andb(eq(U,X),eq(V,Y)),andb(eq(U,Y),eq(V,X))),path(X,Y,X3)) ).
cnf(axiom_041,axiom,
path2(nil2,Y) = btrue ).
cnf(axiom_042,axiom,
path2(cons2(Z,nil2),Y) = btrue ).
cnf(axiom_043,axiom,
path2(cons2(Z,cons2(Y2,Xs)),Y) = andb(or2(path(Z,Y2,Y)),path2(cons2(Y2,Xs),Y)) ).
cnf(axiom_044,axiom,
add(zero,Y) = Y ).
cnf(axiom_045,axiom,
add(suc(Z),Y) = suc(add(Z,Y)) ).
cnf(axiom_046,axiom,
dodeca2(X,nil2) = nil ).
cnf(axiom_047,axiom,
dodeca2(X,cons2(Z,X2)) = cons(pair2(Z,add(suc(X),Z)),dodeca2(X,X2)) ).
cnf(axiom_048,axiom,
dodeca3(X,nil2) = nil ).
cnf(axiom_049,axiom,
dodeca3(X,cons2(Z,X2)) = cons(pair2(add(suc(X),Z),add(add(suc(X),suc(X)),Z)),dodeca3(X,X2)) ).
cnf(axiom_050,axiom,
dodeca4(X,nil2) = nil ).
cnf(axiom_051,axiom,
dodeca4(X,cons2(Z,X2)) = cons(pair2(add(suc(X),suc(Z)),add(add(suc(X),suc(X)),Z)),dodeca4(X,X2)) ).
cnf(axiom_052,axiom,
dodeca5(X,nil2) = nil ).
cnf(axiom_053,axiom,
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)) ).
cnf(axiom_054,axiom,
dodeca6(X,nil2) = nil ).
cnf(axiom_055,axiom,
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)) ).
cnf(axiom_056,axiom,
dodeca7(zero) = nil ).
cnf(axiom_057,axiom,
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)))))))) ).
cnf(axiom_058,axiom,
tour(nil2,nil) = btrue ).
cnf(axiom_059,axiom,
tour(nil2,cons(Z,X2)) = bfalse ).
cnf(axiom_060,axiom,
tour(cons2(X3,X4),nil) = bfalse ).
cnf(axiom_061,axiom,
tour(cons2(X3,X4),cons(pair2(U,V),Vs)) = andb(eq(X3,last(X3,X4)),andb(path2(cons2(X3,X4),cons(pair2(U,V),Vs)),andb(unique(X4),eq(len(cons2(X3,X4)),add(two,maximum(maxNat(U,V),Vs)))))) ).
cnf(axiom_062,axiom,
prop_t3(X) = notb(tour(X,dodeca7(three))) ).
cnf(axiom_063,axiom,
eq2(bfalse,btrue) = bfalse ).
cnf(axiom_064,axiom,
eq2(btrue,bfalse) = bfalse ).
cnf(axiom_065,axiom,
eq(suc(X),suc(Y)) = eq(X,Y) ).
cnf(axiom_066,axiom,
eq(zero,suc(X)) = bfalse ).
cnf(axiom_067,axiom,
eq(suc(X),zero) = bfalse ).
cnf(axiom_068,axiom,
eq(X,X) = btrue ).
cnf(axiom_069,axiom,
eq2(X,X) = btrue ).
cnf(goal,negated_conjecture,
eq2(prop_t3(X),bfalse) != btrue ).
%------------------------------------------------------------------------------