%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : CAT032+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n027.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 10:12:50 EDT 2023
% Result : Theorem 0.50s 1.36s
% Output : Proof 0.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.11 % Problem : CAT032+1 : TPTP v8.1.2. Released v3.4.0.
% 0.09/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n027.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 20:34:36 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.50/1.36
% 0.50/1.36 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.50/1.36 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.50/1.36 %-----------------------------------------------------
% 0.50/1.36 ncf(matrix, plain, [(921 ^ _151609) ^ [] : [-(v2_cat_1(919 ^ []))], (923 ^ _151609) ^ [] : [-(l1_cat_1(919 ^ []))], (926 ^ _151609) ^ [] : [-(v2_cat_1(924 ^ []))], (928 ^ _151609) ^ [] : [-(l1_cat_1(924 ^ []))], (931 ^ _151609) ^ [] : [-(v2_cat_1(929 ^ []))], (933 ^ _151609) ^ [] : [-(l1_cat_1(929 ^ []))], (935 ^ _151609) ^ [] : [r1_isocat_1(k12_nattra_1(919 ^ [], k11_cat_2(924 ^ [], 929 ^ [])), k11_cat_2(k12_nattra_1(919 ^ [], 924 ^ []), k12_nattra_1(919 ^ [], 929 ^ [])))], (226 ^ _151609) ^ [_159014, _159016] : [_159016 = _159014, -(u3_cat_1(_159016) = u3_cat_1(_159014))], (232 ^ _151609) ^ [_159232, _159234] : [_159234 = _159232, -(u4_cat_1(_159234) = u4_cat_1(_159232))], (238 ^ _151609) ^ [_159450, _159452] : [_159452 = _159450, -(u5_cat_1(_159452) = u5_cat_1(_159450))], (244 ^ _151609) ^ [_159668, _159670] : [_159670 = _159668, -(u6_cat_1(_159670) = u6_cat_1(_159668))], (250 ^ _151609) ^ [_159886, _159888] : [_159888 = _159886, -(u1_cat_1(_159888) = u1_cat_1(_159886))], (256 ^ _151609) ^ [_160104, _160106] : [_160106 = _160104, -(u2_cat_1(_160106) = u2_cat_1(_160104))], (262 ^ _151609) ^ [_160350, _160352, _160354, _160356] : [-(k2_zfmisc_1(_160356, _160352) = k2_zfmisc_1(_160354, _160350)), _160356 = _160354, _160352 = _160350], (272 ^ _151609) ^ [_160821, _160823, _160825, _160827, _160829, _160831, _160833, _160835, _160837, _160839, _160841, _160843] : [-(g1_cat_1(_160843, _160839, _160835, _160831, _160827, _160823) = g1_cat_1(_160841, _160837, _160833, _160829, _160825, _160821)), _160843 = _160841, _160839 = _160837, _160835 = _160833, _160831 = _160829, _160827 = _160825, _160823 = _160821], (298 ^ _151609) ^ [_161820, _161822, _161824, _161826, _161828, _161830] : [-(k17_isocat_2(_161830, _161826, _161822) = k17_isocat_2(_161828, _161824, _161820)), _161830 = _161828, _161826 = _161824, _161822 = _161820], (312 ^ _151609) ^ [_162280, _162282] : [_162282 = _162280, -(k1_zfmisc_1(_162282) = k1_zfmisc_1(_162280))], (318 ^ _151609) ^ [_162526, _162528, _162530, _162532] : [-(k11_cat_2(_162532, _162528) = k11_cat_2(_162530, _162526)), _162532 = _162530, _162528 = _162526], (328 ^ _151609) ^ [_162865, _162867, _162869, _162871] : [-(k12_nattra_1(_162871, _162867) = k12_nattra_1(_162869, _162865)), _162871 = _162869, _162867 = _162865], (2 ^ _151609) ^ [_151753] : [-(_151753 = _151753)], (4 ^ _151609) ^ [_151860, _151862] : [_151862 = _151860, -(_151860 = _151862)], (10 ^ _151609) ^ [_152064, _152066, _152068] : [-(_152068 = _152064), _152068 = _152066, _152066 = _152064], (20 ^ _151609) ^ [_152377, _152379] : [-(v1_relat_1(_152377)), _152379 = _152377, v1_relat_1(_152379)], (30 ^ _151609) ^ [_152672, _152674] : [-(v1_cat_1(_152672)), _152674 = _152672, v1_cat_1(_152674)], (40 ^ _151609) ^ [_153023, _153025, _153027, _153029, _153031, _153033] : [-(m2_cat_1(_153031, _153027, _153023)), m2_cat_1(_153033, _153029, _153025), _153033 = _153031, _153029 = _153027, _153025 = _153023], (58 ^ _151609) ^ [_153576, _153578] : [-(v1_funct_1(_153576)), _153578 = _153576, v1_funct_1(_153578)], (68 ^ _151609) ^ [_153927, _153929, _153931, _153933, _153935, _153937] : [-(v1_funct_2(_153935, _153931, _153927)), v1_funct_2(_153937, _153933, _153929), _153937 = _153935, _153933 = _153931, _153929 = _153927], (86 ^ _151609) ^ [_154536, _154538, _154540, _154542, _154544, _154546] : [-(m2_relset_1(_154544, _154540, _154536)), m2_relset_1(_154546, _154542, _154538), _154546 = _154544, _154542 = _154540, _154538 = _154536], (104 ^ _151609) ^ [_155145, _155147, _155149, _155151, _155153, _155155] : [-(m1_relset_1(_155153, _155149, _155145)), m1_relset_1(_155155, _155151, _155147), _155155 = _155153, _155151 = _155149, _155147 = _155145], (122 ^ _151609) ^ [_155726, _155728, _155730, _155732] : [-(r1_tarski(_155730, _155726)), r1_tarski(_155732, _155728), _155732 = _155730, _155728 = _155726], (136 ^ _151609) ^ [_156198, _156200, _156202, _156204, _156206, _156208] : [-(v8_cat_1(_156206, _156202, _156198)), v8_cat_1(_156208, _156204, _156200), _156208 = _156206, _156204 = _156202, _156200 = _156198], (154 ^ _151609) ^ [_156779, _156781, _156783, _156785] : [-(m1_subset_1(_156783, _156779)), m1_subset_1(_156785, _156781), _156785 = _156783, _156781 = _156779], (168 ^ _151609) ^ [_157223, _157225, _157227, _157229] : [-(r2_hidden(_157227, _157223)), r2_hidden(_157229, _157225), _157229 = _157227, _157225 = _157223], (182 ^ _151609) ^ [_157639, _157641] : [-(v1_xboole_0(_157639)), _157641 = _157639, v1_xboole_0(_157641)], (192 ^ _151609) ^ [_157934, _157936] : [-(v2_cat_1(_157934)), _157936 = _157934, v2_cat_1(_157936)], (202 ^ _151609) ^ [_158229, _158231] : [-(l1_cat_1(_158229)), _158231 = _158229, l1_cat_1(_158231)], (212 ^ _151609) ^ [_158532, _158534, _158536, _158538] : [-(r1_isocat_1(_158536, _158532)), r1_isocat_1(_158538, _158534), _158538 = _158536, _158534 = _158532], (338 ^ _151609) ^ [_163232] : [l1_cat_1(_163232), v1_cat_1(_163232), -(_163232 = g1_cat_1(u1_cat_1(_163232), u2_cat_1(_163232), u3_cat_1(_163232), u4_cat_1(_163232), u5_cat_1(_163232), u6_cat_1(_163232)))], (348 ^ _151609) ^ [_163555, _163557] : [r2_hidden(_163557, _163555), r2_hidden(_163555, _163557)], (354 ^ _151609) ^ [_163780, _163782, _163784] : [m1_subset_1(_163780, k1_zfmisc_1(k2_zfmisc_1(_163784, _163782))), -(v1_relat_1(_163780))], (360 ^ _151609) ^ [_163990] : [v2_cat_1(_163990), l1_cat_1(_163990), 367 ^ _151609 : [(368 ^ _151609) ^ [_164227] : [v2_cat_1(_164227), l1_cat_1(_164227), 375 ^ _151609 : [(376 ^ _151609) ^ [] : [r1_isocat_1(_163990, _164227), 380 ^ _151609 : [(381 ^ _151609) ^ [] : [-(m2_cat_1(379 ^ [_163990, _164227], _163990, _164227))], (383 ^ _151609) ^ [] : [-(v8_cat_1(379 ^ [_163990, _164227], _163990, _164227))]]], (385 ^ _151609) ^ [] : [-(r1_isocat_1(_163990, _164227)), 386 ^ _151609 : [(387 ^ _151609) ^ [_164789] : [m2_cat_1(_164789, _163990, _164227), v8_cat_1(_164789, _163990, _164227)]]]]]]], (395 ^ _151609) ^ [_165135, _165137, _165139, _165141, _165143, _165145] : [446 ^ _151609 : [(447 ^ _151609) ^ [] : [-(v1_cat_1(g1_cat_1(_165145, _165143, _165141, _165139, _165137, _165135)))], (449 ^ _151609) ^ [] : [-(l1_cat_1(g1_cat_1(_165145, _165143, _165141, _165139, _165137, _165135)))]], -(v1_xboole_0(_165145)), -(v1_xboole_0(_165143)), v1_funct_1(_165141), v1_funct_2(_165141, _165143, _165145), m1_relset_1(_165141, _165143, _165145), v1_funct_1(_165139), v1_funct_2(_165139, _165143, _165145), m1_relset_1(_165139, _165143, _165145), v1_funct_1(_165137), m1_relset_1(_165137, k2_zfmisc_1(_165143, _165143), _165143), v1_funct_1(_165135), v1_funct_2(_165135, _165145, _165143), m1_relset_1(_165135, _165145, _165143)], (451 ^ _151609) ^ [_166750, _166752] : [466 ^ _151609 : [(467 ^ _151609) ^ [] : [-(v2_cat_1(k11_cat_2(_166752, _166750)))], (469 ^ _151609) ^ [] : [-(l1_cat_1(k11_cat_2(_166752, _166750)))]], v2_cat_1(_166752), l1_cat_1(_166752), v2_cat_1(_166750), l1_cat_1(_166750)], (471 ^ _151609) ^ [_167302, _167304] : [486 ^ _151609 : [(487 ^ _151609) ^ [] : [-(v1_cat_1(k12_nattra_1(_167304, _167302)))], (489 ^ _151609) ^ [] : [-(v2_cat_1(k12_nattra_1(_167304, _167302)))], (491 ^ _151609) ^ [] : [-(l1_cat_1(k12_nattra_1(_167304, _167302)))]], v2_cat_1(_167304), l1_cat_1(_167304), v2_cat_1(_167302), l1_cat_1(_167302)], (493 ^ _151609) ^ [_167946, _167948, _167950] : [-(m2_cat_1(k17_isocat_2(_167950, _167948, _167946), k12_nattra_1(_167950, k11_cat_2(_167948, _167946)), k11_cat_2(k12_nattra_1(_167950, _167948), k12_nattra_1(_167950, _167946)))), v2_cat_1(_167950), l1_cat_1(_167950), v2_cat_1(_167948), l1_cat_1(_167948), v2_cat_1(_167946), l1_cat_1(_167946)], (519 ^ _151609) ^ [] : [true___, -(true___)], (525 ^ _151609) ^ [] : [true___, -(true___)], (531 ^ _151609) ^ [] : [true___, -(true___)], (537 ^ _151609) ^ [] : [true___, -(true___)], (543 ^ _151609) ^ [] : [true___, -(true___)], (549 ^ _151609) ^ [] : [true___, -(true___)], (555 ^ _151609) ^ [_169369, _169371] : [570 ^ _151609 : [(571 ^ _151609) ^ [_169787] : [m2_cat_1(_169787, _169371, _169369), 574 ^ _151609 : [(575 ^ _151609) ^ [] : [-(v1_funct_1(_169787))], (577 ^ _151609) ^ [] : [-(v1_funct_2(_169787, u2_cat_1(_169371), u2_cat_1(_169369)))], (579 ^ _151609) ^ [] : [-(m2_relset_1(_169787, u2_cat_1(_169371), u2_cat_1(_169369)))]]]], v2_cat_1(_169371), l1_cat_1(_169371), v2_cat_1(_169369), l1_cat_1(_169369)], (581 ^ _151609) ^ [_170199, _170201, _170203] : [m2_relset_1(_170199, _170203, _170201), -(m1_subset_1(_170199, k1_zfmisc_1(k2_zfmisc_1(_170203, _170201))))], (587 ^ _151609) ^ [_170413] : [l1_cat_1(_170413), v1_xboole_0(u1_cat_1(_170413))], (593 ^ _151609) ^ [_170604] : [l1_cat_1(_170604), v1_xboole_0(u2_cat_1(_170604))], (599 ^ _151609) ^ [_170795] : [l1_cat_1(_170795), 602 ^ _151609 : [(603 ^ _151609) ^ [] : [-(v1_funct_1(u3_cat_1(_170795)))], (605 ^ _151609) ^ [] : [-(v1_funct_2(u3_cat_1(_170795), u2_cat_1(_170795), u1_cat_1(_170795)))], (607 ^ _151609) ^ [] : [-(m2_relset_1(u3_cat_1(_170795), u2_cat_1(_170795), u1_cat_1(_170795)))]]], (609 ^ _151609) ^ [_171158] : [l1_cat_1(_171158), 612 ^ _151609 : [(613 ^ _151609) ^ [] : [-(v1_funct_1(u4_cat_1(_171158)))], (615 ^ _151609) ^ [] : [-(v1_funct_2(u4_cat_1(_171158), u2_cat_1(_171158), u1_cat_1(_171158)))], (617 ^ _151609) ^ [] : [-(m2_relset_1(u4_cat_1(_171158), u2_cat_1(_171158), u1_cat_1(_171158)))]]], (619 ^ _151609) ^ [_171521] : [l1_cat_1(_171521), 622 ^ _151609 : [(623 ^ _151609) ^ [] : [-(v1_funct_1(u5_cat_1(_171521)))], (625 ^ _151609) ^ [] : [-(m2_relset_1(u5_cat_1(_171521), k2_zfmisc_1(u2_cat_1(_171521), u2_cat_1(_171521)), u2_cat_1(_171521)))]]], (627 ^ _151609) ^ [_171808] : [l1_cat_1(_171808), 630 ^ _151609 : [(631 ^ _151609) ^ [] : [-(v1_funct_1(u6_cat_1(_171808)))], (633 ^ _151609) ^ [] : [-(v1_funct_2(u6_cat_1(_171808), u1_cat_1(_171808), u2_cat_1(_171808)))], (635 ^ _151609) ^ [] : [-(m2_relset_1(u6_cat_1(_171808), u1_cat_1(_171808), u2_cat_1(_171808)))]]], (638 ^ _151609) ^ [] : [-(l1_cat_1(636 ^ []))], (641 ^ _151609) ^ [_172301, _172303] : [-(m1_relset_1(639 ^ [_172301, _172303], _172303, _172301))], (644 ^ _151609) ^ [_172428] : [-(m1_subset_1(642 ^ [_172428], _172428))], (646 ^ _151609) ^ [_172540, _172542] : [-(m2_cat_1(661 ^ [_172540, _172542], _172542, _172540)), v2_cat_1(_172542), l1_cat_1(_172542), v2_cat_1(_172540), l1_cat_1(_172540)], (666 ^ _151609) ^ [_173096, _173098] : [-(m2_relset_1(664 ^ [_173096, _173098], _173098, _173096))], (668 ^ _151609) ^ [_173183] : [v1_xboole_0(k1_zfmisc_1(_173183))], (670 ^ _151609) ^ [] : [-(v1_xboole_0(k1_xboole_0))], (672 ^ _151609) ^ [_173344, _173346] : [v1_xboole_0(k2_zfmisc_1(_173346, _173344)), -(v1_xboole_0(_173346)), -(v1_xboole_0(_173344))], (682 ^ _151609) ^ [_173706, _173708, _173710, _173712, _173714, _173716] : [733 ^ _151609 : [(734 ^ _151609) ^ [_175272, _175274, _175276, _175278, _175280, _175282] : [g1_cat_1(_173716, _173714, _173712, _173710, _173708, _173706) = g1_cat_1(_175282, _175280, _175278, _175276, _175274, _175272), 737 ^ _151609 : [(738 ^ _151609) ^ [] : [-(_173716 = _175282)], (740 ^ _151609) ^ [] : [-(_173714 = _175280)], (742 ^ _151609) ^ [] : [-(_173712 = _175278)], (744 ^ _151609) ^ [] : [-(_173710 = _175276)], (746 ^ _151609) ^ [] : [-(_173708 = _175274)], (748 ^ _151609) ^ [] : [-(_173706 = _175272)]]]], -(v1_xboole_0(_173716)), -(v1_xboole_0(_173714)), v1_funct_1(_173712), v1_funct_2(_173712, _173714, _173716), m1_relset_1(_173712, _173714, _173716), v1_funct_1(_173710), v1_funct_2(_173710, _173714, _173716), m1_relset_1(_173710, _173714, _173716), v1_funct_1(_173708), m1_relset_1(_173708, k2_zfmisc_1(_173714, _173714), _173714), v1_funct_1(_173706), v1_funct_2(_173706, _173716, _173714), m1_relset_1(_173706, _173716, _173714)], (750 ^ _151609) ^ [_176044] : [-(v1_xboole_0(_176044)), 754 ^ _151609 : [(755 ^ _151609) ^ [] : [-(m1_subset_1(753 ^ [_176044], k1_zfmisc_1(_176044)))], (757 ^ _151609) ^ [] : [v1_xboole_0(753 ^ [_176044])]]], (760 ^ _151609) ^ [] : [-(v1_xboole_0(758 ^ []))], (763 ^ _151609) ^ [_176516] : [-(m1_subset_1(761 ^ [_176516], k1_zfmisc_1(_176516)))], (765 ^ _151609) ^ [_176567] : [-(v1_xboole_0(761 ^ [_176567]))], (768 ^ _151609) ^ [] : [v1_xboole_0(766 ^ [])], (770 ^ _151609) ^ [_176813, _176815, _176817] : [m2_relset_1(_176813, _176817, _176815), -(m1_relset_1(_176813, _176817, _176815))], (776 ^ _151609) ^ [_176985, _176987, _176989] : [m1_relset_1(_176985, _176989, _176987), -(m2_relset_1(_176985, _176989, _176987))], (782 ^ _151609) ^ [_177207, _177209] : [-(r1_isocat_1(_177209, _177209)), v2_cat_1(_177209), l1_cat_1(_177209), v2_cat_1(_177207), l1_cat_1(_177207)], (800 ^ _151609) ^ [_177661, _177663] : [-(r1_tarski(_177663, _177663))], (802 ^ _151609) ^ [_177770, _177772] : [r1_isocat_1(_177772, _177770), -(r1_isocat_1(_177770, _177772)), v2_cat_1(_177772), l1_cat_1(_177772), v2_cat_1(_177770), l1_cat_1(_177770)], (824 ^ _151609) ^ [_178330, _178332] : [r2_hidden(_178332, _178330), -(m1_subset_1(_178332, _178330))], (830 ^ _151609) ^ [_178540, _178542] : [m1_subset_1(_178542, _178540), -(v1_xboole_0(_178540)), -(r2_hidden(_178542, _178540))], (840 ^ _151609) ^ [_178867, _178869] : [m1_subset_1(_178869, k1_zfmisc_1(_178867)), -(r1_tarski(_178869, _178867))], (846 ^ _151609) ^ [_179033, _179035] : [r1_tarski(_179035, _179033), -(m1_subset_1(_179035, k1_zfmisc_1(_179033)))], (852 ^ _151609) ^ [_179235] : [v2_cat_1(_179235), l1_cat_1(_179235), 859 ^ _151609 : [(860 ^ _151609) ^ [_179488] : [v2_cat_1(_179488), l1_cat_1(_179488), 867 ^ _151609 : [(868 ^ _151609) ^ [_179736] : [-(v8_cat_1(k17_isocat_2(_179235, _179488, _179736), k12_nattra_1(_179235, k11_cat_2(_179488, _179736)), k11_cat_2(k12_nattra_1(_179235, _179488), k12_nattra_1(_179235, _179736)))), v2_cat_1(_179736), l1_cat_1(_179736)]]]]], (878 ^ _151609) ^ [_180113, _180115, _180117] : [-(m1_subset_1(_180117, _180113)), r2_hidden(_180117, _180115), m1_subset_1(_180115, k1_zfmisc_1(_180113))], (888 ^ _151609) ^ [_180440, _180442, _180444] : [r2_hidden(_180444, _180442), m1_subset_1(_180442, k1_zfmisc_1(_180440)), v1_xboole_0(_180440)], (898 ^ _151609) ^ [_180736] : [v1_xboole_0(_180736), -(_180736 = k1_xboole_0)], (904 ^ _151609) ^ [_180938, _180940] : [r2_hidden(_180940, _180938), v1_xboole_0(_180938)], (910 ^ _151609) ^ [_181125, _181127] : [v1_xboole_0(_181127), -(_181127 = _181125), v1_xboole_0(_181125)]], input).
% 0.50/1.36 ncf('1',plain,[r1_isocat_1(k12_nattra_1(919 ^ [], k11_cat_2(924 ^ [], 929 ^ [])), k11_cat_2(k12_nattra_1(919 ^ [], 924 ^ []), k12_nattra_1(919 ^ [], 929 ^ [])))],start(935 ^ 0)).
% 0.50/1.36 ncf('1.1',plain,[-(r1_isocat_1(k12_nattra_1(919 ^ [], k11_cat_2(924 ^ [], 929 ^ [])), k11_cat_2(k12_nattra_1(919 ^ [], 924 ^ []), k12_nattra_1(919 ^ [], 929 ^ [])))), 387 : m2_cat_1(k17_isocat_2(919 ^ [], 924 ^ [], 929 ^ []), k12_nattra_1(919 ^ [], k11_cat_2(924 ^ [], 929 ^ [])), k11_cat_2(k12_nattra_1(919 ^ [], 924 ^ []), k12_nattra_1(919 ^ [], 929 ^ []))), 387 : v8_cat_1(k17_isocat_2(919 ^ [], 924 ^ [], 929 ^ []), k12_nattra_1(919 ^ [], k11_cat_2(924 ^ [], 929 ^ [])), k11_cat_2(k12_nattra_1(919 ^ [], 924 ^ []), k12_nattra_1(919 ^ [], 929 ^ []))), 385 : v2_cat_1(k11_cat_2(k12_nattra_1(919 ^ [], 924 ^ []), k12_nattra_1(919 ^ [], 929 ^ []))), 385 : l1_cat_1(k11_cat_2(k12_nattra_1(919 ^ [], 924 ^ []), k12_nattra_1(919 ^ [], 929 ^ []))), 368 : v2_cat_1(k12_nattra_1(919 ^ [], k11_cat_2(924 ^ [], 929 ^ []))), 368 : l1_cat_1(k12_nattra_1(919 ^ [], k11_cat_2(924 ^ [], 929 ^ [])))],extension(360 ^ 1,bind([[_163990, _164227, _164789], [k12_nattra_1(919 ^ [], k11_cat_2(924 ^ [], 929 ^ [])), k11_cat_2(k12_nattra_1(919 ^ [], 924 ^ []), k12_nattra_1(919 ^ [], 929 ^ [])), k17_isocat_2(919 ^ [], 924 ^ [], 929 ^ [])]]))).
% 0.50/1.36 ncf('1.1.1',plain,[-(m2_cat_1(k17_isocat_2(919 ^ [], 924 ^ [], 929 ^ []), k12_nattra_1(919 ^ [], k11_cat_2(924 ^ [], 929 ^ [])), k11_cat_2(k12_nattra_1(919 ^ [], 924 ^ []), k12_nattra_1(919 ^ [], 929 ^ [])))), v2_cat_1(919 ^ []), l1_cat_1(919 ^ []), v2_cat_1(924 ^ []), l1_cat_1(924 ^ []), v2_cat_1(929 ^ []), l1_cat_1(929 ^ [])],extension(493 ^ 8,bind([[_167946, _167948, _167950], [929 ^ [], 924 ^ [], 919 ^ []]]))).
% 0.50/1.36 ncf('1.1.1.1',plain,[-(v2_cat_1(919 ^ []))],extension(921 ^ 9)).
% 0.50/1.36 ncf('1.1.1.2',plain,[-(l1_cat_1(919 ^ []))],extension(923 ^ 9)).
% 0.50/1.36 ncf('1.1.1.3',plain,[-(v2_cat_1(924 ^ []))],extension(926 ^ 9)).
% 0.50/1.36 ncf('1.1.1.4',plain,[-(l1_cat_1(924 ^ []))],extension(928 ^ 9)).
% 0.50/1.36 ncf('1.1.1.5',plain,[-(v2_cat_1(929 ^ []))],extension(931 ^ 9)).
% 0.50/1.36 ncf('1.1.1.6',plain,[-(l1_cat_1(929 ^ []))],extension(933 ^ 9)).
% 0.50/1.36 ncf('1.1.2',plain,[-(v8_cat_1(k17_isocat_2(919 ^ [], 924 ^ [], 929 ^ []), k12_nattra_1(919 ^ [], k11_cat_2(924 ^ [], 929 ^ [])), k11_cat_2(k12_nattra_1(919 ^ [], 924 ^ []), k12_nattra_1(919 ^ [], 929 ^ [])))), 868 : v2_cat_1(929 ^ []), 868 : l1_cat_1(929 ^ []), 868 : v2_cat_1(924 ^ []), 868 : l1_cat_1(924 ^ []), 860 : v2_cat_1(919 ^ []), 860 : l1_cat_1(919 ^ [])],extension(852 ^ 8,bind([[_179235, _179488, _179736], [919 ^ [], 924 ^ [], 929 ^ []]]))).
% 0.50/1.36 ncf('1.1.2.1',plain,[-(v2_cat_1(929 ^ []))],extension(931 ^ 13)).
% 0.50/1.36 ncf('1.1.2.2',plain,[-(l1_cat_1(929 ^ []))],extension(933 ^ 13)).
% 0.50/1.36 ncf('1.1.2.3',plain,[-(v2_cat_1(924 ^ []))],extension(926 ^ 11)).
% 0.50/1.36 ncf('1.1.2.4',plain,[-(l1_cat_1(924 ^ []))],extension(928 ^ 11)).
% 0.50/1.36 ncf('1.1.2.5',plain,[-(v2_cat_1(919 ^ []))],extension(921 ^ 9)).
% 0.50/1.36 ncf('1.1.2.6',plain,[-(l1_cat_1(919 ^ []))],extension(923 ^ 9)).
% 0.50/1.36 ncf('1.1.3',plain,[-(v2_cat_1(k11_cat_2(k12_nattra_1(919 ^ [], 924 ^ []), k12_nattra_1(919 ^ [], 929 ^ [])))), v2_cat_1(k12_nattra_1(919 ^ [], 924 ^ [])), l1_cat_1(k12_nattra_1(919 ^ [], 924 ^ [])), v2_cat_1(k12_nattra_1(919 ^ [], 929 ^ [])), l1_cat_1(k12_nattra_1(919 ^ [], 929 ^ []))],extension(451 ^ 4,bind([[_166750, _166752], [k12_nattra_1(919 ^ [], 929 ^ []), k12_nattra_1(919 ^ [], 924 ^ [])]]))).
% 0.50/1.36 ncf('1.1.3.1',plain,[-(v2_cat_1(k12_nattra_1(919 ^ [], 924 ^ []))), v2_cat_1(919 ^ []), l1_cat_1(919 ^ []), v2_cat_1(924 ^ []), l1_cat_1(924 ^ [])],extension(471 ^ 5,bind([[_167302, _167304], [924 ^ [], 919 ^ []]]))).
% 0.50/1.36 ncf('1.1.3.1.1',plain,[-(v2_cat_1(919 ^ []))],extension(921 ^ 6)).
% 0.50/1.36 ncf('1.1.3.1.2',plain,[-(l1_cat_1(919 ^ []))],extension(923 ^ 6)).
% 0.50/1.36 ncf('1.1.3.1.3',plain,[-(v2_cat_1(924 ^ []))],extension(926 ^ 6)).
% 0.50/1.36 ncf('1.1.3.1.4',plain,[-(l1_cat_1(924 ^ []))],extension(928 ^ 6)).
% 0.50/1.36 ncf('1.1.3.2',plain,[-(l1_cat_1(k12_nattra_1(919 ^ [], 924 ^ []))), v2_cat_1(919 ^ []), l1_cat_1(919 ^ []), v2_cat_1(924 ^ []), l1_cat_1(924 ^ [])],extension(471 ^ 5,bind([[_167302, _167304], [924 ^ [], 919 ^ []]]))).
% 0.50/1.36 ncf('1.1.3.2.1',plain,[-(v2_cat_1(919 ^ []))],extension(921 ^ 6)).
% 0.50/1.36 ncf('1.1.3.2.2',plain,[-(l1_cat_1(919 ^ []))],extension(923 ^ 6)).
% 0.50/1.36 ncf('1.1.3.2.3',plain,[-(v2_cat_1(924 ^ []))],extension(926 ^ 6)).
% 0.50/1.36 ncf('1.1.3.2.4',plain,[-(l1_cat_1(924 ^ []))],extension(928 ^ 6)).
% 0.50/1.36 ncf('1.1.3.3',plain,[-(v2_cat_1(k12_nattra_1(919 ^ [], 929 ^ []))), v2_cat_1(919 ^ []), l1_cat_1(919 ^ []), v2_cat_1(929 ^ []), l1_cat_1(929 ^ [])],extension(471 ^ 5,bind([[_167302, _167304], [929 ^ [], 919 ^ []]]))).
% 0.50/1.36 ncf('1.1.3.3.1',plain,[-(v2_cat_1(919 ^ []))],extension(921 ^ 6)).
% 0.50/1.36 ncf('1.1.3.3.2',plain,[-(l1_cat_1(919 ^ []))],extension(923 ^ 6)).
% 0.50/1.36 ncf('1.1.3.3.3',plain,[-(v2_cat_1(929 ^ []))],extension(931 ^ 6)).
% 0.50/1.36 ncf('1.1.3.3.4',plain,[-(l1_cat_1(929 ^ []))],extension(933 ^ 6)).
% 0.50/1.36 ncf('1.1.3.4',plain,[-(l1_cat_1(k12_nattra_1(919 ^ [], 929 ^ []))), v2_cat_1(919 ^ []), l1_cat_1(919 ^ []), v2_cat_1(929 ^ []), l1_cat_1(929 ^ [])],extension(471 ^ 5,bind([[_167302, _167304], [929 ^ [], 919 ^ []]]))).
% 0.50/1.36 ncf('1.1.3.4.1',plain,[-(v2_cat_1(919 ^ []))],extension(921 ^ 6)).
% 0.50/1.36 ncf('1.1.3.4.2',plain,[-(l1_cat_1(919 ^ []))],extension(923 ^ 6)).
% 0.50/1.36 ncf('1.1.3.4.3',plain,[-(v2_cat_1(929 ^ []))],extension(931 ^ 6)).
% 0.50/1.36 ncf('1.1.3.4.4',plain,[-(l1_cat_1(929 ^ []))],extension(933 ^ 6)).
% 0.50/1.36 ncf('1.1.4',plain,[-(l1_cat_1(k11_cat_2(k12_nattra_1(919 ^ [], 924 ^ []), k12_nattra_1(919 ^ [], 929 ^ [])))), v2_cat_1(k12_nattra_1(919 ^ [], 924 ^ [])), l1_cat_1(k12_nattra_1(919 ^ [], 924 ^ [])), v2_cat_1(k12_nattra_1(919 ^ [], 929 ^ [])), l1_cat_1(k12_nattra_1(919 ^ [], 929 ^ []))],extension(451 ^ 4,bind([[_166750, _166752], [k12_nattra_1(919 ^ [], 929 ^ []), k12_nattra_1(919 ^ [], 924 ^ [])]]))).
% 0.50/1.36 ncf('1.1.4.1',plain,[-(v2_cat_1(k12_nattra_1(919 ^ [], 924 ^ []))), v2_cat_1(919 ^ []), l1_cat_1(919 ^ []), v2_cat_1(924 ^ []), l1_cat_1(924 ^ [])],extension(471 ^ 5,bind([[_167302, _167304], [924 ^ [], 919 ^ []]]))).
% 0.50/1.36 ncf('1.1.4.1.1',plain,[-(v2_cat_1(919 ^ []))],extension(921 ^ 6)).
% 0.50/1.36 ncf('1.1.4.1.2',plain,[-(l1_cat_1(919 ^ []))],extension(923 ^ 6)).
% 0.50/1.36 ncf('1.1.4.1.3',plain,[-(v2_cat_1(924 ^ []))],extension(926 ^ 6)).
% 0.50/1.36 ncf('1.1.4.1.4',plain,[-(l1_cat_1(924 ^ []))],extension(928 ^ 6)).
% 0.50/1.36 ncf('1.1.4.2',plain,[-(l1_cat_1(k12_nattra_1(919 ^ [], 924 ^ []))), v2_cat_1(919 ^ []), l1_cat_1(919 ^ []), v2_cat_1(924 ^ []), l1_cat_1(924 ^ [])],extension(471 ^ 5,bind([[_167302, _167304], [924 ^ [], 919 ^ []]]))).
% 0.50/1.36 ncf('1.1.4.2.1',plain,[-(v2_cat_1(919 ^ []))],extension(921 ^ 6)).
% 0.50/1.36 ncf('1.1.4.2.2',plain,[-(l1_cat_1(919 ^ []))],extension(923 ^ 6)).
% 0.50/1.36 ncf('1.1.4.2.3',plain,[-(v2_cat_1(924 ^ []))],extension(926 ^ 6)).
% 0.50/1.36 ncf('1.1.4.2.4',plain,[-(l1_cat_1(924 ^ []))],extension(928 ^ 6)).
% 0.50/1.36 ncf('1.1.4.3',plain,[-(v2_cat_1(k12_nattra_1(919 ^ [], 929 ^ []))), v2_cat_1(919 ^ []), l1_cat_1(919 ^ []), v2_cat_1(929 ^ []), l1_cat_1(929 ^ [])],extension(471 ^ 5,bind([[_167302, _167304], [929 ^ [], 919 ^ []]]))).
% 0.50/1.36 ncf('1.1.4.3.1',plain,[-(v2_cat_1(919 ^ []))],extension(921 ^ 6)).
% 0.50/1.36 ncf('1.1.4.3.2',plain,[-(l1_cat_1(919 ^ []))],extension(923 ^ 6)).
% 0.50/1.36 ncf('1.1.4.3.3',plain,[-(v2_cat_1(929 ^ []))],extension(931 ^ 6)).
% 0.50/1.36 ncf('1.1.4.3.4',plain,[-(l1_cat_1(929 ^ []))],extension(933 ^ 6)).
% 0.50/1.36 ncf('1.1.4.4',plain,[-(l1_cat_1(k12_nattra_1(919 ^ [], 929 ^ []))), v2_cat_1(919 ^ []), l1_cat_1(919 ^ []), v2_cat_1(929 ^ []), l1_cat_1(929 ^ [])],extension(471 ^ 5,bind([[_167302, _167304], [929 ^ [], 919 ^ []]]))).
% 0.50/1.36 ncf('1.1.4.4.1',plain,[-(v2_cat_1(919 ^ []))],extension(921 ^ 6)).
% 0.50/1.36 ncf('1.1.4.4.2',plain,[-(l1_cat_1(919 ^ []))],extension(923 ^ 6)).
% 0.50/1.36 ncf('1.1.4.4.3',plain,[-(v2_cat_1(929 ^ []))],extension(931 ^ 6)).
% 0.50/1.36 ncf('1.1.4.4.4',plain,[-(l1_cat_1(929 ^ []))],extension(933 ^ 6)).
% 0.50/1.36 ncf('1.1.5',plain,[-(v2_cat_1(k12_nattra_1(919 ^ [], k11_cat_2(924 ^ [], 929 ^ [])))), v2_cat_1(919 ^ []), l1_cat_1(919 ^ []), v2_cat_1(k11_cat_2(924 ^ [], 929 ^ [])), l1_cat_1(k11_cat_2(924 ^ [], 929 ^ []))],extension(471 ^ 2,bind([[_167302, _167304], [k11_cat_2(924 ^ [], 929 ^ []), 919 ^ []]]))).
% 0.50/1.36 ncf('1.1.5.1',plain,[-(v2_cat_1(919 ^ []))],extension(921 ^ 3)).
% 0.50/1.36 ncf('1.1.5.2',plain,[-(l1_cat_1(919 ^ []))],extension(923 ^ 3)).
% 0.50/1.36 ncf('1.1.5.3',plain,[-(v2_cat_1(k11_cat_2(924 ^ [], 929 ^ []))), v2_cat_1(924 ^ []), l1_cat_1(924 ^ []), v2_cat_1(929 ^ []), l1_cat_1(929 ^ [])],extension(451 ^ 3,bind([[_166750, _166752], [929 ^ [], 924 ^ []]]))).
% 0.50/1.36 ncf('1.1.5.3.1',plain,[-(v2_cat_1(924 ^ []))],extension(926 ^ 4)).
% 0.50/1.36 ncf('1.1.5.3.2',plain,[-(l1_cat_1(924 ^ []))],extension(928 ^ 4)).
% 0.50/1.36 ncf('1.1.5.3.3',plain,[-(v2_cat_1(929 ^ []))],extension(931 ^ 4)).
% 0.50/1.36 ncf('1.1.5.3.4',plain,[-(l1_cat_1(929 ^ []))],extension(933 ^ 4)).
% 0.50/1.36 ncf('1.1.5.4',plain,[-(l1_cat_1(k11_cat_2(924 ^ [], 929 ^ []))), v2_cat_1(924 ^ []), l1_cat_1(924 ^ []), v2_cat_1(929 ^ []), l1_cat_1(929 ^ [])],extension(451 ^ 3,bind([[_166750, _166752], [929 ^ [], 924 ^ []]]))).
% 0.50/1.36 ncf('1.1.5.4.1',plain,[-(v2_cat_1(924 ^ []))],extension(926 ^ 4)).
% 0.50/1.36 ncf('1.1.5.4.2',plain,[-(l1_cat_1(924 ^ []))],extension(928 ^ 4)).
% 0.50/1.36 ncf('1.1.5.4.3',plain,[-(v2_cat_1(929 ^ []))],extension(931 ^ 4)).
% 0.50/1.36 ncf('1.1.5.4.4',plain,[-(l1_cat_1(929 ^ []))],extension(933 ^ 4)).
% 0.50/1.36 ncf('1.1.6',plain,[-(l1_cat_1(k12_nattra_1(919 ^ [], k11_cat_2(924 ^ [], 929 ^ [])))), v2_cat_1(919 ^ []), l1_cat_1(919 ^ []), v2_cat_1(k11_cat_2(924 ^ [], 929 ^ [])), l1_cat_1(k11_cat_2(924 ^ [], 929 ^ []))],extension(471 ^ 2,bind([[_167302, _167304], [k11_cat_2(924 ^ [], 929 ^ []), 919 ^ []]]))).
% 0.50/1.36 ncf('1.1.6.1',plain,[-(v2_cat_1(919 ^ []))],extension(921 ^ 3)).
% 0.50/1.36 ncf('1.1.6.2',plain,[-(l1_cat_1(919 ^ []))],extension(923 ^ 3)).
% 0.50/1.36 ncf('1.1.6.3',plain,[-(v2_cat_1(k11_cat_2(924 ^ [], 929 ^ []))), v2_cat_1(924 ^ []), l1_cat_1(924 ^ []), v2_cat_1(929 ^ []), l1_cat_1(929 ^ [])],extension(451 ^ 3,bind([[_166750, _166752], [929 ^ [], 924 ^ []]]))).
% 0.50/1.36 ncf('1.1.6.3.1',plain,[-(v2_cat_1(924 ^ []))],extension(926 ^ 4)).
% 0.50/1.36 ncf('1.1.6.3.2',plain,[-(l1_cat_1(924 ^ []))],extension(928 ^ 4)).
% 0.50/1.36 ncf('1.1.6.3.3',plain,[-(v2_cat_1(929 ^ []))],extension(931 ^ 4)).
% 0.50/1.36 ncf('1.1.6.3.4',plain,[-(l1_cat_1(929 ^ []))],extension(933 ^ 4)).
% 0.50/1.36 ncf('1.1.6.4',plain,[-(l1_cat_1(k11_cat_2(924 ^ [], 929 ^ []))), v2_cat_1(924 ^ []), l1_cat_1(924 ^ []), v2_cat_1(929 ^ []), l1_cat_1(929 ^ [])],extension(451 ^ 3,bind([[_166750, _166752], [929 ^ [], 924 ^ []]]))).
% 0.50/1.36 ncf('1.1.6.4.1',plain,[-(v2_cat_1(924 ^ []))],extension(926 ^ 4)).
% 0.50/1.36 ncf('1.1.6.4.2',plain,[-(l1_cat_1(924 ^ []))],extension(928 ^ 4)).
% 0.50/1.36 ncf('1.1.6.4.3',plain,[-(v2_cat_1(929 ^ []))],extension(931 ^ 4)).
% 0.50/1.36 ncf('1.1.6.4.4',plain,[-(l1_cat_1(929 ^ []))],extension(933 ^ 4)).
% 0.50/1.36 %-----------------------------------------------------
% 0.50/1.36 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------