%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SWV543-1.010 : TPTP v9.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.cKyRrQczC7 true
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 2 05:01:33 PM UTC 2025
% Result : Unsatisfiable 4.26s 1.20s
% Output : Refutation 4.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWV543-1.010 : TPTP v9.2.0. Released v4.0.0.
% 0.12/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.cKyRrQczC7 true
% 0.13/0.34 % Computer : n015.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Oct 1 12:35:53 EDT 2025
% 0.13/0.35 % CPUTime :
% 0.13/0.35 % Running portfolio for 300 s
% 0.13/0.35 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.35 % Number of cores: 8
% 0.20/0.35 % Python version: Python 3.6.8
% 0.20/0.35 % Running in FO mode
% 0.56/0.65 % Total configuration time : 435
% 0.56/0.65 % Estimated wc time : 1092
% 0.56/0.65 % Estimated cpu time (7 cpus) : 156.0
% 0.56/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.56/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.56/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.57/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.57/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.57/0.77 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.57/0.77 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.57/0.79 % /export/starexec/sandbox2/solver/bin/fo/fo1_lcnf.sh running for 50s
% 4.26/1.20 % Solved by fo/fo13.sh.
% 4.26/1.20 % done 354 iterations in 0.416s
% 4.26/1.20 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 4.26/1.20 % SZS output start Refutation
% 4.26/1.20 thf(a_1272_type, type, a_1272: $i).
% 4.26/1.20 thf(a_1302_type, type, a_1302: $i).
% 4.26/1.20 thf(a_1253_type, type, a_1253: $i).
% 4.26/1.20 thf(e_1254_type, type, e_1254: $i).
% 4.26/1.20 thf(e_1264_type, type, e_1264: $i).
% 4.26/1.20 thf(e_1316_type, type, e_1316: $i).
% 4.26/1.20 thf(a_1255_type, type, a_1255: $i).
% 4.26/1.20 thf(i9_type, type, i9: $i).
% 4.26/1.20 thf(e_1248_type, type, e_1248: $i).
% 4.26/1.20 thf(a_1282_type, type, a_1282: $i).
% 4.26/1.20 thf(a1_type, type, a1: $i).
% 4.26/1.20 thf(e_1295_type, type, e_1295: $i).
% 4.26/1.20 thf(a_1270_type, type, a_1270: $i).
% 4.26/1.20 thf(a_1300_type, type, a_1300: $i).
% 4.26/1.20 thf(e_1279_type, type, e_1279: $i).
% 4.26/1.20 thf(e_1289_type, type, e_1289: $i).
% 4.26/1.20 thf(store_type, type, store: $i > $i > $i > $i).
% 4.26/1.20 thf(a_1290_type, type, a_1290: $i).
% 4.26/1.20 thf(e_1275_type, type, e_1275: $i).
% 4.26/1.20 thf(a_1259_type, type, a_1259: $i).
% 4.26/1.20 thf(e_1285_type, type, e_1285: $i).
% 4.26/1.20 thf(a_1311_type, type, a_1311: $i).
% 4.26/1.20 thf(a_1265_type, type, a_1265: $i).
% 4.26/1.20 thf(e_1277_type, type, e_1277: $i).
% 4.26/1.20 thf(a_1317_type, type, a_1317: $i).
% 4.26/1.20 thf(e_1252_type, type, e_1252: $i).
% 4.26/1.20 thf(i6_type, type, i6: $i).
% 4.26/1.20 thf(a_1298_type, type, a_1298: $i).
% 4.26/1.20 thf(e_1268_type, type, e_1268: $i).
% 4.26/1.20 thf(a_1304_type, type, a_1304: $i).
% 4.26/1.20 thf(a_1274_type, type, a_1274: $i).
% 4.26/1.20 thf(e_1308_type, type, e_1308: $i).
% 4.26/1.20 thf(i2_type, type, i2: $i).
% 4.26/1.20 thf(a_1280_type, type, a_1280: $i).
% 4.26/1.20 thf(a_1257_type, type, a_1257: $i).
% 4.26/1.20 thf(a_1315_type, type, a_1315: $i).
% 4.26/1.20 thf(e_1260_type, type, e_1260: $i).
% 4.26/1.20 thf(a_1313_type, type, a_1313: $i).
% 4.26/1.20 thf(e_1244_type, type, e_1244: $i).
% 4.26/1.20 thf(a_1309_type, type, a_1309: $i).
% 4.26/1.20 thf(i5_type, type, i5: $i).
% 4.26/1.20 thf(a_1306_type, type, a_1306: $i).
% 4.26/1.20 thf(a_1245_type, type, a_1245: $i).
% 4.26/1.20 thf(e_1287_type, type, e_1287: $i).
% 4.26/1.20 thf(i4_type, type, i4: $i).
% 4.26/1.20 thf(a_1292_type, type, a_1292: $i).
% 4.26/1.20 thf(e_1256_type, type, e_1256: $i).
% 4.26/1.20 thf(a_1294_type, type, a_1294: $i).
% 4.26/1.20 thf(e_1273_type, type, e_1273: $i).
% 4.26/1.20 thf(a_1288_type, type, a_1288: $i).
% 4.26/1.20 thf(a_1269_type, type, a_1269: $i).
% 4.26/1.20 thf(a_1251_type, type, a_1251: $i).
% 4.26/1.20 thf(a_1284_type, type, a_1284: $i).
% 4.26/1.20 thf(a_1307_type, type, a_1307: $i).
% 4.26/1.20 thf(e_1318_type, type, e_1318: $i).
% 4.26/1.20 thf(e_1297_type, type, e_1297: $i).
% 4.26/1.20 thf(e_1281_type, type, e_1281: $i).
% 4.26/1.20 thf(i0_type, type, i0: $i).
% 4.26/1.20 thf(a_1286_type, type, a_1286: $i).
% 4.26/1.20 thf(e_1314_type, type, e_1314: $i).
% 4.26/1.20 thf(select_type, type, select: $i > $i > $i).
% 4.26/1.20 thf(e_1310_type, type, e_1310: $i).
% 4.26/1.20 thf(i7_type, type, i7: $i).
% 4.26/1.20 thf(i3_type, type, i3: $i).
% 4.26/1.20 thf(a_1278_type, type, a_1278: $i).
% 4.26/1.20 thf(a_1267_type, type, a_1267: $i).
% 4.26/1.20 thf(e_1299_type, type, e_1299: $i).
% 4.26/1.20 thf(e_1262_type, type, e_1262: $i).
% 4.26/1.20 thf(a_1276_type, type, a_1276: $i).
% 4.26/1.20 thf(a_1263_type, type, a_1263: $i).
% 4.26/1.20 thf(e_1266_type, type, e_1266: $i).
% 4.26/1.20 thf(a_1247_type, type, a_1247: $i).
% 4.26/1.20 thf(a_1249_type, type, a_1249: $i).
% 4.26/1.20 thf(e_1301_type, type, e_1301: $i).
% 4.26/1.20 thf(i8_type, type, i8: $i).
% 4.26/1.20 thf(a_1261_type, type, a_1261: $i).
% 4.26/1.20 thf(e_1293_type, type, e_1293: $i).
% 4.26/1.20 thf(e_1312_type, type, e_1312: $i).
% 4.26/1.20 thf(i1_type, type, i1: $i).
% 4.26/1.20 thf(a_1283_type, type, a_1283: $i).
% 4.26/1.20 thf(e_1303_type, type, e_1303: $i).
% 4.26/1.20 thf(a_1296_type, type, a_1296: $i).
% 4.26/1.20 thf(e_1250_type, type, e_1250: $i).
% 4.26/1.20 thf(e_1246_type, type, e_1246: $i).
% 4.26/1.20 thf(e_1258_type, type, e_1258: $i).
% 4.26/1.20 thf(e_1291_type, type, e_1291: $i).
% 4.26/1.20 thf(a_1319_type, type, a_1319: $i).
% 4.26/1.20 thf(e_1271_type, type, e_1271: $i).
% 4.26/1.20 thf(e_1305_type, type, e_1305: $i).
% 4.26/1.20 thf(hyp58, axiom, (( e_1281 ) = ( select @ a_1278 @ i9 ))).
% 4.26/1.20 thf(zip_derived_cl61, plain, (((e_1281) = (select @ a_1278 @ i9))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp58])).
% 4.26/1.20 thf(hyp57, axiom, (( e_1279 ) = ( select @ a_1278 @ i5 ))).
% 4.26/1.20 thf(zip_derived_cl60, plain, (((e_1279) = (select @ a_1278 @ i5))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp57])).
% 4.26/1.20 thf(a3, axiom,
% 4.26/1.20 (( store @ ( store @ A @ I @ ( select @ A @ J ) ) @ J @ ( select @ A @ I ) ) =
% 4.26/1.20 ( store @ ( store @ A @ J @ ( select @ A @ I ) ) @ I @ ( select @ A @ J ) ))).
% 4.26/1.20 thf(zip_derived_cl2, plain,
% 4.26/1.20 (![X0 : $i, X1 : $i, X2 : $i]:
% 4.26/1.20 ((store @ (store @ X0 @ X2 @ (select @ X0 @ X1)) @ X1 @
% 4.26/1.20 (select @ X0 @ X2))
% 4.26/1.20 = (store @ (store @ X0 @ X1 @ (select @ X0 @ X2)) @ X2 @
% 4.26/1.20 (select @ X0 @ X1)))),
% 4.26/1.20 inference('cnf', [status(esa)], [a3])).
% 4.26/1.20 thf(zip_derived_cl104, plain,
% 4.26/1.20 (![X0 : $i]:
% 4.26/1.20 ((store @ (store @ a_1278 @ i5 @ (select @ a_1278 @ X0)) @ X0 @ e_1279)
% 4.26/1.20 = (store @ (store @ a_1278 @ X0 @ e_1279) @ i5 @
% 4.26/1.20 (select @ a_1278 @ X0)))),
% 4.26/1.20 inference('s_sup+', [status(thm)], [zip_derived_cl60, zip_derived_cl2])).
% 4.26/1.20 thf(zip_derived_cl2607, plain,
% 4.26/1.20 (((store @ (store @ a_1278 @ i5 @ e_1281) @ i9 @ e_1279)
% 4.26/1.20 = (store @ (store @ a_1278 @ i9 @ e_1279) @ i5 @ e_1281))),
% 4.26/1.20 inference('s_sup+', [status(thm)], [zip_derived_cl61, zip_derived_cl104])).
% 4.26/1.20 thf(hyp38, axiom, (( a_1317 ) = ( store @ a_1315 @ i5 @ e_1316 ))).
% 4.26/1.20 thf(zip_derived_cl41, plain, (((a_1317) = (store @ a_1315 @ i5 @ e_1316))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp38])).
% 4.26/1.20 thf(hyp37, axiom, (( a_1315 ) = ( store @ a_1313 @ i0 @ e_1314 ))).
% 4.26/1.20 thf(zip_derived_cl40, plain, (((a_1315) = (store @ a_1313 @ i0 @ e_1314))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp37])).
% 4.26/1.20 thf(hyp73, axiom, (( e_1314 ) = ( select @ a_1311 @ i3 ))).
% 4.26/1.20 thf(zip_derived_cl76, plain, (((e_1314) = (select @ a_1311 @ i3))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp73])).
% 4.26/1.20 thf(hyp53, axiom, (( e_1271 ) = ( select @ a_1270 @ i2 ))).
% 4.26/1.20 thf(zip_derived_cl56, plain, (((e_1271) = (select @ a_1270 @ i2))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp53])).
% 4.26/1.20 thf(hyp54, axiom, (( e_1273 ) = ( select @ a_1270 @ i1 ))).
% 4.26/1.20 thf(zip_derived_cl57, plain, (((e_1273) = (select @ a_1270 @ i1))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp54])).
% 4.26/1.20 thf(zip_derived_cl2, plain,
% 4.26/1.20 (![X0 : $i, X1 : $i, X2 : $i]:
% 4.26/1.20 ((store @ (store @ X0 @ X2 @ (select @ X0 @ X1)) @ X1 @
% 4.26/1.20 (select @ X0 @ X2))
% 4.26/1.20 = (store @ (store @ X0 @ X1 @ (select @ X0 @ X2)) @ X2 @
% 4.26/1.20 (select @ X0 @ X1)))),
% 4.26/1.20 inference('cnf', [status(esa)], [a3])).
% 4.26/1.20 thf(zip_derived_cl100, plain,
% 4.26/1.20 (![X0 : $i]:
% 4.26/1.20 ((store @ (store @ a_1270 @ i1 @ (select @ a_1270 @ X0)) @ X0 @ e_1273)
% 4.26/1.20 = (store @ (store @ a_1270 @ X0 @ e_1273) @ i1 @
% 4.26/1.20 (select @ a_1270 @ X0)))),
% 4.26/1.20 inference('s_sup+', [status(thm)], [zip_derived_cl57, zip_derived_cl2])).
% 4.26/1.20 thf(zip_derived_cl2363, plain,
% 4.26/1.20 (((store @ (store @ a_1270 @ i1 @ e_1271) @ i2 @ e_1273)
% 4.26/1.20 = (store @ (store @ a_1270 @ i2 @ e_1273) @ i1 @ e_1271))),
% 4.26/1.20 inference('s_sup+', [status(thm)], [zip_derived_cl56, zip_derived_cl100])).
% 4.26/1.20 thf(hyp14, axiom, (( a_1272 ) = ( store @ a_1270 @ i1 @ e_1271 ))).
% 4.26/1.20 thf(zip_derived_cl17, plain, (((a_1272) = (store @ a_1270 @ i1 @ e_1271))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp14])).
% 4.26/1.20 thf(hyp15, axiom, (( a_1274 ) = ( store @ a_1272 @ i2 @ e_1273 ))).
% 4.26/1.20 thf(zip_derived_cl18, plain, (((a_1274) = (store @ a_1272 @ i2 @ e_1273))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp15])).
% 4.26/1.20 thf(hyp34, axiom, (( a_1309 ) = ( store @ a_1307 @ i2 @ e_1308 ))).
% 4.26/1.20 thf(zip_derived_cl37, plain, (((a_1309) = (store @ a_1307 @ i2 @ e_1308))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp34])).
% 4.26/1.20 thf(hyp33, axiom, (( a_1307 ) = ( store @ a_1306 @ i0 @ e_1305 ))).
% 4.26/1.20 thf(zip_derived_cl36, plain, (((a_1307) = (store @ a_1306 @ i0 @ e_1305))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp33])).
% 4.26/1.20 thf(hyp69, axiom, (( e_1305 ) = ( select @ a_1304 @ i0 ))).
% 4.26/1.20 thf(zip_derived_cl72, plain, (((e_1305) = (select @ a_1304 @ i0))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp69])).
% 4.26/1.20 thf(hyp31, axiom, (( a_1304 ) = ( store @ a_1302 @ i5 @ e_1303 ))).
% 4.26/1.20 thf(zip_derived_cl34, plain, (((a_1304) = (store @ a_1302 @ i5 @ e_1303))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp31])).
% 4.26/1.20 thf(hyp68, axiom, (( e_1303 ) = ( select @ a_1300 @ i4 ))).
% 4.26/1.20 thf(zip_derived_cl71, plain, (((e_1303) = (select @ a_1300 @ i4))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp68])).
% 4.26/1.20 thf(hyp48, axiom, (( e_1260 ) = ( select @ a_1259 @ i1 ))).
% 4.26/1.20 thf(zip_derived_cl51, plain, (((e_1260) = (select @ a_1259 @ i1))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp48])).
% 4.26/1.20 thf(hyp49, axiom, (( e_1262 ) = ( select @ a_1259 @ i7 ))).
% 4.26/1.20 thf(zip_derived_cl52, plain, (((e_1262) = (select @ a_1259 @ i7))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp49])).
% 4.26/1.20 thf(zip_derived_cl2, plain,
% 4.26/1.20 (![X0 : $i, X1 : $i, X2 : $i]:
% 4.26/1.20 ((store @ (store @ X0 @ X2 @ (select @ X0 @ X1)) @ X1 @
% 4.26/1.20 (select @ X0 @ X2))
% 4.26/1.20 = (store @ (store @ X0 @ X1 @ (select @ X0 @ X2)) @ X2 @
% 4.26/1.20 (select @ X0 @ X1)))),
% 4.26/1.20 inference('cnf', [status(esa)], [a3])).
% 4.26/1.20 thf(zip_derived_cl95, plain,
% 4.26/1.20 (![X0 : $i]:
% 4.26/1.20 ((store @ (store @ a_1259 @ i7 @ (select @ a_1259 @ X0)) @ X0 @ e_1262)
% 4.26/1.20 = (store @ (store @ a_1259 @ X0 @ e_1262) @ i7 @
% 4.26/1.20 (select @ a_1259 @ X0)))),
% 4.26/1.20 inference('s_sup+', [status(thm)], [zip_derived_cl52, zip_derived_cl2])).
% 4.26/1.20 thf(zip_derived_cl2003, plain,
% 4.26/1.20 (((store @ (store @ a_1259 @ i7 @ e_1260) @ i1 @ e_1262)
% 4.26/1.20 = (store @ (store @ a_1259 @ i1 @ e_1262) @ i7 @ e_1260))),
% 4.26/1.20 inference('s_sup+', [status(thm)], [zip_derived_cl51, zip_derived_cl95])).
% 4.26/1.20 thf(hyp8, axiom, (( a_1261 ) = ( store @ a_1259 @ i7 @ e_1260 ))).
% 4.26/1.20 thf(zip_derived_cl11, plain, (((a_1261) = (store @ a_1259 @ i7 @ e_1260))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp8])).
% 4.26/1.20 thf(hyp9, axiom, (( a_1263 ) = ( store @ a_1261 @ i1 @ e_1262 ))).
% 4.26/1.20 thf(zip_derived_cl12, plain, (((a_1263) = (store @ a_1261 @ i1 @ e_1262))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp9])).
% 4.26/1.20 thf(hyp28, axiom, (( a_1298 ) = ( store @ a_1296 @ i1 @ e_1297 ))).
% 4.26/1.20 thf(zip_derived_cl31, plain, (((a_1298) = (store @ a_1296 @ i1 @ e_1297))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp28])).
% 4.26/1.20 thf(hyp27, axiom, (( a_1296 ) = ( store @ a_1294 @ i9 @ e_1295 ))).
% 4.26/1.20 thf(zip_derived_cl30, plain, (((a_1296) = (store @ a_1294 @ i9 @ e_1295))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp27])).
% 4.26/1.20 thf(hyp64, axiom, (( e_1295 ) = ( select @ a_1292 @ i4 ))).
% 4.26/1.20 thf(zip_derived_cl67, plain, (((e_1295) = (select @ a_1292 @ i4))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp64])).
% 4.26/1.20 thf(hyp3, axiom, (( a_1251 ) = ( store @ a_1249 @ i8 @ e_1250 ))).
% 4.26/1.20 thf(zip_derived_cl6, plain, (((a_1251) = (store @ a_1249 @ i8 @ e_1250))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp3])).
% 4.26/1.20 thf(a1, axiom, (( select @ ( store @ A @ I @ E ) @ I ) = ( E ))).
% 4.26/1.20 thf(zip_derived_cl0, plain,
% 4.26/1.20 (![X0 : $i, X1 : $i, X2 : $i]:
% 4.26/1.20 ((select @ (store @ X1 @ X2 @ X0) @ X2) = (X0))),
% 4.26/1.20 inference('cnf', [status(esa)], [a1])).
% 4.26/1.20 thf(zip_derived_cl263, plain, (((select @ a_1251 @ i8) = (e_1250))),
% 4.26/1.20 inference('s_sup+', [status(thm)], [zip_derived_cl6, zip_derived_cl0])).
% 4.26/1.20 thf(hyp44, axiom, (( e_1252 ) = ( select @ a_1251 @ i5 ))).
% 4.26/1.20 thf(zip_derived_cl47, plain, (((e_1252) = (select @ a_1251 @ i5))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp44])).
% 4.26/1.20 thf(zip_derived_cl2, plain,
% 4.26/1.20 (![X0 : $i, X1 : $i, X2 : $i]:
% 4.26/1.20 ((store @ (store @ X0 @ X2 @ (select @ X0 @ X1)) @ X1 @
% 4.26/1.20 (select @ X0 @ X2))
% 4.26/1.20 = (store @ (store @ X0 @ X1 @ (select @ X0 @ X2)) @ X2 @
% 4.26/1.20 (select @ X0 @ X1)))),
% 4.26/1.20 inference('cnf', [status(esa)], [a3])).
% 4.26/1.20 thf(zip_derived_cl92, plain,
% 4.26/1.20 (![X0 : $i]:
% 4.26/1.20 ((store @ (store @ a_1251 @ i5 @ (select @ a_1251 @ X0)) @ X0 @ e_1252)
% 4.26/1.20 = (store @ (store @ a_1251 @ X0 @ e_1252) @ i5 @
% 4.26/1.20 (select @ a_1251 @ X0)))),
% 4.26/1.20 inference('s_sup+', [status(thm)], [zip_derived_cl47, zip_derived_cl2])).
% 4.26/1.20 thf(zip_derived_cl1814, plain,
% 4.26/1.20 (((store @ (store @ a_1251 @ i5 @ e_1250) @ i8 @ e_1252)
% 4.26/1.20 = (store @ (store @ a_1251 @ i8 @ e_1252) @ i5 @ e_1250))),
% 4.26/1.20 inference('s_sup+', [status(thm)], [zip_derived_cl263, zip_derived_cl92])).
% 4.26/1.20 thf(hyp24, axiom, (( a_1290 ) = ( store @ a_1288 @ i5 @ e_1289 ))).
% 4.26/1.20 thf(zip_derived_cl27, plain, (((a_1290) = (store @ a_1288 @ i5 @ e_1289))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp24])).
% 4.26/1.20 thf(hyp61, axiom, (( e_1289 ) = ( select @ a_1288 @ i8 ))).
% 4.26/1.20 thf(zip_derived_cl64, plain, (((e_1289) = (select @ a_1288 @ i8))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp61])).
% 4.26/1.20 thf(hyp23, axiom, (( a_1288 ) = ( store @ a_1286 @ i8 @ e_1287 ))).
% 4.26/1.20 thf(zip_derived_cl26, plain, (((a_1288) = (store @ a_1286 @ i8 @ e_1287))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp23])).
% 4.26/1.20 thf(zip_derived_cl0, plain,
% 4.26/1.20 (![X0 : $i, X1 : $i, X2 : $i]:
% 4.26/1.20 ((select @ (store @ X1 @ X2 @ X0) @ X2) = (X0))),
% 4.26/1.20 inference('cnf', [status(esa)], [a1])).
% 4.26/1.20 thf(zip_derived_cl359, plain, (((select @ a_1288 @ i8) = (e_1287))),
% 4.26/1.20 inference('s_sup+', [status(thm)], [zip_derived_cl26, zip_derived_cl0])).
% 4.26/1.20 thf(zip_derived_cl395, plain, (((e_1289) = (e_1287))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl64, zip_derived_cl359])).
% 4.26/1.20 thf(zip_derived_cl400, plain, (((a_1290) = (store @ a_1288 @ i5 @ e_1287))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl27, zip_derived_cl395])).
% 4.26/1.20 thf(hyp60, axiom, (( e_1287 ) = ( select @ a_1284 @ i6 ))).
% 4.26/1.20 thf(zip_derived_cl63, plain, (((e_1287) = (select @ a_1284 @ i6))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp60])).
% 4.26/1.20 thf(hyp40, axiom, (( e_1244 ) = ( select @ a1 @ i7 ))).
% 4.26/1.20 thf(zip_derived_cl43, plain, (((e_1244) = (select @ a1 @ i7))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp40])).
% 4.26/1.20 thf(hyp41, axiom, (( e_1246 ) = ( select @ a1 @ i8 ))).
% 4.26/1.20 thf(zip_derived_cl44, plain, (((e_1246) = (select @ a1 @ i8))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp41])).
% 4.26/1.20 thf(zip_derived_cl2, plain,
% 4.26/1.20 (![X0 : $i, X1 : $i, X2 : $i]:
% 4.26/1.20 ((store @ (store @ X0 @ X2 @ (select @ X0 @ X1)) @ X1 @
% 4.26/1.20 (select @ X0 @ X2))
% 4.26/1.20 = (store @ (store @ X0 @ X1 @ (select @ X0 @ X2)) @ X2 @
% 4.26/1.20 (select @ X0 @ X1)))),
% 4.26/1.20 inference('cnf', [status(esa)], [a3])).
% 4.26/1.20 thf(zip_derived_cl87, plain,
% 4.26/1.20 (![X0 : $i]:
% 4.26/1.20 ((store @ (store @ a1 @ i8 @ (select @ a1 @ X0)) @ X0 @ e_1246)
% 4.26/1.20 = (store @ (store @ a1 @ X0 @ e_1246) @ i8 @ (select @ a1 @ X0)))),
% 4.26/1.20 inference('s_sup+', [status(thm)], [zip_derived_cl44, zip_derived_cl2])).
% 4.26/1.20 thf(zip_derived_cl1658, plain,
% 4.26/1.20 (((store @ (store @ a1 @ i8 @ e_1244) @ i7 @ e_1246)
% 4.26/1.20 = (store @ (store @ a1 @ i7 @ e_1246) @ i8 @ e_1244))),
% 4.26/1.20 inference('s_sup+', [status(thm)], [zip_derived_cl43, zip_derived_cl87])).
% 4.26/1.20 thf(hyp0, axiom, (( a_1245 ) = ( store @ a1 @ i8 @ e_1244 ))).
% 4.26/1.20 thf(zip_derived_cl3, plain, (((a_1245) = (store @ a1 @ i8 @ e_1244))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp0])).
% 4.26/1.20 thf(hyp1, axiom, (( a_1247 ) = ( store @ a_1245 @ i7 @ e_1246 ))).
% 4.26/1.20 thf(zip_derived_cl4, plain, (((a_1247) = (store @ a_1245 @ i7 @ e_1246))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp1])).
% 4.26/1.20 thf(hyp20, axiom, (( a_1283 ) = ( store @ a1 @ i7 @ e_1246 ))).
% 4.26/1.20 thf(zip_derived_cl23, plain, (((a_1283) = (store @ a1 @ i7 @ e_1246))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp20])).
% 4.26/1.20 thf(hyp21, axiom, (( a_1284 ) = ( store @ a_1283 @ i8 @ e_1244 ))).
% 4.26/1.20 thf(zip_derived_cl24, plain, (((a_1284) = (store @ a_1283 @ i8 @ e_1244))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp21])).
% 4.26/1.20 thf(zip_derived_cl1659, plain, (((a_1247) = (a_1284))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl1658, zip_derived_cl3, zip_derived_cl4,
% 4.26/1.20 zip_derived_cl23, zip_derived_cl24])).
% 4.26/1.20 thf(hyp43, axiom, (( e_1250 ) = ( select @ a_1247 @ i6 ))).
% 4.26/1.20 thf(zip_derived_cl46, plain, (((e_1250) = (select @ a_1247 @ i6))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp43])).
% 4.26/1.20 thf(zip_derived_cl1661, plain, (((e_1287) = (e_1250))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl63, zip_derived_cl1659, zip_derived_cl46])).
% 4.26/1.20 thf(zip_derived_cl1668, plain, (((a_1290) = (store @ a_1288 @ i5 @ e_1250))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl400, zip_derived_cl1661])).
% 4.26/1.20 thf(zip_derived_cl26, plain, (((a_1288) = (store @ a_1286 @ i8 @ e_1287))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp23])).
% 4.26/1.20 thf(zip_derived_cl1661, plain, (((e_1287) = (e_1250))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl63, zip_derived_cl1659, zip_derived_cl46])).
% 4.26/1.20 thf(zip_derived_cl1665, plain, (((a_1288) = (store @ a_1286 @ i8 @ e_1250))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl26, zip_derived_cl1661])).
% 4.26/1.20 thf(hyp22, axiom, (( a_1286 ) = ( store @ a_1284 @ i6 @ e_1285 ))).
% 4.26/1.20 thf(zip_derived_cl25, plain, (((a_1286) = (store @ a_1284 @ i6 @ e_1285))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp22])).
% 4.26/1.20 thf(hyp59, axiom, (( e_1285 ) = ( select @ a_1284 @ i8 ))).
% 4.26/1.20 thf(zip_derived_cl62, plain, (((e_1285) = (select @ a_1284 @ i8))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp59])).
% 4.26/1.20 thf(zip_derived_cl24, plain, (((a_1284) = (store @ a_1283 @ i8 @ e_1244))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp21])).
% 4.26/1.20 thf(zip_derived_cl0, plain,
% 4.26/1.20 (![X0 : $i, X1 : $i, X2 : $i]:
% 4.26/1.20 ((select @ (store @ X1 @ X2 @ X0) @ X2) = (X0))),
% 4.26/1.20 inference('cnf', [status(esa)], [a1])).
% 4.26/1.20 thf(zip_derived_cl355, plain, (((select @ a_1284 @ i8) = (e_1244))),
% 4.26/1.20 inference('s_sup+', [status(thm)], [zip_derived_cl24, zip_derived_cl0])).
% 4.26/1.20 thf(zip_derived_cl377, plain, (((e_1285) = (e_1244))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl62, zip_derived_cl355])).
% 4.26/1.20 thf(zip_derived_cl384, plain, (((a_1286) = (store @ a_1284 @ i6 @ e_1244))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl25, zip_derived_cl377])).
% 4.26/1.20 thf(zip_derived_cl1659, plain, (((a_1247) = (a_1284))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl1658, zip_derived_cl3, zip_derived_cl4,
% 4.26/1.20 zip_derived_cl23, zip_derived_cl24])).
% 4.26/1.20 thf(zip_derived_cl1664, plain, (((a_1286) = (store @ a_1247 @ i6 @ e_1244))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl384, zip_derived_cl1659])).
% 4.26/1.20 thf(hyp2, axiom, (( a_1249 ) = ( store @ a_1247 @ i6 @ e_1248 ))).
% 4.26/1.20 thf(zip_derived_cl5, plain, (((a_1249) = (store @ a_1247 @ i6 @ e_1248))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp2])).
% 4.26/1.20 thf(zip_derived_cl355, plain, (((select @ a_1284 @ i8) = (e_1244))),
% 4.26/1.20 inference('s_sup+', [status(thm)], [zip_derived_cl24, zip_derived_cl0])).
% 4.26/1.20 thf(zip_derived_cl1659, plain, (((a_1247) = (a_1284))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl1658, zip_derived_cl3, zip_derived_cl4,
% 4.26/1.20 zip_derived_cl23, zip_derived_cl24])).
% 4.26/1.20 thf(hyp42, axiom, (( e_1248 ) = ( select @ a_1247 @ i8 ))).
% 4.26/1.20 thf(zip_derived_cl45, plain, (((e_1248) = (select @ a_1247 @ i8))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp42])).
% 4.26/1.20 thf(zip_derived_cl1662, plain, (((e_1248) = (e_1244))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl355, zip_derived_cl1659, zip_derived_cl45])).
% 4.26/1.20 thf(zip_derived_cl1671, plain, (((a_1249) = (store @ a_1247 @ i6 @ e_1244))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl5, zip_derived_cl1662])).
% 4.26/1.20 thf(zip_derived_cl1758, plain, (((a_1286) = (a_1249))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl1664, zip_derived_cl1671])).
% 4.26/1.20 thf(zip_derived_cl6, plain, (((a_1251) = (store @ a_1249 @ i8 @ e_1250))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp3])).
% 4.26/1.20 thf(zip_derived_cl1779, plain, (((a_1288) = (a_1251))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl1665, zip_derived_cl1758, zip_derived_cl6])).
% 4.26/1.20 thf(zip_derived_cl1782, plain, (((a_1290) = (store @ a_1251 @ i5 @ e_1250))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl1668, zip_derived_cl1779])).
% 4.26/1.20 thf(hyp25, axiom, (( a_1292 ) = ( store @ a_1290 @ i8 @ e_1291 ))).
% 4.26/1.20 thf(zip_derived_cl28, plain, (((a_1292) = (store @ a_1290 @ i8 @ e_1291))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp25])).
% 4.26/1.20 thf(hyp62, axiom, (( e_1291 ) = ( select @ a_1288 @ i5 ))).
% 4.26/1.20 thf(zip_derived_cl65, plain, (((e_1291) = (select @ a_1288 @ i5))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp62])).
% 4.26/1.20 thf(zip_derived_cl1779, plain, (((a_1288) = (a_1251))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl1665, zip_derived_cl1758, zip_derived_cl6])).
% 4.26/1.20 thf(zip_derived_cl47, plain, (((e_1252) = (select @ a_1251 @ i5))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp44])).
% 4.26/1.20 thf(zip_derived_cl1780, plain, (((e_1291) = (e_1252))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl65, zip_derived_cl1779, zip_derived_cl47])).
% 4.26/1.20 thf(zip_derived_cl1783, plain, (((a_1292) = (store @ a_1290 @ i8 @ e_1252))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl28, zip_derived_cl1780])).
% 4.26/1.20 thf(hyp4, axiom, (( a_1253 ) = ( store @ a_1251 @ i8 @ e_1252 ))).
% 4.26/1.20 thf(zip_derived_cl7, plain, (((a_1253) = (store @ a_1251 @ i8 @ e_1252))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp4])).
% 4.26/1.20 thf(hyp5, axiom, (( a_1255 ) = ( store @ a_1253 @ i5 @ e_1254 ))).
% 4.26/1.20 thf(zip_derived_cl8, plain, (((a_1255) = (store @ a_1253 @ i5 @ e_1254))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp5])).
% 4.26/1.20 thf(hyp45, axiom, (( e_1254 ) = ( select @ a_1251 @ i8 ))).
% 4.26/1.20 thf(zip_derived_cl48, plain, (((e_1254) = (select @ a_1251 @ i8))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp45])).
% 4.26/1.20 thf(zip_derived_cl263, plain, (((select @ a_1251 @ i8) = (e_1250))),
% 4.26/1.20 inference('s_sup+', [status(thm)], [zip_derived_cl6, zip_derived_cl0])).
% 4.26/1.20 thf(zip_derived_cl275, plain, (((e_1254) = (e_1250))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl48, zip_derived_cl263])).
% 4.26/1.20 thf(zip_derived_cl280, plain, (((a_1255) = (store @ a_1253 @ i5 @ e_1250))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl8, zip_derived_cl275])).
% 4.26/1.20 thf(zip_derived_cl1816, plain, (((a_1292) = (a_1255))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl1814, zip_derived_cl1782, zip_derived_cl1783,
% 4.26/1.20 zip_derived_cl7, zip_derived_cl280])).
% 4.26/1.20 thf(hyp47, axiom, (( e_1258 ) = ( select @ a_1255 @ i4 ))).
% 4.26/1.20 thf(zip_derived_cl50, plain, (((e_1258) = (select @ a_1255 @ i4))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp47])).
% 4.26/1.20 thf(zip_derived_cl1819, plain, (((e_1295) = (e_1258))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl67, zip_derived_cl1816, zip_derived_cl50])).
% 4.26/1.20 thf(zip_derived_cl1826, plain, (((a_1296) = (store @ a_1294 @ i9 @ e_1258))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl30, zip_derived_cl1819])).
% 4.26/1.20 thf(hyp26, axiom, (( a_1294 ) = ( store @ a_1292 @ i4 @ e_1293 ))).
% 4.26/1.20 thf(zip_derived_cl29, plain, (((a_1294) = (store @ a_1292 @ i4 @ e_1293))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp26])).
% 4.26/1.20 thf(zip_derived_cl1816, plain, (((a_1292) = (a_1255))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl1814, zip_derived_cl1782, zip_derived_cl1783,
% 4.26/1.20 zip_derived_cl7, zip_derived_cl280])).
% 4.26/1.20 thf(zip_derived_cl1817, plain, (((a_1294) = (store @ a_1255 @ i4 @ e_1293))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl29, zip_derived_cl1816])).
% 4.26/1.20 thf(hyp63, axiom, (( e_1293 ) = ( select @ a_1292 @ i9 ))).
% 4.26/1.20 thf(zip_derived_cl66, plain, (((e_1293) = (select @ a_1292 @ i9))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp63])).
% 4.26/1.20 thf(zip_derived_cl1816, plain, (((a_1292) = (a_1255))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl1814, zip_derived_cl1782, zip_derived_cl1783,
% 4.26/1.20 zip_derived_cl7, zip_derived_cl280])).
% 4.26/1.20 thf(hyp46, axiom, (( e_1256 ) = ( select @ a_1255 @ i9 ))).
% 4.26/1.20 thf(zip_derived_cl49, plain, (((e_1256) = (select @ a_1255 @ i9))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp46])).
% 4.26/1.20 thf(zip_derived_cl1818, plain, (((e_1293) = (e_1256))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl66, zip_derived_cl1816, zip_derived_cl49])).
% 4.26/1.20 thf(hyp6, axiom, (( a_1257 ) = ( store @ a_1255 @ i4 @ e_1256 ))).
% 4.26/1.20 thf(zip_derived_cl9, plain, (((a_1257) = (store @ a_1255 @ i4 @ e_1256))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp6])).
% 4.26/1.20 thf(zip_derived_cl1857, plain, (((a_1294) = (a_1257))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl1817, zip_derived_cl1818, zip_derived_cl9])).
% 4.26/1.20 thf(hyp7, axiom, (( a_1259 ) = ( store @ a_1257 @ i9 @ e_1258 ))).
% 4.26/1.20 thf(zip_derived_cl10, plain, (((a_1259) = (store @ a_1257 @ i9 @ e_1258))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp7])).
% 4.26/1.20 thf(zip_derived_cl1879, plain, (((a_1296) = (a_1259))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl1826, zip_derived_cl1857, zip_derived_cl10])).
% 4.26/1.20 thf(zip_derived_cl1880, plain, (((a_1298) = (store @ a_1259 @ i1 @ e_1297))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl31, zip_derived_cl1879])).
% 4.26/1.20 thf(hyp65, axiom, (( e_1297 ) = ( select @ a_1296 @ i7 ))).
% 4.26/1.20 thf(zip_derived_cl68, plain, (((e_1297) = (select @ a_1296 @ i7))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp65])).
% 4.26/1.20 thf(zip_derived_cl1879, plain, (((a_1296) = (a_1259))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl1826, zip_derived_cl1857, zip_derived_cl10])).
% 4.26/1.20 thf(zip_derived_cl52, plain, (((e_1262) = (select @ a_1259 @ i7))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp49])).
% 4.26/1.20 thf(zip_derived_cl1881, plain, (((e_1297) = (e_1262))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl68, zip_derived_cl1879, zip_derived_cl52])).
% 4.26/1.20 thf(zip_derived_cl1907, plain, (((a_1298) = (store @ a_1259 @ i1 @ e_1262))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl1880, zip_derived_cl1881])).
% 4.26/1.20 thf(hyp29, axiom, (( a_1300 ) = ( store @ a_1298 @ i7 @ e_1299 ))).
% 4.26/1.20 thf(zip_derived_cl32, plain, (((a_1300) = (store @ a_1298 @ i7 @ e_1299))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp29])).
% 4.26/1.20 thf(hyp66, axiom, (( e_1299 ) = ( select @ a_1296 @ i1 ))).
% 4.26/1.20 thf(zip_derived_cl69, plain, (((e_1299) = (select @ a_1296 @ i1))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp66])).
% 4.26/1.20 thf(zip_derived_cl1879, plain, (((a_1296) = (a_1259))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl1826, zip_derived_cl1857, zip_derived_cl10])).
% 4.26/1.20 thf(zip_derived_cl51, plain, (((e_1260) = (select @ a_1259 @ i1))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp48])).
% 4.26/1.20 thf(zip_derived_cl1882, plain, (((e_1299) = (e_1260))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl69, zip_derived_cl1879, zip_derived_cl51])).
% 4.26/1.20 thf(zip_derived_cl1886, plain, (((a_1300) = (store @ a_1298 @ i7 @ e_1260))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl32, zip_derived_cl1882])).
% 4.26/1.20 thf(zip_derived_cl2004, plain, (((a_1263) = (a_1300))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl2003, zip_derived_cl11, zip_derived_cl12,
% 4.26/1.20 zip_derived_cl1907, zip_derived_cl1886])).
% 4.26/1.20 thf(hyp51, axiom, (( e_1266 ) = ( select @ a_1263 @ i4 ))).
% 4.26/1.20 thf(zip_derived_cl54, plain, (((e_1266) = (select @ a_1263 @ i4))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp51])).
% 4.26/1.20 thf(zip_derived_cl2007, plain, (((e_1303) = (e_1266))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl71, zip_derived_cl2004, zip_derived_cl54])).
% 4.26/1.20 thf(zip_derived_cl2014, plain, (((a_1304) = (store @ a_1302 @ i5 @ e_1266))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl34, zip_derived_cl2007])).
% 4.26/1.20 thf(hyp30, axiom, (( a_1302 ) = ( store @ a_1300 @ i4 @ e_1301 ))).
% 4.26/1.20 thf(zip_derived_cl33, plain, (((a_1302) = (store @ a_1300 @ i4 @ e_1301))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp30])).
% 4.26/1.20 thf(zip_derived_cl2004, plain, (((a_1263) = (a_1300))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl2003, zip_derived_cl11, zip_derived_cl12,
% 4.26/1.20 zip_derived_cl1907, zip_derived_cl1886])).
% 4.26/1.20 thf(zip_derived_cl2005, plain, (((a_1302) = (store @ a_1263 @ i4 @ e_1301))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl33, zip_derived_cl2004])).
% 4.26/1.20 thf(hyp67, axiom, (( e_1301 ) = ( select @ a_1300 @ i5 ))).
% 4.26/1.20 thf(zip_derived_cl70, plain, (((e_1301) = (select @ a_1300 @ i5))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp67])).
% 4.26/1.20 thf(zip_derived_cl2004, plain, (((a_1263) = (a_1300))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl2003, zip_derived_cl11, zip_derived_cl12,
% 4.26/1.20 zip_derived_cl1907, zip_derived_cl1886])).
% 4.26/1.20 thf(hyp50, axiom, (( e_1264 ) = ( select @ a_1263 @ i5 ))).
% 4.26/1.20 thf(zip_derived_cl53, plain, (((e_1264) = (select @ a_1263 @ i5))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp50])).
% 4.26/1.20 thf(zip_derived_cl2006, plain, (((e_1301) = (e_1264))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl70, zip_derived_cl2004, zip_derived_cl53])).
% 4.26/1.20 thf(hyp10, axiom, (( a_1265 ) = ( store @ a_1263 @ i4 @ e_1264 ))).
% 4.26/1.20 thf(zip_derived_cl13, plain, (((a_1265) = (store @ a_1263 @ i4 @ e_1264))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp10])).
% 4.26/1.20 thf(zip_derived_cl2046, plain, (((a_1302) = (a_1265))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl2005, zip_derived_cl2006, zip_derived_cl13])).
% 4.26/1.20 thf(hyp11, axiom, (( a_1267 ) = ( store @ a_1265 @ i5 @ e_1266 ))).
% 4.26/1.20 thf(zip_derived_cl14, plain, (((a_1267) = (store @ a_1265 @ i5 @ e_1266))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp11])).
% 4.26/1.20 thf(zip_derived_cl2067, plain, (((a_1304) = (a_1267))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl2014, zip_derived_cl2046, zip_derived_cl14])).
% 4.26/1.20 thf(hyp52, axiom, (( e_1268 ) = ( select @ a_1267 @ i0 ))).
% 4.26/1.20 thf(zip_derived_cl55, plain, (((e_1268) = (select @ a_1267 @ i0))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp52])).
% 4.26/1.20 thf(zip_derived_cl2069, plain, (((e_1305) = (e_1268))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl72, zip_derived_cl2067, zip_derived_cl55])).
% 4.26/1.20 thf(zip_derived_cl2071, plain, (((a_1307) = (store @ a_1306 @ i0 @ e_1268))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl36, zip_derived_cl2069])).
% 4.26/1.20 thf(hyp32, axiom, (( a_1306 ) = ( store @ a_1304 @ i0 @ e_1305 ))).
% 4.26/1.20 thf(zip_derived_cl35, plain, (((a_1306) = (store @ a_1304 @ i0 @ e_1305))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp32])).
% 4.26/1.20 thf(zip_derived_cl2067, plain, (((a_1304) = (a_1267))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl2014, zip_derived_cl2046, zip_derived_cl14])).
% 4.26/1.20 thf(zip_derived_cl2068, plain, (((a_1306) = (store @ a_1267 @ i0 @ e_1305))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl35, zip_derived_cl2067])).
% 4.26/1.20 thf(zip_derived_cl2069, plain, (((e_1305) = (e_1268))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl72, zip_derived_cl2067, zip_derived_cl55])).
% 4.26/1.20 thf(hyp12, axiom, (( a_1269 ) = ( store @ a_1267 @ i0 @ e_1268 ))).
% 4.26/1.20 thf(zip_derived_cl15, plain, (((a_1269) = (store @ a_1267 @ i0 @ e_1268))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp12])).
% 4.26/1.20 thf(zip_derived_cl2092, plain, (((a_1306) = (a_1269))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl2068, zip_derived_cl2069, zip_derived_cl15])).
% 4.26/1.20 thf(hyp13, axiom, (( a_1270 ) = ( store @ a_1269 @ i0 @ e_1268 ))).
% 4.26/1.20 thf(zip_derived_cl16, plain, (((a_1270) = (store @ a_1269 @ i0 @ e_1268))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp13])).
% 4.26/1.20 thf(zip_derived_cl2094, plain, (((a_1307) = (a_1270))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl2071, zip_derived_cl2092, zip_derived_cl16])).
% 4.26/1.20 thf(zip_derived_cl2095, plain, (((a_1309) = (store @ a_1270 @ i2 @ e_1308))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl37, zip_derived_cl2094])).
% 4.26/1.20 thf(hyp70, axiom, (( e_1308 ) = ( select @ a_1307 @ i1 ))).
% 4.26/1.20 thf(zip_derived_cl73, plain, (((e_1308) = (select @ a_1307 @ i1))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp70])).
% 4.26/1.20 thf(zip_derived_cl2094, plain, (((a_1307) = (a_1270))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl2071, zip_derived_cl2092, zip_derived_cl16])).
% 4.26/1.20 thf(zip_derived_cl57, plain, (((e_1273) = (select @ a_1270 @ i1))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp54])).
% 4.26/1.20 thf(zip_derived_cl2096, plain, (((e_1308) = (e_1273))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl73, zip_derived_cl2094, zip_derived_cl57])).
% 4.26/1.20 thf(zip_derived_cl2132, plain, (((a_1309) = (store @ a_1270 @ i2 @ e_1273))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl2095, zip_derived_cl2096])).
% 4.26/1.20 thf(hyp35, axiom, (( a_1311 ) = ( store @ a_1309 @ i1 @ e_1310 ))).
% 4.26/1.20 thf(zip_derived_cl38, plain, (((a_1311) = (store @ a_1309 @ i1 @ e_1310))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp35])).
% 4.26/1.20 thf(hyp71, axiom, (( e_1310 ) = ( select @ a_1307 @ i2 ))).
% 4.26/1.20 thf(zip_derived_cl74, plain, (((e_1310) = (select @ a_1307 @ i2))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp71])).
% 4.26/1.20 thf(zip_derived_cl2094, plain, (((a_1307) = (a_1270))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl2071, zip_derived_cl2092, zip_derived_cl16])).
% 4.26/1.20 thf(zip_derived_cl56, plain, (((e_1271) = (select @ a_1270 @ i2))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp53])).
% 4.26/1.20 thf(zip_derived_cl2097, plain, (((e_1310) = (e_1271))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl74, zip_derived_cl2094, zip_derived_cl56])).
% 4.26/1.20 thf(zip_derived_cl2112, plain, (((a_1311) = (store @ a_1309 @ i1 @ e_1271))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl38, zip_derived_cl2097])).
% 4.26/1.20 thf(zip_derived_cl2364, plain, (((a_1274) = (a_1311))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl2363, zip_derived_cl17, zip_derived_cl18,
% 4.26/1.20 zip_derived_cl2132, zip_derived_cl2112])).
% 4.26/1.20 thf(hyp56, axiom, (( e_1277 ) = ( select @ a_1274 @ i3 ))).
% 4.26/1.20 thf(zip_derived_cl59, plain, (((e_1277) = (select @ a_1274 @ i3))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp56])).
% 4.26/1.20 thf(zip_derived_cl2367, plain, (((e_1314) = (e_1277))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl76, zip_derived_cl2364, zip_derived_cl59])).
% 4.26/1.20 thf(zip_derived_cl2372, plain, (((a_1315) = (store @ a_1313 @ i0 @ e_1277))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl40, zip_derived_cl2367])).
% 4.26/1.20 thf(hyp36, axiom, (( a_1313 ) = ( store @ a_1311 @ i3 @ e_1312 ))).
% 4.26/1.20 thf(zip_derived_cl39, plain, (((a_1313) = (store @ a_1311 @ i3 @ e_1312))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp36])).
% 4.26/1.20 thf(zip_derived_cl2364, plain, (((a_1274) = (a_1311))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl2363, zip_derived_cl17, zip_derived_cl18,
% 4.26/1.20 zip_derived_cl2132, zip_derived_cl2112])).
% 4.26/1.20 thf(zip_derived_cl2365, plain, (((a_1313) = (store @ a_1274 @ i3 @ e_1312))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl39, zip_derived_cl2364])).
% 4.26/1.20 thf(hyp72, axiom, (( e_1312 ) = ( select @ a_1311 @ i0 ))).
% 4.26/1.20 thf(zip_derived_cl75, plain, (((e_1312) = (select @ a_1311 @ i0))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp72])).
% 4.26/1.20 thf(zip_derived_cl2364, plain, (((a_1274) = (a_1311))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl2363, zip_derived_cl17, zip_derived_cl18,
% 4.26/1.20 zip_derived_cl2132, zip_derived_cl2112])).
% 4.26/1.20 thf(hyp55, axiom, (( e_1275 ) = ( select @ a_1274 @ i0 ))).
% 4.26/1.20 thf(zip_derived_cl58, plain, (((e_1275) = (select @ a_1274 @ i0))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp55])).
% 4.26/1.20 thf(zip_derived_cl2366, plain, (((e_1312) = (e_1275))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl75, zip_derived_cl2364, zip_derived_cl58])).
% 4.26/1.20 thf(hyp16, axiom, (( a_1276 ) = ( store @ a_1274 @ i3 @ e_1275 ))).
% 4.26/1.20 thf(zip_derived_cl19, plain, (((a_1276) = (store @ a_1274 @ i3 @ e_1275))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp16])).
% 4.26/1.20 thf(zip_derived_cl2403, plain, (((a_1313) = (a_1276))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl2365, zip_derived_cl2366, zip_derived_cl19])).
% 4.26/1.20 thf(hyp17, axiom, (( a_1278 ) = ( store @ a_1276 @ i0 @ e_1277 ))).
% 4.26/1.20 thf(zip_derived_cl20, plain, (((a_1278) = (store @ a_1276 @ i0 @ e_1277))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp17])).
% 4.26/1.20 thf(zip_derived_cl2425, plain, (((a_1315) = (a_1278))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl2372, zip_derived_cl2403, zip_derived_cl20])).
% 4.26/1.20 thf(zip_derived_cl2426, plain, (((a_1317) = (store @ a_1278 @ i5 @ e_1316))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl41, zip_derived_cl2425])).
% 4.26/1.20 thf(hyp74, axiom, (( e_1316 ) = ( select @ a_1315 @ i9 ))).
% 4.26/1.20 thf(zip_derived_cl77, plain, (((e_1316) = (select @ a_1315 @ i9))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp74])).
% 4.26/1.20 thf(zip_derived_cl2425, plain, (((a_1315) = (a_1278))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl2372, zip_derived_cl2403, zip_derived_cl20])).
% 4.26/1.20 thf(zip_derived_cl61, plain, (((e_1281) = (select @ a_1278 @ i9))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp58])).
% 4.26/1.20 thf(zip_derived_cl2427, plain, (((e_1316) = (e_1281))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl77, zip_derived_cl2425, zip_derived_cl61])).
% 4.26/1.20 thf(zip_derived_cl2459, plain, (((a_1317) = (store @ a_1278 @ i5 @ e_1281))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl2426, zip_derived_cl2427])).
% 4.26/1.20 thf(hyp39, axiom, (( a_1319 ) = ( store @ a_1317 @ i9 @ e_1318 ))).
% 4.26/1.20 thf(zip_derived_cl42, plain, (((a_1319) = (store @ a_1317 @ i9 @ e_1318))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp39])).
% 4.26/1.20 thf(hyp75, axiom, (( e_1318 ) = ( select @ a_1315 @ i5 ))).
% 4.26/1.20 thf(zip_derived_cl78, plain, (((e_1318) = (select @ a_1315 @ i5))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp75])).
% 4.26/1.20 thf(zip_derived_cl2425, plain, (((a_1315) = (a_1278))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl2372, zip_derived_cl2403, zip_derived_cl20])).
% 4.26/1.20 thf(zip_derived_cl60, plain, (((e_1279) = (select @ a_1278 @ i5))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp57])).
% 4.26/1.20 thf(zip_derived_cl2428, plain, (((e_1318) = (e_1279))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl78, zip_derived_cl2425, zip_derived_cl60])).
% 4.26/1.20 thf(zip_derived_cl2432, plain, (((a_1319) = (store @ a_1317 @ i9 @ e_1279))),
% 4.26/1.20 inference('demod', [status(thm)], [zip_derived_cl42, zip_derived_cl2428])).
% 4.26/1.20 thf(hyp18, axiom, (( a_1280 ) = ( store @ a_1278 @ i9 @ e_1279 ))).
% 4.26/1.20 thf(zip_derived_cl21, plain, (((a_1280) = (store @ a_1278 @ i9 @ e_1279))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp18])).
% 4.26/1.20 thf(hyp19, axiom, (( a_1282 ) = ( store @ a_1280 @ i5 @ e_1281 ))).
% 4.26/1.20 thf(zip_derived_cl22, plain, (((a_1282) = (store @ a_1280 @ i5 @ e_1281))),
% 4.26/1.20 inference('cnf', [status(esa)], [hyp19])).
% 4.26/1.20 thf(zip_derived_cl2609, plain, (((a_1319) = (a_1282))),
% 4.26/1.20 inference('demod', [status(thm)],
% 4.26/1.20 [zip_derived_cl2607, zip_derived_cl2459, zip_derived_cl2432,
% 4.26/1.20 zip_derived_cl21, zip_derived_cl22])).
% 4.26/1.20 thf(goal, conjecture, (( a_1282 ) = ( a_1319 ))).
% 4.26/1.20 thf(zf_stmt_0, negated_conjecture, (( a_1282 ) != ( a_1319 )),
% 4.26/1.20 inference('cnf.neg', [status(esa)], [goal])).
% 4.26/1.20 thf(zip_derived_cl79, plain, (((a_1282) != (a_1319))),
% 4.26/1.20 inference('cnf', [status(esa)], [zf_stmt_0])).
% 4.26/1.20 thf(zip_derived_cl2610, plain, ($false),
% 4.26/1.20 inference('simplify_reflect-', [status(thm)],
% 4.26/1.20 [zip_derived_cl2609, zip_derived_cl79])).
% 4.26/1.20
% 4.26/1.20 % SZS output end Refutation
% 4.26/1.20
% 4.26/1.20
% 4.26/1.20 % Terminating...
% 4.61/1.26 % Runner terminated.
% 4.61/1.27 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------