%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP426-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 : 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:33:51 PM UTC 2026
% Result : Unsatisfiable 91.35s 12.06s
% Output : CNFRefutation 91.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 68
% Number of leaves : 6
% Syntax : Number of formulae : 113 ( 113 unt; 4 def)
% Number of atoms : 113 ( 112 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 16 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 182 ( 182 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C] : multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),C)))),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C))) = B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,plain,
! [X0,X1,X2] : multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X2),X2))) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f4,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f5,definition,
sF1_fnc = multiply(a3,b3),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f6,definition,
sF0_fnc = multiply(sF1_fnc,c3),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f7,definition,
sF3_fnc = multiply(b3,c3),
introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition]) ).
fof(f8,definition,
sF2_fnc = multiply(a3,sF3_fnc),
introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).
fof(f9,plain,
sF0_fnc != sF2_fnc,
inference(definition_folding,[],[f4,f8,f7,f6,f5]) ).
fof(f10,plain,
! [X0,X1,X2] : multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))),inverse(multiply(inverse(X2),X2))) = X2,
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f11,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))) = multiply(inverse(multiply(X3,inverse(multiply(inverse(X1),X2)))),multiply(X3,inverse(X2))),
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f17,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3)))),inverse(multiply(inverse(X0),multiply(inverse(X3),X3))))),X2)),inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3)))) = multiply(inverse(X3),X3),
inference(paramodulation,[status(thm)],[f3,f10]) ).
fof(f58,plain,
! [X0,X1,X2] : multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X1),X2)))),multiply(a3,inverse(X2))),
inference(equality_split,[status(thm)],[f11]) ).
fof(f59,plain,
! [X0,X1,X2] : multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2))) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X1),X2)))),multiply(a3,inverse(X2))),
inference(equality_split,[status(thm)],[f11]) ).
fof(f60,plain,
! [X0,X1] : X0 = multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),X1)))),multiply(a3,inverse(X1))),
inference(paramodulation,[status(thm)],[f3,f58]) ).
fof(f145,plain,
! [X0,X1,X2] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(a3,inverse(X2))))) = multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X2)))),X2)))),multiply(a3,inverse(X2)))))),multiply(a3,inverse(multiply(a3,inverse(X2))))),
inference(paramodulation,[status(thm)],[f60,f59]) ).
fof(f149,plain,
! [X0,X1,X2] : multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(a3,inverse(X2)))))),inverse(multiply(inverse(multiply(a3,inverse(X2))),multiply(a3,inverse(X2))))) = multiply(a3,inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X2)))),X2))),
inference(paramodulation,[status(thm)],[f60,f3]) ).
fof(f155,plain,
! [X0,X1,X2] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(a3,inverse(X2))))) = multiply(inverse(multiply(a3,inverse(X1))),multiply(a3,inverse(multiply(a3,inverse(X2))))),
inference(forward_demodulation,[status(thm)],[f60,f145]) ).
fof(f198,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(a3,inverse(X2))))) = multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(multiply(a3,inverse(X2))))),
inference(paramodulation,[status(thm)],[f155,f155]) ).
fof(f269,plain,
! [X0,X1,X2] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(a3,inverse(X2))))) = multiply(inverse(multiply(a3,inverse(X1))),multiply(a3,inverse(multiply(a3,inverse(X2))))),
inference(equality_split,[status(thm)],[f198]) ).
fof(f885,plain,
! [X0,X1,X2] : multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(X1),X2)))),multiply(a3,inverse(X2)))),inverse(multiply(inverse(X0),multiply(inverse(X2),X2))))),X1)),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))) = multiply(inverse(X2),X2),
inference(forward_demodulation,[status(thm)],[f59,f17]) ).
fof(f1050,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(multiply(a3,inverse(X0))),multiply(a3,inverse(multiply(a3,inverse(X1)))))),inverse(multiply(inverse(multiply(a3,inverse(X1))),multiply(a3,inverse(X1))))) = multiply(a3,inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),X1))),
inference(forward_demodulation,[status(thm)],[f269,f149]) ).
fof(f1051,plain,
! [X0,X1] : X0 = multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(a3,inverse(X1)))),inverse(multiply(inverse(X1),X1)))),X1))),
inference(paramodulation,[status(thm)],[f3,f1050]) ).
fof(f1105,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2))) = multiply(inverse(multiply(a3,inverse(X1))),multiply(a3,inverse(multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),multiply(a3,inverse(X3)))),inverse(multiply(inverse(X3),X3)))),X3)))))),
inference(paramodulation,[status(thm)],[f1051,f269]) ).
fof(f1125,plain,
! [X0,X1,X2] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2))) = multiply(inverse(multiply(a3,inverse(X1))),multiply(a3,inverse(X2))),
inference(forward_demodulation,[status(thm)],[f1051,f1105]) ).
fof(f1131,plain,
! [X0,X1,X2,X3] : multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X3))) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),X2)))),multiply(a3,inverse(X3))),
inference(paramodulation,[status(thm)],[f3,f1125]) ).
fof(f1145,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2))) = multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(X2))),
inference(paramodulation,[status(thm)],[f1125,f1125]) ).
fof(f1224,plain,
! [X0,X1,X2] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2))) = multiply(inverse(multiply(a3,inverse(X1))),multiply(a3,inverse(X2))),
inference(equality_split,[status(thm)],[f1145]) ).
fof(f1548,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),X1)))),multiply(a3,inverse(X1)))),inverse(X2))) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X1),X1)))),multiply(a3,inverse(X2))),
inference(forward_demodulation,[status(thm)],[f1224,f1131]) ).
fof(f1550,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X1),X1)))),multiply(a3,inverse(multiply(inverse(X1),X1)))),
inference(paramodulation,[status(thm)],[f3,f1548]) ).
fof(f1608,plain,
! [X0] : multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),X0)))),multiply(a3,inverse(multiply(inverse(X0),X0)))) = multiply(inverse(a3),a3),
inference(equality_split,[status(thm)],[f1550]) ).
fof(f1609,plain,
! [X0] : multiply(inverse(X0),X0) = multiply(inverse(a3),a3),
inference(equality_split,[status(thm)],[f1550]) ).
fof(f1662,plain,
! [X0] : inverse(multiply(inverse(X0),X0)) = multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(inverse(a3),a3)),X0)))),multiply(a3,inverse(X0))),
inference(paramodulation,[status(thm)],[f1609,f60]) ).
fof(f1669,plain,
! [X0,X1] : X0 = multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(a3,inverse(X1)))),inverse(multiply(inverse(a3),a3)))),X1))),
inference(paramodulation,[status(thm)],[f1609,f1051]) ).
fof(f1680,plain,
! [X0,X1] : X0 = multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(a3),a3)))),X1)))),multiply(a3,inverse(X1))),
inference(paramodulation,[status(thm)],[f1609,f60]) ).
fof(f1692,plain,
! [X0,X1,X2] : multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(a3),a3))) = X1,
inference(paramodulation,[status(thm)],[f1609,f3]) ).
fof(f1883,plain,
! [X0] : inverse(multiply(inverse(a3),a3)) = multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(inverse(a3),a3)),X0)))),multiply(a3,inverse(X0))),
inference(forward_demodulation,[status(thm)],[f1609,f1662]) ).
fof(f1969,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),X1)))),multiply(a3,inverse(X1)))),inverse(multiply(inverse(a3),a3))) = X0,
inference(forward_demodulation,[status(thm)],[f1224,f1692]) ).
fof(f1996,plain,
! [X0,X1,X2] : multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(a3,inverse(X2)))),inverse(multiply(inverse(X0),multiply(inverse(X2),X2))))),multiply(inverse(multiply(inverse(X1),multiply(a3,inverse(X2)))),inverse(multiply(inverse(a3),a3))))),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))) = multiply(inverse(X2),X2),
inference(paramodulation,[status(thm)],[f1669,f885]) ).
fof(f2021,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),multiply(inverse(X1),X1))))),multiply(a3,inverse(multiply(inverse(a3),a3))))),inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))) = multiply(inverse(X1),X1),
inference(forward_demodulation,[status(thm)],[f1224,f1996]) ).
fof(f2022,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),multiply(inverse(a3),a3))))),multiply(a3,inverse(multiply(inverse(a3),a3))))),inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))) = multiply(inverse(X1),X1),
inference(forward_demodulation,[status(thm)],[f1609,f2021]) ).
fof(f2023,plain,
! [X0] : multiply(inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(inverse(a3),a3)),multiply(inverse(a3),a3))))),multiply(a3,inverse(multiply(inverse(X0),X0))))),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))) = multiply(inverse(X0),X0),
inference(forward_demodulation,[status(thm)],[f1548,f2022]) ).
fof(f2024,plain,
! [X0] : multiply(inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(a3),a3)))),multiply(a3,inverse(multiply(inverse(X0),X0))))),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))) = multiply(inverse(X0),X0),
inference(forward_demodulation,[status(thm)],[f1609,f2023]) ).
fof(f2025,plain,
! [X0] : multiply(inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(a3),a3)))),multiply(a3,inverse(multiply(inverse(a3),a3))))),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))) = multiply(inverse(X0),X0),
inference(forward_demodulation,[status(thm)],[f1609,f2024]) ).
fof(f2026,plain,
! [X0] : multiply(inverse(multiply(inverse(a3),a3)),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))) = multiply(inverse(X0),X0),
inference(forward_demodulation,[status(thm)],[f1608,f2025]) ).
fof(f2027,plain,
! [X0] : multiply(inverse(multiply(inverse(a3),a3)),inverse(multiply(inverse(a3),a3))) = multiply(inverse(X0),X0),
inference(forward_demodulation,[status(thm)],[f1609,f2026]) ).
fof(f2028,plain,
multiply(inverse(multiply(inverse(a3),a3)),inverse(multiply(inverse(a3),a3))) = multiply(inverse(a3),a3),
inference(forward_demodulation,[status(thm)],[f1609,f2027]) ).
fof(f2135,plain,
! [X0] : multiply(inverse(a3),a3) = multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(inverse(a3),a3)),X0)))),multiply(a3,inverse(X0))),
inference(paramodulation,[status(thm)],[f2028,f1680]) ).
fof(f2419,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),X1)))),multiply(a3,inverse(X1)))),multiply(inverse(a3),a3)) = X0,
inference(backward_demodulation,[status(thm)],[f2423,f1969]) ).
fof(f2422,plain,
! [X0,X1] : X0 = multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(a3,inverse(X1)))),multiply(inverse(a3),a3))),X1))),
inference(backward_demodulation,[status(thm)],[f2423,f1669]) ).
fof(f2423,plain,
inverse(multiply(inverse(a3),a3)) = multiply(inverse(a3),a3),
inference(forward_demodulation,[status(thm)],[f2135,f1883]) ).
fof(f2988,plain,
! [X0] : multiply(inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(a3),a3)))),multiply(a3,inverse(X0)))),multiply(inverse(a3),a3)) = X0,
inference(paramodulation,[status(thm)],[f1609,f2419]) ).
fof(f3074,plain,
! [X0] : multiply(inverse(multiply(inverse(multiply(a3,multiply(inverse(a3),a3))),multiply(a3,inverse(X0)))),multiply(inverse(a3),a3)) = X0,
inference(forward_demodulation,[status(thm)],[f2423,f2988]) ).
fof(f3244,plain,
! [X0] : multiply(a3,inverse(X0)) = multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(a3),a3)),multiply(inverse(a3),a3))),X0))),
inference(paramodulation,[status(thm)],[f1609,f2422]) ).
fof(f3284,plain,
! [X0] : multiply(a3,inverse(X0)) = multiply(a3,inverse(multiply(inverse(multiply(inverse(a3),a3)),X0))),
inference(forward_demodulation,[status(thm)],[f1609,f3244]) ).
fof(f3285,plain,
! [X0] : multiply(a3,inverse(X0)) = multiply(a3,inverse(multiply(multiply(inverse(a3),a3),X0))),
inference(forward_demodulation,[status(thm)],[f2423,f3284]) ).
fof(f3762,plain,
! [X0] : multiply(inverse(multiply(inverse(multiply(a3,multiply(inverse(a3),a3))),multiply(a3,inverse(X0)))),multiply(inverse(a3),a3)) = multiply(multiply(inverse(a3),a3),X0),
inference(paramodulation,[status(thm)],[f3285,f3074]) ).
fof(f3783,plain,
! [X0] : X0 = multiply(multiply(inverse(a3),a3),X0),
inference(forward_demodulation,[status(thm)],[f3074,f3762]) ).
fof(f3846,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X1))),multiply(multiply(inverse(a3),a3),inverse(X1)))),inverse(multiply(inverse(X1),X1))) = X0,
inference(paramodulation,[status(thm)],[f3783,f3]) ).
fof(f3878,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1))),inverse(multiply(inverse(X1),X1))) = X0,
inference(forward_demodulation,[status(thm)],[f3783,f3846]) ).
fof(f3879,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1))),inverse(multiply(inverse(a3),a3))) = X0,
inference(forward_demodulation,[status(thm)],[f1609,f3878]) ).
fof(f3880,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1))),multiply(inverse(a3),a3)) = X0,
inference(forward_demodulation,[status(thm)],[f2423,f3879]) ).
fof(f3992,plain,
! [X0] : multiply(inverse(multiply(inverse(inverse(multiply(inverse(a3),a3))),inverse(X0))),multiply(inverse(a3),a3)) = X0,
inference(paramodulation,[status(thm)],[f1609,f3880]) ).
fof(f4094,plain,
! [X0] : multiply(inverse(multiply(inverse(multiply(inverse(a3),a3)),inverse(X0))),multiply(inverse(a3),a3)) = X0,
inference(forward_demodulation,[status(thm)],[f2423,f3992]) ).
fof(f4095,plain,
! [X0] : multiply(inverse(multiply(multiply(inverse(a3),a3),inverse(X0))),multiply(inverse(a3),a3)) = X0,
inference(forward_demodulation,[status(thm)],[f2423,f4094]) ).
fof(f4096,plain,
! [X0] : multiply(inverse(inverse(X0)),multiply(inverse(a3),a3)) = X0,
inference(forward_demodulation,[status(thm)],[f3783,f4095]) ).
fof(f4159,plain,
! [X0] : multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(a3),a3)))),multiply(inverse(a3),a3)) = inverse(X0),
inference(paramodulation,[status(thm)],[f4096,f3880]) ).
fof(f4176,plain,
! [X0] : multiply(inverse(multiply(inverse(inverse(X0)),multiply(inverse(a3),a3))),multiply(inverse(a3),a3)) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f2423,f4159]) ).
fof(f4177,plain,
! [X0] : multiply(inverse(X0),multiply(inverse(a3),a3)) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f4096,f4176]) ).
fof(f4225,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(backward_demodulation,[status(thm)],[f4177,f4096]) ).
fof(f4644,plain,
! [X0,X1,X2] : multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(X2),X2))))) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X1),X2)))),multiply(a3,inverse(X2))),
inference(backward_demodulation,[status(thm)],[f4225,f58]) ).
fof(f4647,plain,
! [X0] : multiply(X0,multiply(inverse(a3),a3)) = inverse(inverse(X0)),
inference(paramodulation,[status(thm)],[f4225,f4177]) ).
fof(f4648,plain,
! [X0] : multiply(X0,inverse(X0)) = multiply(inverse(a3),a3),
inference(paramodulation,[status(thm)],[f4225,f1609]) ).
fof(f4710,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(multiply(a3,inverse(X0))),multiply(a3,inverse(inverse(multiply(inverse(X1),X1)))))),inverse(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X1),X1))))) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),X1)))),multiply(a3,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f1224,f4644]) ).
fof(f4711,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(multiply(a3,inverse(X0))),multiply(a3,multiply(inverse(X1),X1)))),inverse(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X1),X1))))) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),X1)))),multiply(a3,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f4225,f4710]) ).
fof(f4712,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(multiply(a3,inverse(X0))),multiply(a3,multiply(inverse(a3),a3)))),inverse(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X1),X1))))) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),X1)))),multiply(a3,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f1609,f4711]) ).
fof(f4713,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(multiply(a3,inverse(X0))),multiply(a3,multiply(inverse(a3),a3)))),inverse(multiply(multiply(inverse(a3),a3),inverse(multiply(inverse(X1),X1))))) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),X1)))),multiply(a3,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f1609,f4712]) ).
fof(f4714,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(multiply(a3,inverse(X0))),multiply(a3,multiply(inverse(a3),a3)))),inverse(inverse(multiply(inverse(X1),X1)))) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),X1)))),multiply(a3,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f3783,f4713]) ).
fof(f4715,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(multiply(a3,inverse(X0))),multiply(a3,multiply(inverse(a3),a3)))),multiply(inverse(X1),X1)) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),X1)))),multiply(a3,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f4225,f4714]) ).
fof(f4716,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(multiply(a3,inverse(X0))),multiply(a3,multiply(inverse(a3),a3)))),multiply(inverse(a3),a3)) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),X1)))),multiply(a3,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f1609,f4715]) ).
fof(f4717,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(a3,inverse(X0))),multiply(a3,multiply(inverse(a3),a3)))) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),X1)))),multiply(a3,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f4177,f4716]) ).
fof(f4718,plain,
! [X0] : multiply(X0,multiply(inverse(a3),a3)) = X0,
inference(forward_demodulation,[status(thm)],[f4225,f4647]) ).
fof(f5296,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(a3),a3)),multiply(multiply(inverse(X0),X1),inverse(X1)))),inverse(multiply(inverse(X1),X1))) = X0,
inference(paramodulation,[status(thm)],[f4648,f3]) ).
fof(f5304,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X0)))),multiply(inverse(a3),a3))),inverse(multiply(inverse(X0),X0))) = X1,
inference(paramodulation,[status(thm)],[f4648,f3]) ).
fof(f5409,plain,
! [X0,X1] : multiply(inverse(multiply(multiply(inverse(a3),a3),multiply(multiply(inverse(X0),X1),inverse(X1)))),inverse(multiply(inverse(X1),X1))) = X0,
inference(forward_demodulation,[status(thm)],[f2423,f5296]) ).
fof(f5410,plain,
! [X0,X1] : multiply(inverse(multiply(multiply(inverse(X0),X1),inverse(X1))),inverse(multiply(inverse(X1),X1))) = X0,
inference(forward_demodulation,[status(thm)],[f3783,f5409]) ).
fof(f5411,plain,
! [X0,X1] : multiply(inverse(multiply(multiply(inverse(X0),X1),inverse(X1))),inverse(multiply(inverse(a3),a3))) = X0,
inference(forward_demodulation,[status(thm)],[f1609,f5410]) ).
fof(f5412,plain,
! [X0,X1] : multiply(inverse(multiply(multiply(inverse(X0),X1),inverse(X1))),multiply(inverse(a3),a3)) = X0,
inference(forward_demodulation,[status(thm)],[f2423,f5411]) ).
fof(f5413,plain,
! [X0,X1] : inverse(multiply(multiply(inverse(X0),X1),inverse(X1))) = X0,
inference(forward_demodulation,[status(thm)],[f4718,f5412]) ).
fof(f5438,plain,
! [X0,X1] : multiply(inverse(inverse(multiply(X0,inverse(multiply(inverse(X1),X0))))),inverse(multiply(inverse(X0),X0))) = X1,
inference(forward_demodulation,[status(thm)],[f4718,f5304]) ).
fof(f5439,plain,
! [X0,X1] : multiply(multiply(X0,inverse(multiply(inverse(X1),X0))),inverse(multiply(inverse(X0),X0))) = X1,
inference(forward_demodulation,[status(thm)],[f4225,f5438]) ).
fof(f5440,plain,
! [X0,X1] : multiply(multiply(X0,inverse(multiply(inverse(X1),X0))),inverse(multiply(inverse(a3),a3))) = X1,
inference(forward_demodulation,[status(thm)],[f1609,f5439]) ).
fof(f5441,plain,
! [X0,X1] : multiply(multiply(X0,inverse(multiply(inverse(X1),X0))),multiply(inverse(a3),a3)) = X1,
inference(forward_demodulation,[status(thm)],[f2423,f5440]) ).
fof(f5442,plain,
! [X0,X1] : multiply(X0,inverse(multiply(inverse(X1),X0))) = X1,
inference(forward_demodulation,[status(thm)],[f4718,f5441]) ).
fof(f6189,plain,
! [X0,X1] : multiply(X0,inverse(multiply(X1,X0))) = inverse(X1),
inference(paramodulation,[status(thm)],[f4225,f5442]) ).
fof(f7901,plain,
multiply(c3,inverse(sF3_fnc)) = inverse(b3),
inference(paramodulation,[status(thm)],[f7,f6189]) ).
fof(f7907,plain,
! [X0,X1] : multiply(inverse(multiply(X0,X1)),inverse(inverse(X0))) = inverse(X1),
inference(paramodulation,[status(thm)],[f6189,f6189]) ).
fof(f8047,plain,
! [X0,X1] : multiply(inverse(multiply(X0,X1)),X0) = inverse(X1),
inference(forward_demodulation,[status(thm)],[f4225,f7907]) ).
fof(f9676,plain,
multiply(inverse(sF3_fnc),inverse(inverse(b3))) = inverse(c3),
inference(paramodulation,[status(thm)],[f7901,f6189]) ).
fof(f9695,plain,
multiply(inverse(sF3_fnc),b3) = inverse(c3),
inference(forward_demodulation,[status(thm)],[f4225,f9676]) ).
fof(f15939,plain,
inverse(multiply(inverse(c3),inverse(b3))) = sF3_fnc,
inference(paramodulation,[status(thm)],[f9695,f5413]) ).
fof(f17952,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(a3,inverse(X0))),a3)) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),X1)))),multiply(a3,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f4718,f4717]) ).
fof(f17953,plain,
! [X0,X1] : inverse(inverse(inverse(X0))) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),X1)))),multiply(a3,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f8047,f17952]) ).
fof(f17958,plain,
! [X0,X1] : inverse(X0) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),X1)))),multiply(a3,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f4225,f17953]) ).
fof(f18638,plain,
inverse(c3) = multiply(inverse(multiply(a3,sF3_fnc)),multiply(a3,inverse(inverse(b3)))),
inference(paramodulation,[status(thm)],[f15939,f17958]) ).
fof(f18694,plain,
inverse(c3) = multiply(inverse(sF2_fnc),multiply(a3,inverse(inverse(b3)))),
inference(forward_demodulation,[status(thm)],[f8,f18638]) ).
fof(f18695,plain,
inverse(c3) = multiply(inverse(sF2_fnc),multiply(a3,b3)),
inference(forward_demodulation,[status(thm)],[f4225,f18694]) ).
fof(f18696,plain,
inverse(c3) = multiply(inverse(sF2_fnc),sF1_fnc),
inference(forward_demodulation,[status(thm)],[f5,f18695]) ).
fof(f18952,plain,
multiply(sF1_fnc,inverse(inverse(c3))) = inverse(inverse(sF2_fnc)),
inference(paramodulation,[status(thm)],[f18696,f6189]) ).
fof(f18979,plain,
multiply(sF1_fnc,c3) = inverse(inverse(sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f4225,f18952]) ).
fof(f18980,plain,
sF0_fnc = inverse(inverse(sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f6,f18979]) ).
fof(f18981,plain,
sF0_fnc = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f4225,f18980]) ).
fof(f18982,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f18981,f9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP426-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n005.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Sun Sep 20 20:12:48 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.45 % Drodi V4.1.1
% 91.35/12.06 % Refutation found
% 91.35/12.06 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 91.35/12.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.94/12.27 % Elapsed time: 11.816051 seconds
% 4.94/12.27 % CPU time: 92.533472 seconds
% 4.94/12.27 % Total memory used: 827.013 MB
% 4.94/12.27 % Net memory used: 799.203 MB
%------------------------------------------------------------------------------