%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP472-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:36:41 PM UTC 2026
% Result : Unsatisfiable 53.84s 7.22s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP472-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n011.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 20:14:25 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 53.84/7.22 % Refutation found
% 53.84/7.22 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 53.84/7.22 % SZS output start CNFRefutation for theBenchmark
% 53.84/7.22 fof(f1,axiom,(
% 53.84/7.22 (![A,B,C,D]: (divide(divide(inverse(divide(A,B)),divide(divide(C,D),A)),divide(D,C)) = B ))),
% 53.84/7.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.84/7.22 fof(f2,axiom,(
% 53.84/7.22 (![A,B]: (multiply(A,B) = divide(A,inverse(B)) ))),
% 53.84/7.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.84/7.22 fof(f3,negated_conjecture,(
% 53.84/7.22 multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
% 53.84/7.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 53.84/7.22 fof(f4,plain,(
% 53.84/7.22 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0)),divide(X3,X2))=X1)),
% 53.84/7.22 inference(cnf_transformation,[status(thm)],[f1])).
% 53.84/7.22 fof(f5,plain,(
% 53.84/7.22 ![X0,X1]: (multiply(X0,X1)=divide(X0,inverse(X1)))),
% 53.84/7.22 inference(cnf_transformation,[status(thm)],[f2])).
% 53.84/7.22 fof(f6,plain,(
% 53.84/7.22 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)),
% 53.84/7.22 inference(cnf_transformation,[status(thm)],[f3])).
% 53.84/7.22 fof(f7,definition,(
% 53.84/7.22 sF1_fnc=inverse(a1)),
% 53.84/7.22 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 53.84/7.22 fof(f8,definition,(
% 53.84/7.22 sF0_fnc=multiply(sF1_fnc,a1)),
% 53.84/7.22 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 53.84/7.22 fof(f9,definition,(
% 53.84/7.22 sF3_fnc=inverse(b1)),
% 53.84/7.22 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 53.84/7.22 fof(f10,definition,(
% 53.84/7.22 sF2_fnc=multiply(sF3_fnc,b1)),
% 53.84/7.22 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 53.84/7.22 fof(f11,plain,(
% 53.84/7.22 ~sF0_fnc=sF2_fnc),
% 53.84/7.22 inference(definition_folding,[],[f6,f10,f9,f8,f7])).
% 53.84/7.22 fof(f12,plain,(
% 53.84/7.22 ![X0]: (multiply(X0,b1)=divide(X0,sF3_fnc))),
% 53.84/7.22 inference(paramodulation,[status(thm)],[f9,f5])).
% 53.84/7.22 fof(f13,plain,(
% 53.84/7.22 ![X0]: (multiply(X0,a1)=divide(X0,sF1_fnc))),
% 53.84/7.22 inference(paramodulation,[status(thm)],[f7,f5])).
% 53.84/7.22 fof(f14,plain,(
% 53.84/7.22 sF2_fnc=divide(sF3_fnc,sF3_fnc)),
% 53.84/7.22 inference(backward_demodulation,[status(thm)],[f12,f10])).
% 53.84/7.22 fof(f15,plain,(
% 53.84/7.22 sF0_fnc=divide(sF1_fnc,sF1_fnc)),
% 53.84/7.22 inference(backward_demodulation,[status(thm)],[f13,f8])).
% 53.84/7.22 fof(f16,plain,(
% 53.84/7.22 ![X0,X1,X2,X3,X4,X5]: (divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(divide(X4,X5),X3)))),divide(X2,X1))=divide(X5,X4))),
% 53.84/7.22 inference(paramodulation,[status(thm)],[f4,f4])).
% 53.84/7.22 fof(f19,plain,(
% 53.84/7.22 ![X0,X1,X2,X3]: (divide(divide(inverse(multiply(X0,X1)),divide(divide(X2,X3),X0)),divide(X3,X2))=inverse(X1))),
% 53.84/7.22 inference(paramodulation,[status(thm)],[f5,f4])).
% 53.84/7.22 fof(f21,plain,(
% 53.84/7.22 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(inverse(X0),X1)),multiply(divide(X2,X3),X0)),divide(X3,X2))=X1)),
% 53.84/7.22 inference(paramodulation,[status(thm)],[f5,f4])).
% 53.84/7.22 fof(f23,plain,(
% 53.84/7.22 ![X0,X1]: (divide(divide(inverse(divide(X0,X1)),divide(sF0_fnc,X0)),divide(sF1_fnc,sF1_fnc))=X1)),
% 53.84/7.22 inference(paramodulation,[status(thm)],[f15,f4])).
% 53.84/7.22 fof(f24,plain,(
% 53.84/7.22 ![X0,X1]: (divide(divide(inverse(divide(X0,X1)),divide(sF2_fnc,X0)),divide(sF3_fnc,sF3_fnc))=X1)),
% 53.84/7.22 inference(paramodulation,[status(thm)],[f14,f4])).
% 53.84/7.22 fof(f29,plain,(
% 53.84/7.22 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(X0,X1)),divide(divide(inverse(X2),X3),X0)),multiply(X3,X2))=X1)),
% 53.84/7.22 inference(paramodulation,[status(thm)],[f5,f4])).
% 53.84/7.22 fof(f31,plain,(
% 53.84/7.22 ![X0,X1]: (divide(divide(inverse(divide(X0,X1)),divide(sF0_fnc,X0)),sF0_fnc)=X1)),
% 53.84/7.22 inference(forward_demodulation,[status(thm)],[f15,f23])).
% 53.84/7.22 fof(f32,plain,(
% 53.84/7.22 ![X0,X1]: (divide(divide(inverse(divide(X0,X1)),divide(sF2_fnc,X0)),sF2_fnc)=X1)),
% 53.84/7.22 inference(forward_demodulation,[status(thm)],[f14,f24])).
% 53.84/7.22 fof(f35,plain,(
% 53.84/7.22 ![X0,X1]: (divide(divide(inverse(X0),divide(sF0_fnc,divide(inverse(divide(X1,X0)),divide(sF0_fnc,X1)))),sF0_fnc)=sF0_fnc)),
% 53.84/7.22 inference(paramodulation,[status(thm)],[f31,f31])).
% 53.84/7.22 fof(f36,plain,(
% 53.84/7.22 ![X0,X1,X2,X3]: (divide(divide(inverse(X0),divide(sF0_fnc,divide(inverse(divide(X1,X0)),divide(divide(X2,X3),X1)))),sF0_fnc)=divide(X3,X2))),
% 53.84/7.22 inference(paramodulation,[status(thm)],[f4,f31])).
% 53.84/7.22 fof(f37,plain,(
% 53.84/7.22 divide(divide(inverse(sF0_fnc),divide(sF0_fnc,sF1_fnc)),sF0_fnc)=sF1_fnc),
% 53.84/7.22 inference(paramodulation,[status(thm)],[f15,f31])).
% 53.84/7.22 fof(f41,plain,(
% 53.84/7.23 ![X0,X1,X2]: (divide(divide(inverse(divide(sF0_fnc,X0)),X1),divide(divide(sF0_fnc,X2),inverse(divide(X2,X1))))=X0)),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f31,f4])).
% 53.84/7.23 fof(f42,plain,(
% 53.84/7.23 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(X0,X1)),divide(divide(sF0_fnc,divide(inverse(divide(X2,X3)),divide(sF0_fnc,X2))),X0)),X3)=X1)),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f31,f4])).
% 53.84/7.23 fof(f43,plain,(
% 53.84/7.23 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(X0,X1)),divide(X2,X0)),divide(sF0_fnc,divide(inverse(divide(X3,X2)),divide(sF0_fnc,X3))))=X1)),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f31,f4])).
% 53.84/7.23 fof(f44,plain,(
% 53.84/7.23 ![X0,X1,X2,X3]: (divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(sF0_fnc,X3)))),divide(X2,X1))=sF0_fnc)),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f31,f4])).
% 53.84/7.23 fof(f45,plain,(
% 53.84/7.23 ![X0,X1,X2]: (divide(divide(inverse(divide(sF0_fnc,X0)),X1),multiply(divide(sF0_fnc,X2),divide(X2,X1)))=X0)),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f5,f41])).
% 53.84/7.23 fof(f47,plain,(
% 53.84/7.23 ![X0,X1]: (divide(divide(inverse(X0),divide(sF2_fnc,divide(inverse(divide(X1,X0)),divide(sF0_fnc,X1)))),sF2_fnc)=sF0_fnc)),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f31,f32])).
% 53.84/7.23 fof(f51,plain,(
% 53.84/7.23 ![X0,X1]: (divide(divide(inverse(multiply(X0,X1)),divide(sF2_fnc,X0)),sF2_fnc)=inverse(X1))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f5,f32])).
% 53.84/7.23 fof(f53,plain,(
% 53.84/7.23 ![X0,X1,X2]: (divide(divide(inverse(divide(sF2_fnc,X0)),X1),divide(divide(sF2_fnc,X2),inverse(divide(X2,X1))))=X0)),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f32,f4])).
% 53.84/7.23 fof(f57,plain,(
% 53.84/7.23 ![X0,X1,X2,X3]: (divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(sF2_fnc,X3)))),divide(X2,X1))=sF2_fnc)),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f32,f4])).
% 53.84/7.23 fof(f58,plain,(
% 53.84/7.23 ![X0,X1,X2]: (divide(divide(inverse(divide(sF2_fnc,X0)),X1),multiply(divide(sF2_fnc,X2),divide(X2,X1)))=X0)),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f5,f53])).
% 53.84/7.23 fof(f59,plain,(
% 53.84/7.23 ![X0]: (divide(divide(inverse(divide(sF0_fnc,X0)),sF1_fnc),divide(divide(sF0_fnc,sF1_fnc),inverse(sF0_fnc)))=X0)),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f37,f4])).
% 53.84/7.23 fof(f65,plain,(
% 53.84/7.23 ![X0]: (divide(divide(inverse(divide(sF0_fnc,X0)),sF1_fnc),multiply(divide(sF0_fnc,sF1_fnc),sF0_fnc))=X0)),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f5,f59])).
% 53.84/7.23 fof(f299,plain,(
% 53.84/7.23 ![X0,X1,X2]: (divide(divide(inverse(divide(sF2_fnc,X0)),inverse(X1)),divide(divide(sF2_fnc,X2),inverse(multiply(X2,X1))))=X0)),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f51,f4])).
% 53.84/7.23 fof(f315,plain,(
% 53.84/7.23 ![X0,X1,X2]: (divide(multiply(inverse(divide(sF2_fnc,X0)),X1),divide(divide(sF2_fnc,X2),inverse(multiply(X2,X1))))=X0)),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f5,f299])).
% 53.84/7.23 fof(f316,plain,(
% 53.84/7.23 ![X0,X1,X2]: (divide(multiply(inverse(divide(sF2_fnc,X0)),X1),multiply(divide(sF2_fnc,X2),multiply(X2,X1)))=X0)),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f5,f315])).
% 53.84/7.23 fof(f992,plain,(
% 53.84/7.23 ![X0,X1,X2,X3,X4]: (divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(X4,X3)))),divide(X2,X1))=divide(multiply(divide(sF0_fnc,sF1_fnc),sF0_fnc),divide(inverse(divide(sF0_fnc,X4)),sF1_fnc)))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f65,f16])).
% 53.84/7.23 fof(f1003,plain,(
% 53.84/7.23 ![X0,X1]: (divide(multiply(divide(sF0_fnc,sF1_fnc),sF0_fnc),divide(inverse(divide(sF0_fnc,divide(X0,X1))),sF1_fnc))=divide(X1,X0))),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f992,f16])).
% 53.84/7.23 fof(f1012,plain,(
% 53.84/7.23 divide(multiply(divide(sF0_fnc,sF1_fnc),sF0_fnc),divide(inverse(divide(sF0_fnc,sF2_fnc)),sF1_fnc))=sF2_fnc),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f992,f57])).
% 53.84/7.23 fof(f1013,plain,(
% 53.84/7.23 divide(multiply(divide(sF0_fnc,sF1_fnc),sF0_fnc),divide(inverse(divide(sF0_fnc,sF0_fnc)),sF1_fnc))=sF0_fnc),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f992,f44])).
% 53.84/7.23 fof(f1745,plain,(
% 53.84/7.23 ![X0,X1]: (divide(multiply(divide(sF0_fnc,sF1_fnc),sF0_fnc),divide(inverse(divide(sF0_fnc,sF0_fnc)),sF1_fnc))=divide(sF0_fnc,divide(inverse(X0),divide(sF0_fnc,divide(inverse(divide(X1,X0)),divide(sF0_fnc,X1))))))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f35,f1003])).
% 53.84/7.23 fof(f1750,plain,(
% 53.84/7.23 ![X0,X1,X2]: (divide(divide(inverse(divide(sF0_fnc,X0)),sF0_fnc),multiply(divide(sF0_fnc,divide(inverse(X1),divide(sF0_fnc,divide(inverse(divide(X2,X1)),divide(sF0_fnc,X2))))),sF0_fnc))=X0)),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f35,f45])).
% 53.84/7.23 fof(f1762,plain,(
% 53.84/7.23 ![X0,X1]: (divide(divide(inverse(sF0_fnc),divide(sF0_fnc,divide(inverse(X0),divide(sF0_fnc,divide(inverse(divide(X1,X0)),divide(sF0_fnc,X1)))))),sF0_fnc)=sF0_fnc)),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f35,f31])).
% 53.84/7.23 fof(f1772,plain,(
% 53.84/7.23 ![X0,X1]: (sF0_fnc=divide(sF0_fnc,divide(inverse(X0),divide(sF0_fnc,divide(inverse(divide(X1,X0)),divide(sF0_fnc,X1))))))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f1013,f1745])).
% 53.84/7.23 fof(f1775,plain,(
% 53.84/7.23 ![X0]: (divide(divide(inverse(divide(sF0_fnc,X0)),sF0_fnc),multiply(sF0_fnc,sF0_fnc))=X0)),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f1772,f1750])).
% 53.84/7.23 fof(f1784,plain,(
% 53.84/7.23 divide(divide(inverse(sF0_fnc),sF0_fnc),sF0_fnc)=sF0_fnc),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f1772,f1762])).
% 53.84/7.23 fof(f1793,plain,(
% 53.84/7.23 divide(multiply(divide(sF0_fnc,sF1_fnc),sF0_fnc),divide(inverse(divide(sF0_fnc,sF0_fnc)),sF1_fnc))=divide(sF0_fnc,divide(inverse(sF0_fnc),sF0_fnc))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f1784,f1003])).
% 53.84/7.23 fof(f1809,plain,(
% 53.84/7.23 divide(divide(inverse(sF0_fnc),divide(sF2_fnc,divide(inverse(sF0_fnc),sF0_fnc))),sF2_fnc)=sF0_fnc),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f1784,f32])).
% 53.84/7.23 fof(f1820,plain,(
% 53.84/7.23 sF0_fnc=divide(sF0_fnc,divide(inverse(sF0_fnc),sF0_fnc))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f1013,f1793])).
% 53.84/7.23 fof(f1882,plain,(
% 53.84/7.23 divide(divide(inverse(sF0_fnc),sF0_fnc),multiply(sF0_fnc,sF0_fnc))=divide(inverse(sF0_fnc),sF0_fnc)),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f1820,f1775])).
% 53.84/7.23 fof(f1890,plain,(
% 53.84/7.23 ![X0]: (divide(multiply(divide(sF0_fnc,sF1_fnc),sF0_fnc),divide(inverse(divide(sF0_fnc,X0)),sF1_fnc))=divide(multiply(sF0_fnc,sF0_fnc),divide(inverse(divide(sF0_fnc,X0)),sF0_fnc)))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f1775,f1003])).
% 53.84/7.23 fof(f1915,plain,(
% 53.84/7.23 ![X0,X1]: (divide(multiply(sF0_fnc,sF0_fnc),divide(inverse(divide(sF0_fnc,divide(X0,X1))),sF0_fnc))=divide(X1,X0))),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f1890,f1003])).
% 53.84/7.23 fof(f1916,plain,(
% 53.84/7.23 divide(multiply(sF0_fnc,sF0_fnc),divide(inverse(divide(sF0_fnc,sF0_fnc)),sF0_fnc))=sF0_fnc),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f1890,f1013])).
% 53.84/7.23 fof(f1917,plain,(
% 53.84/7.23 divide(multiply(sF0_fnc,sF0_fnc),divide(inverse(divide(sF0_fnc,sF2_fnc)),sF0_fnc))=sF2_fnc),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f1890,f1012])).
% 53.84/7.23 fof(f2092,plain,(
% 53.84/7.23 divide(multiply(sF0_fnc,sF0_fnc),divide(inverse(sF0_fnc),sF0_fnc))=divide(sF0_fnc,inverse(sF0_fnc))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f1820,f1915])).
% 53.84/7.23 fof(f2155,plain,(
% 53.84/7.23 divide(multiply(sF0_fnc,sF0_fnc),divide(inverse(sF0_fnc),sF0_fnc))=multiply(sF0_fnc,sF0_fnc)),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f5,f2092])).
% 53.84/7.23 fof(f2257,plain,(
% 53.84/7.23 ![X0]: (divide(divide(inverse(divide(sF2_fnc,X0)),divide(inverse(divide(sF0_fnc,sF2_fnc)),sF0_fnc)),multiply(divide(sF2_fnc,multiply(sF0_fnc,sF0_fnc)),sF2_fnc))=X0)),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f1917,f58])).
% 53.84/7.23 fof(f2309,plain,(
% 53.84/7.23 ![X0,X1]: (divide(divide(inverse(multiply(sF0_fnc,sF0_fnc)),divide(divide(X0,X1),multiply(sF0_fnc,sF0_fnc))),divide(X1,X0))=divide(inverse(sF0_fnc),sF0_fnc))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f2155,f4])).
% 53.84/7.23 fof(f2488,plain,(
% 53.84/7.23 divide(multiply(sF0_fnc,sF0_fnc),divide(inverse(divide(sF0_fnc,sF0_fnc)),sF0_fnc))=divide(sF2_fnc,divide(inverse(sF0_fnc),divide(sF2_fnc,divide(inverse(sF0_fnc),sF0_fnc))))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f1809,f1915])).
% 53.84/7.23 fof(f2493,plain,(
% 53.84/7.23 ![X0]: (divide(divide(inverse(divide(sF2_fnc,X0)),sF2_fnc),multiply(divide(sF2_fnc,divide(inverse(sF0_fnc),divide(sF2_fnc,divide(inverse(sF0_fnc),sF0_fnc)))),sF0_fnc))=X0)),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f1809,f58])).
% 53.84/7.23 fof(f2505,plain,(
% 53.84/7.23 divide(divide(inverse(sF0_fnc),divide(sF2_fnc,divide(inverse(sF0_fnc),divide(sF2_fnc,divide(inverse(sF0_fnc),sF0_fnc))))),sF2_fnc)=sF2_fnc),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f1809,f32])).
% 53.84/7.23 fof(f2514,plain,(
% 53.84/7.23 sF0_fnc=divide(sF2_fnc,divide(inverse(sF0_fnc),divide(sF2_fnc,divide(inverse(sF0_fnc),sF0_fnc))))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f1916,f2488])).
% 53.84/7.23 fof(f2517,plain,(
% 53.84/7.23 ![X0]: (divide(divide(inverse(divide(sF2_fnc,X0)),sF2_fnc),multiply(sF0_fnc,sF0_fnc))=X0)),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f2514,f2493])).
% 53.84/7.23 fof(f2526,plain,(
% 53.84/7.23 divide(divide(inverse(sF0_fnc),sF0_fnc),sF2_fnc)=sF2_fnc),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f2514,f2505])).
% 53.84/7.23 fof(f2535,plain,(
% 53.84/7.23 divide(multiply(sF0_fnc,sF0_fnc),divide(inverse(divide(sF0_fnc,sF2_fnc)),sF0_fnc))=divide(sF2_fnc,divide(inverse(sF0_fnc),sF0_fnc))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f2526,f1915])).
% 53.84/7.23 fof(f2552,plain,(
% 53.84/7.23 divide(divide(inverse(sF2_fnc),divide(sF2_fnc,divide(inverse(sF0_fnc),sF0_fnc))),sF2_fnc)=sF2_fnc),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f2526,f32])).
% 53.84/7.23 fof(f2574,plain,(
% 53.84/7.23 sF2_fnc=divide(sF2_fnc,divide(inverse(sF0_fnc),sF0_fnc))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f1917,f2535])).
% 53.84/7.23 fof(f2588,plain,(
% 53.84/7.23 divide(divide(inverse(sF2_fnc),sF2_fnc),sF2_fnc)=sF2_fnc),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f2574,f2552])).
% 53.84/7.23 fof(f2641,plain,(
% 53.84/7.23 ![X0,X1]: (divide(multiply(inverse(sF2_fnc),X0),multiply(divide(sF2_fnc,X1),multiply(X1,X0)))=divide(inverse(sF0_fnc),sF0_fnc))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f2574,f316])).
% 53.84/7.23 fof(f2688,plain,(
% 53.84/7.23 divide(multiply(sF0_fnc,sF0_fnc),divide(inverse(divide(sF0_fnc,sF2_fnc)),sF0_fnc))=divide(sF2_fnc,divide(inverse(sF2_fnc),sF2_fnc))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f2588,f1915])).
% 53.84/7.23 fof(f2714,plain,(
% 53.84/7.23 sF2_fnc=divide(sF2_fnc,divide(inverse(sF2_fnc),sF2_fnc))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f1917,f2688])).
% 53.84/7.23 fof(f2878,plain,(
% 53.84/7.23 ![X0]: (divide(divide(inverse(X0),divide(sF0_fnc,divide(inverse(divide(sF2_fnc,X0)),sF2_fnc))),sF0_fnc)=divide(sF2_fnc,inverse(sF2_fnc)))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f2588,f36])).
% 53.84/7.23 fof(f2886,plain,(
% 53.84/7.23 ![X0]: (divide(divide(inverse(X0),divide(sF0_fnc,divide(inverse(divide(sF2_fnc,X0)),sF2_fnc))),sF0_fnc)=divide(sF0_fnc,inverse(sF0_fnc)))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f2526,f36])).
% 53.84/7.23 fof(f2960,plain,(
% 53.84/7.23 ![X0,X1,X2,X3,X4,X5]: (divide(divide(inverse(X0),divide(sF0_fnc,divide(inverse(divide(X1,X0)),divide(divide(X2,X3),X1)))),sF0_fnc)=divide(sF0_fnc,divide(inverse(X4),divide(sF0_fnc,divide(inverse(divide(X5,X4)),divide(divide(X3,X2),X5))))))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f36,f36])).
% 53.84/7.23 fof(f2988,plain,(
% 53.84/7.23 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(X0,X1)),divide(sF0_fnc,divide(inverse(X2),divide(sF0_fnc,divide(inverse(divide(X3,X2)),divide(divide(X1,X0),X3)))))),sF0_fnc)=sF0_fnc)),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f36,f31])).
% 53.84/7.23 fof(f3004,plain,(
% 53.84/7.23 ![X0]: (divide(divide(inverse(X0),divide(sF0_fnc,divide(inverse(divide(sF2_fnc,X0)),sF2_fnc))),sF0_fnc)=multiply(sF2_fnc,sF2_fnc))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f5,f2878])).
% 53.84/7.23 fof(f3013,plain,(
% 53.84/7.23 multiply(sF2_fnc,sF2_fnc)=divide(sF0_fnc,inverse(sF0_fnc))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f3004,f2886])).
% 53.84/7.23 fof(f3020,plain,(
% 53.84/7.23 multiply(sF2_fnc,sF2_fnc)=multiply(sF0_fnc,sF0_fnc)),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f5,f3013])).
% 53.84/7.23 fof(f3128,plain,(
% 53.84/7.23 ![X0,X1,X2,X3]: (divide(X0,X1)=divide(sF0_fnc,divide(inverse(X2),divide(sF0_fnc,divide(inverse(divide(X3,X2)),divide(divide(X0,X1),X3))))))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f36,f2960])).
% 53.84/7.23 fof(f3155,plain,(
% 53.84/7.23 ![X0,X1]: (divide(divide(inverse(divide(X0,X1)),divide(X1,X0)),sF0_fnc)=sF0_fnc)),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f3128,f2988])).
% 53.84/7.23 fof(f3166,plain,(
% 53.84/7.23 ![X0,X1]: (divide(divide(inverse(multiply(sF0_fnc,sF0_fnc)),divide(divide(sF0_fnc,divide(inverse(divide(X0,X1)),divide(sF0_fnc,X0))),multiply(sF0_fnc,sF0_fnc))),X1)=divide(inverse(sF0_fnc),sF0_fnc))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f2155,f42])).
% 53.84/7.23 fof(f3474,plain,(
% 53.84/7.23 ![X0,X1]: (divide(multiply(inverse(sF2_fnc),X0),multiply(divide(sF2_fnc,X1),multiply(X1,X0)))=divide(inverse(sF2_fnc),sF2_fnc))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f2714,f316])).
% 53.84/7.23 fof(f3527,plain,(
% 53.84/7.23 divide(inverse(sF0_fnc),sF0_fnc)=divide(inverse(sF2_fnc),sF2_fnc)),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f2641,f3474])).
% 53.84/7.23 fof(f3564,plain,(
% 53.84/7.23 ![X0,X1]: (divide(divide(inverse(divide(inverse(sF0_fnc),sF0_fnc)),multiply(divide(X0,X1),sF2_fnc)),divide(X1,X0))=sF2_fnc)),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f3527,f21])).
% 53.84/7.23 fof(f3755,plain,(
% 53.84/7.23 ![X0,X1]: (divide(multiply(sF0_fnc,sF0_fnc),divide(inverse(divide(sF0_fnc,sF0_fnc)),sF0_fnc))=divide(sF0_fnc,divide(inverse(divide(X0,X1)),divide(X1,X0))))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f3155,f1915])).
% 53.84/7.23 fof(f3888,plain,(
% 53.84/7.23 ![X0,X1]: (sF0_fnc=divide(sF0_fnc,divide(inverse(divide(X0,X1)),divide(X1,X0))))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f1916,f3755])).
% 53.84/7.23 fof(f4013,plain,(
% 53.84/7.23 ![X0,X1]: (divide(multiply(sF0_fnc,sF0_fnc),divide(inverse(sF0_fnc),sF0_fnc))=divide(divide(X0,X1),inverse(divide(X1,X0))))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f3888,f1915])).
% 53.84/7.23 fof(f4015,plain,(
% 53.84/7.23 ![X0,X1]: (divide(divide(inverse(sF0_fnc),sF0_fnc),multiply(sF0_fnc,sF0_fnc))=divide(inverse(divide(X0,X1)),divide(X1,X0)))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f3888,f1775])).
% 53.84/7.23 fof(f4172,plain,(
% 53.84/7.23 ![X0,X1]: (multiply(sF0_fnc,sF0_fnc)=divide(divide(X0,X1),inverse(divide(X1,X0))))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f2155,f4013])).
% 53.84/7.23 fof(f4177,plain,(
% 53.84/7.23 ![X0,X1]: (multiply(sF0_fnc,sF0_fnc)=multiply(divide(X0,X1),divide(X1,X0)))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f5,f4172])).
% 53.84/7.23 fof(f4188,plain,(
% 53.84/7.23 ![X0,X1]: (divide(inverse(sF0_fnc),sF0_fnc)=divide(inverse(divide(X0,X1)),divide(X1,X0)))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f1882,f4015])).
% 53.84/7.23 fof(f4277,plain,(
% 53.84/7.23 ![X0,X1]: (multiply(sF0_fnc,sF0_fnc)=multiply(multiply(X0,X1),divide(inverse(X1),X0)))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f5,f4177])).
% 53.84/7.23 fof(f4329,plain,(
% 53.84/7.23 ![X0,X1]: (multiply(sF0_fnc,sF0_fnc)=multiply(divide(inverse(X0),X1),multiply(X1,X0)))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f5,f4177])).
% 53.84/7.23 fof(f4343,plain,(
% 53.84/7.23 ![X0,X1]: (divide(divide(inverse(multiply(sF0_fnc,sF0_fnc)),divide(sF2_fnc,divide(X0,X1))),sF2_fnc)=inverse(divide(X1,X0)))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f4177,f51])).
% 53.84/7.23 fof(f4466,plain,(
% 53.84/7.23 ![X0,X1,X2,X3]: (divide(divide(inverse(multiply(sF0_fnc,sF0_fnc)),divide(divide(X0,X1),multiply(X2,X3))),divide(X1,X0))=inverse(divide(inverse(X3),X2)))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f4277,f19])).
% 53.84/7.23 fof(f4476,plain,(
% 53.84/7.23 inverse(divide(inverse(sF0_fnc),sF0_fnc))=divide(inverse(sF0_fnc),sF0_fnc)),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f4466,f2309])).
% 53.84/7.23 fof(f4485,plain,(
% 53.84/7.23 ![X0,X1]: (divide(divide(divide(inverse(sF0_fnc),sF0_fnc),multiply(divide(X0,X1),sF2_fnc)),divide(X1,X0))=sF2_fnc)),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f4476,f3564])).
% 53.84/7.23 fof(f5161,plain,(
% 53.84/7.23 ![X0,X1]: (divide(divide(inverse(sF2_fnc),divide(X0,multiply(sF0_fnc,sF0_fnc))),divide(sF0_fnc,divide(inverse(divide(X1,X0)),divide(sF0_fnc,X1))))=divide(inverse(divide(sF0_fnc,sF2_fnc)),sF0_fnc))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f1917,f43])).
% 53.84/7.23 fof(f5216,plain,(
% 53.84/7.23 ![X0,X1]: (divide(divide(inverse(divide(divide(inverse(sF0_fnc),sF0_fnc),X0)),multiply(sF0_fnc,sF0_fnc)),divide(sF0_fnc,divide(inverse(divide(X1,multiply(sF0_fnc,sF0_fnc))),divide(sF0_fnc,X1))))=X0)),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f2155,f43])).
% 53.84/7.23 fof(f5601,plain,(
% 53.84/7.23 divide(divide(inverse(divide(inverse(sF0_fnc),sF0_fnc)),divide(sF2_fnc,divide(inverse(multiply(sF0_fnc,sF0_fnc)),divide(sF0_fnc,multiply(sF0_fnc,sF0_fnc))))),sF2_fnc)=sF0_fnc),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f2155,f47])).
% 53.84/7.23 fof(f5699,plain,(
% 53.84/7.23 divide(divide(divide(inverse(sF0_fnc),sF0_fnc),divide(sF2_fnc,divide(inverse(multiply(sF0_fnc,sF0_fnc)),divide(sF0_fnc,multiply(sF0_fnc,sF0_fnc))))),sF2_fnc)=sF0_fnc),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f4476,f5601])).
% 53.84/7.23 fof(f5870,plain,(
% 53.84/7.23 ![X0,X1]: (divide(divide(inverse(sF0_fnc),sF0_fnc),X0)=divide(sF0_fnc,divide(inverse(divide(X1,X0)),divide(sF0_fnc,X1))))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f4188,f42])).
% 53.84/7.23 fof(f5871,plain,(
% 53.84/7.23 ![X0,X1]: (divide(divide(inverse(sF0_fnc),sF0_fnc),multiply(X0,X1))=divide(inverse(X1),X0))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f4188,f29])).
% 53.84/7.23 fof(f5872,plain,(
% 53.84/7.23 ![X0,X1]: (divide(divide(inverse(sF0_fnc),sF0_fnc),divide(X0,X1))=divide(X1,X0))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f4188,f4])).
% 53.84/7.23 fof(f5889,plain,(
% 53.84/7.23 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(inverse(sF0_fnc),sF0_fnc)),divide(X0,inverse(divide(X1,X2)))),divide(sF0_fnc,divide(inverse(divide(X3,X0)),divide(sF0_fnc,X3))))=divide(X2,X1))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f4188,f43])).
% 53.84/7.23 fof(f6131,plain,(
% 53.84/7.23 ![X0]: (divide(divide(inverse(divide(divide(inverse(sF0_fnc),sF0_fnc),X0)),multiply(sF0_fnc,sF0_fnc)),divide(divide(inverse(sF0_fnc),sF0_fnc),multiply(sF0_fnc,sF0_fnc)))=X0)),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f5870,f5216])).
% 53.84/7.23 fof(f6202,plain,(
% 53.84/7.23 ![X0]: (divide(divide(inverse(sF2_fnc),divide(X0,multiply(sF0_fnc,sF0_fnc))),divide(divide(inverse(sF0_fnc),sF0_fnc),X0))=divide(inverse(divide(sF0_fnc,sF2_fnc)),sF0_fnc))),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f5870,f5161])).
% 53.84/7.23 fof(f6260,plain,(
% 53.84/7.23 ![X0]: (divide(divide(inverse(multiply(sF0_fnc,sF0_fnc)),divide(divide(divide(inverse(sF0_fnc),sF0_fnc),X0),multiply(sF0_fnc,sF0_fnc))),X0)=divide(inverse(sF0_fnc),sF0_fnc))),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f5870,f3166])).
% 53.84/7.23 fof(f6288,plain,(
% 53.84/7.23 ![X0,X1]: (divide(divide(inverse(sF2_fnc),divide(X0,X1)),divide(X1,X0))=sF2_fnc)),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f5871,f4485])).
% 53.84/7.23 fof(f6294,plain,(
% 53.84/7.23 divide(divide(divide(inverse(multiply(sF0_fnc,sF0_fnc)),divide(sF0_fnc,multiply(sF0_fnc,sF0_fnc))),sF2_fnc),sF2_fnc)=sF0_fnc),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f5872,f5699])).
% 53.84/7.23 fof(f6337,plain,(
% 53.84/7.23 ![X0,X1,X2,X3]: (divide(divide(divide(inverse(sF0_fnc),sF0_fnc),divide(X0,inverse(divide(X1,X2)))),divide(sF0_fnc,divide(inverse(divide(X3,X0)),divide(sF0_fnc,X3))))=divide(X2,X1))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f4476,f5889])).
% 53.84/7.23 fof(f6338,plain,(
% 53.84/7.23 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(X0,X1)),X2),divide(sF0_fnc,divide(inverse(divide(X3,X2)),divide(sF0_fnc,X3))))=divide(X1,X0))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f5872,f6337])).
% 53.84/7.23 fof(f6339,plain,(
% 53.84/7.23 ![X0,X1,X2]: (divide(divide(inverse(divide(X0,X1)),X2),divide(divide(inverse(sF0_fnc),sF0_fnc),X2))=divide(X1,X0))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f5870,f6338])).
% 53.84/7.23 fof(f6506,plain,(
% 53.84/7.23 ![X0]: (divide(X0,divide(inverse(sF0_fnc),sF0_fnc))=X0)),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f6339,f6131])).
% 53.84/7.23 fof(f6673,plain,(
% 53.84/7.23 divide(inverse(sF0_fnc),sF0_fnc)=inverse(divide(sF0_fnc,inverse(sF0_fnc)))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f4188,f6506])).
% 53.84/7.23 fof(f6757,plain,(
% 53.84/7.23 divide(divide(divide(divide(inverse(sF0_fnc),sF0_fnc),divide(sF0_fnc,multiply(sF0_fnc,sF0_fnc))),sF2_fnc),sF2_fnc)=sF0_fnc),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f6772,f6294])).
% 53.84/7.23 fof(f6758,plain,(
% 53.84/7.23 ![X0]: (divide(divide(divide(inverse(sF0_fnc),sF0_fnc),divide(divide(divide(inverse(sF0_fnc),sF0_fnc),X0),multiply(sF0_fnc,sF0_fnc))),X0)=divide(inverse(sF0_fnc),sF0_fnc))),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f6772,f6260])).
% 53.84/7.23 fof(f6765,plain,(
% 53.84/7.23 ![X0,X1]: (divide(divide(divide(inverse(sF0_fnc),sF0_fnc),divide(sF2_fnc,divide(X0,X1))),sF2_fnc)=inverse(divide(X1,X0)))),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f6772,f4343])).
% 53.84/7.23 fof(f6772,plain,(
% 53.84/7.23 divide(inverse(sF0_fnc),sF0_fnc)=inverse(multiply(sF0_fnc,sF0_fnc))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f5,f6673])).
% 53.84/7.23 fof(f6823,plain,(
% 53.84/7.23 divide(divide(divide(multiply(sF0_fnc,sF0_fnc),sF0_fnc),sF2_fnc),sF2_fnc)=sF0_fnc),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f5872,f6757])).
% 53.84/7.23 fof(f6824,plain,(
% 53.84/7.23 ![X0]: (divide(divide(multiply(sF0_fnc,sF0_fnc),divide(divide(inverse(sF0_fnc),sF0_fnc),X0)),X0)=divide(inverse(sF0_fnc),sF0_fnc))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f5872,f6758])).
% 53.84/7.23 fof(f6834,plain,(
% 53.84/7.23 inverse(divide(sF0_fnc,multiply(sF0_fnc,sF0_fnc)))=sF0_fnc),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f6837,f6823])).
% 53.84/7.23 fof(f6837,plain,(
% 53.84/7.23 ![X0,X1]: (divide(divide(divide(X0,X1),sF2_fnc),sF2_fnc)=inverse(divide(X1,X0)))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f5872,f6765])).
% 53.84/7.23 fof(f6989,plain,(
% 53.84/7.23 divide(inverse(sF0_fnc),sF0_fnc)=divide(sF0_fnc,divide(multiply(sF0_fnc,sF0_fnc),sF0_fnc))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f6834,f4188])).
% 53.84/7.23 fof(f7703,plain,(
% 53.84/7.23 ![X0]: (multiply(X0,multiply(sF0_fnc,sF0_fnc))=divide(X0,divide(inverse(sF0_fnc),sF0_fnc)))),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f6772,f5])).
% 53.84/7.23 fof(f7749,plain,(
% 53.84/7.23 ![X0]: (multiply(X0,multiply(sF0_fnc,sF0_fnc))=X0)),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f6506,f7703])).
% 53.84/7.23 fof(f7795,plain,(
% 53.84/7.23 multiply(sF0_fnc,sF0_fnc)=divide(inverse(sF0_fnc),sF0_fnc)),
% 53.84/7.23 inference(paramodulation,[status(thm)],[f4329,f7749])).
% 53.84/7.23 fof(f7824,plain,(
% 53.84/7.23 ![X0]: (divide(X0,multiply(sF0_fnc,sF0_fnc))=X0)),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f7795,f6506])).
% 53.84/7.23 fof(f7829,plain,(
% 53.84/7.23 divide(multiply(sF0_fnc,sF0_fnc),sF0_fnc)=sF0_fnc),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f7795,f1784])).
% 53.84/7.23 fof(f7856,plain,(
% 53.84/7.23 multiply(sF0_fnc,sF0_fnc)=divide(sF0_fnc,divide(multiply(sF0_fnc,sF0_fnc),sF0_fnc))),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f7795,f6989])).
% 53.84/7.23 fof(f7862,plain,(
% 53.84/7.23 ![X0]: (divide(divide(multiply(sF0_fnc,sF0_fnc),divide(divide(inverse(sF0_fnc),sF0_fnc),X0)),X0)=multiply(sF0_fnc,sF0_fnc))),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f7795,f6824])).
% 53.84/7.23 fof(f7980,plain,(
% 53.84/7.23 ![X0]: (divide(divide(inverse(sF2_fnc),divide(X0,multiply(sF0_fnc,sF0_fnc))),divide(multiply(sF0_fnc,sF0_fnc),X0))=divide(inverse(divide(sF0_fnc,sF2_fnc)),sF0_fnc))),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f7795,f6202])).
% 53.84/7.23 fof(f8051,plain,(
% 53.84/7.23 ![X0,X1]: (divide(multiply(sF0_fnc,sF0_fnc),divide(X0,X1))=divide(X1,X0))),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f7795,f5872])).
% 53.84/7.23 fof(f8132,plain,(
% 53.84/7.23 ![X0]: (divide(inverse(divide(sF2_fnc,X0)),sF2_fnc)=X0)),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f7824,f2517])).
% 53.84/7.23 fof(f8138,plain,(
% 53.84/7.23 ![X0]: (divide(divide(inverse(divide(sF2_fnc,X0)),divide(inverse(divide(sF0_fnc,sF2_fnc)),sF0_fnc)),multiply(sF2_fnc,sF2_fnc))=X0)),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f7824,f2257])).
% 53.84/7.23 fof(f8282,plain,(
% 53.84/7.23 multiply(sF0_fnc,sF0_fnc)=divide(sF0_fnc,sF0_fnc)),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f7829,f7856])).
% 53.84/7.23 fof(f8293,plain,(
% 53.84/7.23 ![X0]: (divide(divide(divide(sF0_fnc,sF0_fnc),divide(divide(inverse(sF0_fnc),sF0_fnc),X0)),X0)=multiply(sF0_fnc,sF0_fnc))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f8282,f7862])).
% 53.84/7.23 fof(f8294,plain,(
% 53.84/7.23 ![X0]: (divide(divide(divide(sF0_fnc,sF0_fnc),divide(multiply(sF0_fnc,sF0_fnc),X0)),X0)=multiply(sF0_fnc,sF0_fnc))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f7795,f8293])).
% 53.84/7.23 fof(f8295,plain,(
% 53.84/7.23 ![X0]: (divide(divide(divide(sF0_fnc,sF0_fnc),divide(divide(sF0_fnc,sF0_fnc),X0)),X0)=multiply(sF0_fnc,sF0_fnc))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f8282,f8294])).
% 53.84/7.23 fof(f8296,plain,(
% 53.84/7.23 ![X0]: (divide(divide(divide(sF0_fnc,sF0_fnc),divide(divide(sF0_fnc,sF0_fnc),X0)),X0)=divide(sF0_fnc,sF0_fnc))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f8282,f8295])).
% 53.84/7.23 fof(f8452,plain,(
% 53.84/7.23 sF2_fnc=divide(inverse(divide(sF0_fnc,sF2_fnc)),sF0_fnc)),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f6288,f7980])).
% 53.84/7.23 fof(f8551,plain,(
% 53.84/7.23 ![X0]: (divide(divide(X0,divide(sF0_fnc,sF0_fnc)),X0)=divide(sF0_fnc,sF0_fnc))),
% 53.84/7.23 inference(backward_demodulation,[status(thm)],[f8555,f8296])).
% 53.84/7.23 fof(f8555,plain,(
% 53.84/7.23 ![X0,X1]: (divide(divide(sF0_fnc,sF0_fnc),divide(X0,X1))=divide(X1,X0))),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f8282,f8051])).
% 53.84/7.23 fof(f8629,plain,(
% 53.84/7.23 ![X0]: (divide(divide(inverse(divide(sF2_fnc,X0)),sF2_fnc),multiply(sF2_fnc,sF2_fnc))=X0)),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f8452,f8138])).
% 53.84/7.23 fof(f8630,plain,(
% 53.84/7.23 ![X0]: (divide(X0,multiply(sF2_fnc,sF2_fnc))=X0)),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f8132,f8629])).
% 53.84/7.23 fof(f8631,plain,(
% 53.84/7.23 ![X0]: (divide(X0,multiply(sF0_fnc,sF0_fnc))=X0)),
% 53.84/7.23 inference(forward_demodulation,[status(thm)],[f3020,f8630])).
% 53.84/7.23 fof(f8642,plain,(
% 50.23/7.40 ![X0]: (divide(X0,divide(sF0_fnc,sF0_fnc))=X0)),
% 50.23/7.40 inference(forward_demodulation,[status(thm)],[f8282,f8631])).
% 50.23/7.40 fof(f9634,plain,(
% 50.23/7.40 sF0_fnc=divide(sF0_fnc,sF0_fnc)),
% 50.23/7.40 inference(backward_demodulation,[status(thm)],[f9644,f15])).
% 50.23/7.40 fof(f9635,plain,(
% 50.23/7.40 sF2_fnc=divide(sF0_fnc,sF0_fnc)),
% 50.23/7.40 inference(backward_demodulation,[status(thm)],[f9644,f14])).
% 50.23/7.40 fof(f9644,plain,(
% 50.23/7.40 ![X0]: (divide(X0,X0)=divide(sF0_fnc,sF0_fnc))),
% 50.23/7.40 inference(forward_demodulation,[status(thm)],[f8642,f8551])).
% 50.23/7.40 fof(f10636,plain,(
% 50.23/7.40 sF2_fnc=sF0_fnc),
% 50.23/7.40 inference(forward_demodulation,[status(thm)],[f9634,f9635])).
% 50.23/7.40 fof(f10637,plain,(
% 50.23/7.40 $false),
% 50.23/7.40 inference(forward_subsumption_resolution,[status(thm)],[f10636,f11])).
% 50.23/7.40 % SZS output end CNFRefutation for theBenchmark.p
% 15.73/7.44 % Elapsed time: 7.042956 seconds
% 15.73/7.44 % CPU time: 55.315563 seconds
% 15.73/7.44 % Total memory used: 726.304 MB
% 15.73/7.44 % Net memory used: 719.933 MB
%------------------------------------------------------------------------------