%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV461+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n010.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 239.09s 230.99s
% Output : Proof 239.09s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWV461+1 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n010.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:24:12 EDT 2023
% 0.13/0.34 % CPUTime :
% 239.09/230.99
% 239.09/230.99 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 239.09/230.99 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 239.09/230.99 %-----------------------------------------------------
% 239.09/230.99 ncf(matrix, plain, [(920 ^ _215406) ^ [] : [-(index(status, host(902 ^ [])) = elec_2)], (811 ^ _215406) ^ [_221408, _221410, _221412, _221414] : [setIn(_221414, alive), elem(m_Down(_221412), queue(host(_221414))), 815 ^ _215406 : [(820 ^ _215406) ^ [] : [setIn(814 ^ [_221408, _221410, _221412, _221414], index(down, host(_221408)))], (816 ^ _215406) ^ [] : [leq(host(_221408), 814 ^ [_221408, _221410, _221412, _221414])], (818 ^ _215406) ^ [] : [-(leq(s(zero), 814 ^ [_221408, _221410, _221412, _221414]))], (822 ^ _215406) ^ [] : [814 ^ [_221408, _221410, _221412, _221414] = host(_221410)]], elem(m_Down(_221410), queue(host(_221408))), host(_221408) = host(_221412), host(_221408) = nbr_proc, index(status, host(_221408)) = elec_1], (896 ^ _215406) ^ [] : [leq(nbr_proc, host(618 ^ []))], (894 ^ _215406) ^ [] : [-(host(618 ^ []) = s(zero))], (934 ^ _215406) ^ [] : [-(index(status, host(897 ^ [])) = norm)], (882 ^ _215406) ^ [] : [-(queue(host(619 ^ [])) = q_nil)], (651 ^ _215406) ^ [_216660, _216662] : [-(_216660 = _216662), host(_216660) = host(_216662), setIn(_216662, alive), setIn(_216660, alive)], (645 ^ _215406) ^ [_216421, _216423, _216425] : [elem(m_Ack(_216421, _216425), queue(host(_216423))), leq(host(_216425), host(_216421))], (914 ^ _215406) ^ [] : [-(leq(nbr_proc, s(index(pendack, host(902 ^ [])))))], (899 ^ _215406) ^ [] : [host(618 ^ []) = host(897 ^ [])], (719 ^ _215406) ^ [_218757, _218759, _218761] : [elem(m_Ack(_218761, _218759), queue(host(_218761))), setIn(_218761, alive), setIn(_218757, alive), host(_218757) = host(_218759), index(status, host(_218761)) = elec_2, index(status, host(_218757)) = elec_2], (763 ^ _215406) ^ [_219999, _220001] : [leq(index(pendack, host(_220001)), index(pendack, host(_219999))), -(leq(host(_220001), host(_219999))), setIn(_220001, alive), setIn(_219999, alive), index(status, host(_220001)) = elec_2, index(status, host(_219999)) = elec_2], (932 ^ _215406) ^ [] : [-(index(ldr, host(897 ^ [])) = host(897 ^ []))], (844 ^ _215406) ^ [_222558, _222560, _222562, _222564] : [setIn(_222564, alive), index(ldr, host(_222564)) = host(_222564), index(status, host(_222564)) = norm, setIn(_222558, alive), elem(m_Down(_222560), queue(host(_222558))), elem(m_Ack(_222558, _222562), queue(host(_222558))), leq(nbr_proc, s(index(pendack, host(_222558)))), index(status, host(_222558)) = elec_2, host(_222562) = index(pendack, host(_222558)), host(_222560) = s(index(pendack, host(_222558)))], (904 ^ _215406) ^ [] : [-(s(host(618 ^ [])) = host(902 ^ []))], (675 ^ _215406) ^ [_217391, _217393] : [elem(m_Ack(_217391, _217393), queue(host(_217391))), setIn(_217391, alive), index(status, host(_217391)) = elec_1], (627 ^ _215406) ^ [_215714, _215716] : [elem(m_Ldr(_215714), queue(host(_215716))), leq(host(_215716), host(_215714))], (639 ^ _215406) ^ [_216176, _216178] : [elem(m_Halt(_216176), queue(host(_216178))), leq(host(_216178), host(_216176))], (697 ^ _215406) ^ [_218106, _218108, _218110] : [setIn(_218106, alive), elem(m_Down(_218108), queue(host(_218106))), host(_218108) = host(_218110), setIn(_218110, alive), index(ldr, host(_218110)) = host(_218110), index(status, host(_218110)) = norm], (922 ^ _215406) ^ [] : [-(host(900 ^ []) = index(pendack, host(902 ^ [])))], (621 ^ _215406) ^ [_215505] : [host(619 ^ []) = host(_215505), setIn(_215505, alive)], (665 ^ _215406) ^ [_217064, _217066] : [-(leq(host(_217066), index(pendack, host(_217064)))), setIn(_217064, alive), elem(m_Ack(_217064, _217066), queue(host(_217064)))], (892 ^ _215406) ^ [] : [-(host(619 ^ []) = host(618 ^ []))], (884 ^ _215406) ^ [_223788] : [host(619 ^ []) = host(_223788), -(leq(_223788, 618 ^ []))], (890 ^ _215406) ^ [] : [setIn(618 ^ [], pids)], (926 ^ _215406) ^ [] : [-(setIn(897 ^ [], alive)), -(897 ^ [] = 618 ^ [])], (741 ^ _215406) ^ [_219388, _219390] : [-(leq(index(pendack, host(_219388)), host(_219390))), -(leq(host(_219390), host(_219388))), setIn(_219390, alive), setIn(_219388, alive), index(status, host(_219390)) = elec_2, index(status, host(_219388)) = elec_2], (924 ^ _215406) ^ [] : [-(host(901 ^ []) = s(index(pendack, host(902 ^ []))))], (785 ^ _215406) ^ [_220631, _220633, _220635] : [setIn(_220635, alive), index(ldr, host(_220635)) = host(_220635), index(status, host(_220635)) = norm, -(leq(index(pendack, host(_220631)), host(_220635))), setIn(_220631, alive), elem(m_Halt(_220631), queue(host(_220633))), index(status, host(_220631)) = elec_2], (633 ^ _215406) ^ [_215945, _215947] : [elem(m_Down(_215945), queue(host(_215947))), host(_215945) = host(_215947)], (906 ^ _215406) ^ [] : [host(618 ^ []) = host(902 ^ [])], (916 ^ _215406) ^ [] : [-(elem(m_Down(901 ^ []), snoc(queue(host(902 ^ [])), m_Halt(618 ^ []))))], (908 ^ _215406) ^ [] : [-(setIn(902 ^ [], alive)), -(902 ^ [] = 618 ^ [])], (918 ^ _215406) ^ [] : [-(elem(m_Ack(902 ^ [], 900 ^ []), snoc(queue(host(902 ^ [])), m_Halt(618 ^ []))))], (685 ^ _215406) ^ [_217701] : [-(index(elid, host(_217701)) = _217701), 688 ^ _215406 : [(689 ^ _215406) ^ [] : [index(status, host(_217701)) = elec_1], (691 ^ _215406) ^ [] : [index(status, host(_217701)) = elec_2]], setIn(_217701, alive)], !, (146 ^ _190385) ^ [_195398, _195400, _195402, _195404] : [-(m_Ack(_195404, _195400) = m_Ack(_195402, _195398)), _195404 = _195402, _195400 = _195398], (342 ^ _190385) ^ [_202900, _202902] : [-(head(cons(_202902, _202900)) = _202902)], (218 ^ _190385) ^ [_198013] : [-(leq(host(_198013), nbr_proc))], (260 ^ _190385) ^ [_199861, _199863] : [m_NormQ(_199863) = m_NotNorm(_199861)], (523 ^ _190385) ^ [_209401, _209403, _209405] : [ordered(_209405), -(ordered(snoc(_209405, m_Ack(_209403, _209401))))], (609 ^ _190385) ^ [_212243, _212245] : [610 ^ _190385 : [(611 ^ _190385) ^ [] : [_212245 = s(_212243)], (613 ^ _190385) ^ [] : [leq(_212245, _212243)]], -(leq(_212245, s(_212243)))], (234 ^ _190385) ^ [_198546, _198548, _198550] : [m_Ack(_198550, _198548) = m_Down(_198546)], (310 ^ _190385) ^ [_201711, _201713] : [-(_201713 = _201711), m_Down(_201713) = m_Down(_201711)], (106 ^ _190385) ^ [_193921, _193923] : [_193923 = _193921, -(init(_193923) = init(_193921))], (593 ^ _190385) ^ [_211734, _211736] : [leq(s(_211736), s(_211734)), -(leq(_211736, _211734))], (322 ^ _190385) ^ [_202137, _202139, _202141, _202143] : [-(_202143 = _202141), m_Ack(_202143, _202139) = m_Ack(_202141, _202137)], (140 ^ _190385) ^ [_195152, _195154] : [_195154 = _195152, -(m_Down(_195154) = m_Down(_195152))], (236 ^ _190385) ^ [_198660, _198662, _198664] : [m_Ack(_198664, _198662) = m_NotNorm(_198660)], (252 ^ _190385) ^ [_199473, _199475] : [m_NormQ(_199475) = m_Halt(_199473)], (529 ^ _190385) ^ [_209625, _209627] : [ordered(_209627), -(ordered(snoc(_209627, m_Ldr(_209625))))], (226 ^ _190385) ^ [] : [elec_2 = wait], (262 ^ _190385) ^ [_200003, _200005] : [-(_200005 = _200003), m_Halt(_200005) = m_Halt(_200003)], (429 ^ _190385) ^ [_206107] : [-(pidMsg(m_Down(_206107)) = _206107)], (346 ^ _190385) ^ [_203098, _203100] : [-(last(snoc(_203098, _203100)) = _203100)], (316 ^ _190385) ^ [_201885, _201887] : [-(m_Down(_201887) = m_Down(_201885)), _201887 = _201885], (156 ^ _190385) ^ [_195757, _195759, _195761, _195763] : [-(snoc(_195763, _195759) = snoc(_195761, _195757)), _195763 = _195761, _195759 = _195757], (82 ^ _190385) ^ [_193049, _193051] : [_193051 = _193049, -(m_NormQ(_193051) = m_NormQ(_193049))], (166 ^ _190385) ^ [_196088, _196090] : [_196090 = _196088, -(queue(_196090) = queue(_196088))], (382 ^ _190385) ^ [_204507, _204509, _204511] : [383 ^ _190385 : [(384 ^ _190385) ^ [] : [_204511 = _204509], (386 ^ _190385) ^ [] : [elem(_204511, _204507)]], -(elem(_204511, cons(_204509, _204507)))], (172 ^ _190385) ^ [_196306, _196308] : [_196308 = _196306, -(m_Halt(_196308) = m_Halt(_196306))], (328 ^ _190385) ^ [_202403, _202405, _202407, _202409] : [-(_202405 = _202403), m_Ack(_202409, _202405) = m_Ack(_202407, _202403)], (238 ^ _190385) ^ [_198774, _198776, _198778] : [m_Ack(_198778, _198776) = m_Ldr(_198774)], (427 ^ _190385) ^ [_206025] : [-(pidMsg(m_Halt(_206025)) = _206025)], (222 ^ _190385) ^ [] : [elec_1 = wait], (54 ^ _190385) ^ [_192195, _192197, _192199, _192201] : [-(elem(_192199, _192195)), elem(_192201, _192197), _192201 = _192199, _192197 = _192195], (254 ^ _190385) ^ [_199570, _199572] : [m_Ldr(_199572) = m_Halt(_199570)], (461 ^ _190385) ^ [_207165, _207167] : [-(ordered(cons(_207167, _207165))), ordered(_207165), 467 ^ _190385 : [(476 ^ _190385) ^ [] : [leq(pidMsg(_207167), pidMsg(466 ^ [_207165, _207167]))], (474 ^ _190385) ^ [] : [-(host(pidMsg(466 ^ [_207165, _207167])) = host(pidMsg(_207167)))], (472 ^ _190385) ^ [] : [-(pidElem(466 ^ [_207165, _207167]))], (468 ^ _190385) ^ [] : [-(elem(466 ^ [_207165, _207167], _207165))], (470 ^ _190385) ^ [] : [-(pidElem(_207167))]]], (366 ^ _190385) ^ [_203884] : [-(cons(_203884, q_nil) = snoc(q_nil, _203884))], (250 ^ _190385) ^ [_199376, _199378] : [m_Down(_199378) = m_NormQ(_199376)], (362 ^ _190385) ^ [_203705, _203707] : [q_nil = cons(_203707, _203705)], (240 ^ _190385) ^ [_198888, _198890, _198892] : [m_Ack(_198892, _198890) = m_NormQ(_198888)], (30 ^ _190385) ^ [_191428, _191430] : [-(ordered(_191428)), _191430 = _191428, ordered(_191430)], (431 ^ _190385) ^ [] : [-(ordered(q_nil))], (280 ^ _190385) ^ [_200604, _200606] : [-(m_NormQ(_200606) = m_NormQ(_200604)), _200606 = _200604], (268 ^ _190385) ^ [_200177, _200179] : [-(m_Halt(_200179) = m_Halt(_200177)), _200179 = _200177], (248 ^ _190385) ^ [_199279, _199281] : [m_Down(_199281) = m_NotNorm(_199279)], (433 ^ _190385) ^ [_206262] : [-(ordered(cons(_206262, q_nil)))], (216 ^ _190385) ^ [] : [-(leq(s(zero), nbr_proc))], (480 ^ _190385) ^ [_207932, _207934] : [ordered(snoc(_207932, _207934)), 483 ^ _190385 : [(484 ^ _190385) ^ [] : [-(ordered(_207932))], (486 ^ _190385) ^ [_208171] : [-(leq(pidMsg(_208171), pidMsg(_207934))), elem(_208171, _207932), pidElem(_207934), pidElem(_208171), host(pidMsg(_208171)) = host(pidMsg(_207934))]]], (68 ^ _190385) ^ [_192619, _192621, _192623, _192625] : [-(setIn(_192623, _192619)), setIn(_192625, _192621), _192625 = _192623, _192621 = _192619], (224 ^ _190385) ^ [] : [elec_1 = norm], (20 ^ _190385) ^ [_191133, _191135] : [-(pidElem(_191133)), _191135 = _191133, pidElem(_191135)], (344 ^ _190385) ^ [_202999, _203001] : [-(tail(cons(_203001, _202999)) = _202999)], (419 ^ _190385) ^ [_205747] : [420 ^ _190385 : [(421 ^ _190385) ^ [_205844] : [_205747 = m_Halt(_205844)], (423 ^ _190385) ^ [_205891] : [_205747 = m_Down(_205891)]], -(pidElem(_205747))], (4 ^ _190385) ^ [_190616, _190618] : [_190618 = _190616, -(_190616 = _190618)], (2 ^ _190385) ^ [_190509] : [-(_190509 = _190509)], (200 ^ _190385) ^ [_197379, _197381] : [elem(m_Ack(_197381, _197379), queue(host(_197381))), 203 ^ _190385 : [(204 ^ _190385) ^ [] : [-(setIn(_197381, pids))], (206 ^ _190385) ^ [] : [-(setIn(_197379, pids))]]], (368 ^ _190385) ^ [_203996, _203998, _204000] : [-(snoc(cons(_204000, _203996), _203998) = cons(_204000, snoc(_203996, _203998)))], (549 ^ _190385) ^ [_210247] : [leq(s(_210247), _210247)], (220 ^ _190385) ^ [] : [elec_1 = elec_2], (292 ^ _190385) ^ [_201031, _201033] : [-(m_NotNorm(_201033) = m_NotNorm(_201031)), _201033 = _201031], (504 ^ _190385) ^ [_208649, _208651] : [-(ordered(snoc(_208649, _208651))), ordered(_208649), 510 ^ _190385 : [(519 ^ _190385) ^ [] : [leq(pidMsg(509 ^ [_208649, _208651]), pidMsg(_208651))], (517 ^ _190385) ^ [] : [-(host(pidMsg(509 ^ [_208649, _208651])) = host(pidMsg(_208651)))], (515 ^ _190385) ^ [] : [-(pidElem(509 ^ [_208649, _208651]))], (511 ^ _190385) ^ [] : [-(elem(509 ^ [_208649, _208651], _208649))], (513 ^ _190385) ^ [] : [-(pidElem(_208651))]]], (178 ^ _190385) ^ [_196524, _196526] : [_196526 = _196524, -(s(_196526) = s(_196524))], (10 ^ _190385) ^ [_190820, _190822, _190824] : [-(_190824 = _190820), _190824 = _190822, _190822 = _190820], (184 ^ _190385) ^ [_196770, _196772, _196774, _196776] : [-(index(_196776, _196772) = index(_196774, _196770)), _196776 = _196774, _196772 = _196770], (298 ^ _190385) ^ [_201284, _201286] : [-(_201286 = _201284), m_Ldr(_201286) = m_Ldr(_201284)], (372 ^ _190385) ^ [_204239, _204241, _204243] : [elem(_204243, cons(_204241, _204239)), -(_204243 = _204241), -(elem(_204243, _204239))], (286 ^ _190385) ^ [_200857, _200859] : [-(_200859 = _200857), m_NotNorm(_200859) = m_NotNorm(_200857)], (551 ^ _190385) ^ [_210327] : [-(leq(_210327, _210327))], (246 ^ _190385) ^ [_199182, _199184] : [m_Down(_199184) = m_Ldr(_199182)], (118 ^ _190385) ^ [_194357, _194359] : [_194359 = _194357, -(pidMsg(_194359) = pidMsg(_194357))], (577 ^ _190385) ^ [_211226, _211228, _211230] : [-(leq(_211230, _211226)), leq(_211230, _211228), leq(_211228, _211226)], (88 ^ _190385) ^ [_193267, _193269] : [_193269 = _193267, -(m_NotNorm(_193269) = m_NotNorm(_193267))], (208 ^ _190385) ^ [_197678, _197680] : [s(host(_197680)) = host(_197678), host(_197680) = host(_197678)], (228 ^ _190385) ^ [] : [elec_2 = norm], (587 ^ _190385) ^ [_211564, _211566] : [leq(_211566, _211564), -(leq(s(_211566), s(_211564)))], (617 ^ _190385) ^ [_212487] : [setIn(_212487, setEmpty)], (435 ^ _190385) ^ [_206308] : [-(ordered(snoc(q_nil, _206308)))], (400 ^ _190385) ^ [_205118, _205120, _205122] : [401 ^ _190385 : [(402 ^ _190385) ^ [] : [_205122 = _205120], (404 ^ _190385) ^ [] : [elem(_205122, _205118)]], -(elem(_205122, snoc(_205118, _205120)))], (124 ^ _190385) ^ [_194603, _194605, _194607, _194609] : [-(cons(_194609, _194605) = cons(_194607, _194603)), _194609 = _194607, _194605 = _194603], (244 ^ _190385) ^ [_199085, _199087] : [m_Down(_199087) = m_Halt(_199085)], (364 ^ _190385) ^ [_203801, _203803] : [q_nil = snoc(_203801, _203803)], (553 ^ _190385) ^ [_210434, _210436] : [-(leq(_210436, _210434)), -(leq(_210434, _210436))], (194 ^ _190385) ^ [_197081, _197083] : [_197083 = _197081, -(host(_197083) = host(_197081))], (334 ^ _190385) ^ [_202641, _202643] : [-(host(_202643) = host(_202641)), _202643 = _202641], (256 ^ _190385) ^ [_199667, _199669] : [m_Ldr(_199669) = m_NormQ(_199667)], (134 ^ _190385) ^ [_194934, _194936] : [_194936 = _194934, -(m_Ldr(_194936) = m_Ldr(_194934))], (230 ^ _190385) ^ [] : [norm = wait], (94 ^ _190385) ^ [_193485, _193487] : [_193487 = _193485, -(head(_193487) = head(_193485))], (304 ^ _190385) ^ [_201458, _201460] : [-(m_Ldr(_201460) = m_Ldr(_201458)), _201460 = _201458], (340 ^ _190385) ^ [] : [setIn(nil, alive)], (112 ^ _190385) ^ [_194139, _194141] : [_194141 = _194139, -(last(_194141) = last(_194139))], (214 ^ _190385) ^ [_197880] : [-(leq(s(zero), host(_197880)))], (356 ^ _190385) ^ [_203502] : [-(_203502 = q_nil), -(_203502 = snoc(init(_203502), last(_203502)))], (408 ^ _190385) ^ [_205433] : [pidElem(_205433), -(_205433 = m_Halt(411 ^ [_205433])), -(_205433 = m_Down(411 ^ [_205433]))], (599 ^ _190385) ^ [_211983, _211985] : [leq(_211985, s(_211983)), -(_211985 = s(_211983)), -(leq(_211985, _211983))], (535 ^ _190385) ^ [_209855, _209857, _209859] : [-(leq(_209857, _209855)), ordered(cons(m_Halt(_209857), _209859)), host(_209857) = host(_209855), elem(m_Down(_209855), _209859)], (350 ^ _190385) ^ [_203297] : [-(_203297 = q_nil), -(_203297 = cons(head(_203297), tail(_203297)))], (569 ^ _190385) ^ [_210925, _210927] : [_210927 = _210925, 572 ^ _190385 : [(573 ^ _190385) ^ [] : [-(leq(_210927, _210925))], (575 ^ _190385) ^ [] : [-(leq(_210925, _210927))]]], (258 ^ _190385) ^ [_199764, _199766] : [m_Ldr(_199766) = m_NotNorm(_199764)], (390 ^ _190385) ^ [_204850, _204852, _204854] : [elem(_204854, snoc(_204850, _204852)), -(_204854 = _204852), -(elem(_204854, _204850))], (370 ^ _190385) ^ [_204089] : [elem(_204089, q_nil)], (232 ^ _190385) ^ [_198432, _198434, _198436] : [m_Ack(_198436, _198434) = m_Halt(_198432)], (242 ^ _190385) ^ [_198988, _198990] : [m_NotNorm(_198990) = m_Halt(_198988)], (348 ^ _190385) ^ [_203197, _203199] : [-(init(snoc(_203197, _203199)) = _203197)], (40 ^ _190385) ^ [_191751, _191753, _191755, _191757] : [-(leq(_191755, _191751)), leq(_191757, _191753), _191757 = _191755, _191753 = _191751], (274 ^ _190385) ^ [_200430, _200432] : [-(_200432 = _200430), m_NormQ(_200432) = m_NormQ(_200430)], (437 ^ _190385) ^ [_206448, _206450] : [ordered(cons(_206450, _206448)), 440 ^ _190385 : [(441 ^ _190385) ^ [] : [-(ordered(_206448))], (443 ^ _190385) ^ [_206687] : [-(leq(pidMsg(_206450), pidMsg(_206687))), elem(_206687, _206448), pidElem(_206450), pidElem(_206687), host(pidMsg(_206687)) = host(pidMsg(_206450))]]], (100 ^ _190385) ^ [_193703, _193705] : [_193705 = _193703, -(tail(_193705) = tail(_193703))], (559 ^ _190385) ^ [_210674, _210676] : [-(_210676 = _210674), leq(_210676, _210674), leq(_210674, _210676)]], input).
% 239.09/230.99 ncf('1',plain,[-(index(status, host(902 ^ [])) = elec_2)],start(920 ^ 0)).
% 239.09/230.99 ncf('1.1',plain,[index(status, host(902 ^ [])) = elec_2, setIn(897 ^ [], alive), index(ldr, host(897 ^ [])) = host(897 ^ []), index(status, host(897 ^ [])) = norm, setIn(902 ^ [], alive), elem(m_Down(901 ^ []), queue(host(902 ^ []))), elem(m_Ack(902 ^ [], 900 ^ []), queue(host(902 ^ []))), leq(nbr_proc, s(index(pendack, host(902 ^ [])))), host(900 ^ []) = index(pendack, host(902 ^ [])), host(901 ^ []) = s(index(pendack, host(902 ^ [])))],extension(844 ^ 1,bind([[_222558, _222560, _222562, _222564], [902 ^ [], 901 ^ [], 900 ^ [], 897 ^ []]]))).
% 239.09/230.99 ncf('1.1.1',plain,[-(setIn(897 ^ [], alive)), -(897 ^ [] = 618 ^ [])],extension(926 ^ 2)).
% 239.09/230.99 ncf('1.1.1.1',plain,[897 ^ [] = 618 ^ [], -(618 ^ [] = 897 ^ [])],extension(4 ^ 3,bind([[_190616, _190618], [618 ^ [], 897 ^ []]]))).
% 239.09/230.99 ncf('1.1.1.1.1',plain,[618 ^ [] = 897 ^ [], -(host(618 ^ []) = host(897 ^ []))],extension(194 ^ 4,bind([[_197081, _197083], [897 ^ [], 618 ^ []]]))).
% 239.09/230.99 ncf('1.1.1.1.1.1',plain,[host(618 ^ []) = host(897 ^ [])],extension(899 ^ 5)).
% 239.09/230.99 ncf('1.1.2',plain,[-(index(ldr, host(897 ^ [])) = host(897 ^ []))],extension(932 ^ 2)).
% 239.09/230.99 ncf('1.1.3',plain,[-(index(status, host(897 ^ [])) = norm)],extension(934 ^ 2)).
% 239.09/230.99 ncf('1.1.4',plain,[-(setIn(902 ^ [], alive)), -(902 ^ [] = 618 ^ [])],extension(908 ^ 2)).
% 239.09/230.99 ncf('1.1.4.1',plain,[902 ^ [] = 618 ^ [], -(618 ^ [] = 902 ^ [])],extension(4 ^ 3,bind([[_190616, _190618], [618 ^ [], 902 ^ []]]))).
% 239.09/230.99 ncf('1.1.4.1.1',plain,[618 ^ [] = 902 ^ [], -(host(618 ^ []) = host(902 ^ []))],extension(194 ^ 4,bind([[_197081, _197083], [902 ^ [], 618 ^ []]]))).
% 239.09/230.99 ncf('1.1.4.1.1.1',plain,[host(618 ^ []) = host(902 ^ [])],extension(906 ^ 5)).
% 239.09/230.99 ncf('1.1.5',plain,[-(elem(m_Down(901 ^ []), queue(host(902 ^ [])))), elem(m_Down(901 ^ []), snoc(queue(host(902 ^ [])), m_Halt(618 ^ []))), -(m_Down(901 ^ []) = m_Halt(618 ^ []))],extension(390 ^ 2,bind([[_204850, _204852, _204854], [queue(host(902 ^ [])), m_Halt(618 ^ []), m_Down(901 ^ [])]]))).
% 239.09/230.99 ncf('1.1.5.1',plain,[-(elem(m_Down(901 ^ []), snoc(queue(host(902 ^ [])), m_Halt(618 ^ []))))],extension(916 ^ 3)).
% 239.09/230.99 ncf('1.1.5.2',plain,[m_Down(901 ^ []) = m_Halt(618 ^ [])],extension(244 ^ 3,bind([[_199085, _199087], [618 ^ [], 901 ^ []]]))).
% 239.09/230.99 ncf('1.1.6',plain,[-(elem(m_Ack(902 ^ [], 900 ^ []), queue(host(902 ^ [])))), elem(m_Ack(902 ^ [], 900 ^ []), snoc(queue(host(902 ^ [])), m_Halt(618 ^ []))), -(m_Ack(902 ^ [], 900 ^ []) = m_Halt(618 ^ []))],extension(390 ^ 2,bind([[_204850, _204852, _204854], [queue(host(902 ^ [])), m_Halt(618 ^ []), m_Ack(902 ^ [], 900 ^ [])]]))).
% 239.09/230.99 ncf('1.1.6.1',plain,[-(elem(m_Ack(902 ^ [], 900 ^ []), snoc(queue(host(902 ^ [])), m_Halt(618 ^ []))))],extension(918 ^ 3)).
% 239.09/230.99 ncf('1.1.6.2',plain,[m_Ack(902 ^ [], 900 ^ []) = m_Halt(618 ^ [])],extension(232 ^ 3,bind([[_198432, _198434, _198436], [618 ^ [], 900 ^ [], 902 ^ []]]))).
% 239.09/230.99 ncf('1.1.7',plain,[-(leq(nbr_proc, s(index(pendack, host(902 ^ [])))))],extension(914 ^ 2)).
% 239.09/230.99 ncf('1.1.8',plain,[-(host(900 ^ []) = index(pendack, host(902 ^ [])))],extension(922 ^ 2)).
% 239.09/230.99 ncf('1.1.9',plain,[-(host(901 ^ []) = s(index(pendack, host(902 ^ []))))],extension(924 ^ 2)).
% 239.09/230.99 %-----------------------------------------------------
% 239.09/230.99 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------