%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : KRS157+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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.09s 0.39s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 20
% Syntax : Number of formulae : 98 ( 20 unt; 12 def)
% Number of atoms : 324 ( 0 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 380 ( 154 ~; 159 |; 47 &)
% ( 19 <=>; 0 =>; 0 <=; 1 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 26 ( 25 usr; 13 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 46 ( 39 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f122,axiom,
! [X] :
( cC216(X)
<=> ( cC214xcomp(X)
& cC64(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f133,axiom,
! [X] :
( cC30(X)
<=> ( cC14(X)
& cC28(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f149,axiom,
! [X] :
( cC46(X)
<=> ( cC44(X)
& cC30(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f202,axiom,
! [X] :
( cTEST(X)
<=> ( cC46(X)
& cC216(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f203,axiom,
cTEST(iV3102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f220,conjecture,
( cC30(iV3102)
& cowlThing(iV3102)
& cC28(iV3102)
& cC46(iV3102)
& cC64(iV3102)
& cC216(iV3102)
& cC44(iV3102)
& cC14(iV3102)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f221,negated_conjecture,
~ ( cC30(iV3102)
& cowlThing(iV3102)
& cC28(iV3102)
& cC46(iV3102)
& cC64(iV3102)
& cC216(iV3102)
& cC44(iV3102)
& cC14(iV3102)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negated_conjecture,[status(cth)],[f220]) ).
fof(f222,plain,
( ! [X] : ~ cowlNothing(X)
& ! [X] : cowlThing(X) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f223,plain,
! [X0] : cowlThing(X0),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f224,plain,
! [X0] : ~ cowlNothing(X0),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f225,plain,
! [X] :
( ( xsd_integer(X)
| xsd_string(X) )
& ( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(NNF_transformation,[status(thm)],[f2]) ).
fof(f226,plain,
( ! [X] :
( xsd_integer(X)
| xsd_string(X) )
& ! [X] :
( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(miniscoping,[status(thm)],[f225]) ).
fof(f227,plain,
! [X0] :
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f228,plain,
! [X0] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f885,plain,
! [X] :
( ( ~ cC214xcomp(X)
| ~ cC64(X)
| cC216(X) )
& ( ( cC214xcomp(X)
& cC64(X) )
| ~ cC216(X) ) ),
inference(NNF_transformation,[status(thm)],[f122]) ).
fof(f886,plain,
( ! [X] :
( ~ cC214xcomp(X)
| ~ cC64(X)
| cC216(X) )
& ! [X] :
( ( cC214xcomp(X)
& cC64(X) )
| ~ cC216(X) ) ),
inference(miniscoping,[status(thm)],[f885]) ).
fof(f887,plain,
! [X0] :
( cC64(X0)
| ~ cC216(X0) ),
inference(cnf_transformation,[status(thm)],[f886]) ).
fof(f945,plain,
! [X] :
( ( ~ cC14(X)
| ~ cC28(X)
| cC30(X) )
& ( ( cC14(X)
& cC28(X) )
| ~ cC30(X) ) ),
inference(NNF_transformation,[status(thm)],[f133]) ).
fof(f946,plain,
( ! [X] :
( ~ cC14(X)
| ~ cC28(X)
| cC30(X) )
& ! [X] :
( ( cC14(X)
& cC28(X) )
| ~ cC30(X) ) ),
inference(miniscoping,[status(thm)],[f945]) ).
fof(f947,plain,
! [X0] :
( cC28(X0)
| ~ cC30(X0) ),
inference(cnf_transformation,[status(thm)],[f946]) ).
fof(f948,plain,
! [X0] :
( cC14(X0)
| ~ cC30(X0) ),
inference(cnf_transformation,[status(thm)],[f946]) ).
fof(f1033,plain,
! [X] :
( ( ~ cC44(X)
| ~ cC30(X)
| cC46(X) )
& ( ( cC44(X)
& cC30(X) )
| ~ cC46(X) ) ),
inference(NNF_transformation,[status(thm)],[f149]) ).
fof(f1034,plain,
( ! [X] :
( ~ cC44(X)
| ~ cC30(X)
| cC46(X) )
& ! [X] :
( ( cC44(X)
& cC30(X) )
| ~ cC46(X) ) ),
inference(miniscoping,[status(thm)],[f1033]) ).
fof(f1035,plain,
! [X0] :
( cC30(X0)
| ~ cC46(X0) ),
inference(cnf_transformation,[status(thm)],[f1034]) ).
fof(f1036,plain,
! [X0] :
( cC44(X0)
| ~ cC46(X0) ),
inference(cnf_transformation,[status(thm)],[f1034]) ).
fof(f1037,plain,
! [X0] :
( ~ cC44(X0)
| ~ cC30(X0)
| cC46(X0) ),
inference(cnf_transformation,[status(thm)],[f1034]) ).
fof(f1325,plain,
! [X] :
( ( ~ cC46(X)
| ~ cC216(X)
| cTEST(X) )
& ( ( cC46(X)
& cC216(X) )
| ~ cTEST(X) ) ),
inference(NNF_transformation,[status(thm)],[f202]) ).
fof(f1326,plain,
( ! [X] :
( ~ cC46(X)
| ~ cC216(X)
| cTEST(X) )
& ! [X] :
( ( cC46(X)
& cC216(X) )
| ~ cTEST(X) ) ),
inference(miniscoping,[status(thm)],[f1325]) ).
fof(f1327,plain,
! [X0] :
( cC216(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[status(thm)],[f1326]) ).
fof(f1328,plain,
! [X0] :
( cC46(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[status(thm)],[f1326]) ).
fof(f1330,plain,
cTEST(iV3102),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f1352,plain,
( ~ cC30(iV3102)
| ~ cowlThing(iV3102)
| ~ cC28(iV3102)
| ~ cC46(iV3102)
| ~ cC64(iV3102)
| ~ cC216(iV3102)
| ~ cC44(iV3102)
| ~ cC14(iV3102)
| ? [X] :
( xsd_string(X)
<~> ~ xsd_integer(X) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f221]) ).
fof(f1353,plain,
( ~ cC30(iV3102)
| ~ cowlThing(iV3102)
| ~ cC28(iV3102)
| ~ cC46(iV3102)
| ~ cC64(iV3102)
| ~ cC216(iV3102)
| ~ cC44(iV3102)
| ~ cC14(iV3102)
| ? [X] :
( ( xsd_integer(X)
| ~ xsd_string(X) )
& ( ~ xsd_integer(X)
| xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(NNF_transformation,[status(thm)],[f1352]) ).
fof(f1354,plain,
( ~ cC30(iV3102)
| ~ cowlThing(iV3102)
| ~ cC28(iV3102)
| ~ cC46(iV3102)
| ~ cC64(iV3102)
| ~ cC216(iV3102)
| ~ cC44(iV3102)
| ~ cC14(iV3102)
| ? [X] :
( ( xsd_integer(X)
| ~ xsd_string(X) )
& ( ~ xsd_integer(X)
| xsd_string(X) ) )
| ? [X] : cowlNothing(X)
| ? [X] : ~ cowlThing(X) ),
inference(miniscoping,[status(thm)],[f1353]) ).
fof(f1355,plain,
( ~ cC30(iV3102)
| ~ cowlThing(iV3102)
| ~ cC28(iV3102)
| ~ cC46(iV3102)
| ~ cC64(iV3102)
| ~ cC216(iV3102)
| ~ cC44(iV3102)
| ~ cC14(iV3102)
| ( ( xsd_integer(sK150_skl)
| ~ xsd_string(sK150_skl) )
& ( ~ xsd_integer(sK150_skl)
| xsd_string(sK150_skl) ) )
| cowlNothing(sK149_skl)
| ~ cowlThing(sK148_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK148_skl,sK149_skl,sK150_skl]),skolemize(X,sK148_skl),skolemize(X,sK149_skl),skolemize(X,sK150_skl)],[f1354]) ).
fof(f1356,plain,
( ~ cC30(iV3102)
| ~ cowlThing(iV3102)
| ~ cC28(iV3102)
| ~ cC46(iV3102)
| ~ cC64(iV3102)
| ~ cC216(iV3102)
| ~ cC44(iV3102)
| ~ cC14(iV3102)
| ~ xsd_integer(sK150_skl)
| xsd_string(sK150_skl)
| cowlNothing(sK149_skl)
| ~ cowlThing(sK148_skl) ),
inference(cnf_transformation,[status(thm)],[f1355]) ).
fof(f1357,plain,
( ~ cC30(iV3102)
| ~ cowlThing(iV3102)
| ~ cC28(iV3102)
| ~ cC46(iV3102)
| ~ cC64(iV3102)
| ~ cC216(iV3102)
| ~ cC44(iV3102)
| ~ cC14(iV3102)
| xsd_integer(sK150_skl)
| ~ xsd_string(sK150_skl)
| cowlNothing(sK149_skl)
| ~ cowlThing(sK148_skl) ),
inference(cnf_transformation,[status(thm)],[f1355]) ).
fof(f1358,definition,
( sQ0_spl
<=> cowlThing(sK148_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f1360,plain,
( sQ0_spl
| ~ cowlThing(sK148_skl) ),
inference(component_clause,[status(thm)],[f1358]) ).
fof(f1361,definition,
( sQ1_spl
<=> cowlNothing(sK149_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f1362,plain,
( ~ sQ1_spl
| cowlNothing(sK149_skl) ),
inference(component_clause,[status(thm)],[f1361]) ).
fof(f1364,definition,
( sQ2_spl
<=> xsd_string(sK150_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f1365,plain,
( ~ sQ2_spl
| xsd_string(sK150_skl) ),
inference(component_clause,[status(thm)],[f1364]) ).
fof(f1367,definition,
( sQ3_spl
<=> xsd_integer(sK150_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f1368,plain,
( ~ sQ3_spl
| xsd_integer(sK150_skl) ),
inference(component_clause,[status(thm)],[f1367]) ).
fof(f1369,plain,
( sQ3_spl
| ~ xsd_integer(sK150_skl) ),
inference(component_clause,[status(thm)],[f1367]) ).
fof(f1370,definition,
( sQ4_spl
<=> cC14(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f1372,plain,
( sQ4_spl
| ~ cC14(iV3102) ),
inference(component_clause,[status(thm)],[f1370]) ).
fof(f1373,definition,
( sQ5_spl
<=> cC44(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1375,plain,
( sQ5_spl
| ~ cC44(iV3102) ),
inference(component_clause,[status(thm)],[f1373]) ).
fof(f1376,definition,
( sQ6_spl
<=> cC216(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f1378,plain,
( sQ6_spl
| ~ cC216(iV3102) ),
inference(component_clause,[status(thm)],[f1376]) ).
fof(f1379,definition,
( sQ7_spl
<=> cC64(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f1381,plain,
( sQ7_spl
| ~ cC64(iV3102) ),
inference(component_clause,[status(thm)],[f1379]) ).
fof(f1382,definition,
( sQ8_spl
<=> cC46(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f1385,definition,
( sQ9_spl
<=> cC28(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f1387,plain,
( sQ9_spl
| ~ cC28(iV3102) ),
inference(component_clause,[status(thm)],[f1385]) ).
fof(f1388,definition,
( sQ10_spl
<=> cowlThing(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f1390,plain,
( sQ10_spl
| ~ cowlThing(iV3102) ),
inference(component_clause,[status(thm)],[f1388]) ).
fof(f1391,definition,
( sQ11_spl
<=> cC30(iV3102) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f1393,plain,
( sQ11_spl
| ~ cC30(iV3102) ),
inference(component_clause,[status(thm)],[f1391]) ).
fof(f1394,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)],[f1356,f1358,f1361,f1364,f1367,f1370,f1373,f1376,f1379,f1382,f1385,f1388,f1391]) ).
fof(f1395,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)],[f1357,f1358,f1361,f1364,f1367,f1370,f1373,f1376,f1379,f1382,f1385,f1388,f1391]) ).
fof(f1403,plain,
cC216(iV3102),
inference(resolution,[status(thm)],[f1327,f1330]) ).
fof(f1405,plain,
cC46(iV3102),
inference(resolution,[status(thm)],[f1328,f1330]) ).
fof(f1406,plain,
cC44(iV3102),
inference(resolution,[status(thm)],[f1405,f1036]) ).
fof(f1407,plain,
cC30(iV3102),
inference(resolution,[status(thm)],[f1405,f1035]) ).
fof(f1408,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1407,f1393]) ).
fof(f1409,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f1408]) ).
fof(f1410,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1390,f223]) ).
fof(f1411,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f1410]) ).
fof(f1413,plain,
( ~ cC30(iV3102)
| cC46(iV3102) ),
inference(resolution,[status(thm)],[f1406,f1037]) ).
fof(f1415,plain,
( ~ sQ11_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f1413,f1382,f1391]) ).
fof(f1416,plain,
cC14(iV3102),
inference(resolution,[status(thm)],[f1407,f948]) ).
fof(f1417,plain,
cC28(iV3102),
inference(resolution,[status(thm)],[f1407,f947]) ).
fof(f1420,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1417,f1387]) ).
fof(f1421,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f1420]) ).
fof(f1422,plain,
( sQ7_spl
| ~ cC216(iV3102) ),
inference(resolution,[status(thm)],[f1381,f887]) ).
fof(f1423,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1422,f1403]) ).
fof(f1424,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f1423]) ).
fof(f1425,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1378,f1403]) ).
fof(f1426,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f1425]) ).
fof(f1427,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1375,f1406]) ).
fof(f1428,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f1427]) ).
fof(f1429,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1372,f1416]) ).
fof(f1430,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f1429]) ).
fof(f1431,plain,
( ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1362,f224]) ).
fof(f1432,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f1431]) ).
fof(f1433,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1360,f223]) ).
fof(f1434,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f1433]) ).
fof(f1439,plain,
( ~ sQ3_spl
| ~ xsd_string(sK150_skl) ),
inference(resolution,[status(thm)],[f1368,f227]) ).
fof(f1440,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1439,f1365]) ).
fof(f1441,plain,
( ~ sQ3_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f1440]) ).
fof(f1442,plain,
( sQ3_spl
| xsd_string(sK150_skl) ),
inference(resolution,[status(thm)],[f1369,f228]) ).
fof(f1443,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1442,f1364,f1367]) ).
fof(f1444,plain,
$false,
inference(sat_refutation,[status(thm)],[f1394,f1395,f1409,f1411,f1415,f1421,f1424,f1426,f1428,f1430,f1432,f1434,f1441,f1443]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS157+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 22:55:11 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.39 % Refutation found
% 0.09/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.09/0.42 % Elapsed time: 0.045789 seconds
% 0.09/0.42 % CPU time: 0.128835 seconds
% 0.09/0.42 % Total memory used: 14.324 MB
% 0.09/0.42 % Net memory used: 14.282 MB
%------------------------------------------------------------------------------