%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM537+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n004.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 0.68s 1.37s
% Output : Proof 0.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NUM537+1 : TPTP v8.1.2. Released v4.0.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n004.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 16:51:54 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.68/1.37
% 0.68/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.68/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.68/1.37 %-----------------------------------------------------
% 0.68/1.37 ncf(matrix, plain, [(450 ^ _68193) ^ [] : [aSubsetOf0(xS, sdtmndt0(sdtpldt0(xS, xx), xx)), aSubsetOf0(sdtmndt0(sdtpldt0(xS, xx), xx), xS)], (88 ^ _68193) ^ [_71053, _71055, _71057, _71059] : [-(sdtmndt0(_71059, _71055) = sdtmndt0(_71057, _71053)), _71059 = _71057, _71055 = _71053], (98 ^ _68193) ^ [_71392, _71394, _71396, _71398] : [-(sdtpldt0(_71398, _71394) = sdtpldt0(_71396, _71392)), _71398 = _71396, _71394 = _71392], (2 ^ _68193) ^ [_68337] : [-(_68337 = _68337)], (4 ^ _68193) ^ [_68444, _68446] : [_68446 = _68444, -(_68444 = _68446)], (10 ^ _68193) ^ [_68648, _68650, _68652] : [-(_68652 = _68648), _68652 = _68650, _68650 = _68648], (20 ^ _68193) ^ [_68961, _68963] : [-(isCountable0(_68961)), _68963 = _68961, isCountable0(_68963)], (30 ^ _68193) ^ [_69256, _69258] : [-(isFinite0(_69256)), _69258 = _69256, isFinite0(_69258)], (40 ^ _68193) ^ [_69551, _69553] : [-(aElement0(_69551)), _69553 = _69551, aElement0(_69553)], (50 ^ _68193) ^ [_69846, _69848] : [-(aSet0(_69846)), _69848 = _69846, aSet0(_69848)], (60 ^ _68193) ^ [_70169, _70171, _70173, _70175] : [-(aElementOf0(_70173, _70169)), aElementOf0(_70175, _70171), _70175 = _70173, _70171 = _70169], (74 ^ _68193) ^ [_70593, _70595, _70597, _70599] : [-(aSubsetOf0(_70597, _70593)), aSubsetOf0(_70599, _70595), _70599 = _70597, _70595 = _70593], (108 ^ _68193) ^ [_71715] : [aSet0(_71715), true___, -(true___)], (118 ^ _68193) ^ [_71970] : [aElement0(_71970), true___, -(true___)], (128 ^ _68193) ^ [_72225] : [aSet0(_72225), 131 ^ _68193 : [(132 ^ _68193) ^ [_72355] : [aElementOf0(_72355, _72225), -(aElement0(_72355))]]], (138 ^ _68193) ^ [_72556] : [aSet0(_72556), isFinite0(_72556), true___, -(true___)], (152 ^ _68193) ^ [_72926] : [_72926 = slcrc0, 155 ^ _68193 : [(156 ^ _68193) ^ [] : [-(aSet0(_72926))], (158 ^ _68193) ^ [_73107] : [aElementOf0(_73107, _72926)]]], (160 ^ _68193) ^ [_73175] : [-(_73175 = slcrc0), aSet0(_73175), -(aElementOf0(165 ^ [_73175], _73175))], (171 ^ _68193) ^ [] : [-(isFinite0(slcrc0))], (173 ^ _68193) ^ [_73557] : [aSet0(_73557), isCountable0(_73557), true___, -(true___)], (187 ^ _68193) ^ [_73898] : [isFinite0(_73898), aSet0(_73898), isCountable0(_73898)], (197 ^ _68193) ^ [_74168] : [_74168 = slcrc0, aSet0(_74168), isCountable0(_74168)], (207 ^ _68193) ^ [_74440] : [aSet0(_74440), 210 ^ _68193 : [(211 ^ _68193) ^ [_74616] : [aSubsetOf0(_74616, _74440), 214 ^ _68193 : [(215 ^ _68193) ^ [] : [-(aSet0(_74616))], (217 ^ _68193) ^ [_74825] : [aElementOf0(_74825, _74616), -(aElementOf0(_74825, _74440))]]], (223 ^ _68193) ^ [_75004] : [-(aSubsetOf0(_75004, _74440)), aSet0(_75004), 229 ^ _68193 : [(230 ^ _68193) ^ [] : [-(aElementOf0(228 ^ [_74440, _75004], _75004))], (232 ^ _68193) ^ [] : [aElementOf0(228 ^ [_74440, _75004], _74440)]]]]], (236 ^ _68193) ^ [_75441] : [aSet0(_75441), isFinite0(_75441), 243 ^ _68193 : [(244 ^ _68193) ^ [_75654] : [aSubsetOf0(_75654, _75441), -(isFinite0(_75654))]]], (250 ^ _68193) ^ [_75857] : [aSet0(_75857), -(aSubsetOf0(_75857, _75857))], (256 ^ _68193) ^ [_76059, _76061] : [aSet0(_76061), aSet0(_76059), -(_76061 = _76059), aSubsetOf0(_76061, _76059), aSubsetOf0(_76059, _76061)], (274 ^ _68193) ^ [_76548, _76550, _76552] : [aSet0(_76552), aSet0(_76550), aSet0(_76548), -(aSubsetOf0(_76552, _76548)), aSubsetOf0(_76552, _76550), aSubsetOf0(_76550, _76548)], (296 ^ _68193) ^ [_77134, _77136] : [aSet0(_77136), aElement0(_77134), 303 ^ _68193 : [(334 ^ _68193) ^ [_78395] : [-(_78395 = sdtpldt0(_77136, _77134)), aSet0(_78395), 342 ^ _68193 : [(343 ^ _68193) ^ [] : [-(aElementOf0(339 ^ [_77134, _77136, _78395], _78395))], (345 ^ _68193) ^ [] : [aElement0(339 ^ [_77134, _77136, _78395]), 348 ^ _68193 : [(349 ^ _68193) ^ [] : [aElementOf0(339 ^ [_77134, _77136, _78395], _77136)], (351 ^ _68193) ^ [] : [339 ^ [_77134, _77136, _78395] = _77134]]]], 352 ^ _68193 : [(361 ^ _68193) ^ [] : [aElementOf0(339 ^ [_77134, _77136, _78395], _78395)], (353 ^ _68193) ^ [] : [-(aElement0(339 ^ [_77134, _77136, _78395]))], (355 ^ _68193) ^ [] : [-(aElementOf0(339 ^ [_77134, _77136, _78395], _77136)), -(339 ^ [_77134, _77136, _78395] = _77134)]]], (304 ^ _68193) ^ [_77415] : [_77415 = sdtpldt0(_77136, _77134), 307 ^ _68193 : [(308 ^ _68193) ^ [] : [-(aSet0(_77415))], (310 ^ _68193) ^ [_77678] : [aElementOf0(_77678, _77415), 313 ^ _68193 : [(314 ^ _68193) ^ [] : [-(aElement0(_77678))], (316 ^ _68193) ^ [] : [-(aElementOf0(_77678, _77136)), -(_77678 = _77134)]]], (322 ^ _68193) ^ [_78033] : [-(aElementOf0(_78033, _77415)), aElement0(_78033), 327 ^ _68193 : [(328 ^ _68193) ^ [] : [aElementOf0(_78033, _77136)], (330 ^ _68193) ^ [] : [_78033 = _77134]]]]]]], (444 ^ _68193) ^ [] : [-(aElement0(xx))], (446 ^ _68193) ^ [] : [-(aSet0(xS))], (448 ^ _68193) ^ [] : [aElementOf0(xx, xS)], (434 ^ _68193) ^ [_81730] : [aSet0(_81730), 437 ^ _68193 : [(438 ^ _68193) ^ [_81867] : [aElementOf0(_81867, _81730), -(sdtpldt0(sdtmndt0(_81730, _81867), _81867) = _81730)]]], (365 ^ _68193) ^ [_79432, _79434] : [aSet0(_79434), aElement0(_79432), 372 ^ _68193 : [(403 ^ _68193) ^ [_80700] : [-(_80700 = sdtmndt0(_79434, _79432)), aSet0(_80700), 423 ^ _68193 : [(424 ^ _68193) ^ [] : [-(aElement0(408 ^ [_79432, _79434, _80700]))], (426 ^ _68193) ^ [] : [-(aElementOf0(408 ^ [_79432, _79434, _80700], _79434))], (428 ^ _68193) ^ [] : [408 ^ [_79432, _79434, _80700] = _79432], (430 ^ _68193) ^ [] : [aElementOf0(408 ^ [_79432, _79434, _80700], _80700)]], 411 ^ _68193 : [(412 ^ _68193) ^ [] : [-(aElementOf0(408 ^ [_79432, _79434, _80700], _80700))], (414 ^ _68193) ^ [] : [aElement0(408 ^ [_79432, _79434, _80700]), aElementOf0(408 ^ [_79432, _79434, _80700], _79434), -(408 ^ [_79432, _79434, _80700] = _79432)]]], (373 ^ _68193) ^ [_79715] : [_79715 = sdtmndt0(_79434, _79432), 376 ^ _68193 : [(377 ^ _68193) ^ [] : [-(aSet0(_79715))], (379 ^ _68193) ^ [_79980] : [aElementOf0(_79980, _79715), 382 ^ _68193 : [(383 ^ _68193) ^ [] : [-(aElement0(_79980))], (385 ^ _68193) ^ [] : [-(aElementOf0(_79980, _79434))], (387 ^ _68193) ^ [] : [_79980 = _79432]]], (389 ^ _68193) ^ [_80316] : [-(aElementOf0(_80316, _79715)), aElement0(_80316), aElementOf0(_80316, _79434), -(_80316 = _79432)]]]]]], input).
% 0.68/1.37 ncf('1',plain,[aSubsetOf0(xS, sdtmndt0(sdtpldt0(xS, xx), xx)), aSubsetOf0(sdtmndt0(sdtpldt0(xS, xx), xx), xS)],start(450 ^ 0)).
% 0.68/1.37 ncf('1.1',plain,[-(aSubsetOf0(xS, sdtmndt0(sdtpldt0(xS, xx), xx))), aSubsetOf0(xS, xS), xS = xS, xS = sdtmndt0(sdtpldt0(xS, xx), xx)],extension(74 ^ 1,bind([[_70593, _70595, _70597, _70599], [sdtmndt0(sdtpldt0(xS, xx), xx), xS, xS, xS]]))).
% 0.68/1.37 ncf('1.1.1',plain,[-(aSubsetOf0(xS, xS)), aSubsetOf0(xS, xS), xS = xS, xS = xS],extension(74 ^ 2,bind([[_70593, _70595, _70597, _70599], [xS, xS, xS, xS]]))).
% 0.68/1.37 ncf('1.1.1.1',plain,[-(aSubsetOf0(xS, xS)), aSubsetOf0(xS, xS), xS = xS, xS = xS],extension(74 ^ 3,bind([[_70593, _70595, _70597, _70599], [xS, xS, xS, xS]]))).
% 0.68/1.37 ncf('1.1.1.1.1',plain,[-(aSubsetOf0(xS, xS)), aSet0(xS)],extension(250 ^ 4,bind([[_75857], [xS]]))).
% 0.68/1.37 ncf('1.1.1.1.1.1',plain,[-(aSet0(xS))],extension(446 ^ 5)).
% 0.68/1.37 ncf('1.1.1.1.2',plain,[-(xS = xS)],extension(2 ^ 4,bind([[_68337], [xS]]))).
% 0.68/1.37 ncf('1.1.1.1.3',plain,[-(xS = xS)],extension(2 ^ 4,bind([[_68337], [xS]]))).
% 0.68/1.37 ncf('1.1.1.2',plain,[-(xS = xS)],extension(2 ^ 3,bind([[_68337], [xS]]))).
% 0.68/1.37 ncf('1.1.1.3',plain,[-(xS = xS)],extension(2 ^ 3,bind([[_68337], [xS]]))).
% 0.68/1.37 ncf('1.1.2',plain,[-(xS = xS)],extension(2 ^ 2,bind([[_68337], [xS]]))).
% 0.68/1.37 ncf('1.1.3',plain,[-(xS = sdtmndt0(sdtpldt0(xS, xx), xx)), 403 : aSet0(xS), 426 : -(aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], sdtpldt0(xS, xx))), 414 : aElement0(408 ^ [xx, sdtpldt0(xS, xx), xS]), 414 : aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], sdtpldt0(xS, xx)), 414 : -(408 ^ [xx, sdtpldt0(xS, xx), xS] = xx), 403 : aSet0(sdtpldt0(xS, xx)), 403 : aElement0(xx)],extension(365 ^ 2,bind([[_79432, _79434, _80700], [xx, sdtpldt0(xS, xx), xS]]))).
% 0.68/1.37 ncf('1.1.3.1',plain,[-(aSet0(xS))],extension(446 ^ 5)).
% 0.68/1.37 ncf('1.1.3.2',plain,[aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], sdtpldt0(xS, xx)), 316 : -(aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], xS)), 316 : -(408 ^ [xx, sdtpldt0(xS, xx), xS] = xx), 310 : sdtpldt0(xS, xx) = sdtpldt0(xS, xx), 304 : aSet0(xS), 304 : aElement0(xx)],extension(296 ^ 7,bind([[_77134, _77136, _77415, _77678], [xx, xS, sdtpldt0(xS, xx), 408 ^ [xx, sdtpldt0(xS, xx), xS]]]))).
% 0.68/1.37 ncf('1.1.3.2.1',plain,[aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], xS)],extension(430 ^ 14)).
% 0.68/1.37 ncf('1.1.3.2.2',plain,[408 ^ [xx, sdtpldt0(xS, xx), xS] = xx],extension(428 ^ 14)).
% 0.68/1.37 ncf('1.1.3.2.3',plain,[-(sdtpldt0(xS, xx) = sdtpldt0(xS, xx))],extension(2 ^ 10,bind([[_68337], [sdtpldt0(xS, xx)]]))).
% 0.68/1.37 ncf('1.1.3.2.4',plain,[-(aSet0(xS))],lemmata('[1, 1].x')).
% 0.68/1.37 ncf('1.1.3.2.5',plain,[-(aElement0(xx))],extension(444 ^ 8)).
% 0.68/1.37 ncf('1.1.3.3',plain,[-(aElement0(408 ^ [xx, sdtpldt0(xS, xx), xS])), 132 : aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], xS), 132 : aSet0(xS)],extension(128 ^ 7,bind([[_72225, _72355], [xS, 408 ^ [xx, sdtpldt0(xS, xx), xS]]]))).
% 0.68/1.37 ncf('1.1.3.3.1',plain,[-(aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], xS))],extension(412 ^ 10)).
% 0.68/1.37 ncf('1.1.3.3.2',plain,[-(aSet0(xS))],lemmata('[1, 1].x')).
% 0.68/1.37 ncf('1.1.3.4',plain,[-(aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], sdtpldt0(xS, xx))), 322 : aElement0(408 ^ [xx, sdtpldt0(xS, xx), xS]), 328 : aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], xS), 322 : sdtpldt0(xS, xx) = sdtpldt0(xS, xx), 304 : aSet0(xS), 304 : aElement0(xx)],extension(296 ^ 7,bind([[_77134, _77136, _77415, _78033], [xx, xS, sdtpldt0(xS, xx), 408 ^ [xx, sdtpldt0(xS, xx), xS]]]))).
% 0.68/1.37 ncf('1.1.3.4.1',plain,[-(aElement0(408 ^ [xx, sdtpldt0(xS, xx), xS]))],lemmata('[1, 1].x')).
% 0.68/1.37 ncf('1.1.3.4.2',plain,[-(aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], xS))],extension(412 ^ 14)).
% 0.68/1.37 ncf('1.1.3.4.3',plain,[-(sdtpldt0(xS, xx) = sdtpldt0(xS, xx))],extension(2 ^ 10,bind([[_68337], [sdtpldt0(xS, xx)]]))).
% 0.68/1.37 ncf('1.1.3.4.4',plain,[-(aSet0(xS))],lemmata('[1, 1].x')).
% 0.68/1.37 ncf('1.1.3.4.5',plain,[-(aElement0(xx))],extension(444 ^ 8)).
% 0.68/1.37 ncf('1.1.3.5',plain,[408 ^ [xx, sdtpldt0(xS, xx), xS] = xx, -(aElementOf0(xx, xS)), aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], xS), xS = xS],extension(60 ^ 7,bind([[_70169, _70171, _70173, _70175], [xS, xS, xx, 408 ^ [xx, sdtpldt0(xS, xx), xS]]]))).
% 0.68/1.37 ncf('1.1.3.5.1',plain,[aElementOf0(xx, xS)],extension(448 ^ 8)).
% 0.68/1.37 ncf('1.1.3.5.2',plain,[-(aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], xS))],extension(412 ^ 8)).
% 0.68/1.37 ncf('1.1.3.5.3',plain,[-(xS = xS)],lemmata('[1].x')).
% 0.68/1.37 ncf('1.1.3.6',plain,[-(aSet0(sdtpldt0(xS, xx))), 304 : sdtpldt0(xS, xx) = sdtpldt0(xS, xx), 304 : aSet0(xS), 304 : aElement0(xx)],extension(296 ^ 3,bind([[_77134, _77136, _77415], [xx, xS, sdtpldt0(xS, xx)]]))).
% 0.68/1.37 ncf('1.1.3.6.1',plain,[-(sdtpldt0(xS, xx) = sdtpldt0(xS, xx))],extension(2 ^ 6,bind([[_68337], [sdtpldt0(xS, xx)]]))).
% 0.68/1.37 ncf('1.1.3.6.2',plain,[-(aSet0(xS))],extension(446 ^ 4)).
% 0.68/1.37 ncf('1.1.3.6.3',plain,[-(aElement0(xx))],extension(444 ^ 4)).
% 0.68/1.37 ncf('1.1.3.7',plain,[-(aElement0(xx))],extension(444 ^ 3)).
% 0.68/1.37 ncf('1.2',plain,[-(aSubsetOf0(sdtmndt0(sdtpldt0(xS, xx), xx), xS)), aSubsetOf0(xS, xS), xS = sdtmndt0(sdtpldt0(xS, xx), xx), xS = xS],extension(74 ^ 1,bind([[_70593, _70595, _70597, _70599], [xS, xS, sdtmndt0(sdtpldt0(xS, xx), xx), xS]]))).
% 0.68/1.37 ncf('1.2.1',plain,[-(aSubsetOf0(xS, xS)), aSubsetOf0(xS, xS), xS = xS, xS = xS],extension(74 ^ 2,bind([[_70593, _70595, _70597, _70599], [xS, xS, xS, xS]]))).
% 0.68/1.37 ncf('1.2.1.1',plain,[-(aSubsetOf0(xS, xS)), aSubsetOf0(xS, xS), xS = xS, xS = xS],extension(74 ^ 3,bind([[_70593, _70595, _70597, _70599], [xS, xS, xS, xS]]))).
% 0.68/1.37 ncf('1.2.1.1.1',plain,[-(aSubsetOf0(xS, xS)), aSet0(xS)],extension(250 ^ 4,bind([[_75857], [xS]]))).
% 0.68/1.37 ncf('1.2.1.1.1.1',plain,[-(aSet0(xS))],extension(446 ^ 5)).
% 0.68/1.37 ncf('1.2.1.1.2',plain,[-(xS = xS)],extension(2 ^ 4,bind([[_68337], [xS]]))).
% 0.68/1.37 ncf('1.2.1.1.3',plain,[-(xS = xS)],extension(2 ^ 4,bind([[_68337], [xS]]))).
% 0.68/1.37 ncf('1.2.1.2',plain,[-(xS = xS)],extension(2 ^ 3,bind([[_68337], [xS]]))).
% 0.68/1.37 ncf('1.2.1.3',plain,[-(xS = xS)],extension(2 ^ 3,bind([[_68337], [xS]]))).
% 0.68/1.37 ncf('1.2.2',plain,[-(xS = sdtmndt0(sdtpldt0(xS, xx), xx)), 403 : aSet0(xS), 426 : -(aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], sdtpldt0(xS, xx))), 414 : aElement0(408 ^ [xx, sdtpldt0(xS, xx), xS]), 414 : aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], sdtpldt0(xS, xx)), 414 : -(408 ^ [xx, sdtpldt0(xS, xx), xS] = xx), 403 : aSet0(sdtpldt0(xS, xx)), 403 : aElement0(xx)],extension(365 ^ 2,bind([[_79432, _79434, _80700], [xx, sdtpldt0(xS, xx), xS]]))).
% 0.68/1.37 ncf('1.2.2.1',plain,[-(aSet0(xS))],extension(446 ^ 5)).
% 0.68/1.37 ncf('1.2.2.2',plain,[aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], sdtpldt0(xS, xx)), 316 : -(aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], xS)), 316 : -(408 ^ [xx, sdtpldt0(xS, xx), xS] = xx), 310 : sdtpldt0(xS, xx) = sdtpldt0(xS, xx), 304 : aSet0(xS), 304 : aElement0(xx)],extension(296 ^ 7,bind([[_77134, _77136, _77415, _77678], [xx, xS, sdtpldt0(xS, xx), 408 ^ [xx, sdtpldt0(xS, xx), xS]]]))).
% 0.68/1.37 ncf('1.2.2.2.1',plain,[aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], xS)],extension(430 ^ 14)).
% 0.68/1.37 ncf('1.2.2.2.2',plain,[408 ^ [xx, sdtpldt0(xS, xx), xS] = xx],extension(428 ^ 14)).
% 0.68/1.37 ncf('1.2.2.2.3',plain,[-(sdtpldt0(xS, xx) = sdtpldt0(xS, xx))],extension(2 ^ 10,bind([[_68337], [sdtpldt0(xS, xx)]]))).
% 0.68/1.37 ncf('1.2.2.2.4',plain,[-(aSet0(xS))],lemmata('[2, 1].x')).
% 0.68/1.37 ncf('1.2.2.2.5',plain,[-(aElement0(xx))],extension(444 ^ 8)).
% 0.68/1.37 ncf('1.2.2.3',plain,[-(aElement0(408 ^ [xx, sdtpldt0(xS, xx), xS])), 132 : aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], xS), 132 : aSet0(xS)],extension(128 ^ 7,bind([[_72225, _72355], [xS, 408 ^ [xx, sdtpldt0(xS, xx), xS]]]))).
% 0.68/1.37 ncf('1.2.2.3.1',plain,[-(aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], xS))],extension(412 ^ 10)).
% 0.68/1.37 ncf('1.2.2.3.2',plain,[-(aSet0(xS))],lemmata('[2, 1].x')).
% 0.68/1.37 ncf('1.2.2.4',plain,[-(aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], sdtpldt0(xS, xx))), 322 : aElement0(408 ^ [xx, sdtpldt0(xS, xx), xS]), 328 : aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], xS), 322 : sdtpldt0(xS, xx) = sdtpldt0(xS, xx), 304 : aSet0(xS), 304 : aElement0(xx)],extension(296 ^ 7,bind([[_77134, _77136, _77415, _78033], [xx, xS, sdtpldt0(xS, xx), 408 ^ [xx, sdtpldt0(xS, xx), xS]]]))).
% 0.68/1.37 ncf('1.2.2.4.1',plain,[-(aElement0(408 ^ [xx, sdtpldt0(xS, xx), xS]))],lemmata('[2, 1].x')).
% 0.68/1.37 ncf('1.2.2.4.2',plain,[-(aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], xS))],extension(412 ^ 14)).
% 0.68/1.37 ncf('1.2.2.4.3',plain,[-(sdtpldt0(xS, xx) = sdtpldt0(xS, xx))],extension(2 ^ 10,bind([[_68337], [sdtpldt0(xS, xx)]]))).
% 0.68/1.37 ncf('1.2.2.4.4',plain,[-(aSet0(xS))],lemmata('[2, 1].x')).
% 0.68/1.37 ncf('1.2.2.4.5',plain,[-(aElement0(xx))],extension(444 ^ 8)).
% 0.68/1.37 ncf('1.2.2.5',plain,[408 ^ [xx, sdtpldt0(xS, xx), xS] = xx, -(aElementOf0(xx, xS)), aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], xS), xS = xS],extension(60 ^ 7,bind([[_70169, _70171, _70173, _70175], [xS, xS, xx, 408 ^ [xx, sdtpldt0(xS, xx), xS]]]))).
% 0.68/1.37 ncf('1.2.2.5.1',plain,[aElementOf0(xx, xS)],extension(448 ^ 8)).
% 0.68/1.37 ncf('1.2.2.5.2',plain,[-(aElementOf0(408 ^ [xx, sdtpldt0(xS, xx), xS], xS))],extension(412 ^ 8)).
% 0.68/1.37 ncf('1.2.2.5.3',plain,[-(xS = xS)],extension(2 ^ 8,bind([[_68337], [xS]]))).
% 0.68/1.37 ncf('1.2.2.6',plain,[-(aSet0(sdtpldt0(xS, xx))), 304 : sdtpldt0(xS, xx) = sdtpldt0(xS, xx), 304 : aSet0(xS), 304 : aElement0(xx)],extension(296 ^ 3,bind([[_77134, _77136, _77415], [xx, xS, sdtpldt0(xS, xx)]]))).
% 0.68/1.37 ncf('1.2.2.6.1',plain,[-(sdtpldt0(xS, xx) = sdtpldt0(xS, xx))],extension(2 ^ 6,bind([[_68337], [sdtpldt0(xS, xx)]]))).
% 0.68/1.37 ncf('1.2.2.6.2',plain,[-(aSet0(xS))],extension(446 ^ 4)).
% 0.68/1.37 ncf('1.2.2.6.3',plain,[-(aElement0(xx))],extension(444 ^ 4)).
% 0.68/1.37 ncf('1.2.2.7',plain,[-(aElement0(xx))],extension(444 ^ 3)).
% 0.68/1.37 ncf('1.2.3',plain,[-(xS = xS)],extension(2 ^ 2,bind([[_68337], [xS]]))).
% 0.68/1.37 %-----------------------------------------------------
% 0.68/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------