%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT088+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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.03s 0.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT088+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.55 % Computer : n005.cluster.edu
% 0.10/0.55 % Model : x86_64 x86_64
% 0.10/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.55 % Memory : 8046.5625MB
% 0.10/0.55 % OS : Linux 6.8.0-71-generic
% 0.10/0.56 % CPULimit : 300
% 0.03/0.56 % WCLimit : 300
% 0.03/0.56 % DateTime : Mon Sep 21 01:25:18 UTC 2026
% 0.03/0.56 % CPUTime :
% 0.03/0.57 % Drodi V4.1.1
% 0.03/0.59 % Refutation found
% 0.03/0.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.03/0.59 % SZS output start CNFRefutation for theBenchmark
% 0.03/0.59 fof(f4,axiom,(
% 0.03/0.59 (! [X,Y] :( leq(X,Y)<=> ( less(X,Y)| X = Y ) ) )),
% 0.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.59 fof(f12,axiom,(
% 0.03/0.59 (! [X,A,B] :( in_lopen(X,A,B)<=> ( less(A,X)& leq(X,B) ) ) )),
% 0.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.59 fof(f34,axiom,(
% 0.03/0.59 less(v0,v400) ),
% 0.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.59 fof(f36,axiom,(
% 0.03/0.59 less(v200,v400) ),
% 0.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.59 fof(f40,conjecture,(
% 0.03/0.59 (? [X] :( less(v200,X)& in_lopen(X,v0,v400) ) )),
% 0.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.59 fof(f41,negated_conjecture,(
% 0.03/0.59 ~((? [X] :( less(v200,X)& in_lopen(X,v0,v400) ) ))),
% 0.03/0.59 inference(negated_conjecture,[status(cth)],[f40])).
% 0.03/0.59 fof(f47,plain,(
% 0.03/0.59 ![X,Y]: ((~leq(X,Y)|(less(X,Y)|X=Y))&(leq(X,Y)|(~less(X,Y)&~X=Y)))),
% 0.03/0.59 inference(NNF_transformation,[status(thm)],[f4])).
% 0.03/0.59 fof(f48,plain,(
% 0.03/0.59 (![X,Y]: (~leq(X,Y)|(less(X,Y)|X=Y)))&(![X,Y]: (leq(X,Y)|(~less(X,Y)&~X=Y)))),
% 0.03/0.59 inference(miniscoping,[status(thm)],[f47])).
% 0.03/0.59 fof(f51,plain,(
% 0.03/0.59 ![X0,X1]: (leq(X0,X1)|~X0=X1)),
% 0.03/0.59 inference(cnf_transformation,[status(thm)],[f48])).
% 0.03/0.59 fof(f74,plain,(
% 0.03/0.59 ![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.03/0.59 inference(NNF_transformation,[status(thm)],[f12])).
% 0.03/0.59 fof(f75,plain,(
% 0.03/0.59 (![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.03/0.59 inference(miniscoping,[status(thm)],[f74])).
% 0.03/0.59 fof(f78,plain,(
% 0.03/0.59 ![X0,X1,X2]: (in_lopen(X0,X1,X2)|~less(X1,X0)|~leq(X0,X2))),
% 0.03/0.59 inference(cnf_transformation,[status(thm)],[f75])).
% 0.03/0.59 fof(f132,plain,(
% 0.03/0.59 less(v0,v400)),
% 0.03/0.59 inference(cnf_transformation,[status(thm)],[f34])).
% 0.03/0.59 fof(f134,plain,(
% 0.03/0.59 less(v200,v400)),
% 0.03/0.59 inference(cnf_transformation,[status(thm)],[f36])).
% 0.03/0.59 fof(f143,plain,(
% 0.03/0.59 (![X]: (~less(v200,X)|~in_lopen(X,v0,v400)))),
% 0.03/0.59 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 0.03/0.59 fof(f144,plain,(
% 0.03/0.59 ![X0]: (~less(v200,X0)|~in_lopen(X0,v0,v400))),
% 0.03/0.59 inference(cnf_transformation,[status(thm)],[f143])).
% 0.03/0.59 fof(f145,plain,(
% 0.03/0.59 ![X0]: (leq(X0,X0))),
% 0.03/0.59 inference(destructive_equality_resolution,[status(thm)],[f51])).
% 0.03/0.59 fof(f159,plain,(
% 0.03/0.59 ~in_lopen(v400,v0,v400)),
% 0.03/0.59 inference(resolution,[status(thm)],[f134,f144])).
% 0.03/0.59 fof(f174,plain,(
% 0.03/0.59 ![X0,X1]: (in_lopen(X0,X1,X0)|~less(X1,X0))),
% 0.03/0.59 inference(resolution,[status(thm)],[f145,f78])).
% 0.03/0.59 fof(f200,plain,(
% 0.03/0.59 ~less(v0,v400)),
% 0.03/0.59 inference(resolution,[status(thm)],[f174,f159])).
% 0.03/0.59 fof(f204,plain,(
% 0.03/0.59 $false),
% 0.03/0.59 inference(forward_subsumption_resolution,[status(thm)],[f200,f132])).
% 0.03/0.59 % SZS output end CNFRefutation for theBenchmark.p
% 0.03/0.61 % Elapsed time: 0.047713 seconds
% 0.03/0.61 % CPU time: 0.144697 seconds
% 0.03/0.61 % Total memory used: 66.497 MB
% 0.03/0.61 % Net memory used: 66.416 MB
%------------------------------------------------------------------------------