TPTP Problem File: SWX194-1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX194-1 : TPTP v9.3.0. Released v9.3.0.
% Domain : Software Verification
% Problem : A buggy simplication function for expressions
% Version : Especial.
% English :
% Refs : [CST26] Claessen et al. (2026), Email to Geoff Sutcliffe
% Source : [CST26]
% Names : Expr_prop1.p [CST26]
% Status : Unsatisfiable
% Rating : 0.58 v9.3.0
% Syntax : Number of clauses : 182 ( 176 unt; 0 nHn; 3 RR)
% Number of literals : 188 ( 188 equ; 7 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% Number of functors : 48 ( 48 usr; 4 con; 0-4 aty)
% Number of variables : 434 ( 115 sgn)
% SPC : CNF_UNS_RFO_PEQ_NUE
% Comments :
%------------------------------------------------------------------------------
cnf(axiom,axiom,
aux(Z,Y2,btrue) = mul(n(suc(suc(zero))),v(Z)) ).
cnf(axiom_001,axiom,
aux(Z,Y2,bfalse) = add(v(Z),v(Y2)) ).
cnf(axiom_002,axiom,
aux2(Y,B,btrue) = mul(n(suc(suc(zero))),Y) ).
cnf(axiom_003,axiom,
aux2(add(C,B1),B,bfalse) = add(C,add(B1,B)) ).
cnf(axiom_004,axiom,
aux2(v(Z),v(Y2),bfalse) = aux(Z,Y2,eq2(Z,Z)) ).
cnf(axiom_005,axiom,
aux2(v(Z),n(X),bfalse) = add(v(Z),n(X)) ).
cnf(axiom_006,axiom,
aux2(v(Z),add(X,X2),bfalse) = add(v(Z),add(X,X2)) ).
cnf(axiom_007,axiom,
aux2(v(Z),mul(X,X2),bfalse) = add(v(Z),mul(X,X2)) ).
cnf(axiom_008,axiom,
aux2(v(Z),eq(X,X2),bfalse) = add(v(Z),eq(X,X2)) ).
cnf(axiom_009,axiom,
aux2(n(X),B,bfalse) = add(n(X),B) ).
cnf(axiom_010,axiom,
aux2(mul(X,X2),B,bfalse) = add(mul(X,X2),B) ).
cnf(axiom_011,axiom,
aux2(eq(X,X2),B,bfalse) = add(eq(X,X2),B) ).
cnf(axiom_012,axiom,
aux3(Z,Y2,btrue) = mul(n(suc(suc(zero))),v(Z)) ).
cnf(axiom_013,axiom,
aux3(Z,Y2,bfalse) = add(v(Z),v(Y2)) ).
cnf(axiom_014,axiom,
aux4(Y,B,btrue) = mul(n(suc(suc(zero))),Y) ).
cnf(axiom_015,axiom,
aux4(add(C,B1),B,bfalse) = add(C,add(B1,B)) ).
cnf(axiom_016,axiom,
aux4(v(Z),v(Y2),bfalse) = aux3(Z,Y2,eq2(Z,Z)) ).
cnf(axiom_017,axiom,
aux4(v(Z),n(X),bfalse) = add(v(Z),n(X)) ).
cnf(axiom_018,axiom,
aux4(v(Z),add(X,X2),bfalse) = add(v(Z),add(X,X2)) ).
cnf(axiom_019,axiom,
aux4(v(Z),mul(X,X2),bfalse) = add(v(Z),mul(X,X2)) ).
cnf(axiom_020,axiom,
aux4(v(Z),eq(X,X2),bfalse) = add(v(Z),eq(X,X2)) ).
cnf(axiom_021,axiom,
aux4(n(X),B,bfalse) = add(n(X),B) ).
cnf(axiom_022,axiom,
aux4(mul(X,X2),B,bfalse) = add(mul(X,X2),B) ).
cnf(axiom_023,axiom,
aux4(eq(X,X2),B,bfalse) = add(eq(X,X2),B) ).
cnf(axiom_024,axiom,
aux5(A3,B3,btrue) = n(suc(zero)) ).
cnf(axiom_025,axiom,
aux5(A3,B3,bfalse) = eq(A3,B3) ).
cnf(axiom_026,axiom,
aux6(A,B,n(zero)) = b(B) ).
cnf(axiom_027,axiom,
aux6(A,B,n(suc(X5))) = fail4(y(A),b(B)) ).
cnf(axiom_028,axiom,
aux6(A,B,add(X,X2)) = fail4(y(A),b(B)) ).
cnf(axiom_029,axiom,
aux6(A,B,mul(X,X2)) = fail4(y(A),b(B)) ).
cnf(axiom_030,axiom,
aux6(A,B,eq(X,X2)) = fail4(y(A),b(B)) ).
cnf(axiom_031,axiom,
aux6(A,B,v(X)) = fail4(y(A),b(B)) ).
cnf(axiom_032,axiom,
aux7(C,B2,n(zero)) = n(zero) ).
cnf(axiom_033,axiom,
aux7(C,B2,n(suc(X16))) = fail23(x6(C),b2(B2)) ).
cnf(axiom_034,axiom,
aux7(C,B2,add(X,X2)) = fail23(x6(C),b2(B2)) ).
cnf(axiom_035,axiom,
aux7(C,B2,mul(X,X2)) = fail23(x6(C),b2(B2)) ).
cnf(axiom_036,axiom,
aux7(C,B2,eq(X,X2)) = fail23(x6(C),b2(B2)) ).
cnf(axiom_037,axiom,
aux7(C,B2,v(X)) = fail23(x6(C),b2(B2)) ).
cnf(axiom_038,axiom,
aux8(A2,B3,btrue) = n(suc(zero)) ).
cnf(axiom_039,axiom,
aux8(A2,B3,bfalse) = eq(a3(A2),b3(B3)) ).
cnf(axiom_040,axiom,
aux9(X,A2,B3,btrue) = suc(zero) ).
cnf(axiom_041,axiom,
aux9(X,A2,B3,bfalse) = zero ).
cnf(axiom_042,axiom,
fail1(Y,B) = aux2(Y,B,eq3(Y,B)) ).
cnf(axiom_043,axiom,
fail(Y,n(zero)) = Y ).
cnf(axiom_044,axiom,
fail(Y,n(suc(X3))) = fail1(Y,n(suc(X3))) ).
cnf(axiom_045,axiom,
fail(Y,add(X,X2)) = fail1(Y,add(X,X2)) ).
cnf(axiom_046,axiom,
fail(Y,mul(X,X2)) = fail1(Y,mul(X,X2)) ).
cnf(axiom_047,axiom,
fail(Y,eq(X,X2)) = fail1(Y,eq(X,X2)) ).
cnf(axiom_048,axiom,
fail(Y,v(X)) = fail1(Y,v(X)) ).
cnf(axiom_049,axiom,
fail3(mul(A2,B12),B2) = mul(A2,mul(B12,B2)) ).
cnf(axiom_050,axiom,
fail3(n(X),B2) = mul(n(X),B2) ).
cnf(axiom_051,axiom,
fail3(add(X,X2),B2) = mul(add(X,X2),B2) ).
cnf(axiom_052,axiom,
fail3(eq(X,X2),B2) = mul(eq(X,X2),B2) ).
cnf(axiom_053,axiom,
fail3(v(X),B2) = mul(v(X),B2) ).
cnf(axiom_054,axiom,
fail22(X6,n(zero)) = fail3(X6,n(zero)) ).
cnf(axiom_055,axiom,
fail22(X6,n(suc(zero))) = X6 ).
cnf(axiom_056,axiom,
fail22(X6,n(suc(suc(X9)))) = fail3(X6,n(suc(suc(X9)))) ).
cnf(axiom_057,axiom,
fail22(X6,add(X,X2)) = fail3(X6,add(X,X2)) ).
cnf(axiom_058,axiom,
fail22(X6,mul(X,X2)) = fail3(X6,mul(X,X2)) ).
cnf(axiom_059,axiom,
fail22(X6,eq(X,X2)) = fail3(X6,eq(X,X2)) ).
cnf(axiom_060,axiom,
fail22(X6,v(X)) = fail3(X6,v(X)) ).
cnf(axiom_061,axiom,
fail12(n(zero),B2) = fail22(n(zero),B2) ).
cnf(axiom_062,axiom,
fail12(n(suc(zero)),B2) = B2 ).
cnf(axiom_063,axiom,
fail12(n(suc(suc(X12))),B2) = fail22(n(suc(suc(X12))),B2) ).
cnf(axiom_064,axiom,
fail12(add(X,X2),B2) = fail22(add(X,X2),B2) ).
cnf(axiom_065,axiom,
fail12(mul(X,X2),B2) = fail22(mul(X,X2),B2) ).
cnf(axiom_066,axiom,
fail12(eq(X,X2),B2) = fail22(eq(X,X2),B2) ).
cnf(axiom_067,axiom,
fail12(v(X),B2) = fail22(v(X),B2) ).
cnf(axiom_068,axiom,
fail2(X6,n(zero)) = n(zero) ).
cnf(axiom_069,axiom,
fail2(X6,n(suc(X14))) = fail12(X6,n(suc(X14))) ).
cnf(axiom_070,axiom,
fail2(X6,add(X,X2)) = fail12(X6,add(X,X2)) ).
cnf(axiom_071,axiom,
fail2(X6,mul(X,X2)) = fail12(X6,mul(X,X2)) ).
cnf(axiom_072,axiom,
fail2(X6,eq(X,X2)) = fail12(X6,eq(X,X2)) ).
cnf(axiom_073,axiom,
fail2(X6,v(X)) = fail12(X6,v(X)) ).
cnf(axiom_074,axiom,
fail13(Y,B) = aux4(Y,B,eq3(Y,B)) ).
cnf(axiom_075,axiom,
fail4(Y,n(zero)) = Y ).
cnf(axiom_076,axiom,
fail4(Y,n(suc(X3))) = fail13(Y,n(suc(X3))) ).
cnf(axiom_077,axiom,
fail4(Y,add(X,X2)) = fail13(Y,add(X,X2)) ).
cnf(axiom_078,axiom,
fail4(Y,mul(X,X2)) = fail13(Y,mul(X,X2)) ).
cnf(axiom_079,axiom,
fail4(Y,eq(X,X2)) = fail13(Y,eq(X,X2)) ).
cnf(axiom_080,axiom,
fail4(Y,v(X)) = fail13(Y,v(X)) ).
cnf(axiom_081,axiom,
b(B) = simp1(B) ).
cnf(axiom_082,axiom,
y(A) = simp1(A) ).
cnf(axiom_083,axiom,
fail32(mul(A2,B12),B2) = mul(A2,mul(B12,B2)) ).
cnf(axiom_084,axiom,
fail32(n(X),B2) = mul(n(X),B2) ).
cnf(axiom_085,axiom,
fail32(add(X,X2),B2) = mul(add(X,X2),B2) ).
cnf(axiom_086,axiom,
fail32(eq(X,X2),B2) = mul(eq(X,X2),B2) ).
cnf(axiom_087,axiom,
fail32(v(X),B2) = mul(v(X),B2) ).
cnf(axiom_088,axiom,
fail222(X6,n(zero)) = fail32(X6,n(zero)) ).
cnf(axiom_089,axiom,
fail222(X6,n(suc(zero))) = X6 ).
cnf(axiom_090,axiom,
fail222(X6,n(suc(suc(X9)))) = fail32(X6,n(suc(suc(X9)))) ).
cnf(axiom_091,axiom,
fail222(X6,add(X,X2)) = fail32(X6,add(X,X2)) ).
cnf(axiom_092,axiom,
fail222(X6,mul(X,X2)) = fail32(X6,mul(X,X2)) ).
cnf(axiom_093,axiom,
fail222(X6,eq(X,X2)) = fail32(X6,eq(X,X2)) ).
cnf(axiom_094,axiom,
fail222(X6,v(X)) = fail32(X6,v(X)) ).
cnf(axiom_095,axiom,
fail122(n(zero),B2) = fail222(n(zero),B2) ).
cnf(axiom_096,axiom,
fail122(n(suc(zero)),B2) = B2 ).
cnf(axiom_097,axiom,
fail122(n(suc(suc(X12))),B2) = fail222(n(suc(suc(X12))),B2) ).
cnf(axiom_098,axiom,
fail122(add(X,X2),B2) = fail222(add(X,X2),B2) ).
cnf(axiom_099,axiom,
fail122(mul(X,X2),B2) = fail222(mul(X,X2),B2) ).
cnf(axiom_100,axiom,
fail122(eq(X,X2),B2) = fail222(eq(X,X2),B2) ).
cnf(axiom_101,axiom,
fail122(v(X),B2) = fail222(v(X),B2) ).
cnf(axiom_102,axiom,
fail23(X6,n(zero)) = n(zero) ).
cnf(axiom_103,axiom,
fail23(X6,n(suc(X14))) = fail122(X6,n(suc(X14))) ).
cnf(axiom_104,axiom,
fail23(X6,add(X,X2)) = fail122(X6,add(X,X2)) ).
cnf(axiom_105,axiom,
fail23(X6,mul(X,X2)) = fail122(X6,mul(X,X2)) ).
cnf(axiom_106,axiom,
fail23(X6,eq(X,X2)) = fail122(X6,eq(X,X2)) ).
cnf(axiom_107,axiom,
fail23(X6,v(X)) = fail122(X6,v(X)) ).
cnf(axiom_108,axiom,
b2(B2) = simp1(B2) ).
cnf(axiom_109,axiom,
x6(C) = simp1(C) ).
cnf(axiom_110,axiom,
b3(B3) = simp1(B3) ).
cnf(axiom_111,axiom,
a3(A2) = simp1(A2) ).
cnf(axiom_112,axiom,
step1(add(n(zero),B)) = B ).
cnf(axiom_113,axiom,
step1(add(n(suc(X5)),B)) = fail(n(suc(X5)),B) ).
cnf(axiom_114,axiom,
step1(add(add(X,X2),B)) = fail(add(X,X2),B) ).
cnf(axiom_115,axiom,
step1(add(mul(X,X2),B)) = fail(mul(X,X2),B) ).
cnf(axiom_116,axiom,
step1(add(eq(X,X2),B)) = fail(eq(X,X2),B) ).
cnf(axiom_117,axiom,
step1(add(v(X),B)) = fail(v(X),B) ).
cnf(axiom_118,axiom,
step1(mul(n(zero),B2)) = n(zero) ).
cnf(axiom_119,axiom,
step1(mul(n(suc(X16)),B2)) = fail2(n(suc(X16)),B2) ).
cnf(axiom_120,axiom,
step1(mul(add(X,X2),B2)) = fail2(add(X,X2),B2) ).
cnf(axiom_121,axiom,
step1(mul(mul(X,X2),B2)) = fail2(mul(X,X2),B2) ).
cnf(axiom_122,axiom,
step1(mul(eq(X,X2),B2)) = fail2(eq(X,X2),B2) ).
cnf(axiom_123,axiom,
step1(mul(v(X),B2)) = fail2(v(X),B2) ).
cnf(axiom_124,axiom,
step1(eq(A3,B3)) = aux5(A3,B3,eq3(A3,B3)) ).
cnf(axiom_125,axiom,
step1(n(X)) = n(X) ).
cnf(axiom_126,axiom,
step1(v(X)) = v(X) ).
cnf(axiom_127,axiom,
simp1(add(A,B)) = aux6(A,B,y(A)) ).
cnf(axiom_128,axiom,
simp1(mul(C,B2)) = aux7(C,B2,x6(C)) ).
cnf(axiom_129,axiom,
simp1(eq(A2,B3)) = aux8(A2,B3,eq3(a3(A2),b3(B3))) ).
cnf(axiom_130,axiom,
simp1(n(X)) = n(X) ).
cnf(axiom_131,axiom,
simp1(v(X)) = v(X) ).
cnf(axiom_132,axiom,
fetch(nil,Y) = zero ).
cnf(axiom_133,axiom,
fetch(cons(N,St),zero) = N ).
cnf(axiom_134,axiom,
fetch(cons(N,St),suc(Z)) = fetch(St,Z) ).
cnf(axiom_135,axiom,
addNat(zero,Y) = Y ).
cnf(axiom_136,axiom,
addNat(suc(Z),Y) = suc(addNat(Z,Y)) ).
cnf(axiom_137,axiom,
mulNat(zero,Y) = zero ).
cnf(axiom_138,axiom,
mulNat(suc(Z),Y) = addNat(Y,mulNat(Z,Y)) ).
cnf(axiom_139,axiom,
eval(X,n(N)) = N ).
cnf(axiom_140,axiom,
eval(X,add(A,B)) = addNat(eval(X,A),eval(X,B)) ).
cnf(axiom_141,axiom,
eval(X,mul(C,B2)) = mulNat(eval(X,C),eval(X,B2)) ).
cnf(axiom_142,axiom,
eval(X,eq(A2,B3)) = aux9(X,A2,B3,eq2(eval(X,A2),eval(X,B3))) ).
cnf(axiom_143,axiom,
eval(X,v(Z)) = fetch(X,Z) ).
cnf(axiom_144,axiom,
prop1(X,Y) = eq4(eq2(eval(X,Y),eval(X,simp1(Y))),btrue) ).
cnf(axiom_145,axiom,
eq4(bfalse,btrue) = bfalse ).
cnf(axiom_146,axiom,
eq4(btrue,bfalse) = bfalse ).
cnf(axiom_147,axiom,
eq3(n(X),n(Y)) = eq2(X,Y) ).
cnf(axiom_148,axiom,
( eq3(X,Z) != bfalse
| eq3(add(X,Y),add(Z,X2)) = bfalse ) ).
cnf(axiom_149,axiom,
( eq3(X,Z) != btrue
| eq3(add(X,Y),add(Z,X2)) = eq3(Y,X2) ) ).
cnf(axiom_150,axiom,
( eq3(X,Z) != bfalse
| eq3(mul(X,Y),mul(Z,X2)) = bfalse ) ).
cnf(axiom_151,axiom,
( eq3(X,Z) != btrue
| eq3(mul(X,Y),mul(Z,X2)) = eq3(Y,X2) ) ).
cnf(axiom_152,axiom,
( eq3(X,Z) != bfalse
| eq3(eq(X,Y),eq(Z,X2)) = bfalse ) ).
cnf(axiom_153,axiom,
( eq3(X,Z) != btrue
| eq3(eq(X,Y),eq(Z,X2)) = eq3(Y,X2) ) ).
cnf(axiom_154,axiom,
eq3(v(X),v(Y)) = eq2(X,Y) ).
cnf(axiom_155,axiom,
eq3(n(X),add(Y,Z)) = bfalse ).
cnf(axiom_156,axiom,
eq3(n(X),mul(Y,Z)) = bfalse ).
cnf(axiom_157,axiom,
eq3(n(X),eq(Y,Z)) = bfalse ).
cnf(axiom_158,axiom,
eq3(n(X),v(Y)) = bfalse ).
cnf(axiom_159,axiom,
eq3(add(X,Y),n(Z)) = bfalse ).
cnf(axiom_160,axiom,
eq3(add(X,Y),mul(Z,X2)) = bfalse ).
cnf(axiom_161,axiom,
eq3(add(X,Y),eq(Z,X2)) = bfalse ).
cnf(axiom_162,axiom,
eq3(add(X,Y),v(Z)) = bfalse ).
cnf(axiom_163,axiom,
eq3(mul(X,Y),n(Z)) = bfalse ).
cnf(axiom_164,axiom,
eq3(mul(X,Y),add(Z,X2)) = bfalse ).
cnf(axiom_165,axiom,
eq3(mul(X,Y),eq(Z,X2)) = bfalse ).
cnf(axiom_166,axiom,
eq3(mul(X,Y),v(Z)) = bfalse ).
cnf(axiom_167,axiom,
eq3(eq(X,Y),n(Z)) = bfalse ).
cnf(axiom_168,axiom,
eq3(eq(X,Y),add(Z,X2)) = bfalse ).
cnf(axiom_169,axiom,
eq3(eq(X,Y),mul(Z,X2)) = bfalse ).
cnf(axiom_170,axiom,
eq3(eq(X,Y),v(Z)) = bfalse ).
cnf(axiom_171,axiom,
eq3(v(X),n(Y)) = bfalse ).
cnf(axiom_172,axiom,
eq3(v(X),add(Y,Z)) = bfalse ).
cnf(axiom_173,axiom,
eq3(v(X),mul(Y,Z)) = bfalse ).
cnf(axiom_174,axiom,
eq3(v(X),eq(Y,Z)) = bfalse ).
cnf(axiom_175,axiom,
eq2(suc(X),suc(Y)) = eq2(X,Y) ).
cnf(axiom_176,axiom,
eq2(zero,suc(X)) = bfalse ).
cnf(axiom_177,axiom,
eq2(suc(X),zero) = bfalse ).
cnf(axiom_178,axiom,
eq2(X,X) = btrue ).
cnf(axiom_179,axiom,
eq3(X,X) = btrue ).
cnf(axiom_180,axiom,
eq4(X,X) = btrue ).
cnf(goal,negated_conjecture,
eq4(prop1(X,Y),bfalse) != btrue ).
%------------------------------------------------------------------------------