%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV547-1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:51:39 PM UTC 2026
% Result : Unsatisfiable 27.73s 24.18s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV547-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/20.58 % CPULimit : 300
% 0.07/20.58 % WCLimit : 300
% 0.07/20.58 % DateTime : Mon Sep 21 09:05:33 UTC 2026
% 0.07/20.59 % CPUTime :
% 0.07/20.60 % Drodi V4.1.1
% 27.73/24.18 % Refutation found
% 27.73/24.18 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 27.73/24.18 % SZS output start CNFRefutation for theBenchmark
% 27.73/24.18 fof(f1,axiom,(
% 27.73/24.18 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f3,axiom,(
% 27.73/24.18 (![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)) ))),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f4,hypothesis,(
% 27.73/24.18 a_1296 = store(a1,i8,e_1295) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f5,hypothesis,(
% 27.73/24.18 a_1298 = store(a_1296,i7,e_1297) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f6,hypothesis,(
% 27.73/24.18 a_1300 = store(a_1298,i6,e_1299) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f7,hypothesis,(
% 27.73/24.18 a_1302 = store(a_1300,i8,e_1301) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f8,hypothesis,(
% 27.73/24.18 a_1304 = store(a_1302,i8,e_1303) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f9,hypothesis,(
% 27.73/24.18 a_1306 = store(a_1304,i5,e_1305) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f10,hypothesis,(
% 27.73/24.18 a_1308 = store(a_1306,i4,e_1307) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f11,hypothesis,(
% 27.73/24.18 a_1310 = store(a_1308,i9,e_1309) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f12,hypothesis,(
% 27.73/24.18 a_1312 = store(a_1310,i7,e_1311) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f13,hypothesis,(
% 27.73/24.18 a_1314 = store(a_1312,i1,e_1313) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f14,hypothesis,(
% 27.73/24.18 a_1316 = store(a_1314,i4,e_1315) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f15,hypothesis,(
% 27.73/24.18 a_1318 = store(a_1316,i5,e_1317) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f16,hypothesis,(
% 27.73/24.18 a_1320 = store(a_1318,i0,e_1319) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f17,hypothesis,(
% 27.73/24.18 a_1321 = store(a_1320,i0,e_1319) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f18,hypothesis,(
% 27.73/24.18 a_1323 = store(a_1321,i1,e_1322) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f19,hypothesis,(
% 27.73/24.18 a_1325 = store(a_1323,i2,e_1324) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f20,hypothesis,(
% 27.73/24.18 a_1327 = store(a_1325,i3,e_1326) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f21,hypothesis,(
% 27.73/24.18 a_1329 = store(a_1327,i0,e_1328) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f22,hypothesis,(
% 27.73/24.18 a_1331 = store(a_1329,i9,e_1330) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f23,hypothesis,(
% 27.73/24.18 a_1333 = store(a_1331,i5,e_1332) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f24,hypothesis,(
% 27.73/24.18 a_1334 = store(a1,i7,e_1297) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f25,hypothesis,(
% 27.73/24.18 a_1335 = store(a_1334,i8,e_1295) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f26,hypothesis,(
% 27.73/24.18 a_1337 = store(a_1335,i6,e_1336) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f27,hypothesis,(
% 27.73/24.18 a_1339 = store(a_1337,i8,e_1338) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f28,hypothesis,(
% 27.73/24.18 a_1341 = store(a_1339,i5,e_1340) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f29,hypothesis,(
% 27.73/24.18 a_1343 = store(a_1341,i8,e_1342) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f30,hypothesis,(
% 27.73/24.18 a_1345 = store(a_1343,i4,e_1344) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f31,hypothesis,(
% 27.73/24.18 a_1347 = store(a_1345,i9,e_1346) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f32,hypothesis,(
% 27.73/24.18 a_1349 = store(a_1347,i1,e_1348) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f33,hypothesis,(
% 27.73/24.18 a_1351 = store(a_1349,i7,e_1350) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f34,hypothesis,(
% 27.73/24.18 a_1353 = store(a_1351,i4,e_1352) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f35,hypothesis,(
% 27.73/24.18 a_1355 = store(a_1353,i5,e_1354) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f36,hypothesis,(
% 27.73/24.18 a_1357 = store(a_1355,i0,e_1356) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f37,hypothesis,(
% 27.73/24.18 a_1358 = store(a_1357,i0,e_1356) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f38,hypothesis,(
% 27.73/24.18 a_1360 = store(a_1358,i2,e_1359) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f39,hypothesis,(
% 27.73/24.18 a_1362 = store(a_1360,i1,e_1361) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f40,hypothesis,(
% 27.73/24.18 a_1364 = store(a_1362,i3,e_1363) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f41,hypothesis,(
% 27.73/24.18 a_1366 = store(a_1364,i0,e_1365) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f42,hypothesis,(
% 27.73/24.18 a_1368 = store(a_1366,i5,e_1367) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f43,hypothesis,(
% 27.73/24.18 a_1370 = store(a_1368,i9,e_1369) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f44,hypothesis,(
% 27.73/24.18 e_1295 = select(a1,i7) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f45,hypothesis,(
% 27.73/24.18 e_1297 = select(a1,i8) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f46,hypothesis,(
% 27.73/24.18 e_1299 = select(a_1298,i8) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f47,hypothesis,(
% 27.73/24.18 e_1301 = select(a_1298,i6) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f48,hypothesis,(
% 27.73/24.18 e_1303 = select(a_1302,i5) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f49,hypothesis,(
% 27.73/24.18 e_1305 = select(a_1302,i8) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f50,hypothesis,(
% 27.73/24.18 e_1307 = select(a_1306,i9) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f51,hypothesis,(
% 27.73/24.18 e_1309 = select(a_1306,i4) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f52,hypothesis,(
% 27.73/24.18 e_1311 = select(a_1310,i1) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f53,hypothesis,(
% 27.73/24.18 e_1313 = select(a_1310,i7) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f54,hypothesis,(
% 27.73/24.18 e_1315 = select(a_1314,i5) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f55,hypothesis,(
% 27.73/24.18 e_1317 = select(a_1314,i4) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f56,hypothesis,(
% 27.73/24.18 e_1319 = select(a_1318,i0) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f57,hypothesis,(
% 27.73/24.18 e_1322 = select(a_1321,i2) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f58,hypothesis,(
% 27.73/24.18 e_1324 = select(a_1321,i1) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f59,hypothesis,(
% 27.73/24.18 e_1326 = select(a_1325,i0) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f60,hypothesis,(
% 27.73/24.18 e_1328 = select(a_1325,i3) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f61,hypothesis,(
% 27.73/24.18 e_1330 = select(a_1329,i5) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f62,hypothesis,(
% 27.73/24.18 e_1332 = select(a_1329,i9) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f63,hypothesis,(
% 27.73/24.18 e_1336 = select(a_1335,i8) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f64,hypothesis,(
% 27.73/24.18 e_1338 = select(a_1335,i6) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f65,hypothesis,(
% 27.73/24.18 e_1340 = select(a_1339,i8) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f66,hypothesis,(
% 27.73/24.18 e_1342 = select(a_1339,i5) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f67,hypothesis,(
% 27.73/24.18 e_1344 = select(a_1343,i9) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f68,hypothesis,(
% 27.73/24.18 e_1346 = select(a_1343,i4) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f69,hypothesis,(
% 27.73/24.18 e_1348 = select(a_1347,i7) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f70,hypothesis,(
% 27.73/24.18 e_1350 = select(a_1347,i1) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f71,hypothesis,(
% 27.73/24.18 e_1352 = select(a_1351,i5) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f72,hypothesis,(
% 27.73/24.18 e_1354 = select(a_1351,i4) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f73,hypothesis,(
% 27.73/24.18 e_1356 = select(a_1355,i0) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f74,hypothesis,(
% 27.73/24.18 e_1359 = select(a_1358,i1) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f75,hypothesis,(
% 27.73/24.18 e_1361 = select(a_1358,i2) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f76,hypothesis,(
% 27.73/24.18 e_1363 = select(a_1362,i0) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f77,hypothesis,(
% 27.73/24.18 e_1365 = select(a_1362,i3) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f78,hypothesis,(
% 27.73/24.18 e_1367 = select(a_1366,i9) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f79,hypothesis,(
% 27.73/24.18 e_1369 = select(a_1366,i5) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f80,hypothesis,(
% 27.73/24.18 e_1372 = select(a_1333,i_1371) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f81,hypothesis,(
% 27.73/24.18 e_1373 = select(a_1370,i_1371) ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f83,negated_conjecture,(
% 27.73/24.18 e_1372 != e_1373 ),
% 27.73/24.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.73/24.18 fof(f84,plain,(
% 27.73/24.18 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f1])).
% 27.73/24.18 fof(f87,plain,(
% 27.73/24.18 ![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)))),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f3])).
% 27.73/24.18 fof(f88,plain,(
% 27.73/24.18 a_1296=store(a1,i8,e_1295)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f4])).
% 27.73/24.18 fof(f89,plain,(
% 27.73/24.18 a_1298=store(a_1296,i7,e_1297)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f5])).
% 27.73/24.18 fof(f90,plain,(
% 27.73/24.18 a_1300=store(a_1298,i6,e_1299)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f6])).
% 27.73/24.18 fof(f91,plain,(
% 27.73/24.18 a_1302=store(a_1300,i8,e_1301)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f7])).
% 27.73/24.18 fof(f92,plain,(
% 27.73/24.18 a_1304=store(a_1302,i8,e_1303)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f8])).
% 27.73/24.18 fof(f93,plain,(
% 27.73/24.18 a_1306=store(a_1304,i5,e_1305)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f9])).
% 27.73/24.18 fof(f94,plain,(
% 27.73/24.18 a_1308=store(a_1306,i4,e_1307)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f10])).
% 27.73/24.18 fof(f95,plain,(
% 27.73/24.18 a_1310=store(a_1308,i9,e_1309)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f11])).
% 27.73/24.18 fof(f96,plain,(
% 27.73/24.18 a_1312=store(a_1310,i7,e_1311)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f12])).
% 27.73/24.18 fof(f97,plain,(
% 27.73/24.18 a_1314=store(a_1312,i1,e_1313)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f13])).
% 27.73/24.18 fof(f98,plain,(
% 27.73/24.18 a_1316=store(a_1314,i4,e_1315)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f14])).
% 27.73/24.18 fof(f99,plain,(
% 27.73/24.18 a_1318=store(a_1316,i5,e_1317)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f15])).
% 27.73/24.18 fof(f100,plain,(
% 27.73/24.18 a_1320=store(a_1318,i0,e_1319)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f16])).
% 27.73/24.18 fof(f101,plain,(
% 27.73/24.18 a_1321=store(a_1320,i0,e_1319)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f17])).
% 27.73/24.18 fof(f102,plain,(
% 27.73/24.18 a_1323=store(a_1321,i1,e_1322)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f18])).
% 27.73/24.18 fof(f103,plain,(
% 27.73/24.18 a_1325=store(a_1323,i2,e_1324)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f19])).
% 27.73/24.18 fof(f104,plain,(
% 27.73/24.18 a_1327=store(a_1325,i3,e_1326)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f20])).
% 27.73/24.18 fof(f105,plain,(
% 27.73/24.18 a_1329=store(a_1327,i0,e_1328)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f21])).
% 27.73/24.18 fof(f106,plain,(
% 27.73/24.18 a_1331=store(a_1329,i9,e_1330)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f22])).
% 27.73/24.18 fof(f107,plain,(
% 27.73/24.18 a_1333=store(a_1331,i5,e_1332)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f23])).
% 27.73/24.18 fof(f108,plain,(
% 27.73/24.18 a_1334=store(a1,i7,e_1297)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f24])).
% 27.73/24.18 fof(f109,plain,(
% 27.73/24.18 a_1335=store(a_1334,i8,e_1295)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f25])).
% 27.73/24.18 fof(f110,plain,(
% 27.73/24.18 a_1337=store(a_1335,i6,e_1336)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f26])).
% 27.73/24.18 fof(f111,plain,(
% 27.73/24.18 a_1339=store(a_1337,i8,e_1338)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f27])).
% 27.73/24.18 fof(f112,plain,(
% 27.73/24.18 a_1341=store(a_1339,i5,e_1340)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f28])).
% 27.73/24.18 fof(f113,plain,(
% 27.73/24.18 a_1343=store(a_1341,i8,e_1342)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f29])).
% 27.73/24.18 fof(f114,plain,(
% 27.73/24.18 a_1345=store(a_1343,i4,e_1344)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f30])).
% 27.73/24.18 fof(f115,plain,(
% 27.73/24.18 a_1347=store(a_1345,i9,e_1346)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f31])).
% 27.73/24.18 fof(f116,plain,(
% 27.73/24.18 a_1349=store(a_1347,i1,e_1348)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f32])).
% 27.73/24.18 fof(f117,plain,(
% 27.73/24.18 a_1351=store(a_1349,i7,e_1350)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f33])).
% 27.73/24.18 fof(f118,plain,(
% 27.73/24.18 a_1353=store(a_1351,i4,e_1352)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f34])).
% 27.73/24.18 fof(f119,plain,(
% 27.73/24.18 a_1355=store(a_1353,i5,e_1354)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f35])).
% 27.73/24.18 fof(f120,plain,(
% 27.73/24.18 a_1357=store(a_1355,i0,e_1356)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f36])).
% 27.73/24.18 fof(f121,plain,(
% 27.73/24.18 a_1358=store(a_1357,i0,e_1356)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f37])).
% 27.73/24.18 fof(f122,plain,(
% 27.73/24.18 a_1360=store(a_1358,i2,e_1359)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f38])).
% 27.73/24.18 fof(f123,plain,(
% 27.73/24.18 a_1362=store(a_1360,i1,e_1361)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f39])).
% 27.73/24.18 fof(f124,plain,(
% 27.73/24.18 a_1364=store(a_1362,i3,e_1363)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f40])).
% 27.73/24.18 fof(f125,plain,(
% 27.73/24.18 a_1366=store(a_1364,i0,e_1365)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f41])).
% 27.73/24.18 fof(f126,plain,(
% 27.73/24.18 a_1368=store(a_1366,i5,e_1367)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f42])).
% 27.73/24.18 fof(f127,plain,(
% 27.73/24.18 a_1370=store(a_1368,i9,e_1369)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f43])).
% 27.73/24.18 fof(f128,plain,(
% 27.73/24.18 e_1295=select(a1,i7)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f44])).
% 27.73/24.18 fof(f129,plain,(
% 27.73/24.18 e_1297=select(a1,i8)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f45])).
% 27.73/24.18 fof(f130,plain,(
% 27.73/24.18 e_1299=select(a_1298,i8)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f46])).
% 27.73/24.18 fof(f131,plain,(
% 27.73/24.18 e_1301=select(a_1298,i6)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f47])).
% 27.73/24.18 fof(f132,plain,(
% 27.73/24.18 e_1303=select(a_1302,i5)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f48])).
% 27.73/24.18 fof(f133,plain,(
% 27.73/24.18 e_1305=select(a_1302,i8)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f49])).
% 27.73/24.18 fof(f134,plain,(
% 27.73/24.18 e_1307=select(a_1306,i9)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f50])).
% 27.73/24.18 fof(f135,plain,(
% 27.73/24.18 e_1309=select(a_1306,i4)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f51])).
% 27.73/24.18 fof(f136,plain,(
% 27.73/24.18 e_1311=select(a_1310,i1)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f52])).
% 27.73/24.18 fof(f137,plain,(
% 27.73/24.18 e_1313=select(a_1310,i7)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f53])).
% 27.73/24.18 fof(f138,plain,(
% 27.73/24.18 e_1315=select(a_1314,i5)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f54])).
% 27.73/24.18 fof(f139,plain,(
% 27.73/24.18 e_1317=select(a_1314,i4)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f55])).
% 27.73/24.18 fof(f140,plain,(
% 27.73/24.18 e_1319=select(a_1318,i0)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f56])).
% 27.73/24.18 fof(f141,plain,(
% 27.73/24.18 e_1322=select(a_1321,i2)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f57])).
% 27.73/24.18 fof(f142,plain,(
% 27.73/24.18 e_1324=select(a_1321,i1)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f58])).
% 27.73/24.18 fof(f143,plain,(
% 27.73/24.18 e_1326=select(a_1325,i0)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f59])).
% 27.73/24.18 fof(f144,plain,(
% 27.73/24.18 e_1328=select(a_1325,i3)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f60])).
% 27.73/24.18 fof(f145,plain,(
% 27.73/24.18 e_1330=select(a_1329,i5)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f61])).
% 27.73/24.18 fof(f146,plain,(
% 27.73/24.18 e_1332=select(a_1329,i9)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f62])).
% 27.73/24.18 fof(f147,plain,(
% 27.73/24.18 e_1336=select(a_1335,i8)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f63])).
% 27.73/24.18 fof(f148,plain,(
% 27.73/24.18 e_1338=select(a_1335,i6)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f64])).
% 27.73/24.18 fof(f149,plain,(
% 27.73/24.18 e_1340=select(a_1339,i8)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f65])).
% 27.73/24.18 fof(f150,plain,(
% 27.73/24.18 e_1342=select(a_1339,i5)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f66])).
% 27.73/24.18 fof(f151,plain,(
% 27.73/24.18 e_1344=select(a_1343,i9)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f67])).
% 27.73/24.18 fof(f152,plain,(
% 27.73/24.18 e_1346=select(a_1343,i4)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f68])).
% 27.73/24.18 fof(f153,plain,(
% 27.73/24.18 e_1348=select(a_1347,i7)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f69])).
% 27.73/24.18 fof(f154,plain,(
% 27.73/24.18 e_1350=select(a_1347,i1)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f70])).
% 27.73/24.18 fof(f155,plain,(
% 27.73/24.18 e_1352=select(a_1351,i5)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f71])).
% 27.73/24.18 fof(f156,plain,(
% 27.73/24.18 e_1354=select(a_1351,i4)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f72])).
% 27.73/24.18 fof(f157,plain,(
% 27.73/24.18 e_1356=select(a_1355,i0)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f73])).
% 27.73/24.18 fof(f158,plain,(
% 27.73/24.18 e_1359=select(a_1358,i1)),
% 27.73/24.18 inference(cnf_transformation,[status(thm)],[f74])).
% 27.73/24.18 fof(f159,plain,(
% 27.73/24.18 e_1361=select(a_1358,i2)),
% 27.73/24.19 inference(cnf_transformation,[status(thm)],[f75])).
% 27.73/24.19 fof(f160,plain,(
% 27.73/24.19 e_1363=select(a_1362,i0)),
% 27.73/24.19 inference(cnf_transformation,[status(thm)],[f76])).
% 27.73/24.19 fof(f161,plain,(
% 27.73/24.19 e_1365=select(a_1362,i3)),
% 27.73/24.19 inference(cnf_transformation,[status(thm)],[f77])).
% 27.73/24.19 fof(f162,plain,(
% 27.73/24.19 e_1367=select(a_1366,i9)),
% 27.73/24.19 inference(cnf_transformation,[status(thm)],[f78])).
% 27.73/24.19 fof(f163,plain,(
% 27.73/24.19 e_1369=select(a_1366,i5)),
% 27.73/24.19 inference(cnf_transformation,[status(thm)],[f79])).
% 27.73/24.19 fof(f164,plain,(
% 27.73/24.19 e_1372=select(a_1333,i_1371)),
% 27.73/24.19 inference(cnf_transformation,[status(thm)],[f80])).
% 27.73/24.19 fof(f165,plain,(
% 27.73/24.19 e_1373=select(a_1370,i_1371)),
% 27.73/24.19 inference(cnf_transformation,[status(thm)],[f81])).
% 27.73/24.19 fof(f167,plain,(
% 27.73/24.19 ~e_1372=e_1373),
% 27.73/24.19 inference(cnf_transformation,[status(thm)],[f83])).
% 27.73/24.19 fof(f174,plain,(
% 27.73/24.19 ![X0]: (store(store(a1,X0,e_1297),i8,select(a1,X0))=store(store(a1,i8,select(a1,X0)),X0,select(a1,i8)))),
% 27.73/24.19 inference(paramodulation,[status(thm)],[f129,f87])).
% 27.73/24.19 fof(f203,plain,(
% 27.73/24.19 ![X0]: (store(store(a1,X0,e_1297),i8,select(a1,X0))=store(store(a1,i8,select(a1,X0)),X0,e_1297))),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f129,f174])).
% 27.73/24.19 fof(f256,plain,(
% 27.73/24.19 select(a_1302,i8)=e_1301),
% 27.73/24.19 inference(paramodulation,[status(thm)],[f91,f84])).
% 27.73/24.19 fof(f290,plain,(
% 27.73/24.19 ![X0]: (store(store(a_1302,X0,select(a_1302,i8)),i8,select(a_1302,X0))=store(store(a_1302,i8,select(a_1302,X0)),X0,e_1305))),
% 27.73/24.19 inference(paramodulation,[status(thm)],[f133,f87])).
% 27.73/24.19 fof(f294,plain,(
% 27.73/24.19 ![X0]: (store(store(a_1302,X0,e_1305),i8,select(a_1302,X0))=store(store(a_1302,i8,select(a_1302,X0)),X0,e_1305))),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f133,f290])).
% 27.73/24.19 fof(f399,plain,(
% 27.73/24.19 ![X0]: (store(store(a_1310,X0,select(a_1310,i7)),i7,select(a_1310,X0))=store(store(a_1310,i7,select(a_1310,X0)),X0,e_1313))),
% 27.73/24.19 inference(paramodulation,[status(thm)],[f137,f87])).
% 27.73/24.19 fof(f403,plain,(
% 27.73/24.19 ![X0]: (store(store(a_1310,X0,e_1313),i7,select(a_1310,X0))=store(store(a_1310,i7,select(a_1310,X0)),X0,e_1313))),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f137,f399])).
% 27.73/24.19 fof(f687,plain,(
% 27.73/24.19 ![X0]: (store(store(a_1321,X0,select(a_1321,i1)),i1,select(a_1321,X0))=store(store(a_1321,i1,select(a_1321,X0)),X0,e_1324))),
% 27.73/24.19 inference(paramodulation,[status(thm)],[f142,f87])).
% 27.73/24.19 fof(f691,plain,(
% 27.73/24.19 ![X0]: (store(store(a_1321,X0,e_1324),i1,select(a_1321,X0))=store(store(a_1321,i1,select(a_1321,X0)),X0,e_1324))),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f142,f687])).
% 27.73/24.19 fof(f865,plain,(
% 27.73/24.19 ![X0]: (store(store(a_1329,X0,select(a_1329,i9)),i9,select(a_1329,X0))=store(store(a_1329,i9,select(a_1329,X0)),X0,e_1332))),
% 27.73/24.19 inference(paramodulation,[status(thm)],[f146,f87])).
% 27.73/24.19 fof(f869,plain,(
% 27.73/24.19 ![X0]: (store(store(a_1329,X0,e_1332),i9,select(a_1329,X0))=store(store(a_1329,i9,select(a_1329,X0)),X0,e_1332))),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f146,f865])).
% 27.73/24.19 fof(f2752,plain,(
% 27.73/24.19 store(store(a1,i7,e_1297),i8,select(a1,i7))=store(store(a1,i8,e_1295),i7,e_1297)),
% 27.73/24.19 inference(paramodulation,[status(thm)],[f128,f203])).
% 27.73/24.19 fof(f2760,plain,(
% 27.73/24.19 store(a_1334,i8,select(a1,i7))=store(store(a1,i8,e_1295),i7,e_1297)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f108,f2752])).
% 27.73/24.19 fof(f2761,plain,(
% 27.73/24.19 store(a_1334,i8,e_1295)=store(store(a1,i8,e_1295),i7,e_1297)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f128,f2760])).
% 27.73/24.19 fof(f2762,plain,(
% 27.73/24.19 a_1335=store(store(a1,i8,e_1295),i7,e_1297)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f109,f2761])).
% 27.73/24.19 fof(f2763,plain,(
% 27.73/24.19 a_1335=store(a_1296,i7,e_1297)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f88,f2762])).
% 27.73/24.19 fof(f2764,plain,(
% 27.73/24.19 a_1335=a_1298),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f89,f2763])).
% 27.73/24.19 fof(f4020,plain,(
% 27.73/24.19 e_1338=select(a_1298,i6)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f2764,f148])).
% 27.73/24.19 fof(f4021,plain,(
% 27.73/24.19 e_1336=select(a_1298,i8)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f2764,f147])).
% 27.73/24.19 fof(f4022,plain,(
% 27.73/24.19 a_1337=store(a_1298,i6,e_1336)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f2764,f110])).
% 27.73/24.19 fof(f4024,plain,(
% 27.73/24.19 e_1338=e_1301),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f131,f4020])).
% 27.73/24.19 fof(f4025,plain,(
% 27.73/24.19 e_1336=e_1299),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f130,f4021])).
% 27.73/24.19 fof(f4026,plain,(
% 27.73/24.19 a_1339=store(a_1337,i8,e_1301)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f4024,f111])).
% 27.73/24.19 fof(f4027,plain,(
% 27.73/24.19 a_1337=store(a_1298,i6,e_1299)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f4025,f4022])).
% 27.73/24.19 fof(f4028,plain,(
% 27.73/24.19 a_1337=a_1300),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f90,f4027])).
% 27.73/24.19 fof(f4069,plain,(
% 27.73/24.19 a_1339=store(a_1300,i8,e_1301)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f4028,f4026])).
% 27.73/24.19 fof(f4070,plain,(
% 27.73/24.19 e_1342=select(a_1302,i5)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f4073,f150])).
% 27.73/24.19 fof(f4071,plain,(
% 27.73/24.19 e_1340=select(a_1302,i8)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f4073,f149])).
% 27.73/24.19 fof(f4072,plain,(
% 27.73/24.19 a_1341=store(a_1302,i5,e_1340)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f4073,f112])).
% 27.73/24.19 fof(f4073,plain,(
% 27.73/24.19 a_1339=a_1302),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f91,f4069])).
% 27.73/24.19 fof(f4074,plain,(
% 27.73/24.19 e_1342=e_1303),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f132,f4070])).
% 27.73/24.19 fof(f4075,plain,(
% 27.73/24.19 e_1340=e_1305),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f133,f4071])).
% 27.73/24.19 fof(f4076,plain,(
% 27.73/24.19 a_1343=store(a_1341,i8,e_1303)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f4074,f113])).
% 27.73/24.19 fof(f4077,plain,(
% 27.73/24.19 a_1341=store(a_1302,i5,e_1305)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f4075,f4072])).
% 27.73/24.19 fof(f4701,plain,(
% 27.73/24.19 e_1305=e_1301),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f256,f133])).
% 27.73/24.19 fof(f4710,plain,(
% 27.73/24.19 a_1341=store(a_1302,i5,e_1301)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f4701,f4077])).
% 27.73/24.19 fof(f4712,plain,(
% 27.73/24.19 a_1306=store(a_1304,i5,e_1301)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f4701,f93])).
% 27.73/24.19 fof(f6674,plain,(
% 27.73/24.19 ![X0]: (store(store(a_1302,X0,e_1301),i8,select(a_1302,X0))=store(store(a_1302,i8,select(a_1302,X0)),X0,e_1305))),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f4701,f294])).
% 27.73/24.19 fof(f6675,plain,(
% 27.73/24.19 ![X0]: (store(store(a_1302,X0,e_1301),i8,select(a_1302,X0))=store(store(a_1302,i8,select(a_1302,X0)),X0,e_1301))),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f4701,f6674])).
% 27.73/24.19 fof(f6677,plain,(
% 27.73/24.19 store(store(a_1302,i5,e_1301),i8,select(a_1302,i5))=store(store(a_1302,i8,e_1303),i5,e_1301)),
% 27.73/24.19 inference(paramodulation,[status(thm)],[f132,f6675])).
% 27.73/24.19 fof(f6689,plain,(
% 27.73/24.19 store(a_1341,i8,select(a_1302,i5))=store(store(a_1302,i8,e_1303),i5,e_1301)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f4710,f6677])).
% 27.73/24.19 fof(f6690,plain,(
% 27.73/24.19 store(a_1341,i8,e_1303)=store(store(a_1302,i8,e_1303),i5,e_1301)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f132,f6689])).
% 27.73/24.19 fof(f6691,plain,(
% 27.73/24.19 a_1343=store(store(a_1302,i8,e_1303),i5,e_1301)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f4076,f6690])).
% 27.73/24.19 fof(f6692,plain,(
% 27.73/24.19 a_1343=store(a_1304,i5,e_1301)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f92,f6691])).
% 27.73/24.19 fof(f6693,plain,(
% 27.73/24.19 a_1343=a_1306),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f4712,f6692])).
% 27.73/24.19 fof(f6812,plain,(
% 27.73/24.19 e_1346=select(a_1306,i4)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f6693,f152])).
% 27.73/24.19 fof(f6813,plain,(
% 27.73/24.19 e_1344=select(a_1306,i9)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f6693,f151])).
% 27.73/24.19 fof(f6814,plain,(
% 27.73/24.19 a_1345=store(a_1306,i4,e_1344)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f6693,f114])).
% 27.73/24.19 fof(f6815,plain,(
% 27.73/24.19 e_1346=e_1309),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f135,f6812])).
% 27.73/24.19 fof(f6816,plain,(
% 27.73/24.19 e_1344=e_1307),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f134,f6813])).
% 27.73/24.19 fof(f6817,plain,(
% 27.73/24.19 a_1347=store(a_1345,i9,e_1309)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f6815,f115])).
% 27.73/24.19 fof(f6858,plain,(
% 27.73/24.19 a_1345=store(a_1306,i4,e_1307)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f6816,f6814])).
% 27.73/24.19 fof(f6859,plain,(
% 27.73/24.19 a_1345=a_1308),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f94,f6858])).
% 27.73/24.19 fof(f6860,plain,(
% 27.73/24.19 a_1347=store(a_1308,i9,e_1309)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f6859,f6817])).
% 27.73/24.19 fof(f6861,plain,(
% 27.73/24.19 e_1350=select(a_1310,i1)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f6864,f154])).
% 27.73/24.19 fof(f6862,plain,(
% 27.73/24.19 e_1348=select(a_1310,i7)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f6864,f153])).
% 27.73/24.19 fof(f6863,plain,(
% 27.73/24.19 a_1349=store(a_1310,i1,e_1348)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f6864,f116])).
% 27.73/24.19 fof(f6864,plain,(
% 27.73/24.19 a_1347=a_1310),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f95,f6860])).
% 27.73/24.19 fof(f6865,plain,(
% 27.73/24.19 e_1350=e_1311),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f136,f6861])).
% 27.73/24.19 fof(f6866,plain,(
% 27.73/24.19 e_1348=e_1313),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f137,f6862])).
% 27.73/24.19 fof(f6867,plain,(
% 27.73/24.19 a_1351=store(a_1349,i7,e_1311)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f6865,f117])).
% 27.73/24.19 fof(f6868,plain,(
% 27.73/24.19 a_1349=store(a_1310,i1,e_1313)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f6866,f6863])).
% 27.73/24.19 fof(f8707,plain,(
% 27.73/24.19 store(store(a_1310,i1,e_1313),i7,select(a_1310,i1))=store(store(a_1310,i7,e_1311),i1,e_1313)),
% 27.73/24.19 inference(paramodulation,[status(thm)],[f136,f403])).
% 27.73/24.19 fof(f8720,plain,(
% 27.73/24.19 store(a_1349,i7,select(a_1310,i1))=store(store(a_1310,i7,e_1311),i1,e_1313)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f6868,f8707])).
% 27.73/24.19 fof(f8721,plain,(
% 27.73/24.19 store(a_1349,i7,e_1311)=store(store(a_1310,i7,e_1311),i1,e_1313)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f136,f8720])).
% 27.73/24.19 fof(f8722,plain,(
% 27.73/24.19 a_1351=store(store(a_1310,i7,e_1311),i1,e_1313)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f6867,f8721])).
% 27.73/24.19 fof(f8723,plain,(
% 27.73/24.19 a_1351=store(a_1312,i1,e_1313)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f96,f8722])).
% 27.73/24.19 fof(f8724,plain,(
% 27.73/24.19 a_1351=a_1314),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f97,f8723])).
% 27.73/24.19 fof(f8995,plain,(
% 27.73/24.19 e_1354=select(a_1314,i4)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f8724,f156])).
% 27.73/24.19 fof(f8996,plain,(
% 27.73/24.19 e_1352=select(a_1314,i5)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f8724,f155])).
% 27.73/24.19 fof(f8997,plain,(
% 27.73/24.19 a_1353=store(a_1314,i4,e_1352)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f8724,f118])).
% 27.73/24.19 fof(f8998,plain,(
% 27.73/24.19 e_1354=e_1317),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f139,f8995])).
% 27.73/24.19 fof(f8999,plain,(
% 27.73/24.19 e_1352=e_1315),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f138,f8996])).
% 27.73/24.19 fof(f9000,plain,(
% 27.73/24.19 a_1355=store(a_1353,i5,e_1317)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f8998,f119])).
% 27.73/24.19 fof(f9042,plain,(
% 27.73/24.19 a_1353=store(a_1314,i4,e_1315)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f8999,f8997])).
% 27.73/24.19 fof(f9043,plain,(
% 27.73/24.19 a_1353=a_1316),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f98,f9042])).
% 27.73/24.19 fof(f9044,plain,(
% 27.73/24.19 a_1355=store(a_1316,i5,e_1317)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f9043,f9000])).
% 27.73/24.19 fof(f9045,plain,(
% 27.73/24.19 e_1356=select(a_1318,i0)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f9047,f157])).
% 27.73/24.19 fof(f9046,plain,(
% 27.73/24.19 a_1357=store(a_1318,i0,e_1356)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f9047,f120])).
% 27.73/24.19 fof(f9047,plain,(
% 27.73/24.19 a_1355=a_1318),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f99,f9044])).
% 27.73/24.19 fof(f9048,plain,(
% 27.73/24.19 e_1356=e_1319),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f140,f9045])).
% 27.73/24.19 fof(f9049,plain,(
% 27.73/24.19 a_1358=store(a_1357,i0,e_1319)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f9048,f121])).
% 27.73/24.19 fof(f9050,plain,(
% 27.73/24.19 a_1357=store(a_1318,i0,e_1319)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f9048,f9046])).
% 27.73/24.19 fof(f9051,plain,(
% 27.73/24.19 a_1357=a_1320),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f100,f9050])).
% 27.73/24.19 fof(f9052,plain,(
% 27.73/24.19 a_1358=store(a_1320,i0,e_1319)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f9051,f9049])).
% 27.73/24.19 fof(f9053,plain,(
% 27.73/24.19 e_1361=select(a_1321,i2)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f9056,f159])).
% 27.73/24.19 fof(f9054,plain,(
% 27.73/24.19 e_1359=select(a_1321,i1)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f9056,f158])).
% 27.73/24.19 fof(f9055,plain,(
% 27.73/24.19 a_1360=store(a_1321,i2,e_1359)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f9056,f122])).
% 27.73/24.19 fof(f9056,plain,(
% 27.73/24.19 a_1358=a_1321),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f101,f9052])).
% 27.73/24.19 fof(f9057,plain,(
% 27.73/24.19 e_1361=e_1322),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f141,f9053])).
% 27.73/24.19 fof(f9058,plain,(
% 27.73/24.19 e_1359=e_1324),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f142,f9054])).
% 27.73/24.19 fof(f9106,plain,(
% 27.73/24.19 a_1362=store(a_1360,i1,e_1322)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f9057,f123])).
% 27.73/24.19 fof(f9109,plain,(
% 27.73/24.19 a_1360=store(a_1321,i2,e_1324)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f9058,f9055])).
% 27.73/24.19 fof(f14532,plain,(
% 27.73/24.19 store(store(a_1321,i2,e_1324),i1,select(a_1321,i2))=store(store(a_1321,i1,e_1322),i2,e_1324)),
% 27.73/24.19 inference(paramodulation,[status(thm)],[f141,f691])).
% 27.73/24.19 fof(f14545,plain,(
% 27.73/24.19 store(a_1360,i1,select(a_1321,i2))=store(store(a_1321,i1,e_1322),i2,e_1324)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f9109,f14532])).
% 27.73/24.19 fof(f14546,plain,(
% 27.73/24.19 store(a_1360,i1,e_1322)=store(store(a_1321,i1,e_1322),i2,e_1324)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f141,f14545])).
% 27.73/24.19 fof(f14547,plain,(
% 27.73/24.19 a_1362=store(store(a_1321,i1,e_1322),i2,e_1324)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f9106,f14546])).
% 27.73/24.19 fof(f14548,plain,(
% 27.73/24.19 a_1362=store(a_1323,i2,e_1324)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f102,f14547])).
% 27.73/24.19 fof(f14549,plain,(
% 27.73/24.19 a_1362=a_1325),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f103,f14548])).
% 27.73/24.19 fof(f14652,plain,(
% 27.73/24.19 e_1365=select(a_1325,i3)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f14549,f161])).
% 27.73/24.19 fof(f14653,plain,(
% 27.73/24.19 e_1363=select(a_1325,i0)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f14549,f160])).
% 27.73/24.19 fof(f14654,plain,(
% 27.73/24.19 a_1364=store(a_1325,i3,e_1363)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f14549,f124])).
% 27.73/24.19 fof(f14655,plain,(
% 27.73/24.19 e_1365=e_1328),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f144,f14652])).
% 27.73/24.19 fof(f14656,plain,(
% 27.73/24.19 e_1363=e_1326),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f143,f14653])).
% 27.73/24.19 fof(f14658,plain,(
% 27.73/24.19 a_1366=store(a_1364,i0,e_1328)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f14655,f125])).
% 27.73/24.19 fof(f14700,plain,(
% 27.73/24.19 a_1364=store(a_1325,i3,e_1326)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f14656,f14654])).
% 27.73/24.19 fof(f14701,plain,(
% 27.73/24.19 a_1364=a_1327),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f104,f14700])).
% 27.73/24.19 fof(f14702,plain,(
% 27.73/24.19 a_1366=store(a_1327,i0,e_1328)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f14701,f14658])).
% 27.73/24.19 fof(f14703,plain,(
% 27.73/24.19 e_1369=select(a_1329,i5)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f14706,f163])).
% 27.73/24.19 fof(f14704,plain,(
% 27.73/24.19 e_1367=select(a_1329,i9)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f14706,f162])).
% 27.73/24.19 fof(f14705,plain,(
% 27.73/24.19 a_1368=store(a_1329,i5,e_1367)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f14706,f126])).
% 27.73/24.19 fof(f14706,plain,(
% 27.73/24.19 a_1366=a_1329),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f105,f14702])).
% 27.73/24.19 fof(f14707,plain,(
% 27.73/24.19 e_1369=e_1330),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f145,f14703])).
% 27.73/24.19 fof(f14708,plain,(
% 27.73/24.19 e_1367=e_1332),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f146,f14704])).
% 27.73/24.19 fof(f14718,plain,(
% 27.73/24.19 a_1370=store(a_1368,i9,e_1330)),
% 27.73/24.19 inference(backward_demodulation,[status(thm)],[f14707,f127])).
% 27.73/24.19 fof(f14735,plain,(
% 27.73/24.19 a_1368=store(a_1329,i5,e_1332)),
% 27.73/24.19 inference(forward_demodulation,[status(thm)],[f14708,f14705])).
% 27.73/24.19 fof(f16120,plain,(
% 27.73/24.19 store(store(a_1329,i5,e_1332),i9,select(a_1329,i5))=store(store(a_1329,i9,e_1330),i5,e_1332)),
% 27.73/24.19 inference(paramodulation,[status(thm)],[f145,f869])).
% 27.73/24.19 fof(f16133,plain,(
% 27.73/24.22 store(a_1368,i9,select(a_1329,i5))=store(store(a_1329,i9,e_1330),i5,e_1332)),
% 27.73/24.22 inference(forward_demodulation,[status(thm)],[f14735,f16120])).
% 27.73/24.22 fof(f16134,plain,(
% 27.73/24.22 store(a_1368,i9,e_1330)=store(store(a_1329,i9,e_1330),i5,e_1332)),
% 27.73/24.22 inference(forward_demodulation,[status(thm)],[f145,f16133])).
% 27.73/24.22 fof(f16135,plain,(
% 27.73/24.22 a_1370=store(store(a_1329,i9,e_1330),i5,e_1332)),
% 27.73/24.22 inference(forward_demodulation,[status(thm)],[f14718,f16134])).
% 27.73/24.22 fof(f16136,plain,(
% 27.73/24.22 a_1370=store(a_1331,i5,e_1332)),
% 27.73/24.22 inference(forward_demodulation,[status(thm)],[f106,f16135])).
% 27.73/24.22 fof(f16137,plain,(
% 27.73/24.22 a_1370=a_1333),
% 27.73/24.22 inference(forward_demodulation,[status(thm)],[f107,f16136])).
% 27.73/24.22 fof(f16352,plain,(
% 27.73/24.22 e_1373=select(a_1333,i_1371)),
% 27.73/24.22 inference(backward_demodulation,[status(thm)],[f16137,f165])).
% 27.73/24.22 fof(f16830,plain,(
% 27.73/24.22 e_1373=e_1372),
% 27.73/24.22 inference(forward_demodulation,[status(thm)],[f164,f16352])).
% 27.73/24.22 fof(f16831,plain,(
% 27.73/24.22 $false),
% 27.73/24.22 inference(forward_subsumption_resolution,[status(thm)],[f16830,f167])).
% 27.73/24.22 % SZS output end CNFRefutation for theBenchmark.p
% 10.58/24.27 % Elapsed time: 3.666088 seconds
% 10.58/24.27 % CPU time: 28.764860 seconds
% 10.58/24.27 % Total memory used: 514.401 MB
% 10.58/24.27 % Net memory used: 501.116 MB
%------------------------------------------------------------------------------