%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV042+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 : n003.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:30 PM UTC 2026
% Result : Theorem 0.83s 0.53s
% Output : CNFRefutation 0.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 36
% Syntax : Number of formulae : 142 ( 13 unt; 26 def)
% Number of atoms : 520 ( 105 equ)
% Maximal formula atoms : 30 ( 3 avg)
% Number of connectives : 577 ( 199 ~; 210 |; 115 &)
% ( 29 <=>; 24 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 26 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 15 con; 0-3 aty)
% Number of variables : 114 ( 94 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] :
( X = Y
| gt(Y,X)
| gt(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
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(f5,axiom,
! [X,Y,Z] :
( ( leq(Y,Z)
& leq(X,Y) )
=> leq(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,Y] :
( ( X != Y
& leq(X,Y) )
=> gt(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X,Y] :
( leq(X,Y)
<=> gt(succ(Y),X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [X] : plus(n1,X) = succ(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [X] : minus(X,n1) = pred(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [X] : pred(succ(X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,conjecture,
( ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [D] :
( ( leq(D,minus(plus(n1,n2),n1))
& leq(n0,D) )
=> a_select2(s_center7_init,D) = init )
& ! [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 ) ) )
=> ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [H] :
( ( leq(H,n2)
& leq(n0,H) )
=> a_select2(s_center7_init,H) = init )
& ! [G] :
( ( leq(G,n3)
& leq(n0,G) )
=> a_select2(s_values7_init,G) = init )
& ! [E] :
( ( leq(E,n2)
& leq(n0,E) )
=> ! [F] :
( ( leq(F,n3)
& leq(n0,F) )
=> a_select3(simplex7_init,F,E) = init ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
~ ( ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [D] :
( ( leq(D,minus(plus(n1,n2),n1))
& leq(n0,D) )
=> a_select2(s_center7_init,D) = init )
& ! [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 ) ) )
=> ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [H] :
( ( leq(H,n2)
& leq(n0,H) )
=> a_select2(s_center7_init,H) = init )
& ! [G] :
( ( leq(G,n3)
& leq(n0,G) )
=> a_select2(s_values7_init,G) = init )
& ! [E] :
( ( leq(E,n2)
& leq(n0,E) )
=> ! [F] :
( ( leq(F,n3)
& leq(n0,F) )
=> a_select3(simplex7_init,F,E) = init ) ) ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f87,plain,
! [X0,X1] :
( X0 = X1
| gt(X1,X0)
| gt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f91,plain,
! [X0] : ~ gt(X0,X0),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f92,plain,
! [X0] : leq(X0,X0),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f93,plain,
! [X,Y,Z] :
( leq(X,Z)
| ~ leq(Y,Z)
| ~ leq(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f94,plain,
! [X,Z] :
( leq(X,Z)
| ! [Y] :
( ~ leq(Y,Z)
| ~ leq(X,Y) ) ),
inference(miniscoping,[status(thm)],[f93]) ).
fof(f95,plain,
! [X0,X1,X2] :
( leq(X0,X2)
| ~ leq(X1,X2)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
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(f115,plain,
! [X,Y] :
( ( ~ gt(succ(Y),X)
| leq(X,Y) )
& ( gt(succ(Y),X)
| ~ leq(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f13]) ).
fof(f116,plain,
( ! [X,Y] :
( ~ gt(succ(Y),X)
| leq(X,Y) )
& ! [X,Y] :
( gt(succ(Y),X)
| ~ leq(X,Y) ) ),
inference(miniscoping,[status(thm)],[f115]) ).
fof(f118,plain,
! [X0,X1] :
( ~ gt(succ(X1),X0)
| leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
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(f244,plain,
( ( ( ( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init )
& gt(loopcounter,n1) )
| ? [H] :
( a_select2(s_center7_init,H) != init
& leq(H,n2)
& leq(n0,H) )
| ? [G] :
( a_select2(s_values7_init,G) != init
& leq(G,n3)
& leq(n0,G) )
| ? [E] :
( ? [F] :
( a_select3(simplex7_init,F,E) != init
& leq(F,n3)
& leq(n0,F) )
& leq(E,n2)
& leq(n0,E) ) )
& ( ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init )
| ~ gt(loopcounter,n1) )
& ! [D] :
( a_select2(s_center7_init,D) = init
| ~ leq(D,minus(plus(n1,n2),n1))
| ~ leq(n0,D) )
& ! [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) ) ),
inference(pre_NNF_transformation,[status(thm)],[f54]) ).
fof(f245,definition,
( sP3_prd
<=> ( ? [H] :
( a_select2(s_center7_init,H) != init
& leq(H,n2)
& leq(n0,H) )
| ? [G] :
( a_select2(s_values7_init,G) != init
& leq(G,n3)
& leq(n0,G) )
| ? [E] :
( ? [F] :
( a_select3(simplex7_init,F,E) != init
& leq(F,n3)
& leq(n0,F) )
& leq(E,n2)
& leq(n0,E) ) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f246,plain,
( ( ( ( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init )
& gt(loopcounter,n1) )
| sP3_prd )
& ( ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init )
| ~ gt(loopcounter,n1) )
& ! [D] :
( a_select2(s_center7_init,D) = init
| ~ leq(D,minus(plus(n1,n2),n1))
| ~ leq(n0,D) )
& ! [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) ) ),
inference(formula_renaming,[status(thm)],[f244,f245]) ).
fof(f247,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)],[f246]) ).
fof(f248,plain,
! [X0] :
( a_select2(s_values7_init,X0) = init
| ~ leq(X0,n3)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f249,plain,
! [X0] :
( a_select2(s_center7_init,X0) = init
| ~ leq(X0,minus(plus(n1,n2),n1))
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f250,plain,
( pvar1400_init = init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f251,plain,
( pvar1401_init = init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f252,plain,
( pvar1402_init = init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f253,plain,
( gt(loopcounter,n1)
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f254,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f321,definition,
( sP5_prd
<=> ( ? [G] :
( a_select2(s_values7_init,G) != init
& leq(G,n3)
& leq(n0,G) )
| ? [E] :
( ? [F] :
( a_select3(simplex7_init,F,E) != init
& leq(F,n3)
& leq(n0,F) )
& leq(E,n2)
& leq(n0,E) ) ) ),
introduced(definition,[new_symbols(definition,[sP5_prd])],[]) ).
fof(f322,plain,
( sP3_prd
<=> ( ? [H] :
( a_select2(s_center7_init,H) != init
& leq(H,n2)
& leq(n0,H) )
| sP5_prd ) ),
inference(formula_renaming,[status(thm)],[f245,f321]) ).
fof(f323,plain,
( ( ( ! [H] :
( a_select2(s_center7_init,H) = init
| ~ leq(H,n2)
| ~ leq(n0,H) )
& ~ sP5_prd )
| sP3_prd )
& ( ? [H] :
( a_select2(s_center7_init,H) != init
& leq(H,n2)
& leq(n0,H) )
| sP5_prd
| ~ sP3_prd ) ),
inference(NNF_transformation,[status(thm)],[f322]) ).
fof(f324,plain,
( ( ( ! [H] :
( a_select2(s_center7_init,H) = init
| ~ leq(H,n2)
| ~ leq(n0,H) )
& ~ sP5_prd )
| sP3_prd )
& ( ( a_select2(s_center7_init,sK27_skl) != init
& leq(sK27_skl,n2)
& leq(n0,sK27_skl) )
| sP5_prd
| ~ sP3_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(H,sK27_skl)],[f323]) ).
fof(f325,plain,
( leq(n0,sK27_skl)
| sP5_prd
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f326,plain,
( leq(sK27_skl,n2)
| sP5_prd
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f327,plain,
( a_select2(s_center7_init,sK27_skl) != init
| sP5_prd
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f338,definition,
! [E] :
( sP6_prd(E)
<=> ( ? [F] :
( a_select3(simplex7_init,F,E) != init
& leq(F,n3)
& leq(n0,F) )
& leq(E,n2)
& leq(n0,E) ) ),
introduced(definition,[new_symbols(definition,[sP6_prd])],[]) ).
fof(f339,plain,
( sP5_prd
<=> ( ? [G] :
( a_select2(s_values7_init,G) != init
& leq(G,n3)
& leq(n0,G) )
| ? [E] : sP6_prd(E) ) ),
inference(formula_renaming,[status(thm)],[f321,f338]) ).
fof(f340,plain,
( ( ( ! [G] :
( a_select2(s_values7_init,G) = init
| ~ leq(G,n3)
| ~ leq(n0,G) )
& ! [E] : ~ sP6_prd(E) )
| sP5_prd )
& ( ? [G] :
( a_select2(s_values7_init,G) != init
& leq(G,n3)
& leq(n0,G) )
| ? [E] : sP6_prd(E)
| ~ sP5_prd ) ),
inference(NNF_transformation,[status(thm)],[f339]) ).
fof(f341,plain,
( ( ( ! [G] :
( a_select2(s_values7_init,G) = init
| ~ leq(G,n3)
| ~ leq(n0,G) )
& ! [E] : ~ sP6_prd(E) )
| sP5_prd )
& ( ( a_select2(s_values7_init,sK29_skl) != init
& leq(sK29_skl,n3)
& leq(n0,sK29_skl) )
| sP6_prd(sK28_skl)
| ~ sP5_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28_skl,sK29_skl]),skolemize(E,sK28_skl),skolemize(G,sK29_skl)],[f340]) ).
fof(f342,plain,
( leq(n0,sK29_skl)
| sP6_prd(sK28_skl)
| ~ sP5_prd ),
inference(cnf_transformation,[status(thm)],[f341]) ).
fof(f343,plain,
( leq(sK29_skl,n3)
| sP6_prd(sK28_skl)
| ~ sP5_prd ),
inference(cnf_transformation,[status(thm)],[f341]) ).
fof(f344,plain,
( a_select2(s_values7_init,sK29_skl) != init
| sP6_prd(sK28_skl)
| ~ sP5_prd ),
inference(cnf_transformation,[status(thm)],[f341]) ).
fof(f347,plain,
! [E] :
( ( ! [F] :
( a_select3(simplex7_init,F,E) = init
| ~ leq(F,n3)
| ~ leq(n0,F) )
| ~ leq(E,n2)
| ~ leq(n0,E)
| sP6_prd(E) )
& ( ( ? [F] :
( a_select3(simplex7_init,F,E) != init
& leq(F,n3)
& leq(n0,F) )
& leq(E,n2)
& leq(n0,E) )
| ~ sP6_prd(E) ) ),
inference(NNF_transformation,[status(thm)],[f338]) ).
fof(f348,plain,
( ! [E] :
( ! [F] :
( a_select3(simplex7_init,F,E) = init
| ~ leq(F,n3)
| ~ leq(n0,F) )
| ~ leq(E,n2)
| ~ leq(n0,E)
| sP6_prd(E) )
& ! [E] :
( ( ? [F] :
( a_select3(simplex7_init,F,E) != init
& leq(F,n3)
& leq(n0,F) )
& leq(E,n2)
& leq(n0,E) )
| ~ sP6_prd(E) ) ),
inference(miniscoping,[status(thm)],[f347]) ).
fof(f349,plain,
( ! [E] :
( ! [F] :
( a_select3(simplex7_init,F,E) = init
| ~ leq(F,n3)
| ~ leq(n0,F) )
| ~ leq(E,n2)
| ~ leq(n0,E)
| sP6_prd(E) )
& ! [E] :
( ( a_select3(simplex7_init,sK30_skl(E),E) != init
& leq(sK30_skl(E),n3)
& leq(n0,sK30_skl(E))
& leq(E,n2)
& leq(n0,E) )
| ~ sP6_prd(E) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30_skl]),skolemize(F,sK30_skl(E))],[f348]) ).
fof(f350,plain,
! [X0] :
( leq(n0,X0)
| ~ sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f349]) ).
fof(f351,plain,
! [X0] :
( leq(X0,n2)
| ~ sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f349]) ).
fof(f352,plain,
! [X0] :
( leq(n0,sK30_skl(X0))
| ~ sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f349]) ).
fof(f353,plain,
! [X0] :
( leq(sK30_skl(X0),n3)
| ~ sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f349]) ).
fof(f354,plain,
! [X0] :
( a_select3(simplex7_init,sK30_skl(X0),X0) != init
| ~ sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f349]) ).
fof(f356,definition,
( sQ0_spl
<=> gt(loopcounter,n1) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f359,definition,
( sQ1_spl
<=> pvar1400_init = init ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f362,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f250,f356,f359]) ).
fof(f363,definition,
( sQ2_spl
<=> pvar1401_init = init ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f366,plain,
( sQ2_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f251,f356,f363]) ).
fof(f367,definition,
( sQ3_spl
<=> pvar1402_init = init ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f370,plain,
( sQ3_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f252,f356,f367]) ).
fof(f371,definition,
( sQ4_spl
<=> sP3_prd ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f374,plain,
( sQ0_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f253,f371,f356]) ).
fof(f375,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f254,f371,f359,f363,f367]) ).
fof(f376,definition,
( sQ5_spl
<=> sP5_prd ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f379,definition,
( sQ6_spl
<=> leq(n0,sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f381,plain,
( sQ6_spl
| ~ leq(n0,sK27_skl) ),
inference(component_clause,[status(thm)],[f379]) ).
fof(f382,plain,
( sQ6_spl
| sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f325,f371,f376,f379]) ).
fof(f383,definition,
( sQ7_spl
<=> leq(sK27_skl,n2) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f385,plain,
( sQ7_spl
| ~ leq(sK27_skl,n2) ),
inference(component_clause,[status(thm)],[f383]) ).
fof(f386,plain,
( sQ7_spl
| sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f326,f371,f376,f383]) ).
fof(f387,definition,
( sQ8_spl
<=> a_select2(s_center7_init,sK27_skl) = init ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f389,plain,
( sQ8_spl
| a_select2(s_center7_init,sK27_skl) != init ),
inference(component_clause,[status(thm)],[f387]) ).
fof(f390,plain,
( ~ sQ8_spl
| sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f327,f371,f376,f387]) ).
fof(f396,definition,
( sQ10_spl
<=> sP6_prd(sK28_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f397,plain,
( ~ sQ10_spl
| sP6_prd(sK28_skl) ),
inference(component_clause,[status(thm)],[f396]) ).
fof(f399,definition,
( sQ11_spl
<=> leq(n0,sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f402,plain,
( sQ11_spl
| sQ10_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f342,f376,f396,f399]) ).
fof(f403,definition,
( sQ12_spl
<=> leq(sK29_skl,n3) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f406,plain,
( sQ12_spl
| sQ10_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f343,f376,f396,f403]) ).
fof(f407,definition,
( sQ13_spl
<=> a_select2(s_values7_init,sK29_skl) = init ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f409,plain,
( sQ13_spl
| a_select2(s_values7_init,sK29_skl) != init ),
inference(component_clause,[status(thm)],[f407]) ).
fof(f410,plain,
( ~ sQ13_spl
| sQ10_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f344,f376,f396,f407]) ).
fof(f431,plain,
! [X0] :
( a_select2(s_center7_init,X0) = init
| ~ leq(X0,pred(plus(n1,n2)))
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f210,f249]) ).
fof(f432,plain,
! [X0] :
( a_select2(s_center7_init,X0) = init
| ~ leq(X0,pred(succ(n2)))
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f201,f431]) ).
fof(f433,plain,
! [X0] :
( a_select2(s_center7_init,X0) = init
| ~ leq(X0,n2)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f211,f432]) ).
fof(f628,definition,
( sQ43_spl
<=> leq(n0,n0) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f630,plain,
( sQ43_spl
| ~ leq(n0,n0) ),
inference(component_clause,[status(thm)],[f628]) ).
fof(f643,plain,
( sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f630,f92]) ).
fof(f644,plain,
sQ43_spl,
inference(contradiction_clause,[status(thm)],[f643]) ).
fof(f714,plain,
( sQ13_spl
| ~ leq(sK29_skl,n3)
| ~ leq(n0,sK29_skl) ),
inference(resolution,[status(thm)],[f409,f248]) ).
fof(f715,plain,
( sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f714,f399,f403,f407]) ).
fof(f716,plain,
( sQ8_spl
| ~ leq(sK27_skl,n2)
| ~ leq(n0,sK27_skl) ),
inference(resolution,[status(thm)],[f389,f433]) ).
fof(f717,plain,
( sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f716,f379,f383,f387]) ).
fof(f730,plain,
( ~ sQ10_spl
| a_select3(simplex7_init,sK30_skl(sK28_skl),sK28_skl) != init ),
inference(resolution,[status(thm)],[f397,f354]) ).
fof(f743,plain,
! [X0] :
( sQ7_spl
| ~ leq(X0,n2)
| ~ leq(sK27_skl,X0) ),
inference(resolution,[status(thm)],[f385,f95]) ).
fof(f850,plain,
( sQ6_spl
| ~ gt(succ(sK27_skl),n0) ),
inference(resolution,[status(thm)],[f381,f118]) ).
fof(f861,plain,
( ~ sQ10_spl
| ~ leq(sK30_skl(sK28_skl),n3)
| ~ leq(n0,sK30_skl(sK28_skl))
| ~ leq(sK28_skl,n2)
| ~ leq(n0,sK28_skl) ),
inference(resolution,[status(thm)],[f730,f247]) ).
fof(f862,definition,
( sQ64_spl
<=> leq(n0,sK28_skl) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f864,plain,
( sQ64_spl
| ~ leq(n0,sK28_skl) ),
inference(component_clause,[status(thm)],[f862]) ).
fof(f865,definition,
( sQ65_spl
<=> leq(sK28_skl,n2) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f867,plain,
( sQ65_spl
| ~ leq(sK28_skl,n2) ),
inference(component_clause,[status(thm)],[f865]) ).
fof(f868,definition,
( sQ66_spl
<=> leq(n0,sK30_skl(sK28_skl)) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f870,plain,
( sQ66_spl
| ~ leq(n0,sK30_skl(sK28_skl)) ),
inference(component_clause,[status(thm)],[f868]) ).
fof(f871,definition,
( sQ67_spl
<=> leq(sK30_skl(sK28_skl),n3) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f873,plain,
( sQ67_spl
| ~ leq(sK30_skl(sK28_skl),n3) ),
inference(component_clause,[status(thm)],[f871]) ).
fof(f874,plain,
( ~ sQ10_spl
| ~ sQ67_spl
| ~ sQ66_spl
| ~ sQ65_spl
| ~ sQ64_spl ),
inference(split_clause,[status(thm)],[f861,f862,f865,f868,f871,f396]) ).
fof(f938,plain,
( sQ6_spl
| n0 = succ(sK27_skl)
| ~ leq(n0,succ(sK27_skl)) ),
inference(resolution,[status(thm)],[f850,f107]) ).
fof(f939,plain,
( sQ6_spl
| succ(sK27_skl) = n0
| gt(n0,succ(sK27_skl)) ),
inference(resolution,[status(thm)],[f850,f87]) ).
fof(f943,definition,
( sQ73_spl
<=> leq(n0,succ(sK27_skl)) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f945,plain,
( sQ73_spl
| ~ leq(n0,succ(sK27_skl)) ),
inference(component_clause,[status(thm)],[f943]) ).
fof(f946,definition,
( sQ74_spl
<=> n0 = succ(sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f947,plain,
( ~ sQ74_spl
| n0 = succ(sK27_skl) ),
inference(component_clause,[status(thm)],[f946]) ).
fof(f949,plain,
( sQ6_spl
| sQ74_spl
| ~ sQ73_spl ),
inference(split_clause,[status(thm)],[f938,f943,f946,f379]) ).
fof(f950,definition,
( sQ75_spl
<=> gt(n0,succ(sK27_skl)) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f951,plain,
( ~ sQ75_spl
| gt(n0,succ(sK27_skl)) ),
inference(component_clause,[status(thm)],[f950]) ).
fof(f953,plain,
( sQ6_spl
| sQ74_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f939,f950,f946,f379]) ).
fof(f954,plain,
( ~ sQ75_spl
| ~ sQ74_spl
| gt(n0,n0) ),
inference(forward_demodulation,[status(thm)],[f947,f951]) ).
fof(f955,plain,
( ~ sQ75_spl
| ~ sQ74_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f954,f91]) ).
fof(f956,plain,
( ~ sQ75_spl
| ~ sQ74_spl ),
inference(contradiction_clause,[status(thm)],[f955]) ).
fof(f998,plain,
( sQ65_spl
| ~ sP6_prd(sK28_skl) ),
inference(resolution,[status(thm)],[f867,f351]) ).
fof(f1003,plain,
( sQ65_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f998,f396,f865]) ).
fof(f1007,plain,
( sQ73_spl
| ~ sQ74_spl
| ~ leq(n0,n0) ),
inference(backward_demodulation,[status(thm)],[f947,f945]) ).
fof(f1009,plain,
( sQ73_spl
| ~ sQ74_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f1007,f628,f946,f943]) ).
fof(f1047,plain,
( sQ64_spl
| ~ sP6_prd(sK28_skl) ),
inference(resolution,[status(thm)],[f864,f350]) ).
fof(f1052,plain,
( sQ64_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1047,f396,f862]) ).
fof(f1124,plain,
( sQ7_spl
| ~ sP6_prd(sK27_skl)
| ~ leq(n2,n2) ),
inference(resolution,[status(thm)],[f743,f351]) ).
fof(f1151,definition,
( sQ82_spl
<=> leq(n2,n2) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1153,plain,
( sQ82_spl
| ~ leq(n2,n2) ),
inference(component_clause,[status(thm)],[f1151]) ).
fof(f1154,definition,
( sQ83_spl
<=> sP6_prd(sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1157,plain,
( sQ7_spl
| ~ sQ83_spl
| ~ sQ82_spl ),
inference(split_clause,[status(thm)],[f1124,f1151,f1154,f383]) ).
fof(f1169,plain,
( sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1153,f92]) ).
fof(f1170,plain,
sQ82_spl,
inference(contradiction_clause,[status(thm)],[f1169]) ).
fof(f1192,plain,
( sQ67_spl
| ~ sP6_prd(sK28_skl) ),
inference(resolution,[status(thm)],[f873,f353]) ).
fof(f1197,plain,
( sQ67_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1192,f396,f871]) ).
fof(f1198,plain,
( sQ66_spl
| ~ sP6_prd(sK28_skl) ),
inference(resolution,[status(thm)],[f870,f352]) ).
fof(f1204,plain,
( sQ66_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1198,f396,f868]) ).
fof(f1205,plain,
$false,
inference(sat_refutation,[status(thm)],[f362,f366,f370,f374,f375,f382,f386,f390,f402,f406,f410,f644,f715,f717,f874,f949,f953,f956,f1003,f1009,f1052,f1157,f1170,f1197,f1204]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV042+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n003.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 08:30:31 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.37 % Drodi V4.1.1
% 0.83/0.53 % Refutation found
% 0.83/0.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.83/0.53 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.83/0.54 % Elapsed time: 0.184232 seconds
% 0.83/0.54 % CPU time: 1.234858 seconds
% 0.83/0.54 % Total memory used: 124.661 MB
% 0.83/0.54 % Net memory used: 122.516 MB
%------------------------------------------------------------------------------