%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW355+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 : 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:07:42 PM UTC 2026
% Result : Theorem 125.11s 16.87s
% Output : CNFRefutation 125.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 12
% Syntax : Number of formulae : 50 ( 25 unt; 3 def)
% Number of atoms : 91 ( 8 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 73 ( 32 ~; 29 |; 5 &)
% ( 3 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 4 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 5 con; 0-6 aty)
% Number of variables : 102 ( 98 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [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)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
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(f18,axiom,
! [V_a] : hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),V_a),V_a)),
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(f2233,axiom,
! [V_P_2,T_a] : hAPP(c_Set_OCollect(T_a),V_P_2) = V_P_2,
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(f5245,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(f5246,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)],[f5245]) ).
fof(f5251,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)],[f3]) ).
fof(f5253,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(f5266,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(f5267,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(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)))) ),
inference(cnf_transformation,[status(thm)],[f5266]) ).
fof(f5282,plain,
! [X0] : hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),X0),X0)),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f5335,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(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))))
| ? [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)],[f5335]) ).
fof(f5337,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))],[f5336]) ).
fof(f5338,plain,
! [X0,X1,X2,X3,X4,X5] :
( 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))))
| ~ 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)))) ),
inference(cnf_transformation,[status(thm)],[f5337]) ).
fof(f5339,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),X0)),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),X5)),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)],[f5337]) ).
fof(f12160,plain,
! [X0,X1] : X0 = hAPP(c_Set_OCollect(X1),X0),
inference(cnf_transformation,[status(thm)],[f2233]) ).
fof(f12211,plain,
! [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))),
inference(cnf_transformation,[status(thm)],[f2255]) ).
fof(f19935,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_fequal,X1),X0))
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f5228]) ).
fof(f19961,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)],[f5246]) ).
fof(f20789,plain,
! [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)),
inference(resolution,[status(thm)],[f5267,f19961]) ).
fof(f20961,plain,
! [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),X0)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_HOL_Obool))))
| hBOOL(hAPP(hAPP(X0,sK5_skl(c_Natural_Oevalc(c_Com_Ocom_OSKIP),tc_Com_Ostate,v_G,c_fequal,c_Com_Ocom_OSKIP,X0)),sK6_skl(c_Natural_Oevalc(c_Com_Ocom_OSKIP),tc_Com_Ostate,v_G,c_fequal,c_Com_Ocom_OSKIP,X0))) ),
inference(resolution,[status(thm)],[f5338,f20789]) ).
fof(f21002,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)],[f20961,f5253]) ).
fof(f21072,plain,
sK6_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),
inference(resolution,[status(thm)],[f21002,f19935]) ).
fof(f21222,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(paramodulation,[status(thm)],[f12211,f20789]) ).
fof(f21724,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(forward_demodulation,[status(thm)],[f12211,f5251]) ).
fof(f24931,plain,
! [X0,X1,X2] : c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(c_fequal,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X0),X2),c_Com_Ocom_OSKIP),X2))),
inference(backward_demodulation,[status(thm)],[f12160,f21724]) ).
fof(f24947,plain,
! [X0,X1] : hAPP(c_fequal,X0) = hAPP(hAPP(c_Set_Oinsert(X1),X0),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool))),
inference(backward_demodulation,[status(thm)],[f12160,f12211]) ).
fof(f25777,plain,
~ 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)))),
inference(backward_demodulation,[status(thm)],[f12160,f21222]) ).
fof(f27934,definition,
( sQ110_spl
<=> 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_fequal))) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f27936,plain,
( sQ110_spl
| ~ 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_fequal))) ),
inference(component_clause,[status(thm)],[f27934]) ).
fof(f27937,definition,
( sQ111_spl
<=> 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)))) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f27938,plain,
( ~ sQ111_spl
| 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)))) ),
inference(component_clause,[status(thm)],[f27937]) ).
fof(f27941,plain,
( ~ sQ111_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27938,f25777]) ).
fof(f27942,plain,
~ sQ111_spl,
inference(contradiction_clause,[status(thm)],[f27941]) ).
fof(f27943,plain,
( sQ110_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27936,f24931]) ).
fof(f27944,plain,
sQ110_spl,
inference(contradiction_clause,[status(thm)],[f27943]) ).
fof(f31179,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),X0)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X1),tc_HOL_Obool))))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,hAPP(c_fequal,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X1),X3),X4),X5)))
| ~ hBOOL(hAPP(hAPP(X0,sK5_skl(X0,X1,X2,X3,X4,X5)),sK6_skl(X0,X1,X2,X3,X4,X5))) ),
inference(forward_demodulation,[status(thm)],[f24947,f5339]) ).
fof(f31180,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(c_fequal,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X0),X2),X3),X5)))
| ~ hBOOL(hAPP(hAPP(X4,sK5_skl(X4,X0,X1,X2,X3,X5)),sK6_skl(X4,X0,X1,X2,X3,X5)))
| c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(c_fequal,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X0),X2),X3),X4))) ),
inference(forward_demodulation,[status(thm)],[f24947,f31179]) ).
fof(f31207,plain,
( ~ 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_fequal)))
| ~ 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)))) ),
inference(paramodulation,[status(thm)],[f21072,f31180]) ).
fof(f31208,definition,
( sQ167_spl
<=> 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))) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f31210,plain,
( sQ167_spl
| ~ 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))) ),
inference(component_clause,[status(thm)],[f31208]) ).
fof(f31211,plain,
( ~ sQ110_spl
| ~ sQ167_spl
| sQ111_spl ),
inference(split_clause,[status(thm)],[f31207,f27937,f31208,f27934]) ).
fof(f31212,plain,
( sQ167_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f31210,f5282]) ).
fof(f31213,plain,
sQ167_spl,
inference(contradiction_clause,[status(thm)],[f31212]) ).
fof(f31214,plain,
$false,
inference(sat_refutation,[status(thm)],[f27942,f27944,f31211,f31213]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW355+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n019.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.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 09:48:50 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.79/1.05 % Drodi V4.1.1
% 125.11/16.87 % Refutation found
% 125.11/16.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 125.11/16.87 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.75/17.22 % Elapsed time: 16.831403 seconds
% 4.75/17.22 % CPU time: 126.704525 seconds
% 4.75/17.22 % Total memory used: 1.399 GB
% 4.75/17.22 % Net memory used: 1.348 GB
%------------------------------------------------------------------------------