%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : ALG215+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n021.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 8.25s 8.64s
% Output : Proof 8.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ALG215+1 : TPTP v8.1.2. Released v3.4.0.
% 0.03/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n021.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 18 23:37:27 EDT 2023
% 0.12/0.34 % CPUTime :
% 8.25/8.64
% 8.25/8.64 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 8.25/8.64 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.25/8.64 %-----------------------------------------------------
% 8.25/8.64 ncf(matrix, plain, [(1862 ^ _250083) ^ [] : [v3_struct_0(1860 ^ [])], (1864 ^ _250083) ^ [] : [-(v3_rlvect_1(1860 ^ []))], (1866 ^ _250083) ^ [] : [-(v4_rlvect_1(1860 ^ []))], (1868 ^ _250083) ^ [] : [-(v5_rlvect_1(1860 ^ []))], (1870 ^ _250083) ^ [] : [-(v6_rlvect_1(1860 ^ []))], (1872 ^ _250083) ^ [] : [-(v4_group_1(1860 ^ []))], (1874 ^ _250083) ^ [] : [-(v6_vectsp_1(1860 ^ []))], (1876 ^ _250083) ^ [] : [-(v7_vectsp_1(1860 ^ []))], (1878 ^ _250083) ^ [] : [-(v8_vectsp_1(1860 ^ []))], (1880 ^ _250083) ^ [] : [-(l3_vectsp_1(1860 ^ []))], (1883 ^ _250083) ^ [] : [v3_struct_0(1881 ^ [])], (1885 ^ _250083) ^ [] : [-(v3_rlvect_1(1881 ^ []))], (1887 ^ _250083) ^ [] : [-(v4_rlvect_1(1881 ^ []))], (1889 ^ _250083) ^ [] : [-(v5_rlvect_1(1881 ^ []))], (1891 ^ _250083) ^ [] : [-(v6_rlvect_1(1881 ^ []))], (1893 ^ _250083) ^ [] : [-(v5_vectsp_2(1881 ^ [], 1860 ^ []))], (1895 ^ _250083) ^ [] : [-(l1_vectsp_2(1881 ^ [], 1860 ^ []))], (1897 ^ _250083) ^ [] : [v1_rmod_5(k1_subset_1(u1_struct_0(1881 ^ [])), 1860 ^ [], 1881 ^ [])], (452 ^ _250083) ^ [_264709, _264711, _264713, _264715, _264717, _264719] : [-(k2_rmod_4(_264719, _264715, _264711) = k2_rmod_4(_264717, _264713, _264709)), _264719 = _264717, _264715 = _264713, _264711 = _264709], (466 ^ _250083) ^ [_265225, _265227, _265229, _265231, _265233, _265235] : [-(k5_rmod_4(_265235, _265231, _265227) = k5_rmod_4(_265233, _265229, _265225)), _265235 = _265233, _265231 = _265229, _265227 = _265225], (480 ^ _250083) ^ [_265713, _265715, _265717, _265719] : [-(k2_zfmisc_1(_265719, _265715) = k2_zfmisc_1(_265717, _265713)), _265719 = _265717, _265715 = _265713], (490 ^ _250083) ^ [_266100, _266102, _266104, _266106, _266108, _266110] : [-(a_3_0_rmod_4(_266110, _266106, _266102) = a_3_0_rmod_4(_266108, _266104, _266100)), _266110 = _266108, _266106 = _266104, _266102 = _266100], (504 ^ _250083) ^ [_266560, _266562] : [_266562 = _266560, -(k1_rlvect_1(_266562) = k1_rlvect_1(_266560))], (510 ^ _250083) ^ [_266806, _266808, _266810, _266812] : [-(k1_fraenkel(_266812, _266808) = k1_fraenkel(_266810, _266806)), _266812 = _266810, _266808 = _266806], (520 ^ _250083) ^ [_267165, _267167, _267169, _267171] : [-(k1_funct_2(_267171, _267167) = k1_funct_2(_267169, _267165)), _267171 = _267169, _267167 = _267165], (530 ^ _250083) ^ [_267580, _267582, _267584, _267586, _267588, _267590, _267592, _267594] : [-(k8_funct_2(_267594, _267590, _267586, _267582) = k8_funct_2(_267592, _267588, _267584, _267580)), _267594 = _267592, _267590 = _267588, _267586 = _267584, _267582 = _267580], (548 ^ _250083) ^ [_268213, _268215, _268217, _268219] : [-(k1_funct_1(_268219, _268215) = k1_funct_1(_268217, _268213)), _268219 = _268217, _268215 = _268213], (558 ^ _250083) ^ [_268544, _268546] : [_268546 = _268544, -(k1_zfmisc_1(_268546) = k1_zfmisc_1(_268544))], (564 ^ _250083) ^ [_268762, _268764] : [_268764 = _268762, -(k1_subset_1(_268764) = k1_subset_1(_268762))], (570 ^ _250083) ^ [_268960, _268962] : [_268962 = _268960, -(u1_struct_0(_268962) = u1_struct_0(_268960))], (2 ^ _250083) ^ [_250227] : [-(_250227 = _250227)], (4 ^ _250083) ^ [_250334, _250336] : [_250336 = _250334, -(_250334 = _250336)], (10 ^ _250083) ^ [_250538, _250540, _250542] : [-(_250542 = _250538), _250542 = _250540, _250540 = _250538], (20 ^ _250083) ^ [_250851, _250853] : [-(v1_relat_1(_250851)), _250853 = _250851, v1_relat_1(_250853)], (30 ^ _250083) ^ [_251146, _251148] : [-(v1_fraenkel(_251146)), _251148 = _251146, v1_fraenkel(_251148)], (40 ^ _250083) ^ [_251441, _251443] : [-(l1_group_1(_251441)), _251443 = _251441, l1_group_1(_251443)], (50 ^ _250083) ^ [_251736, _251738] : [-(l1_rlvect_1(_251736)), _251738 = _251736, l1_rlvect_1(_251738)], (60 ^ _250083) ^ [_252031, _252033] : [-(l1_vectsp_1(_252031)), _252033 = _252031, l1_vectsp_1(_252033)], (70 ^ _250083) ^ [_252326, _252328] : [-(l2_vectsp_1(_252326)), _252328 = _252326, l2_vectsp_1(_252328)], (80 ^ _250083) ^ [_252705, _252707, _252709, _252711, _252713, _252715, _252717, _252719] : [-(m2_rmod_4(_252717, _252713, _252709, _252705)), m2_rmod_4(_252719, _252715, _252711, _252707), _252719 = _252717, _252715 = _252713, _252711 = _252709, _252707 = _252705], (102 ^ _250083) ^ [_253467, _253469, _253471, _253473, _253475, _253477] : [-(m1_rmod_4(_253475, _253471, _253467)), m1_rmod_4(_253477, _253473, _253469), _253477 = _253475, _253473 = _253471, _253469 = _253467], (120 ^ _250083) ^ [_254020, _254022] : [-(v1_finset_1(_254020)), _254022 = _254020, v1_finset_1(_254022)], (130 ^ _250083) ^ [_254315, _254317] : [-(l2_struct_0(_254315)), _254317 = _254315, l2_struct_0(_254317)], (140 ^ _250083) ^ [_254610, _254612] : [-(l1_struct_0(_254610)), _254612 = _254610, l1_struct_0(_254612)], (150 ^ _250083) ^ [_254905, _254907] : [-(v1_funct_1(_254905)), _254907 = _254905, v1_funct_1(_254907)], (160 ^ _250083) ^ [_255256, _255258, _255260, _255262, _255264, _255266] : [-(v1_funct_2(_255264, _255260, _255256)), v1_funct_2(_255266, _255262, _255258), _255266 = _255264, _255262 = _255260, _255258 = _255256], (178 ^ _250083) ^ [_255865, _255867, _255869, _255871, _255873, _255875] : [-(m1_fraenkel(_255873, _255869, _255865)), m1_fraenkel(_255875, _255871, _255867), _255875 = _255873, _255871 = _255869, _255867 = _255865], (196 ^ _250083) ^ [_256502, _256504, _256506, _256508, _256510, _256512, _256514, _256516] : [-(m2_fraenkel(_256514, _256510, _256506, _256502)), m2_fraenkel(_256516, _256512, _256508, _256504), _256516 = _256514, _256512 = _256510, _256508 = _256506, _256504 = _256502], (218 ^ _250083) ^ [_257264, _257266, _257268, _257270, _257272, _257274] : [-(m2_relset_1(_257272, _257268, _257264)), m2_relset_1(_257274, _257270, _257266), _257274 = _257272, _257270 = _257268, _257266 = _257264], (236 ^ _250083) ^ [_257873, _257875, _257877, _257879, _257881, _257883] : [-(m1_relset_1(_257881, _257877, _257873)), m1_relset_1(_257883, _257879, _257875), _257883 = _257881, _257879 = _257877, _257875 = _257873], (254 ^ _250083) ^ [_258454, _258456, _258458, _258460] : [-(r1_tarski(_258458, _258454)), r1_tarski(_258460, _258456), _258460 = _258458, _258456 = _258454], (268 ^ _250083) ^ [_258898, _258900, _258902, _258904] : [-(m1_subset_1(_258902, _258898)), m1_subset_1(_258904, _258900), _258904 = _258902, _258900 = _258898], (282 ^ _250083) ^ [_259342, _259344, _259346, _259348] : [-(r2_hidden(_259346, _259342)), r2_hidden(_259348, _259344), _259348 = _259346, _259344 = _259342], (296 ^ _250083) ^ [_259758, _259760] : [-(v1_xboole_0(_259758)), _259760 = _259758, v1_xboole_0(_259760)], (306 ^ _250083) ^ [_260053, _260055] : [-(v4_group_1(_260053)), _260055 = _260053, v4_group_1(_260055)], (316 ^ _250083) ^ [_260348, _260350] : [-(v6_vectsp_1(_260348)), _260350 = _260348, v6_vectsp_1(_260350)], (326 ^ _250083) ^ [_260643, _260645] : [-(v7_vectsp_1(_260643)), _260645 = _260643, v7_vectsp_1(_260645)], (336 ^ _250083) ^ [_260938, _260940] : [-(v8_vectsp_1(_260938)), _260940 = _260938, v8_vectsp_1(_260940)], (346 ^ _250083) ^ [_261233, _261235] : [-(l3_vectsp_1(_261233)), _261235 = _261233, l3_vectsp_1(_261235)], (356 ^ _250083) ^ [_261528, _261530] : [-(v3_struct_0(_261528)), _261530 = _261528, v3_struct_0(_261530)], (366 ^ _250083) ^ [_261823, _261825] : [-(v3_rlvect_1(_261823)), _261825 = _261823, v3_rlvect_1(_261825)], (376 ^ _250083) ^ [_262118, _262120] : [-(v4_rlvect_1(_262118)), _262120 = _262118, v4_rlvect_1(_262120)], (386 ^ _250083) ^ [_262413, _262415] : [-(v5_rlvect_1(_262413)), _262415 = _262413, v5_rlvect_1(_262415)], (396 ^ _250083) ^ [_262708, _262710] : [-(v6_rlvect_1(_262708)), _262710 = _262708, v6_rlvect_1(_262710)], (406 ^ _250083) ^ [_263031, _263033, _263035, _263037] : [-(v5_vectsp_2(_263035, _263031)), v5_vectsp_2(_263037, _263033), _263037 = _263035, _263033 = _263031], (420 ^ _250083) ^ [_263475, _263477, _263479, _263481] : [-(l1_vectsp_2(_263479, _263475)), l1_vectsp_2(_263481, _263477), _263481 = _263479, _263477 = _263475], (434 ^ _250083) ^ [_263927, _263929, _263931, _263933, _263935, _263937] : [-(v1_rmod_5(_263935, _263931, _263927)), v1_rmod_5(_263937, _263933, _263929), _263937 = _263935, _263933 = _263931, _263929 = _263927], (576 ^ _250083) ^ [_269229, _269231] : [r2_hidden(_269231, _269229), r2_hidden(_269229, _269231)], (582 ^ _250083) ^ [_269454, _269456, _269458] : [m1_subset_1(_269454, k1_zfmisc_1(k2_zfmisc_1(_269458, _269456))), -(v1_relat_1(_269454))], (588 ^ _250083) ^ [_269664] : [-(v3_struct_0(_269664)), v3_rlvect_1(_269664), v4_rlvect_1(_269664), v5_rlvect_1(_269664), v6_rlvect_1(_269664), v4_group_1(_269664), v6_vectsp_1(_269664), v7_vectsp_1(_269664), v8_vectsp_1(_269664), l3_vectsp_1(_269664), 627 ^ _250083 : [(628 ^ _250083) ^ [_270629] : [-(v3_struct_0(_270629)), v3_rlvect_1(_270629), v4_rlvect_1(_270629), v5_rlvect_1(_270629), v6_rlvect_1(_270629), v5_vectsp_2(_270629, _269664), l1_vectsp_2(_270629, _269664), 655 ^ _250083 : [(656 ^ _250083) ^ [_271335] : [m1_subset_1(_271335, k1_zfmisc_1(u1_struct_0(_270629))), 659 ^ _250083 : [(674 ^ _250083) ^ [] : [676 ^ _250083 : [(677 ^ _250083) ^ [] : [-(m2_rmod_4(675 ^ [_269664, _270629, _271335], _269664, _270629, _271335))], (679 ^ _250083) ^ [] : [-(k5_rmod_4(_269664, _270629, 675 ^ [_269664, _270629, _271335]) = k1_rlvect_1(_270629))], (681 ^ _250083) ^ [] : [k2_rmod_4(_269664, _270629, 675 ^ [_269664, _270629, _271335]) = k1_xboole_0]], -(v1_rmod_5(_271335, _269664, _270629))], (660 ^ _250083) ^ [] : [v1_rmod_5(_271335, _269664, _270629), 663 ^ _250083 : [(664 ^ _250083) ^ [_271626] : [m2_rmod_4(_271626, _269664, _270629, _271335), k5_rmod_4(_269664, _270629, _271626) = k1_rlvect_1(_270629), -(k2_rmod_4(_269664, _270629, _271626) = k1_xboole_0)]]]]]]]]], (685 ^ _250083) ^ [_272402] : [724 ^ _250083 : [(725 ^ _250083) ^ [_273336] : [752 ^ _250083 : [(753 ^ _250083) ^ [_274011] : [m1_rmod_4(_274011, _272402, _273336), -(k2_rmod_4(_272402, _273336, _274011) = a_3_0_rmod_4(_272402, _273336, _274011))]], -(v3_struct_0(_273336)), v3_rlvect_1(_273336), v4_rlvect_1(_273336), v5_rlvect_1(_273336), v6_rlvect_1(_273336), v5_vectsp_2(_273336, _272402), l1_vectsp_2(_273336, _272402)]], -(v3_struct_0(_272402)), v3_rlvect_1(_272402), v4_rlvect_1(_272402), v5_rlvect_1(_272402), v6_rlvect_1(_272402), v4_group_1(_272402), v6_vectsp_1(_272402), v7_vectsp_1(_272402), v8_vectsp_1(_272402), l3_vectsp_1(_272402)], (759 ^ _250083) ^ [_274245] : [-(v3_struct_0(_274245)), v3_rlvect_1(_274245), v4_rlvect_1(_274245), v5_rlvect_1(_274245), v6_rlvect_1(_274245), v4_group_1(_274245), v6_vectsp_1(_274245), v7_vectsp_1(_274245), v8_vectsp_1(_274245), l3_vectsp_1(_274245), 798 ^ _250083 : [(799 ^ _250083) ^ [_275198] : [826 ^ _250083 : [(827 ^ _250083) ^ [_275892] : [m1_subset_1(_275892, k1_zfmisc_1(u1_struct_0(_275198))), 830 ^ _250083 : [(831 ^ _250083) ^ [_276058] : [m1_rmod_4(_276058, _274245, _275198), 834 ^ _250083 : [(835 ^ _250083) ^ [] : [m2_rmod_4(_276058, _274245, _275198, _275892), -(r1_tarski(k2_rmod_4(_274245, _275198, _276058), _275892))], (841 ^ _250083) ^ [] : [r1_tarski(k2_rmod_4(_274245, _275198, _276058), _275892), -(m2_rmod_4(_276058, _274245, _275198, _275892))]]]]]], -(v3_struct_0(_275198)), v3_rlvect_1(_275198), v4_rlvect_1(_275198), v5_rlvect_1(_275198), v6_rlvect_1(_275198), v5_vectsp_2(_275198, _274245), l1_vectsp_2(_275198, _274245)]]], (847 ^ _250083) ^ [_276609, _276611] : [-(v1_xboole_0(_276609)), -(m1_fraenkel(k1_fraenkel(_276611, _276609), _276611, _276609))], (853 ^ _250083) ^ [] : [true___, -(true___)], (859 ^ _250083) ^ [] : [true___, -(true___)], (865 ^ _250083) ^ [_277052] : [l2_struct_0(_277052), -(m1_subset_1(k1_rlvect_1(_277052), u1_struct_0(_277052)))], (871 ^ _250083) ^ [_277253] : [-(v1_xboole_0(k1_subset_1(_277253)))], (873 ^ _250083) ^ [_277298] : [-(m1_subset_1(k1_subset_1(_277298), k1_zfmisc_1(_277298)))], (875 ^ _250083) ^ [] : [true___, -(true___)], (881 ^ _250083) ^ [] : [true___, -(true___)], (887 ^ _250083) ^ [_277663, _277665, _277667] : [958 ^ _250083 : [(959 ^ _250083) ^ [] : [-(v1_finset_1(k2_rmod_4(_277667, _277665, _277663)))], (961 ^ _250083) ^ [] : [-(m1_subset_1(k2_rmod_4(_277667, _277665, _277663), k1_zfmisc_1(u1_struct_0(_277665))))]], -(v3_struct_0(_277667)), v3_rlvect_1(_277667), v4_rlvect_1(_277667), v5_rlvect_1(_277667), v6_rlvect_1(_277667), v4_group_1(_277667), v6_vectsp_1(_277667), v7_vectsp_1(_277667), v8_vectsp_1(_277667), l3_vectsp_1(_277667), -(v3_struct_0(_277665)), v3_rlvect_1(_277665), v4_rlvect_1(_277665), v5_rlvect_1(_277665), v6_rlvect_1(_277665), v5_vectsp_2(_277665, _277667), l1_vectsp_2(_277665, _277667), m1_rmod_4(_277663, _277667, _277665)], (963 ^ _250083) ^ [] : [true___, -(true___)], (969 ^ _250083) ^ [_279670, _279672, _279674] : [-(m1_subset_1(k5_rmod_4(_279674, _279672, _279670), u1_struct_0(_279672))), -(v3_struct_0(_279674)), v3_rlvect_1(_279674), v4_rlvect_1(_279674), v5_rlvect_1(_279674), v6_rlvect_1(_279674), v4_group_1(_279674), v6_vectsp_1(_279674), v7_vectsp_1(_279674), v8_vectsp_1(_279674), l3_vectsp_1(_279674), -(v3_struct_0(_279672)), v3_rlvect_1(_279672), v4_rlvect_1(_279672), v5_rlvect_1(_279672), v6_rlvect_1(_279672), v5_vectsp_2(_279672, _279674), l1_vectsp_2(_279672, _279674), m1_rmod_4(_279670, _279674, _279672)], (1043 ^ _250083) ^ [_281485, _281487, _281489, _281491] : [-(m1_subset_1(k8_funct_2(_281491, _281489, _281487, _281485), _281489)), -(v1_xboole_0(_281491)), v1_funct_1(_281487), v1_funct_2(_281487, _281491, _281489), m1_relset_1(_281487, _281491, _281489), m1_subset_1(_281485, _281491)], (1065 ^ _250083) ^ [_282094] : [l1_group_1(_282094), -(l1_struct_0(_282094))], (1071 ^ _250083) ^ [_282280] : [l1_rlvect_1(_282280), -(l2_struct_0(_282280))], (1077 ^ _250083) ^ [] : [true___, -(true___)], (1083 ^ _250083) ^ [_282585] : [l1_vectsp_1(_282585), -(l1_group_1(_282585))], (1089 ^ _250083) ^ [_282771] : [l1_struct_0(_282771), 1092 ^ _250083 : [(1093 ^ _250083) ^ [_282901] : [l1_vectsp_2(_282901, _282771), -(l1_rlvect_1(_282901))]]], (1099 ^ _250083) ^ [_283102] : [l2_struct_0(_283102), -(l1_struct_0(_283102))], (1105 ^ _250083) ^ [_283288] : [l2_vectsp_1(_283288), 1108 ^ _250083 : [(1109 ^ _250083) ^ [] : [-(l1_vectsp_1(_283288))], (1111 ^ _250083) ^ [] : [-(l2_struct_0(_283288))]]], (1113 ^ _250083) ^ [_283545] : [l3_vectsp_1(_283545), 1116 ^ _250083 : [(1117 ^ _250083) ^ [] : [-(l1_rlvect_1(_283545))], (1119 ^ _250083) ^ [] : [-(l2_vectsp_1(_283545))]]], (1121 ^ _250083) ^ [_283830, _283832, _283834] : [m1_fraenkel(_283830, _283834, _283832), 1124 ^ _250083 : [(1125 ^ _250083) ^ [] : [v1_xboole_0(_283830)], (1127 ^ _250083) ^ [] : [-(v1_fraenkel(_283830))]]], (1129 ^ _250083) ^ [] : [true___, -(true___)], (1135 ^ _250083) ^ [_284241, _284243] : [1202 ^ _250083 : [(1203 ^ _250083) ^ [_285792] : [m1_rmod_4(_285792, _284243, _284241), -(m2_fraenkel(_285792, u1_struct_0(_284241), u1_struct_0(_284243), k1_fraenkel(u1_struct_0(_284241), u1_struct_0(_284243))))]], -(v3_struct_0(_284243)), v3_rlvect_1(_284243), v4_rlvect_1(_284243), v5_rlvect_1(_284243), v6_rlvect_1(_284243), v4_group_1(_284243), v6_vectsp_1(_284243), v7_vectsp_1(_284243), v8_vectsp_1(_284243), l3_vectsp_1(_284243), -(v3_struct_0(_284241)), v3_rlvect_1(_284241), v4_rlvect_1(_284241), v5_rlvect_1(_284241), v6_rlvect_1(_284241), v5_vectsp_2(_284241, _284243), l1_vectsp_2(_284241, _284243)], (1209 ^ _250083) ^ [] : [true___, -(true___)], (1215 ^ _250083) ^ [_286178, _286180, _286182] : [-(v1_xboole_0(_286180)), m1_fraenkel(_286178, _286182, _286180), 1222 ^ _250083 : [(1223 ^ _250083) ^ [_286430] : [m2_fraenkel(_286430, _286182, _286180, _286178), 1226 ^ _250083 : [(1227 ^ _250083) ^ [] : [-(v1_funct_1(_286430))], (1229 ^ _250083) ^ [] : [-(v1_funct_2(_286430, _286182, _286180))], (1231 ^ _250083) ^ [] : [-(m2_relset_1(_286430, _286182, _286180))]]]]], (1233 ^ _250083) ^ [_286842, _286844, _286846] : [m2_relset_1(_286842, _286846, _286844), -(m1_subset_1(_286842, k1_zfmisc_1(k2_zfmisc_1(_286846, _286844))))], (1239 ^ _250083) ^ [_287084, _287086, _287088] : [1310 ^ _250083 : [(1311 ^ _250083) ^ [_288793] : [m2_rmod_4(_288793, _287088, _287086, _287084), -(m1_rmod_4(_288793, _287088, _287086))]], -(v3_struct_0(_287088)), v3_rlvect_1(_287088), v4_rlvect_1(_287088), v5_rlvect_1(_287088), v6_rlvect_1(_287088), v4_group_1(_287088), v6_vectsp_1(_287088), v7_vectsp_1(_287088), v8_vectsp_1(_287088), l3_vectsp_1(_287088), -(v3_struct_0(_287086)), v3_rlvect_1(_287086), v4_rlvect_1(_287086), v5_rlvect_1(_287086), v6_rlvect_1(_287086), v5_vectsp_2(_287086, _287088), l1_vectsp_2(_287086, _287088), m1_subset_1(_287084, k1_zfmisc_1(u1_struct_0(_287086)))], (1317 ^ _250083) ^ [] : [true___, -(true___)], (1324 ^ _250083) ^ [] : [-(l1_group_1(1322 ^ []))], (1327 ^ _250083) ^ [] : [-(l1_rlvect_1(1325 ^ []))], (1330 ^ _250083) ^ [] : [-(l1_struct_0(1328 ^ []))], (1333 ^ _250083) ^ [] : [-(l1_vectsp_1(1331 ^ []))], (1335 ^ _250083) ^ [_289493] : [l1_struct_0(_289493), -(l1_vectsp_2(1338 ^ [_289493], _289493))], (1343 ^ _250083) ^ [] : [-(l2_struct_0(1341 ^ []))], (1346 ^ _250083) ^ [] : [-(l2_vectsp_1(1344 ^ []))], (1349 ^ _250083) ^ [] : [-(l3_vectsp_1(1347 ^ []))], (1352 ^ _250083) ^ [_290040, _290042] : [-(m1_fraenkel(1350 ^ [_290040, _290042], _290042, _290040))], (1355 ^ _250083) ^ [_290184, _290186] : [-(m1_relset_1(1353 ^ [_290184, _290186], _290186, _290184))], (1357 ^ _250083) ^ [_290301, _290303] : [-(m1_rmod_4(1424 ^ [_290301, _290303], _290303, _290301)), -(v3_struct_0(_290303)), v3_rlvect_1(_290303), v4_rlvect_1(_290303), v5_rlvect_1(_290303), v6_rlvect_1(_290303), v4_group_1(_290303), v6_vectsp_1(_290303), v7_vectsp_1(_290303), v8_vectsp_1(_290303), l3_vectsp_1(_290303), -(v3_struct_0(_290301)), v3_rlvect_1(_290301), v4_rlvect_1(_290301), v5_rlvect_1(_290301), v6_rlvect_1(_290301), v5_vectsp_2(_290301, _290303), l1_vectsp_2(_290301, _290303)], (1429 ^ _250083) ^ [_291981] : [-(m1_subset_1(1427 ^ [_291981], _291981))], (1431 ^ _250083) ^ [_292107, _292109, _292111] : [-(m2_fraenkel(1438 ^ [_292107, _292109, _292111], _292111, _292109, _292107)), -(v1_xboole_0(_292109)), m1_fraenkel(_292107, _292111, _292109)], (1443 ^ _250083) ^ [_292515, _292517] : [-(m2_relset_1(1441 ^ [_292515, _292517], _292517, _292515))], (1445 ^ _250083) ^ [_292646, _292648, _292650] : [-(m2_rmod_4(1516 ^ [_292646, _292648, _292650], _292650, _292648, _292646)), -(v3_struct_0(_292650)), v3_rlvect_1(_292650), v4_rlvect_1(_292650), v5_rlvect_1(_292650), v6_rlvect_1(_292650), v4_group_1(_292650), v6_vectsp_1(_292650), v7_vectsp_1(_292650), v8_vectsp_1(_292650), l3_vectsp_1(_292650), -(v3_struct_0(_292648)), v3_rlvect_1(_292648), v4_rlvect_1(_292648), v5_rlvect_1(_292648), v6_rlvect_1(_292648), v5_vectsp_2(_292648, _292650), l1_vectsp_2(_292648, _292650), m1_subset_1(_292646, k1_zfmisc_1(u1_struct_0(_292648)))], (1520 ^ _250083) ^ [_294482] : [v1_xboole_0(u1_struct_0(_294482)), -(v3_struct_0(_294482)), l1_struct_0(_294482)], (1530 ^ _250083) ^ [_294743] : [v1_xboole_0(k1_zfmisc_1(_294743))], (1532 ^ _250083) ^ [] : [-(v1_xboole_0(k1_xboole_0))], (1534 ^ _250083) ^ [_294904, _294906] : [v1_xboole_0(k2_zfmisc_1(_294906, _294904)), -(v1_xboole_0(_294906)), -(v1_xboole_0(_294904))], (1544 ^ _250083) ^ [_295238, _295240, _295242, _295244] : [1615 ^ _250083 : [(1616 ^ _250083) ^ [] : [r2_hidden(_295244, a_3_0_rmod_4(_295242, _295240, _295238)), 1620 ^ _250083 : [(1621 ^ _250083) ^ [] : [-(m1_subset_1(1619 ^ [_295238, _295240, _295242, _295244], u1_struct_0(_295240)))], (1623 ^ _250083) ^ [] : [-(_295244 = 1619 ^ [_295238, _295240, _295242, _295244])], (1625 ^ _250083) ^ [] : [k8_funct_2(u1_struct_0(_295240), u1_struct_0(_295242), _295238, 1619 ^ [_295238, _295240, _295242, _295244]) = k1_rlvect_1(_295242)]]], (1627 ^ _250083) ^ [] : [-(r2_hidden(_295244, a_3_0_rmod_4(_295242, _295240, _295238))), 1628 ^ _250083 : [(1629 ^ _250083) ^ [_297523] : [m1_subset_1(_297523, u1_struct_0(_295240)), _295244 = _297523, -(k8_funct_2(u1_struct_0(_295240), u1_struct_0(_295242), _295238, _297523) = k1_rlvect_1(_295242))]]]], -(v3_struct_0(_295242)), v3_rlvect_1(_295242), v4_rlvect_1(_295242), v5_rlvect_1(_295242), v6_rlvect_1(_295242), v4_group_1(_295242), v6_vectsp_1(_295242), v7_vectsp_1(_295242), v8_vectsp_1(_295242), l3_vectsp_1(_295242), -(v3_struct_0(_295240)), v3_rlvect_1(_295240), v4_rlvect_1(_295240), v5_rlvect_1(_295240), v6_rlvect_1(_295240), v5_vectsp_2(_295240, _295242), l1_vectsp_2(_295240, _295242), m1_rmod_4(_295238, _295242, _295240)], (1641 ^ _250083) ^ [_297940] : [-(v1_xboole_0(_297940)), 1645 ^ _250083 : [(1646 ^ _250083) ^ [] : [-(m1_subset_1(1644 ^ [_297940], k1_zfmisc_1(_297940)))], (1648 ^ _250083) ^ [] : [v1_xboole_0(1644 ^ [_297940])]]], (1651 ^ _250083) ^ [] : [-(v1_xboole_0(1649 ^ []))], (1653 ^ _250083) ^ [_298361] : [1661 ^ _250083 : [(1662 ^ _250083) ^ [] : [-(m1_subset_1(1660 ^ [_298361], k1_zfmisc_1(u1_struct_0(_298361))))], (1664 ^ _250083) ^ [] : [v1_xboole_0(1660 ^ [_298361])], (1666 ^ _250083) ^ [] : [-(v1_finset_1(1660 ^ [_298361]))]], -(v3_struct_0(_298361)), l1_struct_0(_298361)], (1669 ^ _250083) ^ [_298913] : [-(m1_subset_1(1667 ^ [_298913], k1_zfmisc_1(_298913)))], (1671 ^ _250083) ^ [_298964] : [-(v1_xboole_0(1667 ^ [_298964]))], (1674 ^ _250083) ^ [] : [v1_xboole_0(1672 ^ [])], (1677 ^ _250083) ^ [] : [-(l1_struct_0(1675 ^ []))], (1679 ^ _250083) ^ [] : [v3_struct_0(1675 ^ [])], (1682 ^ _250083) ^ [] : [-(l2_struct_0(1680 ^ []))], (1684 ^ _250083) ^ [] : [v3_struct_0(1680 ^ [])], (1686 ^ _250083) ^ [_299453] : [1694 ^ _250083 : [(1695 ^ _250083) ^ [] : [-(m1_subset_1(1693 ^ [_299453], k1_zfmisc_1(u1_struct_0(_299453))))], (1697 ^ _250083) ^ [] : [v1_xboole_0(1693 ^ [_299453])]], -(v3_struct_0(_299453)), l1_struct_0(_299453)], (1699 ^ _250083) ^ [_299874] : [l1_struct_0(_299874), 1703 ^ _250083 : [(1704 ^ _250083) ^ [] : [-(l1_vectsp_2(1702 ^ [_299874], _299874))], (1706 ^ _250083) ^ [] : [v3_struct_0(1702 ^ [_299874])]]], (1708 ^ _250083) ^ [_300211, _300213] : [-(v1_xboole_0(_300211)), -(k1_fraenkel(_300213, _300211) = k1_funct_2(_300213, _300211))], (1714 ^ _250083) ^ [_300462, _300464, _300466, _300468] : [-(k8_funct_2(_300468, _300466, _300464, _300462) = k1_funct_1(_300464, _300462)), -(v1_xboole_0(_300468)), v1_funct_1(_300464), v1_funct_2(_300464, _300468, _300466), m1_relset_1(_300464, _300468, _300466), m1_subset_1(_300462, _300468)], (1736 ^ _250083) ^ [_301105, _301107, _301109] : [-(v1_xboole_0(_301107)), m1_fraenkel(_301105, _301109, _301107), 1743 ^ _250083 : [(1744 ^ _250083) ^ [_301373] : [m2_fraenkel(_301373, _301109, _301107, _301105), -(m1_subset_1(_301373, _301105))], (1750 ^ _250083) ^ [_301557] : [m1_subset_1(_301557, _301105), -(m2_fraenkel(_301557, _301109, _301107, _301105))]]], (1756 ^ _250083) ^ [_301841, _301843, _301845] : [m2_relset_1(_301841, _301845, _301843), -(m1_relset_1(_301841, _301845, _301843))], (1762 ^ _250083) ^ [_302013, _302015, _302017] : [m1_relset_1(_302013, _302017, _302015), -(m2_relset_1(_302013, _302017, _302015))], (1768 ^ _250083) ^ [_302220, _302222] : [-(r1_tarski(_302222, _302222))], (1770 ^ _250083) ^ [_302329, _302331] : [r2_hidden(_302331, _302329), -(m1_subset_1(_302331, _302329))], (1776 ^ _250083) ^ [_302539, _302541] : [m1_subset_1(_302541, _302539), -(v1_xboole_0(_302539)), -(r2_hidden(_302541, _302539))], (1786 ^ _250083) ^ [_302837, _302839] : [-(_302839 = _302837), 1790 ^ _250083 : [(1791 ^ _250083) ^ [] : [-(r2_hidden(1787 ^ [_302837, _302839], _302839))], (1793 ^ _250083) ^ [] : [r2_hidden(1787 ^ [_302837, _302839], _302837)]], 1794 ^ _250083 : [(1795 ^ _250083) ^ [] : [-(r2_hidden(1787 ^ [_302837, _302839], _302837))], (1797 ^ _250083) ^ [] : [r2_hidden(1787 ^ [_302837, _302839], _302839)]]], (1801 ^ _250083) ^ [_303396, _303398] : [m1_subset_1(_303398, k1_zfmisc_1(_303396)), -(r1_tarski(_303398, _303396))], (1807 ^ _250083) ^ [_303562, _303564] : [r1_tarski(_303564, _303562), -(m1_subset_1(_303564, k1_zfmisc_1(_303562)))], (1813 ^ _250083) ^ [_303764] : [r1_tarski(_303764, k1_xboole_0), -(_303764 = k1_xboole_0)], (1819 ^ _250083) ^ [_303982, _303984, _303986] : [-(m1_subset_1(_303986, _303982)), r2_hidden(_303986, _303984), m1_subset_1(_303984, k1_zfmisc_1(_303982))], (1829 ^ _250083) ^ [_304309, _304311, _304313] : [r2_hidden(_304313, _304311), m1_subset_1(_304311, k1_zfmisc_1(_304309)), v1_xboole_0(_304309)], (1839 ^ _250083) ^ [_304605] : [v1_xboole_0(_304605), -(_304605 = k1_xboole_0)], (1845 ^ _250083) ^ [_304807, _304809] : [r2_hidden(_304809, _304807), v1_xboole_0(_304807)], (1851 ^ _250083) ^ [_304994, _304996] : [v1_xboole_0(_304996), -(_304996 = _304994), v1_xboole_0(_304994)]], input).
% 8.25/8.64 ncf('1',plain,[v3_struct_0(1860 ^ [])],start(1862 ^ 0)).
% 8.25/8.64 ncf('1.1',plain,[-(v3_struct_0(1860 ^ [])), v3_rlvect_1(1860 ^ []), v4_rlvect_1(1860 ^ []), v5_rlvect_1(1860 ^ []), v6_rlvect_1(1860 ^ []), v4_group_1(1860 ^ []), v6_vectsp_1(1860 ^ []), v7_vectsp_1(1860 ^ []), v8_vectsp_1(1860 ^ []), l3_vectsp_1(1860 ^ []), 827 : m1_subset_1(k1_subset_1(u1_struct_0(1881 ^ [])), k1_zfmisc_1(u1_struct_0(1881 ^ []))), 831 : m1_rmod_4(675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))], 1860 ^ [], 1881 ^ []), 835 : m2_rmod_4(675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))], 1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))), 835 : -(r1_tarski(k2_rmod_4(1860 ^ [], 1881 ^ [], 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]), k1_subset_1(u1_struct_0(1881 ^ [])))), 827 : -(v3_struct_0(1881 ^ [])), 827 : v3_rlvect_1(1881 ^ []), 827 : v4_rlvect_1(1881 ^ []), 827 : v5_rlvect_1(1881 ^ []), 827 : v6_rlvect_1(1881 ^ []), 827 : v5_vectsp_2(1881 ^ [], 1860 ^ []), 827 : l1_vectsp_2(1881 ^ [], 1860 ^ [])],extension(759 ^ 1,bind([[_274245, _275198, _275892, _276058], [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ [])), 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]]]))).
% 8.25/8.64 ncf('1.1.1',plain,[-(v3_rlvect_1(1860 ^ []))],extension(1864 ^ 2)).
% 8.25/8.64 ncf('1.1.2',plain,[-(v4_rlvect_1(1860 ^ []))],extension(1866 ^ 2)).
% 8.25/8.64 ncf('1.1.3',plain,[-(v5_rlvect_1(1860 ^ []))],extension(1868 ^ 2)).
% 8.25/8.64 ncf('1.1.4',plain,[-(v6_rlvect_1(1860 ^ []))],extension(1870 ^ 2)).
% 8.25/8.64 ncf('1.1.5',plain,[-(v4_group_1(1860 ^ []))],extension(1872 ^ 2)).
% 8.25/8.64 ncf('1.1.6',plain,[-(v6_vectsp_1(1860 ^ []))],extension(1874 ^ 2)).
% 8.25/8.64 ncf('1.1.7',plain,[-(v7_vectsp_1(1860 ^ []))],extension(1876 ^ 2)).
% 8.25/8.64 ncf('1.1.8',plain,[-(v8_vectsp_1(1860 ^ []))],extension(1878 ^ 2)).
% 8.25/8.64 ncf('1.1.9',plain,[-(l3_vectsp_1(1860 ^ []))],extension(1880 ^ 2)).
% 8.25/8.64 ncf('1.1.10',plain,[-(m1_subset_1(k1_subset_1(u1_struct_0(1881 ^ [])), k1_zfmisc_1(u1_struct_0(1881 ^ []))))],extension(873 ^ 6,bind([[_277298], [u1_struct_0(1881 ^ [])]]))).
% 8.25/8.64 ncf('1.1.11',plain,[-(m1_rmod_4(675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))], 1860 ^ [], 1881 ^ [])), 1311 : m2_rmod_4(675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))], 1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))), 1311 : -(v3_struct_0(1860 ^ [])), 1311 : v3_rlvect_1(1860 ^ []), 1311 : v4_rlvect_1(1860 ^ []), 1311 : v5_rlvect_1(1860 ^ []), 1311 : v6_rlvect_1(1860 ^ []), 1311 : v4_group_1(1860 ^ []), 1311 : v6_vectsp_1(1860 ^ []), 1311 : v7_vectsp_1(1860 ^ []), 1311 : v8_vectsp_1(1860 ^ []), 1311 : l3_vectsp_1(1860 ^ []), 1311 : -(v3_struct_0(1881 ^ [])), 1311 : v3_rlvect_1(1881 ^ []), 1311 : v4_rlvect_1(1881 ^ []), 1311 : v5_rlvect_1(1881 ^ []), 1311 : v6_rlvect_1(1881 ^ []), 1311 : v5_vectsp_2(1881 ^ [], 1860 ^ []), 1311 : l1_vectsp_2(1881 ^ [], 1860 ^ []), 1311 : m1_subset_1(k1_subset_1(u1_struct_0(1881 ^ [])), k1_zfmisc_1(u1_struct_0(1881 ^ [])))],extension(1239 ^ 8,bind([[_287084, _287086, _287088, _288793], [k1_subset_1(u1_struct_0(1881 ^ [])), 1881 ^ [], 1860 ^ [], 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]]]))).
% 8.25/8.64 ncf('1.1.11.1',plain,[-(m2_rmod_4(675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))], 1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ [])))), 674 : -(v1_rmod_5(k1_subset_1(u1_struct_0(1881 ^ [])), 1860 ^ [], 1881 ^ [])), 674 : m1_subset_1(k1_subset_1(u1_struct_0(1881 ^ [])), k1_zfmisc_1(u1_struct_0(1881 ^ []))), 656 : -(v3_struct_0(1881 ^ [])), 656 : v3_rlvect_1(1881 ^ []), 656 : v4_rlvect_1(1881 ^ []), 656 : v5_rlvect_1(1881 ^ []), 656 : v6_rlvect_1(1881 ^ []), 656 : v5_vectsp_2(1881 ^ [], 1860 ^ []), 656 : l1_vectsp_2(1881 ^ [], 1860 ^ []), 628 : -(v3_struct_0(1860 ^ [])), 628 : v3_rlvect_1(1860 ^ []), 628 : v4_rlvect_1(1860 ^ []), 628 : v5_rlvect_1(1860 ^ []), 628 : v6_rlvect_1(1860 ^ []), 628 : v4_group_1(1860 ^ []), 628 : v6_vectsp_1(1860 ^ []), 628 : v7_vectsp_1(1860 ^ []), 628 : v8_vectsp_1(1860 ^ []), 628 : l3_vectsp_1(1860 ^ [])],extension(588 ^ 11,bind([[_269664, _270629, _271335], [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]]))).
% 8.25/8.64 ncf('1.1.11.1.1',plain,[v1_rmod_5(k1_subset_1(u1_struct_0(1881 ^ [])), 1860 ^ [], 1881 ^ [])],extension(1897 ^ 18)).
% 8.25/8.64 ncf('1.1.11.1.2',plain,[-(m1_subset_1(k1_subset_1(u1_struct_0(1881 ^ [])), k1_zfmisc_1(u1_struct_0(1881 ^ []))))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.11.1.3',plain,[v3_struct_0(1881 ^ [])],extension(1883 ^ 14)).
% 8.25/8.64 ncf('1.1.11.1.4',plain,[-(v3_rlvect_1(1881 ^ []))],extension(1885 ^ 14)).
% 8.25/8.64 ncf('1.1.11.1.5',plain,[-(v4_rlvect_1(1881 ^ []))],extension(1887 ^ 14)).
% 8.25/8.64 ncf('1.1.11.1.6',plain,[-(v5_rlvect_1(1881 ^ []))],extension(1889 ^ 14)).
% 8.25/8.64 ncf('1.1.11.1.7',plain,[-(v6_rlvect_1(1881 ^ []))],extension(1891 ^ 14)).
% 8.25/8.64 ncf('1.1.11.1.8',plain,[-(v5_vectsp_2(1881 ^ [], 1860 ^ []))],extension(1893 ^ 14)).
% 8.25/8.64 ncf('1.1.11.1.9',plain,[-(l1_vectsp_2(1881 ^ [], 1860 ^ []))],extension(1895 ^ 14)).
% 8.25/8.64 ncf('1.1.11.1.10',plain,[v3_struct_0(1860 ^ [])],reduction('1')).
% 8.25/8.64 ncf('1.1.11.1.11',plain,[-(v3_rlvect_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.11.1.12',plain,[-(v4_rlvect_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.11.1.13',plain,[-(v5_rlvect_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.11.1.14',plain,[-(v6_rlvect_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.11.1.15',plain,[-(v4_group_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.11.1.16',plain,[-(v6_vectsp_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.11.1.17',plain,[-(v7_vectsp_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.11.1.18',plain,[-(v8_vectsp_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.11.1.19',plain,[-(l3_vectsp_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.11.2',plain,[v3_struct_0(1860 ^ [])],reduction('1')).
% 8.25/8.64 ncf('1.1.11.3',plain,[-(v3_rlvect_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.11.4',plain,[-(v4_rlvect_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.11.5',plain,[-(v5_rlvect_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.11.6',plain,[-(v6_rlvect_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.11.7',plain,[-(v4_group_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.11.8',plain,[-(v6_vectsp_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.11.9',plain,[-(v7_vectsp_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.11.10',plain,[-(v8_vectsp_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.11.11',plain,[-(l3_vectsp_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.11.12',plain,[v3_struct_0(1881 ^ [])],extension(1883 ^ 9)).
% 8.25/8.64 ncf('1.1.11.13',plain,[-(v3_rlvect_1(1881 ^ []))],extension(1885 ^ 9)).
% 8.25/8.64 ncf('1.1.11.14',plain,[-(v4_rlvect_1(1881 ^ []))],extension(1887 ^ 9)).
% 8.25/8.64 ncf('1.1.11.15',plain,[-(v5_rlvect_1(1881 ^ []))],extension(1889 ^ 9)).
% 8.25/8.64 ncf('1.1.11.16',plain,[-(v6_rlvect_1(1881 ^ []))],extension(1891 ^ 9)).
% 8.25/8.64 ncf('1.1.11.17',plain,[-(v5_vectsp_2(1881 ^ [], 1860 ^ []))],extension(1893 ^ 9)).
% 8.25/8.64 ncf('1.1.11.18',plain,[-(l1_vectsp_2(1881 ^ [], 1860 ^ []))],extension(1895 ^ 9)).
% 8.25/8.64 ncf('1.1.11.19',plain,[-(m1_subset_1(k1_subset_1(u1_struct_0(1881 ^ [])), k1_zfmisc_1(u1_struct_0(1881 ^ []))))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.12',plain,[-(m2_rmod_4(675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))], 1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ [])))), m2_rmod_4(675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))], 1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))), 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))] = 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))], 1860 ^ [] = 1860 ^ [], 1881 ^ [] = 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ [])) = k1_subset_1(u1_struct_0(1881 ^ []))],extension(80 ^ 10,bind([[_252705, _252707, _252709, _252711, _252713, _252715, _252717, _252719], [k1_subset_1(u1_struct_0(1881 ^ [])), k1_subset_1(u1_struct_0(1881 ^ [])), 1881 ^ [], 1881 ^ [], 1860 ^ [], 1860 ^ [], 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))], 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]]]))).
% 8.25/8.64 ncf('1.1.12.1',plain,[-(m2_rmod_4(675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))], 1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ [])))), m2_rmod_4(675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))], 1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))), 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))] = 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))], 1860 ^ [] = 1860 ^ [], 1881 ^ [] = 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ [])) = k1_subset_1(u1_struct_0(1881 ^ []))],extension(80 ^ 11,bind([[_252705, _252707, _252709, _252711, _252713, _252715, _252717, _252719], [k1_subset_1(u1_struct_0(1881 ^ [])), k1_subset_1(u1_struct_0(1881 ^ [])), 1881 ^ [], 1881 ^ [], 1860 ^ [], 1860 ^ [], 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))], 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]]]))).
% 8.25/8.64 ncf('1.1.12.1.1',plain,[-(m2_rmod_4(675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))], 1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ [])))), 674 : -(v1_rmod_5(k1_subset_1(u1_struct_0(1881 ^ [])), 1860 ^ [], 1881 ^ [])), 674 : m1_subset_1(k1_subset_1(u1_struct_0(1881 ^ [])), k1_zfmisc_1(u1_struct_0(1881 ^ []))), 656 : -(v3_struct_0(1881 ^ [])), 656 : v3_rlvect_1(1881 ^ []), 656 : v4_rlvect_1(1881 ^ []), 656 : v5_rlvect_1(1881 ^ []), 656 : v6_rlvect_1(1881 ^ []), 656 : v5_vectsp_2(1881 ^ [], 1860 ^ []), 656 : l1_vectsp_2(1881 ^ [], 1860 ^ []), 628 : -(v3_struct_0(1860 ^ [])), 628 : v3_rlvect_1(1860 ^ []), 628 : v4_rlvect_1(1860 ^ []), 628 : v5_rlvect_1(1860 ^ []), 628 : v6_rlvect_1(1860 ^ []), 628 : v4_group_1(1860 ^ []), 628 : v6_vectsp_1(1860 ^ []), 628 : v7_vectsp_1(1860 ^ []), 628 : v8_vectsp_1(1860 ^ []), 628 : l3_vectsp_1(1860 ^ [])],extension(588 ^ 12,bind([[_269664, _270629, _271335], [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]]))).
% 8.25/8.64 ncf('1.1.12.1.1.1',plain,[v1_rmod_5(k1_subset_1(u1_struct_0(1881 ^ [])), 1860 ^ [], 1881 ^ [])],extension(1897 ^ 19)).
% 8.25/8.64 ncf('1.1.12.1.1.2',plain,[-(m1_subset_1(k1_subset_1(u1_struct_0(1881 ^ [])), k1_zfmisc_1(u1_struct_0(1881 ^ []))))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.12.1.1.3',plain,[v3_struct_0(1881 ^ [])],extension(1883 ^ 15)).
% 8.25/8.64 ncf('1.1.12.1.1.4',plain,[-(v3_rlvect_1(1881 ^ []))],extension(1885 ^ 15)).
% 8.25/8.64 ncf('1.1.12.1.1.5',plain,[-(v4_rlvect_1(1881 ^ []))],extension(1887 ^ 15)).
% 8.25/8.64 ncf('1.1.12.1.1.6',plain,[-(v5_rlvect_1(1881 ^ []))],extension(1889 ^ 15)).
% 8.25/8.64 ncf('1.1.12.1.1.7',plain,[-(v6_rlvect_1(1881 ^ []))],extension(1891 ^ 15)).
% 8.25/8.64 ncf('1.1.12.1.1.8',plain,[-(v5_vectsp_2(1881 ^ [], 1860 ^ []))],extension(1893 ^ 15)).
% 8.25/8.64 ncf('1.1.12.1.1.9',plain,[-(l1_vectsp_2(1881 ^ [], 1860 ^ []))],extension(1895 ^ 15)).
% 8.25/8.64 ncf('1.1.12.1.1.10',plain,[v3_struct_0(1860 ^ [])],reduction('1')).
% 8.25/8.64 ncf('1.1.12.1.1.11',plain,[-(v3_rlvect_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.12.1.1.12',plain,[-(v4_rlvect_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.12.1.1.13',plain,[-(v5_rlvect_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.12.1.1.14',plain,[-(v6_rlvect_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.12.1.1.15',plain,[-(v4_group_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.12.1.1.16',plain,[-(v6_vectsp_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.12.1.1.17',plain,[-(v7_vectsp_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.12.1.1.18',plain,[-(v8_vectsp_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.12.1.1.19',plain,[-(l3_vectsp_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.12.1.2',plain,[-(675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))] = 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))])],extension(2 ^ 12,bind([[_250227], [675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]]]))).
% 8.25/8.64 ncf('1.1.12.1.3',plain,[-(1860 ^ [] = 1860 ^ [])],extension(2 ^ 12,bind([[_250227], [1860 ^ []]]))).
% 8.25/8.64 ncf('1.1.12.1.4',plain,[-(1881 ^ [] = 1881 ^ [])],extension(2 ^ 12,bind([[_250227], [1881 ^ []]]))).
% 8.25/8.64 ncf('1.1.12.1.5',plain,[-(k1_subset_1(u1_struct_0(1881 ^ [])) = k1_subset_1(u1_struct_0(1881 ^ [])))],extension(2 ^ 12,bind([[_250227], [k1_subset_1(u1_struct_0(1881 ^ []))]]))).
% 8.25/8.64 ncf('1.1.12.2',plain,[-(675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))] = 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))])],extension(2 ^ 11,bind([[_250227], [675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]]]))).
% 8.25/8.64 ncf('1.1.12.3',plain,[-(1860 ^ [] = 1860 ^ [])],extension(2 ^ 11,bind([[_250227], [1860 ^ []]]))).
% 8.25/8.64 ncf('1.1.12.4',plain,[-(1881 ^ [] = 1881 ^ [])],extension(2 ^ 11,bind([[_250227], [1881 ^ []]]))).
% 8.25/8.64 ncf('1.1.12.5',plain,[-(k1_subset_1(u1_struct_0(1881 ^ [])) = k1_subset_1(u1_struct_0(1881 ^ []))), u1_struct_0(1881 ^ []) = u1_struct_0(1881 ^ [])],extension(564 ^ 11,bind([[_268762, _268764], [u1_struct_0(1881 ^ []), u1_struct_0(1881 ^ [])]]))).
% 8.25/8.64 ncf('1.1.12.5.1',plain,[-(u1_struct_0(1881 ^ []) = u1_struct_0(1881 ^ [])), 1881 ^ [] = 1881 ^ []],extension(570 ^ 12,bind([[_268960, _268962], [1881 ^ [], 1881 ^ []]]))).
% 8.25/8.64 ncf('1.1.12.5.1.1',plain,[-(1881 ^ [] = 1881 ^ [])],lemmata('[1, 1].x')).
% 8.25/8.64 ncf('1.1.13',plain,[r1_tarski(k2_rmod_4(1860 ^ [], 1881 ^ [], 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]), k1_subset_1(u1_struct_0(1881 ^ []))), -(r1_tarski(k2_rmod_4(1860 ^ [], 1881 ^ [], 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]), k1_xboole_0)), k2_rmod_4(1860 ^ [], 1881 ^ [], 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]) = k2_rmod_4(1860 ^ [], 1881 ^ [], 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]), k1_subset_1(u1_struct_0(1881 ^ [])) = k1_xboole_0],extension(254 ^ 10,bind([[_258454, _258456, _258458, _258460], [k1_xboole_0, k1_subset_1(u1_struct_0(1881 ^ [])), k2_rmod_4(1860 ^ [], 1881 ^ [], 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]), k2_rmod_4(1860 ^ [], 1881 ^ [], 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))])]]))).
% 8.25/8.64 ncf('1.1.13.1',plain,[r1_tarski(k2_rmod_4(1860 ^ [], 1881 ^ [], 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]), k1_xboole_0), -(k2_rmod_4(1860 ^ [], 1881 ^ [], 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]) = k1_xboole_0)],extension(1813 ^ 11,bind([[_303764], [k2_rmod_4(1860 ^ [], 1881 ^ [], 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))])]]))).
% 8.25/8.64 ncf('1.1.13.1.1',plain,[k2_rmod_4(1860 ^ [], 1881 ^ [], 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]) = k1_xboole_0, 674 : -(v1_rmod_5(k1_subset_1(u1_struct_0(1881 ^ [])), 1860 ^ [], 1881 ^ [])), 674 : m1_subset_1(k1_subset_1(u1_struct_0(1881 ^ [])), k1_zfmisc_1(u1_struct_0(1881 ^ []))), 656 : -(v3_struct_0(1881 ^ [])), 656 : v3_rlvect_1(1881 ^ []), 656 : v4_rlvect_1(1881 ^ []), 656 : v5_rlvect_1(1881 ^ []), 656 : v6_rlvect_1(1881 ^ []), 656 : v5_vectsp_2(1881 ^ [], 1860 ^ []), 656 : l1_vectsp_2(1881 ^ [], 1860 ^ []), 628 : -(v3_struct_0(1860 ^ [])), 628 : v3_rlvect_1(1860 ^ []), 628 : v4_rlvect_1(1860 ^ []), 628 : v5_rlvect_1(1860 ^ []), 628 : v6_rlvect_1(1860 ^ []), 628 : v4_group_1(1860 ^ []), 628 : v6_vectsp_1(1860 ^ []), 628 : v7_vectsp_1(1860 ^ []), 628 : v8_vectsp_1(1860 ^ []), 628 : l3_vectsp_1(1860 ^ [])],extension(588 ^ 12,bind([[_269664, _270629, _271335], [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]]))).
% 8.25/8.64 ncf('1.1.13.1.1.1',plain,[v1_rmod_5(k1_subset_1(u1_struct_0(1881 ^ [])), 1860 ^ [], 1881 ^ [])],extension(1897 ^ 19)).
% 8.25/8.64 ncf('1.1.13.1.1.2',plain,[-(m1_subset_1(k1_subset_1(u1_struct_0(1881 ^ [])), k1_zfmisc_1(u1_struct_0(1881 ^ []))))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.13.1.1.3',plain,[v3_struct_0(1881 ^ [])],extension(1883 ^ 15)).
% 8.25/8.64 ncf('1.1.13.1.1.4',plain,[-(v3_rlvect_1(1881 ^ []))],extension(1885 ^ 15)).
% 8.25/8.64 ncf('1.1.13.1.1.5',plain,[-(v4_rlvect_1(1881 ^ []))],extension(1887 ^ 15)).
% 8.25/8.64 ncf('1.1.13.1.1.6',plain,[-(v5_rlvect_1(1881 ^ []))],extension(1889 ^ 15)).
% 8.25/8.64 ncf('1.1.13.1.1.7',plain,[-(v6_rlvect_1(1881 ^ []))],extension(1891 ^ 15)).
% 8.25/8.64 ncf('1.1.13.1.1.8',plain,[-(v5_vectsp_2(1881 ^ [], 1860 ^ []))],extension(1893 ^ 15)).
% 8.25/8.64 ncf('1.1.13.1.1.9',plain,[-(l1_vectsp_2(1881 ^ [], 1860 ^ []))],extension(1895 ^ 15)).
% 8.25/8.64 ncf('1.1.13.1.1.10',plain,[v3_struct_0(1860 ^ [])],reduction('1')).
% 8.25/8.64 ncf('1.1.13.1.1.11',plain,[-(v3_rlvect_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.13.1.1.12',plain,[-(v4_rlvect_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.13.1.1.13',plain,[-(v5_rlvect_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.13.1.1.14',plain,[-(v6_rlvect_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.13.1.1.15',plain,[-(v4_group_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.13.1.1.16',plain,[-(v6_vectsp_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.13.1.1.17',plain,[-(v7_vectsp_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.13.1.1.18',plain,[-(v8_vectsp_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.13.1.1.19',plain,[-(l3_vectsp_1(1860 ^ []))],lemmata('[1].x')).
% 8.25/8.64 ncf('1.1.13.2',plain,[-(k2_rmod_4(1860 ^ [], 1881 ^ [], 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]) = k2_rmod_4(1860 ^ [], 1881 ^ [], 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))])), 1860 ^ [] = 1860 ^ [], 1881 ^ [] = 1881 ^ [], 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))] = 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]],extension(452 ^ 11,bind([[_264709, _264711, _264713, _264715, _264717, _264719], [675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))], 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))], 1881 ^ [], 1881 ^ [], 1860 ^ [], 1860 ^ []]]))).
% 8.25/8.64 ncf('1.1.13.2.1',plain,[-(1860 ^ [] = 1860 ^ [])],extension(2 ^ 12,bind([[_250227], [1860 ^ []]]))).
% 8.25/8.64 ncf('1.1.13.2.2',plain,[-(1881 ^ [] = 1881 ^ [])],extension(2 ^ 12,bind([[_250227], [1881 ^ []]]))).
% 8.25/8.64 ncf('1.1.13.2.3',plain,[-(675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))] = 675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))])],extension(2 ^ 12,bind([[_250227], [675 ^ [1860 ^ [], 1881 ^ [], k1_subset_1(u1_struct_0(1881 ^ []))]]]))).
% 8.25/8.64 ncf('1.1.13.3',plain,[-(k1_subset_1(u1_struct_0(1881 ^ [])) = k1_xboole_0), v1_xboole_0(k1_subset_1(u1_struct_0(1881 ^ [])))],extension(1839 ^ 11,bind([[_304605], [k1_subset_1(u1_struct_0(1881 ^ []))]]))).
% 8.25/8.64 ncf('1.1.13.3.1',plain,[-(v1_xboole_0(k1_subset_1(u1_struct_0(1881 ^ []))))],extension(871 ^ 12,bind([[_277253], [u1_struct_0(1881 ^ [])]]))).
% 8.25/8.64 ncf('1.1.14',plain,[v3_struct_0(1881 ^ [])],extension(1883 ^ 4)).
% 8.25/8.64 ncf('1.1.15',plain,[-(v3_rlvect_1(1881 ^ []))],extension(1885 ^ 4)).
% 8.25/8.64 ncf('1.1.16',plain,[-(v4_rlvect_1(1881 ^ []))],extension(1887 ^ 4)).
% 8.25/8.64 ncf('1.1.17',plain,[-(v5_rlvect_1(1881 ^ []))],extension(1889 ^ 4)).
% 8.25/8.64 ncf('1.1.18',plain,[-(v6_rlvect_1(1881 ^ []))],extension(1891 ^ 4)).
% 8.25/8.64 ncf('1.1.19',plain,[-(v5_vectsp_2(1881 ^ [], 1860 ^ []))],extension(1893 ^ 4)).
% 8.25/8.64 ncf('1.1.20',plain,[-(l1_vectsp_2(1881 ^ [], 1860 ^ []))],extension(1895 ^ 4)).
% 8.25/8.64 %-----------------------------------------------------
% 8.25/8.64 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------