%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : LAT376+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 11:29:02 EDT 2023
% Result : Theorem 16.39s 16.95s
% Output : Proof 16.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : LAT376+1 : TPTP v8.1.2. Released v3.4.0.
% 0.12/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n027.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:05 EDT 2023
% 0.12/0.34 % CPUTime :
% 16.39/16.95
% 16.39/16.95 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 16.39/16.95 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.39/16.95 %-----------------------------------------------------
% 16.39/16.95 ncf(matrix, plain, [(2979 ^ _22183) ^ [] : [v2_setfam_1(2977 ^ [])], (2981 ^ _22183) ^ [] : [r3_yellow20(k5_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k7_waybel34(2977 ^ []), k9_waybel34(2977 ^ []), k8_waybel34(2977 ^ []))], (764 ^ _22183) ^ [_33058, _33060] : [_33060 = _33058, -(u2_altcat_1(_33060) = u2_altcat_1(_33058))], (770 ^ _22183) ^ [_33143, _33145, _33147, _33149, _33151, _33153] : [-(u1_functor0(_33153, _33149, _33145) = u1_functor0(_33151, _33147, _33143)), _33153 = _33151, _33149 = _33147, _33145 = _33143], (784 ^ _22183) ^ [_33364, _33366, _33368, _33370, _33372, _33374] : [-(u2_functor0(_33374, _33370, _33366) = u2_functor0(_33372, _33368, _33364)), _33374 = _33372, _33370 = _33368, _33366 = _33364], (798 ^ _22183) ^ [_33585, _33587, _33589, _33591, _33593, _33595] : [-(k3_zfmisc_1(_33595, _33591, _33587) = k3_zfmisc_1(_33593, _33589, _33585)), _33595 = _33593, _33591 = _33589, _33587 = _33585], (812 ^ _22183) ^ [_33806, _33808, _33810, _33812, _33814, _33816] : [-(k3_altcat_1(_33816, _33812, _33808) = k3_altcat_1(_33814, _33810, _33806)), _33816 = _33814, _33812 = _33810, _33808 = _33806], (826 ^ _22183) ^ [_34027, _34029, _34031, _34033] : [-(k2_altcat_1(_34033, _34029) = k2_altcat_1(_34031, _34027)), _34033 = _34031, _34029 = _34027], (836 ^ _22183) ^ [_34176, _34178, _34180, _34182, _34184, _34186] : [-(g2_altcat_1(_34186, _34182, _34178) = g2_altcat_1(_34184, _34180, _34176)), _34186 = _34184, _34182 = _34180, _34178 = _34176], (850 ^ _22183) ^ [_34397, _34399, _34401, _34403] : [-(k2_zfmisc_1(_34403, _34399) = k2_zfmisc_1(_34401, _34397)), _34403 = _34401, _34399 = _34397], (860 ^ _22183) ^ [_34546, _34548] : [_34548 = _34546, -(u1_altcat_1(_34548) = u1_altcat_1(_34546))], (866 ^ _22183) ^ [_34631, _34633, _34635, _34637, _34639, _34641, _34643, _34645] : [-(g2_functor0(_34645, _34641, _34637, _34633) = g2_functor0(_34643, _34639, _34635, _34631)), _34645 = _34643, _34641 = _34639, _34637 = _34635, _34633 = _34631], (884 ^ _22183) ^ [_34932, _34934] : [_34934 = _34932, -(u1_struct_0(_34934) = u1_struct_0(_34932))], (890 ^ _22183) ^ [_35017, _35019, _35021, _35023, _35025, _35027] : [-(k15_functor0(_35027, _35023, _35019) = k15_functor0(_35025, _35021, _35017)), _35027 = _35025, _35023 = _35021, _35019 = _35017], (904 ^ _22183) ^ [_35238, _35240] : [_35240 = _35238, -(k6_waybel34(_35240) = k6_waybel34(_35238))], (910 ^ _22183) ^ [_35323, _35325] : [_35325 = _35323, -(k1_zfmisc_1(_35325) = k1_zfmisc_1(_35323))], (916 ^ _22183) ^ [_35408, _35410] : [_35410 = _35408, -(k5_waybel34(_35410) = k5_waybel34(_35408))], (922 ^ _22183) ^ [_35493, _35495] : [_35495 = _35493, -(k4_waybel34(_35495) = k4_waybel34(_35493))], (928 ^ _22183) ^ [_35578, _35580] : [_35580 = _35578, -(k7_waybel34(_35580) = k7_waybel34(_35578))], (934 ^ _22183) ^ [_35663, _35665] : [_35665 = _35663, -(k9_waybel34(_35665) = k9_waybel34(_35663))], (940 ^ _22183) ^ [_35744, _35746] : [_35746 = _35744, -(k8_waybel34(_35746) = k8_waybel34(_35744))], (2 ^ _22183) ^ [_22213] : [-(_22213 = _22213)], (4 ^ _22183) ^ [_22236, _22238] : [_22238 = _22236, -(_22236 = _22238)], (10 ^ _22183) ^ [_22309, _22311, _22313] : [-(_22313 = _22309), _22313 = _22311, _22311 = _22309], (20 ^ _22183) ^ [_22446, _22448] : [-(v1_xcmplx_0(_22446)), _22448 = _22446, v1_xcmplx_0(_22448)], (30 ^ _22183) ^ [_22571, _22573] : [-(v4_ordinal2(_22571)), _22573 = _22571, v4_ordinal2(_22573)], (40 ^ _22183) ^ [_22696, _22698] : [-(v1_xreal_0(_22696)), _22698 = _22696, v1_xreal_0(_22698)], (50 ^ _22183) ^ [_22821, _22823] : [-(v1_int_1(_22821)), _22823 = _22821, v1_int_1(_22823)], (60 ^ _22183) ^ [_22946, _22948] : [-(v1_rat_1(_22946)), _22948 = _22946, v1_rat_1(_22948)], (70 ^ _22183) ^ [_23071, _23073, _23075, _23077, _23079, _23081] : [-(l1_functor0(_23079, _23075, _23071)), l1_functor0(_23081, _23077, _23073), _23081 = _23079, _23077 = _23075, _23073 = _23071], (88 ^ _22183) ^ [_23340, _23342] : [-(v1_funcop_1(_23340)), _23342 = _23340, v1_funcop_1(_23342)], (98 ^ _22183) ^ [_23465, _23467, _23469, _23471, _23473, _23475] : [-(v14_functor0(_23473, _23469, _23465)), v14_functor0(_23475, _23471, _23467), _23475 = _23473, _23471 = _23469, _23467 = _23465], (116 ^ _22183) ^ [_23734, _23736, _23738, _23740] : [-(m1_pboole(_23738, _23734)), m1_pboole(_23740, _23736), _23740 = _23738, _23736 = _23734], (130 ^ _22183) ^ [_23927, _23929, _23931, _23933, _23935, _23937, _23939, _23941] : [-(m3_pboole(_23939, _23935, _23931, _23927)), m3_pboole(_23941, _23937, _23933, _23929), _23941 = _23939, _23937 = _23935, _23933 = _23931, _23929 = _23927], (152 ^ _22183) ^ [_24280, _24282, _24284, _24286, _24288, _24290] : [-(v1_funct_2(_24288, _24284, _24280)), v1_funct_2(_24290, _24286, _24282), _24290 = _24288, _24286 = _24284, _24282 = _24280], (170 ^ _22183) ^ [_24549, _24551, _24553, _24555, _24557, _24559, _24561, _24563, _24565, _24567, _24569, _24571] : [-(m1_functor0(_24569, _24565, _24561, _24557, _24553, _24549)), m1_functor0(_24571, _24567, _24563, _24559, _24555, _24551), _24571 = _24569, _24567 = _24565, _24563 = _24561, _24559 = _24557, _24555 = _24553, _24551 = _24549], (200 ^ _22183) ^ [_25094, _25096] : [-(v1_membered(_25094)), _25096 = _25094, v1_membered(_25096)], (210 ^ _22183) ^ [_25219, _25221] : [-(v2_membered(_25219)), _25221 = _25219, v2_membered(_25221)], (220 ^ _22183) ^ [_25344, _25346] : [-(v3_membered(_25344)), _25346 = _25344, v3_membered(_25346)], (230 ^ _22183) ^ [_25469, _25471] : [-(v4_membered(_25469)), _25471 = _25469, v4_membered(_25471)], (240 ^ _22183) ^ [_25594, _25596] : [-(v5_membered(_25594)), _25596 = _25594, v5_membered(_25596)], (250 ^ _22183) ^ [_25719, _25721] : [-(v6_altcat_1(_25719)), _25721 = _25719, v6_altcat_1(_25721)], (260 ^ _22183) ^ [_25844, _25846] : [-(v9_altcat_1(_25844)), _25846 = _25844, v9_altcat_1(_25846)], (270 ^ _22183) ^ [_25969, _25971] : [-(v2_yellow18(_25969)), _25971 = _25969, v2_yellow18(_25971)], (280 ^ _22183) ^ [_26094, _26096] : [-(v3_yellow18(_26094)), _26096 = _26094, v3_yellow18(_26096)], (290 ^ _22183) ^ [_26219, _26221] : [-(v4_yellow18(_26219)), _26221 = _26219, v4_yellow18(_26221)], (300 ^ _22183) ^ [_26344, _26346] : [-(v1_yellow21(_26344)), _26346 = _26344, v1_yellow21(_26346)], (310 ^ _22183) ^ [_26469, _26471] : [-(v2_yellow21(_26469)), _26471 = _26469, v2_yellow21(_26471)], (320 ^ _22183) ^ [_26594, _26596] : [-(v3_yellow21(_26594)), _26596 = _26594, v3_yellow21(_26596)], (330 ^ _22183) ^ [_26719, _26721] : [-(v1_relat_1(_26719)), _26721 = _26719, v1_relat_1(_26721)], (340 ^ _22183) ^ [_26844, _26846] : [-(v1_funct_1(_26844)), _26846 = _26844, v1_funct_1(_26846)], (350 ^ _22183) ^ [_26969, _26971] : [-(v2_funct_1(_26969)), _26971 = _26969, v2_funct_1(_26971)], (360 ^ _22183) ^ [_27094, _27096] : [-(v1_finset_1(_27094)), _27096 = _27094, v1_finset_1(_27096)], (370 ^ _22183) ^ [_27219, _27221, _27223, _27225, _27227, _27229] : [-(v11_functor0(_27227, _27223, _27219)), v11_functor0(_27229, _27225, _27221), _27229 = _27227, _27225 = _27223, _27221 = _27219], (388 ^ _22183) ^ [_27488, _27490] : [-(l1_struct_0(_27488)), _27490 = _27488, l1_struct_0(_27490)], (398 ^ _22183) ^ [_27613, _27615] : [-(v1_altcat_2(_27613)), _27615 = _27613, v1_altcat_2(_27615)], (408 ^ _22183) ^ [_27738, _27740] : [-(l1_altcat_1(_27738)), _27740 = _27738, l1_altcat_1(_27740)], (418 ^ _22183) ^ [_27863, _27865, _27867, _27869, _27871, _27873] : [-(l2_functor0(_27871, _27867, _27863)), l2_functor0(_27873, _27869, _27865), _27873 = _27871, _27869 = _27867, _27865 = _27863], (436 ^ _22183) ^ [_28132, _28134, _28136, _28138, _28140, _28142] : [-(v6_functor0(_28140, _28136, _28132)), v6_functor0(_28142, _28138, _28134), _28142 = _28140, _28138 = _28136, _28134 = _28132], (454 ^ _22183) ^ [_28401, _28403, _28405, _28407, _28409, _28411] : [-(v8_functor0(_28409, _28405, _28401)), v8_functor0(_28411, _28407, _28403), _28411 = _28409, _28407 = _28405, _28403 = _28401], (472 ^ _22183) ^ [_28670, _28672, _28674, _28676, _28678, _28680] : [-(v9_functor0(_28678, _28674, _28670)), v9_functor0(_28680, _28676, _28672), _28680 = _28678, _28676 = _28674, _28672 = _28670], (490 ^ _22183) ^ [_28939, _28941, _28943, _28945, _28947, _28949] : [-(v12_functor0(_28947, _28943, _28939)), v12_functor0(_28949, _28945, _28941), _28949 = _28947, _28945 = _28943, _28941 = _28939], (508 ^ _22183) ^ [_29208, _29210, _29212, _29214, _29216, _29218] : [-(m2_relset_1(_29216, _29212, _29208)), m2_relset_1(_29218, _29214, _29210), _29218 = _29216, _29214 = _29212, _29210 = _29208], (526 ^ _22183) ^ [_29477, _29479, _29481, _29483, _29485, _29487] : [-(m1_relset_1(_29485, _29481, _29477)), m1_relset_1(_29487, _29483, _29479), _29487 = _29485, _29483 = _29481, _29479 = _29477], (544 ^ _22183) ^ [_29746, _29748, _29750, _29752] : [-(r1_tarski(_29750, _29746)), r1_tarski(_29752, _29748), _29752 = _29750, _29748 = _29746], (558 ^ _22183) ^ [_29939, _29941] : [-(v11_altcat_1(_29939)), _29941 = _29939, v11_altcat_1(_29941)], (568 ^ _22183) ^ [_30064, _30066] : [-(v12_altcat_1(_30064)), _30066 = _30064, v12_altcat_1(_30066)], (578 ^ _22183) ^ [_30189, _30191] : [-(l2_altcat_1(_30189)), _30191 = _30189, l2_altcat_1(_30191)], (588 ^ _22183) ^ [_30314, _30316, _30318, _30320, _30322, _30324] : [-(v16_functor0(_30322, _30318, _30314)), v16_functor0(_30324, _30320, _30316), _30324 = _30322, _30320 = _30318, _30316 = _30314], (606 ^ _22183) ^ [_30583, _30585, _30587, _30589, _30591, _30593] : [-(m2_functor0(_30591, _30587, _30583)), m2_functor0(_30593, _30589, _30585), _30593 = _30591, _30589 = _30587, _30585 = _30583], (624 ^ _22183) ^ [_30852, _30854, _30856, _30858, _30860, _30862] : [-(v21_functor0(_30860, _30856, _30852)), v21_functor0(_30862, _30858, _30854), _30862 = _30860, _30858 = _30856, _30854 = _30852], (642 ^ _22183) ^ [_31121, _31123] : [-(v3_struct_0(_31121)), _31123 = _31121, v3_struct_0(_31123)], (652 ^ _22183) ^ [_31246, _31248] : [-(v2_altcat_1(_31246)), _31248 = _31246, v2_altcat_1(_31248)], (662 ^ _22183) ^ [_31371, _31373, _31375, _31377] : [-(v3_altcat_2(_31375, _31371)), v3_altcat_2(_31377, _31373), _31377 = _31375, _31373 = _31371], (676 ^ _22183) ^ [_31564, _31566, _31568, _31570] : [-(m1_altcat_2(_31568, _31564)), m1_altcat_2(_31570, _31566), _31570 = _31568, _31566 = _31564], (690 ^ _22183) ^ [_31757, _31759, _31761, _31763] : [-(m1_subset_1(_31761, _31757)), m1_subset_1(_31763, _31759), _31763 = _31761, _31759 = _31757], (704 ^ _22183) ^ [_31950, _31952, _31954, _31956] : [-(r2_hidden(_31954, _31950)), r2_hidden(_31956, _31952), _31956 = _31954, _31952 = _31950], (718 ^ _22183) ^ [_32143, _32145] : [-(v1_xboole_0(_32143)), _32145 = _32143, v1_xboole_0(_32145)], (728 ^ _22183) ^ [_32268, _32270] : [-(v2_setfam_1(_32268)), _32270 = _32268, v2_setfam_1(_32270)], (738 ^ _22183) ^ [_32389, _32391, _32393, _32395, _32397, _32399, _32401, _32403, _32405, _32407] : [-(r3_yellow20(_32405, _32401, _32397, _32393, _32389)), r3_yellow20(_32407, _32403, _32399, _32395, _32391), _32407 = _32405, _32403 = _32401, _32399 = _32397, _32395 = _32393, _32391 = _32389], (946 ^ _22183) ^ [_35871] : [l2_altcat_1(_35871), v6_altcat_1(_35871), -(_35871 = g2_altcat_1(u1_struct_0(_35871), u1_altcat_1(_35871), u2_altcat_1(_35871)))], (956 ^ _22183) ^ [_36012, _36014, _36016] : [v9_functor0(_36012, _36016, _36014), -(_36012 = g2_functor0(_36016, _36014, u1_functor0(_36016, _36014, _36012), u2_functor0(_36016, _36014, _36012))), l1_altcat_1(_36016), l1_altcat_1(_36014), l2_functor0(_36012, _36016, _36014)], (974 ^ _22183) ^ [_36281, _36283] : [r2_hidden(_36283, _36281), r2_hidden(_36281, _36283)], (980 ^ _22183) ^ [_36359] : [v1_membered(_36359), 983 ^ _22183 : [(984 ^ _22183) ^ [_36417] : [m1_subset_1(_36417, _36359), -(v1_xcmplx_0(_36417))]]], (990 ^ _22183) ^ [_36496] : [v2_membered(_36496), 993 ^ _22183 : [(994 ^ _22183) ^ [_36559] : [m1_subset_1(_36559, _36496), 997 ^ _22183 : [(998 ^ _22183) ^ [] : [-(v1_xcmplx_0(_36559))], (1000 ^ _22183) ^ [] : [-(v1_xreal_0(_36559))]]]]], (1002 ^ _22183) ^ [_36662] : [1025 ^ _22183 : [(1026 ^ _22183) ^ [_37044] : [m1_altcat_2(_37044, _36662), 1041 ^ _22183 : [(1042 ^ _22183) ^ [] : [v3_struct_0(_37044)], (1044 ^ _22183) ^ [] : [-(v2_altcat_1(_37044))], (1046 ^ _22183) ^ [] : [-(v9_altcat_1(_37044))], (1048 ^ _22183) ^ [] : [-(v11_altcat_1(_37044))], (1050 ^ _22183) ^ [] : [-(v12_altcat_1(_37044))], (1052 ^ _22183) ^ [] : [-(v1_altcat_2(_37044))], (1054 ^ _22183) ^ [] : [-(v3_altcat_2(_37044, _36662))], (1056 ^ _22183) ^ [] : [-(v2_yellow18(_37044))], (1058 ^ _22183) ^ [] : [-(v3_yellow18(_37044))], (1060 ^ _22183) ^ [] : [-(v4_yellow18(_37044))], (1062 ^ _22183) ^ [] : [-(v1_yellow21(_37044))], (1064 ^ _22183) ^ [] : [-(v2_yellow21(_37044))], (1066 ^ _22183) ^ [] : [-(v3_yellow21(_37044))]], -(v3_struct_0(_37044)), v2_altcat_1(_37044), v3_altcat_2(_37044, _36662)]], -(v3_struct_0(_36662)), v2_altcat_1(_36662), v11_altcat_1(_36662), v12_altcat_1(_36662), v3_yellow21(_36662), l2_altcat_1(_36662)], (1068 ^ _22183) ^ [_37556] : [v3_membered(_37556), 1071 ^ _22183 : [(1072 ^ _22183) ^ [_37624] : [m1_subset_1(_37624, _37556), 1075 ^ _22183 : [(1076 ^ _22183) ^ [] : [-(v1_xcmplx_0(_37624))], (1078 ^ _22183) ^ [] : [-(v1_xreal_0(_37624))], (1080 ^ _22183) ^ [] : [-(v1_rat_1(_37624))]]]]], (1082 ^ _22183) ^ [_37749] : [v4_membered(_37749), 1085 ^ _22183 : [(1086 ^ _22183) ^ [_37822] : [m1_subset_1(_37822, _37749), 1089 ^ _22183 : [(1090 ^ _22183) ^ [] : [-(v1_xcmplx_0(_37822))], (1092 ^ _22183) ^ [] : [-(v1_xreal_0(_37822))], (1094 ^ _22183) ^ [] : [-(v1_int_1(_37822))], (1096 ^ _22183) ^ [] : [-(v1_rat_1(_37822))]]]]], (1098 ^ _22183) ^ [_37969] : [v5_membered(_37969), 1101 ^ _22183 : [(1102 ^ _22183) ^ [_38047] : [m1_subset_1(_38047, _37969), 1105 ^ _22183 : [(1106 ^ _22183) ^ [] : [-(v1_xcmplx_0(_38047))], (1108 ^ _22183) ^ [] : [-(v4_ordinal2(_38047))], (1110 ^ _22183) ^ [] : [-(v1_xreal_0(_38047))], (1112 ^ _22183) ^ [] : [-(v1_int_1(_38047))], (1114 ^ _22183) ^ [] : [-(v1_rat_1(_38047))]]]]], (1116 ^ _22183) ^ [_38216] : [v1_xboole_0(_38216), 1119 ^ _22183 : [(1120 ^ _22183) ^ [] : [-(v1_membered(_38216))], (1122 ^ _22183) ^ [] : [-(v2_membered(_38216))], (1124 ^ _22183) ^ [] : [-(v3_membered(_38216))], (1126 ^ _22183) ^ [] : [-(v4_membered(_38216))], (1128 ^ _22183) ^ [] : [-(v5_membered(_38216))]]], (1130 ^ _22183) ^ [_38377] : [v1_membered(_38377), 1133 ^ _22183 : [(1134 ^ _22183) ^ [_38437] : [m1_subset_1(_38437, k1_zfmisc_1(_38377)), -(v1_membered(_38437))]]], (1140 ^ _22183) ^ [_38520] : [v2_membered(_38520), 1143 ^ _22183 : [(1144 ^ _22183) ^ [_38585] : [m1_subset_1(_38585, k1_zfmisc_1(_38520)), 1147 ^ _22183 : [(1148 ^ _22183) ^ [] : [-(v1_membered(_38585))], (1150 ^ _22183) ^ [] : [-(v2_membered(_38585))]]]]], (1152 ^ _22183) ^ [_38692] : [v3_membered(_38692), 1155 ^ _22183 : [(1156 ^ _22183) ^ [_38762] : [m1_subset_1(_38762, k1_zfmisc_1(_38692)), 1159 ^ _22183 : [(1160 ^ _22183) ^ [] : [-(v1_membered(_38762))], (1162 ^ _22183) ^ [] : [-(v2_membered(_38762))], (1164 ^ _22183) ^ [] : [-(v3_membered(_38762))]]]]], (1166 ^ _22183) ^ [_38891] : [v4_membered(_38891), 1169 ^ _22183 : [(1170 ^ _22183) ^ [_38966] : [m1_subset_1(_38966, k1_zfmisc_1(_38891)), 1173 ^ _22183 : [(1174 ^ _22183) ^ [] : [-(v1_membered(_38966))], (1176 ^ _22183) ^ [] : [-(v2_membered(_38966))], (1178 ^ _22183) ^ [] : [-(v3_membered(_38966))], (1180 ^ _22183) ^ [] : [-(v4_membered(_38966))]]]]], (1182 ^ _22183) ^ [_39117] : [v1_xboole_0(_39117), -(v1_finset_1(_39117))], (1188 ^ _22183) ^ [_39188] : [v1_xboole_0(_39188), -(v1_funct_1(_39188))], (1194 ^ _22183) ^ [_39259, _39261, _39263, _39265, _39267] : [1213 ^ _22183 : [(1214 ^ _22183) ^ [_39565] : [m1_functor0(_39565, _39267, _39265, _39263, _39261, _39259), -(v1_funcop_1(_39565))]], v1_funct_1(_39263), v1_funct_2(_39263, _39267, _39265), m1_relset_1(_39263, _39267, _39265), m1_pboole(_39261, _39267), m1_pboole(_39259, _39265)], (1220 ^ _22183) ^ [_39660, _39662] : [1247 ^ _22183 : [(1248 ^ _22183) ^ [_40036] : [m2_functor0(_40036, _39662, _39660), 1251 ^ _22183 : [(1252 ^ _22183) ^ [] : [-(v8_functor0(_40036, _39662, _39660))], (1254 ^ _22183) ^ [] : [-(v12_functor0(_40036, _39662, _39660))]]]], -(v3_struct_0(_39662)), v2_altcat_1(_39662), v12_altcat_1(_39662), l2_altcat_1(_39662), -(v3_struct_0(_39660)), v12_altcat_1(_39660), l2_altcat_1(_39660)], (1256 ^ _22183) ^ [_40151] : [v5_membered(_40151), -(v4_membered(_40151))], (1262 ^ _22183) ^ [_40222, _40224, _40226] : [m1_subset_1(_40222, k1_zfmisc_1(k2_zfmisc_1(_40226, _40224))), -(v1_relat_1(_40222))], (1268 ^ _22183) ^ [_40309] : [l2_altcat_1(_40309), 1291 ^ _22183 : [(1292 ^ _22183) ^ [] : [v3_struct_0(_40309)], (1294 ^ _22183) ^ [] : [-(v2_altcat_1(_40309))], (1296 ^ _22183) ^ [] : [-(v11_altcat_1(_40309))], (1298 ^ _22183) ^ [] : [-(v12_altcat_1(_40309))], (1300 ^ _22183) ^ [] : [-(v1_altcat_2(_40309))], (1302 ^ _22183) ^ [] : [-(v2_yellow21(_40309))]], -(v3_struct_0(_40309)), v2_altcat_1(_40309), v11_altcat_1(_40309), v12_altcat_1(_40309), v3_yellow21(_40309)], (1304 ^ _22183) ^ [_40745] : [v5_membered(_40745), 1307 ^ _22183 : [(1308 ^ _22183) ^ [_40825] : [m1_subset_1(_40825, k1_zfmisc_1(_40745)), 1311 ^ _22183 : [(1312 ^ _22183) ^ [] : [-(v1_membered(_40825))], (1314 ^ _22183) ^ [] : [-(v2_membered(_40825))], (1316 ^ _22183) ^ [] : [-(v3_membered(_40825))], (1318 ^ _22183) ^ [] : [-(v4_membered(_40825))], (1320 ^ _22183) ^ [] : [-(v5_membered(_40825))]]]]], (1322 ^ _22183) ^ [_40998] : [v1_finset_1(_40998), 1325 ^ _22183 : [(1326 ^ _22183) ^ [_41058] : [m1_subset_1(_41058, k1_zfmisc_1(_40998)), -(v1_finset_1(_41058))]]], (1332 ^ _22183) ^ [_41141] : [1343 ^ _22183 : [(1344 ^ _22183) ^ [] : [-(v1_relat_1(_41141))], (1346 ^ _22183) ^ [] : [-(v1_funct_1(_41141))], (1348 ^ _22183) ^ [] : [-(v2_funct_1(_41141))]], v1_relat_1(_41141), v1_xboole_0(_41141), v1_funct_1(_41141)], (1350 ^ _22183) ^ [_41354] : [l2_altcat_1(_41354), 1361 ^ _22183 : [(1362 ^ _22183) ^ [] : [v3_struct_0(_41354)], (1364 ^ _22183) ^ [] : [-(v1_altcat_2(_41354))]], -(v3_struct_0(_41354)), v12_altcat_1(_41354)], (1366 ^ _22183) ^ [_41558] : [v4_membered(_41558), -(v3_membered(_41558))], (1372 ^ _22183) ^ [_41628] : [-(v2_setfam_1(_41628)), v1_xboole_0(_41628)], (1378 ^ _22183) ^ [_41699] : [l2_altcat_1(_41699), 1401 ^ _22183 : [(1402 ^ _22183) ^ [] : [v3_struct_0(_41699)], (1404 ^ _22183) ^ [] : [-(v2_altcat_1(_41699))], (1406 ^ _22183) ^ [] : [-(v9_altcat_1(_41699))], (1408 ^ _22183) ^ [] : [-(v11_altcat_1(_41699))], (1410 ^ _22183) ^ [] : [-(v12_altcat_1(_41699))], (1412 ^ _22183) ^ [] : [-(v1_altcat_2(_41699))], (1414 ^ _22183) ^ [] : [-(v2_yellow18(_41699))], (1416 ^ _22183) ^ [] : [-(v3_yellow18(_41699))], (1418 ^ _22183) ^ [] : [-(v4_yellow18(_41699))], (1420 ^ _22183) ^ [] : [-(v1_yellow21(_41699))]], -(v3_struct_0(_41699)), v2_altcat_1(_41699), v11_altcat_1(_41699), v12_altcat_1(_41699), v2_yellow21(_41699)], (1422 ^ _22183) ^ [_42223] : [v3_membered(_42223), -(v2_membered(_42223))], (1428 ^ _22183) ^ [_42294, _42296] : [l1_struct_0(_42296), -(v3_struct_0(_42294)), l1_struct_0(_42294), 1439 ^ _22183 : [(1440 ^ _22183) ^ [_42467] : [l1_functor0(_42467, _42296, _42294), v11_functor0(_42467, _42296, _42294), -(v6_functor0(_42467, _42296, _42294))]]], (1450 ^ _22183) ^ [_42614, _42616] : [1477 ^ _22183 : [(1478 ^ _22183) ^ [_43018] : [m2_functor0(_43018, _42616, _42614), v16_functor0(_43018, _42616, _42614), 1485 ^ _22183 : [(1486 ^ _22183) ^ [] : [-(v6_functor0(_43018, _42616, _42614))], (1488 ^ _22183) ^ [] : [-(v8_functor0(_43018, _42616, _42614))], (1490 ^ _22183) ^ [] : [-(v11_functor0(_43018, _42616, _42614))], (1492 ^ _22183) ^ [] : [-(v12_functor0(_43018, _42616, _42614))], (1494 ^ _22183) ^ [] : [-(v14_functor0(_43018, _42616, _42614))]]]], -(v3_struct_0(_42616)), v2_altcat_1(_42616), v12_altcat_1(_42616), l2_altcat_1(_42616), -(v3_struct_0(_42614)), v12_altcat_1(_42614), l2_altcat_1(_42614)], (1496 ^ _22183) ^ [_43267] : [v2_membered(_43267), -(v1_membered(_43267))], (1502 ^ _22183) ^ [_43338, _43340] : [1529 ^ _22183 : [(1530 ^ _22183) ^ [_43742] : [m2_functor0(_43742, _43340, _43338), 1541 ^ _22183 : [(1542 ^ _22183) ^ [] : [-(v6_functor0(_43742, _43340, _43338))], (1544 ^ _22183) ^ [] : [-(v8_functor0(_43742, _43340, _43338))], (1546 ^ _22183) ^ [] : [-(v12_functor0(_43742, _43340, _43338))], (1548 ^ _22183) ^ [] : [-(v16_functor0(_43742, _43340, _43338))]], v11_functor0(_43742, _43340, _43338), v14_functor0(_43742, _43340, _43338)]], -(v3_struct_0(_43340)), v2_altcat_1(_43340), v12_altcat_1(_43340), l2_altcat_1(_43340), -(v3_struct_0(_43338)), v12_altcat_1(_43338), l2_altcat_1(_43338)], (1550 ^ _22183) ^ [_44021] : [1573 ^ _22183 : [(1574 ^ _22183) ^ [_44373] : [m1_altcat_2(_44373, _44021), 1589 ^ _22183 : [(1590 ^ _22183) ^ [] : [v3_struct_0(_44373)], (1592 ^ _22183) ^ [] : [-(v2_altcat_1(_44373))], (1594 ^ _22183) ^ [] : [-(v11_altcat_1(_44373))], (1596 ^ _22183) ^ [] : [-(v12_altcat_1(_44373))], (1598 ^ _22183) ^ [] : [-(v1_altcat_2(_44373))], (1600 ^ _22183) ^ [] : [-(v3_altcat_2(_44373, _44021))], (1602 ^ _22183) ^ [] : [-(v3_yellow18(_44373))]], -(v3_struct_0(_44373)), v2_altcat_1(_44373), v3_altcat_2(_44373, _44021)]], -(v3_struct_0(_44021)), v2_altcat_1(_44021), v11_altcat_1(_44021), v12_altcat_1(_44021), v3_yellow18(_44021), l2_altcat_1(_44021)], (1604 ^ _22183) ^ [_44753, _44755] : [1631 ^ _22183 : [(1632 ^ _22183) ^ [_45129] : [m2_functor0(_45129, _44755, _44753), v16_functor0(_45129, _44755, _44753), -(v6_functor0(_45129, _44755, _44753))]], -(v3_struct_0(_44755)), v2_altcat_1(_44755), v12_altcat_1(_44755), l2_altcat_1(_44755), -(v3_struct_0(_44753)), v12_altcat_1(_44753), l2_altcat_1(_44753)], (1642 ^ _22183) ^ [_45272] : [1665 ^ _22183 : [(1666 ^ _22183) ^ [_45624] : [m1_altcat_2(_45624, _45272), 1681 ^ _22183 : [(1682 ^ _22183) ^ [] : [v3_struct_0(_45624)], (1684 ^ _22183) ^ [] : [-(v2_altcat_1(_45624))], (1686 ^ _22183) ^ [] : [-(v11_altcat_1(_45624))], (1688 ^ _22183) ^ [] : [-(v12_altcat_1(_45624))], (1690 ^ _22183) ^ [] : [-(v1_altcat_2(_45624))], (1692 ^ _22183) ^ [] : [-(v3_altcat_2(_45624, _45272))], (1694 ^ _22183) ^ [] : [-(v2_yellow18(_45624))]], -(v3_struct_0(_45624)), v2_altcat_1(_45624), v3_altcat_2(_45624, _45272)]], -(v3_struct_0(_45272)), v2_altcat_1(_45272), v11_altcat_1(_45272), v12_altcat_1(_45272), v2_yellow18(_45272), l2_altcat_1(_45272)], (1696 ^ _22183) ^ [_46004] : [1719 ^ _22183 : [(1720 ^ _22183) ^ [_46334] : [m1_altcat_2(_46334, _46004), 1731 ^ _22183 : [(1732 ^ _22183) ^ [] : [v3_struct_0(_46334)], (1734 ^ _22183) ^ [] : [-(v2_altcat_1(_46334))], (1736 ^ _22183) ^ [] : [-(v9_altcat_1(_46334))], (1738 ^ _22183) ^ [] : [-(v11_altcat_1(_46334))]], -(v3_struct_0(_46334)), v2_altcat_1(_46334)]], -(v3_struct_0(_46004)), v2_altcat_1(_46004), v9_altcat_1(_46004), v11_altcat_1(_46004), v12_altcat_1(_46004), l2_altcat_1(_46004)], (1740 ^ _22183) ^ [_46594] : [1763 ^ _22183 : [(1764 ^ _22183) ^ [_46946] : [m1_altcat_2(_46946, _46594), 1779 ^ _22183 : [(1780 ^ _22183) ^ [] : [v3_struct_0(_46946)], (1782 ^ _22183) ^ [] : [-(v2_altcat_1(_46946))], (1784 ^ _22183) ^ [] : [-(v11_altcat_1(_46946))], (1786 ^ _22183) ^ [] : [-(v12_altcat_1(_46946))], (1788 ^ _22183) ^ [] : [-(v1_altcat_2(_46946))], (1790 ^ _22183) ^ [] : [-(v3_altcat_2(_46946, _46594))], (1792 ^ _22183) ^ [] : [-(v1_yellow21(_46946))]], -(v3_struct_0(_46946)), v2_altcat_1(_46946), v3_altcat_2(_46946, _46594)]], -(v3_struct_0(_46594)), v2_altcat_1(_46594), v11_altcat_1(_46594), v12_altcat_1(_46594), v1_yellow21(_46594), l2_altcat_1(_46594)], (1794 ^ _22183) ^ [_47326] : [1817 ^ _22183 : [(1818 ^ _22183) ^ [_47703] : [m1_altcat_2(_47703, _47326), 1833 ^ _22183 : [(1834 ^ _22183) ^ [] : [v3_struct_0(_47703)], (1836 ^ _22183) ^ [] : [-(v2_altcat_1(_47703))], (1838 ^ _22183) ^ [] : [-(v9_altcat_1(_47703))], (1840 ^ _22183) ^ [] : [-(v11_altcat_1(_47703))], (1842 ^ _22183) ^ [] : [-(v12_altcat_1(_47703))], (1844 ^ _22183) ^ [] : [-(v1_altcat_2(_47703))], (1846 ^ _22183) ^ [] : [-(v3_altcat_2(_47703, _47326))], (1848 ^ _22183) ^ [] : [-(v2_yellow18(_47703))], (1850 ^ _22183) ^ [] : [-(v3_yellow18(_47703))], (1852 ^ _22183) ^ [] : [-(v4_yellow18(_47703))], (1854 ^ _22183) ^ [] : [-(v1_yellow21(_47703))], (1856 ^ _22183) ^ [] : [-(v2_yellow21(_47703))]], -(v3_struct_0(_47703)), v2_altcat_1(_47703), v3_altcat_2(_47703, _47326)]], -(v3_struct_0(_47326)), v2_altcat_1(_47326), v11_altcat_1(_47326), v12_altcat_1(_47326), v2_yellow21(_47326), l2_altcat_1(_47326)], (1858 ^ _22183) ^ [_48193, _48195, _48197] : [1865 ^ _22183 : [(1866 ^ _22183) ^ [] : [-(v6_altcat_1(g2_altcat_1(_48197, _48195, _48193)))], (1868 ^ _22183) ^ [] : [-(l2_altcat_1(g2_altcat_1(_48197, _48195, _48193)))]], m1_pboole(_48195, k2_zfmisc_1(_48197, _48197)), m3_pboole(_48193, k3_zfmisc_1(_48197, _48197, _48197), k3_altcat_1(_48197, _48195, _48195), k2_altcat_1(_48197, _48195))], (1870 ^ _22183) ^ [_48396, _48398, _48400, _48402] : [1893 ^ _22183 : [(1894 ^ _22183) ^ [] : [-(v9_functor0(g2_functor0(_48402, _48400, _48398, _48396), _48402, _48400))], (1896 ^ _22183) ^ [] : [-(l2_functor0(g2_functor0(_48402, _48400, _48398, _48396), _48402, _48400))]], l1_altcat_1(_48402), l1_altcat_1(_48400), v1_funct_1(_48398), v1_funct_2(_48398, k2_zfmisc_1(u1_struct_0(_48402), u1_struct_0(_48402)), k2_zfmisc_1(u1_struct_0(_48400), u1_struct_0(_48400))), m1_relset_1(_48398, k2_zfmisc_1(u1_struct_0(_48402), u1_struct_0(_48402)), k2_zfmisc_1(u1_struct_0(_48400), u1_struct_0(_48400))), m1_functor0(_48396, k2_zfmisc_1(u1_struct_0(_48402), u1_struct_0(_48402)), k2_zfmisc_1(u1_struct_0(_48400), u1_struct_0(_48400)), _48398, u1_altcat_1(_48402), u1_altcat_1(_48400))], (1898 ^ _22183) ^ [_48905, _48907, _48909] : [1917 ^ _22183 : [(1918 ^ _22183) ^ [] : [-(v9_functor0(k15_functor0(_48909, _48907, _48905), _48907, _48909))], (1920 ^ _22183) ^ [] : [-(l2_functor0(k15_functor0(_48909, _48907, _48905), _48907, _48909))]], -(v3_struct_0(_48909)), l1_altcat_1(_48909), -(v3_struct_0(_48907)), l1_altcat_1(_48907), l2_functor0(_48905, _48909, _48907)], (1922 ^ _22183) ^ [] : [true___, -(true___)], (1928 ^ _22183) ^ [] : [true___, -(true___)], (1934 ^ _22183) ^ [_49364, _49366] : [m1_pboole(_49364, k2_zfmisc_1(_49366, _49366)), -(m1_pboole(k2_altcat_1(_49366, _49364), k3_zfmisc_1(_49366, _49366, _49366)))], (1940 ^ _22183) ^ [] : [true___, -(true___)], (1946 ^ _22183) ^ [_49520, _49522, _49524] : [-(m1_pboole(k3_altcat_1(_49524, _49522, _49520), k3_zfmisc_1(_49524, _49524, _49524))), m1_pboole(_49522, k2_zfmisc_1(_49524, _49524)), m1_pboole(_49520, k2_zfmisc_1(_49524, _49524))], (1956 ^ _22183) ^ [] : [true___, -(true___)], (1962 ^ _22183) ^ [_49739] : [-(v1_xboole_0(_49739)), 1965 ^ _22183 : [(1966 ^ _22183) ^ [] : [v3_struct_0(k4_waybel34(_49739))], (1968 ^ _22183) ^ [] : [-(v2_altcat_1(k4_waybel34(_49739)))], (1970 ^ _22183) ^ [] : [-(v6_altcat_1(k4_waybel34(_49739)))], (1972 ^ _22183) ^ [] : [-(v11_altcat_1(k4_waybel34(_49739)))], (1974 ^ _22183) ^ [] : [-(v12_altcat_1(k4_waybel34(_49739)))], (1976 ^ _22183) ^ [] : [-(v2_yellow21(k4_waybel34(_49739)))], (1978 ^ _22183) ^ [] : [-(l2_altcat_1(k4_waybel34(_49739)))]]], (1980 ^ _22183) ^ [_49980] : [-(v1_xboole_0(_49980)), 1983 ^ _22183 : [(1984 ^ _22183) ^ [] : [v3_struct_0(k5_waybel34(_49980))], (1986 ^ _22183) ^ [] : [-(v2_altcat_1(k5_waybel34(_49980)))], (1988 ^ _22183) ^ [] : [-(v6_altcat_1(k5_waybel34(_49980)))], (1990 ^ _22183) ^ [] : [-(v11_altcat_1(k5_waybel34(_49980)))], (1992 ^ _22183) ^ [] : [-(v12_altcat_1(k5_waybel34(_49980)))], (1994 ^ _22183) ^ [] : [-(v2_yellow21(k5_waybel34(_49980)))], (1996 ^ _22183) ^ [] : [-(l2_altcat_1(k5_waybel34(_49980)))]]], (1998 ^ _22183) ^ [_50218] : [-(v2_setfam_1(_50218)), 2001 ^ _22183 : [(2002 ^ _22183) ^ [] : [-(v9_functor0(k6_waybel34(_50218), k4_waybel34(_50218), k5_waybel34(_50218)))], (2004 ^ _22183) ^ [] : [-(v16_functor0(k6_waybel34(_50218), k4_waybel34(_50218), k5_waybel34(_50218)))], (2006 ^ _22183) ^ [] : [-(m2_functor0(k6_waybel34(_50218), k4_waybel34(_50218), k5_waybel34(_50218)))]]], (2008 ^ _22183) ^ [_50323] : [-(v2_setfam_1(_50323)), 2011 ^ _22183 : [(2012 ^ _22183) ^ [] : [-(v9_functor0(k7_waybel34(_50323), k5_waybel34(_50323), k4_waybel34(_50323)))], (2014 ^ _22183) ^ [] : [-(v16_functor0(k7_waybel34(_50323), k5_waybel34(_50323), k4_waybel34(_50323)))], (2016 ^ _22183) ^ [] : [-(m2_functor0(k7_waybel34(_50323), k5_waybel34(_50323), k4_waybel34(_50323)))]]], (2018 ^ _22183) ^ [_50431] : [-(v1_xboole_0(_50431)), 2021 ^ _22183 : [(2022 ^ _22183) ^ [] : [v3_struct_0(k8_waybel34(_50431))], (2024 ^ _22183) ^ [] : [-(v2_altcat_1(k8_waybel34(_50431)))], (2026 ^ _22183) ^ [] : [-(v6_altcat_1(k8_waybel34(_50431)))], (2028 ^ _22183) ^ [] : [-(v3_altcat_2(k8_waybel34(_50431), k4_waybel34(_50431)))], (2030 ^ _22183) ^ [] : [-(m1_altcat_2(k8_waybel34(_50431), k4_waybel34(_50431)))]]], (2032 ^ _22183) ^ [_50632] : [-(v2_setfam_1(_50632)), 2035 ^ _22183 : [(2036 ^ _22183) ^ [] : [v3_struct_0(k9_waybel34(_50632))], (2038 ^ _22183) ^ [] : [-(v2_altcat_1(k9_waybel34(_50632)))], (2040 ^ _22183) ^ [] : [-(v6_altcat_1(k9_waybel34(_50632)))], (2042 ^ _22183) ^ [] : [-(v3_altcat_2(k9_waybel34(_50632), k5_waybel34(_50632)))], (2044 ^ _22183) ^ [] : [-(m1_altcat_2(k9_waybel34(_50632), k5_waybel34(_50632)))]]], (2046 ^ _22183) ^ [_51032] : [l1_altcat_1(_51032), -(l1_struct_0(_51032))], (2052 ^ _22183) ^ [] : [true___, -(true___)], (2058 ^ _22183) ^ [] : [true___, -(true___)], (2064 ^ _22183) ^ [_51456] : [l2_altcat_1(_51456), -(l1_altcat_1(_51456))], (2070 ^ _22183) ^ [_51656, _51658] : [l1_altcat_1(_51658), l1_altcat_1(_51656), 2077 ^ _22183 : [(2078 ^ _22183) ^ [_51880] : [l2_functor0(_51880, _51658, _51656), -(l1_functor0(_51880, _51658, _51656))]]], (2084 ^ _22183) ^ [_52097] : [l2_altcat_1(_52097), 2087 ^ _22183 : [(2088 ^ _22183) ^ [_52227] : [m1_altcat_2(_52227, _52097), -(l2_altcat_1(_52227))]]], (2094 ^ _22183) ^ [_52484, _52486, _52488, _52490, _52492] : [2113 ^ _22183 : [(2114 ^ _22183) ^ [_53043] : [m1_functor0(_53043, _52492, _52490, _52488, _52486, _52484), -(m1_pboole(_53043, _52492))]], v1_funct_1(_52488), v1_funct_2(_52488, _52492, _52490), m1_relset_1(_52488, _52492, _52490), m1_pboole(_52486, _52492), m1_pboole(_52484, _52490)], (2120 ^ _22183) ^ [_53300, _53302] : [m1_pboole(_53300, _53302), 2123 ^ _22183 : [(2124 ^ _22183) ^ [] : [-(v1_relat_1(_53300))], (2126 ^ _22183) ^ [] : [-(v1_funct_1(_53300))]]], (2128 ^ _22183) ^ [] : [true___, -(true___)], (2134 ^ _22183) ^ [] : [true___, -(true___)], (2140 ^ _22183) ^ [_53819, _53821] : [2167 ^ _22183 : [(2168 ^ _22183) ^ [_54484] : [m2_functor0(_54484, _53821, _53819), -(l2_functor0(_54484, _53821, _53819))]], -(v3_struct_0(_53821)), v2_altcat_1(_53821), v12_altcat_1(_53821), l2_altcat_1(_53821), -(v3_struct_0(_53819)), v12_altcat_1(_53819), l2_altcat_1(_53819)], (2174 ^ _22183) ^ [_54727, _54729, _54731] : [m2_relset_1(_54727, _54731, _54729), -(m1_subset_1(_54727, k1_zfmisc_1(k2_zfmisc_1(_54731, _54729))))], (2180 ^ _22183) ^ [_54969, _54971, _54973] : [m1_pboole(_54971, _54973), m1_pboole(_54969, _54973), 2187 ^ _22183 : [(2188 ^ _22183) ^ [_55205] : [m3_pboole(_55205, _54973, _54971, _54969), -(m1_pboole(_55205, _54973))]]], (2194 ^ _22183) ^ [_55430] : [l1_altcat_1(_55430), -(m1_pboole(u1_altcat_1(_55430), k2_zfmisc_1(u1_struct_0(_55430), u1_struct_0(_55430))))], (2200 ^ _22183) ^ [_55664, _55666, _55668] : [2211 ^ _22183 : [(2212 ^ _22183) ^ [] : [-(v1_funct_1(u1_functor0(_55668, _55666, _55664)))], (2214 ^ _22183) ^ [] : [-(v1_funct_2(u1_functor0(_55668, _55666, _55664), k2_zfmisc_1(u1_struct_0(_55668), u1_struct_0(_55668)), k2_zfmisc_1(u1_struct_0(_55666), u1_struct_0(_55666))))], (2216 ^ _22183) ^ [] : [-(m2_relset_1(u1_functor0(_55668, _55666, _55664), k2_zfmisc_1(u1_struct_0(_55668), u1_struct_0(_55668)), k2_zfmisc_1(u1_struct_0(_55666), u1_struct_0(_55666))))]], l1_struct_0(_55668), l1_struct_0(_55666), l1_functor0(_55664, _55668, _55666)], (2218 ^ _22183) ^ [] : [true___, -(true___)], (2224 ^ _22183) ^ [_56404] : [l2_altcat_1(_56404), -(m3_pboole(u2_altcat_1(_56404), k3_zfmisc_1(u1_struct_0(_56404), u1_struct_0(_56404), u1_struct_0(_56404)), k3_altcat_1(u1_struct_0(_56404), u1_altcat_1(_56404), u1_altcat_1(_56404)), k2_altcat_1(u1_struct_0(_56404), u1_altcat_1(_56404))))], (2230 ^ _22183) ^ [_56682, _56684, _56686] : [-(m1_functor0(u2_functor0(_56686, _56684, _56682), k2_zfmisc_1(u1_struct_0(_56686), u1_struct_0(_56686)), k2_zfmisc_1(u1_struct_0(_56684), u1_struct_0(_56684)), u1_functor0(_56686, _56684, _56682), u1_altcat_1(_56686), u1_altcat_1(_56684))), l1_altcat_1(_56686), l1_altcat_1(_56684), l2_functor0(_56682, _56686, _56684)], (2245 ^ _22183) ^ [] : [-(l1_altcat_1(2243 ^ []))], (2247 ^ _22183) ^ [_57231, _57233] : [-(l1_functor0(2254 ^ [_57231, _57233], _57233, _57231)), l1_struct_0(_57233), l1_struct_0(_57231)], (2259 ^ _22183) ^ [] : [-(l1_struct_0(2257 ^ []))], (2262 ^ _22183) ^ [] : [-(l2_altcat_1(2260 ^ []))], (2264 ^ _22183) ^ [_57764, _57766] : [-(l2_functor0(2271 ^ [_57764, _57766], _57766, _57764)), l1_altcat_1(_57766), l1_altcat_1(_57764)], (2275 ^ _22183) ^ [_58105] : [l2_altcat_1(_58105), -(m1_altcat_2(2278 ^ [_58105], _58105))], (2282 ^ _22183) ^ [_58400, _58402, _58404, _58406, _58408] : [-(m1_functor0(2301 ^ [_58400, _58402, _58404, _58406, _58408], _58408, _58406, _58404, _58402, _58400)), v1_funct_1(_58404), v1_funct_2(_58404, _58408, _58406), m1_relset_1(_58404, _58408, _58406), m1_pboole(_58402, _58408), m1_pboole(_58400, _58406)], (2306 ^ _22183) ^ [_59131] : [-(m1_pboole(2304 ^ [_59131], _59131))], (2309 ^ _22183) ^ [_59270, _59272] : [-(m1_relset_1(2307 ^ [_59270, _59272], _59272, _59270))], (2312 ^ _22183) ^ [_59397] : [-(m1_subset_1(2310 ^ [_59397], _59397))], (2314 ^ _22183) ^ [_59509, _59511] : [-(m2_functor0(2341 ^ [_59509, _59511], _59511, _59509)), -(v3_struct_0(_59511)), v2_altcat_1(_59511), v12_altcat_1(_59511), l2_altcat_1(_59511), -(v3_struct_0(_59509)), v12_altcat_1(_59509), l2_altcat_1(_59509)], (2346 ^ _22183) ^ [_60332, _60334] : [-(m2_relset_1(2344 ^ [_60332, _60334], _60334, _60332))], (2348 ^ _22183) ^ [_60463, _60465, _60467] : [-(m3_pboole(2355 ^ [_60463, _60465, _60467], _60467, _60465, _60463)), m1_pboole(_60465, _60467), m1_pboole(_60463, _60467)], (2359 ^ _22183) ^ [_60841, _60843] : [-(v1_finset_1(k2_zfmisc_1(_60843, _60841))), v1_finset_1(_60843), v1_finset_1(_60841)], (2369 ^ _22183) ^ [_61154, _61156, _61158] : [-(v1_finset_1(k3_zfmisc_1(_61158, _61156, _61154))), v1_finset_1(_61158), v1_finset_1(_61156), v1_finset_1(_61154)], (2383 ^ _22183) ^ [_61542] : [v1_xboole_0(u1_struct_0(_61542)), -(v3_struct_0(_61542)), l1_struct_0(_61542)], (2393 ^ _22183) ^ [_61819] : [-(v2_setfam_1(_61819)), 2396 ^ _22183 : [(2397 ^ _22183) ^ [] : [v3_struct_0(k4_waybel34(_61819))], (2399 ^ _22183) ^ [] : [-(v2_altcat_1(k4_waybel34(_61819)))], (2401 ^ _22183) ^ [] : [-(v6_altcat_1(k4_waybel34(_61819)))], (2403 ^ _22183) ^ [] : [-(v9_altcat_1(k4_waybel34(_61819)))], (2405 ^ _22183) ^ [] : [-(v11_altcat_1(k4_waybel34(_61819)))], (2407 ^ _22183) ^ [] : [-(v12_altcat_1(k4_waybel34(_61819)))], (2409 ^ _22183) ^ [] : [-(v1_altcat_2(k4_waybel34(_61819)))], (2411 ^ _22183) ^ [] : [-(v2_yellow18(k4_waybel34(_61819)))], (2413 ^ _22183) ^ [] : [-(v3_yellow18(k4_waybel34(_61819)))], (2415 ^ _22183) ^ [] : [-(v4_yellow18(k4_waybel34(_61819)))], (2417 ^ _22183) ^ [] : [-(v1_yellow21(k4_waybel34(_61819)))], (2419 ^ _22183) ^ [] : [-(v2_yellow21(k4_waybel34(_61819)))], (2421 ^ _22183) ^ [] : [-(v3_yellow21(k4_waybel34(_61819)))]]], (2423 ^ _22183) ^ [] : [-(v1_xboole_0(k1_xboole_0))], (2425 ^ _22183) ^ [] : [-(v1_membered(k1_xboole_0))], (2427 ^ _22183) ^ [] : [-(v2_membered(k1_xboole_0))], (2429 ^ _22183) ^ [] : [-(v3_membered(k1_xboole_0))], (2431 ^ _22183) ^ [] : [-(v4_membered(k1_xboole_0))], (2433 ^ _22183) ^ [] : [-(v5_membered(k1_xboole_0))], (2435 ^ _22183) ^ [_63230] : [-(v2_setfam_1(_63230)), 2438 ^ _22183 : [(2439 ^ _22183) ^ [] : [v3_struct_0(k5_waybel34(_63230))], (2441 ^ _22183) ^ [] : [-(v2_altcat_1(k5_waybel34(_63230)))], (2443 ^ _22183) ^ [] : [-(v6_altcat_1(k5_waybel34(_63230)))], (2445 ^ _22183) ^ [] : [-(v9_altcat_1(k5_waybel34(_63230)))], (2447 ^ _22183) ^ [] : [-(v11_altcat_1(k5_waybel34(_63230)))], (2449 ^ _22183) ^ [] : [-(v12_altcat_1(k5_waybel34(_63230)))], (2451 ^ _22183) ^ [] : [-(v1_altcat_2(k5_waybel34(_63230)))], (2453 ^ _22183) ^ [] : [-(v2_yellow18(k5_waybel34(_63230)))], (2455 ^ _22183) ^ [] : [-(v3_yellow18(k5_waybel34(_63230)))], (2457 ^ _22183) ^ [] : [-(v4_yellow18(k5_waybel34(_63230)))], (2459 ^ _22183) ^ [] : [-(v1_yellow21(k5_waybel34(_63230)))], (2461 ^ _22183) ^ [] : [-(v2_yellow21(k5_waybel34(_63230)))], (2463 ^ _22183) ^ [] : [-(v3_yellow21(k5_waybel34(_63230)))]]], (2465 ^ _22183) ^ [_64341, _64343, _64345] : [2476 ^ _22183 : [(2477 ^ _22183) ^ [] : [-(v1_relat_1(u2_functor0(_64345, _64343, _64341)))], (2479 ^ _22183) ^ [] : [-(v1_funct_1(u2_functor0(_64345, _64343, _64341)))], (2481 ^ _22183) ^ [] : [-(v1_funcop_1(u2_functor0(_64345, _64343, _64341)))]], l1_altcat_1(_64345), l1_altcat_1(_64343), l2_functor0(_64341, _64345, _64343)], (2483 ^ _22183) ^ [_64898] : [-(v2_setfam_1(_64898)), 2486 ^ _22183 : [(2487 ^ _22183) ^ [] : [-(v6_functor0(k6_waybel34(_64898), k4_waybel34(_64898), k5_waybel34(_64898)))], (2489 ^ _22183) ^ [] : [-(v8_functor0(k6_waybel34(_64898), k4_waybel34(_64898), k5_waybel34(_64898)))], (2491 ^ _22183) ^ [] : [-(v9_functor0(k6_waybel34(_64898), k4_waybel34(_64898), k5_waybel34(_64898)))], (2493 ^ _22183) ^ [] : [-(v11_functor0(k6_waybel34(_64898), k4_waybel34(_64898), k5_waybel34(_64898)))], (2495 ^ _22183) ^ [] : [-(v12_functor0(k6_waybel34(_64898), k4_waybel34(_64898), k5_waybel34(_64898)))], (2497 ^ _22183) ^ [] : [-(v14_functor0(k6_waybel34(_64898), k4_waybel34(_64898), k5_waybel34(_64898)))], (2499 ^ _22183) ^ [] : [-(v16_functor0(k6_waybel34(_64898), k4_waybel34(_64898), k5_waybel34(_64898)))], (2501 ^ _22183) ^ [] : [-(v21_functor0(k6_waybel34(_64898), k4_waybel34(_64898), k5_waybel34(_64898)))]]], (2503 ^ _22183) ^ [_65706] : [-(v2_setfam_1(_65706)), 2506 ^ _22183 : [(2507 ^ _22183) ^ [] : [-(v6_functor0(k7_waybel34(_65706), k5_waybel34(_65706), k4_waybel34(_65706)))], (2509 ^ _22183) ^ [] : [-(v8_functor0(k7_waybel34(_65706), k5_waybel34(_65706), k4_waybel34(_65706)))], (2511 ^ _22183) ^ [] : [-(v9_functor0(k7_waybel34(_65706), k5_waybel34(_65706), k4_waybel34(_65706)))], (2513 ^ _22183) ^ [] : [-(v11_functor0(k7_waybel34(_65706), k5_waybel34(_65706), k4_waybel34(_65706)))], (2515 ^ _22183) ^ [] : [-(v12_functor0(k7_waybel34(_65706), k5_waybel34(_65706), k4_waybel34(_65706)))], (2517 ^ _22183) ^ [] : [-(v14_functor0(k7_waybel34(_65706), k5_waybel34(_65706), k4_waybel34(_65706)))], (2519 ^ _22183) ^ [] : [-(v16_functor0(k7_waybel34(_65706), k5_waybel34(_65706), k4_waybel34(_65706)))], (2521 ^ _22183) ^ [] : [-(v21_functor0(k7_waybel34(_65706), k5_waybel34(_65706), k4_waybel34(_65706)))]]], (2523 ^ _22183) ^ [_66542, _66544, _66546] : [m1_pboole(_66544, k2_zfmisc_1(_66546, _66546)), m3_pboole(_66542, k3_zfmisc_1(_66546, _66546, _66546), k3_altcat_1(_66546, _66544, _66544), k2_altcat_1(_66546, _66544)), 2530 ^ _22183 : [(2531 ^ _22183) ^ [_66866, _66868, _66870] : [g2_altcat_1(_66546, _66544, _66542) = g2_altcat_1(_66870, _66868, _66866), 2534 ^ _22183 : [(2535 ^ _22183) ^ [] : [-(_66546 = _66870)], (2537 ^ _22183) ^ [] : [-(_66544 = _66868)], (2539 ^ _22183) ^ [] : [-(_66542 = _66866)]]]]], (2541 ^ _22183) ^ [_67322, _67324, _67326, _67328] : [2564 ^ _22183 : [(2565 ^ _22183) ^ [_68135, _68137, _68139, _68141] : [g2_functor0(_67328, _67326, _67324, _67322) = g2_functor0(_68141, _68139, _68137, _68135), 2568 ^ _22183 : [(2569 ^ _22183) ^ [] : [-(_67328 = _68141)], (2571 ^ _22183) ^ [] : [-(_67326 = _68139)], (2573 ^ _22183) ^ [] : [-(_67324 = _68137)], (2575 ^ _22183) ^ [] : [-(_67322 = _68135)]]]], l1_altcat_1(_67328), l1_altcat_1(_67326), v1_funct_1(_67324), v1_funct_2(_67324, k2_zfmisc_1(u1_struct_0(_67328), u1_struct_0(_67328)), k2_zfmisc_1(u1_struct_0(_67326), u1_struct_0(_67326))), m1_relset_1(_67324, k2_zfmisc_1(u1_struct_0(_67328), u1_struct_0(_67328)), k2_zfmisc_1(u1_struct_0(_67326), u1_struct_0(_67326))), m1_functor0(_67322, k2_zfmisc_1(u1_struct_0(_67328), u1_struct_0(_67328)), k2_zfmisc_1(u1_struct_0(_67326), u1_struct_0(_67326)), _67324, u1_altcat_1(_67328), u1_altcat_1(_67326))], (2578 ^ _22183) ^ [] : [v1_xboole_0(2576 ^ [])], (2580 ^ _22183) ^ [] : [-(v1_finset_1(2576 ^ []))], (2583 ^ _22183) ^ [] : [-(v1_relat_1(2581 ^ []))], (2585 ^ _22183) ^ [] : [-(v1_funct_1(2581 ^ []))], (2588 ^ _22183) ^ [] : [v1_xboole_0(2586 ^ [])], (2590 ^ _22183) ^ [] : [-(v1_membered(2586 ^ []))], (2592 ^ _22183) ^ [] : [-(v2_membered(2586 ^ []))], (2594 ^ _22183) ^ [] : [-(v3_membered(2586 ^ []))], (2596 ^ _22183) ^ [] : [-(v4_membered(2586 ^ []))], (2598 ^ _22183) ^ [] : [-(v5_membered(2586 ^ []))], (2601 ^ _22183) ^ [] : [-(l2_altcat_1(2599 ^ []))], (2603 ^ _22183) ^ [] : [v3_struct_0(2599 ^ [])], (2605 ^ _22183) ^ [] : [-(v2_altcat_1(2599 ^ []))], (2607 ^ _22183) ^ [] : [-(v6_altcat_1(2599 ^ []))], (2609 ^ _22183) ^ [] : [-(v9_altcat_1(2599 ^ []))], (2611 ^ _22183) ^ [] : [-(v11_altcat_1(2599 ^ []))], (2613 ^ _22183) ^ [] : [-(v12_altcat_1(2599 ^ []))], (2615 ^ _22183) ^ [] : [-(v1_altcat_2(2599 ^ []))], (2617 ^ _22183) ^ [] : [-(v2_yellow18(2599 ^ []))], (2619 ^ _22183) ^ [] : [-(v3_yellow18(2599 ^ []))], (2621 ^ _22183) ^ [] : [-(v4_yellow18(2599 ^ []))], (2623 ^ _22183) ^ [] : [-(v1_yellow21(2599 ^ []))], (2625 ^ _22183) ^ [] : [-(v2_yellow21(2599 ^ []))], (2627 ^ _22183) ^ [] : [-(v3_yellow21(2599 ^ []))], (2630 ^ _22183) ^ [] : [-(v1_relat_1(2628 ^ []))], (2632 ^ _22183) ^ [] : [-(v1_xboole_0(2628 ^ []))], (2634 ^ _22183) ^ [] : [-(v1_funct_1(2628 ^ []))], (2637 ^ _22183) ^ [] : [v2_setfam_1(2635 ^ [])], (2639 ^ _22183) ^ [_70517] : [-(v1_xboole_0(_70517)), 2643 ^ _22183 : [(2644 ^ _22183) ^ [] : [-(m1_subset_1(2642 ^ [_70517], k1_zfmisc_1(_70517)))], (2646 ^ _22183) ^ [] : [v1_xboole_0(2642 ^ [_70517])], (2648 ^ _22183) ^ [] : [-(v1_finset_1(2642 ^ [_70517]))]]], (2651 ^ _22183) ^ [] : [-(v1_relat_1(2649 ^ []))], (2653 ^ _22183) ^ [] : [-(v1_funct_1(2649 ^ []))], (2655 ^ _22183) ^ [] : [-(v2_funct_1(2649 ^ []))], (2657 ^ _22183) ^ [_71152, _71154] : [2665 ^ _22183 : [(2666 ^ _22183) ^ [] : [-(l2_functor0(2664 ^ [_71152, _71154], _71154, _71152))], (2668 ^ _22183) ^ [] : [-(v9_functor0(2664 ^ [_71152, _71154], _71154, _71152))]], l1_altcat_1(_71154), l1_altcat_1(_71152)], (2670 ^ _22183) ^ [_71584] : [-(v2_setfam_1(_71584)), 2674 ^ _22183 : [(2675 ^ _22183) ^ [] : [-(m1_subset_1(2673 ^ [_71584], _71584))], (2677 ^ _22183) ^ [] : [v1_xboole_0(2673 ^ [_71584])]]], (2680 ^ _22183) ^ [] : [-(l1_struct_0(2678 ^ []))], (2682 ^ _22183) ^ [] : [v3_struct_0(2678 ^ [])], (2684 ^ _22183) ^ [_72060] : [-(v1_xboole_0(_72060)), 2688 ^ _22183 : [(2689 ^ _22183) ^ [] : [-(m1_subset_1(2687 ^ [_72060], k1_zfmisc_1(_72060)))], (2691 ^ _22183) ^ [] : [v1_xboole_0(2687 ^ [_72060])], (2693 ^ _22183) ^ [] : [-(v1_finset_1(2687 ^ [_72060]))]]], (2695 ^ _22183) ^ [_72486, _72488] : [2703 ^ _22183 : [(2704 ^ _22183) ^ [] : [-(l2_functor0(2702 ^ [_72486, _72488], _72488, _72486))], (2706 ^ _22183) ^ [] : [-(v11_functor0(2702 ^ [_72486, _72488], _72488, _72486))]], l1_altcat_1(_72488), l1_altcat_1(_72486)], (2708 ^ _22183) ^ [_72918] : [2716 ^ _22183 : [(2717 ^ _22183) ^ [] : [-(m1_subset_1(2715 ^ [_72918], k1_zfmisc_1(u1_struct_0(_72918))))], (2719 ^ _22183) ^ [] : [v1_xboole_0(2715 ^ [_72918])]], -(v3_struct_0(_72918)), l1_struct_0(_72918)], (2722 ^ _22183) ^ [] : [-(l2_altcat_1(2720 ^ []))], (2724 ^ _22183) ^ [] : [v3_struct_0(2720 ^ [])], (2726 ^ _22183) ^ [] : [-(v1_altcat_2(2720 ^ []))], (2728 ^ _22183) ^ [_73563, _73565] : [2748 ^ _22183 : [(2749 ^ _22183) ^ [] : [-(l2_functor0(2747 ^ [_73563, _73565], _73565, _73563))], (2751 ^ _22183) ^ [] : [-(v6_functor0(2747 ^ [_73563, _73565], _73565, _73563))], (2753 ^ _22183) ^ [] : [-(v8_functor0(2747 ^ [_73563, _73565], _73565, _73563))]], -(v3_struct_0(_73565)), l1_altcat_1(_73565), -(v3_struct_0(_73563)), v1_altcat_2(_73563), l1_altcat_1(_73563)], (2755 ^ _22183) ^ [_74366, _74368] : [2779 ^ _22183 : [(2780 ^ _22183) ^ [] : [-(l2_functor0(2778 ^ [_74366, _74368], _74368, _74366))], (2782 ^ _22183) ^ [] : [-(v6_functor0(2778 ^ [_74366, _74368], _74368, _74366))], (2784 ^ _22183) ^ [] : [-(v8_functor0(2778 ^ [_74366, _74368], _74368, _74366))], (2786 ^ _22183) ^ [] : [-(v9_functor0(2778 ^ [_74366, _74368], _74368, _74366))], (2788 ^ _22183) ^ [] : [-(v12_functor0(2778 ^ [_74366, _74368], _74368, _74366))]], -(v3_struct_0(_74368)), v12_altcat_1(_74368), l2_altcat_1(_74368), -(v3_struct_0(_74366)), v12_altcat_1(_74366), l2_altcat_1(_74366)], (2790 ^ _22183) ^ [_75479, _75481, _75483] : [m2_relset_1(_75479, _75483, _75481), -(m1_relset_1(_75479, _75483, _75481))], (2796 ^ _22183) ^ [_75651, _75653, _75655] : [m1_relset_1(_75651, _75655, _75653), -(m2_relset_1(_75651, _75655, _75653))], (2802 ^ _22183) ^ [_75858, _75860] : [-(r1_tarski(_75860, _75860))], (2804 ^ _22183) ^ [_75953] : [-(v2_setfam_1(_75953)), 2807 ^ _22183 : [(2808 ^ _22183) ^ [] : [-(k15_functor0(k4_waybel34(_75953), k5_waybel34(_75953), k6_waybel34(_75953)) = k7_waybel34(_75953))], (2810 ^ _22183) ^ [] : [-(k15_functor0(k5_waybel34(_75953), k4_waybel34(_75953), k7_waybel34(_75953)) = k6_waybel34(_75953))]]], (2812 ^ _22183) ^ [_76279, _76281] : [r2_hidden(_76281, _76279), -(m1_subset_1(_76281, _76279))], (2818 ^ _22183) ^ [_76489, _76491] : [m1_subset_1(_76491, _76489), -(v1_xboole_0(_76489)), -(r2_hidden(_76491, _76489))], (2828 ^ _22183) ^ [_76816, _76818] : [m1_subset_1(_76818, k1_zfmisc_1(_76816)), -(r1_tarski(_76818, _76816))], (2834 ^ _22183) ^ [_76982, _76984] : [r1_tarski(_76984, _76982), -(m1_subset_1(_76984, k1_zfmisc_1(_76982)))], (2840 ^ _22183) ^ [_77212, _77214, _77216] : [-(m1_subset_1(_77216, _77212)), r2_hidden(_77216, _77214), m1_subset_1(_77214, k1_zfmisc_1(_77212))], (2850 ^ _22183) ^ [_77511] : [-(v3_struct_0(_77511)), v2_altcat_1(_77511), v11_altcat_1(_77511), v12_altcat_1(_77511), l2_altcat_1(_77511), 2869 ^ _22183 : [(2870 ^ _22183) ^ [_78098] : [-(v3_struct_0(_78098)), v2_altcat_1(_78098), v11_altcat_1(_78098), v12_altcat_1(_78098), l2_altcat_1(_78098), 2889 ^ _22183 : [(2890 ^ _22183) ^ [_78675] : [v16_functor0(_78675, _77511, _78098), m2_functor0(_78675, _77511, _78098), v21_functor0(_78675, _77511, _78098), 2901 ^ _22183 : [(2902 ^ _22183) ^ [_79071] : [-(v3_struct_0(_79071)), v2_altcat_1(_79071), v3_altcat_2(_79071, _77511), m1_altcat_2(_79071, _77511), 2917 ^ _22183 : [(2918 ^ _22183) ^ [_79546] : [r3_yellow20(_77511, _78098, _78675, _79071, _79546), -(r3_yellow20(_78098, _77511, k15_functor0(_77511, _78098, _78675), _79546, _79071)), -(v3_struct_0(_79546)), v2_altcat_1(_79546), v3_altcat_2(_79546, _78098), m1_altcat_2(_79546, _78098)]]]]]]]]], (2940 ^ _22183) ^ [_80241] : [-(v2_setfam_1(_80241)), -(r3_yellow20(k4_waybel34(_80241), k5_waybel34(_80241), k6_waybel34(_80241), k8_waybel34(_80241), k9_waybel34(_80241)))], (2946 ^ _22183) ^ [_80486, _80488, _80490] : [r2_hidden(_80490, _80488), m1_subset_1(_80488, k1_zfmisc_1(_80486)), v1_xboole_0(_80486)], (2956 ^ _22183) ^ [_80782] : [v1_xboole_0(_80782), -(_80782 = k1_xboole_0)], (2962 ^ _22183) ^ [_80984, _80986] : [r2_hidden(_80986, _80984), v1_xboole_0(_80984)], (2968 ^ _22183) ^ [_81171, _81173] : [v1_xboole_0(_81173), -(_81173 = _81171), v1_xboole_0(_81171)]], input).
% 16.39/16.95 ncf('1',plain,[v2_setfam_1(2977 ^ [])],start(2979 ^ 0)).
% 16.39/16.95 ncf('1.1',plain,[-(v2_setfam_1(2977 ^ [])), 2036 : v3_struct_0(k9_waybel34(2977 ^ []))],extension(2032 ^ 1,bind([[_50632], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1',plain,[-(v3_struct_0(k9_waybel34(2977 ^ []))), 2918 : r3_yellow20(k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []), k6_waybel34(2977 ^ []), k8_waybel34(2977 ^ []), k9_waybel34(2977 ^ [])), 2918 : -(r3_yellow20(k5_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k15_functor0(k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []), k6_waybel34(2977 ^ [])), k9_waybel34(2977 ^ []), k8_waybel34(2977 ^ []))), 2918 : v2_altcat_1(k9_waybel34(2977 ^ [])), 2918 : v3_altcat_2(k9_waybel34(2977 ^ []), k5_waybel34(2977 ^ [])), 2918 : m1_altcat_2(k9_waybel34(2977 ^ []), k5_waybel34(2977 ^ [])), 2918 : -(v3_struct_0(k8_waybel34(2977 ^ []))), 2918 : v2_altcat_1(k8_waybel34(2977 ^ [])), 2918 : v3_altcat_2(k8_waybel34(2977 ^ []), k4_waybel34(2977 ^ [])), 2918 : m1_altcat_2(k8_waybel34(2977 ^ []), k4_waybel34(2977 ^ [])), 2902 : v16_functor0(k6_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ [])), 2902 : m2_functor0(k6_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ [])), 2902 : v21_functor0(k6_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ [])), 2890 : -(v3_struct_0(k5_waybel34(2977 ^ []))), 2890 : v2_altcat_1(k5_waybel34(2977 ^ [])), 2890 : v11_altcat_1(k5_waybel34(2977 ^ [])), 2890 : v12_altcat_1(k5_waybel34(2977 ^ [])), 2890 : l2_altcat_1(k5_waybel34(2977 ^ [])), 2870 : -(v3_struct_0(k4_waybel34(2977 ^ []))), 2870 : v2_altcat_1(k4_waybel34(2977 ^ [])), 2870 : v11_altcat_1(k4_waybel34(2977 ^ [])), 2870 : v12_altcat_1(k4_waybel34(2977 ^ [])), 2870 : l2_altcat_1(k4_waybel34(2977 ^ []))],extension(2850 ^ 4,bind([[_77511, _78098, _78675, _79071, _79546], [k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []), k6_waybel34(2977 ^ []), k8_waybel34(2977 ^ []), k9_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.1',plain,[-(r3_yellow20(k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []), k6_waybel34(2977 ^ []), k8_waybel34(2977 ^ []), k9_waybel34(2977 ^ []))), r3_yellow20(k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []), k6_waybel34(2977 ^ []), k8_waybel34(2977 ^ []), k9_waybel34(2977 ^ [])), k4_waybel34(2977 ^ []) = k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []) = k5_waybel34(2977 ^ []), k6_waybel34(2977 ^ []) = k6_waybel34(2977 ^ []), k8_waybel34(2977 ^ []) = k8_waybel34(2977 ^ []), k9_waybel34(2977 ^ []) = k9_waybel34(2977 ^ [])],extension(738 ^ 13,bind([[_32389, _32391, _32393, _32395, _32397, _32399, _32401, _32403, _32405, _32407], [k9_waybel34(2977 ^ []), k9_waybel34(2977 ^ []), k8_waybel34(2977 ^ []), k8_waybel34(2977 ^ []), k6_waybel34(2977 ^ []), k6_waybel34(2977 ^ []), k5_waybel34(2977 ^ []), k5_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k4_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.1.1',plain,[-(r3_yellow20(k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []), k6_waybel34(2977 ^ []), k8_waybel34(2977 ^ []), k9_waybel34(2977 ^ []))), -(v2_setfam_1(2977 ^ []))],extension(2940 ^ 14,bind([[_80241], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.1.1.1',plain,[v2_setfam_1(2977 ^ [])],reduction('1')).
% 16.39/16.95 ncf('1.1.1.1.2',plain,[-(k4_waybel34(2977 ^ []) = k4_waybel34(2977 ^ []))],extension(2 ^ 14,bind([[_22213], [k4_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.1.3',plain,[-(k5_waybel34(2977 ^ []) = k5_waybel34(2977 ^ []))],extension(2 ^ 14,bind([[_22213], [k5_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.1.4',plain,[-(k6_waybel34(2977 ^ []) = k6_waybel34(2977 ^ []))],extension(2 ^ 14,bind([[_22213], [k6_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.1.5',plain,[-(k8_waybel34(2977 ^ []) = k8_waybel34(2977 ^ []))],extension(2 ^ 14,bind([[_22213], [k8_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.1.6',plain,[-(k9_waybel34(2977 ^ []) = k9_waybel34(2977 ^ []))],extension(2 ^ 14,bind([[_22213], [k9_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.2',plain,[r3_yellow20(k5_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k15_functor0(k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []), k6_waybel34(2977 ^ [])), k9_waybel34(2977 ^ []), k8_waybel34(2977 ^ [])), -(r3_yellow20(k5_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k7_waybel34(2977 ^ []), k9_waybel34(2977 ^ []), k8_waybel34(2977 ^ []))), k5_waybel34(2977 ^ []) = k5_waybel34(2977 ^ []), k4_waybel34(2977 ^ []) = k4_waybel34(2977 ^ []), k15_functor0(k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []), k6_waybel34(2977 ^ [])) = k7_waybel34(2977 ^ []), k9_waybel34(2977 ^ []) = k9_waybel34(2977 ^ []), k8_waybel34(2977 ^ []) = k8_waybel34(2977 ^ [])],extension(738 ^ 13,bind([[_32389, _32391, _32393, _32395, _32397, _32399, _32401, _32403, _32405, _32407], [k8_waybel34(2977 ^ []), k8_waybel34(2977 ^ []), k9_waybel34(2977 ^ []), k9_waybel34(2977 ^ []), k7_waybel34(2977 ^ []), k15_functor0(k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []), k6_waybel34(2977 ^ [])), k4_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []), k5_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.2.1',plain,[r3_yellow20(k5_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k7_waybel34(2977 ^ []), k9_waybel34(2977 ^ []), k8_waybel34(2977 ^ []))],extension(2981 ^ 14)).
% 16.39/16.95 ncf('1.1.1.2.2',plain,[-(k5_waybel34(2977 ^ []) = k5_waybel34(2977 ^ []))],extension(2 ^ 14,bind([[_22213], [k5_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.2.3',plain,[-(k4_waybel34(2977 ^ []) = k4_waybel34(2977 ^ []))],extension(2 ^ 14,bind([[_22213], [k4_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.2.4',plain,[-(k15_functor0(k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []), k6_waybel34(2977 ^ [])) = k7_waybel34(2977 ^ [])), -(v2_setfam_1(2977 ^ []))],extension(2804 ^ 14,bind([[_75953], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.2.4.1',plain,[v2_setfam_1(2977 ^ [])],reduction('1')).
% 16.39/16.95 ncf('1.1.1.2.5',plain,[-(k9_waybel34(2977 ^ []) = k9_waybel34(2977 ^ []))],extension(2 ^ 14,bind([[_22213], [k9_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.2.6',plain,[-(k8_waybel34(2977 ^ []) = k8_waybel34(2977 ^ []))],extension(2 ^ 14,bind([[_22213], [k8_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.3',plain,[-(v2_altcat_1(k9_waybel34(2977 ^ [])))],extension(2038 ^ 13)).
% 16.39/16.95 ncf('1.1.1.4',plain,[-(v3_altcat_2(k9_waybel34(2977 ^ []), k5_waybel34(2977 ^ [])))],extension(2042 ^ 13)).
% 16.39/16.95 ncf('1.1.1.5',plain,[-(m1_altcat_2(k9_waybel34(2977 ^ []), k5_waybel34(2977 ^ [])))],extension(2044 ^ 13)).
% 16.39/16.95 ncf('1.1.1.6',plain,[v3_struct_0(k8_waybel34(2977 ^ [])), -(v1_xboole_0(2977 ^ []))],extension(2018 ^ 11,bind([[_50431], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.6.1',plain,[v1_xboole_0(2977 ^ []), -(v2_setfam_1(2977 ^ []))],extension(1372 ^ 12,bind([[_41628], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.6.1.1',plain,[v2_setfam_1(2977 ^ [])],reduction('1')).
% 16.39/16.95 ncf('1.1.1.7',plain,[-(v2_altcat_1(k8_waybel34(2977 ^ []))), -(v1_xboole_0(2977 ^ []))],extension(2018 ^ 11,bind([[_50431], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.7.1',plain,[v1_xboole_0(2977 ^ []), -(v2_setfam_1(2977 ^ []))],extension(1372 ^ 12,bind([[_41628], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.7.1.1',plain,[v2_setfam_1(2977 ^ [])],reduction('1')).
% 16.39/16.95 ncf('1.1.1.8',plain,[-(v3_altcat_2(k8_waybel34(2977 ^ []), k4_waybel34(2977 ^ []))), -(v1_xboole_0(2977 ^ []))],extension(2018 ^ 11,bind([[_50431], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.8.1',plain,[v1_xboole_0(2977 ^ []), -(v2_setfam_1(2977 ^ []))],extension(1372 ^ 12,bind([[_41628], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.8.1.1',plain,[v2_setfam_1(2977 ^ [])],reduction('1')).
% 16.39/16.95 ncf('1.1.1.9',plain,[-(m1_altcat_2(k8_waybel34(2977 ^ []), k4_waybel34(2977 ^ []))), -(v1_xboole_0(2977 ^ []))],extension(2018 ^ 11,bind([[_50431], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.9.1',plain,[v1_xboole_0(2977 ^ []), -(v2_setfam_1(2977 ^ []))],extension(1372 ^ 12,bind([[_41628], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.9.1.1',plain,[v2_setfam_1(2977 ^ [])],reduction('1')).
% 16.39/16.95 ncf('1.1.1.10',plain,[-(v16_functor0(k6_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []))), v16_functor0(k6_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ [])), k6_waybel34(2977 ^ []) = k6_waybel34(2977 ^ []), k4_waybel34(2977 ^ []) = k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []) = k5_waybel34(2977 ^ [])],extension(588 ^ 9,bind([[_30314, _30316, _30318, _30320, _30322, _30324], [k5_waybel34(2977 ^ []), k5_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k6_waybel34(2977 ^ []), k6_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.10.1',plain,[-(v16_functor0(k6_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []))), -(v2_setfam_1(2977 ^ []))],extension(1998 ^ 10,bind([[_50218], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.10.1.1',plain,[v2_setfam_1(2977 ^ [])],reduction('1')).
% 16.39/16.95 ncf('1.1.1.10.2',plain,[-(k6_waybel34(2977 ^ []) = k6_waybel34(2977 ^ []))],extension(2 ^ 10,bind([[_22213], [k6_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.10.3',plain,[-(k4_waybel34(2977 ^ []) = k4_waybel34(2977 ^ []))],extension(2 ^ 10,bind([[_22213], [k4_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.10.4',plain,[-(k5_waybel34(2977 ^ []) = k5_waybel34(2977 ^ []))],extension(2 ^ 10,bind([[_22213], [k5_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.11',plain,[-(m2_functor0(k6_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []))), m2_functor0(k6_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ [])), k6_waybel34(2977 ^ []) = k6_waybel34(2977 ^ []), k4_waybel34(2977 ^ []) = k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []) = k5_waybel34(2977 ^ [])],extension(606 ^ 9,bind([[_30583, _30585, _30587, _30589, _30591, _30593], [k5_waybel34(2977 ^ []), k5_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k6_waybel34(2977 ^ []), k6_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.11.1',plain,[-(m2_functor0(k6_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []))), -(v2_setfam_1(2977 ^ []))],extension(1998 ^ 10,bind([[_50218], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.11.1.1',plain,[v2_setfam_1(2977 ^ [])],reduction('1')).
% 16.39/16.95 ncf('1.1.1.11.2',plain,[-(k6_waybel34(2977 ^ []) = k6_waybel34(2977 ^ []))],extension(2 ^ 10,bind([[_22213], [k6_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.11.3',plain,[-(k4_waybel34(2977 ^ []) = k4_waybel34(2977 ^ []))],extension(2 ^ 10,bind([[_22213], [k4_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.11.4',plain,[-(k5_waybel34(2977 ^ []) = k5_waybel34(2977 ^ []))],extension(2 ^ 10,bind([[_22213], [k5_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.12',plain,[-(v21_functor0(k6_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []))), v21_functor0(k6_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ [])), k6_waybel34(2977 ^ []) = k6_waybel34(2977 ^ []), k4_waybel34(2977 ^ []) = k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []) = k5_waybel34(2977 ^ [])],extension(624 ^ 9,bind([[_30852, _30854, _30856, _30858, _30860, _30862], [k5_waybel34(2977 ^ []), k5_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k6_waybel34(2977 ^ []), k6_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.12.1',plain,[-(v21_functor0(k6_waybel34(2977 ^ []), k4_waybel34(2977 ^ []), k5_waybel34(2977 ^ []))), -(v2_setfam_1(2977 ^ []))],extension(2483 ^ 10,bind([[_64898], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.12.1.1',plain,[v2_setfam_1(2977 ^ [])],reduction('1')).
% 16.39/16.95 ncf('1.1.1.12.2',plain,[-(k6_waybel34(2977 ^ []) = k6_waybel34(2977 ^ []))],extension(2 ^ 10,bind([[_22213], [k6_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.12.3',plain,[-(k4_waybel34(2977 ^ []) = k4_waybel34(2977 ^ []))],extension(2 ^ 10,bind([[_22213], [k4_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.12.4',plain,[-(k5_waybel34(2977 ^ []) = k5_waybel34(2977 ^ []))],extension(2 ^ 10,bind([[_22213], [k5_waybel34(2977 ^ [])]]))).
% 16.39/16.95 ncf('1.1.1.13',plain,[v3_struct_0(k5_waybel34(2977 ^ [])), -(v1_xboole_0(2977 ^ []))],extension(1980 ^ 7,bind([[_49980], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.13.1',plain,[v1_xboole_0(2977 ^ []), -(v2_setfam_1(2977 ^ []))],extension(1372 ^ 8,bind([[_41628], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.13.1.1',plain,[v2_setfam_1(2977 ^ [])],reduction('1')).
% 16.39/16.95 ncf('1.1.1.14',plain,[-(v2_altcat_1(k5_waybel34(2977 ^ []))), -(v1_xboole_0(2977 ^ []))],extension(1980 ^ 7,bind([[_49980], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.14.1',plain,[v1_xboole_0(2977 ^ []), -(v2_setfam_1(2977 ^ []))],extension(1372 ^ 8,bind([[_41628], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.14.1.1',plain,[v2_setfam_1(2977 ^ [])],reduction('1')).
% 16.39/16.95 ncf('1.1.1.15',plain,[-(v11_altcat_1(k5_waybel34(2977 ^ []))), -(v1_xboole_0(2977 ^ []))],extension(1980 ^ 7,bind([[_49980], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.15.1',plain,[v1_xboole_0(2977 ^ []), -(v2_setfam_1(2977 ^ []))],extension(1372 ^ 8,bind([[_41628], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.15.1.1',plain,[v2_setfam_1(2977 ^ [])],reduction('1')).
% 16.39/16.95 ncf('1.1.1.16',plain,[-(v12_altcat_1(k5_waybel34(2977 ^ []))), -(v1_xboole_0(2977 ^ []))],extension(1980 ^ 7,bind([[_49980], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.16.1',plain,[v1_xboole_0(2977 ^ []), -(v2_setfam_1(2977 ^ []))],extension(1372 ^ 8,bind([[_41628], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.16.1.1',plain,[v2_setfam_1(2977 ^ [])],reduction('1')).
% 16.39/16.95 ncf('1.1.1.17',plain,[-(l2_altcat_1(k5_waybel34(2977 ^ []))), -(v1_xboole_0(2977 ^ []))],extension(1980 ^ 7,bind([[_49980], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.17.1',plain,[v1_xboole_0(2977 ^ []), -(v2_setfam_1(2977 ^ []))],extension(1372 ^ 8,bind([[_41628], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.17.1.1',plain,[v2_setfam_1(2977 ^ [])],reduction('1')).
% 16.39/16.95 ncf('1.1.1.18',plain,[v3_struct_0(k4_waybel34(2977 ^ [])), -(v1_xboole_0(2977 ^ []))],extension(1962 ^ 5,bind([[_49739], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.18.1',plain,[v1_xboole_0(2977 ^ []), -(v2_setfam_1(2977 ^ []))],extension(1372 ^ 6,bind([[_41628], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.18.1.1',plain,[v2_setfam_1(2977 ^ [])],reduction('1')).
% 16.39/16.95 ncf('1.1.1.19',plain,[-(v2_altcat_1(k4_waybel34(2977 ^ []))), -(v1_xboole_0(2977 ^ []))],extension(1962 ^ 5,bind([[_49739], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.19.1',plain,[v1_xboole_0(2977 ^ []), -(v2_setfam_1(2977 ^ []))],extension(1372 ^ 6,bind([[_41628], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.19.1.1',plain,[v2_setfam_1(2977 ^ [])],reduction('1')).
% 16.39/16.95 ncf('1.1.1.20',plain,[-(v11_altcat_1(k4_waybel34(2977 ^ []))), -(v1_xboole_0(2977 ^ []))],extension(1962 ^ 5,bind([[_49739], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.20.1',plain,[v1_xboole_0(2977 ^ []), -(v2_setfam_1(2977 ^ []))],extension(1372 ^ 6,bind([[_41628], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.20.1.1',plain,[v2_setfam_1(2977 ^ [])],reduction('1')).
% 16.39/16.95 ncf('1.1.1.21',plain,[-(v12_altcat_1(k4_waybel34(2977 ^ []))), -(v1_xboole_0(2977 ^ []))],extension(1962 ^ 5,bind([[_49739], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.21.1',plain,[v1_xboole_0(2977 ^ []), -(v2_setfam_1(2977 ^ []))],extension(1372 ^ 6,bind([[_41628], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.21.1.1',plain,[v2_setfam_1(2977 ^ [])],reduction('1')).
% 16.39/16.95 ncf('1.1.1.22',plain,[-(l2_altcat_1(k4_waybel34(2977 ^ []))), -(v1_xboole_0(2977 ^ []))],extension(1962 ^ 5,bind([[_49739], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.22.1',plain,[v1_xboole_0(2977 ^ []), -(v2_setfam_1(2977 ^ []))],extension(1372 ^ 6,bind([[_41628], [2977 ^ []]]))).
% 16.39/16.95 ncf('1.1.1.22.1.1',plain,[v2_setfam_1(2977 ^ [])],reduction('1')).
% 16.39/16.95 %-----------------------------------------------------
% 16.39/16.95 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------