%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : BOO007-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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 162.27s 22.32s
% Output : CNFRefutation 162.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 20
% Syntax : Number of formulae : 165 ( 91 unt; 0 def)
% Number of atoms : 313 ( 52 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 298 ( 150 ~; 148 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 9 con; 0-2 aty)
% Number of variables : 337 ( 337 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] : sum(X,Y,add(X,Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] : product(X,Y,multiply(X,Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y,Z] :
( sum(Y,X,Z)
| ~ sum(X,Y,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y,Z] :
( product(Y,X,Z)
| ~ product(X,Y,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X] : sum(additive_identity,X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X] : sum(X,additive_identity,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X] : product(multiplicative_identity,X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X] : product(X,multiplicative_identity,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,Y,V1,Z,V2,V3,V4] :
( sum(V1,V2,V4)
| ~ product(X,V3,V4)
| ~ sum(Y,Z,V3)
| ~ product(X,Z,V2)
| ~ product(X,Y,V1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [Y,X,V1,Z,V2,V3,V4] :
( product(V3,X,V4)
| ~ sum(V1,V2,V4)
| ~ sum(Y,Z,V3)
| ~ product(Z,X,V2)
| ~ product(Y,X,V1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X,Y,V1,Z,V2,V3,V4] :
( product(V1,V2,V4)
| ~ sum(X,V3,V4)
| ~ product(Y,Z,V3)
| ~ sum(X,Z,V2)
| ~ sum(X,Y,V1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [Y,X,V1,Z,V2,V3,V4] :
( sum(V3,X,V4)
| ~ product(V1,V2,V4)
| ~ product(Y,Z,V3)
| ~ sum(Z,X,V2)
| ~ sum(Y,X,V1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [X] : product(inverse(X),X,additive_identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [X,Y,U,V] :
( U = V
| ~ sum(X,Y,V)
| ~ sum(X,Y,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [X,Y,U,V] :
( U = V
| ~ product(X,Y,V)
| ~ product(X,Y,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,hypothesis,
product(y,z,y_times_z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,hypothesis,
product(x,y_times_z,x_times__y_times_z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,hypothesis,
product(x,y,x_times_y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,hypothesis,
product(x_times_y,z,x_times_y__times_z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,negated_conjecture,
x_times__y_times_z != x_times_y__times_z,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,plain,
! [X0,X1] : sum(X0,X1,add(X0,X1)),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f29,plain,
! [X0,X1] : product(X0,X1,multiply(X0,X1)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f30,plain,
! [X0,X1,X2] :
( ~ sum(X1,X0,X2)
| sum(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f31,plain,
! [X0,X1,X2] :
( ~ product(X1,X0,X2)
| product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f32,plain,
! [X0] : sum(additive_identity,X0,X0),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f33,plain,
! [X0] : sum(X0,additive_identity,X0),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f34,plain,
! [X0] : product(multiplicative_identity,X0,X0),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f35,plain,
! [X0] : product(X0,multiplicative_identity,X0),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f36,plain,
! [V1,V2,V4] :
( sum(V1,V2,V4)
| ! [X,V3] :
( ~ product(X,V3,V4)
| ! [Y,Z] :
( ~ sum(Y,Z,V3)
| ~ product(X,Z,V2)
| ~ product(X,Y,V1) ) ) ),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f37,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( sum(X6,X5,X2)
| ~ product(X0,X3,X6)
| ~ product(X0,X4,X5)
| ~ sum(X3,X4,X1)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f42,plain,
! [X,V3,V4] :
( product(V3,X,V4)
| ! [V1,V2] :
( ~ sum(V1,V2,V4)
| ! [Y,Z] :
( ~ sum(Y,Z,V3)
| ~ product(Z,X,V2)
| ~ product(Y,X,V1) ) ) ),
inference(miniscoping,[status(thm)],[f12]) ).
fof(f43,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( product(X5,X1,X6)
| ~ sum(X2,X4,X6)
| ~ sum(X0,X3,X5)
| ~ product(X3,X1,X4)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f44,plain,
! [V1,V2,V4] :
( product(V1,V2,V4)
| ! [X,V3] :
( ~ sum(X,V3,V4)
| ! [Y,Z] :
( ~ product(Y,Z,V3)
| ~ sum(X,Z,V2)
| ~ sum(X,Y,V1) ) ) ),
inference(miniscoping,[status(thm)],[f13]) ).
fof(f45,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( product(X4,X6,X2)
| ~ sum(X0,X5,X6)
| ~ product(X3,X5,X1)
| ~ sum(X0,X3,X4)
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f50,plain,
! [X,V3,V4] :
( sum(V3,X,V4)
| ! [V1,V2] :
( ~ product(V1,V2,V4)
| ! [Y,Z] :
( ~ product(Y,Z,V3)
| ~ sum(Z,X,V2)
| ~ sum(Y,X,V1) ) ) ),
inference(miniscoping,[status(thm)],[f16]) ).
fof(f51,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ product(X2,X4,X6)
| ~ product(X0,X3,X5)
| sum(X5,X1,X6)
| ~ sum(X3,X1,X4)
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f54,plain,
! [X0] : product(inverse(X0),X0,additive_identity),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f56,plain,
! [U,V] :
( U = V
| ! [X,Y] :
( ~ sum(X,Y,V)
| ~ sum(X,Y,U) ) ),
inference(miniscoping,[status(thm)],[f21]) ).
fof(f57,plain,
! [X0,X1,X2,X3] :
( ~ sum(X2,X3,X1)
| ~ sum(X2,X3,X0)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f58,plain,
! [U,V] :
( U = V
| ! [X,Y] :
( ~ product(X,Y,V)
| ~ product(X,Y,U) ) ),
inference(miniscoping,[status(thm)],[f22]) ).
fof(f59,plain,
! [X0,X1,X2,X3] :
( ~ product(X0,X1,X3)
| X2 = X3
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f60,plain,
product(y,z,y_times_z),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f61,plain,
product(x,y_times_z,x_times__y_times_z),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f62,plain,
product(x,y,x_times_y),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f63,plain,
product(x_times_y,z,x_times_y__times_z),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f64,plain,
x_times__y_times_z != x_times_y__times_z,
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f66,plain,
! [X0,X1,X2,X3] :
( ~ product(x_times_y,X3,X2)
| ~ sum(X0,X3,z)
| sum(X1,X2,x_times_y__times_z)
| ~ product(x_times_y,X0,X1) ),
inference(resolution,[status(thm)],[f37,f63]) ).
fof(f67,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sum(X5,X1,X4)
| ~ product(X0,X5,X3)
| sum(X3,X2,multiply(X0,X4))
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f37,f29]) ).
fof(f68,plain,
! [X0,X1,X2,X3,X4] :
( sum(X4,X2,X0)
| ~ sum(X3,X1,multiplicative_identity)
| ~ product(X0,X3,X4)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f35,f37]) ).
fof(f70,plain,
! [X0] :
( x_times__y_times_z = X0
| ~ product(x,y_times_z,X0) ),
inference(resolution,[status(thm)],[f59,f61]) ).
fof(f72,plain,
! [X0,X1] :
( ~ product(X1,multiplicative_identity,X0)
| X0 = X1 ),
inference(resolution,[status(thm)],[f59,f35]) ).
fof(f73,plain,
! [X0,X1,X2] :
( multiply(X0,X1) = X2
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f59,f29]) ).
fof(f76,plain,
x_times__y_times_z = multiply(x,y_times_z),
inference(resolution,[status(thm)],[f70,f29]) ).
fof(f79,plain,
product(z,x_times_y,x_times_y__times_z),
inference(resolution,[status(thm)],[f31,f63]) ).
fof(f81,plain,
! [X0,X1] : product(X0,X1,multiply(X1,X0)),
inference(resolution,[status(thm)],[f31,f29]) ).
fof(f86,plain,
! [X0] :
( ~ product(z,x_times_y,X0)
| X0 = x_times_y__times_z ),
inference(resolution,[status(thm)],[f79,f59]) ).
fof(f89,plain,
! [X0,X1] :
( X1 = X0
| ~ product(multiplicative_identity,X0,X1) ),
inference(resolution,[status(thm)],[f34,f59]) ).
fof(f92,plain,
! [X0,X1] :
( ~ product(inverse(X1),X1,X0)
| additive_identity = X0 ),
inference(resolution,[status(thm)],[f54,f59]) ).
fof(f104,plain,
multiply(z,x_times_y) = x_times_y__times_z,
inference(resolution,[status(thm)],[f86,f29]) ).
fof(f110,plain,
! [X0,X1,X2,X3,X4] :
( ~ product(X4,X1,X3)
| ~ sum(inverse(X1),X4,X0)
| ~ sum(additive_identity,X3,X2)
| product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f43,f54]) ).
fof(f115,plain,
! [X0,X1,X2,X3] :
( ~ sum(x_times_y,X2,X3)
| product(X3,z,X1)
| ~ product(X2,z,X0)
| ~ sum(x_times_y__times_z,X0,X1) ),
inference(resolution,[status(thm)],[f43,f63]) ).
fof(f116,plain,
! [X0,X1,X2,X3,X4] :
( ~ sum(X2,X0,X4)
| product(X4,multiplicative_identity,X3)
| ~ sum(X2,X1,X3)
| ~ product(X0,multiplicative_identity,X1) ),
inference(resolution,[status(thm)],[f43,f35]) ).
fof(f124,plain,
product(y,x,x_times_y),
inference(resolution,[status(thm)],[f62,f31]) ).
fof(f126,plain,
! [X0,X1,X2,X3] :
( ~ product(x,X3,X0)
| ~ sum(X3,X2,y)
| ~ product(x,X2,X1)
| sum(X0,X1,x_times_y) ),
inference(resolution,[status(thm)],[f62,f37]) ).
fof(f128,plain,
product(z,y,y_times_z),
inference(resolution,[status(thm)],[f60,f31]) ).
fof(f147,plain,
! [X0,X1,X2,X3,X4,X5] :
( product(X2,X4,add(X0,X5))
| ~ product(X1,X3,X5)
| ~ sum(X0,X3,X4)
| ~ sum(X0,X1,X2) ),
inference(resolution,[status(thm)],[f45,f28]) ).
fof(f152,plain,
! [X0,X1,X2] :
( ~ sum(X2,X0,z)
| sum(multiply(X2,x_times_y),X1,x_times_y__times_z)
| ~ product(x_times_y,X0,X1) ),
inference(resolution,[status(thm)],[f81,f66]) ).
fof(f157,plain,
! [X0] : X0 = multiply(multiplicative_identity,X0),
inference(resolution,[status(thm)],[f81,f72]) ).
fof(f160,plain,
! [X0,X1,X2] :
( ~ product(X2,X1,X0)
| X0 = multiply(X1,X2) ),
inference(resolution,[status(thm)],[f81,f59]) ).
fof(f242,plain,
! [X0,X1] : sum(X0,X1,add(X1,X0)),
inference(resolution,[status(thm)],[f30,f28]) ).
fof(f245,plain,
! [X0,X1,X2] :
( ~ sum(x_times_y,X2,X0)
| ~ product(X2,z,X1)
| product(X0,z,add(X1,x_times_y__times_z)) ),
inference(resolution,[status(thm)],[f242,f115]) ).
fof(f269,plain,
y_times_z = multiply(y,z),
inference(resolution,[status(thm)],[f73,f60]) ).
fof(f280,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,X0),
inference(resolution,[status(thm)],[f73,f81]) ).
fof(f442,plain,
! [X0,X1] :
( X0 = X1
| ~ sum(additive_identity,X0,X1) ),
inference(resolution,[status(thm)],[f57,f32]) ).
fof(f445,plain,
! [X0,X1,X2] :
( ~ sum(X2,X1,X0)
| X0 = add(X1,X2) ),
inference(resolution,[status(thm)],[f57,f242]) ).
fof(f446,plain,
! [X0,X1,X2] :
( ~ sum(X1,X2,X0)
| X0 = add(X1,X2) ),
inference(resolution,[status(thm)],[f57,f28]) ).
fof(f450,plain,
! [X0] : add(X0,additive_identity) = X0,
inference(resolution,[status(thm)],[f442,f242]) ).
fof(f451,plain,
! [X0] : add(additive_identity,X0) = X0,
inference(resolution,[status(thm)],[f442,f28]) ).
fof(f472,plain,
! [X0,X1] :
( ~ sum(X0,X1,z)
| sum(multiply(X0,x_times_y),multiply(x_times_y,X1),x_times_y__times_z) ),
inference(resolution,[status(thm)],[f152,f29]) ).
fof(f487,plain,
! [X0,X1] : add(X0,X1) = add(X1,X0),
inference(resolution,[status(thm)],[f445,f28]) ).
fof(f564,plain,
! [X0,X1,X2,X3,X4,X5] :
( sum(X5,X1,X3)
| ~ product(X0,X4,X5)
| ~ sum(X4,X1,X2)
| ~ product(add(X0,X1),X2,X3) ),
inference(resolution,[status(thm)],[f51,f28]) ).
fof(f708,plain,
! [X0] :
( ~ sum(x_times_y,y,X0)
| product(X0,z,add(y_times_z,x_times_y__times_z)) ),
inference(resolution,[status(thm)],[f245,f60]) ).
fof(f717,plain,
! [X0] :
( product(X0,z,add(x_times_y__times_z,y_times_z))
| ~ sum(x_times_y,y,X0) ),
inference(forward_demodulation,[status(thm)],[f487,f708]) ).
fof(f724,plain,
! [X0,X1,X2,X3] :
( ~ sum(X3,X1,X2)
| ~ product(multiplicative_identity,X3,X0)
| sum(X0,X1,multiply(multiplicative_identity,X2)) ),
inference(resolution,[status(thm)],[f67,f34]) ).
fof(f730,plain,
! [X0,X1,X2] :
( ~ sum(X2,y_times_z,X1)
| ~ product(x,X2,X0)
| sum(X0,x_times__y_times_z,multiply(x,X1)) ),
inference(resolution,[status(thm)],[f67,f61]) ).
fof(f736,plain,
! [X0,X1,X2,X3] :
( ~ sum(X0,X2,X3)
| sum(X1,X2,X3)
| ~ product(multiplicative_identity,X0,X1) ),
inference(forward_demodulation,[status(thm)],[f157,f724]) ).
fof(f794,plain,
! [X0,X1,X2] :
( sum(X2,X0,X0)
| ~ sum(X1,multiplicative_identity,multiplicative_identity)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f68,f35]) ).
fof(f860,plain,
! [X0,X1,X2,X3] :
( ~ product(X3,X1,X2)
| ~ sum(inverse(X1),X3,X0)
| product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f110,f32]) ).
fof(f917,plain,
( ~ sum(x,multiplicative_identity,multiplicative_identity)
| sum(x_times_y,y,y) ),
inference(resolution,[status(thm)],[f794,f124]) ).
fof(f918,plain,
( sum(y_times_z,y,y)
| ~ sum(z,multiplicative_identity,multiplicative_identity) ),
inference(resolution,[status(thm)],[f794,f60]) ).
fof(f922,plain,
( sum(y_times_z,z,z)
| ~ sum(y,multiplicative_identity,multiplicative_identity) ),
inference(resolution,[status(thm)],[f794,f128]) ).
fof(f927,plain,
( ~ sum(y,multiplicative_identity,multiplicative_identity)
| sum(x_times_y,x,x) ),
inference(resolution,[status(thm)],[f794,f62]) ).
fof(f993,plain,
! [X0,X1,X2,X3] :
( ~ sum(X0,X1,X3)
| product(X3,multiplicative_identity,X2)
| ~ sum(X0,multiply(multiplicative_identity,X1),X2) ),
inference(resolution,[status(thm)],[f116,f81]) ).
fof(f995,plain,
! [X0,X1,X2,X3] :
( ~ sum(X2,X3,X0)
| ~ sum(X2,X3,X1)
| product(X0,multiplicative_identity,X1) ),
inference(forward_demodulation,[status(thm)],[f157,f993]) ).
fof(f1268,plain,
! [X0,X1] :
( ~ product(x,X0,X1)
| sum(X1,x_times_y,x_times_y)
| ~ sum(X0,y,y) ),
inference(resolution,[status(thm)],[f126,f62]) ).
fof(f1314,plain,
! [X0,X1,X2] :
( ~ sum(X2,X1,X0)
| product(X0,multiplicative_identity,add(X1,X2)) ),
inference(resolution,[status(thm)],[f995,f242]) ).
fof(f1362,plain,
! [X0,X1] : product(add(X0,X1),multiplicative_identity,add(X1,X0)),
inference(resolution,[status(thm)],[f1314,f28]) ).
fof(f1413,plain,
! [X0,X1] : product(multiplicative_identity,add(X0,X1),add(X1,X0)),
inference(resolution,[status(thm)],[f1362,f31]) ).
fof(f1479,plain,
! [X0,X1,X2,X3] :
( sum(add(X1,X0),X2,X3)
| ~ sum(add(X0,X1),X2,X3) ),
inference(resolution,[status(thm)],[f1413,f736]) ).
fof(f1752,plain,
product(add(x_times_y,y),z,add(x_times_y__times_z,y_times_z)),
inference(resolution,[status(thm)],[f717,f28]) ).
fof(f1753,plain,
product(add(y,x_times_y),z,add(x_times_y__times_z,y_times_z)),
inference(forward_demodulation,[status(thm)],[f487,f1752]) ).
fof(f1779,plain,
multiply(add(y,x_times_y),z) = add(x_times_y__times_z,y_times_z),
inference(resolution,[status(thm)],[f1753,f73]) ).
fof(f1784,plain,
multiply(z,add(y,x_times_y)) = add(x_times_y__times_z,y_times_z),
inference(forward_demodulation,[status(thm)],[f280,f1779]) ).
fof(f1955,plain,
! [X0,X1] :
( sum(multiply(x,X0),x_times__y_times_z,multiply(x,X1))
| ~ sum(X0,y_times_z,X1) ),
inference(resolution,[status(thm)],[f730,f29]) ).
fof(f1975,plain,
! [X0,X1,X2,X3] :
( product(X2,X1,add(additive_identity,X3))
| ~ product(X2,X0,X3)
| ~ sum(additive_identity,X0,X1) ),
inference(resolution,[status(thm)],[f147,f32]) ).
fof(f1980,plain,
! [X0,X1,X2,X3,X4] :
( ~ sum(X1,X4,X2)
| ~ product(X0,X4,X3)
| product(add(X0,X1),X2,add(X1,X3)) ),
inference(resolution,[status(thm)],[f147,f242]) ).
fof(f1982,plain,
! [X0,X1,X2,X3] :
( ~ sum(additive_identity,X1,X3)
| product(X0,X3,X2)
| ~ product(X0,X1,X2) ),
inference(forward_demodulation,[status(thm)],[f451,f1975]) ).
fof(f2099,plain,
! [X0,X1,X2] : sum(add(X0,X1),X2,add(X2,add(X1,X0))),
inference(resolution,[status(thm)],[f1479,f242]) ).
fof(f2555,plain,
! [X0,X1,X2] : sum(X0,add(X1,X2),add(X0,add(X2,X1))),
inference(resolution,[status(thm)],[f2099,f30]) ).
fof(f4188,plain,
! [X0,X1,X2] :
( ~ sum(additive_identity,X2,X1)
| product(X0,X1,multiply(X2,X0)) ),
inference(resolution,[status(thm)],[f1982,f81]) ).
fof(f4313,plain,
! [X0,X1,X2] : product(X0,add(additive_identity,add(X1,X2)),multiply(add(X2,X1),X0)),
inference(resolution,[status(thm)],[f4188,f2555]) ).
fof(f4321,plain,
! [X0,X1,X2] : product(X0,add(X1,X2),multiply(add(X2,X1),X0)),
inference(forward_demodulation,[status(thm)],[f451,f4313]) ).
fof(f4540,plain,
! [X0,X1,X2] : multiply(X0,add(X1,X2)) = multiply(add(X2,X1),X0),
inference(resolution,[status(thm)],[f4321,f73]) ).
fof(f4543,plain,
! [X0,X1,X2,X3] :
( multiply(add(X2,X1),X0) = X3
| ~ product(X0,add(X1,X2),X3) ),
inference(resolution,[status(thm)],[f4321,f59]) ).
fof(f4995,plain,
! [X0,X1,X2,X3,X4] :
( ~ sum(X4,X1,X2)
| ~ product(X3,X4,X0)
| sum(X0,X1,multiply(X2,add(X3,X1))) ),
inference(resolution,[status(thm)],[f564,f81]) ).
fof(f7796,plain,
! [X0,X1] :
( product(inverse(X0),X0,X1)
| ~ product(additive_identity,X0,X1) ),
inference(resolution,[status(thm)],[f860,f33]) ).
fof(f8322,plain,
! [X0] : product(inverse(X0),X0,multiply(additive_identity,X0)),
inference(resolution,[status(thm)],[f7796,f29]) ).
fof(f8335,plain,
! [X0] : additive_identity = multiply(additive_identity,X0),
inference(resolution,[status(thm)],[f8322,f92]) ).
fof(f8445,plain,
! [X0] : product(additive_identity,X0,additive_identity),
inference(paramodulation,[status(thm)],[f8335,f29]) ).
fof(f17433,plain,
( ~ sum(y_times_z,y,y)
| sum(x_times__y_times_z,x_times_y,x_times_y) ),
inference(resolution,[status(thm)],[f1268,f61]) ).
fof(f20151,plain,
! [X0,X1,X2] :
( ~ sum(X0,X2,X1)
| product(add(additive_identity,X0),X1,add(X0,additive_identity)) ),
inference(resolution,[status(thm)],[f1980,f8445]) ).
fof(f20237,plain,
! [X0,X1,X2] :
( ~ sum(X0,X2,X1)
| product(X0,X1,add(X0,additive_identity)) ),
inference(forward_demodulation,[status(thm)],[f451,f20151]) ).
fof(f20238,plain,
! [X0,X1,X2] :
( ~ sum(X0,X2,X1)
| product(X0,X1,X0) ),
inference(forward_demodulation,[status(thm)],[f450,f20237]) ).
fof(f20403,plain,
! [X0,X1] : product(X0,add(X1,X0),X0),
inference(resolution,[status(thm)],[f20238,f242]) ).
fof(f20612,plain,
! [X0] : multiplicative_identity = add(X0,multiplicative_identity),
inference(resolution,[status(thm)],[f20403,f89]) ).
fof(f20655,plain,
! [X0,X1] : multiply(add(X0,X1),X0) = X0,
inference(resolution,[status(thm)],[f20403,f4543]) ).
fof(f20684,plain,
! [X0,X1] : X0 = multiply(add(X1,X0),X0),
inference(resolution,[status(thm)],[f20403,f160]) ).
fof(f20709,plain,
! [X0,X1] : X0 = multiply(X0,add(X0,X1)),
inference(forward_demodulation,[status(thm)],[f4540,f20684]) ).
fof(f20714,plain,
! [X0,X1] : X0 = multiply(X0,add(X1,X0)),
inference(forward_demodulation,[status(thm)],[f4540,f20655]) ).
fof(f20902,plain,
! [X0] : sum(X0,multiplicative_identity,multiplicative_identity),
inference(paramodulation,[status(thm)],[f20612,f28]) ).
fof(f21660,plain,
sum(x_times_y,x,x),
inference(backward_subsumption_resolution,[status(thm)],[f927,f20902]) ).
fof(f21661,plain,
sum(y_times_z,z,z),
inference(backward_subsumption_resolution,[status(thm)],[f922,f20902]) ).
fof(f21664,plain,
sum(y_times_z,y,y),
inference(backward_subsumption_resolution,[status(thm)],[f918,f20902]) ).
fof(f21666,plain,
sum(x_times_y,y,y),
inference(backward_subsumption_resolution,[status(thm)],[f917,f20902]) ).
fof(f23849,plain,
sum(x_times__y_times_z,x_times_y,x_times_y),
inference(backward_subsumption_resolution,[status(thm)],[f17433,f21664]) ).
fof(f24119,plain,
y = add(y,x_times_y),
inference(resolution,[status(thm)],[f21666,f445]) ).
fof(f24842,plain,
x_times_y = add(x_times_y,x_times__y_times_z),
inference(resolution,[status(thm)],[f23849,f445]) ).
fof(f24849,plain,
x_times_y = add(x_times__y_times_z,x_times_y),
inference(forward_demodulation,[status(thm)],[f487,f24842]) ).
fof(f24864,plain,
multiply(x_times__y_times_z,x_times_y) = x_times__y_times_z,
inference(paramodulation,[status(thm)],[f24849,f20709]) ).
fof(f26618,plain,
multiply(z,y) = add(x_times_y__times_z,y_times_z),
inference(backward_demodulation,[status(thm)],[f24119,f1784]) ).
fof(f26791,plain,
multiply(y,z) = add(x_times_y__times_z,y_times_z),
inference(forward_demodulation,[status(thm)],[f280,f26618]) ).
fof(f26792,plain,
y_times_z = add(x_times_y__times_z,y_times_z),
inference(forward_demodulation,[status(thm)],[f269,f26791]) ).
fof(f26965,plain,
sum(x_times_y__times_z,y_times_z,y_times_z),
inference(paramodulation,[status(thm)],[f26792,f28]) ).
fof(f27132,plain,
sum(multiply(x,x_times_y__times_z),x_times__y_times_z,multiply(x,y_times_z)),
inference(resolution,[status(thm)],[f26965,f1955]) ).
fof(f27171,plain,
sum(multiply(x,x_times_y__times_z),x_times__y_times_z,x_times__y_times_z),
inference(forward_demodulation,[status(thm)],[f76,f27132]) ).
fof(f30741,plain,
add(x_times__y_times_z,multiply(x,x_times_y__times_z)) = x_times__y_times_z,
inference(resolution,[status(thm)],[f27171,f445]) ).
fof(f43053,plain,
! [X0,X1] :
( sum(x_times_y__times_z,X0,multiply(X1,add(z,X0)))
| ~ sum(x_times_y,X0,X1) ),
inference(resolution,[status(thm)],[f4995,f79]) ).
fof(f43068,plain,
! [X0,X1] :
( sum(x_times__y_times_z,X0,multiply(X1,add(x,X0)))
| ~ sum(y_times_z,X0,X1) ),
inference(resolution,[status(thm)],[f4995,f61]) ).
fof(f46943,plain,
sum(x_times_y__times_z,x,multiply(x,add(z,x))),
inference(resolution,[status(thm)],[f43053,f21660]) ).
fof(f46967,plain,
sum(x_times_y__times_z,x,x),
inference(forward_demodulation,[status(thm)],[f20714,f46943]) ).
fof(f47034,plain,
x = add(x_times_y__times_z,x),
inference(resolution,[status(thm)],[f46967,f446]) ).
fof(f47045,plain,
x = add(x,x_times_y__times_z),
inference(forward_demodulation,[status(thm)],[f487,f47034]) ).
fof(f47139,plain,
x_times_y__times_z = multiply(x_times_y__times_z,x),
inference(paramodulation,[status(thm)],[f47045,f20714]) ).
fof(f47377,plain,
multiply(x,x_times_y__times_z) = x_times_y__times_z,
inference(forward_demodulation,[status(thm)],[f280,f47139]) ).
fof(f48095,plain,
add(x_times__y_times_z,x_times_y__times_z) = x_times__y_times_z,
inference(backward_demodulation,[status(thm)],[f47377,f30741]) ).
fof(f48238,plain,
sum(x_times__y_times_z,z,multiply(z,add(x,z))),
inference(resolution,[status(thm)],[f43068,f21661]) ).
fof(f48266,plain,
sum(x_times__y_times_z,z,z),
inference(forward_demodulation,[status(thm)],[f20714,f48238]) ).
fof(f49050,plain,
sum(multiply(x_times__y_times_z,x_times_y),multiply(x_times_y,z),x_times_y__times_z),
inference(resolution,[status(thm)],[f48266,f472]) ).
fof(f49104,plain,
sum(x_times__y_times_z,multiply(x_times_y,z),x_times_y__times_z),
inference(forward_demodulation,[status(thm)],[f24864,f49050]) ).
fof(f49105,plain,
sum(x_times__y_times_z,multiply(z,x_times_y),x_times_y__times_z),
inference(forward_demodulation,[status(thm)],[f280,f49104]) ).
fof(f49106,plain,
sum(x_times__y_times_z,x_times_y__times_z,x_times_y__times_z),
inference(forward_demodulation,[status(thm)],[f104,f49105]) ).
fof(f49705,plain,
x_times_y__times_z = add(x_times_y__times_z,x_times__y_times_z),
inference(resolution,[status(thm)],[f49106,f445]) ).
fof(f49712,plain,
x_times_y__times_z = add(x_times__y_times_z,x_times_y__times_z),
inference(forward_demodulation,[status(thm)],[f487,f49705]) ).
fof(f49713,plain,
x_times_y__times_z = x_times__y_times_z,
inference(forward_demodulation,[status(thm)],[f48095,f49712]) ).
fof(f49714,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f49713,f64]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO007-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.38 % Computer : n008.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 21 13:48:08 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.40 % Drodi V4.1.1
% 162.27/22.32 % Refutation found
% 162.27/22.32 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 162.27/22.32 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 162.27/22.40 % Elapsed time: 21.995676 seconds
% 162.27/22.40 % CPU time: 173.401276 seconds
% 162.27/22.40 % Total memory used: 369.633 MB
% 162.27/22.40 % Net memory used: 318.559 MB
%------------------------------------------------------------------------------