TPTP Problem File: SWX208-1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX208-1 : TPTP v9.3.0. Released v9.3.0.
% Domain : Software Verification
% Problem : Find the inverse of a printing function
% Version : Especial.
% English :
% Refs : [CST26] Claessen et al. (2026), Email to Geoff Sutcliffe
% Source : [CST26]
% Names : Parse_prop3.p [CST26]
% Status : Unsatisfiable
% Rating : 1.00 v9.3.0
% Syntax : Number of clauses : 279 ( 273 unt; 0 nHn; 227 RR)
% Number of literals : 285 ( 285 equ; 7 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 14 ( 2 avg)
% Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% Number of functors : 46 ( 46 usr; 20 con; 0-3 aty)
% Number of variables : 108 ( 49 sgn)
% SPC : CNF_UNS_RFO_PEQ_NUE
% Comments :
%------------------------------------------------------------------------------
cnf(axiom,axiom,
aux(N,pair2(D1,N2)) = pair2(D1,s(N2)) ).
cnf(axiom_001,axiom,
aux2(X,left(D)) = pair2(D,z) ).
cnf(axiom_002,axiom,
aux2(X,right(N)) = aux(N,mod10(N)) ).
cnf(axiom_003,axiom,
aux3(X,Z,pair2(A1,N)) = showNumnum(cons(A1,X),N) ).
cnf(axiom_004,axiom,
impl(btrue,Q) = Q ).
cnf(axiom_005,axiom,
impl(bfalse,Q) = btrue ).
cnf(axiom_006,axiom,
append(nil,Y) = Y ).
cnf(axiom_007,axiom,
append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)) ).
cnf(axiom_008,axiom,
x2(z,z) = z ).
cnf(axiom_009,axiom,
x2(z,s(Z)) = z ).
cnf(axiom_010,axiom,
x2(s(N),z) = s(N) ).
cnf(axiom_011,axiom,
x2(s(N),s(M)) = x2(N,M) ).
cnf(axiom_012,axiom,
min10(z) = left(dIG0) ).
cnf(axiom_013,axiom,
min10(s(z)) = left(dIG1) ).
cnf(axiom_014,axiom,
min10(s(s(z))) = left(dIG2) ).
cnf(axiom_015,axiom,
min10(s(s(s(z)))) = left(dIG3) ).
cnf(axiom_016,axiom,
min10(s(s(s(s(z))))) = left(dIG4) ).
cnf(axiom_017,axiom,
min10(s(s(s(s(s(z)))))) = left(dIG5) ).
cnf(axiom_018,axiom,
min10(s(s(s(s(s(s(z))))))) = left(dIG6) ).
cnf(axiom_019,axiom,
min10(s(s(s(s(s(s(s(z)))))))) = left(dIG7) ).
cnf(axiom_020,axiom,
min10(s(s(s(s(s(s(s(s(z))))))))) = left(dIG8) ).
cnf(axiom_021,axiom,
min10(s(s(s(s(s(s(s(s(s(z)))))))))) = left(dIG9) ).
cnf(axiom_022,axiom,
min10(s(s(s(s(s(s(s(s(s(s(X9))))))))))) = right(x2(s(s(s(s(s(s(s(s(s(s(X9)))))))))),s(s(s(s(s(s(s(s(s(s(z)))))))))))) ).
cnf(axiom_023,axiom,
mod10(X) = aux2(X,min10(X)) ).
cnf(axiom_024,axiom,
showNumnum(X,z) = X ).
cnf(axiom_025,axiom,
showNumnum(X,s(Z)) = aux3(X,Z,mod10(s(Z))) ).
cnf(axiom_026,axiom,
showNum(z) = cons(dIG0,nil) ).
cnf(axiom_027,axiom,
showNum(s(Y)) = showNumnum(nil,s(Y)) ).
cnf(axiom_028,axiom,
show(x) = cons(cHARX,nil) ).
cnf(axiom_029,axiom,
show(add(B,C)) = append(show(B),append(cons(pLUS,nil),show(C))) ).
cnf(axiom_030,axiom,
show(mul(A3,B2)) = append(showF(A3),append(cons(mULT,nil),showF(B2))) ).
cnf(axiom_031,axiom,
show(num(N)) = showNum(N) ).
cnf(axiom_032,axiom,
showF(add(Y,Z)) = cons(pAR1,append(show(add(Y,Z)),cons(pAR2,nil))) ).
cnf(axiom_033,axiom,
showF(x) = show(x) ).
cnf(axiom_034,axiom,
showF(mul(X,X2)) = show(mul(X,X2)) ).
cnf(axiom_035,axiom,
showF(num(X)) = show(num(X)) ).
cnf(axiom_036,axiom,
prop3(X) = impl(eq(show(X),cons(pAR1,cons(pAR1,cons(cHARX,cons(pLUS,cons(dIG5,cons(pAR2,cons(pLUS,cons(dIG7,cons(pAR2,cons(mULT,cons(cHARX,nil)))))))))))),eq5(btrue,bfalse)) ).
cnf(axiom_037,axiom,
eq4(pAR1,pAR2) = bfalse ).
cnf(axiom_038,axiom,
eq4(pAR1,pLUS) = bfalse ).
cnf(axiom_039,axiom,
eq4(pAR1,mULT) = bfalse ).
cnf(axiom_040,axiom,
eq4(pAR1,cHARX) = bfalse ).
cnf(axiom_041,axiom,
eq4(pAR1,dIG0) = bfalse ).
cnf(axiom_042,axiom,
eq4(pAR1,dIG1) = bfalse ).
cnf(axiom_043,axiom,
eq4(pAR1,dIG2) = bfalse ).
cnf(axiom_044,axiom,
eq4(pAR1,dIG3) = bfalse ).
cnf(axiom_045,axiom,
eq4(pAR1,dIG4) = bfalse ).
cnf(axiom_046,axiom,
eq4(pAR1,dIG5) = bfalse ).
cnf(axiom_047,axiom,
eq4(pAR1,dIG6) = bfalse ).
cnf(axiom_048,axiom,
eq4(pAR1,dIG7) = bfalse ).
cnf(axiom_049,axiom,
eq4(pAR1,dIG8) = bfalse ).
cnf(axiom_050,axiom,
eq4(pAR1,dIG9) = bfalse ).
cnf(axiom_051,axiom,
eq4(pAR2,pAR1) = bfalse ).
cnf(axiom_052,axiom,
eq4(pAR2,pLUS) = bfalse ).
cnf(axiom_053,axiom,
eq4(pAR2,mULT) = bfalse ).
cnf(axiom_054,axiom,
eq4(pAR2,cHARX) = bfalse ).
cnf(axiom_055,axiom,
eq4(pAR2,dIG0) = bfalse ).
cnf(axiom_056,axiom,
eq4(pAR2,dIG1) = bfalse ).
cnf(axiom_057,axiom,
eq4(pAR2,dIG2) = bfalse ).
cnf(axiom_058,axiom,
eq4(pAR2,dIG3) = bfalse ).
cnf(axiom_059,axiom,
eq4(pAR2,dIG4) = bfalse ).
cnf(axiom_060,axiom,
eq4(pAR2,dIG5) = bfalse ).
cnf(axiom_061,axiom,
eq4(pAR2,dIG6) = bfalse ).
cnf(axiom_062,axiom,
eq4(pAR2,dIG7) = bfalse ).
cnf(axiom_063,axiom,
eq4(pAR2,dIG8) = bfalse ).
cnf(axiom_064,axiom,
eq4(pAR2,dIG9) = bfalse ).
cnf(axiom_065,axiom,
eq4(pLUS,pAR1) = bfalse ).
cnf(axiom_066,axiom,
eq4(pLUS,pAR2) = bfalse ).
cnf(axiom_067,axiom,
eq4(pLUS,mULT) = bfalse ).
cnf(axiom_068,axiom,
eq4(pLUS,cHARX) = bfalse ).
cnf(axiom_069,axiom,
eq4(pLUS,dIG0) = bfalse ).
cnf(axiom_070,axiom,
eq4(pLUS,dIG1) = bfalse ).
cnf(axiom_071,axiom,
eq4(pLUS,dIG2) = bfalse ).
cnf(axiom_072,axiom,
eq4(pLUS,dIG3) = bfalse ).
cnf(axiom_073,axiom,
eq4(pLUS,dIG4) = bfalse ).
cnf(axiom_074,axiom,
eq4(pLUS,dIG5) = bfalse ).
cnf(axiom_075,axiom,
eq4(pLUS,dIG6) = bfalse ).
cnf(axiom_076,axiom,
eq4(pLUS,dIG7) = bfalse ).
cnf(axiom_077,axiom,
eq4(pLUS,dIG8) = bfalse ).
cnf(axiom_078,axiom,
eq4(pLUS,dIG9) = bfalse ).
cnf(axiom_079,axiom,
eq4(mULT,pAR1) = bfalse ).
cnf(axiom_080,axiom,
eq4(mULT,pAR2) = bfalse ).
cnf(axiom_081,axiom,
eq4(mULT,pLUS) = bfalse ).
cnf(axiom_082,axiom,
eq4(mULT,cHARX) = bfalse ).
cnf(axiom_083,axiom,
eq4(mULT,dIG0) = bfalse ).
cnf(axiom_084,axiom,
eq4(mULT,dIG1) = bfalse ).
cnf(axiom_085,axiom,
eq4(mULT,dIG2) = bfalse ).
cnf(axiom_086,axiom,
eq4(mULT,dIG3) = bfalse ).
cnf(axiom_087,axiom,
eq4(mULT,dIG4) = bfalse ).
cnf(axiom_088,axiom,
eq4(mULT,dIG5) = bfalse ).
cnf(axiom_089,axiom,
eq4(mULT,dIG6) = bfalse ).
cnf(axiom_090,axiom,
eq4(mULT,dIG7) = bfalse ).
cnf(axiom_091,axiom,
eq4(mULT,dIG8) = bfalse ).
cnf(axiom_092,axiom,
eq4(mULT,dIG9) = bfalse ).
cnf(axiom_093,axiom,
eq4(cHARX,pAR1) = bfalse ).
cnf(axiom_094,axiom,
eq4(cHARX,pAR2) = bfalse ).
cnf(axiom_095,axiom,
eq4(cHARX,pLUS) = bfalse ).
cnf(axiom_096,axiom,
eq4(cHARX,mULT) = bfalse ).
cnf(axiom_097,axiom,
eq4(cHARX,dIG0) = bfalse ).
cnf(axiom_098,axiom,
eq4(cHARX,dIG1) = bfalse ).
cnf(axiom_099,axiom,
eq4(cHARX,dIG2) = bfalse ).
cnf(axiom_100,axiom,
eq4(cHARX,dIG3) = bfalse ).
cnf(axiom_101,axiom,
eq4(cHARX,dIG4) = bfalse ).
cnf(axiom_102,axiom,
eq4(cHARX,dIG5) = bfalse ).
cnf(axiom_103,axiom,
eq4(cHARX,dIG6) = bfalse ).
cnf(axiom_104,axiom,
eq4(cHARX,dIG7) = bfalse ).
cnf(axiom_105,axiom,
eq4(cHARX,dIG8) = bfalse ).
cnf(axiom_106,axiom,
eq4(cHARX,dIG9) = bfalse ).
cnf(axiom_107,axiom,
eq4(dIG0,pAR1) = bfalse ).
cnf(axiom_108,axiom,
eq4(dIG0,pAR2) = bfalse ).
cnf(axiom_109,axiom,
eq4(dIG0,pLUS) = bfalse ).
cnf(axiom_110,axiom,
eq4(dIG0,mULT) = bfalse ).
cnf(axiom_111,axiom,
eq4(dIG0,cHARX) = bfalse ).
cnf(axiom_112,axiom,
eq4(dIG0,dIG1) = bfalse ).
cnf(axiom_113,axiom,
eq4(dIG0,dIG2) = bfalse ).
cnf(axiom_114,axiom,
eq4(dIG0,dIG3) = bfalse ).
cnf(axiom_115,axiom,
eq4(dIG0,dIG4) = bfalse ).
cnf(axiom_116,axiom,
eq4(dIG0,dIG5) = bfalse ).
cnf(axiom_117,axiom,
eq4(dIG0,dIG6) = bfalse ).
cnf(axiom_118,axiom,
eq4(dIG0,dIG7) = bfalse ).
cnf(axiom_119,axiom,
eq4(dIG0,dIG8) = bfalse ).
cnf(axiom_120,axiom,
eq4(dIG0,dIG9) = bfalse ).
cnf(axiom_121,axiom,
eq4(dIG1,pAR1) = bfalse ).
cnf(axiom_122,axiom,
eq4(dIG1,pAR2) = bfalse ).
cnf(axiom_123,axiom,
eq4(dIG1,pLUS) = bfalse ).
cnf(axiom_124,axiom,
eq4(dIG1,mULT) = bfalse ).
cnf(axiom_125,axiom,
eq4(dIG1,cHARX) = bfalse ).
cnf(axiom_126,axiom,
eq4(dIG1,dIG0) = bfalse ).
cnf(axiom_127,axiom,
eq4(dIG1,dIG2) = bfalse ).
cnf(axiom_128,axiom,
eq4(dIG1,dIG3) = bfalse ).
cnf(axiom_129,axiom,
eq4(dIG1,dIG4) = bfalse ).
cnf(axiom_130,axiom,
eq4(dIG1,dIG5) = bfalse ).
cnf(axiom_131,axiom,
eq4(dIG1,dIG6) = bfalse ).
cnf(axiom_132,axiom,
eq4(dIG1,dIG7) = bfalse ).
cnf(axiom_133,axiom,
eq4(dIG1,dIG8) = bfalse ).
cnf(axiom_134,axiom,
eq4(dIG1,dIG9) = bfalse ).
cnf(axiom_135,axiom,
eq4(dIG2,pAR1) = bfalse ).
cnf(axiom_136,axiom,
eq4(dIG2,pAR2) = bfalse ).
cnf(axiom_137,axiom,
eq4(dIG2,pLUS) = bfalse ).
cnf(axiom_138,axiom,
eq4(dIG2,mULT) = bfalse ).
cnf(axiom_139,axiom,
eq4(dIG2,cHARX) = bfalse ).
cnf(axiom_140,axiom,
eq4(dIG2,dIG0) = bfalse ).
cnf(axiom_141,axiom,
eq4(dIG2,dIG1) = bfalse ).
cnf(axiom_142,axiom,
eq4(dIG2,dIG3) = bfalse ).
cnf(axiom_143,axiom,
eq4(dIG2,dIG4) = bfalse ).
cnf(axiom_144,axiom,
eq4(dIG2,dIG5) = bfalse ).
cnf(axiom_145,axiom,
eq4(dIG2,dIG6) = bfalse ).
cnf(axiom_146,axiom,
eq4(dIG2,dIG7) = bfalse ).
cnf(axiom_147,axiom,
eq4(dIG2,dIG8) = bfalse ).
cnf(axiom_148,axiom,
eq4(dIG2,dIG9) = bfalse ).
cnf(axiom_149,axiom,
eq4(dIG3,pAR1) = bfalse ).
cnf(axiom_150,axiom,
eq4(dIG3,pAR2) = bfalse ).
cnf(axiom_151,axiom,
eq4(dIG3,pLUS) = bfalse ).
cnf(axiom_152,axiom,
eq4(dIG3,mULT) = bfalse ).
cnf(axiom_153,axiom,
eq4(dIG3,cHARX) = bfalse ).
cnf(axiom_154,axiom,
eq4(dIG3,dIG0) = bfalse ).
cnf(axiom_155,axiom,
eq4(dIG3,dIG1) = bfalse ).
cnf(axiom_156,axiom,
eq4(dIG3,dIG2) = bfalse ).
cnf(axiom_157,axiom,
eq4(dIG3,dIG4) = bfalse ).
cnf(axiom_158,axiom,
eq4(dIG3,dIG5) = bfalse ).
cnf(axiom_159,axiom,
eq4(dIG3,dIG6) = bfalse ).
cnf(axiom_160,axiom,
eq4(dIG3,dIG7) = bfalse ).
cnf(axiom_161,axiom,
eq4(dIG3,dIG8) = bfalse ).
cnf(axiom_162,axiom,
eq4(dIG3,dIG9) = bfalse ).
cnf(axiom_163,axiom,
eq4(dIG4,pAR1) = bfalse ).
cnf(axiom_164,axiom,
eq4(dIG4,pAR2) = bfalse ).
cnf(axiom_165,axiom,
eq4(dIG4,pLUS) = bfalse ).
cnf(axiom_166,axiom,
eq4(dIG4,mULT) = bfalse ).
cnf(axiom_167,axiom,
eq4(dIG4,cHARX) = bfalse ).
cnf(axiom_168,axiom,
eq4(dIG4,dIG0) = bfalse ).
cnf(axiom_169,axiom,
eq4(dIG4,dIG1) = bfalse ).
cnf(axiom_170,axiom,
eq4(dIG4,dIG2) = bfalse ).
cnf(axiom_171,axiom,
eq4(dIG4,dIG3) = bfalse ).
cnf(axiom_172,axiom,
eq4(dIG4,dIG5) = bfalse ).
cnf(axiom_173,axiom,
eq4(dIG4,dIG6) = bfalse ).
cnf(axiom_174,axiom,
eq4(dIG4,dIG7) = bfalse ).
cnf(axiom_175,axiom,
eq4(dIG4,dIG8) = bfalse ).
cnf(axiom_176,axiom,
eq4(dIG4,dIG9) = bfalse ).
cnf(axiom_177,axiom,
eq4(dIG5,pAR1) = bfalse ).
cnf(axiom_178,axiom,
eq4(dIG5,pAR2) = bfalse ).
cnf(axiom_179,axiom,
eq4(dIG5,pLUS) = bfalse ).
cnf(axiom_180,axiom,
eq4(dIG5,mULT) = bfalse ).
cnf(axiom_181,axiom,
eq4(dIG5,cHARX) = bfalse ).
cnf(axiom_182,axiom,
eq4(dIG5,dIG0) = bfalse ).
cnf(axiom_183,axiom,
eq4(dIG5,dIG1) = bfalse ).
cnf(axiom_184,axiom,
eq4(dIG5,dIG2) = bfalse ).
cnf(axiom_185,axiom,
eq4(dIG5,dIG3) = bfalse ).
cnf(axiom_186,axiom,
eq4(dIG5,dIG4) = bfalse ).
cnf(axiom_187,axiom,
eq4(dIG5,dIG6) = bfalse ).
cnf(axiom_188,axiom,
eq4(dIG5,dIG7) = bfalse ).
cnf(axiom_189,axiom,
eq4(dIG5,dIG8) = bfalse ).
cnf(axiom_190,axiom,
eq4(dIG5,dIG9) = bfalse ).
cnf(axiom_191,axiom,
eq4(dIG6,pAR1) = bfalse ).
cnf(axiom_192,axiom,
eq4(dIG6,pAR2) = bfalse ).
cnf(axiom_193,axiom,
eq4(dIG6,pLUS) = bfalse ).
cnf(axiom_194,axiom,
eq4(dIG6,mULT) = bfalse ).
cnf(axiom_195,axiom,
eq4(dIG6,cHARX) = bfalse ).
cnf(axiom_196,axiom,
eq4(dIG6,dIG0) = bfalse ).
cnf(axiom_197,axiom,
eq4(dIG6,dIG1) = bfalse ).
cnf(axiom_198,axiom,
eq4(dIG6,dIG2) = bfalse ).
cnf(axiom_199,axiom,
eq4(dIG6,dIG3) = bfalse ).
cnf(axiom_200,axiom,
eq4(dIG6,dIG4) = bfalse ).
cnf(axiom_201,axiom,
eq4(dIG6,dIG5) = bfalse ).
cnf(axiom_202,axiom,
eq4(dIG6,dIG7) = bfalse ).
cnf(axiom_203,axiom,
eq4(dIG6,dIG8) = bfalse ).
cnf(axiom_204,axiom,
eq4(dIG6,dIG9) = bfalse ).
cnf(axiom_205,axiom,
eq4(dIG7,pAR1) = bfalse ).
cnf(axiom_206,axiom,
eq4(dIG7,pAR2) = bfalse ).
cnf(axiom_207,axiom,
eq4(dIG7,pLUS) = bfalse ).
cnf(axiom_208,axiom,
eq4(dIG7,mULT) = bfalse ).
cnf(axiom_209,axiom,
eq4(dIG7,cHARX) = bfalse ).
cnf(axiom_210,axiom,
eq4(dIG7,dIG0) = bfalse ).
cnf(axiom_211,axiom,
eq4(dIG7,dIG1) = bfalse ).
cnf(axiom_212,axiom,
eq4(dIG7,dIG2) = bfalse ).
cnf(axiom_213,axiom,
eq4(dIG7,dIG3) = bfalse ).
cnf(axiom_214,axiom,
eq4(dIG7,dIG4) = bfalse ).
cnf(axiom_215,axiom,
eq4(dIG7,dIG5) = bfalse ).
cnf(axiom_216,axiom,
eq4(dIG7,dIG6) = bfalse ).
cnf(axiom_217,axiom,
eq4(dIG7,dIG8) = bfalse ).
cnf(axiom_218,axiom,
eq4(dIG7,dIG9) = bfalse ).
cnf(axiom_219,axiom,
eq4(dIG8,pAR1) = bfalse ).
cnf(axiom_220,axiom,
eq4(dIG8,pAR2) = bfalse ).
cnf(axiom_221,axiom,
eq4(dIG8,pLUS) = bfalse ).
cnf(axiom_222,axiom,
eq4(dIG8,mULT) = bfalse ).
cnf(axiom_223,axiom,
eq4(dIG8,cHARX) = bfalse ).
cnf(axiom_224,axiom,
eq4(dIG8,dIG0) = bfalse ).
cnf(axiom_225,axiom,
eq4(dIG8,dIG1) = bfalse ).
cnf(axiom_226,axiom,
eq4(dIG8,dIG2) = bfalse ).
cnf(axiom_227,axiom,
eq4(dIG8,dIG3) = bfalse ).
cnf(axiom_228,axiom,
eq4(dIG8,dIG4) = bfalse ).
cnf(axiom_229,axiom,
eq4(dIG8,dIG5) = bfalse ).
cnf(axiom_230,axiom,
eq4(dIG8,dIG6) = bfalse ).
cnf(axiom_231,axiom,
eq4(dIG8,dIG7) = bfalse ).
cnf(axiom_232,axiom,
eq4(dIG8,dIG9) = bfalse ).
cnf(axiom_233,axiom,
eq4(dIG9,pAR1) = bfalse ).
cnf(axiom_234,axiom,
eq4(dIG9,pAR2) = bfalse ).
cnf(axiom_235,axiom,
eq4(dIG9,pLUS) = bfalse ).
cnf(axiom_236,axiom,
eq4(dIG9,mULT) = bfalse ).
cnf(axiom_237,axiom,
eq4(dIG9,cHARX) = bfalse ).
cnf(axiom_238,axiom,
eq4(dIG9,dIG0) = bfalse ).
cnf(axiom_239,axiom,
eq4(dIG9,dIG1) = bfalse ).
cnf(axiom_240,axiom,
eq4(dIG9,dIG2) = bfalse ).
cnf(axiom_241,axiom,
eq4(dIG9,dIG3) = bfalse ).
cnf(axiom_242,axiom,
eq4(dIG9,dIG4) = bfalse ).
cnf(axiom_243,axiom,
eq4(dIG9,dIG5) = bfalse ).
cnf(axiom_244,axiom,
eq4(dIG9,dIG6) = bfalse ).
cnf(axiom_245,axiom,
eq4(dIG9,dIG7) = bfalse ).
cnf(axiom_246,axiom,
eq4(dIG9,dIG8) = bfalse ).
cnf(axiom_247,axiom,
eq5(bfalse,btrue) = bfalse ).
cnf(axiom_248,axiom,
eq5(btrue,bfalse) = bfalse ).
cnf(axiom_249,axiom,
( eq3(X,Z) != bfalse
| eq3(add(X,Y),add(Z,X2)) = bfalse ) ).
cnf(axiom_250,axiom,
( eq3(X,Z) != btrue
| eq3(add(X,Y),add(Z,X2)) = eq3(Y,X2) ) ).
cnf(axiom_251,axiom,
( eq3(X,Z) != bfalse
| eq3(mul(X,Y),mul(Z,X2)) = bfalse ) ).
cnf(axiom_252,axiom,
( eq3(X,Z) != btrue
| eq3(mul(X,Y),mul(Z,X2)) = eq3(Y,X2) ) ).
cnf(axiom_253,axiom,
eq3(num(X),num(Y)) = eq2(X,Y) ).
cnf(axiom_254,axiom,
eq3(x,add(X,Y)) = bfalse ).
cnf(axiom_255,axiom,
eq3(x,mul(X,Y)) = bfalse ).
cnf(axiom_256,axiom,
eq3(x,num(X)) = bfalse ).
cnf(axiom_257,axiom,
eq3(add(X,Y),x) = bfalse ).
cnf(axiom_258,axiom,
eq3(add(X,Y),mul(Z,X2)) = bfalse ).
cnf(axiom_259,axiom,
eq3(add(X,Y),num(Z)) = bfalse ).
cnf(axiom_260,axiom,
eq3(mul(X,Y),x) = bfalse ).
cnf(axiom_261,axiom,
eq3(mul(X,Y),add(Z,X2)) = bfalse ).
cnf(axiom_262,axiom,
eq3(mul(X,Y),num(Z)) = bfalse ).
cnf(axiom_263,axiom,
eq3(num(X),x) = bfalse ).
cnf(axiom_264,axiom,
eq3(num(X),add(Y,Z)) = bfalse ).
cnf(axiom_265,axiom,
eq3(num(X),mul(Y,Z)) = bfalse ).
cnf(axiom_266,axiom,
eq2(s(X),s(Y)) = eq2(X,Y) ).
cnf(axiom_267,axiom,
eq2(z,s(X)) = bfalse ).
cnf(axiom_268,axiom,
eq2(s(X),z) = bfalse ).
cnf(axiom_269,axiom,
eq(X,X) = btrue ).
cnf(axiom_270,axiom,
eq2(X,X) = btrue ).
cnf(axiom_271,axiom,
eq3(X,X) = btrue ).
cnf(axiom_272,axiom,
eq4(X,X) = btrue ).
cnf(axiom_273,axiom,
eq5(X,X) = btrue ).
cnf(axiom_274,axiom,
( eq4(X,Z) != bfalse
| eq(cons(X,Y),cons(Z,X2)) = bfalse ) ).
cnf(axiom_275,axiom,
( eq4(X,Z) != btrue
| eq(cons(X,Y),cons(Z,X2)) = eq(Y,X2) ) ).
cnf(axiom_276,axiom,
eq(nil,cons(X,Y)) = bfalse ).
cnf(axiom_277,axiom,
eq(cons(X,Y),nil) = bfalse ).
cnf(goal,negated_conjecture,
eq5(prop3(X),bfalse) != btrue ).
%------------------------------------------------------------------------------