%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW301+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/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:36 PM UTC 2026
% Result : Theorem 27.94s 4.60s
% Output : CNFRefutation 28.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 8
% Syntax : Number of formulae : 40 ( 8 unt; 3 def)
% Number of atoms : 108 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 114 ( 46 ~; 47 |; 9 &)
% ( 3 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 6 ( 5 usr; 4 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 7 con; 0-7 aty)
% Number of variables : 123 ( 113 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f16,axiom,
! [V_Pa_2,V_Qa_2,V_ca_2,V_P_H_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)),c_Hoare__Mirabelle_Otriple_Otriple(T_b,V_P_H_2,V_ca_2,V_Qa_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_Pa_2,B_Z),B_s))
=> hBOOL(hAPP(hAPP(V_P_H_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)),c_Hoare__Mirabelle_Otriple_Otriple(T_b,V_Pa_2,V_ca_2,V_Qa_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [V_Qa_2,V_Pa_2,V_Q_Ha_2,V_ca_2,V_P_H_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)),c_Hoare__Mirabelle_Otriple_Otriple(T_b,V_P_H_2,V_ca_2,V_Q_Ha_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_Pa_2,B_Z),B_s))
=> ! [B_s_H] :
( ! [B_Z_H] :
( hBOOL(hAPP(hAPP(V_P_H_2,B_Z_H),B_s))
=> hBOOL(hAPP(hAPP(V_Q_Ha_2,B_Z_H),B_s_H)) )
=> hBOOL(hAPP(hAPP(V_Qa_2,B_Z),B_s_H)) ) )
=> c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_b)),c_Hoare__Mirabelle_Otriple_Otriple(T_b,V_Pa_2,V_ca_2,V_Qa_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5222,hypothesis,
c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(t_a,v_P,v_c,v_Q_H)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5223,hypothesis,
! [B_Z,B_s] :
( hBOOL(hAPP(hAPP(v_Q_H,B_Z),B_s))
=> hBOOL(hAPP(hAPP(v_Q,B_Z),B_s)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5224,conjecture,
c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(t_a,v_P,v_c,v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5225,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(t_a,v_P,v_c,v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))),
inference(negated_conjecture,[status(cth)],[f5224]) ).
fof(f5263,plain,
! [V_Pa_2,V_Qa_2,V_ca_2,V_P_H_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)),c_Hoare__Mirabelle_Otriple_Otriple(T_b,V_Pa_2,V_ca_2,V_Qa_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_P_H_2,B_Z),B_s))
& hBOOL(hAPP(hAPP(V_Pa_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)),c_Hoare__Mirabelle_Otriple_Otriple(T_b,V_P_H_2,V_ca_2,V_Qa_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool)))) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f5264,plain,
! [V_Qa_2,V_ca_2,V_P_H_2,V_Ga_2,T_b] :
( ! [V_Pa_2] :
( c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_b)),c_Hoare__Mirabelle_Otriple_Otriple(T_b,V_Pa_2,V_ca_2,V_Qa_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_P_H_2,B_Z),B_s))
& hBOOL(hAPP(hAPP(V_Pa_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)),c_Hoare__Mirabelle_Otriple_Otriple(T_b,V_P_H_2,V_ca_2,V_Qa_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool)))) ),
inference(miniscoping,[status(thm)],[f5263]) ).
fof(f5265,plain,
! [V_Qa_2,V_ca_2,V_P_H_2,V_Ga_2,T_b] :
( ! [V_Pa_2] :
( c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_b)),c_Hoare__Mirabelle_Otriple_Otriple(T_b,V_Pa_2,V_ca_2,V_Qa_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool))))
| ( ~ hBOOL(hAPP(hAPP(V_P_H_2,sK1_skl(V_Pa_2,T_b,V_Ga_2,V_P_H_2,V_ca_2,V_Qa_2)),sK2_skl(V_Pa_2,T_b,V_Ga_2,V_P_H_2,V_ca_2,V_Qa_2)))
& hBOOL(hAPP(hAPP(V_Pa_2,sK1_skl(V_Pa_2,T_b,V_Ga_2,V_P_H_2,V_ca_2,V_Qa_2)),sK2_skl(V_Pa_2,T_b,V_Ga_2,V_P_H_2,V_ca_2,V_Qa_2))) ) )
| ~ c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_b)),c_Hoare__Mirabelle_Otriple_Otriple(T_b,V_P_H_2,V_ca_2,V_Qa_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(B_Z,sK1_skl(V_Pa_2,T_b,V_Ga_2,V_P_H_2,V_ca_2,V_Qa_2)),skolemize(B_s,sK2_skl(V_Pa_2,T_b,V_Ga_2,V_P_H_2,V_ca_2,V_Qa_2))],[f5264]) ).
fof(f5266,plain,
! [X0,X1,X2,X3,X4,X5] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),c_Hoare__Mirabelle_Otriple_Otriple(X0,X5,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)),c_Hoare__Mirabelle_Otriple_Otriple(X0,X2,X3,X4)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool)))) ),
inference(cnf_transformation,[status(thm)],[f5265]) ).
fof(f5267,plain,
! [X0,X1,X2,X3,X4,X5] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),c_Hoare__Mirabelle_Otriple_Otriple(X0,X5,X3,X4)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool))))
| ~ hBOOL(hAPP(hAPP(X2,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)),c_Hoare__Mirabelle_Otriple_Otriple(X0,X2,X3,X4)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool)))) ),
inference(cnf_transformation,[status(thm)],[f5265]) ).
fof(f5286,plain,
! [V_Qa_2,V_Pa_2,V_Q_Ha_2,V_ca_2,V_P_H_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)),c_Hoare__Mirabelle_Otriple_Otriple(T_b,V_Pa_2,V_ca_2,V_Qa_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool))))
| ? [B_Z,B_s] :
( ? [B_s_H] :
( ~ hBOOL(hAPP(hAPP(V_Qa_2,B_Z),B_s_H))
& ! [B_Z_H] :
( hBOOL(hAPP(hAPP(V_Q_Ha_2,B_Z_H),B_s_H))
| ~ hBOOL(hAPP(hAPP(V_P_H_2,B_Z_H),B_s)) ) )
& hBOOL(hAPP(hAPP(V_Pa_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)),c_Hoare__Mirabelle_Otriple_Otriple(T_b,V_P_H_2,V_ca_2,V_Q_Ha_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool)))) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f5287,plain,
! [V_Q_Ha_2,V_ca_2,V_P_H_2,V_Ga_2,T_b] :
( ! [V_Qa_2,V_Pa_2] :
( c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_b)),c_Hoare__Mirabelle_Otriple_Otriple(T_b,V_Pa_2,V_ca_2,V_Qa_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool))))
| ? [B_Z,B_s] :
( ? [B_s_H] :
( ~ hBOOL(hAPP(hAPP(V_Qa_2,B_Z),B_s_H))
& ! [B_Z_H] :
( hBOOL(hAPP(hAPP(V_Q_Ha_2,B_Z_H),B_s_H))
| ~ hBOOL(hAPP(hAPP(V_P_H_2,B_Z_H),B_s)) ) )
& hBOOL(hAPP(hAPP(V_Pa_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)),c_Hoare__Mirabelle_Otriple_Otriple(T_b,V_P_H_2,V_ca_2,V_Q_Ha_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool)))) ),
inference(miniscoping,[status(thm)],[f5286]) ).
fof(f5288,plain,
! [V_Q_Ha_2,V_ca_2,V_P_H_2,V_Ga_2,T_b] :
( ! [V_Qa_2,V_Pa_2] :
( c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_b)),c_Hoare__Mirabelle_Otriple_Otriple(T_b,V_Pa_2,V_ca_2,V_Qa_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool))))
| ( ~ hBOOL(hAPP(hAPP(V_Qa_2,sK3_skl(V_Pa_2,V_Qa_2,T_b,V_Ga_2,V_P_H_2,V_ca_2,V_Q_Ha_2)),sK5_skl(V_Pa_2,V_Qa_2,T_b,V_Ga_2,V_P_H_2,V_ca_2,V_Q_Ha_2)))
& ! [B_Z_H] :
( hBOOL(hAPP(hAPP(V_Q_Ha_2,B_Z_H),sK5_skl(V_Pa_2,V_Qa_2,T_b,V_Ga_2,V_P_H_2,V_ca_2,V_Q_Ha_2)))
| ~ hBOOL(hAPP(hAPP(V_P_H_2,B_Z_H),sK4_skl(V_Pa_2,V_Qa_2,T_b,V_Ga_2,V_P_H_2,V_ca_2,V_Q_Ha_2))) )
& hBOOL(hAPP(hAPP(V_Pa_2,sK3_skl(V_Pa_2,V_Qa_2,T_b,V_Ga_2,V_P_H_2,V_ca_2,V_Q_Ha_2)),sK4_skl(V_Pa_2,V_Qa_2,T_b,V_Ga_2,V_P_H_2,V_ca_2,V_Q_Ha_2))) ) )
| ~ c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_b)),c_Hoare__Mirabelle_Otriple_Otriple(T_b,V_P_H_2,V_ca_2,V_Q_Ha_2)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl]),skolemize(B_Z,sK3_skl(V_Pa_2,V_Qa_2,T_b,V_Ga_2,V_P_H_2,V_ca_2,V_Q_Ha_2)),skolemize(B_s,sK4_skl(V_Pa_2,V_Qa_2,T_b,V_Ga_2,V_P_H_2,V_ca_2,V_Q_Ha_2)),skolemize(B_s_H,sK5_skl(V_Pa_2,V_Qa_2,T_b,V_Ga_2,V_P_H_2,V_ca_2,V_Q_Ha_2))],[f5287]) ).
fof(f5289,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),c_Hoare__Mirabelle_Otriple_Otriple(X0,X5,X3,X6)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool))))
| hBOOL(hAPP(hAPP(X5,sK3_skl(X5,X6,X0,X1,X2,X3,X4)),sK4_skl(X5,X6,X0,X1,X2,X3,X4)))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),c_Hoare__Mirabelle_Otriple_Otriple(X0,X2,X3,X4)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool)))) ),
inference(cnf_transformation,[status(thm)],[f5288]) ).
fof(f5290,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),c_Hoare__Mirabelle_Otriple_Otriple(X0,X6,X3,X7)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool))))
| hBOOL(hAPP(hAPP(X4,X5),sK5_skl(X6,X7,X0,X1,X2,X3,X4)))
| ~ hBOOL(hAPP(hAPP(X2,X5),sK4_skl(X6,X7,X0,X1,X2,X3,X4)))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),c_Hoare__Mirabelle_Otriple_Otriple(X0,X2,X3,X4)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool)))) ),
inference(cnf_transformation,[status(thm)],[f5288]) ).
fof(f5291,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),c_Hoare__Mirabelle_Otriple_Otriple(X0,X6,X3,X5)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool))))
| ~ hBOOL(hAPP(hAPP(X5,sK3_skl(X6,X5,X0,X1,X2,X3,X4)),sK5_skl(X6,X5,X0,X1,X2,X3,X4)))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),c_Hoare__Mirabelle_Otriple_Otriple(X0,X2,X3,X4)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool)))) ),
inference(cnf_transformation,[status(thm)],[f5288]) ).
fof(f20037,plain,
c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(t_a,v_P,v_c,v_Q_H)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))),
inference(cnf_transformation,[status(thm)],[f5222]) ).
fof(f20038,plain,
! [B_Z,B_s] :
( hBOOL(hAPP(hAPP(v_Q,B_Z),B_s))
| ~ hBOOL(hAPP(hAPP(v_Q_H,B_Z),B_s)) ),
inference(pre_NNF_transformation,[status(thm)],[f5223]) ).
fof(f20039,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(v_Q,X0),X1))
| ~ hBOOL(hAPP(hAPP(v_Q_H,X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f20038]) ).
fof(f20040,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(t_a,v_P,v_c,v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))),
inference(cnf_transformation,[status(thm)],[f5225]) ).
fof(f20574,plain,
! [X0] :
( hBOOL(hAPP(hAPP(v_P,sK1_skl(v_P,t_a,v_G,X0,v_c,v_Q)),sK2_skl(v_P,t_a,v_G,X0,v_c,v_Q)))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(t_a,X0,v_c,v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) ),
inference(resolution,[status(thm)],[f5266,f20040]) ).
fof(f20588,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(X0,sK1_skl(v_P,t_a,v_G,X0,v_c,v_Q)),sK2_skl(v_P,t_a,v_G,X0,v_c,v_Q)))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(t_a,X0,v_c,v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) ),
inference(resolution,[status(thm)],[f5267,f20040]) ).
fof(f20605,definition,
( sQ8_spl
<=> c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(t_a,v_P,v_c,v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f20609,plain,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(t_a,v_P,v_c,v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(t_a,v_P,v_c,v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) ),
inference(resolution,[status(thm)],[f20574,f20588]) ).
fof(f20611,plain,
~ sQ8_spl,
inference(split_clause,[status(thm)],[f20609,f20605]) ).
fof(f20673,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(hAPP(X1,X2),sK5_skl(v_P,v_Q,t_a,v_G,X0,v_c,X1)))
| ~ hBOOL(hAPP(hAPP(X0,X2),sK4_skl(v_P,v_Q,t_a,v_G,X0,v_c,X1)))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(t_a,X0,v_c,X1)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) ),
inference(resolution,[status(thm)],[f5290,f20040]) ).
fof(f20685,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ hBOOL(hAPP(hAPP(v_Q_H,sK3_skl(X5,v_Q,X0,X1,X2,X3,X4)),sK5_skl(X5,v_Q,X0,X1,X2,X3,X4)))
| c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),c_Hoare__Mirabelle_Otriple_Otriple(X0,X5,X3,v_Q)),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)),c_Hoare__Mirabelle_Otriple_Otriple(X0,X2,X3,X4)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool)))) ),
inference(resolution,[status(thm)],[f5291,f20039]) ).
fof(f22748,plain,
! [X0] :
( hBOOL(hAPP(hAPP(v_Q_H,X0),sK5_skl(v_P,v_Q,t_a,v_G,v_P,v_c,v_Q_H)))
| ~ hBOOL(hAPP(hAPP(v_P,X0),sK4_skl(v_P,v_Q,t_a,v_G,v_P,v_c,v_Q_H))) ),
inference(resolution,[status(thm)],[f20037,f20673]) ).
fof(f23751,definition,
( sQ21_spl
<=> c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(t_a,v_P,v_c,v_Q_H)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f23753,plain,
( sQ21_spl
| ~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(t_a,v_P,v_c,v_Q_H)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) ),
inference(component_clause,[status(thm)],[f23751]) ).
fof(f29136,plain,
( ~ hBOOL(hAPP(hAPP(v_P,sK3_skl(v_P,v_Q,t_a,v_G,v_P,v_c,v_Q_H)),sK4_skl(v_P,v_Q,t_a,v_G,v_P,v_c,v_Q_H)))
| c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(t_a,v_P,v_c,v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(t_a,v_P,v_c,v_Q_H)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) ),
inference(resolution,[status(thm)],[f20685,f22748]) ).
fof(f29137,definition,
( sQ75_spl
<=> hBOOL(hAPP(hAPP(v_P,sK3_skl(v_P,v_Q,t_a,v_G,v_P,v_c,v_Q_H)),sK4_skl(v_P,v_Q,t_a,v_G,v_P,v_c,v_Q_H))) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f29139,plain,
( sQ75_spl
| ~ hBOOL(hAPP(hAPP(v_P,sK3_skl(v_P,v_Q,t_a,v_G,v_P,v_c,v_Q_H)),sK4_skl(v_P,v_Q,t_a,v_G,v_P,v_c,v_Q_H))) ),
inference(component_clause,[status(thm)],[f29137]) ).
fof(f29140,plain,
( ~ sQ75_spl
| sQ8_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f29136,f23751,f20605,f29137]) ).
fof(f29200,plain,
( sQ75_spl
| c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(t_a,v_P,v_c,v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(t_a,v_P,v_c,v_Q_H)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) ),
inference(resolution,[status(thm)],[f29139,f5289]) ).
fof(f29201,plain,
( sQ75_spl
| sQ8_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f29200,f23751,f20605,f29137]) ).
fof(f29202,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f23753,f20037]) ).
fof(f29203,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f29202]) ).
fof(f29204,plain,
$false,
inference(sat_refutation,[status(thm)],[f20611,f29140,f29201,f29203]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW301+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n014.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 09:46:19 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.79/1.05 % Drodi V4.1.1
% 27.94/4.60 % Refutation found
% 27.94/4.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 27.94/4.60 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 13.36/4.74 % Elapsed time: 4.359741 seconds
% 13.36/4.74 % CPU time: 29.327603 seconds
% 13.36/4.74 % Total memory used: 888.212 MB
% 13.36/4.74 % Net memory used: 873.322 MB
%------------------------------------------------------------------------------