%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWW386+1 : TPTP v8.1.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n032.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:22 EDT 2022
% Result : Theorem 31.51s 31.41s
% Output : Proof 31.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : SWW386+1 : TPTP v8.1.0. Released v5.2.0.
% 0.10/0.11 % Command : leancop_casc.sh %s %d
% 0.11/0.31 % Computer : n032.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 600
% 0.11/0.31 % DateTime : Sat Jun 4 09:33:47 EDT 2022
% 0.16/0.31 % CPUTime :
% 31.51/31.41 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.51/31.41 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.51/31.42
% 31.51/31.42 %-----------------------------------------------------
% 31.51/31.42 fof(conj_4, conjecture, c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate, c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate), tc_HOL_Obool)), hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)), hAPP(c_Hoare__Mirabelle_OMGT, hAPP(c_Com_Ocom_OBODY, v_pn))), c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate), tc_HOL_Obool)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', conj_4)).
% 31.51/31.42 fof(fact_MGF, axiom, ! [_1727864] : (c_Hoare__Mirabelle_Ostate__not__singleton => c_Com_OWT__bodies => hBOOL(hAPP(c_Com_OWT, _1727864)) => c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate, c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate), tc_HOL_Obool)), hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)), hAPP(c_Hoare__Mirabelle_OMGT, _1727864)), c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate), tc_HOL_Obool))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', fact_MGF)).
% 31.51/31.42 fof(fact_WT_Oequations_I7_J, axiom, ! [_1728178] : (hBOOL(hAPP(c_Com_OWT, hAPP(c_Com_Ocom_OBODY, _1728178))) <=> ? [_1728207] : hAPP(c_Com_Obody, _1728178) = hAPP(c_Option_Ooption_OSome(tc_Com_Ocom), _1728207)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', fact_WT_Oequations_I7_J)).
% 31.51/31.42 fof(conj_0, hypothesis, c_Hoare__Mirabelle_Ostate__not__singleton, file('/export/starexec/sandbox/benchmark/theBenchmark.p', conj_0)).
% 31.51/31.42 fof(conj_1, hypothesis, c_Com_OWT__bodies, file('/export/starexec/sandbox/benchmark/theBenchmark.p', conj_1)).
% 31.51/31.42 fof(conj_3, hypothesis, hAPP(c_Com_Obody, v_pn) = hAPP(c_Option_Ooption_OSome(tc_Com_Ocom), v_y), file('/export/starexec/sandbox/benchmark/theBenchmark.p', conj_3)).
% 31.51/31.42
% 31.51/31.42 cnf(1, plain, [c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate, c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate), tc_HOL_Obool)), hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)), hAPP(c_Hoare__Mirabelle_OMGT, hAPP(c_Com_Ocom_OBODY, v_pn))), c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate), tc_HOL_Obool))))], clausify(conj_4)).
% 31.51/31.42 cnf(2, plain, [c_Hoare__Mirabelle_Ostate__not__singleton, c_Com_OWT__bodies, hBOOL(hAPP(c_Com_OWT, _453069)), -(c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate, c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate), tc_HOL_Obool)), hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)), hAPP(c_Hoare__Mirabelle_OMGT, _453069)), c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate), tc_HOL_Obool)))))], clausify(fact_MGF)).
% 31.51/31.42 cnf(3, plain, [-(hBOOL(hAPP(c_Com_OWT, hAPP(c_Com_Ocom_OBODY, _453364)))), hAPP(c_Com_Obody, _453364) = hAPP(c_Option_Ooption_OSome(tc_Com_Ocom), _453373)], clausify(fact_WT_Oequations_I7_J)).
% 31.51/31.42 cnf(4, plain, [-(c_Hoare__Mirabelle_Ostate__not__singleton)], clausify(conj_0)).
% 31.51/31.42 cnf(5, plain, [-(c_Com_OWT__bodies)], clausify(conj_1)).
% 31.51/31.42 cnf(6, plain, [-(hAPP(c_Com_Obody, v_pn) = hAPP(c_Option_Ooption_OSome(tc_Com_Ocom), v_y))], clausify(conj_3)).
% 31.51/31.42
% 31.51/31.42 cnf('1',plain,[c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate, c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate), tc_HOL_Obool)), hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)), hAPP(c_Hoare__Mirabelle_OMGT, hAPP(c_Com_Ocom_OBODY, v_pn))), c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate), tc_HOL_Obool))))],start(1)).
% 31.51/31.42 cnf('1.1',plain,[-(c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate, c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate), tc_HOL_Obool)), hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)), hAPP(c_Hoare__Mirabelle_OMGT, hAPP(c_Com_Ocom_OBODY, v_pn))), c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate), tc_HOL_Obool))))), c_Hoare__Mirabelle_Ostate__not__singleton, c_Com_OWT__bodies, hBOOL(hAPP(c_Com_OWT, hAPP(c_Com_Ocom_OBODY, v_pn)))],extension(2,bind([[_453069], [hAPP(c_Com_Ocom_OBODY, v_pn)]]))).
% 31.51/31.42 cnf('1.1.1',plain,[-(c_Hoare__Mirabelle_Ostate__not__singleton)],extension(4)).
% 31.51/31.42 cnf('1.1.2',plain,[-(c_Com_OWT__bodies)],extension(5)).
% 31.51/31.42 cnf('1.1.3',plain,[-(hBOOL(hAPP(c_Com_OWT, hAPP(c_Com_Ocom_OBODY, v_pn)))), hAPP(c_Com_Obody, v_pn) = hAPP(c_Option_Ooption_OSome(tc_Com_Ocom), v_y)],extension(3,bind([[_453364, _453373], [v_pn, v_y]]))).
% 31.51/31.42 cnf('1.1.3.1',plain,[-(hAPP(c_Com_Obody, v_pn) = hAPP(c_Option_Ooption_OSome(tc_Com_Ocom), v_y))],extension(6)).
% 31.51/31.42 %-----------------------------------------------------
% 31.51/31.42
% 31.51/31.42 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------