%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : BOO025-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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:06:47 PM UTC 2026
% Result : Unsatisfiable 3.47s 0.90s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : BOO025-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n010.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 13:49:12 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.11/0.36 % Drodi V4.1.1
% 3.47/0.90 % Refutation found
% 3.47/0.90 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 3.47/0.90 % SZS output start CNFRefutation for theBenchmark
% 3.47/0.90 fof(f1,axiom,(
% 3.47/0.90 (![X,Y]: (multiply(add(X,Y),Y) = Y ))),
% 3.47/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.47/0.90 fof(f2,axiom,(
% 3.47/0.90 (![X,Y,Z]: (multiply(X,add(Y,Z)) = add(multiply(Y,X),multiply(Z,X)) ))),
% 3.47/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.47/0.90 fof(f3,axiom,(
% 3.47/0.90 (![X]: (add(X,inverse(X)) = n1 ))),
% 3.47/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.47/0.90 fof(f4,axiom,(
% 3.47/0.90 (![X,Y,Z]: (pixley(X,Y,Z) = add(multiply(X,inverse(Y)),add(multiply(X,Z),multiply(inverse(Y),Z))) ))),
% 3.47/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.47/0.90 fof(f5,axiom,(
% 3.47/0.90 (![X,Y]: (pixley(X,X,Y) = Y ))),
% 3.47/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.47/0.90 fof(f6,axiom,(
% 3.47/0.90 (![X,Y]: (pixley(X,Y,Y) = X ))),
% 3.47/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.47/0.90 fof(f8,negated_conjecture,(
% 3.47/0.90 multiply(b,inverse(b)) != multiply(a,inverse(a)) ),
% 3.47/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.47/0.90 fof(f9,plain,(
% 3.47/0.90 ![X0,X1]: (multiply(add(X0,X1),X1)=X1)),
% 3.47/0.90 inference(cnf_transformation,[status(thm)],[f1])).
% 3.47/0.90 fof(f10,plain,(
% 3.47/0.90 ![X0,X1,X2]: (multiply(X0,add(X1,X2))=add(multiply(X1,X0),multiply(X2,X0)))),
% 3.47/0.90 inference(cnf_transformation,[status(thm)],[f2])).
% 3.47/0.90 fof(f11,plain,(
% 3.47/0.90 ![X0]: (add(X0,inverse(X0))=n1)),
% 3.47/0.90 inference(cnf_transformation,[status(thm)],[f3])).
% 3.47/0.90 fof(f12,plain,(
% 3.47/0.90 ![X0,X1,X2]: (pixley(X0,X1,X2)=add(multiply(X0,inverse(X1)),add(multiply(X0,X2),multiply(inverse(X1),X2))))),
% 3.47/0.90 inference(cnf_transformation,[status(thm)],[f4])).
% 3.47/0.90 fof(f13,plain,(
% 3.47/0.90 ![X0,X1]: (pixley(X0,X0,X1)=X1)),
% 3.47/0.90 inference(cnf_transformation,[status(thm)],[f5])).
% 3.47/0.90 fof(f14,plain,(
% 3.47/0.90 ![X0,X1]: (pixley(X0,X1,X1)=X0)),
% 3.47/0.90 inference(cnf_transformation,[status(thm)],[f6])).
% 3.47/0.90 fof(f16,plain,(
% 3.47/0.90 ~multiply(b,inverse(b))=multiply(a,inverse(a))),
% 3.47/0.90 inference(cnf_transformation,[status(thm)],[f8])).
% 3.47/0.90 fof(f22,plain,(
% 3.47/0.90 ![X0,X1,X2]: (pixley(X0,X1,X2)=add(multiply(X0,inverse(X1)),multiply(X2,add(X0,inverse(X1)))))),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f10,f12])).
% 3.47/0.90 fof(f29,plain,(
% 3.47/0.90 ![X0]: (multiply(n1,inverse(X0))=inverse(X0))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f11,f9])).
% 3.47/0.90 fof(f31,plain,(
% 3.47/0.90 ![X0,X1,X2]: (multiply(X0,add(add(X1,X0),X2))=add(X0,multiply(X2,X0)))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f9,f10])).
% 3.47/0.90 fof(f32,plain,(
% 3.47/0.90 ![X0,X1]: (multiply(inverse(X0),add(X1,n1))=add(multiply(X1,inverse(X0)),inverse(X0)))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f29,f10])).
% 3.47/0.90 fof(f33,plain,(
% 3.47/0.90 ![X0,X1,X2]: (multiply(X0,add(X1,add(X2,X0)))=add(multiply(X1,X0),X0))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f9,f10])).
% 3.47/0.90 fof(f34,plain,(
% 3.47/0.90 ![X0,X1,X2]: (multiply(multiply(X0,add(X1,X2)),multiply(X2,X0))=multiply(X2,X0))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f10,f9])).
% 3.47/0.90 fof(f35,plain,(
% 3.47/0.90 ![X0,X1]: (multiply(X0,n1)=add(X0,multiply(inverse(add(X1,X0)),X0)))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f11,f31])).
% 3.47/0.90 fof(f48,plain,(
% 3.47/0.90 ![X0,X1,X2]: (multiply(add(X0,X1),multiply(X1,add(X2,add(X0,X1))))=multiply(X1,add(X2,add(X0,X1))))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f9,f34])).
% 3.47/0.90 fof(f52,plain,(
% 3.47/0.90 ![X0,X1]: (multiply(multiply(X0,n1),multiply(inverse(X1),X0))=multiply(inverse(X1),X0))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f11,f34])).
% 3.47/0.90 fof(f60,plain,(
% 3.47/0.90 ![X0,X1,X2]: (multiply(add(X0,X1),add(multiply(X2,X1),X1))=multiply(X1,add(X2,add(X0,X1))))),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f33,f48])).
% 3.47/0.90 fof(f61,plain,(
% 3.47/0.90 ![X0,X1,X2]: (multiply(add(X0,X1),add(multiply(X2,X1),X1))=add(multiply(X2,X1),X1))),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f33,f60])).
% 3.47/0.90 fof(f95,plain,(
% 3.47/0.90 ![X0,X1]: (pixley(X0,X0,X1)=add(multiply(X0,inverse(X0)),multiply(X1,n1)))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f11,f22])).
% 3.47/0.90 fof(f100,plain,(
% 3.47/0.90 ![X0,X1,X2]: (multiply(pixley(X0,X1,X2),multiply(X2,add(X0,inverse(X1))))=multiply(X2,add(X0,inverse(X1))))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f22,f9])).
% 3.47/0.90 fof(f101,plain,(
% 3.47/0.90 ![X0,X1]: (X0=add(multiply(X1,inverse(X1)),multiply(X0,n1)))),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f13,f95])).
% 3.47/0.90 fof(f103,plain,(
% 3.47/0.90 ![X0]: (X0=add(inverse(n1),multiply(X0,n1)))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f29,f101])).
% 3.47/0.90 fof(f107,plain,(
% 3.47/0.90 ![X0,X1]: (multiply(multiply(X0,n1),add(X1,X0))=add(multiply(X1,multiply(X0,n1)),multiply(X0,n1)))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f101,f33])).
% 3.47/0.90 fof(f109,plain,(
% 3.47/0.90 ![X0]: (multiply(X0,multiply(X0,n1))=multiply(X0,n1))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f101,f9])).
% 3.47/0.90 fof(f111,plain,(
% 3.47/0.90 ![X0]: (add(X0,n1)=add(inverse(n1),n1))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f9,f103])).
% 3.47/0.90 fof(f123,plain,(
% 3.47/0.90 ![X0,X1]: (add(X0,n1)=add(X1,n1))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f111,f111])).
% 3.47/0.90 fof(f141,plain,(
% 3.47/0.90 ![X0,X1]: (multiply(X0,add(X1,n1))=add(X0,multiply(n1,X0)))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f123,f31])).
% 3.47/0.90 fof(f159,plain,(
% 3.47/0.90 ![X0,X1,X2]: (multiply(X0,add(X1,n1))=multiply(X0,add(X2,n1)))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f141,f141])).
% 3.47/0.90 fof(f160,plain,(
% 3.47/0.90 ![X0,X1]: (multiply(inverse(X0),add(X1,n1))=add(inverse(X0),inverse(X0)))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f29,f141])).
% 3.47/0.90 fof(f208,plain,(
% 3.47/0.90 ![X0,X1,X2]: (multiply(add(X0,n1),add(X1,n1))=add(add(X0,n1),multiply(n1,add(X2,n1))))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f159,f141])).
% 3.47/0.90 fof(f311,plain,(
% 3.47/0.90 ![X0,X1,X2]: (multiply(add(X0,X1),add(X1,X1))=add(multiply(add(X2,X1),X1),X1))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f9,f61])).
% 3.47/0.90 fof(f312,plain,(
% 3.47/0.90 ![X0,X1]: (multiply(add(X0,multiply(X1,n1)),add(multiply(X1,n1),multiply(X1,n1)))=add(multiply(X1,multiply(X1,n1)),multiply(X1,n1)))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f109,f61])).
% 3.47/0.90 fof(f354,plain,(
% 3.47/0.90 ![X0,X1]: (multiply(add(X0,X1),add(X1,X1))=add(X1,X1))),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f9,f311])).
% 3.47/0.90 fof(f355,plain,(
% 3.47/0.90 ![X0]: (add(multiply(X0,n1),multiply(X0,n1))=add(multiply(X0,multiply(X0,n1)),multiply(X0,n1)))),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f354,f312])).
% 3.47/0.90 fof(f356,plain,(
% 3.47/0.90 ![X0]: (multiply(n1,add(X0,X0))=add(multiply(X0,multiply(X0,n1)),multiply(X0,n1)))),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f10,f355])).
% 3.47/0.90 fof(f357,plain,(
% 3.47/0.90 ![X0]: (multiply(n1,add(X0,X0))=multiply(multiply(X0,n1),add(X0,X0)))),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f107,f356])).
% 3.47/0.90 fof(f362,plain,(
% 3.47/0.90 ![X0,X1]: (multiply(add(X0,n1),add(X1,n1))=add(n1,n1))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f159,f354])).
% 3.47/0.90 fof(f374,plain,(
% 3.47/0.90 ![X0]: (multiply(n1,add(inverse(X0),inverse(X0)))=add(inverse(X0),inverse(X0)))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f11,f354])).
% 3.47/0.90 fof(f382,plain,(
% 3.47/0.90 ![X0,X1]: (multiply(add(X0,X0),multiply(X0,add(X1,X0)))=multiply(X0,add(X1,X0)))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f354,f34])).
% 3.47/0.90 fof(f388,plain,(
% 3.47/0.90 ![X0,X1]: (add(n1,n1)=add(add(X0,n1),multiply(n1,add(X1,n1))))),
% 3.47/0.90 inference(backward_demodulation,[status(thm)],[f362,f208])).
% 3.47/0.90 fof(f429,plain,(
% 3.47/0.90 ![X0,X1,X2]: (multiply(add(X0,n1),add(add(X1,n1),X2))=add(add(n1,n1),multiply(X2,add(X0,n1))))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f362,f10])).
% 3.47/0.90 fof(f455,plain,(
% 3.47/0.90 ![X0,X1]: (multiply(add(X0,X0),add(X1,multiply(X0,n1)))=add(multiply(X1,add(X0,X0)),multiply(n1,add(X0,X0))))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f357,f10])).
% 3.47/0.90 fof(f465,plain,(
% 3.47/0.90 ![X0,X1]: (multiply(add(X0,X0),add(X1,multiply(X0,n1)))=multiply(add(X0,X0),add(X1,n1)))),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f10,f455])).
% 3.47/0.90 fof(f532,plain,(
% 3.47/0.90 ![X0,X1]: (multiply(add(inverse(X0),inverse(X0)),add(X1,n1))=add(add(inverse(X0),inverse(X0)),add(inverse(X0),inverse(X0))))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f374,f141])).
% 3.47/0.90 fof(f551,plain,(
% 3.47/0.90 ![X0]: (multiply(add(n1,n1),add(n1,multiply(n1,n1)))=multiply(n1,add(X0,n1)))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f141,f382])).
% 3.47/0.90 fof(f570,plain,(
% 3.47/0.90 ![X0]: (multiply(add(n1,n1),add(n1,n1))=multiply(n1,add(X0,n1)))),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f465,f551])).
% 3.47/0.90 fof(f575,plain,(
% 3.47/0.90 ![X0]: (add(n1,n1)=add(add(X0,n1),add(n1,n1)))),
% 3.47/0.90 inference(backward_demodulation,[status(thm)],[f576,f388])).
% 3.47/0.90 fof(f576,plain,(
% 3.47/0.90 ![X0]: (add(n1,n1)=multiply(n1,add(X0,n1)))),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f362,f570])).
% 3.47/0.90 fof(f609,plain,(
% 3.47/0.90 ![X0,X1]: (multiply(X0,multiply(X1,add(X0,inverse(X1))))=multiply(X1,add(X0,inverse(X1))))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f14,f100])).
% 3.47/0.90 fof(f667,plain,(
% 3.47/0.90 ![X0,X1]: (multiply(add(X0,n1),add(n1,X1))=add(add(n1,n1),multiply(X1,add(X0,n1))))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f576,f10])).
% 3.47/0.90 fof(f676,plain,(
% 3.47/0.90 ![X0,X1,X2]: (multiply(add(X0,n1),add(add(X1,n1),X2))=multiply(add(X0,n1),add(n1,X2)))),
% 3.47/0.90 inference(backward_demodulation,[status(thm)],[f667,f429])).
% 3.47/0.90 fof(f736,plain,(
% 3.47/0.90 ![X0,X1]: (add(n1,n1)=add(add(X0,n1),add(X1,n1)))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f123,f575])).
% 3.47/0.90 fof(f790,plain,(
% 3.47/0.90 ![X0]: (multiply(add(X0,n1),n1)=add(add(X0,n1),multiply(inverse(add(n1,n1)),add(X0,n1))))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f736,f35])).
% 3.47/0.90 fof(f793,plain,(
% 3.47/0.90 ![X0,X1]: (multiply(add(X0,n1),add(add(n1,n1),X1))=add(add(X0,n1),multiply(X1,add(X0,n1))))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f736,f31])).
% 3.47/0.90 fof(f816,plain,(
% 3.47/0.90 ![X0]: (n1=add(add(X0,n1),multiply(inverse(add(n1,n1)),add(X0,n1))))),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f9,f790])).
% 3.47/0.90 fof(f819,plain,(
% 3.47/0.90 ![X0]: (n1=multiply(add(X0,n1),add(n1,inverse(add(n1,n1)))))),
% 3.47/0.90 inference(backward_demodulation,[status(thm)],[f820,f816])).
% 3.47/0.90 fof(f820,plain,(
% 3.47/0.90 ![X0,X1]: (multiply(add(X0,n1),add(n1,X1))=add(add(X0,n1),multiply(X1,add(X0,n1))))),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f676,f793])).
% 3.47/0.90 fof(f1647,plain,(
% 3.47/0.90 multiply(n1,n1)=multiply(add(n1,n1),add(n1,inverse(add(n1,n1))))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f819,f609])).
% 3.47/0.90 fof(f1676,plain,(
% 3.47/0.90 multiply(n1,n1)=n1),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f819,f1647])).
% 3.47/0.90 fof(f1864,plain,(
% 3.47/0.90 ![X0]: (multiply(n1,multiply(inverse(X0),n1))=multiply(inverse(X0),n1))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f1676,f52])).
% 3.47/0.90 fof(f1866,plain,(
% 3.47/0.90 n1=add(inverse(n1),n1)),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f1676,f103])).
% 3.47/0.90 fof(f1888,plain,(
% 3.47/0.90 ![X0]: (n1=add(X0,n1))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f123,f1866])).
% 3.47/0.90 fof(f1900,plain,(
% 3.47/0.90 ![X0]: (multiply(inverse(X0),n1)=add(inverse(X0),inverse(X0)))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f1866,f160])).
% 3.47/0.90 fof(f1924,plain,(
% 3.47/0.90 ![X0,X1]: (multiply(inverse(X0),n1)=add(multiply(X1,inverse(X0)),inverse(X0)))),
% 3.47/0.90 inference(backward_demodulation,[status(thm)],[f1888,f32])).
% 3.47/0.90 fof(f2046,plain,(
% 3.47/0.90 ![X0]: (multiply(add(inverse(X0),inverse(X0)),n1)=add(add(inverse(X0),inverse(X0)),add(inverse(X0),inverse(X0))))),
% 3.47/0.90 inference(backward_demodulation,[status(thm)],[f1888,f532])).
% 3.47/0.90 fof(f2499,plain,(
% 3.47/0.90 ![X0]: (multiply(multiply(inverse(X0),n1),n1)=add(add(inverse(X0),inverse(X0)),add(inverse(X0),inverse(X0))))),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f1900,f2046])).
% 3.47/0.90 fof(f2500,plain,(
% 3.47/0.90 ![X0]: (multiply(multiply(inverse(X0),n1),n1)=add(multiply(inverse(X0),n1),add(inverse(X0),inverse(X0))))),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f1900,f2499])).
% 3.47/0.90 fof(f2501,plain,(
% 3.47/0.90 ![X0]: (multiply(multiply(inverse(X0),n1),n1)=add(multiply(inverse(X0),n1),multiply(inverse(X0),n1)))),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f1900,f2500])).
% 3.47/0.90 fof(f2502,plain,(
% 3.47/0.90 ![X0]: (multiply(multiply(inverse(X0),n1),n1)=multiply(n1,add(inverse(X0),inverse(X0))))),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f10,f2501])).
% 3.47/0.90 fof(f2503,plain,(
% 3.47/0.90 ![X0]: (multiply(multiply(inverse(X0),n1),n1)=multiply(n1,multiply(inverse(X0),n1)))),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f1900,f2502])).
% 3.47/0.90 fof(f2507,plain,(
% 3.47/0.90 ![X0]: (multiply(multiply(inverse(X0),n1),n1)=multiply(inverse(X0),n1))),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f1864,f2503])).
% 3.47/0.90 fof(f3235,plain,(
% 3.47/0.90 ![X0]: (multiply(inverse(X0),n1)=add(inverse(n1),multiply(inverse(X0),n1)))),
% 3.47/0.90 inference(paramodulation,[status(thm)],[f2507,f103])).
% 3.47/0.90 fof(f3259,plain,(
% 3.47/0.90 ![X0,X1]: (inverse(X0)=add(multiply(X1,inverse(X0)),inverse(X0)))),
% 3.47/0.90 inference(backward_demodulation,[status(thm)],[f3303,f1924])).
% 3.47/0.90 fof(f3303,plain,(
% 3.47/0.90 ![X0]: (multiply(inverse(X0),n1)=inverse(X0))),
% 3.47/0.90 inference(forward_demodulation,[status(thm)],[f103,f3235])).
% 4.02/0.93 fof(f3523,plain,(
% 4.02/0.93 ![X0]: (inverse(X0)=add(inverse(n1),inverse(X0)))),
% 4.02/0.93 inference(paramodulation,[status(thm)],[f3303,f103])).
% 4.02/0.93 fof(f3688,plain,(
% 4.02/0.93 inverse(inverse(n1))=n1),
% 4.02/0.93 inference(paramodulation,[status(thm)],[f11,f3523])).
% 4.02/0.93 fof(f3690,plain,(
% 4.02/0.93 ![X0]: (multiply(inverse(n1),multiply(X0,inverse(X0)))=multiply(X0,add(inverse(n1),inverse(X0))))),
% 4.02/0.93 inference(paramodulation,[status(thm)],[f3523,f609])).
% 4.02/0.93 fof(f3716,plain,(
% 4.02/0.93 ![X0]: (multiply(inverse(n1),multiply(X0,inverse(X0)))=multiply(X0,inverse(X0)))),
% 4.02/0.93 inference(forward_demodulation,[status(thm)],[f3523,f3690])).
% 4.02/0.93 fof(f3762,plain,(
% 4.02/0.93 ![X0]: (multiply(X0,multiply(inverse(n1),add(X0,n1)))=multiply(inverse(n1),add(X0,inverse(inverse(n1)))))),
% 4.02/0.93 inference(paramodulation,[status(thm)],[f3688,f609])).
% 4.02/0.93 fof(f3788,plain,(
% 4.02/0.93 ![X0]: (multiply(X0,multiply(inverse(n1),n1))=multiply(inverse(n1),add(X0,inverse(inverse(n1)))))),
% 4.02/0.93 inference(forward_demodulation,[status(thm)],[f1888,f3762])).
% 4.02/0.93 fof(f3789,plain,(
% 4.02/0.93 ![X0]: (multiply(X0,inverse(n1))=multiply(inverse(n1),add(X0,inverse(inverse(n1)))))),
% 4.02/0.93 inference(forward_demodulation,[status(thm)],[f3303,f3788])).
% 4.02/0.93 fof(f3790,plain,(
% 4.02/0.93 ![X0]: (multiply(X0,inverse(n1))=multiply(inverse(n1),add(X0,n1)))),
% 4.02/0.93 inference(forward_demodulation,[status(thm)],[f3688,f3789])).
% 4.02/0.93 fof(f3791,plain,(
% 4.02/0.93 ![X0]: (multiply(X0,inverse(n1))=multiply(inverse(n1),n1))),
% 4.02/0.93 inference(forward_demodulation,[status(thm)],[f1888,f3790])).
% 4.02/0.93 fof(f3792,plain,(
% 4.02/0.93 ![X0]: (multiply(X0,inverse(n1))=inverse(n1))),
% 4.02/0.93 inference(forward_demodulation,[status(thm)],[f3303,f3791])).
% 4.02/0.93 fof(f4025,plain,(
% 4.02/0.93 ![X0,X1]: (multiply(inverse(n1),add(X0,X1))=add(multiply(X0,inverse(n1)),inverse(n1)))),
% 4.02/0.93 inference(paramodulation,[status(thm)],[f3792,f10])).
% 4.02/0.93 fof(f4053,plain,(
% 4.02/0.93 ![X0,X1]: (multiply(inverse(n1),add(X0,X1))=inverse(n1))),
% 4.02/0.93 inference(forward_demodulation,[status(thm)],[f3259,f4025])).
% 4.02/0.93 fof(f4631,plain,(
% 4.02/0.93 ![X0]: (multiply(inverse(n1),X0)=inverse(n1))),
% 4.02/0.93 inference(paramodulation,[status(thm)],[f101,f4053])).
% 4.02/0.93 fof(f4676,plain,(
% 4.02/0.93 ![X0]: (inverse(n1)=multiply(X0,inverse(X0)))),
% 4.02/0.93 inference(backward_demodulation,[status(thm)],[f4631,f3716])).
% 4.02/0.93 fof(f4712,plain,(
% 4.02/0.93 ~multiply(b,inverse(b))=inverse(n1)),
% 4.02/0.93 inference(backward_demodulation,[status(thm)],[f4676,f16])).
% 4.02/0.93 fof(f4727,plain,(
% 4.02/0.93 ~inverse(n1)=inverse(n1)),
% 4.02/0.93 inference(forward_demodulation,[status(thm)],[f4676,f4712])).
% 4.02/0.93 fof(f4728,plain,(
% 4.02/0.93 $false),
% 4.02/0.93 inference(trivial_equality_resolution,[status(thm)],[f4727])).
% 4.02/0.93 % SZS output end CNFRefutation for theBenchmark.p
% 4.02/0.95 % Elapsed time: 0.581546 seconds
% 4.02/0.95 % CPU time: 4.435805 seconds
% 4.02/0.95 % Total memory used: 149.768 MB
% 4.02/0.95 % Net memory used: 147.094 MB
%------------------------------------------------------------------------------