%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP436-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 : n005.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 78.63s 10.36s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP436-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 : n005.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:13:03 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.15/0.37 % Drodi V4.1.1
% 78.63/10.36 % Refutation found
% 78.63/10.36 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 78.63/10.36 % SZS output start CNFRefutation for theBenchmark
% 78.63/10.36 fof(f1,axiom,(
% 78.63/10.36 (![A,B,C,D]: (multiply(A,inverse(multiply(B,multiply(C,multiply(multiply(inverse(C),inverse(multiply(D,B))),A))))) = D ))),
% 78.63/10.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 78.63/10.36 fof(f2,negated_conjecture,(
% 78.63/10.36 multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
% 78.63/10.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 78.63/10.36 fof(f3,plain,(
% 78.63/10.36 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,X1))),X0)))))=X3)),
% 78.63/10.36 inference(cnf_transformation,[status(thm)],[f1])).
% 78.63/10.36 fof(f4,plain,(
% 78.63/10.36 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)),
% 78.63/10.36 inference(cnf_transformation,[status(thm)],[f2])).
% 78.63/10.36 fof(f5,definition,(
% 78.63/10.36 sF1_fnc=inverse(a1)),
% 78.63/10.36 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 78.63/10.36 fof(f6,definition,(
% 78.63/10.36 sF0_fnc=multiply(sF1_fnc,a1)),
% 78.63/10.36 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 78.63/10.36 fof(f7,definition,(
% 78.63/10.36 sF3_fnc=inverse(b1)),
% 78.63/10.36 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 78.63/10.36 fof(f8,definition,(
% 78.63/10.36 sF2_fnc=multiply(sF3_fnc,b1)),
% 78.63/10.36 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 78.63/10.36 fof(f9,plain,(
% 78.63/10.36 ~sF0_fnc=sF2_fnc),
% 78.63/10.36 inference(definition_folding,[],[f4,f8,f7,f6,f5])).
% 78.63/10.36 fof(f11,plain,(
% 78.63/10.36 ![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)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f3,f3])).
% 78.63/10.36 fof(f12,plain,(
% 78.63/10.36 ![X0,X1,X2]: (multiply(X0,inverse(multiply(X1,multiply(b1,multiply(multiply(sF3_fnc,inverse(multiply(X2,X1))),X0)))))=X2)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f7,f3])).
% 78.63/10.36 fof(f13,plain,(
% 78.63/10.36 ![X0,X1,X2]: (multiply(X0,inverse(multiply(X1,multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(X2,X1))),X0)))))=X2)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f5,f3])).
% 78.63/10.36 fof(f15,plain,(
% 78.63/10.36 ![X0,X1]: (multiply(X0,inverse(multiply(a1,multiply(X1,multiply(multiply(inverse(X1),inverse(sF0_fnc)),X0)))))=sF1_fnc)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f6,f3])).
% 78.63/10.36 fof(f21,plain,(
% 78.63/10.36 ![X0]: (multiply(X0,inverse(multiply(b1,multiply(b1,multiply(multiply(sF3_fnc,inverse(sF2_fnc)),X0)))))=sF3_fnc)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f8,f12])).
% 78.63/10.36 fof(f22,plain,(
% 78.63/10.36 ![X0]: (multiply(X0,inverse(multiply(a1,multiply(b1,multiply(multiply(sF3_fnc,inverse(sF0_fnc)),X0)))))=sF1_fnc)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f6,f12])).
% 78.63/10.36 fof(f25,plain,(
% 78.63/10.36 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(b1,multiply(multiply(sF3_fnc,inverse(multiply(X1,X2))),inverse(X3))),multiply(X3,multiply(X1,X0)))))=X2)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f12,f3])).
% 78.63/10.36 fof(f35,plain,(
% 78.63/10.36 ![X0]: (multiply(X0,inverse(multiply(a1,multiply(a1,multiply(multiply(sF1_fnc,inverse(sF0_fnc)),X0)))))=sF1_fnc)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f6,f13])).
% 78.63/10.36 fof(f39,plain,(
% 78.63/10.36 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(X1,X2))),inverse(X3))),multiply(X3,multiply(X1,X0)))))=X2)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f13,f3])).
% 78.63/10.36 fof(f42,plain,(
% 78.63/10.36 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(X1,X2))),sF3_fnc)),multiply(b1,multiply(X1,X0)))))=X2)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f13,f12])).
% 78.63/10.36 fof(f43,plain,(
% 78.63/10.36 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(inverse(multiply(X1,multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(X2,X1))),X3)))),multiply(b1,multiply(multiply(sF3_fnc,inverse(X2)),X0)))))=X3)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f13,f12])).
% 78.63/10.36 fof(f44,plain,(
% 78.63/10.36 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(inverse(multiply(X1,multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(X2,X1))),X3)))),multiply(X4,multiply(multiply(inverse(X4),inverse(X2)),X0)))))=X3)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f13,f3])).
% 78.63/10.36 fof(f68,plain,(
% 78.63/10.36 ![X0,X1,X2]: (multiply(inverse(multiply(a1,multiply(X0,multiply(multiply(inverse(X0),inverse(sF0_fnc)),multiply(sF1_fnc,inverse(multiply(X1,X2))))))),inverse(multiply(X2,multiply(a1,sF1_fnc))))=X1)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f15,f13])).
% 78.63/10.36 fof(f143,plain,(
% 78.63/10.36 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(a1,multiply(multiply(sF1_fnc,inverse(sF0_fnc)),inverse(X1))),multiply(X1,multiply(sF1_fnc,X0)))))=a1)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f35,f3])).
% 78.63/10.36 fof(f167,plain,(
% 78.63/10.36 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X3))),multiply(X3,multiply(multiply(X4,multiply(multiply(inverse(X4),inverse(multiply(X5,X2))),inverse(X6))),X0)))))=multiply(X6,multiply(X5,inverse(X1))))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f11,f11])).
% 78.63/10.36 fof(f174,plain,(
% 78.63/10.36 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X3))),multiply(X3,multiply(X4,X0)))))=multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(X2,X4))),inverse(X1))))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f13,f11])).
% 78.63/10.36 fof(f181,plain,(
% 78.63/10.36 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(X0,inverse(multiply(multiply(X1,multiply(multiply(inverse(X1),inverse(X2)),inverse(X3))),multiply(X3,multiply(X4,X0)))))=inverse(multiply(multiply(X5,multiply(multiply(inverse(X5),inverse(multiply(X6,X2))),inverse(X7))),multiply(X7,multiply(X6,X4)))))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f11,f11])).
% 78.63/10.36 fof(f989,plain,(
% 78.63/10.36 ![X0,X1]: (multiply(b1,inverse(multiply(multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(sF3_fnc,X0))),inverse(X1))),multiply(X1,sF2_fnc))))=X0)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f8,f39])).
% 78.63/10.36 fof(f1100,plain,(
% 78.63/10.36 ![X0]: (multiply(a1,inverse(multiply(multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(sF1_fnc,X0))),sF3_fnc)),multiply(b1,sF0_fnc))))=X0)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f6,f42])).
% 78.63/10.36 fof(f18402,plain,(
% 78.63/10.36 multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(multiply(sF1_fnc,inverse(sF0_fnc)),sF1_fnc))),inverse(a1)))=a1),
% 78.63/10.36 inference(backward_demodulation,[status(thm)],[f174,f143])).
% 78.63/10.36 fof(f18404,plain,(
% 78.63/10.36 ![X0,X1]: (multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(multiply(sF1_fnc,inverse(multiply(X0,X1))),X0))),inverse(a1)))=X1)),
% 78.63/10.36 inference(backward_demodulation,[status(thm)],[f174,f39])).
% 78.63/10.36 fof(f18405,plain,(
% 78.63/10.36 ![X0,X1]: (multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(multiply(sF3_fnc,inverse(multiply(X0,X1))),X0))),inverse(b1)))=X1)),
% 78.63/10.36 inference(backward_demodulation,[status(thm)],[f174,f25])).
% 78.63/10.36 fof(f18408,plain,(
% 78.63/10.36 ![X0,X1,X2]: (multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(multiply(inverse(X0),inverse(multiply(X1,X2))),X1))),inverse(X0)))=X2)),
% 78.63/10.36 inference(backward_demodulation,[status(thm)],[f174,f11])).
% 78.63/10.36 fof(f18409,plain,(
% 78.63/10.36 ![X0,X1,X2]: (X0=multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(X1,multiply(sF1_fnc,inverse(multiply(X0,multiply(X2,multiply(X1,inverse(a1))))))))),inverse(X2))))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f13,f174])).
% 78.63/10.36 fof(f18761,plain,(
% 78.63/10.36 multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(multiply(sF1_fnc,inverse(sF0_fnc)),sF1_fnc))),sF1_fnc))=a1),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f5,f18402])).
% 78.63/10.36 fof(f18763,plain,(
% 78.63/10.36 ![X0,X1]: (multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(multiply(sF1_fnc,inverse(multiply(X0,X1))),X0))),sF1_fnc))=X1)),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f5,f18404])).
% 78.63/10.36 fof(f18764,plain,(
% 78.63/10.36 ![X0,X1]: (multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(multiply(sF3_fnc,inverse(multiply(X0,X1))),X0))),sF3_fnc))=X1)),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f7,f18405])).
% 78.63/10.36 fof(f18765,plain,(
% 78.63/10.36 ![X0,X1,X2]: (X0=multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(X1,multiply(sF1_fnc,inverse(multiply(X0,multiply(X2,multiply(X1,sF1_fnc)))))))),inverse(X2))))),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f5,f18409])).
% 78.63/10.36 fof(f19061,plain,(
% 78.63/10.36 ![X0,X1,X2]: (multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(X1,multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(X2,X1))),X0))))))),sF1_fnc))=multiply(b1,multiply(multiply(sF3_fnc,inverse(X2)),sF1_fnc)))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f43,f18763])).
% 78.63/10.36 fof(f19063,plain,(
% 78.63/10.36 ![X0,X1,X2,X3]: (multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(X1,multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(X2,X1))),X0))))))),sF1_fnc))=multiply(X3,multiply(multiply(inverse(X3),inverse(X2)),sF1_fnc)))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f44,f18763])).
% 78.63/10.36 fof(f19250,plain,(
% 78.63/10.36 ![X0]: (multiply(a1,multiply(multiply(sF1_fnc,inverse(X0)),sF1_fnc))=multiply(b1,multiply(multiply(sF3_fnc,inverse(X0)),sF1_fnc)))),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f13,f19061])).
% 78.63/10.36 fof(f19251,plain,(
% 78.63/10.36 ![X0,X1]: (multiply(a1,multiply(multiply(sF1_fnc,inverse(X0)),sF1_fnc))=multiply(X1,multiply(multiply(inverse(X1),inverse(X0)),sF1_fnc)))),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f13,f19063])).
% 78.63/10.36 fof(f19369,plain,(
% 78.63/10.36 multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(multiply(sF3_fnc,inverse(sF0_fnc)),sF1_fnc))),sF3_fnc))=a1),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f6,f18764])).
% 78.63/10.36 fof(f19824,plain,(
% 78.63/10.36 ![X0,X1,X2,X3,X4]: (multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(X1,multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(X2,X1))),X0))))))),inverse(X3)))=multiply(X4,multiply(multiply(inverse(X4),inverse(X2)),inverse(X3))))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f44,f18408])).
% 78.63/10.36 fof(f20026,plain,(
% 78.63/10.36 ![X0,X1,X2]: (multiply(a1,multiply(multiply(sF1_fnc,inverse(X0)),inverse(X1)))=multiply(X2,multiply(multiply(inverse(X2),inverse(X0)),inverse(X1))))),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f13,f19824])).
% 78.63/10.36 fof(f24412,plain,(
% 78.63/10.36 ![X0,X1]: (multiply(b1,inverse(multiply(X0,multiply(X1,sF2_fnc))))=multiply(sF1_fnc,inverse(multiply(X0,multiply(X1,multiply(sF3_fnc,sF1_fnc))))))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f18765,f989])).
% 78.63/10.36 fof(f24416,plain,(
% 78.63/10.36 ![X0,X1,X2]: (multiply(inverse(X0),inverse(multiply(multiply(sF1_fnc,inverse(multiply(X1,multiply(X0,multiply(X2,sF1_fnc))))),X1)))=X2)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f18765,f13])).
% 78.63/10.36 fof(f24528,plain,(
% 78.63/10.36 ![X0,X1]: (multiply(sF3_fnc,inverse(multiply(multiply(sF1_fnc,inverse(multiply(X0,multiply(b1,multiply(X1,sF1_fnc))))),X0)))=X1)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f7,f24416])).
% 78.63/10.36 fof(f24579,plain,(
% 78.63/10.36 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(X1,multiply(X2,multiply(X3,X0)))))=multiply(sF1_fnc,inverse(multiply(X1,multiply(X2,multiply(X3,sF1_fnc))))))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f24416,f3])).
% 78.63/10.36 fof(f26488,plain,(
% 78.63/10.36 ![X0]: (multiply(sF3_fnc,inverse(multiply(multiply(b1,inverse(multiply(X0,multiply(b1,sF2_fnc)))),X0)))=sF3_fnc)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f24412,f24528])).
% 78.63/10.36 fof(f26691,plain,(
% 78.63/10.36 ![X0]: (multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(sF3_fnc,multiply(b1,inverse(multiply(X0,multiply(b1,sF2_fnc))))))),sF3_fnc))=X0)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f26488,f18764])).
% 78.63/10.36 fof(f27635,plain,(
% 78.63/10.36 ![X0,X1,X2]: (multiply(sF3_fnc,inverse(multiply(multiply(X0,inverse(multiply(X1,multiply(b1,multiply(X2,X0))))),X1)))=X2)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f24579,f24528])).
% 78.63/10.36 fof(f27637,plain,(
% 78.63/10.36 ![X0,X1,X2,X3]: (X0=multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(X1,multiply(X2,inverse(multiply(X0,multiply(X3,multiply(X1,X2)))))))),inverse(X3))))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f24579,f18765])).
% 78.63/10.36 fof(f42448,plain,(
% 78.63/10.36 ![X0,X1,X2,X3,X4]: (multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(X0,multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(X2,X0))),inverse(X3)))))),inverse(X4)))=multiply(X3,multiply(X2,inverse(X4))))),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f174,f167])).
% 78.63/10.36 fof(f42449,plain,(
% 78.63/10.36 ![X0,X1,X2,X3]: (multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(X0,multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(X1,X0))),inverse(X2)))))),inverse(X3)))=multiply(X2,multiply(X1,inverse(X3))))),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f20026,f42448])).
% 78.63/10.36 fof(f42931,plain,(
% 78.63/10.36 ![X0,X1,X2,X3,X4,X5]: (multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(multiply(inverse(X0),inverse(X1)),X2))),inverse(X0)))=inverse(multiply(multiply(X3,multiply(multiply(inverse(X3),inverse(multiply(X4,X1))),inverse(X5))),multiply(X5,multiply(X4,X2)))))),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f174,f181])).
% 78.63/10.36 fof(f42932,plain,(
% 78.63/10.36 ![X0,X1,X2,X3,X4]: (multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(multiply(inverse(X0),inverse(X1)),X2))),inverse(X0)))=inverse(multiply(multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(X3,X1))),inverse(X4))),multiply(X4,multiply(X3,X2)))))),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f20026,f42931])).
% 78.63/10.36 fof(f43640,plain,(
% 78.63/10.36 ![X0,X1,X2,X3]: (multiply(X0,multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(multiply(inverse(X1),inverse(X2)),X0))),inverse(X1))))=multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(multiply(sF1_fnc,inverse(multiply(X3,X2))),X3))),inverse(a1))))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f42932,f174])).
% 78.63/10.36 fof(f43957,plain,(
% 78.63/10.36 ![X0,X1,X2,X3]: (multiply(X0,multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(multiply(inverse(X1),inverse(X2)),X0))),inverse(X1))))=multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(multiply(sF1_fnc,inverse(multiply(X3,X2))),X3))),sF1_fnc)))),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f5,f43640])).
% 78.63/10.36 fof(f43958,plain,(
% 78.63/10.36 ![X0,X1,X2]: (multiply(X0,multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(multiply(inverse(X1),inverse(X2)),X0))),inverse(X1))))=X2)),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f18763,f43957])).
% 78.63/10.36 fof(f43982,plain,(
% 78.63/10.36 ![X0,X1,X2,X3]: (multiply(multiply(X0,inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(X3)),X0))))),X1)=X3)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f27637,f43958])).
% 78.63/10.36 fof(f44512,plain,(
% 78.63/10.36 ![X0,X1,X2]: (multiply(multiply(X0,inverse(multiply(X1,multiply(a1,multiply(multiply(sF1_fnc,inverse(X2)),X0))))),X1)=X2)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f5,f43982])).
% 78.63/10.36 fof(f45395,plain,(
% 78.63/10.36 ![X0]: (multiply(multiply(sF3_fnc,inverse(multiply(X0,a1))),X0)=multiply(multiply(sF3_fnc,inverse(sF0_fnc)),sF1_fnc))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f19369,f44512])).
% 78.63/10.36 fof(f45397,plain,(
% 78.63/10.36 ![X0,X1,X2]: (multiply(multiply(sF3_fnc,inverse(multiply(X0,X1))),X0)=multiply(multiply(sF3_fnc,inverse(multiply(X2,X1))),X2))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f18764,f44512])).
% 78.63/10.36 fof(f45398,plain,(
% 78.63/10.36 ![X0,X1,X2]: (multiply(multiply(sF1_fnc,inverse(multiply(X0,X1))),X0)=multiply(multiply(sF1_fnc,inverse(multiply(X2,X1))),X2))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f18763,f44512])).
% 78.63/10.36 fof(f45400,plain,(
% 78.63/10.36 ![X0]: (multiply(multiply(sF1_fnc,inverse(multiply(X0,a1))),X0)=multiply(multiply(sF1_fnc,inverse(sF0_fnc)),sF1_fnc))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f18761,f44512])).
% 78.63/10.36 fof(f47893,plain,(
% 78.63/10.36 ![X0]: (multiply(X0,inverse(multiply(a1,multiply(b1,multiply(multiply(sF3_fnc,inverse(sF0_fnc)),sF1_fnc)))))=X0)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f45395,f12])).
% 78.63/10.36 fof(f48120,plain,(
% 78.63/10.36 ![X0]: (multiply(X0,inverse(multiply(a1,multiply(a1,multiply(multiply(sF1_fnc,inverse(sF0_fnc)),sF1_fnc)))))=X0)),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f19250,f47893])).
% 78.63/10.36 fof(f49900,plain,(
% 78.63/10.36 ![X0,X1,X2]: (multiply(X0,inverse(multiply(X1,multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(X2,X1))),X2)))))=X0)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f45398,f13])).
% 78.63/10.36 fof(f50762,plain,(
% 78.63/10.36 ![X0,X1]: (multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(a1,multiply(a1,multiply(multiply(sF1_fnc,inverse(sF0_fnc)),sF1_fnc))))),inverse(X0)))=multiply(X1,multiply(inverse(X1),inverse(X0))))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f45400,f42449])).
% 78.63/10.36 fof(f51001,plain,(
% 78.63/10.36 ![X0,X1]: (multiply(a1,multiply(sF1_fnc,inverse(X0)))=multiply(X1,multiply(inverse(X1),inverse(X0))))),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f35,f50762])).
% 78.63/10.36 fof(f51092,plain,(
% 78.63/10.36 ![X0]: (multiply(a1,multiply(sF1_fnc,inverse(X0)))=multiply(b1,multiply(sF3_fnc,inverse(X0))))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f7,f51001])).
% 78.63/10.36 fof(f56912,plain,(
% 78.63/10.36 ![X0]: (multiply(a1,multiply(sF1_fnc,inverse(multiply(a1,multiply(a1,multiply(multiply(sF1_fnc,inverse(sF0_fnc)),sF1_fnc))))))=multiply(X0,inverse(X0)))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f48120,f51001])).
% 78.63/10.36 fof(f57054,plain,(
% 78.63/10.36 multiply(a1,multiply(sF1_fnc,inverse(multiply(a1,multiply(a1,multiply(multiply(sF1_fnc,inverse(sF0_fnc)),sF1_fnc))))))=multiply(b1,sF3_fnc)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f48120,f51092])).
% 78.63/10.36 fof(f57115,plain,(
% 78.63/10.36 ![X0,X1]: (multiply(multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(a1,multiply(a1,multiply(multiply(sF1_fnc,inverse(sF0_fnc)),sF1_fnc))))))),X0)=multiply(multiply(sF1_fnc,inverse(X1)),X1))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f48120,f45398])).
% 78.63/10.36 fof(f57117,plain,(
% 78.63/10.36 ![X0,X1]: (multiply(multiply(sF3_fnc,inverse(multiply(X0,inverse(multiply(a1,multiply(a1,multiply(multiply(sF1_fnc,inverse(sF0_fnc)),sF1_fnc))))))),X0)=multiply(multiply(sF3_fnc,inverse(X1)),X1))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f48120,f45397])).
% 78.63/10.36 fof(f57238,plain,(
% 78.63/10.36 ![X0]: (multiply(a1,sF1_fnc)=multiply(X0,inverse(X0)))),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f48120,f56912])).
% 78.63/10.36 fof(f57307,plain,(
% 78.63/10.36 multiply(a1,sF1_fnc)=multiply(b1,sF3_fnc)),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f48120,f57054])).
% 78.63/10.36 fof(f57332,plain,(
% 78.63/10.36 ![X0,X1]: (multiply(multiply(sF1_fnc,inverse(X0)),X0)=multiply(multiply(sF1_fnc,inverse(X1)),X1))),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f48120,f57115])).
% 78.63/10.36 fof(f57334,plain,(
% 78.63/10.36 ![X0,X1]: (multiply(multiply(sF3_fnc,inverse(X0)),X0)=multiply(multiply(sF3_fnc,inverse(X1)),X1))),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f48120,f57117])).
% 78.63/10.36 fof(f57357,plain,(
% 78.63/10.36 ![X0]: (multiply(a1,multiply(sF1_fnc,inverse(inverse(X0))))=multiply(X0,multiply(a1,sF1_fnc)))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f57238,f51001])).
% 78.63/10.36 fof(f57784,plain,(
% 78.63/10.36 ![X0]: (multiply(multiply(a1,sF1_fnc),sF1_fnc)=multiply(multiply(sF1_fnc,inverse(X0)),X0))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f57238,f57332])).
% 78.63/10.36 fof(f58452,plain,(
% 78.63/10.36 ![X0]: (multiply(multiply(a1,sF1_fnc),sF3_fnc)=multiply(multiply(sF3_fnc,inverse(X0)),X0))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f57238,f57334])).
% 78.63/10.36 fof(f68585,plain,(
% 78.63/10.36 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(b1,inverse(multiply(X1,multiply(b1,sF2_fnc)))),X1)))=X0)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f26691,f49900])).
% 78.63/10.36 fof(f69541,plain,(
% 78.63/10.36 ![X0]: (multiply(a1,sF1_fnc)=multiply(multiply(b1,inverse(multiply(X0,multiply(b1,sF2_fnc)))),X0))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f57238,f68585])).
% 78.63/10.36 fof(f70734,plain,(
% 78.63/10.36 ![X0]: (multiply(X0,inverse(multiply(a1,sF1_fnc)))=X0)),
% 78.63/10.36 inference(backward_demodulation,[status(thm)],[f69541,f68585])).
% 78.63/10.36 fof(f71027,plain,(
% 78.63/10.36 multiply(multiply(a1,sF1_fnc),sF1_fnc)=multiply(sF1_fnc,inverse(inverse(multiply(a1,sF1_fnc))))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f57784,f70734])).
% 78.63/10.36 fof(f71059,plain,(
% 78.63/10.36 ![X0]: (multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(inverse(X0),a1))),inverse(X0)))=sF1_fnc)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f70734,f18408])).
% 78.63/10.36 fof(f71230,plain,(
% 78.63/10.36 multiply(multiply(a1,sF1_fnc),sF3_fnc)=multiply(sF3_fnc,multiply(a1,sF1_fnc))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f70734,f58452])).
% 78.63/10.36 fof(f71274,plain,(
% 78.63/10.36 multiply(multiply(a1,sF1_fnc),sF1_fnc)=multiply(sF1_fnc,multiply(a1,sF1_fnc))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f70734,f57784])).
% 78.63/10.36 fof(f71413,plain,(
% 78.63/10.36 multiply(a1,multiply(multiply(sF1_fnc,inverse(sF0_fnc)),sF1_fnc))=sF1_fnc),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f45400,f71059])).
% 78.63/10.36 fof(f80666,plain,(
% 78.63/10.36 ![X0]: (multiply(sF3_fnc,multiply(a1,sF1_fnc))=multiply(multiply(sF3_fnc,inverse(X0)),X0))),
% 78.63/10.36 inference(backward_demodulation,[status(thm)],[f71230,f58452])).
% 78.63/10.36 fof(f91935,plain,(
% 78.63/10.36 multiply(sF1_fnc,multiply(a1,sF1_fnc))=multiply(sF1_fnc,inverse(inverse(multiply(a1,sF1_fnc))))),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f71274,f71027])).
% 78.63/10.36 fof(f91944,plain,(
% 78.63/10.36 multiply(a1,inverse(multiply(multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(a1,sF1_fnc)))),sF3_fnc)),multiply(b1,sF0_fnc))))=inverse(inverse(multiply(a1,sF1_fnc)))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f91935,f1100])).
% 78.63/10.36 fof(f92083,plain,(
% 78.63/10.36 multiply(a1,sF1_fnc)=inverse(inverse(multiply(a1,sF1_fnc)))),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f1100,f91944])).
% 78.63/10.36 fof(f92137,plain,(
% 78.63/10.36 multiply(a1,multiply(sF1_fnc,inverse(multiply(a1,sF1_fnc))))=multiply(inverse(multiply(a1,sF1_fnc)),multiply(a1,sF1_fnc))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f92083,f57357])).
% 78.63/10.36 fof(f92292,plain,(
% 78.63/10.36 multiply(a1,sF1_fnc)=multiply(inverse(multiply(a1,sF1_fnc)),multiply(a1,sF1_fnc))),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f70734,f92137])).
% 78.63/10.36 fof(f97993,plain,(
% 78.63/10.36 ![X0]: (multiply(X0,inverse(multiply(multiply(a1,sF1_fnc),multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(a1,sF1_fnc))),inverse(multiply(a1,sF1_fnc)))))))=X0)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f92292,f49900])).
% 78.63/10.36 fof(f98176,plain,(
% 78.63/10.36 ![X0]: (multiply(X0,inverse(multiply(multiply(a1,sF1_fnc),multiply(a1,multiply(sF1_fnc,inverse(multiply(a1,sF1_fnc)))))))=X0)),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f70734,f97993])).
% 78.63/10.36 fof(f98177,plain,(
% 78.63/10.36 ![X0]: (multiply(X0,inverse(multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc))))=X0)),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f70734,f98176])).
% 78.63/10.36 fof(f98643,plain,(
% 78.63/10.36 ![X0]: (multiply(inverse(multiply(a1,multiply(X0,multiply(multiply(inverse(X0),inverse(sF0_fnc)),sF1_fnc)))),inverse(multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc))))=multiply(a1,sF1_fnc))),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f98177,f68])).
% 78.63/10.36 fof(f98945,plain,(
% 78.63/10.36 ![X0]: (inverse(multiply(a1,multiply(X0,multiply(multiply(inverse(X0),inverse(sF0_fnc)),sF1_fnc))))=multiply(a1,sF1_fnc))),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f98177,f98643])).
% 78.63/10.36 fof(f98946,plain,(
% 78.63/10.36 inverse(multiply(a1,multiply(a1,multiply(multiply(sF1_fnc,inverse(sF0_fnc)),sF1_fnc))))=multiply(a1,sF1_fnc)),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f19251,f98945])).
% 78.63/10.36 fof(f98947,plain,(
% 78.63/10.36 inverse(multiply(a1,sF1_fnc))=multiply(a1,sF1_fnc)),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f71413,f98946])).
% 78.63/10.36 fof(f98998,plain,(
% 78.63/10.36 ![X0]: (multiply(X0,multiply(a1,sF1_fnc))=X0)),
% 78.63/10.36 inference(backward_demodulation,[status(thm)],[f98947,f70734])).
% 78.63/10.36 fof(f99357,plain,(
% 78.63/10.36 ![X0]: (sF3_fnc=multiply(multiply(sF3_fnc,inverse(X0)),X0))),
% 78.63/10.36 inference(backward_demodulation,[status(thm)],[f98998,f80666])).
% 78.63/10.36 fof(f99891,plain,(
% 78.63/10.36 multiply(sF0_fnc,inverse(multiply(a1,multiply(b1,sF3_fnc))))=sF1_fnc),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f99357,f22])).
% 78.63/10.36 fof(f99892,plain,(
% 78.63/10.36 multiply(sF2_fnc,inverse(multiply(b1,multiply(b1,sF3_fnc))))=sF3_fnc),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f99357,f21])).
% 78.63/10.36 fof(f99904,plain,(
% 78.63/10.36 ![X0,X1]: (multiply(multiply(X0,X1),inverse(multiply(X1,multiply(b1,sF3_fnc))))=X0)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f99357,f12])).
% 78.63/10.36 fof(f100225,plain,(
% 78.63/10.36 multiply(sF0_fnc,inverse(multiply(a1,multiply(a1,sF1_fnc))))=sF1_fnc),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f57307,f99891])).
% 78.63/10.36 fof(f100226,plain,(
% 78.63/10.36 multiply(sF0_fnc,inverse(a1))=sF1_fnc),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f98998,f100225])).
% 78.63/10.36 fof(f100227,plain,(
% 78.63/10.36 multiply(sF0_fnc,sF1_fnc)=sF1_fnc),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f5,f100226])).
% 78.63/10.36 fof(f100228,plain,(
% 78.63/10.36 multiply(sF2_fnc,inverse(multiply(b1,multiply(a1,sF1_fnc))))=sF3_fnc),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f57307,f99892])).
% 78.63/10.36 fof(f100229,plain,(
% 78.63/10.36 multiply(sF2_fnc,inverse(b1))=sF3_fnc),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f98998,f100228])).
% 78.63/10.36 fof(f100230,plain,(
% 78.63/10.36 multiply(sF2_fnc,sF3_fnc)=sF3_fnc),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f7,f100229])).
% 78.63/10.36 fof(f100265,plain,(
% 78.63/10.36 ![X0,X1]: (multiply(multiply(X0,X1),inverse(multiply(X1,multiply(a1,sF1_fnc))))=X0)),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f57307,f99904])).
% 78.63/10.36 fof(f100266,plain,(
% 78.63/10.36 ![X0,X1]: (multiply(multiply(X0,X1),inverse(X1))=X0)),
% 78.63/10.36 inference(forward_demodulation,[status(thm)],[f98998,f100265])).
% 78.63/10.36 fof(f100683,plain,(
% 78.63/10.36 ![X0]: (multiply(sF3_fnc,inverse(multiply(multiply(sF3_fnc,inverse(multiply(X0,multiply(b1,sF3_fnc)))),X0)))=sF2_fnc)),
% 78.63/10.36 inference(paramodulation,[status(thm)],[f100230,f27635])).
% 78.63/10.36 fof(f100759,plain,(
% 78.63/10.36 ![X0]: (multiply(sF3_fnc,inverse(multiply(multiply(sF3_fnc,inverse(multiply(X0,multiply(a1,sF1_fnc)))),X0)))=sF2_fnc)),
% 76.98/10.49 inference(forward_demodulation,[status(thm)],[f57307,f100683])).
% 76.98/10.49 fof(f100760,plain,(
% 76.98/10.49 ![X0]: (multiply(sF3_fnc,inverse(multiply(multiply(sF3_fnc,inverse(X0)),X0)))=sF2_fnc)),
% 76.98/10.49 inference(forward_demodulation,[status(thm)],[f98998,f100759])).
% 76.98/10.49 fof(f100761,plain,(
% 76.98/10.49 multiply(sF3_fnc,inverse(sF3_fnc))=sF2_fnc),
% 76.98/10.49 inference(forward_demodulation,[status(thm)],[f99357,f100760])).
% 76.98/10.49 fof(f100762,plain,(
% 76.98/10.49 multiply(a1,sF1_fnc)=sF2_fnc),
% 76.98/10.49 inference(forward_demodulation,[status(thm)],[f57238,f100761])).
% 76.98/10.49 fof(f100799,plain,(
% 76.98/10.49 ![X0]: (sF2_fnc=multiply(X0,inverse(X0)))),
% 76.98/10.49 inference(backward_demodulation,[status(thm)],[f100762,f57238])).
% 76.98/10.49 fof(f102715,plain,(
% 76.98/10.49 multiply(sF1_fnc,inverse(sF1_fnc))=sF0_fnc),
% 76.98/10.49 inference(paramodulation,[status(thm)],[f100227,f100266])).
% 76.98/10.49 fof(f103090,plain,(
% 76.98/10.49 sF2_fnc=sF0_fnc),
% 76.98/10.49 inference(forward_demodulation,[status(thm)],[f100799,f102715])).
% 76.98/10.49 fof(f103091,plain,(
% 76.98/10.49 $false),
% 76.98/10.49 inference(forward_subsumption_resolution,[status(thm)],[f103090,f9])).
% 76.98/10.49 % SZS output end CNFRefutation for theBenchmark.p
% 7.77/10.52 % Elapsed time: 10.134411 seconds
% 7.77/10.52 % CPU time: 80.090619 seconds
% 7.77/10.52 % Total memory used: 853.820 MB
% 7.77/10.52 % Net memory used: 847.403 MB
%------------------------------------------------------------------------------