%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM534+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n016.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:55 EDT 2023
% Result : Theorem 3.41s 4.47s
% Output : Proof 3.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : NUM534+1 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.11/0.33 % Computer : n016.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Thu May 18 18:06:11 EDT 2023
% 0.11/0.33 % CPUTime :
% 3.41/4.47
% 3.41/4.47 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 3.41/4.47 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.41/4.47 %-----------------------------------------------------
% 3.41/4.47 ncf(matrix, plain, [(438 ^ _55354) ^ [] : [sdtpldt0(sdtmndt0(xS, xx), xx) = xS], (88 ^ _55354) ^ [_58214, _58216, _58218, _58220] : [-(sdtpldt0(_58220, _58216) = sdtpldt0(_58218, _58214)), _58220 = _58218, _58216 = _58214], (98 ^ _55354) ^ [_58553, _58555, _58557, _58559] : [-(sdtmndt0(_58559, _58555) = sdtmndt0(_58557, _58553)), _58559 = _58557, _58555 = _58553], (2 ^ _55354) ^ [_55498] : [-(_55498 = _55498)], (4 ^ _55354) ^ [_55605, _55607] : [_55607 = _55605, -(_55605 = _55607)], (10 ^ _55354) ^ [_55809, _55811, _55813] : [-(_55813 = _55809), _55813 = _55811, _55811 = _55809], (20 ^ _55354) ^ [_56122, _56124] : [-(isCountable0(_56122)), _56124 = _56122, isCountable0(_56124)], (30 ^ _55354) ^ [_56417, _56419] : [-(isFinite0(_56417)), _56419 = _56417, isFinite0(_56419)], (40 ^ _55354) ^ [_56740, _56742, _56744, _56746] : [-(aSubsetOf0(_56744, _56740)), aSubsetOf0(_56746, _56742), _56746 = _56744, _56742 = _56740], (54 ^ _55354) ^ [_57156, _57158] : [-(aElement0(_57156)), _57158 = _57156, aElement0(_57158)], (64 ^ _55354) ^ [_57451, _57453] : [-(aSet0(_57451)), _57453 = _57451, aSet0(_57453)], (74 ^ _55354) ^ [_57754, _57756, _57758, _57760] : [-(aElementOf0(_57758, _57754)), aElementOf0(_57760, _57756), _57760 = _57758, _57756 = _57754], (108 ^ _55354) ^ [_58876] : [aSet0(_58876), true___, -(true___)], (118 ^ _55354) ^ [_59131] : [aElement0(_59131), true___, -(true___)], (128 ^ _55354) ^ [_59386] : [aSet0(_59386), 131 ^ _55354 : [(132 ^ _55354) ^ [_59516] : [aElementOf0(_59516, _59386), -(aElement0(_59516))]]], (138 ^ _55354) ^ [_59717] : [aSet0(_59717), isFinite0(_59717), true___, -(true___)], (152 ^ _55354) ^ [_60087] : [_60087 = slcrc0, 155 ^ _55354 : [(156 ^ _55354) ^ [] : [-(aSet0(_60087))], (158 ^ _55354) ^ [_60268] : [aElementOf0(_60268, _60087)]]], (160 ^ _55354) ^ [_60336] : [-(_60336 = slcrc0), aSet0(_60336), -(aElementOf0(165 ^ [_60336], _60336))], (171 ^ _55354) ^ [] : [-(isFinite0(slcrc0))], (173 ^ _55354) ^ [_60718] : [aSet0(_60718), isCountable0(_60718), true___, -(true___)], (187 ^ _55354) ^ [_61059] : [isFinite0(_61059), aSet0(_61059), isCountable0(_61059)], (197 ^ _55354) ^ [_61329] : [_61329 = slcrc0, aSet0(_61329), isCountable0(_61329)], (207 ^ _55354) ^ [_61601] : [aSet0(_61601), 210 ^ _55354 : [(211 ^ _55354) ^ [_61777] : [aSubsetOf0(_61777, _61601), 214 ^ _55354 : [(215 ^ _55354) ^ [] : [-(aSet0(_61777))], (217 ^ _55354) ^ [_61986] : [aElementOf0(_61986, _61777), -(aElementOf0(_61986, _61601))]]], (223 ^ _55354) ^ [_62165] : [-(aSubsetOf0(_62165, _61601)), aSet0(_62165), 229 ^ _55354 : [(230 ^ _55354) ^ [] : [-(aElementOf0(228 ^ [_61601, _62165], _62165))], (232 ^ _55354) ^ [] : [aElementOf0(228 ^ [_61601, _62165], _61601)]]]]], (236 ^ _55354) ^ [_62602] : [aSet0(_62602), isFinite0(_62602), 243 ^ _55354 : [(244 ^ _55354) ^ [_62815] : [aSubsetOf0(_62815, _62602), -(isFinite0(_62815))]]], (250 ^ _55354) ^ [_63018] : [aSet0(_63018), -(aSubsetOf0(_63018, _63018))], (256 ^ _55354) ^ [_63220, _63222] : [aSet0(_63222), aSet0(_63220), -(_63222 = _63220), aSubsetOf0(_63222, _63220), aSubsetOf0(_63220, _63222)], (274 ^ _55354) ^ [_63709, _63711, _63713] : [aSet0(_63713), aSet0(_63711), aSet0(_63709), -(aSubsetOf0(_63713, _63709)), aSubsetOf0(_63713, _63711), aSubsetOf0(_63711, _63709)], (434 ^ _55354) ^ [] : [-(aSet0(xS))], (436 ^ _55354) ^ [] : [-(aElementOf0(xx, xS))], (365 ^ _55354) ^ [_66593, _66595] : [aSet0(_66595), aElement0(_66593), 372 ^ _55354 : [(403 ^ _55354) ^ [_67861] : [-(_67861 = sdtmndt0(_66595, _66593)), aSet0(_67861), 423 ^ _55354 : [(424 ^ _55354) ^ [] : [-(aElement0(408 ^ [_66593, _66595, _67861]))], (426 ^ _55354) ^ [] : [-(aElementOf0(408 ^ [_66593, _66595, _67861], _66595))], (428 ^ _55354) ^ [] : [408 ^ [_66593, _66595, _67861] = _66593], (430 ^ _55354) ^ [] : [aElementOf0(408 ^ [_66593, _66595, _67861], _67861)]], 411 ^ _55354 : [(412 ^ _55354) ^ [] : [-(aElementOf0(408 ^ [_66593, _66595, _67861], _67861))], (414 ^ _55354) ^ [] : [aElement0(408 ^ [_66593, _66595, _67861]), aElementOf0(408 ^ [_66593, _66595, _67861], _66595), -(408 ^ [_66593, _66595, _67861] = _66593)]]], (373 ^ _55354) ^ [_66876] : [_66876 = sdtmndt0(_66595, _66593), 376 ^ _55354 : [(377 ^ _55354) ^ [] : [-(aSet0(_66876))], (379 ^ _55354) ^ [_67141] : [aElementOf0(_67141, _66876), 382 ^ _55354 : [(383 ^ _55354) ^ [] : [-(aElement0(_67141))], (385 ^ _55354) ^ [] : [-(aElementOf0(_67141, _66595))], (387 ^ _55354) ^ [] : [_67141 = _66593]]], (389 ^ _55354) ^ [_67477] : [-(aElementOf0(_67477, _66876)), aElement0(_67477), aElementOf0(_67477, _66595), -(_67477 = _66593)]]]]], (296 ^ _55354) ^ [_64295, _64297] : [aSet0(_64297), aElement0(_64295), 303 ^ _55354 : [(334 ^ _55354) ^ [_65556] : [-(_65556 = sdtpldt0(_64297, _64295)), aSet0(_65556), 342 ^ _55354 : [(343 ^ _55354) ^ [] : [-(aElementOf0(339 ^ [_64295, _64297, _65556], _65556))], (345 ^ _55354) ^ [] : [aElement0(339 ^ [_64295, _64297, _65556]), 348 ^ _55354 : [(349 ^ _55354) ^ [] : [aElementOf0(339 ^ [_64295, _64297, _65556], _64297)], (351 ^ _55354) ^ [] : [339 ^ [_64295, _64297, _65556] = _64295]]]], 352 ^ _55354 : [(361 ^ _55354) ^ [] : [aElementOf0(339 ^ [_64295, _64297, _65556], _65556)], (353 ^ _55354) ^ [] : [-(aElement0(339 ^ [_64295, _64297, _65556]))], (355 ^ _55354) ^ [] : [-(aElementOf0(339 ^ [_64295, _64297, _65556], _64297)), -(339 ^ [_64295, _64297, _65556] = _64295)]]], (304 ^ _55354) ^ [_64576] : [_64576 = sdtpldt0(_64297, _64295), 307 ^ _55354 : [(308 ^ _55354) ^ [] : [-(aSet0(_64576))], (310 ^ _55354) ^ [_64839] : [aElementOf0(_64839, _64576), 313 ^ _55354 : [(314 ^ _55354) ^ [] : [-(aElement0(_64839))], (316 ^ _55354) ^ [] : [-(aElementOf0(_64839, _64297)), -(_64839 = _64295)]]], (322 ^ _55354) ^ [_65194] : [-(aElementOf0(_65194, _64576)), aElement0(_65194), 327 ^ _55354 : [(328 ^ _55354) ^ [] : [aElementOf0(_65194, _64297)], (330 ^ _55354) ^ [] : [_65194 = _64295]]]]]]]], input).
% 3.41/4.47 ncf('1',plain,[sdtpldt0(sdtmndt0(xS, xx), xx) = xS],start(438 ^ 0)).
% 3.41/4.47 ncf('1.1',plain,[-(sdtpldt0(sdtmndt0(xS, xx), xx) = xS), xS = sdtpldt0(sdtmndt0(xS, xx), xx)],extension(4 ^ 1,bind([[_55605, _55607], [sdtpldt0(sdtmndt0(xS, xx), xx), xS]]))).
% 3.41/4.47 ncf('1.1.1',plain,[-(xS = sdtpldt0(sdtmndt0(xS, xx), xx)), 334 : aSet0(xS), 343 : -(aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], xS)), 355 : -(aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], sdtmndt0(xS, xx))), 355 : -(339 ^ [xx, sdtmndt0(xS, xx), xS] = xx), 334 : aSet0(sdtmndt0(xS, xx)), 334 : aElement0(xx)],extension(296 ^ 2,bind([[_64295, _64297, _65556], [xx, sdtmndt0(xS, xx), xS]]))).
% 3.41/4.47 ncf('1.1.1.1',plain,[-(aSet0(xS))],extension(434 ^ 5)).
% 3.41/4.47 ncf('1.1.1.2',plain,[aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], xS), 132 : -(aElement0(339 ^ [xx, sdtmndt0(xS, xx), xS])), 132 : aSet0(xS)],extension(128 ^ 7,bind([[_59386, _59516], [xS, 339 ^ [xx, sdtmndt0(xS, xx), xS]]]))).
% 3.41/4.47 ncf('1.1.1.2.1',plain,[aElement0(339 ^ [xx, sdtmndt0(xS, xx), xS]), 389 : -(aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], sdtmndt0(xS, xx))), 389 : aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], xS), 389 : -(339 ^ [xx, sdtmndt0(xS, xx), xS] = xx), 389 : sdtmndt0(xS, xx) = sdtmndt0(xS, xx), 373 : aSet0(xS), 373 : aElement0(xx)],extension(365 ^ 10,bind([[_66593, _66595, _66876, _67477], [xx, xS, sdtmndt0(xS, xx), 339 ^ [xx, sdtmndt0(xS, xx), xS]]]))).
% 3.41/4.47 ncf('1.1.1.2.1.1',plain,[aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], sdtmndt0(xS, xx)), aElement0(339 ^ [xx, sdtmndt0(xS, xx), xS])],extension(345 ^ 15)).
% 3.41/4.47 ncf('1.1.1.2.1.1.1',plain,[-(aElement0(339 ^ [xx, sdtmndt0(xS, xx), xS]))],reduction('1.1.1.2')).
% 3.41/4.47 ncf('1.1.1.2.1.2',plain,[-(aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], xS))],reduction('1.1.1')).
% 3.41/4.47 ncf('1.1.1.2.1.3',plain,[339 ^ [xx, sdtmndt0(xS, xx), xS] = xx, aElement0(339 ^ [xx, sdtmndt0(xS, xx), xS])],extension(345 ^ 15)).
% 3.41/4.47 ncf('1.1.1.2.1.3.1',plain,[-(aElement0(339 ^ [xx, sdtmndt0(xS, xx), xS]))],reduction('1.1.1.2')).
% 3.41/4.47 ncf('1.1.1.2.1.4',plain,[-(sdtmndt0(xS, xx) = sdtmndt0(xS, xx))],extension(2 ^ 13,bind([[_55498], [sdtmndt0(xS, xx)]]))).
% 3.41/4.47 ncf('1.1.1.2.1.5',plain,[-(aSet0(xS))],lemmata('[1, 1].x')).
% 3.41/4.47 ncf('1.1.1.2.1.6',plain,[-(aElement0(xx)), aElementOf0(xx, xS)],extension(132 ^ 11,bind([[_59516], [xx]]))).
% 3.41/4.47 ncf('1.1.1.2.1.6.1',plain,[-(aElementOf0(xx, xS))],extension(436 ^ 12)).
% 3.41/4.47 ncf('1.1.1.2.2',plain,[-(aSet0(xS))],lemmata('[1, 1].x')).
% 3.41/4.47 ncf('1.1.1.3',plain,[aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], sdtmndt0(xS, xx)), 385 : -(aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], xS)), 379 : sdtmndt0(xS, xx) = sdtmndt0(xS, xx), 373 : aSet0(xS), 373 : aElement0(xx)],extension(365 ^ 7,bind([[_66593, _66595, _66876, _67141], [xx, xS, sdtmndt0(xS, xx), 339 ^ [xx, sdtmndt0(xS, xx), xS]]]))).
% 3.41/4.47 ncf('1.1.1.3.1',plain,[aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], xS), -(aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], xS)), 339 ^ [xx, sdtmndt0(xS, xx), xS] = 339 ^ [xx, sdtmndt0(xS, xx), xS], xS = xS],extension(74 ^ 14,bind([[_57754, _57756, _57758, _57760], [xS, xS, 339 ^ [xx, sdtmndt0(xS, xx), xS], 339 ^ [xx, sdtmndt0(xS, xx), xS]]]))).
% 3.41/4.47 ncf('1.1.1.3.1.1',plain,[aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], xS)],extension(361 ^ 15)).
% 3.41/4.47 ncf('1.1.1.3.1.2',plain,[-(339 ^ [xx, sdtmndt0(xS, xx), xS] = 339 ^ [xx, sdtmndt0(xS, xx), xS])],extension(2 ^ 15,bind([[_55498], [339 ^ [xx, sdtmndt0(xS, xx), xS]]]))).
% 3.41/4.47 ncf('1.1.1.3.1.3',plain,[-(xS = xS)],extension(2 ^ 15,bind([[_55498], [xS]]))).
% 3.41/4.47 ncf('1.1.1.3.2',plain,[-(sdtmndt0(xS, xx) = sdtmndt0(xS, xx)), xS = xS, xx = xx],extension(98 ^ 10,bind([[_58553, _58555, _58557, _58559], [xx, xx, xS, xS]]))).
% 3.41/4.47 ncf('1.1.1.3.2.1',plain,[-(xS = xS)],extension(2 ^ 11,bind([[_55498], [xS]]))).
% 3.41/4.47 ncf('1.1.1.3.2.2',plain,[-(xx = xx)],extension(2 ^ 11,bind([[_55498], [xx]]))).
% 3.41/4.47 ncf('1.1.1.3.3',plain,[-(aSet0(xS))],lemmata('[1, 1].x')).
% 3.41/4.47 ncf('1.1.1.3.4',plain,[-(aElement0(xx)), 132 : aElementOf0(xx, xS), 132 : aSet0(xS)],extension(128 ^ 8,bind([[_59386, _59516], [xS, xx]]))).
% 3.41/4.47 ncf('1.1.1.3.4.1',plain,[-(aElementOf0(xx, xS))],extension(436 ^ 11)).
% 3.41/4.47 ncf('1.1.1.3.4.2',plain,[-(aSet0(xS))],lemmata('[1, 1, 1].x')).
% 3.41/4.47 ncf('1.1.1.4',plain,[339 ^ [xx, sdtmndt0(xS, xx), xS] = xx, -(xx = 339 ^ [xx, sdtmndt0(xS, xx), xS])],extension(4 ^ 7,bind([[_55605, _55607], [xx, 339 ^ [xx, sdtmndt0(xS, xx), xS]]]))).
% 3.41/4.47 ncf('1.1.1.4.1',plain,[xx = 339 ^ [xx, sdtmndt0(xS, xx), xS], -(aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], xS)), aElementOf0(xx, xS), xS = xS],extension(74 ^ 8,bind([[_57754, _57756, _57758, _57760], [xS, xS, 339 ^ [xx, sdtmndt0(xS, xx), xS], xx]]))).
% 3.41/4.47 ncf('1.1.1.4.1.1',plain,[aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], xS)],extension(361 ^ 9)).
% 3.41/4.47 ncf('1.1.1.4.1.2',plain,[-(aElementOf0(xx, xS))],extension(436 ^ 9)).
% 3.41/4.47 ncf('1.1.1.4.1.3',plain,[-(xS = xS)],extension(2 ^ 9,bind([[_55498], [xS]]))).
% 3.41/4.47 ncf('1.1.1.5',plain,[-(aSet0(sdtmndt0(xS, xx))), 373 : sdtmndt0(xS, xx) = sdtmndt0(xS, xx), 373 : aSet0(xS), 373 : aElement0(xx)],extension(365 ^ 3,bind([[_66593, _66595, _66876], [xx, xS, sdtmndt0(xS, xx)]]))).
% 3.41/4.47 ncf('1.1.1.5.1',plain,[-(sdtmndt0(xS, xx) = sdtmndt0(xS, xx)), xS = xS, xx = xx],extension(98 ^ 6,bind([[_58553, _58555, _58557, _58559], [xx, xx, xS, xS]]))).
% 3.41/4.47 ncf('1.1.1.5.1.1',plain,[-(xS = xS)],extension(2 ^ 7,bind([[_55498], [xS]]))).
% 3.41/4.47 ncf('1.1.1.5.1.2',plain,[-(xx = xx)],extension(2 ^ 7,bind([[_55498], [xx]]))).
% 3.41/4.47 ncf('1.1.1.5.2',plain,[-(aSet0(xS))],extension(434 ^ 4)).
% 3.41/4.47 ncf('1.1.1.5.3',plain,[-(aElement0(xx)), 132 : aElementOf0(xx, xS), 132 : aSet0(xS)],extension(128 ^ 4,bind([[_59386, _59516], [xS, xx]]))).
% 3.41/4.47 ncf('1.1.1.5.3.1',plain,[-(aElementOf0(xx, xS))],extension(436 ^ 7)).
% 3.41/4.47 ncf('1.1.1.5.3.2',plain,[-(aSet0(xS))],lemmata('[1, 1, 1].x')).
% 3.41/4.47 ncf('1.1.1.6',plain,[-(aElement0(xx)), 132 : aElementOf0(xx, xS), 132 : aSet0(xS)],extension(128 ^ 3,bind([[_59386, _59516], [xS, xx]]))).
% 3.41/4.47 ncf('1.1.1.6.1',plain,[-(aElementOf0(xx, xS)), aElementOf0(xx, xS), xx = xx, xS = xS],extension(74 ^ 6,bind([[_57754, _57756, _57758, _57760], [xS, xS, xx, xx]]))).
% 3.41/4.47 ncf('1.1.1.6.1.1',plain,[-(aElementOf0(xx, xS))],extension(436 ^ 7)).
% 3.41/4.47 ncf('1.1.1.6.1.2',plain,[-(xx = xx)],extension(2 ^ 7,bind([[_55498], [xx]]))).
% 3.41/4.47 ncf('1.1.1.6.1.3',plain,[-(xS = xS)],extension(2 ^ 7,bind([[_55498], [xS]]))).
% 3.41/4.47 ncf('1.1.1.6.2',plain,[-(aSet0(xS))],extension(434 ^ 4)).
% 3.41/4.47 %-----------------------------------------------------
% 3.41/4.47 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------