%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP501-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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:43 PM UTC 2026
% Result : Unsatisfiable 43.88s 5.99s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP501-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n020.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 20 20:16:04 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 43.88/5.99 % Refutation found
% 43.88/5.99 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 43.88/5.99 % SZS output start CNFRefutation for theBenchmark
% 43.88/5.99 fof(f1,axiom,(
% 43.88/5.99 (![A,B,C,D]: (double_divide(inverse(A),inverse(double_divide(inverse(double_divide(A,double_divide(B,C))),double_divide(D,double_divide(B,D))))) = C ))),
% 43.88/5.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 43.88/5.99 fof(f2,axiom,(
% 43.88/5.99 (![A,B]: (multiply(A,B) = inverse(double_divide(B,A)) ))),
% 43.88/5.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 43.88/5.99 fof(f3,negated_conjecture,(
% 43.88/5.99 multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
% 43.88/5.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 43.88/5.99 fof(f4,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (double_divide(inverse(X0),inverse(double_divide(inverse(double_divide(X0,double_divide(X1,X2))),double_divide(X3,double_divide(X1,X3)))))=X2)),
% 43.88/5.99 inference(cnf_transformation,[status(thm)],[f1])).
% 43.88/5.99 fof(f5,plain,(
% 43.88/5.99 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X1,X0)))),
% 43.88/5.99 inference(cnf_transformation,[status(thm)],[f2])).
% 43.88/5.99 fof(f6,plain,(
% 43.88/5.99 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 43.88/5.99 inference(cnf_transformation,[status(thm)],[f3])).
% 43.88/5.99 fof(f12,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(X2,X1)),inverse(double_divide(X0,double_divide(X2,X3)))))=X3)),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f5,f4])).
% 43.88/5.99 fof(f13,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(X2,X1)),multiply(double_divide(X2,X3),X0)))=X3)),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5,f12])).
% 43.88/5.99 fof(f14,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4]: (double_divide(multiply(X0,X1),multiply(double_divide(X2,double_divide(X3,X2)),multiply(double_divide(X3,X4),double_divide(X1,X0))))=X4)),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f5,f13])).
% 43.88/5.99 fof(f15,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(X0),multiply(double_divide(multiply(double_divide(X1,double_divide(X2,X1)),multiply(double_divide(X2,X3),X4)),X3),multiply(double_divide(inverse(X4),X5),X0)))=X5)),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f13,f13])).
% 43.88/5.99 fof(f16,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(X3,X0)))=multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,X3),X2)))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f13,f13])).
% 43.88/5.99 fof(f17,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(multiply(double_divide(X0,double_divide(X1,X0)),multiply(double_divide(X1,X2),X3)),inverse(X3))=inverse(X2))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f13,f5])).
% 43.88/5.99 fof(f19,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(X2,X3)),inverse(X3))=inverse(multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,X2),X1))))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f13,f17])).
% 43.88/5.99 fof(f20,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4]: (multiply(multiply(double_divide(X0,double_divide(X1,X0)),multiply(double_divide(X1,X2),double_divide(X3,X4))),multiply(X4,X3))=inverse(X2))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f5,f17])).
% 43.88/5.99 fof(f22,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (double_divide(multiply(X0,X1),multiply(double_divide(multiply(double_divide(X2,double_divide(X3,X2)),multiply(double_divide(X3,X4),double_divide(X5,X6))),X4),multiply(double_divide(multiply(X6,X5),X7),double_divide(X1,X0))))=X7)),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f14,f14])).
% 43.88/5.99 fof(f23,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6]: (double_divide(multiply(X0,X1),multiply(double_divide(multiply(double_divide(X2,double_divide(X3,X2)),multiply(double_divide(X3,X4),X5)),X4),multiply(double_divide(inverse(X5),X6),double_divide(X1,X0))))=X6)),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f13,f14])).
% 43.88/5.99 fof(f74,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (X0=multiply(double_divide(X1,double_divide(X2,X1)),multiply(double_divide(X2,double_divide(inverse(X3),X0)),X3)))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f13,f16])).
% 43.88/5.99 fof(f76,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6]: (double_divide(inverse(X0),double_divide(inverse(X1),multiply(double_divide(X2,double_divide(inverse(X0),X2)),multiply(X3,X1))))=multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,double_divide(inverse(X6),X3)),X6)))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f16,f16])).
% 43.88/5.99 fof(f120,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (double_divide(inverse(X0),double_divide(inverse(X1),multiply(double_divide(X2,double_divide(inverse(X0),X2)),multiply(X3,X1))))=X3)),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f74,f76])).
% 43.88/5.99 fof(f145,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4]: (double_divide(inverse(multiply(double_divide(X0,double_divide(inverse(X1),X2)),X1)),multiply(double_divide(X3,double_divide(X4,X3)),X2))=double_divide(X0,X4))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f74,f13])).
% 43.88/5.99 fof(f163,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(X0),double_divide(inverse(multiply(double_divide(X1,double_divide(inverse(X2),X3)),X2)),multiply(double_divide(X4,double_divide(inverse(X0),X4)),X3)))=double_divide(X5,double_divide(X1,X5)))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f74,f120])).
% 43.88/5.99 fof(f189,plain,(
% 43.88/5.99 ![X0,X1,X2]: (double_divide(inverse(X0),double_divide(X1,inverse(X0)))=double_divide(X2,double_divide(X1,X2)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f145,f163])).
% 43.88/5.99 fof(f195,plain,(
% 43.88/5.99 ![X0,X1,X2]: (double_divide(X0,double_divide(X1,X0))=double_divide(X2,double_divide(X1,X2)))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f189,f189])).
% 43.88/5.99 fof(f283,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (double_divide(double_divide(X0,X1),double_divide(X2,double_divide(X0,X2)))=double_divide(X3,double_divide(X1,X3)))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f195,f195])).
% 43.88/5.99 fof(f299,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (X0=multiply(double_divide(X1,double_divide(X0,X1)),multiply(double_divide(X2,double_divide(inverse(X3),X2)),X3)))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f195,f74])).
% 43.88/5.99 fof(f323,plain,(
% 43.88/5.99 ![X0,X1,X2]: (multiply(double_divide(X0,X1),X1)=inverse(double_divide(X2,double_divide(X0,X2))))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f195,f5])).
% 43.88/5.99 fof(f384,plain,(
% 43.88/5.99 ![X0,X1,X2]: (multiply(double_divide(X0,X1),X1)=multiply(double_divide(X0,X2),X2))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5,f323])).
% 43.88/5.99 fof(f395,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,X2))=multiply(double_divide(X2,X3),X3))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f195,f384])).
% 43.88/5.99 fof(f413,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(X2,X1)),multiply(double_divide(X2,X3),X3)))=X0)),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f384,f13])).
% 43.88/5.99 fof(f519,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4]: (double_divide(X0,inverse(X1))=multiply(double_divide(X2,double_divide(double_divide(X0,X3),X2)),multiply(double_divide(X4,double_divide(X3,X4)),X1)))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f283,f74])).
% 43.88/5.99 fof(f578,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(double_divide(X3,X4),X0)))=multiply(double_divide(X5,double_divide(X4,X5)),multiply(double_divide(double_divide(X6,X3),double_divide(X7,double_divide(X6,X7))),X2)))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f283,f16])).
% 43.88/5.99 fof(f627,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(double_divide(X0,double_divide(inverse(X1),X0)),X2)=multiply(double_divide(multiply(double_divide(multiply(double_divide(X3,double_divide(X4,X3)),multiply(double_divide(X4,X5),X6)),X5),multiply(double_divide(inverse(X6),X2),X1)),X7),X7))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f15,f395])).
% 43.88/5.99 fof(f629,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(X0,double_divide(inverse(X1),X0)),X2)=multiply(double_divide(multiply(double_divide(X3,double_divide(X4,X3)),multiply(double_divide(X4,X2),X1)),X5),X5))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f13,f395])).
% 43.88/5.99 fof(f770,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(double_divide(X2,X3),X1)),multiply(double_divide(X4,double_divide(X3,X4)),double_divide(X5,double_divide(X2,X5)))))=X0)),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f283,f413])).
% 43.88/5.99 fof(f818,plain,(
% 43.88/5.99 ![X0,X1,X2]: (double_divide(inverse(X0),double_divide(X1,inverse(double_divide(X2,double_divide(X1,X2)))))=X0)),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f519,f770])).
% 43.88/5.99 fof(f819,plain,(
% 43.88/5.99 ![X0,X1,X2]: (double_divide(inverse(X0),double_divide(X1,multiply(double_divide(X1,X2),X2)))=X0)),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5,f818])).
% 43.88/5.99 fof(f824,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (double_divide(multiply(X0,X1),double_divide(X2,multiply(double_divide(X2,X3),X3)))=double_divide(X1,X0))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f5,f819])).
% 43.88/5.99 fof(f826,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (double_divide(inverse(X0),double_divide(X1,multiply(double_divide(X2,double_divide(X3,X2)),double_divide(X3,X1))))=X0)),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f395,f819])).
% 43.88/5.99 fof(f846,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(double_divide(inverse(X0),X1),X1)=multiply(double_divide(X2,double_divide(inverse(X3),X2)),multiply(X3,X0)))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f819,f74])).
% 43.88/5.99 fof(f850,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4]: (multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,inverse(X2)))=multiply(X2,double_divide(X3,multiply(double_divide(X3,X4),X4))))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f819,f395])).
% 43.88/5.99 fof(f858,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(double_divide(inverse(X0),X1),X1)=multiply(X0,double_divide(X2,multiply(double_divide(X2,X3),X3))))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f819,f384])).
% 43.88/5.99 fof(f860,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (double_divide(X0,double_divide(inverse(X1),X0))=double_divide(double_divide(X2,multiply(double_divide(X2,X3),X3)),X1))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f819,f195])).
% 43.88/5.99 fof(f877,plain,(
% 43.88/5.99 ![X0,X1,X2]: (multiply(double_divide(X0,multiply(double_divide(X0,X1),X1)),inverse(X2))=inverse(X2))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f819,f5])).
% 43.88/5.99 fof(f900,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(double_divide(X0,multiply(double_divide(X0,X1),X1)),multiply(X2,X3))=inverse(double_divide(X3,X2)))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f5,f877])).
% 43.88/5.99 fof(f912,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(double_divide(X0,multiply(double_divide(X0,X1),X1)),multiply(X2,X3))=multiply(X2,X3))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5,f900])).
% 43.88/5.99 fof(f1088,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,multiply(X2,X3)))=multiply(double_divide(X3,X2),double_divide(X4,multiply(double_divide(X4,X5),X5))))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f824,f395])).
% 43.88/5.99 fof(f1156,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(X0,multiply(double_divide(X0,X1),X1)),X2)=multiply(double_divide(X3,double_divide(X2,X3)),multiply(double_divide(X4,double_divide(inverse(X5),X4)),X5)))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f299,f912])).
% 43.88/5.99 fof(f1196,plain,(
% 43.88/5.99 ![X0,X1,X2]: (multiply(double_divide(X0,multiply(double_divide(X0,X1),X1)),X2)=X2)),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f299,f1156])).
% 43.88/5.99 fof(f1214,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(double_divide(X0,multiply(double_divide(X1,double_divide(X2,X1)),double_divide(X2,X0))),X3)=X3)),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f395,f1196])).
% 43.88/5.99 fof(f1244,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(X2,X1)),X0))=multiply(double_divide(X2,X3),X3))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f1196,f13])).
% 43.88/5.99 fof(f1384,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4]: (multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,inverse(X2)))=multiply(double_divide(X3,double_divide(inverse(X4),X3)),multiply(X4,X2)))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f826,f74])).
% 43.88/5.99 fof(f1390,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(X2,X3)),inverse(X3))=inverse(multiply(double_divide(double_divide(X4,multiply(double_divide(X5,double_divide(X6,X5)),double_divide(X6,X4))),X7),multiply(double_divide(inverse(X7),X2),X1))))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f826,f19])).
% 43.88/5.99 fof(f1519,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (multiply(multiply(double_divide(X0,double_divide(X1,X0)),multiply(double_divide(inverse(double_divide(X1,X2)),X3),X3)),multiply(multiply(double_divide(X4,X5),X5),X4))=inverse(X2))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f858,f20])).
% 43.88/5.99 fof(f1523,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(multiply(double_divide(X0,double_divide(inverse(double_divide(X1,multiply(double_divide(X1,X2),X2))),X0)),multiply(X3,X4)),inverse(X4))=inverse(multiply(double_divide(X5,double_divide(X6,X5)),multiply(double_divide(inverse(double_divide(X6,X3)),X7),X7))))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f858,f19])).
% 43.88/5.99 fof(f1570,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (multiply(multiply(double_divide(X0,double_divide(X1,X0)),multiply(double_divide(multiply(X2,X1),X3),X3)),multiply(multiply(double_divide(X4,X5),X5),X4))=inverse(X2))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5,f1519])).
% 43.88/5.99 fof(f1576,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(multiply(double_divide(X0,double_divide(multiply(multiply(double_divide(X1,X2),X2),X1),X0)),multiply(X3,X4)),inverse(X4))=inverse(multiply(double_divide(X5,double_divide(X6,X5)),multiply(double_divide(inverse(double_divide(X6,X3)),X7),X7))))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5,f1523])).
% 43.88/5.99 fof(f1577,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(multiply(double_divide(X0,double_divide(multiply(multiply(double_divide(X1,X2),X2),X1),X0)),multiply(X3,X4)),inverse(X4))=inverse(multiply(double_divide(X5,double_divide(X6,X5)),multiply(double_divide(multiply(X3,X6),X7),X7))))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5,f1576])).
% 43.88/5.99 fof(f1680,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (double_divide(multiply(X0,X1),multiply(double_divide(multiply(double_divide(X2,double_divide(X3,X2)),multiply(double_divide(X3,X4),double_divide(X5,X6))),X4),double_divide(X1,X0)))=multiply(double_divide(multiply(X6,X5),X7),X7))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f1196,f22])).
% 43.88/5.99 fof(f1735,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (multiply(double_divide(X0,double_divide(multiply(X1,X2),X0)),X3)=multiply(double_divide(multiply(double_divide(multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,X6),double_divide(X7,X8))),X6),multiply(double_divide(multiply(X8,X7),X3),double_divide(X2,X1))),X9),X9))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f22,f395])).
% 43.88/5.99 fof(f1757,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (multiply(multiply(double_divide(X0,double_divide(multiply(X1,X2),X0)),multiply(X3,X4)),inverse(X4))=inverse(multiply(double_divide(multiply(double_divide(X5,double_divide(X6,X5)),multiply(double_divide(X6,X7),double_divide(X8,X9))),X7),multiply(double_divide(multiply(X9,X8),X3),double_divide(X2,X1)))))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f22,f17])).
% 43.88/5.99 fof(f1808,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (double_divide(double_divide(X0,multiply(double_divide(X1,double_divide(X2,X1)),double_divide(X2,X0))),X3)=double_divide(double_divide(X4,multiply(double_divide(X4,X5),X5)),X3))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f826,f860])).
% 43.88/5.99 fof(f1974,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(X2,X3)),inverse(X3))=inverse(multiply(double_divide(X4,double_divide(X5,double_divide(inverse(X4),X5))),multiply(double_divide(double_divide(X6,multiply(double_divide(X6,X7),X7)),X2),X1))))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f860,f19])).
% 43.88/5.99 fof(f1993,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(X3,X0)))=multiply(double_divide(X4,double_divide(X5,double_divide(inverse(X4),X5))),multiply(double_divide(double_divide(X6,multiply(double_divide(X6,X7),X7)),X3),X2)))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f860,f16])).
% 43.88/5.99 fof(f2003,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (multiply(multiply(double_divide(X0,double_divide(X1,double_divide(inverse(X0),X1))),multiply(double_divide(double_divide(X2,multiply(double_divide(X2,X3),X3)),X4),X5)),inverse(X5))=inverse(X4))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f860,f17])).
% 43.88/5.99 fof(f2171,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (double_divide(inverse(double_divide(X0,X1)),multiply(double_divide(X1,X2),X2))=multiply(double_divide(X0,X3),X3))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f395,f1244])).
% 43.88/5.99 fof(f2331,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (double_divide(multiply(X0,X1),multiply(double_divide(X0,X2),X2))=multiply(double_divide(X1,X3),X3))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5,f2171])).
% 43.88/5.99 fof(f2488,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(double_divide(X0,double_divide(multiply(X1,X0),multiply(double_divide(X1,X2),X2))),X3)=X3)),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f2331,f1214])).
% 43.88/5.99 fof(f2533,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(double_divide(X0,X1),X1)=double_divide(multiply(X2,multiply(double_divide(X2,X3),X3)),X0))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f395,f2488])).
% 43.88/5.99 fof(f2543,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(X0,double_divide(inverse(double_divide(multiply(X1,double_divide(X2,multiply(double_divide(X2,X3),X3))),multiply(double_divide(X1,X4),X4))),X0)),X5)=X5)),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f860,f2488])).
% 43.88/5.99 fof(f2545,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(double_divide(X0,double_divide(multiply(X1,multiply(double_divide(X1,X2),X2)),X0)),X3)=X3)),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f195,f2488])).
% 43.88/5.99 fof(f2651,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(X0,double_divide(multiply(multiply(double_divide(X1,X2),X2),multiply(X1,double_divide(X3,multiply(double_divide(X3,X4),X4)))),X0)),X5)=X5)),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5,f2543])).
% 43.88/5.99 fof(f2695,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(multiply(double_divide(X0,double_divide(X1,X0)),multiply(double_divide(X1,X2),double_divide(multiply(double_divide(X3,X4),X4),X3))),X5),X5)=X2)),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f14,f2533])).
% 43.88/5.99 fof(f2831,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(multiply(X2,multiply(double_divide(X2,X3),X3)),X1)),X0))=multiply(multiply(double_divide(X4,X5),X5),X4))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f2533,f1244])).
% 43.88/5.99 fof(f2839,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(inverse(X0),X1),X1)=multiply(X0,double_divide(multiply(X2,multiply(double_divide(X2,X3),X3)),multiply(multiply(double_divide(X4,X5),X5),X4))))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f2533,f858])).
% 43.88/5.99 fof(f2849,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(multiply(X2,multiply(double_divide(X2,X3),X3)),X1)),multiply(multiply(double_divide(X4,X5),X5),X4)))=X0)),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f2533,f413])).
% 43.88/5.99 fof(f2894,plain,(
% 43.88/5.99 ![X0,X1,X2]: (double_divide(inverse(X0),X0)=multiply(multiply(double_divide(X1,X2),X2),X1))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f2545,f2831])).
% 43.88/5.99 fof(f2904,plain,(
% 43.88/5.99 ![X0,X1,X2]: (double_divide(inverse(X0),multiply(multiply(double_divide(X1,X2),X2),X1))=X0)),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f2545,f2849])).
% 43.88/5.99 fof(f3025,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (double_divide(multiply(X0,X1),multiply(double_divide(multiply(double_divide(X2,double_divide(X3,X2)),multiply(double_divide(X3,X4),X5)),X4),double_divide(X1,X0)))=multiply(double_divide(X6,double_divide(X7,X6)),double_divide(X7,inverse(X5))))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f1214,f23])).
% 43.88/5.99 fof(f3121,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (multiply(multiply(double_divide(X0,double_divide(multiply(X1,X2),X0)),multiply(X3,X4)),inverse(X4))=inverse(multiply(double_divide(multiply(double_divide(X5,double_divide(X6,X5)),multiply(double_divide(X6,X7),X8)),X7),multiply(double_divide(inverse(X8),X3),double_divide(X2,X1)))))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f23,f17])).
% 43.88/5.99 fof(f3286,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4]: (multiply(double_divide(X0,multiply(double_divide(X1,double_divide(inverse(X0),X1)),multiply(multiply(double_divide(X2,X3),X3),X2))),X4)=X4)),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f2894,f1214])).
% 43.88/5.99 fof(f3321,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(multiply(multiply(double_divide(X3,X4),X4),X3),X0)))=X2)),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f2894,f13])).
% 43.88/5.99 fof(f3335,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (multiply(multiply(double_divide(X0,double_divide(X1,X0)),multiply(double_divide(X1,X2),double_divide(X3,multiply(double_divide(X3,X4),X4)))),double_divide(inverse(X5),X5))=inverse(X2))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f2894,f20])).
% 43.88/5.99 fof(f3616,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (double_divide(multiply(X0,X1),multiply(multiply(double_divide(X2,X3),X3),X2))=double_divide(X1,X0))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f5,f2904])).
% 43.88/5.99 fof(f3665,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4]: (X0=multiply(double_divide(X1,double_divide(X0,X1)),multiply(double_divide(multiply(multiply(double_divide(X2,X3),X3),X2),X4),X4)))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f2904,f299])).
% 43.88/5.99 fof(f3688,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4]: (multiply(double_divide(inverse(X0),X1),X1)=multiply(X0,double_divide(inverse(X2),multiply(X2,multiply(multiply(double_divide(X3,X4),X4),X3)))))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f2904,f858])).
% 43.88/5.99 fof(f3701,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4]: (multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,inverse(X2)))=multiply(X2,multiply(multiply(double_divide(X3,X4),X4),X3)))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f2904,f395])).
% 43.88/5.99 fof(f3714,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(multiply(multiply(double_divide(X3,X4),X4),X3),X0)))=multiply(double_divide(X5,double_divide(inverse(X6),X5)),multiply(X6,X2)))),
% 43.88/5.99 inference(paramodulation,[status(thm)],[f2904,f16])).
% 43.88/5.99 fof(f3735,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(double_divide(inverse(X0),X1),X1)=multiply(X0,double_divide(multiply(double_divide(X2,X3),X3),X2)))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f3616,f2839])).
% 43.88/5.99 fof(f3775,plain,(
% 43.88/5.99 ![X0,X1,X2]: (multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,inverse(X2)))=X2)),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f3786,f1384])).
% 43.88/5.99 fof(f3780,plain,(
% 43.88/5.99 ![X0,X1]: (multiply(double_divide(inverse(X0),X1),X1)=X0)),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f3786,f846])).
% 43.88/5.99 fof(f3786,plain,(
% 43.88/5.99 ![X0,X1,X2]: (X0=multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(X2,X0)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f3321,f3714])).
% 43.88/5.99 fof(f3806,plain,(
% 43.88/5.99 ![X0,X1,X2]: (X0=multiply(X0,multiply(multiply(double_divide(X1,X2),X2),X1)))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f3775,f3701])).
% 43.88/5.99 fof(f3810,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (double_divide(multiply(X0,X1),multiply(double_divide(multiply(double_divide(X2,double_divide(X3,X2)),multiply(double_divide(X3,X4),X5)),X4),double_divide(X1,X0)))=X5)),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f3775,f3025])).
% 43.88/5.99 fof(f3815,plain,(
% 43.88/5.99 ![X0,X1,X2]: (X0=multiply(X0,double_divide(X1,multiply(double_divide(X1,X2),X2))))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f3775,f850])).
% 43.88/5.99 fof(f3850,plain,(
% 43.88/5.99 ![X0,X1,X2]: (X0=multiply(X0,double_divide(multiply(double_divide(X1,X2),X2),X1)))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f3780,f3735])).
% 43.88/5.99 fof(f3853,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (X0=multiply(X0,double_divide(inverse(X1),multiply(X1,multiply(multiply(double_divide(X2,X3),X3),X2)))))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f3780,f3688])).
% 43.88/5.99 fof(f3930,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(double_divide(X0,double_divide(X1,X0)),multiply(double_divide(multiply(X2,X1),X3),X3))=inverse(X2))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f3806,f1570])).
% 43.88/5.99 fof(f3935,plain,(
% 43.88/5.99 ![X0,X1,X2]: (multiply(double_divide(X0,double_divide(X1,double_divide(inverse(X0),X1))),X2)=X2)),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f3806,f3286])).
% 43.88/5.99 fof(f4013,plain,(
% 43.88/5.99 ![X0,X1,X2]: (double_divide(X0,X1)=multiply(double_divide(multiply(X1,X0),X2),X2))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f3810,f1680])).
% 43.88/5.99 fof(f4057,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,X2)),double_divide(inverse(X3),X3))=inverse(X2))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f3815,f3335])).
% 43.88/5.99 fof(f4070,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,multiply(X2,X3)))=double_divide(X3,X2))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f3815,f1088])).
% 43.88/5.99 fof(f4089,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(double_divide(X0,double_divide(multiply(multiply(double_divide(X1,X2),X2),X1),X0)),X3)=X3)),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f3815,f2651])).
% 43.88/5.99 fof(f4238,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(double_divide(multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,X2)),X3),X3)=X2)),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f3850,f2695])).
% 43.88/5.99 fof(f4251,plain,(
% 43.88/5.99 ![X0,X1]: (X0=multiply(X0,double_divide(inverse(X1),X1)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f3806,f3853])).
% 43.88/5.99 fof(f4291,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4]: (multiply(multiply(double_divide(X0,double_divide(multiply(multiply(double_divide(X1,X2),X2),X1),X0)),multiply(X3,X4)),inverse(X4))=inverse(inverse(X3)))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f3930,f1577])).
% 43.88/5.99 fof(f4302,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(multiply(double_divide(double_divide(X0,multiply(double_divide(X0,X1),X1)),X2),X3),inverse(X3))=inverse(X2))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f3935,f2003])).
% 43.88/5.99 fof(f4304,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(X3,X0)))=multiply(double_divide(double_divide(X4,multiply(double_divide(X4,X5),X5)),X3),X2))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f3935,f1993])).
% 43.88/5.99 fof(f4307,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(X2,X3)),inverse(X3))=inverse(multiply(double_divide(double_divide(X4,multiply(double_divide(X4,X5),X5)),X2),X1)))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f3935,f1974])).
% 43.88/5.99 fof(f4337,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (X0=multiply(double_divide(X1,double_divide(X0,X1)),double_divide(X2,multiply(double_divide(X2,X3),X3))))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f4013,f3665])).
% 43.88/5.99 fof(f4343,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (multiply(double_divide(X0,double_divide(multiply(X1,X2),X0)),X3)=double_divide(multiply(double_divide(multiply(X4,X5),X3),double_divide(X2,X1)),double_divide(multiply(double_divide(X6,double_divide(X7,X6)),multiply(double_divide(X7,X8),double_divide(X5,X4))),X8)))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f4013,f1735])).
% 43.88/5.99 fof(f4346,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(double_divide(X0,double_divide(inverse(X1),X0)),X2)=double_divide(multiply(double_divide(inverse(X3),X2),X1),double_divide(multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,X6),X3)),X6)))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f4013,f627])).
% 43.88/5.99 fof(f4373,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4]: (multiply(double_divide(X0,double_divide(inverse(X1),X0)),X2)=double_divide(multiply(double_divide(X3,X2),X1),double_divide(X4,double_divide(X3,X4))))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f4013,f629])).
% 43.88/5.99 fof(f4455,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (double_divide(double_divide(X0,inverse(X0)),X1)=double_divide(double_divide(X2,multiply(double_divide(X2,X3),X3)),X1))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f4515,f1808])).
% 43.88/5.99 fof(f4478,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(X2,X3)),inverse(X3))=inverse(multiply(double_divide(double_divide(X4,inverse(X4)),X5),multiply(double_divide(inverse(X5),X2),X1))))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f4515,f1390])).
% 43.88/5.99 fof(f4515,plain,(
% 43.88/5.99 ![X0,X1,X2]: (multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,X2))=inverse(X2))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f4251,f4057])).
% 43.88/5.99 fof(f4557,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (multiply(multiply(double_divide(X0,double_divide(multiply(X1,X2),X0)),multiply(X3,X4)),inverse(X4))=double_divide(multiply(double_divide(multiply(X5,X6),X3),double_divide(X2,X1)),double_divide(multiply(double_divide(X7,double_divide(X8,X7)),multiply(double_divide(X8,X9),double_divide(X6,X5))),X9)))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f4685,f1757])).
% 43.88/5.99 fof(f4560,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (multiply(multiply(double_divide(X0,double_divide(multiply(X1,X2),X0)),multiply(X3,X4)),inverse(X4))=double_divide(multiply(double_divide(inverse(X5),X3),double_divide(X2,X1)),double_divide(multiply(double_divide(X6,double_divide(X7,X6)),multiply(double_divide(X7,X8),X5)),X8)))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f4685,f3121])).
% 43.88/5.99 fof(f4685,plain,(
% 43.88/5.99 ![X0,X1]: (inverse(multiply(X0,X1))=double_divide(X1,X0))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f4515,f4070])).
% 43.88/5.99 fof(f4794,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(double_divide(X3,X4),X0)))=multiply(double_divide(X5,double_divide(X4,X5)),multiply(X3,X2)))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f4817,f578])).
% 43.88/5.99 fof(f4817,plain,(
% 43.88/5.99 ![X0,X1,X2]: (double_divide(double_divide(X0,X1),double_divide(X2,double_divide(X0,X2)))=X1)),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f4013,f4238])).
% 43.88/5.99 fof(f4891,plain,(
% 43.88/5.99 ![X0,X1]: (multiply(multiply(X0,X1),inverse(X1))=inverse(inverse(X0)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f4089,f4291])).
% 43.88/5.99 fof(f4902,plain,(
% 43.88/5.99 ![X0,X1,X2]: (inverse(inverse(double_divide(double_divide(X0,multiply(double_divide(X0,X1),X1)),X2)))=inverse(X2))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f4891,f4302])).
% 43.88/5.99 fof(f4903,plain,(
% 43.88/5.99 ![X0,X1,X2]: (inverse(multiply(X0,double_divide(X1,multiply(double_divide(X1,X2),X2))))=inverse(X0))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5,f4902])).
% 43.88/5.99 fof(f5035,plain,(
% 43.88/5.99 ![X0,X1,X2]: (double_divide(double_divide(X0,multiply(double_divide(X0,X1),X1)),X2)=inverse(X2))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f4685,f4903])).
% 43.88/5.99 fof(f5109,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(X3,X0)))=multiply(inverse(X3),X2))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5035,f4304])).
% 43.88/5.99 fof(f5112,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(X2,X3)),inverse(X3))=double_divide(X1,double_divide(double_divide(X4,multiply(double_divide(X4,X5),X5)),X2)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f4685,f4307])).
% 43.88/5.99 fof(f5137,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(X2,X3)),inverse(X3))=double_divide(X1,inverse(X2)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5035,f5112])).
% 43.88/5.99 fof(f5835,plain,(
% 43.88/5.99 ![X0,X1]: (X0=double_divide(X1,double_divide(X0,X1)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f3815,f4337])).
% 43.88/5.99 fof(f5847,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(multiply(X0,X1),X2)=double_divide(multiply(double_divide(multiply(X3,X4),X2),double_divide(X1,X0)),double_divide(multiply(double_divide(X5,double_divide(X6,X5)),multiply(double_divide(X6,X7),double_divide(X4,X3))),X7)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5835,f4343])).
% 43.88/5.99 fof(f5848,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(multiply(X0,X1),X2)=double_divide(multiply(double_divide(multiply(X3,X4),X2),double_divide(X1,X0)),double_divide(multiply(X5,multiply(double_divide(X5,X6),double_divide(X4,X3))),X6)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5835,f5847])).
% 43.88/5.99 fof(f5852,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(X0),X1)=double_divide(multiply(double_divide(inverse(X2),X1),X0),double_divide(multiply(double_divide(X3,double_divide(X4,X3)),multiply(double_divide(X4,X5),X2)),X5)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5835,f4346])).
% 43.88/5.99 fof(f5855,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),X1)=double_divide(multiply(double_divide(inverse(X2),X1),X0),double_divide(multiply(X3,multiply(double_divide(X3,X4),X2)),X4)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5835,f5852])).
% 43.88/5.99 fof(f5920,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(inverse(X0),X1)=double_divide(multiply(double_divide(X2,X1),X0),double_divide(X3,double_divide(X2,X3))))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5835,f4373])).
% 43.88/5.99 fof(f5927,plain,(
% 43.88/5.99 ![X0,X1,X2]: (multiply(inverse(X0),X1)=double_divide(multiply(double_divide(X2,X1),X0),X2))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5835,f5920])).
% 43.88/5.99 fof(f6052,plain,(
% 43.88/5.99 ![X0,X1]: (double_divide(double_divide(X0,inverse(X0)),X1)=inverse(X1))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5035,f4455])).
% 43.88/5.99 fof(f6096,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (double_divide(X0,inverse(X1))=inverse(multiply(double_divide(double_divide(X2,inverse(X2)),X3),multiply(double_divide(inverse(X3),X1),X0))))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5137,f4478])).
% 43.88/5.99 fof(f6097,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (double_divide(X0,inverse(X1))=double_divide(multiply(double_divide(inverse(X2),X1),X0),double_divide(double_divide(X3,inverse(X3)),X2)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f4685,f6096])).
% 43.88/5.99 fof(f6098,plain,(
% 43.88/5.99 ![X0,X1,X2]: (double_divide(X0,inverse(X1))=double_divide(multiply(double_divide(inverse(X2),X1),X0),inverse(X2)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f6052,f6097])).
% 43.88/5.99 fof(f6117,plain,(
% 43.88/5.99 ![X0,X1]: (double_divide(X0,inverse(X1))=multiply(inverse(X0),X1))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5927,f6098])).
% 43.88/5.99 fof(f6304,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (multiply(multiply(multiply(X0,X1),multiply(X2,X3)),inverse(X3))=double_divide(multiply(double_divide(multiply(X4,X5),X2),double_divide(X1,X0)),double_divide(multiply(double_divide(X6,double_divide(X7,X6)),multiply(double_divide(X7,X8),double_divide(X5,X4))),X8)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5835,f4557])).
% 43.88/5.99 fof(f6305,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(multiply(multiply(X0,X1),multiply(X2,X3)),inverse(X3))=double_divide(multiply(double_divide(multiply(X4,X5),X2),double_divide(X1,X0)),double_divide(multiply(X6,multiply(double_divide(X6,X7),double_divide(X5,X4))),X7)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5835,f6304])).
% 43.88/5.99 fof(f6306,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(multiply(multiply(X0,X1),multiply(X2,X3)),inverse(X3))=multiply(multiply(X0,X1),X2))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5848,f6305])).
% 43.88/5.99 fof(f6313,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(multiply(multiply(X0,X1),multiply(X2,X3)),inverse(X3))=double_divide(multiply(double_divide(inverse(X4),X2),double_divide(X1,X0)),double_divide(multiply(double_divide(X5,double_divide(X6,X5)),multiply(double_divide(X6,X7),X4)),X7)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5835,f4560])).
% 43.88/5.99 fof(f6314,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(multiply(X0,X1),X2)=double_divide(multiply(double_divide(inverse(X3),X2),double_divide(X1,X0)),double_divide(multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,X6),X3)),X6)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f6306,f6313])).
% 43.88/5.99 fof(f6315,plain,(
% 43.88/5.99 ![X0,X1,X2,X3,X4,X5]: (multiply(multiply(X0,X1),X2)=double_divide(multiply(double_divide(inverse(X3),X2),double_divide(X1,X0)),double_divide(multiply(X4,multiply(double_divide(X4,X5),X3)),X5)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5835,f6314])).
% 43.88/5.99 fof(f6316,plain,(
% 43.88/5.99 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(inverse(double_divide(X1,X0)),X2))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5855,f6315])).
% 43.88/5.99 fof(f6318,plain,(
% 43.88/5.99 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=double_divide(double_divide(X1,X0),inverse(X2)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f6117,f6316])).
% 43.88/5.99 fof(f7459,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(inverse(double_divide(X0,X1)),X2)=multiply(double_divide(X3,double_divide(X1,X3)),multiply(X0,X2)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f5109,f4794])).
% 43.88/5.99 fof(f7460,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (double_divide(double_divide(X0,X1),inverse(X2))=multiply(double_divide(X3,double_divide(X1,X3)),multiply(X0,X2)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f6117,f7459])).
% 43.88/5.99 fof(f7461,plain,(
% 43.88/5.99 ![X0,X1,X2,X3]: (multiply(multiply(X0,X1),X2)=multiply(double_divide(X3,double_divide(X0,X3)),multiply(X1,X2)))),
% 43.88/5.99 inference(forward_demodulation,[status(thm)],[f6318,f7460])).
% 43.88/5.99 fof(f7462,plain,(
% 43.88/5.99 ~multiply(a3,multiply(b3,c3))=multiply(a3,multiply(b3,c3))),
% 43.88/5.99 inference(backward_demodulation,[status(thm)],[f7474,f6])).
% 43.88/5.99 fof(f7474,plain,(
% 43.88/5.99 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X0,multiply(X1,X2)))),
% 16.97/6.05 inference(forward_demodulation,[status(thm)],[f5835,f7461])).
% 16.97/6.05 fof(f14895,plain,(
% 16.97/6.05 $false),
% 16.97/6.05 inference(trivial_equality_resolution,[status(thm)],[f7462])).
% 16.97/6.05 % SZS output end CNFRefutation for theBenchmark.p
% 16.97/6.08 % Elapsed time: 5.684559 seconds
% 16.97/6.08 % CPU time: 44.815989 seconds
% 16.97/6.08 % Total memory used: 415.923 MB
% 16.97/6.08 % Net memory used: 406.797 MB
%------------------------------------------------------------------------------