%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW307+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 : n001.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 218.34s 28.60s
% Output : CNFRefutation 219.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 12
% Syntax : Number of formulae : 49 ( 12 unt; 3 def)
% Number of atoms : 99 ( 4 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 93 ( 43 ~; 36 |; 5 &)
% ( 3 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 14 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 4 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 10 con; 0-6 aty)
% Number of variables : 122 ( 116 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f15,axiom,
! [V_Qa_2,V_ca_2,V_Ga_2,T_b,V_Pa_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,hAPP(c_COMBK(tc_fun(tc_Com_Ostate,tc_HOL_Obool),T_b),hAPP(hAPP(c_COMBC(tc_Com_Ostate,tc_Com_Ostate,tc_HOL_Obool),c_fequal),B_s)),V_ca_2,hAPP(c_COMBK(tc_fun(tc_Com_Ostate,tc_HOL_Obool),T_b),hAPP(V_Qa_2,B_Z)))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool)))) )
=> 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/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f2195,axiom,
! [V_y_2,V_x_2,T_c,T_b] : ~ hBOOL(hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_fun(T_c,tc_HOL_Obool))),V_x_2),V_y_2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5211,axiom,
! [V_R_2,V_Qa_2,V_Pa_2,T_d,T_b,T_c] : hAPP(hAPP(hAPP(c_COMBB(T_c,T_b,T_d),V_Pa_2),V_Qa_2),V_R_2) = hAPP(V_Pa_2,hAPP(V_Qa_2,V_R_2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5212,axiom,
! [V_R_2,V_Qa_2,V_Pa_2,T_b,T_d,T_c] : hAPP(hAPP(hAPP(c_COMBC(T_c,T_d,T_b),V_Pa_2),V_Qa_2),V_R_2) = hAPP(hAPP(V_Pa_2,V_R_2),V_Qa_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5221,axiom,
! [V_Qa_2,V_Pa_2] :
( hBOOL(V_Pa_2)
| ~ hBOOL(hAPP(hAPP(c_fconj,V_Pa_2),V_Qa_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5222,axiom,
! [V_Qa_2,V_Pa_2] :
( hBOOL(V_Qa_2)
| ~ hBOOL(hAPP(hAPP(c_fconj,V_Pa_2),V_Qa_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5229,hypothesis,
( hBOOL(v_C)
=> 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/sandbox2/benchmark/theBenchmark.p') ).
fof(f5230,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,hAPP(hAPP(c_COMBC(t_a,tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P))),v_C),v_c,v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5231,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,hAPP(hAPP(c_COMBC(t_a,tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P))),v_C),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)],[f5230]) ).
fof(f5270,plain,
! [V_Qa_2,V_ca_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] :
( ~ 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,hAPP(c_COMBK(tc_fun(tc_Com_Ostate,tc_HOL_Obool),T_b),hAPP(hAPP(c_COMBC(tc_Com_Ostate,tc_Com_Ostate,tc_HOL_Obool),c_fequal),B_s)),V_ca_2,hAPP(c_COMBK(tc_fun(tc_Com_Ostate,tc_HOL_Obool),T_b),hAPP(V_Qa_2,B_Z)))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool))))
& hBOOL(hAPP(hAPP(V_Pa_2,B_Z),B_s)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f5271,plain,
! [V_Qa_2,V_ca_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))))
| ( ~ 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,hAPP(c_COMBK(tc_fun(tc_Com_Ostate,tc_HOL_Obool),T_b),hAPP(hAPP(c_COMBC(tc_Com_Ostate,tc_Com_Ostate,tc_HOL_Obool),c_fequal),sK2_skl(V_Pa_2,T_b,V_Ga_2,V_ca_2,V_Qa_2))),V_ca_2,hAPP(c_COMBK(tc_fun(tc_Com_Ostate,tc_HOL_Obool),T_b),hAPP(V_Qa_2,sK1_skl(V_Pa_2,T_b,V_Ga_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_Pa_2,sK1_skl(V_Pa_2,T_b,V_Ga_2,V_ca_2,V_Qa_2)),sK2_skl(V_Pa_2,T_b,V_Ga_2,V_ca_2,V_Qa_2))) ) ),
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_ca_2,V_Qa_2)),skolemize(B_s,sK2_skl(V_Pa_2,T_b,V_Ga_2,V_ca_2,V_Qa_2))],[f5270]) ).
fof(f5272,plain,
! [X0,X1,X2,X3,X4] :
( c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X1)),c_Hoare__Mirabelle_Otriple_Otriple(X1,X0,X3,X4)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X1),tc_HOL_Obool))))
| hBOOL(hAPP(hAPP(X0,sK1_skl(X0,X1,X2,X3,X4)),sK2_skl(X0,X1,X2,X3,X4))) ),
inference(cnf_transformation,[status(thm)],[f5271]) ).
fof(f5289,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)],[f23]) ).
fof(f5290,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)],[f5289]) ).
fof(f5291,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,sK5_skl(V_Pa_2,T_b,V_Ga_2,V_P_H_2,V_ca_2,V_Qa_2)),sK6_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,sK5_skl(V_Pa_2,T_b,V_Ga_2,V_P_H_2,V_ca_2,V_Qa_2)),sK6_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,[sK5_skl,sK6_skl]),skolemize(B_Z,sK5_skl(V_Pa_2,T_b,V_Ga_2,V_P_H_2,V_ca_2,V_Qa_2)),skolemize(B_s,sK6_skl(V_Pa_2,T_b,V_Ga_2,V_P_H_2,V_ca_2,V_Qa_2))],[f5290]) ).
fof(f5292,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,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)),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)],[f5291]) ).
fof(f5293,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,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)),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)],[f5291]) ).
fof(f11886,plain,
! [X0,X1,X2,X3] : ~ hBOOL(hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_fun(X1,tc_HOL_Obool))),X2),X3)),
inference(cnf_transformation,[status(thm)],[f2195]) ).
fof(f19983,plain,
! [X0,X1,X2,X3,X4,X5] : hAPP(hAPP(hAPP(c_COMBB(X0,X1,X2),X3),X4),X5) = hAPP(X3,hAPP(X4,X5)),
inference(cnf_transformation,[status(thm)],[f5211]) ).
fof(f19984,plain,
! [X0,X1,X2,X3,X4,X5] : hAPP(hAPP(hAPP(c_COMBC(X0,X1,X2),X3),X4),X5) = hAPP(hAPP(X3,X5),X4),
inference(cnf_transformation,[status(thm)],[f5212]) ).
fof(f19993,plain,
! [V_Pa_2] :
( hBOOL(V_Pa_2)
| ! [V_Qa_2] : ~ hBOOL(hAPP(hAPP(c_fconj,V_Pa_2),V_Qa_2)) ),
inference(miniscoping,[status(thm)],[f5221]) ).
fof(f19994,plain,
! [X0,X1] :
( hBOOL(X0)
| ~ hBOOL(hAPP(hAPP(c_fconj,X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f19993]) ).
fof(f19995,plain,
! [V_Qa_2] :
( hBOOL(V_Qa_2)
| ! [V_Pa_2] : ~ hBOOL(hAPP(hAPP(c_fconj,V_Pa_2),V_Qa_2)) ),
inference(miniscoping,[status(thm)],[f5222]) ).
fof(f19996,plain,
! [X0,X1] :
( hBOOL(X1)
| ~ hBOOL(hAPP(hAPP(c_fconj,X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f19995]) ).
fof(f20009,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))))
| ~ hBOOL(v_C) ),
inference(pre_NNF_transformation,[status(thm)],[f5229]) ).
fof(f20010,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))))
| ~ hBOOL(v_C) ),
inference(cnf_transformation,[status(thm)],[f20009]) ).
fof(f20011,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,hAPP(hAPP(c_COMBC(t_a,tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P))),v_C),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)],[f5231]) ).
fof(f20337,definition,
( sQ8_spl
<=> hBOOL(v_C) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f20340,definition,
( sQ9_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,[sQ9_spl])],[split_symbol_definition]) ).
fof(f20343,plain,
( sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f20010,f20337,f20340]) ).
fof(f20708,plain,
! [X0] :
( hBOOL(hAPP(hAPP(hAPP(hAPP(c_COMBC(t_a,tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P))),v_C),sK5_skl(hAPP(hAPP(c_COMBC(t_a,tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P))),v_C),t_a,v_G,X0,v_c,v_Q)),sK6_skl(hAPP(hAPP(c_COMBC(t_a,tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P))),v_C),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)],[f5292,f20011]) ).
fof(f20878,plain,
! [X0] :
( hBOOL(hAPP(hAPP(hAPP(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P)),sK5_skl(hAPP(hAPP(c_COMBC(t_a,tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P))),v_C),t_a,v_G,X0,v_c,v_Q)),v_C),sK6_skl(hAPP(hAPP(c_COMBC(t_a,tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P))),v_C),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(forward_demodulation,[status(thm)],[f19984,f20708]) ).
fof(f20879,plain,
! [X0] :
( hBOOL(hAPP(hAPP(hAPP(c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P),sK5_skl(hAPP(hAPP(c_COMBC(t_a,tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P))),v_C),t_a,v_G,X0,v_c,v_Q))),v_C),sK6_skl(hAPP(hAPP(c_COMBC(t_a,tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P))),v_C),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(forward_demodulation,[status(thm)],[f19983,f20878]) ).
fof(f20880,plain,
! [X0] :
( hBOOL(hAPP(hAPP(hAPP(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P),sK5_skl(hAPP(hAPP(c_COMBC(t_a,tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P))),v_C),t_a,v_G,X0,v_c,v_Q)),sK6_skl(hAPP(hAPP(c_COMBC(t_a,tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P))),v_C),t_a,v_G,X0,v_c,v_Q)),v_C))
| ~ 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(forward_demodulation,[status(thm)],[f19984,f20879]) ).
fof(f20881,plain,
! [X0] :
( hBOOL(hAPP(hAPP(hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj),hAPP(v_P,sK5_skl(hAPP(hAPP(c_COMBC(t_a,tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P))),v_C),t_a,v_G,X0,v_c,v_Q))),sK6_skl(hAPP(hAPP(c_COMBC(t_a,tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P))),v_C),t_a,v_G,X0,v_c,v_Q)),v_C))
| ~ 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(forward_demodulation,[status(thm)],[f19983,f20880]) ).
fof(f20882,plain,
! [X0] :
( hBOOL(hAPP(hAPP(c_fconj,hAPP(hAPP(v_P,sK5_skl(hAPP(hAPP(c_COMBC(t_a,tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P))),v_C),t_a,v_G,X0,v_c,v_Q)),sK6_skl(hAPP(hAPP(c_COMBC(t_a,tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P))),v_C),t_a,v_G,X0,v_c,v_Q))),v_C))
| ~ 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(forward_demodulation,[status(thm)],[f19983,f20881]) ).
fof(f20883,plain,
! [X0] :
( hBOOL(hAPP(hAPP(v_P,sK5_skl(hAPP(hAPP(c_COMBC(t_a,tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P))),v_C),t_a,v_G,X0,v_c,v_Q)),sK6_skl(hAPP(hAPP(c_COMBC(t_a,tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P))),v_C),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)],[f20882,f19994]) ).
fof(f20884,plain,
! [X0] :
( hBOOL(v_C)
| ~ 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)],[f20882,f19996]) ).
fof(f20885,definition,
! [X0] :
( sQ16_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,X0,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,[sQ16_spl])],[split_symbol_definition]) ).
fof(f20886,plain,
! [X0] :
( ~ sQ16_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,X0,v_c,v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) ),
inference(component_clause,[status(thm)],[f20885]) ).
fof(f20888,plain,
( sQ8_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f20884,f20885,f20337]) ).
fof(f20991,plain,
! [X0] :
( ~ sQ16_spl
| hBOOL(hAPP(hAPP(X0,sK1_skl(X0,t_a,v_G,v_c,v_Q)),sK2_skl(X0,t_a,v_G,v_c,v_Q))) ),
inference(resolution,[status(thm)],[f20886,f5272]) ).
fof(f20996,plain,
( ~ sQ16_spl
| $false ),
inference(resolution,[status(thm)],[f20991,f11886]) ).
fof(f21005,plain,
~ sQ16_spl,
inference(contradiction_clause,[status(thm)],[f20996]) ).
fof(f21007,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(X0,sK5_skl(hAPP(hAPP(c_COMBC(t_a,tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P))),v_C),t_a,v_G,X0,v_c,v_Q)),sK6_skl(hAPP(hAPP(c_COMBC(t_a,tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),tc_fun(tc_HOL_Obool,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),t_a),c_COMBC(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_fun(tc_HOL_Obool,tc_HOL_Obool)),t_a),hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj)),v_P))),v_C),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)],[f20011,f5293]) ).
fof(f31341,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)],[f20883,f21007]) ).
fof(f31344,plain,
~ sQ9_spl,
inference(split_clause,[status(thm)],[f31341,f20340]) ).
fof(f31346,plain,
$false,
inference(sat_refutation,[status(thm)],[f20343,f20888,f21005,f31344]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW307+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.35 % Computer : n001.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 09:52:30 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.78/1.03 % Drodi V4.1.1
% 218.34/28.60 % Refutation found
% 218.34/28.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 218.34/28.60 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 24.41/28.89 % Elapsed time: 28.518164 seconds
% 24.41/28.89 % CPU time: 220.312218 seconds
% 24.41/28.89 % Total memory used: 1.586 GB
% 24.41/28.89 % Net memory used: 1.496 GB
%------------------------------------------------------------------------------