%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : BOO074-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 : n004.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:50 PM UTC 2026
% Result : Unsatisfiable 43.81s 6.23s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : BOO074-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n004.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 13:52:04 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.46 % Drodi V4.1.1
% 43.81/6.23 % Refutation found
% 43.81/6.23 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 43.81/6.23 % SZS output start CNFRefutation for theBenchmark
% 43.81/6.23 fof(f1,axiom,(
% 43.81/6.23 (![A,B,C,D]: (inverse(add(inverse(add(inverse(add(A,B)),C)),inverse(add(A,inverse(add(inverse(C),inverse(add(C,D)))))))) = C ))),
% 43.81/6.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 43.81/6.23 fof(f2,negated_conjecture,(
% 43.81/6.23 add(inverse(add(inverse(a),b)),inverse(add(inverse(a),inverse(b)))) != a ),
% 43.81/6.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 43.81/6.23 fof(f3,plain,(
% 43.81/6.23 ![X0,X1,X2,X3]: (inverse(add(inverse(add(inverse(add(X0,X1)),X2)),inverse(add(X0,inverse(add(inverse(X2),inverse(add(X2,X3))))))))=X2)),
% 43.81/6.23 inference(cnf_transformation,[status(thm)],[f1])).
% 43.81/6.23 fof(f4,plain,(
% 43.81/6.23 ~add(inverse(add(inverse(a),b)),inverse(add(inverse(a),inverse(b))))=a),
% 43.81/6.23 inference(cnf_transformation,[status(thm)],[f2])).
% 43.81/6.23 fof(f13,plain,(
% 43.81/6.23 ![X0,X1,X2,X3,X4]: (inverse(add(X0,inverse(add(inverse(add(X1,X2)),inverse(add(inverse(inverse(add(X1,inverse(add(inverse(X0),inverse(add(X0,X3))))))),inverse(add(inverse(add(X1,inverse(add(inverse(X0),inverse(add(X0,X3)))))),X4))))))))=inverse(add(X1,inverse(add(inverse(X0),inverse(add(X0,X3)))))))),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f3,f3])).
% 43.81/6.23 fof(f15,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(X0)),X1)),X0)),X2)),inverse(X0))),X0))=inverse(X0))),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f3,f3])).
% 43.81/6.23 fof(f18,plain,(
% 43.81/6.23 ![X0]: (inverse(add(inverse(add(X0,inverse(X0))),X0))=inverse(X0))),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f3,f15])).
% 43.81/6.23 fof(f39,plain,(
% 43.81/6.23 ![X0,X1]: (inverse(add(inverse(X0),inverse(add(X0,inverse(add(inverse(X0),inverse(add(X0,X1))))))))=X0)),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f18,f3])).
% 43.81/6.23 fof(f57,plain,(
% 43.81/6.23 ![X0]: (inverse(add(inverse(X0),inverse(add(X0,X0))))=X0)),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f39,f39])).
% 43.81/6.23 fof(f69,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(X0,X1)),X2)),inverse(add(X0,X2))))=X2)),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f39,f3])).
% 43.81/6.23 fof(f125,plain,(
% 43.81/6.23 ![X0,X1,X2,X3,X4,X5]: (inverse(add(X0,inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(inverse(add(inverse(X0),inverse(add(X0,X1)))))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),X4)),inverse(add(inverse(inverse(inverse(add(inverse(X0),inverse(add(X0,X1)))))),inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(inverse(add(inverse(X0),inverse(add(X0,X1)))))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X5))))))))=inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(inverse(add(inverse(X0),inverse(add(X0,X1)))))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),inverse(add(inverse(X0),inverse(add(X0,X1)))))))),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f15,f13])).
% 43.81/6.23 fof(f183,plain,(
% 43.81/6.23 ![X0,X1,X2,X3,X4,X5]: (inverse(add(X0,inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(inverse(add(inverse(X0),inverse(add(X0,X1)))))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),X4)),inverse(add(inverse(inverse(inverse(add(inverse(X0),inverse(add(X0,X1)))))),inverse(add(inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))),X5))))))))=inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(inverse(add(inverse(X0),inverse(add(X0,X1)))))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),inverse(add(inverse(X0),inverse(add(X0,X1)))))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f15,f125])).
% 43.81/6.23 fof(f184,plain,(
% 43.81/6.23 ![X0,X1,X2,X3,X4,X5]: (inverse(add(X0,inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(inverse(add(inverse(X0),inverse(add(X0,X1)))))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),X4)),inverse(add(inverse(inverse(inverse(add(inverse(X0),inverse(add(X0,X1)))))),inverse(add(inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))),X5))))))))=inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f15,f183])).
% 43.81/6.23 fof(f281,plain,(
% 43.81/6.23 ![X0,X1]: (inverse(add(inverse(add(X0,X1)),inverse(add(inverse(X0),X1))))=X1)),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f39,f69])).
% 43.81/6.23 fof(f337,plain,(
% 43.81/6.23 ![X0,X1]: (inverse(add(X0,inverse(add(inverse(inverse(X0)),inverse(add(X0,inverse(add(inverse(X0),inverse(add(X0,X1))))))))))=inverse(add(X0,inverse(add(inverse(X0),inverse(add(X0,X1)))))))),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f39,f281])).
% 43.81/6.23 fof(f346,plain,(
% 43.81/6.23 ![X0]: (inverse(add(inverse(add(X0,inverse(add(X0,X0)))),X0))=inverse(add(X0,X0)))),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f57,f281])).
% 43.81/6.23 fof(f359,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(X0,inverse(add(X1,inverse(add(inverse(inverse(add(inverse(X1),X0))),inverse(add(inverse(add(inverse(X1),X0)),X2))))))))=inverse(add(inverse(X1),X0)))),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f281,f3])).
% 43.81/6.23 fof(f373,plain,(
% 43.81/6.23 ![X0,X1]: (inverse(add(X0,inverse(add(add(inverse(add(X1,X0)),inverse(add(inverse(X1),X0))),add(inverse(add(X1,X0)),inverse(add(inverse(X1),X0)))))))=add(inverse(add(X1,X0)),inverse(add(inverse(X1),X0))))),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f281,f57])).
% 43.81/6.23 fof(f413,plain,(
% 43.81/6.23 ![X0]: (inverse(add(inverse(add(X0,X0)),inverse(add(X0,X0))))=X0)),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f346,f69])).
% 43.81/6.23 fof(f462,plain,(
% 43.81/6.23 ![X0]: (inverse(add(inverse(add(add(X0,X0),inverse(add(X0,X0)))),X0))=inverse(add(X0,X0)))),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f413,f281])).
% 43.81/6.23 fof(f637,plain,(
% 43.81/6.23 ![X0]: (inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0))))=X0)),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f462,f69])).
% 43.81/6.23 fof(f685,plain,(
% 43.81/6.23 ![X0,X1]: (inverse(add(X0,inverse(add(X0,inverse(add(inverse(inverse(add(add(X0,X0),X0))),inverse(add(inverse(add(add(X0,X0),X0)),X1))))))))=inverse(add(add(X0,X0),X0)))),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f637,f3])).
% 43.81/6.23 fof(f688,plain,(
% 43.81/6.23 ![X0]: (inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0))))=add(X0,X0))),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f637,f39])).
% 43.81/6.23 fof(f707,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0))))),X1)),add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0))))),X2)),X0)),add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f637,f15])).
% 43.81/6.23 fof(f708,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),X1)),add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0))))),X2)),inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f637,f15])).
% 43.81/6.23 fof(f730,plain,(
% 43.81/6.23 ![X0,X1]: (inverse(add(X0,inverse(add(inverse(add(X1,X0)),inverse(add(inverse(X1),X0))))))=add(inverse(add(X1,X0)),inverse(add(inverse(X1),X0))))),
% 43.81/6.23 inference(backward_demodulation,[status(thm)],[f813,f373])).
% 43.81/6.23 fof(f755,plain,(
% 43.81/6.23 ![X0,X1]: (inverse(add(X0,inverse(add(X0,inverse(add(inverse(inverse(add(add(X0,X0),X0))),inverse(add(inverse(add(add(X0,X0),X0)),X1))))))))=inverse(add(X0,X0)))),
% 43.81/6.23 inference(backward_demodulation,[status(thm)],[f813,f685])).
% 43.81/6.23 fof(f813,plain,(
% 43.81/6.23 ![X0]: (X0=add(X0,X0))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f637,f688])).
% 43.81/6.23 fof(f926,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),X1)),add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0))))),X2)),X0)),add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f637,f707])).
% 43.81/6.23 fof(f927,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),X1)),add(inverse(X0),inverse(add(add(X0,X0),X0))))),X2)),X0)),add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f926])).
% 43.81/6.23 fof(f928,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),X1)),add(inverse(X0),inverse(add(X0,X0))))),X2)),X0)),add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f927])).
% 43.81/6.23 fof(f929,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),X1)),add(inverse(X0),inverse(X0)))),X2)),X0)),add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f928])).
% 43.81/6.23 fof(f930,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),X1)),inverse(X0))),X2)),X0)),add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f929])).
% 43.81/6.23 fof(f931,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),X1)),inverse(X0))),X2)),X0)),add(inverse(X0),inverse(add(add(X0,X0),X0)))))=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f930])).
% 43.81/6.23 fof(f932,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),X1)),inverse(X0))),X2)),X0)),add(inverse(X0),inverse(add(X0,X0)))))=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f931])).
% 43.81/6.23 fof(f933,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),X1)),inverse(X0))),X2)),X0)),add(inverse(X0),inverse(X0))))=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f932])).
% 43.81/6.23 fof(f934,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),X1)),inverse(X0))),X2)),X0)),inverse(X0)))=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f933])).
% 43.81/6.23 fof(f935,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),X1)),inverse(X0))),X2)),X0)),inverse(X0)))=X0)),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f637,f934])).
% 43.81/6.23 fof(f936,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),X1)),add(inverse(X0),inverse(add(add(X0,X0),X0))))),X2)),inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f708])).
% 43.81/6.23 fof(f937,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),X1)),add(inverse(X0),inverse(add(X0,X0))))),X2)),inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f936])).
% 43.81/6.23 fof(f938,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),X1)),add(inverse(X0),inverse(X0)))),X2)),inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f937])).
% 43.81/6.23 fof(f939,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),X1)),inverse(X0))),X2)),inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f938])).
% 43.81/6.23 fof(f940,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),X1)),inverse(X0))),X2)),X0)),add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f637,f939])).
% 43.81/6.23 fof(f941,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),X1)),inverse(X0))),X2)),X0)),add(inverse(X0),inverse(add(add(X0,X0),X0)))))=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f940])).
% 43.81/6.23 fof(f942,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),X1)),inverse(X0))),X2)),X0)),add(inverse(X0),inverse(add(X0,X0)))))=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f941])).
% 43.81/6.23 fof(f943,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),X1)),inverse(X0))),X2)),X0)),add(inverse(X0),inverse(X0))))=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f942])).
% 43.81/6.23 fof(f944,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),X1)),inverse(X0))),X2)),X0)),inverse(X0)))=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f943])).
% 43.81/6.23 fof(f945,plain,(
% 43.81/6.23 ![X0]: (X0=inverse(add(inverse(add(X0,X0)),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f935,f944])).
% 43.81/6.23 fof(f946,plain,(
% 43.81/6.23 ![X0]: (X0=inverse(add(inverse(X0),inverse(add(add(X0,X0),X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f945])).
% 43.81/6.23 fof(f947,plain,(
% 43.81/6.23 ![X0]: (X0=inverse(add(inverse(X0),inverse(add(X0,X0)))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f946])).
% 43.81/6.23 fof(f948,plain,(
% 43.81/6.23 ![X0]: (X0=inverse(add(inverse(X0),inverse(X0))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f947])).
% 43.81/6.23 fof(f952,plain,(
% 43.81/6.23 ![X0,X1,X2,X3,X4,X5]: (inverse(add(X0,inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(inverse(inverse(add(inverse(X0),inverse(add(X0,X1)))))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),X4)),inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),inverse(add(inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))),X5))))))))=inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),
% 43.81/6.23 inference(backward_demodulation,[status(thm)],[f1013,f184])).
% 43.81/6.23 fof(f965,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(X0,inverse(add(X1,inverse(add(add(inverse(X1),X0),inverse(add(inverse(add(inverse(X1),X0)),X2))))))))=inverse(add(inverse(X1),X0)))),
% 43.81/6.23 inference(backward_demodulation,[status(thm)],[f1013,f359])).
% 43.81/6.23 fof(f1001,plain,(
% 43.81/6.23 ![X0,X1]: (inverse(add(X0,inverse(add(X0,inverse(add(X0,inverse(add(inverse(X0),inverse(add(X0,X1))))))))))=inverse(add(X0,inverse(add(inverse(X0),inverse(add(X0,X1)))))))),
% 43.81/6.23 inference(backward_demodulation,[status(thm)],[f1013,f337])).
% 43.81/6.23 fof(f1013,plain,(
% 43.81/6.23 ![X0]: (X0=inverse(inverse(X0)))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f948])).
% 43.81/6.23 fof(f1084,plain,(
% 43.81/6.23 ![X0,X1]: (inverse(add(X0,X0))=add(inverse(add(X1,X0)),inverse(add(inverse(X1),X0))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f281,f730])).
% 43.81/6.23 fof(f1091,plain,(
% 43.81/6.23 ![X0,X1]: (inverse(X0)=add(inverse(add(X1,X0)),inverse(add(inverse(X1),X0))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f1084])).
% 43.81/6.23 fof(f1185,plain,(
% 43.81/6.23 ![X0,X1]: (inverse(add(X0,inverse(add(X0,inverse(add(add(add(X0,X0),X0),inverse(add(inverse(add(add(X0,X0),X0)),X1))))))))=inverse(add(X0,X0)))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f1013,f755])).
% 43.81/6.23 fof(f1186,plain,(
% 43.81/6.23 ![X0,X1]: (inverse(add(X0,inverse(add(X0,inverse(add(add(X0,X0),inverse(add(inverse(add(add(X0,X0),X0)),X1))))))))=inverse(add(X0,X0)))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f1185])).
% 43.81/6.23 fof(f1187,plain,(
% 43.81/6.23 ![X0,X1]: (inverse(add(X0,inverse(add(X0,inverse(add(X0,inverse(add(inverse(add(add(X0,X0),X0)),X1))))))))=inverse(add(X0,X0)))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f1186])).
% 43.81/6.23 fof(f1188,plain,(
% 43.81/6.23 ![X0,X1]: (inverse(add(X0,inverse(add(X0,inverse(add(X0,inverse(add(inverse(add(X0,X0)),X1))))))))=inverse(add(X0,X0)))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f1187])).
% 43.81/6.23 fof(f1189,plain,(
% 43.81/6.23 ![X0,X1]: (inverse(add(X0,inverse(add(X0,inverse(add(X0,inverse(add(inverse(X0),X1))))))))=inverse(add(X0,X0)))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f1188])).
% 43.81/6.23 fof(f1190,plain,(
% 43.81/6.23 ![X0,X1]: (inverse(add(X0,inverse(add(X0,inverse(add(X0,inverse(add(inverse(X0),X1))))))))=inverse(X0))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f813,f1189])).
% 43.81/6.23 fof(f1493,plain,(
% 43.81/6.23 ![X0,X1,X2,X3,X4,X5]: (inverse(add(X0,inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),X4)),inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),inverse(add(inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))),X5))))))))=inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f1013,f952])).
% 43.81/6.23 fof(f1494,plain,(
% 43.81/6.23 ![X0,X1,X2,X3,X4,X5]: (inverse(add(X0,inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),add(inverse(X0),inverse(add(X0,X1))))),X4)),inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),inverse(add(inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))),X5))))))))=inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f1013,f1493])).
% 43.81/6.23 fof(f1495,plain,(
% 43.81/6.23 ![X0,X1,X2,X3,X4,X5]: (inverse(add(X0,inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),add(inverse(X0),inverse(add(X0,X1))))),X4)),inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),inverse(add(add(inverse(X0),inverse(add(X0,X1))),X5))))))))=inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f1013,f1494])).
% 43.81/6.23 fof(f1496,plain,(
% 43.81/6.23 ![X0,X1,X2,X3,X4,X5]: (inverse(add(X0,inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),X2)),inverse(add(inverse(X0),inverse(add(X0,X1)))))),X3)),add(inverse(X0),inverse(add(X0,X1))))),X4)),inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),inverse(add(add(inverse(X0),inverse(add(X0,X1))),X5))))))))=add(inverse(X0),inverse(add(X0,X1))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f1013,f1495])).
% 43.81/6.23 fof(f1611,plain,(
% 43.81/6.23 ![X0,X1]: (inverse(X0)=inverse(add(X0,inverse(add(inverse(X0),inverse(add(X0,X1)))))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f1190,f1001])).
% 43.81/6.23 fof(f1801,plain,(
% 43.81/6.23 ![X0,X1]: (inverse(X0)=add(inverse(add(inverse(X1),X0)),inverse(add(X1,X0))))),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f1013,f1091])).
% 43.81/6.23 fof(f2257,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(X0,inverse(add(inverse(inverse(add(inverse(X0),inverse(add(X0,X1))))),inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),inverse(add(add(inverse(X0),inverse(add(X0,X1))),X2))))))))=add(inverse(X0),inverse(add(X0,X1))))),
% 43.81/6.23 inference(paramodulation,[status(thm)],[f1801,f1496])).
% 43.81/6.23 fof(f2455,plain,(
% 43.81/6.23 ![X0,X1,X2]: (inverse(add(X0,inverse(add(add(inverse(X0),inverse(add(X0,X1))),inverse(add(inverse(add(inverse(X0),inverse(add(X0,X1)))),inverse(add(add(inverse(X0),inverse(add(X0,X1))),X2))))))))=add(inverse(X0),inverse(add(X0,X1))))),
% 43.81/6.23 inference(forward_demodulation,[status(thm)],[f1013,f2257])).
% 43.81/6.30 fof(f2456,plain,(
% 43.81/6.30 ![X0,X1]: (inverse(add(X0,inverse(add(inverse(X0),inverse(add(X0,X1))))))=add(inverse(X0),inverse(add(X0,X1))))),
% 43.81/6.30 inference(forward_demodulation,[status(thm)],[f1611,f2455])).
% 43.81/6.30 fof(f2518,plain,(
% 43.81/6.30 ![X0,X1]: (inverse(X0)=add(inverse(X0),inverse(add(X0,X1))))),
% 43.81/6.30 inference(forward_demodulation,[status(thm)],[f1611,f2456])).
% 43.81/6.30 fof(f9910,plain,(
% 43.81/6.30 ![X0,X1]: (inverse(inverse(X0))=add(X0,inverse(add(inverse(X0),X1))))),
% 43.81/6.30 inference(paramodulation,[status(thm)],[f1013,f2518])).
% 43.81/6.30 fof(f9962,plain,(
% 43.81/6.30 ![X0,X1]: (inverse(add(X0,inverse(add(X1,inverse(add(inverse(X1),X0))))))=inverse(add(inverse(X1),X0)))),
% 43.81/6.30 inference(backward_demodulation,[status(thm)],[f9998,f965])).
% 43.81/6.30 fof(f9998,plain,(
% 43.81/6.30 ![X0,X1]: (X0=add(X0,inverse(add(inverse(X0),X1))))),
% 43.81/6.30 inference(forward_demodulation,[status(thm)],[f1013,f9910])).
% 43.81/6.30 fof(f10231,plain,(
% 43.81/6.30 ~add(inverse(add(inverse(a),b)),inverse(add(inverse(b),inverse(a))))=a),
% 43.81/6.30 inference(backward_demodulation,[status(thm)],[f10279,f4])).
% 43.81/6.30 fof(f10279,plain,(
% 43.81/6.30 ![X0,X1]: (inverse(add(X0,inverse(X1)))=inverse(add(inverse(X1),X0)))),
% 43.81/6.30 inference(forward_demodulation,[status(thm)],[f9998,f9962])).
% 43.81/6.30 fof(f10400,plain,(
% 43.81/6.30 ~add(inverse(add(b,inverse(a))),inverse(add(inverse(b),inverse(a))))=a),
% 43.81/6.30 inference(forward_demodulation,[status(thm)],[f10279,f10231])).
% 43.81/6.30 fof(f10401,plain,(
% 43.81/6.30 ~inverse(inverse(a))=a),
% 43.81/6.30 inference(forward_demodulation,[status(thm)],[f1091,f10400])).
% 43.81/6.30 fof(f10402,plain,(
% 43.81/6.30 ~a=a),
% 43.81/6.30 inference(forward_demodulation,[status(thm)],[f1013,f10401])).
% 43.81/6.30 fof(f10403,plain,(
% 43.81/6.30 $false),
% 43.81/6.30 inference(trivial_equality_resolution,[status(thm)],[f10402])).
% 43.81/6.30 % SZS output end CNFRefutation for theBenchmark.p
% 8.86/6.50 % Elapsed time: 6.027170 seconds
% 8.86/6.50 % CPU time: 47.067100 seconds
% 8.86/6.50 % Total memory used: 1.114 GB
% 8.86/6.50 % Net memory used: 1.082 GB
%------------------------------------------------------------------------------