%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : ITP001+5 : TPTP v8.1.2. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n006.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:23:04 EDT 2023
% Result : Theorem 0.36s 1.37s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : ITP001+5 : TPTP v8.1.2. Bugfixed v7.5.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n006.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 18 21:54:21 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.36/1.37
% 0.36/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.36/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 ncf(matrix, plain, [(1671 ^ _323094) ^ [] : [-(true___)], (1673 ^ _323094) ^ [] : [true___], (2 ^ _323094) ^ [_323238] : [-(_323238 = _323238)], (4 ^ _323094) ^ [_323345, _323347] : [_323347 = _323345, -(_323345 = _323347)], (10 ^ _323094) ^ [_323549, _323551, _323553] : [-(_323553 = _323549), _323553 = _323551, _323551 = _323549], (20 ^ _323094) ^ [_323862, _323864] : [-(p(_323862)), _323864 = _323862, p(_323864)], (44 ^ _323094) ^ [_324581, _324583] : [-(ne(_324581)), _324583 = _324581, ne(_324583)], (30 ^ _323094) ^ [_324185, _324187, _324189, _324191] : [-(mem(_324189, _324185)), mem(_324191, _324187), _324191 = _324189, _324187 = _324185], (54 ^ _323094) ^ [_324886, _324888] : [_324888 = _324886, -(c_2Ebool_2EARB(_324888) = c_2Ebool_2EARB(_324886))], (60 ^ _323094) ^ [_325132, _325134, _325136, _325138] : [-(c_2Ebool_2ERES__ABSTRACT(_325138, _325134) = c_2Ebool_2ERES__ABSTRACT(_325136, _325132)), _325138 = _325136, _325134 = _325132], (70 ^ _323094) ^ [_325491, _325493, _325495, _325497] : [-(c_2Ebool_2Eitself__case(_325497, _325493) = c_2Ebool_2Eitself__case(_325495, _325491)), _325497 = _325495, _325493 = _325491], (80 ^ _323094) ^ [_325822, _325824] : [_325824 = _325822, -(c_2Ebool_2Ethe__value(_325824) = c_2Ebool_2Ethe__value(_325822))], (86 ^ _323094) ^ [_326040, _326042] : [_326042 = _326040, -(ty_2Ebool_2Eitself(_326042) = ty_2Ebool_2Eitself(_326040))], (92 ^ _323094) ^ [_326258, _326260] : [_326260 = _326258, -(i(_326260) = i(_326258))], (98 ^ _323094) ^ [_326476, _326478] : [_326478 = _326476, -(f1(_326478) = f1(_326476))], (104 ^ _323094) ^ [_326694, _326696] : [_326696 = _326694, -(f2(_326696) = f2(_326694))], (110 ^ _323094) ^ [_326940, _326942, _326944, _326946] : [-(f3(_326946, _326942) = f3(_326944, _326940)), _326946 = _326944, _326942 = _326940], (120 ^ _323094) ^ [_327271, _327273] : [_327273 = _327271, -(f4(_327273) = f4(_327271))], (126 ^ _323094) ^ [_327517, _327519, _327521, _327523] : [-(f6(_327523, _327519) = f6(_327521, _327517)), _327523 = _327521, _327519 = _327517], (136 ^ _323094) ^ [_327848, _327850] : [_327850 = _327848, -(f7(_327850) = f7(_327848))], (142 ^ _323094) ^ [_328122, _328124, _328126, _328128, _328130, _328132] : [-(f10(_328132, _328128, _328124) = f10(_328130, _328126, _328122)), _328132 = _328130, _328128 = _328126, _328124 = _328122], (156 ^ _323094) ^ [_328610, _328612, _328614, _328616] : [-(f11(_328616, _328612) = f11(_328614, _328610)), _328616 = _328614, _328612 = _328610], (166 ^ _323094) ^ [_328941, _328943] : [_328943 = _328941, -(c_2Ebool_2E_3F_21(_328943) = c_2Ebool_2E_3F_21(_328941))], (172 ^ _323094) ^ [_329159, _329161] : [_329161 = _329159, -(f12(_329161) = f12(_329159))], (178 ^ _323094) ^ [_329433, _329435, _329437, _329439, _329441, _329443] : [-(f13(_329443, _329439, _329435) = f13(_329441, _329437, _329433)), _329443 = _329441, _329439 = _329437, _329435 = _329433], (192 ^ _323094) ^ [_329921, _329923, _329925, _329927] : [-(c_2Ebool_2ELET(_329927, _329923) = c_2Ebool_2ELET(_329925, _329921)), _329927 = _329925, _329923 = _329921], (202 ^ _323094) ^ [_330336, _330338, _330340, _330342, _330344, _330346, _330348, _330350] : [-(f15(_330350, _330346, _330342, _330338) = f15(_330348, _330344, _330340, _330336)), _330350 = _330348, _330346 = _330344, _330342 = _330340, _330338 = _330336], (220 ^ _323094) ^ [_330997, _330999, _331001, _331003, _331005, _331007] : [-(f16(_331007, _331003, _330999) = f16(_331005, _331001, _330997)), _331007 = _331005, _331003 = _331001, _330999 = _330997], (234 ^ _323094) ^ [_331485, _331487, _331489, _331491] : [-(f17(_331491, _331487) = f17(_331489, _331485)), _331491 = _331489, _331487 = _331485], (244 ^ _323094) ^ [_331816, _331818] : [_331818 = _331816, -(c_2Ebool_2ECOND(_331818) = c_2Ebool_2ECOND(_331816))], (250 ^ _323094) ^ [_332034, _332036] : [_332036 = _332034, -(f18(_332036) = f18(_332034))], (256 ^ _323094) ^ [_332336, _332338, _332340, _332342, _332344, _332346, _332348, _332350] : [-(f19(_332350, _332346, _332342, _332338) = f19(_332348, _332344, _332340, _332336)), _332350 = _332348, _332346 = _332344, _332342 = _332340, _332338 = _332336], (274 ^ _323094) ^ [_332997, _332999, _333001, _333003, _333005, _333007] : [-(f20(_333007, _333003, _332999) = f20(_333005, _333001, _332997)), _333007 = _333005, _333003 = _333001, _332999 = _332997], (288 ^ _323094) ^ [_333485, _333487, _333489, _333491] : [-(f21(_333491, _333487) = f21(_333489, _333485)), _333491 = _333489, _333487 = _333485], (298 ^ _323094) ^ [_333900, _333902, _333904, _333906, _333908, _333910, _333912, _333914] : [-(f22(_333914, _333910, _333906, _333902) = f22(_333912, _333908, _333904, _333900)), _333914 = _333912, _333910 = _333908, _333906 = _333904, _333902 = _333900], (316 ^ _323094) ^ [_334561, _334563, _334565, _334567, _334569, _334571] : [-(f23(_334571, _334567, _334563) = f23(_334569, _334565, _334561)), _334571 = _334569, _334567 = _334565, _334563 = _334561], (330 ^ _323094) ^ [_335049, _335051, _335053, _335055] : [-(f24(_335055, _335051) = f24(_335053, _335049)), _335055 = _335053, _335051 = _335049], (340 ^ _323094) ^ [_335464, _335466, _335468, _335470, _335472, _335474, _335476, _335478] : [-(f25(_335478, _335474, _335470, _335466) = f25(_335476, _335472, _335468, _335464)), _335478 = _335476, _335474 = _335472, _335470 = _335468, _335466 = _335464], (358 ^ _323094) ^ [_336153, _336155, _336157, _336159, _336161, _336163, _336165, _336167] : [-(f27(_336167, _336163, _336159, _336155) = f27(_336165, _336161, _336157, _336153)), _336167 = _336165, _336163 = _336161, _336159 = _336157, _336155 = _336153], (376 ^ _323094) ^ [_336814, _336816, _336818, _336820, _336822, _336824] : [-(f26(_336824, _336820, _336816) = f26(_336822, _336818, _336814)), _336824 = _336822, _336820 = _336818, _336816 = _336814], (390 ^ _323094) ^ [_337358, _337360, _337362, _337364, _337366, _337368, _337370, _337372] : [-(f28(_337372, _337368, _337364, _337360) = f28(_337370, _337366, _337362, _337358)), _337372 = _337370, _337368 = _337366, _337364 = _337362, _337360 = _337358], (408 ^ _323094) ^ [_338019, _338021, _338023, _338025, _338027, _338029] : [-(f29(_338029, _338025, _338021) = f29(_338027, _338023, _338019)), _338029 = _338027, _338025 = _338023, _338021 = _338019], (422 ^ _323094) ^ [_338507, _338509, _338511, _338513] : [-(c_2Ebool_2ETYPE__DEFINITION(_338513, _338509) = c_2Ebool_2ETYPE__DEFINITION(_338511, _338507)), _338513 = _338511, _338509 = _338507], (432 ^ _323094) ^ [_338866, _338868, _338870, _338872] : [-(f30(_338872, _338868) = f30(_338870, _338866)), _338872 = _338870, _338868 = _338866], (442 ^ _323094) ^ [_339253, _339255, _339257, _339259, _339261, _339263] : [-(f31(_339263, _339259, _339255) = f31(_339261, _339257, _339253)), _339263 = _339261, _339259 = _339257, _339255 = _339253], (456 ^ _323094) ^ [_339741, _339743, _339745, _339747] : [-(c_2Ebool_2EONE__ONE(_339747, _339743) = c_2Ebool_2EONE__ONE(_339745, _339741)), _339747 = _339745, _339743 = _339741], (466 ^ _323094) ^ [_340100, _340102, _340104, _340106] : [-(c_2Ebool_2EONTO(_340106, _340102) = c_2Ebool_2EONTO(_340104, _340100)), _340106 = _340104, _340102 = _340100], (476 ^ _323094) ^ [_340459, _340461, _340463, _340465] : [-(c_2Ebool_2Eliteral__case(_340465, _340461) = c_2Ebool_2Eliteral__case(_340463, _340459)), _340465 = _340463, _340461 = _340459], (486 ^ _323094) ^ [_340818, _340820, _340822, _340824] : [-(f14(_340824, _340820) = f14(_340822, _340818)), _340824 = _340822, _340820 = _340818], (496 ^ _323094) ^ [_341177, _341179, _341181, _341183] : [-(f32(_341183, _341179) = f32(_341181, _341177)), _341183 = _341181, _341179 = _341177], (506 ^ _323094) ^ [_341508, _341510] : [_341510 = _341508, -(f33(_341510) = f33(_341508))], (512 ^ _323094) ^ [_341726, _341728] : [_341728 = _341726, -(c_2Ebool_2E_21(_341728) = c_2Ebool_2E_21(_341726))], (518 ^ _323094) ^ [_342000, _342002, _342004, _342006, _342008, _342010] : [-(f34(_342010, _342006, _342002) = f34(_342008, _342004, _342000)), _342010 = _342008, _342006 = _342004, _342002 = _342000], (532 ^ _323094) ^ [_342488, _342490, _342492, _342494] : [-(f35(_342494, _342490) = f35(_342492, _342488)), _342494 = _342492, _342490 = _342488], (542 ^ _323094) ^ [_342819, _342821] : [_342821 = _342819, -(f36(_342821) = f36(_342819))], (548 ^ _323094) ^ [_343037, _343039] : [_343039 = _343037, -(c_2Ebool_2EIN(_343039) = c_2Ebool_2EIN(_343037))], (554 ^ _323094) ^ [_343255, _343257] : [_343257 = _343255, -(c_2Ebool_2E_3F(_343257) = c_2Ebool_2E_3F(_343255))], (560 ^ _323094) ^ [_343501, _343503, _343505, _343507] : [-(f38(_343507, _343503) = f38(_343505, _343501)), _343507 = _343505, _343503 = _343501], (570 ^ _323094) ^ [_343832, _343834] : [_343834 = _343832, -(f39(_343834) = f39(_343832))], (576 ^ _323094) ^ [_344050, _344052] : [_344052 = _344050, -(c_2Emin_2E_3D(_344052) = c_2Emin_2E_3D(_344050))], (582 ^ _323094) ^ [_344324, _344326, _344328, _344330, _344332, _344334] : [-(f41(_344334, _344330, _344326) = f41(_344332, _344328, _344324)), _344334 = _344332, _344330 = _344328, _344326 = _344324], (596 ^ _323094) ^ [_344784, _344786] : [_344786 = _344784, -(c_2Ebool_2ERES__EXISTS(_344786) = c_2Ebool_2ERES__EXISTS(_344784))], (602 ^ _323094) ^ [_345030, _345032, _345034, _345036] : [-(f40(_345036, _345032) = f40(_345034, _345030)), _345036 = _345034, _345032 = _345030], (612 ^ _323094) ^ [_345361, _345363] : [_345363 = _345361, -(c_2Ebool_2ERES__FORALL(_345363) = c_2Ebool_2ERES__FORALL(_345361))], (618 ^ _323094) ^ [_345635, _345637, _345639, _345641, _345643, _345645] : [-(f42(_345645, _345641, _345637) = f42(_345643, _345639, _345635)), _345645 = _345643, _345641 = _345639, _345637 = _345635], (632 ^ _323094) ^ [_346123, _346125, _346127, _346129] : [-(f43(_346129, _346125) = f43(_346127, _346123)), _346129 = _346127, _346125 = _346123], (642 ^ _323094) ^ [_346454, _346456] : [_346456 = _346454, -(c_2Ebool_2ERES__EXISTS__UNIQUE(_346456) = c_2Ebool_2ERES__EXISTS__UNIQUE(_346454))], (648 ^ _323094) ^ [_346672, _346674] : [_346674 = _346672, -(f44(_346674) = f44(_346672))], (654 ^ _323094) ^ [_346918, _346920, _346922, _346924] : [-(arr(_346924, _346920) = arr(_346922, _346918)), _346924 = _346922, _346920 = _346918], (664 ^ _323094) ^ [_347249, _347251] : [_347251 = _347249, -(c_2Emin_2E_40(_347251) = c_2Emin_2E_40(_347249))], (670 ^ _323094) ^ [_347523, _347525, _347527, _347529, _347531, _347533] : [-(f37(_347533, _347529, _347525) = f37(_347531, _347527, _347523)), _347533 = _347531, _347529 = _347527, _347525 = _347523], (684 ^ _323094) ^ [_348011, _348013, _348015, _348017] : [-(ap(_348017, _348013) = ap(_348015, _348011)), _348017 = _348015, _348013 = _348011], (694 ^ _323094) ^ [_348370, _348372, _348374, _348376] : [-(f45(_348376, _348372) = f45(_348374, _348370)), _348376 = _348374, _348372 = _348370], (704 ^ _323094) ^ [_348701, _348703] : [_348703 = _348701, -(c_2Ebool_2ERES__SELECT(_348703) = c_2Ebool_2ERES__SELECT(_348701))], (710 ^ _323094) ^ [_348919, _348921] : [_348921 = _348919, -(f46(_348921) = f46(_348919))], (716 ^ _323094) ^ [_349137, _349139] : [_349139 = _349137, -(c_2Ebool_2EDATATYPE(_349139) = c_2Ebool_2EDATATYPE(_349137))], (722 ^ _323094) ^ [_349363, _349365, _349367, _349369] : [-(k(_349369, _349365) = k(_349367, _349363)), _349369 = _349367, _349365 = _349363], (732 ^ _323094) ^ [] : [-(ne(bool))], (734 ^ _323094) ^ [] : [-(ne(ind))], (736 ^ _323094) ^ [_350198] : [ne(_350198), 739 ^ _323094 : [(740 ^ _323094) ^ [_350330] : [ne(_350330), -(ne(arr(_350198, _350330)))]]], (746 ^ _323094) ^ [_350563, _350565, _350567] : [mem(_350563, arr(_350567, _350565)), 749 ^ _323094 : [(750 ^ _323094) ^ [_350713] : [mem(_350713, _350567), -(mem(ap(_350563, _350713), _350565))]]], (756 ^ _323094) ^ [_350938] : [mem(_350938, bool), 759 ^ _323094 : [(760 ^ _323094) ^ [_351081] : [mem(_351081, bool), -(_350938 = _351081), 767 ^ _323094 : [(768 ^ _323094) ^ [] : [-(p(_350938))], (770 ^ _323094) ^ [] : [p(_351081)]], 771 ^ _323094 : [(772 ^ _323094) ^ [] : [-(p(_351081))], (774 ^ _323094) ^ [] : [p(_350938)]]]]], (778 ^ _323094) ^ [_351631, _351633, _351635] : [mem(_351631, arr(_351635, _351633)), 781 ^ _323094 : [(782 ^ _323094) ^ [_351804] : [mem(_351804, arr(_351635, _351633)), 788 ^ _323094 : [(789 ^ _323094) ^ [] : [-(mem(787 ^ [_351631, _351633, _351635, _351804], _351635))], (791 ^ _323094) ^ [] : [ap(_351631, 787 ^ [_351631, _351633, _351635, _351804]) = ap(_351804, 787 ^ [_351631, _351633, _351635, _351804])]], -(_351631 = _351804)]]], (795 ^ _323094) ^ [_352348, _352350, _352352] : [mem(_352348, _352352), -(ap(k(_352352, _352350), _352348) = _352350)], (801 ^ _323094) ^ [_352556, _352558] : [mem(_352556, _352558), -(ap(i(_352558), _352556) = _352556)], (807 ^ _323094) ^ [_352796] : [ne(_352796), -(mem(c_2Emin_2E_3D(_352796), arr(_352796, arr(_352796, bool))))], (813 ^ _323094) ^ [_353000] : [ne(_353000), 816 ^ _323094 : [(817 ^ _323094) ^ [_353155] : [mem(_353155, _353000), 820 ^ _323094 : [(821 ^ _323094) ^ [_353307] : [mem(_353307, _353000), 824 ^ _323094 : [(825 ^ _323094) ^ [] : [p(ap(ap(c_2Emin_2E_3D(_353000), _353155), _353307)), -(_353155 = _353307)], (831 ^ _323094) ^ [] : [_353155 = _353307, -(p(ap(ap(c_2Emin_2E_3D(_353000), _353155), _353307)))]]]]]]], (837 ^ _323094) ^ [] : [-(mem(c_2Emin_2E_3D_3D_3E, arr(bool, arr(bool, bool))))], (865 ^ _323094) ^ [_354605] : [ne(_354605), -(mem(c_2Emin_2E_40(_354605), arr(arr(_354605, bool), _354605)))], (839 ^ _323094) ^ [_353857] : [mem(_353857, bool), 842 ^ _323094 : [(843 ^ _323094) ^ [_354005] : [mem(_354005, bool), 846 ^ _323094 : [(857 ^ _323094) ^ [] : [858 ^ _323094 : [(859 ^ _323094) ^ [] : [-(p(_353857))], (861 ^ _323094) ^ [] : [p(_354005)]], -(p(ap(ap(c_2Emin_2E_3D_3D_3E, _353857), _354005)))], (847 ^ _323094) ^ [] : [p(ap(ap(c_2Emin_2E_3D_3D_3E, _353857), _354005)), p(_353857), -(p(_354005))]]]]], (871 ^ _323094) ^ [_354817] : [ne(_354817), -(ne(ty_2Ebool_2Eitself(_354817)))], (877 ^ _323094) ^ [_355007] : [ne(_355007), -(mem(c_2Ebool_2E_21(_355007), arr(arr(_355007, bool), bool)))], (883 ^ _323094) ^ [_355211] : [ne(_355211), 886 ^ _323094 : [(887 ^ _323094) ^ [_355368] : [mem(_355368, arr(_355211, bool)), 890 ^ _323094 : [(901 ^ _323094) ^ [] : [903 ^ _323094 : [(904 ^ _323094) ^ [] : [-(mem(902 ^ [_355211, _355368], _355211))], (906 ^ _323094) ^ [] : [p(ap(_355368, 902 ^ [_355211, _355368]))]], -(p(ap(c_2Ebool_2E_21(_355211), _355368)))], (891 ^ _323094) ^ [] : [p(ap(c_2Ebool_2E_21(_355211), _355368)), 894 ^ _323094 : [(895 ^ _323094) ^ [_355637] : [mem(_355637, _355211), -(p(ap(_355368, _355637)))]]]]]]], (910 ^ _323094) ^ [] : [-(mem(c_2Ebool_2E_2F_5C, arr(bool, arr(bool, bool))))], (912 ^ _323094) ^ [_356188] : [mem(_356188, bool), 915 ^ _323094 : [(916 ^ _323094) ^ [_356336] : [mem(_356336, bool), 919 ^ _323094 : [(920 ^ _323094) ^ [] : [p(ap(ap(c_2Ebool_2E_2F_5C, _356188), _356336)), 923 ^ _323094 : [(924 ^ _323094) ^ [] : [-(p(_356188))], (926 ^ _323094) ^ [] : [-(p(_356336))]]], (928 ^ _323094) ^ [] : [-(p(ap(ap(c_2Ebool_2E_2F_5C, _356188), _356336))), p(_356188), p(_356336)]]]]], (938 ^ _323094) ^ [_356956] : [ne(_356956), -(mem(c_2Ebool_2E_3F(_356956), arr(arr(_356956, bool), bool)))], (944 ^ _323094) ^ [_357160] : [ne(_357160), 947 ^ _323094 : [(948 ^ _323094) ^ [_357317] : [mem(_357317, arr(_357160, bool)), 951 ^ _323094 : [(952 ^ _323094) ^ [] : [p(ap(c_2Ebool_2E_3F(_357160), _357317)), 956 ^ _323094 : [(957 ^ _323094) ^ [] : [-(mem(955 ^ [_357160, _357317], _357160))], (959 ^ _323094) ^ [] : [-(p(ap(_357317, 955 ^ [_357160, _357317])))]]], (961 ^ _323094) ^ [] : [-(p(ap(c_2Ebool_2E_3F(_357160), _357317))), 962 ^ _323094 : [(963 ^ _323094) ^ [_357808] : [mem(_357808, _357160), p(ap(_357317, _357808))]]]]]]], (971 ^ _323094) ^ [_358084] : [ne(_358084), -(mem(c_2Ebool_2E_3F_21(_358084), arr(arr(_358084, bool), bool)))], (977 ^ _323094) ^ [_358288] : [ne(_358288), -(mem(c_2Ebool_2EARB(_358288), _358288))], (983 ^ _323094) ^ [] : [-(mem(c_2Ebool_2EBOUNDED, arr(bool, bool)))], (985 ^ _323094) ^ [_358533] : [ne(_358533), -(mem(c_2Ebool_2ECOND(_358533), arr(bool, arr(_358533, arr(_358533, _358533)))))], (991 ^ _323094) ^ [_358743] : [ne(_358743), -(mem(c_2Ebool_2EDATATYPE(_358743), arr(_358743, bool)))], (997 ^ _323094) ^ [] : [-(mem(c_2Ebool_2EF, bool))], (999 ^ _323094) ^ [] : [p(c_2Ebool_2EF)], (1001 ^ _323094) ^ [_359046] : [ne(_359046), -(mem(c_2Ebool_2EIN(_359046), arr(_359046, arr(arr(_359046, bool), bool))))], (1007 ^ _323094) ^ [_359256] : [ne(_359256), 1010 ^ _323094 : [(1011 ^ _323094) ^ [_359398] : [ne(_359398), -(mem(c_2Ebool_2ELET(_359256, _359398), arr(arr(_359256, _359398), arr(_359256, _359398))))]]], (1017 ^ _323094) ^ [_359623] : [ne(_359623), 1020 ^ _323094 : [(1021 ^ _323094) ^ [_359762] : [ne(_359762), -(mem(c_2Ebool_2EONE__ONE(_359623, _359762), arr(arr(_359623, _359762), bool)))]]], (1027 ^ _323094) ^ [_359981] : [ne(_359981), 1030 ^ _323094 : [(1031 ^ _323094) ^ [_360120] : [ne(_360120), -(mem(c_2Ebool_2EONTO(_359981, _360120), arr(arr(_359981, _360120), bool)))]]], (1037 ^ _323094) ^ [_360339] : [ne(_360339), 1040 ^ _323094 : [(1041 ^ _323094) ^ [_360487] : [ne(_360487), -(mem(c_2Ebool_2ERES__ABSTRACT(_360339, _360487), arr(arr(_360339, bool), arr(arr(_360339, _360487), arr(_360339, _360487)))))]]], (1047 ^ _323094) ^ [_360724] : [ne(_360724), -(mem(c_2Ebool_2ERES__EXISTS(_360724), arr(arr(_360724, bool), arr(arr(_360724, bool), bool))))], (1053 ^ _323094) ^ [_360940] : [ne(_360940), -(mem(c_2Ebool_2ERES__EXISTS__UNIQUE(_360940), arr(arr(_360940, bool), arr(arr(_360940, bool), bool))))], (1059 ^ _323094) ^ [_361156] : [ne(_361156), -(mem(c_2Ebool_2ERES__FORALL(_361156), arr(arr(_361156, bool), arr(arr(_361156, bool), bool))))], (1065 ^ _323094) ^ [_361372] : [ne(_361372), -(mem(c_2Ebool_2ERES__SELECT(_361372), arr(arr(_361372, bool), arr(arr(_361372, bool), _361372))))], (1071 ^ _323094) ^ [] : [-(mem(c_2Ebool_2ET, bool))], (1073 ^ _323094) ^ [] : [-(p(c_2Ebool_2ET))], (1075 ^ _323094) ^ [_361694] : [ne(_361694), 1078 ^ _323094 : [(1079 ^ _323094) ^ [_361839] : [ne(_361839), -(mem(c_2Ebool_2ETYPE__DEFINITION(_361694, _361839), arr(arr(_361694, bool), arr(arr(_361839, _361694), bool))))]]], (1085 ^ _323094) ^ [] : [-(mem(c_2Ebool_2E_5C_2F, arr(bool, arr(bool, bool))))], (1087 ^ _323094) ^ [_362123] : [mem(_362123, bool), 1090 ^ _323094 : [(1091 ^ _323094) ^ [_362271] : [mem(_362271, bool), 1094 ^ _323094 : [(1105 ^ _323094) ^ [] : [1106 ^ _323094 : [(1107 ^ _323094) ^ [] : [p(_362123)], (1109 ^ _323094) ^ [] : [p(_362271)]], -(p(ap(ap(c_2Ebool_2E_5C_2F, _362123), _362271)))], (1095 ^ _323094) ^ [] : [p(ap(ap(c_2Ebool_2E_5C_2F, _362123), _362271)), -(p(_362123)), -(p(_362271))]]]]], (1113 ^ _323094) ^ [_362891] : [ne(_362891), 1116 ^ _323094 : [(1117 ^ _323094) ^ [_363032] : [ne(_363032), -(mem(c_2Ebool_2Eitself__case(_362891, _363032), arr(ty_2Ebool_2Eitself(_362891), arr(_363032, _363032))))]]], (1123 ^ _323094) ^ [_363255] : [ne(_363255), 1126 ^ _323094 : [(1127 ^ _323094) ^ [_363397] : [ne(_363397), -(mem(c_2Ebool_2Eliteral__case(_363255, _363397), arr(arr(_363255, _363397), arr(_363255, _363397))))]]], (1133 ^ _323094) ^ [_363622] : [ne(_363622), -(mem(c_2Ebool_2Ethe__value(_363622), ty_2Ebool_2Eitself(_363622)))], (1139 ^ _323094) ^ [] : [-(mem(c_2Ebool_2E_7E, arr(bool, bool)))], (1141 ^ _323094) ^ [_363871] : [mem(_363871, bool), 1144 ^ _323094 : [(1145 ^ _323094) ^ [] : [p(ap(c_2Ebool_2E_7E, _363871)), p(_363871)], (1151 ^ _323094) ^ [] : [-(p(_363871)), -(p(ap(c_2Ebool_2E_7E, _363871)))]]], (1157 ^ _323094) ^ [] : [1158 ^ _323094 : [(1159 ^ _323094) ^ [] : [-(true___)], (1161 ^ _323094) ^ [] : [true___]], -(i(bool) = i(bool))], (1165 ^ _323094) ^ [] : [i(bool) = i(bool), true___, -(true___)], (1175 ^ _323094) ^ [_364676, _364678] : [-(ap(f1(_364678), _364676) = ap(ap(c_2Emin_2E_3D(arr(_364678, bool)), _364676), k(_364678, c_2Ebool_2ET)))], (1177 ^ _323094) ^ [_364790] : [ne(_364790), -(c_2Ebool_2E_21(_364790) = f1(_364790))], (1183 ^ _323094) ^ [_364985, _364987] : [-(ap(f2(_364987), _364985) = ap(_364985, ap(c_2Emin_2E_40(_364987), _364985)))], (1185 ^ _323094) ^ [_365093] : [ne(_365093), -(c_2Ebool_2E_3F(_365093) = f2(_365093))], (1191 ^ _323094) ^ [_365289] : [mem(_365289, bool), 1194 ^ _323094 : [(1195 ^ _323094) ^ [_365451] : [mem(_365451, bool), 1198 ^ _323094 : [(1199 ^ _323094) ^ [_365593] : [-(ap(f3(_365289, _365451), _365593) = ap(ap(c_2Emin_2E_3D_3D_3E, ap(ap(c_2Emin_2E_3D_3D_3E, _365451), ap(ap(c_2Emin_2E_3D_3D_3E, _365289), _365593))), _365593))]]]]], (1201 ^ _323094) ^ [_365724] : [mem(_365724, bool), 1204 ^ _323094 : [(1205 ^ _323094) ^ [_365847] : [-(ap(f4(_365724), _365847) = ap(c_2Ebool_2E_21(bool), f3(_365847, _365724)))]]], (1207 ^ _323094) ^ [_365943] : [-(ap(f5, _365943) = f4(_365943))], (1209 ^ _323094) ^ [] : [-(c_2Ebool_2E_2F_5C = f5)], (1211 ^ _323094) ^ [_366094] : [mem(_366094, bool), 1214 ^ _323094 : [(1215 ^ _323094) ^ [_366262] : [mem(_366262, bool), 1218 ^ _323094 : [(1219 ^ _323094) ^ [_366410] : [-(ap(f6(_366094, _366262), _366410) = ap(ap(c_2Emin_2E_3D_3D_3E, ap(ap(c_2Emin_2E_3D_3D_3E, _366094), _366410)), ap(ap(c_2Emin_2E_3D_3D_3E, ap(ap(c_2Emin_2E_3D_3D_3E, _366262), _366410)), _366410)))]]]]], (1221 ^ _323094) ^ [_366547] : [mem(_366547, bool), 1224 ^ _323094 : [(1225 ^ _323094) ^ [_366670] : [-(ap(f7(_366547), _366670) = ap(c_2Ebool_2E_21(bool), f6(_366547, _366670)))]]], (1227 ^ _323094) ^ [_366766] : [-(ap(f8, _366766) = f7(_366766))], (1229 ^ _323094) ^ [] : [-(c_2Ebool_2E_5C_2F = f8)], (1245 ^ _323094) ^ [] : [1247 ^ _323094 : [(1248 ^ _323094) ^ [] : [-(mem(1246 ^ [], bool))], (1250 ^ _323094) ^ [] : [p(1246 ^ [])]], 1251 ^ _323094 : [(1252 ^ _323094) ^ [] : [-(false___)], (1254 ^ _323094) ^ [] : [false___]]], (1231 ^ _323094) ^ [] : [false___, -(false___), 1238 ^ _323094 : [(1239 ^ _323094) ^ [_367075] : [mem(_367075, bool), -(p(_367075))]]], (1256 ^ _323094) ^ [_367509] : [-(ap(f9, _367509) = ap(ap(c_2Emin_2E_3D_3D_3E, _367509), c_2Ebool_2EF))], (1258 ^ _323094) ^ [] : [-(c_2Ebool_2E_7E = f9)], (1260 ^ _323094) ^ [_367678, _367680] : [mem(_367678, arr(_367680, bool)), 1263 ^ _323094 : [(1264 ^ _323094) ^ [_367859] : [mem(_367859, _367680), 1267 ^ _323094 : [(1268 ^ _323094) ^ [_368016] : [-(ap(f10(_367680, _367678, _367859), _368016) = ap(ap(c_2Emin_2E_3D_3D_3E, ap(ap(c_2Ebool_2E_2F_5C, ap(_367678, _367859)), ap(_367678, _368016))), ap(ap(c_2Emin_2E_3D(_367680), _367859), _368016)))]]]]], (1270 ^ _323094) ^ [_368172, _368174] : [mem(_368172, arr(_368174, bool)), 1273 ^ _323094 : [(1274 ^ _323094) ^ [_368309] : [-(ap(f11(_368174, _368172), _368309) = ap(c_2Ebool_2E_21(_368174), f10(_368174, _368172, _368309)))]]], (1276 ^ _323094) ^ [_368425, _368427] : [-(ap(f12(_368427), _368425) = ap(ap(c_2Ebool_2E_2F_5C, ap(c_2Ebool_2E_3F(_368427), _368425)), ap(c_2Ebool_2E_21(_368427), f11(_368427, _368425))))], (1278 ^ _323094) ^ [_368544] : [ne(_368544), -(c_2Ebool_2E_3F_21(_368544) = f12(_368544))], (1284 ^ _323094) ^ [_368768, _368770, _368772] : [mem(_368768, arr(_368770, _368772)), 1287 ^ _323094 : [(1288 ^ _323094) ^ [_368904] : [-(ap(f13(_368772, _368770, _368768), _368904) = ap(_368768, _368904))]]], (1290 ^ _323094) ^ [_369031, _369033, _369035] : [-(ap(f14(_369035, _369033), _369031) = f13(_369035, _369033, _369031))], (1292 ^ _323094) ^ [_369138] : [ne(_369138), 1295 ^ _323094 : [(1296 ^ _323094) ^ [_369274] : [ne(_369274), -(c_2Ebool_2ELET(_369138, _369274) = f14(_369274, _369138))]]], (1302 ^ _323094) ^ [_369501, _369503] : [mem(_369501, _369503), 1305 ^ _323094 : [(1306 ^ _323094) ^ [_369708] : [mem(_369708, _369503), 1309 ^ _323094 : [(1310 ^ _323094) ^ [_369912] : [mem(_369912, bool), 1313 ^ _323094 : [(1314 ^ _323094) ^ [_370096] : [-(ap(f15(_369503, _369501, _369708, _369912), _370096) = ap(ap(c_2Ebool_2E_2F_5C, ap(ap(c_2Emin_2E_3D_3D_3E, ap(ap(c_2Emin_2E_3D(bool), _369912), c_2Ebool_2ET)), ap(ap(c_2Emin_2E_3D(_369503), _370096), _369501))), ap(ap(c_2Emin_2E_3D_3D_3E, ap(ap(c_2Emin_2E_3D(bool), _369912), c_2Ebool_2EF)), ap(ap(c_2Emin_2E_3D(_369503), _370096), _369708))))]]]]]]], (1316 ^ _323094) ^ [_370280, _370282] : [mem(_370280, bool), 1319 ^ _323094 : [(1320 ^ _323094) ^ [_370439] : [mem(_370439, _370282), 1323 ^ _323094 : [(1324 ^ _323094) ^ [_370580] : [-(ap(f16(_370282, _370280, _370439), _370580) = ap(c_2Emin_2E_40(_370282), f15(_370282, _370439, _370580, _370280)))]]]]], (1326 ^ _323094) ^ [_370720, _370722] : [mem(_370720, bool), 1329 ^ _323094 : [(1330 ^ _323094) ^ [_370846] : [-(ap(f17(_370722, _370720), _370846) = f16(_370722, _370720, _370846))]]], (1332 ^ _323094) ^ [_370957, _370959] : [-(ap(f18(_370959), _370957) = f17(_370959, _370957))], (1334 ^ _323094) ^ [_371060] : [ne(_371060), -(c_2Ebool_2ECOND(_371060) = f18(_371060))], (1340 ^ _323094) ^ [_371284, _371286, _371288] : [mem(_371284, arr(_371286, _371288)), 1343 ^ _323094 : [(1344 ^ _323094) ^ [_371472] : [mem(_371472, _371286), 1347 ^ _323094 : [(1348 ^ _323094) ^ [_371638] : [-(ap(f19(_371288, _371286, _371284, _371472), _371638) = ap(ap(c_2Emin_2E_3D_3D_3E, ap(ap(c_2Emin_2E_3D(_371288), ap(_371284, _371472)), ap(_371284, _371638))), ap(ap(c_2Emin_2E_3D(_371286), _371472), _371638)))]]]]], (1350 ^ _323094) ^ [_371813, _371815, _371817] : [mem(_371813, arr(_371815, _371817)), 1353 ^ _323094 : [(1354 ^ _323094) ^ [_371956] : [-(ap(f20(_371817, _371815, _371813), _371956) = ap(c_2Ebool_2E_21(_371815), f19(_371817, _371815, _371813, _371956)))]]], (1356 ^ _323094) ^ [_372090, _372092, _372094] : [-(ap(f21(_372094, _372092), _372090) = ap(c_2Ebool_2E_21(_372092), f20(_372094, _372092, _372090)))], (1358 ^ _323094) ^ [_372202] : [ne(_372202), 1361 ^ _323094 : [(1362 ^ _323094) ^ [_372338] : [ne(_372338), -(c_2Ebool_2EONE__ONE(_372202, _372338) = f21(_372338, _372202))]]], (1368 ^ _323094) ^ [_372579, _372581, _372583] : [mem(_372579, arr(_372581, _372583)), 1371 ^ _323094 : [(1372 ^ _323094) ^ [_372750] : [mem(_372750, _372583), 1375 ^ _323094 : [(1376 ^ _323094) ^ [_372899] : [-(ap(f22(_372583, _372581, _372579, _372750), _372899) = ap(ap(c_2Emin_2E_3D(_372583), _372750), ap(_372579, _372899)))]]]]], (1378 ^ _323094) ^ [_373057, _373059, _373061] : [mem(_373057, arr(_373061, _373059)), 1381 ^ _323094 : [(1382 ^ _323094) ^ [_373200] : [-(ap(f23(_373061, _373059, _373057), _373200) = ap(c_2Ebool_2E_3F(_373061), f22(_373059, _373061, _373057, _373200)))]]], (1384 ^ _323094) ^ [_373334, _373336, _373338] : [-(ap(f24(_373338, _373336), _373334) = ap(c_2Ebool_2E_21(_373336), f23(_373338, _373336, _373334)))], (1386 ^ _323094) ^ [_373446] : [ne(_373446), 1389 ^ _323094 : [(1390 ^ _323094) ^ [_373582] : [ne(_373582), -(c_2Ebool_2EONTO(_373446, _373582) = f24(_373446, _373582))]]], (1396 ^ _323094) ^ [_373823, _373825, _373827] : [mem(_373823, arr(_373825, _373827)), 1399 ^ _323094 : [(1400 ^ _323094) ^ [_374011] : [mem(_374011, _373825), 1403 ^ _323094 : [(1404 ^ _323094) ^ [_374177] : [-(ap(f25(_373827, _373825, _373823, _374011), _374177) = ap(ap(c_2Emin_2E_3D_3D_3E, ap(ap(c_2Emin_2E_3D(_373827), ap(_373823, _374011)), ap(_373823, _374177))), ap(ap(c_2Emin_2E_3D(_373825), _374011), _374177)))]]]]], (1406 ^ _323094) ^ [_374352, _374354, _374356] : [mem(_374352, arr(_374354, _374356)), 1409 ^ _323094 : [(1410 ^ _323094) ^ [_374495] : [-(ap(f26(_374356, _374354, _374352), _374495) = ap(c_2Ebool_2E_21(_374354), f25(_374356, _374354, _374352, _374495)))]]], (1412 ^ _323094) ^ [_374644, _374646, _374648] : [mem(_374644, arr(_374646, _374648)), 1415 ^ _323094 : [(1416 ^ _323094) ^ [_374815] : [mem(_374815, _374648), 1419 ^ _323094 : [(1420 ^ _323094) ^ [_374964] : [-(ap(f27(_374648, _374646, _374644, _374815), _374964) = ap(ap(c_2Emin_2E_3D(_374648), _374815), ap(_374644, _374964)))]]]]], (1422 ^ _323094) ^ [_375122, _375124, _375126] : [mem(_375122, arr(_375124, bool)), 1425 ^ _323094 : [(1426 ^ _323094) ^ [_375304] : [mem(_375304, arr(_375126, _375124)), 1429 ^ _323094 : [(1430 ^ _323094) ^ [_375467] : [-(ap(f28(_375126, _375124, _375122, _375304), _375467) = ap(ap(c_2Emin_2E_3D(bool), ap(_375122, _375467)), ap(c_2Ebool_2E_3F(_375126), f27(_375124, _375126, _375304, _375467))))]]]]], (1432 ^ _323094) ^ [_375633, _375635, _375637] : [mem(_375633, arr(_375635, bool)), 1435 ^ _323094 : [(1436 ^ _323094) ^ [_375791] : [-(ap(f29(_375637, _375635, _375633), _375791) = ap(ap(c_2Ebool_2E_2F_5C, ap(c_2Ebool_2E_21(_375637), f26(_375635, _375637, _375791))), ap(c_2Ebool_2E_21(_375635), f28(_375637, _375635, _375633, _375791))))]]], (1438 ^ _323094) ^ [_375940, _375942, _375944] : [-(ap(f30(_375944, _375942), _375940) = f29(_375944, _375942, _375940))], (1440 ^ _323094) ^ [_376047] : [ne(_376047), 1443 ^ _323094 : [(1444 ^ _323094) ^ [_376183] : [ne(_376183), -(c_2Ebool_2ETYPE__DEFINITION(_376047, _376183) = f30(_376183, _376047))]]], (1450 ^ _323094) ^ [_376396] : [mem(_376396, bool), 1455 ^ _323094 : [(1466 ^ _323094) ^ [] : [1467 ^ _323094 : [(1468 ^ _323094) ^ [] : [-(true___)], (1470 ^ _323094) ^ [] : [true___]], -(p(_376396))], (1456 ^ _323094) ^ [] : [p(_376396), true___, -(true___)]], 1473 ^ _323094 : [(1474 ^ _323094) ^ [] : [p(_376396), 1477 ^ _323094 : [(1478 ^ _323094) ^ [] : [-(false___)], (1480 ^ _323094) ^ [] : [false___]]], (1482 ^ _323094) ^ [] : [-(p(_376396)), false___, -(false___)]]], (1492 ^ _323094) ^ [_377436, _377438, _377440] : [mem(_377436, arr(_377438, _377440)), 1495 ^ _323094 : [(1496 ^ _323094) ^ [_377572] : [-(ap(f31(_377440, _377438, _377436), _377572) = ap(_377436, _377572))]]], (1498 ^ _323094) ^ [_377686] : [ne(_377686), 1501 ^ _323094 : [(1502 ^ _323094) ^ [_377834] : [ne(_377834), 1505 ^ _323094 : [(1506 ^ _323094) ^ [_377978] : [mem(_377978, arr(_377686, _377834)), -(f31(_377834, _377686, _377978) = _377978)]]]]], (1512 ^ _323094) ^ [_378208] : [ne(_378208), 1515 ^ _323094 : [(1516 ^ _323094) ^ [_378368] : [mem(_378368, arr(_378208, bool)), 1519 ^ _323094 : [(1520 ^ _323094) ^ [_378528] : [mem(_378528, _378208), p(ap(_378368, _378528)), -(p(ap(_378368, ap(c_2Emin_2E_40(_378208), _378368))))]]]]], (1531 ^ _323094) ^ [] : [-(mem(1529 ^ [], arr(ind, ind)))], (1533 ^ _323094) ^ [] : [-(p(ap(c_2Ebool_2EONE__ONE(ind, ind), 1529 ^ [])))], (1535 ^ _323094) ^ [] : [p(ap(c_2Ebool_2EONTO(ind, ind), 1529 ^ []))], (1537 ^ _323094) ^ [_379072] : [ne(_379072), 1540 ^ _323094 : [(1541 ^ _323094) ^ [_379208] : [ne(_379208), -(c_2Ebool_2Eliteral__case(_379072, _379208) = f14(_379208, _379072))]]], (1547 ^ _323094) ^ [_379435, _379437] : [mem(_379435, _379437), 1550 ^ _323094 : [(1551 ^ _323094) ^ [_379560] : [-(ap(f32(_379437, _379435), _379560) = ap(_379560, _379435))]]], (1553 ^ _323094) ^ [_379670, _379672] : [-(ap(f33(_379672), _379670) = f32(_379672, _379670))], (1555 ^ _323094) ^ [_379773] : [ne(_379773), -(c_2Ebool_2EIN(_379773) = f33(_379773))], (1561 ^ _323094) ^ [_379983, _379985] : [mem(_379983, arr(_379985, bool)), 1564 ^ _323094 : [(1565 ^ _323094) ^ [_380158] : [mem(_380158, arr(_379985, bool)), 1568 ^ _323094 : [(1569 ^ _323094) ^ [_380312] : [-(ap(f34(_379985, _379983, _380158), _380312) = ap(ap(c_2Emin_2E_3D_3D_3E, ap(ap(c_2Ebool_2EIN(_379985), _380312), _379983)), ap(_380158, _380312)))]]]]], (1571 ^ _323094) ^ [_380459, _380461] : [mem(_380459, arr(_380461, bool)), 1574 ^ _323094 : [(1575 ^ _323094) ^ [_380596] : [-(ap(f35(_380461, _380459), _380596) = ap(c_2Ebool_2E_21(_380461), f34(_380461, _380459, _380596)))]]], (1577 ^ _323094) ^ [_380712, _380714] : [-(ap(f36(_380714), _380712) = f35(_380714, _380712))], (1579 ^ _323094) ^ [_380815] : [ne(_380815), -(c_2Ebool_2ERES__FORALL(_380815) = f36(_380815))], (1585 ^ _323094) ^ [_381025, _381027] : [mem(_381025, arr(_381027, bool)), 1588 ^ _323094 : [(1589 ^ _323094) ^ [_381200] : [mem(_381200, arr(_381027, bool)), 1592 ^ _323094 : [(1593 ^ _323094) ^ [_381354] : [-(ap(f37(_381027, _381025, _381200), _381354) = ap(ap(c_2Ebool_2E_2F_5C, ap(ap(c_2Ebool_2EIN(_381027), _381354), _381025)), ap(_381200, _381354)))]]]]], (1595 ^ _323094) ^ [_381501, _381503] : [mem(_381501, arr(_381503, bool)), 1598 ^ _323094 : [(1599 ^ _323094) ^ [_381638] : [-(ap(f38(_381503, _381501), _381638) = ap(c_2Ebool_2E_3F(_381503), f37(_381503, _381501, _381638)))]]], (1601 ^ _323094) ^ [_381754, _381756] : [-(ap(f39(_381756), _381754) = f38(_381756, _381754))], (1603 ^ _323094) ^ [_381857] : [ne(_381857), -(c_2Ebool_2ERES__EXISTS(_381857) = f39(_381857))], (1609 ^ _323094) ^ [_382067, _382069] : [mem(_382067, arr(_382069, bool)), 1612 ^ _323094 : [(1613 ^ _323094) ^ [_382198] : [-(ap(f40(_382069, _382067), _382198) = ap(_382067, _382198))]]], (1615 ^ _323094) ^ [_382323, _382325] : [mem(_382323, arr(_382325, bool)), 1618 ^ _323094 : [(1619 ^ _323094) ^ [_382504] : [mem(_382504, _382325), 1622 ^ _323094 : [(1623 ^ _323094) ^ [_382661] : [-(ap(f41(_382325, _382323, _382504), _382661) = ap(ap(c_2Emin_2E_3D_3D_3E, ap(ap(c_2Ebool_2E_2F_5C, ap(_382323, _382504)), ap(_382323, _382661))), ap(ap(c_2Emin_2E_3D(_382325), _382504), _382661)))]]]]], (1625 ^ _323094) ^ [_382817, _382819] : [mem(_382817, arr(_382819, bool)), 1628 ^ _323094 : [(1629 ^ _323094) ^ [_382987] : [mem(_382987, arr(_382819, bool)), 1632 ^ _323094 : [(1633 ^ _323094) ^ [_383136] : [-(ap(f42(_382819, _382817, _382987), _383136) = ap(ap(c_2Ebool_2ERES__FORALL(_382819), _382987), f41(_382819, _382817, _383136)))]]]]], (1635 ^ _323094) ^ [_383278, _383280] : [mem(_383278, arr(_383280, bool)), 1638 ^ _323094 : [(1639 ^ _323094) ^ [_383435] : [-(ap(f43(_383280, _383278), _383435) = ap(ap(c_2Ebool_2E_2F_5C, ap(ap(c_2Ebool_2ERES__EXISTS(_383280), _383278), f40(_383280, _383435))), ap(ap(c_2Ebool_2ERES__FORALL(_383280), _383278), f42(_383280, _383435, _383278))))]]], (1641 ^ _323094) ^ [_383571, _383573] : [-(ap(f44(_383573), _383571) = f43(_383573, _383571))], (1643 ^ _323094) ^ [_383674] : [ne(_383674), -(c_2Ebool_2ERES__EXISTS__UNIQUE(_383674) = f44(_383674))], (1649 ^ _323094) ^ [_383884, _383886] : [mem(_383884, arr(_383886, bool)), 1652 ^ _323094 : [(1653 ^ _323094) ^ [_384021] : [-(ap(f45(_383886, _383884), _384021) = ap(c_2Emin_2E_40(_383886), f37(_383886, _383884, _384021)))]]], (1655 ^ _323094) ^ [_384137, _384139] : [-(ap(f46(_384139), _384137) = f45(_384139, _384137))], (1657 ^ _323094) ^ [_384240] : [ne(_384240), -(c_2Ebool_2ERES__SELECT(_384240) = f46(_384240))], (1663 ^ _323094) ^ [] : [-(c_2Ebool_2EBOUNDED = k(bool, c_2Ebool_2ET))], (1665 ^ _323094) ^ [_384469] : [ne(_384469), -(c_2Ebool_2EDATATYPE(_384469) = k(_384469, c_2Ebool_2ET))]], input).
% 0.36/1.37 ncf('1',plain,[true___],start(1673 ^ 0)).
% 0.36/1.37 ncf('1.1',plain,[-(true___)],extension(1671 ^ 1)).
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------