%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP437-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 : n013.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:37 PM UTC 2026
% Result : Unsatisfiable 46.08s 6.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP437-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n013.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 20:12:36 UTC 2026
% 0.14/0.37 % CPUTime :
% 0.14/0.37 % Drodi V4.1.1
% 46.08/6.42 % Refutation found
% 46.08/6.42 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 46.08/6.42 % SZS output start CNFRefutation for theBenchmark
% 46.08/6.42 fof(f1,axiom,(
% 46.08/6.42 (![A,B,C,D]: (multiply(A,inverse(multiply(B,multiply(C,multiply(multiply(inverse(C),inverse(multiply(D,B))),A))))) = D ))),
% 46.08/6.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.08/6.42 fof(f2,negated_conjecture,(
% 46.08/6.42 multiply(multiply(inverse(b2),b2),a2) != a2 ),
% 46.08/6.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.08/6.42 fof(f3,plain,(
% 46.08/6.42 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,X1))),X0)))))=X3)),
% 46.08/6.42 inference(cnf_transformation,[status(thm)],[f1])).
% 46.08/6.42 fof(f4,plain,(
% 46.08/6.42 ~multiply(multiply(inverse(b2),b2),a2)=a2),
% 46.08/6.42 inference(cnf_transformation,[status(thm)],[f2])).
% 46.08/6.42 fof(f5,definition,(
% 46.08/6.42 sF2_fnc=inverse(b2)),
% 46.08/6.42 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 46.08/6.42 fof(f6,definition,(
% 46.08/6.42 sF1_fnc=multiply(sF2_fnc,b2)),
% 46.08/6.42 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 46.08/6.42 fof(f7,definition,(
% 46.08/6.42 sF0_fnc=multiply(sF1_fnc,a2)),
% 46.08/6.42 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 46.08/6.42 fof(f8,plain,(
% 46.08/6.42 ~sF0_fnc=a2),
% 46.08/6.42 inference(definition_folding,[],[f4,f7,f6,f5])).
% 46.08/6.42 fof(f10,plain,(
% 46.08/6.42 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(X2,X3))),inverse(X4))),multiply(X4,multiply(X2,X0)))))=X3)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f3,f3])).
% 46.08/6.42 fof(f11,plain,(
% 46.08/6.42 ![X0,X1,X2]: (multiply(X0,inverse(multiply(X1,multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(X2,X1))),X0)))))=X2)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f5,f3])).
% 46.08/6.42 fof(f12,plain,(
% 46.08/6.42 ![X0,X1]: (multiply(X0,inverse(multiply(a2,multiply(X1,multiply(multiply(inverse(X1),inverse(sF0_fnc)),X0)))))=sF1_fnc)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f7,f3])).
% 46.08/6.42 fof(f13,plain,(
% 46.08/6.42 ![X0,X1]: (multiply(X0,inverse(multiply(b2,multiply(X1,multiply(multiply(inverse(X1),inverse(sF1_fnc)),X0)))))=sF2_fnc)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f6,f3])).
% 46.08/6.42 fof(f19,plain,(
% 46.08/6.42 ![X0]: (multiply(X0,inverse(multiply(a2,multiply(b2,multiply(multiply(sF2_fnc,inverse(sF0_fnc)),X0)))))=sF1_fnc)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f7,f11])).
% 46.08/6.42 fof(f23,plain,(
% 46.08/6.42 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(X1,X2))),inverse(X3))),multiply(X3,multiply(X1,X0)))))=X2)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f11,f3])).
% 46.08/6.42 fof(f25,plain,(
% 46.08/6.42 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(inverse(multiply(X1,multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(X2,X1))),X3)))),multiply(X4,multiply(multiply(inverse(X4),inverse(X2)),X0)))))=X3)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f11,f3])).
% 46.08/6.42 fof(f34,plain,(
% 46.08/6.42 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(multiply(a2,multiply(X1,multiply(multiply(inverse(X1),inverse(sF0_fnc)),X2)))),multiply(b2,multiply(multiply(sF2_fnc,inverse(sF1_fnc)),X0)))))=X2)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f12,f11])).
% 46.08/6.42 fof(f41,plain,(
% 46.08/6.42 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(X1,multiply(multiply(inverse(X1),inverse(sF1_fnc)),inverse(X2))),multiply(X2,multiply(sF2_fnc,X0)))))=b2)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f13,f3])).
% 46.08/6.42 fof(f88,plain,(
% 46.08/6.42 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X3))),multiply(X3,multiply(X4,X0)))))=multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(X2,X4))),inverse(X1))))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f11,f10])).
% 46.08/6.42 fof(f95,plain,(
% 46.08/6.42 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(multiply(X1,multiply(multiply(inverse(X1),inverse(sF2_fnc)),inverse(X2))),multiply(X2,multiply(X3,X0)))))=inverse(multiply(b2,multiply(X4,multiply(multiply(inverse(X4),inverse(sF1_fnc)),X3)))))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f13,f10])).
% 46.08/6.42 fof(f98,plain,(
% 46.08/6.42 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(multiply(X1,multiply(multiply(inverse(X1),inverse(X2)),inverse(X3))),multiply(X3,multiply(X4,X0)))))=inverse(multiply(X5,multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(X2,X5))),X4)))))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f11,f10])).
% 46.08/6.42 fof(f102,plain,(
% 46.08/6.42 ![X0,X1,X2]: (multiply(b2,inverse(multiply(multiply(X0,multiply(multiply(inverse(X0),inverse(multiply(sF2_fnc,X1))),inverse(X2))),multiply(X2,sF1_fnc))))=X1)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f6,f10])).
% 46.08/6.42 fof(f245,plain,(
% 46.08/6.42 ![X0,X1]: (multiply(b2,inverse(multiply(multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(sF2_fnc,X0))),inverse(X1))),multiply(X1,sF1_fnc))))=X0)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f6,f23])).
% 46.08/6.42 fof(f660,plain,(
% 46.08/6.42 ![X0,X1]: (multiply(b2,inverse(multiply(multiply(X0,multiply(multiply(inverse(X0),inverse(sF1_fnc)),inverse(X1))),multiply(X1,sF1_fnc))))=b2)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f6,f41])).
% 46.08/6.42 fof(f737,plain,(
% 46.08/6.42 ![X0]: (multiply(b2,inverse(multiply(multiply(b2,multiply(multiply(sF2_fnc,inverse(sF1_fnc)),inverse(X0))),multiply(X0,sF1_fnc))))=b2)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f5,f660])).
% 46.08/6.42 fof(f1876,plain,(
% 46.08/6.42 ![X0,X1]: (multiply(b2,inverse(multiply(multiply(X0,multiply(multiply(inverse(X0),inverse(sF1_fnc)),inverse(X1))),multiply(X1,sF1_fnc))))=inverse(multiply(a2,multiply(b2,multiply(multiply(sF2_fnc,inverse(sF0_fnc)),sF2_fnc)))))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f19,f102])).
% 46.08/6.42 fof(f1906,plain,(
% 46.08/6.42 b2=inverse(multiply(a2,multiply(b2,multiply(multiply(sF2_fnc,inverse(sF0_fnc)),sF2_fnc))))),
% 46.08/6.42 inference(forward_demodulation,[status(thm)],[f660,f1876])).
% 46.08/6.42 fof(f4641,plain,(
% 46.08/6.42 ![X0,X1]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(sF2_fnc,inverse(multiply(X0,X1))),X0))),inverse(b2)))=X1)),
% 46.08/6.42 inference(backward_demodulation,[status(thm)],[f88,f23])).
% 46.08/6.42 fof(f4644,plain,(
% 46.08/6.42 ![X0,X1,X2]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(inverse(X0),inverse(multiply(X1,X2))),X1))),inverse(X0)))=X2)),
% 46.08/6.42 inference(backward_demodulation,[status(thm)],[f88,f10])).
% 46.08/6.42 fof(f4645,plain,(
% 46.08/6.42 ![X0,X1,X2]: (X0=multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(X1,multiply(sF2_fnc,inverse(multiply(X0,multiply(X2,multiply(X1,inverse(b2))))))))),inverse(X2))))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f11,f88])).
% 46.08/6.42 fof(f4820,plain,(
% 46.08/6.42 ![X0,X1]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(sF2_fnc,inverse(multiply(X0,X1))),X0))),sF2_fnc))=X1)),
% 46.08/6.42 inference(forward_demodulation,[status(thm)],[f5,f4641])).
% 46.08/6.42 fof(f4821,plain,(
% 46.08/6.42 ![X0,X1,X2]: (X0=multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(X1,multiply(sF2_fnc,inverse(multiply(X0,multiply(X2,multiply(X1,sF2_fnc)))))))),inverse(X2))))),
% 46.08/6.42 inference(forward_demodulation,[status(thm)],[f5,f4645])).
% 46.08/6.42 fof(f4836,plain,(
% 46.08/6.42 ![X0,X1,X2,X3,X4]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(X1,multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(X2,X1))),X0))))))),inverse(X3)))=multiply(X4,multiply(multiply(inverse(X4),inverse(X2)),inverse(X3))))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f25,f4644])).
% 46.08/6.42 fof(f4851,plain,(
% 46.08/6.42 ![X0,X1]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(b2,inverse(multiply(X0,X1))),X0))),inverse(multiply(a2,multiply(b2,multiply(multiply(sF2_fnc,inverse(sF0_fnc)),sF2_fnc))))))=X1)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f1906,f4644])).
% 46.08/6.42 fof(f4941,plain,(
% 46.08/6.42 ![X0,X1,X2]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(X0)),inverse(X1)))=multiply(X2,multiply(multiply(inverse(X2),inverse(X0)),inverse(X1))))),
% 46.08/6.42 inference(forward_demodulation,[status(thm)],[f11,f4836])).
% 46.08/6.42 fof(f4946,plain,(
% 46.08/6.42 ![X0,X1]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(b2,inverse(multiply(X0,X1))),X0))),b2))=X1)),
% 46.08/6.42 inference(forward_demodulation,[status(thm)],[f1906,f4851])).
% 46.08/6.42 fof(f5321,plain,(
% 46.08/6.42 ![X0,X1,X2,X3]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(X1,multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(X2,X1))),X0))))))),sF2_fnc))=multiply(X3,multiply(multiply(inverse(X3),inverse(X2)),sF2_fnc)))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f25,f4820])).
% 46.08/6.42 fof(f5426,plain,(
% 46.08/6.42 ![X0,X1]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(X0)),sF2_fnc))=multiply(X1,multiply(multiply(inverse(X1),inverse(X0)),sF2_fnc)))),
% 46.08/6.42 inference(forward_demodulation,[status(thm)],[f11,f5321])).
% 46.08/6.42 fof(f5452,plain,(
% 46.08/6.42 ![X0,X1,X2,X3]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(X1,multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(X2,X1))),X0))))))),b2))=multiply(X3,multiply(multiply(inverse(X3),inverse(X2)),b2)))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f25,f4946])).
% 46.08/6.42 fof(f5561,plain,(
% 46.08/6.42 ![X0,X1]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(X0)),b2))=multiply(X1,multiply(multiply(inverse(X1),inverse(X0)),b2)))),
% 46.08/6.42 inference(forward_demodulation,[status(thm)],[f11,f5452])).
% 46.08/6.42 fof(f6713,plain,(
% 46.08/6.42 ![X0,X1,X2]: (multiply(inverse(X0),inverse(multiply(multiply(sF2_fnc,inverse(multiply(X1,multiply(X0,multiply(X2,sF2_fnc))))),X1)))=X2)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f4821,f11])).
% 46.08/6.42 fof(f6774,plain,(
% 46.08/6.42 ![X0,X1]: (multiply(sF2_fnc,inverse(multiply(multiply(sF2_fnc,inverse(multiply(X0,multiply(b2,multiply(X1,sF2_fnc))))),X0)))=X1)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f5,f6713])).
% 46.08/6.42 fof(f6806,plain,(
% 46.08/6.42 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(X1,multiply(X2,multiply(X3,X0)))))=multiply(sF2_fnc,inverse(multiply(X1,multiply(X2,multiply(X3,sF2_fnc))))))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f6713,f3])).
% 46.08/6.42 fof(f8605,plain,(
% 46.08/6.42 ![X0,X1,X2]: (multiply(sF2_fnc,inverse(multiply(multiply(X0,inverse(multiply(X1,multiply(b2,multiply(X2,X0))))),X1)))=X2)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f6806,f6774])).
% 46.08/6.42 fof(f8606,plain,(
% 46.08/6.42 ![X0,X1,X2,X3]: (multiply(inverse(X0),inverse(multiply(multiply(X1,inverse(multiply(X2,multiply(X0,multiply(X3,X1))))),X2)))=X3)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f6806,f6713])).
% 46.08/6.42 fof(f8607,plain,(
% 46.08/6.42 ![X0,X1,X2,X3]: (X0=multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(X1,multiply(X2,inverse(multiply(X0,multiply(X3,multiply(X1,X2)))))))),inverse(X3))))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f6806,f4821])).
% 46.08/6.42 fof(f8807,plain,(
% 46.08/6.42 ![X0,X1,X2,X3]: (multiply(inverse(X0),inverse(multiply(X1,multiply(X2,inverse(multiply(multiply(X0,multiply(X3,sF2_fnc)),multiply(b2,multiply(X1,X2))))))))=X3)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f8605,f6713])).
% 46.08/6.42 fof(f8810,plain,(
% 46.08/6.42 ![X0,X1,X2]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(X0,multiply(X1,inverse(multiply(X2,multiply(b2,multiply(X0,X1)))))))),sF2_fnc))=X2)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f8605,f4820])).
% 46.08/6.42 fof(f16675,plain,(
% 46.08/6.42 ![X0,X1,X2]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(inverse(X0),inverse(sF2_fnc)),X1))),inverse(X0)))=inverse(multiply(b2,multiply(X2,multiply(multiply(inverse(X2),inverse(sF1_fnc)),X1)))))),
% 46.08/6.42 inference(forward_demodulation,[status(thm)],[f88,f95])).
% 46.08/6.42 fof(f16873,plain,(
% 46.08/6.42 ![X0,X1]: (multiply(X0,multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(inverse(X1),inverse(sF2_fnc)),X0))),inverse(X1))))=sF2_fnc)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f16675,f13])).
% 46.08/6.42 fof(f17075,plain,(
% 46.08/6.42 ![X0,X1,X2]: (multiply(multiply(X0,inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(sF2_fnc)),X0))))),X1)=sF2_fnc)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f8607,f16873])).
% 46.08/6.42 fof(f17357,plain,(
% 46.08/6.42 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(X1,multiply(multiply(inverse(X1),inverse(sF2_fnc)),sF2_fnc)),multiply(b2,sF2_fnc))))=X0)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f17075,f11])).
% 46.08/6.42 fof(f17528,plain,(
% 46.08/6.42 ![X0]: (multiply(X0,inverse(multiply(multiply(b2,multiply(multiply(sF2_fnc,inverse(sF2_fnc)),sF2_fnc)),multiply(b2,sF2_fnc))))=X0)),
% 46.08/6.42 inference(forward_demodulation,[status(thm)],[f5426,f17357])).
% 46.08/6.42 fof(f19329,plain,(
% 46.08/6.42 ![X0,X1]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(b2,multiply(multiply(sF2_fnc,inverse(sF2_fnc)),sF2_fnc)),multiply(b2,sF2_fnc)))),inverse(X0)))=multiply(X1,multiply(inverse(X1),inverse(X0))))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f17528,f4941])).
% 46.08/6.42 fof(f19330,plain,(
% 46.08/6.42 ![X0]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(b2,multiply(multiply(sF2_fnc,inverse(sF2_fnc)),sF2_fnc)),multiply(b2,sF2_fnc)))),b2))=multiply(X0,multiply(inverse(X0),b2)))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f17528,f5561])).
% 46.08/6.42 fof(f19496,plain,(
% 46.08/6.42 ![X0,X1]: (multiply(b2,multiply(sF2_fnc,inverse(X0)))=multiply(X1,multiply(inverse(X1),inverse(X0))))),
% 46.08/6.42 inference(forward_demodulation,[status(thm)],[f17528,f19329])).
% 46.08/6.42 fof(f19497,plain,(
% 46.08/6.42 ![X0]: (multiply(b2,multiply(sF2_fnc,b2))=multiply(X0,multiply(inverse(X0),b2)))),
% 46.08/6.42 inference(forward_demodulation,[status(thm)],[f17528,f19330])).
% 46.08/6.42 fof(f19498,plain,(
% 46.08/6.42 ![X0]: (multiply(b2,sF1_fnc)=multiply(X0,multiply(inverse(X0),b2)))),
% 46.08/6.42 inference(forward_demodulation,[status(thm)],[f6,f19497])).
% 46.08/6.42 fof(f19576,plain,(
% 46.08/6.42 ![X0,X1]: (multiply(inverse(X0),inverse(multiply(multiply(b2,inverse(multiply(X1,multiply(b2,sF1_fnc)))),X1)))=inverse(X0))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f19498,f8606])).
% 46.08/6.42 fof(f19853,plain,(
% 46.08/6.42 ![X0]: (multiply(b2,multiply(sF2_fnc,inverse(multiply(multiply(b2,multiply(multiply(sF2_fnc,inverse(sF2_fnc)),sF2_fnc)),multiply(b2,sF2_fnc)))))=multiply(X0,inverse(X0)))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f17528,f19496])).
% 46.08/6.42 fof(f20034,plain,(
% 46.08/6.42 ![X0]: (multiply(b2,sF2_fnc)=multiply(X0,inverse(X0)))),
% 46.08/6.42 inference(forward_demodulation,[status(thm)],[f17528,f19853])).
% 46.08/6.42 fof(f22359,plain,(
% 46.08/6.42 ![X0,X1,X2,X3]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(inverse(X0),inverse(X1)),X2))),inverse(X0)))=inverse(multiply(X3,multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(X1,X3))),X2)))))),
% 46.08/6.42 inference(forward_demodulation,[status(thm)],[f88,f98])).
% 46.08/6.42 fof(f22364,plain,(
% 46.08/6.42 ![X0,X1,X2]: (X0=inverse(multiply(X1,multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(X2,X0),X1))),X2)))))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f4644,f22359])).
% 46.08/6.42 fof(f23760,plain,(
% 46.08/6.42 ![X0,X1,X2]: (X0=inverse(multiply(multiply(X1,inverse(multiply(X2,multiply(b2,multiply(multiply(sF2_fnc,X0),X1))))),X2)))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f8810,f22364])).
% 46.08/6.42 fof(f24034,plain,(
% 46.08/6.42 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(b2,inverse(multiply(X1,multiply(b2,sF1_fnc)))),X1)))=inverse(multiply(X2,multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(X3,X0),X2))),X3)))))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f22364,f19576])).
% 46.08/6.42 fof(f24038,plain,(
% 46.08/6.42 ![X0,X1,X2,X3]: (multiply(b2,multiply(sF2_fnc,inverse(multiply(X0,multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(X1,X2),X0))),X1))))))=multiply(X3,multiply(inverse(X3),X2)))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f22364,f19496])).
% 46.08/6.42 fof(f24117,plain,(
% 46.08/6.42 ![X0,X1,X2,X3,X4]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(X0,multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(X1,X2),X0))),X1)))),inverse(multiply(X3,X4))),X3))),X2))=X4)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f22364,f4644])).
% 46.08/6.42 fof(f24173,plain,(
% 46.08/6.42 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(b2,inverse(multiply(X1,multiply(b2,sF1_fnc)))),X1)))=X0)),
% 46.08/6.42 inference(forward_demodulation,[status(thm)],[f22364,f24034])).
% 46.08/6.42 fof(f24174,plain,(
% 46.08/6.42 ![X0,X1]: (multiply(b2,multiply(sF2_fnc,X0))=multiply(X1,multiply(inverse(X1),X0)))),
% 46.08/6.42 inference(forward_demodulation,[status(thm)],[f22364,f24038])).
% 46.08/6.42 fof(f24190,plain,(
% 46.08/6.42 ![X0,X1,X2]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(X0,inverse(multiply(X1,X2))),X1))),X0))=X2)),
% 46.08/6.42 inference(forward_demodulation,[status(thm)],[f22364,f24117])).
% 46.08/6.42 fof(f24868,plain,(
% 46.08/6.42 ![X0]: (multiply(b2,sF2_fnc)=multiply(multiply(b2,inverse(multiply(X0,multiply(b2,sF1_fnc)))),X0))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f20034,f24173])).
% 46.08/6.42 fof(f25170,plain,(
% 46.08/6.42 ![X0]: (multiply(X0,inverse(multiply(b2,sF2_fnc)))=X0)),
% 46.08/6.42 inference(backward_demodulation,[status(thm)],[f24868,f24173])).
% 46.08/6.42 fof(f25446,plain,(
% 46.08/6.42 multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(sF2_fnc,b2))),sF2_fnc))=sF2_fnc),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f25170,f4820])).
% 46.08/6.42 fof(f25593,plain,(
% 46.08/6.42 multiply(b2,multiply(multiply(sF2_fnc,inverse(sF1_fnc)),sF2_fnc))=sF2_fnc),
% 46.08/6.42 inference(forward_demodulation,[status(thm)],[f6,f25446])).
% 46.08/6.42 fof(f30261,plain,(
% 46.08/6.42 ![X0]: (inverse(sF1_fnc)=inverse(multiply(multiply(sF2_fnc,inverse(multiply(X0,sF2_fnc))),X0)))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f25593,f23760])).
% 46.08/6.42 fof(f30630,plain,(
% 46.08/6.42 inverse(sF1_fnc)=inverse(multiply(sF2_fnc,inverse(multiply(inverse(multiply(b2,sF2_fnc)),sF2_fnc))))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f25170,f30261])).
% 46.08/6.42 fof(f32231,plain,(
% 46.08/6.42 ![X0]: (multiply(b2,inverse(multiply(multiply(b2,multiply(multiply(sF2_fnc,inverse(sF1_fnc)),inverse(X0))),multiply(X0,sF1_fnc))))=inverse(multiply(inverse(multiply(b2,sF2_fnc)),sF2_fnc)))),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f30630,f245])).
% 46.08/6.42 fof(f32403,plain,(
% 46.08/6.42 b2=inverse(multiply(inverse(multiply(b2,sF2_fnc)),sF2_fnc))),
% 46.08/6.42 inference(forward_demodulation,[status(thm)],[f737,f32231])).
% 46.08/6.42 fof(f32526,plain,(
% 46.08/6.42 multiply(b2,sF2_fnc)=multiply(multiply(inverse(multiply(b2,sF2_fnc)),sF2_fnc),b2)),
% 46.08/6.42 inference(paramodulation,[status(thm)],[f32403,f20034])).
% 46.08/6.42 fof(f32717,plain,(
% 46.08/6.42 sF2_fnc=inverse(multiply(b2,multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(b2,sF2_fnc))),inverse(multiply(b2,sF2_fnc))))))),
% 46.08/6.43 inference(paramodulation,[status(thm)],[f32526,f22364])).
% 46.08/6.43 fof(f32797,plain,(
% 46.08/6.43 sF2_fnc=inverse(multiply(b2,multiply(b2,multiply(sF2_fnc,inverse(multiply(b2,sF2_fnc))))))),
% 46.08/6.43 inference(forward_demodulation,[status(thm)],[f25170,f32717])).
% 46.08/6.43 fof(f32798,plain,(
% 46.08/6.43 sF2_fnc=inverse(multiply(b2,multiply(b2,sF2_fnc)))),
% 46.08/6.43 inference(forward_demodulation,[status(thm)],[f25170,f32797])).
% 46.08/6.43 fof(f32974,plain,(
% 46.08/6.43 multiply(b2,sF2_fnc)=multiply(multiply(b2,multiply(b2,sF2_fnc)),sF2_fnc)),
% 46.08/6.43 inference(paramodulation,[status(thm)],[f32798,f20034])).
% 46.08/6.43 fof(f34052,plain,(
% 46.08/6.43 multiply(b2,sF2_fnc)=inverse(multiply(sF2_fnc,multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(b2,sF2_fnc))),b2))))),
% 46.08/6.43 inference(paramodulation,[status(thm)],[f32974,f22364])).
% 46.08/6.43 fof(f34057,plain,(
% 46.08/6.43 ![X0,X1,X2]: (multiply(inverse(X0),inverse(multiply(X1,multiply(X2,inverse(multiply(multiply(X0,multiply(b2,sF2_fnc)),multiply(b2,multiply(X1,X2))))))))=multiply(b2,multiply(b2,sF2_fnc)))),
% 46.08/6.43 inference(paramodulation,[status(thm)],[f32974,f8807])).
% 46.08/6.43 fof(f34146,plain,(
% 46.08/6.43 multiply(b2,sF2_fnc)=inverse(multiply(sF2_fnc,multiply(b2,multiply(sF2_fnc,b2))))),
% 46.08/6.43 inference(forward_demodulation,[status(thm)],[f25170,f34052])).
% 46.08/6.43 fof(f34147,plain,(
% 46.08/6.43 multiply(b2,sF2_fnc)=inverse(multiply(sF2_fnc,multiply(b2,sF1_fnc)))),
% 46.08/6.43 inference(forward_demodulation,[status(thm)],[f6,f34146])).
% 46.08/6.43 fof(f34151,plain,(
% 46.08/6.43 b2=multiply(b2,multiply(b2,sF2_fnc))),
% 46.08/6.43 inference(forward_demodulation,[status(thm)],[f8807,f34057])).
% 46.08/6.43 fof(f34257,plain,(
% 46.08/6.43 ![X0]: (multiply(sF2_fnc,inverse(multiply(multiply(sF2_fnc,inverse(multiply(X0,b2))),X0)))=b2)),
% 46.08/6.43 inference(paramodulation,[status(thm)],[f34151,f8605])).
% 46.08/6.43 fof(f37598,plain,(
% 46.08/6.43 multiply(sF2_fnc,inverse(multiply(multiply(sF2_fnc,inverse(multiply(b2,sF2_fnc))),multiply(inverse(multiply(b2,sF2_fnc)),sF2_fnc))))=b2),
% 46.08/6.43 inference(paramodulation,[status(thm)],[f32526,f34257])).
% 46.08/6.43 fof(f37745,plain,(
% 46.08/6.43 multiply(sF2_fnc,inverse(multiply(sF2_fnc,multiply(inverse(multiply(b2,sF2_fnc)),sF2_fnc))))=b2),
% 46.08/6.43 inference(forward_demodulation,[status(thm)],[f25170,f37598])).
% 46.08/6.43 fof(f39035,plain,(
% 46.08/6.43 multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(b2,sF2_fnc))),sF2_fnc))=multiply(inverse(multiply(b2,sF2_fnc)),sF2_fnc)),
% 46.08/6.43 inference(paramodulation,[status(thm)],[f37745,f4820])).
% 46.08/6.43 fof(f39148,plain,(
% 46.08/6.43 multiply(b2,multiply(sF2_fnc,sF2_fnc))=multiply(inverse(multiply(b2,sF2_fnc)),sF2_fnc)),
% 46.08/6.43 inference(forward_demodulation,[status(thm)],[f25170,f39035])).
% 46.08/6.43 fof(f41193,plain,(
% 46.08/6.43 b2=inverse(multiply(b2,multiply(sF2_fnc,sF2_fnc)))),
% 46.08/6.43 inference(backward_demodulation,[status(thm)],[f39148,f32403])).
% 46.08/6.43 fof(f49117,plain,(
% 46.08/6.43 ![X0,X1]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(X0,inverse(multiply(b2,sF2_fnc))),X1))),X0))=inverse(X1))),
% 46.08/6.43 inference(paramodulation,[status(thm)],[f20034,f24190])).
% 46.08/6.43 fof(f49367,plain,(
% 46.08/6.43 ![X0,X1]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(X0,X1))),X0))=inverse(X1))),
% 46.08/6.43 inference(forward_demodulation,[status(thm)],[f25170,f49117])).
% 46.08/6.43 fof(f49444,plain,(
% 46.08/6.43 ![X0,X1]: (multiply(b2,multiply(X0,inverse(multiply(a2,multiply(X1,multiply(multiply(inverse(X1),inverse(sF0_fnc)),X0))))))=inverse(multiply(b2,multiply(multiply(sF2_fnc,inverse(sF1_fnc)),sF2_fnc))))),
% 45.10/6.49 inference(paramodulation,[status(thm)],[f34,f49367])).
% 45.10/6.49 fof(f49615,plain,(
% 45.10/6.49 ![X0]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(b2,sF2_fnc))),X0))=inverse(inverse(X0)))),
% 45.10/6.49 inference(paramodulation,[status(thm)],[f20034,f49367])).
% 45.10/6.49 fof(f49819,plain,(
% 45.10/6.49 multiply(b2,sF1_fnc)=inverse(multiply(b2,multiply(multiply(sF2_fnc,inverse(sF1_fnc)),sF2_fnc)))),
% 45.10/6.49 inference(forward_demodulation,[status(thm)],[f12,f49444])).
% 45.10/6.49 fof(f49820,plain,(
% 45.10/6.49 multiply(b2,sF1_fnc)=inverse(sF2_fnc)),
% 45.10/6.49 inference(forward_demodulation,[status(thm)],[f25593,f49819])).
% 45.10/6.49 fof(f49883,plain,(
% 45.10/6.49 ![X0]: (multiply(b2,multiply(sF2_fnc,X0))=inverse(inverse(X0)))),
% 45.10/6.49 inference(forward_demodulation,[status(thm)],[f25170,f49615])).
% 45.10/6.49 fof(f49971,plain,(
% 45.10/6.49 multiply(b2,sF2_fnc)=inverse(multiply(sF2_fnc,inverse(sF2_fnc)))),
% 45.10/6.49 inference(backward_demodulation,[status(thm)],[f49820,f34147])).
% 45.10/6.49 fof(f50089,plain,(
% 45.10/6.49 multiply(b2,sF2_fnc)=inverse(multiply(b2,sF2_fnc))),
% 45.10/6.49 inference(forward_demodulation,[status(thm)],[f20034,f49971])).
% 45.10/6.49 fof(f50137,plain,(
% 45.10/6.49 b2=inverse(inverse(inverse(sF2_fnc)))),
% 45.10/6.49 inference(backward_demodulation,[status(thm)],[f49883,f41193])).
% 45.10/6.49 fof(f50145,plain,(
% 45.10/6.49 ![X0,X1]: (inverse(inverse(X0))=multiply(X1,multiply(inverse(X1),X0)))),
% 45.10/6.49 inference(backward_demodulation,[status(thm)],[f49883,f24174])).
% 45.10/6.49 fof(f50627,plain,(
% 45.10/6.49 ![X0]: (multiply(X0,multiply(b2,sF2_fnc))=X0)),
% 45.10/6.49 inference(backward_demodulation,[status(thm)],[f50089,f25170])).
% 45.10/6.49 fof(f50937,plain,(
% 45.10/6.49 ![X0,X1]: (multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(multiply(b2,sF2_fnc),X1))))),X0))=X1)),
% 45.10/6.49 inference(paramodulation,[status(thm)],[f50627,f24190])).
% 45.10/6.49 fof(f51131,plain,(
% 45.10/6.49 ![X0]: (inverse(inverse(multiply(multiply(b2,sF2_fnc),X0)))=X0)),
% 45.10/6.49 inference(forward_demodulation,[status(thm)],[f49367,f50937])).
% 45.10/6.49 fof(f51390,plain,(
% 45.10/6.49 ![X0]: (inverse(inverse(inverse(inverse(X0))))=multiply(X0,multiply(b2,sF2_fnc)))),
% 45.10/6.49 inference(paramodulation,[status(thm)],[f20034,f50145])).
% 45.10/6.49 fof(f51695,plain,(
% 45.10/6.49 ![X0]: (inverse(inverse(inverse(inverse(X0))))=X0)),
% 45.10/6.49 inference(forward_demodulation,[status(thm)],[f50627,f51390])).
% 45.10/6.49 fof(f52401,plain,(
% 45.10/6.49 ![X0]: (inverse(inverse(inverse(inverse(X0))))=multiply(inverse(multiply(b2,sF2_fnc)),X0))),
% 45.10/6.49 inference(paramodulation,[status(thm)],[f50145,f51131])).
% 45.10/6.49 fof(f52539,plain,(
% 45.10/6.49 ![X0]: (X0=multiply(inverse(multiply(b2,sF2_fnc)),X0))),
% 45.10/6.49 inference(forward_demodulation,[status(thm)],[f51695,f52401])).
% 45.10/6.49 fof(f52540,plain,(
% 45.10/6.49 ![X0]: (X0=multiply(multiply(b2,sF2_fnc),X0))),
% 45.10/6.49 inference(forward_demodulation,[status(thm)],[f50089,f52539])).
% 45.10/6.49 fof(f52594,plain,(
% 45.10/6.49 ![X0]: (inverse(inverse(X0))=X0)),
% 45.10/6.49 inference(backward_demodulation,[status(thm)],[f52540,f51131])).
% 45.10/6.49 fof(f53326,plain,(
% 45.10/6.49 b2=inverse(sF2_fnc)),
% 45.10/6.49 inference(backward_demodulation,[status(thm)],[f52594,f50137])).
% 45.10/6.49 fof(f55220,plain,(
% 45.10/6.49 multiply(b2,sF2_fnc)=multiply(sF2_fnc,b2)),
% 45.10/6.49 inference(paramodulation,[status(thm)],[f53326,f20034])).
% 45.10/6.49 fof(f55286,plain,(
% 45.10/6.49 multiply(b2,sF2_fnc)=sF1_fnc),
% 45.10/6.49 inference(forward_demodulation,[status(thm)],[f6,f55220])).
% 45.10/6.49 fof(f55510,plain,(
% 45.10/6.49 ![X0]: (X0=multiply(sF1_fnc,X0))),
% 45.10/6.49 inference(backward_demodulation,[status(thm)],[f55286,f52540])).
% 45.10/6.49 fof(f55715,plain,(
% 45.10/6.49 sF0_fnc=a2),
% 45.10/6.49 inference(backward_demodulation,[status(thm)],[f55510,f7])).
% 45.10/6.49 fof(f55986,plain,(
% 45.10/6.49 $false),
% 45.10/6.49 inference(forward_subsumption_resolution,[status(thm)],[f55715,f8])).
% 45.10/6.49 % SZS output end CNFRefutation for theBenchmark.p
% 45.10/6.54 % Elapsed time: 6.157008 seconds
% 45.10/6.54 % CPU time: 48.522297 seconds
% 45.10/6.54 % Total memory used: 616.663 MB
% 45.10/6.54 % Net memory used: 608.364 MB
%------------------------------------------------------------------------------