%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP469-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 : 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:36:40 PM UTC 2026
% Result : Unsatisfiable 227.32s 29.14s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP469-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 : n026.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:16:52 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 227.32/29.14 % Refutation found
% 227.32/29.14 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 227.32/29.14 % SZS output start CNFRefutation for theBenchmark
% 227.32/29.14 fof(f1,axiom,(
% 227.32/29.14 (![A,B,C,D]: (divide(inverse(divide(A,divide(B,divide(C,D)))),divide(divide(D,C),A)) = B ))),
% 227.32/29.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 227.32/29.14 fof(f2,axiom,(
% 227.32/29.14 (![A,B]: (multiply(A,B) = divide(A,inverse(B)) ))),
% 227.32/29.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 227.32/29.14 fof(f3,negated_conjecture,(
% 227.32/29.14 multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
% 227.32/29.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 227.32/29.14 fof(f4,plain,(
% 227.32/29.14 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,divide(X1,divide(X2,X3)))),divide(divide(X3,X2),X0))=X1)),
% 227.32/29.14 inference(cnf_transformation,[status(thm)],[f1])).
% 227.32/29.14 fof(f5,plain,(
% 227.32/29.14 ![X0,X1]: (multiply(X0,X1)=divide(X0,inverse(X1)))),
% 227.32/29.14 inference(cnf_transformation,[status(thm)],[f2])).
% 227.32/29.14 fof(f6,plain,(
% 227.32/29.14 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)),
% 227.32/29.14 inference(cnf_transformation,[status(thm)],[f3])).
% 227.32/29.14 fof(f7,definition,(
% 227.32/29.14 sF1_fnc=inverse(a1)),
% 227.32/29.14 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 227.32/29.14 fof(f8,definition,(
% 227.32/29.14 sF0_fnc=multiply(sF1_fnc,a1)),
% 227.32/29.14 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 227.32/29.14 fof(f9,definition,(
% 227.32/29.14 sF3_fnc=inverse(b1)),
% 227.32/29.14 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 227.32/29.14 fof(f10,definition,(
% 227.32/29.14 sF2_fnc=multiply(sF3_fnc,b1)),
% 227.32/29.14 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 227.32/29.14 fof(f11,plain,(
% 227.32/29.14 ~sF0_fnc=sF2_fnc),
% 227.32/29.14 inference(definition_folding,[],[f6,f10,f9,f8,f7])).
% 227.32/29.14 fof(f12,plain,(
% 227.32/29.14 ![X0]: (multiply(X0,b1)=divide(X0,sF3_fnc))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f9,f5])).
% 227.32/29.14 fof(f13,plain,(
% 227.32/29.14 ![X0]: (multiply(X0,a1)=divide(X0,sF1_fnc))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f7,f5])).
% 227.32/29.14 fof(f14,plain,(
% 227.32/29.14 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),divide(divide(X1,X2),inverse(divide(divide(X2,X1),divide(X0,divide(X3,X4))))))=divide(X4,X3))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f4,f4])).
% 227.32/29.14 fof(f15,plain,(
% 227.32/29.14 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(X0,X1)),divide(divide(X2,divide(X3,X4)),X0))=inverse(divide(X2,divide(X1,divide(X4,X3)))))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f4,f4])).
% 227.32/29.14 fof(f17,plain,(
% 227.32/29.14 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,divide(X1,multiply(X2,X3)))),divide(divide(inverse(X3),X2),X0))=X1)),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f5,f4])).
% 227.32/29.14 fof(f18,plain,(
% 227.32/29.14 ![X0,X1,X2,X3]: (divide(inverse(divide(inverse(X0),divide(X1,divide(X2,X3)))),multiply(divide(X3,X2),X0))=X1)),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f5,f4])).
% 227.32/29.14 fof(f21,plain,(
% 227.32/29.14 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,divide(X3,X4)))))=divide(X4,X3))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f5,f14])).
% 227.32/29.14 fof(f24,plain,(
% 227.32/29.14 sF2_fnc=divide(sF3_fnc,sF3_fnc)),
% 227.32/29.14 inference(backward_demodulation,[status(thm)],[f12,f10])).
% 227.32/29.14 fof(f25,plain,(
% 227.32/29.14 ![X0,X1]: (divide(inverse(divide(X0,divide(X1,divide(sF3_fnc,sF3_fnc)))),divide(sF2_fnc,X0))=X1)),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f24,f4])).
% 227.32/29.14 fof(f27,plain,(
% 227.32/29.14 ![X0,X1]: (divide(inverse(divide(X0,divide(X1,sF2_fnc))),divide(sF2_fnc,X0))=X1)),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f24,f25])).
% 227.32/29.14 fof(f29,plain,(
% 227.32/29.14 sF0_fnc=divide(sF1_fnc,sF1_fnc)),
% 227.32/29.14 inference(backward_demodulation,[status(thm)],[f13,f8])).
% 227.32/29.14 fof(f30,plain,(
% 227.32/29.14 ![X0,X1]: (divide(inverse(divide(X0,divide(X1,divide(sF1_fnc,sF1_fnc)))),divide(sF0_fnc,X0))=X1)),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f29,f4])).
% 227.32/29.14 fof(f32,plain,(
% 227.32/29.14 ![X0,X1]: (divide(inverse(divide(X0,divide(X1,sF0_fnc))),divide(sF0_fnc,X0))=X1)),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f29,f30])).
% 227.32/29.14 fof(f34,plain,(
% 227.32/29.14 ![X0]: (divide(inverse(X0),divide(sF2_fnc,inverse(divide(sF2_fnc,divide(X0,sF2_fnc)))))=sF2_fnc)),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f27,f27])).
% 227.32/29.14 fof(f35,plain,(
% 227.32/29.14 ![X0,X1,X2]: (divide(inverse(X0),divide(sF2_fnc,inverse(divide(sF2_fnc,divide(X0,divide(X1,X2))))))=divide(X2,X1))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f4,f27])).
% 227.32/29.14 fof(f37,plain,(
% 227.32/29.14 ![X0,X1,X2]: (divide(inverse(X0),divide(divide(X1,X2),inverse(divide(divide(X2,X1),divide(X0,sF2_fnc)))))=sF2_fnc)),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f27,f4])).
% 227.32/29.14 fof(f39,plain,(
% 227.32/29.14 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,divide(X1,divide(divide(sF2_fnc,X2),inverse(divide(X2,divide(X3,sF2_fnc))))))),divide(X3,X0))=X1)),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f27,f4])).
% 227.32/29.14 fof(f41,plain,(
% 227.32/29.14 ![X0]: (divide(inverse(X0),multiply(sF2_fnc,divide(sF2_fnc,divide(X0,sF2_fnc))))=sF2_fnc)),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f5,f34])).
% 227.32/29.14 fof(f42,plain,(
% 227.32/29.14 ![X0,X1,X2]: (divide(inverse(X0),multiply(sF2_fnc,divide(sF2_fnc,divide(X0,divide(X1,X2)))))=divide(X2,X1))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f5,f35])).
% 227.32/29.14 fof(f43,plain,(
% 227.32/29.14 ![X0,X1,X2]: (divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,sF2_fnc))))=sF2_fnc)),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f5,f37])).
% 227.32/29.14 fof(f44,plain,(
% 227.32/29.14 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,divide(X1,multiply(divide(sF2_fnc,X2),divide(X2,divide(X3,sF2_fnc)))))),divide(X3,X0))=X1)),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f5,f39])).
% 227.32/29.14 fof(f48,plain,(
% 227.32/29.14 ![X0,X1,X2]: (divide(inverse(X0),divide(sF0_fnc,inverse(divide(sF0_fnc,divide(X0,divide(X1,X2))))))=divide(X2,X1))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f4,f32])).
% 227.32/29.14 fof(f50,plain,(
% 227.32/29.14 ![X0]: (divide(inverse(X0),divide(sF2_fnc,inverse(divide(sF2_fnc,divide(X0,sF0_fnc)))))=sF0_fnc)),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f32,f27])).
% 227.32/29.14 fof(f51,plain,(
% 227.32/29.14 ![X0,X1,X2]: (divide(inverse(X0),divide(divide(X1,X2),inverse(divide(divide(X2,X1),divide(X0,sF0_fnc)))))=sF0_fnc)),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f32,f4])).
% 227.32/29.14 fof(f53,plain,(
% 227.32/29.14 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,divide(X1,divide(divide(sF0_fnc,X2),inverse(divide(X2,divide(X3,sF0_fnc))))))),divide(X3,X0))=X1)),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f32,f4])).
% 227.32/29.14 fof(f57,plain,(
% 227.32/29.14 ![X0,X1,X2]: (divide(inverse(X0),multiply(sF0_fnc,divide(sF0_fnc,divide(X0,divide(X1,X2)))))=divide(X2,X1))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f5,f48])).
% 227.32/29.14 fof(f58,plain,(
% 227.32/29.14 ![X0]: (divide(inverse(X0),multiply(sF2_fnc,divide(sF2_fnc,divide(X0,sF0_fnc))))=sF0_fnc)),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f5,f50])).
% 227.32/29.14 fof(f59,plain,(
% 227.32/29.14 ![X0,X1,X2]: (divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,sF0_fnc))))=sF0_fnc)),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f5,f51])).
% 227.32/29.14 fof(f60,plain,(
% 227.32/29.14 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,divide(X1,multiply(divide(sF0_fnc,X2),divide(X2,divide(X3,sF0_fnc)))))),divide(X3,X0))=X1)),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f5,f53])).
% 227.32/29.14 fof(f63,plain,(
% 227.32/29.14 ![X0,X1,X2,X3]: (divide(sF1_fnc,multiply(divide(X0,X1),divide(divide(X1,X0),divide(a1,divide(X2,X3)))))=divide(X3,X2))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f7,f21])).
% 227.32/29.14 fof(f77,plain,(
% 227.32/29.14 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),multiply(divide(inverse(X1),X2),divide(multiply(X2,X1),divide(X0,divide(X3,X4)))))=divide(X4,X3))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f5,f21])).
% 227.32/29.14 fof(f83,plain,(
% 227.32/29.14 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,X3))))=divide(divide(sF0_fnc,X4),inverse(divide(X4,divide(X3,sF0_fnc)))))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f32,f21])).
% 227.32/29.14 fof(f86,plain,(
% 227.32/29.14 ![X0,X1,X2,X3,X4,X5,X6,X7]: (divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,divide(X3,X4)))))=divide(multiply(divide(X5,X6),divide(divide(X6,X5),divide(X7,divide(X4,X3)))),inverse(X7)))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f21,f21])).
% 227.32/29.14 fof(f87,plain,(
% 227.32/29.14 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,multiply(X3,X4)))))=divide(inverse(X4),X3))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f5,f21])).
% 227.32/29.14 fof(f104,plain,(
% 227.32/29.14 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,X3))))=multiply(divide(sF0_fnc,X4),divide(X4,divide(X3,sF0_fnc))))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f5,f83])).
% 227.32/29.14 fof(f107,plain,(
% 227.32/29.14 ![X0,X1,X2,X3,X4]: (divide(X0,X1)=divide(multiply(divide(X2,X3),divide(divide(X3,X2),divide(X4,divide(X0,X1)))),inverse(X4)))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f21,f86])).
% 227.32/29.14 fof(f108,plain,(
% 227.32/29.14 ![X0,X1,X2,X3,X4]: (divide(X0,X1)=multiply(multiply(divide(X2,X3),divide(divide(X3,X2),divide(X4,divide(X0,X1)))),X4))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f5,f107])).
% 227.32/29.14 fof(f145,plain,(
% 227.32/29.14 ![X0,X1,X2,X3]: (X0=inverse(divide(X1,divide(divide(X0,divide(divide(X2,X3),X1)),divide(X3,X2)))))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f4,f15])).
% 227.32/29.14 fof(f159,plain,(
% 227.32/29.14 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,X1)),divide(X2,X0))=inverse(divide(inverse(divide(X3,divide(X2,sF0_fnc))),divide(X1,divide(X3,sF0_fnc)))))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f32,f15])).
% 227.32/29.14 fof(f167,plain,(
% 227.32/29.14 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0))=inverse(divide(X2,divide(X1,divide(divide(sF0_fnc,X4),inverse(divide(X4,divide(X3,sF0_fnc))))))))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f32,f15])).
% 227.32/29.14 fof(f195,plain,(
% 227.32/29.14 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0))=inverse(divide(X2,divide(X1,multiply(divide(sF0_fnc,X4),divide(X4,divide(X3,sF0_fnc)))))))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f5,f167])).
% 227.32/29.14 fof(f512,plain,(
% 227.32/29.14 ![X0,X1]: (X0=inverse(divide(X1,divide(divide(X0,divide(sF2_fnc,X1)),divide(sF3_fnc,sF3_fnc)))))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f24,f145])).
% 227.32/29.14 fof(f561,plain,(
% 227.32/29.14 ![X0,X1]: (X0=inverse(divide(X1,divide(divide(X0,divide(sF2_fnc,X1)),sF2_fnc))))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f24,f512])).
% 227.32/29.14 fof(f605,plain,(
% 227.32/29.14 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),divide(divide(inverse(X1),X2),inverse(divide(multiply(X2,X1),divide(X0,multiply(X3,X4))))))=divide(inverse(X4),X3))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f17,f17])).
% 227.32/29.14 fof(f606,plain,(
% 227.32/29.14 ![X0,X1,X2]: (divide(inverse(X0),divide(divide(inverse(X1),X2),inverse(divide(multiply(X2,X1),divide(X0,sF0_fnc)))))=sF0_fnc)),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f32,f17])).
% 227.32/29.14 fof(f672,plain,(
% 227.32/29.14 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),multiply(divide(inverse(X1),X2),divide(multiply(X2,X1),divide(X0,multiply(X3,X4)))))=divide(inverse(X4),X3))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f5,f605])).
% 227.32/29.14 fof(f673,plain,(
% 227.32/29.14 ![X0,X1,X2]: (divide(inverse(X0),multiply(divide(inverse(X1),X2),divide(multiply(X2,X1),divide(X0,sF0_fnc))))=sF0_fnc)),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f5,f606])).
% 227.32/29.14 fof(f703,plain,(
% 227.32/29.14 ![X0,X1]: (X0=inverse(divide(inverse(X1),divide(divide(X0,multiply(sF2_fnc,X1)),sF2_fnc))))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f5,f561])).
% 227.32/29.14 fof(f716,plain,(
% 227.32/29.14 ![X0,X1,X2]: (multiply(X0,divide(X1,divide(divide(X2,divide(sF2_fnc,X1)),sF2_fnc)))=divide(X0,X2))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f561,f5])).
% 227.32/29.14 fof(f784,plain,(
% 227.32/29.14 ![X0,X1,X2]: (multiply(X0,divide(inverse(X1),divide(divide(X2,multiply(sF2_fnc,X1)),sF2_fnc)))=divide(X0,X2))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f703,f5])).
% 227.32/29.14 fof(f1045,plain,(
% 227.32/29.14 ![X0,X1,X2,X3]: (divide(inverse(X0),multiply(sF2_fnc,divide(sF2_fnc,divide(X0,divide(X1,X2)))))=divide(multiply(sF2_fnc,divide(sF2_fnc,divide(X3,divide(X2,X1)))),inverse(X3)))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f42,f42])).
% 227.32/29.14 fof(f1092,plain,(
% 227.32/29.14 ![X0,X1,X2]: (divide(X0,X1)=divide(multiply(sF2_fnc,divide(sF2_fnc,divide(X2,divide(X0,X1)))),inverse(X2)))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f42,f1045])).
% 227.32/29.14 fof(f1093,plain,(
% 227.32/29.14 ![X0,X1,X2]: (divide(X0,X1)=multiply(multiply(sF2_fnc,divide(sF2_fnc,divide(X2,divide(X0,X1)))),X2))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f5,f1092])).
% 227.32/29.14 fof(f1739,plain,(
% 227.32/29.14 ![X0,X1]: (divide(sF1_fnc,multiply(divide(X0,X1),divide(divide(X1,X0),divide(a1,sF2_fnc))))=sF2_fnc)),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f7,f43])).
% 227.32/29.14 fof(f1815,plain,(
% 227.32/29.14 ![X0,X1,X2,X3]: (divide(inverse(X0),multiply(sF2_fnc,divide(sF2_fnc,divide(X0,sF2_fnc))))=divide(multiply(divide(X1,X2),divide(divide(X2,X1),divide(X3,sF2_fnc))),inverse(X3)))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f43,f42])).
% 227.32/29.14 fof(f1901,plain,(
% 227.32/29.14 ![X0,X1,X2]: (sF2_fnc=divide(multiply(divide(X0,X1),divide(divide(X1,X0),divide(X2,sF2_fnc))),inverse(X2)))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f41,f1815])).
% 227.32/29.14 fof(f1902,plain,(
% 227.32/29.14 ![X0,X1,X2]: (sF2_fnc=multiply(multiply(divide(X0,X1),divide(divide(X1,X0),divide(X2,sF2_fnc))),X2))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f5,f1901])).
% 227.32/29.14 fof(f2706,plain,(
% 227.32/29.14 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(inverse(X0),divide(X1,divide(X2,X3)))),multiply(divide(X3,X2),X0))=multiply(multiply(sF2_fnc,divide(sF2_fnc,divide(X4,X1))),X4))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f18,f1093])).
% 227.32/29.14 fof(f2754,plain,(
% 227.32/29.14 ![X0,X1]: (X0=multiply(multiply(sF2_fnc,divide(sF2_fnc,divide(X1,X0))),X1))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f18,f2706])).
% 227.32/29.14 fof(f2832,plain,(
% 227.32/29.14 ![X0,X1,X2,X3]: (divide(inverse(X0),multiply(sF0_fnc,divide(sF0_fnc,divide(X0,divide(X1,X2)))))=divide(multiply(sF0_fnc,divide(sF0_fnc,divide(X3,divide(X2,X1)))),inverse(X3)))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f57,f57])).
% 227.32/29.14 fof(f2905,plain,(
% 227.32/29.14 ![X0,X1,X2]: (divide(X0,X1)=divide(multiply(sF0_fnc,divide(sF0_fnc,divide(X2,divide(X0,X1)))),inverse(X2)))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f57,f2832])).
% 227.32/29.14 fof(f2906,plain,(
% 227.32/29.14 ![X0,X1,X2]: (divide(X0,X1)=multiply(multiply(sF0_fnc,divide(sF0_fnc,divide(X2,divide(X0,X1)))),X2))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f5,f2905])).
% 227.32/29.14 fof(f2950,plain,(
% 227.32/29.14 ![X0]: (X0=divide(multiply(sF2_fnc,divide(sF2_fnc,divide(b1,X0))),sF3_fnc))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f12,f2754])).
% 227.32/29.14 fof(f3010,plain,(
% 227.32/29.14 ![X0,X1]: (divide(sF1_fnc,multiply(divide(X0,X1),divide(divide(X1,X0),divide(a1,sF0_fnc))))=sF0_fnc)),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f7,f59])).
% 227.32/29.14 fof(f3277,plain,(
% 227.32/29.14 ![X0]: (inverse(X0)=divide(multiply(sF2_fnc,divide(sF2_fnc,multiply(b1,X0))),sF3_fnc))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f5,f2950])).
% 227.32/29.14 fof(f4119,plain,(
% 227.32/29.14 ![X0,X1]: (divide(multiply(sF2_fnc,divide(sF2_fnc,multiply(b1,X0))),sF3_fnc)=multiply(multiply(sF0_fnc,divide(sF0_fnc,divide(X1,inverse(X0)))),X1))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f3277,f2906])).
% 227.32/29.14 fof(f4121,plain,(
% 227.32/29.14 ![X0,X1]: (divide(multiply(sF2_fnc,divide(sF2_fnc,divide(b1,X0))),sF3_fnc)=multiply(multiply(sF0_fnc,divide(sF0_fnc,divide(X1,X0))),X1))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f2950,f2906])).
% 227.32/29.14 fof(f4174,plain,(
% 227.32/29.14 ![X0,X1]: (inverse(X0)=multiply(multiply(sF0_fnc,divide(sF0_fnc,divide(X1,inverse(X0)))),X1))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f3277,f4119])).
% 227.32/29.14 fof(f4175,plain,(
% 227.32/29.14 ![X0,X1]: (inverse(X0)=multiply(multiply(sF0_fnc,divide(sF0_fnc,multiply(X1,X0))),X1))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f5,f4174])).
% 227.32/29.14 fof(f4178,plain,(
% 227.32/29.14 ![X0,X1]: (X0=multiply(multiply(sF0_fnc,divide(sF0_fnc,divide(X1,X0))),X1))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f2950,f4121])).
% 227.32/29.14 fof(f5711,plain,(
% 227.32/29.14 ![X0,X1,X2]: (sF2_fnc=multiply(divide(divide(X0,X1),X2),divide(X2,divide(sF2_fnc,divide(X1,X0)))))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f716,f1902])).
% 227.32/29.14 fof(f6164,plain,(
% 227.32/29.14 ![X0,X1,X2]: (sF2_fnc=multiply(divide(multiply(X0,X1),X2),divide(X2,divide(sF2_fnc,divide(inverse(X1),X0)))))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f5,f5711])).
% 227.32/29.14 fof(f14386,plain,(
% 227.32/29.14 ![X0,X1,X2]: (divide(X0,X1)=multiply(divide(sF0_fnc,X2),divide(X2,divide(divide(X1,X0),sF0_fnc))))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f21,f104])).
% 227.32/29.14 fof(f14973,plain,(
% 227.32/29.14 ![X0,X1,X2,X3]: (divide(X0,X1)=multiply(divide(sF0_fnc,inverse(divide(sF0_fnc,divide(X2,multiply(divide(sF2_fnc,X3),divide(X3,divide(divide(X1,X0),sF2_fnc))))))),X2))),
% 227.32/29.14 inference(paramodulation,[status(thm)],[f44,f14386])).
% 227.32/29.14 fof(f15062,plain,(
% 227.32/29.14 ![X0,X1,X2,X3]: (divide(X0,X1)=multiply(multiply(sF0_fnc,divide(sF0_fnc,divide(X2,multiply(divide(sF2_fnc,X3),divide(X3,divide(divide(X1,X0),sF2_fnc)))))),X2))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f5,f14973])).
% 227.32/29.14 fof(f15063,plain,(
% 227.32/29.14 ![X0,X1,X2]: (divide(X0,X1)=multiply(divide(sF2_fnc,X2),divide(X2,divide(divide(X1,X0),sF2_fnc))))),
% 227.32/29.14 inference(forward_demodulation,[status(thm)],[f4178,f15062])).
% 227.32/29.14 fof(f15156,plain,(
% 227.32/29.14 ![X0,X1,X2]: (divide(X0,X1)=multiply(multiply(sF2_fnc,X2),divide(inverse(X2),divide(divide(X1,X0),sF2_fnc))))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f5,f15063])).
% 227.32/29.15 fof(f18395,plain,(
% 227.32/29.15 ![X0,X1,X2,X3]: (divide(multiply(sF2_fnc,divide(sF2_fnc,divide(b1,X0))),sF3_fnc)=multiply(multiply(divide(X1,X2),divide(divide(X2,X1),divide(X3,X0))),X3))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f2950,f108])).
% 227.32/29.15 fof(f18603,plain,(
% 227.32/29.15 ![X0,X1,X2,X3]: (X0=multiply(multiply(divide(X1,X2),divide(divide(X2,X1),divide(X3,X0))),X3))),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f2950,f18395])).
% 227.32/29.15 fof(f18683,plain,(
% 227.32/29.15 ![X0,X1,X2]: (X0=divide(multiply(divide(X1,X2),divide(divide(X2,X1),divide(a1,X0))),sF1_fnc))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f13,f18603])).
% 227.32/29.15 fof(f18752,plain,(
% 227.32/29.15 ![X0,X1,X2,X3]: (X0=multiply(multiply(multiply(X1,X2),divide(divide(inverse(X2),X1),divide(X3,X0))),X3))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f5,f18603])).
% 227.32/29.15 fof(f18817,plain,(
% 227.32/29.15 ![X0,X1,X2,X3]: (X0=multiply(multiply(divide(inverse(X1),X2),divide(multiply(X2,X1),divide(X3,X0))),X3))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f5,f18603])).
% 227.32/29.15 fof(f18834,plain,(
% 227.32/29.15 ![X0,X1]: (sF1_fnc=multiply(multiply(divide(X0,X1),divide(divide(X1,X0),sF0_fnc)),sF1_fnc))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f29,f18603])).
% 227.32/29.15 fof(f18841,plain,(
% 227.32/29.15 ![X0,X1]: (sF3_fnc=multiply(multiply(divide(X0,X1),divide(divide(X1,X0),sF2_fnc)),sF3_fnc))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f24,f18603])).
% 227.32/29.15 fof(f19757,plain,(
% 227.32/29.15 ![X0,X1,X2,X3,X4]: (sF1_fnc=multiply(multiply(divide(inverse(X0),X1),divide(divide(multiply(divide(X2,X3),divide(divide(X3,X2),divide(X4,multiply(X1,X0)))),inverse(X4)),sF0_fnc)),sF1_fnc))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f87,f18834])).
% 227.32/29.15 fof(f19894,plain,(
% 227.32/29.15 ![X0,X1,X2,X3,X4]: (sF1_fnc=multiply(multiply(divide(inverse(X0),X1),divide(multiply(multiply(divide(X2,X3),divide(divide(X3,X2),divide(X4,multiply(X1,X0)))),X4),sF0_fnc)),sF1_fnc))),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f5,f19757])).
% 227.32/29.15 fof(f19895,plain,(
% 227.32/29.15 ![X0,X1]: (sF1_fnc=multiply(multiply(divide(inverse(X0),X1),divide(multiply(X1,X0),sF0_fnc)),sF1_fnc))),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f18603,f19894])).
% 227.32/29.15 fof(f20042,plain,(
% 227.32/29.15 ![X0,X1]: (sF3_fnc=multiply(multiply(multiply(X0,X1),divide(divide(inverse(X1),X0),sF2_fnc)),sF3_fnc))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f5,f18841])).
% 227.32/29.15 fof(f24606,plain,(
% 227.32/29.15 ![X0,X1,X2,X3]: (multiply(divide(X0,X1),divide(divide(X1,X0),divide(a1,sF0_fnc)))=multiply(multiply(divide(inverse(X2),X3),divide(multiply(X3,X2),sF0_fnc)),sF1_fnc))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f3010,f18817])).
% 227.32/29.15 fof(f24869,plain,(
% 227.32/29.15 ![X0,X1]: (multiply(divide(X0,X1),divide(divide(X1,X0),divide(a1,sF0_fnc)))=sF1_fnc)),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f19895,f24606])).
% 227.32/29.15 fof(f25028,plain,(
% 227.32/29.15 ![X0,X1]: (multiply(multiply(X0,X1),divide(divide(inverse(X1),X0),divide(a1,sF0_fnc)))=sF1_fnc)),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f5,f24869])).
% 227.32/29.15 fof(f29128,plain,(
% 227.32/29.15 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,X1)),divide(X2,X0))=divide(inverse(divide(X3,X1)),divide(X2,X3)))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f159,f159])).
% 227.32/29.15 fof(f34169,plain,(
% 227.32/29.15 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0)),divide(X3,X2))=X1)),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f195,f60])).
% 227.32/29.15 fof(f36969,plain,(
% 227.32/29.15 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(X0,X1)),divide(sF2_fnc,X0)),divide(multiply(divide(X2,X3),divide(divide(X3,X2),divide(a1,sF2_fnc))),sF1_fnc))=X1)),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f1739,f34169])).
% 227.32/29.15 fof(f37125,plain,(
% 227.32/29.15 ![X0,X1,X2,X3]: (X0=multiply(multiply(multiply(divide(divide(X0,X1),X2),divide(X2,X3)),X3),X1))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f34169,f18752])).
% 227.32/29.15 fof(f37475,plain,(
% 227.32/29.15 ![X0,X1]: (divide(divide(inverse(divide(X0,X1)),divide(sF2_fnc,X0)),sF2_fnc)=X1)),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f18683,f36969])).
% 227.32/29.15 fof(f37864,plain,(
% 227.32/29.15 ![X0,X1]: (divide(divide(inverse(multiply(X0,X1)),divide(sF2_fnc,X0)),sF2_fnc)=inverse(X1))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f5,f37475])).
% 227.32/29.15 fof(f43694,plain,(
% 227.32/29.15 ![X0,X1,X2,X3]: (X0=multiply(multiply(multiply(multiply(divide(X0,X1),X2),divide(inverse(X2),X3)),X3),X1))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f5,f37125])).
% 227.32/29.15 fof(f44026,plain,(
% 227.32/29.15 ![X0,X1]: (sF3_fnc=multiply(multiply(multiply(divide(sF2_fnc,X0),multiply(X0,X1)),inverse(X1)),sF3_fnc))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f37864,f20042])).
% 227.32/29.15 fof(f141724,plain,(
% 227.32/29.15 ![X0,X1,X2,X3,X4]: (divide(divide(X0,X1),inverse(divide(X1,X2)))=multiply(multiply(sF2_fnc,X3),divide(inverse(X3),divide(divide(inverse(divide(X4,X2)),divide(X0,X4)),sF2_fnc))))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f29128,f15156])).
% 227.32/29.15 fof(f143195,plain,(
% 227.32/29.15 ![X0,X1,X2,X3,X4]: (multiply(divide(X0,X1),divide(X1,X2))=multiply(multiply(sF2_fnc,X3),divide(inverse(X3),divide(divide(inverse(divide(X4,X2)),divide(X0,X4)),sF2_fnc))))),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f5,f141724])).
% 227.32/29.15 fof(f143196,plain,(
% 227.32/29.15 ![X0,X1,X2,X3]: (multiply(divide(X0,X1),divide(X1,X2))=divide(divide(X0,X3),inverse(divide(X3,X2))))),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f15156,f143195])).
% 227.32/29.15 fof(f143197,plain,(
% 227.32/29.15 ![X0,X1,X2,X3]: (multiply(divide(X0,X1),divide(X1,X2))=multiply(divide(X0,X3),divide(X3,X2)))),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f5,f143196])).
% 227.32/29.15 fof(f144150,plain,(
% 227.32/29.15 ![X0,X1]: (multiply(sF2_fnc,divide(sF3_fnc,X0))=multiply(divide(sF3_fnc,X1),divide(X1,X0)))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f24,f143197])).
% 227.32/29.15 fof(f144301,plain,(
% 227.32/29.15 ![X0,X1]: (multiply(divide(X0,sF1_fnc),sF0_fnc)=multiply(divide(X0,X1),divide(X1,sF1_fnc)))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f29,f143197])).
% 227.32/29.15 fof(f166060,plain,(
% 227.32/29.15 ![X0,X1]: (multiply(divide(sF1_fnc,sF1_fnc),sF0_fnc)=multiply(sF2_fnc,divide(multiply(divide(X0,X1),divide(divide(X1,X0),divide(a1,sF2_fnc))),sF1_fnc)))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f1739,f144301])).
% 227.32/29.15 fof(f166061,plain,(
% 227.32/29.15 ![X0,X1,X2,X3]: (multiply(divide(sF1_fnc,sF1_fnc),sF0_fnc)=multiply(divide(X0,X1),divide(multiply(divide(X2,X3),divide(divide(X3,X2),divide(a1,divide(X1,X0)))),sF1_fnc)))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f63,f144301])).
% 227.32/29.15 fof(f166302,plain,(
% 227.32/29.15 ![X0,X1]: (multiply(sF0_fnc,sF0_fnc)=multiply(sF2_fnc,divide(multiply(divide(X0,X1),divide(divide(X1,X0),divide(a1,sF2_fnc))),sF1_fnc)))),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f29,f166060])).
% 227.32/29.15 fof(f166303,plain,(
% 227.32/29.15 multiply(sF0_fnc,sF0_fnc)=multiply(sF2_fnc,sF2_fnc)),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f18683,f166302])).
% 227.32/29.15 fof(f166304,plain,(
% 227.32/29.15 ![X0,X1,X2,X3]: (multiply(sF0_fnc,sF0_fnc)=multiply(divide(X0,X1),divide(multiply(divide(X2,X3),divide(divide(X3,X2),divide(a1,divide(X1,X0)))),sF1_fnc)))),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f29,f166061])).
% 227.32/29.15 fof(f166305,plain,(
% 227.32/29.15 ![X0,X1]: (multiply(sF0_fnc,sF0_fnc)=multiply(divide(X0,X1),divide(X1,X0)))),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f18683,f166304])).
% 227.32/29.15 fof(f170207,plain,(
% 227.32/29.15 ![X0,X1,X2,X3,X4]: (multiply(sF0_fnc,sF0_fnc)=multiply(divide(inverse(X0),X1),divide(multiply(divide(X2,X3),divide(divide(X3,X2),divide(X4,multiply(X1,X0)))),inverse(X4))))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f87,f166305])).
% 227.32/29.15 fof(f170220,plain,(
% 227.32/29.15 ![X0,X1]: (multiply(sF0_fnc,sF0_fnc)=multiply(multiply(X0,X1),divide(inverse(X1),X0)))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f5,f166305])).
% 227.32/29.15 fof(f170410,plain,(
% 227.32/29.15 ![X0,X1]: (X0=multiply(multiply(multiply(sF0_fnc,sF0_fnc),divide(X0,X1)),X1))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f166305,f37125])).
% 227.32/29.15 fof(f170615,plain,(
% 227.32/29.15 ![X0,X1,X2,X3,X4]: (multiply(sF0_fnc,sF0_fnc)=multiply(divide(inverse(X0),X1),multiply(multiply(divide(X2,X3),divide(divide(X3,X2),divide(X4,multiply(X1,X0)))),X4)))),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f5,f170207])).
% 227.32/29.15 fof(f170616,plain,(
% 227.32/29.15 ![X0,X1]: (multiply(sF0_fnc,sF0_fnc)=multiply(divide(inverse(X0),X1),multiply(X1,X0)))),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f18603,f170615])).
% 227.32/29.15 fof(f174067,plain,(
% 227.32/29.15 divide(inverse(sF0_fnc),sF0_fnc)=multiply(sF1_fnc,divide(a1,sF0_fnc))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f25028,f170410])).
% 227.32/29.15 fof(f174875,plain,(
% 227.32/29.15 ![X0,X1,X2]: (inverse(X0)=multiply(multiply(multiply(multiply(sF0_fnc,sF0_fnc),divide(inverse(multiply(X1,X0)),X2)),X2),X1))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f170616,f43694])).
% 227.32/29.15 fof(f174993,plain,(
% 227.32/29.15 ![X0,X1]: (inverse(X0)=multiply(inverse(multiply(X1,X0)),X1))),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f170410,f174875])).
% 227.32/29.15 fof(f175015,plain,(
% 227.32/29.15 inverse(sF2_fnc)=multiply(inverse(multiply(sF0_fnc,sF0_fnc)),sF2_fnc)),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f166303,f174993])).
% 227.32/29.15 fof(f175132,plain,(
% 227.32/29.15 ![X0,X1,X2]: (inverse(divide(inverse(X0),divide(divide(X1,multiply(sF2_fnc,X0)),sF2_fnc)))=multiply(inverse(divide(X2,X1)),X2))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f784,f174993])).
% 227.32/29.15 fof(f175222,plain,(
% 227.32/29.15 ![X0,X1]: (X0=multiply(inverse(divide(X1,X0)),X1))),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f703,f175132])).
% 227.32/29.15 fof(f175748,plain,(
% 227.32/29.15 ![X0]: (X0=divide(inverse(divide(a1,X0)),sF1_fnc))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f13,f175222])).
% 227.32/29.15 fof(f190210,plain,(
% 227.32/29.15 inverse(sF0_fnc)=multiply(multiply(sF0_fnc,sF0_fnc),sF0_fnc)),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f170220,f170410])).
% 227.32/29.15 fof(f196013,plain,(
% 227.32/29.15 ![X0,X1,X2]: (divide(inverse(X0),multiply(divide(inverse(X1),X2),divide(multiply(X2,X1),divide(X0,divide(inverse(sF0_fnc),sF0_fnc)))))=divide(inverse(divide(a1,sF0_fnc)),sF1_fnc))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f174067,f672])).
% 227.32/29.15 fof(f196078,plain,(
% 227.32/29.15 divide(sF0_fnc,inverse(sF0_fnc))=divide(inverse(divide(a1,sF0_fnc)),sF1_fnc)),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f77,f196013])).
% 227.32/29.15 fof(f196079,plain,(
% 227.32/29.15 multiply(sF0_fnc,sF0_fnc)=divide(inverse(divide(a1,sF0_fnc)),sF1_fnc)),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f5,f196078])).
% 227.32/29.15 fof(f196080,plain,(
% 227.32/29.15 multiply(sF0_fnc,sF0_fnc)=sF0_fnc),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f175748,f196079])).
% 227.32/29.15 fof(f196127,plain,(
% 227.32/29.15 inverse(sF0_fnc)=multiply(sF0_fnc,sF0_fnc)),
% 227.32/29.15 inference(backward_demodulation,[status(thm)],[f196080,f190210])).
% 227.32/29.15 fof(f196129,plain,(
% 227.32/29.15 inverse(sF2_fnc)=multiply(inverse(sF0_fnc),sF2_fnc)),
% 227.32/29.15 inference(backward_demodulation,[status(thm)],[f196080,f175015])).
% 227.32/29.15 fof(f196136,plain,(
% 227.32/29.15 sF0_fnc=multiply(sF2_fnc,sF2_fnc)),
% 227.32/29.15 inference(backward_demodulation,[status(thm)],[f196080,f166303])).
% 227.32/29.15 fof(f196154,plain,(
% 227.32/29.15 ![X0,X1,X2]: (divide(inverse(X0),multiply(divide(inverse(X1),X2),divide(multiply(X2,X1),divide(X0,sF0_fnc))))=divide(inverse(sF0_fnc),sF0_fnc))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f196080,f672])).
% 227.32/29.15 fof(f196210,plain,(
% 227.32/29.15 inverse(sF0_fnc)=sF0_fnc),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f196080,f196127])).
% 227.32/29.15 fof(f196211,plain,(
% 227.32/29.15 sF0_fnc=divide(inverse(sF0_fnc),sF0_fnc)),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f673,f196154])).
% 227.32/29.15 fof(f196237,plain,(
% 227.32/29.15 ![X0,X1,X2]: (divide(inverse(X0),multiply(divide(inverse(X1),X2),divide(multiply(X2,X1),divide(X0,sF0_fnc))))=divide(inverse(sF2_fnc),sF2_fnc))),
% 227.32/29.15 inference(paramodulation,[status(thm)],[f196136,f672])).
% 227.32/29.15 fof(f196299,plain,(
% 227.32/29.15 sF0_fnc=divide(inverse(sF2_fnc),sF2_fnc)),
% 227.32/29.15 inference(forward_demodulation,[status(thm)],[f673,f196237])).
% 227.32/29.15 fof(f196474,plain,(
% 227.32/29.15 ![X0]: (multiply(X0,sF0_fnc)=divide(X0,sF0_fnc))),
% 227.32/29.16 inference(paramodulation,[status(thm)],[f196210,f5])).
% 227.32/29.16 fof(f196644,plain,(
% 227.32/29.16 sF2_fnc=multiply(inverse(sF0_fnc),inverse(sF2_fnc))),
% 227.32/29.16 inference(paramodulation,[status(thm)],[f196299,f175222])).
% 227.32/29.16 fof(f197039,plain,(
% 227.32/29.16 sF2_fnc=multiply(sF0_fnc,inverse(sF2_fnc))),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f196210,f196644])).
% 227.32/29.16 fof(f197619,plain,(
% 227.32/29.16 sF0_fnc=divide(sF0_fnc,sF0_fnc)),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f196210,f196211])).
% 227.32/29.16 fof(f199098,plain,(
% 227.32/29.16 inverse(sF2_fnc)=multiply(sF0_fnc,sF2_fnc)),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f196210,f196129])).
% 227.32/29.16 fof(f199166,plain,(
% 227.32/29.16 inverse(sF2_fnc)=multiply(multiply(sF0_fnc,divide(sF0_fnc,inverse(sF2_fnc))),sF0_fnc)),
% 227.32/29.16 inference(paramodulation,[status(thm)],[f199098,f4175])).
% 227.32/29.16 fof(f199206,plain,(
% 227.32/29.16 inverse(sF2_fnc)=divide(multiply(sF0_fnc,divide(sF0_fnc,inverse(sF2_fnc))),sF0_fnc)),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f196474,f199166])).
% 227.32/29.16 fof(f199207,plain,(
% 227.32/29.16 inverse(sF2_fnc)=divide(multiply(sF0_fnc,multiply(sF0_fnc,sF2_fnc)),sF0_fnc)),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f5,f199206])).
% 227.32/29.16 fof(f199208,plain,(
% 227.32/29.16 inverse(sF2_fnc)=divide(multiply(sF0_fnc,inverse(sF2_fnc)),sF0_fnc)),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f199098,f199207])).
% 227.32/29.16 fof(f199209,plain,(
% 227.32/29.16 inverse(sF2_fnc)=divide(sF2_fnc,sF0_fnc)),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f197039,f199208])).
% 227.32/29.16 fof(f199265,plain,(
% 227.32/29.16 divide(inverse(sF2_fnc),multiply(sF2_fnc,divide(sF2_fnc,inverse(sF2_fnc))))=sF0_fnc),
% 227.32/29.16 inference(paramodulation,[status(thm)],[f199209,f58])).
% 227.32/29.16 fof(f199634,plain,(
% 227.32/29.16 divide(inverse(sF2_fnc),multiply(sF2_fnc,multiply(sF2_fnc,sF2_fnc)))=sF0_fnc),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f5,f199265])).
% 227.32/29.16 fof(f199635,plain,(
% 227.32/29.16 divide(inverse(sF2_fnc),multiply(sF2_fnc,sF0_fnc))=sF0_fnc),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f196136,f199634])).
% 227.32/29.16 fof(f199636,plain,(
% 227.32/29.16 divide(inverse(sF2_fnc),divide(sF2_fnc,sF0_fnc))=sF0_fnc),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f196474,f199635])).
% 227.32/29.16 fof(f199637,plain,(
% 227.32/29.16 divide(inverse(sF2_fnc),inverse(sF2_fnc))=sF0_fnc),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f199209,f199636])).
% 227.32/29.16 fof(f199638,plain,(
% 227.32/29.16 multiply(inverse(sF2_fnc),sF2_fnc)=sF0_fnc),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f5,f199637])).
% 227.32/29.16 fof(f200034,plain,(
% 227.32/29.16 inverse(sF2_fnc)=multiply(inverse(sF0_fnc),inverse(sF2_fnc))),
% 227.32/29.16 inference(paramodulation,[status(thm)],[f199638,f174993])).
% 227.32/29.16 fof(f200058,plain,(
% 227.32/29.16 sF3_fnc=multiply(multiply(multiply(divide(sF2_fnc,inverse(sF2_fnc)),sF0_fnc),inverse(sF2_fnc)),sF3_fnc)),
% 227.32/29.16 inference(paramodulation,[status(thm)],[f199638,f44026])).
% 227.32/29.16 fof(f200128,plain,(
% 227.32/29.16 inverse(sF2_fnc)=multiply(sF0_fnc,inverse(sF2_fnc))),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f196210,f200034])).
% 227.32/29.16 fof(f200129,plain,(
% 227.32/29.16 inverse(sF2_fnc)=sF2_fnc),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f197039,f200128])).
% 227.32/29.16 fof(f200182,plain,(
% 227.32/29.16 sF3_fnc=multiply(multiply(divide(divide(sF2_fnc,inverse(sF2_fnc)),sF0_fnc),inverse(sF2_fnc)),sF3_fnc)),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f196474,f200058])).
% 227.32/29.16 fof(f200183,plain,(
% 227.32/29.16 sF3_fnc=multiply(multiply(divide(multiply(sF2_fnc,sF2_fnc),sF0_fnc),inverse(sF2_fnc)),sF3_fnc)),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f5,f200182])).
% 227.32/29.16 fof(f200184,plain,(
% 227.32/29.16 sF3_fnc=multiply(multiply(divide(sF0_fnc,sF0_fnc),inverse(sF2_fnc)),sF3_fnc)),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f196136,f200183])).
% 227.32/29.16 fof(f200185,plain,(
% 227.32/29.16 sF3_fnc=multiply(multiply(sF0_fnc,inverse(sF2_fnc)),sF3_fnc)),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f197619,f200184])).
% 227.32/29.16 fof(f200186,plain,(
% 227.32/29.16 sF3_fnc=multiply(sF2_fnc,sF3_fnc)),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f197039,f200185])).
% 227.32/29.16 fof(f200271,plain,(
% 227.32/29.16 inverse(sF3_fnc)=multiply(inverse(sF3_fnc),sF2_fnc)),
% 227.32/29.16 inference(paramodulation,[status(thm)],[f200186,f174993])).
% 227.32/29.16 fof(f200337,plain,(
% 227.32/29.16 sF0_fnc=divide(sF2_fnc,sF2_fnc)),
% 227.32/29.16 inference(backward_demodulation,[status(thm)],[f200129,f196299])).
% 227.32/29.16 fof(f200465,plain,(
% 227.32/29.16 ![X0]: (multiply(X0,sF2_fnc)=divide(X0,sF2_fnc))),
% 227.32/29.16 inference(paramodulation,[status(thm)],[f200129,f5])).
% 227.32/29.16 fof(f219586,plain,(
% 227.32/29.16 inverse(sF3_fnc)=divide(inverse(sF3_fnc),sF2_fnc)),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f200465,f200271])).
% 227.32/29.16 fof(f219606,plain,(
% 227.32/29.16 ![X0]: (sF2_fnc=multiply(divide(multiply(sF2_fnc,sF3_fnc),X0),divide(X0,divide(sF2_fnc,inverse(sF3_fnc)))))),
% 227.32/29.16 inference(paramodulation,[status(thm)],[f219586,f6164])).
% 227.32/29.16 fof(f220022,plain,(
% 227.32/29.16 ![X0]: (sF2_fnc=multiply(divide(sF3_fnc,X0),divide(X0,divide(sF2_fnc,inverse(sF3_fnc)))))),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f200186,f219606])).
% 227.32/29.16 fof(f220023,plain,(
% 227.32/29.16 sF2_fnc=multiply(sF2_fnc,divide(sF3_fnc,divide(sF2_fnc,inverse(sF3_fnc))))),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f144150,f220022])).
% 227.32/29.16 fof(f220024,plain,(
% 227.32/29.16 sF2_fnc=multiply(sF2_fnc,divide(sF3_fnc,multiply(sF2_fnc,sF3_fnc)))),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f5,f220023])).
% 227.32/29.16 fof(f220025,plain,(
% 227.32/29.16 sF2_fnc=multiply(sF2_fnc,divide(sF3_fnc,sF3_fnc))),
% 227.32/29.16 inference(forward_demodulation,[status(thm)],[f200186,f220024])).
% 227.32/29.16 fof(f220026,plain,(
% 227.32/29.16 sF2_fnc=multiply(sF2_fnc,sF2_fnc)),
% 118.59/29.55 inference(forward_demodulation,[status(thm)],[f24,f220025])).
% 118.59/29.55 fof(f220027,plain,(
% 118.59/29.55 sF2_fnc=divide(sF2_fnc,sF2_fnc)),
% 118.59/29.55 inference(forward_demodulation,[status(thm)],[f200465,f220026])).
% 118.59/29.55 fof(f220028,plain,(
% 118.59/29.55 sF2_fnc=sF0_fnc),
% 118.59/29.55 inference(forward_demodulation,[status(thm)],[f200337,f220027])).
% 118.59/29.55 fof(f220029,plain,(
% 118.59/29.55 $false),
% 118.59/29.55 inference(forward_subsumption_resolution,[status(thm)],[f220028,f11])).
% 118.59/29.55 % SZS output end CNFRefutation for theBenchmark.p
% 19.47/29.65 % Elapsed time: 29.246398 seconds
% 19.47/29.65 % CPU time: 230.621343 seconds
% 19.47/29.65 % Total memory used: 1.464 GB
% 19.47/29.65 % Net memory used: 1.438 GB
%------------------------------------------------------------------------------