%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW355+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 : n019.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 194.75s 30.91s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW355+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.11/5.39 % Computer : n019.cluster.edu
% 0.11/5.39 % Model : x86_64 x86_64
% 0.11/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.39 % Memory : 8046.5625MB
% 0.11/5.39 % OS : Linux 6.8.0-71-generic
% 0.11/5.39 % CPULimit : 300
% 0.11/5.39 % WCLimit : 300
% 0.11/5.39 % DateTime : Mon Sep 21 09:48:55 UTC 2026
% 0.11/5.40 % CPUTime :
% 1.01/6.42 % Drodi V4.1.1
% 194.75/30.91 % Refutation found
% 194.75/30.91 % SZS status Theorem for theBenchmark: Theorem is valid
% 194.75/30.91 % SZS output start CNFRefutation for theBenchmark
% 194.75/30.91 fof(f3,axiom,(
% 194.75/30.91 (! [V_P_2,V_Ga_2,T_a] : c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_a),V_P_2),c_Com_Ocom_OSKIP),V_P_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_HOL_Obool)))) )),
% 194.75/30.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 194.75/30.91 fof(f7,axiom,(
% 194.75/30.91 (! [V_Ga_2,V_ts_2,V_G_H_2,T_a] :( c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_G_H_2,V_ts_2)=> ( c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,V_G_H_2)=> c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,V_ts_2) ) ) )),
% 194.75/30.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 194.75/30.91 fof(f9,axiom,(
% 194.75/30.91 (! [V_ts_2,V_t_2,V_Ga_2,T_a] :( c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),V_t_2),V_ts_2))=> ( c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),V_t_2),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_HOL_Obool))))& c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,V_ts_2) ) ) )),
% 194.75/30.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 194.75/30.91 fof(f10,axiom,(
% 194.75/30.91 (! [V_s] : hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),V_s),V_s)) )),
% 194.75/30.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 194.75/30.91 fof(f14,axiom,(
% 194.75/30.91 (! [V_ca_2] : c_Hoare__Mirabelle_OMGT(V_ca_2) = hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(tc_Com_Ostate),c_fequal),V_ca_2),c_Natural_Oevalc(V_ca_2)) )),
% 194.75/30.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 194.75/30.91 fof(f37,axiom,(
% 194.75/30.91 (! [V_Q_2,V_Q_H_2,V_ca_2,V_P_2,V_Ga_2,T_a] :( c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_a),V_P_2),V_ca_2),V_Q_H_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_HOL_Obool))))=> ( (! [B_Z,B_s] :( hBOOL(hAPP(hAPP(V_Q_H_2,B_Z),B_s))=> hBOOL(hAPP(hAPP(V_Q_2,B_Z),B_s)) ))=> c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_a),V_P_2),V_ca_2),V_Q_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_HOL_Obool)))) ) ) )),
% 194.75/30.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 194.75/30.91 fof(f125,axiom,(
% 194.75/30.91 (! [V_y_2,V_x_2,T_a] :( hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),hAPP(c_fequal,V_y_2)))<=> V_x_2 = V_y_2 ) )),
% 194.75/30.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 194.75/30.91 fof(f140,axiom,(
% 194.75/30.91 (! [V_A_2,V_a_2,T_a] :( hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),V_A_2))=> hAPP(hAPP(c_Set_Oinsert(T_a),V_a_2),V_A_2) = V_A_2 ) )),
% 194.75/30.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 194.75/30.91 fof(f1105,axiom,(
% 194.75/30.91 (! [V_a_2,V_B_2,T_a] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_a,tc_HOL_Obool)),V_B_2),hAPP(hAPP(c_Set_Oinsert(T_a),V_a_2),V_B_2))) )),
% 194.75/30.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 194.75/30.91 fof(f1128,axiom,(
% 194.75/30.91 (! [V_Ga_2,V_ts_2,T_a] :( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_HOL_Obool)),V_ts_2),V_Ga_2))=> c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,V_ts_2) ) )),
% 194.75/30.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 194.75/30.91 fof(f2233,axiom,(
% 194.75/30.91 (! [V_P_2,T_a] : hAPP(c_Set_OCollect(T_a),V_P_2) = V_P_2 )),
% 194.75/30.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 194.75/30.91 fof(f2255,axiom,(
% 194.75/30.91 (! [V_a_2,T_a] : hAPP(c_Set_OCollect(T_a),hAPP(c_fequal,V_a_2)) = hAPP(hAPP(c_Set_Oinsert(T_a),V_a_2),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))) )),
% 194.75/30.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 194.75/30.91 fof(f5228,axiom,(
% 194.75/30.91 (! [V_y_2,V_x_2] :( ~ hBOOL(hAPP(hAPP(c_fequal,V_x_2),V_y_2))| V_x_2 = V_y_2 ) )),
% 194.75/30.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 194.75/30.91 fof(f5245,conjecture,(
% 194.75/30.91 c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(tc_Com_Ostate),c_fequal),c_Com_Ocom_OSKIP),c_Natural_Oevalc(c_Com_Ocom_OSKIP))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_HOL_Obool)))) ),
% 194.75/30.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 194.75/30.91 fof(f5246,negated_conjecture,(
% 194.75/30.91 ~(c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(tc_Com_Ostate),c_fequal),c_Com_Ocom_OSKIP),c_Natural_Oevalc(c_Com_Ocom_OSKIP))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_HOL_Obool)))) )),
% 194.75/30.91 inference(negated_conjecture,[status(cth)],[f5245])).
% 194.75/30.91 fof(f5251,plain,(
% 194.75/30.91 ![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)))))),
% 194.75/30.91 inference(cnf_transformation,[status(thm)],[f3])).
% 194.75/30.91 fof(f5260,plain,(
% 194.75/30.91 ![V_Ga_2,V_ts_2,V_G_H_2,T_a]: (~c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_G_H_2,V_ts_2)|(~c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,V_G_H_2)|c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,V_ts_2)))),
% 194.75/30.91 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 194.75/30.91 fof(f5261,plain,(
% 194.75/30.91 ![V_ts_2,V_G_H_2,T_a]: (~c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_G_H_2,V_ts_2)|(![V_Ga_2]: (~c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,V_G_H_2)|c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,V_ts_2))))),
% 194.75/30.91 inference(miniscoping,[status(thm)],[f5260])).
% 194.75/30.91 fof(f5262,plain,(
% 194.75/30.91 ![X0,X1,X2,X3]: (~c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,X2)|~c_Hoare__Mirabelle_Ohoare__derivs(X0,X3,X1)|c_Hoare__Mirabelle_Ohoare__derivs(X0,X3,X2))),
% 194.75/30.91 inference(cnf_transformation,[status(thm)],[f5261])).
% 194.75/30.91 fof(f5266,plain,(
% 194.75/30.91 ![V_ts_2,V_t_2,V_Ga_2,T_a]: (~c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),V_t_2),V_ts_2))|(c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),V_t_2),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_HOL_Obool))))&c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,V_ts_2)))),
% 194.75/30.91 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 194.75/30.91 fof(f5267,plain,(
% 194.75/30.91 ![X0,X1,X2,X3]: (~c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),X2),X3))|c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),X2),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool)))))),
% 194.75/30.91 inference(cnf_transformation,[status(thm)],[f5266])).
% 194.75/30.91 fof(f5269,plain,(
% 194.75/30.91 ![X0]: (hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),X0),X0)))),
% 194.75/30.91 inference(cnf_transformation,[status(thm)],[f10])).
% 194.75/30.91 fof(f5276,plain,(
% 194.75/30.91 ![X0]: (c_Hoare__Mirabelle_OMGT(X0)=hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(tc_Com_Ostate),c_fequal),X0),c_Natural_Oevalc(X0)))),
% 194.75/30.91 inference(cnf_transformation,[status(thm)],[f14])).
% 194.75/30.91 fof(f5335,plain,(
% 194.75/30.91 ![V_Q_2,V_Q_H_2,V_ca_2,V_P_2,V_Ga_2,T_a]: (~c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_a),V_P_2),V_ca_2),V_Q_H_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_HOL_Obool))))|((?[B_Z,B_s]: (hBOOL(hAPP(hAPP(V_Q_H_2,B_Z),B_s))&~hBOOL(hAPP(hAPP(V_Q_2,B_Z),B_s))))|c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_a),V_P_2),V_ca_2),V_Q_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_HOL_Obool))))))),
% 194.75/30.91 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 194.75/30.91 fof(f5336,plain,(
% 194.75/30.91 ![V_Q_H_2,V_ca_2,V_P_2,V_Ga_2,T_a]: (~c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_a),V_P_2),V_ca_2),V_Q_H_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_HOL_Obool))))|(![V_Q_2]: ((?[B_Z,B_s]: (hBOOL(hAPP(hAPP(V_Q_H_2,B_Z),B_s))&~hBOOL(hAPP(hAPP(V_Q_2,B_Z),B_s))))|c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_a),V_P_2),V_ca_2),V_Q_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_HOL_Obool)))))))),
% 194.75/30.91 inference(miniscoping,[status(thm)],[f5335])).
% 194.75/30.91 fof(f5337,plain,(
% 194.75/30.91 ![V_Q_H_2,V_ca_2,V_P_2,V_Ga_2,T_a]: (~c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_a),V_P_2),V_ca_2),V_Q_H_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_HOL_Obool))))|(![V_Q_2]: ((hBOOL(hAPP(hAPP(V_Q_H_2,sK5_skl(V_Q_2,T_a,V_Ga_2,V_P_2,V_ca_2,V_Q_H_2)),sK6_skl(V_Q_2,T_a,V_Ga_2,V_P_2,V_ca_2,V_Q_H_2)))&~hBOOL(hAPP(hAPP(V_Q_2,sK5_skl(V_Q_2,T_a,V_Ga_2,V_P_2,V_ca_2,V_Q_H_2)),sK6_skl(V_Q_2,T_a,V_Ga_2,V_P_2,V_ca_2,V_Q_H_2))))|c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_a),V_P_2),V_ca_2),V_Q_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_HOL_Obool)))))))),
% 194.75/30.91 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl,sK6_skl]),skolemize(B_Z,sK5_skl(V_Q_2,T_a,V_Ga_2,V_P_2,V_ca_2,V_Q_H_2)),skolemize(B_s,sK6_skl(V_Q_2,T_a,V_Ga_2,V_P_2,V_ca_2,V_Q_H_2))],[f5336])).
% 194.75/30.91 fof(f5338,plain,(
% 194.75/30.91 ![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,sK5_skl(X5,X0,X1,X2,X3,X4)),sK6_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)))))),
% 194.75/30.91 inference(cnf_transformation,[status(thm)],[f5337])).
% 194.75/30.91 fof(f5339,plain,(
% 194.75/30.91 ![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,sK5_skl(X5,X0,X1,X2,X3,X4)),sK6_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)))))),
% 194.75/30.91 inference(cnf_transformation,[status(thm)],[f5337])).
% 194.75/30.91 fof(f5591,plain,(
% 194.75/30.91 ![V_y_2,V_x_2,T_a]: ((~hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),hAPP(c_fequal,V_y_2)))|V_x_2=V_y_2)&(hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),hAPP(c_fequal,V_y_2)))|~V_x_2=V_y_2))),
% 194.75/30.91 inference(NNF_transformation,[status(thm)],[f125])).
% 194.75/30.91 fof(f5592,plain,(
% 194.75/30.91 (![V_y_2,V_x_2]: ((![T_a]: ~hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),hAPP(c_fequal,V_y_2))))|V_x_2=V_y_2))&(![V_y_2,V_x_2]: ((![T_a]: hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),hAPP(c_fequal,V_y_2))))|~V_x_2=V_y_2))),
% 194.75/30.91 inference(miniscoping,[status(thm)],[f5591])).
% 194.75/30.91 fof(f5594,plain,(
% 194.75/30.91 ![X0,X1,X2]: (hBOOL(hAPP(hAPP(c_member(X0),X1),hAPP(c_fequal,X2)))|~X1=X2)),
% 194.75/30.91 inference(cnf_transformation,[status(thm)],[f5592])).
% 194.75/30.91 fof(f5648,plain,(
% 194.75/30.91 ![V_A_2,V_a_2,T_a]: (~hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),V_A_2))|hAPP(hAPP(c_Set_Oinsert(T_a),V_a_2),V_A_2)=V_A_2)),
% 194.75/30.91 inference(pre_NNF_transformation,[status(thm)],[f140])).
% 194.75/30.91 fof(f5649,plain,(
% 194.75/30.91 ![X0,X1,X2]: (~hBOOL(hAPP(hAPP(c_member(X0),X1),X2))|hAPP(hAPP(c_Set_Oinsert(X0),X1),X2)=X2)),
% 194.75/30.91 inference(cnf_transformation,[status(thm)],[f5648])).
% 194.75/30.91 fof(f8519,plain,(
% 194.75/30.91 ![X0,X1,X2]: (hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),X1),hAPP(hAPP(c_Set_Oinsert(X0),X2),X1))))),
% 194.75/30.91 inference(cnf_transformation,[status(thm)],[f1105])).
% 194.75/30.91 fof(f8574,plain,(
% 194.75/30.91 ![V_Ga_2,V_ts_2,T_a]: (~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_HOL_Obool)),V_ts_2),V_Ga_2))|c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_2,V_ts_2))),
% 194.75/30.91 inference(pre_NNF_transformation,[status(thm)],[f1128])).
% 194.75/30.91 fof(f8575,plain,(
% 194.75/30.91 ![X0,X1,X2]: (~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool)),X1),X2))|c_Hoare__Mirabelle_Ohoare__derivs(X0,X2,X1))),
% 194.75/30.91 inference(cnf_transformation,[status(thm)],[f8574])).
% 194.75/30.91 fof(f12160,plain,(
% 194.75/30.91 ![X0,X1]: (hAPP(c_Set_OCollect(X0),X1)=X1)),
% 194.75/30.91 inference(cnf_transformation,[status(thm)],[f2233])).
% 194.75/30.91 fof(f12211,plain,(
% 194.75/30.91 ![X0,X1]: (hAPP(c_Set_OCollect(X0),hAPP(c_fequal,X1))=hAPP(hAPP(c_Set_Oinsert(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool))))),
% 194.75/30.91 inference(cnf_transformation,[status(thm)],[f2255])).
% 194.75/30.91 fof(f19935,plain,(
% 194.75/30.91 ![X0,X1]: (~hBOOL(hAPP(hAPP(c_fequal,X0),X1))|X0=X1)),
% 194.75/30.91 inference(cnf_transformation,[status(thm)],[f5228])).
% 194.75/30.91 fof(f19961,plain,(
% 194.75/30.91 ~c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(tc_Com_Ostate),c_fequal),c_Com_Ocom_OSKIP),c_Natural_Oevalc(c_Com_Ocom_OSKIP))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_HOL_Obool))))),
% 194.75/30.91 inference(cnf_transformation,[status(thm)],[f5246])).
% 194.75/30.91 fof(f20259,plain,(
% 194.75/30.91 ![X0,X1]: (hBOOL(hAPP(hAPP(c_member(X0),X1),hAPP(c_fequal,X1))))),
% 194.75/30.91 inference(destructive_equality_resolution,[status(thm)],[f5594])).
% 194.75/30.91 fof(f20749,plain,(
% 194.75/30.91 ![X0]: (~c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,X0,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(tc_Com_Ostate),c_fequal),c_Com_Ocom_OSKIP),c_Natural_Oevalc(c_Com_Ocom_OSKIP))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_HOL_Obool))))|~c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,X0))),
% 194.75/30.91 inference(resolution,[status(thm)],[f5262,f19961])).
% 194.75/30.91 fof(f20751,plain,(
% 194.75/30.91 ![X0]: (~c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(tc_Com_Ostate),c_fequal),c_Com_Ocom_OSKIP),c_Natural_Oevalc(c_Com_Ocom_OSKIP))),X0)))),
% 194.75/30.91 inference(resolution,[status(thm)],[f5267,f19961])).
% 194.75/30.91 fof(f20759,plain,(
% 194.75/30.91 ![X0,X1]: (~c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,X0)|~c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,X0,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(tc_Com_Ostate),c_fequal),c_Com_Ocom_OSKIP),c_Natural_Oevalc(c_Com_Ocom_OSKIP))),X1)))),
% 194.75/30.91 inference(resolution,[status(thm)],[f20749,f5267])).
% 194.75/30.91 fof(f20773,plain,(
% 194.75/30.91 ![X0]: (~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(c_Com_Ocom_OSKIP)),X0)))),
% 194.75/30.91 inference(backward_demodulation,[status(thm)],[f5276,f20751])).
% 194.75/30.91 fof(f20788,plain,(
% 194.75/30.91 ![X0,X1]: (~c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,X0)|~c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,X0,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Hoare__Mirabelle_OMGT(c_Com_Ocom_OSKIP)),X1)))),
% 194.75/30.91 inference(forward_demodulation,[status(thm)],[f5276,f20759])).
% 194.75/30.91 fof(f20936,plain,(
% 194.75/30.91 ![X0,X1,X2,X3]: (hBOOL(hAPP(hAPP(X0,sK5_skl(X1,X2,X3,X0,c_Com_Ocom_OSKIP,X0)),sK6_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)))))),
% 194.75/30.91 inference(resolution,[status(thm)],[f5338,f5251])).
% 194.75/30.91 fof(f21053,plain,(
% 194.75/30.91 ![X0,X1]: (hAPP(hAPP(c_Set_Oinsert(X0),X1),hAPP(c_fequal,X1))=hAPP(c_fequal,X1))),
% 194.75/30.91 inference(resolution,[status(thm)],[f5649,f20259])).
% 194.75/30.91 fof(f21116,plain,(
% 194.75/30.91 ~c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,hAPP(c_fequal,c_Hoare__Mirabelle_OMGT(c_Com_Ocom_OSKIP)))),
% 194.75/30.91 inference(paramodulation,[status(thm)],[f21053,f20773])).
% 194.75/30.91 fof(f21315,plain,(
% 194.75/30.91 ![X0,X1,X2]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),X1),X2),X2))),
% 194.75/30.91 inference(resolution,[status(thm)],[f8575,f8519])).
% 194.75/30.91 fof(f21486,plain,(
% 194.75/30.91 ![X0,X1]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal,X1),hAPP(c_fequal,X1)))),
% 194.75/30.91 inference(paramodulation,[status(thm)],[f21053,f21315])).
% 194.75/30.91 fof(f22108,plain,(
% 194.75/30.91 ![X0,X1,X2]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(c_Set_OCollect(tc_Hoare__Mirabelle_Otriple(X0)),hAPP(c_fequal,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X0),X2),c_Com_Ocom_OSKIP),X2)))))),
% 194.75/30.91 inference(backward_demodulation,[status(thm)],[f12211,f5251])).
% 194.75/30.91 fof(f22109,plain,(
% 194.75/30.91 ![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,sK5_skl(X5,X0,X1,X2,X3,X4)),sK6_skl(X5,X0,X1,X2,X3,X4)))|c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(c_Set_OCollect(tc_Hoare__Mirabelle_Otriple(X0)),hAPP(c_fequal,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X0),X2),X3),X5)))))),
% 194.75/30.91 inference(backward_demodulation,[status(thm)],[f12211,f5339])).
% 194.75/30.91 fof(f22136,plain,(
% 194.75/30.91 ![X0]: (~c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,X0)|~c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,X0,hAPP(c_Set_OCollect(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_fequal,c_Hoare__Mirabelle_OMGT(c_Com_Ocom_OSKIP)))))),
% 194.75/30.91 inference(paramodulation,[status(thm)],[f12211,f20788])).
% 194.75/30.91 fof(f22176,plain,(
% 194.75/30.91 ![X0,X1,X2,X3,X4,X5]: (~c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(c_Set_OCollect(tc_Hoare__Mirabelle_Otriple(X0)),hAPP(c_fequal,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X0),X2),X3),X4))))|~hBOOL(hAPP(hAPP(X5,sK5_skl(X5,X0,X1,X2,X3,X4)),sK6_skl(X5,X0,X1,X2,X3,X4)))|c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(c_Set_OCollect(tc_Hoare__Mirabelle_Otriple(X0)),hAPP(c_fequal,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X0),X2),X3),X5)))))),
% 194.75/30.91 inference(forward_demodulation,[status(thm)],[f12211,f22109])).
% 194.75/30.91 fof(f22557,plain,(
% 194.75/30.91 ![X0,X1,X2,X3]: (~hBOOL(hAPP(hAPP(X0,sK5_skl(X0,X1,X2,X3,c_Com_Ocom_OSKIP,X3)),sK6_skl(X0,X1,X2,X3,c_Com_Ocom_OSKIP,X3)))|c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,hAPP(c_Set_OCollect(tc_Hoare__Mirabelle_Otriple(X1)),hAPP(c_fequal,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X1),X3),c_Com_Ocom_OSKIP),X0)))))),
% 194.75/30.91 inference(resolution,[status(thm)],[f22176,f22108])).
% 194.75/30.91 fof(f24969,plain,(
% 194.75/30.91 ![X0,X1,X2,X3]: (hBOOL(hAPP(hAPP(X0,sK5_skl(X1,X2,X3,X0,c_Com_Ocom_OSKIP,X0)),sK6_skl(X1,X2,X3,X0,c_Com_Ocom_OSKIP,X0)))|c_Hoare__Mirabelle_Ohoare__derivs(X2,X3,hAPP(c_Set_OCollect(tc_Hoare__Mirabelle_Otriple(X2)),hAPP(c_fequal,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X2),X0),c_Com_Ocom_OSKIP),X1)))))),
% 194.75/30.91 inference(forward_demodulation,[status(thm)],[f12211,f20936])).
% 194.75/30.91 fof(f25035,plain,(
% 194.75/30.91 ![X0,X1]: (hBOOL(hAPP(hAPP(X0,sK5_skl(X1,tc_Com_Ostate,v_G,X0,c_Com_Ocom_OSKIP,X0)),sK6_skl(X1,tc_Com_Ostate,v_G,X0,c_Com_Ocom_OSKIP,X0)))|~c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,hAPP(c_Set_OCollect(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_fequal,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(tc_Com_Ostate),X0),c_Com_Ocom_OSKIP),X1))),hAPP(c_Set_OCollect(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_fequal,c_Hoare__Mirabelle_OMGT(c_Com_Ocom_OSKIP)))))),
% 194.75/30.91 inference(resolution,[status(thm)],[f24969,f22136])).
% 194.75/30.91 fof(f42691,plain,(
% 194.75/30.91 ![X0,X1]: (hBOOL(hAPP(hAPP(X0,sK5_skl(X1,tc_Com_Ostate,v_G,X0,c_Com_Ocom_OSKIP,X0)),sK6_skl(X1,tc_Com_Ostate,v_G,X0,c_Com_Ocom_OSKIP,X0)))|~c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,hAPP(c_fequal,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(tc_Com_Ostate),X0),c_Com_Ocom_OSKIP),X1)),hAPP(c_Set_OCollect(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_fequal,c_Hoare__Mirabelle_OMGT(c_Com_Ocom_OSKIP)))))),
% 156.92/31.10 inference(backward_demodulation,[status(thm)],[f12160,f25035])).
% 156.92/31.10 fof(f42954,plain,(
% 156.92/31.10 ![X0,X1]: (hBOOL(hAPP(hAPP(X0,sK5_skl(X1,tc_Com_Ostate,v_G,X0,c_Com_Ocom_OSKIP,X0)),sK6_skl(X1,tc_Com_Ostate,v_G,X0,c_Com_Ocom_OSKIP,X0)))|~c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,hAPP(c_fequal,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(tc_Com_Ostate),X0),c_Com_Ocom_OSKIP),X1)),hAPP(c_fequal,c_Hoare__Mirabelle_OMGT(c_Com_Ocom_OSKIP))))),
% 156.92/31.10 inference(forward_demodulation,[status(thm)],[f12160,f42691])).
% 156.92/31.10 fof(f46285,plain,(
% 156.92/31.10 hBOOL(hAPP(hAPP(c_fequal,sK5_skl(c_Natural_Oevalc(c_Com_Ocom_OSKIP),tc_Com_Ostate,v_G,c_fequal,c_Com_Ocom_OSKIP,c_fequal)),sK6_skl(c_Natural_Oevalc(c_Com_Ocom_OSKIP),tc_Com_Ostate,v_G,c_fequal,c_Com_Ocom_OSKIP,c_fequal)))|~c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,hAPP(c_fequal,c_Hoare__Mirabelle_OMGT(c_Com_Ocom_OSKIP)),hAPP(c_fequal,c_Hoare__Mirabelle_OMGT(c_Com_Ocom_OSKIP)))),
% 156.92/31.10 inference(paramodulation,[status(thm)],[f5276,f42954])).
% 156.92/31.10 fof(f46286,plain,(
% 156.92/31.10 hBOOL(hAPP(hAPP(c_fequal,sK5_skl(c_Natural_Oevalc(c_Com_Ocom_OSKIP),tc_Com_Ostate,v_G,c_fequal,c_Com_Ocom_OSKIP,c_fequal)),sK6_skl(c_Natural_Oevalc(c_Com_Ocom_OSKIP),tc_Com_Ostate,v_G,c_fequal,c_Com_Ocom_OSKIP,c_fequal)))),
% 156.92/31.10 inference(forward_subsumption_resolution,[status(thm)],[f46285,f21486])).
% 156.92/31.10 fof(f70653,plain,(
% 156.92/31.10 ![X0,X1,X2,X3]: (~hBOOL(hAPP(hAPP(X0,sK5_skl(X0,X1,X2,X3,c_Com_Ocom_OSKIP,X3)),sK6_skl(X0,X1,X2,X3,c_Com_Ocom_OSKIP,X3)))|c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,hAPP(c_fequal,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X1),X3),c_Com_Ocom_OSKIP),X0))))),
% 156.92/31.10 inference(forward_demodulation,[status(thm)],[f12160,f22557])).
% 156.92/31.10 fof(f74668,plain,(
% 156.92/31.10 sK5_skl(c_Natural_Oevalc(c_Com_Ocom_OSKIP),tc_Com_Ostate,v_G,c_fequal,c_Com_Ocom_OSKIP,c_fequal)=sK6_skl(c_Natural_Oevalc(c_Com_Ocom_OSKIP),tc_Com_Ostate,v_G,c_fequal,c_Com_Ocom_OSKIP,c_fequal)),
% 156.92/31.10 inference(resolution,[status(thm)],[f46286,f19935])).
% 156.92/31.10 fof(f74791,plain,(
% 156.92/31.10 ~hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),sK5_skl(c_Natural_Oevalc(c_Com_Ocom_OSKIP),tc_Com_Ostate,v_G,c_fequal,c_Com_Ocom_OSKIP,c_fequal)),sK5_skl(c_Natural_Oevalc(c_Com_Ocom_OSKIP),tc_Com_Ostate,v_G,c_fequal,c_Com_Ocom_OSKIP,c_fequal)))|c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,hAPP(c_fequal,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(tc_Com_Ostate),c_fequal),c_Com_Ocom_OSKIP),c_Natural_Oevalc(c_Com_Ocom_OSKIP))))),
% 156.92/31.10 inference(paramodulation,[status(thm)],[f74668,f70653])).
% 156.92/31.10 fof(f74793,plain,(
% 156.92/31.10 ~hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),sK5_skl(c_Natural_Oevalc(c_Com_Ocom_OSKIP),tc_Com_Ostate,v_G,c_fequal,c_Com_Ocom_OSKIP,c_fequal)),sK5_skl(c_Natural_Oevalc(c_Com_Ocom_OSKIP),tc_Com_Ostate,v_G,c_fequal,c_Com_Ocom_OSKIP,c_fequal)))|c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,hAPP(c_fequal,c_Hoare__Mirabelle_OMGT(c_Com_Ocom_OSKIP)))),
% 156.92/31.10 inference(forward_demodulation,[status(thm)],[f5276,f74791])).
% 156.92/31.10 fof(f74794,plain,(
% 156.92/31.10 c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,hAPP(c_fequal,c_Hoare__Mirabelle_OMGT(c_Com_Ocom_OSKIP)))),
% 156.92/31.10 inference(forward_subsumption_resolution,[status(thm)],[f74793,f5269])).
% 156.92/31.10 fof(f74952,plain,(
% 156.92/31.10 $false),
% 156.92/31.10 inference(forward_subsumption_resolution,[status(thm)],[f74794,f21116])).
% 156.92/31.10 % SZS output end CNFRefutation for theBenchmark.p
% 66.61/31.16 % Elapsed time: 25.747188 seconds
% 66.61/31.16 % CPU time: 195.996443 seconds
% 66.61/31.16 % Total memory used: 1.756 GB
% 66.61/31.16 % Net memory used: 1.650 GB
%------------------------------------------------------------------------------