%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : TOP027+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:53:26 PM UTC 2026
% Result : Theorem 145.01s 25.38s
% Output : CNFRefutation 67.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 28
% Syntax : Number of formulae : 110 ( 31 unt; 16 def)
% Number of atoms : 265 ( 19 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 260 ( 105 ~; 85 |; 38 &)
% ( 17 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 35 ( 33 usr; 17 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-3 aty)
% Number of variables : 59 ( 52 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f29,axiom,
! [A] :
( A = k1_xboole_0
<=> ! [B] : ~ r2_hidden(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [A] : r1_tarski(k1_xboole_0,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f134,axiom,
! [A] : r1_xboole_0(A,k1_xboole_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f685,axiom,
( v1_relat_1(k1_xboole_0)
& v1_xboole_0(k1_xboole_0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1265,axiom,
? [A] :
( v3_ordinal1(A)
& v2_ordinal1(A)
& v1_ordinal1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2650,axiom,
( ~ v1_xboole_0(k5_ordinal2)
& v3_ordinal1(k5_ordinal2)
& v2_ordinal1(k5_ordinal2)
& v1_ordinal1(k5_ordinal2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2878,axiom,
( v4_ordinal2(k4_ordinal2)
& v3_ordinal1(k4_ordinal2)
& v2_ordinal1(k4_ordinal2)
& v1_ordinal1(k4_ordinal2)
& ~ v1_xboole_0(k4_ordinal2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3568,axiom,
? [A] :
( v1_xreal_0(A)
& v1_xcmplx_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18338,axiom,
! [A,B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& l1_pre_topc(A)
& v2_pre_topc(A) )
=> v3_pre_topc(k1_tops_1(A,B),A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18475,axiom,
! [A,B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& l1_pre_topc(A) )
=> m1_subset_1(k1_tops_1(A,B),k1_zfmisc_1(u1_struct_0(A))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34386,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v1_tsp_2(B,A)
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
=> ( v3_pre_topc(C,A)
=> C = k3_tex_4(A,k5_subset_1(u1_struct_0(A),B,C)) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34388,conjecture,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v1_tsp_2(B,A)
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
=> k1_tops_1(A,C) = k3_tex_4(A,k5_subset_1(u1_struct_0(A),B,k1_tops_1(A,C))) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34389,negated_conjecture,
~ ! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v1_tsp_2(B,A)
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
=> k1_tops_1(A,C) = k3_tex_4(A,k5_subset_1(u1_struct_0(A),B,k1_tops_1(A,C))) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f34388]) ).
fof(f34479,plain,
! [A] :
( ( ? [B] : r2_hidden(B,A)
| A = k1_xboole_0 )
& ( ! [B] : ~ r2_hidden(B,A)
| A != k1_xboole_0 ) ),
inference(NNF_transformation,[status(thm)],[f29]) ).
fof(f34480,plain,
( ! [A] :
( ? [B] : r2_hidden(B,A)
| A = k1_xboole_0 )
& ! [A] :
( ! [B] : ~ r2_hidden(B,A)
| A != k1_xboole_0 ) ),
inference(miniscoping,[status(thm)],[f34479]) ).
fof(f34481,plain,
( ! [A] :
( r2_hidden(sK22_skl(A),A)
| A = k1_xboole_0 )
& ! [A] :
( ! [B] : ~ r2_hidden(B,A)
| A != k1_xboole_0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(B,sK22_skl(A))],[f34480]) ).
fof(f34483,plain,
! [X0] :
( r2_hidden(sK22_skl(X0),X0)
| X0 = k1_xboole_0 ),
inference(cnf_transformation,[status(thm)],[f34481]) ).
fof(f34618,plain,
! [X0] : r1_tarski(k1_xboole_0,X0),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f34737,plain,
! [X0] : r1_xboole_0(X0,k1_xboole_0),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f35877,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[status(thm)],[f685]) ).
fof(f37339,plain,
( v3_ordinal1(sK244_skl)
& v2_ordinal1(sK244_skl)
& v1_ordinal1(sK244_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK244_skl]),skolemize(A,sK244_skl)],[f1265]) ).
fof(f37342,plain,
v3_ordinal1(sK244_skl),
inference(cnf_transformation,[status(thm)],[f37339]) ).
fof(f41556,plain,
~ v1_xboole_0(k5_ordinal2),
inference(cnf_transformation,[status(thm)],[f2650]) ).
fof(f42507,plain,
v4_ordinal2(k4_ordinal2),
inference(cnf_transformation,[status(thm)],[f2878]) ).
fof(f44692,plain,
( v1_xreal_0(sK1076_skl)
& v1_xcmplx_0(sK1076_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1076_skl]),skolemize(A,sK1076_skl)],[f3568]) ).
fof(f44694,plain,
v1_xreal_0(sK1076_skl),
inference(cnf_transformation,[status(thm)],[f44692]) ).
fof(f93923,plain,
! [A,B] :
( v3_pre_topc(k1_tops_1(A,B),A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A) ),
inference(pre_NNF_transformation,[status(thm)],[f18338]) ).
fof(f93924,plain,
! [X0,X1] :
( v3_pre_topc(k1_tops_1(X0,X1),X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0) ),
inference(cnf_transformation,[status(thm)],[f93923]) ).
fof(f94280,plain,
! [A,B] :
( m1_subset_1(k1_tops_1(A,B),k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_pre_topc(A) ),
inference(pre_NNF_transformation,[status(thm)],[f18475]) ).
fof(f94281,plain,
! [X0,X1] :
( m1_subset_1(k1_tops_1(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(thm)],[f94280]) ).
fof(f152577,plain,
! [A] :
( ! [B] :
( ! [C] :
( C = k3_tex_4(A,k5_subset_1(u1_struct_0(A),B,C))
| ~ v3_pre_topc(C,A)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) )
| ~ v1_tsp_2(B,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f34386]) ).
fof(f152578,plain,
! [X0,X1,X2] :
( X2 = k3_tex_4(X0,k5_subset_1(u1_struct_0(X0),X1,X2))
| ~ v3_pre_topc(X2,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_tsp_2(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f152577]) ).
fof(f152581,plain,
? [A] :
( ? [B] :
( ? [C] :
( k1_tops_1(A,C) != k3_tex_4(A,k5_subset_1(u1_struct_0(A),B,k1_tops_1(A,C)))
& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) )
& v1_tsp_2(B,A)
& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
& l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f34389]) ).
fof(f152582,plain,
( k1_tops_1(sK11971_skl,sK11973_skl) != k3_tex_4(sK11971_skl,k5_subset_1(u1_struct_0(sK11971_skl),sK11972_skl,k1_tops_1(sK11971_skl,sK11973_skl)))
& m1_subset_1(sK11973_skl,k1_zfmisc_1(u1_struct_0(sK11971_skl)))
& v1_tsp_2(sK11972_skl,sK11971_skl)
& m1_subset_1(sK11972_skl,k1_zfmisc_1(u1_struct_0(sK11971_skl)))
& l1_pre_topc(sK11971_skl)
& v2_pre_topc(sK11971_skl)
& ~ v3_struct_0(sK11971_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11971_skl,sK11972_skl,sK11973_skl]),skolemize(A,sK11971_skl),skolemize(B,sK11972_skl),skolemize(C,sK11973_skl)],[f152581]) ).
fof(f152583,plain,
~ v3_struct_0(sK11971_skl),
inference(cnf_transformation,[status(thm)],[f152582]) ).
fof(f152584,plain,
v2_pre_topc(sK11971_skl),
inference(cnf_transformation,[status(thm)],[f152582]) ).
fof(f152585,plain,
l1_pre_topc(sK11971_skl),
inference(cnf_transformation,[status(thm)],[f152582]) ).
fof(f152586,plain,
m1_subset_1(sK11972_skl,k1_zfmisc_1(u1_struct_0(sK11971_skl))),
inference(cnf_transformation,[status(thm)],[f152582]) ).
fof(f152587,plain,
v1_tsp_2(sK11972_skl,sK11971_skl),
inference(cnf_transformation,[status(thm)],[f152582]) ).
fof(f152588,plain,
m1_subset_1(sK11973_skl,k1_zfmisc_1(u1_struct_0(sK11971_skl))),
inference(cnf_transformation,[status(thm)],[f152582]) ).
fof(f152589,plain,
k1_tops_1(sK11971_skl,sK11973_skl) != k3_tex_4(sK11971_skl,k5_subset_1(u1_struct_0(sK11971_skl),sK11972_skl,k1_tops_1(sK11971_skl,sK11973_skl))),
inference(cnf_transformation,[status(thm)],[f152582]) ).
fof(f170733,definition,
! [X1] :
( sQ57_spl
<=> ~ v3_ordinal1(X1) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f170734,plain,
! [X0] :
( ~ sQ57_spl
| ~ v3_ordinal1(X0) ),
inference(component_clause,[status(thm)],[f170733]) ).
fof(f172301,definition,
! [X1] :
( sQ468_spl
<=> ~ v1_xreal_0(X1) ),
introduced(definition,[new_symbols(definition,[sQ468_spl])],[split_symbol_definition]) ).
fof(f172302,plain,
! [X0] :
( ~ sQ468_spl
| ~ v1_xreal_0(X0) ),
inference(component_clause,[status(thm)],[f172301]) ).
fof(f172348,definition,
! [X1] :
( sQ481_spl
<=> ~ v4_ordinal2(X1) ),
introduced(definition,[new_symbols(definition,[sQ481_spl])],[split_symbol_definition]) ).
fof(f172349,plain,
! [X0] :
( ~ sQ481_spl
| ~ v4_ordinal2(X0) ),
inference(component_clause,[status(thm)],[f172348]) ).
fof(f183735,definition,
( sQ2894_spl
<=> l1_pre_topc(sK11971_skl) ),
introduced(definition,[new_symbols(definition,[sQ2894_spl])],[split_symbol_definition]) ).
fof(f183737,plain,
( sQ2894_spl
| ~ l1_pre_topc(sK11971_skl) ),
inference(component_clause,[status(thm)],[f183735]) ).
fof(f183746,plain,
( sQ2894_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f183737,f152585]) ).
fof(f183747,plain,
sQ2894_spl,
inference(contradiction_clause,[status(thm)],[f183746]) ).
fof(f183836,definition,
( sQ2897_spl
<=> v2_pre_topc(sK11971_skl) ),
introduced(definition,[new_symbols(definition,[sQ2897_spl])],[split_symbol_definition]) ).
fof(f183838,plain,
( sQ2897_spl
| ~ v2_pre_topc(sK11971_skl) ),
inference(component_clause,[status(thm)],[f183836]) ).
fof(f183853,plain,
( sQ2897_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f183838,f152584]) ).
fof(f183854,plain,
sQ2897_spl,
inference(contradiction_clause,[status(thm)],[f183853]) ).
fof(f184241,definition,
( sQ2923_spl
<=> m1_subset_1(sK11972_skl,k1_zfmisc_1(u1_struct_0(sK11971_skl))) ),
introduced(definition,[new_symbols(definition,[sQ2923_spl])],[split_symbol_definition]) ).
fof(f184243,plain,
( sQ2923_spl
| ~ m1_subset_1(sK11972_skl,k1_zfmisc_1(u1_struct_0(sK11971_skl))) ),
inference(component_clause,[status(thm)],[f184241]) ).
fof(f184339,plain,
( sQ2923_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f184243,f152586]) ).
fof(f184340,plain,
sQ2923_spl,
inference(contradiction_clause,[status(thm)],[f184339]) ).
fof(f184818,definition,
( sQ2966_spl
<=> v3_struct_0(sK11971_skl) ),
introduced(definition,[new_symbols(definition,[sQ2966_spl])],[split_symbol_definition]) ).
fof(f184819,plain,
( ~ sQ2966_spl
| v3_struct_0(sK11971_skl) ),
inference(component_clause,[status(thm)],[f184818]) ).
fof(f184836,plain,
( ~ sQ2966_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f184819,f152583]) ).
fof(f184837,plain,
~ sQ2966_spl,
inference(contradiction_clause,[status(thm)],[f184836]) ).
fof(f184929,definition,
( sQ2972_spl
<=> m1_subset_1(sK11973_skl,k1_zfmisc_1(u1_struct_0(sK11971_skl))) ),
introduced(definition,[new_symbols(definition,[sQ2972_spl])],[split_symbol_definition]) ).
fof(f184931,plain,
( sQ2972_spl
| ~ m1_subset_1(sK11973_skl,k1_zfmisc_1(u1_struct_0(sK11971_skl))) ),
inference(component_clause,[status(thm)],[f184929]) ).
fof(f185083,plain,
( sQ2972_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f184931,f152588]) ).
fof(f185084,plain,
sQ2972_spl,
inference(contradiction_clause,[status(thm)],[f185083]) ).
fof(f185961,definition,
( sQ3108_spl
<=> k1_xboole_0 = k1_xboole_0 ),
introduced(definition,[new_symbols(definition,[sQ3108_spl])],[split_symbol_definition]) ).
fof(f185963,plain,
( sQ3108_spl
| k1_xboole_0 != k1_xboole_0 ),
inference(component_clause,[status(thm)],[f185961]) ).
fof(f187631,definition,
( sQ3207_spl
<=> v1_tsp_2(sK11972_skl,sK11971_skl) ),
introduced(definition,[new_symbols(definition,[sQ3207_spl])],[split_symbol_definition]) ).
fof(f187633,plain,
( sQ3207_spl
| ~ v1_tsp_2(sK11972_skl,sK11971_skl) ),
inference(component_clause,[status(thm)],[f187631]) ).
fof(f187639,plain,
( sQ3207_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f187633,f152587]) ).
fof(f187640,plain,
sQ3207_spl,
inference(contradiction_clause,[status(thm)],[f187639]) ).
fof(f187844,plain,
( ~ sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f37342,f170734]) ).
fof(f187845,plain,
~ sQ57_spl,
inference(contradiction_clause,[status(thm)],[f187844]) ).
fof(f187901,plain,
( sQ3108_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f185963]) ).
fof(f187902,plain,
sQ3108_spl,
inference(contradiction_clause,[status(thm)],[f187901]) ).
fof(f187909,definition,
! [X0] :
( sQ3218_spl
<=> ~ r1_tarski(k1_xboole_0,X0) ),
introduced(definition,[new_symbols(definition,[sQ3218_spl])],[split_symbol_definition]) ).
fof(f187910,plain,
! [X0] :
( ~ sQ3218_spl
| ~ r1_tarski(k1_xboole_0,X0) ),
inference(component_clause,[status(thm)],[f187909]) ).
fof(f187921,plain,
( ~ sQ3218_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f187910,f34618]) ).
fof(f187922,plain,
~ sQ3218_spl,
inference(contradiction_clause,[status(thm)],[f187921]) ).
fof(f188407,plain,
( ~ v3_pre_topc(k1_tops_1(sK11971_skl,sK11973_skl),sK11971_skl)
| ~ m1_subset_1(k1_tops_1(sK11971_skl,sK11973_skl),k1_zfmisc_1(u1_struct_0(sK11971_skl)))
| ~ v1_tsp_2(sK11972_skl,sK11971_skl)
| ~ m1_subset_1(sK11972_skl,k1_zfmisc_1(u1_struct_0(sK11971_skl)))
| ~ l1_pre_topc(sK11971_skl)
| ~ v2_pre_topc(sK11971_skl)
| v3_struct_0(sK11971_skl) ),
inference(resolution,[status(thm)],[f152589,f152578]) ).
fof(f188409,definition,
( sQ3230_spl
<=> m1_subset_1(k1_tops_1(sK11971_skl,sK11973_skl),k1_zfmisc_1(u1_struct_0(sK11971_skl))) ),
introduced(definition,[new_symbols(definition,[sQ3230_spl])],[split_symbol_definition]) ).
fof(f188411,plain,
( sQ3230_spl
| ~ m1_subset_1(k1_tops_1(sK11971_skl,sK11973_skl),k1_zfmisc_1(u1_struct_0(sK11971_skl))) ),
inference(component_clause,[status(thm)],[f188409]) ).
fof(f188412,definition,
( sQ3231_spl
<=> v3_pre_topc(k1_tops_1(sK11971_skl,sK11973_skl),sK11971_skl) ),
introduced(definition,[new_symbols(definition,[sQ3231_spl])],[split_symbol_definition]) ).
fof(f188414,plain,
( sQ3231_spl
| ~ v3_pre_topc(k1_tops_1(sK11971_skl,sK11973_skl),sK11971_skl) ),
inference(component_clause,[status(thm)],[f188412]) ).
fof(f188415,plain,
( ~ sQ3231_spl
| ~ sQ3230_spl
| ~ sQ3207_spl
| ~ sQ2923_spl
| ~ sQ2894_spl
| ~ sQ2897_spl
| sQ2966_spl ),
inference(split_clause,[status(thm)],[f188407,f184818,f183836,f183735,f184241,f187631,f188409,f188412]) ).
fof(f189615,definition,
( sQ3254_spl
<=> r1_tarski(k1_xboole_0,k1_tops_1(sK11971_skl,k1_xboole_0)) ),
introduced(definition,[new_symbols(definition,[sQ3254_spl])],[split_symbol_definition]) ).
fof(f189617,plain,
( sQ3254_spl
| ~ r1_tarski(k1_xboole_0,k1_tops_1(sK11971_skl,k1_xboole_0)) ),
inference(component_clause,[status(thm)],[f189615]) ).
fof(f189620,plain,
( sQ3254_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f189617,f34618]) ).
fof(f189621,plain,
sQ3254_spl,
inference(contradiction_clause,[status(thm)],[f189620]) ).
fof(f189947,definition,
( sQ3264_spl
<=> r1_xboole_0(k1_xboole_0,k1_xboole_0) ),
introduced(definition,[new_symbols(definition,[sQ3264_spl])],[split_symbol_definition]) ).
fof(f189949,plain,
( sQ3264_spl
| ~ r1_xboole_0(k1_xboole_0,k1_xboole_0) ),
inference(component_clause,[status(thm)],[f189947]) ).
fof(f189951,plain,
( sQ3264_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f189949,f34737]) ).
fof(f189952,plain,
sQ3264_spl,
inference(contradiction_clause,[status(thm)],[f189951]) ).
fof(f191974,plain,
( ~ sQ481_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f42507,f172349]) ).
fof(f191975,plain,
~ sQ481_spl,
inference(contradiction_clause,[status(thm)],[f191974]) ).
fof(f195029,plain,
( sQ3230_spl
| ~ m1_subset_1(sK11973_skl,k1_zfmisc_1(u1_struct_0(sK11971_skl)))
| ~ l1_pre_topc(sK11971_skl) ),
inference(resolution,[status(thm)],[f94281,f188411]) ).
fof(f195059,plain,
( sQ3230_spl
| ~ sQ2972_spl
| ~ sQ2894_spl ),
inference(split_clause,[status(thm)],[f195029,f183735,f184929,f188409]) ).
fof(f195093,plain,
( ~ sQ468_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f44694,f172302]) ).
fof(f195094,plain,
~ sQ468_spl,
inference(contradiction_clause,[status(thm)],[f195093]) ).
fof(f195289,definition,
! [X0] :
( sQ3405_spl
<=> ~ r2_hidden(X0,k5_ordinal2) ),
introduced(definition,[new_symbols(definition,[sQ3405_spl])],[split_symbol_definition]) ).
fof(f195290,plain,
! [X0] :
( ~ sQ3405_spl
| ~ r2_hidden(X0,k5_ordinal2) ),
inference(component_clause,[status(thm)],[f195289]) ).
fof(f195330,plain,
( ~ sQ3405_spl
| k5_ordinal2 = k1_xboole_0 ),
inference(resolution,[status(thm)],[f195290,f34483]) ).
fof(f195353,plain,
( ~ sQ3405_spl
| ~ v1_xboole_0(k1_xboole_0) ),
inference(backward_demodulation,[status(thm)],[f195330,f41556]) ).
fof(f195357,plain,
( ~ sQ3405_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f195353,f35877]) ).
fof(f195358,plain,
~ sQ3405_spl,
inference(contradiction_clause,[status(thm)],[f195357]) ).
fof(f195486,plain,
( sQ3231_spl
| ~ m1_subset_1(sK11973_skl,k1_zfmisc_1(u1_struct_0(sK11971_skl)))
| ~ l1_pre_topc(sK11971_skl)
| ~ v2_pre_topc(sK11971_skl) ),
inference(resolution,[status(thm)],[f93924,f188414]) ).
fof(f195487,plain,
( sQ3231_spl
| ~ sQ2972_spl
| ~ sQ2894_spl
| ~ sQ2897_spl ),
inference(split_clause,[status(thm)],[f195486,f183836,f183735,f184929,f188412]) ).
fof(f195488,plain,
$false,
inference(sat_refutation,[status(thm)],[f183747,f183854,f184340,f184837,f185084,f187640,f187845,f187902,f187922,f188415,f189621,f189952,f191975,f195059,f195094,f195358,f195487]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : TOP027+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n004.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 12:41:17 UTC 2026
% 0.08/0.36 % CPUTime :
% 7.53/7.87 % Drodi V4.1.1
% 145.01/25.38 % Refutation found
% 145.01/25.38 % SZS status Theorem for theBenchmark: Theorem is valid
% 145.01/25.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 12.19/26.57 % Elapsed time: 26.027563 seconds
% 12.19/26.57 % CPU time: 147.100948 seconds
% 12.19/26.57 % Total memory used: 11.217 GB
% 12.19/26.57 % Net memory used: 11.113 GB
%------------------------------------------------------------------------------