%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV543-1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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:38 PM UTC 2026
% Result : Unsatisfiable 23.96s 3.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV543-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n012.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 09:04:37 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 23.96/3.49 % Refutation found
% 23.96/3.49 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 23.96/3.49 % SZS output start CNFRefutation for theBenchmark
% 23.96/3.49 fof(f1,axiom,(
% 23.96/3.49 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f3,axiom,(
% 23.96/3.49 (![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)) ))),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f4,hypothesis,(
% 23.96/3.49 a_1245 = store(a1,i8,e_1244) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f5,hypothesis,(
% 23.96/3.49 a_1247 = store(a_1245,i7,e_1246) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f6,hypothesis,(
% 23.96/3.49 a_1249 = store(a_1247,i6,e_1248) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f7,hypothesis,(
% 23.96/3.49 a_1251 = store(a_1249,i8,e_1250) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f8,hypothesis,(
% 23.96/3.49 a_1253 = store(a_1251,i8,e_1252) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f9,hypothesis,(
% 23.96/3.49 a_1255 = store(a_1253,i5,e_1254) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f10,hypothesis,(
% 23.96/3.49 a_1257 = store(a_1255,i4,e_1256) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f11,hypothesis,(
% 23.96/3.49 a_1259 = store(a_1257,i9,e_1258) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f12,hypothesis,(
% 23.96/3.49 a_1261 = store(a_1259,i7,e_1260) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f13,hypothesis,(
% 23.96/3.49 a_1263 = store(a_1261,i1,e_1262) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f14,hypothesis,(
% 23.96/3.49 a_1265 = store(a_1263,i4,e_1264) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f15,hypothesis,(
% 23.96/3.49 a_1267 = store(a_1265,i5,e_1266) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f16,hypothesis,(
% 23.96/3.49 a_1269 = store(a_1267,i0,e_1268) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f17,hypothesis,(
% 23.96/3.49 a_1270 = store(a_1269,i0,e_1268) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f18,hypothesis,(
% 23.96/3.49 a_1272 = store(a_1270,i1,e_1271) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f19,hypothesis,(
% 23.96/3.49 a_1274 = store(a_1272,i2,e_1273) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f20,hypothesis,(
% 23.96/3.49 a_1276 = store(a_1274,i3,e_1275) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f21,hypothesis,(
% 23.96/3.49 a_1278 = store(a_1276,i0,e_1277) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f22,hypothesis,(
% 23.96/3.49 a_1280 = store(a_1278,i9,e_1279) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f23,hypothesis,(
% 23.96/3.49 a_1282 = store(a_1280,i5,e_1281) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f24,hypothesis,(
% 23.96/3.49 a_1283 = store(a1,i7,e_1246) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f25,hypothesis,(
% 23.96/3.49 a_1284 = store(a_1283,i8,e_1244) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f26,hypothesis,(
% 23.96/3.49 a_1286 = store(a_1284,i6,e_1285) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f27,hypothesis,(
% 23.96/3.49 a_1288 = store(a_1286,i8,e_1287) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f28,hypothesis,(
% 23.96/3.49 a_1290 = store(a_1288,i5,e_1289) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f29,hypothesis,(
% 23.96/3.49 a_1292 = store(a_1290,i8,e_1291) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f30,hypothesis,(
% 23.96/3.49 a_1294 = store(a_1292,i4,e_1293) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f31,hypothesis,(
% 23.96/3.49 a_1296 = store(a_1294,i9,e_1295) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f32,hypothesis,(
% 23.96/3.49 a_1298 = store(a_1296,i1,e_1297) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f33,hypothesis,(
% 23.96/3.49 a_1300 = store(a_1298,i7,e_1299) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f34,hypothesis,(
% 23.96/3.49 a_1302 = store(a_1300,i4,e_1301) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f35,hypothesis,(
% 23.96/3.49 a_1304 = store(a_1302,i5,e_1303) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f36,hypothesis,(
% 23.96/3.49 a_1306 = store(a_1304,i0,e_1305) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f37,hypothesis,(
% 23.96/3.49 a_1307 = store(a_1306,i0,e_1305) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f38,hypothesis,(
% 23.96/3.49 a_1309 = store(a_1307,i2,e_1308) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f39,hypothesis,(
% 23.96/3.49 a_1311 = store(a_1309,i1,e_1310) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f40,hypothesis,(
% 23.96/3.49 a_1313 = store(a_1311,i3,e_1312) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f41,hypothesis,(
% 23.96/3.49 a_1315 = store(a_1313,i0,e_1314) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f42,hypothesis,(
% 23.96/3.49 a_1317 = store(a_1315,i5,e_1316) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f43,hypothesis,(
% 23.96/3.49 a_1319 = store(a_1317,i9,e_1318) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f44,hypothesis,(
% 23.96/3.49 e_1244 = select(a1,i7) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f45,hypothesis,(
% 23.96/3.49 e_1246 = select(a1,i8) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f46,hypothesis,(
% 23.96/3.49 e_1248 = select(a_1247,i8) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f47,hypothesis,(
% 23.96/3.49 e_1250 = select(a_1247,i6) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f48,hypothesis,(
% 23.96/3.49 e_1252 = select(a_1251,i5) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f49,hypothesis,(
% 23.96/3.49 e_1254 = select(a_1251,i8) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f50,hypothesis,(
% 23.96/3.49 e_1256 = select(a_1255,i9) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f51,hypothesis,(
% 23.96/3.49 e_1258 = select(a_1255,i4) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f52,hypothesis,(
% 23.96/3.49 e_1260 = select(a_1259,i1) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f53,hypothesis,(
% 23.96/3.49 e_1262 = select(a_1259,i7) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f54,hypothesis,(
% 23.96/3.49 e_1264 = select(a_1263,i5) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f55,hypothesis,(
% 23.96/3.49 e_1266 = select(a_1263,i4) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f56,hypothesis,(
% 23.96/3.49 e_1268 = select(a_1267,i0) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f57,hypothesis,(
% 23.96/3.49 e_1271 = select(a_1270,i2) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f58,hypothesis,(
% 23.96/3.49 e_1273 = select(a_1270,i1) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f59,hypothesis,(
% 23.96/3.49 e_1275 = select(a_1274,i0) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f60,hypothesis,(
% 23.96/3.49 e_1277 = select(a_1274,i3) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f61,hypothesis,(
% 23.96/3.49 e_1279 = select(a_1278,i5) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f62,hypothesis,(
% 23.96/3.49 e_1281 = select(a_1278,i9) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f63,hypothesis,(
% 23.96/3.49 e_1285 = select(a_1284,i8) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f64,hypothesis,(
% 23.96/3.49 e_1287 = select(a_1284,i6) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f65,hypothesis,(
% 23.96/3.49 e_1289 = select(a_1288,i8) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f66,hypothesis,(
% 23.96/3.49 e_1291 = select(a_1288,i5) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f67,hypothesis,(
% 23.96/3.49 e_1293 = select(a_1292,i9) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f68,hypothesis,(
% 23.96/3.49 e_1295 = select(a_1292,i4) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f69,hypothesis,(
% 23.96/3.49 e_1297 = select(a_1296,i7) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f70,hypothesis,(
% 23.96/3.49 e_1299 = select(a_1296,i1) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f71,hypothesis,(
% 23.96/3.49 e_1301 = select(a_1300,i5) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f72,hypothesis,(
% 23.96/3.49 e_1303 = select(a_1300,i4) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f73,hypothesis,(
% 23.96/3.49 e_1305 = select(a_1304,i0) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f74,hypothesis,(
% 23.96/3.49 e_1308 = select(a_1307,i1) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f75,hypothesis,(
% 23.96/3.49 e_1310 = select(a_1307,i2) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f76,hypothesis,(
% 23.96/3.49 e_1312 = select(a_1311,i0) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f77,hypothesis,(
% 23.96/3.49 e_1314 = select(a_1311,i3) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f78,hypothesis,(
% 23.96/3.49 e_1316 = select(a_1315,i9) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f79,hypothesis,(
% 23.96/3.49 e_1318 = select(a_1315,i5) ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f80,negated_conjecture,(
% 23.96/3.49 a_1282 != a_1319 ),
% 23.96/3.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 23.96/3.49 fof(f81,plain,(
% 23.96/3.49 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f1])).
% 23.96/3.49 fof(f84,plain,(
% 23.96/3.49 ![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)))),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f3])).
% 23.96/3.49 fof(f85,plain,(
% 23.96/3.49 a_1245=store(a1,i8,e_1244)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f4])).
% 23.96/3.49 fof(f86,plain,(
% 23.96/3.49 a_1247=store(a_1245,i7,e_1246)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f5])).
% 23.96/3.49 fof(f87,plain,(
% 23.96/3.49 a_1249=store(a_1247,i6,e_1248)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f6])).
% 23.96/3.49 fof(f88,plain,(
% 23.96/3.49 a_1251=store(a_1249,i8,e_1250)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f7])).
% 23.96/3.49 fof(f89,plain,(
% 23.96/3.49 a_1253=store(a_1251,i8,e_1252)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f8])).
% 23.96/3.49 fof(f90,plain,(
% 23.96/3.49 a_1255=store(a_1253,i5,e_1254)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f9])).
% 23.96/3.49 fof(f91,plain,(
% 23.96/3.49 a_1257=store(a_1255,i4,e_1256)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f10])).
% 23.96/3.49 fof(f92,plain,(
% 23.96/3.49 a_1259=store(a_1257,i9,e_1258)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f11])).
% 23.96/3.49 fof(f93,plain,(
% 23.96/3.49 a_1261=store(a_1259,i7,e_1260)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f12])).
% 23.96/3.49 fof(f94,plain,(
% 23.96/3.49 a_1263=store(a_1261,i1,e_1262)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f13])).
% 23.96/3.49 fof(f95,plain,(
% 23.96/3.49 a_1265=store(a_1263,i4,e_1264)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f14])).
% 23.96/3.49 fof(f96,plain,(
% 23.96/3.49 a_1267=store(a_1265,i5,e_1266)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f15])).
% 23.96/3.49 fof(f97,plain,(
% 23.96/3.49 a_1269=store(a_1267,i0,e_1268)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f16])).
% 23.96/3.49 fof(f98,plain,(
% 23.96/3.49 a_1270=store(a_1269,i0,e_1268)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f17])).
% 23.96/3.49 fof(f99,plain,(
% 23.96/3.49 a_1272=store(a_1270,i1,e_1271)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f18])).
% 23.96/3.49 fof(f100,plain,(
% 23.96/3.49 a_1274=store(a_1272,i2,e_1273)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f19])).
% 23.96/3.49 fof(f101,plain,(
% 23.96/3.49 a_1276=store(a_1274,i3,e_1275)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f20])).
% 23.96/3.49 fof(f102,plain,(
% 23.96/3.49 a_1278=store(a_1276,i0,e_1277)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f21])).
% 23.96/3.49 fof(f103,plain,(
% 23.96/3.49 a_1280=store(a_1278,i9,e_1279)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f22])).
% 23.96/3.49 fof(f104,plain,(
% 23.96/3.49 a_1282=store(a_1280,i5,e_1281)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f23])).
% 23.96/3.49 fof(f105,plain,(
% 23.96/3.49 a_1283=store(a1,i7,e_1246)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f24])).
% 23.96/3.49 fof(f106,plain,(
% 23.96/3.49 a_1284=store(a_1283,i8,e_1244)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f25])).
% 23.96/3.49 fof(f107,plain,(
% 23.96/3.49 a_1286=store(a_1284,i6,e_1285)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f26])).
% 23.96/3.49 fof(f108,plain,(
% 23.96/3.49 a_1288=store(a_1286,i8,e_1287)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f27])).
% 23.96/3.49 fof(f109,plain,(
% 23.96/3.49 a_1290=store(a_1288,i5,e_1289)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f28])).
% 23.96/3.49 fof(f110,plain,(
% 23.96/3.49 a_1292=store(a_1290,i8,e_1291)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f29])).
% 23.96/3.49 fof(f111,plain,(
% 23.96/3.49 a_1294=store(a_1292,i4,e_1293)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f30])).
% 23.96/3.49 fof(f112,plain,(
% 23.96/3.49 a_1296=store(a_1294,i9,e_1295)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f31])).
% 23.96/3.49 fof(f113,plain,(
% 23.96/3.49 a_1298=store(a_1296,i1,e_1297)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f32])).
% 23.96/3.49 fof(f114,plain,(
% 23.96/3.49 a_1300=store(a_1298,i7,e_1299)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f33])).
% 23.96/3.49 fof(f115,plain,(
% 23.96/3.49 a_1302=store(a_1300,i4,e_1301)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f34])).
% 23.96/3.49 fof(f116,plain,(
% 23.96/3.49 a_1304=store(a_1302,i5,e_1303)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f35])).
% 23.96/3.49 fof(f117,plain,(
% 23.96/3.49 a_1306=store(a_1304,i0,e_1305)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f36])).
% 23.96/3.49 fof(f118,plain,(
% 23.96/3.49 a_1307=store(a_1306,i0,e_1305)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f37])).
% 23.96/3.49 fof(f119,plain,(
% 23.96/3.49 a_1309=store(a_1307,i2,e_1308)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f38])).
% 23.96/3.49 fof(f120,plain,(
% 23.96/3.49 a_1311=store(a_1309,i1,e_1310)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f39])).
% 23.96/3.49 fof(f121,plain,(
% 23.96/3.49 a_1313=store(a_1311,i3,e_1312)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f40])).
% 23.96/3.49 fof(f122,plain,(
% 23.96/3.49 a_1315=store(a_1313,i0,e_1314)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f41])).
% 23.96/3.49 fof(f123,plain,(
% 23.96/3.49 a_1317=store(a_1315,i5,e_1316)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f42])).
% 23.96/3.49 fof(f124,plain,(
% 23.96/3.49 a_1319=store(a_1317,i9,e_1318)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f43])).
% 23.96/3.49 fof(f125,plain,(
% 23.96/3.49 e_1244=select(a1,i7)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f44])).
% 23.96/3.49 fof(f126,plain,(
% 23.96/3.49 e_1246=select(a1,i8)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f45])).
% 23.96/3.49 fof(f127,plain,(
% 23.96/3.49 e_1248=select(a_1247,i8)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f46])).
% 23.96/3.49 fof(f128,plain,(
% 23.96/3.49 e_1250=select(a_1247,i6)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f47])).
% 23.96/3.49 fof(f129,plain,(
% 23.96/3.49 e_1252=select(a_1251,i5)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f48])).
% 23.96/3.49 fof(f130,plain,(
% 23.96/3.49 e_1254=select(a_1251,i8)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f49])).
% 23.96/3.49 fof(f131,plain,(
% 23.96/3.49 e_1256=select(a_1255,i9)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f50])).
% 23.96/3.49 fof(f132,plain,(
% 23.96/3.49 e_1258=select(a_1255,i4)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f51])).
% 23.96/3.49 fof(f133,plain,(
% 23.96/3.49 e_1260=select(a_1259,i1)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f52])).
% 23.96/3.49 fof(f134,plain,(
% 23.96/3.49 e_1262=select(a_1259,i7)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f53])).
% 23.96/3.49 fof(f135,plain,(
% 23.96/3.49 e_1264=select(a_1263,i5)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f54])).
% 23.96/3.49 fof(f136,plain,(
% 23.96/3.49 e_1266=select(a_1263,i4)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f55])).
% 23.96/3.49 fof(f137,plain,(
% 23.96/3.49 e_1268=select(a_1267,i0)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f56])).
% 23.96/3.49 fof(f138,plain,(
% 23.96/3.49 e_1271=select(a_1270,i2)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f57])).
% 23.96/3.49 fof(f139,plain,(
% 23.96/3.49 e_1273=select(a_1270,i1)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f58])).
% 23.96/3.49 fof(f140,plain,(
% 23.96/3.49 e_1275=select(a_1274,i0)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f59])).
% 23.96/3.49 fof(f141,plain,(
% 23.96/3.49 e_1277=select(a_1274,i3)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f60])).
% 23.96/3.49 fof(f142,plain,(
% 23.96/3.49 e_1279=select(a_1278,i5)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f61])).
% 23.96/3.49 fof(f143,plain,(
% 23.96/3.49 e_1281=select(a_1278,i9)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f62])).
% 23.96/3.49 fof(f144,plain,(
% 23.96/3.49 e_1285=select(a_1284,i8)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f63])).
% 23.96/3.49 fof(f145,plain,(
% 23.96/3.49 e_1287=select(a_1284,i6)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f64])).
% 23.96/3.49 fof(f146,plain,(
% 23.96/3.49 e_1289=select(a_1288,i8)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f65])).
% 23.96/3.49 fof(f147,plain,(
% 23.96/3.49 e_1291=select(a_1288,i5)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f66])).
% 23.96/3.49 fof(f148,plain,(
% 23.96/3.49 e_1293=select(a_1292,i9)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f67])).
% 23.96/3.49 fof(f149,plain,(
% 23.96/3.49 e_1295=select(a_1292,i4)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f68])).
% 23.96/3.49 fof(f150,plain,(
% 23.96/3.49 e_1297=select(a_1296,i7)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f69])).
% 23.96/3.49 fof(f151,plain,(
% 23.96/3.49 e_1299=select(a_1296,i1)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f70])).
% 23.96/3.49 fof(f152,plain,(
% 23.96/3.49 e_1301=select(a_1300,i5)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f71])).
% 23.96/3.49 fof(f153,plain,(
% 23.96/3.49 e_1303=select(a_1300,i4)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f72])).
% 23.96/3.49 fof(f154,plain,(
% 23.96/3.49 e_1305=select(a_1304,i0)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f73])).
% 23.96/3.49 fof(f155,plain,(
% 23.96/3.49 e_1308=select(a_1307,i1)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f74])).
% 23.96/3.49 fof(f156,plain,(
% 23.96/3.49 e_1310=select(a_1307,i2)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f75])).
% 23.96/3.49 fof(f157,plain,(
% 23.96/3.49 e_1312=select(a_1311,i0)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f76])).
% 23.96/3.49 fof(f158,plain,(
% 23.96/3.49 e_1314=select(a_1311,i3)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f77])).
% 23.96/3.49 fof(f159,plain,(
% 23.96/3.49 e_1316=select(a_1315,i9)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f78])).
% 23.96/3.49 fof(f160,plain,(
% 23.96/3.49 e_1318=select(a_1315,i5)),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f79])).
% 23.96/3.49 fof(f161,plain,(
% 23.96/3.49 ~a_1282=a_1319),
% 23.96/3.49 inference(cnf_transformation,[status(thm)],[f80])).
% 23.96/3.49 fof(f177,plain,(
% 23.96/3.49 ![X0]: (store(store(a1,X0,e_1246),i8,select(a1,X0))=store(store(a1,i8,select(a1,X0)),X0,select(a1,i8)))),
% 23.96/3.49 inference(paramodulation,[status(thm)],[f126,f84])).
% 23.96/3.49 fof(f218,plain,(
% 23.96/3.49 ![X0]: (store(store(a1,X0,e_1246),i8,select(a1,X0))=store(store(a1,i8,select(a1,X0)),X0,e_1246))),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f126,f177])).
% 23.96/3.49 fof(f251,plain,(
% 23.96/3.49 select(a_1251,i8)=e_1250),
% 23.96/3.49 inference(paramodulation,[status(thm)],[f88,f81])).
% 23.96/3.49 fof(f296,plain,(
% 23.96/3.49 ![X0]: (store(store(a_1251,X0,select(a_1251,i8)),i8,select(a_1251,X0))=store(store(a_1251,i8,select(a_1251,X0)),X0,e_1254))),
% 23.96/3.49 inference(paramodulation,[status(thm)],[f130,f84])).
% 23.96/3.49 fof(f300,plain,(
% 23.96/3.49 ![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))),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f130,f296])).
% 23.96/3.49 fof(f404,plain,(
% 23.96/3.49 ![X0]: (store(store(a_1259,X0,select(a_1259,i7)),i7,select(a_1259,X0))=store(store(a_1259,i7,select(a_1259,X0)),X0,e_1262))),
% 23.96/3.49 inference(paramodulation,[status(thm)],[f134,f84])).
% 23.96/3.49 fof(f408,plain,(
% 23.96/3.49 ![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))),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f134,f404])).
% 23.96/3.49 fof(f687,plain,(
% 23.96/3.49 ![X0]: (store(store(a_1270,X0,select(a_1270,i1)),i1,select(a_1270,X0))=store(store(a_1270,i1,select(a_1270,X0)),X0,e_1273))),
% 23.96/3.49 inference(paramodulation,[status(thm)],[f139,f84])).
% 23.96/3.49 fof(f691,plain,(
% 23.96/3.49 ![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))),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f139,f687])).
% 23.96/3.49 fof(f863,plain,(
% 23.96/3.49 ![X0]: (store(store(a_1278,X0,select(a_1278,i5)),i5,select(a_1278,X0))=store(store(a_1278,i5,select(a_1278,X0)),X0,e_1279))),
% 23.96/3.49 inference(paramodulation,[status(thm)],[f142,f84])).
% 23.96/3.49 fof(f867,plain,(
% 23.96/3.49 ![X0]: (store(store(a_1278,X0,e_1279),i5,select(a_1278,X0))=store(store(a_1278,i5,select(a_1278,X0)),X0,e_1279))),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f142,f863])).
% 23.96/3.49 fof(f2721,plain,(
% 23.96/3.49 store(store(a1,i7,e_1246),i8,select(a1,i7))=store(store(a1,i8,e_1244),i7,e_1246)),
% 23.96/3.49 inference(paramodulation,[status(thm)],[f125,f218])).
% 23.96/3.49 fof(f2729,plain,(
% 23.96/3.49 store(a_1283,i8,select(a1,i7))=store(store(a1,i8,e_1244),i7,e_1246)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f105,f2721])).
% 23.96/3.49 fof(f2730,plain,(
% 23.96/3.49 store(a_1283,i8,e_1244)=store(store(a1,i8,e_1244),i7,e_1246)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f125,f2729])).
% 23.96/3.49 fof(f2731,plain,(
% 23.96/3.49 a_1284=store(store(a1,i8,e_1244),i7,e_1246)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f106,f2730])).
% 23.96/3.49 fof(f2732,plain,(
% 23.96/3.49 a_1284=store(a_1245,i7,e_1246)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f85,f2731])).
% 23.96/3.49 fof(f2733,plain,(
% 23.96/3.49 a_1284=a_1247),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f86,f2732])).
% 23.96/3.49 fof(f2935,plain,(
% 23.96/3.49 e_1287=select(a_1247,i6)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f2733,f145])).
% 23.96/3.49 fof(f2936,plain,(
% 23.96/3.49 e_1285=select(a_1247,i8)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f2733,f144])).
% 23.96/3.49 fof(f2937,plain,(
% 23.96/3.49 a_1286=store(a_1247,i6,e_1285)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f2733,f107])).
% 23.96/3.49 fof(f2939,plain,(
% 23.96/3.49 e_1287=e_1250),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f128,f2935])).
% 23.96/3.49 fof(f2940,plain,(
% 23.96/3.49 e_1285=e_1248),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f127,f2936])).
% 23.96/3.49 fof(f2941,plain,(
% 23.96/3.49 a_1288=store(a_1286,i8,e_1250)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f2939,f108])).
% 23.96/3.49 fof(f2942,plain,(
% 23.96/3.49 a_1286=store(a_1247,i6,e_1248)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f2940,f2937])).
% 23.96/3.49 fof(f2943,plain,(
% 23.96/3.49 a_1286=a_1249),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f87,f2942])).
% 23.96/3.49 fof(f2969,plain,(
% 23.96/3.49 a_1288=store(a_1249,i8,e_1250)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f2943,f2941])).
% 23.96/3.49 fof(f2970,plain,(
% 23.96/3.49 e_1291=select(a_1251,i5)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f2973,f147])).
% 23.96/3.49 fof(f2971,plain,(
% 23.96/3.49 e_1289=select(a_1251,i8)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f2973,f146])).
% 23.96/3.49 fof(f2972,plain,(
% 23.96/3.49 a_1290=store(a_1251,i5,e_1289)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f2973,f109])).
% 23.96/3.49 fof(f2973,plain,(
% 23.96/3.49 a_1288=a_1251),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f88,f2969])).
% 23.96/3.49 fof(f2974,plain,(
% 23.96/3.49 e_1291=e_1252),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f129,f2970])).
% 23.96/3.49 fof(f2975,plain,(
% 23.96/3.49 e_1289=e_1254),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f130,f2971])).
% 23.96/3.49 fof(f2976,plain,(
% 23.96/3.49 a_1292=store(a_1290,i8,e_1252)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f2974,f110])).
% 23.96/3.49 fof(f2977,plain,(
% 23.96/3.49 a_1290=store(a_1251,i5,e_1254)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f2975,f2972])).
% 23.96/3.49 fof(f3171,plain,(
% 23.96/3.49 e_1254=e_1250),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f251,f130])).
% 23.96/3.49 fof(f3183,plain,(
% 23.96/3.49 a_1290=store(a_1251,i5,e_1250)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f3171,f2977])).
% 23.96/3.49 fof(f3185,plain,(
% 23.96/3.49 a_1255=store(a_1253,i5,e_1250)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f3171,f90])).
% 23.96/3.49 fof(f6884,plain,(
% 23.96/3.49 ![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))),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f3171,f300])).
% 23.96/3.49 fof(f6885,plain,(
% 23.96/3.49 ![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))),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f3171,f6884])).
% 23.96/3.49 fof(f6887,plain,(
% 23.96/3.49 store(store(a_1251,i5,e_1250),i8,select(a_1251,i5))=store(store(a_1251,i8,e_1252),i5,e_1250)),
% 23.96/3.49 inference(paramodulation,[status(thm)],[f129,f6885])).
% 23.96/3.49 fof(f6899,plain,(
% 23.96/3.49 store(a_1290,i8,select(a_1251,i5))=store(store(a_1251,i8,e_1252),i5,e_1250)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f3183,f6887])).
% 23.96/3.49 fof(f6900,plain,(
% 23.96/3.49 store(a_1290,i8,e_1252)=store(store(a_1251,i8,e_1252),i5,e_1250)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f129,f6899])).
% 23.96/3.49 fof(f6901,plain,(
% 23.96/3.49 a_1292=store(store(a_1251,i8,e_1252),i5,e_1250)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f2976,f6900])).
% 23.96/3.49 fof(f6902,plain,(
% 23.96/3.49 a_1292=store(a_1253,i5,e_1250)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f89,f6901])).
% 23.96/3.49 fof(f6903,plain,(
% 23.96/3.49 a_1292=a_1255),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f3185,f6902])).
% 23.96/3.49 fof(f7424,plain,(
% 23.96/3.49 e_1295=select(a_1255,i4)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f6903,f149])).
% 23.96/3.49 fof(f7425,plain,(
% 23.96/3.49 e_1293=select(a_1255,i9)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f6903,f148])).
% 23.96/3.49 fof(f7426,plain,(
% 23.96/3.49 a_1294=store(a_1255,i4,e_1293)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f6903,f111])).
% 23.96/3.49 fof(f7427,plain,(
% 23.96/3.49 e_1295=e_1258),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f132,f7424])).
% 23.96/3.49 fof(f7428,plain,(
% 23.96/3.49 e_1293=e_1256),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f131,f7425])).
% 23.96/3.49 fof(f7429,plain,(
% 23.96/3.49 a_1296=store(a_1294,i9,e_1258)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f7427,f112])).
% 23.96/3.49 fof(f7470,plain,(
% 23.96/3.49 a_1294=store(a_1255,i4,e_1256)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f7428,f7426])).
% 23.96/3.49 fof(f7471,plain,(
% 23.96/3.49 a_1294=a_1257),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f91,f7470])).
% 23.96/3.49 fof(f7472,plain,(
% 23.96/3.49 a_1296=store(a_1257,i9,e_1258)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f7471,f7429])).
% 23.96/3.49 fof(f7473,plain,(
% 23.96/3.49 e_1299=select(a_1259,i1)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f7476,f151])).
% 23.96/3.49 fof(f7474,plain,(
% 23.96/3.49 e_1297=select(a_1259,i7)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f7476,f150])).
% 23.96/3.49 fof(f7475,plain,(
% 23.96/3.49 a_1298=store(a_1259,i1,e_1297)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f7476,f113])).
% 23.96/3.49 fof(f7476,plain,(
% 23.96/3.49 a_1296=a_1259),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f92,f7472])).
% 23.96/3.49 fof(f7477,plain,(
% 23.96/3.49 e_1299=e_1260),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f133,f7473])).
% 23.96/3.49 fof(f7478,plain,(
% 23.96/3.49 e_1297=e_1262),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f134,f7474])).
% 23.96/3.49 fof(f7479,plain,(
% 23.96/3.49 a_1300=store(a_1298,i7,e_1260)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f7477,f114])).
% 23.96/3.49 fof(f7480,plain,(
% 23.96/3.49 a_1298=store(a_1259,i1,e_1262)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f7478,f7475])).
% 23.96/3.49 fof(f10324,plain,(
% 23.96/3.49 store(store(a_1259,i1,e_1262),i7,select(a_1259,i1))=store(store(a_1259,i7,e_1260),i1,e_1262)),
% 23.96/3.49 inference(paramodulation,[status(thm)],[f133,f408])).
% 23.96/3.49 fof(f10337,plain,(
% 23.96/3.49 store(a_1298,i7,select(a_1259,i1))=store(store(a_1259,i7,e_1260),i1,e_1262)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f7480,f10324])).
% 23.96/3.49 fof(f10338,plain,(
% 23.96/3.49 store(a_1298,i7,e_1260)=store(store(a_1259,i7,e_1260),i1,e_1262)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f133,f10337])).
% 23.96/3.49 fof(f10339,plain,(
% 23.96/3.49 a_1300=store(store(a_1259,i7,e_1260),i1,e_1262)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f7479,f10338])).
% 23.96/3.49 fof(f10340,plain,(
% 23.96/3.49 a_1300=store(a_1261,i1,e_1262)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f93,f10339])).
% 23.96/3.49 fof(f10341,plain,(
% 23.96/3.49 a_1300=a_1263),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f94,f10340])).
% 23.96/3.49 fof(f10952,plain,(
% 23.96/3.49 e_1303=select(a_1263,i4)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f10341,f153])).
% 23.96/3.49 fof(f10953,plain,(
% 23.96/3.49 e_1301=select(a_1263,i5)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f10341,f152])).
% 23.96/3.49 fof(f10954,plain,(
% 23.96/3.49 a_1302=store(a_1263,i4,e_1301)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f10341,f115])).
% 23.96/3.49 fof(f10955,plain,(
% 23.96/3.49 e_1303=e_1266),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f136,f10952])).
% 23.96/3.49 fof(f10956,plain,(
% 23.96/3.49 e_1301=e_1264),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f135,f10953])).
% 23.96/3.49 fof(f10958,plain,(
% 23.96/3.49 a_1304=store(a_1302,i5,e_1266)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f10955,f116])).
% 23.96/3.49 fof(f11000,plain,(
% 23.96/3.49 a_1302=store(a_1263,i4,e_1264)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f10956,f10954])).
% 23.96/3.49 fof(f11001,plain,(
% 23.96/3.49 a_1302=a_1265),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f95,f11000])).
% 23.96/3.49 fof(f11002,plain,(
% 23.96/3.49 a_1304=store(a_1265,i5,e_1266)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f11001,f10958])).
% 23.96/3.49 fof(f11003,plain,(
% 23.96/3.49 e_1305=select(a_1267,i0)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f11005,f154])).
% 23.96/3.49 fof(f11004,plain,(
% 23.96/3.49 a_1306=store(a_1267,i0,e_1305)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f11005,f117])).
% 23.96/3.49 fof(f11005,plain,(
% 23.96/3.49 a_1304=a_1267),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f96,f11002])).
% 23.96/3.49 fof(f11006,plain,(
% 23.96/3.49 e_1305=e_1268),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f137,f11003])).
% 23.96/3.49 fof(f11009,plain,(
% 23.96/3.49 a_1307=store(a_1306,i0,e_1268)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f11006,f118])).
% 23.96/3.49 fof(f11010,plain,(
% 23.96/3.49 a_1306=store(a_1267,i0,e_1268)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f11006,f11004])).
% 23.96/3.49 fof(f11011,plain,(
% 23.96/3.49 a_1306=a_1269),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f97,f11010])).
% 23.96/3.49 fof(f11012,plain,(
% 23.96/3.49 a_1307=store(a_1269,i0,e_1268)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f11011,f11009])).
% 23.96/3.49 fof(f11013,plain,(
% 23.96/3.49 e_1310=select(a_1270,i2)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f11016,f156])).
% 23.96/3.49 fof(f11014,plain,(
% 23.96/3.49 e_1308=select(a_1270,i1)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f11016,f155])).
% 23.96/3.49 fof(f11015,plain,(
% 23.96/3.49 a_1309=store(a_1270,i2,e_1308)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f11016,f119])).
% 23.96/3.49 fof(f11016,plain,(
% 23.96/3.49 a_1307=a_1270),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f98,f11012])).
% 23.96/3.49 fof(f11017,plain,(
% 23.96/3.49 e_1310=e_1271),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f138,f11013])).
% 23.96/3.49 fof(f11018,plain,(
% 23.96/3.49 e_1308=e_1273),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f139,f11014])).
% 23.96/3.49 fof(f11546,plain,(
% 23.96/3.49 a_1311=store(a_1309,i1,e_1271)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f11017,f120])).
% 23.96/3.49 fof(f11562,plain,(
% 23.96/3.49 a_1309=store(a_1270,i2,e_1273)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f11018,f11015])).
% 23.96/3.49 fof(f14539,plain,(
% 23.96/3.49 store(store(a_1270,i2,e_1273),i1,select(a_1270,i2))=store(store(a_1270,i1,e_1271),i2,e_1273)),
% 23.96/3.49 inference(paramodulation,[status(thm)],[f138,f691])).
% 23.96/3.49 fof(f14552,plain,(
% 23.96/3.49 store(a_1309,i1,select(a_1270,i2))=store(store(a_1270,i1,e_1271),i2,e_1273)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f11562,f14539])).
% 23.96/3.49 fof(f14553,plain,(
% 23.96/3.49 store(a_1309,i1,e_1271)=store(store(a_1270,i1,e_1271),i2,e_1273)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f138,f14552])).
% 23.96/3.49 fof(f14554,plain,(
% 23.96/3.49 a_1311=store(store(a_1270,i1,e_1271),i2,e_1273)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f11546,f14553])).
% 23.96/3.49 fof(f14555,plain,(
% 23.96/3.49 a_1311=store(a_1272,i2,e_1273)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f99,f14554])).
% 23.96/3.49 fof(f14556,plain,(
% 23.96/3.49 a_1311=a_1274),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f100,f14555])).
% 23.96/3.49 fof(f15113,plain,(
% 23.96/3.49 e_1314=select(a_1274,i3)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f14556,f158])).
% 23.96/3.49 fof(f15114,plain,(
% 23.96/3.49 e_1312=select(a_1274,i0)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f14556,f157])).
% 23.96/3.49 fof(f15115,plain,(
% 23.96/3.49 a_1313=store(a_1274,i3,e_1312)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f14556,f121])).
% 23.96/3.49 fof(f15116,plain,(
% 23.96/3.49 e_1314=e_1277),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f141,f15113])).
% 23.96/3.49 fof(f15117,plain,(
% 23.96/3.49 e_1312=e_1275),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f140,f15114])).
% 23.96/3.49 fof(f15119,plain,(
% 23.96/3.49 a_1315=store(a_1313,i0,e_1277)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f15116,f122])).
% 23.96/3.49 fof(f15161,plain,(
% 23.96/3.49 a_1313=store(a_1274,i3,e_1275)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f15117,f15115])).
% 23.96/3.49 fof(f15162,plain,(
% 23.96/3.49 a_1313=a_1276),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f101,f15161])).
% 23.96/3.49 fof(f15163,plain,(
% 23.96/3.49 a_1315=store(a_1276,i0,e_1277)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f15162,f15119])).
% 23.96/3.49 fof(f15164,plain,(
% 23.96/3.49 e_1318=select(a_1278,i5)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f15167,f160])).
% 23.96/3.49 fof(f15165,plain,(
% 23.96/3.49 e_1316=select(a_1278,i9)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f15167,f159])).
% 23.96/3.49 fof(f15166,plain,(
% 23.96/3.49 a_1317=store(a_1278,i5,e_1316)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f15167,f123])).
% 23.96/3.49 fof(f15167,plain,(
% 23.96/3.49 a_1315=a_1278),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f102,f15163])).
% 23.96/3.49 fof(f15168,plain,(
% 23.96/3.49 e_1318=e_1279),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f142,f15164])).
% 23.96/3.49 fof(f15169,plain,(
% 23.96/3.49 e_1316=e_1281),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f143,f15165])).
% 23.96/3.49 fof(f15186,plain,(
% 23.96/3.49 a_1319=store(a_1317,i9,e_1279)),
% 23.96/3.49 inference(backward_demodulation,[status(thm)],[f15168,f124])).
% 23.96/3.49 fof(f15212,plain,(
% 23.96/3.49 a_1317=store(a_1278,i5,e_1281)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f15169,f15166])).
% 23.96/3.49 fof(f16882,plain,(
% 23.96/3.49 store(store(a_1278,i9,e_1279),i5,select(a_1278,i9))=store(store(a_1278,i5,e_1281),i9,e_1279)),
% 23.96/3.49 inference(paramodulation,[status(thm)],[f143,f867])).
% 23.96/3.49 fof(f16896,plain,(
% 23.96/3.49 store(a_1280,i5,select(a_1278,i9))=store(store(a_1278,i5,e_1281),i9,e_1279)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f103,f16882])).
% 23.96/3.49 fof(f16897,plain,(
% 23.96/3.49 store(a_1280,i5,e_1281)=store(store(a_1278,i5,e_1281),i9,e_1279)),
% 23.96/3.49 inference(forward_demodulation,[status(thm)],[f143,f16896])).
% 23.96/3.49 fof(f16898,plain,(
% 14.95/3.52 a_1282=store(store(a_1278,i5,e_1281),i9,e_1279)),
% 14.95/3.52 inference(forward_demodulation,[status(thm)],[f104,f16897])).
% 14.95/3.52 fof(f16899,plain,(
% 14.95/3.52 a_1282=store(a_1317,i9,e_1279)),
% 14.95/3.52 inference(forward_demodulation,[status(thm)],[f15212,f16898])).
% 14.95/3.52 fof(f16930,plain,(
% 14.95/3.52 a_1319=a_1282),
% 14.95/3.52 inference(backward_demodulation,[status(thm)],[f16899,f15186])).
% 14.95/3.52 fof(f16941,plain,(
% 14.95/3.52 $false),
% 14.95/3.52 inference(forward_subsumption_resolution,[status(thm)],[f16930,f161])).
% 14.95/3.52 % SZS output end CNFRefutation for theBenchmark.p
% 14.95/3.56 % Elapsed time: 3.194133 seconds
% 14.95/3.56 % CPU time: 24.949512 seconds
% 14.95/3.56 % Total memory used: 401.831 MB
% 14.95/3.56 % Net memory used: 388.493 MB
%------------------------------------------------------------------------------