%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : KRS156+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 : n006.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:49 PM UTC 2026
% Result : Theorem 0.15s 0.39s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 14
% Syntax : Number of formulae : 68 ( 14 unt; 8 def)
% Number of atoms : 211 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 241 ( 98 ~; 100 |; 29 &)
% ( 13 <=>; 0 =>; 0 <=; 1 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 18 ( 17 usr; 9 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 33 ( 26 !; 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(f50,axiom,
! [X] :
( cC140(X)
<=> ( cC138(X)
& cTOP(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f128,axiom,
! [X] :
( cTEST(X)
<=> ( cC116(X)
& cC140(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f132,axiom,
cTEST(iV5475),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f146,conjecture,
( cC138(iV5475)
& cowlThing(iV5475)
& cC140(iV5475)
& cC116(iV5475)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f147,negated_conjecture,
~ ( cC138(iV5475)
& cowlThing(iV5475)
& cC140(iV5475)
& cC116(iV5475)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negated_conjecture,[status(cth)],[f146]) ).
fof(f148,plain,
( ! [X] : ~ cowlNothing(X)
& ! [X] : cowlThing(X) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f149,plain,
! [X0] : cowlThing(X0),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f150,plain,
! [X0] : ~ cowlNothing(X0),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f151,plain,
! [X] :
( ( xsd_integer(X)
| xsd_string(X) )
& ( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(NNF_transformation,[status(thm)],[f2]) ).
fof(f152,plain,
( ! [X] :
( xsd_integer(X)
| xsd_string(X) )
& ! [X] :
( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(miniscoping,[status(thm)],[f151]) ).
fof(f153,plain,
! [X0] :
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f154,plain,
! [X0] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f415,plain,
! [X] :
( ( ~ cC138(X)
| ~ cTOP(X)
| cC140(X) )
& ( ( cC138(X)
& cTOP(X) )
| ~ cC140(X) ) ),
inference(NNF_transformation,[status(thm)],[f50]) ).
fof(f416,plain,
( ! [X] :
( ~ cC138(X)
| ~ cTOP(X)
| cC140(X) )
& ! [X] :
( ( cC138(X)
& cTOP(X) )
| ~ cC140(X) ) ),
inference(miniscoping,[status(thm)],[f415]) ).
fof(f418,plain,
! [X0] :
( cC138(X0)
| ~ cC140(X0) ),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f846,plain,
! [X] :
( ( ~ cC116(X)
| ~ cC140(X)
| cTEST(X) )
& ( ( cC116(X)
& cC140(X) )
| ~ cTEST(X) ) ),
inference(NNF_transformation,[status(thm)],[f128]) ).
fof(f847,plain,
( ! [X] :
( ~ cC116(X)
| ~ cC140(X)
| cTEST(X) )
& ! [X] :
( ( cC116(X)
& cC140(X) )
| ~ cTEST(X) ) ),
inference(miniscoping,[status(thm)],[f846]) ).
fof(f848,plain,
! [X0] :
( cC140(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[status(thm)],[f847]) ).
fof(f849,plain,
! [X0] :
( cC116(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[status(thm)],[f847]) ).
fof(f854,plain,
cTEST(iV5475),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f872,plain,
( ~ cC138(iV5475)
| ~ cowlThing(iV5475)
| ~ cC140(iV5475)
| ~ cC116(iV5475)
| ? [X] :
( xsd_string(X)
<~> ~ xsd_integer(X) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f147]) ).
fof(f873,plain,
( ~ cC138(iV5475)
| ~ cowlThing(iV5475)
| ~ cC140(iV5475)
| ~ cC116(iV5475)
| ? [X] :
( ( xsd_integer(X)
| ~ xsd_string(X) )
& ( ~ xsd_integer(X)
| xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(NNF_transformation,[status(thm)],[f872]) ).
fof(f874,plain,
( ~ cC138(iV5475)
| ~ cowlThing(iV5475)
| ~ cC140(iV5475)
| ~ cC116(iV5475)
| ? [X] :
( ( xsd_integer(X)
| ~ xsd_string(X) )
& ( ~ xsd_integer(X)
| xsd_string(X) ) )
| ? [X] : cowlNothing(X)
| ? [X] : ~ cowlThing(X) ),
inference(miniscoping,[status(thm)],[f873]) ).
fof(f875,plain,
( ~ cC138(iV5475)
| ~ cowlThing(iV5475)
| ~ cC140(iV5475)
| ~ cC116(iV5475)
| ( ( xsd_integer(sK96_skl)
| ~ xsd_string(sK96_skl) )
& ( ~ xsd_integer(sK96_skl)
| xsd_string(sK96_skl) ) )
| cowlNothing(sK95_skl)
| ~ cowlThing(sK94_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK94_skl,sK95_skl,sK96_skl]),skolemize(X,sK94_skl),skolemize(X,sK95_skl),skolemize(X,sK96_skl)],[f874]) ).
fof(f876,plain,
( ~ cC138(iV5475)
| ~ cowlThing(iV5475)
| ~ cC140(iV5475)
| ~ cC116(iV5475)
| ~ xsd_integer(sK96_skl)
| xsd_string(sK96_skl)
| cowlNothing(sK95_skl)
| ~ cowlThing(sK94_skl) ),
inference(cnf_transformation,[status(thm)],[f875]) ).
fof(f877,plain,
( ~ cC138(iV5475)
| ~ cowlThing(iV5475)
| ~ cC140(iV5475)
| ~ cC116(iV5475)
| xsd_integer(sK96_skl)
| ~ xsd_string(sK96_skl)
| cowlNothing(sK95_skl)
| ~ cowlThing(sK94_skl) ),
inference(cnf_transformation,[status(thm)],[f875]) ).
fof(f878,definition,
( sQ0_spl
<=> cowlThing(sK94_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f880,plain,
( sQ0_spl
| ~ cowlThing(sK94_skl) ),
inference(component_clause,[status(thm)],[f878]) ).
fof(f881,definition,
( sQ1_spl
<=> cowlNothing(sK95_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f882,plain,
( ~ sQ1_spl
| cowlNothing(sK95_skl) ),
inference(component_clause,[status(thm)],[f881]) ).
fof(f884,definition,
( sQ2_spl
<=> xsd_string(sK96_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f885,plain,
( ~ sQ2_spl
| xsd_string(sK96_skl) ),
inference(component_clause,[status(thm)],[f884]) ).
fof(f886,plain,
( sQ2_spl
| ~ xsd_string(sK96_skl) ),
inference(component_clause,[status(thm)],[f884]) ).
fof(f887,definition,
( sQ3_spl
<=> xsd_integer(sK96_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f888,plain,
( ~ sQ3_spl
| xsd_integer(sK96_skl) ),
inference(component_clause,[status(thm)],[f887]) ).
fof(f890,definition,
( sQ4_spl
<=> cC116(iV5475) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f892,plain,
( sQ4_spl
| ~ cC116(iV5475) ),
inference(component_clause,[status(thm)],[f890]) ).
fof(f893,definition,
( sQ5_spl
<=> cC140(iV5475) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f895,plain,
( sQ5_spl
| ~ cC140(iV5475) ),
inference(component_clause,[status(thm)],[f893]) ).
fof(f896,definition,
( sQ6_spl
<=> cowlThing(iV5475) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f898,plain,
( sQ6_spl
| ~ cowlThing(iV5475) ),
inference(component_clause,[status(thm)],[f896]) ).
fof(f899,definition,
( sQ7_spl
<=> cC138(iV5475) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f901,plain,
( sQ7_spl
| ~ cC138(iV5475) ),
inference(component_clause,[status(thm)],[f899]) ).
fof(f902,plain,
( ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| sQ2_spl
| sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f876,f878,f881,f884,f887,f890,f893,f896,f899]) ).
fof(f903,plain,
( ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| sQ3_spl
| ~ sQ2_spl
| sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f877,f878,f881,f884,f887,f890,f893,f896,f899]) ).
fof(f906,plain,
cC140(iV5475),
inference(resolution,[status(thm)],[f848,f854]) ).
fof(f907,plain,
cC138(iV5475),
inference(resolution,[status(thm)],[f906,f418]) ).
fof(f908,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f907,f901]) ).
fof(f909,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f908]) ).
fof(f910,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f898,f149]) ).
fof(f911,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f910]) ).
fof(f912,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f895,f906]) ).
fof(f913,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f912]) ).
fof(f914,plain,
cC116(iV5475),
inference(resolution,[status(thm)],[f849,f854]) ).
fof(f915,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f914,f892]) ).
fof(f916,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f915]) ).
fof(f917,plain,
( ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f882,f150]) ).
fof(f918,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f917]) ).
fof(f919,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f880,f149]) ).
fof(f920,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f919]) ).
fof(f921,plain,
( ~ sQ3_spl
| ~ xsd_string(sK96_skl) ),
inference(resolution,[status(thm)],[f888,f153]) ).
fof(f922,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f921,f885]) ).
fof(f923,plain,
( ~ sQ3_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f922]) ).
fof(f924,plain,
( sQ2_spl
| xsd_integer(sK96_skl) ),
inference(resolution,[status(thm)],[f886,f154]) ).
fof(f925,plain,
( sQ2_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f924,f887,f884]) ).
fof(f926,plain,
$false,
inference(sat_refutation,[status(thm)],[f902,f903,f909,f911,f913,f916,f918,f920,f923,f925]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS156+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.35 % Computer : n006.cluster.edu
% 0.11/0.35 % Model : x86_64 x86_64
% 0.11/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.35 % Memory : 8046.5625MB
% 0.11/0.35 % OS : Linux 6.8.0-71-generic
% 0.11/0.35 % CPULimit : 300
% 0.11/0.35 % WCLimit : 300
% 0.11/0.35 % DateTime : Sun Sep 20 22:54:58 UTC 2026
% 0.11/0.35 % CPUTime :
% 0.15/0.37 % Drodi V4.1.1
% 0.15/0.39 % Refutation found
% 0.15/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/0.42 % Elapsed time: 0.058252 seconds
% 0.15/0.42 % CPU time: 0.148159 seconds
% 0.15/0.42 % Total memory used: 30.071 MB
% 0.15/0.42 % Net memory used: 29.938 MB
%------------------------------------------------------------------------------