%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV039+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 : n011.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 14.35s 2.52s
% Output : CNFRefutation 16.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 15
% Syntax : Number of formulae : 165 ( 41 unt; 4 def)
% Number of atoms : 958 ( 278 equ)
% Maximal formula atoms : 51 ( 5 avg)
% Number of connectives : 1309 ( 516 ~; 580 |; 182 &)
% ( 6 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 25 con; 0-3 aty)
% Number of variables : 163 ( 151 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X] : ~ gt(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y,Z] :
( ( leq(Y,Z)
& leq(X,Y) )
=> leq(X,Z) ),
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(f13,axiom,
! [X,Y] :
( leq(X,Y)
<=> gt(succ(Y),X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [Body] : sum(n0,tptp_minus_1,Body) = n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [Body] : tptp_float_0_0 = sum(n0,tptp_minus_1,Body),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
succ(tptp_minus_1) = n0,
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(f41,axiom,
! [X] : succ(pred(X)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,conjecture,
( ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [D] :
( ( leq(D,n2)
& 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 ) )
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init )
=> ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [I] :
( ( leq(I,minus(n0,n1))
& leq(n0,I) )
=> a_select2(s_try7_init,I) = 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 ) )
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
~ ( ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [D] :
( ( leq(D,n2)
& 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 ) )
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init )
=> ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [I] :
( ( leq(I,minus(n0,n1))
& leq(n0,I) )
=> a_select2(s_try7_init,I) = 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 ) )
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f91,plain,
! [X0] : ~ gt(X0,X0),
inference(cnf_transformation,[status(thm)],[f3]) ).
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(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(f110,plain,
! [X0,X1] :
( gt(X1,X0)
| ~ leq(X0,pred(X1)) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f111,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| leq(X0,pred(X1)) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
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(f117,plain,
! [X0,X1] :
( gt(succ(X1),X0)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f197,plain,
! [X0] : sum(n0,tptp_minus_1,X0) = n0,
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f198,plain,
! [X0] : tptp_float_0_0 = sum(n0,tptp_minus_1,X0),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f199,plain,
succ(tptp_minus_1) = n0,
inference(cnf_transformation,[status(thm)],[f28]) ).
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(f212,plain,
! [X0] : succ(pred(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f244,plain,
( ( ( ( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init )
& gt(loopcounter,n1) )
| ? [I] :
( a_select2(s_try7_init,I) != init
& leq(I,minus(n0,n1))
& leq(n0,I) )
| ? [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) )
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != init
| s_sworst7_init != init
| s_best7_init != init )
& ( ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init )
| ~ gt(loopcounter,n1) )
& ! [D] :
( a_select2(s_center7_init,D) = init
| ~ leq(D,n2)
| ~ 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) )
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init ),
inference(pre_NNF_transformation,[status(thm)],[f54]) ).
fof(f245,definition,
! [E] :
( sP3_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,[sP3_prd])],[]) ).
fof(f246,definition,
! [G] :
( sP4_prd(G)
<=> ( a_select2(s_values7_init,G) != init
& leq(G,n3)
& leq(n0,G) ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f247,definition,
! [H] :
( sP5_prd(H)
<=> ( a_select2(s_center7_init,H) != init
& leq(H,n2)
& leq(n0,H) ) ),
introduced(definition,[new_symbols(definition,[sP5_prd])],[]) ).
fof(f248,definition,
! [I] :
( sP6_prd(I)
<=> ( a_select2(s_try7_init,I) != init
& leq(I,minus(n0,n1))
& leq(n0,I) ) ),
introduced(definition,[new_symbols(definition,[sP6_prd])],[]) ).
fof(f249,plain,
( ( ( ( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init )
& gt(loopcounter,n1) )
| ? [I] : sP6_prd(I)
| ? [H] : sP5_prd(H)
| ? [G] : sP4_prd(G)
| ? [E] : sP3_prd(E)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != init
| s_sworst7_init != init
| s_best7_init != init )
& ( ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init )
| ~ gt(loopcounter,n1) )
& ! [D] :
( a_select2(s_center7_init,D) = init
| ~ leq(D,n2)
| ~ 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) )
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init ),
inference(formula_renaming,[status(thm)],[f244,f248,f247,f246,f245]) ).
fof(f250,plain,
( ( ( ( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init )
& gt(loopcounter,n1) )
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != init
| s_sworst7_init != init
| s_best7_init != init )
& ( ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init )
| ~ gt(loopcounter,n1) )
& ! [D] :
( a_select2(s_center7_init,D) = init
| ~ leq(D,n2)
| ~ 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) )
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl,sK25_skl,sK26_skl]),skolemize(E,sK23_skl),skolemize(G,sK24_skl),skolemize(H,sK25_skl),skolemize(I,sK26_skl)],[f249]) ).
fof(f251,plain,
s_best7_init = init,
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f252,plain,
s_sworst7_init = init,
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f253,plain,
s_worst7_init = init,
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f254,plain,
leq(n0,s_best7),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f255,plain,
leq(n0,s_sworst7),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f256,plain,
leq(n0,s_worst7),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f257,plain,
leq(s_best7,n3),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f258,plain,
leq(s_sworst7,n3),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f259,plain,
leq(s_worst7,n3),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f260,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)],[f250]) ).
fof(f261,plain,
! [X0] :
( a_select2(s_values7_init,X0) = init
| ~ leq(X0,n3)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f262,plain,
! [X0] :
( a_select2(s_center7_init,X0) = init
| ~ leq(X0,n2)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f263,plain,
( pvar1400_init = init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f264,plain,
( pvar1401_init = init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f265,plain,
( pvar1402_init = init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f266,plain,
( gt(loopcounter,n1)
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != init
| s_sworst7_init != init
| s_best7_init != init ),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f267,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != init
| s_sworst7_init != init
| s_best7_init != init ),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f334,plain,
! [E] :
( ( ! [F] :
( a_select3(simplex7_init,F,E) = init
| ~ leq(F,n3)
| ~ leq(n0,F) )
| ~ leq(E,n2)
| ~ leq(n0,E)
| sP3_prd(E) )
& ( ( ? [F] :
( a_select3(simplex7_init,F,E) != init
& leq(F,n3)
& leq(n0,F) )
& leq(E,n2)
& leq(n0,E) )
| ~ sP3_prd(E) ) ),
inference(NNF_transformation,[status(thm)],[f245]) ).
fof(f335,plain,
( ! [E] :
( ! [F] :
( a_select3(simplex7_init,F,E) = init
| ~ leq(F,n3)
| ~ leq(n0,F) )
| ~ leq(E,n2)
| ~ leq(n0,E)
| sP3_prd(E) )
& ! [E] :
( ( ? [F] :
( a_select3(simplex7_init,F,E) != init
& leq(F,n3)
& leq(n0,F) )
& leq(E,n2)
& leq(n0,E) )
| ~ sP3_prd(E) ) ),
inference(miniscoping,[status(thm)],[f334]) ).
fof(f336,plain,
( ! [E] :
( ! [F] :
( a_select3(simplex7_init,F,E) = init
| ~ leq(F,n3)
| ~ leq(n0,F) )
| ~ leq(E,n2)
| ~ leq(n0,E)
| sP3_prd(E) )
& ! [E] :
( ( a_select3(simplex7_init,sK31_skl(E),E) != init
& leq(sK31_skl(E),n3)
& leq(n0,sK31_skl(E))
& leq(E,n2)
& leq(n0,E) )
| ~ sP3_prd(E) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31_skl]),skolemize(F,sK31_skl(E))],[f335]) ).
fof(f337,plain,
! [X0] :
( leq(n0,X0)
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f336]) ).
fof(f338,plain,
! [X0] :
( leq(X0,n2)
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f336]) ).
fof(f339,plain,
! [X0] :
( leq(n0,sK31_skl(X0))
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f336]) ).
fof(f340,plain,
! [X0] :
( leq(sK31_skl(X0),n3)
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f336]) ).
fof(f341,plain,
! [X0] :
( a_select3(simplex7_init,sK31_skl(X0),X0) != init
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f336]) ).
fof(f343,plain,
! [G] :
( ( a_select2(s_values7_init,G) = init
| ~ leq(G,n3)
| ~ leq(n0,G)
| sP4_prd(G) )
& ( ( a_select2(s_values7_init,G) != init
& leq(G,n3)
& leq(n0,G) )
| ~ sP4_prd(G) ) ),
inference(NNF_transformation,[status(thm)],[f246]) ).
fof(f344,plain,
( ! [G] :
( a_select2(s_values7_init,G) = init
| ~ leq(G,n3)
| ~ leq(n0,G)
| sP4_prd(G) )
& ! [G] :
( ( a_select2(s_values7_init,G) != init
& leq(G,n3)
& leq(n0,G) )
| ~ sP4_prd(G) ) ),
inference(miniscoping,[status(thm)],[f343]) ).
fof(f345,plain,
! [X0] :
( leq(n0,X0)
| ~ sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f344]) ).
fof(f346,plain,
! [X0] :
( leq(X0,n3)
| ~ sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f344]) ).
fof(f347,plain,
! [X0] :
( a_select2(s_values7_init,X0) != init
| ~ sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f344]) ).
fof(f349,plain,
! [H] :
( ( a_select2(s_center7_init,H) = init
| ~ leq(H,n2)
| ~ leq(n0,H)
| sP5_prd(H) )
& ( ( a_select2(s_center7_init,H) != init
& leq(H,n2)
& leq(n0,H) )
| ~ sP5_prd(H) ) ),
inference(NNF_transformation,[status(thm)],[f247]) ).
fof(f350,plain,
( ! [H] :
( a_select2(s_center7_init,H) = init
| ~ leq(H,n2)
| ~ leq(n0,H)
| sP5_prd(H) )
& ! [H] :
( ( a_select2(s_center7_init,H) != init
& leq(H,n2)
& leq(n0,H) )
| ~ sP5_prd(H) ) ),
inference(miniscoping,[status(thm)],[f349]) ).
fof(f351,plain,
! [X0] :
( leq(n0,X0)
| ~ sP5_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f350]) ).
fof(f352,plain,
! [X0] :
( leq(X0,n2)
| ~ sP5_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f350]) ).
fof(f353,plain,
! [X0] :
( a_select2(s_center7_init,X0) != init
| ~ sP5_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f350]) ).
fof(f355,plain,
! [I] :
( ( a_select2(s_try7_init,I) = init
| ~ leq(I,minus(n0,n1))
| ~ leq(n0,I)
| sP6_prd(I) )
& ( ( a_select2(s_try7_init,I) != init
& leq(I,minus(n0,n1))
& leq(n0,I) )
| ~ sP6_prd(I) ) ),
inference(NNF_transformation,[status(thm)],[f248]) ).
fof(f356,plain,
( ! [I] :
( a_select2(s_try7_init,I) = init
| ~ leq(I,minus(n0,n1))
| ~ leq(n0,I)
| sP6_prd(I) )
& ! [I] :
( ( a_select2(s_try7_init,I) != init
& leq(I,minus(n0,n1))
& leq(n0,I) )
| ~ sP6_prd(I) ) ),
inference(miniscoping,[status(thm)],[f355]) ).
fof(f357,plain,
! [X0] :
( leq(n0,X0)
| ~ sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f356]) ).
fof(f358,plain,
! [X0] :
( leq(X0,minus(n0,n1))
| ~ sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f356]) ).
fof(f371,plain,
s_best7_init = s_sworst7_init,
inference(backward_demodulation,[status(thm)],[f252,f251]) ).
fof(f372,plain,
s_sworst7_init = s_worst7_init,
inference(backward_demodulation,[status(thm)],[f253,f252]) ).
fof(f373,plain,
s_best7_init = s_worst7_init,
inference(backward_demodulation,[status(thm)],[f372,f371]) ).
fof(f378,plain,
pred(n0) = tptp_minus_1,
inference(paramodulation,[status(thm)],[f199,f211]) ).
fof(f405,plain,
! [X0,X1] :
( a_select3(simplex7_init,X1,X0) = s_worst7_init
| ~ leq(X1,n3)
| ~ leq(n0,X1)
| ~ leq(X0,n2)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f253,f260]) ).
fof(f494,plain,
! [X0] :
( gt(n0,X0)
| ~ leq(X0,tptp_minus_1) ),
inference(paramodulation,[status(thm)],[f378,f110]) ).
fof(f500,plain,
! [X0] :
( a_select2(s_values7_init,X0) = s_worst7_init
| ~ leq(X0,n3)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f253,f261]) ).
fof(f515,plain,
! [X0] : ~ leq(succ(X0),X0),
inference(resolution,[status(thm)],[f117,f91]) ).
fof(f556,plain,
! [X0,X1,X2] :
( leq(X2,pred(X0))
| ~ leq(X2,X1)
| ~ gt(X0,X1) ),
inference(resolution,[status(thm)],[f111,f95]) ).
fof(f579,plain,
! [X0] :
( a_select2(s_center7_init,X0) = s_worst7_init
| ~ leq(X0,n2)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f253,f262]) ).
fof(f649,plain,
( pvar1400_init = s_worst7_init
| ~ gt(loopcounter,n1) ),
inference(forward_demodulation,[status(thm)],[f253,f263]) ).
fof(f677,plain,
( pvar1401_init = s_worst7_init
| ~ gt(loopcounter,n1) ),
inference(forward_demodulation,[status(thm)],[f253,f264]) ).
fof(f700,plain,
( pvar1402_init = s_worst7_init
| ~ gt(loopcounter,n1) ),
inference(forward_demodulation,[status(thm)],[f253,f265]) ).
fof(f712,plain,
( gt(loopcounter,n1)
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != init
| s_sworst7_init != init
| s_worst7_init != init ),
inference(forward_demodulation,[status(thm)],[f373,f266]) ).
fof(f713,plain,
( gt(loopcounter,n1)
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != init
| s_sworst7_init != init
| s_worst7_init != s_worst7_init ),
inference(forward_demodulation,[status(thm)],[f253,f712]) ).
fof(f714,plain,
( gt(loopcounter,n1)
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != init
| s_worst7_init != init
| s_worst7_init != s_worst7_init ),
inference(forward_demodulation,[status(thm)],[f372,f713]) ).
fof(f715,plain,
( gt(loopcounter,n1)
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != init
| s_worst7_init != s_worst7_init
| s_worst7_init != s_worst7_init ),
inference(forward_demodulation,[status(thm)],[f253,f714]) ).
fof(f716,plain,
( gt(loopcounter,n1)
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != s_worst7_init
| s_worst7_init != s_worst7_init
| s_worst7_init != s_worst7_init ),
inference(forward_demodulation,[status(thm)],[f253,f715]) ).
fof(f717,plain,
( gt(loopcounter,n1)
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != s_worst7_init ),
inference(duplicate_literals_removal,[status(thm)],[f716]) ).
fof(f718,plain,
( gt(loopcounter,n1)
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7) ),
inference(trivial_equality_resolution,[status(thm)],[f717]) ).
fof(f719,plain,
( gt(loopcounter,n1)
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7) ),
inference(forward_subsumption_resolution,[status(thm)],[f718,f254]) ).
fof(f730,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != init
| s_sworst7_init != init
| s_worst7_init != init ),
inference(forward_demodulation,[status(thm)],[f373,f267]) ).
fof(f731,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != init
| s_sworst7_init != init
| s_worst7_init != s_worst7_init ),
inference(forward_demodulation,[status(thm)],[f253,f730]) ).
fof(f732,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != init
| s_worst7_init != init
| s_worst7_init != s_worst7_init ),
inference(forward_demodulation,[status(thm)],[f372,f731]) ).
fof(f733,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != init
| s_worst7_init != s_worst7_init
| s_worst7_init != s_worst7_init ),
inference(forward_demodulation,[status(thm)],[f253,f732]) ).
fof(f734,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != s_worst7_init
| s_worst7_init != s_worst7_init
| s_worst7_init != s_worst7_init ),
inference(forward_demodulation,[status(thm)],[f253,f733]) ).
fof(f735,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != s_worst7_init
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != s_worst7_init
| s_worst7_init != s_worst7_init
| s_worst7_init != s_worst7_init ),
inference(forward_demodulation,[status(thm)],[f253,f734]) ).
fof(f736,plain,
( pvar1402_init != init
| pvar1401_init != s_worst7_init
| pvar1400_init != s_worst7_init
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != s_worst7_init
| s_worst7_init != s_worst7_init
| s_worst7_init != s_worst7_init ),
inference(forward_demodulation,[status(thm)],[f253,f735]) ).
fof(f737,plain,
( pvar1402_init != s_worst7_init
| pvar1401_init != s_worst7_init
| pvar1400_init != s_worst7_init
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != s_worst7_init
| s_worst7_init != s_worst7_init
| s_worst7_init != s_worst7_init ),
inference(forward_demodulation,[status(thm)],[f253,f736]) ).
fof(f738,plain,
( pvar1402_init != s_worst7_init
| pvar1401_init != s_worst7_init
| pvar1400_init != s_worst7_init
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != s_worst7_init ),
inference(duplicate_literals_removal,[status(thm)],[f737]) ).
fof(f739,plain,
( pvar1402_init != s_worst7_init
| pvar1401_init != s_worst7_init
| pvar1400_init != s_worst7_init
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7) ),
inference(trivial_equality_resolution,[status(thm)],[f738]) ).
fof(f740,plain,
( pvar1402_init != s_worst7_init
| pvar1401_init != s_worst7_init
| pvar1400_init != s_worst7_init
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP4_prd(sK24_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7) ),
inference(forward_subsumption_resolution,[status(thm)],[f739,f254]) ).
fof(f923,plain,
! [X0] :
( a_select3(simplex7_init,sK31_skl(X0),X0) != s_worst7_init
| ~ sP3_prd(X0) ),
inference(forward_demodulation,[status(thm)],[f253,f341]) ).
fof(f924,plain,
! [X0] :
( ~ leq(sK31_skl(X0),n3)
| ~ leq(n0,sK31_skl(X0))
| ~ leq(X0,n2)
| ~ leq(n0,X0)
| ~ sP3_prd(X0) ),
inference(resolution,[status(thm)],[f923,f405]) ).
fof(f925,plain,
! [X0] :
( ~ leq(sK31_skl(X0),n3)
| ~ leq(n0,sK31_skl(X0))
| ~ leq(X0,n2)
| ~ sP3_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f924,f337]) ).
fof(f1164,plain,
! [X0] :
( a_select2(s_values7_init,X0) != s_worst7_init
| ~ sP4_prd(X0) ),
inference(forward_demodulation,[status(thm)],[f253,f347]) ).
fof(f1165,plain,
! [X0] :
( ~ leq(X0,n3)
| ~ leq(n0,X0)
| ~ sP4_prd(X0) ),
inference(resolution,[status(thm)],[f1164,f500]) ).
fof(f1166,plain,
! [X0] :
( ~ leq(X0,n3)
| ~ sP4_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1165,f345]) ).
fof(f1167,plain,
( pvar1402_init != s_worst7_init
| pvar1401_init != s_worst7_init
| pvar1400_init != s_worst7_init
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7) ),
inference(backward_subsumption_resolution,[status(thm)],[f740,f1169]) ).
fof(f1168,plain,
( gt(loopcounter,n1)
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7) ),
inference(backward_subsumption_resolution,[status(thm)],[f719,f1169]) ).
fof(f1169,plain,
! [X0] : ~ sP4_prd(X0),
inference(forward_subsumption_resolution,[status(thm)],[f1166,f346]) ).
fof(f1170,plain,
( pvar1402_init != s_worst7_init
| pvar1401_init != s_worst7_init
| pvar1400_init != s_worst7_init
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7) ),
inference(forward_subsumption_resolution,[status(thm)],[f1167,f255]) ).
fof(f1171,plain,
( gt(loopcounter,n1)
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7) ),
inference(forward_subsumption_resolution,[status(thm)],[f1168,f255]) ).
fof(f1172,plain,
! [X0] :
( a_select2(s_center7_init,X0) != s_worst7_init
| ~ sP5_prd(X0) ),
inference(forward_demodulation,[status(thm)],[f253,f353]) ).
fof(f1173,plain,
! [X0] :
( ~ leq(X0,n2)
| ~ leq(n0,X0)
| ~ sP5_prd(X0) ),
inference(resolution,[status(thm)],[f1172,f579]) ).
fof(f1174,plain,
! [X0] :
( ~ leq(X0,n2)
| ~ sP5_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1173,f351]) ).
fof(f1175,plain,
! [X0] : ~ sP5_prd(X0),
inference(forward_subsumption_resolution,[status(thm)],[f1174,f352]) ).
fof(f1318,plain,
! [X0] :
( leq(X0,pred(n0))
| ~ sP6_prd(X0) ),
inference(forward_demodulation,[status(thm)],[f210,f358]) ).
fof(f1319,plain,
! [X0] :
( leq(X0,tptp_minus_1)
| ~ sP6_prd(X0) ),
inference(forward_demodulation,[status(thm)],[f378,f1318]) ).
fof(f1383,plain,
( pvar1402_init != s_worst7_init
| pvar1401_init != s_worst7_init
| pvar1400_init != s_worst7_init
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3) ),
inference(forward_subsumption_resolution,[status(thm)],[f1170,f256]) ).
fof(f1401,plain,
( gt(loopcounter,n1)
| sP6_prd(sK26_skl)
| sP5_prd(sK25_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3) ),
inference(forward_subsumption_resolution,[status(thm)],[f1171,f256]) ).
fof(f1440,plain,
tptp_float_0_0 = n0,
inference(backward_demodulation,[status(thm)],[f198,f197]) ).
fof(f1470,plain,
! [X0] :
( leq(tptp_float_0_0,sK31_skl(X0))
| ~ sP3_prd(X0) ),
inference(backward_demodulation,[status(thm)],[f1440,f339]) ).
fof(f1486,plain,
! [X0] :
( leq(tptp_float_0_0,X0)
| ~ sP6_prd(X0) ),
inference(backward_demodulation,[status(thm)],[f1440,f357]) ).
fof(f3223,plain,
! [X0] :
( gt(tptp_float_0_0,X0)
| ~ leq(X0,tptp_minus_1) ),
inference(forward_demodulation,[status(thm)],[f1440,f494]) ).
fof(f3229,plain,
! [X0] :
( ~ sP6_prd(X0)
| gt(tptp_float_0_0,X0) ),
inference(resolution,[status(thm)],[f3223,f1319]) ).
fof(f3964,plain,
! [X0,X1] :
( ~ leq(succ(pred(X0)),X1)
| ~ gt(X0,X1) ),
inference(resolution,[status(thm)],[f556,f515]) ).
fof(f3978,plain,
! [X0,X1] :
( ~ leq(X0,X1)
| ~ gt(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f212,f3964]) ).
fof(f3988,plain,
! [X0] :
( ~ sP6_prd(X0)
| ~ leq(tptp_float_0_0,X0) ),
inference(resolution,[status(thm)],[f3978,f3229]) ).
fof(f4043,plain,
! [X0] : ~ sP6_prd(X0),
inference(forward_subsumption_resolution,[status(thm)],[f3988,f1486]) ).
fof(f4045,plain,
( gt(loopcounter,n1)
| sP5_prd(sK25_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3) ),
inference(backward_subsumption_resolution,[status(thm)],[f1401,f4043]) ).
fof(f4046,plain,
( pvar1402_init != s_worst7_init
| pvar1401_init != s_worst7_init
| pvar1400_init != s_worst7_init
| sP5_prd(sK25_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3) ),
inference(backward_subsumption_resolution,[status(thm)],[f1383,f4043]) ).
fof(f4048,plain,
( gt(loopcounter,n1)
| sP5_prd(sK25_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3) ),
inference(forward_subsumption_resolution,[status(thm)],[f4045,f257]) ).
fof(f4049,plain,
( pvar1402_init != s_worst7_init
| pvar1401_init != s_worst7_init
| pvar1400_init != s_worst7_init
| sP5_prd(sK25_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3) ),
inference(forward_subsumption_resolution,[status(thm)],[f4046,f257]) ).
fof(f4072,plain,
( gt(loopcounter,n1)
| sP5_prd(sK25_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3) ),
inference(forward_subsumption_resolution,[status(thm)],[f4048,f258]) ).
fof(f4082,plain,
( pvar1402_init != s_worst7_init
| pvar1401_init != s_worst7_init
| pvar1400_init != s_worst7_init
| sP5_prd(sK25_skl)
| sP3_prd(sK23_skl)
| ~ leq(s_worst7,n3) ),
inference(forward_subsumption_resolution,[status(thm)],[f4049,f258]) ).
fof(f8993,plain,
! [X0] :
( ~ leq(sK31_skl(X0),n3)
| ~ leq(tptp_float_0_0,sK31_skl(X0))
| ~ leq(X0,n2)
| ~ sP3_prd(X0) ),
inference(forward_demodulation,[status(thm)],[f1440,f925]) ).
fof(f8994,plain,
! [X0] :
( ~ leq(sK31_skl(X0),n3)
| ~ leq(tptp_float_0_0,sK31_skl(X0))
| ~ sP3_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f8993,f338]) ).
fof(f8995,plain,
! [X0] :
( ~ sP3_prd(X0)
| ~ leq(tptp_float_0_0,sK31_skl(X0))
| ~ sP3_prd(X0) ),
inference(resolution,[status(thm)],[f8994,f340]) ).
fof(f8998,plain,
! [X0] :
( ~ leq(tptp_float_0_0,sK31_skl(X0))
| ~ sP3_prd(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f8995]) ).
fof(f8999,plain,
! [X0] : ~ sP3_prd(X0),
inference(forward_subsumption_resolution,[status(thm)],[f8998,f1470]) ).
fof(f9006,plain,
( pvar1402_init != s_worst7_init
| pvar1401_init != s_worst7_init
| pvar1400_init != s_worst7_init
| sP5_prd(sK25_skl)
| ~ leq(s_worst7,n3) ),
inference(backward_subsumption_resolution,[status(thm)],[f4082,f8999]) ).
fof(f9007,plain,
( gt(loopcounter,n1)
| sP5_prd(sK25_skl)
| ~ leq(s_worst7,n3) ),
inference(backward_subsumption_resolution,[status(thm)],[f4072,f8999]) ).
fof(f9008,plain,
( pvar1402_init != s_worst7_init
| pvar1401_init != s_worst7_init
| pvar1400_init != s_worst7_init
| sP5_prd(sK25_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f9006,f259]) ).
fof(f9009,plain,
( gt(loopcounter,n1)
| sP5_prd(sK25_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f9007,f259]) ).
fof(f9171,plain,
( pvar1402_init != s_worst7_init
| pvar1401_init != s_worst7_init
| pvar1400_init != s_worst7_init ),
inference(forward_subsumption_resolution,[status(thm)],[f9008,f1175]) ).
fof(f9172,plain,
pvar1402_init = s_worst7_init,
inference(backward_subsumption_resolution,[status(thm)],[f700,f9175]) ).
fof(f9173,plain,
pvar1401_init = s_worst7_init,
inference(backward_subsumption_resolution,[status(thm)],[f677,f9175]) ).
fof(f9174,plain,
pvar1400_init = s_worst7_init,
inference(backward_subsumption_resolution,[status(thm)],[f649,f9175]) ).
fof(f9175,plain,
gt(loopcounter,n1),
inference(forward_subsumption_resolution,[status(thm)],[f9009,f1175]) ).
fof(f9183,plain,
( pvar1402_init != pvar1402_init
| pvar1401_init != s_worst7_init
| pvar1400_init != s_worst7_init ),
inference(backward_demodulation,[status(thm)],[f9172,f9171]) ).
fof(f9194,plain,
( pvar1402_init != pvar1402_init
| pvar1401_init != s_worst7_init
| pvar1400_init != pvar1402_init ),
inference(forward_demodulation,[status(thm)],[f9172,f9183]) ).
fof(f9195,plain,
( pvar1402_init != pvar1402_init
| pvar1401_init != pvar1402_init
| pvar1400_init != pvar1402_init ),
inference(forward_demodulation,[status(thm)],[f9172,f9194]) ).
fof(f9196,plain,
( pvar1401_init != pvar1402_init
| pvar1400_init != pvar1402_init ),
inference(trivial_equality_resolution,[status(thm)],[f9195]) ).
fof(f9197,plain,
pvar1401_init = pvar1402_init,
inference(forward_demodulation,[status(thm)],[f9172,f9173]) ).
fof(f9198,plain,
pvar1400_init = pvar1402_init,
inference(forward_demodulation,[status(thm)],[f9172,f9174]) ).
fof(f9199,plain,
( pvar1401_init != pvar1402_init
| pvar1402_init != pvar1402_init ),
inference(forward_demodulation,[status(thm)],[f9198,f9196]) ).
fof(f9200,plain,
( pvar1402_init != pvar1402_init
| pvar1402_init != pvar1402_init ),
inference(forward_demodulation,[status(thm)],[f9197,f9199]) ).
fof(f9201,plain,
pvar1402_init != pvar1402_init,
inference(duplicate_literals_removal,[status(thm)],[f9200]) ).
fof(f9202,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f9201]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV039+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n011.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 08:28:25 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 14.35/2.52 % Refutation found
% 14.35/2.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 14.35/2.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 16.68/2.56 % Elapsed time: 2.192978 seconds
% 16.68/2.56 % CPU time: 16.974346 seconds
% 16.68/2.56 % Total memory used: 189.076 MB
% 16.68/2.56 % Net memory used: 172.907 MB
%------------------------------------------------------------------------------