%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM539+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n001.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:56 EDT 2023
% Result : Theorem 103.67s 100.56s
% Output : Proof 103.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM539+1 : TPTP v8.1.2. Released v4.0.0.
% 0.13/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n001.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 18 17:55:04 EDT 2023
% 0.13/0.33 % CPUTime :
% 103.67/100.56
% 103.67/100.56 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 103.67/100.56 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 103.67/100.56 %-----------------------------------------------------
% 103.67/100.56 ncf(matrix, plain, [(940 ^ _111031) ^ [] : [szmzizndt0(xS) = szmzizndt0(xT)], (116 ^ _111031) ^ [_114783, _114785, _114787, _114789] : [-(sdtpldt0(_114789, _114785) = sdtpldt0(_114787, _114783)), _114789 = _114787, _114785 = _114783], (126 ^ _111031) ^ [_115114, _115116] : [_115116 = _115114, -(szszuzczcdt0(_115116) = szszuzczcdt0(_115114))], (132 ^ _111031) ^ [_115360, _115362, _115364, _115366] : [-(sdtmndt0(_115366, _115362) = sdtmndt0(_115364, _115360)), _115366 = _115364, _115362 = _115360], (142 ^ _111031) ^ [_115691, _115693] : [_115693 = _115691, -(sbrdtbr0(_115693) = sbrdtbr0(_115691))], (148 ^ _111031) ^ [_115909, _115911] : [_115911 = _115909, -(szmzazxdt0(_115911) = szmzazxdt0(_115909))], (154 ^ _111031) ^ [_116107, _116109] : [_116109 = _116107, -(szmzizndt0(_116109) = szmzizndt0(_116107))], (2 ^ _111031) ^ [_111175] : [-(_111175 = _111175)], (4 ^ _111031) ^ [_111282, _111284] : [_111284 = _111282, -(_111282 = _111284)], (10 ^ _111031) ^ [_111486, _111488, _111490] : [-(_111490 = _111486), _111490 = _111488, _111488 = _111486], (20 ^ _111031) ^ [_111799, _111801] : [-(isCountable0(_111799)), _111801 = _111799, isCountable0(_111801)], (30 ^ _111031) ^ [_112122, _112124, _112126, _112128] : [-(iLess0(_112126, _112122)), iLess0(_112128, _112124), _112128 = _112126, _112124 = _112122], (44 ^ _111031) ^ [_112538, _112540] : [-(aElement0(_112538)), _112540 = _112538, aElement0(_112540)], (54 ^ _111031) ^ [_112833, _112835] : [-(aSet0(_112833)), _112835 = _112833, aSet0(_112835)], (64 ^ _111031) ^ [_113128, _113130] : [-(isFinite0(_113128)), _113130 = _113128, isFinite0(_113130)], (74 ^ _111031) ^ [_113451, _113453, _113455, _113457] : [-(sdtlseqdt0(_113455, _113451)), sdtlseqdt0(_113457, _113453), _113457 = _113455, _113453 = _113451], (88 ^ _111031) ^ [_113895, _113897, _113899, _113901] : [-(aSubsetOf0(_113899, _113895)), aSubsetOf0(_113901, _113897), _113901 = _113899, _113897 = _113895], (102 ^ _111031) ^ [_114319, _114321, _114323, _114325] : [-(aElementOf0(_114323, _114319)), aElementOf0(_114325, _114321), _114325 = _114323, _114321 = _114319], (160 ^ _111031) ^ [_116333] : [aSet0(_116333), true___, -(true___)], (170 ^ _111031) ^ [_116588] : [aElement0(_116588), true___, -(true___)], (180 ^ _111031) ^ [_116843] : [aSet0(_116843), 183 ^ _111031 : [(184 ^ _111031) ^ [_116973] : [aElementOf0(_116973, _116843), -(aElement0(_116973))]]], (190 ^ _111031) ^ [_117174] : [aSet0(_117174), isFinite0(_117174), true___, -(true___)], (204 ^ _111031) ^ [_117544] : [_117544 = slcrc0, 207 ^ _111031 : [(208 ^ _111031) ^ [] : [-(aSet0(_117544))], (210 ^ _111031) ^ [_117725] : [aElementOf0(_117725, _117544)]]], (212 ^ _111031) ^ [_117793] : [-(_117793 = slcrc0), aSet0(_117793), -(aElementOf0(217 ^ [_117793], _117793))], (223 ^ _111031) ^ [] : [-(isFinite0(slcrc0))], (225 ^ _111031) ^ [_118175] : [aSet0(_118175), isCountable0(_118175), true___, -(true___)], (239 ^ _111031) ^ [_118516] : [isFinite0(_118516), aSet0(_118516), isCountable0(_118516)], (249 ^ _111031) ^ [_118786] : [_118786 = slcrc0, aSet0(_118786), isCountable0(_118786)], (259 ^ _111031) ^ [_119058] : [aSet0(_119058), 262 ^ _111031 : [(263 ^ _111031) ^ [_119234] : [aSubsetOf0(_119234, _119058), 266 ^ _111031 : [(267 ^ _111031) ^ [] : [-(aSet0(_119234))], (269 ^ _111031) ^ [_119443] : [aElementOf0(_119443, _119234), -(aElementOf0(_119443, _119058))]]], (275 ^ _111031) ^ [_119622] : [-(aSubsetOf0(_119622, _119058)), aSet0(_119622), 281 ^ _111031 : [(282 ^ _111031) ^ [] : [-(aElementOf0(280 ^ [_119058, _119622], _119622))], (284 ^ _111031) ^ [] : [aElementOf0(280 ^ [_119058, _119622], _119058)]]]]], (288 ^ _111031) ^ [_120059] : [aSet0(_120059), isFinite0(_120059), 295 ^ _111031 : [(296 ^ _111031) ^ [_120272] : [aSubsetOf0(_120272, _120059), -(isFinite0(_120272))]]], (302 ^ _111031) ^ [_120475] : [aSet0(_120475), -(aSubsetOf0(_120475, _120475))], (308 ^ _111031) ^ [_120677, _120679] : [aSet0(_120679), aSet0(_120677), -(_120679 = _120677), aSubsetOf0(_120679, _120677), aSubsetOf0(_120677, _120679)], (326 ^ _111031) ^ [_121166, _121168, _121170] : [aSet0(_121170), aSet0(_121168), aSet0(_121166), -(aSubsetOf0(_121170, _121166)), aSubsetOf0(_121170, _121168), aSubsetOf0(_121168, _121166)], (348 ^ _111031) ^ [_121752, _121754] : [aSet0(_121754), aElement0(_121752), 355 ^ _111031 : [(386 ^ _111031) ^ [_123013] : [-(_123013 = sdtpldt0(_121754, _121752)), aSet0(_123013), 394 ^ _111031 : [(395 ^ _111031) ^ [] : [-(aElementOf0(391 ^ [_121752, _121754, _123013], _123013))], (397 ^ _111031) ^ [] : [aElement0(391 ^ [_121752, _121754, _123013]), 400 ^ _111031 : [(401 ^ _111031) ^ [] : [aElementOf0(391 ^ [_121752, _121754, _123013], _121754)], (403 ^ _111031) ^ [] : [391 ^ [_121752, _121754, _123013] = _121752]]]], 404 ^ _111031 : [(413 ^ _111031) ^ [] : [aElementOf0(391 ^ [_121752, _121754, _123013], _123013)], (405 ^ _111031) ^ [] : [-(aElement0(391 ^ [_121752, _121754, _123013]))], (407 ^ _111031) ^ [] : [-(aElementOf0(391 ^ [_121752, _121754, _123013], _121754)), -(391 ^ [_121752, _121754, _123013] = _121752)]]], (356 ^ _111031) ^ [_122033] : [_122033 = sdtpldt0(_121754, _121752), 359 ^ _111031 : [(360 ^ _111031) ^ [] : [-(aSet0(_122033))], (362 ^ _111031) ^ [_122296] : [aElementOf0(_122296, _122033), 365 ^ _111031 : [(366 ^ _111031) ^ [] : [-(aElement0(_122296))], (368 ^ _111031) ^ [] : [-(aElementOf0(_122296, _121754)), -(_122296 = _121752)]]], (374 ^ _111031) ^ [_122651] : [-(aElementOf0(_122651, _122033)), aElement0(_122651), 379 ^ _111031 : [(380 ^ _111031) ^ [] : [aElementOf0(_122651, _121754)], (382 ^ _111031) ^ [] : [_122651 = _121752]]]]]]], (417 ^ _111031) ^ [_124050, _124052] : [aSet0(_124052), aElement0(_124050), 424 ^ _111031 : [(455 ^ _111031) ^ [_125318] : [-(_125318 = sdtmndt0(_124052, _124050)), aSet0(_125318), 475 ^ _111031 : [(476 ^ _111031) ^ [] : [-(aElement0(460 ^ [_124050, _124052, _125318]))], (478 ^ _111031) ^ [] : [-(aElementOf0(460 ^ [_124050, _124052, _125318], _124052))], (480 ^ _111031) ^ [] : [460 ^ [_124050, _124052, _125318] = _124050], (482 ^ _111031) ^ [] : [aElementOf0(460 ^ [_124050, _124052, _125318], _125318)]], 463 ^ _111031 : [(464 ^ _111031) ^ [] : [-(aElementOf0(460 ^ [_124050, _124052, _125318], _125318))], (466 ^ _111031) ^ [] : [aElement0(460 ^ [_124050, _124052, _125318]), aElementOf0(460 ^ [_124050, _124052, _125318], _124052), -(460 ^ [_124050, _124052, _125318] = _124050)]]], (425 ^ _111031) ^ [_124333] : [_124333 = sdtmndt0(_124052, _124050), 428 ^ _111031 : [(429 ^ _111031) ^ [] : [-(aSet0(_124333))], (431 ^ _111031) ^ [_124598] : [aElementOf0(_124598, _124333), 434 ^ _111031 : [(435 ^ _111031) ^ [] : [-(aElement0(_124598))], (437 ^ _111031) ^ [] : [-(aElementOf0(_124598, _124052))], (439 ^ _111031) ^ [] : [_124598 = _124050]]], (441 ^ _111031) ^ [_124934] : [-(aElementOf0(_124934, _124333)), aElement0(_124934), aElementOf0(_124934, _124052), -(_124934 = _124050)]]]]], (486 ^ _111031) ^ [_126348] : [aSet0(_126348), 489 ^ _111031 : [(490 ^ _111031) ^ [_126485] : [aElementOf0(_126485, _126348), -(sdtpldt0(sdtmndt0(_126348, _126485), _126485) = _126348)]]], (496 ^ _111031) ^ [_126714, _126716] : [aElement0(_126716), aSet0(_126714), -(aElementOf0(_126716, _126714)), -(sdtmndt0(sdtpldt0(_126714, _126716), _126716) = _126714)], (510 ^ _111031) ^ [_127101] : [aElement0(_127101), 513 ^ _111031 : [(514 ^ _111031) ^ [_127238] : [-(isCountable0(sdtpldt0(_127238, _127101))), aSet0(_127238), isCountable0(_127238)]]], (524 ^ _111031) ^ [_127530] : [aElement0(_127530), 527 ^ _111031 : [(528 ^ _111031) ^ [_127667] : [-(isCountable0(sdtmndt0(_127667, _127530))), aSet0(_127667), isCountable0(_127667)]]], (538 ^ _111031) ^ [_127959] : [aElement0(_127959), 541 ^ _111031 : [(542 ^ _111031) ^ [_128096] : [-(isFinite0(sdtpldt0(_128096, _127959))), aSet0(_128096), isFinite0(_128096)]]], (552 ^ _111031) ^ [_128388] : [aElement0(_128388), 555 ^ _111031 : [(556 ^ _111031) ^ [_128525] : [-(isFinite0(sdtmndt0(_128525, _128388))), aSet0(_128525), isFinite0(_128525)]]], (566 ^ _111031) ^ [] : [-(aSet0(szNzAzT0))], (568 ^ _111031) ^ [] : [-(isCountable0(szNzAzT0))], (570 ^ _111031) ^ [] : [-(aElementOf0(sz00, szNzAzT0))], (572 ^ _111031) ^ [_128978] : [aElementOf0(_128978, szNzAzT0), 575 ^ _111031 : [(576 ^ _111031) ^ [] : [-(aElementOf0(szszuzczcdt0(_128978), szNzAzT0))], (578 ^ _111031) ^ [] : [szszuzczcdt0(_128978) = sz00]]], (580 ^ _111031) ^ [_129264, _129266] : [aElementOf0(_129266, szNzAzT0), aElementOf0(_129264, szNzAzT0), szszuzczcdt0(_129266) = szszuzczcdt0(_129264), -(_129266 = _129264)], (594 ^ _111031) ^ [_129648] : [aElementOf0(_129648, szNzAzT0), -(_129648 = sz00), 602 ^ _111031 : [(603 ^ _111031) ^ [] : [-(aElementOf0(601 ^ [_129648], szNzAzT0))], (605 ^ _111031) ^ [] : [-(_129648 = szszuzczcdt0(601 ^ [_129648]))]]], (607 ^ _111031) ^ [_130065] : [aElementOf0(_130065, szNzAzT0), _130065 = szszuzczcdt0(_130065)], (613 ^ _111031) ^ [_130274, _130276] : [aElementOf0(_130276, szNzAzT0), aElementOf0(_130274, szNzAzT0), sdtlseqdt0(_130276, _130274), true___, -(true___)], (631 ^ _111031) ^ [_130724] : [aElementOf0(_130724, szNzAzT0), -(sdtlseqdt0(sz00, _130724))], (637 ^ _111031) ^ [_130914] : [aElementOf0(_130914, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_130914), sz00)], (643 ^ _111031) ^ [_131123, _131125] : [aElementOf0(_131125, szNzAzT0), aElementOf0(_131123, szNzAzT0), 650 ^ _111031 : [(651 ^ _111031) ^ [] : [sdtlseqdt0(_131125, _131123), -(sdtlseqdt0(szszuzczcdt0(_131125), szszuzczcdt0(_131123)))], (657 ^ _111031) ^ [] : [sdtlseqdt0(szszuzczcdt0(_131125), szszuzczcdt0(_131123)), -(sdtlseqdt0(_131125, _131123))]]], (663 ^ _111031) ^ [_131672] : [aElementOf0(_131672, szNzAzT0), -(sdtlseqdt0(_131672, szszuzczcdt0(_131672)))], (669 ^ _111031) ^ [_131866] : [aElementOf0(_131866, szNzAzT0), -(sdtlseqdt0(_131866, _131866))], (675 ^ _111031) ^ [_132070, _132072] : [aElementOf0(_132072, szNzAzT0), aElementOf0(_132070, szNzAzT0), -(_132072 = _132070), sdtlseqdt0(_132072, _132070), sdtlseqdt0(_132070, _132072)], (693 ^ _111031) ^ [_132563, _132565, _132567] : [aElementOf0(_132567, szNzAzT0), aElementOf0(_132565, szNzAzT0), aElementOf0(_132563, szNzAzT0), -(sdtlseqdt0(_132567, _132563)), sdtlseqdt0(_132567, _132565), sdtlseqdt0(_132565, _132563)], (715 ^ _111031) ^ [_133155, _133157] : [aElementOf0(_133157, szNzAzT0), aElementOf0(_133155, szNzAzT0), -(sdtlseqdt0(_133157, _133155)), -(sdtlseqdt0(szszuzczcdt0(_133155), _133157))], (729 ^ _111031) ^ [_133550, _133552] : [aElementOf0(_133552, szNzAzT0), aElementOf0(_133550, szNzAzT0), iLess0(_133552, _133550), true___, -(true___)], (747 ^ _111031) ^ [_134000] : [aElementOf0(_134000, szNzAzT0), -(iLess0(_134000, szszuzczcdt0(_134000)))], (753 ^ _111031) ^ [_134194] : [aSet0(_134194), -(aElement0(sbrdtbr0(_134194)))], (759 ^ _111031) ^ [_134384] : [aSet0(_134384), 762 ^ _111031 : [(763 ^ _111031) ^ [] : [aElementOf0(sbrdtbr0(_134384), szNzAzT0), -(isFinite0(_134384))], (769 ^ _111031) ^ [] : [isFinite0(_134384), -(aElementOf0(sbrdtbr0(_134384), szNzAzT0))]]], (775 ^ _111031) ^ [_134815] : [aSet0(_134815), 778 ^ _111031 : [(779 ^ _111031) ^ [] : [sbrdtbr0(_134815) = sz00, -(_134815 = slcrc0)], (785 ^ _111031) ^ [] : [_134815 = slcrc0, -(sbrdtbr0(_134815) = sz00)]]], (791 ^ _111031) ^ [_135249] : [aSet0(_135249), isFinite0(_135249), 798 ^ _111031 : [(799 ^ _111031) ^ [_135479] : [aElement0(_135479), -(aElementOf0(_135479, _135249)), -(sbrdtbr0(sdtpldt0(_135249, _135479)) = szszuzczcdt0(sbrdtbr0(_135249)))]]], (809 ^ _111031) ^ [_135792] : [aSet0(_135792), 812 ^ _111031 : [(813 ^ _111031) ^ [_135937] : [-(szszuzczcdt0(sbrdtbr0(sdtmndt0(_135792, _135937))) = sbrdtbr0(_135792)), isFinite0(_135792), aElementOf0(_135937, _135792)]]], (823 ^ _111031) ^ [_136245] : [aSet0(_136245), 826 ^ _111031 : [(827 ^ _111031) ^ [_136385] : [-(sdtlseqdt0(sbrdtbr0(_136385), sbrdtbr0(_136245))), isFinite0(_136245), aSubsetOf0(_136385, _136245)]]], (837 ^ _111031) ^ [_136697, _136699] : [aSet0(_136699), aElementOf0(_136697, szNzAzT0), 853 ^ _111031 : [(854 ^ _111031) ^ [] : [-(aSubsetOf0(852 ^ [_136697, _136699], _136699))], (856 ^ _111031) ^ [] : [-(sbrdtbr0(852 ^ [_136697, _136699]) = _136697)]], isFinite0(_136699), sdtlseqdt0(_136697, sbrdtbr0(_136699))], (858 ^ _111031) ^ [_137313] : [aSubsetOf0(_137313, szNzAzT0), -(_137313 = slcrc0), 865 ^ _111031 : [(866 ^ _111031) ^ [_137582] : [_137582 = szmzizndt0(_137313), 869 ^ _111031 : [(870 ^ _111031) ^ [] : [-(aElementOf0(_137582, _137313))], (872 ^ _111031) ^ [_137797] : [aElementOf0(_137797, _137313), -(sdtlseqdt0(_137582, _137797))]]], (878 ^ _111031) ^ [_137976] : [-(_137976 = szmzizndt0(_137313)), aElementOf0(_137976, _137313), 884 ^ _111031 : [(885 ^ _111031) ^ [] : [-(aElementOf0(883 ^ [_137313, _137976], _137313))], (887 ^ _111031) ^ [] : [sdtlseqdt0(_137976, 883 ^ [_137313, _137976])]]]]], (928 ^ _111031) ^ [] : [-(aSubsetOf0(xS, szNzAzT0))], (930 ^ _111031) ^ [] : [-(aSubsetOf0(xT, szNzAzT0))], (932 ^ _111031) ^ [] : [xS = slcrc0], (934 ^ _111031) ^ [] : [xT = slcrc0], (936 ^ _111031) ^ [] : [-(aElementOf0(szmzizndt0(xS), xT))], (938 ^ _111031) ^ [] : [-(aElementOf0(szmzizndt0(xT), xS))], (891 ^ _111031) ^ [_138421] : [aSubsetOf0(_138421, szNzAzT0), isFinite0(_138421), -(_138421 = slcrc0), 902 ^ _111031 : [(903 ^ _111031) ^ [_138773] : [_138773 = szmzazxdt0(_138421), 906 ^ _111031 : [(907 ^ _111031) ^ [] : [-(aElementOf0(_138773, _138421))], (909 ^ _111031) ^ [_138988] : [aElementOf0(_138988, _138421), -(sdtlseqdt0(_138988, _138773))]]], (915 ^ _111031) ^ [_139167] : [-(_139167 = szmzazxdt0(_138421)), aElementOf0(_139167, _138421), 921 ^ _111031 : [(922 ^ _111031) ^ [] : [-(aElementOf0(920 ^ [_138421, _139167], _138421))], (924 ^ _111031) ^ [] : [sdtlseqdt0(920 ^ [_138421, _139167], _139167)]]]]]], input).
% 103.67/100.56 ncf('1',plain,[szmzizndt0(xS) = szmzizndt0(xT)],start(940 ^ 0)).
% 103.67/100.56 ncf('1.1',plain,[-(szmzizndt0(xS) = szmzizndt0(xT)), aElementOf0(szmzizndt0(xS), szNzAzT0), aElementOf0(szmzizndt0(xT), szNzAzT0), sdtlseqdt0(szmzizndt0(xS), szmzizndt0(xT)), sdtlseqdt0(szmzizndt0(xT), szmzizndt0(xS))],extension(675 ^ 1,bind([[_132070, _132072], [szmzizndt0(xT), szmzizndt0(xS)]]))).
% 103.67/100.56 ncf('1.1.1',plain,[-(aElementOf0(szmzizndt0(xS), szNzAzT0)), aElementOf0(szmzizndt0(xS), szNzAzT0), szmzizndt0(xS) = szmzizndt0(xS), szNzAzT0 = szNzAzT0],extension(102 ^ 2,bind([[_114319, _114321, _114323, _114325], [szNzAzT0, szNzAzT0, szmzizndt0(xS), szmzizndt0(xS)]]))).
% 103.67/100.56 ncf('1.1.1.1',plain,[-(aElementOf0(szmzizndt0(xS), szNzAzT0)), 269 : aElementOf0(szmzizndt0(xS), xT), 269 : aSubsetOf0(xT, szNzAzT0), 263 : aSet0(szNzAzT0)],extension(259 ^ 3,bind([[_119058, _119234, _119443], [szNzAzT0, xT, szmzizndt0(xS)]]))).
% 103.67/100.56 ncf('1.1.1.1.1',plain,[-(aElementOf0(szmzizndt0(xS), xT))],extension(936 ^ 8)).
% 103.67/100.56 ncf('1.1.1.1.2',plain,[-(aSubsetOf0(xT, szNzAzT0))],extension(930 ^ 6)).
% 103.67/100.56 ncf('1.1.1.1.3',plain,[-(aSet0(szNzAzT0))],extension(566 ^ 4)).
% 103.67/100.56 ncf('1.1.1.2',plain,[-(szmzizndt0(xS) = szmzizndt0(xS))],extension(2 ^ 3,bind([[_111175], [szmzizndt0(xS)]]))).
% 103.67/100.56 ncf('1.1.1.3',plain,[-(szNzAzT0 = szNzAzT0)],extension(2 ^ 3,bind([[_111175], [szNzAzT0]]))).
% 103.67/100.56 ncf('1.1.2',plain,[-(aElementOf0(szmzizndt0(xT), szNzAzT0)), aElementOf0(szmzizndt0(xT), szNzAzT0), szmzizndt0(xT) = szmzizndt0(xT), szNzAzT0 = szNzAzT0],extension(102 ^ 2,bind([[_114319, _114321, _114323, _114325], [szNzAzT0, szNzAzT0, szmzizndt0(xT), szmzizndt0(xT)]]))).
% 103.67/100.56 ncf('1.1.2.1',plain,[-(aElementOf0(szmzizndt0(xT), szNzAzT0)), 269 : aElementOf0(szmzizndt0(xT), xS), 269 : aSubsetOf0(xS, szNzAzT0), 263 : aSet0(szNzAzT0)],extension(259 ^ 3,bind([[_119058, _119234, _119443], [szNzAzT0, xS, szmzizndt0(xT)]]))).
% 103.67/100.56 ncf('1.1.2.1.1',plain,[-(aElementOf0(szmzizndt0(xT), xS))],extension(938 ^ 8)).
% 103.67/100.56 ncf('1.1.2.1.2',plain,[-(aSubsetOf0(xS, szNzAzT0))],extension(928 ^ 6)).
% 103.67/100.56 ncf('1.1.2.1.3',plain,[-(aSet0(szNzAzT0))],extension(566 ^ 4)).
% 103.67/100.56 ncf('1.1.2.2',plain,[-(szmzizndt0(xT) = szmzizndt0(xT))],extension(2 ^ 3,bind([[_111175], [szmzizndt0(xT)]]))).
% 103.67/100.56 ncf('1.1.2.3',plain,[-(szNzAzT0 = szNzAzT0)],extension(2 ^ 3,bind([[_111175], [szNzAzT0]]))).
% 103.67/100.56 ncf('1.1.3',plain,[-(sdtlseqdt0(szmzizndt0(xS), szmzizndt0(xT))), 872 : aElementOf0(szmzizndt0(xT), xS), 872 : szmzizndt0(xS) = szmzizndt0(xS), 866 : aSubsetOf0(xS, szNzAzT0), 866 : -(xS = slcrc0)],extension(858 ^ 2,bind([[_137313, _137582, _137797], [xS, szmzizndt0(xS), szmzizndt0(xT)]]))).
% 103.67/100.56 ncf('1.1.3.1',plain,[-(aElementOf0(szmzizndt0(xT), xS))],extension(938 ^ 7)).
% 103.67/100.56 ncf('1.1.3.2',plain,[-(szmzizndt0(xS) = szmzizndt0(xS))],extension(2 ^ 5,bind([[_111175], [szmzizndt0(xS)]]))).
% 103.67/100.56 ncf('1.1.3.3',plain,[-(aSubsetOf0(xS, szNzAzT0))],extension(928 ^ 3)).
% 103.67/100.56 ncf('1.1.3.4',plain,[xS = slcrc0, 210 : aElementOf0(szmzizndt0(xT), xS)],extension(204 ^ 3,bind([[_117544, _117725], [xS, szmzizndt0(xT)]]))).
% 103.67/100.56 ncf('1.1.3.4.1',plain,[-(aElementOf0(szmzizndt0(xT), xS))],extension(938 ^ 6)).
% 103.67/100.56 ncf('1.1.4',plain,[-(sdtlseqdt0(szmzizndt0(xT), szmzizndt0(xS))), 872 : aElementOf0(szmzizndt0(xS), xT), 872 : szmzizndt0(xT) = szmzizndt0(xT), 866 : aSubsetOf0(xT, szNzAzT0), 866 : -(xT = slcrc0)],extension(858 ^ 2,bind([[_137313, _137582, _137797], [xT, szmzizndt0(xT), szmzizndt0(xS)]]))).
% 103.67/100.56 ncf('1.1.4.1',plain,[-(aElementOf0(szmzizndt0(xS), xT))],extension(936 ^ 7)).
% 103.67/100.56 ncf('1.1.4.2',plain,[-(szmzizndt0(xT) = szmzizndt0(xT))],extension(2 ^ 5,bind([[_111175], [szmzizndt0(xT)]]))).
% 103.67/100.56 ncf('1.1.4.3',plain,[-(aSubsetOf0(xT, szNzAzT0))],extension(930 ^ 3)).
% 103.67/100.56 ncf('1.1.4.4',plain,[xT = slcrc0, 210 : aElementOf0(szmzizndt0(xS), xT)],extension(204 ^ 3,bind([[_117544, _117725], [xT, szmzizndt0(xS)]]))).
% 103.67/100.56 ncf('1.1.4.4.1',plain,[-(aElementOf0(szmzizndt0(xS), xT))],extension(936 ^ 6)).
% 103.67/100.56 %-----------------------------------------------------
% 103.67/100.56 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------