%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV537-1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:23:16 PM UTC 2026
% Result : Unsatisfiable 18.83s 4.27s
% Output : CNFRefutation 18.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 81
% Syntax : Number of formulae : 482 ( 207 unt; 0 def)
% Number of atoms : 1564 (1563 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 1089 ( 7 ~;1082 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 92 ( 92 usr; 90 con; 0-3 aty)
% Number of variables : 76 ( 0 sgn 76 !; 0 ?; 69 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1) ).
fof(f2,axiom,
! [X2,X3,X0,X1] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2) ).
fof(f3,axiom,
a_1296 = store(a1,i8,e_1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp0) ).
fof(f4,axiom,
a_1298 = store(a_1296,i7,e_1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp1) ).
fof(f5,axiom,
a_1300 = store(a_1298,i6,e_1299),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp2) ).
fof(f6,axiom,
a_1302 = store(a_1300,i8,e_1301),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp3) ).
fof(f7,axiom,
a_1304 = store(a_1302,i8,e_1303),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp4) ).
fof(f8,axiom,
a_1306 = store(a_1304,i5,e_1305),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp5) ).
fof(f9,axiom,
a_1308 = store(a_1306,i4,e_1307),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp6) ).
fof(f10,axiom,
a_1310 = store(a_1308,i9,e_1309),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp7) ).
fof(f11,axiom,
a_1312 = store(a_1310,i7,e_1311),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp8) ).
fof(f12,axiom,
a_1314 = store(a_1312,i1,e_1313),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp9) ).
fof(f13,axiom,
a_1316 = store(a_1314,i4,e_1315),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp10) ).
fof(f14,axiom,
a_1318 = store(a_1316,i5,e_1317),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp11) ).
fof(f15,axiom,
a_1320 = store(a_1318,i0,e_1319),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp12) ).
fof(f16,axiom,
a_1321 = store(a_1320,i0,e_1319),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp13) ).
fof(f17,axiom,
a_1323 = store(a_1321,i1,e_1322),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp14) ).
fof(f18,axiom,
a_1325 = store(a_1323,i2,e_1324),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp15) ).
fof(f19,axiom,
a_1327 = store(a_1325,i3,e_1326),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp16) ).
fof(f20,axiom,
a_1329 = store(a_1327,i0,e_1328),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp17) ).
fof(f21,axiom,
a_1331 = store(a_1329,i9,e_1330),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp18) ).
fof(f22,axiom,
a_1333 = store(a_1331,i5,e_1332),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp19) ).
fof(f23,axiom,
a_1334 = store(a1,i7,e_1297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp20) ).
fof(f24,axiom,
a_1335 = store(a_1334,i8,e_1295),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp21) ).
fof(f25,axiom,
a_1337 = store(a_1335,i6,e_1336),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp22) ).
fof(f26,axiom,
a_1339 = store(a_1337,i8,e_1338),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp23) ).
fof(f27,axiom,
a_1341 = store(a_1339,i5,e_1340),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp24) ).
fof(f28,axiom,
a_1343 = store(a_1341,i8,e_1342),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp25) ).
fof(f29,axiom,
a_1345 = store(a_1343,i4,e_1344),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp26) ).
fof(f30,axiom,
a_1347 = store(a_1345,i9,e_1346),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp27) ).
fof(f31,axiom,
a_1349 = store(a_1347,i1,e_1348),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp28) ).
fof(f32,axiom,
a_1351 = store(a_1349,i7,e_1350),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp29) ).
fof(f33,axiom,
a_1353 = store(a_1351,i4,e_1352),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp30) ).
fof(f34,axiom,
a_1355 = store(a_1353,i5,e_1354),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp31) ).
fof(f35,axiom,
a_1357 = store(a_1355,i0,e_1356),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp32) ).
fof(f36,axiom,
a_1358 = store(a_1357,i0,e_1356),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp33) ).
fof(f37,axiom,
a_1360 = store(a_1358,i2,e_1359),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp34) ).
fof(f38,axiom,
a_1362 = store(a_1360,i1,e_1361),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp35) ).
fof(f39,axiom,
a_1364 = store(a_1362,i3,e_1363),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp36) ).
fof(f40,axiom,
a_1366 = store(a_1364,i0,e_1365),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp37) ).
fof(f41,axiom,
a_1368 = store(a_1366,i5,e_1367),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp38) ).
fof(f42,axiom,
a_1370 = store(a_1368,i9,e_1369),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp39) ).
fof(f43,axiom,
e_1295 = select(a1,i7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp40) ).
fof(f44,axiom,
e_1297 = select(a1,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp41) ).
fof(f45,axiom,
e_1299 = select(a_1298,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp42) ).
fof(f46,axiom,
e_1301 = select(a_1298,i6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp43) ).
fof(f47,axiom,
e_1303 = select(a_1302,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp44) ).
fof(f48,axiom,
e_1305 = select(a_1302,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp45) ).
fof(f49,axiom,
e_1307 = select(a_1306,i9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp46) ).
fof(f50,axiom,
e_1309 = select(a_1306,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp47) ).
fof(f51,axiom,
e_1311 = select(a_1310,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp48) ).
fof(f52,axiom,
e_1313 = select(a_1310,i7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp49) ).
fof(f53,axiom,
e_1315 = select(a_1314,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp50) ).
fof(f54,axiom,
e_1317 = select(a_1314,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp51) ).
fof(f55,axiom,
e_1319 = select(a_1318,i0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp52) ).
fof(f56,axiom,
e_1322 = select(a_1321,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp53) ).
fof(f57,axiom,
e_1324 = select(a_1321,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp54) ).
fof(f58,axiom,
e_1326 = select(a_1325,i0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp55) ).
fof(f59,axiom,
e_1328 = select(a_1325,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp56) ).
fof(f60,axiom,
e_1330 = select(a_1329,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp57) ).
fof(f61,axiom,
e_1332 = select(a_1329,i9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp58) ).
fof(f62,axiom,
e_1336 = select(a_1335,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp59) ).
fof(f63,axiom,
e_1338 = select(a_1335,i6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp60) ).
fof(f64,axiom,
e_1340 = select(a_1339,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp61) ).
fof(f65,axiom,
e_1342 = select(a_1339,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp62) ).
fof(f66,axiom,
e_1344 = select(a_1343,i9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp63) ).
fof(f67,axiom,
e_1346 = select(a_1343,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp64) ).
fof(f68,axiom,
e_1348 = select(a_1347,i7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp65) ).
fof(f69,axiom,
e_1350 = select(a_1347,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp66) ).
fof(f70,axiom,
e_1352 = select(a_1351,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp67) ).
fof(f71,axiom,
e_1354 = select(a_1351,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp68) ).
fof(f72,axiom,
e_1356 = select(a_1355,i0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp69) ).
fof(f73,axiom,
e_1359 = select(a_1358,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp70) ).
fof(f74,axiom,
e_1361 = select(a_1358,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp71) ).
fof(f75,axiom,
e_1363 = select(a_1362,i0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp72) ).
fof(f76,axiom,
e_1365 = select(a_1362,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp73) ).
fof(f77,axiom,
e_1367 = select(a_1366,i9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp74) ).
fof(f78,axiom,
e_1369 = select(a_1366,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp75) ).
fof(f79,axiom,
e_1372 = select(a_1333,i_1371),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp76) ).
fof(f80,axiom,
e_1373 = select(a_1370,i_1371),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp77) ).
fof(f82,negated_conjecture,
e_1372 != e_1373,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
tcf(c_131,plain,
! [X0: $i,X1: $i,X2: $i] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[],[f1]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X1 = X3 )
| ( select(store(X0,X1,X2),X3) = select(X0,X3) ) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_133,plain,
store(a1,i8,e_1295) = a_1296,
inference(cnf_transformation,[],[f3]) ).
tcf(c_134,plain,
store(a_1296,i7,e_1297) = a_1298,
inference(cnf_transformation,[],[f4]) ).
tcf(c_135,plain,
store(a_1298,i6,e_1299) = a_1300,
inference(cnf_transformation,[],[f5]) ).
tcf(c_136,plain,
store(a_1300,i8,e_1301) = a_1302,
inference(cnf_transformation,[],[f6]) ).
tcf(c_137,plain,
store(a_1302,i8,e_1303) = a_1304,
inference(cnf_transformation,[],[f7]) ).
tcf(c_138,plain,
store(a_1304,i5,e_1305) = a_1306,
inference(cnf_transformation,[],[f8]) ).
tcf(c_139,plain,
store(a_1306,i4,e_1307) = a_1308,
inference(cnf_transformation,[],[f9]) ).
tcf(c_140,plain,
store(a_1308,i9,e_1309) = a_1310,
inference(cnf_transformation,[],[f10]) ).
tcf(c_141,plain,
store(a_1310,i7,e_1311) = a_1312,
inference(cnf_transformation,[],[f11]) ).
tcf(c_142,plain,
store(a_1312,i1,e_1313) = a_1314,
inference(cnf_transformation,[],[f12]) ).
tcf(c_143,plain,
store(a_1314,i4,e_1315) = a_1316,
inference(cnf_transformation,[],[f13]) ).
tcf(c_144,plain,
store(a_1316,i5,e_1317) = a_1318,
inference(cnf_transformation,[],[f14]) ).
tcf(c_145,plain,
store(a_1318,i0,e_1319) = a_1320,
inference(cnf_transformation,[],[f15]) ).
tcf(c_146,plain,
store(a_1320,i0,e_1319) = a_1321,
inference(cnf_transformation,[],[f16]) ).
tcf(c_147,plain,
store(a_1321,i1,e_1322) = a_1323,
inference(cnf_transformation,[],[f17]) ).
tcf(c_148,plain,
store(a_1323,i2,e_1324) = a_1325,
inference(cnf_transformation,[],[f18]) ).
tcf(c_149,plain,
store(a_1325,i3,e_1326) = a_1327,
inference(cnf_transformation,[],[f19]) ).
tcf(c_150,plain,
store(a_1327,i0,e_1328) = a_1329,
inference(cnf_transformation,[],[f20]) ).
tcf(c_151,plain,
store(a_1329,i9,e_1330) = a_1331,
inference(cnf_transformation,[],[f21]) ).
tcf(c_152,plain,
store(a_1331,i5,e_1332) = a_1333,
inference(cnf_transformation,[],[f22]) ).
tcf(c_153,plain,
store(a1,i7,e_1297) = a_1334,
inference(cnf_transformation,[],[f23]) ).
tcf(c_154,plain,
store(a_1334,i8,e_1295) = a_1335,
inference(cnf_transformation,[],[f24]) ).
tcf(c_155,plain,
store(a_1335,i6,e_1336) = a_1337,
inference(cnf_transformation,[],[f25]) ).
tcf(c_156,plain,
store(a_1337,i8,e_1338) = a_1339,
inference(cnf_transformation,[],[f26]) ).
tcf(c_157,plain,
store(a_1339,i5,e_1340) = a_1341,
inference(cnf_transformation,[],[f27]) ).
tcf(c_158,plain,
store(a_1341,i8,e_1342) = a_1343,
inference(cnf_transformation,[],[f28]) ).
tcf(c_159,plain,
store(a_1343,i4,e_1344) = a_1345,
inference(cnf_transformation,[],[f29]) ).
tcf(c_160,plain,
store(a_1345,i9,e_1346) = a_1347,
inference(cnf_transformation,[],[f30]) ).
tcf(c_161,plain,
store(a_1347,i1,e_1348) = a_1349,
inference(cnf_transformation,[],[f31]) ).
tcf(c_162,plain,
store(a_1349,i7,e_1350) = a_1351,
inference(cnf_transformation,[],[f32]) ).
tcf(c_163,plain,
store(a_1351,i4,e_1352) = a_1353,
inference(cnf_transformation,[],[f33]) ).
tcf(c_164,plain,
store(a_1353,i5,e_1354) = a_1355,
inference(cnf_transformation,[],[f34]) ).
tcf(c_165,plain,
store(a_1355,i0,e_1356) = a_1357,
inference(cnf_transformation,[],[f35]) ).
tcf(c_166,plain,
store(a_1357,i0,e_1356) = a_1358,
inference(cnf_transformation,[],[f36]) ).
tcf(c_167,plain,
store(a_1358,i2,e_1359) = a_1360,
inference(cnf_transformation,[],[f37]) ).
tcf(c_168,plain,
store(a_1360,i1,e_1361) = a_1362,
inference(cnf_transformation,[],[f38]) ).
tcf(c_169,plain,
store(a_1362,i3,e_1363) = a_1364,
inference(cnf_transformation,[],[f39]) ).
tcf(c_170,plain,
store(a_1364,i0,e_1365) = a_1366,
inference(cnf_transformation,[],[f40]) ).
tcf(c_171,plain,
store(a_1366,i5,e_1367) = a_1368,
inference(cnf_transformation,[],[f41]) ).
tcf(c_172,plain,
store(a_1368,i9,e_1369) = a_1370,
inference(cnf_transformation,[],[f42]) ).
tcf(c_173,plain,
select(a1,i7) = e_1295,
inference(cnf_transformation,[],[f43]) ).
tcf(c_174,plain,
select(a1,i8) = e_1297,
inference(cnf_transformation,[],[f44]) ).
tcf(c_175,plain,
select(a_1298,i8) = e_1299,
inference(cnf_transformation,[],[f45]) ).
tcf(c_176,plain,
select(a_1298,i6) = e_1301,
inference(cnf_transformation,[],[f46]) ).
tcf(c_177,plain,
select(a_1302,i5) = e_1303,
inference(cnf_transformation,[],[f47]) ).
tcf(c_178,plain,
select(a_1302,i8) = e_1305,
inference(cnf_transformation,[],[f48]) ).
tcf(c_179,plain,
select(a_1306,i9) = e_1307,
inference(cnf_transformation,[],[f49]) ).
tcf(c_180,plain,
select(a_1306,i4) = e_1309,
inference(cnf_transformation,[],[f50]) ).
tcf(c_181,plain,
select(a_1310,i1) = e_1311,
inference(cnf_transformation,[],[f51]) ).
tcf(c_182,plain,
select(a_1310,i7) = e_1313,
inference(cnf_transformation,[],[f52]) ).
tcf(c_183,plain,
select(a_1314,i5) = e_1315,
inference(cnf_transformation,[],[f53]) ).
tcf(c_184,plain,
select(a_1314,i4) = e_1317,
inference(cnf_transformation,[],[f54]) ).
tcf(c_185,plain,
select(a_1318,i0) = e_1319,
inference(cnf_transformation,[],[f55]) ).
tcf(c_186,plain,
select(a_1321,i2) = e_1322,
inference(cnf_transformation,[],[f56]) ).
tcf(c_187,plain,
select(a_1321,i1) = e_1324,
inference(cnf_transformation,[],[f57]) ).
tcf(c_188,plain,
select(a_1325,i0) = e_1326,
inference(cnf_transformation,[],[f58]) ).
tcf(c_189,plain,
select(a_1325,i3) = e_1328,
inference(cnf_transformation,[],[f59]) ).
tcf(c_190,plain,
select(a_1329,i5) = e_1330,
inference(cnf_transformation,[],[f60]) ).
tcf(c_191,plain,
select(a_1329,i9) = e_1332,
inference(cnf_transformation,[],[f61]) ).
tcf(c_192,plain,
select(a_1335,i8) = e_1336,
inference(cnf_transformation,[],[f62]) ).
tcf(c_193,plain,
select(a_1335,i6) = e_1338,
inference(cnf_transformation,[],[f63]) ).
tcf(c_194,plain,
select(a_1339,i8) = e_1340,
inference(cnf_transformation,[],[f64]) ).
tcf(c_195,plain,
select(a_1339,i5) = e_1342,
inference(cnf_transformation,[],[f65]) ).
tcf(c_196,plain,
select(a_1343,i9) = e_1344,
inference(cnf_transformation,[],[f66]) ).
tcf(c_197,plain,
select(a_1343,i4) = e_1346,
inference(cnf_transformation,[],[f67]) ).
tcf(c_198,plain,
select(a_1347,i7) = e_1348,
inference(cnf_transformation,[],[f68]) ).
tcf(c_199,plain,
select(a_1347,i1) = e_1350,
inference(cnf_transformation,[],[f69]) ).
tcf(c_200,plain,
select(a_1351,i5) = e_1352,
inference(cnf_transformation,[],[f70]) ).
tcf(c_201,plain,
select(a_1351,i4) = e_1354,
inference(cnf_transformation,[],[f71]) ).
tcf(c_202,plain,
select(a_1355,i0) = e_1356,
inference(cnf_transformation,[],[f72]) ).
tcf(c_203,plain,
select(a_1358,i1) = e_1359,
inference(cnf_transformation,[],[f73]) ).
tcf(c_204,plain,
select(a_1358,i2) = e_1361,
inference(cnf_transformation,[],[f74]) ).
tcf(c_205,plain,
select(a_1362,i0) = e_1363,
inference(cnf_transformation,[],[f75]) ).
tcf(c_206,plain,
select(a_1362,i3) = e_1365,
inference(cnf_transformation,[],[f76]) ).
tcf(c_207,plain,
select(a_1366,i9) = e_1367,
inference(cnf_transformation,[],[f77]) ).
tcf(c_208,plain,
select(a_1366,i5) = e_1369,
inference(cnf_transformation,[],[f78]) ).
tcf(c_209,plain,
select(a_1333,i_1371) = e_1372,
inference(cnf_transformation,[],[f79]) ).
tcf(c_210,plain,
select(a_1370,i_1371) = e_1373,
inference(cnf_transformation,[],[f80]) ).
tcf(c_212,negated_conjecture,
e_1372 != e_1373,
inference(cnf_transformation,[],[f82]) ).
tcf(c_388,negated_conjecture,
e_1372 != e_1373,
inference(demodulation,[status(thm)],[c_212]) ).
tcf(c_592,plain,
select(a_1296,i8) = e_1295,
inference(superposition,[status(thm)],[c_133,c_131]) ).
tcf(c_593,plain,
select(a_1298,i7) = e_1297,
inference(superposition,[status(thm)],[c_134,c_131]) ).
tcf(c_594,plain,
select(a_1300,i6) = e_1299,
inference(superposition,[status(thm)],[c_135,c_131]) ).
tcf(c_595,plain,
select(a_1302,i8) = e_1301,
inference(superposition,[status(thm)],[c_136,c_131]) ).
tcf(c_596,plain,
e_1301 = e_1305,
inference(demodulation,[status(thm)],[c_178,c_595]) ).
tcf(c_597,plain,
select(a_1304,i8) = e_1303,
inference(superposition,[status(thm)],[c_137,c_131]) ).
tcf(c_598,plain,
store(a_1304,i5,e_1301) = a_1306,
inference(light_normalisation,[status(thm)],[c_138,c_596]) ).
tcf(c_599,plain,
select(a_1306,i5) = e_1301,
inference(superposition,[status(thm)],[c_598,c_131]) ).
tcf(c_600,plain,
select(a_1308,i4) = e_1307,
inference(superposition,[status(thm)],[c_139,c_131]) ).
tcf(c_601,plain,
select(a_1310,i9) = e_1309,
inference(superposition,[status(thm)],[c_140,c_131]) ).
tcf(c_602,plain,
select(a_1312,i7) = e_1311,
inference(superposition,[status(thm)],[c_141,c_131]) ).
tcf(c_603,plain,
select(a_1314,i1) = e_1313,
inference(superposition,[status(thm)],[c_142,c_131]) ).
tcf(c_604,plain,
select(a_1316,i4) = e_1315,
inference(superposition,[status(thm)],[c_143,c_131]) ).
tcf(c_605,plain,
select(a_1318,i5) = e_1317,
inference(superposition,[status(thm)],[c_144,c_131]) ).
tcf(c_607,plain,
select(a_1321,i0) = e_1319,
inference(superposition,[status(thm)],[c_146,c_131]) ).
tcf(c_608,plain,
select(a_1323,i1) = e_1322,
inference(superposition,[status(thm)],[c_147,c_131]) ).
tcf(c_609,plain,
select(a_1325,i2) = e_1324,
inference(superposition,[status(thm)],[c_148,c_131]) ).
tcf(c_610,plain,
select(a_1327,i3) = e_1326,
inference(superposition,[status(thm)],[c_149,c_131]) ).
tcf(c_614,plain,
! [X0: $i] :
( ( X0 = i8 )
| ( select(a_1296,X0) = select(a1,X0) ) ),
inference(superposition,[status(thm)],[c_133,c_132]) ).
tcf(c_615,plain,
! [X0: $i] :
( ( X0 = i7 )
| ( select(a_1296,X0) = select(a_1298,X0) ) ),
inference(superposition,[status(thm)],[c_134,c_132]) ).
tcf(c_616,plain,
! [X0: $i] :
( ( X0 = i6 )
| ( select(a_1298,X0) = select(a_1300,X0) ) ),
inference(superposition,[status(thm)],[c_135,c_132]) ).
tcf(c_617,plain,
! [X0: $i] :
( ( X0 = i8 )
| ( select(a_1300,X0) = select(a_1302,X0) ) ),
inference(superposition,[status(thm)],[c_136,c_132]) ).
tcf(c_618,plain,
! [X0: $i] :
( ( X0 = i8 )
| ( select(a_1302,X0) = select(a_1304,X0) ) ),
inference(superposition,[status(thm)],[c_137,c_132]) ).
tcf(c_619,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( select(a_1306,X0) = select(a_1308,X0) ) ),
inference(superposition,[status(thm)],[c_139,c_132]) ).
tcf(c_620,plain,
! [X0: $i] :
( ( X0 = i9 )
| ( select(a_1308,X0) = select(a_1310,X0) ) ),
inference(superposition,[status(thm)],[c_140,c_132]) ).
tcf(c_621,plain,
! [X0: $i] :
( ( X0 = i7 )
| ( select(a_1310,X0) = select(a_1312,X0) ) ),
inference(superposition,[status(thm)],[c_141,c_132]) ).
tcf(c_622,plain,
! [X0: $i] :
( ( X0 = i1 )
| ( select(a_1312,X0) = select(a_1314,X0) ) ),
inference(superposition,[status(thm)],[c_142,c_132]) ).
tcf(c_623,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( select(a_1314,X0) = select(a_1316,X0) ) ),
inference(superposition,[status(thm)],[c_143,c_132]) ).
tcf(c_624,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( select(a_1316,X0) = select(a_1318,X0) ) ),
inference(superposition,[status(thm)],[c_144,c_132]) ).
tcf(c_625,plain,
! [X0: $i] :
( ( X0 = i0 )
| ( select(a_1318,X0) = select(a_1320,X0) ) ),
inference(superposition,[status(thm)],[c_145,c_132]) ).
tcf(c_626,plain,
! [X0: $i] :
( ( X0 = i0 )
| ( select(a_1320,X0) = select(a_1321,X0) ) ),
inference(superposition,[status(thm)],[c_146,c_132]) ).
tcf(c_627,plain,
! [X0: $i] :
( ( X0 = i1 )
| ( select(a_1321,X0) = select(a_1323,X0) ) ),
inference(superposition,[status(thm)],[c_147,c_132]) ).
tcf(c_628,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( select(a_1323,X0) = select(a_1325,X0) ) ),
inference(superposition,[status(thm)],[c_148,c_132]) ).
tcf(c_629,plain,
! [X0: $i] :
( ( X0 = i3 )
| ( select(a_1325,X0) = select(a_1327,X0) ) ),
inference(superposition,[status(thm)],[c_149,c_132]) ).
tcf(c_630,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( select(a_1304,X0) = select(a_1306,X0) ) ),
inference(superposition,[status(thm)],[c_598,c_132]) ).
tcf(c_681,plain,
! [X0: $i] :
( ( X0 = i0 )
| ( select(a_1327,X0) = select(a_1329,X0) ) ),
inference(superposition,[status(thm)],[c_150,c_132]) ).
tcf(c_682,plain,
select(a_1329,i0) = e_1328,
inference(superposition,[status(thm)],[c_150,c_131]) ).
tcf(c_686,plain,
! [X0: $i] :
( ( X0 = i9 )
| ( select(a_1329,X0) = select(a_1331,X0) ) ),
inference(superposition,[status(thm)],[c_151,c_132]) ).
tcf(c_687,plain,
select(a_1331,i9) = e_1330,
inference(superposition,[status(thm)],[c_151,c_131]) ).
tcf(c_691,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( select(a_1331,X0) = select(a_1333,X0) ) ),
inference(superposition,[status(thm)],[c_152,c_132]) ).
tcf(c_692,plain,
select(a_1333,i5) = e_1332,
inference(superposition,[status(thm)],[c_152,c_131]) ).
tcf(c_695,plain,
! [X0: $i] :
( ( X0 = i7 )
| ( select(a1,X0) = select(a_1334,X0) ) ),
inference(superposition,[status(thm)],[c_153,c_132]) ).
tcf(c_696,plain,
select(a_1334,i7) = e_1297,
inference(superposition,[status(thm)],[c_153,c_131]) ).
tcf(c_700,plain,
! [X0: $i] :
( ( X0 = i8 )
| ( select(a_1334,X0) = select(a_1335,X0) ) ),
inference(superposition,[status(thm)],[c_154,c_132]) ).
tcf(c_701,plain,
select(a_1335,i8) = e_1295,
inference(superposition,[status(thm)],[c_154,c_131]) ).
tcf(c_704,plain,
e_1295 = e_1336,
inference(demodulation,[status(thm)],[c_192,c_701]) ).
tcf(c_706,plain,
store(a_1335,i6,e_1295) = a_1337,
inference(light_normalisation,[status(thm)],[c_155,c_704]) ).
tcf(c_707,plain,
! [X0: $i] :
( ( X0 = i6 )
| ( select(a_1335,X0) = select(a_1337,X0) ) ),
inference(superposition,[status(thm)],[c_706,c_132]) ).
tcf(c_708,plain,
select(a_1337,i6) = e_1295,
inference(superposition,[status(thm)],[c_706,c_131]) ).
tcf(c_712,plain,
! [X0: $i] :
( ( X0 = i8 )
| ( select(a_1337,X0) = select(a_1339,X0) ) ),
inference(superposition,[status(thm)],[c_156,c_132]) ).
tcf(c_713,plain,
select(a_1339,i8) = e_1338,
inference(superposition,[status(thm)],[c_156,c_131]) ).
tcf(c_716,plain,
e_1338 = e_1340,
inference(demodulation,[status(thm)],[c_194,c_713]) ).
tcf(c_724,plain,
store(a_1339,i5,e_1338) = a_1341,
inference(light_normalisation,[status(thm)],[c_157,c_716]) ).
tcf(c_725,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( select(a_1339,X0) = select(a_1341,X0) ) ),
inference(superposition,[status(thm)],[c_724,c_132]) ).
tcf(c_726,plain,
select(a_1341,i5) = e_1338,
inference(superposition,[status(thm)],[c_724,c_131]) ).
tcf(c_729,plain,
! [X0: $i] :
( ( X0 = i8 )
| ( select(a_1341,X0) = select(a_1343,X0) ) ),
inference(superposition,[status(thm)],[c_158,c_132]) ).
tcf(c_730,plain,
select(a_1343,i8) = e_1342,
inference(superposition,[status(thm)],[c_158,c_131]) ).
tcf(c_734,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( select(a_1343,X0) = select(a_1345,X0) ) ),
inference(superposition,[status(thm)],[c_159,c_132]) ).
tcf(c_735,plain,
select(a_1345,i4) = e_1344,
inference(superposition,[status(thm)],[c_159,c_131]) ).
tcf(c_739,plain,
! [X0: $i] :
( ( X0 = i9 )
| ( select(a_1345,X0) = select(a_1347,X0) ) ),
inference(superposition,[status(thm)],[c_160,c_132]) ).
tcf(c_740,plain,
select(a_1347,i9) = e_1346,
inference(superposition,[status(thm)],[c_160,c_131]) ).
tcf(c_744,plain,
! [X0: $i] :
( ( X0 = i1 )
| ( select(a_1347,X0) = select(a_1349,X0) ) ),
inference(superposition,[status(thm)],[c_161,c_132]) ).
tcf(c_745,plain,
select(a_1349,i1) = e_1348,
inference(superposition,[status(thm)],[c_161,c_131]) ).
tcf(c_749,plain,
! [X0: $i] :
( ( X0 = i7 )
| ( select(a_1349,X0) = select(a_1351,X0) ) ),
inference(superposition,[status(thm)],[c_162,c_132]) ).
tcf(c_750,plain,
select(a_1351,i7) = e_1350,
inference(superposition,[status(thm)],[c_162,c_131]) ).
tcf(c_754,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( select(a_1351,X0) = select(a_1353,X0) ) ),
inference(superposition,[status(thm)],[c_163,c_132]) ).
tcf(c_755,plain,
select(a_1353,i4) = e_1352,
inference(superposition,[status(thm)],[c_163,c_131]) ).
tcf(c_759,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( select(a_1353,X0) = select(a_1355,X0) ) ),
inference(superposition,[status(thm)],[c_164,c_132]) ).
tcf(c_760,plain,
select(a_1355,i5) = e_1354,
inference(superposition,[status(thm)],[c_164,c_131]) ).
tcf(c_769,plain,
( ( i8 = i7 )
| ( select(a_1298,i8) = e_1295 ) ),
inference(superposition,[status(thm)],[c_615,c_592]) ).
tcf(c_770,plain,
! [X0: $i] :
( ( X0 = i7 )
| ( X0 = i8 )
| ( select(a1,X0) = select(a_1298,X0) ) ),
inference(superposition,[status(thm)],[c_615,c_614]) ).
tcf(c_771,plain,
( ( e_1295 = e_1299 )
| ( i8 = i7 ) ),
inference(light_normalisation,[status(thm)],[c_769,c_175]) ).
tcf(c_778,plain,
! [X0: $i] :
( ( X0 = i0 )
| ( select(a_1355,X0) = select(a_1357,X0) ) ),
inference(superposition,[status(thm)],[c_165,c_132]) ).
tcf(c_779,plain,
select(a_1357,i0) = e_1356,
inference(superposition,[status(thm)],[c_165,c_131]) ).
tcf(c_783,plain,
! [X0: $i] :
( ( X0 = i0 )
| ( select(a_1357,X0) = select(a_1358,X0) ) ),
inference(superposition,[status(thm)],[c_166,c_132]) ).
tcf(c_784,plain,
select(a_1358,i0) = e_1356,
inference(superposition,[status(thm)],[c_166,c_131]) ).
tcf(c_790,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( select(a_1358,X0) = select(a_1360,X0) ) ),
inference(superposition,[status(thm)],[c_167,c_132]) ).
tcf(c_791,plain,
select(a_1360,i2) = e_1359,
inference(superposition,[status(thm)],[c_167,c_131]) ).
tcf(c_797,plain,
! [X0: $i] :
( ( X0 = i1 )
| ( select(a_1360,X0) = select(a_1362,X0) ) ),
inference(superposition,[status(thm)],[c_168,c_132]) ).
tcf(c_798,plain,
select(a_1362,i1) = e_1361,
inference(superposition,[status(thm)],[c_168,c_131]) ).
tcf(c_807,plain,
! [X0: $i] :
( ( X0 = i3 )
| ( select(a_1362,X0) = select(a_1364,X0) ) ),
inference(superposition,[status(thm)],[c_169,c_132]) ).
tcf(c_808,plain,
select(a_1364,i3) = e_1363,
inference(superposition,[status(thm)],[c_169,c_131]) ).
tcf(c_812,plain,
! [X0: $i] :
( ( X0 = i0 )
| ( select(a_1364,X0) = select(a_1366,X0) ) ),
inference(superposition,[status(thm)],[c_170,c_132]) ).
tcf(c_813,plain,
select(a_1366,i0) = e_1365,
inference(superposition,[status(thm)],[c_170,c_131]) ).
tcf(c_817,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( select(a_1366,X0) = select(a_1368,X0) ) ),
inference(superposition,[status(thm)],[c_171,c_132]) ).
tcf(c_818,plain,
select(a_1368,i5) = e_1367,
inference(superposition,[status(thm)],[c_171,c_131]) ).
tcf(c_825,plain,
! [X0: $i] :
( ( X0 = i9 )
| ( select(a_1368,X0) = select(a_1370,X0) ) ),
inference(superposition,[status(thm)],[c_172,c_132]) ).
tcf(c_826,plain,
select(a_1370,i9) = e_1369,
inference(superposition,[status(thm)],[c_172,c_131]) ).
tcf(c_846,plain,
( ( i8 = i6 )
| ( select(a_1302,i6) = e_1299 ) ),
inference(superposition,[status(thm)],[c_617,c_594]) ).
tcf(c_847,plain,
! [X0: $i] :
( ( X0 = i6 )
| ( X0 = i8 )
| ( select(a_1298,X0) = select(a_1302,X0) ) ),
inference(superposition,[status(thm)],[c_617,c_616]) ).
tcf(c_874,plain,
( ( i4 = i9 )
| ( select(a_1310,i4) = e_1307 ) ),
inference(superposition,[status(thm)],[c_620,c_600]) ).
tcf(c_875,plain,
! [X0: $i] :
( ( X0 = i9 )
| ( X0 = i4 )
| ( select(a_1306,X0) = select(a_1310,X0) ) ),
inference(superposition,[status(thm)],[c_620,c_619]) ).
tcf(c_891,plain,
( ( i8 = i7 )
| ( store(a_1298,i6,e_1295) = a_1300 ) ),
inference(superposition,[status(thm)],[c_771,c_135]) ).
tcf(c_910,plain,
( ( i8 = i7 )
| ( select(a_1300,i6) = e_1295 ) ),
inference(superposition,[status(thm)],[c_891,c_131]) ).
tcf(c_924,plain,
( ( i7 = i1 )
| ( select(a_1314,i7) = e_1311 ) ),
inference(superposition,[status(thm)],[c_622,c_602]) ).
tcf(c_925,plain,
! [X0: $i] :
( ( X0 = i1 )
| ( X0 = i7 )
| ( select(a_1310,X0) = select(a_1314,X0) ) ),
inference(superposition,[status(thm)],[c_622,c_621]) ).
tcf(c_963,plain,
( ( i5 = i4 )
| ( select(a_1318,i4) = e_1315 ) ),
inference(superposition,[status(thm)],[c_624,c_604]) ).
tcf(c_964,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( X0 = i5 )
| ( select(a_1314,X0) = select(a_1318,X0) ) ),
inference(superposition,[status(thm)],[c_624,c_623]) ).
tcf(c_1003,plain,
! [X0: $i] :
( ( X0 = i0 )
| ( select(a_1318,X0) = select(a_1321,X0) ) ),
inference(superposition,[status(thm)],[c_626,c_625]) ).
tcf(c_1019,plain,
( ( i1 = i2 )
| ( select(a_1325,i1) = e_1322 ) ),
inference(superposition,[status(thm)],[c_628,c_608]) ).
tcf(c_1020,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( X0 = i1 )
| ( select(a_1321,X0) = select(a_1325,X0) ) ),
inference(superposition,[status(thm)],[c_628,c_627]) ).
tcf(c_1039,plain,
( ( i8 = i5 )
| ( select(a_1306,i8) = e_1303 ) ),
inference(superposition,[status(thm)],[c_630,c_597]) ).
tcf(c_1040,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( X0 = i8 )
| ( select(a_1302,X0) = select(a_1306,X0) ) ),
inference(superposition,[status(thm)],[c_630,c_618]) ).
tcf(c_1052,plain,
( ( i0 = i3 )
| ( select(a_1329,i3) = e_1326 ) ),
inference(superposition,[status(thm)],[c_681,c_610]) ).
tcf(c_1053,plain,
! [X0: $i] :
( ( X0 = i3 )
| ( X0 = i0 )
| ( select(a_1325,X0) = select(a_1329,X0) ) ),
inference(superposition,[status(thm)],[c_681,c_629]) ).
tcf(c_1095,plain,
! [X0: $i] :
( ( X0 = i9 )
| ( X0 = i5 )
| ( select(a_1329,X0) = select(a_1333,X0) ) ),
inference(superposition,[status(thm)],[c_691,c_686]) ).
tcf(c_1096,plain,
( ( i5 = i9 )
| ( select(a_1333,i9) = e_1330 ) ),
inference(superposition,[status(thm)],[c_691,c_687]) ).
tcf(c_1118,plain,
! [X0: $i] :
( ( X0 = i7 )
| ( X0 = i8 )
| ( select(a1,X0) = select(a_1335,X0) ) ),
inference(superposition,[status(thm)],[c_700,c_695]) ).
tcf(c_1119,plain,
( ( i8 = i7 )
| ( select(a_1335,i7) = e_1297 ) ),
inference(superposition,[status(thm)],[c_700,c_696]) ).
tcf(c_1150,plain,
! [X0: $i] :
( ( X0 = i6 )
| ( X0 = i8 )
| ( select(a_1335,X0) = select(a_1339,X0) ) ),
inference(superposition,[status(thm)],[c_712,c_707]) ).
tcf(c_1151,plain,
( ( i8 = i6 )
| ( select(a_1339,i6) = e_1295 ) ),
inference(superposition,[status(thm)],[c_712,c_708]) ).
tcf(c_1174,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( X0 = i8 )
| ( select(a_1339,X0) = select(a_1343,X0) ) ),
inference(superposition,[status(thm)],[c_729,c_725]) ).
tcf(c_1175,plain,
( ( i8 = i5 )
| ( select(a_1343,i5) = e_1338 ) ),
inference(superposition,[status(thm)],[c_729,c_726]) ).
tcf(c_1193,plain,
! [X0: $i] :
( ( X0 = i9 )
| ( X0 = i4 )
| ( select(a_1343,X0) = select(a_1347,X0) ) ),
inference(superposition,[status(thm)],[c_739,c_734]) ).
tcf(c_1194,plain,
( ( i4 = i9 )
| ( select(a_1347,i4) = e_1344 ) ),
inference(superposition,[status(thm)],[c_739,c_735]) ).
tcf(c_1227,plain,
! [X0: $i] :
( ( X0 = i1 )
| ( X0 = i7 )
| ( select(a_1347,X0) = select(a_1351,X0) ) ),
inference(superposition,[status(thm)],[c_749,c_744]) ).
tcf(c_1228,plain,
( ( i7 = i1 )
| ( select(a_1351,i1) = e_1348 ) ),
inference(superposition,[status(thm)],[c_749,c_745]) ).
tcf(c_1264,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( X0 = i5 )
| ( select(a_1351,X0) = select(a_1355,X0) ) ),
inference(superposition,[status(thm)],[c_759,c_754]) ).
tcf(c_1265,plain,
( ( i5 = i4 )
| ( select(a_1355,i4) = e_1352 ) ),
inference(superposition,[status(thm)],[c_759,c_755]) ).
tcf(c_1287,plain,
! [X0: $i] :
( ( X0 = i0 )
| ( select(a_1355,X0) = select(a_1358,X0) ) ),
inference(superposition,[status(thm)],[c_783,c_778]) ).
tcf(c_1304,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( X0 = i1 )
| ( select(a_1358,X0) = select(a_1362,X0) ) ),
inference(superposition,[status(thm)],[c_797,c_790]) ).
tcf(c_1305,plain,
( ( i1 = i2 )
| ( select(a_1362,i2) = e_1359 ) ),
inference(superposition,[status(thm)],[c_797,c_791]) ).
tcf(c_1328,plain,
( ( i7 = i6 )
| ( i8 = i6 )
| ( select(a1,i6) = e_1301 ) ),
inference(superposition,[status(thm)],[c_770,c_176]) ).
tcf(c_1351,plain,
! [X0: $i] :
( ( X0 = i3 )
| ( X0 = i0 )
| ( select(a_1362,X0) = select(a_1366,X0) ) ),
inference(superposition,[status(thm)],[c_812,c_807]) ).
tcf(c_1352,plain,
( ( i0 = i3 )
| ( select(a_1366,i3) = e_1363 ) ),
inference(superposition,[status(thm)],[c_812,c_808]) ).
tcf(c_1396,plain,
! [X0: $i] :
( ( X0 = i9 )
| ( X0 = i5 )
| ( select(a_1366,X0) = select(a_1370,X0) ) ),
inference(superposition,[status(thm)],[c_825,c_817]) ).
tcf(c_1397,plain,
( ( i5 = i9 )
| ( select(a_1370,i5) = e_1367 ) ),
inference(superposition,[status(thm)],[c_825,c_818]) ).
tcf(c_1430,plain,
( ( i5 = i0 )
| ( select(a_1321,i5) = e_1317 ) ),
inference(superposition,[status(thm)],[c_1003,c_605]) ).
tcf(c_1431,plain,
( ( i4 = i0 )
| ( i5 = i4 )
| ( select(a_1321,i4) = e_1315 ) ),
inference(superposition,[status(thm)],[c_1003,c_963]) ).
tcf(c_1457,plain,
( ( i5 = i0 )
| ( select(a_1358,i5) = e_1354 ) ),
inference(superposition,[status(thm)],[c_1287,c_760]) ).
tcf(c_1458,plain,
( ( i4 = i0 )
| ( i5 = i4 )
| ( select(a_1358,i4) = e_1352 ) ),
inference(superposition,[status(thm)],[c_1287,c_1265]) ).
tcf(c_1495,plain,
( ( i6 = i5 )
| ( i8 = i5 )
| ( select(a_1298,i5) = e_1303 ) ),
inference(superposition,[status(thm)],[c_847,c_177]) ).
tcf(c_1507,plain,
( ( i6 = i5 )
| ( i7 = i5 )
| ( i8 = i5 )
| ( select(a1,i5) = e_1303 ) ),
inference(superposition,[status(thm)],[c_770,c_1495]) ).
tcf(c_1523,plain,
( ( i9 = i1 )
| ( i4 = i1 )
| ( select(a_1306,i1) = e_1311 ) ),
inference(superposition,[status(thm)],[c_875,c_181]) ).
tcf(c_1524,plain,
( ( i7 = i9 )
| ( i7 = i4 )
| ( select(a_1306,i7) = e_1313 ) ),
inference(superposition,[status(thm)],[c_875,c_182]) ).
tcf(c_1582,plain,
( ( i5 = i1 )
| ( i7 = i5 )
| ( select(a_1310,i5) = e_1315 ) ),
inference(superposition,[status(thm)],[c_925,c_183]) ).
tcf(c_1583,plain,
( ( i4 = i1 )
| ( i7 = i4 )
| ( select(a_1310,i4) = e_1317 ) ),
inference(superposition,[status(thm)],[c_925,c_184]) ).
tcf(c_1610,plain,
( ( i5 = i1 )
| ( i5 = i9 )
| ( i5 = i4 )
| ( i7 = i5 )
| ( select(a_1306,i5) = e_1315 ) ),
inference(superposition,[status(thm)],[c_875,c_1582]) ).
tcf(c_1612,plain,
( ( i5 = i1 )
| ( i5 = i9 )
| ( i5 = i4 )
| ( e_1301 = e_1315 )
| ( i7 = i5 ) ),
inference(light_normalisation,[status(thm)],[c_1610,c_599]) ).
tcf(c_1627,plain,
( ( e_1307 = e_1317 )
| ( i4 = i1 )
| ( i4 = i9 )
| ( i7 = i4 ) ),
inference(superposition,[status(thm)],[c_1583,c_874]) ).
tcf(c_1642,plain,
( ( i4 = i0 )
| ( i5 = i0 )
| ( select(a_1314,i0) = e_1319 ) ),
inference(superposition,[status(thm)],[c_964,c_185]) ).
tcf(c_1644,plain,
! [X0: $i] :
( ( X0 = i0 )
| ( X0 = i4 )
| ( X0 = i5 )
| ( select(a_1314,X0) = select(a_1321,X0) ) ),
inference(superposition,[status(thm)],[c_964,c_1003]) ).
tcf(c_1659,plain,
( ( i1 = i0 )
| ( i4 = i0 )
| ( i5 = i0 )
| ( i7 = i0 )
| ( select(a_1310,i0) = e_1319 ) ),
inference(superposition,[status(thm)],[c_925,c_1642]) ).
tcf(c_1676,plain,
( ( i0 = i2 )
| ( i1 = i0 )
| ( select(a_1321,i0) = e_1326 ) ),
inference(superposition,[status(thm)],[c_1020,c_188]) ).
tcf(c_1677,plain,
( ( i2 = i3 )
| ( i1 = i3 )
| ( select(a_1321,i3) = e_1328 ) ),
inference(superposition,[status(thm)],[c_1020,c_189]) ).
tcf(c_1683,plain,
( ( e_1319 = e_1326 )
| ( i0 = i2 )
| ( i1 = i0 ) ),
inference(light_normalisation,[status(thm)],[c_1676,c_607]) ).
tcf(c_1699,plain,
( ( i0 = i2 )
| ( i1 = i0 )
| ( store(a_1325,i3,e_1319) = a_1327 ) ),
inference(superposition,[status(thm)],[c_1683,c_149]) ).
tcf(c_1716,plain,
( ( i0 = i2 )
| ( i1 = i0 )
| ( select(a_1327,i3) = e_1319 ) ),
inference(superposition,[status(thm)],[c_1699,c_131]) ).
tcf(c_1730,plain,
( ( i5 = i9 )
| ( i8 = i9 )
| ( select(a_1302,i9) = e_1307 ) ),
inference(superposition,[status(thm)],[c_1040,c_179]) ).
tcf(c_1731,plain,
( ( i5 = i4 )
| ( i8 = i4 )
| ( select(a_1302,i4) = e_1309 ) ),
inference(superposition,[status(thm)],[c_1040,c_180]) ).
tcf(c_1734,plain,
( ( i9 = i1 )
| ( i4 = i1 )
| ( i5 = i1 )
| ( i8 = i1 )
| ( select(a_1302,i1) = e_1311 ) ),
inference(superposition,[status(thm)],[c_1040,c_1523]) ).
tcf(c_1735,plain,
( ( i7 = i9 )
| ( i7 = i4 )
| ( i7 = i5 )
| ( i8 = i7 )
| ( select(a_1302,i7) = e_1313 ) ),
inference(superposition,[status(thm)],[c_1040,c_1524]) ).
tcf(c_1771,plain,
( ( i5 = i9 )
| ( i6 = i9 )
| ( i8 = i9 )
| ( select(a_1298,i9) = e_1307 ) ),
inference(superposition,[status(thm)],[c_847,c_1730]) ).
tcf(c_1789,plain,
( ( i5 = i4 )
| ( i6 = i4 )
| ( i8 = i4 )
| ( select(a_1298,i4) = e_1309 ) ),
inference(superposition,[status(thm)],[c_847,c_1731]) ).
tcf(c_1811,plain,
( ( i5 = i3 )
| ( i5 = i0 )
| ( select(a_1325,i5) = e_1330 ) ),
inference(superposition,[status(thm)],[c_1053,c_190]) ).
tcf(c_1812,plain,
( ( i9 = i3 )
| ( i9 = i0 )
| ( select(a_1325,i9) = e_1332 ) ),
inference(superposition,[status(thm)],[c_1053,c_191]) ).
tcf(c_1847,plain,
( ( i5 = i3 )
| ( i5 = i2 )
| ( i5 = i0 )
| ( i5 = i1 )
| ( select(a_1321,i5) = e_1330 ) ),
inference(superposition,[status(thm)],[c_1020,c_1811]) ).
tcf(c_1860,plain,
( ( i9 = i3 )
| ( i9 = i2 )
| ( i9 = i0 )
| ( i9 = i1 )
| ( select(a_1321,i9) = e_1332 ) ),
inference(superposition,[status(thm)],[c_1020,c_1812]) ).
tcf(c_1876,plain,
( ( i9 = i_1371 )
| ( i5 = i_1371 )
| ( select(a_1329,i_1371) = e_1372 ) ),
inference(superposition,[status(thm)],[c_1095,c_209]) ).
tcf(c_1888,plain,
( ( i3 = i_1371 )
| ( i0 = i_1371 )
| ( i9 = i_1371 )
| ( i5 = i_1371 )
| ( select(a_1325,i_1371) = e_1372 ) ),
inference(superposition,[status(thm)],[c_1053,c_1876]) ).
tcf(c_1905,plain,
( ( i7 = i6 )
| ( i8 = i6 )
| ( select(a1,i6) = e_1338 ) ),
inference(superposition,[status(thm)],[c_1118,c_193]) ).
tcf(c_1916,plain,
( ( e_1301 = e_1338 )
| ( i7 = i6 )
| ( i8 = i6 ) ),
inference(superposition,[status(thm)],[c_1328,c_1905]) ).
tcf(c_1928,plain,
( ( i7 = i6 )
| ( i8 = i6 )
| ( store(a_1337,i8,e_1301) = a_1339 ) ),
inference(superposition,[status(thm)],[c_1916,c_156]) ).
tcf(c_1959,plain,
( ( i7 = i6 )
| ( i8 = i6 )
| ( select(a_1339,i8) = e_1301 ) ),
inference(superposition,[status(thm)],[c_1928,c_131]) ).
tcf(c_1971,plain,
( ( i6 = i5 )
| ( i8 = i5 )
| ( select(a_1335,i5) = e_1342 ) ),
inference(superposition,[status(thm)],[c_1150,c_195]) ).
tcf(c_1982,plain,
( ( i6 = i5 )
| ( i7 = i5 )
| ( i8 = i5 )
| ( select(a1,i5) = e_1342 ) ),
inference(superposition,[status(thm)],[c_1118,c_1971]) ).
tcf(c_1998,plain,
( ( i5 = i9 )
| ( i8 = i9 )
| ( select(a_1339,i9) = e_1344 ) ),
inference(superposition,[status(thm)],[c_1174,c_196]) ).
tcf(c_1999,plain,
( ( i5 = i4 )
| ( i8 = i4 )
| ( select(a_1339,i4) = e_1346 ) ),
inference(superposition,[status(thm)],[c_1174,c_197]) ).
tcf(c_2041,plain,
( ( i5 = i9 )
| ( i6 = i9 )
| ( i8 = i9 )
| ( select(a_1335,i9) = e_1344 ) ),
inference(superposition,[status(thm)],[c_1150,c_1998]) ).
tcf(c_2053,plain,
( ( i5 = i4 )
| ( i6 = i4 )
| ( i8 = i4 )
| ( select(a_1335,i4) = e_1346 ) ),
inference(superposition,[status(thm)],[c_1150,c_1999]) ).
tcf(c_2069,plain,
( ( i7 = i9 )
| ( i7 = i4 )
| ( select(a_1343,i7) = e_1348 ) ),
inference(superposition,[status(thm)],[c_1193,c_198]) ).
tcf(c_2070,plain,
( ( i9 = i1 )
| ( i4 = i1 )
| ( select(a_1343,i1) = e_1350 ) ),
inference(superposition,[status(thm)],[c_1193,c_199]) ).
tcf(c_2085,plain,
( ( i7 = i9 )
| ( i7 = i4 )
| ( i7 = i5 )
| ( i8 = i7 )
| ( select(a_1339,i7) = e_1348 ) ),
inference(superposition,[status(thm)],[c_1174,c_2069]) ).
tcf(c_2098,plain,
( ( i9 = i1 )
| ( i4 = i1 )
| ( i5 = i1 )
| ( i8 = i1 )
| ( select(a_1339,i1) = e_1350 ) ),
inference(superposition,[status(thm)],[c_1174,c_2070]) ).
tcf(c_2147,plain,
( ( i5 = i1 )
| ( i7 = i5 )
| ( select(a_1347,i5) = e_1352 ) ),
inference(superposition,[status(thm)],[c_1227,c_200]) ).
tcf(c_2148,plain,
( ( i4 = i1 )
| ( i7 = i4 )
| ( select(a_1347,i4) = e_1354 ) ),
inference(superposition,[status(thm)],[c_1227,c_201]) ).
tcf(c_2163,plain,
( ( i5 = i1 )
| ( i5 = i9 )
| ( i5 = i4 )
| ( i7 = i5 )
| ( select(a_1343,i5) = e_1352 ) ),
inference(superposition,[status(thm)],[c_1193,c_2147]) ).
tcf(c_2180,plain,
( ( i3 = i_1371 )
| ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i5 = i_1371 )
| ( select(a_1321,i_1371) = e_1372 ) ),
inference(superposition,[status(thm)],[c_1020,c_1888]) ).
tcf(c_2198,plain,
( ( e_1344 = e_1354 )
| ( i4 = i1 )
| ( i4 = i9 )
| ( i7 = i4 ) ),
inference(superposition,[status(thm)],[c_2148,c_1194]) ).
tcf(c_2213,plain,
( ( i4 = i0 )
| ( i5 = i0 )
| ( select(a_1351,i0) = e_1356 ) ),
inference(superposition,[status(thm)],[c_1264,c_202]) ).
tcf(c_2214,plain,
! [X0: $i] :
( ( X0 = i0 )
| ( X0 = i4 )
| ( X0 = i5 )
| ( select(a_1351,X0) = select(a_1358,X0) ) ),
inference(superposition,[status(thm)],[c_1264,c_1287]) ).
tcf(c_2230,plain,
( ( i1 = i0 )
| ( i4 = i0 )
| ( i5 = i0 )
| ( i7 = i0 )
| ( select(a_1347,i0) = e_1356 ) ),
inference(superposition,[status(thm)],[c_1227,c_2213]) ).
tcf(c_2247,plain,
( ( i0 = i2 )
| ( i1 = i0 )
| ( select(a_1358,i0) = e_1363 ) ),
inference(superposition,[status(thm)],[c_1304,c_205]) ).
tcf(c_2248,plain,
( ( i2 = i3 )
| ( i1 = i3 )
| ( select(a_1358,i3) = e_1365 ) ),
inference(superposition,[status(thm)],[c_1304,c_206]) ).
tcf(c_2254,plain,
( ( e_1356 = e_1363 )
| ( i0 = i2 )
| ( i1 = i0 ) ),
inference(light_normalisation,[status(thm)],[c_2247,c_784]) ).
tcf(c_2264,plain,
( ( i0 = i2 )
| ( i1 = i0 )
| ( store(a_1362,i3,e_1356) = a_1364 ) ),
inference(superposition,[status(thm)],[c_2254,c_169]) ).
tcf(c_2281,plain,
( ( i0 = i2 )
| ( i1 = i0 )
| ( select(a_1364,i3) = e_1356 ) ),
inference(superposition,[status(thm)],[c_2264,c_131]) ).
tcf(c_2293,plain,
( ( i9 = i3 )
| ( i9 = i0 )
| ( select(a_1362,i9) = e_1367 ) ),
inference(superposition,[status(thm)],[c_1351,c_207]) ).
tcf(c_2294,plain,
( ( i5 = i3 )
| ( i5 = i0 )
| ( select(a_1362,i5) = e_1369 ) ),
inference(superposition,[status(thm)],[c_1351,c_208]) ).
tcf(c_2309,plain,
( ( i9 = i3 )
| ( i9 = i2 )
| ( i9 = i0 )
| ( i9 = i1 )
| ( select(a_1358,i9) = e_1367 ) ),
inference(superposition,[status(thm)],[c_1304,c_2293]) ).
tcf(c_2322,plain,
( ( i5 = i3 )
| ( i5 = i2 )
| ( i5 = i0 )
| ( i5 = i1 )
| ( select(a_1358,i5) = e_1369 ) ),
inference(superposition,[status(thm)],[c_1304,c_2294]) ).
tcf(c_2341,plain,
( ( i9 = i_1371 )
| ( i5 = i_1371 )
| ( select(a_1366,i_1371) = e_1373 ) ),
inference(superposition,[status(thm)],[c_1396,c_210]) ).
tcf(c_2357,plain,
( ( i3 = i_1371 )
| ( i0 = i_1371 )
| ( i9 = i_1371 )
| ( i5 = i_1371 )
| ( select(a_1362,i_1371) = e_1373 ) ),
inference(superposition,[status(thm)],[c_1351,c_2341]) ).
tcf(c_2377,plain,
( ( i4 = i1 )
| ( i4 = i9 )
| ( i7 = i4 )
| ( store(a_1316,i5,e_1307) = a_1318 ) ),
inference(superposition,[status(thm)],[c_1627,c_144]) ).
tcf(c_2390,plain,
( ( i4 = i1 )
| ( i4 = i9 )
| ( i7 = i4 )
| ( store(a_1353,i5,e_1344) = a_1355 ) ),
inference(superposition,[status(thm)],[c_2198,c_164]) ).
tcf(c_2411,plain,
( ( i5 = i9 )
| ( i6 = i9 )
| ( i7 = i9 )
| ( i8 = i9 )
| ( select(a1,i9) = e_1307 ) ),
inference(superposition,[status(thm)],[c_770,c_1771]) ).
tcf(c_2441,plain,
( ( i4 = i1 )
| ( i4 = i9 )
| ( i7 = i4 )
| ( select(a_1318,i5) = e_1307 ) ),
inference(superposition,[status(thm)],[c_2377,c_131]) ).
tcf(c_2452,plain,
( ( i4 = i1 )
| ( i4 = i9 )
| ( i7 = i4 )
| ( select(a_1355,i5) = e_1344 ) ),
inference(superposition,[status(thm)],[c_2390,c_131]) ).
tcf(c_2462,plain,
( ( i5 = i4 )
| ( i6 = i4 )
| ( i7 = i4 )
| ( i8 = i4 )
| ( select(a1,i4) = e_1309 ) ),
inference(superposition,[status(thm)],[c_770,c_1789]) ).
tcf(c_2493,plain,
( ( e_1303 = e_1342 )
| ( i6 = i5 )
| ( i7 = i5 )
| ( i8 = i5 ) ),
inference(superposition,[status(thm)],[c_1507,c_1982]) ).
tcf(c_2507,plain,
( ( i6 = i5 )
| ( i7 = i5 )
| ( i8 = i5 )
| ( store(a_1341,i8,e_1303) = a_1343 ) ),
inference(superposition,[status(thm)],[c_2493,c_158]) ).
tcf(c_2520,plain,
( ( i5 = i9 )
| ( i6 = i9 )
| ( i7 = i9 )
| ( i8 = i9 )
| ( select(a1,i9) = e_1344 ) ),
inference(superposition,[status(thm)],[c_1118,c_2041]) ).
tcf(c_2541,plain,
( ( i5 = i4 )
| ( i6 = i4 )
| ( i7 = i4 )
| ( i8 = i4 )
| ( select(a1,i4) = e_1346 ) ),
inference(superposition,[status(thm)],[c_1118,c_2053]) ).
tcf(c_2576,plain,
( ( i6 = i5 )
| ( i7 = i5 )
| ( i8 = i5 )
| ( select(a_1343,i8) = e_1303 ) ),
inference(superposition,[status(thm)],[c_2507,c_131]) ).
tcf(c_2588,plain,
( ( i5 = i1 )
| ( i5 = i9 )
| ( i5 = i4 )
| ( i7 = i5 )
| ( store(a_1314,i4,e_1301) = a_1316 ) ),
inference(superposition,[status(thm)],[c_1612,c_143]) ).
tcf(c_2609,plain,
( ( i0 = i2 )
| ( i4 = i2 )
| ( i5 = i2 )
| ( select(a_1314,i2) = e_1322 ) ),
inference(superposition,[status(thm)],[c_1644,c_186]) ).
tcf(c_2610,plain,
( ( i1 = i0 )
| ( i4 = i1 )
| ( i5 = i1 )
| ( select(a_1314,i1) = e_1324 ) ),
inference(superposition,[status(thm)],[c_1644,c_187]) ).
tcf(c_2614,plain,
( ( i2 = i3 )
| ( i0 = i3 )
| ( i1 = i3 )
| ( i4 = i3 )
| ( i5 = i3 )
| ( select(a_1314,i3) = e_1328 ) ),
inference(superposition,[status(thm)],[c_1644,c_1677]) ).
tcf(c_2615,plain,
( ( i3 = i_1371 )
| ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( select(a_1314,i_1371) = e_1372 ) ),
inference(superposition,[status(thm)],[c_1644,c_2180]) ).
tcf(c_2616,plain,
( ( e_1313 = e_1324 )
| ( i1 = i0 )
| ( i4 = i1 )
| ( i5 = i1 ) ),
inference(light_normalisation,[status(thm)],[c_2610,c_603]) ).
tcf(c_2664,plain,
( ( i1 = i0 )
| ( i4 = i1 )
| ( i5 = i1 )
| ( store(a_1323,i2,e_1313) = a_1325 ) ),
inference(superposition,[status(thm)],[c_2616,c_148]) ).
tcf(c_2677,plain,
( ( i0 = i2 )
| ( i1 = i2 )
| ( i4 = i2 )
| ( i5 = i2 )
| ( i7 = i2 )
| ( select(a_1310,i2) = e_1322 ) ),
inference(superposition,[status(thm)],[c_925,c_2609]) ).
tcf(c_2694,plain,
( ( i1 = i0 )
| ( i4 = i1 )
| ( i5 = i1 )
| ( select(a_1325,i2) = e_1313 ) ),
inference(superposition,[status(thm)],[c_2664,c_131]) ).
tcf(c_2710,plain,
( ( i1 = i0 )
| ( i4 = i1 )
| ( i5 = i1 )
| ( select(a_1351,i1) = e_1359 ) ),
inference(superposition,[status(thm)],[c_2214,c_203]) ).
tcf(c_2711,plain,
( ( i0 = i2 )
| ( i4 = i2 )
| ( i5 = i2 )
| ( select(a_1351,i2) = e_1361 ) ),
inference(superposition,[status(thm)],[c_2214,c_204]) ).
tcf(c_2715,plain,
( ( i2 = i3 )
| ( i0 = i3 )
| ( i1 = i3 )
| ( i4 = i3 )
| ( i5 = i3 )
| ( select(a_1351,i3) = e_1365 ) ),
inference(superposition,[status(thm)],[c_2214,c_2248]) ).
tcf(c_2741,plain,
( ( e_1348 = e_1359 )
| ( i1 = i0 )
| ( i4 = i1 )
| ( i5 = i1 )
| ( i7 = i1 ) ),
inference(superposition,[status(thm)],[c_2710,c_1228]) ).
tcf(c_2772,plain,
( ( i0 = i2 )
| ( i1 = i2 )
| ( i4 = i2 )
| ( i5 = i2 )
| ( i7 = i2 )
| ( select(a_1347,i2) = e_1361 ) ),
inference(superposition,[status(thm)],[c_1227,c_2711]) ).
tcf(c_2790,plain,
( ( i3 = i_1371 )
| ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i5 = i_1371 )
| ( select(a_1358,i_1371) = e_1373 ) ),
inference(superposition,[status(thm)],[c_1304,c_2357]) ).
tcf(c_2810,plain,
( ( i5 = i1 )
| ( i5 = i9 )
| ( i5 = i4 )
| ( i7 = i5 )
| ( select(a_1316,i4) = e_1301 ) ),
inference(superposition,[status(thm)],[c_2588,c_131]) ).
tcf(c_2822,plain,
( ( i1 = i0 )
| ( i4 = i1 )
| ( i5 = i1 )
| ( i7 = i1 )
| ( store(a_1358,i2,e_1348) = a_1360 ) ),
inference(superposition,[status(thm)],[c_2741,c_167]) ).
tcf(c_2839,plain,
( ( i1 = i0 )
| ( i4 = i1 )
| ( i5 = i1 )
| ( i7 = i1 )
| ( select(a_1360,i2) = e_1348 ) ),
inference(superposition,[status(thm)],[c_2822,c_131]) ).
tcf(c_2851,plain,
( ( i1 = i0 )
| ( i9 = i0 )
| ( i4 = i0 )
| ( i5 = i0 )
| ( i7 = i0 )
| ( select(a_1306,i0) = e_1319 ) ),
inference(superposition,[status(thm)],[c_875,c_1659]) ).
tcf(c_2869,plain,
( ( i9 = i1 )
| ( i4 = i1 )
| ( i5 = i1 )
| ( i6 = i1 )
| ( i8 = i1 )
| ( select(a_1298,i1) = e_1311 ) ),
inference(superposition,[status(thm)],[c_847,c_1734]) ).
tcf(c_2916,plain,
( ( i7 = i9 )
| ( i7 = i4 )
| ( i7 = i5 )
| ( i7 = i6 )
| ( i8 = i7 )
| ( select(a_1298,i7) = e_1313 ) ),
inference(superposition,[status(thm)],[c_847,c_1735]) ).
tcf(c_2918,plain,
( ( e_1297 = e_1313 )
| ( i7 = i9 )
| ( i7 = i4 )
| ( i7 = i5 )
| ( i7 = i6 )
| ( i8 = i7 ) ),
inference(light_normalisation,[status(thm)],[c_2916,c_593]) ).
tcf(c_2938,plain,
( ( e_1317 = e_1330 )
| ( i5 = i3 )
| ( i5 = i2 )
| ( i5 = i0 )
| ( i5 = i1 ) ),
inference(superposition,[status(thm)],[c_1847,c_1430]) ).
tcf(c_2958,plain,
( ( i5 = i3 )
| ( i5 = i2 )
| ( i5 = i0 )
| ( i5 = i1 )
| ( store(a_1329,i9,e_1317) = a_1331 ) ),
inference(superposition,[status(thm)],[c_2938,c_151]) ).
tcf(c_2974,plain,
( ( i9 = i3 )
| ( i9 = i2 )
| ( i9 = i0 )
| ( i9 = i1 )
| ( i4 = i9 )
| ( i5 = i9 )
| ( select(a_1314,i9) = e_1332 ) ),
inference(superposition,[status(thm)],[c_1644,c_1860]) ).
tcf(c_3048,plain,
( ( i7 = i9 )
| ( i7 = i4 )
| ( i7 = i5 )
| ( i7 = i6 )
| ( i8 = i7 )
| ( select(a_1335,i7) = e_1348 ) ),
inference(superposition,[status(thm)],[c_1150,c_2085]) ).
tcf(c_3066,plain,
( ( i9 = i1 )
| ( i4 = i1 )
| ( i5 = i1 )
| ( i6 = i1 )
| ( i8 = i1 )
| ( select(a_1335,i1) = e_1350 ) ),
inference(superposition,[status(thm)],[c_1150,c_2098]) ).
tcf(c_3087,plain,
( ( e_1338 = e_1352 )
| ( i5 = i1 )
| ( i5 = i9 )
| ( i5 = i4 )
| ( i7 = i5 )
| ( i8 = i5 ) ),
inference(superposition,[status(thm)],[c_2163,c_1175]) ).
tcf(c_3104,plain,
( ( i1 = i0 )
| ( i9 = i0 )
| ( i4 = i0 )
| ( i5 = i0 )
| ( i7 = i0 )
| ( select(a_1343,i0) = e_1356 ) ),
inference(superposition,[status(thm)],[c_1193,c_2230]) ).
tcf(c_3122,plain,
( ( i9 = i3 )
| ( i9 = i2 )
| ( i9 = i0 )
| ( i9 = i1 )
| ( i4 = i9 )
| ( i5 = i9 )
| ( select(a_1351,i9) = e_1367 ) ),
inference(superposition,[status(thm)],[c_2214,c_2309]) ).
tcf(c_3144,plain,
( ( e_1354 = e_1369 )
| ( i5 = i3 )
| ( i5 = i2 )
| ( i5 = i0 )
| ( i5 = i1 ) ),
inference(superposition,[status(thm)],[c_2322,c_1457]) ).
tcf(c_3197,plain,
( ( i3 = i_1371 )
| ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( i7 = i_1371 )
| ( select(a_1310,i_1371) = e_1372 ) ),
inference(superposition,[status(thm)],[c_925,c_2615]) ).
tcf(c_3218,plain,
( ( i4 = i1 )
| ( i4 = i9 )
| ( i5 = i3 )
| ( i5 = i2 )
| ( i5 = i0 )
| ( i5 = i1 )
| ( i7 = i4 )
| ( store(a_1329,i9,e_1307) = a_1331 ) ),
inference(superposition,[status(thm)],[c_1627,c_2958]) ).
tcf(c_3264,plain,
( ( i2 = i3 )
| ( i0 = i3 )
| ( i1 = i3 )
| ( i4 = i3 )
| ( i5 = i3 )
| ( i7 = i3 )
| ( select(a_1310,i3) = e_1328 ) ),
inference(superposition,[status(thm)],[c_925,c_2614]) ).
tcf(c_3285,plain,
( ( i0 = i2 )
| ( i1 = i2 )
| ( i9 = i2 )
| ( i4 = i2 )
| ( i5 = i2 )
| ( i7 = i2 )
| ( select(a_1306,i2) = e_1322 ) ),
inference(superposition,[status(thm)],[c_875,c_2677]) ).
tcf(c_3324,plain,
( ( e_1307 = e_1344 )
| ( i5 = i9 )
| ( i6 = i9 )
| ( i7 = i9 )
| ( i8 = i9 ) ),
inference(superposition,[status(thm)],[c_2411,c_2520]) ).
tcf(c_3366,plain,
( ( e_1309 = e_1346 )
| ( i5 = i4 )
| ( i6 = i4 )
| ( i7 = i4 )
| ( i8 = i4 ) ),
inference(superposition,[status(thm)],[c_2462,c_2541]) ).
tcf(c_3454,plain,
( ( i1 = i0 )
| ( i4 = i1 )
| ( i5 = i1 )
| ( i7 = i9 )
| ( i7 = i4 )
| ( i7 = i5 )
| ( i7 = i6 )
| ( i8 = i7 )
| ( store(a_1323,i2,e_1297) = a_1325 ) ),
inference(superposition,[status(thm)],[c_2918,c_2664]) ).
tcf(c_3455,plain,
( ( i7 = i9 )
| ( i7 = i4 )
| ( i7 = i5 )
| ( i7 = i6 )
| ( i8 = i7 )
| ( store(a_1312,i1,e_1297) = a_1314 ) ),
inference(superposition,[status(thm)],[c_2918,c_142]) ).
tcf(c_3483,plain,
( ( i5 = i1 )
| ( i5 = i9 )
| ( i5 = i4 )
| ( i7 = i5 )
| ( i8 = i5 )
| ( store(a_1351,i4,e_1338) = a_1353 ) ),
inference(superposition,[status(thm)],[c_3087,c_163]) ).
tcf(c_3502,plain,
( ( i2 = i3 )
| ( i0 = i3 )
| ( i1 = i3 )
| ( i4 = i3 )
| ( i5 = i3 )
| ( i7 = i3 )
| ( select(a_1347,i3) = e_1365 ) ),
inference(superposition,[status(thm)],[c_1227,c_2715]) ).
tcf(c_3536,plain,
( ( i0 = i2 )
| ( i1 = i2 )
| ( i9 = i2 )
| ( i4 = i2 )
| ( i5 = i2 )
| ( i7 = i2 )
| ( select(a_1343,i2) = e_1361 ) ),
inference(superposition,[status(thm)],[c_1193,c_2772]) ).
tcf(c_3559,plain,
( ( i3 = i_1371 )
| ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( select(a_1351,i_1371) = e_1373 ) ),
inference(superposition,[status(thm)],[c_2214,c_2790]) ).
tcf(c_3586,plain,
( ( i7 = i9 )
| ( i7 = i4 )
| ( i7 = i5 )
| ( i7 = i6 )
| ( i8 = i7 )
| ( select(a_1314,i1) = e_1297 ) ),
inference(superposition,[status(thm)],[c_3455,c_131]) ).
tcf(c_3603,plain,
( ( i5 = i1 )
| ( i5 = i9 )
| ( i5 = i4 )
| ( i7 = i5 )
| ( i8 = i5 )
| ( select(a_1353,i4) = e_1338 ) ),
inference(superposition,[status(thm)],[c_3483,c_131]) ).
tcf(c_3631,plain,
( ( i4 = i1 )
| ( i4 = i9 )
| ( i5 = i3 )
| ( i5 = i2 )
| ( i5 = i0 )
| ( i5 = i1 )
| ( i7 = i4 )
| ( select(a_1331,i9) = e_1307 ) ),
inference(superposition,[status(thm)],[c_3218,c_131]) ).
tcf(c_3632,plain,
( ( e_1307 = e_1330 )
| ( i4 = i1 )
| ( i4 = i9 )
| ( i5 = i3 )
| ( i5 = i2 )
| ( i5 = i0 )
| ( i5 = i1 )
| ( i7 = i4 ) ),
inference(light_normalisation,[status(thm)],[c_3631,c_687]) ).
tcf(c_3703,plain,
( ( i1 = i0 )
| ( i9 = i0 )
| ( i4 = i0 )
| ( i5 = i0 )
| ( i7 = i0 )
| ( i8 = i0 )
| ( select(a_1302,i0) = e_1319 ) ),
inference(superposition,[status(thm)],[c_1040,c_2851]) ).
tcf(c_3724,plain,
( ( i9 = i1 )
| ( i4 = i1 )
| ( i5 = i1 )
| ( i6 = i1 )
| ( i7 = i1 )
| ( i8 = i1 )
| ( select(a1,i1) = e_1311 ) ),
inference(superposition,[status(thm)],[c_770,c_2869]) ).
tcf(c_3748,plain,
( ( e_1297 = e_1348 )
| ( i7 = i9 )
| ( i7 = i4 )
| ( i7 = i5 )
| ( i7 = i6 )
| ( i8 = i7 ) ),
inference(superposition,[status(thm)],[c_3048,c_1119]) ).
tcf(c_3790,plain,
( ( i7 = i9 )
| ( i7 = i4 )
| ( i7 = i5 )
| ( i7 = i6 )
| ( i8 = i7 )
| ( store(a_1347,i1,e_1297) = a_1349 ) ),
inference(superposition,[status(thm)],[c_3748,c_161]) ).
tcf(c_3819,plain,
( ( i9 = i1 )
| ( i4 = i1 )
| ( i5 = i1 )
| ( i6 = i1 )
| ( i7 = i1 )
| ( i8 = i1 )
| ( select(a1,i1) = e_1350 ) ),
inference(superposition,[status(thm)],[c_1118,c_3066]) ).
tcf(c_3840,plain,
( ( i1 = i0 )
| ( i9 = i0 )
| ( i4 = i0 )
| ( i5 = i0 )
| ( i7 = i0 )
| ( i8 = i0 )
| ( select(a_1339,i0) = e_1356 ) ),
inference(superposition,[status(thm)],[c_1174,c_3104]) ).
tcf(c_3862,plain,
( ( i7 = i9 )
| ( i7 = i4 )
| ( i7 = i5 )
| ( i7 = i6 )
| ( i8 = i7 )
| ( select(a_1349,i1) = e_1297 ) ),
inference(superposition,[status(thm)],[c_3790,c_131]) ).
tcf(c_3878,plain,
( ( i9 = i3 )
| ( i9 = i2 )
| ( i9 = i0 )
| ( i9 = i1 )
| ( i4 = i9 )
| ( i5 = i9 )
| ( i7 = i9 )
| ( select(a_1310,i9) = e_1332 ) ),
inference(superposition,[status(thm)],[c_925,c_2974]) ).
tcf(c_3880,plain,
( ( e_1309 = e_1332 )
| ( i9 = i3 )
| ( i9 = i2 )
| ( i9 = i0 )
| ( i9 = i1 )
| ( i4 = i9 )
| ( i5 = i9 )
| ( i7 = i9 ) ),
inference(light_normalisation,[status(thm)],[c_3878,c_601]) ).
tcf(c_3903,plain,
( ( i9 = i3 )
| ( i9 = i2 )
| ( i9 = i0 )
| ( i9 = i1 )
| ( i4 = i9 )
| ( i5 = i9 )
| ( i7 = i9 )
| ( select(a_1347,i9) = e_1367 ) ),
inference(superposition,[status(thm)],[c_1227,c_3122]) ).
tcf(c_3905,plain,
( ( e_1346 = e_1367 )
| ( i9 = i3 )
| ( i9 = i2 )
| ( i9 = i0 )
| ( i9 = i1 )
| ( i4 = i9 )
| ( i5 = i9 )
| ( i7 = i9 ) ),
inference(light_normalisation,[status(thm)],[c_3903,c_740]) ).
tcf(c_3928,plain,
( ( i2 = i3 )
| ( i0 = i3 )
| ( i1 = i3 )
| ( i9 = i3 )
| ( i4 = i3 )
| ( i5 = i3 )
| ( i7 = i3 )
| ( select(a_1306,i3) = e_1328 ) ),
inference(superposition,[status(thm)],[c_875,c_3264]) ).
tcf(c_3952,plain,
( ( i0 = i2 )
| ( i1 = i2 )
| ( i9 = i2 )
| ( i4 = i2 )
| ( i5 = i2 )
| ( i7 = i2 )
| ( i8 = i2 )
| ( select(a_1302,i2) = e_1322 ) ),
inference(superposition,[status(thm)],[c_1040,c_3285]) ).
tcf(c_3976,plain,
( ( i2 = i3 )
| ( i0 = i3 )
| ( i1 = i3 )
| ( i9 = i3 )
| ( i4 = i3 )
| ( i5 = i3 )
| ( i7 = i3 )
| ( select(a_1343,i3) = e_1365 ) ),
inference(superposition,[status(thm)],[c_1193,c_3502]) ).
tcf(c_4004,plain,
( ( i3 = i_1371 )
| ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( i7 = i_1371 )
| ( select(a_1306,i_1371) = e_1372 ) ),
inference(superposition,[status(thm)],[c_875,c_3197]) ).
tcf(c_4102,plain,
( ( i0 = i2 )
| ( i1 = i2 )
| ( i9 = i2 )
| ( i4 = i2 )
| ( i5 = i2 )
| ( i7 = i2 )
| ( i8 = i2 )
| ( select(a_1339,i2) = e_1361 ) ),
inference(superposition,[status(thm)],[c_1174,c_3536]) ).
tcf(c_4126,plain,
( ( i1 = i0 )
| ( i9 = i0 )
| ( i4 = i0 )
| ( i5 = i0 )
| ( i6 = i0 )
| ( i7 = i0 )
| ( i8 = i0 )
| ( select(a_1298,i0) = e_1319 ) ),
inference(superposition,[status(thm)],[c_847,c_3703]) ).
tcf(c_4164,plain,
( ( e_1311 = e_1350 )
| ( i9 = i1 )
| ( i4 = i1 )
| ( i5 = i1 )
| ( i6 = i1 )
| ( i7 = i1 )
| ( i8 = i1 ) ),
inference(superposition,[status(thm)],[c_3724,c_3819]) ).
tcf(c_4188,plain,
( ( i9 = i1 )
| ( i4 = i1 )
| ( i5 = i1 )
| ( i6 = i1 )
| ( i7 = i1 )
| ( i8 = i1 )
| ( store(a_1349,i7,e_1311) = a_1351 ) ),
inference(superposition,[status(thm)],[c_4164,c_162]) ).
tcf(c_4210,plain,
( ( i1 = i0 )
| ( i9 = i0 )
| ( i4 = i0 )
| ( i5 = i0 )
| ( i6 = i0 )
| ( i7 = i0 )
| ( i8 = i0 )
| ( select(a_1335,i0) = e_1356 ) ),
inference(superposition,[status(thm)],[c_1150,c_3840]) ).
tcf(c_4248,plain,
( ( i9 = i1 )
| ( i4 = i1 )
| ( i5 = i1 )
| ( i6 = i1 )
| ( i7 = i1 )
| ( i8 = i1 )
| ( select(a_1351,i7) = e_1311 ) ),
inference(superposition,[status(thm)],[c_4188,c_131]) ).
tcf(c_4291,plain,
( ( i9 = i3 )
| ( i9 = i2 )
| ( i9 = i0 )
| ( i9 = i1 )
| ( i4 = i9 )
| ( i5 = i9 )
| ( i7 = i9 )
| ( store(a_1366,i5,e_1346) = a_1368 ) ),
inference(superposition,[status(thm)],[c_3905,c_171]) ).
tcf(c_4318,plain,
( ( i3 = i_1371 )
| ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( i7 = i_1371 )
| ( select(a_1347,i_1371) = e_1373 ) ),
inference(superposition,[status(thm)],[c_1227,c_3559]) ).
tcf(c_4345,plain,
( ( i2 = i3 )
| ( i0 = i3 )
| ( i1 = i3 )
| ( i9 = i3 )
| ( i4 = i3 )
| ( i5 = i3 )
| ( i7 = i3 )
| ( i8 = i3 )
| ( select(a_1302,i3) = e_1328 ) ),
inference(superposition,[status(thm)],[c_1040,c_3928]) ).
tcf(c_4372,plain,
( ( i0 = i2 )
| ( i1 = i2 )
| ( i9 = i2 )
| ( i4 = i2 )
| ( i5 = i2 )
| ( i6 = i2 )
| ( i7 = i2 )
| ( i8 = i2 )
| ( select(a_1298,i2) = e_1322 ) ),
inference(superposition,[status(thm)],[c_847,c_3952]) ).
tcf(c_4409,plain,
( ( i3 = i_1371 )
| ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( i7 = i_1371 )
| ( i8 = i_1371 )
| ( select(a_1302,i_1371) = e_1372 ) ),
inference(superposition,[status(thm)],[c_1040,c_4004]) ).
tcf(c_4459,plain,
( ( i9 = i3 )
| ( i9 = i2 )
| ( i9 = i0 )
| ( i9 = i1 )
| ( i4 = i9 )
| ( i5 = i9 )
| ( i7 = i9 )
| ( select(a_1368,i5) = e_1346 ) ),
inference(superposition,[status(thm)],[c_4291,c_131]) ).
tcf(c_4554,plain,
( ( i2 = i3 )
| ( i0 = i3 )
| ( i1 = i3 )
| ( i9 = i3 )
| ( i4 = i3 )
| ( i5 = i3 )
| ( i7 = i3 )
| ( i8 = i3 )
| ( select(a_1339,i3) = e_1365 ) ),
inference(superposition,[status(thm)],[c_1174,c_3976]) ).
tcf(c_4581,plain,
( ( i0 = i2 )
| ( i1 = i2 )
| ( i9 = i2 )
| ( i4 = i2 )
| ( i5 = i2 )
| ( i6 = i2 )
| ( i7 = i2 )
| ( i8 = i2 )
| ( select(a_1335,i2) = e_1361 ) ),
inference(superposition,[status(thm)],[c_1150,c_4102]) ).
tcf(c_4610,plain,
( ( i1 = i0 )
| ( i9 = i0 )
| ( i4 = i0 )
| ( i5 = i0 )
| ( i6 = i0 )
| ( i7 = i0 )
| ( i8 = i0 )
| ( select(a1,i0) = e_1319 ) ),
inference(superposition,[status(thm)],[c_770,c_4126]) ).
tcf(c_4636,plain,
( ( i1 = i0 )
| ( i9 = i0 )
| ( i4 = i0 )
| ( i5 = i0 )
| ( i6 = i0 )
| ( i7 = i0 )
| ( i8 = i0 )
| ( select(a1,i0) = e_1356 ) ),
inference(superposition,[status(thm)],[c_1118,c_4210]) ).
tcf(c_4678,plain,
( ( e_1319 = e_1356 )
| ( i1 = i0 )
| ( i9 = i0 )
| ( i4 = i0 )
| ( i5 = i0 )
| ( i6 = i0 )
| ( i7 = i0 )
| ( i8 = i0 ) ),
inference(superposition,[status(thm)],[c_4610,c_4636]) ).
tcf(c_4704,plain,
( ( i0 = i2 )
| ( i1 = i0 )
| ( i9 = i0 )
| ( i4 = i0 )
| ( i5 = i0 )
| ( i6 = i0 )
| ( i7 = i0 )
| ( i8 = i0 )
| ( store(a_1362,i3,e_1319) = a_1364 ) ),
inference(superposition,[status(thm)],[c_4678,c_2264]) ).
tcf(c_4705,plain,
( ( i1 = i0 )
| ( i9 = i0 )
| ( i4 = i0 )
| ( i5 = i0 )
| ( i6 = i0 )
| ( i7 = i0 )
| ( i8 = i0 )
| ( store(a_1357,i0,e_1319) = a_1358 ) ),
inference(superposition,[status(thm)],[c_4678,c_166]) ).
tcf(c_4839,plain,
( ( i1 = i0 )
| ( i9 = i0 )
| ( i4 = i0 )
| ( i5 = i0 )
| ( i6 = i0 )
| ( i7 = i0 )
| ( i8 = i0 )
| ( select(a_1358,i0) = e_1319 ) ),
inference(superposition,[status(thm)],[c_4705,c_131]) ).
tcf(c_4859,plain,
( ( i3 = i_1371 )
| ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( i7 = i_1371 )
| ( select(a_1343,i_1371) = e_1373 ) ),
inference(superposition,[status(thm)],[c_1193,c_4318]) ).
tcf(c_4934,plain,
( ( i1 = i0 )
| ( i4 = i1 )
| ( i5 = i1 )
| ( i7 = i9 )
| ( i7 = i4 )
| ( i7 = i5 )
| ( i7 = i6 )
| ( i8 = i7 )
| ( select(a_1325,i2) = e_1297 ) ),
inference(superposition,[status(thm)],[c_3454,c_131]) ).
tcf(c_4985,plain,
( ( i0 = i2 )
| ( i1 = i0 )
| ( i9 = i0 )
| ( i4 = i0 )
| ( i5 = i0 )
| ( i6 = i0 )
| ( i7 = i0 )
| ( i8 = i0 )
| ( select(a_1364,i3) = e_1319 ) ),
inference(superposition,[status(thm)],[c_4704,c_131]) ).
tcf(c_4986,plain,
( ( e_1319 = e_1363 )
| ( i0 = i2 )
| ( i1 = i0 )
| ( i9 = i0 )
| ( i4 = i0 )
| ( i5 = i0 )
| ( i6 = i0 )
| ( i7 = i0 )
| ( i8 = i0 ) ),
inference(light_normalisation,[status(thm)],[c_4985,c_808]) ).
tcf(c_5014,plain,
( ( e_1319 = e_1356 )
| ( i0 = i2 )
| ( i1 = i0 )
| ( i9 = i0 )
| ( i4 = i0 )
| ( i5 = i0 )
| ( i6 = i0 )
| ( i7 = i0 )
| ( i8 = i0 ) ),
inference(superposition,[status(thm)],[c_2254,c_4986]) ).
tcf(c_5046,plain,
( ( i2 = i3 )
| ( i0 = i3 )
| ( i1 = i3 )
| ( i9 = i3 )
| ( i4 = i3 )
| ( i5 = i3 )
| ( i6 = i3 )
| ( i7 = i3 )
| ( i8 = i3 )
| ( select(a_1298,i3) = e_1328 ) ),
inference(superposition,[status(thm)],[c_847,c_4345]) ).
tcf(c_5076,plain,
( ( i0 = i2 )
| ( i1 = i2 )
| ( i9 = i2 )
| ( i4 = i2 )
| ( i5 = i2 )
| ( i6 = i2 )
| ( i7 = i2 )
| ( i8 = i2 )
| ( select(a1,i2) = e_1322 ) ),
inference(superposition,[status(thm)],[c_770,c_4372]) ).
tcf(c_5105,plain,
( ( i2 = i3 )
| ( i0 = i3 )
| ( i1 = i3 )
| ( i9 = i3 )
| ( i4 = i3 )
| ( i5 = i3 )
| ( i6 = i3 )
| ( i7 = i3 )
| ( i8 = i3 )
| ( select(a_1335,i3) = e_1365 ) ),
inference(superposition,[status(thm)],[c_1150,c_4554]) ).
tcf(c_5136,plain,
( ( i0 = i2 )
| ( i1 = i2 )
| ( i9 = i2 )
| ( i4 = i2 )
| ( i5 = i2 )
| ( i6 = i2 )
| ( i7 = i2 )
| ( i8 = i2 )
| ( select(a1,i2) = e_1361 ) ),
inference(superposition,[status(thm)],[c_1118,c_4581]) ).
tcf(c_5166,plain,
( ( i3 = i_1371 )
| ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( i7 = i_1371 )
| ( i8 = i_1371 )
| ( select(a_1339,i_1371) = e_1373 ) ),
inference(superposition,[status(thm)],[c_1174,c_4859]) ).
tcf(c_5241,plain,
( ( e_1322 = e_1361 )
| ( i0 = i2 )
| ( i1 = i2 )
| ( i9 = i2 )
| ( i4 = i2 )
| ( i5 = i2 )
| ( i6 = i2 )
| ( i7 = i2 )
| ( i8 = i2 ) ),
inference(superposition,[status(thm)],[c_5076,c_5136]) ).
tcf(c_5270,plain,
( ( i0 = i2 )
| ( i1 = i2 )
| ( i9 = i2 )
| ( i4 = i2 )
| ( i5 = i2 )
| ( i6 = i2 )
| ( i7 = i2 )
| ( i8 = i2 )
| ( store(a_1360,i1,e_1322) = a_1362 ) ),
inference(superposition,[status(thm)],[c_5241,c_168]) ).
tcf(c_5299,plain,
( ( i0 = i2 )
| ( i1 = i2 )
| ( i9 = i2 )
| ( i4 = i2 )
| ( i5 = i2 )
| ( i6 = i2 )
| ( i7 = i2 )
| ( i8 = i2 )
| ( select(a_1362,i1) = e_1322 ) ),
inference(superposition,[status(thm)],[c_5270,c_131]) ).
tcf(c_5321,plain,
( ( i3 = i_1371 )
| ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( i6 = i_1371 )
| ( i7 = i_1371 )
| ( i8 = i_1371 )
| ( select(a_1298,i_1371) = e_1372 ) ),
inference(superposition,[status(thm)],[c_847,c_4409]) ).
tcf(c_5354,plain,
( ( i3 = i_1371 )
| ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( i6 = i_1371 )
| ( i7 = i_1371 )
| ( i8 = i_1371 )
| ( select(a_1335,i_1371) = e_1373 ) ),
inference(superposition,[status(thm)],[c_1150,c_5166]) ).
tcf(c_5494,plain,
( ( i2 = i3 )
| ( i0 = i3 )
| ( i1 = i3 )
| ( i9 = i3 )
| ( i4 = i3 )
| ( i5 = i3 )
| ( i6 = i3 )
| ( i7 = i3 )
| ( i8 = i3 )
| ( select(a1,i3) = e_1328 ) ),
inference(superposition,[status(thm)],[c_770,c_5046]) ).
tcf(c_5526,plain,
( ( i2 = i3 )
| ( i0 = i3 )
| ( i1 = i3 )
| ( i9 = i3 )
| ( i4 = i3 )
| ( i5 = i3 )
| ( i6 = i3 )
| ( i7 = i3 )
| ( i8 = i3 )
| ( select(a1,i3) = e_1365 ) ),
inference(superposition,[status(thm)],[c_1118,c_5105]) ).
tcf(c_5578,plain,
( ( e_1328 = e_1365 )
| ( i2 = i3 )
| ( i0 = i3 )
| ( i1 = i3 )
| ( i9 = i3 )
| ( i4 = i3 )
| ( i5 = i3 )
| ( i6 = i3 )
| ( i7 = i3 )
| ( i8 = i3 ) ),
inference(superposition,[status(thm)],[c_5494,c_5526]) ).
tcf(c_5611,plain,
( ( i2 = i3 )
| ( i0 = i3 )
| ( i1 = i3 )
| ( i9 = i3 )
| ( i4 = i3 )
| ( i5 = i3 )
| ( i6 = i3 )
| ( i7 = i3 )
| ( i8 = i3 )
| ( store(a_1364,i0,e_1328) = a_1366 ) ),
inference(superposition,[status(thm)],[c_5578,c_170]) ).
tcf(c_5643,plain,
( ( i2 = i3 )
| ( i0 = i3 )
| ( i1 = i3 )
| ( i9 = i3 )
| ( i4 = i3 )
| ( i5 = i3 )
| ( i6 = i3 )
| ( i7 = i3 )
| ( i8 = i3 )
| ( select(a_1366,i0) = e_1328 ) ),
inference(superposition,[status(thm)],[c_5611,c_131]) ).
tcf(c_5667,plain,
( ( i3 = i_1371 )
| ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( i6 = i_1371 )
| ( i7 = i_1371 )
| ( i8 = i_1371 )
| ( select(a1,i_1371) = e_1372 ) ),
inference(superposition,[status(thm)],[c_770,c_5321]) ).
tcf(c_5703,plain,
( ( i3 = i_1371 )
| ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( i6 = i_1371 )
| ( i7 = i_1371 )
| ( i8 = i_1371 )
| ( select(a1,i_1371) = e_1373 ) ),
inference(superposition,[status(thm)],[c_1118,c_5354]) ).
tcf(c_5760,plain,
( ( e_1372 = e_1373 )
| ( i3 = i_1371 )
| ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( i6 = i_1371 )
| ( i7 = i_1371 )
| ( i8 = i_1371 ) ),
inference(superposition,[status(thm)],[c_5667,c_5703]) ).
tcf(c_5762,plain,
( ( i3 = i_1371 )
| ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( i6 = i_1371 )
| ( i7 = i_1371 )
| ( i8 = i_1371 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5760,c_388]) ).
tcf(c_5814,plain,
( ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( i6 = i_1371 )
| ( i7 = i_1371 )
| ( i8 = i_1371 )
| ( select(a_1366,i3) = e_1373 ) ),
inference(superposition,[status(thm)],[c_5762,c_2341]) ).
tcf(c_5816,plain,
( ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( i6 = i_1371 )
| ( i7 = i_1371 )
| ( i8 = i_1371 )
| ( select(a_1329,i3) = e_1372 ) ),
inference(superposition,[status(thm)],[c_5762,c_1876]) ).
tcf(c_5883,plain,
( ( e_1363 = e_1373 )
| ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i0 = i3 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( i6 = i_1371 )
| ( i7 = i_1371 )
| ( i8 = i_1371 ) ),
inference(superposition,[status(thm)],[c_5814,c_1352]) ).
tcf(c_5918,plain,
( ( e_1326 = e_1372 )
| ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i0 = i3 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( i6 = i_1371 )
| ( i7 = i_1371 )
| ( i8 = i_1371 ) ),
inference(superposition,[status(thm)],[c_5816,c_1052]) ).
tcf(c_6062,plain,
( ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i0 = i3 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( i6 = i_1371 )
| ( i7 = i_1371 )
| ( i8 = i_1371 )
| ( e_1363 != e_1372 ) ),
inference(superposition,[status(thm)],[c_5883,c_388]) ).
tcf(c_6119,plain,
( ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i0 = i3 )
| ( i1 = i_1371 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( i6 = i_1371 )
| ( i7 = i_1371 )
| ( i8 = i_1371 )
| ( e_1326 != e_1363 ) ),
inference(superposition,[status(thm)],[c_5918,c_6062]) ).
tcf(c_6154,plain,
( ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i0 = i3 )
| ( i0 = i2 )
| ( i1 = i_1371 )
| ( i1 = i0 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( i6 = i_1371 )
| ( i7 = i_1371 )
| ( i8 = i_1371 )
| ( e_1326 != e_1356 ) ),
inference(superposition,[status(thm)],[c_2254,c_6119]) ).
tcf(c_6229,plain,
( ( i2 = i_1371 )
| ( i0 = i_1371 )
| ( i0 = i3 )
| ( i0 = i2 )
| ( i1 = i_1371 )
| ( i1 = i0 )
| ( i9 = i_1371 )
| ( i4 = i_1371 )
| ( i5 = i_1371 )
| ( i6 = i_1371 )
| ( i7 = i_1371 )
| ( i8 = i_1371 )
| ( e_1319 != e_1356 ) ),
inference(superposition,[status(thm)],[c_1683,c_6154]) ).
tcf(c_30229,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_6229,c_5762,c_5643,c_5578,c_5299,c_5241,c_5166,c_5014,c_4985,c_4934,c_4859,c_4839,c_4678,c_4554,c_4459,c_4409,c_4345,c_4248,c_4164,c_4102,c_4004,c_3976,c_3952,c_3928,c_3880,c_3862,c_3840,c_3703,c_3632,c_3603,c_3586,c_3559,c_3536,c_3502,c_3366,c_3324,c_3285,c_3264,c_3144,c_3122,c_3104,c_3066,c_2974,c_2938,c_2869,c_2851,c_2839,c_2810,c_2790,c_2772,c_2741,c_2715,c_2711,c_2710,c_2694,c_2677,c_2616,c_2615,c_2614,c_2609,c_2576,c_2541,c_2493,c_2452,c_2441,c_2357,c_2341,c_2309,c_2294,c_2293,c_2281,c_2248,c_2230,c_2213,c_2180,c_2163,c_2148,c_2147,c_2098,c_2085,c_2070,c_2069,c_2053,c_2041,c_1999,c_1998,c_1971,c_1959,c_1916,c_1905,c_1888,c_1876,c_1860,c_1812,c_1811,c_1789,c_1771,c_1735,c_1734,c_1731,c_1730,c_1716,c_1677,c_1659,c_1642,c_1627,c_1612,c_1583,c_1582,c_1524,c_1523,c_1495,c_1458,c_1457,c_1431,c_1430,c_1397,c_1352,c_1305,c_1265,c_1228,c_1194,c_1175,c_1151,c_1119,c_1096,c_1052,c_1039,c_1019,c_963,c_924,c_910,c_874,c_846,c_826,c_818,c_813,c_808,c_798,c_791,c_784,c_779,c_760,c_755,c_750,c_745,c_740,c_730,c_724,c_713,c_706,c_701,c_692,c_682,c_610,c_609,c_607,c_605,c_604,c_603,c_601,c_599,c_598,c_595,c_594,c_593,c_388,c_210,c_209,c_208,c_207,c_206,c_205,c_204,c_203,c_202,c_201,c_200,c_199,c_198,c_197,c_196,c_195,c_193,c_191,c_190,c_189,c_188,c_187,c_186,c_185,c_184,c_183,c_182,c_181,c_180,c_179,c_177,c_176,c_175,c_174,c_173,c_164,c_163,c_162,c_161,c_160,c_159,c_158,c_156,c_154,c_153,c_144,c_143,c_142,c_141,c_140,c_139,c_137,c_136,c_135,c_134,c_133]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV537-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.38 % Computer : n016.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Thu Sep 24 20:26:46 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.43
% 0.10/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.43
% 0.10/0.43 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 18.83/4.27 % SZS status Started for theBenchmark.p
% 18.83/4.27 % SZS status Unsatisfiable for theBenchmark.p
% 18.83/4.27
% 18.83/4.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 18.83/4.27
% 18.83/4.27 % ------ iProver source info
% 18.83/4.27
% 18.83/4.27 % git: date: 2026-07-19 20:42:38 +0200
% 18.83/4.27 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 18.83/4.27 % git: non_committed_changes: false
% 18.83/4.27
% 18.83/4.27 % ------ Parsing...% successful
% 18.83/4.27
% 18.83/4.27
% 18.83/4.27 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 18.83/4.27
% 18.83/4.27 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 18.83/4.27
% 18.83/4.27 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 18.83/4.27
% 18.83/4.27 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 18.83/4.27 % ------ Proving...
% 18.83/4.27 % ------ Problem Properties
% 18.83/4.27
% 18.83/4.27 %
% 18.83/4.27 % clauses 82
% 18.83/4.27 % conjectures 1
% 18.83/4.27 % EPR 1
% 18.83/4.27 % Horn 81
% 18.83/4.27 % unary 81
% 18.83/4.27 % binary 1
% 18.83/4.27 % lits 83
% 18.83/4.27 % lits eq 83
% 18.83/4.27 % fd_pure 0
% 18.83/4.27 % fd_pseudo 0
% 18.83/4.27 % fd_cond 0
% 18.83/4.27 % fd_pseudo_cond 1
% 18.83/4.27 % AC symbols 0
% 18.83/4.27
% 18.83/4.27 % ------ Schedule dynamic 5 is on
% 18.83/4.27
% 18.83/4.27 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 18.83/4.27
% 18.83/4.27
% 18.83/4.27 % ------
% 18.83/4.27 % Current options:
% 18.83/4.27 % ------
% 18.83/4.27
% 18.83/4.27
% 18.83/4.27 %
% 18.83/4.27
% 18.83/4.27 % ------ Proving...
% 18.83/4.27 %
% 18.83/4.27
% 18.83/4.27 % SZS status Unsatisfiable for theBenchmark.p
% 18.83/4.27
% 18.83/4.27 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 18.83/4.28
% 18.83/4.28
%------------------------------------------------------------------------------