%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP469-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 : n020.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:17 PM UTC 2026
% Result : Unsatisfiable 113.07s 14.67s
% Output : CNFRefutation 106.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 66
% Number of leaves : 7
% Syntax : Number of formulae : 206 ( 206 unt; 4 def)
% Number of atoms : 206 ( 205 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 301 ( 301 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C,D] : divide(inverse(divide(A,divide(B,divide(C,D)))),divide(divide(D,C),A)) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] : multiply(A,B) = divide(A,inverse(B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,negated_conjecture,
multiply(inverse(a1),a1) != multiply(inverse(b1),b1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,plain,
! [X0,X1,X2,X3] : divide(inverse(divide(X0,divide(X1,divide(X2,X3)))),divide(divide(X3,X2),X0)) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f5,plain,
! [X0,X1] : multiply(X0,X1) = divide(X0,inverse(X1)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f6,plain,
multiply(inverse(a1),a1) != multiply(inverse(b1),b1),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f7,definition,
sF1_fnc = inverse(a1),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f8,definition,
sF0_fnc = multiply(sF1_fnc,a1),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f9,definition,
sF3_fnc = inverse(b1),
introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition]) ).
fof(f10,definition,
sF2_fnc = multiply(sF3_fnc,b1),
introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).
fof(f11,plain,
sF0_fnc != sF2_fnc,
inference(definition_folding,[],[f6,f10,f9,f8,f7]) ).
fof(f12,plain,
! [X0] : multiply(X0,b1) = divide(X0,sF3_fnc),
inference(paramodulation,[status(thm)],[f9,f5]) ).
fof(f13,plain,
! [X0] : multiply(X0,a1) = divide(X0,sF1_fnc),
inference(paramodulation,[status(thm)],[f7,f5]) ).
fof(f14,plain,
! [X0,X1,X2,X3,X4] : divide(inverse(X0),divide(divide(X1,X2),inverse(divide(divide(X2,X1),divide(X0,divide(X3,X4)))))) = divide(X4,X3),
inference(paramodulation,[status(thm)],[f4,f4]) ).
fof(f15,plain,
! [X0,X1,X2,X3,X4] : divide(inverse(divide(X0,X1)),divide(divide(X2,divide(X3,X4)),X0)) = inverse(divide(X2,divide(X1,divide(X4,X3)))),
inference(paramodulation,[status(thm)],[f4,f4]) ).
fof(f18,plain,
! [X0,X1,X2,X3] : divide(inverse(divide(inverse(X0),divide(X1,divide(X2,X3)))),multiply(divide(X3,X2),X0)) = X1,
inference(paramodulation,[status(thm)],[f5,f4]) ).
fof(f21,plain,
! [X0,X1,X2,X3,X4] : divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,divide(X3,X4))))) = divide(X4,X3),
inference(forward_demodulation,[status(thm)],[f5,f14]) ).
fof(f24,plain,
sF2_fnc = divide(sF3_fnc,sF3_fnc),
inference(backward_demodulation,[status(thm)],[f12,f10]) ).
fof(f25,plain,
! [X0,X1] : divide(inverse(divide(X0,divide(X1,divide(sF3_fnc,sF3_fnc)))),divide(sF2_fnc,X0)) = X1,
inference(paramodulation,[status(thm)],[f24,f4]) ).
fof(f27,plain,
! [X0,X1] : divide(inverse(divide(X0,divide(X1,sF2_fnc))),divide(sF2_fnc,X0)) = X1,
inference(forward_demodulation,[status(thm)],[f24,f25]) ).
fof(f29,plain,
sF0_fnc = divide(sF1_fnc,sF1_fnc),
inference(backward_demodulation,[status(thm)],[f13,f8]) ).
fof(f30,plain,
! [X0,X1] : divide(inverse(divide(X0,divide(X1,divide(sF1_fnc,sF1_fnc)))),divide(sF0_fnc,X0)) = X1,
inference(paramodulation,[status(thm)],[f29,f4]) ).
fof(f32,plain,
! [X0,X1] : divide(inverse(divide(X0,divide(X1,sF0_fnc))),divide(sF0_fnc,X0)) = X1,
inference(forward_demodulation,[status(thm)],[f29,f30]) ).
fof(f34,plain,
! [X0] : divide(inverse(X0),divide(sF2_fnc,inverse(divide(sF2_fnc,divide(X0,sF2_fnc))))) = sF2_fnc,
inference(paramodulation,[status(thm)],[f27,f27]) ).
fof(f35,plain,
! [X0,X1,X2] : divide(inverse(X0),divide(sF2_fnc,inverse(divide(sF2_fnc,divide(X0,divide(X1,X2)))))) = divide(X2,X1),
inference(paramodulation,[status(thm)],[f4,f27]) ).
fof(f37,plain,
! [X0,X1,X2] : divide(inverse(X0),divide(divide(X1,X2),inverse(divide(divide(X2,X1),divide(X0,sF2_fnc))))) = sF2_fnc,
inference(paramodulation,[status(thm)],[f27,f4]) ).
fof(f41,plain,
! [X0] : divide(inverse(X0),multiply(sF2_fnc,divide(sF2_fnc,divide(X0,sF2_fnc)))) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f5,f34]) ).
fof(f42,plain,
! [X0,X1,X2] : divide(inverse(X0),multiply(sF2_fnc,divide(sF2_fnc,divide(X0,divide(X1,X2))))) = divide(X2,X1),
inference(forward_demodulation,[status(thm)],[f5,f35]) ).
fof(f43,plain,
! [X0,X1,X2] : divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,sF2_fnc)))) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f5,f37]) ).
fof(f46,plain,
! [X0] : divide(inverse(X0),divide(sF0_fnc,inverse(divide(sF0_fnc,divide(X0,sF0_fnc))))) = sF0_fnc,
inference(paramodulation,[status(thm)],[f32,f32]) ).
fof(f47,plain,
! [X0] : divide(inverse(X0),divide(sF0_fnc,inverse(divide(sF0_fnc,divide(X0,sF2_fnc))))) = sF2_fnc,
inference(paramodulation,[status(thm)],[f27,f32]) ).
fof(f48,plain,
! [X0,X1,X2] : divide(inverse(X0),divide(sF0_fnc,inverse(divide(sF0_fnc,divide(X0,divide(X1,X2)))))) = divide(X2,X1),
inference(paramodulation,[status(thm)],[f4,f32]) ).
fof(f51,plain,
! [X0,X1,X2] : divide(inverse(X0),divide(divide(X1,X2),inverse(divide(divide(X2,X1),divide(X0,sF0_fnc))))) = sF0_fnc,
inference(paramodulation,[status(thm)],[f32,f4]) ).
fof(f52,plain,
! [X0,X1,X2] : divide(inverse(divide(X0,X1)),divide(divide(X2,sF0_fnc),X0)) = inverse(divide(X2,divide(X1,sF0_fnc))),
inference(paramodulation,[status(thm)],[f32,f4]) ).
fof(f55,plain,
! [X0] : divide(inverse(X0),multiply(sF0_fnc,divide(sF0_fnc,divide(X0,sF0_fnc)))) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f5,f46]) ).
fof(f56,plain,
! [X0] : divide(inverse(X0),multiply(sF0_fnc,divide(sF0_fnc,divide(X0,sF2_fnc)))) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f5,f47]) ).
fof(f57,plain,
! [X0,X1,X2] : divide(inverse(X0),multiply(sF0_fnc,divide(sF0_fnc,divide(X0,divide(X1,X2))))) = divide(X2,X1),
inference(forward_demodulation,[status(thm)],[f5,f48]) ).
fof(f59,plain,
! [X0,X1,X2] : divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,sF0_fnc)))) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f5,f51]) ).
fof(f63,plain,
! [X0,X1,X2,X3] : divide(sF1_fnc,multiply(divide(X0,X1),divide(divide(X1,X0),divide(a1,divide(X2,X3))))) = divide(X3,X2),
inference(paramodulation,[status(thm)],[f7,f21]) ).
fof(f83,plain,
! [X0,X1,X2,X3,X4] : divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,X3)))) = divide(divide(sF0_fnc,X4),inverse(divide(X4,divide(X3,sF0_fnc)))),
inference(paramodulation,[status(thm)],[f32,f21]) ).
fof(f84,plain,
! [X0,X1,X2,X3,X4] : divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,X3)))) = divide(divide(sF2_fnc,X4),inverse(divide(X4,divide(X3,sF2_fnc)))),
inference(paramodulation,[status(thm)],[f27,f21]) ).
fof(f86,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,divide(X3,X4))))) = divide(multiply(divide(X5,X6),divide(divide(X6,X5),divide(X7,divide(X4,X3)))),inverse(X7)),
inference(paramodulation,[status(thm)],[f21,f21]) ).
fof(f87,plain,
! [X0,X1,X2,X3,X4] : divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,multiply(X3,X4))))) = divide(inverse(X4),X3),
inference(paramodulation,[status(thm)],[f5,f21]) ).
fof(f104,plain,
! [X0,X1,X2,X3,X4] : divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,X3)))) = multiply(divide(sF0_fnc,X4),divide(X4,divide(X3,sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f5,f83]) ).
fof(f105,plain,
! [X0,X1,X2,X3,X4] : divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,X3)))) = multiply(divide(sF2_fnc,X4),divide(X4,divide(X3,sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f5,f84]) ).
fof(f107,plain,
! [X0,X1,X2,X3,X4] : divide(X0,X1) = divide(multiply(divide(X2,X3),divide(divide(X3,X2),divide(X4,divide(X0,X1)))),inverse(X4)),
inference(forward_demodulation,[status(thm)],[f21,f86]) ).
fof(f108,plain,
! [X0,X1,X2,X3,X4] : divide(X0,X1) = multiply(multiply(divide(X2,X3),divide(divide(X3,X2),divide(X4,divide(X0,X1)))),X4),
inference(forward_demodulation,[status(thm)],[f5,f107]) ).
fof(f124,plain,
divide(sF1_fnc,multiply(sF0_fnc,divide(sF0_fnc,divide(a1,sF0_fnc)))) = sF0_fnc,
inference(paramodulation,[status(thm)],[f7,f55]) ).
fof(f145,plain,
! [X0,X1,X2,X3] : X0 = inverse(divide(X1,divide(divide(X0,divide(divide(X2,X3),X1)),divide(X3,X2)))),
inference(paramodulation,[status(thm)],[f4,f15]) ).
fof(f149,plain,
! [X0,X1,X2] : divide(inverse(sF2_fnc),divide(divide(X0,divide(X1,X2)),sF3_fnc)) = inverse(divide(X0,divide(sF3_fnc,divide(X2,X1)))),
inference(paramodulation,[status(thm)],[f24,f15]) ).
fof(f159,plain,
! [X0,X1,X2,X3] : divide(inverse(divide(X0,X1)),divide(X2,X0)) = inverse(divide(inverse(divide(X3,divide(X2,sF0_fnc))),divide(X1,divide(X3,sF0_fnc)))),
inference(paramodulation,[status(thm)],[f32,f15]) ).
fof(f507,plain,
! [X0,X1] : X0 = inverse(divide(X1,divide(divide(X0,divide(sF0_fnc,X1)),divide(sF1_fnc,sF1_fnc)))),
inference(paramodulation,[status(thm)],[f29,f145]) ).
fof(f512,plain,
! [X0,X1] : X0 = inverse(divide(X1,divide(divide(X0,divide(sF2_fnc,X1)),divide(sF3_fnc,sF3_fnc)))),
inference(paramodulation,[status(thm)],[f24,f145]) ).
fof(f525,plain,
! [X0,X1,X2,X3] : X0 = inverse(divide(X1,divide(divide(X0,divide(multiply(X2,X3),X1)),divide(inverse(X3),X2)))),
inference(paramodulation,[status(thm)],[f5,f145]) ).
fof(f560,plain,
! [X0,X1] : X0 = inverse(divide(X1,divide(divide(X0,divide(sF0_fnc,X1)),sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f29,f507]) ).
fof(f561,plain,
! [X0,X1] : X0 = inverse(divide(X1,divide(divide(X0,divide(sF2_fnc,X1)),sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f24,f512]) ).
fof(f589,plain,
! [X0,X1] : X0 = inverse(inverse(divide(X0,divide(X1,divide(inverse(divide(sF0_fnc,X1)),sF0_fnc))))),
inference(paramodulation,[status(thm)],[f15,f560]) ).
fof(f701,plain,
! [X0,X1] : X0 = inverse(inverse(divide(X0,divide(X1,divide(inverse(divide(sF2_fnc,X1)),sF2_fnc))))),
inference(paramodulation,[status(thm)],[f15,f561]) ).
fof(f716,plain,
! [X0,X1,X2] : multiply(X0,divide(X1,divide(divide(X2,divide(sF2_fnc,X1)),sF2_fnc))) = divide(X0,X2),
inference(paramodulation,[status(thm)],[f561,f5]) ).
fof(f1043,plain,
! [X0,X1] : divide(inverse(X0),multiply(sF2_fnc,divide(sF2_fnc,divide(X0,sF2_fnc)))) = divide(multiply(sF0_fnc,divide(sF0_fnc,divide(X1,sF2_fnc))),inverse(X1)),
inference(paramodulation,[status(thm)],[f56,f42]) ).
fof(f1045,plain,
! [X0,X1,X2,X3] : divide(inverse(X0),multiply(sF2_fnc,divide(sF2_fnc,divide(X0,divide(X1,X2))))) = divide(multiply(sF2_fnc,divide(sF2_fnc,divide(X3,divide(X2,X1)))),inverse(X3)),
inference(paramodulation,[status(thm)],[f42,f42]) ).
fof(f1088,plain,
! [X0] : sF2_fnc = divide(multiply(sF0_fnc,divide(sF0_fnc,divide(X0,sF2_fnc))),inverse(X0)),
inference(forward_demodulation,[status(thm)],[f41,f1043]) ).
fof(f1089,plain,
! [X0] : sF2_fnc = multiply(multiply(sF0_fnc,divide(sF0_fnc,divide(X0,sF2_fnc))),X0),
inference(forward_demodulation,[status(thm)],[f5,f1088]) ).
fof(f1092,plain,
! [X0,X1,X2] : divide(X0,X1) = divide(multiply(sF2_fnc,divide(sF2_fnc,divide(X2,divide(X0,X1)))),inverse(X2)),
inference(forward_demodulation,[status(thm)],[f42,f1045]) ).
fof(f1093,plain,
! [X0,X1,X2] : divide(X0,X1) = multiply(multiply(sF2_fnc,divide(sF2_fnc,divide(X2,divide(X0,X1)))),X2),
inference(forward_demodulation,[status(thm)],[f5,f1092]) ).
fof(f1119,plain,
! [X0] : sF2_fnc = multiply(divide(sF0_fnc,X0),divide(X0,divide(sF2_fnc,sF0_fnc))),
inference(paramodulation,[status(thm)],[f716,f1089]) ).
fof(f1738,plain,
! [X0,X1] : divide(sF3_fnc,multiply(divide(X0,X1),divide(divide(X1,X0),divide(b1,sF2_fnc)))) = sF2_fnc,
inference(paramodulation,[status(thm)],[f9,f43]) ).
fof(f1739,plain,
! [X0,X1] : divide(sF1_fnc,multiply(divide(X0,X1),divide(divide(X1,X0),divide(a1,sF2_fnc)))) = sF2_fnc,
inference(paramodulation,[status(thm)],[f7,f43]) ).
fof(f2706,plain,
! [X0,X1,X2,X3,X4] : divide(inverse(divide(inverse(X0),divide(X1,divide(X2,X3)))),multiply(divide(X3,X2),X0)) = multiply(multiply(sF2_fnc,divide(sF2_fnc,divide(X4,X1))),X4),
inference(paramodulation,[status(thm)],[f18,f1093]) ).
fof(f2754,plain,
! [X0,X1] : X0 = multiply(multiply(sF2_fnc,divide(sF2_fnc,divide(X1,X0))),X1),
inference(forward_demodulation,[status(thm)],[f18,f2706]) ).
fof(f2788,plain,
! [X0,X1] : divide(sF1_fnc,multiply(sF0_fnc,divide(sF0_fnc,divide(a1,divide(X0,X1))))) = divide(X1,X0),
inference(paramodulation,[status(thm)],[f7,f57]) ).
fof(f2832,plain,
! [X0,X1,X2,X3] : divide(inverse(X0),multiply(sF0_fnc,divide(sF0_fnc,divide(X0,divide(X1,X2))))) = divide(multiply(sF0_fnc,divide(sF0_fnc,divide(X3,divide(X2,X1)))),inverse(X3)),
inference(paramodulation,[status(thm)],[f57,f57]) ).
fof(f2905,plain,
! [X0,X1,X2] : divide(X0,X1) = divide(multiply(sF0_fnc,divide(sF0_fnc,divide(X2,divide(X0,X1)))),inverse(X2)),
inference(forward_demodulation,[status(thm)],[f57,f2832]) ).
fof(f2906,plain,
! [X0,X1,X2] : divide(X0,X1) = multiply(multiply(sF0_fnc,divide(sF0_fnc,divide(X2,divide(X0,X1)))),X2),
inference(forward_demodulation,[status(thm)],[f5,f2905]) ).
fof(f2950,plain,
! [X0] : X0 = divide(multiply(sF2_fnc,divide(sF2_fnc,divide(b1,X0))),sF3_fnc),
inference(paramodulation,[status(thm)],[f12,f2754]) ).
fof(f3010,plain,
! [X0,X1] : divide(sF1_fnc,multiply(divide(X0,X1),divide(divide(X1,X0),divide(a1,sF0_fnc)))) = sF0_fnc,
inference(paramodulation,[status(thm)],[f7,f59]) ).
fof(f3277,plain,
! [X0] : inverse(X0) = divide(multiply(sF2_fnc,divide(sF2_fnc,multiply(b1,X0))),sF3_fnc),
inference(paramodulation,[status(thm)],[f5,f2950]) ).
fof(f4119,plain,
! [X0,X1] : divide(multiply(sF2_fnc,divide(sF2_fnc,multiply(b1,X0))),sF3_fnc) = multiply(multiply(sF0_fnc,divide(sF0_fnc,divide(X1,inverse(X0)))),X1),
inference(paramodulation,[status(thm)],[f3277,f2906]) ).
fof(f4121,plain,
! [X0,X1] : divide(multiply(sF2_fnc,divide(sF2_fnc,divide(b1,X0))),sF3_fnc) = multiply(multiply(sF0_fnc,divide(sF0_fnc,divide(X1,X0))),X1),
inference(paramodulation,[status(thm)],[f2950,f2906]) ).
fof(f4174,plain,
! [X0,X1] : inverse(X0) = multiply(multiply(sF0_fnc,divide(sF0_fnc,divide(X1,inverse(X0)))),X1),
inference(forward_demodulation,[status(thm)],[f3277,f4119]) ).
fof(f4175,plain,
! [X0,X1] : inverse(X0) = multiply(multiply(sF0_fnc,divide(sF0_fnc,multiply(X1,X0))),X1),
inference(forward_demodulation,[status(thm)],[f5,f4174]) ).
fof(f4178,plain,
! [X0,X1] : X0 = multiply(multiply(sF0_fnc,divide(sF0_fnc,divide(X1,X0))),X1),
inference(forward_demodulation,[status(thm)],[f2950,f4121]) ).
fof(f4231,plain,
! [X0] : X0 = divide(multiply(sF0_fnc,divide(sF0_fnc,divide(a1,X0))),sF1_fnc),
inference(paramodulation,[status(thm)],[f13,f4178]) ).
fof(f4247,plain,
sF1_fnc = multiply(multiply(sF0_fnc,divide(sF0_fnc,sF0_fnc)),sF1_fnc),
inference(paramodulation,[status(thm)],[f29,f4178]) ).
fof(f4252,plain,
sF3_fnc = multiply(multiply(sF0_fnc,divide(sF0_fnc,sF2_fnc)),sF3_fnc),
inference(paramodulation,[status(thm)],[f24,f4178]) ).
fof(f10983,plain,
! [X0,X1] : multiply(divide(X0,X1),divide(divide(X1,X0),divide(b1,sF2_fnc))) = multiply(multiply(sF0_fnc,divide(sF0_fnc,sF2_fnc)),sF3_fnc),
inference(paramodulation,[status(thm)],[f1738,f4178]) ).
fof(f11129,plain,
! [X0,X1] : multiply(divide(X0,X1),divide(divide(X1,X0),divide(b1,sF2_fnc))) = sF3_fnc,
inference(forward_demodulation,[status(thm)],[f4252,f10983]) ).
fof(f11146,plain,
multiply(sF0_fnc,divide(divide(multiply(sF0_fnc,divide(sF0_fnc,divide(a1,sF0_fnc))),sF1_fnc),divide(b1,sF2_fnc))) = sF3_fnc,
inference(paramodulation,[status(thm)],[f124,f11129]) ).
fof(f11262,plain,
multiply(sF0_fnc,divide(sF0_fnc,divide(b1,sF2_fnc))) = sF3_fnc,
inference(forward_demodulation,[status(thm)],[f4231,f11146]) ).
fof(f14384,plain,
! [X0,X1,X2,X3] : divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,X3)))) = multiply(divide(sF0_fnc,a1),divide(a1,divide(X3,sF0_fnc))),
inference(equality_split,[status(thm)],[f104]) ).
fof(f15348,plain,
! [X0,X1] : multiply(divide(sF0_fnc,a1),divide(a1,divide(X0,sF0_fnc))) = multiply(divide(sF2_fnc,X1),divide(X1,divide(X0,sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f14384,f105]) ).
fof(f16743,plain,
! [X0,X1] : multiply(divide(X0,X1),divide(divide(X1,X0),divide(a1,sF0_fnc))) = multiply(multiply(sF0_fnc,divide(sF0_fnc,sF0_fnc)),sF1_fnc),
inference(paramodulation,[status(thm)],[f3010,f4178]) ).
fof(f16898,plain,
! [X0,X1] : multiply(divide(X0,X1),divide(divide(X1,X0),divide(a1,sF0_fnc))) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f4247,f16743]) ).
fof(f16919,plain,
multiply(sF0_fnc,divide(divide(multiply(sF0_fnc,divide(sF0_fnc,divide(a1,sF0_fnc))),sF1_fnc),divide(a1,sF0_fnc))) = sF1_fnc,
inference(paramodulation,[status(thm)],[f124,f16898]) ).
fof(f17041,plain,
multiply(sF0_fnc,divide(sF0_fnc,divide(a1,sF0_fnc))) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f4231,f16919]) ).
fof(f17313,plain,
! [X0,X1,X2,X3] : divide(multiply(sF2_fnc,divide(sF2_fnc,multiply(b1,X0))),sF3_fnc) = multiply(multiply(divide(X1,X2),divide(divide(X2,X1),divide(X3,inverse(X0)))),X3),
inference(paramodulation,[status(thm)],[f3277,f108]) ).
fof(f17315,plain,
! [X0,X1,X2,X3] : divide(multiply(sF2_fnc,divide(sF2_fnc,divide(b1,X0))),sF3_fnc) = multiply(multiply(divide(X1,X2),divide(divide(X2,X1),divide(X3,X0))),X3),
inference(paramodulation,[status(thm)],[f2950,f108]) ).
fof(f17504,plain,
! [X0,X1,X2,X3] : inverse(X0) = multiply(multiply(divide(X1,X2),divide(divide(X2,X1),divide(X3,inverse(X0)))),X3),
inference(forward_demodulation,[status(thm)],[f3277,f17313]) ).
fof(f17505,plain,
! [X0,X1,X2,X3] : inverse(X0) = multiply(multiply(divide(X1,X2),divide(divide(X2,X1),multiply(X3,X0))),X3),
inference(forward_demodulation,[status(thm)],[f5,f17504]) ).
fof(f17508,plain,
! [X0,X1,X2,X3] : X0 = multiply(multiply(divide(X1,X2),divide(divide(X2,X1),divide(X3,X0))),X3),
inference(forward_demodulation,[status(thm)],[f2950,f17315]) ).
fof(f17600,plain,
! [X0,X1] : multiply(divide(sF0_fnc,a1),divide(a1,divide(multiply(X0,X1),sF0_fnc))) = divide(inverse(X1),X0),
inference(forward_demodulation,[status(thm)],[f14384,f87]) ).
fof(f18037,plain,
! [X0,X1,X2] : X0 = divide(multiply(divide(X1,X2),divide(divide(X2,X1),divide(a1,X0))),sF1_fnc),
inference(paramodulation,[status(thm)],[f13,f17508]) ).
fof(f18165,plain,
! [X0,X1] : sF1_fnc = multiply(multiply(divide(X0,X1),divide(divide(X1,X0),sF0_fnc)),sF1_fnc),
inference(paramodulation,[status(thm)],[f29,f17508]) ).
fof(f25256,plain,
! [X0,X1,X2] : divide(inverse(divide(X0,X1)),divide(X2,X0)) = divide(inverse(divide(a1,X1)),divide(X2,a1)),
inference(equality_split,[status(thm)],[f159]) ).
fof(f25648,plain,
! [X0,X1,X2] : divide(sF1_fnc,multiply(sF0_fnc,divide(sF0_fnc,divide(a1,divide(inverse(divide(a1,X0)),divide(X1,a1)))))) = divide(divide(X1,X2),inverse(divide(X2,X0))),
inference(paramodulation,[status(thm)],[f25256,f2788]) ).
fof(f25928,plain,
! [X0,X1,X2] : divide(divide(X0,a1),inverse(divide(a1,X1))) = divide(divide(X0,X2),inverse(divide(X2,X1))),
inference(forward_demodulation,[status(thm)],[f2788,f25648]) ).
fof(f25929,plain,
! [X0,X1,X2] : multiply(divide(X0,a1),divide(a1,X1)) = divide(divide(X0,X2),inverse(divide(X2,X1))),
inference(forward_demodulation,[status(thm)],[f5,f25928]) ).
fof(f25930,plain,
! [X0,X1,X2] : multiply(divide(X0,a1),divide(a1,X1)) = multiply(divide(X0,X2),divide(X2,X1)),
inference(forward_demodulation,[status(thm)],[f5,f25929]) ).
fof(f26116,plain,
! [X0] : multiply(divide(X0,a1),divide(a1,sF1_fnc)) = multiply(divide(X0,sF1_fnc),sF0_fnc),
inference(paramodulation,[status(thm)],[f29,f25930]) ).
fof(f28762,plain,
! [X0,X1] : multiply(divide(X0,X1),divide(X1,sF1_fnc)) = multiply(divide(X0,sF1_fnc),sF0_fnc),
inference(paramodulation,[status(thm)],[f25930,f26116]) ).
fof(f28813,plain,
! [X0,X1] : multiply(sF2_fnc,divide(multiply(divide(X0,X1),divide(divide(X1,X0),divide(a1,sF2_fnc))),sF1_fnc)) = multiply(divide(sF1_fnc,sF1_fnc),sF0_fnc),
inference(paramodulation,[status(thm)],[f1739,f28762]) ).
fof(f28814,plain,
! [X0,X1,X2,X3] : multiply(divide(X0,X1),divide(multiply(divide(X2,X3),divide(divide(X3,X2),divide(a1,divide(X1,X0)))),sF1_fnc)) = multiply(divide(sF1_fnc,sF1_fnc),sF0_fnc),
inference(paramodulation,[status(thm)],[f63,f28762]) ).
fof(f28912,plain,
multiply(sF2_fnc,sF2_fnc) = multiply(divide(sF1_fnc,sF1_fnc),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f18037,f28813]) ).
fof(f28913,plain,
multiply(sF2_fnc,sF2_fnc) = multiply(sF0_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f29,f28912]) ).
fof(f28914,plain,
! [X0,X1] : multiply(divide(X0,X1),divide(X1,X0)) = multiply(divide(sF1_fnc,sF1_fnc),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f18037,f28814]) ).
fof(f28915,plain,
! [X0,X1] : multiply(divide(X0,X1),divide(X1,X0)) = multiply(sF0_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f29,f28914]) ).
fof(f28971,plain,
multiply(divide(sF0_fnc,a1),divide(a1,divide(multiply(sF0_fnc,sF0_fnc),sF0_fnc))) = divide(inverse(sF2_fnc),sF2_fnc),
inference(paramodulation,[status(thm)],[f28913,f17600]) ).
fof(f28978,plain,
inverse(sF2_fnc) = multiply(multiply(sF0_fnc,divide(sF0_fnc,multiply(sF0_fnc,sF0_fnc))),sF2_fnc),
inference(paramodulation,[status(thm)],[f28913,f4175]) ).
fof(f28982,plain,
divide(inverse(sF0_fnc),sF0_fnc) = divide(inverse(sF2_fnc),sF2_fnc),
inference(forward_demodulation,[status(thm)],[f17600,f28971]) ).
fof(f29508,plain,
! [X0,X1] : multiply(divide(sF0_fnc,a1),divide(a1,divide(multiply(sF0_fnc,sF0_fnc),sF0_fnc))) = divide(inverse(divide(X0,X1)),divide(X1,X0)),
inference(paramodulation,[status(thm)],[f28915,f17600]) ).
fof(f29659,plain,
! [X0,X1] : divide(inverse(sF0_fnc),sF0_fnc) = divide(inverse(divide(X0,X1)),divide(X1,X0)),
inference(forward_demodulation,[status(thm)],[f17600,f29508]) ).
fof(f29660,plain,
! [X0] : divide(inverse(sF0_fnc),sF0_fnc) = divide(inverse(divide(a1,X0)),divide(X0,a1)),
inference(forward_demodulation,[status(thm)],[f25256,f29659]) ).
fof(f32473,plain,
! [X0] : divide(inverse(sF0_fnc),sF0_fnc) = inverse(divide(X0,divide(divide(X0,sF0_fnc),sF0_fnc))),
inference(paramodulation,[status(thm)],[f52,f29660]) ).
fof(f33055,plain,
! [X0] : divide(divide(inverse(sF0_fnc),sF0_fnc),divide(sF0_fnc,X0)) = divide(X0,sF0_fnc),
inference(paramodulation,[status(thm)],[f32473,f32]) ).
fof(f33844,plain,
! [X0] : divide(sF1_fnc,multiply(sF0_fnc,divide(sF0_fnc,divide(a1,divide(X0,sF0_fnc))))) = divide(divide(sF0_fnc,X0),divide(inverse(sF0_fnc),sF0_fnc)),
inference(paramodulation,[status(thm)],[f33055,f2788]) ).
fof(f33934,plain,
! [X0] : divide(sF0_fnc,X0) = divide(divide(sF0_fnc,X0),divide(inverse(sF0_fnc),sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f2788,f33844]) ).
fof(f34561,plain,
! [X0] : divide(sF0_fnc,inverse(X0)) = divide(multiply(sF0_fnc,X0),divide(inverse(sF0_fnc),sF0_fnc)),
inference(paramodulation,[status(thm)],[f5,f33934]) ).
fof(f34565,plain,
! [X0] : sF0_fnc = inverse(divide(X0,divide(sF0_fnc,divide(multiply(sF0_fnc,sF0_fnc),X0)))),
inference(paramodulation,[status(thm)],[f33934,f525]) ).
fof(f34728,plain,
! [X0] : multiply(sF0_fnc,X0) = divide(multiply(sF0_fnc,X0),divide(inverse(sF0_fnc),sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f5,f34561]) ).
fof(f35780,plain,
multiply(sF0_fnc,divide(sF0_fnc,divide(a1,sF0_fnc))) = divide(sF1_fnc,divide(inverse(sF0_fnc),sF0_fnc)),
inference(paramodulation,[status(thm)],[f17041,f34728]) ).
fof(f35781,plain,
multiply(sF0_fnc,divide(sF0_fnc,divide(b1,sF2_fnc))) = divide(sF3_fnc,divide(inverse(sF0_fnc),sF0_fnc)),
inference(paramodulation,[status(thm)],[f11262,f34728]) ).
fof(f35942,plain,
sF1_fnc = divide(sF1_fnc,divide(inverse(sF0_fnc),sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f17041,f35780]) ).
fof(f35943,plain,
sF3_fnc = divide(sF3_fnc,divide(inverse(sF0_fnc),sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f11262,f35781]) ).
fof(f39657,plain,
sF0_fnc = inverse(divide(divide(multiply(sF0_fnc,sF0_fnc),divide(inverse(sF0_fnc),sF0_fnc)),sF0_fnc)),
inference(paramodulation,[status(thm)],[f33055,f34565]) ).
fof(f39666,plain,
! [X0] : divide(sF0_fnc,multiply(divide(inverse(X0),multiply(sF0_fnc,sF0_fnc)),X0)) = sF0_fnc,
inference(paramodulation,[status(thm)],[f34565,f18]) ).
fof(f39742,plain,
sF0_fnc = inverse(divide(multiply(sF0_fnc,sF0_fnc),sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f34728,f39657]) ).
fof(f39813,plain,
! [X0] : multiply(X0,divide(multiply(sF0_fnc,sF0_fnc),sF0_fnc)) = divide(X0,sF0_fnc),
inference(paramodulation,[status(thm)],[f39742,f5]) ).
fof(f41738,plain,
divide(sF0_fnc,multiply(divide(sF0_fnc,multiply(sF0_fnc,sF0_fnc)),divide(multiply(sF0_fnc,sF0_fnc),sF0_fnc))) = sF0_fnc,
inference(paramodulation,[status(thm)],[f39742,f39666]) ).
fof(f41904,plain,
divide(sF0_fnc,multiply(sF0_fnc,sF0_fnc)) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f28915,f41738]) ).
fof(f43057,plain,
inverse(sF2_fnc) = multiply(multiply(sF0_fnc,sF0_fnc),sF2_fnc),
inference(backward_demodulation,[status(thm)],[f41904,f28978]) ).
fof(f43068,plain,
! [X0] : X0 = inverse(inverse(divide(X0,divide(multiply(sF0_fnc,sF0_fnc),divide(inverse(sF0_fnc),sF0_fnc))))),
inference(paramodulation,[status(thm)],[f41904,f589]) ).
fof(f43098,plain,
multiply(sF0_fnc,divide(multiply(sF0_fnc,sF0_fnc),sF0_fnc)) = multiply(sF0_fnc,sF0_fnc),
inference(paramodulation,[status(thm)],[f41904,f28915]) ).
fof(f43145,plain,
divide(sF1_fnc,multiply(sF0_fnc,divide(sF0_fnc,divide(a1,sF0_fnc)))) = divide(multiply(sF0_fnc,sF0_fnc),sF0_fnc),
inference(paramodulation,[status(thm)],[f41904,f2788]) ).
fof(f43201,plain,
! [X0] : X0 = inverse(inverse(divide(X0,multiply(sF0_fnc,sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f34728,f43068]) ).
fof(f43205,plain,
divide(sF0_fnc,sF0_fnc) = multiply(sF0_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f39813,f43098]) ).
fof(f43208,plain,
divide(sF1_fnc,sF1_fnc) = divide(multiply(sF0_fnc,sF0_fnc),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f17041,f43145]) ).
fof(f43209,plain,
sF0_fnc = divide(multiply(sF0_fnc,sF0_fnc),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f29,f43208]) ).
fof(f43226,plain,
divide(sF0_fnc,divide(sF0_fnc,sF0_fnc)) = sF0_fnc,
inference(backward_demodulation,[status(thm)],[f43205,f41904]) ).
fof(f43244,plain,
multiply(sF2_fnc,sF2_fnc) = divide(sF0_fnc,sF0_fnc),
inference(backward_demodulation,[status(thm)],[f43205,f28913]) ).
fof(f43265,plain,
! [X0,X1] : inverse(sF0_fnc) = multiply(multiply(divide(X0,X1),divide(divide(X1,X0),divide(sF0_fnc,sF0_fnc))),sF0_fnc),
inference(paramodulation,[status(thm)],[f43205,f17505]) ).
fof(f43284,plain,
inverse(sF0_fnc) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f17508,f43265]) ).
fof(f43294,plain,
sF3_fnc = divide(sF3_fnc,divide(sF0_fnc,sF0_fnc)),
inference(backward_demodulation,[status(thm)],[f43284,f35943]) ).
fof(f43295,plain,
sF1_fnc = divide(sF1_fnc,divide(sF0_fnc,sF0_fnc)),
inference(backward_demodulation,[status(thm)],[f43284,f35942]) ).
fof(f43302,plain,
divide(sF0_fnc,sF0_fnc) = divide(inverse(sF2_fnc),sF2_fnc),
inference(backward_demodulation,[status(thm)],[f43284,f28982]) ).
fof(f43361,plain,
! [X0] : multiply(X0,sF0_fnc) = divide(X0,sF0_fnc),
inference(paramodulation,[status(thm)],[f43284,f5]) ).
fof(f44313,plain,
sF0_fnc = divide(divide(sF0_fnc,sF0_fnc),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f43361,f43209]) ).
fof(f44315,plain,
sF1_fnc = multiply(multiply(divide(sF0_fnc,sF0_fnc),sF0_fnc),sF1_fnc),
inference(paramodulation,[status(thm)],[f44313,f18165]) ).
fof(f44458,plain,
sF1_fnc = multiply(divide(divide(sF0_fnc,sF0_fnc),sF0_fnc),sF1_fnc),
inference(forward_demodulation,[status(thm)],[f43361,f44315]) ).
fof(f44459,plain,
sF1_fnc = multiply(sF0_fnc,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f44313,f44458]) ).
fof(f45418,plain,
divide(inverse(sF2_fnc),divide(sF3_fnc,sF3_fnc)) = inverse(divide(sF3_fnc,divide(sF3_fnc,divide(sF0_fnc,sF0_fnc)))),
inference(paramodulation,[status(thm)],[f43294,f149]) ).
fof(f45572,plain,
divide(inverse(sF2_fnc),sF2_fnc) = inverse(divide(sF3_fnc,divide(sF3_fnc,divide(sF0_fnc,sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f24,f45418]) ).
fof(f45573,plain,
divide(inverse(sF2_fnc),sF2_fnc) = inverse(divide(sF3_fnc,sF3_fnc)),
inference(forward_demodulation,[status(thm)],[f43294,f45572]) ).
fof(f45574,plain,
divide(inverse(sF2_fnc),sF2_fnc) = inverse(sF2_fnc),
inference(forward_demodulation,[status(thm)],[f24,f45573]) ).
fof(f47630,plain,
inverse(sF2_fnc) = multiply(divide(sF0_fnc,sF0_fnc),sF2_fnc),
inference(forward_demodulation,[status(thm)],[f43361,f43057]) ).
fof(f47675,plain,
! [X0] : X0 = inverse(inverse(divide(X0,divide(sF0_fnc,sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f43361,f43201]) ).
fof(f49386,plain,
! [X0] : X0 = inverse(inverse(divide(X0,inverse(sF2_fnc)))),
inference(backward_demodulation,[status(thm)],[f49396,f47675]) ).
fof(f49387,plain,
inverse(sF2_fnc) = multiply(inverse(sF2_fnc),sF2_fnc),
inference(backward_demodulation,[status(thm)],[f49396,f47630]) ).
fof(f49388,plain,
divide(sF0_fnc,inverse(sF2_fnc)) = sF0_fnc,
inference(backward_demodulation,[status(thm)],[f49396,f43226]) ).
fof(f49389,plain,
sF1_fnc = divide(sF1_fnc,inverse(sF2_fnc)),
inference(backward_demodulation,[status(thm)],[f49396,f43295]) ).
fof(f49391,plain,
multiply(sF2_fnc,sF2_fnc) = inverse(sF2_fnc),
inference(backward_demodulation,[status(thm)],[f49396,f43244]) ).
fof(f49396,plain,
divide(sF0_fnc,sF0_fnc) = inverse(sF2_fnc),
inference(forward_demodulation,[status(thm)],[f45574,f43302]) ).
fof(f49548,plain,
! [X0] : X0 = inverse(inverse(multiply(X0,sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f5,f49386]) ).
fof(f49549,plain,
multiply(sF0_fnc,sF2_fnc) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f5,f49388]) ).
fof(f49550,plain,
sF1_fnc = multiply(sF1_fnc,sF2_fnc),
inference(forward_demodulation,[status(thm)],[f5,f49389]) ).
fof(f50817,plain,
inverse(sF2_fnc) = inverse(inverse(inverse(sF2_fnc))),
inference(paramodulation,[status(thm)],[f49387,f49548]) ).
fof(f50821,plain,
sF2_fnc = inverse(inverse(inverse(sF2_fnc))),
inference(paramodulation,[status(thm)],[f49391,f49548]) ).
fof(f50954,plain,
divide(sF0_fnc,sF0_fnc) = sF2_fnc,
inference(backward_demodulation,[status(thm)],[f50957,f49396]) ).
fof(f50955,plain,
divide(inverse(sF2_fnc),sF2_fnc) = sF2_fnc,
inference(backward_demodulation,[status(thm)],[f50957,f45574]) ).
fof(f50957,plain,
inverse(sF2_fnc) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f50821,f50817]) ).
fof(f51014,plain,
! [X0] : multiply(X0,sF2_fnc) = divide(X0,sF2_fnc),
inference(paramodulation,[status(thm)],[f50957,f5]) ).
fof(f51017,plain,
divide(sF2_fnc,sF2_fnc) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f50957,f50955]) ).
fof(f51104,plain,
sF1_fnc = divide(sF1_fnc,sF2_fnc),
inference(backward_demodulation,[status(thm)],[f51014,f49550]) ).
fof(f51105,plain,
divide(sF0_fnc,sF2_fnc) = sF0_fnc,
inference(backward_demodulation,[status(thm)],[f51014,f49549]) ).
fof(f52006,plain,
! [X0] : multiply(divide(sF0_fnc,a1),divide(a1,divide(sF2_fnc,sF0_fnc))) = multiply(divide(sF2_fnc,X0),divide(X0,sF2_fnc)),
inference(paramodulation,[status(thm)],[f51017,f15348]) ).
fof(f52146,plain,
! [X0] : sF2_fnc = multiply(divide(sF2_fnc,X0),divide(X0,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f1119,f52006]) ).
fof(f53587,plain,
divide(sF1_fnc,multiply(sF0_fnc,divide(sF0_fnc,divide(a1,sF0_fnc)))) = divide(sF2_fnc,sF0_fnc),
inference(paramodulation,[status(thm)],[f51105,f2788]) ).
fof(f53677,plain,
divide(sF1_fnc,sF1_fnc) = divide(sF2_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f17041,f53587]) ).
fof(f53678,plain,
sF0_fnc = divide(sF2_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f29,f53677]) ).
fof(f59671,plain,
sF2_fnc = multiply(divide(sF2_fnc,sF1_fnc),sF1_fnc),
inference(paramodulation,[status(thm)],[f51104,f52146]) ).
fof(f59774,plain,
inverse(sF1_fnc) = multiply(multiply(sF0_fnc,divide(sF0_fnc,sF2_fnc)),divide(sF2_fnc,sF1_fnc)),
inference(paramodulation,[status(thm)],[f59671,f4175]) ).
fof(f59793,plain,
inverse(sF1_fnc) = multiply(multiply(sF0_fnc,sF0_fnc),divide(sF2_fnc,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f51105,f59774]) ).
fof(f59794,plain,
inverse(sF1_fnc) = multiply(divide(sF0_fnc,sF0_fnc),divide(sF2_fnc,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f43361,f59793]) ).
fof(f59795,plain,
inverse(sF1_fnc) = multiply(sF2_fnc,divide(sF2_fnc,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f50954,f59794]) ).
fof(f59970,plain,
inverse(divide(sF2_fnc,sF1_fnc)) = multiply(multiply(sF0_fnc,divide(sF0_fnc,inverse(sF1_fnc))),sF2_fnc),
inference(paramodulation,[status(thm)],[f59795,f4175]) ).
fof(f59995,plain,
inverse(divide(sF2_fnc,sF1_fnc)) = divide(multiply(sF0_fnc,divide(sF0_fnc,inverse(sF1_fnc))),sF2_fnc),
inference(forward_demodulation,[status(thm)],[f51014,f59970]) ).
fof(f59996,plain,
inverse(divide(sF2_fnc,sF1_fnc)) = divide(multiply(sF0_fnc,multiply(sF0_fnc,sF1_fnc)),sF2_fnc),
inference(forward_demodulation,[status(thm)],[f5,f59995]) ).
fof(f59997,plain,
inverse(divide(sF2_fnc,sF1_fnc)) = divide(multiply(sF0_fnc,sF1_fnc),sF2_fnc),
inference(forward_demodulation,[status(thm)],[f44459,f59996]) ).
fof(f59998,plain,
inverse(divide(sF2_fnc,sF1_fnc)) = divide(sF1_fnc,sF2_fnc),
inference(forward_demodulation,[status(thm)],[f44459,f59997]) ).
fof(f59999,plain,
inverse(divide(sF2_fnc,sF1_fnc)) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f51104,f59998]) ).
fof(f60006,plain,
! [X0] : X0 = inverse(inverse(divide(X0,divide(sF1_fnc,divide(sF1_fnc,sF2_fnc))))),
inference(paramodulation,[status(thm)],[f59999,f701]) ).
fof(f60068,plain,
! [X0] : X0 = inverse(inverse(divide(X0,divide(sF1_fnc,sF1_fnc)))),
inference(forward_demodulation,[status(thm)],[f51104,f60006]) ).
fof(f60069,plain,
! [X0] : X0 = inverse(inverse(divide(X0,sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f29,f60068]) ).
fof(f60086,plain,
sF2_fnc = inverse(inverse(sF0_fnc)),
inference(paramodulation,[status(thm)],[f53678,f60069]) ).
fof(f60147,plain,
sF2_fnc = inverse(sF0_fnc),
inference(forward_demodulation,[status(thm)],[f43284,f60086]) ).
fof(f60148,plain,
sF2_fnc = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f43284,f60147]) ).
fof(f60149,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f60148,f11]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP469-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n020.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sun Sep 20 20:15:03 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.35 % Drodi V4.1.1
% 113.07/14.67 % Refutation found
% 113.07/14.67 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 113.07/14.67 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 43.08/14.88 % Elapsed time: 14.514691 seconds
% 43.08/14.88 % CPU time: 114.685742 seconds
% 43.08/14.88 % Total memory used: 1.132 GB
% 43.08/14.88 % Net memory used: 1.104 GB
%------------------------------------------------------------------------------