TPTP Problem File: SWX225-1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX225-1 : TPTP v9.3.0. Released v9.3.0.
% Domain : Software Verification
% Problem : Find an untyped lambda term with a specific property
% Version : Especial.
% English :
% Refs : [CST26] Claessen et al. (2026), Email to Geoff Sutcliffe
% Source : [CST26]
% Names : Untyped_thm1.p [CST26]
% Status : Unsatisfiable
% Rating : 1.00 v9.3.0
% Syntax : Number of clauses : 90 ( 88 unt; 0 nHn; 39 RR)
% Number of literals : 92 ( 92 equ; 3 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% Number of functors : 22 ( 22 usr; 10 con; 0-4 aty)
% Number of variables : 103 ( 39 sgn)
% SPC : CNF_UNS_RFO_PEQ_NUE
% Comments :
%------------------------------------------------------------------------------
cnf(axiom,axiom,
fail(Y,Z) = par(Y,Z,step(Y),step(Z)) ).
cnf(axiom_001,axiom,
par(X,Y,nothing,nothing) = nothing ).
cnf(axiom_002,axiom,
par(X,Y,nothing,just(U_red)) = just(x(X,U_red)) ).
cnf(axiom_003,axiom,
par(X,Y,just(T_red),nothing) = just(x(T_red,Y)) ).
cnf(axiom_004,axiom,
par(X,Y,just(T_red),just(U_red2)) = just(x(T_red,U_red2)) ).
cnf(axiom_005,axiom,
step(x(x(x(s,F),G),Z)) = just(x(x(F,Z),x(G,Z))) ).
cnf(axiom_006,axiom,
step(x(x(x(b,F),G),Z)) = just(x(F,x(G,Z))) ).
cnf(axiom_007,axiom,
step(x(x(x(c,F),G),Z)) = just(x(x(F,Z),G)) ).
cnf(axiom_008,axiom,
step(x(x(x(x(X,X2),F),G),Z)) = fail(x(x(x(X,X2),F),G),Z) ).
cnf(axiom_009,axiom,
step(x(x(x(theVar,F),G),Z)) = fail(x(x(theVar,F),G),Z) ).
cnf(axiom_010,axiom,
step(x(x(x(k,F),G),Z)) = fail(x(x(k,F),G),Z) ).
cnf(axiom_011,axiom,
step(x(x(x(i,F),G),Z)) = fail(x(x(i,F),G),Z) ).
cnf(axiom_012,axiom,
step(x(x(k,G),Z)) = just(G) ).
cnf(axiom_013,axiom,
step(x(x(theVar,G),Z)) = fail(x(theVar,G),Z) ).
cnf(axiom_014,axiom,
step(x(x(i,G),Z)) = fail(x(i,G),Z) ).
cnf(axiom_015,axiom,
step(x(x(s,G),Z)) = fail(x(s,G),Z) ).
cnf(axiom_016,axiom,
step(x(x(b,G),Z)) = fail(x(b,G),Z) ).
cnf(axiom_017,axiom,
step(x(x(c,G),Z)) = fail(x(c,G),Z) ).
cnf(axiom_018,axiom,
step(x(i,Z)) = just(Z) ).
cnf(axiom_019,axiom,
step(x(theVar,Z)) = fail(theVar,Z) ).
cnf(axiom_020,axiom,
step(x(k,Z)) = fail(k,Z) ).
cnf(axiom_021,axiom,
step(x(s,Z)) = fail(s,Z) ).
cnf(axiom_022,axiom,
step(x(b,Z)) = fail(b,Z) ).
cnf(axiom_023,axiom,
step(x(c,Z)) = fail(c,Z) ).
cnf(axiom_024,axiom,
step(theVar) = nothing ).
cnf(axiom_025,axiom,
step(k) = nothing ).
cnf(axiom_026,axiom,
step(i) = nothing ).
cnf(axiom_027,axiom,
step(s) = nothing ).
cnf(axiom_028,axiom,
step(b) = nothing ).
cnf(axiom_029,axiom,
step(c) = nothing ).
cnf(axiom_030,axiom,
impl(btrue,Q) = Q ).
cnf(axiom_031,axiom,
impl(bfalse,Q) = btrue ).
cnf(axiom_032,axiom,
thm1(X) = impl(eq3(step(X),just(X)),eq4(btrue,bfalse)) ).
cnf(axiom_033,axiom,
eq(theVar,k) = bfalse ).
cnf(axiom_034,axiom,
eq(theVar,i) = bfalse ).
cnf(axiom_035,axiom,
eq(theVar,s) = bfalse ).
cnf(axiom_036,axiom,
eq(theVar,b) = bfalse ).
cnf(axiom_037,axiom,
eq(theVar,c) = bfalse ).
cnf(axiom_038,axiom,
eq(k,theVar) = bfalse ).
cnf(axiom_039,axiom,
eq(k,i) = bfalse ).
cnf(axiom_040,axiom,
eq(k,s) = bfalse ).
cnf(axiom_041,axiom,
eq(k,b) = bfalse ).
cnf(axiom_042,axiom,
eq(k,c) = bfalse ).
cnf(axiom_043,axiom,
eq(i,theVar) = bfalse ).
cnf(axiom_044,axiom,
eq(i,k) = bfalse ).
cnf(axiom_045,axiom,
eq(i,s) = bfalse ).
cnf(axiom_046,axiom,
eq(i,b) = bfalse ).
cnf(axiom_047,axiom,
eq(i,c) = bfalse ).
cnf(axiom_048,axiom,
eq(s,theVar) = bfalse ).
cnf(axiom_049,axiom,
eq(s,k) = bfalse ).
cnf(axiom_050,axiom,
eq(s,i) = bfalse ).
cnf(axiom_051,axiom,
eq(s,b) = bfalse ).
cnf(axiom_052,axiom,
eq(s,c) = bfalse ).
cnf(axiom_053,axiom,
eq(b,theVar) = bfalse ).
cnf(axiom_054,axiom,
eq(b,k) = bfalse ).
cnf(axiom_055,axiom,
eq(b,i) = bfalse ).
cnf(axiom_056,axiom,
eq(b,s) = bfalse ).
cnf(axiom_057,axiom,
eq(b,c) = bfalse ).
cnf(axiom_058,axiom,
eq(c,theVar) = bfalse ).
cnf(axiom_059,axiom,
eq(c,k) = bfalse ).
cnf(axiom_060,axiom,
eq(c,i) = bfalse ).
cnf(axiom_061,axiom,
eq(c,s) = bfalse ).
cnf(axiom_062,axiom,
eq(c,b) = bfalse ).
cnf(axiom_063,axiom,
eq4(bfalse,btrue) = bfalse ).
cnf(axiom_064,axiom,
eq4(btrue,bfalse) = bfalse ).
cnf(axiom_065,axiom,
( eq(X,Z) != bfalse
| eq(x(X,Y),x(Z,X2)) = bfalse ) ).
cnf(axiom_066,axiom,
( eq(X,Z) != btrue
| eq(x(X,Y),x(Z,X2)) = eq(Y,X2) ) ).
cnf(axiom_067,axiom,
eq(x(X,Y),theVar) = bfalse ).
cnf(axiom_068,axiom,
eq(x(X,Y),k) = bfalse ).
cnf(axiom_069,axiom,
eq(x(X,Y),i) = bfalse ).
cnf(axiom_070,axiom,
eq(x(X,Y),s) = bfalse ).
cnf(axiom_071,axiom,
eq(x(X,Y),b) = bfalse ).
cnf(axiom_072,axiom,
eq(x(X,Y),c) = bfalse ).
cnf(axiom_073,axiom,
eq(theVar,x(X,Y)) = bfalse ).
cnf(axiom_074,axiom,
eq(k,x(X,Y)) = bfalse ).
cnf(axiom_075,axiom,
eq(i,x(X,Y)) = bfalse ).
cnf(axiom_076,axiom,
eq(s,x(X,Y)) = bfalse ).
cnf(axiom_077,axiom,
eq(b,x(X,Y)) = bfalse ).
cnf(axiom_078,axiom,
eq(c,x(X,Y)) = bfalse ).
cnf(axiom_079,axiom,
eq2(suc(X),suc(Y)) = eq2(X,Y) ).
cnf(axiom_080,axiom,
eq2(suc(X),z) = bfalse ).
cnf(axiom_081,axiom,
eq2(z,suc(X)) = bfalse ).
cnf(axiom_082,axiom,
eq(X,X) = btrue ).
cnf(axiom_083,axiom,
eq2(X,X) = btrue ).
cnf(axiom_084,axiom,
eq3(X,X) = btrue ).
cnf(axiom_085,axiom,
eq4(X,X) = btrue ).
cnf(axiom_086,axiom,
eq3(just(X),just(Y)) = eq(X,Y) ).
cnf(axiom_087,axiom,
eq3(nothing,just(X)) = bfalse ).
cnf(axiom_088,axiom,
eq3(just(X),nothing) = bfalse ).
cnf(goal,negated_conjecture,
eq4(thm1(X),bfalse) != btrue ).
%------------------------------------------------------------------------------