%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP437-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/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:34:12 PM UTC 2026
% Result : Unsatisfiable 11.12s 1.84s
% Output : CNFRefutation 11.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 5
% Syntax : Number of formulae : 144 ( 144 unt; 3 def)
% Number of atoms : 144 ( 143 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 15 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 254 ( 254 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C,D] : multiply(A,inverse(multiply(B,multiply(C,multiply(multiply(inverse(C),inverse(multiply(D,B))),A))))) = D,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,X1))),X0))))) = X3,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f4,plain,
multiply(multiply(inverse(b2),b2),a2) != a2,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f5,definition,
sF2_fnc = inverse(b2),
introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).
fof(f6,definition,
sF1_fnc = multiply(sF2_fnc,b2),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f7,definition,
sF0_fnc = multiply(sF1_fnc,a2),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f8,plain,
sF0_fnc != a2,
inference(definition_folding,[],[f4,f7,f6,f5]) ).
fof(f10,plain,
! [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,
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f11,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(X1,multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(X2,X1))),X0))))) = X2,
inference(paramodulation,[status(thm)],[f5,f3]) ).
fof(f13,plain,
! [X0,X1] : multiply(X0,inverse(multiply(b2,multiply(X1,multiply(multiply(inverse(X1),inverse(sF1_fnc)),X0))))) = sF2_fnc,
inference(paramodulation,[status(thm)],[f6,f3]) ).
fof(f19,plain,
! [X0] : multiply(X0,inverse(multiply(a2,multiply(b2,multiply(multiply(sF2_fnc,inverse(sF0_fnc)),X0))))) = sF1_fnc,
inference(paramodulation,[status(thm)],[f7,f11]) ).
fof(f23,plain,
! [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,
inference(paramodulation,[status(thm)],[f11,f3]) ).
fof(f25,plain,
! [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,
inference(paramodulation,[status(thm)],[f11,f3]) ).
fof(f41,plain,
! [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,
inference(paramodulation,[status(thm)],[f13,f3]) ).
fof(f88,plain,
! [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))),
inference(paramodulation,[status(thm)],[f11,f10]) ).
fof(f95,plain,
! [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)))),
inference(paramodulation,[status(thm)],[f13,f10]) ).
fof(f98,plain,
! [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)))),
inference(paramodulation,[status(thm)],[f11,f10]) ).
fof(f102,plain,
! [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,
inference(paramodulation,[status(thm)],[f6,f10]) ).
fof(f118,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(inverse(multiply(multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(X2,X3))),inverse(X4))),multiply(X4,multiply(X2,X5)))),multiply(b2,multiply(multiply(sF2_fnc,inverse(X3)),X0))))) = X5,
inference(paramodulation,[status(thm)],[f10,f11]) ).
fof(f244,plain,
! [X0,X1] : multiply(a2,inverse(multiply(multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(sF1_fnc,X0))),inverse(X1))),multiply(X1,sF0_fnc)))) = X0,
inference(paramodulation,[status(thm)],[f7,f23]) ).
fof(f245,plain,
! [X0,X1] : multiply(b2,inverse(multiply(multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(sF2_fnc,X0))),inverse(X1))),multiply(X1,sF1_fnc)))) = X0,
inference(paramodulation,[status(thm)],[f6,f23]) ).
fof(f660,plain,
! [X0,X1] : multiply(b2,inverse(multiply(multiply(X0,multiply(multiply(inverse(X0),inverse(sF1_fnc)),inverse(X1))),multiply(X1,sF1_fnc)))) = b2,
inference(paramodulation,[status(thm)],[f6,f41]) ).
fof(f737,plain,
! [X0] : multiply(b2,inverse(multiply(multiply(b2,multiply(multiply(sF2_fnc,inverse(sF1_fnc)),inverse(X0))),multiply(X0,sF1_fnc)))) = b2,
inference(paramodulation,[status(thm)],[f5,f660]) ).
fof(f2083,plain,
! [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)))),
inference(paramodulation,[status(thm)],[f19,f102]) ).
fof(f2114,plain,
b2 = inverse(multiply(a2,multiply(b2,multiply(multiply(sF2_fnc,inverse(sF0_fnc)),sF2_fnc)))),
inference(forward_demodulation,[status(thm)],[f660,f2083]) ).
fof(f2138,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(b2,multiply(multiply(sF2_fnc,inverse(sF0_fnc)),sF2_fnc)),multiply(X1,multiply(multiply(inverse(X1),b2),X0))))) = a2,
inference(paramodulation,[status(thm)],[f2114,f3]) ).
fof(f5129,plain,
! [X0,X1] : multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(sF2_fnc,inverse(multiply(X0,X1))),X0))),inverse(b2))) = X1,
inference(backward_demodulation,[status(thm)],[f88,f23]) ).
fof(f5132,plain,
! [X0,X1,X2] : multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(inverse(X0),inverse(multiply(X1,X2))),X1))),inverse(X0))) = X2,
inference(backward_demodulation,[status(thm)],[f88,f10]) ).
fof(f5133,plain,
! [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))),
inference(paramodulation,[status(thm)],[f11,f88]) ).
fof(f5320,plain,
! [X0,X1] : multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(sF2_fnc,inverse(multiply(X0,X1))),X0))),sF2_fnc)) = X1,
inference(forward_demodulation,[status(thm)],[f5,f5129]) ).
fof(f5321,plain,
! [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))),
inference(forward_demodulation,[status(thm)],[f5,f5133]) ).
fof(f5454,plain,
! [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)),
inference(paramodulation,[status(thm)],[f25,f5320]) ).
fof(f5559,plain,
! [X0,X1] : multiply(b2,multiply(multiply(sF2_fnc,inverse(X0)),sF2_fnc)) = multiply(X1,multiply(multiply(inverse(X1),inverse(X0)),sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f11,f5454]) ).
fof(f5664,plain,
! [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))),
inference(paramodulation,[status(thm)],[f25,f5132]) ).
fof(f5669,plain,
! [X0,X1] : multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(a2,multiply(b2,multiply(multiply(sF2_fnc,inverse(sF0_fnc)),sF2_fnc))))),inverse(X0))) = multiply(X1,multiply(multiply(inverse(X1),b2),inverse(X0))),
inference(paramodulation,[status(thm)],[f2138,f5132]) ).
fof(f5679,plain,
! [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,
inference(paramodulation,[status(thm)],[f2114,f5132]) ).
fof(f5708,plain,
! [X0] : multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(inverse(X0),inverse(sF1_fnc)),sF2_fnc))),inverse(X0))) = b2,
inference(paramodulation,[status(thm)],[f6,f5132]) ).
fof(f5779,plain,
! [X0,X1,X2] : multiply(b2,multiply(multiply(sF2_fnc,inverse(X0)),inverse(X1))) = multiply(X2,multiply(multiply(inverse(X2),inverse(X0)),inverse(X1))),
inference(forward_demodulation,[status(thm)],[f11,f5664]) ).
fof(f5781,plain,
! [X0,X1] : multiply(b2,multiply(sF1_fnc,inverse(X0))) = multiply(X1,multiply(multiply(inverse(X1),b2),inverse(X0))),
inference(forward_demodulation,[status(thm)],[f19,f5669]) ).
fof(f5784,plain,
! [X0,X1] : multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(b2,inverse(multiply(X0,X1))),X0))),b2)) = X1,
inference(forward_demodulation,[status(thm)],[f2114,f5679]) ).
fof(f5986,plain,
! [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)),
inference(paramodulation,[status(thm)],[f25,f5784]) ).
fof(f6100,plain,
! [X0,X1] : multiply(b2,multiply(multiply(sF2_fnc,inverse(X0)),b2)) = multiply(X1,multiply(multiply(inverse(X1),inverse(X0)),b2)),
inference(forward_demodulation,[status(thm)],[f11,f5986]) ).
fof(f7579,plain,
! [X0,X1] : multiply(b2,inverse(multiply(X0,multiply(X1,sF1_fnc)))) = multiply(sF2_fnc,inverse(multiply(X0,multiply(X1,multiply(sF2_fnc,sF2_fnc))))),
inference(paramodulation,[status(thm)],[f5321,f245]) ).
fof(f7580,plain,
! [X0,X1] : multiply(a2,inverse(multiply(X0,multiply(X1,sF0_fnc)))) = multiply(sF2_fnc,inverse(multiply(X0,multiply(X1,multiply(sF1_fnc,sF2_fnc))))),
inference(paramodulation,[status(thm)],[f5321,f244]) ).
fof(f7583,plain,
! [X0,X1,X2] : multiply(inverse(X0),inverse(multiply(multiply(sF2_fnc,inverse(multiply(X1,multiply(X0,multiply(X2,sF2_fnc))))),X1))) = X2,
inference(paramodulation,[status(thm)],[f5321,f11]) ).
fof(f7649,plain,
! [X0,X1] : multiply(sF2_fnc,inverse(multiply(multiply(sF2_fnc,inverse(multiply(X0,multiply(b2,multiply(X1,sF2_fnc))))),X0))) = X1,
inference(paramodulation,[status(thm)],[f5,f7583]) ).
fof(f7683,plain,
! [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))))),
inference(paramodulation,[status(thm)],[f7583,f3]) ).
fof(f7838,plain,
! [X0] : multiply(sF2_fnc,inverse(multiply(multiply(b2,inverse(multiply(X0,multiply(b2,sF1_fnc)))),X0))) = sF2_fnc,
inference(paramodulation,[status(thm)],[f7579,f7649]) ).
fof(f7839,plain,
! [X0,X1] : multiply(inverse(X0),inverse(multiply(multiply(b2,inverse(multiply(X1,multiply(X0,sF1_fnc)))),X1))) = sF2_fnc,
inference(paramodulation,[status(thm)],[f7579,f7583]) ).
fof(f7903,plain,
! [X0] : multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(sF2_fnc,multiply(b2,inverse(multiply(X0,multiply(b2,sF1_fnc))))))),sF2_fnc)) = X0,
inference(paramodulation,[status(thm)],[f7838,f5320]) ).
fof(f8624,plain,
! [X0] : multiply(sF2_fnc,inverse(multiply(multiply(a2,inverse(multiply(X0,multiply(b2,sF0_fnc)))),X0))) = sF1_fnc,
inference(paramodulation,[status(thm)],[f7580,f7649]) ).
fof(f8709,plain,
! [X0,X1] : multiply(b2,inverse(multiply(multiply(b2,multiply(multiply(sF2_fnc,inverse(sF1_fnc)),inverse(X0))),multiply(X0,sF1_fnc)))) = inverse(multiply(multiply(a2,inverse(multiply(X1,multiply(b2,sF0_fnc)))),X1)),
inference(paramodulation,[status(thm)],[f8624,f245]) ).
fof(f8748,plain,
! [X0] : b2 = inverse(multiply(multiply(a2,inverse(multiply(X0,multiply(b2,sF0_fnc)))),X0)),
inference(forward_demodulation,[status(thm)],[f737,f8709]) ).
fof(f8756,plain,
! [X0] : b2 = inverse(multiply(X0,multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(sF1_fnc,X0))),inverse(b2))))),
inference(paramodulation,[status(thm)],[f244,f8748]) ).
fof(f8864,plain,
! [X0] : b2 = inverse(multiply(X0,multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(sF1_fnc,X0))),sF2_fnc)))),
inference(forward_demodulation,[status(thm)],[f5,f8756]) ).
fof(f9539,plain,
! [X0,X1,X2] : multiply(sF2_fnc,inverse(multiply(multiply(X0,inverse(multiply(X1,multiply(b2,multiply(X2,X0))))),X1))) = X2,
inference(paramodulation,[status(thm)],[f7683,f7649]) ).
fof(f9540,plain,
! [X0,X1,X2,X3] : multiply(inverse(X0),inverse(multiply(multiply(X1,inverse(multiply(X2,multiply(X0,multiply(X3,X1))))),X2))) = X3,
inference(paramodulation,[status(thm)],[f7683,f7583]) ).
fof(f9541,plain,
! [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))),
inference(paramodulation,[status(thm)],[f7683,f5321]) ).
fof(f10074,plain,
! [X0,X1] : multiply(sF2_fnc,inverse(multiply(sF2_fnc,multiply(b2,inverse(multiply(multiply(b2,multiply(X0,inverse(X1))),multiply(X1,sF1_fnc))))))) = X0,
inference(paramodulation,[status(thm)],[f7839,f9539]) ).
fof(f10194,plain,
! [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,
inference(paramodulation,[status(thm)],[f9539,f7583]) ).
fof(f15955,plain,
! [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)))),
inference(forward_demodulation,[status(thm)],[f88,f95]) ).
fof(f16151,plain,
! [X0,X1] : multiply(X0,multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(inverse(X1),inverse(sF2_fnc)),X0))),inverse(X1)))) = sF2_fnc,
inference(paramodulation,[status(thm)],[f15955,f13]) ).
fof(f16348,plain,
! [X0,X1,X2] : multiply(multiply(X0,inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(sF2_fnc)),X0))))),X1) = sF2_fnc,
inference(paramodulation,[status(thm)],[f9541,f16151]) ).
fof(f16629,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(X1,multiply(multiply(inverse(X1),inverse(sF2_fnc)),sF2_fnc)),multiply(b2,sF2_fnc)))) = X0,
inference(paramodulation,[status(thm)],[f16348,f11]) ).
fof(f16789,plain,
! [X0] : multiply(X0,inverse(multiply(multiply(b2,multiply(multiply(sF2_fnc,inverse(sF2_fnc)),sF2_fnc)),multiply(b2,sF2_fnc)))) = X0,
inference(forward_demodulation,[status(thm)],[f5559,f16629]) ).
fof(f17777,plain,
! [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))),
inference(paramodulation,[status(thm)],[f16789,f5779]) ).
fof(f17778,plain,
! [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)),
inference(paramodulation,[status(thm)],[f16789,f6100]) ).
fof(f17939,plain,
! [X0,X1] : multiply(b2,multiply(sF2_fnc,inverse(X0))) = multiply(X1,multiply(inverse(X1),inverse(X0))),
inference(forward_demodulation,[status(thm)],[f16789,f17777]) ).
fof(f17940,plain,
! [X0] : multiply(b2,multiply(sF2_fnc,b2)) = multiply(X0,multiply(inverse(X0),b2)),
inference(forward_demodulation,[status(thm)],[f16789,f17778]) ).
fof(f17941,plain,
! [X0] : multiply(b2,sF1_fnc) = multiply(X0,multiply(inverse(X0),b2)),
inference(forward_demodulation,[status(thm)],[f6,f17940]) ).
fof(f18016,plain,
! [X0,X1] : multiply(inverse(X0),inverse(multiply(multiply(b2,inverse(multiply(X1,multiply(b2,sF1_fnc)))),X1))) = inverse(X0),
inference(paramodulation,[status(thm)],[f17941,f9540]) ).
fof(f18272,plain,
! [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)),
inference(paramodulation,[status(thm)],[f16789,f17939]) ).
fof(f18444,plain,
! [X0] : multiply(b2,sF2_fnc) = multiply(X0,inverse(X0)),
inference(forward_demodulation,[status(thm)],[f16789,f18272]) ).
fof(f18491,plain,
! [X0] : multiply(b2,multiply(sF2_fnc,inverse(inverse(X0)))) = multiply(X0,multiply(b2,sF2_fnc)),
inference(paramodulation,[status(thm)],[f18444,f17939]) ).
fof(f18514,plain,
! [X0] : multiply(b2,multiply(sF1_fnc,inverse(multiply(inverse(X0),b2)))) = multiply(X0,multiply(b2,sF2_fnc)),
inference(paramodulation,[status(thm)],[f18444,f5781]) ).
fof(f19853,plain,
! [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)))),
inference(forward_demodulation,[status(thm)],[f88,f98]) ).
fof(f19858,plain,
! [X0,X1,X2] : X0 = inverse(multiply(X1,multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(X2,X0),X1))),X2)))),
inference(paramodulation,[status(thm)],[f5132,f19853]) ).
fof(f22104,plain,
! [X0,X1,X2,X3] : X0 = inverse(multiply(multiply(X1,inverse(multiply(X2,multiply(X3,multiply(multiply(inverse(X3),X0),X1))))),X2)),
inference(paramodulation,[status(thm)],[f9541,f19858]) ).
fof(f22421,plain,
! [X0,X1,X2] : 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(sF1_fnc)),sF2_fnc))),X2)) = b2,
inference(paramodulation,[status(thm)],[f19858,f5708]) ).
fof(f22437,plain,
! [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,
inference(paramodulation,[status(thm)],[f19858,f5132]) ).
fof(f22508,plain,
! [X0] : multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(X0,inverse(sF1_fnc)),sF2_fnc))),X0)) = b2,
inference(forward_demodulation,[status(thm)],[f19858,f22421]) ).
fof(f22514,plain,
! [X0,X1,X2] : multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(X0,inverse(multiply(X1,X2))),X1))),X0)) = X2,
inference(forward_demodulation,[status(thm)],[f19858,f22437]) ).
fof(f23292,plain,
! [X0,X1,X2] : X0 = inverse(multiply(multiply(X1,inverse(multiply(X2,multiply(b2,multiply(multiply(sF2_fnc,X0),X1))))),X2)),
inference(paramodulation,[status(thm)],[f5,f22104]) ).
fof(f25711,plain,
multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(b2,sF2_fnc),sF2_fnc))),sF1_fnc)) = b2,
inference(paramodulation,[status(thm)],[f18444,f22508]) ).
fof(f26428,plain,
! [X0,X1,X2] : multiply(b2,multiply(multiply(sF2_fnc,X0),X1)) = multiply(X2,multiply(multiply(inverse(X2),X0),X1)),
inference(paramodulation,[status(thm)],[f22104,f22514]) ).
fof(f26496,plain,
! [X0,X1] : multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(multiply(b2,sF2_fnc),X0))),multiply(X0,X1))) = X1,
inference(paramodulation,[status(thm)],[f18444,f22514]) ).
fof(f29051,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(b2,inverse(multiply(X1,multiply(b2,sF1_fnc)))),X1))) = inverse(multiply(multiply(X2,inverse(multiply(X3,multiply(b2,multiply(multiply(sF2_fnc,X0),X2))))),X3)),
inference(paramodulation,[status(thm)],[f23292,f18016]) ).
fof(f29140,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(b2,inverse(multiply(X1,multiply(b2,sF1_fnc)))),X1))) = X0,
inference(forward_demodulation,[status(thm)],[f23292,f29051]) ).
fof(f29161,plain,
! [X0] : multiply(b2,sF2_fnc) = multiply(multiply(b2,inverse(multiply(X0,multiply(b2,sF1_fnc)))),X0),
inference(paramodulation,[status(thm)],[f18444,f29140]) ).
fof(f29362,plain,
! [X0] : multiply(X0,inverse(multiply(b2,sF2_fnc))) = X0,
inference(backward_demodulation,[status(thm)],[f29161,f29140]) ).
fof(f29374,plain,
! [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,inverse(multiply(sF2_fnc,multiply(b2,sF1_fnc)))),
inference(paramodulation,[status(thm)],[f29161,f10194]) ).
fof(f29488,plain,
b2 = multiply(b2,inverse(multiply(sF2_fnc,multiply(b2,sF1_fnc)))),
inference(forward_demodulation,[status(thm)],[f10194,f29374]) ).
fof(f29509,plain,
! [X0] : multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(b2,sF2_fnc))),multiply(inverse(multiply(b2,sF2_fnc)),X0))) = X0,
inference(paramodulation,[status(thm)],[f29362,f26496]) ).
fof(f29642,plain,
! [X0] : multiply(b2,multiply(sF2_fnc,multiply(inverse(multiply(b2,sF2_fnc)),X0))) = X0,
inference(forward_demodulation,[status(thm)],[f29362,f29509]) ).
fof(f29663,plain,
multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(sF2_fnc,b2))),sF2_fnc)) = sF2_fnc,
inference(paramodulation,[status(thm)],[f29488,f7903]) ).
fof(f29720,plain,
multiply(b2,multiply(multiply(sF2_fnc,inverse(sF1_fnc)),sF2_fnc)) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f6,f29663]) ).
fof(f31034,plain,
multiply(b2,multiply(sF2_fnc,inverse(multiply(b2,sF2_fnc)))) = inverse(multiply(b2,sF2_fnc)),
inference(paramodulation,[status(thm)],[f29362,f29642]) ).
fof(f31124,plain,
multiply(b2,sF2_fnc) = inverse(multiply(b2,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f29362,f31034]) ).
fof(f31163,plain,
! [X0] : multiply(X0,multiply(b2,sF2_fnc)) = X0,
inference(backward_demodulation,[status(thm)],[f31124,f29362]) ).
fof(f31248,plain,
! [X0] : multiply(b2,multiply(sF1_fnc,inverse(multiply(inverse(X0),b2)))) = X0,
inference(backward_demodulation,[status(thm)],[f31163,f18514]) ).
fof(f31249,plain,
! [X0] : multiply(b2,multiply(sF2_fnc,inverse(inverse(X0)))) = X0,
inference(backward_demodulation,[status(thm)],[f31163,f18491]) ).
fof(f31302,plain,
b2 = inverse(multiply(multiply(b2,sF2_fnc),multiply(b2,multiply(multiply(sF2_fnc,inverse(sF1_fnc)),sF2_fnc)))),
inference(paramodulation,[status(thm)],[f31163,f8864]) ).
fof(f31391,plain,
b2 = inverse(multiply(multiply(b2,sF2_fnc),sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f29720,f31302]) ).
fof(f31413,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(inverse(multiply(multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(X1,X2))),inverse(X3))),multiply(X3,multiply(X1,X4)))),multiply(b2,multiply(multiply(sF2_fnc,inverse(X2)),X0))))) = X4,
inference(forward_demodulation,[status(thm)],[f26428,f118]) ).
fof(f32047,plain,
multiply(b2,multiply(multiply(sF2_fnc,b2),sF1_fnc)) = b2,
inference(backward_demodulation,[status(thm)],[f31391,f25711]) ).
fof(f32048,plain,
! [X0] : multiply(b2,multiply(multiply(sF2_fnc,b2),multiply(sF2_fnc,X0))) = X0,
inference(paramodulation,[status(thm)],[f31391,f26496]) ).
fof(f32127,plain,
multiply(b2,multiply(sF1_fnc,sF1_fnc)) = b2,
inference(forward_demodulation,[status(thm)],[f6,f32047]) ).
fof(f32128,plain,
! [X0] : multiply(b2,multiply(sF1_fnc,multiply(sF2_fnc,X0))) = X0,
inference(forward_demodulation,[status(thm)],[f6,f32048]) ).
fof(f32315,plain,
multiply(b2,multiply(sF1_fnc,sF2_fnc)) = multiply(b2,sF2_fnc),
inference(paramodulation,[status(thm)],[f31163,f32128]) ).
fof(f32540,plain,
! [X0] : multiply(sF2_fnc,inverse(multiply(multiply(sF2_fnc,inverse(multiply(X0,multiply(b2,sF2_fnc)))),X0))) = sF1_fnc,
inference(paramodulation,[status(thm)],[f32315,f9539]) ).
fof(f32557,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(inverse(multiply(multiply(b2,multiply(multiply(sF2_fnc,inverse(multiply(b2,X1))),inverse(X2))),multiply(X2,multiply(b2,sF2_fnc)))),multiply(b2,multiply(multiply(sF2_fnc,inverse(X1)),X0))))) = multiply(sF1_fnc,sF2_fnc),
inference(paramodulation,[status(thm)],[f32315,f31413]) ).
fof(f32613,plain,
! [X0] : multiply(sF2_fnc,inverse(multiply(multiply(sF2_fnc,inverse(X0)),X0))) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f31163,f32540]) ).
fof(f32641,plain,
sF2_fnc = multiply(sF1_fnc,sF2_fnc),
inference(forward_demodulation,[status(thm)],[f31413,f32557]) ).
fof(f33669,plain,
! [X0] : multiply(sF2_fnc,inverse(multiply(sF2_fnc,multiply(b2,inverse(multiply(X0,multiply(multiply(inverse(X0),b2),sF1_fnc))))))) = sF1_fnc,
inference(paramodulation,[status(thm)],[f31248,f10074]) ).
fof(f33749,plain,
multiply(sF2_fnc,inverse(multiply(sF2_fnc,multiply(b2,inverse(multiply(b2,multiply(multiply(sF2_fnc,b2),sF1_fnc))))))) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f26428,f33669]) ).
fof(f33750,plain,
multiply(sF2_fnc,inverse(multiply(sF2_fnc,multiply(b2,inverse(multiply(b2,multiply(sF1_fnc,sF1_fnc))))))) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f6,f33749]) ).
fof(f33751,plain,
multiply(sF2_fnc,inverse(multiply(sF2_fnc,multiply(b2,inverse(b2))))) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f32127,f33750]) ).
fof(f33752,plain,
multiply(sF2_fnc,inverse(multiply(sF2_fnc,multiply(b2,sF2_fnc)))) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f18444,f33751]) ).
fof(f33753,plain,
multiply(sF2_fnc,inverse(sF2_fnc)) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f31163,f33752]) ).
fof(f33754,plain,
multiply(b2,sF2_fnc) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f18444,f33753]) ).
fof(f33784,plain,
b2 = inverse(multiply(sF1_fnc,sF2_fnc)),
inference(backward_demodulation,[status(thm)],[f33754,f31391]) ).
fof(f33785,plain,
! [X0] : multiply(X0,sF1_fnc) = X0,
inference(backward_demodulation,[status(thm)],[f33754,f31163]) ).
fof(f33790,plain,
! [X0] : sF1_fnc = multiply(X0,inverse(X0)),
inference(backward_demodulation,[status(thm)],[f33754,f18444]) ).
fof(f33852,plain,
b2 = inverse(sF2_fnc),
inference(forward_demodulation,[status(thm)],[f32641,f33784]) ).
fof(f33882,plain,
multiply(b2,multiply(sF2_fnc,inverse(b2))) = sF2_fnc,
inference(paramodulation,[status(thm)],[f33852,f31249]) ).
fof(f33926,plain,
multiply(b2,multiply(sF2_fnc,sF2_fnc)) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f5,f33882]) ).
fof(f36125,plain,
! [X0] : multiply(b2,multiply(sF1_fnc,sF1_fnc)) = inverse(multiply(multiply(sF2_fnc,inverse(X0)),X0)),
inference(paramodulation,[status(thm)],[f32613,f32128]) ).
fof(f36215,plain,
! [X0] : multiply(b2,sF1_fnc) = inverse(multiply(multiply(sF2_fnc,inverse(X0)),X0)),
inference(forward_demodulation,[status(thm)],[f33785,f36125]) ).
fof(f36216,plain,
! [X0] : b2 = inverse(multiply(multiply(sF2_fnc,inverse(X0)),X0)),
inference(forward_demodulation,[status(thm)],[f33785,f36215]) ).
fof(f36415,plain,
! [X0] : multiply(b2,multiply(sF2_fnc,inverse(b2))) = multiply(multiply(sF2_fnc,inverse(X0)),X0),
inference(paramodulation,[status(thm)],[f36216,f31249]) ).
fof(f36496,plain,
! [X0] : multiply(b2,multiply(sF2_fnc,sF2_fnc)) = multiply(multiply(sF2_fnc,inverse(X0)),X0),
inference(forward_demodulation,[status(thm)],[f5,f36415]) ).
fof(f36497,plain,
! [X0] : sF2_fnc = multiply(multiply(sF2_fnc,inverse(X0)),X0),
inference(forward_demodulation,[status(thm)],[f33926,f36496]) ).
fof(f36544,plain,
! [X0,X1] : multiply(multiply(X0,X1),inverse(multiply(X1,multiply(b2,sF2_fnc)))) = X0,
inference(paramodulation,[status(thm)],[f36497,f11]) ).
fof(f36699,plain,
! [X0,X1] : multiply(multiply(X0,X1),inverse(multiply(X1,sF1_fnc))) = X0,
inference(forward_demodulation,[status(thm)],[f33754,f36544]) ).
fof(f36700,plain,
! [X0,X1] : multiply(multiply(X0,X1),inverse(X1)) = X0,
inference(forward_demodulation,[status(thm)],[f33785,f36699]) ).
fof(f36982,plain,
! [X0] : multiply(sF1_fnc,inverse(inverse(X0))) = X0,
inference(paramodulation,[status(thm)],[f33790,f36700]) ).
fof(f37020,plain,
! [X0,X1] : X0 = inverse(multiply(inverse(X0),multiply(b2,multiply(multiply(sF2_fnc,inverse(X1)),X1)))),
inference(paramodulation,[status(thm)],[f36700,f19858]) ).
fof(f37123,plain,
! [X0] : X0 = inverse(multiply(inverse(X0),multiply(b2,sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f36497,f37020]) ).
fof(f37124,plain,
! [X0] : X0 = inverse(multiply(inverse(X0),sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f33754,f37123]) ).
fof(f37125,plain,
! [X0] : X0 = inverse(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f33785,f37124]) ).
fof(f37705,plain,
sF0_fnc = a2,
inference(backward_demodulation,[status(thm)],[f37711,f7]) ).
fof(f37711,plain,
! [X0] : multiply(sF1_fnc,X0) = X0,
inference(forward_demodulation,[status(thm)],[f37125,f36982]) ).
fof(f37856,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f37705,f8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP437-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n013.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sun Sep 20 20:12:35 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.36 % Drodi V4.1.1
% 11.12/1.84 % Refutation found
% 11.12/1.84 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 11.12/1.84 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.46/1.94 % Elapsed time: 1.568335 seconds
% 2.46/1.94 % CPU time: 11.884392 seconds
% 2.46/1.94 % Total memory used: 237.275 MB
% 2.46/1.94 % Net memory used: 232.530 MB
%------------------------------------------------------------------------------