%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP429-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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:11 PM UTC 2026
% Result : Unsatisfiable 43.23s 5.90s
% Output : CNFRefutation 40.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 62
% Number of leaves : 6
% Syntax : Number of formulae : 176 ( 176 unt; 4 def)
% Number of atoms : 176 ( 175 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 18 ( 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 : 456 ( 456 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C,D] : multiply(A,inverse(multiply(multiply(inverse(multiply(inverse(B),multiply(inverse(A),C))),D),inverse(multiply(B,D))))) = C,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),X3),inverse(multiply(X1,X3))))) = X2,
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(f11,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(inverse(X0)),X2))),X5),inverse(multiply(X4,X5)))),
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f12,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b3),multiply(inverse(X0),X1))),c3),inverse(sF3_fnc)))) = X1,
inference(paramodulation,[status(thm)],[f7,f3]) ).
fof(f13,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(X0),X1))),c3),inverse(sF0_fnc)))) = X1,
inference(paramodulation,[status(thm)],[f6,f3]) ).
fof(f14,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(X0),X1))),sF3_fnc),inverse(sF2_fnc)))) = X1,
inference(paramodulation,[status(thm)],[f8,f3]) ).
fof(f15,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(X0),X1))),b3),inverse(sF1_fnc)))) = X1,
inference(paramodulation,[status(thm)],[f5,f3]) ).
fof(f16,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(X1),X4))),X5),inverse(multiply(X3,X5))))),inverse(X4)))) = X2,
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f17,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b3),X1)),c3),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(b3),multiply(inverse(inverse(X0)),X1))),c3),inverse(sF3_fnc))),
inference(paramodulation,[status(thm)],[f12,f12]) ).
fof(f18,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b3),X1)),c3),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(inverse(inverse(X0)),X1))),X3),inverse(multiply(X2,X3)))),
inference(paramodulation,[status(thm)],[f3,f12]) ).
fof(f19,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(b3),multiply(inverse(inverse(multiply(inverse(X2),multiply(inverse(X0),X3)))),X1))),c3),inverse(sF3_fnc)))))))) = X3,
inference(paramodulation,[status(thm)],[f12,f3]) ).
fof(f22,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),c3),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(X0)),X1))),c3),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f13,f13]) ).
fof(f26,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b3),X1)),c3),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(X0)),X1))),c3),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f13,f12]) ).
fof(f29,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),sF3_fnc),inverse(sF2_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(inverse(X0)),X1))),sF3_fnc),inverse(sF2_fnc))),
inference(paramodulation,[status(thm)],[f14,f14]) ).
fof(f30,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),sF3_fnc),inverse(sF2_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(X0)),X1))),c3),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f13,f14]) ).
fof(f38,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(inverse(X0)),X1))),b3),inverse(sF1_fnc))),
inference(paramodulation,[status(thm)],[f15,f15]) ).
fof(f39,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(inverse(X0)),X1))),sF3_fnc),inverse(sF2_fnc))),
inference(paramodulation,[status(thm)],[f14,f15]) ).
fof(f40,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(X0)),X1))),c3),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f13,f15]) ).
fof(f46,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b3),X1)),c3),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(inverse(X0)),X1))),b3),inverse(sF1_fnc))),
inference(paramodulation,[status(thm)],[f15,f12]) ).
fof(f54,plain,
! [X0,X1,X2] : multiply(multiply(multiply(inverse(multiply(inverse(b3),multiply(inverse(inverse(X0)),X1))),c3),inverse(sF3_fnc)),inverse(multiply(multiply(inverse(multiply(inverse(b3),X2)),c3),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(b3),multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b3),X1)),c3),inverse(sF3_fnc))))),X2))),c3),inverse(sF3_fnc))),
inference(paramodulation,[status(thm)],[f17,f17]) ).
fof(f55,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b3),X1)),c3),inverse(sF3_fnc))))) = X1,
inference(paramodulation,[status(thm)],[f17,f12]) ).
fof(f57,plain,
! [X0,X1,X2] : multiply(multiply(multiply(inverse(multiply(inverse(b3),multiply(inverse(inverse(X0)),X1))),c3),inverse(sF3_fnc)),inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b3),X1)),c3),inverse(sF3_fnc)))),X2))),b3),inverse(sF1_fnc)))) = X2,
inference(paramodulation,[status(thm)],[f17,f15]) ).
fof(f66,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(X0,multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(b3),X2)),c3),inverse(sF3_fnc)))))) = multiply(inverse(inverse(X1)),X2),
inference(paramodulation,[status(thm)],[f17,f55]) ).
fof(f85,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(X0,X1)) = multiply(inverse(inverse(X2)),multiply(inverse(X2),X1)),
inference(paramodulation,[status(thm)],[f12,f66]) ).
fof(f120,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(X0,X1)) = multiply(inverse(X2),multiply(X2,X1)),
inference(paramodulation,[status(thm)],[f85,f85]) ).
fof(f148,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),X3),inverse(multiply(inverse(X0),X3))))) = X2,
inference(paramodulation,[status(thm)],[f85,f3]) ).
fof(f171,plain,
! [X0,X1,X2,X3] : multiply(inverse(inverse(X0)),multiply(inverse(X1),multiply(X1,X2))) = multiply(inverse(X3),multiply(X3,multiply(X0,X2))),
inference(paramodulation,[status(thm)],[f120,f120]) ).
fof(f173,plain,
! [X0] : multiply(inverse(b3),sF3_fnc) = multiply(inverse(X0),multiply(X0,c3)),
inference(paramodulation,[status(thm)],[f7,f120]) ).
fof(f175,plain,
! [X0] : multiply(inverse(a3),sF2_fnc) = multiply(inverse(X0),multiply(X0,sF3_fnc)),
inference(paramodulation,[status(thm)],[f8,f120]) ).
fof(f176,plain,
! [X0] : multiply(inverse(a3),sF1_fnc) = multiply(inverse(X0),multiply(X0,b3)),
inference(paramodulation,[status(thm)],[f5,f120]) ).
fof(f302,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b3),multiply(inverse(X0),c3))),c3),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(b3),sF3_fnc))),X2),inverse(multiply(X1,X2)))),
inference(paramodulation,[status(thm)],[f173,f18]) ).
fof(f305,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b3),multiply(inverse(X0),X1))),c3),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(inverse(X3),multiply(X3,X1)))),X4),inverse(multiply(X2,X4)))),
inference(paramodulation,[status(thm)],[f120,f18]) ).
fof(f350,plain,
! [X0,X1] : c3 = inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(b3),sF3_fnc))),X1),inverse(multiply(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f12,f302]) ).
fof(f353,plain,
! [X0,X1,X2,X3] : X0 = inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X2),multiply(X2,X0)))),X3),inverse(multiply(X1,X3)))),
inference(forward_demodulation,[status(thm)],[f12,f305]) ).
fof(f359,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),multiply(inverse(X0),X3)),inverse(multiply(multiply(inverse(multiply(inverse(b3),X1)),c3),inverse(sF3_fnc))))))))) = X3,
inference(forward_demodulation,[status(thm)],[f17,f19]) ).
fof(f397,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b3),inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),multiply(inverse(inverse(inverse(X0))),X3)),inverse(multiply(multiply(inverse(multiply(inverse(b3),X1)),c3),inverse(sF3_fnc)))))))))),c3),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),X3)),X5),inverse(multiply(X4,X5)))),
inference(paramodulation,[status(thm)],[f359,f18]) ).
fof(f863,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b3),X2)),c3),inverse(sF3_fnc)))),
inference(forward_demodulation,[status(thm)],[f18,f11]) ).
fof(f878,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(inverse(multiply(inverse(X2),X3))),X1))),b3),inverse(sF1_fnc)))))))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b3),X3)),c3),inverse(sF3_fnc)))),
inference(paramodulation,[status(thm)],[f15,f863]) ).
fof(f934,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(X1),X3))),b3),inverse(sF1_fnc)))),inverse(X3)))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b3),X2)),c3),inverse(sF3_fnc)))),
inference(paramodulation,[status(thm)],[f15,f863]) ).
fof(f947,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(inverse(b3),X1)),c3),inverse(sF3_fnc)))))),b3),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),X1)),X3),inverse(multiply(X2,X3)))),
inference(paramodulation,[status(thm)],[f863,f15]) ).
fof(f968,plain,
! [X0,X1,X2] : inverse(multiply(multiply(inverse(multiply(inverse(b3),X0)),c3),inverse(sF3_fnc))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X2),inverse(multiply(X1,X2)))),
inference(forward_demodulation,[status(thm)],[f15,f947]) ).
fof(f981,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),inverse(multiply(multiply(inverse(multiply(inverse(b3),multiply(inverse(X1),X3))),c3),inverse(sF3_fnc)))),inverse(X3)))) = X2,
inference(forward_demodulation,[status(thm)],[f863,f16]) ).
fof(f1024,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(multiply(inverse(multiply(inverse(b3),multiply(inverse(X1),X3))),c3),inverse(sF3_fnc)))),inverse(X3)))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(inverse(X0)),X2))),inverse(multiply(multiply(inverse(multiply(inverse(b3),multiply(inverse(X4),X5))),c3),inverse(sF3_fnc)))),inverse(X5))),
inference(paramodulation,[status(thm)],[f981,f981]) ).
fof(f1252,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X1,X2)),inverse(multiply(inverse(X0),multiply(multiply(inverse(X3),multiply(X3,X4)),X2)))))) = X4,
inference(paramodulation,[status(thm)],[f120,f148]) ).
fof(f1749,plain,
! [X0] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(X0),b3))),c3),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(a3),sF1_fnc))),c3),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f176,f22]) ).
fof(f1758,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(X0),X1))),c3),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(X2),multiply(X2,X1)))),c3),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f120,f22]) ).
fof(f1820,plain,
b3 = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(a3),sF1_fnc))),c3),inverse(sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f13,f1749]) ).
fof(f1834,plain,
! [X0,X1] : X0 = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(X1),multiply(X1,X0)))),c3),inverse(sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f13,f1758]) ).
fof(f1867,plain,
! [X0] : c3 = inverse(multiply(multiply(inverse(multiply(inverse(a3),sF2_fnc)),X0),inverse(multiply(inverse(b3),X0)))),
inference(paramodulation,[status(thm)],[f175,f350]) ).
fof(f1972,plain,
c3 = inverse(multiply(multiply(inverse(b3),sF3_fnc),inverse(multiply(inverse(b3),multiply(multiply(inverse(a3),sF2_fnc),c3))))),
inference(paramodulation,[status(thm)],[f173,f1867]) ).
fof(f2192,plain,
! [X0,X1] : X0 = inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(X1),multiply(X1,X0)))),b3),inverse(sF1_fnc))),
inference(paramodulation,[status(thm)],[f5,f353]) ).
fof(f4540,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(X1),X3))),sF3_fnc),inverse(sF2_fnc)))),inverse(X3)))) = X2,
inference(backward_demodulation,[status(thm)],[f4550,f981]) ).
fof(f4545,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X2)),sF3_fnc),inverse(sF2_fnc)))),
inference(backward_demodulation,[status(thm)],[f4550,f863]) ).
fof(f4550,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),sF3_fnc),inverse(sF2_fnc)))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b3),X1)),c3),inverse(sF3_fnc)))),
inference(forward_demodulation,[status(thm)],[f26,f30]) ).
fof(f5117,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(inverse(a3),X2)),sF3_fnc),inverse(sF2_fnc)))))),inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(X1),X3))),sF3_fnc),inverse(sF2_fnc)))),inverse(X3)))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),X2)),X5),inverse(multiply(X4,X5)))),
inference(paramodulation,[status(thm)],[f4545,f4540]) ).
fof(f5123,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),sF3_fnc),inverse(sF2_fnc)))))),b3),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),X1)),X3),inverse(multiply(X2,X3)))),
inference(paramodulation,[status(thm)],[f4545,f15]) ).
fof(f5179,plain,
! [X0,X1,X2] : inverse(multiply(multiply(inverse(multiply(inverse(a3),X0)),sF3_fnc),inverse(sF2_fnc))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X2),inverse(multiply(X1,X2)))),
inference(forward_demodulation,[status(thm)],[f4540,f5117]) ).
fof(f5185,plain,
! [X0,X1,X2] : inverse(multiply(multiply(inverse(multiply(inverse(a3),X0)),sF3_fnc),inverse(sF2_fnc))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X2),inverse(multiply(X1,X2)))),
inference(forward_demodulation,[status(thm)],[f15,f5123]) ).
fof(f7662,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc))))) = X1,
inference(paramodulation,[status(thm)],[f38,f15]) ).
fof(f7756,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(X1),X3))),b3),inverse(sF1_fnc)))),inverse(X3)))) = X2,
inference(backward_demodulation,[status(thm)],[f7766,f4540]) ).
fof(f7763,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X2)),b3),inverse(sF1_fnc)))),
inference(backward_demodulation,[status(thm)],[f7766,f4545]) ).
fof(f7766,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc)))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),sF3_fnc),inverse(sF2_fnc)))),
inference(forward_demodulation,[status(thm)],[f29,f39]) ).
fof(f8361,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(inverse(a3),X2)),b3),inverse(sF1_fnc)))))),inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(X1),X3))),b3),inverse(sF1_fnc)))),inverse(X3)))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),X2)),X5),inverse(multiply(X4,X5)))),
inference(paramodulation,[status(thm)],[f7763,f7756]) ).
fof(f8367,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc)))))),b3),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),X1)),X3),inverse(multiply(X2,X3)))),
inference(paramodulation,[status(thm)],[f7763,f15]) ).
fof(f8428,plain,
! [X0,X1,X2] : inverse(multiply(multiply(inverse(multiply(inverse(a3),X0)),b3),inverse(sF1_fnc))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X2),inverse(multiply(X1,X2)))),
inference(forward_demodulation,[status(thm)],[f7756,f8361]) ).
fof(f8434,plain,
! [X0,X1,X2] : inverse(multiply(multiply(inverse(multiply(inverse(a3),X0)),b3),inverse(sF1_fnc))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X2),inverse(multiply(X1,X2)))),
inference(forward_demodulation,[status(thm)],[f15,f8367]) ).
fof(f9339,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b3),X1)),c3),inverse(sF3_fnc)))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc)))),
inference(forward_demodulation,[status(thm)],[f38,f46]) ).
fof(f10506,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),X3),inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc))))))))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b3),X3)),c3),inverse(sF3_fnc)))),
inference(forward_demodulation,[status(thm)],[f38,f878]) ).
fof(f10508,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),X3),inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc))))))))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X3)),b3),inverse(sF1_fnc)))),
inference(forward_demodulation,[status(thm)],[f9339,f10506]) ).
fof(f15955,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(X1),X3))),b3),inverse(sF1_fnc)))),inverse(X3)))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X2)),b3),inverse(sF1_fnc)))),
inference(forward_demodulation,[status(thm)],[f9339,f934]) ).
fof(f20988,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(X1),X3))),b3),inverse(sF1_fnc)))),inverse(X3)))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(inverse(X0)),X2))),inverse(multiply(multiply(inverse(multiply(inverse(b3),multiply(inverse(X4),X5))),c3),inverse(sF3_fnc)))),inverse(X5))),
inference(forward_demodulation,[status(thm)],[f9339,f1024]) ).
fof(f20989,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(inverse(inverse(X0)),X1))),inverse(multiply(multiply(inverse(multiply(inverse(b3),multiply(inverse(X2),X3))),c3),inverse(sF3_fnc)))),inverse(X3))),
inference(forward_demodulation,[status(thm)],[f15955,f20988]) ).
fof(f20990,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(inverse(inverse(X0)),X1))),inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(X2),X3))),b3),inverse(sF1_fnc)))),inverse(X3))),
inference(forward_demodulation,[status(thm)],[f9339,f20989]) ).
fof(f22585,plain,
! [X0,X1,X2,X3] : multiply(multiply(inverse(X0),multiply(X0,X1)),inverse(multiply(multiply(inverse(X2),multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(a3),X3)),b3),inverse(sF1_fnc))))),inverse(X3)))) = X1,
inference(paramodulation,[status(thm)],[f7662,f1252]) ).
fof(f22950,plain,
! [X0,X1,X2] : multiply(multiply(inverse(X0),multiply(X0,X1)),inverse(multiply(X2,inverse(X2)))) = X1,
inference(forward_demodulation,[status(thm)],[f7662,f22585]) ).
fof(f23020,plain,
! [X0,X1,X2,X3] : multiply(multiply(inverse(inverse(X0)),multiply(inverse(X1),multiply(X1,X2))),inverse(multiply(X3,inverse(X3)))) = multiply(X0,X2),
inference(paramodulation,[status(thm)],[f171,f22950]) ).
fof(f23228,plain,
! [X0,X1,X2,X3] : multiply(inverse(X0),multiply(X0,inverse(multiply(X1,inverse(X1))))) = multiply(inverse(multiply(inverse(X2),multiply(X2,X3))),X3),
inference(paramodulation,[status(thm)],[f22950,f120]) ).
fof(f26648,plain,
! [X0,X1,X2,X3] : multiply(inverse(inverse(multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc))))))),multiply(inverse(X2),multiply(X2,inverse(multiply(X3,inverse(X3)))))) = X1,
inference(paramodulation,[status(thm)],[f23228,f7662]) ).
fof(f26779,plain,
! [X0,X1,X2] : multiply(inverse(inverse(X0)),multiply(inverse(X1),multiply(X1,inverse(multiply(X2,inverse(X2)))))) = X0,
inference(forward_demodulation,[status(thm)],[f7662,f26648]) ).
fof(f26798,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(X0,multiply(X1,inverse(multiply(X2,inverse(X2)))))) = X1,
inference(paramodulation,[status(thm)],[f171,f26779]) ).
fof(f26953,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(X0),inverse(multiply(X1,inverse(X1)))))),b3),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(X2),inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(inverse(X2)),X3))),b3),inverse(sF1_fnc)))),inverse(X3))),
inference(paramodulation,[status(thm)],[f26779,f20990]) ).
fof(f27065,plain,
! [X0,X1,X2] : inverse(multiply(X0,inverse(X0))) = inverse(multiply(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(inverse(X1)),X2))),b3),inverse(sF1_fnc)))),inverse(X2))),
inference(forward_demodulation,[status(thm)],[f15,f26953]) ).
fof(f27066,plain,
! [X0,X1] : inverse(multiply(X0,inverse(X0))) = inverse(multiply(X1,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f15,f27065]) ).
fof(f27238,plain,
! [X0,X1,X2,X3] : multiply(inverse(inverse(multiply(X0,inverse(X0)))),multiply(inverse(X1),multiply(X1,inverse(multiply(X2,inverse(X2)))))) = multiply(X3,inverse(X3)),
inference(paramodulation,[status(thm)],[f27066,f26779]) ).
fof(f27244,plain,
! [X0,X1,X2,X3,X4] : multiply(multiply(inverse(inverse(multiply(X0,inverse(X0)))),multiply(inverse(X1),multiply(X1,X2))),inverse(multiply(X3,inverse(X3)))) = multiply(multiply(X4,inverse(X4)),X2),
inference(paramodulation,[status(thm)],[f27066,f23020]) ).
fof(f27541,plain,
! [X0,X1] : multiply(X0,inverse(X0)) = multiply(X1,inverse(X1)),
inference(forward_demodulation,[status(thm)],[f26779,f27238]) ).
fof(f27542,plain,
! [X0,X1,X2] : multiply(multiply(X0,inverse(X0)),X1) = multiply(multiply(X2,inverse(X2)),X1),
inference(forward_demodulation,[status(thm)],[f23020,f27244]) ).
fof(f28500,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(X0,multiply(X1,inverse(X1)))) = multiply(X2,inverse(X2)),
inference(paramodulation,[status(thm)],[f27541,f26798]) ).
fof(f29070,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(X1),multiply(X1,multiply(X2,inverse(X2)))))),b3),inverse(sF1_fnc)))) = inverse(inverse(X0)),
inference(paramodulation,[status(thm)],[f28500,f15]) ).
fof(f29180,plain,
! [X0,X1] : multiply(X0,multiply(X1,inverse(X1))) = inverse(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f2192,f29070]) ).
fof(f29191,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,inverse(X1))) = inverse(inverse(inverse(X1))),
inference(paramodulation,[status(thm)],[f120,f29180]) ).
fof(f29581,plain,
! [X0] : multiply(inverse(X0),multiply(X0,c3)) = inverse(inverse(inverse(multiply(multiply(inverse(b3),sF3_fnc),inverse(multiply(inverse(b3),multiply(multiply(inverse(a3),sF2_fnc),c3))))))),
inference(paramodulation,[status(thm)],[f1972,f29191]) ).
fof(f29586,plain,
! [X0] : multiply(inverse(X0),multiply(X0,b3)) = inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(a3),sF1_fnc))),c3),inverse(sF0_fnc))))),
inference(paramodulation,[status(thm)],[f1820,f29191]) ).
fof(f29588,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(X0,X1)) = inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(X2),multiply(X2,X1)))),c3),inverse(sF0_fnc))))),
inference(paramodulation,[status(thm)],[f1834,f29191]) ).
fof(f29756,plain,
multiply(inverse(b3),sF3_fnc) = inverse(inverse(inverse(multiply(multiply(inverse(b3),sF3_fnc),inverse(multiply(inverse(b3),multiply(multiply(inverse(a3),sF2_fnc),c3))))))),
inference(forward_demodulation,[status(thm)],[f173,f29581]) ).
fof(f29757,plain,
multiply(inverse(b3),sF3_fnc) = inverse(inverse(c3)),
inference(forward_demodulation,[status(thm)],[f1972,f29756]) ).
fof(f29765,plain,
multiply(inverse(a3),sF1_fnc) = inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(a3),sF1_fnc))),c3),inverse(sF0_fnc))))),
inference(forward_demodulation,[status(thm)],[f176,f29586]) ).
fof(f29766,plain,
multiply(inverse(a3),sF1_fnc) = inverse(inverse(b3)),
inference(forward_demodulation,[status(thm)],[f1820,f29765]) ).
fof(f29769,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,X1)) = inverse(inverse(X1)),
inference(forward_demodulation,[status(thm)],[f1834,f29588]) ).
fof(f30113,plain,
! [X0,X1] : inverse(inverse(multiply(X0,inverse(multiply(X1,inverse(X1)))))) = X0,
inference(backward_demodulation,[status(thm)],[f29769,f26798]) ).
fof(f30116,plain,
! [X0,X1,X2] : multiply(inverse(inverse(X0)),multiply(inverse(X1),multiply(X1,X2))) = inverse(inverse(multiply(X0,X2))),
inference(backward_demodulation,[status(thm)],[f29769,f171]) ).
fof(f30119,plain,
! [X0,X1] : multiply(inverse(inverse(X0)),inverse(multiply(X1,inverse(X1)))) = X0,
inference(backward_demodulation,[status(thm)],[f29769,f22950]) ).
fof(f30204,plain,
! [X0,X1] : multiply(inverse(inverse(X0)),inverse(inverse(X1))) = inverse(inverse(multiply(X0,X1))),
inference(forward_demodulation,[status(thm)],[f29769,f30116]) ).
fof(f30249,plain,
! [X0,X1] : inverse(inverse(multiply(X0,inverse(X0)))) = multiply(X1,inverse(X1)),
inference(paramodulation,[status(thm)],[f27066,f30113]) ).
fof(f30456,plain,
! [X0,X1,X2] : multiply(X0,inverse(X0)) = multiply(inverse(multiply(X1,inverse(X1))),multiply(X2,inverse(X2))),
inference(paramodulation,[status(thm)],[f30249,f27541]) ).
fof(f30527,plain,
! [X0,X1] : multiply(X0,inverse(inverse(multiply(X1,inverse(X1))))) = inverse(inverse(X0)),
inference(paramodulation,[status(thm)],[f30249,f29180]) ).
fof(f30528,plain,
! [X0,X1,X2] : multiply(multiply(X0,inverse(X0)),X1) = multiply(inverse(inverse(multiply(X2,inverse(X2)))),X1),
inference(paramodulation,[status(thm)],[f30249,f27542]) ).
fof(f30552,plain,
! [X0,X1] : multiply(X0,inverse(X0)) = inverse(inverse(inverse(multiply(X1,inverse(X1))))),
inference(forward_demodulation,[status(thm)],[f29180,f30456]) ).
fof(f30593,plain,
! [X0,X1] : multiply(X0,inverse(X0)) = inverse(multiply(X1,inverse(X1))),
inference(paramodulation,[status(thm)],[f30113,f30552]) ).
fof(f30846,plain,
! [X0,X1,X2] : multiply(multiply(X0,inverse(X0)),X1) = multiply(inverse(multiply(X2,inverse(X2))),X1),
inference(paramodulation,[status(thm)],[f30593,f27542]) ).
fof(f30876,plain,
! [X0,X1] : multiply(inverse(inverse(X0)),multiply(X1,inverse(X1))) = X0,
inference(paramodulation,[status(thm)],[f30593,f30119]) ).
fof(f30891,plain,
! [X0,X1,X2] : multiply(multiply(X0,inverse(X0)),multiply(multiply(X1,inverse(X1)),X2)) = inverse(inverse(X2)),
inference(paramodulation,[status(thm)],[f30593,f29769]) ).
fof(f30931,plain,
! [X0] : inverse(inverse(inverse(inverse(X0)))) = X0,
inference(forward_demodulation,[status(thm)],[f29180,f30876]) ).
fof(f30989,plain,
! [X0,X1] : multiply(X0,multiply(inverse(inverse(inverse(X0))),X1)) = inverse(inverse(X1)),
inference(paramodulation,[status(thm)],[f30931,f29769]) ).
fof(f34962,plain,
! [X0,X1,X2] : multiply(inverse(multiply(X0,inverse(X0))),X1) = multiply(inverse(multiply(X2,inverse(X2))),X1),
inference(paramodulation,[status(thm)],[f30846,f30846]) ).
fof(f38326,plain,
! [X0] : inverse(multiply(multiply(inverse(multiply(inverse(a3),X0)),sF3_fnc),inverse(sF2_fnc))) = inverse(multiply(multiply(inverse(multiply(inverse(b3),X0)),c3),inverse(sF3_fnc))),
inference(forward_demodulation,[status(thm)],[f968,f5179]) ).
fof(f40008,plain,
! [X0] : inverse(multiply(multiply(inverse(multiply(inverse(a3),X0)),b3),inverse(sF1_fnc))) = inverse(multiply(multiply(inverse(multiply(inverse(b3),X0)),c3),inverse(sF3_fnc))),
inference(backward_demodulation,[status(thm)],[f40010,f38326]) ).
fof(f40010,plain,
! [X0] : inverse(multiply(multiply(inverse(multiply(inverse(a3),X0)),b3),inverse(sF1_fnc))) = inverse(multiply(multiply(inverse(multiply(inverse(a3),X0)),sF3_fnc),inverse(sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f5185,f8428]) ).
fof(f44592,plain,
! [X0,X1,X2] : multiply(multiply(multiply(inverse(multiply(inverse(b3),multiply(inverse(inverse(X0)),X1))),c3),inverse(sF3_fnc)),inverse(multiply(multiply(inverse(multiply(inverse(a3),X2)),b3),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(b3),multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b3),X1)),c3),inverse(sF3_fnc))))),X2))),c3),inverse(sF3_fnc))),
inference(forward_demodulation,[status(thm)],[f40008,f54]) ).
fof(f44593,plain,
! [X0,X1,X2] : multiply(multiply(multiply(inverse(multiply(inverse(b3),multiply(inverse(inverse(X0)),X1))),c3),inverse(sF3_fnc)),inverse(multiply(multiply(inverse(multiply(inverse(a3),X2)),b3),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b3),X1)),c3),inverse(sF3_fnc))))),X2))),b3),inverse(sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f40008,f44592]) ).
fof(f44594,plain,
! [X0,X1,X2] : multiply(multiply(multiply(inverse(multiply(inverse(b3),multiply(inverse(inverse(X0)),X1))),c3),inverse(sF3_fnc)),inverse(multiply(multiply(inverse(multiply(inverse(a3),X2)),b3),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc))))),X2))),b3),inverse(sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f40008,f44593]) ).
fof(f45343,plain,
! [X0,X1,X2] : inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc))))),multiply(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b3),X1)),c3),inverse(sF3_fnc)))),X2)))),b3),inverse(sF1_fnc))) = X2,
inference(forward_demodulation,[status(thm)],[f44594,f57]) ).
fof(f45344,plain,
! [X0,X1,X2] : inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc))))),multiply(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc)))),X2)))),b3),inverse(sF1_fnc))) = X2,
inference(forward_demodulation,[status(thm)],[f40008,f45343]) ).
fof(f45345,plain,
! [X0] : inverse(multiply(multiply(inverse(multiply(inverse(a3),inverse(inverse(X0)))),b3),inverse(sF1_fnc))) = X0,
inference(forward_demodulation,[status(thm)],[f29769,f45344]) ).
fof(f50127,plain,
! [X0,X1,X2] : inverse(multiply(multiply(inverse(multiply(inverse(a3),inverse(inverse(X0)))),b3),inverse(sF1_fnc))) = inverse(multiply(multiply(inverse(multiply(X1,inverse(X1))),X2),inverse(multiply(X0,X2)))),
inference(paramodulation,[status(thm)],[f34962,f8434]) ).
fof(f50508,plain,
! [X0,X1,X2] : X0 = inverse(multiply(multiply(inverse(multiply(X1,inverse(X1))),X2),inverse(multiply(X0,X2)))),
inference(forward_demodulation,[status(thm)],[f45345,f50127]) ).
fof(f59465,plain,
! [X0,X1,X2] : X0 = inverse(multiply(inverse(inverse(multiply(X1,inverse(X1)))),inverse(multiply(X0,inverse(inverse(multiply(X2,inverse(X2)))))))),
inference(paramodulation,[status(thm)],[f30528,f50508]) ).
fof(f59864,plain,
! [X0,X1] : X0 = inverse(multiply(inverse(inverse(multiply(X1,inverse(X1)))),inverse(inverse(inverse(X0))))),
inference(forward_demodulation,[status(thm)],[f30527,f59465]) ).
fof(f59865,plain,
! [X0,X1] : X0 = inverse(inverse(inverse(multiply(multiply(X1,inverse(X1)),inverse(X0))))),
inference(forward_demodulation,[status(thm)],[f30204,f59864]) ).
fof(f60223,plain,
! [X0,X1] : inverse(X0) = multiply(multiply(X1,inverse(X1)),inverse(X0)),
inference(paramodulation,[status(thm)],[f59865,f30931]) ).
fof(f60680,plain,
! [X0,X1] : inverse(inverse(inverse(inverse(X0)))) = multiply(multiply(X1,inverse(X1)),X0),
inference(paramodulation,[status(thm)],[f30931,f60223]) ).
fof(f60892,plain,
! [X0,X1] : X0 = multiply(multiply(X1,inverse(X1)),X0),
inference(forward_demodulation,[status(thm)],[f30931,f60680]) ).
fof(f61016,plain,
! [X0,X1] : multiply(multiply(X0,inverse(X0)),X1) = inverse(inverse(X1)),
inference(backward_demodulation,[status(thm)],[f60892,f30891]) ).
fof(f61226,plain,
! [X0] : X0 = inverse(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f60892,f61016]) ).
fof(f61356,plain,
! [X0,X1] : multiply(X0,multiply(inverse(X0),X1)) = inverse(inverse(X1)),
inference(backward_demodulation,[status(thm)],[f61226,f30989]) ).
fof(f61361,plain,
multiply(inverse(a3),sF1_fnc) = b3,
inference(backward_demodulation,[status(thm)],[f61226,f29766]) ).
fof(f61363,plain,
multiply(inverse(b3),sF3_fnc) = c3,
inference(backward_demodulation,[status(thm)],[f61226,f29757]) ).
fof(f61391,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(X0,X1))),c3),inverse(sF0_fnc))),
inference(backward_demodulation,[status(thm)],[f61226,f40]) ).
fof(f61392,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(X0,X1))),b3),inverse(sF1_fnc))),
inference(backward_demodulation,[status(thm)],[f61226,f38]) ).
fof(f61441,plain,
! [X0,X1] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(forward_demodulation,[status(thm)],[f61226,f61356]) ).
fof(f61655,plain,
! [X0,X1,X2] : X0 = inverse(multiply(X1,inverse(multiply(X0,multiply(inverse(inverse(multiply(X2,inverse(X2)))),X1))))),
inference(paramodulation,[status(thm)],[f61441,f50508]) ).
fof(f61715,plain,
! [X0,X1,X2] : X0 = inverse(multiply(X1,inverse(multiply(X0,multiply(multiply(X2,inverse(X2)),X1))))),
inference(forward_demodulation,[status(thm)],[f61226,f61655]) ).
fof(f61716,plain,
! [X0,X1] : X0 = inverse(multiply(X1,inverse(multiply(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f60892,f61715]) ).
fof(f62326,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(multiply(inverse(X2),X3),X1))),c3),inverse(sF0_fnc)))))))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X3)),b3),inverse(sF1_fnc)))),
inference(backward_demodulation,[status(thm)],[f61391,f10508]) ).
fof(f62328,plain,
! [X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(X0,multiply(inverse(X0),X1)))),c3),inverse(sF0_fnc))) = X1,
inference(backward_demodulation,[status(thm)],[f61391,f15]) ).
fof(f62388,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(multiply(inverse(X2),X3),X1))),c3),inverse(sF0_fnc)))))))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(X0,X3))),c3),inverse(sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f61391,f62326]) ).
fof(f62389,plain,
! [X0] : inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X0)),c3),inverse(sF0_fnc))) = X0,
inference(forward_demodulation,[status(thm)],[f61441,f62328]) ).
fof(f62453,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc)))) = multiply(X0,X1),
inference(backward_demodulation,[status(thm)],[f62389,f61391]) ).
fof(f64533,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),X3),X1)))))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(X0,X3))),c3),inverse(sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f62389,f62388]) ).
fof(f64534,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),X3),X1)))))) = multiply(X0,X3),
inference(forward_demodulation,[status(thm)],[f62389,f64533]) ).
fof(f64763,plain,
! [X0,X1] : X0 = inverse(multiply(inverse(multiply(X1,X0)),X1)),
inference(paramodulation,[status(thm)],[f61716,f61716]) ).
fof(f65147,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc)))) = multiply(X0,X1),
inference(backward_demodulation,[status(thm)],[f65148,f61392]) ).
fof(f65148,plain,
! [X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(a3),multiply(X0,X1))),b3),inverse(sF1_fnc))) = multiply(X0,X1),
inference(forward_demodulation,[status(thm)],[f61392,f62453]) ).
fof(f66488,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a3),inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),multiply(inverse(inverse(inverse(X0))),X3)),inverse(multiply(multiply(inverse(multiply(inverse(b3),X1)),c3),inverse(sF3_fnc)))))))))),b3),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),X3)),X5),inverse(multiply(X4,X5)))),
inference(forward_demodulation,[status(thm)],[f40008,f397]) ).
fof(f66489,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),multiply(inverse(inverse(inverse(X0))),X3)),inverse(multiply(multiply(inverse(multiply(inverse(b3),X1)),c3),inverse(sF3_fnc))))))))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),X3)),X5),inverse(multiply(X4,X5)))),
inference(forward_demodulation,[status(thm)],[f65147,f66488]) ).
fof(f66490,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),multiply(inverse(X0),X3)),inverse(multiply(multiply(inverse(multiply(inverse(b3),X1)),c3),inverse(sF3_fnc))))))))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),X3)),X5),inverse(multiply(X4,X5)))),
inference(forward_demodulation,[status(thm)],[f61226,f66489]) ).
fof(f66491,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),multiply(inverse(X0),X3)),inverse(multiply(multiply(inverse(multiply(inverse(a3),X1)),b3),inverse(sF1_fnc))))))))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),X3)),X5),inverse(multiply(X4,X5)))),
inference(forward_demodulation,[status(thm)],[f40008,f66490]) ).
fof(f66492,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),multiply(inverse(X0),X3)),X1)))))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),X3)),X5),inverse(multiply(X4,X5)))),
inference(forward_demodulation,[status(thm)],[f65147,f66491]) ).
fof(f66493,plain,
! [X0,X1,X2,X3] : multiply(X0,multiply(inverse(X0),X1)) = inverse(multiply(multiply(inverse(multiply(inverse(X2),X1)),X3),inverse(multiply(X2,X3)))),
inference(forward_demodulation,[status(thm)],[f64534,f66492]) ).
fof(f66494,plain,
! [X0,X1,X2] : X0 = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X2),inverse(multiply(X1,X2)))),
inference(forward_demodulation,[status(thm)],[f61441,f66493]) ).
fof(f66499,plain,
! [X0] : X0 = inverse(multiply(multiply(inverse(multiply(inverse(a3),X0)),sF3_fnc),inverse(sF2_fnc))),
inference(backward_demodulation,[status(thm)],[f66500,f40010]) ).
fof(f66500,plain,
! [X0] : X0 = inverse(multiply(multiply(inverse(multiply(inverse(a3),X0)),b3),inverse(sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f8434,f66494]) ).
fof(f67041,plain,
sF1_fnc = inverse(multiply(multiply(inverse(b3),sF3_fnc),inverse(sF2_fnc))),
inference(paramodulation,[status(thm)],[f61361,f66499]) ).
fof(f67122,plain,
sF1_fnc = inverse(multiply(c3,inverse(sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f61363,f67041]) ).
fof(f68196,plain,
inverse(sF2_fnc) = inverse(multiply(sF1_fnc,c3)),
inference(paramodulation,[status(thm)],[f67122,f64763]) ).
fof(f68242,plain,
inverse(sF2_fnc) = inverse(sF0_fnc),
inference(forward_demodulation,[status(thm)],[f6,f68196]) ).
fof(f68286,plain,
sF2_fnc = inverse(inverse(sF0_fnc)),
inference(paramodulation,[status(thm)],[f68242,f61226]) ).
fof(f68301,plain,
sF2_fnc = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f61226,f68286]) ).
fof(f68302,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f68301,f9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP429-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n026.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:15:36 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 43.23/5.90 % Refutation found
% 43.23/5.90 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 43.23/5.90 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 24.94/7.14 % Elapsed time: 6.552756 seconds
% 24.94/7.14 % CPU time: 35.973585 seconds
% 24.94/7.14 % Total memory used: 562.920 MB
% 24.94/7.14 % Net memory used: 554.547 MB
%------------------------------------------------------------------------------