%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV033+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 : n013.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.26s 0.72s
% Output : CNFRefutation 0.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 25
% Syntax : Number of formulae : 113 ( 15 unt; 16 def)
% Number of atoms : 369 ( 82 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 393 ( 137 ~; 151 |; 72 &)
% ( 17 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 16 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 10 con; 0-3 aty)
% Number of variables : 101 ( 93 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X] : leq(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,Y] :
( ( X != Y
& leq(X,Y) )
=> gt(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,Y] :
( leq(X,pred(Y))
<=> gt(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [X] : plus(n1,X) = succ(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [X] : minus(X,n1) = pred(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [X] : pred(succ(X)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [X,U,VAL] : a_select2(tptp_update2(X,U,VAL),U) = VAL,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [I,U,X,VAL,VAL2] :
( ( a_select2(X,U) = VAL
& I != U )
=> a_select2(tptp_update2(X,I,VAL2),U) = VAL ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
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(n0,pv1376)
& init = init )
=> ( ! [F] :
( ( leq(F,minus(plus(n1,pv1376),n1))
& leq(n0,F) )
=> a_select2(tptp_update2(s_values7_init,pv1376,init),F) = init )
& ! [D] :
( ( leq(D,n2)
& leq(n0,D) )
=> ! [E] :
( ( leq(E,n3)
& leq(n0,E) )
=> a_select3(simplex7_init,E,D) = init ) )
& 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(n0,pv1376)
& init = init )
=> ( ! [F] :
( ( leq(F,minus(plus(n1,pv1376),n1))
& leq(n0,F) )
=> a_select2(tptp_update2(s_values7_init,pv1376,init),F) = init )
& ! [D] :
( ( leq(D,n2)
& leq(n0,D) )
=> ! [E] :
( ( leq(E,n3)
& leq(n0,E) )
=> a_select3(simplex7_init,E,D) = init ) )
& init = init ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f92,plain,
! [X0] : leq(X0,X0),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f106,plain,
! [X,Y] :
( gt(Y,X)
| X = Y
| ~ leq(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f107,plain,
! [X0,X1] :
( gt(X1,X0)
| X0 = X1
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f108,plain,
! [X,Y] :
( ( ~ gt(Y,X)
| leq(X,pred(Y)) )
& ( gt(Y,X)
| ~ leq(X,pred(Y)) ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f109,plain,
( ! [X,Y] :
( ~ gt(Y,X)
| leq(X,pred(Y)) )
& ! [X,Y] :
( gt(Y,X)
| ~ leq(X,pred(Y)) ) ),
inference(miniscoping,[status(thm)],[f108]) ).
fof(f111,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| leq(X0,pred(X1)) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f201,plain,
! [X0] : plus(n1,X0) = succ(X0),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f210,plain,
! [X0] : minus(X0,n1) = pred(X0),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f211,plain,
! [X0] : pred(succ(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f233,plain,
! [X0,X1,X2] : a_select2(tptp_update2(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f234,plain,
! [I,U,X,VAL,VAL2] :
( a_select2(tptp_update2(X,I,VAL2),U) = VAL
| a_select2(X,U) != VAL
| I = U ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f235,plain,
! [I,U,X,VAL] :
( ! [VAL2] : a_select2(tptp_update2(X,I,VAL2),U) = VAL
| a_select2(X,U) != VAL
| I = U ),
inference(miniscoping,[status(thm)],[f234]) ).
fof(f236,plain,
! [X0,X1,X2,X3,X4] :
( a_select2(tptp_update2(X2,X0,X4),X1) = X3
| a_select2(X2,X1) != X3
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f244,plain,
( ( ? [F] :
( a_select2(tptp_update2(s_values7_init,pv1376,init),F) != init
& leq(F,minus(plus(n1,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) )
| 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(n0,pv1376)
& init = init ),
inference(pre_NNF_transformation,[status(thm)],[f54]) ).
fof(f245,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(f246,plain,
( ( ? [F] :
( a_select2(tptp_update2(s_values7_init,pv1376,init),F) != init
& leq(F,minus(plus(n1,pv1376),n1))
& leq(n0,F) )
| ? [D] : sP3_prd(D)
| 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(n0,pv1376)
& init = init ),
inference(formula_renaming,[status(thm)],[f244,f245]) ).
fof(f247,plain,
( ( ( a_select2(tptp_update2(s_values7_init,pv1376,init),sK24_skl) != init
& leq(sK24_skl,minus(plus(n1,pv1376),n1))
& leq(n0,sK24_skl) )
| sP3_prd(sK23_skl)
| 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(n0,pv1376)
& init = init ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl]),skolemize(D,sK23_skl),skolemize(F,sK24_skl)],[f246]) ).
fof(f249,plain,
leq(n0,pv1376),
inference(cnf_transformation,[status(thm)],[f247]) ).
fof(f251,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)],[f247]) ).
fof(f252,plain,
! [X0] :
( a_select2(s_values7_init,X0) = init
| ~ leq(X0,minus(pv1376,n1))
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f247]) ).
fof(f253,plain,
( leq(n0,sK24_skl)
| sP3_prd(sK23_skl)
| init != init ),
inference(cnf_transformation,[status(thm)],[f247]) ).
fof(f254,plain,
( leq(sK24_skl,minus(plus(n1,pv1376),n1))
| sP3_prd(sK23_skl)
| init != init ),
inference(cnf_transformation,[status(thm)],[f247]) ).
fof(f255,plain,
( a_select2(tptp_update2(s_values7_init,pv1376,init),sK24_skl) != init
| sP3_prd(sK23_skl)
| init != init ),
inference(cnf_transformation,[status(thm)],[f247]) ).
fof(f322,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)],[f245]) ).
fof(f323,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)],[f322]) ).
fof(f324,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))],[f323]) ).
fof(f325,plain,
! [X0] :
( leq(n0,X0)
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f326,plain,
! [X0] :
( leq(X0,n2)
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f327,plain,
! [X0] :
( leq(n0,sK29_skl(X0))
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f328,plain,
! [X0] :
( leq(sK29_skl(X0),n3)
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f329,plain,
! [X0] :
( a_select3(simplex7_init,sK29_skl(X0),X0) != init
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f339,definition,
( sQ0_spl
<=> init = init ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f341,plain,
( sQ0_spl
| init != init ),
inference(component_clause,[status(thm)],[f339]) ).
fof(f342,definition,
( sQ1_spl
<=> sP3_prd(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f343,plain,
( ~ sQ1_spl
| sP3_prd(sK23_skl) ),
inference(component_clause,[status(thm)],[f342]) ).
fof(f345,definition,
( sQ2_spl
<=> leq(n0,sK24_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f348,plain,
( sQ2_spl
| sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f253,f339,f342,f345]) ).
fof(f349,definition,
( sQ3_spl
<=> leq(sK24_skl,minus(plus(n1,pv1376),n1)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f350,plain,
( ~ sQ3_spl
| leq(sK24_skl,minus(plus(n1,pv1376),n1)) ),
inference(component_clause,[status(thm)],[f349]) ).
fof(f352,plain,
( sQ3_spl
| sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f254,f339,f342,f349]) ).
fof(f353,definition,
( sQ4_spl
<=> a_select2(tptp_update2(s_values7_init,pv1376,init),sK24_skl) = init ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f355,plain,
( sQ4_spl
| a_select2(tptp_update2(s_values7_init,pv1376,init),sK24_skl) != init ),
inference(component_clause,[status(thm)],[f353]) ).
fof(f356,plain,
( ~ sQ4_spl
| sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f255,f339,f342,f353]) ).
fof(f368,plain,
! [X0,X1,X2,X3] :
( a_select2(tptp_update2(X2,X0,X3),X1) = a_select2(X2,X1)
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f236]) ).
fof(f369,plain,
! [X0] :
( a_select2(s_values7_init,X0) = init
| ~ leq(X0,pred(pv1376))
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f210,f252]) ).
fof(f570,definition,
( sQ33_spl
<=> leq(n0,n0) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f572,plain,
( sQ33_spl
| ~ leq(n0,n0) ),
inference(component_clause,[status(thm)],[f570]) ).
fof(f580,plain,
( sQ0_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f341]) ).
fof(f581,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f580]) ).
fof(f587,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f572,f92]) ).
fof(f588,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f587]) ).
fof(f611,plain,
( ~ sQ3_spl
| leq(sK24_skl,pred(plus(n1,pv1376))) ),
inference(forward_demodulation,[status(thm)],[f210,f350]) ).
fof(f612,plain,
( ~ sQ3_spl
| leq(sK24_skl,pred(succ(pv1376))) ),
inference(forward_demodulation,[status(thm)],[f201,f611]) ).
fof(f613,plain,
( ~ sQ3_spl
| leq(sK24_skl,pv1376) ),
inference(forward_demodulation,[status(thm)],[f211,f612]) ).
fof(f624,plain,
( ~ sQ1_spl
| a_select3(simplex7_init,sK29_skl(sK23_skl),sK23_skl) != init ),
inference(resolution,[status(thm)],[f329,f343]) ).
fof(f625,plain,
( ~ sQ1_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)],[f624,f251]) ).
fof(f626,definition,
( sQ42_spl
<=> leq(n0,sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f628,plain,
( sQ42_spl
| ~ leq(n0,sK23_skl) ),
inference(component_clause,[status(thm)],[f626]) ).
fof(f629,definition,
( sQ43_spl
<=> leq(sK23_skl,n2) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f631,plain,
( sQ43_spl
| ~ leq(sK23_skl,n2) ),
inference(component_clause,[status(thm)],[f629]) ).
fof(f632,definition,
( sQ44_spl
<=> leq(n0,sK29_skl(sK23_skl)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f634,plain,
( sQ44_spl
| ~ leq(n0,sK29_skl(sK23_skl)) ),
inference(component_clause,[status(thm)],[f632]) ).
fof(f635,definition,
( sQ45_spl
<=> leq(sK29_skl(sK23_skl),n3) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f637,plain,
( sQ45_spl
| ~ leq(sK29_skl(sK23_skl),n3) ),
inference(component_clause,[status(thm)],[f635]) ).
fof(f638,plain,
( ~ sQ1_spl
| ~ sQ45_spl
| ~ sQ44_spl
| ~ sQ43_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f625,f626,f629,f632,f635,f342]) ).
fof(f639,plain,
( sQ43_spl
| ~ sP3_prd(sK23_skl) ),
inference(resolution,[status(thm)],[f631,f326]) ).
fof(f643,plain,
( sQ43_spl
| ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f639,f343]) ).
fof(f644,plain,
( sQ43_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f643]) ).
fof(f645,plain,
( sQ4_spl
| pv1376 = sK24_skl
| a_select2(s_values7_init,sK24_skl) != init ),
inference(paramodulation,[status(thm)],[f368,f355]) ).
fof(f646,definition,
( sQ46_spl
<=> a_select2(s_values7_init,sK24_skl) = init ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f648,plain,
( sQ46_spl
| a_select2(s_values7_init,sK24_skl) != init ),
inference(component_clause,[status(thm)],[f646]) ).
fof(f649,definition,
( sQ47_spl
<=> pv1376 = sK24_skl ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f650,plain,
( ~ sQ47_spl
| pv1376 = sK24_skl ),
inference(component_clause,[status(thm)],[f649]) ).
fof(f652,plain,
( sQ4_spl
| sQ47_spl
| ~ sQ46_spl ),
inference(split_clause,[status(thm)],[f645,f646,f649,f353]) ).
fof(f657,definition,
( sQ48_spl
<=> leq(n0,pv1376) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f659,plain,
( sQ48_spl
| ~ leq(n0,pv1376) ),
inference(component_clause,[status(thm)],[f657]) ).
fof(f664,plain,
( sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f659,f249]) ).
fof(f665,plain,
sQ48_spl,
inference(contradiction_clause,[status(thm)],[f664]) ).
fof(f669,plain,
( sQ46_spl
| ~ leq(sK24_skl,pred(pv1376))
| ~ leq(n0,sK24_skl) ),
inference(resolution,[status(thm)],[f648,f369]) ).
fof(f670,definition,
( sQ50_spl
<=> leq(sK24_skl,pred(pv1376)) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f672,plain,
( sQ50_spl
| ~ leq(sK24_skl,pred(pv1376)) ),
inference(component_clause,[status(thm)],[f670]) ).
fof(f673,plain,
( sQ46_spl
| ~ sQ50_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f669,f345,f670,f646]) ).
fof(f674,plain,
( sQ45_spl
| ~ sP3_prd(sK23_skl) ),
inference(resolution,[status(thm)],[f637,f328]) ).
fof(f678,plain,
( sQ45_spl
| ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f674,f343]) ).
fof(f679,plain,
( sQ45_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f678]) ).
fof(f680,plain,
( sQ44_spl
| ~ sP3_prd(sK23_skl) ),
inference(resolution,[status(thm)],[f634,f327]) ).
fof(f685,plain,
( sQ44_spl
| ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f680,f343]) ).
fof(f686,plain,
( sQ44_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f685]) ).
fof(f687,plain,
( sQ42_spl
| ~ sP3_prd(sK23_skl) ),
inference(resolution,[status(thm)],[f628,f325]) ).
fof(f691,plain,
( sQ42_spl
| ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f687,f343]) ).
fof(f692,plain,
( sQ42_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f691]) ).
fof(f696,plain,
( sQ4_spl
| ~ sQ47_spl
| a_select2(tptp_update2(s_values7_init,pv1376,init),pv1376) != init ),
inference(forward_demodulation,[status(thm)],[f650,f355]) ).
fof(f697,plain,
( sQ4_spl
| ~ sQ47_spl
| init != init ),
inference(forward_demodulation,[status(thm)],[f233,f696]) ).
fof(f698,plain,
( sQ4_spl
| ~ sQ47_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f697]) ).
fof(f699,plain,
( sQ4_spl
| ~ sQ47_spl ),
inference(contradiction_clause,[status(thm)],[f698]) ).
fof(f712,plain,
( sQ50_spl
| ~ gt(pv1376,sK24_skl) ),
inference(resolution,[status(thm)],[f672,f111]) ).
fof(f717,plain,
( sQ50_spl
| sK24_skl = pv1376
| ~ leq(sK24_skl,pv1376) ),
inference(resolution,[status(thm)],[f712,f107]) ).
fof(f721,definition,
( sQ51_spl
<=> leq(sK24_skl,pv1376) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f723,plain,
( sQ51_spl
| ~ leq(sK24_skl,pv1376) ),
inference(component_clause,[status(thm)],[f721]) ).
fof(f724,plain,
( sQ50_spl
| sQ47_spl
| ~ sQ51_spl ),
inference(split_clause,[status(thm)],[f717,f721,f649,f670]) ).
fof(f729,plain,
( sQ51_spl
| ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f723,f613]) ).
fof(f730,plain,
( sQ51_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f729]) ).
fof(f731,plain,
$false,
inference(sat_refutation,[status(thm)],[f348,f352,f356,f581,f588,f638,f644,f652,f665,f673,f679,f686,f692,f699,f724,f730]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV033+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n013.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 08:27:05 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.49 % Drodi V4.1.1
% 0.26/0.72 % Refutation found
% 0.26/0.72 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.26/0.72 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.26/0.76 % Elapsed time: 0.292248 seconds
% 0.26/0.76 % CPU time: 1.503291 seconds
% 0.26/0.76 % Total memory used: 121.416 MB
% 0.26/0.76 % Net memory used: 119.507 MB
%------------------------------------------------------------------------------