%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM535+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% 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 : Fri May 19 11:44:55 EDT 2023
% Result : Theorem 4.00s 4.48s
% Output : Proof 4.00s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : NUM535+1 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n015.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:50:37 EDT 2023
% 0.12/0.33 % CPUTime :
% 4.00/4.48
% 4.00/4.48 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 4.00/4.48 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.00/4.48 %-----------------------------------------------------
% 4.00/4.48 ncf(matrix, plain, [(438 ^ _70291) ^ [] : [aSubsetOf0(xS, sdtpldt0(sdtmndt0(xS, xx), xx)), aSubsetOf0(sdtpldt0(sdtmndt0(xS, xx), xx), xS)], (88 ^ _70291) ^ [_73151, _73153, _73155, _73157] : [-(sdtpldt0(_73157, _73153) = sdtpldt0(_73155, _73151)), _73157 = _73155, _73153 = _73151], (98 ^ _70291) ^ [_73490, _73492, _73494, _73496] : [-(sdtmndt0(_73496, _73492) = sdtmndt0(_73494, _73490)), _73496 = _73494, _73492 = _73490], (2 ^ _70291) ^ [_70435] : [-(_70435 = _70435)], (4 ^ _70291) ^ [_70542, _70544] : [_70544 = _70542, -(_70542 = _70544)], (10 ^ _70291) ^ [_70746, _70748, _70750] : [-(_70750 = _70746), _70750 = _70748, _70748 = _70746], (20 ^ _70291) ^ [_71059, _71061] : [-(isCountable0(_71059)), _71061 = _71059, isCountable0(_71061)], (30 ^ _70291) ^ [_71354, _71356] : [-(isFinite0(_71354)), _71356 = _71354, isFinite0(_71356)], (40 ^ _70291) ^ [_71649, _71651] : [-(aElement0(_71649)), _71651 = _71649, aElement0(_71651)], (50 ^ _70291) ^ [_71944, _71946] : [-(aSet0(_71944)), _71946 = _71944, aSet0(_71946)], (60 ^ _70291) ^ [_72267, _72269, _72271, _72273] : [-(aElementOf0(_72271, _72267)), aElementOf0(_72273, _72269), _72273 = _72271, _72269 = _72267], (74 ^ _70291) ^ [_72691, _72693, _72695, _72697] : [-(aSubsetOf0(_72695, _72691)), aSubsetOf0(_72697, _72693), _72697 = _72695, _72693 = _72691], (108 ^ _70291) ^ [_73813] : [aSet0(_73813), true___, -(true___)], (118 ^ _70291) ^ [_74068] : [aElement0(_74068), true___, -(true___)], (128 ^ _70291) ^ [_74323] : [aSet0(_74323), 131 ^ _70291 : [(132 ^ _70291) ^ [_74453] : [aElementOf0(_74453, _74323), -(aElement0(_74453))]]], (138 ^ _70291) ^ [_74654] : [aSet0(_74654), isFinite0(_74654), true___, -(true___)], (152 ^ _70291) ^ [_75024] : [_75024 = slcrc0, 155 ^ _70291 : [(156 ^ _70291) ^ [] : [-(aSet0(_75024))], (158 ^ _70291) ^ [_75205] : [aElementOf0(_75205, _75024)]]], (160 ^ _70291) ^ [_75273] : [-(_75273 = slcrc0), aSet0(_75273), -(aElementOf0(165 ^ [_75273], _75273))], (171 ^ _70291) ^ [] : [-(isFinite0(slcrc0))], (173 ^ _70291) ^ [_75655] : [aSet0(_75655), isCountable0(_75655), true___, -(true___)], (187 ^ _70291) ^ [_75996] : [isFinite0(_75996), aSet0(_75996), isCountable0(_75996)], (197 ^ _70291) ^ [_76266] : [_76266 = slcrc0, aSet0(_76266), isCountable0(_76266)], (207 ^ _70291) ^ [_76538] : [aSet0(_76538), 210 ^ _70291 : [(211 ^ _70291) ^ [_76714] : [aSubsetOf0(_76714, _76538), 214 ^ _70291 : [(215 ^ _70291) ^ [] : [-(aSet0(_76714))], (217 ^ _70291) ^ [_76923] : [aElementOf0(_76923, _76714), -(aElementOf0(_76923, _76538))]]], (223 ^ _70291) ^ [_77102] : [-(aSubsetOf0(_77102, _76538)), aSet0(_77102), 229 ^ _70291 : [(230 ^ _70291) ^ [] : [-(aElementOf0(228 ^ [_76538, _77102], _77102))], (232 ^ _70291) ^ [] : [aElementOf0(228 ^ [_76538, _77102], _76538)]]]]], (236 ^ _70291) ^ [_77539] : [aSet0(_77539), isFinite0(_77539), 243 ^ _70291 : [(244 ^ _70291) ^ [_77752] : [aSubsetOf0(_77752, _77539), -(isFinite0(_77752))]]], (250 ^ _70291) ^ [_77955] : [aSet0(_77955), -(aSubsetOf0(_77955, _77955))], (256 ^ _70291) ^ [_78157, _78159] : [aSet0(_78159), aSet0(_78157), -(_78159 = _78157), aSubsetOf0(_78159, _78157), aSubsetOf0(_78157, _78159)], (274 ^ _70291) ^ [_78646, _78648, _78650] : [aSet0(_78650), aSet0(_78648), aSet0(_78646), -(aSubsetOf0(_78650, _78646)), aSubsetOf0(_78650, _78648), aSubsetOf0(_78648, _78646)], (434 ^ _70291) ^ [] : [-(aSet0(xS))], (436 ^ _70291) ^ [] : [-(aElementOf0(xx, xS))], (365 ^ _70291) ^ [_81530, _81532] : [aSet0(_81532), aElement0(_81530), 372 ^ _70291 : [(403 ^ _70291) ^ [_82798] : [-(_82798 = sdtmndt0(_81532, _81530)), aSet0(_82798), 423 ^ _70291 : [(424 ^ _70291) ^ [] : [-(aElement0(408 ^ [_81530, _81532, _82798]))], (426 ^ _70291) ^ [] : [-(aElementOf0(408 ^ [_81530, _81532, _82798], _81532))], (428 ^ _70291) ^ [] : [408 ^ [_81530, _81532, _82798] = _81530], (430 ^ _70291) ^ [] : [aElementOf0(408 ^ [_81530, _81532, _82798], _82798)]], 411 ^ _70291 : [(412 ^ _70291) ^ [] : [-(aElementOf0(408 ^ [_81530, _81532, _82798], _82798))], (414 ^ _70291) ^ [] : [aElement0(408 ^ [_81530, _81532, _82798]), aElementOf0(408 ^ [_81530, _81532, _82798], _81532), -(408 ^ [_81530, _81532, _82798] = _81530)]]], (373 ^ _70291) ^ [_81813] : [_81813 = sdtmndt0(_81532, _81530), 376 ^ _70291 : [(377 ^ _70291) ^ [] : [-(aSet0(_81813))], (379 ^ _70291) ^ [_82078] : [aElementOf0(_82078, _81813), 382 ^ _70291 : [(383 ^ _70291) ^ [] : [-(aElement0(_82078))], (385 ^ _70291) ^ [] : [-(aElementOf0(_82078, _81532))], (387 ^ _70291) ^ [] : [_82078 = _81530]]], (389 ^ _70291) ^ [_82414] : [-(aElementOf0(_82414, _81813)), aElement0(_82414), aElementOf0(_82414, _81532), -(_82414 = _81530)]]]]], (296 ^ _70291) ^ [_79232, _79234] : [aSet0(_79234), aElement0(_79232), 303 ^ _70291 : [(334 ^ _70291) ^ [_80493] : [-(_80493 = sdtpldt0(_79234, _79232)), aSet0(_80493), 342 ^ _70291 : [(343 ^ _70291) ^ [] : [-(aElementOf0(339 ^ [_79232, _79234, _80493], _80493))], (345 ^ _70291) ^ [] : [aElement0(339 ^ [_79232, _79234, _80493]), 348 ^ _70291 : [(349 ^ _70291) ^ [] : [aElementOf0(339 ^ [_79232, _79234, _80493], _79234)], (351 ^ _70291) ^ [] : [339 ^ [_79232, _79234, _80493] = _79232]]]], 352 ^ _70291 : [(361 ^ _70291) ^ [] : [aElementOf0(339 ^ [_79232, _79234, _80493], _80493)], (353 ^ _70291) ^ [] : [-(aElement0(339 ^ [_79232, _79234, _80493]))], (355 ^ _70291) ^ [] : [-(aElementOf0(339 ^ [_79232, _79234, _80493], _79234)), -(339 ^ [_79232, _79234, _80493] = _79232)]]], (304 ^ _70291) ^ [_79513] : [_79513 = sdtpldt0(_79234, _79232), 307 ^ _70291 : [(308 ^ _70291) ^ [] : [-(aSet0(_79513))], (310 ^ _70291) ^ [_79776] : [aElementOf0(_79776, _79513), 313 ^ _70291 : [(314 ^ _70291) ^ [] : [-(aElement0(_79776))], (316 ^ _70291) ^ [] : [-(aElementOf0(_79776, _79234)), -(_79776 = _79232)]]], (322 ^ _70291) ^ [_80131] : [-(aElementOf0(_80131, _79513)), aElement0(_80131), 327 ^ _70291 : [(328 ^ _70291) ^ [] : [aElementOf0(_80131, _79234)], (330 ^ _70291) ^ [] : [_80131 = _79232]]]]]]]], input).
% 4.00/4.48 ncf('1',plain,[aSubsetOf0(xS, sdtpldt0(sdtmndt0(xS, xx), xx)), aSubsetOf0(sdtpldt0(sdtmndt0(xS, xx), xx), xS)],start(438 ^ 0)).
% 4.00/4.48 ncf('1.1',plain,[-(aSubsetOf0(xS, sdtpldt0(sdtmndt0(xS, xx), xx))), aSubsetOf0(xS, xS), xS = xS, xS = sdtpldt0(sdtmndt0(xS, xx), xx)],extension(74 ^ 1,bind([[_72691, _72693, _72695, _72697], [sdtpldt0(sdtmndt0(xS, xx), xx), xS, xS, xS]]))).
% 4.00/4.48 ncf('1.1.1',plain,[-(aSubsetOf0(xS, xS)), aSubsetOf0(xS, xS), xS = xS, xS = xS],extension(74 ^ 2,bind([[_72691, _72693, _72695, _72697], [xS, xS, xS, xS]]))).
% 4.00/4.48 ncf('1.1.1.1',plain,[-(aSubsetOf0(xS, xS)), aSubsetOf0(xS, xS), xS = xS, xS = xS],extension(74 ^ 3,bind([[_72691, _72693, _72695, _72697], [xS, xS, xS, xS]]))).
% 4.00/4.48 ncf('1.1.1.1.1',plain,[-(aSubsetOf0(xS, xS)), aSubsetOf0(xS, xS), xS = xS, xS = xS],extension(74 ^ 4,bind([[_72691, _72693, _72695, _72697], [xS, xS, xS, xS]]))).
% 4.00/4.48 ncf('1.1.1.1.1.1',plain,[-(aSubsetOf0(xS, xS)), aSet0(xS)],extension(250 ^ 5,bind([[_77955], [xS]]))).
% 4.00/4.48 ncf('1.1.1.1.1.1.1',plain,[-(aSet0(xS))],extension(434 ^ 6)).
% 4.00/4.48 ncf('1.1.1.1.1.2',plain,[-(xS = xS)],extension(2 ^ 5,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.1.1.1.1.3',plain,[-(xS = xS)],extension(2 ^ 5,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.1.1.1.2',plain,[-(xS = xS)],extension(2 ^ 4,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.1.1.1.3',plain,[-(xS = xS)],extension(2 ^ 4,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.1.1.2',plain,[-(xS = xS)],extension(2 ^ 3,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.1.1.3',plain,[-(xS = xS)],extension(2 ^ 3,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.1.2',plain,[-(xS = xS)],extension(2 ^ 2,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.1.3',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([[_79232, _79234, _80493], [xx, sdtmndt0(xS, xx), xS]]))).
% 4.00/4.48 ncf('1.1.3.1',plain,[-(aSet0(xS))],extension(434 ^ 5)).
% 4.00/4.48 ncf('1.1.3.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([[_74323, _74453], [xS, 339 ^ [xx, sdtmndt0(xS, xx), xS]]]))).
% 4.00/4.48 ncf('1.1.3.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([[_81530, _81532, _81813, _82414], [xx, xS, sdtmndt0(xS, xx), 339 ^ [xx, sdtmndt0(xS, xx), xS]]]))).
% 4.00/4.48 ncf('1.1.3.2.1.1',plain,[aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], sdtmndt0(xS, xx)), aElement0(339 ^ [xx, sdtmndt0(xS, xx), xS])],extension(345 ^ 15)).
% 4.00/4.48 ncf('1.1.3.2.1.1.1',plain,[-(aElement0(339 ^ [xx, sdtmndt0(xS, xx), xS]))],reduction('1.1.3.2')).
% 4.00/4.48 ncf('1.1.3.2.1.2',plain,[-(aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], xS))],reduction('1.1.3')).
% 4.00/4.48 ncf('1.1.3.2.1.3',plain,[339 ^ [xx, sdtmndt0(xS, xx), xS] = xx, aElement0(339 ^ [xx, sdtmndt0(xS, xx), xS])],extension(345 ^ 15)).
% 4.00/4.48 ncf('1.1.3.2.1.3.1',plain,[-(aElement0(339 ^ [xx, sdtmndt0(xS, xx), xS]))],reduction('1.1.3.2')).
% 4.00/4.48 ncf('1.1.3.2.1.4',plain,[-(sdtmndt0(xS, xx) = sdtmndt0(xS, xx))],extension(2 ^ 13,bind([[_70435], [sdtmndt0(xS, xx)]]))).
% 4.00/4.48 ncf('1.1.3.2.1.5',plain,[-(aSet0(xS))],lemmata('[1, 1].x')).
% 4.00/4.48 ncf('1.1.3.2.1.6',plain,[-(aElement0(xx)), aElementOf0(xx, xS)],extension(132 ^ 11,bind([[_74453], [xx]]))).
% 4.00/4.48 ncf('1.1.3.2.1.6.1',plain,[-(aElementOf0(xx, xS))],extension(436 ^ 12)).
% 4.00/4.48 ncf('1.1.3.2.2',plain,[-(aSet0(xS))],lemmata('[1, 1].x')).
% 4.00/4.48 ncf('1.1.3.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([[_81530, _81532, _81813, _82078], [xx, xS, sdtmndt0(xS, xx), 339 ^ [xx, sdtmndt0(xS, xx), xS]]]))).
% 4.00/4.48 ncf('1.1.3.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(60 ^ 14,bind([[_72267, _72269, _72271, _72273], [xS, xS, 339 ^ [xx, sdtmndt0(xS, xx), xS], 339 ^ [xx, sdtmndt0(xS, xx), xS]]]))).
% 4.00/4.48 ncf('1.1.3.3.1.1',plain,[aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], xS)],extension(361 ^ 15)).
% 4.00/4.48 ncf('1.1.3.3.1.2',plain,[-(339 ^ [xx, sdtmndt0(xS, xx), xS] = 339 ^ [xx, sdtmndt0(xS, xx), xS])],extension(2 ^ 15,bind([[_70435], [339 ^ [xx, sdtmndt0(xS, xx), xS]]]))).
% 4.00/4.48 ncf('1.1.3.3.1.3',plain,[-(xS = xS)],extension(2 ^ 15,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.1.3.3.2',plain,[-(sdtmndt0(xS, xx) = sdtmndt0(xS, xx)), xS = xS, xx = xx],extension(98 ^ 10,bind([[_73490, _73492, _73494, _73496], [xx, xx, xS, xS]]))).
% 4.00/4.48 ncf('1.1.3.3.2.1',plain,[-(xS = xS)],lemmata('[1].x')).
% 4.00/4.48 ncf('1.1.3.3.2.2',plain,[-(xx = xx)],extension(2 ^ 11,bind([[_70435], [xx]]))).
% 4.00/4.48 ncf('1.1.3.3.3',plain,[-(aSet0(xS))],lemmata('[1, 1].x')).
% 4.00/4.48 ncf('1.1.3.3.4',plain,[-(aElement0(xx)), 132 : aElementOf0(xx, xS), 132 : aSet0(xS)],extension(128 ^ 8,bind([[_74323, _74453], [xS, xx]]))).
% 4.00/4.48 ncf('1.1.3.3.4.1',plain,[-(aElementOf0(xx, xS))],extension(436 ^ 11)).
% 4.00/4.48 ncf('1.1.3.3.4.2',plain,[-(aSet0(xS))],lemmata('[3, 1, 1].x')).
% 4.00/4.48 ncf('1.1.3.4',plain,[339 ^ [xx, sdtmndt0(xS, xx), xS] = xx, -(xx = 339 ^ [xx, sdtmndt0(xS, xx), xS])],extension(4 ^ 7,bind([[_70542, _70544], [xx, 339 ^ [xx, sdtmndt0(xS, xx), xS]]]))).
% 4.00/4.48 ncf('1.1.3.4.1',plain,[xx = 339 ^ [xx, sdtmndt0(xS, xx), xS], -(aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], xS)), aElementOf0(xx, xS), xS = xS],extension(60 ^ 8,bind([[_72267, _72269, _72271, _72273], [xS, xS, 339 ^ [xx, sdtmndt0(xS, xx), xS], xx]]))).
% 4.00/4.48 ncf('1.1.3.4.1.1',plain,[aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], xS)],extension(361 ^ 9)).
% 4.00/4.48 ncf('1.1.3.4.1.2',plain,[-(aElementOf0(xx, xS))],extension(436 ^ 9)).
% 4.00/4.48 ncf('1.1.3.4.1.3',plain,[-(xS = xS)],lemmata('[1].x')).
% 4.00/4.48 ncf('1.1.3.5',plain,[-(aSet0(sdtmndt0(xS, xx))), 373 : sdtmndt0(xS, xx) = sdtmndt0(xS, xx), 373 : aSet0(xS), 373 : aElement0(xx)],extension(365 ^ 3,bind([[_81530, _81532, _81813], [xx, xS, sdtmndt0(xS, xx)]]))).
% 4.00/4.48 ncf('1.1.3.5.1',plain,[-(sdtmndt0(xS, xx) = sdtmndt0(xS, xx)), xS = xS, xx = xx],extension(98 ^ 6,bind([[_73490, _73492, _73494, _73496], [xx, xx, xS, xS]]))).
% 4.00/4.48 ncf('1.1.3.5.1.1',plain,[-(xS = xS)],extension(2 ^ 7,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.1.3.5.1.2',plain,[-(xx = xx)],extension(2 ^ 7,bind([[_70435], [xx]]))).
% 4.00/4.48 ncf('1.1.3.5.2',plain,[-(aSet0(xS))],extension(434 ^ 4)).
% 4.00/4.48 ncf('1.1.3.5.3',plain,[-(aElement0(xx)), 132 : aElementOf0(xx, xS), 132 : aSet0(xS)],extension(128 ^ 4,bind([[_74323, _74453], [xS, xx]]))).
% 4.00/4.48 ncf('1.1.3.5.3.1',plain,[-(aElementOf0(xx, xS))],extension(436 ^ 7)).
% 4.00/4.48 ncf('1.1.3.5.3.2',plain,[-(aSet0(xS))],lemmata('[3, 1, 1].x')).
% 4.00/4.48 ncf('1.1.3.6',plain,[-(aElement0(xx)), 132 : aElementOf0(xx, xS), 132 : aSet0(xS)],extension(128 ^ 3,bind([[_74323, _74453], [xS, xx]]))).
% 4.00/4.48 ncf('1.1.3.6.1',plain,[-(aElementOf0(xx, xS)), aElementOf0(xx, xS), xx = xx, xS = xS],extension(60 ^ 6,bind([[_72267, _72269, _72271, _72273], [xS, xS, xx, xx]]))).
% 4.00/4.48 ncf('1.1.3.6.1.1',plain,[-(aElementOf0(xx, xS))],extension(436 ^ 7)).
% 4.00/4.48 ncf('1.1.3.6.1.2',plain,[-(xx = xx)],extension(2 ^ 7,bind([[_70435], [xx]]))).
% 4.00/4.48 ncf('1.1.3.6.1.3',plain,[-(xS = xS)],extension(2 ^ 7,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.1.3.6.2',plain,[-(aSet0(xS))],extension(434 ^ 4)).
% 4.00/4.48 ncf('1.2',plain,[-(aSubsetOf0(sdtpldt0(sdtmndt0(xS, xx), xx), xS)), aSubsetOf0(xS, xS), xS = sdtpldt0(sdtmndt0(xS, xx), xx), xS = xS],extension(74 ^ 1,bind([[_72691, _72693, _72695, _72697], [xS, xS, sdtpldt0(sdtmndt0(xS, xx), xx), xS]]))).
% 4.00/4.48 ncf('1.2.1',plain,[-(aSubsetOf0(xS, xS)), aSubsetOf0(xS, xS), xS = xS, xS = xS],extension(74 ^ 2,bind([[_72691, _72693, _72695, _72697], [xS, xS, xS, xS]]))).
% 4.00/4.48 ncf('1.2.1.1',plain,[-(aSubsetOf0(xS, xS)), aSubsetOf0(xS, xS), xS = xS, xS = xS],extension(74 ^ 3,bind([[_72691, _72693, _72695, _72697], [xS, xS, xS, xS]]))).
% 4.00/4.48 ncf('1.2.1.1.1',plain,[-(aSubsetOf0(xS, xS)), aSubsetOf0(xS, xS), xS = xS, xS = xS],extension(74 ^ 4,bind([[_72691, _72693, _72695, _72697], [xS, xS, xS, xS]]))).
% 4.00/4.48 ncf('1.2.1.1.1.1',plain,[-(aSubsetOf0(xS, xS)), aSet0(xS)],extension(250 ^ 5,bind([[_77955], [xS]]))).
% 4.00/4.48 ncf('1.2.1.1.1.1.1',plain,[-(aSet0(xS))],extension(434 ^ 6)).
% 4.00/4.48 ncf('1.2.1.1.1.2',plain,[-(xS = xS)],extension(2 ^ 5,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.2.1.1.1.3',plain,[-(xS = xS)],extension(2 ^ 5,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.2.1.1.2',plain,[-(xS = xS)],extension(2 ^ 4,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.2.1.1.3',plain,[-(xS = xS)],extension(2 ^ 4,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.2.1.2',plain,[-(xS = xS)],extension(2 ^ 3,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.2.1.3',plain,[-(xS = xS)],extension(2 ^ 3,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.2.2',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([[_79232, _79234, _80493], [xx, sdtmndt0(xS, xx), xS]]))).
% 4.00/4.48 ncf('1.2.2.1',plain,[-(aSet0(xS))],extension(434 ^ 5)).
% 4.00/4.48 ncf('1.2.2.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([[_74323, _74453], [xS, 339 ^ [xx, sdtmndt0(xS, xx), xS]]]))).
% 4.00/4.48 ncf('1.2.2.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([[_81530, _81532, _81813, _82414], [xx, xS, sdtmndt0(xS, xx), 339 ^ [xx, sdtmndt0(xS, xx), xS]]]))).
% 4.00/4.48 ncf('1.2.2.2.1.1',plain,[aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], sdtmndt0(xS, xx)), aElement0(339 ^ [xx, sdtmndt0(xS, xx), xS])],extension(345 ^ 15)).
% 4.00/4.48 ncf('1.2.2.2.1.1.1',plain,[-(aElement0(339 ^ [xx, sdtmndt0(xS, xx), xS]))],reduction('1.2.2.2')).
% 4.00/4.48 ncf('1.2.2.2.1.2',plain,[-(aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], xS))],reduction('1.2.2')).
% 4.00/4.48 ncf('1.2.2.2.1.3',plain,[339 ^ [xx, sdtmndt0(xS, xx), xS] = xx, aElement0(339 ^ [xx, sdtmndt0(xS, xx), xS])],extension(345 ^ 15)).
% 4.00/4.48 ncf('1.2.2.2.1.3.1',plain,[-(aElement0(339 ^ [xx, sdtmndt0(xS, xx), xS]))],reduction('1.2.2.2')).
% 4.00/4.48 ncf('1.2.2.2.1.4',plain,[-(sdtmndt0(xS, xx) = sdtmndt0(xS, xx))],extension(2 ^ 13,bind([[_70435], [sdtmndt0(xS, xx)]]))).
% 4.00/4.48 ncf('1.2.2.2.1.5',plain,[-(aSet0(xS))],lemmata('[2, 1].x')).
% 4.00/4.48 ncf('1.2.2.2.1.6',plain,[-(aElement0(xx)), aElementOf0(xx, xS)],extension(132 ^ 11,bind([[_74453], [xx]]))).
% 4.00/4.48 ncf('1.2.2.2.1.6.1',plain,[-(aElementOf0(xx, xS))],extension(436 ^ 12)).
% 4.00/4.48 ncf('1.2.2.2.2',plain,[-(aSet0(xS))],lemmata('[2, 1].x')).
% 4.00/4.48 ncf('1.2.2.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([[_81530, _81532, _81813, _82078], [xx, xS, sdtmndt0(xS, xx), 339 ^ [xx, sdtmndt0(xS, xx), xS]]]))).
% 4.00/4.48 ncf('1.2.2.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(60 ^ 14,bind([[_72267, _72269, _72271, _72273], [xS, xS, 339 ^ [xx, sdtmndt0(xS, xx), xS], 339 ^ [xx, sdtmndt0(xS, xx), xS]]]))).
% 4.00/4.48 ncf('1.2.2.3.1.1',plain,[aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], xS)],extension(361 ^ 15)).
% 4.00/4.48 ncf('1.2.2.3.1.2',plain,[-(339 ^ [xx, sdtmndt0(xS, xx), xS] = 339 ^ [xx, sdtmndt0(xS, xx), xS])],extension(2 ^ 15,bind([[_70435], [339 ^ [xx, sdtmndt0(xS, xx), xS]]]))).
% 4.00/4.48 ncf('1.2.2.3.1.3',plain,[-(xS = xS)],extension(2 ^ 15,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.2.2.3.2',plain,[-(sdtmndt0(xS, xx) = sdtmndt0(xS, xx)), xS = xS, xx = xx],extension(98 ^ 10,bind([[_73490, _73492, _73494, _73496], [xx, xx, xS, xS]]))).
% 4.00/4.48 ncf('1.2.2.3.2.1',plain,[-(xS = xS)],extension(2 ^ 11,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.2.2.3.2.2',plain,[-(xx = xx)],extension(2 ^ 11,bind([[_70435], [xx]]))).
% 4.00/4.48 ncf('1.2.2.3.3',plain,[-(aSet0(xS))],lemmata('[2, 1].x')).
% 4.00/4.48 ncf('1.2.2.3.4',plain,[-(aElement0(xx)), 132 : aElementOf0(xx, xS), 132 : aSet0(xS)],extension(128 ^ 8,bind([[_74323, _74453], [xS, xx]]))).
% 4.00/4.48 ncf('1.2.2.3.4.1',plain,[-(aElementOf0(xx, xS))],extension(436 ^ 11)).
% 4.00/4.48 ncf('1.2.2.3.4.2',plain,[-(aSet0(xS))],lemmata('[2, 2, 1].x')).
% 4.00/4.48 ncf('1.2.2.4',plain,[339 ^ [xx, sdtmndt0(xS, xx), xS] = xx, -(xx = 339 ^ [xx, sdtmndt0(xS, xx), xS])],extension(4 ^ 7,bind([[_70542, _70544], [xx, 339 ^ [xx, sdtmndt0(xS, xx), xS]]]))).
% 4.00/4.48 ncf('1.2.2.4.1',plain,[xx = 339 ^ [xx, sdtmndt0(xS, xx), xS], -(aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], xS)), aElementOf0(xx, xS), xS = xS],extension(60 ^ 8,bind([[_72267, _72269, _72271, _72273], [xS, xS, 339 ^ [xx, sdtmndt0(xS, xx), xS], xx]]))).
% 4.00/4.48 ncf('1.2.2.4.1.1',plain,[aElementOf0(339 ^ [xx, sdtmndt0(xS, xx), xS], xS)],extension(361 ^ 9)).
% 4.00/4.48 ncf('1.2.2.4.1.2',plain,[-(aElementOf0(xx, xS))],extension(436 ^ 9)).
% 4.00/4.48 ncf('1.2.2.4.1.3',plain,[-(xS = xS)],extension(2 ^ 9,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.2.2.5',plain,[-(aSet0(sdtmndt0(xS, xx))), 373 : sdtmndt0(xS, xx) = sdtmndt0(xS, xx), 373 : aSet0(xS), 373 : aElement0(xx)],extension(365 ^ 3,bind([[_81530, _81532, _81813], [xx, xS, sdtmndt0(xS, xx)]]))).
% 4.00/4.48 ncf('1.2.2.5.1',plain,[-(sdtmndt0(xS, xx) = sdtmndt0(xS, xx)), xS = xS, xx = xx],extension(98 ^ 6,bind([[_73490, _73492, _73494, _73496], [xx, xx, xS, xS]]))).
% 4.00/4.48 ncf('1.2.2.5.1.1',plain,[-(xS = xS)],extension(2 ^ 7,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.2.2.5.1.2',plain,[-(xx = xx)],extension(2 ^ 7,bind([[_70435], [xx]]))).
% 4.00/4.48 ncf('1.2.2.5.2',plain,[-(aSet0(xS))],extension(434 ^ 4)).
% 4.00/4.48 ncf('1.2.2.5.3',plain,[-(aElement0(xx)), 132 : aElementOf0(xx, xS), 132 : aSet0(xS)],extension(128 ^ 4,bind([[_74323, _74453], [xS, xx]]))).
% 4.00/4.48 ncf('1.2.2.5.3.1',plain,[-(aElementOf0(xx, xS))],extension(436 ^ 7)).
% 4.00/4.48 ncf('1.2.2.5.3.2',plain,[-(aSet0(xS))],lemmata('[2, 2, 1].x')).
% 4.00/4.48 ncf('1.2.2.6',plain,[-(aElement0(xx)), 132 : aElementOf0(xx, xS), 132 : aSet0(xS)],extension(128 ^ 3,bind([[_74323, _74453], [xS, xx]]))).
% 4.00/4.48 ncf('1.2.2.6.1',plain,[-(aElementOf0(xx, xS)), aElementOf0(xx, xS), xx = xx, xS = xS],extension(60 ^ 6,bind([[_72267, _72269, _72271, _72273], [xS, xS, xx, xx]]))).
% 4.00/4.48 ncf('1.2.2.6.1.1',plain,[-(aElementOf0(xx, xS))],extension(436 ^ 7)).
% 4.00/4.48 ncf('1.2.2.6.1.2',plain,[-(xx = xx)],extension(2 ^ 7,bind([[_70435], [xx]]))).
% 4.00/4.48 ncf('1.2.2.6.1.3',plain,[-(xS = xS)],extension(2 ^ 7,bind([[_70435], [xS]]))).
% 4.00/4.48 ncf('1.2.2.6.2',plain,[-(aSet0(xS))],extension(434 ^ 4)).
% 4.00/4.48 ncf('1.2.3',plain,[-(xS = xS)],extension(2 ^ 2,bind([[_70435], [xS]]))).
% 4.00/4.48 %-----------------------------------------------------
% 4.00/4.48 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------