%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : ALG214+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n007.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 10:08:13 EDT 2023
% Result : Theorem 12.97s 12.75s
% Output : Proof 12.97s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : ALG214+1 : TPTP v8.1.2. Released v3.4.0.
% 0.00/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n007.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 18 23:10:38 EDT 2023
% 0.13/0.33 % CPUTime :
% 12.97/12.75
% 12.97/12.75 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 12.97/12.75 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.97/12.75 %-----------------------------------------------------
% 12.97/12.75 ncf(matrix, plain, [(1844 ^ _248294) ^ [] : [v3_struct_0(1842 ^ [])], (1846 ^ _248294) ^ [] : [-(v3_rlvect_1(1842 ^ []))], (1848 ^ _248294) ^ [] : [-(v4_rlvect_1(1842 ^ []))], (1850 ^ _248294) ^ [] : [-(v5_rlvect_1(1842 ^ []))], (1852 ^ _248294) ^ [] : [-(v6_rlvect_1(1842 ^ []))], (1854 ^ _248294) ^ [] : [-(v4_group_1(1842 ^ []))], (1856 ^ _248294) ^ [] : [-(v6_vectsp_1(1842 ^ []))], (1858 ^ _248294) ^ [] : [-(v7_vectsp_1(1842 ^ []))], (1860 ^ _248294) ^ [] : [-(v8_vectsp_1(1842 ^ []))], (1862 ^ _248294) ^ [] : [-(l3_vectsp_1(1842 ^ []))], (1865 ^ _248294) ^ [] : [v3_struct_0(1863 ^ [])], (1867 ^ _248294) ^ [] : [-(v3_rlvect_1(1863 ^ []))], (1869 ^ _248294) ^ [] : [-(v4_rlvect_1(1863 ^ []))], (1871 ^ _248294) ^ [] : [-(v5_rlvect_1(1863 ^ []))], (1873 ^ _248294) ^ [] : [-(v6_rlvect_1(1863 ^ []))], (1875 ^ _248294) ^ [] : [-(v5_vectsp_2(1863 ^ [], 1842 ^ []))], (1877 ^ _248294) ^ [] : [-(l1_vectsp_2(1863 ^ [], 1842 ^ []))], (1880 ^ _248294) ^ [] : [-(m1_subset_1(1878 ^ [], k1_zfmisc_1(u1_struct_0(1863 ^ []))))], (1883 ^ _248294) ^ [] : [-(m1_subset_1(1881 ^ [], k1_zfmisc_1(u1_struct_0(1863 ^ []))))], (1885 ^ _248294) ^ [] : [-(r1_tarski(1878 ^ [], 1881 ^ []))], (1887 ^ _248294) ^ [] : [-(v1_rmod_5(1881 ^ [], 1842 ^ [], 1863 ^ []))], (1889 ^ _248294) ^ [] : [v1_rmod_5(1878 ^ [], 1842 ^ [], 1863 ^ [])], (452 ^ _248294) ^ [_262920, _262922, _262924, _262926, _262928, _262930] : [-(k2_rmod_4(_262930, _262926, _262922) = k2_rmod_4(_262928, _262924, _262920)), _262930 = _262928, _262926 = _262924, _262922 = _262920], (466 ^ _248294) ^ [_263436, _263438, _263440, _263442, _263444, _263446] : [-(k5_rmod_4(_263446, _263442, _263438) = k5_rmod_4(_263444, _263440, _263436)), _263446 = _263444, _263442 = _263440, _263438 = _263436], (480 ^ _248294) ^ [_263924, _263926, _263928, _263930] : [-(k2_zfmisc_1(_263930, _263926) = k2_zfmisc_1(_263928, _263924)), _263930 = _263928, _263926 = _263924], (490 ^ _248294) ^ [_264311, _264313, _264315, _264317, _264319, _264321] : [-(a_3_0_rmod_4(_264321, _264317, _264313) = a_3_0_rmod_4(_264319, _264315, _264311)), _264321 = _264319, _264317 = _264315, _264313 = _264311], (504 ^ _248294) ^ [_264771, _264773] : [_264773 = _264771, -(k1_rlvect_1(_264773) = k1_rlvect_1(_264771))], (510 ^ _248294) ^ [_265017, _265019, _265021, _265023] : [-(k1_fraenkel(_265023, _265019) = k1_fraenkel(_265021, _265017)), _265023 = _265021, _265019 = _265017], (520 ^ _248294) ^ [_265376, _265378, _265380, _265382] : [-(k1_funct_2(_265382, _265378) = k1_funct_2(_265380, _265376)), _265382 = _265380, _265378 = _265376], (530 ^ _248294) ^ [_265791, _265793, _265795, _265797, _265799, _265801, _265803, _265805] : [-(k8_funct_2(_265805, _265801, _265797, _265793) = k8_funct_2(_265803, _265799, _265795, _265791)), _265805 = _265803, _265801 = _265799, _265797 = _265795, _265793 = _265791], (548 ^ _248294) ^ [_266424, _266426, _266428, _266430] : [-(k1_funct_1(_266430, _266426) = k1_funct_1(_266428, _266424)), _266430 = _266428, _266426 = _266424], (558 ^ _248294) ^ [_266755, _266757] : [_266757 = _266755, -(k1_zfmisc_1(_266757) = k1_zfmisc_1(_266755))], (564 ^ _248294) ^ [_266953, _266955] : [_266955 = _266953, -(u1_struct_0(_266955) = u1_struct_0(_266953))], (2 ^ _248294) ^ [_248438] : [-(_248438 = _248438)], (4 ^ _248294) ^ [_248545, _248547] : [_248547 = _248545, -(_248545 = _248547)], (10 ^ _248294) ^ [_248749, _248751, _248753] : [-(_248753 = _248749), _248753 = _248751, _248751 = _248749], (20 ^ _248294) ^ [_249062, _249064] : [-(v1_relat_1(_249062)), _249064 = _249062, v1_relat_1(_249064)], (30 ^ _248294) ^ [_249357, _249359] : [-(v1_fraenkel(_249357)), _249359 = _249357, v1_fraenkel(_249359)], (40 ^ _248294) ^ [_249652, _249654] : [-(l1_group_1(_249652)), _249654 = _249652, l1_group_1(_249654)], (50 ^ _248294) ^ [_249947, _249949] : [-(l1_rlvect_1(_249947)), _249949 = _249947, l1_rlvect_1(_249949)], (60 ^ _248294) ^ [_250242, _250244] : [-(l1_vectsp_1(_250242)), _250244 = _250242, l1_vectsp_1(_250244)], (70 ^ _248294) ^ [_250537, _250539] : [-(l2_vectsp_1(_250537)), _250539 = _250537, l2_vectsp_1(_250539)], (80 ^ _248294) ^ [_250888, _250890, _250892, _250894, _250896, _250898] : [-(m1_rmod_4(_250896, _250892, _250888)), m1_rmod_4(_250898, _250894, _250890), _250898 = _250896, _250894 = _250892, _250890 = _250888], (98 ^ _248294) ^ [_251441, _251443] : [-(v1_finset_1(_251441)), _251443 = _251441, v1_finset_1(_251443)], (108 ^ _248294) ^ [_251736, _251738] : [-(l2_struct_0(_251736)), _251738 = _251736, l2_struct_0(_251738)], (118 ^ _248294) ^ [_252031, _252033] : [-(l1_struct_0(_252031)), _252033 = _252031, l1_struct_0(_252033)], (128 ^ _248294) ^ [_252326, _252328] : [-(v1_funct_1(_252326)), _252328 = _252326, v1_funct_1(_252328)], (138 ^ _248294) ^ [_252677, _252679, _252681, _252683, _252685, _252687] : [-(v1_funct_2(_252685, _252681, _252677)), v1_funct_2(_252687, _252683, _252679), _252687 = _252685, _252683 = _252681, _252679 = _252677], (156 ^ _248294) ^ [_253286, _253288, _253290, _253292, _253294, _253296] : [-(m1_fraenkel(_253294, _253290, _253286)), m1_fraenkel(_253296, _253292, _253288), _253296 = _253294, _253292 = _253290, _253288 = _253286], (174 ^ _248294) ^ [_253923, _253925, _253927, _253929, _253931, _253933, _253935, _253937] : [-(m2_fraenkel(_253935, _253931, _253927, _253923)), m2_fraenkel(_253937, _253933, _253929, _253925), _253937 = _253935, _253933 = _253931, _253929 = _253927, _253925 = _253923], (196 ^ _248294) ^ [_254685, _254687, _254689, _254691, _254693, _254695] : [-(m2_relset_1(_254693, _254689, _254685)), m2_relset_1(_254695, _254691, _254687), _254695 = _254693, _254691 = _254689, _254687 = _254685], (214 ^ _248294) ^ [_255294, _255296, _255298, _255300, _255302, _255304] : [-(m1_relset_1(_255302, _255298, _255294)), m1_relset_1(_255304, _255300, _255296), _255304 = _255302, _255300 = _255298, _255296 = _255294], (232 ^ _248294) ^ [_255931, _255933, _255935, _255937, _255939, _255941, _255943, _255945] : [-(m2_rmod_4(_255943, _255939, _255935, _255931)), m2_rmod_4(_255945, _255941, _255937, _255933), _255945 = _255943, _255941 = _255939, _255937 = _255935, _255933 = _255931], (254 ^ _248294) ^ [_256665, _256667, _256669, _256671] : [-(r2_hidden(_256669, _256665)), r2_hidden(_256671, _256667), _256671 = _256669, _256667 = _256665], (268 ^ _248294) ^ [_257081, _257083] : [-(v1_xboole_0(_257081)), _257083 = _257081, v1_xboole_0(_257083)], (278 ^ _248294) ^ [_257376, _257378] : [-(v4_group_1(_257376)), _257378 = _257376, v4_group_1(_257378)], (288 ^ _248294) ^ [_257671, _257673] : [-(v6_vectsp_1(_257671)), _257673 = _257671, v6_vectsp_1(_257673)], (298 ^ _248294) ^ [_257966, _257968] : [-(v7_vectsp_1(_257966)), _257968 = _257966, v7_vectsp_1(_257968)], (308 ^ _248294) ^ [_258261, _258263] : [-(v8_vectsp_1(_258261)), _258263 = _258261, v8_vectsp_1(_258263)], (318 ^ _248294) ^ [_258556, _258558] : [-(l3_vectsp_1(_258556)), _258558 = _258556, l3_vectsp_1(_258558)], (328 ^ _248294) ^ [_258851, _258853] : [-(v3_struct_0(_258851)), _258853 = _258851, v3_struct_0(_258853)], (338 ^ _248294) ^ [_259146, _259148] : [-(v3_rlvect_1(_259146)), _259148 = _259146, v3_rlvect_1(_259148)], (348 ^ _248294) ^ [_259441, _259443] : [-(v4_rlvect_1(_259441)), _259443 = _259441, v4_rlvect_1(_259443)], (358 ^ _248294) ^ [_259736, _259738] : [-(v5_rlvect_1(_259736)), _259738 = _259736, v5_rlvect_1(_259738)], (368 ^ _248294) ^ [_260031, _260033] : [-(v6_rlvect_1(_260031)), _260033 = _260031, v6_rlvect_1(_260033)], (378 ^ _248294) ^ [_260354, _260356, _260358, _260360] : [-(v5_vectsp_2(_260358, _260354)), v5_vectsp_2(_260360, _260356), _260360 = _260358, _260356 = _260354], (392 ^ _248294) ^ [_260798, _260800, _260802, _260804] : [-(l1_vectsp_2(_260802, _260798)), l1_vectsp_2(_260804, _260800), _260804 = _260802, _260800 = _260798], (406 ^ _248294) ^ [_261242, _261244, _261246, _261248] : [-(m1_subset_1(_261246, _261242)), m1_subset_1(_261248, _261244), _261248 = _261246, _261244 = _261242], (420 ^ _248294) ^ [_261686, _261688, _261690, _261692] : [-(r1_tarski(_261690, _261686)), r1_tarski(_261692, _261688), _261692 = _261690, _261688 = _261686], (434 ^ _248294) ^ [_262138, _262140, _262142, _262144, _262146, _262148] : [-(v1_rmod_5(_262146, _262142, _262138)), v1_rmod_5(_262148, _262144, _262140), _262148 = _262146, _262144 = _262142, _262140 = _262138], (570 ^ _248294) ^ [_267218, _267220] : [r2_hidden(_267220, _267218), r2_hidden(_267218, _267220)], (576 ^ _248294) ^ [_267443, _267445, _267447] : [m1_subset_1(_267443, k1_zfmisc_1(k2_zfmisc_1(_267447, _267445))), -(v1_relat_1(_267443))], (582 ^ _248294) ^ [_267653] : [-(v3_struct_0(_267653)), v3_rlvect_1(_267653), v4_rlvect_1(_267653), v5_rlvect_1(_267653), v6_rlvect_1(_267653), v4_group_1(_267653), v6_vectsp_1(_267653), v7_vectsp_1(_267653), v8_vectsp_1(_267653), l3_vectsp_1(_267653), 621 ^ _248294 : [(622 ^ _248294) ^ [_268618] : [-(v3_struct_0(_268618)), v3_rlvect_1(_268618), v4_rlvect_1(_268618), v5_rlvect_1(_268618), v6_rlvect_1(_268618), v5_vectsp_2(_268618, _267653), l1_vectsp_2(_268618, _267653), 649 ^ _248294 : [(650 ^ _248294) ^ [_269324] : [m1_subset_1(_269324, k1_zfmisc_1(u1_struct_0(_268618))), 653 ^ _248294 : [(668 ^ _248294) ^ [] : [670 ^ _248294 : [(671 ^ _248294) ^ [] : [-(m2_rmod_4(669 ^ [_267653, _268618, _269324], _267653, _268618, _269324))], (673 ^ _248294) ^ [] : [-(k5_rmod_4(_267653, _268618, 669 ^ [_267653, _268618, _269324]) = k1_rlvect_1(_268618))], (675 ^ _248294) ^ [] : [k2_rmod_4(_267653, _268618, 669 ^ [_267653, _268618, _269324]) = k1_xboole_0]], -(v1_rmod_5(_269324, _267653, _268618))], (654 ^ _248294) ^ [] : [v1_rmod_5(_269324, _267653, _268618), 657 ^ _248294 : [(658 ^ _248294) ^ [_269615] : [m2_rmod_4(_269615, _267653, _268618, _269324), k5_rmod_4(_267653, _268618, _269615) = k1_rlvect_1(_268618), -(k2_rmod_4(_267653, _268618, _269615) = k1_xboole_0)]]]]]]]]], (679 ^ _248294) ^ [_270391] : [718 ^ _248294 : [(719 ^ _248294) ^ [_271325] : [746 ^ _248294 : [(747 ^ _248294) ^ [_272000] : [m1_rmod_4(_272000, _270391, _271325), -(k2_rmod_4(_270391, _271325, _272000) = a_3_0_rmod_4(_270391, _271325, _272000))]], -(v3_struct_0(_271325)), v3_rlvect_1(_271325), v4_rlvect_1(_271325), v5_rlvect_1(_271325), v6_rlvect_1(_271325), v5_vectsp_2(_271325, _270391), l1_vectsp_2(_271325, _270391)]], -(v3_struct_0(_270391)), v3_rlvect_1(_270391), v4_rlvect_1(_270391), v5_rlvect_1(_270391), v6_rlvect_1(_270391), v4_group_1(_270391), v6_vectsp_1(_270391), v7_vectsp_1(_270391), v8_vectsp_1(_270391), l3_vectsp_1(_270391)], (753 ^ _248294) ^ [_272248, _272250] : [-(v1_xboole_0(_272248)), -(m1_fraenkel(k1_fraenkel(_272250, _272248), _272250, _272248))], (759 ^ _248294) ^ [] : [true___, -(true___)], (765 ^ _248294) ^ [] : [true___, -(true___)], (771 ^ _248294) ^ [_272691] : [l2_struct_0(_272691), -(m1_subset_1(k1_rlvect_1(_272691), u1_struct_0(_272691)))], (777 ^ _248294) ^ [] : [true___, -(true___)], (783 ^ _248294) ^ [] : [true___, -(true___)], (789 ^ _248294) ^ [_273153, _273155, _273157] : [860 ^ _248294 : [(861 ^ _248294) ^ [] : [-(v1_finset_1(k2_rmod_4(_273157, _273155, _273153)))], (863 ^ _248294) ^ [] : [-(m1_subset_1(k2_rmod_4(_273157, _273155, _273153), k1_zfmisc_1(u1_struct_0(_273155))))]], -(v3_struct_0(_273157)), v3_rlvect_1(_273157), v4_rlvect_1(_273157), v5_rlvect_1(_273157), v6_rlvect_1(_273157), v4_group_1(_273157), v6_vectsp_1(_273157), v7_vectsp_1(_273157), v8_vectsp_1(_273157), l3_vectsp_1(_273157), -(v3_struct_0(_273155)), v3_rlvect_1(_273155), v4_rlvect_1(_273155), v5_rlvect_1(_273155), v6_rlvect_1(_273155), v5_vectsp_2(_273155, _273157), l1_vectsp_2(_273155, _273157), m1_rmod_4(_273153, _273157, _273155)], (865 ^ _248294) ^ [] : [true___, -(true___)], (871 ^ _248294) ^ [_275160, _275162, _275164] : [-(m1_subset_1(k5_rmod_4(_275164, _275162, _275160), u1_struct_0(_275162))), -(v3_struct_0(_275164)), v3_rlvect_1(_275164), v4_rlvect_1(_275164), v5_rlvect_1(_275164), v6_rlvect_1(_275164), v4_group_1(_275164), v6_vectsp_1(_275164), v7_vectsp_1(_275164), v8_vectsp_1(_275164), l3_vectsp_1(_275164), -(v3_struct_0(_275162)), v3_rlvect_1(_275162), v4_rlvect_1(_275162), v5_rlvect_1(_275162), v6_rlvect_1(_275162), v5_vectsp_2(_275162, _275164), l1_vectsp_2(_275162, _275164), m1_rmod_4(_275160, _275164, _275162)], (945 ^ _248294) ^ [_276975, _276977, _276979, _276981] : [-(m1_subset_1(k8_funct_2(_276981, _276979, _276977, _276975), _276979)), -(v1_xboole_0(_276981)), v1_funct_1(_276977), v1_funct_2(_276977, _276981, _276979), m1_relset_1(_276977, _276981, _276979), m1_subset_1(_276975, _276981)], (967 ^ _248294) ^ [_277584] : [l1_group_1(_277584), -(l1_struct_0(_277584))], (973 ^ _248294) ^ [_277770] : [l1_rlvect_1(_277770), -(l2_struct_0(_277770))], (979 ^ _248294) ^ [] : [true___, -(true___)], (985 ^ _248294) ^ [_278075] : [l1_vectsp_1(_278075), -(l1_group_1(_278075))], (991 ^ _248294) ^ [_278261] : [l1_struct_0(_278261), 994 ^ _248294 : [(995 ^ _248294) ^ [_278391] : [l1_vectsp_2(_278391, _278261), -(l1_rlvect_1(_278391))]]], (1001 ^ _248294) ^ [_278592] : [l2_struct_0(_278592), -(l1_struct_0(_278592))], (1007 ^ _248294) ^ [_278778] : [l2_vectsp_1(_278778), 1010 ^ _248294 : [(1011 ^ _248294) ^ [] : [-(l1_vectsp_1(_278778))], (1013 ^ _248294) ^ [] : [-(l2_struct_0(_278778))]]], (1015 ^ _248294) ^ [_279035] : [l3_vectsp_1(_279035), 1018 ^ _248294 : [(1019 ^ _248294) ^ [] : [-(l1_rlvect_1(_279035))], (1021 ^ _248294) ^ [] : [-(l2_vectsp_1(_279035))]]], (1023 ^ _248294) ^ [_279320, _279322, _279324] : [m1_fraenkel(_279320, _279324, _279322), 1026 ^ _248294 : [(1027 ^ _248294) ^ [] : [v1_xboole_0(_279320)], (1029 ^ _248294) ^ [] : [-(v1_fraenkel(_279320))]]], (1031 ^ _248294) ^ [] : [true___, -(true___)], (1037 ^ _248294) ^ [_279731, _279733] : [1104 ^ _248294 : [(1105 ^ _248294) ^ [_281282] : [m1_rmod_4(_281282, _279733, _279731), -(m2_fraenkel(_281282, u1_struct_0(_279731), u1_struct_0(_279733), k1_fraenkel(u1_struct_0(_279731), u1_struct_0(_279733))))]], -(v3_struct_0(_279733)), v3_rlvect_1(_279733), v4_rlvect_1(_279733), v5_rlvect_1(_279733), v6_rlvect_1(_279733), v4_group_1(_279733), v6_vectsp_1(_279733), v7_vectsp_1(_279733), v8_vectsp_1(_279733), l3_vectsp_1(_279733), -(v3_struct_0(_279731)), v3_rlvect_1(_279731), v4_rlvect_1(_279731), v5_rlvect_1(_279731), v6_rlvect_1(_279731), v5_vectsp_2(_279731, _279733), l1_vectsp_2(_279731, _279733)], (1111 ^ _248294) ^ [] : [true___, -(true___)], (1117 ^ _248294) ^ [_281668, _281670, _281672] : [-(v1_xboole_0(_281670)), m1_fraenkel(_281668, _281672, _281670), 1124 ^ _248294 : [(1125 ^ _248294) ^ [_281920] : [m2_fraenkel(_281920, _281672, _281670, _281668), 1128 ^ _248294 : [(1129 ^ _248294) ^ [] : [-(v1_funct_1(_281920))], (1131 ^ _248294) ^ [] : [-(v1_funct_2(_281920, _281672, _281670))], (1133 ^ _248294) ^ [] : [-(m2_relset_1(_281920, _281672, _281670))]]]]], (1135 ^ _248294) ^ [_282332, _282334, _282336] : [m2_relset_1(_282332, _282336, _282334), -(m1_subset_1(_282332, k1_zfmisc_1(k2_zfmisc_1(_282336, _282334))))], (1141 ^ _248294) ^ [_282574, _282576, _282578] : [1212 ^ _248294 : [(1213 ^ _248294) ^ [_284283] : [m2_rmod_4(_284283, _282578, _282576, _282574), -(m1_rmod_4(_284283, _282578, _282576))]], -(v3_struct_0(_282578)), v3_rlvect_1(_282578), v4_rlvect_1(_282578), v5_rlvect_1(_282578), v6_rlvect_1(_282578), v4_group_1(_282578), v6_vectsp_1(_282578), v7_vectsp_1(_282578), v8_vectsp_1(_282578), l3_vectsp_1(_282578), -(v3_struct_0(_282576)), v3_rlvect_1(_282576), v4_rlvect_1(_282576), v5_rlvect_1(_282576), v6_rlvect_1(_282576), v5_vectsp_2(_282576, _282578), l1_vectsp_2(_282576, _282578), m1_subset_1(_282574, k1_zfmisc_1(u1_struct_0(_282576)))], (1219 ^ _248294) ^ [] : [true___, -(true___)], (1226 ^ _248294) ^ [] : [-(l1_group_1(1224 ^ []))], (1229 ^ _248294) ^ [] : [-(l1_rlvect_1(1227 ^ []))], (1232 ^ _248294) ^ [] : [-(l1_struct_0(1230 ^ []))], (1235 ^ _248294) ^ [] : [-(l1_vectsp_1(1233 ^ []))], (1237 ^ _248294) ^ [_284983] : [l1_struct_0(_284983), -(l1_vectsp_2(1240 ^ [_284983], _284983))], (1245 ^ _248294) ^ [] : [-(l2_struct_0(1243 ^ []))], (1248 ^ _248294) ^ [] : [-(l2_vectsp_1(1246 ^ []))], (1251 ^ _248294) ^ [] : [-(l3_vectsp_1(1249 ^ []))], (1254 ^ _248294) ^ [_285530, _285532] : [-(m1_fraenkel(1252 ^ [_285530, _285532], _285532, _285530))], (1257 ^ _248294) ^ [_285674, _285676] : [-(m1_relset_1(1255 ^ [_285674, _285676], _285676, _285674))], (1259 ^ _248294) ^ [_285791, _285793] : [-(m1_rmod_4(1326 ^ [_285791, _285793], _285793, _285791)), -(v3_struct_0(_285793)), v3_rlvect_1(_285793), v4_rlvect_1(_285793), v5_rlvect_1(_285793), v6_rlvect_1(_285793), v4_group_1(_285793), v6_vectsp_1(_285793), v7_vectsp_1(_285793), v8_vectsp_1(_285793), l3_vectsp_1(_285793), -(v3_struct_0(_285791)), v3_rlvect_1(_285791), v4_rlvect_1(_285791), v5_rlvect_1(_285791), v6_rlvect_1(_285791), v5_vectsp_2(_285791, _285793), l1_vectsp_2(_285791, _285793)], (1331 ^ _248294) ^ [_287471] : [-(m1_subset_1(1329 ^ [_287471], _287471))], (1333 ^ _248294) ^ [_287597, _287599, _287601] : [-(m2_fraenkel(1340 ^ [_287597, _287599, _287601], _287601, _287599, _287597)), -(v1_xboole_0(_287599)), m1_fraenkel(_287597, _287601, _287599)], (1345 ^ _248294) ^ [_288005, _288007] : [-(m2_relset_1(1343 ^ [_288005, _288007], _288007, _288005))], (1347 ^ _248294) ^ [_288136, _288138, _288140] : [-(m2_rmod_4(1418 ^ [_288136, _288138, _288140], _288140, _288138, _288136)), -(v3_struct_0(_288140)), v3_rlvect_1(_288140), v4_rlvect_1(_288140), v5_rlvect_1(_288140), v6_rlvect_1(_288140), v4_group_1(_288140), v6_vectsp_1(_288140), v7_vectsp_1(_288140), v8_vectsp_1(_288140), l3_vectsp_1(_288140), -(v3_struct_0(_288138)), v3_rlvect_1(_288138), v4_rlvect_1(_288138), v5_rlvect_1(_288138), v6_rlvect_1(_288138), v5_vectsp_2(_288138, _288140), l1_vectsp_2(_288138, _288140), m1_subset_1(_288136, k1_zfmisc_1(u1_struct_0(_288138)))], (1422 ^ _248294) ^ [_289972] : [v1_xboole_0(u1_struct_0(_289972)), -(v3_struct_0(_289972)), l1_struct_0(_289972)], (1432 ^ _248294) ^ [_290233] : [v1_xboole_0(k1_zfmisc_1(_290233))], (1434 ^ _248294) ^ [] : [-(v1_xboole_0(k1_xboole_0))], (1436 ^ _248294) ^ [_290394, _290396] : [v1_xboole_0(k2_zfmisc_1(_290396, _290394)), -(v1_xboole_0(_290396)), -(v1_xboole_0(_290394))], (1446 ^ _248294) ^ [_290728, _290730, _290732, _290734] : [1517 ^ _248294 : [(1518 ^ _248294) ^ [] : [r2_hidden(_290734, a_3_0_rmod_4(_290732, _290730, _290728)), 1522 ^ _248294 : [(1523 ^ _248294) ^ [] : [-(m1_subset_1(1521 ^ [_290728, _290730, _290732, _290734], u1_struct_0(_290730)))], (1525 ^ _248294) ^ [] : [-(_290734 = 1521 ^ [_290728, _290730, _290732, _290734])], (1527 ^ _248294) ^ [] : [k8_funct_2(u1_struct_0(_290730), u1_struct_0(_290732), _290728, 1521 ^ [_290728, _290730, _290732, _290734]) = k1_rlvect_1(_290732)]]], (1529 ^ _248294) ^ [] : [-(r2_hidden(_290734, a_3_0_rmod_4(_290732, _290730, _290728))), 1530 ^ _248294 : [(1531 ^ _248294) ^ [_293013] : [m1_subset_1(_293013, u1_struct_0(_290730)), _290734 = _293013, -(k8_funct_2(u1_struct_0(_290730), u1_struct_0(_290732), _290728, _293013) = k1_rlvect_1(_290732))]]]], -(v3_struct_0(_290732)), v3_rlvect_1(_290732), v4_rlvect_1(_290732), v5_rlvect_1(_290732), v6_rlvect_1(_290732), v4_group_1(_290732), v6_vectsp_1(_290732), v7_vectsp_1(_290732), v8_vectsp_1(_290732), l3_vectsp_1(_290732), -(v3_struct_0(_290730)), v3_rlvect_1(_290730), v4_rlvect_1(_290730), v5_rlvect_1(_290730), v6_rlvect_1(_290730), v5_vectsp_2(_290730, _290732), l1_vectsp_2(_290730, _290732), m1_rmod_4(_290728, _290732, _290730)], (1543 ^ _248294) ^ [_293430] : [-(v1_xboole_0(_293430)), 1547 ^ _248294 : [(1548 ^ _248294) ^ [] : [-(m1_subset_1(1546 ^ [_293430], k1_zfmisc_1(_293430)))], (1550 ^ _248294) ^ [] : [v1_xboole_0(1546 ^ [_293430])]]], (1553 ^ _248294) ^ [] : [-(v1_xboole_0(1551 ^ []))], (1555 ^ _248294) ^ [_293851] : [1563 ^ _248294 : [(1564 ^ _248294) ^ [] : [-(m1_subset_1(1562 ^ [_293851], k1_zfmisc_1(u1_struct_0(_293851))))], (1566 ^ _248294) ^ [] : [v1_xboole_0(1562 ^ [_293851])], (1568 ^ _248294) ^ [] : [-(v1_finset_1(1562 ^ [_293851]))]], -(v3_struct_0(_293851)), l1_struct_0(_293851)], (1571 ^ _248294) ^ [_294403] : [-(m1_subset_1(1569 ^ [_294403], k1_zfmisc_1(_294403)))], (1573 ^ _248294) ^ [_294454] : [-(v1_xboole_0(1569 ^ [_294454]))], (1576 ^ _248294) ^ [] : [v1_xboole_0(1574 ^ [])], (1579 ^ _248294) ^ [] : [-(l1_struct_0(1577 ^ []))], (1581 ^ _248294) ^ [] : [v3_struct_0(1577 ^ [])], (1584 ^ _248294) ^ [] : [-(l2_struct_0(1582 ^ []))], (1586 ^ _248294) ^ [] : [v3_struct_0(1582 ^ [])], (1588 ^ _248294) ^ [_294943] : [1596 ^ _248294 : [(1597 ^ _248294) ^ [] : [-(m1_subset_1(1595 ^ [_294943], k1_zfmisc_1(u1_struct_0(_294943))))], (1599 ^ _248294) ^ [] : [v1_xboole_0(1595 ^ [_294943])]], -(v3_struct_0(_294943)), l1_struct_0(_294943)], (1601 ^ _248294) ^ [_295364] : [l1_struct_0(_295364), 1605 ^ _248294 : [(1606 ^ _248294) ^ [] : [-(l1_vectsp_2(1604 ^ [_295364], _295364))], (1608 ^ _248294) ^ [] : [v3_struct_0(1604 ^ [_295364])]]], (1610 ^ _248294) ^ [_295701, _295703] : [-(v1_xboole_0(_295701)), -(k1_fraenkel(_295703, _295701) = k1_funct_2(_295703, _295701))], (1616 ^ _248294) ^ [_295952, _295954, _295956, _295958] : [-(k8_funct_2(_295958, _295956, _295954, _295952) = k1_funct_1(_295954, _295952)), -(v1_xboole_0(_295958)), v1_funct_1(_295954), v1_funct_2(_295954, _295958, _295956), m1_relset_1(_295954, _295958, _295956), m1_subset_1(_295952, _295958)], (1638 ^ _248294) ^ [_296595, _296597, _296599] : [-(v1_xboole_0(_296597)), m1_fraenkel(_296595, _296599, _296597), 1645 ^ _248294 : [(1646 ^ _248294) ^ [_296863] : [m2_fraenkel(_296863, _296599, _296597, _296595), -(m1_subset_1(_296863, _296595))], (1652 ^ _248294) ^ [_297047] : [m1_subset_1(_297047, _296595), -(m2_fraenkel(_297047, _296599, _296597, _296595))]]], (1658 ^ _248294) ^ [_297331, _297333, _297335] : [m2_relset_1(_297331, _297335, _297333), -(m1_relset_1(_297331, _297335, _297333))], (1664 ^ _248294) ^ [_297503, _297505, _297507] : [m1_relset_1(_297503, _297507, _297505), -(m2_relset_1(_297503, _297507, _297505))], (1670 ^ _248294) ^ [_297710, _297712] : [-(r1_tarski(_297712, _297712))], (1672 ^ _248294) ^ [_297819, _297821] : [r2_hidden(_297821, _297819), -(m1_subset_1(_297821, _297819))], (1678 ^ _248294) ^ [_298015] : [-(v3_struct_0(_298015)), v3_rlvect_1(_298015), v4_rlvect_1(_298015), v5_rlvect_1(_298015), v6_rlvect_1(_298015), v4_group_1(_298015), v6_vectsp_1(_298015), v7_vectsp_1(_298015), v8_vectsp_1(_298015), l3_vectsp_1(_298015), 1717 ^ _248294 : [(1718 ^ _248294) ^ [_298980] : [1745 ^ _248294 : [(1746 ^ _248294) ^ [_299686] : [m1_subset_1(_299686, k1_zfmisc_1(u1_struct_0(_298980))), 1749 ^ _248294 : [(1750 ^ _248294) ^ [_299864] : [m1_subset_1(_299864, k1_zfmisc_1(u1_struct_0(_298980))), 1753 ^ _248294 : [(1754 ^ _248294) ^ [_300033] : [m2_rmod_4(_300033, _298015, _298980, _299686), r1_tarski(_299686, _299864), -(m2_rmod_4(_300033, _298015, _298980, _299864))]]]]]], -(v3_struct_0(_298980)), v3_rlvect_1(_298980), v4_rlvect_1(_298980), v5_rlvect_1(_298980), v6_rlvect_1(_298980), v5_vectsp_2(_298980, _298015), l1_vectsp_2(_298980, _298015)]]], (1764 ^ _248294) ^ [_300416, _300418] : [m1_subset_1(_300418, _300416), -(v1_xboole_0(_300416)), -(r2_hidden(_300418, _300416))], (1774 ^ _248294) ^ [_300714, _300716] : [-(_300716 = _300714), 1778 ^ _248294 : [(1779 ^ _248294) ^ [] : [-(r2_hidden(1775 ^ [_300714, _300716], _300716))], (1781 ^ _248294) ^ [] : [r2_hidden(1775 ^ [_300714, _300716], _300714)]], 1782 ^ _248294 : [(1783 ^ _248294) ^ [] : [-(r2_hidden(1775 ^ [_300714, _300716], _300714))], (1785 ^ _248294) ^ [] : [r2_hidden(1775 ^ [_300714, _300716], _300716)]]], (1789 ^ _248294) ^ [_301273, _301275] : [m1_subset_1(_301275, k1_zfmisc_1(_301273)), -(r1_tarski(_301275, _301273))], (1795 ^ _248294) ^ [_301439, _301441] : [r1_tarski(_301441, _301439), -(m1_subset_1(_301441, k1_zfmisc_1(_301439)))], (1801 ^ _248294) ^ [_301669, _301671, _301673] : [-(m1_subset_1(_301673, _301669)), r2_hidden(_301673, _301671), m1_subset_1(_301671, k1_zfmisc_1(_301669))], (1811 ^ _248294) ^ [_301996, _301998, _302000] : [r2_hidden(_302000, _301998), m1_subset_1(_301998, k1_zfmisc_1(_301996)), v1_xboole_0(_301996)], (1821 ^ _248294) ^ [_302292] : [v1_xboole_0(_302292), -(_302292 = k1_xboole_0)], (1827 ^ _248294) ^ [_302494, _302496] : [r2_hidden(_302496, _302494), v1_xboole_0(_302494)], (1833 ^ _248294) ^ [_302681, _302683] : [v1_xboole_0(_302683), -(_302683 = _302681), v1_xboole_0(_302681)]], input).
% 12.97/12.75 ncf('1',plain,[v3_struct_0(1842 ^ [])],start(1844 ^ 0)).
% 12.97/12.75 ncf('1.1',plain,[-(v3_struct_0(1842 ^ [])), v3_rlvect_1(1842 ^ []), v4_rlvect_1(1842 ^ []), v5_rlvect_1(1842 ^ []), v6_rlvect_1(1842 ^ []), v4_group_1(1842 ^ []), v6_vectsp_1(1842 ^ []), v7_vectsp_1(1842 ^ []), v8_vectsp_1(1842 ^ []), l3_vectsp_1(1842 ^ []), 1746 : m1_subset_1(1878 ^ [], k1_zfmisc_1(u1_struct_0(1863 ^ []))), 1750 : m1_subset_1(1878 ^ [], k1_zfmisc_1(u1_struct_0(1863 ^ []))), 1754 : m2_rmod_4(669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []], 1842 ^ [], 1863 ^ [], 1878 ^ []), 1754 : r1_tarski(1878 ^ [], 1878 ^ []), 1754 : -(m2_rmod_4(669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []], 1842 ^ [], 1863 ^ [], 1878 ^ [])), 1746 : -(v3_struct_0(1863 ^ [])), 1746 : v3_rlvect_1(1863 ^ []), 1746 : v4_rlvect_1(1863 ^ []), 1746 : v5_rlvect_1(1863 ^ []), 1746 : v6_rlvect_1(1863 ^ []), 1746 : v5_vectsp_2(1863 ^ [], 1842 ^ []), 1746 : l1_vectsp_2(1863 ^ [], 1842 ^ [])],extension(1678 ^ 1,bind([[_298015, _298980, _299686, _299864, _300033], [1842 ^ [], 1863 ^ [], 1878 ^ [], 1878 ^ [], 669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []]]]))).
% 12.97/12.75 ncf('1.1.1',plain,[-(v3_rlvect_1(1842 ^ []))],extension(1846 ^ 2)).
% 12.97/12.75 ncf('1.1.2',plain,[-(v4_rlvect_1(1842 ^ []))],extension(1848 ^ 2)).
% 12.97/12.75 ncf('1.1.3',plain,[-(v5_rlvect_1(1842 ^ []))],extension(1850 ^ 2)).
% 12.97/12.75 ncf('1.1.4',plain,[-(v6_rlvect_1(1842 ^ []))],extension(1852 ^ 2)).
% 12.97/12.75 ncf('1.1.5',plain,[-(v4_group_1(1842 ^ []))],extension(1854 ^ 2)).
% 12.97/12.75 ncf('1.1.6',plain,[-(v6_vectsp_1(1842 ^ []))],extension(1856 ^ 2)).
% 12.97/12.75 ncf('1.1.7',plain,[-(v7_vectsp_1(1842 ^ []))],extension(1858 ^ 2)).
% 12.97/12.75 ncf('1.1.8',plain,[-(v8_vectsp_1(1842 ^ []))],extension(1860 ^ 2)).
% 12.97/12.75 ncf('1.1.9',plain,[-(l3_vectsp_1(1842 ^ []))],extension(1862 ^ 2)).
% 12.97/12.75 ncf('1.1.10',plain,[-(m1_subset_1(1878 ^ [], k1_zfmisc_1(u1_struct_0(1863 ^ []))))],extension(1880 ^ 6)).
% 12.97/12.75 ncf('1.1.11',plain,[-(m1_subset_1(1878 ^ [], k1_zfmisc_1(u1_struct_0(1863 ^ []))))],extension(1880 ^ 8)).
% 12.97/12.75 ncf('1.1.12',plain,[-(m2_rmod_4(669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []], 1842 ^ [], 1863 ^ [], 1878 ^ [])), m2_rmod_4(669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []], 1842 ^ [], 1863 ^ [], 1878 ^ []), 669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []] = 669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []], 1842 ^ [] = 1842 ^ [], 1863 ^ [] = 1863 ^ [], 1878 ^ [] = 1878 ^ []],extension(232 ^ 10,bind([[_255931, _255933, _255935, _255937, _255939, _255941, _255943, _255945], [1878 ^ [], 1878 ^ [], 1863 ^ [], 1863 ^ [], 1842 ^ [], 1842 ^ [], 669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []], 669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []]]]))).
% 12.97/12.75 ncf('1.1.12.1',plain,[-(m2_rmod_4(669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []], 1842 ^ [], 1863 ^ [], 1878 ^ [])), m2_rmod_4(669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []], 1842 ^ [], 1863 ^ [], 1878 ^ []), 669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []] = 669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []], 1842 ^ [] = 1842 ^ [], 1863 ^ [] = 1863 ^ [], 1878 ^ [] = 1878 ^ []],extension(232 ^ 11,bind([[_255931, _255933, _255935, _255937, _255939, _255941, _255943, _255945], [1878 ^ [], 1878 ^ [], 1863 ^ [], 1863 ^ [], 1842 ^ [], 1842 ^ [], 669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []], 669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []]]]))).
% 12.97/12.75 ncf('1.1.12.1.1',plain,[-(m2_rmod_4(669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []], 1842 ^ [], 1863 ^ [], 1878 ^ [])), 668 : -(v1_rmod_5(1878 ^ [], 1842 ^ [], 1863 ^ [])), 668 : m1_subset_1(1878 ^ [], k1_zfmisc_1(u1_struct_0(1863 ^ []))), 650 : -(v3_struct_0(1863 ^ [])), 650 : v3_rlvect_1(1863 ^ []), 650 : v4_rlvect_1(1863 ^ []), 650 : v5_rlvect_1(1863 ^ []), 650 : v6_rlvect_1(1863 ^ []), 650 : v5_vectsp_2(1863 ^ [], 1842 ^ []), 650 : l1_vectsp_2(1863 ^ [], 1842 ^ []), 622 : -(v3_struct_0(1842 ^ [])), 622 : v3_rlvect_1(1842 ^ []), 622 : v4_rlvect_1(1842 ^ []), 622 : v5_rlvect_1(1842 ^ []), 622 : v6_rlvect_1(1842 ^ []), 622 : v4_group_1(1842 ^ []), 622 : v6_vectsp_1(1842 ^ []), 622 : v7_vectsp_1(1842 ^ []), 622 : v8_vectsp_1(1842 ^ []), 622 : l3_vectsp_1(1842 ^ [])],extension(582 ^ 12,bind([[_267653, _268618, _269324], [1842 ^ [], 1863 ^ [], 1878 ^ []]]))).
% 12.97/12.75 ncf('1.1.12.1.1.1',plain,[v1_rmod_5(1878 ^ [], 1842 ^ [], 1863 ^ [])],extension(1889 ^ 19)).
% 12.97/12.75 ncf('1.1.12.1.1.2',plain,[-(m1_subset_1(1878 ^ [], k1_zfmisc_1(u1_struct_0(1863 ^ []))))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.12.1.1.3',plain,[v3_struct_0(1863 ^ [])],extension(1865 ^ 15)).
% 12.97/12.75 ncf('1.1.12.1.1.4',plain,[-(v3_rlvect_1(1863 ^ []))],extension(1867 ^ 15)).
% 12.97/12.75 ncf('1.1.12.1.1.5',plain,[-(v4_rlvect_1(1863 ^ []))],extension(1869 ^ 15)).
% 12.97/12.75 ncf('1.1.12.1.1.6',plain,[-(v5_rlvect_1(1863 ^ []))],extension(1871 ^ 15)).
% 12.97/12.75 ncf('1.1.12.1.1.7',plain,[-(v6_rlvect_1(1863 ^ []))],extension(1873 ^ 15)).
% 12.97/12.75 ncf('1.1.12.1.1.8',plain,[-(v5_vectsp_2(1863 ^ [], 1842 ^ []))],extension(1875 ^ 15)).
% 12.97/12.75 ncf('1.1.12.1.1.9',plain,[-(l1_vectsp_2(1863 ^ [], 1842 ^ []))],extension(1877 ^ 15)).
% 12.97/12.75 ncf('1.1.12.1.1.10',plain,[v3_struct_0(1842 ^ [])],reduction('1')).
% 12.97/12.75 ncf('1.1.12.1.1.11',plain,[-(v3_rlvect_1(1842 ^ []))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.12.1.1.12',plain,[-(v4_rlvect_1(1842 ^ []))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.12.1.1.13',plain,[-(v5_rlvect_1(1842 ^ []))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.12.1.1.14',plain,[-(v6_rlvect_1(1842 ^ []))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.12.1.1.15',plain,[-(v4_group_1(1842 ^ []))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.12.1.1.16',plain,[-(v6_vectsp_1(1842 ^ []))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.12.1.1.17',plain,[-(v7_vectsp_1(1842 ^ []))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.12.1.1.18',plain,[-(v8_vectsp_1(1842 ^ []))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.12.1.1.19',plain,[-(l3_vectsp_1(1842 ^ []))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.12.1.2',plain,[-(669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []] = 669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []])],extension(2 ^ 12,bind([[_248438], [669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []]]]))).
% 12.97/12.75 ncf('1.1.12.1.3',plain,[-(1842 ^ [] = 1842 ^ [])],extension(2 ^ 12,bind([[_248438], [1842 ^ []]]))).
% 12.97/12.75 ncf('1.1.12.1.4',plain,[-(1863 ^ [] = 1863 ^ [])],extension(2 ^ 12,bind([[_248438], [1863 ^ []]]))).
% 12.97/12.75 ncf('1.1.12.1.5',plain,[-(1878 ^ [] = 1878 ^ [])],extension(2 ^ 12,bind([[_248438], [1878 ^ []]]))).
% 12.97/12.75 ncf('1.1.12.2',plain,[-(669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []] = 669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []])],extension(2 ^ 11,bind([[_248438], [669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []]]]))).
% 12.97/12.75 ncf('1.1.12.3',plain,[-(1842 ^ [] = 1842 ^ [])],extension(2 ^ 11,bind([[_248438], [1842 ^ []]]))).
% 12.97/12.75 ncf('1.1.12.4',plain,[-(1863 ^ [] = 1863 ^ [])],extension(2 ^ 11,bind([[_248438], [1863 ^ []]]))).
% 12.97/12.75 ncf('1.1.12.5',plain,[-(1878 ^ [] = 1878 ^ [])],extension(2 ^ 11,bind([[_248438], [1878 ^ []]]))).
% 12.97/12.75 ncf('1.1.13',plain,[-(r1_tarski(1878 ^ [], 1878 ^ []))],extension(1670 ^ 10,bind([[_297710, _297712], [_176286, 1878 ^ []]]))).
% 12.97/12.75 ncf('1.1.14',plain,[m2_rmod_4(669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []], 1842 ^ [], 1863 ^ [], 1878 ^ []), 1754 : r1_tarski(1878 ^ [], 1881 ^ []), 1754 : -(m2_rmod_4(669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []], 1842 ^ [], 1863 ^ [], 1881 ^ [])), 1754 : m1_subset_1(1881 ^ [], k1_zfmisc_1(u1_struct_0(1863 ^ [])))],extension(1750 ^ 10,bind([[_299864, _300033], [1881 ^ [], 669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []]]]))).
% 12.97/12.75 ncf('1.1.14.1',plain,[-(r1_tarski(1878 ^ [], 1881 ^ []))],extension(1885 ^ 13)).
% 12.97/12.75 ncf('1.1.14.2',plain,[m2_rmod_4(669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []], 1842 ^ [], 1863 ^ [], 1881 ^ []), 658 : k5_rmod_4(1842 ^ [], 1863 ^ [], 669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []]) = k1_rlvect_1(1863 ^ []), 658 : -(k2_rmod_4(1842 ^ [], 1863 ^ [], 669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []]) = k1_xboole_0), 658 : v1_rmod_5(1881 ^ [], 1842 ^ [], 1863 ^ []), 654 : m1_subset_1(1881 ^ [], k1_zfmisc_1(u1_struct_0(1863 ^ []))), 650 : -(v3_struct_0(1863 ^ [])), 650 : v3_rlvect_1(1863 ^ []), 650 : v4_rlvect_1(1863 ^ []), 650 : v5_rlvect_1(1863 ^ []), 650 : v6_rlvect_1(1863 ^ []), 650 : v5_vectsp_2(1863 ^ [], 1842 ^ []), 650 : l1_vectsp_2(1863 ^ [], 1842 ^ []), 622 : -(v3_struct_0(1842 ^ [])), 622 : v3_rlvect_1(1842 ^ []), 622 : v4_rlvect_1(1842 ^ []), 622 : v5_rlvect_1(1842 ^ []), 622 : v6_rlvect_1(1842 ^ []), 622 : v4_group_1(1842 ^ []), 622 : v6_vectsp_1(1842 ^ []), 622 : v7_vectsp_1(1842 ^ []), 622 : v8_vectsp_1(1842 ^ []), 622 : l3_vectsp_1(1842 ^ [])],extension(582 ^ 13,bind([[_267653, _268618, _269324, _269615], [1842 ^ [], 1863 ^ [], 1881 ^ [], 669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []]]]))).
% 12.97/12.75 ncf('1.1.14.2.1',plain,[-(k5_rmod_4(1842 ^ [], 1863 ^ [], 669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []]) = k1_rlvect_1(1863 ^ [])), 668 : -(v1_rmod_5(1878 ^ [], 1842 ^ [], 1863 ^ [])), 668 : m1_subset_1(1878 ^ [], k1_zfmisc_1(u1_struct_0(1863 ^ [])))],extension(650 ^ 22,bind([[_269324], [1878 ^ []]]))).
% 12.97/12.75 ncf('1.1.14.2.1.1',plain,[v1_rmod_5(1878 ^ [], 1842 ^ [], 1863 ^ [])],extension(1889 ^ 25)).
% 12.97/12.75 ncf('1.1.14.2.1.2',plain,[-(m1_subset_1(1878 ^ [], k1_zfmisc_1(u1_struct_0(1863 ^ []))))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.14.2.2',plain,[k2_rmod_4(1842 ^ [], 1863 ^ [], 669 ^ [1842 ^ [], 1863 ^ [], 1878 ^ []]) = k1_xboole_0, 668 : -(v1_rmod_5(1878 ^ [], 1842 ^ [], 1863 ^ [])), 668 : m1_subset_1(1878 ^ [], k1_zfmisc_1(u1_struct_0(1863 ^ [])))],extension(650 ^ 22,bind([[_269324], [1878 ^ []]]))).
% 12.97/12.75 ncf('1.1.14.2.2.1',plain,[v1_rmod_5(1878 ^ [], 1842 ^ [], 1863 ^ [])],extension(1889 ^ 25)).
% 12.97/12.75 ncf('1.1.14.2.2.2',plain,[-(m1_subset_1(1878 ^ [], k1_zfmisc_1(u1_struct_0(1863 ^ []))))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.14.2.3',plain,[-(v1_rmod_5(1881 ^ [], 1842 ^ [], 1863 ^ []))],extension(1887 ^ 20)).
% 12.97/12.75 ncf('1.1.14.2.4',plain,[-(m1_subset_1(1881 ^ [], k1_zfmisc_1(u1_struct_0(1863 ^ []))))],extension(1883 ^ 18)).
% 12.97/12.75 ncf('1.1.14.2.5',plain,[v3_struct_0(1863 ^ [])],extension(1865 ^ 16)).
% 12.97/12.75 ncf('1.1.14.2.6',plain,[-(v3_rlvect_1(1863 ^ []))],extension(1867 ^ 16)).
% 12.97/12.75 ncf('1.1.14.2.7',plain,[-(v4_rlvect_1(1863 ^ []))],extension(1869 ^ 16)).
% 12.97/12.75 ncf('1.1.14.2.8',plain,[-(v5_rlvect_1(1863 ^ []))],extension(1871 ^ 16)).
% 12.97/12.75 ncf('1.1.14.2.9',plain,[-(v6_rlvect_1(1863 ^ []))],extension(1873 ^ 16)).
% 12.97/12.75 ncf('1.1.14.2.10',plain,[-(v5_vectsp_2(1863 ^ [], 1842 ^ []))],extension(1875 ^ 16)).
% 12.97/12.75 ncf('1.1.14.2.11',plain,[-(l1_vectsp_2(1863 ^ [], 1842 ^ []))],extension(1877 ^ 16)).
% 12.97/12.75 ncf('1.1.14.2.12',plain,[v3_struct_0(1842 ^ [])],reduction('1')).
% 12.97/12.75 ncf('1.1.14.2.13',plain,[-(v3_rlvect_1(1842 ^ []))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.14.2.14',plain,[-(v4_rlvect_1(1842 ^ []))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.14.2.15',plain,[-(v5_rlvect_1(1842 ^ []))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.14.2.16',plain,[-(v6_rlvect_1(1842 ^ []))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.14.2.17',plain,[-(v4_group_1(1842 ^ []))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.14.2.18',plain,[-(v6_vectsp_1(1842 ^ []))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.14.2.19',plain,[-(v7_vectsp_1(1842 ^ []))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.14.2.20',plain,[-(v8_vectsp_1(1842 ^ []))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.14.2.21',plain,[-(l3_vectsp_1(1842 ^ []))],lemmata('[1].x')).
% 12.97/12.75 ncf('1.1.14.3',plain,[-(m1_subset_1(1881 ^ [], k1_zfmisc_1(u1_struct_0(1863 ^ []))))],extension(1883 ^ 11)).
% 12.97/12.75 ncf('1.1.15',plain,[v3_struct_0(1863 ^ [])],extension(1865 ^ 4)).
% 12.97/12.75 ncf('1.1.16',plain,[-(v3_rlvect_1(1863 ^ []))],extension(1867 ^ 4)).
% 12.97/12.75 ncf('1.1.17',plain,[-(v4_rlvect_1(1863 ^ []))],extension(1869 ^ 4)).
% 12.97/12.75 ncf('1.1.18',plain,[-(v5_rlvect_1(1863 ^ []))],extension(1871 ^ 4)).
% 12.97/12.75 ncf('1.1.19',plain,[-(v6_rlvect_1(1863 ^ []))],extension(1873 ^ 4)).
% 12.97/12.75 ncf('1.1.20',plain,[-(v5_vectsp_2(1863 ^ [], 1842 ^ []))],extension(1875 ^ 4)).
% 12.97/12.75 ncf('1.1.21',plain,[-(l1_vectsp_2(1863 ^ [], 1842 ^ []))],extension(1877 ^ 4)).
% 12.97/12.75 %-----------------------------------------------------
% 12.97/12.75 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------