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 : Theorem
% Rating : 1.00 v9.3.0
% Syntax : Number of formulae : 65 ( 41 unt; 0 def)
% Number of atoms : 111 ( 93 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 81 ( 35 ~; 0 |; 0 &)
% ( 0 <=>; 46 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 0 prp; 1-2 aty)
% Number of functors : 48 ( 48 usr; 9 con; 0-4 aty)
% Number of variables : 135 ( 130 !; 5 ?)
% SPC : FOF_THM_RFO_SEQ
% Comments :
%------------------------------------------------------------------------------
fof(axiom_001,axiom,
! [X,X2,X3] : proj1tuple(tuple2(X,X2,X3)) = X ).
fof(axiom_002,axiom,
! [X,X2,X3] : proj2tuple(tuple2(X,X2,X3)) = X2 ).
fof(axiom_003,axiom,
! [X,X2,X3] : proj3tuple(tuple2(X,X2,X3)) = X3 ).
fof(axiom_004,axiom,
! [X,X2] : proj1pair(pair22(X,X2)) = X ).
fof(axiom_005,axiom,
! [X,X2] : proj2pair(pair22(X,X2)) = X2 ).
fof(axiom_006,axiom,
! [X,X2] : proj1pair2(pair23(X,X2)) = X ).
fof(axiom_007,axiom,
! [X,X2] : proj2pair2(pair23(X,X2)) = X2 ).
fof(axiom_008,axiom,
! [X,X2] : proj1pair3(pair24(X,X2)) = X ).
fof(axiom_009,axiom,
! [X,X2] : proj2pair3(pair24(X,X2)) = X2 ).
fof(axiom_010,axiom,
! [X,X2] : proj1pair4(pair25(X,X2)) = X ).
fof(axiom_011,axiom,
! [X,X2] : proj2pair4(pair25(X,X2)) = X2 ).
fof(axiom_012,axiom,
! [X,X2] : head(cons(X,X2)) = X ).
fof(axiom_013,axiom,
! [X,X2] : tail(cons(X,X2)) = X2 ).
fof(axiom_014,axiom,
! [X,X2] : nil != cons(X,X2) ).
fof(axiom_015,axiom,
! [X,X2] : head2(cons2(X,X2)) = X ).
fof(axiom_016,axiom,
! [X,X2] : tail2(cons2(X,X2)) = X2 ).
fof(axiom_017,axiom,
! [X,X2] : nil2 != cons2(X,X2) ).
fof(axiom_018,axiom,
! [X] : proj1Succ(succ(X)) = X ).
fof(axiom_019,axiom,
! [X] : zero != succ(X) ).
fof(axiom_020,axiom,
! [X] : proj1Left(left(X)) = X ).
fof(axiom_021,axiom,
! [X] : proj1Right(right(X)) = X ).
fof(axiom_022,axiom,
! [X,X2] : left(X) != right(X2) ).
fof(axiom_023,axiom,
! [X] : proj1Lft(lft(X)) = X ).
fof(axiom_024,axiom,
! [X] : proj1Rgt(rgt(X)) = X ).
fof(axiom_025,axiom,
! [X,X2] : lft(X) != rgt(X2) ).
fof(axiom_026,axiom,
! [X] : lft(X) != stp ).
fof(axiom_027,axiom,
! [X] : rgt(X) != stp ).
fof(axiom_028,axiom,
o != a2 ).
fof(axiom_029,axiom,
o != b ).
fof(axiom_030,axiom,
a2 != b ).
fof(axiom_031,axiom,
split(nil2) = pair24(o,nil2) ).
fof(axiom_032,axiom,
! [Y,Xs] : split(cons2(Y,Xs)) = pair24(Y,Xs) ).
fof(axiom_033,axiom,
! [Y] : rev(nil2,Y) = Y ).
fof(axiom_034,axiom,
! [Y,Z,Xs] :
( Z != o
=> rev(cons2(Z,Xs),Y) = rev(Xs,cons2(Z,Y)) ) ).
fof(axiom_035,axiom,
! [Y,Xs] : rev(cons2(o,Xs),Y) = Y ).
fof(axiom_036,axiom,
one = succ(zero) ).
fof(axiom_037,axiom,
two = succ(one) ).
fof(axiom_038,axiom,
! [Y] : apply(nil,Y) = pair25(o,stp) ).
fof(axiom_039,axiom,
! [Y,Q,Sa,Rhs] :
( Sa = Y
=> apply(cons(pair22(Sa,Rhs),Q),Y) = Rhs ) ).
fof(axiom_040,axiom,
! [Y,Q,Sa,Rhs] :
( Sa != Y
=> apply(cons(pair22(Sa,Rhs),Q),Y) = apply(Q,Y) ) ).
fof(axiom_041,axiom,
! [Y,Z,X2,S,Y1,Lft1] :
( split(Y) = pair24(Y1,Lft1)
=> act(lft(S),Y,Z,X2) = right(tuple2(S,Lft1,cons2(Y1,cons2(Z,X2)))) ) ).
fof(axiom_042,axiom,
! [Y,Z,X2,T] : act(rgt(T),Y,Z,X2) = right(tuple2(T,cons2(Z,Y),X2)) ).
fof(axiom_043,axiom,
! [Y,Z,X2] : act(stp,Y,Z,X2) = left(rev(Y,cons2(Z,X2))) ).
fof(axiom_044,axiom,
! [X,S,Lft,Rgt,X1,Rgt2,X12,What1] :
( split(Rgt) = pair24(X1,Rgt2)
=> ( apply(X,pair23(S,X1)) = pair25(X12,What1)
=> step(X,tuple2(S,Lft,Rgt)) = act(What1,Lft,X12,Rgt2) ) ) ).
fof(axiom_045,axiom,
! [X,Y,Tape] :
( step(X,Y) = left(Tape)
=> steps(X,Y) = Tape ) ).
fof(axiom_046,axiom,
! [X,Y,St] :
( step(X,Y) = right(St)
=> steps(X,Y) = steps(X,St) ) ).
fof(axiom_047,axiom,
! [X,Y] : runt(X,Y) = steps(X,tuple2(zero,nil2,Y)) ).
fof(axiom_048,axiom,
! [X] :
( runt(X,cons2(a2,nil2)) = nil2
=> ~ prog0(X) ) ).
fof(axiom_049,axiom,
! [X,Y,Z] :
( runt(X,cons2(a2,nil2)) = cons2(Y,Z)
=> ( Y != a2
=> ~ prog0(X) ) ) ).
fof(axiom_050,axiom,
! [X] :
( runt(X,cons2(a2,nil2)) = cons2(a2,nil2)
=> ( runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = nil2
=> ~ prog0(X) ) ) ).
fof(axiom_051,axiom,
! [X,X2,X3] :
( runt(X,cons2(a2,nil2)) = cons2(a2,nil2)
=> ( runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(X2,X3)
=> ( X2 != a2
=> ~ prog0(X) ) ) ) ).
fof(axiom_052,axiom,
! [X] :
( runt(X,cons2(a2,nil2)) = cons2(a2,nil2)
=> ( runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,nil2)
=> ~ prog0(X) ) ) ).
fof(axiom_053,axiom,
! [X,X4,X5] :
( runt(X,cons2(a2,nil2)) = cons2(a2,nil2)
=> ( runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(X4,X5))
=> ( X4 != a2
=> ~ prog0(X) ) ) ) ).
fof(axiom_054,axiom,
! [X] :
( runt(X,cons2(a2,nil2)) = cons2(a2,nil2)
=> ( runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(a2,nil2))
=> ~ prog0(X) ) ) ).
fof(axiom_055,axiom,
! [X,X6,X7] :
( runt(X,cons2(a2,nil2)) = cons2(a2,nil2)
=> ( runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(a2,cons2(X6,X7)))
=> ( X6 != a2
=> ~ prog0(X) ) ) ) ).
fof(axiom_056,axiom,
! [X] :
( runt(X,cons2(a2,nil2)) = cons2(a2,nil2)
=> ( runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(a2,cons2(a2,nil2)))
=> ~ prog0(X) ) ) ).
fof(axiom_057,axiom,
! [X,X8,X9] :
( runt(X,cons2(a2,nil2)) = cons2(a2,nil2)
=> ( runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(a2,cons2(a2,cons2(X8,X9))))
=> ( X8 != a2
=> ~ prog0(X) ) ) ) ).
fof(axiom_058,axiom,
! [X] :
( runt(X,cons2(a2,nil2)) = cons2(a2,nil2)
=> ( runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(a2,cons2(a2,cons2(a2,nil2))))
=> ~ prog0(X) ) ) ).
fof(axiom_059,axiom,
! [X,X10,X11] :
( runt(X,cons2(a2,nil2)) = cons2(a2,nil2)
=> ( runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(X10,X11)))))
=> ( X10 != b
=> ~ prog0(X) ) ) ) ).
fof(axiom_060,axiom,
! [X] :
( runt(X,cons2(a2,nil2)) = cons2(a2,nil2)
=> ( runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))
=> ~ prog0(X) ) ) ).
fof(axiom_061,axiom,
! [X,X12,X13] :
( runt(X,cons2(a2,nil2)) = cons2(a2,nil2)
=> ( runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(X12,X13))))))
=> ( X12 != b
=> ~ prog0(X) ) ) ) ).
fof(axiom_062,axiom,
! [X] :
( runt(X,cons2(a2,nil2)) = cons2(a2,nil2)
=> ( runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(b,nil2))))))
=> prog0(X) ) ) ).
fof(axiom_063,axiom,
! [X,X14,X15] :
( runt(X,cons2(a2,nil2)) = cons2(a2,nil2)
=> ( runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(b,cons2(X14,X15)))))))
=> ~ prog0(X) ) ) ).
fof(axiom_064,axiom,
! [X,X16,X17] :
( runt(X,cons2(a2,nil2)) = cons2(a2,cons2(X16,X17))
=> ~ prog0(X) ) ).
fof(goal_065,conjecture,
? [X,Y,Z,V,W] : prog0(cons(pair22(pair23(zero,a2),X),cons(pair22(pair23(zero,b),Y),cons(pair22(pair23(one,a2),Z),cons(pair22(pair23(one,b),V),cons(pair22(pair23(two,a2),W),nil)))))) ).
%------------------------------------------------------------------------------