%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV031+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 : n016.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.15s 5.54s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 21
% Syntax : Number of formulae : 100 ( 18 unt; 17 def)
% Number of atoms : 378 ( 65 equ)
% Maximal formula atoms : 25 ( 3 avg)
% Number of connectives : 432 ( 154 ~; 159 |; 87 &)
% ( 17 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 17 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 13 con; 0-3 aty)
% Number of variables : 78 ( 70 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X] : leq(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [I,L1,U1,J,L2,U2,Val] :
( ( leq(J,U2)
& leq(L2,J)
& leq(I,U1)
& leq(L1,I) )
=> a_select3(tptp_const_array2(dim(L1,U1),dim(L2,U2),Val),I,J) = Val ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [X] : minus(X,n1) = pred(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,conjecture,
( ( ! [C] :
( ( leq(C,n3)
& 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(pv10,minus(n330,n1))
& leq(pv9,minus(n410,n1))
& leq(n0,pv10)
& leq(n0,pv9)
& init = init )
=> ( ! [F] :
( ( leq(F,n3)
& 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(pv9,minus(n410,n1))
& leq(n0,pv9)
& a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv9,pv10) = init
& init = init ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
~ ( ( ! [C] :
( ( leq(C,n3)
& 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(pv10,minus(n330,n1))
& leq(pv9,minus(n410,n1))
& leq(n0,pv10)
& leq(n0,pv9)
& init = init )
=> ( ! [F] :
( ( leq(F,n3)
& 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(pv9,minus(n410,n1))
& leq(n0,pv9)
& a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv9,pv10) = init
& init = init ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f107,plain,
! [X0] : leq(X0,X0),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f143,plain,
! [I,L1,U1,J,L2,U2,Val] :
( a_select3(tptp_const_array2(dim(L1,U1),dim(L2,U2),Val),I,J) = Val
| ~ leq(J,U2)
| ~ leq(L2,J)
| ~ leq(I,U1)
| ~ leq(L1,I) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f144,plain,
! [I,L1,U1,J,L2,U2] :
( ! [Val] : a_select3(tptp_const_array2(dim(L1,U1),dim(L2,U2),Val),I,J) = Val
| ~ leq(J,U2)
| ~ leq(L2,J)
| ~ leq(I,U1)
| ~ leq(L1,I) ),
inference(miniscoping,[status(thm)],[f143]) ).
fof(f145,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( a_select3(tptp_const_array2(dim(X0,X2),dim(X3,X5),X6),X1,X4) = X6
| ~ leq(X4,X5)
| ~ leq(X3,X4)
| ~ leq(X1,X2)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f225,plain,
! [X0] : minus(X0,n1) = pred(X0),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f259,plain,
( ( ? [F] :
( a_select2(s_values7_init,F) != init
& leq(F,n3)
& 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(pv9,minus(n410,n1))
| ~ leq(n0,pv9)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv9,pv10) != init
| init != init )
& ! [C] :
( a_select2(s_values7_init,C) = init
| ~ leq(C,n3)
| ~ 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(pv10,minus(n330,n1))
& leq(pv9,minus(n410,n1))
& leq(n0,pv10)
& leq(n0,pv9)
& 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,n3)
& leq(n0,F) )
| ? [D] : sP3_prd(D)
| ~ leq(pv9,minus(n410,n1))
| ~ leq(n0,pv9)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv9,pv10) != init
| init != init )
& ! [C] :
( a_select2(s_values7_init,C) = init
| ~ leq(C,n3)
| ~ 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(pv10,minus(n330,n1))
& leq(pv9,minus(n410,n1))
& leq(n0,pv10)
& leq(n0,pv9)
& init = init ),
inference(formula_renaming,[status(thm)],[f259,f260]) ).
fof(f262,plain,
( ( ( a_select2(s_values7_init,sK24_skl) != init
& leq(sK24_skl,n3)
& leq(n0,sK24_skl) )
| sP3_prd(sK23_skl)
| ~ leq(pv9,minus(n410,n1))
| ~ leq(n0,pv9)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv9,pv10) != init
| init != init )
& ! [C] :
( a_select2(s_values7_init,C) = init
| ~ leq(C,n3)
| ~ 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(pv10,minus(n330,n1))
& leq(pv9,minus(n410,n1))
& leq(n0,pv10)
& leq(n0,pv9)
& 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,pv9),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f265,plain,
leq(n0,pv10),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f266,plain,
leq(pv9,minus(n410,n1)),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f267,plain,
leq(pv10,minus(n330,n1)),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f268,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(f269,plain,
! [X0] :
( a_select2(s_values7_init,X0) = init
| ~ leq(X0,n3)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f270,plain,
( leq(n0,sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(pv9,minus(n410,n1))
| ~ leq(n0,pv9)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv9,pv10) != init
| init != init ),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f271,plain,
( leq(sK24_skl,n3)
| sP3_prd(sK23_skl)
| ~ leq(pv9,minus(n410,n1))
| ~ leq(n0,pv9)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv9,pv10) != init
| init != init ),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f272,plain,
( a_select2(s_values7_init,sK24_skl) != init
| sP3_prd(sK23_skl)
| ~ leq(pv9,minus(n410,n1))
| ~ leq(n0,pv9)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv9,pv10) != init
| init != init ),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f354,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(f355,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)],[f354]) ).
fof(f356,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))],[f355]) ).
fof(f357,plain,
! [X0] :
( leq(n0,X0)
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f356]) ).
fof(f358,plain,
! [X0] :
( leq(X0,n2)
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f356]) ).
fof(f359,plain,
! [X0] :
( leq(n0,sK29_skl(X0))
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f356]) ).
fof(f360,plain,
! [X0] :
( leq(sK29_skl(X0),n3)
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f356]) ).
fof(f361,plain,
! [X0] :
( a_select3(simplex7_init,sK29_skl(X0),X0) != init
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f356]) ).
fof(f371,definition,
( sQ0_spl
<=> init = init ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f373,plain,
( sQ0_spl
| init != init ),
inference(component_clause,[status(thm)],[f371]) ).
fof(f374,definition,
( sQ1_spl
<=> a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv9,pv10) = init ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f376,plain,
( sQ1_spl
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv9,pv10) != init ),
inference(component_clause,[status(thm)],[f374]) ).
fof(f377,definition,
( sQ2_spl
<=> leq(n0,pv9) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f379,plain,
( sQ2_spl
| ~ leq(n0,pv9) ),
inference(component_clause,[status(thm)],[f377]) ).
fof(f380,definition,
( sQ3_spl
<=> leq(pv9,minus(n410,n1)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f382,plain,
( sQ3_spl
| ~ leq(pv9,minus(n410,n1)) ),
inference(component_clause,[status(thm)],[f380]) ).
fof(f383,definition,
( sQ4_spl
<=> sP3_prd(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f384,plain,
( ~ sQ4_spl
| sP3_prd(sK23_skl) ),
inference(component_clause,[status(thm)],[f383]) ).
fof(f386,definition,
( sQ5_spl
<=> leq(n0,sK24_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f389,plain,
( sQ5_spl
| sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f270,f371,f374,f377,f380,f383,f386]) ).
fof(f390,definition,
( sQ6_spl
<=> leq(sK24_skl,n3) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f393,plain,
( sQ6_spl
| sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f271,f371,f374,f377,f380,f383,f390]) ).
fof(f394,definition,
( sQ7_spl
<=> a_select2(s_values7_init,sK24_skl) = init ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f396,plain,
( sQ7_spl
| a_select2(s_values7_init,sK24_skl) != init ),
inference(component_clause,[status(thm)],[f394]) ).
fof(f397,plain,
( ~ sQ7_spl
| sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f272,f371,f374,f377,f380,f383,f394]) ).
fof(f410,plain,
leq(pv9,pred(n410)),
inference(forward_demodulation,[status(thm)],[f225,f266]) ).
fof(f411,plain,
leq(pv10,pred(n330)),
inference(forward_demodulation,[status(thm)],[f225,f267]) ).
fof(f517,plain,
( sQ3_spl
| ~ leq(pv9,pred(n410)) ),
inference(forward_demodulation,[status(thm)],[f225,f382]) ).
fof(f518,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f517,f410]) ).
fof(f519,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f518]) ).
fof(f520,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f379,f264]) ).
fof(f521,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f520]) ).
fof(f522,plain,
( sQ1_spl
| a_select3(tptp_const_array2(dim(n0,pred(n410)),dim(n0,minus(n330,n1)),init),pv9,pv10) != init ),
inference(forward_demodulation,[status(thm)],[f225,f376]) ).
fof(f523,plain,
( sQ1_spl
| a_select3(tptp_const_array2(dim(n0,pred(n410)),dim(n0,pred(n330)),init),pv9,pv10) != init ),
inference(forward_demodulation,[status(thm)],[f225,f522]) ).
fof(f524,plain,
( sQ0_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f373]) ).
fof(f525,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f524]) ).
fof(f623,definition,
( sQ37_spl
<=> leq(n0,n0) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f625,plain,
( sQ37_spl
| ~ leq(n0,n0) ),
inference(component_clause,[status(thm)],[f623]) ).
fof(f643,plain,
( sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f625,f107]) ).
fof(f644,plain,
sQ37_spl,
inference(contradiction_clause,[status(thm)],[f643]) ).
fof(f656,plain,
( ~ sQ4_spl
| a_select3(simplex7_init,sK29_skl(sK23_skl),sK23_skl) != init ),
inference(resolution,[status(thm)],[f361,f384]) ).
fof(f657,plain,
( ~ sQ4_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)],[f656,f268]) ).
fof(f658,definition,
( sQ44_spl
<=> leq(n0,sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f660,plain,
( sQ44_spl
| ~ leq(n0,sK23_skl) ),
inference(component_clause,[status(thm)],[f658]) ).
fof(f661,definition,
( sQ45_spl
<=> leq(sK23_skl,n2) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f663,plain,
( sQ45_spl
| ~ leq(sK23_skl,n2) ),
inference(component_clause,[status(thm)],[f661]) ).
fof(f664,definition,
( sQ46_spl
<=> leq(n0,sK29_skl(sK23_skl)) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f666,plain,
( sQ46_spl
| ~ leq(n0,sK29_skl(sK23_skl)) ),
inference(component_clause,[status(thm)],[f664]) ).
fof(f667,definition,
( sQ47_spl
<=> leq(sK29_skl(sK23_skl),n3) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f669,plain,
( sQ47_spl
| ~ leq(sK29_skl(sK23_skl),n3) ),
inference(component_clause,[status(thm)],[f667]) ).
fof(f670,plain,
( ~ sQ4_spl
| ~ sQ47_spl
| ~ sQ46_spl
| ~ sQ45_spl
| ~ sQ44_spl ),
inference(split_clause,[status(thm)],[f657,f658,f661,f664,f667,f383]) ).
fof(f671,plain,
( sQ45_spl
| ~ sP3_prd(sK23_skl) ),
inference(resolution,[status(thm)],[f663,f358]) ).
fof(f675,plain,
( sQ45_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f671,f384]) ).
fof(f676,plain,
( sQ45_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f675]) ).
fof(f677,plain,
( sQ7_spl
| ~ leq(sK24_skl,n3)
| ~ leq(n0,sK24_skl) ),
inference(resolution,[status(thm)],[f269,f396]) ).
fof(f678,plain,
( sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f677,f386,f390,f394]) ).
fof(f679,plain,
( sQ1_spl
| ~ leq(pv10,pred(n330))
| ~ leq(n0,pv10)
| ~ leq(pv9,pred(n410))
| ~ leq(n0,pv9) ),
inference(resolution,[status(thm)],[f523,f145]) ).
fof(f680,definition,
( sQ48_spl
<=> leq(pv9,pred(n410)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f682,plain,
( sQ48_spl
| ~ leq(pv9,pred(n410)) ),
inference(component_clause,[status(thm)],[f680]) ).
fof(f683,definition,
( sQ49_spl
<=> leq(n0,pv10) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f685,plain,
( sQ49_spl
| ~ leq(n0,pv10) ),
inference(component_clause,[status(thm)],[f683]) ).
fof(f686,definition,
( sQ50_spl
<=> leq(pv10,pred(n330)) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f688,plain,
( sQ50_spl
| ~ leq(pv10,pred(n330)) ),
inference(component_clause,[status(thm)],[f686]) ).
fof(f689,plain,
( sQ1_spl
| ~ sQ50_spl
| ~ sQ49_spl
| ~ sQ48_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f679,f377,f680,f683,f686,f374]) ).
fof(f690,plain,
( sQ50_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f688,f411]) ).
fof(f691,plain,
sQ50_spl,
inference(contradiction_clause,[status(thm)],[f690]) ).
fof(f692,plain,
( sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f685,f265]) ).
fof(f693,plain,
sQ49_spl,
inference(contradiction_clause,[status(thm)],[f692]) ).
fof(f694,plain,
( sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f682,f410]) ).
fof(f695,plain,
sQ48_spl,
inference(contradiction_clause,[status(thm)],[f694]) ).
fof(f743,plain,
( sQ44_spl
| ~ sP3_prd(sK23_skl) ),
inference(resolution,[status(thm)],[f660,f357]) ).
fof(f748,plain,
( sQ44_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f743,f383,f658]) ).
fof(f838,plain,
( sQ47_spl
| ~ sP3_prd(sK23_skl) ),
inference(resolution,[status(thm)],[f669,f360]) ).
fof(f842,plain,
( sQ47_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f838,f383,f667]) ).
fof(f843,plain,
( sQ46_spl
| ~ sP3_prd(sK23_skl) ),
inference(resolution,[status(thm)],[f666,f359]) ).
fof(f849,plain,
( sQ46_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f843,f383,f664]) ).
fof(f850,plain,
$false,
inference(sat_refutation,[status(thm)],[f389,f393,f397,f519,f521,f525,f644,f670,f676,f678,f689,f691,f693,f695,f748,f842,f849]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV031+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/5.38 % Computer : n016.cluster.edu
% 0.12/5.38 % Model : x86_64 x86_64
% 0.12/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.38 % Memory : 8046.5625MB
% 0.12/5.38 % OS : Linux 6.8.0-71-generic
% 0.12/5.38 % CPULimit : 300
% 0.12/5.38 % WCLimit : 300
% 0.12/5.38 % DateTime : Mon Sep 21 08:32:43 UTC 2026
% 0.12/5.39 % CPUTime :
% 0.12/5.40 % Drodi V4.1.1
% 0.15/5.54 % Refutation found
% 0.15/5.54 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/5.54 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/5.57 % Elapsed time: 0.165264 seconds
% 0.15/5.57 % CPU time: 1.106079 seconds
% 0.15/5.57 % Total memory used: 123.356 MB
% 0.15/5.57 % Net memory used: 121.233 MB
%------------------------------------------------------------------------------