%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : BOO007-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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:18 PM UTC 2026
% Result : Unsatisfiable 1.54s 0.60s
% Output : CNFRefutation 1.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 14
% Syntax : Number of formulae : 96 ( 96 unt; 4 def)
% Number of atoms : 96 ( 95 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 ( 1 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 : 95 ( 95 !; 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(multiply(X,Y),Z) = multiply(add(X,Z),add(Y,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y,Z] : multiply(add(X,Y),Z) = add(multiply(X,Z),multiply(Y,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y,Z] : multiply(X,add(Y,Z)) = add(multiply(X,Y),multiply(X,Z)),
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] : add(inverse(X),X) = multiplicative_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X] : multiply(X,multiplicative_identity) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X] : add(additive_identity,X) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,negated_conjecture,
multiply(a,multiply(b,c)) != multiply(multiply(a,b),c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,plain,
! [X0,X1] : add(X0,X1) = add(X1,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f17,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,X0),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f18,plain,
! [X0,X1,X2] : add(multiply(X0,X1),X2) = multiply(add(X0,X2),add(X1,X2)),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f20,plain,
! [X0,X1,X2] : multiply(add(X0,X1),X2) = add(multiply(X0,X2),multiply(X1,X2)),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f21,plain,
! [X0,X1,X2] : multiply(X0,add(X1,X2)) = add(multiply(X0,X1),multiply(X0,X2)),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f22,plain,
! [X0] : add(X0,inverse(X0)) = multiplicative_identity,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f23,plain,
! [X0] : add(inverse(X0),X0) = multiplicative_identity,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f26,plain,
! [X0] : multiply(X0,multiplicative_identity) = X0,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f29,plain,
! [X0] : add(additive_identity,X0) = X0,
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f30,plain,
multiply(a,multiply(b,c)) != multiply(multiply(a,b),c),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f31,definition,
sF1_fnc = multiply(b,c),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f32,definition,
sF0_fnc = multiply(a,sF1_fnc),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f33,definition,
sF3_fnc = multiply(a,b),
introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition]) ).
fof(f34,definition,
sF2_fnc = multiply(sF3_fnc,c),
introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).
fof(f35,plain,
sF0_fnc != sF2_fnc,
inference(definition_folding,[],[f30,f34,f33,f32,f31]) ).
fof(f36,plain,
sF2_fnc = multiply(c,sF3_fnc),
inference(paramodulation,[status(thm)],[f34,f17]) ).
fof(f44,plain,
! [X0] : multiply(multiplicative_identity,X0) = X0,
inference(paramodulation,[status(thm)],[f17,f26]) ).
fof(f70,plain,
! [X0,X1] : add(multiply(additive_identity,X0),X1) = multiply(X1,add(X0,X1)),
inference(paramodulation,[status(thm)],[f29,f18]) ).
fof(f72,plain,
! [X0,X1,X2] : add(multiply(X0,X1),X2) = multiply(add(X2,X0),add(X1,X2)),
inference(paramodulation,[status(thm)],[f16,f18]) ).
fof(f144,plain,
! [X0,X1] : add(multiply(X0,inverse(X1)),X1) = multiply(add(X0,X1),multiplicative_identity),
inference(paramodulation,[status(thm)],[f23,f18]) ).
fof(f148,plain,
! [X0,X1] : add(multiply(X0,inverse(X1)),X1) = add(X0,X1),
inference(forward_demodulation,[status(thm)],[f26,f144]) ).
fof(f174,plain,
! [X0] : add(inverse(X0),X0) = add(multiplicative_identity,X0),
inference(paramodulation,[status(thm)],[f44,f148]) ).
fof(f190,plain,
! [X0] : multiplicative_identity = add(multiplicative_identity,X0),
inference(forward_demodulation,[status(thm)],[f23,f174]) ).
fof(f211,plain,
! [X0] : multiplicative_identity = add(X0,multiplicative_identity),
inference(paramodulation,[status(thm)],[f16,f190]) ).
fof(f338,plain,
! [X0,X1] : multiply(add(multiplicative_identity,X0),X1) = add(X1,multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f44,f20]) ).
fof(f339,plain,
! [X0] : multiply(add(c,X0),sF3_fnc) = add(sF2_fnc,multiply(X0,sF3_fnc)),
inference(paramodulation,[status(thm)],[f36,f20]) ).
fof(f340,plain,
! [X0] : multiply(add(sF3_fnc,X0),c) = add(sF2_fnc,multiply(X0,c)),
inference(paramodulation,[status(thm)],[f34,f20]) ).
fof(f351,plain,
! [X0,X1] : multiply(add(X0,multiplicative_identity),X1) = add(multiply(X0,X1),X1),
inference(paramodulation,[status(thm)],[f44,f20]) ).
fof(f355,plain,
! [X0] : multiply(add(X0,a),sF1_fnc) = add(multiply(X0,sF1_fnc),sF0_fnc),
inference(paramodulation,[status(thm)],[f32,f20]) ).
fof(f373,plain,
! [X0,X1] : multiply(multiplicative_identity,X0) = add(X0,multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f190,f338]) ).
fof(f374,plain,
! [X0,X1] : X0 = add(X0,multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f44,f373]) ).
fof(f378,plain,
! [X0,X1] : multiply(multiplicative_identity,X0) = add(multiply(X1,X0),X0),
inference(forward_demodulation,[status(thm)],[f211,f351]) ).
fof(f379,plain,
! [X0,X1] : X0 = add(multiply(X1,X0),X0),
inference(forward_demodulation,[status(thm)],[f44,f378]) ).
fof(f397,plain,
! [X0] : multiply(a,add(b,X0)) = add(sF3_fnc,multiply(a,X0)),
inference(paramodulation,[status(thm)],[f33,f21]) ).
fof(f401,plain,
! [X0,X1] : multiply(X0,add(multiplicative_identity,X1)) = add(X0,multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f26,f21]) ).
fof(f414,plain,
! [X0,X1] : multiply(X0,add(X1,multiplicative_identity)) = add(multiply(X0,X1),X0),
inference(paramodulation,[status(thm)],[f26,f21]) ).
fof(f434,plain,
! [X0,X1] : multiply(X0,multiplicative_identity) = add(X0,multiply(X0,X1)),
inference(forward_demodulation,[status(thm)],[f190,f401]) ).
fof(f435,plain,
! [X0,X1] : X0 = add(X0,multiply(X0,X1)),
inference(forward_demodulation,[status(thm)],[f26,f434]) ).
fof(f439,plain,
! [X0,X1] : multiply(X0,multiplicative_identity) = add(multiply(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f211,f414]) ).
fof(f440,plain,
! [X0,X1] : X0 = add(multiply(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f26,f439]) ).
fof(f448,plain,
multiply(multiplicative_identity,sF3_fnc) = add(sF2_fnc,multiply(inverse(c),sF3_fnc)),
inference(paramodulation,[status(thm)],[f22,f339]) ).
fof(f464,plain,
sF3_fnc = add(sF2_fnc,multiply(inverse(c),sF3_fnc)),
inference(forward_demodulation,[status(thm)],[f44,f448]) ).
fof(f476,plain,
sF3_fnc = add(sF2_fnc,multiply(sF3_fnc,inverse(c))),
inference(paramodulation,[status(thm)],[f17,f464]) ).
fof(f514,plain,
! [X0] : additive_identity = multiply(X0,additive_identity),
inference(paramodulation,[status(thm)],[f29,f374]) ).
fof(f525,plain,
c = add(c,sF1_fnc),
inference(paramodulation,[status(thm)],[f31,f374]) ).
fof(f546,plain,
! [X0] : additive_identity = multiply(additive_identity,X0),
inference(paramodulation,[status(thm)],[f17,f514]) ).
fof(f610,plain,
b = add(sF3_fnc,b),
inference(paramodulation,[status(thm)],[f33,f379]) ).
fof(f611,plain,
sF1_fnc = add(sF0_fnc,sF1_fnc),
inference(paramodulation,[status(thm)],[f32,f379]) ).
fof(f645,plain,
a = add(a,sF3_fnc),
inference(paramodulation,[status(thm)],[f33,f435]) ).
fof(f647,plain,
b = add(b,sF1_fnc),
inference(paramodulation,[status(thm)],[f31,f435]) ).
fof(f687,plain,
a = add(sF0_fnc,a),
inference(paramodulation,[status(thm)],[f32,f440]) ).
fof(f752,plain,
multiply(b,c) = add(sF2_fnc,multiply(b,c)),
inference(paramodulation,[status(thm)],[f610,f340]) ).
fof(f759,plain,
sF1_fnc = add(sF2_fnc,multiply(b,c)),
inference(forward_demodulation,[status(thm)],[f31,f752]) ).
fof(f760,plain,
sF1_fnc = add(sF2_fnc,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f31,f759]) ).
fof(f773,plain,
! [X0,X1] : add(additive_identity,X0) = multiply(X0,add(X1,X0)),
inference(forward_demodulation,[status(thm)],[f546,f70]) ).
fof(f774,plain,
! [X0,X1] : X0 = multiply(X0,add(X1,X0)),
inference(forward_demodulation,[status(thm)],[f29,f773]) ).
fof(f808,plain,
! [X0,X1] : X0 = multiply(X0,add(X0,X1)),
inference(paramodulation,[status(thm)],[f16,f774]) ).
fof(f832,plain,
! [X0] : add(multiply(sF1_fnc,X0),c) = multiply(c,add(X0,c)),
inference(paramodulation,[status(thm)],[f525,f72]) ).
fof(f882,plain,
! [X0,X1] : add(multiply(X0,additive_identity),X1) = multiply(add(X1,X0),X1),
inference(paramodulation,[status(thm)],[f29,f72]) ).
fof(f909,plain,
! [X0] : add(multiply(sF1_fnc,X0),c) = c,
inference(forward_demodulation,[status(thm)],[f774,f832]) ).
fof(f932,plain,
! [X0,X1] : add(additive_identity,X0) = multiply(add(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f514,f882]) ).
fof(f933,plain,
! [X0,X1] : X0 = multiply(add(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f29,f932]) ).
fof(f944,plain,
! [X0] : add(multiply(sF3_fnc,X0),a) = multiply(a,add(X0,a)),
inference(paramodulation,[status(thm)],[f645,f72]) ).
fof(f950,plain,
! [X0] : add(multiply(sF3_fnc,X0),a) = a,
inference(forward_demodulation,[status(thm)],[f774,f944]) ).
fof(f960,plain,
! [X0] : add(multiply(sF1_fnc,X0),b) = multiply(b,add(X0,b)),
inference(paramodulation,[status(thm)],[f647,f72]) ).
fof(f966,plain,
! [X0] : add(multiply(sF1_fnc,X0),b) = b,
inference(forward_demodulation,[status(thm)],[f774,f960]) ).
fof(f1251,plain,
sF2_fnc = multiply(sF2_fnc,sF1_fnc),
inference(paramodulation,[status(thm)],[f760,f808]) ).
fof(f1302,plain,
sF0_fnc = multiply(a,sF0_fnc),
inference(paramodulation,[status(thm)],[f687,f933]) ).
fof(f1303,plain,
sF0_fnc = multiply(sF1_fnc,sF0_fnc),
inference(paramodulation,[status(thm)],[f611,f933]) ).
fof(f1316,plain,
sF2_fnc = multiply(sF3_fnc,sF2_fnc),
inference(paramodulation,[status(thm)],[f476,f933]) ).
fof(f4283,plain,
add(sF0_fnc,c) = c,
inference(paramodulation,[status(thm)],[f1303,f909]) ).
fof(f4556,plain,
sF0_fnc = multiply(sF0_fnc,c),
inference(paramodulation,[status(thm)],[f4283,f808]) ).
fof(f4818,plain,
add(sF2_fnc,a) = a,
inference(paramodulation,[status(thm)],[f1316,f950]) ).
fof(f4924,plain,
multiply(a,sF1_fnc) = add(multiply(sF2_fnc,sF1_fnc),sF0_fnc),
inference(paramodulation,[status(thm)],[f4818,f355]) ).
fof(f4972,plain,
sF0_fnc = add(multiply(sF2_fnc,sF1_fnc),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f32,f4924]) ).
fof(f4973,plain,
sF0_fnc = add(sF2_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f1251,f4972]) ).
fof(f6224,plain,
add(sF0_fnc,b) = b,
inference(paramodulation,[status(thm)],[f1303,f966]) ).
fof(f6269,plain,
add(b,sF0_fnc) = b,
inference(paramodulation,[status(thm)],[f16,f6224]) ).
fof(f6525,plain,
multiply(a,b) = add(sF3_fnc,multiply(a,sF0_fnc)),
inference(paramodulation,[status(thm)],[f6269,f397]) ).
fof(f6568,plain,
sF3_fnc = add(sF3_fnc,multiply(a,sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f33,f6525]) ).
fof(f6569,plain,
sF3_fnc = add(sF3_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f1302,f6568]) ).
fof(f6599,plain,
multiply(sF3_fnc,c) = add(sF2_fnc,multiply(sF0_fnc,c)),
inference(paramodulation,[status(thm)],[f6569,f340]) ).
fof(f6620,plain,
sF2_fnc = add(sF2_fnc,multiply(sF0_fnc,c)),
inference(forward_demodulation,[status(thm)],[f34,f6599]) ).
fof(f6621,plain,
sF2_fnc = add(sF2_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f4556,f6620]) ).
fof(f6622,plain,
sF2_fnc = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f4973,f6621]) ).
fof(f6623,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f6622,f35]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : BOO007-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n019.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 21 13:47:19 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 % Drodi V4.1.1
% 1.54/0.60 % Refutation found
% 1.54/0.60 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.54/0.60 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.54/0.61 % Elapsed time: 0.259768 seconds
% 1.54/0.61 % CPU time: 1.931127 seconds
% 1.54/0.61 % Total memory used: 41.041 MB
% 1.54/0.61 % Net memory used: 39.830 MB
%------------------------------------------------------------------------------