%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW392+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:09:04 PM UTC 2026
% Result : Theorem 0.98s 1.78s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW392+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n010.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 09:50:40 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.80/1.04 % Drodi V4.1.1
% 0.98/1.78 % Refutation found
% 0.98/1.78 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.98/1.78 % SZS output start CNFRefutation for theBenchmark
% 0.98/1.78 fof(f3,axiom,(
% 0.98/1.78 (! [V_Pa_2,V_Ga_2,T_b] : c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_b),V_Pa_2),c_Com_Ocom_OSKIP),V_Pa_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool)))) )),
% 0.98/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.98/1.78 fof(f17,axiom,(
% 0.98/1.78 (! [V_Qa_2,V_Q_H_2,V_c_2,V_Pa_2,V_Ga_2,T_b] :( c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_b),V_Pa_2),V_c_2),V_Q_H_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool))))=> ( (! [B_Z,B_s] :( hBOOL(hAPP(hAPP(V_Q_H_2,B_Z),B_s))=> hBOOL(hAPP(hAPP(V_Qa_2,B_Z),B_s)) ))=> c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_b),V_Pa_2),V_c_2),V_Qa_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool)))) ) ) )),
% 0.98/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.98/1.78 fof(f22,axiom,(
% 0.98/1.78 (! [V_x_2,V_A_2,V_y_2,T_b] :( hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(T_b),V_y_2),V_A_2),V_x_2))<=> ( V_y_2 = V_x_2| hBOOL(hAPP(V_A_2,V_x_2)) ) ) )),
% 0.98/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.98/1.78 fof(f1091,axiom,(
% 0.98/1.78 (! [V_com_H_2,V_fun_H_2,V_loc_H_2] : c_Com_Ocom_OSKIP != c_Com_Ocom_OLocal(V_loc_H_2,V_fun_H_2,V_com_H_2) )),
% 0.98/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.98/1.78 fof(f5223,hypothesis,(
% 0.98/1.78 (! [B_Z,B_s] :( hBOOL(hAPP(hAPP(v_P,B_Z),B_s))=> hBOOL(hAPP(hAPP(v_Q,B_Z),B_s)) ) )),
% 0.98/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.98/1.78 fof(f5224,conjecture,(
% 0.98/1.78 c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),c_Com_Ocom_OSKIP),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) ),
% 0.98/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.98/1.78 fof(f5225,negated_conjecture,(
% 0.98/1.78 ~(c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),c_Com_Ocom_OSKIP),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) )),
% 0.98/1.78 inference(negated_conjecture,[status(cth)],[f5224])).
% 0.98/1.78 fof(f5230,plain,(
% 0.98/1.78 ![X0,X1,X2]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X0),X2),c_Com_Ocom_OSKIP),X2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool)))))),
% 0.98/1.78 inference(cnf_transformation,[status(thm)],[f3])).
% 0.98/1.78 fof(f5266,plain,(
% 0.98/1.78 ![V_Qa_2,V_Q_H_2,V_c_2,V_Pa_2,V_Ga_2,T_b]: (~c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_b),V_Pa_2),V_c_2),V_Q_H_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool))))|((?[B_Z,B_s]: (hBOOL(hAPP(hAPP(V_Q_H_2,B_Z),B_s))&~hBOOL(hAPP(hAPP(V_Qa_2,B_Z),B_s))))|c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_b),V_Pa_2),V_c_2),V_Qa_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool))))))),
% 0.98/1.78 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.98/1.78 fof(f5267,plain,(
% 0.98/1.78 ![V_Q_H_2,V_c_2,V_Pa_2,V_Ga_2,T_b]: (~c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_b),V_Pa_2),V_c_2),V_Q_H_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool))))|(![V_Qa_2]: ((?[B_Z,B_s]: (hBOOL(hAPP(hAPP(V_Q_H_2,B_Z),B_s))&~hBOOL(hAPP(hAPP(V_Qa_2,B_Z),B_s))))|c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_b),V_Pa_2),V_c_2),V_Qa_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool)))))))),
% 0.98/1.78 inference(miniscoping,[status(thm)],[f5266])).
% 0.98/1.78 fof(f5268,plain,(
% 0.98/1.78 ![V_Q_H_2,V_c_2,V_Pa_2,V_Ga_2,T_b]: (~c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_b),V_Pa_2),V_c_2),V_Q_H_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool))))|(![V_Qa_2]: ((hBOOL(hAPP(hAPP(V_Q_H_2,sK1_skl(V_Qa_2,T_b,V_Ga_2,V_Pa_2,V_c_2,V_Q_H_2)),sK2_skl(V_Qa_2,T_b,V_Ga_2,V_Pa_2,V_c_2,V_Q_H_2)))&~hBOOL(hAPP(hAPP(V_Qa_2,sK1_skl(V_Qa_2,T_b,V_Ga_2,V_Pa_2,V_c_2,V_Q_H_2)),sK2_skl(V_Qa_2,T_b,V_Ga_2,V_Pa_2,V_c_2,V_Q_H_2))))|c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_b),V_Pa_2),V_c_2),V_Qa_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool)))))))),
% 0.98/1.78 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(B_Z,sK1_skl(V_Qa_2,T_b,V_Ga_2,V_Pa_2,V_c_2,V_Q_H_2)),skolemize(B_s,sK2_skl(V_Qa_2,T_b,V_Ga_2,V_Pa_2,V_c_2,V_Q_H_2))],[f5267])).
% 0.98/1.78 fof(f5269,plain,(
% 0.98/1.78 ![X0,X1,X2,X3,X4,X5]: (~c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X0),X2),X3),X4)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool))))|hBOOL(hAPP(hAPP(X4,sK1_skl(X5,X0,X1,X2,X3,X4)),sK2_skl(X5,X0,X1,X2,X3,X4)))|c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X0),X2),X3),X5)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool)))))),
% 0.98/1.78 inference(cnf_transformation,[status(thm)],[f5268])).
% 0.98/1.78 fof(f5270,plain,(
% 0.98/1.78 ![X0,X1,X2,X3,X4,X5]: (~c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X0),X2),X3),X4)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool))))|~hBOOL(hAPP(hAPP(X5,sK1_skl(X5,X0,X1,X2,X3,X4)),sK2_skl(X5,X0,X1,X2,X3,X4)))|c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X0),X2),X3),X5)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool)))))),
% 0.98/1.78 inference(cnf_transformation,[status(thm)],[f5268])).
% 0.98/1.78 fof(f5281,plain,(
% 0.98/1.78 ![V_x_2,V_A_2,V_y_2,T_b]: ((~hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(T_b),V_y_2),V_A_2),V_x_2))|(V_y_2=V_x_2|hBOOL(hAPP(V_A_2,V_x_2))))&(hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(T_b),V_y_2),V_A_2),V_x_2))|(~V_y_2=V_x_2&~hBOOL(hAPP(V_A_2,V_x_2)))))),
% 0.98/1.78 inference(NNF_transformation,[status(thm)],[f22])).
% 0.98/1.78 fof(f5282,plain,(
% 0.98/1.78 (![V_x_2,V_A_2,V_y_2]: ((![T_b]: ~hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(T_b),V_y_2),V_A_2),V_x_2)))|(V_y_2=V_x_2|hBOOL(hAPP(V_A_2,V_x_2)))))&(![V_x_2,V_A_2,V_y_2]: ((![T_b]: hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(T_b),V_y_2),V_A_2),V_x_2)))|(~V_y_2=V_x_2&~hBOOL(hAPP(V_A_2,V_x_2)))))),
% 0.98/1.78 inference(miniscoping,[status(thm)],[f5281])).
% 0.98/1.78 fof(f5283,plain,(
% 0.98/1.78 ![X0,X1,X2,X3]: (~hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(X0),X1),X2),X3))|X1=X3|hBOOL(hAPP(X2,X3)))),
% 0.98/1.78 inference(cnf_transformation,[status(thm)],[f5282])).
% 0.98/1.78 fof(f5285,plain,(
% 0.98/1.78 ![X0,X1,X2,X3]: (hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(X0),X1),X2),X3))|~hBOOL(hAPP(X2,X3)))),
% 0.98/1.78 inference(cnf_transformation,[status(thm)],[f5282])).
% 0.98/1.78 fof(f8768,plain,(
% 0.98/1.78 ![X0,X1,X2]: (~c_Com_Ocom_OSKIP=c_Com_Ocom_OLocal(X0,X1,X2))),
% 0.98/1.78 inference(cnf_transformation,[status(thm)],[f1091])).
% 0.98/1.78 fof(f20036,plain,(
% 0.98/1.78 ![B_Z,B_s]: (~hBOOL(hAPP(hAPP(v_P,B_Z),B_s))|hBOOL(hAPP(hAPP(v_Q,B_Z),B_s)))),
% 0.98/1.78 inference(pre_NNF_transformation,[status(thm)],[f5223])).
% 0.98/1.78 fof(f20037,plain,(
% 0.98/1.78 ![X0,X1]: (~hBOOL(hAPP(hAPP(v_P,X0),X1))|hBOOL(hAPP(hAPP(v_Q,X0),X1)))),
% 0.98/1.78 inference(cnf_transformation,[status(thm)],[f20036])).
% 0.98/1.78 fof(f20038,plain,(
% 0.98/1.78 ~c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),c_Com_Ocom_OSKIP),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))),
% 0.98/1.78 inference(cnf_transformation,[status(thm)],[f5225])).
% 0.98/1.78 fof(f20900,plain,(
% 0.98/1.78 ![X0,X1,X2,X3]: (hBOOL(hAPP(hAPP(X0,sK1_skl(X1,X2,X3,X0,c_Com_Ocom_OSKIP,X0)),sK2_skl(X1,X2,X3,X0,c_Com_Ocom_OSKIP,X0)))|c_Hoare__Mirabelle_Ohoare__derivs(X2,X3,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X2)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X2),X0),c_Com_Ocom_OSKIP),X1)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X2),tc_HOL_Obool)))))),
% 0.98/1.78 inference(resolution,[status(thm)],[f5269,f5230])).
% 0.98/1.78 fof(f20930,plain,(
% 0.98/1.78 ![X0,X1,X2,X3]: (~hBOOL(hAPP(hAPP(X0,sK1_skl(X0,X1,X2,X3,c_Com_Ocom_OSKIP,X3)),sK2_skl(X0,X1,X2,X3,c_Com_Ocom_OSKIP,X3)))|c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X1)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X1),X3),c_Com_Ocom_OSKIP),X0)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X1),tc_HOL_Obool)))))),
% 0.98/1.78 inference(resolution,[status(thm)],[f5270,f5230])).
% 0.98/1.78 fof(f21901,plain,(
% 0.98/1.78 hBOOL(hAPP(hAPP(v_P,sK1_skl(v_Q,t_a,v_G,v_P,c_Com_Ocom_OSKIP,v_P)),sK2_skl(v_Q,t_a,v_G,v_P,c_Com_Ocom_OSKIP,v_P)))),
% 0.98/1.78 inference(resolution,[status(thm)],[f20900,f20038])).
% 0.98/1.78 fof(f22046,plain,(
% 0.98/1.78 hBOOL(hAPP(hAPP(v_Q,sK1_skl(v_Q,t_a,v_G,v_P,c_Com_Ocom_OSKIP,v_P)),sK2_skl(v_Q,t_a,v_G,v_P,c_Com_Ocom_OSKIP,v_P)))),
% 0.98/1.78 inference(resolution,[status(thm)],[f21901,f20037])).
% 0.98/1.78 fof(f22050,plain,(
% 0.98/1.78 ![X0,X1]: (hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(X0),X1),hAPP(v_Q,sK1_skl(v_Q,t_a,v_G,v_P,c_Com_Ocom_OSKIP,v_P))),sK2_skl(v_Q,t_a,v_G,v_P,c_Com_Ocom_OSKIP,v_P))))),
% 0.98/1.78 inference(resolution,[status(thm)],[f22046,f5285])).
% 0.98/1.78 fof(f22178,definition,(
% 0.98/1.78 ![X0]: (sQ25_spl <=> (X0=sK2_skl(v_Q,t_a,v_G,v_P,c_Com_Ocom_OSKIP,v_P)))),
% 0.98/1.78 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.98/1.78 fof(f22179,plain,(
% 0.98/1.78 ![X0]: (X0=sK2_skl(v_Q,t_a,v_G,v_P,c_Com_Ocom_OSKIP,v_P)|~sQ25_spl)),
% 0.98/1.78 inference(component_clause,[status(thm)],[f22178])).
% 0.98/1.78 fof(f22186,plain,(
% 0.98/1.78 ![X0,X1]: (X0=X1|~sQ25_spl)),
% 0.98/1.78 inference(paramodulation,[status(thm)],[f22179,f22179])).
% 0.98/1.78 fof(f22195,definition,(
% 0.98/1.78 sQ28_spl <=> (c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),c_Com_Ocom_OSKIP),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))))),
% 0.98/1.78 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.98/1.78 fof(f22196,plain,(
% 0.98/1.78 c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),c_Com_Ocom_OSKIP),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))|~sQ28_spl),
% 0.98/1.78 inference(component_clause,[status(thm)],[f22195])).
% 0.98/1.78 fof(f22199,plain,(
% 0.98/1.78 $false|~sQ28_spl),
% 0.98/1.78 inference(forward_subsumption_resolution,[status(thm)],[f22196,f20038])).
% 0.98/1.78 fof(f22200,plain,(
% 0.98/1.78 ~sQ28_spl),
% 0.98/1.78 inference(contradiction_clause,[status(thm)],[f22199])).
% 0.98/1.78 fof(f22345,plain,(
% 0.98/1.78 ![X0]: (X0=sK2_skl(v_Q,t_a,v_G,v_P,c_Com_Ocom_OSKIP,v_P)|hBOOL(hAPP(hAPP(v_Q,sK1_skl(v_Q,t_a,v_G,v_P,c_Com_Ocom_OSKIP,v_P)),sK2_skl(v_Q,t_a,v_G,v_P,c_Com_Ocom_OSKIP,v_P))))),
% 0.98/1.78 inference(resolution,[status(thm)],[f22050,f5283])).
% 0.98/1.78 fof(f22348,definition,(
% 0.98/1.78 sQ29_spl <=> (hBOOL(hAPP(hAPP(v_Q,sK1_skl(v_Q,t_a,v_G,v_P,c_Com_Ocom_OSKIP,v_P)),sK2_skl(v_Q,t_a,v_G,v_P,c_Com_Ocom_OSKIP,v_P))))),
% 0.98/1.78 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.98/1.78 fof(f22349,plain,(
% 0.98/1.78 hBOOL(hAPP(hAPP(v_Q,sK1_skl(v_Q,t_a,v_G,v_P,c_Com_Ocom_OSKIP,v_P)),sK2_skl(v_Q,t_a,v_G,v_P,c_Com_Ocom_OSKIP,v_P)))|~sQ29_spl),
% 1.01/1.85 inference(component_clause,[status(thm)],[f22348])).
% 1.01/1.85 fof(f22351,plain,(
% 1.01/1.85 sQ25_spl|sQ29_spl),
% 1.01/1.85 inference(split_clause,[status(thm)],[f22345,f22178,f22348])).
% 1.01/1.85 fof(f22352,plain,(
% 1.01/1.85 $false|~sQ25_spl),
% 1.01/1.85 inference(backward_subsumption_resolution,[status(thm)],[f8768,f22186])).
% 1.01/1.85 fof(f22359,plain,(
% 1.01/1.85 ~sQ25_spl),
% 1.01/1.85 inference(contradiction_clause,[status(thm)],[f22352])).
% 1.01/1.85 fof(f23385,plain,(
% 1.01/1.85 c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),c_Com_Ocom_OSKIP),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))|~sQ29_spl),
% 1.01/1.85 inference(resolution,[status(thm)],[f20930,f22349])).
% 1.01/1.85 fof(f23392,plain,(
% 1.01/1.85 sQ28_spl|~sQ29_spl),
% 1.01/1.85 inference(split_clause,[status(thm)],[f23385,f22195,f22348])).
% 1.01/1.85 fof(f23394,plain,(
% 1.01/1.85 $false),
% 1.01/1.85 inference(sat_refutation,[status(thm)],[f22200,f22351,f22359,f23392])).
% 1.01/1.85 % SZS output end CNFRefutation for theBenchmark.p
% 1.01/1.88 % Elapsed time: 1.508414 seconds
% 1.01/1.88 % CPU time: 6.649916 seconds
% 1.01/1.88 % Total memory used: 706.643 MB
% 1.01/1.88 % Net memory used: 699.648 MB
%------------------------------------------------------------------------------