%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW395+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 : n026.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:47 PM UTC 2026
% Result : Theorem 76.58s 11.14s
% Output : CNFRefutation 76.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 9
% Syntax : Number of formulae : 45 ( 20 unt; 2 def)
% Number of atoms : 99 ( 23 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 87 ( 33 ~; 30 |; 13 &)
% ( 3 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 3 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 11 con; 0-3 aty)
% Number of variables : 102 ( 95 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f24,axiom,
! [V_x_2,V_A_2,V_y_2,T_b] :
( hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(T_b),V_y_2),V_A_2),V_x_2))
<=> ( hBOOL(hAPP(V_A_2,V_x_2))
| V_y_2 = V_x_2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [T_b,V_a_2,V_Pa_2] :
( ( ~ hBOOL(hAPP(V_Pa_2,V_a_2))
=> hAPP(c_Set_OCollect(T_b),hAPP(hAPP(c_COMBS(T_b,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),T_b),c_fconj),hAPP(c_fequal,V_a_2))),V_Pa_2)) = c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_HOL_Obool)) )
& ( hBOOL(hAPP(V_Pa_2,V_a_2))
=> hAPP(c_Set_OCollect(T_b),hAPP(hAPP(c_COMBS(T_b,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),T_b),c_fconj),hAPP(c_fequal,V_a_2))),V_Pa_2)) = hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_HOL_Obool))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [V_Pa_2,T_b] : hAPP(c_Set_OCollect(T_b),V_Pa_2) = V_Pa_2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [V_a_2,T_b] : hAPP(c_Set_OCollect(T_b),hAPP(hAPP(c_COMBC(T_b,T_b,tc_HOL_Obool),c_fequal),V_a_2)) = hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_HOL_Obool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5223,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(f5241,hypothesis,
! [B_s_H] : c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_HOL_Obool),t_a),hAPP(c_COMBS(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj),hAPP(c_fequal,B_s_H)))),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(f5242,conjecture,
! [B_Z,B_s] :
( hBOOL(hAPP(hAPP(v_P,B_Z),B_s))
=> ? [B_P_H,B_Q_H] :
( ! [B_s_H] :
( ! [B_Z_H] :
( hBOOL(hAPP(hAPP(B_P_H,B_Z_H),B_s))
=> hBOOL(hAPP(hAPP(B_Q_H,B_Z_H),B_s_H)) )
=> hBOOL(hAPP(hAPP(v_Q,B_Z),B_s_H)) )
& c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),B_P_H),v_c),B_Q_H)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5243,negated_conjecture,
~ ! [B_Z,B_s] :
( hBOOL(hAPP(hAPP(v_P,B_Z),B_s))
=> ? [B_P_H,B_Q_H] :
( ! [B_s_H] :
( ! [B_Z_H] :
( hBOOL(hAPP(hAPP(B_P_H,B_Z_H),B_s))
=> hBOOL(hAPP(hAPP(B_Q_H,B_Z_H),B_s_H)) )
=> hBOOL(hAPP(hAPP(v_Q,B_Z),B_s_H)) )
& c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),B_P_H),v_c),B_Q_H)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) ) ),
inference(negated_conjecture,[status(cth)],[f5242]) ).
fof(f5302,plain,
! [V_x_2,V_A_2,V_y_2,T_b] :
( ( ( ~ hBOOL(hAPP(V_A_2,V_x_2))
& V_y_2 != V_x_2 )
| hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(T_b),V_y_2),V_A_2),V_x_2)) )
& ( hBOOL(hAPP(V_A_2,V_x_2))
| V_y_2 = V_x_2
| ~ hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(T_b),V_y_2),V_A_2),V_x_2)) ) ),
inference(NNF_transformation,[status(thm)],[f24]) ).
fof(f5303,plain,
( ! [V_x_2,V_A_2,V_y_2] :
( ( ~ hBOOL(hAPP(V_A_2,V_x_2))
& V_y_2 != V_x_2 )
| ! [T_b] : hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(T_b),V_y_2),V_A_2),V_x_2)) )
& ! [V_x_2,V_A_2,V_y_2] :
( hBOOL(hAPP(V_A_2,V_x_2))
| V_y_2 = V_x_2
| ! [T_b] : ~ hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(T_b),V_y_2),V_A_2),V_x_2)) ) ),
inference(miniscoping,[status(thm)],[f5302]) ).
fof(f5305,plain,
! [X0,X1,X2,X3] :
( X1 != X3
| hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(X0),X1),X2),X3)) ),
inference(cnf_transformation,[status(thm)],[f5303]) ).
fof(f5339,plain,
! [T_b,V_a_2,V_Pa_2] :
( ( hAPP(c_Set_OCollect(T_b),hAPP(hAPP(c_COMBS(T_b,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),T_b),c_fconj),hAPP(c_fequal,V_a_2))),V_Pa_2)) = c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_HOL_Obool))
| hBOOL(hAPP(V_Pa_2,V_a_2)) )
& ( hAPP(c_Set_OCollect(T_b),hAPP(hAPP(c_COMBS(T_b,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),T_b),c_fconj),hAPP(c_fequal,V_a_2))),V_Pa_2)) = hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_HOL_Obool)))
| ~ hBOOL(hAPP(V_Pa_2,V_a_2)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f5340,plain,
( ! [V_a_2,V_Pa_2] :
( ! [T_b] : hAPP(c_Set_OCollect(T_b),hAPP(hAPP(c_COMBS(T_b,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),T_b),c_fconj),hAPP(c_fequal,V_a_2))),V_Pa_2)) = c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_HOL_Obool))
| hBOOL(hAPP(V_Pa_2,V_a_2)) )
& ! [V_a_2,V_Pa_2] :
( ! [T_b] : hAPP(c_Set_OCollect(T_b),hAPP(hAPP(c_COMBS(T_b,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),T_b),c_fconj),hAPP(c_fequal,V_a_2))),V_Pa_2)) = hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_HOL_Obool)))
| ~ hBOOL(hAPP(V_Pa_2,V_a_2)) ) ),
inference(miniscoping,[status(thm)],[f5339]) ).
fof(f5341,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(X2,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(hAPP(c_COMBS(X0,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),X0),c_fconj),hAPP(c_fequal,X1))),X2)) ),
inference(cnf_transformation,[status(thm)],[f5340]) ).
fof(f5343,plain,
! [X0,X1] : hAPP(c_Set_OCollect(X0),X1) = X1,
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f5357,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(hAPP(c_COMBC(X0,X0,tc_HOL_Obool),c_fequal),X1)),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f19881,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)],[f5223]) ).
fof(f19907,plain,
! [X0] : c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_HOL_Obool),t_a),hAPP(c_COMBS(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj),hAPP(c_fequal,X0)))),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)],[f5241]) ).
fof(f19908,plain,
? [B_Z,B_s] :
( ! [B_P_H,B_Q_H] :
( ? [B_s_H] :
( ~ hBOOL(hAPP(hAPP(v_Q,B_Z),B_s_H))
& ! [B_Z_H] :
( hBOOL(hAPP(hAPP(B_Q_H,B_Z_H),B_s_H))
| ~ hBOOL(hAPP(hAPP(B_P_H,B_Z_H),B_s)) ) )
| ~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),B_P_H),v_c),B_Q_H)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) )
& hBOOL(hAPP(hAPP(v_P,B_Z),B_s)) ),
inference(pre_NNF_transformation,[status(thm)],[f5243]) ).
fof(f19909,plain,
( ! [B_P_H,B_Q_H] :
( ( ~ hBOOL(hAPP(hAPP(v_Q,sK524_skl),sK526_skl(B_Q_H,B_P_H)))
& ! [B_Z_H] :
( hBOOL(hAPP(hAPP(B_Q_H,B_Z_H),sK526_skl(B_Q_H,B_P_H)))
| ~ hBOOL(hAPP(hAPP(B_P_H,B_Z_H),sK525_skl)) ) )
| ~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),B_P_H),v_c),B_Q_H)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) )
& hBOOL(hAPP(hAPP(v_P,sK524_skl),sK525_skl)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK524_skl,sK525_skl,sK526_skl]),skolemize(B_Z,sK524_skl),skolemize(B_s,sK525_skl),skolemize(B_s_H,sK526_skl(B_Q_H,B_P_H))],[f19908]) ).
fof(f19910,plain,
hBOOL(hAPP(hAPP(v_P,sK524_skl),sK525_skl)),
inference(cnf_transformation,[status(thm)],[f19909]) ).
fof(f19911,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(hAPP(X2,X1),sK525_skl))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),X2),v_c),X0)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))
| hBOOL(hAPP(hAPP(X0,X1),sK526_skl(X0,X2))) ),
inference(cnf_transformation,[status(thm)],[f19909]) ).
fof(f19912,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(v_Q,sK524_skl),sK526_skl(X1,X0)))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(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(cnf_transformation,[status(thm)],[f19909]) ).
fof(f20218,plain,
! [X0,X1,X2] : hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(X0),X1),X2),X1)),
inference(destructive_equality_resolution,[status(thm)],[f5305]) ).
fof(f20764,plain,
! [X0] : ~ hBOOL(hAPP(hAPP(v_Q,sK524_skl),sK526_skl(v_Q,hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_HOL_Obool),t_a),hAPP(c_COMBS(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj),hAPP(c_fequal,X0)))),v_P)))),
inference(resolution,[status(thm)],[f19907,f19912]) ).
fof(f21077,plain,
! [X0] : hAPP(hAPP(c_Set_Oinsert(X0),sK525_skl),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool))) = hAPP(c_Set_OCollect(X0),hAPP(hAPP(c_COMBS(X0,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),X0),c_fconj),hAPP(c_fequal,sK525_skl))),hAPP(v_P,sK524_skl))),
inference(resolution,[status(thm)],[f5341,f19910]) ).
fof(f23675,plain,
! [X0] : hAPP(hAPP(c_COMBS(X0,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),X0),c_fconj),hAPP(c_fequal,sK525_skl))),hAPP(v_P,sK524_skl)) = hAPP(hAPP(c_Set_Oinsert(X0),sK525_skl),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool))),
inference(backward_demodulation,[status(thm)],[f5343,f21077]) ).
fof(f29040,plain,
! [X0] : c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_COMBC(tc_Hoare__Mirabelle_Otriple(t_a),tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool),c_fequal),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_HOL_Obool),t_a),hAPP(c_COMBS(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj),hAPP(c_fequal,X0)))),v_P)),v_c),v_Q))),
inference(backward_demodulation,[status(thm)],[f29067,f19907]) ).
fof(f29041,plain,
! [X0,X1,X2] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_COMBC(tc_Hoare__Mirabelle_Otriple(t_a),tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool),c_fequal),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),X0),v_c),X2)))
| hBOOL(hAPP(hAPP(X2,X1),sK526_skl(X2,X0)))
| ~ hBOOL(hAPP(hAPP(X0,X1),sK525_skl)) ),
inference(backward_demodulation,[status(thm)],[f29067,f19911]) ).
fof(f29055,plain,
! [X0] : hAPP(hAPP(c_COMBS(X0,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),X0),c_fconj),hAPP(c_fequal,sK525_skl))),hAPP(v_P,sK524_skl)) = hAPP(hAPP(c_COMBC(X0,X0,tc_HOL_Obool),c_fequal),sK525_skl),
inference(backward_demodulation,[status(thm)],[f29067,f23675]) ).
fof(f29067,plain,
! [X0,X1] : hAPP(hAPP(c_Set_Oinsert(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool))) = hAPP(hAPP(c_COMBC(X0,X0,tc_HOL_Obool),c_fequal),X1),
inference(forward_demodulation,[status(thm)],[f5343,f5357]) ).
fof(f29087,plain,
! [X0,X1] : hBOOL(hAPP(hAPP(hAPP(c_COMBC(X0,X0,tc_HOL_Obool),c_fequal),X1),X1)),
inference(paramodulation,[status(thm)],[f29067,f20218]) ).
fof(f31694,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_HOL_Obool),t_a),hAPP(c_COMBS(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj),hAPP(c_fequal,X1)))),v_P),X0),sK525_skl))
| hBOOL(hAPP(hAPP(v_Q,X0),sK526_skl(v_Q,hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_HOL_Obool),t_a),hAPP(c_COMBS(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj),hAPP(c_fequal,X1)))),v_P)))) ),
inference(resolution,[status(thm)],[f29041,f29040]) ).
fof(f35385,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(v_Q,X1),sK526_skl(v_Q,hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_HOL_Obool),t_a),hAPP(c_COMBS(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj),hAPP(c_fequal,X0)))),v_P))))
| ~ hBOOL(hAPP(hAPP(hAPP(c_COMBS(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj),hAPP(c_fequal,X0))),hAPP(v_P,X1)),sK525_skl)) ),
inference(backward_demodulation,[status(thm)],[f19881,f31694]) ).
fof(f35857,plain,
( hBOOL(hAPP(hAPP(v_Q,sK524_skl),sK526_skl(v_Q,hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_HOL_Obool),t_a),hAPP(c_COMBS(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj),hAPP(c_fequal,sK525_skl)))),v_P))))
| ~ hBOOL(hAPP(hAPP(hAPP(c_COMBC(tc_Com_Ostate,tc_Com_Ostate,tc_HOL_Obool),c_fequal),sK525_skl),sK525_skl)) ),
inference(paramodulation,[status(thm)],[f29055,f35385]) ).
fof(f35859,definition,
( sQ389_spl
<=> hBOOL(hAPP(hAPP(hAPP(c_COMBC(tc_Com_Ostate,tc_Com_Ostate,tc_HOL_Obool),c_fequal),sK525_skl),sK525_skl)) ),
introduced(definition,[new_symbols(definition,[sQ389_spl])],[split_symbol_definition]) ).
fof(f35861,plain,
( sQ389_spl
| ~ hBOOL(hAPP(hAPP(hAPP(c_COMBC(tc_Com_Ostate,tc_Com_Ostate,tc_HOL_Obool),c_fequal),sK525_skl),sK525_skl)) ),
inference(component_clause,[status(thm)],[f35859]) ).
fof(f35862,definition,
( sQ390_spl
<=> hBOOL(hAPP(hAPP(v_Q,sK524_skl),sK526_skl(v_Q,hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_HOL_Obool),t_a),hAPP(c_COMBS(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj),hAPP(c_fequal,sK525_skl)))),v_P)))) ),
introduced(definition,[new_symbols(definition,[sQ390_spl])],[split_symbol_definition]) ).
fof(f35863,plain,
( ~ sQ390_spl
| hBOOL(hAPP(hAPP(v_Q,sK524_skl),sK526_skl(v_Q,hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_HOL_Obool),tc_fun(tc_Com_Ostate,tc_HOL_Obool),t_a),hAPP(c_COMBS(tc_Com_Ostate,tc_HOL_Obool,tc_HOL_Obool),hAPP(hAPP(c_COMBB(tc_HOL_Obool,tc_fun(tc_HOL_Obool,tc_HOL_Obool),tc_Com_Ostate),c_fconj),hAPP(c_fequal,sK525_skl)))),v_P)))) ),
inference(component_clause,[status(thm)],[f35862]) ).
fof(f35865,plain,
( sQ390_spl
| ~ sQ389_spl ),
inference(split_clause,[status(thm)],[f35857,f35859,f35862]) ).
fof(f35867,plain,
( ~ sQ390_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f35863,f20764]) ).
fof(f35868,plain,
~ sQ390_spl,
inference(contradiction_clause,[status(thm)],[f35867]) ).
fof(f35869,plain,
( sQ389_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f35861,f29087]) ).
fof(f35870,plain,
sQ389_spl,
inference(contradiction_clause,[status(thm)],[f35869]) ).
fof(f35871,plain,
$false,
inference(sat_refutation,[status(thm)],[f35865,f35868,f35870]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW395+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n026.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 09:53:07 UTC 2026
% 0.18/0.45 % CPUTime :
% 1.27/1.53 % Drodi V4.1.1
% 76.58/11.14 % Refutation found
% 76.58/11.14 % SZS status Theorem for theBenchmark: Theorem is valid
% 76.58/11.14 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 9.70/11.44 % Elapsed time: 10.955612 seconds
% 9.70/11.44 % CPU time: 77.732501 seconds
% 9.70/11.44 % Total memory used: 1.079 GB
% 9.70/11.44 % Net memory used: 1.050 GB
%------------------------------------------------------------------------------