%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : MGT091+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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:35 PM UTC 2026
% Result : Theorem 0.17s 0.51s
% Output : CNFRefutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 14
% Syntax : Number of formulae : 59 ( 15 unt; 6 def)
% Number of atoms : 153 ( 6 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 157 ( 63 ~; 63 |; 21 &)
% ( 10 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 7 prp; 0-8 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-4 aty)
% Number of variables : 105 ( 102 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X,Y] :
( leq(X,Y)
<=> ( X = Y
| less(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,A,B] :
( in_closed(X,A,B)
<=> ( leq(X,B)
& leq(A,X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [I1lo,I1hi,I2lo,I2hi] :
( axis_compatible(I1lo,I1hi,I2lo,I2hi)
<=> ? [X] :
( in_closed(X,I2lo,I2hi)
& in_closed(X,I1lo,I1hi) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [A1,B1,A2,B2,C1,D1,C2,D2] :
( box2_compatible(A1,B1,A2,B2,C1,D1,C2,D2)
<=> ( axis_compatible(A2,B2,C2,D2)
& axis_compatible(A1,B1,C1,D1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
less(v0,v400),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
less(v400,v600),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
less(v400,v800),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,conjecture,
box2_compatible(v0,v600,v0,v600,v400,v800,v400,v800),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,negated_conjecture,
~ box2_compatible(v0,v600,v0,v600,v400,v800,v400,v800),
inference(negated_conjecture,[status(cth)],[f47]) ).
fof(f54,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(f55,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)],[f54]) ).
fof(f57,plain,
! [X0,X1] :
( ~ less(X0,X1)
| leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f58,plain,
! [X0,X1] :
( X0 != X1
| leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f72,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)],[f10]) ).
fof(f73,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)],[f72]) ).
fof(f76,plain,
! [X0,X1,X2] :
( ~ leq(X0,X2)
| ~ leq(X1,X0)
| in_closed(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f99,plain,
! [I1lo,I1hi,I2lo,I2hi] :
( ( ! [X] :
( ~ in_closed(X,I2lo,I2hi)
| ~ in_closed(X,I1lo,I1hi) )
| axis_compatible(I1lo,I1hi,I2lo,I2hi) )
& ( ? [X] :
( in_closed(X,I2lo,I2hi)
& in_closed(X,I1lo,I1hi) )
| ~ axis_compatible(I1lo,I1hi,I2lo,I2hi) ) ),
inference(NNF_transformation,[status(thm)],[f15]) ).
fof(f100,plain,
( ! [I1lo,I1hi,I2lo,I2hi] :
( ! [X] :
( ~ in_closed(X,I2lo,I2hi)
| ~ in_closed(X,I1lo,I1hi) )
| axis_compatible(I1lo,I1hi,I2lo,I2hi) )
& ! [I1lo,I1hi,I2lo,I2hi] :
( ? [X] :
( in_closed(X,I2lo,I2hi)
& in_closed(X,I1lo,I1hi) )
| ~ axis_compatible(I1lo,I1hi,I2lo,I2hi) ) ),
inference(miniscoping,[status(thm)],[f99]) ).
fof(f101,plain,
( ! [I1lo,I1hi,I2lo,I2hi] :
( ! [X] :
( ~ in_closed(X,I2lo,I2hi)
| ~ in_closed(X,I1lo,I1hi) )
| axis_compatible(I1lo,I1hi,I2lo,I2hi) )
& ! [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_compatible(I1lo,I1hi,I2lo,I2hi) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(X,sK1_skl(I2hi,I2lo,I1hi,I1lo))],[f100]) ).
fof(f104,plain,
! [X0,X1,X2,X3,X4] :
( ~ in_closed(X4,X2,X3)
| ~ in_closed(X4,X0,X1)
| axis_compatible(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f141,plain,
! [A1,B1,A2,B2,C1,D1,C2,D2] :
( ( ~ axis_compatible(A2,B2,C2,D2)
| ~ axis_compatible(A1,B1,C1,D1)
| box2_compatible(A1,B1,A2,B2,C1,D1,C2,D2) )
& ( ( axis_compatible(A2,B2,C2,D2)
& axis_compatible(A1,B1,C1,D1) )
| ~ box2_compatible(A1,B1,A2,B2,C1,D1,C2,D2) ) ),
inference(NNF_transformation,[status(thm)],[f30]) ).
fof(f142,plain,
( ! [A1,B1,A2,B2,C1,D1,C2,D2] :
( ~ axis_compatible(A2,B2,C2,D2)
| ~ axis_compatible(A1,B1,C1,D1)
| box2_compatible(A1,B1,A2,B2,C1,D1,C2,D2) )
& ! [A1,B1,A2,B2,C1,D1,C2,D2] :
( ( axis_compatible(A2,B2,C2,D2)
& axis_compatible(A1,B1,C1,D1) )
| ~ box2_compatible(A1,B1,A2,B2,C1,D1,C2,D2) ) ),
inference(miniscoping,[status(thm)],[f141]) ).
fof(f145,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ axis_compatible(X2,X3,X6,X7)
| ~ axis_compatible(X0,X1,X4,X5)
| box2_compatible(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f179,plain,
less(v0,v400),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f181,plain,
less(v400,v600),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f182,plain,
less(v400,v800),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f190,plain,
~ box2_compatible(v0,v600,v0,v600,v400,v800,v400,v800),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f191,plain,
! [X0] : leq(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f58]) ).
fof(f204,plain,
( ~ axis_compatible(v0,v600,v400,v800)
| ~ axis_compatible(v0,v600,v400,v800) ),
inference(resolution,[status(thm)],[f145,f190]) ).
fof(f205,definition,
( sQ0_spl
<=> axis_compatible(v0,v600,v400,v800) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f207,plain,
( sQ0_spl
| ~ axis_compatible(v0,v600,v400,v800) ),
inference(component_clause,[status(thm)],[f205]) ).
fof(f208,plain,
~ sQ0_spl,
inference(split_clause,[status(thm)],[f204,f205]) ).
fof(f381,plain,
! [X0] :
( sQ0_spl
| ~ in_closed(X0,v400,v800)
| ~ in_closed(X0,v0,v600) ),
inference(resolution,[status(thm)],[f104,f207]) ).
fof(f387,plain,
! [X0] :
( sQ0_spl
| ~ leq(X0,v800)
| ~ leq(v400,X0)
| ~ in_closed(X0,v0,v600) ),
inference(resolution,[status(thm)],[f381,f76]) ).
fof(f403,plain,
( sQ0_spl
| ~ leq(v400,v800)
| ~ in_closed(v400,v0,v600) ),
inference(resolution,[status(thm)],[f387,f191]) ).
fof(f404,definition,
( sQ27_spl
<=> in_closed(v400,v0,v600) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f406,plain,
( sQ27_spl
| ~ in_closed(v400,v0,v600) ),
inference(component_clause,[status(thm)],[f404]) ).
fof(f407,definition,
( sQ28_spl
<=> leq(v400,v800) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f409,plain,
( sQ28_spl
| ~ leq(v400,v800) ),
inference(component_clause,[status(thm)],[f407]) ).
fof(f410,plain,
( sQ0_spl
| ~ sQ28_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f403,f404,f407,f205]) ).
fof(f467,definition,
( sQ36_spl
<=> less(v400,v800) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f469,plain,
( sQ36_spl
| ~ less(v400,v800) ),
inference(component_clause,[status(thm)],[f467]) ).
fof(f471,plain,
( sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f469,f182]) ).
fof(f472,plain,
sQ36_spl,
inference(contradiction_clause,[status(thm)],[f471]) ).
fof(f473,plain,
( sQ27_spl
| ~ leq(v400,v600)
| ~ leq(v0,v400) ),
inference(resolution,[status(thm)],[f406,f76]) ).
fof(f474,definition,
( sQ37_spl
<=> leq(v0,v400) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f476,plain,
( sQ37_spl
| ~ leq(v0,v400) ),
inference(component_clause,[status(thm)],[f474]) ).
fof(f477,definition,
( sQ38_spl
<=> leq(v400,v600) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f479,plain,
( sQ38_spl
| ~ leq(v400,v600) ),
inference(component_clause,[status(thm)],[f477]) ).
fof(f480,plain,
( sQ27_spl
| ~ sQ38_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f473,f474,f477,f404]) ).
fof(f484,plain,
( sQ28_spl
| ~ less(v400,v800) ),
inference(resolution,[status(thm)],[f409,f57]) ).
fof(f485,plain,
( sQ28_spl
| ~ sQ36_spl ),
inference(split_clause,[status(thm)],[f484,f467,f407]) ).
fof(f538,plain,
( sQ38_spl
| ~ less(v400,v600) ),
inference(resolution,[status(thm)],[f479,f57]) ).
fof(f539,plain,
( sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f538,f181]) ).
fof(f540,plain,
sQ38_spl,
inference(contradiction_clause,[status(thm)],[f539]) ).
fof(f577,plain,
( sQ37_spl
| ~ less(v0,v400) ),
inference(resolution,[status(thm)],[f476,f57]) ).
fof(f578,plain,
( sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f577,f179]) ).
fof(f579,plain,
sQ37_spl,
inference(contradiction_clause,[status(thm)],[f578]) ).
fof(f580,plain,
$false,
inference(sat_refutation,[status(thm)],[f208,f410,f472,f480,f485,f540,f579]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT091+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n018.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Mon Sep 21 01:28:43 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.47 % Drodi V4.1.1
% 0.17/0.51 % Refutation found
% 0.17/0.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.17/0.56 % Elapsed time: 0.103899 seconds
% 0.17/0.56 % CPU time: 0.251560 seconds
% 0.17/0.56 % Total memory used: 33.016 MB
% 0.17/0.56 % Net memory used: 32.718 MB
%------------------------------------------------------------------------------