%------------------------------------------------------------------------------
% 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   : Unsatisfiable
% Rating   : 0.83 v9.3.0
% Syntax   : Number of clauses     :   92 (  88 unt;   0 nHn;   5 RR)
%            Number of literals    :   96 (  96 equ;   5 neg)
%            Maximal clause size   :    2 (   1 avg)
%            Maximal term depth    :    8 (   2 avg)
%            Number of predicates  :    1 (   0 usr;   0 prp; 2-2 aty)
%            Number of functors    :   26 (  26 usr;   4 con; 0-3 aty)
%            Number of variables   :  180 (  43 sgn)
% SPC      : CNF_UNS_RFO_PEQ_NUE

% Comments :
%------------------------------------------------------------------------------
cnf(axiom,axiom,
    aux(Y,E,btrue) = y(n(s(s(z))),opt(Y)) ).

cnf(axiom_001,axiom,
    aux(x(B,C),E,bfalse) = opt(x(B,x(C,E))) ).

cnf(axiom_002,axiom,
    aux(n(X),E,bfalse) = x(opt(n(X)),opt(E)) ).

cnf(axiom_003,axiom,
    aux(y(X,X2),E,bfalse) = x(opt(y(X,X2)),opt(E)) ).

cnf(axiom_004,axiom,
    aux(x2,E,bfalse) = x(opt(x2),opt(E)) ).

cnf(axiom_005,axiom,
    fail2(Y,E) = aux(Y,E,eq2(Y,E)) ).

cnf(axiom_006,axiom,
    fail1(n(A2),n(B2)) = n(addNat(A2,B2)) ).

cnf(axiom_007,axiom,
    fail1(n(A2),x(X,X2)) = fail2(n(A2),x(X,X2)) ).

cnf(axiom_008,axiom,
    fail1(n(A2),y(X,X2)) = fail2(n(A2),y(X,X2)) ).

cnf(axiom_009,axiom,
    fail1(n(A2),x2) = fail2(n(A2),x2) ).

cnf(axiom_010,axiom,
    fail1(x(X,X2),E) = fail2(x(X,X2),E) ).

cnf(axiom_011,axiom,
    fail1(y(X,X2),E) = fail2(y(X,X2),E) ).

cnf(axiom_012,axiom,
    fail1(x2,E) = fail2(x2,E) ).

cnf(axiom_013,axiom,
    fail(Y,n(s(X2))) = fail1(Y,n(s(X2))) ).

cnf(axiom_014,axiom,
    fail(Y,n(z)) = Y ).

cnf(axiom_015,axiom,
    fail(Y,x(X,X2)) = fail1(Y,x(X,X2)) ).

cnf(axiom_016,axiom,
    fail(Y,y(X,X2)) = fail1(Y,y(X,X2)) ).

cnf(axiom_017,axiom,
    fail(Y,x2) = fail1(Y,x2) ).

cnf(axiom_018,axiom,
    fail4(X5,E2) = y(opt(X5),opt(E2)) ).

cnf(axiom_019,axiom,
    fail32(n(A3),n(B3)) = n(mulNat(A3,B3)) ).

cnf(axiom_020,axiom,
    fail32(n(A3),x(X,X2)) = fail4(n(A3),x(X,X2)) ).

cnf(axiom_021,axiom,
    fail32(n(A3),y(X,X2)) = fail4(n(A3),y(X,X2)) ).

cnf(axiom_022,axiom,
    fail32(n(A3),x2) = fail4(n(A3),x2) ).

cnf(axiom_023,axiom,
    fail32(y(A4,B4),E2) = opt(y(A4,y(B4,E2))) ).

cnf(axiom_024,axiom,
    fail32(x(X,X2),E2) = fail4(x(X,X2),E2) ).

cnf(axiom_025,axiom,
    fail32(x2,E2) = fail4(x2,E2) ).

cnf(axiom_026,axiom,
    fail22(X5,n(s(s(X8)))) = fail32(X5,n(s(s(X8)))) ).

cnf(axiom_027,axiom,
    fail22(X5,n(s(z))) = X5 ).

cnf(axiom_028,axiom,
    fail22(X5,n(z)) = fail32(X5,n(z)) ).

cnf(axiom_029,axiom,
    fail22(X5,x(X,X2)) = fail32(X5,x(X,X2)) ).

cnf(axiom_030,axiom,
    fail22(X5,y(X,X2)) = fail32(X5,y(X,X2)) ).

cnf(axiom_031,axiom,
    fail22(X5,x2) = fail32(X5,x2) ).

cnf(axiom_032,axiom,
    fail12(n(s(s(X11))),E2) = fail22(n(s(s(X11))),E2) ).

cnf(axiom_033,axiom,
    fail12(n(s(z)),E2) = E2 ).

cnf(axiom_034,axiom,
    fail12(n(z),E2) = fail22(n(z),E2) ).

cnf(axiom_035,axiom,
    fail12(x(X,X2),E2) = fail22(x(X,X2),E2) ).

cnf(axiom_036,axiom,
    fail12(y(X,X2),E2) = fail22(y(X,X2),E2) ).

cnf(axiom_037,axiom,
    fail12(x2,E2) = fail22(x2,E2) ).

cnf(axiom_038,axiom,
    fail3(X5,n(s(X13))) = fail12(X5,n(s(X13))) ).

