%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV467+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n023.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:20:45 EDT 2023
% Result : Theorem 52.56s 51.01s
% Output : Proof 52.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SWV467+1 : TPTP v8.1.2. Released v4.0.0.
% 0.04/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n023.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Fri May 19 02:47:13 EDT 2023
% 0.13/0.34 % CPUTime :
% 52.56/51.01
% 52.56/51.01 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 52.56/51.01 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 52.56/51.01 %-----------------------------------------------------
% 52.56/51.01 ncf(matrix, plain, [(635 ^ _225503) ^ [_226078, _226080] : [elem(m_Halt(_226078), queue(host(_226080))), leq(host(_226080), host(_226078))], (681 ^ _225503) ^ [_227603] : [-(index(elid, host(_227603)) = _227603), 684 ^ _225503 : [(687 ^ _225503) ^ [] : [index(status, host(_227603)) = elec_2], (685 ^ _225503) ^ [] : [index(status, host(_227603)) = elec_1]], setIn(_227603, alive)], (759 ^ _225503) ^ [_229901, _229903] : [leq(index(pendack, host(_229903)), index(pendack, host(_229901))), -(leq(host(_229903), host(_229901))), setIn(_229903, alive), setIn(_229901, alive), index(status, host(_229903)) = elec_2, index(status, host(_229901)) = elec_2], (925 ^ _225503) ^ [] : [-(setIn(921 ^ [], alive))], (641 ^ _225503) ^ [_226323, _226325, _226327] : [elem(m_Ack(_226323, _226327), queue(host(_226325))), leq(host(_226327), host(_226323))], (715 ^ _225503) ^ [_228645, _228647] : [-(leq(index(pendack, host(_228645)), host(_228647))), -(leq(host(_228647), host(_228645))), setIn(_228647, alive), setIn(_228645, alive), index(status, host(_228647)) = elec_2, index(status, host(_228645)) = elec_2], (882 ^ _225503) ^ [] : [leq(host(620 ^ []), host(621 ^ []))], (647 ^ _225503) ^ [_226562, _226564] : [-(_226562 = _226564), host(_226562) = host(_226564), setIn(_226564, alive), setIn(_226562, alive)], (880 ^ _225503) ^ [] : [-(setIn(620 ^ [], alive))], (935 ^ _225503) ^ [] : [-(host(919 ^ []) = index(pendack, host(921 ^ [])))], (931 ^ _225503) ^ [] : [-(leq(nbr_proc, s(index(pendack, host(921 ^ [])))))], (939 ^ _225503) ^ [] : [-(setIn(916 ^ [], alive))], (918 ^ _225503) ^ [] : [-(host(620 ^ []) = host(916 ^ []))], (937 ^ _225503) ^ [] : [-(host(920 ^ []) = s(index(pendack, host(921 ^ []))))], (623 ^ _225503) ^ [_225616, _225618] : [elem(m_Ldr(_225616), queue(host(_225618))), leq(host(_225618), host(_225616))], (737 ^ _225503) ^ [_229270, _229272, _229274] : [elem(m_Ack(_229274, _229272), queue(host(_229274))), setIn(_229274, alive), setIn(_229270, alive), host(_229270) = host(_229272), index(status, host(_229274)) = elec_2, index(status, host(_229270)) = elec_2], (807 ^ _225503) ^ [_231310, _231312, _231314, _231316] : [setIn(_231316, alive), elem(m_Down(_231314), queue(host(_231316))), 811 ^ _225503 : [(814 ^ _225503) ^ [] : [-(leq(s(zero), 810 ^ [_231310, _231312, _231314, _231316]))], (816 ^ _225503) ^ [] : [setIn(810 ^ [_231310, _231312, _231314, _231316], index(down, host(_231310)))], (818 ^ _225503) ^ [] : [810 ^ [_231310, _231312, _231314, _231316] = host(_231312)], (812 ^ _225503) ^ [] : [leq(host(_231310), 810 ^ [_231310, _231312, _231314, _231316])]], elem(m_Down(_231312), queue(host(_231310))), host(_231310) = nbr_proc, host(_231310) = host(_231314), index(status, host(_231310)) = elec_1], (923 ^ _225503) ^ [] : [host(620 ^ []) = host(921 ^ [])], (840 ^ _225503) ^ [_232480, _232482, _232484, _232486] : [setIn(_232486, alive), index(ldr, host(_232486)) = host(_232486), index(status, host(_232486)) = norm, setIn(_232480, alive), elem(m_Down(_232482), queue(host(_232480))), elem(m_Ack(_232480, _232484), queue(host(_232480))), leq(nbr_proc, s(index(pendack, host(_232480)))), index(status, host(_232480)) = elec_2, host(_232484) = index(pendack, host(_232480)), host(_232482) = s(index(pendack, host(_232480)))], (890 ^ _225503) ^ [] : [index(status, host(620 ^ [])) = wait, host(621 ^ []) = host(index(elid, host(620 ^ [])))], (910 ^ _225503) ^ [] : [-(index(status, host(620 ^ [])) = elec_1)], (661 ^ _225503) ^ [_226966, _226968] : [-(leq(host(_226968), index(pendack, host(_226966)))), setIn(_226966, alive), elem(m_Ack(_226966, _226968), queue(host(_226966)))], (927 ^ _225503) ^ [] : [-(elem(m_Down(920 ^ []), queue(host(921 ^ []))))], (941 ^ _225503) ^ [] : [-(host(620 ^ []) = host(916 ^ []))], (781 ^ _225503) ^ [_230533, _230535, _230537] : [setIn(_230537, alive), index(ldr, host(_230537)) = host(_230537), index(status, host(_230537)) = norm, -(leq(index(pendack, host(_230533)), host(_230537))), setIn(_230533, alive), elem(m_Halt(_230533), queue(host(_230535))), index(status, host(_230533)) = elec_2], (929 ^ _225503) ^ [] : [-(elem(m_Ack(921 ^ [], 919 ^ []), queue(host(921 ^ []))))], (878 ^ _225503) ^ [] : [-(queue(host(620 ^ [])) = cons(m_Down(621 ^ []), 618 ^ []))], (896 ^ _225503) ^ [_234001] : [-(leq(host(620 ^ []), _234001)), leq(s(zero), _234001), -(setIn(_234001, index(down, host(620 ^ [])))), -(_234001 = host(621 ^ []))], (915 ^ _225503) ^ [] : [setIn(host(913 ^ []), setEmpty)], (912 ^ _225503) ^ [] : [-(leq(nbr_proc, host(620 ^ [])))], (629 ^ _225503) ^ [_225847, _225849] : [elem(m_Down(_225847), queue(host(_225849))), host(_225847) = host(_225849)], (884 ^ _225503) ^ [] : [index(ldr, host(620 ^ [])) = host(621 ^ []), index(status, host(620 ^ [])) = norm], (933 ^ _225503) ^ [] : [-(index(status, host(921 ^ [])) = elec_2)], (693 ^ _225503) ^ [_228008, _228010, _228012] : [setIn(_228008, alive), elem(m_Down(_228010), queue(host(_228008))), host(_228010) = host(_228012), setIn(_228012, alive), index(ldr, host(_228012)) = host(_228012), index(status, host(_228012)) = norm], (671 ^ _225503) ^ [_227293, _227295] : [elem(m_Ack(_227293, _227295), queue(host(_227293))), setIn(_227293, alive), index(status, host(_227293)) = elec_1], !, (124 ^ _197879) ^ [_202097, _202099, _202101, _202103] : [-(snoc(_202103, _202099) = snoc(_202101, _202097)), _202103 = _202101, _202099 = _202097], (322 ^ _197879) ^ [_209631, _209633, _209635, _209637] : [-(_209637 = _209635), m_Ack(_209637, _209633) = m_Ack(_209635, _209631)], (178 ^ _197879) ^ [_204018, _204020] : [_204020 = _204018, -(s(_204020) = s(_204018))], (112 ^ _197879) ^ [_201633, _201635] : [_201635 = _201633, -(last(_201635) = last(_201633))], (328 ^ _197879) ^ [_209897, _209899, _209901, _209903] : [-(_209899 = _209897), m_Ack(_209903, _209899) = m_Ack(_209901, _209897)], (342 ^ _197879) ^ [_210394, _210396] : [-(head(cons(_210396, _210394)) = _210396)], (390 ^ _197879) ^ [_212344, _212346, _212348] : [elem(_212348, snoc(_212344, _212346)), -(_212348 = _212346), -(elem(_212348, _212344))], (559 ^ _197879) ^ [_218168, _218170] : [-(_218170 = _218168), leq(_218170, _218168), leq(_218168, _218170)], (364 ^ _197879) ^ [_211295, _211297] : [q_nil = snoc(_211295, _211297)], (480 ^ _197879) ^ [_215426, _215428] : [ordered(snoc(_215426, _215428)), 483 ^ _197879 : [(486 ^ _197879) ^ [_215665] : [-(leq(pidMsg(_215665), pidMsg(_215428))), elem(_215665, _215426), pidElem(_215428), pidElem(_215665), host(pidMsg(_215665)) = host(pidMsg(_215428))], (484 ^ _197879) ^ [] : [-(ordered(_215426))]]], (286 ^ _197879) ^ [_208351, _208353] : [-(_208353 = _208351), m_NotNorm(_208353) = m_NotNorm(_208351)], (370 ^ _197879) ^ [_211583] : [elem(_211583, q_nil)], (248 ^ _197879) ^ [_206773, _206775] : [m_Down(_206775) = m_NotNorm(_206773)], (68 ^ _197879) ^ [_200113, _200115, _200117, _200119] : [-(setIn(_200117, _200113)), setIn(_200119, _200115), _200119 = _200117, _200115 = _200113], (268 ^ _197879) ^ [_207671, _207673] : [-(m_Halt(_207673) = m_Halt(_207671)), _207673 = _207671], (252 ^ _197879) ^ [_206967, _206969] : [m_NormQ(_206969) = m_Halt(_206967)], (246 ^ _197879) ^ [_206676, _206678] : [m_Down(_206678) = m_Ldr(_206676)], (222 ^ _197879) ^ [] : [elec_1 = wait], (334 ^ _197879) ^ [_210135, _210137] : [-(host(_210137) = host(_210135)), _210137 = _210135], (292 ^ _197879) ^ [_208525, _208527] : [-(m_NotNorm(_208527) = m_NotNorm(_208525)), _208527 = _208525], (146 ^ _197879) ^ [_202892, _202894, _202896, _202898] : [-(cons(_202898, _202894) = cons(_202896, _202892)), _202898 = _202896, _202894 = _202892], (316 ^ _197879) ^ [_209379, _209381] : [-(m_Down(_209381) = m_Down(_209379)), _209381 = _209379], (214 ^ _197879) ^ [_205374] : [-(leq(s(zero), host(_205374)))], (433 ^ _197879) ^ [_213756] : [-(ordered(cons(_213756, q_nil)))], (437 ^ _197879) ^ [_213942, _213944] : [ordered(cons(_213944, _213942)), 440 ^ _197879 : [(443 ^ _197879) ^ [_214181] : [-(leq(pidMsg(_213944), pidMsg(_214181))), elem(_214181, _213942), pidElem(_213944), pidElem(_214181), host(pidMsg(_214181)) = host(pidMsg(_213944))], (441 ^ _197879) ^ [] : [-(ordered(_213942))]]], (4 ^ _197879) ^ [_198110, _198112] : [_198112 = _198110, -(_198110 = _198112)], (461 ^ _197879) ^ [_214659, _214661] : [-(ordered(cons(_214661, _214659))), ordered(_214659), 467 ^ _197879 : [(468 ^ _197879) ^ [] : [-(elem(466 ^ [_214659, _214661], _214659))], (472 ^ _197879) ^ [] : [-(pidElem(466 ^ [_214659, _214661]))], (476 ^ _197879) ^ [] : [leq(pidMsg(_214661), pidMsg(466 ^ [_214659, _214661]))], (474 ^ _197879) ^ [] : [-(host(pidMsg(466 ^ [_214659, _214661])) = host(pidMsg(_214661)))], (470 ^ _197879) ^ [] : [-(pidElem(_214661))]]], (208 ^ _197879) ^ [_205172, _205174] : [s(host(_205174)) = host(_205172), host(_205174) = host(_205172)], (82 ^ _197879) ^ [_200543, _200545] : [_200545 = _200543, -(m_NormQ(_200545) = m_NormQ(_200543))], (280 ^ _197879) ^ [_208098, _208100] : [-(m_NormQ(_208100) = m_NormQ(_208098)), _208100 = _208098], (242 ^ _197879) ^ [_206482, _206484] : [m_NotNorm(_206484) = m_Halt(_206482)], (2 ^ _197879) ^ [_198003] : [-(_198003 = _198003)], (250 ^ _197879) ^ [_206870, _206872] : [m_Down(_206872) = m_NormQ(_206870)], (238 ^ _197879) ^ [_206268, _206270, _206272] : [m_Ack(_206272, _206270) = m_Ldr(_206268)], (140 ^ _197879) ^ [_202646, _202648] : [_202648 = _202646, -(m_Halt(_202648) = m_Halt(_202646))], (382 ^ _197879) ^ [_212001, _212003, _212005] : [383 ^ _197879 : [(386 ^ _197879) ^ [] : [elem(_212005, _212001)], (384 ^ _197879) ^ [] : [_212005 = _212003]], -(elem(_212005, cons(_212003, _212001)))], (54 ^ _197879) ^ [_199689, _199691, _199693, _199695] : [-(leq(_199693, _199689)), leq(_199695, _199691), _199695 = _199693, _199691 = _199689], (200 ^ _197879) ^ [_204873, _204875] : [elem(m_Ack(_204875, _204873), queue(host(_204875))), 203 ^ _197879 : [(206 ^ _197879) ^ [] : [-(setIn(_204873, pids))], (204 ^ _197879) ^ [] : [-(setIn(_204875, pids))]]], (232 ^ _197879) ^ [_205926, _205928, _205930] : [m_Ack(_205930, _205928) = m_Halt(_205926)], (535 ^ _197879) ^ [_217349, _217351, _217353] : [-(leq(_217351, _217349)), ordered(cons(m_Halt(_217351), _217353)), host(_217351) = host(_217349), elem(m_Down(_217349), _217353)], (100 ^ _197879) ^ [_201197, _201199] : [_201199 = _201197, -(tail(_201199) = tail(_201197))], (194 ^ _197879) ^ [_204575, _204577] : [_204577 = _204575, -(host(_204577) = host(_204575))], (340 ^ _197879) ^ [] : [setIn(nil, alive)], (408 ^ _197879) ^ [_212927] : [pidElem(_212927), -(_212927 = m_Halt(411 ^ [_212927])), -(_212927 = m_Down(411 ^ [_212927]))], (348 ^ _197879) ^ [_210691, _210693] : [-(init(snoc(_210691, _210693)) = _210691)], (344 ^ _197879) ^ [_210493, _210495] : [-(tail(cons(_210495, _210493)) = _210493)], (20 ^ _197879) ^ [_198627, _198629] : [-(pidElem(_198627)), _198629 = _198627, pidElem(_198629)], (220 ^ _197879) ^ [] : [elec_1 = elec_2], (310 ^ _197879) ^ [_209205, _209207] : [-(_209207 = _209205), m_Down(_209207) = m_Down(_209205)], (346 ^ _197879) ^ [_210592, _210594] : [-(last(snoc(_210592, _210594)) = _210594)], (304 ^ _197879) ^ [_208952, _208954] : [-(m_Ldr(_208954) = m_Ldr(_208952)), _208954 = _208952], (156 ^ _197879) ^ [_203223, _203225] : [_203225 = _203223, -(m_Down(_203225) = m_Down(_203223))], (172 ^ _197879) ^ [_203800, _203802] : [_203802 = _203800, -(queue(_203802) = queue(_203800))], (236 ^ _197879) ^ [_206154, _206156, _206158] : [m_Ack(_206158, _206156) = m_NotNorm(_206154)], (350 ^ _197879) ^ [_210791] : [-(_210791 = q_nil), -(_210791 = cons(head(_210791), tail(_210791)))], (356 ^ _197879) ^ [_210996] : [-(_210996 = q_nil), -(_210996 = snoc(init(_210996), last(_210996)))], (94 ^ _197879) ^ [_200979, _200981] : [_200981 = _200979, -(head(_200981) = head(_200979))], (419 ^ _197879) ^ [_213241] : [420 ^ _197879 : [(423 ^ _197879) ^ [_213385] : [_213241 = m_Down(_213385)], (421 ^ _197879) ^ [_213338] : [_213241 = m_Halt(_213338)]], -(pidElem(_213241))], (184 ^ _197879) ^ [_204264, _204266, _204268, _204270] : [-(index(_204270, _204266) = index(_204268, _204264)), _204270 = _204268, _204266 = _204264], (244 ^ _197879) ^ [_206579, _206581] : [m_Down(_206581) = m_Halt(_206579)], (218 ^ _197879) ^ [_205507] : [-(leq(host(_205507), nbr_proc))], (10 ^ _197879) ^ [_198314, _198316, _198318] : [-(_198318 = _198314), _198318 = _198316, _198316 = _198314], (617 ^ _197879) ^ [_219981] : [setIn(_219981, setEmpty)], (429 ^ _197879) ^ [_213601] : [-(pidMsg(m_Down(_213601)) = _213601)], (577 ^ _197879) ^ [_218720, _218722, _218724] : [-(leq(_218724, _218720)), leq(_218724, _218722), leq(_218722, _218720)], (216 ^ _197879) ^ [] : [-(leq(s(zero), nbr_proc))], (260 ^ _197879) ^ [_207355, _207357] : [m_NormQ(_207357) = m_NotNorm(_207355)], (30 ^ _197879) ^ [_198922, _198924] : [-(ordered(_198922)), _198924 = _198922, ordered(_198924)], (40 ^ _197879) ^ [_199245, _199247, _199249, _199251] : [-(elem(_199249, _199245)), elem(_199251, _199247), _199251 = _199249, _199247 = _199245], (258 ^ _197879) ^ [_207258, _207260] : [m_Ldr(_207260) = m_NotNorm(_207258)], (553 ^ _197879) ^ [_217928, _217930] : [-(leq(_217930, _217928)), -(leq(_217928, _217930))], (587 ^ _197879) ^ [_219058, _219060] : [leq(_219060, _219058), -(leq(s(_219060), s(_219058)))], (368 ^ _197879) ^ [_211490, _211492, _211494] : [-(snoc(cons(_211494, _211490), _211492) = cons(_211494, snoc(_211490, _211492)))], (366 ^ _197879) ^ [_211378] : [-(cons(_211378, q_nil) = snoc(q_nil, _211378))], (274 ^ _197879) ^ [_207924, _207926] : [-(_207926 = _207924), m_NormQ(_207926) = m_NormQ(_207924)], (298 ^ _197879) ^ [_208778, _208780] : [-(_208780 = _208778), m_Ldr(_208780) = m_Ldr(_208778)], (435 ^ _197879) ^ [_213802] : [-(ordered(snoc(q_nil, _213802)))], (593 ^ _197879) ^ [_219228, _219230] : [leq(s(_219230), s(_219228)), -(leq(_219230, _219228))], (549 ^ _197879) ^ [_217741] : [leq(s(_217741), _217741)], (523 ^ _197879) ^ [_216895, _216897, _216899] : [ordered(_216899), -(ordered(snoc(_216899, m_Ack(_216897, _216895))))], (599 ^ _197879) ^ [_219477, _219479] : [leq(_219479, s(_219477)), -(_219479 = s(_219477)), -(leq(_219479, _219477))], (254 ^ _197879) ^ [_207064, _207066] : [m_Ldr(_207066) = m_Halt(_207064)], (362 ^ _197879) ^ [_211199, _211201] : [q_nil = cons(_211201, _211199)], (106 ^ _197879) ^ [_201415, _201417] : [_201417 = _201415, -(init(_201417) = init(_201415))], (134 ^ _197879) ^ [_202428, _202430] : [_202430 = _202428, -(m_Ldr(_202430) = m_Ldr(_202428))], (256 ^ _197879) ^ [_207161, _207163] : [m_Ldr(_207163) = m_NormQ(_207161)], (427 ^ _197879) ^ [_213519] : [-(pidMsg(m_Halt(_213519)) = _213519)], (88 ^ _197879) ^ [_200761, _200763] : [_200763 = _200761, -(m_NotNorm(_200763) = m_NotNorm(_200761))], (372 ^ _197879) ^ [_211733, _211735, _211737] : [elem(_211737, cons(_211735, _211733)), -(_211737 = _211735), -(elem(_211737, _211733))], (162 ^ _197879) ^ [_203469, _203471, _203473, _203475] : [-(m_Ack(_203475, _203471) = m_Ack(_203473, _203469)), _203475 = _203473, _203471 = _203469], (262 ^ _197879) ^ [_207497, _207499] : [-(_207499 = _207497), m_Halt(_207499) = m_Halt(_207497)], (228 ^ _197879) ^ [] : [elec_2 = norm], (609 ^ _197879) ^ [_219737, _219739] : [610 ^ _197879 : [(613 ^ _197879) ^ [] : [leq(_219739, _219737)], (611 ^ _197879) ^ [] : [_219739 = s(_219737)]], -(leq(_219739, s(_219737)))], (431 ^ _197879) ^ [] : [-(ordered(q_nil))], (400 ^ _197879) ^ [_212612, _212614, _212616] : [401 ^ _197879 : [(404 ^ _197879) ^ [] : [elem(_212616, _212612)], (402 ^ _197879) ^ [] : [_212616 = _212614]], -(elem(_212616, snoc(_212612, _212614)))], (226 ^ _197879) ^ [] : [elec_2 = wait], (569 ^ _197879) ^ [_218419, _218421] : [_218421 = _218419, 572 ^ _197879 : [(575 ^ _197879) ^ [] : [-(leq(_218419, _218421))], (573 ^ _197879) ^ [] : [-(leq(_218421, _218419))]]], (551 ^ _197879) ^ [_217821] : [-(leq(_217821, _217821))], (224 ^ _197879) ^ [] : [elec_1 = norm], (504 ^ _197879) ^ [_216143, _216145] : [-(ordered(snoc(_216143, _216145))), ordered(_216143), 510 ^ _197879 : [(511 ^ _197879) ^ [] : [-(elem(509 ^ [_216143, _216145], _216143))], (515 ^ _197879) ^ [] : [-(pidElem(509 ^ [_216143, _216145]))], (519 ^ _197879) ^ [] : [leq(pidMsg(509 ^ [_216143, _216145]), pidMsg(_216145))], (517 ^ _197879) ^ [] : [-(host(pidMsg(509 ^ [_216143, _216145])) = host(pidMsg(_216145)))], (513 ^ _197879) ^ [] : [-(pidElem(_216145))]]], (529 ^ _197879) ^ [_217119, _217121] : [ordered(_217121), -(ordered(snoc(_217121, m_Ldr(_217119))))], (230 ^ _197879) ^ [] : [norm = wait], (240 ^ _197879) ^ [_206382, _206384, _206386] : [m_Ack(_206386, _206384) = m_NormQ(_206382)], (118 ^ _197879) ^ [_201851, _201853] : [_201853 = _201851, -(pidMsg(_201853) = pidMsg(_201851))], (234 ^ _197879) ^ [_206040, _206042, _206044] : [m_Ack(_206044, _206042) = m_Down(_206040)]], input).
% 52.56/51.01 ncf('1',plain,[setIn(921 ^ [], alive), elem(m_Down(920 ^ []), queue(host(921 ^ []))), 814 : -(leq(s(zero), 810 ^ [620 ^ [], 621 ^ [], 920 ^ [], 921 ^ []])), 814 : elem(m_Down(621 ^ []), queue(host(620 ^ []))), 814 : host(620 ^ []) = nbr_proc, 814 : host(620 ^ []) = host(920 ^ []), 814 : index(status, host(620 ^ [])) = elec_1],start(807 ^ 0,bind([[_231310, _231312, _231314, _231316], [620 ^ [], 621 ^ [], 920 ^ [], 921 ^ []]]))).
% 52.56/51.01 ncf('1.1',plain,[-(setIn(921 ^ [], alive))],extension(925 ^ 1)).
% 52.56/51.01 ncf('1.2',plain,[-(elem(m_Down(920 ^ []), queue(host(921 ^ []))))],extension(927 ^ 1)).
% 52.56/51.01 ncf('1.3',plain,[leq(s(zero), 810 ^ [620 ^ [], 621 ^ [], 920 ^ [], 921 ^ []]), -(leq(host(620 ^ []), 810 ^ [620 ^ [], 621 ^ [], 920 ^ [], 921 ^ []])), -(setIn(810 ^ [620 ^ [], 621 ^ [], 920 ^ [], 921 ^ []], index(down, host(620 ^ [])))), -(810 ^ [620 ^ [], 621 ^ [], 920 ^ [], 921 ^ []] = host(621 ^ []))],extension(896 ^ 3,bind([[_234001], [810 ^ [620 ^ [], 621 ^ [], 920 ^ [], 921 ^ []]]]))).
% 52.56/51.01 ncf('1.3.1',plain,[leq(host(620 ^ []), 810 ^ [620 ^ [], 621 ^ [], 920 ^ [], 921 ^ []])],extension(812 ^ 4)).
% 52.56/51.01 ncf('1.3.2',plain,[setIn(810 ^ [620 ^ [], 621 ^ [], 920 ^ [], 921 ^ []], index(down, host(620 ^ [])))],extension(816 ^ 4)).
% 52.56/51.01 ncf('1.3.3',plain,[810 ^ [620 ^ [], 621 ^ [], 920 ^ [], 921 ^ []] = host(621 ^ [])],extension(818 ^ 4)).
% 52.56/51.01 ncf('1.4',plain,[-(elem(m_Down(621 ^ []), queue(host(620 ^ [])))), elem(m_Down(621 ^ []), snoc(queue(host(620 ^ [])), m_Down(621 ^ []))), -(m_Down(621 ^ []) = m_Down(621 ^ []))],extension(390 ^ 1,bind([[_212344, _212346, _212348], [queue(host(620 ^ [])), m_Down(621 ^ []), m_Down(621 ^ [])]]))).
% 52.56/51.01 ncf('1.4.1',plain,[-(elem(m_Down(621 ^ []), snoc(queue(host(620 ^ [])), m_Down(621 ^ [])))), 402 : m_Down(621 ^ []) = m_Down(621 ^ [])],extension(400 ^ 2,bind([[_212612, _212614, _212616], [queue(host(620 ^ [])), m_Down(621 ^ []), m_Down(621 ^ [])]]))).
% 52.56/51.01 ncf('1.4.1.1',plain,[-(m_Down(621 ^ []) = m_Down(621 ^ []))],extension(2 ^ 5,bind([[_198003], [m_Down(621 ^ [])]]))).
% 52.56/51.01 ncf('1.4.2',plain,[m_Down(621 ^ []) = m_Down(621 ^ []), -(elem(m_Down(621 ^ []), queue(host(620 ^ [])))), elem(m_Down(621 ^ []), cons(m_Down(621 ^ []), 618 ^ [])), cons(m_Down(621 ^ []), 618 ^ []) = queue(host(620 ^ []))],extension(40 ^ 2,bind([[_199245, _199247, _199249, _199251], [queue(host(620 ^ [])), cons(m_Down(621 ^ []), 618 ^ []), m_Down(621 ^ []), m_Down(621 ^ [])]]))).
% 52.56/51.01 ncf('1.4.2.1',plain,[elem(m_Down(621 ^ []), queue(host(620 ^ [])))],reduction('1')).
% 52.56/51.01 ncf('1.4.2.2',plain,[-(elem(m_Down(621 ^ []), cons(m_Down(621 ^ []), 618 ^ []))), 384 : m_Down(621 ^ []) = m_Down(621 ^ [])],extension(382 ^ 3,bind([[_212001, _212003, _212005], [618 ^ [], m_Down(621 ^ []), m_Down(621 ^ [])]]))).
% 52.56/51.01 ncf('1.4.2.2.1',plain,[-(m_Down(621 ^ []) = m_Down(621 ^ []))],reduction('1.4')).
% 52.56/51.01 ncf('1.4.2.3',plain,[-(cons(m_Down(621 ^ []), 618 ^ []) = queue(host(620 ^ []))), queue(host(620 ^ [])) = cons(m_Down(621 ^ []), 618 ^ [])],extension(4 ^ 3,bind([[_198110, _198112], [cons(m_Down(621 ^ []), 618 ^ []), queue(host(620 ^ []))]]))).
% 52.56/51.01 ncf('1.4.2.3.1',plain,[-(queue(host(620 ^ [])) = cons(m_Down(621 ^ []), 618 ^ []))],extension(878 ^ 4)).
% 52.56/51.01 ncf('1.5',plain,[-(host(620 ^ []) = nbr_proc), leq(host(620 ^ []), nbr_proc), leq(nbr_proc, host(620 ^ []))],extension(559 ^ 1,bind([[_218168, _218170], [nbr_proc, host(620 ^ [])]]))).
% 52.56/51.01 ncf('1.5.1',plain,[-(leq(host(620 ^ []), nbr_proc))],extension(218 ^ 2,bind([[_205507], [620 ^ []]]))).
% 52.56/51.01 ncf('1.5.2',plain,[-(leq(nbr_proc, host(620 ^ [])))],extension(912 ^ 2)).
% 52.56/51.01 ncf('1.6',plain,[-(host(620 ^ []) = host(920 ^ [])), leq(host(620 ^ []), host(920 ^ [])), leq(host(920 ^ []), host(620 ^ []))],extension(559 ^ 1,bind([[_218168, _218170], [host(920 ^ []), host(620 ^ [])]]))).
% 52.56/51.01 ncf('1.6.1',plain,[-(leq(host(620 ^ []), host(920 ^ []))), leq(nbr_proc, s(index(pendack, host(921 ^ [])))), nbr_proc = host(620 ^ []), s(index(pendack, host(921 ^ []))) = host(920 ^ [])],extension(54 ^ 2,bind([[_199689, _199691, _199693, _199695], [host(920 ^ []), s(index(pendack, host(921 ^ []))), host(620 ^ []), nbr_proc]]))).
% 52.56/51.01 ncf('1.6.1.1',plain,[-(leq(nbr_proc, s(index(pendack, host(921 ^ [])))))],extension(931 ^ 3)).
% 52.56/51.01 ncf('1.6.1.2',plain,[-(nbr_proc = host(620 ^ [])), host(620 ^ []) = nbr_proc],extension(4 ^ 3,bind([[_198110, _198112], [nbr_proc, host(620 ^ [])]]))).
% 52.56/51.01 ncf('1.6.1.2.1',plain,[-(host(620 ^ []) = nbr_proc)],lemmata('x')).
% 52.56/51.01 ncf('1.6.1.3',plain,[-(s(index(pendack, host(921 ^ []))) = host(920 ^ [])), host(920 ^ []) = s(index(pendack, host(921 ^ [])))],extension(4 ^ 3,bind([[_198110, _198112], [s(index(pendack, host(921 ^ []))), host(920 ^ [])]]))).
% 52.56/51.01 ncf('1.6.1.3.1',plain,[-(host(920 ^ []) = s(index(pendack, host(921 ^ []))))],extension(937 ^ 4)).
% 52.56/51.01 ncf('1.6.2',plain,[-(leq(host(920 ^ []), host(620 ^ []))), leq(host(920 ^ []), nbr_proc), leq(nbr_proc, host(620 ^ []))],extension(577 ^ 2,bind([[_218720, _218722, _218724], [host(620 ^ []), nbr_proc, host(920 ^ [])]]))).
% 52.56/51.01 ncf('1.6.2.1',plain,[-(leq(host(920 ^ []), nbr_proc))],extension(218 ^ 3,bind([[_205507], [920 ^ []]]))).
% 52.56/51.01 ncf('1.6.2.2',plain,[-(leq(nbr_proc, host(620 ^ [])))],extension(912 ^ 3)).
% 52.56/51.01 ncf('1.7',plain,[-(index(status, host(620 ^ [])) = elec_1)],extension(910 ^ 1)).
% 52.56/51.01 %-----------------------------------------------------
% 52.56/51.01 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------