%------------------------------------------------------------------------------
% 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   : Theorem
% Rating   : 1.00 v9.3.0
% Syntax   : Number of formulae    :   48 (  39 unt;   0 def)
%            Number of atoms       :   63 (  57 equ)
%            Maximal formula atoms :    4 (   1 avg)
%            Number of connectives :   50 (  35   ~;   1   |;   0   &)
%                                         (   1 <=>;  13  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    9 (   3 avg)
%            Maximal term depth    :    5 (   2 avg)
%            Number of predicates  :    2 (   1 usr;   0 prp; 1-2 aty)
%            Number of functors    :   19 (  19 usr;   8 con; 0-4 aty)
%            Number of variables   :   67 (  65   !;   2   ?)
% SPC      : FOF_THM_RFO_SEQ

% Comments :
%------------------------------------------------------------------------------
fof(axiom_001,axiom,
    ! [X,X2] : proj1(x(X,X2)) = X ).

fof(axiom_002,axiom,
    ! [X,X2] : proj2(x(X,X2)) = X2 ).

fof(axiom_003,axiom,
    ! [X,X2] : x(X,X2) != theVar ).

fof(axiom_004,axiom,
    ! [X,X2] : x(X,X2) != k ).

fof(axiom_005,axiom,
    ! [X,X2] : x(X,X2) != i ).

fof(axiom_006,axiom,
    ! [X,X2] : x(X,X2) != s ).

fof(axiom_007,axiom,
    ! [X,X2] : x(X,X2) != b ).

fof(axiom_008,axiom,
    ! [X,X2] : x(X,X2) != c ).

fof(axiom_009,axiom,
    theVar != k ).

fof(axiom_010,axiom,
    theVar != i ).

fof(axiom_011,axiom,
    theVar != s ).

fof(axiom_012,axiom,
    theVar != b ).

fof(axiom_013,axiom,
    theVar != c ).

fof(axiom_014,axiom,
    k != i ).

fof(axiom_015,axiom,
    k != s ).

fof(axiom_016,axiom,
    k != b ).

fof(axiom_017,axiom,
    k != c ).

fof(axiom_018,axiom,
    i != s ).

fof(axiom_019,axiom,
    i != b ).

fof(axiom_020,axiom,
    i != c ).

fof(axiom_021,axiom,
    s != b ).

fof(axiom_022,axiom,
    s != c ).

fof(axiom_023,axiom,
    b != c ).

fof(axiom_024,axiom,
    ! [X] : proj1Suc(suc(X)) = X ).

fof(axiom_025,axiom,
    ! [X] : suc(X) != z ).

fof(axiom_026,axiom,
    ! [X] : proj1Just(just(X)) = X ).

fof(axiom_027,axiom,
    ! [X] : nothing != just(X) ).

fof(axiom_028,axiom,
    ! [Y,Z] : fail(Y,Z) = par(Y,Z,step(Y),step(Z)) ).

fof(axiom_029,axiom,
    ! [X,Y] : par(X,Y,nothing,nothing) = nothing ).

fof(axiom_030,axiom,
    ! [X,Y,U_red] : par(X,Y,nothing,just(U_red)) = just(x(X,U_red)) ).

fof(axiom_031,axiom,
    ! [X,Y,T_red] : par(X,Y,just(T_red),nothing) = just(x(T_red,Y)) ).

fof(axiom_032,axiom,
    ! [X,Y,T_red,U_red2] : par(X,Y,just(T_red),just(U_red2)) = just(x(T_red,U_red2)) ).

fof(axiom_033,axiom,
    ! [X] :
      ( X != x(proj1(X),proj2(X))
     => step(X) = nothing ) ).

fof(axiom_034,axiom,
    ! [Y,Z] :
      ( Y != x(proj1(Y),proj2(Y))
     => ( Y != i
       => step(x(Y,Z)) = fail(Y,Z) ) ) ).

fof(axiom_035,axiom,
    ! [Z,X2,G] :
      ( X2 != x(proj1(X2),proj2(X2))
     => ( X2 != k
       => step(x(x(X2,G),Z)) = fail(x(X2,G),Z) ) ) ).

fof(axiom_036,axiom,
    ! [Z,G,X3,F] :
      ( X3 != s
     => ( X3 != b
       => ( X3 != c
         => step(x(x(x(X3,F),G),Z)) = fail(x(x(X3,F),G),Z) ) ) ) ).

fof(axiom_037,axiom,
    ! [Z,G,F] : step(x(x(x(s,F),G),Z)) = just(x(x(F,Z),x(G,Z))) ).

fof(axiom_038,axiom,
    ! [Z,G,F] : step(x(x(x(b,F),G),Z)) = just(x(F,x(G,Z))) ).

fof(axiom_039,axiom,
    ! [Z,G,F] : step(x(x(x(c,F),G),Z)) = just(x(x(F,Z),G)) ).

fof(axiom_040,axiom,
    ! [Z,G] : step(x(x(k,G),Z)) = just(G) ).

fof(axiom_041,axiom,
    ! [Z] : step(x(i,Z)) = just(Z) ).

fof(axiom_042,axiom,
    ! [X] :
      ( X != x(proj1(X),proj2(X))
     => ( X != theVar
       => ~ cheating(X) ) ) ).

fof(axiom_043,axiom,
    ! [A,B] :
      ( cheating(x(A,B))
    <=> ( cheating(A)
        | cheating(B) ) ) ).

fof(axiom_044,axiom,
    cheating(theVar) ).

fof(axiom_045,axiom,
    ! [Y,N] :
      ( step(Y) = nothing
     => astep(suc(N),Y) = nothing ) ).

fof(axiom_046,axiom,
    ! [Y,N,U] :
      ( step(Y) = just(U)
     => astep(suc(N),Y) = astep(N,U) ) ).

fof(axiom_047,axiom,
    ! [Y] : astep(z,Y) = just(Y) ).

fof(goal_048,conjecture,
    ? [N,Y] :
      ~ ( astep(N,x(Y,theVar)) = just(x(theVar,x(Y,theVar)))
       => cheating(Y) ) ).

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