%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP418-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 : n009.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:36 PM UTC 2026
% Result : Unsatisfiable 1.75s 0.85s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP418-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.15/0.42 % Computer : n009.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Sun Sep 20 20:13:12 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.43 % Drodi V4.1.1
% 1.75/0.85 % Refutation found
% 1.75/0.85 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.75/0.85 % SZS output start CNFRefutation for theBenchmark
% 1.75/0.85 fof(f1,axiom,(
% 1.75/0.85 (![A,B,C]: (inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),multiply(A,C))) = B ))),
% 1.75/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.75/0.85 fof(f2,negated_conjecture,(
% 1.75/0.85 multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
% 1.75/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.75/0.85 fof(f3,plain,(
% 1.75/0.85 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2)))=X1)),
% 1.75/0.85 inference(cnf_transformation,[status(thm)],[f1])).
% 1.75/0.85 fof(f4,plain,(
% 1.75/0.85 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)),
% 1.75/0.85 inference(cnf_transformation,[status(thm)],[f2])).
% 1.75/0.85 fof(f5,definition,(
% 1.75/0.85 sF1_fnc=inverse(a1)),
% 1.75/0.85 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 1.75/0.85 fof(f6,definition,(
% 1.75/0.85 sF0_fnc=multiply(sF1_fnc,a1)),
% 1.75/0.85 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 1.75/0.85 fof(f7,definition,(
% 1.75/0.85 sF3_fnc=inverse(b1)),
% 1.75/0.85 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 1.75/0.85 fof(f8,definition,(
% 1.75/0.85 sF2_fnc=multiply(sF3_fnc,b1)),
% 1.75/0.85 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 1.75/0.85 fof(f9,plain,(
% 1.75/0.85 ~sF0_fnc=sF2_fnc),
% 1.75/0.85 inference(definition_folding,[],[f4,f8,f7,f6,f5])).
% 1.75/0.85 fof(f15,plain,(
% 1.75/0.85 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(a1,inverse(multiply(sF1_fnc,a1)))))))),multiply(X0,a1)))=X1)),
% 1.75/0.85 inference(paramodulation,[status(thm)],[f5,f3])).
% 1.75/0.85 fof(f16,plain,(
% 1.75/0.85 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(multiply(inverse(a1),a1)))))))),sF0_fnc))=X0)),
% 1.75/0.85 inference(paramodulation,[status(thm)],[f6,f3])).
% 1.75/0.85 fof(f18,plain,(
% 1.75/0.85 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(a1,inverse(sF0_fnc))))))),multiply(X0,a1)))=X1)),
% 1.75/0.85 inference(forward_demodulation,[status(thm)],[f6,f15])).
% 1.75/0.85 fof(f19,plain,(
% 1.75/0.85 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(multiply(sF1_fnc,a1)))))))),sF0_fnc))=X0)),
% 1.75/0.85 inference(forward_demodulation,[status(thm)],[f5,f16])).
% 1.75/0.85 fof(f20,plain,(
% 1.75/0.85 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc))=X0)),
% 1.75/0.85 inference(forward_demodulation,[status(thm)],[f6,f19])).
% 1.75/0.85 fof(f21,plain,(
% 1.75/0.85 ![X0]: (inverse(multiply(inverse(multiply(sF3_fnc,inverse(multiply(inverse(X0),inverse(multiply(b1,inverse(multiply(inverse(b1),b1)))))))),sF2_fnc))=X0)),
% 1.75/0.85 inference(paramodulation,[status(thm)],[f8,f3])).
% 1.75/0.85 fof(f22,plain,(
% 1.75/0.85 ![X0]: (inverse(multiply(inverse(multiply(sF3_fnc,inverse(multiply(inverse(X0),inverse(multiply(b1,inverse(multiply(sF3_fnc,b1)))))))),sF2_fnc))=X0)),
% 1.75/0.85 inference(forward_demodulation,[status(thm)],[f7,f21])).
% 1.75/0.85 fof(f23,plain,(
% 1.75/0.85 ![X0]: (inverse(multiply(inverse(multiply(sF3_fnc,inverse(multiply(inverse(X0),inverse(multiply(b1,inverse(sF2_fnc))))))),sF2_fnc))=X0)),
% 1.75/0.85 inference(forward_demodulation,[status(thm)],[f8,f22])).
% 1.75/0.85 fof(f24,plain,(
% 1.75/0.85 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc))=multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc))),
% 1.75/0.85 inference(paramodulation,[status(thm)],[f20,f20])).
% 1.75/0.85 fof(f25,plain,(
% 1.75/0.85 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc))=multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2)))),
% 1.75/0.85 inference(paramodulation,[status(thm)],[f3,f20])).
% 1.75/0.85 fof(f26,plain,(
% 1.75/0.85 inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(sF3_fnc,inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc))=b1),
% 1.75/0.85 inference(paramodulation,[status(thm)],[f7,f20])).
% 1.75/0.85 fof(f27,plain,(
% 1.75/0.85 inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(sF1_fnc,inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc))=a1),
% 1.75/0.85 inference(paramodulation,[status(thm)],[f5,f20])).
% 1.75/0.85 fof(f30,plain,(
% 1.75/0.85 ![X0]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(inverse(X0)),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc)=X0)),
% 1.75/0.85 inference(backward_demodulation,[status(thm)],[f24,f20])).
% 1.75/0.85 fof(f34,plain,(
% 1.75/0.85 ![X0,X1,X2]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc)=multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2)))),
% 1.75/0.85 inference(forward_demodulation,[status(thm)],[f24,f25])).
% 1.75/0.85 fof(f35,plain,(
% 1.75/0.85 multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(sF3_fnc),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc)=b1),
% 1.75/0.85 inference(forward_demodulation,[status(thm)],[f24,f26])).
% 1.75/0.85 fof(f36,plain,(
% 1.75/0.85 multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(sF1_fnc),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc)=a1),
% 1.75/0.85 inference(forward_demodulation,[status(thm)],[f24,f27])).
% 1.75/0.85 fof(f53,plain,(
% 1.75/0.85 ![X0]: (inverse(multiply(inverse(multiply(sF3_fnc,inverse(multiply(X0,inverse(multiply(b1,inverse(sF2_fnc))))))),sF2_fnc))=multiply(inverse(multiply(sF3_fnc,inverse(multiply(inverse(X0),inverse(multiply(b1,inverse(sF2_fnc))))))),sF2_fnc))),
% 1.75/0.85 inference(paramodulation,[status(thm)],[f23,f23])).
% 1.75/0.85 fof(f58,plain,(
% 1.75/0.85 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(a1,inverse(sF0_fnc))))))),multiply(X0,a1)))=multiply(inverse(multiply(sF3_fnc,inverse(multiply(inverse(X1),inverse(multiply(b1,inverse(sF2_fnc))))))),sF2_fnc))),
% 1.75/0.85 inference(paramodulation,[status(thm)],[f23,f18])).
% 1.75/0.85 fof(f60,plain,(
% 1.75/0.85 ![X0]: (multiply(inverse(multiply(sF3_fnc,inverse(multiply(inverse(inverse(X0)),inverse(multiply(b1,inverse(sF2_fnc))))))),sF2_fnc)=X0)),
% 1.75/0.85 inference(backward_demodulation,[status(thm)],[f53,f23])).
% 1.75/0.85 fof(f84,plain,(
% 1.75/0.85 ![X0]: (multiply(inverse(multiply(sF3_fnc,inverse(multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc)),inverse(multiply(b1,inverse(sF2_fnc))))))),sF2_fnc)=multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc))),
% 1.75/0.85 inference(paramodulation,[status(thm)],[f24,f60])).
% 1.75/0.85 fof(f88,plain,(
% 1.75/0.85 ![X0]: (multiply(inverse(multiply(sF3_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(inverse(X0)),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc),inverse(multiply(b1,inverse(sF2_fnc))))))),sF2_fnc)=multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc))),
% 1.75/0.85 inference(forward_demodulation,[status(thm)],[f24,f84])).
% 1.75/0.85 fof(f93,plain,(
% 1.75/0.85 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(a1,inverse(sF0_fnc))))))),multiply(X0,a1)))=multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X1),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc))),
% 1.75/0.85 inference(backward_demodulation,[status(thm)],[f97,f58])).
% 1.75/0.85 fof(f97,plain,(
% 1.75/0.85 ![X0]: (multiply(inverse(multiply(sF3_fnc,inverse(multiply(X0,inverse(multiply(b1,inverse(sF2_fnc))))))),sF2_fnc)=multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc))),
% 1.75/0.85 inference(forward_demodulation,[status(thm)],[f30,f88])).
% 1.75/0.85 fof(f106,plain,(
% 1.75/0.85 ![X0,X1]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc)=multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(inverse(X1)),inverse(multiply(a1,inverse(sF0_fnc))))))),inverse(multiply(inverse(X0),inverse(multiply(sF0_fnc,inverse(multiply(inverse(sF0_fnc),sF0_fnc)))))))),X1))),
% 1.75/0.85 inference(paramodulation,[status(thm)],[f30,f34])).
% 1.75/0.85 fof(f107,plain,(
% 1.75/0.85 ![X0]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc)=multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(sF1_fnc),inverse(multiply(a1,inverse(sF0_fnc))))))),inverse(multiply(inverse(X0),inverse(multiply(sF0_fnc,inverse(multiply(inverse(sF0_fnc),sF0_fnc)))))))),a1))),
% 1.75/0.85 inference(paramodulation,[status(thm)],[f36,f34])).
% 1.75/0.85 fof(f245,plain,(
% 1.75/0.85 ![X0,X1]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc)),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc)=multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(a1,inverse(sF0_fnc))))))),multiply(X1,a1)))),
% 1.75/0.85 inference(paramodulation,[status(thm)],[f93,f30])).
% 1.75/0.85 fof(f246,plain,(
% 1.75/0.85 ![X0,X1]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(inverse(X0)),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc)=multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(a1,inverse(sF0_fnc))))))),multiply(X1,a1)))),
% 1.75/0.85 inference(forward_demodulation,[status(thm)],[f24,f245])).
% 1.75/0.85 fof(f249,plain,(
% 1.75/0.85 ![X0,X1]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc)=multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(a1,inverse(sF0_fnc))))))),multiply(X1,a1)))),
% 1.75/0.85 inference(forward_demodulation,[status(thm)],[f30,f246])).
% 1.75/0.85 fof(f324,plain,(
% 1.75/0.85 ![X0,X1]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(inverse(inverse(multiply(a1,inverse(sF0_fnc))))),inverse(multiply(a1,inverse(sF0_fnc))))))),inverse(multiply(inverse(X0),inverse(multiply(sF0_fnc,inverse(multiply(inverse(sF0_fnc),sF0_fnc)))))))),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc)=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc)))),multiply(X1,a1)))),
% 1.75/0.85 inference(paramodulation,[status(thm)],[f106,f249])).
% 1.75/0.85 fof(f354,plain,(
% 1.75/0.85 ![X0,X1]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc)))),sF0_fnc)=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc)))),multiply(X1,a1)))),
% 1.75/0.85 inference(forward_demodulation,[status(thm)],[f106,f324])).
% 1.75/0.85 fof(f355,plain,(
% 1.75/0.85 ![X0,X1]: (multiply(inverse(multiply(sF1_fnc,multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(inverse(X0)),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc))),sF0_fnc)=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc)))),multiply(X1,a1)))),
% 1.75/0.85 inference(forward_demodulation,[status(thm)],[f24,f354])).
% 1.75/0.85 fof(f356,plain,(
% 1.75/0.85 ![X0,X1]: (multiply(inverse(multiply(sF1_fnc,X0)),sF0_fnc)=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc)))),multiply(X1,a1)))),
% 1.75/0.85 inference(forward_demodulation,[status(thm)],[f30,f355])).
% 1.75/0.85 fof(f357,plain,(
% 1.75/0.85 ![X0,X1]: (multiply(inverse(multiply(sF1_fnc,X0)),sF0_fnc)=multiply(inverse(multiply(X1,multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(inverse(X0)),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc))),multiply(X1,a1)))),
% 1.75/0.85 inference(forward_demodulation,[status(thm)],[f24,f356])).
% 1.75/0.85 fof(f359,plain,(
% 1.75/0.85 ![X0,X1]: (multiply(inverse(multiply(sF1_fnc,X0)),sF0_fnc)=multiply(inverse(multiply(X1,X0)),multiply(X1,a1)))),
% 1.75/0.85 inference(forward_demodulation,[status(thm)],[f30,f357])).
% 1.75/0.85 fof(f430,plain,(
% 1.75/0.85 ![X0]: (multiply(inverse(multiply(sF1_fnc,a1)),sF0_fnc)=multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc)),multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(sF1_fnc),inverse(multiply(a1,inverse(sF0_fnc))))))),inverse(multiply(inverse(X0),inverse(multiply(sF0_fnc,inverse(multiply(inverse(sF0_fnc),sF0_fnc)))))))),a1)))),
% 1.75/0.86 inference(paramodulation,[status(thm)],[f107,f359])).
% 1.75/0.86 fof(f437,plain,(
% 1.75/0.86 ![X0]: (multiply(inverse(sF0_fnc),sF0_fnc)=multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc)),multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(sF1_fnc),inverse(multiply(a1,inverse(sF0_fnc))))))),inverse(multiply(inverse(X0),inverse(multiply(sF0_fnc,inverse(multiply(inverse(sF0_fnc),sF0_fnc)))))))),a1)))),
% 1.75/0.86 inference(forward_demodulation,[status(thm)],[f6,f430])).
% 1.75/0.86 fof(f438,plain,(
% 1.75/0.86 ![X0]: (multiply(inverse(sF0_fnc),sF0_fnc)=multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(inverse(X0)),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc),multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(sF1_fnc),inverse(multiply(a1,inverse(sF0_fnc))))))),inverse(multiply(inverse(X0),inverse(multiply(sF0_fnc,inverse(multiply(inverse(sF0_fnc),sF0_fnc)))))))),a1)))),
% 1.75/0.86 inference(forward_demodulation,[status(thm)],[f24,f437])).
% 1.75/0.86 fof(f439,plain,(
% 1.75/0.86 ![X0]: (multiply(inverse(sF0_fnc),sF0_fnc)=multiply(X0,multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(sF1_fnc),inverse(multiply(a1,inverse(sF0_fnc))))))),inverse(multiply(inverse(X0),inverse(multiply(sF0_fnc,inverse(multiply(inverse(sF0_fnc),sF0_fnc)))))))),a1)))),
% 1.75/0.86 inference(forward_demodulation,[status(thm)],[f30,f438])).
% 1.75/0.86 fof(f443,plain,(
% 1.75/0.86 ![X0]: (multiply(inverse(sF0_fnc),sF0_fnc)=multiply(X0,multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF0_fnc))))))),sF0_fnc)))),
% 1.75/0.86 inference(forward_demodulation,[status(thm)],[f107,f439])).
% 1.75/0.86 fof(f1067,plain,(
% 1.75/0.86 multiply(inverse(sF0_fnc),sF0_fnc)=multiply(sF1_fnc,a1)),
% 1.75/0.86 inference(paramodulation,[status(thm)],[f36,f443])).
% 1.75/0.86 fof(f1068,plain,(
% 1.75/0.86 multiply(inverse(sF0_fnc),sF0_fnc)=multiply(sF3_fnc,b1)),
% 1.75/0.86 inference(paramodulation,[status(thm)],[f35,f443])).
% 1.75/0.86 fof(f1136,plain,(
% 1.75/0.86 multiply(inverse(sF0_fnc),sF0_fnc)=sF0_fnc),
% 1.75/0.86 inference(forward_demodulation,[status(thm)],[f6,f1067])).
% 1.75/0.86 fof(f1137,plain,(
% 1.75/0.86 sF2_fnc=sF0_fnc),
% 1.75/0.86 inference(backward_demodulation,[status(thm)],[f1138,f8])).
% 1.75/0.86 fof(f1138,plain,(
% 1.75/0.86 sF0_fnc=multiply(sF3_fnc,b1)),
% 1.75/0.86 inference(forward_demodulation,[status(thm)],[f1136,f1068])).
% 1.75/0.86 fof(f1195,plain,(
% 1.75/0.86 $false),
% 1.75/0.86 inference(forward_subsumption_resolution,[status(thm)],[f1137,f9])).
% 1.75/0.86 % SZS output end CNFRefutation for theBenchmark.p
% 1.04/0.89 % Elapsed time: 0.448468 seconds
% 1.04/0.89 % CPU time: 3.345452 seconds
% 1.04/0.89 % Total memory used: 161.935 MB
% 1.04/0.89 % Net memory used: 157.589 MB
%------------------------------------------------------------------------------