%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : BOO014-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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 10.22s 1.75s
% Output : CNFRefutation 10.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 16
% Syntax : Number of formulae : 159 ( 159 unt; 1 def)
% Number of atoms : 159 ( 158 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 136 ( 136 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] : add(X,Y) = add(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] : multiply(X,Y) = multiply(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y,Z] : add(multiply(X,Y),Z) = multiply(add(X,Z),add(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y,Z] : add(X,multiply(Y,Z)) = multiply(add(X,Y),add(X,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y,Z] : multiply(add(X,Y),Z) = add(multiply(X,Z),multiply(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y,Z] : multiply(X,add(Y,Z)) = add(multiply(X,Y),multiply(X,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X] : add(X,inverse(X)) = multiplicative_identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X] : multiply(X,inverse(X)) = additive_identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X] : multiply(X,multiplicative_identity) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X] : multiply(multiplicative_identity,X) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X] : add(X,additive_identity) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X] : add(additive_identity,X) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,hypothesis,
add(a,b) = c,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,hypothesis,
multiply(inverse(a),inverse(b)) = d,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,negated_conjecture,
inverse(c) != d,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,plain,
! [X0,X1] : add(X0,X1) = add(X1,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f19,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,X0),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f20,plain,
! [X0,X1,X2] : add(multiply(X0,X1),X2) = multiply(add(X0,X2),add(X1,X2)),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f21,plain,
! [X0,X1,X2] : add(X0,multiply(X1,X2)) = multiply(add(X0,X1),add(X0,X2)),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f22,plain,
! [X0,X1,X2] : multiply(add(X0,X1),X2) = add(multiply(X0,X2),multiply(X1,X2)),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f23,plain,
! [X0,X1,X2] : multiply(X0,add(X1,X2)) = add(multiply(X0,X1),multiply(X0,X2)),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f24,plain,
! [X0] : add(X0,inverse(X0)) = multiplicative_identity,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f26,plain,
! [X0] : multiply(X0,inverse(X0)) = additive_identity,
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f28,plain,
! [X0] : multiply(X0,multiplicative_identity) = X0,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f29,plain,
! [X0] : multiply(multiplicative_identity,X0) = X0,
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f30,plain,
! [X0] : add(X0,additive_identity) = X0,
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f31,plain,
! [X0] : add(additive_identity,X0) = X0,
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f32,plain,
add(a,b) = c,
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f33,plain,
multiply(inverse(a),inverse(b)) = d,
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f34,plain,
inverse(c) != d,
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f35,definition,
sF0_fnc = inverse(c),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f36,plain,
sF0_fnc != d,
inference(definition_folding,[],[f34,f35]) ).
fof(f56,plain,
multiply(c,sF0_fnc) = additive_identity,
inference(paramodulation,[status(thm)],[f35,f26]) ).
fof(f61,plain,
add(c,sF0_fnc) = multiplicative_identity,
inference(paramodulation,[status(thm)],[f35,f24]) ).
fof(f79,plain,
! [X0] : add(multiply(c,X0),sF0_fnc) = multiply(multiplicative_identity,add(X0,sF0_fnc)),
inference(paramodulation,[status(thm)],[f61,f20]) ).
fof(f80,plain,
! [X0,X1] : add(multiply(additive_identity,X0),X1) = multiply(X1,add(X0,X1)),
inference(paramodulation,[status(thm)],[f31,f20]) ).
fof(f81,plain,
! [X0] : add(multiply(a,X0),b) = multiply(c,add(X0,b)),
inference(paramodulation,[status(thm)],[f32,f20]) ).
fof(f82,plain,
! [X0,X1] : add(multiply(X0,X1),inverse(X0)) = multiply(multiplicative_identity,add(X1,inverse(X0))),
inference(paramodulation,[status(thm)],[f24,f20]) ).
fof(f87,plain,
! [X0,X1] : add(multiply(X0,additive_identity),X1) = multiply(add(X0,X1),X1),
inference(paramodulation,[status(thm)],[f31,f20]) ).
fof(f89,plain,
! [X0,X1] : add(multiply(X0,X1),inverse(X1)) = multiply(add(X0,inverse(X1)),multiplicative_identity),
inference(paramodulation,[status(thm)],[f24,f20]) ).
fof(f95,plain,
! [X0] : add(sF0_fnc,multiply(c,X0)) = multiply(multiplicative_identity,add(X0,sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f18,f79]) ).
fof(f96,plain,
! [X0] : add(sF0_fnc,multiply(c,X0)) = add(X0,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f29,f95]) ).
fof(f97,plain,
! [X0] : add(b,multiply(a,X0)) = multiply(c,add(X0,b)),
inference(forward_demodulation,[status(thm)],[f18,f81]) ).
fof(f98,plain,
! [X0,X1] : add(inverse(X0),multiply(X0,X1)) = multiply(multiplicative_identity,add(X1,inverse(X0))),
inference(forward_demodulation,[status(thm)],[f18,f82]) ).
fof(f99,plain,
! [X0,X1] : add(inverse(X0),multiply(X0,X1)) = add(X1,inverse(X0)),
inference(forward_demodulation,[status(thm)],[f29,f98]) ).
fof(f103,plain,
! [X0,X1] : add(multiply(X0,additive_identity),X1) = multiply(X1,add(X0,X1)),
inference(forward_demodulation,[status(thm)],[f19,f87]) ).
fof(f106,plain,
! [X0,X1] : add(inverse(X0),multiply(X1,X0)) = multiply(add(X1,inverse(X0)),multiplicative_identity),
inference(forward_demodulation,[status(thm)],[f18,f89]) ).
fof(f107,plain,
! [X0,X1] : add(inverse(X0),multiply(X1,X0)) = add(X1,inverse(X0)),
inference(forward_demodulation,[status(thm)],[f28,f106]) ).
fof(f125,plain,
add(b,multiply(a,additive_identity)) = multiply(c,b),
inference(paramodulation,[status(thm)],[f31,f97]) ).
fof(f126,plain,
add(b,multiply(a,a)) = multiply(c,c),
inference(paramodulation,[status(thm)],[f32,f97]) ).
fof(f129,plain,
add(b,multiply(a,additive_identity)) = multiply(b,c),
inference(forward_demodulation,[status(thm)],[f19,f125]) ).
fof(f173,plain,
! [X0] : add(multiply(additive_identity,additive_identity),X0) = multiply(X0,X0),
inference(paramodulation,[status(thm)],[f31,f80]) ).
fof(f250,plain,
! [X0] : add(X0,multiply(additive_identity,additive_identity)) = multiply(X0,X0),
inference(paramodulation,[status(thm)],[f18,f173]) ).
fof(f302,plain,
add(multiply(additive_identity,b),multiply(a,a)) = multiply(multiply(a,a),multiply(c,c)),
inference(paramodulation,[status(thm)],[f126,f80]) ).
fof(f305,plain,
add(multiply(a,a),multiply(additive_identity,b)) = multiply(multiply(a,a),multiply(c,c)),
inference(forward_demodulation,[status(thm)],[f18,f302]) ).
fof(f306,plain,
add(multiply(a,a),multiply(b,additive_identity)) = multiply(multiply(a,a),multiply(c,c)),
inference(forward_demodulation,[status(thm)],[f19,f305]) ).
fof(f634,plain,
! [X0,X1,X2] : add(X0,multiply(X1,X2)) = multiply(add(X0,X2),add(X0,X1)),
inference(paramodulation,[status(thm)],[f19,f21]) ).
fof(f679,plain,
! [X0] : add(a,multiply(X0,b)) = multiply(add(a,X0),c),
inference(paramodulation,[status(thm)],[f32,f21]) ).
fof(f683,plain,
! [X0,X1] : add(X0,multiply(X1,additive_identity)) = multiply(add(X0,X1),X0),
inference(paramodulation,[status(thm)],[f30,f21]) ).
fof(f741,plain,
! [X0] : add(a,multiply(X0,b)) = multiply(c,add(a,X0)),
inference(forward_demodulation,[status(thm)],[f19,f679]) ).
fof(f744,plain,
! [X0,X1] : add(X0,multiply(X1,additive_identity)) = multiply(X0,add(X0,X1)),
inference(forward_demodulation,[status(thm)],[f19,f683]) ).
fof(f753,plain,
! [X0] : multiply(add(c,X0),sF0_fnc) = add(additive_identity,multiply(X0,sF0_fnc)),
inference(paramodulation,[status(thm)],[f56,f22]) ).
fof(f761,plain,
! [X0,X1] : multiply(add(X0,X1),X0) = add(add(multiply(additive_identity,additive_identity),X0),multiply(X1,X0)),
inference(paramodulation,[status(thm)],[f173,f22]) ).
fof(f768,plain,
! [X0] : multiply(add(X0,c),sF0_fnc) = add(multiply(X0,sF0_fnc),additive_identity),
inference(paramodulation,[status(thm)],[f56,f22]) ).
fof(f770,plain,
! [X0] : multiply(add(X0,inverse(a)),inverse(b)) = add(multiply(X0,inverse(b)),d),
inference(paramodulation,[status(thm)],[f33,f22]) ).
fof(f788,plain,
! [X0] : multiply(sF0_fnc,add(c,X0)) = add(additive_identity,multiply(X0,sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f19,f753]) ).
fof(f789,plain,
! [X0] : multiply(sF0_fnc,add(c,X0)) = multiply(X0,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f31,f788]) ).
fof(f801,plain,
! [X0,X1] : multiply(X0,add(X0,X1)) = add(add(multiply(additive_identity,additive_identity),X0),multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f19,f761]) ).
fof(f802,plain,
! [X0,X1] : add(X0,multiply(X1,additive_identity)) = add(add(multiply(additive_identity,additive_identity),X0),multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f744,f801]) ).
fof(f805,plain,
! [X0] : multiply(sF0_fnc,add(X0,c)) = add(multiply(X0,sF0_fnc),additive_identity),
inference(forward_demodulation,[status(thm)],[f19,f768]) ).
fof(f806,plain,
! [X0] : multiply(sF0_fnc,add(X0,c)) = multiply(X0,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f30,f805]) ).
fof(f808,plain,
! [X0] : multiply(inverse(b),add(X0,inverse(a))) = add(multiply(X0,inverse(b)),d),
inference(forward_demodulation,[status(thm)],[f19,f770]) ).
fof(f809,plain,
! [X0] : multiply(inverse(b),add(X0,inverse(a))) = add(d,multiply(X0,inverse(b))),
inference(forward_demodulation,[status(thm)],[f18,f808]) ).
fof(f842,plain,
! [X0,X1] : multiply(X0,add(X0,X1)) = add(add(X0,multiply(additive_identity,additive_identity)),multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f250,f23]) ).
fof(f850,plain,
! [X0] : multiply(c,add(X0,sF0_fnc)) = add(multiply(c,X0),additive_identity),
inference(paramodulation,[status(thm)],[f56,f23]) ).
fof(f855,plain,
! [X0,X1] : multiply(X0,add(X1,inverse(X0))) = add(multiply(X0,X1),additive_identity),
inference(paramodulation,[status(thm)],[f26,f23]) ).
fof(f877,plain,
! [X0,X1] : add(X0,multiply(X1,additive_identity)) = add(add(X0,multiply(additive_identity,additive_identity)),multiply(X0,X1)),
inference(forward_demodulation,[status(thm)],[f744,f842]) ).
fof(f881,plain,
! [X0] : multiply(c,add(X0,sF0_fnc)) = multiply(c,X0),
inference(forward_demodulation,[status(thm)],[f30,f850]) ).
fof(f884,plain,
! [X0,X1] : multiply(X0,add(X1,inverse(X0))) = multiply(X0,X1),
inference(forward_demodulation,[status(thm)],[f30,f855]) ).
fof(f955,plain,
multiply(sF0_fnc,c) = multiply(additive_identity,sF0_fnc),
inference(paramodulation,[status(thm)],[f31,f806]) ).
fof(f965,plain,
multiply(c,sF0_fnc) = multiply(additive_identity,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f19,f955]) ).
fof(f968,plain,
additive_identity = multiply(additive_identity,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f56,f965]) ).
fof(f979,plain,
! [X0] : multiply(additive_identity,add(X0,sF0_fnc)) = add(multiply(additive_identity,X0),additive_identity),
inference(paramodulation,[status(thm)],[f968,f23]) ).
fof(f987,plain,
! [X0] : multiply(additive_identity,add(X0,sF0_fnc)) = multiply(additive_identity,X0),
inference(forward_demodulation,[status(thm)],[f30,f979]) ).
fof(f1134,plain,
multiply(c,multiplicative_identity) = multiply(c,c),
inference(paramodulation,[status(thm)],[f61,f881]) ).
fof(f1152,plain,
add(multiply(a,a),multiply(b,additive_identity)) = multiply(multiply(a,a),c),
inference(backward_demodulation,[status(thm)],[f1153,f306]) ).
fof(f1153,plain,
c = multiply(c,c),
inference(forward_demodulation,[status(thm)],[f28,f1134]) ).
fof(f1174,plain,
add(multiply(a,a),multiply(b,additive_identity)) = multiply(c,multiply(a,a)),
inference(forward_demodulation,[status(thm)],[f19,f1152]) ).
fof(f1258,plain,
multiply(additive_identity,sF0_fnc) = multiply(additive_identity,additive_identity),
inference(paramodulation,[status(thm)],[f31,f987]) ).
fof(f1272,plain,
! [X0] : add(X0,additive_identity) = multiply(X0,X0),
inference(backward_demodulation,[status(thm)],[f1309,f250]) ).
fof(f1282,plain,
! [X0,X1] : add(X0,multiply(X1,additive_identity)) = add(add(X0,additive_identity),multiply(X0,X1)),
inference(backward_demodulation,[status(thm)],[f1309,f877]) ).
fof(f1285,plain,
! [X0,X1] : add(X0,multiply(X1,additive_identity)) = add(add(additive_identity,X0),multiply(X1,X0)),
inference(backward_demodulation,[status(thm)],[f1309,f802]) ).
fof(f1309,plain,
additive_identity = multiply(additive_identity,additive_identity),
inference(forward_demodulation,[status(thm)],[f968,f1258]) ).
fof(f1329,plain,
add(multiply(a,a),multiply(b,additive_identity)) = multiply(c,a),
inference(backward_demodulation,[status(thm)],[f1335,f1174]) ).
fof(f1335,plain,
! [X0] : X0 = multiply(X0,X0),
inference(forward_demodulation,[status(thm)],[f30,f1272]) ).
fof(f1351,plain,
! [X0,X1] : add(X0,multiply(X1,additive_identity)) = add(X0,multiply(X0,X1)),
inference(forward_demodulation,[status(thm)],[f30,f1282]) ).
fof(f1356,plain,
add(b,multiply(a,b)) = multiply(b,c),
inference(backward_demodulation,[status(thm)],[f1360,f129]) ).
fof(f1360,plain,
! [X0,X1] : add(X0,multiply(X1,additive_identity)) = add(X0,multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f31,f1285]) ).
fof(f1405,plain,
add(a,multiply(b,additive_identity)) = multiply(c,a),
inference(forward_demodulation,[status(thm)],[f1335,f1329]) ).
fof(f1406,plain,
add(a,multiply(b,a)) = multiply(c,a),
inference(forward_demodulation,[status(thm)],[f1360,f1405]) ).
fof(f1407,plain,
add(a,multiply(a,b)) = multiply(c,a),
inference(forward_demodulation,[status(thm)],[f19,f1406]) ).
fof(f1408,plain,
add(a,multiply(a,b)) = multiply(a,c),
inference(forward_demodulation,[status(thm)],[f19,f1407]) ).
fof(f1675,plain,
! [X0] : multiply(X0,inverse(X0)) = multiply(X0,additive_identity),
inference(paramodulation,[status(thm)],[f31,f884]) ).
fof(f1708,plain,
! [X0,X1] : add(additive_identity,X0) = multiply(X0,add(X1,X0)),
inference(backward_demodulation,[status(thm)],[f1742,f103]) ).
fof(f1717,plain,
! [X0,X1] : add(X0,additive_identity) = add(X0,multiply(X1,X0)),
inference(backward_demodulation,[status(thm)],[f1742,f1360]) ).
fof(f1719,plain,
! [X0,X1] : add(X0,additive_identity) = add(X0,multiply(X0,X1)),
inference(backward_demodulation,[status(thm)],[f1742,f1351]) ).
fof(f1731,plain,
! [X0,X1] : add(X0,additive_identity) = multiply(X0,add(X0,X1)),
inference(backward_demodulation,[status(thm)],[f1742,f744]) ).
fof(f1742,plain,
! [X0] : additive_identity = multiply(X0,additive_identity),
inference(forward_demodulation,[status(thm)],[f26,f1675]) ).
fof(f1776,plain,
! [X0,X1] : X0 = multiply(X0,add(X1,X0)),
inference(forward_demodulation,[status(thm)],[f31,f1708]) ).
fof(f1793,plain,
b = multiply(b,c),
inference(backward_demodulation,[status(thm)],[f1800,f1356]) ).
fof(f1800,plain,
! [X0,X1] : X0 = add(X0,multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f30,f1717]) ).
fof(f1802,plain,
a = multiply(a,c),
inference(backward_demodulation,[status(thm)],[f1808,f1408]) ).
fof(f1808,plain,
! [X0,X1] : X0 = add(X0,multiply(X0,X1)),
inference(forward_demodulation,[status(thm)],[f30,f1719]) ).
fof(f1828,plain,
! [X0,X1] : X0 = multiply(X0,add(X0,X1)),
inference(forward_demodulation,[status(thm)],[f30,f1731]) ).
fof(f2066,plain,
add(inverse(b),b) = add(c,inverse(b)),
inference(paramodulation,[status(thm)],[f1793,f99]) ).
fof(f2075,plain,
add(b,inverse(b)) = add(c,inverse(b)),
inference(forward_demodulation,[status(thm)],[f18,f2066]) ).
fof(f2076,plain,
multiplicative_identity = add(c,inverse(b)),
inference(forward_demodulation,[status(thm)],[f24,f2075]) ).
fof(f2124,plain,
c = add(c,a),
inference(paramodulation,[status(thm)],[f1802,f1800]) ).
fof(f2137,plain,
inverse(b) = add(inverse(b),d),
inference(paramodulation,[status(thm)],[f33,f1800]) ).
fof(f2157,plain,
c = add(a,c),
inference(forward_demodulation,[status(thm)],[f18,f2124]) ).
fof(f2163,plain,
inverse(b) = add(d,inverse(b)),
inference(forward_demodulation,[status(thm)],[f18,f2137]) ).
fof(f2264,plain,
multiply(sF0_fnc,c) = multiply(a,sF0_fnc),
inference(paramodulation,[status(thm)],[f2157,f806]) ).
fof(f2279,plain,
multiply(c,sF0_fnc) = multiply(a,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f19,f2264]) ).
fof(f2280,plain,
additive_identity = multiply(a,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f56,f2279]) ).
fof(f2296,plain,
add(inverse(a),additive_identity) = add(sF0_fnc,inverse(a)),
inference(paramodulation,[status(thm)],[f2280,f99]) ).
fof(f2308,plain,
inverse(a) = add(sF0_fnc,inverse(a)),
inference(forward_demodulation,[status(thm)],[f30,f2296]) ).
fof(f2345,plain,
inverse(a) = add(inverse(a),d),
inference(paramodulation,[status(thm)],[f33,f1808]) ).
fof(f2370,plain,
inverse(a) = add(d,inverse(a)),
inference(forward_demodulation,[status(thm)],[f18,f2345]) ).
fof(f3196,plain,
multiply(sF0_fnc,multiplicative_identity) = multiply(inverse(b),sF0_fnc),
inference(paramodulation,[status(thm)],[f2076,f789]) ).
fof(f3228,plain,
sF0_fnc = multiply(inverse(b),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f28,f3196]) ).
fof(f3229,plain,
sF0_fnc = multiply(sF0_fnc,inverse(b)),
inference(forward_demodulation,[status(thm)],[f19,f3228]) ).
fof(f6085,plain,
! [X0,X1,X2] : add(X0,multiply(X1,X2)) = add(X0,multiply(X2,X1)),
inference(paramodulation,[status(thm)],[f21,f634]) ).
fof(f7206,plain,
multiply(b,inverse(b)) = multiply(b,d),
inference(paramodulation,[status(thm)],[f2163,f884]) ).
fof(f7231,plain,
additive_identity = multiply(b,d),
inference(forward_demodulation,[status(thm)],[f26,f7206]) ).
fof(f7273,plain,
add(inverse(d),additive_identity) = add(b,inverse(d)),
inference(paramodulation,[status(thm)],[f7231,f107]) ).
fof(f7290,plain,
inverse(d) = add(b,inverse(d)),
inference(forward_demodulation,[status(thm)],[f30,f7273]) ).
fof(f7346,plain,
multiply(inverse(b),inverse(a)) = add(d,multiply(sF0_fnc,inverse(b))),
inference(paramodulation,[status(thm)],[f2308,f809]) ).
fof(f7372,plain,
multiply(inverse(a),inverse(b)) = add(d,multiply(sF0_fnc,inverse(b))),
inference(forward_demodulation,[status(thm)],[f19,f7346]) ).
fof(f7373,plain,
d = add(d,multiply(sF0_fnc,inverse(b))),
inference(forward_demodulation,[status(thm)],[f33,f7372]) ).
fof(f7374,plain,
d = add(d,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f3229,f7373]) ).
fof(f7883,plain,
sF0_fnc = multiply(sF0_fnc,d),
inference(paramodulation,[status(thm)],[f7374,f1776]) ).
fof(f7913,plain,
sF0_fnc = multiply(d,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f19,f7883]) ).
fof(f8485,plain,
multiply(a,inverse(a)) = multiply(a,d),
inference(paramodulation,[status(thm)],[f2370,f884]) ).
fof(f8513,plain,
additive_identity = multiply(a,d),
inference(forward_demodulation,[status(thm)],[f26,f8485]) ).
fof(f8559,plain,
add(inverse(d),additive_identity) = add(a,inverse(d)),
inference(paramodulation,[status(thm)],[f8513,f107]) ).
fof(f8579,plain,
inverse(d) = add(a,inverse(d)),
inference(forward_demodulation,[status(thm)],[f30,f8559]) ).
fof(f9364,plain,
b = multiply(b,inverse(d)),
inference(paramodulation,[status(thm)],[f7290,f1828]) ).
fof(f9447,plain,
add(a,multiply(inverse(d),b)) = multiply(c,inverse(d)),
inference(paramodulation,[status(thm)],[f8579,f741]) ).
fof(f9477,plain,
add(a,multiply(b,inverse(d))) = multiply(c,inverse(d)),
inference(forward_demodulation,[status(thm)],[f6085,f9447]) ).
fof(f9478,plain,
add(a,b) = multiply(c,inverse(d)),
inference(forward_demodulation,[status(thm)],[f9364,f9477]) ).
fof(f9479,plain,
c = multiply(c,inverse(d)),
inference(forward_demodulation,[status(thm)],[f32,f9478]) ).
fof(f9514,plain,
add(sF0_fnc,c) = add(inverse(d),sF0_fnc),
inference(paramodulation,[status(thm)],[f9479,f96]) ).
fof(f9532,plain,
add(c,sF0_fnc) = add(inverse(d),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f18,f9514]) ).
fof(f9533,plain,
multiplicative_identity = add(inverse(d),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f61,f9532]) ).
fof(f9534,plain,
multiplicative_identity = add(sF0_fnc,inverse(d)),
inference(forward_demodulation,[status(thm)],[f18,f9533]) ).
fof(f9596,plain,
multiply(d,multiplicative_identity) = multiply(d,sF0_fnc),
inference(paramodulation,[status(thm)],[f9534,f884]) ).
fof(f9623,plain,
sF0_fnc = d,
inference(backward_demodulation,[status(thm)],[f9624,f7913]) ).
fof(f9624,plain,
d = multiply(d,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f28,f9596]) ).
fof(f9666,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f9623,f36]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : BOO014-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n007.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 13:45:36 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 10.22/1.75 % Refutation found
% 10.22/1.75 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 10.22/1.75 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 10.22/1.79 % Elapsed time: 1.419012 seconds
% 10.22/1.79 % CPU time: 10.937957 seconds
% 10.22/1.79 % Total memory used: 131.678 MB
% 10.22/1.79 % Net memory used: 129.145 MB
%------------------------------------------------------------------------------