%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HEN011-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:30 PM UTC 2026
% Result : Unsatisfiable 51.80s 7.00s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HEN011-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n004.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 : Sun Sep 20 20:46:35 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 51.80/7.00 % Refutation found
% 51.80/7.00 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 51.80/7.00 % SZS output start CNFRefutation for theBenchmark
% 51.80/7.00 fof(f2,axiom,(
% 51.80/7.00 (![X,Y]: (( ~ quotient(X,Y,zero)| less_equal(X,Y) ) ))),
% 51.80/7.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.80/7.00 fof(f3,axiom,(
% 51.80/7.00 (![X,Y,Z]: (( ~ quotient(X,Y,Z)| less_equal(Z,X) ) ))),
% 51.80/7.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.80/7.00 fof(f4,axiom,(
% 51.80/7.00 (![X,Y,V1,Z,V2,V3,V4,V5]: (( ~ quotient(X,Y,V1)| ~ quotient(Y,Z,V2)| ~ quotient(X,Z,V3)| ~ quotient(V3,V2,V4)| ~ quotient(V1,Z,V5)| less_equal(V4,V5) ) ))),
% 51.80/7.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.80/7.00 fof(f6,axiom,(
% 51.80/7.00 (![X,Y]: (( ~ less_equal(X,Y)| ~ less_equal(Y,X)| X = Y ) ))),
% 51.80/7.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.80/7.00 fof(f7,axiom,(
% 51.80/7.00 (![X]: (less_equal(X,identity) ))),
% 51.80/7.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.80/7.00 fof(f8,axiom,(
% 51.80/7.00 (![X,Y]: (quotient(X,Y,divide(X,Y)) ))),
% 51.80/7.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.80/7.00 fof(f9,axiom,(
% 51.80/7.00 (![X,Y,Z,W]: (( ~ quotient(X,Y,Z)| ~ quotient(X,Y,W)| Z = W ) ))),
% 51.80/7.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.80/7.00 fof(f12,axiom,(
% 51.80/7.00 (![X]: (quotient(X,X,zero) ))),
% 51.80/7.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.80/7.00 fof(f15,axiom,(
% 51.80/7.00 (![X,Y,W1,Z,W2]: (( ~ quotient(X,Y,W1)| ~ less_equal(W1,Z)| ~ quotient(X,Z,W2)| less_equal(W2,Y) ) ))),
% 51.80/7.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.80/7.00 fof(f16,axiom,(
% 51.80/7.00 (![X,Y,Z,W1,W2]: (( ~ less_equal(X,Y)| ~ quotient(Z,Y,W1)| ~ quotient(Z,X,W2)| less_equal(W1,W2) ) ))),
% 51.80/7.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.80/7.00 fof(f17,axiom,(
% 51.80/7.00 (![X,Y,Z,W1,W2]: (( ~ less_equal(X,Y)| ~ quotient(X,Z,W1)| ~ quotient(Y,Z,W2)| less_equal(W1,W2) ) ))),
% 51.80/7.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.80/7.00 fof(f18,axiom,(
% 51.80/7.00 (![X,Y1,Y2,Y3]: (( ~ quotient(identity,X,Y1)| ~ quotient(identity,Y1,Y2)| ~ quotient(identity,Y2,Y3)| Y1 = Y3 ) ))),
% 51.80/7.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.80/7.00 fof(f19,axiom,(
% 51.80/7.00 (![X,Y1,Y2,Y3]: (( ~ quotient(identity,X,Y1)| ~ quotient(identity,Y1,Y2)| ~ quotient(Y1,Y2,Y3)| Y1 = Y3 ) ))),
% 51.80/7.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.80/7.00 fof(f20,hypothesis,(
% 51.80/7.00 quotient(identity,a,idQa) ),
% 51.80/7.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.80/7.00 fof(f21,hypothesis,(
% 51.80/7.00 quotient(identity,b,idQb) ),
% 51.80/7.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.80/7.00 fof(f22,hypothesis,(
% 51.80/7.00 quotient(identity,idQb,idQ_idQb) ),
% 51.80/7.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.80/7.00 fof(f23,hypothesis,(
% 51.80/7.00 quotient(idQa,idQ_idQb,idQa_Q__idQ_idQb) ),
% 51.80/7.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.80/7.00 fof(f24,hypothesis,(
% 51.80/7.00 quotient(identity,idQa,idQ_idQa) ),
% 51.80/7.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.80/7.00 fof(f25,hypothesis,(
% 51.80/7.00 quotient(idQb,idQ_idQa,idQb_Q__idQ_idQa) ),
% 51.80/7.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.80/7.00 fof(f26,negated_conjecture,(
% 51.80/7.00 idQa_Q__idQ_idQb != idQb_Q__idQ_idQa ),
% 51.80/7.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 51.80/7.00 fof(f28,plain,(
% 51.80/7.00 ![X0,X1]: (~quotient(X0,X1,zero)|less_equal(X0,X1))),
% 51.80/7.00 inference(cnf_transformation,[status(thm)],[f2])).
% 51.80/7.00 fof(f29,plain,(
% 51.80/7.00 ![X,Z]: ((![Y]: ~quotient(X,Y,Z))|less_equal(Z,X))),
% 51.80/7.00 inference(miniscoping,[status(thm)],[f3])).
% 51.80/7.00 fof(f30,plain,(
% 51.80/7.00 ![X0,X1,X2]: (~quotient(X0,X1,X2)|less_equal(X2,X0))),
% 51.80/7.00 inference(cnf_transformation,[status(thm)],[f29])).
% 51.80/7.00 fof(f31,plain,(
% 51.80/7.00 ![V4,V5]: ((![V1,Z]: ((![V2,V3]: ((![X]: ((![Y]: (~quotient(X,Y,V1)|~quotient(Y,Z,V2)))|~quotient(X,Z,V3)))|~quotient(V3,V2,V4)))|~quotient(V1,Z,V5)))|less_equal(V4,V5))),
% 51.80/7.00 inference(miniscoping,[status(thm)],[f4])).
% 51.80/7.00 fof(f32,plain,(
% 51.80/7.00 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~quotient(X0,X1,X2)|~quotient(X1,X3,X4)|~quotient(X0,X3,X5)|~quotient(X5,X4,X6)|~quotient(X2,X3,X7)|less_equal(X6,X7))),
% 51.80/7.00 inference(cnf_transformation,[status(thm)],[f31])).
% 51.80/7.00 fof(f34,plain,(
% 51.80/7.00 ![X0,X1]: (~less_equal(X0,X1)|~less_equal(X1,X0)|X0=X1)),
% 51.80/7.00 inference(cnf_transformation,[status(thm)],[f6])).
% 51.80/7.00 fof(f35,plain,(
% 51.80/7.00 ![X0]: (less_equal(X0,identity))),
% 51.80/7.00 inference(cnf_transformation,[status(thm)],[f7])).
% 51.80/7.00 fof(f36,plain,(
% 51.80/7.00 ![X0,X1]: (quotient(X0,X1,divide(X0,X1)))),
% 51.80/7.00 inference(cnf_transformation,[status(thm)],[f8])).
% 51.80/7.00 fof(f37,plain,(
% 51.80/7.00 ![Z,W]: ((![X,Y]: (~quotient(X,Y,Z)|~quotient(X,Y,W)))|Z=W)),
% 51.80/7.00 inference(miniscoping,[status(thm)],[f9])).
% 51.80/7.00 fof(f38,plain,(
% 51.80/7.00 ![X0,X1,X2,X3]: (~quotient(X0,X1,X2)|~quotient(X0,X1,X3)|X2=X3)),
% 51.80/7.00 inference(cnf_transformation,[status(thm)],[f37])).
% 51.80/7.00 fof(f41,plain,(
% 51.80/7.00 ![X0]: (quotient(X0,X0,zero))),
% 51.80/7.00 inference(cnf_transformation,[status(thm)],[f12])).
% 51.80/7.00 fof(f45,plain,(
% 51.80/7.00 ![Y,W2]: ((![X,Z]: ((![W1]: (~quotient(X,Y,W1)|~less_equal(W1,Z)))|~quotient(X,Z,W2)))|less_equal(W2,Y))),
% 51.80/7.00 inference(miniscoping,[status(thm)],[f15])).
% 51.80/7.00 fof(f46,plain,(
% 51.80/7.00 ![X0,X1,X2,X3,X4]: (~quotient(X0,X1,X2)|~less_equal(X2,X3)|~quotient(X0,X3,X4)|less_equal(X4,X1))),
% 51.80/7.00 inference(cnf_transformation,[status(thm)],[f45])).
% 51.80/7.00 fof(f47,plain,(
% 51.80/7.00 ![W1,W2]: ((![X,Z]: ((![Y]: (~less_equal(X,Y)|~quotient(Z,Y,W1)))|~quotient(Z,X,W2)))|less_equal(W1,W2))),
% 51.80/7.00 inference(miniscoping,[status(thm)],[f16])).
% 51.80/7.00 fof(f48,plain,(
% 51.80/7.00 ![X0,X1,X2,X3,X4]: (~less_equal(X0,X1)|~quotient(X2,X1,X3)|~quotient(X2,X0,X4)|less_equal(X3,X4))),
% 51.80/7.00 inference(cnf_transformation,[status(thm)],[f47])).
% 51.80/7.00 fof(f49,plain,(
% 51.80/7.00 ![W1,W2]: ((![Y,Z]: ((![X]: (~less_equal(X,Y)|~quotient(X,Z,W1)))|~quotient(Y,Z,W2)))|less_equal(W1,W2))),
% 51.80/7.00 inference(miniscoping,[status(thm)],[f17])).
% 51.80/7.00 fof(f50,plain,(
% 51.80/7.00 ![X0,X1,X2,X3,X4]: (~less_equal(X0,X1)|~quotient(X0,X2,X3)|~quotient(X1,X2,X4)|less_equal(X3,X4))),
% 51.80/7.00 inference(cnf_transformation,[status(thm)],[f49])).
% 51.80/7.00 fof(f51,plain,(
% 51.80/7.00 ![Y1,Y3]: ((![Y2]: (((![X]: ~quotient(identity,X,Y1))|~quotient(identity,Y1,Y2))|~quotient(identity,Y2,Y3)))|Y1=Y3)),
% 51.80/7.00 inference(miniscoping,[status(thm)],[f18])).
% 51.80/7.00 fof(f52,plain,(
% 51.80/7.00 ![X0,X1,X2,X3]: (~quotient(identity,X0,X1)|~quotient(identity,X1,X2)|~quotient(identity,X2,X3)|X1=X3)),
% 51.80/7.00 inference(cnf_transformation,[status(thm)],[f51])).
% 51.80/7.00 fof(f53,plain,(
% 51.80/7.00 ![Y1,Y3]: ((![Y2]: (((![X]: ~quotient(identity,X,Y1))|~quotient(identity,Y1,Y2))|~quotient(Y1,Y2,Y3)))|Y1=Y3)),
% 51.80/7.00 inference(miniscoping,[status(thm)],[f19])).
% 51.80/7.00 fof(f54,plain,(
% 51.80/7.00 ![X0,X1,X2,X3]: (~quotient(identity,X0,X1)|~quotient(identity,X1,X2)|~quotient(X1,X2,X3)|X1=X3)),
% 51.80/7.00 inference(cnf_transformation,[status(thm)],[f53])).
% 51.80/7.00 fof(f55,plain,(
% 51.80/7.00 quotient(identity,a,idQa)),
% 51.80/7.00 inference(cnf_transformation,[status(thm)],[f20])).
% 51.80/7.00 fof(f56,plain,(
% 51.80/7.00 quotient(identity,b,idQb)),
% 51.80/7.00 inference(cnf_transformation,[status(thm)],[f21])).
% 51.80/7.00 fof(f57,plain,(
% 51.80/7.00 quotient(identity,idQb,idQ_idQb)),
% 51.80/7.00 inference(cnf_transformation,[status(thm)],[f22])).
% 51.80/7.00 fof(f58,plain,(
% 51.80/7.00 quotient(idQa,idQ_idQb,idQa_Q__idQ_idQb)),
% 51.80/7.00 inference(cnf_transformation,[status(thm)],[f23])).
% 51.80/7.00 fof(f59,plain,(
% 51.80/7.00 quotient(identity,idQa,idQ_idQa)),
% 51.80/7.00 inference(cnf_transformation,[status(thm)],[f24])).
% 51.80/7.00 fof(f60,plain,(
% 51.80/7.00 quotient(idQb,idQ_idQa,idQb_Q__idQ_idQa)),
% 51.80/7.00 inference(cnf_transformation,[status(thm)],[f25])).
% 51.80/7.00 fof(f61,plain,(
% 51.80/7.00 ~idQa_Q__idQ_idQb=idQb_Q__idQ_idQa),
% 51.80/7.00 inference(cnf_transformation,[status(thm)],[f26])).
% 51.80/7.00 fof(f65,plain,(
% 51.80/7.00 ![X0]: (less_equal(X0,X0))),
% 51.80/7.00 inference(resolution,[status(thm)],[f28,f41])).
% 51.80/7.00 fof(f74,plain,(
% 51.80/7.00 ![X0,X1]: (less_equal(divide(X0,X1),X0))),
% 51.80/7.00 inference(resolution,[status(thm)],[f30,f36])).
% 51.80/7.00 fof(f77,plain,(
% 51.80/7.00 ![X0,X1,X2,X3,X4]: (~quotient(idQ_idQa,X0,X1)|~quotient(idQb,X0,X2)|~quotient(X2,X1,X3)|~quotient(idQb_Q__idQ_idQa,X0,X4)|less_equal(X3,X4))),
% 51.80/7.00 inference(resolution,[status(thm)],[f32,f60])).
% 51.80/7.00 fof(f78,plain,(
% 51.80/7.00 ![X0,X1,X2,X3,X4]: (~quotient(idQ_idQb,X0,X1)|~quotient(idQa,X0,X2)|~quotient(X2,X1,X3)|~quotient(idQa_Q__idQ_idQb,X0,X4)|less_equal(X3,X4))),
% 51.80/7.00 inference(resolution,[status(thm)],[f32,f58])).
% 51.80/7.00 fof(f92,plain,(
% 51.80/7.00 ![X0,X1,X2,X3]: (~quotient(idQb,X0,X1)|~quotient(X1,divide(idQ_idQa,X0),X2)|~quotient(idQb_Q__idQ_idQa,X0,X3)|less_equal(X2,X3))),
% 51.80/7.00 inference(resolution,[status(thm)],[f77,f36])).
% 51.80/7.00 fof(f102,plain,(
% 51.80/7.00 ![X0,X1,X2,X3]: (~quotient(idQa,X0,X1)|~quotient(X1,divide(idQ_idQb,X0),X2)|~quotient(idQa_Q__idQ_idQb,X0,X3)|less_equal(X2,X3))),
% 51.80/7.00 inference(resolution,[status(thm)],[f78,f36])).
% 51.80/7.00 fof(f106,plain,(
% 51.80/7.00 ![X0,X1]: (~less_equal(X0,divide(X0,X1))|divide(X0,X1)=X0)),
% 51.80/7.00 inference(resolution,[status(thm)],[f74,f34])).
% 51.80/7.00 fof(f126,plain,(
% 51.80/7.00 ![X0]: (~quotient(idQb,idQ_idQa,X0)|idQb_Q__idQ_idQa=X0)),
% 51.80/7.00 inference(resolution,[status(thm)],[f38,f60])).
% 51.80/7.00 fof(f127,plain,(
% 51.80/7.00 ![X0]: (~quotient(idQa,idQ_idQb,X0)|idQa_Q__idQ_idQb=X0)),
% 51.80/7.00 inference(resolution,[status(thm)],[f38,f58])).
% 51.80/7.00 fof(f145,plain,(
% 51.80/7.00 ![X0,X1]: (~less_equal(idQb_Q__idQ_idQa,X0)|~quotient(idQb,X0,X1)|less_equal(X1,idQ_idQa))),
% 51.80/7.00 inference(resolution,[status(thm)],[f46,f60])).
% 51.80/7.00 fof(f146,plain,(
% 51.80/7.00 ![X0,X1]: (~less_equal(idQa_Q__idQ_idQb,X0)|~quotient(idQa,X0,X1)|less_equal(X1,idQ_idQb))),
% 51.80/7.00 inference(resolution,[status(thm)],[f46,f58])).
% 51.80/7.00 fof(f149,plain,(
% 51.80/7.00 ![X0,X1,X2,X3]: (~less_equal(divide(X0,X1),X2)|~quotient(X0,X2,X3)|less_equal(X3,X1))),
% 51.80/7.00 inference(resolution,[status(thm)],[f46,f36])).
% 51.80/7.00 fof(f159,plain,(
% 51.80/7.00 idQb_Q__idQ_idQa=divide(idQb,idQ_idQa)),
% 51.80/7.00 inference(resolution,[status(thm)],[f126,f36])).
% 51.80/7.00 fof(f167,plain,(
% 51.80/7.00 idQa_Q__idQ_idQb=divide(idQa,idQ_idQb)),
% 51.80/7.00 inference(resolution,[status(thm)],[f127,f36])).
% 51.80/7.00 fof(f171,plain,(
% 51.80/7.00 ![X0]: (~less_equal(idQb_Q__idQ_idQa,X0)|less_equal(divide(idQb,X0),idQ_idQa))),
% 51.80/7.00 inference(resolution,[status(thm)],[f145,f36])).
% 51.80/7.00 fof(f176,plain,(
% 51.80/7.00 ![X0]: (~less_equal(idQa_Q__idQ_idQb,X0)|less_equal(divide(idQa,X0),idQ_idQb))),
% 51.80/7.00 inference(resolution,[status(thm)],[f146,f36])).
% 51.80/7.00 fof(f201,plain,(
% 51.80/7.00 ![X0,X1,X2,X3,X4]: (~quotient(X0,X1,X2)|~quotient(X0,divide(X1,X3),X4)|less_equal(X2,X4))),
% 51.80/7.00 inference(resolution,[status(thm)],[f48,f74])).
% 51.80/7.00 fof(f211,plain,(
% 51.80/7.00 ![X0,X1,X2,X3]: (~quotient(X0,X1,X2)|~quotient(identity,X1,X3)|less_equal(X2,X3))),
% 51.80/7.00 inference(resolution,[status(thm)],[f50,f35])).
% 51.80/7.00 fof(f215,plain,(
% 51.80/7.00 ![X0,X1]: (~quotient(identity,idQb,X0)|~quotient(identity,X0,X1)|idQb=X1)),
% 51.80/7.00 inference(resolution,[status(thm)],[f52,f56])).
% 51.80/7.00 fof(f216,plain,(
% 51.80/7.00 ![X0,X1]: (~quotient(identity,idQa,X0)|~quotient(identity,X0,X1)|idQa=X1)),
% 51.80/7.00 inference(resolution,[status(thm)],[f52,f55])).
% 51.80/7.00 fof(f249,plain,(
% 51.80/7.00 ![X0,X1,X2]: (~quotient(idQb,X0,X1)|~quotient(idQb_Q__idQ_idQa,X0,X2)|less_equal(divide(X1,divide(idQ_idQa,X0)),X2))),
% 51.80/7.00 inference(resolution,[status(thm)],[f92,f36])).
% 51.80/7.00 fof(f301,plain,(
% 51.80/7.00 ![X0,X1]: (~quotient(identity,idQ_idQa,X0)|~quotient(idQ_idQa,X0,X1)|idQ_idQa=X1)),
% 51.80/7.00 inference(resolution,[status(thm)],[f54,f59])).
% 51.80/7.00 fof(f302,plain,(
% 51.80/7.00 ![X0,X1]: (~quotient(identity,idQ_idQb,X0)|~quotient(idQ_idQb,X0,X1)|idQ_idQb=X1)),
% 51.80/7.00 inference(resolution,[status(thm)],[f54,f57])).
% 51.80/7.00 fof(f303,plain,(
% 51.80/7.00 ![X0,X1]: (~quotient(identity,idQb,X0)|~quotient(idQb,X0,X1)|idQb=X1)),
% 51.80/7.00 inference(resolution,[status(thm)],[f54,f56])).
% 51.80/7.00 fof(f304,plain,(
% 51.80/7.00 ![X0,X1]: (~quotient(identity,idQa,X0)|~quotient(idQa,X0,X1)|idQa=X1)),
% 51.80/7.00 inference(resolution,[status(thm)],[f54,f55])).
% 51.80/7.00 fof(f365,plain,(
% 51.80/7.00 ![X0,X1,X2]: (~quotient(idQa,X0,X1)|~quotient(idQa_Q__idQ_idQb,X0,X2)|less_equal(divide(X1,divide(idQ_idQb,X0)),X2))),
% 51.80/7.00 inference(resolution,[status(thm)],[f102,f36])).
% 51.80/7.00 fof(f459,plain,(
% 51.80/7.00 less_equal(divide(idQb,idQb_Q__idQ_idQa),idQ_idQa)),
% 51.80/7.00 inference(resolution,[status(thm)],[f171,f65])).
% 51.80/7.00 fof(f463,plain,(
% 51.80/7.00 ![X0,X1,X2]: (~quotient(X0,idQ_idQa,X1)|~quotient(X0,divide(idQb,idQb_Q__idQ_idQa),X2)|less_equal(X1,X2))),
% 51.80/7.00 inference(resolution,[status(thm)],[f459,f48])).
% 51.80/7.00 fof(f469,plain,(
% 51.80/7.00 less_equal(divide(idQa,idQa_Q__idQ_idQb),idQ_idQb)),
% 51.80/7.00 inference(resolution,[status(thm)],[f176,f65])).
% 51.80/7.00 fof(f529,plain,(
% 51.80/7.00 ![X0,X1,X2]: (~quotient(X0,idQ_idQb,X1)|~quotient(X0,divide(idQa,idQa_Q__idQ_idQb),X2)|less_equal(X1,X2))),
% 51.80/7.00 inference(resolution,[status(thm)],[f469,f48])).
% 51.80/7.00 fof(f1223,plain,(
% 51.80/7.00 ![X0]: (~quotient(identity,idQ_idQa,X0)|less_equal(idQb_Q__idQ_idQa,X0))),
% 51.80/7.00 inference(resolution,[status(thm)],[f211,f60])).
% 51.80/7.00 fof(f1224,plain,(
% 51.80/7.00 ![X0]: (~quotient(identity,idQ_idQb,X0)|less_equal(idQa_Q__idQ_idQb,X0))),
% 51.80/7.00 inference(resolution,[status(thm)],[f211,f58])).
% 51.80/7.00 fof(f1230,plain,(
% 51.80/7.00 less_equal(idQb_Q__idQ_idQa,divide(identity,idQ_idQa))),
% 51.80/7.00 inference(resolution,[status(thm)],[f1223,f36])).
% 51.80/7.00 fof(f1233,plain,(
% 51.80/7.00 ![X0,X1,X2]: (~quotient(idQb_Q__idQ_idQa,X0,X1)|~quotient(divide(identity,idQ_idQa),X0,X2)|less_equal(X1,X2))),
% 51.80/7.00 inference(resolution,[status(thm)],[f1230,f50])).
% 51.80/7.00 fof(f1238,plain,(
% 51.80/7.00 less_equal(idQa_Q__idQ_idQb,divide(identity,idQ_idQb))),
% 51.80/7.00 inference(resolution,[status(thm)],[f1224,f36])).
% 51.80/7.00 fof(f1241,plain,(
% 51.80/7.00 ![X0,X1,X2]: (~quotient(idQa_Q__idQ_idQb,X0,X1)|~quotient(divide(identity,idQ_idQb),X0,X2)|less_equal(X1,X2))),
% 51.80/7.00 inference(resolution,[status(thm)],[f1238,f50])).
% 51.80/7.00 fof(f1329,plain,(
% 51.80/7.00 ![X0]: (~quotient(identity,idQ_idQb,X0)|idQb=X0)),
% 51.80/7.00 inference(resolution,[status(thm)],[f215,f57])).
% 51.80/7.00 fof(f1332,plain,(
% 51.80/7.00 ![X0]: (~quotient(identity,idQ_idQa,X0)|idQa=X0)),
% 51.80/7.00 inference(resolution,[status(thm)],[f216,f59])).
% 51.80/7.00 fof(f1409,plain,(
% 51.80/7.00 idQb=divide(identity,idQ_idQb)),
% 51.80/7.00 inference(resolution,[status(thm)],[f1329,f36])).
% 51.80/7.00 fof(f1423,plain,(
% 51.80/7.00 quotient(identity,idQ_idQb,idQb)),
% 51.80/7.00 inference(paramodulation,[status(thm)],[f1409,f36])).
% 51.80/7.00 fof(f1521,plain,(
% 51.80/7.00 ![X0,X1]: (~quotient(idQb_Q__idQ_idQa,X0,X1)|less_equal(divide(divide(idQb,X0),divide(idQ_idQa,X0)),X1))),
% 51.80/7.00 inference(resolution,[status(thm)],[f249,f36])).
% 51.80/7.00 fof(f1558,plain,(
% 51.80/7.00 idQa=divide(identity,idQ_idQa)),
% 51.80/7.00 inference(resolution,[status(thm)],[f1332,f36])).
% 51.80/7.00 fof(f1573,plain,(
% 51.80/7.00 quotient(identity,idQ_idQa,idQa)),
% 51.80/7.00 inference(paramodulation,[status(thm)],[f1558,f36])).
% 51.80/7.00 fof(f1624,plain,(
% 51.80/7.00 ![X0]: (~quotient(identity,idQ_idQa,X0)|idQ_idQa=divide(idQ_idQa,X0))),
% 51.80/7.00 inference(resolution,[status(thm)],[f301,f36])).
% 51.80/7.00 fof(f1630,plain,(
% 51.80/7.00 ![X0]: (~quotient(identity,idQ_idQb,X0)|idQ_idQb=divide(idQ_idQb,X0))),
% 51.80/7.00 inference(resolution,[status(thm)],[f302,f36])).
% 51.80/7.00 fof(f1691,plain,(
% 51.80/7.00 ![X0]: (~quotient(identity,idQb,X0)|idQb=divide(idQb,X0))),
% 51.80/7.00 inference(resolution,[status(thm)],[f303,f36])).
% 51.80/7.00 fof(f1696,plain,(
% 51.80/7.00 ![X0]: (~quotient(identity,idQa,X0)|idQa=divide(idQa,X0))),
% 51.80/7.00 inference(resolution,[status(thm)],[f304,f36])).
% 51.80/7.00 fof(f1826,plain,(
% 51.80/7.00 ![X0,X1,X2,X3]: (~quotient(X0,divide(X1,X2),X3)|less_equal(divide(X0,X1),X3))),
% 51.80/7.00 inference(resolution,[status(thm)],[f201,f36])).
% 51.80/7.00 fof(f2074,plain,(
% 51.80/7.00 ![X0,X1]: (~quotient(idQa_Q__idQ_idQb,X0,X1)|less_equal(divide(divide(idQa,X0),divide(idQ_idQb,X0)),X1))),
% 51.80/7.00 inference(resolution,[status(thm)],[f365,f36])).
% 51.80/7.00 fof(f4502,plain,(
% 51.80/7.00 ![X0,X1,X2]: (~quotient(idQb_Q__idQ_idQa,X0,X1)|~quotient(idQa,X0,X2)|less_equal(X1,X2))),
% 51.80/7.00 inference(forward_demodulation,[status(thm)],[f1558,f1233])).
% 51.80/7.00 fof(f4508,plain,(
% 51.80/7.00 ![X0,X1]: (~quotient(idQa,X0,X1)|less_equal(divide(idQb_Q__idQ_idQa,X0),X1))),
% 51.80/7.00 inference(resolution,[status(thm)],[f4502,f36])).
% 51.80/7.00 fof(f4708,plain,(
% 51.80/7.00 ![X0,X1,X2]: (~quotient(idQa_Q__idQ_idQb,X0,X1)|~quotient(idQb,X0,X2)|less_equal(X1,X2))),
% 51.80/7.00 inference(forward_demodulation,[status(thm)],[f1409,f1241])).
% 51.80/7.00 fof(f4714,plain,(
% 51.80/7.00 ![X0,X1]: (~quotient(idQb,X0,X1)|less_equal(divide(idQa_Q__idQ_idQb,X0),X1))),
% 51.80/7.00 inference(resolution,[status(thm)],[f4708,f36])).
% 51.80/7.00 fof(f5837,plain,(
% 51.80/7.00 ![X0]: (less_equal(divide(divide(idQb,X0),divide(idQ_idQa,X0)),divide(idQb_Q__idQ_idQa,X0)))),
% 51.80/7.00 inference(resolution,[status(thm)],[f1521,f36])).
% 51.80/7.00 fof(f6139,plain,(
% 51.80/7.00 ![X0]: (less_equal(divide(divide(idQa,X0),divide(idQ_idQb,X0)),divide(idQa_Q__idQ_idQb,X0)))),
% 51.80/7.00 inference(resolution,[status(thm)],[f2074,f36])).
% 51.80/7.00 fof(f7028,plain,(
% 51.80/7.00 idQ_idQa=divide(idQ_idQa,idQa)),
% 51.80/7.00 inference(resolution,[status(thm)],[f1624,f1573])).
% 51.80/7.00 fof(f7328,plain,(
% 51.80/7.00 idQ_idQb=divide(idQ_idQb,idQb)),
% 51.80/7.00 inference(resolution,[status(thm)],[f1630,f1423])).
% 51.80/7.00 fof(f7331,plain,(
% 51.80/7.00 idQb=divide(idQb,idQ_idQb)),
% 51.80/7.00 inference(resolution,[status(thm)],[f1691,f57])).
% 51.80/7.00 fof(f7334,plain,(
% 51.80/7.00 idQa=divide(idQa,idQ_idQa)),
% 51.80/7.00 inference(resolution,[status(thm)],[f1696,f59])).
% 51.80/7.00 fof(f7523,plain,(
% 51.80/7.00 quotient(idQb,idQ_idQb,idQb)),
% 51.80/7.00 inference(paramodulation,[status(thm)],[f7331,f36])).
% 51.80/7.00 fof(f7563,plain,(
% 51.80/7.00 quotient(idQa,idQ_idQa,idQa)),
% 51.80/7.00 inference(paramodulation,[status(thm)],[f7334,f36])).
% 51.80/7.00 fof(f7841,plain,(
% 51.80/7.00 ![X0]: (~quotient(idQb,divide(idQa,idQa_Q__idQ_idQb),X0)|less_equal(idQb,X0))),
% 51.80/7.00 inference(resolution,[status(thm)],[f7523,f529])).
% 51.80/7.00 fof(f7874,plain,(
% 51.80/7.00 ![X0]: (~quotient(idQa,divide(idQb,idQb_Q__idQ_idQa),X0)|less_equal(idQa,X0))),
% 51.80/7.00 inference(resolution,[status(thm)],[f7563,f463])).
% 51.80/7.00 fof(f9045,plain,(
% 51.80/7.00 ![X0,X1,X2]: (less_equal(divide(X0,X1),divide(X0,divide(X1,X2))))),
% 51.80/7.00 inference(resolution,[status(thm)],[f1826,f36])).
% 51.80/7.00 fof(f11508,plain,(
% 51.80/7.00 ![X0]: (less_equal(divide(idQb_Q__idQ_idQa,X0),divide(idQa,X0)))),
% 51.80/7.00 inference(resolution,[status(thm)],[f4508,f36])).
% 51.80/7.00 fof(f11522,plain,(
% 51.80/7.00 ![X0,X1]: (~quotient(idQb_Q__idQ_idQa,divide(idQa,X0),X1)|less_equal(X1,X0))),
% 51.80/7.00 inference(resolution,[status(thm)],[f11508,f149])).
% 51.80/7.00 fof(f12776,plain,(
% 51.80/7.00 ![X0]: (less_equal(divide(idQa_Q__idQ_idQb,X0),divide(idQb,X0)))),
% 51.80/7.00 inference(resolution,[status(thm)],[f4714,f36])).
% 51.80/7.00 fof(f12790,plain,(
% 51.80/7.00 ![X0,X1]: (~quotient(idQa_Q__idQ_idQb,divide(idQb,X0),X1)|less_equal(X1,X0))),
% 51.80/7.00 inference(resolution,[status(thm)],[f12776,f149])).
% 51.80/7.00 fof(f13469,plain,(
% 51.80/7.00 ![X0]: (less_equal(idQ_idQb,divide(idQ_idQb,divide(idQb,X0))))),
% 51.80/7.00 inference(paramodulation,[status(thm)],[f7328,f9045])).
% 51.80/7.00 fof(f13477,plain,(
% 51.80/7.00 ![X0]: (less_equal(idQ_idQa,divide(idQ_idQa,divide(idQa,X0))))),
% 51.80/7.00 inference(paramodulation,[status(thm)],[f7028,f9045])).
% 51.80/7.00 fof(f16913,plain,(
% 51.80/7.00 ![X0]: (divide(idQ_idQb,divide(idQb,X0))=idQ_idQb)),
% 51.80/7.00 inference(resolution,[status(thm)],[f13469,f106])).
% 51.80/7.00 fof(f17060,plain,(
% 51.80/7.00 ![X0]: (divide(idQ_idQa,divide(idQa,X0))=idQ_idQa)),
% 51.80/7.00 inference(resolution,[status(thm)],[f13477,f106])).
% 51.80/7.00 fof(f29278,plain,(
% 51.80/7.00 ![X0]: (less_equal(divide(idQb_Q__idQ_idQa,divide(idQa,X0)),X0))),
% 51.80/7.00 inference(resolution,[status(thm)],[f11522,f36])).
% 51.80/7.00 fof(f29962,plain,(
% 51.80/7.00 ![X0]: (less_equal(divide(idQa_Q__idQ_idQb,divide(idQb,X0)),X0))),
% 51.80/7.00 inference(resolution,[status(thm)],[f12790,f36])).
% 51.80/7.00 fof(f45691,plain,(
% 51.80/7.00 less_equal(idQb,divide(idQb,divide(idQa,idQa_Q__idQ_idQb)))),
% 51.80/7.00 inference(resolution,[status(thm)],[f7841,f36])).
% 51.80/7.00 fof(f46526,plain,(
% 51.80/7.00 less_equal(idQa,divide(idQa,divide(idQb,idQb_Q__idQ_idQa)))),
% 51.80/7.00 inference(resolution,[status(thm)],[f7874,f36])).
% 51.80/7.00 fof(f50676,plain,(
% 51.80/7.00 divide(idQb,divide(idQa,idQa_Q__idQ_idQb))=idQb),
% 51.80/7.00 inference(resolution,[status(thm)],[f45691,f106])).
% 51.80/7.00 fof(f50765,plain,(
% 51.80/7.00 less_equal(divide(idQb,divide(idQ_idQa,divide(idQa,idQa_Q__idQ_idQb))),divide(idQb_Q__idQ_idQa,divide(idQa,idQa_Q__idQ_idQb)))),
% 51.80/7.00 inference(paramodulation,[status(thm)],[f50676,f5837])).
% 51.80/7.00 fof(f50861,plain,(
% 51.80/7.00 less_equal(divide(idQb,idQ_idQa),divide(idQb_Q__idQ_idQa,divide(idQa,idQa_Q__idQ_idQb)))),
% 51.80/7.00 inference(forward_demodulation,[status(thm)],[f17060,f50765])).
% 51.80/7.00 fof(f50862,plain,(
% 51.80/7.00 less_equal(idQb_Q__idQ_idQa,divide(idQb_Q__idQ_idQa,divide(idQa,idQa_Q__idQ_idQb)))),
% 51.80/7.00 inference(forward_demodulation,[status(thm)],[f159,f50861])).
% 51.80/7.00 fof(f51517,plain,(
% 51.80/7.00 divide(idQa,divide(idQb,idQb_Q__idQ_idQa))=idQa),
% 51.80/7.00 inference(resolution,[status(thm)],[f46526,f106])).
% 51.80/7.00 fof(f51535,plain,(
% 51.80/7.00 less_equal(divide(idQa,divide(idQ_idQb,divide(idQb,idQb_Q__idQ_idQa))),divide(idQa_Q__idQ_idQb,divide(idQb,idQb_Q__idQ_idQa)))),
% 51.80/7.00 inference(paramodulation,[status(thm)],[f51517,f6139])).
% 51.80/7.00 fof(f51627,plain,(
% 51.80/7.00 less_equal(divide(idQa,idQ_idQb),divide(idQa_Q__idQ_idQb,divide(idQb,idQb_Q__idQ_idQa)))),
% 51.80/7.00 inference(forward_demodulation,[status(thm)],[f16913,f51535])).
% 51.80/7.00 fof(f51628,plain,(
% 51.80/7.00 less_equal(idQa_Q__idQ_idQb,divide(idQa_Q__idQ_idQb,divide(idQb,idQb_Q__idQ_idQa)))),
% 51.80/7.00 inference(forward_demodulation,[status(thm)],[f167,f51627])).
% 51.80/7.00 fof(f51810,plain,(
% 51.80/7.00 divide(idQb_Q__idQ_idQa,divide(idQa,idQa_Q__idQ_idQb))=idQb_Q__idQ_idQa),
% 51.80/7.00 inference(resolution,[status(thm)],[f50862,f106])).
% 51.80/7.00 fof(f51941,plain,(
% 51.80/7.00 less_equal(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb)),
% 51.80/7.00 inference(paramodulation,[status(thm)],[f51810,f29278])).
% 51.80/7.00 fof(f52095,plain,(
% 51.80/7.00 ~less_equal(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa)|idQb_Q__idQ_idQa=idQa_Q__idQ_idQb),
% 51.80/7.00 inference(resolution,[status(thm)],[f51941,f34])).
% 51.80/7.00 fof(f52097,plain,(
% 51.80/7.00 ~less_equal(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa)),
% 51.80/7.00 inference(forward_subsumption_resolution,[status(thm)],[f52095,f61])).
% 51.80/7.00 fof(f55134,plain,(
% 51.80/7.00 divide(idQa_Q__idQ_idQb,divide(idQb,idQb_Q__idQ_idQa))=idQa_Q__idQ_idQb),
% 51.80/7.00 inference(resolution,[status(thm)],[f51628,f106])).
% 51.80/7.00 fof(f55148,plain,(
% 51.80/7.00 less_equal(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa)),
% 51.80/7.00 inference(paramodulation,[status(thm)],[f55134,f29962])).
% 51.80/7.00 fof(f55255,plain,(
% 51.80/7.00 $false),
% 51.80/7.00 inference(forward_subsumption_resolution,[status(thm)],[f55148,f52097])).
% 51.80/7.00 % SZS output end CNFRefutation for theBenchmark.p
% 5.02/7.05 % Elapsed time: 6.670822 seconds
% 5.02/7.05 % CPU time: 52.552548 seconds
% 5.02/7.05 % Total memory used: 310.501 MB
% 5.02/7.05 % Net memory used: 260.300 MB
%------------------------------------------------------------------------------