%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV036+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n028.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 12:19:49 EDT 2023
% Result : Theorem 158.26s 153.41s
% Output : Proof 158.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SWV036+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n028.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri May 19 02:51:03 EDT 2023
% 0.12/0.33 % CPUTime :
% 158.26/153.41
% 158.26/153.41 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 158.26/153.41 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 158.26/153.41 %-----------------------------------------------------
% 158.26/153.41 ncf(matrix, plain, [(849 ^ _364775) ^ [] : [init = init, s_best7_init = init, a_select2(s_values7_init, s_best7) = init, a_select2(s_values7_init, pv1388) = init, 1152 ^ _364775 : [(1153 ^ _364775) ^ [] : [-(gt(a_select2(s_values7, pv1388), a_select2(s_values7, s_best7)))], (1155 ^ _364775) ^ [] : [init = init, s_sworst7_init = init, s_worst7_init = init, leq(n0, s_sworst7), leq(n0, s_worst7), leq(n0, pv1388), leq(s_sworst7, n3), leq(s_worst7, n3), leq(pv1388, n3), 1193 ^ _364775 : [(1194 ^ _364775) ^ [] : [-(leq(n0, 1192 ^ []))], (1196 ^ _364775) ^ [] : [-(leq(1192 ^ [], n2))], (1199 ^ _364775) ^ [] : [-(leq(n0, 1197 ^ []))], (1201 ^ _364775) ^ [] : [-(leq(1197 ^ [], n3))], (1203 ^ _364775) ^ [] : [a_select3(simplex7_init, 1197 ^ [], 1192 ^ []) = init]], 1207 ^ _364775 : [(1208 ^ _364775) ^ [] : [-(leq(n0, 1206 ^ []))], (1210 ^ _364775) ^ [] : [-(leq(1206 ^ [], n3))], (1212 ^ _364775) ^ [] : [a_select2(s_values7_init, 1206 ^ []) = init]], 1216 ^ _364775 : [(1217 ^ _364775) ^ [] : [-(leq(n0, 1215 ^ []))], (1219 ^ _364775) ^ [] : [-(leq(1215 ^ [], n2))], (1221 ^ _364775) ^ [] : [a_select2(s_center7_init, 1215 ^ []) = init]], 1222 ^ _364775 : [(1223 ^ _364775) ^ [] : [-(gt(loopcounter, n1))], (1225 ^ _364775) ^ [] : [pvar1400_init = init, pvar1401_init = init, pvar1402_init = init]]]], 866 ^ _364775 : [(867 ^ _364775) ^ [] : [gt(a_select2(s_values7, pv1388), a_select2(s_values7, s_best7))], (869 ^ _364775) ^ [] : [init = init, s_worst7_init = init, a_select2(s_values7_init, s_worst7) = init, a_select2(s_values7_init, pv1388) = init, 1070 ^ _364775 : [(1071 ^ _364775) ^ [] : [-(leq(a_select2(s_values7, pv1388), a_select2(s_values7, s_worst7)))], (1073 ^ _364775) ^ [] : [init = init, s_best7_init = init, s_worst7_init = init, leq(n0, s_best7), leq(n0, s_worst7), leq(n0, pv1388), leq(s_best7, n3), leq(s_worst7, n3), leq(pv1388, n3), 1111 ^ _364775 : [(1112 ^ _364775) ^ [] : [-(leq(n0, 1110 ^ []))], (1114 ^ _364775) ^ [] : [-(leq(1110 ^ [], n2))], (1117 ^ _364775) ^ [] : [-(leq(n0, 1115 ^ []))], (1119 ^ _364775) ^ [] : [-(leq(1115 ^ [], n3))], (1121 ^ _364775) ^ [] : [a_select3(simplex7_init, 1115 ^ [], 1110 ^ []) = init]], 1125 ^ _364775 : [(1126 ^ _364775) ^ [] : [-(leq(n0, 1124 ^ []))], (1128 ^ _364775) ^ [] : [-(leq(1124 ^ [], n3))], (1130 ^ _364775) ^ [] : [a_select2(s_values7_init, 1124 ^ []) = init]], 1134 ^ _364775 : [(1135 ^ _364775) ^ [] : [-(leq(n0, 1133 ^ []))], (1137 ^ _364775) ^ [] : [-(leq(1133 ^ [], n2))], (1139 ^ _364775) ^ [] : [a_select2(s_center7_init, 1133 ^ []) = init]], 1140 ^ _364775 : [(1141 ^ _364775) ^ [] : [-(gt(loopcounter, n1))], (1143 ^ _364775) ^ [] : [pvar1400_init = init, pvar1401_init = init, pvar1402_init = init]]]], 886 ^ _364775 : [(887 ^ _364775) ^ [] : [leq(a_select2(s_values7, pv1388), a_select2(s_values7, s_worst7))], (889 ^ _364775) ^ [] : [init = init, s_sworst7_init = init, a_select2(s_values7_init, s_sworst7) = init, a_select2(s_values7_init, pv1388) = init, 906 ^ _364775 : [(907 ^ _364775) ^ [] : [leq(a_select2(s_values7, pv1388), a_select2(s_values7, s_sworst7))], (909 ^ _364775) ^ [] : [s_best7_init = init, s_sworst7_init = init, s_worst7_init = init, leq(n0, s_best7), leq(n0, s_sworst7), leq(n0, s_worst7), leq(s_best7, n3), leq(s_sworst7, n3), leq(s_worst7, n3), 947 ^ _364775 : [(948 ^ _364775) ^ [] : [-(leq(n0, 946 ^ []))], (950 ^ _364775) ^ [] : [-(leq(946 ^ [], n2))], (953 ^ _364775) ^ [] : [-(leq(n0, 951 ^ []))], (955 ^ _364775) ^ [] : [-(leq(951 ^ [], n3))], (957 ^ _364775) ^ [] : [a_select3(simplex7_init, 951 ^ [], 946 ^ []) = init]], 961 ^ _364775 : [(962 ^ _364775) ^ [] : [-(leq(n0, 960 ^ []))], (964 ^ _364775) ^ [] : [-(leq(960 ^ [], n3))], (966 ^ _364775) ^ [] : [a_select2(s_values7_init, 960 ^ []) = init]], 970 ^ _364775 : [(971 ^ _364775) ^ [] : [-(leq(n0, 969 ^ []))], (973 ^ _364775) ^ [] : [-(leq(969 ^ [], n2))], (975 ^ _364775) ^ [] : [a_select2(s_center7_init, 969 ^ []) = init]], 976 ^ _364775 : [(977 ^ _364775) ^ [] : [-(gt(loopcounter, n1))], (979 ^ _364775) ^ [] : [pvar1400_init = init, pvar1401_init = init, pvar1402_init = init]]]], 988 ^ _364775 : [(989 ^ _364775) ^ [] : [-(leq(a_select2(s_values7, pv1388), a_select2(s_values7, s_sworst7)))], (991 ^ _364775) ^ [] : [init = init, s_best7_init = init, s_worst7_init = init, leq(n0, s_best7), leq(n0, s_worst7), leq(n0, pv1388), leq(s_best7, n3), leq(s_worst7, n3), leq(pv1388, n3), 1029 ^ _364775 : [(1030 ^ _364775) ^ [] : [-(leq(n0, 1028 ^ []))], (1032 ^ _364775) ^ [] : [-(leq(1028 ^ [], n2))], (1035 ^ _364775) ^ [] : [-(leq(n0, 1033 ^ []))], (1037 ^ _364775) ^ [] : [-(leq(1033 ^ [], n3))], (1039 ^ _364775) ^ [] : [a_select3(simplex7_init, 1033 ^ [], 1028 ^ []) = init]], 1043 ^ _364775 : [(1044 ^ _364775) ^ [] : [-(leq(n0, 1042 ^ []))], (1046 ^ _364775) ^ [] : [-(leq(1042 ^ [], n3))], (1048 ^ _364775) ^ [] : [a_select2(s_values7_init, 1042 ^ []) = init]], 1052 ^ _364775 : [(1053 ^ _364775) ^ [] : [-(leq(n0, 1051 ^ []))], (1055 ^ _364775) ^ [] : [-(leq(1051 ^ [], n2))], (1057 ^ _364775) ^ [] : [a_select2(s_center7_init, 1051 ^ []) = init]], 1058 ^ _364775 : [(1059 ^ _364775) ^ [] : [-(gt(loopcounter, n1))], (1061 ^ _364775) ^ [] : [pvar1400_init = init, pvar1401_init = init, pvar1402_init = init]]]]]]]]], (779 ^ _364775) ^ [] : [-(s_best7_init = init)], (781 ^ _364775) ^ [] : [-(s_sworst7_init = init)], (783 ^ _364775) ^ [] : [-(s_worst7_init = init)], (785 ^ _364775) ^ [] : [-(leq(n0, s_best7))], (787 ^ _364775) ^ [] : [-(leq(n0, s_sworst7))], (789 ^ _364775) ^ [] : [-(leq(n0, s_worst7))], (791 ^ _364775) ^ [] : [-(leq(n2, pv1388))], (793 ^ _364775) ^ [] : [-(leq(s_best7, n3))], (795 ^ _364775) ^ [] : [-(leq(s_sworst7, n3))], (797 ^ _364775) ^ [] : [-(leq(s_worst7, n3))], (799 ^ _364775) ^ [] : [-(leq(pv1388, n3))], (801 ^ _364775) ^ [_395883] : [leq(n0, _395883), leq(_395883, n2), 808 ^ _364775 : [(809 ^ _364775) ^ [_396111] : [-(a_select3(simplex7_init, _396111, _395883) = init), leq(n0, _396111), leq(_396111, n3)]]], (819 ^ _364775) ^ [_396413] : [-(a_select2(s_values7_init, _396413) = init), leq(n0, _396413), leq(_396413, n3)], (839 ^ _364775) ^ [] : [gt(loopcounter, n1), 842 ^ _364775 : [(843 ^ _364775) ^ [] : [-(pvar1400_init = init)], (845 ^ _364775) ^ [] : [-(pvar1401_init = init)], (847 ^ _364775) ^ [] : [-(pvar1402_init = init)]]], (829 ^ _364775) ^ [_396694] : [-(a_select2(s_center7_init, _396694) = init), leq(n0, _396694), leq(_396694, n2)], (607 ^ _364775) ^ [] : [-(gt(n5, n4))], (609 ^ _364775) ^ [] : [-(gt(n4, tptp_minus_1))], (611 ^ _364775) ^ [] : [-(gt(n5, tptp_minus_1))], (613 ^ _364775) ^ [] : [-(gt(n0, tptp_minus_1))], (615 ^ _364775) ^ [] : [-(gt(n1, tptp_minus_1))], (617 ^ _364775) ^ [] : [-(gt(n2, tptp_minus_1))], (619 ^ _364775) ^ [] : [-(gt(n3, tptp_minus_1))], (621 ^ _364775) ^ [] : [-(gt(n4, n0))], (623 ^ _364775) ^ [] : [-(gt(n5, n0))], (625 ^ _364775) ^ [] : [-(gt(n1, n0))], (627 ^ _364775) ^ [] : [-(gt(n2, n0))], (629 ^ _364775) ^ [] : [-(gt(n3, n0))], (631 ^ _364775) ^ [] : [-(gt(n4, n1))], (633 ^ _364775) ^ [] : [-(gt(n5, n1))], (635 ^ _364775) ^ [] : [-(gt(n2, n1))], (637 ^ _364775) ^ [] : [-(gt(n3, n1))], (639 ^ _364775) ^ [] : [-(gt(n4, n2))], (641 ^ _364775) ^ [] : [-(gt(n5, n2))], (643 ^ _364775) ^ [] : [-(gt(n3, n2))], (645 ^ _364775) ^ [] : [-(gt(n4, n3))], (647 ^ _364775) ^ [] : [-(gt(n5, n3))], (649 ^ _364775) ^ [_391946] : [leq(n0, _391946), leq(_391946, n4), -(_391946 = n0), -(_391946 = n1), -(_391946 = n2), -(_391946 = n3), -(_391946 = n4)], (675 ^ _364775) ^ [_392567] : [leq(n0, _392567), leq(_392567, n5), -(_392567 = n0), -(_392567 = n1), -(_392567 = n2), -(_392567 = n3), -(_392567 = n4), -(_392567 = n5)], (705 ^ _364775) ^ [_393274] : [-(_393274 = n0), leq(n0, _393274), leq(_393274, n0)], (715 ^ _364775) ^ [_393549] : [leq(n0, _393549), leq(_393549, n1), -(_393549 = n0), -(_393549 = n1)], (729 ^ _364775) ^ [_393912] : [leq(n0, _393912), leq(_393912, n2), -(_393912 = n0), -(_393912 = n1), -(_393912 = n2)], (769 ^ _364775) ^ [] : [-(succ(succ(succ(succ(n0)))) = n4)], (771 ^ _364775) ^ [] : [-(succ(succ(succ(succ(succ(n0))))) = n5)], (773 ^ _364775) ^ [] : [-(succ(n0) = n1)], (775 ^ _364775) ^ [] : [-(succ(succ(n0)) = n2)], (777 ^ _364775) ^ [] : [-(succ(succ(succ(n0))) = n3)], (747 ^ _364775) ^ [_394361] : [leq(n0, _394361), leq(_394361, n3), -(_394361 = n0), -(_394361 = n1), -(_394361 = n2), -(_394361 = n3)], (2 ^ _364775) ^ [_364908, _364910] : [-(gt(_364910, _364908)), -(gt(_364908, _364910)), -(_364910 = _364908)], (12 ^ _364775) ^ [_365223, _365225, _365227] : [-(gt(_365227, _365223)), gt(_365227, _365225), gt(_365225, _365223)], (22 ^ _364775) ^ [_365502] : [gt(_365502, _365502)], (24 ^ _364775) ^ [_365580] : [-(leq(_365580, _365580))], (26 ^ _364775) ^ [_365701, _365703, _365705] : [-(leq(_365705, _365701)), leq(_365705, _365703), leq(_365703, _365701)], (36 ^ _364775) ^ [_366039, _366041] : [lt(_366041, _366039), -(gt(_366039, _366041))], (42 ^ _364775) ^ [_366201, _366203] : [gt(_366201, _366203), -(lt(_366203, _366201))], (48 ^ _364775) ^ [_366442, _366444] : [geq(_366444, _366442), -(leq(_366442, _366444))], (54 ^ _364775) ^ [_366604, _366606] : [leq(_366604, _366606), -(geq(_366606, _366604))], (60 ^ _364775) ^ [_366816, _366818] : [gt(_366816, _366818), -(leq(_366818, _366816))], (66 ^ _364775) ^ [_367026, _367028] : [-(gt(_367026, _367028)), leq(_367028, _367026), -(_367028 = _367026)], (76 ^ _364775) ^ [_367357, _367359] : [leq(_367359, pred(_367357)), -(gt(_367357, _367359))], (82 ^ _364775) ^ [_367523, _367525] : [gt(_367523, _367525), -(leq(_367525, pred(_367523)))], (88 ^ _364775) ^ [_367710] : [-(gt(succ(_367710), _367710))], (90 ^ _364775) ^ [_367819, _367821] : [leq(_367821, _367819), -(leq(_367821, succ(_367819)))], (96 ^ _364775) ^ [_368062, _368064] : [leq(_368064, _368062), -(gt(succ(_368062), _368064))], (102 ^ _364775) ^ [_368228, _368230] : [gt(succ(_368228), _368230), -(leq(_368230, _368228))], (108 ^ _364775) ^ [_368444, _368446] : [leq(n0, _368446), -(leq(uniform_int_rnd(_368444, _368446), _368446))], (114 ^ _364775) ^ [_368660, _368662] : [leq(n0, _368662), -(leq(n0, uniform_int_rnd(_368660, _368662)))], (120 ^ _364775) ^ [_368904, _368906, _368908, _368910] : [-(a_select2(tptp_const_array1(dim(_368908, _368906), _368904), _368910) = _368904), leq(_368908, _368910), leq(_368910, _368906)], (130 ^ _364775) ^ [_369311, _369313, _369315, _369317, _369319, _369321, _369323] : [-(a_select3(tptp_const_array2(dim(_369321, _369319), dim(_369315, _369313), _369311), _369323, _369317) = _369311), leq(_369321, _369323), leq(_369323, _369319), leq(_369315, _369317), leq(_369317, _369313)], (148 ^ _364775) ^ [_369906, _369908] : [151 ^ _364775 : [(152 ^ _364775) ^ [] : [-(leq(n0, 149 ^ [_369906, _369908]))], (154 ^ _364775) ^ [] : [-(leq(149 ^ [_369906, _369908], _369906))], (156 ^ _364775) ^ [] : [-(leq(n0, 150 ^ [_369906, _369908]))], (158 ^ _364775) ^ [] : [-(leq(150 ^ [_369906, _369908], _369906))], (160 ^ _364775) ^ [] : [a_select3(_369908, 149 ^ [_369906, _369908], 150 ^ [_369906, _369908]) = a_select3(_369908, 150 ^ [_369906, _369908], 149 ^ [_369906, _369908])]], 161 ^ _364775 : [(162 ^ _364775) ^ [_370663, _370665] : [-(a_select3(trans(_369908), _370665, _370663) = a_select3(trans(_369908), _370663, _370665)), leq(n0, _370665), leq(_370665, _369906), leq(n0, _370663), leq(_370663, _369906)]]], (180 ^ _364775) ^ [_371210, _371212] : [183 ^ _364775 : [(184 ^ _364775) ^ [] : [-(leq(n0, 181 ^ [_371210, _371212]))], (186 ^ _364775) ^ [] : [-(leq(181 ^ [_371210, _371212], _371210))], (188 ^ _364775) ^ [] : [-(leq(n0, 182 ^ [_371210, _371212]))], (190 ^ _364775) ^ [] : [-(leq(182 ^ [_371210, _371212], _371210))], (192 ^ _364775) ^ [] : [a_select3(_371212, 181 ^ [_371210, _371212], 182 ^ [_371210, _371212]) = a_select3(_371212, 182 ^ [_371210, _371212], 181 ^ [_371210, _371212])]], 193 ^ _364775 : [(194 ^ _364775) ^ [_371967, _371969] : [-(a_select3(inv(_371212), _371969, _371967) = a_select3(inv(_371212), _371967, _371969)), leq(n0, _371969), leq(_371969, _371210), leq(n0, _371967), leq(_371967, _371210)]]], (212 ^ _364775) ^ [_372514, _372516] : [215 ^ _364775 : [(216 ^ _364775) ^ [] : [-(leq(n0, 213 ^ [_372514, _372516]))], (218 ^ _364775) ^ [] : [-(leq(213 ^ [_372514, _372516], _372514))], (220 ^ _364775) ^ [] : [-(leq(n0, 214 ^ [_372514, _372516]))], (222 ^ _364775) ^ [] : [-(leq(214 ^ [_372514, _372516], _372514))], (224 ^ _364775) ^ [] : [a_select3(_372516, 213 ^ [_372514, _372516], 214 ^ [_372514, _372516]) = a_select3(_372516, 214 ^ [_372514, _372516], 213 ^ [_372514, _372516])]], 225 ^ _364775 : [(226 ^ _364775) ^ [_373327, _373329, _373331, _373333] : [-(a_select3(tptp_update3(_372516, _373329, _373329, _373327), _373333, _373331) = a_select3(tptp_update3(_372516, _373329, _373329, _373327), _373331, _373333)), leq(n0, _373333), leq(_373333, _372514), leq(n0, _373331), leq(_373331, _372514), leq(n0, _373329), leq(_373329, _372514)]]], (252 ^ _364775) ^ [_374146, _374148, _374150] : [257 ^ _364775 : [(258 ^ _364775) ^ [] : [-(leq(n0, 255 ^ [_374146, _374148, _374150]))], (260 ^ _364775) ^ [] : [-(leq(255 ^ [_374146, _374148, _374150], _374146))], (262 ^ _364775) ^ [] : [-(leq(n0, 256 ^ [_374146, _374148, _374150]))], (264 ^ _364775) ^ [] : [-(leq(256 ^ [_374146, _374148, _374150], _374146))], (266 ^ _364775) ^ [] : [a_select3(_374150, 255 ^ [_374146, _374148, _374150], 256 ^ [_374146, _374148, _374150]) = a_select3(_374150, 256 ^ [_374146, _374148, _374150], 255 ^ [_374146, _374148, _374150])]], 269 ^ _364775 : [(270 ^ _364775) ^ [] : [-(leq(n0, 267 ^ [_374146, _374148, _374150]))], (272 ^ _364775) ^ [] : [-(leq(267 ^ [_374146, _374148, _374150], _374146))], (274 ^ _364775) ^ [] : [-(leq(n0, 268 ^ [_374146, _374148, _374150]))], (276 ^ _364775) ^ [] : [-(leq(268 ^ [_374146, _374148, _374150], _374146))], (278 ^ _364775) ^ [] : [a_select3(_374148, 267 ^ [_374146, _374148, _374150], 268 ^ [_374146, _374148, _374150]) = a_select3(_374148, 268 ^ [_374146, _374148, _374150], 267 ^ [_374146, _374148, _374150])]], 279 ^ _364775 : [(280 ^ _364775) ^ [_375655, _375657] : [-(a_select3(tptp_madd(_374150, _374148), _375657, _375655) = a_select3(tptp_madd(_374150, _374148), _375655, _375657)), leq(n0, _375657), leq(_375657, _374146), leq(n0, _375655), leq(_375655, _374146)]]], (298 ^ _364775) ^ [_376241, _376243, _376245] : [303 ^ _364775 : [(304 ^ _364775) ^ [] : [-(leq(n0, 301 ^ [_376241, _376243, _376245]))], (306 ^ _364775) ^ [] : [-(leq(301 ^ [_376241, _376243, _376245], _376241))], (308 ^ _364775) ^ [] : [-(leq(n0, 302 ^ [_376241, _376243, _376245]))], (310 ^ _364775) ^ [] : [-(leq(302 ^ [_376241, _376243, _376245], _376241))], (312 ^ _364775) ^ [] : [a_select3(_376245, 301 ^ [_376241, _376243, _376245], 302 ^ [_376241, _376243, _376245]) = a_select3(_376245, 302 ^ [_376241, _376243, _376245], 301 ^ [_376241, _376243, _376245])]], 315 ^ _364775 : [(316 ^ _364775) ^ [] : [-(leq(n0, 313 ^ [_376241, _376243, _376245]))], (318 ^ _364775) ^ [] : [-(leq(313 ^ [_376241, _376243, _376245], _376241))], (320 ^ _364775) ^ [] : [-(leq(n0, 314 ^ [_376241, _376243, _376245]))], (322 ^ _364775) ^ [] : [-(leq(314 ^ [_376241, _376243, _376245], _376241))], (324 ^ _364775) ^ [] : [a_select3(_376243, 313 ^ [_376241, _376243, _376245], 314 ^ [_376241, _376243, _376245]) = a_select3(_376243, 314 ^ [_376241, _376243, _376245], 313 ^ [_376241, _376243, _376245])]], 325 ^ _364775 : [(326 ^ _364775) ^ [_377750, _377752] : [-(a_select3(tptp_msub(_376245, _376243), _377752, _377750) = a_select3(tptp_msub(_376245, _376243), _377750, _377752)), leq(n0, _377752), leq(_377752, _376241), leq(n0, _377750), leq(_377750, _376241)]]], (344 ^ _364775) ^ [_378336, _378338, _378340] : [347 ^ _364775 : [(348 ^ _364775) ^ [] : [-(leq(n0, 345 ^ [_378336, _378338, _378340]))], (350 ^ _364775) ^ [] : [-(leq(345 ^ [_378336, _378338, _378340], _378336))], (352 ^ _364775) ^ [] : [-(leq(n0, 346 ^ [_378336, _378338, _378340]))], (354 ^ _364775) ^ [] : [-(leq(346 ^ [_378336, _378338, _378340], _378336))], (356 ^ _364775) ^ [] : [a_select3(_378338, 345 ^ [_378336, _378338, _378340], 346 ^ [_378336, _378338, _378340]) = a_select3(_378338, 346 ^ [_378336, _378338, _378340], 345 ^ [_378336, _378338, _378340])]], 357 ^ _364775 : [(358 ^ _364775) ^ [_379149, _379151] : [-(a_select3(tptp_mmul(_378340, tptp_mmul(_378338, trans(_378340))), _379151, _379149) = a_select3(tptp_mmul(_378340, tptp_mmul(_378338, trans(_378340))), _379149, _379151)), leq(n0, _379151), leq(_379151, _378336), leq(n0, _379149), leq(_379149, _378336)]]], (376 ^ _364775) ^ [_379768, _379770, _379772, _379774] : [379 ^ _364775 : [(380 ^ _364775) ^ [] : [-(leq(n0, 377 ^ [_379768, _379770, _379772, _379774]))], (382 ^ _364775) ^ [] : [-(leq(377 ^ [_379768, _379770, _379772, _379774], _379768))], (384 ^ _364775) ^ [] : [-(leq(n0, 378 ^ [_379768, _379770, _379772, _379774]))], (386 ^ _364775) ^ [] : [-(leq(378 ^ [_379768, _379770, _379772, _379774], _379768))], (388 ^ _364775) ^ [] : [a_select3(_379772, 377 ^ [_379768, _379770, _379772, _379774], 378 ^ [_379768, _379770, _379772, _379774]) = a_select3(_379772, 378 ^ [_379768, _379770, _379772, _379774], 377 ^ [_379768, _379770, _379772, _379774])]], 389 ^ _364775 : [(390 ^ _364775) ^ [_380625, _380627] : [-(a_select3(tptp_mmul(_379774, tptp_mmul(_379772, trans(_379774))), _380627, _380625) = a_select3(tptp_mmul(_379774, tptp_mmul(_379772, trans(_379774))), _380625, _380627)), leq(n0, _380627), leq(_380627, _379770), leq(n0, _380625), leq(_380625, _379770)]]], (408 ^ _364775) ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334] : [413 ^ _364775 : [(414 ^ _364775) ^ [] : [-(leq(n0, 411 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334]))], (416 ^ _364775) ^ [] : [-(leq(411 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334], _381320))], (418 ^ _364775) ^ [] : [-(leq(n0, 412 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334]))], (420 ^ _364775) ^ [] : [-(leq(412 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334], _381320))], (422 ^ _364775) ^ [] : [a_select3(_381328, 411 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334], 412 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334]) = a_select3(_381328, 412 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334], 411 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334])]], 427 ^ _364775 : [(428 ^ _364775) ^ [] : [-(leq(n0, 425 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334]))], (430 ^ _364775) ^ [] : [-(leq(425 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334], _381322))], (432 ^ _364775) ^ [] : [-(leq(n0, 426 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334]))], (434 ^ _364775) ^ [] : [-(leq(426 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334], _381322))], (436 ^ _364775) ^ [] : [a_select3(_381334, 425 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334], 426 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334]) = a_select3(_381334, 426 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334], 425 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334])]], 439 ^ _364775 : [(440 ^ _364775) ^ [] : [-(leq(n0, 437 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334]))], (442 ^ _364775) ^ [] : [-(leq(437 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334], _381322))], (444 ^ _364775) ^ [] : [-(leq(n0, 438 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334]))], (446 ^ _364775) ^ [] : [-(leq(438 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334], _381322))], (448 ^ _364775) ^ [] : [a_select3(_381324, 437 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334], 438 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334]) = a_select3(_381324, 438 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334], 437 ^ [_381320, _381322, _381324, _381326, _381328, _381330, _381332, _381334])]], 449 ^ _364775 : [(450 ^ _364775) ^ [_384248, _384250] : [-(a_select3(tptp_madd(_381334, tptp_mmul(_381332, tptp_mmul(tptp_madd(tptp_mmul(_381330, tptp_mmul(_381328, trans(_381330))), tptp_mmul(_381326, tptp_mmul(_381324, trans(_381326)))), trans(_381332)))), _384250, _384248) = a_select3(tptp_madd(_381334, tptp_mmul(_381332, tptp_mmul(tptp_madd(tptp_mmul(_381330, tptp_mmul(_381328, trans(_381330))), tptp_mmul(_381326, tptp_mmul(_381324, trans(_381326)))), trans(_381332)))), _384248, _384250)), leq(n0, _384250), leq(_384250, _381322), leq(n0, _384248), leq(_384248, _381322)]]], (468 ^ _364775) ^ [_385001] : [-(sum(n0, tptp_minus_1, _385001) = n0)], (470 ^ _364775) ^ [_385083] : [-(tptp_float_0_0 = sum(n0, tptp_minus_1, _385083))], (472 ^ _364775) ^ [] : [-(succ(tptp_minus_1) = n0)], (474 ^ _364775) ^ [_385218] : [-(plus(_385218, n1) = succ(_385218))], (476 ^ _364775) ^ [_385301] : [-(plus(n1, _385301) = succ(_385301))], (478 ^ _364775) ^ [_385384] : [-(plus(_385384, n2) = succ(succ(_385384)))], (480 ^ _364775) ^ [_385469] : [-(plus(n2, _385469) = succ(succ(_385469)))], (482 ^ _364775) ^ [_385554] : [-(plus(_385554, n3) = succ(succ(succ(_385554))))], (484 ^ _364775) ^ [_385641] : [-(plus(n3, _385641) = succ(succ(succ(_385641))))], (486 ^ _364775) ^ [_385728] : [-(plus(_385728, n4) = succ(succ(succ(succ(_385728)))))], (488 ^ _364775) ^ [_385817] : [-(plus(n4, _385817) = succ(succ(succ(succ(_385817)))))], (490 ^ _364775) ^ [_385906] : [-(plus(_385906, n5) = succ(succ(succ(succ(succ(_385906))))))], (492 ^ _364775) ^ [_385997] : [-(plus(n5, _385997) = succ(succ(succ(succ(succ(_385997))))))], (494 ^ _364775) ^ [_386088] : [-(minus(_386088, n1) = pred(_386088))], (496 ^ _364775) ^ [_386171] : [-(pred(succ(_386171)) = _386171)], (498 ^ _364775) ^ [_386253] : [-(succ(pred(_386253)) = _386253)], (500 ^ _364775) ^ [_386393, _386395] : [leq(succ(_386395), succ(_386393)), -(leq(_386395, _386393))], (506 ^ _364775) ^ [_386563, _386565] : [leq(_386565, _386563), -(leq(succ(_386565), succ(_386563)))], (512 ^ _364775) ^ [_386783, _386785] : [leq(succ(_386785), _386783), -(gt(_386783, _386785))], (518 ^ _364775) ^ [_386997, _386999] : [leq(minus(_386999, _386997), _386999), -(leq(n0, _386997))], (524 ^ _364775) ^ [_387226, _387228, _387230, _387232] : [-(a_select3(tptp_update3(_387232, _387230, _387228, _387226), _387230, _387228) = _387226)], (526 ^ _364775) ^ [_387418, _387420, _387422, _387424, _387426, _387428, _387430] : [-(a_select3(tptp_update3(_387422, _387430, _387428, _387418), _387426, _387424) = _387420), -(_387430 = _387426), _387428 = _387424, a_select3(_387422, _387426, _387424) = _387420], (540 ^ _364775) ^ [_387961, _387963, _387965, _387967, _387969, _387971] : [-(a_select3(tptp_update3(_387963, _387967, _387965, _387961), _387971, _387969) = _387961), 545 ^ _364775 : [(546 ^ _364775) ^ [] : [-(leq(n0, 543 ^ [_387961, _387963, _387965, _387967, _387969, _387971]))], (548 ^ _364775) ^ [] : [-(leq(n0, 544 ^ [_387961, _387963, _387965, _387967, _387969, _387971]))], (550 ^ _364775) ^ [] : [-(leq(543 ^ [_387961, _387963, _387965, _387967, _387969, _387971], _387967))], (552 ^ _364775) ^ [] : [-(leq(544 ^ [_387961, _387963, _387965, _387967, _387969, _387971], _387965))], (554 ^ _364775) ^ [] : [a_select3(_387963, 543 ^ [_387961, _387963, _387965, _387967, _387969, _387971], 544 ^ [_387961, _387963, _387965, _387967, _387969, _387971]) = _387961]], leq(n0, _387971), leq(_387971, _387967), leq(n0, _387969), leq(_387969, _387965)], (572 ^ _364775) ^ [_389303, _389305, _389307] : [-(a_select2(tptp_update2(_389307, _389305, _389303), _389305) = _389303)], (574 ^ _364775) ^ [_389463, _389465, _389467, _389469, _389471] : [-(a_select2(tptp_update2(_389467, _389471, _389463), _389469) = _389465), -(_389471 = _389469), a_select2(_389467, _389469) = _389465], (603 ^ _364775) ^ [] : [-(true)], (605 ^ _364775) ^ [] : [def = use], (584 ^ _364775) ^ [_389843, _389845, _389847, _389849] : [-(a_select2(tptp_update2(_389845, _389847, _389843), _389849) = _389843), 588 ^ _364775 : [(589 ^ _364775) ^ [] : [-(leq(n0, 587 ^ [_389843, _389845, _389847, _389849]))], (591 ^ _364775) ^ [] : [-(leq(587 ^ [_389843, _389845, _389847, _389849], _389847))], (593 ^ _364775) ^ [] : [a_select2(_389845, 587 ^ [_389843, _389845, _389847, _389849]) = _389843]], leq(n0, _389849), leq(_389849, _389847)]], input).
% 158.26/153.41 ncf('1',plain,[init = init, s_best7_init = init, a_select2(s_values7_init, s_best7) = init, a_select2(s_values7_init, pv1388) = init, 1155 : init = init, 1155 : s_sworst7_init = init, 1155 : s_worst7_init = init, 1155 : leq(n0, s_sworst7), 1155 : leq(n0, s_worst7), 1155 : leq(n0, pv1388), 1155 : leq(s_sworst7, n3), 1155 : leq(s_worst7, n3), 1155 : leq(pv1388, n3), 1203 : a_select3(simplex7_init, 1197 ^ [], 1192 ^ []) = init, 1212 : a_select2(s_values7_init, 1206 ^ []) = init, 1221 : a_select2(s_center7_init, 1215 ^ []) = init, 1225 : pvar1400_init = init, 1225 : pvar1401_init = init, 1225 : pvar1402_init = init, 869 : init = init, 869 : s_worst7_init = init, 869 : a_select2(s_values7_init, s_worst7) = init, 869 : a_select2(s_values7_init, pv1388) = init, 1073 : init = init, 1073 : s_best7_init = init, 1073 : s_worst7_init = init, 1073 : leq(n0, s_best7), 1073 : leq(n0, s_worst7), 1073 : leq(n0, pv1388), 1073 : leq(s_best7, n3), 1073 : leq(s_worst7, n3), 1073 : leq(pv1388, n3), 1121 : a_select3(simplex7_init, 1115 ^ [], 1110 ^ []) = init, 1130 : a_select2(s_values7_init, 1124 ^ []) = init, 1139 : a_select2(s_center7_init, 1133 ^ []) = init, 1143 : pvar1400_init = init, 1143 : pvar1401_init = init, 1143 : pvar1402_init = init, 889 : init = init, 889 : s_sworst7_init = init, 889 : a_select2(s_values7_init, s_sworst7) = init, 889 : a_select2(s_values7_init, pv1388) = init, 909 : s_best7_init = init, 909 : s_sworst7_init = init, 909 : s_worst7_init = init, 909 : leq(n0, s_best7), 909 : leq(n0, s_sworst7), 909 : leq(n0, s_worst7), 909 : leq(s_best7, n3), 909 : leq(s_sworst7, n3), 909 : leq(s_worst7, n3), 957 : a_select3(simplex7_init, 951 ^ [], 946 ^ []) = init, 966 : a_select2(s_values7_init, 960 ^ []) = init, 975 : a_select2(s_center7_init, 969 ^ []) = init, 979 : pvar1400_init = init, 979 : pvar1401_init = init, 979 : pvar1402_init = init, 991 : init = init, 991 : s_best7_init = init, 991 : s_worst7_init = init, 991 : leq(n0, s_best7), 991 : leq(n0, s_worst7), 991 : leq(n0, pv1388), 991 : leq(s_best7, n3), 991 : leq(s_worst7, n3), 991 : leq(pv1388, n3), 1039 : a_select3(simplex7_init, 1033 ^ [], 1028 ^ []) = init, 1048 : a_select2(s_values7_init, 1042 ^ []) = init, 1057 : a_select2(s_center7_init, 1051 ^ []) = init, 1061 : pvar1400_init = init, 1061 : pvar1401_init = init, 1061 : pvar1402_init = init],start(849 ^ 0)).
% 158.26/153.41 ncf('1.1',plain,[-(init = init), -(gt(init, init)), -(gt(init, init))],extension(2 ^ 1,bind([[_364908, _364910], [init, init]]))).
% 158.26/153.41 ncf('1.1.1',plain,[gt(init, init), -(gt(init, init)), gt(init, init)],extension(12 ^ 2,bind([[_365223, _365225, _365227], [init, init, init]]))).
% 158.26/153.41 ncf('1.1.1.1',plain,[gt(init, init)],extension(22 ^ 3,bind([[_365502], [init]]))).
% 158.26/153.41 ncf('1.1.1.2',plain,[-(gt(init, init))],reduction('1.1')).
% 158.26/153.41 ncf('1.1.2',plain,[gt(init, init)],lemmata('[1].x')).
% 158.26/153.41 ncf('1.2',plain,[-(s_best7_init = init)],extension(779 ^ 1)).
% 158.26/153.41 ncf('1.3',plain,[-(a_select2(s_values7_init, s_best7) = init), leq(n0, s_best7), leq(s_best7, n3)],extension(819 ^ 1,bind([[_396413], [s_best7]]))).
% 158.26/153.41 ncf('1.3.1',plain,[-(leq(n0, s_best7))],extension(785 ^ 2)).
% 158.26/153.41 ncf('1.3.2',plain,[-(leq(s_best7, n3))],extension(793 ^ 2)).
% 158.26/153.41 ncf('1.4',plain,[-(a_select2(s_values7_init, pv1388) = init), leq(n0, pv1388), leq(pv1388, n3)],extension(819 ^ 1,bind([[_396413], [pv1388]]))).
% 158.26/153.41 ncf('1.4.1',plain,[-(leq(n0, pv1388)), leq(n0, n2), leq(n2, pv1388)],extension(26 ^ 2,bind([[_365701, _365703, _365705], [pv1388, n2, n0]]))).
% 158.26/153.41 ncf('1.4.1.1',plain,[-(leq(n0, n2)), gt(n2, n0)],extension(60 ^ 3,bind([[_366816, _366818], [n2, n0]]))).
% 158.26/153.41 ncf('1.4.1.1.1',plain,[-(gt(n2, n0))],extension(627 ^ 4)).
% 158.26/153.41 ncf('1.4.1.2',plain,[-(leq(n2, pv1388))],extension(791 ^ 3)).
% 158.26/153.41 ncf('1.4.2',plain,[-(leq(pv1388, n3))],extension(799 ^ 2)).
% 158.26/153.41 ncf('1.5',plain,[-(init = init)],lemmata('x')).
% 158.26/153.41 ncf('1.6',plain,[-(s_sworst7_init = init)],extension(781 ^ 3)).
% 158.26/153.41 ncf('1.7',plain,[-(s_worst7_init = init)],extension(783 ^ 3)).
% 158.26/153.41 ncf('1.8',plain,[-(leq(n0, s_sworst7))],extension(787 ^ 3)).
% 158.26/153.41 ncf('1.9',plain,[-(leq(n0, s_worst7))],extension(789 ^ 3)).
% 158.26/153.41 ncf('1.10',plain,[-(leq(n0, pv1388)), leq(n0, n1), leq(n1, pv1388)],extension(26 ^ 3,bind([[_365701, _365703, _365705], [pv1388, n1, n0]]))).
% 158.26/153.41 ncf('1.10.1',plain,[-(leq(n0, n1)), leq(n0, n1), leq(n1, n1)],extension(26 ^ 4,bind([[_365701, _365703, _365705], [n1, n1, n0]]))).
% 158.26/153.41 ncf('1.10.1.1',plain,[-(leq(n0, n1)), gt(n1, n0)],extension(60 ^ 5,bind([[_366816, _366818], [n1, n0]]))).
% 158.26/153.41 ncf('1.10.1.1.1',plain,[-(gt(n1, n0))],extension(625 ^ 6)).
% 158.26/153.41 ncf('1.10.1.2',plain,[-(leq(n1, n1))],extension(24 ^ 5,bind([[_365580], [n1]]))).
% 158.26/153.41 ncf('1.10.2',plain,[-(leq(n1, pv1388)), leq(n1, n2), leq(n2, pv1388)],extension(26 ^ 4,bind([[_365701, _365703, _365705], [pv1388, n2, n1]]))).
% 158.26/153.41 ncf('1.10.2.1',plain,[-(leq(n1, n2)), gt(n2, n1)],extension(60 ^ 5,bind([[_366816, _366818], [n2, n1]]))).
% 158.26/153.41 ncf('1.10.2.1.1',plain,[-(gt(n2, n1))],extension(635 ^ 6)).
% 158.26/153.41 ncf('1.10.2.2',plain,[-(leq(n2, pv1388))],extension(791 ^ 5)).
% 158.26/153.41 ncf('1.11',plain,[-(leq(s_sworst7, n3))],extension(795 ^ 3)).
% 158.26/153.41 ncf('1.12',plain,[-(leq(s_worst7, n3))],extension(797 ^ 3)).
% 158.26/153.41 ncf('1.13',plain,[-(leq(pv1388, n3))],extension(799 ^ 3)).
% 158.26/153.41 ncf('1.14',plain,[-(a_select3(simplex7_init, 1197 ^ [], 1192 ^ []) = init), 809 : leq(n0, 1197 ^ []), 809 : leq(1197 ^ [], n3), 809 : leq(n0, 1192 ^ []), 809 : leq(1192 ^ [], n2)],extension(801 ^ 5,bind([[_395883, _396111], [1192 ^ [], 1197 ^ []]]))).
% 158.26/153.41 ncf('1.14.1',plain,[-(leq(n0, 1197 ^ []))],extension(1199 ^ 8)).
% 158.26/153.41 ncf('1.14.2',plain,[-(leq(1197 ^ [], n3))],extension(1201 ^ 8)).
% 158.26/153.41 ncf('1.14.3',plain,[-(leq(n0, 1192 ^ []))],extension(1194 ^ 6)).
% 158.26/153.41 ncf('1.14.4',plain,[-(leq(1192 ^ [], n2))],extension(1196 ^ 6)).
% 158.26/153.41 ncf('1.15',plain,[-(a_select2(s_values7_init, 1206 ^ []) = init), leq(n0, 1206 ^ []), leq(1206 ^ [], n3)],extension(819 ^ 5,bind([[_396413], [1206 ^ []]]))).
% 158.26/153.41 ncf('1.15.1',plain,[-(leq(n0, 1206 ^ []))],extension(1208 ^ 6)).
% 158.26/153.41 ncf('1.15.2',plain,[-(leq(1206 ^ [], n3))],extension(1210 ^ 6)).
% 158.26/153.41 ncf('1.16',plain,[-(a_select2(s_center7_init, 1215 ^ []) = init), leq(n0, 1215 ^ []), leq(1215 ^ [], n2)],extension(829 ^ 5,bind([[_396694], [1215 ^ []]]))).
% 158.26/153.41 ncf('1.16.1',plain,[-(leq(n0, 1215 ^ []))],extension(1217 ^ 6)).
% 158.26/153.41 ncf('1.16.2',plain,[-(leq(1215 ^ [], n2))],extension(1219 ^ 6)).
% 158.26/153.41 ncf('1.17',plain,[-(pvar1400_init = init), gt(loopcounter, n1)],extension(839 ^ 5)).
% 158.26/153.41 ncf('1.17.1',plain,[-(gt(loopcounter, n1))],extension(1223 ^ 6)).
% 158.26/153.41 ncf('1.18',plain,[-(pvar1401_init = init), gt(loopcounter, n1)],extension(839 ^ 5)).
% 158.26/153.41 ncf('1.18.1',plain,[-(gt(loopcounter, n1))],extension(1223 ^ 6)).
% 158.26/153.41 ncf('1.19',plain,[-(pvar1402_init = init), gt(loopcounter, n1)],extension(839 ^ 5)).
% 158.26/153.41 ncf('1.19.1',plain,[-(gt(loopcounter, n1))],extension(1223 ^ 6)).
% 158.26/153.41 ncf('1.20',plain,[-(init = init)],lemmata('x')).
% 158.26/153.41 ncf('1.21',plain,[-(s_worst7_init = init)],extension(783 ^ 3)).
% 158.26/153.41 ncf('1.22',plain,[-(a_select2(s_values7_init, s_worst7) = init), leq(n0, s_worst7), leq(s_worst7, n3)],extension(819 ^ 3,bind([[_396413], [s_worst7]]))).
% 158.26/153.41 ncf('1.22.1',plain,[-(leq(n0, s_worst7))],extension(789 ^ 4)).
% 158.26/153.41 ncf('1.22.2',plain,[-(leq(s_worst7, n3))],extension(797 ^ 4)).
% 158.26/153.41 ncf('1.23',plain,[-(a_select2(s_values7_init, pv1388) = init)],lemmata('x')).
% 158.26/153.41 ncf('1.24',plain,[-(init = init)],lemmata('x')).
% 158.26/153.41 ncf('1.25',plain,[-(s_best7_init = init)],lemmata('x')).
% 158.26/153.41 ncf('1.26',plain,[-(s_worst7_init = init)],lemmata('x')).
% 158.26/153.41 ncf('1.27',plain,[-(leq(n0, s_best7))],extension(785 ^ 5)).
% 158.26/153.41 ncf('1.28',plain,[-(leq(n0, s_worst7))],extension(789 ^ 5)).
% 158.26/153.41 ncf('1.29',plain,[-(leq(n0, pv1388)), leq(n0, n1), leq(n1, pv1388)],extension(26 ^ 5,bind([[_365701, _365703, _365705], [pv1388, n1, n0]]))).
% 158.26/153.41 ncf('1.29.1',plain,[-(leq(n0, n1)), leq(n0, n1), leq(n1, n1)],extension(26 ^ 6,bind([[_365701, _365703, _365705], [n1, n1, n0]]))).
% 158.26/153.41 ncf('1.29.1.1',plain,[-(leq(n0, n1)), gt(n1, n0)],extension(60 ^ 7,bind([[_366816, _366818], [n1, n0]]))).
% 158.26/153.41 ncf('1.29.1.1.1',plain,[-(gt(n1, n0))],extension(625 ^ 8)).
% 158.26/153.41 ncf('1.29.1.2',plain,[-(leq(n1, n1))],extension(24 ^ 7,bind([[_365580], [n1]]))).
% 158.26/153.41 ncf('1.29.2',plain,[-(leq(n1, pv1388)), leq(n1, n2), leq(n2, pv1388)],extension(26 ^ 6,bind([[_365701, _365703, _365705], [pv1388, n2, n1]]))).
% 158.26/153.41 ncf('1.29.2.1',plain,[-(leq(n1, n2)), gt(n2, n1)],extension(60 ^ 7,bind([[_366816, _366818], [n2, n1]]))).
% 158.26/153.41 ncf('1.29.2.1.1',plain,[-(gt(n2, n1))],extension(635 ^ 8)).
% 158.26/153.41 ncf('1.29.2.2',plain,[-(leq(n2, pv1388))],extension(791 ^ 7)).
% 158.26/153.41 ncf('1.30',plain,[-(leq(s_best7, n3))],extension(793 ^ 5)).
% 158.26/153.41 ncf('1.31',plain,[-(leq(s_worst7, n3))],extension(797 ^ 5)).
% 158.26/153.41 ncf('1.32',plain,[-(leq(pv1388, n3))],extension(799 ^ 5)).
% 158.26/153.41 ncf('1.33',plain,[-(a_select3(simplex7_init, 1115 ^ [], 1110 ^ []) = init), 809 : leq(n0, 1115 ^ []), 809 : leq(1115 ^ [], n3), 809 : leq(n0, 1110 ^ []), 809 : leq(1110 ^ [], n2)],extension(801 ^ 7,bind([[_395883, _396111], [1110 ^ [], 1115 ^ []]]))).
% 158.26/153.41 ncf('1.33.1',plain,[-(leq(n0, 1115 ^ []))],extension(1117 ^ 10)).
% 158.26/153.41 ncf('1.33.2',plain,[-(leq(1115 ^ [], n3))],extension(1119 ^ 10)).
% 158.26/153.41 ncf('1.33.3',plain,[-(leq(n0, 1110 ^ []))],extension(1112 ^ 8)).
% 158.26/153.41 ncf('1.33.4',plain,[-(leq(1110 ^ [], n2))],extension(1114 ^ 8)).
% 158.26/153.41 ncf('1.34',plain,[-(a_select2(s_values7_init, 1124 ^ []) = init), leq(n0, 1124 ^ []), leq(1124 ^ [], n3)],extension(819 ^ 7,bind([[_396413], [1124 ^ []]]))).
% 158.26/153.41 ncf('1.34.1',plain,[-(leq(n0, 1124 ^ []))],extension(1126 ^ 8)).
% 158.26/153.41 ncf('1.34.2',plain,[-(leq(1124 ^ [], n3))],extension(1128 ^ 8)).
% 158.26/153.41 ncf('1.35',plain,[-(a_select2(s_center7_init, 1133 ^ []) = init), leq(n0, 1133 ^ []), leq(1133 ^ [], n2)],extension(829 ^ 7,bind([[_396694], [1133 ^ []]]))).
% 158.26/153.41 ncf('1.35.1',plain,[-(leq(n0, 1133 ^ []))],extension(1135 ^ 8)).
% 158.26/153.41 ncf('1.35.2',plain,[-(leq(1133 ^ [], n2))],extension(1137 ^ 8)).
% 158.26/153.41 ncf('1.36',plain,[-(pvar1400_init = init), gt(loopcounter, n1)],extension(839 ^ 7)).
% 158.26/153.41 ncf('1.36.1',plain,[-(gt(loopcounter, n1))],extension(1141 ^ 8)).
% 158.26/153.41 ncf('1.37',plain,[-(pvar1401_init = init), gt(loopcounter, n1)],extension(839 ^ 7)).
% 158.26/153.41 ncf('1.37.1',plain,[-(gt(loopcounter, n1))],extension(1141 ^ 8)).
% 158.26/153.41 ncf('1.38',plain,[-(pvar1402_init = init), gt(loopcounter, n1)],extension(839 ^ 7)).
% 158.26/153.41 ncf('1.38.1',plain,[-(gt(loopcounter, n1))],extension(1141 ^ 8)).
% 158.26/153.41 ncf('1.39',plain,[-(init = init)],lemmata('x')).
% 158.26/153.41 ncf('1.40',plain,[-(s_sworst7_init = init)],extension(781 ^ 5)).
% 158.26/153.41 ncf('1.41',plain,[-(a_select2(s_values7_init, s_sworst7) = init), leq(n0, s_sworst7), leq(s_sworst7, n3)],extension(819 ^ 5,bind([[_396413], [s_sworst7]]))).
% 158.26/153.41 ncf('1.41.1',plain,[-(leq(n0, s_sworst7))],extension(787 ^ 6)).
% 158.26/153.41 ncf('1.41.2',plain,[-(leq(s_sworst7, n3))],extension(795 ^ 6)).
% 158.26/153.41 ncf('1.42',plain,[-(a_select2(s_values7_init, pv1388) = init)],lemmata('x')).
% 158.26/153.41 ncf('1.43',plain,[-(s_best7_init = init)],lemmata('x')).
% 158.26/153.41 ncf('1.44',plain,[-(s_sworst7_init = init)],lemmata('x')).
% 158.26/153.41 ncf('1.45',plain,[-(s_worst7_init = init)],lemmata('x')).
% 158.26/153.41 ncf('1.46',plain,[-(leq(n0, s_best7))],extension(785 ^ 7)).
% 158.26/153.41 ncf('1.47',plain,[-(leq(n0, s_sworst7))],extension(787 ^ 7)).
% 158.26/153.41 ncf('1.48',plain,[-(leq(n0, s_worst7))],extension(789 ^ 7)).
% 158.26/153.41 ncf('1.49',plain,[-(leq(s_best7, n3))],extension(793 ^ 7)).
% 158.26/153.41 ncf('1.50',plain,[-(leq(s_sworst7, n3))],extension(795 ^ 7)).
% 158.26/153.41 ncf('1.51',plain,[-(leq(s_worst7, n3))],extension(797 ^ 7)).
% 158.26/153.41 ncf('1.52',plain,[-(a_select3(simplex7_init, 951 ^ [], 946 ^ []) = init), 809 : leq(n0, 951 ^ []), 809 : leq(951 ^ [], n3), 809 : leq(n0, 946 ^ []), 809 : leq(946 ^ [], n2)],extension(801 ^ 9,bind([[_395883, _396111], [946 ^ [], 951 ^ []]]))).
% 158.26/153.41 ncf('1.52.1',plain,[-(leq(n0, 951 ^ []))],extension(953 ^ 12)).
% 158.26/153.41 ncf('1.52.2',plain,[-(leq(951 ^ [], n3))],extension(955 ^ 12)).
% 158.26/153.41 ncf('1.52.3',plain,[-(leq(n0, 946 ^ []))],extension(948 ^ 10)).
% 158.26/153.41 ncf('1.52.4',plain,[-(leq(946 ^ [], n2))],extension(950 ^ 10)).
% 158.26/153.41 ncf('1.53',plain,[-(a_select2(s_values7_init, 960 ^ []) = init), leq(n0, 960 ^ []), leq(960 ^ [], n3)],extension(819 ^ 9,bind([[_396413], [960 ^ []]]))).
% 158.26/153.41 ncf('1.53.1',plain,[-(leq(n0, 960 ^ []))],extension(962 ^ 10)).
% 158.26/153.41 ncf('1.53.2',plain,[-(leq(960 ^ [], n3))],extension(964 ^ 10)).
% 158.26/153.41 ncf('1.54',plain,[-(a_select2(s_center7_init, 969 ^ []) = init), leq(n0, 969 ^ []), leq(969 ^ [], n2)],extension(829 ^ 9,bind([[_396694], [969 ^ []]]))).
% 158.26/153.41 ncf('1.54.1',plain,[-(leq(n0, 969 ^ []))],extension(971 ^ 10)).
% 158.26/153.41 ncf('1.54.2',plain,[-(leq(969 ^ [], n2))],extension(973 ^ 10)).
% 158.26/153.41 ncf('1.55',plain,[-(pvar1400_init = init), gt(loopcounter, n1)],extension(839 ^ 9)).
% 158.26/153.41 ncf('1.55.1',plain,[-(gt(loopcounter, n1))],extension(977 ^ 10)).
% 158.26/153.41 ncf('1.56',plain,[-(pvar1401_init = init), gt(loopcounter, n1)],extension(839 ^ 9)).
% 158.26/153.41 ncf('1.56.1',plain,[-(gt(loopcounter, n1))],extension(977 ^ 10)).
% 158.26/153.41 ncf('1.57',plain,[-(pvar1402_init = init), gt(loopcounter, n1)],extension(839 ^ 9)).
% 158.26/153.41 ncf('1.57.1',plain,[-(gt(loopcounter, n1))],extension(977 ^ 10)).
% 158.26/153.41 ncf('1.58',plain,[-(init = init)],lemmata('x')).
% 158.26/153.41 ncf('1.59',plain,[-(s_best7_init = init)],lemmata('x')).
% 158.26/153.41 ncf('1.60',plain,[-(s_worst7_init = init)],lemmata('x')).
% 158.26/153.41 ncf('1.61',plain,[-(leq(n0, s_best7))],extension(785 ^ 7)).
% 158.26/153.41 ncf('1.62',plain,[-(leq(n0, s_worst7))],extension(789 ^ 7)).
% 158.26/153.41 ncf('1.63',plain,[-(leq(n0, pv1388)), leq(n0, n1), leq(n1, pv1388)],extension(26 ^ 7,bind([[_365701, _365703, _365705], [pv1388, n1, n0]]))).
% 158.26/153.41 ncf('1.63.1',plain,[-(leq(n0, n1)), leq(n0, n1), leq(n1, n1)],extension(26 ^ 8,bind([[_365701, _365703, _365705], [n1, n1, n0]]))).
% 158.26/153.41 ncf('1.63.1.1',plain,[-(leq(n0, n1)), gt(n1, n0)],extension(60 ^ 9,bind([[_366816, _366818], [n1, n0]]))).
% 158.26/153.41 ncf('1.63.1.1.1',plain,[-(gt(n1, n0))],extension(625 ^ 10)).
% 158.26/153.41 ncf('1.63.1.2',plain,[-(leq(n1, n1))],extension(24 ^ 9,bind([[_365580], [n1]]))).
% 158.26/153.41 ncf('1.63.2',plain,[-(leq(n1, pv1388)), leq(n1, n2), leq(n2, pv1388)],extension(26 ^ 8,bind([[_365701, _365703, _365705], [pv1388, n2, n1]]))).
% 158.26/153.41 ncf('1.63.2.1',plain,[-(leq(n1, n2)), gt(n2, n1)],extension(60 ^ 9,bind([[_366816, _366818], [n2, n1]]))).
% 158.26/153.41 ncf('1.63.2.1.1',plain,[-(gt(n2, n1))],extension(635 ^ 10)).
% 158.26/153.41 ncf('1.63.2.2',plain,[-(leq(n2, pv1388))],extension(791 ^ 9)).
% 158.26/153.41 ncf('1.64',plain,[-(leq(s_best7, n3))],extension(793 ^ 7)).
% 158.26/153.41 ncf('1.65',plain,[-(leq(s_worst7, n3))],extension(797 ^ 7)).
% 158.26/153.41 ncf('1.66',plain,[-(leq(pv1388, n3))],extension(799 ^ 7)).
% 158.26/153.41 ncf('1.67',plain,[-(a_select3(simplex7_init, 1033 ^ [], 1028 ^ []) = init), 809 : leq(n0, 1033 ^ []), 809 : leq(1033 ^ [], n3), 809 : leq(n0, 1028 ^ []), 809 : leq(1028 ^ [], n2)],extension(801 ^ 9,bind([[_395883, _396111], [1028 ^ [], 1033 ^ []]]))).
% 158.26/153.41 ncf('1.67.1',plain,[-(leq(n0, 1033 ^ []))],extension(1035 ^ 12)).
% 158.26/153.41 ncf('1.67.2',plain,[-(leq(1033 ^ [], n3))],extension(1037 ^ 12)).
% 158.26/153.41 ncf('1.67.3',plain,[-(leq(n0, 1028 ^ []))],extension(1030 ^ 10)).
% 158.26/153.41 ncf('1.67.4',plain,[-(leq(1028 ^ [], n2))],extension(1032 ^ 10)).
% 158.26/153.41 ncf('1.68',plain,[-(a_select2(s_values7_init, 1042 ^ []) = init), leq(n0, 1042 ^ []), leq(1042 ^ [], n3)],extension(819 ^ 9,bind([[_396413], [1042 ^ []]]))).
% 158.26/153.41 ncf('1.68.1',plain,[-(leq(n0, 1042 ^ []))],extension(1044 ^ 10)).
% 158.26/153.41 ncf('1.68.2',plain,[-(leq(1042 ^ [], n3))],extension(1046 ^ 10)).
% 158.26/153.41 ncf('1.69',plain,[-(a_select2(s_center7_init, 1051 ^ []) = init), leq(n0, 1051 ^ []), leq(1051 ^ [], n2)],extension(829 ^ 9,bind([[_396694], [1051 ^ []]]))).
% 158.26/153.41 ncf('1.69.1',plain,[-(leq(n0, 1051 ^ []))],extension(1053 ^ 10)).
% 158.26/153.41 ncf('1.69.2',plain,[-(leq(1051 ^ [], n2))],extension(1055 ^ 10)).
% 158.26/153.41 ncf('1.70',plain,[-(pvar1400_init = init), gt(loopcounter, n1)],extension(839 ^ 9)).
% 158.26/153.41 ncf('1.70.1',plain,[-(gt(loopcounter, n1))],extension(1059 ^ 10)).
% 158.26/153.41 ncf('1.71',plain,[-(pvar1401_init = init), gt(loopcounter, n1)],extension(839 ^ 9)).
% 158.26/153.41 ncf('1.71.1',plain,[-(gt(loopcounter, n1))],extension(1059 ^ 10)).
% 158.26/153.41 ncf('1.72',plain,[-(pvar1402_init = init), gt(loopcounter, n1)],extension(839 ^ 9)).
% 158.26/153.41 ncf('1.72.1',plain,[-(gt(loopcounter, n1))],extension(1059 ^ 10)).
% 158.26/153.41 %-----------------------------------------------------
% 158.26/153.41 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------