%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV032+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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 45.02s 6.41s
% Output : CNFRefutation 45.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 40
% Syntax : Number of formulae : 190 ( 59 unt; 26 def)
% Number of atoms : 610 ( 115 equ)
% Maximal formula atoms : 32 ( 3 avg)
% Number of connectives : 685 ( 265 ~; 271 |; 107 &)
% ( 26 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 26 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 16 con; 0-3 aty)
% Number of variables : 106 ( 98 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X] : ~ gt(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : leq(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y] :
( gt(Y,X)
=> leq(X,Y) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [Body] : sum(n0,tptp_minus_1,Body) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [Body] : tptp_float_0_0 = sum(n0,tptp_minus_1,Body),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [X] : minus(X,n1) = pred(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [X] : succ(pred(X)) = X,
file('/export/starexec/sandbox2/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(pv20,minus(n330,n1))
& leq(pv19,minus(n410,n1))
& leq(n0,pv1376)
& leq(n0,pv20)
& leq(n0,pv19)
& 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(pv19,minus(n410,n1))
& leq(n0,pv1376)
& leq(n0,pv19)
& a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) = init
& a_select3(simplex7_init,pv1376,n2) = init
& a_select3(simplex7_init,pv1376,n1) = init
& a_select3(simplex7_init,pv1376,n0) = init
& init = init ) ),
file('/export/starexec/sandbox2/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(n0,pv1376)
& leq(n0,pv20)
& leq(n0,pv19)
& 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(pv19,minus(n410,n1))
& leq(n0,pv1376)
& leq(n0,pv19)
& a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) = init
& a_select3(simplex7_init,pv1376,n2) = init
& a_select3(simplex7_init,pv1376,n1) = init
& a_select3(simplex7_init,pv1376,n0) = init
& init = init ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f73,axiom,
gt(n1,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f74,axiom,
gt(n2,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f79,axiom,
gt(n410,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,axiom,
gt(n2,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f99,axiom,
succ(n0) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f106,plain,
! [X0] : ~ gt(X0,X0),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f107,plain,
! [X0] : leq(X0,X0),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f119,plain,
! [X,Y] :
( leq(X,Y)
| ~ gt(Y,X) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f120,plain,
! [X0,X1] :
( leq(X1,X0)
| ~ gt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
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] :
( ~ leq(X3,X6)
| ~ leq(X1,X2)
| ~ leq(X6,X4)
| a_select3(tptp_const_array2(dim(X0,X2),dim(X3,X4),X5),X1,X6) = X5
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f212,plain,
! [X0] : sum(n0,tptp_minus_1,X0) = n0,
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f213,plain,
! [X0] : tptp_float_0_0 = sum(n0,tptp_minus_1,X0),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f225,plain,
! [X0] : minus(X0,n1) = pred(X0),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f227,plain,
! [X0] : X0 = succ(pred(X0)),
inference(cnf_transformation,[status(thm)],[f41]) ).
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(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| 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(n0,pv1376)
& leq(n0,pv20)
& leq(n0,pv19)
& 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(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| 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(n0,pv1376)
& leq(n0,pv20)
& leq(n0,pv19)
& 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(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| 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(n0,pv1376)
& leq(n0,pv20)
& leq(n0,pv19)
& 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,pv19),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f265,plain,
leq(n0,pv20),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f266,plain,
leq(n0,pv1376),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f267,plain,
leq(pv19,minus(n410,n1)),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f268,plain,
leq(pv20,minus(n330,n1)),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f269,plain,
leq(pv1376,n3),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f270,plain,
! [X0,X1] :
( ~ leq(X1,n3)
| ~ leq(X0,n2)
| a_select3(simplex7_init,X1,X0) = init
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f271,plain,
! [X0] :
( a_select2(s_values7_init,X0) = init
| ~ leq(X0,minus(pv1376,n1))
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f272,plain,
( leq(n0,sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| init != init ),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f273,plain,
( leq(sK24_skl,minus(pv1376,n1))
| sP3_prd(sK23_skl)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| init != init ),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f274,plain,
( a_select2(s_values7_init,sK24_skl) != init
| sP3_prd(sK23_skl)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| init != init ),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f293,plain,
gt(n1,n0),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f294,plain,
gt(n2,n0),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f299,plain,
gt(n410,n1),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f300,plain,
gt(n2,n1),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f325,plain,
succ(n0) = n1,
inference(cnf_transformation,[status(thm)],[f99]) ).
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) )
& ( ( ? [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(f357,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)],[f356]) ).
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) )
& ! [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))],[f357]) ).
fof(f359,plain,
! [X0] :
( ~ sP3_prd(X0)
| leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f358]) ).
fof(f360,plain,
! [X0] :
( ~ sP3_prd(X0)
| leq(X0,n2) ),
inference(cnf_transformation,[status(thm)],[f358]) ).
fof(f361,plain,
! [X0] :
( leq(n0,sK29_skl(X0))
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f358]) ).
fof(f362,plain,
! [X0] :
( ~ sP3_prd(X0)
| leq(sK29_skl(X0),n3) ),
inference(cnf_transformation,[status(thm)],[f358]) ).
fof(f363,plain,
! [X0] :
( ~ sP3_prd(X0)
| a_select3(simplex7_init,sK29_skl(X0),X0) != init ),
inference(cnf_transformation,[status(thm)],[f358]) ).
fof(f373,definition,
( sQ0_spl
<=> init = init ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f375,plain,
( sQ0_spl
| init != init ),
inference(component_clause,[status(thm)],[f373]) ).
fof(f376,definition,
( sQ1_spl
<=> a_select3(simplex7_init,pv1376,n0) = init ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f378,plain,
( sQ1_spl
| a_select3(simplex7_init,pv1376,n0) != init ),
inference(component_clause,[status(thm)],[f376]) ).
fof(f379,definition,
( sQ2_spl
<=> a_select3(simplex7_init,pv1376,n1) = init ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f381,plain,
( sQ2_spl
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(component_clause,[status(thm)],[f379]) ).
fof(f382,definition,
( sQ3_spl
<=> a_select3(simplex7_init,pv1376,n2) = init ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f384,plain,
( sQ3_spl
| init != a_select3(simplex7_init,pv1376,n2) ),
inference(component_clause,[status(thm)],[f382]) ).
fof(f385,definition,
( sQ4_spl
<=> a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) = init ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f387,plain,
( sQ4_spl
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init ),
inference(component_clause,[status(thm)],[f385]) ).
fof(f388,definition,
( sQ5_spl
<=> leq(n0,pv19) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f390,plain,
( sQ5_spl
| ~ leq(n0,pv19) ),
inference(component_clause,[status(thm)],[f388]) ).
fof(f391,definition,
( sQ6_spl
<=> leq(n0,pv1376) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f393,plain,
( sQ6_spl
| ~ leq(n0,pv1376) ),
inference(component_clause,[status(thm)],[f391]) ).
fof(f394,definition,
( sQ7_spl
<=> leq(pv19,minus(n410,n1)) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f396,plain,
( sQ7_spl
| ~ leq(pv19,minus(n410,n1)) ),
inference(component_clause,[status(thm)],[f394]) ).
fof(f397,definition,
( sQ8_spl
<=> leq(pv1376,n3) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f399,plain,
( sQ8_spl
| ~ leq(pv1376,n3) ),
inference(component_clause,[status(thm)],[f397]) ).
fof(f400,definition,
( sQ9_spl
<=> sP3_prd(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f401,plain,
( ~ sQ9_spl
| sP3_prd(sK23_skl) ),
inference(component_clause,[status(thm)],[f400]) ).
fof(f403,definition,
( sQ10_spl
<=> leq(n0,sK24_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f404,plain,
( ~ sQ10_spl
| leq(n0,sK24_skl) ),
inference(component_clause,[status(thm)],[f403]) ).
fof(f406,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)],[f272,f373,f376,f379,f382,f385,f388,f391,f394,f397,f400,f403]) ).
fof(f407,definition,
( sQ11_spl
<=> leq(sK24_skl,minus(pv1376,n1)) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f408,plain,
( ~ sQ11_spl
| leq(sK24_skl,minus(pv1376,n1)) ),
inference(component_clause,[status(thm)],[f407]) ).
fof(f410,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)],[f273,f373,f376,f379,f382,f385,f388,f391,f394,f397,f400,f407]) ).
fof(f411,definition,
( sQ12_spl
<=> a_select2(s_values7_init,sK24_skl) = init ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f414,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)],[f274,f373,f376,f379,f382,f385,f388,f391,f394,f397,f400,f411]) ).
fof(f417,plain,
! [X0] :
( init = a_select2(s_values7_init,X0)
| ~ leq(n0,X0)
| ~ leq(X0,pred(pv1376)) ),
inference(forward_demodulation,[status(thm)],[f225,f271]) ).
fof(f421,plain,
tptp_float_0_0 = n0,
inference(backward_demodulation,[status(thm)],[f213,f212]) ).
fof(f423,plain,
leq(pv20,pred(n330)),
inference(forward_demodulation,[status(thm)],[f225,f268]) ).
fof(f432,plain,
gt(n1,tptp_float_0_0),
inference(backward_demodulation,[status(thm)],[f421,f293]) ).
fof(f436,plain,
! [X0,X1] :
( ~ leq(X1,n3)
| ~ leq(X0,n2)
| a_select3(simplex7_init,X1,X0) = init
| ~ leq(tptp_float_0_0,X1)
| ~ leq(n0,X0) ),
inference(backward_demodulation,[status(thm)],[f421,f270]) ).
fof(f443,plain,
! [X0] :
( ~ sP3_prd(X0)
| leq(tptp_float_0_0,X0) ),
inference(backward_demodulation,[status(thm)],[f421,f359]) ).
fof(f446,plain,
leq(tptp_float_0_0,pv20),
inference(backward_demodulation,[status(thm)],[f421,f265]) ).
fof(f449,plain,
! [X0] :
( leq(tptp_float_0_0,sK29_skl(X0))
| ~ sP3_prd(X0) ),
inference(backward_demodulation,[status(thm)],[f421,f361]) ).
fof(f464,plain,
gt(n2,tptp_float_0_0),
inference(backward_demodulation,[status(thm)],[f421,f294]) ).
fof(f465,plain,
! [X0] :
( ~ leq(X0,pred(pv1376))
| init = a_select2(s_values7_init,X0)
| ~ leq(tptp_float_0_0,X0) ),
inference(backward_demodulation,[status(thm)],[f421,f417]) ).
fof(f477,plain,
leq(tptp_float_0_0,pv1376),
inference(backward_demodulation,[status(thm)],[f421,f266]) ).
fof(f515,plain,
! [X0,X1] :
( ~ leq(X1,n2)
| ~ leq(tptp_float_0_0,X0)
| ~ leq(tptp_float_0_0,X1)
| ~ leq(X0,n3)
| a_select3(simplex7_init,X0,X1) = init ),
inference(forward_demodulation,[status(thm)],[f421,f436]) ).
fof(f562,plain,
n1 = succ(tptp_float_0_0),
inference(forward_demodulation,[status(thm)],[f421,f325]) ).
fof(f563,plain,
leq(pv19,pred(n410)),
inference(forward_demodulation,[status(thm)],[f225,f267]) ).
fof(f592,plain,
leq(tptp_float_0_0,pv19),
inference(forward_demodulation,[status(thm)],[f421,f264]) ).
fof(f618,plain,
leq(n1,n2),
inference(resolution,[status(thm)],[f120,f300]) ).
fof(f626,plain,
leq(tptp_float_0_0,n1),
inference(resolution,[status(thm)],[f432,f120]) ).
fof(f629,plain,
leq(tptp_float_0_0,n2),
inference(resolution,[status(thm)],[f464,f120]) ).
fof(f655,definition,
( sQ14_spl
<=> leq(tptp_float_0_0,tptp_float_0_0) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f657,plain,
( sQ14_spl
| ~ leq(tptp_float_0_0,tptp_float_0_0) ),
inference(component_clause,[status(thm)],[f655]) ).
fof(f669,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f399,f269]) ).
fof(f670,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f669]) ).
fof(f671,plain,
( sQ6_spl
| ~ leq(tptp_float_0_0,pv1376) ),
inference(forward_demodulation,[status(thm)],[f421,f393]) ).
fof(f672,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f671,f477]) ).
fof(f673,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f672]) ).
fof(f674,plain,
( sQ1_spl
| init != a_select3(simplex7_init,pv1376,tptp_float_0_0) ),
inference(forward_demodulation,[status(thm)],[f421,f378]) ).
fof(f675,plain,
( sQ5_spl
| ~ leq(tptp_float_0_0,pv19) ),
inference(forward_demodulation,[status(thm)],[f421,f390]) ).
fof(f676,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f675,f592]) ).
fof(f677,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f676]) ).
fof(f678,plain,
( sQ4_spl
| a_select3(tptp_const_array2(dim(tptp_float_0_0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init ),
inference(forward_demodulation,[status(thm)],[f421,f387]) ).
fof(f679,plain,
( sQ4_spl
| a_select3(tptp_const_array2(dim(tptp_float_0_0,pred(n410)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init ),
inference(forward_demodulation,[status(thm)],[f225,f678]) ).
fof(f680,plain,
( sQ4_spl
| a_select3(tptp_const_array2(dim(tptp_float_0_0,pred(n410)),dim(tptp_float_0_0,minus(n330,n1)),init),pv19,pv20) != init ),
inference(forward_demodulation,[status(thm)],[f421,f679]) ).
fof(f681,plain,
( sQ4_spl
| a_select3(tptp_const_array2(dim(tptp_float_0_0,pred(n410)),dim(tptp_float_0_0,pred(n330)),init),pv19,pv20) != init ),
inference(forward_demodulation,[status(thm)],[f225,f680]) ).
fof(f682,plain,
( sQ0_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f375]) ).
fof(f683,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f682]) ).
fof(f685,plain,
( sQ7_spl
| ~ leq(pv19,pred(n410)) ),
inference(forward_demodulation,[status(thm)],[f225,f396]) ).
fof(f686,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f685,f563]) ).
fof(f687,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f686]) ).
fof(f702,plain,
! [X0] :
( ~ sP3_prd(X0)
| ~ leq(X0,n2)
| ~ leq(sK29_skl(X0),n3)
| ~ leq(tptp_float_0_0,X0)
| ~ leq(tptp_float_0_0,sK29_skl(X0)) ),
inference(resolution,[status(thm)],[f515,f363]) ).
fof(f703,plain,
! [X0] :
( ~ sP3_prd(X0)
| ~ leq(sK29_skl(X0),n3)
| ~ leq(tptp_float_0_0,X0)
| ~ leq(X0,n2) ),
inference(forward_subsumption_resolution,[status(thm)],[f702,f449]) ).
fof(f704,plain,
( sQ2_spl
| ~ leq(n1,n2)
| ~ leq(pv1376,n3)
| ~ leq(tptp_float_0_0,n1)
| ~ leq(tptp_float_0_0,pv1376) ),
inference(resolution,[status(thm)],[f381,f515]) ).
fof(f705,definition,
( sQ18_spl
<=> leq(tptp_float_0_0,pv1376) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f707,plain,
( sQ18_spl
| ~ leq(tptp_float_0_0,pv1376) ),
inference(component_clause,[status(thm)],[f705]) ).
fof(f708,definition,
( sQ19_spl
<=> leq(tptp_float_0_0,n1) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f710,plain,
( sQ19_spl
| ~ leq(tptp_float_0_0,n1) ),
inference(component_clause,[status(thm)],[f708]) ).
fof(f711,definition,
( sQ20_spl
<=> leq(n1,n2) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f713,plain,
( sQ20_spl
| ~ leq(n1,n2) ),
inference(component_clause,[status(thm)],[f711]) ).
fof(f714,plain,
( sQ2_spl
| ~ sQ20_spl
| ~ sQ8_spl
| ~ sQ19_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f704,f705,f708,f397,f711,f379]) ).
fof(f715,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f713,f618]) ).
fof(f716,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f715]) ).
fof(f717,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f707,f477]) ).
fof(f718,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f717]) ).
fof(f719,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f710,f626]) ).
fof(f720,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f719]) ).
fof(f721,plain,
( sQ1_spl
| ~ leq(tptp_float_0_0,n2)
| ~ leq(pv1376,n3)
| ~ leq(tptp_float_0_0,tptp_float_0_0)
| ~ leq(tptp_float_0_0,pv1376) ),
inference(resolution,[status(thm)],[f674,f515]) ).
fof(f722,definition,
( sQ21_spl
<=> leq(tptp_float_0_0,n2) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f724,plain,
( sQ21_spl
| ~ leq(tptp_float_0_0,n2) ),
inference(component_clause,[status(thm)],[f722]) ).
fof(f725,plain,
( sQ1_spl
| ~ sQ21_spl
| ~ sQ8_spl
| ~ sQ14_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f721,f705,f655,f397,f722,f376]) ).
fof(f726,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f657,f107]) ).
fof(f727,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f726]) ).
fof(f733,plain,
! [X0] :
( ~ sP3_prd(X0)
| ~ sP3_prd(X0)
| ~ leq(tptp_float_0_0,X0)
| ~ leq(X0,n2) ),
inference(resolution,[status(thm)],[f703,f362]) ).
fof(f734,plain,
! [X0] :
( ~ sP3_prd(X0)
| ~ leq(tptp_float_0_0,X0)
| ~ leq(X0,n2) ),
inference(duplicate_literals_removal,[status(thm)],[f733]) ).
fof(f735,plain,
! [X0] : ~ sP3_prd(X0),
inference(backward_subsumption_resolution,[status(thm)],[f443,f736]) ).
fof(f736,plain,
! [X0] :
( ~ leq(tptp_float_0_0,X0)
| ~ sP3_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f734,f360]) ).
fof(f737,plain,
( ~ sQ9_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f401,f735]) ).
fof(f738,plain,
~ sQ9_spl,
inference(contradiction_clause,[status(thm)],[f737]) ).
fof(f813,plain,
( sQ4_spl
| ~ leq(tptp_float_0_0,pv20)
| ~ leq(pv19,pred(n410))
| ~ leq(pv20,pred(n330))
| ~ leq(tptp_float_0_0,pv19) ),
inference(resolution,[status(thm)],[f681,f145]) ).
fof(f814,definition,
( sQ22_spl
<=> leq(tptp_float_0_0,pv19) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f816,plain,
( sQ22_spl
| ~ leq(tptp_float_0_0,pv19) ),
inference(component_clause,[status(thm)],[f814]) ).
fof(f817,definition,
( sQ23_spl
<=> leq(pv20,pred(n330)) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f819,plain,
( sQ23_spl
| ~ leq(pv20,pred(n330)) ),
inference(component_clause,[status(thm)],[f817]) ).
fof(f820,definition,
( sQ24_spl
<=> leq(pv19,pred(n410)) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f822,plain,
( sQ24_spl
| ~ leq(pv19,pred(n410)) ),
inference(component_clause,[status(thm)],[f820]) ).
fof(f823,definition,
( sQ25_spl
<=> leq(tptp_float_0_0,pv20) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f825,plain,
( sQ25_spl
| ~ leq(tptp_float_0_0,pv20) ),
inference(component_clause,[status(thm)],[f823]) ).
fof(f826,plain,
( sQ4_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f813,f814,f817,f820,f823,f385]) ).
fof(f827,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f825,f446]) ).
fof(f828,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f827]) ).
fof(f829,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f822,f563]) ).
fof(f830,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f829]) ).
fof(f831,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f819,f423]) ).
fof(f832,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f831]) ).
fof(f1015,definition,
( sQ30_spl
<=> pred(n410) = tptp_float_0_0 ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f1016,plain,
( ~ sQ30_spl
| pred(n410) = tptp_float_0_0 ),
inference(component_clause,[status(thm)],[f1015]) ).
fof(f2132,plain,
( sQ3_spl
| ~ leq(pv1376,n3)
| ~ leq(n2,n2)
| ~ leq(tptp_float_0_0,pv1376)
| ~ leq(tptp_float_0_0,n2) ),
inference(resolution,[status(thm)],[f515,f384]) ).
fof(f2134,definition,
( sQ57_spl
<=> leq(n2,n2) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f2136,plain,
( sQ57_spl
| ~ leq(n2,n2) ),
inference(component_clause,[status(thm)],[f2134]) ).
fof(f2137,plain,
( sQ3_spl
| ~ sQ8_spl
| ~ sQ57_spl
| ~ sQ18_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f2132,f722,f705,f2134,f397,f382]) ).
fof(f2139,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f724,f629]) ).
fof(f2140,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f2139]) ).
fof(f2141,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f816,f592]) ).
fof(f2142,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f2141]) ).
fof(f2177,plain,
( sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2136,f107]) ).
fof(f2178,plain,
sQ57_spl,
inference(contradiction_clause,[status(thm)],[f2177]) ).
fof(f2179,plain,
( ~ sQ10_spl
| leq(tptp_float_0_0,sK24_skl) ),
inference(forward_demodulation,[status(thm)],[f421,f404]) ).
fof(f2181,plain,
( ~ sQ11_spl
| leq(sK24_skl,pred(pv1376)) ),
inference(forward_demodulation,[status(thm)],[f225,f408]) ).
fof(f2193,plain,
( ~ sQ30_spl
| succ(tptp_float_0_0) = n410 ),
inference(paramodulation,[status(thm)],[f1016,f227]) ).
fof(f2194,plain,
( ~ sQ30_spl
| n1 = n410 ),
inference(backward_demodulation,[status(thm)],[f2193,f562]) ).
fof(f2200,plain,
( ~ sQ30_spl
| gt(n410,n410) ),
inference(backward_demodulation,[status(thm)],[f2194,f299]) ).
fof(f2248,plain,
( ~ sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2200,f106]) ).
fof(f2249,plain,
~ sQ30_spl,
inference(contradiction_clause,[status(thm)],[f2248]) ).
fof(f2580,plain,
( ~ sQ11_spl
| init = a_select2(s_values7_init,sK24_skl)
| ~ leq(tptp_float_0_0,sK24_skl) ),
inference(resolution,[status(thm)],[f465,f2181]) ).
fof(f2583,definition,
( sQ60_spl
<=> leq(tptp_float_0_0,sK24_skl) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f2585,plain,
( sQ60_spl
| ~ leq(tptp_float_0_0,sK24_skl) ),
inference(component_clause,[status(thm)],[f2583]) ).
fof(f2586,plain,
( ~ sQ11_spl
| sQ12_spl
| ~ sQ60_spl ),
inference(split_clause,[status(thm)],[f2580,f2583,f411,f407]) ).
fof(f2589,plain,
( sQ60_spl
| ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2585,f2179]) ).
fof(f2590,plain,
( sQ60_spl
| ~ sQ10_spl ),
inference(contradiction_clause,[status(thm)],[f2589]) ).
fof(f2591,plain,
$false,
inference(sat_refutation,[status(thm)],[f406,f410,f414,f670,f673,f677,f683,f687,f714,f716,f718,f720,f725,f727,f738,f826,f828,f830,f832,f2137,f2140,f2142,f2178,f2249,f2586,f2590]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV032+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n002.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.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 08:30:17 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.15/0.42 % Drodi V4.1.1
% 45.02/6.41 % Refutation found
% 45.02/6.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 45.02/6.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 45.02/6.49 % Elapsed time: 6.099222 seconds
% 45.02/6.49 % CPU time: 47.543170 seconds
% 45.02/6.49 % Total memory used: 250.232 MB
% 45.02/6.49 % Net memory used: 223.402 MB
%------------------------------------------------------------------------------