%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP422-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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 3.28s 0.88s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP422-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n008.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 20:13:53 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.15/0.38 % Drodi V4.1.1
% 3.28/0.88 % Refutation found
% 3.28/0.88 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 3.28/0.88 % SZS output start CNFRefutation for theBenchmark
% 3.28/0.88 fof(f1,axiom,(
% 3.28/0.88 (![A,B,C]: (inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(A,C))) = B ))),
% 3.28/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.28/0.88 fof(f2,negated_conjecture,(
% 3.28/0.88 multiply(multiply(inverse(b2),b2),a2) != a2 ),
% 3.28/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.28/0.88 fof(f3,plain,(
% 3.28/0.88 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),multiply(X0,X2)))=X1)),
% 3.28/0.88 inference(cnf_transformation,[status(thm)],[f1])).
% 3.28/0.88 fof(f4,plain,(
% 3.28/0.88 ~multiply(multiply(inverse(b2),b2),a2)=a2),
% 3.28/0.88 inference(cnf_transformation,[status(thm)],[f2])).
% 3.28/0.88 fof(f5,definition,(
% 3.28/0.88 sF2_fnc=inverse(b2)),
% 3.28/0.88 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 3.28/0.88 fof(f6,definition,(
% 3.28/0.88 sF1_fnc=multiply(sF2_fnc,b2)),
% 3.28/0.88 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 3.28/0.88 fof(f7,definition,(
% 3.28/0.88 sF0_fnc=multiply(sF1_fnc,a2)),
% 3.28/0.88 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 3.28/0.88 fof(f8,plain,(
% 3.28/0.88 ~sF0_fnc=a2),
% 3.28/0.88 inference(definition_folding,[],[f4,f7,f6,f5])).
% 3.28/0.88 fof(f9,plain,(
% 3.28/0.88 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))=multiply(inverse(X2),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f3,f3])).
% 3.28/0.88 fof(f17,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),multiply(inverse(b2),inverse(multiply(inverse(b2),b2))))))),sF1_fnc))=X0)),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f6,f3])).
% 3.28/0.88 fof(f24,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),multiply(sF2_fnc,inverse(multiply(inverse(b2),b2))))))),sF1_fnc))=X0)),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f5,f17])).
% 3.28/0.88 fof(f25,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),multiply(sF2_fnc,inverse(multiply(sF2_fnc,b2))))))),sF1_fnc))=X0)),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f5,f24])).
% 3.28/0.88 fof(f26,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc))=X0)),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f6,f25])).
% 3.28/0.88 fof(f27,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(inverse(multiply(sF2_fnc,X0)),sF1_fnc))=multiply(sF2_fnc,inverse(multiply(inverse(X0),multiply(inverse(inverse(sF1_fnc)),inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc))))))))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f3,f26])).
% 3.28/0.88 fof(f28,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X0,multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc))=multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f26,f26])).
% 3.28/0.88 fof(f30,plain,(
% 3.28/0.88 inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(sF2_fnc,multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc))=b2),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f5,f26])).
% 3.28/0.88 fof(f31,plain,(
% 3.28/0.88 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc)),inverse(multiply(X2,multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc)))))))),multiply(X0,multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc))))=X1)),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f26,f3])).
% 3.28/0.88 fof(f34,plain,(
% 3.28/0.88 ![X0]: (multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(inverse(X0)),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc)=X0)),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f28,f26])).
% 3.28/0.88 fof(f39,plain,(
% 3.28/0.88 multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(sF2_fnc),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc)=b2),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f28,f30])).
% 3.28/0.88 fof(f40,plain,(
% 3.28/0.88 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(X2,inverse(multiply(X2,multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc)))))))),multiply(X0,multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc))))=X1)),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f26,f31])).
% 3.28/0.88 fof(f48,plain,(
% 3.28/0.88 ![X0,X1,X2,X3]: (inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))=inverse(multiply(inverse(multiply(X3,X1)),multiply(X3,X2))))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f9,f9])).
% 3.28/0.88 fof(f50,plain,(
% 3.28/0.88 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,b2)))=multiply(sF2_fnc,inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(b2),b2))),inverse(multiply(inverse(inverse(multiply(inverse(b2),b2))),inverse(multiply(inverse(b2),b2)))))))))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f5,f9])).
% 3.28/0.88 fof(f52,plain,(
% 3.28/0.88 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,b2)),multiply(X0,X1)))=multiply(inverse(X1),inverse(multiply(sF2_fnc,multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))))))))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f5,f9])).
% 3.28/0.88 fof(f62,plain,(
% 3.28/0.88 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,b2)))=multiply(sF2_fnc,inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(sF2_fnc,b2))),inverse(multiply(inverse(inverse(multiply(inverse(b2),b2))),inverse(multiply(inverse(b2),b2)))))))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f5,f50])).
% 3.28/0.88 fof(f63,plain,(
% 3.28/0.88 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,b2)))=multiply(sF2_fnc,inverse(multiply(inverse(X1),multiply(inverse(inverse(sF1_fnc)),inverse(multiply(inverse(inverse(multiply(inverse(b2),b2))),inverse(multiply(inverse(b2),b2)))))))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f6,f62])).
% 3.28/0.88 fof(f64,plain,(
% 3.28/0.88 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,b2)))=multiply(sF2_fnc,inverse(multiply(inverse(X1),multiply(inverse(inverse(sF1_fnc)),inverse(multiply(inverse(inverse(multiply(sF2_fnc,b2))),inverse(multiply(inverse(b2),b2)))))))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f5,f63])).
% 3.28/0.88 fof(f65,plain,(
% 3.28/0.88 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,b2)))=multiply(sF2_fnc,inverse(multiply(inverse(X1),multiply(inverse(inverse(sF1_fnc)),inverse(multiply(inverse(inverse(sF1_fnc)),inverse(multiply(inverse(b2),b2)))))))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f6,f64])).
% 3.28/0.88 fof(f66,plain,(
% 3.28/0.88 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,b2)))=multiply(sF2_fnc,inverse(multiply(inverse(X1),multiply(inverse(inverse(sF1_fnc)),inverse(multiply(inverse(inverse(sF1_fnc)),inverse(multiply(sF2_fnc,b2)))))))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f5,f65])).
% 3.28/0.88 fof(f67,plain,(
% 3.28/0.88 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,b2)))=multiply(sF2_fnc,inverse(multiply(inverse(X1),multiply(inverse(inverse(sF1_fnc)),inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc))))))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f6,f66])).
% 3.28/0.88 fof(f69,plain,(
% 3.28/0.88 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,b2)))=inverse(multiply(inverse(multiply(sF2_fnc,X1)),sF1_fnc)))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f27,f67])).
% 3.28/0.88 fof(f115,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(inverse(multiply(inverse(multiply(sF2_fnc,X0)),sF1_fnc))),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc)=multiply(inverse(multiply(X1,X0)),multiply(X1,b2)))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f69,f34])).
% 3.28/0.88 fof(f154,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(inverse(multiply(sF2_fnc,X0)),sF1_fnc)=multiply(inverse(multiply(X1,X0)),multiply(X1,b2)))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f34,f115])).
% 3.28/0.88 fof(f189,plain,(
% 3.28/0.88 multiply(inverse(multiply(sF2_fnc,a2)),sF1_fnc)=multiply(inverse(sF0_fnc),multiply(sF1_fnc,b2))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f7,f154])).
% 3.28/0.88 fof(f246,plain,(
% 3.28/0.88 ![X0,X1]: (inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,X0)))=inverse(multiply(inverse(multiply(X1,b2)),multiply(X1,X0))))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f6,f48])).
% 3.28/0.88 fof(f282,plain,(
% 3.28/0.88 ![X0,X1,X2,X3]: (multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc)=multiply(inverse(multiply(X3,X1)),multiply(X3,X2)))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f48,f34])).
% 3.28/0.88 fof(f302,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,X0)))=multiply(inverse(X0),inverse(multiply(sF2_fnc,multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))))))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f246,f52])).
% 3.28/0.88 fof(f304,plain,(
% 3.28/0.88 ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,X1)),multiply(X0,X2))=multiply(inverse(multiply(X3,X1)),multiply(X3,X2)))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f34,f282])).
% 3.28/0.88 fof(f367,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(inverse(multiply(inverse(sF0_fnc),multiply(sF1_fnc,b2))),multiply(inverse(multiply(sF2_fnc,a2)),X0))=multiply(inverse(multiply(X1,sF1_fnc)),multiply(X1,X0)))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f189,f304])).
% 3.28/0.88 fof(f768,plain,(
% 3.28/0.88 inverse(multiply(inverse(multiply(sF2_fnc,b2)),sF1_fnc))=multiply(sF2_fnc,inverse(multiply(sF2_fnc,multiply(inverse(inverse(sF1_fnc)),inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc)))))))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f5,f27])).
% 3.28/0.88 fof(f785,plain,(
% 3.28/0.88 inverse(multiply(inverse(sF1_fnc),sF1_fnc))=multiply(sF2_fnc,inverse(multiply(sF2_fnc,multiply(inverse(inverse(sF1_fnc)),inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc)))))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f6,f768])).
% 3.28/0.88 fof(f829,plain,(
% 3.28/0.88 ![X0]: (multiply(inverse(multiply(inverse(sF0_fnc),multiply(sF1_fnc,b2))),multiply(inverse(multiply(sF2_fnc,a2)),sF1_fnc))=multiply(inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(inverse(X0)),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc)),X0))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f34,f367])).
% 3.28/0.88 fof(f830,plain,(
% 3.28/0.88 multiply(inverse(multiply(inverse(sF0_fnc),multiply(sF1_fnc,b2))),multiply(inverse(multiply(sF2_fnc,a2)),sF1_fnc))=multiply(inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(sF2_fnc),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc)),b2)),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f39,f367])).
% 3.28/0.88 fof(f899,plain,(
% 3.28/0.88 ![X0]: (multiply(inverse(multiply(inverse(sF0_fnc),multiply(sF1_fnc,b2))),multiply(inverse(sF0_fnc),multiply(sF1_fnc,b2)))=multiply(inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(inverse(X0)),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc)),X0))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f189,f829])).
% 3.28/0.88 fof(f900,plain,(
% 3.28/0.88 ![X0]: (multiply(inverse(multiply(inverse(sF0_fnc),multiply(sF1_fnc,b2))),multiply(inverse(sF0_fnc),multiply(sF1_fnc,b2)))=multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(inverse(inverse(X0))),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc),X0))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f28,f899])).
% 3.28/0.88 fof(f901,plain,(
% 3.28/0.88 ![X0]: (multiply(inverse(multiply(inverse(sF0_fnc),multiply(sF1_fnc,b2))),multiply(inverse(sF0_fnc),multiply(sF1_fnc,b2)))=multiply(inverse(X0),X0))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f34,f900])).
% 3.28/0.88 fof(f902,plain,(
% 3.28/0.88 multiply(inverse(multiply(inverse(sF0_fnc),multiply(sF1_fnc,b2))),multiply(inverse(sF0_fnc),multiply(sF1_fnc,b2)))=multiply(inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(sF2_fnc),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc)),b2)),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f189,f830])).
% 3.28/0.88 fof(f903,plain,(
% 3.28/0.88 multiply(inverse(multiply(inverse(sF0_fnc),multiply(sF1_fnc,b2))),multiply(inverse(sF0_fnc),multiply(sF1_fnc,b2)))=multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(inverse(sF2_fnc)),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc),b2)),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f28,f902])).
% 3.28/0.88 fof(f904,plain,(
% 3.28/0.88 multiply(inverse(multiply(inverse(sF0_fnc),multiply(sF1_fnc,b2))),multiply(inverse(sF0_fnc),multiply(sF1_fnc,b2)))=multiply(sF2_fnc,b2)),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f34,f903])).
% 3.28/0.88 fof(f905,plain,(
% 3.28/0.88 ![X0]: (sF1_fnc=multiply(inverse(X0),X0))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f906,f901])).
% 3.28/0.88 fof(f906,plain,(
% 3.28/0.88 multiply(inverse(multiply(inverse(sF0_fnc),multiply(sF1_fnc,b2))),multiply(inverse(sF0_fnc),multiply(sF1_fnc,b2)))=sF1_fnc),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f6,f904])).
% 3.28/0.88 fof(f932,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(inverse(multiply(sF2_fnc,X0)),sF1_fnc))=multiply(sF2_fnc,inverse(multiply(inverse(X0),multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc))))))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f905,f27])).
% 3.28/0.88 fof(f933,plain,(
% 3.28/0.88 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))=multiply(inverse(X2),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(sF1_fnc))))))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f905,f9])).
% 3.28/0.88 fof(f955,plain,(
% 3.28/0.88 inverse(sF1_fnc)=multiply(sF2_fnc,inverse(multiply(sF2_fnc,multiply(inverse(inverse(sF1_fnc)),inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc)))))))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f905,f785])).
% 3.28/0.88 fof(f992,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,X0)))=multiply(inverse(X0),inverse(multiply(sF2_fnc,multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(sF1_fnc))))))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f905,f302])).
% 3.28/0.88 fof(f1034,plain,(
% 3.28/0.88 ![X0]: (multiply(sF2_fnc,inverse(multiply(inverse(inverse(multiply(X0,multiply(sF2_fnc,inverse(sF1_fnc))))),sF1_fnc)))=multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f1044,f28])).
% 3.28/0.88 fof(f1044,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(inverse(multiply(sF2_fnc,X0)),sF1_fnc))=multiply(sF2_fnc,inverse(multiply(inverse(X0),sF1_fnc))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f905,f932])).
% 3.28/0.88 fof(f1045,plain,(
% 3.28/0.88 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))=multiply(inverse(X2),inverse(multiply(inverse(X1),multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc))))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f905,f933])).
% 3.28/0.88 fof(f1058,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc)),inverse(multiply(inverse(inverse(multiply(inverse(X1),multiply(X0,inverse(multiply(X0,multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc))))))),sF1_fnc)))=X1)),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f1074,f40])).
% 3.28/0.88 fof(f1074,plain,(
% 3.28/0.88 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))=multiply(inverse(X2),inverse(multiply(inverse(X1),sF1_fnc))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f905,f1045])).
% 3.28/0.88 fof(f1103,plain,(
% 3.28/0.88 inverse(sF1_fnc)=multiply(sF2_fnc,inverse(multiply(sF2_fnc,multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc)))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f905,f955])).
% 3.28/0.88 fof(f1104,plain,(
% 3.28/0.88 inverse(sF1_fnc)=multiply(sF2_fnc,inverse(multiply(sF2_fnc,sF1_fnc)))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f905,f1103])).
% 3.28/0.88 fof(f1215,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,X0)))=multiply(inverse(X0),inverse(multiply(sF2_fnc,multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc))))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f905,f992])).
% 3.28/0.88 fof(f1221,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,X0)))=multiply(inverse(X0),inverse(multiply(sF2_fnc,sF1_fnc))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f905,f1215])).
% 3.28/0.88 fof(f1307,plain,(
% 3.28/0.88 ![X0]: (multiply(sF2_fnc,inverse(multiply(inverse(inverse(multiply(inverse(X0),multiply(sF2_fnc,inverse(sF1_fnc))))),sF1_fnc)))=X0)),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f1034,f34])).
% 3.28/0.88 fof(f1330,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(inverse(X0)),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc),inverse(multiply(inverse(inverse(multiply(inverse(X1),multiply(X0,inverse(multiply(X0,multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc))))))),sF1_fnc)))=X1)),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f28,f1058])).
% 3.28/0.88 fof(f1331,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(inverse(multiply(inverse(X1),multiply(X0,inverse(multiply(X0,multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),multiply(sF2_fnc,inverse(sF1_fnc)))))),sF1_fnc))))))),sF1_fnc)))=X1)),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f34,f1330])).
% 3.28/0.88 fof(f1332,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(inverse(multiply(inverse(X1),multiply(X0,inverse(multiply(X0,multiply(sF2_fnc,inverse(multiply(inverse(inverse(multiply(X0,multiply(sF2_fnc,inverse(sF1_fnc))))),sF1_fnc))))))))),sF1_fnc)))=X1)),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1034,f1331])).
% 3.28/0.88 fof(f1367,plain,(
% 3.28/0.88 ![X0,X1,X2]: (multiply(inverse(multiply(X0,X1)),multiply(X0,X2))=multiply(inverse(multiply(inverse(X2),X1)),sF1_fnc))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f905,f304])).
% 3.28/0.88 fof(f1368,plain,(
% 3.28/0.88 ![X0,X1,X2]: (multiply(inverse(multiply(X0,X1)),multiply(X0,X2))=multiply(inverse(sF1_fnc),multiply(inverse(X1),X2)))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f905,f304])).
% 3.28/0.88 fof(f1369,plain,(
% 3.28/0.88 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(X0),X1)),sF1_fnc)=multiply(inverse(multiply(X2,X1)),multiply(X2,X0)))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f905,f304])).
% 3.28/0.88 fof(f1371,plain,(
% 3.28/0.88 ![X0]: (multiply(inverse(multiply(sF2_fnc,X0)),sF1_fnc)=multiply(inverse(sF1_fnc),multiply(inverse(X0),b2)))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f905,f154])).
% 3.28/0.88 fof(f1434,plain,(
% 3.28/0.88 ![X0,X1]: (inverse(multiply(inverse(multiply(inverse(X0),X1)),sF1_fnc))=multiply(inverse(X0),inverse(multiply(inverse(X1),sF1_fnc))))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f1367,f1074])).
% 3.28/0.88 fof(f1447,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(inverse(multiply(inverse(X0),X1)),sF1_fnc)=multiply(inverse(sF1_fnc),multiply(inverse(X1),X0)))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1368,f1369])).
% 3.28/0.88 fof(f1580,plain,(
% 3.28/0.88 ![X0,X1]: (inverse(multiply(inverse(sF1_fnc),multiply(inverse(X0),X1)))=multiply(inverse(X1),inverse(multiply(inverse(X0),sF1_fnc))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1447,f1434])).
% 3.28/0.88 fof(f1611,plain,(
% 3.28/0.88 multiply(sF2_fnc,inverse(multiply(inverse(inverse(sF1_fnc)),sF1_fnc)))=multiply(sF2_fnc,inverse(sF1_fnc))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f905,f1307])).
% 3.28/0.88 fof(f1649,plain,(
% 3.28/0.88 ![X0]: (multiply(inverse(multiply(sF2_fnc,inverse(sF1_fnc))),multiply(sF2_fnc,X0))=multiply(inverse(sF1_fnc),multiply(inverse(inverse(multiply(inverse(inverse(sF1_fnc)),sF1_fnc))),X0)))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f1611,f1368])).
% 3.28/0.88 fof(f1650,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(inverse(X0),multiply(sF2_fnc,X1))=multiply(inverse(sF1_fnc),multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X0),multiply(sF2_fnc,inverse(sF1_fnc))))),sF1_fnc))),X1)))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f1307,f1368])).
% 3.28/0.88 fof(f1678,plain,(
% 3.28/0.88 ![X0]: (multiply(inverse(sF1_fnc),multiply(inverse(inverse(sF1_fnc)),X0))=multiply(inverse(sF1_fnc),multiply(inverse(inverse(multiply(inverse(inverse(sF1_fnc)),sF1_fnc))),X0)))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1368,f1649])).
% 3.28/0.88 fof(f1692,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(inverse(X0),sF1_fnc))=multiply(sF2_fnc,inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X0),multiply(sF2_fnc,inverse(sF1_fnc))))),sF1_fnc))),sF1_fnc))))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f1307,f1044])).
% 3.28/0.88 fof(f1714,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(inverse(sF1_fnc),X0))=multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X0),multiply(sF2_fnc,inverse(sF1_fnc))))),sF1_fnc))),inverse(multiply(sF2_fnc,sF1_fnc))))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f1307,f1221])).
% 3.28/0.88 fof(f1715,plain,(
% 3.28/0.88 inverse(multiply(inverse(sF1_fnc),inverse(sF1_fnc)))=multiply(inverse(inverse(multiply(sF2_fnc,sF1_fnc))),inverse(multiply(sF2_fnc,sF1_fnc)))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f1104,f1221])).
% 3.28/0.88 fof(f1727,plain,(
% 3.28/0.88 inverse(multiply(inverse(sF1_fnc),inverse(sF1_fnc)))=sF1_fnc),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f905,f1715])).
% 3.28/0.88 fof(f1740,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(inverse(sF1_fnc),multiply(inverse(multiply(sF2_fnc,X0)),sF1_fnc)))=multiply(inverse(multiply(inverse(X0),b2)),inverse(multiply(inverse(sF1_fnc),sF1_fnc))))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f1371,f1580])).
% 3.28/0.88 fof(f1742,plain,(
% 3.28/0.88 ![X0,X1]: (inverse(multiply(inverse(sF1_fnc),multiply(inverse(sF1_fnc),multiply(inverse(X0),X1))))=multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(inverse(X1),X0)),sF1_fnc))))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f1447,f1580])).
% 3.28/0.88 fof(f1746,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(inverse(sF1_fnc),sF1_fnc))=multiply(inverse(X0),inverse(multiply(inverse(X0),sF1_fnc))))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f905,f1580])).
% 3.28/0.88 fof(f1752,plain,(
% 3.28/0.88 ![X0,X1,X2]: (multiply(multiply(inverse(X0),inverse(multiply(inverse(X1),sF1_fnc))),multiply(inverse(sF1_fnc),X2))=multiply(inverse(sF1_fnc),multiply(inverse(multiply(inverse(X1),X0)),X2)))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f1580,f1368])).
% 3.28/0.88 fof(f1761,plain,(
% 3.28/0.88 ![X0]: (multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(sF2_fnc,X0)),sF1_fnc)))=multiply(inverse(multiply(inverse(X0),b2)),inverse(multiply(inverse(sF1_fnc),sF1_fnc))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1580,f1740])).
% 3.28/0.88 fof(f1762,plain,(
% 3.28/0.88 ![X0]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(inverse(X0),sF1_fnc))))=multiply(inverse(multiply(inverse(X0),b2)),inverse(multiply(inverse(sF1_fnc),sF1_fnc))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1044,f1761])).
% 3.28/0.88 fof(f1763,plain,(
% 3.28/0.88 ![X0]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(inverse(X0),sF1_fnc))))=multiply(inverse(multiply(inverse(X0),b2)),inverse(sF1_fnc)))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f905,f1762])).
% 3.28/0.88 fof(f1766,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(inverse(multiply(inverse(X0),X1)),inverse(multiply(inverse(sF1_fnc),sF1_fnc)))=multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(inverse(X1),X0)),sF1_fnc))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1580,f1742])).
% 3.28/0.88 fof(f1767,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(inverse(multiply(inverse(X0),X1)),inverse(sF1_fnc))=multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(inverse(X1),X0)),sF1_fnc))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f905,f1766])).
% 3.28/0.88 fof(f1768,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(inverse(multiply(inverse(X0),X1)),inverse(sF1_fnc))=multiply(inverse(sF1_fnc),inverse(multiply(inverse(sF1_fnc),multiply(inverse(X0),X1)))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1447,f1767])).
% 3.28/0.88 fof(f1771,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(inverse(multiply(inverse(X0),X1)),inverse(sF1_fnc))=multiply(inverse(sF1_fnc),multiply(inverse(X1),inverse(multiply(inverse(X0),sF1_fnc)))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1580,f1768])).
% 3.28/0.88 fof(f1784,plain,(
% 3.28/0.88 ![X0]: (inverse(sF1_fnc)=multiply(inverse(X0),inverse(multiply(inverse(X0),sF1_fnc))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f905,f1746])).
% 3.28/0.88 fof(f1809,plain,(
% 3.28/0.88 ![X0]: (multiply(sF1_fnc,multiply(inverse(sF1_fnc),X0))=multiply(inverse(sF1_fnc),multiply(inverse(inverse(sF1_fnc)),X0)))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f1727,f1368])).
% 3.28/0.88 fof(f1815,plain,(
% 3.28/0.88 sF1_fnc=multiply(sF1_fnc,multiply(inverse(sF1_fnc),inverse(sF1_fnc)))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f1727,f905])).
% 3.28/0.88 fof(f1817,plain,(
% 3.28/0.88 ![X0]: (multiply(sF1_fnc,multiply(inverse(sF1_fnc),X0))=multiply(inverse(sF1_fnc),multiply(inverse(inverse(multiply(inverse(inverse(sF1_fnc)),sF1_fnc))),X0)))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f1809,f1678])).
% 3.28/0.88 fof(f1824,plain,(
% 3.28/0.88 inverse(sF1_fnc)=multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(sF1_fnc),inverse(sF1_fnc))),sF1_fnc)))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f1727,f1784])).
% 3.28/0.88 fof(f1825,plain,(
% 3.28/0.88 ![X0,X1]: (inverse(sF1_fnc)=multiply(multiply(inverse(X0),inverse(multiply(inverse(X1),sF1_fnc))),inverse(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(X1),X0))),sF1_fnc))))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f1580,f1784])).
% 3.28/0.88 fof(f1833,plain,(
% 3.28/0.88 inverse(sF1_fnc)=multiply(inverse(multiply(inverse(sF1_fnc),inverse(sF1_fnc))),inverse(multiply(sF1_fnc,sF1_fnc)))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f1727,f1784])).
% 3.28/0.88 fof(f1842,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(inverse(inverse(sF1_fnc)),multiply(inverse(X0),X1))=multiply(inverse(sF1_fnc),multiply(inverse(inverse(multiply(inverse(X0),sF1_fnc))),X1)))),
% 3.28/0.88 inference(paramodulation,[status(thm)],[f1784,f1368])).
% 3.28/0.88 fof(f1843,plain,(
% 3.28/0.88 inverse(sF1_fnc)=multiply(sF1_fnc,inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(sF1_fnc)),sF1_fnc))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1447,f1824])).
% 3.28/0.88 fof(f1844,plain,(
% 3.28/0.88 inverse(sF1_fnc)=multiply(sF1_fnc,multiply(inverse(sF1_fnc),inverse(multiply(inverse(inverse(sF1_fnc)),sF1_fnc))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1580,f1843])).
% 3.28/0.88 fof(f1845,plain,(
% 3.28/0.88 ![X0,X1]: (inverse(sF1_fnc)=multiply(multiply(inverse(X0),inverse(multiply(inverse(X1),sF1_fnc))),inverse(multiply(inverse(sF1_fnc),multiply(inverse(multiply(inverse(X1),X0)),sF1_fnc)))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1447,f1825])).
% 3.28/0.88 fof(f1846,plain,(
% 3.28/0.88 ![X0,X1]: (inverse(sF1_fnc)=multiply(multiply(inverse(X0),inverse(multiply(inverse(X1),sF1_fnc))),multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(inverse(X1),X0)),sF1_fnc)))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1580,f1845])).
% 3.28/0.88 fof(f1847,plain,(
% 3.28/0.88 ![X0,X1]: (inverse(sF1_fnc)=multiply(inverse(sF1_fnc),multiply(inverse(multiply(inverse(X0),X1)),inverse(multiply(inverse(multiply(inverse(X0),X1)),sF1_fnc)))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1752,f1846])).
% 3.28/0.88 fof(f1848,plain,(
% 3.28/0.88 ![X0,X1]: (inverse(sF1_fnc)=multiply(inverse(multiply(inverse(multiply(inverse(X0),X1)),multiply(inverse(X0),X1))),inverse(sF1_fnc)))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1771,f1847])).
% 3.28/0.88 fof(f1849,plain,(
% 3.28/0.88 ![X0]: (inverse(sF1_fnc)=multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(X0),X0))),inverse(sF1_fnc)))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1368,f1848])).
% 3.28/0.88 fof(f1850,plain,(
% 3.28/0.88 ![X0]: (inverse(sF1_fnc)=multiply(multiply(inverse(X0),inverse(multiply(inverse(X0),sF1_fnc))),inverse(sF1_fnc)))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1580,f1849])).
% 3.28/0.88 fof(f1851,plain,(
% 3.28/0.88 sF1_fnc=multiply(sF1_fnc,inverse(sF1_fnc))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f1856,f1815])).
% 3.28/0.88 fof(f1852,plain,(
% 3.28/0.88 inverse(inverse(sF1_fnc))=sF1_fnc),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f1856,f1727])).
% 3.28/0.88 fof(f1856,plain,(
% 3.28/0.88 inverse(sF1_fnc)=multiply(inverse(sF1_fnc),inverse(sF1_fnc))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1784,f1850])).
% 3.28/0.88 fof(f1882,plain,(
% 3.28/0.88 inverse(sF1_fnc)=multiply(sF1_fnc,inverse(multiply(sF1_fnc,sF1_fnc)))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1727,f1833])).
% 3.28/0.88 fof(f1909,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(inverse(X0),multiply(sF2_fnc,X1))=multiply(inverse(inverse(sF1_fnc)),multiply(inverse(inverse(multiply(inverse(X0),multiply(sF2_fnc,inverse(sF1_fnc))))),X1)))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f1842,f1650])).
% 3.28/0.88 fof(f1910,plain,(
% 3.28/0.88 ![X0]: (multiply(sF1_fnc,multiply(inverse(sF1_fnc),X0))=multiply(inverse(inverse(sF1_fnc)),multiply(inverse(inverse(sF1_fnc)),X0)))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f1842,f1817])).
% 3.28/0.88 fof(f1916,plain,(
% 3.28/0.88 inverse(sF1_fnc)=multiply(sF1_fnc,multiply(inverse(sF1_fnc),inverse(multiply(sF1_fnc,sF1_fnc))))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f1852,f1844])).
% 3.28/0.88 fof(f1927,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(inverse(X0),multiply(sF2_fnc,X1))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(inverse(X0),multiply(sF2_fnc,inverse(sF1_fnc))))),X1)))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1852,f1909])).
% 3.28/0.88 fof(f1928,plain,(
% 3.28/0.88 ![X0]: (multiply(sF1_fnc,multiply(inverse(sF1_fnc),X0))=multiply(sF1_fnc,multiply(inverse(inverse(sF1_fnc)),X0)))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1852,f1910])).
% 3.28/0.88 fof(f1931,plain,(
% 3.28/0.88 ![X0]: (multiply(sF1_fnc,multiply(inverse(sF1_fnc),X0))=multiply(sF1_fnc,multiply(sF1_fnc,X0)))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1852,f1928])).
% 3.28/0.88 fof(f1934,plain,(
% 3.28/0.88 inverse(sF1_fnc)=multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(sF1_fnc,sF1_fnc))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1931,f1916])).
% 3.28/0.88 fof(f1935,plain,(
% 3.28/0.88 inverse(sF1_fnc)=multiply(sF1_fnc,inverse(sF1_fnc))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1882,f1934])).
% 3.28/0.88 fof(f1937,plain,(
% 3.28/0.88 ![X0,X1]: (inverse(multiply(sF1_fnc,multiply(inverse(X0),X1)))=multiply(inverse(X1),inverse(multiply(inverse(X0),sF1_fnc))))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f2026,f1580])).
% 3.28/0.88 fof(f1938,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(sF1_fnc,multiply(sF2_fnc,X0)))=multiply(inverse(X0),inverse(multiply(sF2_fnc,sF1_fnc))))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f2026,f1221])).
% 3.28/0.88 fof(f1941,plain,(
% 3.28/0.88 ![X0]: (multiply(inverse(multiply(sF2_fnc,X0)),sF1_fnc)=multiply(sF1_fnc,multiply(inverse(X0),b2)))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f2026,f1371])).
% 3.28/0.88 fof(f1942,plain,(
% 3.28/0.88 ![X0]: (multiply(sF2_fnc,inverse(multiply(inverse(inverse(multiply(inverse(X0),multiply(sF2_fnc,sF1_fnc)))),sF1_fnc)))=X0)),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f2026,f1307])).
% 3.28/0.88 fof(f1950,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(inverse(X0),multiply(sF2_fnc,X1))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(inverse(X0),multiply(sF2_fnc,sF1_fnc)))),X1)))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f2026,f1927])).
% 3.28/0.88 fof(f1955,plain,(
% 3.28/0.88 sF1_fnc=multiply(sF1_fnc,sF1_fnc)),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f2026,f1851])).
% 3.28/0.88 fof(f1970,plain,(
% 3.28/0.88 ![X0]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(inverse(X0),sF1_fnc))))=multiply(inverse(multiply(inverse(X0),b2)),sF1_fnc))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f2026,f1763])).
% 3.28/0.88 fof(f1977,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(inverse(sF1_fnc),X0))=multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X0),multiply(sF2_fnc,sF1_fnc)))),sF1_fnc))),inverse(multiply(sF2_fnc,sF1_fnc))))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f2026,f1714])).
% 3.28/0.88 fof(f1986,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(inverse(X0),sF1_fnc))=multiply(sF2_fnc,inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X0),multiply(sF2_fnc,sF1_fnc)))),sF1_fnc))),sF1_fnc))))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f2026,f1692])).
% 3.28/0.88 fof(f2018,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(inverse(multiply(inverse(X1),multiply(X0,inverse(multiply(X0,multiply(sF2_fnc,inverse(multiply(inverse(inverse(multiply(X0,multiply(sF2_fnc,sF1_fnc)))),sF1_fnc))))))))),sF1_fnc)))=X1)),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f2026,f1332])).
% 3.28/0.88 fof(f2019,plain,(
% 3.28/0.88 ![X0]: (multiply(sF2_fnc,inverse(multiply(inverse(inverse(multiply(X0,multiply(sF2_fnc,inverse(sF1_fnc))))),sF1_fnc)))=multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),multiply(sF2_fnc,sF1_fnc))))),sF1_fnc))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f2026,f1034])).
% 3.28/0.88 fof(f2026,plain,(
% 3.28/0.88 inverse(sF1_fnc)=sF1_fnc),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1851,f1935])).
% 3.28/0.88 fof(f2105,plain,(
% 3.28/0.88 ![X0]: (multiply(sF1_fnc,multiply(sF2_fnc,inverse(multiply(inverse(X0),sF1_fnc))))=multiply(inverse(multiply(inverse(X0),b2)),sF1_fnc))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f2026,f1970])).
% 3.28/0.88 fof(f2106,plain,(
% 3.28/0.88 ![X0]: (multiply(sF1_fnc,multiply(sF2_fnc,inverse(multiply(inverse(X0),sF1_fnc))))=multiply(inverse(sF1_fnc),multiply(inverse(b2),X0)))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1447,f2105])).
% 3.28/0.88 fof(f2107,plain,(
% 3.28/0.88 ![X0]: (multiply(sF1_fnc,multiply(sF2_fnc,inverse(multiply(inverse(X0),sF1_fnc))))=multiply(sF1_fnc,multiply(inverse(b2),X0)))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f2026,f2106])).
% 3.28/0.88 fof(f2108,plain,(
% 3.28/0.88 ![X0]: (multiply(sF1_fnc,multiply(sF2_fnc,inverse(multiply(inverse(X0),sF1_fnc))))=multiply(sF1_fnc,multiply(sF2_fnc,X0)))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f5,f2107])).
% 3.28/0.88 fof(f2118,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(sF1_fnc,X0))=multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X0),multiply(sF2_fnc,sF1_fnc)))),sF1_fnc))),inverse(multiply(sF2_fnc,sF1_fnc))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f2026,f1977])).
% 3.28/0.88 fof(f2119,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(sF1_fnc,X0))=inverse(multiply(sF1_fnc,multiply(sF2_fnc,inverse(multiply(inverse(inverse(multiply(inverse(X0),multiply(sF2_fnc,sF1_fnc)))),sF1_fnc))))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1938,f2118])).
% 3.28/0.88 fof(f2120,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(sF1_fnc,X0))=inverse(multiply(sF1_fnc,multiply(sF2_fnc,inverse(multiply(inverse(X0),multiply(sF2_fnc,sF1_fnc)))))))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f2108,f2119])).
% 3.28/0.88 fof(f2178,plain,(
% 3.28/0.88 ![X0]: (multiply(sF2_fnc,inverse(multiply(inverse(inverse(multiply(X0,multiply(sF2_fnc,sF1_fnc)))),sF1_fnc)))=multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),multiply(sF2_fnc,sF1_fnc))))),sF1_fnc))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f2026,f2019])).
% 3.28/0.88 fof(f2179,plain,(
% 3.28/0.88 ![X0]: (multiply(sF2_fnc,inverse(multiply(inverse(inverse(multiply(X0,multiply(sF2_fnc,sF1_fnc)))),sF1_fnc)))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(inverse(X0),multiply(sF2_fnc,sF1_fnc)))),b2)))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1941,f2178])).
% 3.28/0.88 fof(f2180,plain,(
% 3.28/0.88 ![X0]: (multiply(sF2_fnc,inverse(multiply(inverse(inverse(multiply(X0,multiply(sF2_fnc,sF1_fnc)))),sF1_fnc)))=multiply(inverse(X0),multiply(sF2_fnc,b2)))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1950,f2179])).
% 3.28/0.88 fof(f2182,plain,(
% 3.28/0.88 ![X0]: (multiply(inverse(inverse(X0)),sF1_fnc)=X0)),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f2189,f1942])).
% 3.28/0.88 fof(f2185,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(inverse(multiply(inverse(X1),multiply(X0,inverse(multiply(X0,multiply(inverse(X0),sF1_fnc))))))),sF1_fnc)))=X1)),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f2189,f2018])).
% 3.28/0.88 fof(f2189,plain,(
% 3.28/0.88 ![X0]: (multiply(sF2_fnc,inverse(multiply(inverse(inverse(multiply(X0,multiply(sF2_fnc,sF1_fnc)))),sF1_fnc)))=multiply(inverse(X0),sF1_fnc))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f6,f2180])).
% 3.28/0.88 fof(f2211,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(inverse(X0),sF1_fnc))=multiply(sF2_fnc,inverse(multiply(inverse(inverse(multiply(inverse(X0),multiply(sF2_fnc,sF1_fnc)))),sF1_fnc))))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f2182,f1986])).
% 3.28/0.88 fof(f2214,plain,(
% 3.28/0.88 ![X0]: (multiply(sF2_fnc,inverse(multiply(X0,multiply(sF2_fnc,sF1_fnc))))=multiply(inverse(X0),sF1_fnc))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f2182,f2189])).
% 3.28/0.88 fof(f2216,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(X1),multiply(X0,inverse(multiply(X0,multiply(inverse(X0),sF1_fnc)))))))=X1)),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f2182,f2185])).
% 3.28/0.88 fof(f2236,plain,(
% 3.28/0.88 ![X0,X1]: (inverse(multiply(sF1_fnc,multiply(inverse(X0),X1)))=multiply(inverse(X1),X0))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f2237,f1937])).
% 3.28/0.88 fof(f2237,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(inverse(X0),sF1_fnc))=X0)),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f1942,f2211])).
% 3.28/0.88 fof(f2245,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(sF1_fnc,X0))=inverse(multiply(sF1_fnc,multiply(inverse(inverse(X0)),sF1_fnc))))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f2214,f2120])).
% 3.28/0.88 fof(f2269,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(sF1_fnc,X0))=multiply(inverse(sF1_fnc),inverse(X0)))),
% 3.28/0.88 inference(forward_demodulation,[status(thm)],[f2236,f2245])).
% 3.28/0.88 fof(f2277,plain,(
% 3.28/0.88 ![X0,X1]: (multiply(sF1_fnc,inverse(multiply(inverse(X0),X1)))=multiply(inverse(X1),X0))),
% 3.28/0.88 inference(backward_demodulation,[status(thm)],[f2281,f2236])).
% 3.28/0.88 fof(f2281,plain,(
% 3.28/0.88 ![X0]: (inverse(multiply(sF1_fnc,X0))=multiply(sF1_fnc,inverse(X0)))),
% 3.28/0.91 inference(forward_demodulation,[status(thm)],[f2026,f2269])).
% 3.28/0.91 fof(f2307,plain,(
% 3.28/0.91 ![X0]: (sF1_fnc=multiply(X0,multiply(inverse(X0),sF1_fnc)))),
% 3.28/0.91 inference(paramodulation,[status(thm)],[f2237,f905])).
% 3.28/0.91 fof(f2316,plain,(
% 3.28/0.91 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(X1),multiply(X0,inverse(sF1_fnc)))))=X1)),
% 3.28/0.91 inference(backward_demodulation,[status(thm)],[f2307,f2216])).
% 3.28/0.91 fof(f2324,plain,(
% 3.28/0.91 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(X1),multiply(X0,sF1_fnc))))=X1)),
% 3.28/0.91 inference(forward_demodulation,[status(thm)],[f2026,f2316])).
% 3.28/0.91 fof(f2818,plain,(
% 3.28/0.91 ![X0]: (multiply(inverse(multiply(sF1_fnc,sF1_fnc)),X0)=X0)),
% 3.28/0.91 inference(paramodulation,[status(thm)],[f2277,f2324])).
% 3.28/0.91 fof(f2844,plain,(
% 3.28/0.91 ![X0]: (multiply(multiply(sF1_fnc,inverse(sF1_fnc)),X0)=X0)),
% 3.28/0.91 inference(forward_demodulation,[status(thm)],[f2281,f2818])).
% 3.28/0.91 fof(f2845,plain,(
% 3.28/0.91 ![X0]: (multiply(multiply(sF1_fnc,sF1_fnc),X0)=X0)),
% 3.28/0.91 inference(forward_demodulation,[status(thm)],[f2026,f2844])).
% 3.28/0.91 fof(f2861,plain,(
% 3.28/0.91 sF0_fnc=a2),
% 3.28/0.91 inference(backward_demodulation,[status(thm)],[f2911,f7])).
% 3.28/0.91 fof(f2911,plain,(
% 3.28/0.91 ![X0]: (multiply(sF1_fnc,X0)=X0)),
% 3.28/0.91 inference(forward_demodulation,[status(thm)],[f1955,f2845])).
% 3.28/0.91 fof(f3008,plain,(
% 3.28/0.91 $false),
% 3.28/0.91 inference(forward_subsumption_resolution,[status(thm)],[f2861,f8])).
% 3.28/0.91 % SZS output end CNFRefutation for theBenchmark.p
% 0.41/0.93 % Elapsed time: 0.545976 seconds
% 0.41/0.93 % CPU time: 4.090713 seconds
% 0.41/0.93 % Total memory used: 127.984 MB
% 0.41/0.93 % Net memory used: 125.509 MB
%------------------------------------------------------------------------------