%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV030+1 : TPTP v9.3.1. Bugfixed v3.3.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 02:46:29 PM UTC 2026
% Result : Theorem 0.21s 0.81s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 19
% Syntax : Number of formulae : 96 ( 18 unt; 18 def)
% Number of atoms : 428 ( 47 equ)
% Maximal formula atoms : 34 ( 4 avg)
% Number of connectives : 510 ( 178 ~; 186 |; 114 &)
% ( 18 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 18 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 15 con; 0-3 aty)
% Number of variables : 46 ( 38 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f53,conjecture,
( ( ! [C] :
( ( leq(C,minus(pv1376,n1))
& leq(n0,C) )
=> a_select2(s_values7_init,C) = init )
& ! [A] :
( ( leq(A,n2)
& leq(n0,A) )
=> ! [B] :
( ( leq(B,n3)
& leq(n0,B) )
=> a_select3(simplex7_init,B,A) = init ) )
& leq(pv1376,n3)
& leq(pv20,minus(n330,n1))
& leq(pv19,minus(n410,n1))
& leq(pv7,minus(n410,n1))
& leq(n0,pv1376)
& leq(n0,pv20)
& leq(n0,pv19)
& leq(n0,pv7)
& init = init )
=> ( ! [F] :
( ( leq(F,minus(pv1376,n1))
& leq(n0,F) )
=> a_select2(s_values7_init,F) = init )
& ! [D] :
( ( leq(D,n2)
& leq(n0,D) )
=> ! [E] :
( ( leq(E,n3)
& leq(n0,E) )
=> a_select3(simplex7_init,E,D) = init ) )
& leq(pv1376,n3)
& leq(pv20,minus(n330,n1))
& leq(pv19,minus(n410,n1))
& leq(pv7,minus(n410,n1))
& leq(n0,pv1376)
& leq(n0,pv20)
& leq(n0,pv19)
& leq(n0,pv7)
& init = init ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
~ ( ( ! [C] :
( ( leq(C,minus(pv1376,n1))
& leq(n0,C) )
=> a_select2(s_values7_init,C) = init )
& ! [A] :
( ( leq(A,n2)
& leq(n0,A) )
=> ! [B] :
( ( leq(B,n3)
& leq(n0,B) )
=> a_select3(simplex7_init,B,A) = init ) )
& leq(pv1376,n3)
& leq(pv20,minus(n330,n1))
& leq(pv19,minus(n410,n1))
& leq(pv7,minus(n410,n1))
& leq(n0,pv1376)
& leq(n0,pv20)
& leq(n0,pv19)
& leq(n0,pv7)
& init = init )
=> ( ! [F] :
( ( leq(F,minus(pv1376,n1))
& leq(n0,F) )
=> a_select2(s_values7_init,F) = init )
& ! [D] :
( ( leq(D,n2)
& leq(n0,D) )
=> ! [E] :
( ( leq(E,n3)
& leq(n0,E) )
=> a_select3(simplex7_init,E,D) = init ) )
& leq(pv1376,n3)
& leq(pv20,minus(n330,n1))
& leq(pv19,minus(n410,n1))
& leq(pv7,minus(n410,n1))
& leq(n0,pv1376)
& leq(n0,pv20)
& leq(n0,pv19)
& leq(n0,pv7)
& init = init ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f259,plain,
( ( ? [F] :
( a_select2(s_values7_init,F) != init
& leq(F,minus(pv1376,n1))
& leq(n0,F) )
| ? [D] :
( ? [E] :
( a_select3(simplex7_init,E,D) != init
& leq(E,n3)
& leq(n0,E) )
& leq(D,n2)
& leq(n0,D) )
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init )
& ! [C] :
( a_select2(s_values7_init,C) = init
| ~ leq(C,minus(pv1376,n1))
| ~ leq(n0,C) )
& ! [A] :
( ! [B] :
( a_select3(simplex7_init,B,A) = init
| ~ leq(B,n3)
| ~ leq(n0,B) )
| ~ leq(A,n2)
| ~ leq(n0,A) )
& leq(pv1376,n3)
& leq(pv20,minus(n330,n1))
& leq(pv19,minus(n410,n1))
& leq(pv7,minus(n410,n1))
& leq(n0,pv1376)
& leq(n0,pv20)
& leq(n0,pv19)
& leq(n0,pv7)
& init = init ),
inference(pre_NNF_transformation,[status(thm)],[f54]) ).
fof(f260,definition,
! [D] :
( sP3_prd(D)
<=> ( ? [E] :
( a_select3(simplex7_init,E,D) != init
& leq(E,n3)
& leq(n0,E) )
& leq(D,n2)
& leq(n0,D) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f261,plain,
( ( ? [F] :
( a_select2(s_values7_init,F) != init
& leq(F,minus(pv1376,n1))
& leq(n0,F) )
| ? [D] : sP3_prd(D)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init )
& ! [C] :
( a_select2(s_values7_init,C) = init
| ~ leq(C,minus(pv1376,n1))
| ~ leq(n0,C) )
& ! [A] :
( ! [B] :
( a_select3(simplex7_init,B,A) = init
| ~ leq(B,n3)
| ~ leq(n0,B) )
| ~ leq(A,n2)
| ~ leq(n0,A) )
& leq(pv1376,n3)
& leq(pv20,minus(n330,n1))
& leq(pv19,minus(n410,n1))
& leq(pv7,minus(n410,n1))
& leq(n0,pv1376)
& leq(n0,pv20)
& leq(n0,pv19)
& leq(n0,pv7)
& init = init ),
inference(formula_renaming,[status(thm)],[f259,f260]) ).
fof(f262,plain,
( ( ( a_select2(s_values7_init,sK24_skl) != init
& leq(sK24_skl,minus(pv1376,n1))
& leq(n0,sK24_skl) )
| sP3_prd(sK23_skl)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init )
& ! [C] :
( a_select2(s_values7_init,C) = init
| ~ leq(C,minus(pv1376,n1))
| ~ leq(n0,C) )
& ! [A] :
( ! [B] :
( a_select3(simplex7_init,B,A) = init
| ~ leq(B,n3)
| ~ leq(n0,B) )
| ~ leq(A,n2)
| ~ leq(n0,A) )
& leq(pv1376,n3)
& leq(pv20,minus(n330,n1))
& leq(pv19,minus(n410,n1))
& leq(pv7,minus(n410,n1))
& leq(n0,pv1376)
& leq(n0,pv20)
& leq(n0,pv19)
& leq(n0,pv7)
& init = init ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl]),skolemize(D,sK23_skl),skolemize(F,sK24_skl)],[f261]) ).
fof(f264,plain,
leq(n0,pv7),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f265,plain,
leq(n0,pv19),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f266,plain,
leq(n0,pv20),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f267,plain,
leq(n0,pv1376),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f268,plain,
leq(pv7,minus(n410,n1)),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f269,plain,
leq(pv19,minus(n410,n1)),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f270,plain,
leq(pv20,minus(n330,n1)),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f271,plain,
leq(pv1376,n3),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f272,plain,
! [X0,X1] :
( a_select3(simplex7_init,X1,X0) = init
| ~ leq(X1,n3)
| ~ leq(n0,X1)
| ~ leq(X0,n2)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f273,plain,
! [X0] :
( a_select2(s_values7_init,X0) = init
| ~ leq(X0,minus(pv1376,n1))
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f274,plain,
( leq(n0,sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init ),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f275,plain,
( leq(sK24_skl,minus(pv1376,n1))
| sP3_prd(sK23_skl)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init ),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f276,plain,
( a_select2(s_values7_init,sK24_skl) != init
| sP3_prd(sK23_skl)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init ),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f358,plain,
! [D] :
( ( ! [E] :
( a_select3(simplex7_init,E,D) = init
| ~ leq(E,n3)
| ~ leq(n0,E) )
| ~ leq(D,n2)
| ~ leq(n0,D)
| sP3_prd(D) )
& ( ( ? [E] :
( a_select3(simplex7_init,E,D) != init
& leq(E,n3)
& leq(n0,E) )
& leq(D,n2)
& leq(n0,D) )
| ~ sP3_prd(D) ) ),
inference(NNF_transformation,[status(thm)],[f260]) ).
fof(f359,plain,
( ! [D] :
( ! [E] :
( a_select3(simplex7_init,E,D) = init
| ~ leq(E,n3)
| ~ leq(n0,E) )
| ~ leq(D,n2)
| ~ leq(n0,D)
| sP3_prd(D) )
& ! [D] :
( ( ? [E] :
( a_select3(simplex7_init,E,D) != init
& leq(E,n3)
& leq(n0,E) )
& leq(D,n2)
& leq(n0,D) )
| ~ sP3_prd(D) ) ),
inference(miniscoping,[status(thm)],[f358]) ).
fof(f360,plain,
( ! [D] :
( ! [E] :
( a_select3(simplex7_init,E,D) = init
| ~ leq(E,n3)
| ~ leq(n0,E) )
| ~ leq(D,n2)
| ~ leq(n0,D)
| sP3_prd(D) )
& ! [D] :
( ( a_select3(simplex7_init,sK29_skl(D),D) != init
& leq(sK29_skl(D),n3)
& leq(n0,sK29_skl(D))
& leq(D,n2)
& leq(n0,D) )
| ~ sP3_prd(D) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl]),skolemize(E,sK29_skl(D))],[f359]) ).
fof(f361,plain,
! [X0] :
( leq(n0,X0)
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f360]) ).
fof(f362,plain,
! [X0] :
( leq(X0,n2)
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f360]) ).
fof(f363,plain,
! [X0] :
( leq(n0,sK29_skl(X0))
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f360]) ).
fof(f364,plain,
! [X0] :
( leq(sK29_skl(X0),n3)
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f360]) ).
fof(f365,plain,
! [X0] :
( a_select3(simplex7_init,sK29_skl(X0),X0) != init
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f360]) ).
fof(f375,definition,
( sQ0_spl
<=> init = init ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f377,plain,
( sQ0_spl
| init != init ),
inference(component_clause,[status(thm)],[f375]) ).
fof(f378,definition,
( sQ1_spl
<=> leq(n0,pv7) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f380,plain,
( sQ1_spl
| ~ leq(n0,pv7) ),
inference(component_clause,[status(thm)],[f378]) ).
fof(f381,definition,
( sQ2_spl
<=> leq(n0,pv19) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f383,plain,
( sQ2_spl
| ~ leq(n0,pv19) ),
inference(component_clause,[status(thm)],[f381]) ).
fof(f384,definition,
( sQ3_spl
<=> leq(n0,pv20) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f386,plain,
( sQ3_spl
| ~ leq(n0,pv20) ),
inference(component_clause,[status(thm)],[f384]) ).
fof(f387,definition,
( sQ4_spl
<=> leq(n0,pv1376) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f389,plain,
( sQ4_spl
| ~ leq(n0,pv1376) ),
inference(component_clause,[status(thm)],[f387]) ).
fof(f390,definition,
( sQ5_spl
<=> leq(pv7,minus(n410,n1)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f392,plain,
( sQ5_spl
| ~ leq(pv7,minus(n410,n1)) ),
inference(component_clause,[status(thm)],[f390]) ).
fof(f393,definition,
( sQ6_spl
<=> leq(pv19,minus(n410,n1)) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f395,plain,
( sQ6_spl
| ~ leq(pv19,minus(n410,n1)) ),
inference(component_clause,[status(thm)],[f393]) ).
fof(f396,definition,
( sQ7_spl
<=> leq(pv20,minus(n330,n1)) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f398,plain,
( sQ7_spl
| ~ leq(pv20,minus(n330,n1)) ),
inference(component_clause,[status(thm)],[f396]) ).
fof(f399,definition,
( sQ8_spl
<=> leq(pv1376,n3) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f401,plain,
( sQ8_spl
| ~ leq(pv1376,n3) ),
inference(component_clause,[status(thm)],[f399]) ).
fof(f402,definition,
( sQ9_spl
<=> sP3_prd(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f403,plain,
( ~ sQ9_spl
| sP3_prd(sK23_skl) ),
inference(component_clause,[status(thm)],[f402]) ).
fof(f405,definition,
( sQ10_spl
<=> leq(n0,sK24_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f408,plain,
( 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)],[f274,f375,f378,f381,f384,f387,f390,f393,f396,f399,f402,f405]) ).
fof(f409,definition,
( sQ11_spl
<=> leq(sK24_skl,minus(pv1376,n1)) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f412,plain,
( sQ11_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)],[f275,f375,f378,f381,f384,f387,f390,f393,f396,f399,f402,f409]) ).
fof(f413,definition,
( sQ12_spl
<=> a_select2(s_values7_init,sK24_skl) = init ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f415,plain,
( sQ12_spl
| a_select2(s_values7_init,sK24_skl) != init ),
inference(component_clause,[status(thm)],[f413]) ).
fof(f416,plain,
( ~ sQ12_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)],[f276,f375,f378,f381,f384,f387,f390,f393,f396,f399,f402,f413]) ).
fof(f464,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f401,f271]) ).
fof(f465,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f464]) ).
fof(f466,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f389,f267]) ).
fof(f467,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f466]) ).
fof(f468,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f386,f266]) ).
fof(f469,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f468]) ).
fof(f470,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f383,f265]) ).
fof(f471,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f470]) ).
fof(f472,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f380,f264]) ).
fof(f473,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f472]) ).
fof(f474,plain,
( sQ0_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f377]) ).
fof(f475,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f474]) ).
fof(f621,plain,
( ~ sQ9_spl
| a_select3(simplex7_init,sK29_skl(sK23_skl),sK23_skl) != init ),
inference(resolution,[status(thm)],[f365,f403]) ).
fof(f623,plain,
( ~ sQ9_spl
| ~ leq(sK29_skl(sK23_skl),n3)
| ~ leq(n0,sK29_skl(sK23_skl))
| ~ leq(sK23_skl,n2)
| ~ leq(n0,sK23_skl) ),
inference(resolution,[status(thm)],[f272,f621]) ).
fof(f624,definition,
( sQ43_spl
<=> leq(n0,sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f626,plain,
( sQ43_spl
| ~ leq(n0,sK23_skl) ),
inference(component_clause,[status(thm)],[f624]) ).
fof(f627,definition,
( sQ44_spl
<=> leq(sK23_skl,n2) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f629,plain,
( sQ44_spl
| ~ leq(sK23_skl,n2) ),
inference(component_clause,[status(thm)],[f627]) ).
fof(f630,definition,
( sQ45_spl
<=> leq(n0,sK29_skl(sK23_skl)) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f632,plain,
( sQ45_spl
| ~ leq(n0,sK29_skl(sK23_skl)) ),
inference(component_clause,[status(thm)],[f630]) ).
fof(f633,definition,
( sQ46_spl
<=> leq(sK29_skl(sK23_skl),n3) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f635,plain,
( sQ46_spl
| ~ leq(sK29_skl(sK23_skl),n3) ),
inference(component_clause,[status(thm)],[f633]) ).
fof(f636,plain,
( ~ sQ9_spl
| ~ sQ46_spl
| ~ sQ45_spl
| ~ sQ44_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f623,f624,f627,f630,f633,f402]) ).
fof(f637,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f398,f270]) ).
fof(f638,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f637]) ).
fof(f639,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f395,f269]) ).
fof(f640,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f639]) ).
fof(f641,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f392,f268]) ).
fof(f642,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f641]) ).
fof(f646,plain,
( sQ46_spl
| ~ sP3_prd(sK23_skl) ),
inference(resolution,[status(thm)],[f635,f364]) ).
fof(f648,plain,
( sQ46_spl
| ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f646,f403]) ).
fof(f649,plain,
( sQ46_spl
| ~ sQ9_spl ),
inference(contradiction_clause,[status(thm)],[f648]) ).
fof(f650,plain,
( sQ45_spl
| ~ sP3_prd(sK23_skl) ),
inference(resolution,[status(thm)],[f632,f363]) ).
fof(f654,plain,
( sQ45_spl
| ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f650,f403]) ).
fof(f655,plain,
( sQ45_spl
| ~ sQ9_spl ),
inference(contradiction_clause,[status(thm)],[f654]) ).
fof(f656,plain,
( sQ12_spl
| ~ leq(sK24_skl,minus(pv1376,n1))
| ~ leq(n0,sK24_skl) ),
inference(resolution,[status(thm)],[f415,f273]) ).
fof(f657,plain,
( sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f656,f405,f409,f413]) ).
fof(f675,plain,
( sQ43_spl
| ~ sP3_prd(sK23_skl) ),
inference(resolution,[status(thm)],[f626,f361]) ).
fof(f678,plain,
( sQ43_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f675,f402,f624]) ).
fof(f679,plain,
( sQ44_spl
| ~ sP3_prd(sK23_skl) ),
inference(resolution,[status(thm)],[f629,f362]) ).
fof(f681,plain,
( sQ44_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f679,f402,f627]) ).
fof(f682,plain,
$false,
inference(sat_refutation,[status(thm)],[f408,f412,f416,f465,f467,f469,f471,f473,f475,f636,f638,f640,f642,f649,f655,f657,f678,f681]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV030+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.67 % Computer : n006.cluster.edu
% 0.16/0.67 % Model : x86_64 x86_64
% 0.16/0.67 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.67 % Memory : 8046.5625MB
% 0.16/0.67 % OS : Linux 6.8.0-71-generic
% 0.16/0.67 % CPULimit : 300
% 0.16/0.67 % WCLimit : 300
% 0.16/0.67 % DateTime : Mon Sep 21 08:27:43 UTC 2026
% 0.16/0.67 % CPUTime :
% 0.16/0.70 % Drodi V4.1.1
% 0.21/0.81 % Refutation found
% 0.21/0.81 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.21/0.81 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.21/0.85 % Elapsed time: 0.164577 seconds
% 0.21/0.85 % CPU time: 0.941180 seconds
% 0.21/0.85 % Total memory used: 118.295 MB
% 0.21/0.85 % Net memory used: 117.081 MB
%------------------------------------------------------------------------------