%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : MGT068+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:25:32 PM UTC 2026
% Result : Theorem 5.50s 1.30s
% Output : CNFRefutation 5.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 52
% Syntax : Number of formulae : 216 ( 50 unt; 25 def)
% Number of atoms : 522 ( 60 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 535 ( 229 ~; 215 |; 52 &)
% ( 32 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 36 ( 34 usr; 26 prp; 0-8 aty)
% Number of functors : 15 ( 15 usr; 12 con; 0-4 aty)
% Number of variables : 234 ( 227 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : ~ less(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y,Z] :
( ( less(Y,Z)
& less(X,Y) )
=> less(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y] :
( less(Y,X)
| X = Y
| less(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y] :
( leq(X,Y)
<=> ( X = Y
| less(X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y,Z] :
( ( less(Y,Z)
& leq(X,Y) )
=> less(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,Y] :
( less(X,Y)
=> ? [Z] :
( less(Z,Y)
& less(X,Z) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X,A,B] :
( in_closed(X,A,B)
<=> ( leq(X,B)
& leq(A,X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [I1lo,I1hi,I2lo,I2hi] :
( axis_conflict(I1lo,I1hi,I2lo,I2hi)
<=> ~ ? [X] :
( in_closed(X,I2lo,I2hi)
& in_closed(X,I1lo,I1hi) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
is_verdict(conflict),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
is_verdict(compatible),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
is_verdict(unknown),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
conflict != compatible,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
conflict != unknown,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
compatible != unknown,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [V1,V2] :
( ( ( V2 = conflict
| V1 = conflict )
& is_verdict(V2)
& is_verdict(V1) )
=> box_verdict(V1,V2) = conflict ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [V1,V2] :
( ( V2 = compatible
& V1 = compatible
& is_verdict(V2)
& is_verdict(V1) )
=> box_verdict(V1,V2) = compatible ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [V,InfD,SupD] :
( ( leq(V,SupD)
& leq(InfD,V) )
=> completion_compatible(V,InfD,SupD) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [U,V,InfD,SupD] :
( ( less(U,V)
& leq(V,SupD)
& leq(InfD,V)
& leq(U,SupD)
& leq(InfD,U) )
=> completion_conflict(U,V,InfD,SupD) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [U,L] :
( prec(U,L,c,c)
<=> less(U,L) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [U,L] :
( prec(U,L,o,o)
<=> leq(U,L) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [L1,U1,CL1,CU1,L2,U2,CL2,CU2] :
( disjoint(L1,U1,CL1,CU1,L2,U2,CL2,CU2)
<=> ( prec(U2,L1,CU2,CL1)
| prec(U1,L2,CU1,CL2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,hypothesis,
less(n3,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,hypothesis,
less(n5,n10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,hypothesis,
less(n10,n20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,hypothesis,
! [X] : leq(ninf,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,hypothesis,
! [X] : leq(X,nsup),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,conjecture,
( box_verdict(conflict,unknown) = conflict
& completion_compatible(n5,ninf,nsup)
& completion_conflict(n5,n10,ninf,nsup)
& ~ disjoint(n5,nsup,o,c,ninf,n10,c,o)
& ? [Z] :
( less(Z,n10)
& less(n5,Z) )
& axis_conflict(n0,n3,n10,n20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f61,negated_conjecture,
~ ( box_verdict(conflict,unknown) = conflict
& completion_compatible(n5,ninf,nsup)
& completion_conflict(n5,n10,ninf,nsup)
& ~ disjoint(n5,nsup,o,c,ninf,n10,c,o)
& ? [Z] :
( less(Z,n10)
& less(n5,Z) )
& axis_conflict(n0,n3,n10,n20) ),
inference(negated_conjecture,[status(cth)],[f60]) ).
fof(f62,plain,
! [X0] : ~ less(X0,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f63,plain,
! [X,Y,Z] :
( less(X,Z)
| ~ less(Y,Z)
| ~ less(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f64,plain,
! [X,Z] :
( less(X,Z)
| ! [Y] :
( ~ less(Y,Z)
| ~ less(X,Y) ) ),
inference(miniscoping,[status(thm)],[f63]) ).
fof(f65,plain,
! [X0,X1,X2] :
( less(X0,X2)
| ~ less(X1,X2)
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f66,plain,
! [X0,X1] :
( less(X1,X0)
| X0 = X1
| less(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f67,plain,
! [X,Y] :
( ( ( X != Y
& ~ less(X,Y) )
| leq(X,Y) )
& ( X = Y
| less(X,Y)
| ~ leq(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f4]) ).
fof(f68,plain,
( ! [X,Y] :
( ( X != Y
& ~ less(X,Y) )
| leq(X,Y) )
& ! [X,Y] :
( X = Y
| less(X,Y)
| ~ leq(X,Y) ) ),
inference(miniscoping,[status(thm)],[f67]) ).
fof(f70,plain,
! [X0,X1] :
( ~ less(X0,X1)
| leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f76,plain,
! [X,Y,Z] :
( less(X,Z)
| ~ less(Y,Z)
| ~ leq(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f77,plain,
! [X,Z] :
( less(X,Z)
| ! [Y] :
( ~ less(Y,Z)
| ~ leq(X,Y) ) ),
inference(miniscoping,[status(thm)],[f76]) ).
fof(f78,plain,
! [X0,X1,X2] :
( less(X0,X2)
| ~ less(X1,X2)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f85,plain,
! [X,Y] :
( ? [Z] :
( less(Z,Y)
& less(X,Z) )
| ~ less(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f86,plain,
! [X,Y] :
( ( less(sK0_skl(Y,X),Y)
& less(X,sK0_skl(Y,X)) )
| ~ less(X,Y) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Z,sK0_skl(Y,X))],[f85]) ).
fof(f87,plain,
! [X0,X1] :
( less(X0,sK0_skl(X1,X0))
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f88,plain,
! [X0,X1] :
( less(sK0_skl(X1,X0),X1)
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f89,plain,
! [X,A,B] :
( ( ~ leq(X,B)
| ~ leq(A,X)
| in_closed(X,A,B) )
& ( ( leq(X,B)
& leq(A,X) )
| ~ in_closed(X,A,B) ) ),
inference(NNF_transformation,[status(thm)],[f11]) ).
fof(f90,plain,
( ! [X,A,B] :
( ~ leq(X,B)
| ~ leq(A,X)
| in_closed(X,A,B) )
& ! [X,A,B] :
( ( leq(X,B)
& leq(A,X) )
| ~ in_closed(X,A,B) ) ),
inference(miniscoping,[status(thm)],[f89]) ).
fof(f91,plain,
! [X0,X1,X2] :
( leq(X1,X0)
| ~ in_closed(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f92,plain,
! [X0,X1,X2] :
( leq(X0,X2)
| ~ in_closed(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f109,plain,
! [I1lo,I1hi,I2lo,I2hi] :
( axis_conflict(I1lo,I1hi,I2lo,I2hi)
<=> ! [X] :
( ~ in_closed(X,I2lo,I2hi)
| ~ in_closed(X,I1lo,I1hi) ) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f110,plain,
! [I1lo,I1hi,I2lo,I2hi] :
( ( ? [X] :
( in_closed(X,I2lo,I2hi)
& in_closed(X,I1lo,I1hi) )
| axis_conflict(I1lo,I1hi,I2lo,I2hi) )
& ( ! [X] :
( ~ in_closed(X,I2lo,I2hi)
| ~ in_closed(X,I1lo,I1hi) )
| ~ axis_conflict(I1lo,I1hi,I2lo,I2hi) ) ),
inference(NNF_transformation,[status(thm)],[f109]) ).
fof(f111,plain,
( ! [I1lo,I1hi,I2lo,I2hi] :
( ? [X] :
( in_closed(X,I2lo,I2hi)
& in_closed(X,I1lo,I1hi) )
| axis_conflict(I1lo,I1hi,I2lo,I2hi) )
& ! [I1lo,I1hi,I2lo,I2hi] :
( ! [X] :
( ~ in_closed(X,I2lo,I2hi)
| ~ in_closed(X,I1lo,I1hi) )
| ~ axis_conflict(I1lo,I1hi,I2lo,I2hi) ) ),
inference(miniscoping,[status(thm)],[f110]) ).
fof(f112,plain,
( ! [I1lo,I1hi,I2lo,I2hi] :
( ( in_closed(sK1_skl(I2hi,I2lo,I1hi,I1lo),I2lo,I2hi)
& in_closed(sK1_skl(I2hi,I2lo,I1hi,I1lo),I1lo,I1hi) )
| axis_conflict(I1lo,I1hi,I2lo,I2hi) )
& ! [I1lo,I1hi,I2lo,I2hi] :
( ! [X] :
( ~ in_closed(X,I2lo,I2hi)
| ~ in_closed(X,I1lo,I1hi) )
| ~ axis_conflict(I1lo,I1hi,I2lo,I2hi) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(X,sK1_skl(I2hi,I2lo,I1hi,I1lo))],[f111]) ).
fof(f114,plain,
! [X0,X1,X2,X3] :
( in_closed(sK1_skl(X3,X2,X1,X0),X0,X1)
| axis_conflict(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f115,plain,
! [X0,X1,X2,X3] :
( in_closed(sK1_skl(X3,X2,X1,X0),X2,X3)
| axis_conflict(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f129,plain,
is_verdict(conflict),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f130,plain,
is_verdict(compatible),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f131,plain,
is_verdict(unknown),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f132,plain,
conflict != compatible,
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f133,plain,
conflict != unknown,
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f134,plain,
compatible != unknown,
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f137,plain,
! [V1,V2] :
( box_verdict(V1,V2) = conflict
| ( V2 != conflict
& V1 != conflict )
| ~ is_verdict(V2)
| ~ is_verdict(V1) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f138,plain,
! [X0,X1] :
( box_verdict(X0,X1) = conflict
| X0 != conflict
| ~ is_verdict(X1)
| ~ is_verdict(X0) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f140,plain,
! [V1,V2] :
( box_verdict(V1,V2) = compatible
| V2 != compatible
| V1 != compatible
| ~ is_verdict(V2)
| ~ is_verdict(V1) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f141,plain,
! [X0,X1] :
( box_verdict(X0,X1) = compatible
| X1 != compatible
| X0 != compatible
| ~ is_verdict(X1)
| ~ is_verdict(X0) ),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f147,plain,
! [V,InfD,SupD] :
( completion_compatible(V,InfD,SupD)
| ~ leq(V,SupD)
| ~ leq(InfD,V) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f148,plain,
! [X0,X1,X2] :
( completion_compatible(X1,X0,X2)
| ~ leq(X1,X2)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f149,plain,
! [U,V,InfD,SupD] :
( completion_conflict(U,V,InfD,SupD)
| ~ less(U,V)
| ~ leq(V,SupD)
| ~ leq(InfD,V)
| ~ leq(U,SupD)
| ~ leq(InfD,U) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f150,plain,
! [X0,X1,X2,X3] :
( completion_conflict(X1,X3,X0,X2)
| ~ less(X1,X3)
| ~ leq(X3,X2)
| ~ leq(X0,X3)
| ~ leq(X1,X2)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f166,plain,
! [U,L] :
( ( ~ less(U,L)
| prec(U,L,c,c) )
& ( less(U,L)
| ~ prec(U,L,c,c) ) ),
inference(NNF_transformation,[status(thm)],[f39]) ).
fof(f167,plain,
( ! [U,L] :
( ~ less(U,L)
| prec(U,L,c,c) )
& ! [U,L] :
( less(U,L)
| ~ prec(U,L,c,c) ) ),
inference(miniscoping,[status(thm)],[f166]) ).
fof(f168,plain,
! [X0,X1] :
( less(X0,X1)
| ~ prec(X0,X1,c,c) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f178,plain,
! [U,L] :
( ( ~ leq(U,L)
| prec(U,L,o,o) )
& ( leq(U,L)
| ~ prec(U,L,o,o) ) ),
inference(NNF_transformation,[status(thm)],[f42]) ).
fof(f179,plain,
( ! [U,L] :
( ~ leq(U,L)
| prec(U,L,o,o) )
& ! [U,L] :
( leq(U,L)
| ~ prec(U,L,o,o) ) ),
inference(miniscoping,[status(thm)],[f178]) ).
fof(f180,plain,
! [X0,X1] :
( leq(X0,X1)
| ~ prec(X0,X1,o,o) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f182,plain,
! [L1,U1,CL1,CU1,L2,U2,CL2,CU2] :
( ( ( ~ prec(U2,L1,CU2,CL1)
& ~ prec(U1,L2,CU1,CL2) )
| disjoint(L1,U1,CL1,CU1,L2,U2,CL2,CU2) )
& ( prec(U2,L1,CU2,CL1)
| prec(U1,L2,CU1,CL2)
| ~ disjoint(L1,U1,CL1,CU1,L2,U2,CL2,CU2) ) ),
inference(NNF_transformation,[status(thm)],[f43]) ).
fof(f183,plain,
( ! [L1,U1,CL1,CU1,L2,U2,CL2,CU2] :
( ( ~ prec(U2,L1,CU2,CL1)
& ~ prec(U1,L2,CU1,CL2) )
| disjoint(L1,U1,CL1,CU1,L2,U2,CL2,CU2) )
& ! [L1,U1,CL1,CU1,L2,U2,CL2,CU2] :
( prec(U2,L1,CU2,CL1)
| prec(U1,L2,CU1,CL2)
| ~ disjoint(L1,U1,CL1,CU1,L2,U2,CL2,CU2) ) ),
inference(miniscoping,[status(thm)],[f182]) ).
fof(f184,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( prec(X5,X0,X7,X2)
| prec(X1,X4,X3,X6)
| ~ disjoint(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f198,plain,
less(n3,n5),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f199,plain,
less(n5,n10),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f200,plain,
less(n10,n20),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f201,plain,
! [X0] : leq(ninf,X0),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f202,plain,
! [X0] : leq(X0,nsup),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f203,plain,
( box_verdict(conflict,unknown) != conflict
| ~ completion_compatible(n5,ninf,nsup)
| ~ completion_conflict(n5,n10,ninf,nsup)
| disjoint(n5,nsup,o,c,ninf,n10,c,o)
| ! [Z] :
( ~ less(Z,n10)
| ~ less(n5,Z) )
| ~ axis_conflict(n0,n3,n10,n20) ),
inference(pre_NNF_transformation,[status(thm)],[f61]) ).
fof(f204,plain,
! [X0] :
( box_verdict(conflict,unknown) != conflict
| ~ completion_compatible(n5,ninf,nsup)
| ~ completion_conflict(n5,n10,ninf,nsup)
| disjoint(n5,nsup,o,c,ninf,n10,c,o)
| ~ less(X0,n10)
| ~ less(n5,X0)
| ~ axis_conflict(n0,n3,n10,n20) ),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f205,definition,
( sQ0_spl
<=> axis_conflict(n0,n3,n10,n20) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f207,plain,
( sQ0_spl
| ~ axis_conflict(n0,n3,n10,n20) ),
inference(component_clause,[status(thm)],[f205]) ).
fof(f208,definition,
! [X0] :
( sQ1_spl
<=> ( ~ less(X0,n10)
| ~ less(n5,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f209,plain,
! [X0] :
( ~ sQ1_spl
| ~ less(X0,n10)
| ~ less(n5,X0) ),
inference(component_clause,[status(thm)],[f208]) ).
fof(f211,definition,
( sQ2_spl
<=> disjoint(n5,nsup,o,c,ninf,n10,c,o) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f212,plain,
( ~ sQ2_spl
| disjoint(n5,nsup,o,c,ninf,n10,c,o) ),
inference(component_clause,[status(thm)],[f211]) ).
fof(f214,definition,
( sQ3_spl
<=> completion_conflict(n5,n10,ninf,nsup) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f216,plain,
( sQ3_spl
| ~ completion_conflict(n5,n10,ninf,nsup) ),
inference(component_clause,[status(thm)],[f214]) ).
fof(f217,definition,
( sQ4_spl
<=> completion_compatible(n5,ninf,nsup) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f219,plain,
( sQ4_spl
| ~ completion_compatible(n5,ninf,nsup) ),
inference(component_clause,[status(thm)],[f217]) ).
fof(f220,definition,
( sQ5_spl
<=> box_verdict(conflict,unknown) = conflict ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f222,plain,
( sQ5_spl
| box_verdict(conflict,unknown) != conflict ),
inference(component_clause,[status(thm)],[f220]) ).
fof(f223,plain,
( ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| sQ2_spl
| sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f204,f205,f208,f211,f214,f217,f220]) ).
fof(f225,plain,
! [X0] :
( box_verdict(conflict,X0) = conflict
| ~ is_verdict(X0)
| ~ is_verdict(conflict) ),
inference(destructive_equality_resolution,[status(thm)],[f138]) ).
fof(f227,plain,
( box_verdict(compatible,compatible) = compatible
| ~ is_verdict(compatible)
| ~ is_verdict(compatible) ),
inference(destructive_equality_resolution,[status(thm)],[f141]) ).
fof(f228,plain,
( box_verdict(compatible,compatible) = compatible
| ~ is_verdict(compatible) ),
inference(duplicate_literals_removal,[status(thm)],[f227]) ).
fof(f232,plain,
! [X0] :
( less(X0,n5)
| ~ less(X0,n3) ),
inference(resolution,[status(thm)],[f198,f65]) ).
fof(f260,plain,
! [X0,X1] :
( ~ less(X1,X0)
| ~ leq(X0,X1) ),
inference(resolution,[status(thm)],[f78,f62]) ).
fof(f276,plain,
! [X0] : ~ less(nsup,X0),
inference(resolution,[status(thm)],[f260,f202]) ).
fof(f277,plain,
! [X0,X1] :
( ~ less(X1,X0)
| ~ less(X0,X1) ),
inference(resolution,[status(thm)],[f260,f70]) ).
fof(f289,plain,
~ less(n10,n5),
inference(resolution,[status(thm)],[f277,f199]) ).
fof(f290,plain,
~ less(n5,n3),
inference(resolution,[status(thm)],[f277,f198]) ).
fof(f329,definition,
( sQ13_spl
<=> less(n5,n10) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f331,plain,
( sQ13_spl
| ~ less(n5,n10) ),
inference(component_clause,[status(thm)],[f329]) ).
fof(f342,definition,
( sQ15_spl
<=> n10 = n3 ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f343,plain,
( ~ sQ15_spl
| n10 = n3 ),
inference(component_clause,[status(thm)],[f342]) ).
fof(f346,definition,
( sQ16_spl
<=> less(n3,n10) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f347,plain,
( ~ sQ16_spl
| less(n3,n10) ),
inference(component_clause,[status(thm)],[f346]) ).
fof(f386,plain,
! [X0] :
( box_verdict(conflict,X0) = conflict
| ~ is_verdict(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f225,f129]) ).
fof(f387,plain,
box_verdict(conflict,compatible) = conflict,
inference(resolution,[status(thm)],[f386,f130]) ).
fof(f388,plain,
box_verdict(conflict,unknown) = conflict,
inference(resolution,[status(thm)],[f386,f131]) ).
fof(f390,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f388,f222]) ).
fof(f391,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f390]) ).
fof(f507,plain,
( sQ4_spl
| ~ leq(n5,nsup)
| ~ leq(ninf,n5) ),
inference(resolution,[status(thm)],[f148,f219]) ).
fof(f508,definition,
( sQ32_spl
<=> leq(ninf,n5) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f510,plain,
( sQ32_spl
| ~ leq(ninf,n5) ),
inference(component_clause,[status(thm)],[f508]) ).
fof(f511,definition,
( sQ33_spl
<=> leq(n5,nsup) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f513,plain,
( sQ33_spl
| ~ leq(n5,nsup) ),
inference(component_clause,[status(thm)],[f511]) ).
fof(f514,plain,
( sQ4_spl
| ~ sQ33_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f507,f508,f511,f217]) ).
fof(f515,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f513,f202]) ).
fof(f516,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f515]) ).
fof(f517,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f510,f201]) ).
fof(f518,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f517]) ).
fof(f538,plain,
( ~ sQ15_spl
| ~ less(n5,n10) ),
inference(backward_demodulation,[status(thm)],[f343,f290]) ).
fof(f545,plain,
( ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f538,f199]) ).
fof(f546,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f545]) ).
fof(f549,plain,
( sQ3_spl
| ~ less(n5,n10)
| ~ leq(n10,nsup)
| ~ leq(ninf,n10)
| ~ leq(n5,nsup)
| ~ leq(ninf,n5) ),
inference(resolution,[status(thm)],[f216,f150]) ).
fof(f550,definition,
( sQ34_spl
<=> leq(ninf,n10) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f552,plain,
( sQ34_spl
| ~ leq(ninf,n10) ),
inference(component_clause,[status(thm)],[f550]) ).
fof(f553,definition,
( sQ35_spl
<=> leq(n10,nsup) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f555,plain,
( sQ35_spl
| ~ leq(n10,nsup) ),
inference(component_clause,[status(thm)],[f553]) ).
fof(f556,plain,
( sQ3_spl
| ~ sQ13_spl
| ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ33_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f549,f508,f511,f550,f553,f329,f214]) ).
fof(f557,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f555,f202]) ).
fof(f558,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f557]) ).
fof(f559,plain,
( sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f552,f201]) ).
fof(f560,plain,
sQ34_spl,
inference(contradiction_clause,[status(thm)],[f559]) ).
fof(f561,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f331,f199]) ).
fof(f562,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f561]) ).
fof(f701,plain,
~ less(n10,n3),
inference(resolution,[status(thm)],[f232,f289]) ).
fof(f712,plain,
( n3 = n10
| less(n3,n10) ),
inference(resolution,[status(thm)],[f701,f66]) ).
fof(f714,plain,
( sQ15_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f712,f346,f342]) ).
fof(f1030,plain,
box_verdict(compatible,compatible) = compatible,
inference(forward_subsumption_resolution,[status(thm)],[f228,f130]) ).
fof(f1328,plain,
! [X0] :
( ~ sQ16_spl
| less(X0,n10)
| ~ leq(X0,n3) ),
inference(resolution,[status(thm)],[f347,f78]) ).
fof(f1505,plain,
( ~ sQ2_spl
| prec(n10,n5,o,o)
| prec(nsup,ninf,c,c) ),
inference(resolution,[status(thm)],[f184,f212]) ).
fof(f1506,definition,
( sQ75_spl
<=> prec(nsup,ninf,c,c) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1507,plain,
( ~ sQ75_spl
| prec(nsup,ninf,c,c) ),
inference(component_clause,[status(thm)],[f1506]) ).
fof(f1509,definition,
( sQ76_spl
<=> prec(n10,n5,o,o) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1510,plain,
( ~ sQ76_spl
| prec(n10,n5,o,o) ),
inference(component_clause,[status(thm)],[f1509]) ).
fof(f1512,plain,
( ~ sQ2_spl
| sQ76_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f1505,f1506,f1509,f211]) ).
fof(f1555,plain,
( ~ sQ76_spl
| leq(n10,n5) ),
inference(resolution,[status(thm)],[f1510,f180]) ).
fof(f1681,plain,
( sQ0_spl
| in_closed(sK1_skl(n20,n10,n3,n0),n10,n20) ),
inference(resolution,[status(thm)],[f207,f115]) ).
fof(f1682,plain,
( sQ0_spl
| in_closed(sK1_skl(n20,n10,n3,n0),n0,n3) ),
inference(resolution,[status(thm)],[f207,f114]) ).
fof(f1738,plain,
( ~ sQ75_spl
| less(nsup,ninf) ),
inference(resolution,[status(thm)],[f168,f1507]) ).
fof(f1740,plain,
( ~ sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1738,f276]) ).
fof(f1741,plain,
~ sQ75_spl,
inference(contradiction_clause,[status(thm)],[f1740]) ).
fof(f1745,plain,
( ~ sQ76_spl
| ~ less(n5,n10) ),
inference(resolution,[status(thm)],[f1555,f260]) ).
fof(f1752,plain,
( ~ sQ76_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1745,f329,f1509]) ).
fof(f1753,definition,
( sQ84_spl
<=> less(n10,n5) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1754,plain,
( ~ sQ84_spl
| less(n10,n5) ),
inference(component_clause,[status(thm)],[f1753]) ).
fof(f1818,plain,
( sQ0_spl
| leq(n10,sK1_skl(n20,n10,n3,n0)) ),
inference(resolution,[status(thm)],[f1681,f91]) ).
fof(f1889,definition,
( sQ85_spl
<=> box_verdict(compatible,compatible) = conflict ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1890,plain,
( ~ sQ85_spl
| box_verdict(compatible,compatible) = conflict ),
inference(component_clause,[status(thm)],[f1889]) ).
fof(f1895,definition,
( sQ87_spl
<=> box_verdict(compatible,compatible) = unknown ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1896,plain,
( ~ sQ87_spl
| box_verdict(compatible,compatible) = unknown ),
inference(component_clause,[status(thm)],[f1895]) ).
fof(f1912,definition,
( sQ92_spl
<=> box_verdict(conflict,compatible) = compatible ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f1913,plain,
( ~ sQ92_spl
| box_verdict(conflict,compatible) = compatible ),
inference(component_clause,[status(thm)],[f1912]) ).
fof(f1915,definition,
( sQ93_spl
<=> box_verdict(conflict,compatible) = unknown ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1916,plain,
( ~ sQ93_spl
| box_verdict(conflict,compatible) = unknown ),
inference(component_clause,[status(thm)],[f1915]) ).
fof(f1919,plain,
( ~ sQ93_spl
| conflict = unknown ),
inference(forward_demodulation,[status(thm)],[f387,f1916]) ).
fof(f1920,plain,
( ~ sQ93_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1919,f133]) ).
fof(f1921,plain,
~ sQ93_spl,
inference(contradiction_clause,[status(thm)],[f1920]) ).
fof(f1922,plain,
( ~ sQ92_spl
| conflict = compatible ),
inference(forward_demodulation,[status(thm)],[f387,f1913]) ).
fof(f1923,plain,
( ~ sQ92_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1922,f132]) ).
fof(f1924,plain,
~ sQ92_spl,
inference(contradiction_clause,[status(thm)],[f1923]) ).
fof(f1925,plain,
( ~ sQ87_spl
| compatible = unknown ),
inference(forward_demodulation,[status(thm)],[f1030,f1896]) ).
fof(f1926,plain,
( ~ sQ87_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1925,f134]) ).
fof(f1927,plain,
~ sQ87_spl,
inference(contradiction_clause,[status(thm)],[f1926]) ).
fof(f1930,plain,
( ~ sQ85_spl
| compatible = conflict ),
inference(forward_demodulation,[status(thm)],[f1030,f1890]) ).
fof(f1931,plain,
( ~ sQ85_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1930,f132]) ).
fof(f1932,plain,
~ sQ85_spl,
inference(contradiction_clause,[status(thm)],[f1931]) ).
fof(f1940,plain,
( sQ0_spl
| ~ less(sK1_skl(n20,n10,n3,n0),n10) ),
inference(resolution,[status(thm)],[f1818,f260]) ).
fof(f1974,definition,
( sQ97_spl
<=> is_verdict(compatible) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1976,plain,
( sQ97_spl
| ~ is_verdict(compatible) ),
inference(component_clause,[status(thm)],[f1974]) ).
fof(f1978,plain,
( sQ97_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1976,f130]) ).
fof(f1979,plain,
sQ97_spl,
inference(contradiction_clause,[status(thm)],[f1978]) ).
fof(f2013,definition,
! [X0] :
( sQ99_spl
<=> ~ less(n10,X0) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f2014,plain,
! [X0] :
( ~ sQ99_spl
| ~ less(n10,X0) ),
inference(component_clause,[status(thm)],[f2013]) ).
fof(f2017,definition,
( sQ100_spl
<=> nsup = n10 ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f2018,plain,
( ~ sQ100_spl
| nsup = n10 ),
inference(component_clause,[status(thm)],[f2017]) ).
fof(f2265,definition,
! [X0,X1] :
( sQ110_spl
<=> less(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f2266,plain,
! [X0,X1] :
( ~ sQ110_spl
| less(X0,X1) ),
inference(component_clause,[status(thm)],[f2265]) ).
fof(f2486,plain,
( ~ sQ100_spl
| less(nsup,n20) ),
inference(backward_demodulation,[status(thm)],[f2018,f200]) ).
fof(f2496,plain,
( ~ sQ100_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2486,f276]) ).
fof(f2497,plain,
~ sQ100_spl,
inference(contradiction_clause,[status(thm)],[f2496]) ).
fof(f2538,plain,
( sQ0_spl
| leq(sK1_skl(n20,n10,n3,n0),n3) ),
inference(resolution,[status(thm)],[f1682,f92]) ).
fof(f2657,plain,
! [X0] :
( ~ sQ1_spl
| ~ less(n5,X0)
| ~ less(sK0_skl(X0,n5),n10) ),
inference(resolution,[status(thm)],[f209,f87]) ).
fof(f2664,plain,
( ~ sQ99_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f200,f2014]) ).
fof(f2671,plain,
~ sQ99_spl,
inference(contradiction_clause,[status(thm)],[f2664]) ).
fof(f2752,definition,
( sQ127_spl
<=> less(n5,n5) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f2753,plain,
( ~ sQ127_spl
| less(n5,n5) ),
inference(component_clause,[status(thm)],[f2752]) ).
fof(f2764,plain,
( ~ sQ127_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2753,f62]) ).
fof(f2765,plain,
~ sQ127_spl,
inference(contradiction_clause,[status(thm)],[f2764]) ).
fof(f3828,plain,
( ~ sQ16_spl
| sQ0_spl
| less(sK1_skl(n20,n10,n3,n0),n10) ),
inference(resolution,[status(thm)],[f2538,f1328]) ).
fof(f3841,plain,
( ~ sQ16_spl
| sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3828,f1940]) ).
fof(f3842,plain,
( ~ sQ16_spl
| sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f3841]) ).
fof(f3846,plain,
( ~ sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1754,f289]) ).
fof(f3847,plain,
~ sQ84_spl,
inference(contradiction_clause,[status(thm)],[f3846]) ).
fof(f3904,plain,
! [X0,X1] :
( ~ sQ110_spl
| ~ less(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f277,f2266]) ).
fof(f3920,plain,
( ~ sQ110_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3904,f2266]) ).
fof(f3921,plain,
~ sQ110_spl,
inference(contradiction_clause,[status(thm)],[f3920]) ).
fof(f4141,plain,
( ~ sQ1_spl
| ~ less(n5,n10)
| ~ less(n5,n10) ),
inference(resolution,[status(thm)],[f2657,f88]) ).
fof(f4143,plain,
( ~ sQ1_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f4141,f329,f208]) ).
fof(f4144,plain,
$false,
inference(sat_refutation,[status(thm)],[f223,f391,f514,f516,f518,f546,f556,f558,f560,f562,f714,f1512,f1741,f1752,f1921,f1924,f1927,f1932,f1979,f2497,f2671,f2765,f3842,f3847,f3921,f4143]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT068+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n016.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 01:29:37 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 5.50/1.30 % Refutation found
% 5.50/1.30 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.50/1.30 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.51/1.34 % Elapsed time: 0.965007 seconds
% 2.51/1.34 % CPU time: 7.193854 seconds
% 2.51/1.34 % Total memory used: 133.551 MB
% 2.51/1.34 % Net memory used: 125.607 MB
%------------------------------------------------------------------------------