%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : KRS149+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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 12:59:48 PM UTC 2026
% Result : Theorem 0.11s 0.40s
% Output : CNFRefutation 0.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 37
% Syntax : Number of formulae : 137 ( 30 unt; 18 def)
% Number of atoms : 433 ( 0 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 512 ( 216 ~; 205 |; 62 &)
% ( 28 <=>; 0 =>; 0 <=; 1 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 39 ( 38 usr; 19 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 57 ( 50 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [X] :
( cC14(X)
<=> ( ~ cC2(X)
& ~ cC12(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [X] :
( cC216(X)
<=> ( cC64(X)
& ~ cC214(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [X] :
( cC28(X)
<=> ( ~ cC16(X)
& ~ cC26(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [X] :
( cC30(X)
<=> ( cC28(X)
& cC14(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f78,axiom,
! [X] :
( cC44(X)
<=> ( ~ cC42(X)
& ~ cC32(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f79,axiom,
! [X] :
( cC46(X)
<=> ( cC44(X)
& cC30(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f89,axiom,
! [X] :
( cC64(X)
<=> ( cTOP(X)
& ~ cC62(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f113,axiom,
cTOP(iV3102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f115,axiom,
~ cC42(iV3102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f116,axiom,
~ cC12(iV3102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f117,axiom,
~ cC26(iV3102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f119,axiom,
~ cC214(iV3102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f120,axiom,
~ cC62(iV3102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f122,axiom,
~ cC16(iV3102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f123,axiom,
~ cC2(iV3102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f124,axiom,
~ cC32(iV3102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f126,conjecture,
( cowlThing(iV3102)
& cC14(iV3102)
& cC64(iV3102)
& cC28(iV3102)
& cC44(iV3102)
& cC30(iV3102)
& cC46(iV3102)
& cC216(iV3102)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f127,negated_conjecture,
~ ( cowlThing(iV3102)
& cC14(iV3102)
& cC64(iV3102)
& cC28(iV3102)
& cC44(iV3102)
& cC30(iV3102)
& cC46(iV3102)
& cC216(iV3102)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negated_conjecture,[status(cth)],[f126]) ).
fof(f128,plain,
( ! [X] : ~ cowlNothing(X)
& ! [X] : cowlThing(X) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f129,plain,
! [X0] : cowlThing(X0),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
! [X0] : ~ cowlNothing(X0),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f131,plain,
! [X] :
( ( xsd_integer(X)
| xsd_string(X) )
& ( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(NNF_transformation,[status(thm)],[f2]) ).
fof(f132,plain,
( ! [X] :
( xsd_integer(X)
| xsd_string(X) )
& ! [X] :
( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(miniscoping,[status(thm)],[f131]) ).
fof(f133,plain,
! [X0] :
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f134,plain,
! [X0] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f257,plain,
! [X] :
( ( cC2(X)
| cC12(X)
| cC14(X) )
& ( ( ~ cC2(X)
& ~ cC12(X) )
| ~ cC14(X) ) ),
inference(NNF_transformation,[status(thm)],[f25]) ).
fof(f258,plain,
( ! [X] :
( cC2(X)
| cC12(X)
| cC14(X) )
& ! [X] :
( ( ~ cC2(X)
& ~ cC12(X) )
| ~ cC14(X) ) ),
inference(miniscoping,[status(thm)],[f257]) ).
fof(f261,plain,
! [X0] :
( cC2(X0)
| cC12(X0)
| cC14(X0) ),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f483,plain,
! [X] :
( ( ~ cC64(X)
| cC214(X)
| cC216(X) )
& ( ( cC64(X)
& ~ cC214(X) )
| ~ cC216(X) ) ),
inference(NNF_transformation,[status(thm)],[f66]) ).
fof(f484,plain,
( ! [X] :
( ~ cC64(X)
| cC214(X)
| cC216(X) )
& ! [X] :
( ( cC64(X)
& ~ cC214(X) )
| ~ cC216(X) ) ),
inference(miniscoping,[status(thm)],[f483]) ).
fof(f487,plain,
! [X0] :
( ~ cC64(X0)
| cC214(X0)
| cC216(X0) ),
inference(cnf_transformation,[status(thm)],[f484]) ).
fof(f505,plain,
! [X] :
( ( cC16(X)
| cC26(X)
| cC28(X) )
& ( ( ~ cC16(X)
& ~ cC26(X) )
| ~ cC28(X) ) ),
inference(NNF_transformation,[status(thm)],[f70]) ).
fof(f506,plain,
( ! [X] :
( cC16(X)
| cC26(X)
| cC28(X) )
& ! [X] :
( ( ~ cC16(X)
& ~ cC26(X) )
| ~ cC28(X) ) ),
inference(miniscoping,[status(thm)],[f505]) ).
fof(f509,plain,
! [X0] :
( cC16(X0)
| cC26(X0)
| cC28(X0) ),
inference(cnf_transformation,[status(thm)],[f506]) ).
fof(f510,plain,
! [X] :
( ( ~ cC28(X)
| ~ cC14(X)
| cC30(X) )
& ( ( cC28(X)
& cC14(X) )
| ~ cC30(X) ) ),
inference(NNF_transformation,[status(thm)],[f71]) ).
fof(f511,plain,
( ! [X] :
( ~ cC28(X)
| ~ cC14(X)
| cC30(X) )
& ! [X] :
( ( cC28(X)
& cC14(X) )
| ~ cC30(X) ) ),
inference(miniscoping,[status(thm)],[f510]) ).
fof(f514,plain,
! [X0] :
( ~ cC28(X0)
| ~ cC14(X0)
| cC30(X0) ),
inference(cnf_transformation,[status(thm)],[f511]) ).
fof(f549,plain,
! [X] :
( ( cC42(X)
| cC32(X)
| cC44(X) )
& ( ( ~ cC42(X)
& ~ cC32(X) )
| ~ cC44(X) ) ),
inference(NNF_transformation,[status(thm)],[f78]) ).
fof(f550,plain,
( ! [X] :
( cC42(X)
| cC32(X)
| cC44(X) )
& ! [X] :
( ( ~ cC42(X)
& ~ cC32(X) )
| ~ cC44(X) ) ),
inference(miniscoping,[status(thm)],[f549]) ).
fof(f553,plain,
! [X0] :
( cC42(X0)
| cC32(X0)
| cC44(X0) ),
inference(cnf_transformation,[status(thm)],[f550]) ).
fof(f554,plain,
! [X] :
( ( ~ cC44(X)
| ~ cC30(X)
| cC46(X) )
& ( ( cC44(X)
& cC30(X) )
| ~ cC46(X) ) ),
inference(NNF_transformation,[status(thm)],[f79]) ).
fof(f555,plain,
( ! [X] :
( ~ cC44(X)
| ~ cC30(X)
| cC46(X) )
& ! [X] :
( ( cC44(X)
& cC30(X) )
| ~ cC46(X) ) ),
inference(miniscoping,[status(thm)],[f554]) ).
fof(f558,plain,
! [X0] :
( ~ cC44(X0)
| ~ cC30(X0)
| cC46(X0) ),
inference(cnf_transformation,[status(thm)],[f555]) ).
fof(f609,plain,
! [X] :
( ( ~ cTOP(X)
| cC62(X)
| cC64(X) )
& ( ( cTOP(X)
& ~ cC62(X) )
| ~ cC64(X) ) ),
inference(NNF_transformation,[status(thm)],[f89]) ).
fof(f610,plain,
( ! [X] :
( ~ cTOP(X)
| cC62(X)
| cC64(X) )
& ! [X] :
( ( cTOP(X)
& ~ cC62(X) )
| ~ cC64(X) ) ),
inference(miniscoping,[status(thm)],[f609]) ).
fof(f613,plain,
! [X0] :
( ~ cTOP(X0)
| cC62(X0)
| cC64(X0) ),
inference(cnf_transformation,[status(thm)],[f610]) ).
fof(f725,plain,
cTOP(iV3102),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f728,plain,
~ cC42(iV3102),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f729,plain,
~ cC12(iV3102),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f730,plain,
~ cC26(iV3102),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f733,plain,
~ cC214(iV3102),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f734,plain,
~ cC62(iV3102),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f737,plain,
~ cC16(iV3102),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f738,plain,
~ cC2(iV3102),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f739,plain,
~ cC32(iV3102),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f741,plain,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| ? [X] :
( xsd_string(X)
<~> ~ xsd_integer(X) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f127]) ).
fof(f742,plain,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| ? [X] :
( ( xsd_integer(X)
| ~ xsd_string(X) )
& ( ~ xsd_integer(X)
| xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(NNF_transformation,[status(thm)],[f741]) ).
fof(f743,plain,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| ? [X] :
( ( xsd_integer(X)
| ~ xsd_string(X) )
& ( ~ xsd_integer(X)
| xsd_string(X) ) )
| ? [X] : cowlNothing(X)
| ? [X] : ~ cowlThing(X) ),
inference(miniscoping,[status(thm)],[f742]) ).
fof(f744,plain,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| ( ( xsd_integer(sK56_skl)
| ~ xsd_string(sK56_skl) )
& ( ~ xsd_integer(sK56_skl)
| xsd_string(sK56_skl) ) )
| cowlNothing(sK55_skl)
| ~ cowlThing(sK54_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54_skl,sK55_skl,sK56_skl]),skolemize(X,sK54_skl),skolemize(X,sK55_skl),skolemize(X,sK56_skl)],[f743]) ).
fof(f745,plain,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| ~ xsd_integer(sK56_skl)
| xsd_string(sK56_skl)
| cowlNothing(sK55_skl)
| ~ cowlThing(sK54_skl) ),
inference(cnf_transformation,[status(thm)],[f744]) ).
fof(f746,plain,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| xsd_integer(sK56_skl)
| ~ xsd_string(sK56_skl)
| cowlNothing(sK55_skl)
| ~ cowlThing(sK54_skl) ),
inference(cnf_transformation,[status(thm)],[f744]) ).
fof(f747,definition,
( sQ0_spl
<=> cowlThing(sK54_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f749,plain,
( sQ0_spl
| ~ cowlThing(sK54_skl) ),
inference(component_clause,[status(thm)],[f747]) ).
fof(f750,definition,
( sQ1_spl
<=> cowlNothing(sK55_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f751,plain,
( ~ sQ1_spl
| cowlNothing(sK55_skl) ),
inference(component_clause,[status(thm)],[f750]) ).
fof(f753,definition,
( sQ2_spl
<=> xsd_string(sK56_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f754,plain,
( ~ sQ2_spl
| xsd_string(sK56_skl) ),
inference(component_clause,[status(thm)],[f753]) ).
fof(f755,plain,
( sQ2_spl
| ~ xsd_string(sK56_skl) ),
inference(component_clause,[status(thm)],[f753]) ).
fof(f756,definition,
( sQ3_spl
<=> xsd_integer(sK56_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f757,plain,
( ~ sQ3_spl
| xsd_integer(sK56_skl) ),
inference(component_clause,[status(thm)],[f756]) ).
fof(f759,definition,
( sQ4_spl
<=> cC216(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f761,plain,
( sQ4_spl
| ~ cC216(iV3102) ),
inference(component_clause,[status(thm)],[f759]) ).
fof(f762,definition,
( sQ5_spl
<=> cC46(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f765,definition,
( sQ6_spl
<=> cC30(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f768,definition,
( sQ7_spl
<=> cC44(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f769,plain,
( ~ sQ7_spl
| cC44(iV3102) ),
inference(component_clause,[status(thm)],[f768]) ).
fof(f771,definition,
( sQ8_spl
<=> cC28(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f772,plain,
( ~ sQ8_spl
| cC28(iV3102) ),
inference(component_clause,[status(thm)],[f771]) ).
fof(f774,definition,
( sQ9_spl
<=> cC64(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f776,plain,
( sQ9_spl
| ~ cC64(iV3102) ),
inference(component_clause,[status(thm)],[f774]) ).
fof(f777,definition,
( sQ10_spl
<=> cC14(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f780,definition,
( sQ11_spl
<=> cowlThing(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f782,plain,
( sQ11_spl
| ~ cowlThing(iV3102) ),
inference(component_clause,[status(thm)],[f780]) ).
fof(f783,plain,
( ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| sQ2_spl
| sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f745,f747,f750,f753,f756,f759,f762,f765,f768,f771,f774,f777,f780]) ).
fof(f784,plain,
( ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| sQ3_spl
| ~ sQ2_spl
| sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f746,f747,f750,f753,f756,f759,f762,f765,f768,f771,f774,f777,f780]) ).
fof(f785,plain,
( sQ11_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f782,f129]) ).
fof(f786,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f785]) ).
fof(f788,plain,
( cC2(iV3102)
| cC14(iV3102) ),
inference(resolution,[status(thm)],[f261,f729]) ).
fof(f789,definition,
( sQ12_spl
<=> cC2(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f790,plain,
( ~ sQ12_spl
| cC2(iV3102) ),
inference(component_clause,[status(thm)],[f789]) ).
fof(f792,plain,
( sQ12_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f788,f777,f789]) ).
fof(f793,plain,
( cC16(iV3102)
| cC28(iV3102) ),
inference(resolution,[status(thm)],[f509,f730]) ).
fof(f794,definition,
( sQ13_spl
<=> cC16(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f795,plain,
( ~ sQ13_spl
| cC16(iV3102) ),
inference(component_clause,[status(thm)],[f794]) ).
fof(f797,plain,
( sQ13_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f793,f771,f794]) ).
fof(f798,plain,
( cC32(iV3102)
| cC44(iV3102) ),
inference(resolution,[status(thm)],[f553,f728]) ).
fof(f799,definition,
( sQ14_spl
<=> cC32(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f800,plain,
( ~ sQ14_spl
| cC32(iV3102) ),
inference(component_clause,[status(thm)],[f799]) ).
fof(f802,plain,
( sQ14_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f798,f768,f799]) ).
fof(f803,plain,
( sQ9_spl
| ~ cTOP(iV3102)
| cC62(iV3102) ),
inference(resolution,[status(thm)],[f776,f613]) ).
fof(f805,definition,
( sQ15_spl
<=> cC62(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f806,plain,
( ~ sQ15_spl
| cC62(iV3102) ),
inference(component_clause,[status(thm)],[f805]) ).
fof(f808,definition,
( sQ16_spl
<=> cTOP(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f810,plain,
( sQ16_spl
| ~ cTOP(iV3102) ),
inference(component_clause,[status(thm)],[f808]) ).
fof(f811,plain,
( sQ9_spl
| ~ sQ16_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f803,f805,f808,f774]) ).
fof(f812,plain,
( ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f751,f130]) ).
fof(f813,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f812]) ).
fof(f814,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f749,f129]) ).
fof(f815,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f814]) ).
fof(f816,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f810,f725]) ).
fof(f817,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f816]) ).
fof(f818,plain,
( ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f806,f734]) ).
fof(f819,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f818]) ).
fof(f821,plain,
( ~ sQ8_spl
| ~ cC14(iV3102)
| cC30(iV3102) ),
inference(resolution,[status(thm)],[f772,f514]) ).
fof(f823,plain,
( ~ sQ8_spl
| ~ sQ10_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f821,f765,f777,f771]) ).
fof(f824,plain,
( ~ sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f790,f738]) ).
fof(f825,plain,
~ sQ12_spl,
inference(contradiction_clause,[status(thm)],[f824]) ).
fof(f826,plain,
( ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f795,f737]) ).
fof(f827,plain,
~ sQ13_spl,
inference(contradiction_clause,[status(thm)],[f826]) ).
fof(f828,plain,
( ~ sQ7_spl
| ~ cC30(iV3102)
| cC46(iV3102) ),
inference(resolution,[status(thm)],[f769,f558]) ).
fof(f830,plain,
( ~ sQ7_spl
| ~ sQ6_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f828,f762,f765,f768]) ).
fof(f831,plain,
( ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f800,f739]) ).
fof(f832,plain,
~ sQ14_spl,
inference(contradiction_clause,[status(thm)],[f831]) ).
fof(f839,plain,
( sQ4_spl
| ~ cC64(iV3102)
| cC214(iV3102) ),
inference(resolution,[status(thm)],[f761,f487]) ).
fof(f840,definition,
( sQ17_spl
<=> cC214(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f841,plain,
( ~ sQ17_spl
| cC214(iV3102) ),
inference(component_clause,[status(thm)],[f840]) ).
fof(f843,plain,
( sQ4_spl
| ~ sQ9_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f839,f840,f774,f759]) ).
fof(f844,plain,
( ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f841,f733]) ).
fof(f845,plain,
~ sQ17_spl,
inference(contradiction_clause,[status(thm)],[f844]) ).
fof(f851,plain,
( ~ sQ3_spl
| ~ xsd_string(sK56_skl) ),
inference(resolution,[status(thm)],[f757,f133]) ).
fof(f852,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f851,f754]) ).
fof(f853,plain,
( ~ sQ3_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f852]) ).
fof(f854,plain,
( sQ2_spl
| xsd_integer(sK56_skl) ),
inference(resolution,[status(thm)],[f755,f134]) ).
fof(f855,plain,
( sQ2_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f854,f756,f753]) ).
fof(f856,plain,
$false,
inference(sat_refutation,[status(thm)],[f783,f784,f786,f792,f797,f802,f811,f813,f815,f817,f819,f823,f825,f827,f830,f832,f843,f845,f853,f855]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS149+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n005.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 20 22:54:49 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.39 % Drodi V4.1.1
% 0.11/0.40 % Refutation found
% 0.11/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.11/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.11/0.43 % Elapsed time: 0.046036 seconds
% 0.11/0.43 % CPU time: 0.121470 seconds
% 0.11/0.43 % Total memory used: 20.907 MB
% 0.11/0.43 % Net memory used: 20.801 MB
%------------------------------------------------------------------------------