%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : KRS103+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 : n017.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:41 PM UTC 2026
% Result : Unsatisfiable 0.10s 5.39s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 42
% Syntax : Number of formulae : 176 ( 4 unt; 15 def)
% Number of atoms : 542 ( 0 equ)
% Maximal formula atoms : 4 ( 3 avg)
% Number of connectives : 572 ( 206 ~; 325 |; 8 &)
% ( 15 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 33 ( 32 usr; 16 prp; 0-1 aty)
% Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% Number of variables : 89 ( 89 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X] :
( cTest(X)
=> ( cminus6(X)
| cplus9(X)
| cplus1(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X] :
( cTest(X)
=> ( cminus6(X)
| cplus9(X)
| cminus7(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X] :
( cTest(X)
=> ( cminus8(X)
| cminus4(X)
| cminus9(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X] :
( cTest(X)
=> ( cminus8(X)
| cplus6(X)
| cplus4(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [X] :
( cTest(X)
=> ( cplus9(X)
| cplus6(X)
| cminus2(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [X] :
( cTest(X)
=> ( cplus8(X)
| cplus2(X)
| cminus3(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [X] :
( cTest(X)
=> ( cminus6(X)
| cplus4(X)
| cminus2(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [X] :
( cTest(X)
=> ( cminus7(X)
| cplus6(X)
| cminus2(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [X] :
( cTest(X)
=> ( cplus9(X)
| cplus4(X)
| cplus3(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [X] :
( cTest(X)
=> ( cplus4(X)
| cplus3(X)
| cminus9(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [X] :
( cTest(X)
=> ( cminus7(X)
| cminus3(X)
| cminus4(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [X] :
( cTest(X)
=> ( cplus9(X)
| cminus8(X)
| cplus3(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [X] :
( cTest(X)
=> ( cplus7(X)
| cminus2(X)
| cminus9(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [X] :
( cTest(X)
=> ( cplus7(X)
| cplus9(X)
| cminus4(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [X] :
( cTest(X)
=> ( cplus3(X)
| cminus2(X)
| cminus9(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [X] :
( cTest(X)
=> ( cplus2(X)
| cplus4(X)
| cminus1(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [X] :
( cTest(X)
=> ( cminus6(X)
| cplus1(X)
| cminus9(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [X] :
( cTest(X)
=> ( cplus8(X)
| cplus2(X)
| cminus4(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,axiom,
cTest(i2003_11_14_17_20_46476),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [X] :
~ ( cplus8(X)
& cminus8(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [X] :
~ ( cplus9(X)
& cminus9(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [X] :
~ ( cminus4(X)
& cplus4(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [X] :
~ ( cplus7(X)
& cminus7(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [X] :
~ ( cminus3(X)
& cplus3(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [X] :
~ ( cplus2(X)
& cminus2(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [X] :
~ ( cplus1(X)
& cminus1(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [X] :
~ ( cminus6(X)
& cplus6(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f65,plain,
! [X] :
( cminus6(X)
| cplus9(X)
| cplus1(X)
| ~ cTest(X) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f66,plain,
! [X0] :
( cminus6(X0)
| cplus9(X0)
| cplus1(X0)
| ~ cTest(X0) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f77,plain,
! [X] :
( cminus6(X)
| cplus9(X)
| cminus7(X)
| ~ cTest(X) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f78,plain,
! [X0] :
( cminus6(X0)
| cplus9(X0)
| cminus7(X0)
| ~ cTest(X0) ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f79,plain,
! [X] :
( cminus8(X)
| cminus4(X)
| cminus9(X)
| ~ cTest(X) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f80,plain,
! [X0] :
( cminus8(X0)
| cminus4(X0)
| cminus9(X0)
| ~ cTest(X0) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f83,plain,
! [X] :
( cminus8(X)
| cplus6(X)
| cplus4(X)
| ~ cTest(X) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f84,plain,
! [X0] :
( cminus8(X0)
| cplus6(X0)
| cplus4(X0)
| ~ cTest(X0) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f97,plain,
! [X] :
( cplus9(X)
| cplus6(X)
| cminus2(X)
| ~ cTest(X) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f98,plain,
! [X0] :
( cplus9(X0)
| cplus6(X0)
| cminus2(X0)
| ~ cTest(X0) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f101,plain,
! [X] :
( cplus8(X)
| cplus2(X)
| cminus3(X)
| ~ cTest(X) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f102,plain,
! [X0] :
( cplus8(X0)
| cplus2(X0)
| cminus3(X0)
| ~ cTest(X0) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f103,plain,
! [X] :
( cminus6(X)
| cplus4(X)
| cminus2(X)
| ~ cTest(X) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f104,plain,
! [X0] :
( cminus6(X0)
| cplus4(X0)
| cminus2(X0)
| ~ cTest(X0) ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f105,plain,
! [X] :
( cminus7(X)
| cplus6(X)
| cminus2(X)
| ~ cTest(X) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f106,plain,
! [X0] :
( cminus7(X0)
| cplus6(X0)
| cminus2(X0)
| ~ cTest(X0) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f111,plain,
! [X] :
( cplus9(X)
| cplus4(X)
| cplus3(X)
| ~ cTest(X) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f112,plain,
! [X0] :
( cplus9(X0)
| cplus4(X0)
| cplus3(X0)
| ~ cTest(X0) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f117,plain,
! [X] :
( cplus4(X)
| cplus3(X)
| cminus9(X)
| ~ cTest(X) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f118,plain,
! [X0] :
( cplus4(X0)
| cplus3(X0)
| cminus9(X0)
| ~ cTest(X0) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f119,plain,
! [X] :
( cminus7(X)
| cminus3(X)
| cminus4(X)
| ~ cTest(X) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f120,plain,
! [X0] :
( cminus7(X0)
| cminus3(X0)
| cminus4(X0)
| ~ cTest(X0) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f125,plain,
! [X] :
( cplus9(X)
| cminus8(X)
| cplus3(X)
| ~ cTest(X) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f126,plain,
! [X0] :
( cplus9(X0)
| cminus8(X0)
| cplus3(X0)
| ~ cTest(X0) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f127,plain,
! [X] :
( cplus7(X)
| cminus2(X)
| cminus9(X)
| ~ cTest(X) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f128,plain,
! [X0] :
( cplus7(X0)
| cminus2(X0)
| cminus9(X0)
| ~ cTest(X0) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f129,plain,
! [X] :
( cplus7(X)
| cplus9(X)
| cminus4(X)
| ~ cTest(X) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f130,plain,
! [X0] :
( cplus7(X0)
| cplus9(X0)
| cminus4(X0)
| ~ cTest(X0) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f131,plain,
! [X] :
( cplus3(X)
| cminus2(X)
| cminus9(X)
| ~ cTest(X) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f132,plain,
! [X0] :
( cplus3(X0)
| cminus2(X0)
| cminus9(X0)
| ~ cTest(X0) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f133,plain,
! [X] :
( cplus2(X)
| cplus4(X)
| cminus1(X)
| ~ cTest(X) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f134,plain,
! [X0] :
( cplus2(X0)
| cplus4(X0)
| cminus1(X0)
| ~ cTest(X0) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f147,plain,
! [X] :
( cminus6(X)
| cplus1(X)
| cminus9(X)
| ~ cTest(X) ),
inference(pre_NNF_transformation,[status(thm)],[f44]) ).
fof(f148,plain,
! [X0] :
( cminus6(X0)
| cplus1(X0)
| cminus9(X0)
| ~ cTest(X0) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f151,plain,
! [X] :
( cplus8(X)
| cplus2(X)
| cminus4(X)
| ~ cTest(X) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f152,plain,
! [X0] :
( cplus8(X0)
| cplus2(X0)
| cminus4(X0)
| ~ cTest(X0) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f155,plain,
cTest(i2003_11_14_17_20_46476),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f156,plain,
! [X] :
( ~ cplus8(X)
| ~ cminus8(X) ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f157,plain,
! [X0] :
( ~ cplus8(X0)
| ~ cminus8(X0) ),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f158,plain,
! [X] :
( ~ cplus9(X)
| ~ cminus9(X) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f159,plain,
! [X0] :
( ~ cplus9(X0)
| ~ cminus9(X0) ),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f160,plain,
! [X] :
( ~ cminus4(X)
| ~ cplus4(X) ),
inference(pre_NNF_transformation,[status(thm)],[f51]) ).
fof(f161,plain,
! [X0] :
( ~ cminus4(X0)
| ~ cplus4(X0) ),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f162,plain,
! [X] :
( ~ cplus7(X)
| ~ cminus7(X) ),
inference(pre_NNF_transformation,[status(thm)],[f52]) ).
fof(f163,plain,
! [X0] :
( ~ cplus7(X0)
| ~ cminus7(X0) ),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f164,plain,
! [X] :
( ~ cminus3(X)
| ~ cplus3(X) ),
inference(pre_NNF_transformation,[status(thm)],[f53]) ).
fof(f165,plain,
! [X0] :
( ~ cminus3(X0)
| ~ cplus3(X0) ),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f168,plain,
! [X] :
( ~ cplus2(X)
| ~ cminus2(X) ),
inference(pre_NNF_transformation,[status(thm)],[f55]) ).
fof(f169,plain,
! [X0] :
( ~ cplus2(X0)
| ~ cminus2(X0) ),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f170,plain,
! [X] :
( ~ cplus1(X)
| ~ cminus1(X) ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f171,plain,
! [X0] :
( ~ cplus1(X0)
| ~ cminus1(X0) ),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f172,plain,
! [X] :
( ~ cminus6(X)
| ~ cplus6(X) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f173,plain,
! [X0] :
( ~ cminus6(X0)
| ~ cplus6(X0) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f174,plain,
! [X0] :
( cplus9(X0)
| cplus1(X0)
| ~ cTest(X0)
| ~ cplus6(X0) ),
inference(resolution,[status(thm)],[f173,f66]) ).
fof(f175,plain,
! [X0] :
( ~ cplus9(X0)
| cplus4(X0)
| cplus3(X0)
| ~ cTest(X0) ),
inference(resolution,[status(thm)],[f118,f159]) ).
fof(f178,plain,
! [X0] :
( cplus4(X0)
| cplus3(X0)
| ~ cTest(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f175,f112]) ).
fof(f179,plain,
! [X0] :
( ~ cminus3(X0)
| cplus4(X0)
| ~ cTest(X0) ),
inference(resolution,[status(thm)],[f178,f165]) ).
fof(f180,plain,
! [X0] :
( ~ cminus4(X0)
| cplus3(X0)
| ~ cTest(X0) ),
inference(resolution,[status(thm)],[f178,f161]) ).
fof(f181,plain,
! [X0] :
( ~ cminus4(X0)
| ~ cminus3(X0)
| ~ cTest(X0) ),
inference(resolution,[status(thm)],[f179,f161]) ).
fof(f183,plain,
! [X0] :
( ~ cplus1(X0)
| cplus2(X0)
| cplus4(X0)
| ~ cTest(X0) ),
inference(resolution,[status(thm)],[f134,f171]) ).
fof(f186,plain,
! [X0] :
( ~ cminus2(X0)
| cplus8(X0)
| cminus4(X0)
| ~ cTest(X0) ),
inference(resolution,[status(thm)],[f152,f169]) ).
fof(f189,plain,
! [X0] :
( ~ cminus2(X0)
| ~ cplus1(X0)
| cplus4(X0)
| ~ cTest(X0) ),
inference(resolution,[status(thm)],[f183,f169]) ).
fof(f192,plain,
! [X0] :
( ~ cminus8(X0)
| ~ cminus2(X0)
| cminus4(X0)
| ~ cTest(X0) ),
inference(resolution,[status(thm)],[f186,f157]) ).
fof(f194,plain,
! [X0] :
( ~ cminus4(X0)
| ~ cminus2(X0)
| ~ cplus1(X0)
| ~ cTest(X0) ),
inference(resolution,[status(thm)],[f189,f161]) ).
fof(f195,plain,
( ~ cminus8(i2003_11_14_17_20_46476)
| ~ cminus2(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f192,f155]) ).
fof(f196,definition,
( sQ0_spl
<=> cminus4(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f197,plain,
( ~ sQ0_spl
| cminus4(i2003_11_14_17_20_46476) ),
inference(component_clause,[status(thm)],[f196]) ).
fof(f199,definition,
( sQ1_spl
<=> cminus2(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f201,plain,
( sQ1_spl
| ~ cminus2(i2003_11_14_17_20_46476) ),
inference(component_clause,[status(thm)],[f199]) ).
fof(f202,definition,
( sQ2_spl
<=> cminus8(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f204,plain,
( sQ2_spl
| ~ cminus8(i2003_11_14_17_20_46476) ),
inference(component_clause,[status(thm)],[f202]) ).
fof(f205,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f195,f196,f199,f202]) ).
fof(f206,plain,
( sQ2_spl
| cplus9(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| ~ cTest(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f204,f126]) ).
fof(f209,plain,
( sQ2_spl
| cplus6(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476)
| ~ cTest(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f204,f84]) ).
fof(f210,plain,
( sQ2_spl
| cminus4(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476)
| ~ cTest(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f204,f80]) ).
fof(f211,definition,
( sQ3_spl
<=> cTest(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f213,plain,
( sQ3_spl
| ~ cTest(i2003_11_14_17_20_46476) ),
inference(component_clause,[status(thm)],[f211]) ).
fof(f214,definition,
( sQ4_spl
<=> cplus3(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f215,plain,
( ~ sQ4_spl
| cplus3(i2003_11_14_17_20_46476) ),
inference(component_clause,[status(thm)],[f214]) ).
fof(f217,definition,
( sQ5_spl
<=> cplus9(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f218,plain,
( ~ sQ5_spl
| cplus9(i2003_11_14_17_20_46476) ),
inference(component_clause,[status(thm)],[f217]) ).
fof(f219,plain,
( sQ5_spl
| ~ cplus9(i2003_11_14_17_20_46476) ),
inference(component_clause,[status(thm)],[f217]) ).
fof(f220,plain,
( sQ2_spl
| sQ5_spl
| sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f206,f211,f214,f217,f202]) ).
fof(f222,definition,
( sQ6_spl
<=> cplus6(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f223,plain,
( ~ sQ6_spl
| cplus6(i2003_11_14_17_20_46476) ),
inference(component_clause,[status(thm)],[f222]) ).
fof(f229,definition,
( sQ8_spl
<=> cplus4(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f230,plain,
( ~ sQ8_spl
| cplus4(i2003_11_14_17_20_46476) ),
inference(component_clause,[status(thm)],[f229]) ).
fof(f232,plain,
( sQ2_spl
| sQ6_spl
| sQ8_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f209,f211,f229,f222,f202]) ).
fof(f233,definition,
( sQ9_spl
<=> cminus9(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f234,plain,
( ~ sQ9_spl
| cminus9(i2003_11_14_17_20_46476) ),
inference(component_clause,[status(thm)],[f233]) ).
fof(f236,plain,
( sQ2_spl
| sQ0_spl
| sQ9_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f210,f211,f233,f196,f202]) ).
fof(f237,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f213,f155]) ).
fof(f238,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f237]) ).
fof(f242,plain,
( ~ sQ0_spl
| ~ cminus3(i2003_11_14_17_20_46476)
| ~ cTest(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f197,f181]) ).
fof(f243,plain,
( ~ sQ0_spl
| cplus3(i2003_11_14_17_20_46476)
| ~ cTest(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f197,f180]) ).
fof(f248,definition,
( sQ11_spl
<=> cplus2(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f249,plain,
( ~ sQ11_spl
| cplus2(i2003_11_14_17_20_46476) ),
inference(component_clause,[status(thm)],[f248]) ).
fof(f251,definition,
( sQ12_spl
<=> cplus1(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f253,plain,
( sQ12_spl
| ~ cplus1(i2003_11_14_17_20_46476) ),
inference(component_clause,[status(thm)],[f251]) ).
fof(f256,definition,
( sQ13_spl
<=> cminus3(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f258,plain,
( sQ13_spl
| ~ cminus3(i2003_11_14_17_20_46476) ),
inference(component_clause,[status(thm)],[f256]) ).
fof(f259,plain,
( ~ sQ0_spl
| ~ sQ13_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f242,f211,f256,f196]) ).
fof(f260,plain,
( ~ sQ0_spl
| sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f243,f211,f214,f196]) ).
fof(f271,plain,
( ~ sQ9_spl
| ~ cplus9(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f234,f159]) ).
fof(f272,plain,
( ~ sQ9_spl
| ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f271,f218]) ).
fof(f273,plain,
( ~ sQ9_spl
| ~ sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f272]) ).
fof(f275,plain,
( sQ1_spl
| cplus3(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476)
| ~ cTest(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f201,f132]) ).
fof(f276,plain,
( sQ1_spl
| cplus7(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476)
| ~ cTest(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f201,f128]) ).
fof(f277,plain,
( sQ1_spl
| cminus6(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476)
| ~ cTest(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f201,f104]) ).
fof(f278,plain,
( sQ1_spl
| cplus9(i2003_11_14_17_20_46476)
| cplus6(i2003_11_14_17_20_46476)
| ~ cTest(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f201,f98]) ).
fof(f280,plain,
( sQ1_spl
| sQ4_spl
| sQ9_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f275,f211,f233,f214,f199]) ).
fof(f281,definition,
( sQ14_spl
<=> cplus7(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f282,plain,
( ~ sQ14_spl
| cplus7(i2003_11_14_17_20_46476) ),
inference(component_clause,[status(thm)],[f281]) ).
fof(f284,plain,
( sQ1_spl
| sQ14_spl
| sQ9_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f276,f211,f233,f281,f199]) ).
fof(f285,definition,
( sQ15_spl
<=> cminus6(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f286,plain,
( ~ sQ15_spl
| cminus6(i2003_11_14_17_20_46476) ),
inference(component_clause,[status(thm)],[f285]) ).
fof(f288,plain,
( sQ1_spl
| sQ15_spl
| sQ8_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f277,f211,f229,f285,f199]) ).
fof(f289,plain,
( sQ1_spl
| sQ5_spl
| sQ6_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f278,f211,f222,f217,f199]) ).
fof(f290,plain,
( sQ5_spl
| cplus7(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| ~ cTest(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f219,f130]) ).
fof(f294,plain,
( sQ5_spl
| sQ14_spl
| sQ0_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f290,f211,f196,f281,f217]) ).
fof(f301,plain,
( ~ sQ0_spl
| ~ cminus2(i2003_11_14_17_20_46476)
| ~ cplus1(i2003_11_14_17_20_46476)
| ~ cTest(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f197,f194]) ).
fof(f307,plain,
( ~ sQ0_spl
| ~ sQ1_spl
| ~ sQ12_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f301,f211,f251,f199,f196]) ).
fof(f313,plain,
( ~ sQ4_spl
| ~ cminus3(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f215,f165]) ).
fof(f314,plain,
( ~ sQ8_spl
| ~ cminus4(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f230,f161]) ).
fof(f316,plain,
( ~ sQ11_spl
| ~ cminus2(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f249,f169]) ).
fof(f317,plain,
( ~ sQ14_spl
| ~ cminus7(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f282,f163]) ).
fof(f321,plain,
( sQ13_spl
| cplus8(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| ~ cTest(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f258,f102]) ).
fof(f327,definition,
( sQ17_spl
<=> cplus8(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f328,plain,
( ~ sQ17_spl
| cplus8(i2003_11_14_17_20_46476) ),
inference(component_clause,[status(thm)],[f327]) ).
fof(f330,plain,
( sQ13_spl
| sQ17_spl
| sQ11_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f321,f211,f248,f327,f256]) ).
fof(f333,plain,
( ~ sQ11_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f316,f199,f248]) ).
fof(f348,plain,
( sQ12_spl
| cplus9(i2003_11_14_17_20_46476)
| ~ cTest(i2003_11_14_17_20_46476)
| ~ cplus6(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f253,f174]) ).
fof(f350,plain,
( sQ12_spl
| cminus6(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476)
| ~ cTest(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f253,f148]) ).
fof(f355,plain,
( sQ12_spl
| sQ5_spl
| ~ sQ3_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f348,f222,f211,f217,f251]) ).
fof(f357,plain,
( sQ12_spl
| sQ15_spl
| sQ9_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f350,f211,f233,f285,f251]) ).
fof(f362,plain,
( ~ sQ17_spl
| ~ cminus8(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f328,f157]) ).
fof(f363,plain,
( ~ sQ17_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f362,f202,f327]) ).
fof(f372,plain,
( ~ sQ4_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f313,f256,f214]) ).
fof(f374,plain,
( ~ sQ14_spl
| cminus3(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| ~ cTest(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f317,f120]) ).
fof(f376,plain,
( ~ sQ14_spl
| cplus6(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| ~ cTest(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f317,f106]) ).
fof(f378,plain,
( ~ sQ14_spl
| cminus6(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| ~ cTest(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f317,f78]) ).
fof(f380,plain,
( ~ sQ14_spl
| sQ13_spl
| sQ0_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f374,f211,f196,f256,f281]) ).
fof(f382,plain,
( ~ sQ14_spl
| sQ6_spl
| sQ1_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f376,f211,f199,f222,f281]) ).
fof(f384,plain,
( ~ sQ14_spl
| sQ15_spl
| sQ5_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f378,f211,f217,f285,f281]) ).
fof(f431,plain,
( ~ sQ15_spl
| ~ cplus6(i2003_11_14_17_20_46476) ),
inference(resolution,[status(thm)],[f286,f173]) ).
fof(f432,plain,
( ~ sQ15_spl
| ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f431,f223]) ).
fof(f433,plain,
( ~ sQ15_spl
| ~ sQ6_spl ),
inference(contradiction_clause,[status(thm)],[f432]) ).
fof(f434,plain,
( ~ sQ8_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f314,f196,f229]) ).
fof(f435,plain,
$false,
inference(sat_refutation,[status(thm)],[f205,f220,f232,f236,f238,f259,f260,f273,f280,f284,f288,f289,f294,f307,f330,f333,f355,f357,f363,f372,f380,f382,f384,f433,f434]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS103+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.37 % Computer : n017.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Sun Sep 20 22:48:48 UTC 2026
% 0.10/5.37 % CPUTime :
% 0.10/5.38 % Drodi V4.1.1
% 0.10/5.39 % Refutation found
% 0.10/5.39 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/5.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/5.41 % Elapsed time: 0.030722 seconds
% 0.13/5.41 % CPU time: 0.089176 seconds
% 0.13/5.41 % Total memory used: 3.494 MB
% 0.13/5.41 % Net memory used: 3.450 MB
%------------------------------------------------------------------------------