%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT078+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 : n009.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:54 PM UTC 2026
% Result : Theorem 0.14s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT078+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n009.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 01:24:43 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.14/0.40 % Refutation found
% 0.14/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.40 fof(f4,axiom,(
% 0.14/0.40 (! [X,Y] :( leq(X,Y)<=> ( less(X,Y)| X = Y ) ) )),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f5,axiom,(
% 0.14/0.40 (! [X,Y] :( ( leq(X,Y)& leq(Y,X) )=> X = Y ) )),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f9,axiom,(
% 0.14/0.40 (! [X,Y,Z] :( ( leq(X,Y)& leq(Y,Z) )=> leq(X,Z) ) )),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f11,axiom,(
% 0.14/0.40 (! [X,A,B] :( in_lopen(X,A,B)<=> ( less(A,X)& leq(X,B) ) ) )),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f54,axiom,(
% 0.14/0.40 less(v600,v1200) ),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f56,axiom,(
% 0.14/0.40 ( v0 != v8& v0 != v32& v0 != v200& v0 != v600& v0 != v800& v0 != v1200& v8 != v32& v8 != v200& v8 != v600& v8 != v800& v8 != v1200& v32 != v200& v32 != v600& v32 != v800& v32 != v1200& v200 != v600& v200 != v800& v200 != v1200& v600 != v800& v600 != v1200& v800 != v1200 ) ),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f57,conjecture,(
% 0.14/0.40 ~ (? [X,Y,Z] :( in_lopen(X,v0,v600)& leq(v1200,X)& in_lopen(Y,v0,v800)& leq(v200,Y)& in_lopen(Z,v0,v32)& leq(v8,Z) ) )),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f58,negated_conjecture,(
% 0.14/0.40 ~(~ (? [X,Y,Z] :( in_lopen(X,v0,v600)& leq(v1200,X)& in_lopen(Y,v0,v800)& leq(v200,Y)& in_lopen(Z,v0,v32)& leq(v8,Z) ) ))),
% 0.14/0.40 inference(negated_conjecture,[status(cth)],[f57])).
% 0.14/0.40 fof(f64,plain,(
% 0.14/0.40 ![X,Y]: ((~leq(X,Y)|(less(X,Y)|X=Y))&(leq(X,Y)|(~less(X,Y)&~X=Y)))),
% 0.14/0.40 inference(NNF_transformation,[status(thm)],[f4])).
% 0.14/0.40 fof(f65,plain,(
% 0.14/0.40 (![X,Y]: (~leq(X,Y)|(less(X,Y)|X=Y)))&(![X,Y]: (leq(X,Y)|(~less(X,Y)&~X=Y)))),
% 0.14/0.40 inference(miniscoping,[status(thm)],[f64])).
% 0.14/0.40 fof(f67,plain,(
% 0.14/0.40 ![X0,X1]: (leq(X0,X1)|~less(X0,X1))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f65])).
% 0.14/0.40 fof(f69,plain,(
% 0.14/0.40 ![X,Y]: ((~leq(X,Y)|~leq(Y,X))|X=Y)),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.14/0.40 fof(f70,plain,(
% 0.14/0.40 ![X0,X1]: (~leq(X0,X1)|~leq(X1,X0)|X0=X1)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f69])).
% 0.14/0.40 fof(f79,plain,(
% 0.14/0.40 ![X,Y,Z]: ((~leq(X,Y)|~leq(Y,Z))|leq(X,Z))),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.14/0.40 fof(f80,plain,(
% 0.14/0.40 ![X,Z]: ((![Y]: (~leq(X,Y)|~leq(Y,Z)))|leq(X,Z))),
% 0.14/0.40 inference(miniscoping,[status(thm)],[f79])).
% 0.14/0.40 fof(f81,plain,(
% 0.14/0.40 ![X0,X1,X2]: (~leq(X0,X1)|~leq(X1,X2)|leq(X0,X2))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f80])).
% 0.14/0.40 fof(f87,plain,(
% 0.14/0.40 ![X,A,B]: ((~in_lopen(X,A,B)|(less(A,X)&leq(X,B)))&(in_lopen(X,A,B)|(~less(A,X)|~leq(X,B))))),
% 0.14/0.40 inference(NNF_transformation,[status(thm)],[f11])).
% 0.14/0.40 fof(f88,plain,(
% 0.14/0.40 (![X,A,B]: (~in_lopen(X,A,B)|(less(A,X)&leq(X,B))))&(![X,A,B]: (in_lopen(X,A,B)|(~less(A,X)|~leq(X,B))))),
% 0.14/0.40 inference(miniscoping,[status(thm)],[f87])).
% 0.14/0.40 fof(f90,plain,(
% 0.14/0.40 ![X0,X1,X2]: (~in_lopen(X0,X1,X2)|leq(X0,X2))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f88])).
% 0.14/0.40 fof(f166,plain,(
% 0.14/0.40 less(v600,v1200)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f54])).
% 0.14/0.40 fof(f187,plain,(
% 0.14/0.40 ~v600=v1200),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f56])).
% 0.14/0.40 fof(f189,plain,(
% 0.14/0.40 ?[Z]: (((?[Y]: (((?[X]: (in_lopen(X,v0,v600)&leq(v1200,X)))&in_lopen(Y,v0,v800))&leq(v200,Y)))&in_lopen(Z,v0,v32))&leq(v8,Z))),
% 0.14/0.40 inference(miniscoping,[status(thm)],[f58])).
% 0.14/0.40 fof(f190,plain,(
% 0.14/0.40 (((((in_lopen(sK5_skl,v0,v600)&leq(v1200,sK5_skl))&in_lopen(sK4_skl,v0,v800))&leq(v200,sK4_skl))&in_lopen(sK3_skl,v0,v32))&leq(v8,sK3_skl))),
% 0.14/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl]),skolemize(Z,sK3_skl),skolemize(Y,sK4_skl),skolemize(X,sK5_skl)],[f189])).
% 0.14/0.40 fof(f191,plain,(
% 0.14/0.40 in_lopen(sK5_skl,v0,v600)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f190])).
% 0.14/0.40 fof(f192,plain,(
% 0.14/0.40 leq(v1200,sK5_skl)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f190])).
% 0.14/0.40 fof(f223,plain,(
% 0.14/0.40 ~leq(sK5_skl,v1200)|sK5_skl=v1200),
% 0.14/0.40 inference(resolution,[status(thm)],[f70,f192])).
% 0.14/0.40 fof(f240,plain,(
% 0.14/0.40 ![X0]: (~leq(sK5_skl,X0)|~leq(X0,v1200)|sK5_skl=v1200)),
% 0.14/0.40 inference(resolution,[status(thm)],[f81,f223])).
% 0.14/0.40 fof(f310,plain,(
% 0.14/0.40 leq(sK5_skl,v600)),
% 0.14/0.40 inference(resolution,[status(thm)],[f90,f191])).
% 0.14/0.40 fof(f342,plain,(
% 0.14/0.40 leq(v600,v1200)),
% 0.14/0.40 inference(resolution,[status(thm)],[f166,f67])).
% 0.14/0.40 fof(f432,plain,(
% 0.14/0.40 ~leq(v600,v1200)|sK5_skl=v1200),
% 0.14/0.40 inference(resolution,[status(thm)],[f310,f240])).
% 0.14/0.40 fof(f435,plain,(
% 0.14/0.40 ~leq(v600,sK5_skl)|v600=sK5_skl),
% 0.14/0.40 inference(resolution,[status(thm)],[f310,f70])).
% 0.14/0.40 fof(f447,plain,(
% 0.14/0.40 ~v600=sK5_skl),
% 0.14/0.40 inference(backward_demodulation,[status(thm)],[f486,f187])).
% 0.14/0.40 fof(f466,plain,(
% 0.14/0.40 leq(v600,sK5_skl)),
% 0.14/0.40 inference(backward_demodulation,[status(thm)],[f486,f342])).
% 0.14/0.40 fof(f486,plain,(
% 0.14/0.40 sK5_skl=v1200),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f432,f342])).
% 0.14/0.40 fof(f487,plain,(
% 0.14/0.40 ~leq(v600,sK5_skl)),
% 0.14/0.40 inference(backward_subsumption_resolution,[status(thm)],[f435,f447])).
% 0.14/0.40 fof(f490,plain,(
% 0.14/0.40 $false),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f487,f466])).
% 0.14/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.43 % Elapsed time: 0.062693 seconds
% 0.14/0.43 % CPU time: 0.216171 seconds
% 0.14/0.43 % Total memory used: 83.847 MB
% 0.14/0.43 % Net memory used: 83.688 MB
%------------------------------------------------------------------------------