TPTP Problem File: SWX226-1.p

View Solutions - Solve Problem 
%------------------------------------------------------------------------------
% File     : SWX226-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_thm_why.p [CST26]

% Status   : Unsatisfiable
% Rating   : 1.00 v9.3.0
% Syntax   : Number of clauses     :  103 ( 101 unt;   0 nHn;  45 RR)
%            Number of literals    :  105 ( 105 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    :   26 (  26 usr;  10 con; 0-4 aty)
%            Number of variables   :  117 (  44 sgn)
% SPC      : CNF_UNS_RFO_PEQ_NUE

% Comments :
%------------------------------------------------------------------------------
cnf(axiom,axiom,
    aux(Y,N,nothing) = nothing ).

cnf(axiom_001,axiom,
    aux(Y,N,just(U)) = astep(N,U) ).

cnf(axiom_002,axiom,
    fail(Y,Z) = par(Y,Z,step(Y),step(Z)) ).

cnf(axiom_003,axiom,
    par(X,Y,nothing,nothing) = nothing ).

cnf(axiom_004,axiom,
    par(X,Y,nothing,just(U_red)) = just(x(X,U_red)) ).

cnf(axiom_005,axiom,
    par(X,Y,just(T_red),nothing) = just(x(T_red,Y)) ).

cnf(axiom_006,axiom,
    par(X,Y,just(T_red),just(U_red2)) = just(x(T_red,U_red2)) ).

cnf(axiom_007,axiom,
    step(x(x(x(s,F),G),Z)) = just(x(x(F,Z),x(G,Z))) ).

cnf(axiom_008,axiom,
    step(x(x(x(b,F),G),Z)) = just(x(F,x(G,Z))) ).

cnf(axiom_009,axiom,
    step(x(x(x(c,F),G),Z)) = just(x(x(F,Z),G)) ).

cnf(axiom_010,axiom,
    step(x(x(x(x(X,X2),F),G),Z)) = fail(x(x(x(X,X2),F),G),Z) ).

cnf(axiom_011,axiom,
    step(x(x(x(theVar,F),G),Z)) = fail(x(x(theVar,F),G),Z) ).

cnf(axiom_012,axiom,
    step(x(x(x(k,F),G),Z)) = fail(x(x(k,F),G),Z) ).

cnf(axiom_013,axiom,
    step(x(x(x(i,F),G),Z)) = fail(x(x(i,F),G),Z) ).

cnf(axiom_014,axiom,
    step(x(x(k,G),Z)) = just(G) ).

cnf(axiom_015,axiom,
    step(x(x(theVar,G),Z)) = fail(x(theVar,G),Z) ).

cnf(axiom_016,axiom,
    step(x(x(i,G),Z)) = fail(x(i,G),Z) ).

cnf(axiom_017,axiom,
    step(x(x(s,G),Z)) = fail(x(s,G),Z) ).

cnf(axiom_018,axiom,
    step(x(x(b,G),Z)) = fail(x(b,G),Z) ).

cnf(axiom_019,axiom,
    step(x(x(c,G),Z)) = fail(x(c,G),Z) ).

cnf(axiom_020,axiom,
    step(x(i,Z)) = just(Z) ).

cnf(axiom_021,axiom,
    step(x(theVar,Z)) = fail(theVar,Z) ).

cnf(axiom_022,axiom,
    step(x(k,Z)) = fail(k,Z) ).

cnf(axiom_023,axiom,
    step(x(s,Z)) = fail(s,Z) ).

cnf(axiom_024,axiom,
    step(x(b,Z)) = fail(b,Z) ).

cnf(axiom_025,axiom,
    step(x(c,Z)) = fail(c,Z) ).

cnf(axiom_026,axiom,
    step(theVar) = nothing ).

cnf(axiom_027,axiom,
    step(k) = nothing ).

cnf(axiom_028,axiom,
    step(i) = nothing ).

cnf(axiom_029,axiom,
    step(s) = nothing ).

cnf(axiom_030,axiom,
    step(b) = nothing ).

cnf(axiom_031,axiom,
    step(c) = nothing ).

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

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

cnf(axiom_034,axiom,
    impl(btrue,Q) = Q ).

cnf(axiom_035,axiom,
    impl(bfalse,Q) = btrue ).

cnf(axiom_036,axiom,
    cheating(x(A,B)) = orb(cheating(A),cheating(B)) ).

cnf(axiom_037,axiom,
    cheating(theVar) = btrue ).

cnf(axiom_038,axiom,
    cheating(k) = bfalse ).

cnf(axiom_039,axiom,
    cheating(i) = bfalse ).

cnf(axiom_040,axiom,
    cheating(s) = bfalse ).

cnf(axiom_041,axiom,
    cheating(b) = bfalse ).

cnf(axiom_042,axiom,
    cheating(c) = bfalse ).

cnf(axiom_043,axiom,
    astep(suc(N),Y) = aux(Y,N,step(Y)) ).

cnf(axiom_044,axiom,
    astep(z,Y) = just(Y) ).

cnf(axiom_045,axiom,
    thm_why(X,Y) = impl(eq3(astep(X,x(Y,theVar)),just(x(theVar,x(Y,theVar)))),eq4(cheating(Y),btrue)) ).

cnf(axiom_046,axiom,
    eq(theVar,k) = bfalse ).

cnf(axiom_047,axiom,
    eq(theVar,i) = bfalse ).

cnf(axiom_048,axiom,
    eq(theVar,s) = bfalse ).

cnf(axiom_049,axiom,
    eq(theVar,b) = bfalse ).

cnf(axiom_050,axiom,
    eq(theVar,c) = bfalse ).

cnf(axiom_051,axiom,
    eq(k,theVar) = bfalse ).

cnf(axiom_052,axiom,
    eq(k,i) = bfalse ).

cnf(axiom_053,axiom,
    eq(k,s) = bfalse ).

cnf(axiom_054,axiom,
    eq(k,b) = bfalse ).

cnf(axiom_055,axiom,
    eq(k,c) = bfalse ).

cnf(axiom_056,axiom,
    eq(i,theVar) = bfalse ).

cnf(axiom_057,axiom,
    eq(i,k) = bfalse ).

cnf(axiom_058,axiom,
    eq(i,s) = bfalse ).

cnf(axiom_059,axiom,
    eq(i,b) = bfalse ).

cnf(axiom_060,axiom,
    eq(i,c) = bfalse ).

cnf(axiom_061,axiom,
    eq(s,theVar) = bfalse ).

cnf(axiom_062,axiom,
    eq(s,k) = bfalse ).

cnf(axiom_063,axiom,
    eq(s,i) = bfalse ).

cnf(axiom_064,axiom,
    eq(s,b) = bfalse ).

cnf(axiom_065,axiom,
    eq(s,c) = bfalse ).

cnf(axiom_066,axiom,
    eq(b,theVar) = bfalse ).

cnf(axiom_067,axiom,
    eq(b,k) = bfalse ).

cnf(axiom_068,axiom,
    eq(b,i) = bfalse ).

cnf(axiom_069,axiom,
    eq(b,s) = bfalse ).

cnf(axiom_070,axiom,
    eq(b,c) = bfalse ).

cnf(axiom_071,axiom,
    eq(c,theVar) = bfalse ).

cnf(axiom_072,axiom,
    eq(c,k) = bfalse ).

cnf(axiom_073,axiom,
    eq(c,i) = bfalse ).

cnf(axiom_074,axiom,
    eq(c,s) = bfalse ).

cnf(axiom_075,axiom,
    eq(c,b) = bfalse ).

cnf(axiom_076,axiom,
    eq4(bfalse,btrue) = bfalse ).

cnf(axiom_077,axiom,
    eq4(btrue,bfalse) = bfalse ).

cnf(axiom_078,axiom,
    ( eq(X,Z) != bfalse
    | eq(x(X,Y),x(Z,X2)) = bfalse ) ).

cnf(axiom_079,axiom,
    ( eq(X,Z) != btrue
    | eq(x(X,Y),x(Z,X2)) = eq(Y,X2) ) ).

cnf(axiom_080,axiom,
    eq(x(X,Y),theVar) = bfalse ).

cnf(axiom_081,axiom,
    eq(x(X,Y),k) = bfalse ).

cnf(axiom_082,axiom,
    eq(x(X,Y),i) = bfalse ).

cnf(axiom_083,axiom,
    eq(x(X,Y),s) = bfalse ).

cnf(axiom_084,axiom,
    eq(x(X,Y),b) = bfalse ).

cnf(axiom_085,axiom,
    eq(x(X,Y),c) = bfalse ).

cnf(axiom_086,axiom,
    eq(theVar,x(X,Y)) = bfalse ).

cnf(axiom_087,axiom,
    eq(k,x(X,Y)) = bfalse ).

cnf(axiom_088,axiom,
    eq(i,x(X,Y)) = bfalse ).

cnf(axiom_089,axiom,
    eq(s,x(X,Y)) = bfalse ).

cnf(axiom_090,axiom,
    eq(b,x(X,Y)) = bfalse ).

cnf(axiom_091,axiom,
    eq(c,x(X,Y)) = bfalse ).

cnf(axiom_092,axiom,
    eq2(suc(X),suc(Y)) = eq2(X,Y) ).

cnf(axiom_093,axiom,
    eq2(suc(X),z) = bfalse ).

cnf(axiom_094,axiom,
    eq2(z,suc(X)) = bfalse ).

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

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

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

cnf(axiom_098,axiom,
    eq4(X,X) = btrue ).

cnf(axiom_099,axiom,
    eq3(just(X),just(Y)) = eq(X,Y) ).

cnf(axiom_100,axiom,
    eq3(nothing,just(X)) = bfalse ).

cnf(axiom_101,axiom,
    eq3(just(X),nothing) = bfalse ).

cnf(goal,negated_conjecture,
    eq4(thm_why(X,Y),bfalse) != btrue ).

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