%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWV458+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n016.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 : 600s
% DateTime : Wed Jul 20 19:51:08 EDT 2022
% Result : Theorem 220.38s 212.70s
% Output : Proof 220.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SWV458+1 : TPTP v8.1.0. Released v4.0.0.
% 0.04/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n016.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 : 600
% 0.12/0.33 % DateTime : Wed Jun 15 20:26:18 EDT 2022
% 0.12/0.33 % CPUTime :
% 220.38/212.70 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 220.45/212.71 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 220.45/212.71
% 220.45/212.71 %-----------------------------------------------------
% 220.45/212.71 fof(conj, conjecture, ! [_159652, _159655, _159658, _159661] : (! [_159669] : leq(index(pendack, host(_159669)), nbr_proc) & ! [_159669, _159700] : (elem(m_Down(_159700), queue(host(_159669))) => ~ setIn(_159700, alive)) & ! [_159669, _159700] : (elem(m_Ldr(_159700), queue(host(_159669))) => ~ leq(host(_159669), host(_159700))) & ! [_159669, _159700] : (elem(m_Halt(_159700), queue(host(_159669))) => ~ leq(host(_159669), host(_159700))) & ! [_159669, _159846, _159700] : (elem(m_Ack(_159700, _159669), queue(host(_159846))) => ~ leq(host(_159669), host(_159700))) & ! [_159669, _159700] : (~ setIn(_159669, alive) & leq(_159700, _159669) & host(_159700) = host(_159669) => ~ setIn(_159700, alive)) & ! [_159669, _159700] : ((! _159700) = _159669 & host(_159700) = host(_159669) => ~ setIn(_159669, alive) | ~ setIn(_159700, alive)) & ! [_159669] : ((index(status, host(_159669)) = elec_1 | index(status, host(_159669)) = elec_2) & setIn(_159669, alive) => index(elid, host(_159669)) = _159669) & ! [_159669, _159846, _159700] : (setIn(_159700, alive) & elem(m_Down(_159846), queue(host(_159700))) & host(_159846) = host(_159669) => ~ (setIn(_159669, alive) & index(ldr, host(_159669)) = host(_159669) & index(status, host(_159669)) = norm)) & ! [_159669, _159700] : (~ leq(host(_159669), host(_159700)) & setIn(_159669, alive) & setIn(_159700, alive) & index(status, host(_159669)) = elec_2 & index(status, host(_159700)) = elec_2 => leq(index(pendack, host(_159700)), host(_159669))) & ! [_159669, _159846, _159700] : (setIn(_159700, alive) & elem(m_Ack(_159700, _159846), queue(host(_159700))) & host(_159846) = host(_159669) => ~ (setIn(_159669, alive) & index(ldr, host(_159669)) = host(_159669) & index(status, host(_159669)) = norm)) & ! [_159669, _159700] : (~ leq(index(pendack, host(_159700)), host(_159669)) & setIn(_159700, alive) & index(status, host(_159700)) = elec_2 => ~ (setIn(_159669, alive) & index(ldr, host(_159669)) = host(_159669) & index(status, host(_159669)) = norm)) & ! [_159669, _159700] : (setIn(_159669, alive) & setIn(_159700, alive) & index(ldr, host(_159669)) = host(_159669) & index(status, host(_159669)) = norm & index(status, host(_159700)) = norm & index(ldr, host(_159700)) = host(_159700) => _159700 = _159669) & ! [_159669, _159700] : (~ leq(host(_159669), host(_159700)) & setIn(_159669, alive) & setIn(_159700, alive) & index(status, host(_159669)) = elec_2 & index(status, host(_159700)) = elec_2 => ~ leq(index(pendack, host(_159669)), index(pendack, host(_159700)))) & ! [_159669, _159846, _159700] : (~ leq(index(pendack, host(_159700)), host(_159669)) & setIn(_159700, alive) & elem(m_Halt(_159700), queue(host(_159846))) & index(status, host(_159700)) = elec_2 => ~ (setIn(_159669, alive) & index(ldr, host(_159669)) = host(_159669) & index(status, host(_159669)) = norm)) & ! [_159669, _159846, _159700] : (! [_160895] : (~ leq(host(_159700), _160895) & leq(s(zero), _160895) => setIn(_160895, index(down, host(_159700))) | _160895 = host(_159846)) & ~ leq(host(_159700), host(_159669)) & elem(m_Down(_159846), queue(host(_159700))) & index(status, host(_159700)) = elec_1 => ~ (setIn(_159669, alive) & index(ldr, host(_159669)) = host(_159669) & index(status, host(_159669)) = norm)) & queue(host(_159658)) = cons(m_Down(_159661), _159652) => setIn(_159658, alive) => ~ leq(host(_159658), host(_159661)) => ~ (index(ldr, host(_159658)) = host(_159661) & index(status, host(_159658)) = norm | index(status, host(_159658)) = wait & host(_159661) = host(index(elid, host(_159658)))) => ! [_159669] : (~ leq(host(_159658), _159669) & leq(s(zero), _159669) => setIn(_159669, index(down, host(_159658))) | _159669 = host(_159661)) & index(status, host(_159658)) = elec_1 => ~ leq(nbr_proc, host(_159658)) => ! [_159669] : ((! host(_159658)) = host(_159669) => ! [_161334] : (s(host(_159658)) = host(_161334) => (! host(_159658)) = host(_161334) => ! [_161376] : (host(_159658) = host(_161376) => ~ leq(s(host(_159658)), host(_159669)) & setIn(_161376, alive) & elem(m_Halt(_161376), snoc(queue(host(_161334)), m_Halt(_159658))) => ~ (setIn(_159669, alive) & index(ldr, host(_159669)) = host(_159669) & index(status, host(_159669)) = norm))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', conj)).
% 220.45/212.71 fof(axiom_46, axiom, ! [_165212, _165215, _165218] : (elem(_165212, cons(_165215, _165218)) <=> _165212 = _165215 | elem(_165212, _165218)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV011+0.ax', axiom_46)).
% 220.45/212.71 fof(axiom_61, axiom, ! [_165415, _165418] : (leq(_165415, _165418) & leq(_165418, _165415) <=> _165415 = _165418), file('/export/starexec/sandbox2/benchmark/Axioms/SWV011+0.ax', axiom_61)).
% 220.45/212.71 fof(axiom_60, axiom, ! [_165604, _165607] : (leq(_165604, _165607) | leq(_165607, _165604)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV011+0.ax', axiom_60)).
% 220.45/212.71 fof(axiom_64, axiom, ! [_165838, _165841] : (leq(_165838, s(_165841)) <=> _165838 = s(_165841) | leq(_165838, _165841)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV011+0.ax', axiom_64)).
% 220.45/212.71
% 220.45/212.71 cnf(1, plain, [_41275 = _41320, -(_41320 = _41275)], theory(equality)).
% 220.45/212.71 cnf(2, plain, [-(index(status, host(11 ^ [])) = norm)], clausify(conj)).
% 220.45/212.71 cnf(3, plain, [host(6 ^ []) = host(11 ^ [])], clausify(conj)).
% 220.45/212.71 cnf(4, plain, [-(_41122 = _41122)], theory(equality)).
% 220.45/212.71 cnf(5, plain, [-(elem(_42097, _42228)), elem(_42030, _42163), _42030 = _42097, _42163 = _42228], theory(equality)).
% 220.45/212.71 cnf(6, plain, [-(index(status, host(6 ^ [])) = elec_1)], clausify(conj)).
% 220.45/212.71 cnf(7, plain, [-(10 ^ [_109923, _109918, _109913]), 9 ^ [_109923, _109918, _109913] = host(_109918)], clausify(conj)).
% 220.45/212.71 cnf(8, plain, [-(elem(_65695, cons(_65754, _65812))), _65695 = _65754], clausify(axiom_46)).
% 220.45/212.71 cnf(9, plain, [-(_71869 = _71920), leq(_71869, _71920), leq(_71920, _71869)], clausify(axiom_61)).
% 220.45/212.71 cnf(10, plain, [-(_41554 = _41665), _41554 = _41610, _41610 = _41665], theory(equality)).
% 220.45/212.71 cnf(11, plain, [-(leq(_71559, _71604)), -(leq(_71604, _71559))], clausify(axiom_60)).
% 220.45/212.71 cnf(12, plain, [-(10 ^ [_109923, _109918, _109913]), leq(host(_109923), 9 ^ [_109923, _109918, _109913])], clausify(conj)).
% 220.45/212.71 cnf(13, plain, [leq(s(zero), _110083), -(leq(host(6 ^ []), _110083)), -(setIn(_110083, index(down, host(6 ^ [])))), -(_110083 = host(7 ^ []))], clausify(conj)).
% 220.45/212.71 cnf(14, plain, [index(status, host(_109913)) = norm, index(ldr, host(_109913)) = host(_109913), setIn(_109913, alive), 10 ^ [_109923, _109918, _109913], -(leq(host(_109923), host(_109913))), elem(m_Down(_109918), queue(host(_109923))), index(status, host(_109923)) = elec_1], clausify(conj)).
% 220.45/212.71 cnf(15, plain, [-(10 ^ [_109923, _109918, _109913]), setIn(9 ^ [_109923, _109918, _109913], index(down, host(_109923)))], clausify(conj)).
% 220.45/212.71 cnf(16, plain, [elem(_65695, cons(_65754, _65812)), -(_65695 = _65754), -(elem(_65695, _65812))], clausify(axiom_46)).
% 220.45/212.71 cnf(17, plain, [leq(_73082, s(_73137)), -(_73082 = s(_73137)), -(leq(_73082, _73137))], clausify(axiom_64)).
% 220.45/212.71 cnf(18, plain, [-(queue(host(6 ^ [])) = cons(m_Down(7 ^ []), 4 ^ []))], clausify(conj)).
% 220.45/212.71 cnf(19, plain, [-(setIn(11 ^ [], alive))], clausify(conj)).
% 220.45/212.71 cnf(20, plain, [-(index(ldr, host(11 ^ [])) = host(11 ^ []))], clausify(conj)).
% 220.45/212.71 cnf(21, plain, [-(10 ^ [_109923, _109918, _109913]), -(leq(s(zero), 9 ^ [_109923, _109918, _109913]))], clausify(conj)).
% 220.45/212.71 cnf(22, plain, [leq(s(host(6 ^ [])), host(11 ^ []))], clausify(conj)).
% 220.45/212.71 cnf(23, plain, [-(leq(_71920, _71869)), _71869 = _71920], clausify(axiom_61)).
% 220.45/212.71
% 220.45/212.71 cnf('1',plain,[index(status, host(11 ^ [])) = norm, index(ldr, host(11 ^ [])) = host(11 ^ []), setIn(11 ^ [], alive), 10 ^ [6 ^ [], 7 ^ [], 11 ^ []], -(leq(host(6 ^ []), host(11 ^ []))), elem(m_Down(7 ^ []), queue(host(6 ^ []))), index(status, host(6 ^ [])) = elec_1],start(14,bind([[_109913, _109918, _109923], [11 ^ [], 7 ^ [], 6 ^ []]]))).
% 220.45/212.71 cnf('1.1',plain,[-(index(status, host(11 ^ [])) = norm), norm = index(status, host(11 ^ []))],extension(1,bind([[_41275, _41320], [norm, index(status, host(11 ^ []))]]))).
% 220.45/212.71 cnf('1.1.1',plain,[-(norm = index(status, host(11 ^ []))), norm = index(status, host(11 ^ [])), index(status, host(11 ^ [])) = index(status, host(11 ^ []))],extension(10,bind([[_41554, _41610, _41665], [norm, index(status, host(11 ^ [])), index(status, host(11 ^ []))]]))).
% 220.45/212.71 cnf('1.1.1.1',plain,[-(norm = index(status, host(11 ^ []))), index(status, host(11 ^ [])) = norm],extension(1,bind([[_41275, _41320], [index(status, host(11 ^ [])), norm]]))).
% 220.45/212.71 cnf('1.1.1.1.1',plain,[-(index(status, host(11 ^ [])) = norm)],extension(2)).
% 220.45/212.71 cnf('1.1.1.2',plain,[-(index(status, host(11 ^ [])) = index(status, host(11 ^ [])))],extension(4,bind([[_41122], [index(status, host(11 ^ []))]]))).
% 220.45/212.71 cnf('1.2',plain,[-(index(ldr, host(11 ^ [])) = host(11 ^ [])), host(11 ^ []) = index(ldr, host(11 ^ []))],extension(1,bind([[_41275, _41320], [host(11 ^ []), index(ldr, host(11 ^ []))]]))).
% 220.45/212.71 cnf('1.2.1',plain,[-(host(11 ^ []) = index(ldr, host(11 ^ []))), host(11 ^ []) = index(ldr, host(11 ^ [])), index(ldr, host(11 ^ [])) = index(ldr, host(11 ^ []))],extension(10,bind([[_41554, _41610, _41665], [host(11 ^ []), index(ldr, host(11 ^ [])), index(ldr, host(11 ^ []))]]))).
% 220.45/212.71 cnf('1.2.1.1',plain,[-(host(11 ^ []) = index(ldr, host(11 ^ []))), index(ldr, host(11 ^ [])) = host(11 ^ [])],extension(1,bind([[_41275, _41320], [index(ldr, host(11 ^ [])), host(11 ^ [])]]))).
% 220.45/212.71 cnf('1.2.1.1.1',plain,[-(index(ldr, host(11 ^ [])) = host(11 ^ []))],extension(20)).
% 220.45/212.71 cnf('1.2.1.2',plain,[-(index(ldr, host(11 ^ [])) = index(ldr, host(11 ^ [])))],extension(4,bind([[_41122], [index(ldr, host(11 ^ []))]]))).
% 220.45/212.71 cnf('1.3',plain,[-(setIn(11 ^ [], alive))],extension(19)).
% 220.45/212.71 cnf('1.4',plain,[-(10 ^ [6 ^ [], 7 ^ [], 11 ^ []]), 9 ^ [6 ^ [], 7 ^ [], 11 ^ []] = host(7 ^ [])],extension(7,bind([[_109923, _109913, _109918], [6 ^ [], 11 ^ [], 7 ^ []]]))).
% 220.45/212.71 cnf('1.4.1',plain,[-(9 ^ [6 ^ [], 7 ^ [], 11 ^ []] = host(7 ^ [])), leq(s(zero), 9 ^ [6 ^ [], 7 ^ [], 11 ^ []]), -(leq(host(6 ^ []), 9 ^ [6 ^ [], 7 ^ [], 11 ^ []])), -(setIn(9 ^ [6 ^ [], 7 ^ [], 11 ^ []], index(down, host(6 ^ []))))],extension(13,bind([[_110083], [9 ^ [6 ^ [], 7 ^ [], 11 ^ []]]]))).
% 220.45/212.71 cnf('1.4.1.1',plain,[-(leq(s(zero), 9 ^ [6 ^ [], 7 ^ [], 11 ^ []])), -(10 ^ [6 ^ [], 7 ^ [], 11 ^ []])],extension(21,bind([[_109923, _109918, _109913], [6 ^ [], 7 ^ [], 11 ^ []]]))).
% 220.45/212.71 cnf('1.4.1.1.1',plain,[10 ^ [6 ^ [], 7 ^ [], 11 ^ []]],reduction('1')).
% 220.45/212.71 cnf('1.4.1.2',plain,[leq(host(6 ^ []), 9 ^ [6 ^ [], 7 ^ [], 11 ^ []]), -(10 ^ [6 ^ [], 7 ^ [], 11 ^ []])],extension(12,bind([[_109923, _109918, _109913], [6 ^ [], 7 ^ [], 11 ^ []]]))).
% 220.45/212.71 cnf('1.4.1.2.1',plain,[10 ^ [6 ^ [], 7 ^ [], 11 ^ []]],reduction('1')).
% 220.45/212.71 cnf('1.4.1.3',plain,[setIn(9 ^ [6 ^ [], 7 ^ [], 11 ^ []], index(down, host(6 ^ []))), -(10 ^ [6 ^ [], 7 ^ [], 11 ^ []])],extension(15,bind([[_109923, _109918, _109913], [6 ^ [], 7 ^ [], 11 ^ []]]))).
% 220.45/212.71 cnf('1.4.1.3.1',plain,[10 ^ [6 ^ [], 7 ^ [], 11 ^ []]],reduction('1')).
% 220.45/212.71 cnf('1.5',plain,[leq(host(6 ^ []), host(11 ^ [])), -(host(6 ^ []) = host(11 ^ [])), leq(host(11 ^ []), host(6 ^ []))],extension(9,bind([[_71920, _71869], [host(11 ^ []), host(6 ^ [])]]))).
% 220.45/212.71 cnf('1.5.1',plain,[host(6 ^ []) = host(11 ^ [])],extension(3)).
% 220.45/212.71 cnf('1.5.2',plain,[-(leq(host(11 ^ []), host(6 ^ []))), leq(host(11 ^ []), s(host(6 ^ []))), -(host(11 ^ []) = s(host(6 ^ [])))],extension(17,bind([[_73082, _73137], [host(11 ^ []), host(6 ^ [])]]))).
% 220.45/212.71 cnf('1.5.2.1',plain,[-(leq(host(11 ^ []), s(host(6 ^ [])))), -(leq(s(host(6 ^ [])), host(11 ^ [])))],extension(11,bind([[_71604, _71559], [s(host(6 ^ [])), host(11 ^ [])]]))).
% 220.45/212.71 cnf('1.5.2.1.1',plain,[leq(s(host(6 ^ [])), host(11 ^ []))],extension(22)).
% 220.45/212.71 cnf('1.5.2.2',plain,[host(11 ^ []) = s(host(6 ^ [])), -(leq(s(host(6 ^ [])), host(11 ^ [])))],extension(23,bind([[_71920, _71869], [s(host(6 ^ [])), host(11 ^ [])]]))).
% 220.45/212.71 cnf('1.5.2.2.1',plain,[leq(s(host(6 ^ [])), host(11 ^ []))],extension(22)).
% 220.45/212.71 cnf('1.6',plain,[-(elem(m_Down(7 ^ []), queue(host(6 ^ [])))), elem(m_Down(7 ^ []), cons(m_Down(7 ^ []), queue(host(6 ^ [])))), -(m_Down(7 ^ []) = m_Down(7 ^ []))],extension(16,bind([[_65812, _65695, _65754], [queue(host(6 ^ [])), m_Down(7 ^ []), m_Down(7 ^ [])]]))).
% 220.45/212.71 cnf('1.6.1',plain,[-(elem(m_Down(7 ^ []), cons(m_Down(7 ^ []), queue(host(6 ^ []))))), m_Down(7 ^ []) = m_Down(7 ^ [])],extension(8,bind([[_65812, _65695, _65754], [queue(host(6 ^ [])), m_Down(7 ^ []), m_Down(7 ^ [])]]))).
% 220.45/212.71 cnf('1.6.1.1',plain,[-(m_Down(7 ^ []) = m_Down(7 ^ []))],extension(4,bind([[_41122], [m_Down(7 ^ [])]]))).
% 220.45/212.71 cnf('1.6.2',plain,[m_Down(7 ^ []) = m_Down(7 ^ []), -(elem(m_Down(7 ^ []), queue(host(6 ^ [])))), elem(m_Down(7 ^ []), cons(m_Down(7 ^ []), 4 ^ [])), cons(m_Down(7 ^ []), 4 ^ []) = queue(host(6 ^ []))],extension(5,bind([[_42097, _42030, _42163, _42228], [m_Down(7 ^ []), m_Down(7 ^ []), cons(m_Down(7 ^ []), 4 ^ []), queue(host(6 ^ []))]]))).
% 220.45/212.71 cnf('1.6.2.1',plain,[elem(m_Down(7 ^ []), queue(host(6 ^ [])))],reduction('1')).
% 220.45/212.71 cnf('1.6.2.2',plain,[-(elem(m_Down(7 ^ []), cons(m_Down(7 ^ []), 4 ^ []))), m_Down(7 ^ []) = m_Down(7 ^ [])],extension(8,bind([[_65812, _65695, _65754], [4 ^ [], m_Down(7 ^ []), m_Down(7 ^ [])]]))).
% 220.45/212.71 cnf('1.6.2.2.1',plain,[-(m_Down(7 ^ []) = m_Down(7 ^ []))],extension(4,bind([[_41122], [m_Down(7 ^ [])]]))).
% 220.45/212.71 cnf('1.6.2.3',plain,[-(cons(m_Down(7 ^ []), 4 ^ []) = queue(host(6 ^ []))), queue(host(6 ^ [])) = cons(m_Down(7 ^ []), 4 ^ [])],extension(1,bind([[_41275, _41320], [queue(host(6 ^ [])), cons(m_Down(7 ^ []), 4 ^ [])]]))).
% 220.45/212.71 cnf('1.6.2.3.1',plain,[-(queue(host(6 ^ [])) = cons(m_Down(7 ^ []), 4 ^ []))],extension(18)).
% 220.45/212.71 cnf('1.7',plain,[-(index(status, host(6 ^ [])) = elec_1), elec_1 = index(status, host(6 ^ []))],extension(1,bind([[_41275, _41320], [elec_1, index(status, host(6 ^ []))]]))).
% 220.45/212.71 cnf('1.7.1',plain,[-(elec_1 = index(status, host(6 ^ []))), elec_1 = index(status, host(6 ^ [])), index(status, host(6 ^ [])) = index(status, host(6 ^ []))],extension(10,bind([[_41554, _41610, _41665], [elec_1, index(status, host(6 ^ [])), index(status, host(6 ^ []))]]))).
% 220.45/212.71 cnf('1.7.1.1',plain,[-(elec_1 = index(status, host(6 ^ []))), index(status, host(6 ^ [])) = elec_1],extension(1,bind([[_41275, _41320], [index(status, host(6 ^ [])), elec_1]]))).
% 220.45/212.71 cnf('1.7.1.1.1',plain,[-(index(status, host(6 ^ [])) = elec_1)],extension(6)).
% 220.45/212.71 cnf('1.7.1.2',plain,[-(index(status, host(6 ^ [])) = index(status, host(6 ^ [])))],extension(4,bind([[_41122], [index(status, host(6 ^ []))]]))).
% 220.45/212.71 %-----------------------------------------------------
% 220.45/212.72
% 220.45/212.72 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------