%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : BOO008-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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:19 PM UTC 2026
% Result : Unsatisfiable 173.15s 23.32s
% Output : CNFRefutation 173.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 23
% Syntax : Number of formulae : 204 ( 114 unt; 0 def)
% Number of atoms : 397 ( 58 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 388 ( 195 ~; 193 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 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 : 434 ( 434 !; 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(f10,axiom,
! [X,Y,V1,Z,V2,V3,V4] :
( product(X,V3,V4)
| ~ sum(V1,V2,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(f15,axiom,
! [Y,X,V1,Z,V2,V3,V4] :
( product(V1,V2,V4)
| ~ sum(V3,X,V4)
| ~ product(Y,Z,V3)
| ~ sum(Z,X,V2)
| ~ sum(Y,X,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(f18,axiom,
! [X] : sum(X,inverse(X),multiplicative_identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [X] : product(X,inverse(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,
sum(y,z,y_plus_z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,hypothesis,
sum(x,y_plus_z,x__plus_y_plus_z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,hypothesis,
sum(x,y,x_plus_y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,hypothesis,
sum(x_plus_y,z,x_plus_y__plus_z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,negated_conjecture,
x__plus_y_plus_z != x_plus_y__plus_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(f38,plain,
! [X,V3,V4] :
( product(X,V3,V4)
| ! [V1,V2] :
( ~ sum(V1,V2,V4)
| ! [Y,Z] :
( ~ sum(Y,Z,V3)
| ~ product(X,Z,V2)
| ~ product(X,Y,V1) ) ) ),
inference(miniscoping,[status(thm)],[f10]) ).
fof(f39,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sum(X6,X4,X5)
| ~ product(X3,X0,X6)
| product(X3,X2,X5)
| ~ product(X3,X1,X4)
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f38]) ).
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,X4,X0)
| product(X6,X4,X2)
| ~ sum(X5,X3,X6)
| ~ product(X3,X4,X1)
| ~ sum(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(X1,X3,X6)
| ~ sum(X0,X6,X5)
| product(X2,X4,X5)
| ~ sum(X0,X3,X4)
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f48,plain,
! [V1,V2,V4] :
( product(V1,V2,V4)
| ! [X,V3] :
( ~ sum(V3,X,V4)
| ! [Y,Z] :
( ~ product(Y,Z,V3)
| ~ sum(Z,X,V2)
| ~ sum(Y,X,V1) ) ) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f49,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sum(X5,X4,X1)
| ~ sum(X6,X4,X2)
| ~ product(X3,X5,X6)
| ~ sum(X3,X4,X0)
| product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
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] :
( sum(X6,X1,X4)
| ~ sum(X5,X1,X3)
| ~ product(X0,X5,X6)
| ~ product(X2,X3,X4)
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f53,plain,
! [X0] : sum(X0,inverse(X0),multiplicative_identity),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f55,plain,
! [X0] : product(X0,inverse(X0),additive_identity),
inference(cnf_transformation,[status(thm)],[f20]) ).
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] :
( X2 = X3
| ~ sum(X0,X1,X3)
| ~ sum(X0,X1,X2) ),
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,
sum(y,z,y_plus_z),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f61,plain,
sum(x,y_plus_z,x__plus_y_plus_z),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f62,plain,
sum(x,y,x_plus_y),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f63,plain,
sum(x_plus_y,z,x_plus_y__plus_z),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f64,plain,
x__plus_y_plus_z != x_plus_y__plus_z,
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f65,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ product(X5,X1,X4)
| ~ product(X5,X0,X3)
| sum(X3,X4,multiply(X5,X2))
| ~ sum(X0,X1,X2) ),
inference(resolution,[status(thm)],[f37,f29]) ).
fof(f66,plain,
! [X0,X1,X2,X3,X4] :
( ~ sum(X3,X4,multiplicative_identity)
| ~ product(X2,X4,X1)
| ~ product(X2,X3,X0)
| sum(X0,X1,X2) ),
inference(resolution,[status(thm)],[f35,f37]) ).
fof(f67,plain,
! [X0,X1,X2,X3,X4] :
( ~ sum(X4,X0,X3)
| ~ product(multiplicative_identity,X4,X2)
| sum(X2,X1,X3)
| ~ product(multiplicative_identity,X0,X1) ),
inference(resolution,[status(thm)],[f34,f37]) ).
fof(f71,plain,
! [X0,X1] :
( ~ product(multiplicative_identity,X1,X0)
| X0 = X1 ),
inference(resolution,[status(thm)],[f59,f34]) ).
fof(f73,plain,
! [X0,X1] :
( X0 = X1
| ~ product(X0,multiplicative_identity,X1) ),
inference(resolution,[status(thm)],[f59,f35]) ).
fof(f74,plain,
! [X0,X1,X2] :
( X2 = multiply(X0,X1)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f59,f29]) ).
fof(f78,plain,
! [X0] : multiply(X0,multiplicative_identity) = X0,
inference(resolution,[status(thm)],[f73,f29]) ).
fof(f95,plain,
! [X0,X1] : product(X0,X1,multiply(X1,X0)),
inference(resolution,[status(thm)],[f31,f29]) ).
fof(f99,plain,
! [X0,X1,X2] :
( ~ product(X2,X1,X0)
| X0 = multiply(X1,X2) ),
inference(resolution,[status(thm)],[f95,f59]) ).
fof(f103,plain,
sum(z,y,y_plus_z),
inference(resolution,[status(thm)],[f30,f60]) ).
fof(f106,plain,
sum(y,x,x_plus_y),
inference(resolution,[status(thm)],[f30,f62]) ).
fof(f107,plain,
sum(y_plus_z,x,x__plus_y_plus_z),
inference(resolution,[status(thm)],[f30,f61]) ).
fof(f108,plain,
sum(z,x_plus_y,x_plus_y__plus_z),
inference(resolution,[status(thm)],[f30,f63]) ).
fof(f111,plain,
! [X0,X1] : sum(X0,X1,add(X1,X0)),
inference(resolution,[status(thm)],[f30,f28]) ).
fof(f119,plain,
! [X0] : multiply(X0,inverse(X0)) = additive_identity,
inference(resolution,[status(thm)],[f74,f55]) ).
fof(f121,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,X0),
inference(resolution,[status(thm)],[f74,f95]) ).
fof(f175,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ product(X3,X1,X5)
| product(X4,X1,add(X2,X5))
| ~ sum(X0,X3,X4)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f43,f28]) ).
fof(f197,plain,
! [X0] :
( ~ sum(y_plus_z,x,X0)
| X0 = x__plus_y_plus_z ),
inference(resolution,[status(thm)],[f57,f107]) ).
fof(f199,plain,
! [X0] :
( ~ sum(z,x_plus_y,X0)
| X0 = x_plus_y__plus_z ),
inference(resolution,[status(thm)],[f57,f108]) ).
fof(f208,plain,
! [X0,X1] :
( ~ sum(X1,additive_identity,X0)
| X0 = X1 ),
inference(resolution,[status(thm)],[f57,f33]) ).
fof(f209,plain,
! [X0,X1,X2] :
( ~ sum(X1,X0,X2)
| add(X0,X1) = X2 ),
inference(resolution,[status(thm)],[f57,f111]) ).
fof(f210,plain,
! [X0,X1,X2] :
( X2 = add(X0,X1)
| ~ sum(X0,X1,X2) ),
inference(resolution,[status(thm)],[f57,f28]) ).
fof(f214,plain,
! [X0] : add(additive_identity,X0) = X0,
inference(resolution,[status(thm)],[f208,f111]) ).
fof(f215,plain,
! [X0] : add(X0,additive_identity) = X0,
inference(resolution,[status(thm)],[f208,f28]) ).
fof(f223,plain,
x__plus_y_plus_z = add(x,y_plus_z),
inference(resolution,[status(thm)],[f197,f111]) ).
fof(f257,plain,
x_plus_y__plus_z = add(z,x_plus_y),
inference(resolution,[status(thm)],[f199,f28]) ).
fof(f266,plain,
add(y,z) = y_plus_z,
inference(resolution,[status(thm)],[f209,f103]) ).
fof(f272,plain,
add(y,x) = x_plus_y,
inference(resolution,[status(thm)],[f209,f62]) ).
fof(f278,plain,
! [X0,X1] : add(X0,X1) = add(X1,X0),
inference(resolution,[status(thm)],[f209,f28]) ).
fof(f334,plain,
! [X0,X1,X2,X3,X4] :
( ~ sum(additive_identity,X4,X3)
| ~ product(X2,X0,X4)
| product(X2,X1,X3)
| ~ sum(additive_identity,X0,X1) ),
inference(resolution,[status(thm)],[f45,f32]) ).
fof(f336,plain,
! [X0,X1,X2,X3] :
( ~ sum(x,X3,X0)
| ~ product(y_plus_z,X3,X2)
| ~ sum(x,X2,X1)
| product(x__plus_y_plus_z,X0,X1) ),
inference(resolution,[status(thm)],[f45,f61]) ).
fof(f337,plain,
! [X0,X1,X2,X3] :
( ~ product(z,X2,X3)
| ~ sum(x_plus_y,X3,X1)
| ~ sum(x_plus_y,X2,X0)
| product(x_plus_y__plus_z,X0,X1) ),
inference(resolution,[status(thm)],[f45,f63]) ).
fof(f338,plain,
! [X0,X1,X2,X3,X4] :
( ~ sum(X0,X1,X3)
| ~ sum(X0,X2,X4)
| product(multiplicative_identity,X3,X4)
| ~ product(inverse(X0),X1,X2) ),
inference(resolution,[status(thm)],[f45,f53]) ).
fof(f341,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sum(X3,X1,X4)
| ~ sum(X3,X2,X5)
| product(add(X3,X0),X4,X5)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f45,f28]) ).
fof(f368,plain,
! [X0,X1] :
( ~ sum(x_plus_y,X1,X0)
| ~ product(z,additive_identity,X1)
| product(x_plus_y__plus_z,x_plus_y,X0) ),
inference(resolution,[status(thm)],[f337,f33]) ).
fof(f388,plain,
! [X0,X1,X2,X3] :
( product(x_plus_y__plus_z,X3,X2)
| ~ sum(X0,z,X3)
| ~ sum(X1,z,X2)
| ~ product(x_plus_y,X0,X1) ),
inference(resolution,[status(thm)],[f49,f63]) ).
fof(f412,plain,
! [X0,X1] :
( ~ product(y_plus_z,X1,y)
| ~ sum(x,X1,X0)
| product(x__plus_y_plus_z,X0,x_plus_y) ),
inference(resolution,[status(thm)],[f336,f62]) ).
fof(f442,plain,
! [X0,X1,X2,X3] :
( product(X0,x__plus_y_plus_z,X3)
| ~ product(X0,y_plus_z,X2)
| ~ sum(X1,X2,X3)
| ~ product(X0,x,X1) ),
inference(resolution,[status(thm)],[f39,f61]) ).
fof(f477,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ product(X5,X3,X0)
| ~ product(add(X5,X1),X4,X2)
| ~ sum(X3,X1,X4)
| sum(X0,X1,X2) ),
inference(resolution,[status(thm)],[f51,f28]) ).
fof(f516,plain,
! [X0,X1,X2,X3] :
( ~ product(X0,additive_identity,X3)
| sum(X3,X2,multiply(X0,X1))
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f65,f32]) ).
fof(f518,plain,
! [X0,X1,X2] :
( ~ product(X2,y_plus_z,X1)
| ~ product(X2,x,X0)
| sum(X0,X1,multiply(X2,x__plus_y_plus_z)) ),
inference(resolution,[status(thm)],[f65,f61]) ).
fof(f519,plain,
! [X0,X1,X2] :
( ~ product(X0,z,X2)
| sum(X1,X2,multiply(X0,x_plus_y__plus_z))
| ~ product(X0,x_plus_y,X1) ),
inference(resolution,[status(thm)],[f65,f63]) ).
fof(f520,plain,
! [X0,X1,X2,X3] :
( ~ product(X2,inverse(X3),X1)
| ~ product(X2,X3,X0)
| sum(X0,X1,multiply(X2,multiplicative_identity)) ),
inference(resolution,[status(thm)],[f65,f53]) ).
fof(f524,plain,
! [X0,X1,X2,X3] :
( ~ product(X2,X3,X0)
| ~ product(X2,inverse(X3),X1)
| sum(X0,X1,X2) ),
inference(forward_demodulation,[status(thm)],[f78,f520]) ).
fof(f582,plain,
! [X0,X1] :
( sum(X1,additive_identity,X0)
| ~ product(X0,X0,X1) ),
inference(resolution,[status(thm)],[f524,f55]) ).
fof(f583,plain,
! [X0,X1,X2] :
( ~ product(X2,X1,X0)
| sum(X0,multiply(inverse(X1),X2),X2) ),
inference(resolution,[status(thm)],[f524,f95]) ).
fof(f590,plain,
! [X0] : sum(multiply(X0,X0),additive_identity,X0),
inference(resolution,[status(thm)],[f582,f29]) ).
fof(f600,plain,
! [X0] : X0 = multiply(X0,X0),
inference(resolution,[status(thm)],[f590,f208]) ).
fof(f630,plain,
! [X0] : product(X0,X0,X0),
inference(paramodulation,[status(thm)],[f600,f29]) ).
fof(f668,plain,
! [X0] :
( ~ product(z,additive_identity,X0)
| product(x_plus_y__plus_z,x_plus_y,add(X0,x_plus_y)) ),
inference(resolution,[status(thm)],[f368,f111]) ).
fof(f673,plain,
! [X0,X1,X2] :
( ~ sum(multiply(X2,x_plus_y),z,X1)
| ~ sum(X2,z,X0)
| product(x_plus_y__plus_z,X0,X1) ),
inference(resolution,[status(thm)],[f388,f95]) ).
fof(f683,plain,
! [X0,X1,X2] :
( ~ sum(multiply(x,X0),X2,X1)
| ~ product(X0,y_plus_z,X2)
| product(X0,x__plus_y_plus_z,X1) ),
inference(resolution,[status(thm)],[f442,f95]) ).
fof(f688,plain,
product(x_plus_y__plus_z,x_plus_y,add(multiply(z,additive_identity),x_plus_y)),
inference(resolution,[status(thm)],[f668,f29]) ).
fof(f689,plain,
product(x_plus_y__plus_z,x_plus_y,add(x_plus_y,multiply(z,additive_identity))),
inference(forward_demodulation,[status(thm)],[f278,f688]) ).
fof(f709,plain,
! [X0,X1] : sum(multiply(X0,X1),multiply(inverse(X1),X0),X0),
inference(resolution,[status(thm)],[f583,f29]) ).
fof(f718,plain,
add(x_plus_y,multiply(z,additive_identity)) = multiply(x_plus_y,x_plus_y__plus_z),
inference(resolution,[status(thm)],[f689,f99]) ).
fof(f724,plain,
multiply(x_plus_y__plus_z,x_plus_y) = add(x_plus_y,multiply(z,additive_identity)),
inference(forward_demodulation,[status(thm)],[f121,f718]) ).
fof(f866,plain,
! [X0,X1,X2] :
( ~ product(X0,X2,X1)
| ~ sum(multiplicative_identity,X2,multiplicative_identity)
| sum(X0,X1,X0) ),
inference(resolution,[status(thm)],[f66,f35]) ).
fof(f870,plain,
! [X0,X1,X2,X3] :
( ~ product(multiplicative_identity,X3,X0)
| ~ sum(X3,X1,X2)
| sum(X0,X1,X2) ),
inference(resolution,[status(thm)],[f67,f34]) ).
fof(f1084,plain,
! [X0,X1] : sum(multiply(inverse(X0),X1),multiply(X1,X0),X1),
inference(resolution,[status(thm)],[f709,f30]) ).
fof(f1352,plain,
! [X0,X1,X2,X3] :
( product(X3,X1,add(X1,X2))
| ~ sum(multiplicative_identity,X0,X3)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f175,f34]) ).
fof(f1356,plain,
! [X0,X1,X2,X3,X4] :
( ~ sum(X4,X0,X3)
| product(X3,X1,add(multiply(X4,X1),X2))
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f175,f29]) ).
fof(f1771,plain,
! [X0,X1,X2] :
( ~ sum(X2,multiplicative_identity,X0)
| ~ sum(X2,inverse(X2),X1)
| product(multiplicative_identity,X0,X1) ),
inference(resolution,[status(thm)],[f338,f35]) ).
fof(f1967,plain,
! [X0,X1,X2,X3] :
( ~ sum(additive_identity,X3,X2)
| ~ product(X0,X1,X3)
| product(X0,add(additive_identity,X1),X2) ),
inference(resolution,[status(thm)],[f334,f28]) ).
fof(f1968,plain,
! [X0,X1,X2,X3] :
( ~ product(X0,X1,X3)
| ~ sum(additive_identity,X3,X2)
| product(X0,X1,X2) ),
inference(forward_demodulation,[status(thm)],[f214,f1967]) ).
fof(f1983,plain,
! [X0,X1,X2,X3,X4] :
( ~ sum(X0,X1,X4)
| product(add(X0,X2),X4,X3)
| ~ sum(X0,multiply(X1,X2),X3) ),
inference(resolution,[status(thm)],[f341,f95]) ).
fof(f3469,plain,
! [X0,X1,X2] :
( sum(X1,X2,add(X2,X0))
| ~ product(multiplicative_identity,X0,X1) ),
inference(resolution,[status(thm)],[f870,f111]) ).
fof(f3470,plain,
! [X0,X1,X2] :
( sum(X1,X2,add(X0,X2))
| ~ product(multiplicative_identity,X0,X1) ),
inference(resolution,[status(thm)],[f870,f28]) ).
fof(f3678,plain,
! [X0] :
( ~ product(y_plus_z,X0,y)
| product(x__plus_y_plus_z,add(X0,x),x_plus_y) ),
inference(resolution,[status(thm)],[f412,f111]) ).
fof(f4045,plain,
! [X0,X1,X2,X3] :
( ~ product(X2,X3,X0)
| ~ product(add(X2,additive_identity),X3,X1)
| sum(X0,additive_identity,X1) ),
inference(resolution,[status(thm)],[f477,f33]) ).
fof(f4048,plain,
! [X0,X1,X2,X3] :
( sum(X2,additive_identity,X3)
| ~ product(X0,X1,X3)
| ~ product(X0,X1,X2) ),
inference(forward_demodulation,[status(thm)],[f215,f4045]) ).
fof(f4172,plain,
! [X0,X1] :
( sum(multiply(x_plus_y,X0),X1,multiply(X0,x_plus_y__plus_z))
| ~ product(X0,z,X1) ),
inference(resolution,[status(thm)],[f519,f95]) ).
fof(f4266,plain,
! [X0,X1] :
( sum(multiply(x,X0),X1,multiply(X0,x__plus_y_plus_z))
| ~ product(X0,y_plus_z,X1) ),
inference(resolution,[status(thm)],[f518,f95]) ).
fof(f4458,plain,
! [X0,X1,X2] :
( sum(multiply(X0,X1),additive_identity,X2)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f4048,f29]) ).
fof(f4542,plain,
! [X0,X1] : sum(multiply(X0,X1),additive_identity,multiply(X1,X0)),
inference(resolution,[status(thm)],[f4458,f95]) ).
fof(f4597,plain,
! [X0,X1] : sum(additive_identity,multiply(X0,X1),multiply(X1,X0)),
inference(resolution,[status(thm)],[f4542,f30]) ).
fof(f4660,plain,
! [X0,X1,X2,X3] :
( product(X0,X1,multiply(X3,X2))
| ~ product(X0,X1,multiply(X2,X3)) ),
inference(resolution,[status(thm)],[f4597,f1968]) ).
fof(f5611,plain,
! [X0] :
( ~ sum(multiply(y,x_plus_y),z,X0)
| product(x_plus_y__plus_z,y_plus_z,X0) ),
inference(resolution,[status(thm)],[f673,f60]) ).
fof(f6702,plain,
! [X0,X1] : product(multiplicative_identity,multiply(X0,X1),multiply(X1,X0)),
inference(resolution,[status(thm)],[f4660,f34]) ).
fof(f6758,plain,
! [X0,X1,X2] : sum(multiply(X0,X1),X2,add(X2,multiply(X1,X0))),
inference(resolution,[status(thm)],[f6702,f3469]) ).
fof(f6759,plain,
! [X0,X1,X2] : sum(multiply(X0,X1),X2,add(multiply(X1,X0),X2)),
inference(resolution,[status(thm)],[f6702,f3470]) ).
fof(f7451,plain,
! [X0,X1,X2] : add(multiply(X0,X1),X2) = add(X2,multiply(X1,X0)),
inference(resolution,[status(thm)],[f6759,f209]) ).
fof(f7729,plain,
! [X0,X1,X2] : add(X0,multiply(X1,X2)) = add(X0,multiply(X2,X1)),
inference(resolution,[status(thm)],[f6758,f209]) ).
fof(f9957,plain,
product(x_plus_y__plus_z,y_plus_z,add(multiply(y,x_plus_y),z)),
inference(resolution,[status(thm)],[f5611,f28]) ).
fof(f9958,plain,
product(x_plus_y__plus_z,y_plus_z,add(z,multiply(x_plus_y,y))),
inference(forward_demodulation,[status(thm)],[f7451,f9957]) ).
fof(f9959,plain,
product(x_plus_y__plus_z,y_plus_z,add(z,multiply(y,x_plus_y))),
inference(forward_demodulation,[status(thm)],[f7729,f9958]) ).
fof(f10002,plain,
add(z,multiply(y,x_plus_y)) = multiply(y_plus_z,x_plus_y__plus_z),
inference(resolution,[status(thm)],[f9959,f99]) ).
fof(f10008,plain,
multiply(x_plus_y__plus_z,y_plus_z) = add(z,multiply(y,x_plus_y)),
inference(forward_demodulation,[status(thm)],[f121,f10002]) ).
fof(f10591,plain,
! [X0,X1] :
( ~ product(X1,additive_identity,X0)
| sum(X0,additive_identity,multiply(X1,inverse(X1))) ),
inference(resolution,[status(thm)],[f516,f55]) ).
fof(f10600,plain,
! [X0,X1] :
( ~ product(X1,additive_identity,X0)
| sum(X0,additive_identity,additive_identity) ),
inference(forward_demodulation,[status(thm)],[f119,f10591]) ).
fof(f10644,plain,
! [X0] : sum(multiply(X0,additive_identity),additive_identity,additive_identity),
inference(resolution,[status(thm)],[f10600,f29]) ).
fof(f10703,plain,
! [X0] : multiply(X0,additive_identity) = additive_identity,
inference(resolution,[status(thm)],[f10644,f208]) ).
fof(f10976,plain,
multiply(x_plus_y__plus_z,x_plus_y) = add(x_plus_y,additive_identity),
inference(backward_demodulation,[status(thm)],[f10703,f724]) ).
fof(f11159,plain,
x_plus_y = multiply(x_plus_y__plus_z,x_plus_y),
inference(forward_demodulation,[status(thm)],[f215,f10976]) ).
fof(f11253,plain,
sum(multiply(inverse(x_plus_y),x_plus_y__plus_z),x_plus_y,x_plus_y__plus_z),
inference(paramodulation,[status(thm)],[f11159,f1084]) ).
fof(f11260,plain,
sum(multiply(x_plus_y__plus_z,inverse(x_plus_y)),x_plus_y,x_plus_y__plus_z),
inference(forward_demodulation,[status(thm)],[f121,f11253]) ).
fof(f18997,plain,
! [X0,X1] :
( ~ sum(multiplicative_identity,X1,X0)
| product(X0,X1,add(X1,X1)) ),
inference(resolution,[status(thm)],[f1352,f630]) ).
fof(f23667,plain,
! [X0] : product(add(X0,multiplicative_identity),X0,add(X0,X0)),
inference(resolution,[status(thm)],[f18997,f111]) ).
fof(f24060,plain,
! [X0] : add(X0,X0) = multiply(add(X0,multiplicative_identity),X0),
inference(resolution,[status(thm)],[f23667,f74]) ).
fof(f24079,plain,
! [X0] : add(X0,X0) = multiply(X0,add(X0,multiplicative_identity)),
inference(forward_demodulation,[status(thm)],[f121,f24060]) ).
fof(f29017,plain,
! [X0,X1] :
( ~ sum(X1,multiplicative_identity,X0)
| product(multiplicative_identity,X0,multiplicative_identity) ),
inference(resolution,[status(thm)],[f1771,f53]) ).
fof(f29114,plain,
! [X0] : product(multiplicative_identity,add(X0,multiplicative_identity),multiplicative_identity),
inference(resolution,[status(thm)],[f29017,f28]) ).
fof(f29127,plain,
! [X0] : add(X0,multiplicative_identity) = multiplicative_identity,
inference(resolution,[status(thm)],[f29114,f71]) ).
fof(f29474,plain,
! [X0] : add(X0,X0) = multiply(X0,multiplicative_identity),
inference(backward_demodulation,[status(thm)],[f29127,f24079]) ).
fof(f29532,plain,
! [X0] : sum(multiplicative_identity,X0,multiplicative_identity),
inference(paramodulation,[status(thm)],[f29127,f111]) ).
fof(f29570,plain,
! [X0] : X0 = add(X0,X0),
inference(forward_demodulation,[status(thm)],[f78,f29474]) ).
fof(f29893,plain,
! [X0,X1,X2] :
( ~ product(X0,X2,X1)
| sum(X0,X1,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f866,f29532]) ).
fof(f31164,plain,
! [X0,X1] : sum(X0,multiply(X1,X0),X0),
inference(resolution,[status(thm)],[f29893,f95]) ).
fof(f31296,plain,
! [X0,X1,X2] :
( ~ sum(X0,X2,X1)
| product(add(X0,X0),X1,X0) ),
inference(resolution,[status(thm)],[f31164,f1983]) ).
fof(f31337,plain,
! [X0,X1] : add(multiply(X0,X1),X1) = X1,
inference(resolution,[status(thm)],[f31164,f209]) ).
fof(f31342,plain,
! [X0,X1] : sum(multiply(X0,X1),X1,X1),
inference(resolution,[status(thm)],[f31164,f30]) ).
fof(f31385,plain,
! [X0,X1] : X0 = add(X0,multiply(X0,X1)),
inference(forward_demodulation,[status(thm)],[f7451,f31337]) ).
fof(f31399,plain,
! [X0,X1,X2] :
( product(X0,X2,X0)
| ~ sum(X0,X1,X2) ),
inference(forward_demodulation,[status(thm)],[f29570,f31296]) ).
fof(f32001,plain,
! [X0] :
( product(X0,x__plus_y_plus_z,X0)
| ~ product(X0,y_plus_z,X0) ),
inference(resolution,[status(thm)],[f31342,f683]) ).
fof(f32739,plain,
product(z,y_plus_z,z),
inference(resolution,[status(thm)],[f31399,f103]) ).
fof(f32741,plain,
product(y,x_plus_y,y),
inference(resolution,[status(thm)],[f31399,f106]) ).
fof(f32742,plain,
product(y,y_plus_z,y),
inference(resolution,[status(thm)],[f31399,f60]) ).
fof(f32750,plain,
product(x,x_plus_y,x),
inference(resolution,[status(thm)],[f31399,f62]) ).
fof(f32841,plain,
product(x_plus_y,x,x),
inference(resolution,[status(thm)],[f32750,f31]) ).
fof(f32918,plain,
product(y_plus_z,y,y),
inference(resolution,[status(thm)],[f32742,f31]) ).
fof(f33018,plain,
y = multiply(x_plus_y,y),
inference(resolution,[status(thm)],[f32741,f99]) ).
fof(f33023,plain,
multiply(y,x_plus_y) = y,
inference(forward_demodulation,[status(thm)],[f121,f33018]) ).
fof(f33898,plain,
! [X0,X1] :
( ~ sum(X1,x_plus_y,X0)
| product(X0,x,add(multiply(X1,x),x)) ),
inference(resolution,[status(thm)],[f32841,f1356]) ).
fof(f33955,plain,
! [X0,X1] :
( ~ sum(X1,x_plus_y,X0)
| product(X0,x,add(x,multiply(x,X1))) ),
inference(forward_demodulation,[status(thm)],[f7451,f33898]) ).
fof(f33956,plain,
! [X0,X1] :
( ~ sum(X1,x_plus_y,X0)
| product(X0,x,x) ),
inference(forward_demodulation,[status(thm)],[f31385,f33955]) ).
fof(f33969,plain,
product(x__plus_y_plus_z,add(y,x),x_plus_y),
inference(resolution,[status(thm)],[f32918,f3678]) ).
fof(f34048,plain,
product(x__plus_y_plus_z,x_plus_y,x_plus_y),
inference(forward_demodulation,[status(thm)],[f272,f33969]) ).
fof(f34129,plain,
x_plus_y = multiply(x__plus_y_plus_z,x_plus_y),
inference(resolution,[status(thm)],[f34048,f74]) ).
fof(f34376,plain,
multiply(x_plus_y__plus_z,y_plus_z) = add(z,y),
inference(backward_demodulation,[status(thm)],[f33023,f10008]) ).
fof(f34573,plain,
multiply(x_plus_y__plus_z,y_plus_z) = add(y,z),
inference(forward_demodulation,[status(thm)],[f278,f34376]) ).
fof(f34574,plain,
y_plus_z = multiply(x_plus_y__plus_z,y_plus_z),
inference(forward_demodulation,[status(thm)],[f266,f34573]) ).
fof(f35300,plain,
product(x_plus_y__plus_z,y_plus_z,y_plus_z),
inference(paramodulation,[status(thm)],[f34574,f29]) ).
fof(f38091,plain,
product(z,x__plus_y_plus_z,z),
inference(resolution,[status(thm)],[f32001,f32739]) ).
fof(f38260,plain,
product(x__plus_y_plus_z,z,z),
inference(resolution,[status(thm)],[f38091,f31]) ).
fof(f40247,plain,
sum(multiply(x_plus_y,x__plus_y_plus_z),z,multiply(x__plus_y_plus_z,x_plus_y__plus_z)),
inference(resolution,[status(thm)],[f4172,f38260]) ).
fof(f40276,plain,
sum(multiply(x__plus_y_plus_z,x_plus_y),z,multiply(x__plus_y_plus_z,x_plus_y__plus_z)),
inference(forward_demodulation,[status(thm)],[f121,f40247]) ).
fof(f40277,plain,
sum(x_plus_y,z,multiply(x__plus_y_plus_z,x_plus_y__plus_z)),
inference(forward_demodulation,[status(thm)],[f34129,f40276]) ).
fof(f41307,plain,
multiply(x__plus_y_plus_z,x_plus_y__plus_z) = add(x_plus_y,z),
inference(resolution,[status(thm)],[f40277,f210]) ).
fof(f41318,plain,
multiply(x__plus_y_plus_z,x_plus_y__plus_z) = add(z,x_plus_y),
inference(forward_demodulation,[status(thm)],[f278,f41307]) ).
fof(f41319,plain,
multiply(x__plus_y_plus_z,x_plus_y__plus_z) = x_plus_y__plus_z,
inference(forward_demodulation,[status(thm)],[f257,f41318]) ).
fof(f41867,plain,
sum(multiply(x,x_plus_y__plus_z),y_plus_z,multiply(x_plus_y__plus_z,x__plus_y_plus_z)),
inference(resolution,[status(thm)],[f4266,f35300]) ).
fof(f41878,plain,
sum(multiply(x,x_plus_y__plus_z),y_plus_z,multiply(x__plus_y_plus_z,x_plus_y__plus_z)),
inference(forward_demodulation,[status(thm)],[f121,f41867]) ).
fof(f41879,plain,
sum(multiply(x,x_plus_y__plus_z),y_plus_z,x_plus_y__plus_z),
inference(forward_demodulation,[status(thm)],[f41319,f41878]) ).
fof(f42592,plain,
x_plus_y__plus_z = add(y_plus_z,multiply(x,x_plus_y__plus_z)),
inference(resolution,[status(thm)],[f41879,f209]) ).
fof(f61297,plain,
product(x_plus_y__plus_z,x,x),
inference(resolution,[status(thm)],[f33956,f11260]) ).
fof(f61392,plain,
x = multiply(x,x_plus_y__plus_z),
inference(resolution,[status(thm)],[f61297,f99]) ).
fof(f61488,plain,
x_plus_y__plus_z = add(y_plus_z,x),
inference(backward_demodulation,[status(thm)],[f61392,f42592]) ).
fof(f61722,plain,
x_plus_y__plus_z = add(x,y_plus_z),
inference(forward_demodulation,[status(thm)],[f278,f61488]) ).
fof(f61723,plain,
x_plus_y__plus_z = x__plus_y_plus_z,
inference(forward_demodulation,[status(thm)],[f223,f61722]) ).
fof(f61724,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f61723,f64]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO008-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.37 % Computer : n026.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 21 13:49:51 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.39 % Drodi V4.1.1
% 173.15/23.32 % Refutation found
% 173.15/23.32 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 173.15/23.32 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 173.15/23.39 % Elapsed time: 22.993157 seconds
% 173.15/23.39 % CPU time: 182.199516 seconds
% 173.15/23.39 % Total memory used: 376.756 MB
% 173.15/23.39 % Net memory used: 321.061 MB
%------------------------------------------------------------------------------