%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM444+6 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n013.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 : Fri May 19 11:44:39 EDT 2023
% Result : Theorem 21.90s 22.09s
% Output : Proof 21.90s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM444+6 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n013.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 18 17:33:35 EDT 2023
% 0.12/0.33 % CPUTime :
% 21.90/22.09
% 21.90/22.09 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 21.90/22.09 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.90/22.09 %-----------------------------------------------------
% 21.90/22.09 ncf(matrix, plain, [(1103 ^ _192020) ^ [_227184, _227186] : [aInteger0(_227186), aInteger0(_227184), 1163 ^ _192020 : [(1164 ^ _192020) ^ [] : [-(aSet0(szAzrzSzezqlpdtcmdtrp0(xa, xq)))], (1199 ^ _192020) ^ [] : [aElementOf0(_227184, szAzrzSzezqlpdtcmdtrp0(xa, xq))], (1201 ^ _192020) ^ [] : [-(aElementOf0(_227184, stldt0(szAzrzSzezqlpdtcmdtrp0(xa, xq))))], (1166 ^ _192020) ^ [_229601] : [aElementOf0(_229601, szAzrzSzezqlpdtcmdtrp0(xa, xq)), 1169 ^ _192020 : [(1170 ^ _192020) ^ [] : [-(aInteger0(_229601))], (1173 ^ _192020) ^ [] : [-(aInteger0(1171 ^ [_227184, _227186, _229601]))], (1175 ^ _192020) ^ [] : [-(sdtasdt0(xq, 1171 ^ [_227184, _227186, _229601]) = sdtpldt0(_229601, smndt0(xa)))], (1177 ^ _192020) ^ [] : [-(aDivisorOf0(xq, sdtpldt0(_229601, smndt0(xa))))], (1179 ^ _192020) ^ [] : [-(sdteqdtlpzmzozddtrp0(_229601, xa, xq))]]], (1181 ^ _192020) ^ [_230179] : [-(aElementOf0(_230179, szAzrzSzezqlpdtcmdtrp0(xa, xq))), aInteger0(_230179), 1186 ^ _192020 : [(1193 ^ _192020) ^ [] : [aDivisorOf0(xq, sdtpldt0(_230179, smndt0(xa)))], (1195 ^ _192020) ^ [] : [sdteqdtlpzmzozddtrp0(_230179, xa, xq)], (1187 ^ _192020) ^ [_230405] : [aInteger0(_230405), sdtasdt0(xq, _230405) = sdtpldt0(_230179, smndt0(xa))]]]], 1153 ^ _192020 : [(1160 ^ _192020) ^ [] : [aDivisorOf0(xq, sdtpldt0(_227184, smndt0(_227186)))], (1162 ^ _192020) ^ [] : [sdteqdtlpzmzozddtrp0(_227184, _227186, xq)], (1154 ^ _192020) ^ [_229171] : [aInteger0(_229171), sdtasdt0(xq, _229171) = sdtpldt0(_227184, smndt0(_227186))]], 1114 ^ _192020 : [(1150 ^ _192020) ^ [] : [-(aElementOf0(_227186, szAzrzSzezqlpdtcmdtrp0(xa, xq)))], (1152 ^ _192020) ^ [] : [aElementOf0(_227186, stldt0(szAzrzSzezqlpdtcmdtrp0(xa, xq)))], (1115 ^ _192020) ^ [] : [-(aSet0(szAzrzSzezqlpdtcmdtrp0(xa, xq)))], (1117 ^ _192020) ^ [_227842] : [aElementOf0(_227842, szAzrzSzezqlpdtcmdtrp0(xa, xq)), 1120 ^ _192020 : [(1121 ^ _192020) ^ [] : [-(aInteger0(_227842))], (1124 ^ _192020) ^ [] : [-(aInteger0(1122 ^ [_227184, _227186, _227842]))], (1126 ^ _192020) ^ [] : [-(sdtasdt0(xq, 1122 ^ [_227184, _227186, _227842]) = sdtpldt0(_227842, smndt0(xa)))], (1128 ^ _192020) ^ [] : [-(aDivisorOf0(xq, sdtpldt0(_227842, smndt0(xa))))], (1130 ^ _192020) ^ [] : [-(sdteqdtlpzmzozddtrp0(_227842, xa, xq))]]], (1132 ^ _192020) ^ [_228420] : [-(aElementOf0(_228420, szAzrzSzezqlpdtcmdtrp0(xa, xq))), aInteger0(_228420), 1137 ^ _192020 : [(1144 ^ _192020) ^ [] : [aDivisorOf0(xq, sdtpldt0(_228420, smndt0(xa)))], (1146 ^ _192020) ^ [] : [sdteqdtlpzmzozddtrp0(_228420, xa, xq)], (1138 ^ _192020) ^ [_228646] : [aInteger0(_228646), sdtasdt0(xq, _228646) = sdtpldt0(_228420, smndt0(xa))]]]]], (1203 ^ _192020) ^ [] : [1204 ^ _192020 : [(1255 ^ _192020) ^ [] : [-(aElementOf0(1253 ^ [], szAzrzSzezqlpdtcmdtrp0(xa, xq)))], (1257 ^ _192020) ^ [] : [aElementOf0(1253 ^ [], cS1395)], (1259 ^ _192020) ^ [] : [aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa, xq), cS1395)], (1240 ^ _192020) ^ [] : [-(aSet0(cS1395))], (1242 ^ _192020) ^ [_232246] : [aElementOf0(_232246, cS1395), -(aInteger0(_232246))], (1248 ^ _192020) ^ [_232400] : [aInteger0(_232400), -(aElementOf0(_232400, cS1395))], (1205 ^ _192020) ^ [] : [-(aSet0(szAzrzSzezqlpdtcmdtrp0(xa, xq)))], (1207 ^ _192020) ^ [_231044] : [aElementOf0(_231044, szAzrzSzezqlpdtcmdtrp0(xa, xq)), 1210 ^ _192020 : [(1211 ^ _192020) ^ [] : [-(aInteger0(_231044))], (1214 ^ _192020) ^ [] : [-(aInteger0(1212 ^ [_231044]))], (1216 ^ _192020) ^ [] : [-(sdtasdt0(xq, 1212 ^ [_231044]) = sdtpldt0(_231044, smndt0(xa)))], (1218 ^ _192020) ^ [] : [-(aDivisorOf0(xq, sdtpldt0(_231044, smndt0(xa))))], (1220 ^ _192020) ^ [] : [-(sdteqdtlpzmzozddtrp0(_231044, xa, xq))]]], (1222 ^ _192020) ^ [_231574] : [-(aElementOf0(_231574, szAzrzSzezqlpdtcmdtrp0(xa, xq))), aInteger0(_231574), 1227 ^ _192020 : [(1234 ^ _192020) ^ [] : [aDivisorOf0(xq, sdtpldt0(_231574, smndt0(xa)))], (1236 ^ _192020) ^ [] : [sdteqdtlpzmzozddtrp0(_231574, xa, xq)], (1228 ^ _192020) ^ [_231784] : [aInteger0(_231784), sdtasdt0(xq, _231784) = sdtpldt0(_231574, smndt0(xa))]]]], 1260 ^ _192020 : [(1261 ^ _192020) ^ [_232816] : [aElementOf0(_232816, szAzrzSzezqlpdtcmdtrp0(xa, xq)), 1264 ^ _192020 : [(1265 ^ _192020) ^ [] : [-(aInteger0(_232816))], (1268 ^ _192020) ^ [] : [-(aInteger0(1266 ^ [_232816]))], (1270 ^ _192020) ^ [] : [-(sdtasdt0(xq, 1266 ^ [_232816]) = sdtpldt0(_232816, smndt0(xa)))], (1272 ^ _192020) ^ [] : [-(aDivisorOf0(xq, sdtpldt0(_232816, smndt0(xa))))], (1274 ^ _192020) ^ [] : [-(sdteqdtlpzmzozddtrp0(_232816, xa, xq))]]], (1276 ^ _192020) ^ [_233346] : [-(aElementOf0(_233346, szAzrzSzezqlpdtcmdtrp0(xa, xq))), aInteger0(_233346), 1281 ^ _192020 : [(1288 ^ _192020) ^ [] : [aDivisorOf0(xq, sdtpldt0(_233346, smndt0(xa)))], (1290 ^ _192020) ^ [] : [sdteqdtlpzmzozddtrp0(_233346, xa, xq)], (1282 ^ _192020) ^ [_233556] : [aInteger0(_233556), sdtasdt0(xq, _233556) = sdtpldt0(_233346, smndt0(xa))]]], (1369 ^ _192020) ^ [] : [isClosed0(szAzrzSzezqlpdtcmdtrp0(xa, xq))], (1294 ^ _192020) ^ [] : [-(aSet0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa, xq))))], (1296 ^ _192020) ^ [_234036] : [aElementOf0(_234036, stldt0(szAzrzSzezqlpdtcmdtrp0(xa, xq))), 1299 ^ _192020 : [(1300 ^ _192020) ^ [] : [-(aInteger0(_234036))], (1302 ^ _192020) ^ [] : [aElementOf0(_234036, szAzrzSzezqlpdtcmdtrp0(xa, xq))]]], (1304 ^ _192020) ^ [_234264] : [-(aElementOf0(_234264, stldt0(szAzrzSzezqlpdtcmdtrp0(xa, xq)))), aInteger0(_234264), -(aElementOf0(_234264, szAzrzSzezqlpdtcmdtrp0(xa, xq)))], (1367 ^ _192020) ^ [] : [isOpen0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa, xq)))], (1315 ^ _192020) ^ [] : [-(aElementOf0(1313 ^ [], stldt0(szAzrzSzezqlpdtcmdtrp0(xa, xq))))], (1317 ^ _192020) ^ [_234806] : [aInteger0(_234806), -(_234806 = sz00), 1324 ^ _192020 : [(1361 ^ _192020) ^ [] : [-(aElementOf0(1359 ^ [_234806], szAzrzSzezqlpdtcmdtrp0(1313 ^ [], _234806)))], (1363 ^ _192020) ^ [] : [aElementOf0(1359 ^ [_234806], stldt0(szAzrzSzezqlpdtcmdtrp0(xa, xq)))], (1365 ^ _192020) ^ [] : [aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(1313 ^ [], _234806), stldt0(szAzrzSzezqlpdtcmdtrp0(xa, xq)))], (1325 ^ _192020) ^ [] : [-(aSet0(szAzrzSzezqlpdtcmdtrp0(1313 ^ [], _234806)))], (1327 ^ _192020) ^ [_235256] : [aElementOf0(_235256, szAzrzSzezqlpdtcmdtrp0(1313 ^ [], _234806)), 1330 ^ _192020 : [(1331 ^ _192020) ^ [] : [-(aInteger0(_235256))], (1334 ^ _192020) ^ [] : [-(aInteger0(1332 ^ [_234806, _235256]))], (1336 ^ _192020) ^ [] : [-(sdtasdt0(_234806, 1332 ^ [_234806, _235256]) = sdtpldt0(_235256, smndt0(1313 ^ [])))], (1338 ^ _192020) ^ [] : [-(aDivisorOf0(_234806, sdtpldt0(_235256, smndt0(1313 ^ []))))], (1340 ^ _192020) ^ [] : [-(sdteqdtlpzmzozddtrp0(_235256, 1313 ^ [], _234806))]]], (1342 ^ _192020) ^ [_235816] : [-(aElementOf0(_235816, szAzrzSzezqlpdtcmdtrp0(1313 ^ [], _234806))), aInteger0(_235816), 1347 ^ _192020 : [(1354 ^ _192020) ^ [] : [aDivisorOf0(_234806, sdtpldt0(_235816, smndt0(1313 ^ [])))], (1356 ^ _192020) ^ [] : [sdteqdtlpzmzozddtrp0(_235816, 1313 ^ [], _234806)], (1348 ^ _192020) ^ [_236037] : [aInteger0(_236037), sdtasdt0(_234806, _236037) = sdtpldt0(_235816, smndt0(1313 ^ []))]]]]]]], (140 ^ _192020) ^ [_196531, _196533, _196535, _196537] : [-(sdtslmnbsdt0(_196537, _196533) = sdtslmnbsdt0(_196535, _196531)), _196537 = _196535, _196533 = _196531], (150 ^ _192020) ^ [_196890, _196892, _196894, _196896] : [-(sdtbsmnsldt0(_196896, _196892) = sdtbsmnsldt0(_196894, _196890)), _196896 = _196894, _196892 = _196890], (160 ^ _192020) ^ [_197221, _197223] : [_197223 = _197221, -(sbsmnsldt0(_197223) = sbsmnsldt0(_197221))], (166 ^ _192020) ^ [_197467, _197469, _197471, _197473] : [-(sdtasdt0(_197473, _197469) = sdtasdt0(_197471, _197467)), _197473 = _197471, _197469 = _197467], (176 ^ _192020) ^ [_197826, _197828, _197830, _197832] : [-(sdtpldt0(_197832, _197828) = sdtpldt0(_197830, _197826)), _197832 = _197830, _197828 = _197826], (186 ^ _192020) ^ [_198157, _198159] : [_198159 = _198157, -(smndt0(_198159) = smndt0(_198157))], (192 ^ _192020) ^ [_198375, _198377] : [_198377 = _198375, -(stldt0(_198377) = stldt0(_198375))], (198 ^ _192020) ^ [_198601, _198603, _198605, _198607] : [-(szAzrzSzezqlpdtcmdtrp0(_198607, _198603) = szAzrzSzezqlpdtcmdtrp0(_198605, _198601)), _198607 = _198605, _198603 = _198601], (2 ^ _192020) ^ [_192164] : [-(_192164 = _192164)], (4 ^ _192020) ^ [_192271, _192273] : [_192273 = _192271, -(_192271 = _192273)], (10 ^ _192020) ^ [_192475, _192477, _192479] : [-(_192479 = _192475), _192479 = _192477, _192477 = _192475], (20 ^ _192020) ^ [_192788, _192790] : [-(isPrime0(_192788)), _192790 = _192788, isPrime0(_192790)], (30 ^ _192020) ^ [_193083, _193085] : [-(isFinite0(_193083)), _193085 = _193083, isFinite0(_193085)], (40 ^ _192020) ^ [_193378, _193380] : [-(aSet0(_193378)), _193380 = _193378, aSet0(_193380)], (50 ^ _192020) ^ [_193673, _193675] : [-(aInteger0(_193673)), _193675 = _193673, aInteger0(_193675)], (60 ^ _192020) ^ [_193996, _193998, _194000, _194002] : [-(aDivisorOf0(_194000, _193996)), aDivisorOf0(_194002, _193998), _194002 = _194000, _193998 = _193996], (74 ^ _192020) ^ [_194468, _194470, _194472, _194474, _194476, _194478] : [-(sdteqdtlpzmzozddtrp0(_194476, _194472, _194468)), sdteqdtlpzmzozddtrp0(_194478, _194474, _194470), _194478 = _194476, _194474 = _194472, _194470 = _194468], (92 ^ _192020) ^ [_195049, _195051, _195053, _195055] : [-(aElementOf0(_195053, _195049)), aElementOf0(_195055, _195051), _195055 = _195053, _195051 = _195049], (106 ^ _192020) ^ [_195493, _195495, _195497, _195499] : [-(aSubsetOf0(_195497, _195493)), aSubsetOf0(_195499, _195495), _195499 = _195497, _195495 = _195493], (120 ^ _192020) ^ [_195909, _195911] : [-(isOpen0(_195909)), _195911 = _195909, isOpen0(_195911)], (130 ^ _192020) ^ [_196184, _196186] : [-(isClosed0(_196184)), _196186 = _196184, isClosed0(_196186)], (208 ^ _192020) ^ [_198980] : [aInteger0(_198980), true___, -(true___)], (218 ^ _192020) ^ [] : [-(aInteger0(sz00))], (220 ^ _192020) ^ [] : [-(aInteger0(sz10))], (222 ^ _192020) ^ [_199341] : [aInteger0(_199341), -(aInteger0(smndt0(_199341)))], (228 ^ _192020) ^ [_199545, _199547] : [-(aInteger0(sdtpldt0(_199547, _199545))), aInteger0(_199547), aInteger0(_199545)], (238 ^ _192020) ^ [_199844, _199846] : [-(aInteger0(sdtasdt0(_199846, _199844))), aInteger0(_199846), aInteger0(_199844)], (248 ^ _192020) ^ [_200157, _200159, _200161] : [-(sdtpldt0(_200161, sdtpldt0(_200159, _200157)) = sdtpldt0(sdtpldt0(_200161, _200159), _200157)), aInteger0(_200161), aInteger0(_200159), aInteger0(_200157)], (262 ^ _192020) ^ [_200577, _200579] : [-(sdtpldt0(_200579, _200577) = sdtpldt0(_200577, _200579)), aInteger0(_200579), aInteger0(_200577)], (272 ^ _192020) ^ [_200870] : [aInteger0(_200870), 275 ^ _192020 : [(276 ^ _192020) ^ [] : [-(sdtpldt0(_200870, sz00) = _200870)], (278 ^ _192020) ^ [] : [-(_200870 = sdtpldt0(sz00, _200870))]]], (280 ^ _192020) ^ [_201143] : [aInteger0(_201143), 283 ^ _192020 : [(284 ^ _192020) ^ [] : [-(sdtpldt0(_201143, smndt0(_201143)) = sz00)], (286 ^ _192020) ^ [] : [-(sz00 = sdtpldt0(smndt0(_201143), _201143))]]], (288 ^ _192020) ^ [_201452, _201454, _201456] : [-(sdtasdt0(_201456, sdtasdt0(_201454, _201452)) = sdtasdt0(sdtasdt0(_201456, _201454), _201452)), aInteger0(_201456), aInteger0(_201454), aInteger0(_201452)], (302 ^ _192020) ^ [_201872, _201874] : [-(sdtasdt0(_201874, _201872) = sdtasdt0(_201872, _201874)), aInteger0(_201874), aInteger0(_201872)], (312 ^ _192020) ^ [_202165] : [aInteger0(_202165), 315 ^ _192020 : [(316 ^ _192020) ^ [] : [-(sdtasdt0(_202165, sz10) = _202165)], (318 ^ _192020) ^ [] : [-(_202165 = sdtasdt0(sz10, _202165))]]], (320 ^ _192020) ^ [_202466, _202468, _202470] : [331 ^ _192020 : [(332 ^ _192020) ^ [] : [-(sdtasdt0(_202470, sdtpldt0(_202468, _202466)) = sdtpldt0(sdtasdt0(_202470, _202468), sdtasdt0(_202470, _202466)))], (334 ^ _192020) ^ [] : [-(sdtasdt0(sdtpldt0(_202470, _202468), _202466) = sdtpldt0(sdtasdt0(_202470, _202466), sdtasdt0(_202468, _202466)))]], aInteger0(_202470), aInteger0(_202468), aInteger0(_202466)], (336 ^ _192020) ^ [_202985] : [aInteger0(_202985), 339 ^ _192020 : [(340 ^ _192020) ^ [] : [-(sdtasdt0(_202985, sz00) = sz00)], (342 ^ _192020) ^ [] : [-(sz00 = sdtasdt0(sz00, _202985))]]], (344 ^ _192020) ^ [_203258] : [aInteger0(_203258), 347 ^ _192020 : [(348 ^ _192020) ^ [] : [-(sdtasdt0(smndt0(sz10), _203258) = smndt0(_203258))], (350 ^ _192020) ^ [] : [-(smndt0(_203258) = sdtasdt0(_203258, smndt0(sz10)))]]], (352 ^ _192020) ^ [_203553, _203555] : [aInteger0(_203555), aInteger0(_203553), sdtasdt0(_203555, _203553) = sz00, -(_203555 = sz00), -(_203553 = sz00)], (370 ^ _192020) ^ [_204021] : [aInteger0(_204021), 373 ^ _192020 : [(374 ^ _192020) ^ [_204207] : [aDivisorOf0(_204207, _204021), 377 ^ _192020 : [(378 ^ _192020) ^ [] : [-(aInteger0(_204207))], (380 ^ _192020) ^ [] : [_204207 = sz00], (383 ^ _192020) ^ [] : [-(aInteger0(381 ^ [_204021, _204207]))], (385 ^ _192020) ^ [] : [-(sdtasdt0(_204207, 381 ^ [_204021, _204207]) = _204021)]]], (387 ^ _192020) ^ [_204669] : [-(aDivisorOf0(_204669, _204021)), aInteger0(_204669), -(_204669 = sz00), 396 ^ _192020 : [(397 ^ _192020) ^ [_204936] : [aInteger0(_204936), sdtasdt0(_204669, _204936) = _204021]]]]], (405 ^ _192020) ^ [_205239, _205241, _205243] : [aInteger0(_205243), aInteger0(_205241), aInteger0(_205239), -(_205239 = sz00), 420 ^ _192020 : [(421 ^ _192020) ^ [] : [sdteqdtlpzmzozddtrp0(_205243, _205241, _205239), -(aDivisorOf0(_205239, sdtpldt0(_205243, smndt0(_205241))))], (427 ^ _192020) ^ [] : [aDivisorOf0(_205239, sdtpldt0(_205243, smndt0(_205241))), -(sdteqdtlpzmzozddtrp0(_205243, _205241, _205239))]]], (433 ^ _192020) ^ [_206015, _206017] : [-(sdteqdtlpzmzozddtrp0(_206017, _206017, _206015)), aInteger0(_206017), aInteger0(_206015), -(_206015 = sz00)], (447 ^ _192020) ^ [_206418, _206420, _206422] : [sdteqdtlpzmzozddtrp0(_206422, _206420, _206418), -(sdteqdtlpzmzozddtrp0(_206420, _206422, _206418)), aInteger0(_206422), aInteger0(_206420), aInteger0(_206418), -(_206418 = sz00)], (469 ^ _192020) ^ [_207037, _207039, _207041, _207043] : [-(sdteqdtlpzmzozddtrp0(_207043, _207037, _207039)), sdteqdtlpzmzozddtrp0(_207043, _207041, _207039), sdteqdtlpzmzozddtrp0(_207041, _207037, _207039), aInteger0(_207043), aInteger0(_207041), aInteger0(_207039), -(_207039 = sz00), aInteger0(_207037)], (499 ^ _192020) ^ [_207874, _207876, _207878, _207880] : [sdteqdtlpzmzozddtrp0(_207880, _207878, sdtasdt0(_207876, _207874)), 526 ^ _192020 : [(527 ^ _192020) ^ [] : [-(sdteqdtlpzmzozddtrp0(_207880, _207878, _207876))], (529 ^ _192020) ^ [] : [-(sdteqdtlpzmzozddtrp0(_207880, _207878, _207874))]], aInteger0(_207880), aInteger0(_207878), aInteger0(_207876), -(_207876 = sz00), aInteger0(_207874), -(_207874 = sz00)], (531 ^ _192020) ^ [_208755] : [aInteger0(_208755), -(_208755 = sz00), isPrime0(_208755), true___, -(true___)], (549 ^ _192020) ^ [_209186] : [aInteger0(_209186), 552 ^ _192020 : [(553 ^ _192020) ^ [] : [560 ^ _192020 : [(561 ^ _192020) ^ [] : [_209186 = sz10], (563 ^ _192020) ^ [] : [_209186 = smndt0(sz10)]], 554 ^ _192020 : [(555 ^ _192020) ^ [_209393] : [aDivisorOf0(_209393, _209186), isPrime0(_209393)]]], (565 ^ _192020) ^ [] : [573 ^ _192020 : [(574 ^ _192020) ^ [] : [-(aDivisorOf0(572 ^ [_209186], _209186))], (576 ^ _192020) ^ [] : [-(isPrime0(572 ^ [_209186]))]], -(_209186 = sz10), -(_209186 = smndt0(sz10))]]], (578 ^ _192020) ^ [_210035] : [aSet0(_210035), true___, -(true___)], (588 ^ _192020) ^ [_210290] : [aSet0(_210290), 591 ^ _192020 : [(592 ^ _192020) ^ [_210418] : [aElementOf0(_210418, _210290), true___, -(true___)]]], (602 ^ _192020) ^ [_210695] : [aSet0(_210695), 605 ^ _192020 : [(606 ^ _192020) ^ [_210871] : [aSubsetOf0(_210871, _210695), 609 ^ _192020 : [(610 ^ _192020) ^ [] : [-(aSet0(_210871))], (612 ^ _192020) ^ [_211080] : [aElementOf0(_211080, _210871), -(aElementOf0(_211080, _210695))]]], (618 ^ _192020) ^ [_211259] : [-(aSubsetOf0(_211259, _210695)), aSet0(_211259), 624 ^ _192020 : [(625 ^ _192020) ^ [] : [-(aElementOf0(623 ^ [_210695, _211259], _211259))], (627 ^ _192020) ^ [] : [aElementOf0(623 ^ [_210695, _211259], _210695)]]]]], (631 ^ _192020) ^ [_211696] : [aSet0(_211696), isFinite0(_211696), true___, -(true___)], (645 ^ _192020) ^ [_212051, _212053] : [aSubsetOf0(_212053, cS1395), aSubsetOf0(_212051, cS1395), 652 ^ _192020 : [(683 ^ _192020) ^ [_213316] : [-(_213316 = sdtbsmnsldt0(_212053, _212051)), aSet0(_213316), 691 ^ _192020 : [(692 ^ _192020) ^ [] : [-(aElementOf0(688 ^ [_212051, _212053, _213316], _213316))], (694 ^ _192020) ^ [] : [aInteger0(688 ^ [_212051, _212053, _213316]), 697 ^ _192020 : [(698 ^ _192020) ^ [] : [aElementOf0(688 ^ [_212051, _212053, _213316], _212053)], (700 ^ _192020) ^ [] : [aElementOf0(688 ^ [_212051, _212053, _213316], _212051)]]]], 701 ^ _192020 : [(710 ^ _192020) ^ [] : [aElementOf0(688 ^ [_212051, _212053, _213316], _213316)], (702 ^ _192020) ^ [] : [-(aInteger0(688 ^ [_212051, _212053, _213316]))], (704 ^ _192020) ^ [] : [-(aElementOf0(688 ^ [_212051, _212053, _213316], _212053)), -(aElementOf0(688 ^ [_212051, _212053, _213316], _212051))]]], (653 ^ _192020) ^ [_212336] : [_212336 = sdtbsmnsldt0(_212053, _212051), 656 ^ _192020 : [(657 ^ _192020) ^ [] : [-(aSet0(_212336))], (659 ^ _192020) ^ [_212599] : [aElementOf0(_212599, _212336), 662 ^ _192020 : [(663 ^ _192020) ^ [] : [-(aInteger0(_212599))], (665 ^ _192020) ^ [] : [-(aElementOf0(_212599, _212053)), -(aElementOf0(_212599, _212051))]]], (671 ^ _192020) ^ [_212954] : [-(aElementOf0(_212954, _212336)), aInteger0(_212954), 676 ^ _192020 : [(677 ^ _192020) ^ [] : [aElementOf0(_212954, _212053)], (679 ^ _192020) ^ [] : [aElementOf0(_212954, _212051)]]]]]]], (714 ^ _192020) ^ [_214353, _214355] : [aSubsetOf0(_214355, cS1395), aSubsetOf0(_214353, cS1395), 721 ^ _192020 : [(752 ^ _192020) ^ [_215617] : [-(_215617 = sdtslmnbsdt0(_214355, _214353)), aSet0(_215617), 772 ^ _192020 : [(773 ^ _192020) ^ [] : [-(aInteger0(757 ^ [_214353, _214355, _215617]))], (775 ^ _192020) ^ [] : [-(aElementOf0(757 ^ [_214353, _214355, _215617], _214355))], (777 ^ _192020) ^ [] : [-(aElementOf0(757 ^ [_214353, _214355, _215617], _214353))], (779 ^ _192020) ^ [] : [aElementOf0(757 ^ [_214353, _214355, _215617], _215617)]], 760 ^ _192020 : [(761 ^ _192020) ^ [] : [-(aElementOf0(757 ^ [_214353, _214355, _215617], _215617))], (763 ^ _192020) ^ [] : [aInteger0(757 ^ [_214353, _214355, _215617]), aElementOf0(757 ^ [_214353, _214355, _215617], _214355), aElementOf0(757 ^ [_214353, _214355, _215617], _214353)]]], (722 ^ _192020) ^ [_214638] : [_214638 = sdtslmnbsdt0(_214355, _214353), 725 ^ _192020 : [(726 ^ _192020) ^ [] : [-(aSet0(_214638))], (728 ^ _192020) ^ [_214901] : [aElementOf0(_214901, _214638), 731 ^ _192020 : [(732 ^ _192020) ^ [] : [-(aInteger0(_214901))], (734 ^ _192020) ^ [] : [-(aElementOf0(_214901, _214355))], (736 ^ _192020) ^ [] : [-(aElementOf0(_214901, _214353))]]], (738 ^ _192020) ^ [_215236] : [-(aElementOf0(_215236, _214638)), aInteger0(_215236), aElementOf0(_215236, _214355), aElementOf0(_215236, _214353)]]]]], (783 ^ _192020) ^ [_216643] : [aSet0(_216643), 789 ^ _192020 : [(790 ^ _192020) ^ [] : [-(aElementOf0(788 ^ [_216643], _216643))], (792 ^ _192020) ^ [] : [aSubsetOf0(788 ^ [_216643], cS1395)]], 793 ^ _192020 : [(825 ^ _192020) ^ [_218146] : [-(_218146 = sbsmnsldt0(_216643)), aSet0(_218146), 845 ^ _192020 : [(846 ^ _192020) ^ [] : [-(aInteger0(830 ^ [_216643, _218146]))], (849 ^ _192020) ^ [] : [-(aElementOf0(847 ^ [_216643, _218146], _216643))], (851 ^ _192020) ^ [] : [-(aElementOf0(830 ^ [_216643, _218146], 847 ^ [_216643, _218146]))], (853 ^ _192020) ^ [] : [aElementOf0(830 ^ [_216643, _218146], _218146)]], 833 ^ _192020 : [(834 ^ _192020) ^ [] : [-(aElementOf0(830 ^ [_216643, _218146], _218146))], (836 ^ _192020) ^ [] : [aInteger0(830 ^ [_216643, _218146]), 839 ^ _192020 : [(840 ^ _192020) ^ [_218609] : [aElementOf0(_218609, _216643), aElementOf0(830 ^ [_216643, _218146], _218609)]]]]], (794 ^ _192020) ^ [_217057] : [_217057 = sbsmnsldt0(_216643), 797 ^ _192020 : [(798 ^ _192020) ^ [] : [-(aSet0(_217057))], (800 ^ _192020) ^ [_217315] : [aElementOf0(_217315, _217057), 803 ^ _192020 : [(804 ^ _192020) ^ [] : [-(aInteger0(_217315))], (807 ^ _192020) ^ [] : [-(aElementOf0(805 ^ [_216643, _217057, _217315], _216643))], (809 ^ _192020) ^ [] : [-(aElementOf0(_217315, 805 ^ [_216643, _217057, _217315]))]]], (811 ^ _192020) ^ [_217716] : [-(aElementOf0(_217716, _217057)), aInteger0(_217716), 816 ^ _192020 : [(817 ^ _192020) ^ [_217901] : [aElementOf0(_217901, _216643), aElementOf0(_217716, _217901)]]]]]]], (857 ^ _192020) ^ [_219251] : [aSubsetOf0(_219251, cS1395), 860 ^ _192020 : [(885 ^ _192020) ^ [_220210] : [-(_220210 = stldt0(_219251)), aSet0(_220210), 901 ^ _192020 : [(902 ^ _192020) ^ [] : [-(aInteger0(890 ^ [_219251, _220210]))], (904 ^ _192020) ^ [] : [aElementOf0(890 ^ [_219251, _220210], _219251)], (906 ^ _192020) ^ [] : [aElementOf0(890 ^ [_219251, _220210], _220210)]], 893 ^ _192020 : [(894 ^ _192020) ^ [] : [-(aElementOf0(890 ^ [_219251, _220210], _220210))], (896 ^ _192020) ^ [] : [aInteger0(890 ^ [_219251, _220210]), -(aElementOf0(890 ^ [_219251, _220210], _219251))]]], (861 ^ _192020) ^ [_219438] : [_219438 = stldt0(_219251), 864 ^ _192020 : [(865 ^ _192020) ^ [] : [-(aSet0(_219438))], (867 ^ _192020) ^ [_219687] : [aElementOf0(_219687, _219438), 870 ^ _192020 : [(871 ^ _192020) ^ [] : [-(aInteger0(_219687))], (873 ^ _192020) ^ [] : [aElementOf0(_219687, _219251)]]], (875 ^ _192020) ^ [_219935] : [-(aElementOf0(_219935, _219438)), aInteger0(_219935), -(aElementOf0(_219935, _219251))]]]]], (910 ^ _192020) ^ [_221019, _221021] : [aInteger0(_221021), aInteger0(_221019), -(_221019 = sz00), 921 ^ _192020 : [(946 ^ _192020) ^ [_222190] : [-(_222190 = szAzrzSzezqlpdtcmdtrp0(_221021, _221019)), aSet0(_222190), 962 ^ _192020 : [(963 ^ _192020) ^ [] : [-(aInteger0(951 ^ [_221019, _221021, _222190]))], (965 ^ _192020) ^ [] : [-(sdteqdtlpzmzozddtrp0(951 ^ [_221019, _221021, _222190], _221021, _221019))], (967 ^ _192020) ^ [] : [aElementOf0(951 ^ [_221019, _221021, _222190], _222190)]], 954 ^ _192020 : [(955 ^ _192020) ^ [] : [-(aElementOf0(951 ^ [_221019, _221021, _222190], _222190))], (957 ^ _192020) ^ [] : [aInteger0(951 ^ [_221019, _221021, _222190]), sdteqdtlpzmzozddtrp0(951 ^ [_221019, _221021, _222190], _221021, _221019)]]], (922 ^ _192020) ^ [_221387] : [_221387 = szAzrzSzezqlpdtcmdtrp0(_221021, _221019), 925 ^ _192020 : [(926 ^ _192020) ^ [] : [-(aSet0(_221387))], (928 ^ _192020) ^ [_221645] : [aElementOf0(_221645, _221387), 931 ^ _192020 : [(932 ^ _192020) ^ [] : [-(aInteger0(_221645))], (934 ^ _192020) ^ [] : [-(sdteqdtlpzmzozddtrp0(_221645, _221021, _221019))]]], (936 ^ _192020) ^ [_221904] : [-(aElementOf0(_221904, _221387)), aInteger0(_221904), sdteqdtlpzmzozddtrp0(_221904, _221021, _221019)]]]]], (971 ^ _192020) ^ [_223033] : [aSubsetOf0(_223033, cS1395), 974 ^ _192020 : [(975 ^ _192020) ^ [] : [isOpen0(_223033), 978 ^ _192020 : [(979 ^ _192020) ^ [_223295] : [aElementOf0(_223295, _223033), 983 ^ _192020 : [(984 ^ _192020) ^ [] : [-(aInteger0(982 ^ [_223033, _223295]))], (986 ^ _192020) ^ [] : [982 ^ [_223033, _223295] = sz00], (988 ^ _192020) ^ [] : [-(aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(_223295, 982 ^ [_223033, _223295]), _223033))]]]]], (990 ^ _192020) ^ [] : [-(isOpen0(_223033)), 992 ^ _192020 : [(993 ^ _192020) ^ [] : [-(aElementOf0(991 ^ [_223033], _223033))], (995 ^ _192020) ^ [_223888] : [aInteger0(_223888), -(_223888 = sz00), aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(991 ^ [_223033], _223888), _223033)]]]]], (1007 ^ _192020) ^ [_224248] : [aSubsetOf0(_224248, cS1395), 1010 ^ _192020 : [(1011 ^ _192020) ^ [] : [isClosed0(_224248), -(isOpen0(stldt0(_224248)))], (1017 ^ _192020) ^ [] : [isOpen0(stldt0(_224248)), -(isClosed0(_224248))]]], (1023 ^ _192020) ^ [_224678] : [-(isOpen0(sbsmnsldt0(_224678))), aSet0(_224678), 1029 ^ _192020 : [(1030 ^ _192020) ^ [] : [-(aElementOf0(1028 ^ [_224678], _224678))], (1032 ^ _192020) ^ [] : [aSubsetOf0(1028 ^ [_224678], cS1395), isOpen0(1028 ^ [_224678])]]], (1040 ^ _192020) ^ [_225195, _225197] : [-(isOpen0(sdtslmnbsdt0(_225197, _225195))), aSubsetOf0(_225197, cS1395), aSubsetOf0(_225195, cS1395), isOpen0(_225197), isOpen0(_225195)], (1058 ^ _192020) ^ [_225672, _225674] : [-(isClosed0(sdtbsmnsldt0(_225674, _225672))), aSubsetOf0(_225674, cS1395), aSubsetOf0(_225672, cS1395), isClosed0(_225674), isClosed0(_225672)], (1097 ^ _192020) ^ [] : [-(aInteger0(xa))], (1099 ^ _192020) ^ [] : [-(aInteger0(xq))], (1101 ^ _192020) ^ [] : [xq = sz00], (1076 ^ _192020) ^ [_226135] : [-(isClosed0(sbsmnsldt0(_226135))), aSet0(_226135), isFinite0(_226135), 1086 ^ _192020 : [(1087 ^ _192020) ^ [] : [-(aElementOf0(1085 ^ [_226135], _226135))], (1089 ^ _192020) ^ [] : [aSubsetOf0(1085 ^ [_226135], cS1395), isClosed0(1085 ^ [_226135])]]]], input).
% 21.90/22.09 ncf('1',plain,[xq = sz00],start(1101 ^ 0)).
% 21.90/22.09 ncf('1.1',plain,[-(xq = sz00), 1317 : aInteger0(xq), 1327 : aElementOf0(1359 ^ [xq], szAzrzSzezqlpdtcmdtrp0(1313 ^ [], xq)), 1334 : -(aInteger0(1332 ^ [xq, 1359 ^ [xq]])), 1255 : -(aElementOf0(1253 ^ [], szAzrzSzezqlpdtcmdtrp0(xa, xq)))],extension(1203 ^ 1,bind([[_234806, _235256], [xq, 1359 ^ [xq]]]))).
% 21.90/22.09 ncf('1.1.1',plain,[-(aInteger0(xq))],extension(1099 ^ 4)).
% 21.90/22.09 ncf('1.1.2',plain,[-(aElementOf0(1359 ^ [xq], szAzrzSzezqlpdtcmdtrp0(1313 ^ [], xq)))],extension(1361 ^ 6)).
% 21.90/22.09 ncf('1.1.3',plain,[aInteger0(1332 ^ [xq, 1359 ^ [xq]]), 1154 : sdtasdt0(xq, 1332 ^ [xq, 1359 ^ [xq]]) = sdtpldt0(1359 ^ [xq], smndt0(1313 ^ [])), 1154 : aInteger0(1313 ^ []), 1154 : aInteger0(1359 ^ [xq]), 1201 : -(aElementOf0(1359 ^ [xq], stldt0(szAzrzSzezqlpdtcmdtrp0(xa, xq)))), 1150 : -(aElementOf0(1313 ^ [], szAzrzSzezqlpdtcmdtrp0(xa, xq)))],extension(1103 ^ 8,bind([[_227184, _227186, _229171], [1359 ^ [xq], 1313 ^ [], 1332 ^ [xq, 1359 ^ [xq]]]]))).
% 21.90/22.09 ncf('1.1.3.1',plain,[-(sdtasdt0(xq, 1332 ^ [xq, 1359 ^ [xq]]) = sdtpldt0(1359 ^ [xq], smndt0(1313 ^ [])))],extension(1336 ^ 11)).
% 21.90/22.09 ncf('1.1.3.2',plain,[-(aInteger0(1313 ^ [])), aElementOf0(1313 ^ [], stldt0(szAzrzSzezqlpdtcmdtrp0(xa, xq)))],extension(1296 ^ 9,bind([[_234036], [1313 ^ []]]))).
% 21.90/22.09 ncf('1.1.3.2.1',plain,[-(aElementOf0(1313 ^ [], stldt0(szAzrzSzezqlpdtcmdtrp0(xa, xq))))],extension(1315 ^ 10)).
% 21.90/22.09 ncf('1.1.3.3',plain,[-(aInteger0(1359 ^ [xq]))],extension(1331 ^ 9)).
% 21.90/22.09 ncf('1.1.3.4',plain,[aElementOf0(1359 ^ [xq], stldt0(szAzrzSzezqlpdtcmdtrp0(xa, xq)))],extension(1363 ^ 11)).
% 21.90/22.09 ncf('1.1.3.5',plain,[aElementOf0(1313 ^ [], szAzrzSzezqlpdtcmdtrp0(xa, xq)), aElementOf0(1313 ^ [], stldt0(szAzrzSzezqlpdtcmdtrp0(xa, xq)))],extension(1296 ^ 11,bind([[_234036], [1313 ^ []]]))).
% 21.90/22.09 ncf('1.1.3.5.1',plain,[-(aElementOf0(1313 ^ [], stldt0(szAzrzSzezqlpdtcmdtrp0(xa, xq))))],extension(1315 ^ 12)).
% 21.90/22.09 ncf('1.1.4',plain,[aElementOf0(1253 ^ [], szAzrzSzezqlpdtcmdtrp0(xa, xq)), aInteger0(1253 ^ []), aInteger0(1253 ^ []), 1162 : sdteqdtlpzmzozddtrp0(1253 ^ [], 1253 ^ [], xq), 1117 : aElementOf0(1253 ^ [], szAzrzSzezqlpdtcmdtrp0(xa, xq)), 1121 : -(aInteger0(1253 ^ []))],extension(1103 ^ 4,bind([[_227184, _227186, _227842], [1253 ^ [], 1253 ^ [], 1253 ^ []]]))).
% 21.90/22.09 ncf('1.1.4.1',plain,[-(aInteger0(1253 ^ [])), aElementOf0(1253 ^ [], szAzrzSzezqlpdtcmdtrp0(xa, xq))],extension(1207 ^ 5,bind([[_231044], [1253 ^ []]]))).
% 21.90/22.09 ncf('1.1.4.1.1',plain,[-(aElementOf0(1253 ^ [], szAzrzSzezqlpdtcmdtrp0(xa, xq)))],reduction('1.1')).
% 21.90/22.09 ncf('1.1.4.2',plain,[-(aInteger0(1253 ^ []))],lemmata('[1, 1].x')).
% 21.90/22.09 ncf('1.1.4.3',plain,[-(sdteqdtlpzmzozddtrp0(1253 ^ [], 1253 ^ [], xq)), aInteger0(1253 ^ []), aInteger0(xq), -(xq = sz00)],extension(433 ^ 7,bind([[_206015, _206017], [xq, 1253 ^ []]]))).
% 21.90/22.09 ncf('1.1.4.3.1',plain,[-(aInteger0(1253 ^ []))],lemmata('[1, 1].x')).
% 21.90/22.09 ncf('1.1.4.3.2',plain,[-(aInteger0(xq))],extension(1099 ^ 8)).
% 21.90/22.09 ncf('1.1.4.3.3',plain,[xq = sz00],reduction('1')).
% 21.90/22.09 ncf('1.1.4.4',plain,[-(aElementOf0(1253 ^ [], szAzrzSzezqlpdtcmdtrp0(xa, xq)))],reduction('1.1')).
% 21.90/22.09 ncf('1.1.4.5',plain,[aInteger0(1253 ^ []), -(aElementOf0(1253 ^ [], cS1395))],extension(1248 ^ 9,bind([[_232400], [1253 ^ []]]))).
% 21.90/22.09 ncf('1.1.4.5.1',plain,[aElementOf0(1253 ^ [], cS1395)],extension(1257 ^ 10)).
% 21.90/22.09 %-----------------------------------------------------
% 21.90/22.09 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------