TPTP Problem File: SWX218-1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX218-1 : TPTP v9.3.0. Released v9.3.0.
% Domain : Software Verification
% Problem : Find a Turing machine with specified behavior (with extra help)
% Version : Especial.
% English :
% Refs : [CST26] Claessen et al. (2026), Email to Geoff Sutcliffe
% Source : [CST26]
% Names : Turing_prop_help.p [CST26]
% Status : Unsatisfiable
% Rating : 1.00 v9.3.0
% Syntax : Number of clauses : 77 ( 75 unt; 0 nHn; 12 RR)
% Number of literals : 79 ( 79 equ; 3 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% Number of functors : 44 ( 44 usr; 11 con; 0-6 aty)
% Number of variables : 149 ( 74 sgn)
% SPC : CNF_UNS_RFO_PEQ_NUE
% Comments :
%------------------------------------------------------------------------------
cnf(axiom,axiom,
aux(Y,Q,Sa,Rhs,btrue) = Rhs ).
cnf(axiom_001,axiom,
aux(Y,Q,Sa,Rhs,bfalse) = apply(Q,Y) ).
cnf(axiom_002,axiom,
aux2(Y,Z,X2,S,pair23(Y1,Lft1)) = right(tuple2(S,Lft1,cons2(Y1,cons2(Z,X2)))) ).
cnf(axiom_003,axiom,
aux3(X,S,Lft,X1,Rgt,pair24(X12,What1)) = act(What1,Lft,X12,Rgt) ).
cnf(axiom_004,axiom,
aux4(X,S,Lft,Rgt,pair23(X1,Rgt2)) = aux3(X,S,Lft,X1,Rgt2,apply(X,pair22(S,X1))) ).
cnf(axiom_005,axiom,
aux5(X,Y,left(Tape)) = Tape ).
cnf(axiom_006,axiom,
aux5(X,Y,right(St)) = steps(X,St) ).
cnf(axiom_007,axiom,
aux6(X,nil2) = bfalse ).
cnf(axiom_008,axiom,
aux6(X,cons2(a2,nil2)) = bfalse ).
cnf(axiom_009,axiom,
aux6(X,cons2(a2,cons2(a2,nil2))) = bfalse ).
cnf(axiom_010,axiom,
aux6(X,cons2(a2,cons2(a2,cons2(a2,nil2)))) = bfalse ).
cnf(axiom_011,axiom,
aux6(X,cons2(a2,cons2(a2,cons2(a2,cons2(a2,nil2))))) = bfalse ).
cnf(axiom_012,axiom,
aux6(X,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))) = bfalse ).
cnf(axiom_013,axiom,
aux6(X,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(b,nil2))))))) = btrue ).
cnf(axiom_014,axiom,
aux6(X,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(b,cons2(X14,X15)))))))) = bfalse ).
cnf(axiom_015,axiom,
aux6(X,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(o,X13))))))) = bfalse ).
cnf(axiom_016,axiom,
aux6(X,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(a2,X13))))))) = bfalse ).
cnf(axiom_017,axiom,
aux6(X,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(o,X11)))))) = bfalse ).
cnf(axiom_018,axiom,
aux6(X,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(a2,X11)))))) = bfalse ).
cnf(axiom_019,axiom,
aux6(X,cons2(a2,cons2(a2,cons2(a2,cons2(o,X9))))) = bfalse ).
cnf(axiom_020,axiom,
aux6(X,cons2(a2,cons2(a2,cons2(a2,cons2(b,X9))))) = bfalse ).
cnf(axiom_021,axiom,
aux6(X,cons2(a2,cons2(a2,cons2(o,X7)))) = bfalse ).
cnf(axiom_022,axiom,
aux6(X,cons2(a2,cons2(a2,cons2(b,X7)))) = bfalse ).
cnf(axiom_023,axiom,
aux6(X,cons2(a2,cons2(o,X5))) = bfalse ).
cnf(axiom_024,axiom,
aux6(X,cons2(a2,cons2(b,X5))) = bfalse ).
cnf(axiom_025,axiom,
aux6(X,cons2(o,X3)) = bfalse ).
cnf(axiom_026,axiom,
aux6(X,cons2(b,X3)) = bfalse ).
cnf(axiom_027,axiom,
aux7(X,nil2) = bfalse ).
cnf(axiom_028,axiom,
aux7(X,cons2(a2,nil2)) = aux6(X,runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))) ).
cnf(axiom_029,axiom,
aux7(X,cons2(a2,cons2(X16,X17))) = bfalse ).
cnf(axiom_030,axiom,
aux7(X,cons2(o,Z)) = bfalse ).
cnf(axiom_031,axiom,
aux7(X,cons2(b,Z)) = bfalse ).
cnf(axiom_032,axiom,
split(nil2) = pair23(o,nil2) ).
cnf(axiom_033,axiom,
split(cons2(Y,Xs)) = pair23(Y,Xs) ).
cnf(axiom_034,axiom,
rev(nil2,Y) = Y ).
cnf(axiom_035,axiom,
rev(cons2(o,Xs),Y) = Y ).
cnf(axiom_036,axiom,
rev(cons2(a2,Xs),Y) = rev(Xs,cons2(a2,Y)) ).
cnf(axiom_037,axiom,
rev(cons2(b,Xs),Y) = rev(Xs,cons2(b,Y)) ).
cnf(axiom_038,axiom,
one = succ(zero) ).
cnf(axiom_039,axiom,
two = succ(one) ).
cnf(axiom_040,axiom,
apply(nil,Y) = pair24(o,stp) ).
cnf(axiom_041,axiom,
apply(cons(pair2(Sa,Rhs),Q),Y) = aux(Y,Q,Sa,Rhs,eq(Sa,Y)) ).
cnf(axiom_042,axiom,
act(lft(S),Y,Z,X2) = aux2(Y,Z,X2,S,split(Y)) ).
cnf(axiom_043,axiom,
act(rgt(T),Y,Z,X2) = right(tuple2(T,cons2(Z,Y),X2)) ).
cnf(axiom_044,axiom,
act(stp,Y,Z,X2) = left(rev(Y,cons2(Z,X2))) ).
cnf(axiom_045,axiom,
step(X,tuple2(S,Lft,Rgt)) = aux4(X,S,Lft,Rgt,split(Rgt)) ).
cnf(axiom_046,axiom,
steps(X,Y) = aux5(X,Y,step(X,Y)) ).
cnf(axiom_047,axiom,
runt(X,Y) = steps(X,tuple2(zero,nil2,Y)) ).
cnf(axiom_048,axiom,
prog0(X) = aux7(X,runt(X,cons2(a2,nil2))) ).
cnf(axiom_049,axiom,
prop_help(X,Y,Z,X2,X3) = eq3(prog0(cons(pair2(pair22(zero,a2),X),cons(pair2(pair22(zero,b),Y),cons(pair2(pair22(one,a2),Z),cons(pair2(pair22(one,b),X2),cons(pair2(pair22(two,a2),X3),nil)))))),bfalse) ).
cnf(axiom_050,axiom,
eq3(bfalse,btrue) = bfalse ).
cnf(axiom_051,axiom,
eq3(btrue,bfalse) = bfalse ).
cnf(axiom_052,axiom,
eq5(o,a2) = bfalse ).
cnf(axiom_053,axiom,
eq5(o,b) = bfalse ).
cnf(axiom_054,axiom,
eq5(a2,o) = bfalse ).
cnf(axiom_055,axiom,
eq5(a2,b) = bfalse ).
cnf(axiom_056,axiom,
eq5(b,o) = bfalse ).
cnf(axiom_057,axiom,
eq5(b,a2) = bfalse ).
cnf(axiom_058,axiom,
eq2(succ(X),succ(Y)) = eq2(X,Y) ).
cnf(axiom_059,axiom,
eq2(zero,succ(X)) = bfalse ).
cnf(axiom_060,axiom,
eq2(succ(X),zero) = bfalse ).
cnf(axiom_061,axiom,
eq4(lft(X),lft(Y)) = eq2(X,Y) ).
cnf(axiom_062,axiom,
eq4(rgt(X),rgt(Y)) = eq2(X,Y) ).
cnf(axiom_063,axiom,
eq4(lft(X),rgt(Y)) = bfalse ).
cnf(axiom_064,axiom,
eq4(lft(X),stp) = bfalse ).
cnf(axiom_065,axiom,
eq4(rgt(X),lft(Y)) = bfalse ).
cnf(axiom_066,axiom,
eq4(rgt(X),stp) = bfalse ).
cnf(axiom_067,axiom,
eq4(stp,lft(X)) = bfalse ).
cnf(axiom_068,axiom,
eq4(stp,rgt(X)) = bfalse ).
cnf(axiom_069,axiom,
eq(X,X) = btrue ).
cnf(axiom_070,axiom,
eq2(X,X) = btrue ).
cnf(axiom_071,axiom,
eq3(X,X) = btrue ).
cnf(axiom_072,axiom,
eq4(X,X) = btrue ).
cnf(axiom_073,axiom,
eq5(X,X) = btrue ).
cnf(axiom_074,axiom,
( eq2(X,Z) != bfalse
| eq(pair22(X,Y),pair22(Z,X2)) = bfalse ) ).
cnf(axiom_075,axiom,
( eq2(X,Z) != btrue
| eq(pair22(X,Y),pair22(Z,X2)) = eq5(Y,X2) ) ).
cnf(goal,negated_conjecture,
eq3(prop_help(X,Y,Z,X2,X3),bfalse) != btrue ).
%------------------------------------------------------------------------------