%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HEN009-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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 12:45:29 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HEN009-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n026.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sun Sep 20 20:49:08 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.36 % Drodi V4.1.1
% 0.13/0.42 % Refutation found
% 0.13/0.42 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.42 fof(f2,axiom,(
% 0.13/0.42 (![X,Y]: (( ~ quotient(X,Y,zero)| less_equal(X,Y) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f6,axiom,(
% 0.13/0.42 (![X,Y]: (( ~ less_equal(X,Y)| ~ less_equal(Y,X)| X = Y ) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f8,axiom,(
% 0.13/0.42 (![X,Y]: (quotient(X,Y,divide(X,Y)) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f12,axiom,(
% 0.13/0.42 (![X]: (quotient(X,X,zero) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f14,axiom,(
% 0.13/0.42 (![X,Y,Z]: (( ~ less_equal(X,Y)| ~ less_equal(Y,Z)| less_equal(X,Z) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f15,axiom,(
% 0.13/0.42 (![X,Y,W1,Z,W2]: (( ~ quotient(X,Y,W1)| ~ less_equal(W1,Z)| ~ quotient(X,Z,W2)| less_equal(W2,Y) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f18,hypothesis,(
% 0.13/0.42 quotient(identity,a,idQa) ),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f19,hypothesis,(
% 0.13/0.42 quotient(identity,idQa,idQ_idQa) ),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f20,hypothesis,(
% 0.13/0.42 quotient(identity,idQ_idQa,idQ__idQ_idQa) ),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f21,negated_conjecture,(
% 0.13/0.42 idQa != idQ__idQ_idQa ),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f23,plain,(
% 0.13/0.42 ![X0,X1]: (~quotient(X0,X1,zero)|less_equal(X0,X1))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.42 fof(f29,plain,(
% 0.13/0.42 ![X0,X1]: (~less_equal(X0,X1)|~less_equal(X1,X0)|X0=X1)),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.42 fof(f31,plain,(
% 0.13/0.42 ![X0,X1]: (quotient(X0,X1,divide(X0,X1)))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f8])).
% 0.13/0.42 fof(f36,plain,(
% 0.13/0.42 ![X0]: (quotient(X0,X0,zero))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f12])).
% 0.13/0.42 fof(f38,plain,(
% 0.13/0.42 ![X,Z]: ((![Y]: (~less_equal(X,Y)|~less_equal(Y,Z)))|less_equal(X,Z))),
% 0.13/0.42 inference(miniscoping,[status(thm)],[f14])).
% 0.13/0.42 fof(f39,plain,(
% 0.13/0.42 ![X0,X1,X2]: (~less_equal(X0,X1)|~less_equal(X1,X2)|less_equal(X0,X2))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f38])).
% 0.13/0.42 fof(f40,plain,(
% 0.13/0.42 ![Y,W2]: ((![X,Z]: ((![W1]: (~quotient(X,Y,W1)|~less_equal(W1,Z)))|~quotient(X,Z,W2)))|less_equal(W2,Y))),
% 0.13/0.42 inference(miniscoping,[status(thm)],[f15])).
% 0.13/0.42 fof(f41,plain,(
% 0.13/0.42 ![X0,X1,X2,X3,X4]: (~quotient(X0,X1,X2)|~less_equal(X2,X3)|~quotient(X0,X3,X4)|less_equal(X4,X1))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f40])).
% 0.13/0.42 fof(f46,plain,(
% 0.13/0.42 quotient(identity,a,idQa)),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f18])).
% 0.13/0.42 fof(f47,plain,(
% 0.13/0.42 quotient(identity,idQa,idQ_idQa)),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f19])).
% 0.13/0.42 fof(f48,plain,(
% 0.13/0.42 quotient(identity,idQ_idQa,idQ__idQ_idQa)),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f20])).
% 0.13/0.42 fof(f49,plain,(
% 0.13/0.42 ~idQa=idQ__idQ_idQa),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f21])).
% 0.13/0.42 fof(f53,plain,(
% 0.13/0.42 ![X0]: (less_equal(X0,X0))),
% 0.13/0.42 inference(resolution,[status(thm)],[f23,f36])).
% 0.13/0.42 fof(f126,plain,(
% 0.13/0.42 ![X0,X1]: (~less_equal(idQ_idQa,X0)|~quotient(identity,X0,X1)|less_equal(X1,idQa))),
% 0.13/0.42 inference(resolution,[status(thm)],[f41,f47])).
% 0.13/0.42 fof(f127,plain,(
% 0.13/0.42 ![X0,X1]: (~less_equal(idQa,X0)|~quotient(identity,X0,X1)|less_equal(X1,a))),
% 0.13/0.42 inference(resolution,[status(thm)],[f41,f46])).
% 0.13/0.42 fof(f128,plain,(
% 0.13/0.42 ![X0,X1]: (~less_equal(idQ__idQ_idQa,X0)|~quotient(identity,X0,X1)|less_equal(X1,idQ_idQa))),
% 0.13/0.42 inference(resolution,[status(thm)],[f41,f48])).
% 0.13/0.42 fof(f131,plain,(
% 0.13/0.42 ![X0,X1,X2,X3]: (~less_equal(divide(X0,X1),X2)|~quotient(X0,X2,X3)|less_equal(X3,X1))),
% 0.13/0.42 inference(resolution,[status(thm)],[f41,f31])).
% 0.13/0.42 fof(f143,plain,(
% 0.13/0.42 ![X0]: (~less_equal(idQ__idQ_idQa,X0)|less_equal(divide(identity,X0),idQ_idQa))),
% 0.13/0.42 inference(resolution,[status(thm)],[f128,f31])).
% 0.13/0.42 fof(f148,plain,(
% 0.13/0.42 less_equal(divide(identity,idQ__idQ_idQa),idQ_idQa)),
% 0.13/0.42 inference(resolution,[status(thm)],[f143,f53])).
% 0.13/0.42 fof(f210,plain,(
% 0.13/0.42 ![X0]: (~less_equal(idQ_idQa,X0)|less_equal(divide(identity,idQ__idQ_idQa),X0))),
% 0.13/0.42 inference(resolution,[status(thm)],[f148,f39])).
% 0.13/0.42 fof(f583,plain,(
% 0.13/0.42 ~less_equal(idQ_idQa,idQ_idQa)|less_equal(idQ__idQ_idQa,idQa)),
% 0.13/0.42 inference(resolution,[status(thm)],[f126,f48])).
% 0.13/0.42 fof(f588,plain,(
% 0.13/0.42 less_equal(idQ__idQ_idQa,idQa)),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f583,f53])).
% 0.13/0.42 fof(f589,plain,(
% 0.13/0.42 ~less_equal(idQa,idQa)|less_equal(idQ_idQa,a)),
% 0.13/0.42 inference(resolution,[status(thm)],[f127,f47])).
% 0.13/0.42 fof(f596,plain,(
% 0.13/0.42 less_equal(idQ_idQa,a)),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f589,f53])).
% 0.13/0.42 fof(f615,plain,(
% 0.13/0.42 ~less_equal(idQa,idQ__idQ_idQa)|idQ__idQ_idQa=idQa),
% 0.13/0.42 inference(resolution,[status(thm)],[f588,f29])).
% 0.13/0.42 fof(f618,plain,(
% 0.13/0.42 ~less_equal(idQa,idQ__idQ_idQa)),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f615,f49])).
% 0.13/0.42 fof(f655,plain,(
% 0.13/0.42 less_equal(divide(identity,idQ__idQ_idQa),a)),
% 0.13/0.42 inference(resolution,[status(thm)],[f596,f210])).
% 0.13/0.42 fof(f710,plain,(
% 0.13/0.42 ![X0]: (~quotient(identity,a,X0)|less_equal(X0,idQ__idQ_idQa))),
% 0.13/0.42 inference(resolution,[status(thm)],[f131,f655])).
% 0.13/0.42 fof(f903,plain,(
% 0.13/0.42 less_equal(idQa,idQ__idQ_idQa)),
% 0.13/0.42 inference(resolution,[status(thm)],[f710,f46])).
% 0.13/0.42 fof(f905,plain,(
% 0.13/0.42 $false),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f903,f618])).
% 0.13/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.44 % Elapsed time: 0.083968 seconds
% 0.13/0.44 % CPU time: 0.459039 seconds
% 0.13/0.44 % Total memory used: 44.059 MB
% 0.13/0.44 % Net memory used: 43.075 MB
%------------------------------------------------------------------------------