%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWW473+7 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.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 : 600s
% DateTime : Thu Jul 21 00:47:35 EDT 2022
% Result : Theorem 4.78s 5.57s
% Output : Proof 4.78s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWW473+7 : TPTP v8.1.0. Released v5.3.0.
% 0.07/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n028.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Mon Jun 6 02:34:28 EDT 2022
% 0.12/0.34 % CPUTime :
% 4.78/5.57 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.78/5.57 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.78/5.58
% 4.78/5.58 %-----------------------------------------------------
% 4.78/5.58 fof(conj_6, conjecture, hBOOL(hAPP(fun(x_a, bool), bool, hAPP(fun(x_a, bool), fun(fun(x_a, bool), bool), ord_less_eq(fun(x_a, bool)), hAPP(fun(x_a, bool), fun(x_a, bool), hAPP(x_a, fun(fun(x_a, bool), fun(x_a, bool)), insert(x_a), hAPP(pname, x_a, mgt_call, pn)), g)), hAPP(fun(pname, bool), fun(x_a, bool), hAPP(fun(pname, x_a), fun(fun(pname, bool), fun(x_a, bool)), image(pname, x_a), mgt_call), u))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', conj_6)).
% 4.78/5.58 fof(fact_94_imageI, axiom, ! [_645670, _645673, _645676, _645679, _645682] : (hBOOL(hAPP(fun(_645673, bool), bool, hAPP(_645673, fun(fun(_645673, bool), bool), member(_645673), _645679), _645682)) => hBOOL(hAPP(fun(_645670, bool), bool, hAPP(_645670, fun(fun(_645670, bool), bool), member(_645670), hAPP(_645673, _645670, _645676, _645679)), hAPP(fun(_645673, bool), fun(_645670, bool), hAPP(fun(_645673, _645670), fun(fun(_645673, bool), fun(_645670, bool)), image(_645673, _645670), _645676), _645682)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fact_94_imageI)).
% 4.78/5.58 fof(fact_103_insert__subset, axiom, ! [_646282, _646285, _646288, _646291] : (hBOOL(hAPP(fun(_646282, bool), bool, hAPP(fun(_646282, bool), fun(fun(_646282, bool), bool), ord_less_eq(fun(_646282, bool)), hAPP(fun(_646282, bool), fun(_646282, bool), hAPP(_646282, fun(fun(_646282, bool), fun(_646282, bool)), insert(_646282), _646285), _646288)), _646291)) <=> hBOOL(hAPP(fun(_646282, bool), bool, hAPP(_646282, fun(fun(_646282, bool), bool), member(_646282), _646285), _646291)) & hBOOL(hAPP(fun(_646282, bool), bool, hAPP(fun(_646282, bool), fun(fun(_646282, bool), bool), ord_less_eq(fun(_646282, bool)), _646288), _646291))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fact_103_insert__subset)).
% 4.78/5.58 fof(conj_1, hypothesis, hBOOL(hAPP(fun(x_a, bool), bool, hAPP(fun(x_a, bool), fun(fun(x_a, bool), bool), ord_less_eq(fun(x_a, bool)), g), hAPP(fun(pname, bool), fun(x_a, bool), hAPP(fun(pname, x_a), fun(fun(pname, bool), fun(x_a, bool)), image(pname, x_a), mgt_call), u))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', conj_1)).
% 4.78/5.58 fof(conj_4, hypothesis, hBOOL(hAPP(fun(pname, bool), bool, hAPP(pname, fun(fun(pname, bool), bool), member(pname), pn), u)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', conj_4)).
% 4.78/5.58
% 4.78/5.58 cnf(1, plain, [hBOOL(hAPP(fun(x_a, bool), bool, hAPP(fun(x_a, bool), fun(fun(x_a, bool), bool), ord_less_eq(fun(x_a, bool)), hAPP(fun(x_a, bool), fun(x_a, bool), hAPP(x_a, fun(fun(x_a, bool), fun(x_a, bool)), insert(x_a), hAPP(pname, x_a, mgt_call, pn)), g)), hAPP(fun(pname, bool), fun(x_a, bool), hAPP(fun(pname, x_a), fun(fun(pname, bool), fun(x_a, bool)), image(pname, x_a), mgt_call), u)))], clausify(conj_6)).
% 4.78/5.58 cnf(2, plain, [hBOOL(hAPP(fun(_127315, bool), bool, hAPP(_127315, fun(fun(_127315, bool), bool), member(_127315), _127317), _127318)), -(hBOOL(hAPP(fun(_127314, bool), bool, hAPP(_127314, fun(fun(_127314, bool), bool), member(_127314), hAPP(_127315, _127314, _127316, _127317)), hAPP(fun(_127315, bool), fun(_127314, bool), hAPP(fun(_127315, _127314), fun(fun(_127315, bool), fun(_127314, bool)), image(_127315, _127314), _127316), _127318))))], clausify(fact_94_imageI)).
% 4.78/5.58 cnf(3, plain, [-(hBOOL(hAPP(fun(_128491, bool), bool, hAPP(fun(_128491, bool), fun(fun(_128491, bool), bool), ord_less_eq(fun(_128491, bool)), hAPP(fun(_128491, bool), fun(_128491, bool), hAPP(_128491, fun(fun(_128491, bool), fun(_128491, bool)), insert(_128491), _128492), _128493)), _128494))), hBOOL(hAPP(fun(_128491, bool), bool, hAPP(_128491, fun(fun(_128491, bool), bool), member(_128491), _128492), _128494)), hBOOL(hAPP(fun(_128491, bool), bool, hAPP(fun(_128491, bool), fun(fun(_128491, bool), bool), ord_less_eq(fun(_128491, bool)), _128493), _128494))], clausify(fact_103_insert__subset)).
% 4.78/5.58 cnf(4, plain, [-(hBOOL(hAPP(fun(x_a, bool), bool, hAPP(fun(x_a, bool), fun(fun(x_a, bool), bool), ord_less_eq(fun(x_a, bool)), g), hAPP(fun(pname, bool), fun(x_a, bool), hAPP(fun(pname, x_a), fun(fun(pname, bool), fun(x_a, bool)), image(pname, x_a), mgt_call), u))))], clausify(conj_1)).
% 4.78/5.58 cnf(5, plain, [-(hBOOL(hAPP(fun(pname, bool), bool, hAPP(pname, fun(fun(pname, bool), bool), member(pname), pn), u)))], clausify(conj_4)).
% 4.78/5.58
% 4.78/5.58 cnf('1',plain,[hBOOL(hAPP(fun(x_a, bool), bool, hAPP(fun(x_a, bool), fun(fun(x_a, bool), bool), ord_less_eq(fun(x_a, bool)), hAPP(fun(x_a, bool), fun(x_a, bool), hAPP(x_a, fun(fun(x_a, bool), fun(x_a, bool)), insert(x_a), hAPP(pname, x_a, mgt_call, pn)), g)), hAPP(fun(pname, bool), fun(x_a, bool), hAPP(fun(pname, x_a), fun(fun(pname, bool), fun(x_a, bool)), image(pname, x_a), mgt_call), u)))],start(1)).
% 4.78/5.58 cnf('1.1',plain,[-(hBOOL(hAPP(fun(x_a, bool), bool, hAPP(fun(x_a, bool), fun(fun(x_a, bool), bool), ord_less_eq(fun(x_a, bool)), hAPP(fun(x_a, bool), fun(x_a, bool), hAPP(x_a, fun(fun(x_a, bool), fun(x_a, bool)), insert(x_a), hAPP(pname, x_a, mgt_call, pn)), g)), hAPP(fun(pname, bool), fun(x_a, bool), hAPP(fun(pname, x_a), fun(fun(pname, bool), fun(x_a, bool)), image(pname, x_a), mgt_call), u)))), hBOOL(hAPP(fun(x_a, bool), bool, hAPP(x_a, fun(fun(x_a, bool), bool), member(x_a), hAPP(pname, x_a, mgt_call, pn)), hAPP(fun(pname, bool), fun(x_a, bool), hAPP(fun(pname, x_a), fun(fun(pname, bool), fun(x_a, bool)), image(pname, x_a), mgt_call), u))), hBOOL(hAPP(fun(x_a, bool), bool, hAPP(fun(x_a, bool), fun(fun(x_a, bool), bool), ord_less_eq(fun(x_a, bool)), g), hAPP(fun(pname, bool), fun(x_a, bool), hAPP(fun(pname, x_a), fun(fun(pname, bool), fun(x_a, bool)), image(pname, x_a), mgt_call), u)))],extension(3,bind([[_128492, _128491, _128493, _128494], [hAPP(pname, x_a, mgt_call, pn), x_a, g, hAPP(fun(pname, bool), fun(x_a, bool), hAPP(fun(pname, x_a), fun(fun(pname, bool), fun(x_a, bool)), image(pname, x_a), mgt_call), u)]]))).
% 4.78/5.58 cnf('1.1.1',plain,[-(hBOOL(hAPP(fun(x_a, bool), bool, hAPP(x_a, fun(fun(x_a, bool), bool), member(x_a), hAPP(pname, x_a, mgt_call, pn)), hAPP(fun(pname, bool), fun(x_a, bool), hAPP(fun(pname, x_a), fun(fun(pname, bool), fun(x_a, bool)), image(pname, x_a), mgt_call), u)))), hBOOL(hAPP(fun(pname, bool), bool, hAPP(pname, fun(fun(pname, bool), bool), member(pname), pn), u))],extension(2,bind([[_127314, _127316, _127315, _127317, _127318], [x_a, mgt_call, pname, pn, u]]))).
% 4.78/5.58 cnf('1.1.1.1',plain,[-(hBOOL(hAPP(fun(pname, bool), bool, hAPP(pname, fun(fun(pname, bool), bool), member(pname), pn), u)))],extension(5)).
% 4.78/5.58 cnf('1.1.2',plain,[-(hBOOL(hAPP(fun(x_a, bool), bool, hAPP(fun(x_a, bool), fun(fun(x_a, bool), bool), ord_less_eq(fun(x_a, bool)), g), hAPP(fun(pname, bool), fun(x_a, bool), hAPP(fun(pname, x_a), fun(fun(pname, bool), fun(x_a, bool)), image(pname, x_a), mgt_call), u))))],extension(4)).
% 4.78/5.58 %-----------------------------------------------------
% 4.78/5.58
% 4.78/5.59 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------