%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW353+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 : n009.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:01 PM UTC 2026
% Result : Theorem 214.03s 28.14s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW353+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.09/0.36 % Computer : n009.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 09:48:58 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.77/1.07 % Drodi V4.1.1
% 214.03/28.14 % Refutation found
% 214.03/28.14 % SZS status Theorem for theBenchmark: Theorem is valid
% 214.03/28.14 % SZS output start CNFRefutation for theBenchmark
% 214.03/28.14 fof(f9,axiom,(
% 214.03/28.14 (! [V_A_2,V_a_2,T_a] : c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool)) != hAPP(hAPP(c_Set_Oinsert(T_a),V_a_2),V_A_2) )),
% 214.03/28.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.03/28.14 fof(f14,axiom,(
% 214.03/28.14 (! [V_x_2,T_a] : c_Option_Oset(T_a,hAPP(c_Option_Ooption_OSome(T_a),V_x_2)) = hAPP(hAPP(c_Set_Oinsert(T_a),V_x_2),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))) )),
% 214.03/28.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.03/28.14 fof(f124,axiom,(
% 214.03/28.14 (! [T_a,V_x_2] :( V_x_2 != c_Option_Ooption_ONone(T_a)<=> (? [B_y] : V_x_2 = hAPP(c_Option_Ooption_OSome(T_a),B_y) )) )),
% 214.03/28.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.03/28.14 fof(f159,axiom,(
% 214.03/28.14 (! [V_a_2,T_a] : ~ hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool)))) )),
% 214.03/28.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.03/28.14 fof(f160,axiom,(
% 214.03/28.14 (! [V_A_2,V_b_2,V_a_2,T_a] :( hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),hAPP(hAPP(c_Set_Oinsert(T_a),V_b_2),V_A_2)))=> ( V_a_2 != V_b_2=> hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),V_A_2)) ) ) )),
% 214.03/28.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.03/28.14 fof(f167,axiom,(
% 214.03/28.14 (! [V_B_2,V_A_2,V_ca_2,T_a] :( hBOOL(hAPP(hAPP(c_member(T_a),V_ca_2),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_fun(T_a,tc_HOL_Obool)),V_A_2),V_B_2)))=> ~ ( hBOOL(hAPP(hAPP(c_member(T_a),V_ca_2),V_A_2))=> hBOOL(hAPP(hAPP(c_member(T_a),V_ca_2),V_B_2)) ) ) )),
% 214.03/28.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.03/28.14 fof(f243,axiom,(
% 214.03/28.14 (! [V_A_2,V_x_2,T_a] :( ~ hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2))=> hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_fun(T_a,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(T_a),V_x_2),V_A_2)),hAPP(hAPP(c_Set_Oinsert(T_a),V_x_2),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool)))) = V_A_2 ) )),
% 214.03/28.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.03/28.14 fof(f258,axiom,(
% 214.03/28.14 (! [V_A_2,T_a] :( (? [B_x] : hBOOL(hAPP(hAPP(c_member(T_a),B_x),V_A_2)))<=> V_A_2 != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool)) ) )),
% 214.03/28.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.03/28.14 fof(f300,axiom,(
% 214.03/28.14 (! [V_m_2,T_b,V_a_2,T_a] :( hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),c_Map_Odom(T_a,T_b,V_m_2)))<=> hAPP(V_m_2,V_a_2) != c_Option_Ooption_ONone(T_b) ) )),
% 214.03/28.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.03/28.14 fof(f5243,hypothesis,(
% 214.03/28.14 (! [B_x] :( hBOOL(hAPP(hAPP(c_member(tc_Com_Opname),B_x),c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody)))=> c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Hoare__Mirabelle_OMGT(hAPP(c_Com_Ocom_OBODY,B_x))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_HOL_Obool)))) ) )),
% 214.03/28.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.03/28.14 fof(f5244,hypothesis,(
% 214.03/28.14 hAPP(c_Com_Obody,v_pname) = hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),v_y) ),
% 214.03/28.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.03/28.14 fof(f5245,conjecture,(
% 214.03/28.14 c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Hoare__Mirabelle_OMGT(hAPP(c_Com_Ocom_OBODY,v_pname))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_HOL_Obool)))) ),
% 214.03/28.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.03/28.14 fof(f5246,negated_conjecture,(
% 214.03/28.14 ~(c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Hoare__Mirabelle_OMGT(hAPP(c_Com_Ocom_OBODY,v_pname))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_HOL_Obool)))) )),
% 214.03/28.14 inference(negated_conjecture,[status(cth)],[f5245])).
% 214.03/28.14 fof(f5267,plain,(
% 214.03/28.14 ![X0,X1,X2]: (~c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool))=hAPP(hAPP(c_Set_Oinsert(X0),X1),X2))),
% 214.03/28.14 inference(cnf_transformation,[status(thm)],[f9])).
% 214.03/28.14 fof(f5283,plain,(
% 214.03/28.14 ![X0,X1]: (c_Option_Oset(X0,hAPP(c_Option_Ooption_OSome(X0),X1))=hAPP(hAPP(c_Set_Oinsert(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool))))),
% 214.03/28.14 inference(cnf_transformation,[status(thm)],[f14])).
% 214.03/28.14 fof(f5576,plain,(
% 214.03/28.14 ![T_a,V_x_2]: ((V_x_2=c_Option_Ooption_ONone(T_a)|(?[B_y]: V_x_2=hAPP(c_Option_Ooption_OSome(T_a),B_y)))&(~V_x_2=c_Option_Ooption_ONone(T_a)|(![B_y]: ~V_x_2=hAPP(c_Option_Ooption_OSome(T_a),B_y))))),
% 214.03/28.14 inference(NNF_transformation,[status(thm)],[f124])).
% 214.03/28.14 fof(f5577,plain,(
% 214.03/28.14 (![T_a,V_x_2]: (V_x_2=c_Option_Ooption_ONone(T_a)|(?[B_y]: V_x_2=hAPP(c_Option_Ooption_OSome(T_a),B_y))))&(![T_a,V_x_2]: (~V_x_2=c_Option_Ooption_ONone(T_a)|(![B_y]: ~V_x_2=hAPP(c_Option_Ooption_OSome(T_a),B_y))))),
% 214.03/28.14 inference(miniscoping,[status(thm)],[f5576])).
% 214.03/28.14 fof(f5578,plain,(
% 214.03/28.14 (![T_a,V_x_2]: (V_x_2=c_Option_Ooption_ONone(T_a)|V_x_2=hAPP(c_Option_Ooption_OSome(T_a),sK15_skl(V_x_2,T_a))))&(![T_a,V_x_2]: (~V_x_2=c_Option_Ooption_ONone(T_a)|(![B_y]: ~V_x_2=hAPP(c_Option_Ooption_OSome(T_a),B_y))))),
% 214.03/28.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(B_y,sK15_skl(V_x_2,T_a))],[f5577])).
% 214.03/28.14 fof(f5580,plain,(
% 214.03/28.14 ![X0,X1,X2]: (~X0=c_Option_Ooption_ONone(X1)|~X0=hAPP(c_Option_Ooption_OSome(X1),X2))),
% 214.03/28.14 inference(cnf_transformation,[status(thm)],[f5578])).
% 214.03/28.14 fof(f5672,plain,(
% 214.03/28.14 ![X0,X1]: (~hBOOL(hAPP(hAPP(c_member(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)))))),
% 214.03/28.14 inference(cnf_transformation,[status(thm)],[f159])).
% 214.03/28.14 fof(f5673,plain,(
% 214.03/28.14 ![V_A_2,V_b_2,V_a_2,T_a]: (~hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),hAPP(hAPP(c_Set_Oinsert(T_a),V_b_2),V_A_2)))|(V_a_2=V_b_2|hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),V_A_2))))),
% 214.03/28.14 inference(pre_NNF_transformation,[status(thm)],[f160])).
% 214.03/28.14 fof(f5674,plain,(
% 214.03/28.14 ![X0,X1,X2,X3]: (~hBOOL(hAPP(hAPP(c_member(X0),X1),hAPP(hAPP(c_Set_Oinsert(X0),X2),X3)))|X1=X2|hBOOL(hAPP(hAPP(c_member(X0),X1),X3)))),
% 214.03/28.14 inference(cnf_transformation,[status(thm)],[f5673])).
% 214.03/28.14 fof(f5690,plain,(
% 214.03/28.14 ![V_B_2,V_A_2,V_ca_2,T_a]: (~hBOOL(hAPP(hAPP(c_member(T_a),V_ca_2),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_fun(T_a,tc_HOL_Obool)),V_A_2),V_B_2)))|(hBOOL(hAPP(hAPP(c_member(T_a),V_ca_2),V_A_2))&~hBOOL(hAPP(hAPP(c_member(T_a),V_ca_2),V_B_2))))),
% 214.03/28.14 inference(pre_NNF_transformation,[status(thm)],[f167])).
% 214.03/28.14 fof(f5692,plain,(
% 214.03/28.14 ![X0,X1,X2,X3]: (~hBOOL(hAPP(hAPP(c_member(X0),X1),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_fun(X0,tc_HOL_Obool)),X2),X3)))|~hBOOL(hAPP(hAPP(c_member(X0),X1),X3)))),
% 214.03/28.14 inference(cnf_transformation,[status(thm)],[f5690])).
% 214.03/28.14 fof(f5932,plain,(
% 214.03/28.14 ![V_A_2,V_x_2,T_a]: (hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2))|hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_fun(T_a,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(T_a),V_x_2),V_A_2)),hAPP(hAPP(c_Set_Oinsert(T_a),V_x_2),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))))=V_A_2)),
% 214.03/28.14 inference(pre_NNF_transformation,[status(thm)],[f243])).
% 214.03/28.14 fof(f5933,plain,(
% 214.03/28.14 ![X0,X1,X2]: (hBOOL(hAPP(hAPP(c_member(X0),X1),X2))|hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_fun(X0,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(X0),X1),X2)),hAPP(hAPP(c_Set_Oinsert(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool))))=X2)),
% 214.03/28.14 inference(cnf_transformation,[status(thm)],[f5932])).
% 214.03/28.14 fof(f5969,plain,(
% 214.03/28.14 ![V_A_2,T_a]: (((![B_x]: ~hBOOL(hAPP(hAPP(c_member(T_a),B_x),V_A_2)))|~V_A_2=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool)))&((?[B_x]: hBOOL(hAPP(hAPP(c_member(T_a),B_x),V_A_2)))|V_A_2=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))))),
% 214.03/28.14 inference(NNF_transformation,[status(thm)],[f258])).
% 214.03/28.14 fof(f5970,plain,(
% 214.03/28.14 (![V_A_2,T_a]: ((![B_x]: ~hBOOL(hAPP(hAPP(c_member(T_a),B_x),V_A_2)))|~V_A_2=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))))&(![V_A_2,T_a]: ((?[B_x]: hBOOL(hAPP(hAPP(c_member(T_a),B_x),V_A_2)))|V_A_2=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))))),
% 214.03/28.14 inference(miniscoping,[status(thm)],[f5969])).
% 214.03/28.14 fof(f5971,plain,(
% 214.03/28.14 (![V_A_2,T_a]: ((![B_x]: ~hBOOL(hAPP(hAPP(c_member(T_a),B_x),V_A_2)))|~V_A_2=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))))&(![V_A_2,T_a]: (hBOOL(hAPP(hAPP(c_member(T_a),sK26_skl(T_a,V_A_2)),V_A_2))|V_A_2=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))))),
% 214.03/28.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(B_x,sK26_skl(T_a,V_A_2))],[f5970])).
% 214.03/28.14 fof(f5973,plain,(
% 214.03/28.14 ![X0,X1]: (hBOOL(hAPP(hAPP(c_member(X0),sK26_skl(X0,X1)),X1))|X1=c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)))),
% 214.03/28.14 inference(cnf_transformation,[status(thm)],[f5971])).
% 214.03/28.14 fof(f6079,plain,(
% 214.03/28.14 ![V_m_2,T_b,V_a_2,T_a]: ((~hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),c_Map_Odom(T_a,T_b,V_m_2)))|~hAPP(V_m_2,V_a_2)=c_Option_Ooption_ONone(T_b))&(hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),c_Map_Odom(T_a,T_b,V_m_2)))|hAPP(V_m_2,V_a_2)=c_Option_Ooption_ONone(T_b)))),
% 214.03/28.14 inference(NNF_transformation,[status(thm)],[f300])).
% 214.03/28.14 fof(f6080,plain,(
% 214.03/28.14 (![V_m_2,T_b,V_a_2]: ((![T_a]: ~hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),c_Map_Odom(T_a,T_b,V_m_2))))|~hAPP(V_m_2,V_a_2)=c_Option_Ooption_ONone(T_b)))&(![V_m_2,T_b,V_a_2]: ((![T_a]: hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),c_Map_Odom(T_a,T_b,V_m_2))))|hAPP(V_m_2,V_a_2)=c_Option_Ooption_ONone(T_b)))),
% 214.03/28.14 inference(miniscoping,[status(thm)],[f6079])).
% 214.03/28.14 fof(f6082,plain,(
% 214.03/28.14 ![X0,X1,X2,X3]: (hBOOL(hAPP(hAPP(c_member(X0),X1),c_Map_Odom(X0,X2,X3)))|hAPP(X3,X1)=c_Option_Ooption_ONone(X2))),
% 214.03/28.14 inference(cnf_transformation,[status(thm)],[f6080])).
% 214.03/28.14 fof(f19977,plain,(
% 214.03/28.14 ![B_x]: (~hBOOL(hAPP(hAPP(c_member(tc_Com_Opname),B_x),c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody)))|c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Hoare__Mirabelle_OMGT(hAPP(c_Com_Ocom_OBODY,B_x))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_HOL_Obool)))))),
% 214.03/28.14 inference(pre_NNF_transformation,[status(thm)],[f5243])).
% 214.03/28.14 fof(f19978,plain,(
% 214.03/28.14 ![X0]: (~hBOOL(hAPP(hAPP(c_member(tc_Com_Opname),X0),c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody)))|c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Hoare__Mirabelle_OMGT(hAPP(c_Com_Ocom_OBODY,X0))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_HOL_Obool)))))),
% 214.03/28.14 inference(cnf_transformation,[status(thm)],[f19977])).
% 214.03/28.14 fof(f19979,plain,(
% 214.03/28.14 hAPP(c_Com_Obody,v_pname)=hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),v_y)),
% 214.03/28.14 inference(cnf_transformation,[status(thm)],[f5244])).
% 214.03/28.14 fof(f19980,plain,(
% 214.03/28.14 ~c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Hoare__Mirabelle_OMGT(hAPP(c_Com_Ocom_OBODY,v_pname))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_HOL_Obool))))),
% 214.03/28.14 inference(cnf_transformation,[status(thm)],[f5246])).
% 214.03/28.14 fof(f20272,plain,(
% 214.03/28.14 ![X0,X1]: (~c_Option_Ooption_ONone(X0)=hAPP(c_Option_Ooption_OSome(X0),X1))),
% 214.03/28.14 inference(destructive_equality_resolution,[status(thm)],[f5580])).
% 214.03/28.14 fof(f20840,plain,(
% 214.03/28.14 ~c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,c_Option_Oset(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),hAPP(c_Option_Ooption_OSome(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Hoare__Mirabelle_OMGT(hAPP(c_Com_Ocom_OBODY,v_pname)))))),
% 214.03/28.14 inference(backward_demodulation,[status(thm)],[f5283,f19980])).
% 214.03/28.14 fof(f20849,plain,(
% 214.03/28.14 ![X0,X1]: (~c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool))=c_Option_Oset(X0,hAPP(c_Option_Ooption_OSome(X0),X1)))),
% 214.03/28.14 inference(paramodulation,[status(thm)],[f5283,f5267])).
% 214.03/28.14 fof(f21051,plain,(
% 214.03/28.14 ![X0,X1,X2]: (~hBOOL(hAPP(hAPP(c_member(X0),X1),c_Option_Oset(X0,hAPP(c_Option_Ooption_OSome(X0),X2))))|X1=X2|hBOOL(hAPP(hAPP(c_member(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)))))),
% 214.03/28.14 inference(paramodulation,[status(thm)],[f5283,f5674])).
% 214.03/28.14 fof(f21052,plain,(
% 214.03/28.14 ![X0,X1,X2]: (~hBOOL(hAPP(hAPP(c_member(X0),X1),c_Option_Oset(X0,hAPP(c_Option_Ooption_OSome(X0),X2))))|X1=X2)),
% 214.03/28.14 inference(forward_subsumption_resolution,[status(thm)],[f21051,f5672])).
% 214.03/28.14 fof(f21836,plain,(
% 214.03/28.14 ![X0,X1,X2]: (hBOOL(hAPP(hAPP(c_member(X0),X1),X2))|hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_fun(X0,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(X0),X1),X2)),c_Option_Oset(X0,hAPP(c_Option_Ooption_OSome(X0),X1)))=X2)),
% 214.03/28.14 inference(forward_demodulation,[status(thm)],[f5283,f5933])).
% 214.03/28.14 fof(f23960,plain,(
% 214.03/28.14 ![X0]: (~hBOOL(hAPP(hAPP(c_member(tc_Com_Opname),X0),c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody)))|c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,c_Option_Oset(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),hAPP(c_Option_Ooption_OSome(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Hoare__Mirabelle_OMGT(hAPP(c_Com_Ocom_OBODY,X0))))))),
% 116.20/28.33 inference(forward_demodulation,[status(thm)],[f5283,f19978])).
% 116.20/28.33 fof(f23962,plain,(
% 116.20/28.33 ![X0]: (c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,c_Option_Oset(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),hAPP(c_Option_Ooption_OSome(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Hoare__Mirabelle_OMGT(hAPP(c_Com_Ocom_OBODY,X0)))))|hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_fun(tc_Com_Opname,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(tc_Com_Opname),X0),c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody))),c_Option_Oset(tc_Com_Opname,hAPP(c_Option_Ooption_OSome(tc_Com_Opname),X0)))=c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody))),
% 116.20/28.33 inference(resolution,[status(thm)],[f23960,f21836])).
% 116.20/28.33 fof(f44571,plain,(
% 116.20/28.33 ![X0,X1]: (c_Option_Oset(X0,hAPP(c_Option_Ooption_OSome(X0),X1))=c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool))|sK26_skl(X0,c_Option_Oset(X0,hAPP(c_Option_Ooption_OSome(X0),X1)))=X1)),
% 116.20/28.33 inference(resolution,[status(thm)],[f5973,f21052])).
% 116.20/28.33 fof(f44620,plain,(
% 116.20/28.33 ![X0,X1]: (sK26_skl(X0,c_Option_Oset(X0,hAPP(c_Option_Ooption_OSome(X0),X1)))=X1)),
% 116.20/28.33 inference(forward_subsumption_resolution,[status(thm)],[f44571,f20849])).
% 116.20/28.33 fof(f66634,plain,(
% 116.20/28.33 hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_fun(tc_Com_Opname,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(tc_Com_Opname),v_pname),c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody))),c_Option_Oset(tc_Com_Opname,hAPP(c_Option_Ooption_OSome(tc_Com_Opname),v_pname)))=c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody)),
% 116.20/28.33 inference(resolution,[status(thm)],[f23962,f20840])).
% 116.20/28.33 fof(f66883,plain,(
% 116.20/28.33 ![X0]: (~hBOOL(hAPP(hAPP(c_member(tc_Com_Opname),X0),c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody)))|~hBOOL(hAPP(hAPP(c_member(tc_Com_Opname),X0),c_Option_Oset(tc_Com_Opname,hAPP(c_Option_Ooption_OSome(tc_Com_Opname),v_pname)))))),
% 116.20/28.33 inference(paramodulation,[status(thm)],[f66634,f5692])).
% 116.20/28.33 fof(f67484,plain,(
% 116.20/28.33 ~hBOOL(hAPP(hAPP(c_member(tc_Com_Opname),sK26_skl(tc_Com_Opname,c_Option_Oset(tc_Com_Opname,hAPP(c_Option_Ooption_OSome(tc_Com_Opname),v_pname)))),c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody)))|c_Option_Oset(tc_Com_Opname,hAPP(c_Option_Ooption_OSome(tc_Com_Opname),v_pname))=c_Orderings_Obot__class_Obot(tc_fun(tc_Com_Opname,tc_HOL_Obool))),
% 116.20/28.33 inference(resolution,[status(thm)],[f66883,f5973])).
% 116.20/28.33 fof(f67494,plain,(
% 116.20/28.33 ~hBOOL(hAPP(hAPP(c_member(tc_Com_Opname),v_pname),c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody)))|c_Option_Oset(tc_Com_Opname,hAPP(c_Option_Ooption_OSome(tc_Com_Opname),v_pname))=c_Orderings_Obot__class_Obot(tc_fun(tc_Com_Opname,tc_HOL_Obool))),
% 116.20/28.33 inference(forward_demodulation,[status(thm)],[f44620,f67484])).
% 116.20/28.33 fof(f67495,plain,(
% 116.20/28.33 ~hBOOL(hAPP(hAPP(c_member(tc_Com_Opname),v_pname),c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody)))),
% 116.20/28.33 inference(forward_subsumption_resolution,[status(thm)],[f67494,f20849])).
% 116.20/28.33 fof(f67502,plain,(
% 116.20/28.33 hAPP(c_Com_Obody,v_pname)=c_Option_Ooption_ONone(tc_Com_Ocom)),
% 116.20/28.33 inference(resolution,[status(thm)],[f67495,f6082])).
% 116.20/28.33 fof(f82159,plain,(
% 116.20/28.33 c_Option_Ooption_ONone(tc_Com_Ocom)=hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),v_y)),
% 116.20/28.33 inference(forward_demodulation,[status(thm)],[f67502,f19979])).
% 116.20/28.33 fof(f82160,plain,(
% 116.20/28.33 $false),
% 116.20/28.33 inference(forward_subsumption_resolution,[status(thm)],[f82159,f20272])).
% 116.20/28.33 % SZS output end CNFRefutation for theBenchmark.p
% 116.20/28.39 % Elapsed time: 27.996200 seconds
% 116.20/28.39 % CPU time: 216.077233 seconds
% 116.20/28.39 % Total memory used: 1.742 GB
% 116.20/28.39 % Net memory used: 1.647 GB
%------------------------------------------------------------------------------