TPTP Problem File: SWX189-1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX189-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_prop2.p [CST26]
% Status : Unsatisfiable
% Rating : 0.75 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 : 6 ( 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,
prop2(X) = impl(eq2(opt(d(X)),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(prop2(X),bfalse) != btrue ).
%------------------------------------------------------------------------------