%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : BOO026-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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 13.62s 2.21s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : BOO026-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n019.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 13:48:50 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.35 % Drodi V4.1.1
% 13.62/2.21 % Refutation found
% 13.62/2.21 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 13.62/2.21 % SZS output start CNFRefutation for theBenchmark
% 13.62/2.21 fof(f1,axiom,(
% 13.62/2.21 (![X,Y,Z]: (multiply(X,add(Y,Z)) = add(multiply(Y,X),multiply(Z,X)) ))),
% 13.62/2.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.62/2.21 fof(f2,axiom,(
% 13.62/2.21 (![X]: (add(X,inverse(X)) = n1 ))),
% 13.62/2.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.62/2.21 fof(f3,axiom,(
% 13.62/2.21 (![X,Y,Z]: (add(X,multiply(Y,Z)) = multiply(add(Y,X),add(Z,X)) ))),
% 13.62/2.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.62/2.21 fof(f4,axiom,(
% 13.62/2.21 (![X]: (multiply(X,inverse(X)) = n0 ))),
% 13.62/2.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.62/2.21 fof(f5,axiom,(
% 13.62/2.21 (![X,Y]: (add(multiply(X,inverse(X)),add(multiply(X,Y),multiply(inverse(X),Y))) = Y ))),
% 13.62/2.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.62/2.21 fof(f7,axiom,(
% 13.62/2.21 (![X,Y]: (add(multiply(X,inverse(Y)),add(multiply(X,X),multiply(inverse(Y),X))) = X ))),
% 13.62/2.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.62/2.21 fof(f8,axiom,(
% 13.62/2.21 (![X,Y]: (multiply(add(X,inverse(X)),multiply(add(X,Y),add(inverse(X),Y))) = Y ))),
% 13.62/2.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.62/2.21 fof(f9,axiom,(
% 13.62/2.21 (![X,Y]: (multiply(add(X,inverse(Y)),multiply(add(X,Y),add(inverse(Y),Y))) = X ))),
% 13.62/2.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.62/2.21 fof(f10,axiom,(
% 13.62/2.21 (![X,Y]: (multiply(add(X,inverse(Y)),multiply(add(X,X),add(inverse(Y),X))) = X ))),
% 13.62/2.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.62/2.21 fof(f11,negated_conjecture,(
% 13.62/2.21 multiply(add(a,b),b) != b ),
% 13.62/2.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.62/2.21 fof(f12,plain,(
% 13.62/2.21 ![X0,X1,X2]: (multiply(X0,add(X1,X2))=add(multiply(X1,X0),multiply(X2,X0)))),
% 13.62/2.21 inference(cnf_transformation,[status(thm)],[f1])).
% 13.62/2.21 fof(f13,plain,(
% 13.62/2.21 ![X0]: (add(X0,inverse(X0))=n1)),
% 13.62/2.21 inference(cnf_transformation,[status(thm)],[f2])).
% 13.62/2.21 fof(f14,plain,(
% 13.62/2.21 ![X0,X1,X2]: (add(X0,multiply(X1,X2))=multiply(add(X1,X0),add(X2,X0)))),
% 13.62/2.21 inference(cnf_transformation,[status(thm)],[f3])).
% 13.62/2.21 fof(f15,plain,(
% 13.62/2.21 ![X0]: (multiply(X0,inverse(X0))=n0)),
% 13.62/2.21 inference(cnf_transformation,[status(thm)],[f4])).
% 13.62/2.21 fof(f16,plain,(
% 13.62/2.21 ![X0,X1]: (add(multiply(X0,inverse(X0)),add(multiply(X0,X1),multiply(inverse(X0),X1)))=X1)),
% 13.62/2.21 inference(cnf_transformation,[status(thm)],[f5])).
% 13.62/2.21 fof(f18,plain,(
% 13.62/2.21 ![X0,X1]: (add(multiply(X0,inverse(X1)),add(multiply(X0,X0),multiply(inverse(X1),X0)))=X0)),
% 13.62/2.21 inference(cnf_transformation,[status(thm)],[f7])).
% 13.62/2.21 fof(f19,plain,(
% 13.62/2.21 ![X0,X1]: (multiply(add(X0,inverse(X0)),multiply(add(X0,X1),add(inverse(X0),X1)))=X1)),
% 13.62/2.21 inference(cnf_transformation,[status(thm)],[f8])).
% 13.62/2.21 fof(f20,plain,(
% 13.62/2.21 ![X0,X1]: (multiply(add(X0,inverse(X1)),multiply(add(X0,X1),add(inverse(X1),X1)))=X0)),
% 13.62/2.21 inference(cnf_transformation,[status(thm)],[f9])).
% 13.62/2.21 fof(f21,plain,(
% 13.62/2.21 ![X0,X1]: (multiply(add(X0,inverse(X1)),multiply(add(X0,X0),add(inverse(X1),X0)))=X0)),
% 13.62/2.21 inference(cnf_transformation,[status(thm)],[f10])).
% 13.62/2.21 fof(f22,plain,(
% 13.62/2.21 ~multiply(add(a,b),b)=b),
% 13.62/2.21 inference(cnf_transformation,[status(thm)],[f11])).
% 13.62/2.21 fof(f27,plain,(
% 13.62/2.21 ![X0,X1]: (multiply(inverse(X0),add(X1,X0))=add(multiply(X1,inverse(X0)),n0))),
% 13.62/2.21 inference(paramodulation,[status(thm)],[f15,f12])).
% 13.62/2.21 fof(f28,plain,(
% 13.62/2.21 ![X0,X1,X2,X3]: (add(multiply(X0,X1),multiply(multiply(X2,X1),X3))=multiply(multiply(X1,add(X2,X0)),add(X3,multiply(X0,X1))))),
% 13.62/2.21 inference(paramodulation,[status(thm)],[f12,f14])).
% 13.62/2.21 fof(f29,plain,(
% 13.62/2.21 ![X0,X1]: (add(inverse(X0),multiply(X0,X1))=multiply(n1,add(X1,inverse(X0))))),
% 13.62/2.21 inference(paramodulation,[status(thm)],[f13,f14])).
% 13.62/2.21 fof(f30,plain,(
% 13.62/2.21 ![X0,X1,X2,X3]: (add(multiply(X0,X1),multiply(X2,multiply(X3,X1)))=multiply(add(X2,multiply(X0,X1)),multiply(X1,add(X3,X0))))),
% 13.62/2.21 inference(paramodulation,[status(thm)],[f12,f14])).
% 13.62/2.21 fof(f31,plain,(
% 13.62/2.21 ![X0,X1]: (add(inverse(X0),multiply(X1,X0))=multiply(add(X1,inverse(X0)),n1))),
% 13.62/2.21 inference(paramodulation,[status(thm)],[f13,f14])).
% 13.62/2.21 fof(f38,plain,(
% 13.62/2.21 ![X0,X1]: (add(n0,add(multiply(X0,X1),multiply(inverse(X0),X1)))=X1)),
% 13.62/2.21 inference(forward_demodulation,[status(thm)],[f15,f16])).
% 13.62/2.21 fof(f39,plain,(
% 13.62/2.21 ![X0,X1]: (add(n0,multiply(X0,add(X1,inverse(X1))))=X0)),
% 13.62/2.21 inference(forward_demodulation,[status(thm)],[f12,f38])).
% 13.62/2.21 fof(f40,plain,(
% 13.62/2.21 ![X0]: (add(n0,multiply(X0,n1))=X0)),
% 13.62/2.21 inference(forward_demodulation,[status(thm)],[f13,f39])).
% 13.62/2.21 fof(f42,plain,(
% 13.62/2.21 ![X0,X1]: (add(multiply(X0,n1),multiply(X1,n0))=multiply(add(X1,multiply(X0,n1)),X0))),
% 13.62/2.21 inference(paramodulation,[status(thm)],[f40,f14])).
% 13.62/2.21 fof(f43,plain,(
% 13.62/2.21 ![X0,X1]: (add(multiply(X0,n1),multiply(n0,X1))=multiply(X0,add(X1,multiply(X0,n1))))),
% 13.62/2.21 inference(paramodulation,[status(thm)],[f40,f14])).
% 13.62/2.21 fof(f89,plain,(
% 13.62/2.21 ![X0,X1]: (add(n0,add(inverse(X0),multiply(X1,X0)))=add(X1,inverse(X0)))),
% 13.62/2.21 inference(paramodulation,[status(thm)],[f31,f40])).
% 13.62/2.21 fof(f133,plain,(
% 13.62/2.21 ![X0,X1]: (add(multiply(X0,inverse(X1)),multiply(X0,add(X0,inverse(X1))))=X0)),
% 13.62/2.21 inference(forward_demodulation,[status(thm)],[f12,f18])).
% 13.62/2.21 fof(f137,plain,(
% 13.62/2.21 ![X0]: (add(multiply(inverse(inverse(X0)),inverse(X0)),add(multiply(inverse(inverse(X0)),inverse(inverse(X0))),n0))=inverse(inverse(X0)))),
% 13.62/2.21 inference(paramodulation,[status(thm)],[f27,f133])).
% 13.62/2.21 fof(f147,plain,(
% 13.62/2.21 ![X0,X1]: (multiply(n1,multiply(add(X0,X1),add(inverse(X0),X1)))=X1)),
% 13.62/2.21 inference(forward_demodulation,[status(thm)],[f13,f19])).
% 13.62/2.21 fof(f148,plain,(
% 13.62/2.21 ![X0,X1]: (multiply(n1,add(X0,multiply(X1,inverse(X1))))=X0)),
% 13.62/2.21 inference(forward_demodulation,[status(thm)],[f14,f147])).
% 13.62/2.21 fof(f149,plain,(
% 13.62/2.21 ![X0]: (multiply(n1,add(X0,n0))=X0)),
% 13.62/2.21 inference(forward_demodulation,[status(thm)],[f15,f148])).
% 13.62/2.21 fof(f152,plain,(
% 13.62/2.21 ![X0,X1]: (multiply(add(X0,n0),add(X1,n1))=add(multiply(X1,add(X0,n0)),X0))),
% 13.62/2.21 inference(paramodulation,[status(thm)],[f149,f12])).
% 13.62/2.21 fof(f153,plain,(
% 13.62/2.21 ![X0,X1]: (multiply(add(X0,n0),add(n1,X1))=add(X0,multiply(X1,add(X0,n0))))),
% 13.62/2.21 inference(paramodulation,[status(thm)],[f149,f12])).
% 13.62/2.21 fof(f154,plain,(
% 13.62/2.21 ![X0,X1]: (multiply(add(X0,inverse(X1)),add(X1,multiply(X0,inverse(X1))))=X0)),
% 13.62/2.21 inference(forward_demodulation,[status(thm)],[f14,f20])).
% 13.62/2.21 fof(f160,plain,(
% 13.62/2.21 ![X0,X1]: (add(inverse(add(X0,multiply(X1,inverse(X0)))),X1)=multiply(add(add(X1,inverse(X0)),inverse(add(X0,multiply(X1,inverse(X0))))),n1))),
% 13.62/2.21 inference(paramodulation,[status(thm)],[f154,f31])).
% 13.62/2.21 fof(f166,plain,(
% 13.62/2.21 ![X0,X1]: (multiply(add(X0,inverse(X1)),add(X0,multiply(X0,inverse(X1))))=X0)),
% 13.62/2.21 inference(forward_demodulation,[status(thm)],[f14,f21])).
% 13.62/2.21 fof(f177,plain,(
% 13.62/2.21 ![X0,X1,X2]: (multiply(add(X0,multiply(X0,inverse(X1))),add(add(X0,inverse(X1)),X2))=add(X0,multiply(X2,add(X0,multiply(X0,inverse(X1))))))),
% 13.62/2.21 inference(paramodulation,[status(thm)],[f166,f12])).
% 13.62/2.21 fof(f187,plain,(
% 13.62/2.21 ![X0,X1]: (add(multiply(n0,n1),multiply(multiply(X0,n1),X1))=multiply(X0,add(X1,multiply(n0,n1))))),
% 13.62/2.21 inference(paramodulation,[status(thm)],[f149,f28])).
% 13.62/2.21 fof(f337,plain,(
% 13.62/2.21 ![X0,X1]: (add(multiply(X0,n1),multiply(n0,multiply(X1,n1)))=multiply(X0,multiply(n1,add(X1,X0))))),
% 13.62/2.21 inference(paramodulation,[status(thm)],[f40,f30])).
% 13.62/2.21 fof(f438,plain,(
% 13.62/2.21 ![X0]: (add(multiply(X0,n1),multiply(n0,n0))=multiply(X0,X0))),
% 13.62/2.21 inference(paramodulation,[status(thm)],[f40,f42])).
% 13.62/2.21 fof(f447,plain,(
% 13.62/2.21 ![X0]: (add(n0,add(multiply(n1,n1),multiply(X0,n0)))=add(X0,multiply(n1,n1)))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f42,f40])).
% 13.62/2.22 fof(f466,plain,(
% 13.62/2.22 ![X0,X1]: (add(multiply(add(X0,X1),n1),multiply(n0,n0))=add(X1,multiply(X0,X0)))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f14,f438])).
% 13.62/2.22 fof(f493,plain,(
% 13.62/2.22 ![X0,X1]: (multiply(X0,add(X1,X0))=add(multiply(X1,X0),add(multiply(X0,n1),multiply(n0,n0))))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f438,f12])).
% 13.62/2.22 fof(f617,plain,(
% 13.62/2.22 ![X0]: (multiply(add(X0,n0),add(n1,n1))=add(X0,X0))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f149,f152])).
% 13.62/2.22 fof(f621,plain,(
% 13.62/2.22 ![X0,X1]: (multiply(add(X0,n0),add(add(X1,n0),n1))=add(add(n0,multiply(X1,X0)),X0))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f14,f152])).
% 13.62/2.22 fof(f663,plain,(
% 13.62/2.22 ![X0,X1]: (multiply(add(multiply(X0,X1),n0),add(n1,n1))=multiply(X1,add(X0,X0)))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f12,f617])).
% 13.62/2.22 fof(f695,plain,(
% 13.62/2.22 ![X0]: (multiply(inverse(X0),multiply(add(X0,n0),add(n1,n1)))=add(multiply(X0,inverse(X0)),n0))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f617,f27])).
% 13.62/2.22 fof(f707,plain,(
% 13.62/2.22 ![X0]: (multiply(inverse(X0),multiply(add(X0,n0),add(n1,n1)))=add(n0,n0))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f15,f695])).
% 13.62/2.22 fof(f712,plain,(
% 13.62/2.22 ![X0]: (add(n0,multiply(X0,n1))=add(X0,multiply(n0,add(X0,n0))))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f14,f153])).
% 13.62/2.22 fof(f757,plain,(
% 13.62/2.22 ![X0]: (X0=add(X0,multiply(n0,add(X0,n0))))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f40,f712])).
% 13.62/2.22 fof(f825,plain,(
% 13.62/2.22 ![X0,X1]: (add(multiply(add(X0,multiply(X1,X0)),n1),multiply(n0,n0))=multiply(X0,add(X1,X0)))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f12,f466])).
% 13.62/2.22 fof(f1463,plain,(
% 13.62/2.22 ![X0,X1]: (multiply(inverse(multiply(X0,X1)),multiply(X1,add(X0,X0)))=add(n0,n0))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f663,f707])).
% 13.62/2.22 fof(f1549,plain,(
% 13.62/2.22 multiply(inverse(multiply(n0,n1)),n0)=add(n0,n0)),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f149,f1463])).
% 13.62/2.22 fof(f3278,plain,(
% 13.62/2.22 ![X0,X1]: (add(multiply(X0,inverse(X1)),multiply(X0,add(X0,inverse(X1))))=add(X0,multiply(multiply(X0,inverse(X1)),add(X0,multiply(X0,inverse(X1))))))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f14,f177])).
% 13.62/2.22 fof(f3342,plain,(
% 13.62/2.22 ![X0,X1]: (X0=add(X0,multiply(multiply(X0,inverse(X1)),add(X0,multiply(X0,inverse(X1))))))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f133,f3278])).
% 13.62/2.22 fof(f8491,plain,(
% 13.62/2.22 ![X0]: (multiply(n1,add(n0,multiply(X0,n1)))=multiply(X0,add(n1,multiply(n0,n1))))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f12,f187])).
% 13.62/2.22 fof(f8532,plain,(
% 13.62/2.22 ![X0]: (add(multiply(multiply(X0,add(multiply(n0,n1),multiply(n0,n1))),n1),multiply(n0,n0))=multiply(multiply(n0,n1),add(multiply(X0,n1),multiply(n0,n1))))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f187,f825])).
% 13.62/2.22 fof(f8568,plain,(
% 13.62/2.22 ![X0]: (multiply(n1,X0)=multiply(X0,add(n1,multiply(n0,n1))))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f40,f8491])).
% 13.62/2.22 fof(f8603,plain,(
% 13.62/2.22 ![X0]: (add(multiply(multiply(X0,multiply(n1,add(n0,n0))),n1),multiply(n0,n0))=multiply(multiply(n0,n1),add(multiply(X0,n1),multiply(n0,n1))))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f12,f8532])).
% 13.62/2.22 fof(f8604,plain,(
% 13.62/2.22 ![X0]: (add(multiply(multiply(X0,n0),n1),multiply(n0,n0))=multiply(multiply(n0,n1),add(multiply(X0,n1),multiply(n0,n1))))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f149,f8603])).
% 13.62/2.22 fof(f8605,plain,(
% 13.62/2.22 ![X0]: (add(multiply(multiply(X0,n0),n1),multiply(n0,n0))=multiply(multiply(n0,n1),multiply(n1,add(X0,n0))))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f12,f8604])).
% 13.62/2.22 fof(f8606,plain,(
% 13.62/2.22 ![X0]: (add(multiply(multiply(X0,n0),n1),multiply(n0,n0))=multiply(multiply(n0,n1),X0))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f149,f8605])).
% 13.62/2.22 fof(f8829,plain,(
% 13.62/2.22 ![X0]: (multiply(n1,add(X0,multiply(n0,n1)))=add(multiply(n0,n1),multiply(X0,n1)))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f14,f8568])).
% 13.62/2.22 fof(f8830,plain,(
% 13.62/2.22 multiply(n1,n0)=add(multiply(n0,n1),multiply(n0,n1))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f43,f8568])).
% 13.62/2.22 fof(f8831,plain,(
% 13.62/2.22 multiply(n1,add(n1,multiply(n0,n1)))=add(multiply(add(n1,multiply(n0,n1)),n1),multiply(n0,n0))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f438,f8568])).
% 13.62/2.22 fof(f8908,plain,(
% 13.62/2.22 ![X0]: (multiply(n1,add(X0,multiply(n0,n1)))=multiply(n1,add(n0,X0)))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f12,f8829])).
% 13.62/2.22 fof(f8909,plain,(
% 13.62/2.22 multiply(n1,n0)=multiply(n1,add(n0,n0))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f12,f8830])).
% 13.62/2.22 fof(f8910,plain,(
% 13.62/2.22 multiply(n1,n0)=n0),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f149,f8909])).
% 13.62/2.22 fof(f8911,plain,(
% 13.62/2.22 multiply(n1,n1)=add(multiply(add(n1,multiply(n0,n1)),n1),multiply(n0,n0))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f8568,f8831])).
% 13.62/2.22 fof(f8912,plain,(
% 13.62/2.22 multiply(n1,n1)=multiply(n1,add(n0,n1))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f825,f8911])).
% 13.62/2.22 fof(f8982,plain,(
% 13.62/2.22 add(n0,add(inverse(n0),n0))=add(n1,inverse(n0))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f8910,f89])).
% 13.62/2.22 fof(f8984,plain,(
% 13.62/2.22 ![X0]: (multiply(n0,add(n1,X0))=add(n0,multiply(X0,n0)))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f8910,f12])).
% 13.62/2.22 fof(f9263,plain,(
% 13.62/2.22 multiply(n0,n1)=add(n0,multiply(multiply(n0,add(n1,n0)),n0))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f757,f8984])).
% 13.62/2.22 fof(f9269,plain,(
% 13.62/2.22 n1=add(n1,add(n0,multiply(n0,n0)))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f8984,f757])).
% 13.62/2.22 fof(f9319,plain,(
% 13.62/2.22 multiply(n0,n1)=add(n0,multiply(add(n0,multiply(n0,n0)),n0))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f8984,f9263])).
% 13.62/2.22 fof(f14792,plain,(
% 13.62/2.22 add(multiply(add(n0,n0),n1),multiply(n0,n0))=multiply(multiply(n0,n1),inverse(multiply(n0,n1)))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f1549,f8606])).
% 13.62/2.22 fof(f14839,plain,(
% 13.62/2.22 add(multiply(add(n0,n0),n1),multiply(n0,n0))=n0),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f15,f14792])).
% 13.62/2.22 fof(f15239,plain,(
% 13.62/2.22 add(n0,multiply(n0,n0))=n0),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f466,f14839])).
% 13.62/2.22 fof(f15315,plain,(
% 13.62/2.22 multiply(n0,n1)=add(n0,multiply(n0,n0))),
% 13.62/2.22 inference(backward_demodulation,[status(thm)],[f15239,f9319])).
% 13.62/2.22 fof(f15316,plain,(
% 13.62/2.22 n1=add(n1,n0)),
% 13.62/2.22 inference(backward_demodulation,[status(thm)],[f15239,f9269])).
% 13.62/2.22 fof(f15364,plain,(
% 13.62/2.22 multiply(n0,n1)=n0),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f15239,f15315])).
% 13.62/2.22 fof(f15407,plain,(
% 13.62/2.22 ![X0]: (multiply(n1,add(X0,n0))=multiply(n1,add(n0,X0)))),
% 13.62/2.22 inference(backward_demodulation,[status(thm)],[f15364,f8908])).
% 13.62/2.22 fof(f15434,plain,(
% 13.62/2.22 add(n0,multiply(n0,n0))=multiply(n0,n0)),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f15364,f438])).
% 13.62/2.22 fof(f15438,plain,(
% 13.62/2.22 add(n0,n0)=n0),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f15364,f40])).
% 13.62/2.22 fof(f15451,plain,(
% 13.62/2.22 multiply(n1,add(n0,n1))=add(n0,add(multiply(n1,n1),multiply(n0,n0)))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f15364,f493])).
% 13.62/2.22 fof(f15461,plain,(
% 13.62/2.22 ![X0]: (multiply(n1,add(X0,n0))=add(multiply(X0,n1),n0))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f15364,f12])).
% 13.62/2.22 fof(f15465,plain,(
% 13.62/2.22 ![X0]: (X0=multiply(n1,add(n0,X0)))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f149,f15407])).
% 13.62/2.22 fof(f15485,plain,(
% 13.62/2.22 n0=multiply(n0,n0)),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f15239,f15434])).
% 13.62/2.22 fof(f15501,plain,(
% 13.62/2.22 multiply(n1,n1)=add(n0,add(multiply(n1,n1),multiply(n0,n0)))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f8912,f15451])).
% 13.62/2.22 fof(f15502,plain,(
% 13.62/2.22 multiply(n1,n1)=add(n0,multiply(n1,n1))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f447,f15501])).
% 13.62/2.22 fof(f15503,plain,(
% 13.62/2.22 multiply(n1,n1)=n1),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f40,f15502])).
% 13.62/2.22 fof(f15511,plain,(
% 13.62/2.22 ![X0]: (X0=add(multiply(X0,n1),n0))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f149,f15461])).
% 13.62/2.22 fof(f15527,plain,(
% 13.62/2.22 ![X0]: (multiply(add(X0,n0),n1)=add(X0,multiply(n0,add(X0,n0))))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f15316,f153])).
% 13.62/2.22 fof(f15576,plain,(
% 13.62/2.22 ![X0]: (add(n0,multiply(n1,X0))=multiply(n1,add(X0,n0)))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f15316,f14])).
% 13.62/2.22 fof(f15587,plain,(
% 13.62/2.22 ![X0]: (multiply(add(X0,n0),n1)=X0)),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f757,f15527])).
% 13.62/2.22 fof(f15634,plain,(
% 13.62/2.22 ![X0]: (add(n0,multiply(n1,X0))=X0)),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f149,f15576])).
% 13.62/2.22 fof(f16082,plain,(
% 13.62/2.22 add(n0,n1)=n1),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f15503,f40])).
% 13.62/2.22 fof(f16223,plain,(
% 13.62/2.22 inverse(n0)=multiply(n1,n1)),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f13,f15465])).
% 13.62/2.22 fof(f16288,plain,(
% 13.62/2.22 inverse(n0)=n1),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f15503,f16223])).
% 13.62/2.22 fof(f16319,plain,(
% 13.62/2.22 add(n0,add(inverse(n0),n0))=add(n1,n1)),
% 13.62/2.22 inference(backward_demodulation,[status(thm)],[f16288,f8982])).
% 13.62/2.22 fof(f16429,plain,(
% 13.62/2.22 add(n0,add(n1,n0))=add(n1,n1)),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f16288,f16319])).
% 13.62/2.22 fof(f16430,plain,(
% 13.62/2.22 add(n0,n1)=add(n1,n1)),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f15316,f16429])).
% 13.62/2.22 fof(f16431,plain,(
% 13.62/2.22 n1=add(n1,n1)),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f16082,f16430])).
% 13.62/2.22 fof(f17284,plain,(
% 13.62/2.22 add(n0,n0)=inverse(n1)),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f15,f15634])).
% 13.62/2.22 fof(f17290,plain,(
% 13.62/2.22 ![X0]: (multiply(add(X0,n0),add(add(n1,n0),n1))=add(X0,X0))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f15634,f621])).
% 13.62/2.22 fof(f17339,plain,(
% 13.62/2.22 n0=inverse(n1)),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f15438,f17284])).
% 13.62/2.22 fof(f17340,plain,(
% 13.62/2.22 ![X0]: (multiply(add(X0,n0),add(n1,n1))=add(X0,X0))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f15316,f17290])).
% 13.62/2.22 fof(f17341,plain,(
% 13.62/2.22 ![X0]: (multiply(add(X0,n0),n1)=add(X0,X0))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f16431,f17340])).
% 13.62/2.22 fof(f17342,plain,(
% 13.62/2.22 ![X0]: (X0=add(X0,X0))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f15587,f17341])).
% 13.62/2.22 fof(f17493,plain,(
% 13.62/2.22 ![X0]: (multiply(inverse(X0),X0)=add(multiply(X0,inverse(X0)),n0))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f17342,f27])).
% 13.62/2.22 fof(f17606,plain,(
% 13.62/2.22 ![X0]: (multiply(inverse(X0),X0)=add(n0,n0))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f15,f17493])).
% 13.62/2.22 fof(f17607,plain,(
% 13.62/2.22 ![X0]: (multiply(inverse(X0),X0)=n0)),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f17342,f17606])).
% 13.62/2.22 fof(f18522,plain,(
% 13.62/2.22 ![X0]: (add(multiply(X0,n1),multiply(n0,n0))=multiply(X0,multiply(n1,add(inverse(n1),X0))))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f17607,f337])).
% 13.62/2.22 fof(f18593,plain,(
% 13.62/2.22 ![X0]: (add(multiply(X0,n1),n0)=multiply(X0,multiply(n1,add(inverse(n1),X0))))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f15485,f18522])).
% 13.62/2.22 fof(f18594,plain,(
% 13.62/2.22 ![X0]: (X0=multiply(X0,multiply(n1,add(inverse(n1),X0))))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f15511,f18593])).
% 13.62/2.22 fof(f18595,plain,(
% 13.62/2.22 ![X0]: (X0=multiply(X0,multiply(n1,add(n0,X0))))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f17339,f18594])).
% 13.62/2.22 fof(f18596,plain,(
% 13.62/2.22 ![X0]: (X0=multiply(X0,X0))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f15465,f18595])).
% 13.62/2.22 fof(f18777,plain,(
% 13.62/2.22 ![X0]: (add(inverse(X0),X0)=multiply(add(X0,inverse(X0)),n1))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f18596,f31])).
% 13.62/2.22 fof(f18931,plain,(
% 13.62/2.22 ![X0]: (add(inverse(X0),X0)=multiply(n1,n1))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f13,f18777])).
% 13.62/2.22 fof(f18932,plain,(
% 13.62/2.22 ![X0]: (add(inverse(X0),X0)=n1)),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f18596,f18931])).
% 13.62/2.22 fof(f19496,plain,(
% 13.62/2.22 ![X0]: (multiply(n1,add(X0,multiply(inverse(inverse(X0)),inverse(X0))))=inverse(inverse(X0)))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f18932,f154])).
% 13.62/2.22 fof(f19618,plain,(
% 13.62/2.22 ![X0]: (multiply(n1,add(X0,n0))=inverse(inverse(X0)))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f17607,f19496])).
% 13.62/2.22 fof(f19619,plain,(
% 13.62/2.22 ![X0]: (X0=inverse(inverse(X0)))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f149,f19618])).
% 13.62/2.22 fof(f19906,plain,(
% 13.62/2.22 ![X0]: (add(n0,add(multiply(inverse(inverse(X0)),inverse(inverse(X0))),n0))=inverse(inverse(X0)))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f17607,f137])).
% 13.62/2.22 fof(f19907,plain,(
% 13.62/2.22 ![X0]: (add(n0,add(inverse(inverse(X0)),n0))=inverse(inverse(X0)))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f18596,f19906])).
% 13.62/2.22 fof(f19908,plain,(
% 13.62/2.22 ![X0]: (add(n0,add(X0,n0))=inverse(inverse(X0)))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f19619,f19907])).
% 13.62/2.22 fof(f19909,plain,(
% 13.62/2.22 ![X0]: (add(n0,add(X0,n0))=X0)),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f19619,f19908])).
% 13.62/2.22 fof(f21241,plain,(
% 13.62/2.22 ![X0]: (add(inverse(add(inverse(X0),multiply(X0,inverse(inverse(X0))))),X0)=multiply(add(add(X0,inverse(inverse(X0))),inverse(multiply(n1,add(inverse(inverse(X0)),inverse(X0))))),n1))),
% 13.62/2.22 inference(paramodulation,[status(thm)],[f29,f160])).
% 13.62/2.22 fof(f21317,plain,(
% 13.62/2.22 ![X0]: (add(inverse(add(inverse(X0),multiply(X0,X0))),X0)=multiply(add(add(X0,inverse(inverse(X0))),inverse(multiply(n1,add(inverse(inverse(X0)),inverse(X0))))),n1))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f19619,f21241])).
% 13.62/2.22 fof(f21318,plain,(
% 13.62/2.22 ![X0]: (add(inverse(add(inverse(X0),X0)),X0)=multiply(add(add(X0,inverse(inverse(X0))),inverse(multiply(n1,add(inverse(inverse(X0)),inverse(X0))))),n1))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f18596,f21317])).
% 13.62/2.22 fof(f21319,plain,(
% 13.62/2.22 ![X0]: (add(inverse(n1),X0)=multiply(add(add(X0,inverse(inverse(X0))),inverse(multiply(n1,add(inverse(inverse(X0)),inverse(X0))))),n1))),
% 13.62/2.22 inference(forward_demodulation,[status(thm)],[f18932,f21318])).
% 13.62/2.22 fof(f21320,plain,(
% 13.62/2.22 ![X0]: (add(n0,X0)=multiply(add(add(X0,inverse(inverse(X0))),inverse(multiply(n1,add(inverse(inverse(X0)),inverse(X0))))),n1))),
% 14.42/2.27 inference(forward_demodulation,[status(thm)],[f17339,f21319])).
% 14.42/2.27 fof(f21321,plain,(
% 14.42/2.27 ![X0]: (add(n0,X0)=multiply(add(add(X0,X0),inverse(multiply(n1,add(inverse(inverse(X0)),inverse(X0))))),n1))),
% 14.42/2.27 inference(forward_demodulation,[status(thm)],[f19619,f21320])).
% 14.42/2.27 fof(f21322,plain,(
% 14.42/2.27 ![X0]: (add(n0,X0)=multiply(add(X0,inverse(multiply(n1,add(inverse(inverse(X0)),inverse(X0))))),n1))),
% 14.42/2.27 inference(forward_demodulation,[status(thm)],[f17342,f21321])).
% 14.42/2.27 fof(f21323,plain,(
% 14.42/2.27 ![X0]: (add(n0,X0)=multiply(add(X0,inverse(multiply(n1,n1))),n1))),
% 14.42/2.27 inference(forward_demodulation,[status(thm)],[f18932,f21322])).
% 14.42/2.27 fof(f21324,plain,(
% 14.42/2.27 ![X0]: (add(n0,X0)=multiply(add(X0,inverse(n1)),n1))),
% 14.42/2.27 inference(forward_demodulation,[status(thm)],[f18596,f21323])).
% 14.42/2.27 fof(f21325,plain,(
% 14.42/2.27 ![X0]: (add(n0,X0)=multiply(add(X0,n0),n1))),
% 14.42/2.27 inference(forward_demodulation,[status(thm)],[f17339,f21324])).
% 14.42/2.27 fof(f21326,plain,(
% 14.42/2.27 ![X0]: (add(n0,X0)=X0)),
% 14.42/2.27 inference(forward_demodulation,[status(thm)],[f15587,f21325])).
% 14.42/2.27 fof(f21414,plain,(
% 14.42/2.27 ![X0]: (add(X0,n0)=X0)),
% 14.42/2.27 inference(backward_demodulation,[status(thm)],[f21326,f19909])).
% 14.42/2.27 fof(f21420,plain,(
% 14.42/2.27 ![X0]: (multiply(X0,n1)=X0)),
% 14.42/2.27 inference(backward_demodulation,[status(thm)],[f21326,f40])).
% 14.42/2.27 fof(f21428,plain,(
% 14.42/2.27 ![X0]: (n0=multiply(multiply(n0,inverse(X0)),add(n0,multiply(n0,inverse(X0)))))),
% 14.42/2.27 inference(paramodulation,[status(thm)],[f3342,f21326])).
% 14.42/2.27 fof(f21526,plain,(
% 14.42/2.27 ![X0]: (n0=multiply(multiply(n0,inverse(X0)),multiply(n0,inverse(X0))))),
% 14.42/2.27 inference(forward_demodulation,[status(thm)],[f21326,f21428])).
% 14.42/2.27 fof(f21527,plain,(
% 14.42/2.27 ![X0]: (n0=multiply(n0,inverse(X0)))),
% 14.42/2.27 inference(forward_demodulation,[status(thm)],[f18596,f21526])).
% 14.42/2.27 fof(f21649,plain,(
% 14.42/2.27 ![X0,X1]: (multiply(add(X0,n0),add(n1,X1))=add(X0,multiply(X1,X0)))),
% 14.42/2.27 inference(backward_demodulation,[status(thm)],[f21414,f153])).
% 14.42/2.27 fof(f21684,plain,(
% 14.42/2.27 ![X0,X1]: (multiply(X0,add(n1,X1))=add(X0,multiply(X1,X0)))),
% 14.42/2.27 inference(forward_demodulation,[status(thm)],[f21414,f21649])).
% 14.42/2.27 fof(f21893,plain,(
% 14.42/2.27 ![X0,X1]: (add(multiply(X0,n1),multiply(X1,n0))=multiply(add(X1,X0),X0))),
% 14.42/2.27 inference(backward_demodulation,[status(thm)],[f21420,f42])).
% 14.42/2.27 fof(f21918,plain,(
% 14.42/2.27 ![X0,X1]: (add(X0,multiply(X1,n0))=multiply(add(X1,X0),X0))),
% 14.42/2.27 inference(forward_demodulation,[status(thm)],[f21420,f21893])).
% 14.42/2.27 fof(f22372,plain,(
% 14.42/2.27 ![X0]: (n0=multiply(n0,X0))),
% 14.42/2.27 inference(paramodulation,[status(thm)],[f19619,f21527])).
% 14.42/2.27 fof(f22493,plain,(
% 14.42/2.27 ![X0]: (n0=add(n0,multiply(X0,n0)))),
% 14.42/2.27 inference(paramodulation,[status(thm)],[f21684,f22372])).
% 14.42/2.27 fof(f22554,plain,(
% 14.42/2.27 ![X0]: (n0=multiply(X0,n0))),
% 14.42/2.27 inference(forward_demodulation,[status(thm)],[f21326,f22493])).
% 14.42/2.27 fof(f23907,plain,(
% 14.42/2.27 ![X0,X1]: (add(X0,n0)=multiply(add(X1,X0),X0))),
% 14.42/2.27 inference(forward_demodulation,[status(thm)],[f22554,f21918])).
% 14.42/2.27 fof(f23908,plain,(
% 14.42/2.27 ~b=b),
% 14.42/2.27 inference(backward_demodulation,[status(thm)],[f23909,f22])).
% 14.42/2.27 fof(f23909,plain,(
% 14.42/2.27 ![X0,X1]: (X0=multiply(add(X1,X0),X0))),
% 14.42/2.27 inference(forward_demodulation,[status(thm)],[f21414,f23907])).
% 14.42/2.27 fof(f23964,plain,(
% 14.42/2.27 $false),
% 14.42/2.27 inference(trivial_equality_resolution,[status(thm)],[f23908])).
% 14.42/2.27 % SZS output end CNFRefutation for theBenchmark.p
% 1.37/2.38 % Elapsed time: 2.021079 seconds
% 1.37/2.38 % CPU time: 15.407479 seconds
% 1.37/2.38 % Total memory used: 365.022 MB
% 1.37/2.38 % Net memory used: 361.896 MB
%------------------------------------------------------------------------------