%------------------------------------------------------------------------------
% File     : SWX191+1 : TPTP v9.3.0. Released v9.3.0.
% Domain   : Software Verification
% Problem  : Finding an antiderivative
% Version  : Especial.
% English  :

% Refs     : [CST26] Claessen et al. (2026), Email to Geoff Sutcliffe
% Source   : [CST26]
% Names    : Deriv_propm4.p [CST26]

% Status   : Theorem
% Rating   : 1.00 v9.3.0
% Syntax   : Number of formulae    :   54 (  40 unt;   0 def)
%            Number of atoms       :   71 (  71 equ)
%            Maximal formula atoms :    3 (   1 avg)
%            Number of connectives :   40 (  23   ~;   0   |;   0   &)
%                                         (   0 <=>;  17  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    6 (   3 avg)
%            Maximal term depth    :    6 (   2 avg)
%            Number of predicates  :    1 (   0 usr;   0 prp; 2-2 aty)
%            Number of functors    :   24 (  24 usr;   2 con; 0-2 aty)
%            Number of variables   :   95 (  94   !;   1   ?)
% SPC      : FOF_THM_RFO_PEQ

% Comments :
%------------------------------------------------------------------------------
fof(axiom_001,axiom,
    ! [X] : proj1S(s(X)) = X ).

fof(axiom_002,axiom,
    ! [X] : s(X) != z ).

fof(axiom_003,axiom,
    ! [X] : proj1N(n(X)) = X ).

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

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

fof(axiom_006,axiom,
    ! [X,X2] : proj12(y(X,X2)) = X ).

fof(axiom_007,axiom,
    ! [X,X2] : proj22(y(X,X2)) = X2 ).

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

fof(axiom_009,axiom,
    ! [X,X2,X3] : n(X) != y(X2,X3) ).

fof(axiom_010,axiom,
    ! [X] : n(X) != x2 ).

fof(axiom_011,axiom,
    ! [X,X2,X3,X4] : x(X,X2) != y(X3,X4) ).

fof(axiom_012,axiom,
    ! [X,X2] : x(X,X2) != x2 ).

fof(axiom_013,axiom,
    ! [X,X2] : y(X,X2) != x2 ).

fof(axiom_014,axiom,
    ! [Y,E] :
      ( Y = E
     => fail2(Y,E) = y(n(s(s(z))),opt(Y)) ) ).

fof(axiom_015,axiom,
    ! [Y,E] :
      ( Y != E
     => ( Y != x(proj1(Y),proj2(Y))
       => fail2(Y,E) = x(opt(Y),opt(E)) ) ) ).

fof(axiom_016,axiom,
    ! [E,A,B] :
      ( x(A,B) != E
     => fail2(x(A,B),E) = opt(x(A,x(B,E))) ) ).

fof(axiom_017,axiom,
    ! [Y,E] :
      ( Y != n(proj1N(Y))
     => fail1(Y,E) = fail2(Y,E) ) ).

fof(axiom_018,axiom,
    ! [E,C] :
      ( E != n(proj1N(E))
     => fail1(n(C),E) = fail2(n(C),E) ) ).

fof(axiom_019,axiom,
    ! [C,B2] : fail1(n(C),n(B2)) = n(addNat(C,B2)) ).

fof(axiom_020,axiom,
    ! [Y,E] :
      ( E != n(proj1N(E))
     => fail(Y,E) = fail1(Y,E) ) ).

fof(axiom_021,axiom,
    ! [Y,X2] : fail(Y,n(s(X2))) = fail1(Y,n(s(X2))) ).

fof(axiom_022,axiom,
    ! [Y] : fail(Y,n(z)) = Y ).

fof(axiom_023,axiom,
    ! [X5,E2] : fail4(X5,E2) = y(opt(X5),opt(E2)) ).

fof(axiom_024,axiom,
    ! [X5,E2] :
      ( X5 != n(proj1N(X5))
     => ( X5 != y(proj12(X5),proj22(X5))
       => fail32(X5,E2) = fail4(X5,E2) ) ) ).

fof(axiom_025,axiom,
    ! [E2,A2] :
      ( E2 != n(proj1N(E2))
     => fail32(n(A2),E2) = fail4(n(A2),E2) ) ).

fof(axiom_026,axiom,
    ! [A2,B3] : fail32(n(A2),n(B3)) = n(mulNat(A2,B3)) ).

fof(axiom_027,axiom,
    ! [E2,A3,B4] : fail32(y(A3,B4),E2) = opt(y(A3,y(B4,E2))) ).

fof(axiom_028,axiom,
    ! [X5,E2] :
      ( E2 != n(proj1N(E2))
     => fail22(X5,E2) = fail32(X5,E2) ) ).

fof(axiom_029,axiom,
    ! [X5,X8] : fail22(X5,n(s(s(X8)))) = fail32(X5,n(s(s(X8)))) ).

fof(axiom_030,axiom,
    ! [X5] : fail22(X5,n(s(z))) = X5 ).

fof(axiom_031,axiom,
    ! [X5] : fail22(X5,n(z)) = fail32(X5,n(z)) ).

fof(axiom_032,axiom,
    ! [X5,E2] :
      ( X5 != n(proj1N(X5))
     => fail12(X5,E2) = fail22(X5,E2) ) ).

fof(axiom_033,axiom,
    ! [E2,X11] : fail12(n(s(s(X11))),E2) = fail22(n(s(s(X11))),E2) ).

fof(axiom_034,axiom,
    ! [E2] : fail12(n(s(z)),E2) = E2 ).

fof(axiom_035,axiom,
    ! [E2] : fail12(n(z),E2) = fail22(n(z),E2) ).

fof(axiom_036,axiom,
    ! [X5,E2] :
      ( E2 != n(proj1N(E2))
     => fail3(X5,E2) = fail12(X5,E2) ) ).

fof(axiom_037,axiom,
    ! [X5,X13] : fail3(X5,n(s(X13))) = fail12(X5,n(s(X13))) ).

fof(axiom_038,axiom,
    ! [X5] : fail3(X5,n(z)) = n(z) ).

fof(axiom_039,axiom,
    ! [Y] : d(n(Y)) = n(z) ).

fof(axiom_040,axiom,
    ! [F,G] : d(x(F,G)) = x(d(F),d(G)) ).

fof(axiom_041,axiom,
    ! [H,G2] : d(y(H,G2)) = x(y(d(H),G2),y(H,d(G2))) ).

fof(axiom_042,axiom,
    d(x2) = n(s(z)) ).

fof(axiom_043,axiom,
    ! [Y,Z] : addNat(s(Z),Y) = s(addNat(Z,Y)) ).

fof(axiom_044,axiom,
    ! [Y] : addNat(z,Y) = Y ).

fof(axiom_045,axiom,
    ! [Y,Z] : mulNat(s(Z),Y) = addNat(Y,mulNat(Z,Y)) ).

fof(axiom_046,axiom,
    ! [Y] : mulNat(z,Y) = z ).

fof(axiom_047,axiom,
    ! [X] :
      ( X != x(proj1(X),proj2(X))
     => ( X != y(proj12(X),proj22(X))
       => opt(X) = X ) ) ).

fof(axiom_048,axiom,
    ! [Y,E] :
      ( Y != n(proj1N(Y))
     => opt(x(Y,E)) = fail(Y,E) ) ).

fof(axiom_049,axiom,
    ! [E,X4] : opt(x(n(s(X4)),E)) = fail(n(s(X4)),E) ).

fof(axiom_050,axiom,
    ! [E] : opt(x(n(z),E)) = E ).

fof(axiom_051,axiom,
    ! [X5,E2] :
      ( X5 != n(proj1N(X5))
     => opt(y(X5,E2)) = fail3(X5,E2) ) ).

fof(axiom_052,axiom,
    ! [E2,X15] : opt(y(n(s(X15)),E2)) = fail3(n(s(X15)),E2) ).

fof(axiom_053,axiom,
    ! [E2] : opt(y(n(z),E2)) = n(z) ).

fof(goal_054,conjecture,
    ? [E] : opt(d(E)) = x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))) ).

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