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

% 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(goal_042,conjecture,
    ? [X] : step(X) = just(X) ).

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