%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT073+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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:53 PM UTC 2026
% Result : Theorem 0.12s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT073+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n010.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:25:10 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 0.12/0.39 % Refutation found
% 0.12/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.39 fof(f4,axiom,(
% 0.12/0.39 (! [X,Y] :( leq(X,Y)<=> ( less(X,Y)| X = Y ) ) )),
% 0.12/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f7,axiom,(
% 0.12/0.39 (! [X,Y,Z] :( ( leq(X,Y)& less(Y,Z) )=> less(X,Z) ) )),
% 0.12/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f10,axiom,(
% 0.12/0.39 (! [X,A,B] :( in_closed(X,A,B)<=> ( leq(A,X)& leq(X,B) ) ) )),
% 0.12/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f37,hypothesis,(
% 0.12/0.39 less(n0,n5) ),
% 0.12/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f38,hypothesis,(
% 0.12/0.39 less(n5,n10) ),
% 0.12/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f40,conjecture,(
% 0.12/0.39 (? [X] :( in_closed(X,n0,n10)& in_closed(X,n5,n10) ) )),
% 0.12/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f41,negated_conjecture,(
% 0.12/0.39 ~((? [X] :( in_closed(X,n0,n10)& in_closed(X,n5,n10) ) ))),
% 0.12/0.39 inference(negated_conjecture,[status(cth)],[f40])).
% 0.12/0.39 fof(f47,plain,(
% 0.12/0.39 ![X,Y]: ((~leq(X,Y)|(less(X,Y)|X=Y))&(leq(X,Y)|(~less(X,Y)&~X=Y)))),
% 0.12/0.39 inference(NNF_transformation,[status(thm)],[f4])).
% 0.12/0.39 fof(f48,plain,(
% 0.12/0.39 (![X,Y]: (~leq(X,Y)|(less(X,Y)|X=Y)))&(![X,Y]: (leq(X,Y)|(~less(X,Y)&~X=Y)))),
% 0.12/0.39 inference(miniscoping,[status(thm)],[f47])).
% 0.12/0.39 fof(f50,plain,(
% 0.12/0.39 ![X0,X1]: (leq(X0,X1)|~less(X0,X1))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f48])).
% 0.12/0.39 fof(f51,plain,(
% 0.12/0.39 ![X0,X1]: (leq(X0,X1)|~X0=X1)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f48])).
% 0.12/0.39 fof(f56,plain,(
% 0.12/0.39 ![X,Y,Z]: ((~leq(X,Y)|~less(Y,Z))|less(X,Z))),
% 0.12/0.39 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f57,plain,(
% 0.12/0.39 ![X,Z]: ((![Y]: (~leq(X,Y)|~less(Y,Z)))|less(X,Z))),
% 0.12/0.39 inference(miniscoping,[status(thm)],[f56])).
% 0.12/0.39 fof(f58,plain,(
% 0.12/0.39 ![X0,X1,X2]: (~leq(X0,X1)|~less(X1,X2)|less(X0,X2))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f57])).
% 0.12/0.39 fof(f65,plain,(
% 0.12/0.39 ![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.12/0.39 inference(NNF_transformation,[status(thm)],[f10])).
% 0.12/0.39 fof(f66,plain,(
% 0.12/0.39 (![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.12/0.39 inference(miniscoping,[status(thm)],[f65])).
% 0.12/0.39 fof(f69,plain,(
% 0.12/0.39 ![X0,X1,X2]: (in_closed(X0,X1,X2)|~leq(X1,X0)|~leq(X0,X2))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f66])).
% 0.12/0.39 fof(f168,plain,(
% 0.12/0.39 less(n0,n5)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f37])).
% 0.12/0.39 fof(f169,plain,(
% 0.12/0.39 less(n5,n10)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f38])).
% 0.12/0.39 fof(f171,plain,(
% 0.12/0.39 (![X]: (~in_closed(X,n0,n10)|~in_closed(X,n5,n10)))),
% 0.12/0.39 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 0.12/0.39 fof(f172,plain,(
% 0.12/0.39 ![X0]: (~in_closed(X0,n0,n10)|~in_closed(X0,n5,n10))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f171])).
% 0.12/0.39 fof(f173,plain,(
% 0.12/0.39 ![X0]: (leq(X0,X0))),
% 0.12/0.39 inference(destructive_equality_resolution,[status(thm)],[f51])).
% 0.12/0.39 fof(f191,plain,(
% 0.12/0.39 leq(n5,n10)),
% 0.12/0.39 inference(resolution,[status(thm)],[f50,f169])).
% 0.12/0.39 fof(f192,plain,(
% 0.12/0.39 leq(n0,n5)),
% 0.12/0.39 inference(resolution,[status(thm)],[f50,f168])).
% 0.12/0.39 fof(f219,plain,(
% 0.12/0.39 ![X0]: (~less(n5,X0)|less(n0,X0))),
% 0.12/0.39 inference(resolution,[status(thm)],[f58,f192])).
% 0.12/0.39 fof(f234,plain,(
% 0.12/0.39 ![X0]: (~less(n5,X0)|leq(n0,X0))),
% 0.12/0.39 inference(resolution,[status(thm)],[f219,f50])).
% 0.12/0.39 fof(f242,plain,(
% 0.12/0.39 leq(n0,n10)),
% 0.12/0.39 inference(resolution,[status(thm)],[f234,f169])).
% 0.12/0.39 fof(f319,plain,(
% 0.12/0.39 ![X0]: (in_closed(n10,n0,X0)|~leq(n10,X0))),
% 0.12/0.39 inference(resolution,[status(thm)],[f69,f242])).
% 0.12/0.39 fof(f321,plain,(
% 0.12/0.39 ![X0]: (in_closed(n10,n5,X0)|~leq(n10,X0))),
% 0.12/0.39 inference(resolution,[status(thm)],[f69,f191])).
% 0.12/0.39 fof(f366,plain,(
% 0.12/0.39 in_closed(n10,n0,n10)),
% 0.12/0.39 inference(resolution,[status(thm)],[f319,f173])).
% 0.12/0.39 fof(f367,plain,(
% 0.12/0.39 ~in_closed(n10,n5,n10)),
% 0.12/0.39 inference(resolution,[status(thm)],[f366,f172])).
% 0.12/0.39 fof(f372,plain,(
% 0.12/0.39 in_closed(n10,n5,n10)),
% 0.12/0.39 inference(resolution,[status(thm)],[f321,f173])).
% 0.12/0.39 fof(f373,plain,(
% 0.12/0.39 $false),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f372,f367])).
% 0.12/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.42 % Elapsed time: 0.052155 seconds
% 0.12/0.42 % CPU time: 0.189685 seconds
% 0.12/0.42 % Total memory used: 83.145 MB
% 0.12/0.42 % Net memory used: 82.863 MB
%------------------------------------------------------------------------------