%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU439+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n029.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 12:04:38 EDT 2023
% Result : Theorem 58.69s 57.27s
% Output : Proof 58.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU439+1 : TPTP v8.1.2. Released v3.4.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n029.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 13:35:13 EDT 2023
% 0.12/0.33 % CPUTime :
% 58.69/57.27
% 58.69/57.27 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 58.69/57.27 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 58.69/57.27 %-----------------------------------------------------
% 58.69/57.27 ncf(matrix, plain, [(765 ^ _164198) ^ [] : [-(m1_subset_1(763 ^ [], k1_zfmisc_1(k2_zfmisc_1(758 ^ [], 759 ^ []))))], (767 ^ _164198) ^ [] : [760 ^ [] = k1_xboole_0], (769 ^ _164198) ^ [] : [r1_tarski(k8_relset_2(758 ^ [], 759 ^ [], 760 ^ [], 763 ^ []), k9_relat_1(763 ^ [], 760 ^ []))], (762 ^ _164198) ^ [] : [-(m1_subset_1(760 ^ [], k1_zfmisc_1(758 ^ [])))], !, (653 ^ _137232) ^ [_160124, _160126] : [-(r1_tarski(_160126, _160126))], (288 ^ _137232) ^ [_147196, _147198, _147200, _147202, _147204, _147206, _147208, _147210] : [-(k8_relset_2(_147210, _147206, _147202, _147198) = k8_relset_2(_147208, _147204, _147200, _147196)), _147210 = _147208, _147206 = _147204, _147202 = _147200, _147198 = _147196], (721 ^ _137232) ^ [_162545] : [v1_xboole_0(_162545), -(_162545 = k1_xboole_0)], (625 ^ _137232) ^ [_159081, _159083, _159085] : [m1_subset_1(_159081, k1_zfmisc_1(k2_zfmisc_1(_159083, _159085))), -(k6_relset_2(_159085, _159083, _159081) = k5_relset_2(_159083, _159081))], (336 ^ _137232) ^ [_148943] : [v1_relat_1(_148943), 339 ^ _137232 : [(340 ^ _137232) ^ [_149150, _149152] : [_149150 = k9_relat_1(_148943, _149152), 343 ^ _137232 : [(353 ^ _137232) ^ [_149696] : [-(r2_hidden(_149696, _149150)), 354 ^ _137232 : [(355 ^ _137232) ^ [_149801] : [r2_hidden(k4_tarski(_149801, _149696), _148943), r2_hidden(_149801, _149152)]]], (344 ^ _137232) ^ [_149342] : [r2_hidden(_149342, _149150), 348 ^ _137232 : [(351 ^ _137232) ^ [] : [-(r2_hidden(347 ^ [_148943, _149150, _149152, _149342], _149152))], (349 ^ _137232) ^ [] : [-(r2_hidden(k4_tarski(347 ^ [_148943, _149150, _149152, _149342], _149342), _148943))]]]]], (363 ^ _137232) ^ [_150056, _150058] : [-(_150056 = k9_relat_1(_148943, _150058)), 376 ^ _137232 : [(381 ^ _137232) ^ [] : [r2_hidden(364 ^ [_148943, _150056, _150058], _150056)], (379 ^ _137232) ^ [] : [-(r2_hidden(375 ^ [_148943, _150056, _150058], _150058))], (377 ^ _137232) ^ [] : [-(r2_hidden(k4_tarski(375 ^ [_148943, _150056, _150058], 364 ^ [_148943, _150056, _150058]), _148943))]], 367 ^ _137232 : [(370 ^ _137232) ^ [_150360] : [r2_hidden(k4_tarski(_150360, 364 ^ [_148943, _150056, _150058]), _148943), r2_hidden(_150360, _150058)], (368 ^ _137232) ^ [] : [-(r2_hidden(364 ^ [_148943, _150056, _150058], _150056))]]]]], (661 ^ _137232) ^ [_160471, _160473, _160475, _160477] : [m1_subset_1(_160471, k1_zfmisc_1(_160477)), 664 ^ _137232 : [(665 ^ _137232) ^ [_160652] : [m1_subset_1(_160652, k1_zfmisc_1(k2_zfmisc_1(_160477, _160475))), r2_hidden(_160473, k8_relset_2(_160477, _160475, _160471, _160652)), 672 ^ _137232 : [(673 ^ _137232) ^ [_160931] : [r2_hidden(_160931, _160471), -(r2_hidden(_160473, k9_relat_1(_160652, k1_tarski(_160931))))]]]]], (459 ^ _137232) ^ [_153273] : [-(m1_eqrel_1(k3_pua2mss1(_153273), _153273))], (555 ^ _137232) ^ [] : [-(v1_xboole_0(k1_xboole_0))], (427 ^ _137232) ^ [_152587, _152589] : [-(k4_tarski(_152589, _152587) = k2_tarski(k2_tarski(_152589, _152587), k1_tarski(_152589)))], (607 ^ _137232) ^ [] : [-(v1_relat_1(603 ^ []))], (617 ^ _137232) ^ [] : [-(v3_relat_1(613 ^ []))], (491 ^ _137232) ^ [] : [true___, -(true___)], (631 ^ _137232) ^ [_159349, _159351, _159353, _159355] : [-(k8_relset_2(_159355, _159353, _159351, _159349) = k7_relset_2(_159355, _159353, _159351, _159349)), m1_subset_1(_159351, k1_zfmisc_1(_159355)), m1_subset_1(_159349, k1_zfmisc_1(k2_zfmisc_1(_159355, _159353)))], (391 ^ _137232) ^ [_151170] : [-(r2_hidden(392 ^ [_151170], _151170)), -(_151170 = k1_xboole_0)], (695 ^ _137232) ^ [_161692, _161694] : [r1_tarski(_161694, _161692), -(m1_subset_1(_161694, k1_zfmisc_1(_161692)))], (228 ^ _137232) ^ [_144938, _144940, _144942, _144944] : [-(k5_relset_2(_144944, _144940) = k5_relset_2(_144942, _144938)), _144944 = _144942, _144940 = _144938], (256 ^ _137232) ^ [_145958, _145960] : [_145960 = _145958, -(k1_tarski(_145960) = k1_tarski(_145958))], (507 ^ _137232) ^ [_155003, _155005] : [m1_subset_1(_155003, k1_zfmisc_1(k1_zfmisc_1(_155005))), -(m1_subset_1(k8_setfam_1(_155005, _155003), k1_zfmisc_1(_155005)))], (176 ^ _137232) ^ [_143015, _143017, _143019, _143021] : [-(k8_setfam_1(_143021, _143017) = k8_setfam_1(_143019, _143015)), _143021 = _143019, _143017 = _143015], (2 ^ _137232) ^ [_137356] : [-(_137356 = _137356)], (612 ^ _137232) ^ [_158525] : [-(v1_xboole_0(608 ^ [_158525]))], (90 ^ _137232) ^ [_140288, _140290, _140292, _140294, _140296, _140298] : [-(m1_relset_1(_140296, _140292, _140288)), m1_relset_1(_140298, _140294, _140290), _140298 = _140296, _140294 = _140292, _140290 = _140288], (544 ^ _137232) ^ [_156058] : [-(m1_eqrel_1(542 ^ [_156058], _156058))], (429 ^ _137232) ^ [] : [true___, -(true___)], (186 ^ _137232) ^ [_143374, _143376, _143378, _143380] : [-(k2_tarski(_143380, _143376) = k2_tarski(_143378, _143374)), _143380 = _143378, _143376 = _143374], (334 ^ _137232) ^ [_148842, _148844] : [-(k2_tarski(_148844, _148842) = k2_tarski(_148842, _148844))], (655 ^ _137232) ^ [_160233, _160235] : [r2_hidden(_160235, _160233), -(m1_subset_1(_160235, _160233))], (619 ^ _137232) ^ [_158815, _158817, _158819, _158821] : [m1_subset_1(_158817, k1_zfmisc_1(k2_zfmisc_1(_158821, k1_zfmisc_1(_158819)))), -(k4_relset_2(_158821, _158819, _158817, _158815) = k9_relat_1(_158817, _158815))], (447 ^ _137232) ^ [] : [true___, -(true___)], (711 ^ _137232) ^ [_162249, _162251, _162253] : [r2_hidden(_162253, _162251), m1_subset_1(_162251, k1_zfmisc_1(_162249)), v1_xboole_0(_162249)], (600 ^ _137232) ^ [_158116, _158118] : [-(v1_relat_1(596 ^ [_158116, _158118]))], (689 ^ _137232) ^ [_161526, _161528] : [m1_subset_1(_161528, k1_zfmisc_1(_161526)), -(r1_tarski(_161528, _161526))], (647 ^ _137232) ^ [_159917, _159919, _159921] : [m1_relset_1(_159917, _159921, _159919), -(m2_relset_1(_159917, _159921, _159919))], (559 ^ _137232) ^ [] : [-(v3_relat_1(k1_xboole_0))], (453 ^ _137232) ^ [] : [true___, -(true___)], (385 ^ _137232) ^ [_150991] : [_150991 = k1_xboole_0, 388 ^ _137232 : [(389 ^ _137232) ^ [_151104] : [r2_hidden(_151104, _150991)]]], (537 ^ _137232) ^ [_155820, _155822, _155824] : [m2_relset_1(_155820, _155824, _155822), -(m1_subset_1(_155820, k1_zfmisc_1(k2_zfmisc_1(_155824, _155822))))], (598 ^ _137232) ^ [_158042, _158044] : [-(m1_relset_1(596 ^ [_158042, _158044], _158044, _158042))], (278 ^ _137232) ^ [_146781, _146783, _146785, _146787] : [-(k2_zfmisc_1(_146787, _146783) = k2_zfmisc_1(_146785, _146781)), _146787 = _146785, _146783 = _146781], (605 ^ _137232) ^ [] : [v1_xboole_0(603 ^ [])], (679 ^ _137232) ^ [_161199, _161201] : [m1_subset_1(_161201, _161199), -(v1_xboole_0(_161199)), -(r2_hidden(_161201, _161199))], (588 ^ _137232) ^ [_157639] : [-(v1_xboole_0(_157639)), 592 ^ _137232 : [(595 ^ _137232) ^ [] : [v1_xboole_0(591 ^ [_157639])], (593 ^ _137232) ^ [] : [-(m1_subset_1(591 ^ [_157639], k1_zfmisc_1(_157639)))]]], (322 ^ _137232) ^ [_148419] : [v1_xboole_0(_148419), -(v1_relat_1(_148419))], (408 ^ _137232) ^ [_151775, _151777] : [410 ^ _137232 : [(413 ^ _137232) ^ [] : [r2_hidden(409 ^ [_151775, _151777], _151775)], (411 ^ _137232) ^ [] : [-(r2_hidden(409 ^ [_151775, _151777], _151777))]], -(r1_tarski(_151777, _151775))], (513 ^ _137232) ^ [] : [true___, -(true___)], (550 ^ _137232) ^ [_156324] : [-(m1_subset_1(548 ^ [_156324], _156324))], (72 ^ _137232) ^ [_139679, _139681, _139683, _139685, _139687, _139689] : [-(m2_relset_1(_139687, _139683, _139679)), m2_relset_1(_139689, _139685, _139681), _139689 = _139687, _139685 = _139683, _139681 = _139679], (547 ^ _137232) ^ [_156197, _156199] : [-(m1_relset_1(545 ^ [_156197, _156199], _156199, _156197))], (733 ^ _137232) ^ [_162954, _162956] : [v1_xboole_0(_162956), -(_162956 = _162954), v1_xboole_0(_162954)], (262 ^ _137232) ^ [_146204, _146206, _146208, _146210] : [-(k4_tarski(_146210, _146206) = k4_tarski(_146208, _146204)), _146210 = _146208, _146206 = _146204], (38 ^ _137232) ^ [_138617, _138619, _138621, _138623] : [-(m1_eqrel_1(_138621, _138617)), m1_eqrel_1(_138623, _138619), _138623 = _138621, _138619 = _138617], (641 ^ _137232) ^ [_159745, _159747, _159749] : [m2_relset_1(_159745, _159749, _159747), -(m1_relset_1(_159745, _159749, _159747))], (519 ^ _137232) ^ [_155350, _155352] : [m1_eqrel_1(_155350, _155352), -(m1_subset_1(_155350, k1_zfmisc_1(k1_zfmisc_1(_155352))))], (569 ^ _137232) ^ [] : [-(v1_xboole_0(k1_xboole_0))], (567 ^ _137232) ^ [_156979, _156981] : [v1_xboole_0(k2_tarski(_156981, _156979))], (20 ^ _137232) ^ [_138036, _138038, _138040, _138042, _138044, _138046] : [-(v1_funct_2(_138044, _138040, _138036)), v1_funct_2(_138046, _138042, _138038), _138046 = _138044, _138042 = _138040, _138038 = _138036], (701 ^ _137232) ^ [_161922, _161924, _161926] : [-(m1_subset_1(_161926, _161922)), r2_hidden(_161926, _161924), m1_subset_1(_161924, k1_zfmisc_1(_161922))], (10 ^ _137232) ^ [_137667, _137669, _137671] : [-(_137671 = _137667), _137671 = _137669, _137669 = _137667], (4 ^ _137232) ^ [_137463, _137465] : [_137465 = _137463, -(_137463 = _137465)], (417 ^ _137232) ^ [_152146, _152148, _152150] : [m1_subset_1(_152146, k1_zfmisc_1(_152150)), 420 ^ _137232 : [(421 ^ _137232) ^ [_152317] : [m1_subset_1(_152317, k1_zfmisc_1(k2_zfmisc_1(_152150, _152148))), -(k7_relset_2(_152150, _152148, _152146, _152317) = k8_setfam_1(_152148, k4_relset_2(k1_zfmisc_1(_152150), _152148, k6_relset_2(_152148, _152150, _152317), k3_pua2mss1(_152146))))]]], (615 ^ _137232) ^ [] : [-(v1_relat_1(613 ^ []))], (118 ^ _137232) ^ [_141136, _141138] : [-(v1_relat_1(_141136)), _141138 = _141136, v1_relat_1(_141138)], (531 ^ _137232) ^ [] : [true___, -(true___)], (272 ^ _137232) ^ [_146535, _146537] : [_146537 = _146535, -(k1_zfmisc_1(_146537) = k1_zfmisc_1(_146535))], (142 ^ _137232) ^ [_141903, _141905, _141907, _141909] : [-(m1_subset_1(_141907, _141903)), m1_subset_1(_141909, _141905), _141909 = _141907, _141905 = _141903], (481 ^ _137232) ^ [_154088, _154090, _154092] : [m1_subset_1(_154088, k1_zfmisc_1(k2_zfmisc_1(_154090, _154092))), 484 ^ _137232 : [(489 ^ _137232) ^ [] : [-(m2_relset_1(k6_relset_2(_154092, _154090, _154088), k1_zfmisc_1(_154090), k1_zfmisc_1(_154092)))], (487 ^ _137232) ^ [] : [-(v1_funct_2(k6_relset_2(_154092, _154090, _154088), k1_zfmisc_1(_154090), k1_zfmisc_1(_154092)))], (485 ^ _137232) ^ [] : [-(v1_funct_1(k6_relset_2(_154092, _154090, _154088)))]]], (561 ^ _137232) ^ [_156713] : [v1_xboole_0(k1_zfmisc_1(_156713))], (573 ^ _137232) ^ [_157198, _157200] : [v1_xboole_0(k2_zfmisc_1(_157200, _157198)), -(v1_xboole_0(_157200)), -(v1_xboole_0(_157198))], (461 ^ _137232) ^ [_153410, _153412, _153414, _153416] : [m1_subset_1(_153412, k1_zfmisc_1(k2_zfmisc_1(_153416, k1_zfmisc_1(_153414)))), -(m1_subset_1(k4_relset_2(_153416, _153414, _153412, _153410), k1_zfmisc_1(k1_zfmisc_1(_153414))))], (610 ^ _137232) ^ [_158474] : [-(m1_subset_1(608 ^ [_158474], k1_zfmisc_1(_158474)))], (497 ^ _137232) ^ [_154656, _154658, _154660, _154662] : [-(m1_subset_1(k8_relset_2(_154662, _154660, _154658, _154656), k1_zfmisc_1(_154660))), m1_subset_1(_154658, k1_zfmisc_1(_154662)), m1_subset_1(_154656, k1_zfmisc_1(k2_zfmisc_1(_154662, _154660)))], (553 ^ _137232) ^ [_156463, _156465] : [-(m2_relset_1(551 ^ [_156463, _156465], _156465, _156463))], (473 ^ _137232) ^ [_153783, _153785] : [v1_relat_1(_153783), 476 ^ _137232 : [(479 ^ _137232) ^ [] : [-(v1_funct_1(k5_relset_2(_153785, _153783)))], (477 ^ _137232) ^ [] : [-(v1_relat_1(k5_relset_2(_153785, _153783)))]]], (328 ^ _137232) ^ [_148633, _148635, _148637] : [m1_subset_1(_148633, k1_zfmisc_1(k2_zfmisc_1(_148637, _148635))), -(v1_relat_1(_148633))], (196 ^ _137232) ^ [_143789, _143791, _143793, _143795, _143797, _143799, _143801, _143803] : [-(k4_relset_2(_143803, _143799, _143795, _143791) = k4_relset_2(_143801, _143797, _143793, _143789)), _143803 = _143801, _143799 = _143797, _143795 = _143793, _143791 = _143789], (584 ^ _137232) ^ [] : [-(v1_xboole_0(582 ^ []))], (565 ^ _137232) ^ [_156887] : [v1_xboole_0(k1_tarski(_156887))], (108 ^ _137232) ^ [_140841, _140843] : [-(v1_xboole_0(_140841)), _140843 = _140841, v1_xboole_0(_140843)], (170 ^ _137232) ^ [_142769, _142771] : [_142771 = _142769, -(k3_pua2mss1(_142771) = k3_pua2mss1(_142769))], (214 ^ _137232) ^ [_144450, _144452, _144454, _144456, _144458, _144460] : [-(k6_relset_2(_144460, _144456, _144452) = k6_relset_2(_144458, _144454, _144450)), _144460 = _144458, _144456 = _144454, _144452 = _144450], (467 ^ _137232) ^ [] : [true___, -(true___)], (586 ^ _137232) ^ [] : [-(v1_relat_1(582 ^ []))], (398 ^ _137232) ^ [_151461, _151463] : [r1_tarski(_151463, _151461), 401 ^ _137232 : [(402 ^ _137232) ^ [_151598] : [r2_hidden(_151598, _151463), -(r2_hidden(_151598, _151461))]]], (156 ^ _137232) ^ [_142327, _142329, _142331, _142333] : [-(r1_tarski(_142331, _142327)), r1_tarski(_142333, _142329), _142333 = _142331, _142329 = _142327], (306 ^ _137232) ^ [_147809, _147811, _147813, _147815] : [-(k9_relat_1(_147815, _147811) = k9_relat_1(_147813, _147809)), _147815 = _147813, _147811 = _147809], (563 ^ _137232) ^ [_156806, _156808] : [-(v1_relat_1(k2_zfmisc_1(_156808, _156806)))], (52 ^ _137232) ^ [_139033, _139035] : [-(v1_funct_1(_139033)), _139035 = _139033, v1_funct_1(_139035)], (238 ^ _137232) ^ [_145353, _145355, _145357, _145359, _145361, _145363, _145365, _145367] : [-(k7_relset_2(_145367, _145363, _145359, _145355) = k7_relset_2(_145365, _145361, _145357, _145353)), _145367 = _145365, _145363 = _145361, _145359 = _145357, _145355 = _145353], (316 ^ _137232) ^ [_148222, _148224] : [r2_hidden(_148224, _148222), r2_hidden(_148222, _148224)], (743 ^ _137232) ^ [_163245, _163247, _163249] : [v1_relat_1(_163245), 746 ^ _137232 : [(753 ^ _137232) ^ [] : [r2_hidden(k4_tarski(_163247, _163249), _163245), -(r2_hidden(_163249, k9_relat_1(_163245, k1_tarski(_163247))))], (747 ^ _137232) ^ [] : [r2_hidden(_163249, k9_relat_1(_163245, k1_tarski(_163247))), -(r2_hidden(k4_tarski(_163247, _163249), _163245))]]], (727 ^ _137232) ^ [_162747, _162749] : [r2_hidden(_162749, _162747), v1_xboole_0(_162747)], (571 ^ _137232) ^ [] : [-(v1_relat_1(k1_xboole_0))], (441 ^ _137232) ^ [] : [true___, -(true___)], (435 ^ _137232) ^ [] : [true___, -(true___)], (62 ^ _137232) ^ [_139328, _139330] : [-(v3_relat_1(_139328)), _139330 = _139328, v3_relat_1(_139330)], (525 ^ _137232) ^ [] : [true___, -(true___)], (557 ^ _137232) ^ [] : [-(v1_relat_1(k1_xboole_0))], (602 ^ _137232) ^ [_158168, _158170] : [-(v1_funct_1(596 ^ [_158168, _158170]))], (128 ^ _137232) ^ [_141459, _141461, _141463, _141465] : [-(r2_hidden(_141463, _141459)), r2_hidden(_141465, _141461), _141465 = _141463, _141461 = _141459]], input).
% 58.69/57.27 ncf('1',plain,[-(m1_subset_1(763 ^ [], k1_zfmisc_1(k2_zfmisc_1(758 ^ [], 759 ^ []))))],start(765 ^ 0)).
% 58.69/57.27 ncf('1.1',plain,[m1_subset_1(763 ^ [], k1_zfmisc_1(k2_zfmisc_1(758 ^ [], 759 ^ []))), -(v1_relat_1(763 ^ []))],extension(328 ^ 1,bind([[_148633, _148635, _148637], [763 ^ [], 759 ^ [], 758 ^ []]]))).
% 58.69/57.27 ncf('1.1.1',plain,[v1_relat_1(763 ^ []), 747 : r2_hidden(409 ^ [k9_relat_1(763 ^ [], 760 ^ []), k8_relset_2(758 ^ [], 759 ^ [], 760 ^ [], 763 ^ [])], k9_relat_1(763 ^ [], k1_tarski(392 ^ [760 ^ []]))), 747 : -(r2_hidden(k4_tarski(392 ^ [760 ^ []], 409 ^ [k9_relat_1(763 ^ [], 760 ^ []), k8_relset_2(758 ^ [], 759 ^ [], 760 ^ [], 763 ^ [])]), 763 ^ []))],extension(743 ^ 2,bind([[_163245, _163247, _163249], [763 ^ [], 392 ^ [760 ^ []], 409 ^ [k9_relat_1(763 ^ [], 760 ^ []), k8_relset_2(758 ^ [], 759 ^ [], 760 ^ [], 763 ^ [])]]]))).
% 58.69/57.27 ncf('1.1.1.1',plain,[-(r2_hidden(409 ^ [k9_relat_1(763 ^ [], 760 ^ []), k8_relset_2(758 ^ [], 759 ^ [], 760 ^ [], 763 ^ [])], k9_relat_1(763 ^ [], k1_tarski(392 ^ [760 ^ []])))), 673 : r2_hidden(392 ^ [760 ^ []], 760 ^ []), 673 : m1_subset_1(763 ^ [], k1_zfmisc_1(k2_zfmisc_1(758 ^ [], 759 ^ []))), 673 : r2_hidden(409 ^ [k9_relat_1(763 ^ [], 760 ^ []), k8_relset_2(758 ^ [], 759 ^ [], 760 ^ [], 763 ^ [])], k8_relset_2(758 ^ [], 759 ^ [], 760 ^ [], 763 ^ [])), 665 : m1_subset_1(760 ^ [], k1_zfmisc_1(758 ^ []))],extension(661 ^ 5,bind([[_160471, _160473, _160475, _160477, _160652, _160931], [760 ^ [], 409 ^ [k9_relat_1(763 ^ [], 760 ^ []), k8_relset_2(758 ^ [], 759 ^ [], 760 ^ [], 763 ^ [])], 759 ^ [], 758 ^ [], 763 ^ [], 392 ^ [760 ^ []]]]))).
% 58.69/57.27 ncf('1.1.1.1.1',plain,[-(r2_hidden(392 ^ [760 ^ []], 760 ^ [])), -(760 ^ [] = k1_xboole_0)],extension(391 ^ 10,bind([[_151170], [760 ^ []]]))).
% 58.69/57.27 ncf('1.1.1.1.1.1',plain,[760 ^ [] = k1_xboole_0],extension(767 ^ 11)).
% 58.69/57.27 ncf('1.1.1.1.2',plain,[-(m1_subset_1(763 ^ [], k1_zfmisc_1(k2_zfmisc_1(758 ^ [], 759 ^ []))))],reduction('1')).
% 58.69/57.27 ncf('1.1.1.1.3',plain,[-(r2_hidden(409 ^ [k9_relat_1(763 ^ [], 760 ^ []), k8_relset_2(758 ^ [], 759 ^ [], 760 ^ [], 763 ^ [])], k8_relset_2(758 ^ [], 759 ^ [], 760 ^ [], 763 ^ []))), -(r1_tarski(k8_relset_2(758 ^ [], 759 ^ [], 760 ^ [], 763 ^ []), k9_relat_1(763 ^ [], 760 ^ [])))],extension(408 ^ 8,bind([[_151775, _151777], [k9_relat_1(763 ^ [], 760 ^ []), k8_relset_2(758 ^ [], 759 ^ [], 760 ^ [], 763 ^ [])]]))).
% 58.69/57.27 ncf('1.1.1.1.3.1',plain,[r1_tarski(k8_relset_2(758 ^ [], 759 ^ [], 760 ^ [], 763 ^ []), k9_relat_1(763 ^ [], 760 ^ []))],extension(769 ^ 9)).
% 58.69/57.27 ncf('1.1.1.1.4',plain,[-(m1_subset_1(760 ^ [], k1_zfmisc_1(758 ^ [])))],extension(762 ^ 6)).
% 58.69/57.27 ncf('1.1.1.2',plain,[r2_hidden(k4_tarski(392 ^ [760 ^ []], 409 ^ [k9_relat_1(763 ^ [], 760 ^ []), k8_relset_2(758 ^ [], 759 ^ [], 760 ^ [], 763 ^ [])]), 763 ^ []), 355 : r2_hidden(392 ^ [760 ^ []], 760 ^ []), 355 : -(r2_hidden(409 ^ [k9_relat_1(763 ^ [], 760 ^ []), k8_relset_2(758 ^ [], 759 ^ [], 760 ^ [], 763 ^ [])], k9_relat_1(763 ^ [], 760 ^ []))), 353 : k9_relat_1(763 ^ [], 760 ^ []) = k9_relat_1(763 ^ [], 760 ^ []), 340 : v1_relat_1(763 ^ [])],extension(336 ^ 5,bind([[_148943, _149150, _149152, _149696, _149801], [763 ^ [], k9_relat_1(763 ^ [], 760 ^ []), 760 ^ [], 409 ^ [k9_relat_1(763 ^ [], 760 ^ []), k8_relset_2(758 ^ [], 759 ^ [], 760 ^ [], 763 ^ [])], 392 ^ [760 ^ []]]]))).
% 58.69/57.27 ncf('1.1.1.2.1',plain,[-(r2_hidden(392 ^ [760 ^ []], 760 ^ [])), -(760 ^ [] = k1_xboole_0)],extension(391 ^ 12,bind([[_151170], [760 ^ []]]))).
% 58.69/57.27 ncf('1.1.1.2.1.1',plain,[760 ^ [] = k1_xboole_0],extension(767 ^ 13)).
% 58.69/57.27 ncf('1.1.1.2.2',plain,[r2_hidden(409 ^ [k9_relat_1(763 ^ [], 760 ^ []), k8_relset_2(758 ^ [], 759 ^ [], 760 ^ [], 763 ^ [])], k9_relat_1(763 ^ [], 760 ^ [])), -(r1_tarski(k8_relset_2(758 ^ [], 759 ^ [], 760 ^ [], 763 ^ []), k9_relat_1(763 ^ [], 760 ^ [])))],extension(408 ^ 10,bind([[_151775, _151777], [k9_relat_1(763 ^ [], 760 ^ []), k8_relset_2(758 ^ [], 759 ^ [], 760 ^ [], 763 ^ [])]]))).
% 58.69/57.27 ncf('1.1.1.2.2.1',plain,[r1_tarski(k8_relset_2(758 ^ [], 759 ^ [], 760 ^ [], 763 ^ []), k9_relat_1(763 ^ [], 760 ^ []))],extension(769 ^ 11)).
% 58.69/57.27 ncf('1.1.1.2.3',plain,[-(k9_relat_1(763 ^ [], 760 ^ []) = k9_relat_1(763 ^ [], 760 ^ []))],extension(2 ^ 8,bind([[_137356], [k9_relat_1(763 ^ [], 760 ^ [])]]))).
% 58.69/57.27 ncf('1.1.1.2.4',plain,[-(v1_relat_1(763 ^ []))],reduction('1.1')).
% 58.69/57.27 %-----------------------------------------------------
% 58.69/57.27 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------