%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : LAT362+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n022.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:28:58 EDT 2023
% Result : Theorem 0.84s 1.39s
% Output : Proof 0.84s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : LAT362+1 : TPTP v8.1.2. Released v3.4.0.
% 0.10/0.12 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n022.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 18 14:30:47 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.84/1.39
% 0.84/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.84/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.84/1.39 %-----------------------------------------------------
% 0.84/1.39 ncf(matrix, plain, [(2463 ^ _371389) ^ [] : [v2_setfam_1(2461 ^ [])], (2465 ^ _371389) ^ [] : [r2_functor0(k4_waybel34(2461 ^ []), k5_waybel34(2461 ^ []))], (724 ^ _371389) ^ [_394928, _394930] : [_394930 = _394928, -(u2_altcat_1(_394930) = u2_altcat_1(_394928))], (730 ^ _371389) ^ [_395202, _395204, _395206, _395208, _395210, _395212] : [-(u1_functor0(_395212, _395208, _395204) = u1_functor0(_395210, _395206, _395202)), _395212 = _395210, _395208 = _395206, _395204 = _395202], (744 ^ _371389) ^ [_395718, _395720, _395722, _395724, _395726, _395728] : [-(u2_functor0(_395728, _395724, _395720) = u2_functor0(_395726, _395722, _395718)), _395728 = _395726, _395724 = _395722, _395720 = _395718], (758 ^ _371389) ^ [_396178, _396180] : [_396180 = _396178, -(k6_waybel34(_396180) = k6_waybel34(_396178))], (764 ^ _371389) ^ [_396452, _396454, _396456, _396458, _396460, _396462] : [-(k3_zfmisc_1(_396462, _396458, _396454) = k3_zfmisc_1(_396460, _396456, _396452)), _396462 = _396460, _396458 = _396456, _396454 = _396452], (778 ^ _371389) ^ [_396968, _396970, _396972, _396974, _396976, _396978] : [-(k3_altcat_1(_396978, _396974, _396970) = k3_altcat_1(_396976, _396972, _396968)), _396978 = _396976, _396974 = _396972, _396970 = _396968], (792 ^ _371389) ^ [_397456, _397458, _397460, _397462] : [-(k2_altcat_1(_397462, _397458) = k2_altcat_1(_397460, _397456)), _397462 = _397460, _397458 = _397456], (802 ^ _371389) ^ [_397843, _397845, _397847, _397849, _397851, _397853] : [-(g2_altcat_1(_397853, _397849, _397845) = g2_altcat_1(_397851, _397847, _397843)), _397853 = _397851, _397849 = _397847, _397845 = _397843], (816 ^ _371389) ^ [_398331, _398333, _398335, _398337] : [-(k2_zfmisc_1(_398337, _398333) = k2_zfmisc_1(_398335, _398331)), _398337 = _398335, _398333 = _398331], (826 ^ _371389) ^ [_398662, _398664] : [_398664 = _398662, -(u1_altcat_1(_398664) = u1_altcat_1(_398662))], (832 ^ _371389) ^ [_398964, _398966, _398968, _398970, _398972, _398974, _398976, _398978] : [-(g2_functor0(_398978, _398974, _398970, _398966) = g2_functor0(_398976, _398972, _398968, _398964)), _398978 = _398976, _398974 = _398972, _398970 = _398968, _398966 = _398964], (850 ^ _371389) ^ [_399569, _399571] : [_399571 = _399569, -(u1_struct_0(_399571) = u1_struct_0(_399569))], (856 ^ _371389) ^ [_399787, _399789] : [_399789 = _399787, -(k1_zfmisc_1(_399789) = k1_zfmisc_1(_399787))], (862 ^ _371389) ^ [_400005, _400007] : [_400007 = _400005, -(k4_waybel34(_400007) = k4_waybel34(_400005))], (868 ^ _371389) ^ [_400203, _400205] : [_400205 = _400203, -(k5_waybel34(_400205) = k5_waybel34(_400203))], (2 ^ _371389) ^ [_371533] : [-(_371533 = _371533)], (4 ^ _371389) ^ [_371640, _371642] : [_371642 = _371640, -(_371640 = _371642)], (10 ^ _371389) ^ [_371844, _371846, _371848] : [-(_371848 = _371844), _371848 = _371846, _371846 = _371844], (20 ^ _371389) ^ [_372157, _372159] : [-(v1_xcmplx_0(_372157)), _372159 = _372157, v1_xcmplx_0(_372159)], (30 ^ _371389) ^ [_372452, _372454] : [-(v4_ordinal2(_372452)), _372454 = _372452, v4_ordinal2(_372454)], (40 ^ _371389) ^ [_372747, _372749] : [-(v1_xreal_0(_372747)), _372749 = _372747, v1_xreal_0(_372749)], (50 ^ _371389) ^ [_373042, _373044] : [-(v1_int_1(_373042)), _373044 = _373042, v1_int_1(_373044)], (60 ^ _371389) ^ [_373337, _373339] : [-(v1_rat_1(_373337)), _373339 = _373337, v1_rat_1(_373339)], (70 ^ _371389) ^ [_373688, _373690, _373692, _373694, _373696, _373698] : [-(l1_functor0(_373696, _373692, _373688)), l1_functor0(_373698, _373694, _373690), _373698 = _373696, _373694 = _373692, _373690 = _373688], (88 ^ _371389) ^ [_374297, _374299, _374301, _374303, _374305, _374307] : [-(m2_functor0(_374305, _374301, _374297)), m2_functor0(_374307, _374303, _374299), _374307 = _374305, _374303 = _374301, _374299 = _374297], (106 ^ _371389) ^ [_374850, _374852] : [-(v1_funcop_1(_374850)), _374852 = _374850, v1_funcop_1(_374852)], (116 ^ _371389) ^ [_375201, _375203, _375205, _375207, _375209, _375211] : [-(v14_functor0(_375209, _375205, _375201)), v14_functor0(_375211, _375207, _375203), _375211 = _375209, _375207 = _375205, _375203 = _375201], (134 ^ _371389) ^ [_375810, _375812, _375814, _375816, _375818, _375820] : [-(v16_functor0(_375818, _375814, _375810)), v16_functor0(_375820, _375816, _375812), _375820 = _375818, _375816 = _375814, _375812 = _375810], (152 ^ _371389) ^ [_376419, _376421, _376423, _376425, _376427, _376429] : [-(v21_functor0(_376427, _376423, _376419)), v21_functor0(_376429, _376425, _376421), _376429 = _376427, _376425 = _376423, _376421 = _376419], (170 ^ _371389) ^ [_377000, _377002, _377004, _377006] : [-(m1_pboole(_377004, _377000)), m1_pboole(_377006, _377002), _377006 = _377004, _377002 = _377000], (184 ^ _371389) ^ [_377500, _377502, _377504, _377506, _377508, _377510, _377512, _377514] : [-(m3_pboole(_377512, _377508, _377504, _377500)), m3_pboole(_377514, _377510, _377506, _377502), _377514 = _377512, _377510 = _377508, _377506 = _377504, _377502 = _377500], (206 ^ _371389) ^ [_378262, _378264, _378266, _378268, _378270, _378272] : [-(v1_funct_2(_378270, _378266, _378262)), v1_funct_2(_378272, _378268, _378264), _378272 = _378270, _378268 = _378266, _378264 = _378262], (224 ^ _371389) ^ [_378955, _378957, _378959, _378961, _378963, _378965, _378967, _378969, _378971, _378973, _378975, _378977] : [-(m1_functor0(_378975, _378971, _378967, _378963, _378959, _378955)), m1_functor0(_378977, _378973, _378969, _378965, _378961, _378957), _378977 = _378975, _378973 = _378971, _378969 = _378967, _378965 = _378963, _378961 = _378959, _378957 = _378955], (254 ^ _371389) ^ [_380015, _380017] : [-(v1_membered(_380015)), _380017 = _380015, v1_membered(_380017)], (264 ^ _371389) ^ [_380310, _380312] : [-(v2_membered(_380310)), _380312 = _380310, v2_membered(_380312)], (274 ^ _371389) ^ [_380605, _380607] : [-(v3_membered(_380605)), _380607 = _380605, v3_membered(_380607)], (284 ^ _371389) ^ [_380900, _380902] : [-(v4_membered(_380900)), _380902 = _380900, v4_membered(_380902)], (294 ^ _371389) ^ [_381195, _381197] : [-(v5_membered(_381195)), _381197 = _381195, v5_membered(_381197)], (304 ^ _371389) ^ [_381490, _381492] : [-(v6_altcat_1(_381490)), _381492 = _381490, v6_altcat_1(_381492)], (314 ^ _371389) ^ [_381785, _381787] : [-(v9_altcat_1(_381785)), _381787 = _381785, v9_altcat_1(_381787)], (324 ^ _371389) ^ [_382080, _382082] : [-(v11_altcat_1(_382080)), _382082 = _382080, v11_altcat_1(_382082)], (334 ^ _371389) ^ [_382375, _382377] : [-(v2_yellow18(_382375)), _382377 = _382375, v2_yellow18(_382377)], (344 ^ _371389) ^ [_382670, _382672] : [-(v3_yellow18(_382670)), _382672 = _382670, v3_yellow18(_382672)], (354 ^ _371389) ^ [_382965, _382967] : [-(v4_yellow18(_382965)), _382967 = _382965, v4_yellow18(_382967)], (364 ^ _371389) ^ [_383260, _383262] : [-(v1_yellow21(_383260)), _383262 = _383260, v1_yellow21(_383262)], (374 ^ _371389) ^ [_383555, _383557] : [-(v2_yellow21(_383555)), _383557 = _383555, v2_yellow21(_383557)], (384 ^ _371389) ^ [_383850, _383852] : [-(v3_yellow21(_383850)), _383852 = _383850, v3_yellow21(_383852)], (394 ^ _371389) ^ [_384145, _384147] : [-(v1_relat_1(_384145)), _384147 = _384145, v1_relat_1(_384147)], (404 ^ _371389) ^ [_384440, _384442] : [-(v1_funct_1(_384440)), _384442 = _384440, v1_funct_1(_384442)], (414 ^ _371389) ^ [_384735, _384737] : [-(v2_funct_1(_384735)), _384737 = _384735, v2_funct_1(_384737)], (424 ^ _371389) ^ [_385030, _385032] : [-(v1_finset_1(_385030)), _385032 = _385030, v1_finset_1(_385032)], (434 ^ _371389) ^ [_385381, _385383, _385385, _385387, _385389, _385391] : [-(v11_functor0(_385389, _385385, _385381)), v11_functor0(_385391, _385387, _385383), _385391 = _385389, _385387 = _385385, _385383 = _385381], (452 ^ _371389) ^ [_385934, _385936] : [-(l1_struct_0(_385934)), _385936 = _385934, l1_struct_0(_385936)], (462 ^ _371389) ^ [_386229, _386231] : [-(v1_altcat_2(_386229)), _386231 = _386229, v1_altcat_2(_386231)], (472 ^ _371389) ^ [_386524, _386526] : [-(l1_altcat_1(_386524)), _386526 = _386524, l1_altcat_1(_386526)], (482 ^ _371389) ^ [_386875, _386877, _386879, _386881, _386883, _386885] : [-(l2_functor0(_386883, _386879, _386875)), l2_functor0(_386885, _386881, _386877), _386885 = _386883, _386881 = _386879, _386877 = _386875], (500 ^ _371389) ^ [_387484, _387486, _387488, _387490, _387492, _387494] : [-(v6_functor0(_387492, _387488, _387484)), v6_functor0(_387494, _387490, _387486), _387494 = _387492, _387490 = _387488, _387486 = _387484], (518 ^ _371389) ^ [_388093, _388095, _388097, _388099, _388101, _388103] : [-(v8_functor0(_388101, _388097, _388093)), v8_functor0(_388103, _388099, _388095), _388103 = _388101, _388099 = _388097, _388095 = _388093], (536 ^ _371389) ^ [_388702, _388704, _388706, _388708, _388710, _388712] : [-(v9_functor0(_388710, _388706, _388702)), v9_functor0(_388712, _388708, _388704), _388712 = _388710, _388708 = _388706, _388704 = _388702], (554 ^ _371389) ^ [_389311, _389313, _389315, _389317, _389319, _389321] : [-(v12_functor0(_389319, _389315, _389311)), v12_functor0(_389321, _389317, _389313), _389321 = _389319, _389317 = _389315, _389313 = _389311], (572 ^ _371389) ^ [_389920, _389922, _389924, _389926, _389928, _389930] : [-(m2_relset_1(_389928, _389924, _389920)), m2_relset_1(_389930, _389926, _389922), _389930 = _389928, _389926 = _389924, _389922 = _389920], (590 ^ _371389) ^ [_390529, _390531, _390533, _390535, _390537, _390539] : [-(m1_relset_1(_390537, _390533, _390529)), m1_relset_1(_390539, _390535, _390531), _390539 = _390537, _390535 = _390533, _390531 = _390529], (608 ^ _371389) ^ [_391082, _391084] : [-(v3_struct_0(_391082)), _391084 = _391082, v3_struct_0(_391084)], (618 ^ _371389) ^ [_391377, _391379] : [-(v2_altcat_1(_391377)), _391379 = _391377, v2_altcat_1(_391379)], (628 ^ _371389) ^ [_391672, _391674] : [-(v12_altcat_1(_391672)), _391674 = _391672, v12_altcat_1(_391674)], (638 ^ _371389) ^ [_391967, _391969] : [-(l2_altcat_1(_391967)), _391969 = _391967, l2_altcat_1(_391969)], (648 ^ _371389) ^ [_392290, _392292, _392294, _392296] : [-(r1_tarski(_392294, _392290)), r1_tarski(_392296, _392292), _392296 = _392294, _392292 = _392290], (662 ^ _371389) ^ [_392734, _392736, _392738, _392740] : [-(m1_subset_1(_392738, _392734)), m1_subset_1(_392740, _392736), _392740 = _392738, _392736 = _392734], (676 ^ _371389) ^ [_393178, _393180, _393182, _393184] : [-(r2_hidden(_393182, _393178)), r2_hidden(_393184, _393180), _393184 = _393182, _393180 = _393178], (690 ^ _371389) ^ [_393594, _393596] : [-(v1_xboole_0(_393594)), _393596 = _393594, v1_xboole_0(_393596)], (700 ^ _371389) ^ [_393889, _393891] : [-(v2_setfam_1(_393889)), _393891 = _393889, v2_setfam_1(_393891)], (710 ^ _371389) ^ [_394192, _394194, _394196, _394198] : [-(r2_functor0(_394196, _394192)), r2_functor0(_394198, _394194), _394198 = _394196, _394194 = _394192], (874 ^ _371389) ^ [_400470] : [l2_altcat_1(_400470), v6_altcat_1(_400470), -(_400470 = g2_altcat_1(u1_struct_0(_400470), u1_altcat_1(_400470), u2_altcat_1(_400470)))], (884 ^ _371389) ^ [_400789, _400791, _400793] : [v9_functor0(_400789, _400793, _400791), -(_400789 = g2_functor0(_400793, _400791, u1_functor0(_400793, _400791, _400789), u2_functor0(_400793, _400791, _400789))), l1_altcat_1(_400793), l1_altcat_1(_400791), l2_functor0(_400789, _400793, _400791)], (902 ^ _371389) ^ [_401312, _401314] : [r2_hidden(_401314, _401312), r2_hidden(_401312, _401314)], (908 ^ _371389) ^ [_401509] : [v1_membered(_401509), 911 ^ _371389 : [(912 ^ _371389) ^ [_401639] : [m1_subset_1(_401639, _401509), -(v1_xcmplx_0(_401639))]]], (918 ^ _371389) ^ [_401840] : [v2_membered(_401840), 921 ^ _371389 : [(922 ^ _371389) ^ [_401975] : [m1_subset_1(_401975, _401840), 925 ^ _371389 : [(926 ^ _371389) ^ [] : [-(v1_xcmplx_0(_401975))], (928 ^ _371389) ^ [] : [-(v1_xreal_0(_401975))]]]]], (930 ^ _371389) ^ [_402249] : [v3_membered(_402249), 933 ^ _371389 : [(934 ^ _371389) ^ [_402389] : [m1_subset_1(_402389, _402249), 937 ^ _371389 : [(938 ^ _371389) ^ [] : [-(v1_xcmplx_0(_402389))], (940 ^ _371389) ^ [] : [-(v1_xreal_0(_402389))], (942 ^ _371389) ^ [] : [-(v1_rat_1(_402389))]]]]], (944 ^ _371389) ^ [_402735] : [v4_membered(_402735), 947 ^ _371389 : [(948 ^ _371389) ^ [_402880] : [m1_subset_1(_402880, _402735), 951 ^ _371389 : [(952 ^ _371389) ^ [] : [-(v1_xcmplx_0(_402880))], (954 ^ _371389) ^ [] : [-(v1_xreal_0(_402880))], (956 ^ _371389) ^ [] : [-(v1_int_1(_402880))], (958 ^ _371389) ^ [] : [-(v1_rat_1(_402880))]]]]], (960 ^ _371389) ^ [_403298] : [v5_membered(_403298), 963 ^ _371389 : [(964 ^ _371389) ^ [_403448] : [m1_subset_1(_403448, _403298), 967 ^ _371389 : [(968 ^ _371389) ^ [] : [-(v1_xcmplx_0(_403448))], (970 ^ _371389) ^ [] : [-(v4_ordinal2(_403448))], (972 ^ _371389) ^ [] : [-(v1_xreal_0(_403448))], (974 ^ _371389) ^ [] : [-(v1_int_1(_403448))], (976 ^ _371389) ^ [] : [-(v1_rat_1(_403448))]]]]], (978 ^ _371389) ^ [_403938] : [v1_xboole_0(_403938), 981 ^ _371389 : [(982 ^ _371389) ^ [] : [-(v1_membered(_403938))], (984 ^ _371389) ^ [] : [-(v2_membered(_403938))], (986 ^ _371389) ^ [] : [-(v3_membered(_403938))], (988 ^ _371389) ^ [] : [-(v4_membered(_403938))], (990 ^ _371389) ^ [] : [-(v5_membered(_403938))]]], (992 ^ _371389) ^ [_404405] : [v1_membered(_404405), 995 ^ _371389 : [(996 ^ _371389) ^ [_404537] : [m1_subset_1(_404537, k1_zfmisc_1(_404405)), -(v1_membered(_404537))]]], (1002 ^ _371389) ^ [_404742] : [v2_membered(_404742), 1005 ^ _371389 : [(1006 ^ _371389) ^ [_404879] : [m1_subset_1(_404879, k1_zfmisc_1(_404742)), 1009 ^ _371389 : [(1010 ^ _371389) ^ [] : [-(v1_membered(_404879))], (1012 ^ _371389) ^ [] : [-(v2_membered(_404879))]]]]], (1014 ^ _371389) ^ [_405157] : [v3_membered(_405157), 1017 ^ _371389 : [(1018 ^ _371389) ^ [_405299] : [m1_subset_1(_405299, k1_zfmisc_1(_405157)), 1021 ^ _371389 : [(1022 ^ _371389) ^ [] : [-(v1_membered(_405299))], (1024 ^ _371389) ^ [] : [-(v2_membered(_405299))], (1026 ^ _371389) ^ [] : [-(v3_membered(_405299))]]]]], (1028 ^ _371389) ^ [_405649] : [v4_membered(_405649), 1031 ^ _371389 : [(1032 ^ _371389) ^ [_405796] : [m1_subset_1(_405796, k1_zfmisc_1(_405649)), 1035 ^ _371389 : [(1036 ^ _371389) ^ [] : [-(v1_membered(_405796))], (1038 ^ _371389) ^ [] : [-(v2_membered(_405796))], (1040 ^ _371389) ^ [] : [-(v3_membered(_405796))], (1042 ^ _371389) ^ [] : [-(v4_membered(_405796))]]]]], (1044 ^ _371389) ^ [_406218] : [v1_xboole_0(_406218), -(v1_finset_1(_406218))], (1050 ^ _371389) ^ [_406404] : [v1_xboole_0(_406404), -(v1_funct_1(_406404))], (1056 ^ _371389) ^ [_406646, _406648, _406650, _406652, _406654] : [1075 ^ _371389 : [(1076 ^ _371389) ^ [_407204] : [m1_functor0(_407204, _406654, _406652, _406650, _406648, _406646), -(v1_funcop_1(_407204))]], v1_funct_1(_406650), v1_funct_2(_406650, _406654, _406652), m1_relset_1(_406650, _406654, _406652), m1_pboole(_406648, _406654), m1_pboole(_406646, _406652)], (1082 ^ _371389) ^ [_407459, _407461] : [1109 ^ _371389 : [(1110 ^ _371389) ^ [_408131] : [m2_functor0(_408131, _407461, _407459), 1113 ^ _371389 : [(1114 ^ _371389) ^ [] : [-(v8_functor0(_408131, _407461, _407459))], (1116 ^ _371389) ^ [] : [-(v12_functor0(_408131, _407461, _407459))]]]], -(v3_struct_0(_407461)), v2_altcat_1(_407461), v12_altcat_1(_407461), l2_altcat_1(_407461), -(v3_struct_0(_407459)), v12_altcat_1(_407459), l2_altcat_1(_407459)], (1118 ^ _371389) ^ [_408425] : [v5_membered(_408425), -(v4_membered(_408425))], (1124 ^ _371389) ^ [_408639, _408641, _408643] : [m1_subset_1(_408639, k1_zfmisc_1(k2_zfmisc_1(_408643, _408641))), -(v1_relat_1(_408639))], (1130 ^ _371389) ^ [_408849] : [l2_altcat_1(_408849), 1153 ^ _371389 : [(1154 ^ _371389) ^ [] : [v3_struct_0(_408849)], (1156 ^ _371389) ^ [] : [-(v2_altcat_1(_408849))], (1158 ^ _371389) ^ [] : [-(v11_altcat_1(_408849))], (1160 ^ _371389) ^ [] : [-(v12_altcat_1(_408849))], (1162 ^ _371389) ^ [] : [-(v1_altcat_2(_408849))], (1164 ^ _371389) ^ [] : [-(v2_yellow21(_408849))]], -(v3_struct_0(_408849)), v2_altcat_1(_408849), v11_altcat_1(_408849), v12_altcat_1(_408849), v3_yellow21(_408849)], (1166 ^ _371389) ^ [_409805] : [v5_membered(_409805), 1169 ^ _371389 : [(1170 ^ _371389) ^ [_409957] : [m1_subset_1(_409957, k1_zfmisc_1(_409805)), 1173 ^ _371389 : [(1174 ^ _371389) ^ [] : [-(v1_membered(_409957))], (1176 ^ _371389) ^ [] : [-(v2_membered(_409957))], (1178 ^ _371389) ^ [] : [-(v3_membered(_409957))], (1180 ^ _371389) ^ [] : [-(v4_membered(_409957))], (1182 ^ _371389) ^ [] : [-(v5_membered(_409957))]]]]], (1184 ^ _371389) ^ [_410451] : [v1_finset_1(_410451), 1187 ^ _371389 : [(1188 ^ _371389) ^ [_410583] : [m1_subset_1(_410583, k1_zfmisc_1(_410451)), -(v1_finset_1(_410583))]]], (1194 ^ _371389) ^ [_410788] : [1205 ^ _371389 : [(1206 ^ _371389) ^ [] : [-(v1_relat_1(_410788))], (1208 ^ _371389) ^ [] : [-(v1_funct_1(_410788))], (1210 ^ _371389) ^ [] : [-(v2_funct_1(_410788))]], v1_relat_1(_410788), v1_xboole_0(_410788), v1_funct_1(_410788)], (1212 ^ _371389) ^ [_411281] : [l2_altcat_1(_411281), 1223 ^ _371389 : [(1224 ^ _371389) ^ [] : [v3_struct_0(_411281)], (1226 ^ _371389) ^ [] : [-(v1_altcat_2(_411281))]], -(v3_struct_0(_411281)), v12_altcat_1(_411281)], (1228 ^ _371389) ^ [_411708] : [v4_membered(_411708), -(v3_membered(_411708))], (1234 ^ _371389) ^ [_411894] : [-(v2_setfam_1(_411894)), v1_xboole_0(_411894)], (1240 ^ _371389) ^ [_412084] : [l2_altcat_1(_412084), 1263 ^ _371389 : [(1264 ^ _371389) ^ [] : [v3_struct_0(_412084)], (1266 ^ _371389) ^ [] : [-(v2_altcat_1(_412084))], (1268 ^ _371389) ^ [] : [-(v9_altcat_1(_412084))], (1270 ^ _371389) ^ [] : [-(v11_altcat_1(_412084))], (1272 ^ _371389) ^ [] : [-(v12_altcat_1(_412084))], (1274 ^ _371389) ^ [] : [-(v1_altcat_2(_412084))], (1276 ^ _371389) ^ [] : [-(v2_yellow18(_412084))], (1278 ^ _371389) ^ [] : [-(v3_yellow18(_412084))], (1280 ^ _371389) ^ [] : [-(v4_yellow18(_412084))], (1282 ^ _371389) ^ [] : [-(v1_yellow21(_412084))]], -(v3_struct_0(_412084)), v2_altcat_1(_412084), v11_altcat_1(_412084), v12_altcat_1(_412084), v2_yellow21(_412084)], (1284 ^ _371389) ^ [_413320] : [v3_membered(_413320), -(v2_membered(_413320))], (1290 ^ _371389) ^ [_413520, _413522] : [l1_struct_0(_413522), -(v3_struct_0(_413520)), l1_struct_0(_413520), 1301 ^ _371389 : [(1302 ^ _371389) ^ [_413841] : [l1_functor0(_413841, _413522, _413520), v11_functor0(_413841, _413522, _413520), -(v6_functor0(_413841, _413522, _413520))]]], (1312 ^ _371389) ^ [_414169, _414171] : [1339 ^ _371389 : [(1340 ^ _371389) ^ [_414869] : [m2_functor0(_414869, _414171, _414169), v16_functor0(_414869, _414171, _414169), 1347 ^ _371389 : [(1348 ^ _371389) ^ [] : [-(v6_functor0(_414869, _414171, _414169))], (1350 ^ _371389) ^ [] : [-(v8_functor0(_414869, _414171, _414169))], (1352 ^ _371389) ^ [] : [-(v11_functor0(_414869, _414171, _414169))], (1354 ^ _371389) ^ [] : [-(v12_functor0(_414869, _414171, _414169))], (1356 ^ _371389) ^ [] : [-(v14_functor0(_414869, _414171, _414169))]]]], -(v3_struct_0(_414171)), v2_altcat_1(_414171), v12_altcat_1(_414171), l2_altcat_1(_414171), -(v3_struct_0(_414169)), v12_altcat_1(_414169), l2_altcat_1(_414169)], (1358 ^ _371389) ^ [_415492] : [v2_membered(_415492), -(v1_membered(_415492))], (1364 ^ _371389) ^ [_415692, _415694] : [1391 ^ _371389 : [(1392 ^ _371389) ^ [_416392] : [m2_functor0(_416392, _415694, _415692), 1403 ^ _371389 : [(1404 ^ _371389) ^ [] : [-(v6_functor0(_416392, _415694, _415692))], (1406 ^ _371389) ^ [] : [-(v8_functor0(_416392, _415694, _415692))], (1408 ^ _371389) ^ [] : [-(v12_functor0(_416392, _415694, _415692))], (1410 ^ _371389) ^ [] : [-(v16_functor0(_416392, _415694, _415692))]], v11_functor0(_416392, _415694, _415692), v14_functor0(_416392, _415694, _415692)]], -(v3_struct_0(_415694)), v2_altcat_1(_415694), v12_altcat_1(_415694), l2_altcat_1(_415694), -(v3_struct_0(_415692)), v12_altcat_1(_415692), l2_altcat_1(_415692)], (1412 ^ _371389) ^ [_417046, _417048] : [1439 ^ _371389 : [(1440 ^ _371389) ^ [_417718] : [m2_functor0(_417718, _417048, _417046), v16_functor0(_417718, _417048, _417046), -(v6_functor0(_417718, _417048, _417046))]], -(v3_struct_0(_417048)), v2_altcat_1(_417048), v12_altcat_1(_417048), l2_altcat_1(_417048), -(v3_struct_0(_417046)), v12_altcat_1(_417046), l2_altcat_1(_417046)], (1450 ^ _371389) ^ [_418028] : [-(v3_struct_0(_418028)), v2_altcat_1(_418028), v12_altcat_1(_418028), l2_altcat_1(_418028), 1465 ^ _371389 : [(1466 ^ _371389) ^ [_418453] : [-(v3_struct_0(_418453)), v2_altcat_1(_418453), v12_altcat_1(_418453), l2_altcat_1(_418453), 1481 ^ _371389 : [(1482 ^ _371389) ^ [] : [r2_functor0(_418028, _418453), 1486 ^ _371389 : [(1487 ^ _371389) ^ [] : [-(m2_functor0(1485 ^ [_418028, _418453], _418028, _418453))], (1489 ^ _371389) ^ [] : [-(v21_functor0(1485 ^ [_418028, _418453], _418028, _418453))], (1491 ^ _371389) ^ [] : [-(v16_functor0(1485 ^ [_418028, _418453], _418028, _418453))]]], (1493 ^ _371389) ^ [] : [-(r2_functor0(_418028, _418453)), 1494 ^ _371389 : [(1495 ^ _371389) ^ [_419282] : [m2_functor0(_419282, _418028, _418453), v21_functor0(_419282, _418028, _418453), v16_functor0(_419282, _418028, _418453)]]]]]]], (1507 ^ _371389) ^ [_419689, _419691, _419693] : [1514 ^ _371389 : [(1515 ^ _371389) ^ [] : [-(v6_altcat_1(g2_altcat_1(_419693, _419691, _419689)))], (1517 ^ _371389) ^ [] : [-(l2_altcat_1(g2_altcat_1(_419693, _419691, _419689)))]], m1_pboole(_419691, k2_zfmisc_1(_419693, _419693)), m3_pboole(_419689, k3_zfmisc_1(_419693, _419693, _419693), k3_altcat_1(_419693, _419691, _419691), k2_altcat_1(_419693, _419691))], (1519 ^ _371389) ^ [_420147, _420149, _420151, _420153] : [1542 ^ _371389 : [(1543 ^ _371389) ^ [] : [-(v9_functor0(g2_functor0(_420153, _420151, _420149, _420147), _420153, _420151))], (1545 ^ _371389) ^ [] : [-(l2_functor0(g2_functor0(_420153, _420151, _420149, _420147), _420153, _420151))]], l1_altcat_1(_420153), l1_altcat_1(_420151), v1_funct_1(_420149), v1_funct_2(_420149, k2_zfmisc_1(u1_struct_0(_420153), u1_struct_0(_420153)), k2_zfmisc_1(u1_struct_0(_420151), u1_struct_0(_420151))), m1_relset_1(_420149, k2_zfmisc_1(u1_struct_0(_420153), u1_struct_0(_420153)), k2_zfmisc_1(u1_struct_0(_420151), u1_struct_0(_420151))), m1_functor0(_420147, k2_zfmisc_1(u1_struct_0(_420153), u1_struct_0(_420153)), k2_zfmisc_1(u1_struct_0(_420151), u1_struct_0(_420151)), _420149, u1_altcat_1(_420153), u1_altcat_1(_420151))], (1547 ^ _371389) ^ [] : [true___, -(true___)], (1553 ^ _371389) ^ [] : [true___, -(true___)], (1559 ^ _371389) ^ [_421293, _421295] : [m1_pboole(_421293, k2_zfmisc_1(_421295, _421295)), -(m1_pboole(k2_altcat_1(_421295, _421293), k3_zfmisc_1(_421295, _421295, _421295)))], (1565 ^ _371389) ^ [] : [true___, -(true___)], (1571 ^ _371389) ^ [_421656, _421658, _421660] : [-(m1_pboole(k3_altcat_1(_421660, _421658, _421656), k3_zfmisc_1(_421660, _421660, _421660))), m1_pboole(_421658, k2_zfmisc_1(_421660, _421660)), m1_pboole(_421656, k2_zfmisc_1(_421660, _421660))], (1581 ^ _371389) ^ [] : [true___, -(true___)], (1587 ^ _371389) ^ [_422098] : [-(v1_xboole_0(_422098)), 1590 ^ _371389 : [(1591 ^ _371389) ^ [] : [v3_struct_0(k4_waybel34(_422098))], (1593 ^ _371389) ^ [] : [-(v2_altcat_1(k4_waybel34(_422098)))], (1595 ^ _371389) ^ [] : [-(v6_altcat_1(k4_waybel34(_422098)))], (1597 ^ _371389) ^ [] : [-(v11_altcat_1(k4_waybel34(_422098)))], (1599 ^ _371389) ^ [] : [-(v12_altcat_1(k4_waybel34(_422098)))], (1601 ^ _371389) ^ [] : [-(v2_yellow21(k4_waybel34(_422098)))], (1603 ^ _371389) ^ [] : [-(l2_altcat_1(k4_waybel34(_422098)))]]], (1605 ^ _371389) ^ [_422737] : [-(v1_xboole_0(_422737)), 1608 ^ _371389 : [(1609 ^ _371389) ^ [] : [v3_struct_0(k5_waybel34(_422737))], (1611 ^ _371389) ^ [] : [-(v2_altcat_1(k5_waybel34(_422737)))], (1613 ^ _371389) ^ [] : [-(v6_altcat_1(k5_waybel34(_422737)))], (1615 ^ _371389) ^ [] : [-(v11_altcat_1(k5_waybel34(_422737)))], (1617 ^ _371389) ^ [] : [-(v12_altcat_1(k5_waybel34(_422737)))], (1619 ^ _371389) ^ [] : [-(v2_yellow21(k5_waybel34(_422737)))], (1621 ^ _371389) ^ [] : [-(l2_altcat_1(k5_waybel34(_422737)))]]], (1623 ^ _371389) ^ [_423376] : [-(v2_setfam_1(_423376)), 1626 ^ _371389 : [(1627 ^ _371389) ^ [] : [-(v9_functor0(k6_waybel34(_423376), k4_waybel34(_423376), k5_waybel34(_423376)))], (1629 ^ _371389) ^ [] : [-(v16_functor0(k6_waybel34(_423376), k4_waybel34(_423376), k5_waybel34(_423376)))], (1631 ^ _371389) ^ [] : [-(m2_functor0(k6_waybel34(_423376), k4_waybel34(_423376), k5_waybel34(_423376)))]]], (1633 ^ _371389) ^ [_423754] : [l1_altcat_1(_423754), -(l1_struct_0(_423754))], (1639 ^ _371389) ^ [] : [true___, -(true___)], (1645 ^ _371389) ^ [] : [true___, -(true___)], (1651 ^ _371389) ^ [_424178] : [l2_altcat_1(_424178), -(l1_altcat_1(_424178))], (1657 ^ _371389) ^ [_424378, _424380] : [l1_altcat_1(_424380), l1_altcat_1(_424378), 1664 ^ _371389 : [(1665 ^ _371389) ^ [_424602] : [l2_functor0(_424602, _424380, _424378), -(l1_functor0(_424602, _424380, _424378))]]], (1671 ^ _371389) ^ [_424875, _424877, _424879, _424881, _424883] : [1690 ^ _371389 : [(1691 ^ _371389) ^ [_425434] : [m1_functor0(_425434, _424883, _424881, _424879, _424877, _424875), -(m1_pboole(_425434, _424883))]], v1_funct_1(_424879), v1_funct_2(_424879, _424883, _424881), m1_relset_1(_424879, _424883, _424881), m1_pboole(_424877, _424883), m1_pboole(_424875, _424881)], (1697 ^ _371389) ^ [_425691, _425693] : [m1_pboole(_425691, _425693), 1700 ^ _371389 : [(1701 ^ _371389) ^ [] : [-(v1_relat_1(_425691))], (1703 ^ _371389) ^ [] : [-(v1_funct_1(_425691))]]], (1705 ^ _371389) ^ [] : [true___, -(true___)], (1711 ^ _371389) ^ [] : [true___, -(true___)], (1717 ^ _371389) ^ [_426210, _426212] : [1744 ^ _371389 : [(1745 ^ _371389) ^ [_426875] : [m2_functor0(_426875, _426212, _426210), -(l2_functor0(_426875, _426212, _426210))]], -(v3_struct_0(_426212)), v2_altcat_1(_426212), v12_altcat_1(_426212), l2_altcat_1(_426212), -(v3_struct_0(_426210)), v12_altcat_1(_426210), l2_altcat_1(_426210)], (1751 ^ _371389) ^ [_427118, _427120, _427122] : [m2_relset_1(_427118, _427122, _427120), -(m1_subset_1(_427118, k1_zfmisc_1(k2_zfmisc_1(_427122, _427120))))], (1757 ^ _371389) ^ [_427360, _427362, _427364] : [m1_pboole(_427362, _427364), m1_pboole(_427360, _427364), 1764 ^ _371389 : [(1765 ^ _371389) ^ [_427596] : [m3_pboole(_427596, _427364, _427362, _427360), -(m1_pboole(_427596, _427364))]]], (1771 ^ _371389) ^ [_427821] : [l1_altcat_1(_427821), -(m1_pboole(u1_altcat_1(_427821), k2_zfmisc_1(u1_struct_0(_427821), u1_struct_0(_427821))))], (1777 ^ _371389) ^ [_428055, _428057, _428059] : [1788 ^ _371389 : [(1789 ^ _371389) ^ [] : [-(v1_funct_1(u1_functor0(_428059, _428057, _428055)))], (1791 ^ _371389) ^ [] : [-(v1_funct_2(u1_functor0(_428059, _428057, _428055), k2_zfmisc_1(u1_struct_0(_428059), u1_struct_0(_428059)), k2_zfmisc_1(u1_struct_0(_428057), u1_struct_0(_428057))))], (1793 ^ _371389) ^ [] : [-(m2_relset_1(u1_functor0(_428059, _428057, _428055), k2_zfmisc_1(u1_struct_0(_428059), u1_struct_0(_428059)), k2_zfmisc_1(u1_struct_0(_428057), u1_struct_0(_428057))))]], l1_struct_0(_428059), l1_struct_0(_428057), l1_functor0(_428055, _428059, _428057)], (1795 ^ _371389) ^ [] : [true___, -(true___)], (1801 ^ _371389) ^ [_428795] : [l2_altcat_1(_428795), -(m3_pboole(u2_altcat_1(_428795), k3_zfmisc_1(u1_struct_0(_428795), u1_struct_0(_428795), u1_struct_0(_428795)), k3_altcat_1(u1_struct_0(_428795), u1_altcat_1(_428795), u1_altcat_1(_428795)), k2_altcat_1(u1_struct_0(_428795), u1_altcat_1(_428795))))], (1807 ^ _371389) ^ [_429073, _429075, _429077] : [-(m1_functor0(u2_functor0(_429077, _429075, _429073), k2_zfmisc_1(u1_struct_0(_429077), u1_struct_0(_429077)), k2_zfmisc_1(u1_struct_0(_429075), u1_struct_0(_429075)), u1_functor0(_429077, _429075, _429073), u1_altcat_1(_429077), u1_altcat_1(_429075))), l1_altcat_1(_429077), l1_altcat_1(_429075), l2_functor0(_429073, _429077, _429075)], (1822 ^ _371389) ^ [] : [-(l1_altcat_1(1820 ^ []))], (1824 ^ _371389) ^ [_429622, _429624] : [-(l1_functor0(1831 ^ [_429622, _429624], _429624, _429622)), l1_struct_0(_429624), l1_struct_0(_429622)], (1836 ^ _371389) ^ [] : [-(l1_struct_0(1834 ^ []))], (1839 ^ _371389) ^ [] : [-(l2_altcat_1(1837 ^ []))], (1841 ^ _371389) ^ [_430155, _430157] : [-(l2_functor0(1848 ^ [_430155, _430157], _430157, _430155)), l1_altcat_1(_430157), l1_altcat_1(_430155)], (1852 ^ _371389) ^ [_430552, _430554, _430556, _430558, _430560] : [-(m1_functor0(1871 ^ [_430552, _430554, _430556, _430558, _430560], _430560, _430558, _430556, _430554, _430552)), v1_funct_1(_430556), v1_funct_2(_430556, _430560, _430558), m1_relset_1(_430556, _430560, _430558), m1_pboole(_430554, _430560), m1_pboole(_430552, _430558)], (1876 ^ _371389) ^ [_431283] : [-(m1_pboole(1874 ^ [_431283], _431283))], (1879 ^ _371389) ^ [_431422, _431424] : [-(m1_relset_1(1877 ^ [_431422, _431424], _431424, _431422))], (1882 ^ _371389) ^ [_431549] : [-(m1_subset_1(1880 ^ [_431549], _431549))], (1884 ^ _371389) ^ [_431661, _431663] : [-(m2_functor0(1911 ^ [_431661, _431663], _431663, _431661)), -(v3_struct_0(_431663)), v2_altcat_1(_431663), v12_altcat_1(_431663), l2_altcat_1(_431663), -(v3_struct_0(_431661)), v12_altcat_1(_431661), l2_altcat_1(_431661)], (1916 ^ _371389) ^ [_432484, _432486] : [-(m2_relset_1(1914 ^ [_432484, _432486], _432486, _432484))], (1918 ^ _371389) ^ [_432615, _432617, _432619] : [-(m3_pboole(1925 ^ [_432615, _432617, _432619], _432619, _432617, _432615)), m1_pboole(_432617, _432619), m1_pboole(_432615, _432619)], (1929 ^ _371389) ^ [_432993, _432995] : [-(v1_finset_1(k2_zfmisc_1(_432995, _432993))), v1_finset_1(_432995), v1_finset_1(_432993)], (1939 ^ _371389) ^ [_433306, _433308, _433310] : [-(v1_finset_1(k3_zfmisc_1(_433310, _433308, _433306))), v1_finset_1(_433310), v1_finset_1(_433308), v1_finset_1(_433306)], (1953 ^ _371389) ^ [_433694] : [v1_xboole_0(u1_struct_0(_433694)), -(v3_struct_0(_433694)), l1_struct_0(_433694)], (1963 ^ _371389) ^ [_433971] : [-(v2_setfam_1(_433971)), 1966 ^ _371389 : [(1967 ^ _371389) ^ [] : [v3_struct_0(k4_waybel34(_433971))], (1969 ^ _371389) ^ [] : [-(v2_altcat_1(k4_waybel34(_433971)))], (1971 ^ _371389) ^ [] : [-(v6_altcat_1(k4_waybel34(_433971)))], (1973 ^ _371389) ^ [] : [-(v9_altcat_1(k4_waybel34(_433971)))], (1975 ^ _371389) ^ [] : [-(v11_altcat_1(k4_waybel34(_433971)))], (1977 ^ _371389) ^ [] : [-(v12_altcat_1(k4_waybel34(_433971)))], (1979 ^ _371389) ^ [] : [-(v1_altcat_2(k4_waybel34(_433971)))], (1981 ^ _371389) ^ [] : [-(v2_yellow18(k4_waybel34(_433971)))], (1983 ^ _371389) ^ [] : [-(v3_yellow18(k4_waybel34(_433971)))], (1985 ^ _371389) ^ [] : [-(v4_yellow18(k4_waybel34(_433971)))], (1987 ^ _371389) ^ [] : [-(v1_yellow21(k4_waybel34(_433971)))], (1989 ^ _371389) ^ [] : [-(v2_yellow21(k4_waybel34(_433971)))], (1991 ^ _371389) ^ [] : [-(v3_yellow21(k4_waybel34(_433971)))]]], (1993 ^ _371389) ^ [] : [-(v1_xboole_0(k1_xboole_0))], (1995 ^ _371389) ^ [] : [-(v1_membered(k1_xboole_0))], (1997 ^ _371389) ^ [] : [-(v2_membered(k1_xboole_0))], (1999 ^ _371389) ^ [] : [-(v3_membered(k1_xboole_0))], (2001 ^ _371389) ^ [] : [-(v4_membered(k1_xboole_0))], (2003 ^ _371389) ^ [] : [-(v5_membered(k1_xboole_0))], (2005 ^ _371389) ^ [_435382] : [-(v2_setfam_1(_435382)), 2008 ^ _371389 : [(2009 ^ _371389) ^ [] : [v3_struct_0(k5_waybel34(_435382))], (2011 ^ _371389) ^ [] : [-(v2_altcat_1(k5_waybel34(_435382)))], (2013 ^ _371389) ^ [] : [-(v6_altcat_1(k5_waybel34(_435382)))], (2015 ^ _371389) ^ [] : [-(v9_altcat_1(k5_waybel34(_435382)))], (2017 ^ _371389) ^ [] : [-(v11_altcat_1(k5_waybel34(_435382)))], (2019 ^ _371389) ^ [] : [-(v12_altcat_1(k5_waybel34(_435382)))], (2021 ^ _371389) ^ [] : [-(v1_altcat_2(k5_waybel34(_435382)))], (2023 ^ _371389) ^ [] : [-(v2_yellow18(k5_waybel34(_435382)))], (2025 ^ _371389) ^ [] : [-(v3_yellow18(k5_waybel34(_435382)))], (2027 ^ _371389) ^ [] : [-(v4_yellow18(k5_waybel34(_435382)))], (2029 ^ _371389) ^ [] : [-(v1_yellow21(k5_waybel34(_435382)))], (2031 ^ _371389) ^ [] : [-(v2_yellow21(k5_waybel34(_435382)))], (2033 ^ _371389) ^ [] : [-(v3_yellow21(k5_waybel34(_435382)))]]], (2035 ^ _371389) ^ [_436493, _436495, _436497] : [2046 ^ _371389 : [(2047 ^ _371389) ^ [] : [-(v1_relat_1(u2_functor0(_436497, _436495, _436493)))], (2049 ^ _371389) ^ [] : [-(v1_funct_1(u2_functor0(_436497, _436495, _436493)))], (2051 ^ _371389) ^ [] : [-(v1_funcop_1(u2_functor0(_436497, _436495, _436493)))]], l1_altcat_1(_436497), l1_altcat_1(_436495), l2_functor0(_436493, _436497, _436495)], (2053 ^ _371389) ^ [_437050] : [-(v2_setfam_1(_437050)), 2056 ^ _371389 : [(2057 ^ _371389) ^ [] : [-(v6_functor0(k6_waybel34(_437050), k4_waybel34(_437050), k5_waybel34(_437050)))], (2059 ^ _371389) ^ [] : [-(v8_functor0(k6_waybel34(_437050), k4_waybel34(_437050), k5_waybel34(_437050)))], (2061 ^ _371389) ^ [] : [-(v9_functor0(k6_waybel34(_437050), k4_waybel34(_437050), k5_waybel34(_437050)))], (2063 ^ _371389) ^ [] : [-(v11_functor0(k6_waybel34(_437050), k4_waybel34(_437050), k5_waybel34(_437050)))], (2065 ^ _371389) ^ [] : [-(v12_functor0(k6_waybel34(_437050), k4_waybel34(_437050), k5_waybel34(_437050)))], (2067 ^ _371389) ^ [] : [-(v14_functor0(k6_waybel34(_437050), k4_waybel34(_437050), k5_waybel34(_437050)))], (2069 ^ _371389) ^ [] : [-(v16_functor0(k6_waybel34(_437050), k4_waybel34(_437050), k5_waybel34(_437050)))], (2071 ^ _371389) ^ [] : [-(v21_functor0(k6_waybel34(_437050), k4_waybel34(_437050), k5_waybel34(_437050)))]]], (2073 ^ _371389) ^ [_437886, _437888, _437890] : [m1_pboole(_437888, k2_zfmisc_1(_437890, _437890)), m3_pboole(_437886, k3_zfmisc_1(_437890, _437890, _437890), k3_altcat_1(_437890, _437888, _437888), k2_altcat_1(_437890, _437888)), 2080 ^ _371389 : [(2081 ^ _371389) ^ [_438210, _438212, _438214] : [g2_altcat_1(_437890, _437888, _437886) = g2_altcat_1(_438214, _438212, _438210), 2084 ^ _371389 : [(2085 ^ _371389) ^ [] : [-(_437890 = _438214)], (2087 ^ _371389) ^ [] : [-(_437888 = _438212)], (2089 ^ _371389) ^ [] : [-(_437886 = _438210)]]]]], (2091 ^ _371389) ^ [_438666, _438668, _438670, _438672] : [2114 ^ _371389 : [(2115 ^ _371389) ^ [_439479, _439481, _439483, _439485] : [g2_functor0(_438672, _438670, _438668, _438666) = g2_functor0(_439485, _439483, _439481, _439479), 2118 ^ _371389 : [(2119 ^ _371389) ^ [] : [-(_438672 = _439485)], (2121 ^ _371389) ^ [] : [-(_438670 = _439483)], (2123 ^ _371389) ^ [] : [-(_438668 = _439481)], (2125 ^ _371389) ^ [] : [-(_438666 = _439479)]]]], l1_altcat_1(_438672), l1_altcat_1(_438670), v1_funct_1(_438668), v1_funct_2(_438668, k2_zfmisc_1(u1_struct_0(_438672), u1_struct_0(_438672)), k2_zfmisc_1(u1_struct_0(_438670), u1_struct_0(_438670))), m1_relset_1(_438668, k2_zfmisc_1(u1_struct_0(_438672), u1_struct_0(_438672)), k2_zfmisc_1(u1_struct_0(_438670), u1_struct_0(_438670))), m1_functor0(_438666, k2_zfmisc_1(u1_struct_0(_438672), u1_struct_0(_438672)), k2_zfmisc_1(u1_struct_0(_438670), u1_struct_0(_438670)), _438668, u1_altcat_1(_438672), u1_altcat_1(_438670))], (2128 ^ _371389) ^ [] : [v1_xboole_0(2126 ^ [])], (2130 ^ _371389) ^ [] : [-(v1_finset_1(2126 ^ []))], (2133 ^ _371389) ^ [] : [-(v1_relat_1(2131 ^ []))], (2135 ^ _371389) ^ [] : [-(v1_funct_1(2131 ^ []))], (2138 ^ _371389) ^ [] : [v1_xboole_0(2136 ^ [])], (2140 ^ _371389) ^ [] : [-(v1_membered(2136 ^ []))], (2142 ^ _371389) ^ [] : [-(v2_membered(2136 ^ []))], (2144 ^ _371389) ^ [] : [-(v3_membered(2136 ^ []))], (2146 ^ _371389) ^ [] : [-(v4_membered(2136 ^ []))], (2148 ^ _371389) ^ [] : [-(v5_membered(2136 ^ []))], (2151 ^ _371389) ^ [] : [-(l2_altcat_1(2149 ^ []))], (2153 ^ _371389) ^ [] : [v3_struct_0(2149 ^ [])], (2155 ^ _371389) ^ [] : [-(v2_altcat_1(2149 ^ []))], (2157 ^ _371389) ^ [] : [-(v6_altcat_1(2149 ^ []))], (2159 ^ _371389) ^ [] : [-(v9_altcat_1(2149 ^ []))], (2161 ^ _371389) ^ [] : [-(v11_altcat_1(2149 ^ []))], (2163 ^ _371389) ^ [] : [-(v12_altcat_1(2149 ^ []))], (2165 ^ _371389) ^ [] : [-(v1_altcat_2(2149 ^ []))], (2167 ^ _371389) ^ [] : [-(v2_yellow18(2149 ^ []))], (2169 ^ _371389) ^ [] : [-(v3_yellow18(2149 ^ []))], (2171 ^ _371389) ^ [] : [-(v4_yellow18(2149 ^ []))], (2173 ^ _371389) ^ [] : [-(v1_yellow21(2149 ^ []))], (2175 ^ _371389) ^ [] : [-(v2_yellow21(2149 ^ []))], (2177 ^ _371389) ^ [] : [-(v3_yellow21(2149 ^ []))], (2180 ^ _371389) ^ [] : [-(v1_relat_1(2178 ^ []))], (2182 ^ _371389) ^ [] : [-(v1_xboole_0(2178 ^ []))], (2184 ^ _371389) ^ [] : [-(v1_funct_1(2178 ^ []))], (2187 ^ _371389) ^ [] : [v2_setfam_1(2185 ^ [])], (2189 ^ _371389) ^ [_441861] : [-(v1_xboole_0(_441861)), 2193 ^ _371389 : [(2194 ^ _371389) ^ [] : [-(m1_subset_1(2192 ^ [_441861], k1_zfmisc_1(_441861)))], (2196 ^ _371389) ^ [] : [v1_xboole_0(2192 ^ [_441861])], (2198 ^ _371389) ^ [] : [-(v1_finset_1(2192 ^ [_441861]))]]], (2201 ^ _371389) ^ [] : [-(v1_relat_1(2199 ^ []))], (2203 ^ _371389) ^ [] : [-(v1_funct_1(2199 ^ []))], (2205 ^ _371389) ^ [] : [-(v2_funct_1(2199 ^ []))], (2207 ^ _371389) ^ [_442496, _442498] : [2215 ^ _371389 : [(2216 ^ _371389) ^ [] : [-(l2_functor0(2214 ^ [_442496, _442498], _442498, _442496))], (2218 ^ _371389) ^ [] : [-(v9_functor0(2214 ^ [_442496, _442498], _442498, _442496))]], l1_altcat_1(_442498), l1_altcat_1(_442496)], (2220 ^ _371389) ^ [_442928] : [-(v2_setfam_1(_442928)), 2224 ^ _371389 : [(2225 ^ _371389) ^ [] : [-(m1_subset_1(2223 ^ [_442928], _442928))], (2227 ^ _371389) ^ [] : [v1_xboole_0(2223 ^ [_442928])]]], (2230 ^ _371389) ^ [] : [-(l1_struct_0(2228 ^ []))], (2232 ^ _371389) ^ [] : [v3_struct_0(2228 ^ [])], (2234 ^ _371389) ^ [_443404] : [-(v1_xboole_0(_443404)), 2238 ^ _371389 : [(2239 ^ _371389) ^ [] : [-(m1_subset_1(2237 ^ [_443404], k1_zfmisc_1(_443404)))], (2241 ^ _371389) ^ [] : [v1_xboole_0(2237 ^ [_443404])], (2243 ^ _371389) ^ [] : [-(v1_finset_1(2237 ^ [_443404]))]]], (2245 ^ _371389) ^ [_443830, _443832] : [2253 ^ _371389 : [(2254 ^ _371389) ^ [] : [-(l2_functor0(2252 ^ [_443830, _443832], _443832, _443830))], (2256 ^ _371389) ^ [] : [-(v11_functor0(2252 ^ [_443830, _443832], _443832, _443830))]], l1_altcat_1(_443832), l1_altcat_1(_443830)], (2258 ^ _371389) ^ [_444262] : [2266 ^ _371389 : [(2267 ^ _371389) ^ [] : [-(m1_subset_1(2265 ^ [_444262], k1_zfmisc_1(u1_struct_0(_444262))))], (2269 ^ _371389) ^ [] : [v1_xboole_0(2265 ^ [_444262])]], -(v3_struct_0(_444262)), l1_struct_0(_444262)], (2272 ^ _371389) ^ [] : [-(l2_altcat_1(2270 ^ []))], (2274 ^ _371389) ^ [] : [v3_struct_0(2270 ^ [])], (2276 ^ _371389) ^ [] : [-(v1_altcat_2(2270 ^ []))], (2278 ^ _371389) ^ [_444907, _444909] : [2298 ^ _371389 : [(2299 ^ _371389) ^ [] : [-(l2_functor0(2297 ^ [_444907, _444909], _444909, _444907))], (2301 ^ _371389) ^ [] : [-(v6_functor0(2297 ^ [_444907, _444909], _444909, _444907))], (2303 ^ _371389) ^ [] : [-(v8_functor0(2297 ^ [_444907, _444909], _444909, _444907))]], -(v3_struct_0(_444909)), l1_altcat_1(_444909), -(v3_struct_0(_444907)), v1_altcat_2(_444907), l1_altcat_1(_444907)], (2305 ^ _371389) ^ [_445710, _445712] : [2329 ^ _371389 : [(2330 ^ _371389) ^ [] : [-(l2_functor0(2328 ^ [_445710, _445712], _445712, _445710))], (2332 ^ _371389) ^ [] : [-(v6_functor0(2328 ^ [_445710, _445712], _445712, _445710))], (2334 ^ _371389) ^ [] : [-(v8_functor0(2328 ^ [_445710, _445712], _445712, _445710))], (2336 ^ _371389) ^ [] : [-(v9_functor0(2328 ^ [_445710, _445712], _445712, _445710))], (2338 ^ _371389) ^ [] : [-(v12_functor0(2328 ^ [_445710, _445712], _445712, _445710))]], -(v3_struct_0(_445712)), v12_altcat_1(_445712), l2_altcat_1(_445712), -(v3_struct_0(_445710)), v12_altcat_1(_445710), l2_altcat_1(_445710)], (2340 ^ _371389) ^ [_446823, _446825, _446827] : [m2_relset_1(_446823, _446827, _446825), -(m1_relset_1(_446823, _446827, _446825))], (2346 ^ _371389) ^ [_446995, _446997, _446999] : [m1_relset_1(_446995, _446999, _446997), -(m2_relset_1(_446995, _446999, _446997))], (2352 ^ _371389) ^ [_447202, _447204] : [-(r1_tarski(_447204, _447204))], (2354 ^ _371389) ^ [_447311, _447313] : [r2_functor0(_447313, _447311), -(r2_functor0(_447311, _447313)), -(v3_struct_0(_447313)), v2_altcat_1(_447313), v12_altcat_1(_447313), l2_altcat_1(_447313), -(v3_struct_0(_447311)), v2_altcat_1(_447311), v12_altcat_1(_447311), l2_altcat_1(_447311)], (2392 ^ _371389) ^ [_448225, _448227] : [r2_hidden(_448227, _448225), -(m1_subset_1(_448227, _448225))], (2398 ^ _371389) ^ [_448435, _448437] : [m1_subset_1(_448437, _448435), -(v1_xboole_0(_448435)), -(r2_hidden(_448437, _448435))], (2408 ^ _371389) ^ [_448762, _448764] : [m1_subset_1(_448764, k1_zfmisc_1(_448762)), -(r1_tarski(_448764, _448762))], (2414 ^ _371389) ^ [_448928, _448930] : [r1_tarski(_448930, _448928), -(m1_subset_1(_448930, k1_zfmisc_1(_448928)))], (2420 ^ _371389) ^ [_449158, _449160, _449162] : [-(m1_subset_1(_449162, _449158)), r2_hidden(_449162, _449160), m1_subset_1(_449160, k1_zfmisc_1(_449158))], (2430 ^ _371389) ^ [_449485, _449487, _449489] : [r2_hidden(_449489, _449487), m1_subset_1(_449487, k1_zfmisc_1(_449485)), v1_xboole_0(_449485)], (2440 ^ _371389) ^ [_449781] : [v1_xboole_0(_449781), -(_449781 = k1_xboole_0)], (2446 ^ _371389) ^ [_449983, _449985] : [r2_hidden(_449985, _449983), v1_xboole_0(_449983)], (2452 ^ _371389) ^ [_450170, _450172] : [v1_xboole_0(_450172), -(_450172 = _450170), v1_xboole_0(_450170)]], input).
% 0.84/1.39 ncf('1',plain,[r2_functor0(k4_waybel34(2461 ^ []), k5_waybel34(2461 ^ []))],start(2465 ^ 0)).
% 0.84/1.39 ncf('1.1',plain,[-(r2_functor0(k4_waybel34(2461 ^ []), k5_waybel34(2461 ^ []))), 1495 : m2_functor0(k6_waybel34(2461 ^ []), k4_waybel34(2461 ^ []), k5_waybel34(2461 ^ [])), 1495 : v21_functor0(k6_waybel34(2461 ^ []), k4_waybel34(2461 ^ []), k5_waybel34(2461 ^ [])), 1495 : v16_functor0(k6_waybel34(2461 ^ []), k4_waybel34(2461 ^ []), k5_waybel34(2461 ^ [])), 1493 : -(v3_struct_0(k5_waybel34(2461 ^ []))), 1493 : v2_altcat_1(k5_waybel34(2461 ^ [])), 1493 : v12_altcat_1(k5_waybel34(2461 ^ [])), 1493 : l2_altcat_1(k5_waybel34(2461 ^ [])), 1466 : -(v3_struct_0(k4_waybel34(2461 ^ []))), 1466 : v2_altcat_1(k4_waybel34(2461 ^ [])), 1466 : v12_altcat_1(k4_waybel34(2461 ^ [])), 1466 : l2_altcat_1(k4_waybel34(2461 ^ []))],extension(1450 ^ 1,bind([[_418028, _418453, _419282], [k4_waybel34(2461 ^ []), k5_waybel34(2461 ^ []), k6_waybel34(2461 ^ [])]]))).
% 0.84/1.39 ncf('1.1.1',plain,[-(m2_functor0(k6_waybel34(2461 ^ []), k4_waybel34(2461 ^ []), k5_waybel34(2461 ^ []))), m2_functor0(k6_waybel34(2461 ^ []), k4_waybel34(2461 ^ []), k5_waybel34(2461 ^ [])), k6_waybel34(2461 ^ []) = k6_waybel34(2461 ^ []), k4_waybel34(2461 ^ []) = k4_waybel34(2461 ^ []), k5_waybel34(2461 ^ []) = k5_waybel34(2461 ^ [])],extension(88 ^ 8,bind([[_374297, _374299, _374301, _374303, _374305, _374307], [k5_waybel34(2461 ^ []), k5_waybel34(2461 ^ []), k4_waybel34(2461 ^ []), k4_waybel34(2461 ^ []), k6_waybel34(2461 ^ []), k6_waybel34(2461 ^ [])]]))).
% 0.84/1.39 ncf('1.1.1.1',plain,[-(m2_functor0(k6_waybel34(2461 ^ []), k4_waybel34(2461 ^ []), k5_waybel34(2461 ^ []))), -(v2_setfam_1(2461 ^ []))],extension(1623 ^ 9,bind([[_423376], [2461 ^ []]]))).
% 0.84/1.39 ncf('1.1.1.1.1',plain,[v2_setfam_1(2461 ^ [])],extension(2463 ^ 10)).
% 0.84/1.39 ncf('1.1.1.2',plain,[-(k6_waybel34(2461 ^ []) = k6_waybel34(2461 ^ []))],extension(2 ^ 9,bind([[_371533], [k6_waybel34(2461 ^ [])]]))).
% 0.84/1.39 ncf('1.1.1.3',plain,[-(k4_waybel34(2461 ^ []) = k4_waybel34(2461 ^ []))],extension(2 ^ 9,bind([[_371533], [k4_waybel34(2461 ^ [])]]))).
% 0.84/1.39 ncf('1.1.1.4',plain,[-(k5_waybel34(2461 ^ []) = k5_waybel34(2461 ^ []))],extension(2 ^ 9,bind([[_371533], [k5_waybel34(2461 ^ [])]]))).
% 0.84/1.39 ncf('1.1.2',plain,[-(v21_functor0(k6_waybel34(2461 ^ []), k4_waybel34(2461 ^ []), k5_waybel34(2461 ^ []))), v21_functor0(k6_waybel34(2461 ^ []), k4_waybel34(2461 ^ []), k5_waybel34(2461 ^ [])), k6_waybel34(2461 ^ []) = k6_waybel34(2461 ^ []), k4_waybel34(2461 ^ []) = k4_waybel34(2461 ^ []), k5_waybel34(2461 ^ []) = k5_waybel34(2461 ^ [])],extension(152 ^ 8,bind([[_376419, _376421, _376423, _376425, _376427, _376429], [k5_waybel34(2461 ^ []), k5_waybel34(2461 ^ []), k4_waybel34(2461 ^ []), k4_waybel34(2461 ^ []), k6_waybel34(2461 ^ []), k6_waybel34(2461 ^ [])]]))).
% 0.84/1.39 ncf('1.1.2.1',plain,[-(v21_functor0(k6_waybel34(2461 ^ []), k4_waybel34(2461 ^ []), k5_waybel34(2461 ^ []))), -(v2_setfam_1(2461 ^ []))],extension(2053 ^ 9,bind([[_437050], [2461 ^ []]]))).
% 0.84/1.39 ncf('1.1.2.1.1',plain,[v2_setfam_1(2461 ^ [])],extension(2463 ^ 10)).
% 0.84/1.39 ncf('1.1.2.2',plain,[-(k6_waybel34(2461 ^ []) = k6_waybel34(2461 ^ []))],extension(2 ^ 9,bind([[_371533], [k6_waybel34(2461 ^ [])]]))).
% 0.84/1.39 ncf('1.1.2.3',plain,[-(k4_waybel34(2461 ^ []) = k4_waybel34(2461 ^ []))],extension(2 ^ 9,bind([[_371533], [k4_waybel34(2461 ^ [])]]))).
% 0.84/1.39 ncf('1.1.2.4',plain,[-(k5_waybel34(2461 ^ []) = k5_waybel34(2461 ^ []))],extension(2 ^ 9,bind([[_371533], [k5_waybel34(2461 ^ [])]]))).
% 0.84/1.39 ncf('1.1.3',plain,[-(v16_functor0(k6_waybel34(2461 ^ []), k4_waybel34(2461 ^ []), k5_waybel34(2461 ^ []))), v16_functor0(k6_waybel34(2461 ^ []), k4_waybel34(2461 ^ []), k5_waybel34(2461 ^ [])), k6_waybel34(2461 ^ []) = k6_waybel34(2461 ^ []), k4_waybel34(2461 ^ []) = k4_waybel34(2461 ^ []), k5_waybel34(2461 ^ []) = k5_waybel34(2461 ^ [])],extension(134 ^ 8,bind([[_375810, _375812, _375814, _375816, _375818, _375820], [k5_waybel34(2461 ^ []), k5_waybel34(2461 ^ []), k4_waybel34(2461 ^ []), k4_waybel34(2461 ^ []), k6_waybel34(2461 ^ []), k6_waybel34(2461 ^ [])]]))).
% 0.84/1.39 ncf('1.1.3.1',plain,[-(v16_functor0(k6_waybel34(2461 ^ []), k4_waybel34(2461 ^ []), k5_waybel34(2461 ^ []))), -(v2_setfam_1(2461 ^ []))],extension(1623 ^ 9,bind([[_423376], [2461 ^ []]]))).
% 0.84/1.39 ncf('1.1.3.1.1',plain,[v2_setfam_1(2461 ^ [])],extension(2463 ^ 10)).
% 0.84/1.39 ncf('1.1.3.2',plain,[-(k6_waybel34(2461 ^ []) = k6_waybel34(2461 ^ []))],extension(2 ^ 9,bind([[_371533], [k6_waybel34(2461 ^ [])]]))).
% 0.84/1.39 ncf('1.1.3.3',plain,[-(k4_waybel34(2461 ^ []) = k4_waybel34(2461 ^ []))],extension(2 ^ 9,bind([[_371533], [k4_waybel34(2461 ^ [])]]))).
% 0.84/1.39 ncf('1.1.3.4',plain,[-(k5_waybel34(2461 ^ []) = k5_waybel34(2461 ^ []))],extension(2 ^ 9,bind([[_371533], [k5_waybel34(2461 ^ [])]]))).
% 0.84/1.39 ncf('1.1.4',plain,[v3_struct_0(k5_waybel34(2461 ^ [])), -(v1_xboole_0(2461 ^ []))],extension(1605 ^ 4,bind([[_422737], [2461 ^ []]]))).
% 0.84/1.39 ncf('1.1.4.1',plain,[v1_xboole_0(2461 ^ []), -(v2_setfam_1(2461 ^ []))],extension(1234 ^ 5,bind([[_411894], [2461 ^ []]]))).
% 0.84/1.39 ncf('1.1.4.1.1',plain,[v2_setfam_1(2461 ^ [])],extension(2463 ^ 6)).
% 0.84/1.39 ncf('1.1.5',plain,[-(v2_altcat_1(k5_waybel34(2461 ^ []))), -(v1_xboole_0(2461 ^ []))],extension(1605 ^ 4,bind([[_422737], [2461 ^ []]]))).
% 0.84/1.39 ncf('1.1.5.1',plain,[v1_xboole_0(2461 ^ []), -(v2_setfam_1(2461 ^ []))],extension(1234 ^ 5,bind([[_411894], [2461 ^ []]]))).
% 0.84/1.39 ncf('1.1.5.1.1',plain,[v2_setfam_1(2461 ^ [])],extension(2463 ^ 6)).
% 0.84/1.39 ncf('1.1.6',plain,[-(v12_altcat_1(k5_waybel34(2461 ^ []))), -(v1_xboole_0(2461 ^ []))],extension(1605 ^ 4,bind([[_422737], [2461 ^ []]]))).
% 0.84/1.39 ncf('1.1.6.1',plain,[v1_xboole_0(2461 ^ []), -(v2_setfam_1(2461 ^ []))],extension(1234 ^ 5,bind([[_411894], [2461 ^ []]]))).
% 0.84/1.39 ncf('1.1.6.1.1',plain,[v2_setfam_1(2461 ^ [])],extension(2463 ^ 6)).
% 0.84/1.39 ncf('1.1.7',plain,[-(l2_altcat_1(k5_waybel34(2461 ^ []))), -(v1_xboole_0(2461 ^ []))],extension(1605 ^ 4,bind([[_422737], [2461 ^ []]]))).
% 0.84/1.39 ncf('1.1.7.1',plain,[v1_xboole_0(2461 ^ []), -(v2_setfam_1(2461 ^ []))],extension(1234 ^ 5,bind([[_411894], [2461 ^ []]]))).
% 0.84/1.39 ncf('1.1.7.1.1',plain,[v2_setfam_1(2461 ^ [])],extension(2463 ^ 6)).
% 0.84/1.39 ncf('1.1.8',plain,[v3_struct_0(k4_waybel34(2461 ^ [])), -(v1_xboole_0(2461 ^ []))],extension(1587 ^ 2,bind([[_422098], [2461 ^ []]]))).
% 0.84/1.39 ncf('1.1.8.1',plain,[v1_xboole_0(2461 ^ []), -(v2_setfam_1(2461 ^ []))],extension(1234 ^ 3,bind([[_411894], [2461 ^ []]]))).
% 0.84/1.39 ncf('1.1.8.1.1',plain,[v2_setfam_1(2461 ^ [])],extension(2463 ^ 4)).
% 0.84/1.39 ncf('1.1.9',plain,[-(v2_altcat_1(k4_waybel34(2461 ^ []))), -(v1_xboole_0(2461 ^ []))],extension(1587 ^ 2,bind([[_422098], [2461 ^ []]]))).
% 0.84/1.39 ncf('1.1.9.1',plain,[v1_xboole_0(2461 ^ []), -(v2_setfam_1(2461 ^ []))],extension(1234 ^ 3,bind([[_411894], [2461 ^ []]]))).
% 0.84/1.39 ncf('1.1.9.1.1',plain,[v2_setfam_1(2461 ^ [])],extension(2463 ^ 4)).
% 0.84/1.39 ncf('1.1.10',plain,[-(v12_altcat_1(k4_waybel34(2461 ^ []))), -(v1_xboole_0(2461 ^ []))],extension(1587 ^ 2,bind([[_422098], [2461 ^ []]]))).
% 0.84/1.39 ncf('1.1.10.1',plain,[v1_xboole_0(2461 ^ []), -(v2_setfam_1(2461 ^ []))],extension(1234 ^ 3,bind([[_411894], [2461 ^ []]]))).
% 0.84/1.39 ncf('1.1.10.1.1',plain,[v2_setfam_1(2461 ^ [])],extension(2463 ^ 4)).
% 0.84/1.39 ncf('1.1.11',plain,[-(l2_altcat_1(k4_waybel34(2461 ^ []))), -(v1_xboole_0(2461 ^ []))],extension(1587 ^ 2,bind([[_422098], [2461 ^ []]]))).
% 0.84/1.39 ncf('1.1.11.1',plain,[v1_xboole_0(2461 ^ []), -(v2_setfam_1(2461 ^ []))],extension(1234 ^ 3,bind([[_411894], [2461 ^ []]]))).
% 0.84/1.39 ncf('1.1.11.1.1',plain,[v2_setfam_1(2461 ^ [])],extension(2463 ^ 4)).
% 0.84/1.39 %-----------------------------------------------------
% 0.84/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------