%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT091+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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:55 PM UTC 2026
% Result : Theorem 0.22s 0.76s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT091+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.65 % Computer : n001.cluster.edu
% 0.18/0.65 % Model : x86_64 x86_64
% 0.18/0.65 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.65 % Memory : 8046.5625MB
% 0.18/0.65 % OS : Linux 6.8.0-71-generic
% 0.18/0.65 % CPULimit : 300
% 0.18/0.65 % WCLimit : 300
% 0.18/0.65 % DateTime : Mon Sep 21 01:32:13 UTC 2026
% 0.18/0.66 % CPUTime :
% 0.18/0.67 % Drodi V4.1.1
% 0.22/0.76 % Refutation found
% 0.22/0.76 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.22/0.76 % SZS output start CNFRefutation for theBenchmark
% 0.22/0.76 fof(f4,axiom,(
% 0.22/0.76 (! [X,Y] :( leq(X,Y)<=> ( less(X,Y)| X = Y ) ) )),
% 0.22/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.76 fof(f10,axiom,(
% 0.22/0.76 (! [X,A,B] :( in_closed(X,A,B)<=> ( leq(A,X)& leq(X,B) ) ) )),
% 0.22/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.76 fof(f15,axiom,(
% 0.22/0.76 (! [I1lo,I1hi,I2lo,I2hi] :( axis_compatible(I1lo,I1hi,I2lo,I2hi)<=> (? [X] :( in_closed(X,I1lo,I1hi)& in_closed(X,I2lo,I2hi) ) )) )),
% 0.22/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.76 fof(f30,axiom,(
% 0.22/0.76 (! [A1,B1,A2,B2,C1,D1,C2,D2] :( box2_compatible(A1,B1,A2,B2,C1,D1,C2,D2)<=> ( axis_compatible(A1,B1,C1,D1)& axis_compatible(A2,B2,C2,D2) ) ) )),
% 0.22/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.76 fof(f41,axiom,(
% 0.22/0.76 less(v0,v400) ),
% 0.22/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.76 fof(f43,axiom,(
% 0.22/0.76 less(v400,v600) ),
% 0.22/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.76 fof(f44,axiom,(
% 0.22/0.76 less(v400,v800) ),
% 0.22/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.76 fof(f47,conjecture,(
% 0.22/0.76 box2_compatible(v0,v600,v0,v600,v400,v800,v400,v800) ),
% 0.22/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.76 fof(f48,negated_conjecture,(
% 0.22/0.76 ~(box2_compatible(v0,v600,v0,v600,v400,v800,v400,v800) )),
% 0.22/0.76 inference(negated_conjecture,[status(cth)],[f47])).
% 0.22/0.76 fof(f54,plain,(
% 0.22/0.76 ![X,Y]: ((~leq(X,Y)|(less(X,Y)|X=Y))&(leq(X,Y)|(~less(X,Y)&~X=Y)))),
% 0.22/0.76 inference(NNF_transformation,[status(thm)],[f4])).
% 0.22/0.76 fof(f55,plain,(
% 0.22/0.76 (![X,Y]: (~leq(X,Y)|(less(X,Y)|X=Y)))&(![X,Y]: (leq(X,Y)|(~less(X,Y)&~X=Y)))),
% 0.22/0.76 inference(miniscoping,[status(thm)],[f54])).
% 0.22/0.76 fof(f57,plain,(
% 0.22/0.76 ![X0,X1]: (leq(X0,X1)|~less(X0,X1))),
% 0.22/0.76 inference(cnf_transformation,[status(thm)],[f55])).
% 0.22/0.76 fof(f58,plain,(
% 0.22/0.76 ![X0,X1]: (leq(X0,X1)|~X0=X1)),
% 0.22/0.76 inference(cnf_transformation,[status(thm)],[f55])).
% 0.22/0.76 fof(f72,plain,(
% 0.22/0.76 ![X,A,B]: ((~in_closed(X,A,B)|(leq(A,X)&leq(X,B)))&(in_closed(X,A,B)|(~leq(A,X)|~leq(X,B))))),
% 0.22/0.76 inference(NNF_transformation,[status(thm)],[f10])).
% 0.22/0.76 fof(f73,plain,(
% 0.22/0.76 (![X,A,B]: (~in_closed(X,A,B)|(leq(A,X)&leq(X,B))))&(![X,A,B]: (in_closed(X,A,B)|(~leq(A,X)|~leq(X,B))))),
% 0.22/0.76 inference(miniscoping,[status(thm)],[f72])).
% 0.22/0.76 fof(f76,plain,(
% 0.22/0.76 ![X0,X1,X2]: (in_closed(X0,X1,X2)|~leq(X1,X0)|~leq(X0,X2))),
% 0.22/0.76 inference(cnf_transformation,[status(thm)],[f73])).
% 0.22/0.76 fof(f99,plain,(
% 0.22/0.76 ![I1lo,I1hi,I2lo,I2hi]: ((~axis_compatible(I1lo,I1hi,I2lo,I2hi)|(?[X]: (in_closed(X,I1lo,I1hi)&in_closed(X,I2lo,I2hi))))&(axis_compatible(I1lo,I1hi,I2lo,I2hi)|(![X]: (~in_closed(X,I1lo,I1hi)|~in_closed(X,I2lo,I2hi)))))),
% 0.22/0.76 inference(NNF_transformation,[status(thm)],[f15])).
% 0.22/0.76 fof(f100,plain,(
% 0.22/0.76 (![I1lo,I1hi,I2lo,I2hi]: (~axis_compatible(I1lo,I1hi,I2lo,I2hi)|(?[X]: (in_closed(X,I1lo,I1hi)&in_closed(X,I2lo,I2hi)))))&(![I1lo,I1hi,I2lo,I2hi]: (axis_compatible(I1lo,I1hi,I2lo,I2hi)|(![X]: (~in_closed(X,I1lo,I1hi)|~in_closed(X,I2lo,I2hi)))))),
% 0.22/0.76 inference(miniscoping,[status(thm)],[f99])).
% 0.22/0.76 fof(f101,plain,(
% 0.22/0.76 (![I1lo,I1hi,I2lo,I2hi]: (~axis_compatible(I1lo,I1hi,I2lo,I2hi)|(in_closed(sK1_skl(I2hi,I2lo,I1hi,I1lo),I1lo,I1hi)&in_closed(sK1_skl(I2hi,I2lo,I1hi,I1lo),I2lo,I2hi))))&(![I1lo,I1hi,I2lo,I2hi]: (axis_compatible(I1lo,I1hi,I2lo,I2hi)|(![X]: (~in_closed(X,I1lo,I1hi)|~in_closed(X,I2lo,I2hi)))))),
% 0.22/0.76 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(X,sK1_skl(I2hi,I2lo,I1hi,I1lo))],[f100])).
% 0.22/0.76 fof(f104,plain,(
% 0.22/0.76 ![X0,X1,X2,X3,X4]: (axis_compatible(X0,X1,X2,X3)|~in_closed(X4,X0,X1)|~in_closed(X4,X2,X3))),
% 0.22/0.76 inference(cnf_transformation,[status(thm)],[f101])).
% 0.22/0.76 fof(f141,plain,(
% 0.22/0.76 ![A1,B1,A2,B2,C1,D1,C2,D2]: ((~box2_compatible(A1,B1,A2,B2,C1,D1,C2,D2)|(axis_compatible(A1,B1,C1,D1)&axis_compatible(A2,B2,C2,D2)))&(box2_compatible(A1,B1,A2,B2,C1,D1,C2,D2)|(~axis_compatible(A1,B1,C1,D1)|~axis_compatible(A2,B2,C2,D2))))),
% 0.22/0.76 inference(NNF_transformation,[status(thm)],[f30])).
% 0.22/0.76 fof(f142,plain,(
% 0.22/0.76 (![A1,B1,A2,B2,C1,D1,C2,D2]: (~box2_compatible(A1,B1,A2,B2,C1,D1,C2,D2)|(axis_compatible(A1,B1,C1,D1)&axis_compatible(A2,B2,C2,D2))))&(![A1,B1,A2,B2,C1,D1,C2,D2]: (box2_compatible(A1,B1,A2,B2,C1,D1,C2,D2)|(~axis_compatible(A1,B1,C1,D1)|~axis_compatible(A2,B2,C2,D2))))),
% 0.22/0.76 inference(miniscoping,[status(thm)],[f141])).
% 0.22/0.76 fof(f145,plain,(
% 0.22/0.76 ![X0,X1,X2,X3,X4,X5,X6,X7]: (box2_compatible(X0,X1,X2,X3,X4,X5,X6,X7)|~axis_compatible(X0,X1,X4,X5)|~axis_compatible(X2,X3,X6,X7))),
% 0.22/0.76 inference(cnf_transformation,[status(thm)],[f142])).
% 0.22/0.76 fof(f179,plain,(
% 0.22/0.76 less(v0,v400)),
% 0.22/0.76 inference(cnf_transformation,[status(thm)],[f41])).
% 0.22/0.76 fof(f181,plain,(
% 0.22/0.76 less(v400,v600)),
% 0.22/0.76 inference(cnf_transformation,[status(thm)],[f43])).
% 0.22/0.76 fof(f182,plain,(
% 0.22/0.76 less(v400,v800)),
% 0.22/0.76 inference(cnf_transformation,[status(thm)],[f44])).
% 0.22/0.76 fof(f190,plain,(
% 0.22/0.76 ~box2_compatible(v0,v600,v0,v600,v400,v800,v400,v800)),
% 0.22/0.76 inference(cnf_transformation,[status(thm)],[f48])).
% 0.22/0.76 fof(f191,plain,(
% 0.22/0.76 ![X0]: (leq(X0,X0))),
% 0.22/0.76 inference(destructive_equality_resolution,[status(thm)],[f58])).
% 0.22/0.76 fof(f403,plain,(
% 0.22/0.76 ![X0,X1,X2]: (in_closed(X0,X1,X2)|~leq(X0,X2)|~less(X1,X0))),
% 0.22/0.76 inference(resolution,[status(thm)],[f76,f57])).
% 0.22/0.76 fof(f404,plain,(
% 0.22/0.76 ![X0,X1]: (in_closed(X0,X0,X1)|~leq(X0,X1))),
% 0.22/0.76 inference(resolution,[status(thm)],[f76,f191])).
% 0.22/0.76 fof(f406,plain,(
% 0.22/0.76 ![X0,X1]: (in_closed(X0,X0,X1)|~less(X0,X1))),
% 0.22/0.76 inference(resolution,[status(thm)],[f404,f57])).
% 0.22/0.76 fof(f412,plain,(
% 0.22/0.76 ![X0,X1,X2]: (in_closed(X0,X1,X2)|~less(X1,X0)|~less(X0,X2))),
% 0.22/0.76 inference(resolution,[status(thm)],[f403,f57])).
% 0.22/0.76 fof(f425,plain,(
% 0.22/0.76 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~in_closed(X0,X1,X2)|~in_closed(X0,X3,X4)|box2_compatible(X5,X6,X1,X2,X7,X8,X3,X4)|~axis_compatible(X5,X6,X7,X8))),
% 0.22/0.76 inference(resolution,[status(thm)],[f104,f145])).
% 0.22/0.76 fof(f428,plain,(
% 0.22/0.76 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~in_closed(X0,X1,X2)|~in_closed(X0,X3,X4)|box2_compatible(X5,X6,X1,X2,X7,X8,X3,X4)|~in_closed(X9,X5,X6)|~in_closed(X9,X7,X8))),
% 0.22/0.76 inference(resolution,[status(thm)],[f425,f104])).
% 0.22/0.76 fof(f429,plain,(
% 0.22/0.76 ![X0,X1]: (~in_closed(X0,v0,v600)|~in_closed(X0,v400,v800)|~in_closed(X1,v0,v600)|~in_closed(X1,v400,v800))),
% 0.22/0.76 inference(resolution,[status(thm)],[f428,f190])).
% 0.22/0.76 fof(f438,plain,(
% 0.22/0.76 ~in_closed(v400,v0,v600)|~in_closed(v400,v0,v600)|~less(v400,v800)),
% 0.22/0.76 inference(resolution,[status(thm)],[f429,f406])).
% 0.22/0.76 fof(f452,plain,(
% 0.22/0.76 ~in_closed(v400,v0,v600)|~less(v400,v800)),
% 0.22/0.76 inference(duplicate_literals_removal,[status(thm)],[f438])).
% 0.22/0.76 fof(f453,plain,(
% 0.22/0.76 ~in_closed(v400,v0,v600)),
% 0.22/0.76 inference(forward_subsumption_resolution,[status(thm)],[f452,f182])).
% 0.22/0.76 fof(f457,plain,(
% 0.22/0.76 ~less(v0,v400)|~less(v400,v600)),
% 0.22/0.76 inference(resolution,[status(thm)],[f453,f412])).
% 0.22/0.76 fof(f459,plain,(
% 0.22/0.76 ~less(v400,v600)),
% 0.22/0.76 inference(forward_subsumption_resolution,[status(thm)],[f457,f179])).
% 0.22/0.76 fof(f460,plain,(
% 0.22/0.76 $false),
% 0.22/0.76 inference(backward_subsumption_resolution,[status(thm)],[f181,f459])).
% 0.22/0.76 % SZS output end CNFRefutation for theBenchmark.p
% 0.22/0.79 % Elapsed time: 0.116539 seconds
% 0.22/0.79 % CPU time: 0.685598 seconds
% 0.22/0.79 % Total memory used: 87.493 MB
% 0.22/0.79 % Net memory used: 86.750 MB
%------------------------------------------------------------------------------