%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET751+4 : TPTP v8.1.2. Bugfixed v2.2.1.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n004.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:56:22 EDT 2023
% Result : Theorem 83.62s 81.11s
% Output : Proof 83.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SET751+4 : TPTP v8.1.2. Bugfixed v2.2.1.
% 0.07/0.14 % Command : nanocop.sh %s %d
% 0.14/0.35 % Computer : n004.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 18 18:44:54 EDT 2023
% 0.14/0.35 % CPUTime :
% 83.62/81.11
% 83.62/81.11 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 83.62/81.11 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 83.62/81.11 %-----------------------------------------------------
% 83.62/81.11 ncf(matrix, plain, [(1315 ^ _252839) ^ [] : [-(maps(1309 ^ [], 1310 ^ [], 1311 ^ []))], (1319 ^ _252839) ^ [] : [-(subset(1313 ^ [], 1310 ^ []))], (1323 ^ _252839) ^ [] : [subset(image2(1309 ^ [], 1312 ^ []), image2(1309 ^ [], 1313 ^ []))], (1321 ^ _252839) ^ [] : [-(subset(1312 ^ [], 1313 ^ []))], (1317 ^ _252839) ^ [] : [-(subset(1312 ^ [], 1310 ^ []))], !, (1112 ^ _200130) ^ [_242838, _242840, _242842, _242844, _242846] : [increasing(_242846, _242844, _242842, _242840, _242838), 1115 ^ _200130 : [(1116 ^ _200130) ^ [_243090, _243092, _243094, _243096] : [-(apply(_242838, _243094, _243090)), member(_243096, _242844), member(_243094, _242840), member(_243092, _242844), member(_243090, _242840), apply(_242842, _243096, _243092), apply(_242846, _243096, _243094), apply(_242846, _243092, _243090)]]], (1054 ^ _200130) ^ [_240530, _240532, _240534, _240536] : [-(member(_240530, image3(_240536, _240534, _240532))), member(_240530, _240532), 1059 ^ _200130 : [(1060 ^ _200130) ^ [_240724] : [member(_240724, _240534), apply(_240536, _240724, _240530)]]], (466 ^ _200130) ^ [_217037, _217039] : [subset(_217039, _217037), 469 ^ _200130 : [(470 ^ _200130) ^ [_217174] : [member(_217174, _217039), -(member(_217174, _217037))]]], (543 ^ _200130) ^ [_219608, _219610, _219612] : [544 ^ _200130 : [(547 ^ _200130) ^ [] : [member(_219612, _219608)], (545 ^ _200130) ^ [] : [member(_219612, _219610)]], -(member(_219612, union(_219610, _219608)))], (950 ^ _200130) ^ [_236507, _236509, _236511] : [-(one_to_one(_236511, _236509, _236507)), injective(_236511, _236509, _236507), surjective(_236511, _236509, _236507)], (1098 ^ _200130) ^ [_242271, _242273, _242275, _242277] : [-(member(_242271, inverse_image3(_242277, _242275, _242273))), member(_242271, _242273), 1103 ^ _200130 : [(1104 ^ _200130) ^ [_242465] : [member(_242465, _242275), apply(_242277, _242271, _242465)]]], (4 ^ _200130) ^ [_200361, _200363] : [_200363 = _200361, -(_200361 = _200363)], (639 ^ _200130) ^ [_223099, _223101, _223103] : [maps(_223103, _223101, _223099), 642 ^ _200130 : [(652 ^ _200130) ^ [_223717, _223719, _223721] : [member(_223721, _223101), member(_223719, _223099), member(_223717, _223099), -(_223719 = _223717), apply(_223103, _223721, _223719), apply(_223103, _223721, _223717)], (643 ^ _200130) ^ [_223327] : [member(_223327, _223101), 647 ^ _200130 : [(650 ^ _200130) ^ [] : [-(apply(_223103, _223327, 646 ^ [_223099, _223101, _223103, _223327]))], (648 ^ _200130) ^ [] : [-(member(646 ^ [_223099, _223101, _223103, _223327], _223099))]]]]], (561 ^ _200130) ^ [_220280, _220282, _220284] : [-(member(_220284, difference(_220280, _220282))), member(_220284, _220280), -(member(_220284, _220282))], (485 ^ _200130) ^ [_217737, _217739] : [equal_set(_217739, _217737), 488 ^ _200130 : [(491 ^ _200130) ^ [] : [-(subset(_217737, _217739))], (489 ^ _200130) ^ [] : [-(subset(_217739, _217737))]]], (571 ^ _200130) ^ [_220629, _220631] : [member(_220631, singleton(_220629)), -(_220631 = _220629)], (593 ^ _200130) ^ [_221322, _221324, _221326] : [594 ^ _200130 : [(597 ^ _200130) ^ [] : [_221326 = _221322], (595 ^ _200130) ^ [] : [_221326 = _221324]], -(member(_221326, unordered_pair(_221324, _221322)))], (236 ^ _200130) ^ [_208781, _208783, _208785, _208787, _208789, _208791] : [-(one_to_one(_208789, _208785, _208781)), one_to_one(_208791, _208787, _208783), _208791 = _208789, _208787 = _208785, _208783 = _208781], (210 ^ _200130) ^ [_207850, _207852, _207854, _207856, _207858, _207860, _207862, _207864, _207866, _207868] : [-(isomorphism(_207866, _207862, _207858, _207854, _207850)), isomorphism(_207868, _207864, _207860, _207856, _207852), _207868 = _207866, _207864 = _207862, _207860 = _207858, _207856 = _207854, _207852 = _207850], (2 ^ _200130) ^ [_200254] : [-(_200254 = _200254)], (942 ^ _200130) ^ [_236256, _236258, _236260] : [one_to_one(_236260, _236258, _236256), 945 ^ _200130 : [(948 ^ _200130) ^ [] : [-(surjective(_236260, _236258, _236256))], (946 ^ _200130) ^ [] : [-(injective(_236260, _236258, _236256))]]], (376 ^ _200130) ^ [_213588, _213590] : [_213590 = _213588, -(product(_213590) = product(_213588))], (100 ^ _200130) ^ [_203812, _203814, _203816, _203818, _203820, _203822] : [-(injective(_203820, _203816, _203812)), injective(_203822, _203818, _203814), _203822 = _203820, _203818 = _203816, _203814 = _203812], (1033 ^ _200130) ^ [_239660, _239662, _239664] : [-(member(_239660, image2(_239664, _239662))), 1034 ^ _200130 : [(1035 ^ _200130) ^ [_239758] : [member(_239758, _239662), apply(_239664, _239758, _239660)]]], (10 ^ _200130) ^ [_200565, _200567, _200569] : [-(_200569 = _200565), _200569 = _200567, _200567 = _200565], (807 ^ _200130) ^ [_230498, _230500, _230502, _230504] : [equal_maps(_230504, _230502, _230500, _230498), 810 ^ _200130 : [(811 ^ _200130) ^ [_230711, _230713, _230715] : [member(_230715, _230500), member(_230713, _230498), member(_230711, _230498), -(_230713 = _230711), apply(_230504, _230715, _230713), apply(_230502, _230715, _230711)]]], (1228 ^ _200130) ^ [_248660, _248662, _248664, _248666, _248668] : [isomorphism(_248668, _248666, _248664, _248662, _248660), 1231 ^ _200130 : [(1236 ^ _200130) ^ [_249072, _249074, _249076, _249078] : [1259 ^ _200130 : [(1266 ^ _200130) ^ [] : [apply(_248660, _249076, _249072), -(apply(_248664, _249078, _249074))], (1260 ^ _200130) ^ [] : [apply(_248664, _249078, _249074), -(apply(_248660, _249076, _249072))]], member(_249078, _248666), member(_249076, _248662), member(_249074, _248666), member(_249072, _248662), apply(_248668, _249078, _249076), apply(_248668, _249074, _249072)], (1234 ^ _200130) ^ [] : [-(one_to_one(_248668, _248666, _248662))], (1232 ^ _200130) ^ [] : [-(maps(_248668, _248666, _248662))]]], (354 ^ _200130) ^ [_212793, _212795] : [_212795 = _212793, -(singleton(_212795) = singleton(_212793))], (304 ^ _200130) ^ [_211004, _211006, _211008, _211010] : [-(subset(_211008, _211004)), subset(_211010, _211006), _211010 = _211008, _211006 = _211004], (533 ^ _200130) ^ [_219340, _219342, _219344] : [member(_219344, union(_219342, _219340)), -(member(_219344, _219342)), -(member(_219344, _219340))], (360 ^ _200130) ^ [_213039, _213041, _213043, _213045] : [-(unordered_pair(_213045, _213041) = unordered_pair(_213043, _213039)), _213045 = _213043, _213041 = _213039], (1004 ^ _200130) ^ [_238656, _238658, _238660, _238662, _238664] : [member(_238658, _238662), member(_238656, _238660), 1011 ^ _200130 : [(1018 ^ _200130) ^ [] : [apply(inverse_function(_238664, _238662, _238660), _238656, _238658), -(apply(_238664, _238658, _238656))], (1012 ^ _200130) ^ [] : [apply(_238664, _238658, _238656), -(apply(inverse_function(_238664, _238662, _238660), _238656, _238658))]]], (704 ^ _200130) ^ [_225904, _225906, _225908, _225910, _225912, _225914] : [compose_predicate(_225914, _225912, _225910, _225908, _225906, _225904), 707 ^ _200130 : [(708 ^ _200130) ^ [_226116, _226118] : [member(_226118, _225908), member(_226116, _225904), 715 ^ _200130 : [(727 ^ _200130) ^ [] : [-(apply(_225914, _226118, _226116)), 728 ^ _200130 : [(729 ^ _200130) ^ [_226961] : [member(_226961, _225906), apply(_225910, _226118, _226961), apply(_225912, _226961, _226116)]]], (716 ^ _200130) ^ [] : [apply(_225914, _226118, _226116), 720 ^ _200130 : [(725 ^ _200130) ^ [] : [-(apply(_225912, 719 ^ [_225904, _225906, _225908, _225910, _225912, _225914, _226116, _226118], _226116))], (723 ^ _200130) ^ [] : [-(apply(_225910, _226118, 719 ^ [_225904, _225906, _225908, _225910, _225912, _225914, _226116, _226118]))], (721 ^ _200130) ^ [] : [-(member(719 ^ [_225904, _225906, _225908, _225910, _225912, _225914, _226116, _226118], _225906))]]]]]]], (620 ^ _200130) ^ [_222339, _222341] : [member(_222341, product(_222339)), 623 ^ _200130 : [(624 ^ _200130) ^ [_222480] : [member(_222480, _222339), -(member(_222341, _222480))]]], (503 ^ _200130) ^ [_218304, _218306] : [member(_218306, power_set(_218304)), -(subset(_218306, _218304))], (1204 ^ _200130) ^ [_246940, _246942, _246944, _246946, _246948] : [1209 ^ _200130 : [(1214 ^ _200130) ^ [] : [-(member(1207 ^ [_246940, _246942, _246944, _246946, _246948], _246946))], (1220 ^ _200130) ^ [] : [-(apply(_246948, 1205 ^ [_246940, _246942, _246944, _246946, _246948], 1206 ^ [_246940, _246942, _246944, _246946, _246948]))], (1210 ^ _200130) ^ [] : [-(member(1205 ^ [_246940, _246942, _246944, _246946, _246948], _246946))], (1222 ^ _200130) ^ [] : [-(apply(_246948, 1207 ^ [_246940, _246942, _246944, _246946, _246948], 1208 ^ [_246940, _246942, _246944, _246946, _246948]))], (1216 ^ _200130) ^ [] : [-(member(1208 ^ [_246940, _246942, _246944, _246946, _246948], _246942))], (1218 ^ _200130) ^ [] : [-(apply(_246944, 1205 ^ [_246940, _246942, _246944, _246946, _246948], 1207 ^ [_246940, _246942, _246944, _246946, _246948]))], (1224 ^ _200130) ^ [] : [apply(_246940, 1208 ^ [_246940, _246942, _246944, _246946, _246948], 1206 ^ [_246940, _246942, _246944, _246946, _246948])], (1212 ^ _200130) ^ [] : [-(member(1206 ^ [_246940, _246942, _246944, _246946, _246948], _246942))]], -(decreasing(_246948, _246946, _246944, _246942, _246940))], (509 ^ _200130) ^ [_218470, _218472] : [subset(_218472, _218470), -(member(_218472, power_set(_218470)))], (833 ^ _200130) ^ [_231360, _231362, _231364, _231366] : [837 ^ _200130 : [(840 ^ _200130) ^ [] : [-(member(835 ^ [_231360, _231362, _231364, _231366], _231360))], (838 ^ _200130) ^ [] : [-(member(834 ^ [_231360, _231362, _231364, _231366], _231362))], (848 ^ _200130) ^ [] : [835 ^ [_231360, _231362, _231364, _231366] = 836 ^ [_231360, _231362, _231364, _231366]], (844 ^ _200130) ^ [] : [-(apply(_231366, 834 ^ [_231360, _231362, _231364, _231366], 835 ^ [_231360, _231362, _231364, _231366]))], (846 ^ _200130) ^ [] : [-(apply(_231364, 834 ^ [_231360, _231362, _231364, _231366], 836 ^ [_231360, _231362, _231364, _231366]))], (842 ^ _200130) ^ [] : [-(member(836 ^ [_231360, _231362, _231364, _231366], _231360))]], -(equal_maps(_231366, _231364, _231362, _231360))], (136 ^ _200130) ^ [_205058, _205060, _205062, _205064, _205066, _205068, _205070, _205072] : [-(inverse_predicate(_205070, _205066, _205062, _205058)), inverse_predicate(_205072, _205068, _205064, _205060), _205072 = _205070, _205068 = _205066, _205064 = _205062, _205060 = _205058], (862 ^ _200130) ^ [_232818, _232820] : [864 ^ _200130 : [(867 ^ _200130) ^ [] : [apply(_232820, 863 ^ [_232818, _232820], 863 ^ [_232818, _232820])], (865 ^ _200130) ^ [] : [-(member(863 ^ [_232818, _232820], _232818))]], -(identity(_232820, _232818))], (1272 ^ _200130) ^ [_250210, _250212, _250214, _250216, _250218] : [-(isomorphism(_250218, _250216, _250214, _250212, _250210)), maps(_250218, _250216, _250212), one_to_one(_250218, _250216, _250212), 1285 ^ _200130 : [(1290 ^ _200130) ^ [] : [-(member(1283 ^ [_250210, _250212, _250214, _250216, _250218], _250216))], (1296 ^ _200130) ^ [] : [-(apply(_250218, 1283 ^ [_250210, _250212, _250214, _250216, _250218], 1284 ^ [_250210, _250212, _250214, _250216, _250218]))], (1298 ^ _200130) ^ [] : [1299 ^ _200130 : [(1302 ^ _200130) ^ [] : [apply(_250210, 1282 ^ [_250210, _250212, _250214, _250216, _250218], 1284 ^ [_250210, _250212, _250214, _250216, _250218])], (1300 ^ _200130) ^ [] : [-(apply(_250214, 1281 ^ [_250210, _250212, _250214, _250216, _250218], 1283 ^ [_250210, _250212, _250214, _250216, _250218]))]], 1303 ^ _200130 : [(1306 ^ _200130) ^ [] : [apply(_250214, 1281 ^ [_250210, _250212, _250214, _250216, _250218], 1283 ^ [_250210, _250212, _250214, _250216, _250218])], (1304 ^ _200130) ^ [] : [-(apply(_250210, 1282 ^ [_250210, _250212, _250214, _250216, _250218], 1284 ^ [_250210, _250212, _250214, _250216, _250218]))]]], (1292 ^ _200130) ^ [] : [-(member(1284 ^ [_250210, _250212, _250214, _250216, _250218], _250212))], (1286 ^ _200130) ^ [] : [-(member(1281 ^ [_250210, _250212, _250214, _250216, _250218], _250216))], (1288 ^ _200130) ^ [] : [-(member(1282 ^ [_250210, _250212, _250214, _250216, _250218], _250212))], (1294 ^ _200130) ^ [] : [-(apply(_250218, 1281 ^ [_250210, _250212, _250214, _250216, _250218], 1282 ^ [_250210, _250212, _250214, _250216, _250218]))]]], (476 ^ _200130) ^ [_217351, _217353] : [478 ^ _200130 : [(481 ^ _200130) ^ [] : [member(477 ^ [_217351, _217353], _217351)], (479 ^ _200130) ^ [] : [-(member(477 ^ [_217351, _217353], _217353))]], -(subset(_217353, _217351))], (158 ^ _200130) ^ [_205876, _205878, _205880, _205882, _205884, _205886, _205888, _205890, _205892, _205894] : [-(increasing(_205892, _205888, _205884, _205880, _205876)), increasing(_205894, _205890, _205886, _205882, _205878), _205894 = _205892, _205890 = _205888, _205886 = _205884, _205882 = _205880, _205878 = _205876], (515 ^ _200130) ^ [_218729, _218731, _218733] : [member(_218733, intersection(_218731, _218729)), 518 ^ _200130 : [(521 ^ _200130) ^ [] : [-(member(_218733, _218729))], (519 ^ _200130) ^ [] : [-(member(_218733, _218731))]]], (577 ^ _200130) ^ [_220795, _220797] : [_220797 = _220795, -(member(_220797, singleton(_220795)))], (1087 ^ _200130) ^ [_241843, _241845, _241847, _241849] : [member(_241843, inverse_image3(_241849, _241847, _241845)), 1090 ^ _200130 : [(1096 ^ _200130) ^ [] : [-(apply(_241849, _241843, 1092 ^ [_241843, _241845, _241847, _241849]))], (1094 ^ _200130) ^ [] : [-(member(1092 ^ [_241843, _241845, _241847, _241849], _241847))], (1091 ^ _200130) ^ [] : [-(member(_241843, _241845))]]], (583 ^ _200130) ^ [_221054, _221056, _221058] : [member(_221058, unordered_pair(_221056, _221054)), -(_221058 = _221056), -(_221058 = _221054)], (929 ^ _200130) ^ [_235657, _235659, _235661] : [-(surjective(_235661, _235659, _235657)), 931 ^ _200130 : [(934 ^ _200130) ^ [_235908] : [member(_235908, _235659), apply(_235661, _235908, 930 ^ [_235657, _235659, _235661])], (932 ^ _200130) ^ [] : [-(member(930 ^ [_235657, _235659, _235661], _235657))]]], (20 ^ _200130) ^ [_200906, _200908, _200910, _200912] : [-(equal_set(_200910, _200906)), equal_set(_200912, _200908), _200912 = _200910, _200908 = _200906], (610 ^ _200130) ^ [_221962, _221964] : [-(member(_221964, sum(_221962))), 611 ^ _200130 : [(612 ^ _200130) ^ [_222056] : [member(_222056, _221962), member(_221964, _222056)]]], (324 ^ _200130) ^ [_211744, _211746, _211748, _211750] : [-(intersection(_211750, _211746) = intersection(_211748, _211744)), _211750 = _211748, _211746 = _211744], (334 ^ _200130) ^ [_212103, _212105, _212107, _212109] : [-(union(_212109, _212105) = union(_212107, _212103)), _212109 = _212107, _212105 = _212103], (984 ^ _200130) ^ [_237665, _237667, _237669, _237671] : [-(inverse_predicate(_237671, _237669, _237667, _237665)), 987 ^ _200130 : [(992 ^ _200130) ^ [] : [993 ^ _200130 : [(996 ^ _200130) ^ [] : [apply(_237671, 986 ^ [_237665, _237667, _237669, _237671], 985 ^ [_237665, _237667, _237669, _237671])], (994 ^ _200130) ^ [] : [-(apply(_237669, 985 ^ [_237665, _237667, _237669, _237671], 986 ^ [_237665, _237667, _237669, _237671]))]], 997 ^ _200130 : [(1000 ^ _200130) ^ [] : [apply(_237669, 985 ^ [_237665, _237667, _237669, _237671], 986 ^ [_237665, _237667, _237669, _237671])], (998 ^ _200130) ^ [] : [-(apply(_237671, 986 ^ [_237665, _237667, _237669, _237671], 985 ^ [_237665, _237667, _237669, _237671]))]]], (990 ^ _200130) ^ [] : [-(member(986 ^ [_237665, _237667, _237669, _237671], _237665))], (988 ^ _200130) ^ [] : [-(member(985 ^ [_237665, _237667, _237669, _237671], _237667))]]], (456 ^ _200130) ^ [_216599, _216601, _216603, _216605] : [-(image2(_216605, _216601) = image2(_216603, _216599)), _216605 = _216603, _216601 = _216599], (871 ^ _200130) ^ [_233228, _233230, _233232] : [injective(_233232, _233230, _233228), 874 ^ _200130 : [(875 ^ _200130) ^ [_233435, _233437, _233439] : [member(_233439, _233230), member(_233437, _233230), member(_233435, _233228), -(_233439 = _233437), apply(_233232, _233439, _233435), apply(_233232, _233437, _233435)]]], (382 ^ _200130) ^ [_213918, _213920, _213922, _213924, _213926, _213928, _213930, _213932, _213934, _213936] : [-(compose_function(_213936, _213932, _213928, _213924, _213920) = compose_function(_213934, _213930, _213926, _213922, _213918)), _213936 = _213934, _213932 = _213930, _213928 = _213926, _213924 = _213922, _213920 = _213918], (370 ^ _200130) ^ [_213370, _213372] : [_213372 = _213370, -(sum(_213372) = sum(_213370))], (286 ^ _200130) ^ [_210443, _210445, _210447, _210449, _210451, _210453] : [-(maps(_210451, _210447, _210443)), maps(_210453, _210449, _210445), _210453 = _210451, _210449 = _210447, _210445 = _210443], (118 ^ _200130) ^ [_204421, _204423, _204425, _204427, _204429, _204431] : [-(surjective(_204429, _204425, _204421)), surjective(_204431, _204427, _204423), _204431 = _204429, _204427 = _204425, _204423 = _204421], (404 ^ _200130) ^ [_214740, _214742, _214744, _214746, _214748, _214750] : [-(inverse_function(_214750, _214746, _214742) = inverse_function(_214748, _214744, _214740)), _214750 = _214748, _214746 = _214744, _214742 = _214740], (318 ^ _200130) ^ [_211498, _211500] : [_211500 = _211498, -(power_set(_211500) = power_set(_211498))], (630 ^ _200130) ^ [_222657, _222659] : [632 ^ _200130 : [(635 ^ _200130) ^ [] : [member(_222659, 631 ^ [_222657, _222659])], (633 ^ _200130) ^ [] : [-(member(631 ^ [_222657, _222659], _222657))]], -(member(_222659, product(_222657)))], (1068 ^ _200130) ^ [_241069, _241071, _241073] : [member(_241069, inverse_image2(_241073, _241071)), 1072 ^ _200130 : [(1075 ^ _200130) ^ [] : [-(apply(_241073, _241069, 1071 ^ [_241069, _241071, _241073]))], (1073 ^ _200130) ^ [] : [-(member(1071 ^ [_241069, _241071, _241073], _241071))]]], (553 ^ _200130) ^ [_220028, _220030, _220032] : [member(_220032, difference(_220028, _220030)), 556 ^ _200130 : [(559 ^ _200130) ^ [] : [member(_220032, _220030)], (557 ^ _200130) ^ [] : [-(member(_220032, _220028))]]], (1043 ^ _200130) ^ [_240102, _240104, _240106, _240108] : [member(_240102, image3(_240108, _240106, _240104)), 1046 ^ _200130 : [(1052 ^ _200130) ^ [] : [-(apply(_240108, 1048 ^ [_240102, _240104, _240106, _240108], _240102))], (1050 ^ _200130) ^ [] : [-(member(1048 ^ [_240102, _240104, _240106, _240108], _240106))], (1047 ^ _200130) ^ [] : [-(member(_240102, _240104))]]], (184 ^ _200130) ^ [_206863, _206865, _206867, _206869, _206871, _206873, _206875, _206877, _206879, _206881] : [-(decreasing(_206879, _206875, _206871, _206867, _206863)), decreasing(_206881, _206877, _206873, _206869, _206865), _206881 = _206879, _206877 = _206875, _206873 = _206871, _206869 = _206867, _206865 = _206863], (432 ^ _200130) ^ [_215744, _215746, _215748, _215750] : [-(inverse_image2(_215750, _215746) = inverse_image2(_215748, _215744)), _215750 = _215748, _215746 = _215744], (774 ^ _200130) ^ [_229173, _229175, _229177, _229179, _229181, _229183, _229185] : [member(_229175, _229181), member(_229173, _229177), 781 ^ _200130 : [(793 ^ _200130) ^ [] : [-(apply(compose_function(_229185, _229183, _229181, _229179, _229177), _229175, _229173)), 794 ^ _200130 : [(795 ^ _200130) ^ [_229988] : [member(_229988, _229179), apply(_229183, _229175, _229988), apply(_229185, _229988, _229173)]]], (782 ^ _200130) ^ [] : [apply(compose_function(_229185, _229183, _229181, _229179, _229177), _229175, _229173), 786 ^ _200130 : [(791 ^ _200130) ^ [] : [-(apply(_229185, 785 ^ [_229173, _229175, _229177, _229179, _229181, _229183, _229185], _229173))], (789 ^ _200130) ^ [] : [-(apply(_229183, _229175, 785 ^ [_229173, _229175, _229177, _229179, _229181, _229183, _229185]))], (787 ^ _200130) ^ [] : [-(member(785 ^ [_229173, _229175, _229177, _229179, _229181, _229183, _229185], _229179))]]]]], (674 ^ _200130) ^ [_224344, _224346, _224348] : [-(maps(_224348, _224346, _224344)), 689 ^ _200130 : [(692 ^ _200130) ^ [] : [-(member(687 ^ [_224344, _224346, _224348], _224344))], (690 ^ _200130) ^ [] : [-(member(686 ^ [_224344, _224346, _224348], _224346))], (700 ^ _200130) ^ [] : [687 ^ [_224344, _224346, _224348] = 688 ^ [_224344, _224346, _224348]], (696 ^ _200130) ^ [] : [-(apply(_224348, 686 ^ [_224344, _224346, _224348], 687 ^ [_224344, _224346, _224348]))], (698 ^ _200130) ^ [] : [-(apply(_224348, 686 ^ [_224344, _224346, _224348], 688 ^ [_224344, _224346, _224348]))], (694 ^ _200130) ^ [] : [-(member(688 ^ [_224344, _224346, _224348], _224344))]], 678 ^ _200130 : [(681 ^ _200130) ^ [_224684] : [member(_224684, _224344), apply(_224348, 677 ^ [_224344, _224346, _224348], _224684)], (679 ^ _200130) ^ [] : [-(member(677 ^ [_224344, _224346, _224348], _224346))]]], (741 ^ _200130) ^ [_227379, _227381, _227383, _227385, _227387, _227389] : [-(compose_predicate(_227389, _227387, _227385, _227383, _227381, _227379)), 744 ^ _200130 : [(749 ^ _200130) ^ [] : [763 ^ _200130 : [(766 ^ _200130) ^ [] : [-(apply(_227385, 742 ^ [_227379, _227381, _227383, _227385, _227387, _227389], 762 ^ [_227379, _227381, _227383, _227385, _227387, _227389]))], (768 ^ _200130) ^ [] : [-(apply(_227387, 762 ^ [_227379, _227381, _227383, _227385, _227387, _227389], 743 ^ [_227379, _227381, _227383, _227385, _227387, _227389]))], (770 ^ _200130) ^ [] : [apply(_227389, 742 ^ [_227379, _227381, _227383, _227385, _227387, _227389], 743 ^ [_227379, _227381, _227383, _227385, _227387, _227389])], (764 ^ _200130) ^ [] : [-(member(762 ^ [_227379, _227381, _227383, _227385, _227387, _227389], _227381))]], 750 ^ _200130 : [(753 ^ _200130) ^ [_228104] : [member(_228104, _227381), apply(_227385, 742 ^ [_227379, _227381, _227383, _227385, _227387, _227389], _228104), apply(_227387, _228104, 743 ^ [_227379, _227381, _227383, _227385, _227387, _227389])], (751 ^ _200130) ^ [] : [-(apply(_227389, 742 ^ [_227379, _227381, _227383, _227385, _227387, _227389], 743 ^ [_227379, _227381, _227383, _227385, _227387, _227389]))]]], (747 ^ _200130) ^ [] : [-(member(743 ^ [_227379, _227381, _227383, _227385, _227387, _227389], _227379))], (745 ^ _200130) ^ [] : [-(member(742 ^ [_227379, _227381, _227383, _227385, _227387, _227389], _227383))]]], (551 ^ _200130) ^ [_219878] : [member(_219878, empty_set)], (960 ^ _200130) ^ [_236881, _236883, _236885, _236887] : [inverse_predicate(_236887, _236885, _236883, _236881), 963 ^ _200130 : [(964 ^ _200130) ^ [_237063, _237065] : [member(_237065, _236883), member(_237063, _236881), 971 ^ _200130 : [(978 ^ _200130) ^ [] : [apply(_236887, _237063, _237065), -(apply(_236885, _237065, _237063))], (972 ^ _200130) ^ [] : [apply(_236885, _237065, _237063), -(apply(_236887, _237063, _237065))]]]]], (418 ^ _200130) ^ [_215256, _215258, _215260, _215262, _215264, _215266] : [-(image3(_215266, _215262, _215258) = image3(_215264, _215260, _215256)), _215266 = _215264, _215262 = _215260, _215258 = _215256], (897 ^ _200130) ^ [_234060, _234062, _234064] : [901 ^ _200130 : [(904 ^ _200130) ^ [] : [-(member(899 ^ [_234060, _234062, _234064], _234062))], (902 ^ _200130) ^ [] : [-(member(898 ^ [_234060, _234062, _234064], _234062))], (912 ^ _200130) ^ [] : [898 ^ [_234060, _234062, _234064] = 899 ^ [_234060, _234062, _234064]], (908 ^ _200130) ^ [] : [-(apply(_234064, 898 ^ [_234060, _234062, _234064], 900 ^ [_234060, _234062, _234064]))], (910 ^ _200130) ^ [] : [-(apply(_234064, 899 ^ [_234060, _234062, _234064], 900 ^ [_234060, _234062, _234064]))], (906 ^ _200130) ^ [] : [-(member(900 ^ [_234060, _234062, _234064], _234060))]], -(injective(_234064, _234062, _234060))], (86 ^ _200130) ^ [_203340, _203342, _203344, _203346] : [-(identity(_203344, _203340)), identity(_203346, _203342), _203346 = _203344, _203342 = _203340], (34 ^ _200130) ^ [_201462, _201464, _201466, _201468, _201470, _201472, _201474, _201476, _201478, _201480, _201482, _201484] : [-(compose_predicate(_201482, _201478, _201474, _201470, _201466, _201462)), compose_predicate(_201484, _201480, _201476, _201472, _201468, _201464), _201484 = _201482, _201480 = _201478, _201476 = _201474, _201472 = _201470, _201468 = _201466, _201464 = _201462], (601 ^ _200130) ^ [_221651, _221653] : [member(_221653, sum(_221651)), 605 ^ _200130 : [(608 ^ _200130) ^ [] : [-(member(_221653, 604 ^ [_221651, _221653]))], (606 ^ _200130) ^ [] : [-(member(604 ^ [_221651, _221653], _221651))]]], (493 ^ _200130) ^ [_217974, _217976] : [-(equal_set(_217976, _217974)), subset(_217976, _217974), subset(_217974, _217976)], (442 ^ _200130) ^ [_216131, _216133, _216135, _216137, _216139, _216141] : [-(inverse_image3(_216141, _216137, _216133) = inverse_image3(_216139, _216135, _216131)), _216141 = _216139, _216137 = _216135, _216133 = _216131], (268 ^ _200130) ^ [_209834, _209836, _209838, _209840, _209842, _209844] : [-(apply(_209842, _209838, _209834)), apply(_209844, _209840, _209836), _209844 = _209842, _209840 = _209838, _209836 = _209834], (254 ^ _200130) ^ [_209362, _209364, _209366, _209368] : [-(member(_209366, _209362)), member(_209368, _209364), _209368 = _209366, _209364 = _209362], (64 ^ _200130) ^ [_202606, _202608, _202610, _202612, _202614, _202616, _202618, _202620] : [-(equal_maps(_202618, _202614, _202610, _202606)), equal_maps(_202620, _202616, _202612, _202608), _202620 = _202618, _202616 = _202614, _202612 = _202610, _202608 = _202606], (916 ^ _200130) ^ [_235149, _235151, _235153] : [surjective(_235153, _235151, _235149), 919 ^ _200130 : [(920 ^ _200130) ^ [_235304] : [member(_235304, _235149), 924 ^ _200130 : [(927 ^ _200130) ^ [] : [-(apply(_235153, 923 ^ [_235149, _235151, _235153, _235304], _235304))], (925 ^ _200130) ^ [] : [-(member(923 ^ [_235149, _235151, _235153, _235304], _235151))]]]]], (1024 ^ _200130) ^ [_239328, _239330, _239332] : [member(_239328, image2(_239332, _239330)), 1028 ^ _200130 : [(1031 ^ _200130) ^ [] : [-(apply(_239332, 1027 ^ [_239328, _239330, _239332], _239328))], (1029 ^ _200130) ^ [] : [-(member(1027 ^ [_239328, _239330, _239332], _239330))]]], (1170 ^ _200130) ^ [_245759, _245761, _245763, _245765, _245767] : [decreasing(_245767, _245765, _245763, _245761, _245759), 1173 ^ _200130 : [(1174 ^ _200130) ^ [_246011, _246013, _246015, _246017] : [-(apply(_245759, _246011, _246015)), member(_246017, _245765), member(_246015, _245761), member(_246013, _245765), member(_246011, _245761), apply(_245763, _246017, _246013), apply(_245767, _246017, _246015), apply(_245767, _246013, _246011)]]], (1146 ^ _200130) ^ [_244019, _244021, _244023, _244025, _244027] : [1151 ^ _200130 : [(1156 ^ _200130) ^ [] : [-(member(1149 ^ [_244019, _244021, _244023, _244025, _244027], _244025))], (1162 ^ _200130) ^ [] : [-(apply(_244027, 1147 ^ [_244019, _244021, _244023, _244025, _244027], 1148 ^ [_244019, _244021, _244023, _244025, _244027]))], (1152 ^ _200130) ^ [] : [-(member(1147 ^ [_244019, _244021, _244023, _244025, _244027], _244025))], (1164 ^ _200130) ^ [] : [-(apply(_244027, 1149 ^ [_244019, _244021, _244023, _244025, _244027], 1150 ^ [_244019, _244021, _244023, _244025, _244027]))], (1158 ^ _200130) ^ [] : [-(member(1150 ^ [_244019, _244021, _244023, _244025, _244027], _244021))], (1160 ^ _200130) ^ [] : [-(apply(_244023, 1147 ^ [_244019, _244021, _244023, _244025, _244027], 1149 ^ [_244019, _244021, _244023, _244025, _244027]))], (1166 ^ _200130) ^ [] : [apply(_244019, 1148 ^ [_244019, _244021, _244023, _244025, _244027], 1150 ^ [_244019, _244021, _244023, _244025, _244027])], (1154 ^ _200130) ^ [] : [-(member(1148 ^ [_244019, _244021, _244023, _244025, _244027], _244021))]], -(increasing(_244027, _244025, _244023, _244021, _244019))], (523 ^ _200130) ^ [_218980, _218982, _218984] : [-(member(_218984, intersection(_218982, _218980))), member(_218984, _218982), member(_218984, _218980)], (1077 ^ _200130) ^ [_241401, _241403, _241405] : [-(member(_241401, inverse_image2(_241405, _241403))), 1078 ^ _200130 : [(1079 ^ _200130) ^ [_241499] : [member(_241499, _241403), apply(_241405, _241401, _241499)]]], (344 ^ _200130) ^ [_212462, _212464, _212466, _212468] : [-(difference(_212468, _212464) = difference(_212466, _212462)), _212468 = _212466, _212464 = _212462], (852 ^ _200130) ^ [_232501, _232503] : [identity(_232503, _232501), 855 ^ _200130 : [(856 ^ _200130) ^ [_232639] : [member(_232639, _232501), -(apply(_232503, _232639, _232639))]]]], input).
% 83.62/81.11 ncf('1',plain,[-(subset(1312 ^ [], 1313 ^ []))],start(1321 ^ 0)).
% 83.62/81.11 ncf('1.1',plain,[subset(1312 ^ [], 1313 ^ []), 470 : member(1027 ^ [477 ^ [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])], 1312 ^ [], 1309 ^ []], 1312 ^ []), 470 : -(member(1027 ^ [477 ^ [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])], 1312 ^ [], 1309 ^ []], 1313 ^ []))],extension(466 ^ 1,bind([[_217037, _217039, _217174], [1313 ^ [], 1312 ^ [], 1027 ^ [477 ^ [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])], 1312 ^ [], 1309 ^ []]]]))).
% 83.62/81.11 ncf('1.1.1',plain,[-(member(1027 ^ [477 ^ [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])], 1312 ^ [], 1309 ^ []], 1312 ^ [])), member(477 ^ [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])], image2(1309 ^ [], 1312 ^ []))],extension(1024 ^ 4,bind([[_239328, _239330, _239332], [477 ^ [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])], 1312 ^ [], 1309 ^ []]]))).
% 83.62/81.11 ncf('1.1.1.1',plain,[-(member(477 ^ [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])], image2(1309 ^ [], 1312 ^ []))), -(subset(image2(1309 ^ [], 1312 ^ []), image2(1309 ^ [], 1313 ^ [])))],extension(476 ^ 5,bind([[_217351, _217353], [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])]]))).
% 83.62/81.11 ncf('1.1.1.1.1',plain,[subset(image2(1309 ^ [], 1312 ^ []), image2(1309 ^ [], 1313 ^ []))],extension(1323 ^ 6)).
% 83.62/81.11 ncf('1.1.2',plain,[member(1027 ^ [477 ^ [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])], 1312 ^ [], 1309 ^ []], 1313 ^ []), 1035 : apply(1309 ^ [], 1027 ^ [477 ^ [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])], 1312 ^ [], 1309 ^ []], 477 ^ [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])]), 1035 : -(member(477 ^ [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])], image2(1309 ^ [], 1313 ^ [])))],extension(1033 ^ 4,bind([[_239660, _239662, _239664, _239758], [477 ^ [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])], 1313 ^ [], 1309 ^ [], 1027 ^ [477 ^ [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])], 1312 ^ [], 1309 ^ []]]]))).
% 83.62/81.11 ncf('1.1.2.1',plain,[-(apply(1309 ^ [], 1027 ^ [477 ^ [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])], 1312 ^ [], 1309 ^ []], 477 ^ [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])])), member(477 ^ [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])], image2(1309 ^ [], 1312 ^ []))],extension(1024 ^ 7,bind([[_239328, _239330, _239332], [477 ^ [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])], 1312 ^ [], 1309 ^ []]]))).
% 83.62/81.11 ncf('1.1.2.1.1',plain,[-(member(477 ^ [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])], image2(1309 ^ [], 1312 ^ []))), -(subset(image2(1309 ^ [], 1312 ^ []), image2(1309 ^ [], 1313 ^ [])))],extension(476 ^ 8,bind([[_217351, _217353], [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])]]))).
% 83.62/81.11 ncf('1.1.2.1.1.1',plain,[subset(image2(1309 ^ [], 1312 ^ []), image2(1309 ^ [], 1313 ^ []))],extension(1323 ^ 9)).
% 83.62/81.11 ncf('1.1.2.2',plain,[member(477 ^ [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])], image2(1309 ^ [], 1313 ^ [])), -(subset(image2(1309 ^ [], 1312 ^ []), image2(1309 ^ [], 1313 ^ [])))],extension(476 ^ 5,bind([[_217351, _217353], [image2(1309 ^ [], 1313 ^ []), image2(1309 ^ [], 1312 ^ [])]]))).
% 83.62/81.11 ncf('1.1.2.2.1',plain,[subset(image2(1309 ^ [], 1312 ^ []), image2(1309 ^ [], 1313 ^ []))],extension(1323 ^ 6)).
% 83.62/81.11 %-----------------------------------------------------
% 83.62/81.11 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------