%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV543-1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:23:28 PM UTC 2026
% Result : Unsatisfiable 8.06s 1.62s
% Output : CNFRefutation 8.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 79
% Syntax : Number of formulae : 253 ( 253 unt; 0 def)
% Number of atoms : 253 ( 252 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 89 ( 89 usr; 87 con; 0-3 aty)
% Number of variables : 21 ( 0 sgn 21 !; 0 ?; 15 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1) ).
fof(f3,axiom,
! [X2,X0,X1] : store(store(X0,X1,select(X0,X2)),X2,select(X0,X1)) = store(store(X0,X2,select(X0,X1)),X1,select(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a3) ).
fof(f4,axiom,
a_1245 = store(a1,i8,e_1244),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp0) ).
fof(f5,axiom,
a_1247 = store(a_1245,i7,e_1246),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp1) ).
fof(f6,axiom,
a_1249 = store(a_1247,i6,e_1248),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp2) ).
fof(f7,axiom,
a_1251 = store(a_1249,i8,e_1250),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp3) ).
fof(f8,axiom,
a_1253 = store(a_1251,i8,e_1252),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp4) ).
fof(f9,axiom,
a_1255 = store(a_1253,i5,e_1254),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp5) ).
fof(f10,axiom,
a_1257 = store(a_1255,i4,e_1256),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp6) ).
fof(f11,axiom,
a_1259 = store(a_1257,i9,e_1258),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp7) ).
fof(f12,axiom,
a_1261 = store(a_1259,i7,e_1260),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp8) ).
fof(f13,axiom,
a_1263 = store(a_1261,i1,e_1262),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp9) ).
fof(f14,axiom,
a_1265 = store(a_1263,i4,e_1264),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp10) ).
fof(f15,axiom,
a_1267 = store(a_1265,i5,e_1266),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp11) ).
fof(f16,axiom,
a_1269 = store(a_1267,i0,e_1268),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp12) ).
fof(f17,axiom,
a_1270 = store(a_1269,i0,e_1268),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp13) ).
fof(f18,axiom,
a_1272 = store(a_1270,i1,e_1271),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp14) ).
fof(f19,axiom,
a_1274 = store(a_1272,i2,e_1273),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp15) ).
fof(f20,axiom,
a_1276 = store(a_1274,i3,e_1275),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp16) ).
fof(f21,axiom,
a_1278 = store(a_1276,i0,e_1277),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp17) ).
fof(f22,axiom,
a_1280 = store(a_1278,i9,e_1279),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp18) ).
fof(f23,axiom,
a_1282 = store(a_1280,i5,e_1281),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp19) ).
fof(f24,axiom,
a_1283 = store(a1,i7,e_1246),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp20) ).
fof(f25,axiom,
a_1284 = store(a_1283,i8,e_1244),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp21) ).
fof(f26,axiom,
a_1286 = store(a_1284,i6,e_1285),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp22) ).
fof(f27,axiom,
a_1288 = store(a_1286,i8,e_1287),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp23) ).
fof(f28,axiom,
a_1290 = store(a_1288,i5,e_1289),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp24) ).
fof(f29,axiom,
a_1292 = store(a_1290,i8,e_1291),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp25) ).
fof(f30,axiom,
a_1294 = store(a_1292,i4,e_1293),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp26) ).
fof(f31,axiom,
a_1296 = store(a_1294,i9,e_1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp27) ).
fof(f32,axiom,
a_1298 = store(a_1296,i1,e_1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp28) ).
fof(f33,axiom,
a_1300 = store(a_1298,i7,e_1299),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp29) ).
fof(f34,axiom,
a_1302 = store(a_1300,i4,e_1301),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp30) ).
fof(f35,axiom,
a_1304 = store(a_1302,i5,e_1303),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp31) ).
fof(f36,axiom,
a_1306 = store(a_1304,i0,e_1305),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp32) ).
fof(f37,axiom,
a_1307 = store(a_1306,i0,e_1305),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp33) ).
fof(f38,axiom,
a_1309 = store(a_1307,i2,e_1308),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp34) ).
fof(f39,axiom,
a_1311 = store(a_1309,i1,e_1310),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp35) ).
fof(f40,axiom,
a_1313 = store(a_1311,i3,e_1312),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp36) ).
fof(f41,axiom,
a_1315 = store(a_1313,i0,e_1314),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp37) ).
fof(f42,axiom,
a_1317 = store(a_1315,i5,e_1316),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp38) ).
fof(f43,axiom,
a_1319 = store(a_1317,i9,e_1318),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp39) ).
fof(f44,axiom,
e_1244 = select(a1,i7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp40) ).
fof(f45,axiom,
e_1246 = select(a1,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp41) ).
fof(f46,axiom,
e_1248 = select(a_1247,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp42) ).
fof(f47,axiom,
e_1250 = select(a_1247,i6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp43) ).
fof(f48,axiom,
e_1252 = select(a_1251,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp44) ).
fof(f49,axiom,
e_1254 = select(a_1251,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp45) ).
fof(f50,axiom,
e_1256 = select(a_1255,i9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp46) ).
fof(f51,axiom,
e_1258 = select(a_1255,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp47) ).
fof(f52,axiom,
e_1260 = select(a_1259,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp48) ).
fof(f53,axiom,
e_1262 = select(a_1259,i7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp49) ).
fof(f54,axiom,
e_1264 = select(a_1263,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp50) ).
fof(f55,axiom,
e_1266 = select(a_1263,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp51) ).
fof(f56,axiom,
e_1268 = select(a_1267,i0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp52) ).
fof(f57,axiom,
e_1271 = select(a_1270,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp53) ).
fof(f58,axiom,
e_1273 = select(a_1270,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp54) ).
fof(f59,axiom,
e_1275 = select(a_1274,i0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp55) ).
fof(f60,axiom,
e_1277 = select(a_1274,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp56) ).
fof(f61,axiom,
e_1279 = select(a_1278,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp57) ).
fof(f62,axiom,
e_1281 = select(a_1278,i9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp58) ).
fof(f63,axiom,
e_1285 = select(a_1284,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp59) ).
fof(f64,axiom,
e_1287 = select(a_1284,i6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp60) ).
fof(f65,axiom,
e_1289 = select(a_1288,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp61) ).
fof(f66,axiom,
e_1291 = select(a_1288,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp62) ).
fof(f67,axiom,
e_1293 = select(a_1292,i9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp63) ).
fof(f68,axiom,
e_1295 = select(a_1292,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp64) ).
fof(f69,axiom,
e_1297 = select(a_1296,i7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp65) ).
fof(f70,axiom,
e_1299 = select(a_1296,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp66) ).
fof(f71,axiom,
e_1301 = select(a_1300,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp67) ).
fof(f72,axiom,
e_1303 = select(a_1300,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp68) ).
fof(f73,axiom,
e_1305 = select(a_1304,i0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp69) ).
fof(f74,axiom,
e_1308 = select(a_1307,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp70) ).
fof(f75,axiom,
e_1310 = select(a_1307,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp71) ).
fof(f76,axiom,
e_1312 = select(a_1311,i0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp72) ).
fof(f77,axiom,
e_1314 = select(a_1311,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp73) ).
fof(f78,axiom,
e_1316 = select(a_1315,i9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp74) ).
fof(f79,axiom,
e_1318 = select(a_1315,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp75) ).
fof(f80,negated_conjecture,
a_1282 != a_1319,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
tcf(c_129,plain,
! [X0: $i,X1: $i,X2: $i] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[],[f1]) ).
tcf(c_131,plain,
! [X0: $i,X1: $i,X2: $i] : store(store(X0,X1,select(X0,X2)),X2,select(X0,X1)) = store(store(X0,X2,select(X0,X1)),X1,select(X0,X2)),
inference(cnf_transformation,[],[f3]) ).
tcf(c_132,plain,
store(a1,i8,e_1244) = a_1245,
inference(cnf_transformation,[],[f4]) ).
tcf(c_133,plain,
store(a_1245,i7,e_1246) = a_1247,
inference(cnf_transformation,[],[f5]) ).
tcf(c_134,plain,
store(a_1247,i6,e_1248) = a_1249,
inference(cnf_transformation,[],[f6]) ).
tcf(c_135,plain,
store(a_1249,i8,e_1250) = a_1251,
inference(cnf_transformation,[],[f7]) ).
tcf(c_136,plain,
store(a_1251,i8,e_1252) = a_1253,
inference(cnf_transformation,[],[f8]) ).
tcf(c_137,plain,
store(a_1253,i5,e_1254) = a_1255,
inference(cnf_transformation,[],[f9]) ).
tcf(c_138,plain,
store(a_1255,i4,e_1256) = a_1257,
inference(cnf_transformation,[],[f10]) ).
tcf(c_139,plain,
store(a_1257,i9,e_1258) = a_1259,
inference(cnf_transformation,[],[f11]) ).
tcf(c_140,plain,
store(a_1259,i7,e_1260) = a_1261,
inference(cnf_transformation,[],[f12]) ).
tcf(c_141,plain,
store(a_1261,i1,e_1262) = a_1263,
inference(cnf_transformation,[],[f13]) ).
tcf(c_142,plain,
store(a_1263,i4,e_1264) = a_1265,
inference(cnf_transformation,[],[f14]) ).
tcf(c_143,plain,
store(a_1265,i5,e_1266) = a_1267,
inference(cnf_transformation,[],[f15]) ).
tcf(c_144,plain,
store(a_1267,i0,e_1268) = a_1269,
inference(cnf_transformation,[],[f16]) ).
tcf(c_145,plain,
store(a_1269,i0,e_1268) = a_1270,
inference(cnf_transformation,[],[f17]) ).
tcf(c_146,plain,
store(a_1270,i1,e_1271) = a_1272,
inference(cnf_transformation,[],[f18]) ).
tcf(c_147,plain,
store(a_1272,i2,e_1273) = a_1274,
inference(cnf_transformation,[],[f19]) ).
tcf(c_148,plain,
store(a_1274,i3,e_1275) = a_1276,
inference(cnf_transformation,[],[f20]) ).
tcf(c_149,plain,
store(a_1276,i0,e_1277) = a_1278,
inference(cnf_transformation,[],[f21]) ).
tcf(c_150,plain,
store(a_1278,i9,e_1279) = a_1280,
inference(cnf_transformation,[],[f22]) ).
tcf(c_151,plain,
store(a_1280,i5,e_1281) = a_1282,
inference(cnf_transformation,[],[f23]) ).
tcf(c_152,plain,
store(a1,i7,e_1246) = a_1283,
inference(cnf_transformation,[],[f24]) ).
tcf(c_153,plain,
store(a_1283,i8,e_1244) = a_1284,
inference(cnf_transformation,[],[f25]) ).
tcf(c_154,plain,
store(a_1284,i6,e_1285) = a_1286,
inference(cnf_transformation,[],[f26]) ).
tcf(c_155,plain,
store(a_1286,i8,e_1287) = a_1288,
inference(cnf_transformation,[],[f27]) ).
tcf(c_156,plain,
store(a_1288,i5,e_1289) = a_1290,
inference(cnf_transformation,[],[f28]) ).
tcf(c_157,plain,
store(a_1290,i8,e_1291) = a_1292,
inference(cnf_transformation,[],[f29]) ).
tcf(c_158,plain,
store(a_1292,i4,e_1293) = a_1294,
inference(cnf_transformation,[],[f30]) ).
tcf(c_159,plain,
store(a_1294,i9,e_1295) = a_1296,
inference(cnf_transformation,[],[f31]) ).
tcf(c_160,plain,
store(a_1296,i1,e_1297) = a_1298,
inference(cnf_transformation,[],[f32]) ).
tcf(c_161,plain,
store(a_1298,i7,e_1299) = a_1300,
inference(cnf_transformation,[],[f33]) ).
tcf(c_162,plain,
store(a_1300,i4,e_1301) = a_1302,
inference(cnf_transformation,[],[f34]) ).
tcf(c_163,plain,
store(a_1302,i5,e_1303) = a_1304,
inference(cnf_transformation,[],[f35]) ).
tcf(c_164,plain,
store(a_1304,i0,e_1305) = a_1306,
inference(cnf_transformation,[],[f36]) ).
tcf(c_165,plain,
store(a_1306,i0,e_1305) = a_1307,
inference(cnf_transformation,[],[f37]) ).
tcf(c_166,plain,
store(a_1307,i2,e_1308) = a_1309,
inference(cnf_transformation,[],[f38]) ).
tcf(c_167,plain,
store(a_1309,i1,e_1310) = a_1311,
inference(cnf_transformation,[],[f39]) ).
tcf(c_168,plain,
store(a_1311,i3,e_1312) = a_1313,
inference(cnf_transformation,[],[f40]) ).
tcf(c_169,plain,
store(a_1313,i0,e_1314) = a_1315,
inference(cnf_transformation,[],[f41]) ).
tcf(c_170,plain,
store(a_1315,i5,e_1316) = a_1317,
inference(cnf_transformation,[],[f42]) ).
tcf(c_171,plain,
store(a_1317,i9,e_1318) = a_1319,
inference(cnf_transformation,[],[f43]) ).
tcf(c_172,plain,
select(a1,i7) = e_1244,
inference(cnf_transformation,[],[f44]) ).
tcf(c_173,plain,
select(a1,i8) = e_1246,
inference(cnf_transformation,[],[f45]) ).
tcf(c_174,plain,
select(a_1247,i8) = e_1248,
inference(cnf_transformation,[],[f46]) ).
tcf(c_175,plain,
select(a_1247,i6) = e_1250,
inference(cnf_transformation,[],[f47]) ).
tcf(c_176,plain,
select(a_1251,i5) = e_1252,
inference(cnf_transformation,[],[f48]) ).
tcf(c_177,plain,
select(a_1251,i8) = e_1254,
inference(cnf_transformation,[],[f49]) ).
tcf(c_178,plain,
select(a_1255,i9) = e_1256,
inference(cnf_transformation,[],[f50]) ).
tcf(c_179,plain,
select(a_1255,i4) = e_1258,
inference(cnf_transformation,[],[f51]) ).
tcf(c_180,plain,
select(a_1259,i1) = e_1260,
inference(cnf_transformation,[],[f52]) ).
tcf(c_181,plain,
select(a_1259,i7) = e_1262,
inference(cnf_transformation,[],[f53]) ).
tcf(c_182,plain,
select(a_1263,i5) = e_1264,
inference(cnf_transformation,[],[f54]) ).
tcf(c_183,plain,
select(a_1263,i4) = e_1266,
inference(cnf_transformation,[],[f55]) ).
tcf(c_184,plain,
select(a_1267,i0) = e_1268,
inference(cnf_transformation,[],[f56]) ).
tcf(c_185,plain,
select(a_1270,i2) = e_1271,
inference(cnf_transformation,[],[f57]) ).
tcf(c_186,plain,
select(a_1270,i1) = e_1273,
inference(cnf_transformation,[],[f58]) ).
tcf(c_187,plain,
select(a_1274,i0) = e_1275,
inference(cnf_transformation,[],[f59]) ).
tcf(c_188,plain,
select(a_1274,i3) = e_1277,
inference(cnf_transformation,[],[f60]) ).
tcf(c_189,plain,
select(a_1278,i5) = e_1279,
inference(cnf_transformation,[],[f61]) ).
tcf(c_190,plain,
select(a_1278,i9) = e_1281,
inference(cnf_transformation,[],[f62]) ).
tcf(c_191,plain,
select(a_1284,i8) = e_1285,
inference(cnf_transformation,[],[f63]) ).
tcf(c_192,plain,
select(a_1284,i6) = e_1287,
inference(cnf_transformation,[],[f64]) ).
tcf(c_193,plain,
select(a_1288,i8) = e_1289,
inference(cnf_transformation,[],[f65]) ).
tcf(c_194,plain,
select(a_1288,i5) = e_1291,
inference(cnf_transformation,[],[f66]) ).
tcf(c_195,plain,
select(a_1292,i9) = e_1293,
inference(cnf_transformation,[],[f67]) ).
tcf(c_196,plain,
select(a_1292,i4) = e_1295,
inference(cnf_transformation,[],[f68]) ).
tcf(c_197,plain,
select(a_1296,i7) = e_1297,
inference(cnf_transformation,[],[f69]) ).
tcf(c_198,plain,
select(a_1296,i1) = e_1299,
inference(cnf_transformation,[],[f70]) ).
tcf(c_199,plain,
select(a_1300,i5) = e_1301,
inference(cnf_transformation,[],[f71]) ).
tcf(c_200,plain,
select(a_1300,i4) = e_1303,
inference(cnf_transformation,[],[f72]) ).
tcf(c_201,plain,
select(a_1304,i0) = e_1305,
inference(cnf_transformation,[],[f73]) ).
tcf(c_202,plain,
select(a_1307,i1) = e_1308,
inference(cnf_transformation,[],[f74]) ).
tcf(c_203,plain,
select(a_1307,i2) = e_1310,
inference(cnf_transformation,[],[f75]) ).
tcf(c_204,plain,
select(a_1311,i0) = e_1312,
inference(cnf_transformation,[],[f76]) ).
tcf(c_205,plain,
select(a_1311,i3) = e_1314,
inference(cnf_transformation,[],[f77]) ).
tcf(c_206,plain,
select(a_1315,i9) = e_1316,
inference(cnf_transformation,[],[f78]) ).
tcf(c_207,plain,
select(a_1315,i5) = e_1318,
inference(cnf_transformation,[],[f79]) ).
tcf(c_208,negated_conjecture,
a_1282 != a_1319,
inference(cnf_transformation,[],[f80]) ).
tcf(c_380,negated_conjecture,
a_1282 != a_1319,
inference(demodulation,[status(thm)],[c_208]) ).
tcf(c_577,plain,
select(a_1251,i8) = e_1250,
inference(superposition,[status(thm)],[c_135,c_129]) ).
tcf(c_578,plain,
e_1250 = e_1254,
inference(demodulation,[status(thm)],[c_177,c_577]) ).
tcf(c_580,plain,
store(a_1253,i5,e_1250) = a_1255,
inference(light_normalisation,[status(thm)],[c_137,c_578]) ).
tcf(c_692,plain,
select(a_1284,i8) = e_1244,
inference(superposition,[status(thm)],[c_153,c_129]) ).
tcf(c_695,plain,
e_1244 = e_1285,
inference(demodulation,[status(thm)],[c_191,c_692]) ).
tcf(c_697,plain,
store(a_1284,i6,e_1244) = a_1286,
inference(light_normalisation,[status(thm)],[c_154,c_695]) ).
tcf(c_704,plain,
select(a_1288,i8) = e_1287,
inference(superposition,[status(thm)],[c_155,c_129]) ).
tcf(c_707,plain,
e_1287 = e_1289,
inference(demodulation,[status(thm)],[c_193,c_704]) ).
tcf(c_715,plain,
store(a_1288,i5,e_1287) = a_1290,
inference(light_normalisation,[status(thm)],[c_156,c_707]) ).
tcf(c_1088,plain,
! [X0: $i] : store(store(a1,i7,select(a1,X0)),X0,e_1244) = store(store(a1,X0,e_1244),i7,select(a1,X0)),
inference(superposition,[status(thm)],[c_172,c_131]) ).
tcf(c_1092,plain,
! [X0: $i] : store(store(a_1251,i5,select(a_1251,X0)),X0,e_1252) = store(store(a_1251,X0,e_1252),i5,select(a_1251,X0)),
inference(superposition,[status(thm)],[c_176,c_131]) ).
tcf(c_1096,plain,
! [X0: $i] : store(store(a_1259,i1,select(a_1259,X0)),X0,e_1260) = store(store(a_1259,X0,e_1260),i1,select(a_1259,X0)),
inference(superposition,[status(thm)],[c_180,c_131]) ).
tcf(c_1101,plain,
! [X0: $i] : store(store(a_1270,i2,select(a_1270,X0)),X0,e_1271) = store(store(a_1270,X0,e_1271),i2,select(a_1270,X0)),
inference(superposition,[status(thm)],[c_185,c_131]) ).
tcf(c_1105,plain,
! [X0: $i] : store(store(a_1278,i5,select(a_1278,X0)),X0,e_1279) = store(store(a_1278,X0,e_1279),i5,select(a_1278,X0)),
inference(superposition,[status(thm)],[c_189,c_131]) ).
tcf(c_1169,plain,
! [X0: $i,X1: $i,X2: $i] : select(store(store(X0,X1,select(X0,X2)),X2,select(X0,X1)),X1) = select(X0,X2),
inference(superposition,[status(thm)],[c_131,c_129]) ).
tcf(c_3010,plain,
! [X0: $i] : select(store(store(a1,X0,e_1244),i7,select(a1,X0)),X0) = e_1244,
inference(superposition,[status(thm)],[c_172,c_1169]) ).
tcf(c_4638,plain,
select(store(a_1245,i7,select(a1,i8)),i8) = e_1244,
inference(superposition,[status(thm)],[c_132,c_3010]) ).
tcf(c_4650,plain,
e_1244 = e_1248,
inference(light_normalisation,[status(thm)],[c_4638,c_133,c_173,c_174]) ).
tcf(c_4657,plain,
store(a_1247,i6,e_1244) = a_1249,
inference(demodulation,[status(thm)],[c_134,c_4650]) ).
tcf(c_8448,plain,
store(store(a1,i8,e_1244),i7,e_1246) = store(store(a1,i7,e_1246),i8,e_1244),
inference(superposition,[status(thm)],[c_173,c_1088]) ).
tcf(c_8452,plain,
a_1247 = a_1284,
inference(light_normalisation,[status(thm)],[c_8448,c_132,c_133,c_152,c_153]) ).
tcf(c_8466,plain,
store(a_1247,i6,e_1244) = a_1286,
inference(demodulation,[status(thm)],[c_697,c_8452]) ).
tcf(c_8469,plain,
select(a_1247,i6) = e_1287,
inference(demodulation,[status(thm)],[c_192,c_8452]) ).
tcf(c_8470,plain,
e_1250 = e_1287,
inference(light_normalisation,[status(thm)],[c_8469,c_175]) ).
tcf(c_8478,plain,
store(a_1288,i5,e_1250) = a_1290,
inference(demodulation,[status(thm)],[c_715,c_8470]) ).
tcf(c_8481,plain,
store(a_1286,i8,e_1250) = a_1288,
inference(demodulation,[status(thm)],[c_155,c_8470]) ).
tcf(c_8482,plain,
a_1249 = a_1286,
inference(light_normalisation,[status(thm)],[c_8466,c_4657]) ).
tcf(c_8554,plain,
a_1251 = a_1288,
inference(light_normalisation,[status(thm)],[c_8481,c_135,c_8482]) ).
tcf(c_8555,plain,
store(a_1251,i5,e_1250) = a_1290,
inference(demodulation,[status(thm)],[c_8478,c_8554]) ).
tcf(c_8561,plain,
select(a_1251,i5) = e_1291,
inference(demodulation,[status(thm)],[c_194,c_8554]) ).
tcf(c_8562,plain,
e_1252 = e_1291,
inference(light_normalisation,[status(thm)],[c_8561,c_176]) ).
tcf(c_8569,plain,
store(a_1290,i8,e_1252) = a_1292,
inference(demodulation,[status(thm)],[c_157,c_8562]) ).
tcf(c_9363,plain,
store(store(a_1251,i8,e_1252),i5,e_1250) = store(store(a_1251,i5,e_1250),i8,e_1252),
inference(superposition,[status(thm)],[c_577,c_1092]) ).
tcf(c_9368,plain,
a_1255 = a_1292,
inference(light_normalisation,[status(thm)],[c_9363,c_136,c_580,c_8555,c_8569]) ).
tcf(c_9387,plain,
store(a_1255,i4,e_1293) = a_1294,
inference(demodulation,[status(thm)],[c_158,c_9368]) ).
tcf(c_9388,plain,
select(a_1255,i4) = e_1295,
inference(demodulation,[status(thm)],[c_196,c_9368]) ).
tcf(c_9389,plain,
select(a_1255,i9) = e_1293,
inference(demodulation,[status(thm)],[c_195,c_9368]) ).
tcf(c_9390,plain,
e_1256 = e_1293,
inference(light_normalisation,[status(thm)],[c_9389,c_178]) ).
tcf(c_9395,plain,
e_1258 = e_1295,
inference(light_normalisation,[status(thm)],[c_9388,c_179]) ).
tcf(c_9399,plain,
store(a_1294,i9,e_1258) = a_1296,
inference(demodulation,[status(thm)],[c_159,c_9395]) ).
tcf(c_9493,plain,
a_1257 = a_1294,
inference(light_normalisation,[status(thm)],[c_9387,c_138,c_9390]) ).
tcf(c_9499,plain,
a_1259 = a_1296,
inference(light_normalisation,[status(thm)],[c_9399,c_139,c_9493]) ).
tcf(c_9506,plain,
store(a_1259,i1,e_1297) = a_1298,
inference(demodulation,[status(thm)],[c_160,c_9499]) ).
tcf(c_9507,plain,
select(a_1259,i1) = e_1299,
inference(demodulation,[status(thm)],[c_198,c_9499]) ).
tcf(c_9508,plain,
select(a_1259,i7) = e_1297,
inference(demodulation,[status(thm)],[c_197,c_9499]) ).
tcf(c_9509,plain,
e_1262 = e_1297,
inference(light_normalisation,[status(thm)],[c_9508,c_181]) ).
tcf(c_9510,plain,
e_1260 = e_1299,
inference(light_normalisation,[status(thm)],[c_9507,c_180]) ).
tcf(c_9520,plain,
store(a_1298,i7,e_1260) = a_1300,
inference(demodulation,[status(thm)],[c_161,c_9510]) ).
tcf(c_9684,plain,
store(a_1259,i1,e_1262) = a_1298,
inference(light_normalisation,[status(thm)],[c_9506,c_9509]) ).
tcf(c_9821,plain,
store(store(a_1259,i7,e_1260),i1,e_1262) = store(store(a_1259,i1,e_1262),i7,e_1260),
inference(superposition,[status(thm)],[c_181,c_1096]) ).
tcf(c_9826,plain,
a_1263 = a_1300,
inference(light_normalisation,[status(thm)],[c_9821,c_140,c_141,c_9520,c_9684]) ).
tcf(c_9837,plain,
store(a_1263,i4,e_1301) = a_1302,
inference(demodulation,[status(thm)],[c_162,c_9826]) ).
tcf(c_9838,plain,
select(a_1263,i4) = e_1303,
inference(demodulation,[status(thm)],[c_200,c_9826]) ).
tcf(c_9839,plain,
select(a_1263,i5) = e_1301,
inference(demodulation,[status(thm)],[c_199,c_9826]) ).
tcf(c_9840,plain,
e_1264 = e_1301,
inference(light_normalisation,[status(thm)],[c_9839,c_182]) ).
tcf(c_9847,plain,
e_1266 = e_1303,
inference(light_normalisation,[status(thm)],[c_9838,c_183]) ).
tcf(c_9851,plain,
store(a_1302,i5,e_1266) = a_1304,
inference(demodulation,[status(thm)],[c_163,c_9847]) ).
tcf(c_10011,plain,
a_1265 = a_1302,
inference(light_normalisation,[status(thm)],[c_9837,c_142,c_9840]) ).
tcf(c_10016,plain,
a_1267 = a_1304,
inference(light_normalisation,[status(thm)],[c_9851,c_143,c_10011]) ).
tcf(c_10022,plain,
store(a_1267,i0,e_1305) = a_1306,
inference(demodulation,[status(thm)],[c_164,c_10016]) ).
tcf(c_10023,plain,
select(a_1267,i0) = e_1305,
inference(demodulation,[status(thm)],[c_201,c_10016]) ).
tcf(c_10024,plain,
e_1268 = e_1305,
inference(light_normalisation,[status(thm)],[c_10023,c_184]) ).
tcf(c_10033,plain,
store(a_1306,i0,e_1268) = a_1307,
inference(demodulation,[status(thm)],[c_165,c_10024]) ).
tcf(c_10223,plain,
a_1269 = a_1306,
inference(light_normalisation,[status(thm)],[c_10022,c_144,c_10024]) ).
tcf(c_10239,plain,
a_1270 = a_1307,
inference(light_normalisation,[status(thm)],[c_10033,c_145,c_10223]) ).
tcf(c_10245,plain,
store(a_1270,i2,e_1308) = a_1309,
inference(demodulation,[status(thm)],[c_166,c_10239]) ).
tcf(c_10246,plain,
select(a_1270,i2) = e_1310,
inference(demodulation,[status(thm)],[c_203,c_10239]) ).
tcf(c_10247,plain,
select(a_1270,i1) = e_1308,
inference(demodulation,[status(thm)],[c_202,c_10239]) ).
tcf(c_10248,plain,
e_1273 = e_1308,
inference(light_normalisation,[status(thm)],[c_10247,c_186]) ).
tcf(c_10249,plain,
e_1271 = e_1310,
inference(light_normalisation,[status(thm)],[c_10246,c_185]) ).
tcf(c_10259,plain,
store(a_1309,i1,e_1271) = a_1311,
inference(demodulation,[status(thm)],[c_167,c_10249]) ).
tcf(c_10441,plain,
store(a_1270,i2,e_1273) = a_1309,
inference(light_normalisation,[status(thm)],[c_10245,c_10248]) ).
tcf(c_10538,plain,
store(store(a_1270,i1,e_1271),i2,e_1273) = store(store(a_1270,i2,e_1273),i1,e_1271),
inference(superposition,[status(thm)],[c_186,c_1101]) ).
tcf(c_10544,plain,
a_1274 = a_1311,
inference(light_normalisation,[status(thm)],[c_10538,c_146,c_147,c_10259,c_10441]) ).
tcf(c_10559,plain,
store(a_1274,i3,e_1312) = a_1313,
inference(demodulation,[status(thm)],[c_168,c_10544]) ).
tcf(c_10560,plain,
select(a_1274,i3) = e_1314,
inference(demodulation,[status(thm)],[c_205,c_10544]) ).
tcf(c_10561,plain,
select(a_1274,i0) = e_1312,
inference(demodulation,[status(thm)],[c_204,c_10544]) ).
tcf(c_10562,plain,
e_1275 = e_1312,
inference(light_normalisation,[status(thm)],[c_10561,c_187]) ).
tcf(c_10567,plain,
e_1277 = e_1314,
inference(light_normalisation,[status(thm)],[c_10560,c_188]) ).
tcf(c_10571,plain,
store(a_1313,i0,e_1277) = a_1315,
inference(demodulation,[status(thm)],[c_169,c_10567]) ).
tcf(c_10709,plain,
a_1276 = a_1313,
inference(light_normalisation,[status(thm)],[c_10559,c_148,c_10562]) ).
tcf(c_10715,plain,
a_1278 = a_1315,
inference(light_normalisation,[status(thm)],[c_10571,c_149,c_10709]) ).
tcf(c_10722,plain,
store(a_1278,i5,e_1316) = a_1317,
inference(demodulation,[status(thm)],[c_170,c_10715]) ).
tcf(c_10723,plain,
select(a_1278,i5) = e_1318,
inference(demodulation,[status(thm)],[c_207,c_10715]) ).
tcf(c_10724,plain,
select(a_1278,i9) = e_1316,
inference(demodulation,[status(thm)],[c_206,c_10715]) ).
tcf(c_10725,plain,
e_1281 = e_1316,
inference(light_normalisation,[status(thm)],[c_10724,c_190]) ).
tcf(c_10726,plain,
e_1279 = e_1318,
inference(light_normalisation,[status(thm)],[c_10723,c_189]) ).
tcf(c_10739,plain,
store(a_1317,i9,e_1279) = a_1319,
inference(demodulation,[status(thm)],[c_171,c_10726]) ).
tcf(c_10848,plain,
store(store(a_1278,i5,e_1281),i9,e_1279) = store(store(a_1278,i9,e_1279),i5,e_1281),
inference(superposition,[status(thm)],[c_190,c_1105]) ).
tcf(c_10853,plain,
store(store(a_1278,i5,e_1281),i9,e_1279) = a_1282,
inference(light_normalisation,[status(thm)],[c_10848,c_150,c_151]) ).
tcf(c_10922,plain,
store(a_1278,i5,e_1281) = a_1317,
inference(light_normalisation,[status(thm)],[c_10722,c_10725]) ).
tcf(c_10923,plain,
store(a_1317,i9,e_1279) = a_1282,
inference(demodulation,[status(thm)],[c_10853,c_10922]) ).
tcf(c_10928,plain,
a_1282 = a_1319,
inference(light_normalisation,[status(thm)],[c_10739,c_10923]) ).
tcf(c_10929,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_10928,c_380]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV543-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.08/0.36 % Computer : n004.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Thu Sep 24 20:24:24 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.08/0.40 Running first-order theorem proving
% 0.08/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.41
% 0.08/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.08/0.41
% 0.08/0.41 % Detected problem language: tptp
% 0.08/0.42 % Proving...
% 8.06/1.62 % SZS status Started for theBenchmark.p
% 8.06/1.62 % SZS status Unsatisfiable for theBenchmark.p
% 8.06/1.62
% 8.06/1.62 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 8.06/1.62
% 8.06/1.62 % ------ iProver source info
% 8.06/1.62
% 8.06/1.62 % git: date: 2026-07-19 20:42:38 +0200
% 8.06/1.62 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 8.06/1.62 % git: non_committed_changes: false
% 8.06/1.62
% 8.06/1.62 % ------ Parsing...% successful
% 8.06/1.62
% 8.06/1.62
% 8.06/1.62 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 8.06/1.62
% 8.06/1.62 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 8.06/1.62
% 8.06/1.62 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 8.06/1.62
% 8.06/1.62 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 8.06/1.62 % ------ Proving...
% 8.06/1.62 % ------ Problem Properties
% 8.06/1.62
% 8.06/1.62 %
% 8.06/1.62 % clauses 80
% 8.06/1.62 % conjectures 1
% 8.06/1.62 % EPR 1
% 8.06/1.62 % Horn 79
% 8.06/1.62 % unary 79
% 8.06/1.62 % binary 1
% 8.06/1.62 % lits 81
% 8.06/1.62 % lits eq 81
% 8.06/1.62 % fd_pure 0
% 8.06/1.62 % fd_pseudo 0
% 8.06/1.62 % fd_cond 0
% 8.06/1.62 % fd_pseudo_cond 1
% 8.06/1.62 % AC symbols 0
% 8.06/1.62
% 8.06/1.62 % ------ Schedule dynamic 5 is on
% 8.06/1.62
% 8.06/1.62 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 8.06/1.62
% 8.06/1.62
% 8.06/1.62 % ------
% 8.06/1.62 % Current options:
% 8.06/1.62 % ------
% 8.06/1.62
% 8.06/1.62
% 8.06/1.62 %
% 8.06/1.62
% 8.06/1.62 % ------ Proving...
% 8.06/1.62 %
% 8.06/1.62
% 8.06/1.62 % SZS status Unsatisfiable for theBenchmark.p
% 8.06/1.62
% 8.06/1.62 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.06/1.63
% 8.06/1.63
%------------------------------------------------------------------------------