cnf(axiom_039,axiom,
    fail3(X5,n(z)) = n(z) ).

cnf(axiom_040,axiom,
    fail3(X5,x(X,X2)) = fail12(X5,x(X,X2)) ).

cnf(axiom_041,axiom,
    fail3(X5,y(X,X2)) = fail12(X5,y(X,X2)) ).

cnf(axiom_042,axiom,
    fail3(X5,x2) = fail12(X5,x2) ).

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

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

cnf(axiom_045,axiom,
    d(n(Y)) = n(z) ).

cnf(axiom_046,axiom,
    d(x(F,G)) = x(d(F),d(G)) ).

cnf(axiom_047,axiom,
    d(y(H,G2)) = x(y(d(H),G2),y(H,d(G2))) ).

cnf(axiom_048,axiom,
    d(x2) = n(s(z)) ).

cnf(axiom_049,axiom,
    addNat(s(Z),Y) = s(addNat(Z,Y)) ).

cnf(axiom_050,axiom,
    addNat(z,Y) = Y ).

cnf(axiom_051,axiom,
    mulNat(s(Z),Y) = addNat(Y,mulNat(Z,Y)) ).

cnf(axiom_052,axiom,
    mulNat(z,Y) = z ).

cnf(axiom_053,axiom,
    opt(x(n(s(X4)),E)) = fail(n(s(X4)),E) ).

cnf(axiom_054,axiom,
    opt(x(n(z),E)) = E ).

cnf(axiom_055,axiom,
    opt(x(x(X,X2),E)) = fail(x(X,X2),E) ).

cnf(axiom_056,axiom,
    opt(x(y(X,X2),E)) = fail(y(X,X2),E) ).

cnf(axiom_057,axiom,
    opt(x(x2,E)) = fail(x2,E) ).

cnf(axiom_058,axiom,
    opt(y(n(s(X15)),E2)) = fail3(n(s(X15)),E2) ).

cnf(axiom_059,axiom,
    opt(y(n(z),E2)) = n(z) ).

cnf(axiom_060,axiom,
    opt(y(x(X,X2),E2)) = fail3(x(X,X2),E2) ).

cnf(axiom_061,axiom,
    opt(y(y(X,X2),E2)) = fail3(y(X,X2),E2) ).

cnf(axiom_062,axiom,
    opt(y(x2,E2)) = fail3(x2,E2) ).

cnf(axiom_063,axiom,
    opt(n(X)) = n(X) ).

cnf(axiom_064,axiom,
    opt(x2) = x2 ).

cnf(axiom_065,axiom,
    propm4(X) = impl(eq2(opt(d(X)),x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2)))))),eq3(btrue,bfalse)) ).

cnf(axiom_066,axiom,
    eq3(bfalse,btrue) = bfalse ).

cnf(axiom_067,axiom,
    eq3(btrue,bfalse) = bfalse ).

cnf(axiom_068,axiom,
    eq2(n(X),n(Y)) = eq(X,Y) ).

cnf(axiom_069,axiom,
    ( eq2(X,Z) != bfalse
    | eq2(x(X,Y),x(Z,X2)) = bfalse ) ).

cnf(axiom_070,axiom,
    ( eq2(X,Z) != btrue
    | eq2(x(X,Y),x(Z,X2)) = eq2(Y,X2) ) ).

cnf(axiom_071,axiom,
    ( eq2(X,Z) != bfalse
    | eq2(y(X,Y),y(Z,X2)) = bfalse ) ).

cnf(axiom_072,axiom,
    ( eq2(X,Z) != btrue
    | eq2(y(X,Y),y(Z,X2)) = eq2(Y,X2) ) ).

cnf(axiom_073,axiom,
    eq2(n(X),x(Y,Z)) = bfalse ).

cnf(axiom_074,axiom,
    eq2(n(X),y(Y,Z)) = bfalse ).

cnf(axiom_075,axiom,
    eq2(n(X),x2) = bfalse ).

cnf(axiom_076,axiom,
    eq2(x(X,Y),n(Z)) = bfalse ).

cnf(axiom_077,axiom,
    eq2(x(X,Y),y(Z,X2)) = bfalse ).

cnf(axiom_078,axiom,
    eq2(x(X,Y),x2) = bfalse ).

cnf(axiom_079,axiom,
    eq2(y(X,Y),n(Z)) = bfalse ).

cnf(axiom_080,axiom,
    eq2(y(X,Y),x(Z,X2)) = bfalse ).

cnf(axiom_081,axiom,
    eq2(y(X,Y),x2) = bfalse ).

cnf(axiom_082,axiom,
    eq2(x2,n(X)) = bfalse ).

cnf(axiom_083,axiom,
    eq2(x2,x(X,Y)) = bfalse ).

cnf(axiom_084,axiom,
    eq2(x2,y(X,Y)) = bfalse ).

cnf(axiom_085,axiom,
    eq(s(X),s(Y)) = eq(X,Y) ).

cnf(axiom_086,axiom,
    eq(s(X),z) = bfalse ).

cnf(axiom_087,axiom,
    eq(z,s(X)) = bfalse ).

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

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

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

cnf(goal,negated_conjecture,
    eq3(propm4(X),bfalse) != btrue ).

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