%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV543-1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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 : Thu Sep 24 02:48:48 PM UTC 2026
% Result : Unsatisfiable 17.34s 2.68s
% Output : CNFRefutation 12.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 79
% Syntax : Number of formulae : 284 ( 284 unt; 0 def)
% Number of atoms : 284 ( 283 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% 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 : 24 ( 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,I,E] : select(store(A,I,E),I) = E,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,I,J] : store(store(A,I,select(A,J)),J,select(A,I)) = store(store(A,J,select(A,I)),I,select(A,J)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,hypothesis,
a_1245 = store(a1,i8,e_1244),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,hypothesis,
a_1247 = store(a_1245,i7,e_1246),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,hypothesis,
a_1249 = store(a_1247,i6,e_1248),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,hypothesis,
a_1251 = store(a_1249,i8,e_1250),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,hypothesis,
a_1253 = store(a_1251,i8,e_1252),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,hypothesis,
a_1255 = store(a_1253,i5,e_1254),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,hypothesis,
a_1257 = store(a_1255,i4,e_1256),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,hypothesis,
a_1259 = store(a_1257,i9,e_1258),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,hypothesis,
a_1261 = store(a_1259,i7,e_1260),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,hypothesis,
a_1263 = store(a_1261,i1,e_1262),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,hypothesis,
a_1265 = store(a_1263,i4,e_1264),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,hypothesis,
a_1267 = store(a_1265,i5,e_1266),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,hypothesis,
a_1269 = store(a_1267,i0,e_1268),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,hypothesis,
a_1270 = store(a_1269,i0,e_1268),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,hypothesis,
a_1272 = store(a_1270,i1,e_1271),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,hypothesis,
a_1274 = store(a_1272,i2,e_1273),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,hypothesis,
a_1276 = store(a_1274,i3,e_1275),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,hypothesis,
a_1278 = store(a_1276,i0,e_1277),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,hypothesis,
a_1280 = store(a_1278,i9,e_1279),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,hypothesis,
a_1282 = store(a_1280,i5,e_1281),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,hypothesis,
a_1283 = store(a1,i7,e_1246),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,hypothesis,
a_1284 = store(a_1283,i8,e_1244),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,hypothesis,
a_1286 = store(a_1284,i6,e_1285),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,hypothesis,
a_1288 = store(a_1286,i8,e_1287),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,hypothesis,
a_1290 = store(a_1288,i5,e_1289),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,hypothesis,
a_1292 = store(a_1290,i8,e_1291),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,hypothesis,
a_1294 = store(a_1292,i4,e_1293),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,hypothesis,
a_1296 = store(a_1294,i9,e_1295),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,hypothesis,
a_1298 = store(a_1296,i1,e_1297),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,hypothesis,
a_1300 = store(a_1298,i7,e_1299),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,hypothesis,
a_1302 = store(a_1300,i4,e_1301),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,hypothesis,
a_1304 = store(a_1302,i5,e_1303),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,hypothesis,
a_1306 = store(a_1304,i0,e_1305),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,hypothesis,
a_1307 = store(a_1306,i0,e_1305),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,hypothesis,
a_1309 = store(a_1307,i2,e_1308),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,hypothesis,
a_1311 = store(a_1309,i1,e_1310),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,hypothesis,
a_1313 = store(a_1311,i3,e_1312),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,hypothesis,
a_1315 = store(a_1313,i0,e_1314),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,hypothesis,
a_1317 = store(a_1315,i5,e_1316),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,hypothesis,
a_1319 = store(a_1317,i9,e_1318),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,hypothesis,
e_1244 = select(a1,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,hypothesis,
e_1246 = select(a1,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,hypothesis,
e_1248 = select(a_1247,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,hypothesis,
e_1250 = select(a_1247,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,hypothesis,
e_1252 = select(a_1251,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,hypothesis,
e_1254 = select(a_1251,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,hypothesis,
e_1256 = select(a_1255,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,hypothesis,
e_1258 = select(a_1255,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,hypothesis,
e_1260 = select(a_1259,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,hypothesis,
e_1262 = select(a_1259,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,hypothesis,
e_1264 = select(a_1263,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,hypothesis,
e_1266 = select(a_1263,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,hypothesis,
e_1268 = select(a_1267,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,hypothesis,
e_1271 = select(a_1270,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,hypothesis,
e_1273 = select(a_1270,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,hypothesis,
e_1275 = select(a_1274,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,hypothesis,
e_1277 = select(a_1274,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f61,hypothesis,
e_1279 = select(a_1278,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f62,hypothesis,
e_1281 = select(a_1278,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,hypothesis,
e_1285 = select(a_1284,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,hypothesis,
e_1287 = select(a_1284,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f65,hypothesis,
e_1289 = select(a_1288,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,hypothesis,
e_1291 = select(a_1288,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,hypothesis,
e_1293 = select(a_1292,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f68,hypothesis,
e_1295 = select(a_1292,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,hypothesis,
e_1297 = select(a_1296,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,hypothesis,
e_1299 = select(a_1296,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,hypothesis,
e_1301 = select(a_1300,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,hypothesis,
e_1303 = select(a_1300,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,hypothesis,
e_1305 = select(a_1304,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,hypothesis,
e_1308 = select(a_1307,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,hypothesis,
e_1310 = select(a_1307,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,hypothesis,
e_1312 = select(a_1311,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f77,hypothesis,
e_1314 = select(a_1311,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f78,hypothesis,
e_1316 = select(a_1315,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f79,hypothesis,
e_1318 = select(a_1315,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,negated_conjecture,
a_1282 != a_1319,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f81,plain,
! [X0,X1,X2] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f84,plain,
! [X0,X1,X2] : 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,[status(thm)],[f3]) ).
fof(f85,plain,
a_1245 = store(a1,i8,e_1244),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f86,plain,
a_1247 = store(a_1245,i7,e_1246),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f87,plain,
a_1249 = store(a_1247,i6,e_1248),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f88,plain,
a_1251 = store(a_1249,i8,e_1250),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f89,plain,
a_1253 = store(a_1251,i8,e_1252),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f90,plain,
a_1255 = store(a_1253,i5,e_1254),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f91,plain,
a_1257 = store(a_1255,i4,e_1256),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f92,plain,
a_1259 = store(a_1257,i9,e_1258),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f93,plain,
a_1261 = store(a_1259,i7,e_1260),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f94,plain,
a_1263 = store(a_1261,i1,e_1262),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f95,plain,
a_1265 = store(a_1263,i4,e_1264),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f96,plain,
a_1267 = store(a_1265,i5,e_1266),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f97,plain,
a_1269 = store(a_1267,i0,e_1268),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f98,plain,
a_1270 = store(a_1269,i0,e_1268),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f99,plain,
a_1272 = store(a_1270,i1,e_1271),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f100,plain,
a_1274 = store(a_1272,i2,e_1273),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f101,plain,
a_1276 = store(a_1274,i3,e_1275),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f102,plain,
a_1278 = store(a_1276,i0,e_1277),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f103,plain,
a_1280 = store(a_1278,i9,e_1279),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f104,plain,
a_1282 = store(a_1280,i5,e_1281),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f105,plain,
a_1283 = store(a1,i7,e_1246),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f106,plain,
a_1284 = store(a_1283,i8,e_1244),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f107,plain,
a_1286 = store(a_1284,i6,e_1285),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f108,plain,
a_1288 = store(a_1286,i8,e_1287),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f109,plain,
a_1290 = store(a_1288,i5,e_1289),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f110,plain,
a_1292 = store(a_1290,i8,e_1291),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f111,plain,
a_1294 = store(a_1292,i4,e_1293),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f112,plain,
a_1296 = store(a_1294,i9,e_1295),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f113,plain,
a_1298 = store(a_1296,i1,e_1297),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f114,plain,
a_1300 = store(a_1298,i7,e_1299),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f115,plain,
a_1302 = store(a_1300,i4,e_1301),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f116,plain,
a_1304 = store(a_1302,i5,e_1303),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f117,plain,
a_1306 = store(a_1304,i0,e_1305),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f118,plain,
a_1307 = store(a_1306,i0,e_1305),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f119,plain,
a_1309 = store(a_1307,i2,e_1308),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f120,plain,
a_1311 = store(a_1309,i1,e_1310),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f121,plain,
a_1313 = store(a_1311,i3,e_1312),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f122,plain,
a_1315 = store(a_1313,i0,e_1314),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f123,plain,
a_1317 = store(a_1315,i5,e_1316),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f124,plain,
a_1319 = store(a_1317,i9,e_1318),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f125,plain,
e_1244 = select(a1,i7),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f126,plain,
e_1246 = select(a1,i8),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f127,plain,
e_1248 = select(a_1247,i8),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f128,plain,
e_1250 = select(a_1247,i6),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f129,plain,
e_1252 = select(a_1251,i5),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f130,plain,
e_1254 = select(a_1251,i8),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f131,plain,
e_1256 = select(a_1255,i9),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f132,plain,
e_1258 = select(a_1255,i4),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f133,plain,
e_1260 = select(a_1259,i1),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f134,plain,
e_1262 = select(a_1259,i7),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f135,plain,
e_1264 = select(a_1263,i5),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f136,plain,
e_1266 = select(a_1263,i4),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f137,plain,
e_1268 = select(a_1267,i0),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f138,plain,
e_1271 = select(a_1270,i2),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f139,plain,
e_1273 = select(a_1270,i1),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f140,plain,
e_1275 = select(a_1274,i0),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f141,plain,
e_1277 = select(a_1274,i3),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f142,plain,
e_1279 = select(a_1278,i5),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f143,plain,
e_1281 = select(a_1278,i9),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f144,plain,
e_1285 = select(a_1284,i8),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f145,plain,
e_1287 = select(a_1284,i6),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f146,plain,
e_1289 = select(a_1288,i8),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f147,plain,
e_1291 = select(a_1288,i5),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f148,plain,
e_1293 = select(a_1292,i9),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f149,plain,
e_1295 = select(a_1292,i4),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f150,plain,
e_1297 = select(a_1296,i7),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f151,plain,
e_1299 = select(a_1296,i1),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f152,plain,
e_1301 = select(a_1300,i5),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f153,plain,
e_1303 = select(a_1300,i4),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f154,plain,
e_1305 = select(a_1304,i0),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f155,plain,
e_1308 = select(a_1307,i1),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f156,plain,
e_1310 = select(a_1307,i2),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f157,plain,
e_1312 = select(a_1311,i0),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f158,plain,
e_1314 = select(a_1311,i3),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f159,plain,
e_1316 = select(a_1315,i9),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f160,plain,
e_1318 = select(a_1315,i5),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f161,plain,
a_1282 != a_1319,
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f184,plain,
! [X0] : store(store(a_1278,X0,e_1281),i9,select(a_1278,X0)) = store(store(a_1278,i9,select(a_1278,X0)),X0,select(a_1278,i9)),
inference(paramodulation,[status(thm)],[f143,f84]) ).
fof(f188,plain,
! [X0] : store(store(a_1270,X0,e_1273),i1,select(a_1270,X0)) = store(store(a_1270,i1,select(a_1270,X0)),X0,select(a_1270,i1)),
inference(paramodulation,[status(thm)],[f139,f84]) ).
fof(f193,plain,
! [X0] : store(store(a_1259,X0,e_1262),i7,select(a_1259,X0)) = store(store(a_1259,i7,select(a_1259,X0)),X0,select(a_1259,i7)),
inference(paramodulation,[status(thm)],[f134,f84]) ).
fof(f197,plain,
! [X0] : store(store(a_1251,X0,e_1254),i8,select(a_1251,X0)) = store(store(a_1251,i8,select(a_1251,X0)),X0,select(a_1251,i8)),
inference(paramodulation,[status(thm)],[f130,f84]) ).
fof(f206,plain,
! [X0] : store(store(a1,X0,e_1246),i8,select(a1,X0)) = store(store(a1,i8,select(a1,X0)),X0,select(a1,i8)),
inference(paramodulation,[status(thm)],[f126,f84]) ).
fof(f334,plain,
! [X0] : store(store(a_1278,X0,e_1281),i9,select(a_1278,X0)) = store(store(a_1278,i9,select(a_1278,X0)),X0,e_1281),
inference(forward_demodulation,[status(thm)],[f143,f184]) ).
fof(f338,plain,
! [X0] : store(store(a_1270,X0,e_1273),i1,select(a_1270,X0)) = store(store(a_1270,i1,select(a_1270,X0)),X0,e_1273),
inference(forward_demodulation,[status(thm)],[f139,f188]) ).
fof(f343,plain,
! [X0] : store(store(a_1259,X0,e_1262),i7,select(a_1259,X0)) = store(store(a_1259,i7,select(a_1259,X0)),X0,e_1262),
inference(forward_demodulation,[status(thm)],[f134,f193]) ).
fof(f347,plain,
! [X0] : store(store(a_1251,X0,e_1254),i8,select(a_1251,X0)) = store(store(a_1251,i8,select(a_1251,X0)),X0,e_1254),
inference(forward_demodulation,[status(thm)],[f130,f197]) ).
fof(f354,plain,
! [X0] : store(store(a1,X0,e_1246),i8,select(a1,X0)) = store(store(a1,i8,select(a1,X0)),X0,e_1246),
inference(forward_demodulation,[status(thm)],[f126,f206]) ).
fof(f720,plain,
select(a_1251,i8) = e_1250,
inference(paramodulation,[status(thm)],[f88,f81]) ).
fof(f721,plain,
e_1254 = e_1250,
inference(backward_demodulation,[status(thm)],[f720,f130]) ).
fof(f740,plain,
a_1255 = store(a_1253,i5,e_1250),
inference(forward_demodulation,[status(thm)],[f721,f90]) ).
fof(f1074,plain,
select(a_1284,i8) = e_1244,
inference(paramodulation,[status(thm)],[f106,f81]) ).
fof(f1387,plain,
e_1285 = e_1244,
inference(backward_demodulation,[status(thm)],[f1074,f144]) ).
fof(f1396,plain,
a_1286 = store(a_1284,i6,e_1244),
inference(forward_demodulation,[status(thm)],[f1387,f107]) ).
fof(f1408,plain,
select(a_1288,i8) = e_1287,
inference(paramodulation,[status(thm)],[f108,f81]) ).
fof(f1409,plain,
e_1289 = e_1287,
inference(backward_demodulation,[status(thm)],[f1408,f146]) ).
fof(f1418,plain,
a_1290 = store(a_1288,i5,e_1287),
inference(forward_demodulation,[status(thm)],[f1409,f109]) ).
fof(f2976,plain,
store(store(a_1278,i5,e_1281),i9,select(a_1278,i5)) = store(store(a_1278,i9,e_1279),i5,e_1281),
inference(paramodulation,[status(thm)],[f142,f334]) ).
fof(f2983,plain,
store(store(a_1278,i5,e_1281),i9,e_1279) = store(store(a_1278,i9,e_1279),i5,e_1281),
inference(forward_demodulation,[status(thm)],[f142,f2976]) ).
fof(f2984,plain,
store(store(a_1278,i5,e_1281),i9,e_1279) = store(a_1280,i5,e_1281),
inference(forward_demodulation,[status(thm)],[f103,f2983]) ).
fof(f2985,plain,
store(store(a_1278,i5,e_1281),i9,e_1279) = a_1282,
inference(forward_demodulation,[status(thm)],[f104,f2984]) ).
fof(f4683,plain,
! [X0] : store(store(a_1251,X0,e_1250),i8,select(a_1251,X0)) = store(store(a_1251,i8,select(a_1251,X0)),X0,e_1254),
inference(forward_demodulation,[status(thm)],[f721,f347]) ).
fof(f4684,plain,
! [X0] : store(store(a_1251,X0,e_1250),i8,select(a_1251,X0)) = store(store(a_1251,i8,select(a_1251,X0)),X0,e_1250),
inference(forward_demodulation,[status(thm)],[f721,f4683]) ).
fof(f8507,plain,
store(a_1283,i8,select(a1,i7)) = store(store(a1,i8,select(a1,i7)),i7,e_1246),
inference(paramodulation,[status(thm)],[f105,f354]) ).
fof(f8532,plain,
store(a_1283,i8,e_1244) = store(store(a1,i8,select(a1,i7)),i7,e_1246),
inference(forward_demodulation,[status(thm)],[f125,f8507]) ).
fof(f8533,plain,
a_1284 = store(store(a1,i8,select(a1,i7)),i7,e_1246),
inference(forward_demodulation,[status(thm)],[f106,f8532]) ).
fof(f8534,plain,
a_1284 = store(store(a1,i8,e_1244),i7,e_1246),
inference(forward_demodulation,[status(thm)],[f125,f8533]) ).
fof(f8535,plain,
a_1284 = store(a_1245,i7,e_1246),
inference(forward_demodulation,[status(thm)],[f85,f8534]) ).
fof(f8536,plain,
a_1284 = a_1247,
inference(forward_demodulation,[status(thm)],[f86,f8535]) ).
fof(f8973,plain,
a_1286 = store(a_1247,i6,e_1244),
inference(backward_demodulation,[status(thm)],[f8536,f1396]) ).
fof(f8974,plain,
select(a_1247,i8) = e_1244,
inference(backward_demodulation,[status(thm)],[f8536,f1074]) ).
fof(f8976,plain,
e_1287 = select(a_1247,i6),
inference(backward_demodulation,[status(thm)],[f8536,f145]) ).
fof(f8983,plain,
e_1287 = e_1250,
inference(forward_demodulation,[status(thm)],[f128,f8976]) ).
fof(f8990,plain,
a_1290 = store(a_1288,i5,e_1250),
inference(backward_demodulation,[status(thm)],[f8983,f1418]) ).
fof(f8993,plain,
a_1288 = store(a_1286,i8,e_1250),
inference(backward_demodulation,[status(thm)],[f8983,f108]) ).
fof(f8995,plain,
e_1248 = e_1244,
inference(backward_demodulation,[status(thm)],[f8974,f127]) ).
fof(f9013,plain,
a_1249 = store(a_1247,i6,e_1244),
inference(backward_demodulation,[status(thm)],[f8995,f87]) ).
fof(f9213,plain,
a_1286 = a_1249,
inference(backward_demodulation,[status(thm)],[f9013,f8973]) ).
fof(f9247,plain,
a_1288 = store(a_1249,i8,e_1250),
inference(backward_demodulation,[status(thm)],[f9213,f8993]) ).
fof(f9252,plain,
a_1288 = a_1251,
inference(forward_demodulation,[status(thm)],[f88,f9247]) ).
fof(f9254,plain,
a_1290 = store(a_1251,i5,e_1250),
inference(backward_demodulation,[status(thm)],[f9252,f8990]) ).
fof(f9261,plain,
e_1291 = select(a_1251,i5),
inference(backward_demodulation,[status(thm)],[f9252,f147]) ).
fof(f9265,plain,
e_1291 = e_1252,
inference(forward_demodulation,[status(thm)],[f129,f9261]) ).
fof(f9549,plain,
a_1292 = store(a_1290,i8,e_1252),
inference(backward_demodulation,[status(thm)],[f9265,f110]) ).
fof(f9578,plain,
store(a_1290,i8,select(a_1251,i5)) = store(store(a_1251,i8,select(a_1251,i5)),i5,e_1250),
inference(paramodulation,[status(thm)],[f9254,f4684]) ).
fof(f9588,plain,
store(a_1290,i8,e_1252) = store(store(a_1251,i8,select(a_1251,i5)),i5,e_1250),
inference(forward_demodulation,[status(thm)],[f129,f9578]) ).
fof(f9589,plain,
store(a_1290,i8,e_1252) = store(store(a_1251,i8,e_1252),i5,e_1250),
inference(forward_demodulation,[status(thm)],[f129,f9588]) ).
fof(f9590,plain,
store(a_1290,i8,e_1252) = store(a_1253,i5,e_1250),
inference(forward_demodulation,[status(thm)],[f89,f9589]) ).
fof(f9591,plain,
store(a_1290,i8,e_1252) = a_1255,
inference(forward_demodulation,[status(thm)],[f740,f9590]) ).
fof(f9649,plain,
a_1292 = a_1255,
inference(backward_demodulation,[status(thm)],[f9591,f9549]) ).
fof(f9692,plain,
a_1294 = store(a_1255,i4,e_1293),
inference(backward_demodulation,[status(thm)],[f9649,f111]) ).
fof(f9693,plain,
e_1295 = select(a_1255,i4),
inference(backward_demodulation,[status(thm)],[f9649,f149]) ).
fof(f9694,plain,
e_1293 = select(a_1255,i9),
inference(backward_demodulation,[status(thm)],[f9649,f148]) ).
fof(f9701,plain,
e_1295 = e_1258,
inference(forward_demodulation,[status(thm)],[f132,f9693]) ).
fof(f9702,plain,
e_1293 = e_1256,
inference(forward_demodulation,[status(thm)],[f131,f9694]) ).
fof(f9705,plain,
a_1296 = store(a_1294,i9,e_1258),
inference(backward_demodulation,[status(thm)],[f9701,f112]) ).
fof(f9760,plain,
a_1294 = store(a_1255,i4,e_1256),
inference(forward_demodulation,[status(thm)],[f9702,f9692]) ).
fof(f9765,plain,
a_1294 = a_1257,
inference(forward_demodulation,[status(thm)],[f91,f9760]) ).
fof(f9766,plain,
a_1296 = store(a_1257,i9,e_1258),
inference(forward_demodulation,[status(thm)],[f9765,f9705]) ).
fof(f9773,plain,
a_1298 = store(a_1259,i1,e_1297),
inference(backward_demodulation,[status(thm)],[f9776,f113]) ).
fof(f9774,plain,
e_1299 = select(a_1259,i1),
inference(backward_demodulation,[status(thm)],[f9776,f151]) ).
fof(f9775,plain,
e_1297 = select(a_1259,i7),
inference(backward_demodulation,[status(thm)],[f9776,f150]) ).
fof(f9776,plain,
a_1296 = a_1259,
inference(forward_demodulation,[status(thm)],[f92,f9766]) ).
fof(f9783,plain,
e_1299 = e_1260,
inference(forward_demodulation,[status(thm)],[f133,f9774]) ).
fof(f9784,plain,
e_1297 = e_1262,
inference(forward_demodulation,[status(thm)],[f134,f9775]) ).
fof(f9786,plain,
a_1300 = store(a_1298,i7,e_1260),
inference(backward_demodulation,[status(thm)],[f9783,f114]) ).
fof(f9789,plain,
a_1298 = store(a_1259,i1,e_1262),
inference(forward_demodulation,[status(thm)],[f9784,f9773]) ).
fof(f9790,plain,
store(a_1298,i7,select(a_1259,i1)) = store(store(a_1259,i7,select(a_1259,i1)),i1,e_1262),
inference(paramodulation,[status(thm)],[f9789,f343]) ).
fof(f9800,plain,
store(a_1298,i7,e_1260) = store(store(a_1259,i7,select(a_1259,i1)),i1,e_1262),
inference(forward_demodulation,[status(thm)],[f133,f9790]) ).
fof(f9801,plain,
store(a_1298,i7,e_1260) = store(store(a_1259,i7,e_1260),i1,e_1262),
inference(forward_demodulation,[status(thm)],[f133,f9800]) ).
fof(f9802,plain,
store(a_1298,i7,e_1260) = store(a_1261,i1,e_1262),
inference(forward_demodulation,[status(thm)],[f93,f9801]) ).
fof(f9803,plain,
store(a_1298,i7,e_1260) = a_1263,
inference(forward_demodulation,[status(thm)],[f94,f9802]) ).
fof(f10536,plain,
a_1300 = a_1263,
inference(backward_demodulation,[status(thm)],[f9803,f9786]) ).
fof(f10577,plain,
a_1302 = store(a_1263,i4,e_1301),
inference(backward_demodulation,[status(thm)],[f10536,f115]) ).
fof(f10578,plain,
e_1303 = select(a_1263,i4),
inference(backward_demodulation,[status(thm)],[f10536,f153]) ).
fof(f10579,plain,
e_1301 = select(a_1263,i5),
inference(backward_demodulation,[status(thm)],[f10536,f152]) ).
fof(f10586,plain,
e_1303 = e_1266,
inference(forward_demodulation,[status(thm)],[f136,f10578]) ).
fof(f10587,plain,
e_1301 = e_1264,
inference(forward_demodulation,[status(thm)],[f135,f10579]) ).
fof(f10590,plain,
a_1304 = store(a_1302,i5,e_1266),
inference(backward_demodulation,[status(thm)],[f10586,f116]) ).
fof(f10640,plain,
a_1302 = store(a_1263,i4,e_1264),
inference(forward_demodulation,[status(thm)],[f10587,f10577]) ).
fof(f10644,plain,
a_1302 = a_1265,
inference(forward_demodulation,[status(thm)],[f95,f10640]) ).
fof(f10645,plain,
a_1304 = store(a_1265,i5,e_1266),
inference(forward_demodulation,[status(thm)],[f10644,f10590]) ).
fof(f10652,plain,
a_1306 = store(a_1267,i0,e_1305),
inference(backward_demodulation,[status(thm)],[f10654,f117]) ).
fof(f10653,plain,
e_1305 = select(a_1267,i0),
inference(backward_demodulation,[status(thm)],[f10654,f154]) ).
fof(f10654,plain,
a_1304 = a_1267,
inference(forward_demodulation,[status(thm)],[f96,f10645]) ).
fof(f10658,plain,
e_1305 = e_1268,
inference(forward_demodulation,[status(thm)],[f137,f10653]) ).
fof(f10661,plain,
a_1307 = store(a_1306,i0,e_1268),
inference(backward_demodulation,[status(thm)],[f10658,f118]) ).
fof(f10663,plain,
a_1306 = store(a_1267,i0,e_1268),
inference(forward_demodulation,[status(thm)],[f10658,f10652]) ).
fof(f10667,plain,
a_1306 = a_1269,
inference(forward_demodulation,[status(thm)],[f97,f10663]) ).
fof(f10668,plain,
a_1307 = store(a_1269,i0,e_1268),
inference(forward_demodulation,[status(thm)],[f10667,f10661]) ).
fof(f10672,plain,
a_1309 = store(a_1270,i2,e_1308),
inference(backward_demodulation,[status(thm)],[f10675,f119]) ).
fof(f10673,plain,
e_1310 = select(a_1270,i2),
inference(backward_demodulation,[status(thm)],[f10675,f156]) ).
fof(f10674,plain,
e_1308 = select(a_1270,i1),
inference(backward_demodulation,[status(thm)],[f10675,f155]) ).
fof(f10675,plain,
a_1307 = a_1270,
inference(forward_demodulation,[status(thm)],[f98,f10668]) ).
fof(f10679,plain,
e_1310 = e_1271,
inference(forward_demodulation,[status(thm)],[f138,f10673]) ).
fof(f10680,plain,
e_1308 = e_1273,
inference(forward_demodulation,[status(thm)],[f139,f10674]) ).
fof(f10947,plain,
a_1311 = store(a_1309,i1,e_1271),
inference(backward_demodulation,[status(thm)],[f10679,f120]) ).
fof(f10948,plain,
a_1309 = store(a_1270,i2,e_1273),
inference(backward_demodulation,[status(thm)],[f10680,f10672]) ).
fof(f11028,plain,
store(a_1309,i1,select(a_1270,i2)) = store(store(a_1270,i1,select(a_1270,i2)),i2,e_1273),
inference(paramodulation,[status(thm)],[f10948,f338]) ).
fof(f11038,plain,
store(a_1309,i1,e_1271) = store(store(a_1270,i1,select(a_1270,i2)),i2,e_1273),
inference(forward_demodulation,[status(thm)],[f138,f11028]) ).
fof(f11039,plain,
a_1311 = store(store(a_1270,i1,select(a_1270,i2)),i2,e_1273),
inference(forward_demodulation,[status(thm)],[f10947,f11038]) ).
fof(f11040,plain,
a_1311 = store(store(a_1270,i1,e_1271),i2,e_1273),
inference(forward_demodulation,[status(thm)],[f138,f11039]) ).
fof(f11041,plain,
a_1311 = store(a_1272,i2,e_1273),
inference(forward_demodulation,[status(thm)],[f99,f11040]) ).
fof(f11042,plain,
a_1311 = a_1274,
inference(forward_demodulation,[status(thm)],[f100,f11041]) ).
fof(f11073,plain,
a_1313 = store(a_1274,i3,e_1312),
inference(backward_demodulation,[status(thm)],[f11042,f121]) ).
fof(f11074,plain,
e_1314 = select(a_1274,i3),
inference(backward_demodulation,[status(thm)],[f11042,f158]) ).
fof(f11075,plain,
e_1312 = select(a_1274,i0),
inference(backward_demodulation,[status(thm)],[f11042,f157]) ).
fof(f11076,plain,
e_1314 = e_1277,
inference(forward_demodulation,[status(thm)],[f141,f11074]) ).
fof(f11077,plain,
e_1312 = e_1275,
inference(forward_demodulation,[status(thm)],[f140,f11075]) ).
fof(f11089,plain,
a_1315 = store(a_1313,i0,e_1277),
inference(backward_demodulation,[status(thm)],[f11076,f122]) ).
fof(f11171,plain,
a_1313 = store(a_1274,i3,e_1275),
inference(forward_demodulation,[status(thm)],[f11077,f11073]) ).
fof(f11182,plain,
a_1313 = a_1276,
inference(forward_demodulation,[status(thm)],[f101,f11171]) ).
fof(f11183,plain,
a_1315 = store(a_1276,i0,e_1277),
inference(forward_demodulation,[status(thm)],[f11182,f11089]) ).
fof(f11194,plain,
a_1317 = store(a_1278,i5,e_1316),
inference(backward_demodulation,[status(thm)],[f11197,f123]) ).
fof(f11195,plain,
e_1318 = select(a_1278,i5),
inference(backward_demodulation,[status(thm)],[f11197,f160]) ).
fof(f11196,plain,
e_1316 = select(a_1278,i9),
inference(backward_demodulation,[status(thm)],[f11197,f159]) ).
fof(f11197,plain,
a_1315 = a_1278,
inference(forward_demodulation,[status(thm)],[f102,f11183]) ).
fof(f11198,plain,
e_1318 = e_1279,
inference(forward_demodulation,[status(thm)],[f142,f11195]) ).
fof(f11199,plain,
e_1316 = e_1281,
inference(forward_demodulation,[status(thm)],[f143,f11196]) ).
fof(f11257,plain,
a_1319 = store(a_1317,i9,e_1279),
inference(backward_demodulation,[status(thm)],[f11198,f124]) ).
fof(f11896,plain,
a_1317 = store(a_1278,i5,e_1281),
inference(backward_demodulation,[status(thm)],[f11199,f11194]) ).
fof(f11954,plain,
store(a_1317,i9,e_1279) = a_1282,
inference(backward_demodulation,[status(thm)],[f11896,f2985]) ).
fof(f11988,plain,
a_1319 = a_1282,
inference(backward_demodulation,[status(thm)],[f11954,f11257]) ).
fof(f11998,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f11988,f161]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV543-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n013.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 09:04:06 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 17.34/2.68 % Refutation found
% 17.34/2.68 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 17.34/2.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 12.50/2.74 % Elapsed time: 2.360312 seconds
% 12.50/2.74 % CPU time: 18.274923 seconds
% 12.50/2.74 % Total memory used: 352.589 MB
% 12.50/2.74 % Net memory used: 333.600 MB
%------------------------------------------------------------------------------