%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW356+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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:07:42 PM UTC 2026
% Result : Theorem 96.21s 13.23s
% Output : CNFRefutation 96.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 11
% Syntax : Number of formulae : 47 ( 17 unt; 4 def)
% Number of atoms : 91 ( 5 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 74 ( 30 ~; 31 |; 5 &)
% ( 4 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 5 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 5 con; 0-6 aty)
% Number of variables : 85 ( 81 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [V_a2_2,V_a1_2,T_a] : c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_a1_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(T_a),V_a2_2),c_Com_Ocom_OSKIP),V_a2_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_HOL_Obool)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [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,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)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [V_s] : hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),V_s),V_s)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [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)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2255,axiom,
! [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))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5228,axiom,
! [V_y_2,V_x_2] :
( V_x_2 = V_y_2
| ~ hBOOL(hAPP(hAPP(c_fequal,V_x_2),V_y_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5244,conjecture,
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)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5245,negated_conjecture,
~ 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)))),
inference(negated_conjecture,[status(cth)],[f5244]) ).
fof(f5252,plain,
! [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)))),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f5265,plain,
! [V_ts_2,V_t_2,V_Ga_2,T_a] :
( ( c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_Ga_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,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),V_t_2),V_ts_2)) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f5266,plain,
! [X0,X1,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))))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),X2),X3)) ),
inference(cnf_transformation,[status(thm)],[f5265]) ).
fof(f5268,plain,
! [X0] : hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),X0),X0)),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f5334,plain,
! [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_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_2,B_Z),B_s))
& hBOOL(hAPP(hAPP(V_Q_H_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_H_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_HOL_Obool)))) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f5335,plain,
! [V_Q_H_2,V_ca_2,V_P_2,V_Ga_2,T_a] :
( ! [V_Q_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))))
| ? [B_Z,B_s] :
( ~ hBOOL(hAPP(hAPP(V_Q_2,B_Z),B_s))
& hBOOL(hAPP(hAPP(V_Q_H_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_H_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_HOL_Obool)))) ),
inference(miniscoping,[status(thm)],[f5334]) ).
fof(f5336,plain,
! [V_Q_H_2,V_ca_2,V_P_2,V_Ga_2,T_a] :
( ! [V_Q_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))))
| ( ~ 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)))
& 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))) ) )
| ~ 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)))) ),
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))],[f5335]) ).
fof(f5337,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ 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),X4),X5),X0)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X2),tc_HOL_Obool))))
| 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),X4),X5),X1)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X2),tc_HOL_Obool))))
| hBOOL(hAPP(hAPP(X0,sK5_skl(X1,X2,X3,X4,X5,X0)),sK6_skl(X1,X2,X3,X4,X5,X0))) ),
inference(cnf_transformation,[status(thm)],[f5336]) ).
fof(f5338,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ 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),X4),X5)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X1),tc_HOL_Obool))))
| 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),X4),X0)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X1),tc_HOL_Obool))))
| ~ hBOOL(hAPP(hAPP(X0,sK5_skl(X0,X1,X2,X3,X4,X5)),sK6_skl(X0,X1,X2,X3,X4,X5))) ),
inference(cnf_transformation,[status(thm)],[f5336]) ).
fof(f12210,plain,
! [X0,X1] : hAPP(hAPP(c_Set_Oinsert(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool))) = hAPP(c_Set_OCollect(X0),hAPP(c_fequal,X1)),
inference(cnf_transformation,[status(thm)],[f2255]) ).
fof(f19934,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_fequal,X1),X0))
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f5228]) ).
fof(f19959,plain,
~ 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)))),
inference(cnf_transformation,[status(thm)],[f5245]) ).
fof(f20840,plain,
! [X0,X1,X2,X3] :
( 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))))
| 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))) ),
inference(resolution,[status(thm)],[f5337,f5252]) ).
fof(f21104,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,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),c_fequal),c_Com_Ocom_OSKIP),c_Natural_Oevalc(c_Com_Ocom_OSKIP))))),
inference(backward_demodulation,[status(thm)],[f12210,f19959]) ).
fof(f21107,plain,
! [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)))),
inference(backward_demodulation,[status(thm)],[f12210,f5252]) ).
fof(f21111,plain,
! [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(c_Set_OCollect(tc_Hoare__Mirabelle_Otriple(X0)),hAPP(c_fequal,X2))) ),
inference(backward_demodulation,[status(thm)],[f12210,f5266]) ).
fof(f21225,definition,
( sQ18_spl
<=> c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,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),c_fequal),c_Com_Ocom_OSKIP),c_Natural_Oevalc(c_Com_Ocom_OSKIP))))) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f21226,plain,
( ~ sQ18_spl
| c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,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),c_fequal),c_Com_Ocom_OSKIP),c_Natural_Oevalc(c_Com_Ocom_OSKIP))))) ),
inference(component_clause,[status(thm)],[f21225]) ).
fof(f21232,plain,
( ~ sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21226,f21104]) ).
fof(f21233,plain,
~ sQ18_spl,
inference(contradiction_clause,[status(thm)],[f21232]) ).
fof(f24704,plain,
! [X0,X1,X2,X3] :
( 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))))
| 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))) ),
inference(forward_demodulation,[status(thm)],[f12210,f20840]) ).
fof(f24752,plain,
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))),
inference(resolution,[status(thm)],[f24704,f21104]) ).
fof(f24769,plain,
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),
inference(resolution,[status(thm)],[f24752,f19934]) ).
fof(f26026,plain,
( ~ 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_fequal)),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,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))))
| ~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),sK6_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))) ),
inference(paramodulation,[status(thm)],[f24769,f5338]) ).
fof(f26027,definition,
( sQ75_spl
<=> hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),sK6_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))) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f26029,plain,
( sQ75_spl
| ~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),sK6_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))) ),
inference(component_clause,[status(thm)],[f26027]) ).
fof(f26030,definition,
( sQ76_spl
<=> 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)))) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f26031,plain,
( ~ sQ76_spl
| 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)))) ),
inference(component_clause,[status(thm)],[f26030]) ).
fof(f26033,definition,
( sQ77_spl
<=> 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_fequal)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_HOL_Obool)))) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f26035,plain,
( sQ77_spl
| ~ 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_fequal)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_HOL_Obool)))) ),
inference(component_clause,[status(thm)],[f26033]) ).
fof(f26036,plain,
( ~ sQ77_spl
| sQ76_spl
| ~ sQ75_spl ),
inference(split_clause,[status(thm)],[f26026,f26027,f26030,f26033]) ).
fof(f26037,plain,
( sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f26029,f5268]) ).
fof(f26038,plain,
sQ75_spl,
inference(contradiction_clause,[status(thm)],[f26037]) ).
fof(f26257,plain,
( ~ sQ76_spl
| c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,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),c_fequal),c_Com_Ocom_OSKIP),c_Natural_Oevalc(c_Com_Ocom_OSKIP))))) ),
inference(resolution,[status(thm)],[f26031,f21111]) ).
fof(f26264,plain,
( ~ sQ76_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f26257,f21225,f26030]) ).
fof(f26364,plain,
( sQ77_spl
| ~ c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,v_G,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),c_fequal),c_Com_Ocom_OSKIP),c_fequal)))) ),
inference(backward_demodulation,[status(thm)],[f12210,f26035]) ).
fof(f26417,plain,
( sQ77_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f26364,f21107]) ).
fof(f26418,plain,
sQ77_spl,
inference(contradiction_clause,[status(thm)],[f26417]) ).
fof(f26419,plain,
$false,
inference(sat_refutation,[status(thm)],[f21233,f26036,f26038,f26264,f26418]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW356+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.46 % Computer : n014.cluster.edu
% 0.19/0.46 % Model : x86_64 x86_64
% 0.19/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.46 % Memory : 8046.5625MB
% 0.19/0.46 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Mon Sep 21 09:48:50 UTC 2026
% 0.19/0.47 % CPUTime :
% 0.64/1.05 % Drodi V4.1.1
% 96.21/13.23 % Refutation found
% 96.21/13.23 % SZS status Theorem for theBenchmark: Theorem is valid
% 96.21/13.23 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.58/13.57 % Elapsed time: 13.087303 seconds
% 2.58/13.57 % CPU time: 97.974952 seconds
% 2.58/13.57 % Total memory used: 1.224 GB
% 2.58/13.57 % Net memory used: 1.198 GB
%------------------------------------------------------------------------------