%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GRP653+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n003.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:16:28 EDT 2023
% Result : Theorem 0.48s 1.40s
% Output : Proof 0.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : GRP653+1 : TPTP v8.1.2. Released v3.4.0.
% 0.04/0.14 % Command : nanocop.sh %s %d
% 0.14/0.35 % Computer : n003.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 : Fri May 19 02:09:30 EDT 2023
% 0.14/0.35 % CPUTime :
% 0.48/1.40
% 0.48/1.40 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.48/1.40 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/1.40 %-----------------------------------------------------
% 0.48/1.40 ncf(matrix, plain, [(1399 ^ _205816) ^ [] : [v3_struct_0(1397 ^ [])], (1401 ^ _205816) ^ [] : [-(v3_group_1(1397 ^ []))], (1403 ^ _205816) ^ [] : [-(v4_group_1(1397 ^ []))], (1405 ^ _205816) ^ [] : [-(l1_group_1(1397 ^ []))], (1408 ^ _205816) ^ [] : [v3_struct_0(1406 ^ [])], (1410 ^ _205816) ^ [] : [-(v3_group_1(1406 ^ []))], (1412 ^ _205816) ^ [] : [-(v4_group_1(1406 ^ []))], (1414 ^ _205816) ^ [] : [-(l1_group_1(1406 ^ []))], (1417 ^ _205816) ^ [] : [-(v1_funct_1(1415 ^ []))], (1419 ^ _205816) ^ [] : [-(v1_funct_2(1415 ^ [], u1_struct_0(1397 ^ []), u1_struct_0(1406 ^ [])))], (1421 ^ _205816) ^ [] : [-(v1_group_6(1415 ^ [], 1397 ^ [], 1406 ^ []))], (1423 ^ _205816) ^ [] : [-(m2_relset_1(1415 ^ [], u1_struct_0(1397 ^ []), u1_struct_0(1406 ^ [])))], (1425 ^ _205816) ^ [] : [-(v2_funct_1(1415 ^ []))], (1427 ^ _205816) ^ [] : [m1_lattice4(k3_latsubgr(1397 ^ [], 1406 ^ [], 1415 ^ []), k11_group_4(1397 ^ []), k11_group_4(1406 ^ []))], (436 ^ _205816) ^ [_219733, _219735] : [_219735 = _219733, -(u1_lattices(_219735) = u1_lattices(_219733))], (442 ^ _205816) ^ [_219951, _219953] : [_219953 = _219951, -(u2_lattices(_219953) = u2_lattices(_219951))], (448 ^ _205816) ^ [_220197, _220199, _220201, _220203] : [-(k2_zfmisc_1(_220203, _220199) = k2_zfmisc_1(_220201, _220197)), _220203 = _220201, _220199 = _220197], (458 ^ _205816) ^ [_220584, _220586, _220588, _220590, _220592, _220594] : [-(g3_lattices(_220594, _220590, _220586) = g3_lattices(_220592, _220588, _220584)), _220594 = _220592, _220590 = _220588, _220586 = _220584], (472 ^ _205816) ^ [_221044, _221046] : [_221046 = _221044, -(k1_zfmisc_1(_221046) = k1_zfmisc_1(_221044))], (478 ^ _205816) ^ [_221262, _221264] : [_221264 = _221262, -(u1_struct_0(_221264) = u1_struct_0(_221262))], (498 ^ _205816) ^ [_221976, _221978] : [_221978 = _221976, -(k11_group_4(_221978) = k11_group_4(_221976))], (484 ^ _205816) ^ [_221536, _221538, _221540, _221542, _221544, _221546] : [-(k3_latsubgr(_221546, _221542, _221538) = k3_latsubgr(_221544, _221540, _221536)), _221546 = _221544, _221542 = _221540, _221538 = _221536], (2 ^ _205816) ^ [_205960] : [-(_205960 = _205960)], (4 ^ _205816) ^ [_206067, _206069] : [_206069 = _206067, -(_206067 = _206069)], (10 ^ _205816) ^ [_206271, _206273, _206275] : [-(_206275 = _206271), _206275 = _206273, _206273 = _206271], (20 ^ _205816) ^ [_206640, _206642, _206644, _206646, _206648, _206650] : [-(v1_partfun1(_206648, _206644, _206640)), v1_partfun1(_206650, _206646, _206642), _206650 = _206648, _206646 = _206644, _206642 = _206640], (38 ^ _205816) ^ [_207193, _207195] : [-(l1_lattices(_207193)), _207195 = _207193, l1_lattices(_207195)], (48 ^ _205816) ^ [_207488, _207490] : [-(l2_lattices(_207488)), _207490 = _207488, l2_lattices(_207490)], (58 ^ _205816) ^ [_207783, _207785] : [-(v3_lattices(_207783)), _207785 = _207783, v3_lattices(_207785)], (68 ^ _205816) ^ [_208078, _208080] : [-(v4_lattices(_208078)), _208080 = _208078, v4_lattices(_208080)], (78 ^ _205816) ^ [_208373, _208375] : [-(v5_lattices(_208373)), _208375 = _208373, v5_lattices(_208375)], (88 ^ _205816) ^ [_208668, _208670] : [-(v6_lattices(_208668)), _208670 = _208668, v6_lattices(_208670)], (98 ^ _205816) ^ [_208963, _208965] : [-(v7_lattices(_208963)), _208965 = _208963, v7_lattices(_208965)], (108 ^ _205816) ^ [_209258, _209260] : [-(v8_lattices(_209258)), _209260 = _209258, v8_lattices(_209260)], (118 ^ _205816) ^ [_209553, _209555] : [-(v9_lattices(_209553)), _209555 = _209553, v9_lattices(_209555)], (128 ^ _205816) ^ [_209848, _209850] : [-(v13_lattices(_209848)), _209850 = _209848, v13_lattices(_209850)], (138 ^ _205816) ^ [_210143, _210145] : [-(v14_lattices(_210143)), _210145 = _210143, v14_lattices(_210145)], (148 ^ _205816) ^ [_210438, _210440] : [-(v15_lattices(_210438)), _210440 = _210438, v15_lattices(_210440)], (158 ^ _205816) ^ [_210733, _210735] : [-(v1_relat_1(_210733)), _210735 = _210733, v1_relat_1(_210735)], (168 ^ _205816) ^ [_211028, _211030] : [-(l1_struct_0(_211028)), _211030 = _211028, l1_struct_0(_211030)], (178 ^ _205816) ^ [_211379, _211381, _211383, _211385, _211387, _211389] : [-(m1_relset_1(_211387, _211383, _211379)), m1_relset_1(_211389, _211385, _211381), _211389 = _211387, _211385 = _211383, _211381 = _211379], (196 ^ _205816) ^ [_211932, _211934] : [-(v10_lattices(_211932)), _211934 = _211932, v10_lattices(_211934)], (206 ^ _205816) ^ [_212227, _212229] : [-(l3_lattices(_212227)), _212229 = _212227, l3_lattices(_212229)], (216 ^ _205816) ^ [_212578, _212580, _212582, _212584, _212586, _212588] : [-(m3_vectsp_8(_212586, _212582, _212578)), m3_vectsp_8(_212588, _212584, _212580), _212588 = _212586, _212584 = _212582, _212580 = _212578], (234 ^ _205816) ^ [_213187, _213189, _213191, _213193, _213195, _213197] : [-(m4_vectsp_8(_213195, _213191, _213187)), m4_vectsp_8(_213197, _213193, _213189), _213197 = _213195, _213193 = _213191, _213189 = _213187], (252 ^ _205816) ^ [_213768, _213770, _213772, _213774] : [-(r1_tarski(_213772, _213768)), r1_tarski(_213774, _213770), _213774 = _213772, _213770 = _213768], (266 ^ _205816) ^ [_214212, _214214, _214216, _214218] : [-(m1_subset_1(_214216, _214212)), m1_subset_1(_214218, _214214), _214218 = _214216, _214214 = _214212], (280 ^ _205816) ^ [_214656, _214658, _214660, _214662] : [-(r2_hidden(_214660, _214656)), r2_hidden(_214662, _214658), _214662 = _214660, _214658 = _214656], (294 ^ _205816) ^ [_215072, _215074] : [-(v1_xboole_0(_215072)), _215074 = _215072, v1_xboole_0(_215074)], (304 ^ _205816) ^ [_215367, _215369] : [-(v3_struct_0(_215367)), _215369 = _215367, v3_struct_0(_215369)], (314 ^ _205816) ^ [_215662, _215664] : [-(v3_group_1(_215662)), _215664 = _215662, v3_group_1(_215664)], (324 ^ _205816) ^ [_215957, _215959] : [-(v4_group_1(_215957)), _215959 = _215957, v4_group_1(_215959)], (334 ^ _205816) ^ [_216252, _216254] : [-(l1_group_1(_216252)), _216254 = _216252, l1_group_1(_216254)], (344 ^ _205816) ^ [_216547, _216549] : [-(v1_funct_1(_216547)), _216549 = _216547, v1_funct_1(_216549)], (354 ^ _205816) ^ [_216898, _216900, _216902, _216904, _216906, _216908] : [-(v1_funct_2(_216906, _216902, _216898)), v1_funct_2(_216908, _216904, _216900), _216908 = _216906, _216904 = _216902, _216900 = _216898], (372 ^ _205816) ^ [_217507, _217509, _217511, _217513, _217515, _217517] : [-(v1_group_6(_217515, _217511, _217507)), v1_group_6(_217517, _217513, _217509), _217517 = _217515, _217513 = _217511, _217509 = _217507], (390 ^ _205816) ^ [_218116, _218118, _218120, _218122, _218124, _218126] : [-(m2_relset_1(_218124, _218120, _218116)), m2_relset_1(_218126, _218122, _218118), _218126 = _218124, _218122 = _218120, _218118 = _218116], (408 ^ _205816) ^ [_218669, _218671] : [-(v2_funct_1(_218669)), _218671 = _218669, v2_funct_1(_218671)], (418 ^ _205816) ^ [_219000, _219002, _219004, _219006, _219008, _219010] : [-(m1_lattice4(_219008, _219004, _219000)), m1_lattice4(_219010, _219006, _219002), _219010 = _219008, _219006 = _219004, _219002 = _219000], (504 ^ _205816) ^ [_222215] : [l3_lattices(_222215), v3_lattices(_222215), -(_222215 = g3_lattices(u1_struct_0(_222215), u2_lattices(_222215), u1_lattices(_222215)))], (514 ^ _205816) ^ [_222520, _222522] : [r2_hidden(_222522, _222520), r2_hidden(_222520, _222522)], (520 ^ _205816) ^ [_222745, _222747, _222749] : [m1_relset_1(_222745, _222749, _222747), 531 ^ _205816 : [(532 ^ _205816) ^ [] : [-(v1_funct_1(_222745))], (534 ^ _205816) ^ [] : [-(v1_funct_2(_222745, _222749, _222747))]], v1_funct_1(_222745), v1_partfun1(_222745, _222749, _222747)], (536 ^ _205816) ^ [_223240, _223242, _223244] : [m1_subset_1(_223240, k1_zfmisc_1(k2_zfmisc_1(_223244, _223242))), -(v1_relat_1(_223240))], (542 ^ _205816) ^ [_223464, _223466] : [-(v1_xboole_0(_223464)), 545 ^ _205816 : [(546 ^ _205816) ^ [_223628] : [m1_relset_1(_223628, _223466, _223464), 557 ^ _205816 : [(558 ^ _205816) ^ [] : [-(v1_funct_1(_223628))], (560 ^ _205816) ^ [] : [-(v1_partfun1(_223628, _223466, _223464))], (562 ^ _205816) ^ [] : [-(v1_funct_2(_223628, _223466, _223464))]], v1_funct_1(_223628), v1_funct_2(_223628, _223466, _223464)]]], (564 ^ _205816) ^ [_224196, _224198] : [-(v1_xboole_0(_224198)), -(v1_xboole_0(_224196)), 571 ^ _205816 : [(572 ^ _205816) ^ [_224457] : [m1_relset_1(_224457, _224198, _224196), 583 ^ _205816 : [(584 ^ _205816) ^ [] : [-(v1_funct_1(_224457))], (586 ^ _205816) ^ [] : [v1_xboole_0(_224457)], (588 ^ _205816) ^ [] : [-(v1_partfun1(_224457, _224198, _224196))], (590 ^ _205816) ^ [] : [-(v1_funct_2(_224457, _224198, _224196))]], v1_funct_1(_224457), v1_funct_2(_224457, _224198, _224196)]]], (592 ^ _205816) ^ [_225116, _225118, _225120] : [615 ^ _205816 : [(616 ^ _205816) ^ [] : [-(v3_lattices(g3_lattices(_225120, _225118, _225116)))], (618 ^ _205816) ^ [] : [-(l3_lattices(g3_lattices(_225120, _225118, _225116)))]], v1_funct_1(_225118), v1_funct_2(_225118, k2_zfmisc_1(_225120, _225120), _225120), m1_relset_1(_225118, k2_zfmisc_1(_225120, _225120), _225120), v1_funct_1(_225116), v1_funct_2(_225116, k2_zfmisc_1(_225120, _225120), _225120), m1_relset_1(_225116, k2_zfmisc_1(_225120, _225120), _225120)], (620 ^ _205816) ^ [_225900] : [635 ^ _205816 : [(636 ^ _205816) ^ [] : [v3_struct_0(k11_group_4(_225900))], (638 ^ _205816) ^ [] : [-(v3_lattices(k11_group_4(_225900)))], (640 ^ _205816) ^ [] : [-(v10_lattices(k11_group_4(_225900)))], (642 ^ _205816) ^ [] : [-(l3_lattices(k11_group_4(_225900)))]], -(v3_struct_0(_225900)), v3_group_1(_225900), v4_group_1(_225900), l1_group_1(_225900)], (644 ^ _205816) ^ [] : [true___, -(true___)], (650 ^ _205816) ^ [] : [true___, -(true___)], (656 ^ _205816) ^ [] : [true___, -(true___)], (662 ^ _205816) ^ [_226951, _226953, _226955] : [705 ^ _205816 : [(706 ^ _205816) ^ [] : [-(v1_funct_1(k3_latsubgr(_226955, _226953, _226951)))], (708 ^ _205816) ^ [] : [-(v1_funct_2(k3_latsubgr(_226955, _226953, _226951), u1_struct_0(k11_group_4(_226955)), u1_struct_0(k11_group_4(_226953))))], (710 ^ _205816) ^ [] : [-(m2_relset_1(k3_latsubgr(_226955, _226953, _226951), u1_struct_0(k11_group_4(_226955)), u1_struct_0(k11_group_4(_226953))))]], -(v3_struct_0(_226955)), v3_group_1(_226955), v4_group_1(_226955), l1_group_1(_226955), -(v3_struct_0(_226953)), v3_group_1(_226953), v4_group_1(_226953), l1_group_1(_226953), v1_funct_1(_226951), v1_funct_2(_226951, u1_struct_0(_226955), u1_struct_0(_226953)), m1_relset_1(_226951, u1_struct_0(_226955), u1_struct_0(_226953))], (712 ^ _205816) ^ [_228302] : [l1_group_1(_228302), -(l1_struct_0(_228302))], (718 ^ _205816) ^ [_228488] : [l1_lattices(_228488), -(l1_struct_0(_228488))], (724 ^ _205816) ^ [] : [true___, -(true___)], (730 ^ _205816) ^ [_228793] : [l2_lattices(_228793), -(l1_struct_0(_228793))], (736 ^ _205816) ^ [_228979] : [l3_lattices(_228979), 739 ^ _205816 : [(740 ^ _205816) ^ [] : [-(l1_lattices(_228979))], (742 ^ _205816) ^ [] : [-(l2_lattices(_228979))]]], (744 ^ _205816) ^ [_229250, _229252] : [767 ^ _205816 : [(768 ^ _205816) ^ [_229848] : [m1_lattice4(_229848, _229252, _229250), 771 ^ _205816 : [(772 ^ _205816) ^ [] : [-(v1_funct_1(_229848))], (774 ^ _205816) ^ [] : [-(v1_funct_2(_229848, u1_struct_0(_229252), u1_struct_0(_229250)))], (776 ^ _205816) ^ [] : [-(m2_relset_1(_229848, u1_struct_0(_229252), u1_struct_0(_229250)))]]]], -(v3_struct_0(_229252)), v10_lattices(_229252), l3_lattices(_229252), -(v3_struct_0(_229250)), v10_lattices(_229250), l3_lattices(_229250)], (778 ^ _205816) ^ [] : [true___, -(true___)], (784 ^ _205816) ^ [] : [true___, -(true___)], (790 ^ _205816) ^ [_230498, _230500, _230502] : [m2_relset_1(_230498, _230502, _230500), -(m1_subset_1(_230498, k1_zfmisc_1(k2_zfmisc_1(_230502, _230500))))], (796 ^ _205816) ^ [_230726, _230728] : [819 ^ _205816 : [(820 ^ _205816) ^ [_231324] : [m3_vectsp_8(_231324, _230728, _230726), 823 ^ _205816 : [(824 ^ _205816) ^ [] : [-(v1_funct_1(_231324))], (826 ^ _205816) ^ [] : [-(v1_funct_2(_231324, u1_struct_0(_230728), u1_struct_0(_230726)))], (828 ^ _205816) ^ [] : [-(m2_relset_1(_231324, u1_struct_0(_230728), u1_struct_0(_230726)))]]]], -(v3_struct_0(_230728)), v10_lattices(_230728), l3_lattices(_230728), -(v3_struct_0(_230726)), v10_lattices(_230726), l3_lattices(_230726)], (830 ^ _205816) ^ [_231722, _231724] : [853 ^ _205816 : [(854 ^ _205816) ^ [_232320] : [m4_vectsp_8(_232320, _231724, _231722), 857 ^ _205816 : [(858 ^ _205816) ^ [] : [-(v1_funct_1(_232320))], (860 ^ _205816) ^ [] : [-(v1_funct_2(_232320, u1_struct_0(_231724), u1_struct_0(_231722)))], (862 ^ _205816) ^ [] : [-(m2_relset_1(_232320, u1_struct_0(_231724), u1_struct_0(_231722)))]]]], -(v3_struct_0(_231724)), v10_lattices(_231724), l3_lattices(_231724), -(v3_struct_0(_231722)), v10_lattices(_231722), l3_lattices(_231722)], (864 ^ _205816) ^ [_232704] : [l1_lattices(_232704), 867 ^ _205816 : [(868 ^ _205816) ^ [] : [-(v1_funct_1(u1_lattices(_232704)))], (870 ^ _205816) ^ [] : [-(v1_funct_2(u1_lattices(_232704), k2_zfmisc_1(u1_struct_0(_232704), u1_struct_0(_232704)), u1_struct_0(_232704)))], (872 ^ _205816) ^ [] : [-(m2_relset_1(u1_lattices(_232704), k2_zfmisc_1(u1_struct_0(_232704), u1_struct_0(_232704)), u1_struct_0(_232704)))]]], (874 ^ _205816) ^ [] : [true___, -(true___)], (880 ^ _205816) ^ [_233206] : [l2_lattices(_233206), 883 ^ _205816 : [(884 ^ _205816) ^ [] : [-(v1_funct_1(u2_lattices(_233206)))], (886 ^ _205816) ^ [] : [-(v1_funct_2(u2_lattices(_233206), k2_zfmisc_1(u1_struct_0(_233206), u1_struct_0(_233206)), u1_struct_0(_233206)))], (888 ^ _205816) ^ [] : [-(m2_relset_1(u2_lattices(_233206), k2_zfmisc_1(u1_struct_0(_233206), u1_struct_0(_233206)), u1_struct_0(_233206)))]]], (891 ^ _205816) ^ [] : [-(l1_group_1(889 ^ []))], (894 ^ _205816) ^ [] : [-(l1_lattices(892 ^ []))], (897 ^ _205816) ^ [] : [-(l1_struct_0(895 ^ []))], (900 ^ _205816) ^ [] : [-(l2_lattices(898 ^ []))], (903 ^ _205816) ^ [] : [-(l3_lattices(901 ^ []))], (905 ^ _205816) ^ [_234048, _234050] : [-(m1_lattice4(928 ^ [_234048, _234050], _234050, _234048)), -(v3_struct_0(_234050)), v10_lattices(_234050), l3_lattices(_234050), -(v3_struct_0(_234048)), v10_lattices(_234048), l3_lattices(_234048)], (933 ^ _205816) ^ [_234784, _234786] : [-(m1_relset_1(931 ^ [_234784, _234786], _234786, _234784))], (936 ^ _205816) ^ [_234911] : [-(m1_subset_1(934 ^ [_234911], _234911))], (939 ^ _205816) ^ [_235050, _235052] : [-(m2_relset_1(937 ^ [_235050, _235052], _235052, _235050))], (941 ^ _205816) ^ [_235167, _235169] : [-(m3_vectsp_8(964 ^ [_235167, _235169], _235169, _235167)), -(v3_struct_0(_235169)), v10_lattices(_235169), l3_lattices(_235169), -(v3_struct_0(_235167)), v10_lattices(_235167), l3_lattices(_235167)], (968 ^ _205816) ^ [_235876, _235878] : [-(m4_vectsp_8(991 ^ [_235876, _235878], _235878, _235876)), -(v3_struct_0(_235878)), v10_lattices(_235878), l3_lattices(_235878), -(v3_struct_0(_235876)), v10_lattices(_235876), l3_lattices(_235876)], (995 ^ _205816) ^ [_236571] : [1010 ^ _205816 : [(1011 ^ _205816) ^ [] : [v3_struct_0(k11_group_4(_236571))], (1013 ^ _205816) ^ [] : [-(v3_lattices(k11_group_4(_236571)))], (1015 ^ _205816) ^ [] : [-(v4_lattices(k11_group_4(_236571)))], (1017 ^ _205816) ^ [] : [-(v5_lattices(k11_group_4(_236571)))], (1019 ^ _205816) ^ [] : [-(v6_lattices(k11_group_4(_236571)))], (1021 ^ _205816) ^ [] : [-(v7_lattices(k11_group_4(_236571)))], (1023 ^ _205816) ^ [] : [-(v8_lattices(k11_group_4(_236571)))], (1025 ^ _205816) ^ [] : [-(v9_lattices(k11_group_4(_236571)))], (1027 ^ _205816) ^ [] : [-(v10_lattices(k11_group_4(_236571)))], (1029 ^ _205816) ^ [] : [-(v13_lattices(k11_group_4(_236571)))], (1031 ^ _205816) ^ [] : [-(v14_lattices(k11_group_4(_236571)))], (1033 ^ _205816) ^ [] : [-(v15_lattices(k11_group_4(_236571)))]], -(v3_struct_0(_236571)), v3_group_1(_236571), v4_group_1(_236571), l1_group_1(_236571)], (1035 ^ _205816) ^ [_237829] : [v1_xboole_0(u1_struct_0(_237829)), -(v3_struct_0(_237829)), l1_struct_0(_237829)], (1045 ^ _205816) ^ [_238090] : [v1_xboole_0(k1_zfmisc_1(_238090))], (1047 ^ _205816) ^ [] : [-(v1_xboole_0(k1_xboole_0))], (1049 ^ _205816) ^ [_238251, _238253] : [v1_xboole_0(k2_zfmisc_1(_238253, _238251)), -(v1_xboole_0(_238253)), -(v1_xboole_0(_238251))], (1059 ^ _205816) ^ [_238571, _238573, _238575] : [1082 ^ _205816 : [(1083 ^ _205816) ^ [_239263, _239265, _239267] : [g3_lattices(_238575, _238573, _238571) = g3_lattices(_239267, _239265, _239263), 1086 ^ _205816 : [(1087 ^ _205816) ^ [] : [-(_238575 = _239267)], (1089 ^ _205816) ^ [] : [-(_238573 = _239265)], (1091 ^ _205816) ^ [] : [-(_238571 = _239263)]]]], v1_funct_1(_238573), v1_funct_2(_238573, k2_zfmisc_1(_238575, _238575), _238575), m1_relset_1(_238573, k2_zfmisc_1(_238575, _238575), _238575), v1_funct_1(_238571), v1_funct_2(_238571, k2_zfmisc_1(_238575, _238575), _238575), m1_relset_1(_238571, k2_zfmisc_1(_238575, _238575), _238575)], (1094 ^ _205816) ^ [_239753, _239755] : [-(m1_relset_1(1092 ^ [_239753, _239755], _239755, _239753))], (1096 ^ _205816) ^ [_239827, _239829] : [-(v1_relat_1(1092 ^ [_239827, _239829]))], (1098 ^ _205816) ^ [_239899, _239901] : [-(v1_funct_1(1092 ^ [_239899, _239901]))], (1100 ^ _205816) ^ [_239951, _239953] : [-(v1_funct_2(1092 ^ [_239951, _239953], _239953, _239951))], (1103 ^ _205816) ^ [] : [-(v1_relat_1(1101 ^ []))], (1105 ^ _205816) ^ [] : [-(v1_funct_1(1101 ^ []))], (1107 ^ _205816) ^ [] : [-(v2_funct_1(1101 ^ []))], (1109 ^ _205816) ^ [] : [-(v1_xboole_0(1101 ^ []))], (1111 ^ _205816) ^ [_240329] : [-(v1_xboole_0(_240329)), 1115 ^ _205816 : [(1116 ^ _205816) ^ [] : [-(m1_subset_1(1114 ^ [_240329], k1_zfmisc_1(_240329)))], (1118 ^ _205816) ^ [] : [v1_xboole_0(1114 ^ [_240329])]]], (1121 ^ _205816) ^ [] : [-(v1_xboole_0(1119 ^ []))], (1124 ^ _205816) ^ [_240821, _240823] : [-(m1_relset_1(1122 ^ [_240821, _240823], _240823, _240821))], (1126 ^ _205816) ^ [_240895, _240897] : [-(v1_relat_1(1122 ^ [_240895, _240897]))], (1128 ^ _205816) ^ [_240947, _240949] : [-(v1_funct_1(1122 ^ [_240947, _240949]))], (1131 ^ _205816) ^ [_241103] : [-(m1_subset_1(1129 ^ [_241103], k1_zfmisc_1(_241103)))], (1133 ^ _205816) ^ [_241154] : [-(v1_xboole_0(1129 ^ [_241154]))], (1136 ^ _205816) ^ [] : [v1_xboole_0(1134 ^ [])], (1139 ^ _205816) ^ [] : [-(l1_struct_0(1137 ^ []))], (1141 ^ _205816) ^ [] : [v3_struct_0(1137 ^ [])], (1143 ^ _205816) ^ [_241493] : [1151 ^ _205816 : [(1152 ^ _205816) ^ [] : [-(m1_subset_1(1150 ^ [_241493], k1_zfmisc_1(u1_struct_0(_241493))))], (1154 ^ _205816) ^ [] : [v1_xboole_0(1150 ^ [_241493])]], -(v3_struct_0(_241493)), l1_struct_0(_241493)], (1156 ^ _205816) ^ [_241971, _241973, _241975] : [m2_relset_1(_241971, _241975, _241973), -(m1_relset_1(_241971, _241975, _241973))], (1162 ^ _205816) ^ [_242143, _242145, _242147] : [m1_relset_1(_242143, _242147, _242145), -(m2_relset_1(_242143, _242147, _242145))], (1168 ^ _205816) ^ [_242350, _242352] : [-(r1_tarski(_242352, _242352))], (1170 ^ _205816) ^ [_242445] : [-(v3_struct_0(_242445)), v10_lattices(_242445), l3_lattices(_242445), 1181 ^ _205816 : [(1182 ^ _205816) ^ [_242803] : [-(v3_struct_0(_242803)), v10_lattices(_242803), l3_lattices(_242803), 1193 ^ _205816 : [(1194 ^ _205816) ^ [_243153] : [v1_funct_1(_243153), v1_funct_2(_243153, u1_struct_0(_242445), u1_struct_0(_242803)), m2_relset_1(_243153, u1_struct_0(_242445), u1_struct_0(_242803)), 1205 ^ _205816 : [(1206 ^ _205816) ^ [] : [m1_lattice4(_243153, _242445, _242803), 1209 ^ _205816 : [(1210 ^ _205816) ^ [] : [-(m4_vectsp_8(_243153, _242445, _242803))], (1212 ^ _205816) ^ [] : [-(m3_vectsp_8(_243153, _242445, _242803))]]], (1214 ^ _205816) ^ [] : [-(m1_lattice4(_243153, _242445, _242803)), m4_vectsp_8(_243153, _242445, _242803), m3_vectsp_8(_243153, _242445, _242803)]]]]]]], (1224 ^ _205816) ^ [_244032, _244034] : [r2_hidden(_244034, _244032), -(m1_subset_1(_244034, _244032))], (1230 ^ _205816) ^ [_244242, _244244] : [m1_subset_1(_244244, _244242), -(v1_xboole_0(_244242)), -(r2_hidden(_244244, _244242))], (1240 ^ _205816) ^ [_244526] : [-(v3_struct_0(_244526)), v3_group_1(_244526), v4_group_1(_244526), l1_group_1(_244526), 1255 ^ _205816 : [(1256 ^ _205816) ^ [_244978] : [-(v3_struct_0(_244978)), v3_group_1(_244978), v4_group_1(_244978), l1_group_1(_244978), 1271 ^ _205816 : [(1272 ^ _205816) ^ [_245421] : [v2_funct_1(_245421), -(m3_vectsp_8(k3_latsubgr(_244526, _244978, _245421), k11_group_4(_244526), k11_group_4(_244978))), v1_funct_1(_245421), v1_funct_2(_245421, u1_struct_0(_244526), u1_struct_0(_244978)), v1_group_6(_245421, _244526, _244978), m2_relset_1(_245421, u1_struct_0(_244526), u1_struct_0(_244978))]]]]], (1294 ^ _205816) ^ [_246059] : [-(v3_struct_0(_246059)), v3_group_1(_246059), v4_group_1(_246059), l1_group_1(_246059), 1309 ^ _205816 : [(1310 ^ _205816) ^ [_246506] : [-(v3_struct_0(_246506)), v3_group_1(_246506), v4_group_1(_246506), l1_group_1(_246506), 1325 ^ _205816 : [(1326 ^ _205816) ^ [_246944] : [-(m4_vectsp_8(k3_latsubgr(_246059, _246506, _246944), k11_group_4(_246059), k11_group_4(_246506))), v1_funct_1(_246944), v1_funct_2(_246944, u1_struct_0(_246059), u1_struct_0(_246506)), v1_group_6(_246944, _246059, _246506), m2_relset_1(_246944, u1_struct_0(_246059), u1_struct_0(_246506))]]]]], (1344 ^ _205816) ^ [_247532, _247534] : [m1_subset_1(_247534, k1_zfmisc_1(_247532)), -(r1_tarski(_247534, _247532))], (1350 ^ _205816) ^ [_247698, _247700] : [r1_tarski(_247700, _247698), -(m1_subset_1(_247700, k1_zfmisc_1(_247698)))], (1356 ^ _205816) ^ [_247928, _247930, _247932] : [-(m1_subset_1(_247932, _247928)), r2_hidden(_247932, _247930), m1_subset_1(_247930, k1_zfmisc_1(_247928))], (1366 ^ _205816) ^ [_248255, _248257, _248259] : [r2_hidden(_248259, _248257), m1_subset_1(_248257, k1_zfmisc_1(_248255)), v1_xboole_0(_248255)], (1376 ^ _205816) ^ [_248551] : [v1_xboole_0(_248551), -(_248551 = k1_xboole_0)], (1382 ^ _205816) ^ [_248753, _248755] : [r2_hidden(_248755, _248753), v1_xboole_0(_248753)], (1388 ^ _205816) ^ [_248940, _248942] : [v1_xboole_0(_248942), -(_248942 = _248940), v1_xboole_0(_248940)]], input).
% 0.48/1.40 ncf('1',plain,[v3_struct_0(1397 ^ [])],start(1399 ^ 0)).
% 0.48/1.40 ncf('1.1',plain,[-(v3_struct_0(1397 ^ [])), 706 : -(v1_funct_1(k3_latsubgr(1397 ^ [], 1406 ^ [], 1415 ^ []))), 706 : v3_group_1(1397 ^ []), 706 : v4_group_1(1397 ^ []), 706 : l1_group_1(1397 ^ []), 706 : -(v3_struct_0(1406 ^ [])), 706 : v3_group_1(1406 ^ []), 706 : v4_group_1(1406 ^ []), 706 : l1_group_1(1406 ^ []), 706 : v1_funct_1(1415 ^ []), 706 : v1_funct_2(1415 ^ [], u1_struct_0(1397 ^ []), u1_struct_0(1406 ^ [])), 706 : m1_relset_1(1415 ^ [], u1_struct_0(1397 ^ []), u1_struct_0(1406 ^ []))],extension(662 ^ 1,bind([[_226951, _226953, _226955], [1415 ^ [], 1406 ^ [], 1397 ^ []]]))).
% 0.48/1.40 ncf('1.1.1',plain,[v1_funct_1(k3_latsubgr(1397 ^ [], 1406 ^ [], 1415 ^ [])), 1194 : v1_funct_2(k3_latsubgr(1397 ^ [], 1406 ^ [], 1415 ^ []), u1_struct_0(k11_group_4(1397 ^ [])), u1_struct_0(k11_group_4(1406 ^ []))), 1194 : m2_relset_1(k3_latsubgr(1397 ^ [], 1406 ^ [], 1415 ^ []), u1_struct_0(k11_group_4(1397 ^ [])), u1_struct_0(k11_group_4(1406 ^ []))), 1214 : -(m1_lattice4(k3_latsubgr(1397 ^ [], 1406 ^ [], 1415 ^ []), k11_group_4(1397 ^ []), k11_group_4(1406 ^ []))), 1214 : m4_vectsp_8(k3_latsubgr(1397 ^ [], 1406 ^ [], 1415 ^ []), k11_group_4(1397 ^ []), k11_group_4(1406 ^ [])), 1214 : m3_vectsp_8(k3_latsubgr(1397 ^ [], 1406 ^ [], 1415 ^ []), k11_group_4(1397 ^ []), k11_group_4(1406 ^ [])), 1194 : -(v3_struct_0(k11_group_4(1406 ^ []))), 1194 : v10_lattices(k11_group_4(1406 ^ [])), 1194 : l3_lattices(k11_group_4(1406 ^ [])), 1182 : -(v3_struct_0(k11_group_4(1397 ^ []))), 1182 : v10_lattices(k11_group_4(1397 ^ [])), 1182 : l3_lattices(k11_group_4(1397 ^ []))],extension(1170 ^ 4,bind([[_242445, _242803, _243153], [k11_group_4(1397 ^ []), k11_group_4(1406 ^ []), k3_latsubgr(1397 ^ [], 1406 ^ [], 1415 ^ [])]]))).
% 0.48/1.40 ncf('1.1.1.1',plain,[-(v1_funct_2(k3_latsubgr(1397 ^ [], 1406 ^ [], 1415 ^ []), u1_struct_0(k11_group_4(1397 ^ [])), u1_struct_0(k11_group_4(1406 ^ []))))],extension(708 ^ 9)).
% 0.48/1.40 ncf('1.1.1.2',plain,[-(m2_relset_1(k3_latsubgr(1397 ^ [], 1406 ^ [], 1415 ^ []), u1_struct_0(k11_group_4(1397 ^ [])), u1_struct_0(k11_group_4(1406 ^ []))))],extension(710 ^ 9)).
% 0.48/1.40 ncf('1.1.1.3',plain,[m1_lattice4(k3_latsubgr(1397 ^ [], 1406 ^ [], 1415 ^ []), k11_group_4(1397 ^ []), k11_group_4(1406 ^ []))],extension(1427 ^ 11)).
% 0.48/1.40 ncf('1.1.1.4',plain,[-(m4_vectsp_8(k3_latsubgr(1397 ^ [], 1406 ^ [], 1415 ^ []), k11_group_4(1397 ^ []), k11_group_4(1406 ^ []))), 1326 : v1_funct_1(1415 ^ []), 1326 : v1_funct_2(1415 ^ [], u1_struct_0(1397 ^ []), u1_struct_0(1406 ^ [])), 1326 : v1_group_6(1415 ^ [], 1397 ^ [], 1406 ^ []), 1326 : m2_relset_1(1415 ^ [], u1_struct_0(1397 ^ []), u1_struct_0(1406 ^ [])), 1326 : -(v3_struct_0(1406 ^ [])), 1326 : v3_group_1(1406 ^ []), 1326 : v4_group_1(1406 ^ []), 1326 : l1_group_1(1406 ^ []), 1310 : -(v3_struct_0(1397 ^ [])), 1310 : v3_group_1(1397 ^ []), 1310 : v4_group_1(1397 ^ []), 1310 : l1_group_1(1397 ^ [])],extension(1294 ^ 11,bind([[_246059, _246506, _246944], [1397 ^ [], 1406 ^ [], 1415 ^ []]]))).
% 0.48/1.40 ncf('1.1.1.4.1',plain,[-(v1_funct_1(1415 ^ []))],extension(1417 ^ 16)).
% 0.48/1.40 ncf('1.1.1.4.2',plain,[-(v1_funct_2(1415 ^ [], u1_struct_0(1397 ^ []), u1_struct_0(1406 ^ [])))],extension(1419 ^ 16)).
% 0.48/1.40 ncf('1.1.1.4.3',plain,[-(v1_group_6(1415 ^ [], 1397 ^ [], 1406 ^ []))],extension(1421 ^ 16)).
% 0.48/1.40 ncf('1.1.1.4.4',plain,[-(m2_relset_1(1415 ^ [], u1_struct_0(1397 ^ []), u1_struct_0(1406 ^ [])))],extension(1423 ^ 16)).
% 0.48/1.40 ncf('1.1.1.4.5',plain,[v3_struct_0(1406 ^ [])],extension(1408 ^ 14)).
% 0.48/1.40 ncf('1.1.1.4.6',plain,[-(v3_group_1(1406 ^ []))],extension(1410 ^ 14)).
% 0.48/1.40 ncf('1.1.1.4.7',plain,[-(v4_group_1(1406 ^ []))],extension(1412 ^ 14)).
% 0.48/1.40 ncf('1.1.1.4.8',plain,[-(l1_group_1(1406 ^ []))],extension(1414 ^ 14)).
% 0.48/1.40 ncf('1.1.1.4.9',plain,[v3_struct_0(1397 ^ [])],reduction('1')).
% 0.48/1.40 ncf('1.1.1.4.10',plain,[-(v3_group_1(1397 ^ []))],extension(1401 ^ 12)).
% 0.48/1.40 ncf('1.1.1.4.11',plain,[-(v4_group_1(1397 ^ []))],extension(1403 ^ 12)).
% 0.48/1.40 ncf('1.1.1.4.12',plain,[-(l1_group_1(1397 ^ []))],extension(1405 ^ 12)).
% 0.48/1.40 ncf('1.1.1.5',plain,[-(m3_vectsp_8(k3_latsubgr(1397 ^ [], 1406 ^ [], 1415 ^ []), k11_group_4(1397 ^ []), k11_group_4(1406 ^ []))), 1272 : v2_funct_1(1415 ^ []), 1272 : v1_funct_1(1415 ^ []), 1272 : v1_funct_2(1415 ^ [], u1_struct_0(1397 ^ []), u1_struct_0(1406 ^ [])), 1272 : v1_group_6(1415 ^ [], 1397 ^ [], 1406 ^ []), 1272 : m2_relset_1(1415 ^ [], u1_struct_0(1397 ^ []), u1_struct_0(1406 ^ [])), 1272 : -(v3_struct_0(1406 ^ [])), 1272 : v3_group_1(1406 ^ []), 1272 : v4_group_1(1406 ^ []), 1272 : l1_group_1(1406 ^ []), 1256 : -(v3_struct_0(1397 ^ [])), 1256 : v3_group_1(1397 ^ []), 1256 : v4_group_1(1397 ^ []), 1256 : l1_group_1(1397 ^ [])],extension(1240 ^ 11,bind([[_244526, _244978, _245421], [1397 ^ [], 1406 ^ [], 1415 ^ []]]))).
% 0.48/1.40 ncf('1.1.1.5.1',plain,[-(v2_funct_1(1415 ^ []))],extension(1425 ^ 16)).
% 0.48/1.40 ncf('1.1.1.5.2',plain,[-(v1_funct_1(1415 ^ []))],extension(1417 ^ 16)).
% 0.48/1.40 ncf('1.1.1.5.3',plain,[-(v1_funct_2(1415 ^ [], u1_struct_0(1397 ^ []), u1_struct_0(1406 ^ [])))],extension(1419 ^ 16)).
% 0.48/1.40 ncf('1.1.1.5.4',plain,[-(v1_group_6(1415 ^ [], 1397 ^ [], 1406 ^ []))],extension(1421 ^ 16)).
% 0.48/1.40 ncf('1.1.1.5.5',plain,[-(m2_relset_1(1415 ^ [], u1_struct_0(1397 ^ []), u1_struct_0(1406 ^ [])))],extension(1423 ^ 16)).
% 0.48/1.40 ncf('1.1.1.5.6',plain,[v3_struct_0(1406 ^ [])],extension(1408 ^ 14)).
% 0.48/1.40 ncf('1.1.1.5.7',plain,[-(v3_group_1(1406 ^ []))],extension(1410 ^ 14)).
% 0.48/1.40 ncf('1.1.1.5.8',plain,[-(v4_group_1(1406 ^ []))],extension(1412 ^ 14)).
% 0.48/1.40 ncf('1.1.1.5.9',plain,[-(l1_group_1(1406 ^ []))],extension(1414 ^ 14)).
% 0.48/1.40 ncf('1.1.1.5.10',plain,[v3_struct_0(1397 ^ [])],reduction('1')).
% 0.48/1.40 ncf('1.1.1.5.11',plain,[-(v3_group_1(1397 ^ []))],extension(1401 ^ 12)).
% 0.48/1.40 ncf('1.1.1.5.12',plain,[-(v4_group_1(1397 ^ []))],extension(1403 ^ 12)).
% 0.48/1.40 ncf('1.1.1.5.13',plain,[-(l1_group_1(1397 ^ []))],extension(1405 ^ 12)).
% 0.48/1.40 ncf('1.1.1.6',plain,[v3_struct_0(k11_group_4(1406 ^ [])), -(v3_struct_0(1406 ^ [])), v3_group_1(1406 ^ []), v4_group_1(1406 ^ []), l1_group_1(1406 ^ [])],extension(620 ^ 7,bind([[_225900], [1406 ^ []]]))).
% 0.48/1.40 ncf('1.1.1.6.1',plain,[v3_struct_0(1406 ^ [])],extension(1408 ^ 8)).
% 0.48/1.40 ncf('1.1.1.6.2',plain,[-(v3_group_1(1406 ^ []))],extension(1410 ^ 8)).
% 0.48/1.40 ncf('1.1.1.6.3',plain,[-(v4_group_1(1406 ^ []))],extension(1412 ^ 8)).
% 0.48/1.40 ncf('1.1.1.6.4',plain,[-(l1_group_1(1406 ^ []))],extension(1414 ^ 8)).
% 0.48/1.40 ncf('1.1.1.7',plain,[-(v10_lattices(k11_group_4(1406 ^ []))), -(v3_struct_0(1406 ^ [])), v3_group_1(1406 ^ []), v4_group_1(1406 ^ []), l1_group_1(1406 ^ [])],extension(620 ^ 7,bind([[_225900], [1406 ^ []]]))).
% 0.48/1.40 ncf('1.1.1.7.1',plain,[v3_struct_0(1406 ^ [])],extension(1408 ^ 8)).
% 0.48/1.40 ncf('1.1.1.7.2',plain,[-(v3_group_1(1406 ^ []))],extension(1410 ^ 8)).
% 0.48/1.40 ncf('1.1.1.7.3',plain,[-(v4_group_1(1406 ^ []))],extension(1412 ^ 8)).
% 0.48/1.40 ncf('1.1.1.7.4',plain,[-(l1_group_1(1406 ^ []))],extension(1414 ^ 8)).
% 0.48/1.40 ncf('1.1.1.8',plain,[-(l3_lattices(k11_group_4(1406 ^ []))), -(v3_struct_0(1406 ^ [])), v3_group_1(1406 ^ []), v4_group_1(1406 ^ []), l1_group_1(1406 ^ [])],extension(620 ^ 7,bind([[_225900], [1406 ^ []]]))).
% 0.48/1.40 ncf('1.1.1.8.1',plain,[v3_struct_0(1406 ^ [])],extension(1408 ^ 8)).
% 0.48/1.40 ncf('1.1.1.8.2',plain,[-(v3_group_1(1406 ^ []))],extension(1410 ^ 8)).
% 0.48/1.40 ncf('1.1.1.8.3',plain,[-(v4_group_1(1406 ^ []))],extension(1412 ^ 8)).
% 0.48/1.40 ncf('1.1.1.8.4',plain,[-(l1_group_1(1406 ^ []))],extension(1414 ^ 8)).
% 0.48/1.40 ncf('1.1.1.9',plain,[v3_struct_0(k11_group_4(1397 ^ [])), -(v3_struct_0(1397 ^ [])), v3_group_1(1397 ^ []), v4_group_1(1397 ^ []), l1_group_1(1397 ^ [])],extension(620 ^ 5,bind([[_225900], [1397 ^ []]]))).
% 0.48/1.40 ncf('1.1.1.9.1',plain,[v3_struct_0(1397 ^ [])],reduction('1')).
% 0.48/1.40 ncf('1.1.1.9.2',plain,[-(v3_group_1(1397 ^ []))],extension(1401 ^ 6)).
% 0.48/1.40 ncf('1.1.1.9.3',plain,[-(v4_group_1(1397 ^ []))],extension(1403 ^ 6)).
% 0.48/1.40 ncf('1.1.1.9.4',plain,[-(l1_group_1(1397 ^ []))],extension(1405 ^ 6)).
% 0.48/1.40 ncf('1.1.1.10',plain,[-(v10_lattices(k11_group_4(1397 ^ []))), -(v3_struct_0(1397 ^ [])), v3_group_1(1397 ^ []), v4_group_1(1397 ^ []), l1_group_1(1397 ^ [])],extension(620 ^ 5,bind([[_225900], [1397 ^ []]]))).
% 0.48/1.40 ncf('1.1.1.10.1',plain,[v3_struct_0(1397 ^ [])],reduction('1')).
% 0.48/1.40 ncf('1.1.1.10.2',plain,[-(v3_group_1(1397 ^ []))],extension(1401 ^ 6)).
% 0.48/1.40 ncf('1.1.1.10.3',plain,[-(v4_group_1(1397 ^ []))],extension(1403 ^ 6)).
% 0.48/1.40 ncf('1.1.1.10.4',plain,[-(l1_group_1(1397 ^ []))],extension(1405 ^ 6)).
% 0.48/1.40 ncf('1.1.1.11',plain,[-(l3_lattices(k11_group_4(1397 ^ []))), -(v3_struct_0(1397 ^ [])), v3_group_1(1397 ^ []), v4_group_1(1397 ^ []), l1_group_1(1397 ^ [])],extension(620 ^ 5,bind([[_225900], [1397 ^ []]]))).
% 0.48/1.40 ncf('1.1.1.11.1',plain,[v3_struct_0(1397 ^ [])],reduction('1')).
% 0.48/1.40 ncf('1.1.1.11.2',plain,[-(v3_group_1(1397 ^ []))],extension(1401 ^ 6)).
% 0.48/1.40 ncf('1.1.1.11.3',plain,[-(v4_group_1(1397 ^ []))],extension(1403 ^ 6)).
% 0.48/1.40 ncf('1.1.1.11.4',plain,[-(l1_group_1(1397 ^ []))],extension(1405 ^ 6)).
% 0.48/1.40 ncf('1.1.2',plain,[-(v3_group_1(1397 ^ []))],extension(1401 ^ 2)).
% 0.48/1.40 ncf('1.1.3',plain,[-(v4_group_1(1397 ^ []))],extension(1403 ^ 2)).
% 0.48/1.40 ncf('1.1.4',plain,[-(l1_group_1(1397 ^ []))],extension(1405 ^ 2)).
% 0.48/1.40 ncf('1.1.5',plain,[v3_struct_0(1406 ^ [])],extension(1408 ^ 2)).
% 0.48/1.40 ncf('1.1.6',plain,[-(v3_group_1(1406 ^ []))],extension(1410 ^ 2)).
% 0.48/1.40 ncf('1.1.7',plain,[-(v4_group_1(1406 ^ []))],extension(1412 ^ 2)).
% 0.48/1.40 ncf('1.1.8',plain,[-(l1_group_1(1406 ^ []))],extension(1414 ^ 2)).
% 0.48/1.40 ncf('1.1.9',plain,[-(v1_funct_1(1415 ^ []))],extension(1417 ^ 2)).
% 0.48/1.40 ncf('1.1.10',plain,[-(v1_funct_2(1415 ^ [], u1_struct_0(1397 ^ []), u1_struct_0(1406 ^ [])))],extension(1419 ^ 2)).
% 0.48/1.40 ncf('1.1.11',plain,[-(m1_relset_1(1415 ^ [], u1_struct_0(1397 ^ []), u1_struct_0(1406 ^ []))), m2_relset_1(1415 ^ [], u1_struct_0(1397 ^ []), u1_struct_0(1406 ^ []))],extension(1156 ^ 2,bind([[_241971, _241973, _241975], [1415 ^ [], u1_struct_0(1406 ^ []), u1_struct_0(1397 ^ [])]]))).
% 0.48/1.40 ncf('1.1.11.1',plain,[-(m2_relset_1(1415 ^ [], u1_struct_0(1397 ^ []), u1_struct_0(1406 ^ [])))],extension(1423 ^ 3)).
% 0.48/1.40 %-----------------------------------------------------
% 0.48/1.40 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------