%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : BOO015-4 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/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:06:22 PM UTC 2026
% Result : Unsatisfiable 28.60s 4.45s
% Output : CNFRefutation 28.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 14
% Syntax : Number of formulae : 163 ( 163 unt; 5 def)
% Number of atoms : 163 ( 162 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 : 4 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 9 con; 0-2 aty)
% Number of variables : 177 ( 177 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] : add(X,Y) = add(Y,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] : multiply(X,Y) = multiply(Y,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y,Z] : add(X,multiply(Y,Z)) = multiply(add(X,Y),add(X,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y,Z] : multiply(X,add(Y,Z)) = add(multiply(X,Y),multiply(X,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X] : add(X,additive_identity) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X] : multiply(X,multiplicative_identity) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X] : add(X,inverse(X)) = multiplicative_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X] : multiply(X,inverse(X)) = additive_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,negated_conjecture,
inverse(multiply(a,b)) != add(inverse(a),inverse(b)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,plain,
! [X0,X1] : add(X0,X1) = add(X1,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f11,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,X0),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f12,plain,
! [X0,X1,X2] : add(X0,multiply(X1,X2)) = multiply(add(X0,X1),add(X0,X2)),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f13,plain,
! [X0,X1,X2] : multiply(X0,add(X1,X2)) = add(multiply(X0,X1),multiply(X0,X2)),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f14,plain,
! [X0] : add(X0,additive_identity) = X0,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f15,plain,
! [X0] : multiply(X0,multiplicative_identity) = X0,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f16,plain,
! [X0] : add(X0,inverse(X0)) = multiplicative_identity,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f17,plain,
! [X0] : multiply(X0,inverse(X0)) = additive_identity,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f18,plain,
inverse(multiply(a,b)) != add(inverse(a),inverse(b)),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f19,definition,
sF1_fnc = multiply(a,b),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f20,definition,
sF0_fnc = inverse(sF1_fnc),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f21,definition,
sF3_fnc = inverse(a),
introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition]) ).
fof(f22,definition,
sF4_fnc = inverse(b),
introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition]) ).
fof(f23,definition,
sF2_fnc = add(sF3_fnc,sF4_fnc),
introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).
fof(f24,plain,
sF0_fnc != sF2_fnc,
inference(definition_folding,[],[f18,f23,f22,f21,f20,f19]) ).
fof(f33,plain,
! [X0,X1,X2] : add(X0,multiply(X1,X2)) = multiply(add(X0,X2),add(X0,X1)),
inference(paramodulation,[status(thm)],[f11,f12]) ).
fof(f35,plain,
! [X0] : add(sF3_fnc,multiply(sF4_fnc,X0)) = multiply(sF2_fnc,add(sF3_fnc,X0)),
inference(paramodulation,[status(thm)],[f23,f12]) ).
fof(f36,plain,
! [X0,X1,X2] : add(X0,multiply(X1,X2)) = multiply(add(X1,X0),add(X0,X2)),
inference(paramodulation,[status(thm)],[f10,f12]) ).
fof(f39,plain,
! [X0,X1,X2] : add(X0,multiply(X1,X2)) = multiply(add(X0,X1),add(X2,X0)),
inference(paramodulation,[status(thm)],[f10,f12]) ).
fof(f43,plain,
! [X0,X1,X2] : add(X0,multiply(X1,X2)) = add(X0,multiply(X2,X1)),
inference(forward_demodulation,[status(thm)],[f12,f33]) ).
fof(f49,plain,
! [X0,X1,X2] : add(multiply(X0,X1),X2) = add(X2,multiply(X1,X0)),
inference(paramodulation,[status(thm)],[f10,f43]) ).
fof(f82,plain,
! [X0] : add(sF1_fnc,X0) = add(X0,multiply(b,a)),
inference(paramodulation,[status(thm)],[f19,f49]) ).
fof(f115,plain,
! [X0,X1,X2,X3] : multiply(add(X0,X1),add(add(X0,X2),X3)) = add(add(X0,multiply(X1,X2)),multiply(add(X0,X1),X3)),
inference(paramodulation,[status(thm)],[f12,f13]) ).
fof(f116,plain,
! [X0] : multiply(a,add(b,X0)) = add(sF1_fnc,multiply(a,X0)),
inference(paramodulation,[status(thm)],[f19,f13]) ).
fof(f119,plain,
! [X0,X1,X2,X3] : multiply(add(X0,X1),add(X2,add(X0,X3))) = add(multiply(add(X0,X1),X2),add(X0,multiply(X1,X3))),
inference(paramodulation,[status(thm)],[f12,f13]) ).
fof(f121,plain,
! [X0,X1,X2] : multiply(X0,add(X1,X2)) = add(multiply(X0,X1),multiply(X2,X0)),
inference(paramodulation,[status(thm)],[f11,f13]) ).
fof(f138,plain,
! [X0] : add(sF3_fnc,multiply(sF4_fnc,X0)) = multiply(sF2_fnc,add(X0,sF3_fnc)),
inference(paramodulation,[status(thm)],[f10,f35]) ).
fof(f147,plain,
! [X0] : add(additive_identity,X0) = X0,
inference(paramodulation,[status(thm)],[f10,f14]) ).
fof(f151,plain,
! [X0,X1] : add(X0,multiply(X1,additive_identity)) = multiply(add(X0,X1),X0),
inference(paramodulation,[status(thm)],[f14,f12]) ).
fof(f155,plain,
! [X0] : multiply(multiplicative_identity,X0) = X0,
inference(paramodulation,[status(thm)],[f11,f15]) ).
fof(f200,plain,
add(b,sF4_fnc) = multiplicative_identity,
inference(paramodulation,[status(thm)],[f22,f16]) ).
fof(f201,plain,
add(a,sF3_fnc) = multiplicative_identity,
inference(paramodulation,[status(thm)],[f21,f16]) ).
fof(f205,plain,
! [X0,X1] : add(X0,multiply(X1,inverse(X0))) = multiply(add(X0,X1),multiplicative_identity),
inference(paramodulation,[status(thm)],[f16,f12]) ).
fof(f208,plain,
! [X0,X1] : add(X0,multiply(X1,inverse(X0))) = add(X0,X1),
inference(forward_demodulation,[status(thm)],[f15,f205]) ).
fof(f215,plain,
multiply(sF1_fnc,sF0_fnc) = additive_identity,
inference(paramodulation,[status(thm)],[f20,f17]) ).
fof(f217,plain,
! [X0,X1] : multiply(X0,add(X1,inverse(X0))) = add(multiply(X0,X1),additive_identity),
inference(paramodulation,[status(thm)],[f17,f13]) ).
fof(f218,plain,
! [X0,X1] : multiply(X0,add(inverse(X0),X1)) = add(additive_identity,multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f17,f13]) ).
fof(f219,plain,
! [X0,X1] : add(multiply(inverse(X0),X0),X1) = add(X1,additive_identity),
inference(paramodulation,[status(thm)],[f17,f49]) ).
fof(f221,plain,
! [X0,X1] : multiply(X0,add(X1,inverse(X0))) = multiply(X0,X1),
inference(forward_demodulation,[status(thm)],[f14,f217]) ).
fof(f222,plain,
! [X0,X1] : multiply(X0,add(inverse(X0),X1)) = multiply(X0,X1),
inference(forward_demodulation,[status(thm)],[f147,f218]) ).
fof(f223,plain,
! [X0,X1] : add(multiply(inverse(X0),X0),X1) = X1,
inference(forward_demodulation,[status(thm)],[f14,f219]) ).
fof(f227,plain,
! [X0] : add(b,multiply(X0,sF4_fnc)) = multiply(add(b,X0),multiplicative_identity),
inference(paramodulation,[status(thm)],[f200,f12]) ).
fof(f229,plain,
! [X0] : add(b,multiply(X0,sF4_fnc)) = add(b,X0),
inference(forward_demodulation,[status(thm)],[f15,f227]) ).
fof(f231,plain,
! [X0] : add(a,multiply(X0,sF3_fnc)) = multiply(add(a,X0),multiplicative_identity),
inference(paramodulation,[status(thm)],[f201,f12]) ).
fof(f233,plain,
! [X0] : add(a,multiply(X0,sF3_fnc)) = add(a,X0),
inference(forward_demodulation,[status(thm)],[f15,f231]) ).
fof(f243,plain,
! [X0] : add(sF4_fnc,multiply(sF3_fnc,X0)) = multiply(sF2_fnc,add(sF4_fnc,X0)),
inference(paramodulation,[status(thm)],[f23,f36]) ).
fof(f244,plain,
! [X0,X1] : add(inverse(X0),multiply(X0,X1)) = multiply(multiplicative_identity,add(inverse(X0),X1)),
inference(paramodulation,[status(thm)],[f16,f36]) ).
fof(f276,plain,
! [X0,X1] : add(inverse(X0),multiply(X0,X1)) = add(inverse(X0),X1),
inference(forward_demodulation,[status(thm)],[f155,f244]) ).
fof(f394,plain,
! [X0] : multiply(inverse(X0),X0) = additive_identity,
inference(paramodulation,[status(thm)],[f14,f223]) ).
fof(f686,plain,
! [X0,X1] : multiply(add(X0,sF1_fnc),add(add(X0,sF0_fnc),X1)) = add(add(X0,additive_identity),multiply(add(X0,sF1_fnc),X1)),
inference(paramodulation,[status(thm)],[f215,f115]) ).
fof(f696,plain,
! [X0,X1] : multiply(add(X0,a),add(add(X0,b),X1)) = add(add(X0,sF1_fnc),multiply(add(X0,a),X1)),
inference(paramodulation,[status(thm)],[f19,f115]) ).
fof(f749,plain,
! [X0,X1] : multiply(add(X0,sF1_fnc),add(add(X0,sF0_fnc),X1)) = add(X0,multiply(add(X0,sF1_fnc),X1)),
inference(forward_demodulation,[status(thm)],[f14,f686]) ).
fof(f883,plain,
! [X0] : add(X0,additive_identity) = add(X0,inverse(inverse(X0))),
inference(paramodulation,[status(thm)],[f394,f208]) ).
fof(f884,plain,
! [X0] : add(X0,inverse(X0)) = add(X0,multiplicative_identity),
inference(paramodulation,[status(thm)],[f155,f208]) ).
fof(f885,plain,
! [X0] : add(X0,additive_identity) = add(X0,X0),
inference(paramodulation,[status(thm)],[f17,f208]) ).
fof(f911,plain,
! [X0] : X0 = add(X0,inverse(inverse(X0))),
inference(forward_demodulation,[status(thm)],[f14,f883]) ).
fof(f912,plain,
! [X0] : multiplicative_identity = add(X0,multiplicative_identity),
inference(forward_demodulation,[status(thm)],[f16,f884]) ).
fof(f913,plain,
! [X0] : X0 = add(X0,X0),
inference(forward_demodulation,[status(thm)],[f14,f885]) ).
fof(f1058,plain,
! [X0] : multiplicative_identity = add(multiplicative_identity,X0),
inference(paramodulation,[status(thm)],[f10,f912]) ).
fof(f1060,plain,
multiply(a,multiplicative_identity) = add(sF1_fnc,multiply(a,multiplicative_identity)),
inference(paramodulation,[status(thm)],[f912,f116]) ).
fof(f1077,plain,
a = add(sF1_fnc,multiply(a,multiplicative_identity)),
inference(forward_demodulation,[status(thm)],[f15,f1060]) ).
fof(f1078,plain,
a = add(sF1_fnc,a),
inference(forward_demodulation,[status(thm)],[f15,f1077]) ).
fof(f1429,plain,
! [X0,X1] : multiply(X0,add(multiplicative_identity,X1)) = add(X0,multiply(X1,X0)),
inference(paramodulation,[status(thm)],[f15,f121]) ).
fof(f1438,plain,
! [X0,X1] : multiply(X0,add(X1,multiplicative_identity)) = add(multiply(X0,X1),X0),
inference(paramodulation,[status(thm)],[f155,f121]) ).
fof(f1492,plain,
! [X0,X1] : multiply(X0,multiplicative_identity) = add(X0,multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f1058,f1429]) ).
fof(f1493,plain,
! [X0,X1] : X0 = add(X0,multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f15,f1492]) ).
fof(f1500,plain,
! [X0,X1] : multiply(X0,multiplicative_identity) = add(multiply(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f912,f1438]) ).
fof(f1501,plain,
! [X0,X1] : X0 = add(multiply(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f15,f1500]) ).
fof(f1525,plain,
add(sF1_fnc,additive_identity) = multiply(b,a),
inference(paramodulation,[status(thm)],[f147,f82]) ).
fof(f1565,plain,
sF1_fnc = multiply(b,a),
inference(forward_demodulation,[status(thm)],[f14,f1525]) ).
fof(f1625,plain,
! [X0] : additive_identity = multiply(X0,additive_identity),
inference(paramodulation,[status(thm)],[f147,f1493]) ).
fof(f1628,plain,
! [X0,X1] : X0 = add(X0,multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f43,f1493]) ).
fof(f1795,plain,
b = add(sF1_fnc,b),
inference(paramodulation,[status(thm)],[f1565,f1501]) ).
fof(f1812,plain,
! [X0,X1] : X0 = add(multiply(X1,X0),X0),
inference(paramodulation,[status(thm)],[f11,f1501]) ).
fof(f1887,plain,
! [X0,X1,X2] : multiply(add(X0,X0),add(X1,add(X0,X2))) = add(multiply(add(X0,X0),X1),X0),
inference(paramodulation,[status(thm)],[f1628,f119]) ).
fof(f1900,plain,
! [X0,X1,X2] : multiply(X0,add(X1,add(X0,X2))) = add(multiply(add(X0,X0),X1),X0),
inference(forward_demodulation,[status(thm)],[f913,f1887]) ).
fof(f1901,plain,
! [X0,X1,X2] : multiply(X0,add(X1,add(X0,X2))) = add(multiply(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f913,f1900]) ).
fof(f1902,plain,
! [X0,X1,X2] : multiply(X0,add(X1,add(X0,X2))) = X0,
inference(forward_demodulation,[status(thm)],[f1501,f1901]) ).
fof(f2467,plain,
! [X0,X1] : multiply(X0,add(X0,X1)) = X0,
inference(paramodulation,[status(thm)],[f147,f1902]) ).
fof(f2500,plain,
! [X0,X1] : multiply(X0,add(X1,X0)) = X0,
inference(paramodulation,[status(thm)],[f911,f1902]) ).
fof(f2568,plain,
multiply(sF1_fnc,b) = sF1_fnc,
inference(paramodulation,[status(thm)],[f1795,f2467]) ).
fof(f2570,plain,
multiply(sF1_fnc,a) = sF1_fnc,
inference(paramodulation,[status(thm)],[f1078,f2467]) ).
fof(f2588,plain,
multiply(sF3_fnc,sF2_fnc) = sF3_fnc,
inference(paramodulation,[status(thm)],[f23,f2467]) ).
fof(f2590,plain,
! [X0] : multiply(X0,X0) = X0,
inference(paramodulation,[status(thm)],[f911,f2467]) ).
fof(f2705,plain,
! [X0,X1] : add(X0,additive_identity) = multiply(add(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f1625,f151]) ).
fof(f2706,plain,
! [X0,X1] : X0 = multiply(add(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f14,f2705]) ).
fof(f2748,plain,
! [X0,X1] : X0 = multiply(add(X1,X0),X0),
inference(paramodulation,[status(thm)],[f10,f2706]) ).
fof(f3037,plain,
multiply(sF4_fnc,sF2_fnc) = sF4_fnc,
inference(paramodulation,[status(thm)],[f23,f2500]) ).
fof(f3065,plain,
! [X0,X1] : add(X0,X1) = add(X1,add(X0,X1)),
inference(paramodulation,[status(thm)],[f2500,f1812]) ).
fof(f3070,plain,
! [X0,X1] : add(X0,X1) = add(add(X0,X1),X1),
inference(paramodulation,[status(thm)],[f2500,f1493]) ).
fof(f3270,plain,
! [X0,X1] : add(X0,inverse(X0)) = add(X0,add(X1,inverse(X0))),
inference(paramodulation,[status(thm)],[f2748,f208]) ).
fof(f3298,plain,
! [X0,X1] : multiplicative_identity = add(X0,add(X1,inverse(X0))),
inference(forward_demodulation,[status(thm)],[f16,f3270]) ).
fof(f3418,plain,
! [X0,X1] : multiply(X0,inverse(X0)) = multiply(X0,multiply(X1,inverse(X0))),
inference(paramodulation,[status(thm)],[f1812,f221]) ).
fof(f3470,plain,
! [X0,X1] : additive_identity = multiply(X0,multiply(X1,inverse(X0))),
inference(forward_demodulation,[status(thm)],[f17,f3418]) ).
fof(f3504,plain,
sF2_fnc = add(sF4_fnc,sF2_fnc),
inference(paramodulation,[status(thm)],[f3037,f1812]) ).
fof(f3627,plain,
! [X0] : multiply(X0,multiplicative_identity) = multiply(X0,inverse(inverse(X0))),
inference(paramodulation,[status(thm)],[f16,f222]) ).
fof(f3680,plain,
! [X0] : X0 = multiply(X0,inverse(inverse(X0))),
inference(forward_demodulation,[status(thm)],[f15,f3627]) ).
fof(f3964,plain,
! [X0] : add(sF2_fnc,multiply(sF4_fnc,X0)) = multiply(sF2_fnc,add(sF2_fnc,X0)),
inference(paramodulation,[status(thm)],[f3504,f36]) ).
fof(f3972,plain,
! [X0] : add(sF2_fnc,multiply(sF4_fnc,X0)) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f2467,f3964]) ).
fof(f4010,plain,
! [X0] : inverse(inverse(X0)) = add(X0,inverse(inverse(X0))),
inference(paramodulation,[status(thm)],[f3680,f1812]) ).
fof(f4030,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f911,f4010]) ).
fof(f4044,plain,
inverse(sF4_fnc) = b,
inference(paramodulation,[status(thm)],[f22,f4030]) ).
fof(f4045,plain,
inverse(sF3_fnc) = a,
inference(paramodulation,[status(thm)],[f21,f4030]) ).
fof(f7922,plain,
! [X0] : additive_identity = multiply(sF3_fnc,multiply(X0,a)),
inference(paramodulation,[status(thm)],[f4045,f3470]) ).
fof(f7923,plain,
! [X0] : additive_identity = multiply(sF4_fnc,multiply(X0,b)),
inference(paramodulation,[status(thm)],[f4044,f3470]) ).
fof(f7924,plain,
! [X0,X1] : additive_identity = multiply(inverse(X0),multiply(X1,X0)),
inference(paramodulation,[status(thm)],[f4030,f3470]) ).
fof(f9884,plain,
add(sF4_fnc,multiply(sF3_fnc,sF3_fnc)) = add(sF3_fnc,multiply(sF4_fnc,sF4_fnc)),
inference(paramodulation,[status(thm)],[f138,f243]) ).
fof(f9953,plain,
add(sF4_fnc,sF3_fnc) = add(sF3_fnc,multiply(sF4_fnc,sF4_fnc)),
inference(forward_demodulation,[status(thm)],[f2590,f9884]) ).
fof(f9954,plain,
add(sF4_fnc,sF3_fnc) = add(sF3_fnc,sF4_fnc),
inference(forward_demodulation,[status(thm)],[f2590,f9953]) ).
fof(f9955,plain,
add(sF4_fnc,sF3_fnc) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f23,f9954]) ).
fof(f17213,plain,
additive_identity = multiply(sF3_fnc,sF1_fnc),
inference(paramodulation,[status(thm)],[f2570,f7922]) ).
fof(f17305,plain,
additive_identity = multiply(sF1_fnc,sF3_fnc),
inference(paramodulation,[status(thm)],[f11,f17213]) ).
fof(f17415,plain,
add(inverse(sF1_fnc),additive_identity) = add(inverse(sF1_fnc),sF3_fnc),
inference(paramodulation,[status(thm)],[f17305,f276]) ).
fof(f17455,plain,
inverse(sF1_fnc) = add(inverse(sF1_fnc),sF3_fnc),
inference(forward_demodulation,[status(thm)],[f14,f17415]) ).
fof(f17456,plain,
sF0_fnc = add(inverse(sF1_fnc),sF3_fnc),
inference(forward_demodulation,[status(thm)],[f20,f17455]) ).
fof(f17457,plain,
sF0_fnc = add(sF0_fnc,sF3_fnc),
inference(forward_demodulation,[status(thm)],[f20,f17456]) ).
fof(f17509,plain,
multiply(sF3_fnc,sF0_fnc) = sF3_fnc,
inference(paramodulation,[status(thm)],[f17457,f2500]) ).
fof(f17728,plain,
additive_identity = multiply(sF4_fnc,sF1_fnc),
inference(paramodulation,[status(thm)],[f2568,f7923]) ).
fof(f17824,plain,
additive_identity = multiply(sF1_fnc,sF4_fnc),
inference(paramodulation,[status(thm)],[f11,f17728]) ).
fof(f17937,plain,
add(inverse(sF1_fnc),additive_identity) = add(inverse(sF1_fnc),sF4_fnc),
inference(paramodulation,[status(thm)],[f17824,f276]) ).
fof(f17977,plain,
inverse(sF1_fnc) = add(inverse(sF1_fnc),sF4_fnc),
inference(forward_demodulation,[status(thm)],[f14,f17937]) ).
fof(f17978,plain,
sF0_fnc = add(inverse(sF1_fnc),sF4_fnc),
inference(forward_demodulation,[status(thm)],[f20,f17977]) ).
fof(f17979,plain,
sF0_fnc = add(sF0_fnc,sF4_fnc),
inference(forward_demodulation,[status(thm)],[f20,f17978]) ).
fof(f18023,plain,
add(sF0_fnc,sF4_fnc) = add(sF4_fnc,sF0_fnc),
inference(paramodulation,[status(thm)],[f17979,f3065]) ).
fof(f18038,plain,
! [X0] : add(sF0_fnc,multiply(sF4_fnc,X0)) = multiply(sF0_fnc,add(X0,sF0_fnc)),
inference(paramodulation,[status(thm)],[f17979,f39]) ).
fof(f18047,plain,
sF0_fnc = add(sF4_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f17979,f18023]) ).
fof(f18056,plain,
! [X0] : add(sF0_fnc,multiply(sF4_fnc,X0)) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f2500,f18038]) ).
fof(f18063,plain,
add(sF4_fnc,multiply(sF3_fnc,sF0_fnc)) = multiply(sF2_fnc,sF0_fnc),
inference(paramodulation,[status(thm)],[f18047,f243]) ).
fof(f18103,plain,
add(sF4_fnc,sF3_fnc) = multiply(sF2_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f17509,f18063]) ).
fof(f18104,plain,
sF2_fnc = multiply(sF2_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f9955,f18103]) ).
fof(f18271,plain,
sF0_fnc = add(sF2_fnc,sF0_fnc),
inference(paramodulation,[status(thm)],[f18104,f1812]) ).
fof(f18651,plain,
additive_identity = multiply(inverse(sF2_fnc),sF3_fnc),
inference(paramodulation,[status(thm)],[f2588,f7924]) ).
fof(f18658,plain,
additive_identity = multiply(inverse(sF2_fnc),sF4_fnc),
inference(paramodulation,[status(thm)],[f3037,f7924]) ).
fof(f18901,plain,
add(a,additive_identity) = add(a,inverse(sF2_fnc)),
inference(paramodulation,[status(thm)],[f18651,f233]) ).
fof(f18946,plain,
a = add(a,inverse(sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f14,f18901]) ).
fof(f19003,plain,
add(b,additive_identity) = add(b,inverse(sF2_fnc)),
inference(paramodulation,[status(thm)],[f18658,f229]) ).
fof(f19047,plain,
b = add(b,inverse(sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f14,f19003]) ).
fof(f19497,plain,
multiplicative_identity = add(sF2_fnc,a),
inference(paramodulation,[status(thm)],[f18946,f3298]) ).
fof(f19726,plain,
multiplicative_identity = add(sF2_fnc,b),
inference(paramodulation,[status(thm)],[f19047,f3298]) ).
fof(f68975,plain,
! [X0] : multiply(multiplicative_identity,add(add(sF2_fnc,b),X0)) = add(add(sF2_fnc,sF1_fnc),multiply(add(sF2_fnc,a),X0)),
inference(paramodulation,[status(thm)],[f19497,f696]) ).
fof(f69186,plain,
! [X0] : add(add(sF2_fnc,b),X0) = add(add(sF2_fnc,sF1_fnc),multiply(add(sF2_fnc,a),X0)),
inference(forward_demodulation,[status(thm)],[f155,f68975]) ).
fof(f69187,plain,
! [X0] : add(multiplicative_identity,X0) = add(add(sF2_fnc,sF1_fnc),multiply(add(sF2_fnc,a),X0)),
inference(forward_demodulation,[status(thm)],[f19726,f69186]) ).
fof(f69188,plain,
! [X0] : multiplicative_identity = add(add(sF2_fnc,sF1_fnc),multiply(add(sF2_fnc,a),X0)),
inference(forward_demodulation,[status(thm)],[f1058,f69187]) ).
fof(f69189,plain,
! [X0] : multiplicative_identity = add(add(sF2_fnc,sF1_fnc),multiply(multiplicative_identity,X0)),
inference(forward_demodulation,[status(thm)],[f19497,f69188]) ).
fof(f69190,plain,
! [X0] : multiplicative_identity = add(add(sF2_fnc,sF1_fnc),X0),
inference(forward_demodulation,[status(thm)],[f155,f69189]) ).
fof(f85853,plain,
multiplicative_identity = add(sF2_fnc,sF1_fnc),
inference(paramodulation,[status(thm)],[f3070,f69190]) ).
fof(f86450,plain,
! [X0] : multiply(multiplicative_identity,add(add(sF2_fnc,sF0_fnc),X0)) = add(sF2_fnc,multiply(add(sF2_fnc,sF1_fnc),X0)),
inference(paramodulation,[status(thm)],[f85853,f749]) ).
fof(f86530,plain,
! [X0] : add(add(sF2_fnc,sF0_fnc),X0) = add(sF2_fnc,multiply(add(sF2_fnc,sF1_fnc),X0)),
inference(forward_demodulation,[status(thm)],[f155,f86450]) ).
fof(f86531,plain,
! [X0] : add(sF0_fnc,X0) = add(sF2_fnc,multiply(add(sF2_fnc,sF1_fnc),X0)),
inference(forward_demodulation,[status(thm)],[f18271,f86530]) ).
fof(f86532,plain,
! [X0] : add(sF0_fnc,X0) = add(sF2_fnc,multiply(multiplicative_identity,X0)),
inference(forward_demodulation,[status(thm)],[f85853,f86531]) ).
fof(f86533,plain,
! [X0] : add(sF0_fnc,X0) = add(sF2_fnc,X0),
inference(forward_demodulation,[status(thm)],[f155,f86532]) ).
fof(f87825,plain,
! [X0] : add(sF0_fnc,multiply(sF4_fnc,X0)) = sF2_fnc,
inference(backward_demodulation,[status(thm)],[f86533,f3972]) ).
fof(f88064,plain,
sF0_fnc = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f18056,f87825]) ).
fof(f88065,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f88064,f24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : BOO015-4 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n020.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 13:49:18 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.46 % Drodi V4.1.1
% 28.60/4.45 % Refutation found
% 28.60/4.45 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 28.60/4.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 26.55/5.72 % Elapsed time: 5.044468 seconds
% 26.55/5.72 % CPU time: 22.522749 seconds
% 26.55/5.72 % Total memory used: 152.228 MB
% 26.55/5.72 % Net memory used: 147.545 MB
%------------------------------------------------------------------------------