%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP423-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 : n016.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:50 PM UTC 2026
% Result : Unsatisfiable 220.99s 28.65s
% Output : CNFRefutation 220.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 81
% Number of leaves : 6
% Syntax : Number of formulae : 129 ( 129 unt; 4 def)
% Number of atoms : 129 ( 128 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 12 ( 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 : 164 ( 164 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C] : inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),multiply(inverse(C),inverse(multiply(inverse(C),C))))))),multiply(A,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] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),multiply(X0,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] : 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)))))))),
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f15,plain,
! [X0] : inverse(multiply(inverse(multiply(b3,inverse(multiply(inverse(X0),multiply(inverse(c3),inverse(multiply(inverse(c3),c3))))))),sF3_fnc)) = X0,
inference(paramodulation,[status(thm)],[f7,f3]) ).
fof(f17,plain,
! [X0] : inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),multiply(inverse(b3),inverse(multiply(inverse(b3),b3))))))),sF1_fnc)) = X0,
inference(paramodulation,[status(thm)],[f5,f3]) ).
fof(f20,plain,
! [X0] : inverse(multiply(inverse(multiply(b3,X0)),sF3_fnc)) = multiply(inverse(c3),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(c3),c3)))))))),
inference(paramodulation,[status(thm)],[f3,f15]) ).
fof(f21,plain,
! [X0] : inverse(multiply(inverse(multiply(b3,inverse(multiply(X0,multiply(inverse(c3),inverse(multiply(inverse(c3),c3))))))),sF3_fnc)) = multiply(inverse(multiply(b3,inverse(multiply(inverse(X0),multiply(inverse(c3),inverse(multiply(inverse(c3),c3))))))),sF3_fnc),
inference(paramodulation,[status(thm)],[f15,f15]) ).
fof(f73,plain,
! [X0,X1,X2,X3] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))) = inverse(multiply(inverse(multiply(X3,X1)),multiply(X3,X2))),
inference(paramodulation,[status(thm)],[f10,f10]) ).
fof(f117,plain,
! [X0,X1,X2] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))) = X1,
inference(paramodulation,[status(thm)],[f10,f3]) ).
fof(f179,plain,
! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))) = inverse(multiply(inverse(multiply(b3,X1)),multiply(b3,X2))),
inference(equality_split,[status(thm)],[f73]) ).
fof(f180,plain,
! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))) = inverse(multiply(inverse(multiply(b3,X1)),multiply(b3,X2))),
inference(equality_split,[status(thm)],[f73]) ).
fof(f199,plain,
! [X0] : inverse(multiply(inverse(multiply(sF1_fnc,X0)),sF0_fnc)) = inverse(multiply(inverse(multiply(b3,X0)),multiply(b3,c3))),
inference(paramodulation,[status(thm)],[f6,f179]) ).
fof(f223,plain,
! [X0,X1,X2] : inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(b3,X0)),multiply(b3,X1))),multiply(inverse(b3),inverse(multiply(inverse(b3),b3))))))),sF1_fnc)) = multiply(inverse(multiply(X2,X0)),multiply(X2,X1)),
inference(paramodulation,[status(thm)],[f179,f17]) ).
fof(f280,plain,
! [X0] : inverse(multiply(inverse(multiply(sF1_fnc,X0)),sF0_fnc)) = inverse(multiply(inverse(multiply(b3,X0)),sF3_fnc)),
inference(forward_demodulation,[status(thm)],[f7,f199]) ).
fof(f286,plain,
! [X0,X1,X2] : multiply(inverse(multiply(b3,X0)),multiply(b3,X1)) = multiply(inverse(multiply(X2,X0)),multiply(X2,X1)),
inference(forward_demodulation,[status(thm)],[f17,f223]) ).
fof(f375,plain,
! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(b3,X1)),sF3_fnc)),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),multiply(X0,X2))) = multiply(inverse(multiply(sF1_fnc,X1)),sF0_fnc),
inference(paramodulation,[status(thm)],[f280,f3]) ).
fof(f378,plain,
! [X0] : multiply(inverse(multiply(b3,X0)),sF3_fnc) = multiply(inverse(multiply(sF1_fnc,X0)),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f3,f375]) ).
fof(f679,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(multiply(X3,X1)),multiply(X3,X2)),
inference(paramodulation,[status(thm)],[f286,f286]) ).
fof(f682,plain,
! [X0,X1] : multiply(inverse(multiply(b3,X0)),sF3_fnc) = multiply(inverse(multiply(X1,X0)),multiply(X1,c3)),
inference(paramodulation,[status(thm)],[f7,f286]) ).
fof(f699,plain,
! [X0] : multiply(inverse(multiply(b3,sF3_fnc)),multiply(b3,X0)) = multiply(inverse(sF2_fnc),multiply(a3,X0)),
inference(paramodulation,[status(thm)],[f8,f286]) ).
fof(f700,plain,
! [X0] : multiply(inverse(multiply(b3,b3)),multiply(b3,X0)) = multiply(inverse(sF1_fnc),multiply(a3,X0)),
inference(paramodulation,[status(thm)],[f5,f286]) ).
fof(f840,plain,
! [X0,X1,X2] : multiply(inverse(multiply(b3,X0)),multiply(b3,multiply(X1,c3))) = multiply(inverse(multiply(inverse(multiply(X1,X2)),X0)),multiply(inverse(multiply(b3,X2)),sF3_fnc)),
inference(paramodulation,[status(thm)],[f682,f286]) ).
fof(f919,plain,
! [X0,X1,X2] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(multiply(b3,X1)),multiply(b3,X2)),
inference(equality_split,[status(thm)],[f679]) ).
fof(f1765,plain,
! [X0] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(b3,X0)),sF3_fnc))),multiply(inverse(c3),inverse(multiply(inverse(c3),c3))))) = X0,
inference(paramodulation,[status(thm)],[f20,f3]) ).
fof(f1797,plain,
! [X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(b3,X0)),multiply(b3,X1)))),multiply(inverse(X1),inverse(multiply(inverse(X1),X1))))) = X0,
inference(forward_demodulation,[status(thm)],[f180,f117]) ).
fof(f2032,plain,
! [X0] : multiply(inverse(multiply(b3,inverse(multiply(inverse(inverse(X0)),multiply(inverse(c3),inverse(multiply(inverse(c3),c3))))))),sF3_fnc) = X0,
inference(backward_demodulation,[status(thm)],[f21,f15]) ).
fof(f5855,plain,
! [X0] : multiply(inverse(multiply(b3,sF3_fnc)),multiply(b3,multiply(b3,c3))) = multiply(inverse(X0),multiply(inverse(multiply(b3,inverse(multiply(inverse(inverse(X0)),multiply(inverse(c3),inverse(multiply(inverse(c3),c3))))))),sF3_fnc)),
inference(paramodulation,[status(thm)],[f2032,f840]) ).
fof(f6030,plain,
! [X0] : multiply(inverse(sF2_fnc),multiply(a3,multiply(b3,c3))) = multiply(inverse(X0),multiply(inverse(multiply(b3,inverse(multiply(inverse(inverse(X0)),multiply(inverse(c3),inverse(multiply(inverse(c3),c3))))))),sF3_fnc)),
inference(forward_demodulation,[status(thm)],[f699,f5855]) ).
fof(f6031,plain,
! [X0] : multiply(inverse(sF2_fnc),multiply(a3,sF3_fnc)) = multiply(inverse(X0),multiply(inverse(multiply(b3,inverse(multiply(inverse(inverse(X0)),multiply(inverse(c3),inverse(multiply(inverse(c3),c3))))))),sF3_fnc)),
inference(forward_demodulation,[status(thm)],[f7,f6030]) ).
fof(f6032,plain,
! [X0] : multiply(inverse(sF2_fnc),sF2_fnc) = multiply(inverse(X0),multiply(inverse(multiply(b3,inverse(multiply(inverse(inverse(X0)),multiply(inverse(c3),inverse(multiply(inverse(c3),c3))))))),sF3_fnc)),
inference(forward_demodulation,[status(thm)],[f8,f6031]) ).
fof(f6033,plain,
! [X0] : multiply(inverse(sF2_fnc),sF2_fnc) = multiply(inverse(X0),X0),
inference(forward_demodulation,[status(thm)],[f2032,f6032]) ).
fof(f6161,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1),
inference(paramodulation,[status(thm)],[f6033,f6033]) ).
fof(f6237,plain,
! [X0] : inverse(multiply(inverse(inverse(multiply(inverse(sF2_fnc),sF2_fnc))),multiply(inverse(X0),inverse(multiply(inverse(X0),X0))))) = X0,
inference(paramodulation,[status(thm)],[f6033,f1797]) ).
fof(f6278,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(sF2_fnc),sF2_fnc)),multiply(inverse(X0),X1)) = multiply(inverse(multiply(b3,X0)),multiply(b3,X1)),
inference(paramodulation,[status(thm)],[f6033,f919]) ).
fof(f6329,plain,
! [X0] : multiply(inverse(X0),X0) = multiply(inverse(b3),b3),
inference(equality_split,[status(thm)],[f6161]) ).
fof(f6330,plain,
! [X0] : multiply(inverse(X0),X0) = multiply(inverse(b3),b3),
inference(equality_split,[status(thm)],[f6161]) ).
fof(f6412,plain,
! [X0] : inverse(multiply(inverse(b3),b3)) = multiply(inverse(X0),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))))),
inference(paramodulation,[status(thm)],[f6329,f10]) ).
fof(f6876,plain,
! [X0] : inverse(multiply(inverse(b3),b3)) = multiply(inverse(X0),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(b3),b3))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))))),
inference(forward_demodulation,[status(thm)],[f6330,f6412]) ).
fof(f6877,plain,
! [X0] : inverse(multiply(inverse(b3),b3)) = multiply(inverse(X0),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(b3),b3))),inverse(multiply(inverse(b3),b3)))))),
inference(forward_demodulation,[status(thm)],[f6330,f6876]) ).
fof(f6878,plain,
! [X0] : inverse(multiply(inverse(b3),b3)) = multiply(inverse(X0),inverse(multiply(inverse(X0),multiply(inverse(b3),b3)))),
inference(forward_demodulation,[status(thm)],[f6330,f6877]) ).
fof(f7056,plain,
! [X0] : inverse(multiply(inverse(inverse(multiply(inverse(b3),b3))),multiply(inverse(X0),inverse(multiply(inverse(X0),X0))))) = X0,
inference(forward_demodulation,[status(thm)],[f6330,f6237]) ).
fof(f7057,plain,
! [X0] : inverse(multiply(inverse(inverse(multiply(inverse(b3),b3))),multiply(inverse(X0),inverse(multiply(inverse(b3),b3))))) = X0,
inference(forward_demodulation,[status(thm)],[f6330,f7056]) ).
fof(f7491,plain,
inverse(multiply(inverse(b3),b3)) = multiply(inverse(multiply(inverse(b3),b3)),inverse(multiply(inverse(b3),b3))),
inference(paramodulation,[status(thm)],[f6329,f6878]) ).
fof(f7505,plain,
! [X0] : inverse(multiply(inverse(b3),b3)) = multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(b3,X0)),sF3_fnc))),multiply(inverse(c3),inverse(multiply(inverse(c3),c3))))),inverse(multiply(X0,multiply(inverse(b3),b3)))),
inference(paramodulation,[status(thm)],[f1765,f6878]) ).
fof(f7549,plain,
! [X0] : inverse(multiply(inverse(b3),b3)) = multiply(X0,inverse(multiply(X0,multiply(inverse(b3),b3)))),
inference(forward_demodulation,[status(thm)],[f1765,f7505]) ).
fof(f8492,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(b3),b3)),multiply(inverse(X0),X1)) = multiply(inverse(multiply(b3,X0)),multiply(b3,X1)),
inference(forward_demodulation,[status(thm)],[f6330,f6278]) ).
fof(f9317,plain,
inverse(multiply(inverse(inverse(multiply(inverse(b3),b3))),inverse(multiply(inverse(b3),b3)))) = multiply(inverse(b3),b3),
inference(paramodulation,[status(thm)],[f7491,f7057]) ).
fof(f9336,plain,
inverse(multiply(inverse(b3),b3)) = multiply(inverse(b3),b3),
inference(forward_demodulation,[status(thm)],[f6330,f9317]) ).
fof(f9341,plain,
! [X0,X1] : multiply(multiply(inverse(b3),b3),multiply(inverse(X0),X1)) = multiply(inverse(multiply(b3,X0)),multiply(b3,X1)),
inference(backward_demodulation,[status(thm)],[f9336,f8492]) ).
fof(f9344,plain,
! [X0] : multiply(inverse(b3),b3) = multiply(X0,inverse(multiply(X0,multiply(inverse(b3),b3)))),
inference(backward_demodulation,[status(thm)],[f9336,f7549]) ).
fof(f9345,plain,
! [X0] : inverse(multiply(inverse(inverse(multiply(inverse(b3),b3))),multiply(inverse(X0),multiply(inverse(b3),b3)))) = X0,
inference(backward_demodulation,[status(thm)],[f9336,f7057]) ).
fof(f9555,plain,
! [X0] : inverse(multiply(inverse(multiply(inverse(b3),b3)),multiply(inverse(X0),multiply(inverse(b3),b3)))) = X0,
inference(forward_demodulation,[status(thm)],[f9336,f9345]) ).
fof(f9556,plain,
! [X0] : inverse(multiply(multiply(inverse(b3),b3),multiply(inverse(X0),multiply(inverse(b3),b3)))) = X0,
inference(forward_demodulation,[status(thm)],[f9336,f9555]) ).
fof(f10535,plain,
! [X0] : inverse(multiply(inverse(multiply(b3,X0)),multiply(b3,multiply(inverse(b3),b3)))) = X0,
inference(backward_demodulation,[status(thm)],[f9341,f9556]) ).
fof(f10861,plain,
! [X0] : X0 = inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(b3),b3)),inverse(multiply(inverse(multiply(inverse(b3),b3)),multiply(inverse(b3),b3)))))),
inference(paramodulation,[status(thm)],[f3,f10535]) ).
fof(f10935,plain,
! [X0] : X0 = inverse(multiply(inverse(X0),multiply(inverse(b3),b3))),
inference(forward_demodulation,[status(thm)],[f9344,f10861]) ).
fof(f11157,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(inverse(b3),b3)))) = multiply(inverse(multiply(inverse(b3),b3)),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(multiply(inverse(b3),b3)),multiply(inverse(b3),b3)))),inverse(multiply(inverse(multiply(inverse(b3),b3)),inverse(multiply(inverse(multiply(inverse(b3),b3)),multiply(inverse(b3),b3))))))))),
inference(paramodulation,[status(thm)],[f10935,f10]) ).
fof(f11221,plain,
! [X0] : inverse(multiply(inverse(multiply(b3,X0)),multiply(b3,multiply(inverse(b3),b3)))) = multiply(inverse(multiply(inverse(b3),b3)),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(multiply(inverse(b3),b3)),multiply(inverse(b3),b3)))),inverse(multiply(inverse(multiply(inverse(b3),b3)),inverse(multiply(inverse(multiply(inverse(b3),b3)),multiply(inverse(b3),b3))))))))),
inference(forward_demodulation,[status(thm)],[f180,f11157]) ).
fof(f11222,plain,
! [X0] : X0 = multiply(inverse(multiply(inverse(b3),b3)),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(multiply(inverse(b3),b3)),multiply(inverse(b3),b3)))),inverse(multiply(inverse(multiply(inverse(b3),b3)),inverse(multiply(inverse(multiply(inverse(b3),b3)),multiply(inverse(b3),b3))))))))),
inference(forward_demodulation,[status(thm)],[f10535,f11221]) ).
fof(f11223,plain,
! [X0] : X0 = multiply(multiply(inverse(b3),b3),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(multiply(inverse(b3),b3)),multiply(inverse(b3),b3)))),inverse(multiply(inverse(multiply(inverse(b3),b3)),inverse(multiply(inverse(multiply(inverse(b3),b3)),multiply(inverse(b3),b3))))))))),
inference(forward_demodulation,[status(thm)],[f9336,f11222]) ).
fof(f11224,plain,
! [X0] : X0 = multiply(multiply(inverse(b3),b3),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(multiply(b3,b3)),multiply(b3,b3)))),inverse(multiply(inverse(multiply(inverse(b3),b3)),inverse(multiply(inverse(multiply(inverse(b3),b3)),multiply(inverse(b3),b3))))))))),
inference(forward_demodulation,[status(thm)],[f180,f11223]) ).
fof(f11225,plain,
! [X0] : X0 = multiply(multiply(inverse(b3),b3),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(sF1_fnc),multiply(a3,b3)))),inverse(multiply(inverse(multiply(inverse(b3),b3)),inverse(multiply(inverse(multiply(inverse(b3),b3)),multiply(inverse(b3),b3))))))))),
inference(forward_demodulation,[status(thm)],[f700,f11224]) ).
fof(f11226,plain,
! [X0] : X0 = multiply(multiply(inverse(b3),b3),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),inverse(multiply(inverse(multiply(inverse(b3),b3)),inverse(multiply(inverse(multiply(inverse(b3),b3)),multiply(inverse(b3),b3))))))))),
inference(forward_demodulation,[status(thm)],[f5,f11225]) ).
fof(f11227,plain,
! [X0] : X0 = multiply(multiply(inverse(b3),b3),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(b3),b3))),inverse(multiply(inverse(multiply(inverse(b3),b3)),inverse(multiply(inverse(multiply(inverse(b3),b3)),multiply(inverse(b3),b3))))))))),
inference(forward_demodulation,[status(thm)],[f6330,f11226]) ).
fof(f11228,plain,
! [X0] : X0 = multiply(multiply(inverse(b3),b3),inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(b3),b3)),inverse(multiply(inverse(multiply(inverse(b3),b3)),inverse(multiply(inverse(multiply(inverse(b3),b3)),multiply(inverse(b3),b3))))))))),
inference(forward_demodulation,[status(thm)],[f9336,f11227]) ).
fof(f11229,plain,
! [X0] : X0 = multiply(multiply(inverse(b3),b3),inverse(multiply(inverse(X0),multiply(multiply(inverse(b3),b3),inverse(multiply(inverse(multiply(inverse(b3),b3)),inverse(multiply(inverse(multiply(inverse(b3),b3)),multiply(inverse(b3),b3))))))))),
inference(forward_demodulation,[status(thm)],[f9336,f11228]) ).
fof(f11230,plain,
! [X0] : X0 = multiply(multiply(inverse(b3),b3),inverse(multiply(inverse(X0),multiply(multiply(inverse(b3),b3),inverse(multiply(inverse(b3),b3)))))),
inference(forward_demodulation,[status(thm)],[f9344,f11229]) ).
fof(f11231,plain,
! [X0] : X0 = multiply(multiply(inverse(b3),b3),inverse(multiply(inverse(X0),multiply(multiply(inverse(b3),b3),multiply(inverse(b3),b3))))),
inference(forward_demodulation,[status(thm)],[f9336,f11230]) ).
fof(f11232,plain,
! [X0] : X0 = multiply(multiply(inverse(b3),b3),inverse(multiply(inverse(X0),multiply(inverse(multiply(b3,b3)),multiply(b3,b3))))),
inference(forward_demodulation,[status(thm)],[f9341,f11231]) ).
fof(f11233,plain,
! [X0] : X0 = multiply(multiply(inverse(b3),b3),inverse(multiply(inverse(X0),multiply(inverse(sF1_fnc),multiply(a3,b3))))),
inference(forward_demodulation,[status(thm)],[f700,f11232]) ).
fof(f11234,plain,
! [X0] : X0 = multiply(multiply(inverse(b3),b3),inverse(multiply(inverse(X0),multiply(inverse(sF1_fnc),sF1_fnc)))),
inference(forward_demodulation,[status(thm)],[f5,f11233]) ).
fof(f11235,plain,
! [X0] : X0 = multiply(multiply(inverse(b3),b3),inverse(multiply(inverse(X0),multiply(inverse(b3),b3)))),
inference(forward_demodulation,[status(thm)],[f6330,f11234]) ).
fof(f11236,plain,
! [X0] : X0 = multiply(multiply(inverse(b3),b3),X0),
inference(forward_demodulation,[status(thm)],[f10935,f11235]) ).
fof(f11660,plain,
! [X0] : multiply(inverse(multiply(b3,X0)),sF3_fnc) = multiply(inverse(multiply(multiply(inverse(b3),b3),X0)),c3),
inference(paramodulation,[status(thm)],[f11236,f682]) ).
fof(f11670,plain,
! [X0,X1] : multiply(inverse(X0),multiply(multiply(inverse(b3),b3),X1)) = multiply(inverse(multiply(b3,X0)),multiply(b3,X1)),
inference(paramodulation,[status(thm)],[f11236,f919]) ).
fof(f11682,plain,
! [X0,X1] : multiply(inverse(X0),X1) = multiply(inverse(multiply(b3,X0)),multiply(b3,X1)),
inference(forward_demodulation,[status(thm)],[f11236,f11670]) ).
fof(f11694,plain,
! [X0] : multiply(inverse(multiply(b3,X0)),sF3_fnc) = multiply(inverse(X0),c3),
inference(forward_demodulation,[status(thm)],[f11236,f11660]) ).
fof(f11810,plain,
! [X0] : inverse(multiply(inverse(X0),c3)) = multiply(inverse(c3),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(c3),c3)))))))),
inference(backward_demodulation,[status(thm)],[f11694,f20]) ).
fof(f11812,plain,
! [X0] : multiply(inverse(X0),c3) = multiply(inverse(multiply(sF1_fnc,X0)),sF0_fnc),
inference(backward_demodulation,[status(thm)],[f11694,f378]) ).
fof(f11848,plain,
! [X0] : inverse(multiply(inverse(X0),c3)) = multiply(inverse(c3),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(b3),b3))),inverse(multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(c3),c3)))))))),
inference(forward_demodulation,[status(thm)],[f6330,f11810]) ).
fof(f11849,plain,
! [X0] : inverse(multiply(inverse(X0),c3)) = multiply(inverse(c3),inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(b3),b3)),inverse(multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(c3),c3)))))))),
inference(forward_demodulation,[status(thm)],[f9336,f11848]) ).
fof(f11850,plain,
! [X0] : inverse(multiply(inverse(X0),c3)) = multiply(inverse(c3),inverse(multiply(inverse(X0),multiply(multiply(inverse(b3),b3),inverse(multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(c3),c3)))))))),
inference(forward_demodulation,[status(thm)],[f9336,f11849]) ).
fof(f11851,plain,
! [X0] : inverse(multiply(inverse(X0),c3)) = multiply(inverse(c3),inverse(multiply(inverse(X0),inverse(multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(c3),c3))))))),
inference(forward_demodulation,[status(thm)],[f11236,f11850]) ).
fof(f11852,plain,
! [X0] : inverse(multiply(inverse(X0),c3)) = multiply(inverse(c3),inverse(multiply(inverse(X0),inverse(multiply(inverse(b3),b3))))),
inference(forward_demodulation,[status(thm)],[f6330,f11851]) ).
fof(f11853,plain,
! [X0] : inverse(multiply(inverse(X0),c3)) = multiply(inverse(c3),inverse(multiply(inverse(X0),multiply(inverse(b3),b3)))),
inference(forward_demodulation,[status(thm)],[f9336,f11852]) ).
fof(f11854,plain,
! [X0] : inverse(multiply(inverse(X0),c3)) = multiply(inverse(c3),X0),
inference(forward_demodulation,[status(thm)],[f10935,f11853]) ).
fof(f11912,plain,
inverse(multiply(multiply(inverse(b3),b3),c3)) = multiply(inverse(c3),multiply(inverse(b3),b3)),
inference(paramodulation,[status(thm)],[f9336,f11854]) ).
fof(f12121,plain,
inverse(c3) = multiply(inverse(c3),multiply(inverse(b3),b3)),
inference(forward_demodulation,[status(thm)],[f11236,f11912]) ).
fof(f12872,plain,
c3 = inverse(inverse(c3)),
inference(paramodulation,[status(thm)],[f12121,f10935]) ).
fof(f12897,plain,
multiply(c3,inverse(c3)) = multiply(inverse(b3),b3),
inference(paramodulation,[status(thm)],[f12872,f6329]) ).
fof(f13505,plain,
! [X0] : X0 = multiply(multiply(c3,inverse(c3)),X0),
inference(backward_demodulation,[status(thm)],[f12897,f11236]) ).
fof(f13506,plain,
! [X0] : X0 = inverse(multiply(inverse(X0),multiply(c3,inverse(c3)))),
inference(backward_demodulation,[status(thm)],[f12897,f10935]) ).
fof(f13511,plain,
inverse(multiply(inverse(b3),b3)) = multiply(c3,inverse(c3)),
inference(backward_demodulation,[status(thm)],[f12897,f9336]) ).
fof(f13514,plain,
! [X0] : multiply(inverse(X0),X0) = multiply(c3,inverse(c3)),
inference(backward_demodulation,[status(thm)],[f12897,f6330]) ).
fof(f13542,plain,
inverse(multiply(c3,inverse(c3))) = multiply(c3,inverse(c3)),
inference(forward_demodulation,[status(thm)],[f12897,f13511]) ).
fof(f13857,plain,
! [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(c3,inverse(c3))))))),
inference(backward_demodulation,[status(thm)],[f13514,f10]) ).
fof(f13864,plain,
! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(inverse(X2),inverse(multiply(c3,inverse(c3)))))))),multiply(X0,X2))) = X1,
inference(backward_demodulation,[status(thm)],[f13514,f3]) ).
fof(f13902,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(b3,inverse(multiply(inverse(X0),multiply(inverse(X1),inverse(multiply(c3,inverse(c3)))))))),multiply(b3,X1))) = X0,
inference(forward_demodulation,[status(thm)],[f180,f13864]) ).
fof(f13913,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(b3,X0)),multiply(b3,X1))) = multiply(inverse(X1),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(c3,inverse(c3))))))),
inference(forward_demodulation,[status(thm)],[f180,f13857]) ).
fof(f13914,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(b3,X0)),multiply(b3,X1))) = multiply(inverse(X1),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(c3,inverse(c3)))),inverse(multiply(c3,inverse(c3))))))),
inference(forward_demodulation,[status(thm)],[f13514,f13913]) ).
fof(f13915,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(b3,X0)),multiply(b3,X1))) = multiply(inverse(X1),inverse(multiply(inverse(X0),multiply(c3,inverse(c3))))),
inference(forward_demodulation,[status(thm)],[f13514,f13914]) ).
fof(f14078,plain,
! [X0,X1] : multiply(inverse(X0),inverse(multiply(inverse(X1),multiply(inverse(X0),inverse(multiply(c3,inverse(c3))))))) = X1,
inference(backward_demodulation,[status(thm)],[f14083,f13902]) ).
fof(f14083,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(b3,X0)),multiply(b3,X1))) = multiply(inverse(X1),X0),
inference(forward_demodulation,[status(thm)],[f13506,f13915]) ).
fof(f14183,plain,
! [X0,X1] : multiply(inverse(X0),inverse(multiply(inverse(X1),multiply(inverse(X0),multiply(c3,inverse(c3)))))) = X1,
inference(backward_demodulation,[status(thm)],[f13542,f14078]) ).
fof(f14435,plain,
! [X0,X1] : inverse(multiply(inverse(X0),X1)) = multiply(inverse(X1),X0),
inference(backward_demodulation,[status(thm)],[f11682,f14083]) ).
fof(f14449,plain,
! [X0,X1] : multiply(inverse(X0),multiply(inverse(multiply(inverse(X0),multiply(c3,inverse(c3)))),X1)) = X1,
inference(backward_demodulation,[status(thm)],[f14435,f14183]) ).
fof(f14471,plain,
! [X0,X1] : multiply(inverse(X0),multiply(multiply(inverse(multiply(c3,inverse(c3))),X0),X1)) = X1,
inference(forward_demodulation,[status(thm)],[f14435,f14449]) ).
fof(f14472,plain,
! [X0,X1] : multiply(inverse(X0),multiply(multiply(multiply(c3,inverse(c3)),X0),X1)) = X1,
inference(forward_demodulation,[status(thm)],[f13542,f14471]) ).
fof(f14473,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(forward_demodulation,[status(thm)],[f13505,f14472]) ).
fof(f14505,plain,
! [X0,X1] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(paramodulation,[status(thm)],[f14473,f14473]) ).
fof(f14512,plain,
! [X0,X1] : inverse(X0) = multiply(inverse(multiply(X1,X0)),X1),
inference(paramodulation,[status(thm)],[f14473,f14435]) ).
fof(f14533,plain,
! [X0,X1] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(paramodulation,[status(thm)],[f14505,f14473]) ).
fof(f14800,plain,
! [X0,X1] : multiply(multiply(X0,X1),inverse(X1)) = X0,
inference(paramodulation,[status(thm)],[f14512,f14533]) ).
fof(f14801,plain,
! [X0,X1] : inverse(inverse(X0)) = multiply(inverse(X1),multiply(X1,X0)),
inference(paramodulation,[status(thm)],[f14512,f14435]) ).
fof(f14811,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f14473,f14801]) ).
fof(f14872,plain,
multiply(sF1_fnc,inverse(b3)) = a3,
inference(paramodulation,[status(thm)],[f5,f14800]) ).
fof(f14927,plain,
multiply(inverse(inverse(b3)),c3) = multiply(inverse(a3),sF0_fnc),
inference(paramodulation,[status(thm)],[f14872,f11812]) ).
fof(f14932,plain,
multiply(b3,c3) = multiply(inverse(a3),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f14811,f14927]) ).
fof(f14933,plain,
sF3_fnc = multiply(inverse(a3),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7,f14932]) ).
fof(f15049,plain,
multiply(a3,sF3_fnc) = sF0_fnc,
inference(paramodulation,[status(thm)],[f14933,f14533]) ).
fof(f15054,plain,
sF2_fnc = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f8,f15049]) ).
fof(f15055,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f15054,f9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP423-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n016.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 20:17:37 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 220.99/28.65 % Refutation found
% 220.99/28.65 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 220.99/28.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 17.26/28.96 % Elapsed time: 28.552505 seconds
% 17.26/28.96 % CPU time: 224.666378 seconds
% 17.26/28.96 % Total memory used: 1.249 GB
% 17.26/28.96 % Net memory used: 1.239 GB
%------------------------------------------------------------------------------